d52e4f3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add source location data to PUniverse

This enables highlighting of UniqueType, AnyType. Fixes #2380.

commitd52e4f30584eb5206f904edb113fb03af19248ea authorBartosz Przygoda <bprzygoda@gmail.com> dateMon 8 Aug 2016, 21:39 (10 years ago) parent37fdae0

7 files changed+23−18

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+5−5 src/Idris/Delaborate.hs+1−1 src/Idris/Elab/Class.hs+2−2 src/Idris/Elab/Term.hs+4−1 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+6−4 src/Idris/Parser/Expr.hs+4−4

src/Idris/AbsSyntaxTree.hs+5−5

@@ -1148,7 +1148,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

11481148 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

11491149 | PHidden PTerm -- ^ Irrelevant or hidden pattern

11501150 | PType FC -- ^ 'Type' type

1151− | PUniverse Universe -- ^ Some universe

1151+ | PUniverse FC Universe -- ^ Some universe

11521152 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

11531153 | PConstant FC Const -- ^ Builtin types

11541154 | Placeholder -- ^ Underscore

@@ -1211,7 +1211,7 @@ mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

12111211mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)

12121212mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

12131213mapPTermFC f g (PType fc) = PType (f fc)

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

1214+mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u

12151215mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)

12161216mapPTermFC f g (PConstant fc c) = PConstant (f fc) c

12171217mapPTermFC f g Placeholder = Placeholder

@@ -1443,7 +1443,7 @@ highestFC (PAlternative _ _ args) =

14431443 (fc:_) -> Just fc

14441444highestFC (PHidden _) = Nothing

14451445highestFC (PType fc) = Just fc

1446−highestFC (PUniverse _) = Nothing

1446+highestFC (PUniverse _ _) = Nothing

14471447highestFC (PGoal fc _ _ _) = Just fc

14481448highestFC (PConstant fc _) = Just fc

14491449highestFC Placeholder = Nothing

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

20832083 depth d . prettySe (decD d) startPrec bnd)

20842084 empty as

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

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

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

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

20882088 -- XXX: add pretty for tactics

20892089 prettySe d p bnd (PProof ts) =

@@ -2408,7 +2408,7 @@ instance Sized PTerm where

24082408 size (PDisamb _ tm) = size tm

24092409 size (PNoImplicits tm) = size tm

24102410 size (PType _) = 1

2411− size (PUniverse _) = 1

2411+ size (PUniverse _ _) = 1

24122412 size (PConstant fc const) = 1 + size fc + size const

24132413 size Placeholder = 1

24142414 size (PDoBlock dos) = 1 + size dos

src/Idris/Delaborate.hs+1−1

@@ -175,7 +175,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

175175 de env _ Erased = Placeholder

176176 de env _ Impossible = Placeholder

177177 de env _ (TType i) = PType un

178− de env _ (UType u) = PUniverse u

178+ de env _ (UType u) = PUniverse un u

179179

180180 dens x | fullname = x

181181 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

src/Idris/Elab/Class.hs+2−2

@@ -155,8 +155,8 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

155155

156156 -- To make sure the type constructor of the class is in the appropriate

157157 -- uniqueness hierarchy

158− chkUniq u@(PUniverse _) (PType _) = u

159− chkUniq (PUniverse l) (PUniverse r) = PUniverse (min l r)

158+ chkUniq u@(PUniverse _ _) (PType _) = u

159+ chkUniq (PUniverse _ l) (PUniverse _ r) = PUniverse NoFC (min l r)

160160 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t

161161 chkUniq _ t = t

162162

src/Idris/Elab/Term.hs+4−1

@@ -369,7 +369,10 @@ elab ist info emode opts fn tm

369369 do apply RType []

370370 solve

371371 highlightSource fc' (AnnType "Type" "The type of types")

372− elab' ina fc (PUniverse u) = do apply (RUType u) []; solve

372+ elab' ina fc (PUniverse fc' u) =

373+ do apply (RUType u) []

374+ solve

375+ highlightSource fc' (AnnType (show u) "The type of unique types")

373376-- elab' (_,_,inty) (PConstant c)

374377-- | constType c && pattern && not reflection && not inty

375378-- = lift $ tfail (Msg "Typecase is not allowed")

src/Idris/Error.hs+1−1

@@ -121,7 +121,7 @@ warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> wa

121121warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms

122122warnDisamb ist (PHidden tm) = warnDisamb ist tm

123123warnDisamb ist (PType _) = return ()

124−warnDisamb ist (PUniverse _) = return ()

124+warnDisamb ist (PUniverse _ _) = return ()

125125warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y

126126warnDisamb ist (PConstant _ _) = return ()

127127warnDisamb ist Placeholder = return ()

src/Idris/IBC.hs+6−4

@@ -49,7 +49,7 @@ import Codec.Archive.Zip

4949import Debug.Trace

5050

5151ibcVersion :: Word16

52−ibcVersion = 145

52+ibcVersion = 146

5353

5454-- | When IBC is being loaded - we'll load different things (and omit

5555-- different structures/definitions) depending on which phase we're in.

@@ -1850,8 +1850,9 @@ instance Binary PTerm where

18501850 PDisamb x1 x2 -> do putWord8 37

18511851 put x1

18521852 put x2

1853− PUniverse x1 -> do putWord8 38

1854− put x1

1853+ PUniverse x1 x2 -> do putWord8 38

1854+ put x1

1855+ put x2

18551856 PRunElab x1 x2 x3 -> do putWord8 39

18561857 put x1

18571858 put x2

@@ -2003,7 +2004,8 @@ instance Binary PTerm where

20032004 x2 <- get

20042005 return (PDisamb x1 x2)

20052006 38 -> do x1 <- get

2006− return (PUniverse x1)

2007+ x2 <- get

2008+ return (PUniverse x1 x2)

20072009 39 -> do x1 <- get

20082010 x2 <- get

20092011 x3 <- get

src/Idris/Parser/Expr.hs+4−4

@@ -413,11 +413,11 @@ simpleExpr syn =

413413 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

414414 <|> proofExpr syn

415415 <|> tacticsExpr syn

416− <|> try (do reserved "Type*"; return $ PUniverse AllTypes)

417− <|> do reserved "AnyType"; return $ PUniverse AllTypes

416+ <|> try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)

417+ <|> do fc <- reservedFC "AnyType"; return $ PUniverse fc AllTypes

418418 <|> PType <$> reservedFC "Type"

419− <|> do reserved "UniqueType"; return $ PUniverse UniqueType

420− <|> do reserved "NullType"; return $ PUniverse NullType

419+ <|> do fc <- reservedFC "UniqueType"; return $ PUniverse fc UniqueType

420+ <|> do fc <- reservedFC "NullType"; return $ PUniverse fc NullType

421421 <|> do (c, cfc) <- constant

422422 fc <- getFC

423423 return (modifyConst syn fc (PConstant cfc c))