@@ -94,6 +94,7 @@ data IOption = IOption {
94 , opt_printdepth :: Maybe Int
94 , opt_printdepth :: Maybe Int
95 , opt_evaltypes :: Bool -- ^ normalise types in :t
95 , opt_evaltypes :: Bool -- ^ normalise types in :t
96 , opt_desugarnats :: Bool
96 , opt_desugarnats :: Bool
97+ , opt_autoimpls :: Bool
97 } deriving (Show, Eq)
98 } deriving (Show, Eq)
99defaultOpts = IOption { opt_logLevel = 0
100defaultOpts = IOption { opt_logLevel = 0
@@ -121,6 +122,7 @@ defaultOpts = IOption { opt_logLevel = 0
121 , opt_printdepth = Just 5000
122 , opt_printdepth = Just 5000
122 , opt_evaltypes = True
123 , opt_evaltypes = True
123 , opt_desugarnats = False
124 , opt_desugarnats = False
125+ , opt_autoimpls = True
126data PPOption = PPOption {
128data PPOption = PPOption {
@@ -194,7 +196,6 @@ data IState = IState {
194 -- ^ list of lhs/rhs, and a list of missing clauses
196 -- ^ list of lhs/rhs, and a list of missing clauses
195 idris_flags :: Ctxt [FnOpt],
197 idris_flags :: Ctxt [FnOpt],
196 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
198 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
197− idris_calledgraph :: Ctxt [Name],
198 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
199 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
199 idris_moduledocs :: Ctxt (Docstring DocTerm),
200 idris_moduledocs :: Ctxt (Docstring DocTerm),
200 -- ^ module documentation is saved in a special MN so the context
201 -- ^ module documentation is saved in a special MN so the context
@@ -235,7 +236,7 @@ data IState = IState {
235 brace_stack :: [Maybe Int],
236 brace_stack :: [Maybe Int],
236 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
237 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
237 idris_parsedSpan :: Maybe FC,
238 idris_parsedSpan :: Maybe FC,
238− hide_list :: [(Name, Maybe Accessibility)],
239+ hide_list :: Ctxt Accessibility,
239 default_access :: Accessibility,
240 default_access :: Accessibility,
240 default_total :: Bool,
241 default_total :: Bool,
241 ibc_write :: [IBCWrite],
242 ibc_write :: [IBCWrite],
@@ -262,7 +263,9 @@ data IState = IState {
262 idris_exports :: [Name], -- ^ Functions with ExportList
263 idris_exports :: [Name], -- ^ Functions with ExportList
263 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
264 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
264 idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser
265 idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser
265− idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
266+ idris_deprecated :: Ctxt String, -- ^ Deprecated names and explanation
267+ idris_inmodule :: S.Set Name, -- ^ Names defined in current module
268+ idris_ttstats :: M.Map Term (Int, Term)
268-- Required for parsers library, and therefore trifecta
271-- Required for parsers library, and therefore trifecta
@@ -279,11 +282,10 @@ deriving instance NFData SizeChange
279type SCGEntry = (Name, [Maybe (Int, SizeChange)])
282type SCGEntry = (Name, [Maybe (Int, SizeChange)])
280type UsageReason = (Name, Int) -- fn_name, its_arg_number
283type UsageReason = (Name, Int) -- fn_name, its_arg_number
282−data CGInfo = CGInfo { argsdef :: [Name],
285+data CGInfo = CGInfo { calls :: [Name],
283− calls :: [(Name, [[Name]])],
284 scg :: [SCGEntry],
286 scg :: [SCGEntry],
286− usedpos :: [(Int, [UsageReason])] }
287+ usedpos :: [(Int, [UsageReason])]
287 deriving Show
289 deriving Show
289deriving instance Binary CGInfo
291deriving instance Binary CGInfo
@@ -348,12 +350,13 @@ idrisInit = IState initContext S.empty []
348 emptyContext emptyContext emptyContext emptyContext
350 emptyContext emptyContext emptyContext emptyContext
349 emptyContext emptyContext emptyContext emptyContext
351 emptyContext emptyContext emptyContext emptyContext
350 emptyContext emptyContext emptyContext emptyContext
352 emptyContext emptyContext emptyContext emptyContext
351− emptyContext emptyContext
353+ emptyContext
352 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
354 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
353− [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
355+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Hidden False [] Nothing [] []
354 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
356 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
355 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
357 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
356− emptyContext
358+ emptyContext S.empty M.empty
358-- | The monad for the main REPL - reading and processing files and updating
361-- | The monad for the main REPL - reading and processing files and updating
359-- global state (hence the IO inner monad).
362-- global state (hence the IO inner monad).
@@ -631,13 +634,17 @@ is_scoped :: Plicity -> Maybe ImplicitInfo
631is_scoped (Imp _ _ _ s) = s
634is_scoped (Imp _ _ _ s) = s
632is_scoped _ = Nothing
635is_scoped _ = Nothing
634−impl = Imp [] Dynamic False (Just (Impl False True))
637+impl = Imp [] Dynamic False (Just (Impl False True))
635−forall_imp = Imp [] Dynamic False (Just (Impl False False))
639+forall_imp = Imp [] Dynamic False (Just (Impl False False))
636forall_constraint = Imp [] Dynamic False (Just (Impl True False))
640forall_constraint = Imp [] Dynamic False (Just (Impl True False))
637−expl = Exp [] Dynamic False
642+expl = Exp [] Dynamic False
638−expl_param = Exp [] Dynamic True
643+expl_param = Exp [] Dynamic True
639−constraint = Constraint [] Static
645+constraint = Constraint [] Static
640−tacimpl t = TacImp [] Dynamic t
647+tacimpl t = TacImp [] Dynamic t
642data FnOpt = Inlinable -- always evaluate when simplifying
649data FnOpt = Inlinable -- always evaluate when simplifying
643 | TotalFn | PartialFn | CoveringFn
650 | TotalFn | PartialFn | CoveringFn
@@ -695,7 +702,7 @@ data PDecl' t
695 FC -- Record name precise location
702 FC -- Record name precise location
696 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
703 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
697 [(Name, Docstring (Either Err t))] -- Param Docs
704 [(Name, Docstring (Either Err t))] -- Param Docs
698− [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
705+ [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
699 (Maybe (Name, FC)) -- Optional constructor name and location
706 (Maybe (Name, FC)) -- Optional constructor name and location
700 (Docstring (Either Err t)) -- Constructor doc
707 (Docstring (Either Err t)) -- Constructor doc
701 SyntaxInfo -- Constructor SyntaxInfo
708 SyntaxInfo -- Constructor SyntaxInfo
@@ -717,6 +724,7 @@ data PDecl' t
717 [(Name, Docstring (Either Err t))] -- Parameter docs
724 [(Name, Docstring (Either Err t))] -- Parameter docs
718 SyntaxInfo
725 SyntaxInfo
719 FC [(Name, t)] -- constraints
726 FC [(Name, t)] -- constraints
720 Name -- class
728 Name -- class
721 FC -- precise location of class
729 FC -- precise location of class
722 [t] -- parameters
730 [t] -- parameters
@@ -756,6 +764,7 @@ data Directive = DLib Codegen String |
756 DErrorHandlers Name FC Name FC [(Name, FC)] |
764 DErrorHandlers Name FC Name FC [(Name, FC)] |
757 DLanguage LanguageExt |
765 DLanguage LanguageExt |
758 DDeprecate Name String |
766 DDeprecate Name String |
767+ DAutoImplicits Bool |
759 DUsed FC Name Name
768 DUsed FC Name Name
761-- | A set of instructions for things that need to happen in IState
770-- | A set of instructions for things that need to happen in IState
@@ -875,10 +884,10 @@ mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor c
875 (map (mapPDeclFC f g) body)
884 (map (mapPDeclFC f g) body)
876 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
885 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
878−mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn cnfc params instTy instN body) =
887+mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc cnfc params instTy instN body) =
879 PInstance doc paramDocs syn (f fc)
888 PInstance doc paramDocs syn (f fc)
880 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
889 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
881− cn (g cnfc) (map (mapPTermFC f g) params)
890+ cn acc (g cnfc) (map (mapPTermFC f g) params)
882 (mapPTermFC f g instTy)
891 (mapPTermFC f g instTy)
884 (map (mapPDeclFC f g) body)
893 (map (mapPDeclFC f g) body)
@@ -918,7 +927,7 @@ declared (PParams _ _ ds) = concatMap declared ds
918declared (PNamespace _ _ ds) = concatMap declared ds
927declared (PNamespace _ _ ds) = concatMap declared ds
919declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
928declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
920declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
929declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
921−declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
930+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
922declared (PDSL n _) = [n]
931declared (PDSL n _) = [n]
923declared (PSyntax _ _) = []
932declared (PSyntax _ _) = []
924declared (PMutual _ ds) = concatMap declared ds
933declared (PMutual _ ds) = concatMap declared ds
@@ -927,39 +936,39 @@ declared _ = []
928-- get the names declared, not counting nested parameter blocks
937-- get the names declared, not counting nested parameter blocks
929tldeclared :: PDecl -> [Name]
938tldeclared :: PDecl -> [Name]
930−tldeclared (PFix _ _ _) = []
939+tldeclared (PFix _ _ _) = []
931−tldeclared (PTy _ _ _ _ _ n _ t) = [n]
940+tldeclared (PTy _ _ _ _ _ n _ t) = [n]
932−tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
941+tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
933−tldeclared (PClauses _ _ n _) = [] -- not a declaration
942+tldeclared (PClauses _ _ n _) = [] -- not a declaration
934−tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
943+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
935tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
944tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
936 where fstt (_, _, a, _, _, _, _) = a
945 where fstt (_, _, a, _, _, _, _) = a
937−tldeclared (PParams _ _ ds) = []
946+tldeclared (PParams _ _ ds) = []
938−tldeclared (PMutual _ ds) = concatMap tldeclared ds
947+tldeclared (PMutual _ ds) = concatMap tldeclared ds
939−tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
948+tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
940−tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
949+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
941−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
950+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
942−tldeclared _ = []
951+tldeclared _ = []
944defined :: PDecl -> [Name]
953defined :: PDecl -> [Name]
945−defined (PFix _ _ _) = []
954+defined (PFix _ _ _) = []
946−defined (PTy _ _ _ _ _ n _ t) = []
955+defined (PTy _ _ _ _ _ n _ t) = []
947−defined (PPostulate _ _ _ _ _ _ n t) = []
956+defined (PPostulate _ _ _ _ _ _ n t) = []
948−defined (PClauses _ _ n _) = [n] -- not a declaration
957+defined (PClauses _ _ n _) = [n] -- not a declaration
949−defined (PCAF _ n _) = [n]
958+defined (PCAF _ n _) = [n]
950−defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
959+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
951 where fstt (_, _, a, _, _, _, _) = a
960 where fstt (_, _, a, _, _, _, _) = a
952−defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
961+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
953−defined (PParams _ _ ds) = concatMap defined ds
962+defined (PParams _ _ ds) = concatMap defined ds
954−defined (PNamespace _ _ ds) = concatMap defined ds
963+defined (PNamespace _ _ ds) = concatMap defined ds
955−defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
964+defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
956−defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
965+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
957−defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
966+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
958−defined (PDSL n _) = [n]
967+defined (PDSL n _) = [n]
959−defined (PSyntax _ _) = []
968+defined (PSyntax _ _) = []
960−defined (PMutual _ ds) = concatMap defined ds
969+defined (PMutual _ ds) = concatMap defined ds
961−defined (PDirective _) = []
970+defined (PDirective _) = []
962−defined _ = []
971+defined _ = []
964updateN :: [(Name, Name)] -> Name -> Name
973updateN :: [(Name, Name)] -> Name -> Name
965updateN ns n | Just n' <- lookup n ns = n'
974updateN ns n | Just n' <- lookup n ns = n'
@@ -1040,33 +1049,33 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1040-- general-purpose FCs, and the second transforms those that are used
1049-- general-purpose FCs, and the second transforms those that are used
1041-- for semantic source highlighting, so they can be treated specially.
1050-- for semantic source highlighting, so they can be treated specially.
1042mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1051mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1043−mapPTermFC f g (PQuote q) = PQuote q
1052+mapPTermFC f g (PQuote q) = PQuote q
1044−mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1053+mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1045−mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1054+mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1046−mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1055+mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1047−mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1056+mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1048−mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1057+mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1049−mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1058+mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1050−mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1059+mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1051−mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1060+mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1052−mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1061+mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1053−mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1062+mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1054−mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1063+mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1055−mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1064+mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1056−mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)
1065+mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)
1057−mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1066+mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1058−mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1067+mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1059−mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1068+mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1060−mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1069+mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1061−mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1070+mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1062−mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1071+mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1063−mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1072+mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1064−mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1073+mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1065−mapPTermFC f g (PType fc) = PType (f fc)
1074+mapPTermFC f g (PType fc) = PType (f fc)
1066−mapPTermFC f g (PUniverse u) = PUniverse u
1075+mapPTermFC f g (PUniverse u) = PUniverse u
1067−mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1076+mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1068−mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1077+mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1069−mapPTermFC f g Placeholder = Placeholder
1078+mapPTermFC f g Placeholder = Placeholder
1070mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1079mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1071 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1080 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1072 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1081 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
@@ -1074,22 +1083,22 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1074 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1083 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1075 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1084 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1076 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1085 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1077−mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1086+mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1078−mapPTermFC f g (PReturn fc) = PReturn (f fc)
1087+mapPTermFC f g (PReturn fc) = PReturn (f fc)
1079−mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1088+mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1080−mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1089+mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1081−mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1090+mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1082−mapPTermFC f g (PElabError err) = PElabError err
1091+mapPTermFC f g (PElabError err) = PElabError err
1083−mapPTermFC f g PImpossible = PImpossible
1092+mapPTermFC f g PImpossible = PImpossible
1084−mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1093+mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1085−mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1094+mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1086−mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1095+mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1087−mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1096+mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1088−mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1097+mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1089−mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1098+mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1090−mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1099+mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1091−mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1100+mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1092−mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1101+mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1095dg instance Binary PTerm
1104dg instance Binary PTerm
@@ -1098,28 +1107,27 @@ deriving instance NFData PTerm
1099mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1108mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1100mapPT f t = f (mpt t) where
1109mapPT f t = f (mpt t) where
1101− mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1110+ mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1102− mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1111+ mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1103− mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1112+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1104− mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
1113+ mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1106− mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1114+ mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1107− mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1115+ mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1108− mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1116+ mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1109− mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1117+ mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1110− mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1118+ mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1111− mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1119+ mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1112 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1120 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1113− mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1121+ mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1114− mpt (PHidden t) = PHidden (mapPT f t)
1122+ mpt (PHidden t) = PHidden (mapPT f t)
1115− mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1123+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1116− mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1124+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1117− mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1125+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1118− mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1126+ mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1119− mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1127+ mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1120− mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1128+ mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1121− mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1129+ mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1122− mpt x = x
1130+ mpt x = x
1125data PTactic' t = Intro [Name] | Intros | Focus Name
1133data PTactic' t = Intro [Name] | Intros | Focus Name
@@ -1160,39 +1168,39 @@ deriving instance Binary PTactic'
1160deriving instance NFData PTactic'
1168deriving instance NFData PTactic'
1162instance Sized a => Sized (PTactic' a) where
1170instance Sized a => Sized (PTactic' a) where
1163− size (Intro nms) = 1 + size nms
1171+ size (Intro nms) = 1 + size nms
1164− size Intros = 1
1172+ size Intros = 1
1165− size (Focus nm) = 1 + size nm
1173+ size (Focus nm) = 1 + size nm
1166− size (Refine nm bs) = 1 + size nm + length bs
1174+ size (Refine nm bs) = 1 + size nm + length bs
1167− size (Rewrite t) = 1 + size t
1175+ size (Rewrite t) = 1 + size t
1168− size (Induction t) = 1 + size t
1176+ size (Induction t) = 1 + size t
1169− size (LetTac nm t) = 1 + size nm + size t
1177+ size (LetTac nm t) = 1 + size nm + size t
1170− size (Exact t) = 1 + size t
1178+ size (Exact t) = 1 + size t
1171− size Compute = 1
1179+ size Compute = 1
1172− size Trivial = 1
1180+ size Trivial = 1
1173− size Solve = 1
1181+ size Solve = 1
1174− size Attack = 1
1182+ size Attack = 1
1175− size ProofState = 1
1183+ size ProofState = 1
1176− size ProofTerm = 1
1184+ size ProofTerm = 1
1177− size Undo = 1
1185+ size Undo = 1
1178− size (Try l r) = 1 + size l + size r
1186+ size (Try l r) = 1 + size l + size r
1179− size (TSeq l r) = 1 + size l + size r
1187+ size (TSeq l r) = 1 + size l + size r
1180− size (ApplyTactic t) = 1 + size t
1188+ size (ApplyTactic t) = 1 + size t
1181− size (Reflect t) = 1 + size t
1189+ size (Reflect t) = 1 + size t
1182− size (Fill t) = 1 + size t
1190+ size (Fill t) = 1 + size t
1183− size Qed = 1
1191+ size Qed = 1
1184− size Abandon = 1
1192+ size Abandon = 1
1185− size Skip = 1
1193+ size Skip = 1
1186− size (TFail ts) = 1 + size ts
1194+ size (TFail ts) = 1 + size ts
1187− size SourceFC = 1
1195+ size SourceFC = 1
1188− size DoUnify = 1
1196+ size DoUnify = 1
1189− size (CaseTac x) = 1 + size x
1197+ size (CaseTac x) = 1 + size x
1190− size (Equiv t) = 1 + size t
1198+ size (Equiv t) = 1 + size t
1191− size (Claim x y) = 1 + size x + size y
1199+ size (Claim x y) = 1 + size x + size y
1192− size Unfocus = 1
1200+ size Unfocus = 1
1193− size (MatchRefine x) = 1 + size x
1201+ size (MatchRefine x) = 1 + size x
1194 size (LetTacTy x y z) = 1 + size x + size y + size z
1202 size (LetTacTy x y z) = 1 + size x + size y + size z
1195− size TCInstance = 1
1203+ size TCInstance = 1
1197type PTactic = PTactic' PTerm
1205type PTactic = PTactic' PTerm
@@ -1208,11 +1216,11 @@ deriving instance NFData PDo'
1210instance Sized a => Sized (PDo' a) where
1218instance Sized a => Sized (PDo' a) where
1211− size (DoExp fc t) = 1 + size fc + size t
1219+ size (DoExp fc t) = 1 + size fc + size t
1212− size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1220+ size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1213− size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1221+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1214− size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1222+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1215− size (DoLetP fc l r) = 1 + size fc + size l + size r
1223+ size (DoLetP fc l r) = 1 + size fc + size l + size r
1217type PDo = PDo' PTerm
1225type PDo = PDo' PTerm
@@ -1244,10 +1252,10 @@ data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1244 deriving (Show, Eq, Data, Typeable)
1252 deriving (Show, Eq, Data, Typeable)
1246instance Sized a => Sized (PArg' a) where
1254instance Sized a => Sized (PArg' a) where
1247− size (PImp p _ l nm trm) = 1 + size nm + size trm
1255+ size (PImp p _ l nm trm) = 1 + size nm + size trm
1248− size (PExp p l nm trm) = 1 + size nm + size trm
1256+ size (PExp p l nm trm) = 1 + size nm + size trm
1249− size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1257+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1250− size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1258+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1253deriving instance Binary PArg'
1261deriving instance Binary PArg'
@@ -1255,43 +1263,43 @@ deriving instance NFData PArg'
1257pimp n t mach = PImp 1 mach [] n t
1265pimp n t mach = PImp 1 mach [] n t
1258−pexp t = PExp 1 [] (sMN 0 "arg") t
1266+pexp t = PExp 1 [] (sMN 0 "arg") t
1259−pconst t = PConstraint 1 [] (sMN 0 "carg") t
1267+pconst t = PConstraint 1 [] (sMN 0 "carg") t
1260ptacimp n s t = PTacImplicit 2 [] n s t
1268ptacimp n s t = PTacImplicit 2 [] n s t
1262type PArg = PArg' PTerm
1270type PArg = PArg' PTerm
1264-- | Get the highest FC in a term, if one exists
1272-- | Get the highest FC in a term, if one exists
1265highestFC :: PTerm -> Maybe FC
1273highestFC :: PTerm -> Maybe FC
1266−highestFC (PQuote _) = Nothing
1274+highestFC (PQuote _) = Nothing
1267−highestFC (PRef fc _ _) = Just fc
1275+highestFC (PRef fc _ _) = Just fc
1268−highestFC (PInferRef fc _ _) = Just fc
1276+highestFC (PInferRef fc _ _) = Just fc
1269−highestFC (PPatvar fc _) = Just fc
1277+highestFC (PPatvar fc _) = Just fc
1270−highestFC (PLam fc _ _ _ _) = Just fc
1278+highestFC (PLam fc _ _ _ _) = Just fc
1271−highestFC (PPi _ _ _ _ _) = Nothing
1279+highestFC (PPi _ _ _ _ _) = Nothing
1272−highestFC (PLet fc _ _ _ _ _) = Just fc
1280+highestFC (PLet fc _ _ _ _ _) = Just fc
1273−highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1281+highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1274−highestFC (PApp fc _ _) = Just fc
1282+highestFC (PApp fc _ _) = Just fc
1275−highestFC (PAppBind fc _ _) = Just fc
1283+highestFC (PAppBind fc _ _) = Just fc
1276−highestFC (PMatchApp fc _) = Just fc
1284+highestFC (PMatchApp fc _) = Just fc
1277−highestFC (PCase fc _ _) = Just fc
1285+highestFC (PCase fc _ _) = Just fc
1278−highestFC (PIfThenElse fc _ _ _) = Just fc
1286+highestFC (PIfThenElse fc _ _ _) = Just fc
1279−highestFC (PTrue fc _) = Just fc
1287+highestFC (PTrue fc _) = Just fc
1280−highestFC (PResolveTC fc) = Just fc
1288+highestFC (PResolveTC fc) = Just fc
1281−highestFC (PRewrite fc _ _ _) = Just fc
1289+highestFC (PRewrite fc _ _ _) = Just fc
1282−highestFC (PPair fc _ _ _ _) = Just fc
1290+highestFC (PPair fc _ _ _ _) = Just fc
1283−highestFC (PDPair fc _ _ _ _ _) = Just fc
1291+highestFC (PDPair fc _ _ _ _ _) = Just fc
1284−highestFC (PAs fc _ _) = Just fc
1292+highestFC (PAs fc _ _) = Just fc
1285highestFC (PAlternative _ _ args) =
1293highestFC (PAlternative _ _ args) =
1286 case mapMaybe highestFC args of
1294 case mapMaybe highestFC args of
1287 [] -> Nothing
1295 [] -> Nothing
1288 (fc:_) -> Just fc
1296 (fc:_) -> Just fc
1289−highestFC (PHidden _) = Nothing
1297+highestFC (PHidden _) = Nothing
1290−highestFC (PType fc) = Just fc
1298+highestFC (PType fc) = Just fc
1291−highestFC (PUniverse _) = Nothing
1299+highestFC (PUniverse _) = Nothing
1292−highestFC (PGoal fc _ _ _) = Just fc
1300+highestFC (PGoal fc _ _ _) = Just fc
1293−highestFC (PConstant fc _) = Just fc
1301+highestFC (PConstant fc _) = Just fc
1294−highestFC Placeholder = Nothing
1302+highestFC Placeholder = Nothing
1295highestFC (PDoBlock lines) =
1303highestFC (PDoBlock lines) =
1296 case map getDoFC lines of
1304 case map getDoFC lines of
1297 [] -> Nothing
1305 [] -> Nothing
@@ -1303,23 +1311,23 @@ highestFC (PDoBlock lines) =
1303 getDoFC (DoLet fc nm nfc l r) = fc
1311 getDoFC (DoLet fc nm nfc l r) = fc
1304 getDoFC (DoLetP fc l r) = fc
1312 getDoFC (DoLetP fc l r) = fc
1306−highestFC (PIdiom fc _) = Just fc
1314+highestFC (PIdiom fc _) = Just fc
1307−highestFC (PReturn fc) = Just fc
1315+highestFC (PReturn fc) = Just fc
1308−highestFC (PMetavar fc _) = Just fc
1316+highestFC (PMetavar fc _) = Just fc
1309−highestFC (PProof _) = Nothing
1317+highestFC (PProof _) = Nothing
1310−highestFC (PTactics _) = Nothing
1318+highestFC (PTactics _) = Nothing
1311−highestFC (PElabError _) = Nothing
1319+highestFC (PElabError _) = Nothing
1312−highestFC PImpossible = Nothing
1320+highestFC PImpossible = Nothing
1313−highestFC (PCoerced tm) = highestFC tm
1321+highestFC (PCoerced tm) = highestFC tm
1314−highestFC (PDisamb _ opts) = highestFC opts
1322+highestFC (PDisamb _ opts) = highestFC opts
1315−highestFC (PUnifyLog tm) = highestFC tm
1323+highestFC (PUnifyLog tm) = highestFC tm
1316−highestFC (PNoImplicits tm) = highestFC tm
1324+highestFC (PNoImplicits tm) = highestFC tm
1317−highestFC (PQuasiquote _ _) = Nothing
1325+highestFC (PQuasiquote _ _) = Nothing
1318−highestFC (PUnquote tm) = highestFC tm
1326+highestFC (PUnquote tm) = highestFC tm
1319−highestFC (PQuoteName _ _ fc) = Just fc
1327+highestFC (PQuoteName _ _ fc) = Just fc
1320−highestFC (PRunElab fc _ _) = Just fc
1328+highestFC (PRunElab fc _ _) = Just fc
1321−highestFC (PConstSugar fc _) = Just fc
1329+highestFC (PConstSugar fc _) = Just fc
1322−highestFC (PAppImpl t _) = highestFC t
1330+highestFC (PAppImpl t _) = highestFC t
1324-- Type class data
1332-- Type class data
@@ -1397,11 +1405,11 @@ data Syntax = Rule [SSymbol] PTerm SynContext
1398syntaxNames :: Syntax -> [Name]
1406syntaxNames :: Syntax -> [Name]
1399syntaxNames (Rule syms _ _) = mapMaybe ename syms
1407syntaxNames (Rule syms _ _) = mapMaybe ename syms
1400− where ename (Keyword n) = Just n
1408+ where ename (Keyword n) = Just n
1401− ename _ = Nothing
1409+ ename _ = Nothing
1402syntaxNames (DeclRule syms _) = mapMaybe ename syms
1410syntaxNames (DeclRule syms _) = mapMaybe ename syms
1403− where ename (Keyword n) = Just n
1411+ where ename (Keyword n) = Just n
1404− ename _ = Nothing
1412+ ename _ = Nothing
1406syntaxSymbols :: Syntax -> [SSymbol]
1414syntaxSymbols :: Syntax -> [SSymbol]
1407syntaxSymbols (Rule ss _ _) = ss
1415syntaxSymbols (Rule ss _ _) = ss
@@ -1434,9 +1442,9 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1435 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1443 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1437− ruleSort [] [] = EQ
1445+ ruleSort [] [] = EQ
1438− ruleSort [] _ = LT
1446+ ruleSort [] _ = LT
1439− ruleSort _ [] = GT
1447+ ruleSort _ [] = GT
1440 ruleSort (s1:ss1) (s2:ss2) =
1448 ruleSort (s1:ss1) (s2:ss2) =
1441 case symCompare s1 s2 of
1449 case symCompare s1 s2 of
1442 EQ -> ruleSort ss1 ss2
1450 EQ -> ruleSort ss1 ss2
@@ -1444,25 +1452,25 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1445 -- Better than creating Ord instance for SSymbol since
1453 -- Better than creating Ord instance for SSymbol since
1446 -- in general this ordering does not really make sense.
1454 -- in general this ordering does not really make sense.
1447− symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1455+ symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1448− symCompare (Keyword _) _ = LT
1456+ symCompare (Keyword _) _ = LT
1449− symCompare (Symbol _) (Keyword _) = GT
1457+ symCompare (Symbol _) (Keyword _) = GT
1450− symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1458+ symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1451− symCompare (Symbol _) _ = LT
1459+ symCompare (Symbol _) _ = LT
1452− symCompare (Binding _) (Keyword _) = GT
1460+ symCompare (Binding _) (Keyword _) = GT
1453− symCompare (Binding _) (Symbol _) = GT
1461+ symCompare (Binding _) (Symbol _) = GT
1454− symCompare (Binding b1) (Binding b2) = compare b1 b2
1462+ symCompare (Binding b1) (Binding b2) = compare b1 b2
1455− symCompare (Binding _) _ = LT
1463+ symCompare (Binding _) _ = LT
1456− symCompare (Expr _) (Keyword _) = GT
1464+ symCompare (Expr _) (Keyword _) = GT
1457− symCompare (Expr _) (Symbol _) = GT
1465+ symCompare (Expr _) (Symbol _) = GT
1458− symCompare (Expr _) (Binding _) = GT
1466+ symCompare (Expr _) (Binding _) = GT
1459− symCompare (Expr e1) (Expr e2) = compare e1 e2
1467+ symCompare (Expr e1) (Expr e2) = compare e1 e2
1460− symCompare (Expr _) _ = LT
1468+ symCompare (Expr _) _ = LT
1461− symCompare (SimpleExpr _) (Keyword _) = GT
1469+ symCompare (SimpleExpr _) (Keyword _) = GT
1462− symCompare (SimpleExpr _) (Symbol _) = GT
1470+ symCompare (SimpleExpr _) (Symbol _) = GT
1463− symCompare (SimpleExpr _) (Binding _) = GT
1471+ symCompare (SimpleExpr _) (Binding _) = GT
1464− symCompare (SimpleExpr _) (Expr _) = GT
1472+ symCompare (SimpleExpr _) (Expr _) = GT
1465− symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1473+ symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1467initDSL = DSL (PRef f [] (sUN ">>="))
1475initDSL = DSL (PRef f [] (sUN ">>="))
1468 (PRef f [] (sUN "return"))
1476 (PRef f [] (sUN "return"))
@@ -1534,10 +1542,10 @@ getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1534getInferTerm (App _ (App _ _ _) tm) = tm
1542getInferTerm (App _ (App _ _ _) tm) = tm
1535getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1543getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1537−getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1545+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1538− where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1546+ where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1539− toTy (PVar t) = PVTy t
1547+ toTy (PVar t) = PVTy t
1540− toTy b = b
1548+ toTy b = b
1541getInferType (App _ (App _ _ ty) _) = ty
1549getInferType (App _ (App _ _ ty) _) = ty
@@ -1562,9 +1570,9 @@ pairCon = sNS (sUN "MkPair") ["Builtins"]
1562upairTy = sNS (sUN "UPair") ["Builtins"]
1570upairTy = sNS (sUN "UPair") ["Builtins"]
1563upairCon = sNS (sUN "MkUPair") ["Builtins"]
1571upairCon = sNS (sUN "MkUPair") ["Builtins"]
1565−eqTy = sUN "="
1573+eqTy = sUN "="
1566eqCon = sUN "Refl"
1574eqCon = sUN "Refl"
1567−eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1575+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1568 "The propositional equality type. A proof that `x` = `y`." ++
1576 "The propositional equality type. A proof that `x` = `y`." ++
1569 "\n\n" ++
1577 "\n\n" ++
1570 "To use such a proof, pattern-match on it, and the two equal things will " ++
1578 "To use such a proof, pattern-match on it, and the two equal things will " ++
@@ -1607,8 +1615,8 @@ modDocName :: Name
1607modDocName = sMN 0 "ModuleDocs"
1615modDocName = sMN 0 "ModuleDocs"
1609-- Defined in builtins.idr
1617-- Defined in builtins.idr
1610−sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1618+sigmaTy = sNS (sUN "DPair") ["Builtins"]
1611−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1613piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1614piBind = piBindp expl
1622piBind = piBindp expl
@@ -1648,11 +1656,11 @@ annotationColour ist (AnnConst c) =
1648 in Just $ if constIsType c
1656 in Just $ if constIsType c
1649 then typeColour theme
1657 then typeColour theme
1650 else dataColour theme
1658 else dataColour theme
1651−annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1659+annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1652−annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1660+annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1653−annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1661+annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1654annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1662annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1655−annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1663+annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1656annotationColour ist (AnnName n _ _ _) =
1664annotationColour ist (AnnName n _ _ _) =
1657 let ctxt = tt_ctxt ist
1665 let ctxt = tt_ctxt ist
1658 theme = idris_colourTheme ist
1666 theme = idris_colourTheme ist
@@ -1738,7 +1746,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1740 case s of
1748 case s of
1741− Static -> text "[static]" <> space
1749+ Static -> text "%static" <> space
1742 _ -> empty
1750 _ -> empty
1743 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1751 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1744 | ppopt_impl ppo =
1752 | ppopt_impl ppo =
@@ -1749,12 +1757,12 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1751 case s of
1759 case s of
1752− Static -> text "[static]" <> space
1760+ Static -> text "%static" <> space
1753 _ -> empty
1761 _ -> empty
1754 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1762 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1755 depth d . bracket p startPrec $
1763 depth d . bracket p startPrec $
1756 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1764 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1757− prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
1765+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1758 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1766 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1759 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1767 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1760 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1768 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
@@ -1791,7 +1799,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1791 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1799 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1792 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1800 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1793 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1801 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1794− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1802+ (l@(PExp{}) : r@(PExp{}) : rest) ->
1795 depth d . bracket p funcAppPrec $
1803 depth d . bracket p funcAppPrec $
1796 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1804 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1797 align (group (vsep (map (prettyArgS d bnd) rest)))
1805 align (group (vsep (map (prettyArgS d bnd) rest)))
@@ -1842,20 +1850,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1842 -- disambiguation on PDPair.
1850 -- disambiguation on PDPair.
1843 vars tm = filter noNS (allNamesIn tm)
1851 vars tm = filter noNS (allNamesIn tm)
1844 noNS (NS _ _) = False
1852 noNS (NS _ _) = False
1845− noNS _ = True
1853+ noNS _ = True
1847 prettySe d p bnd (PIfThenElse _ c t f) =
1855 prettySe d p bnd (PIfThenElse _ c t f) =
1848 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1856 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1849− [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1857+ [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1850 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1858 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1851 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1859 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1853− prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1861+ prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1854− prettySe d p bnd (PResolveTC _) = kwd "%instance"
1862+ prettySe d p bnd (PResolveTC _) = kwd "%instance"
1855− prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1863+ prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1856− prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1864+ prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1857 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1865 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1858− prettySe d p bnd (PRewrite _ l r _) =
1866+ prettySe d p bnd (PRewrite _ l r _) =
1859 depth d . bracket p startPrec $
1867 depth d . bracket p startPrec $
1860 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1868 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1861 prettySe d p bnd (PTyped l r) =
1869 prettySe d p bnd (PTyped l r) =
@@ -1865,9 +1873,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1865 align . group . vsep . punctuate (ann comma) $
1873 align . group . vsep . punctuate (ann comma) $
1866 map (prettySe (decD d) startPrec bnd) elts
1874 map (prettySe (decD d) startPrec bnd) elts
1867 where ann = case pun of
1875 where ann = case pun of
1868− TypeOrTerm -> id
1876+ TypeOrTerm -> id
1869− IsType -> annName pairTy
1877+ IsType -> annName pairTy
1870− IsTerm -> annName pairCon
1878+ IsTerm -> annName pairCon
1871 prettySe d p bnd (PDPair _ _ pun l t r) =
1879 prettySe d p bnd (PDPair _ _ pun l t r) =
1872 depth d $
1880 depth d $
1873 annotated lparen <>
1881 annotated lparen <>
@@ -1876,30 +1884,32 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1876 prettySe (decD d) startPrec (addBinding bnd) r <>
1884 prettySe (decD d) startPrec (addBinding bnd) r <>
1877 annotated rparen
1885 annotated rparen
1878 where annotated = case pun of
1886 where annotated = case pun of
1879− IsType -> annName sigmaTy
1887+ IsType -> annName sigmaTy
1880− IsTerm -> annName sigmaCon
1888+ IsTerm -> annName sigmaCon
1881− TypeOrTerm -> id
1889+ TypeOrTerm -> id
1882 (left, addBinding) = case (l, pun) of
1890 (left, addBinding) = case (l, pun) of
1883 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1891 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1884− _ -> (prettySe (decD d) startPrec bnd l, id)
1892+ _ -> (prettySe (decD d) startPrec bnd l, id)
1885 prettySe d p bnd (PAlternative ns a as) =
1893 prettySe d p bnd (PAlternative ns a as) =
1886 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1894 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1888 prettyAs =
1896 prettyAs =
1897+ foldr ((\ l r -> l <+> text "," <+> r) .
1889− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1898+ depth d . prettySe (decD d) startPrec bnd)
1890− prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1900+ prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1891− prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1901+ prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1892− prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1902+ prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1893 -- XXX: add pretty for tactics
1903 -- XXX: add pretty for tactics
1894− prettySe d p bnd (PProof ts) =
1904+ prettySe d p bnd (PProof ts) =
1895 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1905 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1896− prettySe d p bnd (PTactics ts) =
1906+ prettySe d p bnd (PTactics ts) =
1897 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1907 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1898− prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1908+ prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1899− prettySe d p bnd (PReturn f) = kwd "return"
1909+ prettySe d p bnd (PReturn f) = kwd "return"
1900− prettySe d p bnd PImpossible = kwd "impossible"
1910+ prettySe d p bnd PImpossible = kwd "impossible"
1901− prettySe d p bnd Placeholder = text "_"
1911+ prettySe d p bnd Placeholder = text "_"
1902− prettySe d p bnd (PDoBlock dos) =
1912+ prettySe d p bnd (PDoBlock dos) =
1903 bracket p startPrec $
1913 bracket p startPrec $
1904 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1914 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1905 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1915 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
@@ -1921,47 +1931,46 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1921 text "no pretty printer for pattern-matching do binding" :
1931 text "no pretty printer for pattern-matching do binding" :
1922 ppdo bnd dos
1932 ppdo bnd dos
1923 ppdo _ [] = []
1933 ppdo _ [] = []
1924− prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1934+ prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1925− prettySe d p bnd (PElabError s) = pretty s
1935+ prettySe d p bnd (PElabError s) = pretty s
1926 -- Quasiquote pprinting ignores bound vars
1936 -- Quasiquote pprinting ignores bound vars
1927− prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1937+ prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1928 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1938 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1929− prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1939+ prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1930− prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1940+ prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1931 where start = if res then "`{" else "`{{"
1941 where start = if res then "`{" else "`{{"
1932 end = if res then "}" else "}}"
1942 end = if res then "}" else "}}"
1933− prettySe d p bnd (PRunElab _ tm _) =
1943+ prettySe d p bnd (PRunElab _ tm _) =
1934 bracket p funcAppPrec . group . align . hang 2 $
1944 bracket p funcAppPrec . group . align . hang 2 $
1935 text "%runElab" <$>
1945 text "%runElab" <$>
1936 prettySe (decD d) funcAppPrec bnd tm
1946 prettySe (decD d) funcAppPrec bnd tm
1937− prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1947+ prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1939− prettySe d p bnd _ = text "missing pretty-printer for term"
1948+ prettySe d p bnd _ = text "missing pretty-printer for term"
1941 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1950 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1942 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1951 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1943 where display (UN n) = T.unpack n
1952 where display (UN n) = T.unpack n
1944 display (MN _ n) = T.unpack n
1953 display (MN _ n) = T.unpack n
1945 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1954 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1946− display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1955+ display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1947 display n = show n
1956 display n = show n
1949− prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1958+ prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1950− prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1959+ prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1951− prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1960+ prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1952− prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1961+ prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1954− prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1963+ prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1955− prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1964+ prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1956− prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1965+ prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1957 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1966 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1959 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1968 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1960 annName n = annotate (AnnName n Nothing Nothing Nothing)
1969 annName n = annotate (AnnName n Nothing Nothing Nothing)
1962 opStr :: Name -> String
1971 opStr :: Name -> String
1963− opStr (NS n _) = opStr n
1972+ opStr (NS n _) = opStr n
1964− opStr (UN n) = T.unpack n
1973+ opStr (UN n) = T.unpack n
1966 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1975 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1967 slist' (Just d) _ _ _ | d <= 0 = Nothing
1976 slist' (Just d) _ _ _ | d <= 0 = Nothing
@@ -2023,7 +2032,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
2023 ellipsis = text "..."
2032 ellipsis = text "..."
2025 depth Nothing = id
2034 depth Nothing = id
2026− depth (Just d) = if d <= 0 then const (ellipsis) else id
2035+ depth (Just d) = if d <= 0 then const ellipsis else id
2028 decD = fmap (\x -> x - 1)
2037 decD = fmap (\x -> x - 1)
@@ -2038,7 +2047,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
2038-- | Strip away namespace information
2047-- | Strip away namespace information
2039basename :: Name -> Name
2048basename :: Name -> Name
2040basename (NS n _) = basename n
2049basename (NS n _) = basename n
2041−basename n = n
2050+basename n = n
2043-- | Determine whether a name was the one inserted for a hole or
2052-- | Determine whether a name was the one inserted for a hole or
2044-- guess by the delaborator
2053-- guess by the delaborator
@@ -2058,15 +2067,15 @@ prettyName
2058 -> Name -- ^^ the name to pprint
2067 -> Name -- ^^ the name to pprint
2059 -> Doc OutputAnnotation
2068 -> Doc OutputAnnotation
2060prettyName infixParen showNS bnd n
2069prettyName infixParen showNS bnd n
2061− | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2070+ | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2062− | (UN n') <- n, T.unpack n' == "_" = text "_"
2071+ | (UN n') <- n, T.unpack n' == "_" = text "_"
2063− | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2072+ | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2064− | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2073+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2065 where fullName = text nameSpace <> parenthesise (text (baseName n))
2074 where fullName = text nameSpace <> parenthesise (text (baseName n))
2066− baseName (UN n) = T.unpack n
2075+ baseName (UN n) = T.unpack n
2067− baseName (NS n ns) = baseName n
2076+ baseName (NS n ns) = baseName n
2068− baseName (MN i s) = T.unpack s
2077+ baseName (MN i s) = T.unpack s
2069− baseName other = show other
2078+ baseName other = show other
2070 nameSpace = case n of
2079 nameSpace = case n of
2071 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2080 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
@@ -2081,13 +2090,13 @@ showCImp ppo (PClause _ n l ws r w)
2081 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2090 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2082 <+> text "where" <+> text (show w)
2091 <+> text "where" <+> text (show w)
2084− showWs [] = empty
2093+ showWs [] = empty
2085 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2094 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2086showCImp ppo (PWith _ n l ws r pn w)
2095showCImp ppo (PWith _ n l ws r pn w)
2087 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2096 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2088 <+> braces (text (show w))
2097 <+> braces (text (show w))
2090− showWs [] = empty
2099+ showWs [] = empty
2091 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2100 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
@@ -2099,43 +2108,43 @@ showDImp ppo (PDatadecl n nfc ty cons)
2099showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2108showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2100showDecls o ds = vsep (map (showDeclImp o) ds)
2109showDecls o ds = vsep (map (showDeclImp o) ds)
2102−showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2111+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2103showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2112showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2104−showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2113+showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2105 indent 2 (vsep (map (showCImp o) cs))
2114 indent 2 (vsep (map (showCImp o) cs))
2106−showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2115+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2107−showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2116+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2108−showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2117+showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2109showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2118showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2110showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2119showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2111 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2120 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2112−showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
2121+showDeclImp o (PInstance _ _ _ _ cs acc n _ _ t _ ds)
2113 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2122 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2114showDeclImp _ _ = text "..."
2123showDeclImp _ _ = text "..."
2115-- showDeclImp (PImport o) = "import " ++ o
2124-- showDeclImp (PImport o) = "import " ++ o
2117getImps :: [PArg] -> [(Name, PTerm)]
2126getImps :: [PArg] -> [(Name, PTerm)]
2118getImps [] = []
2127getImps [] = []
2119−getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2128+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2120−getImps (_ : xs) = getImps xs
2129+getImps (_ : xs) = getImps xs
2122getExps :: [PArg] -> [PTerm]
2131getExps :: [PArg] -> [PTerm]
2123getExps [] = []
2132getExps [] = []
2124−getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2133+getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2125−getExps (_ : xs) = getExps xs
2134+getExps (_ : xs) = getExps xs
2127getShowArgs :: [PArg] -> [PArg]
2136getShowArgs :: [PArg] -> [PArg]
2128getShowArgs [] = []
2137getShowArgs [] = []
2129getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2138getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2130getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2139getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2131 | PImp _ _ _ _ tm <- e
2140 | PImp _ _ _ _ tm <- e
2132− , containsHole tm = e : getShowArgs xs
2141+ , containsHole tm = e : getShowArgs xs
2133getShowArgs (_ : xs) = getShowArgs xs
2142getShowArgs (_ : xs) = getShowArgs xs
2135getConsts :: [PArg] -> [PTerm]
2144getConsts :: [PArg] -> [PTerm]
2136−getConsts [] = []
2145+getConsts [] = []
2137getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2146getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2138−getConsts (_ : xs) = getConsts xs
2147+getConsts (_ : xs) = getConsts xs
2140getAll :: [PArg] -> [PTerm]
2149getAll :: [PArg] -> [PTerm]
2141getAll = map getTm
2150getAll = map getTm
@@ -2149,13 +2158,13 @@ showName :: Maybe IState -- ^^ the Idris state, for information about names an
2149 -> Name -- ^^ the term to show
2158 -> Name -- ^^ the term to show
2150 -> String
2159 -> String
2151showName ist bnd ppo colour n = case ist of
2160showName ist bnd ppo colour n = case ist of
2152− Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2161+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2153− Nothing -> showbasic n
2162+ Nothing -> showbasic n
2154 where name = if ppopt_impl ppo then show n else showbasic n
2163 where name = if ppopt_impl ppo then show n else showbasic n
2155− showbasic n@(UN _) = showCG n
2164+ showbasic n@(UN _) = showCG n
2156− showbasic (MN i s) = str s
2165+ showbasic (MN i s) = str s
2157− showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2166+ showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2158− showbasic (SN s) = show s
2167+ showbasic (SN s) = show s
2159 fst3 (x, _, _) = x
2168 fst3 (x, _, _) = x
2160 colourise n t = let ctxt' = fmap tt_ctxt ist in
2169 colourise n t = let ctxt' = fmap tt_ctxt ist in
2161 case ctxt' of
2170 case ctxt' of
@@ -2187,42 +2196,42 @@ showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2189instance Sized PTerm where
2198instance Sized PTerm where
2190− size (PQuote rawTerm) = size rawTerm
2199+ size (PQuote rawTerm) = size rawTerm
2191− size (PRef fc _ name) = size name
2200+ size (PRef fc _ name) = size name
2192− size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2201+ size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2193− size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2202+ size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2194− size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2203+ size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2195− size (PTyped trm ty) = 1 + size trm + size ty
2204+ size (PTyped trm ty) = 1 + size trm + size ty
2196− size (PApp fc name args) = 1 + size args
2205+ size (PApp fc name args) = 1 + size args
2197− size (PAppBind fc name args) = 1 + size args
2206+ size (PAppBind fc name args) = 1 + size args
2198− size (PCase fc trm bdy) = 1 + size trm + size bdy
2207+ size (PCase fc trm bdy) = 1 + size trm + size bdy
2199− size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2208+ size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2200− size (PTrue fc _) = 1
2209+ size (PTrue fc _) = 1
2201− size (PResolveTC fc) = 1
2210+ size (PResolveTC fc) = 1
2202− size (PRewrite fc left right _) = 1 + size left + size right
2211+ size (PRewrite fc left right _) = 1 + size left + size right
2203− size (PPair fc _ _ left right) = 1 + size left + size right
2212+ size (PPair fc _ _ left right) = 1 + size left + size right
2204− size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2213+ size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2205− size (PAlternative _ a alts) = 1 + size alts
2214+ size (PAlternative _ a alts) = 1 + size alts
2206− size (PHidden hidden) = size hidden
2215+ size (PHidden hidden) = size hidden
2207− size (PUnifyLog tm) = size tm
2216+ size (PUnifyLog tm) = size tm
2208− size (PDisamb _ tm) = size tm
2217+ size (PDisamb _ tm) = size tm
2209− size (PNoImplicits tm) = size tm
2218+ size (PNoImplicits tm) = size tm
2210− size (PType _) = 1
2219+ size (PType _) = 1
2211− size (PUniverse _) = 1
2220+ size (PUniverse _) = 1
2212− size (PConstant fc const) = 1 + size fc + size const
2221+ size (PConstant fc const) = 1 + size fc + size const
2213− size Placeholder = 1
2222+ size Placeholder = 1
2214− size (PDoBlock dos) = 1 + size dos
2223+ size (PDoBlock dos) = 1 + size dos
2215− size (PIdiom fc term) = 1 + size term
2224+ size (PIdiom fc term) = 1 + size term
2216− size (PReturn fc) = 1
2225+ size (PReturn fc) = 1
2217− size (PMetavar _ name) = 1
2226+ size (PMetavar _ name) = 1
2218− size (PProof tactics) = size tactics
2227+ size (PProof tactics) = size tactics
2219− size (PElabError err) = size err
2228+ size (PElabError err) = size err
2220− size PImpossible = 1
2229+ size PImpossible = 1
2221− size _ = 0
2230+ size _ = 0
2223getPArity :: PTerm -> Int
2232getPArity :: PTerm -> Int
2224−getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2233+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2225−getPArity _ = 0
2234+getPArity _ = 0
2227-- Return all names, free or globally bound, in the given term.
2236-- Return all names, free or globally bound, in the given term.
@@ -2230,31 +2239,30 @@ allNamesIn :: PTerm -> [Name]
2230allNamesIn tm = nub $ ni 0 [] tm
2239allNamesIn tm = nub $ ni 0 [] tm
2231 where -- TODO THINK added niTacImp, but is it right?
2240 where -- TODO THINK added niTacImp, but is it right?
2232 ni 0 env (PRef _ _ n)
2241 ni 0 env (PRef _ _ n)
2233− | not (n `elem` env) = [n]
2242+ | not (n `elem` env) = [n]
2234− ni 0 env (PPatvar _ n) = [n]
2243+ ni 0 env (PPatvar _ n) = [n]
2235− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2244+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2236− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2245+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2237− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)
2246+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2238− ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2247+ ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2239− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2248+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2240− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2249+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2241− ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2250+ ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2242− ni 0 env (PHidden tm) = ni 0 env tm
2251+ ni 0 env (PHidden tm) = ni 0 env tm
2243− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2252+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2244− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2253+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2245− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2254+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2246− ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2255+ ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2247− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2256+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2248− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2257+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2249− ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2258+ ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2250− ni 0 env (PUnifyLog tm) = ni 0 env tm
2259+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2251− ni 0 env (PDisamb _ tm) = ni 0 env tm
2260+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2252− ni 0 env (PNoImplicits tm) = ni 0 env tm
2261+ ni 0 env (PNoImplicits tm) = ni 0 env tm
2254− ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2255− ni i env (PUnquote tm) = ni (i - 1) env tm
2263+ ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2264+ ni i env (PUnquote tm) = ni (i - 1) env tm
2257− ni i env tm = concatMap (ni i env) (children tm)
2265+ ni i env tm = concatMap (ni i env) (children tm)
2259 niTacImp i env (TacImp _ _ scr) = ni i env scr
2267 niTacImp i env (TacImp _ _ scr) = ni i env scr
2260 niTacImp _ _ _ = []
2268 niTacImp _ _ _ = []
@@ -2265,32 +2273,32 @@ boundNamesIn :: PTerm -> [Name]
2265boundNamesIn tm = S.toList (ni 0 S.empty tm)
2273boundNamesIn tm = S.toList (ni 0 S.empty tm)
2266 where -- TODO THINK Added niTacImp, but is it right?
2274 where -- TODO THINK Added niTacImp, but is it right?
2267 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2275 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2268− ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2276+ ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2269− ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2277+ ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2270− ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2278+ ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2271− ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2279+ ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2272− ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2280+ ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2273− ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2281+ ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2274− ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2282+ ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2275− ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r
2283+ ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r
2276− ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2284+ ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2277− ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2285+ ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2278 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2286 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2279− ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2287+ ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2280− ni 0 set (PAlternative ns a as) = niTms 0 set as
2288+ ni 0 set (PAlternative ns a as) = niTms 0 set as
2281− ni 0 set (PHidden tm) = ni 0 set tm
2289+ ni 0 set (PHidden tm) = ni 0 set tm
2282− ni 0 set (PUnifyLog tm) = ni 0 set tm
2290+ ni 0 set (PUnifyLog tm) = ni 0 set tm
2283− ni 0 set (PDisamb _ tm) = ni 0 set tm
2291+ ni 0 set (PDisamb _ tm) = ni 0 set tm
2284− ni 0 set (PNoImplicits tm) = ni 0 set tm
2292+ ni 0 set (PNoImplicits tm) = ni 0 set tm
2286− ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2294+ ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2287− ni i set (PUnquote tm) = ni (i - 1) set tm
2295+ ni i set (PUnquote tm) = ni (i - 1) set tm
2289− ni i set tm = foldr S.union set (map (ni i set) (children tm))
2297+ ni i set tm = foldr (S.union . ni i set) set (children tm)
2291 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2299 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2292− niTms i set [] = set
2300+ niTms i set [] = set
2293− niTms i set (x : xs) = niTms i (ni i set x) xs
2301+ niTms i set (x : xs) = niTms i (ni i set x) xs
2295 niTacImp i set (TacImp _ _ scr) = ni i set scr
2303 niTacImp i set (TacImp _ _ scr) = ni i set scr
2296 niTacImp i set _ = set
2304 niTacImp i set _ = set
@@ -2306,18 +2314,18 @@ implicitNamesIn uvars ist tm
2306 addFn n = do (imps, fns) <- get
2314 addFn n = do (imps, fns) <- get
2307 put (imps, n: fns)
2315 put (imps, n: fns)
2309− notCAF [] = False
2317+ notCAF [] = False
2310 notCAF (PExp _ _ _ _ : _) = True
2318 notCAF (PExp _ _ _ _ : _) = True
2311− notCAF (_ : xs) = notCAF xs
2319+ notCAF (_ : xs) = notCAF xs
2313 notHidden (n, _) = case getAccessibility n of
2321 notHidden (n, _) = case getAccessibility n of
2314− Hidden -> False
2322+ Hidden -> False
2315− _ -> True
2323+ _ -> True
2317 getAccessibility n
2325 getAccessibility n
2318 = case lookupDefAccExact n False (tt_ctxt ist) of
2326 = case lookupDefAccExact n False (tt_ctxt ist) of
2319− Just (n,t) -> t
2327+ Just (n,t) -> t
2320− _ -> Public
2328+ _ -> Public
2322 ni 0 env (PRef _ _ n@(NS _ _))
2330 ni 0 env (PRef _ _ n@(NS _ _))
2323 | not (n `elem` env)
2331 | not (n `elem` env)
@@ -2327,44 +2335,44 @@ implicitNamesIn uvars ist tm
2327 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2335 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2328 ni 0 env (PApp _ f@(PRef _ _ n) as)
2336 ni 0 env (PApp _ f@(PRef _ _ n) as)
2329 | n `elem` uvars = do ni 0 env f
2337 | n `elem` uvars = do ni 0 env f
2330− mapM_ (ni 0 env) (map getTm as)
2338+ mapM_ (ni 0 env . getTm) as
2331 | otherwise = do case lookupTy n (tt_ctxt ist) of
2339 | otherwise = do case lookupTy n (tt_ctxt ist) of
2332− [] -> return ()
2340+ [] -> return ()
2333− _ -> addFn n
2341+ _ -> addFn n
2334− mapM_ (ni 0 env) (map getTm as)
2342+ mapM_ (ni 0 env . getTm) as
2335 ni 0 env (PApp _ f as) = do ni 0 env f
2343 ni 0 env (PApp _ f as) = do ni 0 env f
2336− mapM_ (ni 0 env) (map getTm as)
2344+ mapM_ (ni 0 env . getTm) as
2337 ni 0 env (PAppBind _ f as) = do ni 0 env f
2345 ni 0 env (PAppBind _ f as) = do ni 0 env f
2338− mapM_ (ni 0 env) (map getTm as)
2346+ mapM_ (ni 0 env . getTm) as
2339 ni 0 env (PCase _ c os) = do ni 0 env c
2347 ni 0 env (PCase _ c os) = do ni 0 env c
2340 -- names in 'os', not counting the names bound in the cases
2348 -- names in 'os', not counting the names bound in the cases
2341− mapM_ (ni 0 env) (map snd os)
2349+ mapM_ (ni 0 env . snd) os
2342 (imps, fns) <- get
2350 (imps, fns) <- get
2343 put ([] ,[])
2351 put ([] ,[])
2344− mapM_ (ni 0 env) (map fst os)
2352+ mapM_ (ni 0 env . fst) os
2345 (impsfst, _) <- get
2353 (impsfst, _) <- get
2346 put (nub imps \\ nub impsfst, fns)
2354 put (nub imps \\ nub impsfst, fns)
2347− ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2355+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2348− ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2356+ ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2349− ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2357+ ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2350− ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r
2358+ ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r
2351− ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2359+ ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2352− ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2360+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2353− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2361+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2354− ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2362+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2355− ni 0 env t
2363+ ni 0 env t
2356− ni 0 env r
2364+ ni 0 env r
2357− ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2365+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2358− ni 0 env (PHidden tm) = ni 0 env tm
2366+ ni 0 env (PHidden tm) = ni 0 env tm
2359− ni 0 env (PUnifyLog tm) = ni 0 env tm
2367+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2360− ni 0 env (PDisamb _ tm) = ni 0 env tm
2368+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2361− ni 0 env (PNoImplicits tm) = ni 0 env tm
2369+ ni 0 env (PNoImplicits tm) = ni 0 env tm
2363 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2371 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2364 maybe (return ()) (ni i env) ty
2372 maybe (return ()) (ni i env) ty
2365 ni i env (PUnquote tm) = ni (i - 1) env tm
2373 ni i env (PUnquote tm) = ni (i - 1) env tm
2367− ni i env tm = mapM_ (ni i env) (children tm)
2375+ ni i env tm = mapM_ (ni i env) (children tm)
2369-- Return names which are free in the given term.
2377-- Return names which are free in the given term.
2370namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2378namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
@@ -2373,32 +2381,32 @@ namesIn uvars ist tm = nub $ ni 0 [] tm
2373 ni 0 env (PRef _ _ n)
2381 ni 0 env (PRef _ _ n)
2374 | not (n `elem` env)
2382 | not (n `elem` env)
2375 = case lookupTy n (tt_ctxt ist) of
2383 = case lookupTy n (tt_ctxt ist) of
2376− [] -> [n]
2384+ [] -> [n]
2377− _ -> if n `elem` (map fst uvars) then [n] else []
2385+ _ -> [n | n `elem` (map fst uvars)]
2378− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2386+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2379− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2387+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2380− ni 0 env (PCase _ c os) = ni 0 env c ++
2388+ ni 0 env (PCase _ c os) = ni 0 env c ++
2381 -- names in 'os', not counting the names bound in the cases
2389 -- names in 'os', not counting the names bound in the cases
2382− (nub (concatMap (ni 0 env) (map snd os))
2390+ (nub (concatMap (ni 0 env . snd) os)
2383− \\ nub (concatMap (ni 0 env) (map fst os)))
2391+ \\ nub (concatMap (ni 0 env . fst) os))
2384− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2392+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2385 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2393 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2386− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2394+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2387− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2395+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2388− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2396+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2389− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2397+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2390 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2398 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2391− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2399+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2392 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2400 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2393− ni 0 env (PHidden tm) = ni 0 env tm
2401+ ni 0 env (PHidden tm) = ni 0 env tm
2394− ni 0 env (PUnifyLog tm) = ni 0 env tm
2402+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2395− ni 0 env (PDisamb _ tm) = ni 0 env tm
2403+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2396− ni 0 env (PNoImplicits tm) = ni 0 env tm
2404+ ni 0 env (PNoImplicits tm) = ni 0 env tm
2398− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2406+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2399− ni i env (PUnquote tm) = ni (i - 1) env tm
2407+ ni i env (PUnquote tm) = ni (i - 1) env tm
2401− ni i env tm = concatMap (ni i env) (children tm)
2409+ ni i env tm = concatMap (ni i env) (children tm)
2403 niTacImp i env (TacImp _ _ scr) = ni i env scr
2411 niTacImp i env (TacImp _ _ scr) = ni i env scr
2404 niTacImp _ _ _ = []
2412 niTacImp _ _ _ = []
@@ -2413,27 +2421,27 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm
2413 = case lookupDefExact n (tt_ctxt ist) of
2421 = case lookupDefExact n (tt_ctxt ist) of
2414 Nothing -> [n]
2422 Nothing -> [n]
2416− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2424+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2417− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2425+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2418− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)
2426+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2419− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2427+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2420− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2428+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2421− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2429+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2422− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2430+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2423− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2431+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2424− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2432+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2425 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2433 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2426− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2434+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2427 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2435 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2428− ni 0 env (PHidden tm) = ni 0 env tm
2436+ ni 0 env (PHidden tm) = ni 0 env tm
2429− ni 0 env (PUnifyLog tm) = ni 0 env tm
2437+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2430− ni 0 env (PDisamb _ tm) = ni 0 env tm
2438+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2431− ni 0 env (PNoImplicits tm) = ni 0 env tm
2439+ ni 0 env (PNoImplicits tm) = ni 0 env tm
2433− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2441+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2434− ni i env (PUnquote tm) = ni (i - 1) env tm
2442+ ni i env (PUnquote tm) = ni (i - 1) env tm
2436− ni i env tm = concatMap (ni i env) (children tm)
2444+ ni i env tm = concatMap (ni i env) (children tm)
2438 niTacImp i env (TacImp _ _ scr) = ni i env scr
2446 niTacImp i env (TacImp _ _ scr) = ni i env scr
2439 niTacImp _ _ _ = []
2447 niTacImp _ _ _ = []