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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Genarg
open Geninterp
open Tac2expr
open Tac2interp
(** Dynamic tags *)
let val_tag t = match val_tag t with
| Val.Base t -> t
| _ -> assert false
let val_constr = val_tag (topwit Stdarg.wit_constr)
let val_ident = val_tag (topwit Stdarg.wit_ident)
let val_pattern = Val.create "ltac2:pattern"
let val_pp = Val.create "ltac2:pp"
let val_sort = Val.create "ltac2:sort"
let val_cast = Val.create "ltac2:cast"
let val_inductive = Val.create "ltac2:inductive"
let val_constant = Val.create "ltac2:constant"
let val_constructor = Val.create "ltac2:constructor"
let val_projection = Val.create "ltac2:projection"
let val_univ = Val.create "ltac2:universe"
let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ =
Val.create "ltac2:kont"
let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
match Val.eq tag tag' with
| None -> assert false
| Some Refl -> v
(** Conversion functions *)
let of_unit () = ValInt 0
let to_unit = function
| ValInt 0 -> ()
| _ -> assert false
let of_int n = ValInt n
let to_int = function
| ValInt n -> n
| _ -> assert false
let of_bool b = if b then ValInt 0 else ValInt 1
let to_bool = function
| ValInt 0 -> true
| ValInt 1 -> false
| _ -> assert false
let of_char n = ValInt (Char.code n)
let to_char = function
| ValInt n -> Char.chr n
| _ -> assert false
let of_string s = ValStr s
let to_string = function
| ValStr s -> s
| _ -> assert false
let rec of_list f = function
| [] -> ValInt 0
| x :: l -> ValBlk (0, [| f x; of_list f l |])
let rec to_list f = function
| ValInt 0 -> []
| ValBlk (0, [|v; vl|]) -> f v :: to_list f vl
| _ -> assert false
let of_ext tag c =
ValExt (Val.Dyn (tag, c))
let to_ext tag = function
| ValExt e -> extract_val tag e
| _ -> assert false
let of_constr c = of_ext val_constr c
let to_constr c = to_ext val_constr c
let of_ident c = of_ext val_ident c
let to_ident c = to_ext val_ident c
let of_pattern c = of_ext val_pattern c
let to_pattern c = to_ext val_pattern c
(** FIXME: handle backtrace in Ltac2 exceptions *)
let of_exn c = match fst c with
| LtacError (kn, c) -> ValOpn (kn, c)
| _ -> of_ext val_exn c
let to_exn c = match c with
| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
| _ -> to_ext val_exn c
let of_option f = function
| None -> ValInt 0
| Some c -> ValBlk (0, [|f c|])
let to_option f = function
| ValInt 0 -> None
| ValBlk (0, [|c|]) -> Some (f c)
| _ -> assert false
let of_pp c = of_ext val_pp c
let to_pp c = to_ext val_pp c
let of_tuple cl = ValBlk (0, cl)
let to_tuple = function
| ValBlk (0, cl) -> cl
| _ -> assert false
let of_array f vl = ValBlk (0, Array.map f vl)
let to_array f = function
| ValBlk (0, vl) -> Array.map f vl
| _ -> assert false
let of_constant c = of_ext val_constant c
let to_constant c = to_ext val_constant c
|
