1
0
forked from GitHub/gf-core

the compiler now compiles with the new runtime

This commit is contained in:
krangelov
2021-09-13 18:32:57 +02:00
parent c5ce2fd4b7
commit cf7673525f
26 changed files with 765 additions and 105 deletions

View File

@@ -11,7 +11,7 @@ module PGF2.Expr(Var, Cat, Fun,
mkFloat, unFloat,
mkMeta, unMeta,
exprSize, exprFunctions,
exprSize, exprFunctions, exprSubstitute,
mkType, unType,
mkHypo, mkDepHypo, mkImplHypo
@@ -169,6 +169,15 @@ exprFunctions (EImplArg e) = exprFunctions e
exprFunctions (EFun f) = [f]
exprFunctions _ = []
exprSubstitute :: Expr -> [Expr] -> Expr
exprSubstitute (EAbs bt x e) vs = EAbs bt x (exprSubstitute e vs)
exprSubstitute (EApp e1 e2) vs = EApp (exprSubstitute e1 vs) (exprSubstitute e2 vs)
exprSubstitute (EMeta i) vs = vs !! i
exprSubstitute (ETyped e ty) vs = ETyped (exprSubstitute e vs) ty
exprSubstitute (EImplArg e) vs = EImplArg (exprSubstitute e vs)
exprSubstitute e vs = e
-- | creates a type from list of hypothesises, category and
-- list of arguments for the category. The operation
-- @mkType [h_1,...,h_n] C [e_1,...,e_m]@ will create