git.iko.soy/Idris-dev
on master help sign in
Stop let-binding Elab scripts around their holes

This prevents them from showing up in intermediate elaboration states and making things difficult to read.

commit83aa146947b0f523de485adbdbdbd3b05e24267f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 8 Oct 2015, 18:37 (11 years ago) parent3b9206b
3 files changed+12−7
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+4−4 test/meta002/Tacs.idr+7−2 test/meta002/expected+1−1
src/Idris/Elab/Term.hs+4−4
@@ -1237,17 +1237,17 @@ elab ist info emode opts fn tm
12371237 elab' ina fc (PRunElab fc' tm ns) =
12381238 do attack
12391239 n <- getNameFrom (sMN 0 "tacticScript")
1240− n' <- getNameFrom (sMN 0 "tacticExpr")
12411240 let scriptTy = RApp (Var (sNS (sUN "Elab")
12421241 ["Elab", "Reflection", "Language"]))
12431242 (Var unitTy)
12441243 claim n scriptTy
1245− movelast n
1246− letbind n' scriptTy (Var n)
12471244 focus n
1245+ attack -- to get an extra hole
12481246 elab' ina (Just fc') tm
1247+ script <- get_guess
1248+ solve -- eliminate the hole. Becuase there are no references, the script is only in the binding
12491249 env <- get_env
1250− runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns
1250+ runElabAction ist (maybe fc' id fc) env script ns
12511251 solve
12521252 elab' ina fc (PConstSugar constFC tm) =
12531253 -- Here we elaborate the contained term, then calculate
test/meta002/Tacs.idr+7−2
@@ -53,6 +53,7 @@ test1 = %runElab triv
5353test2 : Nat
5454test2 = %runElab triv
5555
56+partial
5657obvious : Elab ()
5758obvious = do g <- goalType
5859 case g of
@@ -120,8 +121,12 @@ namespace STLC
120121 unfocus holeName
121122 return holeName
122123
123− foo : %runElab (elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT))
124− foo = id
124+ -- FIXME: Removing the let-bound Elab script showed a deficiency in
125+ -- how accessible arguments are identified in type signatures. It
126+ -- would be nice if this worked without the extraneous
127+ -- `let`. (perhaps a flag on Pi that says it came from the parser?)
128+ someDef : let x = () in %runElab ((elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT)))
129+ someDef = id
125130
126131 namespace Untyped
127132 ||| Completely untyped terms
test/meta002/expected+1−1
@@ -1,3 +1,3 @@
1−Tacs.idr:291:15:
1+Tacs.idr:296:15:
22When checking right hand side of testElab3:
33Unifying ty and ARR ty t would lead to infinite value