git.iko.soy/Idris-dev
on master help sign in
Stop let-binding Elab scripts around their holes
83aa146David Raymond Christiansen
src/Idris/Elab/Term.hs+4−4
compare with master
unifiedsplit
@@ -1237,17 +1237,17 @@ elab ist info emode opts fn tm
1237 elab' ina fc (PRunElab fc' tm ns) =
1237 elab' ina fc (PRunElab fc' tm ns) =
1238 do attack
1238 do attack
1239 n <- getNameFrom (sMN 0 "tacticScript")
1239 n <- getNameFrom (sMN 0 "tacticScript")
1240− n' <- getNameFrom (sMN 0 "tacticExpr")
1241 let scriptTy = RApp (Var (sNS (sUN "Elab")
1240 let scriptTy = RApp (Var (sNS (sUN "Elab")
1242 ["Elab", "Reflection", "Language"]))
1241 ["Elab", "Reflection", "Language"]))
1243 (Var unitTy)
1242 (Var unitTy)
1244 claim n scriptTy
1243 claim n scriptTy
1245− movelast n
1246− letbind n' scriptTy (Var n)
1247 focus n
1244 focus n
1245+ attack -- to get an extra hole
1248 elab' ina (Just fc') tm
1246 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
1249 env <- get_env
1249 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
1251 solve
1251 solve
1252 elab' ina fc (PConstSugar constFC tm) =
1252 elab' ina fc (PConstSugar constFC tm) =
1253 -- Here we elaborate the contained term, then calculate
1253 -- Here we elaborate the contained term, then calculate
test/meta002/Tacs.idr+7−2
@@ -53,6 +53,7 @@ test1 = %runElab triv
53test2 : Nat
53test2 : Nat
54test2 = %runElab triv
54test2 = %runElab triv
55
55
56+partial
56obvious : Elab ()
57obvious : Elab ()
57obvious = do g <- goalType
58obvious = do g <- goalType
58 case g of
59 case g of
@@ -120,8 +121,12 @@ namespace STLC
120 unfocus holeName
121 unfocus holeName
121 return holeName
122 return holeName
122
123
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?)
123− foo : %runElab (elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT))
128+ someDef : let x = () in %runElab ((elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT)))
124− foo = id
129+ someDef = id
125
130
126 namespace Untyped
131 namespace Untyped
127 ||| Completely untyped terms
132 ||| Completely untyped terms
test/meta002/expected+1−1
@@ -1,3 +1,3 @@
1−Tacs.idr:291:15:
1+Tacs.idr:296:15:
2When checking right hand side of testElab3:
2When checking right hand side of testElab3:
3Unifying ty and ARR ty t would lead to infinite value
3Unifying ty and ARR ty t would lead to infinite value