44 lines
1.5 KiB
Plaintext
44 lines
1.5 KiB
Plaintext
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 { 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) }
|
|
derive instance Functor ProofTree
|
|
|
|
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
|