@@ -593,7 +593,7 @@ type ProvideWhat = ProvideWhat' PTerm
593593-- datatypes and typeclasses.
594594data PDecl' t
595595 = PFix FC Fixity [String] -- ^ Fixity declaration
596− | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
596+ | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
597597 | PPostulate Bool -- external def if true
598598 (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
599599 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
@@ -603,30 +603,33 @@ data PDecl' t
603603 | PNamespace String [PDecl' t] -- ^ New namespace
604604 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
605605 Name -- Record name
606− [(Name, Plicity, t)] -- Parameters
606+ FC -- Record name precise location
607+ [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
607608 [(Name, Docstring (Either Err PTerm))] -- Param Docs
608− [((Maybe Name), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
609− (Maybe Name) -- Optional constructor name
609+ [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
610+ (Maybe (Name, FC)) -- Optional constructor name and location
610611 (Docstring (Either Err PTerm)) -- Constructor doc
611612 SyntaxInfo -- Constructor SyntaxInfo
612613 -- ^ Record declaration
613614 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
614615 [(Name, t)] -- constraints
615616 Name -- class name
616− [(Name, t)] -- parameters
617+ FC -- accurate location of class name
618+ [(Name, FC, t)] -- parameters and precise locations
617619 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
618− [Name] -- determining parameters
620+ [(Name, FC)] -- determining parameters and precise locations
619621 [PDecl' t] -- declarations
620− (Maybe Name) -- instance constructor name
622+ (Maybe (Name, FC)) -- instance constructor name and location
621623 (Docstring (Either Err PTerm)) -- instance constructor docs
622624 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
623− -- class name, parameters, method declarations, optional constructor name
625+ -- class name, class name location, parameters, method declarations, optional constructor name
624626 | PInstance
625627 (Docstring (Either Err PTerm)) -- Instance docs
626628 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
627629 SyntaxInfo
628630 FC [(Name, t)] -- constraints
629631 Name -- class
632+ FC -- precise location of class
630633 [t] -- parameters
631634 t -- full instance type
632635 (Maybe Name) -- explicit name
@@ -672,14 +675,19 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
672675data EState = EState {
673676 case_decls :: [(Name, PDecl)],
674677 delayed_elab :: [Elab' EState ()],
675− new_tyDecls :: [RDeclInstructions]
678+ new_tyDecls :: [RDeclInstructions],
679+ highlighting :: [(FC, OutputAnnotation)]
676680 }
677681
678682initEState :: EState
679−initEState = EState [] [] []
683+initEState = EState [] [] [] []
680684
681685type ElabD a = Elab' EState a
682686
687+highlightSource :: FC -> OutputAnnotation -> ElabD ()
688+highlightSource fc annot =
689+ updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
690+
683691-- | One clause of a top-level definition. Term arguments to constructors are:
684692--
685693-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
@@ -690,10 +698,10 @@ type ElabD a = Elab' EState a
690698--
691699-- 4. The where block (PDecl' t)
692700
693−data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
694− | PWith FC Name t [t] t (Maybe Name) [PDecl' t]
695− | PClauseR FC [t] t [PDecl' t]
696− | PWithR FC [t] t (Maybe Name) [PDecl' t]
701+data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
702+ | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
703+ | PClauseR FC [t] t [PDecl' t]
704+ | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
697705 deriving Functor
698706{-!
699707deriving instance Binary PClause'
@@ -702,11 +710,12 @@ deriving instance NFData PClause'
702710
703711-- | Data declaration
704712data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
713+ d_name_fc :: FC, -- ^ The precise location of the type constructor name
705714 d_tcon :: t, -- ^ Type constructor
706− d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
715+ d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
707716 }
708717 -- ^ Data declaration
709− | PLaterdecl { d_name :: Name, d_tcon :: t }
718+ | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
710719 -- ^ "Placeholder" for data whose constructors are defined later
711720 deriving Functor
712721{-!
@@ -725,18 +734,18 @@ type PClause = PClause' PTerm
725734
726735declared :: PDecl -> [Name]
727736declared (PFix _ _ _) = []
728−declared (PTy _ _ _ _ _ n t) = [n]
737+declared (PTy _ _ _ _ _ n fc t) = [n]
729738declared (PPostulate _ _ _ _ _ n t) = [n]
730739declared (PClauses _ _ n _) = [] -- not a declaration
731740declared (PCAF _ n _) = [n]
732−declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
733− where fstt (_, _, a, _, _, _) = a
734−declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
741+declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
742+ where fstt (_, _, a, _, _, _, _) = a
743+declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
735744declared (PParams _ _ ds) = concatMap declared ds
736745declared (PNamespace _ ds) = concatMap declared ds
737−declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
738−declared (PClass _ _ _ _ n _ _ _ ms cn cd) = n : (maybeToList cn ++ concatMap declared ms)
739−declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
746+declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
747+declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
748+declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
740749declared (PDSL n _) = [n]
741750declared (PSyntax _ _) = []
742751declared (PMutual _ ds) = concatMap declared ds
@@ -746,33 +755,33 @@ declared _ = []
746755-- get the names declared, not counting nested parameter blocks
747756tldeclared :: PDecl -> [Name]
748757tldeclared (PFix _ _ _) = []
749−tldeclared (PTy _ _ _ _ _ n t) = [n]
758+tldeclared (PTy _ _ _ _ _ n _ t) = [n]
750759tldeclared (PPostulate _ _ _ _ _ n t) = [n]
751760tldeclared (PClauses _ _ n _) = [] -- not a declaration
752−tldeclared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
753−tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
754− where fstt (_, _, a, _, _, _) = a
761+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
762+tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
763+ where fstt (_, _, a, _, _, _, _) = a
755764tldeclared (PParams _ _ ds) = []
756765tldeclared (PMutual _ ds) = concatMap tldeclared ds
757766tldeclared (PNamespace _ ds) = concatMap tldeclared ds
758−tldeclared (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap tldeclared ms)
759−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []
767+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
768+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
760769tldeclared _ = []
761770
762771defined :: PDecl -> [Name]
763772defined (PFix _ _ _) = []
764−defined (PTy _ _ _ _ _ n t) = []
773+defined (PTy _ _ _ _ _ n _ t) = []
765774defined (PPostulate _ _ _ _ _ n t) = []
766775defined (PClauses _ _ n _) = [n] -- not a declaration
767776defined (PCAF _ n _) = [n]
768−defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
769− where fstt (_, _, a, _, _, _) = a
770−defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
777+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
778+ where fstt (_, _, a, _, _, _, _) = a
779+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
771780defined (PParams _ _ ds) = concatMap defined ds
772781defined (PNamespace _ ds) = concatMap defined ds
773−defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
774−defined (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap defined ms)
775−defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
782+defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
783+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
784+defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
776785defined (PDSL n _) = [n]
777786defined (PSyntax _ _) = []
778787defined (PMutual _ ds) = concatMap defined ds
@@ -807,9 +816,9 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
807816 | PRef FC Name -- ^ A reference to a variable
808817 | PInferRef FC Name -- ^ A name to be defined later
809818 | PPatvar FC Name -- ^ A pattern variable
810− | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
811− | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
812− | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
819+ | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
820+ | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
821+ | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
813822 | PTyped PTerm PTerm -- ^ Term with explicit type
814823 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
815824 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
@@ -825,10 +834,10 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
825834 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
826835 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
827836 | PHidden PTerm -- ^ Irrelevant or hidden pattern
828− | PType -- ^ 'Type' type
837+ | PType FC -- ^ 'Type' type
829838 | PUniverse Universe -- ^ Some universe
830839 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
831− | PConstant Const -- ^ Builtin types
840+ | PConstant FC Const -- ^ Builtin types
832841 | Placeholder -- ^ Underscore
833842 | PDoBlock [PDo] -- ^ Do notation
834843 | PIdiom FC PTerm -- ^ Idiom brackets
@@ -856,9 +865,9 @@ deriving instance NFData PTerm
856865
857866mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
858867mapPT f t = f (mpt t) where
859− mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
860− mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
861− mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
868+ mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
869+ mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
870+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
862871 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
863872 (fmap (mapPT f) g)
864873 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
@@ -945,9 +954,9 @@ instance Sized a => Sized (PTactic' a) where
945954type PTactic = PTactic' PTerm
946955
947956data PDo' t = DoExp FC t
948− | DoBind FC Name t
957+ | DoBind FC Name FC t -- ^ second FC is precise name location
949958 | DoBindP FC t t [(t,t)]
950− | DoLet FC Name t t
959+ | DoLet FC Name FC t t -- ^ second FC is precise name location
951960 | DoLetP FC t t
952961 deriving (Eq, Functor, Data, Typeable)
953962{-!
@@ -957,9 +966,9 @@ deriving instance NFData PDo'
957966
958967instance Sized a => Sized (PDo' a) where
959968 size (DoExp fc t) = 1 + size fc + size t
960− size (DoBind fc nm t) = 1 + size fc + size nm + size t
969+ size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
961970 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
962− size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
971+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
963972 size (DoLetP fc l r) = 1 + size fc + size l + size r
964973
965974type PDo = PDo' PTerm
@@ -1014,9 +1023,9 @@ highestFC (PQuote _) = Nothing
10141023highestFC (PRef fc _) = Just fc
10151024highestFC (PInferRef fc _) = Just fc
10161025highestFC (PPatvar fc _) = Just fc
1017−highestFC (PLam fc _ _ _) = Just fc
1018−highestFC (PPi _ _ _ _) = Nothing
1019−highestFC (PLet fc _ _ _ _) = Just fc
1026+highestFC (PLam fc _ _ _ _) = Just fc
1027+highestFC (PPi _ _ _ _ _) = Nothing
1028+highestFC (PLet fc _ _ _ _ _) = Just fc
10201029highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
10211030highestFC (PApp fc _ _) = Just fc
10221031highestFC (PAppBind fc _ _) = Just fc
@@ -1034,10 +1043,10 @@ highestFC (PAlternative _ args) =
10341043 [] -> Nothing
10351044 (fc:_) -> Just fc
10361045highestFC (PHidden _) = Nothing
1037−highestFC PType = Nothing
1046+highestFC (PType fc) = Just fc
10381047highestFC (PUniverse _) = Nothing
10391048highestFC (PGoal fc _ _ _) = Just fc
1040−highestFC (PConstant _) = Nothing
1049+highestFC (PConstant fc _) = Just fc
10411050highestFC Placeholder = Nothing
10421051highestFC (PDoBlock lines) =
10431052 case map getDoFC lines of
@@ -1045,9 +1054,9 @@ highestFC (PDoBlock lines) =
10451054 (fc:_) -> Just fc
10461055 where
10471056 getDoFC (DoExp fc t) = fc
1048− getDoFC (DoBind fc nm t) = fc
1057+ getDoFC (DoBind fc nm nfc t) = fc
10491058 getDoFC (DoBindP fc l r alts) = fc
1050− getDoFC (DoLet fc nm l r) = fc
1059+ getDoFC (DoLet fc nm nfc l r) = fc
10511060 getDoFC (DoLetP fc l r) = fc
10521061
10531062highestFC (PIdiom fc _) = Just fc
@@ -1252,10 +1261,10 @@ bi = fileFC "builtin"
12521261
12531262inferTy = sMN 0 "__Infer"
12541263inferCon = sMN 0 "__infer"
1255−inferDecl = PDatadecl inferTy
1256− PType
1257− [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1258− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1264+inferDecl = PDatadecl inferTy NoFC
1265+ (PType bi)
1266+ [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1267+ PPi expl (sMN 0 "ival") NoFC (PRef bi (sMN 0 "iType"))
12591268 (PRef bi inferTy)), bi, [])]
12601269inferOpts = []
12611270
@@ -1309,16 +1318,16 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
13091318 "\n\n" ++
13101319 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
13111320
1312−eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1313− (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1314− PType))
1321+eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1322+ (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1323+ (PType bi)))
13151324 [(reflDoc, reflParamDoc,
1316− eqCon, PPi impl (n "A") PType (
1317− PPi impl (n "x") (PRef bi (n "A"))
1318− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1319− pimp (n "B") Placeholder False,
1320− pexp (PRef bi (n "x")),
1321− pexp (PRef bi (n "x"))])), bi, [])]
1325+ eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1326+ PPi impl (n "x") NoFC (PRef bi (n "A"))
1327+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1328+ pimp (n "B") Placeholder False,
1329+ pexp (PRef bi (n "x")),
1330+ pexp (PRef bi (n "x"))])), bi, [])]
13221331 where n a = sUN a
13231332 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
13241333 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
@@ -1348,7 +1357,7 @@ piBind = piBindp expl
13481357
13491358piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
13501359piBindp p [] t = t
1351−piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1360+piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
13521361
13531362
13541363-- Pretty-printing declarations and terms
@@ -1437,15 +1446,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14371446 | Just str <- slist p bnd e = str
14381447 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
14391448 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1440− prettySe p bnd (PLam fc n ty sc) =
1449+ prettySe p bnd (PLam fc n nfc ty sc) =
14411450 bracket p startPrec . group . align . hang 2 $
14421451 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
14431452 prettySe startPrec ((n, False):bnd) sc
1444− prettySe p bnd (PLet fc n ty v sc) =
1453+ prettySe p bnd (PLet fc n nfc ty v sc) =
14451454 bracket p startPrec . group . align $
14461455 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
14471456 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1448− prettySe p bnd (PPi (Exp l s _) n ty sc)
1457+ prettySe p bnd (PPi (Exp l s _) n _ ty sc)
14491458 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
14501459 bracket p startPrec . group $
14511460 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
@@ -1458,7 +1467,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14581467 case s of
14591468 Static -> text "[static]" <> space
14601469 _ -> empty
1461− prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1470+ prettySe p bnd (PPi (Imp l s _ fa) n _ ty sc)
14621471 | ppopt_impl ppo =
14631472 bracket p startPrec $
14641473 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
@@ -1469,10 +1478,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14691478 case s of
14701479 Static -> text "[static]" <> space
14711480 _ -> empty
1472− prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1481+ prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
14731482 bracket p startPrec $
14741483 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1475− prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1484+ prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
14761485 bracket p startPrec $
14771486 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
14781487 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
@@ -1525,7 +1534,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
15251534 (prettySe left bnd l <+> opName False) <$>
15261535 group (prettySe right bnd r)
15271536 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1528− | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1537+ | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
15291538 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
15301539 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
15311540 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
@@ -1601,9 +1610,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16011610 where
16021611 prettyAs =
16031612 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1604− prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1613+ prettySe p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
16051614 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1606− prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1615+ prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
16071616 -- XXX: add pretty for tactics
16081617 prettySe p bnd (PProof ts) =
16091618 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
@@ -1763,24 +1772,24 @@ showCImp ppo (PWith _ n l ws r pn w)
17631772
17641773
17651774showDImp :: PPOption -> PData -> Doc OutputAnnotation
1766−showDImp ppo (PDatadecl n ty cons)
1775+showDImp ppo (PDatadecl n nfc ty cons)
17671776 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1768− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1777+ (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
17691778
17701779showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
17711780showDecls o ds = vsep (map (showDeclImp o) ds)
17721781
17731782showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1774−showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1783+showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
17751784showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
17761785 indent 2 (vsep (map (showCImp o) cs))
17771786showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
17781787showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
17791788showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
17801789showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1781−showDeclImp o (PClass _ _ _ cs n ps _ _ ds _ _)
1790+showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
17821791 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1783−showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)
1792+showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
17841793 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
17851794showDeclImp _ _ = text "..."
17861795-- showDeclImp (PImport o) = "import " ++ o
@@ -1857,9 +1866,9 @@ showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
18571866instance Sized PTerm where
18581867 size (PQuote rawTerm) = size rawTerm
18591868 size (PRef fc name) = size name
1860− size (PLam fc name ty bdy) = 1 + size ty + size bdy
1861− size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1862− size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1869+ size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
1870+ size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
1871+ size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
18631872 size (PTyped trm ty) = 1 + size trm + size ty
18641873 size (PApp fc name args) = 1 + size args
18651874 size (PAppBind fc name args) = 1 + size args
@@ -1875,9 +1884,9 @@ instance Sized PTerm where
18751884 size (PUnifyLog tm) = size tm
18761885 size (PDisamb _ tm) = size tm
18771886 size (PNoImplicits tm) = size tm
1878− size PType = 1
1887+ size (PType _) = 1
18791888 size (PUniverse _) = 1
1880− size (PConstant const) = 1 + size const
1889+ size (PConstant fc const) = 1 + size fc + size const
18811890 size Placeholder = 1
18821891 size (PDoBlock dos) = 1 + size dos
18831892 size (PIdiom fc term) = 1 + size term
@@ -1889,7 +1898,7 @@ instance Sized PTerm where
18891898 size _ = 0
18901899
18911900getPArity :: PTerm -> Int
1892−getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1901+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
18931902getPArity _ = 0
18941903
18951904-- Return all names, free or globally bound, in the given term.
@@ -1904,8 +1913,8 @@ allNamesIn tm = nub $ ni [] tm
19041913 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
19051914 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
19061915 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
1907− ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1908− ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1916+ ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
1917+ ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
19091918 ni env (PHidden tm) = ni env tm
19101919 ni env (PRewrite _ l r _) = ni env l ++ ni env r
19111920 ni env (PTyped l r) = ni env l ++ ni env r
@@ -1930,9 +1939,9 @@ boundNamesIn tm = S.toList (ni S.empty tm)
19301939 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
19311940 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
19321941 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
1933− ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc
1934− ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
1935− ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
1942+ ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
1943+ ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
1944+ ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
19361945 ni set (PRewrite _ l r _) = ni (ni set l) r
19371946 ni set (PTyped l r) = ni (ni set l) r
19381947 ni set (PPair _ _ l r) = ni (ni set l) r
@@ -1970,8 +1979,8 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm
19701979 (nub (concatMap (ni env) (map snd os))
19711980 \\ nub (concatMap (ni env) (map fst os)))
19721981 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
1973− ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1974− ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1982+ ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
1983+ ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
19751984 ni env (PRewrite _ l r _) = ni env l ++ ni env r
19761985 ni env (PTyped l r) = ni env l ++ ni env r
19771986 ni env (PPair _ _ l r) = ni env l ++ ni env r
@@ -2000,8 +2009,8 @@ namesIn uvars ist tm = nub $ ni [] tm
20002009 (nub (concatMap (ni env) (map snd os))
20012010 \\ nub (concatMap (ni env) (map fst os)))
20022011 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2003− ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
2004− ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2012+ ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2013+ ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
20052014 ni env (PRewrite _ l r _) = ni env l ++ ni env r
20062015 ni env (PTyped l r) = ni env l ++ ni env r
20072016 ni env (PPair _ _ l r) = ni env l ++ ni env r
@@ -2031,8 +2040,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm
20312040 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
20322041 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
20332042 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2034− ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
2035− ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2043+ ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2044+ ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
20362045 ni env (PRewrite _ l r _) = ni env l ++ ni env r
20372046 ni env (PTyped l r) = ni env l ++ ni env r
20382047 ni env (PPair _ _ l r) = ni env l ++ ni env r