141 lines
4.3 KiB
Elm
141 lines
4.3 KiB
Elm
module Bergamot.Rules exposing (..)
|
|
|
|
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
|
|
|
|
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
|
|
, gas: Int
|
|
}
|
|
|
|
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) -> if psp.gas > 0 then (f a) env psp else Search.fail)
|
|
|
|
join : Prover (Prover a) -> Prover a
|
|
join p = andThen (\x -> x) p
|
|
|
|
apply : Prover a -> Prover (a -> b) -> Prover b
|
|
apply pa pf = pf |> andThen (\f -> map f pa)
|
|
|
|
map : (a -> b) -> Prover a -> Prover b
|
|
map f p env ps =
|
|
p env ps
|
|
|> 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 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
|
|
|
|
yield : Prover a -> Prover a
|
|
yield p env ps = Search.yield (p env ps)
|
|
|
|
getEnv : Prover RuleEnv
|
|
getEnv env ps = Search.pure (env, ps)
|
|
|
|
getUnificationState : Prover UnificationState
|
|
getUnificationState env ps = Search.pure (ps.unificationState, ps)
|
|
|
|
burn : Prover ()
|
|
burn env ps = Search.pure ((), { ps | gas = ps.gas - 1})
|
|
|
|
liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
|
|
liftInstantiation f a env ps =
|
|
let
|
|
(b, is) = f a ps.instantiationState
|
|
in
|
|
Search.pure (b, { ps | instantiationState = is })
|
|
|
|
liftUnification : (a -> a -> UnificationState -> Maybe (a, UnificationState)) -> a -> a -> Prover a
|
|
liftUnification f a1 a2 env ps =
|
|
case f a1 a2 ps.unificationState of
|
|
Just (a, us) -> Search.pure (a, { ps | unificationState = us })
|
|
Nothing -> Search.fail
|
|
|
|
withVars : Prover a -> Prover a
|
|
withVars p env ps =
|
|
p env ps
|
|
|> 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 t r =
|
|
withVars (pure Tuple.pair
|
|
|> apply (liftInstantiation instantiate r.conclusion)
|
|
|> 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))
|
|
|
|
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
|
|
|
|
proveTerm : Term UnificationVar -> Prover ProofTree
|
|
proveTerm t =
|
|
burn
|
|
|> andThen (\() -> getEnv)
|
|
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) (builtinRules t) env.rules)
|
|
|
|
prove : Term Metavariable -> Prover ProofTree
|
|
prove mt =
|
|
liftInstantiation instantiate mt
|
|
|> andThen proveTerm
|
|
|
|
single : RuleEnv -> Prover a -> Maybe a
|
|
single env p =
|
|
p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
|
|
|> Search.one
|
|
|> Maybe.map (Tuple.first << Tuple.first)
|