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: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
11
(* This module instantiates the structure of generic deBruijn terms to Coq *)
20
(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
22
type existential_key = int
23
type metavariable = int
25
(* This defines the strategy to use for verifiying a Cast *)
27
(* This defines Cases annotations *)
28
type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle |
31
{ ind_nargs : int; (* number of real args of the inductive type *)
36
ci_cstr_nargs : int array; (* number of real args of each constructor *)
37
ci_pp_info : case_printing (* not interpreted by the kernel *)
40
let val_cstyle = val_enum "case_style" 5 in
41
let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
42
val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
46
type contents = Pos | Null
49
| Prop of contents (* proposition types *)
52
type sorts_family = InProp | InSet | InType
54
let family_of_sort = function
59
let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
60
let val_sortfam = val_enum "sorts_family" 3
62
(********************************************************************)
63
(* Constructions as implemented *)
64
(********************************************************************)
66
(* [constr array] is an instance matching definitional [named_context] in
67
the same order (i.e. last argument first) *)
68
type 'constr pexistential = existential_key * 'constr array
69
type 'constr prec_declaration =
70
name array * 'constr array * 'constr array
71
type 'constr pfixpoint =
72
(int array * int) * 'constr prec_declaration
73
type 'constr pcofixpoint =
74
int * 'constr prec_declaration
76
let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
78
val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
81
[|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
82
let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
84
type cast_kind = VMcast | DEFAULTcast
85
let val_cast = val_enum "cast_kind" 2
87
(*s*******************************************************************)
88
(* The type of constructions *)
93
| Meta of metavariable
94
| Evar of constr pexistential
96
| Cast of constr * cast_kind * constr
97
| Prod of name * constr * constr
98
| Lambda of name * constr * constr
99
| LetIn of name * constr * constr * constr
100
| App of constr * constr array
103
| Construct of constructor
104
| Case of case_info * constr * constr * constr array
105
| Fix of constr pfixpoint
106
| CoFix of constr pcofixpoint
108
let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
109
[|val_int|]; (* Rel *)
110
[|val_id|]; (* Var *)
111
[|val_int|]; (* Meta *)
112
[|val_evar val_constr|]; (* Evar *)
113
[|val_sort|]; (* Sort *)
114
[|val_constr;val_cast;val_constr|]; (* Cast *)
115
[|val_name;val_constr;val_constr|]; (* Prod *)
116
[|val_name;val_constr;val_constr|]; (* Lambda *)
117
[|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
118
[|val_constr;val_array val_constr|]; (* App *)
119
[|val_kn|]; (* Const *)
120
[|val_ind|]; (* Ind *)
121
[|val_cstr|]; (* Construct *)
122
[|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
123
[|val_fix val_constr|]; (* Fix *)
124
[|val_cofix val_constr|] (* CoFix *)
127
type existential = constr pexistential
128
type rec_declaration = constr prec_declaration
129
type fixpoint = constr pfixpoint
130
type cofixpoint = constr pcofixpoint
133
let rec strip_outer_cast c = match c with
134
| Cast (c,_,_) -> strip_outer_cast c
137
let rec collapse_appl c = match c with
139
let rec collapse_rec f cl2 =
140
match (strip_outer_cast f) with
141
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
147
let decompose_app c =
148
match collapse_appl c with
149
| App (f,cl) -> (f, Array.to_list cl)
153
let applist (f,l) = App (f, Array.of_list l)
156
(****************************************************************************)
157
(* Functions for dealing with constr terms *)
158
(****************************************************************************)
160
(*********************)
162
(*********************)
164
let iter_constr_with_binders g f n c = match c with
165
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
167
| Cast (c,_,t) -> f n c; f n t
168
| Prod (_,t,c) -> f n t; f (g n) c
169
| Lambda (_,t,c) -> f n t; f (g n) c
170
| LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
171
| App (c,l) -> f n c; Array.iter (f n) l
172
| Evar (_,l) -> Array.iter (f n) l
173
| Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
174
| Fix (_,(_,tl,bl)) ->
176
Array.iter (f (iterate g (Array.length tl) n)) bl
177
| CoFix (_,(_,tl,bl)) ->
179
Array.iter (f (iterate g (Array.length tl) n)) bl
183
(* (closedn n M) raises FreeVar if a variable of height greater than n
184
occurs in M, returns () otherwise *)
187
let rec closed_rec n c = match c with
188
| Rel m -> if m>n then raise LocalOccur
189
| _ -> iter_constr_with_binders succ closed_rec n c
191
try closed_rec n c; true with LocalOccur -> false
193
(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
195
let closed0 = closedn 0
197
(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *)
200
let rec occur_rec n c = match c with
201
| Rel m -> if m = n then raise LocalOccur
202
| _ -> iter_constr_with_binders succ occur_rec n c
204
try occur_rec n term; true with LocalOccur -> false
206
(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
209
let noccur_between n m term =
210
let rec occur_rec n c = match c with
211
| Rel(p) -> if n<=p && p<n+m then raise LocalOccur
212
| _ -> iter_constr_with_binders succ occur_rec n c
214
try occur_rec n term; true with LocalOccur -> false
216
(* Checking function for terms containing existential variables.
217
The function [noccur_with_meta] considers the fact that
218
each existential variable (as well as each isevar)
219
in the term appears applied to its local context,
220
which may contain the CoFix variables. These occurrences of CoFix variables
221
are not considered *)
223
let noccur_with_meta n m term =
224
let rec occur_rec n c = match c with
225
| Rel p -> if n<=p & p<n+m then raise LocalOccur
228
| (Cast (Meta _,_,_)| Meta _) -> ()
229
| _ -> iter_constr_with_binders succ occur_rec n c)
231
| _ -> iter_constr_with_binders succ occur_rec n c
233
try (occur_rec n term; true) with LocalOccur -> false
236
(*********************)
238
(*********************)
240
let map_constr_with_binders g f l c = match c with
241
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
243
| Cast (c,k,t) -> Cast (f l c, k, f l t)
244
| Prod (na,t,c) -> Prod (na, f l t, f (g l) c)
245
| Lambda (na,t,c) -> Lambda (na, f l t, f (g l) c)
246
| LetIn (na,b,t,c) -> LetIn (na, f l b, f l t, f (g l) c)
247
| App (c,al) -> App (f l c, Array.map (f l) al)
248
| Evar (e,al) -> Evar (e, Array.map (f l) al)
249
| Case (ci,p,c,bl) -> Case (ci, f l p, f l c, Array.map (f l) bl)
250
| Fix (ln,(lna,tl,bl)) ->
251
let l' = iterate g (Array.length tl) l in
252
Fix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
253
| CoFix(ln,(lna,tl,bl)) ->
254
let l' = iterate g (Array.length tl) l in
255
CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
257
(* The generic lifting function *)
258
let rec exliftn el c = match c with
259
| Rel i -> Rel(reloc_rel i el)
260
| _ -> map_constr_with_binders el_lift exliftn el c
262
(* Lifting the binding depth across k bindings *)
265
match el_liftn (pred n) (el_shft k ELID) with
266
| ELID -> (fun c -> c)
269
let lift k = liftn k 1
271
(*********************)
273
(*********************)
275
(* (subst1 M c) substitutes M for Rel(1) in c
276
we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel
277
M1,...,Mn for respectively Rel(1),...,Rel(n) in c *)
279
(* 1st : general case *)
280
type info = Closed | Open | Unknown
281
type 'a substituend = { mutable sinfo: info; sit: 'a }
283
let rec lift_substituend depth s =
286
| Open -> lift depth s.sit
288
s.sinfo <- if closed0 s.sit then Closed else Open;
289
lift_substituend depth s
291
let make_substituend c = { sinfo=Unknown; sit=c }
293
let substn_many lamv n c =
294
let lv = Array.length lamv in
297
let rec substrec depth c = match c with
300
else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
302
| _ -> map_constr_with_binders succ substrec depth c in
306
substn_many (Array.map make_substituend (Array.of_list laml)) n
307
let substl laml = substnl laml 0
308
let subst1 lam = substl [lam]
311
(***************************************************************************)
312
(* Type of assumptions and contexts *)
313
(***************************************************************************)
316
val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
318
val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
319
let val_nctxt = val_list val_ndecl
320
let val_rctxt = val_list val_rdecl
322
type named_declaration = identifier * constr option * constr
323
type rel_declaration = name * constr option * constr
325
let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
326
let map_rel_declaration = map_named_declaration
328
let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
329
let fold_rel_declaration = fold_named_declaration
332
type named_context = named_declaration list
333
let empty_named_context = []
334
let fold_named_context f l ~init = List.fold_right f l init
336
type section_context = named_context
338
type rel_context = rel_declaration list
339
let empty_rel_context = []
340
let rel_context_length = List.length
341
let rel_context_nhyps hyps =
342
let rec nhyps acc = function
344
| (_,None,_)::hyps -> nhyps (1+acc) hyps
345
| (_,Some _,_)::hyps -> nhyps acc hyps in
347
let fold_rel_context f l ~init = List.fold_right f l init
349
let map_context f l =
350
let map_decl (n, body_o, typ as decl) =
351
let body_o' = Option.smartmap f body_o in
353
if body_o' == body_o && typ' == typ then decl else
356
list_smartmap map_decl l
358
let map_rel_context = map_context
360
let extended_rel_list n hyps =
361
let rec reln l p = function
362
| (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
363
| (_,Some _,_) :: hyps -> reln l (p+1) hyps
368
(* Iterate lambda abstractions *)
370
(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
371
let compose_lam l b =
372
let rec lamrec = function
374
| ((v,t)::l, b) -> lamrec (l, Lambda (v,t,b))
378
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
379
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
381
let rec lamdec_rec l c = match c with
382
| Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
383
| Cast (c,_,_) -> lamdec_rec l c
388
(* Decompose lambda abstractions and lets, until finding n
390
let decompose_lam_n_assum n =
392
error "decompose_lam_n_assum: integer parameter must be positive";
393
let rec lamdec_rec l n c =
396
| Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c
397
| LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
398
| Cast (c,_,_) -> lamdec_rec l n c
399
| c -> error "decompose_lam_n_assum: not enough abstractions"
401
lamdec_rec empty_rel_context n
403
(* Iterate products, with or without lets *)
405
(* Constructs either [(x:t)c] or [[x=b:t]c] *)
406
let mkProd_or_LetIn (na,body,t) c =
408
| None -> Prod (na, t, c)
409
| Some b -> LetIn (na, b, t, c)
411
let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)
413
let decompose_prod_assum =
414
let rec prodec_rec l c =
416
| Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) c
417
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c
418
| Cast (c,_,_) -> prodec_rec l c
421
prodec_rec empty_rel_context
423
let decompose_prod_n_assum n =
425
error "decompose_prod_n_assum: integer parameter must be positive";
426
let rec prodec_rec l n c =
429
| Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c
430
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
431
| Cast (c,_,_) -> prodec_rec l n c
432
| c -> error "decompose_prod_n_assum: not enough assumptions"
434
prodec_rec empty_rel_context n
437
(***************************)
438
(* Other term constructors *)
439
(***************************)
441
type arity = rel_context * sorts
442
let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
444
let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
447
let rec prodec_rec l c =
449
| Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c
450
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
451
| Cast (c,_,_) -> prodec_rec l c
453
| _ -> anomaly "destArity: not an arity"
459
| Prod (_,_,c) -> isArity c
460
| LetIn (_,b,_,c) -> isArity (subst1 b c)
461
| Cast (c,_,_) -> isArity c
465
(*******************************)
466
(* alpha conversion functions *)
467
(*******************************)
469
(* alpha conversion : ignore print names and casts *)
471
let compare_constr f t1 t2 =
473
| Rel n1, Rel n2 -> n1 = n2
474
| Meta m1, Meta m2 -> m1 = m2
475
| Var id1, Var id2 -> id1 = id2
476
| Sort s1, Sort s2 -> s1 = s2
477
| Cast (c1,_,_), _ -> f c1 t2
478
| _, Cast (c2,_,_) -> f t1 c2
479
| Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
480
| Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
481
| LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
482
| App (c1,l1), App (c2,l2) ->
483
if Array.length l1 = Array.length l2 then
484
f c1 c2 & array_for_all2 f l1 l2
486
let (h1,l1) = decompose_app t1 in
487
let (h2,l2) = decompose_app t2 in
488
if List.length l1 = List.length l2 then
489
f h1 h2 & List.for_all2 f l1 l2
491
| Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
492
| Const c1, Const c2 -> c1 = c2
493
| Ind c1, Ind c2 -> c1 = c2
494
| Construct c1, Construct c2 -> c1 = c2
495
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
496
f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
497
| Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
498
ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
499
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
500
ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
503
let rec eq_constr m n =
505
compare_constr eq_constr m n
507
let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
added
removed
checker/term.ml
