Add support for reifying proof trees

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-11-26 13:14:44 -08:00
parent a24fbad249
commit e123f24af0
2 changed files with 22 additions and 9 deletions

View File

@ -1,6 +1,6 @@
module Bergamot.Rules exposing (..) module Bergamot.Rules exposing (..)
import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState) import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
import Bergamot.Search as Search exposing (Search) import Bergamot.Search as Search exposing (Search)
import Debug import Debug
@ -44,6 +44,15 @@ map f p env ps =
p env ps p env ps
|> Search.map (Tuple.mapFirst f) |> Search.map (Tuple.mapFirst f)
mapM : (a -> Prover b) -> List a -> Prover (List b)
mapM f l =
case l of
x :: xs ->
pure (::)
|> apply (f x)
|> apply (mapM f xs)
[] -> pure []
interleave : Prover a -> Prover a -> Prover a interleave : Prover a -> Prover a -> Prover a
interleave p1 p2 env ps = interleave p1 p2 env ps =
Search.interleave (p1 env ps) (p2 env ps) Search.interleave (p1 env ps) (p2 env ps)
@ -57,6 +66,9 @@ fail env ps = Search.fail
getEnv : Prover RuleEnv getEnv : Prover RuleEnv
getEnv env ps = Search.pure (env, ps) getEnv env ps = Search.pure (env, ps)
getUnificationState : Prover UnificationState
getUnificationState env ps = Search.pure (ps.unificationState, ps)
liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
liftInstantiation f a env ps = liftInstantiation f a env ps =
let let
@ -75,6 +87,13 @@ withVars p env ps =
p env ps p env ps
|> Search.map (Tuple.mapSecond (\psp -> { psp | instantiationState = resetVars psp.instantiationState })) |> Search.map (Tuple.mapSecond (\psp -> { psp | instantiationState = resetVars psp.instantiationState }))
reifyProofTree : ProofTree -> Prover ProofTree
reifyProofTree (MkProofTree node) =
pure (\t trees -> MkProofTree { node | conclusion = t, premises = trees })
|> apply (map (reify node.conclusion) getUnificationState)
|> apply (mapM reifyProofTree node.premises)
rule : Term UnificationVar -> Rule -> Prover ProofTree rule : Term UnificationVar -> Rule -> Prover ProofTree
rule t r = rule t r =
withVars (pure Tuple.pair withVars (pure Tuple.pair
@ -86,13 +105,7 @@ rule t r =
|> apply (provePremises prems)) |> apply (provePremises prems))
provePremises : List (Term UnificationVar) -> Prover (List ProofTree) provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
provePremises l = provePremises = mapM proveTerm
case l of
t :: ts ->
pure (::)
|> apply (proveTerm t)
|> apply (provePremises ts)
[] -> pure []
proveTerm : Term UnificationVar -> Prover ProofTree proveTerm : Term UnificationVar -> Prover ProofTree
proveTerm t = proveTerm t =

View File

@ -27,7 +27,7 @@ init () = ({ program = "", query = "" }, Cmd.none)
proveQuery : String -> String -> Maybe ProofTree proveQuery : String -> String -> Maybe ProofTree
proveQuery progs querys = proveQuery progs querys =
case (run program progs, run term querys) of case (run program progs, run term querys) of
(Just prog, Just query) -> single prog (prove query) (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing _ -> Nothing
view : Model -> Html Msg view : Model -> Html Msg