From 9544e05da143f5f6678bbd3540482ba03e60e189 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sun, 31 May 2020 13:05:06 +0100
Subject: [PATCH] Process elaborator scripts

Still all they can do is check and log. Now scripts must return
something of type TT, which is in practice a TTImp that goes to the
elaborator for final checking
---
 libs/base/Language/Reflection.idr |  6 ++---
 src/TTImp/Elab/RunElab.idr        | 39 +++++++++++++++++++++----------
 2 files changed, 30 insertions(+), 15 deletions(-)

diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr
index 17c6c6bb3..6f49c9987 100644
--- a/libs/base/Language/Reflection.idr
+++ b/libs/base/Language/Reflection.idr
@@ -13,18 +13,18 @@ data Elab : Type -> Type where
      Check : TTImp -> Elab TT
 
 mutual
-  export
+  public export
   Functor Elab where
     map f e = do e' <- e
                  pure (f e')
 
-  export
+  public export
   Applicative Elab where
     pure = Pure
     f <*> a = do f' <- f
                  a' <- a
                  pure (f' a')
 
-  export
+  public export
   Monad Elab where
     (>>=) = Bind
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index c31948fdd..13f5fa2a7 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -22,11 +22,10 @@ elabScript : {vars : _} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto e : Ref EST (EState vars)} ->
-             FC -> RigCount -> ElabInfo -> NestedNames vars ->
-             Env Term vars -> NF vars -> Maybe (Glued vars) ->
-             Core (Term vars, Glued vars)
-elabScript fc rig elabinfo nest env
-           tm@(NDCon _ nm _ _ args) exp
+             FC -> ElabInfo -> NestedNames vars ->
+             Env Term vars -> NF vars ->
+             Core (NF vars)
+elabScript fc elabinfo nest env tm@(NDCon _ nm _ _ args)
     = do defs <- get Ctxt
          fnm <- toFullNames nm
          case fnm of
@@ -40,13 +39,26 @@ elabScript fc rig elabinfo nest env
            empty <- clearDefs defs
            throw (BadRunElab fc env !(quote empty env tm))
 
-    elabCon : Defs -> String -> List (Closure vars) -> Core (Term vars, Glued vars)
-    elabCon defs "Check" [ttimp]
-        = do tt <- evalClosure defs ttimp
-             raw <- reify defs tt
-             check rig elabinfo nest env raw exp
+    elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)
+    elabCon defs "Pure" [_,val] = evalClosure defs val
+    elabCon defs "Bind" [_,_,act,k]
+        = do act' <- elabScript fc elabinfo nest env
+                                !(evalClosure defs act)
+             case !(evalClosure defs k) of
+                  NBind _ x (Lam _ _ _) sc =>
+                      elabScript fc elabinfo nest env
+                                 !(sc defs (toClosure withAll env
+                                                 !(quote defs env act')))
+                  _ => failWith defs
+    elabCon defs "Log" [lvl, str]
+        = do lvl' <- evalClosure defs lvl
+             logC !(reify defs lvl') $
+                  do str' <- evalClosure defs str
+                     reify defs str'
+             nfOpts withAll defs env !(reflect fc defs env ())
+    elabCon defs "Check" [ttimp] = evalClosure defs ttimp -- to be reified
     elabCon defs n args = failWith defs
-elabScript fc rig elabinfo nest env script exp
+elabScript fc elabinfo nest env script
     = do defs <- get Ctxt
          empty <- clearDefs defs
          throw (BadRunElab fc env !(quote empty env script))
@@ -66,4 +78,7 @@ checkRunElab rig elabinfo nest env fc script exp
          when (not (isExtension ElabReflection defs)) $
              throw (GenericMsg fc "%language ElabReflection not enabled")
          (stm, sty) <- check rig elabinfo nest env script Nothing
-         elabScript fc rig elabinfo nest env !(nf defs env stm) exp
+         defs <- get Ctxt -- checking might have resolved some holes
+         ntm <- elabScript fc elabinfo nest env !(nfOpts withAll defs env stm)
+         defs <- get Ctxt -- might have updated as part of the script
+         check rig elabinfo nest env !(reify defs ntm) exp