summaryrefslogtreecommitdiff
path: root/contrib/interface/xlate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/xlate.ml')
-rw-r--r--contrib/interface/xlate.ml376
1 files changed, 184 insertions, 192 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 02dc57de..da87086e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -3,7 +3,6 @@
open String;;
open Char;;
open Util;;
-open Ast;;
open Names;;
open Ascent;;
open Genarg;;
@@ -64,11 +63,7 @@ let coercion_description t = !coercion_description_holder t;;
let set_coercion_description f =
coercion_description_holder:=f; ();;
-let string_of_node_loc the_node =
- match Util.unloc (loc the_node) with
- (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";;
-
-let xlate_error s = failwith ("Translation error: " ^ s);;
+let xlate_error s = print_endline ("xlate_error : "^s);failwith ("Translation error: " ^ s);;
let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;;
@@ -266,11 +261,13 @@ let rec xlate_match_pattern =
| CPatAlias (_, pattern, id) ->
CT_pattern_as
(xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
+ | CPatOr (_,l) -> xlate_error "CPatOr: TODO"
| CPatDelimiters(_, key, p) ->
CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
- | CPatNumeral(_,n) ->
+ | CPatPrim (_,Numeral n) ->
CT_coerce_NUM_to_MATCH_PATTERN
- (CT_int_encapsulator(Bignat.bigint_to_string n))
+ (CT_int_encapsulator(Bigint.to_string n))
+ | CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
| CPatNotation(_, s, l) ->
CT_pattern_notation(CT_string s,
CT_match_pattern_list(List.map xlate_match_pattern l))
@@ -373,14 +370,11 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CApp(_, (_,f), l) ->
CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
| CCases (_, _, [], _) -> assert false
- | CCases (_, (Some _, _), _, _) -> xlate_error "NOT parsed: Cases with Some"
- | CCases (_,(None, ret_type), tm::tml, eqns)->
+ | CCases (_, ret_type, tm::tml, eqns)->
CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
List.map xlate_matched_formula tml),
xlate_formula_opt ret_type,
CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
- | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) ->
- xlate_error "No more COrderedCase"
| CLetTuple (_,a::l, ret_info, c, b) ->
CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
List.map xlate_id_opt_aux l),
@@ -393,27 +387,18 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
(xlate_formula c, xlate_return_info ret_info,
xlate_formula b1, xlate_formula b2)
- | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
- CT_inductive_let(xlate_formula_opt po,
- xlate_id_opt_ne_list l,
- xlate_formula c, xlate_formula b)
- | COrderedCase (_,c,v,e,l) ->
- let case_string = match c with
- Term.MatchStyle -> "Match"
- | _ -> "Case" in
- CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e,
- CT_formula_list(List.map xlate_formula l))
| CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
| CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
- | CNumeral(_, i) ->
- CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bignat.bigint_to_string i))
+ | CPrim (_, Numeral i) ->
+ CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
+ | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
| CHole _ -> CT_existvarc
(* I assume CDynamic has been inserted to make free form extension of
the language possible, but this would go agains the logic of pcoq anyway. *)
| CDynamic (_, _) -> assert false
| CDelimiters (_, key, num) ->
CT_num_encapsulator(CT_num_type key , xlate_formula num)
- | CCast (_, e, t) ->
+ | CCast (_, e,_, t) ->
CT_coerce_TYPED_FORMULA_to_FORMULA
(CT_typed_formula(xlate_formula e, xlate_formula t))
| CPatVar (_, (_,i)) when is_int_meta i ->
@@ -430,11 +415,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
CT_cofixc(xlate_ident id,
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
| CFix (_, (_, id), lm::lmi) ->
- let strip_mutrec (fid, n, bl, arf, ardef) =
+ let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
let (struct_arg,bl,arf,ardef) =
if bl = [] then
let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
- let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
@@ -485,14 +469,14 @@ let xlate_hyp = function
let xlate_hyp_location =
function
- | AI (_,id), nums, (InHypTypeOnly,_) ->
+ | AI (_,id), nums, InHypTypeOnly ->
CT_intype(xlate_ident id, nums_to_int_list nums)
- | AI (_,id), nums, (InHypValueOnly,_) ->
+ | AI (_,id), nums, InHypValueOnly ->
CT_invalue(xlate_ident id, nums_to_int_list nums)
- | AI (_,id), [], (InHyp,_) ->
+ | AI (_,id), [], InHyp ->
CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_coerce_ID_to_UNFOLD (xlate_ident id))
- | AI (_,id), a::l, (InHyp,_) ->
+ | AI (_,id), a::l, InHyp ->
CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_unfold_occ (xlate_ident id,
CT_int_ne_list(CT_int a, nums_to_int_list_aux l)))
@@ -631,6 +615,7 @@ let rec xlate_intro_pattern =
ll)
| IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
| IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
+ | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
let compute_INV_TYPE = function
FullInversionClear -> CT_inv_clear
@@ -678,9 +663,11 @@ let xlate_one_unfold_block = function
| (n::nums, qid) ->
CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
-let xlate_intro_patt_opt = function
- None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
- | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+let xlate_with_names = function
+ IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+ | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+
+let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
function
@@ -729,6 +716,7 @@ and xlate_red_tactic =
function
| Red true -> xlate_error ""
| Red false -> CT_red
+ | CbvVm -> CT_cbvvm
| Hnf -> CT_hnf
| Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
| Simpl (Some (l,c)) ->
@@ -788,6 +776,7 @@ and xlate_tactic =
| TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
| TacSolve([]) -> assert false
| TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
+ | TacComplete _ -> xlate_error "TODO: tactical complete"
| TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
| TacTry t -> CT_try (xlate_tactic t)
| TacRepeat t -> CT_repeat(xlate_tactic t)
@@ -798,7 +787,8 @@ and xlate_tactic =
xlate_tactic t)
| TacProgress t -> CT_progress(xlate_tactic t)
| TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
- | TacMatch (exp, rules) ->
+ | TacMatch (true,_,_) -> failwith "TODO: lazy match"
+ | TacMatch (false, exp, rules) ->
CT_match_tac(xlate_tactic exp,
match List.map
(function
@@ -814,11 +804,11 @@ and xlate_tactic =
| [] -> assert false
| fst::others ->
CT_match_tac_rules(fst, others))
- | TacMatchContext (_,[]) -> failwith ""
- | TacMatchContext (false,rule1::rules) ->
+ | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
+ | TacMatchContext (false,false,rule1::rules) ->
CT_match_context(xlate_context_rule rule1,
List.map xlate_context_rule rules)
- | TacMatchContext (true,rule1::rules) ->
+ | TacMatchContext (false,true,rule1::rules) ->
CT_match_context_reverse(xlate_context_rule rule1,
List.map xlate_context_rule rules)
| TacLetIn (l, t) ->
@@ -855,18 +845,23 @@ and xlate_tactic =
(xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
CT_rec_tactic_in(tl, xlate_tactic t)
| TacAtom (_, t) -> xlate_tac t
- | TacFail (count, "") -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
- | TacFail (count, s) -> CT_fail(xlate_id_or_int count,
+ | TacFail (count, []) -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
+ | TacFail (count, [MsgString s]) -> CT_fail(xlate_id_or_int count,
ctf_STRING_OPT_SOME (CT_string s))
- | TacId "" -> CT_idtac ctf_STRING_OPT_NONE
- | TacId s -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+ | TacFail (count, _) -> xlate_error "TODO: generic fail message"
+ | TacId [] -> CT_idtac ctf_STRING_OPT_NONE
+ | TacId [MsgString s] -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+ | TacId _ -> xlate_error "TODO: generic idtac message"
| TacInfo t -> CT_info(xlate_tactic t)
| TacArg a -> xlate_call_or_tacarg a
and xlate_tac =
function
| TacExtend (_, "firstorder", tac_opt::l) ->
- let t1 = match out_gen (wit_opt rawwit_tactic) tac_opt with
+ let t1 =
+ match
+ out_gen (wit_opt rawwit_main_tactic) tac_opt
+ with
| None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
| Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in
(match l with
@@ -914,7 +909,7 @@ and xlate_tac =
CT_discriminate_eq
(xlate_quantified_hypothesis_opt
(out_gen (wit_opt rawwit_quant_hyp) idopt))
- | TacExtend (_,"deq", [idopt]) ->
+ | TacExtend (_,"simplify_eq", [idopt]) ->
let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
let idopt2 = match idopt1 with
None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
@@ -962,53 +957,68 @@ and xlate_tac =
| TacRight bindl -> CT_right (xlate_bindings bindl)
| TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
| TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
- | TacExtend (_,"replace", [c1; c2]) ->
- let c1 = xlate_formula (out_gen rawwit_constr c1) in
- let c2 = xlate_formula (out_gen rawwit_constr c2) in
- CT_replace_with (c1, c2)
+ | TacExtend (_,"replace", [c1; c2;id_opt;tac_opt]) ->
+ let c1 = xlate_formula (out_gen rawwit_constr c1) in
+ let c2 = xlate_formula (out_gen rawwit_constr c2) in
+ let id_opt =
+ match out_gen Extratactics.rawwit_in_arg_hyp id_opt with
+ | None -> ctv_ID_OPT_NONE
+ | Some id -> ctf_ID_OPT_SOME (xlate_ident id)
+ in
+ let tac_opt =
+ match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
+ | None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
+ | Some tac ->
+ let tac = xlate_tactic tac in
+ CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
+ in
+ CT_replace_with (c1, c2,id_opt,tac_opt)
| TacExtend (_,"rewrite", [b; cbindl]) ->
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
if b then CT_rewrite_lr (c, bindl, ctv_ID_OPT_NONE)
else CT_rewrite_rl (c, bindl, ctv_ID_OPT_NONE)
- | TacExtend (_,"rewritein", [b; cbindl; id]) ->
+ | TacExtend (_,"rewrite_in", [b; cbindl; id]) ->
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
- let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+ let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
if b then CT_rewrite_lr (c, bindl, id)
else CT_rewrite_rl (c, bindl, id)
- | TacExtend (_,"conditionalrewrite", [t; b; cbindl]) ->
- let t = out_gen rawwit_tactic t in
+ | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
+ let t = out_gen rawwit_main_tactic t in
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
- | TacExtend (_,"conditionalrewritein", [t; b; cbindl; id]) ->
- let t = out_gen rawwit_tactic t in
+ | TacExtend (_,"conditional_rewrite", [t; b; cbindl; id]) ->
+ let t = out_gen rawwit_main_tactic t in
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
- let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+ let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id)
else CT_condrewrite_rl (xlate_tactic t, c, bindl, id)
- | TacExtend (_,"dependentrewrite", [b; id_or_constr]) ->
+ | TacExtend (_,"dependent_rewrite", [b; c]) ->
let b = out_gen Extraargs.rawwit_orient b in
- (match genarg_tag id_or_constr with
- | IdentArgType -> (*Dependent Rewrite/SubstHypInConcl*)
- let id = xlate_ident (out_gen rawwit_ident id_or_constr) in
+ let c = xlate_formula (out_gen rawwit_constr c) in
+ (match c with
+ | CT_coerce_ID_to_FORMULA (CT_ident _ as id) ->
if b then CT_deprewrite_lr id else CT_deprewrite_rl id
- | ConstrArgType -> (*CutRewrite/SubstConcl*)
- let c = xlate_formula (out_gen rawwit_constr id_or_constr) in
- if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
- else CT_cutrewrite_rl (c, ctv_ID_OPT_NONE)
- | _ -> xlate_error "")
- | TacExtend (_,"dependentrewrite", [b; c; id]) -> (*CutRewrite in/SubstHyp*)
+ | _ -> xlate_error "dependent rewrite on term: not supported")
+ | TacExtend (_,"dependent_rewrite", [b; c; id]) ->
+ xlate_error "dependent rewrite on terms in hypothesis: not supported"
+ | TacExtend (_,"cut_rewrite", [b; c]) ->
+ let b = out_gen Extraargs.rawwit_orient b in
+ let c = xlate_formula (out_gen rawwit_constr c) in
+ if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
+ else CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
+ | TacExtend (_,"cut_rewrite", [b; c; id]) ->
let b = out_gen Extraargs.rawwit_orient b in
let c = xlate_formula (out_gen rawwit_constr c) in
- let id = xlate_ident (out_gen rawwit_ident id) in
+ let id = xlate_ident (snd (out_gen rawwit_var id)) in
if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
| TacExtend(_, "subst", [l]) ->
@@ -1021,6 +1031,7 @@ and xlate_tac =
| TacTransitivity c -> CT_transitivity (xlate_formula c)
| TacAssumption -> CT_assumption
| TacExact c -> CT_exact (xlate_formula c)
+ | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
| TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id)
| TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id)
| TacDestructConcl -> CT_dconcl
@@ -1031,14 +1042,16 @@ and xlate_tac =
(if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
(if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
| TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
- | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
- | TacAuto (nopt, None) ->
+ | TacAuto (nopt, [], Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
+ | TacAuto (nopt, [], None) ->
CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
- | TacAuto (nopt, Some (id1::idl)) ->
+ | TacAuto (nopt, [], Some (id1::idl)) ->
CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
+ | TacAuto (nopt, _::_, _) ->
+ xlate_error "TODO: auto using"
|TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
let (id_list:ct_ID list) =
List.map (fun x -> CT_ident x) (out_gen (wit_list1 rawwit_pre_ident) l) in
@@ -1048,11 +1061,11 @@ and xlate_tac =
match t with
[t0] ->
CT_coerce_TACTIC_COM_to_TACTIC_OPT
- (xlate_tactic(out_gen rawwit_tactic t0))
+ (xlate_tactic(out_gen rawwit_main_tactic t0))
| [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
| _ -> assert false in
CT_autorewrite (CT_id_ne_list(fst, id_list1), t1)
- | TacExtend (_,"eauto", [nopt; popt; idl]) ->
+ | TacExtend (_,"eauto", [nopt; popt; lems; idl]) ->
let first_n =
match out_gen (wit_opt rawwit_int_or_var) nopt with
| Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
@@ -1063,6 +1076,10 @@ and xlate_tac =
| Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
| Some ArgArg n -> xlate_int_to_id_or_int_opt n
| None -> none_in_id_or_int_opt in
+ let _lems =
+ match out_gen Eauto.rawwit_auto_using lems with
+ | [] -> []
+ | _ -> xlate_error "TODO: eauto using" in
let idl = out_gen Eauto.rawwit_hintbases idl in
(match idl with
None -> CT_eauto_with(first_n,
@@ -1084,12 +1101,14 @@ and xlate_tac =
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
CT_eapply (c, bindl)
- | TacTrivial (Some []) -> CT_trivial
- | TacTrivial None ->
+ | TacTrivial ([],Some []) -> CT_trivial
+ | TacTrivial ([],None) ->
CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
- | TacTrivial (Some (id1::idl)) ->
+ | TacTrivial ([],Some (id1::idl)) ->
CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
(CT_id_ne_list(CT_ident id1,List.map (fun x -> CT_ident x) idl))))
+ | TacTrivial (_::_,_) ->
+ xlate_error "TODO: trivial using"
| TacReduce (red, l) ->
CT_reduce (xlate_red_tactic red, xlate_clause l)
| TacApply (c,bindl) ->
@@ -1111,7 +1130,7 @@ and xlate_tac =
CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
| TacCase (c1,sl) ->
CT_casetac (xlate_formula c1, xlate_bindings sl)
- | TacSimpleInduction (h,_) -> CT_induction (xlate_quantified_hypothesis h)
+ | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
| TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
| TacCut c -> CT_cut (xlate_formula c)
| TacLApply c -> CT_use (xlate_formula c)
@@ -1123,20 +1142,21 @@ and xlate_tac =
CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
| TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
| TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
- | TacClear [] ->
+ | TacClear (false,[]) ->
xlate_error "Clear expects a non empty list of identifiers"
- | TacClear (id::idl) ->
+ | TacClear (false,id::idl) ->
let idl' = List.map xlate_hyp idl in
CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
+ | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
| (*For translating tactics/Inv.v *)
TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
- xlate_intro_patt_opt l,
+ xlate_with_names l,
CT_id_list (List.map xlate_hyp idl))
| TacInversion (DepInversion (k,copt,l),quant_hyp) ->
let id = xlate_quantified_hypothesis quant_hyp in
CT_depinversion (compute_INV_TYPE k, id,
- xlate_intro_patt_opt l, xlate_formula_opt copt)
+ xlate_with_names l, xlate_formula_opt copt)
| TacInversion (InversionUsing (c,idlist), id) ->
let id = xlate_quantified_hypothesis id in
CT_use_inversion (id, xlate_formula c,
@@ -1148,28 +1168,34 @@ and xlate_tac =
CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
| TacDAuto (a, b) ->
CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
- | TacNewDestruct(a,b,(c,_)) ->
- CT_new_destruct
- (xlate_int_or_constr a, xlate_using b,
- xlate_intro_patt_opt c)
- | TacNewInduction(a,b,(c,_)) ->
- CT_new_induction
- (xlate_int_or_constr a, xlate_using b,
- xlate_intro_patt_opt c)
- | TacInstantiate (a, b, cl) ->
+ | TacNewDestruct(a,b,c) ->
+ CT_new_destruct (* Julien F. : est-ce correct *)
+ (List.map xlate_int_or_constr a, xlate_using b,
+ xlate_with_names c)
+ | TacNewInduction(a,b,c) ->
+ CT_new_induction (* Pierre C. : est-ce correct *)
+ (List.map xlate_int_or_constr a, xlate_using b,
+ xlate_with_names c)
+ (*| TacInstantiate (a, b, cl) ->
CT_instantiate(CT_int a, xlate_formula b,
- xlate_clause cl)
+ assert false) *)
+ | TacLetTac (na, c, cl) when cl = nowhere ->
+ CT_pose(xlate_id_opt_aux na, xlate_formula c)
| TacLetTac (na, c, cl) ->
CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
(* TODO LATER: This should be shared with Unfold,
but the structures are different *)
xlate_clause cl)
- | TacForward (true, name, c) ->
- CT_pose(xlate_id_opt_aux name, xlate_formula c)
- | TacForward (false, name, c) ->
- CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
- | TacTrueCut (na, c) ->
- CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c)
+ | TacAssert (None, IntroIdentifier id, c) ->
+ CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
+ | TacAssert (None, IntroAnonymous, c) ->
+ CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+ | TacAssert (Some (TacId []), IntroIdentifier id, c) ->
+ CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
+ | TacAssert (Some (TacId []), IntroAnonymous, c) ->
+ CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+ | TacAssert _ ->
+ xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
| TacAnyConstructor(Some tac) ->
CT_any_constructor
(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
@@ -1181,6 +1207,7 @@ and xlate_tac =
(List.map xlate_formula
(out_gen (wit_list0 rawwit_constr) args)))
| TacExtend (_,id, l) ->
+ print_endline ("Extratactics : "^ id);
CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
| TacAlias _ -> xlate_error "Alias not supported"
@@ -1216,8 +1243,11 @@ and coerce_genarg_to_TARG x =
CT_coerce_FORMULA_OR_INT_to_TARG
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
(CT_coerce_ID_to_ID_OR_INT id))
- | HypArgType ->
- xlate_error "TODO (similar to IdentArgType)"
+ | VarArgType ->
+ let id = xlate_ident (snd (out_gen rawwit_var x)) in
+ CT_coerce_FORMULA_OR_INT_to_TARG
+ (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
+ (CT_coerce_ID_to_ID_OR_INT id))
| RefArgType ->
let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
CT_coerce_FORMULA_OR_INT_to_TARG
@@ -1233,19 +1263,14 @@ and coerce_genarg_to_TARG x =
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
- | TacticArgType ->
- let t = xlate_tactic (out_gen rawwit_tactic x) in
+ | TacticArgType n ->
+ let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
CT_coerce_TACTIC_COM_to_TARG t
- | OpenConstrArgType ->
- CT_coerce_SCOMMENT_CONTENT_to_TARG
- (CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
- (snd (out_gen
- rawwit_open_constr x))))
- | CastedOpenConstrArgType ->
+ | OpenConstrArgType b ->
CT_coerce_SCOMMENT_CONTENT_to_TARG
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
- (snd (out_gen
- rawwit_casted_open_constr x))))
+ (snd (out_gen
+ (rawwit_open_constr_gen b) x))))
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
| BindingsArgType -> xlate_error "TODO: generic with bindings"
| RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1315,8 +1340,11 @@ let coerce_genarg_to_VARG x =
CT_coerce_ID_OPT_OR_ALL_to_VARG
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
(CT_coerce_ID_to_ID_OPT id))
- | HypArgType ->
- xlate_error "TODO (similar to IdentArgType)"
+ | VarArgType ->
+ let id = xlate_ident (snd (out_gen rawwit_var x)) in
+ CT_coerce_ID_OPT_OR_ALL_to_VARG
+ (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
+ (CT_coerce_ID_to_ID_OPT id))
| RefArgType ->
let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
CT_coerce_ID_OPT_OR_ALL_to_VARG
@@ -1332,11 +1360,10 @@ let coerce_genarg_to_VARG x =
(CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
- | TacticArgType ->
- let t = xlate_tactic (out_gen rawwit_tactic x) in
+ | TacticArgType n ->
+ let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
- | OpenConstrArgType -> xlate_error "TODO: generic open constr"
- | CastedOpenConstrArgType -> xlate_error "TODO: generic open constr"
+ | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
| BindingsArgType -> xlate_error "TODO: generic with bindings"
| RedExprArgType -> xlate_error "TODO: red expr as generic argument"
@@ -1347,23 +1374,9 @@ let coerce_genarg_to_VARG x =
| ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
-let xlate_thm x = CT_thm (match x with
- | Theorem -> "Theorem"
- | Remark -> "Remark"
- | Lemma -> "Lemma"
- | Fact -> "Fact")
+let xlate_thm x = CT_thm (string_of_theorem_kind x)
-
-let xlate_defn x = CT_defn (match x with
- | (Local, Definition) -> "Local"
- | (Global, Definition) -> "Definition"
- | (Global, SubClass) -> "SubClass"
- | (Global, Coercion) -> "Coercion"
- | (Local, SubClass) -> "Local SubClass"
- | (Local, Coercion) -> "Local Coercion"
- | (Global,CanonicalStructure) -> "Canonical Structure"
- | (Local, CanonicalStructure) ->
- xlate_error "Local CanonicalStructure not parsed")
+let xlate_defn k = CT_defn (string_of_definition_kind k)
let xlate_var x = CT_var (match x with
| (Global,Definitional) -> "Parameter"
@@ -1511,17 +1524,18 @@ let rec xlate_module_type = function
| CMTEwith(mty, decl) ->
let mty1 = xlate_module_type mty in
(match decl with
- CWith_Definition((_, id), c) ->
- CT_module_type_with_def(xlate_module_type mty,
- xlate_ident id, xlate_formula c)
- | CWith_Module((_, id), (_, qid)) ->
- CT_module_type_with_mod(xlate_module_type mty,
- xlate_ident id,
+ CWith_Definition((_, idl), c) ->
+ CT_module_type_with_def(mty1,
+ CT_id_list (List.map xlate_ident idl),
+ xlate_formula c)
+ | CWith_Module((_, idl), (_, qid)) ->
+ CT_module_type_with_mod(mty1,
+ CT_id_list (List.map xlate_ident idl),
CT_ident (xlate_qualid qid)));;
let xlate_module_binder_list (l:module_binder list) =
CT_module_binder_list
- (List.map (fun (idl, mty) ->
+ (List.map (fun (_, idl, mty) ->
let idl1 =
List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in
let fst,idl2 = match idl1 with
@@ -1643,18 +1657,13 @@ let rec xlate_vernac =
CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1,
ainv1, fth1, ainvl1, bind)
|_ -> assert false)
- | VernacExtend (("HintRewriteV7"|"HintRewriteV8") as key, largs) ->
- let in_v8 = (key = "HintRewriteV8") in
- let orient = out_gen Extraargs.rawwit_orient (List.nth largs 0) in
- let formula_list = out_gen (wit_list1 rawwit_constr) (List.nth largs 1) in
- let t =
- if List.length largs = 4 then
- out_gen rawwit_tactic (List.nth largs (if in_v8 then 2 else 3))
- else
- TacId "" in
- let base =
- out_gen rawwit_pre_ident
- (if in_v8 then last largs else List.nth largs 2) in
+ | VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) ->
+ let orient = out_gen Extraargs.rawwit_orient o in
+ let formula_list = out_gen (wit_list1 rawwit_constr) f in
+ let base = out_gen rawwit_pre_ident b in
+ let t =
+ match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId []
+ in
let ct_orient = match orient with
| true -> CT_lr
| false -> CT_rl in
@@ -1665,7 +1674,7 @@ let rec xlate_vernac =
| VernacHints (local,dbnames,h) ->
let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
(match h with
- | HintsConstructors (None, l) ->
+ | HintsConstructors l ->
let n1, names = match List.map tac_qualid_to_ct_ID l with
n1 :: names -> n1, names
| _ -> failwith "" in
@@ -1675,15 +1684,10 @@ let rec xlate_vernac =
else
CT_hints(CT_ident "Constructors",
CT_id_ne_list(n1, names), dblist)
- | HintsExtern (None, n, c, t) ->
+ | HintsExtern (n, c, t) ->
CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
| HintsResolve l | HintsImmediate l ->
- let l =
- List.map
- (function (None, f) -> xlate_formula f
- | _ ->
- xlate_error "obsolete Hint Resolve not supported") l in
- let f1, formulas = match l with
+ let f1, formulas = match List.map xlate_formula l with
a :: tl -> a, tl
| _ -> failwith "" in
let l' = CT_formula_ne_list(f1, formulas) in
@@ -1700,10 +1704,7 @@ let rec xlate_vernac =
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
| _ -> assert false)
| HintsUnfold l ->
- let l = List.map
- (function (None,ref) -> loc_qualid_to_ct_ID ref |
- _ -> xlate_error "obsolete Hint Unfold not supported") l in
- let n1, names = match l with
+ let n1, names = match List.map loc_qualid_to_ct_ID l with
n1 :: names -> n1, names
| _ -> failwith "" in
if local then
@@ -1724,9 +1725,6 @@ let rec xlate_vernac =
CT_hint_destruct
(xlate_ident id, CT_int n, dl, xlate_formula f,
xlate_tactic t, dblist)
- | HintsExtern(Some _, _, _, _)
- | HintsConstructors(Some _, _) ->
- xlate_error "obsolete Hint Constructors not supported"
)
| VernacEndProof (Proved (true,None)) ->
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
@@ -1759,6 +1757,7 @@ let rec xlate_vernac =
| VernacShow (ShowGoalImplicitly (Some n)) -> CT_show_implicit (CT_int n)
| VernacShow ShowExistentials -> CT_show_existentials
| VernacShow ShowScript -> CT_show_script
+ | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)"
| VernacGo arg -> CT_go (xlate_locn arg)
| VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l)
| VernacShow ExplainTree l ->
@@ -1775,6 +1774,8 @@ let rec xlate_vernac =
| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
| PrintHintDbName id ->
CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
+ | PrintRewriteHintDbName id ->
+ CT_print_rewrite_hintdb (CT_ident id)
| PrintHint id ->
CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
@@ -1783,12 +1784,15 @@ let rec xlate_vernac =
| PrintMLModules -> CT_ml_print_modules
| PrintGraph -> CT_print_graph
| PrintClasses -> CT_print_classes
+ | PrintLtac qid -> CT_print_ltac (loc_qualid_to_ct_ID qid)
| PrintCoercions -> CT_print_coercions
| PrintCoercionPaths (id1, id2) ->
CT_print_path (xlate_class id1, xlate_class id2)
+ | PrintCanonicalConversions ->
+ xlate_error "TODO: Print Canonical Structures"
| PrintInspect n -> CT_inspect (CT_int n)
| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
- | PrintLocalContext -> CT_print
+ | PrintSetoids -> CT_print_setoids
| PrintTables -> CT_print_tables
| PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
| PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
@@ -1867,13 +1871,12 @@ let rec xlate_vernac =
translate_opt_notation_decl notopt) in
CT_mind_decl
(CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
- | VernacFixpoint [] -> xlate_error "mutual recursive"
- | VernacFixpoint (lm :: lmi) ->
- let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
+ | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
+ | VernacFixpoint ((lm :: lmi),boxed) ->
+ let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) =
let (struct_arg,bl,arf,ardef) =
if bl = [] then
let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
- let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
@@ -1885,8 +1888,8 @@ let rec xlate_vernac =
| _ -> xlate_error "mutual recursive" in
CT_fix_decl
(CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
- | VernacCoFixpoint [] -> xlate_error "mutual corecursive"
- | VernacCoFixpoint (lm :: lmi) ->
+ | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
+ | VernacCoFixpoint ((lm :: lmi),boxed) ->
let strip_mutcorec (fid, bl, arf, ardef) =
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
xlate_formula arf, xlate_formula ardef) in
@@ -1916,20 +1919,18 @@ let rec xlate_vernac =
| Some mty1 ->
CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
(xlate_module_type mty1))
- | VernacDefineModule((_, id), bl, mty_o, mexpr_o) ->
+ | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
CT_module(xlate_ident id,
xlate_module_binder_list bl,
xlate_module_type_check_opt mty_o,
match mexpr_o with
None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
| Some m -> xlate_module_expr m)
- | VernacDeclareModule((_, id), bl, mty_o, mexpr_o) ->
+ | VernacDeclareModule(_,(_, id), bl, mty_o) ->
CT_declare_module(xlate_ident id,
xlate_module_binder_list bl,
- xlate_module_type_check_opt mty_o,
- match mexpr_o with
- None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
- | Some m -> xlate_module_expr m)
+ xlate_module_type_check_opt (Some mty_o),
+ CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
| VernacRequire (impexp, spec, id::idl) ->
let ct_impexp, ct_spec = get_require_flags impexp spec in
CT_require (ct_impexp, ct_spec,
@@ -1943,8 +1944,6 @@ let rec xlate_vernac =
CT_require(ct_impexp, ct_spec,
CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
- | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
-
| VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
| VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
| VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
@@ -1966,8 +1965,7 @@ let rec xlate_vernac =
CT_id_ne_list(xlate_class_rawexpr a,
List.map xlate_class_rawexpr l))
| VernacBindScope(id, []) -> assert false
- | VernacNotation(b, c, None, _, _) -> assert false
- | VernacNotation(b, c, Some(s,modif_list), _, opt_scope) ->
+ | VernacNotation(b, c, (s,modif_list), opt_scope) ->
let translated_s = CT_string s in
let formula = xlate_formula c in
let translated_modif_list =
@@ -1981,7 +1979,7 @@ let rec xlate_vernac =
else
CT_define_notation(translated_s, formula,
translated_modif_list, translated_scope)
- | VernacSyntaxExtension(b,Some(s,modif_list), None) ->
+ | VernacSyntaxExtension(b,(s,modif_list)) ->
let translated_s = CT_string s in
let translated_modif_list =
CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
@@ -1989,8 +1987,7 @@ let rec xlate_vernac =
CT_local_reserve_notation(translated_s, translated_modif_list)
else
CT_reserve_notation(translated_s, translated_modif_list)
- | VernacSyntaxExtension(_, _, _) -> assert false
- | VernacInfix (b,(str,modl),id,_, opt_scope) ->
+ | VernacInfix (b,(str,modl),id, opt_scope) ->
let id1 = loc_qualid_to_ct_ID id in
let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
let s = CT_string str in
@@ -2001,7 +1998,6 @@ let rec xlate_vernac =
CT_local_infix(s, id1,modl1, translated_scope)
else
CT_infix(s, id1,modl1, translated_scope)
- | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
| VernacCoercion (s, id1, id2, id3) ->
let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
let local_opt =
@@ -2032,8 +2028,6 @@ let rec xlate_vernac =
(CT_command_list(xlate_vernac a,
List.map (fun (_, x) -> xlate_vernac x) l))
| VernacList([]) -> assert false
- | (VernacV7only _ | VernacV8only _) ->
- xlate_error "Not treated here"
| VernacNop -> CT_proof_no_op
| VernacComments l ->
CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
@@ -2057,6 +2051,7 @@ let rec xlate_vernac =
| VernacReserve([], _) -> assert false
| VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
| VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
+ | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module"
| VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
| VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
| VernacTime(v) -> CT_time(xlate_vernac v)
@@ -2113,9 +2108,9 @@ let rec xlate_vernac =
| VernacVar _ -> xlate_error "Grammar vernac obsolete"
| (VernacGlobalCheck _|VernacPrintOption _|
VernacMemOption (_, _)|VernacRemoveOption (_, _)
- | VernacBack _|VernacRestoreState _| VernacWriteState _|
- VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _|
- VernacTacticGrammar _)
+ | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
+ VernacSolveExistential (_, _)|VernacCanonical _ |
+ VernacTacticNotation _)
-> xlate_error "TODO: vernac";;
let rec xlate_vernac_list =
@@ -2123,8 +2118,5 @@ let rec xlate_vernac_list =
| VernacList (v::l) ->
CT_command_list
(xlate_vernac (snd v), List.map (fun (_,x) -> xlate_vernac x) l)
- | VernacV7only v ->
- if !Options.v7 then xlate_vernac_list v
- else xlate_error "Unknown command"
| VernacList [] -> xlate_error "xlate_command_list"
| _ -> xlate_error "Not a list of commands";;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 20:09:45 +0000