added prdcns to checking xtors

ps-tuebingen · Jun 18, 2024 · 26e12c5 · 26e12c5
1 parent d442bdd
commit 26e12c5
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 8 deletions.
diff --git a/one-sided-defs/src/Common.purs b/one-sided-defs/src/Common.purs
@@ -10,6 +10,7 @@ module Common (
   Xtorname (..),
   Variance (..),
   PrdCns (..),
+  multPrdCns,
   EvaluationOrder (..),
   defaultEo,
   DeclTy (..),
@@ -77,6 +78,14 @@ instance Show PrdCns where
   show Cns = "cns"
   show PrdCns = "prdcns"
 
+multPrdCns :: PrdCns -> PrdCns -> PrdCns
+multPrdCns Prd Prd   = Prd 
+multPrdCns Cns Cns   = Cns 
+multPrdCns Prd Cns   = Cns
+multPrdCns Cns Prd   = Cns 
+multPrdCns PrdCns pc = pc
+multPrdCns pc PrdCns = pc
+
 --------------------------------------------------------
 -------------- Classes for Free Variables --------------
 --------------------------------------------------------

diff --git a/one-sided-defs/src/Syntax/Kinded/Program.purs b/one-sided-defs/src/Syntax/Kinded/Program.purs
@@ -23,7 +23,7 @@ import Prelude ((&&), (==), class Show, show, (<>), (<$>))
 import Data.List (List, null, intercalate)
 import Data.Map (Map,insert, empty,isEmpty)
 import Data.Maybe (Maybe(..),isNothing)
-import Data.Tuple (Tuple(..))
+import Data.Tuple (Tuple)
 import Data.Bifunctor (rmap)
 
 data XtorSig = XtorSig{sigPos :: Loc, sigName :: Xtorname, sigArgs :: List (Tuple PrdCns Ty)} 

diff --git a/one-sided-defs/src/Syntax/Kinded/Substitution.purs b/one-sided-defs/src/Syntax/Kinded/Substitution.purs
@@ -7,7 +7,7 @@ module Syntax.Kinded.Substitution (
 ) where 
 
 import Syntax.Kinded.Terms (Term(..),Command(..),Pattern(..))
-import Syntax.Kinded.Types (Ty(..))
+import Syntax.Kinded.Types (Ty)
 import Common (Variable,Typevar)
 
 import Prelude ((<$>))

diff --git a/one-sided-kinding/src/Kinding/Terms.purs b/one-sided-kinding/src/Kinding/Terms.purs
@@ -9,17 +9,17 @@ import Kinding.Types (checkKindType)
 import Environment (lookupXtorDecl,lookupXtor)
 import Errors (zipWithErrorM)
 import Loc (Loc)
-import Common (PrdCns(..),EvaluationOrder(..), getKind,Kind, DeclTy(..))
+import Common (PrdCns(..),EvaluationOrder(..), getKind,Kind, DeclTy(..),multPrdCns)
 import Syntax.Typed.Terms (Term(..),Pattern(..),Command(..))              as T 
 import Syntax.Typed.Types (Ty(..)) as T
 import Syntax.Kinded.Terms (Term(..),Pattern(..),Command(..), getPrdCns)  as K
 import Syntax.Kinded.Program (DataDecl(..), XtorSig(..))                  as K
 
-import Prelude ((<$>),($), bind,pure, (>>>))
+import Prelude ((<$>),($), bind,pure)
 import Control.Monad.Except (throwError)
 import Data.Traversable (for)
 import Data.List(List(..))
-import Data.Tuple (Tuple(..),snd)
+import Data.Tuple (Tuple(..))
 
 
 checkPatterns :: Loc -> List T.Pattern -> KindM (Tuple K.DataDecl (List K.Pattern))
@@ -61,12 +61,12 @@ kindTerm (T.Xtor loc nm args ty) pc eo = do
   let Tuple ty' pc' = getCo XTor decl.declType pc ty  
   ty'' <- checkKindType ty' eo
   (K.XtorSig sig) <- lookupXtor loc nm
-  let argKnds :: List Kind 
-      argKnds = snd >>> getKind <$> sig.sigArgs
+  let argKnds :: List (Tuple PrdCns Kind)
+      argKnds = (\(Tuple pc'' ty) ->  Tuple (multPrdCns pc' pc'') (getKind ty))<$> sig.sigArgs
   let kndFun eo' = pure eo'
   argKnds' <- for argKnds kndFun 
   argsZipped <- zipWithErrorM args argKnds' (ErrXtorArity loc nm)
-  args' <- for argsZipped (\(Tuple arg knd)  -> kindTerm arg pc knd)
+  args' <- for argsZipped (\(Tuple arg (Tuple pc'' knd))  -> kindTerm arg pc'' knd)
   pure $ K.Xtor loc pc' nm args' ty''
 
 kindTerm (T.XCase loc pts ty) pc eo = do