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
173
174
175
|
type t =
| Var of string
| Integer of Z.t
| Rational of Q.t
| String of string
| Reference of string
| Nil
| Record of t Label.Map.t
let rec of_term (term : Term.t) =
match term with
| Term.Integer z -> Integer z
| Term.Rational q -> Rational q
| Term.String s -> String s
| Term.Reference name -> Reference name
| Term.Nil -> Nil
| Term.Record map -> Record (Label.Map.map of_term map)
let rec to_term = function
| Var _ -> None
| Reference name -> Result.to_option (Term.reference name)
| Integer z -> Some (Term.integer z)
| Rational q ->
(* Rebuilding through the smart constructor keeps canonicity a
single-point invariant. The denominator is nonzero by
construction, so this cannot fail. *)
Result.to_option (Term.rational ~num:(Q.num q) ~den:(Q.den q))
| String s -> Some (Term.string s)
| Nil -> Some Term.nil
| Record map ->
let closed =
Label.Map.fold
(fun label pattern acc ->
match (acc, to_term pattern) with
| Some bindings, Some term -> Some ((label, term) :: bindings)
| _ -> None)
map (Some [])
in
Option.bind closed (fun bindings -> Result.to_option (Term.record bindings))
let is_ground pattern = Option.is_some (to_term pattern)
let vars pattern =
let rec collect acc = function
| Var v -> if List.mem v acc then acc else v :: acc
| Integer _ | Rational _ | String _ | Reference _ | Nil -> acc
| Record map -> Label.Map.fold (fun _ p acc -> collect acc p) map acc
in
List.rev (collect [] pattern)
let forced_label name =
match Label.of_string name with Ok l -> l | Error _ -> assert false
let head_label = forced_label "head"
let tail_label = forced_label "tail"
let cons ~head ~tail =
Record Label.Map.(empty |> add head_label head |> add tail_label tail)
let rec equal a b =
match (a, b) with
| Var x, Var y -> String.equal x y
| Integer x, Integer y -> Z.equal x y
| Rational x, Rational y -> Q.equal x y
| String x, String y -> String.equal x y
| Reference x, Reference y -> String.equal x y
| Nil, Nil -> true
| Record x, Record y -> Label.Map.equal equal x y
| _ -> false
(* Containment runs the checker extracted from
theories/DecreaseChecker.v, whose soundness and decrease are
proven. The trusted seam is this conversion (injective by leaf
kind) and the two equality functions. *)
type checker_leaf =
| L_var of string
| L_int of Z.t
| L_rat of Q.t
| L_str of string
| L_ref of string
| L_nil
let checker_leaf_equal a b =
match (a, b) with
| L_var x, L_var y | L_str x, L_str y | L_ref x, L_ref y -> String.equal x y
| L_int x, L_int y -> Z.equal x y
| L_rat x, L_rat y -> Q.equal x y
| L_nil, L_nil -> true
| _ -> false
let rec to_checker = function
| Var v -> Decrease_extracted.Leaf (L_var v)
| Integer z -> Decrease_extracted.Leaf (L_int z)
| Rational q -> Decrease_extracted.Leaf (L_rat q)
| String s -> Decrease_extracted.Leaf (L_str s)
| Reference name -> Decrease_extracted.Leaf (L_ref name)
| Nil -> Decrease_extracted.Leaf L_nil
| Record map ->
Decrease_extracted.Node
(List.fold_right
(fun (label, value) rest ->
Decrease_extracted.FCons (label, to_checker value, rest))
(Label.Map.bindings map) Decrease_extracted.FNil)
let strictly_contains pattern ~sub =
Decrease_extracted.contains Label.equal checker_leaf_equal (to_checker sub)
(to_checker pattern)
let rec pp fmt = function
| Var v -> Format.pp_print_string fmt v
| Integer z -> Z.pp_print fmt z
| Rational q -> Q.pp_print fmt q
| String s -> Format.fprintf fmt "%S" s
| Reference name -> Format.fprintf fmt "#%s" name
| Nil -> Format.pp_print_string fmt "#()"
| Record map ->
Format.fprintf fmt "@[<hv 1>{";
let first = ref true in
Label.Map.iter
(fun label p ->
if not !first then Format.fprintf fmt "@ ";
first := false;
Format.fprintf fmt "%a %a" Label.pp label pp p)
map;
Format.fprintf fmt "}@]"
module Subst = struct
module M = Map.Make (String)
type pattern = t
type nonrec t = pattern M.t
let empty = M.empty
let rec walk subst pattern =
match pattern with
| Var v -> (
match M.find_opt v subst with
| Some bound -> walk subst bound
| None -> pattern)
| _ -> pattern
let rec resolve subst pattern =
match walk subst pattern with
| Record map -> Record (Label.Map.map (resolve subst) map)
| other -> other
let rec occurs subst v pattern =
match walk subst pattern with
| Var w -> String.equal v w
| Record map -> Label.Map.exists (fun _ p -> occurs subst v p) map
| _ -> false
let rec unify subst a b =
let a = walk subst a and b = walk subst b in
match (a, b) with
| Var x, Var y when String.equal x y -> Some subst
| Var x, other | other, Var x ->
if occurs subst x other then None else Some (M.add x other subst)
| Integer x, Integer y -> if Z.equal x y then Some subst else None
| Rational x, Rational y -> if Q.equal x y then Some subst else None
| String x, String y -> if String.equal x y then Some subst else None
| Nil, Nil -> Some subst
| Record x, Record y ->
if
Label.Map.cardinal x = Label.Map.cardinal y
&& Label.Map.for_all (fun label _ -> Label.Map.mem label y) x
then
Label.Map.fold
(fun label p acc ->
Option.bind acc (fun s -> unify s p (Label.Map.find label y)))
x (Some subst)
else None
| _ -> None
end
|
