diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/interface/ascent.mli | 20 | ||||
-rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 32 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 79 |
4 files changed, 88 insertions, 45 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index a1f6e2489..790ffb4b3 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -267,6 +267,10 @@ and ct_ID_OPT_OR_ALL = and ct_ID_OR_INT = CT_coerce_ID_to_ID_OR_INT of ct_ID | CT_coerce_INT_to_ID_OR_INT of ct_INT +and ct_ID_OR_INT_OPT = + CT_coerce_ID_OPT_to_ID_OR_INT_OPT of ct_ID_OPT + | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT of ct_ID_OR_INT + | CT_coerce_INT_OPT_to_ID_OR_INT_OPT of ct_INT_OPT and ct_ID_OR_STRING = CT_coerce_ID_to_ID_OR_STRING of ct_ID | CT_coerce_STRING_to_ID_OR_STRING of ct_STRING @@ -443,16 +447,16 @@ and ct_TACTIC_COM = | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT | CT_dconcl | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA - | CT_depinversion of ct_INV_TYPE * ct_ID * ct_FORMULA_OPT + | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_FORMULA_OPT | CT_deprewrite_lr of ct_ID | CT_deprewrite_rl of ct_ID | CT_destruct of ct_ID_OR_INT | CT_dhyp of ct_ID - | CT_discriminate_eq of ct_ID_OPT + | CT_discriminate_eq of ct_ID_OR_INT_OPT | CT_do of ct_INT * ct_TACTIC_COM | CT_eapply of ct_FORMULA * ct_SPEC_LIST - | CT_eauto of ct_INT_OPT - | CT_eauto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR + | CT_eauto of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT + | CT_eauto_with of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT * ct_ID_NE_LIST_OR_STAR | CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING | CT_elim_type of ct_FORMULA | CT_exact of ct_FORMULA @@ -465,12 +469,12 @@ and ct_TACTIC_COM = | CT_idtac | CT_induction of ct_ID_OR_INT | CT_info of ct_TACTIC_COM - | CT_injection_eq of ct_ID_OPT + | CT_injection_eq of ct_ID_OR_INT_OPT | 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 - | CT_inversion of ct_INV_TYPE * ct_ID * ct_ID_LIST + | 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_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list @@ -504,7 +508,7 @@ and ct_TACTIC_COM = | CT_trivial_with of ct_ID_NE_LIST_OR_STAR | CT_try of ct_TACTIC_COM | CT_use of ct_FORMULA - | CT_use_inversion of ct_ID * ct_FORMULA * ct_ID_LIST + | CT_use_inversion of ct_ID_OR_INT * ct_FORMULA * ct_ID_LIST | CT_user_tac of ct_ID * ct_TARG_LIST and ct_TACTIC_OPT = CT_coerce_NONE_to_TACTIC_OPT of ct_NONE @@ -563,8 +567,8 @@ and ct_VARG = | CT_coerce_FORMULA_LIST_to_VARG of ct_FORMULA_LIST | CT_coerce_FORMULA_OPT_to_VARG of ct_FORMULA_OPT | 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 - | CT_coerce_INT_OPT_to_VARG of ct_INT_OPT | CT_coerce_STRING_OPT_to_VARG of ct_STRING_OPT | CT_coerce_TACTIC_OPT_to_VARG of ct_TACTIC_OPT | CT_coerce_VARG_LIST_to_VARG of ct_VARG_LIST diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 79375cf2b..b35a5f56f 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -177,7 +177,7 @@ let constant_to_ast_list kn = None -> make_variable_ast (id_of_label (label kn)) typ l | Some c1 -> - make_definition_ast (id_of_label (label kn)) c1 typ l) + make_definition_ast (id_of_label (label kn)) (Lazy.force_val c1) typ l) let variable_to_ast_list sp = let ((id, c, v), _) = get_variable sp in diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index e2f519504..219584113 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -663,6 +663,10 @@ and fID_OPT_OR_ALL = function and fID_OR_INT = function | CT_coerce_ID_to_ID_OR_INT x -> fID x | CT_coerce_INT_to_ID_OR_INT x -> fINT x +and fID_OR_INT_OPT = function +| CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x +| CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x +| CT_coerce_INT_OPT_to_ID_OR_INT_OPT x -> fINT_OPT x and fID_OR_STRING = function | CT_coerce_ID_to_ID_OR_STRING x -> fID x | CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x @@ -1019,7 +1023,7 @@ and fTACTIC_COM = function fNODE "decompose_list" 2 | CT_depinversion(x1, x2, x3) -> fINV_TYPE x1; - fID x2; + fID_OR_INT x2; fFORMULA_OPT x3; fNODE "depinversion" 3 | CT_deprewrite_lr(x1) -> @@ -1035,7 +1039,7 @@ and fTACTIC_COM = function fID x1; fNODE "dhyp" 1 | CT_discriminate_eq(x1) -> - fID_OPT x1; + fID_OR_INT_OPT x1; fNODE "discriminate_eq" 1 | CT_do(x1, x2) -> fINT x1; @@ -1045,13 +1049,15 @@ and fTACTIC_COM = function fFORMULA x1; fSPEC_LIST x2; fNODE "eapply" 2 -| CT_eauto(x1) -> - fINT_OPT x1; - fNODE "eauto" 1 -| CT_eauto_with(x1, x2) -> - fINT_OPT x1; - fID_NE_LIST_OR_STAR x2; - fNODE "eauto_with" 2 +| CT_eauto(x1, x2) -> + fID_OR_INT_OPT x1; + fID_OR_INT_OPT x2; + fNODE "eauto" 2 +| CT_eauto_with(x1, x2, x3) -> + fID_OR_INT_OPT x1; + fID_OR_INT_OPT x2; + fID_NE_LIST_OR_STAR x3; + fNODE "eauto_with" 3 | CT_elim(x1, x2, x3) -> fFORMULA x1; fSPEC_LIST x2; @@ -1092,7 +1098,7 @@ and fTACTIC_COM = function fTACTIC_COM x1; fNODE "info" 1 | CT_injection_eq(x1) -> - fID_OPT x1; + fID_OR_INT_OPT x1; fNODE "injection_eq" 1 | CT_intro(x1) -> fID_OPT x1; @@ -1109,7 +1115,7 @@ and fTACTIC_COM = function fNODE "intros_until" 1 | CT_inversion(x1, x2, x3) -> fINV_TYPE x1; - fID x2; + fID_OR_INT x2; fID_LIST x3; fNODE "inversion" 3 | CT_left(x1) -> @@ -1228,7 +1234,7 @@ and fTACTIC_COM = function fFORMULA x1; fNODE "use" 1 | CT_use_inversion(x1, x2, x3) -> - fID x1; + fID_OR_INT x1; fFORMULA x2; fID_LIST x3; fNODE "use_inversion" 3 @@ -1327,8 +1333,8 @@ and fVAR = function | CT_coerce_FORMULA_LIST_to_VARG x -> fFORMULA_LIST x | CT_coerce_FORMULA_OPT_to_VARG x -> fFORMULA_OPT 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 -| CT_coerce_INT_OPT_to_VARG x -> fINT_OPT x | CT_coerce_STRING_OPT_to_VARG x -> fSTRING_OPT x | CT_coerce_TACTIC_OPT_to_VARG x -> fTACTIC_OPT x | CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 700fa0f7c..4e4b51833 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -203,6 +203,18 @@ let xlate_int = | Num (_, n) -> CT_int n | _ -> xlate_error "xlate_int: not an int";; +let xlate_id_to_id_or_int_opt s = + CT_coerce_ID_OPT_to_ID_OR_INT_OPT + (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id s)));; + +let xlate_int_to_id_or_int_opt n = + CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT + (CT_coerce_INT_to_ID_OR_INT (CT_int n));; + +let none_in_id_or_int_opt = + CT_coerce_ID_OPT_to_ID_OR_INT_OPT + (CT_coerce_NONE_to_ID_OPT(CT_none));; + let xlate_int_opt = function | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n) | None -> CT_coerce_NONE_to_INT_OPT CT_none @@ -846,6 +858,12 @@ let xlate_quantified_hypothesis = function | AnonHyp n -> CT_coerce_INT_to_ID_OR_INT (CT_int n) | NamedHyp id -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id) +let xlate_quantified_hypothesis_opt = function + | None -> + CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE + | Some (AnonHyp n) -> xlate_int_to_id_or_int_opt n + | Some (NamedHyp id) -> xlate_id_to_id_or_int_opt id;; + let xlate_explicit_binding (h,c) = CT_binding (xlate_quantified_hypothesis h, xlate_constr c) @@ -1094,13 +1112,15 @@ and xlate_tac = | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2" | TacExtend ("Discriminate", [idopt]) -> CT_discriminate_eq - (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt)) + (xlate_quantified_hypothesis_opt + (out_gen (wit_opt rawwit_quant_hyp) idopt)) | TacExtend ("DEq", [idopt]) -> CT_simplify_eq (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt)) | TacExtend ("Injection", [idopt]) -> CT_injection_eq - (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt)) + (xlate_quantified_hypothesis_opt + (out_gen (wit_opt rawwit_quant_hyp) idopt)) | TacFix (idopt, n) -> CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list []) | TacMutualFix (id, n, fixtac_list) -> @@ -1205,15 +1225,26 @@ and xlate_tac = 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))) | TacExtend ("EAuto", [nopt; popt; idl]) -> - let control = - match out_gen (wit_opt rawwit_int_or_var) nopt with - | Some breadth -> Some (true, breadth) - | None -> - match out_gen (wit_opt rawwit_int_or_var) popt with - | Some depth -> Some (false, depth) - | None -> None in - let idl = out_gen (wit_opt (wit_list0 rawwit_string)) idl in - xlate_error "TODO: EAuto n p" + 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 + | Some ArgArg n -> xlate_int_to_id_or_int_opt n + | None -> none_in_id_or_int_opt in + let second_n = + match out_gen (wit_opt rawwit_int_or_var) popt with + | 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 idl = out_gen Eauto.rawwit_hintbases idl in + (match idl with + None -> CT_eauto_with(first_n, second_n, CT_star) + | Some [] -> CT_eauto(first_n, second_n) + | Some (a::l) -> + CT_eauto_with(first_n, second_n, + CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR + (CT_id_ne_list + (CT_ident a, + List.map (fun x -> CT_ident x) l)))) | TacExtend ("Prolog", [cl; n]) -> let cl = List.map xlate_constr (out_gen (wit_list0 rawwit_constr) cl) in (match out_gen wit_int_or_var n with @@ -1272,15 +1303,13 @@ and xlate_tac = CT_clear (CT_id_ne_list (ident_or_meta_to_ct_ID id, idl')) | (*For translating tactics/Inv.v *) TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s, [id]) -> - let quant_hyp = (out_gen rawwit_quant_hyp id) in - (match quant_hyp with - NamedHyp id1 -> let id = xlate_ident id1 in - CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list []) - | AnonHyp _ -> assert false) + let quant_hyp = out_gen rawwit_quant_hyp id in + CT_inversion(compute_INV_TYPE_from_string s, + xlate_quantified_hypothesis quant_hyp, CT_id_list []) | TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s, [id;copt_or_idl]) -> -(* TODO: rawwit_ident should be rawwit_quant_hyp *) - let id = xlate_ident (out_gen rawwit_ident id) in + let quant_hyp = (out_gen rawwit_quant_hyp id) in + let id = xlate_quantified_hypothesis quant_hyp in (match genarg_tag copt_or_idl with | List1ArgType IdentArgType -> (* InvIn *) let idl = out_gen (wit_list1 rawwit_ident) copt_or_idl in @@ -1292,11 +1321,11 @@ and xlate_tac = (compute_INV_TYPE_from_string s, id, xlate_constr_opt copt) | _ -> xlate_error "") | TacExtend ("InversionUsing", [id; c]) -> - let id = xlate_ident (out_gen rawwit_ident id) in + let id = xlate_quantified_hypothesis (out_gen rawwit_quant_hyp id) in let c = out_gen rawwit_constr c in CT_use_inversion (id, xlate_constr c, CT_id_list []) | TacExtend ("InversionUsing", [id; c; idlist]) -> - let id = xlate_ident (out_gen rawwit_ident id) in + let id = xlate_quantified_hypothesis (out_gen rawwit_quant_hyp id) in let c = out_gen rawwit_constr c in let idlist = out_gen (wit_list1 rawwit_ident) idlist in CT_use_inversion (id, xlate_constr c, @@ -1385,11 +1414,15 @@ let coerce_genarg_to_VARG x = | BoolArgType -> xlate_error "TODO: generic boolean argument" | IntArgType -> let n = out_gen rawwit_int x in - CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT (CT_int n)) + CT_coerce_ID_OR_INT_OPT_to_VARG + (CT_coerce_INT_OPT_to_ID_OR_INT_OPT + (CT_coerce_INT_to_INT_OPT (CT_int n))) | IntOrVarArgType -> (match out_gen rawwit_int_or_var x with | ArgArg n -> - CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT (CT_int n)) + CT_coerce_ID_OR_INT_OPT_to_VARG + (CT_coerce_INT_OPT_to_ID_OR_INT_OPT + (CT_coerce_INT_to_INT_OPT (CT_int n))) | ArgVar (_,id) -> CT_coerce_ID_OPT_OR_ALL_to_VARG (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL @@ -1626,7 +1659,7 @@ let xlate_vernac = | VernacFocus nopt -> CT_focus (xlate_int_opt nopt) | VernacUnfocus -> CT_unfocus | VernacExtend ("HintRewrite", orient :: formula_list :: base :: t) -> - let orient = out_gen rawwit_bool orient in + let orient = out_gen Extraargs.rawwit_orient orient in let formula_list = out_gen (wit_list1 (rawwit_constr)) formula_list in let base = out_gen rawwit_pre_ident base in let t = match t with |