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