aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
authorherbelin2002-05-29 10:48:37 +0000
committerherbelin2002-05-29 10:48:37 +0000
commit32170384190168856efeac5bcf90edf1170b54d6 (patch)
tree0ea86b672df93d997fa1cab70b678ea7abdcf171 /contrib/interface
parent1e5182e9d5c29ae9adeed20dae32969785758809 (diff)
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/Centaur.v8
-rwxr-xr-xcontrib/interface/blast.ml11
-rw-r--r--contrib/interface/blast.mli4
-rw-r--r--contrib/interface/centaur.ml4 (renamed from contrib/interface/centaur.ml)308
-rw-r--r--contrib/interface/dad.ml102
-rw-r--r--contrib/interface/dad.mli4
-rw-r--r--contrib/interface/debug_tac.ml4 (renamed from contrib/interface/debug_tac.ml)174
-rw-r--r--contrib/interface/debug_tac.mli6
-rw-r--r--contrib/interface/name_to_ast.ml62
-rw-r--r--contrib/interface/name_to_ast.mli2
-rw-r--r--contrib/interface/parse.ml131
-rw-r--r--contrib/interface/pbp.ml471
-rw-r--r--contrib/interface/pbp.mli4
-rw-r--r--contrib/interface/showproof.ml207
-rw-r--r--contrib/interface/xlate.ml1393
-rw-r--r--contrib/interface/xlate.mli8
16 files changed, 2367 insertions, 528 deletions
diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v
index 654cf123fa..d27929f86d 100644
--- a/contrib/interface/Centaur.v
+++ b/contrib/interface/Centaur.v
@@ -1,3 +1,4 @@
+(*
Declare ML Module "ctast".
Declare ML Module "paths".
Declare ML Module "name_to_ast".
@@ -15,7 +16,7 @@ Declare ML Module "history".
Declare ML Module "centaur".
(* Require Export Illustrations. *)
(* Require Export AddDad. *)
-
+(*
Grammar vernac vernac : ast :=
goal_cmd [ "Goal" "Cmd" numarg($n) "with" tacarg($tac) "." ] ->
[(GOAL_CMD $n (TACTIC $tac))]
@@ -33,7 +34,7 @@ Grammar vernac vernac : ast :=
| compute_in_goal [ "COMPUTE_IN_GOAL" numarg($n) constrarg($c) "." ] ->
[(CHECK_IN_GOAL "COMPUTE" $n $c)]
| centaur_reset [ "Centaur" "Reset" identarg($id) "." ] -> [(Centaur_Reset $id)]
-(* | show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)] *)
+(*| show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)]*)
| start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ]
| start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ].
Grammar vernac ne_id_list : ast list :=
@@ -83,4 +84,5 @@ Grammar vernac vernac : ast :=
| text_proof_flag_on [ "Text" "Mode" "Off" "." ] ->
[(TEXT_MODE (AST "off"))].
-
+*)
+*)
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index f6a47f9862..4c57760de0 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -191,7 +191,7 @@ and e_my_find_search db_list local_db hdc concl =
tclTHEN (unify_e_resolve (term,cl))
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> unfold_constr c
- | Extern tacast -> Tacticals.conclPattern concl
+ | Extern tacast -> Auto.conclPattern concl
(out_some p) tacast
in
(free_try tac,fmt_autotactic t))
@@ -567,7 +567,6 @@ let vire_extvar s =
let blast gls =
let leaf g = {
status = Incomplete_proof;
- subproof = None;
goal = g;
ref = None } in
try (let (sgl,v) as res = !blast_tactic gls in
@@ -592,17 +591,19 @@ let blast gls =
;;
let blast_tac display_function = function
- | ((Integer n)::_) as l ->
+ | (n::_) as l ->
(function g ->
let exp_ast = (blast g) in
- (display_function (ast_to_ct exp_ast);
+ (display_function exp_ast;
tclIDTAC g))
| _ -> failwith "expecting other arguments";;
let blast_tac_txt =
- blast_tac (function x -> msgnl(Printer.gentacpr (ct_to_ast x)));;
+ blast_tac (function x -> msgnl(Pptactic.pr_raw_tactic x));;
+(* Obsolète ?
overwriting_add_tactic "Blast1" blast_tac_txt;;
+*)
(*
Grammar tactic ne_numarg_list : list :=
diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli
index e8bcf95c63..21c29bc986 100644
--- a/contrib/interface/blast.mli
+++ b/contrib/interface/blast.mli
@@ -1,5 +1,5 @@
-val blast_tac : (Ctast.t -> 'a) ->
- Proof_type.tactic_arg list ->
+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;;
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml4
index 6f5281d565..e1ef0ecc15 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml4
@@ -1,3 +1,4 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
(*Toplevel loop for the communication between Coq and Centaur *)
open Names;;
@@ -42,11 +43,20 @@ open Astterm;;
open Nametab;;
open Showproof;;
open Showproof_ct;;
+open Tacexpr;;
+open Vernacexpr;;
+let pcoq_started = ref None;;
+
+let if_pcoq f a =
+ if !pcoq_started <> None then f a else error "Pcoq is not started";;
let text_proof_flag = ref "en";;
+(*
let current_proof_name = ref "";;
+*)
+let current_proof_name () = string_of_id (get_current_proof_name ())
let current_goal_index = ref 0;;
@@ -72,13 +82,13 @@ let print_path p =
;;
let kill_proof_node index =
- let paths = History.historical_undo !current_proof_name index in
+ let paths = History.historical_undo (current_proof_name()) index in
let _ = List.iter
(fun path -> (traverse_to path;
Pfedit.mutate weak_undo_pftreestate;
traverse_to []))
paths in
- History.border_length !current_proof_name;;
+ History.border_length (current_proof_name());;
(*Message functions, the text of these messages is recognized by the protocols *)
@@ -100,7 +110,7 @@ let ctf_acknowledge_command request_id command_count opt_exn =
int command_count ++ fnl() ++
int goal_count ++ fnl () ++
int goal_index ++ fnl () ++
- str !current_proof_name ++ fnl() ++
+ str (current_proof_name()) ++ fnl() ++
(match opt_exn with
Some e -> Cerrors.explain_exn e
| None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
@@ -203,7 +213,7 @@ let check_break () =
else ();;
let print_past_goal index =
- let path = History.get_path_for_rank !current_proof_name index in
+ let path = History.get_path_for_rank (current_proof_name()) index in
try traverse_to path;
let pf = proof_of_pftreestate (get_pftreestate ()) in
output_results (ctf_PathGoalMessage ())
@@ -223,7 +233,7 @@ let show_nth n =
then output_results (ctf_TextMessage !global_request_id)
(Some (P_text (show_proof !text_proof_flag [])))
else
- let path = History.get_nth_open_path !current_proof_name n in
+ let path = History.get_nth_open_path (current_proof_name()) n in
output_results (ctf_TextMessage !global_request_id)
(Some (P_text (show_proof !text_proof_flag path))))
else
@@ -240,9 +250,11 @@ let show_nth n =
let ctv_SEARCH_LIST = ref ([] : ct_PREMISE list);;
-let filter_by_module_from_varg_list (l:vernac_arg list) =
- let dir_list, b = Vernacentries.inside_outside l in
+(*
+let filter_by_module_from_varg_list l =
+ let dir_list, b = Vernacentries.interp_search_restriction l in
Search.filter_by_module_from_list (dir_list, b);;
+*)
let add_search (global_reference:global_reference) assumptions cstr =
try
@@ -260,15 +272,17 @@ let add_search (global_reference:global_reference) assumptions cstr =
ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST
with e -> msgnl (str "add_search raised an exception"); raise e;;
+(*
let make_error_stream node_string =
str "The syntax of " ++ str node_string ++
str " is inconsistent with the vernac interpreter entry";;
+*)
let ctf_EmptyGoalMessage id =
fnl () ++ str "Empty Goal is a no-op. Fun oh fun." ++ fnl ();;
-let print_check (ast, judg) =
+let print_check judg =
let {uj_val=value; uj_type=typ} = judg in
let value_ct_ast =
(try translate_constr false (Global.env()) value
@@ -289,7 +303,7 @@ let print_check (ast, judg) =
(CT_typed_formula(value_ct_ast,type_ct_ast)
)]))));;
-let ct_print_eval ast red_fun env evd judg =
+let ct_print_eval ast red_fun env judg =
((if refining() then traverse_to []);
let {uj_val=value; uj_type=typ} = judg in
let nvalue = red_fun value
@@ -320,13 +334,13 @@ let globcv x =
| _ -> failwith "globcv : unexpected value";;
let pbp_tac_pcoq =
- pbp_tac (function (x:Ctast.t) ->
+ pbp_tac (function (x:raw_tactic_expr) ->
output_results
(ctf_header "pbp_results" !global_request_id)
(Some (P_t(xlate_tactic x))));;
let blast_tac_pcoq =
- blast_tac (function (x:Ctast.t) ->
+ blast_tac (function (x:raw_tactic_expr) ->
output_results
(ctf_header "pbp_results" !global_request_id)
(Some (P_t(xlate_tactic x))));;
@@ -345,18 +359,17 @@ let search_output_results () =
(List.rev !ctv_SEARCH_LIST))));;
-let debug_tac2_pcoq = function
- [Tacexp ast] ->
+let debug_tac2_pcoq tac =
(fun g ->
let the_goal = ref (None : goal sigma option) in
- let the_ast = ref ast in
+ let the_ast = ref tac in
let the_path = ref ([] : int list) in
try
- let result = report_error ast 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) ++
fnl () ++ str "the tactic is" ++ fnl () ++
- Printer.gentacpr ast);
+ Pptactic.pr_raw_tactic tac);
result)
with
e ->
@@ -370,13 +383,12 @@ let debug_tac2_pcoq = function
(List.map
(fun n -> CT_coerce_INT_to_SIGNED_INT
(CT_int n))
- (clean_path 0 ast
+ (clean_path tac
(List.rev !the_path)))))));
(output_results
(ctf_OtherGoal !global_request_id)
(Some (P_r (translate_goal (sig_it g)))));
- raise e)
- | _ -> error "wrong arguments for debug_tac2_pcoq";;
+ raise e);;
let rec selectinspect n env =
match env with
@@ -437,13 +449,15 @@ let pair_list_to_ct l =
[ct_int_to_TARG a; ct_int_to_TARG b])))
l));;
+(* Annule toutes les commandes qui s'appliquent sur les sous-buts du
+ but auquel a été appliquée la n-ième tactique *)
let logical_kill n =
- let path = History.get_path_for_rank !current_proof_name n in
+ let path = History.get_path_for_rank (current_proof_name()) n in
begin
traverse_to path;
Pfedit.mutate weak_undo_pftreestate;
(let kept_cmds, undone_cmds, remaining_goals, current_goal =
- History.logical_undo !current_proof_name n in
+ History.logical_undo (current_proof_name()) n in
output_results (ctf_undoResults !global_request_id)
(Some
(P_t
@@ -457,24 +471,118 @@ let logical_kill n =
traverse_to []
end;;
+let simulate_solve n tac =
+ let path = History.get_nth_open_path (current_proof_name()) n in
+ solve_nth n (Tacinterp.hide_interp tac);
+ traverse_to path;
+ Pfedit.mutate weak_undo_pftreestate;
+ traverse_to []
+
+let kill_node_verbose n =
+ let ngoals = kill_proof_node n in
+ output_results_nl (ctf_KilledMessage !global_request_id ngoals)
+
+let set_text_mode s = text_proof_flag := s
+
+VERNAC COMMAND EXTEND TextMode
+| [ "Text" "Mode" "fr" ] -> [ set_text_mode "fr" ]
+| [ "Text" "Mode" "en" ] -> [ set_text_mode "en" ]
+| [ "Text" "Mode" "Off" ] -> [ set_text_mode "off" ]
+END
+
+VERNAC COMMAND EXTEND OutputGoal
+ [ "Goal" ] -> [ output_results_nl(ctf_EmptyGoalMessage "") ]
+END
+
+VERNAC COMMAND EXTEND OutputGoal
+ [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ]
+END
+
+VERNAC COMMAND EXTEND KillProof
+| [ "Kill" "Proof" "after" natural(n) ] -> [ kill_node_verbose n ]
+| [ "Kill" "Proof" "at" natural(n) ] -> [ kill_node_verbose n ]
+END
+
+VERNAC COMMAND EXTEND KillSubProof
+ [ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ]
+END
+
+let start_proof_hook () =
+ History.start_proof (current_proof_name());
+ current_goal_index := 1
+
+let solve_hook n =
+ let name = current_proof_name () in
+ let old_n_count = History.border_length name in
+ let pf = proof_of_pftreestate (get_pftreestate ()) in
+ let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
+ begin
+ current_goal_index := n;
+ History.push_command name n n_goals
+ end
+
+let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
+
+let pcoq_search s l =
+ ctv_SEARCH_LIST:=[];
+ begin match s with
+ | SearchPattern c ->
+ let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ raw_pattern_search (filter_by_module_from_list l) add_search pat
+ | SearchRewrite c ->
+ let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ raw_search_rewrite (filter_by_module_from_list l) add_search pat;
+ | SearchHead locqid ->
+ filtered_search
+ (filter_by_module_from_list l) add_search (Nametab.global locqid)
+ end;
+ search_output_results()
+
+let pcoq_print_name (_,qid) =
+ let results = xlate_vernac_list (name_to_ast qid) in
+ output_results
+ (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
+ (Some (P_cl results))
+
+let pcoq_print_check j =
+ let a,b = print_check j in output_results a b
+
+let pcoq_print_eval redfun env c j =
+ let strm, vtp = ct_print_eval (Ctast.ast_to_ct c) redfun env j in
+ output_results strm vtp;;
+
+open Vernacentries
+
+let pcoq_show_goal = function
+ | Some n -> show_nth n
+ | None ->
+ if !pcoq_started = Some true (* = debug *) then show_open_subgoals ()
+ else errorlabstrm "show_goal"
+ (str "Show must be followed by an integer in Centaur mode");;
+
+let pcoq_hook = {
+ start_proof = start_proof_hook;
+ solve = solve_hook;
+ abort = abort_hook;
+ search = pcoq_search;
+ print_name = pcoq_print_name;
+ print_check = pcoq_print_check;
+ print_eval = pcoq_print_eval;
+ show_goal = pcoq_show_goal
+}
+
+(*
let command_changes = [
("TEXT_MODE",
(function
- | [VARG_AST (Str(_,x))] ->
- (match x with
- "fr" -> (function () -> text_proof_flag := "fr")
- | "en" -> (function () -> text_proof_flag := "en")
- | "off" -> (function () -> text_proof_flag := "off")
- | s -> errorlabstrm "TEXT_MODE" (make_error_stream
- ("Unexpected flag " ^ s)))
- | _ -> errorlabstrm "TEXT_MODE"
- (make_error_stream "Unexpected argument")));
+ | [Coqast.VARG_AST (Str(_,x))] ->
+ (fun () -> set_text_mode x)));
("StartProof",
(function
- | (VARG_STRING kind) ::
- ((VARG_IDENTIFIER s) ::
- ((VARG_CONSTR c) :: [])) ->
+ | (Coqast.VARG_STRING kind) ::
+ ((Coqast.VARG_IDENTIFIER s) ::
+ ((Coqast.VARG_CONSTR c) :: [])) ->
let stre =
match kind with
| "THEOREM" -> NeverDischarge
@@ -495,22 +603,18 @@ let command_changes = [
);
let str = (string_of_id s) in
start_proof_com (Some s) stre c;
- History.start_proof str;
- current_proof_name := str;
- current_goal_index := 1
+ start_proof_hook str;
end
| _ -> errorlabstrm "StartProof" (make_error_stream "StartProof")));
-
+
("GOAL",
(function
- | (VARG_CONSTR c) :: [] ->
+ | (Coqast.VARG_CONSTR c) :: [] ->
(fun () ->
if not (refining ()) then
begin
start_proof_com None NeverDischarge c;
- History.start_proof "Unnamed_thm";
- current_proof_name := "Unnamed_thm";
- current_goal_index := 1
+ start_proof_hook "Unnamed_thm"
end)
| [] ->
(function () -> output_results_nl(ctf_EmptyGoalMessage ""))
@@ -518,24 +622,21 @@ let command_changes = [
("SOLVE",
(function
- | [VARG_NUMBER n; VARG_TACTIC tcom] ->
+ | [Coqast.VARG_NUMBER n; Coqast.VARG_TACTIC tcom] ->
(fun () ->
if not (refining ()) then
error "Unknown command of the non proof-editing mode";
solve_nth n (Tacinterp.hide_interp tcom);
- let old_n_count = History.border_length !current_proof_name in
- let pf = proof_of_pftreestate (get_pftreestate ()) in
- let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
- begin
- current_goal_index := n;
- History.push_command !current_proof_name n n_goals
- end)
+(* pcoq *)
+ solve_hook n
+(**)
| _ -> errorlabstrm "SOLVE" (make_error_stream "SOLVE")));
+(* SIMULE SOLVE SANS EFFET *)
("GOAL_CMD",
(function
- | (VARG_NUMBER n) ::
- ((VARG_TACTIC tac) :: []) ->
+ | (Coqast.VARG_NUMBER n) ::
+ ((Coqast.VARG_TACTIC tac) :: []) ->
(function () ->
let path = History.get_nth_open_path !current_proof_name n in
solve_nth n (Tacinterp.hide_interp tac);
@@ -543,29 +644,35 @@ let command_changes = [
Pfedit.mutate weak_undo_pftreestate;
traverse_to [])
| _ -> errorlabstrm "GOAL_CMD" (make_error_stream "GOAL_CMD")));
-
+
+(* Revient à l'état avant l'application de la n-ième tactique *)
("KILL_NODE",
(function
- | (VARG_NUMBER n) :: [] ->
+ | (Coqast.VARG_NUMBER n) :: [] ->
(function () ->
let ngoals = kill_proof_node n in
output_results_nl
(ctf_KilledMessage !global_request_id ngoals))
| _ -> errorlabstrm "KILL_NODE" (make_error_stream "KILL_NODE")));
+(* Annule toutes les commandes qui s'appliquent sur les sous-buts du
+ but auquel a été appliquée la n-ième tactique *)
("KILL_SUB_PROOF",
(function
- | [VARG_NUMBER n] ->
+ | [Coqast.VARG_NUMBER n] ->
(function () -> logical_kill n)
| _ -> errorlabstrm "KILL_SUB_PROOF" (make_error_stream "KILL_SUB_PROOF")));
("RESUME",
- (function [VARG_IDENTIFIER id] ->
+ (function [Coqast.VARG_IDENTIFIER id] ->
(fun () ->
let str = (string_of_id id) in
resume_proof id;
+(* Pcoq *)
current_proof_name := str)
+(**)
| _ -> errorlabstrm "RESUME" (make_error_stream "RESUME")));
+(* NoOp... *)
("BeginSilent",
(function
| [] ->
@@ -586,23 +693,27 @@ let command_changes = [
("ABORT",
(function
- | (VARG_IDENTIFIER id) :: [] ->
+ | (Coqast.VARG_IDENTIFIER id) :: [] ->
(function
() ->
delete_proof id;
+(* Pcoq *)
current_proof_name := "";
output_results_nl
(ctf_AbortedMessage !global_request_id (string_of_id id)))
+(**)
| [] ->
(function
() -> delete_current_proof ();
+(* Pcoq *)
current_proof_name := "";
output_results_nl
(ctf_AbortedMessage !global_request_id ""))
+(**)
| _ -> errorlabstrm "ABORT" (make_error_stream "ABORT")));
("SEARCH",
function
- (VARG_QUALID qid)::l ->
+ (Coqast.VARG_QUALID qid)::l ->
(fun () ->
ctv_SEARCH_LIST:=[];
let global_ref = Nametab.global dummy_loc qid in
@@ -614,7 +725,7 @@ let command_changes = [
("SearchRewrite",
function
- (VARG_CONSTR c)::l ->
+ (Coqast.VARG_CONSTR c)::l ->
(fun () ->
ctv_SEARCH_LIST:=[];
let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
@@ -626,7 +737,7 @@ let command_changes = [
("SearchPattern",
function
- (VARG_CONSTR c)::l ->
+ (Coqast.VARG_CONSTR c)::l ->
(fun () ->
ctv_SEARCH_LIST := [];
let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
@@ -638,7 +749,7 @@ let command_changes = [
("PrintId",
(function
- | [VARG_QUALID qid] ->
+ | [Coqast.VARG_QUALID qid] ->
(function () ->
let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in
output_results
@@ -648,7 +759,7 @@ let command_changes = [
("Check",
(function
- | (VARG_STRING kind) :: ((VARG_CONSTR c) :: g) ->
+ | (Coqast.VARG_STRING kind) :: ((Coqast.VARG_CONSTR c) :: g) ->
let evmap, env =
Vernacentries.get_current_context_of_args g in
let f =
@@ -664,7 +775,7 @@ let command_changes = [
("Eval",
(function
- | VARG_TACTIC_ARG(Redexp redexp):: VARG_CONSTR c :: g ->
+ | Coqast.VARG_TACTIC_ARG(Redexp redexp):: Coqast.VARG_CONSTR c :: g ->
let evmap, env = Vernacentries.get_current_context_of_args g in
let redfun =
ct_print_eval (Ctast.ast_to_ct c) (Tacred.reduction_of_redexp redexp env evmap) env in
@@ -675,7 +786,7 @@ let command_changes = [
("Centaur_Reset",
(function
- | (VARG_IDENTIFIER c) :: [] ->
+ | (Coqast.VARG_IDENTIFIER c) :: [] ->
if refining () then
output_results (ctf_AbortedAllMessage ()) None;
current_proof_name := "";
@@ -710,21 +821,25 @@ let command_changes = [
"Show_dad_rules" (make_error_stream "Show_dad_rules")));
("INSPECT",
(function
- | [VARG_NUMBER n] ->
+ | [Coqast.VARG_NUMBER n] ->
(function () -> inspect n)
| _ -> errorlabstrm "INSPECT" (make_error_stream "INSPECT")))
];;
-
+*)
+(*
let non_debug_changes = [
("SHOW",
(function
- | [VARG_NUMBER n] -> (function () -> show_nth n)
+ | [Coqast.VARG_NUMBER n] -> (function () -> show_nth n)
| _ -> errorlabstrm "SHOW" (make_error_stream "SHOW")))];;
+*)
+(* Moved to Vernacentries...
let command_creations = [
("Comments",
function l -> (fun () -> message ("Comments ok\n")));
+(* Dead code
("CommentsBold",
function l -> (fun () -> message ("CommentsBold ok\n")));
("Title",
@@ -734,28 +849,62 @@ let command_creations = [
("Note",
function l -> (fun () -> message ("Note ok\n")));
("NL",
- function l -> (fun () -> message ("Newline ok\n")))];;
-
+ function l -> (fun () -> message ("Newline ok\n")))
+*)
+];;
+*)
+
+TACTIC EXTEND Pbp
+| [ "Pbp" ident_opt(idopt) natural_list(nl) ] ->
+ [ if_pcoq pbp_tac_pcoq idopt nl ]
+END
+TACTIC EXTEND Blast
+| [ "Blast" ne_natural_list(nl) ] ->
+ [ if_pcoq blast_tac_pcoq nl ]
+END
+TACTIC EXTEND Dad
+| [ "Dad" natural_list(nl1) "to" natural_list(nl2) ] ->
+ [ if_pcoq dad_tac_pcoq nl1 nl2 ]
+END
+
+TACTIC EXTEND CtDebugTac
+| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ]
+END
+
+TACTIC EXTEND CtDebugTac2
+| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ]
+END
let start_pcoq_mode debug =
begin
+ pcoq_started := Some debug;
start_dad();
set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x)));
declare_in_coq();
+(*
add_tactic "PcoqPbp" pbp_tac_pcoq;
add_tactic "PcoqBlast" blast_tac_pcoq;
add_tactic "Dad" dad_tac_pcoq;
add_tactic "CtDebugTac" debug_tac2_pcoq;
add_tactic "CtDebugTac2" debug_tac2_pcoq;
+*)
(* The following ones are added to enable rich comments in pcoq *)
+(* TODO ...
add_tactic "Image" (fun _ -> tclIDTAC);
+*)
+(* "Comments" moved to Vernacentries, other obsolete ?
List.iter (fun (a,b) -> vinterp_add a b) command_creations;
+*)
+(* Now hooks in Vernacentries
List.iter (fun (a,b) -> overwriting_vinterp_add a b) command_changes;
if not debug then
List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes;
+*)
+ set_pcoq_hook pcoq_hook;
end;;
+(*
vinterp_add "START_PCOQ"
(function _ ->
(function () ->
@@ -773,4 +922,25 @@ vinterp_add "START_PCOQ_DEBUG"
set_start_marker "--->";
set_end_marker "<---";
raise Vernacinterp.ProtectedLoop));;
-
+*)
+let start_pcoq () =
+ start_pcoq_mode false;
+ set_acknowledge_command ctf_acknowledge_command;
+ set_start_marker "CENTAUR_RESERVED_TOKEN_start_command";
+ set_end_marker "CENTAUR_RESERVED_TOKEN_end_command"(*;
+ raise Vernacexpr.ProtectedLoop*)
+
+let start_pcoq_debug () =
+ start_pcoq_mode true;
+ set_acknowledge_command ctf_acknowledge_command;
+ set_start_marker "--->";
+ set_end_marker "<---"(*;
+ raise Vernacexpr.ProtectedLoop;;*)
+
+VERNAC COMMAND EXTEND StartPcoq
+ [ "Start" "Pcoq" "Mode" ] -> [ start_pcoq () ]
+END
+
+VERNAC COMMAND EXTEND StartPcoqDebug
+| [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ]
+END
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index ceb0f5953f..9d90782e4d 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -25,6 +25,10 @@ open Pp;;
open Paths;;
+open Genarg;;
+open Tacexpr;;
+open Rawterm;;
+
(* In a first approximation, drag-and-drop rules are like in CtCoq
1/ a pattern,
2,3/ Two paths: start and end positions,
@@ -37,7 +41,8 @@ open Paths;;
*)
-type dad_rule = Ctast.t * int list * int list * int * int list * Ctast.t;;
+type dad_rule =
+ Ctast.t * int list * int list * int * int list * raw_atomic_tactic_expr;;
(* This value will be used systematically when constructing objects of
type Ctast.t, the value is stupid and meaningless, but it is needed
@@ -65,13 +70,20 @@ let rec get_subterm (depth:int) (path: int list) (constr:constr) =
let map_subst (env :env)
(subst:(int * Term.constr) list) =
let rec map_subst_aux = function
- Node(_, "META", [Num(_, i)]) ->
+ Coqast.Node(_, "META", [Coqast.Num(_, i)]) ->
let constr = List.assoc i subst in
- Ctast.ast_to_ct (ast_of_constr false env constr)
- | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l)
+ ast_of_constr false env constr
+ | Coqast.Node(loc, s, l) -> Coqast.Node(loc, s, List.map map_subst_aux l)
| ast -> ast in
map_subst_aux;;
+let map_subst_tactic env subst = function
+ | TacExtend ("Rewrite" as x,[b;cbl]) ->
+ let c,bl = out_gen rawwit_constr_with_bindings cbl in
+ assert (bl = NoBindings);
+ let c = (map_subst env subst c,NoBindings) in
+ TacExtend (x,[b;in_gen rawwit_constr_with_bindings c])
+ | _ -> failwith "map_subst_tactic: unsupported tactic"
(* This function is really the one that is important. *)
let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
@@ -93,7 +105,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
(ct_to_ast pat) in
let subst = matches constr_pat term_to_match in
if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then
- map_subst env subst cmd
+ TacAtom (zz, map_subst_tactic env subst cmd)
else
failwith "internal"
with
@@ -103,7 +115,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
let dad_rule_list = ref ([]: (string * dad_rule) list);;
-
+(*
(* \\ This function is also used in pbp. *)
let rec tactic_args_to_ints = function
[] -> []
@@ -130,6 +142,12 @@ let dad_tac display_function = function
(find_cmd (!dad_rule_list) (pf_env g)
(pf_concl g) p_a p1prime p2prime));
tclIDTAC g);;
+*)
+let dad_tac display_function p1 p2 g =
+ let (p_a, p1prime, p2prime) = decompose_path (p1,p2) in
+ (display_function
+ (find_cmd (!dad_rule_list) (pf_env g) (pf_concl g) p_a p1prime p2prime));
+ tclIDTAC g;;
(* Now we enter dad rule list management. *)
@@ -233,34 +251,40 @@ let rec sort_list = function
| a::l -> add_in_list_sorting a (sort_list l);;
let mk_dad_meta n = Node(zz,"META",[Num(zz, n)]);;
-let mk_rewrite1 ast =
- Node(zz,"TACTICLIST",
- [Node(zz,"RewriteLR",
- [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);;
-
-let mk_rewrite2 ast =
- Node(zz,"TACTICLIST",
- [Node(zz,"RewriteRL",
- [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);;
-
-
-
-let start_dad () =
-vinterp_add "AddDadRule"
- (function
- | [VARG_STRING name; VARG_CONSTR pat; VARG_NUMBERLIST p1;
- VARG_NUMBERLIST p2; VARG_TACTIC com] ->
- (function () ->
- let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
- (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
- | _ -> errorlabstrm "AddDadRule1" (str "AddDadRule2"));
+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
+ TacExtend ("Rewrite",[b;cb])
+
+open Vernacexpr
+
+let dad_status = ref false;;
+
+let start_dad () = dad_status := true;;
+
+let add_dad_rule_fn name pat p1 p2 tac =
+ let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
+ add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr tac;;
+
+(* To be parsed by camlp4
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+VERNAC COMMAND EXTEND AddDadRule
+ [ "Add" "Dad" "Rule" string(name) constr(pat)
+ "From" natural_list(p1) "To" natural_list(p2) tactic(tac) ] ->
+ [ add_dad_rule_fn name pat p1 p2 tac ]
+END
+
+*)
+
add_dad_rule "distributivity-inv"
(Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
[2; 2]
[2; 1]
1
[2]
-(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "distributivity1-r"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
@@ -268,7 +292,7 @@ add_dad_rule "distributivity1-r"
[]
0
[]
-(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "distributivity1-l"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
@@ -276,7 +300,7 @@ add_dad_rule "distributivity1-l"
[]
0
[]
-(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "associativity"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
@@ -284,7 +308,7 @@ add_dad_rule "associativity"
[]
0
[]
-(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "minus-identity-lr"
(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])]))
@@ -292,7 +316,7 @@ add_dad_rule "minus-identity-lr"
[2; 2]
1
[2]
-(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])]));
+(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])));
add_dad_rule "minus-identity-rl"
(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])]))
@@ -300,7 +324,7 @@ add_dad_rule "minus-identity-rl"
[2; 1]
1
[2]
-(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])]));
+(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])));
add_dad_rule "plus-sym-rl"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])]))
@@ -308,7 +332,7 @@ add_dad_rule "plus-sym-rl"
[2; 1]
1
[2]
-(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "plus-sym-lr"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])]))
@@ -316,7 +340,7 @@ add_dad_rule "plus-sym-lr"
[2; 2]
1
[2]
-(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "absorb-0-r-rl"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")]))
@@ -324,7 +348,7 @@ add_dad_rule "absorb-0-r-rl"
[1]
0
[]
-(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])]));
+(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])));
add_dad_rule "absorb-0-r-lr"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")]))
@@ -332,7 +356,7 @@ add_dad_rule "absorb-0-r-lr"
[2; 2]
0
[]
-(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])]));
+(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])));
add_dad_rule "plus-permute-lr"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
@@ -340,7 +364,7 @@ add_dad_rule "plus-permute-lr"
[2; 2; 2; 1]
1
[2]
-(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));
+(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
add_dad_rule "plus-permute-rl"
(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
@@ -348,7 +372,7 @@ add_dad_rule "plus-permute-rl"
[2; 1]
1
[2]
-(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));;
+(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));;
vinterp_add "StartDad"
(function
diff --git a/contrib/interface/dad.mli b/contrib/interface/dad.mli
index 9f8f7354b2..dc2b2734cd 100644
--- a/contrib/interface/dad.mli
+++ b/contrib/interface/dad.mli
@@ -4,7 +4,7 @@ open Tacmach;;
val dad_rule_names : unit -> string list;;
val start_dad : unit -> unit;;
-val dad_tac : (Ctast.t -> 'a) -> tactic_arg list -> goal sigma ->
+val dad_tac : (Tacexpr.raw_tactic_expr -> 'a) -> int list -> int list -> goal sigma ->
goal list sigma * validation;;
val add_dad_rule : string -> Ctast.t -> (int list) -> (int list) ->
- int -> (int list) -> Ctast.t -> unit;;
+ int -> (int list) -> Tacexpr.raw_atomic_tactic_expr -> unit;;
diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml4
index be469108fb..b4db228030 100644
--- a/contrib/interface/debug_tac.ml
+++ b/contrib/interface/debug_tac.ml4
@@ -1,11 +1,16 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
open Ast;;
open Coqast;;
open Tacmach;;
+open Tacticals;;
open Proof_trees;;
open Pp;;
-open Printer;;
+open Pptactic;;
open Util;;
open Proof_type;;
+open Tacexpr;;
+open Genarg;;
(* Compacting and uncompacting proof commands *)
@@ -67,9 +72,14 @@ 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;;
let rec collect_status = function
Report_node(true,_,_)::tl -> collect_status tl
@@ -105,7 +115,8 @@ let count_subgoals2
card_holder := Recursive_fail(List.hd !new_report_holder));
result;;
-let rec local_interp : Coqast.t -> report_holder -> tactic = function
+let rec local_interp : raw_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) ->
@@ -123,7 +134,21 @@ let rec local_interp : Coqast.t -> report_holder -> tactic = function
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) ->
+ (fun report_holder -> checked_then report_holder a b)
+ | t ->
+ (fun report_holder g ->
+ try
+ let (gls, _) as result = Tacinterp.interp t 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))
+
(* This tactical receives a tactic and a list of tactics as argument.
It applies the first tactic and then maps the list of tactics to
@@ -137,7 +162,7 @@ let rec local_interp : Coqast.t -> report_holder -> tactic = function
- In case of success of the first tactic, but count mismatch, then
Mismatch n is added to the report holder. *)
-and checked_thens: report_holder -> Coqast.t -> Coqast.t list -> tactic =
+and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> tactic =
(fun report_holder t1 l g ->
let flag = ref true in
let traceable_t1 = traceable t1 in
@@ -192,7 +217,7 @@ and checked_thens: report_holder -> Coqast.t -> Coqast.t list -> tactic =
reporting information about the success of all tactics in the report
holder. It never fails. *)
-and checked_then: report_holder -> Coqast.t -> Coqast.t -> tactic =
+and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic =
(fun report_holder t1 t2 g ->
let flag = ref true in
let card_holder = ref Fail in
@@ -238,23 +263,38 @@ and checked_then: report_holder -> Coqast.t -> Coqast.t -> tactic =
by the list of integers given as extra arguments.
*)
-let on_then : tactic_arg list -> tactic = function
- (Tacexp t1)::(Tacexp t2)::l ->
+let on_then = function [t1;t2;l] ->
+ let t1 = out_gen wit_tactic t1 in
+ let t2 = out_gen wit_tactic t2 in
+ let l = out_gen (wit_list0 wit_int) l in
tclTHEN_i (Tacinterp.interp t1)
(fun i ->
- if List.mem (Integer (i + 1)) l then
+ if List.mem (i + 1) l then
(Tacinterp.interp t2)
else
tclIDTAC)
- | _ -> error "bad arguments for on_then";;
+ | _ -> 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 l = in_gen (wit_list0 rawwit_int) selected_indices in
+ TacAtom (dummy_loc, TacExtend ("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",
@@ -269,7 +309,15 @@ let rec expand_tactic = function
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)]) ->
@@ -299,6 +347,38 @@ let rec reconstruct_success_tac ast =
"this error case should not happen on an unknown tactic"
(str "error in reconstruction with " ++ fnl () ++
(gentacpr ast)));;
+*)
+let rec reconstruct_success_tac tac =
+ match tac with
+ TacThens (a,l) ->
+ (function
+ Report_node(true, n, l) -> tac
+ | Report_node(false, n, rl) ->
+ TacThens (a,List.map2 reconstruct_success_tac l rl)
+ | Failed n -> TacId
+ | Tree_fail r -> reconstruct_success_tac a r
+ | Mismatch (n,p) -> a)
+ | TacThen (a,b) ->
+ (function
+ Report_node(true, n, l) -> tac
+ | Report_node(false, n, rl) ->
+ let selected_indices = select_success 1 rl in
+ TacAtom (Ast.dummy_loc,TacExtend ("OnThen",
+ [in_gen rawwit_tactic a;
+ in_gen rawwit_tactic b;
+ in_gen (wit_list0 rawwit_int) selected_indices]))
+ | 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
+ | _ ->
+ errorlabstrm
+ "this error case should not happen on an unknown tactic"
+ (str "error in reconstruction with " ++ fnl () ++
+ (pr_raw_tactic tac)));;
let rec path_to_first_error = function
@@ -311,6 +391,7 @@ 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
@@ -323,32 +404,38 @@ and flatten_then = function
| Node(_, "OnThen", t1::t2::l) ->
ope("OnThen", (flatten_then t1)::(flatten_then t2)::l)
| ast -> ast;;
+*)
let debug_tac = function
[(Tacexp ast)] ->
(fun g ->
let report = ref ([] : report_tree list) in
let result = local_interp ast report g in
- let clean_ast = expand_tactic ast in
+ let clean_ast = (* expand_tactic *) ast in
let report_tree =
try List.hd !report with
Failure "hd" -> (msgnl (str "report is empty"); Failed 1) in
let success_tac =
reconstruct_success_tac clean_ast report_tree in
- let compact_success_tac =
- flatten_then success_tac in
+ let compact_success_tac = (* flatten_then *) success_tac in
msgnl (fnl () ++
str "========= Successful tactic =============" ++
fnl () ++
- gentacpr compact_success_tac ++ fnl () ++
+ pr_raw_tactic compact_success_tac ++ fnl () ++
str "========= End of successful tactic ============");
result)
| _ -> error "wrong arguments for debug_tac";;
+(* TODO ... used ?
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 ->
@@ -362,15 +449,24 @@ let rec clean_path p ast l =
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 ->
+ fst::(clean_path (if fst = 1 then a else b) tl)
+ | TacThens (a,l), 1::tl ->
+ 1::(clean_path a tl)
+ | TacThens (a,tacs), 2::fst::tl ->
+ 2::fst::(clean_path (List.nth tacs (fst - 1)) tl)
+ | _, [] -> []
+ | _, _ -> failwith "this case should not happen in clean_path";;
let rec report_error
- : Coqast.t -> goal sigma option ref -> Coqast.t ref -> int list ref ->
+ : raw_tactic_expr -> goal sigma option ref -> raw_tactic_expr ref -> int list ref ->
int list -> tactic =
- fun ast the_goal the_ast returned_path path ->
- match ast with
- Node(loc1, "TACTICLIST", [a;(Node(loc2, "TACLIST", l)) as tail]) ->
+ fun tac the_goal the_ast returned_path path ->
+ match tac with
+ TacThens (a,l) ->
let the_card_holder = ref Fail in
let the_flag = ref false in
let the_exn = ref (Failure "") in
@@ -392,10 +488,10 @@ let rec report_error
else
(match !the_card_holder with
Fail ->
- the_ast := ope("TACTICLIST", [!the_ast; tail]);
+ the_ast := TacThens (!the_ast, l);
raise !the_exn
| Goals_mismatch p ->
- the_ast := ast;
+ the_ast := tac;
returned_path := path;
error ("Wrong number of tactics: expected " ^
(string_of_int (List.length l)) ^ " received " ^
@@ -406,10 +502,7 @@ let rec report_error
| t::tl -> (report_error t the_goal the_ast returned_path (n::2::path))::
(fold_num (n + 1) tl) in
fold_num 1 l)
- | Node(_, "TACTICLIST", a::((Node(_, "TACLIST", l)) as b)::c::tl) ->
- report_error(ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
- the_goal the_ast returned_path path
- | Node(_, "TACTICLIST", [a;b]) ->
+ | TacThen (a,b) ->
let the_count = ref 1 in
tclTHEN
(fun g ->
@@ -417,7 +510,7 @@ let rec report_error
report_error a the_goal the_ast returned_path (1::path) g
with
e ->
- (the_ast := ope("TACTICLIST", [!the_ast; b]);
+ (the_ast := TacThen (!the_ast, b);
raise e))
(fun g ->
try
@@ -430,18 +523,15 @@ let rec report_error
if !the_count > 1 then
msgnl
(str "in branch no " ++ int !the_count ++
- str " after tactic " ++ gentacpr a);
+ str " after tactic " ++ pr_raw_tactic a);
raise e)
- | Node(_, "TACTICLIST", a::b::c::tl) ->
- report_error (ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
- the_goal the_ast returned_path path
- | ast ->
+ | tac ->
(fun g ->
try
- Tacinterp.interp ast g
+ Tacinterp.interp tac g
with
e ->
- (the_ast := ast;
+ (the_ast := tac;
the_goal := Some g;
returned_path := path;
raise e));;
@@ -450,14 +540,13 @@ let strip_some = function
Some n -> n
| None -> failwith "No optional value";;
-let descr_first_error = function
- [(Tacexp ast)] ->
+let descr_first_error tac =
(fun g ->
let the_goal = ref (None : goal sigma option) in
- let the_ast = ref ast in
+ let the_ast = ref tac in
let the_path = ref ([] : int list) in
try
- let result = report_error ast the_goal the_ast the_path [] g in
+ let result = report_error tac the_goal the_ast the_path [] g in
msgnl (str "no Error here");
result
with
@@ -467,8 +556,15 @@ let descr_first_error = function
fnl () ++ str "on goal" ++ fnl () ++
pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
str "faulty tactic is" ++ fnl () ++ fnl () ++
- gentacpr (flatten_then !the_ast) ++ fnl ());
+ pr_raw_tactic ((*flatten_then*) !the_ast) ++ fnl ());
tclIDTAC g))
- | _ -> error "wrong arguments for descr_first_error";;
+(* TODO ... used ??
add_tactic "DebugTac2" descr_first_error;;
+*)
+
+(*
+TACTIC EXTEND DebugTac2
+ [ ??? ] -> [ descr_first_error tac ]
+END
+*)
diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli
index a582b029e4..05cef23aa7 100644
--- a/contrib/interface/debug_tac.mli
+++ b/contrib/interface/debug_tac.mli
@@ -1,6 +1,6 @@
-val report_error : Coqast.t ->
+val report_error : Tacexpr.raw_tactic_expr ->
Proof_type.goal Proof_type.sigma option ref ->
- Coqast.t ref -> int list ref -> int list -> Tacmach.tactic;;
+ Tacexpr.raw_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;;
-val clean_path : int -> Coqast.t -> int list -> int list;;
+val clean_path : Tacexpr.raw_tactic_expr -> int list -> int list;;
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index a7d5644f0a..0f3dcdf67e 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -17,7 +17,7 @@ open Util;;
open Pp;;
open Declare;;
open Nametab
-
+open Vernacexpr;;
(* This function converts the parameter binders of an inductive definition,
in particular you have to be careful to handle each element in the
@@ -26,9 +26,7 @@ open Nametab
let convert_env =
let convert_binder env (na, _, c) =
match na with
- | Name id ->
- ope("BINDER",
- [ast_of_constr true env c;nvar id])
+ | Name id -> (id, ast_of_constr true env c)
| Anonymous -> failwith "anomaly: Anonymous variables in inductives" in
let rec cvrec env = function
[] -> []
@@ -56,9 +54,9 @@ let impl_args_to_string = function
let implicit_args_id_to_ast_list id l ast_list =
(match impl_args_to_string l with
None -> ast_list
- | Some(s) -> (string ("For " ^ (string_of_id id)))::
- (string s)::
- ast_list);;
+ | Some(s) -> CommentString ("For " ^ (string_of_id id))::
+ CommentString s::
+ ast_list);;
(* This function construct an ast to enumerate the implicit positions for an
inductive type and its constructors. It is obtained directly from
@@ -66,7 +64,7 @@ let implicit_args_id_to_ast_list id l ast_list =
let implicit_args_to_ast_list sp mipv =
let implicit_args_descriptions =
- let ast_list = ref ([]:Coqast.t list) in
+ let ast_list = ref [] in
(Array.iteri
(fun i mip ->
let imps = inductive_implicits_list(sp, i) in
@@ -82,7 +80,7 @@ let implicit_args_to_ast_list sp mipv =
!ast_list) in
match implicit_args_descriptions with
[] -> []
- | _ -> [ope("COMMENT", List.rev implicit_args_descriptions)];;
+ | _ -> [VernacComments (List.rev implicit_args_descriptions)];;
let convert_qualid qid =
let d, id = Nametab.repr_qualid qid in
@@ -97,10 +95,11 @@ let convert_qualid qid =
let convert_constructors envpar names types =
let array_idC =
array_map2
- (fun n t -> ope("BINDER",
- [ast_of_constr true envpar t; nvar n]))
+ (fun n t ->
+ let coercion_flag = false (* arbitrary *) in
+ (n, coercion_flag, ast_of_constr true envpar t))
names types in
- Node((0,0), "BINDERLIST", Array.to_list array_idC);;
+ Array.to_list array_idC;;
(* this function converts one inductive type in a possibly multiple inductive
definition *)
@@ -109,11 +108,11 @@ let convert_one_inductive sp tyi =
let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
let env = Global.env () in
let envpar = push_rel_context params env in
- ope("VERNACARGLIST",
- [convert_qualid (Nametab.shortest_qualid_of_global env (IndRef (sp, tyi)));
- ope("CONSTR", [ast_of_constr true envpar arity]);
- ope("BINDERLIST", convert_env(List.rev params));
- convert_constructors envpar cstrnames cstrtypes]);;
+ let sp = sp_of_global env (IndRef (sp, tyi)) in
+ (basename sp,
+ convert_env(List.rev params),
+ (ast_of_constr true envpar arity),
+ convert_constructors envpar cstrnames cstrtypes);;
(* This function converts a Mutual inductive definition to a Coqast.t.
It is obtained directly from print_mutual in pretty.ml. However, all
@@ -121,22 +120,21 @@ let convert_one_inductive sp tyi =
let mutual_to_ast_list sp mib =
let mipv = (Global.lookup_mind sp).mind_packets in
- let _, ast_list =
+ let _, l =
Array.fold_right
(fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
- (ope("MUTUALINDUCTIVE",
- [string (if mib.mind_finite then "Inductive" else "CoInductive");
- ope("VERNACARGLIST", ast_list)])::
- (implicit_args_to_ast_list sp mipv));;
+ VernacInductive (mib.mind_finite, l)
+ :: (implicit_args_to_ast_list sp mipv);;
let constr_to_ast v =
ast_of_constr true (Global.env()) v;;
let implicits_to_ast_list implicits =
- (match (impl_args_to_string implicits) with
- None -> []
- | Some s -> [ope("COMMENT", [string s])]);;
+ match (impl_args_to_string implicits) with
+ | None -> []
+ | Some s -> [VernacComments [CommentString s]];;
+(*
let make_variable_ast name typ implicits =
(ope("VARIABLE",
[string "VARIABLE";
@@ -145,7 +143,13 @@ let make_variable_ast name typ implicits =
[(constr_to_ast (body_of_type typ));
nvar name])])]))::(implicits_to_ast_list implicits)
;;
+*)
+let make_variable_ast name typ implicits =
+ (VernacAssumption
+ (AssumptionVariable, [name, constr_to_ast (body_of_type typ)]))
+ ::(implicits_to_ast_list implicits);;
+(*
let make_definition_ast name c typ implicits =
(ope("DEFINITION",
[string "DEFINITION";
@@ -155,6 +159,12 @@ let make_definition_ast name c typ implicits =
[(constr_to_ast c);
(constr_to_ast (body_of_type typ))])])]))::
(implicits_to_ast_list implicits);;
+*)
+let make_definition_ast name c typ implicits =
+ VernacDefinition (Definition, name, None,
+ (ope("CAST", [(constr_to_ast c);(constr_to_ast (body_of_type typ))])),
+ None, (fun _ _ -> ()))
+ ::(implicits_to_ast_list implicits);;
(* This function is inspired by print_constant *)
let constant_to_ast_list sp =
@@ -238,5 +248,5 @@ let name_to_ast (qid:Nametab.qualid) =
(Nametab.pr_qualid qid ++
spc () ++ str "not a defined object")
in
- ope("vernac_list", l);;
+ VernacList (List.map (fun x -> (dummy_loc,x)) l)
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 894b273926..4a68e0134f 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1,2 +1,2 @@
-val name_to_ast : Nametab.qualid -> Coqast.t;;
+val name_to_ast : Nametab.qualid -> Vernacexpr.vernac_expr;;
val convert_qualid : Nametab.qualid -> Coqast.t;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 389fa8cda8..5bce60f223 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -18,6 +18,8 @@ open Line_parser;;
open Pcoq;;
+open Vernacexpr;;
+
type parsed_tree =
| P_cl of ct_COMMAND_LIST
| P_c of ct_COMMAND
@@ -55,6 +57,7 @@ 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 *)
@@ -62,23 +65,29 @@ let try_require_module import specif names =
try Library.require_module
(if specif = "UNSPECIFIED" then None
else Some (specif = "SPECIFICATION"))
- (List.map (fun name -> Nametab.make_short_qualid (Names.id_of_string name))
+ (List.map
+ (fun name ->
+ (dummy_loc,Nametab.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")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
+ 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))) ->
@@ -92,6 +101,23 @@ let execute_when_necessary ast =
((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
+ | VernacRequire (_,_,l) ->
+ (try
+ Vernacentries.interp v
+ with _ ->
+ let l=prlist_with_sep spc (fun (_,qid) -> Nametab.pr_qualid qid) l in
+ msgnl (str "Reinterning of " ++ l ++ str " failed"))
+ | VernacRequireFrom (_,_,name,_) ->
+ (try
+ Vernacentries.interp v
+ with _ ->
+ msgnl (str "Reinterning of " ++ Nameops.pr_id name ++ str " failed"))
+ | _ -> ()); v;;
let parse_to_dot =
let rec dot st = match Stream.next st with
@@ -106,13 +132,13 @@ let rec discard_to_dot stream =
let rec decompose_string_aux s n =
try let index = String.index_from s n '\n' in
- (Ctast.str (String.sub s n (index - n)))::
+ (String.sub s n (index - n))::
(decompose_string_aux s (index + 1))
- with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];;
+ with Not_found -> [String.sub s n ((String.length s) - n)];;
let decompose_string s n =
match decompose_string_aux s n with
- (Ctast.Str(_,""))::tl -> tl
+ ""::tl -> tl
| a -> a;;
let make_string_list file_chan fst_pos snd_pos =
@@ -161,13 +187,21 @@ let rec get_substring_list string_list fst_pos snd_pos =
(* When parsing a list of commands, we try to recover error messages for
each individual command. *)
+type parse_result =
+ | ParseOK of Vernacexpr.vernac_expr located option
+ | ParseError of string * string list
+
+let embed_string s =
+ CT_coerce_STRING_OPT_to_VARG (CT_coerce_STRING_to_STRING_OPT (CT_string s))
+
+let make_parse_error_item s l =
+ CT_user_vernac (CT_ident s, CT_varg_list (List.map embed_string l))
+
let parse_command_list reqid stream string_list =
let rec parse_whole_stream () =
let this_pos = Stream.count stream in
let first_ast =
- try option_app
- Ctast.ast_to_ct (Gram.Entry.parse
- Pcoq.main_entry (Gram.parsable stream))
+ try ParseOK (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
with
| (Stdpp.Exc_located(l, Stream.Error txt)) as e ->
begin
@@ -176,31 +210,48 @@ 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))))
- with End_of_file -> None
+*)
+ ParseError ("PARSE_ERROR",
+ get_substring_list string_list this_pos
+ (Stream.count stream))
+ with End_of_file -> ParseOK None
end
| 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 ("PARSE_ERROR2",
+ get_substring_list string_list this_pos (Stream.count stream))
end in
match first_ast with
- | Some ast ->
+ | ParseOK (Some (loc,ast)) ->
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()
- | None -> [] in
+*)
+ make_parse_error_item "PARSING_ERROR2"
+ (get_substring_list string_list this_pos
+ (Stream.count stream)))::parse_whole_stream()
+ | ParseOK None -> []
+ | ParseError (s,l) ->
+ (make_parse_error_item s l)::parse_whole_stream()
+ in
match parse_whole_stream () with
| first_one::tail -> (P_cl (CT_command_list(first_one, tail)))
| [] -> raise (UserError ("parse_string", (str "empty text.")));;
@@ -219,25 +270,25 @@ let parse_string_action reqid phylum char_stream string_list =
P_c
(xlate_vernac
(execute_when_necessary
- (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream)))))
+ (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream))))
| "TACTIC_COM" ->
P_t
- (xlate_tactic (Ctast.ast_to_ct(Gram.Entry.parse Pcoq.Tactic.tactic_eoi
- (Gram.parsable char_stream))))
+ (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi
+ (Gram.parsable char_stream)))
| "FORMULA" ->
P_f
(xlate_formula
(Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream))))
- | "ID" -> P_id (xlate_id
- (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.ident
- (Gram.parsable char_stream))))
+ | "ID" -> P_id (xlate_ident
+ (Gram.Entry.parse Pcoq.Prim.ident
+ (Gram.parsable char_stream)))
| "STRING" ->
P_s
- (xlate_string (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.string
- (Gram.parsable char_stream))))
+ (CT_string (Gram.Entry.parse Pcoq.Prim.string
+ (Gram.parsable char_stream)))
| "INT" ->
- P_i (xlate_int (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.number
- (Gram.parsable char_stream))))
+ P_i (CT_int (Gram.Entry.parse Pcoq.Prim.natural
+ (Gram.parsable char_stream)))
| _ -> error "parse_string_action : bad phylum" in
print_parse_results reqid msg
with
@@ -273,10 +324,7 @@ let parse_file_action reqid file_name =
let this_pos = Stream.count stream in
match
try
- let this_ast =
- option_app Ctast.ast_to_ct
- (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in
- this_ast
+ ParseOK(Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
with
| Stdpp.Exc_located(l,Stream.Error txt) ->
msgnl (ctf_SyntaxWarningMessage reqid
@@ -287,21 +335,21 @@ let parse_file_action reqid file_name =
(try
begin
discard_to_dot ();
- Some( Node(l, "PARSING_ERROR",
+ ParseError ("PARSING_ERROR",
(make_string_list file_chan_err this_pos
- (Stream.count stream))))
+ (Stream.count stream)))
end
- with End_of_file -> None)
+ with End_of_file -> ParseOK None)
| e ->
begin
Gram.Entry.parse parse_to_dot (Gram.parsable stream);
- Some(Node((0,0), "PARSING_ERROR2",
- (make_string_list file_chan this_pos
- (Stream.count stream))))
+ ParseError ("PARSING_ERROR2",
+ (make_string_list file_chan this_pos
+ (Stream.count stream)))
end
with
- | Some ast ->
+ | ParseOK (Some (_,ast)) ->
let ast0=(execute_when_necessary ast) in
let term =
(try xlate_vernac ast
@@ -311,12 +359,13 @@ let parse_file_action reqid file_name =
" " ^
(string_of_int (Stream.count stream)) ^
"\n");
- xlate_vernac
- (Node((0,0), "PARSING_ERROR2",
- (make_string_list file_chan_err this_pos
- (Stream.count stream))))) in
+ make_parse_error_item "PARSING_ERROR2"
+ (make_string_list file_chan_err this_pos
+ (Stream.count stream))) in
term::parse_whole_file ()
- | None -> [] in
+ | ParseOK None -> []
+ | ParseError (s,l) ->
+ (make_parse_error_item s l)::parse_whole_file () in
parse_whole_file () with
| first_one :: tail ->
print_parse_results reqid
@@ -379,9 +428,9 @@ let load_syntax_action reqid module_name =
msg (str "loading " ++ str module_name ++ str "... ");
try
(let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
- read_module qid;
+ read_module (dummy_loc,qid);
msg (str "opening... ");
- import_module false qid;
+ import_module false (dummy_loc,qid);
msgnl (str "done" ++ fnl ());
())
with
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 2e92dd7c9d..5dd9d071b5 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -14,6 +14,7 @@ open Environ;;
open Proof_trees;;
open Proof_type;;
open Tacmach;;
+open Tacexpr;;
open Typing;;
open Pp;;
@@ -24,37 +25,79 @@ let get_hyp_by_name g name =
let env = pf_env g in
try (let judgment =
Pretyping.understand_judgment
- evd env (RVar(dummy_loc, id_of_string name)) in
+ evd env (RVar(dummy_loc, 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 parse_ast = Pcoq.parse_string Pcoq.Constr.constr in
- let parse s = Astterm.interp_constr Evd.empty (Global.env())
- (parse_ast s) in
- ("cste",type_of (Global.env()) Evd.empty (parse name)))
+ with _ -> (let ast = Termast.ast_of_qualid (Nametab.make_short_qualid name)in
+ let c = Astterm.interp_constr evd env ast in
+ ("cste",type_of (Global.env()) Evd.empty c))
;;
+type pbp_atom =
+ | PbpTryAssumption of identifier option
+ | PbpTryClear of identifier list
+ | PbpGeneralize of identifier * identifier list
+ | PbpLApply of identifier (* = CutAndApply *)
+ | PbpIntros of identifier list
+ | PbpSplit
+ (* Existential *)
+ | PbpExists of identifier
+ (* Or *)
+ | PbpLeft
+ | PbpRight
+ (* Not *)
+ | PbpReduce
+ (* Head *)
+ | PbpApply of identifier
+ | PbpElim of identifier * identifier list;;
+
+(* Invariant: In PbpThens ([a1;...;an],[t1;...;tp]), all tactics
+ [a1]..[an-1] are atomic (or try of an atomic) tactic and produce
+ exactly one goal, and [an] produces exactly p subgoals
+
+ In [PbpThen [a1;..an]], all tactics are (try of) atomic tactics and
+ produces exactly one subgoal, except the last one which may complete the
+ goal
+
+ Convention: [PbpThen []] is Idtac and [PbpThen t] is a coercion
+ from atomic to composed tactic
+*)
+
+type pbp_sequence =
+ | PbpThens of pbp_atom list * pbp_sequence list
+ | PbpThen of pbp_atom list
+
+(* This flattens sequences of tactics producing just one subgoal *)
+let chain_tactics tl1 = function
+ | PbpThens (tl2, tl3) -> PbpThens (tl1@tl2, tl3)
+ | PbpThen tl2 -> PbpThen (tl1@tl2)
+
type pbp_rule = (identifier list *
- string list *
+ identifier list *
bool *
- string option *
+ identifier option *
(types, constr) kind_of_term *
int list *
(identifier list ->
- string list ->
+ identifier list ->
bool ->
- string option -> (types, constr) kind_of_term -> int list -> Ctast.t)) ->
- Ctast.t option;;
+ identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
+ pbp_sequence option;;
let zz = (0,0);;
+(*
let make_named_intro s =
Node(zz, "Intros",
[Node(zz,"INTROPATTERN",
[Node(zz,"LISTPATTERN",
[Node(zz, "IDENTIFIER",
[Nvar(zz, s)])])])]);;
+*)
+let make_named_intro id = PbpIntros [id]
+(*
let get_name_from_intro = function
Node(a, "Intros",
[Node(b,"INTROPATTERN",
@@ -63,21 +106,24 @@ let get_name_from_intro = function
[Nvar(e, s)])])])]) ->
Some s
| _ -> None;;
-
+*)
+(*
let make_clears = function
[] -> Node(zz, "Idtac",[])
| str_list ->
Node(zz, "TRY", [Node(zz,"Clear",
[Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)])
]);;
+*)
+let make_clears str_list = PbpThen [PbpTryClear str_list]
let add_clear_names_if_necessary tactic clear_names =
match clear_names with
[] -> tactic
- | l -> Node(zz, "TACTICLIST", [make_clears l; tactic]);;
+ | l -> chain_tactics [PbpTryClear l] tactic;;
let make_final_cmd f optname clear_names constr path =
- let tactic = f optname constr path in
+(* let tactic = f optname constr path in*)
add_clear_names_if_necessary (f optname constr path) clear_names;;
let (rem_cast:pbp_rule) = function
@@ -94,18 +140,17 @@ let (forall_intro: pbp_rule) = function
(2::path),
f) ->
let x' = next_global_ident_away x avoid in
- Some(Node(zz, "TACTICLIST",
- [make_named_intro (string_of_id x'); f (x'::avoid)
- clear_names clear_flag None (kind_of_term body) path]))
+ Some(chain_tactics [make_named_intro x']
+ (f (x'::avoid)
+ clear_names clear_flag None (kind_of_term body) path))
| _ -> None;;
let (imply_intro2: pbp_rule) = function
avoid, clear_names,
clear_flag, None, Prod(Anonymous, _, body), 2::path, f ->
let h' = next_global_ident_away (id_of_string "H") avoid in
- Some(Node(zz, "TACTICLIST",
- [make_named_intro (string_of_id h');
- f (h'::avoid) clear_names clear_flag None (kind_of_term body) path]))
+ Some(chain_tactics [make_named_intro h']
+ (f (h'::avoid) clear_names clear_flag None (kind_of_term body) path))
| _ -> None;;
@@ -113,72 +158,90 @@ let (imply_intro1: pbp_rule) = function
avoid, clear_names,
clear_flag, None, Prod(Anonymous, prem, body), 1::path, f ->
let h' = next_global_ident_away (id_of_string "H") avoid in
- let str_h' = (string_of_id h') in
- Some(Node(zz, "TACTICLIST",
- [make_named_intro str_h';
- f (h'::avoid) clear_names clear_flag (Some str_h')
- (kind_of_term prem) path]))
+ let str_h' = h' in
+ Some(chain_tactics [make_named_intro str_h']
+ (f (h'::avoid) clear_names clear_flag (Some str_h')
+ (kind_of_term prem) path))
| _ -> None;;
+let make_pbp_pattern x =
+ Coqast.Node(zz,"APPLIST",
+ [Coqast.Nvar (zz, id_of_string "PBP_META");
+ Coqast.Nvar (zz, id_of_string ("Value_for_" ^ (string_of_id x)))])
+
+let rec make_then = function
+ | [] -> TacId
+ | [t] -> t
+ | t1::t2::l -> make_then (TacThen (t1,t2)::l)
+
+let make_pbp_atomic_tactic = function
+ | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
+ | PbpTryAssumption (Some a) ->
+ TacTry (TacAtom (zz, TacExact (Coqast.Nvar (zz,a))))
+ | PbpExists x ->
+ TacAtom (zz, TacSplit (ImplicitBindings [make_pbp_pattern x]))
+ | PbpGeneralize (h,args) ->
+ let l = Coqast.Nvar (zz, h)::List.map make_pbp_pattern args in
+ TacAtom (zz, TacGeneralize [Coqast.Node (zz, "APPLIST", l)])
+ | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
+ | PbpRight -> TacAtom (zz, TacRight NoBindings)
+ | PbpReduce -> TacAtom (zz, TacReduce (Red false, []))
+ | PbpIntros l ->
+ let l = List.map (fun id -> IntroIdentifier id) l in
+ TacAtom (zz, TacIntroPattern l)
+ | PbpLApply h -> TacAtom (zz, TacLApply (Coqast.Nvar (zz, h)))
+ | PbpApply h -> TacAtom (zz, TacApply (Coqast.Nvar(zz, h),NoBindings))
+ | PbpElim (hyp_name, names) ->
+ let bind = List.map (fun s -> (NamedHyp s,make_pbp_pattern s)) names in
+ TacAtom
+ (zz, TacElim ((Coqast.Nvar(zz,hyp_name),ExplicitBindings bind),None))
+ | PbpTryClear l ->
+ TacTry (TacAtom (zz, TacClear (List.map (fun s -> AN (zz,s)) l)))
+ | PbpSplit -> TacAtom (zz, TacSplit NoBindings);;
+
+let rec make_pbp_tactic = function
+ | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
+ | PbpThens (l,tl) ->
+ TacThens
+ (make_then (List.map make_pbp_atomic_tactic l),
+ List.map make_pbp_tactic tl)
let (forall_elim: pbp_rule) = function
avoid, clear_names, clear_flag,
Some h, Prod(Name x, _, body), 2::path, f ->
let h' = next_global_ident_away (id_of_string "H") avoid in
let clear_names' = if clear_flag then h::clear_names else clear_names in
- let str_h' = (string_of_id h') in
- Some(Node(zz, "TACTICLIST",
- [Node(zz,"Generalize",[Node
- (zz, "COMMAND",
- [Node
- (zz, "APPLIST",
- [Nvar (zz, h);
- Node(zz,"APPLIST", [Nvar (zz, "PBP_META");
- Nvar(zz, "Value_for_" ^ (string_of_id x))])])])]);
- make_named_intro str_h';
- f (h'::avoid) clear_names' true (Some str_h') (kind_of_term body) path]))
+ Some
+ (chain_tactics [PbpGeneralize (h,[x]); make_named_intro h']
+ (f (h'::avoid) clear_names' true (Some h') (kind_of_term body) path))
| _ -> None;;
-
+
+
let (imply_elim1: pbp_rule) = function
avoid, clear_names, clear_flag,
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_away (id_of_string "H") avoid in
let str_h' = (string_of_id h') in
- Some(Node
- (zz, "TACTICLIST",
- [Node
- (zz, "CutAndApply",
- [Node (zz, "COMMAND", [Nvar (zz, h)])]);
- Node(zz, "TACLIST",
- [Node
- (zz, "TACTICLIST",
- [Node (zz, "Intro", [Nvar (zz, str_h')]);
- make_clears (h::clear_names)]);
- Node (zz, "TACTICLIST",
- [f avoid clear_names' false None
- (kind_of_term prem) path])])]))
+ Some(PbpThens
+ ([PbpLApply h],
+ [PbpThen [PbpIntros [h']];
+ make_clears (h::clear_names);
+ f avoid clear_names' false None (kind_of_term prem) path]))
| _ -> None;;
+
let (imply_elim2: pbp_rule) = function
avoid, clear_names, clear_flag,
Some h, Prod(Anonymous, prem, body), 2::path, f ->
let clear_names' = if clear_flag then h::clear_names else clear_names in
let h' = next_global_ident_away (id_of_string "H") avoid in
- let str_h' = (string_of_id h') in
- Some(Node
- (zz, "TACTICLIST",
- [Node
- (zz, "CutAndApply",
- [Node (zz, "COMMAND", [Nvar (zz, h)])]);
- Node(zz, "TACLIST",
- [Node
- (zz, "TACTICLIST",
- [Node (zz, "Intro", [Nvar (zz, str_h')]);
- f (h'::avoid) clear_names' false (Some str_h')
- (kind_of_term body) path]);
- Node (zz, "TACTICLIST",
- [make_clears clear_names])])]))
+ Some(PbpThens
+ ([PbpLApply h],
+ [chain_tactics [PbpIntros [h']]
+ (f (h'::avoid) clear_names' false (Some h')
+ (kind_of_term body) path);
+ make_clears clear_names]))
| _ -> None;;
let reference dir s =
@@ -217,18 +280,11 @@ let (and_intro: pbp_rule) = function
let cont_cmd = f avoid clear_names false None
(kind_of_term cont_term) path in
let clear_cmd = make_clears clear_names in
- let cmds = List.map
- (function tac ->
- Node (zz, "TACTICLIST", [tac]))
+ let cmds =
(if a = 1
then [cont_cmd;clear_cmd]
else [clear_cmd;cont_cmd]) in
- Some
- (Node
- (zz, "TACTICLIST",
- [Node (zz, "Split", [Node (zz, "BINDINGS", [])]);
- Node
- (zz, "TACLIST", cmds)]))
+ Some (PbpThens ([PbpSplit],cmds))
else None
| _ -> None;;
@@ -239,17 +295,7 @@ let (ex_intro: pbp_rule) = function
or (is_matching_local (sigconstr ()) oper)
or (is_matching_local (sigTconstr ()) oper) ->
(match kind_of_term c2 with
- Lambda(Name x, _, body) ->
- Some(Node(zz, "Split",
- [Node(zz, "BINDINGS",
- [Node(zz, "BINDING",
- [Node(zz, "COMMAND",
- [Node(zz, "APPLIST",
- [Nvar(zz, "PBP_META");
- Nvar(zz,
- ("Value_for_" ^
- (string_of_id x)))])
- ])])])]))
+ Lambda(Name x, _, body) -> Some (PbpThen [PbpExists x])
| _ -> None)
| _ -> None;;
@@ -261,12 +307,10 @@ let (or_intro: pbp_rule) = function
(is_matching_local (sumconstr ()) or_oper))
& (a = 1 or a = 2) then
let cont_term = if a = 1 then c1 else c2 in
- let fst_cmd = Node(zz, (if a = 1 then "Left" else "Right"),
- [Node(zz, "BINDINGS",[])]) in
+ let fst_cmd = if a = 1 then PbpLeft else PbpRight in
let cont_cmd = f avoid clear_names false None
(kind_of_term cont_term) path in
- Some(Node(zz, "TACTICLIST",
- [fst_cmd;cont_cmd]))
+ Some(chain_tactics [fst_cmd] cont_cmd)
else
None
| _ -> None;;
@@ -279,19 +323,16 @@ let (not_intro: pbp_rule) = function
if(is_matching_local (notconstr ()) not_oper) or
(is_matching_local (notTconstr ()) not_oper) then
let h' = next_global_ident_away (id_of_string "H") avoid in
- let str_h' = (string_of_id h') in
- Some(Node(zz,"TACTICLIST",
- [Node(zz,"Reduce",[Node(zz,"REDEXP",[Node(zz,"Red",[])]);
- Node(zz,"CLAUSE",[])]);
- make_named_intro str_h';
- f (h'::avoid) clear_names false (Some str_h')
- (kind_of_term c1) path]))
+ Some(chain_tactics [PbpReduce;make_named_intro h']
+ (f (h'::avoid) clear_names false (Some h')
+ (kind_of_term c1) path))
else
None
| _ -> None;;
+(*
let elim_with_bindings hyp_name names =
Node(zz,"Elim",
[Node(zz, "COMMAND", [Nvar(zz,hyp_name)]);
@@ -307,6 +348,9 @@ let elim_with_bindings hyp_name names =
[Nvar(zz,"PBP_META");
Nvar(zz,
"value_for_" ^ s)])])])) names)]);;
+*)
+let elim_with_bindings hyp_name names =
+ PbpElim (hyp_name, names);;
let auxiliary_goals clear_names clear_flag this_name n_aux =
let clear_cmd =
@@ -338,13 +382,13 @@ let auxiliary_goals clear_names clear_flag this_name n_aux =
let rec down_prods: (types, constr) kind_of_term * (int list) * int ->
- string list * (int list) * int * (types, constr) kind_of_term *
+ identifier list * (int list) * int * (types, constr) kind_of_term *
(int list) =
function
Prod(Name x, _, body), 2::path, k ->
let res_sl, res_il, res_i, res_cstr, res_p
= down_prods (kind_of_term body, path, k+1) in
- (string_of_id x)::res_sl, (k::res_il), res_i, res_cstr, res_p
+ x::res_sl, (k::res_il), res_i, res_cstr, res_p
| Prod(Anonymous, _, body), 2::path, k ->
let res_sl, res_il, res_i, res_cstr, res_p
= down_prods (kind_of_term body, path, k+1) in
@@ -400,6 +444,7 @@ let (mk_db_indices: int list -> int -> int list) =
answer is true, then the built command takes advantage of the power of
head tactics. *)
+(*
let (head_tactic_patt: pbp_rule) = function
avoid, clear_names, clear_flag, Some h, cstr, path, f ->
(match down_prods (cstr, path, 0) with
@@ -505,7 +550,98 @@ let (head_tactic_patt: pbp_rule) = function
clear_names)
| _ -> None)
| _ -> None;;
-
+*)
+
+let (head_tactic_patt: pbp_rule) = function
+ avoid, clear_names, clear_flag, Some h, cstr, path, f ->
+ (match down_prods (cstr, path, 0) with
+ | (str_list, _, nprems,
+ App(oper,[|c1|]), 2::1::path)
+ when
+ (is_matching_local (notconstr ()) oper) or
+ (is_matching_local (notTconstr ()) oper) ->
+ Some(chain_tactics [elim_with_bindings h str_list]
+ (f avoid clear_names false None (kind_of_term c1) path))
+ | (str_list, _, nprems,
+ App(oper, [|c1; c2|]), 2::a::path)
+ when ((is_matching_local (andconstr()) oper) or
+ (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
+ let h1 = next_global_ident_away (id_of_string "H") avoid in
+ let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in
+ Some(PbpThens
+ ([elim_with_bindings h str_list;
+ make_named_intro h1;
+ make_named_intro h2],
+ let cont_body =
+ if a = 1 then c1 else c2 in
+ let cont_tac =
+ f (h2::h1::avoid) (h::clear_names)
+ false (Some (if 1 = a then h1 else h2))
+ (kind_of_term cont_body) path in
+ cont_tac::(auxiliary_goals
+ clear_names clear_flag
+ h nprems)))
+ | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
+ when ((is_matching_local (exconstr ()) oper) or
+ (is_matching_local (exTconstr ()) oper) or
+ (is_matching_local (sigconstr ()) oper) or
+ (is_matching_local (sigTconstr()) oper)) & a = 2 ->
+ (match (kind_of_term c2),path with
+ Lambda(Name x, _,body), (2::path) ->
+ Some(PbpThens
+ ([elim_with_bindings h str_list],
+ let x' = next_global_ident_away x avoid in
+ let cont_body =
+ Prod(Name x', c1,
+ mkProd(Anonymous, body,
+ mkVar(dummy_id))) in
+ let cont_tac
+ = f avoid (h::clear_names) false None
+ cont_body (2::1::path) in
+ cont_tac::(auxiliary_goals
+ clear_names clear_flag
+ h nprems)))
+ | _ -> None)
+ | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
+ when ((is_matching_local (orconstr ()) oper) or
+ (is_matching_local (sumboolconstr ()) oper) or
+ (is_matching_local (sumconstr ()) oper)) &
+ (a = 1 or a = 2) ->
+ Some(PbpThens
+ ([elim_with_bindings h str_list],
+ let cont_body =
+ if a = 1 then c1 else c2 in
+ (* h' is the name for the new intro *)
+ let h' = next_global_ident_away (id_of_string "H") avoid in
+ let cont_tac =
+ chain_tactics
+ [make_named_intro h']
+ (f
+ (* h' should not be used again *)
+ (h'::avoid)
+ (* the disjunct itself can be discarded *)
+ (h::clear_names) false (Some h')
+ (kind_of_term cont_body) path) in
+ let snd_tac =
+ chain_tactics
+ [make_named_intro h']
+ (make_clears (h::clear_names)) in
+ let tacs1 =
+ if a = 1 then
+ [cont_tac; snd_tac]
+ else
+ [snd_tac; cont_tac] in
+ tacs1@(auxiliary_goals (h::clear_names)
+ false dummy_id nprems)))
+ | (str_list, int_list, nprems, c, [])
+ when (check_apply c (mk_db_indices int_list nprems)) &
+ (match c with Prod(_,_,_) -> false
+ | _ -> true) &
+ (List.length int_list) + nprems > 0 ->
+ Some(add_clear_names_if_necessary (PbpThen [PbpApply h]) clear_names)
+ | _ -> None)
+ | _ -> None;;
+
let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
forall_elim; imply_intro1; imply_elim1; imply_elim2;
@@ -541,11 +677,15 @@ let rec clean_trace flag =
command requested by the point-and-shoot strategy. Default is
Try Assumption--Try Exact. *)
+(*
let default_ast optname constr path =
match optname with
None -> Node(zz, "TRY", [Node(zz, "Assumption",[])])
| Some(a) -> Node(zz, "TRY",
[Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);;
+*)
+
+let default_ast optname constr path = PbpThen [PbpTryAssumption optname]
(* This is the main proof by pointing function. *)
(* avoid: les noms a ne pas utiliser *)
@@ -564,8 +704,9 @@ let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
in try_all_rules (!pbp_rules);;
(* these are the optimisation functions. *)
-(* This function takes care of flattening successive intro commands. *)
+(* This function takes care of flattening successive then commands. *)
+(*
let rec optim1 =
function
Node(a,"TACTICLIST",b) ->
@@ -591,10 +732,25 @@ let rec optim1 =
| [t] -> t
| args -> Node(zz,"TACTICLIST", args))
| t -> t;;
-
+*)
+
+(* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy
+ that t is some [PbpAtom t] *)
+(*
+let rec flatten_sequence =
+ function
+ PbpThens (tl1,tl2) -> PbpThens (tl1,List.map flatten_sequence tl2)
+ | PbpThen (tl1,t1) as x ->
+ (match flatten_sequence t1 with
+ | PbpThenCont (tl2,t2) -> PbpThenCont (tl1@tl2,t2)
+ | PbpThens (tl2,tl3) -> PbpThens (tl1@tl2,tl3)
+ | PbpAtom _ -> x)
+ | PbpAtom t as x -> x;;
+*)
(* This optimization function takes care of compacting successive Intro commands
together. *)
+(*
let rec optim2 =
function
Node(a,"TACTICLIST",b) ->
@@ -624,7 +780,42 @@ let rec optim2 =
| l -> (put_ids l)::t1::(group_intros [] others)) in
Node(a,"TACTICLIST",group_intros [] b)
| t -> t;;
+*)
+(*
+let rec optim2 = function
+ | TacThens (t,tl) -> TacThens (optim2 t, List.map optim2 tl)
+ | t ->
+ let get_ids =
+ List.map (function IntroIdentifier _ as x -> x
+ | _ -> failwith "get_ids expected an identifier") in
+ let rec group_intros names = function
+ [] -> (match names with
+ [] -> []
+ | l -> [TacIntroPattern l])
+ | (TacIntroPattern ids)::others ->
+ group_intros (names@(get_ids ids)) others
+ | t1::others ->
+ (match names with
+ [] -> t1::(group_intros [] others)
+ | l -> (TacIntroPattern l)::t1::(group_intros [] others)) in
+ make_then (group_intros [] (flatten_sequence t))
+*)
+let rec group_intros names = function
+ [] -> (match names with
+ [] -> []
+ | l -> [PbpIntros l])
+ | (PbpIntros ids)::others -> group_intros (names@ids) others
+ | t1::others ->
+ (match names with
+ [] -> t1::(group_intros [] others)
+ | l -> (PbpIntros l)::t1::(group_intros [] others))
+
+let rec optim2 = function
+ | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2)
+ | PbpThen tl -> PbpThen (group_intros [] tl)
+
+(*
let rec merge_ast_in_command com1 com2 =
let args1 =
(match com1 with
@@ -635,7 +826,8 @@ let rec merge_ast_in_command com1 com2 =
Node(_, "APPLIST", hyp::args) -> args
| _ -> failwith "unexpected com2 in merge_ast_in_command") in
Node(zz, "COMMAND", [Node(zz, "APPLIST", args1@args2)]);;
-
+*)
+(*
let cleanup_clears empty_allowed names str_list other =
let rec clean_aux = function
[] -> []
@@ -653,42 +845,44 @@ let cleanup_clears empty_allowed names str_list other =
else [Node(zz,"Idtac",[])]
| _ -> other)
| l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;;
-
+*)
+let rec cleanup_clears str_list = function
+ [] -> []
+ | x::tail ->
+ if List.mem x str_list then cleanup_clears str_list tail
+ else x::(cleanup_clears str_list tail);;
(* This function takes care of compacting instanciations of universal
quantifications. *)
+
+let rec optim3_aux str_list = function
+ (PbpGeneralize (h,l1))::(PbpIntros [s])::(PbpGeneralize (h',l2))::others
+ when s=h' ->
+ optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others)
+ | (PbpTryClear names)::other ->
+ (match cleanup_clears str_list names with
+ [] -> other
+ | l -> (PbpTryClear l)::other)
+ | a::l -> a::(optim3_aux str_list l)
+ | [] -> [];;
+
let rec optim3 str_list = function
- Node(a,"TACTICLIST", b) ->
- let rec optim3_aux empty_allowed str_list = function
- ((Node(a, "Generalize", [Node(_, "COMMAND", [com1])])) as t1)::
- intro::
- (Node(b, "Generalize", [Node(_, "COMMAND", [com2])]) as t2)::others ->
- (match get_name_from_intro intro with
- None -> t1::intro::(optim3_aux true str_list (t2::others))
- | Some s -> optim3_aux true (s::str_list)
- (Node(a, "Generalize",
- [merge_ast_in_command com1 com2])::others))
- |( Node(zz, "TRY", [Node(a,"Clear", [Node(_,"CLAUSE", names)])]))::other ->
- cleanup_clears empty_allowed names str_list other
- | [Node(a,"TACLIST",branches)] ->
- [Node(a,"TACLIST",List.map (optim3 str_list) branches)]
- | a::l -> a::(optim3_aux true str_list l)
- | [] -> if empty_allowed then
- []
- else failwith "strange value in optim3_aux" in
- Node(a, "TACTICLIST", optim3_aux false str_list b)
- | t -> t;;
+ PbpThens (tl1, tl2) ->
+ PbpThens (optim3_aux str_list tl1, List.map (optim3 str_list) tl2)
+ | PbpThen tl -> PbpThen (optim3_aux str_list tl)
-let optim x = optim3 [] (optim2 (optim1 x));;
+let optim x = make_pbp_tactic (optim3 [] (optim2 x));;
+(* TODO
add_tactic "Traced_Try" traced_try_entry;;
+*)
let rec tactic_args_to_ints = function
[] -> []
| (Integer n)::l -> n::(tactic_args_to_ints l)
| _ -> failwith "expecting only numbers";;
-
+(*
let pbp_tac display_function = function
(Identifier a)::l ->
(function g ->
@@ -720,3 +914,34 @@ let pbp_tac display_function = function
| _ -> failwith "expecting other arguments";;
+*)
+let pbp_tac display_function idopt nl =
+ match idopt with
+ | Some str ->
+ (function g ->
+ let (ou,tstr) = (get_hyp_by_name g str) in
+ let exp_ast =
+ pbpt default_ast
+ (match ou with
+ "hyp" ->(pf_ids_of_hyps g)
+ |_ -> (str::(pf_ids_of_hyps g)))
+ []
+ false
+ (Some str)
+ (kind_of_term tstr)
+ nl in
+ (display_function (optim exp_ast); tclIDTAC g))
+ | None ->
+ if nl <> [] then
+ (function g ->
+ let exp_ast =
+ (pbpt default_ast (pf_ids_of_hyps g) [] false
+ None (kind_of_term (pf_concl g)) nl) in
+ (display_function (optim exp_ast); tclIDTAC g))
+ else
+ (function g ->
+ (display_function
+ (make_pbp_tactic (default_ast None (pf_concl g) []));
+ tclIDTAC g));;
+
+
diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli
index 57794ec229..43ec1274d8 100644
--- a/contrib/interface/pbp.mli
+++ b/contrib/interface/pbp.mli
@@ -1,4 +1,4 @@
-val pbp_tac : (Ctast.t -> 'a) ->
- Proof_type.tactic_arg list ->
+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;;
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 9a5f803d3c..ae876e129f 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -27,6 +27,9 @@ open Proof_trees
open Sign
open Pp
open Printer
+open Rawterm
+open Tacexpr
+open Genarg
(*****************************************************************************)
(*
Arbre de preuve maison:
@@ -40,7 +43,7 @@ type nhyp = {hyp_name : identifier;
hyp_full_type: Term.constr}
;;
-type ntactic = Coqast.t list
+type ntactic = tactic_expr
;;
type nproof =
@@ -154,14 +157,15 @@ let seq_to_lnhyp sign sign' cl =
let rule_is_complex r =
match r with
- Tactic ("Interp",_) -> true
- | Tactic ("Auto", _) -> true
- | Tactic ("Symmetry", _) -> true
- |_ -> false
+ Tactic (TacArg (Tacexp t),_) -> true
+ | Tactic (TacAtom (_,TacAuto _), _) -> true
+ | Tactic (TacAtom (_,TacSymmetry), _) -> true
+ |_ -> false
;;
let ast_of_constr = Termast.ast_of_constr true (Global.env()) ;;
+(*
let rule_to_ntactic r =
let rast =
(match r with
@@ -178,6 +182,20 @@ let rule_to_ntactic r =
else [rast ]
;;
+*)
+let rule_to_ntactic r =
+ let rt =
+ (match r with
+ Tactic (t,_) -> t
+ | Prim (Refine h) -> TacAtom (Ast.dummy_loc,TacExact h)
+ | _ -> TacAtom (Ast.dummy_loc, TacIntroPattern [])) in
+ if rule_is_complex r
+ then (match rt with
+ TacArg (Tacexp _) as t -> t
+ | _ -> assert false)
+
+ else rt
+;;
let term_of_command x =
@@ -238,14 +256,12 @@ let to_nproof sigma osign pf =
| Some(r,spfl) ->
if rule_is_complex r
then (
- let p1=(match pf.subproof with
- Some x -> to_nproof_rec sigma sign x
- |_-> assert false) in
+ let p1= to_nproof_rec sigma sign (subproof_of_proof pf) in
let ntree= fill_unproved p1
(List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
spfl) in
(match r with
- Tactic ("Auto",_) ->
+ Tactic (TacAtom (_, TacAuto _),_) ->
if spfl=[]
then
{t_info="to_prove";
@@ -253,7 +269,7 @@ let to_nproof sigma osign pf =
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 ([Node ((0,0), "InfoAuto",[])], [ntree])}
+ t_proof= Proof (TacAtom (Ast.dummy_loc,TacExtend ("InfoAuto",[])), [ntree])}
else ntree
| _ -> ntree))
else
@@ -399,11 +415,15 @@ let enumerate f ln =
let constr_of_ast = Astterm.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
French ->
@@ -942,6 +962,7 @@ let natural_lhyp lh hi =
Analyse des tactiques.
*)
+(*
let name_tactic tac =
match tac with
(Node(_,"Interp",
@@ -950,7 +971,14 @@ let name_tactic tac =
|(Node(_,t,_))::_ -> t
| _ -> assert false
;;
+*)
+let name_tactic = function
+ | TacIntroPattern _ -> "Intro"
+ | TacAssumption -> "Assumption"
+ | _ -> failwith "TODO"
+;;
+(*
let arg1_tactic tac =
match tac with
(Node(_,"Interp",
@@ -960,6 +988,9 @@ let arg1_tactic tac =
| x::_ -> x
| _ -> assert false
;;
+*)
+
+let arg1_tactic tac = failwith "TODO"
let arg2_tactic tac =
match tac with
@@ -970,6 +1001,7 @@ let arg2_tactic tac =
| _ -> assert false
;;
+(*
type nat_tactic =
Split of (Coqast.t list)
| Generalize of (Coqast.t list)
@@ -992,7 +1024,7 @@ let analyse_tac tac =
| [Node (_, x,la)] -> Other (x,la)
| _ -> assert false
;;
-
+*)
@@ -1103,6 +1135,17 @@ let terms_of_equality e =
let eq_term = eq_constr;;
+let is_equality_tac = function
+ | TacAtom (_,
+ (TacExtend
+ (("ERewriteLR"|"ERewriteRL"|"ERewriteLRocc"|"ERewriteRLocc"
+ |"ERewriteParallel"|"ERewriteNormal"
+ |"RewriteLR"|"RewriteRL"|"Replace"),_)
+ | TacReduce _
+ | TacSymmetry | TacReflexivity
+ | TacExact _ | TacIntroPattern _ | TacIntroMove _ | TacAuto _)) -> true
+ | _ -> false
+
let equalities_ntree ig ntree =
let rec equalities_ntree ig ntree =
if not (is_equality (concl ntree))
@@ -1111,12 +1154,7 @@ let equalities_ntree ig ntree =
match (proof ntree) with
Notproved -> [(ig,ntree)]
| Proof (tac,ltree) ->
- if List.mem (name_tactic tac)
- ["ERewriteLR";"ERewriteRL"; "ERewriteLRocc";"ERewriteRLocc";
- "ERewriteParallel";"ERewriteNormal"; "Reduce";
- "RewriteLR";"RewriteRL";
- "Replace";"Symmetry";"Reflexivity";
- "Exact";"Intros";"Intro";"Auto"]
+ if is_equality_tac tac
then (match ltree with
[] -> [(ig,ntree)]
| t::_ -> let res=(equalities_ntree ig t) in
@@ -1176,7 +1214,7 @@ let rec natural_ntree ig ntree =
let lemma = match (proof ntree) with
Proof (tac,ltree) ->
(try (sph [spt (dbize (gLOB ge)
- (term_of_command (arg1_tactic tac)));
+ (term_of_command (arg1_tactic tac)));(* TODO *)
(match ltree with
[] ->spe
| [_] -> spe
@@ -1224,55 +1262,62 @@ let rec natural_ntree ig ntree =
sph [spi; sps (intro_not_proved_goal gs); spb;
tag_toprove g ]
]
- | Proof (tac,ltree) ->
- (let tactic= name_tactic tac in
- let ntext =
- (match tactic with
+
+ | Proof (TacId,ltree) -> natural_ntree ig (List.hd ltree)
+ | Proof (TacAtom (_,tac),ltree) ->
+ (let ntext =
+ match tac with
(* Pas besoin de l'argument éventuel de la tactique *)
- "Intros" -> natural_intros ig lh g gs ltree
- | "Intro" -> natural_intros ig lh g gs ltree
- | "Idtac" -> natural_ntree ig (List.hd ltree)
- | "Fix" -> natural_fix ig lh g gs (arg2_tactic tac) ltree
- | "Split" -> natural_split ig lh g gs ge tac ltree
- | "Generalize" -> natural_generalize ig lh g gs ge tac ltree
- | "Right" -> natural_right ig lh g gs ltree
- | "Left" -> natural_left ig lh g gs ltree
- | (* "Simpl" *)"Reduce" -> natural_reduce ig lh g gs ge tac ltree
- | "InfoAuto" -> natural_infoauto ig lh g gs ltree
- | "Auto" -> natural_auto ig lh g gs ltree
- | "EAuto" -> natural_auto ig lh g gs ltree
- | "Trivial" -> natural_trivial ig lh g gs ltree
- | "Assumption" -> natural_trivial ig lh g gs ltree
- | "Clear" -> natural_clear ig lh g gs ltree
+ TacIntroPattern _ -> natural_intros ig lh g gs ltree
+ | TacIntroMove _ -> natural_intros ig lh g gs ltree
+ | TacFix (_,n) -> natural_fix ig lh g gs n ltree
+ | TacSplit NoBindings -> natural_split ig lh g gs ge [] ltree
+ | TacSplit(ImplicitBindings l) -> natural_split ig lh g gs ge l ltree
+ | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree
+ | TacRight _ -> natural_right ig lh g gs ltree
+ | TacLeft _ -> natural_left ig lh g gs ltree
+ | (* "Simpl" *)TacReduce (r,cl) ->
+ natural_reduce ig lh g gs ge r cl ltree
+ | TacExtend ("InfoAuto",[]) -> natural_infoauto ig lh g gs ltree
+ | TacAuto _ -> natural_auto ig lh g gs ltree
+ | TacExtend ("EAuto",_) -> natural_auto ig lh g gs ltree
+ | TacTrivial _ -> natural_trivial ig lh g gs ltree
+ | TacAssumption -> natural_trivial ig lh g gs ltree
+ | TacClear _ -> natural_clear ig lh g gs ltree
(* Besoin de l'argument de la tactique *)
- | "Induction" ->
- let arg1=(term_of_command (arg1_tactic tac)) in
- natural_induction ig lh g gs ge arg1 ltree false
- | "InductionIntro" ->
- let arg1=(term_of_command (arg1_tactic tac)) in
- natural_induction ig lh g gs ge arg1 ltree true
- | _ ->
- let arg1=(term_of_command (arg1_tactic tac)) in
- let arg1=dbize (gLOB ge) arg1 in
- (match tactic with
- "Apply" -> natural_apply ig lh g gs arg1 ltree
- | "Exact" -> natural_exact ig lh g gs arg1 ltree
- | "Cut" -> natural_cut ig lh g gs arg1 ltree
- | "CutIntro" -> natural_cutintro ig lh g gs arg1 ltree
- | "Case" -> natural_case ig lh g gs ge arg1 ltree false
- | "CaseIntro" -> natural_case ig lh g gs ge arg1 ltree true
- | "Elim" -> natural_elim ig lh g gs ge arg1 ltree false
- | "ElimIntro" -> natural_elim ig lh g gs ge arg1 ltree true
- | "RewriteRL" -> natural_rewrite ig lh g gs arg1 ltree
- | "RewriteLR" -> natural_rewrite ig lh g gs arg1 ltree
- | "ERewriteRL" -> natural_rewrite ig lh g gs arg1 ltree
- | "ERewriteLR" -> natural_rewrite ig lh g gs arg1 ltree
- |_ -> natural_generic ig lh g gs (sps tactic) (prl sp_tac tac) ltree)
- )
+ | TacOldInduction (NamedHyp id) ->
+ natural_induction ig lh g gs ge id ltree false
+ | TacExtend ("InductionIntro",[a]) ->
+ let id=(out_gen wit_ident a) in
+ natural_induction ig lh g gs ge id ltree true
+ | TacApply (c,_) -> natural_apply ig lh g gs c ltree
+ | 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
+ natural_cutintro ig lh g gs a ltree
+ | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
+ | TacExtend ("CaseIntro",[a]) ->
+ let c = out_gen wit_constr a in
+ natural_case ig lh g gs ge c ltree true
+ | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false
+ | TacExtend ("ElimIntro",[a]) ->
+ let c = out_gen wit_constr a in
+ natural_elim ig lh g gs ge c ltree true
+ | TacExtend ("Rewrite",[_;a]) ->
+ let (c,_) = out_gen wit_constr_with_bindings a in
+ natural_rewrite ig lh g gs c ltree
+ | TacExtend ("ERewriteRL",[a]) ->
+ let c = out_gen wit_constr a in (* TODO *)
+ natural_rewrite ig lh g gs c ltree
+ | TacExtend ("ERewriteLR",[a]) ->
+ let c = out_gen wit_constr a in (* TODO *)
+ natural_rewrite ig lh g gs c ltree
+ |_ -> natural_generic ig lh g gs (sps (name_tactic tac)) (prl sp_tac [tac]) ltree
in
ntext (* spwithtac ntext tactic*)
)
-
+ | Proof _ -> failwith "Don't know what to do with that"
in
if info<>"not_proved"
then spshrink info ntext
@@ -1580,12 +1625,9 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
(*
InductionIntro n
*)
-and natural_induction ig lh g gs ge arg1 ltree with_intros=
+and natural_induction ig lh g gs ge arg2 ltree with_intros=
let env = (gLOB (g_env (List.hd ltree))) in
- let arg1=dbize env arg1 in
- let arg2 = match (kind_of_term arg1) with
- Var(arg2) -> arg2
- | _ -> assert false in
+ 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
@@ -1637,8 +1679,7 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
(***********************************************************************)
(* Points fixes *)
-and natural_fix ig lh g gs arg ltree =
- let narg = match arg with Num(_,narg) -> narg |_ -> assert false in
+and natural_fix ig lh g gs narg ltree =
let {t_info=info;
t_goal={newhyp=lh1;t_concl=g1;t_full_concl=gf1;
t_full_env=ge1};t_proof=p1}=(List.hd ltree) in
@@ -1656,10 +1697,7 @@ and natural_fix ig lh g gs arg ltree =
ltree)
]
| _ -> assert false
-and natural_reduce ig lh g gs ge tac ltree =
- let (mode,la) = match analyse_tac tac with
- Reduce (mode,la) -> (mode,la)
- |_ -> assert false in
+and natural_reduce ig lh g gs ge mode la ltree =
match la with
[] ->
spv
@@ -1669,7 +1707,7 @@ and natural_reduce ig lh g gs ge tac ltree =
{ihsg=All_subgoals_hyp;isgintro="simpl"})
ltree)
]
- | [Nvar (_,hyp)] ->
+ | [hyp] ->
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1678,14 +1716,11 @@ and natural_reduce ig lh g gs ge tac ltree =
ltree)
]
| _ -> assert false
-and natural_split ig lh g gs ge tac ltree =
- let la = match analyse_tac tac with
- Split la -> la
- |_ -> assert false in
+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 arg1= (*dbize env*) arg in
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1702,14 +1737,13 @@ and natural_split ig lh g gs ge tac ltree =
ltree)
]
| _ -> assert false
-and natural_generalize ig lh g gs ge tac ltree =
- match analyse_tac tac with
- Generalize la ->
- (match la with
+and natural_generalize ig lh g gs ge la ltree =
+ match la with
[arg] ->
let env= (gLOB ge) in
- let arg1= dbize env arg in
- let type_arg=type_of_ast ge arg in
+ let arg1= (*dbize env*) 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);
(show_goal2 lh ig g gs "");
@@ -1718,8 +1752,7 @@ and natural_generalize ig lh g gs ge tac ltree =
{ihsg=All_subgoals_hyp;isgintro=""})
ltree)
]
- | _ -> assert false)
- | _ -> assert false
+ | _ -> assert false
and natural_right ig lh g gs ltree =
spv
[ (natural_lhyp lh ig.ihsg);
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7f38ca0d27..2e49ec4e3d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -8,6 +8,10 @@ open Ast;;
open Names;;
open Ctast;;
open Ascent;;
+open Genarg;;
+open Rawterm;;
+open Tacexpr;;
+open Vernacexpr;;
let in_coq_ref = ref false;;
@@ -77,6 +81,10 @@ let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;;
let ctf_STRING_OPT_SOME s = CT_coerce_STRING_to_STRING_OPT s;;
+let ctf_STRING_OPT = function
+ | None -> ctf_STRING_OPT_NONE
+ | Some s -> ctf_STRING_OPT_SOME s
+
let ctv_ID_OPT_NONE = CT_coerce_NONE_to_ID_OPT CT_none;;
let ctf_ID_OPT_SOME s = CT_coerce_ID_to_ID_OPT s;;
@@ -102,7 +110,12 @@ let castc x = CT_coerce_TYPED_FORMULA_to_FORMULA x;;
let varc x = CT_coerce_ID_to_FORMULA x;;
+let xlate_ident id = CT_ident (string_of_id id)
+
+(*
let ident_tac s = CT_user_tac (CT_ident s, CT_targ_list []);;
+*)
+let ident_tac s = CT_user_tac (xlate_ident s, CT_targ_list []);;
let ident_vernac s = CT_user_vernac (CT_ident s, CT_varg_list []);;
@@ -141,6 +154,7 @@ type iVARG = Varg_binder of ct_BINDER
| Varg_tactic_arg of iTARG
| Varg_varglist of iVARG list;;
+(*
let coerce_iTARG_to_TARG =
function
| Targ_intropatt x -> xlate_error "coerce_iTARG_to_TARG (3)"
@@ -160,7 +174,9 @@ let coerce_iTARG_to_TARG =
| Targ_cofixtac x -> CT_coerce_COFIXTAC_to_TARG x
| Targ_tacexp x -> CT_coerce_TACTIC_COM_to_TARG x
| Targ_redexp x -> xlate_error "coerce_iTarg_to_TARG(2)";;
+*)
+(*
let rec coerce_iVARG_to_VARG =
function
| Varg_binder x -> CT_coerce_BINDER_to_VARG x
@@ -189,6 +205,7 @@ let rec coerce_iVARG_to_VARG =
CT_coerce_VARG_LIST_to_VARG
(CT_varg_list (List.map coerce_iVARG_to_VARG x))
| _ -> xlate_error "coerce_iVARG_to_VARG: leftover case";;
+*)
let coerce_iVARG_to_FORMULA =
function
@@ -219,9 +236,14 @@ let xlate_id =
| s -> CT_ident s)
| _ -> xlate_error "xlate_id: not an identifier";;
+(*
let xlate_id_unit = function
Node(_, "VOID", []) -> CT_unit
| x -> CT_coerce_ID_to_ID_UNIT (xlate_id x);;
+*)
+let xlate_id_unit = function
+ None -> CT_unit
+ | Some x -> CT_coerce_ID_to_ID_UNIT (xlate_ident x);;
let xlate_id_opt =
function
@@ -231,11 +253,20 @@ let xlate_id_opt =
| s -> ctf_ID_OPT_SOME (CT_ident s))
| _ -> xlate_error "xlate_id: not an identifier";;
+let xlate_ident_opt =
+ function
+ | None -> ctv_ID_OPT_NONE
+ | Some id -> ctf_ID_OPT_SOME (xlate_ident id)
+
let xlate_int =
function
| Num (_, n) -> CT_int n
| _ -> xlate_error "xlate_int: not an int";;
+let xlate_int_opt = function
+ | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
+ | None -> CT_coerce_NONE_to_INT_OPT CT_none
+
let xlate_string =
function
| Str (_, s) -> CT_string s
@@ -313,6 +344,28 @@ let qualid_to_ct_ID =
| Node(_, "QUALIDMETA",[Num(_,n)]) -> Some(CT_metac (CT_int n))
| _ -> None;;
+let tac_qualid_to_ct_ID qid = CT_ident (Nametab.string_of_qualid qid)
+
+let loc_qualid_to_ct_ID (_,qid) = CT_ident (Nametab.string_of_qualid qid)
+
+let qualid_or_meta_to_ct_ID = function
+ | AN (_,qid) -> tac_qualid_to_ct_ID qid
+ | MetaNum (_,n) -> CT_metac (CT_int n)
+
+let ident_or_meta_to_ct_ID = function
+ | AN (_,id) -> xlate_ident id
+ | MetaNum (_,n) -> CT_metac (CT_int n)
+
+let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
+
+let reference_to_ct_ID = function
+ | RIdent (_,id) -> CT_ident (Names.string_of_id id)
+ | RQualid (_,qid) -> CT_ident (Nametab.string_of_qualid qid)
+
+let xlate_class = function
+ | FunClass -> CT_ident "FUNCLASS"
+ | SortClass -> CT_ident "SORTCLASS"
+ | RefClass qid -> loc_qualid_to_ct_ID qid
let special_case_qualid cont_function astnode =
match qualid_to_ct_ID astnode with
@@ -744,6 +797,13 @@ let xlate_special_cases cont_function arg =
| [] -> None in
xlate_rec xlate_formula_special_cases;;
+let xlate_sort =
+ function
+ | Coqast.Node (_, "SET", []) -> CT_sortc "Set"
+ | Coqast.Node (_, "PROP", []) -> CT_sortc "Prop"
+ | Coqast.Node (_, "TYPE", []) -> CT_sortc "Type"
+ | _ -> xlate_error "xlate_sort";;
+
let xlate_formula a =
!set_flags ();
let rec ctrec =
@@ -766,10 +826,28 @@ let xlate_formula a =
| _ -> xlate_error "xlate_formula" in
strip_Rform (ctrec a);;
+(*
let xlate_formula_opt =
function
| Node (_, "None", []) -> ctv_FORMULA_OPT_NONE
| e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e);;
+*)
+let xlate_formula_opt =
+ function
+ | None -> ctv_FORMULA_OPT_NONE
+ | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e);;
+
+let xlate_constr c = xlate_formula (Ctast.ast_to_ct c)
+
+let xlate_constr_opt c = xlate_formula_opt (option_app Ctast.ast_to_ct c)
+
+let xlate_hyp_location =
+ function
+ | InHyp (AI (_,id)) -> xlate_ident id
+ | InHyp (MetaId _) -> xlate_error "MetaId should occur only in quotations"
+ | InHypType id -> xlate_error "TODO: in (Type of id)"
+
+let xlate_clause l = CT_id_list (List.map xlate_hyp_location l)
(** Tactics
*)
@@ -826,7 +904,7 @@ let make_ID_from_FORMULA =
| _ -> xlate_error "make_ID_from_FORMULA: non-formula argument";;
let make_ID_from_iTARG_FORMULA x = make_ID_from_FORMULA (strip_targ_command x);;
-
+(*
let filter_binding_or_command_list bl =
match bl with
| (Targ_binding_com cmd) :: bl' ->
@@ -837,6 +915,23 @@ let filter_binding_or_command_list bl =
(CT_binding_list (List.map strip_targ_binding bl))
| [] -> CT_coerce_FORMULA_LIST_to_SPEC_LIST (CT_formula_list [])
| _ -> xlate_error "filter_binding_or_command_list";;
+*)
+let xlate_quantified_hypothesis = function
+ | AnonHyp n -> CT_coerce_INT_to_ID_OR_INT (CT_int n)
+ | NamedHyp id -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id)
+
+let xlate_explicit_binding (h,c) =
+ CT_binding (xlate_quantified_hypothesis h, xlate_constr c)
+
+let xlate_bindings = function
+ | ImplicitBindings l ->
+ CT_coerce_FORMULA_LIST_to_SPEC_LIST
+ (CT_formula_list (List.map xlate_constr l))
+ | ExplicitBindings l ->
+ CT_coerce_BINDING_LIST_to_SPEC_LIST
+ (CT_binding_list (List.map xlate_explicit_binding l))
+ | NoBindings ->
+ CT_coerce_FORMULA_LIST_to_SPEC_LIST (CT_formula_list [])
let strip_targ_spec_list =
function
@@ -849,6 +944,7 @@ let strip_targ_intropatt =
| _ -> xlate_error "strip_targ_intropatt";;
+(*
let rec get_flag_rec =
function
| n1 :: tail ->
@@ -873,7 +969,23 @@ let rec get_flag_rec =
| Node (_, a, _) -> error ("get_flag_rec : unexpected flag " ^ a)
| _ -> error "get_flag_rec : unexpected flag")
| [] -> [], CT_unf [];;
-
+*)
+let get_flag r =
+ let conv_flags, red_ids =
+ if r.rDelta then
+ [CT_delta], CT_unfbut (List.map qualid_or_meta_to_ct_ID r.rConst)
+ else
+ (if r.rConst = []
+ then (* probably useless: just for compatibility *) []
+ else [CT_delta]),
+ CT_unf (List.map qualid_or_meta_to_ct_ID r.rConst) in
+ let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in
+ let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in
+ let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in
+ (* Rem: EVAR flag obsolète *)
+ conv_flags, red_ids
+
+(*
let rec xlate_intro_pattern =
function
| Node(_,"CONJPATTERN", l) ->
@@ -886,10 +998,21 @@ let rec xlate_intro_pattern =
CT_coerce_ID_to_INTRO_PATT(CT_ident c)
| Node(_, a, _) -> failwith ("xlate_intro_pattern on node " ^ a)
| _ -> failwith "xlate_intro_pattern";;
+*)
+let rec xlate_intro_pattern =
+ function
+ | IntroOrAndPattern [l] ->
+ CT_conj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern l))
+ | IntroOrAndPattern ll ->
+ let insert_conj l = CT_conj_pattern (CT_intro_patt_list
+ (List.map xlate_intro_pattern l))
+ in CT_disj_pattern(CT_intro_patt_list (List.map insert_conj ll))
+ | IntroWildcard -> xlate_error "TODO: '_' intro pattern"
+ | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
let compute_INV_TYPE_from_string = function
"InversionClear" -> CT_inv_clear
- | "HalfInversion" -> CT_inv_simple
+ | "SimpleInversion" -> CT_inv_simple
| "Inversion" -> CT_inv_regular
| _ -> failwith "unexpected Inversion type";;
@@ -909,6 +1032,7 @@ let tactic_special_case cont_function cvt_arg = function
| _ -> assert false;;
let xlate_context_pattern = function
+(*
Node(_,"TERM", [Node(_, "COMMAND", [v])]) ->
CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
| Node(_,"SUBTERM", [Node(_,"COMMAND",[v])]) ->
@@ -916,12 +1040,23 @@ let xlate_context_pattern = function
| Node(_,"SUBTERM", [Nvar(_, s); Node(_, "COMMAND", [v])]) ->
CT_context(ctf_ID_OPT_SOME (CT_ident s), xlate_formula v)
| _ -> assert false;;
+*)
+ | Term v ->
+ CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_constr v)
+ | Subterm (idopt, v) ->
+ CT_context(xlate_ident_opt idopt, xlate_constr v)
+
let xlate_match_context_hyps = function
+(*
[b] -> CT_premise_pattern(ctv_ID_OPT_NONE, xlate_context_pattern b)
| [Nvar(_,s);b] -> CT_premise_pattern(ctf_ID_OPT_SOME (CT_ident s),
xlate_context_pattern b)
| _ -> assert false;;
+*)
+ | NoHypId b -> CT_premise_pattern(ctv_ID_OPT_NONE, xlate_context_pattern b)
+ | Hyp ((_,id),b) -> CT_premise_pattern(ctf_ID_OPT_SOME (xlate_ident id),
+ xlate_context_pattern b)
let xlate_largs_to_id_unit largs =
@@ -929,6 +1064,8 @@ let xlate_largs_to_id_unit largs =
fst::rest -> fst, rest
| _ -> assert false;;
+(* Obsolete, partially replaced by xlate_tacarg and partially dispatched on
+ throughout the code for each tactic entry
let rec cvt_arg =
function
| Nvar (_, id) -> Targ_ident (CT_ident id)
@@ -991,8 +1128,75 @@ let rec cvt_arg =
(string_of_int l1) ^ " " ^
(string_of_int l2))
| _ -> failwith "cvt_arg"
+*)
+let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
+ function
+ | TacVoid ->
+ CT_void
+ | Tacexp t ->
+ CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic t)
+ | Integer n ->
+ CT_coerce_ID_OR_INT_to_TACTIC_ARG
+ (CT_coerce_INT_to_ID_OR_INT (CT_int n))
+ | Reference r ->
+ CT_coerce_ID_OR_INT_to_TACTIC_ARG
+ (CT_coerce_ID_to_ID_OR_INT (reference_to_ct_ID r))
+ | TacDynamic _ ->
+ failwith "Dynamics not treated in xlate_ast"
+ | ConstrMayEval (ConstrTerm c) ->
+ CT_coerce_FORMULA_to_TACTIC_ARG (xlate_constr c)
+ | ConstrMayEval _ ->
+ xlate_error "TODO: Eval/Inst as tactic argument"
+ | MetaIdArg _ ->
+ xlate_error "MetaIdArg should only be used in quotations"
+ | MetaNumArg (_,n) ->
+ CT_coerce_FORMULA_to_TACTIC_ARG
+ (CT_coerce_ID_to_FORMULA(CT_metac (CT_int n)))
+ | t ->
+ CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_call_or_tacarg t)
+
+and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) =
+ function
+ (* Moved from xlate_tactic *)
+ | TacCall (_,Reference r, a::l) ->
+ CT_simple_user_tac
+ (reference_to_ct_ID r,
+ CT_tactic_arg_list(xlate_tacarg a,List.map xlate_tacarg l))
+ | TacCall (_,_,_) -> xlate_error ""
+ | Reference (RIdent (_,s)) -> ident_tac s
+ | t -> xlate_error "TODO: result other than tactic or constr"
+
and xlate_red_tactic =
function
+ | Red true -> xlate_error ""
+ | Red false -> CT_red
+ | Hnf -> CT_hnf
+ | Simpl -> CT_simpl
+ | Cbv flag_list ->
+ let conv_flags, red_ids = get_flag flag_list in
+ CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
+ | Lazy flag_list ->
+ let conv_flags, red_ids = get_flag flag_list in
+ CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
+ | Unfold unf_list ->
+ let ct_unf_list = List.map (fun (nums,qid) ->
+ CT_unfold_occ (CT_int_list (List.map (fun x -> CT_int x) nums),
+ qualid_or_meta_to_ct_ID qid)) unf_list in
+ (match ct_unf_list with
+ | first :: others -> CT_unfold (CT_unfold_ne_list (first, others))
+ | [] -> error "there should be at least one thing to unfold")
+ | Fold formula_list ->
+ CT_fold(CT_formula_list(List.map xlate_constr formula_list))
+ | Pattern l ->
+ let pat_list = List.map (fun (nums,c) ->
+ CT_pattern_occ
+ (CT_int_list (List.map (fun x -> CT_int x) nums),
+ xlate_constr c)) l in
+ (match pat_list with
+ | first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
+ | [] -> error "Expecting at least one pattern in a Pattern command")
+ | ExtraRedExpr _ -> xlate_error "TODO: ExtraRedExpr"
+(*
| Node (loc, s, []) ->
(match s with
| "Red" -> CT_red
@@ -1038,14 +1242,20 @@ and xlate_red_tactic =
formula_list))
| Node (_, a, _) -> error ("xlate_red_tactic: unexpected argument " ^ a)
| _ -> error "xlate_red_tactic : unexpected argument"
+*)
and xlate_tactic =
function
- | Node (_, s, l) ->
+(* | Node (_, s, l) ->
(match s, l with
+*)
+(*
| "FUN", [Node(_, "FUNVAR", largs); t] ->
- let fst, rest = xlate_largs_to_id_unit largs in
- CT_tactic_fun
- (CT_id_unit_list(fst, rest), xlate_tactic t)
+*)
+ | TacFun (largs, t) ->
+ let fst, rest = xlate_largs_to_id_unit largs in
+ CT_tactic_fun (CT_id_unit_list(fst, rest), xlate_tactic t)
+ | TacFunRec _ -> xlate_error "Merged with Tactic Definition"
+(*
| "TACTICLIST", (t :: tl) ->
(match List.map xlate_tactic (t::tl) with
| [] -> xlate_error "xlate_tactic: internal xlate_error"
@@ -1054,17 +1264,37 @@ and xlate_tactic =
| xt :: xtl -> CT_then (xt, xtl))
| "TACTICLIST", _ ->
xlate_error "xlate_tactic: malformed tactic-expression TACTICLIST"
+*)
+ | TacThen (t1, t2) ->
+ (match xlate_tactic t1 with
+ | CT_then(t,tl) -> CT_then (t, tl@[xlate_tactic t2])
+ | xt1 -> CT_then (xt1, [xlate_tactic t2]))
+(*
| "TACLIST", (t :: tl) ->
(match List.map xlate_tactic (t::tl) with
| [] -> xlate_error "xlate_tactic: internal xlate_error"
| xt :: [] -> xt
| xt :: xtl -> CT_parallel (xt, xtl))
+*)
+ | TacThens (t, tl) -> CT_parallel (xlate_tactic t, List.map xlate_tactic tl)
+(*
| "FIRST", (a::l) ->
+*)
+ | TacFirst [] -> xlate_error ""
+ | TacFirst (a::l) ->
CT_first(xlate_tactic a,List.map xlate_tactic l)
+(*
| "TCLSOLVE", (a::l) ->
+*)
+ | TacSolve [] -> xlate_error ""
+ | TacSolve (a::l) ->
CT_tacsolve(xlate_tactic a, List.map xlate_tactic l)
+(*
| "DO", ((Num (_, n)) :: (t :: [])) -> CT_do (CT_int n, xlate_tactic t)
| "DO", _ -> xlate_error "xlate_tactic: malformed tactic-expression DO"
+*)
+ | TacDo (n, t) -> CT_do (CT_int n, xlate_tactic t)
+(*
| "TRY", (t :: []) -> CT_try (xlate_tactic t)
| "TRY", _ -> xlate_error "xlate_tactic: malformed tactic-expression TRY"
| "REPEAT", (t :: []) -> CT_repeat (xlate_tactic t)
@@ -1074,12 +1304,27 @@ and xlate_tactic =
| "INFO", (t :: []) -> CT_info (xlate_tactic t)
| "REPEAT", _ ->
xlate_error "xlate_tactic: malformed tactic-expression REPEAT"
+*)
+ | TacTry t -> CT_try (xlate_tactic t)
+ | TacRepeat t -> CT_repeat (xlate_tactic t)
+ | TacAbstract (t, None) -> CT_abstract(ctv_ID_OPT_NONE, (xlate_tactic t))
+ | TacAbstract (t, Some id) ->
+ CT_abstract(ctf_ID_OPT_SOME (xlate_ident id), (xlate_tactic t))
+ | TacInfo t -> CT_info (xlate_tactic t)
+ | TacProgress t -> xlate_error "TODO: Progress t"
+(*
| "ORELSE", (t1 :: (t2 :: [])) ->
CT_orelse (xlate_tactic t1, xlate_tactic t2)
| "ORELSE", _ ->
xlate_error "xlate_tactic: malformed tactic-expression ORELSE"
+*)
+ | TacOrelse (t1, t2) -> CT_orelse (xlate_tactic t1, xlate_tactic t2)
+
+(*
| ((s, l) as it) when (is_tactic_special_case s) ->
tactic_special_case xlate_tactic cvt_arg it
+*)
+(* moved to xlate_call_or_tacarg
| "APP", (Nvar(_,s))::l ->
let args =
List.map (function
@@ -1093,6 +1338,8 @@ and xlate_tactic =
fst::args2 -> fst, args2
| _ -> assert false in
CT_simple_user_tac(CT_ident s, CT_tactic_arg_list(fst, args2))
+*)
+(*
| "MATCH", exp::rules ->
CT_match_tac(mk_let_value exp,
match List.map
@@ -1119,9 +1366,33 @@ and xlate_tactic =
| [] -> assert false
| fst::others ->
CT_match_tac_rules(fst, others))
+*)
+ | TacMatch (exp, rules) ->
+ CT_match_tac(CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body exp),
+ match List.map
+ (function
+ | Pat ([],p,tac) ->
+ CT_match_tac_rule(xlate_context_pattern p,
+ mk_let_value tac)
+ | Pat (_,p,tac) -> xlate_error"No hyps in pure Match"
+ | All tac ->
+ CT_match_tac_rule
+ (CT_coerce_FORMULA_to_CONTEXT_PATTERN
+ CT_existvarc,
+ mk_let_value tac)) rules with
+ | [] -> assert false
+ | fst::others ->
+ CT_match_tac_rules(fst, others))
+
+(*
| "MATCHCONTEXT", rule1::rules ->
+*)
+ | TacMatchContext (_,[]) -> failwith ""
+ | TacMatchContext (lr,rule1::rules) ->
+ (* TODO : traiter la direction "lr" *)
CT_match_context(xlate_context_rule rule1,
List.map xlate_context_rule rules)
+(*
| "LET", [Node(_, "LETDECL",l);
t] ->
let cvt_clause =
@@ -1136,30 +1407,87 @@ and xlate_tactic =
(xlate_tactic v))
| Node(_, s, _) -> failwith ("cvt_clause : unexpected " ^ s)
| _ -> assert false in
+*)
+ | TacLetIn (l, t) ->
+ let cvt_clause =
+ function
+ ((_,s),None,ConstrMayEval v) ->
+ CT_let_clause(xlate_ident s,
+ CT_coerce_DEF_BODY_to_LET_VALUE
+ (formula_to_def_body v))
+ | ((_,s),None,Tacexp t) ->
+ CT_let_clause(xlate_ident s,
+ CT_coerce_TACTIC_COM_to_LET_VALUE
+ (xlate_tactic t))
+ | ((_,s),None,t) ->
+ CT_let_clause(xlate_ident s,
+ CT_coerce_TACTIC_COM_to_LET_VALUE
+ (xlate_call_or_tacarg t))
+ | ((_,s),Some c,v) -> xlate_error "TODO: Let id : c := t In t'" in
let cl_l = List.map cvt_clause l in
(match cl_l with
| [] -> assert false
| fst::others ->
CT_lettac (CT_let_clauses(fst, others), mk_let_value t))
+ | TacLetCut _ -> xlate_error "Unclear future of syntax Let x := t"
+ | TacLetRecIn _ -> xlate_error "TODO: Rec x = t In"
+
+(*
| s, l -> xlate_tac (s, List.map cvt_arg l))
+*)
+ | TacAtom (_, t) -> xlate_tac t
+(* was in xlate_tac *)
+ | TacFail 0 -> CT_fail
+ | TacFail n -> xlate_error "TODO: Fail n"
+ | TacId -> CT_idtac
+(* moved to xlate_call_or_tacarg
| Nvar(_, s) -> ident_tac s
+*)
+(*
| the_node -> xlate_error ("xlate_tactic at " ^
(string_of_node_loc the_node) )
+*)
+ | TacArg a -> xlate_call_or_tacarg a
and xlate_tac =
- function
+ function
+(*
| "Absurd", ((Targ_command c) :: []) -> CT_absurd c
| "Change", [Targ_command f; Targ_id_list b] -> CT_change(f,b)
| "Contradiction", [] -> CT_contradiction
+*)
+ | TacExtend ("Absurd",[c]) ->
+ CT_absurd (xlate_constr (out_gen rawwit_constr c))
+ | TacChange (f, b) -> CT_change (xlate_constr f, xlate_clause b)
+ | TacExtend ("Contradiction",[]) -> CT_contradiction
+(*
| "DoubleInd", ((Targ_int n1) :: ((Targ_int n2) :: [])) ->
- CT_tac_double (n1, n2)
+ CT_tac_double (n1, n2)
+*)
+ | TacDoubleInduction (AnonHyp n1, AnonHyp n2) ->
+ CT_tac_double (CT_int n1, CT_int n2)
+ | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2"
+(*
| "Discr", [] -> CT_discriminate_eq ctv_ID_OPT_NONE
| "DiscrHyp", ((Targ_ident id) :: []) ->
CT_discriminate_eq (ctf_ID_OPT_SOME id)
| "DEqConcl", [] -> CT_simplify_eq ctv_ID_OPT_NONE
| "DEqHyp", ((Targ_ident id) :: []) -> CT_simplify_eq (ctf_ID_OPT_SOME id)
+*)
+ | TacExtend ("Discriminate", [idopt]) ->
+ CT_discriminate_eq
+ (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
+ | TacExtend ("DEq", [idopt]) ->
+ CT_simplify_eq
+ (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
+(*
| "Inj", [] -> CT_injection_eq ctv_ID_OPT_NONE
| "InjHyp", ((Targ_ident id) :: []) -> CT_injection_eq (ctf_ID_OPT_SOME id)
+*)
+ | TacExtend ("Injection", [idopt]) ->
+ CT_injection_eq
+ (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
+(*
| "Fix", ((Targ_int n) :: []) ->
CT_fixtactic (ctv_ID_OPT_NONE, n, CT_fix_tac_list [])
| "Fix", ((Targ_ident id) :: ((Targ_int n) :: fixtac_list)) ->
@@ -1171,40 +1499,126 @@ and xlate_tac =
CT_cofixtactic
(CT_coerce_ID_to_ID_OPT id,
CT_cofix_tac_list (List.map strip_targ_cofixtac cofixtac_list))
+*)
+ | TacFix (idopt, n) ->
+ CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
+ | TacMutualFix (id, n, fixtac_list) ->
+ let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_constr c) in
+ CT_fixtactic
+ (ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
+ CT_fix_tac_list (List.map f fixtac_list))
+ | TacCofix idopt ->
+ CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
+ | TacMutualCofix (id, cofixtac_list) ->
+ let f (id,c) = CT_cofixtac (xlate_ident id, xlate_constr c) in
+ CT_cofixtactic
+ (CT_coerce_ID_to_ID_OPT (xlate_ident id),
+ CT_cofix_tac_list (List.map f cofixtac_list))
+(*
| "IntrosUntil", ((Targ_ident id) :: []) -> CT_intros_until id
+*)
+ | TacIntrosUntil (NamedHyp id) -> CT_intros_until (xlate_ident id)
+ | TacIntrosUntil (AnonHyp n) -> xlate_error "TODO: Intros until n"
+(*
| "IntroMove", [Targ_ident id1;Targ_ident id2] ->
- CT_intro_after(CT_coerce_ID_to_ID_OPT id1, id2)
+*)
+ | TacIntroMove (Some id1, Some (_,id2)) ->
+ CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
+(*
| "IntroMove", [Targ_ident id2] ->
- CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, id2)
+*)
+ | TacIntroMove (None, Some (_,id2)) ->
+ CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_ident id2)
+(*
| "MoveDep", [Targ_ident id1;Targ_ident id2] ->
- CT_move_after(id1, id2)
+*)
+ | TacMove (true, (_,id1), (_,id2)) ->
+ CT_move_after(xlate_ident id1, xlate_ident id2)
+ | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
+(*
| "Intros", [] -> CT_intros (CT_intro_patt_list [])
| "Intros", [patt_list] ->
CT_intros (strip_targ_intropatt patt_list)
+*)
+ | TacIntroPattern [] -> CT_intros (CT_intro_patt_list [])
+ | TacIntroPattern patt_list ->
+ CT_intros (CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
+(*
| "Intro", [Targ_ident (CT_ident id)] ->
- CT_intros (CT_intro_patt_list [CT_coerce_ID_to_INTRO_PATT(CT_ident id)])
+*)
+ | TacIntroMove (Some id, None) ->
+ CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
+ | TacIntroMove (None, None) -> xlate_error "TODO: Intro"
+(*
| "Left", (bindl :: []) -> CT_left (strip_targ_spec_list bindl)
| "Right", (bindl :: []) -> CT_right (strip_targ_spec_list bindl)
| "Split", (bindl :: []) -> CT_split (strip_targ_spec_list bindl)
+*)
+ | TacLeft bindl -> CT_left (xlate_bindings bindl)
+ | TacRight bindl -> CT_right (xlate_bindings bindl)
+ | TacSplit bindl -> CT_split (xlate_bindings bindl)
+(*
| "Replace", ((Targ_command c1) :: ((Targ_command c2) :: [])) ->
CT_replace_with (c1, c2)
+*)
+ | TacExtend ("Replace", [c1; c2]) ->
+ let c1 = xlate_constr (out_gen rawwit_constr c1) in
+ let c2 = xlate_constr (out_gen rawwit_constr c2) in
+ CT_replace_with (c1, c2)
| (*Changes to Equality.v some more rewrite possibilities *)
+(*
"RewriteLR", [(Targ_command c); bindl] ->
CT_rewrite_lr (c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE)
- | "RewriteLRin", ((Targ_ident id) :: ((Targ_command c) :: (bindl::[]))) ->
- CT_rewrite_lr (c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id)
| "RewriteRL", [Targ_command c; bindl] ->
CT_rewrite_rl (c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE)
+*)
+ 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_constr 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)
+(*
+ | "RewriteLRin", ((Targ_ident id) :: ((Targ_command c) :: (bindl::[]))) ->
+ CT_rewrite_lr (c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id)
| "RewriteRLin", [Targ_ident id; Targ_command c; bindl] ->
CT_rewrite_rl (c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id)
+*)
+ | TacExtend ("RewriteIn", [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_constr c and bindl = xlate_bindings bindl in
+ let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+ if b then CT_rewrite_lr (c, bindl, id)
+ else CT_rewrite_rl (c, bindl, id)
+(*
| "CondRewriteLR", [Targ_tacexp t; Targ_command c; bindl] ->
CT_condrewrite_lr (t, c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE)
| "CondRewriteRL", [Targ_tacexp t; Targ_command c; bindl] ->
CT_condrewrite_rl (t, c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE)
+*)
+ | TacExtend ("ConditionalRewrite", [t; b; cbindl]) ->
+ let t = out_gen rawwit_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_constr 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)
+(*
| "CondRewriteLRin", [Targ_tacexp t; Targ_ident id; Targ_command c; bindl] ->
CT_condrewrite_lr (t, c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id)
| "CondRewriteRLin", [Targ_tacexp t; Targ_ident id; Targ_command c; bindl] ->
CT_condrewrite_rl (t, c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id)
+*)
+ | TacExtend ("ConditionalRewriteIn", [t; b; cbindl; id]) ->
+ let t = out_gen rawwit_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_constr c and bindl = xlate_bindings bindl in
+ let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+ if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id)
+ else CT_condrewrite_rl (xlate_tactic t, c, bindl, id)
+(*
| "SubstConcl_LR", ((Targ_command c) :: []) ->
CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
| "SubstHyp_LR", ((Targ_command c) :: ((Targ_ident id) :: [])) ->
@@ -1215,16 +1629,53 @@ and xlate_tac =
CT_cutrewrite_rl (c, ctf_ID_OPT_SOME id)
| "SubstHypInConcl_LR", ((Targ_ident id) :: []) -> CT_deprewrite_lr id
| "SubstHypInConcl_RL", ((Targ_ident id) :: []) -> CT_deprewrite_rl id
+*)
+ | TacExtend ("DependentRewrite", [b; id_or_constr]) ->
+ 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
+ if b then CT_deprewrite_lr id else CT_deprewrite_rl id
+ | ConstrArgType -> (*CutRewrite/SubstConcl*)
+ let c = xlate_constr (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*)
+ let b = out_gen Extraargs.rawwit_orient b in
+ let c = xlate_constr (out_gen rawwit_constr c) in
+ let id = xlate_ident (out_gen rawwit_ident id) in
+ if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
+ else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
+(*
| "Reflexivity", [] -> CT_reflexivity
| "Symmetry", [] -> CT_symmetry
| "Transitivity", ((Targ_command c) :: []) -> CT_transitivity c
+*)
+ | TacReflexivity -> CT_reflexivity
+ | TacSymmetry -> CT_symmetry
+ | TacTransitivity c -> CT_transitivity (xlate_constr c)
+(*
| "Assumption", [] -> CT_assumption
+*)
+ | TacAssumption -> CT_assumption
+(* Moved to xlate_tactic
| "FAIL", [] -> CT_fail
| "IDTAC", [] -> CT_idtac
+*)
+(*
| "Exact", ((Targ_command c) :: []) -> CT_exact c
+*)
+ | TacExact c -> CT_exact (xlate_constr c)
+(*
| "DHyp", [Targ_ident id] -> CT_dhyp id
| "CDHyp", [Targ_ident id] -> CT_cdhyp id
| "DConcl", [] -> CT_dconcl
+*)
+ | TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id)
+ | TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id)
+ | TacDestructConcl -> CT_dconcl
+(*
| "SuperAuto", [a1;a2;a3;a4] ->
CT_superauto(
(match a1 with
@@ -1242,8 +1693,19 @@ and xlate_tac =
| _ -> (CT_coerce_NONE_to_USINGTDB CT_none)))
+*)
+ | TacSuperAuto (nopt,l,a3,a4) ->
+ CT_superauto(
+ xlate_int_opt nopt,
+ xlate_qualid_list l,
+ (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))
+(*
| "AutoTDB", [Targ_int n] -> CT_autotdb (CT_coerce_INT_to_INT_OPT n)
| "AutoTDB", [] -> CT_autotdb (CT_coerce_NONE_to_INT_OPT CT_none)
+*)
+ | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
+(*
| "Auto", ((Targ_int n) :: []) -> CT_auto (CT_coerce_INT_to_INT_OPT n)
| "Auto", ((Targ_string (CT_string "*"))::[])
-> CT_auto_with((CT_coerce_NONE_to_INT_OPT CT_none), CT_star)
@@ -1264,6 +1726,14 @@ and xlate_tac =
idl)))
| "Auto", ((Targ_int n) :: ((Targ_string (CT_string "*")) :: [])) ->
CT_auto_with ((CT_coerce_INT_to_INT_OPT n), CT_star)
+*)
+ | TacAuto (nopt, Some []) -> CT_auto (xlate_int_opt nopt)
+ | TacAuto (nopt, None) -> CT_auto_with (xlate_int_opt nopt, CT_star)
+ | TacAuto (nopt, Some (id1::idl)) ->
+ CT_auto_with(xlate_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)))
+(*
| "EAuto", ((Targ_int n) :: []) -> CT_eauto (CT_coerce_INT_to_INT_OPT n)
| "EAuto", [] -> CT_eauto (CT_coerce_NONE_to_INT_OPT CT_none)
| "EAuto", ((Targ_int n) :: ((Targ_ident id1) :: idl)) ->
@@ -1284,12 +1754,42 @@ and xlate_tac =
CT_eauto_with ((CT_coerce_INT_to_INT_OPT n), CT_star)
| "EAuto", ((Targ_string (CT_string "*"))::[])
-> CT_eauto_with((CT_coerce_NONE_to_INT_OPT CT_none), CT_star)
+*)
+ | TacExtend ("EAuto", [nopt; popt; idl]) ->
+ let control =
+ match out_gen (wit_opt rawwit_int_or_var) nopt with
+ | Some breadth -> Some (true, breadth)
+ | None ->
+ match out_gen (wit_opt rawwit_int_or_var) popt with
+ | Some depth -> Some (false, depth)
+ | None -> None in
+ let idl = out_gen (wit_opt (wit_list0 rawwit_string)) idl in
+ xlate_error "TODO: EAuto n p"
+ (* Something like:
+ match idl with
+ | None -> CT_eauto_with (..., CT_star)
+ | Some [] -> CT_eauto ...
+ | Some (id::l) -> CT_eauto_with (..., ...)
+ *)
+(*
| "Prolog", ((Targ_int n) :: idlist) ->
(*according to coqdev the code is right, they want formula *)
CT_prolog (CT_formula_list (List.map strip_targ_command idlist), n)
- | (**)
+*)
+ | TacExtend ("Prolog", [cl; n]) ->
+ let cl = List.map xlate_constr (out_gen (wit_list0 rawwit_constr) cl) in
+ (match out_gen wit_int_or_var n with
+ | ArgVar _ -> xlate_error ""
+ | ArgArg n -> CT_prolog (CT_formula_list cl, CT_int n))
+(*
"EApplyWithBindings", ((Targ_command c) :: (bindl :: [])) ->
CT_eapply (c, strip_targ_spec_list bindl)
+*)
+ | TacExtend ("EApply", [cbindl]) ->
+ let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
+ let c = xlate_constr c and bindl = xlate_bindings bindl in
+ CT_eapply (c, bindl)
+(*
| "Trivial", [] -> CT_trivial
| "Trivial", ((Targ_string (CT_string "*"))::[]) ->
CT_trivial_with(CT_star)
@@ -1299,25 +1799,61 @@ and xlate_tac =
List.map (function Targ_ident x -> x
| _ -> xlate_error "Trivial expects identifiers")
idl))))
+*)
+ | TacTrivial (Some []) -> CT_trivial
+ | TacTrivial None -> CT_trivial_with(CT_star)
+ | 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))))
+(*
| "Reduce", ((Targ_redexp id) :: ((Targ_id_list l) :: [])) ->
CT_reduce (id, l)
+*)
+ | TacReduce (red, l) ->
+ CT_reduce (xlate_red_tactic red, xlate_clause l)
+(*
| "Apply", ((Targ_command c) :: (bindl :: [])) ->
CT_apply (c, strip_targ_spec_list bindl)
+*)
+ | TacApply (c,bindl) ->
+ CT_apply (xlate_constr c, xlate_bindings bindl)
+(*
| "Constructor", ((Targ_int n) :: (bindl :: [])) ->
CT_constructor (n, strip_targ_spec_list bindl)
+*)
+ | TacConstructor (n_or_meta, bindl) ->
+ let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
+ in CT_constructor (CT_int n, xlate_bindings bindl)
+(*
| "Specialize",
((Targ_int n) :: ((Targ_command c) :: ((Targ_spec_list sl) :: []))) ->
CT_specialize (CT_coerce_INT_to_INT_OPT n, c, sl)
| "Specialize", ((Targ_command c) :: ((Targ_spec_list sl) :: [])) ->
CT_specialize (CT_coerce_NONE_to_INT_OPT CT_none, c, sl)
+*)
+ | TacSpecialize (nopt, (c,sl)) ->
+ CT_specialize (xlate_int_opt nopt, xlate_constr c, xlate_bindings sl)
+(*
| "Generalize", (first :: cl) ->
CT_generalize
(CT_formula_ne_list
(strip_targ_command first, List.map strip_targ_command cl))
| "GeneralizeDep", [Targ_command c] ->
CT_generalize_dependent c
+*)
+ | TacGeneralize [] -> xlate_error ""
+ | TacGeneralize (first :: cl) ->
+ CT_generalize
+ (CT_formula_ne_list (xlate_constr first, List.map xlate_constr cl))
+ | TacGeneralizeDep c ->
+ CT_generalize_dependent (xlate_constr c)
+(*
| "ElimType", ((Targ_command c) :: []) -> CT_elim_type c
| "CaseType", ((Targ_command c) :: []) -> CT_case_type c
+*)
+ | TacElimType c -> CT_elim_type (xlate_constr c)
+ | TacCaseType c -> CT_case_type (xlate_constr c)
+(*
| "Elim", ((Targ_command c1) :: ((Targ_spec_list sl) :: [])) ->
CT_elim (c1, sl, CT_coerce_NONE_to_USING CT_none)
| "Elim",
@@ -1327,28 +1863,67 @@ and xlate_tac =
CT_elim (c1, sl, CT_using (c2, sl2))
| "Case", ((Targ_command c1) :: ((Targ_spec_list sl) :: [])) ->
CT_casetac (c1, sl)
+*)
+ | TacElim ((c1,sl), None) ->
+ CT_elim (xlate_constr c1, xlate_bindings sl,
+ CT_coerce_NONE_to_USING CT_none)
+ | TacElim ((c1,sl), Some (c2,sl2)) ->
+ CT_elim (xlate_constr c1, xlate_bindings sl,
+ CT_using (xlate_constr c2, xlate_bindings sl2))
+ | TacCase (c1,sl) ->
+ CT_casetac (xlate_constr c1, xlate_bindings sl)
+(*
| "Induction", ((Targ_ident id) :: []) ->
CT_induction (CT_coerce_ID_to_ID_OR_INT id)
| "Induction", ((Targ_int n) :: []) ->
CT_induction (CT_coerce_INT_to_ID_OR_INT n)
+*)
+ | TacOldInduction h -> CT_induction (xlate_quantified_hypothesis h)
+(*
| "Destruct", ((Targ_ident id) :: []) ->
CT_destruct (CT_coerce_ID_to_ID_OR_INT id)
| "Destruct", ((Targ_int n) :: []) ->
CT_destruct (CT_coerce_INT_to_ID_OR_INT n)
+*)
+ | TacOldDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
+(*
| "Cut", ((Targ_command c) :: []) -> CT_cut c
+*)
+ | TacCut c -> CT_cut (xlate_constr c)
+(*
| "CutAndApply", ((Targ_command c) :: []) -> CT_use c
+*)
+ | TacLApply c -> CT_use (xlate_constr c)
+(*
| "DecomposeThese", ((Targ_id_list l) :: ((Targ_command c) :: [])) ->
(match l with
CT_id_list (id :: l') ->
CT_decompose_list(
CT_id_ne_list(id,l'),c)
| _ -> xlate_error "DecomposeThese : empty list of identifiers?")
+*)
+ | TacDecompose ([],c) ->
+ xlate_error "Decompose : empty list of identifiers?"
+ | TacDecompose (id::l,c) ->
+ let id' = qualid_or_meta_to_ct_ID id in
+ let l' = List.map qualid_or_meta_to_ct_ID l in
+ CT_decompose_list(CT_id_ne_list(id',l'),xlate_constr c)
+ | TacDecomposeAnd c -> xlate_error "TODO: Decompose Record"
+ | TacDecomposeOr c -> xlate_error "TODO: Decompose Sum"
+(*
| "Clear", [id_list] ->
(match id_list with
Targ_id_list(CT_id_list(id::idl)) ->
CT_clear (CT_id_ne_list (id, idl))
| _ -> xlate_error "Clear expects a non empty list of identifiers")
+*)
+ | TacClear [] ->
+ xlate_error "Clear expects a non empty list of identifiers"
+ | TacClear (id::idl) ->
+ let idl' = List.map ident_or_meta_to_ct_ID idl in
+ CT_clear (CT_id_ne_list (ident_or_meta_to_ct_ID id, idl'))
| (*For translating tactics/Inv.v *)
+(*
"Inv", [Targ_string (CT_string s); Targ_ident id] ->
CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list [])
| "InvIn", ((Targ_ident (CT_ident s))::((Targ_ident id) :: idlist)) ->
@@ -1362,15 +1937,107 @@ and xlate_tac =
((Targ_ident id) :: ((Targ_command c) :: []))) ->
CT_depinversion
(compute_INV_TYPE_from_string s, id, CT_coerce_FORMULA_to_FORMULA_OPT c)
+*)
+ TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s, [id]) ->
+ let id = xlate_ident (out_gen rawwit_ident id) in
+ CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list [])
+ | TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s,
+ [id;copt_or_idl]) ->
+ let id = xlate_ident (out_gen rawwit_ident id) in
+ (match genarg_tag copt_or_idl with
+ | List1ArgType IdentArgType -> (* InvIn *)
+ let idl = out_gen (wit_list1 rawwit_ident) copt_or_idl in
+ CT_inversion (compute_INV_TYPE_from_string s, id,
+ CT_id_list (List.map xlate_ident idl))
+ | OptArgType ConstrArgType -> (* DInv *)
+ let copt = out_gen (wit_opt rawwit_constr) copt_or_idl in
+ CT_depinversion
+ (compute_INV_TYPE_from_string s, id, xlate_constr_opt copt)
+ | _ -> xlate_error "")
+(*
| "UseInversionLemma", ((Targ_ident id) :: ((Targ_command c) :: [])) ->
CT_use_inversion (id, c, CT_id_list [])
| "UseInversionLemmaIn", ((Targ_ident id) :: ((Targ_command c) :: idlist)) ->
CT_use_inversion (id, c, CT_id_list (List.map strip_targ_ident idlist))
+*)
+ | TacExtend ("InversionUsing", [id; c]) ->
+ let id = xlate_ident (out_gen rawwit_ident id) in
+ let c = out_gen rawwit_constr c in
+ CT_use_inversion (id, xlate_constr c, CT_id_list [])
+ | TacExtend ("InversionUsing", [id; c; idlist]) ->
+ let id = xlate_ident (out_gen rawwit_ident id) in
+ let c = out_gen rawwit_constr c in
+ let idlist = out_gen (wit_list1 rawwit_ident) idlist in
+ CT_use_inversion (id, xlate_constr c,
+ CT_id_list (List.map xlate_ident idlist))
+(*
| "Omega", [] -> CT_omega
+*)
+ | TacExtend ("Omega", []) -> CT_omega
+(*
| "APP", (Targ_ident id)::l ->
CT_user_tac (id, CT_targ_list (List.map coerce_iTARG_to_TARG l))
+*)
+ | TacRename (_, _) -> xlate_error "TODO: Rename id into id'"
+ | TacClearBody _ -> xlate_error "TODO: Clear Body H"
+ | TacDAuto (_, _) -> xlate_error "TODO: DAuto"
+ | TacNewDestruct _ -> xlate_error "TODO: NewDestruct"
+ | TacNewInduction _ -> xlate_error "TODO: NewInduction"
+ | TacInstantiate (_, _) -> xlate_error "TODO: Instantiate"
+ | TacLetTac (_, _, _) -> xlate_error "TODO: LetTac"
+ | TacForward (_, _, _) -> xlate_error "TODO: Assert/Pose id:=c"
+ | TacTrueCut (_, _) -> xlate_error "TODO: Assert id:t"
+ | TacAnyConstructor tacopt -> xlate_error "TODO: Constructor tac"
+(*
| s, l ->
CT_user_tac (CT_ident s, CT_targ_list (List.map coerce_iTARG_to_TARG l))
+*)
+ | TacExtend (id, l) ->
+ CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
+ | TacAlias (_, _, _) -> xlate_error "TODO: aliases"
+
+and coerce_genarg_to_TARG x =
+ match Genarg.genarg_tag x with
+ (* Basic types *)
+ | BoolArgType -> xlate_error "TODO: generic boolean argument"
+ | IntArgType ->
+ let n = out_gen rawwit_int x in
+ CT_coerce_ID_OR_INT_to_TARG (CT_coerce_INT_to_ID_OR_INT (CT_int n))
+ | IntOrVarArgType ->
+ let x = match out_gen rawwit_int_or_var x with
+ | ArgArg n -> CT_coerce_INT_to_ID_OR_INT (CT_int n)
+ | ArgVar (_,id) -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id) in
+ CT_coerce_ID_OR_INT_to_TARG x
+ | StringArgType ->
+ let s = CT_string (out_gen rawwit_string x) in
+ CT_coerce_ID_OR_STRING_to_TARG (CT_coerce_STRING_to_ID_OR_STRING s)
+ | PreIdentArgType ->
+ let id = CT_ident (out_gen rawwit_pre_ident x) in
+ CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
+ | IdentArgType ->
+ let id = xlate_ident (out_gen rawwit_ident x) in
+ CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
+ | QualidArgType ->
+ let id = tac_qualid_to_ct_ID (snd (out_gen rawwit_qualid x)) in
+ CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
+ (* Specific types *)
+ | ConstrArgType ->
+ CT_coerce_FORMULA_to_TARG (xlate_constr (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
+ CT_coerce_TACTIC_COM_to_TARG t
+ | CastedOpenConstrArgType -> xlate_error "TODO: open constr"
+ | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
+ | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
+ | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
+ | List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
+ | OptArgType x -> xlate_error "TODO: optional generic arguments"
+ | PairArgType (u,v) -> xlate_error "TODO: pairs of generic arguments"
+ | ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
+
+(*
and (xlate_context_rule: Ctast.t -> ct_CONTEXT_RULE) =
function
| Node(_, "MATCHCONTEXTRULE", parts) ->
@@ -1384,6 +2051,16 @@ and (xlate_context_rule: Ctast.t -> ct_CONTEXT_RULE) =
let hyps, cpat, tactic = xlate_ctxt_rule_aux parts in
CT_context_rule(CT_context_hyp_list hyps, cpat, tactic)
| _ -> assert false
+*)
+and xlate_context_rule =
+ function
+ | Pat (hyps, concl_pat, tactic) ->
+ CT_context_rule(
+ CT_context_hyp_list (List.map xlate_match_context_hyps hyps),
+ xlate_context_pattern concl_pat, xlate_tactic tactic)
+ | All te ->
+ xlate_error "TODO: wildcard match_context_rule"
+(*
and (formula_to_def_body : Ctast.t -> ct_DEF_BODY) =
function
| Node(_, "EVAL", [f;Node(_, "REDEXP", [tac])]) ->
@@ -1404,11 +2081,29 @@ and (formula_to_def_body : Ctast.t -> ct_DEF_BODY) =
| _ ->
failwith("error raised inside formula_to_def_body (3) " ^
s))
+*)
+and formula_to_def_body =
+ function
+ | ConstrEval (red, f) ->
+ CT_coerce_EVAL_CMD_to_DEF_BODY(
+ CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
+ xlate_red_tactic red, xlate_constr f))
+ | ConstrContext _ -> xlate_error "TODO: Inst"
+ | ConstrTypeOf _ -> xlate_error "TODO: Check"
+ | ConstrTerm c -> ct_coerce_FORMULA_to_DEF_BODY(xlate_constr c)
+
+(*
and mk_let_value = function
Node(_, "COMMAND", [v]) ->
CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body v)
| v -> CT_coerce_TACTIC_COM_to_LET_VALUE(xlate_tactic v);;
+*)
+and mk_let_value = function
+ TacArg (ConstrMayEval v) ->
+ CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body v)
+ | v -> CT_coerce_TACTIC_COM_to_LET_VALUE(xlate_tactic v);;
+(*
let strip_varg_int =
function
| Varg_int n -> n
@@ -1428,14 +2123,75 @@ let strip_varg_binder =
function
| Varg_binder n -> n
| _ -> xlate_error "strip vernac: non-binder argument";;
-
+*)
+
+let coerce_genarg_to_VARG x =
+ match Genarg.genarg_tag x with
+ (* Basic types *)
+ | BoolArgType -> xlate_error "TODO: generic boolean argument"
+ | IntArgType ->
+ let n = out_gen rawwit_int x in
+ CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT (CT_int n))
+ | IntOrVarArgType ->
+ (match out_gen rawwit_int_or_var x with
+ | ArgArg n ->
+ CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT (CT_int n))
+ | ArgVar (_,id) ->
+ CT_coerce_ID_OPT_OR_ALL_to_VARG
+ (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
+ (CT_coerce_ID_to_ID_OPT (xlate_ident id))))
+ | StringArgType ->
+ let s = CT_string (out_gen rawwit_string x) in
+ CT_coerce_STRING_OPT_to_VARG (CT_coerce_STRING_to_STRING_OPT s)
+ | PreIdentArgType ->
+ let id = CT_ident (out_gen rawwit_pre_ident 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))
+ | IdentArgType ->
+ let id = xlate_ident (out_gen rawwit_ident 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))
+ | QualidArgType ->
+ let id = tac_qualid_to_ct_ID (snd (out_gen rawwit_qualid 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))
+ (* Specific types *)
+ | ConstrArgType ->
+ CT_coerce_FORMULA_OPT_to_VARG
+ (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_constr (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
+ CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
+ | CastedOpenConstrArgType -> xlate_error "TODO: open constr"
+ | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
+ | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
+ | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
+ | List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
+ | OptArgType x -> xlate_error "TODO: optional generic arguments"
+ | PairArgType (u,v) -> xlate_error "TODO: pairs of generic arguments"
+ | 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"
| _ -> xlate_error "xlate_thm");;
+*)
+let xlate_thm x = CT_thm (match x with
+ | Theorem -> "Theorem"
+ | Remark -> "Remark"
+ | Lemma -> "Lemma"
+ | Fact -> "Fact"
+ | Decl -> "Decl")
+(*
let xlate_defn x = CT_defn (match x with
| "DEFINITION" -> "Definition"
| "LOCAL" -> "Local"
@@ -1448,12 +2204,26 @@ let xlate_defn x = CT_defn (match x with
| "COERCION" -> "Coercion"
| "LCOERCION" -> "LCOERCION"
| _ -> xlate_error "xlate_defn");;
+*)
+let xlate_defn x = CT_defn (match x with
+ | LocalDefinition -> "Local"
+ | Definition -> "Definition")
+(*
let xlate_defn_or_thm s =
try CT_coerce_THM_to_DEFN_OR_THM (xlate_thm s)
with
| _ -> CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn s);;
+*)
+let xlate_defn_or_thm =
+ function
+ (* Unable to decide if a fact in one section or at toplevel, a remark
+ at toplevel or a theorem or a Definition *)
+ | StartTheoremProof k -> CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k)
+ | StartDefinitionBody k -> CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k);;
+
+(*
let xlate_var x = CT_var (match x with
| "HYPOTHESES" -> "Hypothesis"
| "HYPOTHESIS" -> "Hypothesis"
@@ -1466,15 +2236,28 @@ let xlate_var x = CT_var (match x with
"Axiom" as s -> s
| "Parameter" as s -> s
| _ -> xlate_error "xlate_var");;
+*)
+let xlate_var x = CT_var (match x with
+ | AssumptionParameter -> "Parameter"
+ | AssumptionAxiom -> "Axiom"
+ | AssumptionVariable -> "Variable"
+ | AssumptionHypothesis -> "Hypothesis");;
+(*
let xlate_dep =
function
| "DEP" -> CT_dep "Induction for"
| "NODEP" -> CT_dep "Minimality for"
| _ -> xlate_error "xlate_dep";;
+*)
+let xlate_dep =
+ function
+ | true -> CT_dep "Induction for"
+ | false -> CT_dep "Minimality for";;
let xlate_locn =
function
+(*
| Varg_int n -> CT_coerce_INT_to_INT_OR_LOCN n
| Varg_string (CT_string "top") ->
CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "top")
@@ -1483,6 +2266,22 @@ let xlate_locn =
| Varg_string (CT_string "next") ->
CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "next")
| _ -> xlate_error "xlate_locn";;
+*)
+ | GoTo n -> CT_coerce_INT_to_INT_OR_LOCN (CT_int n)
+ | GoTop -> CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "top")
+ | GoPrev -> CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "prev")
+ | GoNext -> CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "next")
+
+let xlate_search_restr =
+ function
+ | SearchOutside [] -> CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none
+ | SearchInside (m1::l1) ->
+ CT_in_modules (CT_id_ne_list(loc_qualid_to_ct_ID m1,
+ List.map loc_qualid_to_ct_ID l1))
+ | SearchOutside (m1::l1) ->
+ CT_out_modules (CT_id_ne_list(loc_qualid_to_ct_ID m1,
+ List.map loc_qualid_to_ct_ID l1))
+ | SearchInside [] -> xlate_error "bad extra argument for Search"
let xlate_check =
function
@@ -1491,18 +2290,12 @@ let xlate_check =
| _ -> xlate_error "xlate_check";;
let build_constructors l =
- let strip_coerce =
- function
- | CT_coerce_ID_to_ID_OPT id -> id
- | _ -> xlate_error "build_constructors" in
- let rec rebind =
- function
- | [] -> []
- | (CT_binder ((CT_id_opt_ne_list (id, ids)), c)) :: l ->
- (List.map (function id_opt -> CT_constr (strip_coerce id_opt, c))
- (id::ids)) @ rebind l in
- CT_constr_list (rebind l);;
+ let f (id,coe,c) =
+ if coe then xlate_error "TODO: coercions in constructors"
+ else CT_constr (xlate_ident id, xlate_constr c) in
+ CT_constr_list (List.map f l)
+(*
let build_record_field_list l =
let build_record_field =
function
@@ -1515,6 +2308,17 @@ let build_record_field_list l =
CT_constr_coercion (id, coerce_iVARG_to_FORMULA c)
| _ -> xlate_error "unexpected field in build_record_field_list" in
CT_recconstr_list (List.map build_record_field l);;
+*)
+let build_record_field_list l =
+ let build_record_field (coe,d) = match d with
+ | AssumExpr (id,c) ->
+ if coe then CT_constr_coercion (xlate_ident id, xlate_constr c)
+ else
+ CT_coerce_CONSTR_to_RECCONSTR
+ (CT_constr (xlate_ident id, xlate_constr c))
+ | DefExpr (id,c,topt) ->
+ xlate_error "TODO: manifest fields in Record" in
+ CT_recconstr_list (List.map build_record_field l);;
let xlate_ast =
let rec xlate_ast_aux =
@@ -1540,6 +2344,7 @@ let xlate_ast =
(CT_id_list (List.map (function s -> CT_ident s) sl)) in
xlate_ast_aux;;
+(*
let get_require_flags impexp spec =
let ct_impexp =
match impexp with
@@ -1553,18 +2358,38 @@ let get_require_flags impexp spec =
| CT_string "IMPLEMENTATION" -> ctv_SPEC_OPT_NONE
| CT_string s -> xlate_error ("unexpected Require specification flag " ^ s) in
ct_impexp, ct_spec;;
+*)
+
+let get_require_flags impexp spec =
+ let ct_impexp =
+ match impexp with
+ | false -> CT_import
+ | true -> CT_export in
+ let ct_spec =
+ match spec with
+ | None -> ctv_SPEC_OPT_NONE
+ | Some true -> CT_spec
+ | Some false -> ctv_SPEC_OPT_NONE in
+ ct_impexp, ct_spec;;
let cvt_optional_eval_for_definition c1 optional_eval =
match optional_eval with
- None -> ct_coerce_FORMULA_to_DEF_BODY c1
- | Some (Targ_redexp red_com) ->
+ None -> ct_coerce_FORMULA_to_DEF_BODY (xlate_constr c1)
+ | Some red ->
CT_coerce_EVAL_CMD_to_DEF_BODY(
CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
- red_com,
- c1))
- | _ -> xlate_error
- "bad extra argument (tactic?) for Definition";;
+ xlate_red_tactic red,
+ xlate_constr c1))
+
+let cvt_vernac_binder = function
+ | (id,c) ->
+ CT_binder(CT_id_opt_ne_list (xlate_ident_opt (Some id),[]),xlate_constr c)
+let cvt_vernac_binders args =
+ CT_binder_list(List.map cvt_vernac_binder args)
+
+
+(*
let rec cvt_varg =
function
| Node (_, "VERNACARGLIST", l) -> Varg_varglist (List.map cvt_varg l)
@@ -1611,16 +2436,27 @@ let rec cvt_varg =
(string_of_node_loc it))
| the_node -> failwith ("cvt_varg : " ^ (string_of_node_loc the_node))
and xlate_vernac =
+*)
+let xlate_vernac =
function
+(*
| Node(_, "TACDEF", [Nvar(_,id);
Node(_,"AST",
[Node(_,"FUN",
[Node(_,"FUNVAR",
largs);
tac])])]) ->
- CT_tactic_definition(CT_ident id,
- CT_id_list(List.map xlate_id largs),
+*)
+ | VernacDeclareTacticDefinition (loc,[(_,id),TacFun (largs,tac)]) ->
+ let fst, rest = xlate_largs_to_id_unit largs in
+ let extract = function CT_unit -> xlate_error "TODO: void parameter"
+ | CT_coerce_ID_to_ID_UNIT x -> x in
+ let largs = List.map extract (fst::rest) in
+ CT_tactic_definition(xlate_ident id,
+ (* TODO, replace CT_id_list by CT_id_unit_list *)
+ CT_id_list largs,
xlate_tactic tac)
+(*
| Node(_, "TACDEF", Nvar(_, id)::
((Node(_, "AST",[Node(_, "REC", [vc])])::tl) as the_list)) ->
let x_rec_tacs =
@@ -1639,11 +2475,37 @@ and xlate_vernac =
let fst, others = match x_rec_tacs with
fst::others -> fst, others
| _ -> assert false in
+*)
+ | VernacDeclareTacticDefinition
+ (loc,((id,TacFunRec (largs,tac))::_ as the_list)) ->
+ let x_rec_tacs =
+ List.map
+ (function
+ | ((_,x),TacFunRec ((_,fst),(argl,tac))) ->
+ let fst, rest = xlate_largs_to_id_unit ((Some fst)::argl) in
+ CT_rec_tactic_fun(xlate_ident x,
+ CT_id_unit_list(fst, rest),
+ xlate_tactic tac)
+ | ((_,x),tac) ->
+ CT_rec_tactic_fun(xlate_ident x,
+ (* Pas clair... *)
+ CT_id_unit_list (xlate_id_unit (Some x), []),
+ xlate_tactic tac)) the_list in
+ let fst, others = match x_rec_tacs with
+ fst::others -> fst, others
+ | _ -> assert false in
CT_rec_tactic_definition(CT_rec_tactic_fun_list(fst, others))
+(*
| Node(_, "TACDEF", [Nvar(_,id);Node(_,"AST",[tac])]) ->
- CT_tactic_definition(CT_ident id, CT_id_list[], xlate_tactic tac)
+*)
+ | VernacDeclareTacticDefinition (_,[(_,id),tac]) ->
+ CT_tactic_definition(xlate_ident id, CT_id_list[], xlate_tactic tac)
+ | VernacDeclareTacticDefinition (loc,_) -> xlate_error "Shouldn't occur"
+(*
| Node (_, s, l) ->
(match s, List.map cvt_varg l with
+*)
+(*
| "LoadFile", ((Varg_string verbose) :: ((Varg_string s) :: [])) ->
CT_load (
(match verbose with
@@ -1652,6 +2514,14 @@ and xlate_vernac =
| CT_string s ->
xlate_error ("expecting the keyword Verbose only :" ^ s)),
CT_coerce_STRING_to_ID_OR_STRING s)
+*)
+ | VernacLoad (verbose,s) ->
+ CT_load (
+ (match verbose with
+ | false -> CT_coerce_NONE_to_VERBOSE_OPT CT_none
+ | true -> CT_verbose),
+ CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
+(*
| "Eval",
((Varg_tactic_arg (Targ_redexp tac)) :: ((Varg_constr f) :: tail)) ->
let numopt =
@@ -1659,23 +2529,44 @@ and xlate_vernac =
| (Varg_int i) :: [] -> CT_coerce_INT_to_INT_OPT i
| [] -> CT_coerce_NONE_to_INT_OPT CT_none
| _ -> xlate_error "Eval expects an optional integer" in
- CT_coerce_EVAL_CMD_to_COMMAND(CT_eval (numopt, tac, f))
+*)
+ | VernacCheckMayEval (Some red, numopt, f) ->
+ let red = xlate_red_tactic red in
+ CT_coerce_EVAL_CMD_to_COMMAND
+ (CT_eval (xlate_int_opt numopt, red, xlate_constr f))
+(*
| "PWD", [] -> CT_pwd
| "CD", ((Varg_string str) :: []) -> CT_cd (ctf_STRING_OPT_SOME str)
| "CD", [] -> CT_cd ctf_STRING_OPT_NONE
| "ADDPATH", ((Varg_string str) :: []) -> CT_addpath str
| "RECADDPATH", ((Varg_string str) :: []) -> CT_recaddpath str
| "DELPATH", ((Varg_string str) :: []) -> CT_delpath str
- | "PrintPath", [] -> CT_print_loadpath
| "QUIT", [] -> CT_quit
- | (*ML commands *)
- "AddMLPath", ((Varg_string str) :: []) -> CT_ml_add_path str
+*)
+ | VernacChdir (Some str) -> CT_cd (ctf_STRING_OPT_SOME (CT_string str))
+ | VernacChdir None -> CT_cd ctf_STRING_OPT_NONE
+ | VernacAddLoadPath (false,str,None) -> CT_addpath (CT_string str)
+ | VernacAddLoadPath (true,str,None) -> CT_recaddpath (CT_string str)
+ | VernacAddLoadPath (_,str,Some x) ->
+ xlate_error"TODO: Add (Rec) LoadPath as"
+ | VernacRemoveLoadPath str -> CT_delpath (CT_string str)
+ | VernacToplevelControl Quit -> CT_quit
+ | VernacToplevelControl _ -> xlate_error "TODO?: Drop/ProtectedToplevel"
+ (*ML commands *)
+(*
+ | "AddMLPath", ((Varg_string str) :: []) -> CT_ml_add_path str
| "RecAddMLPath", ((Varg_string str) :: []) -> CT_rec_ml_add_path str
- | "PrintMLPath", [] -> CT_ml_print_path
- | "PrintMLModules", [] -> CT_ml_print_modules
- | "DeclareMLModule", (str :: l) ->
CT_ml_declare_modules
(CT_string_ne_list (strip_varg_string str, List.map strip_varg_string l))
+ | "DeclareMLModule", (str :: l) ->
+*)
+ | VernacAddMLPath (false,str) -> CT_ml_add_path (CT_string str)
+ | VernacAddMLPath (true,str) -> CT_rec_ml_add_path (CT_string str)
+ | VernacDeclareMLModule [] -> failwith ""
+ | VernacDeclareMLModule (str :: l) ->
+ CT_ml_declare_modules
+ (CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l))
+(*
| "GOAL", [] -> CT_proof_no_op
| "GOAL", (c :: []) -> CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (coerce_iVARG_to_FORMULA c))
| (*My attempt at getting all variants of Abort to use abort node *)
@@ -1690,6 +2581,17 @@ and xlate_vernac =
| "FOCUS", [] -> CT_focus (CT_coerce_NONE_to_INT_OPT CT_none)
| "FOCUS", [Varg_int n] -> CT_focus (CT_coerce_INT_to_INT_OPT n)
| "UNFOCUS", [] -> CT_unfocus
+*)
+ | VernacStartProof (_, None, c, _, _) ->
+ CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_constr c))
+ | VernacAbort (Some id) -> CT_abort(ctf_ID_OPT_OR_ALL_SOME(xlate_ident id))
+ | VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
+ | VernacAbortAll -> CT_abort ctv_ID_OPT_OR_ALL_ALL
+ | VernacRestart -> CT_restart
+ | VernacSolve (n, tac) -> CT_solve (CT_int n, xlate_tactic tac)
+ | VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
+ | VernacUnfocus -> CT_unfocus
+(*
| "HintRewrite", [orient; formula_list; Varg_ident base; Varg_tactic t] ->
let ct_orient = match orient with
| Varg_string (CT_string "LR") -> CT_lr
@@ -1698,7 +2600,23 @@ and xlate_vernac =
let f_ne_list = match formula_list with
Varg_constrlist (fst::rest) -> CT_formula_ne_list(fst,rest)
| _ -> assert false in
- CT_hintrewrite(ct_orient, f_ne_list, base, t)
+*)
+ | VernacExtend ("HintRewrite", orient :: formula_list :: base :: t) ->
+ let orient = out_gen rawwit_bool orient in
+ let formula_list = out_gen (wit_list1 (rawwit_constr)) formula_list in
+ let base = out_gen rawwit_pre_ident base in
+ let t = match t with
+ | [] -> TacId
+ | [t] -> out_gen rawwit_tactic t
+ | _ -> failwith "" in
+ let ct_orient = match orient with
+ | true -> CT_lr
+ | false -> CT_rl in
+ let f_ne_list = match List.map xlate_constr formula_list with
+ (fst::rest) -> CT_formula_ne_list(fst,rest)
+ | _ -> assert false in
+ CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
+(*
| "HintResolve",
((Varg_ident id_name) ::
((Varg_varglist dbnames) :: ((Varg_constr c)::[]))) ->
@@ -1731,6 +2649,24 @@ and xlate_vernac =
Varg_tactic t] ->
CT_hint(id_name, CT_id_list (List.map coerce_iVARG_to_ID dbnames),
CT_extern(n, c, t))
+*)
+ | VernacHints (dbnames,h) ->
+ let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
+ (match h with
+ | HintsResolve [Some id_name, c] -> (* = Old HintResolve *)
+ CT_hint(xlate_ident id_name, dblist, CT_resolve (xlate_constr c))
+ | HintsImmediate [Some id_name, c] -> (* = Old HintImmediate *)
+ CT_hint(xlate_ident id_name, dblist, CT_immediate(xlate_constr c))
+ | HintsUnfold [Some id_name, q] -> (* = Old HintUnfold *)
+ CT_hint(xlate_ident id_name, dblist,
+ CT_unfold_hint (loc_qualid_to_ct_ID q))
+ | HintsConstructors (id_name, q) ->
+ CT_hint(xlate_ident id_name, dblist,
+ CT_constructors (loc_qualid_to_ct_ID q))
+ | HintsExtern (id_name, n, c, t) ->
+ CT_hint(xlate_ident id_name, dblist,
+ CT_extern(CT_int n, xlate_constr c, xlate_tactic t))
+(*
| "HintsResolve",
(Varg_varglist(dbnames)::(Varg_ident n1) :: names) ->
CT_hints(CT_ident "Resolve",
@@ -1746,7 +2682,44 @@ and xlate_vernac =
CT_hints(CT_ident "Unfold",
CT_id_ne_list(n1, List.map coerce_iVARG_to_ID names),
CT_id_list(List.map coerce_iVARG_to_ID dbnames))
+*)
+ | HintsResolve l -> (* = Old HintsResolve *)
+ let l = List.map
+ (function
+ (None,Coqast.Node(_,"QUALID",l)) -> Astterm.interp_qualid l
+ | _ -> failwith "") l in
+ let n1, names = match List.map tac_qualid_to_ct_ID l with
+ n1 :: names -> n1, names
+ | _ -> failwith "" in
+ CT_hints(CT_ident "Resolve",
+ CT_id_ne_list(n1, names),
+ dblist)
+ | HintsImmediate l -> (* = Old HintsImmediate *)
+ let l = List.map
+ (function
+ (None,Coqast.Node(_,"QUALID",l)) -> Astterm.interp_qualid l
+ | _ -> failwith "") l in
+ let n1, names = match List.map tac_qualid_to_ct_ID l with
+ n1 :: names -> n1, names
+ | _ -> failwith "" in
+ CT_hints(CT_ident "Immediate",
+ CT_id_ne_list(n1, names),
+ dblist)
+ | HintsUnfold l -> (* = Old HintsUnfold *)
+ let l = List.map
+ (function
+ (None,qid) -> loc_qualid_to_ct_ID qid
+ | _ -> failwith "") l in
+ let n1, names = match l with
+ n1 :: names -> n1, names
+ | _ -> failwith "" in
+ CT_hints(CT_ident "Unfold",
+ CT_id_ne_list(n1, names),
+ dblist))
+(* Obsolete
| "BY", ((Varg_tactic tcom) :: []) -> xlate_error "BY not implemented"
+*)
+(*
| (*My attempt to get all variants of Save to use the same node *)
"SaveNamed", [] ->
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
@@ -1764,33 +2737,101 @@ and xlate_vernac =
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm kind_string), ctf_ID_OPT_SOME s)
| "SaveAnonymous", [Varg_ident s] ->
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctf_ID_OPT_SOME s)
+*)
+ | VernacEndProof (true,None) ->
+ CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
+ | VernacEndProof (false,None) ->
+ CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE)
+ | VernacEndProof (b,Some (s, Some kind)) ->
+ CT_save (CT_coerce_THM_to_THM_OPT (xlate_thm kind),
+ ctf_ID_OPT_SOME (xlate_ident s))
+ | VernacEndProof (b,Some (s,None)) ->
+ CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"),
+ ctf_ID_OPT_SOME (xlate_ident s))
+(*
| "TRANSPARENT", (id :: idl) ->
- CT_transparent(CT_id_ne_list(strip_varg_ident id,
- List.map strip_varg_ident idl))
+*)
+ | VernacSetOpacity (false, id :: idl) ->
+ CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id,
+ List.map loc_qualid_to_ct_ID idl))
+(*
| "OPAQUE", (id :: idl)
- -> CT_opaque (CT_id_ne_list(strip_varg_ident id,
- List.map strip_varg_ident idl))
+*)
+ | VernacSetOpacity (true, id :: idl)
+ -> CT_opaque (CT_id_ne_list(loc_qualid_to_ct_ID id,
+ List.map loc_qualid_to_ct_ID idl))
+ | VernacSetOpacity (_, []) -> xlate_error "Shouldn't occur"
+(* No longer supported
| "WriteModule", ((Varg_ident id) :: []) ->
CT_write_module (id, CT_coerce_NONE_to_STRING_OPT CT_none)
+*)
+(*
| "UNDO", ((Varg_int n) :: []) -> CT_undo (CT_coerce_INT_to_INT_OPT n)
- | "SHOW", [] -> CT_show_goal (CT_coerce_NONE_to_INT_OPT CT_none)
- | "SHOW", ((Varg_int n) :: []) -> CT_show_goal (CT_coerce_INT_to_INT_OPT n)
+*)
+ | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n))
+(*
+ | "SHOW", [] ->
+ | "SHOW", ((Varg_int n) :: []) ->
+*)
+ | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt)
+(*
| "ShowNode", [] -> CT_show_node
| "ShowProof", [] -> CT_show_proof
| "ShowTree", [] -> CT_show_tree
| "ShowScript", [] -> CT_show_script
| "ShowProofs", [] -> CT_show_proofs
| "SHOWIMPL", [] -> CT_show_implicits
+*)
+ | VernacShow ShowNode -> CT_show_node
+ | VernacShow ShowProof -> CT_show_proof
+ | VernacShow ShowTree -> CT_show_tree
+ | VernacShow ShowProofNames -> CT_show_proofs
+ | VernacShow (ShowIntros _|ShowGoalImplicitly _|ShowExistentials|ShowScript)
+ -> xlate_error "TODO: Show Intro/Intros/Implicits/Existentials/Script"
+(*
| "Go", (arg :: []) -> CT_go (xlate_locn arg)
+*)
+ | VernacGo arg -> CT_go (xlate_locn arg)
+(*
| "ExplainProof", l ->
- CT_explain_proof (CT_int_list (List.map strip_varg_int l))
+*)
+ | VernacShow ExplainProof l ->
+ CT_explain_proof (CT_int_list (List.map (fun x -> CT_int x) l))
+(*
| "ExplainProofTree", l ->
- CT_explain_prooftree (CT_int_list (List.map strip_varg_int l))
- | "PrintHint", [] -> CT_print_hint (CT_coerce_NONE_to_ID_OPT CT_none)
- | "PrintHintDb", [Varg_ident id] -> CT_print_hintdb id
+*)
+ | VernacShow ExplainTree l ->
+ CT_explain_prooftree (CT_int_list (List.map (fun x -> CT_int x) l))
+(*
| "CheckGuard", [] -> CT_guarded
- | "PrintHintId", ((Varg_ident id) :: []) ->
- CT_print_hint (CT_coerce_ID_to_ID_OPT id)
+*)
+ | VernacCheckGuard -> CT_guarded
+ | VernacPrint p ->
+ (match p with
+ PrintFullContext -> CT_print_all
+ | PrintName id -> CT_print_id (loc_qualid_to_ct_ID id)
+ | PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id)
+ | PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id)
+ | PrintModules -> CT_print_modules
+ | PrintGrammar (phylum, name) -> CT_print_grammar CT_grammar_none
+ | PrintHintDb -> CT_print_hint (CT_coerce_NONE_to_ID_OPT CT_none)
+ | PrintHintDbName id -> CT_print_hintdb (CT_ident id)
+ | PrintHint id ->
+ CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
+ | PrintLoadPath -> CT_print_loadpath
+ | PrintMLLoadPath -> CT_ml_print_path
+ | PrintMLModules -> CT_ml_print_modules
+ | PrintGraph -> CT_print_graph
+ | PrintClasses -> CT_print_classes
+ | PrintCoercions -> CT_print_coercions
+ | PrintCoercionPaths (id1, id2) ->
+ CT_print_path (xlate_class id1, xlate_class id2)
+ | PrintInspect n -> CT_inspect (CT_int n)
+ | PrintUniverses _ -> xlate_error "TODO: Dump Universes"
+ | PrintHintGoal -> xlate_error "TODO: Print Hint"
+ | PrintLocalContext -> xlate_error "TODO: Print"
+ | PrintTables -> xlate_error "TODO: Print Tables")
+(*
| "PrintAll", [] -> CT_print_all
| "PrintId", ((Varg_ident id) :: []) -> CT_print_id id
| "PrintOpaqueId", ((Varg_ident id) :: []) -> CT_print_opaqueid id
@@ -1799,22 +2840,51 @@ and xlate_vernac =
| "PrintModules", [] -> CT_print_modules
| "PrintGrammar", ((Varg_ident phylum) :: ((Varg_ident name) :: [])) ->
CT_print_grammar CT_grammar_none
+ | "PrintHint", [] -> CT_print_hint (CT_coerce_NONE_to_ID_OPT CT_none)
+ | "PrintHintDb", [Varg_ident id] -> CT_print_hintdb id
+ | "PrintHintId", ((Varg_ident id) :: []) ->
+ | "PrintPath", [] -> CT_print_loadpath
+ | "PrintMLPath", [] -> CT_ml_print_path
+ | "PrintMLModules", [] -> CT_ml_print_modules
+ | "PrintGRAPH", [] -> CT_print_graph
+ | "PrintCLASSES", [] -> CT_print_classes
+ | "PrintCOERCIONS", [] -> CT_print_coercions
+ | "PrintPATH", ((Varg_ident id1) :: ((Varg_ident id2) :: [])) ->
+ CT_print_path (id1, id2)
+ | "INSPECT", ((Varg_int n) :: []) -> CT_inspect n
+*)
+(* No longer supported
| "BeginModule", ((Varg_ident id) :: []) -> CT_module id
+*)
+(*
| "BeginSection", ((Varg_ident id) :: []) ->
- CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section id)
- | "EndSection", ((Varg_ident id) :: []) -> CT_section_end id
+*)
+ | VernacBeginSection id ->
+ CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
+(*
+ | "EndSection", ((Varg_ident id) :: []) ->
+*)
+ | VernacEndSection id -> CT_section_end (xlate_ident id)
+(*
| "StartProof",
((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) ->
+*)
+ | VernacStartProof (kind, Some s, c, _, _) ->
CT_coerce_THEOREM_GOAL_to_COMMAND(
- CT_theorem_goal (xlate_defn_or_thm kind, s, coerce_iVARG_to_FORMULA c))
+ CT_theorem_goal (xlate_defn_or_thm kind, xlate_ident s,xlate_constr c))
+(*
| (*My attempt: suspend and resume as separate nodes *)
"SUSPEND", [] -> CT_suspend
| "RESUME", ((Varg_ident id) :: []) -> CT_resume (ctf_ID_OPT_SOME id)
| "RESUME", [] -> CT_resume ctv_ID_OPT_NONE
- | (*formerly | ("SUSPEND", []) -> suspend(CT_true)
+ (*formerly | ("SUSPEND", []) -> suspend(CT_true)
| ("RESUME", []) -> suspend(CT_false)
*)
- "DEFINITION",
+*)
+ | VernacSuspend -> CT_suspend
+ | VernacResume idopt -> CT_resume (xlate_ident_opt idopt)
+(*
+ | "DEFINITION",
(* reference : toplevel/vernacentries.ml *)
(Varg_string (CT_string kind):: Varg_ident s :: Varg_constr c :: rest) ->
let typ_opt, red_option = match rest with
@@ -1827,17 +2897,29 @@ and xlate_vernac =
CT_coerce_FORMULA_to_FORMULA_OPT
(CT_coerce_SORT_TYPE_to_FORMULA b), None
| _ -> assert false in
- CT_definition
- (xlate_defn kind, s,
- cvt_optional_eval_for_definition c red_option, typ_opt)
+*)
+ | VernacDefinition (kind,s,red_option,c,typ_opt,_) ->
+ CT_definition
+ (xlate_defn kind, xlate_ident s,
+ cvt_optional_eval_for_definition c red_option,
+ xlate_constr_opt typ_opt)
+(*
| "VARIABLE",
((Varg_string (CT_string kind)) :: ((Varg_binderlist b) :: [])) ->
CT_variable (xlate_var kind, b)
| "PARAMETER",
((Varg_string (CT_string kind)) :: ((Varg_binderlist b) :: [])) ->
CT_variable (xlate_var kind, b)
+*)
+ | VernacAssumption (kind, b) ->
+ CT_variable (xlate_var kind, cvt_vernac_binders b)
+(*
| "Check", ((Varg_string (CT_string kind)) :: (c :: [])) ->
CT_check (coerce_iVARG_to_FORMULA c)
+*)
+ | VernacCheckMayEval (None, numopt, c) ->
+ CT_check (xlate_constr c)
+(*
| "SearchPattern",Varg_constr c::l ->
(match l with
| [] -> CT_search_pattern(c,
@@ -1864,7 +2946,15 @@ and xlate_vernac =
| _ -> xlate_error "bad extra argument for Search") in
CT_search(id, modifier)
| _ -> xlate_error "bad argument list for Search")
- | "INSPECT", ((Varg_int n) :: []) -> CT_inspect n
+*)
+ | VernacSearch (s,x) ->
+ (match s with
+ | SearchPattern c ->
+ CT_search_pattern(xlate_constr c, xlate_search_restr x)
+ | SearchHead id ->
+ CT_search(loc_qualid_to_ct_ID id, xlate_search_restr x)
+ | SearchRewrite c -> xlate_error "TODO: SearchRewrite")
+(*
| (*Record from tactics/Record.v *)
"RECORD",
((Varg_string coercion_or_not) :: ((Varg_ident s) ::
@@ -1887,6 +2977,21 @@ and xlate_vernac =
| _ -> assert false),
record_constructor,
build_record_field_list field_list)
+*)
+ | (*Record from tactics/Record.v *)
+ VernacRecord
+ (add_coercion, s, binders, c1, rec_constructor_or_none, field_list) ->
+ let record_constructor = xlate_ident_opt rec_constructor_or_none in
+(* match rec_constructor_or_none with
+ | None -> CT_coerce_NONE_to_ID_OPT CT_none
+ | Some id -> CT_coerce_ID_to_ID_OPT id in
+*) CT_record
+ ((if add_coercion then CT_coercion_atm else
+ CT_coerce_NONE_to_COERCION_OPT(CT_none)),
+ xlate_ident s, cvt_vernac_binders binders, xlate_sort c1, record_constructor,
+ build_record_field_list field_list)
+
+(* TODO
| (*Inversions from tactics/Inv.v *)
"MakeSemiInversionLemmaFromHyp",
((Varg_int n) :: ((Varg_ident id1) :: ((Varg_ident id2) :: []))) ->
@@ -1914,6 +3019,8 @@ and xlate_vernac =
((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) ->
CT_derive_depinversion
(CT_inv_clear, id, coerce_iVARG_to_FORMULA c, sort)
+*)
+(*
|
"ONEINDUCTIVE",
((Varg_string (CT_string f)) ::
@@ -1953,6 +3060,17 @@ and xlate_vernac =
| _ -> xlate_error "mutual inductive" in
CT_mind_decl
(CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
+*)
+ | VernacInductive (isind, lmi) ->
+ let co_or_ind = if isind then "Inductive" else "CoInductive" in
+ let strip_mutind (s, parameters, c, constructors) =
+ CT_ind_spec
+ (xlate_ident s, cvt_vernac_binders parameters, xlate_constr c,
+ build_constructors constructors) in
+ CT_mind_decl
+ (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
+
+(*
| "MUTUALRECURSIVE", ((Varg_varglist (lm :: lmi)) :: []) ->
let strip_mutrec =
function
@@ -1965,6 +3083,19 @@ and xlate_vernac =
| _ -> xlate_error "mutual recursive" in
CT_fix_decl
(CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
+*)
+ | VernacFixpoint [] -> xlate_error "mutual recursive"
+ | VernacFixpoint (lm :: lmi) ->
+ let strip_mutrec (fid, bl, arf, ardef) =
+ match cvt_vernac_binders bl with
+ | CT_binder_list (b :: bl) ->
+ CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
+ xlate_constr arf, xlate_constr ardef)
+ | _ -> xlate_error "mutual recursive" in
+ CT_fix_decl
+ (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
+
+(*
| "MUTUALCORECURSIVE", ((Varg_varglist (lm :: lmi)) :: []) ->
let strip_mutcorec =
function
@@ -1974,6 +3105,15 @@ and xlate_vernac =
| _ -> xlate_error "mutual corecursive" in
CT_cofix_decl
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
+*)
+ | VernacCoFixpoint [] -> xlate_error "mutual corecursive"
+ | VernacCoFixpoint (lm :: lmi) ->
+ let strip_mutcorec (fid, arf, ardef) =
+ CT_cofix_rec (xlate_ident fid, xlate_constr arf, xlate_constr ardef) in
+ CT_cofix_decl
+ (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
+
+(*
| "INDUCTIONSCHEME", ((Varg_varglist (lm :: lmi)) :: []) ->
let strip_ind =
function
@@ -1985,6 +3125,17 @@ and xlate_vernac =
| _ -> xlate_error "induction scheme" in
CT_ind_scheme
(CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
+*)
+ | VernacScheme [] -> xlate_error "induction scheme"
+ | VernacScheme (lm :: lmi) ->
+ let strip_ind (id, depstr, inde, sort) =
+ CT_scheme_spec
+ (xlate_ident id, xlate_dep depstr,
+ CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
+ xlate_sort sort) in
+ CT_ind_scheme
+ (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
+(*
|
"SyntaxMacro", ((Varg_ident id) :: (c :: [])) ->
CT_syntax_macro
@@ -1992,31 +3143,53 @@ and xlate_vernac =
| "SyntaxMacro", ((Varg_ident id) :: (c :: ((Varg_int n) :: []))) ->
CT_syntax_macro
(id, coerce_iVARG_to_FORMULA c, CT_coerce_INT_to_INT_OPT n)
+*)
+ | VernacSyntacticDefinition (id, c, nopt) ->
+ CT_syntax_macro (xlate_ident id, xlate_constr c, xlate_int_opt nopt)
+
+(* Obsolete
| "ABSTRACTION", ((Varg_ident id) :: (c :: l)) ->
CT_abstraction
(id, coerce_iVARG_to_FORMULA c, CT_int_list (List.map strip_varg_int l))
+*)
+(*
| "Require",
((Varg_string impexp) ::
((Varg_string spec) :: ((Varg_ident id) :: []))) ->
+*)
+ | VernacRequire (None, spec, lid) -> xlate_error "TODO: Read Module"
+ | VernacRequire (Some impexp, spec, [id]) ->
let ct_impexp, ct_spec = get_require_flags impexp spec in
- CT_require (ct_impexp, ct_spec, id, CT_coerce_NONE_to_STRING_OPT CT_none)
+ CT_require (ct_impexp, ct_spec, loc_qualid_to_ct_ID id,
+ CT_coerce_NONE_to_STRING_OPT CT_none)
+ | VernacRequire (_,_,([]|_::_::_)) ->
+ xlate_error "TODO: general form of future Require"
+(*
| "RequireFrom",
((Varg_string impexp) ::
((Varg_string spec) ::
((Varg_ident id) :: ((Varg_string filename) :: [])))) ->
+*)
+ | VernacRequireFrom (impexp, spec, id, filename) ->
let ct_impexp, ct_spec = get_require_flags impexp spec in
CT_require
- (ct_impexp, ct_spec, id, CT_coerce_STRING_to_STRING_OPT filename)
+ (ct_impexp, ct_spec, xlate_ident id,
+ CT_coerce_STRING_to_STRING_OPT (CT_string filename))
+(*
| "SYNTAX", ((Varg_ident phylum) :: ((Varg_ident s) :: (x :: (y :: l)))) ->
- xlate_error "SYNTAX not implemented"
- | (*Two versions of the syntax node with and without the binder list. *)
+*)
+ | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
+ (*Two versions of the syntax node with and without the binder list. *)
(*Need to update the metal file and ascent.mli first!
| ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg; blist]) ->
(syntaxop phy s spatarg unparg blist)
| ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg]) ->
(syntaxop phy s spatarg unparg
coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*)
+(* Token is obsolete (automatically done by Grammar) and with no effects
"TOKEN", ((Varg_string str) :: []) -> CT_token str
+*)
+(*
| "INFIX",
((Varg_ast (CT_coerce_ID_OR_STRING_to_AST
(CT_coerce_STRING_to_ID_OR_STRING
@@ -2029,11 +3202,26 @@ and xlate_vernac =
| "NONA" -> CT_nona
| "NONE" -> CT_coerce_NONE_to_ASSOC CT_none
| _ -> xlate_error "infix1"), n, str, id)
+*)
+ | VernacInfix (str_assoc, n, str, id) ->
+ CT_infix (
+ (match str_assoc with
+ | Some Gramext.LeftA -> CT_lefta
+ | Some Gramext.RightA -> CT_righta
+ | Some Gramext.NonA -> CT_nona
+ | None -> CT_coerce_NONE_to_ASSOC CT_none),
+ CT_int n, CT_string str, loc_qualid_to_ct_ID id)
+(*
| "GRAMMAR", (ge :: []) -> xlate_error "GRAMMAR not implemented"
+*)
+ | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
+(* Undo and Hyps Limit are now handled through the global options entries
| "SETUNDO", ((Varg_int n) :: []) -> CT_setundo n
| "UNSETUNDO", [] -> CT_unsetundo
| "SETHYPSLIMIT", ((Varg_int n) :: []) -> CT_sethyp n
| "UNSETHYPSLIMIT", [] -> CT_unsethyp
+*)
+(*
| "COERCION",
((Varg_string (CT_string s)) ::
((Varg_string (CT_string str)) ::
@@ -2049,12 +3237,32 @@ and xlate_vernac =
| "" -> CT_coerce_NONE_to_LOCAL_OPT CT_none
| _ -> xlate_error "unknown flag for a coercion2" in
CT_coercion (local_opt, id_opt, id1, id2, id3)
+*)
+ | VernacCoercion (s, id1, id2, id3) ->
+ let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
+ let local_opt =
+ match s with
+ (* Cannot decide whether it is a global or a Local but at toplevel *)
+ | Nametab.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+ | Nametab.DischargeAt _ -> CT_local
+ | Nametab.NotDeclare -> assert false in
+ CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1,
+ xlate_class id2, xlate_class id3)
+
+ | VernacIdentityCoercion (s, id1, id2, id3) ->
+ let id_opt = CT_identity in
+ let local_opt =
+ match s with
+ (* Cannot decide whether it is a global or a Local but at toplevel *)
+ | Nametab.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+ | Nametab.DischargeAt _ -> CT_local
+ | Nametab.NotDeclare -> assert false in
+ CT_coercion (local_opt, id_opt, xlate_ident id1,
+ xlate_class id2, xlate_class id3)
+(* Not supported
| "CLASS", (_ :: ((Varg_ident id1) :: [])) -> CT_class id1
- | "PrintGRAPH", [] -> CT_print_graph
- | "PrintCLASSES", [] -> CT_print_classes
- | "PrintCOERCIONS", [] -> CT_print_coercions
- | "PrintPATH", ((Varg_ident id1) :: ((Varg_ident id2) :: [])) ->
- CT_print_path (id1, id2)
+*)
+(* Natural entries are currently not supported
| "SelectLanguageText", ((Varg_ident id) :: []) -> CT_set_natural id
| "PrintText", ((Varg_ident id) :: []) -> CT_print_natural id
| "AddTextParamOmit", ((Varg_ident id) :: []) ->
@@ -2079,9 +3287,17 @@ and xlate_vernac =
CT_remove_natural_feature (CT_nat_transparent, id)
| "PrintTextParamImmediate", [] ->
CT_print_natural_feature CT_nat_transparent
+*)
+(*
| "ResetName", ((Varg_ident id) :: []) -> CT_reset id
- | "ResetSection", ((Varg_ident id) :: []) -> CT_reset_section id
| "ResetInitial", [] -> CT_restore_state (CT_ident "Initial")
+*)
+ | VernacResetName id -> CT_reset (xlate_ident id)
+ | VernacResetInitial -> CT_restore_state (CT_ident "Initial")
+(* No longer supported
+ | "ResetSection", ((Varg_ident id) :: []) -> CT_reset_section id
+*)
+(* Omega flags are handled through the global options entries
| "OmegaFlag", ((Varg_string (CT_string s)) :: []) ->
let fst_code = code (get s 0) in
let
@@ -2096,13 +3312,26 @@ and xlate_vernac =
| _ ->
CT_omega_flag
(set_or_unset, CT_coerce_STRING_to_OMEGA_FEATURE (CT_string s)))
- | s, l ->
+*)
+ | VernacExtend (s, l) ->
CT_user_vernac
- (CT_ident s, CT_varg_list (List.map coerce_iVARG_to_VARG l)))
- | _ -> xlate_error "xlate_vernac";;
+ (CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
+ | VernacDebug b -> xlate_error "TODO: Debug On/Off"
+
+ | VernacList l -> xlate_error "Not treated here"
+ | (VernacLocate _|VernacGlobalCheck _|VernacPrintOption _|
+ VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
+ VernacSetOption (_, _)|VernacUnsetOption _|VernacDeclareImplicits (_, _)|
+ VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _|
+ VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
+ VernacImport (_, _)|VernacExactProof _|VernacDistfix (_, _, _, _)|
+ VernacTacticGrammar _|VernacVar _|VernacTime _|VernacNop|VernacComments _)
+ -> xlate_error "TODO: vernac"
let xlate_vernac_list =
function
- | Node (_, "vernac_list", (v :: l)) ->
- CT_command_list (xlate_vernac v, List.map xlate_vernac l)
- | _ -> xlate_error "xlate_command_list";;
+ | VernacList (v::l) ->
+ CT_command_list
+ (xlate_vernac (snd v), List.map (fun (_,x) -> xlate_vernac x) l)
+ | VernacList [] -> xlate_error "xlate_command_list"
+ | _ -> xlate_error "Not a list of commands";;
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index b93635e473..0e9fd223fa 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -1,12 +1,12 @@
open Ascent;;
-val xlate_vernac : Ctast.t -> ct_COMMAND;;
-val xlate_tactic : Ctast.t -> ct_TACTIC_COM;;
+val xlate_vernac : Vernacexpr.vernac_expr -> ct_COMMAND;;
+val xlate_tactic : Tacexpr.raw_tactic_expr -> ct_TACTIC_COM;;
val xlate_formula : Ctast.t -> ct_FORMULA;;
val xlate_int : Ctast.t -> ct_INT;;
val xlate_string : Ctast.t -> ct_STRING;;
-val xlate_id : Ctast.t -> ct_ID;;
-val xlate_vernac_list : Ctast.t -> ct_COMMAND_LIST;;
+val xlate_ident : Names.identifier -> ct_ID;;
+val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;;
val g_nat_syntax_flag : bool ref;;
val set_flags : (unit -> unit) ref;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 04:49:40 +0000