init

diff --git a/src/Symantic/Compiler/Term.hs b/src/Symantic/Compiler/Term.hs
index 75baae939cec157289e5f4caaba182df80deb168..1575f6a3a868a72ae8372f67db73ed73a7a393f1 100644 (file)
--- 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
   -- 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)
 instance
   ( forall sem. Syntaxes syns sem => Unabstractable sem
   , Syntaxes syns (Forall syns)


@@ -103,14 +104,14 @@ instance
   (.@) = appOpenTerm
 
 appOpenTerm ::
   (.@) = 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)
   ) =>
   ( 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)
 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 7b491bbef2cbfd95760bfeb4e6eec8d107fa9b5a..a579cff7e09918483a7a618ab1e15556ae456315 100644 (file)
--- 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
     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
       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)
       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
       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 $
             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 ->
     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
     TokenTermAtom "($)" -> Parser $ \_ctx ->
       Right $ TermVT ((aTy ~> bTy @'[]) ~> aTy ~> bTy) $ E (Sym.$)
     tok -> next tok