b774d12 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove NLet binder from reflection API

b774d12David Raymond Christiansen11 years ago

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

compare with master

unifiedsplit

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

55binderTy (Lam t) = t

56binderTy (Pi t _) = t

57binderTy (Let t1 t2) = t1

58−binderTy (NLet t1 t2) = t1

59binderTy (Hole t) = t

58binderTy (Hole t) = t

60binderTy (GHole t) = t

59binderTy (GHole t) = t

61binderTy (Guess t1 t2) = t1

60binderTy (Guess t1 t2) = t1

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

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

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

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

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

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

197 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

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

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

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

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

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

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

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

207 (Lam t) == (Lam t') = t == t'

205 (Lam t) == (Lam t') = t == t'

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

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

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

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

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

211 (Hole t) == (Hole t') = t == t'

208 (Hole t) == (Hole t') = t == t'

212 (GHole t) == (GHole t') = t == t'

209 (GHole t) == (GHole t') = t == t'

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

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

libs/prelude/Language/Reflection.idr−8

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

119data Binder a = Lam a

120 | Pi a a

121 | Let a a

122− | NLet a a

123 | Hole a

122 | Hole a

124 | GHole a

123 | GHole a

125 | Guess a a

124 | Guess a a

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

131 map f (Lam x) = Lam (f x)

130 map f (Lam x) = Lam (f x)

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

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

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

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

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

135 map f (Hole x) = Hole (f x)

133 map f (Hole x) = Hole (f x)

136 map f (GHole x) = GHole (f x)

134 map f (GHole x) = GHole (f x)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

564 ~(assert_total (quote k)))

560 ~(assert_total (quote k)))

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

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

566 ~(assert_total (quote y)))

562 ~(assert_total (quote y)))

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

568− ~(assert_total (quote y)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

libs/pruviloj/Pruviloj/Induction.idr−4

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

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

49 alphaEqual subst tm1 tm1' &&

50 alphaEqual subst tm2 tm2'

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

52− alphaEqual subst tm1 tm1' &&

53− alphaEqual subst tm2 tm2'

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

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

55 alphaEqual subst tm tm'

52 alphaEqual subst tm tm'

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

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

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

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

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

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

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

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

77 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) |]

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

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

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

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

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

80 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

63getBinderTy (Lam t) = t

64getBinderTy (Pi t _) = t

65getBinderTy (Let t _) = t

66−getBinderTy (NLet t _) = t

67getBinderTy (Hole t) = t

66getBinderTy (Hole t) = t

68getBinderTy (GHole t) = t

67getBinderTy (GHole t) = t

69getBinderTy (Guess t _) = t

68getBinderTy (Guess t _) = t

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

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

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

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

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

813+ -- ^ A function binding

813 | Pi { binderImpl :: Maybe ImplicitInfo,

814 | Pi { binderImpl :: Maybe ImplicitInfo,

814 binderTy :: !b,

815 binderTy :: !b,

815 binderKind :: !b }

816 binderKind :: !b }

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

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

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

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

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

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

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

819− has no relevance in TT. -}

821+ -- otherwise has no relevance in TT.

820 | Let { binderTy :: !b,

822 | Let { binderTy :: !b,

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

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

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

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

823 | NLet { binderTy :: !b,

825 | NLet { binderTy :: !b,

824 binderVal :: b }

826 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.

825 | Hole { binderTy :: !b}

830 | 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.

826 | GHole { envlen :: Int,

834 | GHole { envlen :: Int,

827 localnames :: [Name],

835 localnames :: [Name],

828 binderTy :: !b}

836 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.

829 | Guess { binderTy :: !b,

840 | Guess { binderTy :: !b,

830 binderVal :: b }

841 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.

831 | PVar { binderTy :: !b }

846 | PVar { binderTy :: !b }

832− -- ^ A pattern variable

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

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

833 | PVTy { binderTy :: !b }

849 | PVTy { binderTy :: !b }

850+ -- ^ The type of a pattern binding

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

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

835{-!

852{-!

836deriving instance Binary Binder

853deriving instance Binary Binder

src/Idris/Reflection.hs+2−4

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

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

311reifyTTBinderApp reif f [x, y]

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

315reifyTTBinderApp reif f [t]

313reifyTTBinderApp reif f [t]

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

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

317reifyTTBinderApp reif f [t]

315reifyTTBinderApp reif f [t]

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

586reflectBinderQuotePattern q ty unq (NLet x y)

584reflectBinderQuotePattern q ty unq (NLet x y)

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

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

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

586 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']

590 solve

588 solve

591 focus x'; q unq x

589 focus x'; q unq x

592 focus y'; q unq y

590 focus y'; q unq y

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

743reflectBinderQuote q ty unq (Let x y)

741reflectBinderQuote q ty unq (Let x y)

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

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

745reflectBinderQuote q ty unq (NLet x y)

743reflectBinderQuote 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]

747reflectBinderQuote q ty unq (Hole t)

745reflectBinderQuote q ty unq (Hole t)

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

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

749reflectBinderQuote q ty unq (GHole _ _ t)

747reflectBinderQuote q ty unq (GHole _ _ t)