@@ -18,7 +18,7 @@ import Idris.Core.Typecheck (check, recheck)
1818import Idris.ErrReverse (errReverse)
1919import Idris.ElabQuasiquote (extractUnquotes)
2020import Idris.Elab.Utils
21−import qualified Util.Pretty as U
21+import qualified Util.Pretty as U
2222
2323import Control.Applicative ((<$>))
2424import Control.Monad
@@ -76,9 +76,9 @@ build ist info emode opts fn tm
7676 u <- getUnifyLog
7777 hs <- get_holes
7878
79− when (not pattern) $
79+ when (not pattern) $
8080 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
81− "Remaining problems:\n" ++ qshow probs) $
81+ "Remaining problems:\n" ++ qshow probs) $
8282 do unify_all; matchProblems True; unifyProblems
8383
8484 probs <- get_probs
@@ -99,7 +99,7 @@ build ist info emode opts fn tm
9999 else return (tm, ds, is)
100100 where pattern = emode == ELHS
101101 tydecl = emode == ETyDecl
102−
102+
103103 mkPat = do hs <- get_holes
104104 tm <- get_term
105105 case hs of
@@ -197,14 +197,14 @@ elab ist info emode opts fn tm
197197 -- ++ "\nholes " ++ show hs
198198 -- ++ "\nproblems " ++ show ps
199199 -- ++ "\n-----------\n") $
200− --trace ("ELAB " ++ show t') $
200+ --trace ("ELAB " ++ show t') $
201201 let fc = fileFC "Force"
202202 env <- get_env
203203 handleError (forceErr env)
204204 (elab' ina t')
205205 (elab' ina (PApp fc (PRef fc (sUN "Force"))
206206 [pimp (sUN "t") Placeholder True,
207− pimp (sUN "a") Placeholder True,
207+ pimp (sUN "a") Placeholder True,
208208 pexp ct])) True
209209
210210 forceErr env (CantUnify _ t t' _ _ _)
@@ -240,9 +240,9 @@ elab ist info emode opts fn tm
240240 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
241241 elab' ina PType = do apply RType []; solve
242242 elab' ina (PUniverse u) = do apply (RUType u) []; solve
243−-- elab' (_,_,inty) (PConstant c)
243+-- elab' (_,_,inty) (PConstant c)
244244-- | constType c && pattern && not reflection && not inty
245−-- = lift $ tfail (Msg "Typecase is not allowed")
245+-- = lift $ tfail (Msg "Typecase is not allowed")
246246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
247247 elab' ina (PQuote r) = do fill r; solve
248248 elab' ina (PTrue fc _) =
@@ -338,7 +338,7 @@ elab ist info emode opts fn tm
338338-- elab' (_, _, inty) (PRef fc f)
339339-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
340340-- = lift $ tfail (Msg "Typecase is not allowed")
341− elab' (ina, guarded, inty, qq) (PRef fc n)
341+ elab' (ina, guarded, inty, qq) (PRef fc n)
342342 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
343343 = do ctxt <- get_context
344344 let defined = case lookupTy n ctxt of
@@ -363,7 +363,7 @@ elab ist info emode opts fn tm
363363 = do -- if n is a type constructor name, this makes no sense...
364364 ctxt <- get_context
365365 when (isTConName n ctxt) $
366− lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
366+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
367367 checkPiGoal n
368368 attack; intro (Just n);
369369 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
@@ -373,7 +373,7 @@ elab ist info emode opts fn tm
373373 -- if n is a type constructor name, this makes no sense...
374374 ctxt <- get_context
375375 when (isTConName n ctxt) $
376− lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
376+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
377377 checkPiGoal n
378378 claim tyn RType
379379 explicit tyn
@@ -539,7 +539,7 @@ elab ist info emode opts fn tm
539539 sortBy cmpArg (zip ns args)
540540 ulog <- getUnifyLog
541541 elabArgs ist (ina || not isinf, guarded, inty, qq)
542− [] fc False f ns'
542+ [] fc False f ns'
543543 (f == sUN "Force")
544544 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
545545 solve
@@ -558,7 +558,7 @@ elab ist info emode opts fn tm
558558 else movelast n)
559559 (ivs' \\ ivs)
560560 where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
561− -- reason for lambdas after alternatives is that having
561+ -- reason for lambdas after alternatives is that having
562562 -- the alternative resolved can help with typechecking the lambda
563563 -- or the rewrite. Rewrites/tactics need as much information
564564 -- as possible about the type.
@@ -568,7 +568,7 @@ elab ist info emode opts fn tm
568568 | constraint x && not (constraint y) = LT
569569 | constraint y && not (constraint x) = GT
570570 | otherwise
571− = compare (conDepth 0 (getTm x) + priority x + alt x)
571+ = compare (conDepth 0 (getTm x) + priority x + alt x)
572572 (conDepth 0 (getTm y) + priority y + alt y)
573573 where alt t = case getTm t of
574574 PAlternative False _ -> 5
@@ -581,14 +581,14 @@ elab ist info emode opts fn tm
581581
582582 constraint (PConstraint _ _ _ _) = True
583583 constraint _ = False
584−
584+
585585 -- Score a point for every level where there is a non-constructor
586586 -- function (so higher score --> done later)
587587 -- Only relevant when on lhs
588588 conDepth d t | not pattern = 0
589589 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
590590 | otherwise = max (100 - d) 1
591− conDepth d (PApp _ f as)
591+ conDepth d (PApp _ f as)
592592 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
593593 conDepth d (PPatvar _ _) = 0
594594 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
@@ -602,7 +602,7 @@ elab ist info emode opts fn tm
602602 Nothing -> return ()
603603 Just b ->
604604 case unApply (binderTy b) of
605− (P _ c _, args) ->
605+ (P _ c _, args) ->
606606 case lookupCtxt c (idris_classes ist) of
607607 [] -> return ()
608608 _ -> -- type class, set as injective
@@ -615,7 +615,7 @@ elab ist info emode opts fn tm
615615 probs <- get_probs
616616 traceWhen ulog (qshow probs) $ return ()
617617 _ -> return ()
618−
618+
619619 setinjArg (P _ n _) = setinj n
620620 setinjArg _ = return ()
621621
@@ -634,7 +634,7 @@ elab ist info emode opts fn tm
634634 solve
635635 elab' ina Placeholder = do (h : hs) <- get_holes
636636 movelast h
637− elab' ina (PMetavar n) =
637+ elab' ina (PMetavar n) =
638638 do ptm <- get_term
639639 -- When building the metavar application, leave out the unique
640640 -- names which have been used elsewhere in the term, since we
@@ -699,21 +699,6 @@ elab ist info emode opts fn tm
699699 args <- get_env
700700 envU <- mapM (getKind args) args
701701 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
702−-- ++ allNamesIn scr
703−
704− -- in the definition we build for the case, only pass through
705− -- names which are directly used, type class constraints, and
706− -- variables any of these depend on
707− -- FIXME: This probably doesn't help us, but leaving it in
708− -- temporarily (but commented out). If this comment is still
709− -- here in master, please delete the code!
710−-- let directUse = filter (\n -> usedIn namesUsedInRHS n
711−-- || tcName (binderTy (snd n))) args
712−-- let args' = args -- chaseDeps args (map fst directUse) directUse
713−-- let argsDropped = map fst $
714−-- filter (\(n, _) -> case lookup n args' of
715−-- Nothing -> True
716−-- _ -> False) args
717702
718703 -- Drop the unique arguments used in the scrutinee (since it's
719704 -- not valid to use them again anyway)
@@ -724,7 +709,7 @@ elab ist info emode opts fn tm
724709 let cname' = mkN cname
725710-- elab' ina (PMetavar cname')
726711 attack; defer argsDropped cname'; solve
727−
712+
728713 -- if the scrutinee is one of the 'args' in env, we should
729714 -- inspect it directly, rather than adding it as a new argument
730715 let newdef = PClauses fc [] cname'
@@ -748,10 +733,10 @@ elab ist info emode opts fn tm
748733 Just u -> u
749734 _ -> False
750735
751− getKind env (n, _)
736+ getKind env (n, _)
752737 = case lookup n env of
753738 Nothing -> return (n, False) -- can't happen, actually...
754− Just b ->
739+ Just b ->
755740 do ty <- get_type (forget (binderTy b))
756741 case ty of
757742 UType UniqueType -> return (n, True)
@@ -764,8 +749,8 @@ elab ist info emode opts fn tm
764749 _ -> False
765750 tcName _ = False
766751
767− usedIn ns (n, b)
768− = n `elem` ns
752+ usedIn ns (n, b)
753+ = n `elem` ns
769754 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
770755
771756 -- FIXME: This probably doesn't help us here, but leaving
@@ -872,7 +857,7 @@ elab ist info emode opts fn tm
872857 isScr (PRef _ n) (n', b) = (n', (n == n', b))
873858 isScr _ (n', b) = (n', (False, b))
874859
875− caseBlock :: FC -> Name ->
860+ caseBlock :: FC -> Name ->
876861 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
877862 caseBlock fc n env opts
878863 = let args' = findScr env
@@ -882,12 +867,12 @@ elab ist info emode opts fn tm
882867 where -- Find the variable we want as the scrutinee and mark it as
883868 -- 'True'. If the scrutinee is in the environment, match on that
884869 -- otherwise match on the new argument we're adding.
885− findScr ((n, (True, t)) : xs)
870+ findScr ((n, (True, t)) : xs)
886871 = (n, (True, t)) : scrName n xs
887− findScr [(n, (_, t))] = [(n, (True, t))]
872+ findScr [(n, (_, t))] = [(n, (True, t))]
888873 findScr (x : xs) = x : findScr xs
889874 -- [] can't happen since scrutinee is in the environment!
890−
875+
891876 -- To make sure top level pattern name remains in scope, put
892877 -- it at the end of the environment
893878 scrName n [] = []
@@ -931,7 +916,7 @@ elab ist info emode opts fn tm
931916 _ -> return t
932917 where
933918 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)
934− mkDelay env t
919+ mkDelay env t
935920 = let fc = fileFC "Delay" in
936921 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))
937922 [pexp t])
@@ -998,10 +983,10 @@ elab ist info emode opts fn tm
998983 failed' <- -- trace (show (n, t, hs, tm)) $
999984 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
1000985 case holeName `elem` hs of
1001− True -> do focus holeName;
986+ True -> do focus holeName;
1002987 g <- goal
1003988 ulog <- getUnifyLog
1004− traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
989+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
1005990 elab ina t; return failed
1006991 False -> return failed
1007992 done_elaborating_arg f argName
@@ -1057,7 +1042,7 @@ pruneByType env t c as
10571042 getName (PRef _ n) = Just n
10581043 getName (PApp _ f _) = getName f
10591044 getName _ = Nothing
1060−
1045+
10611046pruneByType env (P _ n _) c as
10621047-- if the goal type is polymorphic, keep e
10631048 | [] <- lookupTy n c = as
@@ -1098,11 +1083,11 @@ trivial' ist
10981083 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
10991084proofSearch' ist rec depth prv top n hints
11001085 = do unifyProblems
1101− proofSearch rec prv depth
1086+ proofSearch rec prv depth
11021087 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
11031088
11041089resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
1105−resolveTC = resTC' []
1090+resolveTC = resTC' []
11061091
11071092resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
11081093resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
@@ -1112,7 +1097,7 @@ resTC' tcs defaultOn depth topg fn ist
11121097 ptm <- get_term
11131098 ulog <- getUnifyLog
11141099 hs <- get_holes
1115− traceWhen ulog ("Resolving class " ++ show g) $
1100+ traceWhen ulog ("Resolving class " ++ show g) $
11161101 try' (trivial' ist)
11171102 (do t <- goal
11181103 let (tc, ttypes) = unApply t
@@ -1129,7 +1114,7 @@ resTC' tcs defaultOn depth topg fn ist
11291114
11301115 -- HACK! Rather than giving a special name, better to have some kind
11311116 -- of flag in ClassInfo structure
1132− chaser (UN nm)
1117+ chaser (UN nm)
11331118 | ('@':'@':_) <- str nm = True -- old way
11341119 chaser (SN (ParentN _ _)) = True
11351120 chaser (NS n _) = chaser n
@@ -1173,7 +1158,7 @@ resTC' tcs defaultOn depth topg fn ist
11731158 args <- map snd <$> try' (apply (Var n) imps)
11741159 (match_apply (Var n) imps) True
11751160 ps' <- get_probs
1176− when (length ps < length ps' || unrecoverable ps') $
1161+ when (length ps < length ps' || unrecoverable ps') $
11771162 fail "Can't apply type class"
11781163-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
11791164 mapM_ (\ (_,n) -> do focus n
@@ -1181,7 +1166,7 @@ resTC' tcs defaultOn depth topg fn ist
11811166 let (tc', ttype) = unApply t'
11821167 let got = fst (unApply t)
11831168 let depth' = if tc' `elem` tcs
1184− then depth - 1 else depth
1169+ then depth - 1 else depth
11851170 resTC' (got : tcs) defaultOn depth' topg fn ist)
11861171 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
11871172 -- if there's any arguments left, we've failed to resolve
@@ -1232,11 +1217,11 @@ case_ ind autoSolve ist fn tm = do
12321217-- if a tactic adds unification problems, return an error
12331218
12341219runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
1235−runTac autoSolve ist fn tac
1220+runTac autoSolve ist fn tac
12361221 = do env <- get_env
12371222 g <- goal
12381223 let tac' = fmap (addImplBound ist (map fst env)) tac
1239− if autoSolve
1224+ if autoSolve
12401225 then runT tac'
12411226 else no_errors (runT tac')
12421227 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
@@ -1398,11 +1383,11 @@ runTac autoSolve ist fn tac
13981383 letbind scriptvar scriptTy (Var script)
13991384 focus script
14001385 ptm <- get_term
1401− elab ist toplevel ERHS [] (sMN 0 "tac")
1386+ elab ist toplevel ERHS [] (sMN 0 "tac")
14021387 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
14031388 (script', _) <- get_type_val (Var scriptvar)
14041389 -- now that we have the script apply
1405− -- it to the reflected goal
1390+ -- it to the reflected goal
14061391 restac <- getNameFrom (sMN 0 "restac")
14071392 claim restac tacticTy
14081393 focus restac
@@ -1482,7 +1467,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)
14821467
14831468reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
14841469reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1485−reifyApp _ t [Constant (I i)]
1470+reifyApp _ t [Constant (I i)]
14861471 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
14871472reifyApp _ t [x]
14881473 | t == reflm "Refine" = do n <- reifyTTName x
@@ -2223,4 +2208,3 @@ envTupleType
22232208 ]
22242209
22252210solveAll = try (do solve; solveAll) (return ())
2226−