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

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