@@ -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
@@ -137,14 +140,20 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
137 | otherwise = mergeTy sc sc'
140 | otherwise = mergeTy sc sc'
138 mergeTy _ sc = sc
141 mergeTy _ sc = sc
146+ errrep = txt "ErrorReportPart"
140− tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))
148+ tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
141− (App (P _ (NS (UN "Maybe") ns2) _)
149+ (App (P _ (NS (UN m) ns2) _)
142− (App (P _ (NS (UN "List") ns3) _)
150+ (App (P _ (NS (UN l) ns3) _)
143− (P _ (NS (UN "ErrorReportPart") ns4) _))))
151+ (P _ (NS (UN r) ns4) _))))
152+ | e == err && m == maybe && l == lst && r == errrep
144− | ns1 == ["Errors","Reflection","Language"]
153+ , ns1 == map txt ["Errors","Reflection","Language"]
145− , ns2 == ["Maybe", "Prelude"]
154+ , ns2 == map txt ["Maybe", "Prelude"]
146− , ns3 == ["List", "Prelude"]
155+ , ns3 == map txt ["List", "Prelude"]
147− , ns4 == ["Errors","Reflection","Language"] = True
156+ , ns4 == map txt ["Errors","Reflection","Language"] = True
148 tyIsHandler _ = False
157 tyIsHandler _ = False
@@ -295,7 +304,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
295type EliminatorState = StateT (Map.Map String Int) Idris
304type EliminatorState = StateT (Map.Map String Int) Idris
297-- 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
298−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()
307+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->
308+ ElabInfo -> EliminatorState ()
299elabEliminator paramPos n ty cons info = do
309elabEliminator paramPos n ty cons info = do
300 elimLog $ "Elaborating eliminator"
310 elimLog $ "Elaborating eliminator"
301 let (cnstrs, _) = splitPi ty
311 let (cnstrs, _) = splitPi ty
@@ -303,7 +313,7 @@ elabEliminator paramPos n ty cons info = do
303 generalParams <- namePis False pms
313 generalParams <- namePis False pms
304 motiveIdxs <- namePis False idxs
314 motiveIdxs <- namePis False idxs
305 let motive = mkMotive n paramPos generalParams motiveIdxs
315 let motive = mkMotive n paramPos generalParams motiveIdxs
306− consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
316+ consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do
307 name <- freshName $ "elim_" ++ simpleName cnm
317 name <- freshName $ "elim_" ++ simpleName cnm
308 consTerm <- extractConsTerm c generalParams
318 consTerm <- extractConsTerm c generalParams
309 return (name, expl, consTerm)) cons
319 return (name, expl, consTerm)) cons
@@ -319,13 +329,13 @@ elabEliminator paramPos n ty cons info = do
319 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)
320 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
330 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
321 elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
331 elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
322− Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
332+ State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
323 -- Do not elaborate clauses if there aren't any
333 -- Do not elaborate clauses if there aren't any
324 case eliminatorClauses of
334 case eliminatorClauses of
325 [] -> return ()
335 [] -> return ()
326− _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
336+ _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
327 where elimLog :: String -> EliminatorState ()
337 where elimLog :: String -> EliminatorState ()
328− elimLog s = Control.Monad.State.lift (logLvl 2 s)
338+ elimLog s = State.lift (logLvl 2 s)
330 elimFC :: FC
340 elimFC :: FC
331 elimFC = fileFC "(eliminator)"
341 elimFC = fileFC "(eliminator)"
@@ -335,7 +345,7 @@ elabEliminator paramPos n ty cons info = do
336 applyNS :: Name -> [String] -> Name
346 applyNS :: Name -> [String] -> Name
337 applyNS n [] = n
347 applyNS n [] = n
338− applyNS n ns = NS n ns
348+ applyNS n ns = sNS n ns
340 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
350 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
341 splitPi = splitPi' []
351 splitPi = splitPi' []
@@ -374,11 +384,11 @@ elabEliminator paramPos n ty cons info = do
375 simpleName :: Name -> String
385 simpleName :: Name -> String
376 simpleName (NS n _) = simpleName n
386 simpleName (NS n _) = simpleName n
377− simpleName (MN i n) = n ++ show i
387+ simpleName (MN i n) = str n ++ show i
378 simpleName n = show n
388 simpleName n = show n
380 nameSpaces :: Name -> [String]
390 nameSpaces :: Name -> [String]
381− nameSpaces (NS _ ns) = ns
391+ nameSpaces (NS _ ns) = map str ns
382 nameSpaces _ = []
392 nameSpaces _ = []
384 freshName :: String -> EliminatorState Name
394 freshName :: String -> EliminatorState Name
@@ -387,16 +397,16 @@ elabEliminator paramPos n ty cons info = do
387 let i = fromMaybe 0 (Map.lookup key nameMap)
397 let i = fromMaybe 0 (Map.lookup key nameMap)
388 let name = key ++ show i
398 let name = key ++ show i
389 put $ Map.insert key (i+1) nameMap
399 put $ Map.insert key (i+1) nameMap
390− return (UN name)
400+ return (sUN name)
392 scrutineeName :: Name
402 scrutineeName :: Name
393− scrutineeName = UN "scrutinee"
403+ scrutineeName = sUN "scrutinee"
395 scrutineeArgName :: Name
405 scrutineeArgName :: Name
396− scrutineeArgName = UN "scrutineeArg"
406+ scrutineeArgName = sUN "scrutineeArg"
398 motiveName :: Name
408 motiveName :: Name
399− motiveName = UN "prop"
409+ motiveName = sUN "prop"
401 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
411 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
402 mkMotive n paramPos params indicies =
412 mkMotive n paramPos params indicies =
@@ -460,9 +470,9 @@ elabEliminator paramPos n ty cons info = do
460 splitArgPms _ = ([],[])
470 splitArgPms _ = ([],[])
463− implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
473+ implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
464− implicitIndexes (cns@(doc, cnm, ty, fc)) = do
474+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
465− i <- Control.Monad.State.lift getIState
475+ i <- State.lift getIState
466 implargs' <- case lookupCtxt cnm (idris_implicits i) of
476 implargs' <- case lookupCtxt cnm (idris_implicits i) of
467 [] -> do fail $ "Error while showing implicits for " ++ show cnm
477 [] -> do fail $ "Error while showing implicits for " ++ show cnm
468 [args] -> do return args
478 [args] -> do return args
@@ -475,18 +485,18 @@ elabEliminator paramPos n ty cons info = do
475 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
485 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
476 _ -> return implargs
486 _ -> return implargs
478− extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
488+ extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
479− extractConsTerm (doc, cnm, ty, fc) generalParameters = do
489+ extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do
480 let cons' = replaceParams paramPos generalParameters ty
490 let cons' = replaceParams paramPos generalParameters ty
481 let (args, resTy) = splitPi cons'
491 let (args, resTy) = splitPi cons'
482− implidxs <- implicitIndexes (doc, cnm, ty, fc)
492+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
483 consArgs <- namePis True args
493 consArgs <- namePis True args
484 let recArgs = findRecArgs consArgs
494 let recArgs = findRecArgs consArgs
485 let recMotives = map applyRecMotive recArgs
495 let recMotives = map applyRecMotive recArgs
486 let (_, consIdxs) = splitArgPms resTy
496 let (_, consIdxs) = splitArgPms resTy
487 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
497 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
488 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
498 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
489− 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))
490 where (_, idxs) = splitArgPms ty
500 where (_, idxs) = splitArgPms ty
492 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
502 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
@@ -511,12 +521,12 @@ elabEliminator paramPos n ty cons info = do
511 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
521 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
512 convertImplPi _ = Nothing
522 convertImplPi _ = Nothing
514− 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
515− generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
525+ generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
516 let cons' = replaceParams paramPos generalParameters ty
526 let cons' = replaceParams paramPos generalParameters ty
517 let (args, resTy) = splitPi cons'
527 let (args, resTy) = splitPi cons'
518− i <- Control.Monad.State.lift getIState
528+ i <- State.lift getIState
519− implidxs <- implicitIndexes (doc, cnm, ty, fc)
529+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
520 let (_, generalIdxs') = splitArgPms resTy
530 let (_, generalIdxs') = splitArgPms resTy
521 let generalIdxs = map pexp generalIdxs'
531 let generalIdxs = map pexp generalIdxs'
522 consArgs <- namePis True args
532 consArgs <- namePis True args
@@ -537,7 +547,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
538 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
548 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
539 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
549 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
540− addNameHint eqTy (UN "prf")
550+ addNameHint eqTy (sUN "prf")
541 elabDecl EAll toplevel elimDecl
551 elabDecl EAll toplevel elimDecl
542 mapM_ elabPrim primitives
552 mapM_ elabPrim primitives
543 -- 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
@@ -560,11 +570,11 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
561 p_believeMe [_,_,x] = Just x
571 p_believeMe [_,_,x] = Just x
562 p_believeMe _ = Nothing
572 p_believeMe _ = Nothing
563− believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
573+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))
564− (Bind (UN "b") (Pi (TType (UVar (-2))))
574+ (Bind (sUN "b") (Pi (TType (UVar (-2))))
565− (Bind (UN "x") (Pi (V 1)) (V 1)))
575+ (Bind (sUN "x") (Pi (V 1)) (V 1)))
566 elabBelieveMe
576 elabBelieveMe
567− = do let prim__believe_me = (UN "prim__believe_me")
577+ = do let prim__believe_me = sUN "prim__believe_me"
568 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
578 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
569 setTotality prim__believe_me (Partial NotCovering)
579 setTotality prim__believe_me (Partial NotCovering)
570 i <- getIState
580 i <- getIState
@@ -578,19 +588,19 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
578 | otherwise = Just (VApp vnNothing VErased)
588 | otherwise = Just (VApp vnNothing VErased)
579 p_synEq args = Nothing
589 p_synEq args = Nothing
581− nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased
591+ nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased
582− vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased
592+ vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased
583− vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased
593+ vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased
584 vnRefl = VP (DCon 0 2) eqCon VErased
594 vnRefl = VP (DCon 0 2) eqCon VErased
586− synEqTy = Bind (UN "a") (Pi (TType (UVar (-3))))
596+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))
587− (Bind (UN "b") (Pi (TType (UVar (-3))))
597+ (Bind (sUN "b") (Pi (TType (UVar (-3))))
588− (Bind (UN "x") (Pi (V 1))
598+ (Bind (sUN "x") (Pi (V 1))
589− (Bind (UN "y") (Pi (V 1))
599+ (Bind (sUN "y") (Pi (V 1))
590 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
600 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
591 [V 3, V 2, V 1, V 0]]))))
601 [V 3, V 2, V 1, V 0]]))))
592 elabSynEq
602 elabSynEq
593− = do let synEq = UN "prim__syntactic_eq"
603+ = do let synEq = sUN "prim__syntactic_eq"
595 updateContext (addOperator synEq synEqTy 4 p_synEq)
605 updateContext (addOperator synEq synEqTy 4 p_synEq)
596 setTotality synEq (Total [])
606 setTotality synEq (Total [])
@@ -628,7 +638,7 @@ elabProvider info syn fc n ty tm
628 -- Execute the type provider and normalise the result
638 -- Execute the type provider and normalise the result
629 -- use 'run__provider' to convert to a primitive IO action
639 -- use 'run__provider' to convert to a primitive IO action
631− rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)
641+ rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
632 [Erased, e])
642 [Erased, e])
633 let rhs' = normalise ctxt [] rhs
643 let rhs' = normalise ctxt [] rhs
634 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
644 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
@@ -646,9 +656,10 @@ elabProvider info syn fc n ty tm
647 isProviderOf :: TT Name -> TT Name -> Bool
657 isProviderOf :: TT Name -> TT Name -> Bool
648 isProviderOf tp prov
658 isProviderOf tp prov
649− | (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"
650− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
662+ , prov == txt "Provider" && provs == txt "Providers" = True
652 isProviderOf _ _ = False
663 isProviderOf _ _ = False
654-- | Elaborate a type provider
665-- | Elaborate a type provider
@@ -658,8 +669,8 @@ elabTransform info fc safe lhs_in rhs_in
658 i <- getIState
669 i <- getIState
659 let lhs = addImplPat i lhs_in
670 let lhs = addImplPat i lhs_in
660 ((lhs', dlhs, []), _) <-
671 ((lhs', dlhs, []), _) <-
661− tclift $ elaborate ctxt (MN 0 "transLHS") infP []
672+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []
662− (erun fc (buildTC i info True [] (UN "transform")
673+ (erun fc (buildTC i info True [] (sUN "transform")
663 (infTerm lhs)))
674 (infTerm lhs)))
664 let lhs_tm = orderPats (getInferTerm lhs')
675 let lhs_tm = orderPats (getInferTerm lhs')
665 let lhs_ty = getInferType lhs'
676 let lhs_ty = getInferType lhs'
@@ -669,13 +680,13 @@ elabTransform info fc safe lhs_in rhs_in
669 logLvl 3 ("Transform LHS " ++ show clhs_tm)
680 logLvl 3 ("Transform LHS " ++ show clhs_tm)
670 let rhs = addImplBound i (map fst newargs) rhs_in
681 let rhs = addImplBound i (map fst newargs) rhs_in
671 ((rhs', defer), _) <-
682 ((rhs', defer), _) <-
672− tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []
683+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
673 (do pbinds lhs_tm
684 (do pbinds lhs_tm
674− erun fc (build i info False [] (UN "transform") rhs)
686+ erun fc (build i info False [] (sUN "transform") rhs)
675 erun fc $ psolve lhs_tm
687 erun fc $ psolve lhs_tm
676 tt <- get_term
688 tt <- get_term
677− let (tm, ds) = runState (collectDeferred Nothing tt) []
689+ return (runState (collectDeferred Nothing tt) []))
679 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
690 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
680 logLvl 3 ("Transform RHS " ++ show crhs_tm)
691 logLvl 3 ("Transform RHS " ++ show crhs_tm)
681 when safe $ case converts ctxt [] clhs_tm crhs_tm of
692 when safe $ case converts ctxt [] clhs_tm crhs_tm of
@@ -688,7 +699,7 @@ elabTransform info fc safe lhs_in rhs_in
688elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
699elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
689 PTerm -> String -> Name -> PTerm -> Idris ()
700 PTerm -> String -> Name -> PTerm -> Idris ()
690elabRecord info syn doc fc tyn ty cdoc cn cty
701elabRecord info syn doc fc tyn ty cdoc cn cty
691− = 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, [])])
692 cty' <- implicit syn cn cty
703 cty' <- implicit syn cn cty
693 i <- getIState
704 i <- getIState
694 cty <- case lookupTy cn (tt_ctxt i) of
705 cty <- case lookupTy cn (tt_ctxt i) of
@@ -742,18 +753,18 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
742 getRecTy (PPi _ n ty s) = getRecTy s
753 getRecTy (PPi _ n ty s) = getRecTy s
743 getRecTy t = t
754 getRecTy t = t
745− rec = MN 0 "rec"
756+ rec = sMN 0 "rec"
747− mkp (UN n) = MN 0 ("p_" ++ n)
758+ mkp (UN n) = sMN 0 ("p_" ++ str n)
748− mkp (MN i n) = MN i ("p_" ++ n)
759+ mkp (MN i n) = sMN i ("p_" ++ str n)
749 mkp (NS n s) = NS (mkp n) s
760 mkp (NS n s) = NS (mkp n) s
751− mkImp (UN n) = UN ("implicit_" ++ n)
762+ mkImp (UN n) = sUN ("implicit_" ++ str n)
752− mkImp (MN i n) = MN i ("implicit_" ++ n)
763+ mkImp (MN i n) = sMN i ("implicit_" ++ str n)
753 mkImp (NS n s) = NS (mkImp n) s
764 mkImp (NS n s) = NS (mkImp n) s
755− mkType (UN n) = UN ("set_" ++ n)
766+ mkType (UN n) = sUN ("set_" ++ str n)
756− mkType (MN i n) = MN i ("set_" ++ n)
767+ mkType (MN i n) = sMN i ("set_" ++ str n)
757 mkType (NS n s) = NS (mkType n) s
768 mkType (NS n s) = NS (mkType n) s
759 mkProj recty substs cimp ((pn_in, pty), pos)
770 mkProj recty substs cimp ((pn_in, pty), pos)
@@ -776,11 +787,11 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
777 mkUpdate recty k num ((pn, pty), pos)
788 mkUpdate recty k num ((pn, pty), pos)
778 = do let setname = expandNS syn $ mkType pn
789 = do let setname = expandNS syn $ mkType pn
779− let valname = MN 0 "updateval"
790+ let valname = sMN 0 "updateval"
780 let pt = k (PPi expl pn pty
791 let pt = k (PPi expl pn pty
781 (PPi expl rec recty recty))
792 (PPi expl rec recty recty))
782 let pfnTy = PTy "" defaultSyntax fc [] setname pt
793 let pfnTy = PTy "" defaultSyntax fc [] setname pt
783− 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]
784 let lhsArgs = pls
795 let lhsArgs = pls
785 let rhsArgs = take pos pls ++ (PRef fc valname) :
796 let rhsArgs = take pos pls ++ (PRef fc valname) :
786 drop (pos + 1) pls
797 drop (pos + 1) pls
@@ -795,8 +806,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
795 return (pn, pfnTy, PClauses fc [] setname [pclause])
806 return (pn, pfnTy, PClauses fc [] setname [pclause])
797elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
808elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
798− (String, Name, PTerm, FC) -> Idris (Name, Type)
809+ (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)
799−elabCon info syn tn codata (doc, n, t_in, fc)
810+elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
800 = do checkUndefined fc n
811 = do checkUndefined fc n
801 ctxt <- getContext
812 ctxt <- getContext
802 i <- getIState
813 i <- getIState
@@ -819,7 +830,10 @@ elabCon info syn tn codata (doc, n, t_in, fc)
819 addIBC (IBCDef n)
830 addIBC (IBCDef n)
820 addDocStr n doc
831 addDocStr n doc
821 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
822− forceArgs tn n cty'
836+ forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
823 return (n, cty')
837 return (n, cty')
825 tyIs (Bind n b sc) = tyIs sc
839 tyIs (Bind n b sc) = tyIs sc
@@ -831,6 +845,11 @@ elabCon info syn tn codata (doc, n, t_in, fc)
831 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)
832 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
834-- | 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
835-- top-level definition.
854-- top-level definition.
836elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
855elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
@@ -1143,7 +1162,7 @@ elabPE info fc caller r =
1143 _ -> error "Can't happen (getSpecTy)"
1162 _ -> error "Can't happen (getSpecTy)"
1145 getSpecClause ist (n, args)
1164 getSpecClause ist (n, args)
1146− = let newnm = UN ("__"++show (nsroot n) ++ "_" ++
1165+ = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++
1147 showSep "_" (map showArg args)) in
1166 showSep "_" (map showArg args)) in
1148 -- UN (show n ++ show (map snd args)) in
1167 -- UN (show n ++ show (map snd args)) in
1149 (n, newnm, mkPE_TermDecl ist newnm n args)
1168 (n, newnm, mkPE_TermDecl ist newnm n args)
@@ -1168,8 +1187,8 @@ elabValBind info aspat tm_in
1168 ((tm', defer, is), _) <-
1187 ((tm', defer, is), _) <-
1169-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
1188-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
1170-- (build i info aspat (MN 0 "val") tm))
1189-- (build i info aspat (MN 0 "val") tm))
1171− tclift (elaborate ctxt (MN 0 "val") infP []
1190+ tclift (elaborate ctxt (sMN 0 "val") infP []
1172− (build i info aspat [Reflection] (MN 0 "val") (infTerm tm)))
1191+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
1173 let vtm = orderPats (getInferTerm tm')
1192 let vtm = orderPats (getInferTerm tm')
1175 def' <- checkDef (fileFC "(input)") defer
1194 def' <- checkDef (fileFC "(input)") defer
@@ -1199,7 +1218,7 @@ checkPossible info fc tcgen fname lhs_in
1199 i <- getIState
1218 i <- getIState
1200 let lhs = addImpl i lhs_in
1219 let lhs = addImpl i lhs_in
1201 -- if the LHS type checks, it is possible
1220 -- if the LHS type checks, it is possible
1202− case elaborate ctxt (MN 0 "patLHS") infP []
1221+ case elaborate ctxt (sMN 0 "patLHS") infP []
1203 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
1222 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
1204 OK ((lhs', _, _), _) ->
1223 OK ((lhs', _, _), _) ->
1205 do let lhs_tm = orderPats (getInferTerm lhs')
1224 do let lhs_tm = orderPats (getInferTerm lhs')
@@ -1254,7 +1273,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1254 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))
1256 ((lhs', dlhs, []), _) <-
1275 ((lhs', dlhs, []), _) <-
1257− tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1276+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1258 (errAt "left hand side of " fname
1277 (errAt "left hand side of " fname
1259 (erun fc (buildTC i info True opts fname (infTerm lhs))))
1278 (erun fc (buildTC i info True opts fname (infTerm lhs))))
1260 let lhs_tm = orderPats (getInferTerm lhs')
1279 let lhs_tm = orderPats (getInferTerm lhs')
@@ -1267,8 +1286,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1268 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
1287 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
1270− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1291+ addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1271− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1292+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1273 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1294 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1274 -- Elaborate where block
1295 -- Elaborate where block
@@ -1296,10 +1317,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1296 ctxt <- getContext -- new context with where block added
1317 ctxt <- getContext -- new context with where block added
1297 logLvl 5 "STARTING CHECK"
1318 logLvl 5 "STARTING CHECK"
1298 ((rhs', defer, is), _) <-
1319 ((rhs', defer, is), _) <-
1299− tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
1320+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
1300 (do pbinds lhs_tm
1321 (do pbinds lhs_tm
1301 (_, _, is) <- errAt "right hand side of " fname
1323 (_, _, is) <- errAt "right hand side of " fname
1302− (erun fc (build i info False opts fname rhs))
1324+ (erun fc (build i info False opts fname rhs))
1303 errAt "right hand side of " fname
1325 errAt "right hand side of " fname
1304 (erun fc $ psolve lhs_tm)
1326 (erun fc $ psolve lhs_tm)
1305 hs <- get_holes
1327 hs <- get_holes
@@ -1326,6 +1348,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1327 ctxt <- getContext
1349 ctxt <- getContext
1328 logLvl 5 $ "Rechecking"
1350 logLvl 5 $ "Rechecking"
1351+ logLvl 6 $ " ==> " ++ show (forget rhs')
1329 (crhs, crhsty) <- recheckC fc [] rhs'
1352 (crhs, crhsty) <- recheckC fc [] rhs'
1330 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
1353 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
1331 case converts ctxt [] clhsty crhsty of
1354 case converts ctxt [] clhsty crhsty of
@@ -1431,7 +1454,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1431 let lhs = addImplPat i (stripLinear i lhs_in)
1454 let lhs = addImplPat i (stripLinear i lhs_in)
1432 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1455 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1433 ((lhs', dlhs, []), _) <-
1456 ((lhs', dlhs, []), _) <-
1434− tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1457+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1435 (errAt "left hand side of with in " fname
1458 (errAt "left hand side of with in " fname
1436 (erun fc (buildTC i info True opts fname (infTerm lhs))) )
1459 (erun fc (buildTC i info True opts fname (infTerm lhs))) )
1437 let lhs_tm = orderPats (getInferTerm lhs')
1460 let lhs_tm = orderPats (getInferTerm lhs')
@@ -1445,9 +1468,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1445 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
1468 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
1446 -- Elaborate wval in this context
1469 -- Elaborate wval in this context
1447 ((wval', defer, is), _) <-
1470 ((wval', defer, is), _) <-
1448− tclift $ elaborate ctxt (MN 0 "withRHS")
1471+ tclift $ elaborate ctxt (sMN 0 "withRHS")
1449 (bindTyArgs PVTy bargs infP) []
1472 (bindTyArgs PVTy bargs infP) []
1450 (do pbinds lhs_tm
1473 (do pbinds lhs_tm
1451 -- TODO: may want where here - see winfo abpve
1475 -- TODO: may want where here - see winfo abpve
1452 (_', d, is) <- errAt "with value in " fname
1476 (_', d, is) <- errAt "with value in " fname
1453 (erun fc (build i info False opts fname (infTerm wval)))
1477 (erun fc (build i info False opts fname (infTerm wval)))
@@ -1477,11 +1501,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1477 let wargtype = getRetTy cwvaltyN
1501 let wargtype = getRetTy cwvaltyN
1478 logLvl 5 ("Abstract over " ++ show wargval)
1502 logLvl 5 ("Abstract over " ++ show wargval)
1479 let wtype = bindTyArgs Pi (bargs_pre ++
1503 let wtype = bindTyArgs Pi (bargs_pre ++
1480− (MN 0 "warg", wargtype) :
1504+ (sMN 0 "warg", wargtype) :
1481− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
1505+ map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
1482− (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
1506+ (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)
1483 logLvl 3 ("New function type " ++ show wtype)
1507 logLvl 3 ("New function type " ++ show wtype)
1484− let wname = MN windex (show fname)
1508+ let wname = sMN windex (show fname)
1486 let imps = getImps wtype -- add to implicits context
1510 let imps = getImps wtype -- add to implicits context
1487 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
1511 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
@@ -1509,8 +1533,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1509 ctxt <- getContext -- New context with block added
1533 ctxt <- getContext -- New context with block added
1510 i <- getIState
1534 i <- getIState
1511 ((rhs', defer, is), _) <-
1535 ((rhs', defer, is), _) <-
1512− tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []
1536+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []
1513 (do pbinds lhs_tm
1537 (do pbinds lhs_tm
1514 (_, d, is) <- erun fc (build i info False opts fname rhs)
1539 (_, d, is) <- erun fc (build i info False opts fname rhs)
1515 psolve lhs_tm
1540 psolve lhs_tm
1516 tt <- get_term
1541 tt <- get_term
@@ -1589,7 +1614,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->
1589 FC -> [PTerm] ->
1614 FC -> [PTerm] ->
1590 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1615 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1591elabClass info syn doc fc constraints tn ps ds
1616elabClass info syn doc fc constraints tn ps ds
1592− = 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)
1593 let tty = pibind ps PType
1618 let tty = pibind ps PType
1594 let constraint = PApp fc (PRef fc tn)
1619 let constraint = PApp fc (PRef fc tn)
1595 (map (pexp . PRef fc) (map fst ps))
1620 (map (pexp . PRef fc) (map fst ps))
@@ -1612,7 +1637,7 @@ elabClass info syn doc fc constraints tn ps ds
1612 let cty = impbind ps $ conbind constraints
1637 let cty = impbind ps $ conbind constraints
1613 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1638 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1614 constraint
1639 constraint
1615− let cons = [("", cn, cty, fc)]
1640+ let cons = [("", cn, cty, fc, [])]
1616 let ddecl = PDatadecl tn tty cons
1641 let ddecl = PDatadecl tn tty cons
1617 logLvl 5 $ "Class data " ++ showDImp True ddecl
1642 logLvl 5 $ "Class data " ++ showDImp True ddecl
1618 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
@@ -1650,7 +1675,7 @@ elabClass info syn doc fc constraints tn ps ds
1651 impbind [] x = x
1676 impbind [] x = x
1652 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)
1653− 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)
1654 conbind [] x = x
1679 conbind [] x = x
1656 getMName (PTy _ _ _ _ n _) = nsroot n
1681 getMName (PTy _ _ _ _ n _) = nsroot n
@@ -1674,7 +1699,7 @@ elabClass info syn doc fc constraints tn ps ds
1674 _ -> ifail $ show n ++ " is not a method"
1699 _ -> ifail $ show n ++ " is not a method"
1675 defdecl _ _ _ = ifail "Can't happen (defdecl)"
1700 defdecl _ _ _ = ifail "Can't happen (defdecl)"
1677− defaultdec (UN n) = UN ("default#" ++ n)
1702+ defaultdec (UN n) = sUN ("default#" ++ str n)
1678 defaultdec (NS n ns) = NS (defaultdec n) ns
1703 defaultdec (NS n ns) = NS (defaultdec n) ns
1680 tydecl (PTy _ _ _ _ _ _) = True
1705 tydecl (PTy _ _ _ _ _ _) = True
@@ -1686,13 +1711,13 @@ elabClass info syn doc fc constraints tn ps ds
1687 -- Generate a function for chasing a dictionary constraint
1712 -- Generate a function for chasing a dictionary constraint
1688 cfun cn c syn all con
1713 cfun cn c syn all con
1689− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
1714+ = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)
1690 -- SN (ParentN cn (show con))
1715 -- SN (ParentN cn (show con))
1691− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1716+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
1692 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)
1693 let lhs = PApp fc (PRef fc cfn) [pconst capp]
1718 let lhs = PApp fc (PRef fc cfn) [pconst capp]
1694 let rhs = PResolveTC (fileFC "HACK")
1719 let rhs = PResolveTC (fileFC "HACK")
1695− let ty = PPi constraint (MN 0 "pc") c con
1720+ let ty = PPi constraint (sMN 0 "pc") c con
1696 iLOG (showImp Nothing True False ty)
1721 iLOG (showImp Nothing True False ty)
1697 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1722 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1698 i <- getIState
1723 i <- getIState
@@ -1712,10 +1737,10 @@ elabClass info syn doc fc constraints tn ps ds
1712 -- dictionary (this is inlinable, always)
1737 -- dictionary (this is inlinable, always)
1713 tfun cn c syn all (m, (doc, o, ty))
1738 tfun cn c syn all (m, (doc, o, ty))
1714 = do let ty' = insertConstraint c ty
1739 = do let ty' = insertConstraint c ty
1715− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
1740+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
1716 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)
1717 let margs = getMArgs ty
1742 let margs = getMArgs ty
1718− let anames = map (\x -> MN x "arg") [0..]
1743+ let anames = map (\x -> sMN x "arg") [0..]
1719 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)
1720 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
1745 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
1721 iLOG (showImp Nothing True False ty)
1746 iLOG (showImp Nothing True False ty)
@@ -1744,7 +1769,7 @@ elabClass info syn doc fc constraints tn ps ds
1745 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
1770 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
1746 = PPi p n ty (insertConstraint c sc)
1771 = PPi p n ty (insertConstraint c sc)
1747− insertConstraint c sc = PPi constraint (MN 0 "class") c sc
1772+ insertConstraint c sc = PPi constraint (sMN 0 "class") c sc
1749 -- make arguments explicit and don't bind class parameters
1774 -- make arguments explicit and don't bind class parameters
1750 toExp ns e (PPi (Imp l s _ p) n ty sc)
1775 toExp ns e (PPi (Imp l s _ p) n ty sc)
@@ -1754,19 +1779,21 @@ elabClass info syn doc fc constraints tn ps ds
1754 toExp ns e sc = sc
1779 toExp ns e sc = sc
1756elabInstance :: ElabInfo -> SyntaxInfo ->
1781elabInstance :: ElabInfo -> SyntaxInfo ->
1782+ ElabWhat -> -- phase
1757 FC -> [PTerm] -> -- constraints
1783 FC -> [PTerm] -> -- constraints
1758 Name -> -- the class
1784 Name -> -- the class
1759 [PTerm] -> -- class parameters (i.e. instance)
1785 [PTerm] -> -- class parameters (i.e. instance)
1760 PTerm -> -- full instance type
1786 PTerm -> -- full instance type
1761 Maybe Name -> -- explicit name
1787 Maybe Name -> -- explicit name
1762 [PDecl] -> Idris ()
1788 [PDecl] -> Idris ()
1763−elabInstance info syn fc cs n ps t expn ds
1789+elabInstance info syn what fc cs n ps t expn ds = do
1764− = do i <- getIState
1790+ i <- getIState
1765− (n, ci) <- case lookupCtxtName n (idris_classes i) of
1791+ (n, ci) <- case lookupCtxtName n (idris_classes i) of
1766− [c] -> return c
1792+ [c] -> return c
1767− _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1793+ _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1768− let constraint = PApp fc (PRef fc n) (map pexp ps)
1794+ let constraint = PApp fc (PRef fc n) (map pexp ps)
1769− let iname = mkiname n ps expn
1795+ let iname = mkiname n ps expn
1796+ when (what /= EDefns) $ do
1770 nty <- elabType' True info syn "" fc [] iname t
1797 nty <- elabType' True info syn "" fc [] iname t
1771 -- 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,
1772 -- 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
@@ -1775,6 +1802,7 @@ elabInstance info syn fc cs n ps t expn ds
1775 (class_instances ci)
1802 (class_instances ci)
1776 addInstance intInst n iname
1803 addInstance intInst n iname
1777 Just _ -> addInstance intInst n iname
1804 Just _ -> addInstance intInst n iname
1805+ when (what /= ETypes) $ do
1778 let ips = zip (class_params ci) ps
1806 let ips = zip (class_params ci) ps
1779 let ns = case n of
1807 let ns = case n of
1780 NS n ns' -> ns'
1808 NS n ns' -> ns'
@@ -1827,7 +1855,7 @@ elabInstance info syn fc cs n ps t expn ds
1828 mkiname n' ps' expn' =
1856 mkiname n' ps' expn' =
1829 case expn' of
1857 case expn' of
1830− Nothing -> SN (InstanceN n' (map show ps'))
1858+ Nothing -> SN (sInstanceN n' (map show ps'))
1831 Just nm -> nm
1859 Just nm -> nm
1833 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
1861 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
@@ -1875,14 +1903,14 @@ elabInstance info syn fc cs n ps t expn ds
1875 mkMethApp (n, _, _, ty)
1903 mkMethApp (n, _, _, ty)
1876 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
1904 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
1877 lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
1905 lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
1878− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1906+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
1879 lamBind i (PPi _ n ty sc) sc'
1907 lamBind i (PPi _ n ty sc) sc'
1880− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
1908+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
1881 lamBind i _ sc = sc
1909 lamBind i _ sc = sc
1882 methArgs i (PPi (Imp _ _ _ _) n ty sc)
1910 methArgs i (PPi (Imp _ _ _ _) n ty sc)
1883− = 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
1884 methArgs i (PPi (Exp _ _ _ _) n ty sc)
1912 methArgs i (PPi (Exp _ _ _ _) n ty sc)
1885− = 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
1886 methArgs i (PPi (Constraint _ _ _) n ty sc)
1914 methArgs i (PPi (Constraint _ _ _) n ty sc)
1887 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
1915 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
1888 methArgs i _ = []
1916 methArgs i _ = []
@@ -1905,14 +1933,14 @@ elabInstance info syn fc cs n ps t expn ds
1906 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
1934 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
1908− 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)
1909 conbind [] x = x
1937 conbind [] x = x
1911 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)
1912 coninsert cs sc = conbind cs sc
1940 coninsert cs sc = conbind cs sc
1914 insertDefaults :: IState -> Name ->
1942 insertDefaults :: IState -> Name ->
1915− [(Name, (Name, PDecl))] -> [String] ->
1943+ [(Name, (Name, PDecl))] -> [T.Text] ->
1916 [PDecl] -> [PDecl]
1944 [PDecl] -> [PDecl]
1917 insertDefaults i iname [] ns ds = ds
1945 insertDefaults i iname [] ns ds = ds
1918 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
1946 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
@@ -2034,8 +2062,10 @@ elabDecl' what info d@(PClauses f o n ps)
2034 [] -> []
2062 [] -> []
2035 elabClauses info f (o ++ o') n ps
2063 elabClauses info f (o ++ o') n ps
2036elabDecl' what info (PMutual f ps)
2064elabDecl' what info (PMutual f ps)
2066+ [p] -> elabDecl what info p
2037− = do mapM_ (elabDecl ETypes info) ps
2067+ _ -> do mapM_ (elabDecl ETypes info) ps
2038− mapM_ (elabDecl EDefns info) ps
2068+ mapM_ (elabDecl EDefns info) ps
2039 -- Do totality checking after entire mutual block
2069 -- Do totality checking after entire mutual block
2040 i <- get
2070 i <- get
2041 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
2071 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
@@ -2071,9 +2101,8 @@ elabDecl' what info (PClass doc s f cs n ps ds)
2071 = do iLOG $ "Elaborating class " ++ show n
2101 = do iLOG $ "Elaborating class " ++ show n
2072 elabClass info (s { syn_params = [] }) doc f cs n ps ds
2102 elabClass info (s { syn_params = [] }) doc f cs n ps ds
2073elabDecl' what info (PInstance s f cs n ps t expn ds)
2103elabDecl' what info (PInstance s f cs n ps t expn ds)
2075 = do iLOG $ "Elaborating instance " ++ show n
2104 = do iLOG $ "Elaborating instance " ++ show n
2076− elabInstance info s f cs n ps t expn ds
2105+ elabInstance info s what f cs n ps t expn ds
2077elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
2106elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
2078 | what /= ETypes
2107 | what /= ETypes
2079 = do iLOG $ "Elaborating record " ++ show tyn
2108 = do iLOG $ "Elaborating record " ++ show tyn