@@ -593,7 +593,7 @@ type ProvideWhat = ProvideWhat' PTerm
593-- datatypes and typeclasses.
593-- datatypes and typeclasses.
594data PDecl' t
594data PDecl' t
595 = PFix FC Fixity [String] -- ^ Fixity declaration
595 = 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)
597 | PPostulate Bool -- external def if true
597 | PPostulate Bool -- external def if true
598 (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
598 (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
599 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
599 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
@@ -603,30 +603,33 @@ data PDecl' t
603 | PNamespace String [PDecl' t] -- ^ New namespace
603 | PNamespace String [PDecl' t] -- ^ New namespace
604 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
604 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
605 Name -- Record name
605 Name -- Record name
606+ FC -- Record name precise location
606− [(Name, Plicity, t)] -- Parameters
607+ [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
607 [(Name, Docstring (Either Err PTerm))] -- Param Docs
608 [(Name, Docstring (Either Err PTerm))] -- Param Docs
608− [((Maybe Name), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
609+ [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
609− (Maybe Name) -- Optional constructor name
610+ (Maybe (Name, FC)) -- Optional constructor name and location
610 (Docstring (Either Err PTerm)) -- Constructor doc
611 (Docstring (Either Err PTerm)) -- Constructor doc
611 SyntaxInfo -- Constructor SyntaxInfo
612 SyntaxInfo -- Constructor SyntaxInfo
612 -- ^ Record declaration
613 -- ^ Record declaration
613 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
614 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
614 [(Name, t)] -- constraints
615 [(Name, t)] -- constraints
615 Name -- class name
616 Name -- class name
617+ FC -- accurate location of class name
616− [(Name, t)] -- parameters
618+ [(Name, FC, t)] -- parameters and precise locations
617 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
619 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
618− [Name] -- determining parameters
620+ [(Name, FC)] -- determining parameters and precise locations
619 [PDecl' t] -- declarations
621 [PDecl' t] -- declarations
620− (Maybe Name) -- instance constructor name
622+ (Maybe (Name, FC)) -- instance constructor name and location
621 (Docstring (Either Err PTerm)) -- instance constructor docs
623 (Docstring (Either Err PTerm)) -- instance constructor docs
622 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
624 -- ^ 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
624 | PInstance
626 | PInstance
625 (Docstring (Either Err PTerm)) -- Instance docs
627 (Docstring (Either Err PTerm)) -- Instance docs
626 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
628 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
627 SyntaxInfo
629 SyntaxInfo
628 FC [(Name, t)] -- constraints
630 FC [(Name, t)] -- constraints
629 Name -- class
631 Name -- class
632+ FC -- precise location of class
630 [t] -- parameters
633 [t] -- parameters
631 t -- full instance type
634 t -- full instance type
632 (Maybe Name) -- explicit name
635 (Maybe Name) -- explicit name
@@ -672,14 +675,19 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
672data EState = EState {
675data EState = EState {
673 case_decls :: [(Name, PDecl)],
676 case_decls :: [(Name, PDecl)],
674 delayed_elab :: [Elab' EState ()],
677 delayed_elab :: [Elab' EState ()],
675− new_tyDecls :: [RDeclInstructions]
678+ new_tyDecls :: [RDeclInstructions],
679+ highlighting :: [(FC, OutputAnnotation)]
678initEState :: EState
682initEState :: EState
679−initEState = EState [] [] []
683+initEState = EState [] [] [] []
681type ElabD a = Elab' EState a
685type ElabD a = Elab' EState a
687+highlightSource :: FC -> OutputAnnotation -> ElabD ()
688+highlightSource fc annot =
689+ updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
683-- | One clause of a top-level definition. Term arguments to constructors are:
691-- | One clause of a top-level definition. Term arguments to constructors are:
685-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
693-- 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
691-- 4. The where block (PDecl' t)
699-- 4. The where block (PDecl' t)
693−data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
701+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]
702+ | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
695− | PClauseR FC [t] t [PDecl' t]
703+ | PClauseR FC [t] t [PDecl' t]
696− | PWithR FC [t] t (Maybe Name) [PDecl' t]
704+ | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
697 deriving Functor
705 deriving Functor
699deriving instance Binary PClause'
707deriving instance Binary PClause'
@@ -702,11 +710,12 @@ deriving instance NFData PClause'
703-- | Data declaration
711-- | Data declaration
704data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
712data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
713+ d_name_fc :: FC, -- ^ The precise location of the type constructor name
705 d_tcon :: t, -- ^ Type constructor
714 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
708 -- ^ Data declaration
717 -- ^ Data declaration
709− | PLaterdecl { d_name :: Name, d_tcon :: t }
718+ | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
710 -- ^ "Placeholder" for data whose constructors are defined later
719 -- ^ "Placeholder" for data whose constructors are defined later
711 deriving Functor
720 deriving Functor
@@ -725,18 +734,18 @@ type PClause = PClause' PTerm
726declared :: PDecl -> [Name]
735declared :: PDecl -> [Name]
727declared (PFix _ _ _) = []
736declared (PFix _ _ _) = []
728−declared (PTy _ _ _ _ _ n t) = [n]
737+declared (PTy _ _ _ _ _ n fc t) = [n]
729declared (PPostulate _ _ _ _ _ n t) = [n]
738declared (PPostulate _ _ _ _ _ n t) = [n]
730declared (PClauses _ _ n _) = [] -- not a declaration
739declared (PClauses _ _ n _) = [] -- not a declaration
731declared (PCAF _ n _) = [n]
740declared (PCAF _ n _) = [n]
732−declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
741+declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
733− where fstt (_, _, a, _, _, _) = a
742+ where fstt (_, _, a, _, _, _, _) = a
734−declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
743+declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
735declared (PParams _ _ ds) = concatMap declared ds
744declared (PParams _ _ ds) = concatMap declared ds
736declared (PNamespace _ ds) = concatMap declared ds
745declared (PNamespace _ ds) = concatMap declared ds
737−declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
746+declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
738−declared (PClass _ _ _ _ n _ _ _ ms cn cd) = n : (maybeToList cn ++ concatMap declared ms)
747+declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
739−declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
748+declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
740declared (PDSL n _) = [n]
749declared (PDSL n _) = [n]
741declared (PSyntax _ _) = []
750declared (PSyntax _ _) = []
742declared (PMutual _ ds) = concatMap declared ds
751declared (PMutual _ ds) = concatMap declared ds
@@ -746,33 +755,33 @@ declared _ = []
746-- get the names declared, not counting nested parameter blocks
755-- get the names declared, not counting nested parameter blocks
747tldeclared :: PDecl -> [Name]
756tldeclared :: PDecl -> [Name]
748tldeclared (PFix _ _ _) = []
757tldeclared (PFix _ _ _) = []
749−tldeclared (PTy _ _ _ _ _ n t) = [n]
758+tldeclared (PTy _ _ _ _ _ n _ t) = [n]
750tldeclared (PPostulate _ _ _ _ _ n t) = [n]
759tldeclared (PPostulate _ _ _ _ _ n t) = [n]
751tldeclared (PClauses _ _ n _) = [] -- not a declaration
760tldeclared (PClauses _ _ n _) = [] -- not a declaration
752−tldeclared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
761+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
753−tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
762+tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
754− where fstt (_, _, a, _, _, _) = a
763+ where fstt (_, _, a, _, _, _, _) = a
755tldeclared (PParams _ _ ds) = []
764tldeclared (PParams _ _ ds) = []
756tldeclared (PMutual _ ds) = concatMap tldeclared ds
765tldeclared (PMutual _ ds) = concatMap tldeclared ds
757tldeclared (PNamespace _ ds) = concatMap tldeclared ds
766tldeclared (PNamespace _ ds) = concatMap tldeclared ds
758−tldeclared (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap tldeclared ms)
767+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
759−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []
768+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
760tldeclared _ = []
769tldeclared _ = []
762defined :: PDecl -> [Name]
771defined :: PDecl -> [Name]
763defined (PFix _ _ _) = []
772defined (PFix _ _ _) = []
764−defined (PTy _ _ _ _ _ n t) = []
773+defined (PTy _ _ _ _ _ n _ t) = []
765defined (PPostulate _ _ _ _ _ n t) = []
774defined (PPostulate _ _ _ _ _ n t) = []
766defined (PClauses _ _ n _) = [n] -- not a declaration
775defined (PClauses _ _ n _) = [n] -- not a declaration
767defined (PCAF _ n _) = [n]
776defined (PCAF _ n _) = [n]
768−defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
777+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
769− where fstt (_, _, a, _, _, _) = a
778+ where fstt (_, _, a, _, _, _, _) = a
770−defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
779+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
771defined (PParams _ _ ds) = concatMap defined ds
780defined (PParams _ _ ds) = concatMap defined ds
772defined (PNamespace _ ds) = concatMap defined ds
781defined (PNamespace _ ds) = concatMap defined ds
773−defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
782+defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
774−defined (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap defined ms)
783+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
775−defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
784+defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
776defined (PDSL n _) = [n]
785defined (PDSL n _) = [n]
777defined (PSyntax _ _) = []
786defined (PSyntax _ _) = []
778defined (PMutual _ ds) = concatMap defined ds
787defined (PMutual _ ds) = concatMap defined ds
@@ -807,9 +816,9 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
807 | PRef FC Name -- ^ A reference to a variable
816 | PRef FC Name -- ^ A reference to a variable
808 | PInferRef FC Name -- ^ A name to be defined later
817 | PInferRef FC Name -- ^ A name to be defined later
809 | PPatvar FC Name -- ^ A pattern variable
818 | PPatvar FC Name -- ^ A pattern variable
810− | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
819+ | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
811− | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
820+ | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
812− | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
821+ | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
813 | PTyped PTerm PTerm -- ^ Term with explicit type
822 | PTyped PTerm PTerm -- ^ Term with explicit type
814 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
823 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
815 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
824 | 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
825 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
834 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
826 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
835 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
827 | PHidden PTerm -- ^ Irrelevant or hidden pattern
836 | PHidden PTerm -- ^ Irrelevant or hidden pattern
828− | PType -- ^ 'Type' type
837+ | PType FC -- ^ 'Type' type
829 | PUniverse Universe -- ^ Some universe
838 | PUniverse Universe -- ^ Some universe
830 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
839 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
831− | PConstant Const -- ^ Builtin types
840+ | PConstant FC Const -- ^ Builtin types
832 | Placeholder -- ^ Underscore
841 | Placeholder -- ^ Underscore
833 | PDoBlock [PDo] -- ^ Do notation
842 | PDoBlock [PDo] -- ^ Do notation
834 | PIdiom FC PTerm -- ^ Idiom brackets
843 | PIdiom FC PTerm -- ^ Idiom brackets
@@ -856,9 +865,9 @@ deriving instance NFData PTerm
857mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
866mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
858mapPT f t = f (mpt t) where
867mapPT f t = f (mpt t) where
859− mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
868+ mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
860− mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
869+ mpt (PPi p n nfc t s) = PPi p n nfc (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)
870+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
862 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
871 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
863 (fmap (mapPT f) g)
872 (fmap (mapPT f) g)
864 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
873 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
945type PTactic = PTactic' PTerm
954type PTactic = PTactic' PTerm
947data PDo' t = DoExp FC t
956data PDo' t = DoExp FC t
948− | DoBind FC Name t
957+ | DoBind FC Name FC t -- ^ second FC is precise name location
949 | DoBindP FC t t [(t,t)]
958 | 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
951 | DoLetP FC t t
960 | DoLetP FC t t
952 deriving (Eq, Functor, Data, Typeable)
961 deriving (Eq, Functor, Data, Typeable)
@@ -957,9 +966,9 @@ deriving instance NFData PDo'
958instance Sized a => Sized (PDo' a) where
967instance Sized a => Sized (PDo' a) where
959 size (DoExp fc t) = 1 + size fc + size t
968 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
961 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
970 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
963 size (DoLetP fc l r) = 1 + size fc + size l + size r
972 size (DoLetP fc l r) = 1 + size fc + size l + size r
965type PDo = PDo' PTerm
974type PDo = PDo' PTerm
@@ -1014,9 +1023,9 @@ highestFC (PQuote _) = Nothing
1014highestFC (PRef fc _) = Just fc
1023highestFC (PRef fc _) = Just fc
1015highestFC (PInferRef fc _) = Just fc
1024highestFC (PInferRef fc _) = Just fc
1016highestFC (PPatvar fc _) = Just fc
1025highestFC (PPatvar fc _) = Just fc
1017−highestFC (PLam fc _ _ _) = Just fc
1026+highestFC (PLam fc _ _ _ _) = Just fc
1018−highestFC (PPi _ _ _ _) = Nothing
1027+highestFC (PPi _ _ _ _ _) = Nothing
1019−highestFC (PLet fc _ _ _ _) = Just fc
1028+highestFC (PLet fc _ _ _ _ _) = Just fc
1020highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1029highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1021highestFC (PApp fc _ _) = Just fc
1030highestFC (PApp fc _ _) = Just fc
1022highestFC (PAppBind fc _ _) = Just fc
1031highestFC (PAppBind fc _ _) = Just fc
@@ -1034,10 +1043,10 @@ highestFC (PAlternative _ args) =
1034 [] -> Nothing
1043 [] -> Nothing
1035 (fc:_) -> Just fc
1044 (fc:_) -> Just fc
1036highestFC (PHidden _) = Nothing
1045highestFC (PHidden _) = Nothing
1037−highestFC PType = Nothing
1046+highestFC (PType fc) = Just fc
1038highestFC (PUniverse _) = Nothing
1047highestFC (PUniverse _) = Nothing
1039highestFC (PGoal fc _ _ _) = Just fc
1048highestFC (PGoal fc _ _ _) = Just fc
1040−highestFC (PConstant _) = Nothing
1049+highestFC (PConstant fc _) = Just fc
1041highestFC Placeholder = Nothing
1050highestFC Placeholder = Nothing
1042highestFC (PDoBlock lines) =
1051highestFC (PDoBlock lines) =
1043 case map getDoFC lines of
1052 case map getDoFC lines of
@@ -1045,9 +1054,9 @@ highestFC (PDoBlock lines) =
1045 (fc:_) -> Just fc
1054 (fc:_) -> Just fc
1047 getDoFC (DoExp fc t) = fc
1056 getDoFC (DoExp fc t) = fc
1048− getDoFC (DoBind fc nm t) = fc
1057+ getDoFC (DoBind fc nm nfc t) = fc
1049 getDoFC (DoBindP fc l r alts) = fc
1058 getDoFC (DoBindP fc l r alts) = fc
1050− getDoFC (DoLet fc nm l r) = fc
1059+ getDoFC (DoLet fc nm nfc l r) = fc
1051 getDoFC (DoLetP fc l r) = fc
1060 getDoFC (DoLetP fc l r) = fc
1053highestFC (PIdiom fc _) = Just fc
1062highestFC (PIdiom fc _) = Just fc
@@ -1252,10 +1261,10 @@ bi = fileFC "builtin"
1253inferTy = sMN 0 "__Infer"
1262inferTy = sMN 0 "__Infer"
1254inferCon = sMN 0 "__infer"
1263inferCon = sMN 0 "__infer"
1255−inferDecl = PDatadecl inferTy
1264+inferDecl = PDatadecl inferTy NoFC
1256− PType
1265+ (PType bi)
1257− [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1266+ [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1258− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1267+ PPi expl (sMN 0 "ival") NoFC (PRef bi (sMN 0 "iType"))
1259 (PRef bi inferTy)), bi, [])]
1268 (PRef bi inferTy)), bi, [])]
1260inferOpts = []
1269inferOpts = []
@@ -1309,16 +1318,16 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1309 "\n\n" ++
1318 "\n\n" ++
1310 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1319 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1312−eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1321+eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1313− (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1322+ (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1314− PType))
1323+ (PType bi)))
1315 [(reflDoc, reflParamDoc,
1324 [(reflDoc, reflParamDoc,
1316− eqCon, PPi impl (n "A") PType (
1325+ eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1317− PPi impl (n "x") (PRef bi (n "A"))
1326+ PPi impl (n "x") NoFC (PRef bi (n "A"))
1318− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1327+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1319− pimp (n "B") Placeholder False,
1328+ pimp (n "B") Placeholder False,
1320− pexp (PRef bi (n "x")),
1329+ pexp (PRef bi (n "x")),
1321− pexp (PRef bi (n "x"))])), bi, [])]
1330+ pexp (PRef bi (n "x"))])), bi, [])]
1322 where n a = sUN a
1331 where n a = sUN a
1323 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1332 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1324 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1333 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
@@ -1348,7 +1357,7 @@ piBind = piBindp expl
1349piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1358piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1350piBindp p [] t = t
1359piBindp 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)
1354-- Pretty-printing declarations and terms
1363-- Pretty-printing declarations and terms
@@ -1437,15 +1446,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1437 | Just str <- slist p bnd e = str
1446 | Just str <- slist p bnd e = str
1438 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1447 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1439 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1448 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) =
1441 bracket p startPrec . group . align . hang 2 $
1450 bracket p startPrec . group . align . hang 2 $
1442 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1451 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1443 prettySe startPrec ((n, False):bnd) sc
1452 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) =
1445 bracket p startPrec . group . align $
1454 bracket p startPrec . group . align $
1446 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1455 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1447 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1456 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)
1449 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1458 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1450 bracket p startPrec . group $
1459 bracket p startPrec . group $
1451 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1460 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
1458 case s of
1467 case s of
1459 Static -> text "[static]" <> space
1468 Static -> text "[static]" <> space
1460 _ -> empty
1469 _ -> 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)
1462 | ppopt_impl ppo =
1471 | ppopt_impl ppo =
1463 bracket p startPrec $
1472 bracket p startPrec $
1464 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1473 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
@@ -1469,10 +1478,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1469 case s of
1478 case s of
1470 Static -> text "[static]" <> space
1479 Static -> text "[static]" <> space
1471 _ -> empty
1480 _ -> empty
1472− prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1481+ prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
1473 bracket p startPrec $
1482 bracket p startPrec $
1474 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1483 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) =
1476 bracket p startPrec $
1485 bracket p startPrec $
1477 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1486 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1478 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1487 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
@@ -1525,7 +1534,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1525 (prettySe left bnd l <+> opName False) <$>
1534 (prettySe left bnd l <+> opName False) <$>
1526 group (prettySe right bnd r)
1535 group (prettySe right bnd r)
1527 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1536 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,
1529 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1538 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1530 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1539 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1531 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1540 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
@@ -1601,9 +1610,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1602 prettyAs =
1611 prettyAs =
1603 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1612 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"
1605 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1614 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))
1607 -- XXX: add pretty for tactics
1616 -- XXX: add pretty for tactics
1608 prettySe p bnd (PProof ts) =
1617 prettySe p bnd (PProof ts) =
1609 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1618 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
@@ -1763,24 +1772,24 @@ showCImp ppo (PWith _ n l ws r pn w)
1765showDImp :: PPOption -> PData -> Doc OutputAnnotation
1774showDImp :: PPOption -> PData -> Doc OutputAnnotation
1766−showDImp ppo (PDatadecl n ty cons)
1775+showDImp ppo (PDatadecl n nfc ty cons)
1767 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1776 = 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))
1770showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1779showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1771showDecls o ds = vsep (map (showDeclImp o) ds)
1780showDecls o ds = vsep (map (showDeclImp o) ds)
1773showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1782showDeclImp _ (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
1775showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1784showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1776 indent 2 (vsep (map (showCImp o) cs))
1785 indent 2 (vsep (map (showCImp o) cs))
1777showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1786showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1778showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1787showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1779showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1788showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1780showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1789showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1781−showDeclImp o (PClass _ _ _ cs n ps _ _ ds _ _)
1790+showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
1782 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1791 = 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)
1784 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1793 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1785showDeclImp _ _ = text "..."
1794showDeclImp _ _ = text "..."
1786-- showDeclImp (PImport o) = "import " ++ o
1795-- showDeclImp (PImport o) = "import " ++ o
@@ -1857,9 +1866,9 @@ showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1857instance Sized PTerm where
1866instance Sized PTerm where
1858 size (PQuote rawTerm) = size rawTerm
1867 size (PQuote rawTerm) = size rawTerm
1859 size (PRef fc name) = size name
1868 size (PRef fc name) = size name
1860− size (PLam fc name ty bdy) = 1 + size ty + size bdy
1869+ size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
1861− size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1870+ size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
1862− size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1871+ size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
1863 size (PTyped trm ty) = 1 + size trm + size ty
1872 size (PTyped trm ty) = 1 + size trm + size ty
1864 size (PApp fc name args) = 1 + size args
1873 size (PApp fc name args) = 1 + size args
1865 size (PAppBind fc name args) = 1 + size args
1874 size (PAppBind fc name args) = 1 + size args
@@ -1875,9 +1884,9 @@ instance Sized PTerm where
1875 size (PUnifyLog tm) = size tm
1884 size (PUnifyLog tm) = size tm
1876 size (PDisamb _ tm) = size tm
1885 size (PDisamb _ tm) = size tm
1877 size (PNoImplicits tm) = size tm
1886 size (PNoImplicits tm) = size tm
1878− size PType = 1
1887+ size (PType _) = 1
1879 size (PUniverse _) = 1
1888 size (PUniverse _) = 1
1880− size (PConstant const) = 1 + size const
1889+ size (PConstant fc const) = 1 + size fc + size const
1881 size Placeholder = 1
1890 size Placeholder = 1
1882 size (PDoBlock dos) = 1 + size dos
1891 size (PDoBlock dos) = 1 + size dos
1883 size (PIdiom fc term) = 1 + size term
1892 size (PIdiom fc term) = 1 + size term
@@ -1889,7 +1898,7 @@ instance Sized PTerm where
1889 size _ = 0
1898 size _ = 0
1891getPArity :: PTerm -> Int
1900getPArity :: PTerm -> Int
1892−getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1901+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
1893getPArity _ = 0
1902getPArity _ = 0
1895-- Return all names, free or globally bound, in the given term.
1904-- Return all names, free or globally bound, in the given term.
@@ -1904,8 +1913,8 @@ allNamesIn tm = nub $ ni [] tm
1904 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1913 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1905 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1914 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1906 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
1915 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
1916+ 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
1917+ ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1909 ni env (PHidden tm) = ni env tm
1918 ni env (PHidden tm) = ni env tm
1910 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1919 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1911 ni env (PTyped l r) = ni env l ++ ni env r
1920 ni env (PTyped l r) = ni env l ++ ni env r
@@ -1930,9 +1939,9 @@ boundNamesIn tm = S.toList (ni S.empty tm)
1930 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
1939 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
1931 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
1940 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
1932 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
1941 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
1942+ 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
1943+ ni set (PLet fc n nfc 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
1944+ ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
1936 ni set (PRewrite _ l r _) = ni (ni set l) r
1945 ni set (PRewrite _ l r _) = ni (ni set l) r
1937 ni set (PTyped l r) = ni (ni set l) r
1946 ni set (PTyped l r) = ni (ni set l) r
1938 ni set (PPair _ _ l r) = ni (ni set l) r
1947 ni set (PPair _ _ l r) = ni (ni set l) r
@@ -1970,8 +1979,8 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm
1970 (nub (concatMap (ni env) (map snd os))
1979 (nub (concatMap (ni env) (map snd os))
1971 \\ nub (concatMap (ni env) (map fst os)))
1980 \\ nub (concatMap (ni env) (map fst os)))
1972 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
1981 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
1982+ 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
1983+ ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
1975 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1984 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1976 ni env (PTyped l r) = ni env l ++ ni env r
1985 ni env (PTyped l r) = ni env l ++ ni env r
1977 ni env (PPair _ _ l r) = ni env l ++ ni env r
1986 ni env (PPair _ _ l r) = ni env l ++ ni env r
@@ -2000,8 +2009,8 @@ namesIn uvars ist tm = nub $ ni [] tm
2000 (nub (concatMap (ni env) (map snd os))
2009 (nub (concatMap (ni env) (map snd os))
2001 \\ nub (concatMap (ni env) (map fst os)))
2010 \\ nub (concatMap (ni env) (map fst os)))
2002 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2011 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
2012+ ni env (PLam fc n nfc 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
2013+ ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2005 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2014 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2006 ni env (PTyped l r) = ni env l ++ ni env r
2015 ni env (PTyped l r) = ni env l ++ ni env r
2007 ni env (PPair _ _ l r) = ni env l ++ ni env r
2016 ni env (PPair _ _ l r) = ni env l ++ ni env r
@@ -2031,8 +2040,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm
2031 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2040 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2032 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2041 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2033 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2042 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
2043+ 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
2044+ ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2036 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2045 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2037 ni env (PTyped l r) = ni env l ++ ni env r
2046 ni env (PTyped l r) = ni env l ++ ni env r
2038 ni env (PPair _ _ l r) = ni env l ++ ni env r
2047 ni env (PPair _ _ l r) = ni env l ++ ni env r