git.iko.soy/Idris-dev
on 13ebfcf help sign in
Idris-dev/src/Idris/ElabTerm.hs
2758 lines 126 kB history raw
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
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, recheck)
18import Idris.ErrReverse (errReverse)
19import Idris.ElabQuasiquote (extractUnquotes)
20import Idris.Elab.Utils
21import qualified Util.Pretty as U
23import Control.Applicative ((<$>))
24import Control.Monad
25import Control.Monad.State.Strict
26import Data.List
27import qualified Data.Map as M
28import Data.Maybe (mapMaybe, fromMaybe)
29import qualified Data.Set as S
30import qualified Data.Text as T
31import Data.Vector.Unboxed (Vector)
32import qualified Data.Vector.Unboxed as V
34import Debug.Trace
36data ElabMode = ETyDecl | ELHS | ERHS
37 deriving Eq
39-- Using the elaborator, convert a term in raw syntax to a fully
40-- elaborated, typechecked term.
41--
42-- If building a pattern match, we convert undeclared variables from
43-- holes to pattern bindings.
45-- Also find deferred names in the term and their types
47build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
48 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
49build ist info emode opts fn tm
50 = do elab ist info emode opts fn tm
51 let tmIn = tm
52 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
53 [TIPartial] -> True
54 _ -> False
56 when (not pattern) $ solveAutos ist fn True
58 hs <- get_holes
59 ivs <- get_instances
60 ptm <- get_term
61 -- Resolve remaining type classes. Two passes - first to get the
62 -- default Num instances, second to clean up the rest
63 when (not pattern) $
64 mapM_ (\n -> when (n `elem` hs) $
65 do focus n
66 g <- goal
67 try (resolveTC True 7 g fn ist)
68 (movelast n)) ivs
69 ivs <- get_instances
70 hs <- get_holes
71 when (not pattern) $
72 mapM_ (\n -> when (n `elem` hs) $
73 do focus n
74 g <- goal
75 resolveTC True 7 g fn ist) ivs
76 tm <- get_term
77 ctxt <- get_context
78 probs <- get_probs
79 u <- getUnifyLog
80 hs <- get_holes
82 when (not pattern) $
83 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
84 "Remaining problems:\n" ++ qshow probs) $
85 do unify_all; matchProblems True; unifyProblems
87 probs <- get_probs
88 case probs of
89 [] -> return ()
90 ((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $
91 if inf then return ()
92 else lift (Error e)
94 when tydecl (do update_term orderPats
95 mkPat)
96-- update_term liftPats)
97 EState is _ <- getAux
98 tt <- get_term
99 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
100 log <- getLog
101 if (log /= "") then trace log $ return (tm, ds, is)
102 else return (tm, ds, is)
103 where pattern = emode == ELHS
104 tydecl = emode == ETyDecl
106 mkPat = do hs <- get_holes
107 tm <- get_term
108 case hs of
109 (h: hs) -> do patvar h; mkPat
110 [] -> return ()
112-- Build a term autogenerated as a typeclass method definition
113-- (Separate, so we don't go overboard resolving things that we don't
114-- know about yet on the LHS of a pattern def)
116buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
117 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
118buildTC ist info emode opts fn tm
119 = do -- set name supply to begin after highest index in tm
120 let ns = allNamesIn tm
121 let tmIn = tm
122 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
123 [TIPartial] -> True
124 _ -> False
125 initNextNameFrom ns
126 elab ist info emode opts fn tm
127 probs <- get_probs
128 tm <- get_term
129 case probs of
130 [] -> return ()
131 ((_,_,_,_,e,_,_):es) -> if inf then return ()
132 else lift (Error e)
133 dots <- get_dotterm
134 -- 'dots' are the PHidden things which have not been solved by
135 -- unification
136 when (not (null dots)) $
137 lift (Error (CantMatch (getInferTerm tm)))
138 EState is _ <- getAux
139 tt <- get_term
140 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
141 log <- getLog
142 if (log /= "") then trace log $ return (tm, ds, is)
143 else return (tm, ds, is)
144 where pattern = emode == ELHS
146-- return whether arguments of the given constructor name can be
147-- matched on. If they're polymorphic, no, unless the type has beed made
148-- concrete by the time we get around to elaborating the argument.
149getUnmatchable :: Context -> Name -> [Bool]
150getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
151 = case lookupTyExact n ctxt of
152 Nothing -> []
153 Just ty -> checkArgs [] [] ty
154 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
155 checkArgs env ns (Bind n (Pi _ t _) sc)
156 = let env' = case t of
157 TType _ -> n : env
158 _ -> env in
159 checkArgs env' (intersect env (refsIn t) : ns)
160 (instantiate (P Bound n t) sc)
161 checkArgs env ns t
162 = map (not . null) (reverse ns)
164getUnmatchable ctxt n = []
166data ElabCtxt = ElabCtxt { e_inarg :: Bool,
167 e_isfn :: Bool, -- ^ Function part of application
168 e_guarded :: Bool,
169 e_intype :: Bool,
170 e_qq :: Bool,
171 e_nomatching :: Bool -- ^ can't pattern match
172 }
174initElabCtxt = ElabCtxt False False False False False False
176goal_polymorphic :: ElabD Bool
177goal_polymorphic =
178 do ty <- goal
179 case ty of
180 P _ n _ -> do env <- get_env
181 case lookup n env of
182 Nothing -> return False
183 _ -> return True
184 _ -> return False
186-- Returns the set of declarations we need to add to complete the definition
187-- (most likely case blocks to elaborate)
189elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
190 ElabD ()
191elab ist info emode opts fn tm
192 = do let loglvl = opt_logLevel (idris_options ist)
193 when (loglvl > 5) $ unifyLog True
194 compute -- expand type synonyms, etc
195 let fc = maybe "(unknown)"
196 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
197 est <- getAux
198 sequence_ (delayed_elab est)
199 end_unify
200 ptm <- get_term
201 when pattern -- convert remaining holes to pattern vars
202 (do update_term orderPats
203 unify_all
204 matchProblems False -- only the ones we matched earlier
205 unifyProblems
206 mkPat)
207 where
208 pattern = emode == ELHS
209 bindfree = emode == ETyDecl || emode == ELHS
211 tcgen = Dictionary `elem` opts
212 reflection = Reflection `elem` opts
214 isph arg = case getTm arg of
215 Placeholder -> (True, priority arg)
216 tm -> (False, priority arg)
218 toElab ina arg = case getTm arg of
219 Placeholder -> Nothing
220 v -> Just (priority arg, elabE ina (elabFC info) v)
222 toElab' ina arg = case getTm arg of
223 Placeholder -> Nothing
224 v -> Just (elabE ina (elabFC info) v)
226 mkPat = do hs <- get_holes
227 tm <- get_term
228 case hs of
229 (h: hs) -> do patvar h; mkPat
230 [] -> return ()
232 -- | elabE elaborates an expression, possibly wrapping implicit coercions
233 -- and forces/delays. If you make a recursive call in elab', it is
234 -- normally correct to call elabE - the ones that don't are desugarings
235 -- typically
236 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
237 elabE ina fc' t =
238 --do g <- goal
239 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
240 do solved <- get_recents
241 as <- get_autos
242 -- If any of the autos use variables which have recently been solved,
243 -- have another go at solving them now.
244 mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns
245 then solveAuto ist fn False a
246 else return ()) as
248 itm <- if not pattern then insertImpLam ina t else return t
249 ct <- insertCoerce ina itm
250 t' <- insertLazy ct
251 g <- goal
252 tm <- get_term
253 ps <- get_probs
254 hs <- get_holes
256 --trace ("Elaborating " ++ show t' ++ " in " ++ show g
257 -- ++ "\n" ++ show tm
258 -- ++ "\nholes " ++ show hs
259 -- ++ "\nproblems " ++ show ps
260 -- ++ "\n-----------\n") $
261 --trace ("ELAB " ++ show t') $
262 let fc = fileFC "Force"
263 env <- get_env
264 handleError (forceErr env)
265 (elab' ina fc' t')
266 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))
267 [pimp (sUN "t") Placeholder True,
268 pimp (sUN "a") Placeholder True,
269 pexp ct])) True
271 forceErr env (CantUnify _ (t,_) (t',_) _ _ _)
272 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
273 ht == txt "Lazy'" = True
274 forceErr env (CantUnify _ (t,_) (t',_) _ _ _)
275 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
276 ht == txt "Lazy'" = True
277 forceErr env (InfiniteUnify _ t _)
278 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
279 ht == txt "Lazy'" = True
280 forceErr env (Elaborating _ _ t) = forceErr env t
281 forceErr env (ElaboratingArg _ _ _ t) = forceErr env t
282 forceErr env (At _ t) = forceErr env t
283 forceErr env t = False
285 local f = do e <- get_env
286 return (f `elem` map fst e)
288 -- | Is a constant a type?
289 constType :: Const -> Bool
290 constType (AType _) = True
291 constType StrType = True
292 constType PtrType = True
293 constType VoidType = True
294 constType _ = False
296 -- "guarded" means immediately under a constructor, to help find patvars
298 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)
299 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable
300 -> PTerm -- ^ The term to elaborate
301 -> ElabD ()
302 elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step
303 elab' ina fc PType = do apply RType []; solve
304 elab' ina fc (PUniverse u) = do apply (RUType u) []; solve
305-- elab' (_,_,inty) (PConstant c)
306-- | constType c && pattern && not reflection && not inty
307-- = lift $ tfail (Msg "Typecase is not allowed")
308 elab' ina fc tm@(PConstant c)
309 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
310 && isTypeConst c
311 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
312 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
313 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
314 | otherwise = do apply (RConstant c) []; solve
315 elab' ina fc (PQuote r) = do fill r; solve
316 elab' ina _ (PTrue fc _) =
317 do hnf_compute
318 g <- goal
319 case g of
320 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
321 UType _ -> elab' ina (Just fc) (PRef fc unitTy)
322 _ -> elab' ina (Just fc) (PRef fc unitCon)
323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
324 = do g <- goal; resolveTC False 5 g fn ist
325 elab' ina fc (PResolveTC fc')
326 = do c <- getNameFrom (sMN 0 "class")
327 instanceArg c
328 elab' ina _ (PRefl fc t)
329 = elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
330 pimp (sMN 0 "x") t False])
331 elab' ina _ (PEq fc Placeholder Placeholder l r)
332 = try (do tyn <- getNameFrom (sMN 0 "aqty")
333 claim tyn RType
334 movelast tyn
335 elab' ina (Just fc) (PApp fc (PRef fc eqTy)
336 [pimp (sUN "A") (PRef fc tyn) True,
337 pimp (sUN "B") (PRef fc tyn) False,
338 pexp l, pexp r]))
339 (do atyn <- getNameFrom (sMN 0 "aqty")
340 btyn <- getNameFrom (sMN 0 "bqty")
341 claim atyn RType
342 movelast atyn
343 claim btyn RType
344 movelast btyn
345 elab' ina (Just fc) (PApp fc (PRef fc eqTy)
346 [pimp (sUN "A") (PRef fc atyn) True,
347 pimp (sUN "B") (PRef fc btyn) False,
348 pexp l, pexp r]))
350 elab' ina _ (PEq fc lt rt l r) = elab' ina (Just fc) (PApp fc (PRef fc eqTy)
351 [pimp (sUN "A") lt True,
352 pimp (sUN "B") rt False,
353 pexp l, pexp r])
354 elab' ina _ (PPair fc _ l r)
355 = do hnf_compute
356 g <- goal
357 let (tc, _) = unApply g
358 case g of
359 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
360 [pexp l,pexp r])
361 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)
362 [pexp l,pexp r])
363 _ -> case tc of
364 P _ n _ | n == upairTy
365 -> elab' ina (Just fc) (PApp fc (PRef fc upairCon)
366 [pimp (sUN "A") Placeholder False,
367 pimp (sUN "B") Placeholder False,
368 pexp l, pexp r])
369 _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
370 [pimp (sUN "A") Placeholder False,
371 pimp (sUN "B") Placeholder False,
372 pexp l, pexp r])
373-- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)
374-- [pimp (sUN "A") Placeholder False,
375-- pimp (sUN "B") Placeholder False,
376-- pexp l, pexp r]))
377-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)
378-- [pimp (sUN "A") Placeholder False,
379-- pimp (sUN "B") Placeholder False,
380-- pexp l, pexp r]))
381-- True
383 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
384 = case t of
385 Placeholder ->
386 do hnf_compute
387 g <- goal
388 case g of
389 TType _ -> asType
390 _ -> asValue
391 _ -> asType
392 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
393 [pexp t,
394 pexp (PLam fc n Placeholder r)])
395 asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)
396 [pimp (sMN 0 "a") t False,
397 pimp (sMN 0 "P") Placeholder True,
398 pexp l, pexp r])
399 elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc existsCon)
400 [pimp (sMN 0 "a") t False,
401 pimp (sMN 0 "P") Placeholder True,
402 pexp l, pexp r])
403 elab' ina fc (PAlternative True as)
404 = do hnf_compute
405 ty <- goal
406 ctxt <- get_context
407 let (tc, _) = unApply ty
408 env <- get_env
409 let as' = pruneByType (map fst env) tc ctxt as
410-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++
411-- show (length as') ++ "\n" ++
412-- showSep ", " (map showTmImpls as') ++ "\nEND") $
413 tryAll (zip (map (elab' ina fc) as') (map showHd as'))
414 where showHd (PApp _ (PRef _ n) _) = n
415 showHd (PRef _ n) = n
416 showHd (PApp _ h _) = showHd h
417 showHd x = NErased -- We probably should do something better than this here
418 elab' ina fc (PAlternative False as)
419 = trySeq as
420 where -- if none work, take the error from the first
421 trySeq (x : xs) = let e1 = elab' ina fc x in
422 try' e1 (trySeq' e1 xs) True
423 trySeq [] = fail "Nothing to try in sequence"
424 trySeq' deferr [] = proofFail deferr
425 trySeq' deferr (x : xs)
426 = try' (do elab' ina fc x
427 solveAutos ist fn False) (trySeq' deferr xs) True
428 elab' ina _ (PPatvar fc n) | bindfree = do patvar n; update_term liftPats
429-- elab' (_, _, inty) (PRef fc f)
430-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
431-- = lift $ tfail (Msg "Typecase is not allowed")
432 elab' ec _ tm@(PRef fc n)
433 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
434 && isTConName n (tt_ctxt ist)
435 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
436 | pattern && not reflection && not (e_qq ec) && e_nomatching ec
437 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
438 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
439 = do let ina = e_inarg ec
440 guarded = e_guarded ec
441 inty = e_intype ec
442 ctxt <- get_context
443 let defined = case lookupTy n ctxt of
444 [] -> False
445 _ -> True
446 -- this is to stop us resolve type classes recursively
447 -- trace (show (n, guarded)) $
448 if (tcname n && ina) then erun fc $ do patvar n; -- update_term liftPats
449 else if (defined && not guarded)
450 then do apply (Var n) []; solve
451 else try (do apply (Var n) []; solve)
452 (do patvar n; update_term liftPats)
453 where inparamBlock n = case lookupCtxtName n (inblock info) of
454 [] -> False
455 _ -> True
456 bindable (NS _ _) = False
457 bindable (UN xs) = True
458 bindable n = implicitable n
459 elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])
460 elab' ina fc' tm@(PRef fc n)
461 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
462 && isTConName n (tt_ctxt ist)
463 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
464 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
465 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
466 | otherwise =
467 do fty <- get_type (Var n) -- check for implicits
468 ctxt <- get_context
469 env <- get_env
470 let a' = insertScopedImps fc (normalise ctxt env fty) []
471 if null a'
472 then erun fc $ do apply (Var n) []; solve
473 else elab' ina fc' (PApp fc tm [])
474 elab' ina _ (PLam fc n Placeholder sc)
475 = do -- if n is a type constructor name, this makes no sense...
476 ctxt <- get_context
477 when (isTConName n ctxt) $
478 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
479 checkPiGoal n
480 attack; intro (Just n);
481 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
482 elabE (ina { e_inarg = True } ) (Just fc) sc; solve
483 elab' ec _ (PLam fc n ty sc)
484 = do tyn <- getNameFrom (sMN 0 "lamty")
485 -- if n is a type constructor name, this makes no sense...
486 ctxt <- get_context
487 when (isTConName n ctxt) $
488 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
489 checkPiGoal n
490 claim tyn RType
491 explicit tyn
492 attack
493 ptm <- get_term
494 hs <- get_holes
495 introTy (Var tyn) (Just n)
496 focus tyn
498 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
499 elabE (ec { e_inarg = True }) (Just fc) sc
500 solve
501 elab' ina fc (PPi p n Placeholder sc)
502 = do attack; arg n (is_scoped p) (sMN 0 "ty")
503 elabE (ina { e_inarg = True, e_intype = True }) fc sc
504 solve
505 elab' ina fc (PPi p n ty sc)
506 = do attack; tyn <- getNameFrom (sMN 0 "ty")
507 claim tyn RType
508 n' <- case n of
509 MN _ _ -> unique_hole n
510 _ -> return n
511 forall n' (is_scoped p) (Var tyn)
512 focus tyn
513 let ec' = ina { e_inarg = True, e_intype = True }
514 elabE ec' fc ty
515 elabE ec' fc sc
516 solve
517 elab' ina _ (PLet fc n ty val sc)
518 = do attack
519 ivs <- get_instances
520 tyn <- getNameFrom (sMN 0 "letty")
521 claim tyn RType
522 valn <- getNameFrom (sMN 0 "letval")
523 claim valn (Var tyn)
524 explicit valn
525 letbind n (Var tyn) (Var valn)
526 case ty of
527 Placeholder -> return ()
528 _ -> do focus tyn
529 explicit tyn
530 elabE (ina { e_inarg = True, e_intype = True })
531 (Just fc) ty
532 focus valn
533 elabE (ina { e_inarg = True, e_intype = True })
534 (Just fc) val
535 ivs' <- get_instances
536 env <- get_env
537 elabE (ina { e_inarg = True }) (Just fc) sc
538 when (not pattern) $
539 mapM_ (\n -> do focus n
540 g <- goal
541 hs <- get_holes
542 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
543 then try (resolveTC True 7 g fn ist)
544 (movelast n)
545 else movelast n)
546 (ivs' \\ ivs)
547 -- HACK: If the name leaks into its type, it may leak out of
548 -- scope outside, so substitute in the outer scope.
549 expandLet n (case lookup n env of
550 Just (Let t v) -> v
551 other -> error ("Value not a let binding: " ++ show other))
552 solve
553 elab' ina _ (PGoal fc r n sc) = do
554 rty <- goal
555 attack
556 tyn <- getNameFrom (sMN 0 "letty")
557 claim tyn RType
558 valn <- getNameFrom (sMN 0 "letval")
559 claim valn (Var tyn)
560 letbind n (Var tyn) (Var valn)
561 focus valn
562 elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])
563 env <- get_env
564 computeLet n
565 elabE (ina { e_inarg = True }) (Just fc) sc
566 solve
567-- elab' ina fc (PLet n Placeholder
568-- (PApp fc r [pexp (delab ist rty)]) sc)
569 elab' ina _ tm@(PApp fc (PInferRef _ f) args) = do
570 rty <- goal
571 ds <- get_deferred
572 ctxt <- get_context
573 -- make a function type a -> b -> c -> ... -> rty for the
574 -- new function name
575 env <- get_env
576 argTys <- claimArgTys env args
577 fn <- getNameFrom (sMN 0 "inf_fn")
578 let fty = fnTy argTys rty
579-- trace (show (ptm, map fst argTys)) $ focus fn
580 -- build and defer the function application
581 attack; deferType (mkN f) fty (map fst argTys); solve
582 -- elaborate the arguments, to unify their types. They all have to
583 -- be explicit.
584 mapM_ elabIArg (zip argTys args)
585 where claimArgTys env [] = return []
586 claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
587 = do nty <- get_type (Var n)
588 ans <- claimArgTys env xs
589 return ((n, (False, forget nty)) : ans)
590 claimArgTys env (_ : xs)
591 = do an <- getNameFrom (sMN 0 "inf_argTy")
592 aval <- getNameFrom (sMN 0 "inf_arg")
593 claim an RType
594 claim aval (Var an)
595 ans <- claimArgTys env xs
596 return ((aval, (True, (Var an))) : ans)
597 fnTy [] ret = forget ret
598 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)
600 localVar env (PRef _ x)
601 = case lookup x env of
602 Just _ -> Just x
603 _ -> Nothing
604 localVar env _ = Nothing
606 elabIArg ((n, (True, ty)), def) =
607 do focus n; elabE ina (Just fc) (getTm def)
608 elabIArg _ = return () -- already done, just a name
610 mkN n@(NS _ _) = n
611 mkN n@(SN _) = n
612 mkN n = case namespace info of
613 Just xs@(_:_) -> sNS n xs
614 _ -> n
616 elab' ina _ (PMatchApp fc fn)
617 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
618 [(n, args)] -> return (n, map (const True) args)
619 _ -> lift $ tfail (NoSuchVariable fn)
620 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
621 solve
622 -- if f is local, just do a simple_app
623 -- FIXME: Anyone feel like refactoring this mess? - EB
624 elab' ina topfc tm@(PApp fc (PRef _ f) args_in)
625 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
626 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
627 | otherwise = implicitApp $
628 do env <- get_env
629 ty <- goal
630 fty <- get_type (Var f)
631 ctxt <- get_context
632 let args = insertScopedImps fc (normalise ctxt env fty) args_in
633 let unmatchableArgs = if pattern
634 then getUnmatchable (tt_ctxt ist) f
635 else []
636-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
637 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
638 && isTConName f (tt_ctxt ist)) $
639 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
640 if (f `elem` map fst env && length args == 1 && length args_in == 1)
641 then -- simple app, as below
642 do simple_app False
643 (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))
644 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
645 (show tm)
646 solve
647 return []
648 else
649 do ivs <- get_instances
650 ps <- get_probs
651 -- HACK: we shouldn't resolve type classes if we're defining an instance
652 -- function or default definition.
653 let isinf = f == inferCon || tcname f
654 -- if f is a type class, we need to know its arguments so that
655 -- we can unify with them
656 case lookupCtxt f (idris_classes ist) of
657 [] -> return ()
658 _ -> do mapM_ setInjective (map getTm args)
659 -- maybe more things are solvable now
660 unifyProblems
661 let guarded = isConName f ctxt
662-- trace ("args is " ++ show args) $ return ()
663 ns <- apply (Var f) (map isph args)
664-- trace ("ns is " ++ show ns) $ return ()
665 -- mark any type class arguments as injective
666 mapM_ checkIfInjective (map snd ns)
667 unifyProblems -- try again with the new information,
668 -- to help with disambiguation
669 -- Sort so that the implicit tactics and alternatives go last
670 let (ns', eargs) = unzip $
671 sortBy cmpArg (zip ns args)
672 ulog <- getUnifyLog
673 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
674 [] fc False f
675 (zip ns' (unmatchableArgs ++ repeat False))
676 (f == sUN "Force")
677 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
678 imp <- if (e_isfn ina) then
679 do guess <- get_guess
680 gty <- get_type (forget guess)
681 env <- get_env
682 let ty_n = normalise ctxt env gty
683 return $ getReqImps ty_n
684 else return []
685 -- Now we find out how many implicits we needed at the
686 -- end of the application by looking at the goal again
687 -- - Have another go, but this time add the
688 -- implicits (can't think of a better way than this...)
689 case imp of
690 rs@(_:_) | not pattern -> return rs -- quit, try again
691 _ -> do solve
692 hs <- get_holes
693 ivs' <- get_instances
694 -- Attempt to resolve any type classes which have 'complete' types,
695 -- i.e. no holes in them
696 when (not pattern || (e_inarg ina && not tcgen &&
697 not (e_guarded ina))) $
698 mapM_ (\n -> do focus n
699 g <- goal
700 env <- get_env
701 hs <- get_holes
702 if all (\n -> not (n `elem` hs)) (freeNames g)
703 then try (resolveTC False 7 g fn ist)
704 (movelast n)
705 else movelast n)
706 (ivs' \\ ivs)
707 return []
708 where
709 -- Run the elaborator, which returns how many implicit
710 -- args were needed, then run it again with those args. We need
711 -- this because we have to elaborate the whole application to
712 -- find out whether any computations have caused more implicits
713 -- to be needed.
714 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
715 implicitApp elab
716 | pattern = do elab; return ()
717 | otherwise
718 = do s <- get
719 imps <- elab
720 case imps of
721 [] -> return ()
722 es -> do put s
723 elab' ina topfc (PAppImpl tm es)
725 getReqImps (Bind x (Pi (Just i) ty _) sc)
726 = i : getReqImps sc
727 getReqImps _ = []
729 -- normal < alternatives < lambdas < rewrites < tactic < default tactic
730 -- reason for lambdas after alternatives is that having
731 -- the alternative resolved can help with typechecking the lambda
732 -- or the rewrite. Rewrites/tactics need as much information
733 -- as possible about the type.
734 -- FIXME: Better would be to allow alternative resolution to be
735 -- retried after more information is in.
736 cmpArg (_, x) (_, y)
737 | constraint x && not (constraint y) = LT
738 | constraint y && not (constraint x) = GT
739 | otherwise
740 = compare (conDepth 0 (getTm x) + priority x + alt x)
741 (conDepth 0 (getTm y) + priority y + alt y)
742 where alt t = case getTm t of
743 PAlternative False _ -> 5
744 PAlternative True _ -> 2
745 PTactics _ -> 150
746 PLam _ _ _ _ -> 3
747 PRewrite _ _ _ _ -> 4
748 PResolveTC _ -> 0
749 PHidden _ -> 150
750 _ -> 1
752 constraint (PConstraint _ _ _ _) = True
753 constraint _ = False
755 -- Score a point for every level where there is a non-constructor
756 -- function (so higher score --> done later), and lots of points
757 -- if there is a PHidden since this should be unifiable.
758 -- Only relevant when on lhs
759 conDepth d t | not pattern = 0
760 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
761 | otherwise = max (100 - d) 1
762 conDepth d (PApp _ f as)
763 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
764 conDepth d (PPatvar _ _) = 0
765 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
766 conDepth d (PHidden _) = 150
767 conDepth d Placeholder = 0
768 conDepth d (PResolveTC _) = 0
769 conDepth d t = max (100 - d) 1
771 checkIfInjective n = do
772 env <- get_env
773 case lookup n env of
774 Nothing -> return ()
775 Just b ->
776 case unApply (binderTy b) of
777 (P _ c _, args) ->
778 case lookupCtxt c (idris_classes ist) of
779 [] -> return ()
780 _ -> -- type class, set as injective
781 do mapM_ setinjArg args
782 -- maybe we can solve more things now...
783 ulog <- getUnifyLog
784 probs <- get_probs
785 traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $
786 unifyProblems
787 probs <- get_probs
788 traceWhen ulog (qshow probs) $ return ()
789 _ -> return ()
791 setinjArg (P _ n _) = setinj n
792 setinjArg _ = return ()
794 tacTm (PTactics _) = True
795 tacTm (PProof _) = True
796 tacTm _ = False
798 setInjective (PRef _ n) = setinj n
799 setInjective (PApp _ (PRef _ n) _) = setinj n
800 setInjective _ = return ()
802 elab' ina _ tm@(PApp fc f [arg]) =
803 erun fc $
804 do simple_app (not $ headRef f)
805 (elabE (ina { e_isfn = True }) (Just fc) f)
806 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
807 (show tm)
808 solve
809 where headRef (PRef _ _) = True
810 headRef (PApp _ f _) = headRef f
811 headRef _ = False
813 elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
814 solve
815 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
816 appImpl (e : es) = simple_app False
817 (appImpl es)
818 (elab' ina fc Placeholder)
819 (show f)
820 elab' ina fc Placeholder
821 = do (h : hs) <- get_holes
822 movelast h
823 elab' ina fc (PMetavar n) =
824 do ptm <- get_term
825 -- When building the metavar application, leave out the unique
826 -- names which have been used elsewhere in the term, since we
827 -- won't be able to use them in the resulting application.
828 let unique_used = getUniqueUsed (tt_ctxt ist) ptm
829 let n' = mkN n
830 attack
831 defer unique_used n'
832 solve
833 where mkN n@(NS _ _) = n
834 mkN n = case namespace info of
835 Just xs@(_:_) -> sNS n xs
836 _ -> n
837 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
838 elab' ina fc (PTactics ts)
839 | not pattern = do mapM_ (runTac False ist fc fn) ts
840 | otherwise = elab' ina fc Placeholder
841 elab' ina fc (PElabError e) = lift $ tfail e
842 elab' ina _ (PRewrite fc r sc newg)
843 = do attack
844 tyn <- getNameFrom (sMN 0 "rty")
845 claim tyn RType
846 valn <- getNameFrom (sMN 0 "rval")
847 claim valn (Var tyn)
848 letn <- getNameFrom (sMN 0 "_rewrite_rule")
849 letbind letn (Var tyn) (Var valn)
850 focus valn
851 elab' ina (Just fc) r
852 compute
853 g <- goal
854 rewrite (Var letn)
855 g' <- goal
856 when (g == g') $ lift $ tfail (NoRewriting g)
857 case newg of
858 Nothing -> elab' ina (Just fc) sc
859 Just t -> doEquiv t sc
860 solve
861 where doEquiv t sc =
862 do attack
863 tyn <- getNameFrom (sMN 0 "ety")
864 claim tyn RType
865 valn <- getNameFrom (sMN 0 "eqval")
866 claim valn (Var tyn)
867 letn <- getNameFrom (sMN 0 "equiv_val")
868 letbind letn (Var tyn) (Var valn)
869 focus tyn
870 elab' ina (Just fc) t
871 focus valn
872 elab' ina (Just fc) sc
873 elab' ina (Just fc) (PRef fc letn)
874 solve
875 elab' ina _ c@(PCase fc scr opts)
876 = do attack
877 tyn <- getNameFrom (sMN 0 "scty")
878 claim tyn RType
879 valn <- getNameFrom (sMN 0 "scval")
880 scvn <- getNameFrom (sMN 0 "scvar")
881 claim valn (Var tyn)
882 letbind scvn (Var tyn) (Var valn)
883 focus valn
884 elabE (ina { e_inarg = True }) (Just fc) scr
885 -- Solve any remaining implicits - we need to solve as many
886 -- as possible before making the 'case' type
887 unifyProblems
888 matchProblems True
889 args <- get_env
890 envU <- mapM (getKind args) args
891 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
893 -- Drop the unique arguments used in the term already
894 -- and in the scrutinee (since it's
895 -- not valid to use them again anyway)
896 --
897 -- Also drop unique arguments which don't appear explicitly
898 -- in either case branch so they don't count as used
899 -- unnecessarily (can only do this for unique things, since we
900 -- assume they don't appear implicitly in types)
901 ptm <- get_term
902 let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
904 let argsDropped = filter (isUnique envU)
905 (nub $ allNamesIn scr ++ inApp ptm ++
906 inOpts)
908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
910 cname <- unique_hole' True (mkCaseName fn)
911 let cname' = mkN cname
912-- elab' ina fc (PMetavar cname')
913 attack; defer argsDropped cname'; solve
915 -- if the scrutinee is one of the 'args' in env, we should
916 -- inspect it directly, rather than adding it as a new argument
917 let newdef = PClauses fc [] cname'
918 (caseBlock fc cname'
919 (map (isScr scr) (reverse args')) opts)
920 -- elaborate case
921 updateAux (\e -> e { case_decls = newdef : case_decls e } )
922 -- if we haven't got the type yet, hopefully we'll get it later!
923 movelast tyn
924 solve
925 where mkCaseName (NS n ns) = NS (mkCaseName n) ns
926 mkCaseName n = SN (CaseN n)
927-- mkCaseName (UN x) = UN (x ++ "_case")
928-- mkCaseName (MN i x) = MN i (x ++ "_case")
929 mkN n@(NS _ _) = n
930 mkN n = case namespace info of
931 Just xs@(_:_) -> sNS n xs
932 _ -> n
934 inApp (P _ n _) = [n]
935 inApp (App f a) = inApp f ++ inApp a
936 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
937 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
938 inApp (Bind n b sc) = inApp sc
939 inApp _ = []
941 isUnique envk n = case lookup n envk of
942 Just u -> u
943 _ -> False
945 getKind env (n, _)
946 = case lookup n env of
947 Nothing -> return (n, False) -- can't happen, actually...
948 Just b ->
949 do ty <- get_type (forget (binderTy b))
950 case ty of
951 UType UniqueType -> return (n, True)
952 UType AllTypes -> return (n, True)
953 _ -> return (n, False)
955 tcName tm | (P _ n _, _) <- unApply tm
956 = case lookupCtxt n (idris_classes ist) of
957 [_] -> True
958 _ -> False
959 tcName _ = False
961 usedIn ns (n, b)
962 = n `elem` ns
963 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
965 elab' ina fc (PUnifyLog t) = do unifyLog True
966 elab' ina fc t
967 unifyLog False
968 elab' ina fc (PQuasiquote t goal)
969 = do -- First extract the unquoted subterms, replacing them with fresh
970 -- names in the quasiquoted term. Claim their reflections to be
971 -- an inferred type (to support polytypic quasiquotes).
972 (t, unq) <- extractUnquotes 0 t
973 let unquoteNames = map fst unq
974 mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")
975 claim uqh RType
976 movelast uqh
977 claim uqn (Var uqh)) unquoteNames
980 -- Save the old state - we need a fresh proof state to avoid
981 -- capturing lexically available variables in the quoted term.
982 ctxt <- get_context
983 saveState
984 updatePS (const .
985 newProof (sMN 0 "q") ctxt $
986 P Ref (reflm "TT") Erased)
988 -- Re-add the unquotes, letting Idris infer the (fictional)
989 -- types. Here, they represent the real type rather than the type
990 -- of their reflection.
991 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
992 claim ty RType
993 movelast ty
994 claim n (Var ty)
995 movelast n)
996 unquoteNames
998 -- Determine whether there's an explicit goal type, and act accordingly
999 -- Establish holes for the type and value of the term to be
1000 -- quasiquoted
1001 qTy <- getNameFrom (sMN 0 "qquoteTy")
1002 claim qTy RType
1003 movelast qTy
1004 qTm <- getNameFrom (sMN 0 "qquoteTm")
1005 claim qTm (Var qTy)
1007 -- Let-bind the result of elaborating the contained term, so that
1008 -- the hole doesn't disappear
1009 nTm <- getNameFrom (sMN 0 "quotedTerm")
1010 letbind nTm (Var qTy) (Var qTm)
1012 -- Fill out the goal type, if relevant
1013 case goal of
1014 Nothing -> return ()
1015 Just gTy -> do focus qTy
1016 elabE (ina { e_qq = True }) fc gTy
1018 -- Elaborate the quasiquoted term into the hole
1019 focus qTm
1020 elabE (ina { e_qq = True }) fc t
1021 end_unify
1023 -- We now have an elaborated term. Reflect it and solve the
1024 -- original goal in the original proof state.
1025 env <- get_env
1026 loadState
1027 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
1029 case quoted of
1030 Just q -> do ctxt <- get_context
1031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
1032 if pattern
1033 then do try' (reflectTTQuotePattern unquoteNames q')
1034 (reflectRawQuotePattern unquoteNames (forget q'))
1035 True
1036 else do try' (fill $ reflectTTQuote unquoteNames q')
1037 -- we forget q' instead of using q to ensure rechecking
1038 (fill $ reflectRawQuote unquoteNames (forget q'))
1039 True -- ignore errors like proof search does
1040 solve
1042 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
1044 -- Finally fill in the terms or patterns from the unquotes. This
1045 -- happens last so that their holes still exist while elaborating
1046 -- the main quotation.
1047 mapM_ elabUnquote unq
1048 where elabUnquote (n, tm)
1049 = do focus n
1050 elabE (ina { e_qq = False }) fc tm
1053 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
1054 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
1055 elab' ina fc (PHidden t)
1056 | reflection = elab' ina fc t
1057 | otherwise
1058 = do (h : hs) <- get_holes
1059 -- Dotting a hole means that either the hole or any outer
1060 -- hole (a hole outside any occurrence of it)
1061 -- must be solvable by unification as well as being filled
1062 -- in directly.
1063 -- Delay dotted things to the end, then when we elaborate them
1064 -- we can check the result against what was inferred
1065 movelast h
1066 delayElab $ do focus h
1067 dotterm
1068 elab' ina fc t
1069 elab' ina fc (PRunTactics fc' tm) =
1070 do attack
1071 n <- getNameFrom (sMN 0 "tacticScript")
1072 n' <- getNameFrom (sMN 0 "tacticExpr")
1073 let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1074 claim n scriptTy
1075 movelast n
1076 letbind n' scriptTy (Var n)
1077 focus n
1078 elab' ina (Just fc') tm
1079 env <- get_env
1080 ctxt <- get_context
1081 runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)
1082 solve
1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1085 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
1087 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
1088 isScr (PRef _ n) (n', b) = (n', (n == n', b))
1089 isScr _ (n', b) = (n', (False, b))
1091 caseBlock :: FC -> Name ->
1092 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
1093 caseBlock fc n env opts
1094 = let args' = findScr env
1095 args = map mkarg (map getNmScr args') in
1096 map (mkClause args) opts
1098 where -- Find the variable we want as the scrutinee and mark it as
1099 -- 'True'. If the scrutinee is in the environment, match on that
1100 -- otherwise match on the new argument we're adding.
1101 findScr ((n, (True, t)) : xs)
1102 = (n, (True, t)) : scrName n xs
1103 findScr [(n, (_, t))] = [(n, (True, t))]
1104 findScr (x : xs) = x : findScr xs
1105 -- [] can't happen since scrutinee is in the environment!
1106 findScr [] = error "The impossible happened - the scrutinee was not in the environment"
1108 -- To make sure top level pattern name remains in scope, put
1109 -- it at the end of the environment
1110 scrName n [] = []
1111 scrName n [(_, t)] = [(n, t)]
1112 scrName n (x : xs) = x : scrName n xs
1114 getNmScr (n, (s, _)) = (n, s)
1116 mkarg (n, s) = (PRef fc n, s)
1117 -- may be shadowed names in the new pattern - so replace the
1118 -- old ones with an _
1119 mkClause args (l, r)
1120 = let args' = map (shadowed (allNamesIn l)) args
1121 lhs = PApp (getFC fc l) (PRef (getFC fc l) n)
1122 (map (mkLHSarg l) args') in
1123 PClause (getFC fc l) n lhs [] r []
1125 mkLHSarg l (tm, True) = pexp l
1126 mkLHSarg l (tm, False) = pexp tm
1128 shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)
1129 shadowed new t = t
1131 getFC d (PApp fc _ _) = fc
1132 getFC d (PRef fc _) = fc
1133 getFC d (PAlternative _ (x:_)) = getFC d x
1134 getFC d x = d
1136 insertLazy :: PTerm -> ElabD PTerm
1137 insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t
1138 insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t
1139 insertLazy (PCoerced t) = return t
1140 insertLazy t =
1141 do ty <- goal
1142 env <- get_env
1143 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
1144 let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]
1145 case tyh of
1146 P _ (UN l) _ | l == txt "Lazy'"
1147 -> return (PAlternative False tries)
1148 _ -> return t
1149 where
1150 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)
1151 mkDelay env t
1152 = let fc = fileFC "Delay" in
1153 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))
1154 [pexp t])
1157 -- Don't put implicit coercions around applications which are marked
1158 -- as '%noImplicit', or around case blocks, otherwise we get exponential
1159 -- blowup especially where there are errors deep in large expressions.
1160 notImplicitable (PApp _ f _) = notImplicitable f
1161 -- TMP HACK no coercing on bind (make this configurable)
1162 notImplicitable (PRef _ n)
1163 | [opts] <- lookupCtxt n (idris_flags ist)
1164 = NoImplicit `elem` opts
1165 notImplicitable (PAlternative True as) = any notImplicitable as
1166 -- case is tricky enough without implicit coercions! If they are needed,
1167 -- they can go in the branches separately.
1168 notImplicitable (PCase _ _ _) = True
1169 notImplicitable _ = False
1171 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
1172 | tcinstance i
1173 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1174 | otherwise
1175 = pimp n Placeholder True : insertScopedImps fc sc xs
1176 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
1177 = x : insertScopedImps fc sc xs
1178 insertScopedImps _ _ xs = xs
1180 insertImpLam ina t =
1181 do ty <- goal
1182 env <- get_env
1183 let ty' = normalise (tt_ctxt ist) env ty
1184 addLam ty' t
1185 where
1186 -- just one level at a time
1187 addLam (Bind n (Pi (Just _) _ _) sc) t =
1188 do impn <- unique_hole (sMN 0 "imp")
1189 if e_isfn ina -- apply to an implicit immediately
1190 then return (PApp emptyFC
1191 (PLam emptyFC impn Placeholder t)
1192 [pexp Placeholder])
1193 else return (PLam emptyFC impn Placeholder t)
1194 addLam _ t = return t
1196 insertCoerce ina t@(PCase _ _ _) = return t
1197 insertCoerce ina t | notImplicitable t = return t
1198 insertCoerce ina t =
1199 do ty <- goal
1200 -- Check for possible coercions to get to the goal
1201 -- and add them as 'alternatives'
1202 env <- get_env
1203 let ty' = normalise (tt_ctxt ist) env ty
1204 let cs = getCoercionsTo ist ty'
1205 let t' = case (t, cs) of
1206 (PCoerced tm, _) -> tm
1207 (_, []) -> t
1208 (_, cs) -> PAlternative False [t ,
1209 PAlternative True (map (mkCoerce env t) cs)]
1210 return t'
1211 where
1212 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
1213 addImplBound ist (map fst env)
1214 (PApp fc (PRef fc n) [pexp (PCoerced t)])
1216 -- | Elaborate the arguments to a function
1217 elabArgs :: IState -- ^ The current Idris state
1218 -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)
1219 -> [Bool]
1220 -> FC -- ^ Source location
1221 -> Bool
1222 -> Name -- ^ Name of the function being applied
1223 -> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable)
1224 -> Bool -- ^ under a 'force'
1225 -> [PTerm] -- ^ argument
1226 -> ElabD ()
1227 elabArgs ist ina failed fc retry f [] force _ = return ()
1228 elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)
1229 = do hs <- get_holes
1230 if holeName `elem` hs then
1231 do focus holeName
1232 case t of
1233 Placeholder -> do movelast holeName
1234 elabArgs ist ina failed fc r f ns force args
1235 _ -> elabArg t
1236 else elabArgs ist ina failed fc r f ns force args
1237 where elabArg t =
1238 do -- solveAutos ist fn False
1239 now_elaborating fc f argName
1240 wrapErr f argName $ do
1241 hs <- get_holes
1242 tm <- get_term
1243 -- No coercing under an explicit Force (or it can Force/Delay
1244 -- recursively!)
1245 let elab = if force then elab' else elabE
1246 failed' <- -- trace (show (n, t, hs, tm)) $
1247 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
1248 do focus holeName;
1249 g <- goal
1250 -- Can't pattern match on polymorphic goals
1251 poly <- goal_polymorphic
1252 ulog <- getUnifyLog
1253 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
1254 elab (ina { e_nomatching = unm && poly }) (Just fc) t
1255 return failed
1256 done_elaborating_arg f argName
1257 elabArgs ist ina failed fc r f ns force args
1258 wrapErr f argName action =
1259 do elabState <- get
1260 while <- elaborating_app
1261 let while' = map (\(x, y, z)-> (y, z)) while
1262 (result, newState) <- case runStateT action elabState of
1263 OK (res, newState) -> return (res, newState)
1264 Error e -> do done_elaborating_arg f argName
1265 lift (tfail (elaboratingArgErr while' e))
1266 put newState
1267 return result
1268 elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
1269 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1271-- For every alternative, look at the function at the head. Automatically resolve
1272-- any nested alternatives where that function is also at the head
1274pruneAlt :: [PTerm] -> [PTerm]
1275pruneAlt xs = map prune xs
1276 where
1277 prune (PApp fc1 (PRef fc2 f) as)
1278 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
1279 prune t = t
1281 choose f (PAlternative a as)
1282 = let as' = fmap (choose f) as
1283 fs = filter (headIs f) as' in
1284 case fs of
1285 [a] -> a
1286 _ -> PAlternative a as'
1288 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
1289 choose f t = t
1291 headIs f (PApp _ (PRef _ f') _) = f == f'
1292 headIs f (PApp _ f' _) = headIs f f'
1293 headIs f _ = True -- keep if it's not an application
1295-- Rule out alternatives that don't return the same type as the head of the goal
1296-- (If there are none left as a result, do nothing)
1297pruneByType :: [Name] -> Term -> -- head of the goal
1298 Context -> [PTerm] -> [PTerm]
1299-- if an alternative has a locally bound name at the head, take it
1300pruneByType env t c as
1301 | Just a <- locallyBound as = [a]
1302 where
1303 locallyBound [] = Nothing
1304 locallyBound (t:ts)
1305 | Just n <- getName t,
1306 n `elem` env = Just t
1307 | otherwise = locallyBound ts
1308 getName (PRef _ n) = Just n
1309 getName (PApp _ f _) = getName f
1310 getName (PHidden t) = getName t
1311 getName _ = Nothing
1313pruneByType env (P _ n _) ctxt as
1314-- if the goal type is polymorphic, keep e
1315 | [] <- lookupTy n ctxt = as
1316 | otherwise
1317 = let asV = filter (headIs True n) as
1318 as' = filter (headIs False n) as in
1319 case as' of
1320 [] -> case asV of
1321 [] -> as
1322 _ -> asV
1323 _ -> as'
1324 where
1325 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
1326 headIs var f (PApp _ f' _) = headIs var f f'
1327 headIs var f (PPi _ _ _ sc) = headIs var f sc
1328 headIs var f (PHidden t) = headIs var f t
1329 headIs _ _ _ = True -- keep if it's not an application
1331 typeHead var f f'
1332 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
1333 case lookupTy f' ctxt of
1334 [ty] -> case unApply (getRetTy ty) of
1335 (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f
1336 _ -> let ty' = normalise ctxt [] ty in
1337 case unApply (getRetTy ty') of
1338 (P _ ftyn _, _) -> ftyn == f
1339 (V _, _) -> var -- keep, variable
1340 _ -> False
1341 _ -> False
1343pruneByType _ t _ as = as
1345findInstances :: IState -> Term -> [Name]
1346findInstances ist t
1347 | (P _ n _, _) <- unApply t
1348 = case lookupCtxt n (idris_classes ist) of
1349 [CI _ _ _ _ _ ins] -> ins
1350 _ -> []
1351 | otherwise = []
1353-- Try again to solve auto implicits
1354solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()
1355solveAuto ist fn ambigok n
1356 = do hs <- get_holes
1357 when (n `elem` hs) $ do
1358 focus n
1359 g <- goal
1360 isg <- is_guess -- if it's a guess, we're working on it recursively, so stop
1361 when (not isg) $
1362 proofSearch' ist True ambigok 100 True Nothing fn []
1364solveAutos :: IState -> Name -> Bool -> ElabD ()
1365solveAutos ist fn ambigok
1366 = do autos <- get_autos
1367 mapM_ (solveAuto ist fn ambigok) (map fst autos)
1369trivial' ist
1370 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1371proofSearch' ist rec ambigok depth prv top n hints
1372 = do unifyProblems
1373 proofSearch rec prv ambigok (not prv) depth
1374 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
1376-- Resolve type classes. This will only pick up 'normal' instances, never
1377-- named instances (hence using 'tcname' to check it's a generated instance
1378-- name).
1379resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
1380resolveTC = resTC' []
1382resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
1383resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
1384resTC' tcs defaultOn depth topg fn ist
1385 = do compute
1386 g <- goal
1387 ptm <- get_term
1388 ulog <- getUnifyLog
1389 hs <- get_holes
1390 traceWhen ulog ("Resolving class " ++ show g) $
1391 try' (trivial' ist)
1392 (do t <- goal
1393 let (tc, ttypes) = unApply t
1394 scopeOnly <- needsDefault t tc ttypes
1395 let stk = elab_stack ist
1396 let insts_in = findInstances ist t
1397 let insts = if scopeOnly then filter chaser insts_in
1398 else insts_in
1399 tm <- get_term
1400 let depth' = if scopeOnly then 2 else depth
1401 blunderbuss t depth' stk (stk ++ insts)) True
1402 where
1403 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
1404 | otherwise = (fail "Can't resolve", show n)
1406 -- HACK! Rather than giving a special name, better to have some kind
1407 -- of flag in ClassInfo structure
1408 chaser (UN nm)
1409 | ('@':'@':_) <- str nm = True -- old way
1410 chaser (SN (ParentN _ _)) = True
1411 chaser (NS n _) = chaser n
1412 chaser _ = False
1414 numclass = sNS (sUN "Num") ["Classes","Prelude"]
1416 needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
1417 = do focus a
1418 fill (RConstant (AType (ATInt ITBig))) -- default Integer
1419 solve
1420 return False
1421 needsDefault t f as
1422 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t
1423 needsDefault t f a = return False -- trace (show t) $ return ()
1425 boundVar (P Bound _ _) = True
1426 boundVar _ = False
1428 blunderbuss t d stk [] = do -- c <- get_env
1429 -- ps <- get_probs
1430 lift $ tfail $ CantResolve topg
1431 blunderbuss t d stk (n:ns)
1432 | n /= fn && (n `elem` stk || tcname n)
1433 = try' (resolve n d) (blunderbuss t d stk ns) True
1434 | otherwise = blunderbuss t d stk ns
1436 resolve n depth
1437 | depth == 0 = fail $ "Can't resolve type class"
1438 | otherwise
1439 = do t <- goal
1440 let (tc, ttypes) = unApply t
1441-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
1442-- else do
1443 -- if there's a hole in the goal, don't even try
1444 let imps = case lookupCtxtName n (idris_implicits ist) of
1445 [] -> []
1446 [args] -> map isImp (snd args) -- won't be overloaded!
1447 xs -> error "The impossible happened - overloading is not expected here!"
1448 ps <- get_probs
1449 tm <- get_term
1450 args <- map snd <$> try' (apply (Var n) imps)
1451 (match_apply (Var n) imps) True
1452 ps' <- get_probs
1453 when (length ps < length ps' || unrecoverable ps') $
1454 fail "Can't apply type class"
1455-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
1456 mapM_ (\ (_,n) -> do focus n
1457 t' <- goal
1458 let (tc', ttype) = unApply t'
1459 let got = fst (unApply t)
1460 let depth' = if tc' `elem` tcs
1461 then depth - 1 else depth
1462 resTC' (got : tcs) defaultOn depth' topg fn ist)
1463 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
1464 -- if there's any arguments left, we've failed to resolve
1465 hs <- get_holes
1466 ulog <- getUnifyLog
1467 solve
1468 traceWhen ulog ("Got " ++ show n) $ return ()
1469 where isImp (PImp p _ _ _ _) = (True, p)
1470 isImp arg = (False, priority arg)
1472collectDeferred :: Maybe Name ->
1473 Term -> State [(Name, (Int, Maybe Name, Type))] Term
1474collectDeferred top (Bind n (GHole i t) app) =
1475 do ds <- get
1476 t' <- collectDeferred top t
1477 when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
1478 collectDeferred top app
1479collectDeferred top (Bind n b t) = do b' <- cdb b
1480 t' <- collectDeferred top t
1481 return (Bind n b' t')
1482 where
1483 cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
1484 cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
1485 cdb b = do ty' <- collectDeferred top (binderTy b)
1486 return (b { binderTy = ty' })
1487collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
1488collectDeferred top t = return t
1490case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1491case_ ind autoSolve ist fn tm = do
1492 attack
1493 tyn <- getNameFrom (sMN 0 "ity")
1494 claim tyn RType
1495 valn <- getNameFrom (sMN 0 "ival")
1496 claim valn (Var tyn)
1497 letn <- getNameFrom (sMN 0 "irule")
1498 letbind letn (Var tyn) (Var valn)
1499 focus valn
1500 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1501 env <- get_env
1502 let (Just binding) = lookup letn env
1503 let val = binderVal binding
1504 if ind then induction (forget val)
1505 else casetac (forget val)
1506 when autoSolve solveAll
1508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1510 where
1511 eval = normaliseAll ctxt env . finalise
1512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1513 returnUnit = fmap fst $ get_type_val (Var unitCon)
1515 -- | Do a step in the reflected elaborator monad. The input is the
1516 -- step, the output is the (reflected) term returned.
1517 runTacTm :: Term -> ElabD Term
1518 runTacTm (unApply -> tac@(P _ n _, args))
1519 | n == tacN "prim__Solve", [] <- args
1520 = do solve
1521 returnUnit
1522 | n == tacN "prim__Goal", [] <- args
1523 = do (h:_) <- get_holes
1524 t <- goal
1525 fmap fst . get_type_val $
1526 rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1527 (reflectName h, reflect t)
1528 | n == tacN "prim__Holes", [] <- args
1529 = do hs <- get_holes
1530 fmap fst . get_type_val $
1531 mkList (Var $ reflm "TTName") (map reflectName hs)
1532 | n == tacN "prim__Guess", [] <- args
1533 = do ok <- is_guess
1534 if ok
1535 then do guess <- fmap forget get_guess
1536 fmap fst . get_type_val $
1537 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1538 (Var (reflm "TT")))
1539 guess
1540 else fmap fst . get_type_val $
1541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1542 (Var (reflm "TT"))
1543 | n == tacN "prim__SourceLocation", [] <- args
1544 = fmap fst . get_type_val $
1545 reflectFC fc
1546 | n == tacN "prim__Env", [] <- args
1547 = do env <- get_env
1548 fmap fst . get_type_val $ reflectEnv env
1549 | n == tacN "prim__Fail", [_a, errs] <- args
1550 = do parts <- reifyReportParts (eval errs)
1551 lift . tfail $ ReflectionError [parts] (Msg "")
1552 | n == tacN "prim__PureTactical", [_a, tm] <- args
1553 = return tm
1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1555 = do let first' = eval first
1556 res <- runTacTm first'
1557 let next = eval (App andThen res)
1558 runTacTm next
1559 | n == tacN "prim__Try", [_a, first, alt] <- args
1560 = do let first' = eval first
1561 let alt' = eval alt
1562 try' (runTacTm first') (runTacTm alt') True
1563 | n == tacN "prim__Fill", [raw] <- args
1564 = do raw' <- reifyRaw raw
1565 apply raw' []
1566 returnUnit
1567 | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args
1568 = do n <- getNameFrom (sMN 0 hint)
1569 fmap fst $ get_type_val (reflectName n)
1570 | n == tacN "prim__Claim", [n, ty] <- args
1571 = do n' <- reifyTTName n
1572 ty' <- reifyRaw ty
1573 claim n' ty'
1574 returnUnit
1575 | n == tacN "prim__Forget", [tt] <- args
1576 = do tt' <- reifyTT tt
1577 fmap fst . get_type_val $ reflect tt'
1578 | n == tacN "prim__Attack", [] <- args
1579 = do attack
1580 returnUnit
1581 | n == tacN "prim__Rewrite", [rule] <- args
1582 = do r <- reifyRaw rule
1583 rewrite r
1584 returnUnit
1585 | n == tacN "prim__Focus", [what] <- args
1586 = do n' <- reifyTTName what
1587 focus n'
1588 returnUnit
1589 | n == tacN "prim__Unfocus", [what] <- args
1590 = do n' <- reifyTTName what
1591 movelast n'
1592 returnUnit
1593 | n == tacN "prim__Intro", [mn] <- args
1594 = do n <- case fromTTMaybe mn of
1595 Nothing -> return Nothing
1596 Just name -> fmap Just $ reifyTTName name
1597 intro n
1598 returnUnit
1599 | n == tacN "prim__Debug", [ty, msg] <- args
1600 = do let msg' = fromTTMaybe msg
1601 case msg' of
1602 Nothing -> debugElaborator Nothing
1603 Just (Constant (Str m)) -> debugElaborator (Just m)
1604 Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x
1605 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1607-- Running tactics directly
1608-- if a tactic adds unification problems, return an error
1610runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
1611runTac autoSolve ist perhapsFC fn tac
1612 = do env <- get_env
1613 g <- goal
1614 let tac' = fmap (addImplBound ist (map fst env)) tac
1615 if autoSolve
1616 then runT tac'
1617 else no_errors (runT tac')
1618 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
1619 where
1620 runT (Intro []) = do g <- goal
1621 attack; intro (bname g)
1622 where
1623 bname (Bind n _ _) = Just n
1624 bname _ = Nothing
1625 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
1626 runT Intros = do g <- goal
1627 attack; intro (bname g)
1628 try' (runT Intros)
1629 (return ()) True
1630 where
1631 bname (Bind n _ _) = Just n
1632 bname _ = Nothing
1633 runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm
1634 when autoSolve solveAll
1635 runT (MatchRefine fn)
1636 = do fnimps <-
1637 case lookupCtxtName fn (idris_implicits ist) of
1638 [] -> do a <- envArgs fn
1639 return [(fn, a)]
1640 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
1641 let tacs = map (\ (fn', imps) ->
1642 (match_apply (Var fn') (map (\x -> (x, 0)) imps),
1643 fn')) fnimps
1644 tryAll tacs
1645 when autoSolve solveAll
1646 where envArgs n = do e <- get_env
1647 case lookup n e of
1648 Just t -> return $ map (const False)
1649 (getArgTys (binderTy t))
1650 _ -> return []
1651 runT (Refine fn [])
1652 = do fnimps <-
1653 case lookupCtxtName fn (idris_implicits ist) of
1654 [] -> do a <- envArgs fn
1655 return [(fn, a)]
1656 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
1657 let tacs = map (\ (fn', imps) ->
1658 (apply (Var fn') (map (\x -> (x, 0)) imps),
1659 fn')) fnimps
1660 tryAll tacs
1661 when autoSolve solveAll
1662 where isImp (PImp _ _ _ _ _) = True
1663 isImp _ = False
1664 envArgs n = do e <- get_env
1665 case lookup n e of
1666 Just t -> return $ map (const False)
1667 (getArgTys (binderTy t))
1668 _ -> return []
1669 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
1670 when autoSolve solveAll
1671 runT DoUnify = do unify_all
1672 when autoSolve solveAll
1673 runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")
1674 claim tmHole RType
1675 claim n (Var tmHole)
1676 focus tmHole
1677 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1678 focus n
1679 runT (Equiv tm) -- let bind tm, then
1680 = do attack
1681 tyn <- getNameFrom (sMN 0 "ety")
1682 claim tyn RType
1683 valn <- getNameFrom (sMN 0 "eqval")
1684 claim valn (Var tyn)
1685 letn <- getNameFrom (sMN 0 "equiv_val")
1686 letbind letn (Var tyn) (Var valn)
1687 focus tyn
1688 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1689 focus valn
1690 when autoSolve solveAll
1691 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
1692 = do attack; -- (h:_) <- get_holes
1693 tyn <- getNameFrom (sMN 0 "rty")
1694 -- start_unify h
1695 claim tyn RType
1696 valn <- getNameFrom (sMN 0 "rval")
1697 claim valn (Var tyn)
1698 letn <- getNameFrom (sMN 0 "rewrite_rule")
1699 letbind letn (Var tyn) (Var valn)
1700 focus valn
1701 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1702 rewrite (Var letn)
1703 when autoSolve solveAll
1704 runT (Induction tm) -- let bind tm, similar to the others
1705 = case_ True autoSolve ist fn tm
1706 runT (CaseTac tm)
1707 = case_ False autoSolve ist fn tm
1708 runT (LetTac n tm)
1709 = do attack
1710 tyn <- getNameFrom (sMN 0 "letty")
1711 claim tyn RType
1712 valn <- getNameFrom (sMN 0 "letval")
1713 claim valn (Var tyn)
1714 letn <- unique_hole n
1715 letbind letn (Var tyn) (Var valn)
1716 focus valn
1717 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1718 when autoSolve solveAll
1719 runT (LetTacTy n ty tm)
1720 = do attack
1721 tyn <- getNameFrom (sMN 0 "letty")
1722 claim tyn RType
1723 valn <- getNameFrom (sMN 0 "letval")
1724 claim valn (Var tyn)
1725 letn <- unique_hole n
1726 letbind letn (Var tyn) (Var valn)
1727 focus tyn
1728 elab ist toplevel ERHS [] (sMN 0 "tac") ty
1729 focus valn
1730 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1731 when autoSolve solveAll
1732 runT Compute = compute
1733 runT Trivial = do trivial' ist; when autoSolve solveAll
1734 runT TCInstance = runT (Exact (PResolveTC emptyFC))
1735 runT (ProofSearch rec prover depth top hints)
1736 = do proofSearch' ist rec False depth prover top fn hints
1737 when autoSolve solveAll
1738 runT (Focus n) = focus n
1739 runT Unfocus = do hs <- get_holes
1740 case hs of
1741 [] -> return ()
1742 (h : _) -> movelast h
1743 runT Solve = solve
1744 runT (Try l r) = do try' (runT l) (runT r) True
1745 runT (TSeq l r) = do runT l; runT r
1746 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
1747 tgoal <- goal -- store the goal
1748 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
1749 script <- getNameFrom (sMN 0 "script")
1750 claim script scriptTy
1751 scriptvar <- getNameFrom (sMN 0 "scriptvar" )
1752 letbind scriptvar scriptTy (Var script)
1753 focus script
1754 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1755 (script', _) <- get_type_val (Var scriptvar)
1756 -- now that we have the script apply
1757 -- it to the reflected goal and context
1758 restac <- getNameFrom (sMN 0 "restac")
1759 claim restac tacticTy
1760 focus restac
1761 fill (raw_apply (forget script')
1762 [reflectEnv tenv, reflect tgoal])
1763 restac' <- get_guess
1764 solve
1765 -- normalise the result in order to
1766 -- reify it
1767 ctxt <- get_context
1768 env <- get_env
1769 let tactic = normalise ctxt env restac'
1770 runReflected tactic
1771 where tacticTy = Var (reflm "Tactic")
1772 listTy = Var (sNS (sUN "List") ["List", "Prelude"])
1773 scriptTy = (RBind (sMN 0 "__pi_arg")
1774 (Pi Nothing (RApp listTy envTupleType) RType)
1775 (RBind (sMN 1 "__pi_arg")
1776 (Pi Nothing (Var $ reflm "TT") RType) tacticTy))
1777 runT (ByReflection tm) -- run the reflection function 'tm' on the
1778 -- goal, then apply the resulting reflected Tactic
1779 = do tgoal <- goal
1780 attack
1781 script <- getNameFrom (sMN 0 "script")
1782 claim script scriptTy
1783 scriptvar <- getNameFrom (sMN 0 "scriptvar" )
1784 letbind scriptvar scriptTy (Var script)
1785 focus script
1786 ptm <- get_term
1787 elab ist toplevel ERHS [] (sMN 0 "tac")
1788 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
1789 (script', _) <- get_type_val (Var scriptvar)
1790 -- now that we have the script apply
1791 -- it to the reflected goal
1792 restac <- getNameFrom (sMN 0 "restac")
1793 claim restac tacticTy
1794 focus restac
1795 fill (forget script')
1796 restac' <- get_guess
1797 solve
1798 -- normalise the result in order to
1799 -- reify it
1800 ctxt <- get_context
1801 env <- get_env
1802 let tactic = normalise ctxt env restac'
1803 runReflected tactic
1804 where tacticTy = Var (reflm "Tactic")
1805 scriptTy = tacticTy
1807 runT (Reflect v) = do attack -- let x = reflect v in ...
1808 tyn <- getNameFrom (sMN 0 "letty")
1809 claim tyn RType
1810 valn <- getNameFrom (sMN 0 "letval")
1811 claim valn (Var tyn)
1812 letn <- getNameFrom (sMN 0 "letvar")
1813 letbind letn (Var tyn) (Var valn)
1814 focus valn
1815 elab ist toplevel ERHS [] (sMN 0 "tac") v
1816 (value, _) <- get_type_val (Var letn)
1817 ctxt <- get_context
1818 env <- get_env
1819 let value' = hnf ctxt env value
1820 runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))
1821 runT (Fill v) = do attack -- let x = fill x in ...
1822 tyn <- getNameFrom (sMN 0 "letty")
1823 claim tyn RType
1824 valn <- getNameFrom (sMN 0 "letval")
1825 claim valn (Var tyn)
1826 letn <- getNameFrom (sMN 0 "letvar")
1827 letbind letn (Var tyn) (Var valn)
1828 focus valn
1829 elab ist toplevel ERHS [] (sMN 0 "tac") v
1830 (value, _) <- get_type_val (Var letn)
1831 ctxt <- get_context
1832 env <- get_env
1833 let value' = normalise ctxt env value
1834 rawValue <- reifyRaw value'
1835 runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)
1836 runT (GoalType n tac) = do g <- goal
1837 case unApply g of
1838 (P _ n' _, _) ->
1839 if nsroot n' == sUN n
1840 then runT tac
1841 else fail "Wrong goal type"
1842 _ -> fail "Wrong goal type"
1843 runT ProofState = do g <- goal
1844 return ()
1845 runT Skip = return ()
1846 runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")
1847 runT SourceFC =
1848 case perhapsFC of
1849 Nothing -> lift . tfail $ Msg "There is no source location available."
1850 Just fc ->
1851 do fill $ reflectFC fc
1852 solve
1853 runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"
1854 runT x = fail $ "Not implemented " ++ show x
1856 runReflected t = do t' <- reify ist t
1857 runTac autoSolve ist perhapsFC fn t'
1859-- | Prefix a name with the "Language.Reflection" namespace
1860reflm :: String -> Name
1861reflm n = sNS (sUN n) ["Reflection", "Language"]
1864-- | Reify tactics from their reflected representation
1865reify :: IState -> Term -> ElabD PTactic
1866reify _ (P _ n _) | n == reflm "Intros" = return Intros
1867reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
1868reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
1869reify _ (P _ n _) | n == reflm "Solve" = return Solve
1870reify _ (P _ n _) | n == reflm "Compute" = return Compute
1871reify _ (P _ n _) | n == reflm "Skip" = return Skip
1872reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
1873reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
1874reify ist t@(App _ _)
1875 | (P _ f _, args) <- unApply t = reifyApp ist f args
1876reify _ t = fail ("Unknown tactic " ++ show t)
1878reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
1879reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1880reifyApp _ t [Constant (I i)]
1881 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
1882reifyApp _ t [x]
1883 | t == reflm "Refine" = do n <- reifyTTName x
1884 return $ Refine n []
1885reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
1886 goal <- reifyTT ty
1887 return $ Claim n' (delab ist goal)
1888reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
1889reifyApp ist t [Constant (Str n), x]
1890 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1891reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1892reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
1893reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
1894reifyApp ist t [t']
1895 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
1896reifyApp ist t [t']
1897 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
1898reifyApp ist t [t']
1899 | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
1900reifyApp _ t [t']
1901 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
1902reifyApp ist t [t']
1903 | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
1904reifyApp ist t [x]
1905 | t == reflm "Focus" = liftM Focus (reifyTTName x)
1906reifyApp ist t [t']
1907 | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
1908reifyApp ist t [n, t']
1909 | t == reflm "LetTac" = do n' <- reifyTTName n
1910 t'' <- reifyTT t'
1911 return $ LetTac n' (delab ist t')
1912reifyApp ist t [n, tt', t']
1913 | t == reflm "LetTacTy" = do n' <- reifyTTName n
1914 tt'' <- reifyTT tt'
1915 t'' <- reifyTT t'
1916 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
1917reifyApp ist t [errs]
1918 | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
1919reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
1921reifyReportParts :: Term -> ElabD [ErrorReportPart]
1922reifyReportParts errs =
1923 case unList errs of
1924 Nothing -> fail "Failed to reify errors"
1925 Just errs' ->
1926 let parts = mapM reifyReportPart errs' in
1927 case parts of
1928 Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1929 Right errs'' ->
1930 return errs''
1932-- | Reify terms from their reflected representation
1933reifyTT :: Term -> ElabD Term
1934reifyTT t@(App _ _)
1935 | (P _ f _, args) <- unApply t = reifyTTApp f args
1936reifyTT t@(P _ n _)
1937 | n == reflm "Erased" = return $ Erased
1938reifyTT t@(P _ n _)
1939 | n == reflm "Impossible" = return $ Impossible
1940reifyTT t = fail ("Unknown reflection term: " ++ show t)
1942reifyTTApp :: Name -> [Term] -> ElabD Term
1943reifyTTApp t [nt, n, x]
1944 | t == reflm "P" = do nt' <- reifyTTNameType nt
1945 n' <- reifyTTName n
1946 x' <- reifyTT x
1947 return $ P nt' n' x'
1948reifyTTApp t [Constant (I i)]
1949 | t == reflm "V" = return $ V i
1950reifyTTApp t [n, b, x]
1951 | t == reflm "Bind" = do n' <- reifyTTName n
1952 b' <- reifyTTBinder reifyTT (reflm "TT") b
1953 x' <- reifyTT x
1954 return $ Bind n' b' x'
1955reifyTTApp t [f, x]
1956 | t == reflm "App" = do f' <- reifyTT f
1957 x' <- reifyTT x
1958 return $ App f' x'
1959reifyTTApp t [c]
1960 | t == reflm "TConst" = liftM Constant (reifyTTConst c)
1961reifyTTApp t [t', Constant (I i)]
1962 | t == reflm "Proj" = do t'' <- reifyTT t'
1963 return $ Proj t'' i
1964reifyTTApp t [tt]
1965 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
1966reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
1968-- | Reify raw terms from their reflected representation
1969reifyRaw :: Term -> ElabD Raw
1970reifyRaw t@(App _ _)
1971 | (P _ f _, args) <- unApply t = reifyRawApp f args
1972reifyRaw t@(P _ n _)
1973 | n == reflm "RType" = return $ RType
1974reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
1976reifyRawApp :: Name -> [Term] -> ElabD Raw
1977reifyRawApp t [n]
1978 | t == reflm "Var" = liftM Var (reifyTTName n)
1979reifyRawApp t [n, b, x]
1980 | t == reflm "RBind" = do n' <- reifyTTName n
1981 b' <- reifyTTBinder reifyRaw (reflm "Raw") b
1982 x' <- reifyRaw x
1983 return $ RBind n' b' x'
1984reifyRawApp t [f, x]
1985 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
1986reifyRawApp t [t']
1987 | t == reflm "RForce" = liftM RForce (reifyRaw t')
1988reifyRawApp t [c]
1989 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
1990reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
1992reifyTTName :: Term -> ElabD Name
1993reifyTTName t
1994 | (P _ f _, args) <- unApply t = reifyTTNameApp f args
1995reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
1997reifyTTNameApp :: Name -> [Term] -> ElabD Name
1998reifyTTNameApp t [Constant (Str n)]
1999 | t == reflm "UN" = return $ sUN n
2000reifyTTNameApp t [n, ns]
2001 | t == reflm "NS" = do n' <- reifyTTName n
2002 ns' <- reifyTTNamespace ns
2003 return $ sNS n' ns'
2004reifyTTNameApp t [Constant (I i), Constant (Str n)]
2005 | t == reflm "MN" = return $ sMN i n
2006reifyTTNameApp t []
2007 | t == reflm "NErased" = return NErased
2008reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
2010reifyTTNamespace :: Term -> ElabD [String]
2011reifyTTNamespace t@(App _ _)
2012 = case unApply t of
2013 (P _ f _, [Constant StrType])
2014 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
2015 (P _ f _, [Constant StrType, Constant (Str n), ns])
2016 | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
2017 _ -> fail ("Unknown reflection namespace arg: " ++ show t)
2018reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
2020reifyTTNameType :: Term -> ElabD NameType
2021reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
2022reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
2023reifyTTNameType t@(App _ _)
2024 = case unApply t of
2025 (P _ f _, [Constant (I tag), Constant (I num)])
2026 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
2027 | f == reflm "TCon" -> return $ TCon tag num
2028 _ -> fail ("Unknown reflection name type: " ++ show t)
2029reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
2031reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
2032reifyTTBinder reificator binderType t@(App _ _)
2033 = case unApply t of
2034 (P _ f _, bt:args) | forget bt == Var binderType
2035 -> reifyTTBinderApp reificator f args
2036 _ -> fail ("Mismatching binder reflection: " ++ show t)
2037reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
2039reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
2040reifyTTBinderApp reif f [t]
2041 | f == reflm "Lam" = liftM Lam (reif t)
2042reifyTTBinderApp reif f [t, k]
2043 | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
2044reifyTTBinderApp reif f [x, y]
2045 | f == reflm "Let" = liftM2 Let (reif x) (reif y)
2046reifyTTBinderApp reif f [x, y]
2047 | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
2048reifyTTBinderApp reif f [t]
2049 | f == reflm "Hole" = liftM Hole (reif t)
2050reifyTTBinderApp reif f [t]
2051 | f == reflm "GHole" = liftM (GHole 0) (reif t)
2052reifyTTBinderApp reif f [x, y]
2053 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
2054reifyTTBinderApp reif f [t]
2055 | f == reflm "PVar" = liftM PVar (reif t)
2056reifyTTBinderApp reif f [t]
2057 | f == reflm "PVTy" = liftM PVTy (reif t)
2058reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
2060reifyTTConst :: Term -> ElabD Const
2061reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
2062reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
2063reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
2064reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
2065reifyTTConst t@(App _ _)
2066 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
2067reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
2069reifyTTConstApp :: Name -> Term -> ElabD Const
2070reifyTTConstApp f aty
2071 | f == reflm "AType" = fmap AType (reifyArithTy aty)
2072reifyTTConstApp f (Constant c@(I _))
2073 | f == reflm "I" = return $ c
2074reifyTTConstApp f (Constant c@(BI _))
2075 | f == reflm "BI" = return $ c
2076reifyTTConstApp f (Constant c@(Fl _))
2077 | f == reflm "Fl" = return $ c
2078reifyTTConstApp f (Constant c@(I _))
2079 | f == reflm "Ch" = return $ c
2080reifyTTConstApp f (Constant c@(Str _))
2081 | f == reflm "Str" = return $ c
2082reifyTTConstApp f (Constant c@(B8 _))
2083 | f == reflm "B8" = return $ c
2084reifyTTConstApp f (Constant c@(B16 _))
2085 | f == reflm "B16" = return $ c
2086reifyTTConstApp f (Constant c@(B32 _))
2087 | f == reflm "B32" = return $ c
2088reifyTTConstApp f (Constant c@(B64 _))
2089 | f == reflm "B64" = return $ c
2090reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
2092reifyArithTy :: Term -> ElabD ArithTy
2093reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
2094reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
2095reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
2097reifyNativeTy :: Term -> ElabD NativeTy
2098reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2099reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2100reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2101reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2102reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
2104reifyIntTy :: Term -> ElabD IntTy
2105reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
2106reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
2107reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
2108reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2109reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
2110 (reifyNativeTy nt)
2111reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
2113reifyTTUExp :: Term -> ElabD UExp
2114reifyTTUExp t@(App _ _)
2115 = case unApply t of
2116 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
2117 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
2118 _ -> fail ("Unknown reflection type universe expression: " ++ show t)
2119reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
2121-- | Create a reflected call to a named function/constructor
2122reflCall :: String -> [Raw] -> Raw
2123reflCall funName args
2124 = raw_apply (Var (reflm funName)) args
2126-- | Lift a term into its Language.Reflection.TT representation
2127reflect :: Term -> Raw
2128reflect = reflectTTQuote []
2130-- | Lift a term into its Language.Reflection.Raw representation
2131reflectRaw :: Raw -> Raw
2132reflectRaw = reflectRawQuote []
2134claimTT :: Name -> ElabD Name
2135claimTT n = do n' <- getNameFrom n
2136 claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
2137 return n'
2139-- | Convert a reflected term to a more suitable form for pattern-matching.
2140-- In particular, the less-interesting bits are elaborated to _ patterns. This
2141-- happens to NameTypes, universe levels, names that are bound but not used,
2142-- and the type annotation field of the P constructor.
2143reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2144reflectTTQuotePattern unq (P _ n _)
2145 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2146 do fill (Var n) ; solve
2147 | otherwise =
2148 do tyannot <- claimTT (sMN 0 "pTyAnnot")
2149 movelast tyannot -- use a _ pattern here
2150 nt <- getNameFrom (sMN 0 "nt")
2151 claim nt (Var (reflm "NameType"))
2152 movelast nt -- use a _ pattern here
2153 n' <- getNameFrom (sMN 0 "n")
2154 claim n' (Var (reflm "TTName"))
2155 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2156 solve
2157 focus n'; reflectNameQuotePattern n
2158reflectTTQuotePattern unq (V n)
2159 = do fill $ reflCall "V" [RConstant (I n)]
2160 solve
2161reflectTTQuotePattern unq (Bind n b x)
2162 = do x' <- claimTT (sMN 0 "sc")
2163 movelast x'
2164 b' <- getNameFrom (sMN 0 "binder")
2165 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
2166 (Var (sNS (sUN "TT") ["Reflection", "Language"])))
2167 if n `elem` freeNames x
2168 then do fill $ reflCall "Bind"
2169 [reflectName n,
2170 Var b',
2171 Var x']
2172 solve
2173 else do any <- getNameFrom (sMN 0 "anyName")
2174 claim any (Var (reflm "TTName"))
2175 movelast any
2176 fill $ reflCall "Bind"
2177 [Var any,
2178 Var b',
2179 Var x']
2180 solve
2181 focus x'; reflectTTQuotePattern unq x
2182 focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
2183reflectTTQuotePattern unq (App f x)
2184 = do f' <- claimTT (sMN 0 "f"); movelast f'
2185 x' <- claimTT (sMN 0 "x"); movelast x'
2186 fill $ reflCall "App" [Var f', Var x']
2187 solve
2188 focus f'; reflectTTQuotePattern unq f
2189 focus x'; reflectTTQuotePattern unq x
2190reflectTTQuotePattern unq (Constant c)
2191 = do fill $ reflCall "TConst" [reflectConstant c]
2192 solve
2193reflectTTQuotePattern unq (Proj t i)
2194 = do t' <- claimTT (sMN 0 "t"); movelast t'
2195 fill $ reflCall "Proj" [Var t', RConstant (I i)]
2196 solve
2197 focus t'; reflectTTQuotePattern unq t
2198reflectTTQuotePattern unq (Erased)
2199 = do erased <- claimTT (sMN 0 "erased")
2200 movelast erased
2201 fill $ (Var erased)
2202 solve
2203reflectTTQuotePattern unq (Impossible)
2204 = do fill $ Var (reflm "Impossible")
2205 solve
2206reflectTTQuotePattern unq (TType exp)
2207 = do ue <- getNameFrom (sMN 0 "uexp")
2208 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2209 movelast ue
2210 fill $ reflCall "TType" [Var ue]
2211 solve
2212reflectTTQuotePattern unq (UType u)
2213 = do uH <- getNameFrom (sMN 0 "someUniv")
2214 claim uH (Var (reflm "Universe"))
2215 movelast uH
2216 fill $ reflCall "UType" [Var uH]
2217 solve
2218 focus uH
2219 fill (Var (reflm (case u of
2220 NullType -> "NullType"
2221 UniqueType -> "UniqueType"
2222 AllTypes -> "AllTypes")))
2223 solve
2225reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
2226reflectRawQuotePattern unq (Var n)
2227 -- the unquoted names already have types, just use them
2228 | n `elem` unq = do fill (Var n); solve
2229 | otherwise = do fill (reflCall "Var" [reflectName n]); solve
2230reflectRawQuotePattern unq (RBind n b sc) =
2231 do scH <- getNameFrom (sMN 0 "sc")
2232 claim scH (Var (reflm "Raw"))
2233 movelast scH
2234 bH <- getNameFrom (sMN 0 "binder")
2235 claim bH (RApp (Var (reflm "Binder"))
2236 (Var (reflm "Raw")))
2237 if n `elem` freeNamesR sc
2238 then do fill $ reflCall "RBind" [reflectName n,
2239 Var bH,
2240 Var scH]
2241 solve
2242 else do any <- getNameFrom (sMN 0 "anyName")
2243 claim any (Var (reflm "TTName"))
2244 movelast any
2245 fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2246 solve
2247 focus scH; reflectRawQuotePattern unq sc
2248 focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
2249 where freeNamesR (Var n) = [n]
2250 freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
2251 freeNamesR body \\ [n],
2252 freeNamesR t]
2253 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
2254 (freeNamesR body \\ [n])
2255 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
2256 freeNamesR RType = []
2257 freeNamesR (RUType _) = []
2258 freeNamesR (RForce r) = freeNamesR r
2259 freeNamesR (RConstant _) = []
2260reflectRawQuotePattern unq (RApp f x) =
2261 do fH <- getNameFrom (sMN 0 "f")
2262 claim fH (Var (reflm "Raw"))
2263 movelast fH
2264 xH <- getNameFrom (sMN 0 "x")
2265 claim xH (Var (reflm "Raw"))
2266 movelast xH
2267 fill $ reflCall "RApp" [Var fH, Var xH]
2268 solve
2269 focus fH; reflectRawQuotePattern unq f
2270 focus xH; reflectRawQuotePattern unq x
2271reflectRawQuotePattern unq RType =
2272 do fill (Var (reflm "RType"))
2273 solve
2274reflectRawQuotePattern unq (RUType univ) =
2275 do uH <- getNameFrom (sMN 0 "universe")
2276 claim uH (Var (reflm "Universe"))
2277 movelast uH
2278 fill $ reflCall "RUType" [Var uH]
2279 solve
2280 focus uH; fill (reflectUniverse univ); solve
2281reflectRawQuotePattern unq (RForce r) =
2282 do rH <- getNameFrom (sMN 0 "raw")
2283 claim rH (Var (reflm "Raw"))
2284 movelast rH
2285 fill $ reflCall "RForce" [Var rH]
2286 solve
2287 focus rH; reflectRawQuotePattern unq r
2288reflectRawQuotePattern unq (RConstant c) =
2289 do cH <- getNameFrom (sMN 0 "const")
2290 claim cH (Var (reflm "Constant"))
2291 movelast cH
2292 fill (reflCall "RConstant" [Var cH]); solve
2293 focus cH
2294 fill (reflectConstant c); solve
2296reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
2297reflectBinderQuotePattern q unq (Lam t)
2298 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2299 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2300 solve
2301 focus t'; q unq t
2302reflectBinderQuotePattern q unq (Pi _ t k)
2303 = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2304 k' <- claimTT (sMN 0 "k"); movelast k';
2305 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2306 solve
2307 focus t'; q unq t
2308reflectBinderQuotePattern q unq (Let x y)
2309 = do x' <- claimTT (sMN 0 "ty"); movelast x';
2310 y' <- claimTT (sMN 0 "v"); movelast y';
2311 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2312 solve
2313 focus x'; q unq x
2314 focus y'; q unq y
2315reflectBinderQuotePattern q unq (NLet x y)
2316 = do x' <- claimTT (sMN 0 "ty"); movelast x'
2317 y' <- claimTT (sMN 0 "v"); movelast y'
2318 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2319 solve
2320 focus x'; q unq x
2321 focus y'; q unq y
2322reflectBinderQuotePattern q unq (Hole t)
2323 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2324 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2325 solve
2326 focus t'; q unq t
2327reflectBinderQuotePattern q unq (GHole _ t)
2328 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2329 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2330 solve
2331 focus t'; q unq t
2332reflectBinderQuotePattern q unq (Guess x y)
2333 = do x' <- claimTT (sMN 0 "ty"); movelast x'
2334 y' <- claimTT (sMN 0 "v"); movelast y'
2335 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2336 solve
2337 focus x'; q unq x
2338 focus y'; q unq y
2339reflectBinderQuotePattern q unq (PVar t)
2340 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2341 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2342 solve
2343 focus t'; q unq t
2344reflectBinderQuotePattern q unq (PVTy t)
2345 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2346 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2347 solve
2348 focus t'; q unq t
2350reflectUniverse :: Universe -> Raw
2351reflectUniverse u =
2352 (Var (reflm (case u of
2353 NullType -> "NullType"
2354 UniqueType -> "UniqueType"
2355 AllTypes -> "AllTypes")))
2357-- | Create a reflected TT term, but leave refs to the provided name intact
2358reflectTTQuote :: [Name] -> Term -> Raw
2359reflectTTQuote unq (P nt n t)
2360 | n `elem` unq = Var n
2361 | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2362reflectTTQuote unq (V n)
2363 = reflCall "V" [RConstant (I n)]
2364reflectTTQuote unq (Bind n b x)
2365 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2366reflectTTQuote unq (App f x)
2367 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2368reflectTTQuote unq (Constant c)
2369 = reflCall "TConst" [reflectConstant c]
2370reflectTTQuote unq (Proj t i)
2371 = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2372reflectTTQuote unq (Erased) = Var (reflm "Erased")
2373reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2374reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2375reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2377reflectRawQuote :: [Name] -> Raw -> Raw
2378reflectRawQuote unq (Var n)
2379 | n `elem` unq = Var n
2380 | otherwise = reflCall "Var" [reflectName n]
2381reflectRawQuote unq (RBind n b r) =
2382 reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]
2383reflectRawQuote unq (RApp f x) =
2384 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2385reflectRawQuote unq RType = Var (reflm "RType")
2386reflectRawQuote unq (RUType u) =
2387 reflCall "RUType" [reflectUniverse u]
2388reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2389reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
2391reflectNameType :: NameType -> Raw
2392reflectNameType (Bound) = Var (reflm "Bound")
2393reflectNameType (Ref) = Var (reflm "Ref")
2394reflectNameType (DCon x y _)
2395 = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
2396reflectNameType (TCon x y)
2397 = reflCall "TCon" [RConstant (I x), RConstant (I y)]
2399reflectName :: Name -> Raw
2400reflectName (UN s)
2401 = reflCall "UN" [RConstant (Str (str s))]
2402reflectName (NS n ns)
2403 = reflCall "NS" [ reflectName n
2404 , foldr (\ n s ->
2405 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
2406 [ RConstant StrType, RConstant (Str n), s ])
2407 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
2408 [ RConstant StrType ])
2409 (map str ns)
2411reflectName (MN i n)
2412 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
2413reflectName (NErased) = Var (reflm "NErased")
2414reflectName n = Var (reflm "NErased") -- special name, not yet implemented
2416-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
2417-- MNs corresponding to will care about the string but not the number. All
2418-- others become _.
2419reflectNameQuotePattern :: Name -> ElabD ()
2420reflectNameQuotePattern n@(UN s)
2421 = do fill $ reflectName n
2422 solve
2423reflectNameQuotePattern n@(NS _ _)
2424 = do fill $ reflectName n
2425 solve
2426reflectNameQuotePattern (MN _ n)
2427 = do i <- getNameFrom (sMN 0 "mnCounter")
2428 claim i (RConstant (AType (ATInt ITNative)))
2429 movelast i
2430 fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
2431 solve
2432reflectNameQuotePattern _ -- for all other names, match any
2433 = do nameHole <- getNameFrom (sMN 0 "name")
2434 claim nameHole (Var (reflm "TTName"))
2435 movelast nameHole
2436 fill (Var nameHole)
2437 solve
2439reflectBinder :: Binder Term -> Raw
2440reflectBinder = reflectBinderQuote reflectTTQuote []
2442reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2443reflectBinderQuote q unq (Lam t)
2444 = reflCall "Lam" [Var (reflm "TT"), q unq t]
2445reflectBinderQuote q unq (Pi _ t k)
2446 = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2447reflectBinderQuote q unq (Let x y)
2448 = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2449reflectBinderQuote q unq (NLet x y)
2450 = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2451reflectBinderQuote q unq (Hole t)
2452 = reflCall "Hole" [Var (reflm "TT"), q unq t]
2453reflectBinderQuote q unq (GHole _ t)
2454 = reflCall "GHole" [Var (reflm "TT"), q unq t]
2455reflectBinderQuote q unq (Guess x y)
2456 = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2457reflectBinderQuote q unq (PVar t)
2458 = reflCall "PVar" [Var (reflm "TT"), q unq t]
2459reflectBinderQuote q unq (PVTy t)
2460 = reflCall "PVTy" [Var (reflm "TT"), q unq t]
2462mkList :: Raw -> [Raw] -> Raw
2463mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
2464mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
2465 x)
2466 (mkList ty xs)
2468reflectConstant :: Const -> Raw
2469reflectConstant c@(I _) = reflCall "I" [RConstant c]
2470reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
2471reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
2472reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
2473reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
2474reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
2475reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
2476reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
2477reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
2478reflectConstant (B8V ws) = reflCall "B8V" [mkList (Var (sUN "Bits8")) . map (RConstant . B8) . V.toList $ ws]
2479reflectConstant (B16V ws) = reflCall "B8V" [mkList (Var (sUN "Bits16")) . map (RConstant . B16) . V.toList $ ws]
2480reflectConstant (B32V ws) = reflCall "B8V" [mkList (Var (sUN "Bits32")) . map (RConstant . B32) . V.toList $ ws]
2481reflectConstant (B64V ws) = reflCall "B8V" [mkList (Var (sUN "Bits64")) . map (RConstant . B64) . V.toList $ ws]
2482reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
2483reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
2484reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
2485reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
2486reflectConstant StrType = Var (reflm "StrType")
2487reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
2488reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
2489reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
2490reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
2491reflectConstant (AType (ATInt (ITVec IT8 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT8"), RConstant (I c)]]]
2492reflectConstant (AType (ATInt (ITVec IT16 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT16"), RConstant (I c)]]]
2493reflectConstant (AType (ATInt (ITVec IT32 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT32"), RConstant (I c)]]]
2494reflectConstant (AType (ATInt (ITVec IT64 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT64"), RConstant (I c)]]]
2495reflectConstant PtrType = Var (reflm "PtrType")
2496reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
2497reflectConstant BufferType = Var (reflm "BufferType")
2498reflectConstant VoidType = Var (reflm "VoidType")
2499reflectConstant Forgot = Var (reflm "Forgot")
2500reflectConstant WorldType = Var (reflm "WorldType")
2501reflectConstant TheWorld = Var (reflm "TheWorld")
2503reflectUExp :: UExp -> Raw
2504reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2505reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
2507-- | Reflect the environment of a proof into a List (TTName, Binder TT)
2508reflectEnv :: Env -> Raw
2509reflectEnv = foldr consToEnvList emptyEnvList
2510 where
2511 consToEnvList :: (Name, Binder Term) -> Raw -> Raw
2512 consToEnvList (n, b) l
2513 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
2514 [ envTupleType
2515 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
2516 , (RApp (Var $ reflm "Binder")
2517 (Var $ reflm "TT"))
2518 , reflectName n
2519 , reflectBinder b
2521 , l
2524 emptyEnvList :: Raw
2525 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
2526 [envTupleType]
2528-- | Reflect an error into the internal datatype of Idris -- TODO
2529rawBool :: Bool -> Raw
2530rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
2531rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
2533rawNil :: Raw -> Raw
2534rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
2536rawCons :: Raw -> Raw -> Raw -> Raw
2537rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
2539rawList :: Raw -> [Raw] -> Raw
2540rawList ty = foldr (rawCons ty) (rawNil ty)
2542rawPairTy :: Raw -> Raw -> Raw
2543rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
2545rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
2546rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
2548reflectCtxt :: [(Name, Type)] -> Raw
2549reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
2550 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
2551 (reflectName n, reflect t)))
2552 ctxt)
2554reflectErr :: Err -> Raw
2555reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
2556reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
2557reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
2558 raw_apply (Var $ reflErrName "CantUnify")
2559 [ rawBool b
2560 , reflect t1
2561 , reflect t2
2562 , reflectErr e
2563 , reflectCtxt ctxt
2564 , RConstant (I i)]
2565reflectErr (InfiniteUnify n tm ctxt) =
2566 raw_apply (Var $ reflErrName "InfiniteUnify")
2567 [ reflectName n
2568 , reflect tm
2569 , reflectCtxt ctxt
2571reflectErr (CantConvert t t' ctxt) =
2572 raw_apply (Var $ reflErrName "CantConvert")
2573 [ reflect t
2574 , reflect t'
2575 , reflectCtxt ctxt
2577reflectErr (CantSolveGoal t ctxt) =
2578 raw_apply (Var $ reflErrName "CantSolveGoal")
2579 [ reflect t
2580 , reflectCtxt ctxt
2582reflectErr (UnifyScope n n' t ctxt) =
2583 raw_apply (Var $ reflErrName "UnifyScope")
2584 [ reflectName n
2585 , reflectName n'
2586 , reflect t
2587 , reflectCtxt ctxt
2589reflectErr (CantInferType str) =
2590 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
2591reflectErr (NonFunctionType t t') =
2592 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
2593reflectErr (NotEquality t t') =
2594 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
2595reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
2596reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
2597reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
2598reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
2599reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
2600reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
2601reflectErr (NotInjective t1 t2 t3) =
2602 raw_apply (Var $ reflErrName "NotInjective")
2603 [ reflect t1
2604 , reflect t2
2605 , reflect t3
2607reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
2608reflectErr (CantResolveAlts ss) =
2609 raw_apply (Var $ reflErrName "CantResolveAlts")
2610 [rawList (Var $ reflm "TTName") (map reflectName ss)]
2611reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
2612reflectErr UniverseError = Var $ reflErrName "UniverseError"
2613reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
2614reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
2615reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
2616reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
2617reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
2618reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
2619reflectErr (ProviderError str) =
2620 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
2621reflectErr (LoadingFailed str err) =
2622 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2623reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2625-- | Reflect a file context
2626reflectFC :: FC -> Raw
2627reflectFC fc = raw_apply (Var (reflm "FileLoc"))
2628 [ RConstant (Str (fc_fname fc))
2629 , raw_apply (Var pairCon) $
2630 [intTy, intTy] ++
2631 map (RConstant . I)
2632 [ fst (fc_start fc)
2633 , snd (fc_start fc)
2635 , raw_apply (Var pairCon) $
2636 [intTy, intTy] ++
2637 map (RConstant . I)
2638 [ fst (fc_end fc)
2639 , snd (fc_end fc)
2642 where intTy = RConstant (AType (ATInt ITNative))
2644elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2645elaboratingArgErr [] err = err
2646elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
2647 where rewrite (ElaboratingArg _ _ _ _) = Nothing
2648 rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
2649 rewrite (At fc e) = fmap (At fc) (rewrite e)
2650 rewrite err = Just (ElaboratingArg f x during err)
2653withErrorReflection :: Idris a -> Idris a
2654withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2655 where handle :: Err -> Idris Err
2656 handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"
2657 return e -- Don't do meta-reflection of errors
2658 handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
2659 return e
2660 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
2661 handle e@(At fc err) = do logLvl 3 "Reflecting body of At"
2662 err' <- handle err
2663 return (At fc err')
2664 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
2665 err' <- handle err
2666 return (Elaborating what n err')
2667 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
2668 hs <- getFnHandlers f a
2669 err' <- if null hs
2670 then handle err
2671 else applyHandlers err hs
2672 return (ElaboratingArg f a prev err')
2673 -- ProofSearchFail is an internal detail - so don't expose it
2674 handle (ProofSearchFail e) = handle e
2675 -- TODO: argument-specific error handlers go here for ElaboratingArg
2676 handle e = do ist <- getIState
2677 logLvl 2 "Starting error reflection"
2678 let handlers = idris_errorhandlers ist
2679 applyHandlers e handlers
2680 getFnHandlers :: Name -> Name -> Idris [Name]
2681 getFnHandlers f arg = do ist <- getIState
2682 let funHandlers = maybe M.empty id .
2683 lookupCtxtExact f .
2684 idris_function_errorhandlers $ ist
2685 return . maybe [] S.toList . M.lookup arg $ funHandlers
2688 applyHandlers e handlers =
2689 do ist <- getIState
2690 let err = fmap (errReverse ist) e
2691 logLvl 3 $ "Using reflection handlers " ++
2692 concat (intersperse ", " (map show handlers))
2693 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
2695 -- Typecheck error handlers - if this fails, then something else was wrong earlier!
2696 handlers <- case mapM (check (tt_ctxt ist) []) reports of
2697 Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
2698 OK hs -> return hs
2700 -- Normalize error handler terms to produce the new messages
2701 ctxt <- getContext
2702 let results = map (normalise ctxt []) (map fst handlers)
2703 logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
2705 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
2706 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
2707 errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
2708 Left err -> ierror err
2709 Right ok -> return ok
2710 return $ case errorparts of
2711 [] -> e
2712 parts -> ReflectionError errorparts e
2714fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
2715fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
2716 | just == txt "Just" = Just tm
2717fromTTMaybe x = Nothing
2719reflErrName :: String -> Name
2720reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
2722-- | Attempt to reify a report part from TT to the internal
2723-- representation. Not in Idris or ElabD monads because it should be usable
2724-- from either.
2725reifyReportPart :: Term -> Either Err ErrorReportPart
2726reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
2727 Right (TextPart msg)
2728reifyReportPart (App (P (DCon _ _ _) n _) ttn)
2729 | n == reflm "NamePart" =
2730 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of
2731 Error e -> Left . InternalMsg $
2732 "could not reify name term " ++
2733 show ttn ++
2734 " when reflecting an error:" ++ show e
2735 OK (n', _)-> Right $ NamePart n'
2736reifyReportPart (App (P (DCon _ _ _) n _) tm)
2737 | n == reflm "TermPart" =
2738 case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of
2739 Error e -> Left . InternalMsg $
2740 "could not reify reflected term " ++
2741 show tm ++
2742 " when reflecting an error:" ++ show e
2743 OK (tm', _) -> Right $ TermPart tm'
2744reifyReportPart (App (P (DCon _ _ _) n _) tm)
2745 | n == reflm "SubReport" =
2746 case unList tm of
2747 Just xs -> do subParts <- mapM reifyReportPart xs
2748 Right (SubReport subParts)
2749 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
2750reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
2752envTupleType :: Raw
2753envTupleType
2754 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
2755 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
2758solveAll = try (do solve; solveAll) (return ())