@@ -28,12 +28,13 @@ import Idris.Core.CaseTree
29import Control.DeepSeq
29import Control.DeepSeq
30import Control.Monad
30import Control.Monad
31−import Control.Monad.State
31+import Control.Monad.State.Strict as State
32import Data.List
32import Data.List
33import Data.Maybe
33import Data.Maybe
34import Debug.Trace
34import Debug.Trace
36import qualified Data.Map as Map
36import qualified Data.Map as Map
37+import qualified Data.Text as T
37import Data.Char(isLetter, toLower)
38import Data.Char(isLetter, toLower)
38import Data.List.Split (splitOn)
39import Data.List.Split (splitOn)
@@ -91,8 +92,10 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
91 let nty' = normalise ctxt [] nty
92 let nty' = normalise ctxt [] nty
93 -- Add normalised type to internals
94 -- Add normalised type to internals
94− addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))
97+ addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))
95− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))
98+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))
97 let (t, _) = unApply (getRetTy nty')
100 let (t, _) = unApply (getRetTy nty')
98 let corec = case t of
101 let corec = case t of
@@ -112,6 +115,19 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
112 addIBC (IBCFlags n opts')
115 addIBC (IBCFlags n opts')
113 when (Implicit `elem` opts) $ do addCoercion n
116 when (Implicit `elem` opts) $ do addCoercion n
114 addIBC (IBCCoercion n)
117 addIBC (IBCCoercion n)
118+ -- If the function is declared as an error handler and the language
119+ -- extension is enabled, then add it to the list of error handlers.
120+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
121+ when (ErrorHandler `elem` opts) $ do
124+ -- TODO: Check that the declared type is the correct type for an error handler:
125+ -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
127+ then do i <- getIState
128+ putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
129+ else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
130+ else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
115 when corec $ do setAccessibility n Frozen
131 when corec $ do setAccessibility n Frozen
116 addIBC (IBCAccess n Frozen)
132 addIBC (IBCAccess n Frozen)
117 return usety
133 return usety
@@ -124,6 +140,22 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
124 | otherwise = mergeTy sc sc'
140 | otherwise = mergeTy sc sc'
125 mergeTy _ sc = sc
141 mergeTy _ sc = sc
146+ errrep = txt "ErrorReportPart"
148+ tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
149+ (App (P _ (NS (UN m) ns2) _)
150+ (App (P _ (NS (UN l) ns3) _)
151+ (P _ (NS (UN r) ns4) _))))
152+ | e == err && m == maybe && l == lst && r == errrep
153+ , ns1 == map txt ["Errors","Reflection","Language"]
154+ , ns2 == map txt ["Maybe", "Prelude"]
155+ , ns3 == map txt ["List", "Prelude"]
156+ , ns4 == map txt ["Errors","Reflection","Language"] = True
157+ tyIsHandler _ = False
128elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
160elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
129 FC -> FnOpts -> Name -> PTerm -> Idris ()
161 FC -> FnOpts -> Name -> PTerm -> Idris ()
@@ -272,7 +304,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
272type EliminatorState = StateT (Map.Map String Int) Idris
304type EliminatorState = StateT (Map.Map String Int) Idris
274-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
306-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
275−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()
307+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->
308+ ElabInfo -> EliminatorState ()
276elabEliminator paramPos n ty cons info = do
309elabEliminator paramPos n ty cons info = do
277 elimLog $ "Elaborating eliminator"
310 elimLog $ "Elaborating eliminator"
278 let (cnstrs, _) = splitPi ty
311 let (cnstrs, _) = splitPi ty
@@ -280,7 +313,7 @@ elabEliminator paramPos n ty cons info = do
280 generalParams <- namePis False pms
313 generalParams <- namePis False pms
281 motiveIdxs <- namePis False idxs
314 motiveIdxs <- namePis False idxs
282 let motive = mkMotive n paramPos generalParams motiveIdxs
315 let motive = mkMotive n paramPos generalParams motiveIdxs
283− consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
316+ consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do
284 name <- freshName $ "elim_" ++ simpleName cnm
317 name <- freshName $ "elim_" ++ simpleName cnm
285 consTerm <- extractConsTerm c generalParams
318 consTerm <- extractConsTerm c generalParams
286 return (name, expl, consTerm)) cons
319 return (name, expl, consTerm)) cons
@@ -296,13 +329,13 @@ elabEliminator paramPos n ty cons info = do
296 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
329 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
297 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
330 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
298 elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
331 elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
299− Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
332+ State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
300 -- Do not elaborate clauses if there aren't any
333 -- Do not elaborate clauses if there aren't any
301 case eliminatorClauses of
334 case eliminatorClauses of
302 [] -> return ()
335 [] -> return ()
303− _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
336+ _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
304 where elimLog :: String -> EliminatorState ()
337 where elimLog :: String -> EliminatorState ()
305− elimLog s = Control.Monad.State.lift (logLvl 2 s)
338+ elimLog s = State.lift (logLvl 2 s)
307 elimFC :: FC
340 elimFC :: FC
308 elimFC = fileFC "(eliminator)"
341 elimFC = fileFC "(eliminator)"
@@ -312,7 +345,7 @@ elabEliminator paramPos n ty cons info = do
313 applyNS :: Name -> [String] -> Name
346 applyNS :: Name -> [String] -> Name
314 applyNS n [] = n
347 applyNS n [] = n
315− applyNS n ns = NS n ns
348+ applyNS n ns = sNS n ns
317 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
350 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
318 splitPi = splitPi' []
351 splitPi = splitPi' []
@@ -351,11 +384,11 @@ elabEliminator paramPos n ty cons info = do
352 simpleName :: Name -> String
385 simpleName :: Name -> String
353 simpleName (NS n _) = simpleName n
386 simpleName (NS n _) = simpleName n
354− simpleName (MN i n) = n ++ show i
387+ simpleName (MN i n) = str n ++ show i
355 simpleName n = show n
388 simpleName n = show n
357 nameSpaces :: Name -> [String]
390 nameSpaces :: Name -> [String]
358− nameSpaces (NS _ ns) = ns
391+ nameSpaces (NS _ ns) = map str ns
359 nameSpaces _ = []
392 nameSpaces _ = []
361 freshName :: String -> EliminatorState Name
394 freshName :: String -> EliminatorState Name
@@ -364,16 +397,16 @@ elabEliminator paramPos n ty cons info = do
364 let i = fromMaybe 0 (Map.lookup key nameMap)
397 let i = fromMaybe 0 (Map.lookup key nameMap)
365 let name = key ++ show i
398 let name = key ++ show i
366 put $ Map.insert key (i+1) nameMap
399 put $ Map.insert key (i+1) nameMap
367− return (UN name)
400+ return (sUN name)
369 scrutineeName :: Name
402 scrutineeName :: Name
370− scrutineeName = UN "scrutinee"
403+ scrutineeName = sUN "scrutinee"
372 scrutineeArgName :: Name
405 scrutineeArgName :: Name
373− scrutineeArgName = UN "scrutineeArg"
406+ scrutineeArgName = sUN "scrutineeArg"
375 motiveName :: Name
408 motiveName :: Name
376− motiveName = UN "prop"
409+ motiveName = sUN "prop"
378 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
411 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
379 mkMotive n paramPos params indicies =
412 mkMotive n paramPos params indicies =
@@ -437,9 +470,9 @@ elabEliminator paramPos n ty cons info = do
437 splitArgPms _ = ([],[])
470 splitArgPms _ = ([],[])
440− implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
473+ implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
441− implicitIndexes (cns@(doc, cnm, ty, fc)) = do
474+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
442− i <- Control.Monad.State.lift getIState
475+ i <- State.lift getIState
443 implargs' <- case lookupCtxt cnm (idris_implicits i) of
476 implargs' <- case lookupCtxt cnm (idris_implicits i) of
444 [] -> do fail $ "Error while showing implicits for " ++ show cnm
477 [] -> do fail $ "Error while showing implicits for " ++ show cnm
445 [args] -> do return args
478 [args] -> do return args
@@ -452,18 +485,18 @@ elabEliminator paramPos n ty cons info = do
452 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
485 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
453 _ -> return implargs
486 _ -> return implargs
455− extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
488+ extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
456− extractConsTerm (doc, cnm, ty, fc) generalParameters = do
489+ extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do
457 let cons' = replaceParams paramPos generalParameters ty
490 let cons' = replaceParams paramPos generalParameters ty
458 let (args, resTy) = splitPi cons'
491 let (args, resTy) = splitPi cons'
459− implidxs <- implicitIndexes (doc, cnm, ty, fc)
492+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
460 consArgs <- namePis True args
493 consArgs <- namePis True args
461 let recArgs = findRecArgs consArgs
494 let recArgs = findRecArgs consArgs
462 let recMotives = map applyRecMotive recArgs
495 let recMotives = map applyRecMotive recArgs
463 let (_, consIdxs) = splitArgPms resTy
496 let (_, consIdxs) = splitArgPms resTy
464 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
497 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
465 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
498 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
466− applyRecMotive (n,_,ty) = (UN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
499+ applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
467 where (_, idxs) = splitArgPms ty
500 where (_, idxs) = splitArgPms ty
469 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
502 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
@@ -488,12 +521,12 @@ elabEliminator paramPos n ty cons info = do
488 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
521 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
489 convertImplPi _ = Nothing
522 convertImplPi _ = Nothing
491− generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
524+ generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
492− generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
525+ generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
493 let cons' = replaceParams paramPos generalParameters ty
526 let cons' = replaceParams paramPos generalParameters ty
494 let (args, resTy) = splitPi cons'
527 let (args, resTy) = splitPi cons'
495− i <- Control.Monad.State.lift getIState
528+ i <- State.lift getIState
496− implidxs <- implicitIndexes (doc, cnm, ty, fc)
529+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
497 let (_, generalIdxs') = splitArgPms resTy
530 let (_, generalIdxs') = splitArgPms resTy
498 let generalIdxs = map pexp generalIdxs'
531 let generalIdxs = map pexp generalIdxs'
499 consArgs <- namePis True args
532 consArgs <- namePis True args
@@ -514,7 +547,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
515 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
548 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
516 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
549 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
517− addNameHint eqTy (UN "prf")
550+ addNameHint eqTy (sUN "prf")
518 elabDecl EAll toplevel elimDecl
551 elabDecl EAll toplevel elimDecl
519 mapM_ elabPrim primitives
552 mapM_ elabPrim primitives
520 -- Special case prim__believe_me because it doesn't work on just constants
553 -- Special case prim__believe_me because it doesn't work on just constants
@@ -537,11 +570,11 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
538 p_believeMe [_,_,x] = Just x
571 p_believeMe [_,_,x] = Just x
539 p_believeMe _ = Nothing
572 p_believeMe _ = Nothing
540− believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
573+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))
541− (Bind (UN "b") (Pi (TType (UVar (-2))))
574+ (Bind (sUN "b") (Pi (TType (UVar (-2))))
542− (Bind (UN "x") (Pi (V 1)) (V 1)))
575+ (Bind (sUN "x") (Pi (V 1)) (V 1)))
543 elabBelieveMe
576 elabBelieveMe
544− = do let prim__believe_me = (UN "prim__believe_me")
577+ = do let prim__believe_me = sUN "prim__believe_me"
545 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
578 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
546 setTotality prim__believe_me (Partial NotCovering)
579 setTotality prim__believe_me (Partial NotCovering)
547 i <- getIState
580 i <- getIState
@@ -555,19 +588,19 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
555 | otherwise = Just (VApp vnNothing VErased)
588 | otherwise = Just (VApp vnNothing VErased)
556 p_synEq args = Nothing
589 p_synEq args = Nothing
558− nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased
591+ nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased
559− vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased
592+ vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased
560− vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased
593+ vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased
561 vnRefl = VP (DCon 0 2) eqCon VErased
594 vnRefl = VP (DCon 0 2) eqCon VErased
563− synEqTy = Bind (UN "a") (Pi (TType (UVar (-3))))
596+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))
564− (Bind (UN "b") (Pi (TType (UVar (-3))))
597+ (Bind (sUN "b") (Pi (TType (UVar (-3))))
565− (Bind (UN "x") (Pi (V 1))
598+ (Bind (sUN "x") (Pi (V 1))
566− (Bind (UN "y") (Pi (V 1))
599+ (Bind (sUN "y") (Pi (V 1))
567 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
600 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
568 [V 3, V 2, V 1, V 0]]))))
601 [V 3, V 2, V 1, V 0]]))))
569 elabSynEq
602 elabSynEq
570− = do let synEq = UN "prim__syntactic_eq"
603+ = do let synEq = sUN "prim__syntactic_eq"
572 updateContext (addOperator synEq synEqTy 4 p_synEq)
605 updateContext (addOperator synEq synEqTy 4 p_synEq)
573 setTotality synEq (Total [])
606 setTotality synEq (Total [])
@@ -605,7 +638,7 @@ elabProvider info syn fc n ty tm
605 -- Execute the type provider and normalise the result
638 -- Execute the type provider and normalise the result
606 -- use 'run__provider' to convert to a primitive IO action
639 -- use 'run__provider' to convert to a primitive IO action
608− rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)
641+ rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
609 [Erased, e])
642 [Erased, e])
610 let rhs' = normalise ctxt [] rhs
643 let rhs' = normalise ctxt [] rhs
611 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
644 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
@@ -623,9 +656,10 @@ elabProvider info syn fc n ty tm
624 isProviderOf :: TT Name -> TT Name -> Bool
657 isProviderOf :: TT Name -> TT Name -> Bool
625 isProviderOf tp prov
658 isProviderOf tp prov
626− | (P _ (UN "IO") _, [prov']) <- unApply prov
659+ | (P _ (UN io) _, [prov']) <- unApply prov
660+ , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'
661+ , tp == tp', io == txt "IO"
627− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
662+ , prov == txt "Provider" && provs == txt "Providers" = True
629 isProviderOf _ _ = False
663 isProviderOf _ _ = False
631-- | Elaborate a type provider
665-- | Elaborate a type provider
@@ -635,8 +669,8 @@ elabTransform info fc safe lhs_in rhs_in
635 i <- getIState
669 i <- getIState
636 let lhs = addImplPat i lhs_in
670 let lhs = addImplPat i lhs_in
637 ((lhs', dlhs, []), _) <-
671 ((lhs', dlhs, []), _) <-
638− tclift $ elaborate ctxt (MN 0 "transLHS") infP []
672+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []
639− (erun fc (buildTC i info True [] (UN "transform")
673+ (erun fc (buildTC i info True [] (sUN "transform")
640 (infTerm lhs)))
674 (infTerm lhs)))
641 let lhs_tm = orderPats (getInferTerm lhs')
675 let lhs_tm = orderPats (getInferTerm lhs')
642 let lhs_ty = getInferType lhs'
676 let lhs_ty = getInferType lhs'
@@ -646,13 +680,13 @@ elabTransform info fc safe lhs_in rhs_in
646 logLvl 3 ("Transform LHS " ++ show clhs_tm)
680 logLvl 3 ("Transform LHS " ++ show clhs_tm)
647 let rhs = addImplBound i (map fst newargs) rhs_in
681 let rhs = addImplBound i (map fst newargs) rhs_in
648 ((rhs', defer), _) <-
682 ((rhs', defer), _) <-
649− tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []
683+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
650 (do pbinds lhs_tm
684 (do pbinds lhs_tm
651− erun fc (build i info False [] (UN "transform") rhs)
686+ erun fc (build i info False [] (sUN "transform") rhs)
652 erun fc $ psolve lhs_tm
687 erun fc $ psolve lhs_tm
653 tt <- get_term
688 tt <- get_term
654− let (tm, ds) = runState (collectDeferred Nothing tt) []
689+ return (runState (collectDeferred Nothing tt) []))
656 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
690 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
657 logLvl 3 ("Transform RHS " ++ show crhs_tm)
691 logLvl 3 ("Transform RHS " ++ show crhs_tm)
658 when safe $ case converts ctxt [] clhs_tm crhs_tm of
692 when safe $ case converts ctxt [] clhs_tm crhs_tm of
@@ -665,7 +699,7 @@ elabTransform info fc safe lhs_in rhs_in
665elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
699elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
666 PTerm -> String -> Name -> PTerm -> Idris ()
700 PTerm -> String -> Name -> PTerm -> Idris ()
667elabRecord info syn doc fc tyn ty cdoc cn cty
701elabRecord info syn doc fc tyn ty cdoc cn cty
668− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
702+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])
669 cty' <- implicit syn cn cty
703 cty' <- implicit syn cn cty
670 i <- getIState
704 i <- getIState
671 cty <- case lookupTy cn (tt_ctxt i) of
705 cty <- case lookupTy cn (tt_ctxt i) of
@@ -719,18 +753,18 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
719 getRecTy (PPi _ n ty s) = getRecTy s
753 getRecTy (PPi _ n ty s) = getRecTy s
720 getRecTy t = t
754 getRecTy t = t
722− rec = MN 0 "rec"
756+ rec = sMN 0 "rec"
724− mkp (UN n) = MN 0 ("p_" ++ n)
758+ mkp (UN n) = sMN 0 ("p_" ++ str n)
725− mkp (MN i n) = MN i ("p_" ++ n)
759+ mkp (MN i n) = sMN i ("p_" ++ str n)
726 mkp (NS n s) = NS (mkp n) s
760 mkp (NS n s) = NS (mkp n) s
728− mkImp (UN n) = UN ("implicit_" ++ n)
762+ mkImp (UN n) = sUN ("implicit_" ++ str n)
729− mkImp (MN i n) = MN i ("implicit_" ++ n)
763+ mkImp (MN i n) = sMN i ("implicit_" ++ str n)
730 mkImp (NS n s) = NS (mkImp n) s
764 mkImp (NS n s) = NS (mkImp n) s
732− mkType (UN n) = UN ("set_" ++ n)
766+ mkType (UN n) = sUN ("set_" ++ str n)
733− mkType (MN i n) = MN i ("set_" ++ n)
767+ mkType (MN i n) = sMN i ("set_" ++ str n)
734 mkType (NS n s) = NS (mkType n) s
768 mkType (NS n s) = NS (mkType n) s
736 mkProj recty substs cimp ((pn_in, pty), pos)
770 mkProj recty substs cimp ((pn_in, pty), pos)
@@ -753,11 +787,11 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
754 mkUpdate recty k num ((pn, pty), pos)
788 mkUpdate recty k num ((pn, pty), pos)
755 = do let setname = expandNS syn $ mkType pn
789 = do let setname = expandNS syn $ mkType pn
756− let valname = MN 0 "updateval"
790+ let valname = sMN 0 "updateval"
757 let pt = k (PPi expl pn pty
791 let pt = k (PPi expl pn pty
758 (PPi expl rec recty recty))
792 (PPi expl rec recty recty))
759 let pfnTy = PTy "" defaultSyntax fc [] setname pt
793 let pfnTy = PTy "" defaultSyntax fc [] setname pt
760− let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]
794+ let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
761 let lhsArgs = pls
795 let lhsArgs = pls
762 let rhsArgs = take pos pls ++ (PRef fc valname) :
796 let rhsArgs = take pos pls ++ (PRef fc valname) :
763 drop (pos + 1) pls
797 drop (pos + 1) pls
@@ -772,8 +806,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
772 return (pn, pfnTy, PClauses fc [] setname [pclause])
806 return (pn, pfnTy, PClauses fc [] setname [pclause])
774elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
808elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
775− (String, Name, PTerm, FC) -> Idris (Name, Type)
809+ (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)
776−elabCon info syn tn codata (doc, n, t_in, fc)
810+elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
777 = do checkUndefined fc n
811 = do checkUndefined fc n
778 ctxt <- getContext
812 ctxt <- getContext
779 i <- getIState
813 i <- getIState
@@ -796,7 +830,10 @@ elabCon info syn tn codata (doc, n, t_in, fc)
796 addIBC (IBCDef n)
830 addIBC (IBCDef n)
797 addDocStr n doc
831 addDocStr n doc
798 addIBC (IBCDoc n)
832 addIBC (IBCDoc n)
833+ let fs = map (getNamePos 0 t) forcenames
834+ -- FIXME: 'forcenames' is an almighty hack! Need a better way of
835+ -- erasing non-forceable things
799− forceArgs tn n cty'
836+ forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
800 return (n, cty')
837 return (n, cty')
802 tyIs (Bind n b sc) = tyIs sc
839 tyIs (Bind n b sc) = tyIs sc
@@ -808,6 +845,11 @@ elabCon info syn tn codata (doc, n, t_in, fc)
808 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)
845 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)
809 mkLazy t = t
846 mkLazy t = t
848+ getNamePos :: Int -> PTerm -> Name -> Maybe Int
849+ getNamePos i (PPi _ n _ sc) x | n == x = Just i
850+ | otherwise = getNamePos (i + 1) sc x
851+ getNamePos _ _ _ = Nothing
811-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
853-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
812-- top-level definition.
854-- top-level definition.
813elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
855elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
@@ -1120,7 +1162,7 @@ elabPE info fc caller r =
1120 _ -> error "Can't happen (getSpecTy)"
1162 _ -> error "Can't happen (getSpecTy)"
1122 getSpecClause ist (n, args)
1164 getSpecClause ist (n, args)
1123− = let newnm = UN ("__"++show (nsroot n) ++ "_" ++
1165+ = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++
1124 showSep "_" (map showArg args)) in
1166 showSep "_" (map showArg args)) in
1125 -- UN (show n ++ show (map snd args)) in
1167 -- UN (show n ++ show (map snd args)) in
1126 (n, newnm, mkPE_TermDecl ist newnm n args)
1168 (n, newnm, mkPE_TermDecl ist newnm n args)
@@ -1145,8 +1187,8 @@ elabValBind info aspat tm_in
1145 ((tm', defer, is), _) <-
1187 ((tm', defer, is), _) <-
1146-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
1188-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
1147-- (build i info aspat (MN 0 "val") tm))
1189-- (build i info aspat (MN 0 "val") tm))
1148− tclift (elaborate ctxt (MN 0 "val") infP []
1190+ tclift (elaborate ctxt (sMN 0 "val") infP []
1149− (build i info aspat [Reflection] (MN 0 "val") (infTerm tm)))
1191+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
1150 let vtm = orderPats (getInferTerm tm')
1192 let vtm = orderPats (getInferTerm tm')
1152 def' <- checkDef (fileFC "(input)") defer
1194 def' <- checkDef (fileFC "(input)") defer
@@ -1176,7 +1218,7 @@ checkPossible info fc tcgen fname lhs_in
1176 i <- getIState
1218 i <- getIState
1177 let lhs = addImpl i lhs_in
1219 let lhs = addImpl i lhs_in
1178 -- if the LHS type checks, it is possible
1220 -- if the LHS type checks, it is possible
1179− case elaborate ctxt (MN 0 "patLHS") infP []
1221+ case elaborate ctxt (sMN 0 "patLHS") infP []
1180 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
1222 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
1181 OK ((lhs', _, _), _) ->
1223 OK ((lhs', _, _), _) ->
1182 do let lhs_tm = orderPats (getInferTerm lhs')
1224 do let lhs_tm = orderPats (getInferTerm lhs')
@@ -1231,7 +1273,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1231 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
1273 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
1233 ((lhs', dlhs, []), _) <-
1275 ((lhs', dlhs, []), _) <-
1234− tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1276+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1235 (errAt "left hand side of " fname
1277 (errAt "left hand side of " fname
1236 (erun fc (buildTC i info True opts fname (infTerm lhs))))
1278 (erun fc (buildTC i info True opts fname (infTerm lhs))))
1237 let lhs_tm = orderPats (getInferTerm lhs')
1279 let lhs_tm = orderPats (getInferTerm lhs')
@@ -1244,8 +1286,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1245 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
1287 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
1247− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1291+ addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1248− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1292+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1250 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1294 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1251 -- Elaborate where block
1295 -- Elaborate where block
@@ -1273,10 +1317,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1273 ctxt <- getContext -- new context with where block added
1317 ctxt <- getContext -- new context with where block added
1274 logLvl 5 "STARTING CHECK"
1318 logLvl 5 "STARTING CHECK"
1275 ((rhs', defer, is), _) <-
1319 ((rhs', defer, is), _) <-
1276− tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
1320+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
1277 (do pbinds lhs_tm
1321 (do pbinds lhs_tm
1278 (_, _, is) <- errAt "right hand side of " fname
1323 (_, _, is) <- errAt "right hand side of " fname
1279− (erun fc (build i info False opts fname rhs))
1324+ (erun fc (build i info False opts fname rhs))
1280 errAt "right hand side of " fname
1325 errAt "right hand side of " fname
1281 (erun fc $ psolve lhs_tm)
1326 (erun fc $ psolve lhs_tm)
1282 hs <- get_holes
1327 hs <- get_holes
@@ -1287,7 +1332,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1287 return (tm, ds, is))
1332 return (tm, ds, is))
1288 logLvl 5 "DONE CHECK"
1333 logLvl 5 "DONE CHECK"
1289 logLvl 2 $ "---> " ++ show rhs'
1334 logLvl 2 $ "---> " ++ show rhs'
1290− when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
1335+ when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)
1291 def' <- checkDef fc defer
1336 def' <- checkDef fc defer
1292 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1337 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1293 addDeferred def''
1338 addDeferred def''
@@ -1303,6 +1348,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1304 ctxt <- getContext
1349 ctxt <- getContext
1305 logLvl 5 $ "Rechecking"
1350 logLvl 5 $ "Rechecking"
1351+ logLvl 6 $ " ==> " ++ show (forget rhs')
1306 (crhs, crhsty) <- recheckC fc [] rhs'
1352 (crhs, crhsty) <- recheckC fc [] rhs'
1307 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
1353 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
1308 case converts ctxt [] clhsty crhsty of
1354 case converts ctxt [] clhsty crhsty of
@@ -1408,7 +1454,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1408 let lhs = addImplPat i (stripLinear i lhs_in)
1454 let lhs = addImplPat i (stripLinear i lhs_in)
1409 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1455 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1410 ((lhs', dlhs, []), _) <-
1456 ((lhs', dlhs, []), _) <-
1411− tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1457+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1412 (errAt "left hand side of with in " fname
1458 (errAt "left hand side of with in " fname
1413 (erun fc (buildTC i info True opts fname (infTerm lhs))) )
1459 (erun fc (buildTC i info True opts fname (infTerm lhs))) )
1414 let lhs_tm = orderPats (getInferTerm lhs')
1460 let lhs_tm = orderPats (getInferTerm lhs')
@@ -1422,9 +1468,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1422 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
1468 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
1423 -- Elaborate wval in this context
1469 -- Elaborate wval in this context
1424 ((wval', defer, is), _) <-
1470 ((wval', defer, is), _) <-
1425− tclift $ elaborate ctxt (MN 0 "withRHS")
1471+ tclift $ elaborate ctxt (sMN 0 "withRHS")
1426 (bindTyArgs PVTy bargs infP) []
1472 (bindTyArgs PVTy bargs infP) []
1427 (do pbinds lhs_tm
1473 (do pbinds lhs_tm
1428 -- TODO: may want where here - see winfo abpve
1475 -- TODO: may want where here - see winfo abpve
1429 (_', d, is) <- errAt "with value in " fname
1476 (_', d, is) <- errAt "with value in " fname
1430 (erun fc (build i info False opts fname (infTerm wval)))
1477 (erun fc (build i info False opts fname (infTerm wval)))
@@ -1454,11 +1501,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1454 let wargtype = getRetTy cwvaltyN
1501 let wargtype = getRetTy cwvaltyN
1455 logLvl 5 ("Abstract over " ++ show wargval)
1502 logLvl 5 ("Abstract over " ++ show wargval)
1456 let wtype = bindTyArgs Pi (bargs_pre ++
1503 let wtype = bindTyArgs Pi (bargs_pre ++
1457− (MN 0 "warg", wargtype) :
1504+ (sMN 0 "warg", wargtype) :
1458− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
1505+ map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
1459− (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
1506+ (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)
1460 logLvl 3 ("New function type " ++ show wtype)
1507 logLvl 3 ("New function type " ++ show wtype)
1461− let wname = MN windex (show fname)
1508+ let wname = sMN windex (show fname)
1463 let imps = getImps wtype -- add to implicits context
1510 let imps = getImps wtype -- add to implicits context
1464 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
1511 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
@@ -1486,8 +1533,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1486 ctxt <- getContext -- New context with block added
1533 ctxt <- getContext -- New context with block added
1487 i <- getIState
1534 i <- getIState
1488 ((rhs', defer, is), _) <-
1535 ((rhs', defer, is), _) <-
1489− tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []
1536+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []
1490 (do pbinds lhs_tm
1537 (do pbinds lhs_tm
1491 (_, d, is) <- erun fc (build i info False opts fname rhs)
1539 (_, d, is) <- erun fc (build i info False opts fname rhs)
1492 psolve lhs_tm
1540 psolve lhs_tm
1493 tt <- get_term
1541 tt <- get_term
@@ -1566,7 +1614,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->
1566 FC -> [PTerm] ->
1614 FC -> [PTerm] ->
1567 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1615 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1568elabClass info syn doc fc constraints tn ps ds
1616elabClass info syn doc fc constraints tn ps ds
1569− = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1617+ = do let cn = sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1570 let tty = pibind ps PType
1618 let tty = pibind ps PType
1571 let constraint = PApp fc (PRef fc tn)
1619 let constraint = PApp fc (PRef fc tn)
1572 (map (pexp . PRef fc) (map fst ps))
1620 (map (pexp . PRef fc) (map fst ps))
@@ -1589,7 +1637,7 @@ elabClass info syn doc fc constraints tn ps ds
1589 let cty = impbind ps $ conbind constraints
1637 let cty = impbind ps $ conbind constraints
1590 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1638 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1591 constraint
1639 constraint
1592− let cons = [("", cn, cty, fc)]
1640+ let cons = [("", cn, cty, fc, [])]
1593 let ddecl = PDatadecl tn tty cons
1641 let ddecl = PDatadecl tn tty cons
1594 logLvl 5 $ "Class data " ++ showDImp True ddecl
1642 logLvl 5 $ "Class data " ++ showDImp True ddecl
1595 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
1643 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
@@ -1627,7 +1675,7 @@ elabClass info syn doc fc constraints tn ps ds
1628 impbind [] x = x
1676 impbind [] x = x
1629 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
1677 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
1630− conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
1678+ conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
1631 conbind [] x = x
1679 conbind [] x = x
1633 getMName (PTy _ _ _ _ n _) = nsroot n
1681 getMName (PTy _ _ _ _ n _) = nsroot n
@@ -1651,7 +1699,7 @@ elabClass info syn doc fc constraints tn ps ds
1651 _ -> ifail $ show n ++ " is not a method"
1699 _ -> ifail $ show n ++ " is not a method"
1652 defdecl _ _ _ = ifail "Can't happen (defdecl)"
1700 defdecl _ _ _ = ifail "Can't happen (defdecl)"
1654− defaultdec (UN n) = UN ("default#" ++ n)
1702+ defaultdec (UN n) = sUN ("default#" ++ str n)
1655 defaultdec (NS n ns) = NS (defaultdec n) ns
1703 defaultdec (NS n ns) = NS (defaultdec n) ns
1657 tydecl (PTy _ _ _ _ _ _) = True
1705 tydecl (PTy _ _ _ _ _ _) = True
@@ -1663,13 +1711,13 @@ elabClass info syn doc fc constraints tn ps ds
1664 -- Generate a function for chasing a dictionary constraint
1712 -- Generate a function for chasing a dictionary constraint
1665 cfun cn c syn all con
1713 cfun cn c syn all con
1666− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
1714+ = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)
1667 -- SN (ParentN cn (show con))
1715 -- SN (ParentN cn (show con))
1668− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1716+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
1669 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
1717 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
1670 let lhs = PApp fc (PRef fc cfn) [pconst capp]
1718 let lhs = PApp fc (PRef fc cfn) [pconst capp]
1671 let rhs = PResolveTC (fileFC "HACK")
1719 let rhs = PResolveTC (fileFC "HACK")
1672− let ty = PPi constraint (MN 0 "pc") c con
1720+ let ty = PPi constraint (sMN 0 "pc") c con
1673 iLOG (showImp Nothing True False ty)
1721 iLOG (showImp Nothing True False ty)
1674 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1722 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1675 i <- getIState
1723 i <- getIState
@@ -1689,10 +1737,10 @@ elabClass info syn doc fc constraints tn ps ds
1689 -- dictionary (this is inlinable, always)
1737 -- dictionary (this is inlinable, always)
1690 tfun cn c syn all (m, (doc, o, ty))
1738 tfun cn c syn all (m, (doc, o, ty))
1691 = do let ty' = insertConstraint c ty
1739 = do let ty' = insertConstraint c ty
1692− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1740+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
1693 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
1741 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
1694 let margs = getMArgs ty
1742 let margs = getMArgs ty
1695− let anames = map (\x -> MN x "arg") [0..]
1743+ let anames = map (\x -> sMN x "arg") [0..]
1696 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
1744 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
1697 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
1745 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
1698 iLOG (showImp Nothing True False ty)
1746 iLOG (showImp Nothing True False ty)
@@ -1721,7 +1769,7 @@ elabClass info syn doc fc constraints tn ps ds
1722 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
1770 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
1723 = PPi p n ty (insertConstraint c sc)
1771 = PPi p n ty (insertConstraint c sc)
1724− insertConstraint c sc = PPi constraint (MN 0 "class") c sc
1772+ insertConstraint c sc = PPi constraint (sMN 0 "class") c sc
1726 -- make arguments explicit and don't bind class parameters
1774 -- make arguments explicit and don't bind class parameters
1727 toExp ns e (PPi (Imp l s _ p) n ty sc)
1775 toExp ns e (PPi (Imp l s _ p) n ty sc)
@@ -1731,19 +1779,21 @@ elabClass info syn doc fc constraints tn ps ds
1731 toExp ns e sc = sc
1779 toExp ns e sc = sc
1733elabInstance :: ElabInfo -> SyntaxInfo ->
1781elabInstance :: ElabInfo -> SyntaxInfo ->
1782+ ElabWhat -> -- phase
1734 FC -> [PTerm] -> -- constraints
1783 FC -> [PTerm] -> -- constraints
1735 Name -> -- the class
1784 Name -> -- the class
1736 [PTerm] -> -- class parameters (i.e. instance)
1785 [PTerm] -> -- class parameters (i.e. instance)
1737 PTerm -> -- full instance type
1786 PTerm -> -- full instance type
1738 Maybe Name -> -- explicit name
1787 Maybe Name -> -- explicit name
1739 [PDecl] -> Idris ()
1788 [PDecl] -> Idris ()
1740−elabInstance info syn fc cs n ps t expn ds
1789+elabInstance info syn what fc cs n ps t expn ds = do
1741− = do i <- getIState
1790+ i <- getIState
1742− (n, ci) <- case lookupCtxtName n (idris_classes i) of
1791+ (n, ci) <- case lookupCtxtName n (idris_classes i) of
1743− [c] -> return c
1792+ [c] -> return c
1744− _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1793+ _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1745− let constraint = PApp fc (PRef fc n) (map pexp ps)
1794+ let constraint = PApp fc (PRef fc n) (map pexp ps)
1746− let iname = mkiname n ps expn
1795+ let iname = mkiname n ps expn
1796+ when (what /= EDefns) $ do
1747 nty <- elabType' True info syn "" fc [] iname t
1797 nty <- elabType' True info syn "" fc [] iname t
1748 -- if the instance type matches any of the instances we have already,
1798 -- if the instance type matches any of the instances we have already,
1749 -- and it's not a named instance, then it's overlapping, so report an error
1799 -- and it's not a named instance, then it's overlapping, so report an error
@@ -1752,6 +1802,7 @@ elabInstance info syn fc cs n ps t expn ds
1752 (class_instances ci)
1802 (class_instances ci)
1753 addInstance intInst n iname
1803 addInstance intInst n iname
1754 Just _ -> addInstance intInst n iname
1804 Just _ -> addInstance intInst n iname
1805+ when (what /= ETypes) $ do
1755 let ips = zip (class_params ci) ps
1806 let ips = zip (class_params ci) ps
1756 let ns = case n of
1807 let ns = case n of
1757 NS n ns' -> ns'
1808 NS n ns' -> ns'
@@ -1804,7 +1855,7 @@ elabInstance info syn fc cs n ps t expn ds
1805 mkiname n' ps' expn' =
1856 mkiname n' ps' expn' =
1806 case expn' of
1857 case expn' of
1807− Nothing -> SN (InstanceN n' (map show ps'))
1858+ Nothing -> SN (sInstanceN n' (map show ps'))
1808 Just nm -> nm
1859 Just nm -> nm
1810 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
1861 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
@@ -1852,14 +1903,14 @@ elabInstance info syn fc cs n ps t expn ds
1852 mkMethApp (n, _, _, ty)
1903 mkMethApp (n, _, _, ty)
1853 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
1904 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
1854 lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
1905 lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
1855− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1906+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
1856 lamBind i (PPi _ n ty sc) sc'
1907 lamBind i (PPi _ n ty sc) sc'
1857− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1908+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
1858 lamBind i _ sc = sc
1909 lamBind i _ sc = sc
1859 methArgs i (PPi (Imp _ _ _ _) n ty sc)
1910 methArgs i (PPi (Imp _ _ _ _) n ty sc)
1860− = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
1911+ = PImp 0 True False n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc
1861 methArgs i (PPi (Exp _ _ _ _) n ty sc)
1912 methArgs i (PPi (Exp _ _ _ _) n ty sc)
1862− = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
1913+ = PExp 0 False (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc
1863 methArgs i (PPi (Constraint _ _ _) n ty sc)
1914 methArgs i (PPi (Constraint _ _ _) n ty sc)
1864 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
1915 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
1865 methArgs i _ = []
1916 methArgs i _ = []
@@ -1882,14 +1933,14 @@ elabInstance info syn fc cs n ps t expn ds
1883 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
1934 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
1885− conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
1936+ conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
1886 conbind [] x = x
1937 conbind [] x = x
1888 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
1939 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
1889 coninsert cs sc = conbind cs sc
1940 coninsert cs sc = conbind cs sc
1891 insertDefaults :: IState -> Name ->
1942 insertDefaults :: IState -> Name ->
1892− [(Name, (Name, PDecl))] -> [String] ->
1943+ [(Name, (Name, PDecl))] -> [T.Text] ->
1893 [PDecl] -> [PDecl]
1944 [PDecl] -> [PDecl]
1894 insertDefaults i iname [] ns ds = ds
1945 insertDefaults i iname [] ns ds = ds
1895 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
1946 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
@@ -1980,7 +2031,7 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds
1981elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
2032elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
1982elabDecl what info d
2033elabDecl what info d
1983− = idrisCatch (elabDecl' what info d) (setAndReport)
2034+ = idrisCatch (withErrorReflection $ elabDecl' what info d) (setAndReport)
1985elabDecl' _ info (PFix _ _ _)
2036elabDecl' _ info (PFix _ _ _)
1986 = return () -- nothing to elaborate
2037 = return () -- nothing to elaborate
@@ -2011,8 +2062,10 @@ elabDecl' what info d@(PClauses f o n ps)
2011 [] -> []
2062 [] -> []
2012 elabClauses info f (o ++ o') n ps
2063 elabClauses info f (o ++ o') n ps
2013elabDecl' what info (PMutual f ps)
2064elabDecl' what info (PMutual f ps)
2066+ [p] -> elabDecl what info p
2014− = do mapM_ (elabDecl ETypes info) ps
2067+ _ -> do mapM_ (elabDecl ETypes info) ps
2015− mapM_ (elabDecl EDefns info) ps
2068+ mapM_ (elabDecl EDefns info) ps
2016 -- Do totality checking after entire mutual block
2069 -- Do totality checking after entire mutual block
2017 i <- get
2070 i <- get
2018 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
2071 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
@@ -2048,9 +2101,8 @@ elabDecl' what info (PClass doc s f cs n ps ds)
2048 = do iLOG $ "Elaborating class " ++ show n
2101 = do iLOG $ "Elaborating class " ++ show n
2049 elabClass info (s { syn_params = [] }) doc f cs n ps ds
2102 elabClass info (s { syn_params = [] }) doc f cs n ps ds
2050elabDecl' what info (PInstance s f cs n ps t expn ds)
2103elabDecl' what info (PInstance s f cs n ps t expn ds)
2052 = do iLOG $ "Elaborating instance " ++ show n
2104 = do iLOG $ "Elaborating instance " ++ show n
2053− elabInstance info s f cs n ps t expn ds
2105+ elabInstance info s what f cs n ps t expn ds
2054elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
2106elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
2055 | what /= ETypes
2107 | what /= ETypes
2056 = do iLOG $ "Elaborating record " ++ show tyn
2108 = do iLOG $ "Elaborating record " ++ show tyn
@@ -2074,7 +2126,7 @@ elabDecl' _ _ _ = return () -- skipped this time
2075elabCaseBlock info opts d@(PClauses f o n ps)
2127elabCaseBlock info opts d@(PClauses f o n ps)
2076 = do addIBC (IBCDef n)
2128 = do addIBC (IBCDef n)
2077− logLvl 6 $ "CASE BLOCK: " ++ show (n, d)
2129+ logLvl 5 $ "CASE BLOCK: " ++ show (n, d)
2078 let opts' = nub (o ++ opts)
2130 let opts' = nub (o ++ opts)
2079 -- propagate totality assertion to the new definitions
2131 -- propagate totality assertion to the new definitions
2080 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]
2132 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]