105c230 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Simplify reflection and Raw

Some constructors of TT will never occur during elaboration, but are instead a part of the optimization process. Thus, they have been removed from reflection, to simplify the interface. Likewise, I discovered that RForce is no longer produced anywhere in Idris, so it was also deleted from both the reflection API and the internals.

commit105c23021726f26aba83c5235a36257ee3566c86 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 6 Oct 2015, 17:03 (11 years ago) parent75e45f9

11 files changed+15−58

compare with master

unifiedsplit

libs/base/Language/Reflection/Utils.idr−7 libs/prelude/Language/Reflection.idr+2−9 libs/pruviloj/Pruviloj/Induction.idr−1 libs/pruviloj/Pruviloj/Renamers.idr−1 src/Idris/Core/Binary.hs+1−5 src/Idris/Core/DeepSeq.hs−1 src/Idris/Core/TT.hs−5 src/Idris/Core/Typecheck.hs−3 src/Idris/DataOpts.hs−1 src/Idris/IBC.hs+1−1 src/Idris/Reflection.hs+11−24

libs/base/Language/Reflection/Utils.idr−7

@@ -223,9 +223,7 @@ instance Show TT where

223223 my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t

224224 my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2

225225 my_show d (TConst c) = showCon d "TConst" $ showArg c

226− my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i

227226 my_show d Erased = "Erased"

228− my_show d Impossible = "Impossible"

229227 my_show d (TType u) = showCon d "TType" $ showArg u

230228

231229instance Eq TT where

@@ -236,9 +234,7 @@ instance Eq TT where

236234 equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'

237235 equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'

238236 equalp (TConst c) (TConst c') = c == c'

239− equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'

240237 equalp Erased Erased = True

241− equalp Impossible Impossible = True

242238 equalp (TType u) (TType u') = u == u'

243239 equalp x y = False

244240

@@ -267,10 +263,8 @@ forget tm = fe [] tm

267263 fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]

268264 fe env (App f a) = [| RApp (fe env f) (fe env a) |]

269265 fe env (TConst c) = Just $ RConstant c

270− fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming

271266 fe env (TType i) = Just RType

272267 fe env Erased = Just $ RConstant Forgot

273− fe env Impossible = Nothing

274268

275269instance Show Raw where

276270 showPrec = my_show

@@ -279,7 +273,6 @@ instance Show Raw where

279273 my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm

280274 my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'

281275 my_show d RType = "RType"

282− my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm

283276 my_show d (RConstant c) = showCon d "RConstant" $ showArg c

284277

285278instance Show SourceLocation where

libs/prelude/Language/Reflection.idr+2−9

@@ -175,14 +175,11 @@ data TT =

175175 App TT TT |

176176 ||| Embed a constant

177177 TConst Const |

178− ||| Argument projection; runtime only

179− Proj TT Int |

180178 ||| Erased terms

181179 Erased |

182− ||| Impossible terms

183− Impossible |

184180 ||| The type of types along (with universe constraints)

185181 TType TTUExp |

182+ ||| Alternative universes for dealing with uniqueness

186183 UType Universe

187184%name TT tm, tm'

188185

@@ -196,8 +193,8 @@ data Raw =

196193 RApp Raw Raw |

197194 ||| The type of types

198195 RType |

196+ ||| Alternative universes for dealing with uniqueness

199197 RUType Universe |

200− RForce Raw |

201198 ||| Embed a constant

202199 RConstant Const

203200%name Raw tm, tm'

@@ -556,9 +553,7 @@ mutual

556553 quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))

557554 quote (App f x) = `(App ~(quote f) ~(quote x))

558555 quote (TConst c) = `(TConst ~(quote c))

559− quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))

560556 quote Erased = `(Erased)

561− quote Impossible = `(Impossible)

562557 quote (TType uexp) = `(TType ~(quote uexp))

563558 quote (UType u) = `(UType ~(quote u))

564559

@@ -585,7 +580,6 @@ mutual

585580 quoteRawTT (RApp tm tm') = `(RApp ~(quoteRawTT tm) ~(quoteRawTT tm'))

586581 quoteRawTT RType = `(RType)

587582 quoteRawTT (RUType u) = `(RUType ~(quote u))

588− quoteRawTT (RForce tm) = `(RForce ~(quoteRawTT tm))

589583 quoteRawTT (RConstant c) = `(RConstant ~(quote c))

590584

591585 quoteRawBinderTT : Binder Raw -> TT

@@ -614,7 +608,6 @@ mutual

614608 quoteRawRaw (RApp tm tm') = `(RApp ~(quoteRawRaw tm) ~(quoteRawRaw tm'))

615609 quoteRawRaw RType = `(RType)

616610 quoteRawRaw (RUType u) = `(RUType ~(quote u))

617− quoteRawRaw (RForce tm) = `(RForce ~(quoteRawRaw tm))

618611 quoteRawRaw (RConstant c) = `(RConstant ~(quote c))

619612

620613 quoteRawBinderRaw : Binder Raw -> Raw

libs/pruviloj/Pruviloj/Induction.idr−1

@@ -36,7 +36,6 @@ mutual

3636 alphaEqual subst f g && alphaEqual subst x y

3737 alphaEqual subst RType RType = True

3838 alphaEqual subst (RUType u) (RUType u') = u == u'

39− alphaEqual subst (RForce tm) (RForce tm') = alphaEqual subst tm tm'

4039 alphaEqual subst (RConstant c) (RConstant c') = c == c'

4140 alphaEqual subst _ _ = False

4241

libs/pruviloj/Pruviloj/Renamers.idr−1

@@ -39,5 +39,4 @@ alphaRaw subst (RBind n b tm) =

3939alphaRaw subst (RApp tm tm') = RApp (alphaRaw subst tm) (alphaRaw subst tm')

4040alphaRaw subst RType = RType

4141alphaRaw subst (RUType x) = RUType x

42−alphaRaw subst (RForce tm) = RForce (alphaRaw subst tm)

4342alphaRaw subst (RConstant c) = RConstant c

src/Idris/Core/Binary.hs+1−5

@@ -452,9 +452,7 @@ instance Binary Raw where

452452 RType -> putWord8 3

453453 RConstant x1 -> do putWord8 4

454454 put x1

455− RForce x1 -> do putWord8 5

456− put x1

457− RUType x1 -> do putWord8 6

455+ RUType x1 -> do putWord8 5

458456 put x1

459457 get

460458 = do i <- getWord8

@@ -472,8 +470,6 @@ instance Binary Raw where

472470 4 -> do x1 <- get

473471 return (RConstant x1)

474472 5 -> do x1 <- get

475− return (RForce x1)

476− 6 -> do x1 <- get

477473 return (RUType x1)

478474 _ -> error "Corrupted binary data for Raw"

479475

src/Idris/Core/DeepSeq.hs−1

@@ -81,7 +81,6 @@ instance NFData Raw where

8181 rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8282 rnf RType = ()

8383 rnf (RUType x1) = rnf x1 `seq` ()

84− rnf (RForce x1) = rnf x1 `seq` ()

8584 rnf (RConstant x1) = x1 `seq` ()

8685

8786instance NFData FC where

src/Idris/Core/TT.hs−5

@@ -776,7 +776,6 @@ data Raw = Var Name

776776 | RApp Raw Raw

777777 | RType

778778 | RUType Universe

779− | RForce Raw

780779 | RConstant Const

781780 deriving (Show, Eq, Data, Typeable)

782781

@@ -786,7 +785,6 @@ instance Sized Raw where

786785 size (RApp left right) = 1 + size left + size right

787786 size RType = 1

788787 size (RUType _) = 1

789− size (RForce raw) = 1 + size raw

790788 size (RConstant const) = size const

791789

792790instance Pretty Raw OutputAnnotation where

@@ -1823,9 +1821,6 @@ pprintRaw bound (RApp f x) =

18231821pprintRaw bound RType = text "RType"

18241822pprintRaw bound (RUType u) = enclose lparen rparen . group . align . hang 2 $

18251823 text "RUType" <$> text (show u)

1826−pprintRaw bound (RForce r) =

1827− enclose lparen rparen . group . align . hang 2 $

1828− vsep [text "RForce", pprintRaw bound r]

18291824pprintRaw bound (RConstant c) =

18301825 enclose lparen rparen . group . align . hang 2 $

18311826 vsep [text "RConstant", annotate (AnnConst c) (text (show c))]

src/Idris/Core/Typecheck.hs−3

@@ -160,9 +160,6 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

160160 constType TheWorld = Constant WorldType

161161 constType Forgot = Erased

162162 constType _ = TType (UVal 0)

163− chk u env (RForce t)

164− = do (_, ty) <- chk u env t

165− return (Erased, ty)

166163 chk u env (RBind n (Pi i s k) t)

167164 = do (sv, st) <- chk u env s

168165 (v, cs) <- get

src/Idris/DataOpts.hs−1

@@ -40,7 +40,6 @@ instance Optimisable Raw where

4040 | otherwise = RApp <$> applyOpts f <*> applyOpts a

4141

4242 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t

43− applyOpts (RForce t) = applyOpts t

4443 applyOpts t = return t

4544

4645-- Erase types (makes ibc smaller, and we don't need them)

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 120

43+ibcVersion = 121

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

src/Idris/Reflection.hs+11−24

@@ -219,8 +219,6 @@ reifyRawApp t [n, b, x]

219219 return $ RBind n' b' x'

220220reifyRawApp t [f, x]

221221 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)

222−reifyRawApp t [t']

223− | t == reflm "RForce" = liftM RForce (reifyRaw t')

224222reifyRawApp t [c]

225223 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

226224reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))

@@ -475,18 +473,15 @@ reflectTTQuotePattern unq (Constant c)

475473 = do fill $ reflCall "TConst" [reflectConstant c]

476474 solve

477475reflectTTQuotePattern unq (Proj t i)

478− = do t' <- claimTy (sMN 0 "t") (Var (reflm "TT")) ; movelast t'

479− fill $ reflCall "Proj" [Var t', RConstant (I i)]

480− solve

481− focus t'; reflectTTQuotePattern unq t

482−reflectTTQuotePattern unq (Erased)

476+ = lift . tfail . InternalMsg $

477+ "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."

478+reflectTTQuotePattern unq Erased

483479 = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))

484480 movelast erased

485481 fill $ (Var erased)

486− solve

487−reflectTTQuotePattern unq (Impossible)

488− = do fill $ Var (reflm "Impossible")

489− solve

482+reflectTTQuotePattern unq Impossible

483+ = lift . tfail . InternalMsg $

484+ "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."

490485reflectTTQuotePattern unq (TType exp)

491486 = do ue <- getNameFrom (sMN 0 "uexp")

492487 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

@@ -539,7 +534,6 @@ reflectRawQuotePattern unq (RBind n b sc) =

539534 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

540535 freeNamesR RType = []

541536 freeNamesR (RUType _) = []

542− freeNamesR (RForce r) = freeNamesR r

543537 freeNamesR (RConstant _) = []

544538reflectRawQuotePattern unq (RApp f x) =

545539 do fH <- getNameFrom (sMN 0 "f")

@@ -562,13 +556,6 @@ reflectRawQuotePattern unq (RUType univ) =

562556 fill $ reflCall "RUType" [Var uH]

563557 solve

564558 focus uH; fill (reflectUniverse univ); solve

565−reflectRawQuotePattern unq (RForce r) =

566− do rH <- getNameFrom (sMN 0 "raw")

567− claim rH (Var (reflm "Raw"))

568− movelast rH

569− fill $ reflCall "RForce" [Var rH]

570− solve

571− focus rH; reflectRawQuotePattern unq r

572559reflectRawQuotePattern unq (RConstant c) =

573560 do cH <- getNameFrom (sMN 0 "const")

574561 claim cH (Var (reflm "Constant"))

@@ -651,12 +638,13 @@ reflectTTQuote unq (App _ f x)

651638 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

652639reflectTTQuote unq (Constant c)

653640 = reflCall "TConst" [reflectConstant c]

654−reflectTTQuote unq (Proj t i)

655− = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]

656−reflectTTQuote unq (Erased) = Var (reflm "Erased")

657−reflectTTQuote unq (Impossible) = Var (reflm "Impossible")

658641reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

659642reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]

643+reflectTTQuote _ (Proj _ _) =

644+ error "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."

645+reflectTTQuote unq Erased = Var (reflm "Erased")

646+reflectTTQuote _ Impossible =

647+ error "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."

660648

661649reflectRawQuote :: [Name] -> Raw -> Raw

662650reflectRawQuote unq (Var n)

@@ -669,7 +657,6 @@ reflectRawQuote unq (RApp f x) =

669657reflectRawQuote unq RType = Var (reflm "RType")

670658reflectRawQuote unq (RUType u) =

671659 reflCall "RUType" [reflectUniverse u]

672−reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]

673660reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]

674661

675662reflectNameType :: NameType -> Raw