Source file inverse.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
(** Compute the inverse image of a term wrt an injective function. *)
open Term
open Timed
open Common
open Print
open Lplib
(** Logging function for unification. *)
let log = Logger.make 'v' "invr" "inverse"
let log = log.pp
(** [cache f s] is equivalent to [f s] but [f s] is computed only once unless
the rules of [s] are changed. *)
let cache : (sym -> 'a) -> (sym -> 'a) = fun f ->
let cache = ref [] in
fun s ->
let srs = !(s.sym_rules) in
try let rs, x = List.assq s !cache in
if rs == srs then x else raise Not_found
with Not_found -> let x = f s in cache := (s, (srs, x))::!cache; x
(** [const_graph s] returns the list of pairs [(s0,s1)] such that [s]
has a rule of the form [s (s0 ...) ↪ s1 ...]. *)
let const_graph : sym -> (sym * sym) list = fun s ->
if Logger.log_enabled () then log "check rules of %a" sym s;
let add s0 s1 l =
if Logger.log_enabled () then
log (Color.yel "%a %a ↪ %a") sym s sym s0 sym s1;
(s0,s1)::l
in
let f l rule =
match rule.lhs with
| [l1] ->
begin
match get_args l1 with
| Symb s0, _ ->
let n = Bindlib.mbinder_arity rule.rhs in
let r = Bindlib.msubst rule.rhs (Array.make n TE_None) in
begin
match get_args r with
| Symb s1, _ -> add s0 s1 l
| _ -> l
end
| _ -> l
end
| _ -> l
in
List.fold_left f [] !(s.sym_rules)
(** cached version of [const_rules]. *)
let const_graph : sym -> (sym * sym) list = cache const_graph
(** [inverse_const s s'] returns [s0] if [s] has a rule of the form [s (s0
...) ↪ s' ...].
@raise [Not_found] otherwise. *)
let inverse_const : sym -> sym -> sym = fun s s' ->
fst (List.find (fun (_,s1) -> s1 == s') (const_graph s))
(** [prod_graph s] returns the list of tuples [(s0,s1,s2,b)] such that [s] has
a rule of the form [s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x]
occurs in [r]. *)
let prod_graph : sym -> (sym * sym * sym * bool) list = fun s ->
if Logger.log_enabled () then log "check rules of %a" sym s;
let add (s0,s1,s2,b) l =
if Logger.log_enabled () then
if b then log (Color.yel "%a (%a _ _) ↪ Π x:%a _, %a _[x]")
sym s sym s0 sym s1 sym s2
else log (Color.yel "%a (%a _ _) ↪ %a _ → %a _")
sym s sym s0 sym s1 sym s2;
(s0,s1,s2,b)::l
in
let f l rule =
match rule.lhs with
| [l1] ->
begin
match get_args l1 with
| Symb s0, [_;_] ->
let n = Bindlib.mbinder_arity rule.rhs in
let r = Bindlib.msubst rule.rhs (Array.make n TE_None) in
begin
match r with
| Prod(a,b) ->
begin
match get_args a with
| Symb s1, [_] ->
begin
match get_args (Bindlib.subst b mk_Kind) with
| Symb(s2), [_] -> add (s0,s1,s2,Bindlib.binder_occur b) l
| _ -> l
end
| _ -> l
end
| _ -> l
end
| _ -> l
end
| _ -> l
in
List.fold_left f [] !(s.sym_rules)
(** cached version of [prod_graph]. *)
let prod_graph : sym -> (sym * sym * sym * bool) list = cache prod_graph
(** [inverse_prod s s'] returns [(s0,s1,s2,b)] if [s] has a rule of the form
[s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x] occurs in [r], and
either [s1] has a rule of the form [s1 (s3 ...) ↪ s' ...] or [s1 == s'].
@raise [Not_found] otherwise. *)
let inverse_prod : sym -> sym -> sym * sym * sym * bool = fun s s' ->
match prod_graph s with
| [] -> raise Not_found
| [x] -> x
| graph ->
let f (_,s1,_,_) =
try let _ = inverse_const s1 s' in true with Not_found -> false in
try List.find f graph
with Not_found -> List.find (fun (_,s1,_,_) -> s1 == s') graph
(** [inverse s v] tries to compute a term [u] such that [s(u)] reduces to [v].
@raise [Not_found] otherwise. *)
let rec inverse : sym -> term -> term = fun s v ->
if Logger.log_enabled () then log "compute %a⁻¹(%a)" sym s term v;
match get_args v with
| Symb s', [t] when s' == s -> t
| Symb s', ts -> add_args (mk_Symb (inverse_const s s')) ts
| Prod(a,b), _ ->
let s0,s1,s2,occ =
match get_args a with
| Symb s', _ -> inverse_prod s s'
| _ -> raise Not_found
in
let t1 = inverse s1 a in
let t2 =
let x, b = Bindlib.unbind b in
let b = inverse s2 b in
if occ then
Bindlib.unbox (_Abst (lift a) (Bindlib.bind_var x (lift b)))
else b
in
add_args (mk_Symb s0) [t1;t2]
| _ -> raise Not_found
let inverse : sym -> term -> term = fun s v ->
let t = inverse s v in let v' = mk_Appl(mk_Symb s,t) in
if Eval.eq_modulo [] v' v then t
else (if Logger.log_enabled() then log "%a ≢ %a@" term v' term v;
raise Not_found)