Tweak builtin rules to handle floats and more

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-26 13:08:24 -08:00
parent 4c12fee4aa
commit b828c73e43

View File

@ -158,6 +158,15 @@ builtinRules t =
Call "int" [Var output] ->
let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
in rec 0
Call "float" [FloatLit f] ->
MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] }
|> pure
Call "float" [Var output] ->
let rec f = interleave (suggest "BuiltinFloat" (FloatLit f) output) (lazy <| \_ -> rec (f+1))
in rec 0
Call "num" [tp] ->
interleave (builtinRules (Call "int" [tp])) (builtinRules (Call "float" [tp]))
|> map (\prem -> MkProofTree { name = "BuiltinNum", conclusion = t, premises = [prem] })
Call "str" [StringLit s] ->
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|> pure
@ -171,12 +180,15 @@ builtinRules t =
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 = []})
Call "tostring" [Call s [], Var output] ->
liftUnification unify (Var output) (StringLit <| encodeStr s)
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
Call "tostring" [tp, Var output] ->
let
suggestStr s = suggest "BuiltinToString" (StringLit s) output
in
case tp of
IntLit i -> suggestStr (String.fromInt i)
FloatLit f -> suggestStr (String.fromFloat f)
Call s [] -> suggestStr (encodeStr s)
_ -> fail
Call "escapestring" [StringLit s, Var output] ->
liftUnification unify (Var output) (StringLit (encodeStr s))
|> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})