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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
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)))
(* A few hardcoded cases for efficiency *)
| [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)
(* Generic cases *)
| 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)
|
