From bc83f0ed532ddca435154dd496c97c70fadd5bcc Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 22 Dec 2023 21:59:41 -0800 Subject: [PATCH] Add bidirectional inference for `int(?x)` and `str(?x)`. Signed-off-by: Danila Fedorin --- src/Bergamot/Rules.elm | 82 ++++++++++++++++++++++++----------------- src/Bergamot/Search.elm | 5 ++- 2 files changed, 52 insertions(+), 35 deletions(-) diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm index 7bd971e..4f0b7de 100644 --- a/src/Bergamot/Rules.elm +++ b/src/Bergamot/Rules.elm @@ -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 diff --git a/src/Bergamot/Search.elm b/src/Bergamot/Search.elm index db90203..69f19a9 100644 --- a/src/Bergamot/Search.elm +++ b/src/Bergamot/Search.elm @@ -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