blob: dcd458f8b8a185aed1c25480e0d2d660fe3399fa (
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
|
(* $Id$ *)
(*i*)
open Util
open Names
(*i*)
(* A generic notion of terms with binders. *)
exception FreeVar
exception Occur
(* \label{generic_terms}
Generic terms, over any kind of operators. *)
type 'oper term =
| DOP0 of 'oper (* atomic terms *)
| DOP1 of 'oper * 'oper term (* operator of arity 1 *)
| DOP2 of 'oper * 'oper term * 'oper term (* operator of arity 2 *)
| DOPN of 'oper * 'oper term array (* operator of variadic arity *)
| DOPL of 'oper * 'oper term list (* operator of variadic arity *)
| DLAM of name * 'oper term (* deBruijn binder on one term*)
| DLAMV of name * 'oper term array (* deBruijn binder on many terms*)
| VAR of identifier (* named variable *)
| Rel of int (* variable as deBruijn index *)
val isRel : 'a term -> bool
val isVAR : 'a term -> bool
val free_rels : 'a term -> Intset.t
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
(* lifts *)
type lift_spec =
| ELID
| ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
| ELLFT of int * lift_spec (* ELLFT(n,l) == apply l to de Bruijn > n *)
(* i.e under n binders *)
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
(* explicit substitutions of type 'a *)
type 'a subs =
| ESID (* ESID = identity *)
| CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *)
| SHIFT of int * 'a subs (* SHIFT(n,S)= (\^n o S) terms in S are relocated *)
(* with n vars *)
| LIFT of int * 'a subs (* LIFT(n,S)=(\%n S) stands for ((\^n o S).n...1) *)
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 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
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 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
type modification_action = ABSTRACT | ERASE
type 'a modification =
| NOT_OCCUR
| DO_ABSTRACT of 'a * modification_action list
| DO_REPLACE
val modify_opers : ('a term -> 'a term) -> ('a term -> 'a term -> 'a term)
-> ('a * 'a modification) list -> '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 rel_vect : int -> int -> 'a term array
val rel_list : int -> int -> 'a term list
val count_dlam : 'a term -> int
(* For hash-consing use *)
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
|
