@@ -31,9 +31,9 @@ import Data.List
31import Data.Maybe
31import Data.Maybe
32import Debug.Trace
32import Debug.Trace
34−recheckC fc env t
34+recheckC fc env t
35 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
35 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
36− ctxt <- getContext
36+ ctxt <- getContext
37 (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of
37 (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of
38 Error e -> tfail (At fc e)
38 Error e -> tfail (At fc e)
39 OK x -> return x
39 OK x -> return x
@@ -47,7 +47,7 @@ checkDef fc ns = do ctxt <- getContext
47-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
47-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
48elabType :: ElabInfo -> SyntaxInfo -> String ->
48elabType :: ElabInfo -> SyntaxInfo -> String ->
49 FC -> FnOpts -> Name -> PTerm -> Idris ()
49 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
51 n = liftname info n_in in -}
51 n = liftname info n_in in -}
52 do checkUndefined fc n
52 do checkUndefined fc n
53 ctxt <- getContext
53 ctxt <- getContext
@@ -59,12 +59,12 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
60 let ty = addImpl i ty'
60 let ty = addImpl i ty'
61 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
61 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
62− ((tyT, defer, is), log) <-
62+ ((tyT, defer, is), log) <-
63 tclift $ elaborate ctxt n (TType (UVal 0)) []
63 tclift $ elaborate ctxt n (TType (UVal 0)) []
64 (errAt "type of " n (erun fc (build i info False n ty)))
64 (errAt "type of " n (erun fc (build i info False n ty)))
65 ds <- checkDef fc defer
65 ds <- checkDef fc defer
66 addDeferred ds
66 addDeferred ds
67− mapM_ (elabCaseBlock info opts) is
67+ mapM_ (elabCaseBlock info opts) is
68 ctxt <- getContext
68 ctxt <- getContext
69 logLvl 5 $ "Rechecking"
69 logLvl 5 $ "Rechecking"
70 logLvl 6 $ show tyT
70 logLvl 6 $ show tyT
@@ -147,7 +147,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
147 i <- getIState
147 i <- getIState
148 t_in <- implicit syn n t_in
148 t_in <- implicit syn n t_in
149 let t = addImpl i t_in
149 let t = addImpl i t_in
150− ((t', defer, is), log) <-
150+ ((t', defer, is), log) <-
151 tclift $ elaborate ctxt n (TType (UVal 0)) []
151 tclift $ elaborate ctxt n (TType (UVal 0)) []
152 (errAt "data declaration " n (erun fc (build i info False n t)))
152 (errAt "data declaration " n (erun fc (build i info False n t)))
153 def' <- checkDef fc defer
153 def' <- checkDef fc defer
@@ -156,11 +156,11 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
156 (cty, _) <- recheckC fc [] t'
156 (cty, _) <- recheckC fc [] t'
157 logLvl 2 $ "---> " ++ show cty
157 logLvl 2 $ "---> " ++ show cty
158 -- temporary, to check cons
158 -- temporary, to check cons
159− when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
159+ when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
160 cons <- mapM (elabCon info syn n codata) dcons
160 cons <- mapM (elabCon info syn n codata) dcons
161 ttag <- getName
161 ttag <- getName
162 i <- getIState
162 i <- getIState
163− let as = map (const Nothing) (getArgTys cty)
163+ let as = map (const Nothing) (getArgTys cty)
164 let params = findParams (map snd cons)
164 let params = findParams (map snd cons)
165 logLvl 2 $ "Parameters : " ++ show params
165 logLvl 2 $ "Parameters : " ++ show params
166 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
166 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)
172 collapseCons n cons
172 collapseCons n cons
173 updateContext (addDatatype (Data n ttag cty cons))
173 updateContext (addDatatype (Data n ttag cty cons))
174 mapM_ (checkPositive n) cons
174 mapM_ (checkPositive n) cons
176 -- parameters are names which are unchanged across the structure,
176 -- parameters are names which are unchanged across the structure,
177 -- which appear exactly once in the return type of a constructor
177 -- which appear exactly once in the return type of a constructor
@@ -184,14 +184,14 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
184 paramPos allapps
184 paramPos allapps
186 paramPos [] = []
186 paramPos [] = []
187− paramPos (args : rest)
187+ paramPos (args : rest)
188 = dropNothing $ keepSame (zip [0..] args) rest
188 = dropNothing $ keepSame (zip [0..] args) rest
190 dropNothing [] = []
190 dropNothing [] = []
191 dropNothing ((x, Nothing) : ts) = dropNothing ts
191 dropNothing ((x, Nothing) : ts) = dropNothing ts
192 dropNothing ((x, _) : ts) = x : dropNothing ts
192 dropNothing ((x, _) : ts) = x : dropNothing ts
194− keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
194+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
195 [(Int, Maybe Name)]
195 [(Int, Maybe Name)]
196 keepSame as [] = as
196 keepSame as [] = as
197 keepSame as (args : rest) = keepSame (update as args) rest
197 keepSame as (args : rest) = keepSame (update as args) rest
@@ -211,14 +211,14 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
211 getDataApp _ = []
211 getDataApp _ = []
213 -- keep the arguments which are single names, which don't appear
213 -- keep the arguments which are single names, which don't appear
214− -- elsewhere
214+ -- elsewhere
216 mParam args [] = []
216 mParam args [] = []
217 mParam args (P Bound n _ : rest)
217 mParam args (P Bound n _ : rest)
218− | count n args == 1
218+ | count n args == 1
219 = Just n : mParam args rest
219 = Just n : mParam args rest
220 where count n [] = 0
220 where count n [] = 0
221− count n (t : ts)
221+ count n (t : ts)
222 | n `elem` freeNames t = 1 + count n ts
222 | n `elem` freeNames t = 1 + count n ts
223 | otherwise = count n ts
223 | otherwise = count n ts
224 mParam args (_ : rest) = Nothing : mParam args rest
224 mParam args (_ : rest) = Nothing : mParam args rest
@@ -253,7 +253,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
253 believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
253 believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
254 (Bind (UN "b") (Pi (TType (UVar (-2))))
254 (Bind (UN "b") (Pi (TType (UVar (-2))))
255 (Bind (UN "x") (Pi (V 1)) (V 1)))
255 (Bind (UN "x") (Pi (V 1)) (V 1)))
256− elabBelieveMe
256+ elabBelieveMe
257 = do let prim__believe_me = (UN "prim__believe_me")
257 = do let prim__believe_me = (UN "prim__believe_me")
258 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
258 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
259 setTotality prim__believe_me (Partial NotCovering)
259 setTotality prim__believe_me (Partial NotCovering)
@@ -279,7 +279,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
279 (Bind (UN "y") (Pi (V 1))
279 (Bind (UN "y") (Pi (V 1))
280 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
280 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
281 [V 3, V 2, V 1, V 0]]))))
281 [V 3, V 2, V 1, V 0]]))))
282− elabSynEq
282+ elabSynEq
283 = do let synEq = UN "prim__syntactic_eq"
283 = do let synEq = UN "prim__syntactic_eq"
285 updateContext (addOperator synEq synEqTy 4 p_synEq)
285 updateContext (addOperator synEq synEqTy 4 p_synEq)
@@ -375,10 +375,10 @@ elabTransform info fc safe lhs_in rhs_in
375 addIBC (IBCTrans (clhs_tm, crhs_tm))
375 addIBC (IBCTrans (clhs_tm, crhs_tm))
378−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
378+elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
379 PTerm -> String -> Name -> PTerm -> Idris ()
379 PTerm -> String -> Name -> PTerm -> Idris ()
380elabRecord info syn doc fc tyn ty cdoc cn cty
380elabRecord 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)])
382 cty' <- implicit syn cn cty
382 cty' <- implicit syn cn cty
383 i <- getIState
383 i <- getIState
384 cty <- case lookupTy cn (tt_ctxt i) of
384 cty <- case lookupTy cn (tt_ctxt i) of
@@ -408,8 +408,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
408 = do i <- getIState
408 = do i <- getIState
409 idrisCatch (do elabDecl' EAll info ty
409 idrisCatch (do elabDecl' EAll info ty
410 elabDecl' EAll info val)
410 elabDecl' EAll info val)
411− (\v -> do iputStrLn $ show fc ++
411+ (\v -> do iputStrLn $ show fc ++
412− ":Warning - can't generate setter for " ++
412+ ":Warning - can't generate setter for " ++
413 show fn ++ " (" ++ show ty ++ ")"
413 show fn ++ " (" ++ show ty ++ ")"
414 putIState i)
414 putIState i)
@@ -459,9 +459,9 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
459 let lhs = PApp fc (PRef fc pn)
459 let lhs = PApp fc (PRef fc pn)
460 [pexp (PApp fc (PRef fc cn) iargs)]
460 [pexp (PApp fc (PRef fc cn) iargs)]
461 let rhs = PRef fc (mkp pn)
461 let rhs = PRef fc (mkp pn)
462− let pclause = PClause fc pn lhs [] rhs []
462+ let pclause = PClause fc pn lhs [] rhs []
463 return [pfnTy, PClauses fc [] pn [pclause]]
463 return [pfnTy, PClauses fc [] pn [pclause]]
465 implicitise (pa, t) = pa { getTm = t }
465 implicitise (pa, t) = pa { getTm = t }
467 mkUpdate recty k num ((pn, pty), pos)
467 mkUpdate recty k num ((pn, pty), pos)
@@ -484,7 +484,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
484 (map pexp rhsArgs)) []
484 (map pexp rhsArgs)) []
485 return (pn, pfnTy, PClauses fc [] setname [pclause])
485 return (pn, pfnTy, PClauses fc [] setname [pclause])
487−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
487+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
488 (String, Name, PTerm, FC) -> Idris (Name, Type)
488 (String, Name, PTerm, FC) -> Idris (Name, Type)
489elabCon info syn tn codata (doc, n, t_in, fc)
489elabCon info syn tn codata (doc, n, t_in, fc)
490 = do checkUndefined fc n
490 = do checkUndefined fc n
@@ -493,7 +493,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
493 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
493 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
494 let t = addImpl i t_in
494 let t = addImpl i t_in
495 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
495 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
496− ((t', defer, is), log) <-
496+ ((t', defer, is), log) <-
497 tclift $ elaborate ctxt n (TType (UVal 0)) []
497 tclift $ elaborate ctxt n (TType (UVal 0)) []
498 (errAt "constructor " n (erun fc (build i info False n t)))
498 (errAt "constructor " n (erun fc (build i info False n t)))
499 logLvl 2 $ "Rechecking " ++ show t'
499 logLvl 2 $ "Rechecking " ++ show t'
@@ -512,8 +512,8 @@ elabCon info syn tn codata (doc, n, t_in, fc)
512 return (n, cty')
512 return (n, cty')
514 tyIs (Bind n b sc) = tyIs sc
514 tyIs (Bind n b sc) = tyIs sc
515− tyIs t | (P _ n' _, _) <- unApply t
515+ tyIs t | (P _ n' _, _) <- unApply t
516− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))
516+ = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))
517 else return ()
517 else return ()
518 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))
518 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))
@@ -523,7 +523,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
523-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
523-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
524-- top-level definition.
524-- top-level definition.
525elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
525elabClauses :: 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
527 do ctxt <- getContext
527 do ctxt <- getContext
528 -- Check n actually exists, with no definition yet
528 -- Check n actually exists, with no definition yet
529 let tys = lookupTy n ctxt
529 let tys = lookupTy n ctxt
@@ -535,7 +535,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
535 -- question: CAFs in where blocks?
535 -- question: CAFs in where blocks?
536 tclift $ tfail $ At fc (NoTypeDecl n)
536 tclift $ tfail $ At fc (NoTypeDecl n)
537 [ty] -> return ty
537 [ty] -> return ty
538− pats_in <- mapM (elabClause info opts)
538+ pats_in <- mapM (elabClause info opts)
539 (zip [0..] cs)
539 (zip [0..] cs)
540 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
540 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
@@ -553,9 +553,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
553 _ -> False
553 _ -> False
554 solveDeferred n
554 solveDeferred n
555 ist <- getIState
555 ist <- getIState
556− when doNothing $
556+ when doNothing $
557 case lookupCtxt n (idris_optimisation ist) of
557 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 })
559 (idris_optimisation ist)
559 (idris_optimisation ist)
560 putIState (ist { idris_optimisation = opts })
560 putIState (ist { idris_optimisation = opts })
561 _ -> do let opts = addDef n (Optimise True False [] [])
561 _ -> 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
563 putIState (ist { idris_optimisation = opts })
563 putIState (ist { idris_optimisation = opts })
564 addIBC (IBCOpt n)
564 addIBC (IBCOpt n)
565 ist <- getIState
565 ist <- getIState
566− let pats = doTransforms ist pats_in
566+ let pats = doTransforms ist pats_in
568− -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
568+ -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
569− -- show l ++ " = " ++
569+ -- show l ++ " = " ++
570 -- show r) pats))
570 -- show r) pats))
571 let tcase = opt_typecase (idris_options ist)
571 let tcase = opt_typecase (idris_options ist)
@@ -583,7 +583,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
583 -- This will get further optimised for run-time, and, separately,
583 -- This will get further optimised for run-time, and, separately,
584 -- further inlined to help with totality checking.
584 -- further inlined to help with totality checking.
585 let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats
585 let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats
587 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef
587 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef
589 -- TODO: Inlining on initial definition happens here.
589 -- 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
601 -- patterns after collapsing optimisation applied
601 -- patterns after collapsing optimisation applied
602 -- (i.e. check if the function should do nothing at run time)
602 -- (i.e. check if the function should do nothing at run time)
603− optpats <- if doNothing
603+ optpats <- if doNothing
604 then return $ [Right (mkApp (P Bound n Erased)
604 then return $ [Right (mkApp (P Bound n Erased)
605 (take numArgs (repeat Erased)), Erased)]
605 (take numArgs (repeat Erased)), Erased)]
606 else stripCollapsed pats
606 else stripCollapsed pats
@@ -610,22 +610,22 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
610 _ -> return ()
610 _ -> return ()
612 let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats
612 let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats
613− tree@(CaseDef scargs sc _) <- tclift $
613+ tree@(CaseDef scargs sc _) <- tclift $
614 simpleCase tcase False reflect CompileTime fc pdef
614 simpleCase tcase False reflect CompileTime fc pdef
615 cov <- coverage
615 cov <- coverage
616 pmissing <-
616 pmissing <-
618 then do missing <- genClauses fc n (map getLHS pdef) cs
618 then do missing <- genClauses fc n (map getLHS pdef) cs
619− -- missing <- genMissing n scargs sc
619+ -- missing <- genMissing n scargs sc
620 missing' <- filterM (checkPossible info fc True n) missing
620 missing' <- filterM (checkPossible info fc True n) missing
621 let clhs = map getLHS pdef
621 let clhs = map getLHS pdef
622− logLvl 2 $ "Must be unreachable:\n" ++
622+ logLvl 2 $ "Must be unreachable:\n" ++
623 showSep "\n" (map (showImp Nothing True False) missing') ++
623 showSep "\n" (map (showImp Nothing True False) missing') ++
624 "\nAgainst: " ++
624 "\nAgainst: " ++
625 showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
625 showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
626 -- filter out anything in missing' which is
626 -- filter out anything in missing' which is
627 -- matched by any of clhs. This might happen since
627 -- 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
629 -- particular form, rather than force a case
629 -- particular form, rather than force a case
630 -- to be impossible.
630 -- to be impossible.
631 return (filter (noMatch ist clhs) missing')
631 return (filter (noMatch ist clhs) missing')
@@ -633,7 +633,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
633 let pcover = null pmissing
633 let pcover = null pmissing
635 -- pdef' is the version that gets compiled for run-time
635 -- pdef' is the version that gets compiled for run-time
636− pdef' <- applyOpts optpdef
636+ pdef' <- applyOpts optpdef
637 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
637 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
639 ist <- getIState
639 ist <- getIState
@@ -641,8 +641,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
641 let tot = if pcover || AssertTotal `elem` opts
641 let tot = if pcover || AssertTotal `elem` opts
642 then Unchecked -- finish checking later
642 then Unchecked -- finish checking later
643 else Partial NotCovering -- already know it's not total
643 else Partial NotCovering -- already know it's not total
644− -- case lookupCtxt (namespace info) n (idris_flags ist) of
644+ -- case lookupCtxt (namespace info) n (idris_flags ist) of
645− -- [fs] -> if TotalFn `elem` fs
645+ -- [fs] -> if TotalFn `elem` fs
646 -- then case tot of
646 -- then case tot of
647 -- Total _ -> return ()
647 -- Total _ -> return ()
648 -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
648 -- 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
652 CaseDef _ _ [] -> return ()
652 CaseDef _ _ [] -> return ()
653 CaseDef _ _ xs -> mapM_ (\x ->
653 CaseDef _ _ xs -> mapM_ (\x ->
654 iputStrLn $ show fc ++
654 iputStrLn $ show fc ++
655− ":warning - Unreachable case: " ++
655+ ":warning - Unreachable case: " ++
656 show (delab ist x)) xs
656 show (delab ist x)) xs
657 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
657 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
@@ -662,12 +662,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
662 logLvl 3 $ "Optimised: " ++ show tree'
662 logLvl 3 $ "Optimised: " ++ show tree'
663 ctxt <- getContext
663 ctxt <- getContext
664 ist <- getIState
664 ist <- getIState
665− putIState (ist { idris_patdefs = addDef n (pdef', pmissing)
665+ putIState (ist { idris_patdefs = addDef n (pdef', pmissing)
666 (idris_patdefs ist) })
666 (idris_patdefs ist) })
667 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
667 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
668 case lookupTy n ctxt of
668 case lookupTy n ctxt of
669 [ty] -> do updateContext (addCasedef n caseInfo
669 [ty] -> do updateContext (addCasedef n caseInfo
670− tcase knowncovering
670+ tcase knowncovering
672 (AssertTotal `elem` opts)
672 (AssertTotal `elem` opts)
@@ -698,14 +698,14 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
699 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True) tm of
699 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True) tm of
700 Right _ -> False
700 Right _ -> False
701− Left miss -> True) cs
701+ Left miss -> True) cs
703 checkUndefined n ctxt = case lookupDef n ctxt of
703 checkUndefined n ctxt = case lookupDef n ctxt of
704 [] -> return ()
704 [] -> return ()
705 [TyDecl _ _] -> return ()
705 [TyDecl _ _] -> return ()
706 _ -> tclift $ tfail (At fc (AlreadyDefined n))
706 _ -> tclift $ tfail (At fc (AlreadyDefined n))
708− debind (Right (x, y)) = let (vs, x') = depat [] x
708+ debind (Right (x, y)) = let (vs, x') = depat [] x
709 (_, y') = depat [] y in
709 (_, y') = depat [] y in
710 (vs, x', y')
710 (vs, x', y')
711 debind (Left x) = let (vs, x') = depat [] x in
711 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
714 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
714 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
715 depat acc x = (acc, x)
715 depat acc x = (acc, x)
717 getLHS (_, l, _) = l
717 getLHS (_, l, _) = l
719− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
719+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
720 simple_lhs ctxt t = t
720 simple_lhs ctxt t = t
722 specNames [] = Nothing
722 specNames [] = Nothing
723 specNames (Specialise ns : _) = Just ns
723 specNames (Specialise ns : _) = Just ns
724 specNames (_ : xs) = specNames xs
724 specNames (_ : xs) = specNames xs
726− sameLength ((_, x, _) : xs)
726+ sameLength ((_, x, _) : xs)
727 = do l <- sameLength xs
727 = do l <- sameLength xs
728 let (f, as) = unApply x
728 let (f, as) = unApply x
729 if (null xs || l == length as) then return (length as)
729 if (null xs || l == length as) then return (length as)
730 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
730 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
731 sameLength [] = return 0
731 sameLength [] = return 0
733− -- apply all transformations (just specialisation for now, add
733+ -- apply all transformations (just specialisation for now, add
734 -- user defined transformation rules later)
734 -- user defined transformation rules later)
735− doTransforms ist pats =
735+ doTransforms ist pats =
736 case specNames opts of
736 case specNames opts of
737 Nothing -> pats
737 Nothing -> pats
738 Just ns -> partial_eval (tt_ctxt ist) ns pats
738 Just ns -> partial_eval (tt_ctxt ist) ns pats
@@ -750,14 +750,14 @@ elabValBind info aspat tm_in
750 -- * ordinary elaboration
750 -- * ordinary elaboration
751 -- * elaboration as a Type
751 -- * elaboration as a Type
752 -- * elaboration as a function a -> b
752 -- * elaboration as a function a -> b
754− ((tm', defer, is), _) <-
754+ ((tm', defer, is), _) <-
755−-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
755+-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
756-- (build i info aspat (MN 0 "val") tm))
756-- (build i info aspat (MN 0 "val") tm))
757 tclift (elaborate ctxt (MN 0 "val") infP []
757 tclift (elaborate ctxt (MN 0 "val") infP []
758 (build i info aspat (MN 0 "val") (infTerm tm)))
758 (build i info aspat (MN 0 "val") (infTerm tm)))
759 let vtm = orderPats (getInferTerm tm')
759 let vtm = orderPats (getInferTerm tm')
760− let bargs = getPBtys vtm
760+ let bargs = getPBtys vtm
762 def' <- checkDef (fileFC "(input)") defer
762 def' <- checkDef (fileFC "(input)") defer
763 addDeferred def'
763 addDeferred def'
@@ -796,7 +796,7 @@ checkPossible info fc tcgen fname lhs_in
796-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
796-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
797 err@(Error _) -> return False
797 err@(Error _) -> return False
799−elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
799+elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
800 Idris (Either Term (Term, Term))
800 Idris (Either Term (Term, Term))
801elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
801elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
802 = do let tcgen = Dictionary `elem` opts
802 = do let tcgen = Dictionary `elem` opts
@@ -805,7 +805,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
805 True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
805 True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
806 False -> do ptm <- mkPatTm lhs_in
806 False -> do ptm <- mkPatTm lhs_in
807 return (Left ptm)
807 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)
809 = do let tcgen = Dictionary `elem` opts
809 = do let tcgen = Dictionary `elem` opts
810 ctxt <- getContext
810 ctxt <- getContext
@@ -818,15 +818,15 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
818 _ -> error "Can't happen (elabClause function type)"
818 _ -> error "Can't happen (elabClause function type)"
819 let fn_is = case lookupCtxt fname (idris_implicits i) of
819 let fn_is = case lookupCtxt fname (idris_implicits i) of
821− _ -> []
821+ _ -> []
822 let params = getParamsInType i [] fn_is fn_ty
822 let params = getParamsInType i [] fn_is fn_ty
823 let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))
823 let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))
824 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
824 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
825 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
825 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
827− ((lhs', dlhs, []), _) <-
827+ ((lhs', dlhs, []), _) <-
828 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
828 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
829− (errAt "left hand side of " fname
829+ (errAt "left hand side of " fname
830 (erun fc (buildTC i info True tcgen fname (infTerm lhs))))
830 (erun fc (buildTC i info True tcgen fname (infTerm lhs))))
831 let lhs_tm = orderPats (getInferTerm lhs')
831 let lhs_tm = orderPats (getInferTerm lhs')
832 let lhs_ty = getInferType lhs'
832 let lhs_ty = getInferType lhs'
@@ -848,7 +848,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
848 let defs = nub (decls ++ concatMap defined whereblock)
848 let defs = nub (decls ++ concatMap defined whereblock)
849 let newargs = pvars ist lhs_tm
849 let newargs = pvars ist lhs_tm
850 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
850 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
852 -- Split the where block into declarations with a type, and those
852 -- Split the where block into declarations with a type, and those
853 -- without
853 -- without
854 -- Elaborate those with a type *before* RHS, those without *after*
854 -- 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)
864 logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
864 logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
865 ctxt <- getContext -- new context with where block added
865 ctxt <- getContext -- new context with where block added
866 logLvl 5 "STARTING CHECK"
866 logLvl 5 "STARTING CHECK"
867− ((rhs', defer, is), _) <-
867+ ((rhs', defer, is), _) <-
868 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
868 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
869 (do pbinds lhs_tm
869 (do pbinds lhs_tm
870− (_, _, is) <- errAt "right hand side of " fname
870+ (_, _, is) <- errAt "right hand side of " fname
871 (erun fc (build i info False fname rhs))
871 (erun fc (build i info False fname rhs))
872− errAt "right hand side of " fname
872+ errAt "right hand side of " fname
873 (erun fc $ psolve lhs_tm)
873 (erun fc $ psolve lhs_tm)
874 tt <- get_term
874 tt <- get_term
875 let (tm, ds) = runState (collectDeferred (Just fname) tt) []
875 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)
897 checkInferred fc (delab' i crhs True) rhs
897 checkInferred fc (delab' i crhs True) rhs
898 return $ Right (clhs, crhs)
898 return $ Right (clhs, crhs)
900− decorate (NS x ns)
900+ decorate (NS x ns)
901− = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
901+ = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
902-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
902-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
903− decorate x
903+ decorate x
904 = SN (WhereN cnum fname x)
904 = SN (WhereN cnum fname x)
905-- = NS (SN (WhereN cnum fname x)) [show cnum]
905-- = NS (SN (WhereN cnum fname x)) [show cnum]
906-- = NS (UN ('#':show x)) [show cnum, show fname]
906-- = 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)
909 sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)
909 sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)
910 = let (bf, af) = sepBlocks' (n : ns) bs in
910 = let (bf, af) = sepBlocks' (n : ns) bs in
911 (d : bf, af)
911 (d : bf, af)
912− sepBlocks' ns (d@(PClauses _ _ n _) : bs)
912+ sepBlocks' ns (d@(PClauses _ _ n _) : bs)
913 | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in
913 | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in
914 (bf, d : af)
914 (bf, d : af)
915 sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
915 sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
916 (b : bf, af)
916 (b : bf, af)
917 sepBlocks' ns [] = ([], [])
917 sepBlocks' ns [] = ([], [])
919− pinfo ns ps i
919+ pinfo ns ps i
920 = let ds = concatMap declared ps
920 = let ds = concatMap declared ps
921 newps = params info ++ ns
921 newps = params info ++ ns
922 dsParams = map (\n -> (n, map fst newps)) ds
922 dsParams = map (\n -> (n, map fst newps)) ds
923− newb = addAlist dsParams (inblock info)
923+ newb = addAlist dsParams (inblock info)
924 l = liftname info in
924 l = liftname info in
925 info { params = newps,
925 info { params = newps,
926 inblock = newb,
926 inblock = newb,
@@ -929,24 +929,24 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
929 -- _ -> MN i (show n)) . l
929 -- _ -> MN i (show n)) . l
932− getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
932+ getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
933 = getParamsInType i env is (instantiate (P Bound n t) sc)
933 = 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)
935 = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)
935 = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)
936 getParamsInType i env is tm@(App f a)
936 getParamsInType i env is tm@(App f a)
937− | (P _ tn _, args) <- unApply tm
937+ | (P _ tn _, args) <- unApply tm
938 = case lookupCtxt tn (idris_datatypes i) of
938 = case lookupCtxt tn (idris_datatypes i) of
939 [t] -> nub $ paramNames args env (param_pos t) ++
939 [t] -> nub $ paramNames args env (param_pos t) ++
940− getParamsInType i env is f ++
940+ getParamsInType i env is f ++
941 getParamsInType i env is a
941 getParamsInType i env is a
942− [] -> nub $ getParamsInType i env is f ++
942+ [] -> nub $ getParamsInType i env is f ++
943 getParamsInType i env is a
943 getParamsInType i env is a
944− | otherwise = nub $ getParamsInType i env is f ++
944+ | otherwise = nub $ getParamsInType i env is f ++
945 getParamsInType i env is a
945 getParamsInType i env is a
946 getParamsInType i _ _ _ = []
946 getParamsInType i _ _ _ = []
948 paramNames args env [] = []
948 paramNames args env [] = []
949− paramNames args env (p : ps)
949+ paramNames args env (p : ps)
950 | length args > p = case args!!p of
950 | length args > p = case args!!p of
951 P _ n _ -> if n `elem` env
951 P _ n _ -> if n `elem` env
952 then n : paramNames args env ps
952 then n : paramNames args env ps
@@ -964,7 +964,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
964 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
964 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
965 propagateParams ps x = x
965 propagateParams ps x = x
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)
968 = do let tcgen = Dictionary `elem` opts
968 = do let tcgen = Dictionary `elem` opts
969 ctxt <- getContext
969 ctxt <- getContext
970 -- Build the LHS as an "Infer", and pull out its type and
970 -- 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)
972 i <- getIState
972 i <- getIState
973 let lhs = addImplPat i lhs_in
973 let lhs = addImplPat i lhs_in
974 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
974 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
975− ((lhs', dlhs, []), _) <-
975+ ((lhs', dlhs, []), _) <-
976 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
976 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
977 (errAt "left hand side of with in " fname
977 (errAt "left hand side of with in " fname
978 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) )
978 (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)
986 let wval = addImplBound i (map fst bargs) wval_in
986 let wval = addImplBound i (map fst bargs) wval_in
987 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
987 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
988 -- Elaborate wval in this context
988 -- Elaborate wval in this context
989− ((wval', defer, is), _) <-
989+ ((wval', defer, is), _) <-
990− tclift $ elaborate ctxt (MN 0 "withRHS")
990+ tclift $ elaborate ctxt (MN 0 "withRHS")
991 (bindTyArgs PVTy bargs infP) []
991 (bindTyArgs PVTy bargs infP) []
992 (do pbinds lhs_tm
992 (do pbinds lhs_tm
993 -- TODO: may want where here - see winfo abpve
993 -- TODO: may want where here - see winfo abpve
994− (_', d, is) <- errAt "with value in " fname
994+ (_', d, is) <- errAt "with value in " fname
995 (erun fc (build i info False fname (infTerm wval)))
995 (erun fc (build i info False fname (infTerm wval)))
996 erun fc $ psolve lhs_tm
996 erun fc $ psolve lhs_tm
997 tt <- get_term
997 tt <- get_term
@@ -1008,18 +1008,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1008 -- rather than a de Bruijn index.
1008 -- rather than a de Bruijn index.
1009 let pdeps = usedNamesIn pvars i (delab i cwvalty)
1009 let pdeps = usedNamesIn pvars i (delab i cwvalty)
1010 let (bargs_pre, bargs_post) = split pdeps bargs []
1010 let (bargs_pre, bargs_post) = split pdeps bargs []
1011− logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
1011+ logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
1012 " depends on " ++ show pdeps ++ " from " ++ show pvars)
1012 " depends on " ++ show pdeps ++ " from " ++ show pvars)
1013 logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
1013 logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
1014 windex <- getName
1014 windex <- getName
1015 -- build a type declaration for the new function:
1015 -- 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
1017 let wargval = getRetTy cwvalN
1017 let wargval = getRetTy cwvalN
1018 let wargtype = getRetTy cwvaltyN
1018 let wargtype = getRetTy cwvaltyN
1019 logLvl 5 ("Abstract over " ++ show wargval)
1019 logLvl 5 ("Abstract over " ++ show wargval)
1020− let wtype = bindTyArgs Pi (bargs_pre ++
1020+ let wtype = bindTyArgs Pi (bargs_pre ++
1021− (MN 0 "warg", wargtype) :
1021+ (MN 0 "warg", wargtype) :
1022− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
1022+ map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
1023 (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
1023 (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
1024 logLvl 3 ("New function type " ++ show wtype)
1024 logLvl 3 ("New function type " ++ show wtype)
1025 let wname = MN windex (show fname)
1025 let wname = MN windex (show fname)
@@ -1041,8 +1041,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1041 mapM_ (elabDecl EAll info) wb
1041 mapM_ (elabDecl EAll info) wb
1043 -- rhs becomes: fname' ps wval
1043 -- rhs becomes: fname' ps wval
1044− let rhs = PApp fc (PRef fc wname)
1044+ let rhs = PApp fc (PRef fc wname)
1045− (map (pexp . (PRef fc) . fst) bargs_pre ++
1045+ (map (pexp . (PRef fc) . fst) bargs_pre ++
1046 pexp wval :
1046 pexp wval :
1047 (map (pexp . (PRef fc) . fst) bargs_post))
1047 (map (pexp . (PRef fc) . fst) bargs_post))
1048 logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)
1048 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)
1074 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
1074 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
1075 = do i <- getIState
1075 = do i <- getIState
1076 let tm = addImplPat i tm_in
1076 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 " ++
1078 showImp Nothing True False toplhs)
1078 showImp Nothing True False toplhs)
1079 case matchClause i toplhs tm of
1079 case matchClause i toplhs tm of
1080 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")
1080 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 ->
1082 do logLvl 3 ("Match vars : " ++ show mvars)
1082 do logLvl 3 ("Match vars : " ++ show mvars)
1083 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1083 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1084 return $ PClause fc wname lhs ws rhs wheres
1084 return $ PClause fc wname lhs ws rhs wheres
1085 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
1085 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
1086 = do i <- getIState
1086 = do i <- getIState
1087 let tm = addImplPat i tm_in
1087 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 " ++
1089 showImp Nothing True False toplhs)
1089 showImp Nothing True False toplhs)
1090 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
1090 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
1091 case matchClause i toplhs tm of
1091 case matchClause i toplhs tm of
1092 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
1092 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 ->
1094 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1094 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'
1096 mkAux wname toplhs ns ns' c
1096 mkAux wname toplhs ns ns' c
1097 = ifail $ show fc ++ "badly formed with clause"
1097 = ifail $ show fc ++ "badly formed with clause"
@@ -1102,11 +1102,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1102 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w
1102 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w
1103 = let ns = map (keepMvar (map fst mvars) fc') ns_in
1103 = let ns = map (keepMvar (map fst mvars) fc') ns_in
1104 ns' = map (keepMvar (map fst mvars) fc') ns_in' in
1104 ns' = map (keepMvar (map fst mvars) fc') ns_in' in
1105− return $ substMatches mvars $
1105+ return $ substMatches mvars $
1106− PApp fc (PRef fc' wname)
1106+ PApp fc (PRef fc' wname)
1107 (map pexp ns ++ pexp w : (map pexp ns'))
1107 (map pexp ns ++ pexp w : (map pexp ns'))
1108− updateLHS n wname mvars ns ns' tm w
1108+ updateLHS n wname mvars ns ns' tm w
1109− = ifail $ "Not implemented match " ++ show tm
1109+ = ifail $ "Not implemented match " ++ show tm
1111 keepMvar mvs fc v | v `elem` mvs = PRef fc v
1111 keepMvar mvs fc v | v `elem` mvs = PRef fc v
1112 | otherwise = Placeholder
1112 | otherwise = Placeholder
@@ -1118,16 +1118,16 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1118 split deps ((n, ty) : rest) pre
1118 split deps ((n, ty) : rest) pre
1119 | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)
1119 | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)
1120 | otherwise = split deps rest ((n, ty) : pre)
1120 | otherwise = split deps rest ((n, ty) : pre)
1121− split deps [] pre = (reverse pre, [])
1121+ split deps [] pre = (reverse pre, [])
1123 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
1123 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
1125data MArgTy = IA | EA | CA deriving Show
1125data MArgTy = IA | EA | CA deriving Show
1127elabClass :: ElabInfo -> SyntaxInfo -> String ->
1127elabClass :: ElabInfo -> SyntaxInfo -> String ->
1128− FC -> [PTerm] ->
1128+ FC -> [PTerm] ->
1129 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1129 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
1131 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1131 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1132 let tty = pibind ps PType
1132 let tty = pibind ps PType
1133 let constraint = PApp fc (PRef fc tn)
1133 let constraint = PApp fc (PRef fc tn)
@@ -1137,20 +1137,20 @@ elabClass info syn doc fc constraints tn ps ds
1137 let mnames = map getMName mdecls
1137 let mnames = map getMName mdecls
1138 logLvl 2 $ "Building methods " ++ show mnames
1138 logLvl 2 $ "Building methods " ++ show mnames
1139 ims <- mapM (tdecl mnames) mdecls
1139 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)
1141 (filter clause ds)
1141 (filter clause ds)
1142− let (methods, imethods)
1142+ let (methods, imethods)
1143 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
1143 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
1144 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
1144 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) [])
1146 -- build instance constructor type
1146 -- build instance constructor type
1147 -- decorate names of functions to ensure they can't be referred
1147 -- decorate names of functions to ensure they can't be referred
1148 -- to elsewhere in the class declaration
1148 -- to elsewhere in the class declaration
1149 -- TODO: Remove mdec to make it a dependent record, which would
1149 -- TODO: Remove mdec to make it a dependent record, which would
1150 -- allow dependent type classes, but building instances will
1150 -- allow dependent type classes, but building instances will
1151 -- then need some attention.
1151 -- then need some attention.
1152− let cty = impbind ps $ conbind constraints
1152+ let cty = impbind ps $ conbind constraints
1153− $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)
1153+ $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)
1154 constraint
1154 constraint
1155 let cons = [("", cn, cty, fc)]
1155 let cons = [("", cn, cty, fc)]
1156 let ddecl = PDatadecl tn tty cons
1156 let ddecl = PDatadecl tn tty cons
@@ -1158,7 +1158,7 @@ elabClass info syn doc fc constraints tn ps ds
1158 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl
1158 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl
1159 -- for each constraint, build a top level function to chase it
1159 -- for each constraint, build a top level function to chase it
1160 logLvl 5 $ "Building functions"
1160 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
1162 ++ using syn }
1162 ++ using syn }
1163 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints
1163 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints
1164 mapM_ (elabDecl EAll info) (concat fns)
1164 mapM_ (elabDecl EAll info) (concat fns)
@@ -1172,19 +1172,19 @@ elabClass info syn doc fc constraints tn ps ds
1173 nodoc (n, (_, o, t)) = (n, (o, t))
1173 nodoc (n, (_, o, t)) = (n, (o, t))
1174 pibind [] x = x
1174 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)
1177 mdec (UN n) = SN (MethodN (UN n))
1177 mdec (UN n) = SN (MethodN (UN n))
1178 mdec (NS x n) = NS (mdec x) n
1178 mdec (NS x n) = NS (mdec x) n
1179 mdec x = x
1179 mdec x = x
1181 impbind [] x = x
1181 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)
1183 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
1183 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
1184 conbind [] x = x
1184 conbind [] x = x
1186 getMName (PTy _ _ _ _ n _) = nsroot n
1186 getMName (PTy _ _ _ _ n _) = nsroot n
1187− tdecl allmeths (PTy doc syn _ o n t)
1187+ tdecl allmeths (PTy doc syn _ o n t)
1188 = do t' <- implicit' syn allmeths n t
1188 = do t' <- implicit' syn allmeths n t
1189 logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
1189 logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
1190 return ( (n, (toExp (map fst ps) Exp t')),
1190 return ( (n, (toExp (map fst ps) Exp t')),
@@ -1192,12 +1192,12 @@ elabClass info syn doc fc constraints tn ps ds
1192 (n, (syn, o, t) ) )
1192 (n, (syn, o, t) ) )
1193 tdecl _ _ = ifail "Not allowed in a class declaration"
1193 tdecl _ _ = ifail "Not allowed in a class declaration"
1195− -- Create default definitions
1195+ -- Create default definitions
1196 defdecl mtys c d@(PClauses fc opts n cs) =
1196 defdecl mtys c d@(PClauses fc opts n cs) =
1197 case lookup n mtys of
1197 case lookup n mtys of
1198 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1198 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1199 let ds = map (decorateid defaultdec)
1199 let ds = map (decorateid defaultdec)
1200− [PTy "" syn fc [] n ty',
1200+ [PTy "" syn fc [] n ty',
1201 PClauses fc (o ++ opts) n cs]
1201 PClauses fc (o ++ opts) n cs]
1202 iLOG (show ds)
1202 iLOG (show ds)
1203 return (n, ((defaultdec n, ds!!1), ds))
1203 return (n, ((defaultdec n, ds!!1), ds))
@@ -1214,7 +1214,7 @@ elabClass info syn doc fc constraints tn ps ds
1215 -- Generate a function for chasing a dictionary constraint
1215 -- Generate a function for chasing a dictionary constraint
1216 cfun cn c syn all con
1216 cfun cn c syn all con
1217− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
1217+ = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
1218 -- SN (ParentN cn (show con))
1218 -- SN (ParentN cn (show con))
1219 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1219 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1220 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
1220 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
1239 -- Generate a top level function which looks up a method in a given
1239 -- Generate a top level function which looks up a method in a given
1240 -- dictionary (this is inlinable, always)
1240 -- 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))
1242 = do let ty' = insertConstraint c ty
1242 = do let ty' = insertConstraint c ty
1243 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1243 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1244 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
1244 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
1260 getMeth (m:ms) (a:as) x | x == a = PRef fc m
1260 getMeth (m:ms) (a:as) x | x == a = PRef fc m
1261 | otherwise = getMeth ms as x
1261 | otherwise = getMeth ms as x
1263− lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns
1263+ lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns
1264− lhsArgs (IA : xs) ns = lhsArgs xs ns
1264+ lhsArgs (IA : xs) ns = lhsArgs xs ns
1265 lhsArgs (CA : xs) ns = lhsArgs xs ns
1265 lhsArgs (CA : xs) ns = lhsArgs xs ns
1266 lhsArgs [] _ = []
1266 lhsArgs [] _ = []
1268− rhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : 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
1269+ rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
1270 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
1270 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
1271 rhsArgs [] _ = []
1271 rhsArgs [] _ = []
@@ -1281,43 +1281,43 @@ elabClass info syn doc fc constraints tn ps ds
1281 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
1281 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
1282 toExp ns e sc = sc
1282 toExp ns e sc = sc
1284−elabInstance :: ElabInfo -> SyntaxInfo ->
1284+elabInstance :: ElabInfo -> SyntaxInfo ->
1285 FC -> [PTerm] -> -- constraints
1285 FC -> [PTerm] -> -- constraints
1286− Name -> -- the class
1286+ Name -> -- the class
1287− [PTerm] -> -- class parameters (i.e. instance)
1287+ [PTerm] -> -- class parameters (i.e. instance)
1288 PTerm -> -- full instance type
1288 PTerm -> -- full instance type
1289 Maybe Name -> -- explicit name
1289 Maybe Name -> -- explicit name
1290 [PDecl] -> Idris ()
1290 [PDecl] -> Idris ()
1291elabInstance info syn fc cs n ps t expn ds
1291elabInstance info syn fc cs n ps t expn ds
1292− = do i <- getIState
1292+ = do i <- getIState
1293 (n, ci) <- case lookupCtxtName n (idris_classes i) of
1293 (n, ci) <- case lookupCtxtName n (idris_classes i) of
1294 [c] -> return c
1294 [c] -> return c
1295 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1295 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1296 let constraint = PApp fc (PRef fc n) (map pexp ps)
1296 let constraint = PApp fc (PRef fc n) (map pexp ps)
1297 let iname = case expn of
1297 let iname = case expn of
1298− Nothing -> SN (InstanceN n (map show ps))
1298+ Nothing -> SN (InstanceN n (map show ps))
1299 -- UN ('@':show n ++ "$" ++ show ps)
1299 -- UN ('@':show n ++ "$" ++ show ps)
1300 Just nm -> nm
1300 Just nm -> nm
1301 -- if the instance type matches any of the instances we have already,
1301 -- if the instance type matches any of the instances we have already,
1302 -- and it's not a named instance, then it's overlapping, so report an error
1302 -- and it's not a named instance, then it's overlapping, so report an error
1303 case expn of
1303 case expn of
1304− Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)
1304+ Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)
1305 addInstance intInst n iname
1305 addInstance intInst n iname
1306− Just _ -> addInstance intInst n iname
1306+ Just _ -> addInstance intInst n iname
1307 elabType info syn "" fc [] iname t
1307 elabType info syn "" fc [] iname t
1308 let ips = zip (class_params ci) ps
1308 let ips = zip (class_params ci) ps
1309 let ns = case n of
1309 let ns = case n of
1310 NS n ns' -> ns'
1310 NS n ns' -> ns'
1312− -- get the implicit parameters that need passing through to the
1312+ -- get the implicit parameters that need passing through to the
1313 -- where block
1313 -- where block
1314 wparams <- mapM (\p -> case p of
1314 wparams <- mapM (\p -> case p of
1315 PApp _ _ args -> getWParams args
1315 PApp _ _ args -> getWParams args
1316 _ -> return []) ps
1316 _ -> return []) ps
1317 let pnames = map pname (concat (nub wparams))
1317 let pnames = map pname (concat (nub wparams))
1318− let mtys = map (\ (n, (op, t)) ->
1318+ let mtys = map (\ (n, (op, t)) ->
1319 let t' = substMatchesShadow ips pnames t in
1319 let t' = substMatchesShadow ips pnames t in
1320− (decorate ns iname n,
1320+ (decorate ns iname n,
1321 op, coninsert cs t', t'))
1321 op, coninsert cs t', t'))
1322 (class_methods ci)
1322 (class_methods ci)
1323 logLvl 3 (show (mtys, ips))
1323 logLvl 3 (show (mtys, ips))
@@ -1329,12 +1329,12 @@ elabInstance info syn fc cs n ps t expn ds
1329 let wbVals = map (decorateid (decorate ns iname)) ds'
1329 let wbVals = map (decorateid (decorate ns iname)) ds'
1330 let wb = wbTys ++ wbVals
1330 let wb = wbTys ++ wbVals
1331 logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)
1331 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 " ++
1333 show (concat (nub wparams))
1333 show (concat (nub wparams))
1334 let lhs = PRef fc iname
1334 let lhs = PRef fc iname
1335 let rhs = PApp fc (PRef fc (instanceName ci))
1335 let rhs = PApp fc (PRef fc (instanceName ci))
1336 (map (pexp . mkMethApp) mtys)
1336 (map (pexp . mkMethApp) mtys)
1337− let idecls = [PClauses fc [Dictionary] iname
1337+ let idecls = [PClauses fc [Dictionary] iname
1338 [PClause fc iname lhs [] rhs wb]]
1338 [PClause fc iname lhs [] rhs wb]]
1339 iLOG (show idecls)
1339 iLOG (show idecls)
1340 mapM (elabDecl EAll info) idecls
1340 mapM (elabDecl EAll info) idecls
@@ -1360,23 +1360,23 @@ elabInstance info syn fc cs n ps t expn ds
1360 Right _ -> overlapping tret tret'
1360 Right _ -> overlapping tret tret'
1361 Left _ -> return ()
1361 Left _ -> return ()
1362 _ -> return ()
1362 _ -> return ()
1363− overlapping t t' = tclift $ tfail (At fc (Msg $
1363+ overlapping t t' = tclift $ tfail (At fc (Msg $
1364 "Overlapping instance: " ++ show t' ++ " already defined"))
1364 "Overlapping instance: " ++ show t' ++ " already defined"))
1365 getRetType (PPi _ _ _ sc) = getRetType sc
1365 getRetType (PPi _ _ _ sc) = getRetType sc
1366 getRetType t = t
1366 getRetType t = t
1368− mkMethApp (n, _, _, ty)
1368+ mkMethApp (n, _, _, ty)
1369 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
1369 = 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'
1371 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1371 = 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'
1373 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1373 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1374 lamBind i _ sc = sc
1374 lamBind i _ sc = sc
1375− methArgs i (PPi (Imp _ _ _ _) n ty sc)
1375+ methArgs i (PPi (Imp _ _ _ _) n ty sc)
1376 = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
1376 = 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)
1378 = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
1378 = 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)
1380 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
1380 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
1381 methArgs i _ = []
1381 methArgs i _ = []
@@ -1384,8 +1384,8 @@ elabInstance info syn fc cs n ps t expn ds
1384 papp fc f as = PApp fc f as
1384 papp fc f as = PApp fc f as
1386 getWParams [] = return []
1386 getWParams [] = return []
1387− getWParams (p : ps)
1387+ getWParams (p : ps)
1388− | PRef _ n <- getTm p
1388+ | PRef _ n <- getTm p
1389 = do ps' <- getWParams ps
1389 = do ps' <- getWParams ps
1390 ctxt <- getContext
1390 ctxt <- getContext
1391 case lookupP n ctxt of
1391 case lookupP n ctxt of
@@ -1405,16 +1405,16 @@ elabInstance info syn fc cs n ps t expn ds
1405 coninsert cs sc = conbind cs sc
1405 coninsert cs sc = conbind cs sc
1407 insertDefaults :: IState -> Name ->
1407 insertDefaults :: IState -> Name ->
1408− [(Name, (Name, PDecl))] -> [String] ->
1408+ [(Name, (Name, PDecl))] -> [String] ->
1409 [PDecl] -> [PDecl]
1409 [PDecl] -> [PDecl]
1410 insertDefaults i iname [] ns ds = ds
1410 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
1412 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
1412 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
1414 insertDef i meth def clauses ns iname decls
1414 insertDef i meth def clauses ns iname decls
1415 | null $ filter (clauseFor meth iname ns) decls
1415 | null $ filter (clauseFor meth iname ns) decls
1416 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
1416 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
1417− -- trace (show newd) $
1417+ -- trace (show newd) $
1418 decls ++ [newd]
1418 decls ++ [newd]
1419 | otherwise = decls
1419 | otherwise = decls
@@ -1425,12 +1425,12 @@ elabInstance info syn fc cs n ps t expn ds
1426 checkInClass ns meth
1426 checkInClass ns meth
1427 | not (null (filter (eqRoot meth) ns)) = return ()
1427 | not (null (filter (eqRoot meth) ns)) = return ()
1428− | otherwise = tclift $ tfail (At fc (Msg $
1428+ | otherwise = tclift $ tfail (At fc (Msg $
1429 show meth ++ " not a method of class " ++ show n))
1429 show meth ++ " not a method of class " ++ show n))
1431 eqRoot x y = nsroot x == nsroot y
1431 eqRoot x y = nsroot x == nsroot y
1433− clauseFor m iname ns (PClauses _ _ m' _)
1433+ clauseFor m iname ns (PClauses _ _ m' _)
1434 = decorate ns iname m == decorate ns iname m'
1434 = decorate ns iname m == decorate ns iname m'
1435 clauseFor m iname ns _ = False
1435 clauseFor m iname ns _ = False
@@ -1460,17 +1460,17 @@ elabInstance info syn fc cs n ps t expn ds
1462decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t
1462decorateid 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)
1464 = PClauses f o (decorate n) (map dc cs)
1464 = PClauses f o (decorate n) (map dc cs)
1465 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds
1465 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)
1466+ dc (PWith fc n t as w ds)
1467− = PWith fc (decorate n) (dappname t) as w
1467+ = PWith fc (decorate n) (dappname t) as w
1468 (map (decorateid decorate) ds)
1468 (map (decorateid decorate) ds)
1469 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
1469 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
1470 dappname t = t
1470 dappname t = t
1473−pbinds (Bind n (PVar t) sc) = do attack; patbind n
1473+pbinds (Bind n (PVar t) sc) = do attack; patbind n
1474 pbinds sc
1474 pbinds sc
1475pbinds tm = return ()
1475pbinds tm = return ()
@@ -1495,8 +1495,8 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds
1495-- mapM_ (elabDecl EDefns info) ds
1495-- mapM_ (elabDecl EDefns info) ds
1497elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
1497elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
1498−elabDecl what info d
1498+elabDecl what info d
1499− = idrisCatch (elabDecl' what info d)
1499+ = idrisCatch (elabDecl' what info d)
1500 (\e -> do setErrLine (getErrLine e)
1500 (\e -> do setErrLine (getErrLine e)
1501 ist <- getIState
1501 ist <- getIState
1502 let h = idris_outh ist
1502 let h = idris_outh ist
@@ -1504,24 +1504,24 @@ elabDecl what info d
1505elabDecl' _ info (PFix _ _ _)
1505elabDecl' _ info (PFix _ _ _)
1506 = return () -- nothing to elaborate
1506 = return () -- nothing to elaborate
1507−elabDecl' _ info (PSyntax _ p)
1507+elabDecl' _ info (PSyntax _ p)
1508 = return () -- nothing to elaborate
1508 = 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)
1510 | what /= EDefns
1510 | what /= EDefns
1511 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
1511 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
1512 elabType info s doc f o n ty
1512 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)
1514 | what /= EDefns
1514 | what /= EDefns
1515 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
1515 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
1516 elabPostulate info s doc f o n ty
1516 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)
1518 | what /= ETypes
1518 | what /= ETypes
1519 = do iLOG $ "Elaborating " ++ show (d_name d)
1519 = do iLOG $ "Elaborating " ++ show (d_name d)
1520 elabData info s doc f co d
1520 elabData info s doc f co d
1521− | otherwise
1521+ | otherwise
1522 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)
1522 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)
1523 elabData info s doc f co (PLaterdecl (d_name d) (d_tcon d))
1523 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)
1525 | what /= ETypes
1525 | what /= ETypes
1526 = do iLOG $ "Elaborating clause " ++ show n
1526 = do iLOG $ "Elaborating clause " ++ show n
1527 i <- getIState -- get the type options too
1527 i <- getIState -- get the type options too
@@ -1529,7 +1529,7 @@ elabDecl' what info d@(PClauses f o n ps)
1529 [fs] -> fs
1529 [fs] -> fs
1530 [] -> []
1530 [] -> []
1531 elabClauses info f (o ++ o') n ps
1531 elabClauses info f (o ++ o') n ps
1532−elabDecl' what info (PMutual f ps)
1532+elabDecl' what info (PMutual f ps)
1533 = do mapM_ (elabDecl ETypes info) ps
1533 = do mapM_ (elabDecl ETypes info) ps
1534 mapM_ (elabDecl EDefns info) ps
1534 mapM_ (elabDecl EDefns info) ps
1535 -- Do totality checking after entire mutual block
1535 -- Do totality checking after entire mutual block
@@ -1541,32 +1541,32 @@ elabDecl' what info (PMutual f ps)
1541 mapM_ checkDeclTotality (idris_totcheck i)
1541 mapM_ checkDeclTotality (idris_totcheck i)
1542 clear_totcheck
1542 clear_totcheck
1544−elabDecl' what info (PParams f ns ps)
1544+elabDecl' what info (PParams f ns ps)
1545 = do i <- getIState
1545 = do i <- getIState
1546 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
1546 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
1547 show (concatMap tldeclared ps)
1547 show (concatMap tldeclared ps)
1548 let nblock = pblock i
1548 let nblock = pblock i
1549− mapM_ (elabDecl' what info) nblock
1549+ mapM_ (elabDecl' what info) nblock
1551 pinfo = let ds = concatMap tldeclared ps
1551 pinfo = let ds = concatMap tldeclared ps
1552 newps = params info ++ ns
1552 newps = params info ++ ns
1553 dsParams = map (\n -> (n, map fst newps)) ds
1553 dsParams = map (\n -> (n, map fst newps)) ds
1554− newb = addAlist dsParams (inblock info) in
1554+ newb = addAlist dsParams (inblock info) in
1555 info { params = newps,
1555 info { params = newps,
1556 inblock = newb }
1556 inblock = newb }
1557− pblock i = map (expandParamsD False i id ns
1557+ pblock i = map (expandParamsD False i id ns
1558 (concatMap tldeclared ps)) ps
1558 (concatMap tldeclared ps)) ps
1560elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
1560elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
1562 ninfo = case namespace info of
1562 ninfo = case namespace info of
1563 Nothing -> info { namespace = Just [n] }
1563 Nothing -> info { namespace = Just [n] }
1564− Just ns -> info { namespace = Just (n:ns) }
1564+ Just ns -> info { namespace = Just (n:ns) }
1565−elabDecl' what info (PClass doc s f cs n ps ds)
1565+elabDecl' what info (PClass doc s f cs n ps ds)
1566 | what /= EDefns
1566 | what /= EDefns
1567 = do iLOG $ "Elaborating class " ++ show n
1567 = do iLOG $ "Elaborating class " ++ show n
1568 elabClass info (s { syn_params = [] }) doc f cs n ps ds
1568 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)
1570 | what /= ETypes
1570 | what /= ETypes
1571 = do iLOG $ "Elaborating instance " ++ show n
1571 = do iLOG $ "Elaborating instance " ++ show n
1572 elabInstance info s f cs n ps t expn ds
1572 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)
1574 | what /= ETypes
1574 | what /= ETypes
1575 = do iLOG $ "Elaborating record " ++ show tyn
1575 = do iLOG $ "Elaborating record " ++ show tyn
1576 elabRecord info s doc f tyn ty cdoc cn cty
1576 elabRecord info s doc f tyn ty cdoc cn cty
1577− | otherwise
1577+ | otherwise
1578 = do iLOG $ "Elaborating [type of] " ++ show tyn
1578 = do iLOG $ "Elaborating [type of] " ++ show tyn
1579 elabData info s doc f False (PLaterdecl tyn ty)
1579 elabData info s doc f False (PLaterdecl tyn ty)
1580elabDecl' _ info (PDSL n dsl)
1580elabDecl' _ info (PDSL n dsl)
1581 = do i <- getIState
1581 = 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) })
1583 addIBC (IBCDSL n)
1583 addIBC (IBCDSL n)
1584−elabDecl' what info (PDirective i)
1584+elabDecl' what info (PDirective i)
1585 | what /= EDefns = i
1585 | what /= EDefns = i
1586elabDecl' what info (PProvider syn fc n tp tm)
1586elabDecl' what info (PProvider syn fc n tp tm)
1587 | what /= EDefns
1587 | what /= EDefns
1588 = do iLOG $ "Elaborating type provider " ++ show n
1588 = do iLOG $ "Elaborating type provider " ++ show n
1589 elabProvider info syn fc n tp tm
1589 elabProvider info syn fc n tp tm
1590elabDecl' what info (PTransform fc safety old new)
1590elabDecl' what info (PTransform fc safety old new)
1591− = elabTransform info fc safety old new
1591+ = elabTransform info fc safety old new
1592−elabDecl' _ _ _ = return () -- skipped this time
1592+elabDecl' _ _ _ = return () -- skipped this time
1594−elabCaseBlock info opts d@(PClauses f o n ps)
1594+elabCaseBlock info opts d@(PClauses f o n ps)
1595 = do addIBC (IBCDef n)
1595 = do addIBC (IBCDef n)
1596 logLvl 6 $ "CASE BLOCK: " ++ show (n, d)
1596 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 )
1599-- elabDecl' info (PImport i) = loadModule i
1599-- elabDecl' info (PImport i) = loadModule i
@@ -1608,9 +1608,9 @@ checkInferred fc inf user =
1608 showImp Nothing True False user
1608 showImp Nothing True False user
1609 logLvl 10 $ "Checking match"
1609 logLvl 10 $ "Checking match"
1610 i <- getIState
1610 i <- getIState
1611− tclift $ case matchClause' True i user inf of
1611+ tclift $ case matchClause' True i user inf of
1612 _ -> return ()
1612 _ -> return ()
1613−-- Left (x, y) -> tfail $ At fc
1613+-- Left (x, y) -> tfail $ At fc
1614-- (Msg $ "The type-checked term and given term do not match: "
1614-- (Msg $ "The type-checked term and given term do not match: "
1615-- ++ show x ++ " and " ++ show y)
1615-- ++ show x ++ " and " ++ show y)
1616 logLvl 10 $ "Checked match"
1616 logLvl 10 $ "Checked match"
@@ -1624,7 +1624,7 @@ inferredDiff fc inf user =
1624 do i <- getIState
1624 do i <- getIState
1625 logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
1625 logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
1626 showImp Nothing True False user
1626 showImp Nothing True False user
1627− tclift $ case matchClause' True i user inf of
1627+ tclift $ case matchClause' True i user inf of
1628 Right vs -> return False
1628 Right vs -> return False
1629 Left (x, y) -> return True
1629 Left (x, y) -> return True