diff options
Diffstat (limited to 'contrib/interface')
-rw-r--r-- | contrib/interface/ascent.mli | 6 | ||||
-rw-r--r-- | contrib/interface/blast.ml | 2 | ||||
-rw-r--r-- | contrib/interface/centaur.ml4 | 2 | ||||
-rw-r--r-- | contrib/interface/dad.ml | 2 | ||||
-rw-r--r-- | contrib/interface/debug_tac.ml4 | 2 | ||||
-rw-r--r-- | contrib/interface/name_to_ast.ml | 6 | ||||
-rw-r--r-- | contrib/interface/showproof.ml | 32 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 15 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 87 |
9 files changed, 82 insertions, 72 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 8f880a76..b6cc55f6 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -21,7 +21,7 @@ and ct_BINDING = CT_binding of ct_ID_OR_INT * ct_FORMULA and ct_BINDING_LIST = CT_binding_list of ct_BINDING list -and ct_BOOL = +and t_BOOL = CT_false | CT_true and ct_CASE = @@ -46,7 +46,7 @@ and ct_COMMAND = | CT_coerce_THEOREM_GOAL_to_COMMAND of ct_THEOREM_GOAL | CT_abort of ct_ID_OPT_OR_ALL | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST - | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_BINDING_LIST + | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA_OPT | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID | CT_addpath of ct_STRING * ct_ID_OPT | CT_arguments_scope of ct_ID * ct_ID_OPT_LIST @@ -684,7 +684,7 @@ and ct_TACTIC_COM = | CT_reflexivity | CT_rename of ct_ID * ct_ID | CT_repeat of ct_TACTIC_COM - | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT + | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_CLAUSE * ct_TACTIC_OPT | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE | CT_right of ct_SPEC_LIST diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 9e450068..dc27cf98 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -92,7 +92,7 @@ let rec def_const_in_term_rec vl x = | Case(_,x,t,a) -> def_const_in_term_rec vl x | Cast(x,_,t)-> def_const_in_term_rec vl t - | Const(c) -> def_const_in_term_rec vl (lookup_constant c vl).const_type + | Const(c) -> def_const_in_term_rec vl (Typeops.type_of_constant vl c) | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x) ;; let def_const_in_term_ x = diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 8fcdb5d9..730e055b 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -396,7 +396,7 @@ let inspect n = let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> - let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in + let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 578abc49..8096bc31 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -73,7 +73,7 @@ let rec map_subst (env :env) (subst:patvar_map) = function | CPatVar (_,(_,i)) -> let constr = List.assoc i subst in extern_constr false env constr - | x -> map_constr_expr_with_binders (map_subst env) (fun _ x -> x) subst x;; + | x -> map_constr_expr_with_binders (fun _ x -> x) (map_subst env) subst x;; let map_subst_tactic env subst = function | TacExtend (loc,("Rewrite" as x),[b;cbl]) -> diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index e1b8e712..890bb3ce 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -336,7 +336,7 @@ let debug_tac = function add_tactic "DebugTac" debug_tac;; *) -Refiner.add_tactic "OnThen" on_then;; +Tacinterp.add_tactic "OnThen" on_then;; let rec clean_path tac l = match tac, l with diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index b06ba199..9a503cfb 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -107,10 +107,10 @@ let convert_one_inductive sp tyi = let env = Global.env () in let envpar = push_rel_context params env in let sp = sp_of_global (IndRef (sp, tyi)) in - ((dummy_loc,basename sp), None, + (((dummy_loc,basename sp), convert_env(List.rev params), (extern_constr true envpar arity), - convert_constructors envpar cstrnames cstrtypes);; + convert_constructors envpar cstrnames cstrtypes), None);; (* This function converts a Mutual inductive definition to a Coqast.t. It is obtained directly from print_mutual in pretty.ml. However, all @@ -149,7 +149,7 @@ let make_definition_ast name c typ implicits = let constant_to_ast_list kn = let cb = Global.lookup_constant kn in let c = cb.const_body in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in let l = implicits_of_global (ConstRef kn) in (match c with None -> diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index ce2ee1e7..4bec7350 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -156,16 +156,16 @@ let seq_to_lnhyp sign sign' cl = let rule_is_complex r = match r with - Tactic (TacArg (Tacexp t),_) -> true - | Tactic (TacAtom (_,TacAuto _), _) -> true - | Tactic (TacAtom (_,TacSymmetry _), _) -> true + Nested (Tactic + ((TacArg (Tacexp _) + |TacAtom (_,(TacAuto _|TacSymmetry _))),_),_) -> true |_ -> false ;; let rule_to_ntactic r = let rt = (match r with - Tactic (t,_) -> t + Nested(Tactic (t,_),_) -> t | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h) | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in if rule_is_complex r @@ -234,17 +234,17 @@ let to_nproof sigma osign pf = (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof) spfl) in (match r with - Tactic (TacAtom (_, TacAuto _),_) -> - if spfl=[] - then - {t_info="to_prove"; - t_goal= {newhyp=[]; - t_concl=concl ntree; - t_full_concl=ntree.t_goal.t_full_concl; - t_full_env=ntree.t_goal.t_full_env}; - t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])} - else ntree - | _ -> ntree)) + Nested(Tactic (TacAtom (_, TacAuto _),_),_) -> + if spfl=[] + then + {t_info="to_prove"; + t_goal= {newhyp=[]; + t_concl=concl ntree; + t_full_concl=ntree.t_goal.t_full_concl; + t_full_env=ntree.t_goal.t_full_env}; + t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])} + else ntree + | _ -> ntree)) else {t_info="to_prove"; t_goal=(seq_to_lnhyp oldsign nsign cl); @@ -725,7 +725,7 @@ let rec nsortrec vl x = | Case(_,x,t,a) -> nsortrec vl x | Cast(x,_, t)-> nsortrec vl t - | Const c -> nsortrec vl (lookup_constant c vl).const_type + | Const c -> nsortrec vl (Typeops.type_of_constant vl c) | _ -> nsortrec vl (type_of vl Evd.empty x) ;; let nsort x = diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 064d20ab..fe227f99 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -112,19 +112,12 @@ and fCOMMAND = function fFORMULA x2; fINT_LIST x3; fNODE "abstraction" 3 -| CT_add_field(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) -> +| CT_add_field(x1, x2, x3, x4) -> fFORMULA x1; fFORMULA x2; fFORMULA x3; - fFORMULA x4; - fFORMULA x5; - fFORMULA x6; - fFORMULA x7; - fFORMULA x8; - fFORMULA x9; - fFORMULA x10; - fBINDING_LIST x11; - fNODE "add_field" 11 + fFORMULA_OPT x4; + fNODE "add_field" 4 | CT_add_natural_feature(x1, x2) -> fNATURAL_FEATURE x1; fID x2; @@ -1711,7 +1704,7 @@ and fTACTIC_COM = function | CT_replace_with(x1, x2,x3,x4) -> fFORMULA x1; fFORMULA x2; - fID_OPT x3; + fCLAUSE x3; fTACTIC_OPT x4; fNODE "replace_with" 4 | CT_rewrite_lr(x1, x2, x3) -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 024cb599..6c9e8239 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -497,6 +497,8 @@ let xlate_hyp_location = | (_, MetaId _),_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" + + let xlate_clause cls = let hyps_info = match cls.onhyps with @@ -724,7 +726,9 @@ and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) = | Reference (Ident (_,s)) -> ident_tac s | ConstrMayEval(ConstrTerm a) -> CT_formula_marker(xlate_formula a) - | TacFreshId s -> CT_fresh(ctf_STRING_OPT s) + | TacFreshId [] -> CT_fresh(ctf_STRING_OPT None) + | TacFreshId [ArgArg s] -> CT_fresh(ctf_STRING_OPT (Some s)) + | TacFreshId _ -> xlate_error "TODO: fresh with many args" | t -> xlate_error "TODO LATER: result other than tactic or constr" and xlate_red_tactic = @@ -937,6 +941,8 @@ and xlate_tac = CT_injection_eq (xlate_quantified_hypothesis_opt (out_gen (wit_opt rawwit_quant_hyp) idopt)) + | TacExtend (_,"injection_as", [idopt;ipat]) -> + xlate_error "TODO: injection as" | TacFix (idopt, n) -> CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list []) | TacMutualFix (id, n, fixtac_list) -> @@ -972,22 +978,36 @@ 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;id_opt;tac_opt]) -> + | TacExtend (_,"replace", [c1; c2;cl;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 cl = + (* J.F. : 18/08/2006 + Hack to coerce the "clause" argument of replace to a real clause + To be remove if we can reuse the clause grammar entrie defined in g_tactic + *) + let cl_as_clause = Extraargs.raw_in_arg_hyp_to_clause (out_gen Extraargs.rawwit_in_arg_hyp cl) in + let cl_as_xlate_arg = + {cl_as_clause with + Tacexpr.onhyps = + option_map + (fun l -> + List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l + ) + cl_as_clause.Tacexpr.onhyps + } + in + cl_as_xlate_arg + in + let cl = xlate_clause cl in let tac_opt = - match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with + match out_gen (Extraargs.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) + CT_replace_with (c1, c2,cl,tac_opt) | TacRewrite(b,cbindl,cl) -> let cl = xlate_clause cl and c = xlate_formula (fst cbindl) @@ -1077,12 +1097,12 @@ and xlate_tac = 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 + | 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 + | 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 @@ -1625,6 +1645,15 @@ let rec xlate_vernac = CT_solve (CT_int n, xlate_tactic tac, if b then CT_dotdot else CT_coerce_NONE_to_DOTDOT_OPT CT_none) + +(* MMode *) + + | (VernacDeclProof | VernacReturn | VernacProofInstr _) -> + anomaly "No MMode in CTcoq" + + +(* /MMode *) + | VernacFocus nopt -> CT_focus (xlate_int_opt nopt) | VernacUnfocus -> CT_unfocus |VernacExtend("Extraction", [f;l]) -> @@ -1645,27 +1674,14 @@ let rec xlate_vernac = CT_no_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst, List.map loc_qualid_to_ct_ID l2)) | VernacExtend("Field", - [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl;minusdiv]) -> + [fth;ainv;ainvl;div]) -> (match List.map (fun v -> xlate_formula(out_gen rawwit_constr v)) - [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl] + [fth;ainv;ainvl] with - [a1;aplus1;amult1;aone1;azero1;aopp1;aeq1;ainv1;fth1;ainvl1] -> - let bind = - match out_gen Field.rawwit_minus_div_arg minusdiv with - None, None -> - CT_binding_list[] - | Some m, None -> - CT_binding_list[ - CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m)] - | None, Some d -> - CT_binding_list[ - CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)] - | Some m, Some d -> - CT_binding_list[ - CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m); - CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)] in - CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1, - ainv1, fth1, ainvl1, bind) + [fth1;ainv1;ainvl1] -> + let adiv1 = + xlate_formula_opt (out_gen (wit_opt rawwit_constr) div) in + CT_add_field(fth1, ainv1, ainvl1, adiv1) |_ -> assert false) | VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) -> let orient = out_gen Extraargs.rawwit_orient o in @@ -1768,9 +1784,10 @@ let rec xlate_vernac = | VernacShow ShowExistentials -> CT_show_existentials | VernacShow ShowScript -> CT_show_script | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)" + | VernacShow(ShowThesis) -> xlate_error "TODO: VernacShow(ShowThesis _)" | VernacGo arg -> CT_go (xlate_locn arg) - | VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l) - | VernacShow ExplainTree l -> + | VernacShow (ExplainProof l) -> CT_explain_proof (nums_to_int_list l) + | VernacShow (ExplainTree l) -> CT_explain_prooftree (nums_to_int_list l) | VernacCheckGuard -> CT_guarded | VernacPrint p -> @@ -1874,7 +1891,7 @@ let rec xlate_vernac = build_record_field_list field_list) | VernacInductive (isind, lmi) -> let co_or_ind = if isind then "Inductive" else "CoInductive" in - let strip_mutind ((_,s), notopt, parameters, c, constructors) = + let strip_mutind (((_,s), parameters, c, constructors), notopt) = CT_ind_spec (xlate_ident s, xlate_binder_list parameters, xlate_formula c, build_constructors constructors, @@ -1883,7 +1900,7 @@ let rec xlate_vernac = (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi)) | VernacFixpoint ([],_) -> xlate_error "mutual recursive" | VernacFixpoint ((lm :: lmi),boxed) -> - let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) = + let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) = let (struct_arg,bl,arf,ardef) = (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) (* By the way, how could [bl = []] happen in V8 syntax ? *) @@ -1903,7 +1920,7 @@ let rec xlate_vernac = (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi)) | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive" | VernacCoFixpoint ((lm :: lmi),boxed) -> - let strip_mutcorec (fid, bl, arf, ardef) = + let strip_mutcorec ((fid, bl, arf, ardef), _ntn) = CT_cofix_rec (xlate_ident fid, xlate_binder_list bl, xlate_formula arf, xlate_formula ardef) in CT_cofix_decl |