@@ -94,6 +94,7 @@ data IOption = IOption {
9494 , opt_printdepth :: Maybe Int
9595 , opt_evaltypes :: Bool -- ^ normalise types in :t
9696 , opt_desugarnats :: Bool
97+ , opt_autoimpls :: Bool
9798 } deriving (Show, Eq)
9899
99100defaultOpts = IOption { opt_logLevel = 0
@@ -121,6 +122,7 @@ defaultOpts = IOption { opt_logLevel = 0
121122 , opt_printdepth = Just 5000
122123 , opt_evaltypes = True
123124 , opt_desugarnats = False
125+ , opt_autoimpls = True
124126 }
125127
126128data PPOption = PPOption {
@@ -194,7 +196,6 @@ data IState = IState {
194196 -- ^ list of lhs/rhs, and a list of missing clauses
195197 idris_flags :: Ctxt [FnOpt],
196198 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
197− idris_calledgraph :: Ctxt [Name],
198199 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
199200 idris_moduledocs :: Ctxt (Docstring DocTerm),
200201 -- ^ module documentation is saved in a special MN so the context
@@ -235,7 +236,7 @@ data IState = IState {
235236 brace_stack :: [Maybe Int],
236237 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
237238 idris_parsedSpan :: Maybe FC,
238− hide_list :: [(Name, Maybe Accessibility)],
239+ hide_list :: Ctxt Accessibility,
239240 default_access :: Accessibility,
240241 default_total :: Bool,
241242 ibc_write :: [IBCWrite],
@@ -262,7 +263,9 @@ data IState = IState {
262263 idris_exports :: [Name], -- ^ Functions with ExportList
263264 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
264265 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)
266269 }
267270
268271-- Required for parsers library, and therefore trifecta
@@ -279,11 +282,10 @@ deriving instance NFData SizeChange
279282type SCGEntry = (Name, [Maybe (Int, SizeChange)])
280283type UsageReason = (Name, Int) -- fn_name, its_arg_number
281284
282−data CGInfo = CGInfo { argsdef :: [Name],
283− calls :: [(Name, [[Name]])],
285+data CGInfo = CGInfo { calls :: [Name],
284286 scg :: [SCGEntry],
285− argsused :: [Name],
286− usedpos :: [(Int, [UsageReason])] }
287+ usedpos :: [(Int, [UsageReason])]
288+ }
287289 deriving Show
288290{-!
289291deriving instance Binary CGInfo
@@ -348,12 +350,13 @@ idrisInit = IState initContext S.empty []
348350 emptyContext emptyContext emptyContext emptyContext
349351 emptyContext emptyContext emptyContext emptyContext
350352 emptyContext emptyContext emptyContext emptyContext
351− emptyContext emptyContext
353+ emptyContext
352354 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
353− [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
355+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Hidden False [] Nothing [] []
354356 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
355357 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
356− emptyContext
358+ emptyContext S.empty M.empty
359+
357360
358361-- | The monad for the main REPL - reading and processing files and updating
359362-- global state (hence the IO inner monad).
@@ -631,13 +634,17 @@ is_scoped :: Plicity -> Maybe ImplicitInfo
631634is_scoped (Imp _ _ _ s) = s
632635is_scoped _ = Nothing
633636
634−impl = Imp [] Dynamic False (Just (Impl False True))
635−forall_imp = Imp [] Dynamic False (Just (Impl False False))
637+impl = Imp [] Dynamic False (Just (Impl False True))
638+
639+forall_imp = Imp [] Dynamic False (Just (Impl False False))
636640forall_constraint = Imp [] Dynamic False (Just (Impl True False))
637−expl = Exp [] Dynamic False
638−expl_param = Exp [] Dynamic True
639−constraint = Constraint [] Static
640−tacimpl t = TacImp [] Dynamic t
641+
642+expl = Exp [] Dynamic False
643+expl_param = Exp [] Dynamic True
644+
645+constraint = Constraint [] Static
646+
647+tacimpl t = TacImp [] Dynamic t
641648
642649data FnOpt = Inlinable -- always evaluate when simplifying
643650 | TotalFn | PartialFn | CoveringFn
@@ -695,7 +702,7 @@ data PDecl' t
695702 FC -- Record name precise location
696703 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
697704 [(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
699706 (Maybe (Name, FC)) -- Optional constructor name and location
700707 (Docstring (Either Err t)) -- Constructor doc
701708 SyntaxInfo -- Constructor SyntaxInfo
@@ -717,6 +724,7 @@ data PDecl' t
717724 [(Name, Docstring (Either Err t))] -- Parameter docs
718725 SyntaxInfo
719726 FC [(Name, t)] -- constraints
727+ Accessibility
720728 Name -- class
721729 FC -- precise location of class
722730 [t] -- parameters
@@ -756,6 +764,7 @@ data Directive = DLib Codegen String |
756764 DErrorHandlers Name FC Name FC [(Name, FC)] |
757765 DLanguage LanguageExt |
758766 DDeprecate Name String |
767+ DAutoImplicits Bool |
759768 DUsed FC Name Name
760769
761770-- | 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
875884 (map (mapPDeclFC f g) body)
876885 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
877886 ctorDoc
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) =
879888 PInstance doc paramDocs syn (f fc)
880889 (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)
882891 (mapPTermFC f g instTy)
883892 instN
884893 (map (mapPDeclFC f g) body)
@@ -918,7 +927,7 @@ declared (PParams _ _ ds) = concatMap declared ds
918927declared (PNamespace _ _ ds) = concatMap declared ds
919928declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
920929declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
921−declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
930+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
922931declared (PDSL n _) = [n]
923932declared (PSyntax _ _) = []
924933declared (PMutual _ ds) = concatMap declared ds
@@ -927,39 +936,39 @@ declared _ = []
927936
928937-- get the names declared, not counting nested parameter blocks
929938tldeclared :: PDecl -> [Name]
930−tldeclared (PFix _ _ _) = []
931−tldeclared (PTy _ _ _ _ _ n _ t) = [n]
932−tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
933−tldeclared (PClauses _ _ n _) = [] -- not a declaration
934−tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
939+tldeclared (PFix _ _ _) = []
940+tldeclared (PTy _ _ _ _ _ n _ t) = [n]
941+tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
942+tldeclared (PClauses _ _ n _) = [] -- not a declaration
943+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
935944tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
936945 where fstt (_, _, a, _, _, _, _) = a
937−tldeclared (PParams _ _ ds) = []
938−tldeclared (PMutual _ ds) = concatMap tldeclared ds
939−tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
940−tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
941−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
942−tldeclared _ = []
946+tldeclared (PParams _ _ ds) = []
947+tldeclared (PMutual _ ds) = concatMap tldeclared ds
948+tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
949+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
950+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
951+tldeclared _ = []
943952
944953defined :: PDecl -> [Name]
945−defined (PFix _ _ _) = []
946−defined (PTy _ _ _ _ _ n _ t) = []
947−defined (PPostulate _ _ _ _ _ _ n t) = []
948−defined (PClauses _ _ n _) = [n] -- not a declaration
949−defined (PCAF _ n _) = [n]
950−defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
954+defined (PFix _ _ _) = []
955+defined (PTy _ _ _ _ _ n _ t) = []
956+defined (PPostulate _ _ _ _ _ _ n t) = []
957+defined (PClauses _ _ n _) = [n] -- not a declaration
958+defined (PCAF _ n _) = [n]
959+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
951960 where fstt (_, _, a, _, _, _, _) = a
952−defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
953−defined (PParams _ _ ds) = concatMap defined ds
954−defined (PNamespace _ _ ds) = concatMap defined ds
955−defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
956−defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
957−defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
958−defined (PDSL n _) = [n]
959−defined (PSyntax _ _) = []
960−defined (PMutual _ ds) = concatMap defined ds
961−defined (PDirective _) = []
962−defined _ = []
961+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
962+defined (PParams _ _ ds) = concatMap defined ds
963+defined (PNamespace _ _ ds) = concatMap defined ds
964+defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
965+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
966+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
967+defined (PDSL n _) = [n]
968+defined (PSyntax _ _) = []
969+defined (PMutual _ ds) = concatMap defined ds
970+defined (PDirective _) = []
971+defined _ = []
963972
964973updateN :: [(Name, Name)] -> Name -> Name
965974updateN ns n | Just n' <- lookup n ns = n'
@@ -1040,33 +1049,33 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
10401049-- general-purpose FCs, and the second transforms those that are used
10411050-- for semantic source highlighting, so they can be treated specially.
10421051mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1043−mapPTermFC f g (PQuote q) = PQuote q
1044−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
1046−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)
1048−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)
1050−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)
1052−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)
1054−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)
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)
1057−mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1058−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)
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)
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)
1062−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)
1064−mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1065−mapPTermFC f g (PType fc) = PType (f fc)
1066−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)
1068−mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1069−mapPTermFC f g Placeholder = Placeholder
1052+mapPTermFC f g (PQuote q) = PQuote q
1053+mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1054+mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1055+mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1056+mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) 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)
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)
1059+mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1060+mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1061+mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1062+mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1063+mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1064+mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
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)
1066+mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1067+mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
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)
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)
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)
1071+mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1072+mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1073+mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1074+mapPTermFC f g (PType fc) = PType (f fc)
1075+mapPTermFC f g (PUniverse u) = PUniverse u
1076+mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1077+mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1078+mapPTermFC f g Placeholder = Placeholder
10701079mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
10711080 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
10721081 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)
10741083 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
10751084 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
10761085 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)
1078−mapPTermFC f g (PReturn fc) = PReturn (f fc)
1079−mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1080−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)
1082−mapPTermFC f g (PElabError err) = PElabError err
1083−mapPTermFC f g PImpossible = PImpossible
1084−mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1085−mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1086−mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1087−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)
1089−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
1091−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)
1086+mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1087+mapPTermFC f g (PReturn fc) = PReturn (f fc)
1088+mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1089+mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1090+mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1091+mapPTermFC f g (PElabError err) = PElabError err
1092+mapPTermFC f g PImpossible = PImpossible
1093+mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1094+mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1095+mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1096+mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1097+mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1098+mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1099+mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1100+mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1101+mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
10931102
10941103{-!
10951104dg instance Binary PTerm
@@ -1098,28 +1107,27 @@ deriving instance NFData PTerm
10981107
10991108mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
11001109mapPT f t = f (mpt t) where
1101− 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)
1103− 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)
1105− (fmap (mapPT f) g)
1106− 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)
1108− 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)
1110− 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)
1110+ mpt (PLam fc n nfc t s) = PLam fc 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)
1112+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1113+ mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1114+ mpt (PApp fc t as) = PApp 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)
1116+ mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1117+ mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1118+ mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1119+ mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
11121120 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)
1114− mpt (PHidden t) = PHidden (mapPT f t)
1115− mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1116− mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1117− mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1118− mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1119− mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1120− mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1121− mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1122− mpt x = x
1121+ mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1122+ mpt (PHidden t) = PHidden (mapPT f t)
1123+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1124+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1125+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1126+ mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1127+ mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1128+ mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1129+ mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1130+ mpt x = x
11231131
11241132
11251133data PTactic' t = Intro [Name] | Intros | Focus Name
@@ -1160,39 +1168,39 @@ deriving instance Binary PTactic'
11601168deriving instance NFData PTactic'
11611169!-}
11621170instance Sized a => Sized (PTactic' a) where
1163− size (Intro nms) = 1 + size nms
1164− size Intros = 1
1165− size (Focus nm) = 1 + size nm
1166− size (Refine nm bs) = 1 + size nm + length bs
1167− size (Rewrite t) = 1 + size t
1168− size (Induction t) = 1 + size t
1169− size (LetTac nm t) = 1 + size nm + size t
1170− size (Exact t) = 1 + size t
1171− size Compute = 1
1172− size Trivial = 1
1173− size Solve = 1
1174− size Attack = 1
1175− size ProofState = 1
1176− size ProofTerm = 1
1177− size Undo = 1
1178− size (Try l r) = 1 + size l + size r
1179− size (TSeq l r) = 1 + size l + size r
1180− size (ApplyTactic t) = 1 + size t
1181− size (Reflect t) = 1 + size t
1182− size (Fill t) = 1 + size t
1183− size Qed = 1
1184− size Abandon = 1
1185− size Skip = 1
1186− size (TFail ts) = 1 + size ts
1187− size SourceFC = 1
1188− size DoUnify = 1
1189− size (CaseTac x) = 1 + size x
1190− size (Equiv t) = 1 + size t
1191− size (Claim x y) = 1 + size x + size y
1192− size Unfocus = 1
1193− size (MatchRefine x) = 1 + size x
1171+ size (Intro nms) = 1 + size nms
1172+ size Intros = 1
1173+ size (Focus nm) = 1 + size nm
1174+ size (Refine nm bs) = 1 + size nm + length bs
1175+ size (Rewrite t) = 1 + size t
1176+ size (Induction t) = 1 + size t
1177+ size (LetTac nm t) = 1 + size nm + size t
1178+ size (Exact t) = 1 + size t
1179+ size Compute = 1
1180+ size Trivial = 1
1181+ size Solve = 1
1182+ size Attack = 1
1183+ size ProofState = 1
1184+ size ProofTerm = 1
1185+ size Undo = 1
1186+ size (Try l r) = 1 + size l + size r
1187+ size (TSeq l r) = 1 + size l + size r
1188+ size (ApplyTactic t) = 1 + size t
1189+ size (Reflect t) = 1 + size t
1190+ size (Fill t) = 1 + size t
1191+ size Qed = 1
1192+ size Abandon = 1
1193+ size Skip = 1
1194+ size (TFail ts) = 1 + size ts
1195+ size SourceFC = 1
1196+ size DoUnify = 1
1197+ size (CaseTac x) = 1 + size x
1198+ size (Equiv t) = 1 + size t
1199+ size (Claim x y) = 1 + size x + size y
1200+ size Unfocus = 1
1201+ size (MatchRefine x) = 1 + size x
11941202 size (LetTacTy x y z) = 1 + size x + size y + size z
1195− size TCInstance = 1
1203+ size TCInstance = 1
11961204
11971205type PTactic = PTactic' PTerm
11981206
@@ -1208,11 +1216,11 @@ deriving instance NFData PDo'
12081216!-}
12091217
12101218instance Sized a => Sized (PDo' a) where
1211− 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
1213− 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
1215− size (DoLetP fc l r) = 1 + size fc + size l + size r
1219+ size (DoExp fc t) = 1 + size fc + size t
1220+ size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1221+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1222+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1223+ size (DoLetP fc l r) = 1 + size fc + size l + size r
12161224
12171225type PDo = PDo' PTerm
12181226
@@ -1244,10 +1252,10 @@ data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
12441252 deriving (Show, Eq, Data, Typeable)
12451253
12461254instance Sized a => Sized (PArg' a) where
1247− size (PImp p _ l nm trm) = 1 + size nm + size trm
1248− 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
1250− size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1255+ size (PImp p _ l nm trm) = 1 + size nm + size trm
1256+ size (PExp p l nm trm) = 1 + size nm + size trm
1257+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1258+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
12511259
12521260{-!
12531261deriving instance Binary PArg'
@@ -1255,43 +1263,43 @@ deriving instance NFData PArg'
12551263!-}
12561264
12571265pimp n t mach = PImp 1 mach [] n t
1258−pexp t = PExp 1 [] (sMN 0 "arg") t
1259−pconst t = PConstraint 1 [] (sMN 0 "carg") t
1266+pexp t = PExp 1 [] (sMN 0 "arg") t
1267+pconst t = PConstraint 1 [] (sMN 0 "carg") t
12601268ptacimp n s t = PTacImplicit 2 [] n s t
12611269
12621270type PArg = PArg' PTerm
12631271
12641272-- | Get the highest FC in a term, if one exists
12651273highestFC :: PTerm -> Maybe FC
1266−highestFC (PQuote _) = Nothing
1267−highestFC (PRef fc _ _) = Just fc
1268−highestFC (PInferRef fc _ _) = Just fc
1269−highestFC (PPatvar fc _) = Just fc
1270−highestFC (PLam fc _ _ _ _) = Just fc
1271−highestFC (PPi _ _ _ _ _) = Nothing
1272−highestFC (PLet fc _ _ _ _ _) = Just fc
1273−highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1274−highestFC (PApp fc _ _) = Just fc
1275−highestFC (PAppBind fc _ _) = Just fc
1276−highestFC (PMatchApp fc _) = Just fc
1277−highestFC (PCase fc _ _) = Just fc
1278−highestFC (PIfThenElse fc _ _ _) = Just fc
1279−highestFC (PTrue fc _) = Just fc
1280−highestFC (PResolveTC fc) = Just fc
1281−highestFC (PRewrite fc _ _ _) = Just fc
1282−highestFC (PPair fc _ _ _ _) = Just fc
1283−highestFC (PDPair fc _ _ _ _ _) = Just fc
1284−highestFC (PAs fc _ _) = Just fc
1274+highestFC (PQuote _) = Nothing
1275+highestFC (PRef fc _ _) = Just fc
1276+highestFC (PInferRef fc _ _) = Just fc
1277+highestFC (PPatvar fc _) = Just fc
1278+highestFC (PLam fc _ _ _ _) = Just fc
1279+highestFC (PPi _ _ _ _ _) = Nothing
1280+highestFC (PLet fc _ _ _ _ _) = Just fc
1281+highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1282+highestFC (PApp fc _ _) = Just fc
1283+highestFC (PAppBind fc _ _) = Just fc
1284+highestFC (PMatchApp fc _) = Just fc
1285+highestFC (PCase fc _ _) = Just fc
1286+highestFC (PIfThenElse fc _ _ _) = Just fc
1287+highestFC (PTrue fc _) = Just fc
1288+highestFC (PResolveTC fc) = Just fc
1289+highestFC (PRewrite fc _ _ _) = Just fc
1290+highestFC (PPair fc _ _ _ _) = Just fc
1291+highestFC (PDPair fc _ _ _ _ _) = Just fc
1292+highestFC (PAs fc _ _) = Just fc
12851293highestFC (PAlternative _ _ args) =
12861294 case mapMaybe highestFC args of
12871295 [] -> Nothing
12881296 (fc:_) -> Just fc
1289−highestFC (PHidden _) = Nothing
1290−highestFC (PType fc) = Just fc
1291−highestFC (PUniverse _) = Nothing
1292−highestFC (PGoal fc _ _ _) = Just fc
1293−highestFC (PConstant fc _) = Just fc
1294−highestFC Placeholder = Nothing
1297+highestFC (PHidden _) = Nothing
1298+highestFC (PType fc) = Just fc
1299+highestFC (PUniverse _) = Nothing
1300+highestFC (PGoal fc _ _ _) = Just fc
1301+highestFC (PConstant fc _) = Just fc
1302+highestFC Placeholder = Nothing
12951303highestFC (PDoBlock lines) =
12961304 case map getDoFC lines of
12971305 [] -> Nothing
@@ -1303,23 +1311,23 @@ highestFC (PDoBlock lines) =
13031311 getDoFC (DoLet fc nm nfc l r) = fc
13041312 getDoFC (DoLetP fc l r) = fc
13051313
1306−highestFC (PIdiom fc _) = Just fc
1307−highestFC (PReturn fc) = Just fc
1308−highestFC (PMetavar fc _) = Just fc
1309−highestFC (PProof _) = Nothing
1310−highestFC (PTactics _) = Nothing
1311−highestFC (PElabError _) = Nothing
1312−highestFC PImpossible = Nothing
1313−highestFC (PCoerced tm) = highestFC tm
1314−highestFC (PDisamb _ opts) = highestFC opts
1315−highestFC (PUnifyLog tm) = highestFC tm
1316−highestFC (PNoImplicits tm) = highestFC tm
1317−highestFC (PQuasiquote _ _) = Nothing
1318−highestFC (PUnquote tm) = highestFC tm
1319−highestFC (PQuoteName _ _ fc) = Just fc
1320−highestFC (PRunElab fc _ _) = Just fc
1321−highestFC (PConstSugar fc _) = Just fc
1322−highestFC (PAppImpl t _) = highestFC t
1314+highestFC (PIdiom fc _) = Just fc
1315+highestFC (PReturn fc) = Just fc
1316+highestFC (PMetavar fc _) = Just fc
1317+highestFC (PProof _) = Nothing
1318+highestFC (PTactics _) = Nothing
1319+highestFC (PElabError _) = Nothing
1320+highestFC PImpossible = Nothing
1321+highestFC (PCoerced tm) = highestFC tm
1322+highestFC (PDisamb _ opts) = highestFC opts
1323+highestFC (PUnifyLog tm) = highestFC tm
1324+highestFC (PNoImplicits tm) = highestFC tm
1325+highestFC (PQuasiquote _ _) = Nothing
1326+highestFC (PUnquote tm) = highestFC tm
1327+highestFC (PQuoteName _ _ fc) = Just fc
1328+highestFC (PRunElab fc _ _) = Just fc
1329+highestFC (PConstSugar fc _) = Just fc
1330+highestFC (PAppImpl t _) = highestFC t
13231331
13241332-- Type class data
13251333
@@ -1397,11 +1405,11 @@ data Syntax = Rule [SSymbol] PTerm SynContext
13971405
13981406syntaxNames :: Syntax -> [Name]
13991407syntaxNames (Rule syms _ _) = mapMaybe ename syms
1400− where ename (Keyword n) = Just n
1401− ename _ = Nothing
1408+ where ename (Keyword n) = Just n
1409+ ename _ = Nothing
14021410syntaxNames (DeclRule syms _) = mapMaybe ename syms
1403− where ename (Keyword n) = Just n
1404− ename _ = Nothing
1411+ where ename (Keyword n) = Just n
1412+ ename _ = Nothing
14051413
14061414syntaxSymbols :: Syntax -> [SSymbol]
14071415syntaxSymbols (Rule ss _ _) = ss
@@ -1434,9 +1442,9 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
14341442 where
14351443 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
14361444
1437− ruleSort [] [] = EQ
1438− ruleSort [] _ = LT
1439− ruleSort _ [] = GT
1445+ ruleSort [] [] = EQ
1446+ ruleSort [] _ = LT
1447+ ruleSort _ [] = GT
14401448 ruleSort (s1:ss1) (s2:ss2) =
14411449 case symCompare s1 s2 of
14421450 EQ -> ruleSort ss1 ss2
@@ -1444,25 +1452,25 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
14441452
14451453 -- Better than creating Ord instance for SSymbol since
14461454 -- in general this ordering does not really make sense.
1447− symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1448− symCompare (Keyword _) _ = LT
1449− symCompare (Symbol _) (Keyword _) = GT
1450− symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1451− symCompare (Symbol _) _ = LT
1452− symCompare (Binding _) (Keyword _) = GT
1453− symCompare (Binding _) (Symbol _) = GT
1454− symCompare (Binding b1) (Binding b2) = compare b1 b2
1455− symCompare (Binding _) _ = LT
1456− symCompare (Expr _) (Keyword _) = GT
1457− symCompare (Expr _) (Symbol _) = GT
1458− symCompare (Expr _) (Binding _) = GT
1459− symCompare (Expr e1) (Expr e2) = compare e1 e2
1460− symCompare (Expr _) _ = LT
1461− symCompare (SimpleExpr _) (Keyword _) = GT
1462− symCompare (SimpleExpr _) (Symbol _) = GT
1463− symCompare (SimpleExpr _) (Binding _) = GT
1464− symCompare (SimpleExpr _) (Expr _) = GT
1465− symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1455+ symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1456+ symCompare (Keyword _) _ = LT
1457+ symCompare (Symbol _) (Keyword _) = GT
1458+ symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1459+ symCompare (Symbol _) _ = LT
1460+ symCompare (Binding _) (Keyword _) = GT
1461+ symCompare (Binding _) (Symbol _) = GT
1462+ symCompare (Binding b1) (Binding b2) = compare b1 b2
1463+ symCompare (Binding _) _ = LT
1464+ symCompare (Expr _) (Keyword _) = GT
1465+ symCompare (Expr _) (Symbol _) = GT
1466+ symCompare (Expr _) (Binding _) = GT
1467+ symCompare (Expr e1) (Expr e2) = compare e1 e2
1468+ symCompare (Expr _) _ = LT
1469+ symCompare (SimpleExpr _) (Keyword _) = GT
1470+ symCompare (SimpleExpr _) (Symbol _) = GT
1471+ symCompare (SimpleExpr _) (Binding _) = GT
1472+ symCompare (SimpleExpr _) (Expr _) = GT
1473+ symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
14661474
14671475initDSL = DSL (PRef f [] (sUN ">>="))
14681476 (PRef f [] (sUN "return"))
@@ -1534,10 +1542,10 @@ getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
15341542getInferTerm (App _ (App _ _ _) tm) = tm
15351543getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
15361544
1537−getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1538− where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1539− toTy (PVar t) = PVTy t
1540− toTy b = b
1545+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1546+ where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1547+ toTy (PVar t) = PVTy t
1548+ toTy b = b
15411549getInferType (App _ (App _ _ ty) _) = ty
15421550
15431551
@@ -1562,9 +1570,9 @@ pairCon = sNS (sUN "MkPair") ["Builtins"]
15621570upairTy = sNS (sUN "UPair") ["Builtins"]
15631571upairCon = sNS (sUN "MkUPair") ["Builtins"]
15641572
1565−eqTy = sUN "="
1573+eqTy = sUN "="
15661574eqCon = sUN "Refl"
1567−eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1575+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
15681576 "The propositional equality type. A proof that `x` = `y`." ++
15691577 "\n\n" ++
15701578 "To use such a proof, pattern-match on it, and the two equal things will " ++
@@ -1607,8 +1615,8 @@ modDocName :: Name
16071615modDocName = sMN 0 "ModuleDocs"
16081616
16091617-- Defined in builtins.idr
1610−sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1611−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1618+sigmaTy = sNS (sUN "DPair") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
16121620
16131621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
16141622piBind = piBindp expl
@@ -1648,11 +1656,11 @@ annotationColour ist (AnnConst c) =
16481656 in Just $ if constIsType c
16491657 then typeColour theme
16501658 else dataColour theme
1651−annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1652−annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1653−annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1659+annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1660+annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1661+annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
16541662annotationColour 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)
16561664annotationColour ist (AnnName n _ _ _) =
16571665 let ctxt = tt_ctxt ist
16581666 theme = idris_colourTheme ist
@@ -1738,7 +1746,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17381746
17391747 st =
17401748 case s of
1741− Static -> text "[static]" <> space
1749+ Static -> text "%static" <> space
17421750 _ -> empty
17431751 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
17441752 | ppopt_impl ppo =
@@ -1749,12 +1757,12 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17491757 where
17501758 st =
17511759 case s of
1752− Static -> text "[static]" <> space
1760+ Static -> text "%static" <> space
17531761 _ -> empty
17541762 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
17551763 depth d . bracket p startPrec $
17561764 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) =
17581766 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
17591767 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
17601768 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
17911799 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
17921800 [l,r] -> let precedence = maybe (startPrec - 1) prec f
17931801 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1794− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1802+ (l@(PExp{}) : r@(PExp{}) : rest) ->
17951803 depth d . bracket p funcAppPrec $
17961804 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
17971805 align (group (vsep (map (prettyArgS d bnd) rest)))
@@ -1842,20 +1850,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18421850 -- disambiguation on PDPair.
18431851 vars tm = filter noNS (allNamesIn tm)
18441852 noNS (NS _ _) = False
1845− noNS _ = True
1853+ noNS _ = True
18461854
18471855 prettySe d p bnd (PIfThenElse _ c t f) =
18481856 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
18501858 , kwd "then" <+> prettySe (decD d) startPrec bnd t
18511859 , kwd "else" <+> prettySe (decD d) startPrec bnd f
18521860 ]
1853− prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1854− prettySe d p bnd (PResolveTC _) = kwd "%instance"
1855− prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1856− prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1861+ prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1862+ prettySe d p bnd (PResolveTC _) = kwd "%instance"
1863+ prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1864+ prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
18571865 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1858− prettySe d p bnd (PRewrite _ l r _) =
1866+ prettySe d p bnd (PRewrite _ l r _) =
18591867 depth d . bracket p startPrec $
18601868 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
18611869 prettySe d p bnd (PTyped l r) =
@@ -1865,9 +1873,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18651873 align . group . vsep . punctuate (ann comma) $
18661874 map (prettySe (decD d) startPrec bnd) elts
18671875 where ann = case pun of
1868− TypeOrTerm -> id
1869− IsType -> annName pairTy
1870− IsTerm -> annName pairCon
1876+ TypeOrTerm -> id
1877+ IsType -> annName pairTy
1878+ IsTerm -> annName pairCon
18711879 prettySe d p bnd (PDPair _ _ pun l t r) =
18721880 depth d $
18731881 annotated lparen <>
@@ -1876,30 +1884,32 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18761884 prettySe (decD d) startPrec (addBinding bnd) r <>
18771885 annotated rparen
18781886 where annotated = case pun of
1879− IsType -> annName sigmaTy
1880− IsTerm -> annName sigmaCon
1881− TypeOrTerm -> id
1887+ IsType -> annName sigmaTy
1888+ IsTerm -> annName sigmaCon
1889+ TypeOrTerm -> id
18821890 (left, addBinding) = case (l, pun) of
18831891 (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)
18851893 prettySe d p bnd (PAlternative ns a as) =
18861894 lparen <> text "|" <> prettyAs <> text "|" <> rparen
18871895 where
18881896 prettyAs =
1889− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1890− 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)
1892− prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1897+ foldr ((\ l r -> l <+> text "," <+> r) .
1898+ depth d . prettySe (decD d) startPrec bnd)
1899+ empty as
1900+ prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1901+ prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1902+ prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
18931903 -- XXX: add pretty for tactics
1894− prettySe d p bnd (PProof ts) =
1904+ prettySe d p bnd (PProof ts) =
18951905 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1896− prettySe d p bnd (PTactics ts) =
1906+ prettySe d p bnd (PTactics ts) =
18971907 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1898− 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"
1900− prettySe d p bnd PImpossible = kwd "impossible"
1901− prettySe d p bnd Placeholder = text "_"
1902− prettySe d p bnd (PDoBlock dos) =
1908+ prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1909+ prettySe d p bnd (PReturn f) = kwd "return"
1910+ prettySe d p bnd PImpossible = kwd "impossible"
1911+ prettySe d p bnd Placeholder = text "_"
1912+ prettySe d p bnd (PDoBlock dos) =
19031913 bracket p startPrec $
19041914 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
19051915 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
19211931 text "no pretty printer for pattern-matching do binding" :
19221932 ppdo bnd dos
19231933 ppdo _ [] = []
1924− prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1925− prettySe d p bnd (PElabError s) = pretty s
1934+ prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1935+ prettySe d p bnd (PElabError s) = pretty s
19261936 -- 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 ")"
19281938 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
1930− prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1939+ prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1940+ prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
19311941 where start = if res then "`{" else "`{{"
19321942 end = if res then "}" else "}}"
1933− prettySe d p bnd (PRunElab _ tm _) =
1943+ prettySe d p bnd (PRunElab _ tm _) =
19341944 bracket p funcAppPrec . group . align . hang 2 $
19351945 text "%runElab" <$>
19361946 prettySe (decD d) funcAppPrec bnd tm
1937− prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1938−
1939− prettySe d p bnd _ = text "missing pretty-printer for term"
1947+ prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1948+ prettySe d p bnd _ = text "missing pretty-printer for term"
19401949
19411950 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
19421951 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
19431952 where display (UN n) = T.unpack n
19441953 display (MN _ n) = T.unpack n
19451954 -- 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
19471956 display n = show n
19481957
1949− prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1950− prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1951− prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1952− prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1958+ prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1959+ prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1960+ prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1961+ prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
19531962
1954− 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
1956− prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1963+ prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1964+ prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1965+ prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
19571966 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
19581967
19591968 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
19601969 annName n = annotate (AnnName n Nothing Nothing Nothing)
19611970
19621971 opStr :: Name -> String
1963− opStr (NS n _) = opStr n
1964− opStr (UN n) = T.unpack n
1972+ opStr (NS n _) = opStr n
1973+ opStr (UN n) = T.unpack n
19651974
19661975 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
19671976 slist' (Just d) _ _ _ | d <= 0 = Nothing
@@ -2023,7 +2032,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20232032 ellipsis = text "..."
20242033
20252034 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
20272036
20282037 decD = fmap (\x -> x - 1)
20292038
@@ -2038,7 +2047,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20382047-- | Strip away namespace information
20392048basename :: Name -> Name
20402049basename (NS n _) = basename n
2041−basename n = n
2050+basename n = n
20422051
20432052-- | Determine whether a name was the one inserted for a hole or
20442053-- guess by the delaborator
@@ -2058,15 +2067,15 @@ prettyName
20582067 -> Name -- ^^ the name to pprint
20592068 -> Doc OutputAnnotation
20602069prettyName infixParen showNS bnd n
2061− | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2062− | (UN n') <- n, T.unpack n' == "_" = text "_"
2063− | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2064− | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2070+ | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2071+ | (UN n') <- n, T.unpack n' == "_" = text "_"
2072+ | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2073+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
20652074 where fullName = text nameSpace <> parenthesise (text (baseName n))
2066− baseName (UN n) = T.unpack n
2067− baseName (NS n ns) = baseName n
2068− baseName (MN i s) = T.unpack s
2069− baseName other = show other
2075+ baseName (UN n) = T.unpack n
2076+ baseName (NS n ns) = baseName n
2077+ baseName (MN i s) = T.unpack s
2078+ baseName other = show other
20702079 nameSpace = case n of
20712080 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
20722081 _ -> ""
@@ -2081,13 +2090,13 @@ showCImp ppo (PClause _ n l ws r w)
20812090 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
20822091 <+> text "where" <+> text (show w)
20832092 where
2084− showWs [] = empty
2093+ showWs [] = empty
20852094 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
20862095showCImp ppo (PWith _ n l ws r pn w)
20872096 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
20882097 <+> braces (text (show w))
20892098 where
2090− showWs [] = empty
2099+ showWs [] = empty
20912100 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
20922101
20932102
@@ -2099,43 +2108,43 @@ showDImp ppo (PDatadecl n nfc ty cons)
20992108showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
21002109showDecls o ds = vsep (map (showDeclImp o) ds)
21012110
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))
21032112showDeclImp 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" <+>
21052114 indent 2 (vsep (map (showCImp o) cs))
2106−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)
2108−showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2115+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2116+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2117+showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
21092118showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
21102119showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
21112120 = 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)
21132122 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
21142123showDeclImp _ _ = text "..."
21152124-- showDeclImp (PImport o) = "import " ++ o
21162125
21172126getImps :: [PArg] -> [(Name, PTerm)]
21182127getImps [] = []
2119−getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2120−getImps (_ : xs) = getImps xs
2128+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2129+getImps (_ : xs) = getImps xs
21212130
21222131getExps :: [PArg] -> [PTerm]
21232132getExps [] = []
2124−getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2125−getExps (_ : xs) = getExps xs
2133+getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2134+getExps (_ : xs) = getExps xs
21262135
21272136getShowArgs :: [PArg] -> [PArg]
21282137getShowArgs [] = []
21292138getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
21302139getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
21312140 | PImp _ _ _ _ tm <- e
2132− , containsHole tm = e : getShowArgs xs
2141+ , containsHole tm = e : getShowArgs xs
21332142getShowArgs (_ : xs) = getShowArgs xs
21342143
21352144getConsts :: [PArg] -> [PTerm]
2136−getConsts [] = []
2145+getConsts [] = []
21372146getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2138−getConsts (_ : xs) = getConsts xs
2147+getConsts (_ : xs) = getConsts xs
21392148
21402149getAll :: [PArg] -> [PTerm]
21412150getAll = map getTm
@@ -2149,13 +2158,13 @@ showName :: Maybe IState -- ^^ the Idris state, for information about names an
21492158 -> Name -- ^^ the term to show
21502159 -> String
21512160showName ist bnd ppo colour n = case ist of
2152− Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2153− Nothing -> showbasic n
2161+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2162+ Nothing -> showbasic n
21542163 where name = if ppopt_impl ppo then show n else showbasic n
2155− showbasic n@(UN _) = showCG n
2156− showbasic (MN i s) = str s
2157− showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2158− showbasic (SN s) = show s
2164+ showbasic n@(UN _) = showCG n
2165+ showbasic (MN i s) = str s
2166+ showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2167+ showbasic (SN s) = show s
21592168 fst3 (x, _, _) = x
21602169 colourise n t = let ctxt' = fmap tt_ctxt ist in
21612170 case ctxt' of
@@ -2187,42 +2196,42 @@ showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
21872196
21882197
21892198instance Sized PTerm where
2190− size (PQuote rawTerm) = size rawTerm
2191− size (PRef fc _ name) = size name
2192− 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
2194− 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
2196− size (PApp fc name args) = 1 + size args
2197− size (PAppBind fc name args) = 1 + size args
2198− size (PCase fc trm bdy) = 1 + size trm + size bdy
2199− size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2200− size (PTrue fc _) = 1
2201− size (PResolveTC fc) = 1
2202− size (PRewrite fc left right _) = 1 + size left + size right
2203− size (PPair fc _ _ left right) = 1 + size left + size right
2204− size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2205− size (PAlternative _ a alts) = 1 + size alts
2206− size (PHidden hidden) = size hidden
2207− size (PUnifyLog tm) = size tm
2208− size (PDisamb _ tm) = size tm
2209− size (PNoImplicits tm) = size tm
2210− size (PType _) = 1
2211− size (PUniverse _) = 1
2212− size (PConstant fc const) = 1 + size fc + size const
2213− size Placeholder = 1
2214− size (PDoBlock dos) = 1 + size dos
2215− size (PIdiom fc term) = 1 + size term
2216− size (PReturn fc) = 1
2217− size (PMetavar _ name) = 1
2218− size (PProof tactics) = size tactics
2219− size (PElabError err) = size err
2220− size PImpossible = 1
2221− size _ = 0
2199+ size (PQuote rawTerm) = size rawTerm
2200+ size (PRef fc _ name) = size name
2201+ size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2202+ size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2203+ size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2204+ size (PTyped trm ty) = 1 + size trm + size ty
2205+ size (PApp fc name args) = 1 + size args
2206+ size (PAppBind fc name args) = 1 + size args
2207+ size (PCase fc trm bdy) = 1 + size trm + size bdy
2208+ size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2209+ size (PTrue fc _) = 1
2210+ size (PResolveTC fc) = 1
2211+ size (PRewrite fc left right _) = 1 + size left + size right
2212+ size (PPair fc _ _ left right) = 1 + size left + size right
2213+ size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2214+ size (PAlternative _ a alts) = 1 + size alts
2215+ size (PHidden hidden) = size hidden
2216+ size (PUnifyLog tm) = size tm
2217+ size (PDisamb _ tm) = size tm
2218+ size (PNoImplicits tm) = size tm
2219+ size (PType _) = 1
2220+ size (PUniverse _) = 1
2221+ size (PConstant fc const) = 1 + size fc + size const
2222+ size Placeholder = 1
2223+ size (PDoBlock dos) = 1 + size dos
2224+ size (PIdiom fc term) = 1 + size term
2225+ size (PReturn fc) = 1
2226+ size (PMetavar _ name) = 1
2227+ size (PProof tactics) = size tactics
2228+ size (PElabError err) = size err
2229+ size PImpossible = 1
2230+ size _ = 0
22222231
22232232getPArity :: PTerm -> Int
2224−getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2225−getPArity _ = 0
2233+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2234+getPArity _ = 0
22262235
22272236-- Return all names, free or globally bound, in the given term.
22282237
@@ -2230,31 +2239,30 @@ allNamesIn :: PTerm -> [Name]
22302239allNamesIn tm = nub $ ni 0 [] tm
22312240 where -- TODO THINK added niTacImp, but is it right?
22322241 ni 0 env (PRef _ _ n)
2233− | not (n `elem` env) = [n]
2234− ni 0 env (PPatvar _ n) = [n]
2235− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2236− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2237− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)
2238− 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
2240− 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
2242− ni 0 env (PHidden tm) = ni 0 env tm
2243− 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
2245− 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
2247− 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
2249− ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2250− ni 0 env (PUnifyLog tm) = ni 0 env tm
2251− ni 0 env (PDisamb _ tm) = ni 0 env tm
2252− ni 0 env (PNoImplicits tm) = ni 0 env tm
2253−
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
2242+ | not (n `elem` env) = [n]
2243+ ni 0 env (PPatvar _ n) = [n]
2244+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2245+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2246+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2247+ ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2248+ ni 0 env (PLam fc n _ ty sc) = 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
2250+ ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2251+ ni 0 env (PHidden tm) = ni 0 env tm
2252+ ni 0 env (PRewrite _ 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
2254+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2255+ ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2256+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2257+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2258+ ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2259+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2260+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2261+ ni 0 env (PNoImplicits tm) = ni 0 env tm
22562262
2257− ni i env tm = concatMap (ni i env) (children 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
2265+ ni i env tm = concatMap (ni i env) (children tm)
22582266
22592267 niTacImp i env (TacImp _ _ scr) = ni i env scr
22602268 niTacImp _ _ _ = []
@@ -2265,32 +2273,32 @@ boundNamesIn :: PTerm -> [Name]
22652273boundNamesIn tm = S.toList (ni 0 S.empty tm)
22662274 where -- TODO THINK Added niTacImp, but is it right?
22672275 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)
2269− 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)
2271− 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
2273− 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
2275− 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
2277− ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2276+ ni 0 set (PApp _ 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)
2278+ ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2279+ ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2280+ ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) 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
2282+ ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2283+ ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r
2284+ ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2285+ ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
22782286 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
2280− ni 0 set (PAlternative ns a as) = niTms 0 set as
2281− ni 0 set (PHidden tm) = ni 0 set tm
2282− ni 0 set (PUnifyLog tm) = ni 0 set tm
2283− ni 0 set (PDisamb _ tm) = ni 0 set tm
2284− ni 0 set (PNoImplicits tm) = ni 0 set tm
2287+ ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2288+ ni 0 set (PAlternative ns a as) = niTms 0 set as
2289+ ni 0 set (PHidden tm) = ni 0 set tm
2290+ ni 0 set (PUnifyLog tm) = ni 0 set tm
2291+ ni 0 set (PDisamb _ tm) = ni 0 set tm
2292+ ni 0 set (PNoImplicits tm) = ni 0 set tm
22852293
2286− 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
2294+ ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2295+ ni i set (PUnquote tm) = ni (i - 1) set tm
22882296
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)
22902298
22912299 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2292− niTms i set [] = set
2293− niTms i set (x : xs) = niTms i (ni i set x) xs
2300+ niTms i set [] = set
2301+ niTms i set (x : xs) = niTms i (ni i set x) xs
22942302
22952303 niTacImp i set (TacImp _ _ scr) = ni i set scr
22962304 niTacImp i set _ = set
@@ -2306,18 +2314,18 @@ implicitNamesIn uvars ist tm
23062314 addFn n = do (imps, fns) <- get
23072315 put (imps, n: fns)
23082316
2309− notCAF [] = False
2317+ notCAF [] = False
23102318 notCAF (PExp _ _ _ _ : _) = True
2311− notCAF (_ : xs) = notCAF xs
2319+ notCAF (_ : xs) = notCAF xs
23122320
23132321 notHidden (n, _) = case getAccessibility n of
2314− Hidden -> False
2315− _ -> True
2322+ Hidden -> False
2323+ _ -> True
23162324
23172325 getAccessibility n
23182326 = case lookupDefAccExact n False (tt_ctxt ist) of
2319− Just (n,t) -> t
2320− _ -> Public
2327+ Just (n,t) -> t
2328+ _ -> Public
23212329
23222330 ni 0 env (PRef _ _ n@(NS _ _))
23232331 | not (n `elem` env)
@@ -2327,44 +2335,44 @@ implicitNamesIn uvars ist tm
23272335 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
23282336 ni 0 env (PApp _ f@(PRef _ _ n) as)
23292337 | n `elem` uvars = do ni 0 env f
2330− mapM_ (ni 0 env) (map getTm as)
2338+ mapM_ (ni 0 env . getTm) as
23312339 | otherwise = do case lookupTy n (tt_ctxt ist) of
2332− [] -> return ()
2333− _ -> addFn n
2334− mapM_ (ni 0 env) (map getTm as)
2340+ [] -> return ()
2341+ _ -> addFn n
2342+ mapM_ (ni 0 env . getTm) as
23352343 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
23372345 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
23392347 ni 0 env (PCase _ c os) = do ni 0 env c
23402348 -- 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
23422350 (imps, fns) <- get
23432351 put ([] ,[])
2344− mapM_ (ni 0 env) (map fst os)
2352+ mapM_ (ni 0 env . fst) os
23452353 (impsfst, _) <- get
23462354 put (nub imps \\ nub impsfst, fns)
2347− 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
2349− 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
2351− 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
2353− 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
2355− ni 0 env t
2356− ni 0 env r
2357− ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2358− ni 0 env (PHidden tm) = ni 0 env tm
2359− ni 0 env (PUnifyLog tm) = ni 0 env tm
2360− ni 0 env (PDisamb _ tm) = ni 0 env tm
2361− ni 0 env (PNoImplicits tm) = ni 0 env tm
2355+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2356+ ni 0 env (PLam fc 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
2358+ ni 0 env (PRewrite _ 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
2360+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2361+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2362+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2363+ ni 0 env t
2364+ ni 0 env r
2365+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2366+ ni 0 env (PHidden tm) = ni 0 env tm
2367+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2368+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2369+ ni 0 env (PNoImplicits tm) = ni 0 env tm
23622370
23632371 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
23642372 maybe (return ()) (ni i env) ty
23652373 ni i env (PUnquote tm) = ni (i - 1) env tm
23662374
2367− ni i env tm = mapM_ (ni i env) (children tm)
2375+ ni i env tm = mapM_ (ni i env) (children tm)
23682376
23692377-- Return names which are free in the given term.
23702378namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
@@ -2373,32 +2381,32 @@ namesIn uvars ist tm = nub $ ni 0 [] tm
23732381 ni 0 env (PRef _ _ n)
23742382 | not (n `elem` env)
23752383 = case lookupTy n (tt_ctxt ist) of
2376− [] -> [n]
2377− _ -> if n `elem` (map fst uvars) then [n] else []
2378− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2379− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2380− ni 0 env (PCase _ c os) = ni 0 env c ++
2384+ [] -> [n]
2385+ _ -> [n | n `elem` (map fst uvars)]
2386+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2387+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2388+ ni 0 env (PCase _ c os) = ni 0 env c ++
23812389 -- names in 'os', not counting the names bound in the cases
2382− (nub (concatMap (ni 0 env) (map snd os))
2383− \\ nub (concatMap (ni 0 env) (map fst os)))
2384− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2390+ (nub (concatMap (ni 0 env . snd) os)
2391+ \\ nub (concatMap (ni 0 env . fst) os))
2392+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
23852393 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
2387− 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
2389− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2394+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2395+ ni 0 env (PRewrite _ 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
2397+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
23902398 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
23922400 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2393− ni 0 env (PHidden tm) = ni 0 env tm
2394− ni 0 env (PUnifyLog tm) = ni 0 env tm
2395− ni 0 env (PDisamb _ tm) = ni 0 env tm
2396− ni 0 env (PNoImplicits tm) = ni 0 env tm
2401+ ni 0 env (PHidden tm) = ni 0 env tm
2402+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2403+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2404+ ni 0 env (PNoImplicits tm) = ni 0 env tm
23972405
2398− 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
2406+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2407+ ni i env (PUnquote tm) = ni (i - 1) env tm
24002408
2401− ni i env tm = concatMap (ni i env) (children tm)
2409+ ni i env tm = concatMap (ni i env) (children tm)
24022410
24032411 niTacImp i env (TacImp _ _ scr) = ni i env scr
24042412 niTacImp _ _ _ = []
@@ -2413,27 +2421,27 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm
24132421 = case lookupDefExact n (tt_ctxt ist) of
24142422 Nothing -> [n]
24152423 _ -> []
2416− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2417− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2418− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)
2419− 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
2421− 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
2423− 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
2424+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2425+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2426+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2427+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2428+ ni 0 env (PLam fc n _ ty sc) = 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
2430+ ni 0 env (PRewrite _ 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
2432+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
24252433 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
24272435 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2428− ni 0 env (PHidden tm) = ni 0 env tm
2429− ni 0 env (PUnifyLog tm) = ni 0 env tm
2430− ni 0 env (PDisamb _ tm) = ni 0 env tm
2431− ni 0 env (PNoImplicits tm) = ni 0 env tm
2436+ ni 0 env (PHidden tm) = ni 0 env tm
2437+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2438+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2439+ ni 0 env (PNoImplicits tm) = ni 0 env tm
24322440
2433− 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
2441+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2442+ ni i env (PUnquote tm) = ni (i - 1) env tm
24352443
2436− ni i env tm = concatMap (ni i env) (children tm)
2444+ ni i env tm = concatMap (ni i env) (children tm)
24372445
24382446 niTacImp i env (TacImp _ _ scr) = ni i env scr
24392447 niTacImp _ _ _ = []