module Language.Bergamot.Rules where

import Prelude

import Language.Bergamot.Syntax (Expr)

import Control.Monad.State.Trans (runStateT)
import Control.Monad.State.Class (class MonadState, gets, modify)
import Control.Monad.Unify.Class (class MonadUnify, fresh)
import Data.List (List)
import Data.Traversable (class Traversable, traverse)
import Data.Foldable (class Foldable)
import Data.Map (Map, lookup, insert)
import Data.Map as Map
import Data.Tuple (fst)
import Data.Newtype (class Newtype)
import Data.Maybe (Maybe(..))

newtype Rule k = MkRule { name :: String, head :: Expr k, tail :: List (Expr k) }
derive instance Newtype (Rule k) _
derive instance Functor Rule
derive instance Foldable Rule
derive instance Traversable Rule

type Metavariable = String
type Metavariables k = Map Metavariable k

newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree k) }

metavariable :: forall k f m. MonadState (Metavariables k) m => MonadUnify k f m => Metavariable -> m k
metavariable s = do
    r <- gets (lookup s)
    case r of
        Just v -> pure v
        Nothing -> do
           v <- fresh
           modify (insert s v) *> pure v

-- note: unification expression ef not the same as functor-to-instantiate f, this way we can instantiate
-- things that contain expression etc.
instantiate :: forall k f ef m. Traversable f => MonadUnify k ef m => f Metavariable -> m (f k)
instantiate f = map fst $ runStateT (traverse metavariable f) Map.empty