bergamot-elm/src/Bergamot/Rules.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)

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)

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)

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 }))

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))

provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
provePremises l =
    case l of
        t :: ts ->
            pure (::)
            |> apply (prove t)
            |> apply (provePremises ts)
        [] -> pure []

prove : Term Metavariable -> Prover ProofTree
prove mt =
    pure (\t env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
    |> apply (liftInstantiation instantiate mt)
    |> apply getEnv
    |> join

single : RuleEnv -> Prover a -> Maybe a
single env p =
    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState }
    |> Search.one
    |> Maybe.map (Tuple.first << Tuple.first)