Add a 'call' primitive

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-01 18:15:32 -08:00
parent 905b760dd7
commit 549527d0cc

View File

@ -138,6 +138,10 @@ builtinRules t =
Call "sym" [Call s []] ->
MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
|> pure
Call "call" [Call s ts, Var name, Var args] ->
pure (\_ _ -> MkProofTree { name = "BuiltinCall", conclusion = t, premises = [] })
|> apply (liftUnification unify (Var name) (StringLit <| encodeStr s))
|> apply (liftUnification unify (Var args) (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []) ts))
Call "tostring" [IntLit i, Var output] ->
liftUnification unify (Var output) (StringLit (String.fromInt i))
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})