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

Add bidirectional inference for `int(?x)` and `str(?x)`. 

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-22 21:59:41 -08:00
parent 12d823e944
commit bc83f0ed53
2 changed files with 52 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

82
src/Bergamot/Rules.elm
View File

@ -67,6 +67,9 @@ interleave p1 p2 env ps =
pure : a -> Prover a
pure a env ps = Search.pure (a, ps)
lazy : (() -> Prover a) -> Prover a
lazy f env ps = Search.lazy ((\p -> p env ps) << f)
fail : Prover a
fail env ps = Search.fail
@ -129,40 +132,51 @@ collectStrings t =
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 (\_ -> 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 "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 = []})
Call "tostring" [Call s [], Var output] ->
liftUnification unify (Var output) (StringLit <| encodeStr s)
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
Call "escapestring" [StringLit s, Var output] ->
liftUnification unify (Var output) (StringLit (encodeStr s))
|> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})
Call "latexifystring" [StringLit s, Var output] ->
liftUnification unify (Var output) (StringLit (encodeLatex s))
|> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
_ -> fail
let
suggest r v output =
liftUnification unify (Var output) v
|> map (\_ -> MkProofTree { name = r, conclusion = t, premises = [] })
in
case t of
Call "concat" [StringLit s1, StringLit s2, Var output] ->
liftUnification unify (Var output) (StringLit (s1 ++ s2))
|> 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 "int" [Var output] ->
let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
in rec 0
Call "str" [StringLit s] ->
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|> pure
Call "str" [Var output] ->
List.foldr (\s -> interleave (suggest "BuiltinStr" (StringLit s) output)) fail
<| String.split "" "abcdefghijklmnopqrstuvwxyz"
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 = []})
Call "tostring" [Call s [], Var output] ->
liftUnification unify (Var output) (StringLit <| encodeStr s)
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
Call "escapestring" [StringLit s, Var output] ->
liftUnification unify (Var output) (StringLit (encodeStr s))
|> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})
Call "latexifystring" [StringLit s, Var output] ->
liftUnification unify (Var output) (StringLit (encodeLatex s))
|> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
_ -> fail
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
provePremises = mapM proveTerm

5
src/Bergamot/Search.elm
View File

@ -1,4 +1,4 @@
module Bergamot.Search exposing (Search, map, apply, andThen, pure, fail, yield, interleave, one)
module Bergamot.Search exposing (Search, map, apply, andThen, pure, lazy, fail, yield, interleave, one)
type SearchStep a
= Empty
@ -31,6 +31,9 @@ andThen f sa () =
pure : a -> Search a
pure a () = Found a (\() -> Empty)
lazy : (() -> Search a) -> Search a
lazy f () = f () ()
fail : Search a
fail () = Empty