diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index cdcd2ea72..ada77764f 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -47,15 +47,18 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp nfOpts withAll defs env !(reflect fc defs False env tm) elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars) - elabCon defs "Pure" [_,val] = evalClosure defs val + elabCon defs "Pure" [_,val] + = do empty <- clearDefs defs + evalClosure empty val elabCon defs "Bind" [_,_,act,k] = do act' <- elabScript fc nest env !(evalClosure defs act) exp case !(evalClosure defs k) of NBind _ x (Lam _ _ _) sc => - elabScript fc nest env + do empty <- clearDefs defs + elabScript fc nest env !(sc defs (toClosure withAll env - !(quote defs env act'))) exp + !(quote empty env act'))) exp _ => failWith defs elabCon defs "Fail" [_,msg] = do msg' <- evalClosure defs msg @@ -165,7 +168,8 @@ checkRunElab rig elabinfo nest env fc script exp ntm <- elabScript fc nest env !(nfOpts withAll defs env stm) (Just (gnf env expected)) defs <- get Ctxt -- might have updated as part of the script - pure (!(quote defs env ntm), gnf env expected) + empty <- clearDefs defs + pure (!(quote empty env ntm), gnf env expected) where mkExpected : Maybe (Glued vars) -> Core (Term vars) mkExpected (Just ty) = pure !(getTerm ty) diff --git a/tests/idris2/reflection002/expected b/tests/idris2/reflection002/expected index a7a46818c..361def40a 100644 --- a/tests/idris2/reflection002/expected +++ b/tests/idris2/reflection002/expected @@ -1,8 +1,8 @@ 1/1: Building power (power.idr) Main> Main.cube : Nat -> Nat -cube = \x => mult x (mult x (mult x 1)) +cube = \x => mult x (mult x (mult x (const (fromInteger 1) x))) Main> 27 Main> Main.cube' : Nat -> Nat -cube' = \x => mult (mult (plus x 0) x) x +cube' = \x => mult (mult (mult (const (fromInteger 1) x) x) x) x Main> 27 Main> Bye for now!