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)