git.iko.soy/Idris-dev
on 0337afe help sign in
Idris-dev/libs/base/Language/Reflection.idr
215 lines 6.3 kB history raw
1module Language.Reflection
3%access public
5data TTName = UN String
6 -- ^ User-provided name
7 | NS TTName (List String)
8 -- ^ Root, namespaces
9 | MN Int String
10 -- ^ Machine chosen names
11 | NErased
12 -- ^ Name of somethng which is never used in scope
13%name TTName n, n'
15implicit
16userSuppliedName : String -> TTName
17userSuppliedName = UN
19data TTUExp = UVar Int
20 -- ^ universe variable
21 | UVal Int
22 -- ^ explicit universe variable
23%name TTUExp uexp
25||| Primitive constants
26data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
27 | IType | BIType | FlType | ChType | StrType
28 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
29 | B8Type | B16Type | B32Type | B64Type
30 | PtrType | VoidType | Forgot
32%name Const c, c'
34abstract class ReflConst (a : Type) where
35 toConst : a -> Const
37instance ReflConst Int where
38 toConst x = I x
40instance ReflConst Integer where
41 toConst = BI
43instance ReflConst Float where
44 toConst = Fl
46instance ReflConst Char where
47 toConst = Ch
49instance ReflConst String where
50 toConst = Str
52instance ReflConst Bits8 where
53 toConst = B8
55instance ReflConst Bits16 where
56 toConst = B16
58instance ReflConst Bits32 where
59 toConst = B32
61instance ReflConst Bits64 where
62 toConst = B64
64implicit
65reflectConstant: (ReflConst a) => a -> Const
66reflectConstant = toConst
69||| Types of named references
70data NameType = Bound
71 -- ^ reference which is just bound, e.g. by intro
72 | Ref
73 -- ^ reference to a variable
74 | DCon Int Int
75 -- ^ constructor with tag and number
76 | TCon Int Int
77 -- ^ type constructor with tag and number
78%name NameType nt, nt'
80||| Types annotations for bound variables in different
81||| binding contexts
82data Binder a = Lam a
83 | Pi a
84 | Let a a
85 | NLet a a
86 | Hole a
87 | GHole a
88 | Guess a a
89 | PVar a
90 | PVTy a
91%name Binder b, b'
93instance Functor Binder where
94 map f (Lam x) = Lam (f x)
95 map f (Pi x) = Pi (f x)
96 map f (Let x y) = Let (f x) (f y)
97 map f (NLet x y) = NLet (f x) (f y)
98 map f (Hole x) = Hole (f x)
99 map f (GHole x) = GHole (f x)
100 map f (Guess x y) = Guess (f x) (f y)
101 map f (PVar x) = PVar (f x)
102 map f (PVTy x) = PVTy (f x)
104instance Foldable Binder where
105 foldr f z (Lam x) = f x z
106 foldr f z (Pi x) = f x z
107 foldr f z (Let x y) = f x (f y z)
108 foldr f z (NLet x y) = f x (f y z)
109 foldr f z (Hole x) = f x z
110 foldr f z (GHole x) = f x z
111 foldr f z (Guess x y) = f x (f y z)
112 foldr f z (PVar x) = f x z
113 foldr f z (PVTy x) = f x z
115instance Traversable Binder where
116 traverse f (Lam x) = [| Lam (f x) |]
117 traverse f (Pi x) = [| Pi (f x) |]
118 traverse f (Let x y) = [| Let (f x) (f y) |]
119 traverse f (NLet x y) = [| NLet (f x) (f y) |]
120 traverse f (Hole x) = [| Hole (f x) |]
121 traverse f (GHole x) = [| GHole (f x) |]
122 traverse f (Guess x y) = [| Guess (f x) (f y) |]
123 traverse f (PVar x) = [| PVar (f x) |]
124 traverse f (PVTy x) = [| PVTy (f x) |]
127||| Reflection of the well typed core language
128data TT = P NameType TTName TT
129 -- ^ named binders
130 | V Int
131 -- ^ variables
132 | Bind TTName (Binder TT) TT
133 -- ^ type annotated named bindings
134 | App TT TT
135 -- ^ (named) application of a function to a value
136 | TConst Const
137 -- ^ constants
138 | Proj TT Int
139 -- ^ argument projection; runtime only
140 | Erased
141 -- ^ erased terms
142 | Impossible
143 -- ^ impossible terms
144 | TType TTUExp
145 -- ^ types
147%name TT tm, tm'
149||| Raw terms without types
150data Raw = Var TTName
151 | RBind TTName (Binder Raw) Raw
152 | RApp Raw Raw
153 | RType
154 | RForce Raw
155 | RConstant Const
157%name Raw tm, tm'
159||| Error reports are a list of report parts
160data ErrorReportPart = TextPart String
161 | NamePart TTName
162 | TermPart TT
163 | SubReport (List ErrorReportPart)
164%name ErrorReportPart part, p
166data Tactic = Try Tactic Tactic
167 -- ^ try the first tactic and resort to the second one on failure
168 | GoalType String Tactic
169 -- ^ only run if the goal has the right type
170 | Refine TTName
171 -- ^ resolve function name, find matching arguments in the
172 -- context and compute the proof target
173 | Seq Tactic Tactic
174 -- ^ apply both tactics in sequence
175 | Trivial
176 -- ^ intelligently construct the proof target from the context
177 | Search Int
178 -- ^ build a proof by applying contructors up to a maximum depth
179 | Instance
180 -- ^ resolve a type class
181 | Solve
182 -- ^ infer the proof target from the context
183 | Intros
184 -- ^ introduce all variables into the context
185 | Intro TTName
186 -- ^ introduce a named variable into the context, use the
187 -- first one if the given name is not found
188 | ApplyTactic TT
189 -- ^ invoke the reflected rep. of another tactic
190 | Reflect TT
191 -- ^ turn a value into its reflected representation
192 | ByReflection TT
193 -- ^ use a %reflection function
194 | Fill Raw
195 -- ^ turn a raw value back into a term
196 | Exact TT
197 -- ^ use the given value to conclude the proof
198 | Focus TTName
199 -- ^ focus a named hole
200 | Rewrite TT
201 -- ^ rewrite using the reflected rep. of a equality proof
202 | Induction TT
203 -- ^ do induction on the particular expression
204 | Case TT
205 -- ^ do case analysis on particular expression
206 | LetTac TTName TT
207 -- ^ name a reflected term
208 | LetTacTy TTName TT TT
209 -- ^ name a reflected term and type it
210 | Compute
211 -- ^ normalise the context
212 | Skip
213 -- ^ do nothing
214 | Fail (List ErrorReportPart)
215%name Tactic tac, tac'