@@ -5,15 +5,18 @@ module Idris.ElabTerm where
55import Idris.AbsSyntax
66import Idris.DSL
77import Idris.Delaborate
8+import Idris.Error
89import Idris.ProofSearch
910
1011import Idris.Core.Elaborate hiding (Tactic(..))
1112import Idris.Core.TT
1213import Idris.Core.Evaluate
14+import Idris.Core.Typecheck (check)
1315
1416import Control.Monad
15−import Control.Monad.State
17+import Control.Monad.State.Strict
1618import Data.List
19+import Data.Maybe (mapMaybe)
1720
1821import Debug.Trace
1922
@@ -78,7 +81,10 @@ build ist info pattern opts fn tm
7881buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
7982 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
8083buildTC ist info pattern opts fn tm
81− = do elab ist info pattern opts fn tm
84+ = do -- set name supply to begin after highest index in tm
85+ let ns = allNamesIn tm
86+ initNextNameFrom ns
87+ elab ist info pattern opts fn tm
8288 probs <- get_probs
8389 tm <- get_term
8490 case probs of
@@ -104,7 +110,6 @@ elab ist info pattern opts fn tm
104110 end_unify
105111 when pattern -- convert remaining holes to pattern vars
106112 (do update_term orderPats
107− tm <- get_term
108113 mkPat)
109114 where
110115 tcgen = Dictionary `elem` opts
@@ -168,18 +173,18 @@ elab ist info pattern opts fn tm
168173 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
169174 = do g <- goal; resolveTC 5 g fn ist
170175 elab' ina (PResolveTC fc)
171− | True = do c <- unique_hole (MN 0 "class")
176+ | True = do c <- getNameFrom (sMN 0 "class")
172177 instanceArg c
173178 | otherwise = do g <- goal
174179 try (resolveTC 2 g fn ist)
175− (do c <- unique_hole (MN 0 "class")
180+ (do c <- getNameFrom (sMN 0 "class")
176181 instanceArg c)
177182 elab' ina (PRefl fc t)
178− = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder True,
179− pimp (MN 0 "x") t False])
183+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
184+ pimp (sMN 0 "x") t False])
180185 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)
181− [pimp (MN 0 "a") Placeholder True,
182− pimp (MN 0 "b") Placeholder False,
186+ [pimp (sMN 0 "A") Placeholder True,
187+ pimp (sMN 0 "B") Placeholder False,
183188 pexp l, pexp r])
184189 elab' ina@(_, a, inty) (PPair fc l r)
185190 = do hnf_compute
@@ -188,8 +193,8 @@ elab ist info pattern opts fn tm
188193 TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
189194 [pexp l,pexp r])
190195 _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
191− [pimp (MN 0 "A") Placeholder True,
192− pimp (MN 0 "B") Placeholder True,
196+ [pimp (sMN 0 "A") Placeholder True,
197+ pimp (sMN 0 "B") Placeholder True,
193198 pexp l, pexp r])
194199 elab' ina (PDPair fc l@(PRef _ n) t r)
195200 = case t of
@@ -204,12 +209,12 @@ elab ist info pattern opts fn tm
204209 [pexp t,
205210 pexp (PLam n Placeholder r)])
206211 asValue = elab' ina (PApp fc (PRef fc existsCon)
207− [pimp (MN 0 "a") t False,
208− pimp (MN 0 "P") Placeholder True,
212+ [pimp (sMN 0 "a") t False,
213+ pimp (sMN 0 "P") Placeholder True,
209214 pexp l, pexp r])
210215 elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)
211− [pimp (MN 0 "a") t False,
212− pimp (MN 0 "P") Placeholder True,
216+ [pimp (sMN 0 "a") t False,
217+ pimp (sMN 0 "P") Placeholder True,
213218 pexp l, pexp r])
214219 elab' ina (PAlternative True as)
215220 = do hnf_compute
@@ -256,38 +261,35 @@ elab ist info pattern opts fn tm
256261 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
257262 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
258263 elab' ina@(_, a, inty) (PLam n Placeholder sc)
259− = do -- n' <- unique_hole n
260− -- let sc' = mapPT (repN n n') sc
261− ptm <- get_term
262− g <- goal
264+ = do -- if n is a type constructor name, this makes no sense...
265+ ctxt <- get_context
266+ when (isTConName n ctxt) $
267+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
263268 checkPiGoal n
264269 attack; intro (Just n);
265270 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
266271 elabE (True, a, inty) sc; solve
267− where repN n n' (PRef fc x) | x == n' = PRef fc n'
268− repN _ _ t = t
269272 elab' ina@(_, a, inty) (PLam n ty sc)
270− = do hsin <- get_holes
271− ptmin <- get_term
272− tyn <- unique_hole (MN 0 "lamty")
273+ = do tyn <- getNameFrom (sMN 0 "lamty")
274+ -- if n is a type constructor name, this makes no sense...
275+ ctxt <- get_context
276+ when (isTConName n ctxt) $
277+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
273278 checkPiGoal n
274279 claim tyn RType
275280 explicit tyn
276281 attack
277282 ptm <- get_term
278283 hs <- get_holes
279− -- trace ("BEFORE:\n" ++ show hsin ++ "\n" ++ show ptmin ++
280− -- "\nNOW:\n" ++ show hs ++ "\n" ++ show ptm) $
281284 introTy (Var tyn) (Just n)
282− -- end_unify
283285 focus tyn
284286 elabE (True, a, True) ty
285287 elabE (True, a, inty) sc
286288 solve
287289 elab' ina@(_, a, _) (PPi _ n Placeholder sc)
288− = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve
290+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve
289291 elab' ina@(_, a, _) (PPi _ n ty sc)
290− = do attack; tyn <- unique_hole (MN 0 "ty")
292+ = do attack; tyn <- getNameFrom (sMN 0 "ty")
291293 claim tyn RType
292294 n' <- case n of
293295 MN _ _ -> unique_hole n
@@ -299,9 +301,9 @@ elab ist info pattern opts fn tm
299301 solve
300302 elab' ina@(_, a, inty) (PLet n ty val sc)
301303 = do attack;
302− tyn <- unique_hole (MN 0 "letty")
304+ tyn <- getNameFrom (sMN 0 "letty")
303305 claim tyn RType
304− valn <- unique_hole (MN 0 "letval")
306+ valn <- getNameFrom (sMN 0 "letval")
305307 claim valn (Var tyn)
306308 explicit valn
307309 letbind n (Var tyn) (Var valn)
@@ -322,9 +324,9 @@ elab ist info pattern opts fn tm
322324 elab' ina@(_, a, inty) (PGoal fc r n sc) = do
323325 rty <- goal
324326 attack
325− tyn <- unique_hole (MN 0 "letty")
327+ tyn <- getNameFrom (sMN 0 "letty")
326328 claim tyn RType
327− valn <- unique_hole (MN 0 "letval")
329+ valn <- getNameFrom (sMN 0 "letval")
328330 claim valn (Var tyn)
329331 letbind n (Var tyn) (Var valn)
330332 focus valn
@@ -343,7 +345,7 @@ elab ist info pattern opts fn tm
343345 -- new function name
344346 env <- get_env
345347 argTys <- claimArgTys env args
346− fn <- unique_hole (MN 0 "inf_fn")
348+ fn <- getNameFrom (sMN 0 "inf_fn")
347349 let fty = fnTy argTys rty
348350-- trace (show (ptm, map fst argTys)) $ focus fn
349351 -- build and defer the function application
@@ -357,8 +359,8 @@ elab ist info pattern opts fn tm
357359 ans <- claimArgTys env xs
358360 return ((n, (False, forget nty)) : ans)
359361 claimArgTys env (_ : xs)
360− = do an <- unique_hole (MN 0 "inf_argTy")
361− aval <- unique_hole (MN 0 "inf_arg")
362+ = do an <- getNameFrom (sMN 0 "inf_argTy")
363+ aval <- getNameFrom (sMN 0 "inf_arg")
362364 claim an RType
363365 claim aval (Var an)
364366 ans <- claimArgTys env xs
@@ -378,7 +380,7 @@ elab ist info pattern opts fn tm
378380 mkN n@(NS _ _) = n
379381 mkN n@(SN _) = n
380382 mkN n = case namespace info of
381− Just xs@(_:_) -> NS n xs
383+ Just xs@(_:_) -> sNS n xs
382384 _ -> n
383385
384386 elab' ina (PMatchApp fc fn)
@@ -391,16 +393,12 @@ elab ist info pattern opts fn tm
391393 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
392394 = lift $ tfail (Msg "Typecase is not allowed")
393395 -- if f is local, just do a simple_app
394− elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args')
395− = do let args = {- case lookupCtxt f (inblock info) of
396− Just ps -> (map (pexp . (PRef fc)) ps ++ args')
397− _ -> -} args'
398−-- newtm <- mkSpecialised ist fc f (map getTm args') tm
399− env <- get_env
400− if (f `elem` map fst env && length args' == 1)
396+ elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
397+ = do env <- get_env
398+ if (f `elem` map fst env && length args == 1)
401399 then -- simple app, as below
402400 do simple_app (elabE (ina, g, inty) (PRef fc f))
403− (elabE (True, g, inty) (getTm (head args')))
401+ (elabE (True, g, inty) (getTm (head args)))
404402 (show tm)
405403 solve
406404 else
@@ -413,24 +411,17 @@ elab ist info pattern opts fn tm
413411 -- we can unify with them
414412 case lookupCtxt f (idris_classes ist) of
415413 [] -> return ()
416− _ -> mapM_ setInjective (map getTm args')
414+ _ -> mapM_ setInjective (map getTm args)
417415 ctxt <- get_context
418416 let guarded = isConName f ctxt
419417 ns <- apply (Var f) (map isph args)
420− ptm <- get_term
421− g <- goal
422− -- Sort so that the implicit tactics go last
418+ -- Sort so that the implicit tactics and alternatives go last
423419 let (ns', eargs) = unzip $
424− sortBy (\(_,x) (_,y) ->
425− compare (priority x) (priority y))
426− (zip ns args)
420+ sortBy cmpArg (zip ns args)
427421 elabArgs (ina || not isinf, guarded, inty)
428422 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
429− mkSpecialised ist fc f (map getTm args') tm
430423 solve
431− ptm <- get_term
432424 ivs' <- get_instances
433− ps' <- get_probs
434425 -- Attempt to resolve any type classes which have 'complete' types,
435426 -- i.e. no holes in them
436427 when (not pattern || (ina && not tcgen && not guarded)) $
@@ -446,6 +437,13 @@ elab ist info pattern opts fn tm
446437 (ivs' \\ ivs)
447438 where tcArg (n, PConstraint _ _ Placeholder _) = True
448439 tcArg _ = False
440+
441+ -- normal < tactic < default tactic
442+ cmpArg (_, x) (_, y)
443+ = compare (priority x + alt x) (priority y + alt y)
444+ where alt t = case getTm t of
445+ PAlternative False _ -> 5
446+ _ -> 0
449447
450448 tacTm (PTactics _) = True
451449 tacTm (PProof _) = True
@@ -466,7 +464,7 @@ elab ist info pattern opts fn tm
466464 do attack; defer n'; solve
467465 where mkN n@(NS _ _) = n
468466 mkN n = case namespace info of
469− Just xs@(_:_) -> NS n xs
467+ Just xs@(_:_) -> sNS n xs
470468 _ -> n
471469 elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts
472470 elab' ina (PTactics ts)
@@ -475,11 +473,11 @@ elab ist info pattern opts fn tm
475473 elab' ina (PElabError e) = fail (pshow ist e)
476474 elab' ina (PRewrite fc r sc newg)
477475 = do attack
478− tyn <- unique_hole (MN 0 "rty")
476+ tyn <- getNameFrom (sMN 0 "rty")
479477 claim tyn RType
480− valn <- unique_hole (MN 0 "rval")
478+ valn <- getNameFrom (sMN 0 "rval")
481479 claim valn (Var tyn)
482− letn <- unique_hole (MN 0 "rewrite_rule")
480+ letn <- getNameFrom (sMN 0 "rewrite_rule")
483481 letbind letn (Var tyn) (Var valn)
484482 focus valn
485483 elab' ina r
@@ -494,11 +492,11 @@ elab ist info pattern opts fn tm
494492 solve
495493 where doEquiv t sc =
496494 do attack
497− tyn <- unique_hole (MN 0 "ety")
495+ tyn <- getNameFrom (sMN 0 "ety")
498496 claim tyn RType
499− valn <- unique_hole (MN 0 "eqval")
497+ valn <- getNameFrom (sMN 0 "eqval")
500498 claim valn (Var tyn)
501− letn <- unique_hole (MN 0 "equiv_val")
499+ letn <- getNameFrom (sMN 0 "equiv_val")
502500 letbind letn (Var tyn) (Var valn)
503501 focus tyn
504502 elab' ina t
@@ -508,10 +506,10 @@ elab ist info pattern opts fn tm
508506 solve
509507 elab' ina@(_, a, inty) c@(PCase fc scr opts)
510508 = do attack
511− tyn <- unique_hole (MN 0 "scty")
509+ tyn <- getNameFrom (sMN 0 "scty")
512510 claim tyn RType
513− valn <- unique_hole (MN 0 "scval")
514− scvn <- unique_hole (MN 0 "scvar")
511+ valn <- getNameFrom (sMN 0 "scval")
512+ scvn <- getNameFrom (sMN 0 "scvar")
515513 claim valn (Var tyn)
516514 letbind scvn (Var tyn) (Var valn)
517515 focus valn
@@ -537,7 +535,7 @@ elab ist info pattern opts fn tm
537535-- mkCaseName (MN i x) = MN i (x ++ "_case")
538536 mkN n@(NS _ _) = n
539537 mkN n = case namespace info of
540− Just xs@(_:_) -> NS n xs
538+ Just xs@(_:_) -> sNS n xs
541539 _ -> n
542540 elab' ina (PUnifyLog t) = do unifyLog True
543541 elab' ina t
@@ -617,8 +615,8 @@ elab ist info pattern opts fn tm
617615 = elabArgs ina failed fc r ns args
618616 elabArgs ina failed fc r (n:ns) ((lazy, t) : args)
619617 | lazy && not pattern
620− = do elabArg n (PApp bi (PRef bi (UN "lazy"))
621− [pimp (UN "a") Placeholder True,
618+ = do elabArg n (PApp bi (PRef bi (sUN "lazy"))
619+ [pimp (sUN "a") Placeholder True,
622620 pexp t]);
623621 | otherwise = elabArg n t
624622 where elabArg n t
@@ -698,9 +696,9 @@ findInstances ist t
698696 | otherwise = []
699697
700698trivial' ist
701− = trivial (elab ist toplevel False [] (MN 0 "tac")) ist
699+ = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist
702700proofSearch' ist top n hints
703− = proofSearch (elab ist toplevel False [] (MN 0 "tac")) top n hints ist
701+ = proofSearch (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist
704702
705703
706704resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
@@ -710,9 +708,10 @@ resolveTC depth topg fn ist
710708 = do hnf_compute
711709 g <- goal
712710 ptm <- get_term
711+ ulog <- getUnifyLog
713712 hs <- get_holes
714− if True -- all (\n -> not (n `elem` hs)) (freeNames g)
715− then try' (trivial' ist)
713+ traceWhen ulog ("Resolving class " ++ show g) $
714+ try' (trivial' ist)
716715 (do t <- goal
717716 let (tc, ttypes) = unApply t
718717 scopeOnly <- needsDefault t tc ttypes
@@ -720,28 +719,23 @@ resolveTC depth topg fn ist
720719 let insts = if scopeOnly then filter chaser insts_in
721720 else insts_in
722721 tm <- get_term
723−-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
724−-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
725−-- if scopeOnly then fail "Can't resolve" else
726722 let depth' = if scopeOnly then 2 else depth
727723 blunderbuss t depth' insts) True
728− else do try' (trivial' ist)
729− (do g <- goal
730− fail $ "Can't resolve " ++ show g) True
731−-- tm <- get_term
732−-- fail $ "Can't resolve yet in " ++ show tm
733724 where
734725 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
735726 | otherwise = (fail "Can't resolve", show n)
736727
737728 -- HACK! Rather than giving a special name, better to have some kind
738729 -- of flag in ClassInfo structure
739− chaser (UN ('@':'@':_)) = True -- old way
730+ chaser (UN nm)
731+ | ('@':'@':_) <- str nm = True -- old way
740732 chaser (SN (ParentN _ _)) = True
741733 chaser (NS n _) = chaser n
742734 chaser _ = False
743735
744− needsDefault t num@(P _ (NS (UN "Num") ["Classes","Prelude"]) _) [P Bound a _]
736+ numclass = sNS (sUN "Num") ["Classes","Prelude"]
737+
738+ needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass
745739 = do focus a
746740 fill (RConstant (AType (ATInt ITBig))) -- default Integer
747741 solve
@@ -774,8 +768,8 @@ resolveTC depth topg fn ist
774768 [args] -> map isImp (snd args) -- won't be overloaded!
775769 ps <- get_probs
776770 tm <- get_term
777− args <- try' (match_apply (Var n) imps)
778− (apply (Var n) imps) True
771+ args <- try' (apply (Var n) imps)
772+ (match_apply (Var n) imps) True
779773 ps' <- get_probs
780774 when (length ps < length ps') $ fail "Can't apply type class"
781775-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
@@ -787,7 +781,9 @@ resolveTC depth topg fn ist
787781 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
788782 -- if there's any arguments left, we've failed to resolve
789783 hs <- get_holes
790− solve
784+ ulog <- getUnifyLog
785+ solve
786+ traceWhen ulog ("Got " ++ show n) $ return ()
791787 where isImp (PImp p _ _ _ _ _) = (True, p)
792788 isImp arg = (False, priority arg)
793789
@@ -814,7 +810,9 @@ collectDeferred top t = return t
814810runTac :: Bool -> IState -> PTactic -> ElabD ()
815811runTac autoSolve ist tac
816812 = do env <- get_env
817− no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)
813+ g <- goal
814+ no_errors (runT (fmap (addImplBound ist (map fst env)) tac))
815+ (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
818816 where
819817 runT (Intro []) = do g <- goal
820818 attack; intro (bname g)
@@ -829,7 +827,7 @@ runTac autoSolve ist tac
829827 where
830828 bname (Bind n _ _) = Just n
831829 bname _ = Nothing
832− runT (Exact tm) = do elab ist toplevel False [] (MN 0 "tac") tm
830+ runT (Exact tm) = do elab ist toplevel False [] (sMN 0 "tac") tm
833831 when autoSolve solveAll
834832 runT (MatchRefine fn)
835833 = do fnimps <-
@@ -869,27 +867,27 @@ runTac autoSolve ist tac
869867 when autoSolve solveAll
870868 runT (Equiv tm) -- let bind tm, then
871869 = do attack
872− tyn <- unique_hole (MN 0 "ety")
870+ tyn <- getNameFrom (sMN 0 "ety")
873871 claim tyn RType
874− valn <- unique_hole (MN 0 "eqval")
872+ valn <- getNameFrom (sMN 0 "eqval")
875873 claim valn (Var tyn)
876− letn <- unique_hole (MN 0 "equiv_val")
874+ letn <- getNameFrom (sMN 0 "equiv_val")
877875 letbind letn (Var tyn) (Var valn)
878876 focus tyn
879− elab ist toplevel False [] (MN 0 "tac") tm
877+ elab ist toplevel False [] (sMN 0 "tac") tm
880878 focus valn
881879 when autoSolve solveAll
882880 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
883881 = do attack; -- (h:_) <- get_holes
884− tyn <- unique_hole (MN 0 "rty")
882+ tyn <- getNameFrom (sMN 0 "rty")
885883 -- start_unify h
886884 claim tyn RType
887− valn <- unique_hole (MN 0 "rval")
885+ valn <- getNameFrom (sMN 0 "rval")
888886 claim valn (Var tyn)
889− letn <- unique_hole (MN 0 "rewrite_rule")
887+ letn <- getNameFrom (sMN 0 "rewrite_rule")
890888 letbind letn (Var tyn) (Var valn)
891889 focus valn
892− elab ist toplevel False [] (MN 0 "tac") tm
890+ elab ist toplevel False [] (sMN 0 "tac") tm
893891 rewrite (Var letn)
894892 when autoSolve solveAll
895893 runT (Induction nm)
@@ -897,27 +895,27 @@ runTac autoSolve ist tac
897895 when autoSolve solveAll
898896 runT (LetTac n tm)
899897 = do attack
900− tyn <- unique_hole (MN 0 "letty")
898+ tyn <- getNameFrom (sMN 0 "letty")
901899 claim tyn RType
902− valn <- unique_hole (MN 0 "letval")
900+ valn <- getNameFrom (sMN 0 "letval")
903901 claim valn (Var tyn)
904902 letn <- unique_hole n
905903 letbind letn (Var tyn) (Var valn)
906904 focus valn
907− elab ist toplevel False [] (MN 0 "tac") tm
905+ elab ist toplevel False [] (sMN 0 "tac") tm
908906 when autoSolve solveAll
909907 runT (LetTacTy n ty tm)
910908 = do attack
911− tyn <- unique_hole (MN 0 "letty")
909+ tyn <- getNameFrom (sMN 0 "letty")
912910 claim tyn RType
913− valn <- unique_hole (MN 0 "letval")
911+ valn <- getNameFrom (sMN 0 "letval")
914912 claim valn (Var tyn)
915913 letn <- unique_hole n
916914 letbind letn (Var tyn) (Var valn)
917915 focus tyn
918− elab ist toplevel False [] (MN 0 "tac") ty
916+ elab ist toplevel False [] (sMN 0 "tac") ty
919917 focus valn
920− elab ist toplevel False [] (MN 0 "tac") tm
918+ elab ist toplevel False [] (sMN 0 "tac") tm
921919 when autoSolve solveAll
922920 runT Compute = compute
923921 runT Trivial = do trivial' ist; when autoSolve solveAll
@@ -930,16 +928,16 @@ runTac autoSolve ist tac
930928 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
931929 tgoal <- goal -- store the goal
932930 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
933− script <- unique_hole (MN 0 "script")
931+ script <- getNameFrom (sMN 0 "script")
934932 claim script scriptTy
935− scriptvar <- unique_hole (MN 0 "scriptvar" )
933+ scriptvar <- getNameFrom (sMN 0 "scriptvar" )
936934 letbind scriptvar scriptTy (Var script)
937935 focus script
938− elab ist toplevel False [] (MN 0 "tac") tm
936+ elab ist toplevel False [] (sMN 0 "tac") tm
939937 (script', _) <- get_type_val (Var scriptvar)
940938 -- now that we have the script apply
941939 -- it to the reflected goal and context
942− restac <- unique_hole (MN 0 "restac")
940+ restac <- getNameFrom (sMN 0 "restac")
943941 claim restac tacticTy
944942 focus restac
945943 fill (raw_apply (forget script')
@@ -953,27 +951,27 @@ runTac autoSolve ist tac
953951 let tactic = normalise ctxt env restac'
954952 runReflected tactic
955953 where tacticTy = Var (reflm "Tactic")
956− listTy = Var (NS (UN "List") ["List", "Prelude"])
957− scriptTy = (RBind (UN "__pi_arg")
954+ listTy = Var (sNS (sUN "List") ["List", "Prelude"])
955+ scriptTy = (RBind (sUN "__pi_arg")
958956 (Pi (RApp listTy envTupleType))
959− (RBind (UN "__pi_arg1")
957+ (RBind (sUN "__pi_arg1")
960958 (Pi (Var $ reflm "TT")) tacticTy))
961959 runT (ByReflection tm) -- run the reflection function 'tm' on the
962960 -- goal, then apply the resulting reflected Tactic
963961 = do tgoal <- goal
964962 attack
965− script <- unique_hole (MN 0 "script")
963+ script <- getNameFrom (sMN 0 "script")
966964 claim script scriptTy
967− scriptvar <- unique_hole (MN 0 "scriptvar" )
965+ scriptvar <- getNameFrom (sMN 0 "scriptvar" )
968966 letbind scriptvar scriptTy (Var script)
969967 focus script
970968 ptm <- get_term
971− elab ist toplevel False [] (MN 0 "tac")
969+ elab ist toplevel False [] (sMN 0 "tac")
972970 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
973971 (script', _) <- get_type_val (Var scriptvar)
974972 -- now that we have the script apply
975973 -- it to the reflected goal
976− restac <- unique_hole (MN 0 "restac")
974+ restac <- getNameFrom (sMN 0 "restac")
977975 claim restac tacticTy
978976 focus restac
979977 fill (forget script')
@@ -989,28 +987,28 @@ runTac autoSolve ist tac
989987 scriptTy = tacticTy
990988
991989 runT (Reflect v) = do attack -- let x = reflect v in ...
992− tyn <- unique_hole (MN 0 "letty")
990+ tyn <- getNameFrom (sMN 0 "letty")
993991 claim tyn RType
994− valn <- unique_hole (MN 0 "letval")
992+ valn <- getNameFrom (sMN 0 "letval")
995993 claim valn (Var tyn)
996− letn <- unique_hole (MN 0 "letvar")
994+ letn <- getNameFrom (sMN 0 "letvar")
997995 letbind letn (Var tyn) (Var valn)
998996 focus valn
999− elab ist toplevel False [] (MN 0 "tac") v
997+ elab ist toplevel False [] (sMN 0 "tac") v
1000998 (value, _) <- get_type_val (Var letn)
1001999 ctxt <- get_context
10021000 env <- get_env
10031001 let value' = hnf ctxt env value
10041002 runTac autoSolve ist (Exact $ PQuote (reflect value'))
10051003 runT (Fill v) = do attack -- let x = fill x in ...
1006− tyn <- unique_hole (MN 0 "letty")
1004+ tyn <- getNameFrom (sMN 0 "letty")
10071005 claim tyn RType
1008− valn <- unique_hole (MN 0 "letval")
1006+ valn <- getNameFrom (sMN 0 "letval")
10091007 claim valn (Var tyn)
1010− letn <- unique_hole (MN 0 "letvar")
1008+ letn <- getNameFrom (sMN 0 "letvar")
10111009 letbind letn (Var tyn) (Var valn)
10121010 focus valn
1013− elab ist toplevel False [] (MN 0 "tac") v
1011+ elab ist toplevel False [] (sMN 0 "tac") v
10141012 (value, _) <- get_type_val (Var letn)
10151013 ctxt <- get_context
10161014 env <- get_env
@@ -1020,20 +1018,20 @@ runTac autoSolve ist tac
10201018 runT (GoalType n tac) = do g <- goal
10211019 case unApply g of
10221020 (P _ n' _, _) ->
1023− if nsroot n' == UN n
1021+ if nsroot n' == sUN n
10241022 then runT tac
10251023 else fail "Wrong goal type"
10261024 _ -> fail "Wrong goal type"
10271025 runT ProofState = do g <- goal
1028− trace (show g) $ return ()
1026+ return ()
10291027 runT x = fail $ "Not implemented " ++ show x
10301028
10311029 runReflected t = do t' <- reify ist t
10321030 runTac autoSolve ist t'
10331031
1034−-- | Prefix a name with the "Reflection.Language" namespace
1032+-- | Prefix a name with the "Language.Reflection" namespace
10351033reflm :: String -> Name
1036−reflm n = NS (UN n) ["Reflection", "Language"]
1034+reflm n = sNS (sUN n) ["Reflection", "Language"]
10371035
10381036
10391037-- | Reify tactics from their reflected representation
@@ -1055,7 +1053,7 @@ reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist
10551053reifyApp ist t [Constant (Str n), x]
10561054 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
10571055reifyApp _ t [Constant (Str n)]
1058− | t == reflm "Intro" = return $ Intro [UN n]
1056+ | t == reflm "Intro" = return $ Intro [sUN n]
10591057reifyApp ist t [t']
10601058 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
10611059reifyApp ist t [t']
@@ -1146,13 +1144,13 @@ reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
11461144
11471145reifyTTNameApp :: Name -> [Term] -> ElabD Name
11481146reifyTTNameApp t [Constant (Str n)]
1149− | t == reflm "UN" = return $ UN n
1147+ | t == reflm "UN" = return $ sUN n
11501148reifyTTNameApp t [n, ns]
11511149 | t == reflm "NS" = do n' <- reifyTTName n
11521150 ns' <- reifyTTNamespace ns
1153− return $ NS n' ns'
1151+ return $ sNS n' ns'
11541152reifyTTNameApp t [Constant (I i), Constant (Str n)]
1155− | t == reflm "MN" = return $ MN i n
1153+ | t == reflm "MN" = return $ sMN i n
11561154reifyTTNameApp t []
11571155 | t == reflm "NErased" = return NErased
11581156reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
@@ -1161,9 +1159,9 @@ reifyTTNamespace :: Term -> ElabD [String]
11611159reifyTTNamespace t@(App _ _)
11621160 = case unApply t of
11631161 (P _ f _, [Constant StrType])
1164− | f == NS (UN "Nil") ["List", "Prelude"] -> return []
1162+ | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
11651163 (P _ f _, [Constant StrType, Constant (Str n), ns])
1166− | f == NS (UN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
1164+ | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
11671165 _ -> fail ("Unknown reflection namespace arg: " ++ show t)
11681166reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
11691167
@@ -1285,19 +1283,19 @@ reflectNameType (TCon x y)
12851283 = reflCall "TCon" [RConstant (I x), RConstant (I y)]
12861284
12871285reflectName :: Name -> Raw
1288−reflectName (UN str)
1289− = reflCall "UN" [RConstant (Str str)]
1286+reflectName (UN s)
1287+ = reflCall "UN" [RConstant (Str (str s))]
12901288reflectName (NS n ns)
12911289 = reflCall "NS" [ reflectName n
12921290 , foldr (\ n s ->
1293− raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )
1291+ raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
12941292 [ RConstant StrType, RConstant (Str n), s ])
1295− ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )
1293+ ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
12961294 [ RConstant StrType ])
1297− ns
1295+ (map str ns)
12981296 ]
12991297reflectName (MN i n)
1300− = reflCall "MN" [RConstant (I i), RConstant (Str n)]
1298+ = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
13011299reflectName (NErased) = Var (reflm "NErased")
13021300reflectName n = Var (reflm "NErased") -- special name, not yet implemented
13031301
@@ -1354,7 +1352,7 @@ reflectEnv = foldr consToEnvList emptyEnvList
13541352 where
13551353 consToEnvList :: (Name, Binder Term) -> Raw -> Raw
13561354 consToEnvList (n, b) l
1357− = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))
1355+ = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
13581356 [ envTupleType
13591357 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
13601358 , (RApp (Var $ reflm "Binder")
@@ -1366,14 +1364,182 @@ reflectEnv = foldr consToEnvList emptyEnvList
13661364 ]
13671365
13681366 emptyEnvList :: Raw
1369− emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))
1367+ emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
13701368 [envTupleType]
13711369
13721370-- | Reflect an error into the internal datatype of Idris -- TODO
1371+rawBool :: Bool -> Raw
1372+rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
1373+rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
1374+
1375+rawNil :: Raw -> Raw
1376+rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
1377+
1378+rawCons :: Raw -> Raw -> Raw -> Raw
1379+rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
1380+
1381+rawList :: Raw -> [Raw] -> Raw
1382+rawList ty = foldr (rawCons ty) (rawNil ty)
1383+
1384+rawPairTy :: Raw -> Raw -> Raw
1385+rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
1386+
1387+rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
1388+rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
1389+
1390+reflectCtxt :: [(Name, Type)] -> Raw
1391+reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
1392+ (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
1393+ (reflectName n, reflect t)))
1394+ ctxt)
1395+
13731396reflectErr :: Err -> Raw
1374−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1375−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1376−reflectErr x = trace ("Couldn't reflect error " ++ show x) raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str $ show x)]
1397+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
1398+reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
1399+reflectErr (CantUnify b t1 t2 e ctxt i) =
1400+ raw_apply (Var $ reflErrName "CantUnify")
1401+ [ rawBool b
1402+ , reflect t1
1403+ , reflect t2
1404+ , reflectErr e
1405+ , reflectCtxt ctxt
1406+ , RConstant (I i)]
1407+reflectErr (InfiniteUnify n tm ctxt) =
1408+ raw_apply (Var $ reflErrName "InfiniteUnify")
1409+ [ reflectName n
1410+ , reflect tm
1411+ , reflectCtxt ctxt
1412+ ]
1413+reflectErr (CantConvert t t' ctxt) =
1414+ raw_apply (Var $ reflErrName "CantConvert")
1415+ [ reflect t
1416+ , reflect t'
1417+ , reflectCtxt ctxt
1418+ ]
1419+reflectErr (CantSolveGoal t ctxt) =
1420+ raw_apply (Var $ reflErrName "CantSolveGoal")
1421+ [ reflect t
1422+ , reflectCtxt ctxt
1423+ ]
1424+reflectErr (UnifyScope n n' t ctxt) =
1425+ raw_apply (Var $ reflErrName "UnifyScope")
1426+ [ reflectName n
1427+ , reflectName n'
1428+ , reflect t
1429+ , reflectCtxt ctxt
1430+ ]
1431+reflectErr (CantInferType str) =
1432+ raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
1433+reflectErr (NonFunctionType t t') =
1434+ raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
1435+reflectErr (NotEquality t t') =
1436+ raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
1437+reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
1438+reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
1439+reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
1440+reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
1441+reflectErr (NotInjective t1 t2 t3) =
1442+ raw_apply (Var $ reflErrName "NotInjective")
1443+ [ reflect t1
1444+ , reflect t2
1445+ , reflect t3
1446+ ]
1447+reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
1448+reflectErr (CantResolveAlts ss) =
1449+ raw_apply (Var $ reflErrName "CantResolve")
1450+ [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]
1451+reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
1452+reflectErr UniverseError = Var $ reflErrName "UniverseError"
1453+reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
1454+reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
1455+reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
1456+reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
1457+reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
1458+reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
1459+reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]
1460+ where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")
1461+ [ RConstant (Str source)
1462+ , RConstant (I line)
1463+ , RConstant (I col)
1464+ ]
1465+reflectErr (Elaborating str n e) =
1466+ raw_apply (Var $ reflErrName "Elaborating")
1467+ [ RConstant (Str str)
1468+ , reflectName n
1469+ , reflectErr e
1470+ ]
1471+reflectErr (ProviderError str) =
1472+ raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
1473+reflectErr (LoadingFailed str err) =
1474+ raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
1475+reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
1476+
1477+withErrorReflection :: Idris a -> Idris a
1478+withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1479+ where handle :: Err -> Idris Err
1480+ handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"
1481+ return e -- Don't do meta-reflection of errors
1482+ handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
1483+ return e
1484+ handle e = do ist <- getIState
1485+ logLvl 2 "Starting error reflection"
1486+ let handlers = idris_errorhandlers ist
1487+ logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
1488+ let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers
1489+
1490+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1491+ handlers <- case mapM (check (tt_ctxt ist) []) reports of
1492+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1493+ OK hs -> return hs
1494+
1495+ -- Normalize error handler terms to produce the new messages
1496+ ctxt <- getContext
1497+ let results = map (normalise ctxt []) (map fst handlers)
1498+ logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1499+
1500+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1501+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1502+ errorparts <- mapM (mapM reifyReportPart) errorpartsTT
1503+
1504+ return $ case errorparts of
1505+ [] -> e
1506+ parts -> ReflectionError errorparts e
1507+
1508+ fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1509+ fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)
1510+ | just == txt "Just" = Just tm
1511+ fromTTMaybe x = Nothing
1512+
1513+reflErrName :: String -> Name
1514+reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
1515+
1516+reifyReportPart :: Term -> Idris ErrorReportPart
1517+reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =
1518+ return (TextPart msg)
1519+reifyReportPart (App (P (DCon _ _) n _) ttn)
1520+ | n == reflErrName "NamePart" =
1521+ case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of
1522+ Error e -> ierror . InternalMsg $
1523+ "could not reify name term " ++
1524+ show ttn ++
1525+ " when reflecting an error"
1526+ OK (n', _)-> return $ NamePart n'
1527+reifyReportPart (App (P (DCon _ _) n _) tm)
1528+ | n == reflErrName "TermPart" =
1529+ do ist <- getIState
1530+ case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of
1531+ Error e -> ierror . InternalMsg $
1532+ "could not reify reflected term " ++
1533+ show tm ++
1534+ " when reflecting an error"
1535+ OK (tm', _) -> return $ TermPart tm'
1536+reifyReportPart (App (P (DCon _ _) n _) tm)
1537+ | n == reflErrName "SubReport" =
1538+ case unList tm of
1539+ Just xs -> do subParts <- mapM reifyReportPart xs
1540+ return (SubReport subParts)
1541+ Nothing -> ierror . InternalMsg $ "could not reify subreport " ++ show tm
1542+reifyReportPart x = ierror . InternalMsg $ "could not reify " ++ show x
13771543
13781544envTupleType :: Raw
13791545envTupleType
@@ -1383,44 +1549,3 @@ envTupleType
13831549
13841550solveAll = try (do solve; solveAll) (return ())
13851551
1386−-- If the function application is specialisable, make a new
1387−-- top level function by normalising the application
1388−-- and elaborating the new expression.
1389−
1390−mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm
1391−mkSpecialised i fc n args def
1392− = do let tm' = def
1393− case lookupCtxt n (idris_statics i) of
1394− [as] -> if (not (or as)) then return tm' else
1395− mkSpecDecl i n (zip args as) tm'
1396− _ -> return tm'
1397−
1398−mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm
1399−mkSpecDecl i n pargs tm'
1400− = do t <- goal
1401− g <- get_guess
1402− let (f, args) = unApply g
1403− let sargs = zip args (map snd pargs)
1404− let staticArgs = map fst (filter (\ (_,x) -> x) sargs)
1405− let ns = group (sort (concatMap staticFnNames staticArgs))
1406− let ntimes = map (\xs -> (head xs, length xs - 1)) ns
1407− if (not (null ns)) then
1408− do env <- get_env
1409− let g' = g -- specialise ctxt env ntimes g
1410− return tm'
1411−-- trace (show t ++ "\n" ++
1412−-- show ntimes ++ "\n" ++
1413−-- show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO
1414− else return tm'
1415− where
1416− ctxt = tt_ctxt i
1417− cg = idris_callgraph i
1418−
1419− staticFnNames tm | (P _ f _, as) <- unApply tm
1420− = if not (isFnName f ctxt) then []
1421− else case lookupCtxt f cg of
1422− [ns] -> f : f : [] --(ns \\ [f])
1423− [] -> [f,f]
1424− _ -> []
1425− staticFnNames _ = []
1426−