aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorbertot2002-10-03 13:47:12 +0000
committerbertot2002-10-03 13:47:12 +0000
commit84566056d2f020347d781b10f97d77155ed45a95 (patch)
tree5a1e81f21efb7dc131ce34c1acf85cde8578fe63
parent8aa4056506b595584f1215a842cfd9693694a2ed (diff)
Previous version did compile but did not make it possible to actually run
pcoq. This version does work. Main modification is: - change centaur.ml4 so that * the Pcoq mode is really started by Start Pcoq Mode. * Reset <id> and Reset Initial work as planned for Pcoq (commands are Pcoq Reset <id> and Pcoq ResetInitial). * current_proof_name() does not raise an exception when there is no current proof. - change xlate.ml so that the main tacticals are translated correctly to pcoq data structures. - change in ascent.mli so that * we make sure Fail can now have a numeric argument, * progress is added - vtp.ml is changed in accordance with ascent.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--contrib/interface/ascent.mli3
-rw-r--r--contrib/interface/centaur.ml455
-rw-r--r--contrib/interface/vtp.ml7
-rw-r--r--contrib/interface/xlate.ml1534
4 files changed, 67 insertions, 1532 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 4527f66086..a1f6e2489b 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -457,7 +457,7 @@ and ct_TACTIC_COM =
| CT_elim_type of ct_FORMULA
| CT_exact of ct_FORMULA
| CT_exists of ct_SPEC_LIST
- | CT_fail
+ | CT_fail of ct_INT
| CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
| CT_fixtactic of ct_ID_OPT * ct_INT * ct_FIX_TAC_LIST
| CT_generalize of ct_FORMULA_NE_LIST
@@ -479,6 +479,7 @@ and ct_TACTIC_COM =
| CT_omega
| CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
| CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
+ | CT_progress of ct_TACTIC_COM
| CT_prolog of ct_FORMULA_LIST * ct_INT
| CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
| CT_reduce of ct_RED_COM * ct_ID_LIST
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a0620d4ba2..b1602655f1 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -57,7 +57,11 @@ let text_proof_flag = ref "en";;
(*
let current_proof_name = ref "";;
*)
-let current_proof_name () = string_of_id (get_current_proof_name ())
+let current_proof_name () =
+ try
+ string_of_id (get_current_proof_name ())
+ with
+ UserError("Pfedit.get_proof", _) -> "";;
let current_goal_index = ref 0;;
@@ -482,6 +486,19 @@ let kill_node_verbose n =
let set_text_mode s = text_proof_flag := s
+let pcoq_reset_initial() =
+ output_results(ctf_AbortedAllMessage()) None;
+ Vernacentries.abort_refine Lib.reset_initial ();
+ output_results(ctf_ResetInitialMessage()) None;;
+
+let pcoq_reset x =
+ if refining() then
+ output_results (ctf_AbortedAllMessage ()) None;
+ Vernacentries.abort_refine Lib.reset_name x;
+ output_results
+ (ctf_ResetIdentMessage !global_request_id (string_of_id x)) None;;
+
+
VERNAC ARGUMENT EXTEND text_mode
| [ "fr" ] -> [ "fr" ]
| [ "en" ] -> [ "en" ]
@@ -512,6 +529,14 @@ VERNAC COMMAND EXTEND KillSubProof
[ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ]
END
+VERNAC COMMAND EXTEND PcoqReset
+ [ "Pcoq" "Reset" ident(x) ] -> [ pcoq_reset x ]
+END
+
+VERNAC COMMAND EXTEND PcoqResetInitial
+ [ "Pcoq" "ResetInitial" ] -> [ pcoq_reset_initial() ]
+END
+
let start_proof_hook () =
History.start_proof (current_proof_name());
current_goal_index := 1
@@ -909,38 +934,20 @@ let start_pcoq_mode debug =
set_pcoq_hook pcoq_hook;
end;;
-(*
-vinterp_add "START_PCOQ"
- (function _ ->
- (function () ->
- 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 Vernacinterp.ProtectedLoop));;
-
-vinterp_add "START_PCOQ_DEBUG"
- (function _ ->
- (function () ->
- start_pcoq_mode true;
- set_acknowledge_command ctf_acknowledge_command;
- 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*)
+ 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;;*)
+ set_end_marker "<---";
+ raise Vernacexpr.ProtectedLoop;;
VERNAC COMMAND EXTEND StartPcoq
[ "Start" "Pcoq" "Mode" ] -> [ start_pcoq () ]
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 597553cd52..e2f5195040 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1066,7 +1066,9 @@ and fTACTIC_COM = function
| CT_exists(x1) ->
fSPEC_LIST x1;
fNODE "exists" 1
-| CT_fail -> fNODE "fail" 0
+| CT_fail(x1) ->
+ fINT x1;
+ fNODE "fail" 1
| CT_first(x,l) ->
fTACTIC_COM x;
(List.iter fTACTIC_COM l);
@@ -1138,6 +1140,9 @@ and fTACTIC_COM = function
fTACTIC_COM x;
(List.iter fTACTIC_COM l);
fNODE "parallel" (1 + (List.length l))
+| CT_progress(x1) ->
+ fTACTIC_COM x1;
+ fNODE "progress" 1
| CT_prolog(x1, x2) ->
fFORMULA_LIST x1;
fINT x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index d3d25534ce..2dc5aa3110 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -112,9 +112,6 @@ 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 []);;
@@ -154,58 +151,6 @@ 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)"
- | Targ_command x -> CT_coerce_FORMULA_to_TARG x
- | Targ_id_list x -> xlate_error "coerce_iTARG_to_TARG"
- | Targ_spec_list x -> CT_coerce_SPEC_LIST_to_TARG x
- | Targ_binding_com x -> CT_coerce_FORMULA_to_TARG x
- | Targ_ident x -> CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT x)
- | Targ_int x -> CT_coerce_ID_OR_INT_to_TARG (CT_coerce_INT_to_ID_OR_INT x)
- | Targ_binding x -> CT_coerce_BINDING_to_TARG x
- | Targ_pattern x -> CT_coerce_PATTERN_to_TARG x
- | Targ_unfold_ne_list x -> CT_coerce_UNFOLD_NE_LIST_to_TARG x
- | Targ_unfold x -> CT_coerce_UNFOLD_to_TARG x
- | Targ_string x ->
- CT_coerce_ID_OR_STRING_to_TARG (CT_coerce_STRING_to_ID_OR_STRING x)
- | Targ_fixtac x -> CT_coerce_FIXTAC_to_TARG x
- | 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
- | Varg_binderlist x -> CT_coerce_BINDER_LIST_to_VARG x
- | Varg_bindernelist x -> CT_coerce_BINDER_NE_LIST_to_VARG x
- | Varg_call (id, l) -> xlate_error "coerce_iVARG_to_VARG: CALL as varg"
- | Varg_constr x ->
- CT_coerce_FORMULA_OPT_to_VARG (CT_coerce_FORMULA_to_FORMULA_OPT x)
- | Varg_sorttype x ->
- CT_coerce_FORMULA_OPT_to_VARG
- (CT_coerce_FORMULA_to_FORMULA_OPT (CT_coerce_SORT_TYPE_to_FORMULA x))
- | Varg_constrlist x -> CT_coerce_FORMULA_LIST_to_VARG (CT_formula_list x)
- | Varg_ident x ->
- CT_coerce_ID_OPT_OR_ALL_to_VARG
- (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_ID_to_ID_OPT x))
- | Varg_int x -> CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT x)
- | Varg_intlist x -> CT_coerce_INT_LIST_to_VARG x
- | Varg_none -> CT_coerce_FORMULA_OPT_to_VARG ctv_FORMULA_OPT_NONE
- | Varg_string x ->
- CT_coerce_STRING_OPT_to_VARG (CT_coerce_STRING_to_STRING_OPT x)
- | Varg_tactic x ->
- CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT x)
- | Varg_astlist x -> CT_coerce_AST_LIST_to_VARG x
- | Varg_ast x -> CT_coerce_AST_to_VARG x
- | Varg_varglist x ->
- 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
@@ -236,11 +181,6 @@ 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);;
@@ -829,12 +769,6 @@ 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
@@ -907,18 +841,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' ->
- CT_coerce_FORMULA_LIST_to_SPEC_LIST
- (CT_formula_list (List.map strip_targ_command bl))
- | (Targ_binding b) :: bl' ->
- CT_coerce_BINDING_LIST_to_SPEC_LIST
- (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)
@@ -946,33 +869,6 @@ let strip_targ_intropatt =
| Targ_intropatt x -> x
| _ -> xlate_error "strip_targ_intropatt";;
-
-(*
-let rec get_flag_rec =
- function
- | n1 :: tail ->
- let conv_id_fun = (fun x -> match qualid_to_ct_ID x with
- Some y -> y
- | None -> assert false) in
- let conv_flags, red_ids = get_flag_rec tail in
- (match n1 with
- | Node (_, "Beta", []) -> CT_beta::conv_flags, red_ids
- | Node (_, "Delta", []) -> CT_delta::conv_flags, red_ids
- | Node (_, "Iota", []) -> CT_iota::conv_flags, red_ids
- | Node (_, "Zeta", []) -> CT_zeta::conv_flags, red_ids
- | Node (_, "Evar", []) -> CT_evar::conv_flags, red_ids
- | Node (_, "Unf", l) ->
- (match red_ids with
- | CT_unf [] -> conv_flags, CT_unf (List.map conv_id_fun l)
- | _ -> error "Cannot specify identifiers to unfold twice")
- | Node (_, "UnfBut", l) ->
- (match red_ids with
- | CT_unf [] -> conv_flags, CT_unfbut (List.map conv_id_fun l)
- | _ -> error "Cannot specify identifiers to unfold twice")
- | 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
@@ -988,20 +884,6 @@ let get_flag r =
(* Rem: EVAR flag obsolète *)
conv_flags, red_ids
-(*
-let rec xlate_intro_pattern =
- function
- | Node(_,"CONJPATTERN", l) ->
- CT_conj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern
- (flatten_one_level l)))
- | Node(_, "DISJPATTERN", l) ->
- CT_disj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern
- (flatten_one_level l)))
- | Node(_, "IDENTIFIER", [Nvar(_,c)]) ->
- 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] ->
@@ -1035,15 +917,6 @@ 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])]) ->
- CT_context(ctv_ID_OPT_NONE, xlate_formula v)
- | 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) ->
@@ -1051,12 +924,6 @@ let xlate_context_pattern = function
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)
@@ -1067,71 +934,6 @@ 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)
- | Str (_, s) -> Targ_string (CT_string s)
- | Num (_, n) -> Targ_int (CT_int n)
- | Node (_, "LETPATTERNS", fst::l) ->
- let mk_unfold_occ = function
- Node(_, "HYPPATTERN", Nvar(_, name)::ints) ->
- CT_unfold_occ(
- CT_int_list (List.map xlate_int ints), CT_ident name)
- | Node(_, "CCLPATTERN", ints) ->
- CT_unfold_occ(
- CT_int_list (List.map xlate_int ints), CT_ident "Goal")
- | _ -> xlate_error "unexpected argument in mk_unfold_occ" in
- Targ_unfold_ne_list(
- CT_unfold_ne_list(mk_unfold_occ fst, List.map mk_unfold_occ l))
- | Node (_, "COMMAND", (c :: [])) -> Targ_command (xlate_formula c)
- | Node (_, ("CASTEDCOMMAND"|"CASTEDOPENCOMMAND"), (c :: [])) -> Targ_command (xlate_formula c)
- | Node (_, "BINDINGS", bl) ->
- Targ_spec_list (filter_binding_or_command_list (List.map cvt_arg bl))
- | Node (_, "BINDING", ((Node (_, "COMMAND", (c :: []))) :: [])) ->
- Targ_binding_com (xlate_formula c)
- | Node (_, "BINDING",
- ((Num (_, n)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) ->
- Targ_binding
- (CT_binding (CT_coerce_INT_to_ID_OR_INT (CT_int n), xlate_formula c))
- | Node (_, "BINDING",
- ((Nvar (_, id)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) ->
- Targ_binding
- (CT_binding (CT_coerce_ID_to_ID_OR_INT (CT_ident id), xlate_formula c))
- | Node (_, "TACTIC", (t :: [])) -> Targ_tacexp (xlate_tactic t)
- | Node (_, "FIXEXP",
- ((Nvar (_, id)) ::
- ((Num (_, n)) :: ((Node (_, "COMMAND", (c :: []))) :: [])))) ->
- Targ_fixtac (CT_fixtac (CT_ident id, CT_int n, xlate_formula c))
- | Node (_, "COFIXEXP",
- ((Nvar (_, id)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) ->
- Targ_cofixtac (CT_cofixtac (CT_ident id, xlate_formula c))
- | Node ((l1,l2), "CLAUSE", l) ->
- Targ_id_list (CT_id_list
- (List.map
- (function
- | Node(_, "INHYP", [Nvar (_, x)]) -> CT_ident x
- | Node(_, "INHYP",
- [Node(_, "COMMAND",
- [Node(_, "META",
- [Num (_, x)])])]) ->
- CT_metac (CT_int x)
- | _ ->
- xlate_error
- ("expected identifiers in a CLAUSE " ^
- (string_of_int l1) ^ " " ^
- (string_of_int l2))) l))
- | Node (_, "REDEXP", (tac :: [])) -> Targ_redexp (xlate_red_tactic tac)
- | Node (_, "INTROPATTERN",
- [Node(_,"LISTPATTERN", l)]) ->
- Targ_intropatt (CT_intro_patt_list(List.map xlate_intro_pattern l))
- | Node(_, "Str", [x]) -> cvt_arg x
- | Node ((l1,l2), a, _) -> failwith ("cvt_arg on node " ^ a ^ " at " ^
- (string_of_int l1) ^ " " ^
- (string_of_int l2))
- | _ -> failwith "cvt_arg"
-*)
let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
function
| TacVoid ->
@@ -1199,310 +1001,51 @@ and xlate_red_tactic =
| 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
- | "Hnf" -> CT_hnf
- | "Simpl" -> CT_simpl
- | "Fold" -> CT_fold(CT_formula_list[])
- | _ -> xlate_error ("xlate_red_tactic, unexpected singleton " ^ s))
- | Node ((l1,l2), "Unfold", unf_list) ->
- let ct_unf_list = List.map (function
- | Node (_, "UNFOLD", qid::nums) ->
- (match qualid_to_ct_ID qid with
- Some x ->
- CT_unfold_occ (CT_int_list (List.map xlate_int nums), x)
- | _ -> failwith ("bad form in Unfold at characters " ^
- (string_of_int l1) ^ " " ^
- (string_of_int l2)) )
- | n ->
- xlate_error ("xlate_red_tactic, expected unfold occurrence at " ^
- (string_of_node_loc n)))
- 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")
- | Node (_, "Cbv", flag_list) ->
- let conv_flags, red_ids = get_flag_rec flag_list in
- CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
- | Node (_, "Lazy", flag_list) ->
- let conv_flags, red_ids = get_flag_rec flag_list in
- CT_lazy (CT_conversion_flag_list conv_flags, red_ids)
- | Node (_, "Pattern", l) ->
- let pat_list = List.map (function
- | Node (_, "PATTERN", ((Node (_, "COMMAND", (c :: []))) :: nums)) ->
- CT_pattern_occ
- (CT_int_list (List.map xlate_int nums), xlate_formula c)
- | _ -> error "Expecting patterns in a Pattern command") 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")
- | Node (_, "Fold", formula_list) ->
- CT_fold(CT_formula_list(List.map
- (function Node(_,"COMMAND", [c]) -> xlate_formula c
- | _ -> error("xlate_red_tactic expected a COMMAND"))
- formula_list))
- | Node (_, a, _) -> error ("xlate_red_tactic: unexpected argument " ^ a)
- | _ -> error "xlate_red_tactic : unexpected argument"
-*)
+
and xlate_tactic =
function
-(* | Node (_, s, l) ->
- (match s, l with
-*)
-(*
- | "FUN", [Node(_, "FUNVAR", largs); 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"
- | xt :: [] -> xt
- | CT_then(xt,xtl1) :: xtl -> CT_then (xt, xtl1@xtl)
- | 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)
- | "ABSTRACT", (Node(_,_,[t]) :: []) -> CT_abstract(ctv_ID_OPT_NONE, (xlate_tactic t))
- | "ABSTRACT", (Nvar(_, id)::(Node(_,"TACTIC",[t]) :: [])) ->
- CT_abstract(ctf_ID_OPT_SOME (CT_ident id), (xlate_tactic t))
- | "INFO", (t :: []) -> CT_info (xlate_tactic t)
- | "REPEAT", _ ->
- xlate_error "xlate_tactic: malformed tactic-expression REPEAT"
-*)
+ | TacThen (t1,t2) ->
+ (match xlate_tactic t1 with
+ CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
+ | t -> CT_then (t,[xlate_tactic t2]))
+ | TacFirst([]) -> assert false
+ | TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
+ | TacSolve([]) -> assert false
+ | TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
| 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
- | Node(_, "COMMAND", [x]) ->
- CT_coerce_FORMULA_to_TACTIC_ARG (xlate_formula x)
- | x ->
- CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic x))
- l in
- let fst,args2 =
- match args with
- 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
- (function
- | Node(_,"MATCHRULE",
- [Node(_,"TERM", [Node(_,"COMMAND", [p])]);
- tac]) ->
- CT_match_tac_rule(
- CT_coerce_FORMULA_to_CONTEXT_PATTERN
- (xlate_formula p),
- mk_let_value tac)
- | Node(_,"MATCHRULE", [tac]) ->
- CT_match_tac_rule
- (CT_coerce_FORMULA_to_CONTEXT_PATTERN
- CT_existvarc,
- mk_let_value tac)
- | Node((l1,l2),s,_) ->
- failwith ("problem with match_tac at " ^
- (string_of_int l1) ^
- " " ^
- (string_of_int l2) ^
- ": " ^ s)
- | _ -> assert false) rules with
- | [] -> 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 =
- function
- | Node(_, "LETCLAUSE", [Nvar(_, s);Node(_,"COMMAND",[v])]) ->
- CT_let_clause(CT_ident s,
- CT_coerce_DEF_BODY_to_LET_VALUE
- (formula_to_def_body v))
- | Node(_, "LETCLAUSE", [Nvar(_, s); v]) ->
- CT_let_clause(CT_ident s,
- CT_coerce_TACTIC_COM_to_LET_VALUE
- (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))
-*)
+ | TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
+ | TacDo(n, t) -> CT_do(CT_int n, xlate_tactic t)
+ | TacRepeat t -> CT_repeat(xlate_tactic t)
+ | TacProgress t -> CT_progress(xlate_tactic t)
+ | TacAbstract(t,id_opt) ->
+ CT_abstract((match id_opt with
+ None -> ctv_ID_OPT_NONE
+ | Some id -> ctf_ID_OPT_SOME (CT_ident (string_of_id id))),
+ xlate_tactic t)
| TacAtom (_, t) -> xlate_tac t
-(* was in xlate_tac *)
- | TacFail 0 -> CT_fail
- | TacFail n -> xlate_error "TODO: Fail n"
+ | TacFail n -> CT_fail (CT_int 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) )
-*)
+ | TacInfo t -> CT_info(xlate_tactic t)
| TacArg a -> xlate_call_or_tacarg a
and xlate_tac =
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)
-*)
| 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)) ->
- CT_fixtactic
- (ctf_ID_OPT_SOME id, n,
- CT_fix_tac_list (List.map strip_targ_fixtac fixtac_list))
- | "Cofix", [] -> CT_cofixtactic (ctv_ID_OPT_NONE, CT_cofix_tac_list [])
- | "Cofix", ((Targ_ident id) :: cofixtac_list) ->
- 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) ->
@@ -1517,76 +1060,35 @@ and xlate_tac =
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] ->
-*)
| TacIntroMove (Some id1, Some (_,id2)) ->
CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
-(*
- | "IntroMove", [Targ_ident 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] ->
-*)
| 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)] ->
-*)
| 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)
- | "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
@@ -1594,12 +1096,6 @@ and xlate_tac =
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
@@ -1607,12 +1103,6 @@ and xlate_tac =
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
@@ -1621,18 +1111,6 @@ and xlate_tac =
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) :: [])) ->
- CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
- | "SubstConcl_RL", ((Targ_command c) :: []) ->
- CT_cutrewrite_rl (c, ctv_ID_OPT_NONE)
- | "SubstHyp_RL", ((Targ_command c) :: ((Targ_ident id) :: [])) ->
- 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
@@ -1650,114 +1128,27 @@ and xlate_tac =
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
- | Targ_int n -> (CT_coerce_INT_to_INT_OPT n)
- | _ -> (CT_coerce_NONE_to_INT_OPT CT_none)),
- (match a2 with
- | Targ_id_list l -> l
- | _ -> xlate_error
- "SuperAuto expects a list of identifiers as second argument"),
- (match a3 with
- | Targ_string (CT_string "Destructing") -> CT_destructing
- | _ -> (CT_coerce_NONE_to_DESTRUCTING CT_none)),
- (match a4 with
- | Targ_string (CT_string "UsingTDB") -> CT_usingtdb
- | _ -> (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)
- | "Auto", [] -> CT_auto (CT_coerce_NONE_to_INT_OPT CT_none)
- | "Auto", ((Targ_int n) :: ((Targ_ident id1) :: idl)) ->
- CT_auto_with ((CT_coerce_INT_to_INT_OPT n),
- CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
- CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x
- | _ -> xlate_error
- "Auto expects identifiers")
- idl)))
- | "Auto", ((Targ_ident id1) :: idl) ->
- CT_auto_with ((CT_coerce_NONE_to_INT_OPT CT_none),
- CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
- CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x
- | _ -> xlate_error
- "Auto expects identifiers")
- 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)) ->
- CT_eauto_with ((CT_coerce_INT_to_INT_OPT n),
- CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
- CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x
- | _ -> xlate_error
- "Auto expects identifiers")
- idl)))
- | "EAuto", ((Targ_ident id1) :: idl) ->
- CT_eauto_with ((CT_coerce_NONE_to_INT_OPT CT_none),
- CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
- CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x
- | _ -> xlate_error
- "Auto expects identifiers")
- idl)))
- | "EAuto", ((Targ_int n) :: ((Targ_string (CT_string "*")) :: [])) ->
- 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
@@ -1768,105 +1159,37 @@ and xlate_tac =
| 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)
- | "Trivial", ((Targ_ident id1):: idl) ->
- CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
- (CT_id_ne_list(id1,
- 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",
- ((Targ_command c1) ::
- ((Targ_spec_list sl) ::
- ((Targ_command c2) :: ((Targ_spec_list sl2) :: [])))) ->
- 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)
@@ -1875,36 +1198,10 @@ and xlate_tac =
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) ->
@@ -1913,34 +1210,12 @@ and xlate_tac =
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)) ->
- CT_inversion
- (compute_INV_TYPE_from_string s, id,
- CT_id_list (List.map strip_targ_ident idlist))
- | "DInv", ((Targ_ident (CT_ident s))::((Targ_ident id) :: [])) ->
- CT_depinversion
- (compute_INV_TYPE_from_string s, id, ctv_FORMULA_OPT_NONE)
- | "DInvWith", ((Targ_ident (CT_ident s))::
- ((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 [])
@@ -1957,12 +1232,6 @@ and xlate_tac =
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
@@ -1973,14 +1242,7 @@ and xlate_tac =
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"
@@ -1991,10 +1253,6 @@ and xlate_tac =
| 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"
@@ -2039,22 +1297,6 @@ and coerce_genarg_to_TARG x =
| 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) ->
- let rec xlate_ctxt_rule_aux = function
- [concl_pat; tac] ->
- [], xlate_context_pattern concl_pat, xlate_tactic tac
- | Node(_,"MATCHCONTEXTHYPS", hyp_parts)::b ->
- let hyps, cpat, tactic = xlate_ctxt_rule_aux b in
- (xlate_match_context_hyps hyp_parts)::hyps, cpat, tactic
- | _ -> assert false in
- 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) ->
@@ -2063,28 +1305,6 @@ and xlate_context_rule =
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])]) ->
- (try
- CT_coerce_EVAL_CMD_to_DEF_BODY(
- CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
- xlate_red_tactic tac,
- xlate_formula f))
- with Failure s ->
- failwith ("error raised inside formula_to_def_body " ^
- s))
- | f -> (try ct_coerce_FORMULA_to_DEF_BODY(xlate_formula f)
- with Failure s ->
- match f with
- Node(_,s1, _) ->
- failwith ("error raised inside formula_to_def_body (2) " ^
- s1 ^ " " ^ s)
- | _ ->
- failwith("error raised inside formula_to_def_body (3) " ^
- s))
-*)
and formula_to_def_body =
function
| ConstrEval (red, f) ->
@@ -2095,39 +1315,11 @@ and formula_to_def_body =
| 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
- | _ -> xlate_error "strip vernac: non-integer argument";;
-
-let strip_varg_string =
- function
- | Varg_string str -> str
- | _ -> xlate_error "strip vernac: non-string argument";;
-
-let strip_varg_ident =
- function
- | Varg_ident id -> id
- | _ -> xlate_error "strip vernac: non-ident argument";;
-
-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 *)
@@ -2179,14 +1371,7 @@ let coerce_genarg_to_VARG x =
| 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"
@@ -2194,30 +1379,11 @@ let xlate_thm x = CT_thm (match x with
| Fact -> "Fact"
| Decl -> "Decl")
-(*
-let xlate_defn x = CT_defn (match x with
- | "DEFINITION" -> "Definition"
- | "LOCAL" -> "Local"
- | "OBJECT" -> "@Definition"
- | "LOBJECT" -> "@Local"
- | "OBJCOERCION" -> "@Coercion"
- | "LOBJCOERCION" -> "LOBJCOERCION"
- | "SUBCLASS" -> "SubClass"
- | "LSUBCLASS" -> "LSUBCLASS"
- | "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
@@ -2226,33 +1392,13 @@ let xlate_defn_or_thm =
| 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"
- | "VARIABLE" -> "Variable"
- | "VARIABLES" -> "Variable"
- | "AXIOM" -> "Axiom"
- | "PARAMETER" -> "Parameter"
- | "PARAMETERS" -> "Parameter"
- | (*backwards compatible with 14a leave for now *)
- "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"
@@ -2260,16 +1406,6 @@ let xlate_dep =
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")
- | Varg_string (CT_string "prev") ->
- CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "prev")
- | 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")
@@ -2298,20 +1434,6 @@ let build_constructors l =
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
- | Varg_varglist ((Varg_string (CT_string "")) ::((Varg_string assum) ::
- ((Varg_ident id) :: (c :: [])))) ->
- CT_coerce_CONSTR_to_RECCONSTR (CT_constr (id, coerce_iVARG_to_FORMULA c))
- | Varg_varglist ((Varg_string (CT_string "COERCION"))
- ::((Varg_string assum) ::
- ((Varg_ident id) :: (c :: [])))) ->
- 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) ->
@@ -2347,22 +1469,6 @@ 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
- | CT_string "IMPORT" -> CT_import
- | CT_string "EXPORT" -> CT_export
- | CT_string s -> xlate_error ("unexpected Require import flag " ^ s) in
- let ct_spec =
- match spec with
- | CT_string "UNSPECIFIED" -> ctv_SPEC_OPT_NONE
- | CT_string "SPECIFICATION" -> CT_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
@@ -2392,64 +1498,8 @@ 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)
- | Node (_, "VERNACCALL", ((Str (_, na)) :: l)) ->
- Varg_call (CT_ident na, List.map cvt_varg l)
- | Node (_, "VERNACCALL", ((Id (_, na)) :: l)) ->
- Varg_call (CT_ident na, List.map cvt_varg l)
- | Node (_, ("QUALIDARG"|"QUALIDCONSTARG"), _) as it ->
- (match qualid_to_ct_ID it with
- Some x -> Varg_ident x
- | None -> assert false)
- | Nvar (_, id) -> Varg_ident (CT_ident id)
- | Str (_, s) -> Varg_string (CT_string s)
- | Num (_, n) -> Varg_int (CT_int n)
- | Node (_, "NONE", []) -> Varg_none
- | Node (_, "CONSTR", ((Node (_, "PROP", ((Id (_, c)) :: []))) :: [])) ->
- (match c with
- | "Pos" -> Varg_sorttype (CT_sortc "Set")
- | "Null" -> Varg_sorttype (CT_sortc "Prop")
- | _ -> xlate_error "cvt_varg : PROP : Failed match ")
- | Node (_, "CONSTR", ((Node (_, "PROP", [])) :: [])) ->
- Varg_sorttype (CT_sortc "Prop")
- | Node (_, "CONSTR", ((Node (_, "TYPE", _)) :: [])) ->
- Varg_sorttype (CT_sortc "Type")
- | Node (_, "CONSTR", [c]) -> Varg_constr (xlate_formula c)
- | Node (_, "CONSTRLIST", cs) -> Varg_constrlist (List.map xlate_formula cs)
- | Node (_, "TACTIC", [c]) -> Varg_tactic (xlate_tactic c)
- | Node (_, "BINDER", args) as arg ->
- Varg_binder(cvt_binder xlate_formula arg)
- | Node (_, "BINDERLIST", l) as arg ->
- Varg_binderlist(cvt_binders xlate_formula arg)
- | Node (_, "BINDERS", l) as arg ->
- Varg_binderlist(cvt_binders xlate_formula arg)
- | Node (_, "NUMBERLIST", ln) ->
- Varg_intlist (CT_int_list (List.map xlate_int ln))
- | Node (_, "AST", [Node(_, "ASTACT", [
- Node(_, "ASTLIST", [Node(_, "TACTICLIST", _) as it])])]) ->
- Varg_tactic(xlate_tactic it)
- | Node (_, "AST", (a :: [])) -> Varg_ast (xlate_ast a)
- | Node (_, "ASTLIST", al) ->
- Varg_astlist (CT_ast_list (List.map xlate_ast al))
- | Node (_, "TACTIC_ARG", (targ :: [])) -> Varg_tactic_arg (cvt_arg targ)
- | Node (_, s, _) as it -> failwith ("cvt_varg : " ^ s ^ " at location " ^
- (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])])]) ->
-*)
| 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"
@@ -2459,26 +1509,6 @@ let xlate_vernac =
(* 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 =
- List.fold_right
- (fun e res -> match e with
- Node(_,"AST",
- [Node(_,"REC",
- [Node(_,"RECCLAUSE", [Nvar(_,x);
- Node(_, "FUNVAR", argl);
- tac])])]) ->
- let fst, rest = xlate_largs_to_id_unit argl in
- CT_rec_tactic_fun(CT_ident x,
- CT_id_unit_list(fst, rest),
- xlate_tactic tac)::res
- | _ -> res) the_list [] in
- 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 =
@@ -2498,54 +1528,19 @@ let xlate_vernac =
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])]) ->
-*)
| 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
- | CT_string "" -> CT_coerce_NONE_to_VERBOSE_OPT CT_none
- | CT_string "Verbose" as it -> CT_verbose
- | 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 =
- match tail with
- | (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
-*)
| 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
- | "QUIT", [] -> CT_quit
-*)
| 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)
@@ -2556,35 +1551,12 @@ let xlate_vernac =
| 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
- 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 *)
- "ABORT", ((Varg_ident id) :: []) -> CT_abort (ctf_ID_OPT_OR_ALL_SOME id)
- | "ABORT", [] -> CT_abort ctv_ID_OPT_OR_ALL_NONE
- | "ABORTALL", [] -> CT_abort ctv_ID_OPT_OR_ALL_ALL
- | (*formerly | ("ABORTALL", []) -> ident_vernac "Abort All" *)
- "RESTART", [] -> CT_restart
- | "PROOF", (c :: []) -> CT_proof (coerce_iVARG_to_FORMULA c)
- | "SOLVE", ((Varg_int n) :: ((Varg_tactic tcom) :: [])) ->
- CT_solve (n, tcom)
- | "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
-*)
| VernacGoal 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))
@@ -2594,16 +1566,6 @@ let xlate_vernac =
| 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
- | Varg_string (CT_string "Rl") -> CT_rl
- | _ -> assert false in
- let f_ne_list = match formula_list with
- Varg_constrlist (fst::rest) -> CT_formula_ne_list(fst,rest)
- | _ -> assert false in
-*)
| 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
@@ -2619,40 +1581,6 @@ let xlate_vernac =
(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)::[]))) ->
- CT_hint(id_name,
- CT_id_list(List.map coerce_iVARG_to_ID
- dbnames), CT_resolve(c))
- | "HintUnfold",
- ((Varg_ident id_name) ::
- ((Varg_varglist dbnames) :: ((Varg_ident c)::[]))) ->
- CT_hint(id_name,
- CT_id_list(List.map coerce_iVARG_to_ID
- dbnames), CT_unfold_hint(c))
- | "HintConstructors",
- ((Varg_ident id_name) ::
- ((Varg_varglist dbnames) :: ((Varg_ident c)::[]))) ->
- CT_hint(id_name,
- CT_id_list(List.map coerce_iVARG_to_ID
- dbnames), CT_constructors(c))
- | "HintImmediate",
- ((Varg_ident id_name) ::
- ((Varg_varglist dbnames) :: ((Varg_constr c)::[]))) ->
- CT_hint(id_name,
- CT_id_list(List.map coerce_iVARG_to_ID
- dbnames), CT_immediate(c))
- | "HintExtern",
- [Varg_ident id_name;
- Varg_varglist dbnames;
- Varg_int n;
- Varg_constr c;
- 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
@@ -2669,23 +1597,6 @@ let xlate_vernac =
| 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",
- CT_id_ne_list(n1, List.map coerce_iVARG_to_ID names),
- CT_id_list(List.map coerce_iVARG_to_ID dbnames))
- | "HintsImmediate",
- (Varg_varglist(dbnames)::(Varg_ident n1) :: names) ->
- CT_hints(CT_ident "Immediate",
- CT_id_ne_list(n1, List.map coerce_iVARG_to_ID names),
- CT_id_list(List.map coerce_iVARG_to_ID dbnames))
- | "HintsUnfold",
- (Varg_varglist(dbnames)::(Varg_ident n1) :: names) ->
- 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
@@ -2719,28 +1630,6 @@ let xlate_vernac =
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)
- | "DefinedNamed", [] ->
- CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE)
- | "SaveAnonymous", [Varg_string (CT_string kind); Varg_ident s] ->
- let kind_string =
- match kind with
- "THEOREM" -> "Theorem"
- | "LEMMA" -> "Lemma"
- | "FACT" -> "Fact"
- | "REMARK" -> "Remark"
- | "DECL" -> "Decl"
- | _ -> assert false in
- 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) ->
@@ -2751,63 +1640,26 @@ let xlate_vernac =
| 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) ->
-*)
| 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)
-*)
| 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)
-*)
| 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 ->
-*)
| VernacShow ExplainProof l ->
CT_explain_proof (CT_int_list (List.map (fun x -> CT_int x) l))
-(*
- | "ExplainProofTree", l ->
-*)
| VernacShow ExplainTree l ->
CT_explain_prooftree (CT_int_list (List.map (fun x -> CT_int x) l))
-(*
- | "CheckGuard", [] -> CT_guarded
-*)
| VernacCheckGuard -> CT_guarded
| VernacPrint p ->
(match p with
@@ -2834,73 +1686,14 @@ let xlate_vernac =
| 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
- | "PrintSec", ((Varg_ident id) :: []) -> CT_print_section id
- | "PrintStates", [] -> CT_print_states
- | "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) :: []) ->
-*)
| VernacBeginSection id ->
CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
-(*
- | "EndSection", ((Varg_ident id) :: []) ->
-*)
| VernacEndSegment id -> CT_section_end (xlate_ident id)
-(*
- | "StartProof",
- ((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) ->
-*)
| VernacStartTheoremProof (k, s, c, _, _) ->
CT_coerce_THEOREM_GOAL_to_COMMAND(
CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), 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)
- | ("RESUME", []) -> suspend(CT_false)
- *)
-*)
| 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
- | [] -> ctv_FORMULA_OPT_NONE, None
- | [Varg_constr b] -> CT_coerce_FORMULA_to_FORMULA_OPT b, None
- | [Varg_tactic_arg r] -> ctv_FORMULA_OPT_NONE, Some r
- | [Varg_constr b; Varg_tactic_arg r] ->
- CT_coerce_FORMULA_to_FORMULA_OPT b, Some r
- | [Varg_sorttype b] ->
- CT_coerce_FORMULA_to_FORMULA_OPT
- (CT_coerce_SORT_TYPE_to_FORMULA b), None
- | _ -> assert false in
-*)
| VernacDefinition (k,s,ProveBody (bl,typ),_) ->
if bl <> [] then xlate_error "TODO: Def bindings";
CT_coerce_THEOREM_GOAL_to_COMMAND(
@@ -2911,51 +1704,11 @@ let xlate_vernac =
(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) ->
let b = List.map snd b in (* TODO: handle possible coercions *)
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,
- CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none)
- | (Varg_string (CT_string x))::(Varg_ident m1)::l1 ->
- let l2 = CT_id_ne_list(m1, List.map coerce_iVARG_to_ID l1) in
- let modifier =
- (match x with
- | "inside" -> CT_in_modules l2
- | "outside" -> CT_out_modules l2
- | _ -> xlate_error "bad extra argument for Search") in
- CT_search_pattern(c, modifier)
- | _ -> xlate_error "bad argument list for SearchPattern")
-
- | "SEARCH", (Varg_ident id):: l ->
- (match l with
- | [] -> CT_search(id, CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none)
- | (Varg_string (CT_string x))::(Varg_ident m1)::l1 ->
- let l2 = CT_id_ne_list(m1, List.map coerce_iVARG_to_ID l1) in
- let modifier =
- (match x with
- | "inside" -> CT_in_modules l2
- | "outside" -> CT_out_modules l2
- | _ -> xlate_error "bad extra argument for Search") in
- CT_search(id, modifier)
- | _ -> xlate_error "bad argument list for Search")
-*)
| VernacSearch (s,x) ->
(match s with
| SearchPattern c ->
@@ -2963,38 +1716,12 @@ let xlate_vernac =
| 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) ::
- ((Varg_binderlist binders) ::
- (c1 ::
- ((Varg_varglist rec_constructor_or_none) ::
- ((Varg_varglist field_list) :: [])))))) ->
- let record_constructor =
- match rec_constructor_or_none with
- | [] -> CT_coerce_NONE_to_ID_OPT CT_none
- | (Varg_ident id) :: [] -> CT_coerce_ID_to_ID_OPT id
- | _ -> xlate_error "unexpected record constructor" in
- CT_record
- ((match coercion_or_not with CT_string "" ->
- CT_coerce_NONE_to_COERCION_OPT(CT_none)
- | _ -> CT_coercion_atm),
- s, binders,
- (match c1 with (Varg_sorttype c) -> c
- |(Varg_constr (CT_coerce_SORT_TYPE_to_FORMULA c)) -> c
- | _ -> 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
+ 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,
@@ -3029,47 +1756,6 @@ let xlate_vernac =
CT_derive_depinversion
(CT_inv_clear, id, coerce_iVARG_to_FORMULA c, sort)
*)
-(*
- |
- "ONEINDUCTIVE",
- ((Varg_string (CT_string f)) ::
- ((Varg_ident s) ::
- (c ::
- ((Varg_binderlist binders) ::
- ((Varg_binderlist (CT_binder_list constructors)) :: []))))) ->
- CT_mind_decl
- (CT_co_ind f,
- CT_ind_spec_list(
- [CT_ind_spec(s,binders, coerce_iVARG_to_FORMULA c,
- build_constructors constructors)]))
- | "OLDMUTUALINDUCTIVE",
- [Varg_binderlist binders; Varg_string(CT_string f);
- Varg_varglist lmi] ->
- let strip_mutind =
- function
- | Varg_varglist([Varg_ident s;c;
- Varg_binderlist (CT_binder_list constructors)]) ->
- CT_ind_spec(s, binders, coerce_iVARG_to_FORMULA c,
- build_constructors constructors)
- | _ -> xlate_error "mutual inductive, old style" in
- CT_mind_decl(CT_co_ind f, CT_ind_spec_list(List.map strip_mutind lmi))
- | "MUTUALINDUCTIVE",
- ((Varg_string (CT_string co_or_ind)) ::
- ((Varg_varglist lmi) ::[])) ->
- let strip_mutind =
- function
- | Varg_varglist ((Varg_ident s) ::
- (c ::
- ((Varg_binderlist parameters) ::
- ((Varg_binderlist (CT_binder_list constructors))
- :: [])))) ->
- CT_ind_spec
- (s, parameters, coerce_iVARG_to_FORMULA c,
- build_constructors constructors)
- | _ -> 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) =
@@ -3078,21 +1764,6 @@ let xlate_vernac =
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
- | Varg_varglist ((Varg_ident fid) ::
- ((Varg_binderlist (CT_binder_list (b :: bl))) ::
- (arf :: (ardef :: [])))) ->
- CT_fix_rec
- (fid, CT_binder_ne_list (b, bl), coerce_iVARG_to_FORMULA arf,
- coerce_iVARG_to_FORMULA ardef)
- | _ -> 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) =
@@ -3103,38 +1774,12 @@ let xlate_vernac =
| _ -> 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
- | Varg_varglist ((Varg_ident fid) :: (arf :: (ardef :: []))) ->
- CT_cofix_rec
- (fid, coerce_iVARG_to_FORMULA arf, coerce_iVARG_to_FORMULA ardef)
- | _ -> 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
- | Varg_varglist ((Varg_ident fid) ::
- ((Varg_string (CT_string depstr)) ::
- (inde :: ((Varg_sorttype sort) :: [])))) ->
- CT_scheme_spec
- (fid, xlate_dep depstr, coerce_iVARG_to_FORMULA inde, sort)
- | _ -> 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) =
@@ -3144,28 +1789,8 @@ let xlate_vernac =
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
- (id, coerce_iVARG_to_FORMULA c, CT_coerce_NONE_to_INT_OPT CT_none)
- | "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
@@ -3173,20 +1798,12 @@ let xlate_vernac =
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, xlate_ident id,
CT_coerce_STRING_to_STRING_OPT (CT_string filename))
-(*
- | "SYNTAX", ((Varg_ident phylum) :: ((Varg_ident s) :: (x :: (y :: l)))) ->
-*)
+
| 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!
@@ -3195,23 +1812,6 @@ let xlate_vernac =
| ("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
- (CT_string str_assoc)))) ::
- ((Varg_int n) :: ((Varg_string str) :: ((Varg_ident id) :: [])))) ->
- CT_infix (
- (match str_assoc with
- | "LEFTA" -> CT_lefta
- | "RIGHTA" -> CT_righta
- | "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
@@ -3220,33 +1820,7 @@ let xlate_vernac =
| 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)) ::
- ((Varg_ident id1) :: ((Varg_ident id2) :: ((Varg_ident id3) :: []))))) ->
- let id_opt =
- match str with
- | "IDENTITY" -> CT_identity
- | "" -> CT_coerce_NONE_to_IDENTITY_OPT CT_none
- | _ -> xlate_error "unknown flag for a coercion1" in
- let local_opt =
- match s with
- | "LOCAL" -> CT_local
- | "" -> 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 =
@@ -3268,60 +1842,8 @@ let xlate_vernac =
| Libnames.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
-*)
-(* 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) :: []) ->
- CT_add_natural_feature (CT_implicit, id)
- | "MemTextParamOmit", ((Varg_ident id) :: []) ->
- CT_test_natural_feature (CT_implicit, id)
- | "RemoveTextParamOmit", ((Varg_ident id) :: []) ->
- CT_remove_natural_feature (CT_implicit, id)
- | "PrintTextParamOmit", [] -> CT_print_natural_feature CT_implicit
- | "AddTextParamRecSub", ((Varg_ident id) :: []) ->
- CT_add_natural_feature (CT_contractible, id)
- | "MemTextParamRecSub", ((Varg_ident id) :: []) ->
- CT_test_natural_feature (CT_contractible, id)
- | "RemoveTextParamRecSub", ((Varg_ident id) :: []) ->
- CT_remove_natural_feature (CT_contractible, id)
- | "PrintTextParamRecSub", [] -> CT_print_natural_feature CT_contractible
- | "AddTextParamImmediate", ((Varg_ident id) :: []) ->
- CT_add_natural_feature (CT_nat_transparent, id)
- | "MemTextParamImmediate", ((Varg_ident id) :: []) ->
- CT_test_natural_feature (CT_nat_transparent, id)
- | "RemoveTextParamImmediate", ((Varg_ident id) :: []) ->
- CT_remove_natural_feature (CT_nat_transparent, id)
- | "PrintTextParamImmediate", [] ->
- CT_print_natural_feature CT_nat_transparent
-*)
-(*
- | "ResetName", ((Varg_ident id) :: []) -> CT_reset 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
- set_or_unset, tail =
- if fst_code = code_plus then (CT_set, sub s 1 (length s - 1))
- else if fst_code = code_minus then (CT_unset, sub s 1 (length s - 1))
- else (CT_switch, s) in
- (match tail with
- | "time" -> CT_omega_flag (set_or_unset, CT_flag_time)
- | "action" -> CT_omega_flag (set_or_unset, CT_flag_action)
- | "system" -> CT_omega_flag (set_or_unset, CT_flag_system)
- | _ ->
- CT_omega_flag
- (set_or_unset, CT_coerce_STRING_to_OMEGA_FEATURE (CT_string s)))
-*)
| VernacExtend (s, l) ->
CT_user_vernac
(CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:38:40 +0000