1
(** Translation from coq abstract syntax trees to centaur vernac
19
(* // Verify whether this is dead code, as of coq version 7 *)
20
(* The following three sentences have been added to cope with a change
21
of strategy from the Coq team in the way rules construct ast's. The
22
problem is that now grammar rules will refer to identifiers by giving
23
their absolute name, using the mutconstruct when needed. Unfortunately,
24
when you have a mutconstruct structure, you don't have a way to guess
25
the corresponding identifier without an environment, and the parser
26
does not have an environment. We add one, only for the constructs
27
that are always loaded. *)
28
let type_table = ((Hashtbl.create 17) :
29
(string, ((string array) array)) Hashtbl.t);;
31
Hashtbl.add type_table "Coq.Init.Logic.and"
32
[|[|"dummy";"conj"|]|];;
34
Hashtbl.add type_table "Coq.Init.Datatypes.prod"
35
[|[|"dummy";"pair"|]|];;
37
Hashtbl.add type_table "Coq.Init.Datatypes.nat"
40
Hashtbl.add type_table "Coq.ZArith.fast_integer.Z"
41
[|[|"";"ZERO";"POS";"NEG"|]|];;
44
Hashtbl.add type_table "Coq.ZArith.fast_integer.positive"
45
[|[|"";"xI";"xO";"xH"|]|];;
47
(*The following two codes are added to cope with the distinction
48
between ocaml and caml-light syntax while using ctcaml to
49
manipulate the program *)
50
let code_plus = code (get "+" 0);;
52
let code_minus = code (get "-" 0);;
54
let coercion_description_holder = ref (function _ -> None : t -> int option);;
56
let coercion_description t = !coercion_description_holder t;;
58
let set_coercion_description f =
59
coercion_description_holder:=f; ();;
61
let xlate_error s = print_endline ("xlate_error : "^s);failwith ("Translation error: " ^ s);;
63
let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;;
65
let ctf_STRING_OPT_SOME s = CT_coerce_STRING_to_STRING_OPT s;;
67
let ctf_STRING_OPT = function
68
| None -> ctf_STRING_OPT_NONE
69
| Some s -> ctf_STRING_OPT_SOME (CT_string s)
71
let ctv_ID_OPT_NONE = CT_coerce_NONE_to_ID_OPT CT_none;;
73
let ctf_ID_OPT_SOME s = CT_coerce_ID_to_ID_OPT s;;
75
let ctv_ID_OPT_OR_ALL_NONE =
76
CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_NONE_to_ID_OPT CT_none);;
78
let ctv_FORMULA_OPT_NONE =
79
CT_coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT CT_none);;
81
let ctv_PATTERN_OPT_NONE = CT_coerce_NONE_to_PATTERN_OPT CT_none;;
83
let ctv_DEF_BODY_OPT_NONE = CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT
84
ctv_FORMULA_OPT_NONE;;
86
let ctf_ID_OPT_OR_ALL_SOME s =
87
CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (ctf_ID_OPT_SOME s);;
89
let ctv_ID_OPT_OR_ALL_ALL = CT_all;;
91
let ctv_SPEC_OPT_NONE = CT_coerce_NONE_to_SPEC_OPT CT_none;;
93
let ct_coerce_FORMULA_to_DEF_BODY x =
94
CT_coerce_CONTEXT_PATTERN_to_DEF_BODY
95
(CT_coerce_FORMULA_to_CONTEXT_PATTERN x);;
97
let castc x = CT_coerce_TYPED_FORMULA_to_FORMULA x;;
99
let varc x = CT_coerce_ID_to_FORMULA x;;
101
let xlate_ident id = CT_ident (string_of_id id)
103
let ident_tac s = CT_user_tac (xlate_ident s, CT_targ_list []);;
105
let ident_vernac s = CT_user_vernac (CT_ident s, CT_varg_list []);;
107
let nums_to_int_list_aux l = List.map (fun x -> CT_int x) l;;
109
let nums_to_int_list l = CT_int_list(nums_to_int_list_aux l);;
111
let num_or_var_to_int = function
112
| ArgArg x -> CT_int x
113
| _ -> xlate_error "TODO: nums_to_int_list_aux ArgVar";;
115
let nums_or_var_to_int_list_aux l = List.map num_or_var_to_int l;;
117
let nums_or_var_to_int_list l = CT_int_list(nums_or_var_to_int_list_aux l);;
119
let nums_or_var_to_int_ne_list n l =
120
CT_int_ne_list(num_or_var_to_int n, nums_or_var_to_int_list_aux l);;
122
type iTARG = Targ_command of ct_FORMULA
123
| Targ_intropatt of ct_INTRO_PATT_LIST
124
| Targ_id_list of ct_ID_LIST
125
| Targ_spec_list of ct_SPEC_LIST
126
| Targ_binding_com of ct_FORMULA
127
| Targ_ident of ct_ID
129
| Targ_binding of ct_BINDING
130
| Targ_pattern of ct_PATTERN
131
| Targ_unfold of ct_UNFOLD
132
| Targ_unfold_ne_list of ct_UNFOLD_NE_LIST
133
| Targ_string of ct_STRING
134
| Targ_fixtac of ct_FIXTAC
135
| Targ_cofixtac of ct_COFIXTAC
136
| Targ_tacexp of ct_TACTIC_COM
137
| Targ_redexp of ct_RED_COM;;
139
type iVARG = Varg_binder of ct_BINDER
140
| Varg_binderlist of ct_BINDER_LIST
141
| Varg_bindernelist of ct_BINDER_NE_LIST
142
| Varg_call of ct_ID * iVARG list
143
| Varg_constr of ct_FORMULA
144
| Varg_sorttype of ct_SORT_TYPE
145
| Varg_constrlist of ct_FORMULA list
146
| Varg_ident of ct_ID
148
| Varg_intlist of ct_INT_LIST
150
| Varg_string of ct_STRING
151
| Varg_tactic of ct_TACTIC_COM
153
| Varg_astlist of ct_AST_LIST
154
| Varg_tactic_arg of iTARG
155
| Varg_varglist of iVARG list;;
158
let coerce_iVARG_to_FORMULA =
161
| Varg_sorttype x -> CT_coerce_SORT_TYPE_to_FORMULA x
162
| Varg_ident id -> CT_coerce_ID_to_FORMULA id
163
| _ -> xlate_error "coerce_iVARG_to_FORMULA: unexpected argument";;
165
let coerce_iVARG_to_ID =
166
function Varg_ident id -> id
167
| _ -> xlate_error "coerce_iVARG_to_ID";;
169
let coerce_VARG_to_ID =
171
| CT_coerce_ID_OPT_OR_ALL_to_VARG (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_ID_to_ID_OPT x)) ->
173
| _ -> xlate_error "coerce_VARG_to_ID";;
175
let xlate_ident_opt =
177
| None -> ctv_ID_OPT_NONE
178
| Some id -> ctf_ID_OPT_SOME (xlate_ident id)
180
let xlate_id_to_id_or_int_opt s =
181
CT_coerce_ID_OPT_to_ID_OR_INT_OPT
182
(CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id s)));;
184
let xlate_int_to_id_or_int_opt n =
185
CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
186
(CT_coerce_INT_to_ID_OR_INT (CT_int n));;
188
let none_in_id_or_int_opt =
189
CT_coerce_ID_OPT_to_ID_OR_INT_OPT
190
(CT_coerce_NONE_to_ID_OPT(CT_none));;
192
let xlate_int_opt = function
193
| Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
194
| None -> CT_coerce_NONE_to_INT_OPT CT_none
196
let xlate_int_or_var_opt_to_int_opt = function
197
| Some (ArgArg n) -> CT_coerce_INT_to_INT_OPT (CT_int n)
198
| Some (ArgVar _) -> xlate_error "int_or_var: TODO"
199
| None -> CT_coerce_NONE_to_INT_OPT CT_none
201
let apply_or_by_notation f = function
203
| ByNotation _ -> xlate_error "TODO: ByNotation"
205
let tac_qualid_to_ct_ID ref =
206
CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
208
let loc_qualid_to_ct_ID ref =
209
CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
211
let int_of_meta n = int_of_string (string_of_id n)
212
let is_int_meta n = try let _ = int_of_meta n in true with _ -> false
214
let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
216
let reference_to_ct_ID = function
217
| Ident (_,id) -> CT_ident (Names.string_of_id id)
218
| Qualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
220
let xlate_class = function
221
| FunClass -> CT_ident "FUNCLASS"
222
| SortClass -> CT_ident "SORTCLASS"
223
| RefClass qid -> loc_qualid_to_ct_ID qid
225
let id_to_pattern_var ctid =
227
| CT_metaid _ -> xlate_error "metaid not expected in pattern_var"
229
CT_coerce_ID_OPT_to_MATCH_PATTERN (CT_coerce_NONE_to_ID_OPT CT_none)
230
| CT_ident id_string ->
231
CT_coerce_ID_OPT_to_MATCH_PATTERN
232
(CT_coerce_ID_to_ID_OPT (CT_ident id_string))
233
| CT_metac _ -> assert false;;
235
exception Not_natural;;
239
| RProp Term.Pos -> CT_sortc "Set"
240
| RProp Term.Null -> CT_sortc "Prop"
241
| RType None -> CT_sortc "Type"
242
| RType (Some u) -> xlate_error "xlate_sort";;
246
let d,i = Libnames.repr_qualid a in
247
let l = Names.repr_dirpath d in
248
List.fold_left (fun s i1 -> (string_of_id i1) ^ "." ^ s) (string_of_id i) l;;
250
(* // The next two functions should be modified to make direct reference
251
to a notation operator *)
252
let notation_to_formula s l = CT_notation(CT_string s, CT_formula_list l);;
254
let xlate_reference = function
255
Ident(_,i) -> CT_ident (string_of_id i)
256
| Qualid(_, q) -> CT_ident (xlate_qualid q);;
257
let rec xlate_match_pattern =
259
| CPatAtom(_, Some s) -> id_to_pattern_var (xlate_reference s)
260
| CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_")
261
| CPatCstr(_, f, []) -> id_to_pattern_var (xlate_reference f)
262
| CPatCstr (_, f1 , (arg1 :: args)) ->
264
(id_to_pattern_var (xlate_reference f1),
265
CT_match_pattern_ne_list
266
(xlate_match_pattern arg1,
267
List.map xlate_match_pattern args))
268
| CPatAlias (_, pattern, id) ->
270
(xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
271
| CPatOr (_,l) -> xlate_error "CPatOr: TODO"
272
| CPatDelimiters(_, key, p) ->
273
CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
274
| CPatPrim (_,Numeral n) ->
275
CT_coerce_NUM_to_MATCH_PATTERN
276
(CT_int_encapsulator(Bigint.to_string n))
277
| CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
278
| CPatNotation(_, s, (l,[])) ->
279
CT_pattern_notation(CT_string s,
280
CT_match_pattern_list(List.map xlate_match_pattern l))
281
| CPatNotation(_, s, (l,_)) ->
282
xlate_error "CPatNotation (recursive notation): TODO"
286
let xlate_id_opt_aux = function
287
Name id -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
288
| Anonymous -> ctv_ID_OPT_NONE;;
290
let xlate_id_opt (_, v) = xlate_id_opt_aux v;;
292
let xlate_id_opt_ne_list = function
294
| a::l -> CT_id_opt_ne_list(xlate_id_opt a, List.map xlate_id_opt l);;
297
let rec last = function
302
let rec decompose_last = function
305
| a::tl -> let rl, b = decompose_last tl in (a::rl), b;;
307
let make_fix_struct (n,bl) =
308
let names = names_of_local_assums bl in
309
let nn = List.length names in
310
if nn = 1 || n = None then ctv_ID_OPT_NONE
311
else ctf_ID_OPT_SOME(CT_ident (string_of_id (snd (Option.get n))));;
313
let rec xlate_binder = function
314
(l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
315
and xlate_return_info = function
316
| (Some Anonymous, None) | (None, None) ->
317
CT_coerce_NONE_to_RETURN_INFO CT_none
318
| (None, Some t) -> CT_return(xlate_formula t)
319
| (Some x, Some t) -> CT_as_and_return(xlate_id_opt_aux x, xlate_formula t)
320
| (Some _, None) -> assert false
321
and xlate_formula_opt =
323
| None -> ctv_FORMULA_OPT_NONE
324
| Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e)
326
and xlate_binder_l = function
327
LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
328
| LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n,
331
xlate_match_pattern_ne_list = function
333
| a::l -> CT_match_pattern_ne_list(xlate_match_pattern a,
334
List.map xlate_match_pattern l)
335
and translate_one_equation = function
336
(_,[_,lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
337
| _ -> xlate_error "TODO: disjunctive multiple patterns"
339
xlate_binder_ne_list = function
341
| a::l -> CT_binder_ne_list(xlate_binder a, List.map xlate_binder l)
343
xlate_binder_list = function
344
l -> CT_binder_list( List.map xlate_binder_l l)
345
and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
347
CRef r -> varc (xlate_reference r)
348
| CArrow(_,a,b)-> CT_arrowc (xlate_formula a, xlate_formula b)
349
| CProdN(_,ll,b) as whole_term ->
350
let rec gather_binders = function
352
ll@(gather_binders b)
354
let rec fetch_ultimate_body = function
355
CProdN(_, _, b) -> fetch_ultimate_body b
357
CT_prodc(xlate_binder_ne_list (gather_binders whole_term),
358
xlate_formula (fetch_ultimate_body b))
359
| CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
360
| CLetIn(_, v, a, b) ->
361
CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
362
| CAppExpl(_, (Some n, r), l) ->
363
let l', last = decompose_last l in
364
CT_proj(xlate_formula last,
366
(CT_bang(varc (xlate_reference r)),
367
List.map xlate_formula l'))
368
| CAppExpl(_, (None, r), []) -> CT_bang(varc(xlate_reference r))
369
| CAppExpl(_, (None, r), l) ->
370
CT_appc(CT_bang(varc (xlate_reference r)),
371
xlate_formula_ne_list l)
372
| CApp(_, (Some n,f), l) ->
373
let l', last = decompose_last l in
374
CT_proj(xlate_formula_expl last,
376
(xlate_formula f, List.map xlate_formula_expl l'))
377
| CApp(_, (_,f), l) ->
378
CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
379
| CRecord (_,_,_) -> xlate_error "CRecord: TODO"
380
| CCases (_, _, _, [], _) -> assert false
381
| CCases (_, _, ret_type, tm::tml, eqns)->
382
CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
383
List.map xlate_matched_formula tml),
384
xlate_formula_opt ret_type,
385
CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
386
| CLetTuple (_,a::l, ret_info, c, b) ->
387
CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
388
List.map xlate_id_opt_aux l),
389
xlate_return_info ret_info,
392
| CLetTuple (_, [], _, _, _) -> xlate_error "NOT parsed: Let with ()"
393
| CIf (_,c, ret_info, b1, b2) ->
395
(xlate_formula c, xlate_return_info ret_info,
396
xlate_formula b1, xlate_formula b2)
398
| CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
399
| CNotation(_, s,(l,[])) -> notation_to_formula s (List.map xlate_formula l)
400
| CNotation(_, s,(l,_)) -> xlate_error "CNotation (recursive): TODO"
401
| CGeneralization(_,_,_,_) -> xlate_error "CGeneralization: TODO"
402
| CPrim (_, Numeral i) ->
403
CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
404
| CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
405
| CHole _ -> CT_existvarc
406
(* I assume CDynamic has been inserted to make free form extension of
407
the language possible, but this would go agains the logic of pcoq anyway. *)
408
| CDynamic (_, _) -> assert false
409
| CDelimiters (_, key, num) ->
410
CT_num_encapsulator(CT_num_type key , xlate_formula num)
411
| CCast (_, e, CastConv (_, t)) ->
412
CT_coerce_TYPED_FORMULA_to_FORMULA
413
(CT_typed_formula(xlate_formula e, xlate_formula t))
414
| CCast (_, e, CastCoerce) -> assert false
415
| CPatVar (_, (_,i)) when is_int_meta i ->
416
CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i)))
417
| CPatVar (_, (false, s)) ->
418
CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s))
419
| CPatVar (_, (true, s)) ->
420
xlate_error "Second order variable not supported"
421
| CEvar _ -> xlate_error "CEvar not supported"
422
| CCoFix (_, (_, id), lm::lmi) ->
423
let strip_mutcorec ((_, fid), bl,arf, ardef) =
424
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
425
xlate_formula arf, xlate_formula ardef) in
426
CT_cofixc(xlate_ident id,
427
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
428
| CFix (_, (_, id), lm::lmi) ->
429
let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) =
430
let struct_arg = make_fix_struct (n, bl) in
431
let arf = xlate_formula arf in
432
let ardef = xlate_formula ardef in
433
match xlate_binder_list bl with
434
| CT_binder_list (b :: bl) ->
435
CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
436
struct_arg, arf, ardef)
437
| _ -> xlate_error "mutual recursive" in
438
CT_fixc (xlate_ident id,
440
(CT_coerce_FIX_REC_to_FIX_BINDER
441
(strip_mutrec lm), List.map
442
(fun x-> CT_coerce_FIX_REC_to_FIX_BINDER (strip_mutrec x))
444
| CCoFix _ -> assert false
445
| CFix _ -> assert false
446
and xlate_matched_formula = function
447
(f, (Some x, Some y)) ->
448
CT_formula_as_in(xlate_formula f, xlate_id_opt_aux x, xlate_formula y)
449
| (f, (None, Some y)) ->
450
CT_formula_in(xlate_formula f, xlate_formula y)
451
| (f, (Some x, None)) ->
452
CT_formula_as(xlate_formula f, xlate_id_opt_aux x)
453
| (f, (None, None)) ->
454
CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f)
455
and xlate_formula_expl = function
456
(a, None) -> xlate_formula a
457
| (a, Some (_,ExplByPos (i, _))) ->
458
xlate_error "explicitation of implicit by rank not supported"
459
| (a, Some (_,ExplByName i)) ->
460
CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
461
and xlate_formula_expl_ne_list = function
463
| a::l -> CT_formula_ne_list(xlate_formula_expl a, List.map xlate_formula_expl l)
464
and xlate_formula_ne_list = function
466
| a::l -> CT_formula_ne_list(xlate_formula a, List.map xlate_formula l);;
468
let (xlate_ident_or_metaid:
469
Names.identifier Util.located Tacexpr.or_metaid -> ct_ID) = function
470
AI (_, x) -> xlate_ident x
471
| MetaId(_, x) -> CT_metaid x;;
473
let nums_of_occs (b,nums) =
475
else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums
477
let xlate_hyp = function
478
| AI (_,id) -> xlate_ident id
479
| MetaId _ -> xlate_error "MetaId should occur only in quotations"
481
let xlate_hyp_location =
483
| (occs, AI (_,id)), InHypTypeOnly ->
484
CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
485
| (occs, AI (_,id)), InHypValueOnly ->
486
CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
487
| (occs, AI (_,id)), InHyp when occs = all_occurrences_expr ->
488
CT_coerce_UNFOLD_to_HYP_LOCATION
489
(CT_coerce_ID_to_UNFOLD (xlate_ident id))
490
| ((_,a::l as occs), AI (_,id)), InHyp ->
491
let nums = nums_of_occs occs in
492
let a = List.hd nums and l = List.tl nums in
493
CT_coerce_UNFOLD_to_HYP_LOCATION
494
(CT_unfold_occ (xlate_ident id,
495
CT_int_ne_list(num_or_var_to_int a,
496
nums_or_var_to_int_list_aux l)))
497
| (_, AI (_,id)), InHyp -> xlate_error "Unused" (* (true,]) *)
499
xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
503
let xlate_clause cls =
505
match cls.onhyps with
506
None -> CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR CT_star
507
| Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
510
if cls.concl_occs <> no_occurrences_expr then
511
CT_coerce_STAR_to_STAR_OPT CT_star
513
CT_coerce_NONE_to_STAR_OPT CT_none)
517
let strip_targ_spec_list =
519
| Targ_spec_list x -> x
520
| _ -> xlate_error "strip tactic: non binding-list argument";;
522
let strip_targ_binding =
524
| Targ_binding x -> x
525
| _ -> xlate_error "strip tactic: non-binding argument";;
527
let strip_targ_command =
529
| Targ_command x -> x
530
| Targ_binding_com x -> x
531
| _ -> xlate_error "strip tactic: non-command argument";;
533
let strip_targ_ident =
536
| _ -> xlate_error "strip tactic: non-ident argument";;
541
| _ -> xlate_error "strip tactic: non-int argument";;
543
let strip_targ_pattern =
545
| Targ_pattern x -> x
546
| _ -> xlate_error "strip tactic: non-pattern argument";;
548
let strip_targ_unfold =
551
| _ -> xlate_error "strip tactic: non-unfold argument";;
553
let strip_targ_fixtac =
556
| _ -> xlate_error "strip tactic: non-fixtac argument";;
558
let strip_targ_cofixtac =
560
| Targ_cofixtac x -> x
561
| _ -> xlate_error "strip tactic: non-cofixtac argument";;
563
(*Need to transform formula to id for "Prolog" tactic problem *)
564
let make_ID_from_FORMULA =
566
| CT_coerce_ID_to_FORMULA id -> id
567
| _ -> xlate_error "make_ID_from_FORMULA: non-formula argument";;
569
let make_ID_from_iTARG_FORMULA x = make_ID_from_FORMULA (strip_targ_command x);;
571
let xlate_quantified_hypothesis = function
572
| AnonHyp n -> CT_coerce_INT_to_ID_OR_INT (CT_int n)
573
| NamedHyp id -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id)
575
let xlate_quantified_hypothesis_opt = function
577
CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE
578
| Some (AnonHyp n) -> xlate_int_to_id_or_int_opt n
579
| Some (NamedHyp id) -> xlate_id_to_id_or_int_opt id;;
581
let xlate_id_or_int = function
582
ArgArg n -> CT_coerce_INT_to_ID_OR_INT(CT_int n)
583
| ArgVar(_, s) -> CT_coerce_ID_to_ID_OR_INT(xlate_ident s);;
585
let xlate_explicit_binding (loc,h,c) =
586
CT_binding (xlate_quantified_hypothesis h, xlate_formula c)
588
let xlate_bindings = function
589
| ImplicitBindings l ->
590
CT_coerce_FORMULA_LIST_to_SPEC_LIST
591
(CT_formula_list (List.map xlate_formula l))
592
| ExplicitBindings l ->
593
CT_coerce_BINDING_LIST_to_SPEC_LIST
594
(CT_binding_list (List.map xlate_explicit_binding l))
596
CT_coerce_FORMULA_LIST_to_SPEC_LIST (CT_formula_list [])
598
let strip_targ_spec_list =
600
| Targ_spec_list x -> x
601
| _ -> xlate_error "strip_tar_spec_list";;
603
let strip_targ_intropatt =
605
| Targ_intropatt x -> x
606
| _ -> xlate_error "strip_targ_intropatt";;
609
let conv_flags, red_ids =
610
let csts = List.map (apply_or_by_notation tac_qualid_to_ct_ID) r.rConst in
612
[CT_delta], CT_unfbut csts
615
then (* probably useless: just for compatibility *) []
618
let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in
619
let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in
620
let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in
621
(* Rem: EVAR flag obsol�te *)
624
let rec xlate_intro_pattern (loc,pat) = match pat with
625
| IntroOrAndPattern [] -> assert false
626
| IntroOrAndPattern (fp::ll) ->
628
(CT_intro_patt_list(List.map xlate_intro_pattern fp),
631
CT_intro_patt_list(List.map xlate_intro_pattern l))
633
| IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
634
| IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
635
| IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
636
| IntroFresh _ -> xlate_error "TODO: IntroFresh"
637
| IntroRewrite _ -> xlate_error "TODO: IntroRewrite"
639
let compute_INV_TYPE = function
640
FullInversionClear -> CT_inv_clear
641
| SimpleInversion -> CT_inv_simple
642
| FullInversion -> CT_inv_regular
644
let is_tactic_special_case = function
645
"AutoRewrite" -> true
648
let xlate_context_pattern = function
650
CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
651
| Subterm (b, idopt, v) -> (* TODO: application pattern *)
652
CT_context(xlate_ident_opt idopt, xlate_formula v)
655
let xlate_match_context_hyps = function
656
| Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b)
657
| Def (na,b,t) -> xlate_error "TODO: Let hyps"
658
(* CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b, xlate_context_pattern t);; *)
660
let xlate_arg_to_id_opt = function
661
Some id -> CT_coerce_ID_to_ID_OPT(CT_ident (string_of_id id))
662
| None -> ctv_ID_OPT_NONE;;
664
let xlate_largs_to_id_opt largs =
665
match List.map xlate_arg_to_id_opt largs with
666
fst::rest -> fst, rest
667
| _ -> assert false;;
669
let xlate_int_or_constr = function
670
ElimOnConstr (a,NoBindings) -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
671
| ElimOnConstr _ -> xlate_error "TODO: ElimOnConstr with bindings"
672
| ElimOnIdent(_,i) ->
673
CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
674
(CT_coerce_ID_to_ID_OR_INT(xlate_ident i))
676
CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
677
(CT_coerce_INT_to_ID_OR_INT(CT_int i));;
679
let xlate_using = function
680
None -> CT_coerce_NONE_to_USING(CT_none)
681
| Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
683
let xlate_one_unfold_block = function
685
CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid)
686
| (((_,_::_) as occs), qid) ->
687
let l = nums_of_occs occs in
688
CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid,
689
nums_or_var_to_int_ne_list (List.hd l) (List.tl l))
690
| ((false,[]), qid) -> xlate_error "Unused"
693
let xlate_with_names = function
694
None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
695
| Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
697
let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
699
let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
704
CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic t)
706
CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG
707
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
708
(CT_coerce_INT_to_ID_OR_INT (CT_int n)))
710
CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG
711
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
712
(CT_coerce_ID_to_ID_OR_INT (reference_to_ct_ID r)))
714
failwith "Dynamics not treated in xlate_ast"
715
| ConstrMayEval (ConstrTerm c) ->
716
CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG
717
(CT_coerce_FORMULA_to_FORMULA_OR_INT (xlate_formula c))
718
| ConstrMayEval(ConstrEval(r,c)) ->
719
CT_coerce_EVAL_CMD_to_TACTIC_ARG
720
(CT_eval(CT_coerce_NONE_to_INT_OPT CT_none, xlate_red_tactic r,
722
| ConstrMayEval(ConstrTypeOf(c)) ->
723
CT_coerce_TERM_CHANGE_to_TACTIC_ARG(CT_check_term(xlate_formula c))
725
xlate_error "MetaIdArg should only be used in quotations"
727
CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_call_or_tacarg t)
729
and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) =
731
(* Moved from xlate_tactic *)
732
| TacCall (_, r, a::l) ->
734
(reference_to_ct_ID r,
735
CT_tactic_arg_list(xlate_tacarg a,List.map xlate_tacarg l))
736
| Reference (Ident (_,s)) -> ident_tac s
737
| ConstrMayEval(ConstrTerm a) ->
738
CT_formula_marker(xlate_formula a)
739
| TacFreshId [] -> CT_fresh(ctf_STRING_OPT None)
740
| TacFreshId [ArgArg s] -> CT_fresh(ctf_STRING_OPT (Some s))
741
| TacFreshId _ -> xlate_error "TODO: fresh with many args"
742
| t -> xlate_error "TODO LATER: result other than tactic or constr"
744
and xlate_red_tactic =
746
| Red true -> xlate_error ""
747
| Red false -> CT_red
750
| Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
751
| Simpl (Some (occs,c)) ->
752
let l = nums_of_occs occs in
754
(CT_coerce_PATTERN_to_PATTERN_OPT
756
(CT_int_list(nums_or_var_to_int_list_aux l), xlate_formula c)))
758
let conv_flags, red_ids = get_flag flag_list in
759
CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
761
let conv_flags, red_ids = get_flag flag_list in
762
CT_lazy (CT_conversion_flag_list conv_flags, red_ids)
764
let ct_unf_list = List.map xlate_one_unfold_block unf_list in
765
(match ct_unf_list with
766
| first :: others -> CT_unfold (CT_unfold_ne_list (first, others))
767
| [] -> error "there should be at least one thing to unfold")
768
| Fold formula_list ->
769
CT_fold(CT_formula_list(List.map xlate_formula formula_list))
771
let pat_list = List.map (fun (occs,c) ->
773
(CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)),
774
xlate_formula c)) l in
776
| first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
777
| [] -> error "Expecting at least one pattern in a Pattern command")
778
| ExtraRedExpr _ -> xlate_error "TODO LATER: ExtraRedExpr (probably dead code)"
780
and xlate_local_rec_tac = function
781
(* TODO LATER: local recursive tactics and global ones should be handled in
783
| ((_,x),Tacexp (TacFun (argl,tac))) ->
784
let fst, rest = xlate_largs_to_id_opt argl in
785
CT_rec_tactic_fun(xlate_ident x,
786
CT_id_opt_ne_list(fst, rest),
788
| _ -> xlate_error "TODO: more general argument of 'let rec in'"
792
| TacFun (largs, t) ->
793
let fst, rest = xlate_largs_to_id_opt largs in
794
CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
795
| TacThen (t1,[||],t2,[||]) ->
796
(match xlate_tactic t1 with
797
CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
798
| t -> CT_then (t,[xlate_tactic t2]))
799
| TacThen _ -> xlate_error "TacThen generalization TODO"
800
| TacThens(t1,[]) -> assert false
801
| TacThens(t1,t::l) ->
802
let ct = xlate_tactic t in
803
let cl = List.map xlate_tactic l in
804
(match xlate_tactic t1 with
805
CT_then(ct1,cl1) -> CT_then(ct1, cl1@[CT_parallel(ct, cl)])
806
| ct1 -> CT_then(ct1,[CT_parallel(ct, cl)]))
807
| TacFirst([]) -> assert false
808
| TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
809
| TacSolve([]) -> assert false
810
| TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
811
| TacComplete _ -> xlate_error "TODO: tactical complete"
812
| TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
813
| TacTry t -> CT_try (xlate_tactic t)
814
| TacRepeat t -> CT_repeat(xlate_tactic t)
815
| TacAbstract(t,id_opt) ->
816
CT_abstract((match id_opt with
817
None -> ctv_ID_OPT_NONE
818
| Some id -> ctf_ID_OPT_SOME (CT_ident (string_of_id id))),
820
| TacProgress t -> CT_progress(xlate_tactic t)
821
| TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
822
| TacMatch (true,_,_) -> failwith "TODO: lazy match"
823
| TacMatch (false, exp, rules) ->
824
CT_match_tac(xlate_tactic exp,
828
CT_match_tac_rule(xlate_context_pattern p,
830
| Pat (_,p,tac) -> xlate_error"No hyps in pure Match"
833
(CT_coerce_FORMULA_to_CONTEXT_PATTERN
835
mk_let_value tac)) rules with
838
CT_match_tac_rules(fst, others))
839
| TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
840
| TacMatchGoal (false,false,rule1::rules) ->
841
CT_match_context(xlate_context_rule rule1,
842
List.map xlate_context_rule rules)
843
| TacMatchGoal (false,true,rule1::rules) ->
844
CT_match_context_reverse(xlate_context_rule rule1,
845
List.map xlate_context_rule rules)
846
| TacLetIn (false, l, t) ->
849
((_,s),ConstrMayEval v) ->
850
CT_let_clause(xlate_ident s,
851
CT_coerce_NONE_to_TACTIC_OPT CT_none,
852
CT_coerce_DEF_BODY_to_LET_VALUE
853
(formula_to_def_body v))
854
| ((_,s),Tacexp t) ->
855
CT_let_clause(xlate_ident s,
856
CT_coerce_NONE_to_TACTIC_OPT CT_none,
857
CT_coerce_TACTIC_COM_to_LET_VALUE
860
CT_let_clause(xlate_ident s,
861
CT_coerce_NONE_to_TACTIC_OPT CT_none,
862
CT_coerce_TACTIC_COM_to_LET_VALUE
863
(xlate_call_or_tacarg t)) in
864
let cl_l = List.map cvt_clause l in
868
CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t))
869
| TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition"
870
| TacLetIn(true, f1::l, t) ->
871
let tl = CT_rec_tactic_fun_list
872
(xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
873
CT_rec_tactic_in(tl, xlate_tactic t)
874
| TacAtom (_, t) -> xlate_tac t
875
| TacFail (count, []) -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
876
| TacFail (count, [MsgString s]) -> CT_fail(xlate_id_or_int count,
877
ctf_STRING_OPT_SOME (CT_string s))
878
| TacFail (count, _) -> xlate_error "TODO: generic fail message"
879
| TacId [] -> CT_idtac ctf_STRING_OPT_NONE
880
| TacId [MsgString s] -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
881
| TacId _ -> xlate_error "TODO: generic idtac message"
882
| TacInfo t -> CT_info(xlate_tactic t)
883
| TacArg a -> xlate_call_or_tacarg a
887
| TacExtend (_, "firstorder", tac_opt::l) ->
890
out_gen (wit_opt rawwit_main_tactic) tac_opt
892
| None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
893
| Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in
895
[] -> CT_firstorder t1
897
(match genarg_tag l1 with
898
List1ArgType PreIdentArgType ->
900
(fun x -> CT_ident x)
901
(out_gen (wit_list1 rawwit_pre_ident) l1) in
903
match l2 with fst::l3 -> fst,l3 | [] -> assert false in
904
CT_firstorder_using(t1, CT_id_ne_list(fst, l3))
905
| List1ArgType RefArgType ->
906
let l2 = List.map reference_to_ct_ID
907
(out_gen (wit_list1 rawwit_ref) l1) in
909
match l2 with fst::l3 -> fst, l3 | [] -> assert false in
910
CT_firstorder_with(t1, CT_id_ne_list(fst, l3))
913
| TacExtend (_, "refine", [c]) ->
914
CT_refine (xlate_formula (snd (out_gen rawwit_casted_open_constr c)))
915
| TacExtend (_,"absurd",[c]) ->
916
CT_absurd (xlate_formula (out_gen rawwit_constr c))
917
| TacExtend (_,"contradiction",[opt_c]) ->
918
(match out_gen (wit_opt rawwit_constr_with_bindings) opt_c with
919
None -> CT_contradiction
921
let c1 = xlate_formula c in
922
let bindings = xlate_bindings b in
923
CT_contradiction_thm(c1, bindings))
924
| TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
925
| TacChange (Some(l,c), f, b) ->
926
(* TODO LATER: combine with other constructions of pattern_occ *)
927
let l = nums_of_occs l in
929
CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l),
933
| TacExtend (_,"contradiction",[]) -> CT_contradiction
934
| TacDoubleInduction (n1, n2) ->
935
CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
936
| TacExtend (_,"discriminate", []) ->
937
CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
938
| TacExtend (_,"discriminate", [id]) ->
940
(xlate_quantified_hypothesis_opt
941
(Some (out_gen rawwit_quant_hyp id)))
942
| TacExtend (_,"simplify_eq", []) ->
943
CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT
944
(CT_coerce_NONE_to_ID_OPT CT_none))
945
| TacExtend (_,"simplify_eq", [id]) ->
946
let id1 = out_gen rawwit_quant_hyp id in
947
let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
948
(xlate_quantified_hypothesis id1) in
950
| TacExtend (_,"injection", []) ->
951
CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
952
| TacExtend (_,"injection", [id]) ->
954
(xlate_quantified_hypothesis_opt
955
(Some (out_gen rawwit_quant_hyp id)))
956
| TacExtend (_,"injection_as", [idopt;ipat]) ->
957
xlate_error "TODO: injection as"
958
| TacFix (idopt, n) ->
959
CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
960
| TacMutualFix (false, id, n, fixtac_list) ->
961
let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in
963
(ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
964
CT_fix_tac_list (List.map f fixtac_list))
965
| TacMutualFix (true, id, n, fixtac_list) ->
966
xlate_error "TODO: non user-visible fix"
968
CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
969
| TacMutualCofix (false, id, cofixtac_list) ->
970
let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in
972
(CT_coerce_ID_to_ID_OPT (xlate_ident id),
973
CT_cofix_tac_list (List.map f cofixtac_list))
974
| TacMutualCofix (true, id, cofixtac_list) ->
975
xlate_error "TODO: non user-visible cofix"
976
| TacIntrosUntil (NamedHyp id) ->
977
CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
978
| TacIntrosUntil (AnonHyp n) ->
979
CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n))
980
| TacIntroMove (Some id1, MoveAfter id2) ->
981
CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_hyp id2)
982
| TacIntroMove (None, MoveAfter id2) ->
983
CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_hyp id2)
984
| TacMove (true, id1, MoveAfter id2) ->
985
CT_move_after(xlate_hyp id1, xlate_hyp id2)
986
| TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
987
| TacMove _ -> xlate_error "TODO: move before, at top, at bottom"
988
| TacIntroPattern patt_list ->
990
(CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
991
| TacIntroMove (Some id, MoveToEnd true) ->
992
CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
993
| TacIntroMove (None, MoveToEnd true) ->
994
CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
995
| TacIntroMove _ -> xlate_error "TODO"
996
| TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
997
| TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
998
| TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
999
| TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl)
1000
| TacSplit _ | TacRight _ | TacLeft _ ->
1001
xlate_error "TODO: esplit, eright, etc"
1002
| TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
1003
let c1 = xlate_formula (out_gen rawwit_constr c1) in
1004
let c2 = xlate_formula (out_gen rawwit_constr c2) in
1006
(* J.F. : 18/08/2006
1007
Hack to coerce the "clause" argument of replace to a real clause
1008
To be remove if we can reuse the clause grammar entrie defined in g_tactic
1010
let cl_as_clause = Extraargs.raw_in_arg_hyp_to_clause (out_gen Extraargs.rawwit_in_arg_hyp cl) in
1011
let cl_as_xlate_arg =
1016
List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
1018
cl_as_clause.Tacexpr.onhyps
1023
let cl = xlate_clause cl in
1025
match out_gen (Extraargs.rawwit_by_arg_tac) tac_opt with
1026
| None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
1028
let tac = xlate_tactic tac in
1029
CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
1031
CT_replace_with (c1, c2,cl,tac_opt)
1032
| TacRewrite(false,[b,Precisely 1,cbindl],cl,None) ->
1033
let cl = xlate_clause cl
1034
and c = xlate_formula (fst cbindl)
1035
and bindl = xlate_bindings (snd cbindl) in
1036
if b then CT_rewrite_lr (c, bindl, cl)
1037
else CT_rewrite_rl (c, bindl, cl)
1038
| TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by"
1039
| TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once"
1040
| TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite"
1041
| TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
1042
let t = out_gen rawwit_main_tactic t in
1043
let b = out_gen Extraargs.rawwit_orient b in
1044
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
1045
let c = xlate_formula c and bindl = xlate_bindings bindl in
1046
if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
1047
else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
1048
| TacExtend (_,"conditional_rewrite", [t; b; cbindl; id]) ->
1049
let t = out_gen rawwit_main_tactic t in
1050
let b = out_gen Extraargs.rawwit_orient b in
1051
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
1052
let c = xlate_formula c and bindl = xlate_bindings bindl in
1053
let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
1054
if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id)
1055
else CT_condrewrite_rl (xlate_tactic t, c, bindl, id)
1056
| TacExtend (_,"dependent_rewrite", [b; c]) ->
1057
let b = out_gen Extraargs.rawwit_orient b in
1058
let c = xlate_formula (out_gen rawwit_constr c) in
1060
| CT_coerce_ID_to_FORMULA (CT_ident _ as id) ->
1061
if b then CT_deprewrite_lr id else CT_deprewrite_rl id
1062
| _ -> xlate_error "dependent rewrite on term: not supported")
1063
| TacExtend (_,"dependent_rewrite", [b; c; id]) ->
1064
xlate_error "dependent rewrite on terms in hypothesis: not supported"
1065
| TacExtend (_,"cut_rewrite", [b; c]) ->
1066
let b = out_gen Extraargs.rawwit_orient b in
1067
let c = xlate_formula (out_gen rawwit_constr c) in
1068
if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
1069
else CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
1070
| TacExtend (_,"cut_rewrite", [b; c; id]) ->
1071
let b = out_gen Extraargs.rawwit_orient b in
1072
let c = xlate_formula (out_gen rawwit_constr c) in
1073
let id = xlate_ident (snd (out_gen rawwit_var id)) in
1074
if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
1075
else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
1076
| TacExtend(_, "subst", [l]) ->
1079
(List.map (fun x -> CT_ident (string_of_id x))
1080
(out_gen (wit_list1 rawwit_ident) l)))
1081
| TacReflexivity -> CT_reflexivity
1082
| TacSymmetry cls -> CT_symmetry(xlate_clause cls)
1083
| TacTransitivity c -> CT_transitivity (xlate_formula c)
1084
| TacAssumption -> CT_assumption
1085
| TacExact c -> CT_exact (xlate_formula c)
1086
| TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
1087
| TacVmCastNoCheck c -> CT_vm_cast_no_check (xlate_formula c)
1088
| TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id)
1089
| TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id)
1090
| TacDestructConcl -> CT_dconcl
1091
| TacSuperAuto (nopt,l,a3,a4) ->
1094
xlate_qualid_list l,
1095
(if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
1096
(if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
1097
| TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
1098
| TacAuto (nopt, [], Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
1099
| TacAuto (nopt, [], None) ->
1100
CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
1101
CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
1102
| TacAuto (nopt, [], Some (id1::idl)) ->
1103
CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
1104
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
1105
CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
1106
| TacAuto (nopt, _::_, _) ->
1107
xlate_error "TODO: auto using"
1108
|TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
1109
let (id_list:ct_ID list) =
1110
List.map (fun x -> CT_ident x) (out_gen (wit_list1 rawwit_pre_ident) l) in
1111
let fst, (id_list1: ct_ID list) =
1112
match id_list with [] -> assert false | a::tl -> a,tl in
1116
CT_coerce_TACTIC_COM_to_TACTIC_OPT
1117
(xlate_tactic(out_gen rawwit_main_tactic t0))
1118
| [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
1119
| _ -> assert false in
1120
CT_autorewrite (CT_id_ne_list(fst, id_list1), t1)
1121
| TacExtend (_,"eauto", [nopt; popt; lems; idl]) ->
1123
match out_gen (wit_opt rawwit_int_or_var) nopt with
1124
| Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
1125
| Some (ArgArg n) -> xlate_int_to_id_or_int_opt n
1126
| None -> none_in_id_or_int_opt in
1128
match out_gen (wit_opt rawwit_int_or_var) popt with
1129
| Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
1130
| Some (ArgArg n) -> xlate_int_to_id_or_int_opt n
1131
| None -> none_in_id_or_int_opt in
1133
match out_gen Eauto.rawwit_auto_using lems with
1135
| _ -> xlate_error "TODO: eauto using" in
1136
let idl = out_gen Eauto.rawwit_hintbases idl in
1138
None -> CT_eauto_with(first_n,
1140
CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
1141
| Some [] -> CT_eauto(first_n, second_n)
1143
CT_eauto_with(first_n, second_n,
1144
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR
1147
List.map (fun x -> CT_ident x) l))))
1148
| TacExtend (_,"prolog", [cl; n]) ->
1149
let cl = List.map xlate_formula (out_gen (wit_list0 rawwit_constr) cl) in
1150
(match out_gen rawwit_int_or_var n with
1151
| ArgVar _ -> xlate_error ""
1152
| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int n))
1153
(* eapply now represented by TacApply (true,cbindl)
1154
| TacExtend (_,"eapply", [cbindl]) ->
1156
| TacTrivial ([],Some []) -> CT_trivial
1157
| TacTrivial ([],None) ->
1158
CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
1159
| TacTrivial ([],Some (id1::idl)) ->
1160
CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
1161
(CT_id_ne_list(CT_ident id1,List.map (fun x -> CT_ident x) idl))))
1162
| TacTrivial (_::_,_) ->
1163
xlate_error "TODO: trivial using"
1164
| TacReduce (red, l) ->
1165
CT_reduce (xlate_red_tactic red, xlate_clause l)
1166
| TacApply (true,false,[c,bindl],None) ->
1167
CT_apply (xlate_formula c, xlate_bindings bindl)
1168
| TacApply (true,true,[c,bindl],None) ->
1169
CT_eapply (xlate_formula c, xlate_bindings bindl)
1170
| TacApply (_,_,_,_) ->
1171
xlate_error "TODO: simple (e)apply and iterated apply and apply in"
1172
| TacConstructor (false,n_or_meta, bindl) ->
1173
let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
1174
in CT_constructor (CT_int n, xlate_bindings bindl)
1175
| TacConstructor _ -> xlate_error "TODO: econstructor"
1176
| TacSpecialize (nopt, (c,sl)) ->
1177
CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
1178
| TacGeneralize [] -> xlate_error ""
1179
| TacGeneralize ((((true,[]),first),Anonymous) :: cl)
1180
when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr
1181
& na = Anonymous) cl ->
1183
(CT_formula_ne_list (xlate_formula first,
1184
List.map (fun ((_,c),_) -> xlate_formula c) cl))
1185
| TacGeneralize _ -> xlate_error "TODO: Generalize at and as"
1186
| TacGeneralizeDep c ->
1187
CT_generalize_dependent (xlate_formula c)
1188
| TacElimType c -> CT_elim_type (xlate_formula c)
1189
| TacCaseType c -> CT_case_type (xlate_formula c)
1190
| TacElim (false,(c1,sl), u) ->
1191
CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
1192
| TacCase (false,(c1,sl)) ->
1193
CT_casetac (xlate_formula c1, xlate_bindings sl)
1194
| TacElim (true,_,_) | TacCase (true,_)
1195
| TacInductionDestruct (_,true,_) ->
1196
xlate_error "TODO: eelim, ecase, edestruct, einduction"
1197
| TacSimpleInductionDestruct (true,h) ->
1198
CT_induction (xlate_quantified_hypothesis h)
1199
| TacSimpleInductionDestruct (false,h) ->
1200
CT_destruct (xlate_quantified_hypothesis h)
1201
| TacCut c -> CT_cut (xlate_formula c)
1202
| TacLApply c -> CT_use (xlate_formula c)
1203
| TacDecompose ([],c) ->
1204
xlate_error "Decompose : empty list of identifiers?"
1205
| TacDecompose (id::l,c) ->
1206
let id' = apply_or_by_notation tac_qualid_to_ct_ID id in
1207
let l' = List.map (apply_or_by_notation tac_qualid_to_ct_ID) l in
1208
CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
1209
| TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
1210
| TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
1211
| TacClear (false,[]) ->
1212
xlate_error "Clear expects a non empty list of identifiers"
1213
| TacClear (false,id::idl) ->
1214
let idl' = List.map xlate_hyp idl in
1215
CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
1216
| TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
1217
| TacRevert _ -> xlate_error "TODO: revert"
1218
| (*For translating tactics/Inv.v *)
1219
TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
1220
CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
1222
CT_id_list (List.map xlate_hyp idl))
1223
| TacInversion (DepInversion (k,copt,l),quant_hyp) ->
1224
let id = xlate_quantified_hypothesis quant_hyp in
1225
CT_depinversion (compute_INV_TYPE k, id,
1226
xlate_with_names l, xlate_formula_opt copt)
1227
| TacInversion (InversionUsing (c,idlist), id) ->
1228
let id = xlate_quantified_hypothesis id in
1229
CT_use_inversion (id, xlate_formula c,
1230
CT_id_list (List.map xlate_hyp idlist))
1231
| TacExtend (_,"omega", []) -> CT_omega
1232
| TacRename [id1, id2] -> CT_rename(xlate_hyp id1, xlate_hyp id2)
1233
| TacRename _ -> xlate_error "TODO: add support for n-ary rename"
1234
| TacClearBody([]) -> assert false
1235
| TacClearBody(a::l) ->
1236
CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
1237
| TacDAuto (a, b, []) ->
1238
CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
1239
| TacDAuto (a, b, _) ->
1240
xlate_error "TODO: dauto using"
1241
| TacInductionDestruct(true,false,[a,b,(None,c),None]) ->
1243
(List.map xlate_int_or_constr a, xlate_using b,
1245
| TacInductionDestruct(false,false,[a,b,(None,c),None]) ->
1247
(List.map xlate_int_or_constr a, xlate_using b,
1249
| TacInductionDestruct(_,false,_) ->
1250
xlate_error "TODO: clause 'in' and full 'as' of destruct/induction"
1251
| TacLetTac (na, c, cl, true) when cl = nowhere ->
1252
CT_pose(xlate_id_opt_aux na, xlate_formula c)
1253
| TacLetTac (na, c, cl, true) ->
1254
CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
1255
(* TODO LATER: This should be shared with Unfold,
1256
but the structures are different *)
1258
| TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
1259
| TacAssert (None, Some (_,IntroIdentifier id), c) ->
1260
CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
1261
| TacAssert (None, None, c) ->
1262
CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
1263
| TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) ->
1264
CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
1265
| TacAssert (Some (TacId []), None, c) ->
1266
CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
1268
xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
1269
| TacAnyConstructor(false,Some tac) ->
1271
(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
1272
| TacAnyConstructor(false,None) ->
1273
CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none)
1274
| TacAnyConstructor _ -> xlate_error "TODO: econstructor"
1275
| TacExtend(_, "ring", [args]) ->
1278
(List.map xlate_formula
1279
(out_gen (wit_list0 rawwit_constr) args)))
1280
| TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal"
1281
| TacExtend (_,id, l) ->
1282
print_endline ("Extratactics : "^ id);
1283
CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
1284
| TacAlias _ -> xlate_error "Alias not supported"
1286
and coerce_genarg_to_TARG x =
1287
match Genarg.genarg_tag x with
1289
| BoolArgType -> xlate_error "TODO: generic boolean argument"
1291
let n = out_gen rawwit_int x in
1292
CT_coerce_FORMULA_OR_INT_to_TARG
1293
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
1294
(CT_coerce_INT_to_ID_OR_INT (CT_int n)))
1295
| IntOrVarArgType ->
1296
let x = match out_gen rawwit_int_or_var x with
1297
| ArgArg n -> CT_coerce_INT_to_ID_OR_INT (CT_int n)
1298
| ArgVar (_,id) -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id) in
1299
CT_coerce_FORMULA_OR_INT_to_TARG
1300
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT x)
1302
let s = CT_string (out_gen rawwit_string x) in
1303
CT_coerce_SCOMMENT_CONTENT_to_TARG
1304
(CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT
1305
(CT_coerce_STRING_to_ID_OR_STRING s))
1306
| PreIdentArgType ->
1307
let id = CT_ident (out_gen rawwit_pre_ident x) in
1308
CT_coerce_FORMULA_OR_INT_to_TARG
1309
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
1310
(CT_coerce_ID_to_ID_OR_INT id))
1311
| IntroPatternArgType ->
1313
| IdentArgType true ->
1314
let id = xlate_ident (out_gen rawwit_ident x) in
1315
CT_coerce_FORMULA_OR_INT_to_TARG
1316
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
1317
(CT_coerce_ID_to_ID_OR_INT id))
1318
| IdentArgType false ->
1321
let id = xlate_ident (snd (out_gen rawwit_var x)) in
1322
CT_coerce_FORMULA_OR_INT_to_TARG
1323
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
1324
(CT_coerce_ID_to_ID_OR_INT id))
1326
let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
1327
CT_coerce_FORMULA_OR_INT_to_TARG
1328
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
1329
(CT_coerce_ID_to_ID_OR_INT id))
1330
(* Specific types *)
1332
CT_coerce_SCOMMENT_CONTENT_to_TARG
1333
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT
1334
(CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x))))
1336
CT_coerce_SCOMMENT_CONTENT_to_TARG
1337
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
1338
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
1339
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
1340
| OpenConstrArgType b ->
1341
CT_coerce_SCOMMENT_CONTENT_to_TARG
1342
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
1344
(rawwit_open_constr_gen b) x))))
1345
| ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
1346
let n = Option.get (Pcoq.tactic_genarg_level s) in
1347
let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
1348
CT_coerce_TACTIC_COM_to_TARG t
1349
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
1350
| BindingsArgType -> xlate_error "TODO: generic with bindings"
1351
| RedExprArgType -> xlate_error "TODO: generic red expr"
1352
| List0ArgType l -> xlate_error "TODO: lists of generic arguments"
1353
| List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
1354
| OptArgType x -> xlate_error "TODO: optional generic arguments"
1355
| PairArgType (u,v) -> xlate_error "TODO: pairs of generic arguments"
1356
| ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
1357
and xlate_context_rule =
1359
| Pat (hyps, concl_pat, tactic) ->
1361
(CT_context_hyp_list (List.map xlate_match_context_hyps hyps),
1362
xlate_context_pattern concl_pat, xlate_tactic tactic)
1364
CT_def_context_rule (xlate_tactic tactic)
1365
and formula_to_def_body =
1367
| ConstrEval (red, f) ->
1368
CT_coerce_EVAL_CMD_to_DEF_BODY(
1369
CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
1370
xlate_red_tactic red, xlate_formula f))
1371
| ConstrContext((_, id), f) ->
1372
CT_coerce_CONTEXT_PATTERN_to_DEF_BODY
1374
(CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id id)),
1376
| ConstrTypeOf f -> CT_type_of (xlate_formula f)
1377
| ConstrTerm c -> ct_coerce_FORMULA_to_DEF_BODY(xlate_formula c)
1379
and mk_let_value = function
1380
TacArg (ConstrMayEval v) ->
1381
CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body v)
1382
| v -> CT_coerce_TACTIC_COM_to_LET_VALUE(xlate_tactic v);;
1384
let coerce_genarg_to_VARG x =
1385
match Genarg.genarg_tag x with
1387
| BoolArgType -> xlate_error "TODO: generic boolean argument"
1389
let n = out_gen rawwit_int x in
1390
CT_coerce_ID_OR_INT_OPT_to_VARG
1391
(CT_coerce_INT_OPT_to_ID_OR_INT_OPT
1392
(CT_coerce_INT_to_INT_OPT (CT_int n)))
1393
| IntOrVarArgType ->
1394
(match out_gen rawwit_int_or_var x with
1396
CT_coerce_ID_OR_INT_OPT_to_VARG
1397
(CT_coerce_INT_OPT_to_ID_OR_INT_OPT
1398
(CT_coerce_INT_to_INT_OPT (CT_int n)))
1400
CT_coerce_ID_OPT_OR_ALL_to_VARG
1401
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
1402
(CT_coerce_ID_to_ID_OPT (xlate_ident id))))
1404
let s = CT_string (out_gen rawwit_string x) in
1405
CT_coerce_STRING_OPT_to_VARG (CT_coerce_STRING_to_STRING_OPT s)
1406
| PreIdentArgType ->
1407
let id = CT_ident (out_gen rawwit_pre_ident x) in
1408
CT_coerce_ID_OPT_OR_ALL_to_VARG
1409
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
1410
(CT_coerce_ID_to_ID_OPT id))
1411
| IntroPatternArgType ->
1413
| IdentArgType true ->
1414
let id = xlate_ident (out_gen rawwit_ident x) in
1415
CT_coerce_ID_OPT_OR_ALL_to_VARG
1416
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
1417
(CT_coerce_ID_to_ID_OPT id))
1418
| IdentArgType false ->
1421
let id = xlate_ident (snd (out_gen rawwit_var x)) in
1422
CT_coerce_ID_OPT_OR_ALL_to_VARG
1423
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
1424
(CT_coerce_ID_to_ID_OPT id))
1426
let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
1427
CT_coerce_ID_OPT_OR_ALL_to_VARG
1428
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
1429
(CT_coerce_ID_to_ID_OPT id))
1430
(* Specific types *)
1432
CT_coerce_FORMULA_OPT_to_VARG
1433
(CT_coerce_FORMULA_to_FORMULA_OPT
1434
(CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x))))
1436
CT_coerce_FORMULA_OPT_to_VARG
1437
(CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
1438
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
1439
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
1440
| ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
1441
let n = Option.get (Pcoq.tactic_genarg_level s) in
1442
let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
1443
CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
1444
| OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
1445
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
1446
| BindingsArgType -> xlate_error "TODO: generic with bindings"
1447
| RedExprArgType -> xlate_error "TODO: red expr as generic argument"
1448
| List0ArgType l -> xlate_error "TODO: lists of generic arguments"
1449
| List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
1450
| OptArgType x -> xlate_error "TODO: optional generic arguments"
1451
| PairArgType (u,v) -> xlate_error "TODO: pairs of generic arguments"
1452
| ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
1455
let xlate_thm x = CT_thm (string_of_theorem_kind x)
1457
let xlate_defn k = CT_defn (string_of_definition_kind k)
1459
let xlate_var x = CT_var (match x with
1460
| (Global,Definitional) -> "Parameter"
1461
| (Global,Logical) -> "Axiom"
1462
| (Local,Definitional) -> "Variable"
1463
| (Local,Logical) -> "Hypothesis"
1464
| (Global,Conjectural) -> "Conjecture"
1465
| (Local,Conjectural) -> xlate_error "No local conjecture");;
1470
| true -> CT_dep "Induction for"
1471
| false -> CT_dep "Minimality for";;
1475
| GoTo n -> CT_coerce_INT_to_INT_OR_LOCN (CT_int n)
1476
| GoTop -> CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "top")
1477
| GoPrev -> CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "prev")
1478
| GoNext -> CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "next")
1480
let xlate_search_restr =
1482
| SearchOutside [] -> CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none
1483
| SearchInside (m1::l1) ->
1484
CT_in_modules (CT_id_ne_list(loc_qualid_to_ct_ID m1,
1485
List.map loc_qualid_to_ct_ID l1))
1486
| SearchOutside (m1::l1) ->
1487
CT_out_modules (CT_id_ne_list(loc_qualid_to_ct_ID m1,
1488
List.map loc_qualid_to_ct_ID l1))
1489
| SearchInside [] -> xlate_error "bad extra argument for Search"
1493
| "CHECK" -> "Check"
1494
| "PRINTTYPE" -> "Type"
1495
| _ -> xlate_error "xlate_check";;
1497
let build_constructors l =
1498
let f (coe,((_,id),c)) =
1499
if coe then CT_constr_coercion (xlate_ident id, xlate_formula c)
1500
else CT_constr (xlate_ident id, xlate_formula c) in
1501
CT_constr_list (List.map f l)
1503
let build_record_field_list l =
1504
let build_record_field ((coe,d),not) = match d with
1505
| AssumExpr (id,c) ->
1506
if coe then CT_recconstr_coercion (xlate_id_opt id, xlate_formula c)
1508
CT_recconstr(xlate_id_opt id, xlate_formula c)
1509
| DefExpr (id,c,topt) ->
1511
CT_defrecconstr_coercion(xlate_id_opt id, xlate_formula c,
1512
xlate_formula_opt topt)
1514
CT_defrecconstr(xlate_id_opt id, xlate_formula c, xlate_formula_opt topt) in
1515
CT_recconstr_list (List.map build_record_field l);;
1517
let get_require_flags impexp spec =
1520
| None -> CT_coerce_NONE_to_IMPEXP CT_none
1521
| Some false -> CT_import
1522
| Some true -> CT_export in
1525
| None -> ctv_SPEC_OPT_NONE
1526
| Some true -> CT_spec
1527
| Some false -> ctv_SPEC_OPT_NONE in
1528
ct_impexp, ct_spec;;
1530
let cvt_optional_eval_for_definition c1 optional_eval =
1531
match optional_eval with
1532
None -> ct_coerce_FORMULA_to_DEF_BODY (xlate_formula c1)
1534
CT_coerce_EVAL_CMD_to_DEF_BODY(
1535
CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
1536
xlate_red_tactic red,
1539
let cvt_vernac_binder = function
1543
(xlate_ident_opt (Some (snd id)),
1544
List.map (fun id -> xlate_ident_opt (Some (snd id))) idl),
1547
CT_binder_coercion(l,t)
1550
| _, _ -> xlate_error "binder with no left part, rejected";;
1552
let cvt_vernac_binders = function
1553
a::args -> CT_binder_ne_list(cvt_vernac_binder a, List.map cvt_vernac_binder args)
1554
| [] -> assert false;;
1557
let xlate_comment = function
1558
CommentConstr c -> CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula c)
1559
| CommentString s -> CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT
1560
(CT_coerce_STRING_to_ID_OR_STRING(CT_string s))
1562
CT_coerce_FORMULA_to_SCOMMENT_CONTENT
1563
(CT_coerce_NUM_to_FORMULA(CT_int_encapsulator (string_of_int n)));;
1565
let translate_opt_notation_decl = function
1566
None -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none)
1570
None -> ctv_ID_OPT_NONE
1571
| Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in
1572
CT_decl_notation(CT_string s, xlate_formula f, tr_sc);;
1574
let xlate_level = function
1575
Extend.NumLevel n -> CT_coerce_INT_to_INT_OR_NEXT(CT_int n)
1576
| Extend.NextLevel -> CT_next_level;;
1578
let xlate_syntax_modifier = function
1579
Extend.SetItemLevel((s::sl), level) ->
1581
(CT_id_ne_list(CT_ident s, List.map (fun s -> CT_ident s) sl),
1583
| Extend.SetItemLevel([], _) -> assert false
1584
| Extend.SetLevel level -> CT_set_level (CT_int level)
1585
| Extend.SetAssoc Gramext.LeftA -> CT_lefta
1586
| Extend.SetAssoc Gramext.RightA -> CT_righta
1587
| Extend.SetAssoc Gramext.NonA -> CT_nona
1588
| Extend.SetEntryType(x,typ) ->
1589
CT_entry_type(CT_ident x,
1591
Extend.ETIdent -> CT_ident "ident"
1592
| Extend.ETReference -> CT_ident "global"
1593
| Extend.ETBigint -> CT_ident "bigint"
1594
| _ -> xlate_error "syntax_type not parsed")
1595
| Extend.SetOnlyParsing -> CT_only_parsing
1596
| Extend.SetFormat(_,s) -> CT_format(CT_string s);;
1599
let rec xlate_module_type = function
1600
| CMTEident(_, qid) ->
1601
CT_coerce_ID_to_MODULE_TYPE(CT_ident (xlate_qualid qid))
1602
| CMTEwith(mty, decl) ->
1603
let mty1 = xlate_module_type mty in
1605
CWith_Definition((_, idl), c) ->
1606
CT_module_type_with_def(mty1,
1607
CT_id_list (List.map xlate_ident idl),
1609
| CWith_Module((_, idl), (_, qid)) ->
1610
CT_module_type_with_mod(mty1,
1611
CT_id_list (List.map xlate_ident idl),
1612
CT_ident (xlate_qualid qid)))
1613
| CMTEapply (_,_) -> xlate_error "TODO: Funsig application";;
1616
let xlate_module_binder_list (l:module_binder list) =
1617
CT_module_binder_list
1618
(List.map (fun (_, idl, mty) ->
1620
List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in
1621
let fst,idl2 = match idl1 with
1623
| fst::idl2 -> fst,idl2 in
1625
(CT_id_ne_list(fst, idl2), xlate_module_type mty)) l);;
1627
let xlate_module_type_check_opt = function
1628
None -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
1629
(CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE)
1630
| Some(mty, true) -> CT_only_check(xlate_module_type mty)
1631
| Some(mty, false) ->
1632
CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
1633
(CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
1634
(xlate_module_type mty));;
1636
let rec xlate_module_expr = function
1637
CMEident (_, qid) -> CT_coerce_ID_OPT_to_MODULE_EXPR
1638
(CT_coerce_ID_to_ID_OPT (CT_ident (xlate_qualid qid)))
1639
| CMEapply (me1, me2) -> CT_module_app(xlate_module_expr me1,
1640
xlate_module_expr me2)
1642
let rec xlate_vernac =
1644
| VernacDeclareTacticDefinition (true, tacs) ->
1648
CT_tac_def(reference_to_ct_ID id, xlate_tactic body))
1652
CT_tactic_definition
1653
(CT_tac_def_ne_list(fst, tacs1)))
1654
| VernacDeclareTacticDefinition(false, _) ->
1655
xlate_error "obsolete tactic definition not handled"
1656
| VernacLoad (verbose,s) ->
1659
| false -> CT_coerce_NONE_to_VERBOSE_OPT CT_none
1660
| true -> CT_verbose),
1661
CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
1662
| VernacCheckMayEval (Some red, numopt, f) ->
1663
let red = xlate_red_tactic red in
1664
CT_coerce_EVAL_CMD_to_COMMAND
1665
(CT_eval (xlate_int_opt numopt, red, xlate_formula f))
1666
|VernacChdir opt_s -> CT_cd (ctf_STRING_OPT opt_s)
1667
| VernacAddLoadPath (false,str,None) ->
1668
CT_addpath (CT_string str, ctv_ID_OPT_NONE)
1669
| VernacAddLoadPath (false,str,Some x) ->
1670
CT_addpath (CT_string str,
1671
CT_coerce_ID_to_ID_OPT (CT_ident (string_of_dirpath x)))
1672
| VernacAddLoadPath (true,str,None) ->
1673
CT_recaddpath (CT_string str, ctv_ID_OPT_NONE)
1674
| VernacAddLoadPath (_,str, Some x) ->
1675
CT_recaddpath (CT_string str,
1676
CT_coerce_ID_to_ID_OPT (CT_ident (string_of_dirpath x)))
1677
| VernacRemoveLoadPath str -> CT_delpath (CT_string str)
1678
| VernacToplevelControl Quit -> CT_quit
1679
| VernacToplevelControl _ -> xlate_error "Drop/ProtectedToplevel not supported"
1681
| VernacAddMLPath (false,str) -> CT_ml_add_path (CT_string str)
1682
| VernacAddMLPath (true,str) -> CT_rec_ml_add_path (CT_string str)
1683
| VernacDeclareMLModule [] -> failwith ""
1684
| VernacDeclareMLModule (str :: l) ->
1685
CT_ml_declare_modules
1686
(CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l))
1688
CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_formula c))
1689
| VernacAbort (Some (_,id)) ->
1690
CT_abort(ctf_ID_OPT_OR_ALL_SOME(xlate_ident id))
1691
| VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
1692
| VernacAbortAll -> CT_abort ctv_ID_OPT_OR_ALL_ALL
1693
| VernacRestart -> CT_restart
1694
| VernacSolve (n, tac, b) ->
1695
CT_solve (CT_int n, xlate_tactic tac,
1697
else CT_coerce_NONE_to_DOTDOT_OPT CT_none)
1701
| (VernacDeclProof | VernacReturn | VernacProofInstr _) ->
1702
anomaly "No MMode in CTcoq"
1707
| VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
1708
| VernacUnfocus -> CT_unfocus
1709
|VernacExtend("Extraction", [f;l]) ->
1710
let file = out_gen rawwit_string f in
1711
let l1 = out_gen (wit_list1 rawwit_ref) l in
1712
let fst,l2 = match l1 with [] -> assert false | fst::l2 -> fst, l2 in
1713
CT_extract_to_file(CT_string file,
1714
CT_id_ne_list(loc_qualid_to_ct_ID fst,
1715
List.map loc_qualid_to_ct_ID l2))
1716
| VernacExtend("ExtractionInline", [l]) ->
1717
let l1 = out_gen (wit_list1 rawwit_ref) l in
1718
let fst, l2 = match l1 with [] -> assert false | fst ::l2 -> fst, l2 in
1719
CT_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
1720
List.map loc_qualid_to_ct_ID l2))
1721
| VernacExtend("ExtractionNoInline", [l]) ->
1722
let l1 = out_gen (wit_list1 rawwit_ref) l in
1723
let fst, l2 = match l1 with [] -> assert false | fst ::l2 -> fst, l2 in
1724
CT_no_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
1725
List.map loc_qualid_to_ct_ID l2))
1726
| VernacExtend("Field",
1727
[fth;ainv;ainvl;div]) ->
1728
(match List.map (fun v -> xlate_formula(out_gen rawwit_constr v))
1731
[fth1;ainv1;ainvl1] ->
1733
xlate_formula_opt (out_gen (wit_opt rawwit_constr) div) in
1734
CT_add_field(fth1, ainv1, ainvl1, adiv1)
1736
| VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) ->
1737
let orient = out_gen Extraargs.rawwit_orient o in
1738
let formula_list = out_gen (wit_list1 rawwit_constr) f in
1739
let base = out_gen rawwit_pre_ident b in
1741
match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId []
1743
let ct_orient = match orient with
1746
let f_ne_list = match List.map xlate_formula formula_list with
1747
(fst::rest) -> CT_formula_ne_list(fst,rest)
1748
| _ -> assert false in
1749
CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
1750
| VernacCreateHintDb (local,dbname,b) ->
1751
xlate_error "TODO: VernacCreateHintDb"
1752
| VernacHints (local,dbnames,h) ->
1753
let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
1755
| HintsConstructors l ->
1756
let n1, names = match List.map tac_qualid_to_ct_ID l with
1757
n1 :: names -> n1, names
1758
| _ -> failwith "" in
1760
CT_local_hints(CT_ident "Constructors",
1761
CT_id_ne_list(n1, names), dblist)
1763
CT_hints(CT_ident "Constructors",
1764
CT_id_ne_list(n1, names), dblist)
1765
| HintsExtern (n, c, t) ->
1766
let pat = match c with
1767
| None -> CT_coerce_ID_OPT_to_FORMULA_OPT (CT_coerce_NONE_to_ID_OPT CT_none)
1768
| Some c -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula c)
1769
in CT_hint_extern(CT_int n, pat, xlate_tactic t, dblist)
1770
| HintsImmediate l ->
1771
let f1, formulas = match List.map xlate_formula l with
1773
| _ -> failwith "" in
1774
let l' = CT_formula_ne_list(f1, formulas) in
1778
CT_local_hints_resolve(l', dblist)
1779
| HintsImmediate _ ->
1780
CT_local_hints_immediate(l', dblist)
1781
| _ -> assert false)
1784
HintsResolve _ -> CT_hints_resolve(l', dblist)
1785
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
1786
| _ -> assert false)
1788
let f1, formulas = match List.map xlate_formula (List.map pi3 l) with
1790
| _ -> failwith "" in
1791
let l' = CT_formula_ne_list(f1, formulas) in
1795
CT_local_hints_resolve(l', dblist)
1796
| HintsImmediate _ ->
1797
CT_local_hints_immediate(l', dblist)
1798
| _ -> assert false)
1801
HintsResolve _ -> CT_hints_resolve(l', dblist)
1802
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
1803
| _ -> assert false)
1805
let n1, names = match List.map loc_qualid_to_ct_ID l with
1806
n1 :: names -> n1, names
1807
| _ -> failwith "" in
1809
CT_local_hints(CT_ident "Unfold",
1810
CT_id_ne_list(n1, names), dblist)
1812
CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)
1813
| HintsTransparency (l,b) ->
1814
let n1, names = match List.map loc_qualid_to_ct_ID l with
1815
n1 :: names -> n1, names
1816
| _ -> failwith "" in
1817
let ty = if b then "Transparent" else "Opaque" in
1819
CT_local_hints(CT_ident ty,
1820
CT_id_ne_list(n1, names), dblist)
1822
CT_hints(CT_ident ty, CT_id_ne_list(n1, names), dblist)
1823
| HintsDestruct(id, n, loc, f, t) ->
1824
let dl = match loc with
1825
ConclLocation() -> CT_conclusion_location
1826
| HypLocation true -> CT_discardable_hypothesis
1827
| HypLocation false -> CT_hypothesis_location in
1829
CT_local_hint_destruct
1830
(xlate_ident id, CT_int n,
1831
dl, xlate_formula f, xlate_tactic t, dblist)
1834
(xlate_ident id, CT_int n, dl, xlate_formula f,
1835
xlate_tactic t, dblist)
1837
| VernacEndProof (Proved (true,None)) ->
1838
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
1839
| VernacEndProof (Proved (false,None)) ->
1840
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE)
1841
| VernacEndProof (Proved (b,Some ((_,s), Some kind))) ->
1842
CT_save (CT_coerce_THM_to_THM_OPT (xlate_thm kind),
1843
ctf_ID_OPT_SOME (xlate_ident s))
1844
| VernacEndProof (Proved (b,Some ((_,s),None))) ->
1845
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"),
1846
ctf_ID_OPT_SOME (xlate_ident s))
1847
| VernacEndProof Admitted ->
1848
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE)
1849
| VernacSetOpacity (_,l) ->
1850
CT_strategy(CT_level_list
1851
(List.map (fun (l,q) ->
1852
(level_to_ct_LEVEL l,
1853
CT_id_list(List.map loc_qualid_to_ct_ID q))) l))
1854
| VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n))
1855
| VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt)
1856
| VernacShow ShowNode -> CT_show_node
1857
| VernacShow ShowProof -> CT_show_proof
1858
| VernacShow ShowTree -> CT_show_tree
1859
| VernacShow ShowProofNames -> CT_show_proofs
1860
| VernacShow (ShowIntros true) -> CT_show_intros
1861
| VernacShow (ShowIntros false) -> CT_show_intro
1862
| VernacShow (ShowGoalImplicitly None) -> CT_show_implicit (CT_int 1)
1863
| VernacShow (ShowGoalImplicitly (Some n)) -> CT_show_implicit (CT_int n)
1864
| VernacShow ShowExistentials -> CT_show_existentials
1865
| VernacShow ShowScript -> CT_show_script
1866
| VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)"
1867
| VernacShow(ShowThesis) -> xlate_error "TODO: VernacShow(ShowThesis _)"
1868
| VernacGo arg -> CT_go (xlate_locn arg)
1869
| VernacShow (ExplainProof l) -> CT_explain_proof (nums_to_int_list l)
1870
| VernacShow (ExplainTree l) ->
1871
CT_explain_prooftree (nums_to_int_list l)
1872
| VernacCheckGuard -> CT_guarded
1875
PrintFullContext -> CT_print_all
1876
| PrintName id -> CT_print_id (loc_qualid_to_ct_ID id)
1877
| PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id)
1878
| PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id)
1879
| PrintModules -> CT_print_modules
1880
| PrintGrammar name -> CT_print_grammar CT_grammar_none
1881
| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
1882
| PrintHintDbName id ->
1883
CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
1884
| PrintRewriteHintDbName id ->
1885
CT_print_rewrite_hintdb (CT_ident id)
1887
CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
1888
| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
1889
| PrintLoadPath None -> CT_print_loadpath
1890
| PrintLoadPath _ -> xlate_error "TODO: Print LoadPath dir"
1891
| PrintMLLoadPath -> CT_ml_print_path
1892
| PrintMLModules -> CT_ml_print_modules
1893
| PrintGraph -> CT_print_graph
1894
| PrintClasses -> CT_print_classes
1895
| PrintLtac qid -> CT_print_ltac (loc_qualid_to_ct_ID qid)
1896
| PrintCoercions -> CT_print_coercions
1897
| PrintCoercionPaths (id1, id2) ->
1898
CT_print_path (xlate_class id1, xlate_class id2)
1899
| PrintCanonicalConversions ->
1900
xlate_error "TODO: Print Canonical Structures"
1901
| PrintAssumptions _ ->
1902
xlate_error "TODO: Print Needed Assumptions"
1903
| PrintInstances _ ->
1904
xlate_error "TODO: Print Instances"
1905
| PrintTypeClasses ->
1906
xlate_error "TODO: Print TypeClasses"
1907
| PrintInspect n -> CT_inspect (CT_int n)
1908
| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
1909
| PrintTables -> CT_print_tables
1910
| PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
1911
| PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
1912
| PrintScopes -> CT_print_scopes
1913
| PrintScope id -> CT_print_scope (CT_ident id)
1914
| PrintVisibility id_opt ->
1917
Some id -> CT_coerce_ID_to_ID_OPT(CT_ident id)
1918
| None -> ctv_ID_OPT_NONE)
1919
| PrintAbout qid -> CT_print_about(loc_qualid_to_ct_ID qid)
1920
| PrintImplicit qid -> CT_print_implicit(loc_qualid_to_ct_ID qid))
1921
| VernacBeginSection (_,id) ->
1922
CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
1923
| VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
1924
| VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
1925
CT_coerce_THEOREM_GOAL_to_COMMAND(
1926
CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
1927
xlate_binder_list bl, xlate_formula c))
1928
| VernacStartTheoremProof _ ->
1929
xlate_error "TODO: Mutually dependent theorems"
1930
| VernacSuspend -> CT_suspend
1931
| VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
1932
| VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
1933
CT_coerce_THEOREM_GOAL_to_COMMAND
1935
(CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k),
1936
xlate_ident s, xlate_binder_list bl, xlate_formula typ))
1937
| VernacDefinition (kind,(_,s),DefineBody(bl,red_option,c,typ_opt),_) ->
1939
(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
1940
cvt_optional_eval_for_definition c red_option,
1941
xlate_formula_opt typ_opt)
1942
| VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline"
1943
(*inline : bool -> automatic delta reduction at fonctor application*)
1944
(* CT_variable (xlate_var kind, cvt_vernac_binders b)*)
1945
| VernacCheckMayEval (None, numopt, c) ->
1946
CT_check (xlate_formula c)
1947
| VernacSearch (s,x) ->
1948
let translated_restriction = xlate_search_restr x in
1950
| SearchPattern c ->
1951
CT_search_pattern(xlate_formula c, translated_restriction)
1953
CT_search(loc_qualid_to_ct_ID id, translated_restriction)
1954
| SearchRewrite c ->
1955
CT_search_rewrite(xlate_formula c, translated_restriction)
1956
| SearchAbout (a::l) ->
1957
let xlate_search_about_item (b,it) =
1958
if not b then xlate_error "TODO: negative searchabout constraint";
1960
SearchSubPattern (CRef x) ->
1961
CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
1962
| SearchString (s,None) ->
1963
CT_coerce_STRING_to_ID_OR_STRING(CT_string s)
1964
| SearchString _ | SearchSubPattern _ ->
1966
"TODO: search subpatterns or notation with explicit scope"
1969
(CT_id_or_string_ne_list(xlate_search_about_item a,
1970
List.map xlate_search_about_item l),
1971
translated_restriction)
1972
| SearchAbout [] -> assert false)
1974
(* | (\*Record from tactics/Record.v *\) *)
1976
(* (_, (add_coercion, (_,s)), binders, c1, *)
1977
(* rec_constructor_or_none, field_list) -> *)
1978
(* let record_constructor = *)
1979
(* xlate_ident_opt (Option.map snd rec_constructor_or_none) in *)
1981
(* ((if add_coercion then CT_coercion_atm else *)
1982
(* CT_coerce_NONE_to_COERCION_OPT(CT_none)), *)
1983
(* xlate_ident s, xlate_binder_list binders, *)
1984
(* xlate_formula (Option.get c1), record_constructor, *)
1985
(* build_record_field_list field_list) *)
1986
| VernacInductive (isind, lmi) ->
1987
let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in
1988
let strip_mutind = function
1989
(((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->
1991
(xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c),
1992
build_constructors constructors,
1993
translate_opt_notation_decl notopt)
1994
| _ -> xlate_error "TODO: Record notation in (Co)Inductive" in
1996
(CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
1997
| VernacFixpoint ([],_) -> xlate_error "mutual recursive"
1998
| VernacFixpoint ((lm :: lmi),boxed) ->
1999
let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) =
2000
let struct_arg = make_fix_struct (n, bl) in
2001
let arf = xlate_formula arf in
2002
let ardef = xlate_formula ardef in
2003
match xlate_binder_list bl with
2004
| CT_binder_list (b :: bl) ->
2005
CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
2006
struct_arg, arf, ardef)
2007
| _ -> xlate_error "mutual recursive" in
2009
(CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
2010
| VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
2011
| VernacCoFixpoint ((lm :: lmi),boxed) ->
2012
let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) =
2013
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
2014
xlate_formula arf, xlate_formula ardef) in
2016
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
2017
| VernacScheme [] -> xlate_error "induction scheme"
2018
| VernacScheme (lm :: lmi) ->
2019
let strip_ind = function
2020
| (Some (_,id), InductionScheme (depstr, inde, sort)) ->
2022
(xlate_ident id, xlate_dep depstr,
2023
CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
2025
| (None, InductionScheme (depstr, inde, sort)) ->
2027
(xlate_ident (id_of_string ""), xlate_dep depstr,
2028
CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
2030
| (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in
2032
(CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
2033
| VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
2034
| VernacSyntacticDefinition ((_,id), ([],c), false, _) ->
2035
CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
2036
| VernacSyntacticDefinition ((_,id), _, _, _) ->
2037
xlate_error"TODO: Local abbreviations and abbreviations with parameters"
2038
(* Modules and Module Types *)
2039
| VernacInclude (_) -> xlate_error "TODO : Include "
2040
| VernacDeclareModuleType((_, id), bl, mty_o) ->
2041
CT_module_type_decl(xlate_ident id,
2042
xlate_module_binder_list bl,
2045
CT_coerce_ID_OPT_to_MODULE_TYPE_OPT
2048
CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
2049
(xlate_module_type mty1))
2050
| VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
2051
CT_module(xlate_ident id,
2052
xlate_module_binder_list bl,
2053
xlate_module_type_check_opt mty_o,
2055
None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
2056
| Some m -> xlate_module_expr m)
2057
| VernacDeclareModule(_,(_, id), bl, mty_o) ->
2058
CT_declare_module(xlate_ident id,
2059
xlate_module_binder_list bl,
2060
xlate_module_type_check_opt (Some mty_o),
2061
CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
2062
| VernacRequire (impexp, spec, id::idl) ->
2063
let ct_impexp, ct_spec = get_require_flags impexp spec in
2064
CT_require (ct_impexp, ct_spec,
2065
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STRING(
2066
CT_id_ne_list(loc_qualid_to_ct_ID id,
2067
List.map loc_qualid_to_ct_ID idl)))
2068
| VernacRequire (_,_,[]) ->
2069
xlate_error "Require should have at least one id argument"
2070
| VernacRequireFrom (impexp, spec, filename) ->
2071
let ct_impexp, ct_spec = get_require_flags impexp spec in
2072
CT_require(ct_impexp, ct_spec,
2073
CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
2075
| VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
2076
| VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
2077
| VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
2078
| VernacOpenCloseScope(false, false, s) -> CT_close_scope(CT_ident s)
2079
| VernacArgumentsScope(true, qid, l) ->
2080
CT_arguments_scope(loc_qualid_to_ct_ID qid,
2085
None -> ctv_ID_OPT_NONE
2086
| Some x -> ctf_ID_OPT_SOME(CT_ident x)) l))
2087
| VernacArgumentsScope(false, qid, l) ->
2088
xlate_error "TODO: Arguments Scope Global"
2089
| VernacDelimiters(s1,s2) -> CT_delim_scope(CT_ident s1, CT_ident s2)
2090
| VernacBindScope(id, a::l) ->
2091
let xlate_class_rawexpr = function
2092
FunClass -> CT_ident "Funclass" | SortClass -> CT_ident "Sortclass"
2093
| RefClass qid -> loc_qualid_to_ct_ID qid in
2094
CT_bind_scope(CT_ident id,
2095
CT_id_ne_list(xlate_class_rawexpr a,
2096
List.map xlate_class_rawexpr l))
2097
| VernacBindScope(id, []) -> assert false
2098
| VernacNotation(b, c, (s,modif_list), opt_scope) ->
2099
let translated_s = CT_string s in
2100
let formula = xlate_formula c in
2101
let translated_modif_list =
2102
CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
2103
let translated_scope = match opt_scope with
2104
None -> ctv_ID_OPT_NONE
2105
| Some x -> ctf_ID_OPT_SOME(CT_ident x) in
2107
CT_local_define_notation
2108
(translated_s, formula, translated_modif_list, translated_scope)
2110
CT_define_notation(translated_s, formula,
2111
translated_modif_list, translated_scope)
2112
| VernacSyntaxExtension(b,(s,modif_list)) ->
2113
let translated_s = CT_string s in
2114
let translated_modif_list =
2115
CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
2117
CT_local_reserve_notation(translated_s, translated_modif_list)
2119
CT_reserve_notation(translated_s, translated_modif_list)
2120
| VernacInfix (b,(str,modl),id, opt_scope) ->
2121
let id1 = loc_qualid_to_ct_ID id in
2122
let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
2123
let s = CT_string str in
2124
let translated_scope = match opt_scope with
2125
None -> ctv_ID_OPT_NONE
2126
| Some x -> ctf_ID_OPT_SOME(CT_ident x) in
2128
CT_local_infix(s, id1,modl1, translated_scope)
2130
CT_infix(s, id1,modl1, translated_scope)
2131
| VernacCoercion (s, id1, id2, id3) ->
2132
let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
2135
(* Cannot decide whether it is a global or a Local but at toplevel *)
2136
| Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none
2137
| Local -> CT_local in
2138
CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1,
2139
xlate_class id2, xlate_class id3)
2141
| VernacIdentityCoercion (s, (_,id1), id2, id3) ->
2142
let id_opt = CT_identity in
2145
(* Cannot decide whether it is a global or a Local but at toplevel *)
2146
| Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none
2147
| Local -> CT_local in
2148
CT_coercion (local_opt, id_opt, xlate_ident id1,
2149
xlate_class id2, xlate_class id3)
2152
| VernacDeclareInstance _|VernacContext _|
2153
VernacInstance (_, _, _, _, _) ->
2154
xlate_error "TODO: Type Classes commands"
2156
| VernacResetName id -> CT_reset (xlate_ident (snd id))
2157
| VernacResetInitial -> CT_restore_state (CT_ident "Initial")
2158
| VernacExtend (s, l) ->
2160
(CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
2161
| VernacList((_, a)::l) ->
2162
CT_coerce_COMMAND_LIST_to_COMMAND
2163
(CT_command_list(xlate_vernac a,
2164
List.map (fun (_, x) -> xlate_vernac x) l))
2165
| VernacList([]) -> assert false
2166
| VernacNop -> CT_proof_no_op
2167
| VernacComments l ->
2168
CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
2169
| VernacDeclareImplicits(true, id, opt_positions) ->
2171
(reference_to_ct_ID id,
2172
match opt_positions with
2173
None -> CT_coerce_NONE_to_ID_LIST_OPT CT_none
2175
CT_coerce_ID_LIST_to_ID_LIST_OPT
2178
(function ExplByPos (x,_), _, _
2180
"explication argument by rank is obsolete"
2181
| ExplByName id, _, _ -> CT_ident (string_of_id id)) l)))
2182
| VernacDeclareImplicits(false, id, opt_positions) ->
2183
xlate_error "TODO: Implicit Arguments Global"
2184
| VernacReserve((_,a)::l, f) ->
2185
CT_reserve(CT_id_ne_list(xlate_ident a,
2186
List.map (fun (_,x) -> xlate_ident x) l),
2188
| VernacReserve([], _) -> assert false
2189
| VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
2190
| VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
2191
| VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module"
2192
| VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
2193
| VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
2194
| VernacTime(v) -> CT_time(xlate_vernac v)
2195
| VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
2196
|VernacExactProof f -> CT_proof(xlate_formula f)
2197
| VernacSetOption (table, BoolValue true) ->
2200
PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
2201
| SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
2202
| TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
2203
CT_set_option(table1)
2204
| VernacSetOption (table, v) ->
2207
PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
2208
| SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
2209
| TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
2212
| BoolValue _ -> assert false
2214
CT_coerce_STRING_to_SINGLE_OPTION_VALUE(CT_string s)
2216
CT_coerce_INT_to_SINGLE_OPTION_VALUE(CT_int n) in
2217
CT_set_option_value(table1, value)
2218
| VernacUnsetOption(table) ->
2221
PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
2222
| SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
2223
| TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
2224
CT_unset_option(table1)
2225
| VernacAddOption (table, l) ->
2229
| QualidRefValue x ->
2230
CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
2231
| StringRefValue x ->
2232
CT_coerce_STRING_to_ID_OR_STRING(CT_string x)) l in
2234
match values with [] -> assert false | a::b -> (a,b) in
2237
PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
2238
| SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
2239
| TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
2240
CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1))
2241
| VernacImport(true, a::l) ->
2242
CT_export_id(CT_id_ne_list(reference_to_ct_ID a,
2243
List.map reference_to_ct_ID l))
2244
| VernacImport(false, a::l) ->
2245
CT_import_id(CT_id_ne_list(reference_to_ct_ID a,
2246
List.map reference_to_ct_ID l))
2247
| VernacImport(_, []) -> assert false
2248
| VernacProof t -> CT_proof_with(xlate_tactic t)
2249
| (VernacGlobalCheck _|VernacPrintOption _|
2250
VernacMemOption (_, _)|VernacRemoveOption (_, _)
2251
| VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
2252
VernacSolveExistential (_, _)|VernacCanonical _ |
2253
VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _)
2254
-> xlate_error "TODO: vernac"
2255
and level_to_ct_LEVEL = function
2256
Conv_oracle.Opaque -> CT_Opaque
2257
| Conv_oracle.Level n -> CT_Level (CT_int n)
2258
| Conv_oracle.Expand -> CT_Expand;;
2261
let rec xlate_vernac_list =
2263
| VernacList (v::l) ->
2265
(xlate_vernac (snd v), List.map (fun (_,x) -> xlate_vernac x) l)
2266
| VernacList [] -> xlate_error "xlate_command_list"
2267
| _ -> xlate_error "Not a list of commands";;
added
removed
contrib/interface/xlate.ml
