summaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/ascent.mli6
-rw-r--r--contrib/interface/blast.ml2
-rw-r--r--contrib/interface/centaur.ml42
-rw-r--r--contrib/interface/dad.ml2
-rw-r--r--contrib/interface/debug_tac.ml42
-rw-r--r--contrib/interface/name_to_ast.ml6
-rw-r--r--contrib/interface/showproof.ml32
-rw-r--r--contrib/interface/vtp.ml15
-rw-r--r--contrib/interface/xlate.ml87
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 08:36:04 +0000