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

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

compare with master

unifiedsplit

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

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

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

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

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

227 my_show d Erased = "Erased"

226 my_show d Erased = "Erased"

228− my_show d Impossible = "Impossible"

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

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

230

228

231instance Eq TT where

229instance Eq TT where

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

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

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

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

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

238 equalp (TConst c) (TConst c') = c == c'

236 equalp (TConst c) (TConst c') = c == c'

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

240 equalp Erased Erased = True

237 equalp Erased Erased = True

241− equalp Impossible Impossible = True

242 equalp (TType u) (TType u') = u == u'

238 equalp (TType u) (TType u') = u == u'

243 equalp x y = False

239 equalp x y = False

244

240

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

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

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

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

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

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

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

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

271 fe env (TType i) = Just RType

266 fe env (TType i) = Just RType

272 fe env Erased = Just $ RConstant Forgot

267 fe env Erased = Just $ RConstant Forgot

273− fe env Impossible = Nothing

274

268

275instance Show Raw where

269instance Show Raw where

276 showPrec = my_show

270 showPrec = my_show

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

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

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

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

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

281 my_show d RType = "RType"

275 my_show d RType = "RType"

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

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

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

284

277

285instance Show SourceLocation where

278instance Show SourceLocation where

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

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

175 App TT TT |

176 ||| Embed a constant

177 TConst Const |

178− ||| Argument projection; runtime only

179− Proj TT Int |

180 ||| Erased terms

178 ||| Erased terms

181 Erased |

179 Erased |

182− ||| Impossible terms

183− Impossible |

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

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

185 TType TTUExp |

181 TType TTUExp |

182+ ||| Alternative universes for dealing with uniqueness

186 UType Universe

183 UType Universe

187%name TT tm, tm'

184%name TT tm, tm'

188

185

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

196 RApp Raw Raw |

193 RApp Raw Raw |

197 ||| The type of types

194 ||| The type of types

198 RType |

195 RType |

196+ ||| Alternative universes for dealing with uniqueness

199 RUType Universe |

197 RUType Universe |

200− RForce Raw |

201 ||| Embed a constant

198 ||| Embed a constant

202 RConstant Const

199 RConstant Const

203%name Raw tm, tm'

200%name Raw tm, tm'

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

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

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

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

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

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

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

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

560 quote Erased = `(Erased)

556 quote Erased = `(Erased)

561− quote Impossible = `(Impossible)

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

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

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

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

564

559

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

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

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

586 quoteRawTT RType = `(RType)

581 quoteRawTT RType = `(RType)

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

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

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

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

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

590

584

591 quoteRawBinderTT : Binder Raw -> TT

585 quoteRawBinderTT : Binder Raw -> TT

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

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

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

615 quoteRawRaw RType = `(RType)

609 quoteRawRaw RType = `(RType)

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

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

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

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

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

619

612

620 quoteRawBinderRaw : Binder Raw -> Raw

613 quoteRawBinderRaw : Binder Raw -> Raw

libs/pruviloj/Pruviloj/Induction.idr−1

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

36 alphaEqual subst f g && alphaEqual subst x y

37 alphaEqual subst RType RType = True

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

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

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

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

41 alphaEqual subst _ _ = False

40 alphaEqual subst _ _ = False

42

41

libs/pruviloj/Pruviloj/Renamers.idr−1

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

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

40alphaRaw subst RType = RType

41alphaRaw subst (RUType x) = RUType x

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

43alphaRaw subst (RConstant c) = RConstant c

42alphaRaw subst (RConstant c) = RConstant c

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

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

452 RType -> putWord8 3

453 RConstant x1 -> do putWord8 4

454 put x1

455− RForce x1 -> do putWord8 5

456− put x1

457− RUType x1 -> do putWord8 6

455+ RUType x1 -> do putWord8 5

458 put x1

456 put x1

459 get

457 get

460 = do i <- getWord8

458 = do i <- getWord8

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

472 4 -> do x1 <- get

470 4 -> do x1 <- get

473 return (RConstant x1)

471 return (RConstant x1)

474 5 -> do x1 <- get

472 5 -> do x1 <- get

475− return (RForce x1)

476− 6 -> do x1 <- get

477 return (RUType x1)

473 return (RUType x1)

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

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

479

475

src/Idris/Core/DeepSeq.hs−1

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

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

82 rnf RType = ()

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

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

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

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

86

85

87instance NFData FC where

86instance NFData FC where

src/Idris/Core/TT.hs−5

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

776 | RApp Raw Raw

777 | RType

778 | RUType Universe

779− | RForce Raw

780 | RConstant Const

779 | RConstant Const

781 deriving (Show, Eq, Data, Typeable)

780 deriving (Show, Eq, Data, Typeable)

782

781

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

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

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

787 size RType = 1

786 size RType = 1

788 size (RUType _) = 1

787 size (RUType _) = 1

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

790 size (RConstant const) = size const

788 size (RConstant const) = size const

791

789

792instance Pretty Raw OutputAnnotation where

790instance Pretty Raw OutputAnnotation where

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

1823pprintRaw bound RType = text "RType"

1821pprintRaw bound RType = text "RType"

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

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

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

1823 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]

1829pprintRaw bound (RConstant c) =

1824pprintRaw bound (RConstant c) =

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

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

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

1826 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

160 constType TheWorld = Constant WorldType

161 constType Forgot = Erased

162 constType _ = TType (UVal 0)

163− chk u env (RForce t)

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

165− return (Erased, ty)

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

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

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

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

168 (v, cs) <- get

165 (v, cs) <- get

src/Idris/DataOpts.hs−1

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

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

41

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

43− applyOpts (RForce t) = applyOpts t

44 applyOpts t = return t

43 applyOpts t = return t

45

44

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

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

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 120

43+ibcVersion = 121

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/Reflection.hs+11−24

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

219 return $ RBind n' b' x'

220reifyRawApp t [f, x]

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

222−reifyRawApp t [t']

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

224reifyRawApp t [c]

222reifyRawApp t [c]

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

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

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

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

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

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

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

476 solve

474 solve

477reflectTTQuotePattern unq (Proj t i)

475reflectTTQuotePattern unq (Proj t i)

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

476+ = lift . tfail . InternalMsg $

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

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

480− solve

481− focus t'; reflectTTQuotePattern unq t

482−reflectTTQuotePattern unq (Erased)

478+reflectTTQuotePattern unq Erased

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

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

484 movelast erased

480 movelast erased

485 fill $ (Var erased)

481 fill $ (Var erased)

486− solve

487−reflectTTQuotePattern unq (Impossible)

482+reflectTTQuotePattern unq Impossible

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

483+ = lift . tfail . InternalMsg $

489− solve

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

490reflectTTQuotePattern unq (TType exp)

485reflectTTQuotePattern unq (TType exp)

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

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

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

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

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

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

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

540 freeNamesR RType = []

535 freeNamesR RType = []

541 freeNamesR (RUType _) = []

536 freeNamesR (RUType _) = []

542− freeNamesR (RForce r) = freeNamesR r

543 freeNamesR (RConstant _) = []

537 freeNamesR (RConstant _) = []

544reflectRawQuotePattern unq (RApp f x) =

538reflectRawQuotePattern unq (RApp f x) =

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

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

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

562 fill $ reflCall "RUType" [Var uH]

556 fill $ reflCall "RUType" [Var uH]

563 solve

557 solve

564 focus uH; fill (reflectUniverse univ); solve

558 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

572reflectRawQuotePattern unq (RConstant c) =

559reflectRawQuotePattern unq (RConstant c) =

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

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

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

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

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

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

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

652reflectTTQuote unq (Constant c)

639reflectTTQuote unq (Constant c)

653 = reflCall "TConst" [reflectConstant c]

640 = 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")

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

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

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

642reflectTTQuote 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."

660

648

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

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

662reflectRawQuote unq (Var n)

650reflectRawQuote unq (Var n)

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

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

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

670reflectRawQuote unq (RUType u) =

658reflectRawQuote unq (RUType u) =

671 reflCall "RUType" [reflectUniverse u]

659 reflCall "RUType" [reflectUniverse u]

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

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

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

674

661

675reflectNameType :: NameType -> Raw

662reflectNameType :: NameType -> Raw