summaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/ascent.mli15
-rw-r--r--[-rwxr-xr-x]contrib/interface/blast.ml44
-rw-r--r--contrib/interface/blast.mli4
-rw-r--r--contrib/interface/centaur.ml453
-rw-r--r--contrib/interface/ctast.ml76
-rw-r--r--contrib/interface/dad.ml2
-rw-r--r--contrib/interface/debug_tac.ml4148
-rw-r--r--contrib/interface/debug_tac.mli2
-rwxr-xr-xcontrib/interface/line_parser.ml44
-rw-r--r--contrib/interface/name_to_ast.ml30
-rw-r--r--contrib/interface/name_to_ast.mli1
-rw-r--r--contrib/interface/parse.ml79
-rw-r--r--contrib/interface/pbp.ml12
-rw-r--r--contrib/interface/pbp.mli4
-rw-r--r--contrib/interface/showproof.ml130
-rwxr-xr-xcontrib/interface/showproof.mli2
-rw-r--r--contrib/interface/showproof_ct.ml9
-rw-r--r--contrib/interface/translate.ml88
-rw-r--r--contrib/interface/vernacrc2
-rw-r--r--contrib/interface/vtp.ml25
-rw-r--r--contrib/interface/xlate.ml376
21 files changed, 317 insertions, 789 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 61d0d5a3..fb71288a 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -119,11 +119,13 @@ and ct_COMMAND =
| CT_print_about of ct_ID
| CT_print_all
| CT_print_classes
+ | CT_print_ltac of ct_ID
| CT_print_coercions
| CT_print_grammar of ct_GRAMMAR
| CT_print_graph
| CT_print_hint of ct_ID_OPT
| CT_print_hintdb of ct_ID_OR_STAR
+ | CT_print_rewrite_hintdb of ct_ID
| CT_print_id of ct_ID
| CT_print_implicit of ct_ID
| CT_print_loadpath
@@ -135,6 +137,7 @@ and ct_COMMAND =
| CT_print_opaqueid of ct_ID
| CT_print_path of ct_ID * ct_ID
| CT_print_proof of ct_ID
+ | CT_print_setoids
| CT_print_scope of ct_ID
| CT_print_scopes
| CT_print_section of ct_ID
@@ -465,8 +468,8 @@ and ct_MODULE_EXPR =
| CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR
and ct_MODULE_TYPE =
CT_coerce_ID_to_MODULE_TYPE of ct_ID
- | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID * ct_FORMULA
- | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * ct_ID
+ | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID_LIST * ct_FORMULA
+ | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID
and ct_MODULE_TYPE_CHECK =
CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
| CT_only_check of ct_MODULE_TYPE
@@ -530,6 +533,7 @@ and ct_RED_COM =
| CT_lazy of ct_CONVERSION_FLAG_LIST * ct_CONV_SET
| CT_pattern of ct_PATTERN_NE_LIST
| CT_red
+ | CT_cbvvm
| CT_simpl of ct_PATTERN_OPT
| CT_unfold of ct_UNFOLD_NE_LIST
and ct_RETURN_INFO =
@@ -637,6 +641,7 @@ and ct_TACTIC_COM =
| CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING
| CT_elim_type of ct_FORMULA
| CT_exact of ct_FORMULA
+ | CT_exact_no_check of ct_FORMULA
| CT_exists of ct_SPEC_LIST
| CT_fail of ct_ID_OR_INT * ct_STRING_OPT
| CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
@@ -665,8 +670,8 @@ 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_INTRO_PATT_OPT
- | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT
+ | CT_new_destruct of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
+ | CT_new_induction of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
| CT_omega
| CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
| CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
@@ -679,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_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT
| CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
| CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
| CT_right of ct_SPEC_LIST
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index d5236a7a..21f977f1 100755..100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -1,13 +1,11 @@
(* Une tactique qui tente de démontrer toute seule le but courant,
interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A)
*)
-open Ctast;;
open Termops;;
open Nameops;;
open Auto;;
open Clenv;;
open Command;;
-open Ctast;;
open Declarations;;
open Declare;;
open Eauto;;
@@ -38,7 +36,6 @@ open Typing;;
open Util;;
open Vernacentries;;
open Vernacinterp;;
-open Evar_refiner;;
let parse_com = Pcoq.parse_string Pcoq.Constr.constr;;
@@ -94,7 +91,7 @@ let rec def_const_in_term_rec vl x =
def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
| Case(_,x,t,a)
-> def_const_in_term_rec vl x
- | Cast(x,t)-> def_const_in_term_rec vl t
+ | Cast(x,_,t)-> def_const_in_term_rec vl t
| Const(c) -> def_const_in_term_rec vl (lookup_constant c vl).const_type
| _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
;;
@@ -113,7 +110,7 @@ let rec print_info_script sigma osign pf =
match pf.ref with
| None -> (mt ())
| Some(r,spfl) ->
- pr_rule r ++
+ Tactic_printer.pr_rule r ++
match spfl with
| [] ->
(str " " ++ fnl())
@@ -152,8 +149,7 @@ let pp_string x =
(***************************************************************************)
let unify_e_resolve (c,clenv) gls =
- let (wc,kONT) = startWalk gls in
- let clenv' = connect_clenv wc clenv in
+ let clenv' = connect_clenv gls clenv in
let _ = clenv_unique_resolver false clenv' gls in
vernac_e_resolve_constr c gls
@@ -179,7 +175,7 @@ and e_my_find_search db_list local_db hdc concl =
list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
in
let tac_of_hint =
- fun ({pri=b; pat = p; code=t} as patac) ->
+ fun ({pri=b; pat = p; code=t} as _patac) ->
(b,
let tac =
match t with
@@ -189,7 +185,7 @@ and e_my_find_search db_list local_db hdc concl =
| Res_pf_THEN_trivial_fail (term,cl) ->
tclTHEN (unify_e_resolve (term,cl))
(e_trivial_fail_db db_list local_db)
- | Unfold_nth c -> unfold_constr c
+ | Unfold_nth c -> unfold_in_concl [[],c]
| Extern tacast -> Auto.conclPattern concl
(out_some p) tacast
in
@@ -341,7 +337,7 @@ let e_breadth_search debug n db_list local_db gl =
with Not_found -> error "EAuto: breadth first search failed"
let e_search_auto debug (n,p) db_list gl =
- let local_db = make_local_hint_db gl in
+ let local_db = make_local_hint_db [] gl in
if n = 0 then
e_depth_search debug p db_list local_db gl
else
@@ -351,17 +347,17 @@ let eauto debug np dbnames =
let db_list =
List.map
(fun x ->
- try Stringmap.find x !searchtable
+ try searchtable_map x
with Not_found -> error ("EAuto: "^x^": No such Hint database"))
("core"::dbnames)
in
tclTRY (e_search_auto debug np db_list)
let full_eauto debug n gl =
- let dbnames = stringmap_dom !searchtable in
+ let dbnames = current_db_names () in
let dbnames = list_subtract dbnames ["v62"] in
- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
- let local_db = make_local_hint_db gl in
+ let db_list = List.map searchtable_map dbnames in
+ let _local_db = make_local_hint_db [] gl in
tclTRY (e_search_auto debug n db_list) gl
let my_full_eauto n gl = full_eauto false (n,0) gl
@@ -369,8 +365,6 @@ let my_full_eauto n gl = full_eauto false (n,0) gl
(**********************************************************************
copié de tactics/auto.ml on a juste modifié search_gen
*)
-let searchtable_map name =
- Stringmap.find name !searchtable
(* local_db is a Hint database containing the hypotheses of current goal *)
(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
@@ -397,7 +391,7 @@ and my_find_search db_list local_db hdc concl =
(local_db::db_list)
in
List.map
- (fun ({pri=b; pat=p; code=t} as patac) ->
+ (fun ({pri=b; pat=p; code=t} as _patac) ->
(b,
match t with
| Res_pf (term,cl) -> unify_resolve (term,cl)
@@ -407,7 +401,7 @@ and my_find_search db_list local_db hdc concl =
tclTHEN
(unify_resolve (term,cl))
(trivial_fail_db db_list local_db)
- | Unfold_nth c -> unfold_constr c
+ | Unfold_nth c -> unfold_in_concl [[],c]
| Extern tacast ->
conclPattern concl (out_some p) tacast))
tacl
@@ -476,7 +470,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
try
[make_apply_entry (pf_env g') (project g')
(true,false)
- hid (mkVar hid,body_of_type htyp)]
+ (mkVar hid,body_of_type htyp)]
with Failure _ -> []
in
(free_try
@@ -499,11 +493,11 @@ let search = search_gen 0
let default_search_depth = ref 5
let full_auto n gl =
- let dbnames = stringmap_dom !searchtable in
+ let dbnames = current_db_names () in
let dbnames = list_subtract dbnames ["v62"] in
- let db_list = List.map (fun x -> searchtable_map x) dbnames in
+ let db_list = List.map searchtable_map dbnames in
let hyps = pf_hyps gl in
- tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+ tclTRY (search n db_list (make_local_hint_db [] gl) hyps) gl
let default_full_auto gl = full_auto !default_search_depth gl
(************************************************************************)
@@ -568,7 +562,7 @@ let blast gls =
open_subgoals = 1;
goal = g;
ref = None } in
- try (let (sgl,v) as res = !blast_tactic gls in
+ try (let (sgl,v) as _res = !blast_tactic gls in
let {it=lg} = sgl in
if lg = []
then (let pf = v (List.map leaf (sig_it sgl)) in
@@ -590,7 +584,7 @@ let blast gls =
;;
let blast_tac display_function = function
- | (n::_) as l ->
+ | (n::_) as _l ->
(function g ->
let exp_ast = (blast g) in
(display_function exp_ast;
@@ -599,7 +593,7 @@ let blast_tac display_function = function
let blast_tac_txt =
blast_tac
- (function x -> msgnl(Pptactic.pr_glob_tactic (Tacinterp.glob_tactic x)));;
+ (function x -> msgnl(Pptactic.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
(* Obsolète ?
overwriting_add_tactic "Blast1" blast_tac_txt;;
diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli
index 21c29bc9..f6701943 100644
--- a/contrib/interface/blast.mli
+++ b/contrib/interface/blast.mli
@@ -1,5 +1,3 @@
val blast_tac : (Tacexpr.raw_tactic_expr -> 'a) ->
- int list ->
- Proof_type.goal Tacmach.sigma ->
- Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
+ int list -> Proof_type.tactic
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 7bf12f3b..8fcdb5d9 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -4,7 +4,6 @@
open Names;;
open Nameops;;
open Util;;
-open Ast;;
open Term;;
open Pp;;
open Libnames;;
@@ -13,7 +12,6 @@ open Library;;
open Vernacinterp;;
open Evd;;
open Proof_trees;;
-open Termast;;
open Tacmach;;
open Pfedit;;
open Proof_type;;
@@ -28,7 +26,6 @@ open Vernacinterp;;
open Vernac;;
open Command;;
open Protectedtoplevel;;
-open Coqast;;
open Line_oriented_parser;;
open Xlate;;
open Vtp;;
@@ -283,15 +280,12 @@ let print_check judg =
let value_ct_ast =
(try translate_constr false (Global.env()) value
with UserError(f,str) ->
- raise(UserError(f,
- Ast.print_ast
- (ast_of_constr true (Global.env()) value) ++
+ raise(UserError(f,Printer.pr_lconstr value ++
fnl () ++ str ))) in
let type_ct_ast =
(try translate_constr false (Global.env()) typ
with UserError(f,str) ->
- raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env())
- value) ++ fnl() ++ str))) in
+ raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
((ctf_SearchResults !global_request_id),
(Some (P_pl
(CT_premises_list
@@ -315,18 +309,6 @@ and ntyp = nf_betaiota typ in
-(* The following function is copied from globpr in env/printer.ml *)
-let globcv x =
- match x with
- | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
- convert_qualid
- (Nametab.shortest_qualid_of_global Idset.empty (IndRef(sp,tyi)))
- | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
- convert_qualid
- (Nametab.shortest_qualid_of_global Idset.empty
- (ConstructRef ((sp, tyi), i)))
- | _ -> failwith "globcv : unexpected value";;
-
let pbp_tac_pcoq =
pbp_tac (function (x:raw_tactic_expr) ->
output_results
@@ -360,12 +342,13 @@ let debug_tac2_pcoq tac =
let the_ast = ref tac in
let the_path = ref ([] : int list) in
try
- let result = report_error tac the_goal the_ast the_path [] g in
+ let _result = report_error tac the_goal the_ast the_path [] g in
(errorlabstrm "DEBUG TACTIC"
- (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
+ (str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++
fnl () ++ str "the tactic is" ++ fnl () ++
- Pptactic.pr_glob_tactic tac);
- result)
+ Pptactic.pr_glob_tactic (Global.env()) tac) (*
+Caution, this is in the middle of what looks like dead code. ;
+ result *))
with
e ->
match !the_goal with
@@ -413,11 +396,11 @@ 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 kn in
+ let {const_type=typ} = Global.lookup_constant (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))
- (Pretyping.understand Evd.empty (Global.env())
+ (Pretyping.Default.understand Evd.empty (Global.env())
(RRef(dummy_loc, IndRef(kn,0))))
| _ -> failwith ("unexpected value 1 for "^
(string_of_id (basename (fst oname)))))
@@ -571,11 +554,11 @@ let pcoq_search s l =
(* Check sequentially whether the pattern is one of the premises *)
let rec hyp_pattern_filter pat name a c =
- let c1 = strip_outer_cast c in
+ let _c1 = strip_outer_cast c in
match kind_of_term c with
| Prod(_, hyp, c2) ->
(try
-(* let _ = msgnl ((str "WHOLE ") ++ (Printer.prterm c)) in
+(* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *)
if Matching.is_matching pat hyp then
(msgnl (str "ok"); true)
@@ -616,7 +599,7 @@ let pcoq_show_goal = function
| Some n -> show_nth n
| None ->
if !pcoq_started = Some true (* = debug *) then
- msg (Pfedit.pr_open_subgoals ())
+ msg (Printer.pr_open_subgoals ())
else errorlabstrm "show_goal"
(str "Show must be followed by an integer in Centaur mode");;
@@ -632,17 +615,17 @@ let pcoq_hook = {
}
-TACTIC EXTEND Pbp
-| [ "Pbp" ident_opt(idopt) natural_list(nl) ] ->
+TACTIC EXTEND pbp
+| [ "pbp" ident_opt(idopt) natural_list(nl) ] ->
[ if_pcoq pbp_tac_pcoq idopt nl ]
END
-TACTIC EXTEND CtDebugTac
-| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
+TACTIC EXTEND ct_debugtac
+| [ "debugtac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
END
-TACTIC EXTEND CtDebugTac2
-| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
+TACTIC EXTEND ct_debugtac2
+| [ "debugtac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
END
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
deleted file mode 100644
index 67279bb8..00000000
--- a/contrib/interface/ctast.ml
+++ /dev/null
@@ -1,76 +0,0 @@
-(* A copy of pre V7 ast *)
-
-open Names
-open Libnames
-
-type loc = Util.loc
-
-type t =
- | Node of loc * string * t list
- | Nvar of loc * string
- | Slam of loc * string option * t
- | Num of loc * int
- | Id of loc * string
- | Str of loc * string
- | Path of loc * string list
- | Dynamic of loc * Dyn.t
-
-let section_path sl =
- match List.rev sl with
- | s::pa ->
- Libnames.encode_kn
- (make_dirpath (List.map id_of_string pa))
- (id_of_string s)
- | [] -> invalid_arg "section_path"
-
-let is_meta s = String.length s > 0 && s.[0] == '$'
-
-let purge_str s =
- if String.length s == 0 || s.[0] <> '$' then s
- else String.sub s 1 (String.length s - 1)
-
-let rec ct_to_ast = function
- | Node (loc,a,b) -> Coqast.Node (loc,a,List.map ct_to_ast b)
- | Nvar (loc,a) ->
- if is_meta a then Coqast.Nmeta (loc,purge_str a)
- else Coqast.Nvar (loc,id_of_string a)
- | Slam (loc,Some a,b) ->
- if is_meta a then Coqast.Smetalam (loc,purge_str a,ct_to_ast b)
- else Coqast.Slam (loc,Some (id_of_string a),ct_to_ast b)
- | Slam (loc,None,b) -> Coqast.Slam (loc,None,ct_to_ast b)
- | Num (loc,a) -> Coqast.Num (loc,a)
- | Id (loc,a) -> Coqast.Id (loc,a)
- | Str (loc,a) -> Coqast.Str (loc,a)
- | Path (loc,sl) -> Coqast.Path (loc,section_path sl)
- | Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
-
-let rec ast_to_ct = function x -> failwith "ast_to_ct: not TODO?"
-(*
- | Coqast.Node (loc,a,b) -> Node (loc,a,List.map ast_to_ct b)
- | Coqast.Nvar (loc,a) -> Nvar (loc,string_of_id a)
- | Coqast.Nmeta (loc,a) -> Nvar (loc,"$"^a)
- | Coqast.Slam (loc,Some a,b) ->
- Slam (loc,Some (string_of_id a),ast_to_ct b)
- | Coqast.Slam (loc,None,b) -> Slam (loc,None,ast_to_ct b)
- | Coqast.Smetalam (loc,a,b) -> Slam (loc,Some ("$"^a),ast_to_ct b)
- | Coqast.Num (loc,a) -> Num (loc,a)
- | Coqast.Id (loc,a) -> Id (loc,a)
- | Coqast.Str (loc,a) -> Str (loc,a)
- | Coqast.Path (loc,a) ->
- let (sl,bn) = Libnames.decode_kn a in
- Path(loc, (List.map string_of_id
- (List.rev (repr_dirpath sl))) @ [string_of_id bn])
- | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
-*)
-
-let loc = function
- | Node (loc,_,_) -> loc
- | Nvar (loc,_) -> loc
- | Slam (loc,_,_) -> loc
- | Num (loc,_) -> loc
- | Id (loc,_) -> loc
- | Str (loc,_) -> loc
- | Path (loc,_) -> loc
- | Dynamic (loc,_) -> loc
-
-let str s = Str(Util.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index ec989296..578abc49 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -251,7 +251,7 @@ let rec sort_list = function
let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));;
let mk_rewrite lr ast =
let b = in_gen rawwit_bool lr in
- let cb = in_gen rawwit_constr_with_bindings ((*Ctast.ct_to_ast*) ast,NoBindings) in
+ let cb = in_gen rawwit_constr_with_bindings (ast,NoBindings) in
TacExtend (zz,"Rewrite",[b;cb])
open Vernacexpr
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index bf596b28..56abfb82 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -1,7 +1,5 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-open Ast;;
-open Coqast;;
open Tacmach;;
open Tacticals;;
open Proof_trees;;
@@ -12,6 +10,8 @@ open Proof_type;;
open Tacexpr;;
open Genarg;;
+let pr_glob_tactic = Pptactic.pr_glob_tactic (Global.env())
+
(* Compacting and uncompacting proof commands *)
type report_tree =
@@ -72,11 +72,6 @@ let check_subgoals_count2
Recursive_fail (List.hd !new_report_holder)));
result;;
-(*
-let traceable = function
- Node(_, "TACTICLIST", a::b::tl) -> true
- | _ -> false;;
-*)
let traceable = function
| TacThen _ | TacThens _ -> true
| _ -> false;;
@@ -116,25 +111,6 @@ let count_subgoals2
result;;
let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
-(*
- Node(_, "TACTICLIST", [a;Node(_, "TACLIST", l)]) ->
- (fun report_holder -> checked_thens report_holder a l)
- | Node(_, "TACTICLIST", a::((Node(_, "TACLIST", l))as b)::c::tl) ->
- local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
- | Node(_, "TACTICLIST", [a;b]) ->
- (fun report_holder -> checked_then report_holder a b)
- | Node(_, "TACTICLIST", a::b::c::tl) ->
- local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
- | ast ->
- (fun report_holder g ->
- try
- let (gls, _) as result = Tacinterp.interp ast g in
- report_holder := (Report_node(true, List.length (sig_it gls), []))
- ::!report_holder;
- result
- with e -> (report_holder := (Failed 1)::!report_holder;
- tclIDTAC g))
-*)
TacThens (a,l) ->
(fun report_holder -> checked_thens report_holder a l)
| TacThen (a,b) ->
@@ -263,9 +239,14 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti
by the list of integers given as extra arguments.
*)
+let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
+let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level
+let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level
+
+
let on_then = function [t1;t2;l] ->
- let t1 = out_gen wit_tactic t1 in
- let t2 = out_gen wit_tactic t2 in
+ let t1 = out_gen wit_main_tactic t1 in
+ let t2 = out_gen wit_main_tactic t2 in
let l = out_gen (wit_list0 wit_int) l in
tclTHEN_i (Tacinterp.eval_tactic t1)
(fun i ->
@@ -276,78 +257,18 @@ let on_then = function [t1;t2;l] ->
| _ -> anomaly "bad arguments for on_then";;
let mkOnThen t1 t2 selected_indices =
- let a = in_gen rawwit_tactic t1 in
- let b = in_gen rawwit_tactic t2 in
+ let a = in_gen rawwit_main_tactic t1 in
+ let b = in_gen rawwit_main_tactic t2 in
let l = in_gen (wit_list0 rawwit_int) selected_indices in
TacAtom (dummy_loc, TacExtend (dummy_loc, "OnThen", [a;b;l]));;
(* Analyzing error reports *)
-(*
-let rec select_success n = function
- [] -> []
- | Report_node(true,_,_)::tl -> (Num((0,0),n))::select_success (n+1) tl
- | _::tl -> select_success (n+1) tl;;
-*)
let rec select_success n = function
[] -> []
| Report_node(true,_,_)::tl -> n::select_success (n+1) tl
| _::tl -> select_success (n+1) tl;;
-(*
-let rec expand_tactic = function
- Node(loc1, "TACTICLIST", [a;Node(loc2,"TACLIST", l)]) ->
- Node(loc1, "TACTICLIST",
- [expand_tactic a;
- Node(loc2, "TACLIST", List.map expand_tactic l)])
- | Node(loc1, "TACTICLIST", a::((Node(loc2, "TACLIST", l))as b)::c::tl) ->
- expand_tactic (Node(loc1, "TACTICLIST",
- (Node(loc1, "TACTICLIST", [a;b]))::c::tl))
- | Node(loc1, "TACTICLIST", [a;b]) ->
- Node(loc1, "TACTICLIST",[expand_tactic a;expand_tactic b])
- | Node(loc1, "TACTICLIST", a::b::c::tl) ->
- expand_tactic (Node(loc1, "TACTICLIST",
- (Node(loc1, "TACTICLIST", [a;b]))::c::tl))
- | any -> any;;
-*)
-(* Useless: already in binary form...
-let rec expand_tactic = function
- TacThens (a,l) -> TacThens (expand_tactic a, List.map expand_tactic l)
- | TacThen (a,b) -> TacThen (expand_tactic a, expand_tactic b)
- | any -> any;;
-*)
-
-(*
-let rec reconstruct_success_tac ast =
- match ast with
- Node(_, "TACTICLIST", [a;Node(_,"TACLIST",l)]) ->
- (function
- Report_node(true, n, l) -> ast
- | Report_node(false, n, rl) ->
- ope("TACTICLIST",[a;ope("TACLIST",
- List.map2 reconstruct_success_tac l rl)])
- | Failed n -> ope("Idtac",[])
- | Tree_fail r -> reconstruct_success_tac a r
- | Mismatch (n,p) -> a)
- | Node(_, "TACTICLIST", [a;b]) ->
- (function
- Report_node(true, n, l) -> ast
- | Report_node(false, n, rl) ->
- let selected_indices = select_success 1 rl in
- ope("OnThen", a::b::selected_indices)
- | Failed n -> ope("Idtac",[])
- | Tree_fail r -> reconstruct_success_tac a r
- | _ -> error "this error case should not happen in a THEN tactic")
- | _ ->
- (function
- Report_node(true, n, l) -> ast
- | Failed n -> ope("Idtac",[])
- | _ ->
- errorlabstrm
- "this error case should not happen on an unknown tactic"
- (str "error in reconstruction with " ++ fnl () ++
- (gentacpr ast)));;
-*)
let rec reconstruct_success_tac (tac:glob_tactic_expr) =
match tac with
TacThens (a,l) ->
@@ -355,7 +276,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
Report_node(true, n, l) -> tac
| Report_node(false, n, rl) ->
TacThens (a,List.map2 reconstruct_success_tac l rl)
- | Failed n -> TacId ""
+ | Failed n -> TacId []
| Tree_fail r -> reconstruct_success_tac a r
| Mismatch (n,p) -> a)
| TacThen (a,b) ->
@@ -364,16 +285,16 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
| Report_node(false, n, rl) ->
let selected_indices = select_success 1 rl in
TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen",
- [in_gen globwit_tactic a;
- in_gen globwit_tactic b;
+ [in_gen globwit_main_tactic a;
+ in_gen globwit_main_tactic b;
in_gen (wit_list0 globwit_int) selected_indices]))
- | Failed n -> TacId ""
+ | Failed n -> TacId []
| Tree_fail r -> reconstruct_success_tac a r
| _ -> error "this error case should not happen in a THEN tactic")
| _ ->
(function
Report_node(true, n, l) -> tac
- | Failed n -> TacId ""
+ | Failed n -> TacId []
| _ ->
errorlabstrm
"this error case should not happen on an unknown tactic"
@@ -391,21 +312,6 @@ let rec path_to_first_error = function
p::(path_to_first_error t)
| _ -> [];;
-(*
-let rec flatten_then_list tail = function
- | Node(_, "TACTICLIST", [a;b]) ->
- flatten_then_list ((flatten_then b)::tail) a
- | ast -> ast::tail
-and flatten_then = function
- Node(_, "TACTICLIST", [a;b]) ->
- ope("TACTICLIST", flatten_then_list [flatten_then b] a)
- | Node(_, "TACLIST", l) ->
- ope("TACLIST", List.map flatten_then l)
- | Node(_, "OnThen", t1::t2::l) ->
- ope("OnThen", (flatten_then t1)::(flatten_then t2)::l)
- | ast -> ast;;
-*)
-
let debug_tac = function
[(Tacexp ast)] ->
(fun g ->
@@ -430,26 +336,8 @@ let debug_tac = function
add_tactic "DebugTac" debug_tac;;
*)
-(*
-hide_tactic "OnThen" on_then;;
-*)
Refiner.add_tactic "OnThen" on_then;;
-(*
-let rec clean_path p ast l =
- match ast, l with
- Node(_, "TACTICLIST", ([_;_] as tacs)), fst::tl ->
- fst::(clean_path 0 (List.nth tacs (fst - 1)) tl)
- | Node(_, "TACTICLIST", tacs), 2::tl ->
- let rank = (List.length tacs) - p in
- rank::(clean_path 0 (List.nth tacs (rank - 1)) tl)
- | Node(_, "TACTICLIST", tacs), 1::tl ->
- clean_path (p+1) ast tl
- | Node(_, "TACLIST", tacs), fst::tl ->
- fst::(clean_path 0 (List.nth tacs (fst - 1)) tl)
- | _, [] -> []
- | _, _ -> failwith "this case should not happen in clean_path";;
-*)
let rec clean_path tac l =
match tac, l with
| TacThen (a,b), fst::tl ->
@@ -554,8 +442,8 @@ let descr_first_error tac =
(msgnl (str "Execution of this tactic raised message " ++ fnl () ++
fnl () ++ Cerrors.explain_exn e ++ fnl () ++
fnl () ++ str "on goal" ++ fnl () ++
- pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
- str "faulty tactic is" ++ fnl () ++ fnl () ++
+ Printer.pr_goal (sig_it (strip_some !the_goal)) ++
+ fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++
pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ());
tclIDTAC g))
diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli
index ded714b6..da4bbaa0 100644
--- a/contrib/interface/debug_tac.mli
+++ b/contrib/interface/debug_tac.mli
@@ -1,6 +1,6 @@
val report_error : Tacexpr.glob_tactic_expr ->
- Proof_type.goal Proof_type.sigma option ref ->
+ Proof_type.goal Evd.sigma option ref ->
Tacexpr.glob_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;;
val clean_path : Tacexpr.glob_tactic_expr -> int list -> int list;;
diff --git a/contrib/interface/line_parser.ml4 b/contrib/interface/line_parser.ml4
index b5669351..0b13a092 100755
--- a/contrib/interface/line_parser.ml4
+++ b/contrib/interface/line_parser.ml4
@@ -84,7 +84,7 @@ let rec string len = parser
spaces and tabulations are ignored, identifiers, integers,
strings, opening and closing square brackets. Lexical errors are
ignored ! *)
-let rec next_token = parser count
+let rec next_token = parser _count
[< '' ' | '\t'; tok = next_token >] -> tok
| [< ''_' | 'a'..'z' | 'A'..'Z' as c;i = (ident (add_in_buff 0 c))>] -> i
| [< ''0'..'9' as c ; i = (parse_int (get_digit c))>] -> i
@@ -96,7 +96,7 @@ let rec next_token = parser count
(* A very simple lexical analyser to recognize a integer value behind
blank characters *)
-let rec next_int = parser count
+let rec next_int = parser _count
[< '' ' | '\t'; v = next_int >] -> v
| [< ''0'..'9' as c; i = (parse_int (get_digit c))>] ->
(match i with
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index eaff0968..b06ba199 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -2,9 +2,6 @@ open Sign;;
open Classops;;
open Names;;
open Nameops
-open Coqast;;
-open Ast;;
-open Termast;;
open Term;;
open Impargs;;
open Reduction;;
@@ -90,13 +87,6 @@ let implicit_args_to_ast_list sp mipv =
[] -> []
| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
-let convert_qualid qid =
- let d, id = Libnames.repr_qualid qid in
- match repr_dirpath d with
- [] -> nvar id
- | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
- [nvar id] d);;
-
(* This function converts constructors for an inductive definition to a
Coqast.t. It is obtained directly from print_constructors in pretty.ml *)
@@ -142,16 +132,6 @@ let implicits_to_ast_list implicits =
| None -> []
| Some s -> [VernacComments [CommentString s]];;
-(*
-let make_variable_ast name typ implicits =
- (ope("VARIABLE",
- [string "VARIABLE";
- ope("BINDERLIST",
- [ope("BINDER",
- [(constr_to_ast (body_of_type typ));
- nvar name])])]))::(implicits_to_ast_list implicits)
- ;;
-*)
let make_variable_ast name typ implicits =
(VernacAssumption
((Local,Definitional),
@@ -160,7 +140,7 @@ let make_variable_ast name typ implicits =
let make_definition_ast name c typ implicits =
- VernacDefinition ((Global,Definition), (dummy_loc,name), DefineBody ([], None,
+ VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
(constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
@@ -173,9 +153,9 @@ let constant_to_ast_list kn =
let l = implicits_of_global (ConstRef kn) in
(match c with
None ->
- make_variable_ast (id_of_label (label kn)) typ l
+ make_variable_ast (id_of_label (con_label kn)) typ l
| Some c1 ->
- make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)
+ make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
let variable_to_ast_list sp =
let (id, c, v) = get_variable sp in
@@ -198,7 +178,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
let tag = object_tag lobj in
match tag with
| "VARIABLE" -> variable_to_ast_list (basename sp)
- | "CONSTANT" -> constant_to_ast_list kn
+ | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn)
| "INDUCTIVE" -> inductive_to_ast_list kn
| s ->
errorlabstrm
@@ -240,7 +220,7 @@ let name_to_ast ref =
| Some c1 -> make_definition_ast name c1 typ [])
with Not_found ->
try
- let sp = Nametab.locate_syntactic_definition qid in
+ let _sp = Nametab.locate_syntactic_definition qid in
errorlabstrm "print"
(str "printing of syntax definitions not implemented")
with Not_found ->
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 0eca0a1e..b8c2d7dc 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1,2 +1 @@
val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
-val convert_qualid : Libnames.qualid -> Coqast.t;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 3f0b2d2e..4d4df59f 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -48,55 +48,8 @@ let ctf_FileErrorMessage reqid pps =
int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++
fnl ();;
-(*
-(*In the code for CoqV6.2, the require_module call is encapsulated in
- a function "without_mes_ambig". Here I have supposed that this
- function has no effect on parsing *)
-let try_require_module import specif names =
- try Library.require_module
- (if specif = "UNSPECIFIED" then None
- else Some (specif = "SPECIFICATION"))
- (List.map
- (fun name ->
- (dummy_loc,Libnames.make_short_qualid (Names.id_of_string name)))
- names)
- (import = "IMPORT")
- with
- | e -> msgnl (str "Reinterning of " ++ prlist str names ++ str " failed");;
-*)
-(*
-let try_require_module_from_file import specif name fname =
- try Library.require_module_from_file (if specif = "UNSPECIFIED" then None
- else Some (specif = "SPECIFICATION")) (Some (Names.id_of_string name)) fname (import = "IMPORT")
- with
- | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
-*)
-(*
-let execute_when_necessary ast =
- (match ast with
- | Node (_, "GRAMMAR", ((Nvar (_, s)) :: ((Node (_, "ASTLIST", al)) :: []))) ->
- Metasyntax.add_grammar_obj s (List.map Ctast.ct_to_ast al)
-(* Obsolete
- | Node (_, "TOKEN", ((Str (_, s)) :: [])) -> Metasyntax.add_token_obj s
-*)
- | Node (_, "Require",
- ((Str (_, import)) ::
- ((Str (_, specif)) :: l))) ->
- let mnames = List.map (function
- | (Nvar (_, m)) -> m
- | _ -> error "parse_string_action : bad require expression") l in
- try_require_module import specif mnames
- | Node (_, "RequireFrom",
- ((Str (_, import)) ::
- ((Str (_, specif)) ::
- ((Nvar (_, mname)) :: ((Str (_, file_name)) :: []))))) ->
- try_require_module_from_file import specif mname file_name
- | _ -> ()); ast;;
-*)
-
let execute_when_necessary v =
(match v with
- | VernacGrammar _ -> Vernacentries.interp v
| VernacOpenCloseScope sc -> Vernacentries.interp v
| VernacRequire (_,_,l) ->
(try
@@ -202,12 +155,6 @@ let parse_command_list reqid stream string_list =
discard_to_dot stream;
msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++
int (Stream.count stream));
-(*
- Some( Node(l, "PARSING_ERROR",
- List.map Ctast.str
- (get_substring_list string_list this_pos
- (Stream.count stream))))
-*)
ParseError ("PARSING_ERROR",
get_substring_list string_list this_pos
(Stream.count stream))
@@ -216,27 +163,14 @@ let parse_command_list reqid stream string_list =
| e->
begin
discard_to_dot stream;
-(*
- Some(Node((0,0), "PARSING_ERROR2",
- List.map Ctast.str
- (get_substring_list string_list this_pos
- (Stream.count stream))))
-*)
ParseError ("PARSING_ERROR2",
get_substring_list string_list this_pos (Stream.count stream))
end in
match first_ast with
| ParseOK (Some (loc,ast)) ->
- let ast0 = (execute_when_necessary ast) in
+ let _ast0 = (execute_when_necessary ast) in
(try xlate_vernac ast
with e ->
-(*
- xlate_vernac
- (Node((0,0), "PARSING_ERROR2",
- List.map Ctast.str
- (get_substring_list string_list this_pos
- (Stream.count stream)))))::parse_whole_stream()
-*)
make_parse_error_item "PARSING_ERROR2"
(get_substring_list string_list this_pos
(Stream.count stream)))::parse_whole_stream()
@@ -311,7 +245,7 @@ let parse_file_action reqid file_name =
get the text when a syntax error occurs *)
let file_chan_err = open_in file_name in
let stream = Stream.of_channel file_chan in
- let stream_err = Stream.of_channel file_chan_err in
+ let _stream_err = Stream.of_channel file_chan_err in
let rec discard_to_dot () =
try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in
@@ -345,7 +279,7 @@ let parse_file_action reqid file_name =
with
| ParseOK (Some (_,ast)) ->
- let ast0=(execute_when_necessary ast) in
+ let _ast0=(execute_when_necessary ast) in
let term =
(try xlate_vernac ast
with e ->
@@ -395,13 +329,13 @@ let add_path_action reqid string_arg =
let print_version_action () =
msgnl (mt ());
- msgnl (str "$Id: parse.ml,v 1.22 2004/04/21 08:36:58 barras Exp $");;
+ msgnl (str "$Id: parse.ml 7844 2006-01-11 16:36:14Z bertot $");;
let load_syntax_action reqid module_name =
msg (str "loading " ++ str module_name ++ str "... ");
try
(let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
- read_library (dummy_loc,qid);
+ require_library [dummy_loc,qid] None;
msg (str "opening... ");
Declaremods.import_module false (Nametab.locate_module qid);
msgnl (str "done" ++ fnl ());
@@ -456,7 +390,6 @@ Libobject.relax true;
coqdir [ "contrib"; "interface"; "vernacrc"] in
try
(Gramext.warning_verbose := false;
- Esyntax.warning_verbose := false;
coqparser_loop (open_in vernacrc))
with
| End_of_file -> ()
@@ -470,7 +403,7 @@ Libobject.relax true;
(try let user_vernacrc =
try Some(Sys.getenv "USERVERNACRC")
with
- | Not_found as e ->
+ | Not_found ->
msgnl (str "no .vernacrc file"); None in
(match user_vernacrc with
Some f -> coqparser_loop (open_in f)
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index e0f88ba6..d2f71bfc 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -34,13 +34,13 @@ let get_hyp_by_name g name =
let evd = project g in
let env = pf_env g in
try (let judgment =
- Pretyping.understand_judgment
+ Pretyping.Default.understand_judgment
evd env (RVar(zz, name)) in
("hyp",judgment.uj_type))
(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
Loïc *)
with _ -> (let c = Nametab.global (Ident (zz,name)) in
- ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c)))
+ ("cste",type_of (Global.env()) Evd.empty (constr_of_global c)))
;;
type pbp_atom =
@@ -106,7 +106,7 @@ let make_final_cmd f optname clear_names constr path =
add_clear_names_if_necessary (f optname constr path) clear_names;;
let (rem_cast:pbp_rule) = function
- (a,c,cf,o, Cast(f,_), p, func) ->
+ (a,c,cf,o, Cast(f,_,_), p, func) ->
Some(func a c cf o (kind_of_term f) p)
| _ -> None;;
@@ -154,7 +154,7 @@ let make_pbp_pattern x =
[make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]
let rec make_then = function
- | [] -> TacId ""
+ | [] -> TacId []
| [t] -> t
| t1::t2::l -> make_then (TacThen (t1,t2)::l)
@@ -177,7 +177,7 @@ let make_pbp_atomic_tactic = function
TacAtom
(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
| PbpTryClear l ->
- TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l)))
+ TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
| PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
let rec make_pbp_tactic = function
@@ -203,7 +203,7 @@ let (imply_elim1: pbp_rule) = function
Some h, Prod(Anonymous, prem, body), 1::path, f ->
let clear_names' = if clear_flag then h::clear_names else clear_names in
let h' = next_global_ident hyp_radix avoid in
- let str_h' = (string_of_id h') in
+ let _str_h' = (string_of_id h') in
Some(PbpThens
([PbpLApply h],
[chain_tactics [make_named_intro h'] (make_clears (h::clear_names));
diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli
index 43ec1274..9daba184 100644
--- a/contrib/interface/pbp.mli
+++ b/contrib/interface/pbp.mli
@@ -1,4 +1,2 @@
val pbp_tac : (Tacexpr.raw_tactic_expr -> 'a) ->
- Names.identifier option -> int list ->
- Proof_type.goal Tacmach.sigma ->
- Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
+ Names.identifier option -> int list -> Proof_type.tactic
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5b265ec8..b7da5c1b 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -11,7 +11,6 @@ open Term
open Termops
open Util
open Proof_type
-open Coqast
open Pfedit
open Translate
open Term
@@ -54,7 +53,7 @@ and ngoal=
{newhyp : nhyp list;
t_concl : Term.constr;
t_full_concl: Term.constr;
- t_full_env: Sign.named_context}
+ t_full_env: Environ.named_context_val}
and ntree=
{t_info:string;
t_goal:ngoal;
@@ -151,7 +150,7 @@ let seq_to_lnhyp sign sign' cl =
{newhyp=nh;
t_concl=cl;
t_full_concl=long_type_hyp !lh cl;
- t_full_env = sign@sign'}
+ t_full_env = Environ.val_of_named_context (sign@sign')}
;;
@@ -163,26 +162,6 @@ let rule_is_complex r =
|_ -> false
;;
-let ast_of_constr = Termast.ast_of_constr true (Global.env()) ;;
-
-(*
-let rule_to_ntactic r =
- let rast =
- (match r with
- Tactic (s,l) ->
- Ast.ope (s,(List.map ast_of_cvt_arg l))
- | Prim (Refine h) ->
- Ast.ope ("Exact",
- [Node ((0,0), "COMMAND", [ast_of_constr h])])
- | _ -> Ast.ope ("Intros",[])) in
- if rule_is_complex r
- then (match rast with
- Node(_,_,[Node(_,_,[Node(_,_,x)])]) ->x
- | _ -> assert false)
-
- else [rast ]
-;;
-*)
let rule_to_ntactic r =
let rt =
(match r with
@@ -197,14 +176,6 @@ let rule_to_ntactic r =
else rt
;;
-(*
-let term_of_command x =
- match x with
- Node(_,_,y::_) -> y
- | _ -> x
-;;
-*)
-
(* Attribue les preuves de la liste l aux sous-buts non-prouvés de nt *)
@@ -226,7 +197,7 @@ let fill_unproved nt l =
let new_sign osign sign =
let res=ref [] in
List.iter (fun (id,c,ty) ->
- try (let (_,_,ty1)= (lookup_named id osign) in
+ try (let (_,_,_ty1)= (lookup_named id osign) in
())
with Not_found -> res:=(id,c,ty)::(!res))
sign;
@@ -247,6 +218,7 @@ let old_sign osign sign =
let to_nproof sigma osign pf =
let rec to_nproof_rec sigma osign pf =
let {evar_hyps=sign;evar_concl=cl} = pf.goal in
+ let sign = Environ.named_context_of_val sign in
let nsign = new_sign osign sign in
let oldsign = old_sign osign sign in
match pf.ref with
@@ -417,13 +389,6 @@ let enumerate f ln =
let constr_of_ast = Constrintern.interp_constr Evd.empty (Global.env());;
-(*
-let sp_tac tac =
- try spt (constr_of_ast (term_of_command tac))
- with _ -> (* let Node(_,t,_) = tac in *)
- spe (* sps ("error in sp_tac " ^ t) *)
-;;
-*)
let sp_tac tac = failwith "TODO"
let soit_A_une_proposition nh ln t= match !natural_language with
@@ -759,7 +724,7 @@ let rec nsortrec vl x =
nsortrec vl (mkInd (inductive_of_constructor c))
| Case(_,x,t,a)
-> nsortrec vl x
- | Cast(x,t)-> nsortrec vl t
+ | Cast(x,_, t)-> nsortrec vl t
| Const c -> nsortrec vl (lookup_constant c vl).const_type
| _ -> nsortrec vl (type_of vl Evd.empty x)
;;
@@ -791,7 +756,7 @@ let rec group_lhyp lh =
let natural_ghyp (sort,ln,lt) intro =
let t=List.hd lt in
let nh=List.length ln in
- let ns=List.hd ln in
+ let _ns=List.hd ln in
match sort with
Nprop -> soit_A_une_proposition nh ln t
| Ntype -> soit_X_un_element_de_T nh ln t
@@ -963,16 +928,6 @@ let natural_lhyp lh hi =
Analyse des tactiques.
*)
-(*
-let name_tactic tac =
- match tac with
- (Node(_,"Interp",
- (Node(_,_,
- (Node(_,t,_))::_))::_))::_ -> t
- |(Node(_,t,_))::_ -> t
- | _ -> assert false
-;;
-*)
let name_tactic = function
| TacIntroPattern _ -> "Intro"
| TacAssumption -> "Assumption"
@@ -991,51 +946,8 @@ let arg1_tactic tac =
;;
*)
-let arg1_tactic tac = failwith "TODO"
-
-let arg2_tactic tac =
- match tac with
- (Node(_,"Interp",
- (Node(_,_,
- (Node(_,_,_::x::_))::_))::_))::_ -> x
- | (Node(_,_,_::x::_))::_ -> x
- | _ -> assert false
-;;
-
-(*
-type nat_tactic =
- Split of (Coqast.t list)
- | Generalize of (Coqast.t list)
- | Reduce of string*(Coqast.t list)
- | Other of string*(Coqast.t list)
-;;
-
-let analyse_tac tac =
- match tac with
- [Node (_, "Split", [Node (_, "BINDINGS", [])])]
- -> Split []
- | [Node (_, "Split",[Node(_, "BINDINGS",[Node(_, "BINDING",
- [Node (_, "COMMAND", x)])])])]
- -> Split x
- | [Node (_, "Generalize", [Node (_, "COMMAND", x)])]
- ->Generalize x
- | [Node (_, "Reduce", [Node (_, "REDEXP", [Node (_, mode, _)]);
- Node (_, "CLAUSE", lhyp)])]
- -> Reduce(mode,lhyp)
- | [Node (_, x,la)] -> Other (x,la)
- | _ -> assert false
-;;
-*)
-
-
-
+let arg1_tactic tac = failwith "TODO";;
-
-let id_of_command x =
- match x with
- Node(_,_,Node(_,_,y::_)::_) -> y
- |_ -> assert false
-;;
type type_info_subgoals =
{ihsg: type_info_subgoals_hyp;
isgintro : string}
@@ -1285,7 +1197,7 @@ let rec natural_ntree ig ntree =
| TacAssumption -> natural_trivial ig lh g gs ltree
| TacClear _ -> natural_clear ig lh g gs ltree
(* Besoin de l'argument de la tactique *)
- | TacSimpleInduction (NamedHyp id,_) ->
+ | TacSimpleInduction (NamedHyp id) ->
natural_induction ig lh g gs ge id ltree false
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
@@ -1294,7 +1206,7 @@ let rec natural_ntree ig ntree =
| TacExact c -> natural_exact ig lh g gs c ltree
| TacCut c -> natural_cut ig lh g gs c ltree
| TacExtend (_,"CutIntro",[a]) ->
- let c = out_gen wit_constr a in
+ let _c = out_gen wit_constr a in
natural_cutintro ig lh g gs a ltree
| TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
| TacExtend (_,"CaseIntro",[a]) ->
@@ -1518,7 +1430,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
if with_intros
then (arity_of_constr_of_mind env indf 1)
else 0 in
- let ici= 1 in
+ let _ici= 1 in
sph[ (natural_ntree
{ihsg=
(match (nsort targ1) with
@@ -1547,7 +1459,7 @@ and prod_list_var t =
and hd_is_mind t ti =
try (let env = Global.env() in
let IndType (indf,targ) = find_rectype env Evd.empty t in
- let ncti= Array.length(get_constructors env indf) in
+ let _ncti= Array.length(get_constructors env indf) in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
(string_of_id mip.mind_typename) = ti)
@@ -1556,7 +1468,7 @@ and mind_ind_info_hyp_constr indf c =
let env = Global.env() in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
- let p = mip.mind_nparams in
+ let _p = mib.mind_nparams in
let a = arity_of_constr_of_mind env indf c in
let lp=ref (get_constructors env indf).(c).cs_args in
let lr=ref [] in
@@ -1586,8 +1498,8 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
let ncti= Array.length(get_constructors env indf) in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
- let ti =(string_of_id mip.mind_typename) in
- let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
+ let _ti =(string_of_id mip.mind_typename) in
+ let _type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1630,11 +1542,11 @@ and natural_induction ig lh g gs ge arg2 ltree with_intros=
let arg1= mkVar arg2 in
let targ1 = prod_head (type_of env Evd.empty arg1) in
let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors env indf) in
+ let _ncti= Array.length(get_constructors env indf) in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
- let ti =(string_of_id mip.mind_typename) in
- let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
+ let _ti =(string_of_id mip.mind_typename) in
+ let _type_arg= targ1(*List.nth targ (mis_index dmi)*) in
let lh1= hyps (List.hd ltree) in (* la liste des hyp jusqu'a n *)
(* on les enleve des hypotheses des sous-buts *)
@@ -1719,8 +1631,8 @@ and natural_reduce ig lh g gs ge mode la ltree =
and natural_split ig lh g gs ge la ltree =
match la with
[arg] ->
- let env= (gLOB ge) in
- let arg1= (*dbize env*) arg in
+ let _env= (gLOB ge) in
+ let arg1= (*dbize _env*) arg in
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1740,9 +1652,9 @@ and natural_split ig lh g gs ge la ltree =
and natural_generalize ig lh g gs ge la ltree =
match la with
[arg] ->
- let env= (gLOB ge) in
+ let _env= (gLOB ge) in
let arg1= (*dbize env*) arg in
- let type_arg=type_of (Global.env()) Evd.empty arg in
+ let _type_arg=type_of (Global.env()) Evd.empty arg in
(* let type_arg=type_of_ast ge arg in*)
spv
[ (natural_lhyp lh ig.ihsg);
diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli
index ee269458..9b6787b7 100755
--- a/contrib/interface/showproof.mli
+++ b/contrib/interface/showproof.mli
@@ -4,9 +4,7 @@ open Names
open Term
open Util
open Proof_type
-open Coqast
open Pfedit
-open Translate
open Term
open Reduction
open Clenv
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index ee901c5e..dd7f455d 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -3,7 +3,6 @@
Vers Ctcoq
*)
-open Esyntax
open Metasyntax
open Printer
open Pp
@@ -131,12 +130,12 @@ let rec sp_print x =
| "\n" -> fnl ()
| "Retour chariot pour Show proof" -> fnl ()
|_ -> str s)
- | CT_text_formula f -> prterm (Hashtbl.find ct_FORMULA_constr f)
+ | CT_text_formula f -> pr_lconstr (Hashtbl.find ct_FORMULA_constr f)
| CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
CT_text_path (CT_signed_int_list p);
CT_coerce_ID_to_TEXT (CT_ident "goal");
g] ->
- let p=(List.map (fun y -> match y with
+ let _p=(List.map (fun y -> match y with
(CT_coerce_INT_to_SIGNED_INT
(CT_int x)) -> x
| _ -> raise (Failure "sp_print")) p) in
@@ -149,7 +148,7 @@ let rec sp_print x =
CT_text_path (CT_signed_int_list p);
CT_coerce_ID_to_TEXT (CT_ident hyp);
g] ->
- let p=(List.map (fun y -> match y with
+ let _p=(List.map (fun y -> match y with
(CT_coerce_INT_to_SIGNED_INT
(CT_int x)) -> x
| _ -> raise (Failure "sp_print")) p) in
@@ -159,7 +158,7 @@ let rec sp_print x =
CT_text_path (CT_signed_int_list p);
CT_coerce_ID_to_TEXT (CT_ident hyp);
g] ->
- let p=(List.map (fun y -> match y with
+ let _p=(List.map (fun y -> match y with
(CT_coerce_INT_to_SIGNED_INT
(CT_int x)) -> x
| _ -> raise (Failure "sp_print")) p) in
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index e63baecf..6e4782be 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -1,13 +1,11 @@
open Names;;
open Sign;;
open Util;;
-open Ast;;
open Term;;
open Pp;;
open Libobject;;
open Library;;
open Vernacinterp;;
-open Termast;;
open Tacmach;;
open Pfedit;;
open Parsing;;
@@ -15,97 +13,11 @@ open Evd;;
open Evarutil;;
open Xlate;;
-open Ctast;;
open Vtp;;
open Ascent;;
open Environ;;
open Proof_type;;
-(* dead code: let rel_reference gt k oper =
- if is_existential_oper oper then ope("XTRA", [str "ISEVAR"])
- else begin
- let id = id_of_global oper in
- let oper', _ = global_operator (Nametab.sp_of_id k id) id in
- if oper = oper' then nvar (string_of_id id)
- else failwith "xlate"
-end;;
-*)
-
-(* dead code:
-let relativize relfun =
- let rec relrec =
- function
- | Nvar (_, id) -> nvar id
- | Slam (l, na, ast) -> Slam (l, na, relrec ast)
- | Node (loc, nna, l) as ast -> begin
- try relfun ast
- with
- | Failure _ -> Node (loc, nna, List.map relrec l)
- end
- | a -> a in
- relrec;;
-*)
-
-(* dead code:
-let dbize_sp =
- function
- | Path (loc, sl, s) -> begin
- try section_path sl s
- with
- | Invalid_argument _ | Failure _ ->
- anomaly_loc
- (loc, "Translate.dbize_sp (taken from Astterm)",
- [< str "malformed section-path" >])
- end
- | ast ->
- anomaly_loc
- (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
- [< str "not a section-path" >]);;
-*)
-
-(* dead code:
-let relativize_cci gt = relativize (function
- | Node (_, "CONST", (p :: _)) as gt ->
- rel_reference gt CCI (Const (dbize_sp p))
- | Node (_, "MUTIND", (p :: ((Num (_, tyi)) :: _))) as gt ->
- rel_reference gt CCI (MutInd (dbize_sp p, tyi))
- | Node (_, "MUTCONSTRUCT", (p :: ((Num (_, tyi)) :: ((Num (_, i)) :: _)))) as gt ->
- rel_reference gt CCI (MutConstruct (
- (dbize_sp p, tyi), i))
- | _ -> failwith "caught") gt;;
-*)
-
-let coercion_description_holder = ref (function _ -> None : t -> int option);;
-
-let coercion_description t = !coercion_description_holder t;;
-
-let set_coercion_description f =
- coercion_description_holder:=f; ();;
-
-let rec nth_tl l n = if n = 0 then l
- else (match l with
- | a :: b -> nth_tl b (n - 1)
- | [] -> failwith "list too short for nth_tl");;
-
-let rec discard_coercions =
- function
- | Slam (l, na, ast) -> Slam (l, na, discard_coercions ast)
- | Node (l, ("APPLIST" as nna), (f :: args as all_sons)) ->
- (match coercion_description f with
- | Some n ->
- let new_args =
- try nth_tl args n
- with
- | Failure "list too short for nth_tl" -> [] in
- (match new_args with
- | a :: (b :: c) -> Node (l, nna, List.map discard_coercions new_args)
- | a :: [] -> discard_coercions a
- | [] -> Node (l, nna, List.map discard_coercions all_sons))
- | None -> Node (l, nna, List.map discard_coercions all_sons))
- | Node (l, nna, all_sons) ->
- Node (l, nna, List.map discard_coercions all_sons)
- | it -> it;;
-
(*translates a formula into a centaur-tree --> FORMULA *)
let translate_constr at_top env c =
xlate_formula (Constrextern.extern_constr at_top env c);;
diff --git a/contrib/interface/vernacrc b/contrib/interface/vernacrc
index 42b5e5ab..4d3dc558 100644
--- a/contrib/interface/vernacrc
+++ b/contrib/interface/vernacrc
@@ -1,4 +1,4 @@
-# $Id: vernacrc,v 1.3 2004/01/14 14:52:59 bertot Exp $
+# $Id: vernacrc 5202 2004-01-14 14:52:59Z bertot $
# This file is loaded initially by ./vernacparser.
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index ff418523..5a7ccc26 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -407,6 +407,9 @@ and fCOMMAND = function
fNODE "print_about" 1
| CT_print_all -> fNODE "print_all" 0
| CT_print_classes -> fNODE "print_classes" 0
+| CT_print_ltac id ->
+ fID id;
+ fNODE "print_ltac" 1
| CT_print_coercions -> fNODE "print_coercions" 0
| CT_print_grammar(x1) ->
fGRAMMAR x1;
@@ -418,6 +421,9 @@ and fCOMMAND = function
| CT_print_hintdb(x1) ->
fID_OR_STAR x1;
fNODE "print_hintdb" 1
+| CT_print_rewrite_hintdb(x1) ->
+ fID x1;
+ fNODE "print_rewrite_hintdb" 1
| CT_print_id(x1) ->
fID x1;
fNODE "print_id" 1
@@ -451,6 +457,7 @@ and fCOMMAND = function
| CT_print_scope(x1) ->
fID x1;
fNODE "print_scope" 1
+| CT_print_setoids -> fNODE "print_setoids" 0
| CT_print_scopes -> fNODE "print_scopes" 0
| CT_print_section(x1) ->
fID x1;
@@ -1153,12 +1160,12 @@ and fMODULE_TYPE = function
| CT_coerce_ID_to_MODULE_TYPE x -> fID x
| CT_module_type_with_def(x1, x2, x3) ->
fMODULE_TYPE x1;
- fID x2;
+ fID_LIST x2;
fFORMULA x3;
fNODE "module_type_with_def" 3
| CT_module_type_with_mod(x1, x2, x3) ->
fMODULE_TYPE x1;
- fID x2;
+ fID_LIST x2;
fID x3;
fNODE "module_type_with_mod" 3
and fMODULE_TYPE_CHECK = function
@@ -1281,6 +1288,7 @@ and fRED_COM = function
fPATTERN_NE_LIST x1;
fNODE "pattern" 1
| CT_red -> fNODE "red" 0
+| CT_cbvvm -> fNODE "vm_compute" 0
| CT_simpl(x1) ->
fPATTERN_OPT x1;
fNODE "simpl" 1
@@ -1545,6 +1553,9 @@ and fTACTIC_COM = function
| CT_exact(x1) ->
fFORMULA x1;
fNODE "exact" 1
+| CT_exact_no_check(x1) ->
+ fFORMULA x1;
+ fNODE "exact_no_check" 1
| CT_exists(x1) ->
fSPEC_LIST x1;
fNODE "exists" 1
@@ -1649,12 +1660,12 @@ and fTACTIC_COM = function
fID x2;
fNODE "move_after" 2
| CT_new_destruct(x1, x2, x3) ->
- fFORMULA_OR_INT x1;
+ (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *)
fUSING x2;
fINTRO_PATT_OPT x3;
fNODE "new_destruct" 3
| CT_new_induction(x1, x2, x3) ->
- fFORMULA_OR_INT x1;
+ (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *)
fUSING x2;
fINTRO_PATT_OPT x3;
fNODE "new_induction" 3
@@ -1697,10 +1708,12 @@ and fTACTIC_COM = function
| CT_repeat(x1) ->
fTACTIC_COM x1;
fNODE "repeat" 1
-| CT_replace_with(x1, x2) ->
+| CT_replace_with(x1, x2,x3,x4) ->
fFORMULA x1;
fFORMULA x2;
- fNODE "replace_with" 2
+ fID_OPT x3;
+ fTACTIC_OPT x4;
+ fNODE "replace_with" 4
| CT_rewrite_lr(x1, x2, x3) ->
fFORMULA x1;
fSPEC_LIST x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 02dc57de..da87086e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -3,7 +3,6 @@
open String;;
open Char;;
open Util;;
-open Ast;;
open Names;;
open Ascent;;
open Genarg;;
@@ -64,11 +63,7 @@ let coercion_description t = !coercion_description_holder t;;
let set_coercion_description f =
coercion_description_holder:=f; ();;
-let string_of_node_loc the_node =
- match Util.unloc (loc the_node) with
- (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";;
-
-let xlate_error s = failwith ("Translation error: " ^ s);;
+let xlate_error s = print_endline ("xlate_error : "^s);failwith ("Translation error: " ^ s);;
let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;;
@@ -266,11 +261,13 @@ let rec xlate_match_pattern =
| CPatAlias (_, pattern, id) ->
CT_pattern_as
(xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
+ | CPatOr (_,l) -> xlate_error "CPatOr: TODO"
| CPatDelimiters(_, key, p) ->
CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
- | CPatNumeral(_,n) ->
+ | CPatPrim (_,Numeral n) ->
CT_coerce_NUM_to_MATCH_PATTERN
- (CT_int_encapsulator(Bignat.bigint_to_string n))
+ (CT_int_encapsulator(Bigint.to_string n))
+ | CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
| CPatNotation(_, s, l) ->
CT_pattern_notation(CT_string s,
CT_match_pattern_list(List.map xlate_match_pattern l))
@@ -373,14 +370,11 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CApp(_, (_,f), l) ->
CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
| CCases (_, _, [], _) -> assert false
- | CCases (_, (Some _, _), _, _) -> xlate_error "NOT parsed: Cases with Some"
- | CCases (_,(None, ret_type), tm::tml, eqns)->
+ | CCases (_, ret_type, tm::tml, eqns)->
CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
List.map xlate_matched_formula tml),
xlate_formula_opt ret_type,
CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
- | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) ->
- xlate_error "No more COrderedCase"
| CLetTuple (_,a::l, ret_info, c, b) ->
CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
List.map xlate_id_opt_aux l),
@@ -393,27 +387,18 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
(xlate_formula c, xlate_return_info ret_info,
xlate_formula b1, xlate_formula b2)
- | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
- CT_inductive_let(xlate_formula_opt po,
- xlate_id_opt_ne_list l,
- xlate_formula c, xlate_formula b)
- | COrderedCase (_,c,v,e,l) ->
- let case_string = match c with
- Term.MatchStyle -> "Match"
- | _ -> "Case" in
- CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e,
- CT_formula_list(List.map xlate_formula l))
| CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
| CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
- | CNumeral(_, i) ->
- CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bignat.bigint_to_string i))
+ | CPrim (_, Numeral i) ->
+ CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
+ | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
| CHole _ -> CT_existvarc
(* I assume CDynamic has been inserted to make free form extension of
the language possible, but this would go agains the logic of pcoq anyway. *)
| CDynamic (_, _) -> assert false
| CDelimiters (_, key, num) ->
CT_num_encapsulator(CT_num_type key , xlate_formula num)
- | CCast (_, e, t) ->
+ | CCast (_, e,_, t) ->
CT_coerce_TYPED_FORMULA_to_FORMULA
(CT_typed_formula(xlate_formula e, xlate_formula t))
| CPatVar (_, (_,i)) when is_int_meta i ->
@@ -430,11 +415,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
CT_cofixc(xlate_ident id,
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
| CFix (_, (_, id), lm::lmi) ->
- let strip_mutrec (fid, n, bl, arf, ardef) =
+ let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
let (struct_arg,bl,arf,ardef) =
if bl = [] then
let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
- let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
@@ -485,14 +469,14 @@ let xlate_hyp = function
let xlate_hyp_location =
function
- | AI (_,id), nums, (InHypTypeOnly,_) ->
+ | AI (_,id), nums, InHypTypeOnly ->
CT_intype(xlate_ident id, nums_to_int_list nums)
- | AI (_,id), nums, (InHypValueOnly,_) ->
+ | AI (_,id), nums, InHypValueOnly ->
CT_invalue(xlate_ident id, nums_to_int_list nums)
- | AI (_,id), [], (InHyp,_) ->
+ | AI (_,id), [], InHyp ->
CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_coerce_ID_to_UNFOLD (xlate_ident id))
- | AI (_,id), a::l, (InHyp,_) ->
+ | AI (_,id), a::l, InHyp ->
CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_unfold_occ (xlate_ident id,
CT_int_ne_list(CT_int a, nums_to_int_list_aux l)))
@@ -631,6 +615,7 @@ let rec xlate_intro_pattern =
ll)
| IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
| IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
+ | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
let compute_INV_TYPE = function
FullInversionClear -> CT_inv_clear
@@ -678,9 +663,11 @@ let xlate_one_unfold_block = function
| (n::nums, qid) ->
CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
-let xlate_intro_patt_opt = function
- None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
- | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+let xlate_with_names = function
+ IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+ | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+
+let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
function
@@ -729,6 +716,7 @@ and xlate_red_tactic =
function
| Red true -> xlate_error ""
| Red false -> CT_red
+ | CbvVm -> CT_cbvvm
| Hnf -> CT_hnf
| Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
| Simpl (Some (l,c)) ->
@@ -788,6 +776,7 @@ and xlate_tactic =
| TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
| TacSolve([]) -> assert false
| TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
+ | TacComplete _ -> xlate_error "TODO: tactical complete"
| TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
| TacTry t -> CT_try (xlate_tactic t)
| TacRepeat t -> CT_repeat(xlate_tactic t)
@@ -798,7 +787,8 @@ and xlate_tactic =
xlate_tactic t)
| TacProgress t -> CT_progress(xlate_tactic t)
| TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
- | TacMatch (exp, rules) ->
+ | TacMatch (true,_,_) -> failwith "TODO: lazy match"
+ | TacMatch (false, exp, rules) ->
CT_match_tac(xlate_tactic exp,
match List.map
(function
@@ -814,11 +804,11 @@ and xlate_tactic =
| [] -> assert false
| fst::others ->
CT_match_tac_rules(fst, others))
- | TacMatchContext (_,[]) -> failwith ""
- | TacMatchContext (false,rule1::rules) ->
+ | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
+ | TacMatchContext (false,false,rule1::rules) ->
CT_match_context(xlate_context_rule rule1,
List.map xlate_context_rule rules)
- | TacMatchContext (true,rule1::rules) ->
+ | TacMatchContext (false,true,rule1::rules) ->
CT_match_context_reverse(xlate_context_rule rule1,
List.map xlate_context_rule rules)
| TacLetIn (l, t) ->
@@ -855,18 +845,23 @@ 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 (count, "") -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
- | TacFail (count, s) -> CT_fail(xlate_id_or_int count,
+ | TacFail (count, []) -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
+ | TacFail (count, [MsgString s]) -> CT_fail(xlate_id_or_int count,
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))
+ | TacFail (count, _) -> xlate_error "TODO: generic fail message"
+ | TacId [] -> CT_idtac ctf_STRING_OPT_NONE
+ | TacId [MsgString s] -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+ | TacId _ -> xlate_error "TODO: generic idtac message"
| TacInfo t -> CT_info(xlate_tactic t)
| TacArg a -> xlate_call_or_tacarg a
and xlate_tac =
function
| TacExtend (_, "firstorder", tac_opt::l) ->
- let t1 = match out_gen (wit_opt rawwit_tactic) tac_opt with
+ let t1 =
+ match
+ out_gen (wit_opt rawwit_main_tactic) tac_opt
+ with
| None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
| Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in
(match l with
@@ -914,7 +909,7 @@ and xlate_tac =
CT_discriminate_eq
(xlate_quantified_hypothesis_opt
(out_gen (wit_opt rawwit_quant_hyp) idopt))
- | TacExtend (_,"deq", [idopt]) ->
+ | TacExtend (_,"simplify_eq", [idopt]) ->
let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
let idopt2 = match idopt1 with
None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
@@ -962,53 +957,68 @@ 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]) ->
- let c1 = xlate_formula (out_gen rawwit_constr c1) in
- let c2 = xlate_formula (out_gen rawwit_constr c2) in
- CT_replace_with (c1, c2)
+ | TacExtend (_,"replace", [c1; c2;id_opt;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 tac_opt =
+ match out_gen (Extratactics.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)
| TacExtend (_,"rewrite", [b; cbindl]) ->
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
if b then CT_rewrite_lr (c, bindl, ctv_ID_OPT_NONE)
else CT_rewrite_rl (c, bindl, ctv_ID_OPT_NONE)
- | TacExtend (_,"rewritein", [b; cbindl; id]) ->
+ | TacExtend (_,"rewrite_in", [b; cbindl; id]) ->
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
- let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+ let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
if b then CT_rewrite_lr (c, bindl, id)
else CT_rewrite_rl (c, bindl, id)
- | TacExtend (_,"conditionalrewrite", [t; b; cbindl]) ->
- let t = out_gen rawwit_tactic t in
+ | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
+ let t = out_gen rawwit_main_tactic t in
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
- | TacExtend (_,"conditionalrewritein", [t; b; cbindl; id]) ->
- let t = out_gen rawwit_tactic t in
+ | TacExtend (_,"conditional_rewrite", [t; b; cbindl; id]) ->
+ let t = out_gen rawwit_main_tactic t in
let b = out_gen Extraargs.rawwit_orient b in
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
- let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+ let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id)
else CT_condrewrite_rl (xlate_tactic t, c, bindl, id)
- | TacExtend (_,"dependentrewrite", [b; id_or_constr]) ->
+ | TacExtend (_,"dependent_rewrite", [b; c]) ->
let b = out_gen Extraargs.rawwit_orient b in
- (match genarg_tag id_or_constr with
- | IdentArgType -> (*Dependent Rewrite/SubstHypInConcl*)
- let id = xlate_ident (out_gen rawwit_ident id_or_constr) in
+ let c = xlate_formula (out_gen rawwit_constr c) in
+ (match c with
+ | CT_coerce_ID_to_FORMULA (CT_ident _ as id) ->
if b then CT_deprewrite_lr id else CT_deprewrite_rl id
- | ConstrArgType -> (*CutRewrite/SubstConcl*)
- let c = xlate_formula (out_gen rawwit_constr id_or_constr) in
- if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
- else CT_cutrewrite_rl (c, ctv_ID_OPT_NONE)
- | _ -> xlate_error "")
- | TacExtend (_,"dependentrewrite", [b; c; id]) -> (*CutRewrite in/SubstHyp*)
+ | _ -> xlate_error "dependent rewrite on term: not supported")
+ | TacExtend (_,"dependent_rewrite", [b; c; id]) ->
+ xlate_error "dependent rewrite on terms in hypothesis: not supported"
+ | TacExtend (_,"cut_rewrite", [b; c]) ->
+ let b = out_gen Extraargs.rawwit_orient b in
+ let c = xlate_formula (out_gen rawwit_constr c) in
+ if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
+ else CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
+ | TacExtend (_,"cut_rewrite", [b; c; id]) ->
let b = out_gen Extraargs.rawwit_orient b in
let c = xlate_formula (out_gen rawwit_constr c) in
- let id = xlate_ident (out_gen rawwit_ident id) in
+ let id = xlate_ident (snd (out_gen rawwit_var id)) in
if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
| TacExtend(_, "subst", [l]) ->
@@ -1021,6 +1031,7 @@ and xlate_tac =
| TacTransitivity c -> CT_transitivity (xlate_formula c)
| TacAssumption -> CT_assumption
| TacExact c -> CT_exact (xlate_formula c)
+ | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
| TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id)
| TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id)
| TacDestructConcl -> CT_dconcl
@@ -1031,14 +1042,16 @@ and xlate_tac =
(if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
(if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
| TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
- | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
- | TacAuto (nopt, None) ->
+ | TacAuto (nopt, [], Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
+ | TacAuto (nopt, [], None) ->
CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
- | TacAuto (nopt, Some (id1::idl)) ->
+ | TacAuto (nopt, [], Some (id1::idl)) ->
CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
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)))
+ | TacAuto (nopt, _::_, _) ->
+ xlate_error "TODO: auto using"
|TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
let (id_list:ct_ID list) =
List.map (fun x -> CT_ident x) (out_gen (wit_list1 rawwit_pre_ident) l) in
@@ -1048,11 +1061,11 @@ and xlate_tac =
match t with
[t0] ->
CT_coerce_TACTIC_COM_to_TACTIC_OPT
- (xlate_tactic(out_gen rawwit_tactic t0))
+ (xlate_tactic(out_gen rawwit_main_tactic t0))
| [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
| _ -> assert false in
CT_autorewrite (CT_id_ne_list(fst, id_list1), t1)
- | TacExtend (_,"eauto", [nopt; popt; idl]) ->
+ | TacExtend (_,"eauto", [nopt; popt; lems; idl]) ->
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
@@ -1063,6 +1076,10 @@ and xlate_tac =
| 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 _lems =
+ match out_gen Eauto.rawwit_auto_using lems with
+ | [] -> []
+ | _ -> xlate_error "TODO: eauto using" in
let idl = out_gen Eauto.rawwit_hintbases idl in
(match idl with
None -> CT_eauto_with(first_n,
@@ -1084,12 +1101,14 @@ and xlate_tac =
let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
let c = xlate_formula c and bindl = xlate_bindings bindl in
CT_eapply (c, bindl)
- | TacTrivial (Some []) -> CT_trivial
- | TacTrivial None ->
+ | TacTrivial ([],Some []) -> CT_trivial
+ | TacTrivial ([],None) ->
CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
- | TacTrivial (Some (id1::idl)) ->
+ | TacTrivial ([],Some (id1::idl)) ->
CT_trivial_with(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))))
+ | TacTrivial (_::_,_) ->
+ xlate_error "TODO: trivial using"
| TacReduce (red, l) ->
CT_reduce (xlate_red_tactic red, xlate_clause l)
| TacApply (c,bindl) ->
@@ -1111,7 +1130,7 @@ and xlate_tac =
CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
| TacCase (c1,sl) ->
CT_casetac (xlate_formula c1, xlate_bindings sl)
- | TacSimpleInduction (h,_) -> CT_induction (xlate_quantified_hypothesis h)
+ | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
| TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
| TacCut c -> CT_cut (xlate_formula c)
| TacLApply c -> CT_use (xlate_formula c)
@@ -1123,20 +1142,21 @@ and xlate_tac =
CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
| TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
| TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
- | TacClear [] ->
+ | TacClear (false,[]) ->
xlate_error "Clear expects a non empty list of identifiers"
- | TacClear (id::idl) ->
+ | TacClear (false,id::idl) ->
let idl' = List.map xlate_hyp idl in
CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
+ | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
| (*For translating tactics/Inv.v *)
TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
- xlate_intro_patt_opt l,
+ xlate_with_names l,
CT_id_list (List.map xlate_hyp idl))
| TacInversion (DepInversion (k,copt,l),quant_hyp) ->
let id = xlate_quantified_hypothesis quant_hyp in
CT_depinversion (compute_INV_TYPE k, id,
- xlate_intro_patt_opt l, xlate_formula_opt copt)
+ xlate_with_names l, xlate_formula_opt copt)
| TacInversion (InversionUsing (c,idlist), id) ->
let id = xlate_quantified_hypothesis id in
CT_use_inversion (id, xlate_formula c,
@@ -1148,28 +1168,34 @@ and xlate_tac =
CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
| TacDAuto (a, b) ->
CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
- | TacNewDestruct(a,b,(c,_)) ->
- CT_new_destruct
- (xlate_int_or_constr a, xlate_using b,
- xlate_intro_patt_opt c)
- | TacNewInduction(a,b,(c,_)) ->
- CT_new_induction
- (xlate_int_or_constr a, xlate_using b,
- xlate_intro_patt_opt c)
- | TacInstantiate (a, b, cl) ->
+ | TacNewDestruct(a,b,c) ->
+ CT_new_destruct (* Julien F. : est-ce correct *)
+ (List.map xlate_int_or_constr a, xlate_using b,
+ xlate_with_names c)
+ | TacNewInduction(a,b,c) ->
+ CT_new_induction (* Pierre C. : est-ce correct *)
+ (List.map xlate_int_or_constr a, xlate_using b,
+ xlate_with_names c)
+ (*| TacInstantiate (a, b, cl) ->
CT_instantiate(CT_int a, xlate_formula b,
- xlate_clause cl)
+ assert false) *)
+ | TacLetTac (na, c, cl) when cl = nowhere ->
+ CT_pose(xlate_id_opt_aux na, xlate_formula c)
| TacLetTac (na, c, cl) ->
CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
(* TODO LATER: This should be shared with Unfold,
but the structures are different *)
xlate_clause cl)
- | TacForward (true, name, c) ->
- CT_pose(xlate_id_opt_aux name, xlate_formula c)
- | TacForward (false, name, c) ->
- CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
- | TacTrueCut (na, c) ->
- CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c)
+ | TacAssert (None, IntroIdentifier id, c) ->
+ CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
+ | TacAssert (None, IntroAnonymous, c) ->
+ CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+ | TacAssert (Some (TacId []), IntroIdentifier id, c) ->
+ CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
+ | TacAssert (Some (TacId []), IntroAnonymous, c) ->
+ CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+ | TacAssert _ ->
+ xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
| TacAnyConstructor(Some tac) ->
CT_any_constructor
(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
@@ -1181,6 +1207,7 @@ and xlate_tac =
(List.map xlate_formula
(out_gen (wit_list0 rawwit_constr) args)))
| TacExtend (_,id, l) ->
+ print_endline ("Extratactics : "^ id);
CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
| TacAlias _ -> xlate_error "Alias not supported"
@@ -1216,8 +1243,11 @@ and coerce_genarg_to_TARG x =
CT_coerce_FORMULA_OR_INT_to_TARG
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
(CT_coerce_ID_to_ID_OR_INT id))
- | HypArgType ->
- xlate_error "TODO (similar to IdentArgType)"
+ | VarArgType ->
+ let id = xlate_ident (snd (out_gen rawwit_var x)) in
+ 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_FORMULA_OR_INT_to_TARG
@@ -1233,19 +1263,14 @@ and coerce_genarg_to_TARG x =
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
- | TacticArgType ->
- let t = xlate_tactic (out_gen rawwit_tactic x) in
+ | TacticArgType n ->
+ let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
CT_coerce_TACTIC_COM_to_TARG t
- | OpenConstrArgType ->
- CT_coerce_SCOMMENT_CONTENT_to_TARG
- (CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
- (snd (out_gen
- rawwit_open_constr x))))
- | CastedOpenConstrArgType ->
+ | OpenConstrArgType b ->
CT_coerce_SCOMMENT_CONTENT_to_TARG
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
- (snd (out_gen
- rawwit_casted_open_constr x))))
+ (snd (out_gen
+ (rawwit_open_constr_gen b) x))))
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
| BindingsArgType -> xlate_error "TODO: generic with bindings"
| RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1315,8 +1340,11 @@ let coerce_genarg_to_VARG x =
CT_coerce_ID_OPT_OR_ALL_to_VARG
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
(CT_coerce_ID_to_ID_OPT id))
- | HypArgType ->
- xlate_error "TODO (similar to IdentArgType)"
+ | VarArgType ->
+ let id = xlate_ident (snd (out_gen rawwit_var x)) in
+ CT_coerce_ID_OPT_OR_ALL_to_VARG
+ (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
+ (CT_coerce_ID_to_ID_OPT id))
| RefArgType ->
let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
CT_coerce_ID_OPT_OR_ALL_to_VARG
@@ -1332,11 +1360,10 @@ let coerce_genarg_to_VARG x =
(CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
- | TacticArgType ->
- let t = xlate_tactic (out_gen rawwit_tactic x) in
+ | TacticArgType n ->
+ let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
- | OpenConstrArgType -> xlate_error "TODO: generic open constr"
- | CastedOpenConstrArgType -> xlate_error "TODO: generic open constr"
+ | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
| BindingsArgType -> xlate_error "TODO: generic with bindings"
| RedExprArgType -> xlate_error "TODO: red expr as generic argument"
@@ -1347,23 +1374,9 @@ let coerce_genarg_to_VARG x =
| ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
-let xlate_thm x = CT_thm (match x with
- | Theorem -> "Theorem"
- | Remark -> "Remark"
- | Lemma -> "Lemma"
- | Fact -> "Fact")
+let xlate_thm x = CT_thm (string_of_theorem_kind x)
-
-let xlate_defn x = CT_defn (match x with
- | (Local, Definition) -> "Local"
- | (Global, Definition) -> "Definition"
- | (Global, SubClass) -> "SubClass"
- | (Global, Coercion) -> "Coercion"
- | (Local, SubClass) -> "Local SubClass"
- | (Local, Coercion) -> "Local Coercion"
- | (Global,CanonicalStructure) -> "Canonical Structure"
- | (Local, CanonicalStructure) ->
- xlate_error "Local CanonicalStructure not parsed")
+let xlate_defn k = CT_defn (string_of_definition_kind k)
let xlate_var x = CT_var (match x with
| (Global,Definitional) -> "Parameter"
@@ -1511,17 +1524,18 @@ let rec xlate_module_type = function
| CMTEwith(mty, decl) ->
let mty1 = xlate_module_type mty in
(match decl with
- CWith_Definition((_, id), c) ->
- CT_module_type_with_def(xlate_module_type mty,
- xlate_ident id, xlate_formula c)
- | CWith_Module((_, id), (_, qid)) ->
- CT_module_type_with_mod(xlate_module_type mty,
- xlate_ident id,
+ CWith_Definition((_, idl), c) ->
+ CT_module_type_with_def(mty1,
+ CT_id_list (List.map xlate_ident idl),
+ xlate_formula c)
+ | CWith_Module((_, idl), (_, qid)) ->
+ CT_module_type_with_mod(mty1,
+ CT_id_list (List.map xlate_ident idl),
CT_ident (xlate_qualid qid)));;
let xlate_module_binder_list (l:module_binder list) =
CT_module_binder_list
- (List.map (fun (idl, mty) ->
+ (List.map (fun (_, idl, mty) ->
let idl1 =
List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in
let fst,idl2 = match idl1 with
@@ -1643,18 +1657,13 @@ let rec xlate_vernac =
CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1,
ainv1, fth1, ainvl1, bind)
|_ -> assert false)
- | VernacExtend (("HintRewriteV7"|"HintRewriteV8") as key, largs) ->
- let in_v8 = (key = "HintRewriteV8") in
- let orient = out_gen Extraargs.rawwit_orient (List.nth largs 0) in
- let formula_list = out_gen (wit_list1 rawwit_constr) (List.nth largs 1) in
- let t =
- if List.length largs = 4 then
- out_gen rawwit_tactic (List.nth largs (if in_v8 then 2 else 3))
- else
- TacId "" in
- let base =
- out_gen rawwit_pre_ident
- (if in_v8 then last largs else List.nth largs 2) in
+ | VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) ->
+ let orient = out_gen Extraargs.rawwit_orient o in
+ let formula_list = out_gen (wit_list1 rawwit_constr) f in
+ let base = out_gen rawwit_pre_ident b in
+ let t =
+ match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId []
+ in
let ct_orient = match orient with
| true -> CT_lr
| false -> CT_rl in
@@ -1665,7 +1674,7 @@ let rec xlate_vernac =
| VernacHints (local,dbnames,h) ->
let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
(match h with
- | HintsConstructors (None, l) ->
+ | HintsConstructors l ->
let n1, names = match List.map tac_qualid_to_ct_ID l with
n1 :: names -> n1, names
| _ -> failwith "" in
@@ -1675,15 +1684,10 @@ let rec xlate_vernac =
else
CT_hints(CT_ident "Constructors",
CT_id_ne_list(n1, names), dblist)
- | HintsExtern (None, n, c, t) ->
+ | HintsExtern (n, c, t) ->
CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
| HintsResolve l | HintsImmediate l ->
- let l =
- List.map
- (function (None, f) -> xlate_formula f
- | _ ->
- xlate_error "obsolete Hint Resolve not supported") l in
- let f1, formulas = match l with
+ let f1, formulas = match List.map xlate_formula l with
a :: tl -> a, tl
| _ -> failwith "" in
let l' = CT_formula_ne_list(f1, formulas) in
@@ -1700,10 +1704,7 @@ let rec xlate_vernac =
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
| _ -> assert false)
| HintsUnfold l ->
- let l = List.map
- (function (None,ref) -> loc_qualid_to_ct_ID ref |
- _ -> xlate_error "obsolete Hint Unfold not supported") l in
- let n1, names = match l with
+ let n1, names = match List.map loc_qualid_to_ct_ID l with
n1 :: names -> n1, names
| _ -> failwith "" in
if local then
@@ -1724,9 +1725,6 @@ let rec xlate_vernac =
CT_hint_destruct
(xlate_ident id, CT_int n, dl, xlate_formula f,
xlate_tactic t, dblist)
- | HintsExtern(Some _, _, _, _)
- | HintsConstructors(Some _, _) ->
- xlate_error "obsolete Hint Constructors not supported"
)
| VernacEndProof (Proved (true,None)) ->
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
@@ -1759,6 +1757,7 @@ let rec xlate_vernac =
| VernacShow (ShowGoalImplicitly (Some n)) -> CT_show_implicit (CT_int n)
| VernacShow ShowExistentials -> CT_show_existentials
| VernacShow ShowScript -> CT_show_script
+ | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)"
| VernacGo arg -> CT_go (xlate_locn arg)
| VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l)
| VernacShow ExplainTree l ->
@@ -1775,6 +1774,8 @@ let rec xlate_vernac =
| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
| PrintHintDbName id ->
CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
+ | PrintRewriteHintDbName id ->
+ CT_print_rewrite_hintdb (CT_ident id)
| PrintHint id ->
CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
@@ -1783,12 +1784,15 @@ let rec xlate_vernac =
| PrintMLModules -> CT_ml_print_modules
| PrintGraph -> CT_print_graph
| PrintClasses -> CT_print_classes
+ | PrintLtac qid -> CT_print_ltac (loc_qualid_to_ct_ID qid)
| PrintCoercions -> CT_print_coercions
| PrintCoercionPaths (id1, id2) ->
CT_print_path (xlate_class id1, xlate_class id2)
+ | PrintCanonicalConversions ->
+ xlate_error "TODO: Print Canonical Structures"
| PrintInspect n -> CT_inspect (CT_int n)
| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
- | PrintLocalContext -> CT_print
+ | PrintSetoids -> CT_print_setoids
| PrintTables -> CT_print_tables
| PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
| PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
@@ -1867,13 +1871,12 @@ let rec xlate_vernac =
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"
- | VernacFixpoint (lm :: lmi) ->
- let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
+ | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
+ | VernacFixpoint ((lm :: lmi),boxed) ->
+ let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) =
let (struct_arg,bl,arf,ardef) =
if bl = [] then
let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
- let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
@@ -1885,8 +1888,8 @@ let rec xlate_vernac =
| _ -> xlate_error "mutual recursive" in
CT_fix_decl
(CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
- | VernacCoFixpoint [] -> xlate_error "mutual corecursive"
- | VernacCoFixpoint (lm :: lmi) ->
+ | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
+ | VernacCoFixpoint ((lm :: lmi),boxed) ->
let strip_mutcorec (fid, bl, arf, ardef) =
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
xlate_formula arf, xlate_formula ardef) in
@@ -1916,20 +1919,18 @@ let rec xlate_vernac =
| Some mty1 ->
CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
(xlate_module_type mty1))
- | VernacDefineModule((_, id), bl, mty_o, mexpr_o) ->
+ | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
CT_module(xlate_ident id,
xlate_module_binder_list bl,
xlate_module_type_check_opt mty_o,
match mexpr_o with
None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
| Some m -> xlate_module_expr m)
- | VernacDeclareModule((_, id), bl, mty_o, mexpr_o) ->
+ | VernacDeclareModule(_,(_, id), bl, mty_o) ->
CT_declare_module(xlate_ident id,
xlate_module_binder_list bl,
- xlate_module_type_check_opt mty_o,
- match mexpr_o with
- None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
- | Some m -> xlate_module_expr m)
+ xlate_module_type_check_opt (Some mty_o),
+ CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
| VernacRequire (impexp, spec, id::idl) ->
let ct_impexp, ct_spec = get_require_flags impexp spec in
CT_require (ct_impexp, ct_spec,
@@ -1943,8 +1944,6 @@ let rec xlate_vernac =
CT_require(ct_impexp, ct_spec,
CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
- | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
-
| VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
| VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
| VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
@@ -1966,8 +1965,7 @@ let rec xlate_vernac =
CT_id_ne_list(xlate_class_rawexpr a,
List.map xlate_class_rawexpr l))
| VernacBindScope(id, []) -> assert false
- | VernacNotation(b, c, None, _, _) -> assert false
- | VernacNotation(b, c, Some(s,modif_list), _, opt_scope) ->
+ | VernacNotation(b, c, (s,modif_list), opt_scope) ->
let translated_s = CT_string s in
let formula = xlate_formula c in
let translated_modif_list =
@@ -1981,7 +1979,7 @@ let rec xlate_vernac =
else
CT_define_notation(translated_s, formula,
translated_modif_list, translated_scope)
- | VernacSyntaxExtension(b,Some(s,modif_list), None) ->
+ | VernacSyntaxExtension(b,(s,modif_list)) ->
let translated_s = CT_string s in
let translated_modif_list =
CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
@@ -1989,8 +1987,7 @@ let rec xlate_vernac =
CT_local_reserve_notation(translated_s, translated_modif_list)
else
CT_reserve_notation(translated_s, translated_modif_list)
- | VernacSyntaxExtension(_, _, _) -> assert false
- | VernacInfix (b,(str,modl),id,_, opt_scope) ->
+ | VernacInfix (b,(str,modl),id, opt_scope) ->
let id1 = loc_qualid_to_ct_ID id in
let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
let s = CT_string str in
@@ -2001,7 +1998,6 @@ let rec xlate_vernac =
CT_local_infix(s, id1,modl1, translated_scope)
else
CT_infix(s, id1,modl1, translated_scope)
- | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
| VernacCoercion (s, id1, id2, id3) ->
let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
let local_opt =
@@ -2032,8 +2028,6 @@ let rec xlate_vernac =
(CT_command_list(xlate_vernac a,
List.map (fun (_, x) -> xlate_vernac x) l))
| VernacList([]) -> assert false
- | (VernacV7only _ | VernacV8only _) ->
- xlate_error "Not treated here"
| VernacNop -> CT_proof_no_op
| VernacComments l ->
CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
@@ -2057,6 +2051,7 @@ let rec xlate_vernac =
| VernacReserve([], _) -> assert false
| VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
| VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
+ | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module"
| VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
| VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
| VernacTime(v) -> CT_time(xlate_vernac v)
@@ -2113,9 +2108,9 @@ let rec xlate_vernac =
| VernacVar _ -> xlate_error "Grammar vernac obsolete"
| (VernacGlobalCheck _|VernacPrintOption _|
VernacMemOption (_, _)|VernacRemoveOption (_, _)
- | VernacBack _|VernacRestoreState _| VernacWriteState _|
- VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _|
- VernacTacticGrammar _)
+ | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
+ VernacSolveExistential (_, _)|VernacCanonical _ |
+ VernacTacticNotation _)
-> xlate_error "TODO: vernac";;
let rec xlate_vernac_list =
@@ -2123,8 +2118,5 @@ let rec xlate_vernac_list =
| VernacList (v::l) ->
CT_command_list
(xlate_vernac (snd v), List.map (fun (_,x) -> xlate_vernac x) l)
- | VernacV7only v ->
- if !Options.v7 then xlate_vernac_list v
- else xlate_error "Unknown command"
| VernacList [] -> xlate_error "xlate_command_list"
| _ -> xlate_error "Not a list of commands";;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 08:08:19 +0000