@@ -28,12 +28,13 @@ import Idris.Core.CaseTree
2828
2929import Control.DeepSeq
3030import Control.Monad
31−import Control.Monad.State
31+import Control.Monad.State.Strict as State
3232import Data.List
3333import Data.Maybe
3434import Debug.Trace
3535
3636import qualified Data.Map as Map
37+import qualified Data.Text as T
3738import Data.Char(isLetter, toLower)
3839import Data.List.Split (splitOn)
3940
@@ -91,8 +92,10 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
9192 let nty' = normalise ctxt [] nty
9293
9394 -- Add normalised type to internals
94− 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')))
95+ rep <- useREPL
96+ when rep $ do
97+ addInternalApp (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')))
9699
97100 let (t, _) = unApply (getRetTy nty')
98101 let corec = case t of
@@ -137,14 +140,20 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
137140 | otherwise = mergeTy sc sc'
138141 mergeTy _ sc = sc
139142
140− tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))
141− (App (P _ (NS (UN "Maybe") ns2) _)
142− (App (P _ (NS (UN "List") ns3) _)
143− (P _ (NS (UN "ErrorReportPart") ns4) _))))
144− | ns1 == ["Errors","Reflection","Language"]
145− , ns2 == ["Maybe", "Prelude"]
146− , ns3 == ["List", "Prelude"]
147− , ns4 == ["Errors","Reflection","Language"] = True
143+ err = txt "Err"
144+ maybe = txt "Maybe"
145+ lst = txt "List"
146+ errrep = txt "ErrorReportPart"
147+
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
148157 tyIsHandler _ = False
149158
150159
@@ -295,7 +304,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
295304type EliminatorState = StateT (Map.Map String Int) Idris
296305
297306-- 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 ()
299309elabEliminator paramPos n ty cons info = do
300310 elimLog $ "Elaborating eliminator"
301311 let (cnstrs, _) = splitPi ty
@@ -303,7 +313,7 @@ elabEliminator paramPos n ty cons info = do
303313 generalParams <- namePis False pms
304314 motiveIdxs <- namePis False idxs
305315 let motive = mkMotive n paramPos generalParams motiveIdxs
306− consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
316+ consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do
307317 name <- freshName $ "elim_" ++ simpleName cnm
308318 consTerm <- extractConsTerm c generalParams
309319 return (name, expl, consTerm)) cons
@@ -319,13 +329,13 @@ elabEliminator paramPos n ty cons info = do
319329 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
320330 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
321331 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 ())
323333 -- Do not elaborate clauses if there aren't any
324334 case eliminatorClauses of
325335 [] -> return ()
326− _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
336+ _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
327337 where elimLog :: String -> EliminatorState ()
328− elimLog s = Control.Monad.State.lift (logLvl 2 s)
338+ elimLog s = State.lift (logLvl 2 s)
329339
330340 elimFC :: FC
331341 elimFC = fileFC "(eliminator)"
@@ -335,7 +345,7 @@ elabEliminator paramPos n ty cons info = do
335345
336346 applyNS :: Name -> [String] -> Name
337347 applyNS n [] = n
338− applyNS n ns = NS n ns
348+ applyNS n ns = sNS n ns
339349
340350 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
341351 splitPi = splitPi' []
@@ -374,11 +384,11 @@ elabEliminator paramPos n ty cons info = do
374384
375385 simpleName :: Name -> String
376386 simpleName (NS n _) = simpleName n
377− simpleName (MN i n) = n ++ show i
387+ simpleName (MN i n) = str n ++ show i
378388 simpleName n = show n
379389
380390 nameSpaces :: Name -> [String]
381− nameSpaces (NS _ ns) = ns
391+ nameSpaces (NS _ ns) = map str ns
382392 nameSpaces _ = []
383393
384394 freshName :: String -> EliminatorState Name
@@ -387,16 +397,16 @@ elabEliminator paramPos n ty cons info = do
387397 let i = fromMaybe 0 (Map.lookup key nameMap)
388398 let name = key ++ show i
389399 put $ Map.insert key (i+1) nameMap
390− return (UN name)
400+ return (sUN name)
391401
392402 scrutineeName :: Name
393− scrutineeName = UN "scrutinee"
403+ scrutineeName = sUN "scrutinee"
394404
395405 scrutineeArgName :: Name
396− scrutineeArgName = UN "scrutineeArg"
406+ scrutineeArgName = sUN "scrutineeArg"
397407
398408 motiveName :: Name
399− motiveName = UN "prop"
409+ motiveName = sUN "prop"
400410
401411 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
402412 mkMotive n paramPos params indicies =
@@ -460,9 +470,9 @@ elabEliminator paramPos n ty cons info = do
460470 splitArgPms _ = ([],[])
461471
462472
463− implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
464− implicitIndexes (cns@(doc, cnm, ty, fc)) = do
465− i <- Control.Monad.State.lift getIState
473+ implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
474+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
475+ i <- State.lift getIState
466476 implargs' <- case lookupCtxt cnm (idris_implicits i) of
467477 [] -> do fail $ "Error while showing implicits for " ++ show cnm
468478 [args] -> do return args
@@ -475,18 +485,18 @@ elabEliminator paramPos n ty cons info = do
475485 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
476486 _ -> return implargs
477487
478− extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
479− extractConsTerm (doc, cnm, ty, fc) generalParameters = do
488+ extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
489+ extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do
480490 let cons' = replaceParams paramPos generalParameters ty
481491 let (args, resTy) = splitPi cons'
482− implidxs <- implicitIndexes (doc, cnm, ty, fc)
492+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
483493 consArgs <- namePis True args
484494 let recArgs = findRecArgs consArgs
485495 let recMotives = map applyRecMotive recArgs
486496 let (_, consIdxs) = splitArgPms resTy
487497 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
488498 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))
490500 where (_, idxs) = splitArgPms ty
491501
492502 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
@@ -511,12 +521,12 @@ elabEliminator paramPos n ty cons info = do
511521 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
512522 convertImplPi _ = Nothing
513523
514− generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
515− generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
524+ generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
525+ generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
516526 let cons' = replaceParams paramPos generalParameters ty
517527 let (args, resTy) = splitPi cons'
518− i <- Control.Monad.State.lift getIState
519− implidxs <- implicitIndexes (doc, cnm, ty, fc)
528+ i <- State.lift getIState
529+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
520530 let (_, generalIdxs') = splitArgPms resTy
521531 let generalIdxs = map pexp generalIdxs'
522532 consArgs <- namePis True args
@@ -537,7 +547,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
537547 (zip
538548 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
539549 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
540− addNameHint eqTy (UN "prf")
550+ addNameHint eqTy (sUN "prf")
541551 elabDecl EAll toplevel elimDecl
542552 mapM_ elabPrim primitives
543553 -- Special case prim__believe_me because it doesn't work on just constants
@@ -560,11 +570,11 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
560570
561571 p_believeMe [_,_,x] = Just x
562572 p_believeMe _ = Nothing
563− believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
564− (Bind (UN "b") (Pi (TType (UVar (-2))))
565− (Bind (UN "x") (Pi (V 1)) (V 1)))
573+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))
574+ (Bind (sUN "b") (Pi (TType (UVar (-2))))
575+ (Bind (sUN "x") (Pi (V 1)) (V 1)))
566576 elabBelieveMe
567− = do let prim__believe_me = (UN "prim__believe_me")
577+ = do let prim__believe_me = sUN "prim__believe_me"
568578 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
569579 setTotality prim__believe_me (Partial NotCovering)
570580 i <- getIState
@@ -578,19 +588,19 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
578588 | otherwise = Just (VApp vnNothing VErased)
579589 p_synEq args = Nothing
580590
581− nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased
582− vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased
583− vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased
591+ nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased
592+ vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased
593+ vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased
584594 vnRefl = VP (DCon 0 2) eqCon VErased
585595
586− synEqTy = Bind (UN "a") (Pi (TType (UVar (-3))))
587− (Bind (UN "b") (Pi (TType (UVar (-3))))
588− (Bind (UN "x") (Pi (V 1))
589− (Bind (UN "y") (Pi (V 1))
596+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))
597+ (Bind (sUN "b") (Pi (TType (UVar (-3))))
598+ (Bind (sUN "x") (Pi (V 1))
599+ (Bind (sUN "y") (Pi (V 1))
590600 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
591601 [V 3, V 2, V 1, V 0]]))))
592602 elabSynEq
593− = do let synEq = UN "prim__syntactic_eq"
603+ = do let synEq = sUN "prim__syntactic_eq"
594604
595605 updateContext (addOperator synEq synEqTy 4 p_synEq)
596606 setTotality synEq (Total [])
@@ -628,7 +638,7 @@ elabProvider info syn fc n ty tm
628638 -- Execute the type provider and normalise the result
629639 -- use 'run__provider' to convert to a primitive IO action
630640
631− rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)
641+ rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
632642 [Erased, e])
633643 let rhs' = normalise ctxt [] rhs
634644 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
@@ -646,9 +656,10 @@ elabProvider info syn fc n ty tm
646656
647657 isProviderOf :: TT Name -> TT Name -> Bool
648658 isProviderOf tp prov
649− | (P _ (UN "IO") _, [prov']) <- unApply prov
650− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
651− , tp == tp' = True
659+ | (P _ (UN io) _, [prov']) <- unApply prov
660+ , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'
661+ , tp == tp', io == txt "IO"
662+ , prov == txt "Provider" && provs == txt "Providers" = True
652663 isProviderOf _ _ = False
653664
654665-- | Elaborate a type provider
@@ -658,8 +669,8 @@ elabTransform info fc safe lhs_in rhs_in
658669 i <- getIState
659670 let lhs = addImplPat i lhs_in
660671 ((lhs', dlhs, []), _) <-
661− tclift $ elaborate ctxt (MN 0 "transLHS") infP []
662− (erun fc (buildTC i info True [] (UN "transform")
672+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []
673+ (erun fc (buildTC i info True [] (sUN "transform")
663674 (infTerm lhs)))
664675 let lhs_tm = orderPats (getInferTerm lhs')
665676 let lhs_ty = getInferType lhs'
@@ -669,13 +680,13 @@ elabTransform info fc safe lhs_in rhs_in
669680 logLvl 3 ("Transform LHS " ++ show clhs_tm)
670681 let rhs = addImplBound i (map fst newargs) rhs_in
671682 ((rhs', defer), _) <-
672− tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []
683+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
673684 (do pbinds lhs_tm
674− erun fc (build i info False [] (UN "transform") rhs)
685+ setNextName
686+ erun fc (build i info False [] (sUN "transform") rhs)
675687 erun fc $ psolve lhs_tm
676688 tt <- get_term
677− let (tm, ds) = runState (collectDeferred Nothing tt) []
678− return (tm, ds))
689+ return (runState (collectDeferred Nothing tt) []))
679690 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
680691 logLvl 3 ("Transform RHS " ++ show crhs_tm)
681692 when safe $ case converts ctxt [] clhs_tm crhs_tm of
@@ -688,7 +699,7 @@ elabTransform info fc safe lhs_in rhs_in
688699elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
689700 PTerm -> String -> Name -> PTerm -> Idris ()
690701elabRecord 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, [])])
692703 cty' <- implicit syn cn cty
693704 i <- getIState
694705 cty <- case lookupTy cn (tt_ctxt i) of
@@ -742,18 +753,18 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
742753 getRecTy (PPi _ n ty s) = getRecTy s
743754 getRecTy t = t
744755
745− rec = MN 0 "rec"
756+ rec = sMN 0 "rec"
746757
747− mkp (UN n) = MN 0 ("p_" ++ n)
748− mkp (MN i n) = MN i ("p_" ++ n)
758+ mkp (UN n) = sMN 0 ("p_" ++ str n)
759+ mkp (MN i n) = sMN i ("p_" ++ str n)
749760 mkp (NS n s) = NS (mkp n) s
750761
751− mkImp (UN n) = UN ("implicit_" ++ n)
752− mkImp (MN i n) = MN i ("implicit_" ++ n)
762+ mkImp (UN n) = sUN ("implicit_" ++ str n)
763+ mkImp (MN i n) = sMN i ("implicit_" ++ str n)
753764 mkImp (NS n s) = NS (mkImp n) s
754765
755− mkType (UN n) = UN ("set_" ++ n)
756− mkType (MN i n) = MN i ("set_" ++ n)
766+ mkType (UN n) = sUN ("set_" ++ str n)
767+ mkType (MN i n) = sMN i ("set_" ++ str n)
757768 mkType (NS n s) = NS (mkType n) s
758769
759770 mkProj recty substs cimp ((pn_in, pty), pos)
@@ -776,11 +787,11 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
776787
777788 mkUpdate recty k num ((pn, pty), pos)
778789 = do let setname = expandNS syn $ mkType pn
779− let valname = MN 0 "updateval"
790+ let valname = sMN 0 "updateval"
780791 let pt = k (PPi expl pn pty
781792 (PPi expl rec recty recty))
782793 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]
784795 let lhsArgs = pls
785796 let rhsArgs = take pos pls ++ (PRef fc valname) :
786797 drop (pos + 1) pls
@@ -795,8 +806,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
795806 return (pn, pfnTy, PClauses fc [] setname [pclause])
796807
797808elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
798− (String, Name, PTerm, FC) -> Idris (Name, Type)
799−elabCon info syn tn codata (doc, n, t_in, fc)
809+ (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)
810+elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
800811 = do checkUndefined fc n
801812 ctxt <- getContext
802813 i <- getIState
@@ -819,7 +830,10 @@ elabCon info syn tn codata (doc, n, t_in, fc)
819830 addIBC (IBCDef n)
820831 addDocStr n doc
821832 addIBC (IBCDoc n)
822− forceArgs tn n cty'
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
836+ forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
823837 return (n, cty')
824838 where
825839 tyIs (Bind n b sc) = tyIs sc
@@ -831,6 +845,11 @@ elabCon info syn tn codata (doc, n, t_in, fc)
831845 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)
832846 mkLazy t = t
833847
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
852+
834853-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
835854-- top-level definition.
836855elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
@@ -1143,7 +1162,7 @@ elabPE info fc caller r =
11431162 _ -> error "Can't happen (getSpecTy)"
11441163
11451164 getSpecClause ist (n, args)
1146− = let newnm = UN ("__"++show (nsroot n) ++ "_" ++
1165+ = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++
11471166 showSep "_" (map showArg args)) in
11481167 -- UN (show n ++ show (map snd args)) in
11491168 (n, newnm, mkPE_TermDecl ist newnm n args)
@@ -1168,8 +1187,8 @@ elabValBind info aspat tm_in
11681187 ((tm', defer, is), _) <-
11691188-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
11701189-- (build i info aspat (MN 0 "val") tm))
1171− tclift (elaborate ctxt (MN 0 "val") infP []
1172− (build i info aspat [Reflection] (MN 0 "val") (infTerm tm)))
1190+ tclift (elaborate ctxt (sMN 0 "val") infP []
1191+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
11731192 let vtm = orderPats (getInferTerm tm')
11741193
11751194 def' <- checkDef (fileFC "(input)") defer
@@ -1199,7 +1218,7 @@ checkPossible info fc tcgen fname lhs_in
11991218 i <- getIState
12001219 let lhs = addImpl i lhs_in
12011220 -- if the LHS type checks, it is possible
1202− case elaborate ctxt (MN 0 "patLHS") infP []
1221+ case elaborate ctxt (sMN 0 "patLHS") infP []
12031222 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
12041223 OK ((lhs', _, _), _) ->
12051224 do let lhs_tm = orderPats (getInferTerm lhs')
@@ -1254,7 +1273,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12541273 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
12551274
12561275 ((lhs', dlhs, []), _) <-
1257− tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1276+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
12581277 (errAt "left hand side of " fname
12591278 (erun fc (buildTC i info True opts fname (infTerm lhs))))
12601279 let lhs_tm = orderPats (getInferTerm lhs')
@@ -1267,8 +1286,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12671286
12681287 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
12691288
1270− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1271− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1289+ rep <- useREPL
1290+ when rep $ do
1291+ addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1292+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
12721293
12731294 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
12741295 -- Elaborate where block
@@ -1296,10 +1317,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12961317 ctxt <- getContext -- new context with where block added
12971318 logLvl 5 "STARTING CHECK"
12981319 ((rhs', defer, is), _) <-
1299− tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
1320+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
13001321 (do pbinds lhs_tm
1322+ setNextName
13011323 (_, _, 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))
13031325 errAt "right hand side of " fname
13041326 (erun fc $ psolve lhs_tm)
13051327 hs <- get_holes
@@ -1326,6 +1348,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13261348
13271349 ctxt <- getContext
13281350 logLvl 5 $ "Rechecking"
1351+ logLvl 6 $ " ==> " ++ show (forget rhs')
13291352 (crhs, crhsty) <- recheckC fc [] rhs'
13301353 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
13311354 case converts ctxt [] clhsty crhsty of
@@ -1431,7 +1454,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14311454 let lhs = addImplPat i (stripLinear i lhs_in)
14321455 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
14331456 ((lhs', dlhs, []), _) <-
1434− tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1457+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
14351458 (errAt "left hand side of with in " fname
14361459 (erun fc (buildTC i info True opts fname (infTerm lhs))) )
14371460 let lhs_tm = orderPats (getInferTerm lhs')
@@ -1445,9 +1468,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14451468 logLvl 5 ("Checking " ++ showImp Nothing True False wval)
14461469 -- Elaborate wval in this context
14471470 ((wval', defer, is), _) <-
1448− tclift $ elaborate ctxt (MN 0 "withRHS")
1471+ tclift $ elaborate ctxt (sMN 0 "withRHS")
14491472 (bindTyArgs PVTy bargs infP) []
14501473 (do pbinds lhs_tm
1474+ setNextName
14511475 -- TODO: may want where here - see winfo abpve
14521476 (_', d, is) <- errAt "with value in " fname
14531477 (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)
14771501 let wargtype = getRetTy cwvaltyN
14781502 logLvl 5 ("Abstract over " ++ show wargval)
14791503 let wtype = bindTyArgs Pi (bargs_pre ++
1480− (MN 0 "warg", wargtype) :
1481− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
1482− (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
1504+ (sMN 0 "warg", wargtype) :
1505+ map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
1506+ (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)
14831507 logLvl 3 ("New function type " ++ show wtype)
1484− let wname = MN windex (show fname)
1508+ let wname = sMN windex (show fname)
14851509
14861510 let imps = getImps wtype -- add to implicits context
14871511 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)
15091533 ctxt <- getContext -- New context with block added
15101534 i <- getIState
15111535 ((rhs', defer, is), _) <-
1512− tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []
1536+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []
15131537 (do pbinds lhs_tm
1538+ setNextName
15141539 (_, d, is) <- erun fc (build i info False opts fname rhs)
15151540 psolve lhs_tm
15161541 tt <- get_term
@@ -1589,7 +1614,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->
15891614 FC -> [PTerm] ->
15901615 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
15911616elabClass 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)
15931618 let tty = pibind ps PType
15941619 let constraint = PApp fc (PRef fc tn)
15951620 (map (pexp . PRef fc) (map fst ps))
@@ -1612,7 +1637,7 @@ elabClass info syn doc fc constraints tn ps ds
16121637 let cty = impbind ps $ conbind constraints
16131638 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
16141639 constraint
1615− let cons = [("", cn, cty, fc)]
1640+ let cons = [("", cn, cty, fc, [])]
16161641 let ddecl = PDatadecl tn tty cons
16171642 logLvl 5 $ "Class data " ++ showDImp True ddecl
16181643 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
16501675
16511676 impbind [] x = x
16521677 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)
16541679 conbind [] x = x
16551680
16561681 getMName (PTy _ _ _ _ n _) = nsroot n
@@ -1674,7 +1699,7 @@ elabClass info syn doc fc constraints tn ps ds
16741699 _ -> ifail $ show n ++ " is not a method"
16751700 defdecl _ _ _ = ifail "Can't happen (defdecl)"
16761701
1677− defaultdec (UN n) = UN ("default#" ++ n)
1702+ defaultdec (UN n) = sUN ("default#" ++ str n)
16781703 defaultdec (NS n ns) = NS (defaultdec n) ns
16791704
16801705 tydecl (PTy _ _ _ _ _ _) = True
@@ -1686,13 +1711,13 @@ elabClass info syn doc fc constraints tn ps ds
16861711
16871712 -- Generate a function for chasing a dictionary constraint
16881713 cfun cn c syn all con
1689− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
1714+ = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)
16901715 -- 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..]
16921717 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
16931718 let lhs = PApp fc (PRef fc cfn) [pconst capp]
16941719 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
16961721 iLOG (showImp Nothing True False ty)
16971722 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
16981723 i <- getIState
@@ -1712,10 +1737,10 @@ elabClass info syn doc fc constraints tn ps ds
17121737 -- dictionary (this is inlinable, always)
17131738 tfun cn c syn all (m, (doc, o, ty))
17141739 = 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..]
17161741 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
17171742 let margs = getMArgs ty
1718− let anames = map (\x -> MN x "arg") [0..]
1743+ let anames = map (\x -> sMN x "arg") [0..]
17191744 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
17201745 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
17211746 iLOG (showImp Nothing True False ty)
@@ -1744,7 +1769,7 @@ elabClass info syn doc fc constraints tn ps ds
17441769
17451770 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
17461771 = 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
17481773
17491774 -- make arguments explicit and don't bind class parameters
17501775 toExp ns e (PPi (Imp l s _ p) n ty sc)
@@ -1754,19 +1779,21 @@ elabClass info syn doc fc constraints tn ps ds
17541779 toExp ns e sc = sc
17551780
17561781elabInstance :: ElabInfo -> SyntaxInfo ->
1782+ ElabWhat -> -- phase
17571783 FC -> [PTerm] -> -- constraints
17581784 Name -> -- the class
17591785 [PTerm] -> -- class parameters (i.e. instance)
17601786 PTerm -> -- full instance type
17611787 Maybe Name -> -- explicit name
17621788 [PDecl] -> Idris ()
1763−elabInstance info syn fc cs n ps t expn ds
1764− = do i <- getIState
1765− (n, ci) <- case lookupCtxtName n (idris_classes i) of
1766− [c] -> return c
1767− _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1768− let constraint = PApp fc (PRef fc n) (map pexp ps)
1769− let iname = mkiname n ps expn
1789+elabInstance info syn what fc cs n ps t expn ds = do
1790+ i <- getIState
1791+ (n, ci) <- case lookupCtxtName n (idris_classes i) of
1792+ [c] -> return c
1793+ _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1794+ let constraint = PApp fc (PRef fc n) (map pexp ps)
1795+ let iname = mkiname n ps expn
1796+ when (what /= EDefns) $ do
17701797 nty <- elabType' True info syn "" fc [] iname t
17711798 -- if the instance type matches any of the instances we have already,
17721799 -- 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
17751802 (class_instances ci)
17761803 addInstance intInst n iname
17771804 Just _ -> addInstance intInst n iname
1805+ when (what /= ETypes) $ do
17781806 let ips = zip (class_params ci) ps
17791807 let ns = case n of
17801808 NS n ns' -> ns'
@@ -1827,7 +1855,7 @@ elabInstance info syn fc cs n ps t expn ds
18271855
18281856 mkiname n' ps' expn' =
18291857 case expn' of
1830− Nothing -> SN (InstanceN n' (map show ps'))
1858+ Nothing -> SN (sInstanceN n' (map show ps'))
18311859 Just nm -> nm
18321860
18331861 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
18751903 mkMethApp (n, _, _, ty)
18761904 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
18771905 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')
18791907 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')
18811909 lamBind i _ sc = sc
18821910 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
18841912 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
18861914 methArgs i (PPi (Constraint _ _ _) n ty sc)
18871915 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
18881916 methArgs i _ = []
@@ -1905,14 +1933,14 @@ elabInstance info syn fc cs n ps t expn ds
19051933
19061934 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
19071935
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)
19091937 conbind [] x = x
19101938
19111939 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
19121940 coninsert cs sc = conbind cs sc
19131941
19141942 insertDefaults :: IState -> Name ->
1915− [(Name, (Name, PDecl))] -> [String] ->
1943+ [(Name, (Name, PDecl))] -> [T.Text] ->
19161944 [PDecl] -> [PDecl]
19171945 insertDefaults i iname [] ns ds = ds
19181946 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
@@ -2034,8 +2062,10 @@ elabDecl' what info d@(PClauses f o n ps)
20342062 [] -> []
20352063 elabClauses info f (o ++ o') n ps
20362064elabDecl' what info (PMutual f ps)
2037− = do mapM_ (elabDecl ETypes info) ps
2038− mapM_ (elabDecl EDefns info) ps
2065+ = do case ps of
2066+ [p] -> elabDecl what info p
2067+ _ -> do mapM_ (elabDecl ETypes info) ps
2068+ mapM_ (elabDecl EDefns info) ps
20392069 -- Do totality checking after entire mutual block
20402070 i <- get
20412071 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
@@ -2071,9 +2101,8 @@ elabDecl' what info (PClass doc s f cs n ps ds)
20712101 = do iLOG $ "Elaborating class " ++ show n
20722102 elabClass info (s { syn_params = [] }) doc f cs n ps ds
20732103elabDecl' what info (PInstance s f cs n ps t expn ds)
2074− | what /= ETypes
20752104 = 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
20772106elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
20782107 | what /= ETypes
20792108 = do iLOG $ "Elaborating record " ++ show tyn