Source file tac2val.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
open Util
open Names
open Proofview.Notations
type ('a, _) arity0 =
| OneAty : ('a, 'a -> 'a Proofview.tactic) arity0
| AddAty : ('a, 'b) arity0 -> ('a, 'a -> 'b) arity0
type tag = int
type valexpr =
| ValInt of int
(** Immediate integers *)
| ValBlk of tag * valexpr array
(** Structured blocks *)
| ValStr of Bytes.t
(** Strings *)
| ValCls of closure
(** Closures *)
| ValOpn of KerName.t * valexpr array
(** Open constructors *)
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
and closure = MLTactic : (valexpr, 'v) arity0 * Tac2expr.frame option * 'v -> closure
let arity_one = OneAty
let arity_suc a = AddAty a
type 'a arity = (valexpr, 'a) arity0
let mk_closure arity f = MLTactic (arity, None, f)
let mk_closure_val arity f = ValCls (mk_closure arity f)
module Valexpr =
struct
type t = valexpr
let is_int = function
| ValInt _ -> true
| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false
let tag v = match v with
| ValBlk (n, _) -> n
| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
CErrors.anomaly (Pp.str "Unexpected value shape")
let field v n = match v with
| ValBlk (_, v) -> v.(n)
| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
CErrors.anomaly (Pp.str "Unexpected value shape")
let set_field v n w = match v with
| ValBlk (_, v) -> v.(n) <- w
| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
CErrors.anomaly (Pp.str "Unexpected value shape")
let make_block tag v = ValBlk (tag, v)
let make_int n = ValInt n
end
let to_closure = function
| ValCls cls -> cls
| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false
let wrap fr tac = match fr with
| None -> tac
| Some fr -> Tac2bt.with_frame fr tac
let rec apply : type a. a arity -> _ -> a -> valexpr list -> valexpr Proofview.tactic =
fun arity fr f args -> match args, arity with
| [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, fr, f)))
| [a0], OneAty -> wrap fr (f a0)
| [a0; a1], AddAty OneAty -> wrap fr (f a0 a1)
| [a0; a1; a2], AddAty (AddAty OneAty) -> wrap fr (f a0 a1 a2)
| [a0; a1; a2; a3], AddAty (AddAty (AddAty OneAty)) -> wrap fr (f a0 a1 a2 a3)
| a :: args, OneAty ->
wrap fr (f a) >>= fun f ->
let MLTactic (arity, fr, f) = to_closure f in
apply arity fr f args
| a :: args, AddAty arity ->
apply arity fr (f a) args
let apply (MLTactic (arity, wrap, f)) args = apply arity wrap f args
let apply_val v args = apply (to_closure v) args
type n_closure =
| NClosure : 'a arity * (valexpr list -> 'a) -> n_closure
let rec abstract n f =
if Int.equal n 1 then NClosure (OneAty, fun accu v -> f (List.rev (v :: accu)))
else
let NClosure (arity, fe) = abstract (n - 1) f in
NClosure (AddAty arity, fun accu v -> fe (v :: accu))
let abstract n f =
match n with
| 1 -> MLTactic (OneAty, None, fun a -> f [a])
| 2 -> MLTactic (AddAty OneAty, None, fun a b -> f [a;b])
| 3 -> MLTactic (AddAty (AddAty OneAty), None, fun a b c -> f [a;b;c])
| 4 -> MLTactic (AddAty (AddAty (AddAty OneAty)), None, fun a b c d -> f [a;b;c;d])
| _ ->
let () = assert (n > 0) in
let NClosure (arity, f) = abstract n f in
MLTactic (arity, None, f [])
let annotate_closure fr (MLTactic (arity, fr0, f)) =
assert (Option.is_empty fr0);
MLTactic (arity, Some fr, f)
let rec purify_closure : type a. a arity -> (unit -> a) -> a = fun arity f ->
match arity with
| OneAty -> (fun x -> Proofview.tclUNIT () >>= fun () -> f () x)
| AddAty a -> (fun x -> purify_closure a (fun () -> f () x))
let purify_closure ar f = purify_closure ar (fun () -> f)