46b5cb6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2950 from Heather/colours

46b5cb6Niklas Larsson11 years ago

src/Idris/AbsSyntax.hs+26−27

compare with master

unifiedsplit

@@ -77,7 +77,7 @@ addDyLib libs = do i <- getIState

77 (\_ -> return Nothing)) $ libs

78 case msum handle of

79 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

80− concat (intersperse "," libs) ++ "\"")

80+ intercalate "," libs ++ "\"")

81 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }

82 return (Left x)

83 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib

@@ -235,8 +235,7 @@ getCoercionsTo i ty =

235 findCoercions t (n : ns) =

236 let ps = case lookupTy n (tt_ctxt i) of

237 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of

238− (t', _) ->

238+ (t', _) -> [n | t == t']

239− if t == t' then [n] else []

240 _ -> [] in

239 _ -> [] in

241 ps ++ findCoercions t ns

240 ps ++ findCoercions t ns

242

241

@@ -250,7 +249,7 @@ addCalls n calls

250 = do i <- getIState

249 = do i <- getIState

251 case lookupCtxtExact n (idris_callgraph i) of

250 case lookupCtxtExact n (idris_callgraph i) of

252 Nothing -> addToCG n (CGInfo calls [] [])

251 Nothing -> addToCG n (CGInfo calls [] [])

253− Just (CGInfo cs scg used) ->

252+ Just (CGInfo cs scg used) ->

254 addToCG n (CGInfo (nub (calls ++ cs)) scg used)

253 addToCG n (CGInfo (nub (calls ++ cs)) scg used)

255

254

256addTyInferred :: Name -> Idris ()

255addTyInferred :: Name -> Idris ()

@@ -268,7 +267,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

268 findMVApps x y

267 findMVApps x y

269 = do let (fx, argsx) = unApply x

268 = do let (fx, argsx) = unApply x

270 let (fy, argsy) = unApply y

269 let (fy, argsy) = unApply y

271− if (not (fx == fy))

270+ if (fx /= fy)

272 then do

271 then do

273 tryAddMV fx y

272 tryAddMV fx y

274 tryAddMV fy x

273 tryAddMV fy x

@@ -1070,7 +1069,7 @@ logLvlCats cs l str = do

1070 runIO . hPutStrLn h $ convSExp "log" good n

1069 runIO . hPutStrLn h $ convSExp "log" good n

1071 where

1070 where

1072 inCat :: [LogCat] -> [LogCat] -> Bool

1071 inCat :: [LogCat] -> [LogCat] -> Bool

1073− inCat cs cats = or $ map (\x -> elem x cats) cs

1072+ inCat cs cats = any (`elem` cats) cs

1074

1073

1075cmdOptType :: Opt -> Idris Bool

1074cmdOptType :: Opt -> Idris Bool

1076cmdOptType x = do i <- getIState

1075cmdOptType x = do i <- getIState

@@ -1147,25 +1146,25 @@ expandParams dec ps ns infs tm = en 0 tm

1147 | n `nselem` ns = PQuote (Var (dec n))

1146 | n `nselem` ns = PQuote (Var (dec n))

1148 en 0 (PApp fc (PInferRef fc' hl n) as)

1147 en 0 (PApp fc (PInferRef fc' hl n) as)

1149 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1148 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1150− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1149+ (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))

1151 en 0 (PApp fc (PRef fc' hl n) as)

1150 en 0 (PApp fc (PRef fc' hl n) as)

1152 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))

1151 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))

1153− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1152+ (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))

1154 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1153 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1155− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1154+ (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))

1156 en 0 (PAppBind fc (PRef fc' hl n) as)

1155 en 0 (PAppBind fc (PRef fc' hl n) as)

1157 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))

1156 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))

1158− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1157+ (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))

1159 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1158 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1160− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1159+ (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))

1161 en 0 (PRef fc hl n)

1160 en 0 (PRef fc hl n)

1162 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1161 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1163− (map (pexp . (PRef fc hl)) (map fst ps))

1162+ (map ((pexp . (PRef fc hl)) . fst) ps)

1164 | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1163 | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1165− (map (pexp . (PRef fc hl)) (map fst ps))

1164+ (map ((pexp . (PRef fc hl)) . fst) ps)

1166 en 0 (PInferRef fc hl n)

1165 en 0 (PInferRef fc hl n)

1167 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1166 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1168− (map (pexp . (PRef fc hl)) (map fst ps))

1167+ (map ((pexp . (PRef fc hl)) . fst) ps)

1169 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)

1168 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)

1170 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)

1169 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)

1171 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)

1170 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)

@@ -1237,7 +1236,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

1237 removeBound lhs ns = ns \\ nub (bnames lhs)

1236 removeBound lhs ns = ns \\ nub (bnames lhs)

1238

1237

1239 bnames (PRef _ _ n) = [n]

1238 bnames (PRef _ _ n) = [n]

1240− bnames (PApp _ _ args) = concatMap bnames (map getTm args)

1239+ bnames (PApp _ _ args) = concatMap (bnames . getTm) args

1241 bnames (PPair _ _ _ l r) = bnames l ++ bnames r

1240 bnames (PPair _ _ _ l r) = bnames l ++ bnames r

1242 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r

1241 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r

1243 bnames _ = []

1242 bnames _ = []

@@ -1304,9 +1303,9 @@ getPriority i tm = 1 -- pri tm

1304 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))

1303 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))

1305 pri (PTrue _ _) = 0

1304 pri (PTrue _ _) = 0

1306 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1305 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1307− pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

1306+ pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

1308− pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

1307+ pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

1309− pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

1308+ pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))

1310 pri (PTyped l r) = pri l

1309 pri (PTyped l r) = pri l

1311 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))

1310 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))

1312 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1311 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

@@ -1323,11 +1322,11 @@ addStatics n tm ptm =

1323 let paramnames

1322 let paramnames

1324 = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1323 = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1325 Just p -> getNamesFrom 0 (fn_params p) tm ++

1324 Just p -> getNamesFrom 0 (fn_params p) tm ++

1326− concatMap (getParamNames ist) (map snd statics)

1325+ concatMap (getParamNames ist . snd) statics

1327− _ -> concatMap (getParamNames ist) (map snd statics)

1326+ _ -> concatMap (getParamNames ist . snd) statics

1328

1327

1329− let stnames = nub $ concatMap freeArgNames (map snd statics)

1328+ let stnames = nub $ concatMap (freeArgNames . snd) statics

1330− let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

1329+ let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)

1331 \\ paramnames

1330 \\ paramnames

1332 -- also get the arguments which are 'uniquely inferrable' from

1331 -- also get the arguments which are 'uniquely inferrable' from

1333 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

1332 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

@@ -1336,7 +1335,7 @@ addStatics n tm ptm =

1336 filter (\x -> not (elem x dnames)) stnames

1335 filter (\x -> not (elem x dnames)) stnames

1337 let stpos = staticList statics' tm

1336 let stpos = staticList statics' tm

1338 i <- getIState

1337 i <- getIState

1339− when (not (null statics)) $

1338+ unless (null statics) $

1340 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"

1339 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"

1341 ++ showTmImpls ptm ++ "\n"

1340 ++ showTmImpls ptm ++ "\n"

1342 ++ show statics ++ "\n" ++ show dynamics

1341 ++ show statics ++ "\n" ++ show dynamics

@@ -1422,7 +1421,7 @@ addUsingConstraints syn fc t

1422 | otherwise = doAdd cs ns t

1421 | otherwise = doAdd cs ns t

1423

1422

1424 mkConst c args = PApp fc (PRef fc [] c)

1423 mkConst c args = PApp fc (PRef fc [] c)

1425− (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc [] n)) args)

1424+ (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)

1426

1425

1427 getConstraints (PPi (Constraint _ _) _ _ c sc)

1426 getConstraints (PPi (Constraint _ _) _ _ c sc)

1428 = getcapp c ++ getConstraints sc

1427 = getcapp c ++ getConstraints sc

@@ -1448,7 +1447,7 @@ addUsingImpls syn n fc t

1448

1447

1449 let badnames = filter (\n -> not (implicitable n) &&

1448 let badnames = filter (\n -> not (implicitable n) &&

1450 n `notElem` (map iname uimpls)) ns

1449 n `notElem` (map iname uimpls)) ns

1451− when (not (null badnames)) $

1450+ unless (null badnames) $

1452 throwError (At fc (Elaborating "type of " n Nothing

1451 throwError (At fc (Elaborating "type of " n Nothing

1453 (NoSuchVariable (head badnames))))

1452 (NoSuchVariable (head badnames))))

1454 let cs = getArgnames t -- get already bound names

1453 let cs = getArgnames t -- get already bound names

@@ -1532,7 +1531,7 @@ implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1532implicit' info syn ignore n ptm

1531implicit' info syn ignore n ptm

1533 = do i <- getIState

1532 = do i <- getIState

1534 auto <- getAutoImpls

1533 auto <- getAutoImpls

1535− if not auto

1534+ if not auto

1536 then return ptm

1535 then return ptm

1537 else do

1536 else do

1538 let (tm', impdata) = implicitise syn ignore i ptm

1537 let (tm', impdata) = implicitise syn ignore i ptm

@@ -1588,7 +1587,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1588 -- Find names in argument position in a type, suitable for implicit

1587 -- Find names in argument position in a type, suitable for implicit

1589 -- binding

1588 -- binding

1590 -- Not the function position, but do everything else...

1589 -- Not the function position, but do everything else...

1591− implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)

1590+ implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args

1592 implNamesIn uv t = namesIn uv ist t

1591 implNamesIn uv t = namesIn uv ist t

1593

1592

1594 imps top env ty@(PApp _ f as)

1593 imps top env ty@(PApp _ f as)

src/Idris/AbsSyntaxTree.hs+450−447

@@ -284,7 +284,7 @@ type UsageReason = (Name, Int) -- fn_name, its_arg_number

284

285data CGInfo = CGInfo { calls :: [Name],

286 scg :: [SCGEntry],

287− usedpos :: [(Int, [UsageReason])]

287+ usedpos :: [(Int, [UsageReason])]

288 }

289 deriving Show

290{-!

@@ -350,7 +350,7 @@ idrisInit = IState initContext S.empty []

350 emptyContext emptyContext emptyContext emptyContext

351 emptyContext emptyContext emptyContext emptyContext

352 emptyContext emptyContext emptyContext emptyContext

353− emptyContext

353+ emptyContext

354 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

355 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Hidden False [] Nothing [] []

356 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

@@ -634,13 +634,17 @@ is_scoped :: Plicity -> Maybe ImplicitInfo

634is_scoped (Imp _ _ _ s) = s

635is_scoped _ = Nothing

636

637−impl = Imp [] Dynamic False (Just (Impl False True))

637+impl = Imp [] Dynamic False (Just (Impl False True))

638+

638−forall_imp = Imp [] Dynamic False (Just (Impl False False))

639+forall_imp = Imp [] Dynamic False (Just (Impl False False))

639forall_constraint = Imp [] Dynamic False (Just (Impl True False))

640forall_constraint = Imp [] Dynamic False (Just (Impl True False))

641+

640−expl = Exp [] Dynamic False

642+expl = Exp [] Dynamic False

641−expl_param = Exp [] Dynamic True

643+expl_param = Exp [] Dynamic True

644+

642−constraint = Constraint [] Static

645+constraint = Constraint [] Static

646+

643−tacimpl t = TacImp [] Dynamic t

647+tacimpl t = TacImp [] Dynamic t

644

648

645data FnOpt = Inlinable -- always evaluate when simplifying

649data FnOpt = Inlinable -- always evaluate when simplifying

646 | TotalFn | PartialFn | CoveringFn

650 | TotalFn | PartialFn | CoveringFn

@@ -698,7 +702,7 @@ data PDecl' t

698 FC -- Record name precise location

702 FC -- Record name precise location

699 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

703 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

700 [(Name, Docstring (Either Err t))] -- Param Docs

704 [(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

702 (Maybe (Name, FC)) -- Optional constructor name and location

706 (Maybe (Name, FC)) -- Optional constructor name and location

703 (Docstring (Either Err t)) -- Constructor doc

707 (Docstring (Either Err t)) -- Constructor doc

704 SyntaxInfo -- Constructor SyntaxInfo

708 SyntaxInfo -- Constructor SyntaxInfo

@@ -932,39 +936,39 @@ declared _ = []

932

936

933-- get the names declared, not counting nested parameter blocks

937-- get the names declared, not counting nested parameter blocks

934tldeclared :: PDecl -> [Name]

938tldeclared :: PDecl -> [Name]

935−tldeclared (PFix _ _ _) = []

939+tldeclared (PFix _ _ _) = []

936−tldeclared (PTy _ _ _ _ _ n _ t) = [n]

940+tldeclared (PTy _ _ _ _ _ n _ t) = [n]

937−tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]

941+tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]

938−tldeclared (PClauses _ _ n _) = [] -- not a declaration

942+tldeclared (PClauses _ _ n _) = [] -- not a declaration

939−tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

943+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

940tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

944tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

941 where fstt (_, _, a, _, _, _, _) = a

945 where fstt (_, _, a, _, _, _, _) = a

942−tldeclared (PParams _ _ ds) = []

946+tldeclared (PParams _ _ ds) = []

943−tldeclared (PMutual _ ds) = concatMap tldeclared ds

947+tldeclared (PMutual _ ds) = concatMap tldeclared ds

944−tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds

948+tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds

945−tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

949+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

946−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

950+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

947−tldeclared _ = []

951+tldeclared _ = []

948

952

949defined :: PDecl -> [Name]

953defined :: PDecl -> [Name]

950−defined (PFix _ _ _) = []

954+defined (PFix _ _ _) = []

951−defined (PTy _ _ _ _ _ n _ t) = []

955+defined (PTy _ _ _ _ _ n _ t) = []

952−defined (PPostulate _ _ _ _ _ _ n t) = []

956+defined (PPostulate _ _ _ _ _ _ n t) = []

953−defined (PClauses _ _ n _) = [n] -- not a declaration

957+defined (PClauses _ _ n _) = [n] -- not a declaration

954−defined (PCAF _ n _) = [n]

958+defined (PCAF _ n _) = [n]

955−defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

959+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

956 where fstt (_, _, a, _, _, _, _) = a

960 where fstt (_, _, a, _, _, _, _) = a

957−defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

961+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

958−defined (PParams _ _ ds) = concatMap defined ds

962+defined (PParams _ _ ds) = concatMap defined ds

959−defined (PNamespace _ _ ds) = concatMap defined ds

963+defined (PNamespace _ _ ds) = concatMap defined ds

960−defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

964+defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

961−defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

965+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

962−defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

966+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

963−defined (PDSL n _) = [n]

967+defined (PDSL n _) = [n]

964−defined (PSyntax _ _) = []

968+defined (PSyntax _ _) = []

965−defined (PMutual _ ds) = concatMap defined ds

969+defined (PMutual _ ds) = concatMap defined ds

966−defined (PDirective _) = []

970+defined (PDirective _) = []

967−defined _ = []

971+defined _ = []

968

972

969updateN :: [(Name, Name)] -> Name -> Name

973updateN :: [(Name, Name)] -> Name -> Name

970updateN ns n | Just n' <- lookup n ns = n'

974updateN ns n | Just n' <- lookup n ns = n'

@@ -1045,33 +1049,33 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

1045-- general-purpose FCs, and the second transforms those that are used

1049-- general-purpose FCs, and the second transforms those that are used

1046-- for semantic source highlighting, so they can be treated specially.

1050-- for semantic source highlighting, so they can be treated specially.

1047mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm

1051mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm

1048−mapPTermFC f g (PQuote q) = PQuote q

1052+mapPTermFC f g (PQuote q) = PQuote q

1049−mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n

1053+mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n

1050−mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n

1054+mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n

1051−mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n

1055+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)

1056+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)

1057+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)

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)

1055−mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)

1059+mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)

1056−mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

1060+mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

1057−mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls

1061+mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls

1058−mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

1062+mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

1059−mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n

1063+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)

1064+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)

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)

1062−mapPTermFC f g (PTrue fc info) = PTrue (f fc) info

1066+mapPTermFC f g (PTrue fc info) = PTrue (f fc) info

1063−mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)

1067+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)

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)

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)

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)

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)

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)

1067−mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

1071+mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

1068−mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)

1072+mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)

1069−mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

1073+mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

1070−mapPTermFC f g (PType fc) = PType (f fc)

1074+mapPTermFC f g (PType fc) = PType (f fc)

1071−mapPTermFC f g (PUniverse u) = PUniverse u

1075+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)

1076+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

1077+mapPTermFC f g (PConstant fc c) = PConstant (f fc) c

1074−mapPTermFC f g Placeholder = Placeholder

1078+mapPTermFC f g Placeholder = Placeholder

1075mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

1079mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

1076 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)

1080 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)

1077 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)

1081 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)

@@ -1079,22 +1083,22 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

1079 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)

1083 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)

1080 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1084 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1081 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1085 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1082−mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)

1086+mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)

1083−mapPTermFC f g (PReturn fc) = PReturn (f fc)

1087+mapPTermFC f g (PReturn fc) = PReturn (f fc)

1084−mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n

1088+mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n

1085−mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)

1089+mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)

1086−mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)

1090+mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)

1087−mapPTermFC f g (PElabError err) = PElabError err

1091+mapPTermFC f g (PElabError err) = PElabError err

1088−mapPTermFC f g PImpossible = PImpossible

1092+mapPTermFC f g PImpossible = PImpossible

1089−mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)

1093+mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)

1090−mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)

1094+mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)

1091−mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)

1095+mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)

1092−mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)

1096+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)

1097+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)

1098+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

1099+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)

1100+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)

1101+mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)

1098

1102

1099{-!

1103{-!

1100dg instance Binary PTerm

1104dg instance Binary PTerm

@@ -1103,28 +1107,27 @@ deriving instance NFData PTerm

1103

1107

1104mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

1108mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

1105mapPT f t = f (mpt t) where

1109mapPT f t = f (mpt t) where

1106− mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)

1110+ mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)

1107− mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)

1111+ mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)

1108− mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

1112+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

1109− mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)

1113+ mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s) (fmap (mapPT f) g)

1110− (fmap (mapPT f) g)

1111− mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

1114+ mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

1112− mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

1115+ mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

1113− mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

1116+ mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

1114− mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

1117+ mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

1115− mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

1118+ 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)

1119+ mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)

1117 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)

1120 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)

1118− mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)

1121+ mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)

1119− mpt (PHidden t) = PHidden (mapPT f t)

1122+ mpt (PHidden t) = PHidden (mapPT f t)

1120− mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

1123+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

1121− mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

1124+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

1122− mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

1125+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

1123− mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

1126+ mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

1124− mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)

1127+ mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)

1125− mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)

1128+ mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)

1126− mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)

1129+ mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)

1127− mpt x = x

1130+ mpt x = x

1128

1131

1129

1132

1130data PTactic' t = Intro [Name] | Intros | Focus Name

1133data PTactic' t = Intro [Name] | Intros | Focus Name

@@ -1165,39 +1168,39 @@ deriving instance Binary PTactic'

1165deriving instance NFData PTactic'

1168deriving instance NFData PTactic'

1166!-}

1169!-}

1167instance Sized a => Sized (PTactic' a) where

1170instance Sized a => Sized (PTactic' a) where

1168− size (Intro nms) = 1 + size nms

1171+ size (Intro nms) = 1 + size nms

1169− size Intros = 1

1172+ size Intros = 1

1170− size (Focus nm) = 1 + size nm

1173+ size (Focus nm) = 1 + size nm

1171− size (Refine nm bs) = 1 + size nm + length bs

1174+ size (Refine nm bs) = 1 + size nm + length bs

1172− size (Rewrite t) = 1 + size t

1175+ size (Rewrite t) = 1 + size t

1173− size (Induction t) = 1 + size t

1176+ size (Induction t) = 1 + size t

1174− size (LetTac nm t) = 1 + size nm + size t

1177+ size (LetTac nm t) = 1 + size nm + size t

1175− size (Exact t) = 1 + size t

1178+ size (Exact t) = 1 + size t

1176− size Compute = 1

1179+ size Compute = 1

1177− size Trivial = 1

1180+ size Trivial = 1

1178− size Solve = 1

1181+ size Solve = 1

1179− size Attack = 1

1182+ size Attack = 1

1180− size ProofState = 1

1183+ size ProofState = 1

1181− size ProofTerm = 1

1184+ size ProofTerm = 1

1182− size Undo = 1

1185+ size Undo = 1

1183− size (Try l r) = 1 + size l + size r

1186+ size (Try l r) = 1 + size l + size r

1184− size (TSeq l r) = 1 + size l + size r

1187+ size (TSeq l r) = 1 + size l + size r

1185− size (ApplyTactic t) = 1 + size t

1188+ size (ApplyTactic t) = 1 + size t

1186− size (Reflect t) = 1 + size t

1189+ size (Reflect t) = 1 + size t

1187− size (Fill t) = 1 + size t

1190+ size (Fill t) = 1 + size t

1188− size Qed = 1

1191+ size Qed = 1

1189− size Abandon = 1

1192+ size Abandon = 1

1190− size Skip = 1

1193+ size Skip = 1

1191− size (TFail ts) = 1 + size ts

1194+ size (TFail ts) = 1 + size ts

1192− size SourceFC = 1

1195+ size SourceFC = 1

1193− size DoUnify = 1

1196+ size DoUnify = 1

1194− size (CaseTac x) = 1 + size x

1197+ size (CaseTac x) = 1 + size x

1195− size (Equiv t) = 1 + size t

1198+ size (Equiv t) = 1 + size t

1196− size (Claim x y) = 1 + size x + size y

1199+ size (Claim x y) = 1 + size x + size y

1197− size Unfocus = 1

1200+ size Unfocus = 1

1198− size (MatchRefine x) = 1 + size x

1201+ size (MatchRefine x) = 1 + size x

1199 size (LetTacTy x y z) = 1 + size x + size y + size z

1202 size (LetTacTy x y z) = 1 + size x + size y + size z

1200− size TCInstance = 1

1203+ size TCInstance = 1

1201

1204

1202type PTactic = PTactic' PTerm

1205type PTactic = PTactic' PTerm

1203

1206

@@ -1213,11 +1216,11 @@ deriving instance NFData PDo'

1213!-}

1216!-}

1214

1217

1215instance Sized a => Sized (PDo' a) where

1218instance Sized a => Sized (PDo' a) where

1216− size (DoExp fc t) = 1 + size fc + size t

1219+ 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

1220+ 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

1221+ 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

1222+ 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

1223+ size (DoLetP fc l r) = 1 + size fc + size l + size r

1221

1224

1222type PDo = PDo' PTerm

1225type PDo = PDo' PTerm

1223

1226

@@ -1249,10 +1252,10 @@ data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp

1249 deriving (Show, Eq, Data, Typeable)

1252 deriving (Show, Eq, Data, Typeable)

1250

1253

1251instance Sized a => Sized (PArg' a) where

1254instance Sized a => Sized (PArg' a) where

1252− size (PImp p _ l nm trm) = 1 + size nm + size trm

1255+ size (PImp p _ l nm trm) = 1 + size nm + size trm

1253− size (PExp p l nm trm) = 1 + size nm + size trm

1256+ 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

1257+ 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

1258+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

1256

1259

1257{-!

1260{-!

1258deriving instance Binary PArg'

1261deriving instance Binary PArg'

@@ -1260,43 +1263,43 @@ deriving instance NFData PArg'

1260!-}

1263!-}

1261

1264

1262pimp n t mach = PImp 1 mach [] n t

1265pimp n t mach = PImp 1 mach [] n t

1263−pexp t = PExp 1 [] (sMN 0 "arg") t

1266+pexp t = PExp 1 [] (sMN 0 "arg") t

1264−pconst t = PConstraint 1 [] (sMN 0 "carg") t

1267+pconst t = PConstraint 1 [] (sMN 0 "carg") t

1265ptacimp n s t = PTacImplicit 2 [] n s t

1268ptacimp n s t = PTacImplicit 2 [] n s t

1266

1269

1267type PArg = PArg' PTerm

1270type PArg = PArg' PTerm

1268

1271

1269-- | Get the highest FC in a term, if one exists

1272-- | Get the highest FC in a term, if one exists

1270highestFC :: PTerm -> Maybe FC

1273highestFC :: PTerm -> Maybe FC

1271−highestFC (PQuote _) = Nothing

1274+highestFC (PQuote _) = Nothing

1272−highestFC (PRef fc _ _) = Just fc

1275+highestFC (PRef fc _ _) = Just fc

1273−highestFC (PInferRef fc _ _) = Just fc

1276+highestFC (PInferRef fc _ _) = Just fc

1274−highestFC (PPatvar fc _) = Just fc

1277+highestFC (PPatvar fc _) = Just fc

1275−highestFC (PLam fc _ _ _ _) = Just fc

1278+highestFC (PLam fc _ _ _ _) = Just fc

1276−highestFC (PPi _ _ _ _ _) = Nothing

1279+highestFC (PPi _ _ _ _ _) = Nothing

1277−highestFC (PLet fc _ _ _ _ _) = Just fc

1280+highestFC (PLet fc _ _ _ _ _) = Just fc

1278−highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty

1281+highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty

1279−highestFC (PApp fc _ _) = Just fc

1282+highestFC (PApp fc _ _) = Just fc

1280−highestFC (PAppBind fc _ _) = Just fc

1283+highestFC (PAppBind fc _ _) = Just fc

1281−highestFC (PMatchApp fc _) = Just fc

1284+highestFC (PMatchApp fc _) = Just fc

1282−highestFC (PCase fc _ _) = Just fc

1285+highestFC (PCase fc _ _) = Just fc

1283−highestFC (PIfThenElse fc _ _ _) = Just fc

1286+highestFC (PIfThenElse fc _ _ _) = Just fc

1284−highestFC (PTrue fc _) = Just fc

1287+highestFC (PTrue fc _) = Just fc

1285−highestFC (PResolveTC fc) = Just fc

1288+highestFC (PResolveTC fc) = Just fc

1286−highestFC (PRewrite fc _ _ _) = Just fc

1289+highestFC (PRewrite fc _ _ _) = Just fc

1287−highestFC (PPair fc _ _ _ _) = Just fc

1290+highestFC (PPair fc _ _ _ _) = Just fc

1288−highestFC (PDPair fc _ _ _ _ _) = Just fc

1291+highestFC (PDPair fc _ _ _ _ _) = Just fc

1289−highestFC (PAs fc _ _) = Just fc

1292+highestFC (PAs fc _ _) = Just fc

1290highestFC (PAlternative _ _ args) =

1293highestFC (PAlternative _ _ args) =

1291 case mapMaybe highestFC args of

1294 case mapMaybe highestFC args of

1292 [] -> Nothing

1295 [] -> Nothing

1293 (fc:_) -> Just fc

1296 (fc:_) -> Just fc

1294−highestFC (PHidden _) = Nothing

1297+highestFC (PHidden _) = Nothing

1295−highestFC (PType fc) = Just fc

1298+highestFC (PType fc) = Just fc

1296−highestFC (PUniverse _) = Nothing

1299+highestFC (PUniverse _) = Nothing

1297−highestFC (PGoal fc _ _ _) = Just fc

1300+highestFC (PGoal fc _ _ _) = Just fc

1298−highestFC (PConstant fc _) = Just fc

1301+highestFC (PConstant fc _) = Just fc

1299−highestFC Placeholder = Nothing

1302+highestFC Placeholder = Nothing

1300highestFC (PDoBlock lines) =

1303highestFC (PDoBlock lines) =

1301 case map getDoFC lines of

1304 case map getDoFC lines of

1302 [] -> Nothing

1305 [] -> Nothing

@@ -1308,23 +1311,23 @@ highestFC (PDoBlock lines) =

1308 getDoFC (DoLet fc nm nfc l r) = fc

1311 getDoFC (DoLet fc nm nfc l r) = fc

1309 getDoFC (DoLetP fc l r) = fc

1312 getDoFC (DoLetP fc l r) = fc

1310

1313

1311−highestFC (PIdiom fc _) = Just fc

1314+highestFC (PIdiom fc _) = Just fc

1312−highestFC (PReturn fc) = Just fc

1315+highestFC (PReturn fc) = Just fc

1313−highestFC (PMetavar fc _) = Just fc

1316+highestFC (PMetavar fc _) = Just fc

1314−highestFC (PProof _) = Nothing

1317+highestFC (PProof _) = Nothing

1315−highestFC (PTactics _) = Nothing

1318+highestFC (PTactics _) = Nothing

1316−highestFC (PElabError _) = Nothing

1319+highestFC (PElabError _) = Nothing

1317−highestFC PImpossible = Nothing

1320+highestFC PImpossible = Nothing

1318−highestFC (PCoerced tm) = highestFC tm

1321+highestFC (PCoerced tm) = highestFC tm

1319−highestFC (PDisamb _ opts) = highestFC opts

1322+highestFC (PDisamb _ opts) = highestFC opts

1320−highestFC (PUnifyLog tm) = highestFC tm

1323+highestFC (PUnifyLog tm) = highestFC tm

1321−highestFC (PNoImplicits tm) = highestFC tm

1324+highestFC (PNoImplicits tm) = highestFC tm

1322−highestFC (PQuasiquote _ _) = Nothing

1325+highestFC (PQuasiquote _ _) = Nothing

1323−highestFC (PUnquote tm) = highestFC tm

1326+highestFC (PUnquote tm) = highestFC tm

1324−highestFC (PQuoteName _ _ fc) = Just fc

1327+highestFC (PQuoteName _ _ fc) = Just fc

1325−highestFC (PRunElab fc _ _) = Just fc

1328+highestFC (PRunElab fc _ _) = Just fc

1326−highestFC (PConstSugar fc _) = Just fc

1329+highestFC (PConstSugar fc _) = Just fc

1327−highestFC (PAppImpl t _) = highestFC t

1330+highestFC (PAppImpl t _) = highestFC t

1328

1331

1329-- Type class data

1332-- Type class data

1330

1333

@@ -1402,11 +1405,11 @@ data Syntax = Rule [SSymbol] PTerm SynContext

1402

1405

1403syntaxNames :: Syntax -> [Name]

1406syntaxNames :: Syntax -> [Name]

1404syntaxNames (Rule syms _ _) = mapMaybe ename syms

1407syntaxNames (Rule syms _ _) = mapMaybe ename syms

1405− where ename (Keyword n) = Just n

1408+ where ename (Keyword n) = Just n

1406− ename _ = Nothing

1409+ ename _ = Nothing

1407syntaxNames (DeclRule syms _) = mapMaybe ename syms

1410syntaxNames (DeclRule syms _) = mapMaybe ename syms

1408− where ename (Keyword n) = Just n

1411+ where ename (Keyword n) = Just n

1409− ename _ = Nothing

1412+ ename _ = Nothing

1410

1413

1411syntaxSymbols :: Syntax -> [SSymbol]

1414syntaxSymbols :: Syntax -> [SSymbol]

1412syntaxSymbols (Rule ss _ _) = ss

1415syntaxSymbols (Rule ss _ _) = ss

@@ -1439,9 +1442,9 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

1439 where

1442 where

1440 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)

1443 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)

1441

1444

1442− ruleSort [] [] = EQ

1445+ ruleSort [] [] = EQ

1443− ruleSort [] _ = LT

1446+ ruleSort [] _ = LT

1444− ruleSort _ [] = GT

1447+ ruleSort _ [] = GT

1445 ruleSort (s1:ss1) (s2:ss2) =

1448 ruleSort (s1:ss1) (s2:ss2) =

1446 case symCompare s1 s2 of

1449 case symCompare s1 s2 of

1447 EQ -> ruleSort ss1 ss2

1450 EQ -> ruleSort ss1 ss2

@@ -1449,25 +1452,25 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

1449

1452

1450 -- Better than creating Ord instance for SSymbol since

1453 -- Better than creating Ord instance for SSymbol since

1451 -- in general this ordering does not really make sense.

1454 -- in general this ordering does not really make sense.

1452− symCompare (Keyword n1) (Keyword n2) = compare n1 n2

1455+ symCompare (Keyword n1) (Keyword n2) = compare n1 n2

1453− symCompare (Keyword _) _ = LT

1456+ symCompare (Keyword _) _ = LT

1454− symCompare (Symbol _) (Keyword _) = GT

1457+ symCompare (Symbol _) (Keyword _) = GT

1455− symCompare (Symbol s1) (Symbol s2) = compare s1 s2

1458+ symCompare (Symbol s1) (Symbol s2) = compare s1 s2

1456− symCompare (Symbol _) _ = LT

1459+ symCompare (Symbol _) _ = LT

1457− symCompare (Binding _) (Keyword _) = GT

1460+ symCompare (Binding _) (Keyword _) = GT

1458− symCompare (Binding _) (Symbol _) = GT

1461+ symCompare (Binding _) (Symbol _) = GT

1459− symCompare (Binding b1) (Binding b2) = compare b1 b2

1462+ symCompare (Binding b1) (Binding b2) = compare b1 b2

1460− symCompare (Binding _) _ = LT

1463+ symCompare (Binding _) _ = LT

1461− symCompare (Expr _) (Keyword _) = GT

1464+ symCompare (Expr _) (Keyword _) = GT

1462− symCompare (Expr _) (Symbol _) = GT

1465+ symCompare (Expr _) (Symbol _) = GT

1463− symCompare (Expr _) (Binding _) = GT

1466+ symCompare (Expr _) (Binding _) = GT

1464− symCompare (Expr e1) (Expr e2) = compare e1 e2

1467+ symCompare (Expr e1) (Expr e2) = compare e1 e2

1465− symCompare (Expr _) _ = LT

1468+ symCompare (Expr _) _ = LT

1466− symCompare (SimpleExpr _) (Keyword _) = GT

1469+ symCompare (SimpleExpr _) (Keyword _) = GT

1467− symCompare (SimpleExpr _) (Symbol _) = GT

1470+ symCompare (SimpleExpr _) (Symbol _) = GT

1468− symCompare (SimpleExpr _) (Binding _) = GT

1471+ symCompare (SimpleExpr _) (Binding _) = GT

1469− symCompare (SimpleExpr _) (Expr _) = GT

1472+ symCompare (SimpleExpr _) (Expr _) = GT

1470− symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2

1473+ symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2

1471

1474

1472initDSL = DSL (PRef f [] (sUN ">>="))

1475initDSL = DSL (PRef f [] (sUN ">>="))

1473 (PRef f [] (sUN "return"))

1476 (PRef f [] (sUN "return"))

@@ -1539,10 +1542,10 @@ getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

1539getInferTerm (App _ (App _ _ _) tm) = tm

1542getInferTerm (App _ (App _ _ _) tm) = tm

1540getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1543getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1541

1544

1542−getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1545+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1543− where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

1546+ where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

1544− toTy (PVar t) = PVTy t

1547+ toTy (PVar t) = PVTy t

1545− toTy b = b

1548+ toTy b = b

1546getInferType (App _ (App _ _ ty) _) = ty

1549getInferType (App _ (App _ _ ty) _) = ty

1547

1550

1548

1551

@@ -1564,12 +1567,12 @@ falseTy = sUN "Void"

1564pairTy = sNS (sUN "Pair") ["Builtins"]

1567pairTy = sNS (sUN "Pair") ["Builtins"]

1565pairCon = sNS (sUN "MkPair") ["Builtins"]

1568pairCon = sNS (sUN "MkPair") ["Builtins"]

1566

1569

1567−upairTy = sNS (sUN "UPair") ["Builtins"]

1570+upairTy = sNS (sUN "UPair") ["Builtins"]

1568−upairCon = sNS (sUN "MkUPair") ["Builtins"]

1571+upairCon = sNS (sUN "MkUPair") ["Builtins"]

1569

1572

1570−eqTy = sUN "="

1573+eqTy = sUN "="

1571eqCon = sUN "Refl"

1574eqCon = sUN "Refl"

1572−eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

1575+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

1573 "The propositional equality type. A proof that `x` = `y`." ++

1576 "The propositional equality type. A proof that `x` = `y`." ++

1574 "\n\n" ++

1577 "\n\n" ++

1575 "To use such a proof, pattern-match on it, and the two equal things will " ++

1578 "To use such a proof, pattern-match on it, and the two equal things will " ++

@@ -1612,7 +1615,7 @@ modDocName :: Name

1612modDocName = sMN 0 "ModuleDocs"

1615modDocName = sMN 0 "ModuleDocs"

1613

1616

1614-- Defined in builtins.idr

1617-- Defined in builtins.idr

1615−sigmaTy = sNS (sUN "Sigma") ["Builtins"]

1618+sigmaTy = sNS (sUN "Sigma") ["Builtins"]

1616sigmaCon = sNS (sUN "MkSigma") ["Builtins"]

1619sigmaCon = sNS (sUN "MkSigma") ["Builtins"]

1617

1620

1618piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm

@@ -1653,11 +1656,11 @@ annotationColour ist (AnnConst c) =

1653 in Just $ if constIsType c

1656 in Just $ if constIsType c

1654 then typeColour theme

1657 then typeColour theme

1655 else dataColour theme

1658 else dataColour theme

1656−annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)

1659+annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)

1657−annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)

1660+annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)

1658−annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)

1661+annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)

1659annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)

1662annotationColour 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)

1661annotationColour ist (AnnName n _ _ _) =

1664annotationColour ist (AnnName n _ _ _) =

1662 let ctxt = tt_ctxt ist

1665 let ctxt = tt_ctxt ist

1663 theme = idris_colourTheme ist

1666 theme = idris_colourTheme ist

@@ -1759,7 +1762,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1759 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1762 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1760 depth d . bracket p startPrec $

1763 depth d . bracket p startPrec $

1761 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1764 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1762− prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =

1765+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =

1763 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1766 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1764 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1767 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1765 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

1768 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

1796 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))

1799 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))

1797 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1800 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1798 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)

1801 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)

1799− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1802+ (l@(PExp{}) : r@(PExp{}) : rest) ->

1800 depth d . bracket p funcAppPrec $

1803 depth d . bracket p funcAppPrec $

1801 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1804 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1802 align (group (vsep (map (prettyArgS d bnd) rest)))

1805 align (group (vsep (map (prettyArgS d bnd) rest)))

@@ -1847,20 +1850,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1847 -- disambiguation on PDPair.

1850 -- disambiguation on PDPair.

1848 vars tm = filter noNS (allNamesIn tm)

1851 vars tm = filter noNS (allNamesIn tm)

1849 noNS (NS _ _) = False

1852 noNS (NS _ _) = False

1850− noNS _ = True

1853+ noNS _ = True

1851

1854

1852 prettySe d p bnd (PIfThenElse _ c t f) =

1855 prettySe d p bnd (PIfThenElse _ c t f) =

1853 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $

1856 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

1855 , kwd "then" <+> prettySe (decD d) startPrec bnd t

1858 , kwd "then" <+> prettySe (decD d) startPrec bnd t

1856 , kwd "else" <+> prettySe (decD d) startPrec bnd f

1859 , kwd "else" <+> prettySe (decD d) startPrec bnd f

1857 ]

1860 ]

1858− prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm

1861+ prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm

1859− prettySe d p bnd (PResolveTC _) = kwd "%instance"

1862+ prettySe d p bnd (PResolveTC _) = kwd "%instance"

1860− prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1863+ prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1861− prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1864+ prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1862 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

1865 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

1863− prettySe d p bnd (PRewrite _ l r _) =

1866+ prettySe d p bnd (PRewrite _ l r _) =

1864 depth d . bracket p startPrec $

1867 depth d . bracket p startPrec $

1865 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r

1868 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r

1866 prettySe d p bnd (PTyped l r) =

1869 prettySe d p bnd (PTyped l r) =

@@ -1870,9 +1873,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1870 align . group . vsep . punctuate (ann comma) $

1873 align . group . vsep . punctuate (ann comma) $

1871 map (prettySe (decD d) startPrec bnd) elts

1874 map (prettySe (decD d) startPrec bnd) elts

1872 where ann = case pun of

1875 where ann = case pun of

1873− TypeOrTerm -> id

1876+ TypeOrTerm -> id

1874− IsType -> annName pairTy

1877+ IsType -> annName pairTy

1875− IsTerm -> annName pairCon

1878+ IsTerm -> annName pairCon

1876 prettySe d p bnd (PDPair _ _ pun l t r) =

1879 prettySe d p bnd (PDPair _ _ pun l t r) =

1877 depth d $

1880 depth d $

1878 annotated lparen <>

1881 annotated lparen <>

@@ -1881,30 +1884,32 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1881 prettySe (decD d) startPrec (addBinding bnd) r <>

1884 prettySe (decD d) startPrec (addBinding bnd) r <>

1882 annotated rparen

1885 annotated rparen

1883 where annotated = case pun of

1886 where annotated = case pun of

1884− IsType -> annName sigmaTy

1887+ IsType -> annName sigmaTy

1885− IsTerm -> annName sigmaCon

1888+ IsTerm -> annName sigmaCon

1886− TypeOrTerm -> id

1889+ TypeOrTerm -> id

1887 (left, addBinding) = case (l, pun) of

1890 (left, addBinding) = case (l, pun) of

1888 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1891 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1889− _ -> (prettySe (decD d) startPrec bnd l, id)

1892+ _ -> (prettySe (decD d) startPrec bnd l, id)

1890 prettySe d p bnd (PAlternative ns a as) =

1893 prettySe d p bnd (PAlternative ns a as) =

1891 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1894 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1892 where

1895 where

1893 prettyAs =

1896 prettyAs =

1897+ foldr ((\ l r -> l <+> text "," <+> r) .

1894− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as

1898+ depth d . prettySe (decD d) startPrec bnd)

1899+ empty as

1895− prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"

1900+ prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"

1896− prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1901+ prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1897− prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))

1902+ prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))

1898 -- XXX: add pretty for tactics

1903 -- XXX: add pretty for tactics

1899− prettySe d p bnd (PProof ts) =

1904+ prettySe d p bnd (PProof ts) =

1900 kwd "proof" <+> lbrace <> ellipsis <> rbrace

1905 kwd "proof" <+> lbrace <> ellipsis <> rbrace

1901− prettySe d p bnd (PTactics ts) =

1906+ prettySe d p bnd (PTactics ts) =

1902 kwd "tactics" <+> lbrace <> ellipsis <> rbrace

1907 kwd "tactics" <+> lbrace <> ellipsis <> rbrace

1903− prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n

1908+ prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n

1904− prettySe d p bnd (PReturn f) = kwd "return"

1909+ prettySe d p bnd (PReturn f) = kwd "return"

1905− prettySe d p bnd PImpossible = kwd "impossible"

1910+ prettySe d p bnd PImpossible = kwd "impossible"

1906− prettySe d p bnd Placeholder = text "_"

1911+ prettySe d p bnd Placeholder = text "_"

1907− prettySe d p bnd (PDoBlock dos) =

1912+ prettySe d p bnd (PDoBlock dos) =

1908 bracket p startPrec $

1913 bracket p startPrec $

1909 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))

1914 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))

1910 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos

1915 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos

@@ -1926,47 +1931,46 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1926 text "no pretty printer for pattern-matching do binding" :

1931 text "no pretty printer for pattern-matching do binding" :

1927 ppdo bnd dos

1932 ppdo bnd dos

1928 ppdo _ [] = []

1933 ppdo _ [] = []

1929− prettySe d p bnd (PCoerced t) = prettySe d p bnd t

1934+ prettySe d p bnd (PCoerced t) = prettySe d p bnd t

1930− prettySe d p bnd (PElabError s) = pretty s

1935+ prettySe d p bnd (PElabError s) = pretty s

1931 -- Quasiquote pprinting ignores bound vars

1936 -- 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 ")"

1933 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"

1938 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"

1934− prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t

1939+ prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t

1935− prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end

1940+ prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end

1936 where start = if res then "`{" else "`{{"

1941 where start = if res then "`{" else "`{{"

1937 end = if res then "}" else "}}"

1942 end = if res then "}" else "}}"

1938− prettySe d p bnd (PRunElab _ tm _) =

1943+ prettySe d p bnd (PRunElab _ tm _) =

1939 bracket p funcAppPrec . group . align . hang 2 $

1944 bracket p funcAppPrec . group . align . hang 2 $

1940 text "%runElab" <$>

1945 text "%runElab" <$>

1941 prettySe (decD d) funcAppPrec bnd tm

1946 prettySe (decD d) funcAppPrec bnd tm

1942− prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless

1947+ prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless

1943−

1944− prettySe d p bnd _ = text "missing pretty-printer for term"

1948+ prettySe d p bnd _ = text "missing pretty-printer for term"

1945

1949

1946 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation

1950 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation

1947 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))

1951 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))

1948 where display (UN n) = T.unpack n

1952 where display (UN n) = T.unpack n

1949 display (MN _ n) = T.unpack n

1953 display (MN _ n) = T.unpack n

1950 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings

1954 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings

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

1952 display n = show n

1956 display n = show n

1953

1957

1954− prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)

1958+ prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)

1955− prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm

1959+ prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm

1956− prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm

1960+ prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm

1957− prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)

1961+ prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)

1958

1962

1959− prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg

1963+ 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

1964+ 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

1965+ prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace

1962 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace

1966 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace

1963

1967

1964 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1968 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1965 annName n = annotate (AnnName n Nothing Nothing Nothing)

1969 annName n = annotate (AnnName n Nothing Nothing Nothing)

1966

1970

1967 opStr :: Name -> String

1971 opStr :: Name -> String

1968− opStr (NS n _) = opStr n

1972+ opStr (NS n _) = opStr n

1969− opStr (UN n) = T.unpack n

1973+ opStr (UN n) = T.unpack n

1970

1974

1971 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]

1975 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]

1972 slist' (Just d) _ _ _ | d <= 0 = Nothing

1976 slist' (Just d) _ _ _ | d <= 0 = Nothing

@@ -2028,7 +2032,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

2028 ellipsis = text "..."

2032 ellipsis = text "..."

2029

2033

2030 depth Nothing = id

2034 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

2032

2036

2033 decD = fmap (\x -> x - 1)

2037 decD = fmap (\x -> x - 1)

2034

2038

@@ -2043,7 +2047,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

2043-- | Strip away namespace information

2047-- | Strip away namespace information

2044basename :: Name -> Name

2048basename :: Name -> Name

2045basename (NS n _) = basename n

2049basename (NS n _) = basename n

2046−basename n = n

2050+basename n = n

2047

2051

2048-- | Determine whether a name was the one inserted for a hole or

2052-- | Determine whether a name was the one inserted for a hole or

2049-- guess by the delaborator

2053-- guess by the delaborator

@@ -2063,15 +2067,15 @@ prettyName

2063 -> Name -- ^^ the name to pprint

2067 -> Name -- ^^ the name to pprint

2064 -> Doc OutputAnnotation

2068 -> Doc OutputAnnotation

2065prettyName infixParen showNS bnd n

2069prettyName infixParen showNS bnd n

2066− | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

2070+ | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

2067− | (UN n') <- n, T.unpack n' == "_" = text "_"

2071+ | (UN n') <- n, T.unpack n' == "_" = text "_"

2068− | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName

2072+ | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName

2069− | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

2073+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

2070 where fullName = text nameSpace <> parenthesise (text (baseName n))

2074 where fullName = text nameSpace <> parenthesise (text (baseName n))

2071− baseName (UN n) = T.unpack n

2075+ baseName (UN n) = T.unpack n

2072− baseName (NS n ns) = baseName n

2076+ baseName (NS n ns) = baseName n

2073− baseName (MN i s) = T.unpack s

2077+ baseName (MN i s) = T.unpack s

2074− baseName other = show other

2078+ baseName other = show other

2075 nameSpace = case n of

2079 nameSpace = case n of

2076 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""

2080 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""

2077 _ -> ""

2081 _ -> ""

@@ -2086,13 +2090,13 @@ showCImp ppo (PClause _ n l ws r w)

2086 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r

2090 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r

2087 <+> text "where" <+> text (show w)

2091 <+> text "where" <+> text (show w)

2088 where

2092 where

2089− showWs [] = empty

2093+ showWs [] = empty

2090 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

2094 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

2091showCImp ppo (PWith _ n l ws r pn w)

2095showCImp ppo (PWith _ n l ws r pn w)

2092 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

2096 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

2093 <+> braces (text (show w))

2097 <+> braces (text (show w))

2094 where

2098 where

2095− showWs [] = empty

2099+ showWs [] = empty

2096 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

2100 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

2097

2101

2098

2102

@@ -2104,13 +2108,13 @@ showDImp ppo (PDatadecl n nfc ty cons)

2104showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

2108showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

2105showDecls o ds = vsep (map (showDeclImp o) ds)

2109showDecls o ds = vsep (map (showDeclImp o) ds)

2106

2110

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))

2108showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

2112showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

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" <+>

2110 indent 2 (vsep (map (showCImp o) cs))

2114 indent 2 (vsep (map (showCImp o) cs))

2111−showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

2115+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)

2116+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)

2117+showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

2114showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

2118showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

2115showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

2119showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

2116 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

2120 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

@@ -2121,26 +2125,26 @@ showDeclImp _ _ = text "..."

2121

2125

2122getImps :: [PArg] -> [(Name, PTerm)]

2126getImps :: [PArg] -> [(Name, PTerm)]

2123getImps [] = []

2127getImps [] = []

2124−getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

2128+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

2125−getImps (_ : xs) = getImps xs

2129+getImps (_ : xs) = getImps xs

2126

2130

2127getExps :: [PArg] -> [PTerm]

2131getExps :: [PArg] -> [PTerm]

2128getExps [] = []

2132getExps [] = []

2129−getExps (PExp _ _ _ tm : xs) = tm : getExps xs

2133+getExps (PExp _ _ _ tm : xs) = tm : getExps xs

2130−getExps (_ : xs) = getExps xs

2134+getExps (_ : xs) = getExps xs

2131

2135

2132getShowArgs :: [PArg] -> [PArg]

2136getShowArgs :: [PArg] -> [PArg]

2133getShowArgs [] = []

2137getShowArgs [] = []

2134getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs

2138getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs

2135getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs

2139getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs

2136 | PImp _ _ _ _ tm <- e

2140 | PImp _ _ _ _ tm <- e

2137− , containsHole tm = e : getShowArgs xs

2141+ , containsHole tm = e : getShowArgs xs

2138getShowArgs (_ : xs) = getShowArgs xs

2142getShowArgs (_ : xs) = getShowArgs xs

2139

2143

2140getConsts :: [PArg] -> [PTerm]

2144getConsts :: [PArg] -> [PTerm]

2141−getConsts [] = []

2145+getConsts [] = []

2142getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs

2146getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs

2143−getConsts (_ : xs) = getConsts xs

2147+getConsts (_ : xs) = getConsts xs

2144

2148

2145getAll :: [PArg] -> [PTerm]

2149getAll :: [PArg] -> [PTerm]

2146getAll = map getTm

2150getAll = map getTm

@@ -2154,13 +2158,13 @@ showName :: Maybe IState -- ^^ the Idris state, for information about names an

2154 -> Name -- ^^ the term to show

2158 -> Name -- ^^ the term to show

2155 -> String

2159 -> String

2156showName ist bnd ppo colour n = case ist of

2160showName ist bnd ppo colour n = case ist of

2157− Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

2161+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

2158− Nothing -> showbasic n

2162+ Nothing -> showbasic n

2159 where name = if ppopt_impl ppo then show n else showbasic n

2163 where name = if ppopt_impl ppo then show n else showbasic n

2160− showbasic n@(UN _) = showCG n

2164+ showbasic n@(UN _) = showCG n

2161− showbasic (MN i s) = str s

2165+ showbasic (MN i s) = str s

2162− showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

2166+ showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

2163− showbasic (SN s) = show s

2167+ showbasic (SN s) = show s

2164 fst3 (x, _, _) = x

2168 fst3 (x, _, _) = x

2165 colourise n t = let ctxt' = fmap tt_ctxt ist in

2169 colourise n t = let ctxt' = fmap tt_ctxt ist in

2166 case ctxt' of

2170 case ctxt' of

@@ -2192,42 +2196,42 @@ showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""

2192

2196

2193

2197

2194instance Sized PTerm where

2198instance Sized PTerm where

2195− size (PQuote rawTerm) = size rawTerm

2199+ size (PQuote rawTerm) = size rawTerm

2196− size (PRef fc _ name) = size name

2200+ size (PRef fc _ name) = size name

2197− size (PLam fc name _ ty bdy) = 1 + size ty + size bdy

2201+ 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

2202+ 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

2203+ 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

2204+ size (PTyped trm ty) = 1 + size trm + size ty

2201− size (PApp fc name args) = 1 + size args

2205+ size (PApp fc name args) = 1 + size args

2202− size (PAppBind fc name args) = 1 + size args

2206+ size (PAppBind fc name args) = 1 + size args

2203− size (PCase fc trm bdy) = 1 + size trm + size bdy

2207+ size (PCase fc trm bdy) = 1 + size trm + size bdy

2204− size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

2208+ size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

2205− size (PTrue fc _) = 1

2209+ size (PTrue fc _) = 1

2206− size (PResolveTC fc) = 1

2210+ size (PResolveTC fc) = 1

2207− size (PRewrite fc left right _) = 1 + size left + size right

2211+ size (PRewrite fc left right _) = 1 + size left + size right

2208− size (PPair fc _ _ left right) = 1 + size left + size right

2212+ size (PPair fc _ _ left right) = 1 + size left + size right

2209− size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right

2213+ size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right

2210− size (PAlternative _ a alts) = 1 + size alts

2214+ size (PAlternative _ a alts) = 1 + size alts

2211− size (PHidden hidden) = size hidden

2215+ size (PHidden hidden) = size hidden

2212− size (PUnifyLog tm) = size tm

2216+ size (PUnifyLog tm) = size tm

2213− size (PDisamb _ tm) = size tm

2217+ size (PDisamb _ tm) = size tm

2214− size (PNoImplicits tm) = size tm

2218+ size (PNoImplicits tm) = size tm

2215− size (PType _) = 1

2219+ size (PType _) = 1

2216− size (PUniverse _) = 1

2220+ size (PUniverse _) = 1

2217− size (PConstant fc const) = 1 + size fc + size const

2221+ size (PConstant fc const) = 1 + size fc + size const

2218− size Placeholder = 1

2222+ size Placeholder = 1

2219− size (PDoBlock dos) = 1 + size dos

2223+ size (PDoBlock dos) = 1 + size dos

2220− size (PIdiom fc term) = 1 + size term

2224+ size (PIdiom fc term) = 1 + size term

2221− size (PReturn fc) = 1

2225+ size (PReturn fc) = 1

2222− size (PMetavar _ name) = 1

2226+ size (PMetavar _ name) = 1

2223− size (PProof tactics) = size tactics

2227+ size (PProof tactics) = size tactics

2224− size (PElabError err) = size err

2228+ size (PElabError err) = size err

2225− size PImpossible = 1

2229+ size PImpossible = 1

2226− size _ = 0

2230+ size _ = 0

2227

2231

2228getPArity :: PTerm -> Int

2232getPArity :: PTerm -> Int

2229−getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc

2233+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc

2230−getPArity _ = 0

2234+getPArity _ = 0

2231

2235

2232-- Return all names, free or globally bound, in the given term.

2236-- Return all names, free or globally bound, in the given term.

2233

2237

@@ -2235,31 +2239,30 @@ allNamesIn :: PTerm -> [Name]

2235allNamesIn tm = nub $ ni 0 [] tm

2239allNamesIn tm = nub $ ni 0 [] tm

2236 where -- TODO THINK added niTacImp, but is it right?

2240 where -- TODO THINK added niTacImp, but is it right?

2237 ni 0 env (PRef _ _ n)

2241 ni 0 env (PRef _ _ n)

2238− | not (n `elem` env) = [n]

2242+ | not (n `elem` env) = [n]

2239− ni 0 env (PPatvar _ n) = [n]

2243+ ni 0 env (PPatvar _ n) = [n]

2240− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2244+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2241− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2245+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2242− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)

2246+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os

2243− ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f

2247+ ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f

2244− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2248+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2245− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2249+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2246− ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

2250+ ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

2247− ni 0 env (PHidden tm) = ni 0 env tm

2251+ ni 0 env (PHidden tm) = ni 0 env tm

2248− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2252+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2249− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2253+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2250− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2254+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2251− ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r

2255+ ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r

2252− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2256+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2253− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2257+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2254− ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls

2258+ ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls

2255− ni 0 env (PUnifyLog tm) = ni 0 env tm

2259+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2256− ni 0 env (PDisamb _ tm) = ni 0 env tm

2260+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2257− ni 0 env (PNoImplicits tm) = ni 0 env tm

2261+ 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

2261

2262

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

2262− ni i env tm = concatMap (ni i env) (children tm)

2265+ ni i env tm = concatMap (ni i env) (children tm)

2263

2266

2264 niTacImp i env (TacImp _ _ scr) = ni i env scr

2267 niTacImp i env (TacImp _ _ scr) = ni i env scr

2265 niTacImp _ _ _ = []

2268 niTacImp _ _ _ = []

@@ -2270,32 +2273,32 @@ boundNamesIn :: PTerm -> [Name]

2270boundNamesIn tm = S.toList (ni 0 S.empty tm)

2273boundNamesIn tm = S.toList (ni 0 S.empty tm)

2271 where -- TODO THINK Added niTacImp, but is it right?

2274 where -- TODO THINK Added niTacImp, but is it right?

2272 ni :: Int -> S.Set Name -> PTerm -> S.Set Name

2275 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)

2276+ 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)

2277+ 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)

2278+ 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]

2279+ 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

2280+ 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

2281+ 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

2282+ 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

2283+ 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

2284+ 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

2285+ ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r

2283 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r

2286 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r

2284− ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r

2287+ ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r

2285− ni 0 set (PAlternative ns a as) = niTms 0 set as

2288+ ni 0 set (PAlternative ns a as) = niTms 0 set as

2286− ni 0 set (PHidden tm) = ni 0 set tm

2289+ ni 0 set (PHidden tm) = ni 0 set tm

2287− ni 0 set (PUnifyLog tm) = ni 0 set tm

2290+ ni 0 set (PUnifyLog tm) = ni 0 set tm

2288− ni 0 set (PDisamb _ tm) = ni 0 set tm

2291+ ni 0 set (PDisamb _ tm) = ni 0 set tm

2289− ni 0 set (PNoImplicits tm) = ni 0 set tm

2292+ ni 0 set (PNoImplicits tm) = ni 0 set tm

2290

2293

2291− ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty

2294+ ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty

2292− ni i set (PUnquote tm) = ni (i - 1) set tm

2295+ ni i set (PUnquote tm) = ni (i - 1) set tm

2293

2296

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)

2295

2298

2296 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name

2299 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name

2297− niTms i set [] = set

2300+ niTms i set [] = set

2298− niTms i set (x : xs) = niTms i (ni i set x) xs

2301+ niTms i set (x : xs) = niTms i (ni i set x) xs

2299

2302

2300 niTacImp i set (TacImp _ _ scr) = ni i set scr

2303 niTacImp i set (TacImp _ _ scr) = ni i set scr

2301 niTacImp i set _ = set

2304 niTacImp i set _ = set

@@ -2311,18 +2314,18 @@ implicitNamesIn uvars ist tm

2311 addFn n = do (imps, fns) <- get

2314 addFn n = do (imps, fns) <- get

2312 put (imps, n: fns)

2315 put (imps, n: fns)

2313

2316

2314− notCAF [] = False

2317+ notCAF [] = False

2315 notCAF (PExp _ _ _ _ : _) = True

2318 notCAF (PExp _ _ _ _ : _) = True

2316− notCAF (_ : xs) = notCAF xs

2319+ notCAF (_ : xs) = notCAF xs

2317

2320

2318 notHidden (n, _) = case getAccessibility n of

2321 notHidden (n, _) = case getAccessibility n of

2319− Hidden -> False

2322+ Hidden -> False

2320− _ -> True

2323+ _ -> True

2321

2324

2322 getAccessibility n

2325 getAccessibility n

2323 = case lookupDefAccExact n False (tt_ctxt ist) of

2326 = case lookupDefAccExact n False (tt_ctxt ist) of

2324− Just (n,t) -> t

2327+ Just (n,t) -> t

2325− _ -> Public

2328+ _ -> Public

2326

2329

2327 ni 0 env (PRef _ _ n@(NS _ _))

2330 ni 0 env (PRef _ _ n@(NS _ _))

2328 | not (n `elem` env)

2331 | not (n `elem` env)

@@ -2332,44 +2335,44 @@ implicitNamesIn uvars ist tm

2332 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n

2335 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n

2333 ni 0 env (PApp _ f@(PRef _ _ n) as)

2336 ni 0 env (PApp _ f@(PRef _ _ n) as)

2334 | n `elem` uvars = do ni 0 env f

2337 | n `elem` uvars = do ni 0 env f

2335− mapM_ (ni 0 env) (map getTm as)

2338+ mapM_ (ni 0 env . getTm) as

2336 | otherwise = do case lookupTy n (tt_ctxt ist) of

2339 | otherwise = do case lookupTy n (tt_ctxt ist) of

2337− [] -> return ()

2340+ [] -> return ()

2338− _ -> addFn n

2341+ _ -> addFn n

2339− mapM_ (ni 0 env) (map getTm as)

2342+ mapM_ (ni 0 env . getTm) as

2340 ni 0 env (PApp _ f as) = do ni 0 env f

2343 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

2342 ni 0 env (PAppBind _ f as) = do ni 0 env f

2345 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

2344 ni 0 env (PCase _ c os) = do ni 0 env c

2347 ni 0 env (PCase _ c os) = do ni 0 env c

2345 -- names in 'os', not counting the names bound in the cases

2348 -- 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

2347 (imps, fns) <- get

2350 (imps, fns) <- get

2348 put ([] ,[])

2351 put ([] ,[])

2349− mapM_ (ni 0 env) (map fst os)

2352+ mapM_ (ni 0 env . fst) os

2350 (impsfst, _) <- get

2353 (impsfst, _) <- get

2351 put (nub imps \\ nub impsfst, fns)

2354 put (nub imps \\ nub impsfst, fns)

2352− ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

2355+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

2353− ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2356+ ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2354− ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2357+ ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2355− ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r

2358+ ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r

2356− ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2359+ ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2357− ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

2360+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

2358− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

2361+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

2359− ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

2362+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

2360− ni 0 env t

2363+ ni 0 env t

2361− ni 0 env r

2364+ ni 0 env r

2362− ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as

2365+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as

2363− ni 0 env (PHidden tm) = ni 0 env tm

2366+ ni 0 env (PHidden tm) = ni 0 env tm

2364− ni 0 env (PUnifyLog tm) = ni 0 env tm

2367+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2365− ni 0 env (PDisamb _ tm) = ni 0 env tm

2368+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2366− ni 0 env (PNoImplicits tm) = ni 0 env tm

2369+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2367

2370

2368 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm

2371 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm

2369 maybe (return ()) (ni i env) ty

2372 maybe (return ()) (ni i env) ty

2370 ni i env (PUnquote tm) = ni (i - 1) env tm

2373 ni i env (PUnquote tm) = ni (i - 1) env tm

2371

2374

2372− ni i env tm = mapM_ (ni i env) (children tm)

2375+ ni i env tm = mapM_ (ni i env) (children tm)

2373

2376

2374-- Return names which are free in the given term.

2377-- Return names which are free in the given term.

2375namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

2378namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

@@ -2378,32 +2381,32 @@ namesIn uvars ist tm = nub $ ni 0 [] tm

2378 ni 0 env (PRef _ _ n)

2381 ni 0 env (PRef _ _ n)

2379 | not (n `elem` env)

2382 | not (n `elem` env)

2380 = case lookupTy n (tt_ctxt ist) of

2383 = case lookupTy n (tt_ctxt ist) of

2381− [] -> [n]

2384+ [] -> [n]

2382− _ -> if n `elem` (map fst uvars) then [n] else []

2385+ _ -> [n | n `elem` (map fst uvars)]

2383− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2386+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2384− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2387+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2385− ni 0 env (PCase _ c os) = ni 0 env c ++

2388+ ni 0 env (PCase _ c os) = ni 0 env c ++

2386 -- names in 'os', not counting the names bound in the cases

2389 -- names in 'os', not counting the names bound in the cases

2387− (nub (concatMap (ni 0 env) (map snd os))

2390+ (nub (concatMap (ni 0 env . snd) os)

2388− \\ nub (concatMap (ni 0 env) (map fst os)))

2391+ \\ nub (concatMap (ni 0 env . fst) os))

2389− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2392+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2390 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2393 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2391− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2394+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2392− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2395+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2393− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2396+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2394− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2397+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2395 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2398 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

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

2397 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2400 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2398− ni 0 env (PHidden tm) = ni 0 env tm

2401+ ni 0 env (PHidden tm) = ni 0 env tm

2399− ni 0 env (PUnifyLog tm) = ni 0 env tm

2402+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2400− ni 0 env (PDisamb _ tm) = ni 0 env tm

2403+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2401− ni 0 env (PNoImplicits tm) = ni 0 env tm

2404+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2402

2405

2403− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2406+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2404− ni i env (PUnquote tm) = ni (i - 1) env tm

2407+ ni i env (PUnquote tm) = ni (i - 1) env tm

2405

2408

2406− ni i env tm = concatMap (ni i env) (children tm)

2409+ ni i env tm = concatMap (ni i env) (children tm)

2407

2410

2408 niTacImp i env (TacImp _ _ scr) = ni i env scr

2411 niTacImp i env (TacImp _ _ scr) = ni i env scr

2409 niTacImp _ _ _ = []

2412 niTacImp _ _ _ = []

@@ -2418,27 +2421,27 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm

2418 = case lookupDefExact n (tt_ctxt ist) of

2421 = case lookupDefExact n (tt_ctxt ist) of

2419 Nothing -> [n]

2422 Nothing -> [n]

2420 _ -> []

2423 _ -> []

2421− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2424+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2422− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2425+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2423− ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)

2426+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os

2424− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2427+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2425− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2428+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2426− ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2429+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2427− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2430+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2428− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2431+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2429− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2432+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2430 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2433 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

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

2432 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2435 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2433− ni 0 env (PHidden tm) = ni 0 env tm

2436+ ni 0 env (PHidden tm) = ni 0 env tm

2434− ni 0 env (PUnifyLog tm) = ni 0 env tm

2437+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2435− ni 0 env (PDisamb _ tm) = ni 0 env tm

2438+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2436− ni 0 env (PNoImplicits tm) = ni 0 env tm

2439+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2437

2440

2438− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2441+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2439− ni i env (PUnquote tm) = ni (i - 1) env tm

2442+ ni i env (PUnquote tm) = ni (i - 1) env tm

2440

2443

2441− ni i env tm = concatMap (ni i env) (children tm)

2444+ ni i env tm = concatMap (ni i env) (children tm)

2442

2445

2443 niTacImp i env (TacImp _ _ scr) = ni i env scr

2446 niTacImp i env (TacImp _ _ scr) = ni i env scr

2444 niTacImp _ _ _ = []

2447 niTacImp _ _ _ = []

src/Idris/Colours.hs+6−6

@@ -47,9 +47,9 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True

47mkSGR :: IdrisColour -> [SGR]

48mkSGR (IdrisColour c v u b i) =

49 fg c ++

50− (if u then [SetUnderlining SingleUnderline] else []) ++

50+ [SetUnderlining SingleUnderline | u] ++

51− (if b then [SetConsoleIntensity BoldIntensity] else []) ++

51+ [SetConsoleIntensity BoldIntensity | b] ++

52− (if i then [SetItalicized True] else [])

52+ [SetItalicized True | i]

53 where

54 fg Nothing = []

55 fg (Just c) = [SetColor Foreground (if v then Vivid else Dull) c]

@@ -71,9 +71,9 @@ hEndColourise h _ = hSetSGR h [Reset]

71colouriseWithSTX :: IdrisColour -> String -> String

72colouriseWithSTX (IdrisColour c v u b i) str = setSGRCode sgr ++ "\STX" ++ str ++ setSGRCode [Reset] ++ "\STX"

73 where sgr = fg c ++

74− (if u then [SetUnderlining SingleUnderline] else []) ++

74+ [SetUnderlining SingleUnderline | u] ++

75− (if b then [SetConsoleIntensity BoldIntensity] else []) ++

75+ [SetConsoleIntensity BoldIntensity | b] ++

76− (if i then [SetItalicized True] else [])

76+ [SetItalicized True | i]

77 fg Nothing = []

78 fg (Just c) = [SetColor Foreground (if v then Vivid else Dull) c]