1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: rawterm.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
21
(* Untyped intermediate terms, after ASTs and before constr. *)
23
(* locs here refers to the ident's location, not whole pat *)
24
(* the last argument of PatCstr is a possible alias ident for the pattern *)
26
| PatVar of loc * name
27
| PatCstr of loc * constructor * cases_pattern list * name
29
let cases_pattern_loc = function
31
| PatCstr(loc,_,_,_) -> loc
33
type patvar = identifier
35
type rawsort = RProp of Term.contents | RType of Univ.universe option
37
type binder_kind = BProd | BLambda | BLetIn
39
type binding_kind = Lib.binding_kind = Explicit | Implicit
41
type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
43
type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
46
| ImplicitBindings of 'a list
47
| ExplicitBindings of 'a explicit_bindings
50
type 'a with_bindings = 'a * 'a bindings
53
| CastConv of cast_kind * 'a
54
| CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
57
| RRef of (loc * global_reference)
58
| RVar of (loc * identifier)
59
| REvar of loc * existential_key * rawconstr list option
60
| RPatVar of loc * (bool * patvar) (* Used for patterns only *)
61
| RApp of loc * rawconstr * rawconstr list
62
| RLambda of loc * name * binding_kind * rawconstr * rawconstr
63
| RProd of loc * name * binding_kind * rawconstr * rawconstr
64
| RLetIn of loc * name * rawconstr * rawconstr
65
| RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
66
| RLetTuple of loc * name list * (name * rawconstr option) *
68
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
69
| RRec of loc * fix_kind * identifier array * rawdecl list array *
70
rawconstr array * rawconstr array
71
| RSort of loc * rawsort
72
| RHole of (loc * hole_kind)
73
| RCast of loc * rawconstr * rawconstr cast_type
74
| RDynamic of loc * Dyn.t
76
and rawdecl = name * binding_kind * rawconstr option * rawconstr
78
and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
81
| RFix of ((int option * fix_recursion_order) array * int)
84
and predicate_pattern =
85
name * (loc * inductive * int * name list) option
87
and tomatch_tuple = (rawconstr * predicate_pattern)
89
and tomatch_tuples = tomatch_tuple list
91
and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
93
and cases_clauses = cases_clause list
95
let cases_predicate_names tml =
96
List.flatten (List.map (function
97
| (tm,(na,None)) -> [na]
98
| (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
100
(*i - if PRec (_, names, arities, bodies) is in env then arities are
101
typed in env too and bodies are typed in env enriched by the
102
arities incrementally lifted
104
[On pourrait plutot mettre les arit�s aves le type qu'elles auront
105
dans le contexte servant � typer les body ???]
107
- boolean in POldCase means it is recursive
109
let map_rawdecl f (na,k,obd,ty) = (na,k,Option.map f obd,f ty)
111
let map_rawconstr f = function
112
| RVar (loc,id) -> RVar (loc,id)
113
| RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
114
| RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
115
| RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
116
| RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
117
| RCases (loc,sty,rtntypopt,tml,pl) ->
118
RCases (loc,sty,Option.map f rtntypopt,
119
List.map (fun (tm,x) -> (f tm,x)) tml,
120
List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
121
| RLetTuple (loc,nal,(na,po),b,c) ->
122
RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
123
| RIf (loc,c,(na,po),b1,b2) ->
124
RIf (loc,f c,(na,Option.map f po),f b1,f b2)
125
| RRec (loc,fk,idl,bl,tyl,bv) ->
126
RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
127
Array.map f tyl,Array.map f bv)
128
| RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x)
129
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
133
let name_app f e = function
134
| Name id -> let (id, e) = f id e in (Name id, e)
135
| Anonymous -> Anonymous, e
137
let fold_ident g idl e =
140
(fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e)
141
in (Array.of_list idl,e)
143
let map_rawconstr_with_binders_loc loc g f e = function
144
| RVar (_,id) -> RVar (loc,id)
145
| RApp (_,a,args) -> RApp (loc,f e a, List.map (f e) args)
146
| RLambda (_,na,ty,c) ->
147
let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
148
| RProd (_,na,ty,c) ->
149
let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
150
| RLetIn (_,na,b,c) ->
151
let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
152
| RCases (_,tyopt,tml,pl) ->
153
(* We don't modify pattern variable since we don't traverse patterns *)
154
let g' id e = snd (g id e) in
155
let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
157
(loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl)
158
| RRec (_,fk,idl,tyl,bv) ->
159
let idl',e' = fold_ident g idl e in
160
RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
161
| RCast (_,c,t) -> RCast (loc,f e c,f e t)
162
| RSort (_,x) -> RSort (loc,x)
163
| RHole (_,x) -> RHole (loc,x)
164
| RRef (_,x) -> RRef (loc,x)
165
| REvar (_,x,l) -> REvar (loc,x,l)
166
| RPatVar (_,x) -> RPatVar (loc,x)
167
| RDynamic (_,x) -> RDynamic (loc,x)
170
let occur_rawconstr id =
171
let rec occur = function
172
| RVar (loc,id') -> id = id'
173
| RApp (loc,f,args) -> (occur f) or (List.exists occur args)
174
| RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
175
| RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
176
| RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
177
| RCases (loc,sty,rtntypopt,tml,pl) ->
178
(occur_option rtntypopt)
179
or (List.exists (fun (tm,_) -> occur tm) tml)
180
or (List.exists occur_pattern pl)
181
| RLetTuple (loc,nal,rtntyp,b,c) ->
182
occur_return_type rtntyp id
183
or (occur b) or (not (List.mem (Name id) nal) & (occur c))
184
| RIf (loc,c,rtntyp,b1,b2) ->
185
occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
186
| RRec (loc,fk,idl,bl,tyl,bv) ->
187
not (array_for_all4 (fun fid bl ty bd ->
188
let rec occur_fix = function
189
[] -> not (occur ty) && (fid=id or not(occur bd))
190
| (na,k,bbd,bty)::bl ->
193
Some bd -> not (occur bd)
195
(na=Name id or not(occur_fix bl)) in
198
| RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
199
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
201
and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
203
and occur_option = function None -> false | Some p -> occur p
205
and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt
210
let add_name_to_ids set na =
213
| Name id -> Idset.add id set
216
let rec vars bounded vs = function
217
| RVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
218
| RApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
219
| RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
220
let vs' = vars bounded vs ty in
221
let bounded' = add_name_to_ids bounded na in
223
| RCases (loc,sty,rtntypopt,tml,pl) ->
224
let vs1 = vars_option bounded vs rtntypopt in
225
let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
226
List.fold_left (vars_pattern bounded) vs2 pl
227
| RLetTuple (loc,nal,rtntyp,b,c) ->
228
let vs1 = vars_return_type bounded vs rtntyp in
229
let vs2 = vars bounded vs1 b in
230
let bounded' = List.fold_left add_name_to_ids bounded nal in
232
| RIf (loc,c,rtntyp,b1,b2) ->
233
let vs1 = vars_return_type bounded vs rtntyp in
234
let vs2 = vars bounded vs1 c in
235
let vs3 = vars bounded vs2 b1 in
237
| RRec (loc,fk,idl,bl,tyl,bv) ->
238
let bounded' = Array.fold_right Idset.add idl bounded in
239
let vars_fix i vs fid =
242
(fun (vs,bounded) (na,k,bbd,bty) ->
243
let vs' = vars_option bounded vs bbd in
244
let vs'' = vars bounded vs' bty in
245
let bounded' = add_name_to_ids bounded na in
251
let vs2 = vars bounded1 vs1 tyl.(i) in
252
vars bounded1 vs2 bv.(i)
254
array_fold_left_i vars_fix vs idl
255
| RCast (loc,c,k) -> let v = vars bounded vs c in
256
(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
257
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
259
and vars_pattern bounded vs (loc,idl,p,c) =
260
let bounded' = List.fold_right Idset.add idl bounded in
263
and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
265
and vars_return_type bounded vs (na,tyopt) =
266
let bounded' = add_name_to_ids bounded na in
267
vars_option bounded' vs tyopt
270
let vs = vars Idset.empty Idset.empty rt in
274
let loc_of_rawconstr = function
275
| RRef (loc,_) -> loc
276
| RVar (loc,_) -> loc
277
| REvar (loc,_,_) -> loc
278
| RPatVar (loc,_) -> loc
279
| RApp (loc,_,_) -> loc
280
| RLambda (loc,_,_,_,_) -> loc
281
| RProd (loc,_,_,_,_) -> loc
282
| RLetIn (loc,_,_,_) -> loc
283
| RCases (loc,_,_,_,_) -> loc
284
| RLetTuple (loc,_,_,_,_) -> loc
285
| RIf (loc,_,_,_,_) -> loc
286
| RRec (loc,_,_,_,_,_) -> loc
287
| RSort (loc,_) -> loc
288
| RHole (loc,_) -> loc
289
| RCast (loc,_,_) -> loc
290
| RDynamic (loc,_) -> loc
292
(**********************************************************************)
293
(* Conversion from rawconstr to cases pattern, if possible *)
295
let rec cases_pattern_of_rawconstr na = function
296
| RVar (loc,id) when na<>Anonymous ->
297
(* Unable to manage the presence of both an alias and a variable *)
299
| RVar (loc,id) -> PatVar (loc,Name id)
300
| RHole (loc,_) -> PatVar (loc,na)
301
| RRef (loc,ConstructRef cstr) ->
302
PatCstr (loc,cstr,[],na)
303
| RApp (loc,RRef (_,ConstructRef cstr),l) ->
304
PatCstr (loc,cstr,List.map (cases_pattern_of_rawconstr Anonymous) l,na)
305
| _ -> raise Not_found
307
(* Turn a closed cases pattern into a rawconstr *)
308
let rec rawconstr_of_closed_cases_pattern_aux = function
309
| PatCstr (loc,cstr,[],Anonymous) ->
310
RRef (loc,ConstructRef cstr)
311
| PatCstr (loc,cstr,l,Anonymous) ->
312
let ref = RRef (loc,ConstructRef cstr) in
313
RApp (loc,ref, List.map rawconstr_of_closed_cases_pattern_aux l)
314
| _ -> raise Not_found
316
let rawconstr_of_closed_cases_pattern = function
317
| PatCstr (loc,cstr,l,na) ->
318
na,rawconstr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
322
(**********************************************************************)
323
(* Reduction expressions *)
325
type 'a raw_red_flag = {
329
rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
334
{rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
336
type 'a or_var = ArgArg of 'a | ArgVar of identifier located
338
type occurrences_expr = bool * int or_var list
340
let all_occurrences_expr_but l = (false,l)
341
let no_occurrences_expr_but l = (true,l)
342
let all_occurrences_expr = (false,[])
343
let no_occurrences_expr = (true,[])
345
type 'a with_occurrences = occurrences_expr * 'a
347
type ('a,'b) red_expr_gen =
350
| Simpl of 'a with_occurrences option
351
| Cbv of 'b raw_red_flag
352
| Lazy of 'b raw_red_flag
353
| Unfold of 'b with_occurrences list
355
| Pattern of 'a with_occurrences list
356
| ExtraRedExpr of string
359
type ('a,'b) may_eval =
361
| ConstrEval of ('a,'b) red_expr_gen * 'a
362
| ConstrContext of (loc * identifier) * 'a
added
removed
pretyping/rawterm.ml
