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
176
177
178
179
180
181
182
183
184
185
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Names
open Nametab
open Rawterm
open Topconstr
type argument_type =
(* Basic types *)
| BoolArgType
| IntArgType
| IntOrVarArgType
| StringArgType
| PreIdentArgType
| IdentArgType
| RefArgType
(* Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
| TacticArgType
| CastedOpenConstrArgType
| ConstrWithBindingsArgType
| RedExprArgType
| List0ArgType of argument_type
| List1ArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string
type 'a or_var = ArgArg of 'a | ArgVar of identifier located
(* Dynamics but tagged by a type expression *)
type ('a,'b) generic_argument = argument_type * Obj.t
let dyntab = ref ([] : string list)
type ('a,'b,'c) abstract_argument_type = argument_type
let create_arg s =
if List.mem s !dyntab then
anomaly ("Genarg.create: already declared generic argument " ^ s);
dyntab := s :: !dyntab;
let t = ExtraArgType s in
(t,t)
let exists_argtype s = List.mem s !dyntab
type open_constr = Evd.evar_map * Term.constr
(*type open_rawconstr = Coqast.t*)
type open_rawconstr = constr_expr
let rawwit_bool = BoolArgType
let wit_bool = BoolArgType
let rawwit_int = IntArgType
let wit_int = IntArgType
let rawwit_int_or_var = IntOrVarArgType
let wit_int_or_var = IntOrVarArgType
let rawwit_string = StringArgType
let wit_string = StringArgType
let rawwit_ident = IdentArgType
let wit_ident = IdentArgType
let rawwit_pre_ident = PreIdentArgType
let wit_pre_ident = PreIdentArgType
let rawwit_ref = RefArgType
let wit_ref = RefArgType
let rawwit_quant_hyp = QuantHypArgType
let wit_quant_hyp = QuantHypArgType
let rawwit_sort = SortArgType
let wit_sort = SortArgType
let rawwit_constr = ConstrArgType
let wit_constr = ConstrArgType
let rawwit_constr_may_eval = ConstrMayEvalArgType
let wit_constr_may_eval = ConstrMayEvalArgType
let rawwit_tactic = TacticArgType
let wit_tactic = TacticArgType
let rawwit_casted_open_constr = CastedOpenConstrArgType
let wit_casted_open_constr = CastedOpenConstrArgType
let rawwit_constr_with_bindings = ConstrWithBindingsArgType
let wit_constr_with_bindings = ConstrWithBindingsArgType
let rawwit_red_expr = RedExprArgType
let wit_red_expr = RedExprArgType
let wit_list0 t = List0ArgType t
let wit_list1 t = List1ArgType t
let wit_opt t = OptArgType t
let wit_pair t1 t2 = PairArgType (t1,t2)
let in_gen t o = (t,Obj.repr o)
let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen"
let genarg_tag (s,_) = s
let fold_list0 f = function
| (List0ArgType t as u, l) ->
List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
| _ -> failwith "Genarg: not a list0"
let fold_list1 f = function
| (List1ArgType t as u, l) ->
List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
| _ -> failwith "Genarg: not a list1"
let fold_opt f a = function
| (OptArgType t as u, l) ->
(match Obj.magic l with
| None -> a
| Some x -> f (in_gen t x))
| _ -> failwith "Genarg: not a opt"
let fold_pair f = function
| (PairArgType (t1,t2) as u, l) ->
let (x1,x2) = Obj.magic l in
f (in_gen t1 x1) (in_gen t2 x2)
| _ -> failwith "Genarg: not a pair"
let app_list0 f = function
| (List0ArgType t as u, l) ->
let o = Obj.magic l in
(u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not a list0"
let app_list1 f = function
| (List1ArgType t as u, l) ->
let o = Obj.magic l in
(u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not a list1"
let app_opt f = function
| (OptArgType t as u, l) ->
let o = Obj.magic l in
(u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not an opt"
let app_pair f1 f2 = function
| (PairArgType (t1,t2) as u, l) ->
let (o1,o2) = Obj.magic l in
let o1 = out_gen t1 (f1 (in_gen t1 o1)) in
let o2 = out_gen t2 (f2 (in_gen t2 o2)) in
(u, Obj.repr (o1,o2))
| _ -> failwith "Genarg: not a pair"
let or_var_app f = function
| ArgArg x -> ArgArg (f x)
| ArgVar _ as x -> x
let smash_var_app t f g = function
| ArgArg x -> f x
| ArgVar (_,id) ->
let (u, _ as x) = g id in
if t <> u then failwith "Genarg: a variable bound to a wrong type";
x
let unquote x = x
type an_arg_of_this_type = Obj.t
let in_generic t x = (t, Obj.repr x)
|
