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

Unify conclusion before instantiating premises to save some time

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-01 23:40:29 -08:00
parent 12fa4dc1fd
commit 1fca9171b1
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Bergamot/Rules.elm
View File

@ -105,12 +105,12 @@ reifyProofTree (MkProofTree node) =
rule : Term UnificationVar -> Rule -> Prover ProofTree
rule t r =
withVars (pure Tuple.pair
|> apply (liftInstantiation instantiate r.conclusion)
|> apply (liftInstantiation instantiate r.conclusion
|> andThen (\conc -> liftUnification unify t conc))
|> apply (liftInstantiation instantiateList r.premises))
|> andThen (\(conc, prems) ->
pure (\tp trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees })
|> apply (liftUnification unify t conc)
|> apply (provePremises prems))
provePremises prems)
|> map (\trees -> MkProofTree { name = r.name, conclusion = t, premises = trees })
collectStrings : Term UnificationVar -> Prover (List String)
collectStrings t =