git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2702 from david-christiansen/reflection-simplification
1304510David Christiansen
libs/base/Language/Reflection/Utils.idr−3
compare with master
unifiedsplit
@@ -55,7 +55,6 @@ binderTy : Binder t -> t
55binderTy (Lam t) = t
55binderTy (Lam t) = t
56binderTy (Pi t _) = t
56binderTy (Pi t _) = t
57binderTy (Let t1 t2) = t1
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+65−20
@@ -116,22 +116,62 @@ data NameType =
116
116
117||| Types annotations for bound variables in different
117||| Types annotations for bound variables in different
118||| binding contexts
118||| binding contexts
119+|||
120+||| @ tmTy the terms that can occur inside the binder, as type
121+||| annotations or bound values
119−data Binder a = Lam a
122+data Binder : (tmTy : Type) -> Type where
123+ ||| Lambdas
124+ |||
125+ ||| @ ty the type of the argument
126+ Lam : (ty : a) -> Binder a
127+
128+ ||| Function types.
129+ |||
130+ ||| @ kind The kind of arrow. Only relevant when dealing with
131+ ||| uniqueness, so you can usually pretend that this
132+ ||| field doesn't exist. For ordinary functions, use the
133+ ||| type of types here.
120− | Pi a a
134+ Pi : (ty, kind : a) -> Binder a
135+
136+ ||| A let binder
137+ |||
138+ ||| @ ty the type of the bound variable
139+ ||| @ val the bound value
121− | Let a a
140+ Let : (ty, val : a) -> Binder a
122− | NLet a a
141+
142+ ||| A hole that can occur during elaboration, and must be filled
143+ |||
144+ ||| @ ty the type of the value that will eventually be put into the hole
123− | Hole a
145+ Hole : (ty : a) -> Binder a
146+
147+ ||| A hole that will later become a top-level metavariable
124− | GHole a
148+ GHole : (ty : a) -> Binder a
149+
150+ ||| A hole with a solution in it. Computationally inert.
151+ |||
152+ ||| @ ty the type of the value in the hole
153+ ||| @ val the value in the hole
125− | Guess a a
154+ Guess : (ty, val : a) -> Binder a
155+
156+ ||| A pattern variable. These bindings surround the terms that make
157+ ||| up the left and right sides of pattern-matching definition
158+ ||| clauses.
159+ |||
160+ ||| @ ty the type of the pattern variable
126− | PVar a
161+ PVar : (ty : a) -> Binder a
162+
163+ ||| The type of a pattern binding. This is to `PVar` as `Pi` is to
164+ ||| `Lam`.
165+ |||
166+ ||| @ ty the type of the pattern variable
127− | PVTy a
167+ PVTy : (ty : a) -> Binder a
168+
128%name Binder b, b'
169%name Binder b, b'
129
170
130instance Functor Binder where
171instance Functor Binder where
131 map f (Lam x) = Lam (f x)
172 map f (Lam x) = Lam (f x)
132 map f (Pi x k) = Pi (f x) (f k)
173 map f (Pi x k) = Pi (f x) (f k)
133 map f (Let x y) = Let (f x) (f y)
174 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)
175 map f (Hole x) = Hole (f x)
136 map f (GHole x) = GHole (f x)
176 map f (GHole x) = GHole (f x)
137 map f (Guess x y) = Guess (f x) (f y)
177 map f (Guess x y) = Guess (f x) (f y)
@@ -142,7 +182,6 @@ instance Foldable Binder where
142 foldr f z (Lam x) = f x z
182 foldr f z (Lam x) = f x z
143 foldr f z (Pi x k) = f x (f k z)
183 foldr f z (Pi x k) = f x (f k z)
144 foldr f z (Let x y) = f x (f y z)
184 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
185 foldr f z (Hole x) = f x z
147 foldr f z (GHole x) = f x z
186 foldr f z (GHole x) = f x z
148 foldr f z (Guess x y) = f x (f y z)
187 foldr f z (Guess x y) = f x (f y z)
@@ -153,14 +192,13 @@ instance Traversable Binder where
153 traverse f (Lam x) = [| Lam (f x) |]
192 traverse f (Lam x) = [| Lam (f x) |]
154 traverse f (Pi x k) = [| Pi (f x) (f k) |]
193 traverse f (Pi x k) = [| Pi (f x) (f k) |]
155 traverse f (Let x y) = [| Let (f x) (f y) |]
194 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) |]
195 traverse f (Hole x) = [| Hole (f x) |]
158 traverse f (GHole x) = [| GHole (f x) |]
196 traverse f (GHole x) = [| GHole (f x) |]
159 traverse f (Guess x y) = [| Guess (f x) (f y) |]
197 traverse f (Guess x y) = [| Guess (f x) (f y) |]
160 traverse f (PVar x) = [| PVar (f x) |]
198 traverse f (PVar x) = [| PVar (f x) |]
161 traverse f (PVTy x) = [| PVTy (f x) |]
199 traverse f (PVTy x) = [| PVTy (f x) |]
162
200
163−||| Universes
201+||| The various universes involved in the uniqueness mechanism
164data Universe = NullType | UniqueType | AllTypes
202data Universe = NullType | UniqueType | AllTypes
165
203
166||| Reflection of the well typed core language
204||| Reflection of the well typed core language
@@ -199,8 +237,18 @@ data Raw =
199 RConstant Const
237 RConstant Const
200%name Raw tm, tm'
238%name Raw tm, tm'
201
239
202−data SourceLocation : Type where
240+||| A source location in an Idris file
241+record SourceLocation where
242+ ||| Either a source span or a source location. `start` and `end`
243+ ||| will be the same if it's a point location.
244+ constructor FileLoc
245+
246+ ||| The file name of the source location
203− FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
247+ filename : String
248+ ||| The line and column of the beginning of the source span
249+ start : (Int, Int)
250+ ||| The line and column of the end of the source span
251+ end : (Int, Int)
204
252
205%name SourceLocation loc
253%name SourceLocation loc
206
254
@@ -218,7 +266,7 @@ data ErrorReportPart =
218 SubReport (List ErrorReportPart)
266 SubReport (List ErrorReportPart)
219%name ErrorReportPart part, p
267%name ErrorReportPart part, p
220
268
221−||| A representation of Idris's tactics that can be returned from custom
269+||| A representation of Idris's old tactics that can be returned from custom
222||| tactic implementations. Generate these using `applyTactic`.
270||| tactic implementations. Generate these using `applyTactic`.
223data Tactic =
271data Tactic =
224 ||| Try the first tactic and resort to the second one on failure
272 ||| Try the first tactic and resort to the second one on failure
@@ -277,6 +325,7 @@ data Tactic =
277 Fail (List ErrorReportPart) |
325 Fail (List ErrorReportPart) |
278 ||| Attempt to fill the hole with source code information
326 ||| Attempt to fill the hole with source code information
279 SourceFC
327 SourceFC
328+
280%name Tactic tac, tac'
329%name Tactic tac, tac'
281
330
282
331
@@ -564,8 +613,6 @@ mutual
564 ~(assert_total (quote k)))
613 ~(assert_total (quote k)))
565 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
614 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
566 ~(assert_total (quote y)))
615 ~(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)))
616 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
570 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
617 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
571 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
618 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
@@ -586,7 +633,6 @@ mutual
586 quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))
633 quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))
587 quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))
634 quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))
588 quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
635 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))
636 quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x))
591 quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))
637 quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))
592 quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
638 quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
@@ -614,7 +660,6 @@ mutual
614 quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))
660 quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))
615 quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))
661 quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))
616 quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
662 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))
663 quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x))
619 quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))
664 quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))
620 quoteRawBinderRaw (Guess x y) = `(Guess {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
665 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') =
48 alphaEqualBinders subst (Let tm1 tm2) (Let tm1' tm2') =
49 alphaEqual subst tm1 tm1' &&
49 alphaEqual subst tm1 tm1' &&
50 alphaEqual subst tm2 tm2'
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
63getBinderTy (Lam t) = t
64getBinderTy (Pi t _) = t
64getBinderTy (Pi t _) = t
65getBinderTy (Let 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
810-- the types of bindings (and their values, if any); the attached identifiers are part
811-- of the 'Bind' constructor for the 'TT' type.
811-- of the 'Bind' constructor for the 'TT' type.
812data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
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)
310 | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
311reifyTTBinderApp reif f [x, y]
311reifyTTBinderApp reif f [x, y]
312 | f == reflm "Let" = liftM2 Let (reif x) (reif 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)