@@ -284,7 +284,7 @@ type UsageReason = (Name, Int) -- fn_name, its_arg_number
284284
285285data CGInfo = CGInfo { calls :: [Name],
286286 scg :: [SCGEntry],
287− usedpos :: [(Int, [UsageReason])]
287+ usedpos :: [(Int, [UsageReason])]
288288 }
289289 deriving Show
290290{-!
@@ -350,7 +350,7 @@ idrisInit = IState initContext S.empty []
350350 emptyContext emptyContext emptyContext emptyContext
351351 emptyContext emptyContext emptyContext emptyContext
352352 emptyContext emptyContext emptyContext emptyContext
353− emptyContext
353+ emptyContext
354354 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
355355 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Hidden False [] Nothing [] []
356356 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
@@ -634,13 +634,17 @@ is_scoped :: Plicity -> Maybe ImplicitInfo
634634is_scoped (Imp _ _ _ s) = s
635635is_scoped _ = Nothing
636636
637−impl = Imp [] Dynamic False (Just (Impl False True))
638−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))
639640forall_constraint = Imp [] Dynamic False (Just (Impl True False))
640−expl = Exp [] Dynamic False
641−expl_param = Exp [] Dynamic True
642−constraint = Constraint [] Static
643−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
644648
645649data FnOpt = Inlinable -- always evaluate when simplifying
646650 | TotalFn | PartialFn | CoveringFn
@@ -698,7 +702,7 @@ data PDecl' t
698702 FC -- Record name precise location
699703 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
700704 [(Name, Docstring (Either Err t))] -- Param Docs
701− [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
705+ [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
702706 (Maybe (Name, FC)) -- Optional constructor name and location
703707 (Docstring (Either Err t)) -- Constructor doc
704708 SyntaxInfo -- Constructor SyntaxInfo
@@ -932,39 +936,39 @@ declared _ = []
932936
933937-- get the names declared, not counting nested parameter blocks
934938tldeclared :: PDecl -> [Name]
935−tldeclared (PFix _ _ _) = []
936−tldeclared (PTy _ _ _ _ _ n _ t) = [n]
937−tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
938−tldeclared (PClauses _ _ n _) = [] -- not a declaration
939−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)
940944tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
941945 where fstt (_, _, a, _, _, _, _) = a
942−tldeclared (PParams _ _ ds) = []
943−tldeclared (PMutual _ ds) = concatMap tldeclared ds
944−tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
945−tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
946−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
947−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 _ = []
948952
949953defined :: PDecl -> [Name]
950−defined (PFix _ _ _) = []
951−defined (PTy _ _ _ _ _ n _ t) = []
952−defined (PPostulate _ _ _ _ _ _ n t) = []
953−defined (PClauses _ _ n _) = [n] -- not a declaration
954−defined (PCAF _ n _) = [n]
955−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
956960 where fstt (_, _, a, _, _, _, _) = a
957−defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
958−defined (PParams _ _ ds) = concatMap defined ds
959−defined (PNamespace _ _ ds) = concatMap defined ds
960−defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
961−defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
962−defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []
963−defined (PDSL n _) = [n]
964−defined (PSyntax _ _) = []
965−defined (PMutual _ ds) = concatMap defined ds
966−defined (PDirective _) = []
967−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 _ = []
968972
969973updateN :: [(Name, Name)] -> Name -> Name
970974updateN ns n | Just n' <- lookup n ns = n'
@@ -1045,33 +1049,33 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
10451049-- general-purpose FCs, and the second transforms those that are used
10461050-- for semantic source highlighting, so they can be treated specially.
10471051mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1048−mapPTermFC f g (PQuote q) = PQuote q
1049−mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1050−mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1051−mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1052−mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1053−mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1054−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)
1055−mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1056−mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1057−mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1058−mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1059−mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1060−mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1061−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)
1062−mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1063−mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1064−mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1065−mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1066−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)
1067−mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1068−mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1069−mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1070−mapPTermFC f g (PType fc) = PType (f fc)
1071−mapPTermFC f g (PUniverse u) = PUniverse u
1072−mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1073−mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1074−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
10751079mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
10761080 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
10771081 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
@@ -1079,22 +1083,22 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
10791083 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
10801084 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
10811085 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1082−mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1083−mapPTermFC f g (PReturn fc) = PReturn (f fc)
1084−mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1085−mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1086−mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1087−mapPTermFC f g (PElabError err) = PElabError err
1088−mapPTermFC f g PImpossible = PImpossible
1089−mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1090−mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1091−mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1092−mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1093−mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1094−mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1095−mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1096−mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1097−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)
10981102
10991103{-!
11001104dg instance Binary PTerm
@@ -1103,28 +1107,27 @@ deriving instance NFData PTerm
11031107
11041108mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
11051109mapPT f t = f (mpt t) where
1106− mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1107− mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1108− mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1109− mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
1110− (fmap (mapPT f) g)
1111− mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1112− mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1113− mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1114− mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1115− mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1116− 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)
11171120 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1118− mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1119− mpt (PHidden t) = PHidden (mapPT f t)
1120− mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1121− mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1122− mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1123− mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1124− mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1125− mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1126− mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1127− 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
11281131
11291132
11301133data PTactic' t = Intro [Name] | Intros | Focus Name
@@ -1165,39 +1168,39 @@ deriving instance Binary PTactic'
11651168deriving instance NFData PTactic'
11661169!-}
11671170instance Sized a => Sized (PTactic' a) where
1168− size (Intro nms) = 1 + size nms
1169− size Intros = 1
1170− size (Focus nm) = 1 + size nm
1171− size (Refine nm bs) = 1 + size nm + length bs
1172− size (Rewrite t) = 1 + size t
1173− size (Induction t) = 1 + size t
1174− size (LetTac nm t) = 1 + size nm + size t
1175− size (Exact t) = 1 + size t
1176− size Compute = 1
1177− size Trivial = 1
1178− size Solve = 1
1179− size Attack = 1
1180− size ProofState = 1
1181− size ProofTerm = 1
1182− size Undo = 1
1183− size (Try l r) = 1 + size l + size r
1184− size (TSeq l r) = 1 + size l + size r
1185− size (ApplyTactic t) = 1 + size t
1186− size (Reflect t) = 1 + size t
1187− size (Fill t) = 1 + size t
1188− size Qed = 1
1189− size Abandon = 1
1190− size Skip = 1
1191− size (TFail ts) = 1 + size ts
1192− size SourceFC = 1
1193− size DoUnify = 1
1194− size (CaseTac x) = 1 + size x
1195− size (Equiv t) = 1 + size t
1196− size (Claim x y) = 1 + size x + size y
1197− size Unfocus = 1
1198− 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
11991202 size (LetTacTy x y z) = 1 + size x + size y + size z
1200− size TCInstance = 1
1203+ size TCInstance = 1
12011204
12021205type PTactic = PTactic' PTerm
12031206
@@ -1213,11 +1216,11 @@ deriving instance NFData PDo'
12131216!-}
12141217
12151218instance Sized a => Sized (PDo' a) where
1216− size (DoExp fc t) = 1 + size fc + size t
1217− size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1218− size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1219− size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1220− 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
12211224
12221225type PDo = PDo' PTerm
12231226
@@ -1249,10 +1252,10 @@ data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
12491252 deriving (Show, Eq, Data, Typeable)
12501253
12511254instance Sized a => Sized (PArg' a) where
1252− size (PImp p _ l nm trm) = 1 + size nm + size trm
1253− size (PExp p l nm trm) = 1 + size nm + size trm
1254− size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1255− 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
12561259
12571260{-!
12581261deriving instance Binary PArg'
@@ -1260,43 +1263,43 @@ deriving instance NFData PArg'
12601263!-}
12611264
12621265pimp n t mach = PImp 1 mach [] n t
1263−pexp t = PExp 1 [] (sMN 0 "arg") t
1264−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
12651268ptacimp n s t = PTacImplicit 2 [] n s t
12661269
12671270type PArg = PArg' PTerm
12681271
12691272-- | Get the highest FC in a term, if one exists
12701273highestFC :: PTerm -> Maybe FC
1271−highestFC (PQuote _) = Nothing
1272−highestFC (PRef fc _ _) = Just fc
1273−highestFC (PInferRef fc _ _) = Just fc
1274−highestFC (PPatvar fc _) = Just fc
1275−highestFC (PLam fc _ _ _ _) = Just fc
1276−highestFC (PPi _ _ _ _ _) = Nothing
1277−highestFC (PLet fc _ _ _ _ _) = Just fc
1278−highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1279−highestFC (PApp fc _ _) = Just fc
1280−highestFC (PAppBind fc _ _) = Just fc
1281−highestFC (PMatchApp fc _) = Just fc
1282−highestFC (PCase fc _ _) = Just fc
1283−highestFC (PIfThenElse fc _ _ _) = Just fc
1284−highestFC (PTrue fc _) = Just fc
1285−highestFC (PResolveTC fc) = Just fc
1286−highestFC (PRewrite fc _ _ _) = Just fc
1287−highestFC (PPair fc _ _ _ _) = Just fc
1288−highestFC (PDPair fc _ _ _ _ _) = Just fc
1289−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
12901293highestFC (PAlternative _ _ args) =
12911294 case mapMaybe highestFC args of
12921295 [] -> Nothing
12931296 (fc:_) -> Just fc
1294−highestFC (PHidden _) = Nothing
1295−highestFC (PType fc) = Just fc
1296−highestFC (PUniverse _) = Nothing
1297−highestFC (PGoal fc _ _ _) = Just fc
1298−highestFC (PConstant fc _) = Just fc
1299−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
13001303highestFC (PDoBlock lines) =
13011304 case map getDoFC lines of
13021305 [] -> Nothing
@@ -1308,23 +1311,23 @@ highestFC (PDoBlock lines) =
13081311 getDoFC (DoLet fc nm nfc l r) = fc
13091312 getDoFC (DoLetP fc l r) = fc
13101313
1311−highestFC (PIdiom fc _) = Just fc
1312−highestFC (PReturn fc) = Just fc
1313−highestFC (PMetavar fc _) = Just fc
1314−highestFC (PProof _) = Nothing
1315−highestFC (PTactics _) = Nothing
1316−highestFC (PElabError _) = Nothing
1317−highestFC PImpossible = Nothing
1318−highestFC (PCoerced tm) = highestFC tm
1319−highestFC (PDisamb _ opts) = highestFC opts
1320−highestFC (PUnifyLog tm) = highestFC tm
1321−highestFC (PNoImplicits tm) = highestFC tm
1322−highestFC (PQuasiquote _ _) = Nothing
1323−highestFC (PUnquote tm) = highestFC tm
1324−highestFC (PQuoteName _ _ fc) = Just fc
1325−highestFC (PRunElab fc _ _) = Just fc
1326−highestFC (PConstSugar fc _) = Just fc
1327−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
13281331
13291332-- Type class data
13301333
@@ -1402,11 +1405,11 @@ data Syntax = Rule [SSymbol] PTerm SynContext
14021405
14031406syntaxNames :: Syntax -> [Name]
14041407syntaxNames (Rule syms _ _) = mapMaybe ename syms
1405− where ename (Keyword n) = Just n
1406− ename _ = Nothing
1408+ where ename (Keyword n) = Just n
1409+ ename _ = Nothing
14071410syntaxNames (DeclRule syms _) = mapMaybe ename syms
1408− where ename (Keyword n) = Just n
1409− ename _ = Nothing
1411+ where ename (Keyword n) = Just n
1412+ ename _ = Nothing
14101413
14111414syntaxSymbols :: Syntax -> [SSymbol]
14121415syntaxSymbols (Rule ss _ _) = ss
@@ -1439,9 +1442,9 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
14391442 where
14401443 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
14411444
1442− ruleSort [] [] = EQ
1443− ruleSort [] _ = LT
1444− ruleSort _ [] = GT
1445+ ruleSort [] [] = EQ
1446+ ruleSort [] _ = LT
1447+ ruleSort _ [] = GT
14451448 ruleSort (s1:ss1) (s2:ss2) =
14461449 case symCompare s1 s2 of
14471450 EQ -> ruleSort ss1 ss2
@@ -1449,25 +1452,25 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
14491452
14501453 -- Better than creating Ord instance for SSymbol since
14511454 -- in general this ordering does not really make sense.
1452− symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1453− symCompare (Keyword _) _ = LT
1454− symCompare (Symbol _) (Keyword _) = GT
1455− symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1456− symCompare (Symbol _) _ = LT
1457− symCompare (Binding _) (Keyword _) = GT
1458− symCompare (Binding _) (Symbol _) = GT
1459− symCompare (Binding b1) (Binding b2) = compare b1 b2
1460− symCompare (Binding _) _ = LT
1461− symCompare (Expr _) (Keyword _) = GT
1462− symCompare (Expr _) (Symbol _) = GT
1463− symCompare (Expr _) (Binding _) = GT
1464− symCompare (Expr e1) (Expr e2) = compare e1 e2
1465− symCompare (Expr _) _ = LT
1466− symCompare (SimpleExpr _) (Keyword _) = GT
1467− symCompare (SimpleExpr _) (Symbol _) = GT
1468− symCompare (SimpleExpr _) (Binding _) = GT
1469− symCompare (SimpleExpr _) (Expr _) = GT
1470− 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
14711474
14721475initDSL = DSL (PRef f [] (sUN ">>="))
14731476 (PRef f [] (sUN "return"))
@@ -1539,10 +1542,10 @@ getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
15391542getInferTerm (App _ (App _ _ _) tm) = tm
15401543getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
15411544
1542−getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1543− where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1544− toTy (PVar t) = PVTy t
1545− 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
15461549getInferType (App _ (App _ _ ty) _) = ty
15471550
15481551
@@ -1564,12 +1567,12 @@ falseTy = sUN "Void"
15641567pairTy = sNS (sUN "Pair") ["Builtins"]
15651568pairCon = sNS (sUN "MkPair") ["Builtins"]
15661569
1567−upairTy = sNS (sUN "UPair") ["Builtins"]
1568−upairCon = sNS (sUN "MkUPair") ["Builtins"]
1570+upairTy = sNS (sUN "UPair") ["Builtins"]
1571+upairCon = sNS (sUN "MkUPair") ["Builtins"]
15691572
1570−eqTy = sUN "="
1573+eqTy = sUN "="
15711574eqCon = sUN "Refl"
1572−eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1575+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
15731576 "The propositional equality type. A proof that `x` = `y`." ++
15741577 "\n\n" ++
15751578 "To use such a proof, pattern-match on it, and the two equal things will " ++
@@ -1612,7 +1615,7 @@ modDocName :: Name
16121615modDocName = sMN 0 "ModuleDocs"
16131616
16141617-- Defined in builtins.idr
1615−sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1618+sigmaTy = sNS (sUN "Sigma") ["Builtins"]
16161619sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
16171620
16181621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
@@ -1653,11 +1656,11 @@ annotationColour ist (AnnConst c) =
16531656 in Just $ if constIsType c
16541657 then typeColour theme
16551658 else dataColour theme
1656−annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1657−annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1658−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)
16591662annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1660−annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1663+annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
16611664annotationColour ist (AnnName n _ _ _) =
16621665 let ctxt = tt_ctxt ist
16631666 theme = idris_colourTheme ist
@@ -1759,7 +1762,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17591762 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
17601763 depth d . bracket p startPrec $
17611764 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1762− prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
1765+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
17631766 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
17641767 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
17651768 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
@@ -1796,7 +1799,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17961799 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
17971800 [l,r] -> let precedence = maybe (startPrec - 1) prec f
17981801 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1799− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1802+ (l@(PExp{}) : r@(PExp{}) : rest) ->
18001803 depth d . bracket p funcAppPrec $
18011804 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
18021805 align (group (vsep (map (prettyArgS d bnd) rest)))
@@ -1847,20 +1850,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18471850 -- disambiguation on PDPair.
18481851 vars tm = filter noNS (allNamesIn tm)
18491852 noNS (NS _ _) = False
1850− noNS _ = True
1853+ noNS _ = True
18511854
18521855 prettySe d p bnd (PIfThenElse _ c t f) =
18531856 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1854− [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1857+ [ kwd "if" <+> prettySe (decD d) startPrec bnd c
18551858 , kwd "then" <+> prettySe (decD d) startPrec bnd t
18561859 , kwd "else" <+> prettySe (decD d) startPrec bnd f
18571860 ]
1858− prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1859− prettySe d p bnd (PResolveTC _) = kwd "%instance"
1860− prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1861− 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 "()"
18621865 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1863− prettySe d p bnd (PRewrite _ l r _) =
1866+ prettySe d p bnd (PRewrite _ l r _) =
18641867 depth d . bracket p startPrec $
18651868 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
18661869 prettySe d p bnd (PTyped l r) =
@@ -1870,9 +1873,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18701873 align . group . vsep . punctuate (ann comma) $
18711874 map (prettySe (decD d) startPrec bnd) elts
18721875 where ann = case pun of
1873− TypeOrTerm -> id
1874− IsType -> annName pairTy
1875− IsTerm -> annName pairCon
1876+ TypeOrTerm -> id
1877+ IsType -> annName pairTy
1878+ IsTerm -> annName pairCon
18761879 prettySe d p bnd (PDPair _ _ pun l t r) =
18771880 depth d $
18781881 annotated lparen <>
@@ -1881,30 +1884,32 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18811884 prettySe (decD d) startPrec (addBinding bnd) r <>
18821885 annotated rparen
18831886 where annotated = case pun of
1884− IsType -> annName sigmaTy
1885− IsTerm -> annName sigmaCon
1886− TypeOrTerm -> id
1887+ IsType -> annName sigmaTy
1888+ IsTerm -> annName sigmaCon
1889+ TypeOrTerm -> id
18871890 (left, addBinding) = case (l, pun) of
18881891 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1889− _ -> (prettySe (decD d) startPrec bnd l, id)
1892+ _ -> (prettySe (decD d) startPrec bnd l, id)
18901893 prettySe d p bnd (PAlternative ns a as) =
18911894 lparen <> text "|" <> prettyAs <> text "|" <> rparen
18921895 where
18931896 prettyAs =
1894− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1895− prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1896− prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1897− 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))
18981903 -- XXX: add pretty for tactics
1899− prettySe d p bnd (PProof ts) =
1904+ prettySe d p bnd (PProof ts) =
19001905 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1901− prettySe d p bnd (PTactics ts) =
1906+ prettySe d p bnd (PTactics ts) =
19021907 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1903− prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1904− prettySe d p bnd (PReturn f) = kwd "return"
1905− prettySe d p bnd PImpossible = kwd "impossible"
1906− prettySe d p bnd Placeholder = text "_"
1907− 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) =
19081913 bracket p startPrec $
19091914 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
19101915 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
@@ -1926,47 +1931,46 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
19261931 text "no pretty printer for pattern-matching do binding" :
19271932 ppdo bnd dos
19281933 ppdo _ [] = []
1929− prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1930− 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
19311936 -- Quasiquote pprinting ignores bound vars
1932− 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 ")"
19331938 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1934− prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1935− 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
19361941 where start = if res then "`{" else "`{{"
19371942 end = if res then "}" else "}}"
1938− prettySe d p bnd (PRunElab _ tm _) =
1943+ prettySe d p bnd (PRunElab _ tm _) =
19391944 bracket p funcAppPrec . group . align . hang 2 $
19401945 text "%runElab" <$>
19411946 prettySe (decD d) funcAppPrec bnd tm
1942− prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1943−
1944− 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"
19451949
19461950 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
19471951 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
19481952 where display (UN n) = T.unpack n
19491953 display (MN _ n) = T.unpack n
19501954 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1951− 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
19521956 display n = show n
19531957
1954− prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1955− prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1956− prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1957− 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)
19581962
1959− prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1960− prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1961− 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
19621966 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
19631967
19641968 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
19651969 annName n = annotate (AnnName n Nothing Nothing Nothing)
19661970
19671971 opStr :: Name -> String
1968− opStr (NS n _) = opStr n
1969− opStr (UN n) = T.unpack n
1972+ opStr (NS n _) = opStr n
1973+ opStr (UN n) = T.unpack n
19701974
19711975 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
19721976 slist' (Just d) _ _ _ | d <= 0 = Nothing
@@ -2028,7 +2032,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20282032 ellipsis = text "..."
20292033
20302034 depth Nothing = id
2031− depth (Just d) = if d <= 0 then const (ellipsis) else id
2035+ depth (Just d) = if d <= 0 then const ellipsis else id
20322036
20332037 decD = fmap (\x -> x - 1)
20342038
@@ -2043,7 +2047,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20432047-- | Strip away namespace information
20442048basename :: Name -> Name
20452049basename (NS n _) = basename n
2046−basename n = n
2050+basename n = n
20472051
20482052-- | Determine whether a name was the one inserted for a hole or
20492053-- guess by the delaborator
@@ -2063,15 +2067,15 @@ prettyName
20632067 -> Name -- ^^ the name to pprint
20642068 -> Doc OutputAnnotation
20652069prettyName infixParen showNS bnd n
2066− | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2067− | (UN n') <- n, T.unpack n' == "_" = text "_"
2068− | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2069− | 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
20702074 where fullName = text nameSpace <> parenthesise (text (baseName n))
2071− baseName (UN n) = T.unpack n
2072− baseName (NS n ns) = baseName n
2073− baseName (MN i s) = T.unpack s
2074− 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
20752079 nameSpace = case n of
20762080 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
20772081 _ -> ""
@@ -2086,13 +2090,13 @@ showCImp ppo (PClause _ n l ws r w)
20862090 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
20872091 <+> text "where" <+> text (show w)
20882092 where
2089− showWs [] = empty
2093+ showWs [] = empty
20902094 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
20912095showCImp ppo (PWith _ n l ws r pn w)
20922096 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
20932097 <+> braces (text (show w))
20942098 where
2095− showWs [] = empty
2099+ showWs [] = empty
20962100 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
20972101
20982102
@@ -2104,13 +2108,13 @@ showDImp ppo (PDatadecl n nfc ty cons)
21042108showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
21052109showDecls o ds = vsep (map (showDeclImp o) ds)
21062110
2107−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))
21082112showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2109−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" <+>
21102114 indent 2 (vsep (map (showCImp o) cs))
2111−showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2112−showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2113−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)
21142118showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
21152119showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
21162120 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
@@ -2121,26 +2125,26 @@ showDeclImp _ _ = text "..."
21212125
21222126getImps :: [PArg] -> [(Name, PTerm)]
21232127getImps [] = []
2124−getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2125−getImps (_ : xs) = getImps xs
2128+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2129+getImps (_ : xs) = getImps xs
21262130
21272131getExps :: [PArg] -> [PTerm]
21282132getExps [] = []
2129−getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2130−getExps (_ : xs) = getExps xs
2133+getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2134+getExps (_ : xs) = getExps xs
21312135
21322136getShowArgs :: [PArg] -> [PArg]
21332137getShowArgs [] = []
21342138getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
21352139getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
21362140 | PImp _ _ _ _ tm <- e
2137− , containsHole tm = e : getShowArgs xs
2141+ , containsHole tm = e : getShowArgs xs
21382142getShowArgs (_ : xs) = getShowArgs xs
21392143
21402144getConsts :: [PArg] -> [PTerm]
2141−getConsts [] = []
2145+getConsts [] = []
21422146getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2143−getConsts (_ : xs) = getConsts xs
2147+getConsts (_ : xs) = getConsts xs
21442148
21452149getAll :: [PArg] -> [PTerm]
21462150getAll = map getTm
@@ -2154,13 +2158,13 @@ showName :: Maybe IState -- ^^ the Idris state, for information about names an
21542158 -> Name -- ^^ the term to show
21552159 -> String
21562160showName ist bnd ppo colour n = case ist of
2157− Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2158− Nothing -> showbasic n
2161+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2162+ Nothing -> showbasic n
21592163 where name = if ppopt_impl ppo then show n else showbasic n
2160− showbasic n@(UN _) = showCG n
2161− showbasic (MN i s) = str s
2162− showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2163− 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
21642168 fst3 (x, _, _) = x
21652169 colourise n t = let ctxt' = fmap tt_ctxt ist in
21662170 case ctxt' of
@@ -2192,42 +2196,42 @@ showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
21922196
21932197
21942198instance Sized PTerm where
2195− size (PQuote rawTerm) = size rawTerm
2196− size (PRef fc _ name) = size name
2197− size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2198− size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2199− size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2200− size (PTyped trm ty) = 1 + size trm + size ty
2201− size (PApp fc name args) = 1 + size args
2202− size (PAppBind fc name args) = 1 + size args
2203− size (PCase fc trm bdy) = 1 + size trm + size bdy
2204− size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2205− size (PTrue fc _) = 1
2206− size (PResolveTC fc) = 1
2207− size (PRewrite fc left right _) = 1 + size left + size right
2208− size (PPair fc _ _ left right) = 1 + size left + size right
2209− size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2210− size (PAlternative _ a alts) = 1 + size alts
2211− size (PHidden hidden) = size hidden
2212− size (PUnifyLog tm) = size tm
2213− size (PDisamb _ tm) = size tm
2214− size (PNoImplicits tm) = size tm
2215− size (PType _) = 1
2216− size (PUniverse _) = 1
2217− size (PConstant fc const) = 1 + size fc + size const
2218− size Placeholder = 1
2219− size (PDoBlock dos) = 1 + size dos
2220− size (PIdiom fc term) = 1 + size term
2221− size (PReturn fc) = 1
2222− size (PMetavar _ name) = 1
2223− size (PProof tactics) = size tactics
2224− size (PElabError err) = size err
2225− size PImpossible = 1
2226− 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
22272231
22282232getPArity :: PTerm -> Int
2229−getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2230−getPArity _ = 0
2233+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2234+getPArity _ = 0
22312235
22322236-- Return all names, free or globally bound, in the given term.
22332237
@@ -2235,31 +2239,30 @@ allNamesIn :: PTerm -> [Name]
22352239allNamesIn tm = nub $ ni 0 [] tm
22362240 where -- TODO THINK added niTacImp, but is it right?
22372241 ni 0 env (PRef _ _ n)
2238− | not (n `elem` env) = [n]
2239− ni 0 env (PPatvar _ n) = [n]
2240− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2241− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2242− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)
2243− ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2244− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2245− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2246− ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2247− ni 0 env (PHidden tm) = ni 0 env tm
2248− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2249− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2250− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2251− ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2252− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2253− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2254− ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2255− ni 0 env (PUnifyLog tm) = ni 0 env tm
2256− ni 0 env (PDisamb _ tm) = ni 0 env tm
2257− ni 0 env (PNoImplicits tm) = ni 0 env tm
2258−
2259− ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2260− 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
22612262
2262− 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)
22632266
22642267 niTacImp i env (TacImp _ _ scr) = ni i env scr
22652268 niTacImp _ _ _ = []
@@ -2270,32 +2273,32 @@ boundNamesIn :: PTerm -> [Name]
22702273boundNamesIn tm = S.toList (ni 0 S.empty tm)
22712274 where -- TODO THINK Added niTacImp, but is it right?
22722275 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2273− ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2274− ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2275− ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2276− ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2277− ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2278− ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2279− ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2280− ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r
2281− ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2282− 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
22832286 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2284− ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2285− ni 0 set (PAlternative ns a as) = niTms 0 set as
2286− ni 0 set (PHidden tm) = ni 0 set tm
2287− ni 0 set (PUnifyLog tm) = ni 0 set tm
2288− ni 0 set (PDisamb _ tm) = ni 0 set tm
2289− 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
22902293
2291− ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2292− 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
22932296
2294− 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)
22952298
22962299 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2297− niTms i set [] = set
2298− 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
22992302
23002303 niTacImp i set (TacImp _ _ scr) = ni i set scr
23012304 niTacImp i set _ = set
@@ -2311,18 +2314,18 @@ implicitNamesIn uvars ist tm
23112314 addFn n = do (imps, fns) <- get
23122315 put (imps, n: fns)
23132316
2314− notCAF [] = False
2317+ notCAF [] = False
23152318 notCAF (PExp _ _ _ _ : _) = True
2316− notCAF (_ : xs) = notCAF xs
2319+ notCAF (_ : xs) = notCAF xs
23172320
23182321 notHidden (n, _) = case getAccessibility n of
2319− Hidden -> False
2320− _ -> True
2322+ Hidden -> False
2323+ _ -> True
23212324
23222325 getAccessibility n
23232326 = case lookupDefAccExact n False (tt_ctxt ist) of
2324− Just (n,t) -> t
2325− _ -> Public
2327+ Just (n,t) -> t
2328+ _ -> Public
23262329
23272330 ni 0 env (PRef _ _ n@(NS _ _))
23282331 | not (n `elem` env)
@@ -2332,44 +2335,44 @@ implicitNamesIn uvars ist tm
23322335 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
23332336 ni 0 env (PApp _ f@(PRef _ _ n) as)
23342337 | n `elem` uvars = do ni 0 env f
2335− mapM_ (ni 0 env) (map getTm as)
2338+ mapM_ (ni 0 env . getTm) as
23362339 | otherwise = do case lookupTy n (tt_ctxt ist) of
2337− [] -> return ()
2338− _ -> addFn n
2339− mapM_ (ni 0 env) (map getTm as)
2340+ [] -> return ()
2341+ _ -> addFn n
2342+ mapM_ (ni 0 env . getTm) as
23402343 ni 0 env (PApp _ f as) = do ni 0 env f
2341− mapM_ (ni 0 env) (map getTm as)
2344+ mapM_ (ni 0 env . getTm) as
23422345 ni 0 env (PAppBind _ f as) = do ni 0 env f
2343− mapM_ (ni 0 env) (map getTm as)
2346+ mapM_ (ni 0 env . getTm) as
23442347 ni 0 env (PCase _ c os) = do ni 0 env c
23452348 -- names in 'os', not counting the names bound in the cases
2346− mapM_ (ni 0 env) (map snd os)
2349+ mapM_ (ni 0 env . snd) os
23472350 (imps, fns) <- get
23482351 put ([] ,[])
2349− mapM_ (ni 0 env) (map fst os)
2352+ mapM_ (ni 0 env . fst) os
23502353 (impsfst, _) <- get
23512354 put (nub imps \\ nub impsfst, fns)
2352− ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2353− ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2354− ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2355− ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r
2356− ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2357− ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2358− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2359− ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2360− ni 0 env t
2361− ni 0 env r
2362− ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2363− ni 0 env (PHidden tm) = ni 0 env tm
2364− ni 0 env (PUnifyLog tm) = ni 0 env tm
2365− ni 0 env (PDisamb _ tm) = ni 0 env tm
2366− 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
23672370
23682371 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
23692372 maybe (return ()) (ni i env) ty
23702373 ni i env (PUnquote tm) = ni (i - 1) env tm
23712374
2372− ni i env tm = mapM_ (ni i env) (children tm)
2375+ ni i env tm = mapM_ (ni i env) (children tm)
23732376
23742377-- Return names which are free in the given term.
23752378namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
@@ -2378,32 +2381,32 @@ namesIn uvars ist tm = nub $ ni 0 [] tm
23782381 ni 0 env (PRef _ _ n)
23792382 | not (n `elem` env)
23802383 = case lookupTy n (tt_ctxt ist) of
2381− [] -> [n]
2382− _ -> if n `elem` (map fst uvars) then [n] else []
2383− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2384− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2385− 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 ++
23862389 -- names in 'os', not counting the names bound in the cases
2387− (nub (concatMap (ni 0 env) (map snd os))
2388− \\ nub (concatMap (ni 0 env) (map fst os)))
2389− 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]
23902393 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2391− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2392− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2393− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2394− 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
23952398 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2396− 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
23972400 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2398− ni 0 env (PHidden tm) = ni 0 env tm
2399− ni 0 env (PUnifyLog tm) = ni 0 env tm
2400− ni 0 env (PDisamb _ tm) = ni 0 env tm
2401− 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
24022405
2403− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2404− 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
24052408
2406− ni i env tm = concatMap (ni i env) (children tm)
2409+ ni i env tm = concatMap (ni i env) (children tm)
24072410
24082411 niTacImp i env (TacImp _ _ scr) = ni i env scr
24092412 niTacImp _ _ _ = []
@@ -2418,27 +2421,27 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm
24182421 = case lookupDefExact n (tt_ctxt ist) of
24192422 Nothing -> [n]
24202423 _ -> []
2421− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2422− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2423− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)
2424− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2425− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2426− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2427− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2428− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2429− 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
24302433 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2431− 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
24322435 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2433− ni 0 env (PHidden tm) = ni 0 env tm
2434− ni 0 env (PUnifyLog tm) = ni 0 env tm
2435− ni 0 env (PDisamb _ tm) = ni 0 env tm
2436− 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
24372440
2438− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2439− 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
24402443
2441− ni i env tm = concatMap (ni i env) (children tm)
2444+ ni i env tm = concatMap (ni i env) (children tm)
24422445
24432446 niTacImp i env (TacImp _ _ scr) = ni i env scr
24442447 niTacImp _ _ _ = []