@@ -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
@@ -210,12 +211,14 @@ data IState = IState {
210211 idris_name :: Int,
211212 idris_lineapps :: [((FilePath, Int), PTerm)],
212213 -- ^ 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))],
214215 -- ^ The currently defined but not proven metavariables. The Int
215216 -- is the number of vars to display as a context, the Maybe Name
216217 -- 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− -- allowed
218+ -- available for proof search and the Bools are whether :p is
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)
219222 idris_coercions :: [Name],
220223 idris_errRev :: [(Term, Term)],
221224 syntax_rules :: SyntaxRules,
@@ -235,7 +238,7 @@ data IState = IState {
235238 brace_stack :: [Maybe Int],
236239 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
237240 idris_parsedSpan :: Maybe FC,
238− hide_list :: [(Name, Maybe Accessibility)],
241+ hide_list :: Ctxt Accessibility,
239242 default_access :: Accessibility,
240243 default_total :: Bool,
241244 ibc_write :: [IBCWrite],
@@ -262,7 +265,9 @@ data IState = IState {
262265 idris_exports :: [Name], -- ^ Functions with ExportList
263266 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
264267 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)
266271 }
267272
268273-- Required for parsers library, and therefore trifecta
@@ -279,11 +284,10 @@ deriving instance NFData SizeChange
279284type SCGEntry = (Name, [Maybe (Int, SizeChange)])
280285type UsageReason = (Name, Int) -- fn_name, its_arg_number
281286
282−data CGInfo = CGInfo { argsdef :: [Name],
283− calls :: [(Name, [[Name]])],
287+data CGInfo = CGInfo { calls :: [Name],
284288 scg :: [SCGEntry],
285− argsused :: [Name],
286− usedpos :: [(Int, [UsageReason])] }
289+ usedpos :: [(Int, [UsageReason])]
290+ }
287291 deriving Show
288292{-!
289293deriving instance Binary CGInfo
@@ -348,12 +352,13 @@ idrisInit = IState initContext S.empty []
348352 emptyContext emptyContext emptyContext emptyContext
349353 emptyContext emptyContext emptyContext emptyContext
350354 emptyContext emptyContext emptyContext emptyContext
351− emptyContext emptyContext
355+ emptyContext
352356 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
353− [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
357+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []
354358 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
355359 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
356− emptyContext
360+ emptyContext S.empty M.empty
361+
357362
358363-- | The monad for the main REPL - reading and processing files and updating
359364-- global state (hence the IO inner monad).
@@ -631,13 +636,17 @@ is_scoped :: Plicity -> Maybe ImplicitInfo
631636is_scoped (Imp _ _ _ s) = s
632637is_scoped _ = Nothing
633638
634−impl = Imp [] Dynamic False (Just (Impl False True))
635−forall_imp = Imp [] Dynamic False (Just (Impl False False))
639+impl = Imp [] Dynamic False (Just (Impl False True))
640+
641+forall_imp = Imp [] Dynamic False (Just (Impl False False))
636642forall_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
643+
644+expl = Exp [] Dynamic False
645+expl_param = Exp [] Dynamic True
646+
647+constraint = Constraint [] Static
648+
649+tacimpl t = TacImp [] Dynamic t
641650
642651data FnOpt = Inlinable -- always evaluate when simplifying
643652 | TotalFn | PartialFn | CoveringFn
@@ -695,7 +704,7 @@ data PDecl' t
695704 FC -- Record name precise location
696705 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
697706 [(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
699708 (Maybe (Name, FC)) -- Optional constructor name and location
700709 (Docstring (Either Err t)) -- Constructor doc
701710 SyntaxInfo -- Constructor SyntaxInfo
@@ -717,6 +726,8 @@ data PDecl' t
717726 [(Name, Docstring (Either Err t))] -- Parameter docs
718727 SyntaxInfo
719728 FC [(Name, t)] -- constraints
729+ Accessibility
730+ FnOpts
720731 Name -- class
721732 FC -- precise location of class
722733 [t] -- parameters
@@ -756,6 +767,7 @@ data Directive = DLib Codegen String |
756767 DErrorHandlers Name FC Name FC [(Name, FC)] |
757768 DLanguage LanguageExt |
758769 DDeprecate Name String |
770+ DAutoImplicits Bool |
759771 DUsed FC Name Name
760772
761773-- | A set of instructions for things that need to happen in IState
@@ -763,6 +775,9 @@ data Directive = DLib Codegen String |
763775data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
764776 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
765777 | RAddInstance Name Name
778+ | RDatatypeDeclInstrs Name [PArg]
779+ | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
780+ -- ^ Datatype, constructors
766781
767782-- | For elaborator state
768783data EState = EState {
@@ -875,10 +890,10 @@ mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor c
875890 (map (mapPDeclFC f g) body)
876891 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
877892 ctorDoc
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) =
879894 PInstance doc paramDocs syn (f fc)
880895 (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)
882897 (mapPTermFC f g instTy)
883898 instN
884899 (map (mapPDeclFC f g) body)
@@ -918,7 +933,7 @@ declared (PParams _ _ ds) = concatMap declared ds
918933declared (PNamespace _ _ ds) = concatMap declared ds
919934declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
920935declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
921−declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
936+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
922937declared (PDSL n _) = [n]
923938declared (PSyntax _ _) = []
924939declared (PMutual _ ds) = concatMap declared ds
@@ -927,39 +942,39 @@ declared _ = []
927942
928943-- get the names declared, not counting nested parameter blocks
929944tldeclared :: 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)
945+tldeclared (PFix _ _ _) = []
946+tldeclared (PTy _ _ _ _ _ n _ t) = [n]
947+tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
948+tldeclared (PClauses _ _ n _) = [] -- not a declaration
949+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
935950tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
936951 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 _ = []
952+tldeclared (PParams _ _ ds) = []
953+tldeclared (PMutual _ ds) = concatMap tldeclared ds
954+tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
955+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
956+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
957+tldeclared _ = []
943958
944959defined :: 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
960+defined (PFix _ _ _) = []
961+defined (PTy _ _ _ _ _ n _ t) = []
962+defined (PPostulate _ _ _ _ _ _ n t) = []
963+defined (PClauses _ _ n _) = [n] -- not a declaration
964+defined (PCAF _ n _) = [n]
965+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
951966 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 _ = []
967+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
968+defined (PParams _ _ ds) = concatMap defined ds
969+defined (PNamespace _ _ ds) = concatMap defined ds
970+defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
971+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
972+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
973+defined (PDSL n _) = [n]
974+defined (PSyntax _ _) = []
975+defined (PMutual _ ds) = concatMap defined ds
976+defined (PDirective _) = []
977+defined _ = []
963978
964979updateN :: [(Name, Name)] -> Name -> Name
965980updateN ns n | Just n' <- lookup n ns = n'
@@ -1040,33 +1055,33 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
10401055-- general-purpose FCs, and the second transforms those that are used
10411056-- for semantic source highlighting, so they can be treated specially.
10421057mapPTermFC :: (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
1058+mapPTermFC f g (PQuote q) = PQuote q
1059+mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1060+mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1061+mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1062+mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) 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)
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)
1065+mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1066+mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1067+mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1068+mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1069+mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1070+mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
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)
1072+mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1073+mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
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)
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)
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)
1077+mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1078+mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1079+mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1080+mapPTermFC f g (PType fc) = PType (f fc)
1081+mapPTermFC f g (PUniverse u) = PUniverse u
1082+mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1083+mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1084+mapPTermFC f g Placeholder = Placeholder
10701085mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
10711086 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
10721087 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)
10741089 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
10751090 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
10761091 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)
1092+mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1093+mapPTermFC f g (PReturn fc) = PReturn (f fc)
1094+mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1095+mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1096+mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1097+mapPTermFC f g (PElabError err) = PElabError err
1098+mapPTermFC f g PImpossible = PImpossible
1099+mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1100+mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1101+mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1102+mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1103+mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1104+mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1105+mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1106+mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1107+mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
10931108
10941109{-!
10951110dg instance Binary PTerm
@@ -1098,28 +1113,27 @@ deriving instance NFData PTerm
10981113
10991114mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
11001115mapPT 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)
1116+ mpt (PLam fc n nfc t s) = PLam fc 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)
1118+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1119+ mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1120+ 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)
1122+ 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)
1124+ 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)
11121126 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
1127+ mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1128+ mpt (PHidden t) = PHidden (mapPT f t)
1129+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1130+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1131+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1132+ mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1133+ mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1134+ mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1135+ mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1136+ mpt x = x
11231137
11241138
11251139data PTactic' t = Intro [Name] | Intros | Focus Name
@@ -1160,39 +1174,39 @@ deriving instance Binary PTactic'
11601174deriving instance NFData PTactic'
11611175!-}
11621176instance 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
1177+ size (Intro nms) = 1 + size nms
1178+ size Intros = 1
1179+ size (Focus nm) = 1 + size nm
1180+ size (Refine nm bs) = 1 + size nm + length bs
1181+ size (Rewrite t) = 1 + size t
1182+ size (Induction t) = 1 + size t
1183+ size (LetTac nm t) = 1 + size nm + size t
1184+ size (Exact t) = 1 + size t
1185+ size Compute = 1
1186+ size Trivial = 1
1187+ size Solve = 1
1188+ size Attack = 1
1189+ size ProofState = 1
1190+ size ProofTerm = 1
1191+ size Undo = 1
1192+ size (Try l r) = 1 + size l + size r
1193+ size (TSeq l r) = 1 + size l + size r
1194+ size (ApplyTactic t) = 1 + size t
1195+ size (Reflect t) = 1 + size t
1196+ size (Fill t) = 1 + size t
1197+ size Qed = 1
1198+ size Abandon = 1
1199+ size Skip = 1
1200+ size (TFail ts) = 1 + size ts
1201+ size SourceFC = 1
1202+ size DoUnify = 1
1203+ size (CaseTac x) = 1 + size x
1204+ size (Equiv t) = 1 + size t
1205+ size (Claim x y) = 1 + size x + size y
1206+ size Unfocus = 1
1207+ size (MatchRefine x) = 1 + size x
11941208 size (LetTacTy x y z) = 1 + size x + size y + size z
1195− size TCInstance = 1
1209+ size TCInstance = 1
11961210
11971211type PTactic = PTactic' PTerm
11981212
@@ -1208,11 +1222,11 @@ deriving instance NFData PDo'
12081222!-}
12091223
12101224instance 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
1225+ size (DoExp fc t) = 1 + size fc + size t
1226+ size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1227+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1228+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1229+ size (DoLetP fc l r) = 1 + size fc + size l + size r
12161230
12171231type PDo = PDo' PTerm
12181232
@@ -1244,10 +1258,10 @@ data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
12441258 deriving (Show, Eq, Data, Typeable)
12451259
12461260instance 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
1261+ size (PImp p _ l nm trm) = 1 + size nm + size trm
1262+ size (PExp p l nm trm) = 1 + size nm + size trm
1263+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1264+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
12511265
12521266{-!
12531267deriving instance Binary PArg'
@@ -1255,43 +1269,43 @@ deriving instance NFData PArg'
12551269!-}
12561270
12571271pimp 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
1272+pexp t = PExp 1 [] (sMN 0 "arg") t
1273+pconst t = PConstraint 1 [] (sMN 0 "carg") t
12601274ptacimp n s t = PTacImplicit 2 [] n s t
12611275
12621276type PArg = PArg' PTerm
12631277
12641278-- | Get the highest FC in a term, if one exists
12651279highestFC :: 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
1280+highestFC (PQuote _) = Nothing
1281+highestFC (PRef fc _ _) = Just fc
1282+highestFC (PInferRef fc _ _) = Just fc
1283+highestFC (PPatvar fc _) = Just fc
1284+highestFC (PLam fc _ _ _ _) = Just fc
1285+highestFC (PPi _ _ _ _ _) = Nothing
1286+highestFC (PLet fc _ _ _ _ _) = Just fc
1287+highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1288+highestFC (PApp fc _ _) = Just fc
1289+highestFC (PAppBind fc _ _) = Just fc
1290+highestFC (PMatchApp fc _) = Just fc
1291+highestFC (PCase fc _ _) = Just fc
1292+highestFC (PIfThenElse fc _ _ _) = Just fc
1293+highestFC (PTrue fc _) = Just fc
1294+highestFC (PResolveTC fc) = Just fc
1295+highestFC (PRewrite fc _ _ _) = Just fc
1296+highestFC (PPair fc _ _ _ _) = Just fc
1297+highestFC (PDPair fc _ _ _ _ _) = Just fc
1298+highestFC (PAs fc _ _) = Just fc
12851299highestFC (PAlternative _ _ args) =
12861300 case mapMaybe highestFC args of
12871301 [] -> Nothing
12881302 (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
1303+highestFC (PHidden _) = Nothing
1304+highestFC (PType fc) = Just fc
1305+highestFC (PUniverse _) = Nothing
1306+highestFC (PGoal fc _ _ _) = Just fc
1307+highestFC (PConstant fc _) = Just fc
1308+highestFC Placeholder = Nothing
12951309highestFC (PDoBlock lines) =
12961310 case map getDoFC lines of
12971311 [] -> Nothing
@@ -1303,23 +1317,23 @@ highestFC (PDoBlock lines) =
13031317 getDoFC (DoLet fc nm nfc l r) = fc
13041318 getDoFC (DoLetP fc l r) = fc
13051319
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
1320+highestFC (PIdiom fc _) = Just fc
1321+highestFC (PReturn fc) = Just fc
1322+highestFC (PMetavar fc _) = Just fc
1323+highestFC (PProof _) = Nothing
1324+highestFC (PTactics _) = Nothing
1325+highestFC (PElabError _) = Nothing
1326+highestFC PImpossible = Nothing
1327+highestFC (PCoerced tm) = highestFC tm
1328+highestFC (PDisamb _ opts) = highestFC opts
1329+highestFC (PUnifyLog tm) = highestFC tm
1330+highestFC (PNoImplicits tm) = highestFC tm
1331+highestFC (PQuasiquote _ _) = Nothing
1332+highestFC (PUnquote tm) = highestFC tm
1333+highestFC (PQuoteName _ _ fc) = Just fc
1334+highestFC (PRunElab fc _ _) = Just fc
1335+highestFC (PConstSugar fc _) = Just fc
1336+highestFC (PAppImpl t _) = highestFC t
13231337
13241338-- Type class data
13251339
@@ -1397,11 +1411,11 @@ data Syntax = Rule [SSymbol] PTerm SynContext
13971411
13981412syntaxNames :: Syntax -> [Name]
13991413syntaxNames (Rule syms _ _) = mapMaybe ename syms
1400− where ename (Keyword n) = Just n
1401− ename _ = Nothing
1414+ where ename (Keyword n) = Just n
1415+ ename _ = Nothing
14021416syntaxNames (DeclRule syms _) = mapMaybe ename syms
1403− where ename (Keyword n) = Just n
1404− ename _ = Nothing
1417+ where ename (Keyword n) = Just n
1418+ ename _ = Nothing
14051419
14061420syntaxSymbols :: Syntax -> [SSymbol]
14071421syntaxSymbols (Rule ss _ _) = ss
@@ -1434,9 +1448,9 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
14341448 where
14351449 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
14361450
1437− ruleSort [] [] = EQ
1438− ruleSort [] _ = LT
1439− ruleSort _ [] = GT
1451+ ruleSort [] [] = EQ
1452+ ruleSort [] _ = LT
1453+ ruleSort _ [] = GT
14401454 ruleSort (s1:ss1) (s2:ss2) =
14411455 case symCompare s1 s2 of
14421456 EQ -> ruleSort ss1 ss2
@@ -1444,25 +1458,25 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
14441458
14451459 -- Better than creating Ord instance for SSymbol since
14461460 -- 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
1461+ symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1462+ symCompare (Keyword _) _ = LT
1463+ symCompare (Symbol _) (Keyword _) = GT
1464+ symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1465+ symCompare (Symbol _) _ = LT
1466+ symCompare (Binding _) (Keyword _) = GT
1467+ symCompare (Binding _) (Symbol _) = GT
1468+ symCompare (Binding b1) (Binding b2) = compare b1 b2
1469+ symCompare (Binding _) _ = LT
1470+ symCompare (Expr _) (Keyword _) = GT
1471+ symCompare (Expr _) (Symbol _) = GT
1472+ symCompare (Expr _) (Binding _) = GT
1473+ symCompare (Expr e1) (Expr e2) = compare e1 e2
1474+ symCompare (Expr _) _ = LT
1475+ symCompare (SimpleExpr _) (Keyword _) = GT
1476+ symCompare (SimpleExpr _) (Symbol _) = GT
1477+ symCompare (SimpleExpr _) (Binding _) = GT
1478+ symCompare (SimpleExpr _) (Expr _) = GT
1479+ symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
14661480
14671481initDSL = DSL (PRef f [] (sUN ">>="))
14681482 (PRef f [] (sUN "return"))
@@ -1534,10 +1548,10 @@ getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
15341548getInferTerm (App _ (App _ _ _) tm) = tm
15351549getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
15361550
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
1551+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1552+ where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1553+ toTy (PVar t) = PVTy t
1554+ toTy b = b
15411555getInferType (App _ (App _ _ ty) _) = ty
15421556
15431557
@@ -1562,9 +1576,9 @@ pairCon = sNS (sUN "MkPair") ["Builtins"]
15621576upairTy = sNS (sUN "UPair") ["Builtins"]
15631577upairCon = sNS (sUN "MkUPair") ["Builtins"]
15641578
1565−eqTy = sUN "="
1579+eqTy = sUN "="
15661580eqCon = sUN "Refl"
1567−eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1581+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
15681582 "The propositional equality type. A proof that `x` = `y`." ++
15691583 "\n\n" ++
15701584 "To use such a proof, pattern-match on it, and the two equal things will " ++
@@ -1607,8 +1621,8 @@ modDocName :: Name
16071621modDocName = sMN 0 "ModuleDocs"
16081622
16091623-- Defined in builtins.idr
1610−sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1611−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1624+sigmaTy = sNS (sUN "DPair") ["Builtins"]
1625+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
16121626
16131627piBind :: [(Name, PTerm)] -> PTerm -> PTerm
16141628piBind = piBindp expl
@@ -1648,11 +1662,11 @@ annotationColour ist (AnnConst c) =
16481662 in Just $ if constIsType c
16491663 then typeColour theme
16501664 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)
1665+annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1666+annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1667+annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
16541668annotationColour 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)
16561670annotationColour ist (AnnName n _ _ _) =
16571671 let ctxt = tt_ctxt ist
16581672 theme = idris_colourTheme ist
@@ -1738,7 +1752,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17381752
17391753 st =
17401754 case s of
1741− Static -> text "[static]" <> space
1755+ Static -> text "%static" <> space
17421756 _ -> empty
17431757 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
17441758 | ppopt_impl ppo =
@@ -1749,12 +1763,12 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17491763 where
17501764 st =
17511765 case s of
1752− Static -> text "[static]" <> space
1766+ Static -> text "%static" <> space
17531767 _ -> empty
17541768 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
17551769 depth d . bracket p startPrec $
17561770 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) =
17581772 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
17591773 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
17601774 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
17911805 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
17921806 [l,r] -> let precedence = maybe (startPrec - 1) prec f
17931807 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1794− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1808+ (l@(PExp{}) : r@(PExp{}) : rest) ->
17951809 depth d . bracket p funcAppPrec $
17961810 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
17971811 align (group (vsep (map (prettyArgS d bnd) rest)))
@@ -1842,20 +1856,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18421856 -- disambiguation on PDPair.
18431857 vars tm = filter noNS (allNamesIn tm)
18441858 noNS (NS _ _) = False
1845− noNS _ = True
1859+ noNS _ = True
18461860
18471861 prettySe d p bnd (PIfThenElse _ c t f) =
18481862 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
18501864 , kwd "then" <+> prettySe (decD d) startPrec bnd t
18511865 , kwd "else" <+> prettySe (decD d) startPrec bnd f
18521866 ]
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 "()"
1867+ prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1868+ prettySe d p bnd (PResolveTC _) = kwd "%instance"
1869+ prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1870+ prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
18571871 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1858− prettySe d p bnd (PRewrite _ l r _) =
1872+ prettySe d p bnd (PRewrite _ l r _) =
18591873 depth d . bracket p startPrec $
18601874 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
18611875 prettySe d p bnd (PTyped l r) =
@@ -1865,9 +1879,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18651879 align . group . vsep . punctuate (ann comma) $
18661880 map (prettySe (decD d) startPrec bnd) elts
18671881 where ann = case pun of
1868− TypeOrTerm -> id
1869− IsType -> annName pairTy
1870− IsTerm -> annName pairCon
1882+ TypeOrTerm -> id
1883+ IsType -> annName pairTy
1884+ IsTerm -> annName pairCon
18711885 prettySe d p bnd (PDPair _ _ pun l t r) =
18721886 depth d $
18731887 annotated lparen <>
@@ -1876,30 +1890,32 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18761890 prettySe (decD d) startPrec (addBinding bnd) r <>
18771891 annotated rparen
18781892 where annotated = case pun of
1879− IsType -> annName sigmaTy
1880− IsTerm -> annName sigmaCon
1881− TypeOrTerm -> id
1893+ IsType -> annName sigmaTy
1894+ IsTerm -> annName sigmaCon
1895+ TypeOrTerm -> id
18821896 (left, addBinding) = case (l, pun) of
18831897 (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)
18851899 prettySe d p bnd (PAlternative ns a as) =
18861900 lparen <> text "|" <> prettyAs <> text "|" <> rparen
18871901 where
18881902 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))
1903+ foldr ((\ l r -> l <+> text "," <+> r) .
1904+ depth d . prettySe (decD d) startPrec bnd)
1905+ empty as
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))
18931909 -- XXX: add pretty for tactics
1894− prettySe d p bnd (PProof ts) =
1910+ prettySe d p bnd (PProof ts) =
18951911 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1896− prettySe d p bnd (PTactics ts) =
1912+ prettySe d p bnd (PTactics ts) =
18971913 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) =
1914+ prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1915+ prettySe d p bnd (PReturn f) = kwd "return"
1916+ prettySe d p bnd PImpossible = kwd "impossible"
1917+ prettySe d p bnd Placeholder = text "_"
1918+ prettySe d p bnd (PDoBlock dos) =
19031919 bracket p startPrec $
19041920 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
19051921 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
19211937 text "no pretty printer for pattern-matching do binding" :
19221938 ppdo bnd dos
19231939 ppdo _ [] = []
1924− prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1925− prettySe d p bnd (PElabError s) = pretty s
1940+ prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1941+ prettySe d p bnd (PElabError s) = pretty s
19261942 -- 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 ")"
19281944 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
1945+ prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1946+ prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
19311947 where start = if res then "`{" else "`{{"
19321948 end = if res then "}" else "}}"
1933− prettySe d p bnd (PRunElab _ tm _) =
1949+ prettySe d p bnd (PRunElab _ tm _) =
19341950 bracket p funcAppPrec . group . align . hang 2 $
19351951 text "%runElab" <$>
19361952 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"
1953+ prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1954+ prettySe d p bnd _ = text "missing pretty-printer for term"
19401955
19411956 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
19421957 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
19431958 where display (UN n) = T.unpack n
19441959 display (MN _ n) = T.unpack n
19451960 -- 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
19471962 display n = show n
19481963
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)
1964+ prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1965+ prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1966+ prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1967+ prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
19531968
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
1969+ prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1970+ prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1971+ prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
19571972 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
19581973
19591974 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
19601975 annName n = annotate (AnnName n Nothing Nothing Nothing)
19611976
19621977 opStr :: Name -> String
1963− opStr (NS n _) = opStr n
1964− opStr (UN n) = T.unpack n
1978+ opStr (NS n _) = opStr n
1979+ opStr (UN n) = T.unpack n
19651980
19661981 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
19671982 slist' (Just d) _ _ _ | d <= 0 = Nothing
@@ -2023,7 +2038,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20232038 ellipsis = text "..."
20242039
20252040 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
20272042
20282043 decD = fmap (\x -> x - 1)
20292044
@@ -2038,7 +2053,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20382053-- | Strip away namespace information
20392054basename :: Name -> Name
20402055basename (NS n _) = basename n
2041−basename n = n
2056+basename n = n
20422057
20432058-- | Determine whether a name was the one inserted for a hole or
20442059-- guess by the delaborator
@@ -2058,15 +2073,15 @@ prettyName
20582073 -> Name -- ^^ the name to pprint
20592074 -> Doc OutputAnnotation
20602075prettyName 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
2076+ | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2077+ | (UN n') <- n, T.unpack n' == "_" = text "_"
2078+ | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2079+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
20652080 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
2081+ baseName (UN n) = T.unpack n
2082+ baseName (NS n ns) = baseName n
2083+ baseName (MN i s) = T.unpack s
2084+ baseName other = show other
20702085 nameSpace = case n of
20712086 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
20722087 _ -> ""
@@ -2081,13 +2096,13 @@ showCImp ppo (PClause _ n l ws r w)
20812096 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
20822097 <+> text "where" <+> text (show w)
20832098 where
2084− showWs [] = empty
2099+ showWs [] = empty
20852100 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
20862101showCImp ppo (PWith _ n l ws r pn w)
20872102 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
20882103 <+> braces (text (show w))
20892104 where
2090− showWs [] = empty
2105+ showWs [] = empty
20912106 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
20922107
20932108
@@ -2099,43 +2114,43 @@ showDImp ppo (PDatadecl n nfc ty cons)
20992114showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
21002115showDecls o ds = vsep (map (showDeclImp o) ds)
21012116
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))
21032118showDeclImp 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" <+>
21052120 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)
2121+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2122+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2123+showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
21092124showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
21102125showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
21112126 = 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)
21132128 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
21142129showDeclImp _ _ = text "..."
21152130-- showDeclImp (PImport o) = "import " ++ o
21162131
21172132getImps :: [PArg] -> [(Name, PTerm)]
21182133getImps [] = []
2119−getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2120−getImps (_ : xs) = getImps xs
2134+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2135+getImps (_ : xs) = getImps xs
21212136
21222137getExps :: [PArg] -> [PTerm]
21232138getExps [] = []
2124−getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2125−getExps (_ : xs) = getExps xs
2139+getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2140+getExps (_ : xs) = getExps xs
21262141
21272142getShowArgs :: [PArg] -> [PArg]
21282143getShowArgs [] = []
21292144getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
21302145getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
21312146 | PImp _ _ _ _ tm <- e
2132− , containsHole tm = e : getShowArgs xs
2147+ , containsHole tm = e : getShowArgs xs
21332148getShowArgs (_ : xs) = getShowArgs xs
21342149
21352150getConsts :: [PArg] -> [PTerm]
2136−getConsts [] = []
2151+getConsts [] = []
21372152getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2138−getConsts (_ : xs) = getConsts xs
2153+getConsts (_ : xs) = getConsts xs
21392154
21402155getAll :: [PArg] -> [PTerm]
21412156getAll = map getTm
@@ -2149,13 +2164,13 @@ showName :: Maybe IState -- ^^ the Idris state, for information about names an
21492164 -> Name -- ^^ the term to show
21502165 -> String
21512166showName 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
2167+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2168+ Nothing -> showbasic n
21542169 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
2170+ showbasic n@(UN _) = showCG n
2171+ showbasic (MN i s) = str s
2172+ showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2173+ showbasic (SN s) = show s
21592174 fst3 (x, _, _) = x
21602175 colourise n t = let ctxt' = fmap tt_ctxt ist in
21612176 case ctxt' of
@@ -2187,42 +2202,42 @@ showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
21872202
21882203
21892204instance 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
2205+ size (PQuote rawTerm) = size rawTerm
2206+ size (PRef fc _ name) = size name
2207+ size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2208+ size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2209+ size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2210+ size (PTyped trm ty) = 1 + size trm + size ty
2211+ size (PApp fc name args) = 1 + size args
2212+ size (PAppBind fc name args) = 1 + size args
2213+ size (PCase fc trm bdy) = 1 + size trm + size bdy
2214+ size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2215+ size (PTrue fc _) = 1
2216+ size (PResolveTC fc) = 1
2217+ size (PRewrite fc left right _) = 1 + size left + size right
2218+ size (PPair fc _ _ left right) = 1 + size left + size right
2219+ size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2220+ size (PAlternative _ a alts) = 1 + size alts
2221+ size (PHidden hidden) = size hidden
2222+ size (PUnifyLog tm) = size tm
2223+ size (PDisamb _ tm) = size tm
2224+ size (PNoImplicits tm) = size tm
2225+ size (PType _) = 1
2226+ size (PUniverse _) = 1
2227+ size (PConstant fc const) = 1 + size fc + size const
2228+ size Placeholder = 1
2229+ size (PDoBlock dos) = 1 + size dos
2230+ size (PIdiom fc term) = 1 + size term
2231+ size (PReturn fc) = 1
2232+ size (PMetavar _ name) = 1
2233+ size (PProof tactics) = size tactics
2234+ size (PElabError err) = size err
2235+ size PImpossible = 1
2236+ size _ = 0
22222237
22232238getPArity :: PTerm -> Int
2224−getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2225−getPArity _ = 0
2239+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2240+getPArity _ = 0
22262241
22272242-- Return all names, free or globally bound, in the given term.
22282243
@@ -2230,31 +2245,30 @@ allNamesIn :: PTerm -> [Name]
22302245allNamesIn tm = nub $ ni 0 [] tm
22312246 where -- TODO THINK added niTacImp, but is it right?
22322247 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
2248+ | not (n `elem` env) = [n]
2249+ ni 0 env (PPatvar _ n) = [n]
2250+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2251+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2252+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2253+ ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2254+ ni 0 env (PLam fc n _ ty sc) = 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
2256+ ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2257+ ni 0 env (PHidden tm) = ni 0 env tm
2258+ ni 0 env (PRewrite _ 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
2260+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2261+ ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2262+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2263+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2264+ ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2265+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2266+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2267+ ni 0 env (PNoImplicits tm) = ni 0 env tm
22562268
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)
22582272
22592273 niTacImp i env (TacImp _ _ scr) = ni i env scr
22602274 niTacImp _ _ _ = []
@@ -2265,32 +2279,32 @@ boundNamesIn :: PTerm -> [Name]
22652279boundNamesIn tm = S.toList (ni 0 S.empty tm)
22662280 where -- TODO THINK Added niTacImp, but is it right?
22672281 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
2282+ ni 0 set (PApp _ 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)
2284+ ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2285+ ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2286+ ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) 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
2288+ ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2289+ ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r
2290+ ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2291+ ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
22782292 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
2293+ ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2294+ ni 0 set (PAlternative ns a as) = niTms 0 set as
2295+ ni 0 set (PHidden tm) = ni 0 set tm
2296+ ni 0 set (PUnifyLog tm) = ni 0 set tm
2297+ ni 0 set (PDisamb _ tm) = ni 0 set tm
2298+ ni 0 set (PNoImplicits tm) = ni 0 set tm
22852299
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
2300+ ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2301+ ni i set (PUnquote tm) = ni (i - 1) set tm
22882302
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)
22902304
22912305 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
2306+ niTms i set [] = set
2307+ niTms i set (x : xs) = niTms i (ni i set x) xs
22942308
22952309 niTacImp i set (TacImp _ _ scr) = ni i set scr
22962310 niTacImp i set _ = set
@@ -2306,18 +2320,19 @@ implicitNamesIn uvars ist tm
23062320 addFn n = do (imps, fns) <- get
23072321 put (imps, n: fns)
23082322
2309− notCAF [] = False
2323+ notCAF [] = False
23102324 notCAF (PExp _ _ _ _ : _) = True
2311− notCAF (_ : xs) = notCAF xs
2325+ notCAF (_ : xs) = notCAF xs
23122326
23132327 notHidden (n, _) = case getAccessibility n of
2314− Hidden -> False
2315− _ -> True
2328+ Hidden -> False
2329+ Private -> False
2330+ _ -> True
23162331
23172332 getAccessibility n
23182333 = case lookupDefAccExact n False (tt_ctxt ist) of
2319− Just (n,t) -> t
2320− _ -> Public
2334+ Just (n,t) -> t
2335+ _ -> Public
23212336
23222337 ni 0 env (PRef _ _ n@(NS _ _))
23232338 | not (n `elem` env)
@@ -2327,44 +2342,44 @@ implicitNamesIn uvars ist tm
23272342 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
23282343 ni 0 env (PApp _ f@(PRef _ _ n) as)
23292344 | n `elem` uvars = do ni 0 env f
2330− mapM_ (ni 0 env) (map getTm as)
2345+ mapM_ (ni 0 env . getTm) as
23312346 | otherwise = do case lookupTy n (tt_ctxt ist) of
2332− [] -> return ()
2333− _ -> addFn n
2334− mapM_ (ni 0 env) (map getTm as)
2347+ [] -> return ()
2348+ _ -> addFn n
2349+ mapM_ (ni 0 env . getTm) as
23352350 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
23372352 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
23392354 ni 0 env (PCase _ c os) = do ni 0 env c
23402355 -- 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
23422357 (imps, fns) <- get
23432358 put ([] ,[])
2344− mapM_ (ni 0 env) (map fst os)
2359+ mapM_ (ni 0 env . fst) os
23452360 (impsfst, _) <- get
23462361 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
2362+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2363+ ni 0 env (PLam fc 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
2365+ ni 0 env (PRewrite _ 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
2367+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2368+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2369+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2370+ ni 0 env t
2371+ ni 0 env r
2372+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2373+ ni 0 env (PHidden tm) = ni 0 env tm
2374+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2375+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2376+ ni 0 env (PNoImplicits tm) = ni 0 env tm
23622377
23632378 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
23642379 maybe (return ()) (ni i env) ty
23652380 ni i env (PUnquote tm) = ni (i - 1) env tm
23662381
2367− ni i env tm = mapM_ (ni i env) (children tm)
2382+ ni i env tm = mapM_ (ni i env) (children tm)
23682383
23692384-- Return names which are free in the given term.
23702385namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
@@ -2373,32 +2388,32 @@ namesIn uvars ist tm = nub $ ni 0 [] tm
23732388 ni 0 env (PRef _ _ n)
23742389 | not (n `elem` env)
23752390 = 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 ++
2391+ [] -> [n]
2392+ _ -> [n | n `elem` (map fst uvars)]
2393+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2394+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2395+ ni 0 env (PCase _ c os) = ni 0 env c ++
23812396 -- 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]
2397+ (nub (concatMap (ni 0 env . snd) os)
2398+ \\ nub (concatMap (ni 0 env . fst) os))
2399+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
23852400 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
2401+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2402+ ni 0 env (PRewrite _ 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
2404+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
23902405 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
23922407 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
2408+ ni 0 env (PHidden tm) = ni 0 env tm
2409+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2410+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2411+ ni 0 env (PNoImplicits tm) = ni 0 env tm
23972412
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
2413+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2414+ ni i env (PUnquote tm) = ni (i - 1) env tm
24002415
2401− ni i env tm = concatMap (ni i env) (children tm)
2416+ ni i env tm = concatMap (ni i env) (children tm)
24022417
24032418 niTacImp i env (TacImp _ _ scr) = ni i env scr
24042419 niTacImp _ _ _ = []
@@ -2413,27 +2428,27 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm
24132428 = case lookupDefExact n (tt_ctxt ist) of
24142429 Nothing -> [n]
24152430 _ -> []
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
2431+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2432+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2433+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2434+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2435+ ni 0 env (PLam fc n _ ty sc) = 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
2437+ ni 0 env (PRewrite _ 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
2439+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
24252440 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
24272442 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
2443+ ni 0 env (PHidden tm) = ni 0 env tm
2444+ ni 0 env (PUnifyLog tm) = ni 0 env tm
2445+ ni 0 env (PDisamb _ tm) = ni 0 env tm
2446+ ni 0 env (PNoImplicits tm) = ni 0 env tm
24322447
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
2448+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2449+ ni i env (PUnquote tm) = ni (i - 1) env tm
24352450
2436− ni i env tm = concatMap (ni i env) (children tm)
2451+ ni i env tm = concatMap (ni i env) (children tm)
24372452
24382453 niTacImp i env (TacImp _ _ scr) = ni i env scr
24392454 niTacImp _ _ _ = []