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

Add a builtin rule for string concatenation

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-01 13:10:51 -08:00
parent 546265f2e6
commit e659172320
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/Bergamot/Rules.elm
View File

@ -1,6 +1,6 @@
module Bergamot.Rules exposing (..)
import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
import Bergamot.Syntax exposing (Term(..), Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
import Bergamot.Search as Search exposing (Search)
import Debug
@ -111,6 +111,14 @@ rule t r =
|> apply (liftUnification unify t conc)
|> apply (provePremises prems))
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 = []})
_ -> fail
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
provePremises = mapM proveTerm
@ -118,7 +126,7 @@ proveTerm : Term UnificationVar -> Prover ProofTree
proveTerm t =
burn
|> andThen (\() -> getEnv)
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) (builtinRules t) env.rules)
prove : Term Metavariable -> Prover ProofTree
prove mt =