diff --git a/one-sided-defs/src/Common.purs b/one-sided-defs/src/Common.purs index 4635125..f08fae3 100644 --- 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 index cd0ac88..f439a0d 100644 --- 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 index 9ddd5c1..4855d88 100644 --- 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 index afd4cfb..ad04953 100644 --- 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