1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(* $Id$ *)
(*i*)
open Util
open Names
(*i*)
(* \label{generic_terms} A generic notion of terms with binders,
over any kind of operators.
[DLAM] is a de Bruijn binder on one term, and [DLAMV] on many terms.
[VAR] is used for named variables and [Rel] for variables as
de Bruijn indices. *)
type 'oper term =
| DOP0 of 'oper
| DOP1 of 'oper * 'oper term
| DOP2 of 'oper * 'oper term * 'oper term
| DOPN of 'oper * 'oper term array
| DOPL of 'oper * 'oper term list
| DLAM of name * 'oper term
| DLAMV of name * 'oper term array
| VAR of identifier
| Rel of int
val free_rels : 'a term -> Intset.t
(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
val closed0 : 'a term -> bool
(* [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
val noccurn : int -> 'a term -> bool
(* [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
for n <= p < n+m *)
val noccur_between : int -> int -> 'a term -> bool
(* [liftn n k c] lifts by [n] indexes above [k] in [c] *)
val liftn : int -> int -> 'a term -> 'a term
(* [lift n c] lifts by [n] the positive indexes in [c] *)
val lift : int -> 'a term -> 'a term
(* [pop c] lifts by -1 the positive indexes in [c] *)
val pop : 'a term -> 'a term
(* [lift_context n ctxt] lifts terms in [ctxt] by [n] preserving
(i.e. not lifting) the internal references between terms of [ctxt];
more recent terms come first in [ctxt] *)
val lift_context : int -> (name * 'a term) list -> (name * 'a term) list
(* [substnl [a1;...;an] k c] substitutes in parallele [a1],...,[an]
for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
accordingly indexes in [a1],...,[an] *)
val substnl : 'a term list -> int -> 'a term -> 'a term
val substl : 'a term list -> 'a term -> 'a term
val subst1 : 'a term -> 'a term -> 'a term
(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
val global_vars : 'a term -> identifier list
val global_vars_set : 'a term -> Idset.t
val subst_var : identifier -> 'a term -> 'a term
val replace_vars : (identifier * 'a term) list -> 'a term -> 'a term
(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
val rel_vect : int -> int -> 'a term array
val rel_list : int -> int -> 'a term list
(*i************************************************************************i*)
(*i Pour Closure *)
(* Explicit substitutions of type ['a]. [ESID] = identity.
[CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] =
$(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars.
[LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
type 'a subs =
| ESID
| CONS of 'a * 'a subs
| SHIFT of int * 'a subs
| LIFT of int * 'a subs
val subs_cons : 'a * 'a subs -> 'a subs
val subs_lift : 'a subs -> 'a subs
val subs_shft : int * 'a subs -> 'a subs
val expand_rel : int -> 'a subs -> (int * 'a, int) union
(*
val exp_rel : int -> int -> 'a subs -> (int * 'a, int) union
*)
(*i*)
(*i Pour Closure *)
(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l].
[ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
type lift_spec =
| ELID
| ELSHFT of lift_spec * int
| ELLFT of int * lift_spec
val el_shft : int -> lift_spec -> lift_spec
val el_lift : lift_spec -> lift_spec
val reloc_rel: int -> lift_spec -> int
(*
val exliftn : lift_spec -> 'a term -> 'a term
val el_liftn : int -> lift_spec -> lift_spec
*)
(*i*)
(*i À virer...
exception FreeVar
val closedn : int -> 'a term -> unit
exception Occur
type info = Closed | Open | Unknown
val global_varsl : identifier list -> 'a term -> identifier list
val subst_varn : identifier -> int -> 'a term -> 'a term
val sAPP : 'a term -> 'a term -> 'a term
val sAPPV : 'a term -> 'a term -> 'a term array
val sAPPVi : int -> 'a term -> 'a term -> 'a term
val sAPPList : 'a term -> 'a term list -> 'a term
val sAPPVList : 'a term -> 'a term list-> 'a term array
val sAPPViList : int -> 'a term -> 'a term list -> 'a term
val under_dlams : ('a term -> 'a term) -> 'a term -> 'a term
val put_DLAMSV : name list -> 'a term array -> 'a term
val decomp_DLAMV : int -> 'a term -> 'a term array
val decomp_DLAMV_name : int -> 'a term -> name list * 'a term array
val decomp_all_DLAMV_name : 'a term -> name list * 'a term array
val put_DLAMSV_subst : identifier list -> 'a term array -> 'a term
val count_dlam : 'a term -> int
(*s For hash-consing. (déplacé dans term) *)
val hash_term :
('a term -> 'a term)
* (('a -> 'a) * (name -> name) * (identifier -> identifier))
-> 'a term -> 'a term
val comp_term : 'a term -> 'a term -> bool
i*)
|
