@@ -17,6 +17,34 @@ skip = pure ()
1717try : Alternative f => f a -> f ()
1818try tac = ignore tac <|> pure ()
1919
20+||| Remove type information from a `TT` term, in a context. Fails if
21+||| de Bruijn indices are out of scope.
22+forget' : List TTName -> TT -> Elab Raw
23+forget' env (P nt n tm) = pure (Var n)
24+forget' env (V x) = Var <$> getName x env
25+ where getName : Int -> List a -> Elab a
26+ getName _ [] = fail [TextPart "Scope error when forget'ting types"]
27+ getName i (n::ns) = if i <= 0 then pure n else getName (i-1) ns
28+forget' env (Bind n b tm) =
29+ [| (RBind n)
30+ (assert_total $ traverse (forget' env) b)
31+ (forget' (n::env) tm) |]
32+forget' env (App tm tm') = [| RApp (forget' env tm) (forget' env tm') |]
33+forget' env (TConst c) = pure (RConstant c)
34+forget' env Erased = pure (RConstant Forgot)
35+forget' env (TType uexp) = pure RType
36+forget' env (UType uni) = pure (RUType uni)
37+
38+||| Remove type information from a `TT` term. Fails if de Bruijn
39+||| indices are out of scope.
40+forget : TT -> Elab Raw
41+forget tm = forget' [] tm
42+
43+||| Get the goal type as a Raw term. Fails if there are no holes.
44+goalType : Elab Raw
45+goalType = do g <- getGoal
46+ forget (snd g)
47+
2048||| Solve the goal using the most recent applicable hypothesis
2149hypothesis : Elab ()
2250hypothesis =
@@ -155,7 +183,7 @@ inferType tac =
155183 _ => fail [TextPart "Not infer"]
156184 where
157185 startInfer : Elab ()
158− startInfer = do [_, (_, tmH)] <- apply (Var `{MkInfer}) [(True, 0), (False, 1)]
186+ startInfer = do [_, tmH] <- apply (Var `{MkInfer}) [True, False]
159187 | err => fail [TextPart "Type inference failure"]
160188 solve
161189 focus tmH
@@ -181,15 +209,15 @@ andThen first after =
181209||| @ tm the term to apply to some number of goals
182210refine : (tm : Raw) -> Elab (List TTName)
183211refine tm =
184− do ty <- (snd <$> check !getEnv tm) >>= forgetTypes
212+ do ty <- (snd <$> check !getEnv tm) >>= forget
185213 g <- goalType
186214
187215 -- we don't care about negative results because it'll just fail anyway
188216 let argCount = minus (countPi ty) (countPi g)
189− newHoles <- apply tm (replicate argCount (True, 0))
217+ newHoles <- apply tm (replicate argCount True)
190218 solve
191219 actualHoles <- getHoles
192− return (filter (flip elem actualHoles) (map snd newHoles))
220+ return (filter (flip elem actualHoles) newHoles)
193221
194222 where countPi : Raw -> Nat
195223 countPi (RBind _ (Pi _ _) body) = S (countPi body)
@@ -206,7 +234,7 @@ both tm n1 n2 =
206234 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
207235 where
208236 isPairTy : TT -> Elab (Raw, Raw)
209− isPairTy `((~A, ~B) : Type) = [| MkPair (forgetTypes A) (forgetTypes B) |]
237+ isPairTy `((~A, ~B) : Type) = [| MkPair (forget A) (forget B) |]
210238 isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]
211239
212240||| Let-bind all results of completely destructuring nested tuples.