diff options
| -rw-r--r-- | contrib/interface/ascent.mli | 27 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml4 | 5 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 58 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 137 |
4 files changed, 175 insertions, 52 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index d9641bd34..428606be7 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -249,6 +249,9 @@ and ct_FORMULA_NE_LIST = and ct_FORMULA_OPT = CT_coerce_FORMULA_to_FORMULA_OPT of ct_FORMULA | CT_coerce_ID_OPT_to_FORMULA_OPT of ct_ID_OPT +and ct_FORMULA_OR_INT = + CT_coerce_FORMULA_to_FORMULA_OR_INT of ct_FORMULA + | CT_coerce_ID_OR_INT_to_FORMULA_OR_INT of ct_ID_OR_INT and ct_GRAMMAR = CT_grammar_none and ct_HINT_EXPRESSION = @@ -260,11 +263,14 @@ and ct_HINT_EXPRESSION = and ct_ID = CT_ident of string | CT_metac of ct_INT + | CT_metaid of string and ct_IDENTITY_OPT = CT_coerce_NONE_to_IDENTITY_OPT of ct_NONE | CT_identity and ct_ID_LIST = CT_id_list of ct_ID list +and ct_ID_LIST_LIST = + CT_id_list_list of ct_ID_LIST list and ct_ID_NE_LIST = CT_id_ne_list of ct_ID * ct_ID list and ct_ID_NE_LIST_OR_STAR = @@ -447,8 +453,7 @@ and ct_STRING_OPT = | CT_coerce_STRING_to_STRING_OPT of ct_STRING and ct_TACTIC_ARG = CT_coerce_EVAL_CMD_to_TACTIC_ARG of ct_EVAL_CMD - | CT_coerce_FORMULA_to_TACTIC_ARG of ct_FORMULA - | CT_coerce_ID_OR_INT_to_TACTIC_ARG of ct_ID_OR_INT + | CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG of ct_FORMULA_OR_INT | CT_coerce_TACTIC_COM_to_TACTIC_ARG of ct_TACTIC_COM | CT_coerce_TERM_CHANGE_to_TACTIC_ARG of ct_TERM_CHANGE | CT_void @@ -457,8 +462,9 @@ and ct_TACTIC_ARG_LIST = and ct_TACTIC_COM = CT_abstract of ct_ID_OPT * ct_TACTIC_COM | CT_absurd of ct_FORMULA + | CT_any_constructor of ct_TACTIC_OPT | CT_apply of ct_FORMULA * ct_SPEC_LIST - | CT_assert of ct_ID * ct_FORMULA + | CT_assert of ct_ID_OPT * ct_FORMULA | CT_assumption | CT_auto of ct_INT_OPT | CT_auto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR @@ -470,6 +476,7 @@ and ct_TACTIC_COM = | CT_change of ct_FORMULA * ct_ID_OR_INTYPE_LIST | CT_change_local of ct_PATTERN * ct_FORMULA * ct_ID_OR_INTYPE_LIST | CT_clear of ct_ID_NE_LIST + | CT_clear_body of ct_ID_NE_LIST | CT_cofixtactic of ct_ID_OPT * ct_COFIX_TAC_LIST | CT_condrewrite_lr of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT | CT_condrewrite_rl of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT @@ -478,6 +485,7 @@ and ct_TACTIC_COM = | CT_cut of ct_FORMULA | CT_cutrewrite_lr of ct_FORMULA * ct_ID_OPT | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT + | CT_dauto of ct_INT_OPT * ct_INT_OPT | CT_dconcl | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA | CT_decompose_record of ct_FORMULA @@ -505,21 +513,25 @@ and ct_TACTIC_COM = | CT_induction of ct_ID_OR_INT | CT_info of ct_TACTIC_COM | CT_injection_eq of ct_ID_OR_INT_OPT + | CT_instantiate of ct_INT * ct_FORMULA | CT_intro of ct_ID_OPT | CT_intro_after of ct_ID_OPT * ct_ID | CT_intros of ct_INTRO_PATT_LIST | CT_intros_until of ct_ID_OR_INT | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST | CT_left of ct_SPEC_LIST - | CT_lettac of ct_LET_CLAUSES * ct_LET_VALUE + | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE + | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_LIST | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | CT_match_tac of ct_LET_VALUE * ct_MATCH_TAC_RULES | CT_move_after of ct_ID * ct_ID + | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST + | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST | CT_omega | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list - | CT_pose of ct_ID * ct_FORMULA + | CT_pose of ct_ID_OPT * ct_FORMULA | CT_progress of ct_TACTIC_COM | CT_prolog of ct_FORMULA_LIST * ct_INT | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM @@ -557,7 +569,7 @@ and ct_TARG = CT_coerce_BINDING_to_TARG of ct_BINDING | CT_coerce_COFIXTAC_to_TARG of ct_COFIXTAC | CT_coerce_FIXTAC_to_TARG of ct_FIXTAC - | CT_coerce_ID_OR_INT_to_TARG of ct_ID_OR_INT + | CT_coerce_FORMULA_OR_INT_to_TARG of ct_FORMULA_OR_INT | CT_coerce_PATTERN_to_TARG of ct_PATTERN | CT_coerce_SCOMMENT_CONTENT_to_TARG of ct_SCOMMENT_CONTENT | CT_coerce_SIGNED_INT_LIST_to_TARG of ct_SIGNED_INT_LIST @@ -590,6 +602,8 @@ and ct_TYPED_FORMULA = CT_typed_formula of ct_FORMULA * ct_FORMULA and ct_UNFOLD = CT_unfold_occ of ct_INT_LIST * ct_ID +and ct_UNFOLD_LIST = + CT_unfold_list of ct_UNFOLD list and ct_UNFOLD_NE_LIST = CT_unfold_ne_list of ct_UNFOLD * ct_UNFOLD list and ct_USING = @@ -608,6 +622,7 @@ and ct_VARG = | CT_coerce_BINDER_NE_LIST_to_VARG of ct_BINDER_NE_LIST | CT_coerce_FORMULA_LIST_to_VARG of ct_FORMULA_LIST | CT_coerce_FORMULA_OPT_to_VARG of ct_FORMULA_OPT + | CT_coerce_FORMULA_OR_INT_to_VARG of ct_FORMULA_OR_INT | CT_coerce_ID_OPT_OR_ALL_to_VARG of ct_ID_OPT_OR_ALL | CT_coerce_ID_OR_INT_OPT_to_VARG of ct_ID_OR_INT_OPT | CT_coerce_INT_LIST_to_VARG of ct_INT_LIST diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index a2dcd7e20..c9197ab34 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -433,8 +433,9 @@ let inspect n = (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));; let ct_int_to_TARG n = - CT_coerce_ID_OR_INT_to_TARG - (CT_coerce_INT_to_ID_OR_INT (CT_int n));; + CT_coerce_FORMULA_OR_INT_to_TARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_INT_to_ID_OR_INT (CT_int n)));; let pair_list_to_ct l = CT_user_tac(CT_ident "pair_int_list", diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 34cb2a816..df83a0499 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -648,6 +648,9 @@ and fFORMULA_NE_LIST = function and fFORMULA_OPT = function | CT_coerce_FORMULA_to_FORMULA_OPT x -> fFORMULA x | CT_coerce_ID_OPT_to_FORMULA_OPT x -> fID_OPT x +and fFORMULA_OR_INT = function +| CT_coerce_FORMULA_to_FORMULA_OR_INT x -> fFORMULA x +| CT_coerce_ID_OR_INT_to_FORMULA_OR_INT x -> fID_OR_INT x and fGRAMMAR = function | CT_grammar_none -> fNODE "grammar_none" 0 and fHINT_EXPRESSION = function @@ -674,13 +677,19 @@ and fID = function print_string "\n"| CT_metac(x1) -> fINT x1; fNODE "metac" 1 -and fIDENTITY_OPT = function +| CT_metaid x -> fATOM "metaid"; + (f_atom_string x); + print_string "\n"and fIDENTITY_OPT = function | CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x | CT_identity -> fNODE "identity" 0 and fID_LIST = function | CT_id_list l -> (List.iter fID l); fNODE "id_list" (List.length l) +and fID_LIST_LIST = function +| CT_id_list_list l -> + (List.iter fID_LIST l); + fNODE "id_list_list" (List.length l) and fID_NE_LIST = function | CT_id_ne_list(x,l) -> fID x; @@ -997,8 +1006,7 @@ and fSTRING_OPT = function | CT_coerce_STRING_to_STRING_OPT x -> fSTRING x and fTACTIC_ARG = function | CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x -| CT_coerce_FORMULA_to_TACTIC_ARG x -> fFORMULA x -| CT_coerce_ID_OR_INT_to_TACTIC_ARG x -> fID_OR_INT x +| CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG x -> fFORMULA_OR_INT x | CT_coerce_TACTIC_COM_to_TACTIC_ARG x -> fTACTIC_COM x | CT_coerce_TERM_CHANGE_to_TACTIC_ARG x -> fTERM_CHANGE x | CT_void -> fNODE "void" 0 @@ -1015,12 +1023,15 @@ and fTACTIC_COM = function | CT_absurd(x1) -> fFORMULA x1; fNODE "absurd" 1 +| CT_any_constructor(x1) -> + fTACTIC_OPT x1; + fNODE "any_constructor" 1 | CT_apply(x1, x2) -> fFORMULA x1; fSPEC_LIST x2; fNODE "apply" 2 | CT_assert(x1, x2) -> - fID x1; + fID_OPT x1; fFORMULA x2; fNODE "assert" 2 | CT_assumption -> fNODE "assumption" 0 @@ -1060,6 +1071,9 @@ and fTACTIC_COM = function | CT_clear(x1) -> fID_NE_LIST x1; fNODE "clear" 1 +| CT_clear_body(x1) -> + fID_NE_LIST x1; + fNODE "clear_body" 1 | CT_cofixtactic(x1, x2) -> fID_OPT x1; fCOFIX_TAC_LIST x2; @@ -1092,6 +1106,10 @@ and fTACTIC_COM = function fFORMULA x1; fID_OPT x2; fNODE "cutrewrite_rl" 2 +| CT_dauto(x1, x2) -> + fINT_OPT x1; + fINT_OPT x2; + fNODE "dauto" 2 | CT_dconcl -> fNODE "dconcl" 0 | CT_decompose_list(x1, x2) -> fID_NE_LIST x1; @@ -1182,6 +1200,10 @@ and fTACTIC_COM = function | CT_injection_eq(x1) -> fID_OR_INT_OPT x1; fNODE "injection_eq" 1 +| CT_instantiate(x1, x2) -> + fINT x1; + fFORMULA x2; + fNODE "instantiate" 2 | CT_intro(x1) -> fID_OPT x1; fNODE "intro" 1 @@ -1203,10 +1225,15 @@ and fTACTIC_COM = function | CT_left(x1) -> fSPEC_LIST x1; fNODE "left" 1 -| CT_lettac(x1, x2) -> +| CT_let_ltac(x1, x2) -> fLET_CLAUSES x1; fLET_VALUE x2; - fNODE "lettac" 2 + fNODE "let_ltac" 2 +| CT_lettac(x1, x2, x3) -> + fID x1; + fFORMULA x2; + fUNFOLD_LIST x3; + fNODE "lettac" 3 | CT_match_context(x,l) -> fCONTEXT_RULE x; (List.iter fCONTEXT_RULE l); @@ -1223,6 +1250,16 @@ and fTACTIC_COM = function fID x1; fID x2; fNODE "move_after" 2 +| CT_new_destruct(x1, x2, x3) -> + fFORMULA_OR_INT x1; + fUSING x2; + fID_LIST_LIST x3; + fNODE "new_destruct" 3 +| CT_new_induction(x1, x2, x3) -> + fFORMULA_OR_INT x1; + fUSING x2; + fID_LIST_LIST x3; + fNODE "new_induction" 3 | CT_omega -> fNODE "omega" 0 | CT_orelse(x1, x2) -> fTACTIC_COM x1; @@ -1233,7 +1270,7 @@ and fTACTIC_COM = function (List.iter fTACTIC_COM l); fNODE "parallel" (1 + (List.length l)) | CT_pose(x1, x2) -> - fID x1; + fID_OPT x1; fFORMULA x2; fNODE "pose" 2 | CT_progress(x1) -> @@ -1350,7 +1387,7 @@ and fTARG = function | CT_coerce_BINDING_to_TARG x -> fBINDING x | CT_coerce_COFIXTAC_to_TARG x -> fCOFIXTAC x | CT_coerce_FIXTAC_to_TARG x -> fFIXTAC x -| CT_coerce_ID_OR_INT_to_TARG x -> fID_OR_INT x +| CT_coerce_FORMULA_OR_INT_to_TARG x -> fFORMULA_OR_INT x | CT_coerce_PATTERN_to_TARG x -> fPATTERN x | CT_coerce_SCOMMENT_CONTENT_to_TARG x -> fSCOMMENT_CONTENT x | CT_coerce_SIGNED_INT_LIST_to_TARG x -> fSIGNED_INT_LIST x @@ -1415,6 +1452,10 @@ and fUNFOLD = function fINT_LIST x1; fID x2; fNODE "unfold_occ" 2 +and fUNFOLD_LIST = function +| CT_unfold_list l -> + (List.iter fUNFOLD l); + fNODE "unfold_list" (List.length l) and fUNFOLD_NE_LIST = function | CT_unfold_ne_list(x,l) -> fUNFOLD x; @@ -1440,6 +1481,7 @@ and fVAR = function | CT_coerce_BINDER_NE_LIST_to_VARG x -> fBINDER_NE_LIST x | CT_coerce_FORMULA_LIST_to_VARG x -> fFORMULA_LIST x | CT_coerce_FORMULA_OPT_to_VARG x -> fFORMULA_OPT x +| CT_coerce_FORMULA_OR_INT_to_VARG x -> fFORMULA_OR_INT x | CT_coerce_ID_OPT_OR_ALL_to_VARG x -> fID_OPT_OR_ALL x | CT_coerce_ID_OR_INT_OPT_to_VARG x -> fID_OR_INT_OPT x | CT_coerce_INT_LIST_to_VARG x -> fINT_LIST x diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 43a2aad72..801f7208e 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -218,6 +218,7 @@ let xlate_class = function let id_to_pattern_var ctid = match ctid with + | CT_metaid _ -> xlate_error "metaid not expected in pattern_var" | CT_ident "_" -> CT_coerce_ID_OPT_to_MATCH_PATTERN (CT_coerce_NONE_to_ID_OPT CT_none) | CT_ident id_string -> @@ -380,7 +381,10 @@ and xlate_formula_ne_list = function [] -> assert false | a::l -> CT_formula_ne_list(xlate_formula a, List.map xlate_formula l);; - +let (xlate_ident_or_metaid: + Names.identifier Util.located Tacexpr.or_metaid -> ct_ID) = function + AI (_, x) -> xlate_ident x + | MetaId(_, x) -> CT_metaid x;; let xlate_hyp_location = function @@ -534,6 +538,39 @@ let xlate_largs_to_id_unit largs = fst::rest -> fst, rest | _ -> assert false;; +let xlate_int_or_constr = function + ElimOnConstr a -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a) + | ElimOnIdent(_,i) -> + CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_ID_to_ID_OR_INT(xlate_ident i)) + | ElimOnAnonHyp i -> + CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_INT_to_ID_OR_INT(CT_int i));; + +let xlate_using = function + None -> CT_coerce_NONE_to_USING(CT_none) + | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);; + +let xlate_one_unfold_block = function + (nums,qid) -> + CT_unfold_occ (CT_int_list (List.map (fun x -> CT_int x) nums), + qualid_or_meta_to_ct_ID qid);; + +let xlate_lettac_clauses = function + (opt_l, l') -> + let res = + (List.map + (fun (id, l) -> + CT_unfold_occ(CT_int_list (List.map (fun x -> CT_int x) l), + xlate_ident_or_metaid id)) l') in + match opt_l with + Some l -> + CT_unfold_list + ((CT_unfold_occ + (CT_int_list (List.map (fun x -> CT_int x) l), + CT_ident "Goal"))::res) + | None -> CT_unfold_list res;; + let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = function | TacVoid -> @@ -541,15 +578,18 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = | Tacexp t -> CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic t) | Integer n -> - CT_coerce_ID_OR_INT_to_TACTIC_ARG - (CT_coerce_INT_to_ID_OR_INT (CT_int n)) + CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_INT_to_ID_OR_INT (CT_int n))) | Reference r -> - CT_coerce_ID_OR_INT_to_TACTIC_ARG - (CT_coerce_ID_to_ID_OR_INT (reference_to_ct_ID r)) + CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_ID_to_ID_OR_INT (reference_to_ct_ID r))) | TacDynamic _ -> failwith "Dynamics not treated in xlate_ast" | ConstrMayEval (ConstrTerm c) -> - CT_coerce_FORMULA_to_TACTIC_ARG (xlate_formula c) + CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG + (CT_coerce_FORMULA_to_FORMULA_OR_INT (xlate_formula c)) | ConstrMayEval(ConstrEval(r,c)) -> CT_coerce_EVAL_CMD_to_TACTIC_ARG (CT_eval(CT_coerce_NONE_to_INT_OPT CT_none, xlate_red_tactic r, @@ -559,8 +599,9 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = | MetaIdArg _ -> xlate_error "MetaIdArg should only be used in quotations" | MetaNumArg (_,n) -> - CT_coerce_FORMULA_to_TACTIC_ARG - (CT_coerce_ID_to_FORMULA(CT_metac (CT_int n))) + CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_ID_to_ID_OR_INT(CT_metac (CT_int n)))) | t -> CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_call_or_tacarg t) @@ -592,9 +633,7 @@ and xlate_red_tactic = let conv_flags, red_ids = get_flag flag_list in CT_cbv (CT_conversion_flag_list conv_flags, red_ids) | Unfold unf_list -> - let ct_unf_list = List.map (fun (nums,qid) -> - CT_unfold_occ (CT_int_list (List.map (fun x -> CT_int x) nums), - qualid_or_meta_to_ct_ID qid)) unf_list in + let ct_unf_list = List.map xlate_one_unfold_block unf_list in (match ct_unf_list with | first :: others -> CT_unfold (CT_unfold_ne_list (first, others)) | [] -> error "there should be at least one thing to unfold") @@ -711,7 +750,7 @@ and xlate_tactic = (match cl_l with | [] -> assert false | fst::others -> - CT_lettac (CT_let_clauses(fst, others), mk_let_value t)) + CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t)) | TacLetCut _ -> xlate_error "Unclear future of syntax Let x := t" | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition" | TacLetRecIn(f1::l, t) -> @@ -907,12 +946,8 @@ and xlate_tac = CT_generalize_dependent (xlate_formula c) | TacElimType c -> CT_elim_type (xlate_formula c) | TacCaseType c -> CT_case_type (xlate_formula c) - | TacElim ((c1,sl), None) -> - CT_elim (xlate_formula c1, xlate_bindings sl, - CT_coerce_NONE_to_USING CT_none) - | TacElim ((c1,sl), Some (c2,sl2)) -> - CT_elim (xlate_formula c1, xlate_bindings sl, - CT_using (xlate_formula c2, xlate_bindings sl2)) + | TacElim ((c1,sl), u) -> + CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u) | TacCase (c1,sl) -> CT_casetac (xlate_formula c1, xlate_bindings sl) | TacOldInduction h -> CT_induction (xlate_quantified_hypothesis h) @@ -964,20 +999,41 @@ and xlate_tac = CT_id_list (List.map xlate_ident idlist)) | TacExtend (_,"Omega", []) -> CT_omega | TacRename ((_,id1), (_,id2)) -> CT_rename(xlate_ident id1, xlate_ident id2) - | TacClearBody _ -> xlate_error "TODO: Clear Body H" - | TacDAuto (_, _) -> xlate_error "TODO: DAuto" - | TacNewDestruct _ -> xlate_error "TODO: NewDestruct" - | TacNewInduction _ -> xlate_error "TODO: NewInduction" - | TacInstantiate (_, _) -> xlate_error "TODO: Instantiate" - | TacLetTac (_, _, _) -> xlate_error "TODO: LetTac" - | TacForward (true, Name id, c) -> - CT_pose(CT_ident (string_of_id id), xlate_formula c) - | TacForward (false, Name id, c) -> - CT_assert(CT_ident (string_of_id id), xlate_formula c) - | TacForward (_, _, _) -> xlate_error "TODO: Assert/Pose id:=c" + | TacClearBody([]) -> assert false + | TacClearBody(a::l) -> + CT_clear_body + (CT_id_ne_list + (ident_or_meta_to_ct_ID a, List.map ident_or_meta_to_ct_ID l)) + | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b) + | TacNewDestruct(a,b,c) -> + CT_new_destruct + (xlate_int_or_constr a, xlate_using b, + CT_id_list_list + (List.map (fun l -> CT_id_list(List.map xlate_ident l)) c)) + | TacNewInduction(a,b,c) -> + CT_new_induction + (xlate_int_or_constr a, xlate_using b, + CT_id_list_list + (List.map (fun l -> CT_id_list(List.map xlate_ident l)) c)) + | TacInstantiate (a, b) -> + CT_instantiate(CT_int a, xlate_formula b) + | TacLetTac (id, c, cl) -> + CT_lettac(xlate_ident id, xlate_formula c, + (* TODO LATER: This should be shared with Unfold, + but the structures are different *) + xlate_lettac_clauses cl) + | TacForward (true, name, c) -> +(* TODO LATER : avoid adding a location that will be ignored *) + CT_pose(xlate_id_opt ((0,0), name), xlate_formula c) + | TacForward (false, name, c) -> + CT_assert(xlate_id_opt ((0,0),name), xlate_formula c) | TacTrueCut (idopt, c) -> CT_truecut(xlate_ident_opt idopt, xlate_formula c) - | TacAnyConstructor tacopt -> xlate_error "TODO: Constructor tac" + | TacAnyConstructor(Some tac) -> + CT_any_constructor + (CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac)) + | TacAnyConstructor(None) -> + CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none) | TacExtend(_, "Ring", [arg]) -> CT_ring (CT_formula_list @@ -985,7 +1041,7 @@ and xlate_tac = (out_gen (wit_list0 rawwit_constr) arg))) | TacExtend (_,id, l) -> CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l)) - | TacAlias (_, _, _) -> xlate_error "TODO: aliases" + | TacAlias (_, _, _) -> xlate_error "TODO LATER: aliases" and coerce_genarg_to_TARG x = match Genarg.genarg_tag x with @@ -993,12 +1049,15 @@ and coerce_genarg_to_TARG x = | BoolArgType -> xlate_error "TODO: generic boolean argument" | IntArgType -> let n = out_gen rawwit_int x in - CT_coerce_ID_OR_INT_to_TARG (CT_coerce_INT_to_ID_OR_INT (CT_int n)) + CT_coerce_FORMULA_OR_INT_to_TARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_INT_to_ID_OR_INT (CT_int n))) | IntOrVarArgType -> let x = match out_gen rawwit_int_or_var x with | ArgArg n -> CT_coerce_INT_to_ID_OR_INT (CT_int n) | ArgVar (_,id) -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id) in - CT_coerce_ID_OR_INT_to_TARG x + CT_coerce_FORMULA_OR_INT_to_TARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT x) | StringArgType -> let s = CT_string (out_gen rawwit_string x) in CT_coerce_SCOMMENT_CONTENT_to_TARG @@ -1006,13 +1065,19 @@ and coerce_genarg_to_TARG x = (CT_coerce_STRING_to_ID_OR_STRING s)) | PreIdentArgType -> let id = CT_ident (out_gen rawwit_pre_ident x) in - CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id) + CT_coerce_FORMULA_OR_INT_to_TARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_ID_to_ID_OR_INT id)) | IdentArgType -> let id = xlate_ident (out_gen rawwit_ident x) in - CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id) + 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_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id) + CT_coerce_FORMULA_OR_INT_to_TARG + (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT + (CT_coerce_ID_to_ID_OR_INT id)) (* Specific types *) | SortArgType -> CT_coerce_SCOMMENT_CONTENT_to_TARG |