@@ -31,9 +31,9 @@ import Data.List
3131import Data.Maybe
3232import Debug.Trace
3333
34−recheckC fc env t
34+recheckC fc env t
3535 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
36− ctxt <- getContext
36+ ctxt <- getContext
3737 (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of
3838 Error e -> tfail (At fc e)
3939 OK x -> return x
@@ -47,7 +47,7 @@ checkDef fc ns = do ctxt <- getContext
4747-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
4848elabType :: ElabInfo -> SyntaxInfo -> String ->
4949 FC -> FnOpts -> Name -> PTerm -> Idris ()
50−elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
50+elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
5151 n = liftname info n_in in -}
5252 do checkUndefined fc n
5353 ctxt <- getContext
@@ -59,12 +59,12 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
5959
6060 let ty = addImpl i ty'
6161 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
62− ((tyT, defer, is), log) <-
62+ ((tyT, defer, is), log) <-
6363 tclift $ elaborate ctxt n (TType (UVal 0)) []
6464 (errAt "type of " n (erun fc (build i info False n ty)))
6565 ds <- checkDef fc defer
6666 addDeferred ds
67− mapM_ (elabCaseBlock info opts) is
67+ mapM_ (elabCaseBlock info opts) is
6868 ctxt <- getContext
6969 logLvl 5 $ "Rechecking"
7070 logLvl 6 $ show tyT
@@ -147,7 +147,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
147147 i <- getIState
148148 t_in <- implicit syn n t_in
149149 let t = addImpl i t_in
150− ((t', defer, is), log) <-
150+ ((t', defer, is), log) <-
151151 tclift $ elaborate ctxt n (TType (UVal 0)) []
152152 (errAt "data declaration " n (erun fc (build i info False n t)))
153153 def' <- checkDef fc defer
@@ -156,11 +156,11 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
156156 (cty, _) <- recheckC fc [] t'
157157 logLvl 2 $ "---> " ++ show cty
158158 -- temporary, to check cons
159− when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
159+ when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
160160 cons <- mapM (elabCon info syn n codata) dcons
161161 ttag <- getName
162162 i <- getIState
163− let as = map (const Nothing) (getArgTys cty)
163+ let as = map (const Nothing) (getArgTys cty)
164164 let params = findParams (map snd cons)
165165 logLvl 2 $ "Parameters : " ++ show params
166166 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
@@ -172,7 +172,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
172172 collapseCons n cons
173173 updateContext (addDatatype (Data n ttag cty cons))
174174 mapM_ (checkPositive n) cons
175− where
175+ where
176176 -- parameters are names which are unchanged across the structure,
177177 -- which appear exactly once in the return type of a constructor
178178
@@ -184,14 +184,14 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
184184 paramPos allapps
185185
186186 paramPos [] = []
187− paramPos (args : rest)
187+ paramPos (args : rest)
188188 = dropNothing $ keepSame (zip [0..] args) rest
189189
190190 dropNothing [] = []
191191 dropNothing ((x, Nothing) : ts) = dropNothing ts
192192 dropNothing ((x, _) : ts) = x : dropNothing ts
193193
194− keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
194+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
195195 [(Int, Maybe Name)]
196196 keepSame as [] = as
197197 keepSame as (args : rest) = keepSame (update as args) rest
@@ -211,14 +211,14 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
211211 getDataApp _ = []
212212
213213 -- keep the arguments which are single names, which don't appear
214− -- elsewhere
214+ -- elsewhere
215215
216216 mParam args [] = []
217217 mParam args (P Bound n _ : rest)
218− | count n args == 1
218+ | count n args == 1
219219 = Just n : mParam args rest
220220 where count n [] = 0
221− count n (t : ts)
221+ count n (t : ts)
222222 | n `elem` freeNames t = 1 + count n ts
223223 | otherwise = count n ts
224224 mParam args (_ : rest) = Nothing : mParam args rest
@@ -253,7 +253,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
253253 believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
254254 (Bind (UN "b") (Pi (TType (UVar (-2))))
255255 (Bind (UN "x") (Pi (V 1)) (V 1)))
256− elabBelieveMe
256+ elabBelieveMe
257257 = do let prim__believe_me = (UN "prim__believe_me")
258258 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
259259 setTotality prim__believe_me (Partial NotCovering)
@@ -279,7 +279,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
279279 (Bind (UN "y") (Pi (V 1))
280280 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
281281 [V 3, V 2, V 1, V 0]]))))
282− elabSynEq
282+ elabSynEq
283283 = do let synEq = UN "prim__syntactic_eq"
284284
285285 updateContext (addOperator synEq synEqTy 4 p_synEq)
@@ -375,10 +375,10 @@ elabTransform info fc safe lhs_in rhs_in
375375 addIBC (IBCTrans (clhs_tm, crhs_tm))
376376
377377
378−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
378+elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
379379 PTerm -> String -> Name -> PTerm -> Idris ()
380380elabRecord info syn doc fc tyn ty cdoc cn cty
381− = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
381+ = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
382382 cty' <- implicit syn cn cty
383383 i <- getIState
384384 cty <- case lookupTy cn (tt_ctxt i) of
@@ -408,8 +408,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
408408 = do i <- getIState
409409 idrisCatch (do elabDecl' EAll info ty
410410 elabDecl' EAll info val)
411− (\v -> do iputStrLn $ show fc ++
412− ":Warning - can't generate setter for " ++
411+ (\v -> do iputStrLn $ show fc ++
412+ ":Warning - can't generate setter for " ++
413413 show fn ++ " (" ++ show ty ++ ")"
414414 putIState i)
415415
@@ -459,9 +459,9 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
459459 let lhs = PApp fc (PRef fc pn)
460460 [pexp (PApp fc (PRef fc cn) iargs)]
461461 let rhs = PRef fc (mkp pn)
462− let pclause = PClause fc pn lhs [] rhs []
462+ let pclause = PClause fc pn lhs [] rhs []
463463 return [pfnTy, PClauses fc [] pn [pclause]]
464−
464+
465465 implicitise (pa, t) = pa { getTm = t }
466466
467467 mkUpdate recty k num ((pn, pty), pos)
@@ -484,7 +484,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
484484 (map pexp rhsArgs)) []
485485 return (pn, pfnTy, PClauses fc [] setname [pclause])
486486
487−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
487+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
488488 (String, Name, PTerm, FC) -> Idris (Name, Type)
489489elabCon info syn tn codata (doc, n, t_in, fc)
490490 = do checkUndefined fc n
@@ -493,7 +493,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
493493 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
494494 let t = addImpl i t_in
495495 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
496− ((t', defer, is), log) <-
496+ ((t', defer, is), log) <-
497497 tclift $ elaborate ctxt n (TType (UVal 0)) []
498498 (errAt "constructor " n (erun fc (build i info False n t)))
499499 logLvl 2 $ "Rechecking " ++ show t'
@@ -512,8 +512,8 @@ elabCon info syn tn codata (doc, n, t_in, fc)
512512 return (n, cty')
513513 where
514514 tyIs (Bind n b sc) = tyIs sc
515− tyIs t | (P _ n' _, _) <- unApply t
516− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))
515+ tyIs t | (P _ n' _, _) <- unApply t
516+ = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))
517517 else return ()
518518 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))
519519
@@ -523,7 +523,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
523523-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
524524-- top-level definition.
525525elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
526−elabClauses info fc opts n_in cs = let n = liftname info n_in in
526+elabClauses info fc opts n_in cs = let n = liftname info n_in in
527527 do ctxt <- getContext
528528 -- Check n actually exists, with no definition yet
529529 let tys = lookupTy n ctxt
@@ -535,7 +535,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
535535 -- question: CAFs in where blocks?
536536 tclift $ tfail $ At fc (NoTypeDecl n)
537537 [ty] -> return ty
538− pats_in <- mapM (elabClause info opts)
538+ pats_in <- mapM (elabClause info opts)
539539 (zip [0..] cs)
540540 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
541541
@@ -553,9 +553,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
553553 _ -> False
554554 solveDeferred n
555555 ist <- getIState
556− when doNothing $
556+ when doNothing $
557557 case lookupCtxt n (idris_optimisation ist) of
558− [oi] -> do let opts = addDef n (oi { collapsible = True })
558+ [oi] -> do let opts = addDef n (oi { collapsible = True })
559559 (idris_optimisation ist)
560560 putIState (ist { idris_optimisation = opts })
561561 _ -> do let opts = addDef n (Optimise True False [] [])
@@ -563,10 +563,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
563563 putIState (ist { idris_optimisation = opts })
564564 addIBC (IBCOpt n)
565565 ist <- getIState
566− let pats = doTransforms ist pats_in
566+ let pats = doTransforms ist pats_in
567567
568− -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
569− -- show l ++ " = " ++
568+ -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
569+ -- show l ++ " = " ++
570570 -- show r) pats))
571571 let tcase = opt_typecase (idris_options ist)
572572
@@ -583,7 +583,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
583583 -- This will get further optimised for run-time, and, separately,
584584 -- further inlined to help with totality checking.
585585 let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats
586−
586+
587587 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef
588588
589589 -- TODO: Inlining on initial definition happens here.
@@ -600,7 +600,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
600600
601601 -- patterns after collapsing optimisation applied
602602 -- (i.e. check if the function should do nothing at run time)
603− optpats <- if doNothing
603+ optpats <- if doNothing
604604 then return $ [Right (mkApp (P Bound n Erased)
605605 (take numArgs (repeat Erased)), Erased)]
606606 else stripCollapsed pats
@@ -610,22 +610,22 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
610610 _ -> return ()
611611
612612 let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats
613− tree@(CaseDef scargs sc _) <- tclift $
613+ tree@(CaseDef scargs sc _) <- tclift $
614614 simpleCase tcase False reflect CompileTime fc pdef
615615 cov <- coverage
616616 pmissing <-
617− if cov
617+ if cov
618618 then do missing <- genClauses fc n (map getLHS pdef) cs
619− -- missing <- genMissing n scargs sc
619+ -- missing <- genMissing n scargs sc
620620 missing' <- filterM (checkPossible info fc True n) missing
621621 let clhs = map getLHS pdef
622− logLvl 2 $ "Must be unreachable:\n" ++
622+ logLvl 2 $ "Must be unreachable:\n" ++
623623 showSep "\n" (map (showImp Nothing True False) missing') ++
624624 "\nAgainst: " ++
625625 showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
626626 -- filter out anything in missing' which is
627627 -- matched by any of clhs. This might happen since
628− -- unification may force a variable to take a
628+ -- unification may force a variable to take a
629629 -- particular form, rather than force a case
630630 -- to be impossible.
631631 return (filter (noMatch ist clhs) missing')
@@ -633,7 +633,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
633633 let pcover = null pmissing
634634
635635 -- pdef' is the version that gets compiled for run-time
636− pdef' <- applyOpts optpdef
636+ pdef' <- applyOpts optpdef
637637 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
638638
639639 ist <- getIState
@@ -641,8 +641,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
641641 let tot = if pcover || AssertTotal `elem` opts
642642 then Unchecked -- finish checking later
643643 else Partial NotCovering -- already know it's not total
644− -- case lookupCtxt (namespace info) n (idris_flags ist) of
645− -- [fs] -> if TotalFn `elem` fs
644+ -- case lookupCtxt (namespace info) n (idris_flags ist) of
645+ -- [fs] -> if TotalFn `elem` fs
646646 -- then case tot of
647647 -- Total _ -> return ()
648648 -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
@@ -652,7 +652,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
652652 CaseDef _ _ [] -> return ()
653653 CaseDef _ _ xs -> mapM_ (\x ->
654654 iputStrLn $ show fc ++
655− ":warning - Unreachable case: " ++
655+ ":warning - Unreachable case: " ++
656656 show (delab ist x)) xs
657657 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
658658
@@ -662,12 +662,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
662662 logLvl 3 $ "Optimised: " ++ show tree'
663663 ctxt <- getContext
664664 ist <- getIState
665− putIState (ist { idris_patdefs = addDef n (pdef', pmissing)
665+ putIState (ist { idris_patdefs = addDef n (pdef', pmissing)
666666 (idris_patdefs ist) })
667667 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
668668 case lookupTy n ctxt of
669669 [ty] -> do updateContext (addCasedef n caseInfo
670− tcase knowncovering
670+ tcase knowncovering
671671 reflect
672672 (AssertTotal `elem` opts)
673673 pats
@@ -698,14 +698,14 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
698698 where
699699 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True) tm of
700700 Right _ -> False
701− Left miss -> True) cs
701+ Left miss -> True) cs
702702
703703 checkUndefined n ctxt = case lookupDef n ctxt of
704704 [] -> return ()
705705 [TyDecl _ _] -> return ()
706706 _ -> tclift $ tfail (At fc (AlreadyDefined n))
707707
708− debind (Right (x, y)) = let (vs, x') = depat [] x
708+ debind (Right (x, y)) = let (vs, x') = depat [] x
709709 (_, y') = depat [] y in
710710 (vs, x', y')
711711 debind (Left x) = let (vs, x') = depat [] x in
@@ -713,26 +713,26 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
713713
714714 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
715715 depat acc x = (acc, x)
716−
716+
717717 getLHS (_, l, _) = l
718718
719− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
719+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
720720 simple_lhs ctxt t = t
721721
722722 specNames [] = Nothing
723723 specNames (Specialise ns : _) = Just ns
724724 specNames (_ : xs) = specNames xs
725725
726− sameLength ((_, x, _) : xs)
726+ sameLength ((_, x, _) : xs)
727727 = do l <- sameLength xs
728728 let (f, as) = unApply x
729729 if (null xs || l == length as) then return (length as)
730730 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
731731 sameLength [] = return 0
732732
733− -- apply all transformations (just specialisation for now, add
733+ -- apply all transformations (just specialisation for now, add
734734 -- user defined transformation rules later)
735− doTransforms ist pats =
735+ doTransforms ist pats =
736736 case specNames opts of
737737 Nothing -> pats
738738 Just ns -> partial_eval (tt_ctxt ist) ns pats
@@ -750,14 +750,14 @@ elabValBind info aspat tm_in
750750 -- * ordinary elaboration
751751 -- * elaboration as a Type
752752 -- * elaboration as a function a -> b
753−
754− ((tm', defer, is), _) <-
755−-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
753+
754+ ((tm', defer, is), _) <-
755+-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
756756-- (build i info aspat (MN 0 "val") tm))
757757 tclift (elaborate ctxt (MN 0 "val") infP []
758758 (build i info aspat (MN 0 "val") (infTerm tm)))
759759 let vtm = orderPats (getInferTerm tm')
760− let bargs = getPBtys vtm
760+ let bargs = getPBtys vtm
761761
762762 def' <- checkDef (fileFC "(input)") defer
763763 addDeferred def'
@@ -796,7 +796,7 @@ checkPossible info fc tcgen fname lhs_in
796796-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
797797 err@(Error _) -> return False
798798
799−elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
799+elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
800800 Idris (Either Term (Term, Term))
801801elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
802802 = do let tcgen = Dictionary `elem` opts
@@ -805,7 +805,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
805805 True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
806806 False -> do ptm <- mkPatTm lhs_in
807807 return (Left ptm)
808−elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
808+elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
809809 = do let tcgen = Dictionary `elem` opts
810810 ctxt <- getContext
811811
@@ -818,15 +818,15 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
818818 _ -> error "Can't happen (elabClause function type)"
819819 let fn_is = case lookupCtxt fname (idris_implicits i) of
820820 [t] -> t
821− _ -> []
821+ _ -> []
822822 let params = getParamsInType i [] fn_is fn_ty
823823 let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))
824824 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
825825 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
826826
827− ((lhs', dlhs, []), _) <-
827+ ((lhs', dlhs, []), _) <-
828828 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
829− (errAt "left hand side of " fname
829+ (errAt "left hand side of " fname
830830 (erun fc (buildTC i info True tcgen fname (infTerm lhs))))
831831 let lhs_tm = orderPats (getInferTerm lhs')
832832 let lhs_ty = getInferType lhs'
@@ -848,7 +848,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
848848 let defs = nub (decls ++ concatMap defined whereblock)
849849 let newargs = pvars ist lhs_tm
850850 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
851−
851+
852852 -- Split the where block into declarations with a type, and those
853853 -- without
854854 -- Elaborate those with a type *before* RHS, those without *after*
@@ -864,12 +864,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
864864 logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
865865 ctxt <- getContext -- new context with where block added
866866 logLvl 5 "STARTING CHECK"
867− ((rhs', defer, is), _) <-
867+ ((rhs', defer, is), _) <-
868868 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
869869 (do pbinds lhs_tm
870− (_, _, is) <- errAt "right hand side of " fname
870+ (_, _, is) <- errAt "right hand side of " fname
871871 (erun fc (build i info False fname rhs))
872− errAt "right hand side of " fname
872+ errAt "right hand side of " fname
873873 (erun fc $ psolve lhs_tm)
874874 tt <- get_term
875875 let (tm, ds) = runState (collectDeferred (Just fname) tt) []
@@ -897,10 +897,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
897897 checkInferred fc (delab' i crhs True) rhs
898898 return $ Right (clhs, crhs)
899899 where
900− decorate (NS x ns)
901− = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
900+ decorate (NS x ns)
901+ = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
902902-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
903− decorate x
903+ decorate x
904904 = SN (WhereN cnum fname x)
905905-- = NS (SN (WhereN cnum fname x)) [show cnum]
906906-- = NS (UN ('#':show x)) [show cnum, show fname]
@@ -909,18 +909,18 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
909909 sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)
910910 = let (bf, af) = sepBlocks' (n : ns) bs in
911911 (d : bf, af)
912− sepBlocks' ns (d@(PClauses _ _ n _) : bs)
912+ sepBlocks' ns (d@(PClauses _ _ n _) : bs)
913913 | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in
914914 (bf, d : af)
915915 sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
916916 (b : bf, af)
917917 sepBlocks' ns [] = ([], [])
918918
919− pinfo ns ps i
919+ pinfo ns ps i
920920 = let ds = concatMap declared ps
921921 newps = params info ++ ns
922922 dsParams = map (\n -> (n, map fst newps)) ds
923− newb = addAlist dsParams (inblock info)
923+ newb = addAlist dsParams (inblock info)
924924 l = liftname info in
925925 info { params = newps,
926926 inblock = newb,
@@ -929,24 +929,24 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
929929 -- _ -> MN i (show n)) . l
930930 }
931931
932− getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
932+ getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
933933 = getParamsInType i env is (instantiate (P Bound n t) sc)
934− getParamsInType i env (_ : is) (Bind n (Pi t) sc)
934+ getParamsInType i env (_ : is) (Bind n (Pi t) sc)
935935 = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)
936936 getParamsInType i env is tm@(App f a)
937− | (P _ tn _, args) <- unApply tm
937+ | (P _ tn _, args) <- unApply tm
938938 = case lookupCtxt tn (idris_datatypes i) of
939939 [t] -> nub $ paramNames args env (param_pos t) ++
940− getParamsInType i env is f ++
940+ getParamsInType i env is f ++
941941 getParamsInType i env is a
942− [] -> nub $ getParamsInType i env is f ++
942+ [] -> nub $ getParamsInType i env is f ++
943943 getParamsInType i env is a
944− | otherwise = nub $ getParamsInType i env is f ++
944+ | otherwise = nub $ getParamsInType i env is f ++
945945 getParamsInType i env is a
946946 getParamsInType i _ _ _ = []
947947
948948 paramNames args env [] = []
949− paramNames args env (p : ps)
949+ paramNames args env (p : ps)
950950 | length args > p = case args!!p of
951951 P _ n _ -> if n `elem` env
952952 then n : paramNames args env ps
@@ -964,7 +964,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
964964 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
965965 propagateParams ps x = x
966966
967−elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
967+elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
968968 = do let tcgen = Dictionary `elem` opts
969969 ctxt <- getContext
970970 -- Build the LHS as an "Infer", and pull out its type and
@@ -972,7 +972,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
972972 i <- getIState
973973 let lhs = addImplPat i lhs_in
974974 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
975− ((lhs', dlhs, []), _) <-
975+ ((lhs', dlhs, []), _) <-
976976 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
977977 (errAt "left hand side of with in " fname
978978 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) )
@@ -986,12 +986,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
986986 let wval = addImplBound i (map fst bargs) wval_in
987987 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
988988 -- Elaborate wval in this context
989− ((wval', defer, is), _) <-
990− tclift $ elaborate ctxt (MN 0 "withRHS")
989+ ((wval', defer, is), _) <-
990+ tclift $ elaborate ctxt (MN 0 "withRHS")
991991 (bindTyArgs PVTy bargs infP) []
992992 (do pbinds lhs_tm
993993 -- TODO: may want where here - see winfo abpve
994− (_', d, is) <- errAt "with value in " fname
994+ (_', d, is) <- errAt "with value in " fname
995995 (erun fc (build i info False fname (infTerm wval)))
996996 erun fc $ psolve lhs_tm
997997 tt <- get_term
@@ -1008,18 +1008,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
10081008 -- rather than a de Bruijn index.
10091009 let pdeps = usedNamesIn pvars i (delab i cwvalty)
10101010 let (bargs_pre, bargs_post) = split pdeps bargs []
1011− logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
1011+ logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
10121012 " depends on " ++ show pdeps ++ " from " ++ show pvars)
10131013 logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
10141014 windex <- getName
10151015 -- build a type declaration for the new function:
1016− -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
1016+ -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
10171017 let wargval = getRetTy cwvalN
10181018 let wargtype = getRetTy cwvaltyN
10191019 logLvl 5 ("Abstract over " ++ show wargval)
1020− let wtype = bindTyArgs Pi (bargs_pre ++
1021− (MN 0 "warg", wargtype) :
1022− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
1020+ let wtype = bindTyArgs Pi (bargs_pre ++
1021+ (MN 0 "warg", wargtype) :
1022+ map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
10231023 (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
10241024 logLvl 3 ("New function type " ++ show wtype)
10251025 let wname = MN windex (show fname)
@@ -1041,8 +1041,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
10411041 mapM_ (elabDecl EAll info) wb
10421042
10431043 -- rhs becomes: fname' ps wval
1044− let rhs = PApp fc (PRef fc wname)
1045− (map (pexp . (PRef fc) . fst) bargs_pre ++
1044+ let rhs = PApp fc (PRef fc wname)
1045+ (map (pexp . (PRef fc) . fst) bargs_pre ++
10461046 pexp wval :
10471047 (map (pexp . (PRef fc) . fst) bargs_post))
10481048 logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)
@@ -1074,25 +1074,25 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
10741074 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
10751075 = do i <- getIState
10761076 let tm = addImplPat i tm_in
1077− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
1077+ logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
10781078 showImp Nothing True False toplhs)
10791079 case matchClause i toplhs tm of
10801080 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")
1081− Right mvars ->
1081+ Right mvars ->
10821082 do logLvl 3 ("Match vars : " ++ show mvars)
10831083 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
10841084 return $ PClause fc wname lhs ws rhs wheres
10851085 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
10861086 = do i <- getIState
10871087 let tm = addImplPat i tm_in
1088− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
1088+ logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
10891089 showImp Nothing True False toplhs)
10901090 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
10911091 case matchClause i toplhs tm of
10921092 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
1093− Right mvars ->
1093+ Right mvars ->
10941094 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1095− return $ PWith fc wname lhs ws wval withs'
1095+ return $ PWith fc wname lhs ws wval withs'
10961096 mkAux wname toplhs ns ns' c
10971097 = ifail $ show fc ++ "badly formed with clause"
10981098
@@ -1102,11 +1102,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
11021102 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w
11031103 = let ns = map (keepMvar (map fst mvars) fc') ns_in
11041104 ns' = map (keepMvar (map fst mvars) fc') ns_in' in
1105− return $ substMatches mvars $
1106− PApp fc (PRef fc' wname)
1105+ return $ substMatches mvars $
1106+ PApp fc (PRef fc' wname)
11071107 (map pexp ns ++ pexp w : (map pexp ns'))
1108− updateLHS n wname mvars ns ns' tm w
1109− = ifail $ "Not implemented match " ++ show tm
1108+ updateLHS n wname mvars ns ns' tm w
1109+ = ifail $ "Not implemented match " ++ show tm
11101110
11111111 keepMvar mvs fc v | v `elem` mvs = PRef fc v
11121112 | otherwise = Placeholder
@@ -1118,16 +1118,16 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
11181118 split deps ((n, ty) : rest) pre
11191119 | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)
11201120 | otherwise = split deps rest ((n, ty) : pre)
1121− split deps [] pre = (reverse pre, [])
1121+ split deps [] pre = (reverse pre, [])
11221122
11231123 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
11241124
11251125data MArgTy = IA | EA | CA deriving Show
11261126
11271127elabClass :: ElabInfo -> SyntaxInfo -> String ->
1128− FC -> [PTerm] ->
1128+ FC -> [PTerm] ->
11291129 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1130−elabClass info syn doc fc constraints tn ps ds
1130+elabClass info syn doc fc constraints tn ps ds
11311131 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
11321132 let tty = pibind ps PType
11331133 let constraint = PApp fc (PRef fc tn)
@@ -1137,20 +1137,20 @@ elabClass info syn doc fc constraints tn ps ds
11371137 let mnames = map getMName mdecls
11381138 logLvl 2 $ "Building methods " ++ show mnames
11391139 ims <- mapM (tdecl mnames) mdecls
1140− defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
1140+ defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
11411141 (filter clause ds)
1142− let (methods, imethods)
1142+ let (methods, imethods)
11431143 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
11441144 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
1145− addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])
1145+ addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])
11461146 -- build instance constructor type
11471147 -- decorate names of functions to ensure they can't be referred
11481148 -- to elsewhere in the class declaration
11491149 -- TODO: Remove mdec to make it a dependent record, which would
11501150 -- allow dependent type classes, but building instances will
11511151 -- then need some attention.
1152− let cty = impbind ps $ conbind constraints
1153− $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)
1152+ let cty = impbind ps $ conbind constraints
1153+ $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)
11541154 constraint
11551155 let cons = [("", cn, cty, fc)]
11561156 let ddecl = PDatadecl tn tty cons
@@ -1158,7 +1158,7 @@ elabClass info syn doc fc constraints tn ps ds
11581158 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl
11591159 -- for each constraint, build a top level function to chase it
11601160 logLvl 5 $ "Building functions"
1161− let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
1161+ let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
11621162 ++ using syn }
11631163 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints
11641164 mapM_ (elabDecl EAll info) (concat fns)
@@ -1172,19 +1172,19 @@ elabClass info syn doc fc constraints tn ps ds
11721172 where
11731173 nodoc (n, (_, o, t)) = (n, (o, t))
11741174 pibind [] x = x
1175− pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
1175+ pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
11761176
11771177 mdec (UN n) = SN (MethodN (UN n))
11781178 mdec (NS x n) = NS (mdec x) n
11791179 mdec x = x
11801180
11811181 impbind [] x = x
1182− impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
1182+ impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
11831183 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
11841184 conbind [] x = x
11851185
11861186 getMName (PTy _ _ _ _ n _) = nsroot n
1187− tdecl allmeths (PTy doc syn _ o n t)
1187+ tdecl allmeths (PTy doc syn _ o n t)
11881188 = do t' <- implicit' syn allmeths n t
11891189 logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
11901190 return ( (n, (toExp (map fst ps) Exp t')),
@@ -1192,12 +1192,12 @@ elabClass info syn doc fc constraints tn ps ds
11921192 (n, (syn, o, t) ) )
11931193 tdecl _ _ = ifail "Not allowed in a class declaration"
11941194
1195− -- Create default definitions
1195+ -- Create default definitions
11961196 defdecl mtys c d@(PClauses fc opts n cs) =
11971197 case lookup n mtys of
11981198 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
11991199 let ds = map (decorateid defaultdec)
1200− [PTy "" syn fc [] n ty',
1200+ [PTy "" syn fc [] n ty',
12011201 PClauses fc (o ++ opts) n cs]
12021202 iLOG (show ds)
12031203 return (n, ((defaultdec n, ds!!1), ds))
@@ -1214,7 +1214,7 @@ elabClass info syn doc fc constraints tn ps ds
12141214
12151215 -- Generate a function for chasing a dictionary constraint
12161216 cfun cn c syn all con
1217− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
1217+ = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
12181218 -- SN (ParentN cn (show con))
12191219 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
12201220 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
@@ -1238,7 +1238,7 @@ elabClass info syn doc fc constraints tn ps ds
12381238
12391239 -- Generate a top level function which looks up a method in a given
12401240 -- dictionary (this is inlinable, always)
1241− tfun cn c syn all (m, (doc, o, ty))
1241+ tfun cn c syn all (m, (doc, o, ty))
12421242 = do let ty' = insertConstraint c ty
12431243 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
12441244 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
@@ -1260,13 +1260,13 @@ elabClass info syn doc fc constraints tn ps ds
12601260 getMeth (m:ms) (a:as) x | x == a = PRef fc m
12611261 | otherwise = getMeth ms as x
12621262
1263− lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns
1264− lhsArgs (IA : xs) ns = lhsArgs xs ns
1263+ lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns
1264+ lhsArgs (IA : xs) ns = lhsArgs xs ns
12651265 lhsArgs (CA : xs) ns = lhsArgs xs ns
12661266 lhsArgs [] _ = []
12671267
1268− rhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns
1269− rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
1268+ rhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns
1269+ rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
12701270 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
12711271 rhsArgs [] _ = []
12721272
@@ -1281,43 +1281,43 @@ elabClass info syn doc fc constraints tn ps ds
12811281 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
12821282 toExp ns e sc = sc
12831283
1284−elabInstance :: ElabInfo -> SyntaxInfo ->
1284+elabInstance :: ElabInfo -> SyntaxInfo ->
12851285 FC -> [PTerm] -> -- constraints
1286− Name -> -- the class
1287− [PTerm] -> -- class parameters (i.e. instance)
1286+ Name -> -- the class
1287+ [PTerm] -> -- class parameters (i.e. instance)
12881288 PTerm -> -- full instance type
12891289 Maybe Name -> -- explicit name
12901290 [PDecl] -> Idris ()
12911291elabInstance info syn fc cs n ps t expn ds
1292− = do i <- getIState
1292+ = do i <- getIState
12931293 (n, ci) <- case lookupCtxtName n (idris_classes i) of
12941294 [c] -> return c
12951295 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
12961296 let constraint = PApp fc (PRef fc n) (map pexp ps)
12971297 let iname = case expn of
1298− Nothing -> SN (InstanceN n (map show ps))
1298+ Nothing -> SN (InstanceN n (map show ps))
12991299 -- UN ('@':show n ++ "$" ++ show ps)
13001300 Just nm -> nm
13011301 -- if the instance type matches any of the instances we have already,
13021302 -- and it's not a named instance, then it's overlapping, so report an error
13031303 case expn of
1304− Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)
1304+ Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)
13051305 addInstance intInst n iname
1306− Just _ -> addInstance intInst n iname
1306+ Just _ -> addInstance intInst n iname
13071307 elabType info syn "" fc [] iname t
13081308 let ips = zip (class_params ci) ps
13091309 let ns = case n of
13101310 NS n ns' -> ns'
13111311 _ -> []
1312− -- get the implicit parameters that need passing through to the
1312+ -- get the implicit parameters that need passing through to the
13131313 -- where block
13141314 wparams <- mapM (\p -> case p of
13151315 PApp _ _ args -> getWParams args
13161316 _ -> return []) ps
13171317 let pnames = map pname (concat (nub wparams))
1318− let mtys = map (\ (n, (op, t)) ->
1318+ let mtys = map (\ (n, (op, t)) ->
13191319 let t' = substMatchesShadow ips pnames t in
1320− (decorate ns iname n,
1320+ (decorate ns iname n,
13211321 op, coninsert cs t', t'))
13221322 (class_methods ci)
13231323 logLvl 3 (show (mtys, ips))
@@ -1329,12 +1329,12 @@ elabInstance info syn fc cs n ps t expn ds
13291329 let wbVals = map (decorateid (decorate ns iname)) ds'
13301330 let wb = wbTys ++ wbVals
13311331 logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)
1332− logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
1332+ logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
13331333 show (concat (nub wparams))
13341334 let lhs = PRef fc iname
13351335 let rhs = PApp fc (PRef fc (instanceName ci))
13361336 (map (pexp . mkMethApp) mtys)
1337− let idecls = [PClauses fc [Dictionary] iname
1337+ let idecls = [PClauses fc [Dictionary] iname
13381338 [PClause fc iname lhs [] rhs wb]]
13391339 iLOG (show idecls)
13401340 mapM (elabDecl EAll info) idecls
@@ -1360,23 +1360,23 @@ elabInstance info syn fc cs n ps t expn ds
13601360 Right _ -> overlapping tret tret'
13611361 Left _ -> return ()
13621362 _ -> return ()
1363− overlapping t t' = tclift $ tfail (At fc (Msg $
1363+ overlapping t t' = tclift $ tfail (At fc (Msg $
13641364 "Overlapping instance: " ++ show t' ++ " already defined"))
13651365 getRetType (PPi _ _ _ sc) = getRetType sc
13661366 getRetType t = t
13671367
1368− mkMethApp (n, _, _, ty)
1368+ mkMethApp (n, _, _, ty)
13691369 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
1370− lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
1370+ lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
13711371 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1372− lamBind i (PPi _ n ty sc) sc'
1372+ lamBind i (PPi _ n ty sc) sc'
13731373 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
13741374 lamBind i _ sc = sc
1375− methArgs i (PPi (Imp _ _ _ _) n ty sc)
1375+ methArgs i (PPi (Imp _ _ _ _) n ty sc)
13761376 = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
1377− methArgs i (PPi (Exp _ _ _ _) n ty sc)
1377+ methArgs i (PPi (Exp _ _ _ _) n ty sc)
13781378 = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
1379− methArgs i (PPi (Constraint _ _ _) n ty sc)
1379+ methArgs i (PPi (Constraint _ _ _) n ty sc)
13801380 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
13811381 methArgs i _ = []
13821382
@@ -1384,8 +1384,8 @@ elabInstance info syn fc cs n ps t expn ds
13841384 papp fc f as = PApp fc f as
13851385
13861386 getWParams [] = return []
1387− getWParams (p : ps)
1388− | PRef _ n <- getTm p
1387+ getWParams (p : ps)
1388+ | PRef _ n <- getTm p
13891389 = do ps' <- getWParams ps
13901390 ctxt <- getContext
13911391 case lookupP n ctxt of
@@ -1405,16 +1405,16 @@ elabInstance info syn fc cs n ps t expn ds
14051405 coninsert cs sc = conbind cs sc
14061406
14071407 insertDefaults :: IState -> Name ->
1408− [(Name, (Name, PDecl))] -> [String] ->
1408+ [(Name, (Name, PDecl))] -> [String] ->
14091409 [PDecl] -> [PDecl]
14101410 insertDefaults i iname [] ns ds = ds
1411− insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
1411+ insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
14121412 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
14131413
14141414 insertDef i meth def clauses ns iname decls
14151415 | null $ filter (clauseFor meth iname ns) decls
14161416 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
1417− -- trace (show newd) $
1417+ -- trace (show newd) $
14181418 decls ++ [newd]
14191419 | otherwise = decls
14201420
@@ -1425,12 +1425,12 @@ elabInstance info syn fc cs n ps t expn ds
14251425
14261426 checkInClass ns meth
14271427 | not (null (filter (eqRoot meth) ns)) = return ()
1428− | otherwise = tclift $ tfail (At fc (Msg $
1428+ | otherwise = tclift $ tfail (At fc (Msg $
14291429 show meth ++ " not a method of class " ++ show n))
14301430
14311431 eqRoot x y = nsroot x == nsroot y
14321432
1433− clauseFor m iname ns (PClauses _ _ m' _)
1433+ clauseFor m iname ns (PClauses _ _ m' _)
14341434 = decorate ns iname m == decorate ns iname m'
14351435 clauseFor m iname ns _ = False
14361436
@@ -1460,17 +1460,17 @@ elabInstance info syn fc cs n ps t expn ds
14601460-}
14611461
14621462decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t
1463−decorateid decorate (PClauses f o n cs)
1463+decorateid decorate (PClauses f o n cs)
14641464 = PClauses f o (decorate n) (map dc cs)
14651465 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds
1466− dc (PWith fc n t as w ds)
1467− = PWith fc (decorate n) (dappname t) as w
1466+ dc (PWith fc n t as w ds)
1467+ = PWith fc (decorate n) (dappname t) as w
14681468 (map (decorateid decorate) ds)
14691469 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
14701470 dappname t = t
14711471
14721472
1473−pbinds (Bind n (PVar t) sc) = do attack; patbind n
1473+pbinds (Bind n (PVar t) sc) = do attack; patbind n
14741474 pbinds sc
14751475pbinds tm = return ()
14761476
@@ -1495,8 +1495,8 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds
14951495-- mapM_ (elabDecl EDefns info) ds
14961496
14971497elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
1498−elabDecl what info d
1499− = idrisCatch (elabDecl' what info d)
1498+elabDecl what info d
1499+ = idrisCatch (elabDecl' what info d)
15001500 (\e -> do setErrLine (getErrLine e)
15011501 ist <- getIState
15021502 let h = idris_outh ist
@@ -1504,24 +1504,24 @@ elabDecl what info d
15041504
15051505elabDecl' _ info (PFix _ _ _)
15061506 = return () -- nothing to elaborate
1507−elabDecl' _ info (PSyntax _ p)
1507+elabDecl' _ info (PSyntax _ p)
15081508 = return () -- nothing to elaborate
1509−elabDecl' what info (PTy doc s f o n ty)
1509+elabDecl' what info (PTy doc s f o n ty)
15101510 | what /= EDefns
15111511 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
15121512 elabType info s doc f o n ty
1513−elabDecl' what info (PPostulate doc s f o n ty)
1513+elabDecl' what info (PPostulate doc s f o n ty)
15141514 | what /= EDefns
15151515 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
15161516 elabPostulate info s doc f o n ty
1517−elabDecl' what info (PData doc s f co d)
1517+elabDecl' what info (PData doc s f co d)
15181518 | what /= ETypes
15191519 = do iLOG $ "Elaborating " ++ show (d_name d)
15201520 elabData info s doc f co d
1521− | otherwise
1521+ | otherwise
15221522 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)
15231523 elabData info s doc f co (PLaterdecl (d_name d) (d_tcon d))
1524−elabDecl' what info d@(PClauses f o n ps)
1524+elabDecl' what info d@(PClauses f o n ps)
15251525 | what /= ETypes
15261526 = do iLOG $ "Elaborating clause " ++ show n
15271527 i <- getIState -- get the type options too
@@ -1529,7 +1529,7 @@ elabDecl' what info d@(PClauses f o n ps)
15291529 [fs] -> fs
15301530 [] -> []
15311531 elabClauses info f (o ++ o') n ps
1532−elabDecl' what info (PMutual f ps)
1532+elabDecl' what info (PMutual f ps)
15331533 = do mapM_ (elabDecl ETypes info) ps
15341534 mapM_ (elabDecl EDefns info) ps
15351535 -- Do totality checking after entire mutual block
@@ -1541,32 +1541,32 @@ elabDecl' what info (PMutual f ps)
15411541 mapM_ checkDeclTotality (idris_totcheck i)
15421542 clear_totcheck
15431543
1544−elabDecl' what info (PParams f ns ps)
1544+elabDecl' what info (PParams f ns ps)
15451545 = do i <- getIState
15461546 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
15471547 show (concatMap tldeclared ps)
15481548 let nblock = pblock i
1549− mapM_ (elabDecl' what info) nblock
1549+ mapM_ (elabDecl' what info) nblock
15501550 where
15511551 pinfo = let ds = concatMap tldeclared ps
15521552 newps = params info ++ ns
15531553 dsParams = map (\n -> (n, map fst newps)) ds
1554− newb = addAlist dsParams (inblock info) in
1554+ newb = addAlist dsParams (inblock info) in
15551555 info { params = newps,
15561556 inblock = newb }
1557− pblock i = map (expandParamsD False i id ns
1557+ pblock i = map (expandParamsD False i id ns
15581558 (concatMap tldeclared ps)) ps
15591559
15601560elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
15611561 where
15621562 ninfo = case namespace info of
15631563 Nothing -> info { namespace = Just [n] }
1564− Just ns -> info { namespace = Just (n:ns) }
1565−elabDecl' what info (PClass doc s f cs n ps ds)
1564+ Just ns -> info { namespace = Just (n:ns) }
1565+elabDecl' what info (PClass doc s f cs n ps ds)
15661566 | what /= EDefns
15671567 = do iLOG $ "Elaborating class " ++ show n
15681568 elabClass info (s { syn_params = [] }) doc f cs n ps ds
1569−elabDecl' what info (PInstance s f cs n ps t expn ds)
1569+elabDecl' what info (PInstance s f cs n ps t expn ds)
15701570 | what /= ETypes
15711571 = do iLOG $ "Elaborating instance " ++ show n
15721572 elabInstance info s f cs n ps t expn ds
@@ -1574,27 +1574,27 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
15741574 | what /= ETypes
15751575 = do iLOG $ "Elaborating record " ++ show tyn
15761576 elabRecord info s doc f tyn ty cdoc cn cty
1577− | otherwise
1577+ | otherwise
15781578 = do iLOG $ "Elaborating [type of] " ++ show tyn
15791579 elabData info s doc f False (PLaterdecl tyn ty)
15801580elabDecl' _ info (PDSL n dsl)
15811581 = do i <- getIState
1582− putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1582+ putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
15831583 addIBC (IBCDSL n)
1584−elabDecl' what info (PDirective i)
1584+elabDecl' what info (PDirective i)
15851585 | what /= EDefns = i
15861586elabDecl' what info (PProvider syn fc n tp tm)
15871587 | what /= EDefns
15881588 = do iLOG $ "Elaborating type provider " ++ show n
15891589 elabProvider info syn fc n tp tm
15901590elabDecl' what info (PTransform fc safety old new)
1591− = elabTransform info fc safety old new
1592−elabDecl' _ _ _ = return () -- skipped this time
1591+ = elabTransform info fc safety old new
1592+elabDecl' _ _ _ = return () -- skipped this time
15931593
1594−elabCaseBlock info opts d@(PClauses f o n ps)
1594+elabCaseBlock info opts d@(PClauses f o n ps)
15951595 = do addIBC (IBCDef n)
15961596 logLvl 6 $ "CASE BLOCK: " ++ show (n, d)
1597− elabDecl' EAll info (PClauses f (nub (o ++ opts)) n ps )
1597+ elabDecl' EAll info (PClauses f (nub (o ++ opts)) n ps )
15981598
15991599-- elabDecl' info (PImport i) = loadModule i
16001600
@@ -1608,9 +1608,9 @@ checkInferred fc inf user =
16081608 showImp Nothing True False user
16091609 logLvl 10 $ "Checking match"
16101610 i <- getIState
1611− tclift $ case matchClause' True i user inf of
1611+ tclift $ case matchClause' True i user inf of
16121612 _ -> return ()
1613−-- Left (x, y) -> tfail $ At fc
1613+-- Left (x, y) -> tfail $ At fc
16141614-- (Msg $ "The type-checked term and given term do not match: "
16151615-- ++ show x ++ " and " ++ show y)
16161616 logLvl 10 $ "Checked match"
@@ -1624,7 +1624,7 @@ inferredDiff fc inf user =
16241624 do i <- getIState
16251625 logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
16261626 showImp Nothing True False user
1627− tclift $ case matchClause' True i user inf of
1627+ tclift $ case matchClause' True i user inf of
16281628 Right vs -> return False
16291629 Left (x, y) -> return True
16301630