git.iko.soy/Idris-dev
on 307efbb help sign in
Idris-dev/libs/base/Language/Reflection.idr
197 lines 5.6 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 Nat | 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 Nat 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'
159data Tactic = Try Tactic Tactic
160 -- ^ try the first tactic and resort to the second one on failure
161 | GoalType String Tactic
162 -- ^ only run if the goal has the right type
163 | Refine TTName
164 -- ^ resolve function name, find matching arguments in the
165 -- context and compute the proof target
166 | Seq Tactic Tactic
167 -- ^ apply both tactics in sequence
168 | Trivial
169 -- ^ intelligently construct the proof target from the context
170 | Solve
171 -- ^ infer the proof target from the context
172 | Intros
173 -- ^ introduce all variables into the context
174 | Intro TTName
175 -- ^ introduce a named variable into the context, use the
176 -- first one if the given name is not found
177 | ApplyTactic TT
178 -- ^ invoke the reflected rep. of another tactic
179 | Reflect TT
180 -- ^ turn a value into its reflected representation
181 | Fill Raw
182 -- ^ turn a raw value back into a term
183 | Exact TT
184 -- ^ use the given value to conclude the proof
185 | Focus TTName
186 -- ^ focus a named hole
187 | Rewrite TT
188 -- ^ rewrite using the reflected rep. of a equality proof
189 | Induction TTName
190 -- ^ do induction on the particular expression
191 | LetTac TTName TT
192 -- ^ name a reflected term
193 | LetTacTy TTName TT TT
194 -- ^ name a reflected term and type it
195 | Compute
196 -- ^ normalise the context
197%name Tactic tac, tac'