Implement a 'match' builtin to provide introspection of terms in the CaPriCon tactic language

capricon/src/Algebra/Monad/Concatenative.hs

 {-# LANGUAGE FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, LambdaCase, DeriveGeneric #-}
 module Algebra.Monad.Concatenative(
   -- * Extensible stack types
-  StackBuiltin(..),StackSymbol(..),StackVal(..),StackStep(..),StackClosure(..),
+  StackBuiltin(..),StackSymbol(..),StackVal(..),StackStep(..),StackClosure(..),execValue,
   t'StackDict,
   -- * The MonadStack class
   StackState,defaultState,
@@ -143,8 +143,8 @@ execSymbolImpl execBuiltin' onComment atom = do
   where execStep [] stp = runStep execBuiltin' onComment stp
         execStep (StackClosure cs p:ps) stp = progStack =- (StackClosure cs (stp:p):ps)
 
-execBuiltin :: (StackSymbol s, MonadState (StackState st s b a) m) => (b -> m ()) -> (s -> m ()) -> StackBuiltin b -> m ()
-execBuiltin runExtra onComment = go
+execBuiltinImpl :: (StackSymbol s, MonadState (StackState st s b a) m) => (b -> m ()) -> (s -> m ()) -> StackBuiltin b -> m ()
+execBuiltinImpl runExtra onComment = go
   where 
     go Builtin_Def = get >>= \st -> case st^.stack of
       (val:StackSymbol var:tl) -> do dict =~ insert var val ; stack =- tl
@@ -236,16 +236,22 @@ execBuiltin runExtra onComment = go
 class (StackSymbol s,Monad m) => MonadStack st s b a m | m -> st s b a where
   execSymbol :: (b -> m ()) -> (s -> m ()) -> s -> m ()
   execProgram :: (b -> m ()) -> (s -> m ()) -> StackProgram s b a -> m ()
+  execBuiltin :: (b -> m ()) -> (s -> m ()) -> StackBuiltin b -> m ()
   runStackState :: State [StackVal s b a] x -> m x
   runExtraState :: State st x -> m x
   runDictState :: State (Map s (StackVal s b a)) x -> m x
 
+execValue runExtra onComment (StackProg p) = execProgram runExtra onComment p
+execValue runExtra onComment (StackBuiltin b) = execBuiltin runExtra onComment b
+execValue _ _ _ = unit
+
 newtype ConcatT st b o s m a = ConcatT { _concatT :: StateT (StackState st s b o) m a }
                           deriving (Functor,SemiApplicative,Unit,Applicative,MonadTrans)
 instance Monad m => Monad (ConcatT st b o s m) where join = coerceJoin ConcatT
 instance (StackSymbol s,Monad m) => MonadStack st s b a (ConcatT st b a s m) where
-  execSymbol x y z = ConcatT $ execSymbolImpl (execBuiltin (map _concatT x) (map _concatT y)) (map _concatT y) z
-  execProgram x y p = ConcatT $ traverse_ (runStep (execBuiltin (map _concatT x) (map _concatT y)) (map _concatT y)) p
+  execSymbol x y z = ConcatT $ execSymbolImpl (execBuiltinImpl (map _concatT x) (map _concatT y)) (map _concatT y) z
+  execProgram x y p = ConcatT $ traverse_ (runStep (execBuiltinImpl (map _concatT x) (map _concatT y)) (map _concatT y)) p
+  execBuiltin x y b = ConcatT $ execBuiltinImpl (map _concatT x) (map _concatT y) b
   runStackState st = ConcatT $ (\x -> return (swap $ stack (map swap (st^..state)) x))^.stateT
   runExtraState st = ConcatT $ (\x -> return (swap $ extraState (map swap (st^..state)) x))^.stateT
   runDictState st = ConcatT $ (\x -> return (swap $ dict (map swap (st^..state)) x))^.stateT

capricon/src/CaPriCon/Run.hs

@@ -79,7 +79,7 @@ data COCBuiltin io str = COCB_Print
                        | COCB_HypBefore | COCB_Subst | COCB_Rename
                        | COCB_ContextVars | COCB_Axiom
                        | COCB_GetShowDir | COCB_SetShowDir | COCB_InsertNodeDir
-                       | COCB_Format | COCB_Extract
+                       | COCB_Format | COCB_Extract | COCB_MatchTerm
                        deriving (Show,Generic)
 data ReadImpl io str bytes = ReadImpl (str -> io (Maybe bytes))
 data WriteImpl io str bytes = WriteImpl (str -> bytes -> io ())
@@ -251,6 +251,45 @@ runCOCBuiltin COCB_Mu = do
     StackCOC (COCExpr e):t | Just e' <- runInContext ctx (mkMu e) -> StackCOC (COCExpr e'):t
                            | otherwise -> StackCOC COCNull:t
     st -> st
+
+runCOCBuiltin COCB_MatchTerm = do
+  st <- runStackState get
+  cctx <- runExtraState (getl context)
+  let tailCall v go = go >> execValue runCOCBuiltin (const unit) v
+  case st of
+    onLambda:onProduct:onApply:onMu:onVar:onAxiom:StackCOC (COCExpr (ContextNode d e)):st' ->
+      case e of
+        Bind Lambda x tx e' -> tailCall onLambda $ do
+          runExtraState $ context =~ ((x,tx):)
+          runStackState $ put (StackCOC (COCExpr (ContextNode (d+1) (Cons (Ap (Sym 0) []))))
+                               :StackCOC (COCExpr (ContextNode (d+1) e'))
+                               :st')
+        Bind Prod x tx e' -> tailCall onProduct $ do
+          runExtraState $ context =~ ((x,tx):)
+          runStackState $ put (StackCOC (COCExpr (ContextNode (d+1) (Cons (Ap (Sym 0) []))))
+                               :StackCOC (COCExpr (ContextNode (d+1) e'))
+                               :st')
+        Cons (Ap h []) -> do
+          case h of
+            Sym i | (x,_):_ <- takeLast (d-i) cctx -> tailCall onVar $ runStackState $ put (StackSymbol x:st')
+                  | otherwise -> tailCall onVar $ runStackState $ put (StackSymbol ("#"+fromString (show i)):st')
+            Mu ctx _ a -> do
+              let a' = foldl' (\e' (x,tx,_) -> Bind Lambda x tx e') (Cons a) ctx
+              tailCall onMu $ runStackState $ put (StackCOC (COCExpr (ContextNode d a'))
+                                                   :st')
+            Axiom t a -> tailCall onAxiom $ do
+              runStackState $ put (StackSymbol a
+                                   :StackCOC (COCExpr (ContextNode 0 t))
+                                   :st')
+        Cons (Ap h args) -> tailCall onApply $ do
+          runStackState $ put (StackList (map (StackCOC . COCExpr . ContextNode d) args)
+                               :StackCOC (COCExpr (ContextNode d (Cons (Ap h []))))
+                               :st')
+        _ -> unit
+
+    _ -> unit
+          
+
 runCOCBuiltin COCB_TypeOf = do
   ctx <- runExtraState (getl context)
   runStackState $ modify $ \case
@@ -411,6 +450,7 @@ cocDict version getResource getBResource writeResource writeBResource =
                ("term/convertible"         , Builtin_Extra COCB_Convertible        ),
                ("term/axiom"               , Builtin_Extra COCB_Axiom              ),
                ("term/extract"             , Builtin_Extra COCB_Extract            ),
+               ("term/match"               , Builtin_Extra COCB_MatchTerm          ),
 
                ("context/intro"           , Builtin_Extra COCB_Hyp                ),
                ("context/intro-before"    , Builtin_Extra COCB_HypBefore          ),