blob: 6825c3978b81ebb8d3be546bb61e5fac9d97d08f (
plain)
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
|
(* $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 isRel : 'a term -> bool
val isVAR : 'a term -> bool
val free_rels : 'a term -> Intset.t
exception FreeVar
exception Occur
val closedn : int -> 'a term -> unit
val closed0 : 'a term -> bool
val noccurn : int -> 'a term -> bool
val noccur_bet : int -> int -> 'a term -> bool
(*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 el_liftn : int -> lift_spec -> lift_spec
val reloc_rel: int -> lift_spec -> int
val exliftn : lift_spec -> 'a term -> 'a term
val liftn : int -> int -> 'a term -> 'a term
val lift : int -> 'a term -> 'a term
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
(*s 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 exp_rel : int -> int -> 'a subs -> (int * 'a, int) union
val expand_rel : int -> 'a subs -> (int * 'a, int) union
type info = Closed | Open | Unknown
type 'a substituend = { mutable sinfo : info; sit : 'a }
val lift_substituend : int -> 'a term substituend -> 'a term
val make_substituend : 'a term -> 'a term substituend
val substn_many : 'a term substituend array -> int -> 'a term -> 'a term
val substl : 'a term list -> 'a term -> 'a term
val subst1 : 'a term -> 'a term -> 'a term
val occur_opern : 'a -> 'a term -> bool
val occur_oper0 : 'a -> 'a term -> bool
val occur_var : identifier -> 'a term -> bool
val occur_oper : 'a -> 'a term -> bool
val process_opers_of_term :
('a -> bool) -> ('a -> 'b) -> 'b list -> 'a term -> 'b list
val dependent : 'a term -> 'a term -> bool
val global_varsl : identifier list -> 'a term -> identifier list
val global_vars : 'a term -> identifier list
val global_vars_set : 'a term -> Idset.t
val subst_var : identifier -> 'a term -> 'a term
val subst_varn : identifier -> int -> 'a term -> 'a term
val replace_vars :
(identifier * 'a term substituend) list -> 'a term -> 'a term
val rename_diff_occ :
identifier -> identifier list ->'a term -> identifier list * '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 eq_term : 'a term -> 'a term -> bool
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 rel_vect : int -> int -> 'a term array
val rel_list : int -> int -> 'a term list
val count_dlam : 'a term -> int
(*s For hash-consing. *)
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
|
