"pre-commit-hooks": "pre-commit-hooks_2"
},
"locked": {
- "lastModified": 1693351084,
- "narHash": "sha256-uS5fbMlqU6dyGSVhBQd6UsFAFSVkFZsi8lzWp0JK1bI=",
+ "lastModified": 1693433189,
+ "narHash": "sha256-k4bWG1z6qvt7Cee15H0xwgVngBBQRqhFm4rp6JHn8Qg=",
"ref": "refs/heads/main",
- "rev": "e113439871b322cb047c8b6021760eef6cd84520",
- "revCount": 94,
+ "rev": "9d93dbea0b1173304ac78b695371b3e14d0d8b9f",
+ "revCount": 100,
"type": "git",
"url": "git://git.sourcephile.fr/haskell/symantic-base"
},
+{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Control.Applicative (Applicative (..))
import Data.Function ((.))
import Data.Function qualified as Fun
+import Data.Monoid (Monoid)
import GHC.Types (Constraint, Type)
+import Symantic.Semantics.Eval (Eval (..))
import Symantic.Semantics.Forall
import Symantic.Syntaxes.Classes (Syntaxes, Unabstractable (..))
import Type.Reflection (Typeable)
type Syntax = Semantic -> Constraint
-- * Class 'AbstractableTy'
-class AbstractableTy meta sem where
+class AbstractableTy ty sem where
-- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
- lamTy :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)
+ lamTy :: ty a -> (sem a -> sem b) -> sem (a -> b)
fun ::
- AbstractableTy () sem =>
+ forall prov sem a b.
+ Monoid prov =>
+ AbstractableTy (Ty prov '[]) sem =>
Typeable a =>
(sem a -> sem b) ->
sem (a -> b)
-fun = lamTy (monoTy @_ @())
+fun = lamTy (monoTy @_ @prov)
-- * Class 'Constable'
class Constable sem where
constB = Forall constB
constC = Forall constC
instance
- ( forall sem. Syntaxes syns sem => AbstractableTy meta sem
+ ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
-- , forall sem a. syn sem => AbstractableLam sem a
-- , forall sem. syn sem => AbstractableLam sem a
-- , forall sem. syn sem => Typeable sem -- user instance not accepted
-- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
) =>
- AbstractableTy meta (Forall syns)
+ AbstractableTy (Ty prov '[]) (Forall syns)
where
lamTy aTy f = Forall (lamTy aTy (\a -> let Forall b = f (forallSem a) in b))
where
-- * Type 'OpenTerm'
data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
- -- E contains embedded closed (i.e. already abstracted) terms.
+ -- | 'E' contains embedded closed (i.e. already abstracted) terms.
E :: Forall syns a -> OpenTerm syns vs a
- -- V represents a reference to the innermost/top environment
- -- variable, i.e. Z
+ -- | 'V' represents a reference to the innermost/top environment variable, i.e. Z
V :: OpenTerm syns (a ': vs) a
- -- N represents internalizing the innermost bound variable as a
+ -- | 'N' represents internalizing the innermost bound variable as a
-- function argument. In other words, we can represent an open
-- term referring to a certain variable as a function which
-- takes that variable as an argument.
N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
- -- For efficiency, there is also a special variant of N for the
- -- case where the term does not refer to the topmost variable at all.
+ -- | 'W' is a special variant of N for efficiency,
+ -- in the case where the term does not refer
+ -- to the topmost variable at all.
W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
instance
- ( forall sem. Syntaxes syns sem => AbstractableTy meta sem
+ ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
, Syntaxes syns (Forall syns)
) =>
- AbstractableTy meta (OpenTerm syns '[])
+ AbstractableTy (Ty prov '[]) (OpenTerm syns '[])
where
- lamTy aTy f = E (lamTy aTy (runOpenTerm . f . E))
+ lamTy aTy f = E (lamTy aTy (unE . f . E))
instance
( forall sem. Syntaxes syns sem => Constable sem
, Syntaxes syns (Forall syns)
constB = E constB
constC = E constC
--- * Type 'R'
-newtype R a = R {unR :: a}
-instance AbstractableTy meta R where
- lamTy _aTy f = R (unR . f . R)
-instance Unabstractable R where
- R f .@ R x = R (f x)
-instance Constable R where
- constI = R Fun.id
- constK = R Fun.const
- constS = R (<*>)
- constB = R (.)
- constC = R Fun.flip
+instance AbstractableTy (Ty prov '[]) Eval where
+ lamTy _aTy f = Eval (unEval . f . Eval)
+instance Constable Eval where
+ constI = Eval Fun.id
+ constK = Eval Fun.const
+ constS = Eval (<*>)
+ constB = Eval (.)
+ constC = Eval Fun.flip
-runOpenTerm :: OpenTerm syns '[] a -> Forall syns a
-runOpenTerm t = case t of E t' -> t'
+runOpenTerm :: Syntaxes syns Eval => OpenTerm syns '[] a -> a
+runOpenTerm t | E (Forall sem) <- t = unEval sem
-eval :: Syntaxes syns R => OpenTerm syns '[] a -> a
-eval t
- | Forall sem <- runOpenTerm t =
- unR sem
+unE :: OpenTerm syns '[] a -> Forall syns a
+unE t = case t of E t' -> t'
instance
( forall sem. Syntaxes syns sem => Constable sem
OpenTerm syns as (a -> b) ->
OpenTerm syns as a ->
OpenTerm syns as b
-W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)
-W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
-E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
-W e `appOpenTerm` V = N e
-V `appOpenTerm` W e = N (E (constC .@ constI) `appOpenTerm` e)
-W e1 `appOpenTerm` N e2 = N (E constB `appOpenTerm` e1 `appOpenTerm` e2)
-N e1 `appOpenTerm` W e2 = N (E constC `appOpenTerm` e1 `appOpenTerm` e2)
-N e1 `appOpenTerm` N e2 = N (E constS `appOpenTerm` e1 `appOpenTerm` e2)
-N e `appOpenTerm` V = N (E constS `appOpenTerm` e `appOpenTerm` E constI)
-V `appOpenTerm` N e = N (E (constS .@ constI) `appOpenTerm` e)
E d `appOpenTerm` N e = N (E (constB .@ d) `appOpenTerm` e)
E d `appOpenTerm` V = N (E d)
-V `appOpenTerm` E d = N (E (constC .@ constI .@ d))
-N e `appOpenTerm` E d = N (E (constC .@ constC .@ d) `appOpenTerm` e)
+E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
E d1 `appOpenTerm` E d2 = E (d1 .@ d2)
+N e `appOpenTerm` E d = N (E (constC .@ constC .@ d) `appOpenTerm` e)
+N e `appOpenTerm` V = N (E constS `appOpenTerm` e `appOpenTerm` E constI)
+N e1 `appOpenTerm` N e2 = N (E constS `appOpenTerm` e1 `appOpenTerm` e2)
+N e1 `appOpenTerm` W e2 = N (E constC `appOpenTerm` e1 `appOpenTerm` e2)
+V `appOpenTerm` E d = N (E (constC .@ constI .@ d))
+V `appOpenTerm` N e = N (E (constS .@ constI) `appOpenTerm` e)
+V `appOpenTerm` W e = N (E (constC .@ constI) `appOpenTerm` e)
+W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
+W e `appOpenTerm` V = N e
+W e1 `appOpenTerm` N e2 = N (E constB `appOpenTerm` e1 `appOpenTerm` e2)
+W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)
import Symantic.Typer
-- * Type 'Parser'
-data Parser syns meta = Parser
+data Parser syns prov = Parser
{ unParser ::
- ( -- MT.State (TokenTerm meta a)
+ ( -- MT.State (TokenTerm prov a)
forall vs.
- CtxTy meta vs Void ->
- Either (PerSyntax syns (ErrorParser meta)) (TermVT syns meta vs)
+ CtxTy prov vs Void ->
+ Either (PerSyntax syns (ErrorParser prov)) (TermVT syns prov vs)
)
}
type ErrMsg = String
-- * Data family 'ErrorParser'
-data family ErrorParser meta (syn :: Syntax)
+data family ErrorParser prov (syn :: Syntax)
---- * Type 'SomeParsingError'
-- data SomeParsingError
-- Maybe.Just HRefl -> Maybe.Just constr
-- Maybe.Nothing -> Maybe.Nothing
-data TermVT syns meta vs = forall a vs'.
+data TermVT syns prov vs = forall a vs'.
TermVT
- { termVTType :: Ty meta vs' a
+ { termVTType :: Ty prov vs' a
, unTermVT :: OpenTerm syns vs a
}
| BinTree2 (BinTree a) (BinTree a)
deriving (Eq, Show)
-type TermAST meta = BinTree (TokenTerm meta)
-data TokenTerm meta
- = TokenTermAbst String (TyT meta '[]) (TermAST meta)
+type TermAST prov = BinTree (TokenTerm prov)
+data TokenTerm prov
+ = TokenTermAbst String (TyT prov '[]) (TermAST prov)
| TokenTermVar Name
| TokenTermAtom String
deriving (Show)
-- It is built top-down from the closest
-- including /lambda abstraction/ to the farest.
-- It determines the 'Type's of 'CtxTe'.
-data CtxTy meta (as :: [Type]) void where
- CtxTyZ :: CtxTy meta '[] Void
- CtxTyS :: NameTe -> Ty meta '[] a -> CtxTy meta as Void -> CtxTy meta (a ': as) Void
+data CtxTy prov (as :: [Type]) void where
+ CtxTyZ :: CtxTy prov '[] Void
+ CtxTyS :: NameTe -> Ty prov '[] a -> CtxTy prov as Void -> CtxTy prov (a ': as) Void
infixr 5 `CtxTyS`
module Symantic.Parser.Source where
-import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Control.Monad.Classes qualified as MC
import Control.Monad.Trans.Writer.CPS qualified as MT
import Data.Bool (Bool (..))
import Data.Eq (Eq)
import Data.Function ((.))
-import Data.Functor (Functor)
import Data.Functor.Classes (Show1 (..), liftShowList2, liftShowsPrec2, showsPrec1, showsUnaryWith)
import Data.Kind (Type)
import Data.Monoid (Monoid (..))
import Data.Ord (Ord)
-import Data.Semigroup (Semigroup (..))
import Data.Tuple (fst)
import Data.Typeable (Typeable)
import Text.Show (Show (..))
import Symantic.Parser
-- TODO: var num
-newtype Printer meta a = Printer {unPrinter :: TermAST meta}
-print :: Printer meta a -> TermAST meta
+newtype Printer prov a = Printer {unPrinter :: TermAST prov}
+print :: Printer prov a -> TermAST prov
print = unPrinter
-print2 :: String -> Printer meta a1 -> Printer meta a2 -> Printer meta a3
+print2 :: String -> Printer prov a1 -> Printer prov a2 -> Printer prov a3
print2 n (Printer aT) (Printer bT) = Printer $ BinTree2 (BinTree2 (BinTree0 (TokenTermAtom n)) aT) bT
import Symantic.Typer ()
parse ::
- forall syns meta finalSyns.
+ forall syns prov finalSyns.
finalSyns ~ (Unabstractable ': Constable ': syns) =>
- Show meta =>
- Monoid meta =>
+ (forall k. ProvenanceKindOf (Ty @k) prov) =>
+ (forall k. ProvenanceKindOf (Var @k) prov) =>
+ Show prov =>
+ Monoid prov =>
Syntaxes finalSyns (Forall finalSyns) =>
- Parsers finalSyns finalSyns meta =>
- TermAST meta ->
- Either (PerSyntax finalSyns (ErrorParser meta)) (TermVT finalSyns meta '[])
+ Parsers finalSyns finalSyns prov =>
+ TermAST prov ->
+ Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov '[])
parse ast = unParser (fix openParser ast) CtxTyZ
where
-- Unabstractable and Constable are always required.
TyApp
{ tyAppFun =
TyApp
- { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
+ { tyAppFun = TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
, tyAppArg = fxTy
}
, tyAppArg = rTy
Nothing -> Left $ perSyntax $ ErrorParserUnabstractableArgumentMismatch (TyVT fxTy'') (TyVT xTy'')
Just HRefl -> Right $ TermVT rTy $ f .@ a
_ -> Left $ perSyntax $ ErrorParserUnabstractableNotAFunction (TyVT fTy)
- openParser final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e
-data instance ErrorParser meta Unabstractable
- = ErrorParserUnabstractableArgumentMismatch (TyVT meta) (TyVT meta)
- | ErrorParserUnabstractableNotAFunction (TyVT meta)
- | ErrorParserUnabstractableUnify (ErrorUnify meta)
- deriving (Show)
-
-data instance ErrorParser meta Constable
- = ErrorParserConstableInvalid (TokenTerm meta)
+ openParser final (BinTree0 e) = parsers @finalSyns @finalSyns @prov final e
+data instance ErrorParser prov Unabstractable
+ = ErrorParserUnabstractableArgumentMismatch (TyVT prov) (TyVT prov)
+ | ErrorParserUnabstractableNotAFunction (TyVT prov)
+ | ErrorParserUnabstractableUnify (ErrorUnify prov)
deriving (Show)
-- * Class 'Parsers'
-class Parsers syns finalSyns meta where
- parsers :: OpenParser finalSyns meta
-instance PerSyntaxable finalSyns Constable => Parsers '[] finalSyns meta where
+class Parsers syns finalSyns prov where
+ parsers :: OpenParser finalSyns prov
+instance PerSyntaxable finalSyns Constable => Parsers '[] finalSyns prov where
parsers _final tok = Parser $ \_ctx ->
Left $ perSyntax $ ErrorParserConstableInvalid tok
+data instance ErrorParser prov Constable
+ = ErrorParserConstableInvalid (TokenTerm prov)
+ deriving (Show)
instance
- ( TokenParser syn finalSyns meta
- , Parsers syns finalSyns meta
+ ( TokenParser syn finalSyns prov
+ , Parsers syns finalSyns prov
) =>
- Parsers (syn ': syns) finalSyns meta
+ Parsers (syn ': syns) finalSyns prov
where
parsers final = tokenParser @syn @finalSyns (parsers @syns @finalSyns final) final
-- ** Type 'OpenParser'
-type OpenParser syns meta =
- Show meta =>
- Monoid meta =>
- {-final-} (TermAST meta -> Parser syns meta) ->
- TokenTerm meta ->
- Parser syns meta
+type OpenParser syns prov =
+ Show prov =>
+ Monoid prov =>
+ {-final-} (TermAST prov -> Parser syns prov) ->
+ TokenTerm prov ->
+ Parser syns prov
-- ** Class 'TokenParser'
-class TokenParser syn finalSyns meta where
+class TokenParser syn finalSyns prov where
tokenParser ::
- {-next-} (TokenTerm meta -> Parser finalSyns meta) ->
- OpenParser finalSyns meta
+ {-next-} (TokenTerm prov -> Parser finalSyns prov) ->
+ OpenParser finalSyns prov
instance
( Syntaxes finalSyns (Forall finalSyns)
) =>
- TokenParser Unabstractable finalSyns meta
+ TokenParser Unabstractable finalSyns prov
where
tokenParser next _final = next
-data instance ErrorParser meta (AbstractableTy meta)
+data instance ErrorParser prov (AbstractableTy (Ty prov '[]))
= ErrorParserAbstractableUnknown Name
- | ErrorParserAbstractableNotAType (TyVT meta)
+ | ErrorParserAbstractableNotAType (TyVT prov)
deriving (Show)
instance
( Syntaxes finalSyns (Forall finalSyns)
, forall sem. Syntaxes finalSyns sem => Constable sem
, forall sem. Syntaxes finalSyns sem => Unabstractable sem
- , PerSyntaxable finalSyns (AbstractableTy meta)
+ , PerSyntaxable finalSyns (AbstractableTy (Ty prov '[]))
+ , forall k. ProvenanceKindOf (Ty @k) prov
) =>
- TokenParser (AbstractableTy meta) finalSyns meta
+ TokenParser (AbstractableTy (Ty prov '[])) finalSyns prov
where
tokenParser _next _final (TokenTermVar vN) = Parser go
where
- go :: forall vs. CtxTy meta vs Void -> Either (PerSyntax finalSyns (ErrorParser meta)) (TermVT finalSyns meta vs)
+ go :: forall vs. CtxTy prov vs Void -> Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov vs)
go CtxTyZ = Left $ perSyntax $ ErrorParserAbstractableUnknown vN
go (CtxTyS n ty _) | n == vN = Right $ TermVT ty $ V
go (CtxTyS _n _typ tys) = do
TermVT ty ot <- go tys
Right $ TermVT ty $ W ot
- tokenParser _next final (TokenTermAbst argName (TyT (argTy :: Ty meta '[] a)) bT) =
+ tokenParser _next final (TokenTermAbst argName (TyT (argTy :: Ty prov '[] a)) bT) =
Parser $ \ctx ->
- case eqTy (monoTy @Type @meta) (kindOf argTy) of
+ case eqTy (monoTy @Type @prov) (kindOf argTy) of
Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT argTy)
Just HRefl -> do
TermVT resTy (b :: OpenTerm syn bVS b) <- (unParser (final bT)) (CtxTyS argName argTy ctx)
( Syntaxes finalSyns (Forall finalSyns)
, forall sem. Syntaxes finalSyns sem => Addable sem
) =>
- TokenParser Addable finalSyns meta
+ TokenParser Addable finalSyns prov
where
tokenParser next _final = \case
TokenTermAtom s
Parser $ \ctx ->
Right
$ TermVT
- (tyOfTypeRep mempty (lenVar ctx) (typeRep @Int))
+ (tyOfTypeRep (lenVar ctx) (typeRep @Int))
$ E
$ Forall @_ @Int
$ lit i
( Syntaxes syns (Forall syns)
, forall sem. Syntaxes syns sem => Constable sem
) =>
- TokenParser Constable syns meta
+ TokenParser Constable syns prov
where
tokenParser next _final = \case
TokenTermAtom "id" -> Parser $ \_ctx ->
lit :: Int -> sem Int
neg :: sem (Int -> Int)
add :: sem (Int -> Int -> Int)
-data instance ErrorParser meta Addable
+data instance ErrorParser prov Addable
deriving (Show)
-- * Class 'Mulable'
-- tree0Parser = unParser $ parse tree0Print
-- parseMulable ::
--- forall syn meta.
+-- forall syn prov.
-- ( forall sem. syn sem => Mulable sem
-- , forall sem. syn sem => Addable sem
-- , syn (Forall syn)
-- ) =>
--- Monoid meta =>
--- Show meta =>
--- (TermAST meta -> Parser syn meta) ->
--- TermAST meta -> Parser syn meta
+-- Monoid prov =>
+-- Show prov =>
+-- (TermAST prov -> Parser syn prov) ->
+-- TermAST prov -> Parser syn prov
-- parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "mul")) aT) bT) =
-- Parser $ \ctx -> do
-- case (final aT, final bT) of
-- (Parser aE, Parser bE) -> do
-- TermVT aTy (Forall a :: Forall syn a) <- aE ctx
--- case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar aTy} of
+-- case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::prov}, tyConstLen = lenVar aTy} of
-- Nothing -> Left "TypeError: Mulable 1"
-- Just HRefl -> do
-- TermVT bTy (Forall b :: Forall syn b) <- bE ctx
--- case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar bTy} of
+-- case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::prov}, tyConstLen = lenVar bTy} of
-- Nothing -> Left "TypeError: Mulable 2"
-- Just HRefl -> do
-- Right $ TermVT aTy (Forall @_ @a $ mul a b)
printConst n = Printer (BinTree0 (TokenTermAtom n))
-instance Constable (Printer meta) where
+instance Constable (Printer prov) where
constI = printConst "id"
constK = printConst "const"
constS = printConst "(<*>)"
constB = printConst "(.)"
constC = printConst "flip"
-instance Addable (Printer meta) where
+instance Addable (Printer prov) where
lit n = Printer $ BinTree0 (TokenTermAtom (show n))
neg = printConst "neg"
add = printConst "add"
-instance Mulable (Printer meta) where
+instance Mulable (Printer prov) where
mul = print2 "mul"
-instance Unabstractable (Printer meta) where
+instance Unabstractable (Printer prov) where
Printer f .@ Printer a = Printer $ BinTree2 f a
-instance (Monoid meta) => AbstractableTy meta (Printer meta) where
- lamTy xTy (f :: Printer meta a -> Printer meta b) =
+instance (Monoid prov) => AbstractableTy (Ty prov '[]) (Printer prov) where
+ lamTy xTy (f :: Printer prov a -> Printer prov b) =
Printer $
BinTree0
( TokenTermAbst
)
-- * Type 'FinalSyntaxes'
-type FinalSyntaxes meta = '[AbstractableTy meta, Addable]
+type FinalSyntaxes prov = '[AbstractableTy (Ty prov '[]), Addable]
-- tree0 = lit 0
tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))
-- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
-tree2 = fun (\x -> add .@ x .@ lit 0)
-tree3 = fun (\x -> add .@ x .@ x)
+tree2 = fun @() (\x -> add .@ x .@ lit 0)
+tree3 = fun @() (\x -> add .@ x .@ x)
tree4 = constS .@ add .@ constI
tree0Print = print tree0
tree0ParsePrint :: TermAST ()
tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
Left e -> error $ show e
- Right (TermVT _ty (runOpenTerm -> Forall sem)) -> print sem
+ Right (TermVT _ty (unE -> Forall sem)) -> print sem
-- tree1ParsePrint :: TermAST ()
-- tree1ParsePrint = case parse @(FinalSyntaxes ()) @() tree1Print of
-- Left e -> error e
--- Right (TermVT _ty (runOpenTerm -> Forall sem)) -> print sem
+-- Right (TermVT _ty (unE -> Forall sem)) -> print sem
tree2ParsePrint :: TermAST ()
tree2ParsePrint = case parse @(FinalSyntaxes ()) @() tree2Print of
Left e -> error $ show e
- Right (TermVT _ty (runOpenTerm -> Forall sem)) -> print sem
+ Right (TermVT _ty (unE -> Forall sem)) -> print sem
tree3ParsePrint :: TermAST ()
tree3ParsePrint = case parse @(FinalSyntaxes ()) @() tree3Print of
Left e -> error $ show e
- Right (TermVT _ty (runOpenTerm -> Forall sem)) -> print sem
+ Right (TermVT _ty (unE -> Forall sem)) -> print sem
tree3ParsePrint' :: TermAST ()
tree3ParsePrint' = case parse @(FinalSyntaxes ()) @() tree3ParsePrint of
Left e -> error $ show e
- Right (TermVT _ty (runOpenTerm -> Forall sem)) -> print sem
+ Right (TermVT _ty (unE -> Forall sem)) -> print sem
tree4ParsePrint :: TermAST ()
tree4ParsePrint = case parse @(FinalSyntaxes ()) @() tree4Print of
Left e -> error $ show e
- Right (TermVT _ty (runOpenTerm -> Forall sem)) -> print sem
+ Right (TermVT _ty (unE -> Forall sem)) -> print sem
import Data.Kind (Type)
import Data.Maybe (Maybe (..))
import GHC.Stack (HasCallStack)
-import Type.Reflection ((:~~:) (..))
+import Type.Reflection (TypeRep, eqTypeRep, (:~~:) (..))
class EqTy (x :: xK -> Type) (y :: yK -> Type) where
-- | /Heterogeneous type equality/:
-- return two proofs when two types are equals:
-- one for the type and one for the kind.
eqTy :: HasCallStack => x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)
+instance EqTy TypeRep TypeRep where
+ eqTy = eqTypeRep
import Control.Monad.Classes as MC ()
import Control.Monad.Classes.Run as MC ()
import Data.Eq (Eq (..))
-import Data.Function (($), (.))
+import Data.Function (($))
import Data.Functor ((<$>))
import Data.Map.Strict qualified as Map
import Data.Maybe (Maybe (..), isJust)
import GHC.Types
import Text.Show (Show (..))
import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..), pattern App)
-import Prelude (error)
import Prelude qualified
import Symantic.Typer.Eq
import Symantic.Typer.List
-data Const meta (a :: aK) = Const
- { constType :: TypeRep a
- , constMeta :: meta
- }
- deriving (Show)
-instance EqTy (Const meta) (Const meta) where
- eqTy Const{constType = x} Const{constType = y} = eqTypeRep x y
+data WithProv prov a = WithProv {withProv :: prov, unWithProv :: a}
+-- * Type 'Const'
+type Const = TypeRep
+
+-- * Type 'Name'
type Name = String
+-- * Type 'Prov'
+type Prov = Type
+
-- * Type 'Var'
-data Var :: forall vK. Type -> [Type] -> vK -> Type where
+data Var :: forall vK. Prov -> [Type] -> vK -> Type where
VarZ ::
- { varZKind :: Kind meta vK
+ { varZKind :: Kind prov vK
, varZNext :: Len ws
- , varZMeta :: meta
} ->
- Var meta (Proxy (v :: vK) ': ws) (v :: vK)
- VarS :: Var meta vs v -> Var meta (not_v ': vs) v
-deriving instance Show meta => Show (Var meta vs v)
+ Var prov (Proxy (v :: vK) ': ws) (v :: vK)
+ VarS :: Var prov vs v -> Var prov (not_v ': vs) v
+deriving instance Show prov => Show (Var prov vs v)
-pattern Var :: () => () => Kind meta vK -> Len ws -> meta -> Var meta vs' (v :: vK)
-pattern Var{varKind, varNext, varMeta} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext, varZMeta = varMeta})
+pattern Var :: () => () => Kind prov vK -> Len ws -> Var prov vs' (v :: vK)
+pattern Var{varKind, varNext} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext})
{-# COMPLETE Var #-}
-- -- * Type 'VarVS'
-data VarVS meta (v :: vK) = forall vs. VarVS (Var meta vs v)
-var :: Var meta vs (v :: vK) -> VarVS meta (v :: vK)
+data VarVS prov (v :: vK) = forall vs. VarVS (Var prov vs v)
+var :: Var prov vs (v :: vK) -> VarVS prov (v :: vK)
var v@VarZ{} = VarVS v
var (VarS v) = var v
-instance EqTy (Var meta vs) (Var meta vs) where
+instance EqTy (Var prov vs) (Var prov vs) where
eqTy VarZ{} VarZ{} = Just HRefl
eqTy (VarS x) (VarS y) = eqTy x y
eqTy _ _ = Nothing
type VarSem = Type -> [Type] -> Type -> Type
-- data VarV (var::VarSem) vs = forall vK (v::vK). VarVSem (var vs v)
-data VarV meta vs = forall v. VarV (Var meta vs v)
+data VarV prov vs = forall v. VarV (Var prov vs v)
class LenVar var where
- lenVar :: var meta vs a -> Len vs
+ lenVar :: var prov vs a -> Len vs
instance LenVar Var where
lenVar VarZ{varZNext} = LenS varZNext
lenVar (VarS v) = LenS (lenVar v)
class LenVar var => AllocVars var where
- allocVarsL :: Len len -> var meta vs x -> var meta (len ++ vs) x
- allocVarsR :: Len len -> var meta vs x -> var meta (vs ++ len) x
+ allocVarsL :: Len len -> var prov vs x -> var prov (len ++ vs) x
+ allocVarsR :: Len len -> var prov vs x -> var prov (vs ++ len) x
instance AllocVars Var where
allocVarsL LenZ v = v
allocVarsL (LenS len) v = VarS (allocVarsL len v)
appendVars ::
AllocVars xVar =>
AllocVars yVar =>
- xVar meta xVS (x :: xK) ->
- yVar meta yVS (y :: yK) ->
- ( xVar meta (xVS ++ yVS) x
- , yVar meta (xVS ++ yVS) y
+ xVar prov xVS (x :: xK) ->
+ yVar prov yVS (y :: yK) ->
+ ( xVar prov (xVS ++ yVS) x
+ , yVar prov (xVS ++ yVS) y
)
appendVars x y =
( allocVarsR (lenVar y) x
-- | Index of a 'Var'.
type IndexVar = Int
-indexVar :: Var meta vs v -> Int
+indexVar :: Var prov vs v -> Int
indexVar VarZ{} = 0
indexVar (VarS v) = 1 Prelude.+ indexVar v
--- instance KindOf (Var meta vs) where
+-- instance KindOf (Var prov vs) where
-- kindOf = fmap go
-- where
--- go :: forall vs2 aK a. Var meta vs2 (Proxy (a::aK)) -> TypeRep aK
+-- go :: forall vs2 aK a. Var prov vs2 (Proxy (a::aK)) -> TypeRep aK
-- go VarZ{varKind} = varKind
-- go (VarS v) = go v
-- * Type 'Vars'
-type Vars meta vs = Map.Map Name (VarV meta vs)
+type Vars prov vs = Map.Map Name (VarV prov vs)
-lookupVar :: Name -> Vars meta vs -> Maybe (VarV meta vs)
+lookupVar :: Name -> Vars prov vs -> Maybe (VarV prov vs)
lookupVar = Map.lookup
-insertVar :: Name -> VarV meta vs -> Vars meta vs -> Vars meta vs
+insertVar :: Name -> VarV prov vs -> Vars prov vs -> Vars prov vs
insertVar = Map.insert
-- * Type 'UsedVars'
-- | List of 'Var's, used to change the context of a 'Var'
-- when removing unused 'Var's.
-data UsedVars oldVS meta newVS a where
- UsedVarsZ :: UsedVars oldVS meta '[] a
+data UsedVars oldVS prov newVS a where
+ UsedVarsZ :: UsedVars oldVS prov '[] a
UsedVarsS ::
- Var meta oldVS (v :: vK) ->
- UsedVars oldVS meta newVS a ->
- UsedVars oldVS meta (Proxy (v :: vK) ': newVS) a
+ Var prov oldVS (v :: vK) ->
+ UsedVars oldVS prov newVS a ->
+ UsedVars oldVS prov (Proxy (v :: vK) ': newVS) a
instance LenVar (UsedVars oldVS) where
lenVar UsedVarsZ = LenZ
lenVar (UsedVarsS _v oldVS) = LenS $ lenVar oldVS
lookupUsedVars ::
- Var meta oldVS (v :: vK) ->
- UsedVars oldVS meta newVS a ->
- Maybe (Var meta newVS (v :: vK))
+ Var prov oldVS (v :: vK) ->
+ UsedVars oldVS prov newVS a ->
+ Maybe (Var prov newVS (v :: vK))
lookupUsedVars _v UsedVarsZ = Nothing
lookupUsedVars v (UsedVarsS v' us) = do
case v `eqTy` v' of
Just HRefl ->
case v' of
- Var{varKind, varMeta} ->
+ Var{varKind} ->
Just
VarZ
{ varZNext = lenVar us
, varZKind = varKind
- , varZMeta = varMeta
}
Nothing -> VarS Data.Functor.<$> lookupUsedVars v us
insertUsedVars ::
- Var meta vs v ->
- UsedVars vs meta us a ->
- Maybe (UsedVars vs meta (Proxy v ': us) a)
+ Var prov vs v ->
+ UsedVars vs prov us a ->
+ Maybe (UsedVars vs prov (Proxy v ': us) a)
insertUsedVars v vs =
case lookupUsedVars v vs of
Just{} -> Nothing
-- | Test whether a given 'Var' occurs within @(t)@.
class VarOccursIn (t :: Type -> [Type] -> aK -> Type) where
- varOccursIn :: Var meta vs v -> t meta vs a -> Bool
+ varOccursIn :: Var prov vs v -> t prov vs a -> Bool
-- * Class 'UsedVarsOf'
class UsedVarsOf t where
usedVarsOf ::
- UsedVars vs meta oldVS a ->
- t meta vs b ->
- (forall newVS. UsedVars vs meta newVS a -> ret) ->
+ UsedVars vs prov oldVS a ->
+ t prov vs b ->
+ (forall newVS. UsedVars vs prov newVS a -> ret) ->
ret
-- * Type 'Ty'
-- Use a CUSK, because it's a polymorphically recursive type,
-- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
-data Ty :: forall aK. Type -> [Type] -> aK -> Type where
- TyConst :: {tyConst :: Const meta a, tyConstLen :: Len vs} -> Ty meta vs a
- TyVar :: {tyVar :: Var meta vs a, tyVarName :: Name} -> Ty meta vs a
- TyApp :: {tyAppFun :: Ty meta vs f, tyAppArg :: Ty meta vs a} -> Ty meta vs (f a)
+data Ty :: forall aK. Prov -> [Type] -> aK -> Type where
+ TyConst :: {tyConst :: Const a, tyConstLen :: Len vs} -> Ty prov vs a
+ TyVar :: {tyVar :: Var prov vs a, tyVarName :: Name} -> Ty prov vs a
+ TyApp :: {tyAppFun :: Ty prov vs f, tyAppArg :: Ty prov vs a} -> Ty prov vs (f a)
+ TyProv :: {tyProv :: prov, tyUnProv :: Ty prov vs a} -> Ty prov vs a
infixl 9 `TyApp`
-tyOfTypeRep :: meta -> Len vs -> TypeRep a -> Ty meta vs a
-tyOfTypeRep meta len ty = case ty of
- App f x -> TyApp{tyAppFun = tyOfTypeRep meta len f, tyAppArg = tyOfTypeRep meta len x}
- constType -> TyConst{tyConst = Const{constType, constMeta = meta}, tyConstLen = len}
+tyOfTypeRep :: Len vs -> TypeRep a -> Ty prov vs a
+tyOfTypeRep len ty = case ty of
+ App f x -> TyApp{tyAppFun = tyOfTypeRep len f, tyAppArg = tyOfTypeRep len x}
+ constType -> TyConst{tyConst = constType, tyConstLen = len}
-- | Monomorphic 'Ty' from a 'Typeable'.
-monoTy :: forall {aK} (a :: aK) meta. Typeable a => Monoid meta => Ty meta '[] a
-monoTy = tyOfTypeRep mempty LenZ typeRep
-
-aTy :: LenInj vs => Monoid meta => Ty meta (Proxy a ': vs) (a :: Type)
-bTy :: LenInj vs => Monoid meta => Ty meta (Proxy a ': Proxy b ': vs) (b :: Type)
-cTy :: LenInj vs => Monoid meta => Ty meta (Proxy a : Proxy b : Proxy c : vs) (c :: Type)
-dTy :: LenInj vs => Monoid meta => Ty meta (Proxy a : Proxy b : Proxy c : Proxy d : vs) (d :: Type)
-aTy = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "a"}
-bTy = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "b"}
-cTy = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "c"}
-dTy = TyVar{tyVar = VarS $ VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "d"}
+monoTy :: forall {aK} (a :: aK) prov. Typeable a => Ty prov '[] a
+monoTy = tyOfTypeRep LenZ typeRep
+
+aTy :: LenInj vs => Monoid prov => Ty prov (Proxy a ': vs) (a :: Type)
+bTy :: LenInj vs => Monoid prov => Ty prov (Proxy a ': Proxy b ': vs) (b :: Type)
+cTy :: LenInj vs => Monoid prov => Ty prov (Proxy a : Proxy b : Proxy c : vs) (c :: Type)
+dTy :: LenInj vs => Monoid prov => Ty prov (Proxy a : Proxy b : Proxy c : Proxy d : vs) (d :: Type)
+aTy = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "a"}
+bTy = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "b"}
+cTy = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "c"}
+dTy = TyVar{tyVar = VarS $ VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "d"}
pattern FUN ::
-- CReq
- forall k (fun :: k) meta vs.
+ forall k (fun :: k) prov vs.
() =>
- {-Monoid meta-}
+ {-Monoid prov-}
-- CProv
forall
(r1 :: RuntimeRep)
-- , r1 ~ LiftedRep
-- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
) =>
- Ty meta vs arg ->
- Ty meta vs res ->
- Ty meta vs fun
+ Ty prov vs arg ->
+ Ty prov vs res ->
+ Ty prov vs fun
pattern FUN arg res <-
TyApp
{ tyAppFun =
TyApp
- { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
+ { tyAppFun = TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
, tyAppArg = arg
}
, tyAppArg = res
}
-(~>) :: Monoid meta => Ty meta vs a -> Ty meta vs b -> Ty meta vs (a -> b)
+(~>) :: Monoid prov => Ty prov vs a -> Ty prov vs b -> Ty prov vs (a -> b)
(~>) arg res =
TyApp
{ tyAppFun =
TyApp
{ tyAppFun =
- TyConst{tyConst = Const{constType = typeRep, constMeta = mempty}, tyConstLen = (lenVar arg)}
+ TyConst{tyConst = typeRep, tyConstLen = (lenVar arg)}
, tyAppArg = arg
}
, tyAppArg = res
}
infixr 0 ~>
-deriving instance Show meta => Show (Ty meta vs a)
+deriving instance Show prov => Show (Ty prov vs a)
-- type instance SourceOf (Ty vs src t) = src
instance LenVar Ty where
lenVar TyConst{tyConstLen} = tyConstLen
lenVar TyApp{tyAppFun} = lenVar tyAppFun
lenVar TyVar{tyVar} = lenVar tyVar
+ lenVar TyProv{tyUnProv} = lenVar tyUnProv
-- lenVars (TyFam l _f _as) = l
instance AllocVars Ty where
allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
+ allocVarsL len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsL len tyUnProv}
-- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
+ allocVarsR len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsR len tyUnProv}
-- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
+
instance VarOccursIn Ty where
varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
varOccursIn _v TyVar{} = False
varOccursIn _v TyConst{} = False
varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
+ varOccursIn v TyProv{..} = varOccursIn v tyUnProv
-- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
instance UsedVarsOf Ty where
case insertUsedVars v vs of
Nothing -> k vs
Just vs' -> k vs'
+ usedVarsOf vs TyProv{tyUnProv} k = usedVarsOf vs tyUnProv k
-- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
-- ** Type 'TyT'
-- | Existential for 'Type'.
-data TyT meta vs = forall a. TyT (Ty meta vs a)
+data TyT prov vs = forall a. TyT (Ty prov vs a)
-- type instance SourceOf (TyT vs src) = src
-instance Eq (TyT meta vs) where
+instance Eq (TyT prov vs) where
TyT x == TyT y = isJust $ eqTy x y
-instance Show meta => Show (TyT meta vs) where
+instance Show prov => Show (TyT prov vs) where
showsPrec p (TyT x) = showsPrec p x
-- * Type 'Kind'
-type Kind meta a = Ty meta '[] a
+type Kind prov a = Ty prov '[] a
-- ** Type 'KindK'
-type KindK meta = TyT meta '[]
+type KindK prov = TyT prov '[]
-- ** Type 'TyVT'
-data TyVT meta = forall vs a. TyVT (Ty meta vs a)
+data TyVT prov = forall vs a. TyVT (Ty prov vs a)
-deriving instance Show meta => Show (TyVT meta)
+deriving instance Show prov => Show (TyVT prov)
instance Eq (TyVT m) where
TyVT x == TyVT y = isJust (eqTy x' y')
where
-- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
-- eqTy x y = eqTy (unSourced x) (unSourced y)
-instance EqTy (Ty meta vs) (Ty meta vs) where
+instance EqTy (Ty prov vs) (Ty prov vs) where
eqTy = go
where
- go :: forall xK xT yK yT. Ty meta vs (xT :: xK) -> Ty meta vs (yT :: yK) -> Maybe (xT :~~: yT)
+ go :: forall xK xT yK yT. Ty prov vs (xT :: xK) -> Ty prov vs (yT :: yK) -> Maybe (xT :~~: yT)
go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
| Just HRefl <- go xF yF
, Just HRefl <- go xA yA =
Just HRefl
+ go TyProv{tyUnProv = x} y = go x y
+ go x TyProv{tyUnProv = y} = go x y
go _x _y = Nothing
-- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
-- eqTy x y@TyFam{} = eqTy x (expandFam y)
-- * Type 'Tys'
-data Tys (as :: [Type]) meta vs (a :: aK) where
- TysZ :: Tys '[] meta vs a
- TysS :: Ty meta vs a -> Tys as meta vs b -> Tys (Proxy a ': as) meta vs b
+data Tys (as :: [Type]) prov vs (a :: aK) where
+ TysZ :: Tys '[] prov vs a
+ TysS :: Ty prov vs a -> Tys as prov vs b -> Tys (Proxy a ': as) prov vs b
infixr 5 `TysS`
-- type instance SourceOf (Tys vs src ts) = src
--- instance ConstsOf (Tys meta vs ts) where
+-- instance ConstsOf (Tys prov vs ts) where
-- constsOf TysZ = Set.empty
-- constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
instance UsedVarsOf (Tys as) where
-- go TyFam{} = Nothing
proj_ConstKi ::
- forall kc (c :: kc) u meta.
+ forall kc (c :: kc) u.
Typeable c =>
-- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
-- KindInjP (Ty_of_Type kc) =>
- Const meta u ->
+ Const u ->
Maybe (c :~~: u)
-proj_ConstKi = eqTypeRep (typeRep @c) . constType
+proj_ConstKi = eqTypeRep (typeRep @c)
-- ** Type @(#>)@
newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
-- | Qualify a 'Type'.
-(#>) :: Monoid meta => Ty meta vs q -> Ty meta vs t -> Ty meta vs (q #> t)
+(#>) :: Monoid prov => Ty prov vs q -> Ty prov vs t -> Ty prov vs (q #> t)
(#>) q t =
-- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
TyApp
{ tyAppFun =
TyApp
- { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#>), constMeta = mempty}, tyConstLen = lenVar q}
+ { tyAppFun = TyConst{tyConst = typeRep @(#>), tyConstLen = lenVar q}
, tyAppArg = q
}
, tyAppArg = t
instance ((x, y) :: Constraint) => x # y
-- | Unify two 'K.Constraint's.
-(#) :: Monoid meta => Ty meta vs qx -> Ty meta vs qy -> Ty meta vs (qx # qy)
+(#) :: Monoid prov => Ty prov vs qx -> Ty prov vs qy -> Ty prov vs (qx # qy)
(#) a b =
-- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
TyApp
{ tyAppFun =
TyApp
- { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#), constMeta = mempty}, tyConstLen = lenVar a}
+ { tyAppFun = TyConst{tyConst = typeRep @(#), tyConstLen = lenVar a}
, tyAppArg = a
}
, tyAppArg = b
infixr 2 #
-- * Class 'KindOf'
-class KindOf (ty :: Type -> [Type] -> aK -> Type) where
+class KindOf (ty :: Prov -> [Type] -> aK -> Type) where
-- | Return the kind of the given 'Var'.
kindOf ::
-- HasCallStack =>
- Show meta =>
- ty meta vs (a :: aK) ->
- Kind meta (aK :: Type)
+ ProvenanceKindOf ty prov =>
+ Show prov =>
+ ty prov vs (a :: aK) ->
+ Kind prov (aK :: Type)
instance KindOf Var where
- kindOf Var{varKind} = varKind
+ kindOf v@Var{varKind} = TyProv (provenanceKindOf v) varKind
instance KindOf Ty where
- kindOf TyConst{tyConst = Const{..} :: Const meta (a :: aK)} =
- tyOfTypeRep constMeta LenZ (typeRepKind constType)
- kindOf TyApp{tyAppFun = f} = case kindOf f of
- TyApp
- { tyAppFun =
+ kindOf ty = TyProv (provenanceKindOf ty) (go ty)
+ where
+ go ::
+ Show prov =>
+ Ty prov vs (a :: aK) ->
+ Kind prov (aK :: Type)
+ go TyConst{tyConst = constType :: Const (a :: aK)} =
+ tyOfTypeRep LenZ (typeRepKind constType)
+ go TyApp{tyAppFun = f} = case go f of
TyApp
- { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
- }
- , tyAppArg = k
- } -> k
- t -> error $ "here: " <> show t
- kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind
+ { tyAppFun =
+ TyApp
+ { tyAppFun = TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
+ }
+ , tyAppArg = k
+ } -> k
+ t -> Prelude.error $ "here: " <> show t
+ go TyVar{..} = varKind tyVar
+ go TyProv{..} = go tyUnProv
+
+-- ** Class 'ProvenanceKindOf'
+class ProvenanceKindOf (ty :: Prov -> [Type] -> aK -> Type) prov where
+ provenanceKindOf :: ty prov vs (a :: aK) -> prov
+instance ProvenanceKindOf ty () where
+ provenanceKindOf _ = ()
+instance ProvenanceKindOf Ty String where
+ provenanceKindOf = show
+instance ProvenanceKindOf Var String where
+ provenanceKindOf = show
-- kindOf (TyFam _src _len fam _as) = kindOfConst fam
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
import Symantic.Parser.Error (ErrorInj (..))
import Symantic.Typer.Eq (EqTy (eqTy))
-import Symantic.Typer.Type (
- IndexVar,
- KindK,
- KindOf (kindOf),
- Ty (TyApp, TyConst, TyVar, tyConst, tyVar),
- TyT (..),
- TyVT (..),
- Tys (..),
- Var,
- VarOccursIn (..),
- indexVar,
- proj_ConstKi,
- type (#>),
- )
+import Symantic.Typer.Type
-- * Type 'Subst'
-- | /Type variable substitution/.
--
-- WARNING: a 'Subst' MUST be without loops, and fully expanded.
-newtype Subst meta vs
- = Subst (Map IndexVar (VT meta vs))
+newtype Subst prov vs
+ = Subst (Map IndexVar (VT prov vs))
-deriving instance (Show meta, Monoid meta) => Show (Subst meta vs)
-instance Monoid meta => Semigroup (Subst meta vs) where
+deriving instance (Show prov) => Show (Subst prov vs)
+instance Semigroup (Subst prov vs) where
(<>) = unionSubst
-instance Monoid meta => Monoid (Subst meta vs) where
+instance Monoid (Subst prov vs) where
mempty = Subst Map.empty
mappend = (<>)
-- so that, when using the resulting 'Subst',
-- there is no need to apply it multiple times
-- until there is no more substitution to be done.
-unionSubst :: Subst meta vs -> Subst meta vs -> Subst meta vs
+unionSubst :: Subst prov vs -> Subst prov vs -> Subst prov vs
unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) Data.Functor.<$> y)
-- * Type 'VT'
-- | A 'Var' and a 'Type' existentialized over their type index.
-data VT meta vs = forall t. VT (Var meta vs t) (Ty meta vs t)
+data VT prov vs = forall t. VT (Var prov vs t) (Ty prov vs t)
-deriving instance (Show meta, Monoid meta) => Show (VT meta vs)
+deriving instance (Show prov) => Show (VT prov vs)
-insertSubst :: Monoid meta => Var meta vs v -> Ty meta vs v -> Subst meta vs -> Subst meta vs
+insertSubst :: Var prov vs v -> Ty prov vs v -> Subst prov vs -> Subst prov vs
insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s
-lookupSubst :: Monoid meta => Var meta vs v -> Subst meta vs -> Maybe (Ty meta vs v)
+lookupSubst :: Var prov vs v -> Subst prov vs -> Maybe (Ty prov vs v)
lookupSubst v (Subst s)
| Just (VT v' t) <- Map.lookup (indexVar v) s
, Just HRefl <- v `eqTy` v' =
class Substable t where
-- | Like 'substVar', but without the /occurence check/.
substVarUnsafe ::
- Var meta vs v -> Ty meta vs v -> t meta vs a -> t meta vs a
+ Var prov vs v -> Ty prov vs v -> t prov vs a -> t prov vs a
-- | Substitute all the 'Var's which have a match in given 'Subst'.
subst ::
- Subst meta vs -> t meta vs a -> t meta vs a
+ Subst prov vs -> t prov vs a -> t prov vs a
instance Substable Ty where
substVarUnsafe _v _r t@TyConst{} = t
+ substVarUnsafe v r ty@TyProv{tyUnProv} =
+ ty{tyUnProv = substVarUnsafe v r tyUnProv}
substVarUnsafe v r (TyApp f a) =
TyApp
(substVarUnsafe v r f)
Just HRefl -> r
Nothing -> t
- -- substVarUnsafe v r (TyFam meta len fam as) =
- -- TyFam meta len fam $ substVarUnsafe v r as
+ -- substVarUnsafe v r (TyFam prov len fam as) =
+ -- TyFam prov len fam $ substVarUnsafe v r as
subst _s t@TyConst{} = t
+ subst s ty@TyProv{tyUnProv} = ty{tyUnProv = subst s tyUnProv}
subst s (TyApp f a) = TyApp (subst s f) (subst s a)
subst (Subst s) t@TyVar{tyVar = tv} =
case Map.lookup (indexVar tv) s of
Nothing -> Prelude.error "[BUG] subst: kind mismatch"
Just HRefl -> r
--- subst s (TyFam meta len fam as) = TyFam meta len fam $ subst s as
+-- subst s (TyFam prov len fam as) = TyFam prov len fam $ subst s as
instance Substable (Tys as) where
substVarUnsafe _v _r TysZ = TysZ
substVarUnsafe v r (TysS t ts) =
substVar ::
VarOccursIn t =>
Substable t =>
- Var meta vs v ->
- Ty meta vs v ->
- t meta vs a ->
- Maybe (t meta vs a)
+ Var prov vs v ->
+ Ty prov vs v ->
+ t prov vs a ->
+ Maybe (t prov vs a)
substVar v r t =
if v `varOccursIn` r
then Nothing -- NOTE: occurence check
-- ** Type 'ErrorUnify'
-- | Reasons why two 'Type's cannot be unified.
-data ErrorUnify meta
+data ErrorUnify prov
= -- | /occurence check/: a 'Var' is unified with a 'Type'
-- which contains this same 'Var'.
- ErrorUnifyVarLoop IndexVar (TyVT meta)
+ ErrorUnifyVarLoop IndexVar (TyVT prov)
| -- | Two 'TyConst's should be the same, but are different.
- ErrorUnifyConst (TyVT meta) (TyVT meta)
+ ErrorUnifyConst (TyVT prov) (TyVT prov)
| -- | Two 'Kind's should be the same, but are different.
- ErrorUnifyKind (KindK meta) (KindK meta) (TyVT meta) (TyVT meta)
+ ErrorUnifyKind (KindK prov) (KindK prov) (TyVT prov) (TyVT prov)
| -- | Cannot unify those two 'Type's.
- ErrorUnifyType (TyVT meta) (TyVT meta)
+ ErrorUnifyType (TyVT prov) (TyVT prov)
-deriving instance Monoid meta => Eq (ErrorUnify meta)
-deriving instance (Show meta, Monoid meta) => Show (ErrorUnify meta)
+deriving instance Eq (ErrorUnify prov)
+deriving instance (Show prov) => Show (ErrorUnify prov)
-instance ErrorInj (ErrorUnify meta) (ErrorUnify meta) where
+instance ErrorInj (ErrorUnify prov) (ErrorUnify prov) where
errorInj = id
-data SourceTypeArg meta
- = SourceTypeArg (TyVT meta)
+data SourceTypeArg prov
+ = SourceTypeArg (TyVT prov)
-- | Return the left spine of a 'Ty':
-- the root 'Ty' and its 'Ty' parameters,
-- from the left to the right.
spineTy ::
- forall meta vs t.
- -- MC.MonadWriter (SourceTypeArg meta) (Sourced meta) =>
- Ty meta vs t ->
- (TyT meta vs, [TyT meta vs])
+ forall prov vs t.
+ -- MC.MonadWriter (SourceTypeArg prov) (Sourced prov) =>
+ Ty prov vs t ->
+ (TyT prov vs, [TyT prov vs])
spineTy = go []
where
- go :: forall kx (x :: kx). [TyT meta vs] -> Ty meta vs x -> (TyT meta vs, [TyT meta vs])
+ go :: forall kx (x :: kx). [TyT prov vs] -> Ty prov vs x -> (TyT prov vs, [TyT prov vs])
-- Skip the constraint @q@.
go ctx (TyApp (TyApp (TyConst{tyConst = c}) _q) t)
| Just HRefl <- proj_ConstKi @_ @(#>) c =
-- | Return the /most general unification/ of two 'Type's, when it exists.
unifyType ::
- forall xyK (x :: xyK) (y :: xyK) vs meta.
- Monoid meta =>
- Show meta =>
- Subst meta vs ->
- Ty meta vs (x :: xyK) ->
- Ty meta vs (y :: xyK) ->
- Either (ErrorUnify meta) (Subst meta vs)
+ forall xyK (x :: xyK) (y :: xyK) vs prov.
+ (forall k. ProvenanceKindOf (Ty @k) prov) =>
+ (forall k. ProvenanceKindOf (Var @k) prov) =>
+ Show prov =>
+ Subst prov vs ->
+ Ty prov vs (x :: xyK) ->
+ Ty prov vs (y :: xyK) ->
+ Either (ErrorUnify prov) (Subst prov vs)
unifyType vs x y =
case (spineTy x, spineTy y) of
((TyT xRootTy, px), (TyT yRootTy, py)) ->
xK = kindOf x
goVar ::
forall k (a :: k) (b :: k) ws.
- Subst meta ws ->
- Var meta ws a ->
- Ty meta ws b ->
- Either (ErrorUnify meta) (Subst meta ws)
+ (forall k'. ProvenanceKindOf (Ty @k') prov) =>
+ (forall k'. ProvenanceKindOf (Var @k') prov) =>
+ Show prov =>
+ Subst prov ws ->
+ Var prov ws a ->
+ Ty prov ws b ->
+ Either (ErrorUnify prov) (Subst prov ws)
goVar sub va b =
case va `lookupSubst` sub of
Just a -> unifyType sub b a
Right $ insertSubst va b' mempty <> sub
goZip ::
forall ws.
- Subst meta ws ->
- [TyT meta ws] ->
- [TyT meta ws] ->
- Either (ErrorUnify meta) (Subst meta ws)
+ Subst prov ws ->
+ [TyT prov ws] ->
+ [TyT prov ws] ->
+ Either (ErrorUnify prov) (Subst prov ws)
goZip sub [] [] = Right sub
goZip sub (TyT a : as) (TyT b : bs) =
case aK `eqTy` bK of
ghc-options:
-Wall -Wincomplete-record-updates -Wincomplete-uni-patterns
-Wmonomorphism-restriction -Wpartial-fields
- -fprint-potential-instances
-
--- -fprint-explicit-kinds
+ -fprint-potential-instances -fprint-explicit-kinds
-- -dshow-passes
-- -ddump-to-file
sourcephile / git / tmp / julm / symantic.git / commitdiff