git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2702 from david-christiansen/reflection-simplification

Reflection simplification

commit13045109d058b248a2fc69c786a969b9d14f4b85 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 7 Oct 2015, 18:18 (11 years ago) parent01e51f1cc9cac4
6 files changed+89−37
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr−3 libs/prelude/Language/Reflection.idr+65−20 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+65−20
@@ -116,22 +116,62 @@ data NameType =
116116
117117||| Types annotations for bound variables in different
118118||| binding contexts
119−data Binder a = Lam a
120− | Pi a a
121− | Let a a
122− | NLet a a
123− | Hole a
124− | GHole a
125− | Guess a a
126− | PVar a
127− | PVTy a
119+|||
120+||| @ tmTy the terms that can occur inside the binder, as type
121+||| annotations or bound values
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.
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
140+ Let : (ty, val : a) -> Binder 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
145+ Hole : (ty : a) -> Binder a
146+
147+ ||| A hole that will later become a top-level metavariable
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
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
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
167+ PVTy : (ty : a) -> Binder a
168+
128169%name Binder b, b'
129170
130171instance Functor Binder where
131172 map f (Lam x) = Lam (f x)
132173 map f (Pi x k) = Pi (f x) (f k)
133174 map f (Let x y) = Let (f x) (f y)
134− map f (NLet x y) = NLet (f x) (f y)
135175 map f (Hole x) = Hole (f x)
136176 map f (GHole x) = GHole (f x)
137177 map f (Guess x y) = Guess (f x) (f y)
@@ -142,7 +182,6 @@ instance Foldable Binder where
142182 foldr f z (Lam x) = f x z
143183 foldr f z (Pi x k) = f x (f k z)
144184 foldr f z (Let x y) = f x (f y z)
145− foldr f z (NLet x y) = f x (f y z)
146185 foldr f z (Hole x) = f x z
147186 foldr f z (GHole x) = f x z
148187 foldr f z (Guess x y) = f x (f y z)
@@ -153,14 +192,13 @@ instance Traversable Binder where
153192 traverse f (Lam x) = [| Lam (f x) |]
154193 traverse f (Pi x k) = [| Pi (f x) (f k) |]
155194 traverse f (Let x y) = [| Let (f x) (f y) |]
156− traverse f (NLet x y) = [| NLet (f x) (f y) |]
157195 traverse f (Hole x) = [| Hole (f x) |]
158196 traverse f (GHole x) = [| GHole (f x) |]
159197 traverse f (Guess x y) = [| Guess (f x) (f y) |]
160198 traverse f (PVar x) = [| PVar (f x) |]
161199 traverse f (PVTy x) = [| PVTy (f x) |]
162200
163−||| Universes
201+||| The various universes involved in the uniqueness mechanism
164202data Universe = NullType | UniqueType | AllTypes
165203
166204||| Reflection of the well typed core language
@@ -199,8 +237,18 @@ data Raw =
199237 RConstant Const
200238%name Raw tm, tm'
201239
202−data SourceLocation : Type where
203− FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
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
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)
204252
205253%name SourceLocation loc
206254
@@ -218,7 +266,7 @@ data ErrorReportPart =
218266 SubReport (List ErrorReportPart)
219267%name ErrorReportPart part, p
220268
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
222270||| tactic implementations. Generate these using `applyTactic`.
223271data Tactic =
224272 ||| Try the first tactic and resort to the second one on failure
@@ -277,6 +325,7 @@ data Tactic =
277325 Fail (List ErrorReportPart) |
278326 ||| Attempt to fill the hole with source code information
279327 SourceFC
328+
280329%name Tactic tac, tac'
281330
282331
@@ -564,8 +613,6 @@ mutual
564613 ~(assert_total (quote k)))
565614 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
566615 ~(assert_total (quote y)))
567− quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))
568− ~(assert_total (quote y)))
569616 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
570617 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
571618 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
@@ -586,7 +633,6 @@ mutual
586633 quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))
587634 quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))
588635 quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
589− quoteRawBinderTT (NLet x y) = `(NLet {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
590636 quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x))
591637 quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))
592638 quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
@@ -614,7 +660,6 @@ mutual
614660 quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))
615661 quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))
616662 quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
617− quoteRawBinderRaw (NLet x y) = `(NLet {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
618663 quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x))
619664 quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))
620665 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)