Source file libTerm.ml
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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
(** Basic operations on terms. *)
open Term
open Lplib open Extra
(** [is_kind t] tells whether [t] is of the form Π x1, .., Π xn, TYPE. *)
let rec is_kind : term -> bool = fun t ->
match unfold t with
| Type -> true
| Prod(_,b) -> is_kind (Bindlib.subst b mk_Kind)
| _ -> false
(** [to_tvar t] returns [x] if [t] is of the form [Vari x] and fails
otherwise. *)
let to_tvar : term -> tvar = fun t ->
match t with Vari(x) -> x | _ -> assert false
(** {b NOTE} the [Array.map to_tvar] function is useful when working
with multiple binders. For example, this is the case when manipulating
pattern variables ([Patt] constructor) or metatavariables ([Meta]
constructor). Remark that it is important for these constructors to hold
an array of terms, rather than an array of variables: a variable can only
be substituted when if it is injected in a term (using the [Vari]
constructor). *)
(** {b NOTE} the result of {!val:to_tvar} can generally NOT be precomputed. A
first reason is that we cannot know in advance what variable identifier is
going to arise when working under binders, for which fresh variables will
often be generated. A second reason is that free variables should never be
“marshaled” (e.g., by the {!module:Sign} module), as this would break the
freshness invariant of new variables. *)
(** Given a symbol [s], [remove_impl_args s ts] returns the non-implicit
arguments of [s] among [ts]. *)
let remove_impl_args : sym -> term list -> term list = fun s ts ->
let rec remove bs ts =
match (bs, ts) with
| (true::bs , _::ts) -> remove bs ts
| (false::bs, t::ts) -> t :: remove bs ts
| (_ , _ ) -> ts
in
remove s.sym_impl ts
(** [iter f t] applies the function [f] to every node of the term [t] with
bound variables replaced by [Kind]. Note: [f] is called on already unfolded
terms only. *)
let iter : (term -> unit) -> term -> unit = fun action ->
let rec iter t =
let t = unfold t in
action t;
match t with
| Wild
| Plac _
| TRef(_)
| Vari(_)
| Type
| Kind
| Symb(_) -> ()
| Patt(_,_,ts)
| TEnv(_,ts)
| Meta(_,ts) -> Array.iter iter ts
| Prod(a,b)
| Abst(a,b) -> iter a; iter (Bindlib.subst b mk_Kind)
| Appl(t,u) -> iter t; iter u
| LLet(a,t,u) -> iter a; iter t; iter (Bindlib.subst u mk_Kind)
in iter
(** [unbind_name b s] is like [Bindlib.unbind b] but returns a valid variable
name when [b] binds no variable. The string [s] is the prefix of the
variable's name.*)
let unbind_name : string -> tbinder -> tvar * term = fun s b ->
if Bindlib.binder_occur b then Bindlib.unbind b
else let x = new_tvar s in (x, Bindlib.subst b (mk_Vari x))
(** [unbind2_name b1 b2 s] is like [Bindlib.unbind2 b1 b2] but returns a valid
variable name when [b1] or [b2] binds no variable. The string [s] is the
prefix of the variable's name.*)
let unbind2_name : string -> tbinder -> tbinder -> tvar * term * term =
fun s b1 b2 ->
if Bindlib.binder_occur b1 || Bindlib.binder_occur b2 then
Bindlib.unbind2 b1 b2
else let x = new_tvar s in
(x, Bindlib.subst b1 (mk_Vari x), Bindlib.subst b2 (mk_Vari x))
(** [distinct_vars ctx ts] checks that the terms [ts] are distinct
variables. If so, the variables are returned. *)
let distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts ->
let exception Not_unique_var in
let open Stdlib in
let vars = ref VarSet.empty in
let to_var t =
match Ctxt.unfold ctx t with
| Vari(x) ->
if VarSet.mem x !vars then raise Not_unique_var;
vars := VarSet.add x !vars; x
| _ -> raise Not_unique_var
in
try Some (Array.map to_var ts) with Not_unique_var -> None
(** If [ts] is not made of variables or function symbols prefixed by ['$']
only, then [nl_distinct_vars ts] returns [None]. Otherwise, it returns
a pair [(vs, map)] where [vs] is an array of variables made of the linear
variables of [ts] and fresh variables for the non-linear variables and the
symbols prefixed by ['$'], and [map] records by which variable each linear
symbol prefixed by ['$'] is replaced.
The symbols prefixed by ['$'] are introduced by [infer.ml] which converts
metavariables into fresh symbols, and those metavariables are introduced by
[sr.ml] which replaces pattern variables by metavariables. *)
let nl_distinct_vars : term array -> (tvar array * tvar StrMap.t) option =
fun ts ->
let exception Not_a_var in
let open Stdlib in
let vars = ref VarSet.empty
and nl_vars = ref VarSet.empty
and patt_vars = ref StrMap.empty in
let rec to_var t =
match unfold t with
| Vari(v) ->
if VarSet.mem v !vars then nl_vars := VarSet.add v !nl_vars
else vars := VarSet.add v !vars;
v
| Symb(f) when f.sym_name <> "" && f.sym_name.[0] = '$' ->
let v =
try StrMap.find f.sym_name !patt_vars
with Not_found ->
let v = new_tvar f.sym_name in
patt_vars := StrMap.add f.sym_name v !patt_vars;
v
in to_var (mk_Vari v)
| _ -> raise Not_a_var
in
let replace_nl_var v =
if VarSet.mem v !nl_vars then new_tvar "_" else v
in
try
let vs = Array.map to_var ts in
let vs = Array.map replace_nl_var vs in
let fn n v m = if VarSet.mem v !nl_vars then m else StrMap.add n v m in
let map = StrMap.fold fn !patt_vars StrMap.empty in
Some (vs, map)
with Not_a_var -> None
(** [sym_to_var m t] replaces in [t] every symbol [f] by a variable according
to the map [map]. *)
let sym_to_var : tvar StrMap.t -> term -> term = fun map ->
let rec to_var t =
match unfold t with
| Symb f -> (try mk_Vari (StrMap.find f.sym_name map) with Not_found -> t)
| Prod(a,b) -> mk_Prod (to_var a, to_var_binder b)
| Abst(a,b) -> mk_Abst (to_var a, to_var_binder b)
| LLet(a,t,u) -> mk_LLet (to_var a, to_var t, to_var_binder u)
| Appl(a,b) -> mk_Appl(to_var a, to_var b)
| Meta(m,ts) -> mk_Meta(m, Array.map to_var ts)
| Patt _ -> assert false
| TEnv _ -> assert false
| TRef _ -> assert false
| _ -> t
and to_var_binder b =
let (x,b) = Bindlib.unbind b in bind x lift (to_var b)
in fun t -> if StrMap.is_empty map then t else to_var t
(** [codom_binder n t] returns the [n]-th binder of [t] if [t] is a product of
arith >= [n]. *)
let rec codom_binder : int -> term -> tbinder = fun n t ->
match unfold t with
| Prod(_,b) ->
if n <= 0 then b else codom_binder (n-1) (Bindlib.subst b mk_Kind)
| _ -> assert false