232 lines
8.7 KiB
Elm
232 lines
8.7 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 Bergamot.Utils exposing (encodeStr, encodeLatex)
|
|
|
|
import Debug
|
|
|
|
type alias Rule =
|
|
{ name : String
|
|
, conclusion : Term Metavariable
|
|
, premises : List (Term Metavariable)
|
|
}
|
|
|
|
type alias Section =
|
|
{ name : String
|
|
, rules : List Rule
|
|
}
|
|
|
|
type ProofTree = MkProofTree
|
|
{ name : String
|
|
, conclusion : Term UnificationVar
|
|
, premises : List ProofTree
|
|
}
|
|
|
|
type alias RuleEnv =
|
|
{ sections : List Section
|
|
}
|
|
|
|
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) -> (f a) env psp)
|
|
|
|
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)
|
|
|
|
lazy : (() -> Prover a) -> Prover a
|
|
lazy f env ps = Search.lazy ((\p -> p env ps) << f)
|
|
|
|
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)
|
|
|
|
getRules : Prover (List Rule)
|
|
getRules env ps = Search.pure (List.concatMap (.rules) env.sections, ps)
|
|
|
|
getUnificationState : Prover UnificationState
|
|
getUnificationState env ps = Search.pure (ps.unificationState, ps)
|
|
|
|
burn : Prover a -> Prover a
|
|
burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail
|
|
|
|
try : Prover a -> Prover (Maybe a)
|
|
try p env ps =
|
|
p env { ps | gas = 30 }
|
|
|> Search.one
|
|
|> Maybe.map (Tuple.first << Tuple.first)
|
|
|> (\mx -> Search.pure (mx, ps))
|
|
|
|
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
|
|
|> andThen (\conc -> liftUnification unify t conc))
|
|
|> apply (liftInstantiation instantiateList r.premises))
|
|
|> andThen (\(conc, prems) ->
|
|
provePremises prems)
|
|
|> map (\trees -> MkProofTree { name = r.name, conclusion = t, premises = trees })
|
|
|
|
collectStrings : Term UnificationVar -> Prover (List String)
|
|
collectStrings t =
|
|
case t of
|
|
Call "cons" [StringLit s, rest] -> map (\ss -> s :: ss) <| collectStrings rest
|
|
Call "nil" [] -> pure []
|
|
_ -> fail
|
|
|
|
builtinRules : Term UnificationVar -> Prover ProofTree
|
|
builtinRules t =
|
|
let
|
|
suggest r v output =
|
|
liftUnification unify (Var output) v
|
|
|> map (\_ -> MkProofTree { name = r, conclusion = t, premises = [] })
|
|
in
|
|
case t of
|
|
Call "concat" [StringLit s1, StringLit s2, Var output] ->
|
|
liftUnification unify (Var output) (StringLit (s1 ++ s2))
|
|
|> map (\_ -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
|
|
Call "join" [tp, Var output] ->
|
|
collectStrings tp
|
|
|> andThen (\ss -> liftUnification unify (Var output) (StringLit (String.concat ss)))
|
|
|> map (\_ -> MkProofTree { name = "BuiltinJoin", conclusion = t, premises = []})
|
|
Call "int" [IntLit i] ->
|
|
MkProofTree { name = "BuiltinInt", conclusion = t, premises = [] }
|
|
|> pure
|
|
Call "int" [Var output] ->
|
|
let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
|
|
in rec 0
|
|
Call "float" [FloatLit f] ->
|
|
MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] }
|
|
|> pure
|
|
Call "float" [Var output] ->
|
|
let rec f = interleave (suggest "BuiltinFloat" (FloatLit f) output) (lazy <| \_ -> rec (f+1))
|
|
in rec 0
|
|
Call "num" [tp] ->
|
|
interleave (builtinRules (Call "int" [tp])) (builtinRules (Call "float" [tp]))
|
|
|> map (\prem -> MkProofTree { name = "BuiltinNum", conclusion = t, premises = [prem] })
|
|
Call "str" [StringLit s] ->
|
|
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|
|
|> pure
|
|
Call "str" [Var output] ->
|
|
List.foldr (\s -> interleave (suggest "BuiltinStr" (StringLit s) output)) fail
|
|
<| String.split "" "abcdefghijklmnopqrstuvwxyz"
|
|
Call "sym" [Call s []] ->
|
|
MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
|
|
|> pure
|
|
Call "call" [Call s ts, Var name, Var args] ->
|
|
pure (\_ _ -> MkProofTree { name = "BuiltinCall", conclusion = t, premises = [] })
|
|
|> apply (liftUnification unify (Var name) (StringLit <| encodeStr s))
|
|
|> apply (liftUnification unify (Var args) (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []) ts))
|
|
Call "tostring" [tp, Var output] ->
|
|
let
|
|
suggestStr s = suggest "BuiltinToString" (StringLit s) output
|
|
in
|
|
case tp of
|
|
IntLit i -> suggestStr (String.fromInt i)
|
|
FloatLit f -> suggestStr (String.fromFloat f)
|
|
Call s [] -> suggestStr (encodeStr s)
|
|
_ -> fail
|
|
Call "escapestring" [StringLit s, Var output] ->
|
|
liftUnification unify (Var output) (StringLit (encodeStr s))
|
|
|> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})
|
|
Call "latexifystring" [StringLit s, Var output] ->
|
|
liftUnification unify (Var output) (StringLit (encodeLatex s))
|
|
|> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
|
|
Call "not" [tp] ->
|
|
try (proveTerm tp)
|
|
|> andThen (\mp ->
|
|
case mp of
|
|
Nothing -> pure <| MkProofTree { name = "BuiltinNot", conclusion = t, premises = [] }
|
|
Just _ -> fail)
|
|
Call "symeq" [Call s1 [], Call s2 []] ->
|
|
if s1 == s2
|
|
then pure <| MkProofTree { name = "BuiltinSymEq", conclusion = t, premises = [] }
|
|
else fail
|
|
_ -> fail
|
|
|
|
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
|
provePremises = mapM proveTerm
|
|
|
|
proveTerm : Term UnificationVar -> Prover ProofTree
|
|
proveTerm t =
|
|
getUnificationState
|
|
|> map (\us -> reify t us)
|
|
|> andThen (\tp ->
|
|
burn (
|
|
getRules
|
|
|> andThen (List.foldr (\r -> interleave ((rule tp r))) (builtinRules tp))))
|
|
|
|
prove : Term Metavariable -> Prover ProofTree
|
|
prove mt =
|
|
withVars (liftInstantiation instantiate mt)
|
|
|> andThen proveTerm
|
|
|
|
single : RuleEnv -> Prover a -> Maybe a
|
|
single env p =
|
|
p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 15 }
|
|
|> Search.one
|
|
|> Maybe.map (Tuple.first << Tuple.first)
|