d52e4f3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add source location data to PUniverse

d52e4f3Bartosz Przygoda10 years ago

src/Idris/AbsSyntaxTree.hs+5−5

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

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

1149 | PHidden PTerm -- ^ Irrelevant or hidden pattern

1150 | PType FC -- ^ 'Type' type

1151− | PUniverse Universe -- ^ Some universe

1151+ | PUniverse FC Universe -- ^ Some universe

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

1153 | PConstant FC Const -- ^ Builtin types

1154 | Placeholder -- ^ Underscore

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

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

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

1213mapPTermFC 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

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

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

1217mapPTermFC f g Placeholder = Placeholder

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

1443 (fc:_) -> Just fc

1444highestFC (PHidden _) = Nothing

1445highestFC (PType fc) = Just fc

1446−highestFC (PUniverse _) = Nothing

1446+highestFC (PUniverse _ _) = Nothing

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

1448highestFC (PConstant fc _) = Just fc

1449highestFC Placeholder = Nothing

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

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

2084 empty as

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

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

2088 -- XXX: add pretty for tactics

2089 prettySe d p bnd (PProof ts) =

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

2408 size (PDisamb _ tm) = size tm

2409 size (PNoImplicits tm) = size tm

2410 size (PType _) = 1

2411− size (PUniverse _) = 1

2411+ size (PUniverse _ _) = 1

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

2413 size Placeholder = 1

2414 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

175 de env _ Erased = Placeholder

176 de env _ Impossible = Placeholder

177 de env _ (TType i) = PType un

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

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

179

180 dens x | fullname = x

181 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

155

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

157 -- uniqueness hierarchy

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

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

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

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

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

161 chkUniq _ t = t

162

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

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

369 do apply RType []

370 solve

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

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

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

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

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

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

378-- = 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

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

122warnDisamb ist (PHidden tm) = warnDisamb ist tm

123warnDisamb ist (PType _) = return ()

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

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

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

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

127warnDisamb ist Placeholder = return ()

src/Idris/IBC.hs+6−4

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

49import Debug.Trace

51ibcVersion :: Word16

52−ibcVersion = 145

52+ibcVersion = 146

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

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

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

1850 PDisamb x1 x2 -> do putWord8 37

1851 put x1

1852 put x2

1853− PUniverse x1 -> do putWord8 38

1853+ PUniverse x1 x2 -> do putWord8 38

1854− put x1

1854+ put x1

1855+ put x2

1855 PRunElab x1 x2 x3 -> do putWord8 39

1856 PRunElab x1 x2 x3 -> do putWord8 39

1856 put x1

1857 put x1

1857 put x2

1858 put x2

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

2003 x2 <- get

2004 x2 <- get

2004 return (PDisamb x1 x2)

2005 return (PDisamb x1 x2)

2005 38 -> do x1 <- get

2006 38 -> do x1 <- get

2007+ x2 <- get

2006− return (PUniverse x1)

2008+ return (PUniverse x1 x2)

2007 39 -> do x1 <- get

2009 39 -> do x1 <- get

2008 x2 <- get

2010 x2 <- get

2009 x3 <- get

2011 x3 <- get

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

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

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

414 <|> proofExpr syn

415 <|> tacticsExpr syn

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

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

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

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

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

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

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

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

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

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

422 fc <- getFC

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