idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

Reduce amount of normalisation in elab scripts

Browse Source 
We don't want to unfold definitions in 'pure' or 'check' or 'bind' since
we want the exact expression that the script author has used.
This commit is contained in:
Edwin Brady 2020-06-03 00:22:03 +01:00
parent d8d13d912e
commit c682ded9c4
2 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/TTImp/Elab/RunElab.idr
View File

@ -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)

4
tests/idris2/reflection002/expected
View File

@ -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!