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
let (<?>) = Dolmen.Std.Misc.(<?>)
let lexicographic = Dolmen.Std.Misc.lexicographic
module E = Dolmen.Std.Expr
module B = Dolmen.Std.Builtin
module T = Dolmen.Std.Expr.Term
module V = Dolmen.Std.Expr.Term.Var
module C = Dolmen.Std.Expr.Term.Const
exception Not_a_pattern of T.t
exception Partial_destructor of C.t * Value.t
type t = {
head : C.t;
args : Value.t list;
}
let print fmt { head; args; } =
match args with
| [] ->
Format.fprintf fmt "{%a}" C.print head
| _ ->
let pp_sep = Format.pp_print_space in
Format.fprintf fmt "{%a@ %a}"
C.print head (Format.pp_print_list ~pp_sep Value.print) args
let compare t t' =
C.compare t.head t'.head
<?> (lexicographic Value.compare, t.args, t'.args)
let ops = Value.ops ~print ~compare ()
let mk head args =
Value.mk ~ops { head; args; }
let tester cstr value =
let { head; args = _ } = Value.extract_exn ~ops value in
if C.equal cstr head then Bool.mk true else Bool.mk false
let destructor cstr field value =
let { head; args; } = Value.extract_exn ~ops value in
if C.equal cstr head
then List.nth args field
else raise (Partial_destructor (cstr, value))
let builtins _ (cst : C.t) =
match cst.builtin with
| B.Constructor _ -> Some (Fun.fun_n ~cst (mk cst))
| B.Tester { cstr; _ } -> Some (Fun.fun_1 ~cst (tester cstr))
| B.Destructor { cstr; field; _ } -> Some (Fun.fun_1 ~cst (destructor cstr field))
| _ -> None
type pat =
| Var of V.t
| Cstr of C.t * T.t list
let view_pat (t : T.t) =
match t.term_descr with
| Var v -> Var v
| Cst ( { builtin = B.Constructor _; _ } as cstr )
-> Cstr (cstr, [])
| App ({ term_descr = Cst ({
builtin = B.Constructor _; _ } as cstr); _ }, _, args)
-> Cstr (cstr, args)
| Cst _ | App _ | Binder _ | Match _ ->
raise (Not_a_pattern t)
let rec pattern_match env pat value =
match view_pat pat with
| Var pat_var ->
Some (Env.update_model env (Model.Var.add pat_var value))
| Cstr (pat_cstr, pat_args) ->
let v = Value.extract_exn ~ops value in
if C.equal pat_cstr v.head then
pattern_match_list env pat_args v.args
else
None
and pattern_match_list env pats values =
match pats, values with
| [], [] -> Some env
| pat :: pats, value :: values ->
begin match pattern_match env pat value with
| None -> None
| Some env -> pattern_match_list env pats values
end
| [], _ :: _ | _ :: _, [] ->
assert false