git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/ElabTerm.hs
1715 lines 78 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.ElabTerm where
5import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
7import Idris.DSL
8import Idris.Delaborate
9import Idris.Error
10import Idris.ProofSearch
11import Idris.Output (pshow)
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.TT
15import Idris.Core.Evaluate
16import Idris.Core.Unify
17import Idris.Core.Typecheck (check)
18import Idris.ErrReverse (errReverse)
20import Control.Applicative ((<$>))
21import Control.Monad
22import Control.Monad.State.Strict
23import Data.List
24import qualified Data.Map as M
25import Data.Maybe (mapMaybe, fromMaybe)
26import qualified Data.Set as S
27import qualified Data.Text as T
29import Debug.Trace
31-- Using the elaborator, convert a term in raw syntax to a fully
32-- elaborated, typechecked term.
33--
34-- If building a pattern match, we convert undeclared variables from
35-- holes to pattern bindings.
37-- Also find deferred names in the term and their types
39build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
40 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
41build ist info pattern opts fn tm
42 = do elab ist info pattern opts fn tm
43 let tmIn = tm
44 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
45 [TIPartial] -> True
46 _ -> False
47 ivs <- get_instances
48 hs <- get_holes
49 ptm <- get_term
50 -- Resolve remaining type classes. Two passes - first to get the
51 -- default Num instances, second to clean up the rest
52 when (not pattern) $
53 mapM_ (\n -> when (n `elem` hs) $
54 do focus n
55 g <- goal
56 try (resolveTC 7 g fn ist)
57 (movelast n)) ivs
58 ivs <- get_instances
59 hs <- get_holes
60 when (not pattern) $
61 mapM_ (\n -> when (n `elem` hs) $
62 do focus n
63 g <- goal
64 resolveTC 7 g fn ist) ivs
65 tm <- get_term
66 ctxt <- get_context
67 probs <- get_probs
68 u <- getUnifyLog
70 when (not pattern) $
71 traceWhen u ("Remaining problems:\n" ++ show probs) $
72 do unify_all; matchProblems True; unifyProblems
73 probs <- get_probs
74 case probs of
75 [] -> return ()
76 ((_,_,_,e,_,_):es) -> if inf then return ()
77 else lift (Error e)
78 is <- getAux
79 tt <- get_term
80 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
81 log <- getLog
82 if (log /= "") then trace log $ return (tm, ds, is)
83 else return (tm, ds, is)
85-- Build a term autogenerated as a typeclass method definition
86-- (Separate, so we don't go overboard resolving things that we don't
87-- know about yet on the LHS of a pattern def)
89buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
90 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
91buildTC ist info pattern opts fn tm
92 = do -- set name supply to begin after highest index in tm
93 let ns = allNamesIn tm
94 let tmIn = tm
95 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
96 [TIPartial] -> True
97 _ -> False
98 initNextNameFrom ns
99 elab ist info pattern opts fn tm
100 probs <- get_probs
101 tm <- get_term
102 case probs of
103 [] -> return ()
104 ((_,_,_,e,_,_):es) -> if inf then return ()
105 else lift (Error e)
106 is <- getAux
107 tt <- get_term
108 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
109 log <- getLog
110 if (log /= "") then trace log $ return (tm, ds, is)
111 else return (tm, ds, is)
113-- Returns the set of declarations we need to add to complete the definition
114-- (most likely case blocks to elaborate)
116elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
117 ElabD ()
118elab ist info pattern opts fn tm
119 = do let loglvl = opt_logLevel (idris_options ist)
120 when (loglvl > 5) $ unifyLog True
121 compute -- expand type synonyms, etc
122 elabE (False, False, False) tm -- (in argument, guarded, in type)
123 end_unify
124 when pattern -- convert remaining holes to pattern vars
125 (do update_term orderPats
126 unify_all
127 matchProblems False -- only the ones we matched earlier
128 unifyProblems
129 mkPat)
130 where
131 tcgen = Dictionary `elem` opts
132 reflect = Reflection `elem` opts
134 isph arg = case getTm arg of
135 Placeholder -> (True, priority arg)
136 _ -> (False, priority arg)
138 toElab ina arg = case getTm arg of
139 Placeholder -> Nothing
140 v -> Just (priority arg, elabE ina v)
142 toElab' ina arg = case getTm arg of
143 Placeholder -> Nothing
144 v -> Just (elabE ina v)
146 mkPat = do hs <- get_holes
147 tm <- get_term
148 case hs of
149 (h: hs) -> do patvar h; mkPat
150 [] -> return ()
152 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
153 elabE ina t =
154 --do g <- goal
155 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
156 do ct <- insertCoerce ina t
157 t' <- insertLazy ct
158 g <- goal
159 tm <- get_term
160 ps <- get_probs
161 hs <- get_holes
162 --trace ("Elaborating " ++ show t' ++ " in " ++ show g
163 -- ++ "\n" ++ show tm
164 -- ++ "\nholes " ++ show hs
165 -- ++ "\nproblems " ++ show ps
166 -- ++ "\n-----------\n") $
167 --trace ("ELAB " ++ show t') $
168 let fc = fileFC "Force"
169 env <- get_env
170 handleError (forceErr env)
171 (elab' ina t')
172 (elab' ina (PApp fc (PRef fc (sUN "Force"))
173 [pimp (sUN "t") Placeholder True,
174 pimp (sUN "a") Placeholder True,
175 pexp ct])) True
177 forceErr env (CantUnify _ t t' _ _ _)
178 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
179 ht == txt "Lazy'" = True
180 forceErr env (CantUnify _ t t' _ _ _)
181 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
182 ht == txt "Lazy'" = True
183 forceErr env (InfiniteUnify _ t _)
184 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
185 ht == txt "Lazy'" = True
186 forceErr env (Elaborating _ _ t) = forceErr env t
187 forceErr env (ElaboratingArg _ _ _ t) = forceErr env t
188 forceErr env (At _ t) = forceErr env t
189 forceErr env t = False
191 local f = do e <- get_env
192 return (f `elem` map fst e)
194 -- | Is a constant a type?
195 constType :: Const -> Bool
196 constType (AType _) = True
197 constType StrType = True
198 constType PtrType = True
199 constType VoidType = True
200 constType _ = False
202 elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
203 -> PTerm -- ^ The term to elaborate
204 -> ElabD ()
205 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
206 elab' ina PType = do apply RType []; solve
207-- elab' (_,_,inty) (PConstant c)
208-- | constType c && pattern && not reflect && not inty
209-- = lift $ tfail (Msg "Typecase is not allowed")
210 elab' ina (PConstant c) = do apply (RConstant c) []; solve
211 elab' ina (PQuote r) = do fill r; solve
212 elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
213 (elab' ina (PRef fc unitTy))
214 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
215 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
216 = do g <- goal; resolveTC 5 g fn ist
217 elab' ina (PResolveTC fc)
218 | True = do c <- getNameFrom (sMN 0 "class")
219 instanceArg c
220 | otherwise = do g <- goal
221 try (resolveTC 2 g fn ist)
222 (do c <- getNameFrom (sMN 0 "class")
223 instanceArg c)
224 elab' ina (PRefl fc t)
225 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
226 pimp (sMN 0 "x") t False])
227 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)
228 [pimp (sMN 0 "A") Placeholder True,
229 pimp (sMN 0 "B") Placeholder False,
230 pexp l, pexp r])
231 elab' ina@(_, a, inty) (PPair fc _ l r)
232 = do hnf_compute
233 g <- goal
234 case g of
235 TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
236 [pexp l,pexp r])
237 _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
238 [pimp (sMN 0 "A") Placeholder True,
239 pimp (sMN 0 "B") Placeholder True,
240 pexp l, pexp r])
241 elab' ina (PDPair fc p l@(PRef _ n) t r)
242 = case t of
243 Placeholder ->
244 do hnf_compute
245 g <- goal
246 case g of
247 TType _ -> asType
248 _ -> asValue
249 _ -> asType
250 where asType = elab' ina (PApp fc (PRef fc sigmaTy)
251 [pexp t,
252 pexp (PLam n Placeholder r)])
253 asValue = elab' ina (PApp fc (PRef fc existsCon)
254 [pimp (sMN 0 "a") t False,
255 pimp (sMN 0 "P") Placeholder True,
256 pexp l, pexp r])
257 elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)
258 [pimp (sMN 0 "a") t False,
259 pimp (sMN 0 "P") Placeholder True,
260 pexp l, pexp r])
261 elab' ina (PAlternative True as)
262 = do hnf_compute
263 ty <- goal
264 ctxt <- get_context
265 let (tc, _) = unApply ty
266 let as' = pruneByType tc ctxt as
267-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
268 tryAll (zip (map (elab' ina) as') (map showHd as'))
269 where showHd (PApp _ (PRef _ n) _) = show n
270 showHd (PRef _ n) = show n
271 showHd (PApp _ h _) = show h
272 showHd x = show x
273 elab' ina (PAlternative False as)
274 = trySeq as
275 where -- if none work, take the error from the first
276 trySeq (x : xs) = let e1 = elab' ina x in
277 try' e1 (trySeq' e1 xs) True
278 trySeq' deferr [] = proofFail deferr
279 trySeq' deferr (x : xs)
280 = try' (elab' ina x) (trySeq' deferr xs) True
281 elab' ina (PPatvar fc n) | pattern = patvar n
282-- elab' (_, _, inty) (PRef fc f)
283-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
284-- = lift $ tfail (Msg "Typecase is not allowed")
285 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
286 = do ctxt <- get_context
287 let defined = case lookupTy n ctxt of
288 [] -> False
289 _ -> True
290 -- this is to stop us resolve type classes recursively
291 -- trace (show (n, guarded)) $
292 if (tcname n && ina) then erun fc $ patvar n
293 else if (defined && not guarded)
294 then do apply (Var n) []; solve
295 else try (do apply (Var n) []; solve)
296 (patvar n)
297 where inparamBlock n = case lookupCtxtName n (inblock info) of
298 [] -> False
299 _ -> True
300 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
301 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
302 elab' ina@(_, a, inty) (PLam n Placeholder sc)
303 = do -- if n is a type constructor name, this makes no sense...
304 ctxt <- get_context
305 when (isTConName n ctxt) $
306 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
307 checkPiGoal n
308 attack; intro (Just n);
309 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
310 elabE (True, a, inty) sc; solve
311 elab' ina@(_, a, inty) (PLam n ty sc)
312 = do tyn <- getNameFrom (sMN 0 "lamty")
313 -- if n is a type constructor name, this makes no sense...
314 ctxt <- get_context
315 when (isTConName n ctxt) $
316 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
317 checkPiGoal n
318 claim tyn RType
319 explicit tyn
320 attack
321 ptm <- get_term
322 hs <- get_holes
323 introTy (Var tyn) (Just n)
324 focus tyn
325 elabE (True, a, True) ty
326 elabE (True, a, inty) sc
327 solve
328 elab' ina@(_, a, _) (PPi _ n Placeholder sc)
329 = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve
330 elab' ina@(_, a, _) (PPi _ n ty sc)
331 = do attack; tyn <- getNameFrom (sMN 0 "ty")
332 claim tyn RType
333 n' <- case n of
334 MN _ _ -> unique_hole n
335 _ -> return n
336 forall n' (Var tyn)
337 focus tyn
338 elabE (True, a, True) ty
339 elabE (True, a, True) sc
340 solve
341 elab' ina@(_, a, inty) (PLet n ty val sc)
342 = do attack;
343 tyn <- getNameFrom (sMN 0 "letty")
344 claim tyn RType
345 valn <- getNameFrom (sMN 0 "letval")
346 claim valn (Var tyn)
347 explicit valn
348 letbind n (Var tyn) (Var valn)
349 case ty of
350 Placeholder -> return ()
351 _ -> do focus tyn
352 explicit tyn
353 elabE (True, a, True) ty
354 focus valn
355 elabE (True, a, True) val
356 env <- get_env
357 elabE (True, a, inty) sc
358 -- HACK: If the name leaks into its type, it may leak out of
359 -- scope outside, so substitute in the outer scope.
360 expandLet n (case lookup n env of
361 Just (Let t v) -> v)
362 solve
363 elab' ina@(_, a, inty) (PGoal fc r n sc) = do
364 rty <- goal
365 attack
366 tyn <- getNameFrom (sMN 0 "letty")
367 claim tyn RType
368 valn <- getNameFrom (sMN 0 "letval")
369 claim valn (Var tyn)
370 letbind n (Var tyn) (Var valn)
371 focus valn
372 elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
373 env <- get_env
374 computeLet n
375 elabE (True, a, inty) sc
376 solve
377-- elab' ina (PLet n Placeholder
378-- (PApp fc r [pexp (delab ist rty)]) sc)
379 elab' ina tm@(PApp fc (PInferRef _ f) args) = do
380 rty <- goal
381 ds <- get_deferred
382 ctxt <- get_context
383 -- make a function type a -> b -> c -> ... -> rty for the
384 -- new function name
385 env <- get_env
386 argTys <- claimArgTys env args
387 fn <- getNameFrom (sMN 0 "inf_fn")
388 let fty = fnTy argTys rty
389-- trace (show (ptm, map fst argTys)) $ focus fn
390 -- build and defer the function application
391 attack; deferType (mkN f) fty (map fst argTys); solve
392 -- elaborate the arguments, to unify their types. They all have to
393 -- be explicit.
394 mapM_ elabIArg (zip argTys args)
395 where claimArgTys env [] = return []
396 claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
397 = do nty <- get_type (Var n)
398 ans <- claimArgTys env xs
399 return ((n, (False, forget nty)) : ans)
400 claimArgTys env (_ : xs)
401 = do an <- getNameFrom (sMN 0 "inf_argTy")
402 aval <- getNameFrom (sMN 0 "inf_arg")
403 claim an RType
404 claim aval (Var an)
405 ans <- claimArgTys env xs
406 return ((aval, (True, (Var an))) : ans)
407 fnTy [] ret = forget ret
408 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)
410 localVar env (PRef _ x)
411 = case lookup x env of
412 Just _ -> Just x
413 _ -> Nothing
414 localVar env _ = Nothing
416 elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
417 elabIArg _ = return () -- already done, just a name
419 mkN n@(NS _ _) = n
420 mkN n@(SN _) = n
421 mkN n = case namespace info of
422 Just xs@(_:_) -> sNS n xs
423 _ -> n
425 elab' ina (PMatchApp fc fn)
426 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
427 [(n, args)] -> return (n, map (const True) args)
428 _ -> lift $ tfail (NoSuchVariable fn)
429 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
430 solve
431 elab' (_, _, inty) (PApp fc (PRef _ f) args')
432 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
433 = lift $ tfail (Msg "Typecase is not allowed")
434 -- if f is local, just do a simple_app
435 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
436 = do env <- get_env
437 if (f `elem` map fst env && length args == 1)
438 then -- simple app, as below
439 do simple_app (elabE (ina, g, inty) (PRef fc f))
440 (elabE (True, g, inty) (getTm (head args)))
441 (show tm)
442 solve
443 else
444 do ivs <- get_instances
445 ps <- get_probs
446 -- HACK: we shouldn't resolve type classes if we're defining an instance
447 -- function or default definition.
448 let isinf = f == inferCon || tcname f
449 -- if f is a type class, we need to know its arguments so that
450 -- we can unify with them
451 case lookupCtxt f (idris_classes ist) of
452 [] -> return ()
453 _ -> mapM_ setInjective (map getTm args)
454 ctxt <- get_context
455 let guarded = isConName f ctxt
456-- trace ("args is " ++ show args) $ return ()
457 ns <- apply (Var f) (map isph args)
458-- trace ("ns is " ++ show ns) $ return ()
459 -- mark any type class arguments as injective
460 mapM_ checkIfInjective (map snd ns)
461 unifyProblems -- try again with the new information,
462 -- to help with disambiguation
463 -- Sort so that the implicit tactics and alternatives go last
464 let (ns', eargs) = unzip $
465 sortBy cmpArg (zip ns args)
466 elabArgs ist (ina || not isinf, guarded, inty)
467 [] fc False f ns'
468 (f == sUN "Force")
469 (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
470 solve
471 ivs' <- get_instances
472 -- Attempt to resolve any type classes which have 'complete' types,
473 -- i.e. no holes in them
474 when (not pattern || (ina && not tcgen && not guarded)) $
475 mapM_ (\n -> do focus n
476 g <- goal
477 env <- get_env
478 hs <- get_holes
479 if all (\n -> not (n `elem` hs)) (freeNames g)
480 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
481 then try (resolveTC 7 g fn ist)
482 (movelast n)
483 else movelast n)
484 (ivs' \\ ivs)
485 where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
486 -- reason for lambdas after alternatives is that having
487 -- the alternative resolved can help with typechecking the lambda
488 -- or the rewrite. Rewrites/tactics need as much information
489 -- as possible about the type.
490 -- FIXME: Better would be to allow alternative resolution to be
491 -- retried after more information is in.
492 cmpArg (_, x) (_, y)
493 = compare (conDepth 0 (getTm x) + priority x + alt x)
494 (conDepth 0 (getTm y) + priority y + alt y)
495 where alt t = case getTm t of
496 PAlternative False _ -> 5
497 PAlternative True _ -> 1
498 PLam _ _ _ -> 2
499 PRewrite _ _ _ _ -> 3
500 _ -> 0
502 -- Score a point for every level where there is a non-constructor
503 -- function (so higher score --> done later)
504 -- Only relevant when on lhs
505 conDepth d t | not pattern = 0
506 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
507 | otherwise = max (100 - d) 1
508 conDepth d (PApp _ f as)
509 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
510 conDepth d (PPatvar _ _) = 0
511 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
512 conDepth d Placeholder = 0
513 conDepth d t = max (100 - d) 1
515 checkIfInjective n = do
516 env <- get_env
517 case lookup n env of
518 Nothing -> return ()
519 Just b ->
520 case unApply (binderTy b) of
521 (P _ c _, args) ->
522 case lookupCtxt c (idris_classes ist) of
523 [] -> return ()
524 _ -> -- type class, set as injective
525 mapM_ setinjArg args
526 _ -> return ()
528 setinjArg (P _ n _) = setinj n
529 setinjArg _ = return ()
531 tacTm (PTactics _) = True
532 tacTm (PProof _) = True
533 tacTm _ = False
535 setInjective (PRef _ n) = setinj n
536 setInjective (PApp _ (PRef _ n) _) = setinj n
537 setInjective _ = return ()
539 elab' ina@(_, a, inty) tm@(PApp fc f [arg])
540 = erun fc $
541 do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
542 (show tm)
543 solve
544 elab' ina Placeholder = do (h : hs) <- get_holes
545 movelast h
546 elab' ina (PMetavar n) = let n' = mkN n in
547 do attack; defer n'; solve
548 where mkN n@(NS _ _) = n
549 mkN n = case namespace info of
550 Just xs@(_:_) -> sNS n xs
551 _ -> n
552 elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts
553 elab' ina (PTactics ts)
554 | not pattern = do mapM_ (runTac False ist fn) ts
555 | otherwise = elab' ina Placeholder
556 elab' ina (PElabError e) = fail (pshow ist e)
557 elab' ina (PRewrite fc r sc newg)
558 = do attack
559 tyn <- getNameFrom (sMN 0 "rty")
560 claim tyn RType
561 valn <- getNameFrom (sMN 0 "rval")
562 claim valn (Var tyn)
563 letn <- getNameFrom (sMN 0 "rewrite_rule")
564 letbind letn (Var tyn) (Var valn)
565 focus valn
566 elab' ina r
567 compute
568 g <- goal
569 rewrite (Var letn)
570 g' <- goal
571 when (g == g') $ lift $ tfail (NoRewriting g)
572 case newg of
573 Nothing -> elab' ina sc
574 Just t -> doEquiv t sc
575 solve
576 where doEquiv t sc =
577 do attack
578 tyn <- getNameFrom (sMN 0 "ety")
579 claim tyn RType
580 valn <- getNameFrom (sMN 0 "eqval")
581 claim valn (Var tyn)
582 letn <- getNameFrom (sMN 0 "equiv_val")
583 letbind letn (Var tyn) (Var valn)
584 focus tyn
585 elab' ina t
586 focus valn
587 elab' ina sc
588 elab' ina (PRef fc letn)
589 solve
590 elab' ina@(_, a, inty) c@(PCase fc scr opts)
591 = do attack
592 tyn <- getNameFrom (sMN 0 "scty")
593 claim tyn RType
594 valn <- getNameFrom (sMN 0 "scval")
595 scvn <- getNameFrom (sMN 0 "scvar")
596 claim valn (Var tyn)
597 letbind scvn (Var tyn) (Var valn)
598 focus valn
599 elabE (True, a, inty) scr
600 args <- get_env
601 cname <- unique_hole' True (mkCaseName fn)
602 let cname' = mkN cname
603 elab' ina (PMetavar cname')
604 -- if the scrutinee is one of the 'args' in env, we should
605 -- inspect it directly, rather than adding it as a new argument
606 let newdef = PClauses fc [] cname'
607 (caseBlock fc cname'
608 (map (isScr scr) (reverse args)) opts)
609 -- elaborate case
610 env <- get_env
611 updateAux (newdef : )
612 -- if we haven't got the type yet, hopefully we'll get it later!
613 movelast tyn
614 solve
615 where mkCaseName (NS n ns) = NS (mkCaseName n) ns
616 mkCaseName n = SN (CaseN n)
617-- mkCaseName (UN x) = UN (x ++ "_case")
618-- mkCaseName (MN i x) = MN i (x ++ "_case")
619 mkN n@(NS _ _) = n
620 mkN n = case namespace info of
621 Just xs@(_:_) -> sNS n xs
622 _ -> n
623 elab' ina (PUnifyLog t) = do unifyLog True
624 elab' ina t
625 unifyLog False
626 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
628 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
629 isScr (PRef _ n) (n', b) = (n', (n == n', b))
630 isScr _ (n', b) = (n', (False, b))
632 caseBlock :: FC -> Name ->
633 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
634 caseBlock fc n env opts
635 = let args' = findScr env
636 args = map mkarg (map getNmScr args') in
637 map (mkClause args) opts
639 where -- Find the variable we want as the scrutinee and mark it as
640 -- 'True'. If the scrutinee is in the environment, match on that
641 -- otherwise match on the new argument we're adding.
642 findScr ((n, (True, t)) : xs)
643 = (n, (True, t)) : scrName n xs
644 findScr [(n, (_, t))] = [(n, (True, t))]
645 findScr (x : xs) = x : findScr xs
646 -- [] can't happen since scrutinee is in the environment!
648 -- To make sure top level pattern name remains in scope, put
649 -- it at the end of the environment
650 scrName n [] = []
651 scrName n [(_, t)] = [(n, t)]
652 scrName n (x : xs) = x : scrName n xs
654 getNmScr (n, (s, _)) = (n, s)
656 mkarg (n, s) = (PRef fc n, s)
657 -- may be shadowed names in the new pattern - so replace the
658 -- old ones with an _
659 mkClause args (l, r)
660 = let args' = map (shadowed (allNamesIn l)) args
661 lhs = PApp (getFC fc l) (PRef (getFC fc l) n)
662 (map (mkLHSarg l) args') in
663 PClause (getFC fc l) n lhs [] r []
665 mkLHSarg l (tm, True) = pexp l
666 mkLHSarg l (tm, False) = pexp tm
668 shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)
669 shadowed new t = t
671 getFC d (PApp fc _ _) = fc
672 getFC d (PRef fc _) = fc
673 getFC d (PAlternative _ (x:_)) = getFC d x
674 getFC d x = d
676 insertLazy :: PTerm -> ElabD PTerm
677 insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t
678 insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t
679 insertLazy (PCoerced t) = return t
680 insertLazy t =
681 do ty <- goal
682 env <- get_env
683 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
684 let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]
685 case tyh of
686 P _ (UN l) _ | l == txt "Lazy'"
687 -> return (PAlternative False tries)
688 _ -> return t
689 where
690 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)
691 mkDelay t = let fc = fileFC "Delay" in
692 addImpl ist (PApp fc (PRef fc (sUN "Delay"))
693 [pexp t])
695 insertCoerce ina t =
696 do ty <- goal
697 -- Check for possible coercions to get to the goal
698 -- and add them as 'alternatives'
699 env <- get_env
700 let ty' = normalise (tt_ctxt ist) env ty
701 let cs = getCoercionsTo ist ty'
702 let t' = case (t, cs) of
703 (PCoerced tm, _) -> tm
704 (_, []) -> t
705 (_, cs) -> PAlternative False [t ,
706 PAlternative True (map (mkCoerce t) cs)]
707 return t'
708 where
709 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!
710 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])
712 -- | Elaborate the arguments to a function
713 elabArgs :: IState -- ^ The current Idris state
714 -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
715 -> [Bool]
716 -> FC -- ^ Source location
717 -> Bool
718 -> Name -- ^ Name of the function being applied
719 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)
720 -> Bool -- ^ under a 'force'
721 -> [(Bool, PTerm)] -- ^ (Laziness, argument)
722 -> ElabD ()
723 elabArgs ist ina failed fc retry f [] force _ = return ()
724 elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)
725 = elabArgs ist ina failed fc r f ns force args
726 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
727 | lazy && not pattern
728 = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))
729 [pimp (sUN "a") Placeholder True,
730 pexp t])
731 | otherwise = elabArg argName holeName t
732 where elabArg argName holeName t =
733 do now_elaborating fc f argName
734 wrapErr f argName $ do
735 hs <- get_holes
736 tm <- get_term
737 -- No coercing under an explicit Force (or it can Force/Delay
738 -- recursively!)
739 let elab = if force then elab' else elabE
740 failed' <- -- trace (show (n, t, hs, tm)) $
741 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
742 case holeName `elem` hs of
743 True -> do focus holeName; elab ina t; return failed
744 False -> return failed
745 done_elaborating_arg f argName
746 elabArgs ist ina failed fc r f ns force args
747 wrapErr f argName action =
748 do elabState <- get
749 while <- elaborating_app
750 let while' = map (\(x, y, z)-> (y, z)) while
751 (result, newState) <- case runStateT action elabState of
752 OK (res, newState) -> return (res, newState)
753 Error e -> do done_elaborating_arg f argName
754 lift (tfail (elaboratingArgErr while' e))
755 put newState
756 return result
759-- For every alternative, look at the function at the head. Automatically resolve
760-- any nested alternatives where that function is also at the head
762pruneAlt :: [PTerm] -> [PTerm]
763pruneAlt xs = map prune xs
764 where
765 prune (PApp fc1 (PRef fc2 f) as)
766 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
767 prune t = t
769 choose f (PAlternative a as)
770 = let as' = fmap (choose f) as
771 fs = filter (headIs f) as' in
772 case fs of
773 [a] -> a
774 _ -> PAlternative a as'
776 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
777 choose f t = t
779 headIs f (PApp _ (PRef _ f') _) = f == f'
780 headIs f (PApp _ f' _) = headIs f f'
781 headIs f _ = True -- keep if it's not an application
783-- Rule out alternatives that don't return the same type as the head of the goal
784-- (If there are none left as a result, do nothing)
785pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
786pruneByType (P _ n _) c as
787-- if the goal type is polymorphic, keep e
788 | [] <- lookupTy n c = as
789 | otherwise
790 = let asV = filter (headIs True n) as
791 as' = filter (headIs False n) as in
792 case as' of
793 [] -> case asV of
794 [] -> as
795 _ -> asV
796 _ -> as'
797 where
798 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
799 headIs var f (PApp _ f' _) = headIs var f f'
800 headIs var f (PPi _ _ _ sc) = headIs var f sc
801 headIs _ _ _ = True -- keep if it's not an application
803 typeHead var f f'
804 = case lookupTy f' c of
805 [ty] -> let ty' = normalise c [] ty in
806 case unApply (getRetTy ty') of
807 (P _ ftyn _, _) -> ftyn == f
808 (V _, _) -> var -- keep, variable
809 _ -> False
810 _ -> False
812pruneByType t _ as = as
814findInstances :: IState -> Term -> [Name]
815findInstances ist t
816 | (P _ n _, _) <- unApply t
817 = case lookupCtxt n (idris_classes ist) of
818 [CI _ _ _ _ _ ins] -> ins
819 _ -> []
820 | otherwise = []
822trivial' ist
823 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist
824proofSearch' ist rec top n hints
825 = proofSearch rec (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist
828resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
829resolveTC = resTC' []
831resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"
832resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
833resTC' tcs depth topg fn ist
834 = do hnf_compute
835 g <- goal
836 ptm <- get_term
837 ulog <- getUnifyLog
838 hs <- get_holes
839 traceWhen ulog ("Resolving class " ++ show g) $
840 try' (trivial' ist)
841 (do t <- goal
842 let (tc, ttypes) = unApply t
843 scopeOnly <- needsDefault t tc ttypes
844 let insts_in = findInstances ist t
845 let insts = if scopeOnly then filter chaser insts_in
846 else insts_in
847 tm <- get_term
848 let depth' = if scopeOnly then 2 else depth
849 blunderbuss t depth' insts) True
850 where
851 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
852 | otherwise = (fail "Can't resolve", show n)
854 -- HACK! Rather than giving a special name, better to have some kind
855 -- of flag in ClassInfo structure
856 chaser (UN nm)
857 | ('@':'@':_) <- str nm = True -- old way
858 chaser (SN (ParentN _ _)) = True
859 chaser (NS n _) = chaser n
860 chaser _ = False
862 numclass = sNS (sUN "Num") ["Classes","Prelude"]
864 needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass
865 = do focus a
866 fill (RConstant (AType (ATInt ITBig))) -- default Integer
867 solve
868 return False
869 needsDefault t f as
870 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t
871 needsDefault t f a = return False -- trace (show t) $ return ()
873 boundVar (P Bound _ _) = True
874 boundVar _ = False
876 blunderbuss t d [] = do -- c <- get_env
877 -- ps <- get_probs
878 lift $ tfail $ CantResolve topg
879 blunderbuss t d (n:ns)
880 | n /= fn && tcname n = try' (resolve n d)
881 (blunderbuss t d ns) True
882 | otherwise = blunderbuss t d ns
884 resolve n depth
885 | depth == 0 = fail $ "Can't resolve type class"
886 | otherwise
887 = do t <- goal
888 let (tc, ttypes) = unApply t
889-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
890-- else do
891 -- if there's a hole in the goal, don't even try
892 let imps = case lookupCtxtName n (idris_implicits ist) of
893 [] -> []
894 [args] -> map isImp (snd args) -- won't be overloaded!
895 ps <- get_probs
896 tm <- get_term
897 args <- map snd <$> try' (apply (Var n) imps)
898 (match_apply (Var n) imps) True
899 ps' <- get_probs
900 when (length ps < length ps') $ fail "Can't apply type class"
901-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
902 mapM_ (\ (_,n) -> do focus n
903 t' <- goal
904 let (tc', ttype) = unApply t'
905 let got = fst (unApply t)
906 let depth' = if tc' `elem` tcs
907 then depth - 1 else depth
908 resTC' (got : tcs) depth' topg fn ist)
909 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
910 -- if there's any arguments left, we've failed to resolve
911 hs <- get_holes
912 ulog <- getUnifyLog
913 solve
914 traceWhen ulog ("Got " ++ show n) $ return ()
915 where isImp (PImp p _ _ _ _) = (True, p)
916 isImp arg = (False, priority arg)
918collectDeferred :: Maybe Name ->
919 Term -> State [(Name, (Int, Maybe Name, Type))] Term
920collectDeferred top (Bind n (GHole i t) app) =
921 do ds <- get
922 t' <- collectDeferred top t
923 when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
924 collectDeferred top app
925collectDeferred top (Bind n b t) = do b' <- cdb b
926 t' <- collectDeferred top t
927 return (Bind n b' t')
928 where
929 cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
930 cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
931 cdb b = do ty' <- collectDeferred top (binderTy b)
932 return (b { binderTy = ty' })
933collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
934collectDeferred top t = return t
936-- Running tactics directly
937-- if a tactic adds unification problems, return an error
939runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
940runTac autoSolve ist fn tac
941 = do env <- get_env
942 g <- goal
943 if autoSolve
944 then runT (fmap (addImplBound ist (map fst env)) tac)
945 else no_errors (runT (fmap (addImplBound ist (map fst env)) tac))
946 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
947 where
948 runT (Intro []) = do g <- goal
949 attack; intro (bname g)
950 where
951 bname (Bind n _ _) = Just n
952 bname _ = Nothing
953 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
954 runT Intros = do g <- goal
955 attack; intro (bname g)
956 try' (runT Intros)
957 (return ()) True
958 where
959 bname (Bind n _ _) = Just n
960 bname _ = Nothing
961 runT (Exact tm) = do elab ist toplevel False [] (sMN 0 "tac") tm
962 when autoSolve solveAll
963 runT (MatchRefine fn)
964 = do fnimps <-
965 case lookupCtxtName fn (idris_implicits ist) of
966 [] -> do a <- envArgs fn
967 return [(fn, a)]
968 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
969 let tacs = map (\ (fn', imps) ->
970 (match_apply (Var fn') (map (\x -> (x, 0)) imps),
971 show fn')) fnimps
972 tryAll tacs
973 when autoSolve solveAll
974 where envArgs n = do e <- get_env
975 case lookup n e of
976 Just t -> return $ map (const False)
977 (getArgTys (binderTy t))
978 _ -> return []
979 runT (Refine fn [])
980 = do fnimps <-
981 case lookupCtxtName fn (idris_implicits ist) of
982 [] -> do a <- envArgs fn
983 return [(fn, a)]
984 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
985 let tacs = map (\ (fn', imps) ->
986 (apply (Var fn') (map (\x -> (x, 0)) imps),
987 show fn')) fnimps
988 tryAll tacs
989 when autoSolve solveAll
990 where isImp (PImp _ _ _ _ _) = True
991 isImp _ = False
992 envArgs n = do e <- get_env
993 case lookup n e of
994 Just t -> return $ map (const False)
995 (getArgTys (binderTy t))
996 _ -> return []
997 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
998 when autoSolve solveAll
999 runT DoUnify = do unify_all
1000 when autoSolve solveAll
1001 runT (Equiv tm) -- let bind tm, then
1002 = do attack
1003 tyn <- getNameFrom (sMN 0 "ety")
1004 claim tyn RType
1005 valn <- getNameFrom (sMN 0 "eqval")
1006 claim valn (Var tyn)
1007 letn <- getNameFrom (sMN 0 "equiv_val")
1008 letbind letn (Var tyn) (Var valn)
1009 focus tyn
1010 elab ist toplevel False [] (sMN 0 "tac") tm
1011 focus valn
1012 when autoSolve solveAll
1013 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
1014 = do attack; -- (h:_) <- get_holes
1015 tyn <- getNameFrom (sMN 0 "rty")
1016 -- start_unify h
1017 claim tyn RType
1018 valn <- getNameFrom (sMN 0 "rval")
1019 claim valn (Var tyn)
1020 letn <- getNameFrom (sMN 0 "rewrite_rule")
1021 letbind letn (Var tyn) (Var valn)
1022 focus valn
1023 elab ist toplevel False [] (sMN 0 "tac") tm
1024 rewrite (Var letn)
1025 when autoSolve solveAll
1026 runT (Induction nm)
1027 = do induction nm
1028 when autoSolve solveAll
1029 runT (LetTac n tm)
1030 = do attack
1031 tyn <- getNameFrom (sMN 0 "letty")
1032 claim tyn RType
1033 valn <- getNameFrom (sMN 0 "letval")
1034 claim valn (Var tyn)
1035 letn <- unique_hole n
1036 letbind letn (Var tyn) (Var valn)
1037 focus valn
1038 elab ist toplevel False [] (sMN 0 "tac") tm
1039 when autoSolve solveAll
1040 runT (LetTacTy n ty tm)
1041 = do attack
1042 tyn <- getNameFrom (sMN 0 "letty")
1043 claim tyn RType
1044 valn <- getNameFrom (sMN 0 "letval")
1045 claim valn (Var tyn)
1046 letn <- unique_hole n
1047 letbind letn (Var tyn) (Var valn)
1048 focus tyn
1049 elab ist toplevel False [] (sMN 0 "tac") ty
1050 focus valn
1051 elab ist toplevel False [] (sMN 0 "tac") tm
1052 when autoSolve solveAll
1053 runT Compute = compute
1054 runT Trivial = do trivial' ist; when autoSolve solveAll
1055 runT TCInstance = runT (Exact (PResolveTC emptyFC))
1056 runT (ProofSearch rec top hints)
1057 = do proofSearch' ist rec top fn hints; when autoSolve solveAll
1058 runT (Focus n) = focus n
1059 runT Solve = solve
1060 runT (Try l r) = do try' (runT l) (runT r) True
1061 runT (TSeq l r) = do runT l; runT r
1062 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
1063 tgoal <- goal -- store the goal
1064 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
1065 script <- getNameFrom (sMN 0 "script")
1066 claim script scriptTy
1067 scriptvar <- getNameFrom (sMN 0 "scriptvar" )
1068 letbind scriptvar scriptTy (Var script)
1069 focus script
1070 elab ist toplevel False [] (sMN 0 "tac") tm
1071 (script', _) <- get_type_val (Var scriptvar)
1072 -- now that we have the script apply
1073 -- it to the reflected goal and context
1074 restac <- getNameFrom (sMN 0 "restac")
1075 claim restac tacticTy
1076 focus restac
1077 fill (raw_apply (forget script')
1078 [reflectEnv tenv, reflect tgoal])
1079 restac' <- get_guess
1080 solve
1081 -- normalise the result in order to
1082 -- reify it
1083 ctxt <- get_context
1084 env <- get_env
1085 let tactic = normalise ctxt env restac'
1086 runReflected tactic
1087 where tacticTy = Var (reflm "Tactic")
1088 listTy = Var (sNS (sUN "List") ["List", "Prelude"])
1089 scriptTy = (RBind (sMN 0 "__pi_arg")
1090 (Pi (RApp listTy envTupleType))
1091 (RBind (sMN 1 "__pi_arg")
1092 (Pi (Var $ reflm "TT")) tacticTy))
1093 runT (ByReflection tm) -- run the reflection function 'tm' on the
1094 -- goal, then apply the resulting reflected Tactic
1095 = do tgoal <- goal
1096 attack
1097 script <- getNameFrom (sMN 0 "script")
1098 claim script scriptTy
1099 scriptvar <- getNameFrom (sMN 0 "scriptvar" )
1100 letbind scriptvar scriptTy (Var script)
1101 focus script
1102 ptm <- get_term
1103 elab ist toplevel False [] (sMN 0 "tac")
1104 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
1105 (script', _) <- get_type_val (Var scriptvar)
1106 -- now that we have the script apply
1107 -- it to the reflected goal
1108 restac <- getNameFrom (sMN 0 "restac")
1109 claim restac tacticTy
1110 focus restac
1111 fill (forget script')
1112 restac' <- get_guess
1113 solve
1114 -- normalise the result in order to
1115 -- reify it
1116 ctxt <- get_context
1117 env <- get_env
1118 let tactic = normalise ctxt env restac'
1119 runReflected tactic
1120 where tacticTy = Var (reflm "Tactic")
1121 scriptTy = tacticTy
1123 runT (Reflect v) = do attack -- let x = reflect v in ...
1124 tyn <- getNameFrom (sMN 0 "letty")
1125 claim tyn RType
1126 valn <- getNameFrom (sMN 0 "letval")
1127 claim valn (Var tyn)
1128 letn <- getNameFrom (sMN 0 "letvar")
1129 letbind letn (Var tyn) (Var valn)
1130 focus valn
1131 elab ist toplevel False [] (sMN 0 "tac") v
1132 (value, _) <- get_type_val (Var letn)
1133 ctxt <- get_context
1134 env <- get_env
1135 let value' = hnf ctxt env value
1136 runTac autoSolve ist fn (Exact $ PQuote (reflect value'))
1137 runT (Fill v) = do attack -- let x = fill x in ...
1138 tyn <- getNameFrom (sMN 0 "letty")
1139 claim tyn RType
1140 valn <- getNameFrom (sMN 0 "letval")
1141 claim valn (Var tyn)
1142 letn <- getNameFrom (sMN 0 "letvar")
1143 letbind letn (Var tyn) (Var valn)
1144 focus valn
1145 elab ist toplevel False [] (sMN 0 "tac") v
1146 (value, _) <- get_type_val (Var letn)
1147 ctxt <- get_context
1148 env <- get_env
1149 let value' = normalise ctxt env value
1150 rawValue <- reifyRaw value'
1151 runTac autoSolve ist fn (Exact $ PQuote rawValue)
1152 runT (GoalType n tac) = do g <- goal
1153 case unApply g of
1154 (P _ n' _, _) ->
1155 if nsroot n' == sUN n
1156 then runT tac
1157 else fail "Wrong goal type"
1158 _ -> fail "Wrong goal type"
1159 runT ProofState = do g <- goal
1160 return ()
1161 runT x = fail $ "Not implemented " ++ show x
1163 runReflected t = do t' <- reify ist t
1164 runTac autoSolve ist fn t'
1166-- | Prefix a name with the "Language.Reflection" namespace
1167reflm :: String -> Name
1168reflm n = sNS (sUN n) ["Reflection", "Language"]
1171-- | Reify tactics from their reflected representation
1172reify :: IState -> Term -> ElabD PTactic
1173reify _ (P _ n _) | n == reflm "Intros" = return Intros
1174reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
1175reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
1176reify _ (P _ n _) | n == reflm "Solve" = return Solve
1177reify _ (P _ n _) | n == reflm "Compute" = return Compute
1178reify ist t@(App _ _)
1179 | (P _ f _, args) <- unApply t = reifyApp ist f args
1180reify _ t = fail ("Unknown tactic " ++ show t)
1182reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
1183reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1184reifyApp _ t [x]
1185 | t == reflm "Refine" = do n <- reifyTTName x
1186 return $ Refine n []
1187reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
1188reifyApp ist t [Constant (Str n), x]
1189 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1190reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1191reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)
1192reifyApp ist t [t']
1193 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
1194reifyApp ist t [t']
1195 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
1196reifyApp ist t [t']
1197 | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
1198reifyApp _ t [t']
1199 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
1200reifyApp ist t [t']
1201 | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
1202reifyApp ist t [x]
1203 | t == reflm "Focus" = liftM Focus (reifyTTName x)
1204reifyApp ist t [t']
1205 | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
1206reifyApp ist t [n, t']
1207 | t == reflm "LetTac" = do n' <- reifyTTName n
1208 t'' <- reifyTT t'
1209 return $ LetTac n' (delab ist t')
1210reifyApp ist t [n, tt', t']
1211 | t == reflm "LetTacTy" = do n' <- reifyTTName n
1212 tt'' <- reifyTT tt'
1213 t'' <- reifyTT t'
1214 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
1215reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
1217-- | Reify terms from their reflected representation
1218reifyTT :: Term -> ElabD Term
1219reifyTT t@(App _ _)
1220 | (P _ f _, args) <- unApply t = reifyTTApp f args
1221reifyTT t@(P _ n _)
1222 | n == reflm "Erased" = return $ Erased
1223reifyTT t@(P _ n _)
1224 | n == reflm "Impossible" = return $ Impossible
1225reifyTT t = fail ("Unknown reflection term: " ++ show t)
1227reifyTTApp :: Name -> [Term] -> ElabD Term
1228reifyTTApp t [nt, n, x]
1229 | t == reflm "P" = do nt' <- reifyTTNameType nt
1230 n' <- reifyTTName n
1231 x' <- reifyTT x
1232 return $ P nt' n' x'
1233reifyTTApp t [Constant (I i)]
1234 | t == reflm "V" = return $ V i
1235reifyTTApp t [n, b, x]
1236 | t == reflm "Bind" = do n' <- reifyTTName n
1237 b' <- reifyTTBinder reifyTT (reflm "TT") b
1238 x' <- reifyTT x
1239 return $ Bind n' b' x'
1240reifyTTApp t [f, x]
1241 | t == reflm "App" = do f' <- reifyTT f
1242 x' <- reifyTT x
1243 return $ App f' x'
1244reifyTTApp t [c]
1245 | t == reflm "TConst" = liftM Constant (reifyTTConst c)
1246reifyTTApp t [t', Constant (I i)]
1247 | t == reflm "Proj" = do t'' <- reifyTT t'
1248 return $ Proj t'' i
1249reifyTTApp t [tt]
1250 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
1251reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
1253-- | Reify raw terms from their reflected representation
1254reifyRaw :: Term -> ElabD Raw
1255reifyRaw t@(App _ _)
1256 | (P _ f _, args) <- unApply t = reifyRawApp f args
1257reifyRaw t@(P _ n _)
1258 | n == reflm "RType" = return $ RType
1259reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)
1261reifyRawApp :: Name -> [Term] -> ElabD Raw
1262reifyRawApp t [n]
1263 | t == reflm "Var" = liftM Var (reifyTTName n)
1264reifyRawApp t [n, b, x]
1265 | t == reflm "RBind" = do n' <- reifyTTName n
1266 b' <- reifyTTBinder reifyRaw (reflm "Raw") b
1267 x' <- reifyRaw x
1268 return $ RBind n' b' x'
1269reifyRawApp t [f, x]
1270 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
1271reifyRawApp t [t']
1272 | t == reflm "RForce" = liftM RForce (reifyRaw t')
1273reifyRawApp t [c]
1274 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
1275reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))
1277reifyTTName :: Term -> ElabD Name
1278reifyTTName t
1279 | (P _ f _, args) <- unApply t = reifyTTNameApp f args
1280reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
1282reifyTTNameApp :: Name -> [Term] -> ElabD Name
1283reifyTTNameApp t [Constant (Str n)]
1284 | t == reflm "UN" = return $ sUN n
1285reifyTTNameApp t [n, ns]
1286 | t == reflm "NS" = do n' <- reifyTTName n
1287 ns' <- reifyTTNamespace ns
1288 return $ sNS n' ns'
1289reifyTTNameApp t [Constant (I i), Constant (Str n)]
1290 | t == reflm "MN" = return $ sMN i n
1291reifyTTNameApp t []
1292 | t == reflm "NErased" = return NErased
1293reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
1295reifyTTNamespace :: Term -> ElabD [String]
1296reifyTTNamespace t@(App _ _)
1297 = case unApply t of
1298 (P _ f _, [Constant StrType])
1299 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
1300 (P _ f _, [Constant StrType, Constant (Str n), ns])
1301 | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
1302 _ -> fail ("Unknown reflection namespace arg: " ++ show t)
1303reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
1305reifyTTNameType :: Term -> ElabD NameType
1306reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
1307reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
1308reifyTTNameType t@(App _ _)
1309 = case unApply t of
1310 (P _ f _, [Constant (I tag), Constant (I num)])
1311 | f == reflm "DCon" -> return $ DCon tag num
1312 | f == reflm "TCon" -> return $ TCon tag num
1313 _ -> fail ("Unknown reflection name type: " ++ show t)
1314reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
1316reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
1317reifyTTBinder reificator binderType t@(App _ _)
1318 = case unApply t of
1319 (P _ f _, bt:args) | forget bt == Var binderType
1320 -> reifyTTBinderApp reificator f args
1321 _ -> fail ("Mismatching binder reflection: " ++ show t)
1322reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
1324reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
1325reifyTTBinderApp reif f [t]
1326 | f == reflm "Lam" = liftM Lam (reif t)
1327reifyTTBinderApp reif f [t]
1328 | f == reflm "Pi" = liftM Pi (reif t)
1329reifyTTBinderApp reif f [x, y]
1330 | f == reflm "Let" = liftM2 Let (reif x) (reif y)
1331reifyTTBinderApp reif f [x, y]
1332 | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
1333reifyTTBinderApp reif f [t]
1334 | f == reflm "Hole" = liftM Hole (reif t)
1335reifyTTBinderApp reif f [t]
1336 | f == reflm "GHole" = liftM (GHole 0) (reif t)
1337reifyTTBinderApp reif f [x, y]
1338 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
1339reifyTTBinderApp reif f [t]
1340 | f == reflm "PVar" = liftM PVar (reif t)
1341reifyTTBinderApp reif f [t]
1342 | f == reflm "PVTy" = liftM PVTy (reif t)
1343reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
1345reifyTTConst :: Term -> ElabD Const
1346reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative))
1347reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig))
1348reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat)
1349reifyTTConst (P _ n _) | n == reflm "ChType" = return (AType (ATInt ITChar))
1350reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
1351reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8)))
1352reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16)))
1353reifyTTConst (P _ n _) | n == reflm "B32Type" = return (AType (ATInt (ITFixed IT32)))
1354reifyTTConst (P _ n _) | n == reflm "B64Type" = return (AType (ATInt (ITFixed IT64)))
1355reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
1356reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
1357reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
1358reifyTTConst t@(App _ _)
1359 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
1360reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
1362reifyTTConstApp :: Name -> Term -> ElabD Const
1363reifyTTConstApp f (Constant c@(I _))
1364 | f == reflm "I" = return $ c
1365reifyTTConstApp f (Constant c@(BI _))
1366 | f == reflm "BI" = return $ c
1367reifyTTConstApp f (Constant c@(Fl _))
1368 | f == reflm "Fl" = return $ c
1369reifyTTConstApp f (Constant c@(I _))
1370 | f == reflm "Ch" = return $ c
1371reifyTTConstApp f (Constant c@(Str _))
1372 | f == reflm "Str" = return $ c
1373reifyTTConstApp f (Constant c@(B8 _))
1374 | f == reflm "B8" = return $ c
1375reifyTTConstApp f (Constant c@(B16 _))
1376 | f == reflm "B16" = return $ c
1377reifyTTConstApp f (Constant c@(B32 _))
1378 | f == reflm "B32" = return $ c
1379reifyTTConstApp f (Constant c@(B64 _))
1380 | f == reflm "B64" = return $ c
1381reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
1383reifyTTUExp :: Term -> ElabD UExp
1384reifyTTUExp t@(App _ _)
1385 = case unApply t of
1386 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
1387 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
1388 _ -> fail ("Unknown reflection type universe expression: " ++ show t)
1389reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
1391-- | Create a reflected call to a named function/constructor
1392reflCall :: String -> [Raw] -> Raw
1393reflCall funName args
1394 = raw_apply (Var (reflm funName)) args
1396-- | Lift a term into its Language.Reflection.TT representation
1397reflect :: Term -> Raw
1398reflect (P nt n t)
1399 = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
1400reflect (V n)
1401 = reflCall "V" [RConstant (I n)]
1402reflect (Bind n b x)
1403 = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
1404reflect (App f x)
1405 = reflCall "App" [reflect f, reflect x]
1406reflect (Constant c)
1407 = reflCall "TConst" [reflectConstant c]
1408reflect (Proj t i)
1409 = reflCall "Proj" [reflect t, RConstant (I i)]
1410reflect (Erased) = Var (reflm "Erased")
1411reflect (Impossible) = Var (reflm "Impossible")
1412reflect (TType exp) = reflCall "TType" [reflectUExp exp]
1414reflectNameType :: NameType -> Raw
1415reflectNameType (Bound) = Var (reflm "Bound")
1416reflectNameType (Ref) = Var (reflm "Ref")
1417reflectNameType (DCon x y)
1418 = reflCall "DCon" [RConstant (I x), RConstant (I y)]
1419reflectNameType (TCon x y)
1420 = reflCall "TCon" [RConstant (I x), RConstant (I y)]
1422reflectName :: Name -> Raw
1423reflectName (UN s)
1424 = reflCall "UN" [RConstant (Str (str s))]
1425reflectName (NS n ns)
1426 = reflCall "NS" [ reflectName n
1427 , foldr (\ n s ->
1428 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
1429 [ RConstant StrType, RConstant (Str n), s ])
1430 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
1431 [ RConstant StrType ])
1432 (map str ns)
1434reflectName (MN i n)
1435 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
1436reflectName (NErased) = Var (reflm "NErased")
1437reflectName n = Var (reflm "NErased") -- special name, not yet implemented
1439reflectBinder :: Binder Term -> Raw
1440reflectBinder (Lam t)
1441 = reflCall "Lam" [Var (reflm "TT"), reflect t]
1442reflectBinder (Pi t)
1443 = reflCall "Pi" [Var (reflm "TT"), reflect t]
1444reflectBinder (Let x y)
1445 = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
1446reflectBinder (NLet x y)
1447 = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
1448reflectBinder (Hole t)
1449 = reflCall "Hole" [Var (reflm "TT"), reflect t]
1450reflectBinder (GHole _ t)
1451 = reflCall "GHole" [Var (reflm "TT"), reflect t]
1452reflectBinder (Guess x y)
1453 = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
1454reflectBinder (PVar t)
1455 = reflCall "PVar" [Var (reflm "TT"), reflect t]
1456reflectBinder (PVTy t)
1457 = reflCall "PVTy" [Var (reflm "TT"), reflect t]
1459reflectConstant :: Const -> Raw
1460reflectConstant c@(I _) = reflCall "I" [RConstant c]
1461reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
1462reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
1463reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
1464reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
1465reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")
1466reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")
1467reflectConstant (AType ATFloat) = Var (reflm "FlType")
1468reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType")
1469reflectConstant (StrType) = Var (reflm "StrType")
1470reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
1471reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
1472reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
1473reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
1474reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type")
1475reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")
1476reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")
1477reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")
1478reflectConstant (PtrType) = Var (reflm "PtrType")
1479reflectConstant (VoidType) = Var (reflm "VoidType")
1480reflectConstant (Forgot) = Var (reflm "Forgot")
1482reflectUExp :: UExp -> Raw
1483reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
1484reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
1486-- | Reflect the environment of a proof into a List (TTName, Binder TT)
1487reflectEnv :: Env -> Raw
1488reflectEnv = foldr consToEnvList emptyEnvList
1489 where
1490 consToEnvList :: (Name, Binder Term) -> Raw -> Raw
1491 consToEnvList (n, b) l
1492 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
1493 [ envTupleType
1494 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
1495 , (RApp (Var $ reflm "Binder")
1496 (Var $ reflm "TT"))
1497 , reflectName n
1498 , reflectBinder b
1500 , l
1503 emptyEnvList :: Raw
1504 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
1505 [envTupleType]
1507-- | Reflect an error into the internal datatype of Idris -- TODO
1508rawBool :: Bool -> Raw
1509rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
1510rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
1512rawNil :: Raw -> Raw
1513rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
1515rawCons :: Raw -> Raw -> Raw -> Raw
1516rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
1518rawList :: Raw -> [Raw] -> Raw
1519rawList ty = foldr (rawCons ty) (rawNil ty)
1521rawPairTy :: Raw -> Raw -> Raw
1522rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
1524rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
1525rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
1527reflectCtxt :: [(Name, Type)] -> Raw
1528reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
1529 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
1530 (reflectName n, reflect t)))
1531 ctxt)
1533reflectErr :: Err -> Raw
1534reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
1535reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
1536reflectErr (CantUnify b t1 t2 e ctxt i) =
1537 raw_apply (Var $ reflErrName "CantUnify")
1538 [ rawBool b
1539 , reflect t1
1540 , reflect t2
1541 , reflectErr e
1542 , reflectCtxt ctxt
1543 , RConstant (I i)]
1544reflectErr (InfiniteUnify n tm ctxt) =
1545 raw_apply (Var $ reflErrName "InfiniteUnify")
1546 [ reflectName n
1547 , reflect tm
1548 , reflectCtxt ctxt
1550reflectErr (CantConvert t t' ctxt) =
1551 raw_apply (Var $ reflErrName "CantConvert")
1552 [ reflect t
1553 , reflect t'
1554 , reflectCtxt ctxt
1556reflectErr (CantSolveGoal t ctxt) =
1557 raw_apply (Var $ reflErrName "CantSolveGoal")
1558 [ reflect t
1559 , reflectCtxt ctxt
1561reflectErr (UnifyScope n n' t ctxt) =
1562 raw_apply (Var $ reflErrName "UnifyScope")
1563 [ reflectName n
1564 , reflectName n'
1565 , reflect t
1566 , reflectCtxt ctxt
1568reflectErr (CantInferType str) =
1569 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
1570reflectErr (NonFunctionType t t') =
1571 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
1572reflectErr (NotEquality t t') =
1573 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
1574reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
1575reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
1576reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
1577reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
1578reflectErr (NotInjective t1 t2 t3) =
1579 raw_apply (Var $ reflErrName "NotInjective")
1580 [ reflect t1
1581 , reflect t2
1582 , reflect t3
1584reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
1585reflectErr (CantResolveAlts ss) =
1586 raw_apply (Var $ reflErrName "CantResolve")
1587 [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]
1588reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
1589reflectErr UniverseError = Var $ reflErrName "UniverseError"
1590reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
1591reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
1592reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
1593reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
1594reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
1595reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
1596reflectErr (ProviderError str) =
1597 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
1598reflectErr (LoadingFailed str err) =
1599 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
1600reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
1602elaboratingArgErr :: [(Name, Name)] -> Err -> Err
1603elaboratingArgErr [] err = err
1604elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
1605 where rewrite (ElaboratingArg _ _ _ _) = Nothing
1606 rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
1607 rewrite (At fc e) = fmap (At fc) (rewrite e)
1608 rewrite err = Just (ElaboratingArg f x during err)
1611withErrorReflection :: Idris a -> Idris a
1612withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1613 where handle :: Err -> Idris Err
1614 handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"
1615 return e -- Don't do meta-reflection of errors
1616 handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
1617 return e
1618 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
1619 handle e@(At fc err) = do logLvl 3 "Reflecting body of At"
1620 err' <- handle err
1621 return (At fc err')
1622 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
1623 err' <- handle err
1624 return (Elaborating what n err')
1625 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1626 hs <- getFnHandlers f a
1627 err' <- if null hs
1628 then handle err
1629 else applyHandlers err hs
1630 return (ElaboratingArg f a prev err')
1631 -- TODO: argument-specific error handlers go here for ElaboratingArg
1632 handle e = do ist <- getIState
1633 logLvl 2 "Starting error reflection"
1634 let handlers = idris_errorhandlers ist
1635 applyHandlers e handlers
1636 getFnHandlers :: Name -> Name -> Idris [Name]
1637 getFnHandlers f arg = do ist <- getIState
1638 let funHandlers = maybe M.empty id .
1639 lookupCtxtExact f .
1640 idris_function_errorhandlers $ ist
1641 return . maybe [] S.toList . M.lookup arg $ funHandlers
1644 applyHandlers e handlers =
1645 do ist <- getIState
1646 let err = fmap (errReverse ist) e
1647 logLvl 3 $ "Using reflection handlers " ++
1648 concat (intersperse ", " (map show handlers))
1649 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1651 -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1652 handlers <- case mapM (check (tt_ctxt ist) []) reports of
1653 Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1654 OK hs -> return hs
1656 -- Normalize error handler terms to produce the new messages
1657 ctxt <- getContext
1658 let results = map (normalise ctxt []) (map fst handlers)
1659 logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1661 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1662 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1663 errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1664 Left err -> ierror err
1665 Right ok -> return ok
1666 return $ case errorparts of
1667 [] -> e
1668 parts -> ReflectionError errorparts e
1670fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1671fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)
1672 | just == txt "Just" = Just tm
1673fromTTMaybe x = Nothing
1675reflErrName :: String -> Name
1676reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
1678-- | Attempt to reify a report part from TT to the internal
1679-- representation. Not in Idris or ElabD monads because it should be usable
1680-- from either.
1681reifyReportPart :: Term -> Either Err ErrorReportPart
1682reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =
1683 Right (TextPart msg)
1684reifyReportPart (App (P (DCon _ _) n _) ttn)
1685 | n == reflErrName "NamePart" =
1686 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of
1687 Error e -> Left . InternalMsg $
1688 "could not reify name term " ++
1689 show ttn ++
1690 " when reflecting an error:" ++ show e
1691 OK (n', _)-> Right $ NamePart n'
1692reifyReportPart (App (P (DCon _ _) n _) tm)
1693 | n == reflErrName "TermPart" =
1694 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of
1695 Error e -> Left . InternalMsg $
1696 "could not reify reflected term " ++
1697 show tm ++
1698 " when reflecting an error:" ++ show e
1699 OK (tm', _) -> Right $ TermPart tm'
1700reifyReportPart (App (P (DCon _ _) n _) tm)
1701 | n == reflErrName "SubReport" =
1702 case unList tm of
1703 Just xs -> do subParts <- mapM reifyReportPart xs
1704 Right (SubReport subParts)
1705 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
1706reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
1708envTupleType :: Raw
1709envTupleType
1710 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
1711 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
1714solveAll = try (do solve; solveAll) (return ())