diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/interface/ascent.mli | 11 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 25 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 36 |
3 files changed, 46 insertions, 26 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 829972ecf..7106b5d65 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -187,6 +187,9 @@ and ct_CONV_SET = | CT_unfbut of ct_ID list and ct_CO_IND = CT_co_ind of string +and ct_DECL_NOTATION_OPT = + CT_coerce_NONE_to_DECL_NOTATION_OPT of ct_NONE + | CT_decl_notation of ct_STRING * ct_FORMULA * ct_ID_OPT and ct_DEF = CT_def of ct_ID_OPT * ct_FORMULA and ct_DEFN = @@ -317,7 +320,7 @@ and ct_IMPEXP = CT_export | CT_import and ct_IND_SPEC = - CT_ind_spec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_CONSTR_LIST + CT_ind_spec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_CONSTR_LIST * ct_DECL_NOTATION_OPT and ct_IND_SPEC_LIST = CT_ind_spec_list of ct_IND_SPEC list and ct_INT = @@ -532,12 +535,12 @@ and ct_TACTIC_COM = | CT_elim_type of ct_FORMULA | CT_exact of ct_FORMULA | CT_exists of ct_SPEC_LIST - | CT_fail of ct_INT + | CT_fail of ct_INT * ct_STRING_OPT | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list | CT_fixtactic of ct_ID_OPT * ct_INT * ct_FIX_TAC_LIST | CT_generalize of ct_FORMULA_NE_LIST | CT_generalize_dependent of ct_FORMULA - | CT_idtac + | CT_idtac of ct_STRING_OPT | CT_induction of ct_ID_OR_INT | CT_info of ct_TACTIC_COM | CT_injection_eq of ct_ID_OR_INT_OPT @@ -554,7 +557,7 @@ and ct_TACTIC_COM = | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | CT_match_tac of ct_TACTIC_COM * 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_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST | CT_omega | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index eeb09b2a9..f3610f4d3 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -500,7 +500,14 @@ and fCONV_SET = function and fCO_IND = function | CT_co_ind x -> fATOM "co_ind"; (f_atom_string x); - print_string "\n"and fDEF = function + print_string "\n"and fDECL_NOTATION_OPT = function +| CT_coerce_NONE_to_DECL_NOTATION_OPT x -> fNONE x +| CT_decl_notation(x1, x2, x3) -> + fSTRING x1; + fFORMULA x2; + fID_OPT x3; + fNODE "decl_notation" 3 +and fDEF = function | CT_def(x1, x2) -> fID_OPT x1; fFORMULA x2; @@ -772,12 +779,13 @@ and fIMPEXP = function | CT_export -> fNODE "export" 0 | CT_import -> fNODE "import" 0 and fIND_SPEC = function -| CT_ind_spec(x1, x2, x3, x4) -> +| CT_ind_spec(x1, x2, x3, x4, x5) -> fID x1; fBINDER_LIST x2; fFORMULA x3; fCONSTR_LIST x4; - fNODE "ind_spec" 4 + fDECL_NOTATION_OPT x5; + fNODE "ind_spec" 5 and fIND_SPEC_LIST = function | CT_ind_spec_list l -> (List.iter fIND_SPEC l); @@ -1248,9 +1256,10 @@ and fTACTIC_COM = function | CT_exists(x1) -> fSPEC_LIST x1; fNODE "exists" 1 -| CT_fail(x1) -> +| CT_fail(x1, x2) -> fINT x1; - fNODE "fail" 1 + fSTRING_OPT x2; + fNODE "fail" 2 | CT_first(x,l) -> fTACTIC_COM x; (List.iter fTACTIC_COM l); @@ -1266,7 +1275,9 @@ and fTACTIC_COM = function | CT_generalize_dependent(x1) -> fFORMULA x1; fNODE "generalize_dependent" 1 -| CT_idtac -> fNODE "idtac" 0 +| CT_idtac(x1) -> + fSTRING_OPT x1; + fNODE "idtac" 1 | CT_induction(x1) -> fID_OR_INT x1; fNODE "induction" 1 @@ -1330,7 +1341,7 @@ and fTACTIC_COM = function | CT_new_destruct(x1, x2, x3) -> fFORMULA_OR_INT x1; fUSING x2; - fID_LIST_LIST x3; + fINTRO_PATT_LIST x3; fNODE "new_destruct" 3 | CT_new_induction(x1, x2, x3) -> fFORMULA_OR_INT x1; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 2d6cca540..aae7d714f 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -606,11 +606,6 @@ let rec xlate_intro_pattern = | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" ) | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c) -let xlate_newind_names = - function - | IntroIdentifier id -> xlate_ident id - | _ -> xlate_error "TODO: intro_patterns for NewDestruct/NewInduction" - let compute_INV_TYPE = function FullInversionClear -> CT_inv_clear | SimpleInversion -> CT_inv_simple @@ -853,10 +848,10 @@ 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 (n,"") -> CT_fail (CT_int n) - | TacFail (n,s) -> xlate_error "TODO: Fail n message" - | TacId "" -> CT_idtac - | TacId _ -> xlate_error "TODO: Idtac with argument" + | TacFail (n,"") -> CT_fail(CT_int n, ctf_STRING_OPT_NONE) + | TacFail (n,s) -> CT_fail(CT_int n, 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)) | TacInfo t -> CT_info(xlate_tactic t) | TacArg a -> xlate_call_or_tacarg a @@ -1095,8 +1090,11 @@ and xlate_tac = | 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_newind_names l)) c)) + (CT_intro_patt_list + (List.map (fun l -> + CT_conj_pattern + (CT_intro_patt_list + (List.map xlate_intro_pattern l))) c))) | TacNewInduction(a,b,(c,_)) -> CT_new_induction (xlate_int_or_constr a, xlate_using b, @@ -1391,6 +1389,15 @@ let xlate_comment = function CT_coerce_FORMULA_to_SCOMMENT_CONTENT (CT_coerce_NUM_to_FORMULA(CT_int_encapsulator (string_of_int n)));; +let translate_opt_notation_decl = function + None -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none) + | Some(s, f, sc) -> + let tr_sc = + match sc with + None -> ctv_ID_OPT_NONE + | Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in + CT_decl_notation(CT_string s, xlate_formula f, tr_sc);; + let xlate_vernac = function | VernacDeclareTacticDefinition (false,[(_,id),TacFun (largs,tac)]) -> @@ -1650,11 +1657,10 @@ let xlate_vernac = | VernacInductive (isind, lmi) -> let co_or_ind = if isind then "Inductive" else "CoInductive" in let strip_mutind ((_,s), notopt, parameters, c, constructors) = - if notopt = None then - CT_ind_spec + CT_ind_spec (xlate_ident s, xlate_binder_list parameters, xlate_formula c, - build_constructors constructors) - else xlate_error "TODO: Notation in Inductive" in + build_constructors constructors, + 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" |