Everything-I-Know-About-Types/bergamot-elm
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Implement more builtins

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-01 16:26:34 -08:00
parent faa65ff77b
commit f4619672a9
1 changed files with 26 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/Bergamot/Rules.elm
View File

@ -111,12 +111,32 @@ rule t r =
|> apply (liftUnification unify t conc)
|> apply (provePremises prems))
collectStrings : Term UnificationVar -> Prover (List String)
collectStrings t =
case t of
Call "cons" [StringLit s, rest] -> map (\ss -> s :: ss) <| collectStrings rest
Call "nil" [] -> pure []
_ -> fail
builtinRules : Term UnificationVar -> Prover ProofTree
builtinRules t =
case t of
Call "concat" [StringLit s1, StringLit s2, Var output] ->
liftUnification unify (Var output) (StringLit (s1 ++ s2))
|> map (\tp -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
|> map (\_ -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
Call "join" [tp, Var output] ->
collectStrings tp
|> andThen (\ss -> liftUnification unify (Var output) (StringLit (String.concat ss)))
|> map (\_ -> MkProofTree { name = "BuiltinJoin", conclusion = t, premises = []})
Call "int" [IntLit i] ->
MkProofTree { name = "BuiltinInt", conclusion = t, premises = [] }
|> pure
Call "str" [StringLit s] ->
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|> pure
Call "tostring" [IntLit i, Var output] ->
liftUnification unify (Var output) (StringLit (String.fromInt i))
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
_ -> fail
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
@ -124,9 +144,11 @@ provePremises = mapM proveTerm
proveTerm : Term UnificationVar -> Prover ProofTree
proveTerm t =
burn
|> andThen (\() -> getEnv)
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) (builtinRules t) env.rules)
map (reify t) getUnificationState
|> andThen (\tp ->
burn
|> andThen (\() -> getEnv)
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp) env.rules))
prove : Term Metavariable -> Prover ProofTree
prove mt =