88 lines
2.5 KiB
Elm
88 lines
2.5 KiB
Elm
module Bergamot.Rules exposing (..)
|
|
|
|
import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState)
|
|
import Bergamot.Search as Search exposing (Search)
|
|
|
|
import Debug
|
|
|
|
type alias Rule =
|
|
{ name : String
|
|
, conclusion : Term Metavariable
|
|
, premises : List (Term Metavariable)
|
|
}
|
|
|
|
type ProofTree = MkProofTree
|
|
{ name : String
|
|
, conclusion : Term UnificationVar
|
|
, premises : List ProofTree
|
|
}
|
|
|
|
type alias RuleEnv =
|
|
{ rules : List Rule
|
|
}
|
|
|
|
type alias ProveState =
|
|
{ unificationState : UnificationState
|
|
, instantiationState : InstantiationState
|
|
}
|
|
|
|
type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
|
|
|
|
andThen : (a -> Prover b) -> Prover a -> Prover b
|
|
andThen f p env ps =
|
|
p env ps
|
|
|> Search.andThen (\(a, psp) -> (f a) env psp)
|
|
|
|
map : (a -> b) -> Prover a -> Prover b
|
|
map f p env ps =
|
|
p env ps
|
|
|> Search.map (Tuple.mapFirst f)
|
|
|
|
interleave : Prover a -> Prover a -> Prover a
|
|
interleave p1 p2 env ps =
|
|
Search.interleave (p1 env ps) (p2 env ps)
|
|
|
|
pure : a -> Prover a
|
|
pure a env ps = Search.pure (a, ps)
|
|
|
|
fail : Prover a
|
|
fail env ps = Search.fail
|
|
|
|
getEnv : Prover RuleEnv
|
|
getEnv env ps = Search.pure (env, ps)
|
|
|
|
rule : Term UnificationVar -> Rule -> Prover ProofTree
|
|
rule t r env ps =
|
|
let
|
|
(conc, is) = instantiate r.conclusion ps.instantiationState
|
|
(prems, isp) = instantiateList r.premises is
|
|
in
|
|
case unify t conc ps.unificationState of
|
|
Nothing -> Search.fail
|
|
Just (tp, usp) ->
|
|
let
|
|
psp = { ps | instantiationState = resetVars isp
|
|
, unificationState = usp }
|
|
in
|
|
provePremises prems env psp
|
|
|> Search.map (Tuple.mapFirst (\trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees }))
|
|
|
|
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
|
provePremises l =
|
|
case l of
|
|
t :: ts ->
|
|
prove t
|
|
|> andThen (\tree -> map (\trees -> tree :: trees) (provePremises ts))
|
|
[] -> pure []
|
|
|
|
prove : Term UnificationVar -> Prover ProofTree
|
|
prove t =
|
|
getEnv
|
|
|> andThen (List.foldl (\r -> interleave (rule t r)) fail << .rules)
|
|
|
|
single : RuleEnv -> Prover a -> Maybe a
|
|
single env p =
|
|
p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState }
|
|
|> Search.one
|
|
|> Maybe.map (Tuple.first << Tuple.first)
|