diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/ascent.mli | 3 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml4 | 55 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 7 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 1534 |
4 files changed, 67 insertions, 1532 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 4527f6608..a1f6e2489 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 a0620d4ba..b1602655f 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 597553cd5..e2f519504 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 d3d25534c..2dc5aa311 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)) |