From: Julien Moutinho <julm@sourcephile.fr>
Date: Thu, 14 Sep 2023 01:42:27 +0000 (+0200)
Subject: init
X-Git-Url: https://git.sourcephile.fr/tmp/julm/symantic.git/commitdiff_plain

init
---

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