summaryrefslogtreecommitdiff
path: root/interp/genarg.ml
blob: 511cf88a32d8151e0fcf3b005c9a685c9d0296f4 (plain)
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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: genarg.ml 7879 2006-01-16 13:58:09Z herbelin $ *)

open Pp
open Util
open Names
open Nameops
open Nametab
open Rawterm
open Topconstr
open Term

type argument_type =
  (* Basic types *)
  | BoolArgType
  | IntArgType
  | IntOrVarArgType
  | StringArgType
  | PreIdentArgType
  | IntroPatternArgType
  | IdentArgType
  | VarArgType
  | RefArgType
  (* Specific types *)
  | SortArgType
  | ConstrArgType
  | ConstrMayEvalArgType
  | QuantHypArgType
  | TacticArgType of int
  | OpenConstrArgType of bool
  | ConstrWithBindingsArgType
  | BindingsArgType
  | 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
type 'a and_short_name = 'a * identifier located option
type rawconstr_and_expr = rawconstr * constr_expr option

(* 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,t)

let exists_argtype s = List.mem s !dyntab

type intro_pattern_expr =
  | IntroOrAndPattern of case_intro_pattern_expr
  | IntroWildcard
  | IntroIdentifier of identifier
  | IntroAnonymous
and case_intro_pattern_expr = intro_pattern_expr list list

let rec pr_intro_pattern = function
  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
  | IntroWildcard -> str "_"
  | IntroIdentifier id -> pr_id id
  | IntroAnonymous -> str "?"

and pr_case_intro_pattern = function
  | [pl] ->
      str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
  | pll ->
      str "[" ++
      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
      ++ str "]"

type open_constr = Evd.evar_map * Term.constr
type open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr

let rawwit_bool = BoolArgType
let globwit_bool = BoolArgType
let wit_bool = BoolArgType

let rawwit_int = IntArgType
let globwit_int = IntArgType
let wit_int = IntArgType

let rawwit_int_or_var = IntOrVarArgType
let globwit_int_or_var = IntOrVarArgType
let wit_int_or_var = IntOrVarArgType

let rawwit_string = StringArgType
let globwit_string = StringArgType
let wit_string = StringArgType

let rawwit_pre_ident = PreIdentArgType
let globwit_pre_ident = PreIdentArgType
let wit_pre_ident = PreIdentArgType

let rawwit_intro_pattern = IntroPatternArgType
let globwit_intro_pattern = IntroPatternArgType
let wit_intro_pattern = IntroPatternArgType

let rawwit_ident = IdentArgType
let globwit_ident = IdentArgType
let wit_ident = IdentArgType

let rawwit_var = VarArgType
let globwit_var = VarArgType
let wit_var = VarArgType

let rawwit_ref = RefArgType
let globwit_ref = RefArgType
let wit_ref = RefArgType

let rawwit_quant_hyp = QuantHypArgType
let globwit_quant_hyp = QuantHypArgType
let wit_quant_hyp = QuantHypArgType

let rawwit_sort = SortArgType
let globwit_sort = SortArgType
let wit_sort = SortArgType

let rawwit_constr = ConstrArgType
let globwit_constr = ConstrArgType
let wit_constr = ConstrArgType

let rawwit_constr_may_eval = ConstrMayEvalArgType
let globwit_constr_may_eval = ConstrMayEvalArgType
let wit_constr_may_eval = ConstrMayEvalArgType

let rawwit_tactic n = TacticArgType n
let globwit_tactic n = TacticArgType n
let wit_tactic n = TacticArgType n

let rawwit_open_constr_gen b = OpenConstrArgType b
let globwit_open_constr_gen b = OpenConstrArgType b 
let wit_open_constr_gen b = OpenConstrArgType b

let rawwit_open_constr = rawwit_open_constr_gen false
let globwit_open_constr = globwit_open_constr_gen false
let wit_open_constr = wit_open_constr_gen false

let rawwit_casted_open_constr = rawwit_open_constr_gen true
let globwit_casted_open_constr = globwit_open_constr_gen true
let wit_casted_open_constr = wit_open_constr_gen true

let rawwit_constr_with_bindings = ConstrWithBindingsArgType
let globwit_constr_with_bindings = ConstrWithBindingsArgType
let wit_constr_with_bindings = ConstrWithBindingsArgType

let rawwit_bindings = BindingsArgType
let globwit_bindings = BindingsArgType
let wit_bindings = BindingsArgType

let rawwit_red_expr = RedExprArgType
let globwit_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, 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, 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, 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), 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 unquote x = x

type an_arg_of_this_type = Obj.t

let in_generic t x = (t, Obj.repr x)