From: Julien Moutinho 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