From cec02939dff40fa51e57e743ab9cf014be88ee57 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Thu, 14 Sep 2023 03:42:27 +0200
Subject: [PATCH] init
---
src/Symantic/Compiler/Term.hs | 23 ++++++++++++-----------
src/Symantic/Syntaxes.hs | 6 ++++--
2 files changed, 16 insertions(+), 13 deletions(-)
diff --git a/src/Symantic/Compiler/Term.hs b/src/Symantic/Compiler/Term.hs
index 75baae9..1575f6a 100644
--- a/src/Symantic/Compiler/Term.hs
+++ b/src/Symantic/Compiler/Term.hs
@@ -64,13 +64,14 @@ data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
-- 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 (Ty prov '[]) sem
- , Syntaxes syns (Forall syns)
- ) =>
- AbstractableTy (Ty prov '[]) (OpenTerm syns '[])
- where
- lamTy aTy f = E (lamTy aTy (unE Fun.. f Fun.. E))
+
+-- instance
+-- ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
+-- , Syntaxes syns (Forall syns)
+-- ) =>
+-- AbstractableTy (Ty prov '[]) (OpenTerm syns '[])
+-- where
+-- lamTy aTy f = E (lamTy aTy (unE Fun.. f Fun.. E))
instance
( forall sem. Syntaxes syns sem => Unabstractable sem
, Syntaxes syns (Forall syns)
@@ -103,14 +104,14 @@ instance
(.@) = appOpenTerm
appOpenTerm ::
- forall syns as a b.
+ forall syns vs a b.
( forall sem. Syntaxes syns sem => Unabstractable sem
, forall sem. Syntaxes syns sem => Instantiable sem
, Syntaxes syns (Forall syns)
) =>
- OpenTerm syns as (a -> b) ->
- OpenTerm syns as a ->
- OpenTerm syns as b
+ OpenTerm syns vs (a -> b) ->
+ OpenTerm syns vs a ->
+ OpenTerm syns vs b
E d `appOpenTerm` N e = N (E ((Sym..) .@ d) `appOpenTerm` e)
E d `appOpenTerm` V = N (E d)
E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
diff --git a/src/Symantic/Syntaxes.hs b/src/Symantic/Syntaxes.hs
index 7b491bb..a579cff 100644
--- a/src/Symantic/Syntaxes.hs
+++ b/src/Symantic/Syntaxes.hs
@@ -135,7 +135,9 @@ instance
where
go :: forall vs. CtxTy prov vs Void -> Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov vs)
go CtxTyZ = Left $ perSyntax $ ErrorParserAbstractableUnknown varName
+ -- Introduce 'V'
go (CtxTyS n ty _) | n == varName = Right $ TermVT ty V
+ -- Introduce 'W'
go (CtxTyS _n _typ tys) = do
TermVT ty ot <- go tys
Right $ TermVT ty (W ot)
@@ -144,7 +146,7 @@ instance
case eqTy (monoTy @Type @prov) (kindOf argTy) of
Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT argTy)
Just HRefl -> do
- TermVT resTy (res :: OpenTerm syn bVS res) <-
+ TermVT resTy (res :: OpenTerm syn resVS res) <-
unParser (final bT) (CtxTyS argName argTy ctx)
let argTy' = allocVarsR (lenVar resTy) argTy
Right $
@@ -194,7 +196,7 @@ instance
TokenTermAtom "(.)" -> Parser $ \_ctx ->
Right $ TermVT ((bTy ~> cTy @'[]) ~> (aTy ~> bTy) ~> aTy ~> cTy) $ E (Sym..)
TokenTermAtom "flip" -> Parser $ \_ctx ->
- Right $ TermVT ((aTy ~> bTy ~> cTy @'[]) ~> bTy ~> aTy ~> cTy) $ E (Sym.flip)
+ Right $ TermVT ((aTy ~> bTy ~> cTy @'[]) ~> bTy ~> aTy ~> cTy) $ E Sym.flip
TokenTermAtom "($)" -> Parser $ \_ctx ->
Right $ TermVT ((aTy ~> bTy @'[]) ~> aTy ~> bTy) $ E (Sym.$)
tok -> next tok
--
2.47.2