b774d12 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove NLet binder from reflection API

This will never occur during elaboration - it's a part of the evaluator.

commitb774d124e35e3f3c5c6eded2453696a8f4586b0b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 7 Oct 2015, 11:50 (11 years ago) parent4b06aa4

6 files changed+24−25

compare with master

unifiedsplit

libs/base/Language/Reflection/Utils.idr−3 libs/prelude/Language/Reflection.idr−8 libs/pruviloj/Pruviloj/Induction.idr−4 libs/pruviloj/Pruviloj/Internals.idr−1 src/Idris/Core/TT.hs+22−5 src/Idris/Reflection.hs+2−4

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

@@ -55,7 +55,6 @@ binderTy : Binder t -> t

5555binderTy (Lam t) = t

5656binderTy (Pi t _) = t

5757binderTy (Let t1 t2) = t1

58−binderTy (NLet t1 t2) = t1

5958binderTy (Hole t) = t

6059binderTy (GHole t) = t

6160binderTy (Guess t1 t2) = t1

@@ -196,7 +195,6 @@ instance (Show a) => Show (Binder a) where

196195 showPrec d (Lam t) = showCon d "Lam" $ showArg t

197196 showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2

198197 showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2

199− showPrec d (NLet t1 t2) = showCon d "NLet" $ showArg t1 ++ showArg t2

200198 showPrec d (Hole t) = showCon d "Hole" $ showArg t

201199 showPrec d (GHole t) = showCon d "GHole" $ showArg t

202200 showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2

@@ -207,7 +205,6 @@ instance (Eq a) => Eq (Binder a) where

207205 (Lam t) == (Lam t') = t == t'

208206 (Pi t k) == (Pi t' k') = t == t' && k == k'

209207 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'

210− (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'

211208 (Hole t) == (Hole t') = t == t'

212209 (GHole t) == (GHole t') = t == t'

213210 (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'

libs/prelude/Language/Reflection.idr−8

@@ -119,7 +119,6 @@ data NameType =

119119data Binder a = Lam a

120120 | Pi a a

121121 | Let a a

122− | NLet a a

123122 | Hole a

124123 | GHole a

125124 | Guess a a

@@ -131,7 +130,6 @@ instance Functor Binder where

131130 map f (Lam x) = Lam (f x)

132131 map f (Pi x k) = Pi (f x) (f k)

133132 map f (Let x y) = Let (f x) (f y)

134− map f (NLet x y) = NLet (f x) (f y)

135133 map f (Hole x) = Hole (f x)

136134 map f (GHole x) = GHole (f x)

137135 map f (Guess x y) = Guess (f x) (f y)

@@ -142,7 +140,6 @@ instance Foldable Binder where

142140 foldr f z (Lam x) = f x z

143141 foldr f z (Pi x k) = f x (f k z)

144142 foldr f z (Let x y) = f x (f y z)

145− foldr f z (NLet x y) = f x (f y z)

146143 foldr f z (Hole x) = f x z

147144 foldr f z (GHole x) = f x z

148145 foldr f z (Guess x y) = f x (f y z)

@@ -153,7 +150,6 @@ instance Traversable Binder where

153150 traverse f (Lam x) = [| Lam (f x) |]

154151 traverse f (Pi x k) = [| Pi (f x) (f k) |]

155152 traverse f (Let x y) = [| Let (f x) (f y) |]

156− traverse f (NLet x y) = [| NLet (f x) (f y) |]

157153 traverse f (Hole x) = [| Hole (f x) |]

158154 traverse f (GHole x) = [| GHole (f x) |]

159155 traverse f (Guess x y) = [| Guess (f x) (f y) |]

@@ -564,8 +560,6 @@ mutual

564560 ~(assert_total (quote k)))

565561 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))

566562 ~(assert_total (quote y)))

567− quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))

568− ~(assert_total (quote y)))

569563 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))

570564 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))

571565 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))

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

586580 quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))

587581 quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))

588582 quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))

589− quoteRawBinderTT (NLet x y) = `(NLet {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))

590583 quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x))

591584 quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))

592585 quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))

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

614607 quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))

615608 quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))

616609 quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))

617− quoteRawBinderRaw (NLet x y) = `(NLet {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))

618610 quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x))

619611 quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))

620612 quoteRawBinderRaw (Guess x y) = `(Guess {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))

libs/pruviloj/Pruviloj/Induction.idr−4

@@ -48,9 +48,6 @@ mutual

4848 alphaEqualBinders subst (Let tm1 tm2) (Let tm1' tm2') =

4949 alphaEqual subst tm1 tm1' &&

5050 alphaEqual subst tm2 tm2'

51− alphaEqualBinders subst (NLet tm1 tm2) (NLet tm1' tm2') =

52− alphaEqual subst tm1 tm1' &&

53− alphaEqual subst tm2 tm2'

5451 alphaEqualBinders subst (Hole tm) (Hole tm') =

5552 alphaEqual subst tm tm'

5653 alphaEqualBinders subst (GHole tm) (GHole tm') =

@@ -78,7 +75,6 @@ generalize hint ctxt subj = do n <- gensym hint

7875 genB n (Lam ty) inner = [| Lam (gen' n ty inner) |]

7976 genB n (Pi ty ty') inner = [| Pi (gen' n ty inner) (gen' n ty' inner) |]

8077 genB n (Let ty val) inner = [| Let (gen' n ty inner) (gen' n val inner) |]

81− genB n (NLet ty val) inner = [| NLet (gen' n ty inner) (gen' n val inner) |]

8278 genB n (Hole ty) inner = [| Hole (gen' n ty inner) |]

8379 genB n (GHole ty) inner = [| GHole (gen' n ty inner) |]

8480 genB n (Guess ty val) inner = [| Guess (gen' n ty inner) (gen' n val inner) |]

libs/pruviloj/Pruviloj/Internals.idr−1

@@ -63,7 +63,6 @@ getBinderTy : Binder t -> t

6363getBinderTy (Lam t) = t

6464getBinderTy (Pi t _) = t

6565getBinderTy (Let t _) = t

66−getBinderTy (NLet t _) = t

6766getBinderTy (Hole t) = t

6867getBinderTy (GHole t) = t

6968getBinderTy (Guess t _) = t

src/Idris/Core/TT.hs+22−5

@@ -810,27 +810,44 @@ deriving instance NFData ImplicitInfo

810810-- the types of bindings (and their values, if any); the attached identifiers are part

811811-- of the 'Bind' constructor for the 'TT' type.

812812data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}

813+ -- ^ A function binding

813814 | Pi { binderImpl :: Maybe ImplicitInfo,

814815 binderTy :: !b,

815816 binderKind :: !b }

816− {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@

817− The 'binderImpl' flag says whether it was a scoped implicit

818− (i.e. forall bound) in the high level Idris, but otherwise

819− has no relevance in TT. -}

817+ -- ^ A binding that occurs in a function type

818+ -- expression, e.g. @(x:Int) -> ...@ The 'binderImpl'

819+ -- flag says whether it was a scoped implicit

820+ -- (i.e. forall bound) in the high level Idris, but

821+ -- otherwise has no relevance in TT.

820822 | Let { binderTy :: !b,

821823 binderVal :: b {-^ value for bound variable-}}

822824 -- ^ A binding that occurs in a @let@ expression

823825 | NLet { binderTy :: !b,

824826 binderVal :: b }

827+ -- ^ NLet is an intermediate product in the evaluator

828+ -- that's used for temporarily naming locals during

829+ -- reduction. It won't occur outside the evaluator.

825830 | Hole { binderTy :: !b}

831+ -- ^ A hole in a term under construction in the

832+ -- elaborator. If this is not filled during

833+ -- elaboration, it is an error.

826834 | GHole { envlen :: Int,

827835 localnames :: [Name],

828836 binderTy :: !b}

837+ -- ^ A saved TT hole that will later be converted to a

838+ -- top-level Idris metavariable applied to all

839+ -- elements of its local environment.

829840 | Guess { binderTy :: !b,

830841 binderVal :: b }

842+ -- ^ A provided value for a hole. It will later be

843+ -- substituted - the guess is to keep it

844+ -- computationally inert while working on other things

845+ -- if necessary.

831846 | PVar { binderTy :: !b }

832− -- ^ A pattern variable

847+ -- ^ A pattern variable (these are bound around terms

848+ -- that make up pattern-match clauses)

833849 | PVTy { binderTy :: !b }

850+ -- ^ The type of a pattern binding

834851 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)

835852{-!

836853deriving instance Binary Binder

src/Idris/Reflection.hs+2−4

@@ -310,8 +310,6 @@ reifyTTBinderApp reif f [t, k]

310310 | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)

311311reifyTTBinderApp reif f [x, y]

312312 | f == reflm "Let" = liftM2 Let (reif x) (reif y)

313−reifyTTBinderApp reif f [x, y]

314− | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)

315313reifyTTBinderApp reif f [t]

316314 | f == reflm "Hole" = liftM Hole (reif t)

317315reifyTTBinderApp reif f [t]

@@ -586,7 +584,7 @@ reflectBinderQuotePattern q ty unq (Let x y)

586584reflectBinderQuotePattern q ty unq (NLet x y)

587585 = do x' <- claimTy (sMN 0 "ty") ty; movelast x'

588586 y' <- claimTy (sMN 0 "v") ty; movelast y'

589− fill $ reflCall "NLet" [ty, Var x', Var y']

587+ fill $ reflCall "Let" [ty, Var x', Var y']

590588 solve

591589 focus x'; q unq x

592590 focus y'; q unq y

@@ -743,7 +741,7 @@ reflectBinderQuote q ty unq (Pi _ t k)

743741reflectBinderQuote q ty unq (Let x y)

744742 = reflCall "Let" [Var ty, q unq x, q unq y]

745743reflectBinderQuote q ty unq (NLet x y)

746− = reflCall "NLet" [Var ty, q unq x, q unq y]

744+ = reflCall "Let" [Var ty, q unq x, q unq y]

747745reflectBinderQuote q ty unq (Hole t)

748746 = reflCall "Hole" [Var ty, q unq t]

749747reflectBinderQuote q ty unq (GHole _ _ t)