[ experim ] Use old approach and additional elab option

buzden · Aug 10, 2023 · e11e65f · e11e65f
1 parent dfe6f0e
commit e11e65f
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 3 deletions.
diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr
@@ -120,7 +120,9 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
 
          defs <- get Ctxt
          e <- newRef EST (initEStateSub defining env' sub)
-         let rigc = getRigNeeded mode
+         let rigc = case foldMap (\case OverrideRig x => Just x; _ => Nothing) opts of
+                      Nothing => getRigNeeded mode
+                      Just x  => x
 
          (chktm, chkty) <- check {e} rigc (initElabInfo mode) nest env tm ty
          -- Final retry of constraints and delayed elaborations

diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr
@@ -49,13 +49,15 @@ data ElabOpt
   | InCase
   | InPartialEval
   | InTrans
+  | OverrideRig RigCount
 
 public export
 Eq ElabOpt where
   HolesOkay == HolesOkay = True
   InCase == InCase = True
   InPartialEval == InPartialEval = True
   InTrans == InTrans = True
+  OverrideRig x == OverrideRig y = x == y
   _ == _ = False
 
 -- Descriptions of implicit name bindings. They're either just the name,

diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr
@@ -38,6 +38,5 @@ processRunElab eopts nest env fc tm
          unit <- getCon fc defs (builtin "Unit")
          exp <- appCon fc defs n [unit]
 
-         e <- newRef EST $ initEStateSub tidx env SubRefl
-         (stm, _) <- check bot (initElabInfo InExpr) nest env tm $ Just $ gnf env exp
+         stm <- checkTerm tidx InExpr (OverrideRig bot :: eopts) nest env tm (gnf env exp)
          ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing