ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-14 03:14:14 +03:00
Code Issues Projects Releases Wiki Activity

Simplify reflection and Raw

Browse Source 
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.
This commit is contained in:
David Raymond Christiansen 2015-10-06 17:03:38 +02:00
parent 75e45f9e7c
commit 105c230217
11 changed files with 15 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libs/base/Language/Reflection/Utils.idr
View File

@ -223,9 +223,7 @@ instance Show TT where
my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t
my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2
my_show d (TConst c) = showCon d "TConst" $ showArg c
my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i
my_show d Erased = "Erased"
my_show d Impossible = "Impossible"
my_show d (TType u) = showCon d "TType" $ showArg u
instance Eq TT where
@ -236,9 +234,7 @@ instance Eq TT where
equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'
equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'
equalp (TConst c) (TConst c') = c == c'
equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
equalp Erased Erased = True
equalp Impossible Impossible = True
equalp (TType u) (TType u') = u == u'
equalp x y = False
@ -267,10 +263,8 @@ forget tm = fe [] tm
fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]
fe env (App f a) = [| RApp (fe env f) (fe env a) |]
fe env (TConst c) = Just $ RConstant c
fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming
fe env (TType i) = Just RType
fe env Erased = Just $ RConstant Forgot
fe env Impossible = Nothing
instance Show Raw where
showPrec = my_show
@ -279,7 +273,6 @@ instance Show Raw where
my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm
my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'
my_show d RType = "RType"
my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm
my_show d (RConstant c) = showCon d "RConstant" $ showArg c
instance Show SourceLocation where

11
libs/prelude/Language/Reflection.idr
View File

@ -175,14 +175,11 @@ data TT =
App TT TT |
||| Embed a constant
TConst Const |
||| Argument projection; runtime only
Proj TT Int |
||| Erased terms
Erased |
||| Impossible terms
Impossible |
||| The type of types along (with universe constraints)
TType TTUExp |
||| Alternative universes for dealing with uniqueness
UType Universe
%name TT tm, tm'
@ -196,8 +193,8 @@ data Raw =
RApp Raw Raw |
||| The type of types
RType |
||| Alternative universes for dealing with uniqueness
RUType Universe |
RForce Raw |
||| Embed a constant
RConstant Const
%name Raw tm, tm'
@ -556,9 +553,7 @@ mutual
quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))
quote (App f x) = `(App ~(quote f) ~(quote x))
quote (TConst c) = `(TConst ~(quote c))
quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))
quote Erased = `(Erased)
quote Impossible = `(Impossible)
quote (TType uexp) = `(TType ~(quote uexp))
quote (UType u) = `(UType ~(quote u))
@ -585,7 +580,6 @@ mutual
quoteRawTT (RApp tm tm') = `(RApp ~(quoteRawTT tm) ~(quoteRawTT tm'))
quoteRawTT RType = `(RType)
quoteRawTT (RUType u) = `(RUType ~(quote u))
quoteRawTT (RForce tm) = `(RForce ~(quoteRawTT tm))
quoteRawTT (RConstant c) = `(RConstant ~(quote c))
quoteRawBinderTT : Binder Raw -> TT
@ -614,7 +608,6 @@ mutual
quoteRawRaw (RApp tm tm') = `(RApp ~(quoteRawRaw tm) ~(quoteRawRaw tm'))
quoteRawRaw RType = `(RType)
quoteRawRaw (RUType u) = `(RUType ~(quote u))
quoteRawRaw (RForce tm) = `(RForce ~(quoteRawRaw tm))
quoteRawRaw (RConstant c) = `(RConstant ~(quote c))
quoteRawBinderRaw : Binder Raw -> Raw

1
libs/pruviloj/Pruviloj/Induction.idr
View File

@ -36,7 +36,6 @@ mutual
alphaEqual subst f g && alphaEqual subst x y
alphaEqual subst RType RType = True
alphaEqual subst (RUType u) (RUType u') = u == u'
alphaEqual subst (RForce tm) (RForce tm') = alphaEqual subst tm tm'
alphaEqual subst (RConstant c) (RConstant c') = c == c'
alphaEqual subst _ _ = False

1
libs/pruviloj/Pruviloj/Renamers.idr
View File

@ -39,5 +39,4 @@ alphaRaw subst (RBind n b tm) =
alphaRaw subst (RApp tm tm') = RApp (alphaRaw subst tm) (alphaRaw subst tm')
alphaRaw subst RType = RType
alphaRaw subst (RUType x) = RUType x
alphaRaw subst (RForce tm) = RForce (alphaRaw subst tm)
alphaRaw subst (RConstant c) = RConstant c

6
src/Idris/Core/Binary.hs
View File

@ -452,9 +452,7 @@ instance Binary Raw where
RType -> putWord8 3
RConstant x1 -> do putWord8 4
put x1
RForce x1 -> do putWord8 5
put x1
RUType x1 -> do putWord8 6
RUType x1 -> do putWord8 5
put x1
get
= do i <- getWord8
@ -472,8 +470,6 @@ instance Binary Raw where
4 -> do x1 <- get
return (RConstant x1)
5 -> do x1 <- get
return (RForce x1)
6 -> do x1 <- get
return (RUType x1)
_ -> error "Corrupted binary data for Raw"

1
src/Idris/Core/DeepSeq.hs
View File

@ -81,7 +81,6 @@ instance NFData Raw where
rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf RType = ()
rnf (RUType x1) = rnf x1 `seq` ()
rnf (RForce x1) = rnf x1 `seq` ()
rnf (RConstant x1) = x1 `seq` ()
instance NFData FC where

5
src/Idris/Core/TT.hs
View File

@ -776,7 +776,6 @@ data Raw = Var Name
| RApp Raw Raw
| RType
| RUType Universe
| RForce Raw
| RConstant Const
deriving (Show, Eq, Data, Typeable)
@ -786,7 +785,6 @@ instance Sized Raw where
size (RApp left right) = 1 + size left + size right
size RType = 1
size (RUType _) = 1
size (RForce raw) = 1 + size raw
size (RConstant const) = size const
instance Pretty Raw OutputAnnotation where
@ -1823,9 +1821,6 @@ pprintRaw bound (RApp f x) =
pprintRaw bound RType = text "RType"
pprintRaw bound (RUType u) = enclose lparen rparen . group . align . hang 2 $
text "RUType" <$> text (show u)
pprintRaw bound (RForce r) =
enclose lparen rparen . group . align . hang 2 $
vsep [text "RForce", pprintRaw bound r]
pprintRaw bound (RConstant c) =
enclose lparen rparen . group . align . hang 2 $
vsep [text "RConstant", annotate (AnnConst c) (text (show c))]

3
src/Idris/Core/Typecheck.hs
View File

@ -160,9 +160,6 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
constType TheWorld = Constant WorldType
constType Forgot = Erased
constType _ = TType (UVal 0)
chk u env (RForce t)
= do (_, ty) <- chk u env t
return (Erased, ty)
chk u env (RBind n (Pi i s k) t)
= do (sv, st) <- chk u env s
(v, cs) <- get

1
src/Idris/DataOpts.hs
View File

@ -40,7 +40,6 @@ instance Optimisable Raw where
| otherwise = RApp <$> applyOpts f <*> applyOpts a
applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
applyOpts (RForce t) = applyOpts t
applyOpts t = return t
-- Erase types (makes ibc smaller, and we don't need them)

2
src/Idris/IBC.hs
View File

@ -40,7 +40,7 @@ import System.Directory
import Codec.Archive.Zip
ibcVersion :: Word16
ibcVersion = 120
ibcVersion = 121
data IBCFile = IBCFile { ver :: Word16,
sourcefile :: FilePath,

35
src/Idris/Reflection.hs
View File

@ -219,8 +219,6 @@ reifyRawApp t [n, b, x]
return $ RBind n' b' x'
reifyRawApp t [f, x]
| t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
reifyRawApp t [t']
| t == reflm "RForce" = liftM RForce (reifyRaw t')
reifyRawApp t [c]
| t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
@ -475,18 +473,15 @@ reflectTTQuotePattern unq (Constant c)
= do fill $ reflCall "TConst" [reflectConstant c]
solve
reflectTTQuotePattern unq (Proj t i)
= do t' <- claimTy (sMN 0 "t") (Var (reflm "TT")) ; movelast t'
fill $ reflCall "Proj" [Var t', RConstant (I i)]
solve
focus t'; reflectTTQuotePattern unq t
reflectTTQuotePattern unq (Erased)
= lift . tfail . InternalMsg $
"Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern unq Erased
= do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))
movelast erased
fill $ (Var erased)
solve
reflectTTQuotePattern unq (Impossible)
= do fill $ Var (reflm "Impossible")
solve
reflectTTQuotePattern unq Impossible
= lift . tfail . InternalMsg $
"Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern unq (TType exp)
= do ue <- getNameFrom (sMN 0 "uexp")
claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
@ -539,7 +534,6 @@ reflectRawQuotePattern unq (RBind n b sc) =
freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
freeNamesR RType = []
freeNamesR (RUType _) = []
freeNamesR (RForce r) = freeNamesR r
freeNamesR (RConstant _) = []
reflectRawQuotePattern unq (RApp f x) =
do fH <- getNameFrom (sMN 0 "f")
@ -562,13 +556,6 @@ reflectRawQuotePattern unq (RUType univ) =
fill $ reflCall "RUType" [Var uH]
solve
focus uH; fill (reflectUniverse univ); solve
reflectRawQuotePattern unq (RForce r) =
do rH <- getNameFrom (sMN 0 "raw")
claim rH (Var (reflm "Raw"))
movelast rH
fill $ reflCall "RForce" [Var rH]
solve
focus rH; reflectRawQuotePattern unq r
reflectRawQuotePattern unq (RConstant c) =
do cH <- getNameFrom (sMN 0 "const")
claim cH (Var (reflm "Constant"))
@ -651,12 +638,13 @@ reflectTTQuote unq (App _ f x)
= reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
reflectTTQuote unq (Constant c)
= reflCall "TConst" [reflectConstant c]
reflectTTQuote unq (Proj t i)
= reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
reflectTTQuote unq (Erased) = Var (reflm "Erased")
reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
reflectTTQuote _ (Proj _ _) =
error "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuote unq Erased = Var (reflm "Erased")
reflectTTQuote _ Impossible =
error "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectRawQuote :: [Name] -> Raw -> Raw
reflectRawQuote unq (Var n)
@ -669,7 +657,6 @@ reflectRawQuote unq (RApp f x) =
reflectRawQuote unq RType = Var (reflm "RType")
reflectRawQuote unq (RUType u) =
reflCall "RUType" [reflectUniverse u]
reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
reflectNameType :: NameType -> Raw