diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/COPYRIGHT | 6 | ||||
| -rw-r--r-- | contrib/interface/ascent.mli | 9 | ||||
| -rw-r--r-- | contrib/interface/blast.ml | 59 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml4 | 408 | ||||
| -rw-r--r-- | contrib/interface/debug_tac.ml4 | 10 | ||||
| -rw-r--r-- | contrib/interface/depends.ml | 454 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 12 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.mli | 4 | ||||
| -rw-r--r-- | contrib/interface/parse.ml | 27 | ||||
| -rw-r--r-- | contrib/interface/pbp.ml | 16 | ||||
| -rw-r--r-- | contrib/interface/showproof.ml | 23 | ||||
| -rw-r--r-- | contrib/interface/translate.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/translate.mli | 1 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 1575 | ||||
| -rw-r--r-- | contrib/interface/vtp.mli | 27 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 337 | ||||
| -rw-r--r-- | contrib/interface/xlate.mli | 1 |
17 files changed, 1869 insertions, 1103 deletions
diff --git a/contrib/interface/COPYRIGHT b/contrib/interface/COPYRIGHT index 2fb11c6b..23aeb6bb 100644 --- a/contrib/interface/COPYRIGHT +++ b/contrib/interface/COPYRIGHT @@ -1,8 +1,9 @@ (*****************************************************************************) (* *) -(* Coq support for the Pcoq Graphical Interface of Coq *) +(* Coq support for the Pcoq and tmEgg Graphical Interfaces of Coq *) (* *) (* Copyright (C) 1999-2004 INRIA Sophia-Antipolis (Lemme team) *) +(* Copyright (C) 2006,2007 Lionel Elie Mamane *) (* *) (*****************************************************************************) @@ -10,6 +11,9 @@ The current directory contrib/interface implements Coq support for the Pcoq Graphical Interface of Coq. It has been developed by Yves Bertot with contributions from Loïc Pottier and Laurence Rideau. +Modifications by Lionel Elie Mamane <lionel@mamane.lu> for +generalising the protocol to suit other Coq interfaces. + The Pcoq Graphical Interface (see http://www-sop.inria.fr/lemme/pcoq) is developed by the Lemme team at INRIA Sophia-Antipolis (see http://www-sop.inria.fr/lemme) diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index ef1d095e..32338523 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -113,7 +113,6 @@ and ct_COMMAND = | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT | CT_no_inline of ct_ID_NE_LIST | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE - | CT_opaque of ct_ID_NE_LIST | CT_open_scope of ct_ID | CT_print | CT_print_about of ct_ID @@ -189,13 +188,13 @@ and ct_COMMAND = | CT_show_script | CT_show_tree | CT_solve of ct_INT * ct_TACTIC_COM * ct_DOTDOT_OPT + | CT_strategy of ct_LEVEL_LIST | CT_suspend | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT | CT_tactic_definition of ct_TAC_DEF_NE_LIST | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT | CT_time of ct_COMMAND - | CT_transparent of ct_ID_NE_LIST | CT_undo of ct_INT_OPT | CT_unfocus | CT_unset_option of ct_TABLE @@ -204,6 +203,12 @@ and ct_COMMAND = | CT_user_vernac of ct_ID * ct_VARG_LIST | CT_variable of ct_VAR * ct_BINDER_NE_LIST | CT_write_module of ct_ID * ct_STRING_OPT +and ct_LEVEL_LIST = + CT_level_list of (ct_LEVEL * ct_ID_LIST) list +and ct_LEVEL = + CT_Opaque + | CT_Level of ct_INT + | CT_Expand and ct_COMMAND_LIST = CT_command_list of ct_COMMAND * ct_COMMAND list and ct_COMMENT = diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index dc27cf98..6ec0fac4 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -151,7 +151,7 @@ let pp_string x = let unify_e_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in - vernac_e_resolve_constr c gls + Hiddentac.h_simplest_eapply c gls let rec e_trivial_fail_db db_list local_db goal = let tacl = @@ -161,33 +161,36 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (add_hint_list hintl local_db) g'))) :: (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in + let flags = Auto.auto_unif_flags in let hintl = if occur_existential concl then - list_map_append (Hint_db.map_all hdc) (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) + (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) + (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = - fun ({pri=b; pat = p; code=t} as _patac) -> + fun (st, ({pri=b; pat = p; code=t} as _patac)) -> (b, let tac = match t with - | Res_pf (term,cl) -> unify_resolve (term,cl) + | Res_pf (term,cl) -> unify_resolve st (term,cl) | ERes_pf (term,cl) -> unify_e_resolve (term,cl) | Give_exact (c) -> e_give_exact_constr c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> Auto.conclPattern concl - (out_some p) tacast + (Option.get p) tacast in (free_try tac,fmt_autotactic t)) (*i @@ -227,8 +230,8 @@ module MySearchProblem = struct depth : int; (*r depth of search before failing *) tacres : goal list sigma * validation; last_tactic : std_ppcmds; - dblist : Auto.Hint_db.t list; - localdb : Auto.Hint_db.t list } + dblist : Auto.hint_db list; + localdb : Auto.hint_db list } let success s = (sig_it (fst s.tacres)) = [] @@ -242,9 +245,6 @@ module MySearchProblem = struct with e when Logic.catchable_exception e -> filter_tactics (glls,v) tacl - let rec list_addn n x l = - if n = 0 then l else x :: (list_addn (pred n) x l) - (* Ordering of states is lexicographic on depth (greatest first) then number of remaining goals. *) let compare s s' = @@ -279,7 +279,7 @@ module MySearchProblem = struct let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in - let ldb = Hint_db.add_list hintl (List.hd s.localdb) in + let ldb = add_hint_list hintl (List.hd s.localdb) in { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb }) @@ -337,7 +337,7 @@ let e_breadth_search debug n db_list local_db gl = with Not_found -> error "EAuto: breadth first search failed" let e_search_auto debug (n,p) db_list gl = - let local_db = make_local_hint_db [] gl in + let local_db = make_local_hint_db true [] gl in if n = 0 then e_depth_search debug p db_list local_db gl else @@ -357,7 +357,7 @@ let full_eauto debug n gl = let dbnames = current_db_names () in let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map searchtable_map dbnames in - let _local_db = make_local_hint_db [] gl in + let _local_db = make_local_hint_db true [] gl in tclTRY (e_search_auto debug n db_list) gl let my_full_eauto n gl = full_eauto false (n,0) gl @@ -375,7 +375,7 @@ let rec trivial_fail_db db_list local_db gl = tclTHEN intro (fun g'-> let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') + in trivial_fail_db db_list (add_hint_list hintl local_db) g') in tclFIRST (assumption::intro_tac:: @@ -383,27 +383,29 @@ let rec trivial_fail_db db_list local_db gl = (trivial_resolve db_list local_db (pf_concl gl)))) gl and my_find_search db_list local_db hdc concl = + let flags = Auto.auto_unif_flags in let tacl = if occur_existential concl then - list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) + (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db) - (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) + (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in List.map - (fun ({pri=b; pat=p; code=t} as _patac) -> + (fun (st, {pri=b; pat=p; code=t} as _patac) -> (b, match t with - | Res_pf (term,cl) -> unify_resolve (term,cl) + | Res_pf (term,cl) -> unify_resolve st (term,cl) | ERes_pf (_,c) -> (fun gl -> error "eres_pf") | Give_exact c -> exact_check c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN - (unify_resolve (term,cl)) + (unify_resolve st (term,cl)) (trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> - conclPattern concl (out_some p) tacast)) + conclPattern concl (Option.get p) tacast)) tacl and trivial_resolve db_list local_db cl = @@ -470,11 +472,12 @@ let rec search_gen decomp n db_list local_db extra_sign goal = try [make_apply_entry (pf_env g') (project g') (true,false) - (mkVar hid,body_of_type htyp)] + None + (mkVar hid,htyp)] with Failure _ -> [] in (free_try - (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d]) + (search_gen decomp n db_list (add_hint_list hintl local_db) [d]) g')) in let rec_tacs = @@ -497,7 +500,7 @@ let full_auto n gl = let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map searchtable_map dbnames in let hyps = pf_hyps gl in - tclTRY (search n db_list (make_local_hint_db [] gl) hyps) gl + tclTRY (search n db_list (make_local_hint_db false [] gl) hyps) gl let default_full_auto gl = full_auto !default_search_depth gl (************************************************************************) diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 730e055b..a4dc0eac 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -1,11 +1,28 @@ (*i camlp4deps: "parsing/grammar.cma" i*) +(* + * This file has been modified by Lionel Elie Mamane <lionel@mamane.lu> + * to implement the following features + * - Terms (optionally) as pretty-printed string and not trees + * - (Optionally) give most commands their usual Coq semantics + * - Add the backtracking information to the status message. + * in the following time period + * - May-November 2006 + * and + * - Make use of new Command.save_hook to generate dependencies at + * save-time. + * in + * - June 2007 + *) + (*Toplevel loop for the communication between Coq and Centaur *) open Names;; open Nameops;; open Util;; open Term;; open Pp;; +open Ppconstr;; +open Prettyp;; open Libnames;; open Libobject;; open Library;; @@ -43,6 +60,7 @@ open Showproof;; open Showproof_ct;; open Tacexpr;; open Vernacexpr;; +open Printer;; let pcoq_started = ref None;; @@ -51,6 +69,11 @@ let if_pcoq f a = let text_proof_flag = ref "en";; +let pcoq_history = ref true;; + +let assert_pcoq_history f a = + if !pcoq_history then f a else error "Pcoq-style history tracking deactivated";; + let current_proof_name () = try string_of_id (get_current_proof_name ()) @@ -85,10 +108,33 @@ let kill_proof_node index = History.border_length (current_proof_name());; +type vtp_tree = + | P_rl of ct_RULE_LIST + | P_r of ct_RULE + | P_s_int of ct_SIGNED_INT_LIST + | P_pl of ct_PREMISES_LIST + | P_cl of ct_COMMAND_LIST + | P_t of ct_TACTIC_COM + | P_text of ct_TEXT + | P_ids of ct_ID_LIST;; + +let print_tree t = + (match t with + | P_rl x -> fRULE_LIST x + | P_r x -> fRULE x + | P_s_int x -> fSIGNED_INT_LIST x + | P_pl x -> fPREMISES_LIST x + | P_cl x -> fCOMMAND_LIST x + | P_t x -> fTACTIC_COM x + | P_text x -> fTEXT x + | P_ids x -> fID_LIST x) + ++ (str "e\nblabla\n");; + + (*Message functions, the text of these messages is recognized by the protocols *) (*of CtCoq *) let ctf_header message_name request_id = - fnl () ++ str "message" ++ fnl() ++ str message_name ++ fnl() ++ + str "message" ++ fnl() ++ str message_name ++ fnl() ++ int request_id ++ fnl();; let ctf_acknowledge_command request_id command_count opt_exn = @@ -97,14 +143,20 @@ let ctf_acknowledge_command request_id command_count opt_exn = let g_count = List.length (fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in - g_count, (min g_count !current_goal_index) + g_count, !current_goal_index else - (0, 0) in + (0, 0) + and statnum = Lib.current_command_label () + and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0 + and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in (ctf_header "acknowledge" request_id ++ int command_count ++ fnl() ++ int goal_count ++ fnl () ++ int goal_index ++ fnl () ++ str (current_proof_name()) ++ fnl() ++ + int statnum ++ fnl() ++ + print_tree (P_ids pending) ++ + int dpth ++ fnl() ++ (match opt_exn with Some e -> Cerrors.explain_exn e | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; @@ -126,6 +178,8 @@ let ctf_PathGoalMessage () = let ctf_GoalReqIdMessage = ctf_header "single_goal_state";; +let ctf_GoalsReqIdMessage = ctf_header "goals_state";; + let ctf_NewStateMessage = ctf_header "fresh_state";; let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ @@ -153,39 +207,16 @@ let ctf_ResetIdentMessage request_id s = ctf_header "reset_ident" request_id ++ str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; -type vtp_tree = - | P_rl of ct_RULE_LIST - | P_r of ct_RULE - | P_s_int of ct_SIGNED_INT_LIST - | P_pl of ct_PREMISES_LIST - | P_cl of ct_COMMAND_LIST - | P_t of ct_TACTIC_COM - | P_text of ct_TEXT - | P_ids of ct_ID_LIST;; - -let print_tree t = - (match t with - | P_rl x -> fRULE_LIST x - | P_r x -> fRULE x - | P_s_int x -> fSIGNED_INT_LIST x - | P_pl x -> fPREMISES_LIST x - | P_cl x -> fCOMMAND_LIST x - | P_t x -> fTACTIC_COM x - | P_text x -> fTEXT x - | P_ids x -> fID_LIST x); - print_string "e\nblabla\n";; - - let break_happened = ref false;; let output_results stream vtp_tree = let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> (break_happened := true;()))) in - msg stream; - match vtp_tree with - Some t -> print_tree t - | None -> ();; + msg (stream ++ + (match vtp_tree with + Some t -> print_tree t + | None -> mt()));; let output_results_nl stream = let _ = Sys.signal Sys.sigint @@ -221,20 +252,18 @@ let print_past_goal index = let show_nth n = try - let pf = proof_of_pftreestate (get_pftreestate()) in - if (!text_proof_flag<>"off") then - (if n=0 - then output_results (ctf_TextMessage !global_request_id) - (Some (P_text (show_proof !text_proof_flag []))) - else - let path = History.get_nth_open_path (current_proof_name()) n in - output_results (ctf_TextMessage !global_request_id) - (Some (P_text (show_proof !text_proof_flag path)))) - else - output_results (ctf_GoalReqIdMessage !global_request_id) - (let goal = List.nth (fst (frontier pf)) - (n - 1) in - (Some (P_r (translate_goal goal)))) + output_results (ctf_GoalReqIdMessage !global_request_id + ++ pr_nth_open_subgoal n) + None + with + | Invalid_argument s -> + error "No focused proof (No proof-editing in progress)";; + +let show_subgoals () = + try + output_results (ctf_GoalReqIdMessage !global_request_id + ++ pr_open_subgoals ()) + None with | Invalid_argument s -> error "No focused proof (No proof-editing in progress)";; @@ -275,39 +304,24 @@ let ctf_EmptyGoalMessage id = fnl () ++ str "Empty Goal is a no-op. Fun oh fun." ++ fnl ();; -let print_check judg = - let {uj_val=value; uj_type=typ} = judg in - let value_ct_ast = - (try translate_constr false (Global.env()) value - with UserError(f,str) -> - raise(UserError(f,Printer.pr_lconstr value ++ - fnl () ++ str ))) in - let type_ct_ast = - (try translate_constr false (Global.env()) typ - with UserError(f,str) -> - raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in - ((ctf_SearchResults !global_request_id), - (Some (P_pl - (CT_premises_list - [CT_coerce_TYPED_FORMULA_to_PREMISE - (CT_typed_formula(value_ct_ast,type_ct_ast) - )]))));; - -let ct_print_eval ast red_fun env judg = -((if refining() then traverse_to []); -let {uj_val=value; uj_type=typ} = judg in -let nvalue = red_fun value -(* // Attention , ici il faut peut être utiliser des environnemenst locaux *) -and ntyp = nf_betaiota typ in -(ctf_SearchResults !global_request_id, - Some (P_pl - (CT_premises_list - [CT_eval_result - (xlate_formula ast, - translate_constr false env nvalue, - translate_constr false env ntyp)]))));; - - +let print_check env judg = + ((ctf_SearchResults !global_request_id) ++ + print_judgment env judg, + None);; + +let ct_print_eval red_fun env evmap ast judg = + (if refining() then traverse_to []); + let {uj_val=value; uj_type=typ} = judg in + let nvalue = (red_fun env evmap) value + (* // Attention , ici il faut peut être utiliser des environnemenst locaux *) + and ntyp = nf_betaiota typ in + print_tree + (P_pl + (CT_premises_list + [CT_eval_result + (xlate_formula ast, + translate_constr false env nvalue, + translate_constr false env ntyp)]));; let pbp_tac_pcoq = pbp_tac (function (x:raw_tactic_expr) -> @@ -330,6 +344,7 @@ let dad_tac_pcoq = </cpa> *) let search_output_results () = + (* LEM: See comments for pcoq_search *) output_results (ctf_SearchResults !global_request_id) (Some (P_pl (CT_premises_list @@ -393,7 +408,7 @@ let inspect n = oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> - let (_, _, v) = get_variable (basename sp) in + let (_, _, v) = Global.lookup_named (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in @@ -491,19 +506,19 @@ VERNAC COMMAND EXTEND OutputGoal END VERNAC COMMAND EXTEND OutputGoal - [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ] + [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ assert_pcoq_history (simulate_solve n) tac ] END VERNAC COMMAND EXTEND KillProofAfter -| [ "Kill" "Proof" "after" natural(n) ] -> [ kill_node_verbose n ] +| [ "Kill" "Proof" "after" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ] END VERNAC COMMAND EXTEND KillProofAt -| [ "Kill" "Proof" "at" natural(n) ] -> [ kill_node_verbose n ] +| [ "Kill" "Proof" "at" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ] END VERNAC COMMAND EXTEND KillSubProof - [ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ] + [ "Kill" "SubProof" natural(n) ] -> [ assert_pcoq_history logical_kill n ] END VERNAC COMMAND EXTEND PcoqReset @@ -515,18 +530,17 @@ VERNAC COMMAND EXTEND PcoqResetInitial END let start_proof_hook () = - History.start_proof (current_proof_name()); + if !pcoq_history then History.start_proof (current_proof_name()); current_goal_index := 1 let solve_hook n = - let name = current_proof_name () in - let old_n_count = History.border_length name in - let pf = proof_of_pftreestate (get_pftreestate ()) in - let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in - begin - current_goal_index := n; - History.push_command name n n_goals - end + current_goal_index := n; + if !pcoq_history then + let name = current_proof_name () in + let old_n_count = History.border_length name in + let pf = proof_of_pftreestate (get_pftreestate ()) in + let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in + History.push_command name n n_goals let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s) @@ -535,6 +549,12 @@ let interp_search_about_item = function | SearchString s -> GlobSearchString s let pcoq_search s l = + (* LEM: I don't understand why this is done in this way (redoing the + * match on s here) instead of making the code in + * parsing/search.ml call the right function instead of + * "plain_display". Investigates this later. + * TODO + *) ctv_SEARCH_LIST:=[]; begin match s with | SearchAbout sl -> @@ -581,27 +601,25 @@ let hyp_search_pattern c l = (Some (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));; let pcoq_print_name ref = - let results = xlate_vernac_list (name_to_ast ref) in output_results - (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ()) - (Some (P_cl results)) + (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl () ++ print_name ref ) + None -let pcoq_print_check j = - let a,b = print_check j in output_results a b +let pcoq_print_check env j = + let a,b = print_check env j in output_results a b -let pcoq_print_eval redfun env c j = - let strm, vtp = ct_print_eval c redfun env j in - output_results strm vtp;; +let pcoq_print_eval redfun env evmap c j = + output_results + (ctf_SearchResults !global_request_id + ++ Prettyp.print_eval redfun env evmap c j) + None;; open Vernacentries let pcoq_show_goal = function | Some n -> show_nth n - | None -> - if !pcoq_started = Some true (* = debug *) then - msg (Printer.pr_open_subgoals ()) - else errorlabstrm "show_goal" - (str "Show must be followed by an integer in Centaur mode");; + | None -> show_subgoals () +;; let pcoq_hook = { start_proof = start_proof_hook; @@ -614,6 +632,165 @@ let pcoq_hook = { show_goal = pcoq_show_goal } +let pcoq_term_pr = { + pr_constr_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_constr_expr c)); + (* In future translate_constr false (Global.env()) + * Except with right bool/env which I'll get :) + *) + pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")"); + pr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr c)); + pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lpattern_expr c)) +} + +let start_pcoq_trees () = + set_term_pr pcoq_term_pr + +(* BEGIN functions for object_pr *) + +(* These functions in general mirror what name_to_ast does in a subcase, + and then print the corresponding object as a PCoq tree. *) + +let object_to_ast_template object_to_ast_list sp = + let l = object_to_ast_list sp in + VernacList (List.map (fun x -> (dummy_loc, x)) l) + +let pcoq_print_object_template object_to_ast_list sp = + let results = xlate_vernac_list (object_to_ast_template object_to_ast_list sp) in + print_tree (P_cl results) + +(* This function mirror what print_check does *) + +let pcoq_print_typed_value_in_env env (value, typ) = + let value_ct_ast = + (try translate_constr false (Global.env()) value + with UserError(f,str) -> + raise(UserError(f,Printer.pr_lconstr value ++ + fnl () ++ str ))) in + let type_ct_ast = + (try translate_constr false (Global.env()) typ + with UserError(f,str) -> + raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in + print_tree + (P_pl + (CT_premises_list + [CT_coerce_TYPED_FORMULA_to_PREMISE + (CT_typed_formula(value_ct_ast,type_ct_ast) + )])) +;; + +(* This function mirrors what show_nth does *) + +let pcoq_pr_subgoal n gl = + try + print_tree + (if (!text_proof_flag<>"off") then + (* This is a horrendeous hack; it ignores the "gl" argument + and just takes the currently focused proof. This will bite + us back one day. + TODO: Fix this. + *) + ( + if not !pcoq_history then error "Text mode requires Pcoq history tracking."; + if n=0 + then (P_text (show_proof !text_proof_flag [])) + else + let path = History.get_nth_open_path (current_proof_name()) n in + (P_text (show_proof !text_proof_flag path))) + else + (let goal = List.nth gl (n - 1) in + (P_r (translate_goal goal)))) + with + | Invalid_argument _ + | Failure "nth" + | Not_found -> error "No such goal";; + +let pcoq_pr_subgoals close_cmd evar gl = + (*LEM: TODO: we should check for evar emptiness or not, and do something *) + try + print_tree + (if (!text_proof_flag<>"off") then + raise (Anomaly ("centaur.ml4:pcoq_pr_subgoals", str "Text mode show all subgoals not implemented")) + else + (P_rl (translate_goals gl))) + with + | Invalid_argument _ + | Failure "nth" + | Not_found -> error "No such goal";; + + +(* END functions for object_pr *) + +let pcoq_object_pr = { + print_inductive = pcoq_print_object_template inductive_to_ast_list; + (* TODO: Check what that with_infos means, and adapt accordingly *) + print_constant_with_infos = pcoq_print_object_template constant_to_ast_list; + print_section_variable = pcoq_print_object_template variable_to_ast_list; + print_syntactic_def = pcoq_print_object_template (fun x -> errorlabstrm "print" + (str "printing of syntax definitions not implemented in PCoq syntax")); + (* TODO: These are placeholders only; write them *) + print_module = (fun x y -> str "pcoq_print_module not implemented"); + print_modtype = (fun x -> str "pcoq_print_modtype not implemented"); + print_named_decl = (fun x -> str "pcoq_print_named_decl not implemented"); + (* TODO: Find out what the first argument x (a bool) is about and react accordingly *) + print_leaf_entry = (fun x -> pcoq_print_object_template leaf_entry_to_ast_list); + print_library_entry = (fun x y -> Some (str "pcoq_print_library_entry not implemented")); + print_context = (fun x y z -> str "pcoq_print_context not implemented"); + print_typed_value_in_env = pcoq_print_typed_value_in_env; + Prettyp.print_eval = ct_print_eval; +};; + +let pcoq_printer_pr = { + pr_subgoals = pcoq_pr_subgoals; + pr_subgoal = pcoq_pr_subgoal; + pr_goal = (fun x -> str "pcoq_pr_goal not implemented"); +};; + + +let start_pcoq_objects () = + set_object_pr pcoq_object_pr; + set_printer_pr pcoq_printer_pr + +let start_default_objects () = + set_object_pr default_object_pr; + set_printer_pr default_printer_pr + +let full_name_of_ref r = + (match r with + | VarRef _ -> str "VAR" + | ConstRef _ -> str "CST" + | IndRef _ -> str "IND" + | ConstructRef _ -> str "CSR") + ++ str " " ++ (pr_sp (Nametab.sp_of_global r)) + (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *) + +let string_of_ref = + (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*) + Depends.o Libnames.string_of_path Nametab.sp_of_global + +let print_depends compute_depends ptree = + output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl()) + (str "This object depends on:" ++ fnl()) + (compute_depends ptree)) + None + +let output_depends compute_depends ptree = + (* Using an ident list for that is arguably stretching it, but less effort than touching the vtp types *) + output_results (ctf_header "depends" !global_request_id ++ + print_tree (P_ids (CT_id_list (List.map + (fun x -> CT_ident (string_of_ref x)) + (compute_depends ptree))))) + None + +let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' = + Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[])); + Command.set_declare_assumption_hook (print_depends (fun (c:types) -> Depends.depends_of_constr c [])); + Command.set_start_hook (print_depends (fun c -> Depends.depends_of_constr c [])); + Command.set_save_hook (print_depends'' (Depends.depends_of_pftreestate Depends.depends_of_pftree)); + Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt [])) + +let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends + +let start_depends_dumps_debug () = gen_start_depends_dumps print_depends print_depends print_depends print_depends TACTIC EXTEND pbp | [ "pbp" ident_opt(idopt) natural_list(nl) ] -> @@ -635,7 +812,6 @@ let start_pcoq_mode debug = (* <\cpa> start_dad(); </cpa> *) - declare_in_coq(); (* The following ones are added to enable rich comments in pcoq *) (* TODO ... add_tactic "Image" (fun _ -> tclIDTAC); @@ -649,6 +825,8 @@ let start_pcoq_mode debug = List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes; *) set_pcoq_hook pcoq_hook; + start_pcoq_objects(); + Flags.print_emacs := false; Pp.make_pp_nonemacs(); end;; @@ -681,3 +859,23 @@ END VERNAC COMMAND EXTEND StartPcoqDebug | [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ] END + +VERNAC COMMAND EXTEND StartPcoqTerms +| [ "Start" "Pcoq" "Trees" ] -> [ start_pcoq_trees () ] +END + +VERNAC COMMAND EXTEND StartPcoqObjects +| [ "Start" "Pcoq" "Objects" ] -> [ start_pcoq_objects () ] +END + +VERNAC COMMAND EXTEND StartDefaultObjects +| [ "Start" "Default" "Objects" ] -> [ start_default_objects () ] +END + +VERNAC COMMAND EXTEND StartDependencyDumps +| [ "Start" "Dependency" "Dumps" ] -> [ start_depends_dumps () ] +END + +VERNAC COMMAND EXTEND StopPcoqHistory +| [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ] +END diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index 890bb3ce..aad3a765 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -113,7 +113,7 @@ let count_subgoals2 let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function TacThens (a,l) -> (fun report_holder -> checked_thens report_holder a l) - | TacThen (a,b) -> + | TacThen (a,[||],b,[||]) -> (fun report_holder -> checked_then report_holder a b) | t -> (fun report_holder g -> @@ -279,7 +279,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) = | Failed n -> TacId [] | Tree_fail r -> reconstruct_success_tac a r | Mismatch (n,p) -> a) - | TacThen (a,b) -> + | TacThen (a,[||],b,[||]) -> (function Report_node(true, n, l) -> tac | Report_node(false, n, rl) -> @@ -340,7 +340,7 @@ Tacinterp.add_tactic "OnThen" on_then;; let rec clean_path tac l = match tac, l with - | TacThen (a,b), fst::tl -> + | TacThen (a,[||],b,[||]), fst::tl -> fst::(clean_path (if fst = 1 then a else b) tl) | TacThens (a,l), 1::tl -> 1::(clean_path a tl) @@ -390,7 +390,7 @@ let rec report_error | t::tl -> (report_error t the_goal the_ast returned_path (n::2::path)):: (fold_num (n + 1) tl) in fold_num 1 l) - | TacThen (a,b) -> + | TacThen (a,[||],b,[||]) -> let the_count = ref 1 in tclTHEN (fun g -> @@ -398,7 +398,7 @@ let rec report_error report_error a the_goal the_ast returned_path (1::path) g with e -> - (the_ast := TacThen (!the_ast, b); + (the_ast := TacThen (!the_ast,[||], b,[||]); raise e)) (fun g -> try diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml new file mode 100644 index 00000000..dd40c5cc --- /dev/null +++ b/contrib/interface/depends.ml @@ -0,0 +1,454 @@ +(************************************************************************) +(* v * The Coq Proof Assistant *) +(* <O___,, * *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1, *) +(* * or (at your option) any later version. *) +(************************************************************************) + +(* Copyright © 2007, Lionel Elie Mamane <lionel@mamane.lu> *) + +(* This is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *) +(* Lesser General Public License for more details. *) + +(* You should have received a copy of the GNU Lesser General Public *) +(* License along with this library; if not, write to the Free Software *) +(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, *) +(* MA 02110-1301, USA *) + + +(* LEM TODO: a .mli file *) + +open Refiner +open Proof_type +open Rawterm +open Term +open Libnames +open Util +open Tacexpr +open Entries + +(* DBG utilities, to be removed *) +let print_bool b = print_string (string_of_bool b) +let string_of_ppcmds p = Pp.pp_with Format.str_formatter p; Format.flush_str_formatter() +let acc_str f = List.fold_left (fun a b -> a ^ (f b) ^ "+") "O" +(* End utilities, to be removed *) + +let explore_tree pfs = + print_string "explore_tree called\n"; + print_string "pfs is a top: "; + (* We expect yes. *) + print_string (if (is_top_pftreestate pfs) then "yes" else "no"); + print_newline(); + let rec explain_tree (pt:proof_tree) = + match pt.ref with + | None -> "none" + | Some (Prim p, l) -> "<Prim (" ^ (explain_prim p) ^ ") | " ^ (acc_str explain_tree l) ^ ">" + | Some (Nested (t,p), l) -> "<Nested (" ^ explain_compound t ^ ", " ^ (explain_tree p) ^ ") | " ^ (acc_str explain_tree l) ^ ">" + | Some (Decl_proof _, _) -> "Decl_proof" + | Some (Daimon, _) -> "Daimon" + and explain_compound cr = + match cr with + | Tactic (texp, b) -> "Tactic (" ^ (string_of_ppcmds (Tactic_printer.pr_tactic texp)) ^ ", " ^ (string_of_bool b) ^ ")" + | Proof_instr (b, instr) -> "Proof_instr (" ^ (string_of_bool b) ^ (string_of_ppcmds (Tactic_printer.pr_proof_instr instr)) ^ ")" + and explain_prim = function + | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c)) + | Intro identifier -> "Intro" + | Intro_replacing identifier -> "Intro_replacing" + | Cut (bool, identifier, types) -> "Cut" + | FixRule (identifier, int, l) -> "FixRule" + | Cofix (identifier, l) -> "Cofix" + | Convert_concl (types, cast_kind) -> "Convert_concl" + | Convert_hyp named_declaration -> "Convert_hyp" + | Thin identifier_list -> "Thin" + | ThinBody identifier_list -> "ThinBody" + | Move (bool, identifier, identifier') -> "Move" + | Rename (identifier, identifier') -> "Rename" + | Change_evars -> "Change_evars" + in + let pt = proof_of_pftreestate pfs in + (* We expect 0 *) + print_string "Number of open subgoals: "; + print_int pt.open_subgoals; + print_newline(); + print_string "First rule is a "; + print_string (explain_tree pt); + print_newline() + + +let o f g x = f (g x) +let fst_of_3 (x, _, _) = x +let snd_of_3 (_, x, _) = x +let trd_of_3 (_, _, x) = x + +(* TODO: These for now return a Libnames.global_reference, but a + prooftree will also depend on things like tactic declarations, etc + so we may need a new type for that. *) +let rec depends_of_hole_kind hk acc = match hk with + | Evd.ImplicitArg (gr,_) -> gr::acc + | Evd.TomatchTypeParameter (ind, _) -> (IndRef ind)::acc + | Evd.BinderType _ + | Evd.QuestionMark _ + | Evd.CasesType + | Evd.InternalHole + | Evd.GoalEvar + | Evd.ImpossibleCase -> acc + +let depends_of_'a_cast_type depends_of_'a act acc = match act with + | CastConv (ck, a) -> depends_of_'a a acc + | CastCoerce -> acc + +let depends_of_'a_bindings depends_of_'a ab acc = match ab with + | ImplicitBindings al -> list_union_map depends_of_'a al acc + | ExplicitBindings apl -> list_union_map (fun x y -> depends_of_'a (trd_of_3 x) y) apl acc + | NoBindings -> acc + +let depends_of_'a_with_bindings depends_of_'a (a, ab) acc = + depends_of_'a a (depends_of_'a_bindings depends_of_'a ab acc) + +(* let depends_of_constr_with_bindings = depends_of_'a_with_bindings depends_of_constr *) +(* and depends_of_open_constr_with_bindings = depends_of_'a_with_bindings depends_of_open_let *) + +let depends_of_'a_induction_arg depends_of_'a aia acc = match aia with + | ElimOnConstr a -> depends_of_'a a acc + | ElimOnIdent _ -> + (* TODO: Check that this really refers only to an hypothesis (not a section variable, etc.) + * It *seems* thaat section variables are seen as hypotheses, so we have a problem :-( + + * Plan: Load all section variables before anything in that + * section and call the user's proof script "brittle" and refuse + * to handle if it breaks because of that + *) + acc + | ElimOnAnonHyp _ -> acc + +let depends_of_'a_or_var depends_of_'a aov acc = match aov with + | ArgArg a -> depends_of_'a a acc + | ArgVar _ -> acc + +let depends_of_'a_with_occurences depends_of_'a (_,a) acc = + depends_of_'a a acc + +let depends_of_'a_'b_red_expr_gen depends_of_'a reg acc = match reg with + (* TODO: dirty assumption that the 'b doesn't make any dependency *) + | Red _ + | Hnf + | Cbv _ + | Lazy _ + | Unfold _ + | ExtraRedExpr _ + | CbvVm -> acc + | Simpl awoo -> + Option.fold_right + (depends_of_'a_with_occurences depends_of_'a) + awoo + acc + | Fold al -> list_union_map depends_of_'a al acc + | Pattern awol -> + list_union_map + (depends_of_'a_with_occurences depends_of_'a) + awol + acc + +let depends_of_'a_'b_inversion_strength depends_of_'a is acc = match is with + (* TODO: dirty assumption that the 'b doesn't make any dependency *) + | NonDepInversion _ -> acc + | DepInversion (_, ao, _) -> Option.fold_right depends_of_'a ao acc + | InversionUsing (a, _) -> depends_of_'a a acc + +let depends_of_'a_pexistential depends_of_'a (_, aa) acc = array_union_map depends_of_'a aa acc + +let depends_of_named_vals nvs acc = + (* TODO: I'm stopping here because I have noooo idea what to do with values... *) + acc + +let depends_of_inductive ind acc = (IndRef ind)::acc + +let rec depends_of_constr c acc = match kind_of_term c with + | Rel _ -> acc + | Var id -> (VarRef id)::acc + | Meta _ -> acc + | Evar ev -> depends_of_'a_pexistential depends_of_constr ev acc + | Sort _ -> acc + | Cast (c, _, t) -> depends_of_constr c (depends_of_constr t acc) + | Prod (_, t, t') -> depends_of_constr t (depends_of_constr t' acc) + | Lambda (_, t, c) -> depends_of_constr t (depends_of_constr c acc) + | LetIn (_, c, t, c') -> depends_of_constr c (depends_of_constr t (depends_of_constr c' acc)) + | App (c, ca) -> depends_of_constr c (array_union_map depends_of_constr ca acc) + | Const cnst -> (ConstRef cnst)::acc + | Ind ind -> (IndRef ind)::acc + | Construct cons -> (ConstructRef cons)::acc + | Case (_, c, c', ca) -> depends_of_constr c (depends_of_constr c' (array_union_map depends_of_constr ca acc)) + | Fix (_, (_, ta, ca)) + | CoFix (_, (_, ta, ca)) -> array_union_map depends_of_constr ca (array_union_map depends_of_constr ta acc) +and depends_of_evar_map evm acc = + Evd.fold (fun ev evi -> depends_of_evar_info evi) evm acc +and depends_of_evar_info evi acc = + (* TODO: evi.evar_extra contains a dynamic... Figure out what to do with it. *) + depends_of_constr evi.Evd.evar_concl (depends_of_evar_body evi.Evd.evar_body (depends_of_named_context_val evi.Evd.evar_hyps acc)) +and depends_of_evar_body evb acc = match evb with + | Evd.Evar_empty -> acc + | Evd.Evar_defined c -> depends_of_constr c acc +and depends_of_named_context nc acc = list_union_map depends_of_named_declaration nc acc +and depends_of_named_context_val ncv acc = + depends_of_named_context (Environ.named_context_of_val ncv) (depends_of_named_vals (Environ.named_vals_of_val ncv) acc) +and depends_of_named_declaration (_,co,t) acc = depends_of_constr t (Option.fold_right depends_of_constr co acc) + + + +let depends_of_open_constr (evm,c) acc = + depends_of_constr c (depends_of_evar_map evm acc) + +let rec depends_of_rawconstr rc acc = match rc with + | RRef (_,r) -> r::acc + | RVar (_, id) -> (VarRef id)::acc + | REvar (_, _, rclo) -> Option.fold_right depends_of_rawconstr_list rclo acc + | RPatVar _ -> acc + | RApp (_, rc, rcl) -> depends_of_rawconstr rc (depends_of_rawconstr_list rcl acc) + | RLambda (_, _, _, rct, rcb) + | RProd (_, _, _, rct, rcb) + | RLetIn (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc) + | RCases (_, _, rco, tmt, cc) -> + (* LEM TODO: handle the cc *) + (Option.fold_right depends_of_rawconstr rco + (list_union_map + (fun (rc, pp) acc -> + Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp) + (depends_of_rawconstr rc acc)) + tmt + acc)) + | RLetTuple (_,_,(_,rco),rc0,rc1) -> + depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc)) + | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in + dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc)))) + | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in + dorca rca0 (dorca rca1 (array_union_map + (list_union_map (fun (_,_,rco,rc) acc -> depends_of_rawconstr rc (Option.fold_right depends_of_rawconstr rco acc))) + rdla + acc)) + | RSort _ -> acc + | RHole (_, hk) -> depends_of_hole_kind hk acc + | RCast (_, rc, rcct) -> depends_of_rawconstr rc (depends_of_'a_cast_type depends_of_rawconstr rcct acc) + | RDynamic (_, dyn) -> failwith "Depends of a dyn not implemented yet" (* TODO: figure out how these dyns are used*) +and depends_of_rawconstr_list l = list_union_map depends_of_rawconstr l + +let depends_of_rawconstr_and_expr (rc, _) acc = + (* TODO Le constr_expr représente le même terme que le rawconstr. Vérifier ça. *) + depends_of_rawconstr rc acc + +let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of_'tac = + (* TODO: + * Dirty assumptions that the 'id, 'cst, 'ref don't generate dependencies + *) + let rec depends_of_tacexpr texp acc = match texp with + | TacAtom (_, atexpr) -> depends_of_atomic_tacexpr atexpr acc + | TacThen (tac0, taca0, tac1, taca1) -> + depends_of_tacexpr tac0 (array_union_map depends_of_tacexpr taca0 (depends_of_tacexpr tac1 (array_union_map depends_of_tacexpr taca1 acc))) + | TacThens (tac, tacl) -> + depends_of_tacexpr tac (list_union_map depends_of_tacexpr tacl acc) + | TacFirst tacl -> list_union_map depends_of_tacexpr tacl acc + | TacComplete tac -> depends_of_tacexpr tac acc + | TacSolve tacl -> list_union_map depends_of_tacexpr tacl acc + | TacTry tac -> depends_of_tacexpr tac acc + | TacOrelse (tac0, tac1) -> depends_of_tacexpr tac0 (depends_of_tacexpr tac1 acc) + | TacDo (_, tac) -> depends_of_tacexpr tac acc + | TacRepeat tac -> depends_of_tacexpr tac acc + | TacProgress tac -> depends_of_tacexpr tac acc + | TacAbstract (tac, _) -> depends_of_tacexpr tac acc + | TacId _ + | TacFail _ -> acc + | TacInfo tac -> depends_of_tacexpr tac acc + | TacLetIn (_, igtal, tac) -> + depends_of_tacexpr + tac + (list_union_map + (fun x y -> depends_of_tac_arg (snd x) y) + igtal + acc) + | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet" + | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet" + | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc + | TacArg tacarg -> depends_of_tac_arg tacarg acc + and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with + (* Basic tactics *) + | TacIntroPattern _ + | TacIntrosUntil _ + | TacIntroMove _ + | TacAssumption -> acc + | TacExact c + | TacExactNoCheck c + | TacVmCastNoCheck c -> depends_of_'constr c acc + | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc + | TacElim (_, cwb, cwbo) -> + depends_of_'constr_with_bindings cwb + (Option.fold_right depends_of_'constr_with_bindings cwbo acc) + | TacElimType c -> depends_of_'constr c acc + | TacCase (_, cb) -> depends_of_'constr_with_bindings cb acc + | TacCaseType c -> depends_of_'constr c acc + | TacFix _ + | TacMutualFix _ + | TacCofix _ + | TacMutualCofix _ -> failwith "depends_of_atomic_tacexpr of a Tac(Mutual)(Co)Fix not implemented yet" + | TacCut c -> depends_of_'constr c acc + | TacAssert (taco, _, c) -> + Option.fold_right depends_of_'tac taco (depends_of_'constr c acc) + | TacGeneralize cl -> + list_union_map depends_of_'constr (List.map (fun ((_,c),_) -> c) cl) + acc + | TacGeneralizeDep c -> depends_of_'constr c acc + | TacLetTac (_,c,_,_) -> depends_of_'constr c acc + + (* Derived basic tactics *) + | TacSimpleInduction _ + | TacSimpleDestruct _ + | TacDoubleInduction _ -> acc + | TacNewInduction (_, cwbial, cwbo, _, _) + | TacNewDestruct (_, cwbial, cwbo, _, _) -> + list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings) + cwbial + (Option.fold_right depends_of_'constr_with_bindings cwbo acc) + | TacDecomposeAnd c + | TacDecomposeOr c -> depends_of_'constr c acc + | TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc) + | TacSpecialize (_,cwb) -> depends_of_'constr_with_bindings cwb acc + | TacLApply c -> depends_of_'constr c acc + + (* Automation tactics *) + | TacTrivial (cl, bs) -> + (* TODO: Maybe make use of bs: list of hint bases to be used. *) + list_union_map depends_of_'constr cl acc + | TacAuto (_, cs, bs) -> + (* TODO: Maybe make use of bs: list of hint bases to be used. + None -> all ("with *") + Some list -> a list, "core" added implicitly *) + list_union_map depends_of_'constr cs acc + | TacAutoTDB _ -> acc + | TacDestructHyp _ -> acc + | TacDestructConcl -> acc + | TacSuperAuto _ -> (* TODO: this reference thing is scary*) + acc + | TacDAuto _ -> acc + + (* Context management *) + | TacClear _ + | TacClearBody _ + | TacMove _ + | TacRename _ + | TacRevert _ -> acc + + (* Constructors *) + | TacLeft (_,cb) + | TacRight (_,cb) + | TacSplit (_, _, cb) + | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc + | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc + + (* Conversion *) + | TacReduce (reg,_) -> + depends_of_'a_'b_red_expr_gen depends_of_'constr reg acc + | TacChange (cwoo, c, _) -> + depends_of_'constr + c + (Option.fold_right (depends_of_'a_with_occurences depends_of_'constr) cwoo acc) + + (* Equivalence relations *) + | TacReflexivity + | TacSymmetry _ -> acc + | TacTransitivity c -> depends_of_'constr c acc + + (* Equality and inversion *) + | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc + | TacInversion (is, _) -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc + + (* For ML extensions *) + | TacExtend (_, _, cgal) -> failwith "depends of TacExtend not implemented because depends of a generic_argument not implemented" + + (* For syntax extensions *) + | TacAlias (_,_,gal,(_,gte)) -> failwith "depends of a TacAlias not implemented because depends of a generic_argument not implemented" + and depends_of_tac_fun_ast tfa acc = failwith "depend_of_tac_fun_ast not implemented yet" + and depends_of_tac_arg ta acc = match ta with + | TacDynamic (_,d) -> failwith "Don't know what to do with a Dyn in tac_arg" + | TacVoid -> acc + | MetaIdArg _ -> failwith "Don't know what to do with a MetaIdArg in tac_arg" + | ConstrMayEval me -> failwith "TODO: depends_of_tac_arg of a ConstrMayEval" + | IntroPattern _ -> acc + | Reference ltc -> acc (* TODO: This assumes the "ltac constant" cannot somehow refer to a named object... *) + | Integer _ -> acc + | TacCall (_,ltc,l) -> (* TODO: This assumes the "ltac constant" cannot somehow refer to a named object... *) + list_union_map depends_of_tac_arg l acc + | TacExternal (_,_,_,l) -> list_union_map depends_of_tac_arg l acc + | TacFreshId _ -> acc + | Tacexp tac -> + depends_of_'tac tac acc + in + depends_of_tacexpr + +let rec depends_of_glob_tactic_expr (gte:glob_tactic_expr) acc = + depends_of_gen_tactic_expr + depends_of_rawconstr_and_expr + (depends_of_'a_or_var depends_of_inductive) + depends_of_glob_tactic_expr + gte + acc + +let rec depends_of_tacexpr te acc = + depends_of_gen_tactic_expr + depends_of_open_constr + depends_of_inductive + depends_of_glob_tactic_expr + te + acc + +let depends_of_compound_rule cr acc = match cr with + | Tactic (texp, _) -> depends_of_tacexpr texp acc + | Proof_instr (b, instr) -> + (* TODO: What is the boolean b? Should check. *) + failwith "Dependency calculation of Proof_instr not implemented yet" +and depends_of_prim_rule pr acc = match pr with + | Refine c -> depends_of_constr c acc + | Intro id -> acc + | Intro_replacing id -> acc + | Cut (_, _, t) -> depends_of_constr t acc (* TODO: check what 2nd argument contains *) + | FixRule (_, _, l) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *) + | Cofix (_, l) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *) + | Convert_concl (t, _) -> depends_of_constr t acc + | Convert_hyp (_, None, t) -> depends_of_constr t acc + | Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc) + | Thin _ -> acc + | ThinBody _ -> acc + | Move _ -> acc + | Rename _ -> acc + | Change_evars -> acc + +let rec depends_of_pftree pt acc = + match pt.ref with + | None -> acc + | Some (Prim pr , l) -> depends_of_prim_rule pr (list_union_map depends_of_pftree l acc) + | Some (Nested (t, p), l) -> depends_of_compound_rule t (depends_of_pftree p (list_union_map depends_of_pftree l acc)) + | Some (Decl_proof _ , l) -> list_union_map depends_of_pftree l acc + | Some (Daimon, l) -> list_union_map depends_of_pftree l acc + +let rec depends_of_pftree_head pt acc = + match pt.ref with + | None -> acc + | Some (Prim pr , l) -> depends_of_prim_rule pr acc + | Some (Nested (t, p), l) -> depends_of_compound_rule t (depends_of_pftree p acc) + | Some (Decl_proof _ , l) -> acc + | Some (Daimon, l) -> acc + +let depends_of_pftreestate depends_of_pftree pfs = +(* print_string "depends_of_pftreestate called\n"; *) +(* explore_tree pfs; *) + let pt = proof_of_pftreestate pfs in + assert (is_top_pftreestate pfs); + assert (pt.open_subgoals = 0); + depends_of_pftree pt [] + +let depends_of_definition_entry de ~acc = + Option.fold_right + depends_of_constr + de.const_entry_type + (depends_of_constr de.const_entry_body acc) diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 9a503cfb..6b17e739 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -28,7 +28,7 @@ let convert_env = let convert_binder env (na, b, c) = match b with | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b) - | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in + | None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in let rec cvrec env = function [] -> [] | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in @@ -134,14 +134,14 @@ let implicits_to_ast_list implicits = let make_variable_ast name typ implicits = (VernacAssumption - ((Local,Definitional), - [false,([dummy_loc,name], constr_to_ast (body_of_type typ))])) + ((Local,Definitional),false,(*inline flag*) + [false,([dummy_loc,name], constr_to_ast typ)])) ::(implicits_to_ast_list implicits);; let make_definition_ast name c typ implicits = - VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None, - (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), + VernacDefinition ((Global,false,Definition), (dummy_loc,name), + DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)), (fun _ _ -> ())) ::(implicits_to_ast_list implicits);; @@ -158,7 +158,7 @@ let constant_to_ast_list kn = make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = - let (id, c, v) = get_variable sp in + let (id, c, v) = Global.lookup_named sp in let l = implicits_of_global (VarRef sp) in (match c with None -> diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli index b8c2d7dc..f9e83b5e 100644 --- a/contrib/interface/name_to_ast.mli +++ b/contrib/interface/name_to_ast.mli @@ -1 +1,5 @@ val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;; +val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;; +val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;; +val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;; +val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 8cca7614..bf8614b4 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -21,18 +21,19 @@ type parsed_tree = | P_i of ct_INT;; let print_parse_results n msg = - print_string "message\nparsed\n"; - print_int n; - print_string "\n"; - (match msg with - | P_cl x -> fCOMMAND_LIST x - | P_c x -> fCOMMAND x - | P_t x -> fTACTIC_COM x - | P_f x -> fFORMULA x - | P_id x -> fID x - | P_s x -> fSTRING x - | P_i x -> fINT x); - print_string "e\nblabla\n"; + Pp.msg + ( str "message\nparsed\n" ++ + int n ++ + str "\n" ++ + (match msg with + | P_cl x -> fCOMMAND_LIST x + | P_c x -> fCOMMAND x + | P_t x -> fTACTIC_COM x + | P_f x -> fFORMULA x + | P_id x -> fID x + | P_s x -> fSTRING x + | P_i x -> fINT x) ++ + str "e\nblabla\n"); flush stdout;; let ctf_SyntaxErrorMessage reqid pps = @@ -329,7 +330,7 @@ let add_path_action reqid string_arg = let print_version_action () = msgnl (mt ()); - msgnl (str "$Id: parse.ml 9397 2006-11-21 21:50:54Z herbelin $");; + msgnl (str "$Id: parse.ml 9476 2007-01-10 15:44:44Z lmamane $");; let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index d2f71bfc..06b957d9 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -156,29 +156,29 @@ let make_pbp_pattern x = let rec make_then = function | [] -> TacId [] | [t] -> t - | t1::t2::l -> make_then (TacThen (t1,t2)::l) + | t1::t2::l -> make_then (TacThen (t1,[||],t2,[||])::l) let make_pbp_atomic_tactic = function | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption)) | PbpTryAssumption (Some a) -> TacTry (TacAtom (zz, TacExact (make_var a))) | PbpExists x -> - TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x])) + TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in - TacAtom (zz, TacGeneralize [make_app (make_var h) l]) - | PbpLeft -> TacAtom (zz, TacLeft NoBindings) - | PbpRight -> TacAtom (zz, TacRight NoBindings) + TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous]) + | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) + | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) | PbpLApply h -> TacAtom (zz, TacLApply (make_var h)) - | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings)) + | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings))) | PbpElim (hyp_name, names) -> let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in TacAtom - (zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None)) + (zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l))) - | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));; + | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));; let rec make_pbp_tactic = function | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 4bec7350..953fb5e7 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -166,7 +166,7 @@ let rule_to_ntactic r = let rt = (match r with Nested(Tactic (t,_),_) -> t - | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h) + | Prim (Refine h) -> TacAtom (dummy_loc,TacExact (Tactics.inj_open h)) | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in if rule_is_complex r then (match rt with @@ -1183,8 +1183,8 @@ let rec natural_ntree ig ntree = TacIntroPattern _ -> natural_intros ig lh g gs ltree | TacIntroMove _ -> natural_intros ig lh g gs ltree | TacFix (_,n) -> natural_fix ig lh g gs n ltree - | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree - | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge l ltree + | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree + | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree | TacRight _ -> natural_right ig lh g gs ltree | TacLeft _ -> natural_left ig lh g gs ltree @@ -1202,17 +1202,18 @@ let rec natural_ntree ig ntree = | TacExtend (_,"InductionIntro",[a]) -> let id=(out_gen wit_ident a) in natural_induction ig lh g gs ge id ltree true - | TacApply (c,_) -> natural_apply ig lh g gs c ltree - | TacExact c -> natural_exact ig lh g gs c ltree - | TacCut c -> natural_cut ig lh g gs c ltree + | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree + | TacExact c -> natural_exact ig lh g gs (snd c) ltree + | TacCut c -> natural_cut ig lh g gs (snd c) ltree | TacExtend (_,"CutIntro",[a]) -> let _c = out_gen wit_constr a in natural_cutintro ig lh g gs a ltree - | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false + | TacCase (_,(c,_)) -> natural_case ig lh g gs ge (snd c) ltree false | TacExtend (_,"CaseIntro",[a]) -> let c = out_gen wit_constr a in natural_case ig lh g gs ge c ltree true - | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false + | TacElim (_,(c,_),_) -> + natural_elim ig lh g gs ge (snd c) ltree false | TacExtend (_,"ElimIntro",[a]) -> let c = out_gen wit_constr a in natural_elim ig lh g gs ge c ltree true @@ -1611,7 +1612,7 @@ and natural_fix ig lh g gs narg ltree = | _ -> assert false and natural_reduce ig lh g gs ge mode la ltree = match la with - {onhyps=Some[];onconcl=true} -> + {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); @@ -1619,7 +1620,7 @@ and natural_reduce ig lh g gs ge mode la ltree = {ihsg=All_subgoals_hyp;isgintro="simpl"}) ltree) ] - | {onhyps=Some[hyp]; onconcl=false} -> + | {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); @@ -1651,7 +1652,7 @@ and natural_split ig lh g gs ge la ltree = | _ -> assert false and natural_generalize ig lh g gs ge la ltree = match la with - [arg] -> + [(_,(_,arg)),_] -> let _env= (gLOB ge) in let arg1= (*dbize env*) arg in let _type_arg=type_of (Global.env()) Evd.empty arg in diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml index 6e4782be..559860b2 100644 --- a/contrib/interface/translate.ml +++ b/contrib/interface/translate.ml @@ -75,3 +75,6 @@ let translate_path l = (*translates a path and a goal into a centaur-tree --> RULE *) let translate_goal (g:goal) = CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);; + +let translate_goals (gl: goal list) = + CT_rule_list (List.map translate_goal gl);; diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli index 65d8331b..34841fc4 100644 --- a/contrib/interface/translate.mli +++ b/contrib/interface/translate.mli @@ -5,6 +5,7 @@ open Environ;; open Term;; val translate_goal : goal -> ct_RULE;; +val translate_goals : goal list -> ct_RULE_LIST;; (* The boolean argument indicates whether names from the environment should *) (* be avoided (same interpretation as for prterm_env and ast_of_constr) *) val translate_constr : bool -> env -> constr -> ct_FORMULA;; diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 166a0cbf..551ad3a3 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1,103 +1,108 @@ open Ascent;; +open Pp;; + +(* LEM: This is actually generated automatically *) let fNODE s n = - print_string "n\n"; - print_string ("vernac$" ^ s); - print_string "\n"; - print_int n; - print_string "\n";; + (str "n\n") ++ + (str ("vernac$" ^ s)) ++ + (str "\n") ++ + (int n) ++ + (str "\n");; let fATOM s1 = - print_string "a\n"; - print_string ("vernac$" ^ s1); - print_string "\n";; + (str "a\n") ++ + (str ("vernac$" ^ s1)) ++ + (str "\n");; -let f_atom_string = print_string;; -let f_atom_int = print_int;; +let f_atom_string = str;; +let f_atom_int = int;; let rec fAST = function | CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x | CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x | CT_coerce_SINGLE_OPTION_VALUE_to_AST x -> fSINGLE_OPTION_VALUE x | CT_astnode(x1, x2) -> - fID x1; - fAST_LIST x2; + fID x1 ++ + fAST_LIST x2 ++ fNODE "astnode" 2 | CT_astpath(x1) -> - fID_LIST x1; + fID_LIST x1 ++ fNODE "astpath" 1 | CT_astslam(x1, x2) -> - fID_OPT x1; - fAST x2; + fID_OPT x1 ++ + fAST x2 ++ fNODE "astslam" 2 and fAST_LIST = function | CT_ast_list l -> - (List.iter fAST l); + (List.fold_left (++) (mt()) (List.map fAST l)) ++ fNODE "ast_list" (List.length l) and fBINARY = function -| CT_binary x -> fATOM "binary"; - (f_atom_int x); - print_string "\n"and fBINDER = function +| CT_binary x -> fATOM "binary" ++ + (f_atom_int x) ++ + str "\n" +and fBINDER = function | CT_coerce_DEF_to_BINDER x -> fDEF x | CT_binder(x1, x2) -> - fID_OPT_NE_LIST x1; - fFORMULA x2; + fID_OPT_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "binder" 2 | CT_binder_coercion(x1, x2) -> - fID_OPT_NE_LIST x1; - fFORMULA x2; + fID_OPT_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "binder_coercion" 2 and fBINDER_LIST = function | CT_binder_list l -> - (List.iter fBINDER l); + (List.fold_left (++) (mt()) (List.map fBINDER l)) ++ fNODE "binder_list" (List.length l) and fBINDER_NE_LIST = function | CT_binder_ne_list(x,l) -> - fBINDER x; - (List.iter fBINDER l); + fBINDER x ++ + (List.fold_left (++) (mt()) (List.map fBINDER l)) ++ fNODE "binder_ne_list" (1 + (List.length l)) and fBINDING = function | CT_binding(x1, x2) -> - fID_OR_INT x1; - fFORMULA x2; + fID_OR_INT x1 ++ + fFORMULA x2 ++ fNODE "binding" 2 and fBINDING_LIST = function | CT_binding_list l -> - (List.iter fBINDING l); + (List.fold_left (++) (mt()) (List.map fBINDING l)) ++ fNODE "binding_list" (List.length l) and fBOOL = function | CT_false -> fNODE "false" 0 | CT_true -> fNODE "true" 0 and fCASE = function -| CT_case x -> fATOM "case"; - (f_atom_string x); - print_string "\n"and fCLAUSE = function +| CT_case x -> fATOM "case" ++ + (f_atom_string x) ++ + str "\n" +and fCLAUSE = function | CT_clause(x1, x2) -> - fHYP_LOCATION_LIST_OR_STAR x1; - fSTAR_OPT x2; + fHYP_LOCATION_LIST_OR_STAR x1 ++ + fSTAR_OPT x2 ++ fNODE "clause" 2 and fCOERCION_OPT = function | CT_coerce_NONE_to_COERCION_OPT x -> fNONE x | CT_coercion_atm -> fNODE "coercion_atm" 0 and fCOFIXTAC = function | CT_cofixtac(x1, x2) -> - fID x1; - fFORMULA x2; + fID x1 ++ + fFORMULA x2 ++ fNODE "cofixtac" 2 and fCOFIX_REC = function | CT_cofix_rec(x1, x2, x3, x4) -> - fID x1; - fBINDER_LIST x2; - fFORMULA x3; - fFORMULA x4; + fID x1 ++ + fBINDER_LIST x2 ++ + fFORMULA x3 ++ + fFORMULA x4 ++ fNODE "cofix_rec" 4 and fCOFIX_REC_LIST = function | CT_cofix_rec_list(x,l) -> - fCOFIX_REC x; - (List.iter fCOFIX_REC l); + fCOFIX_REC x ++ + (List.fold_left (++) (mt()) (List.map fCOFIX_REC l)) ++ fNODE "cofix_rec_list" (1 + (List.length l)) and fCOFIX_TAC_LIST = function | CT_cofix_tac_list l -> - (List.iter fCOFIXTAC l); + (List.fold_left (++) (mt()) (List.map fCOFIXTAC l)) ++ fNODE "cofix_tac_list" (List.length l) and fCOMMAND = function | CT_coerce_COMMAND_LIST_to_COMMAND x -> fCOMMAND_LIST x @@ -105,479 +110,476 @@ and fCOMMAND = function | CT_coerce_SECTION_BEGIN_to_COMMAND x -> fSECTION_BEGIN x | CT_coerce_THEOREM_GOAL_to_COMMAND x -> fTHEOREM_GOAL x | CT_abort(x1) -> - fID_OPT_OR_ALL x1; + fID_OPT_OR_ALL x1 ++ fNODE "abort" 1 | CT_abstraction(x1, x2, x3) -> - fID x1; - fFORMULA x2; - fINT_LIST x3; + fID x1 ++ + fFORMULA x2 ++ + fINT_LIST x3 ++ fNODE "abstraction" 3 | CT_add_field(x1, x2, x3, x4) -> - fFORMULA x1; - fFORMULA x2; - fFORMULA x3; - fFORMULA_OPT x4; + fFORMULA x1 ++ + fFORMULA x2 ++ + fFORMULA x3 ++ + fFORMULA_OPT x4 ++ fNODE "add_field" 4 | CT_add_natural_feature(x1, x2) -> - fNATURAL_FEATURE x1; - fID x2; + fNATURAL_FEATURE x1 ++ + fID x2 ++ fNODE "add_natural_feature" 2 | CT_addpath(x1, x2) -> - fSTRING x1; - fID_OPT x2; + fSTRING x1 ++ + fID_OPT x2 ++ fNODE "addpath" 2 | CT_arguments_scope(x1, x2) -> - fID x1; - fID_OPT_LIST x2; + fID x1 ++ + fID_OPT_LIST x2 ++ fNODE "arguments_scope" 2 | CT_bind_scope(x1, x2) -> - fID x1; - fID_NE_LIST x2; + fID x1 ++ + fID_NE_LIST x2 ++ fNODE "bind_scope" 2 | CT_cd(x1) -> - fSTRING_OPT x1; + fSTRING_OPT x1 ++ fNODE "cd" 1 | CT_check(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "check" 1 | CT_class(x1) -> - fID x1; + fID x1 ++ fNODE "class" 1 | CT_close_scope(x1) -> - fID x1; + fID x1 ++ fNODE "close_scope" 1 | CT_coercion(x1, x2, x3, x4, x5) -> - fLOCAL_OPT x1; - fIDENTITY_OPT x2; - fID x3; - fID x4; - fID x5; + fLOCAL_OPT x1 ++ + fIDENTITY_OPT x2 ++ + fID x3 ++ + fID x4 ++ + fID x5 ++ fNODE "coercion" 5 | CT_cofix_decl(x1) -> - fCOFIX_REC_LIST x1; + fCOFIX_REC_LIST x1 ++ fNODE "cofix_decl" 1 | CT_compile_module(x1, x2, x3) -> - fVERBOSE_OPT x1; - fID x2; - fSTRING_OPT x3; + fVERBOSE_OPT x1 ++ + fID x2 ++ + fSTRING_OPT x3 ++ fNODE "compile_module" 3 | CT_declare_module(x1, x2, x3, x4) -> - fID x1; - fMODULE_BINDER_LIST x2; - fMODULE_TYPE_CHECK x3; - fMODULE_EXPR x4; + fID x1 ++ + fMODULE_BINDER_LIST x2 ++ + fMODULE_TYPE_CHECK x3 ++ + fMODULE_EXPR x4 ++ fNODE "declare_module" 4 | CT_define_notation(x1, x2, x3, x4) -> - fSTRING x1; - fFORMULA x2; - fMODIFIER_LIST x3; - fID_OPT x4; + fSTRING x1 ++ + fFORMULA x2 ++ + fMODIFIER_LIST x3 ++ + fID_OPT x4 ++ fNODE "define_notation" 4 | CT_definition(x1, x2, x3, x4, x5) -> - fDEFN x1; - fID x2; - fBINDER_LIST x3; - fDEF_BODY x4; - fFORMULA_OPT x5; + fDEFN x1 ++ + fID x2 ++ + fBINDER_LIST x3 ++ + fDEF_BODY x4 ++ + fFORMULA_OPT x5 ++ fNODE "definition" 5 | CT_delim_scope(x1, x2) -> - fID x1; - fID x2; + fID x1 ++ + fID x2 ++ fNODE "delim_scope" 2 | CT_delpath(x1) -> - fSTRING x1; + fSTRING x1 ++ fNODE "delpath" 1 | CT_derive_depinversion(x1, x2, x3, x4) -> - fINV_TYPE x1; - fID x2; - fFORMULA x3; - fSORT_TYPE x4; + fINV_TYPE x1 ++ + fID x2 ++ + fFORMULA x3 ++ + fSORT_TYPE x4 ++ fNODE "derive_depinversion" 4 | CT_derive_inversion(x1, x2, x3, x4) -> - fINV_TYPE x1; - fINT_OPT x2; - fID x3; - fID x4; + fINV_TYPE x1 ++ + fINT_OPT x2 ++ + fID x3 ++ + fID x4 ++ fNODE "derive_inversion" 4 | CT_derive_inversion_with(x1, x2, x3, x4) -> - fINV_TYPE x1; - fID x2; - fFORMULA x3; - fSORT_TYPE x4; + fINV_TYPE x1 ++ + fID x2 ++ + fFORMULA x3 ++ + fSORT_TYPE x4 ++ fNODE "derive_inversion_with" 4 | CT_explain_proof(x1) -> - fINT_LIST x1; + fINT_LIST x1 ++ fNODE "explain_proof" 1 | CT_explain_prooftree(x1) -> - fINT_LIST x1; + fINT_LIST x1 ++ fNODE "explain_prooftree" 1 | CT_export_id(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "export_id" 1 | CT_extract_to_file(x1, x2) -> - fSTRING x1; - fID_NE_LIST x2; + fSTRING x1 ++ + fID_NE_LIST x2 ++ fNODE "extract_to_file" 2 | CT_extraction(x1) -> - fID_OPT x1; + fID_OPT x1 ++ fNODE "extraction" 1 | CT_fix_decl(x1) -> - fFIX_REC_LIST x1; + fFIX_REC_LIST x1 ++ fNODE "fix_decl" 1 | CT_focus(x1) -> - fINT_OPT x1; + fINT_OPT x1 ++ fNODE "focus" 1 | CT_go(x1) -> - fINT_OR_LOCN x1; + fINT_OR_LOCN x1 ++ fNODE "go" 1 | CT_guarded -> fNODE "guarded" 0 | CT_hint_destruct(x1, x2, x3, x4, x5, x6) -> - fID x1; - fINT x2; - fDESTRUCT_LOCATION x3; - fFORMULA x4; - fTACTIC_COM x5; - fID_LIST x6; + fID x1 ++ + fINT x2 ++ + fDESTRUCT_LOCATION x3 ++ + fFORMULA x4 ++ + fTACTIC_COM x5 ++ + fID_LIST x6 ++ fNODE "hint_destruct" 6 | CT_hint_extern(x1, x2, x3, x4) -> - fINT x1; - fFORMULA x2; - fTACTIC_COM x3; - fID_LIST x4; + fINT x1 ++ + fFORMULA x2 ++ + fTACTIC_COM x3 ++ + fID_LIST x4 ++ fNODE "hint_extern" 4 | CT_hintrewrite(x1, x2, x3, x4) -> - fORIENTATION x1; - fFORMULA_NE_LIST x2; - fID x3; - fTACTIC_COM x4; + fORIENTATION x1 ++ + fFORMULA_NE_LIST x2 ++ + fID x3 ++ + fTACTIC_COM x4 ++ fNODE "hintrewrite" 4 | CT_hints(x1, x2, x3) -> - fID x1; - fID_NE_LIST x2; - fID_LIST x3; + fID x1 ++ + fID_NE_LIST x2 ++ + fID_LIST x3 ++ fNODE "hints" 3 | CT_hints_immediate(x1, x2) -> - fFORMULA_NE_LIST x1; - fID_LIST x2; + fFORMULA_NE_LIST x1 ++ + fID_LIST x2 ++ fNODE "hints_immediate" 2 | CT_hints_resolve(x1, x2) -> - fFORMULA_NE_LIST x1; - fID_LIST x2; + fFORMULA_NE_LIST x1 ++ + fID_LIST x2 ++ fNODE "hints_resolve" 2 | CT_hyp_search_pattern(x1, x2) -> - fFORMULA x1; - fIN_OR_OUT_MODULES x2; + fFORMULA x1 ++ + fIN_OR_OUT_MODULES x2 ++ fNODE "hyp_search_pattern" 2 | CT_implicits(x1, x2) -> - fID x1; - fID_LIST_OPT x2; + fID x1 ++ + fID_LIST_OPT x2 ++ fNODE "implicits" 2 | CT_import_id(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "import_id" 1 | CT_ind_scheme(x1) -> - fSCHEME_SPEC_LIST x1; + fSCHEME_SPEC_LIST x1 ++ fNODE "ind_scheme" 1 | CT_infix(x1, x2, x3, x4) -> - fSTRING x1; - fID x2; - fMODIFIER_LIST x3; - fID_OPT x4; + fSTRING x1 ++ + fID x2 ++ + fMODIFIER_LIST x3 ++ + fID_OPT x4 ++ fNODE "infix" 4 | CT_inline(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "inline" 1 | CT_inspect(x1) -> - fINT x1; + fINT x1 ++ fNODE "inspect" 1 | CT_kill_node(x1) -> - fINT x1; + fINT x1 ++ fNODE "kill_node" 1 | CT_load(x1, x2) -> - fVERBOSE_OPT x1; - fID_OR_STRING x2; + fVERBOSE_OPT x1 ++ + fID_OR_STRING x2 ++ fNODE "load" 2 | CT_local_close_scope(x1) -> - fID x1; + fID x1 ++ fNODE "local_close_scope" 1 | CT_local_define_notation(x1, x2, x3, x4) -> - fSTRING x1; - fFORMULA x2; - fMODIFIER_LIST x3; - fID_OPT x4; + fSTRING x1 ++ + fFORMULA x2 ++ + fMODIFIER_LIST x3 ++ + fID_OPT x4 ++ fNODE "local_define_notation" 4 | CT_local_hint_destruct(x1, x2, x3, x4, x5, x6) -> - fID x1; - fINT x2; - fDESTRUCT_LOCATION x3; - fFORMULA x4; - fTACTIC_COM x5; - fID_LIST x6; + fID x1 ++ + fINT x2 ++ + fDESTRUCT_LOCATION x3 ++ + fFORMULA x4 ++ + fTACTIC_COM x5 ++ + fID_LIST x6 ++ fNODE "local_hint_destruct" 6 | CT_local_hint_extern(x1, x2, x3, x4) -> - fINT x1; - fFORMULA x2; - fTACTIC_COM x3; - fID_LIST x4; + fINT x1 ++ + fFORMULA x2 ++ + fTACTIC_COM x3 ++ + fID_LIST x4 ++ fNODE "local_hint_extern" 4 | CT_local_hints(x1, x2, x3) -> - fID x1; - fID_NE_LIST x2; - fID_LIST x3; + fID x1 ++ + fID_NE_LIST x2 ++ + fID_LIST x3 ++ fNODE "local_hints" 3 | CT_local_hints_immediate(x1, x2) -> - fFORMULA_NE_LIST x1; - fID_LIST x2; + fFORMULA_NE_LIST x1 ++ + fID_LIST x2 ++ fNODE "local_hints_immediate" 2 | CT_local_hints_resolve(x1, x2) -> - fFORMULA_NE_LIST x1; - fID_LIST x2; + fFORMULA_NE_LIST x1 ++ + fID_LIST x2 ++ fNODE "local_hints_resolve" 2 | CT_local_infix(x1, x2, x3, x4) -> - fSTRING x1; - fID x2; - fMODIFIER_LIST x3; - fID_OPT x4; + fSTRING x1 ++ + fID x2 ++ + fMODIFIER_LIST x3 ++ + fID_OPT x4 ++ fNODE "local_infix" 4 | CT_local_open_scope(x1) -> - fID x1; + fID x1 ++ fNODE "local_open_scope" 1 | CT_local_reserve_notation(x1, x2) -> - fSTRING x1; - fMODIFIER_LIST x2; + fSTRING x1 ++ + fMODIFIER_LIST x2 ++ fNODE "local_reserve_notation" 2 | CT_locate(x1) -> - fID x1; + fID x1 ++ fNODE "locate" 1 | CT_locate_file(x1) -> - fSTRING x1; + fSTRING x1 ++ fNODE "locate_file" 1 | CT_locate_lib(x1) -> - fID x1; + fID x1 ++ fNODE "locate_lib" 1 | CT_locate_notation(x1) -> - fSTRING x1; + fSTRING x1 ++ fNODE "locate_notation" 1 | CT_mind_decl(x1, x2) -> - fCO_IND x1; - fIND_SPEC_LIST x2; + fCO_IND x1 ++ + fIND_SPEC_LIST x2 ++ fNODE "mind_decl" 2 | CT_ml_add_path(x1) -> - fSTRING x1; + fSTRING x1 ++ fNODE "ml_add_path" 1 | CT_ml_declare_modules(x1) -> - fSTRING_NE_LIST x1; + fSTRING_NE_LIST x1 ++ fNODE "ml_declare_modules" 1 | CT_ml_print_modules -> fNODE "ml_print_modules" 0 | CT_ml_print_path -> fNODE "ml_print_path" 0 | CT_module(x1, x2, x3, x4) -> - fID x1; - fMODULE_BINDER_LIST x2; - fMODULE_TYPE_CHECK x3; - fMODULE_EXPR x4; + fID x1 ++ + fMODULE_BINDER_LIST x2 ++ + fMODULE_TYPE_CHECK x3 ++ + fMODULE_EXPR x4 ++ fNODE "module" 4 | CT_module_type_decl(x1, x2, x3) -> - fID x1; - fMODULE_BINDER_LIST x2; - fMODULE_TYPE_OPT x3; + fID x1 ++ + fMODULE_BINDER_LIST x2 ++ + fMODULE_TYPE_OPT x3 ++ fNODE "module_type_decl" 3 | CT_no_inline(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "no_inline" 1 | CT_omega_flag(x1, x2) -> - fOMEGA_MODE x1; - fOMEGA_FEATURE x2; + fOMEGA_MODE x1 ++ + fOMEGA_FEATURE x2 ++ fNODE "omega_flag" 2 -| CT_opaque(x1) -> - fID_NE_LIST x1; - fNODE "opaque" 1 | CT_open_scope(x1) -> - fID x1; + fID x1 ++ fNODE "open_scope" 1 | CT_print -> fNODE "print" 0 | CT_print_about(x1) -> - fID x1; + fID x1 ++ fNODE "print_about" 1 | CT_print_all -> fNODE "print_all" 0 | CT_print_classes -> fNODE "print_classes" 0 | CT_print_ltac id -> - fID id; + fID id ++ fNODE "print_ltac" 1 | CT_print_coercions -> fNODE "print_coercions" 0 | CT_print_grammar(x1) -> - fGRAMMAR x1; + fGRAMMAR x1 ++ fNODE "print_grammar" 1 | CT_print_graph -> fNODE "print_graph" 0 | CT_print_hint(x1) -> - fID_OPT x1; + fID_OPT x1 ++ fNODE "print_hint" 1 | CT_print_hintdb(x1) -> - fID_OR_STAR x1; + fID_OR_STAR x1 ++ fNODE "print_hintdb" 1 | CT_print_rewrite_hintdb(x1) -> - fID x1; + fID x1 ++ fNODE "print_rewrite_hintdb" 1 | CT_print_id(x1) -> - fID x1; + fID x1 ++ fNODE "print_id" 1 | CT_print_implicit(x1) -> - fID x1; + fID x1 ++ fNODE "print_implicit" 1 | CT_print_loadpath -> fNODE "print_loadpath" 0 | CT_print_module(x1) -> - fID x1; + fID x1 ++ fNODE "print_module" 1 | CT_print_module_type(x1) -> - fID x1; + fID x1 ++ fNODE "print_module_type" 1 | CT_print_modules -> fNODE "print_modules" 0 | CT_print_natural(x1) -> - fID x1; + fID x1 ++ fNODE "print_natural" 1 | CT_print_natural_feature(x1) -> - fNATURAL_FEATURE x1; + fNATURAL_FEATURE x1 ++ fNODE "print_natural_feature" 1 | CT_print_opaqueid(x1) -> - fID x1; + fID x1 ++ fNODE "print_opaqueid" 1 | CT_print_path(x1, x2) -> - fID x1; - fID x2; + fID x1 ++ + fID x2 ++ fNODE "print_path" 2 | CT_print_proof(x1) -> - fID x1; + fID x1 ++ fNODE "print_proof" 1 | CT_print_scope(x1) -> - fID x1; + fID x1 ++ fNODE "print_scope" 1 | CT_print_setoids -> fNODE "print_setoids" 0 | CT_print_scopes -> fNODE "print_scopes" 0 | CT_print_section(x1) -> - fID x1; + fID x1 ++ fNODE "print_section" 1 | CT_print_states -> fNODE "print_states" 0 | CT_print_tables -> fNODE "print_tables" 0 | CT_print_universes(x1) -> - fSTRING_OPT x1; + fSTRING_OPT x1 ++ fNODE "print_universes" 1 | CT_print_visibility(x1) -> - fID_OPT x1; + fID_OPT x1 ++ fNODE "print_visibility" 1 | CT_proof(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "proof" 1 | CT_proof_no_op -> fNODE "proof_no_op" 0 | CT_proof_with(x1) -> - fTACTIC_COM x1; + fTACTIC_COM x1 ++ fNODE "proof_with" 1 | CT_pwd -> fNODE "pwd" 0 | CT_quit -> fNODE "quit" 0 | CT_read_module(x1) -> - fID x1; + fID x1 ++ fNODE "read_module" 1 | CT_rec_ml_add_path(x1) -> - fSTRING x1; + fSTRING x1 ++ fNODE "rec_ml_add_path" 1 | CT_recaddpath(x1, x2) -> - fSTRING x1; - fID_OPT x2; + fSTRING x1 ++ + fID_OPT x2 ++ fNODE "recaddpath" 2 | CT_record(x1, x2, x3, x4, x5, x6) -> - fCOERCION_OPT x1; - fID x2; - fBINDER_LIST x3; - fFORMULA x4; - fID_OPT x5; - fRECCONSTR_LIST x6; + fCOERCION_OPT x1 ++ + fID x2 ++ + fBINDER_LIST x3 ++ + fFORMULA x4 ++ + fID_OPT x5 ++ + fRECCONSTR_LIST x6 ++ fNODE "record" 6 | CT_remove_natural_feature(x1, x2) -> - fNATURAL_FEATURE x1; - fID x2; + fNATURAL_FEATURE x1 ++ + fID x2 ++ fNODE "remove_natural_feature" 2 | CT_require(x1, x2, x3) -> - fIMPEXP x1; - fSPEC_OPT x2; - fID_NE_LIST_OR_STRING x3; + fIMPEXP x1 ++ + fSPEC_OPT x2 ++ + fID_NE_LIST_OR_STRING x3 ++ fNODE "require" 3 | CT_reserve(x1, x2) -> - fID_NE_LIST x1; - fFORMULA x2; + fID_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "reserve" 2 | CT_reserve_notation(x1, x2) -> - fSTRING x1; - fMODIFIER_LIST x2; + fSTRING x1 ++ + fMODIFIER_LIST x2 ++ fNODE "reserve_notation" 2 | CT_reset(x1) -> - fID x1; + fID x1 ++ fNODE "reset" 1 | CT_reset_section(x1) -> - fID x1; + fID x1 ++ fNODE "reset_section" 1 | CT_restart -> fNODE "restart" 0 | CT_restore_state(x1) -> - fID x1; + fID x1 ++ fNODE "restore_state" 1 | CT_resume(x1) -> - fID_OPT x1; + fID_OPT x1 ++ fNODE "resume" 1 | CT_save(x1, x2) -> - fTHM_OPT x1; - fID_OPT x2; + fTHM_OPT x1 ++ + fID_OPT x2 ++ fNODE "save" 2 | CT_scomments(x1) -> - fSCOMMENT_CONTENT_LIST x1; + fSCOMMENT_CONTENT_LIST x1 ++ fNODE "scomments" 1 | CT_search(x1, x2) -> - fID x1; - fIN_OR_OUT_MODULES x2; + fID x1 ++ + fIN_OR_OUT_MODULES x2 ++ fNODE "search" 2 | CT_search_about(x1, x2) -> - fID_OR_STRING_NE_LIST x1; - fIN_OR_OUT_MODULES x2; + fID_OR_STRING_NE_LIST x1 ++ + fIN_OR_OUT_MODULES x2 ++ fNODE "search_about" 2 | CT_search_pattern(x1, x2) -> - fFORMULA x1; - fIN_OR_OUT_MODULES x2; + fFORMULA x1 ++ + fIN_OR_OUT_MODULES x2 ++ fNODE "search_pattern" 2 | CT_search_rewrite(x1, x2) -> - fFORMULA x1; - fIN_OR_OUT_MODULES x2; + fFORMULA x1 ++ + fIN_OR_OUT_MODULES x2 ++ fNODE "search_rewrite" 2 | CT_section_end(x1) -> - fID x1; + fID x1 ++ fNODE "section_end" 1 | CT_section_struct(x1, x2, x3) -> - fSECTION_BEGIN x1; - fSECTION_BODY x2; - fCOMMAND x3; + fSECTION_BEGIN x1 ++ + fSECTION_BODY x2 ++ + fCOMMAND x3 ++ fNODE "section_struct" 3 | CT_set_natural(x1) -> - fID x1; + fID x1 ++ fNODE "set_natural" 1 | CT_set_natural_default -> fNODE "set_natural_default" 0 | CT_set_option(x1) -> - fTABLE x1; + fTABLE x1 ++ fNODE "set_option" 1 | CT_set_option_value(x1, x2) -> - fTABLE x1; - fSINGLE_OPTION_VALUE x2; + fTABLE x1 ++ + fSINGLE_OPTION_VALUE x2 ++ fNODE "set_option_value" 2 | CT_set_option_value2(x1, x2) -> - fTABLE x1; - fID_OR_STRING_NE_LIST x2; + fTABLE x1 ++ + fID_OR_STRING_NE_LIST x2 ++ fNODE "set_option_value2" 2 | CT_sethyp(x1) -> - fINT x1; + fINT x1 ++ fNODE "sethyp" 1 | CT_setundo(x1) -> - fINT x1; + fINT x1 ++ fNODE "setundo" 1 | CT_show_existentials -> fNODE "show_existentials" 0 | CT_show_goal(x1) -> - fINT_OPT x1; + fINT_OPT x1 ++ fNODE "show_goal" 1 | CT_show_implicit(x1) -> - fINT x1; + fINT x1 ++ fNODE "show_implicit" 1 | CT_show_intro -> fNODE "show_intro" 0 | CT_show_intros -> fNODE "show_intros" 0 @@ -587,97 +589,103 @@ and fCOMMAND = function | CT_show_script -> fNODE "show_script" 0 | CT_show_tree -> fNODE "show_tree" 0 | CT_solve(x1, x2, x3) -> - fINT x1; - fTACTIC_COM x2; - fDOTDOT_OPT x3; + fINT x1 ++ + fTACTIC_COM x2 ++ + fDOTDOT_OPT x3 ++ fNODE "solve" 3 +| CT_strategy(CT_level_list x1) -> + List.fold_left (++) (mt()) + (List.map (fun(l,q) -> fLEVEL l ++ fID_LIST q ++ fNODE "pair"2) x1) ++ + fNODE "strategy" (List.length x1) | CT_suspend -> fNODE "suspend" 0 | CT_syntax_macro(x1, x2, x3) -> - fID x1; - fFORMULA x2; - fINT_OPT x3; + fID x1 ++ + fFORMULA x2 ++ + fINT_OPT x3 ++ fNODE "syntax_macro" 3 | CT_tactic_definition(x1) -> - fTAC_DEF_NE_LIST x1; + fTAC_DEF_NE_LIST x1 ++ fNODE "tactic_definition" 1 | CT_test_natural_feature(x1, x2) -> - fNATURAL_FEATURE x1; - fID x2; + fNATURAL_FEATURE x1 ++ + fID x2 ++ fNODE "test_natural_feature" 2 | CT_theorem_struct(x1, x2) -> - fTHEOREM_GOAL x1; - fPROOF_SCRIPT x2; + fTHEOREM_GOAL x1 ++ + fPROOF_SCRIPT x2 ++ fNODE "theorem_struct" 2 | CT_time(x1) -> - fCOMMAND x1; + fCOMMAND x1 ++ fNODE "time" 1 -| CT_transparent(x1) -> - fID_NE_LIST x1; - fNODE "transparent" 1 | CT_undo(x1) -> - fINT_OPT x1; + fINT_OPT x1 ++ fNODE "undo" 1 | CT_unfocus -> fNODE "unfocus" 0 | CT_unset_option(x1) -> - fTABLE x1; + fTABLE x1 ++ fNODE "unset_option" 1 | CT_unsethyp -> fNODE "unsethyp" 0 | CT_unsetundo -> fNODE "unsetundo" 0 | CT_user_vernac(x1, x2) -> - fID x1; - fVARG_LIST x2; + fID x1 ++ + fVARG_LIST x2 ++ fNODE "user_vernac" 2 | CT_variable(x1, x2) -> - fVAR x1; - fBINDER_NE_LIST x2; + fVAR x1 ++ + fBINDER_NE_LIST x2 ++ fNODE "variable" 2 | CT_write_module(x1, x2) -> - fID x1; - fSTRING_OPT x2; + fID x1 ++ + fSTRING_OPT x2 ++ fNODE "write_module" 2 +and fLEVEL = function +| CT_Opaque -> fNODE "opaque" 0 +| CT_Level n -> fINT n ++ fNODE "level" 1 +| CT_Expand -> fNODE "expand" 0 and fCOMMAND_LIST = function | CT_command_list(x,l) -> - fCOMMAND x; - (List.iter fCOMMAND l); + fCOMMAND x ++ + (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++ fNODE "command_list" (1 + (List.length l)) and fCOMMENT = function -| CT_comment x -> fATOM "comment"; - (f_atom_string x); - print_string "\n"and fCOMMENT_S = function +| CT_comment x -> fATOM "comment" ++ + (f_atom_string x) ++ + str "\n" +and fCOMMENT_S = function | CT_comment_s l -> - (List.iter fCOMMENT l); + (List.fold_left (++) (mt()) (List.map fCOMMENT l)) ++ fNODE "comment_s" (List.length l) and fCONSTR = function | CT_constr(x1, x2) -> - fID x1; - fFORMULA x2; + fID x1 ++ + fFORMULA x2 ++ fNODE "constr" 2 | CT_constr_coercion(x1, x2) -> - fID x1; - fFORMULA x2; + fID x1 ++ + fFORMULA x2 ++ fNODE "constr_coercion" 2 and fCONSTR_LIST = function | CT_constr_list l -> - (List.iter fCONSTR l); + (List.fold_left (++) (mt()) (List.map fCONSTR l)) ++ fNODE "constr_list" (List.length l) and fCONTEXT_HYP_LIST = function | CT_context_hyp_list l -> - (List.iter fPREMISE_PATTERN l); + (List.fold_left (++) (mt()) (List.map fPREMISE_PATTERN l)) ++ fNODE "context_hyp_list" (List.length l) and fCONTEXT_PATTERN = function | CT_coerce_FORMULA_to_CONTEXT_PATTERN x -> fFORMULA x | CT_context(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "context" 2 and fCONTEXT_RULE = function | CT_context_rule(x1, x2, x3) -> - fCONTEXT_HYP_LIST x1; - fCONTEXT_PATTERN x2; - fTACTIC_COM x3; + fCONTEXT_HYP_LIST x1 ++ + fCONTEXT_PATTERN x2 ++ + fTACTIC_COM x3 ++ fNODE "context_rule" 3 | CT_def_context_rule(x1) -> - fTACTIC_COM x1; + fTACTIC_COM x1 ++ fNODE "def_context_rule" 1 and fCONVERSION_FLAG = function | CT_beta -> fNODE "beta" 0 @@ -687,49 +695,52 @@ and fCONVERSION_FLAG = function | CT_zeta -> fNODE "zeta" 0 and fCONVERSION_FLAG_LIST = function | CT_conversion_flag_list l -> - (List.iter fCONVERSION_FLAG l); + (List.fold_left (++) (mt()) (List.map fCONVERSION_FLAG l)) ++ fNODE "conversion_flag_list" (List.length l) and fCONV_SET = function | CT_unf l -> - (List.iter fID l); + (List.fold_left (++) (mt()) (List.map fID l)) ++ fNODE "unf" (List.length l) | CT_unfbut l -> - (List.iter fID l); + (List.fold_left (++) (mt()) (List.map fID l)) ++ fNODE "unfbut" (List.length l) and fCO_IND = function -| CT_co_ind x -> fATOM "co_ind"; - (f_atom_string x); - print_string "\n"and fDECL_NOTATION_OPT = function +| CT_co_ind x -> fATOM "co_ind" ++ + (f_atom_string x) ++ + str "\n" +and fDECL_NOTATION_OPT = function | CT_coerce_NONE_to_DECL_NOTATION_OPT x -> fNONE x | CT_decl_notation(x1, x2, x3) -> - fSTRING x1; - fFORMULA x2; - fID_OPT x3; + fSTRING x1 ++ + fFORMULA x2 ++ + fID_OPT x3 ++ fNODE "decl_notation" 3 and fDEF = function | CT_def(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "def" 2 and fDEFN = function -| CT_defn x -> fATOM "defn"; - (f_atom_string x); - print_string "\n"and fDEFN_OR_THM = function +| CT_defn x -> fATOM "defn" ++ + (f_atom_string x) ++ + str "\n" +and fDEFN_OR_THM = function | CT_coerce_DEFN_to_DEFN_OR_THM x -> fDEFN x | CT_coerce_THM_to_DEFN_OR_THM x -> fTHM x and fDEF_BODY = function | CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x | CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x | CT_type_of(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "type_of" 1 and fDEF_BODY_OPT = function | CT_coerce_DEF_BODY_to_DEF_BODY_OPT x -> fDEF_BODY x | CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT x -> fFORMULA_OPT x and fDEP = function -| CT_dep x -> fATOM "dep"; - (f_atom_string x); - print_string "\n"and fDESTRUCTING = function +| CT_dep x -> fATOM "dep" ++ + (f_atom_string x) ++ + str "\n" +and fDESTRUCTING = function | CT_coerce_NONE_to_DESTRUCTING x -> fNONE x | CT_destructing -> fNODE "destructing" 0 and fDESTRUCT_LOCATION = function @@ -741,54 +752,54 @@ and fDOTDOT_OPT = function | CT_dotdot -> fNODE "dotdot" 0 and fEQN = function | CT_eqn(x1, x2) -> - fMATCH_PATTERN_NE_LIST x1; - fFORMULA x2; + fMATCH_PATTERN_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "eqn" 2 and fEQN_LIST = function | CT_eqn_list l -> - (List.iter fEQN l); + (List.fold_left (++) (mt()) (List.map fEQN l)) ++ fNODE "eqn_list" (List.length l) and fEVAL_CMD = function | CT_eval(x1, x2, x3) -> - fINT_OPT x1; - fRED_COM x2; - fFORMULA x3; + fINT_OPT x1 ++ + fRED_COM x2 ++ + fFORMULA x3 ++ fNODE "eval" 3 and fFIXTAC = function | CT_fixtac(x1, x2, x3) -> - fID x1; - fINT x2; - fFORMULA x3; + fID x1 ++ + fINT x2 ++ + fFORMULA x3 ++ fNODE "fixtac" 3 and fFIX_BINDER = function | CT_coerce_FIX_REC_to_FIX_BINDER x -> fFIX_REC x | CT_fix_binder(x1, x2, x3, x4) -> - fID x1; - fINT x2; - fFORMULA x3; - fFORMULA x4; + fID x1 ++ + fINT x2 ++ + fFORMULA x3 ++ + fFORMULA x4 ++ fNODE "fix_binder" 4 and fFIX_BINDER_LIST = function | CT_fix_binder_list(x,l) -> - fFIX_BINDER x; - (List.iter fFIX_BINDER l); + fFIX_BINDER x ++ + (List.fold_left (++) (mt()) (List.map fFIX_BINDER l)) ++ fNODE "fix_binder_list" (1 + (List.length l)) and fFIX_REC = function | CT_fix_rec(x1, x2, x3, x4, x5) -> - fID x1; - fBINDER_NE_LIST x2; - fID_OPT x3; - fFORMULA x4; - fFORMULA x5; + fID x1 ++ + fBINDER_NE_LIST x2 ++ + fID_OPT x3 ++ + fFORMULA x4 ++ + fFORMULA x5 ++ fNODE "fix_rec" 5 and fFIX_REC_LIST = function | CT_fix_rec_list(x,l) -> - fFIX_REC x; - (List.iter fFIX_REC l); + fFIX_REC x ++ + (List.fold_left (++) (mt()) (List.map fFIX_REC l)) ++ fNODE "fix_rec_list" (1 + (List.length l)) and fFIX_TAC_LIST = function | CT_fix_tac_list l -> - (List.iter fFIXTAC l); + (List.fold_left (++) (mt()) (List.map fFIXTAC l)) ++ fNODE "fix_tac_list" (List.length l) and fFORMULA = function | CT_coerce_BINARY_to_FORMULA x -> fBINARY x @@ -797,90 +808,90 @@ and fFORMULA = function | CT_coerce_SORT_TYPE_to_FORMULA x -> fSORT_TYPE x | CT_coerce_TYPED_FORMULA_to_FORMULA x -> fTYPED_FORMULA x | CT_appc(x1, x2) -> - fFORMULA x1; - fFORMULA_NE_LIST x2; + fFORMULA x1 ++ + fFORMULA_NE_LIST x2 ++ fNODE "appc" 2 | CT_arrowc(x1, x2) -> - fFORMULA x1; - fFORMULA x2; + fFORMULA x1 ++ + fFORMULA x2 ++ fNODE "arrowc" 2 | CT_bang(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "bang" 1 | CT_cases(x1, x2, x3) -> - fMATCHED_FORMULA_NE_LIST x1; - fFORMULA_OPT x2; - fEQN_LIST x3; + fMATCHED_FORMULA_NE_LIST x1 ++ + fFORMULA_OPT x2 ++ + fEQN_LIST x3 ++ fNODE "cases" 3 | CT_cofixc(x1, x2) -> - fID x1; - fCOFIX_REC_LIST x2; + fID x1 ++ + fCOFIX_REC_LIST x2 ++ fNODE "cofixc" 2 | CT_elimc(x1, x2, x3, x4) -> - fCASE x1; - fFORMULA_OPT x2; - fFORMULA x3; - fFORMULA_LIST x4; + fCASE x1 ++ + fFORMULA_OPT x2 ++ + fFORMULA x3 ++ + fFORMULA_LIST x4 ++ fNODE "elimc" 4 | CT_existvarc -> fNODE "existvarc" 0 | CT_fixc(x1, x2) -> - fID x1; - fFIX_BINDER_LIST x2; + fID x1 ++ + fFIX_BINDER_LIST x2 ++ fNODE "fixc" 2 | CT_if(x1, x2, x3, x4) -> - fFORMULA x1; - fRETURN_INFO x2; - fFORMULA x3; - fFORMULA x4; + fFORMULA x1 ++ + fRETURN_INFO x2 ++ + fFORMULA x3 ++ + fFORMULA x4 ++ fNODE "if" 4 | CT_inductive_let(x1, x2, x3, x4) -> - fFORMULA_OPT x1; - fID_OPT_NE_LIST x2; - fFORMULA x3; - fFORMULA x4; + fFORMULA_OPT x1 ++ + fID_OPT_NE_LIST x2 ++ + fFORMULA x3 ++ + fFORMULA x4 ++ fNODE "inductive_let" 4 | CT_labelled_arg(x1, x2) -> - fID x1; - fFORMULA x2; + fID x1 ++ + fFORMULA x2 ++ fNODE "labelled_arg" 2 | CT_lambdac(x1, x2) -> - fBINDER_NE_LIST x1; - fFORMULA x2; + fBINDER_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "lambdac" 2 | CT_let_tuple(x1, x2, x3, x4) -> - fID_OPT_NE_LIST x1; - fRETURN_INFO x2; - fFORMULA x3; - fFORMULA x4; + fID_OPT_NE_LIST x1 ++ + fRETURN_INFO x2 ++ + fFORMULA x3 ++ + fFORMULA x4 ++ fNODE "let_tuple" 4 | CT_letin(x1, x2) -> - fDEF x1; - fFORMULA x2; + fDEF x1 ++ + fFORMULA x2 ++ fNODE "letin" 2 | CT_notation(x1, x2) -> - fSTRING x1; - fFORMULA_LIST x2; + fSTRING x1 ++ + fFORMULA_LIST x2 ++ fNODE "notation" 2 | CT_num_encapsulator(x1, x2) -> - fNUM_TYPE x1; - fFORMULA x2; + fNUM_TYPE x1 ++ + fFORMULA x2 ++ fNODE "num_encapsulator" 2 | CT_prodc(x1, x2) -> - fBINDER_NE_LIST x1; - fFORMULA x2; + fBINDER_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "prodc" 2 | CT_proj(x1, x2) -> - fFORMULA x1; - fFORMULA_NE_LIST x2; + fFORMULA x1 ++ + fFORMULA_NE_LIST x2 ++ fNODE "proj" 2 and fFORMULA_LIST = function | CT_formula_list l -> - (List.iter fFORMULA l); + (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++ fNODE "formula_list" (List.length l) and fFORMULA_NE_LIST = function | CT_formula_ne_list(x,l) -> - fFORMULA x; - (List.iter fFORMULA l); + fFORMULA x ++ + (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++ fNODE "formula_ne_list" (1 + (List.length l)) and fFORMULA_OPT = function | CT_coerce_FORMULA_to_FORMULA_OPT x -> fFORMULA x @@ -893,44 +904,46 @@ and fGRAMMAR = function and fHYP_LOCATION = function | CT_coerce_UNFOLD_to_HYP_LOCATION x -> fUNFOLD x | CT_intype(x1, x2) -> - fID x1; - fINT_LIST x2; + fID x1 ++ + fINT_LIST x2 ++ fNODE "intype" 2 | CT_invalue(x1, x2) -> - fID x1; - fINT_LIST x2; + fID x1 ++ + fINT_LIST x2 ++ fNODE "invalue" 2 and fHYP_LOCATION_LIST_OR_STAR = function | CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR x -> fSTAR x | CT_hyp_location_list l -> - (List.iter fHYP_LOCATION l); + (List.fold_left (++) (mt()) (List.map fHYP_LOCATION l)) ++ fNODE "hyp_location_list" (List.length l) and fID = function -| CT_ident x -> fATOM "ident"; - (f_atom_string x); - print_string "\n"| CT_metac(x1) -> - fINT x1; +| CT_ident x -> fATOM "ident" ++ + (f_atom_string x) ++ + str "\n" +| CT_metac(x1) -> + fINT x1 ++ fNODE "metac" 1 -| CT_metaid x -> fATOM "metaid"; - (f_atom_string x); - print_string "\n"and fIDENTITY_OPT = function +| CT_metaid x -> fATOM "metaid" ++ + (f_atom_string x) ++ + str "\n" +and fIDENTITY_OPT = function | CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x | CT_identity -> fNODE "identity" 0 and fID_LIST = function | CT_id_list l -> - (List.iter fID l); + (List.fold_left (++) (mt()) (List.map fID l)) ++ fNODE "id_list" (List.length l) and fID_LIST_LIST = function | CT_id_list_list l -> - (List.iter fID_LIST l); + (List.fold_left (++) (mt()) (List.map fID_LIST l)) ++ fNODE "id_list_list" (List.length l) and fID_LIST_OPT = function | CT_coerce_ID_LIST_to_ID_LIST_OPT x -> fID_LIST x | CT_coerce_NONE_to_ID_LIST_OPT x -> fNONE x and fID_NE_LIST = function | CT_id_ne_list(x,l) -> - fID x; - (List.iter fID l); + fID x ++ + (List.fold_left (++) (mt()) (List.map fID l)) ++ fNODE "id_ne_list" (1 + (List.length l)) and fID_NE_LIST_OR_STAR = function | CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR x -> fID_NE_LIST x @@ -943,12 +956,12 @@ and fID_OPT = function | CT_coerce_NONE_to_ID_OPT x -> fNONE x and fID_OPT_LIST = function | CT_id_opt_list l -> - (List.iter fID_OPT l); + (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++ fNODE "id_opt_list" (List.length l) and fID_OPT_NE_LIST = function | CT_id_opt_ne_list(x,l) -> - fID_OPT x; - (List.iter fID_OPT l); + fID_OPT x ++ + (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++ fNODE "id_opt_ne_list" (1 + (List.length l)) and fID_OPT_OR_ALL = function | CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x @@ -968,8 +981,8 @@ and fID_OR_STRING = function | CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x and fID_OR_STRING_NE_LIST = function | CT_id_or_string_ne_list(x,l) -> - fID_OR_STRING x; - (List.iter fID_OR_STRING l); + fID_OR_STRING x ++ + (List.fold_left (++) (mt()) (List.map fID_OR_STRING l)) ++ fNODE "id_or_string_ne_list" (1 + (List.length l)) and fIMPEXP = function | CT_coerce_NONE_to_IMPEXP x -> fNONE x @@ -977,40 +990,41 @@ and fIMPEXP = function | CT_import -> fNODE "import" 0 and fIND_SPEC = function | CT_ind_spec(x1, x2, x3, x4, x5) -> - fID x1; - fBINDER_LIST x2; - fFORMULA x3; - fCONSTR_LIST x4; - fDECL_NOTATION_OPT x5; + fID x1 ++ + fBINDER_LIST x2 ++ + fFORMULA x3 ++ + fCONSTR_LIST x4 ++ + fDECL_NOTATION_OPT x5 ++ fNODE "ind_spec" 5 and fIND_SPEC_LIST = function | CT_ind_spec_list l -> - (List.iter fIND_SPEC l); + (List.fold_left (++) (mt()) (List.map fIND_SPEC l)) ++ fNODE "ind_spec_list" (List.length l) and fINT = function -| CT_int x -> fATOM "int"; - (f_atom_int x); - print_string "\n"and fINTRO_PATT = function +| CT_int x -> fATOM "int" ++ + (f_atom_int x) ++ + str "\n" +and fINTRO_PATT = function | CT_coerce_ID_to_INTRO_PATT x -> fID x | CT_disj_pattern(x,l) -> - fINTRO_PATT_LIST x; - (List.iter fINTRO_PATT_LIST l); + fINTRO_PATT_LIST x ++ + (List.fold_left (++) (mt()) (List.map fINTRO_PATT_LIST l)) ++ fNODE "disj_pattern" (1 + (List.length l)) and fINTRO_PATT_LIST = function | CT_intro_patt_list l -> - (List.iter fINTRO_PATT l); + (List.fold_left (++) (mt()) (List.map fINTRO_PATT l)) ++ fNODE "intro_patt_list" (List.length l) and fINTRO_PATT_OPT = function | CT_coerce_ID_OPT_to_INTRO_PATT_OPT x -> fID_OPT x | CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT x -> fINTRO_PATT x and fINT_LIST = function | CT_int_list l -> - (List.iter fINT l); + (List.fold_left (++) (mt()) (List.map fINT l)) ++ fNODE "int_list" (List.length l) and fINT_NE_LIST = function | CT_int_ne_list(x,l) -> - fINT x; - (List.iter fINT l); + fINT x ++ + (List.fold_left (++) (mt()) (List.map fINT l)) ++ fNODE "int_ne_list" (1 + (List.length l)) and fINT_OPT = function | CT_coerce_INT_to_INT_OPT x -> fINT x @@ -1028,21 +1042,21 @@ and fINV_TYPE = function and fIN_OR_OUT_MODULES = function | CT_coerce_NONE_to_IN_OR_OUT_MODULES x -> fNONE x | CT_in_modules(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "in_modules" 1 | CT_out_modules(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "out_modules" 1 and fLET_CLAUSE = function | CT_let_clause(x1, x2, x3) -> - fID x1; - fTACTIC_OPT x2; - fLET_VALUE x3; + fID x1 ++ + fTACTIC_OPT x2 ++ + fLET_VALUE x3 ++ fNODE "let_clause" 3 and fLET_CLAUSES = function | CT_let_clauses(x,l) -> - fLET_CLAUSE x; - (List.iter fLET_CLAUSE l); + fLET_CLAUSE x ++ + (List.fold_left (++) (mt()) (List.map fLET_CLAUSE l)) ++ fNODE "let_clauses" (1 + (List.length l)) and fLET_VALUE = function | CT_coerce_DEF_BODY_to_LET_VALUE x -> fDEF_BODY x @@ -1051,120 +1065,121 @@ and fLOCAL_OPT = function | CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x | CT_local -> fNODE "local" 0 and fLOCN = function -| CT_locn x -> fATOM "locn"; - (f_atom_string x); - print_string "\n"and fMATCHED_FORMULA = function +| CT_locn x -> fATOM "locn" ++ + (f_atom_string x) ++ + str "\n" +and fMATCHED_FORMULA = function | CT_coerce_FORMULA_to_MATCHED_FORMULA x -> fFORMULA x | CT_formula_as(x1, x2) -> - fFORMULA x1; - fID_OPT x2; + fFORMULA x1 ++ + fID_OPT x2 ++ fNODE "formula_as" 2 | CT_formula_as_in(x1, x2, x3) -> - fFORMULA x1; - fID_OPT x2; - fFORMULA x3; + fFORMULA x1 ++ + fID_OPT x2 ++ + fFORMULA x3 ++ fNODE "formula_as_in" 3 | CT_formula_in(x1, x2) -> - fFORMULA x1; - fFORMULA x2; + fFORMULA x1 ++ + fFORMULA x2 ++ fNODE "formula_in" 2 and fMATCHED_FORMULA_NE_LIST = function | CT_matched_formula_ne_list(x,l) -> - fMATCHED_FORMULA x; - (List.iter fMATCHED_FORMULA l); + fMATCHED_FORMULA x ++ + (List.fold_left (++) (mt()) (List.map fMATCHED_FORMULA l)) ++ fNODE "matched_formula_ne_list" (1 + (List.length l)) and fMATCH_PATTERN = function | CT_coerce_ID_OPT_to_MATCH_PATTERN x -> fID_OPT x | CT_coerce_NUM_to_MATCH_PATTERN x -> fNUM x | CT_pattern_app(x1, x2) -> - fMATCH_PATTERN x1; - fMATCH_PATTERN_NE_LIST x2; + fMATCH_PATTERN x1 ++ + fMATCH_PATTERN_NE_LIST x2 ++ fNODE "pattern_app" 2 | CT_pattern_as(x1, x2) -> - fMATCH_PATTERN x1; - fID_OPT x2; + fMATCH_PATTERN x1 ++ + fID_OPT x2 ++ fNODE "pattern_as" 2 | CT_pattern_delimitors(x1, x2) -> - fNUM_TYPE x1; - fMATCH_PATTERN x2; + fNUM_TYPE x1 ++ + fMATCH_PATTERN x2 ++ fNODE "pattern_delimitors" 2 | CT_pattern_notation(x1, x2) -> - fSTRING x1; - fMATCH_PATTERN_LIST x2; + fSTRING x1 ++ + fMATCH_PATTERN_LIST x2 ++ fNODE "pattern_notation" 2 and fMATCH_PATTERN_LIST = function | CT_match_pattern_list l -> - (List.iter fMATCH_PATTERN l); + (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++ fNODE "match_pattern_list" (List.length l) and fMATCH_PATTERN_NE_LIST = function | CT_match_pattern_ne_list(x,l) -> - fMATCH_PATTERN x; - (List.iter fMATCH_PATTERN l); + fMATCH_PATTERN x ++ + (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++ fNODE "match_pattern_ne_list" (1 + (List.length l)) and fMATCH_TAC_RULE = function | CT_match_tac_rule(x1, x2) -> - fCONTEXT_PATTERN x1; - fLET_VALUE x2; + fCONTEXT_PATTERN x1 ++ + fLET_VALUE x2 ++ fNODE "match_tac_rule" 2 and fMATCH_TAC_RULES = function | CT_match_tac_rules(x,l) -> - fMATCH_TAC_RULE x; - (List.iter fMATCH_TAC_RULE l); + fMATCH_TAC_RULE x ++ + (List.fold_left (++) (mt()) (List.map fMATCH_TAC_RULE l)) ++ fNODE "match_tac_rules" (1 + (List.length l)) and fMODIFIER = function | CT_entry_type(x1, x2) -> - fID x1; - fID x2; + fID x1 ++ + fID x2 ++ fNODE "entry_type" 2 | CT_format(x1) -> - fSTRING x1; + fSTRING x1 ++ fNODE "format" 1 | CT_lefta -> fNODE "lefta" 0 | CT_nona -> fNODE "nona" 0 | CT_only_parsing -> fNODE "only_parsing" 0 | CT_righta -> fNODE "righta" 0 | CT_set_item_level(x1, x2) -> - fID_NE_LIST x1; - fINT_OR_NEXT x2; + fID_NE_LIST x1 ++ + fINT_OR_NEXT x2 ++ fNODE "set_item_level" 2 | CT_set_level(x1) -> - fINT x1; + fINT x1 ++ fNODE "set_level" 1 and fMODIFIER_LIST = function | CT_modifier_list l -> - (List.iter fMODIFIER l); + (List.fold_left (++) (mt()) (List.map fMODIFIER l)) ++ fNODE "modifier_list" (List.length l) and fMODULE_BINDER = function | CT_module_binder(x1, x2) -> - fID_NE_LIST x1; - fMODULE_TYPE x2; + fID_NE_LIST x1 ++ + fMODULE_TYPE x2 ++ fNODE "module_binder" 2 and fMODULE_BINDER_LIST = function | CT_module_binder_list l -> - (List.iter fMODULE_BINDER l); + (List.fold_left (++) (mt()) (List.map fMODULE_BINDER l)) ++ fNODE "module_binder_list" (List.length l) and fMODULE_EXPR = function | CT_coerce_ID_OPT_to_MODULE_EXPR x -> fID_OPT x | CT_module_app(x1, x2) -> - fMODULE_EXPR x1; - fMODULE_EXPR x2; + fMODULE_EXPR x1 ++ + fMODULE_EXPR x2 ++ fNODE "module_app" 2 and fMODULE_TYPE = function | CT_coerce_ID_to_MODULE_TYPE x -> fID x | CT_module_type_with_def(x1, x2, x3) -> - fMODULE_TYPE x1; - fID_LIST x2; - fFORMULA x3; + fMODULE_TYPE x1 ++ + fID_LIST x2 ++ + fFORMULA x3 ++ fNODE "module_type_with_def" 3 | CT_module_type_with_mod(x1, x2, x3) -> - fMODULE_TYPE x1; - fID_LIST x2; - fID x3; + fMODULE_TYPE x1 ++ + fID_LIST x2 ++ + fID x3 ++ fNODE "module_type_with_mod" 3 and fMODULE_TYPE_CHECK = function | CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x | CT_only_check(x1) -> - fMODULE_TYPE x1; + fMODULE_TYPE x1 ++ fNODE "only_check" 1 and fMODULE_TYPE_OPT = function | CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x @@ -1176,12 +1191,14 @@ and fNATURAL_FEATURE = function and fNONE = function | CT_none -> fNODE "none" 0 and fNUM = function -| CT_int_encapsulator x -> fATOM "int_encapsulator"; - (f_atom_string x); - print_string "\n"and fNUM_TYPE = function -| CT_num_type x -> fATOM "num_type"; - (f_atom_string x); - print_string "\n"and fOMEGA_FEATURE = function +| CT_int_encapsulator x -> fATOM "int_encapsulator" ++ + (f_atom_string x) ++ + str "\n" +and fNUM_TYPE = function +| CT_num_type x -> fATOM "num_type" ++ + (f_atom_string x) ++ + str "\n" +and fOMEGA_FEATURE = function | CT_coerce_STRING_to_OMEGA_FEATURE x -> fSTRING x | CT_flag_action -> fNODE "flag_action" 0 | CT_flag_system -> fNODE "flag_system" 0 @@ -1195,13 +1212,13 @@ and fORIENTATION = function | CT_rl -> fNODE "rl" 0 and fPATTERN = function | CT_pattern_occ(x1, x2) -> - fINT_LIST x1; - fFORMULA x2; + fINT_LIST x1 ++ + fFORMULA x2 ++ fNODE "pattern_occ" 2 and fPATTERN_NE_LIST = function | CT_pattern_ne_list(x,l) -> - fPATTERN x; - (List.iter fPATTERN l); + fPATTERN x ++ + (List.fold_left (++) (mt()) (List.map fPATTERN l)) ++ fNODE "pattern_ne_list" (1 + (List.length l)) and fPATTERN_OPT = function | CT_coerce_NONE_to_PATTERN_OPT x -> fNONE x @@ -1209,146 +1226,147 @@ and fPATTERN_OPT = function and fPREMISE = function | CT_coerce_TYPED_FORMULA_to_PREMISE x -> fTYPED_FORMULA x | CT_eval_result(x1, x2, x3) -> - fFORMULA x1; - fFORMULA x2; - fFORMULA x3; + fFORMULA x1 ++ + fFORMULA x2 ++ + fFORMULA x3 ++ fNODE "eval_result" 3 | CT_premise(x1, x2) -> - fID x1; - fFORMULA x2; + fID x1 ++ + fFORMULA x2 ++ fNODE "premise" 2 and fPREMISES_LIST = function | CT_premises_list l -> - (List.iter fPREMISE l); + (List.fold_left (++) (mt()) (List.map fPREMISE l)) ++ fNODE "premises_list" (List.length l) and fPREMISE_PATTERN = function | CT_premise_pattern(x1, x2) -> - fID_OPT x1; - fCONTEXT_PATTERN x2; + fID_OPT x1 ++ + fCONTEXT_PATTERN x2 ++ fNODE "premise_pattern" 2 and fPROOF_SCRIPT = function | CT_proof_script l -> - (List.iter fCOMMAND l); + (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++ fNODE "proof_script" (List.length l) and fRECCONSTR = function | CT_defrecconstr(x1, x2, x3) -> - fID_OPT x1; - fFORMULA x2; - fFORMULA_OPT x3; + fID_OPT x1 ++ + fFORMULA x2 ++ + fFORMULA_OPT x3 ++ fNODE "defrecconstr" 3 | CT_defrecconstr_coercion(x1, x2, x3) -> - fID_OPT x1; - fFORMULA x2; - fFORMULA_OPT x3; + fID_OPT x1 ++ + fFORMULA x2 ++ + fFORMULA_OPT x3 ++ fNODE "defrecconstr_coercion" 3 | CT_recconstr(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "recconstr" 2 | CT_recconstr_coercion(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "recconstr_coercion" 2 and fRECCONSTR_LIST = function | CT_recconstr_list l -> - (List.iter fRECCONSTR l); + (List.fold_left (++) (mt()) (List.map fRECCONSTR l)) ++ fNODE "recconstr_list" (List.length l) and fREC_TACTIC_FUN = function | CT_rec_tactic_fun(x1, x2, x3) -> - fID x1; - fID_OPT_NE_LIST x2; - fTACTIC_COM x3; + fID x1 ++ + fID_OPT_NE_LIST x2 ++ + fTACTIC_COM x3 ++ fNODE "rec_tactic_fun" 3 and fREC_TACTIC_FUN_LIST = function | CT_rec_tactic_fun_list(x,l) -> - fREC_TACTIC_FUN x; - (List.iter fREC_TACTIC_FUN l); + fREC_TACTIC_FUN x ++ + (List.fold_left (++) (mt()) (List.map fREC_TACTIC_FUN l)) ++ fNODE "rec_tactic_fun_list" (1 + (List.length l)) and fRED_COM = function | CT_cbv(x1, x2) -> - fCONVERSION_FLAG_LIST x1; - fCONV_SET x2; + fCONVERSION_FLAG_LIST x1 ++ + fCONV_SET x2 ++ fNODE "cbv" 2 | CT_fold(x1) -> - fFORMULA_LIST x1; + fFORMULA_LIST x1 ++ fNODE "fold" 1 | CT_hnf -> fNODE "hnf" 0 | CT_lazy(x1, x2) -> - fCONVERSION_FLAG_LIST x1; - fCONV_SET x2; + fCONVERSION_FLAG_LIST x1 ++ + fCONV_SET x2 ++ fNODE "lazy" 2 | CT_pattern(x1) -> - fPATTERN_NE_LIST x1; + fPATTERN_NE_LIST x1 ++ fNODE "pattern" 1 | CT_red -> fNODE "red" 0 | CT_cbvvm -> fNODE "vm_compute" 0 | CT_simpl(x1) -> - fPATTERN_OPT x1; + fPATTERN_OPT x1 ++ fNODE "simpl" 1 | CT_unfold(x1) -> - fUNFOLD_NE_LIST x1; + fUNFOLD_NE_LIST x1 ++ fNODE "unfold" 1 and fRETURN_INFO = function | CT_coerce_NONE_to_RETURN_INFO x -> fNONE x | CT_as_and_return(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "as_and_return" 2 | CT_return(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "return" 1 and fRULE = function | CT_rule(x1, x2) -> - fPREMISES_LIST x1; - fFORMULA x2; + fPREMISES_LIST x1 ++ + fFORMULA x2 ++ fNODE "rule" 2 and fRULE_LIST = function | CT_rule_list l -> - (List.iter fRULE l); + (List.fold_left (++) (mt()) (List.map fRULE l)) ++ fNODE "rule_list" (List.length l) and fSCHEME_SPEC = function | CT_scheme_spec(x1, x2, x3, x4) -> - fID x1; - fDEP x2; - fFORMULA x3; - fSORT_TYPE x4; + fID x1 ++ + fDEP x2 ++ + fFORMULA x3 ++ + fSORT_TYPE x4 ++ fNODE "scheme_spec" 4 and fSCHEME_SPEC_LIST = function | CT_scheme_spec_list(x,l) -> - fSCHEME_SPEC x; - (List.iter fSCHEME_SPEC l); + fSCHEME_SPEC x ++ + (List.fold_left (++) (mt()) (List.map fSCHEME_SPEC l)) ++ fNODE "scheme_spec_list" (1 + (List.length l)) and fSCOMMENT_CONTENT = function | CT_coerce_FORMULA_to_SCOMMENT_CONTENT x -> fFORMULA x | CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT x -> fID_OR_STRING x and fSCOMMENT_CONTENT_LIST = function | CT_scomment_content_list l -> - (List.iter fSCOMMENT_CONTENT l); + (List.fold_left (++) (mt()) (List.map fSCOMMENT_CONTENT l)) ++ fNODE "scomment_content_list" (List.length l) and fSECTION_BEGIN = function | CT_section(x1) -> - fID x1; + fID x1 ++ fNODE "section" 1 and fSECTION_BODY = function | CT_section_body l -> - (List.iter fCOMMAND l); + (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++ fNODE "section_body" (List.length l) and fSIGNED_INT = function | CT_coerce_INT_to_SIGNED_INT x -> fINT x | CT_minus(x1) -> - fINT x1; + fINT x1 ++ fNODE "minus" 1 and fSIGNED_INT_LIST = function | CT_signed_int_list l -> - (List.iter fSIGNED_INT l); + (List.fold_left (++) (mt()) (List.map fSIGNED_INT l)) ++ fNODE "signed_int_list" (List.length l) and fSINGLE_OPTION_VALUE = function | CT_coerce_INT_to_SINGLE_OPTION_VALUE x -> fINT x | CT_coerce_STRING_to_SINGLE_OPTION_VALUE x -> fSTRING x and fSORT_TYPE = function -| CT_sortc x -> fATOM "sortc"; - (f_atom_string x); - print_string "\n"and fSPEC_LIST = function +| CT_sortc x -> fATOM "sortc" ++ + (f_atom_string x) ++ + str "\n" +and fSPEC_LIST = function | CT_coerce_BINDING_LIST_to_SPEC_LIST x -> fBINDING_LIST x | CT_coerce_FORMULA_LIST_to_SPEC_LIST x -> fFORMULA_LIST x and fSPEC_OPT = function @@ -1360,12 +1378,13 @@ and fSTAR_OPT = function | CT_coerce_NONE_to_STAR_OPT x -> fNONE x | CT_coerce_STAR_to_STAR_OPT x -> fSTAR x and fSTRING = function -| CT_string x -> fATOM "string"; - (f_atom_string x); - print_string "\n"and fSTRING_NE_LIST = function +| CT_string x -> fATOM "string" ++ + (f_atom_string x) ++ + str "\n" +and fSTRING_NE_LIST = function | CT_string_ne_list(x,l) -> - fSTRING x; - (List.iter fSTRING l); + fSTRING x ++ + (List.fold_left (++) (mt()) (List.map fSTRING l)) ++ fNODE "string_ne_list" (1 + (List.length l)) and fSTRING_OPT = function | CT_coerce_NONE_to_STRING_OPT x -> fNONE x @@ -1373,8 +1392,8 @@ and fSTRING_OPT = function and fTABLE = function | CT_coerce_ID_to_TABLE x -> fID x | CT_table(x1, x2) -> - fID x1; - fID x2; + fID x1 ++ + fID x2 ++ fNODE "table" 2 and fTACTIC_ARG = function | CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x @@ -1384,429 +1403,429 @@ and fTACTIC_ARG = function | CT_void -> fNODE "void" 0 and fTACTIC_ARG_LIST = function | CT_tactic_arg_list(x,l) -> - fTACTIC_ARG x; - (List.iter fTACTIC_ARG l); + fTACTIC_ARG x ++ + (List.fold_left (++) (mt()) (List.map fTACTIC_ARG l)) ++ fNODE "tactic_arg_list" (1 + (List.length l)) and fTACTIC_COM = function | CT_abstract(x1, x2) -> - fID_OPT x1; - fTACTIC_COM x2; + fID_OPT x1 ++ + fTACTIC_COM x2 ++ fNODE "abstract" 2 | CT_absurd(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "absurd" 1 | CT_any_constructor(x1) -> - fTACTIC_OPT x1; + fTACTIC_OPT x1 ++ fNODE "any_constructor" 1 | CT_apply(x1, x2) -> - fFORMULA x1; - fSPEC_LIST x2; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ fNODE "apply" 2 | CT_assert(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "assert" 2 | CT_assumption -> fNODE "assumption" 0 | CT_auto(x1) -> - fINT_OPT x1; + fINT_OPT x1 ++ fNODE "auto" 1 | CT_auto_with(x1, x2) -> - fINT_OPT x1; - fID_NE_LIST_OR_STAR x2; + fINT_OPT x1 ++ + fID_NE_LIST_OR_STAR x2 ++ fNODE "auto_with" 2 | CT_autorewrite(x1, x2) -> - fID_NE_LIST x1; - fTACTIC_OPT x2; + fID_NE_LIST x1 ++ + fTACTIC_OPT x2 ++ fNODE "autorewrite" 2 | CT_autotdb(x1) -> - fINT_OPT x1; + fINT_OPT x1 ++ fNODE "autotdb" 1 | CT_case_type(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "case_type" 1 | CT_casetac(x1, x2) -> - fFORMULA x1; - fSPEC_LIST x2; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ fNODE "casetac" 2 | CT_cdhyp(x1) -> - fID x1; + fID x1 ++ fNODE "cdhyp" 1 | CT_change(x1, x2) -> - fFORMULA x1; - fCLAUSE x2; + fFORMULA x1 ++ + fCLAUSE x2 ++ fNODE "change" 2 | CT_change_local(x1, x2, x3) -> - fPATTERN x1; - fFORMULA x2; - fCLAUSE x3; + fPATTERN x1 ++ + fFORMULA x2 ++ + fCLAUSE x3 ++ fNODE "change_local" 3 | CT_clear(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "clear" 1 | CT_clear_body(x1) -> - fID_NE_LIST x1; + fID_NE_LIST x1 ++ fNODE "clear_body" 1 | CT_cofixtactic(x1, x2) -> - fID_OPT x1; - fCOFIX_TAC_LIST x2; + fID_OPT x1 ++ + fCOFIX_TAC_LIST x2 ++ fNODE "cofixtactic" 2 | CT_condrewrite_lr(x1, x2, x3, x4) -> - fTACTIC_COM x1; - fFORMULA x2; - fSPEC_LIST x3; - fID_OPT x4; + fTACTIC_COM x1 ++ + fFORMULA x2 ++ + fSPEC_LIST x3 ++ + fID_OPT x4 ++ fNODE "condrewrite_lr" 4 | CT_condrewrite_rl(x1, x2, x3, x4) -> - fTACTIC_COM x1; - fFORMULA x2; - fSPEC_LIST x3; - fID_OPT x4; + fTACTIC_COM x1 ++ + fFORMULA x2 ++ + fSPEC_LIST x3 ++ + fID_OPT x4 ++ fNODE "condrewrite_rl" 4 | CT_constructor(x1, x2) -> - fINT x1; - fSPEC_LIST x2; + fINT x1 ++ + fSPEC_LIST x2 ++ fNODE "constructor" 2 | CT_contradiction -> fNODE "contradiction" 0 | CT_contradiction_thm(x1, x2) -> - fFORMULA x1; - fSPEC_LIST x2; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ fNODE "contradiction_thm" 2 | CT_cut(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "cut" 1 | CT_cutrewrite_lr(x1, x2) -> - fFORMULA x1; - fID_OPT x2; + fFORMULA x1 ++ + fID_OPT x2 ++ fNODE "cutrewrite_lr" 2 | CT_cutrewrite_rl(x1, x2) -> - fFORMULA x1; - fID_OPT x2; + fFORMULA x1 ++ + fID_OPT x2 ++ fNODE "cutrewrite_rl" 2 | CT_dauto(x1, x2) -> - fINT_OPT x1; - fINT_OPT x2; + fINT_OPT x1 ++ + fINT_OPT x2 ++ fNODE "dauto" 2 | CT_dconcl -> fNODE "dconcl" 0 | CT_decompose_list(x1, x2) -> - fID_NE_LIST x1; - fFORMULA x2; + fID_NE_LIST x1 ++ + fFORMULA x2 ++ fNODE "decompose_list" 2 | CT_decompose_record(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "decompose_record" 1 | CT_decompose_sum(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "decompose_sum" 1 | CT_depinversion(x1, x2, x3, x4) -> - fINV_TYPE x1; - fID_OR_INT x2; - fINTRO_PATT_OPT x3; - fFORMULA_OPT x4; + fINV_TYPE x1 ++ + fID_OR_INT x2 ++ + fINTRO_PATT_OPT x3 ++ + fFORMULA_OPT x4 ++ fNODE "depinversion" 4 | CT_deprewrite_lr(x1) -> - fID x1; + fID x1 ++ fNODE "deprewrite_lr" 1 | CT_deprewrite_rl(x1) -> - fID x1; + fID x1 ++ fNODE "deprewrite_rl" 1 | CT_destruct(x1) -> - fID_OR_INT x1; + fID_OR_INT x1 ++ fNODE "destruct" 1 | CT_dhyp(x1) -> - fID x1; + fID x1 ++ fNODE "dhyp" 1 | CT_discriminate_eq(x1) -> - fID_OR_INT_OPT x1; + fID_OR_INT_OPT x1 ++ fNODE "discriminate_eq" 1 | CT_do(x1, x2) -> - fID_OR_INT x1; - fTACTIC_COM x2; + fID_OR_INT x1 ++ + fTACTIC_COM x2 ++ fNODE "do" 2 | CT_eapply(x1, x2) -> - fFORMULA x1; - fSPEC_LIST x2; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ fNODE "eapply" 2 | CT_eauto(x1, x2) -> - fID_OR_INT_OPT x1; - fID_OR_INT_OPT x2; + fID_OR_INT_OPT x1 ++ + fID_OR_INT_OPT x2 ++ fNODE "eauto" 2 | CT_eauto_with(x1, x2, x3) -> - fID_OR_INT_OPT x1; - fID_OR_INT_OPT x2; - fID_NE_LIST_OR_STAR x3; + fID_OR_INT_OPT x1 ++ + fID_OR_INT_OPT x2 ++ + fID_NE_LIST_OR_STAR x3 ++ fNODE "eauto_with" 3 | CT_elim(x1, x2, x3) -> - fFORMULA x1; - fSPEC_LIST x2; - fUSING x3; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ + fUSING x3 ++ fNODE "elim" 3 | CT_elim_type(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "elim_type" 1 | CT_exact(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "exact" 1 | CT_exact_no_check(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "exact_no_check" 1 | CT_vm_cast_no_check(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "vm_cast_no_check" 1 | CT_exists(x1) -> - fSPEC_LIST x1; + fSPEC_LIST x1 ++ fNODE "exists" 1 | CT_fail(x1, x2) -> - fID_OR_INT x1; - fSTRING_OPT x2; + fID_OR_INT x1 ++ + fSTRING_OPT x2 ++ fNODE "fail" 2 | CT_first(x,l) -> - fTACTIC_COM x; - (List.iter fTACTIC_COM l); + fTACTIC_COM x ++ + (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++ fNODE "first" (1 + (List.length l)) | CT_firstorder(x1) -> - fTACTIC_OPT x1; + fTACTIC_OPT x1 ++ fNODE "firstorder" 1 | CT_firstorder_using(x1, x2) -> - fTACTIC_OPT x1; - fID_NE_LIST x2; + fTACTIC_OPT x1 ++ + fID_NE_LIST x2 ++ fNODE "firstorder_using" 2 | CT_firstorder_with(x1, x2) -> - fTACTIC_OPT x1; - fID_NE_LIST x2; + fTACTIC_OPT x1 ++ + fID_NE_LIST x2 ++ fNODE "firstorder_with" 2 | CT_fixtactic(x1, x2, x3) -> - fID_OPT x1; - fINT x2; - fFIX_TAC_LIST x3; + fID_OPT x1 ++ + fINT x2 ++ + fFIX_TAC_LIST x3 ++ fNODE "fixtactic" 3 | CT_formula_marker(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "formula_marker" 1 | CT_fresh(x1) -> - fSTRING_OPT x1; + fSTRING_OPT x1 ++ fNODE "fresh" 1 | CT_generalize(x1) -> - fFORMULA_NE_LIST x1; + fFORMULA_NE_LIST x1 ++ fNODE "generalize" 1 | CT_generalize_dependent(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "generalize_dependent" 1 | CT_idtac(x1) -> - fSTRING_OPT x1; + fSTRING_OPT x1 ++ fNODE "idtac" 1 | CT_induction(x1) -> - fID_OR_INT x1; + fID_OR_INT x1 ++ fNODE "induction" 1 | CT_info(x1) -> - fTACTIC_COM x1; + fTACTIC_COM x1 ++ fNODE "info" 1 | CT_injection_eq(x1) -> - fID_OR_INT_OPT x1; + fID_OR_INT_OPT x1 ++ fNODE "injection_eq" 1 | CT_instantiate(x1, x2, x3) -> - fINT x1; - fFORMULA x2; - fCLAUSE x3; + fINT x1 ++ + fFORMULA x2 ++ + fCLAUSE x3 ++ fNODE "instantiate" 3 | CT_intro(x1) -> - fID_OPT x1; + fID_OPT x1 ++ fNODE "intro" 1 | CT_intro_after(x1, x2) -> - fID_OPT x1; - fID x2; + fID_OPT x1 ++ + fID x2 ++ fNODE "intro_after" 2 | CT_intros(x1) -> - fINTRO_PATT_LIST x1; + fINTRO_PATT_LIST x1 ++ fNODE "intros" 1 | CT_intros_until(x1) -> - fID_OR_INT x1; + fID_OR_INT x1 ++ fNODE "intros_until" 1 | CT_inversion(x1, x2, x3, x4) -> - fINV_TYPE x1; - fID_OR_INT x2; - fINTRO_PATT_OPT x3; - fID_LIST x4; + fINV_TYPE x1 ++ + fID_OR_INT x2 ++ + fINTRO_PATT_OPT x3 ++ + fID_LIST x4 ++ fNODE "inversion" 4 | CT_left(x1) -> - fSPEC_LIST x1; + fSPEC_LIST x1 ++ fNODE "left" 1 | CT_let_ltac(x1, x2) -> - fLET_CLAUSES x1; - fLET_VALUE x2; + fLET_CLAUSES x1 ++ + fLET_VALUE x2 ++ fNODE "let_ltac" 2 | CT_lettac(x1, x2, x3) -> - fID_OPT x1; - fFORMULA x2; - fCLAUSE x3; + fID_OPT x1 ++ + fFORMULA x2 ++ + fCLAUSE x3 ++ fNODE "lettac" 3 | CT_match_context(x,l) -> - fCONTEXT_RULE x; - (List.iter fCONTEXT_RULE l); + fCONTEXT_RULE x ++ + (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++ fNODE "match_context" (1 + (List.length l)) | CT_match_context_reverse(x,l) -> - fCONTEXT_RULE x; - (List.iter fCONTEXT_RULE l); + fCONTEXT_RULE x ++ + (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++ fNODE "match_context_reverse" (1 + (List.length l)) | CT_match_tac(x1, x2) -> - fTACTIC_COM x1; - fMATCH_TAC_RULES x2; + fTACTIC_COM x1 ++ + fMATCH_TAC_RULES x2 ++ fNODE "match_tac" 2 | CT_move_after(x1, x2) -> - fID x1; - fID x2; + fID x1 ++ + fID x2 ++ fNODE "move_after" 2 | CT_new_destruct(x1, x2, x3) -> - (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *) - fUSING x2; - fINTRO_PATT_OPT x3; + (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Julien F. Est-ce correct? *) + fUSING x2 ++ + fINTRO_PATT_OPT x3 ++ fNODE "new_destruct" 3 | CT_new_induction(x1, x2, x3) -> - (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *) - fUSING x2; - fINTRO_PATT_OPT x3; + (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Pierre C. Est-ce correct? *) + fUSING x2 ++ + fINTRO_PATT_OPT x3 ++ fNODE "new_induction" 3 | CT_omega -> fNODE "omega" 0 | CT_orelse(x1, x2) -> - fTACTIC_COM x1; - fTACTIC_COM x2; + fTACTIC_COM x1 ++ + fTACTIC_COM x2 ++ fNODE "orelse" 2 | CT_parallel(x,l) -> - fTACTIC_COM x; - (List.iter fTACTIC_COM l); + fTACTIC_COM x ++ + (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++ fNODE "parallel" (1 + (List.length l)) | CT_pose(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "pose" 2 | CT_progress(x1) -> - fTACTIC_COM x1; + fTACTIC_COM x1 ++ fNODE "progress" 1 | CT_prolog(x1, x2) -> - fFORMULA_LIST x1; - fINT x2; + fFORMULA_LIST x1 ++ + fINT x2 ++ fNODE "prolog" 2 | CT_rec_tactic_in(x1, x2) -> - fREC_TACTIC_FUN_LIST x1; - fTACTIC_COM x2; + fREC_TACTIC_FUN_LIST x1 ++ + fTACTIC_COM x2 ++ fNODE "rec_tactic_in" 2 | CT_reduce(x1, x2) -> - fRED_COM x1; - fCLAUSE x2; + fRED_COM x1 ++ + fCLAUSE x2 ++ fNODE "reduce" 2 | CT_refine(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "refine" 1 | CT_reflexivity -> fNODE "reflexivity" 0 | CT_rename(x1, x2) -> - fID x1; - fID x2; + fID x1 ++ + fID x2 ++ fNODE "rename" 2 | CT_repeat(x1) -> - fTACTIC_COM x1; + fTACTIC_COM x1 ++ fNODE "repeat" 1 | CT_replace_with(x1, x2,x3,x4) -> - fFORMULA x1; - fFORMULA x2; - fCLAUSE x3; - fTACTIC_OPT x4; + fFORMULA x1 ++ + fFORMULA x2 ++ + fCLAUSE x3 ++ + fTACTIC_OPT x4 ++ fNODE "replace_with" 4 | CT_rewrite_lr(x1, x2, x3) -> - fFORMULA x1; - fSPEC_LIST x2; - fCLAUSE x3; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ + fCLAUSE x3 ++ fNODE "rewrite_lr" 3 | CT_rewrite_rl(x1, x2, x3) -> - fFORMULA x1; - fSPEC_LIST x2; - fCLAUSE x3; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ + fCLAUSE x3 ++ fNODE "rewrite_rl" 3 | CT_right(x1) -> - fSPEC_LIST x1; + fSPEC_LIST x1 ++ fNODE "right" 1 | CT_ring(x1) -> - fFORMULA_LIST x1; + fFORMULA_LIST x1 ++ fNODE "ring" 1 | CT_simple_user_tac(x1, x2) -> - fID x1; - fTACTIC_ARG_LIST x2; + fID x1 ++ + fTACTIC_ARG_LIST x2 ++ fNODE "simple_user_tac" 2 | CT_simplify_eq(x1) -> - fID_OR_INT_OPT x1; + fID_OR_INT_OPT x1 ++ fNODE "simplify_eq" 1 | CT_specialize(x1, x2, x3) -> - fINT_OPT x1; - fFORMULA x2; - fSPEC_LIST x3; + fINT_OPT x1 ++ + fFORMULA x2 ++ + fSPEC_LIST x3 ++ fNODE "specialize" 3 | CT_split(x1) -> - fSPEC_LIST x1; + fSPEC_LIST x1 ++ fNODE "split" 1 | CT_subst(x1) -> - fID_LIST x1; + fID_LIST x1 ++ fNODE "subst" 1 | CT_superauto(x1, x2, x3, x4) -> - fINT_OPT x1; - fID_LIST x2; - fDESTRUCTING x3; - fUSINGTDB x4; + fINT_OPT x1 ++ + fID_LIST x2 ++ + fDESTRUCTING x3 ++ + fUSINGTDB x4 ++ fNODE "superauto" 4 | CT_symmetry(x1) -> - fCLAUSE x1; + fCLAUSE x1 ++ fNODE "symmetry" 1 | CT_tac_double(x1, x2) -> - fID_OR_INT x1; - fID_OR_INT x2; + fID_OR_INT x1 ++ + fID_OR_INT x2 ++ fNODE "tac_double" 2 | CT_tacsolve(x,l) -> - fTACTIC_COM x; - (List.iter fTACTIC_COM l); + fTACTIC_COM x ++ + (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++ fNODE "tacsolve" (1 + (List.length l)) | CT_tactic_fun(x1, x2) -> - fID_OPT_NE_LIST x1; - fTACTIC_COM x2; + fID_OPT_NE_LIST x1 ++ + fTACTIC_COM x2 ++ fNODE "tactic_fun" 2 | CT_then(x,l) -> - fTACTIC_COM x; - (List.iter fTACTIC_COM l); + fTACTIC_COM x ++ + (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++ fNODE "then" (1 + (List.length l)) | CT_transitivity(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "transitivity" 1 | CT_trivial -> fNODE "trivial" 0 | CT_trivial_with(x1) -> - fID_NE_LIST_OR_STAR x1; + fID_NE_LIST_OR_STAR x1 ++ fNODE "trivial_with" 1 | CT_truecut(x1, x2) -> - fID_OPT x1; - fFORMULA x2; + fID_OPT x1 ++ + fFORMULA x2 ++ fNODE "truecut" 2 | CT_try(x1) -> - fTACTIC_COM x1; + fTACTIC_COM x1 ++ fNODE "try" 1 | CT_use(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "use" 1 | CT_use_inversion(x1, x2, x3) -> - fID_OR_INT x1; - fFORMULA x2; - fID_LIST x3; + fID_OR_INT x1 ++ + fFORMULA x2 ++ + fID_LIST x3 ++ fNODE "use_inversion" 3 | CT_user_tac(x1, x2) -> - fID x1; - fTARG_LIST x2; + fID x1 ++ + fTARG_LIST x2 ++ fNODE "user_tac" 2 and fTACTIC_OPT = function | CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x | CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x and fTAC_DEF = function | CT_tac_def(x1, x2) -> - fID x1; - fTACTIC_COM x2; + fID x1 ++ + fTACTIC_COM x2 ++ fNODE "tac_def" 2 and fTAC_DEF_NE_LIST = function | CT_tac_def_ne_list(x,l) -> - fTAC_DEF x; - (List.iter fTAC_DEF l); + fTAC_DEF x ++ + (List.fold_left (++) (mt()) (List.map fTAC_DEF l)) ++ fNODE "tac_def_ne_list" (1 + (List.length l)) and fTARG = function | CT_coerce_BINDING_to_TARG x -> fBINDING x @@ -1824,81 +1843,83 @@ and fTARG = function | CT_coerce_UNFOLD_NE_LIST_to_TARG x -> fUNFOLD_NE_LIST x and fTARG_LIST = function | CT_targ_list l -> - (List.iter fTARG l); + (List.fold_left (++) (mt()) (List.map fTARG l)) ++ fNODE "targ_list" (List.length l) and fTERM_CHANGE = function | CT_check_term(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "check_term" 1 | CT_inst_term(x1, x2) -> - fID x1; - fFORMULA x2; + fID x1 ++ + fFORMULA x2 ++ fNODE "inst_term" 2 and fTEXT = function | CT_coerce_ID_to_TEXT x -> fID x | CT_text_formula(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "text_formula" 1 | CT_text_h l -> - (List.iter fTEXT l); + (List.fold_left (++) (mt()) (List.map fTEXT l)) ++ fNODE "text_h" (List.length l) | CT_text_hv l -> - (List.iter fTEXT l); + (List.fold_left (++) (mt()) (List.map fTEXT l)) ++ fNODE "text_hv" (List.length l) | CT_text_op l -> - (List.iter fTEXT l); + (List.fold_left (++) (mt()) (List.map fTEXT l)) ++ fNODE "text_op" (List.length l) | CT_text_path(x1) -> - fSIGNED_INT_LIST x1; + fSIGNED_INT_LIST x1 ++ fNODE "text_path" 1 | CT_text_v l -> - (List.iter fTEXT l); + (List.fold_left (++) (mt()) (List.map fTEXT l)) ++ fNODE "text_v" (List.length l) and fTHEOREM_GOAL = function | CT_goal(x1) -> - fFORMULA x1; + fFORMULA x1 ++ fNODE "goal" 1 | CT_theorem_goal(x1, x2, x3, x4) -> - fDEFN_OR_THM x1; - fID x2; - fBINDER_LIST x3; - fFORMULA x4; + fDEFN_OR_THM x1 ++ + fID x2 ++ + fBINDER_LIST x3 ++ + fFORMULA x4 ++ fNODE "theorem_goal" 4 and fTHM = function -| CT_thm x -> fATOM "thm"; - (f_atom_string x); - print_string "\n"and fTHM_OPT = function +| CT_thm x -> fATOM "thm" ++ + (f_atom_string x) ++ + str "\n" +and fTHM_OPT = function | CT_coerce_NONE_to_THM_OPT x -> fNONE x | CT_coerce_THM_to_THM_OPT x -> fTHM x and fTYPED_FORMULA = function | CT_typed_formula(x1, x2) -> - fFORMULA x1; - fFORMULA x2; + fFORMULA x1 ++ + fFORMULA x2 ++ fNODE "typed_formula" 2 and fUNFOLD = function | CT_coerce_ID_to_UNFOLD x -> fID x | CT_unfold_occ(x1, x2) -> - fID x1; - fINT_NE_LIST x2; + fID x1 ++ + fINT_NE_LIST x2 ++ fNODE "unfold_occ" 2 and fUNFOLD_NE_LIST = function | CT_unfold_ne_list(x,l) -> - fUNFOLD x; - (List.iter fUNFOLD l); + fUNFOLD x ++ + (List.fold_left (++) (mt()) (List.map fUNFOLD l)) ++ fNODE "unfold_ne_list" (1 + (List.length l)) and fUSING = function | CT_coerce_NONE_to_USING x -> fNONE x | CT_using(x1, x2) -> - fFORMULA x1; - fSPEC_LIST x2; + fFORMULA x1 ++ + fSPEC_LIST x2 ++ fNODE "using" 2 and fUSINGTDB = function | CT_coerce_NONE_to_USINGTDB x -> fNONE x | CT_usingtdb -> fNODE "usingtdb" 0 and fVAR = function -| CT_var x -> fATOM "var"; - (f_atom_string x); - print_string "\n"and fVARG = function +| CT_var x -> fATOM "var" ++ + (f_atom_string x) ++ + str "\n" +and fVARG = function | CT_coerce_AST_to_VARG x -> fAST x | CT_coerce_AST_LIST_to_VARG x -> fAST_LIST x | CT_coerce_BINDER_to_VARG x -> fBINDER x @@ -1916,7 +1937,7 @@ and fVAR = function | CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x and fVARG_LIST = function | CT_varg_list l -> - (List.iter fVARG l); + (List.fold_left (++) (mt()) (List.map fVARG l)) ++ fNODE "varg_list" (List.length l) and fVERBOSE_OPT = function | CT_coerce_NONE_to_VERBOSE_OPT x -> fNONE x diff --git a/contrib/interface/vtp.mli b/contrib/interface/vtp.mli index fe30b317..d7bd8db5 100644 --- a/contrib/interface/vtp.mli +++ b/contrib/interface/vtp.mli @@ -1,15 +1,16 @@ open Ascent;; +open Pp;; -val fCOMMAND_LIST : ct_COMMAND_LIST -> unit;; -val fCOMMAND : ct_COMMAND -> unit;; -val fTACTIC_COM : ct_TACTIC_COM -> unit;; -val fFORMULA : ct_FORMULA -> unit;; -val fID : ct_ID -> unit;; -val fSTRING : ct_STRING -> unit;; -val fINT : ct_INT -> unit;; -val fRULE_LIST : ct_RULE_LIST -> unit;; -val fRULE : ct_RULE -> unit;; -val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> unit;; -val fPREMISES_LIST : ct_PREMISES_LIST -> unit;; -val fID_LIST : ct_ID_LIST -> unit;; -val fTEXT : ct_TEXT -> unit;;
\ No newline at end of file +val fCOMMAND_LIST : ct_COMMAND_LIST -> std_ppcmds;; +val fCOMMAND : ct_COMMAND -> std_ppcmds;; +val fTACTIC_COM : ct_TACTIC_COM -> std_ppcmds;; +val fFORMULA : ct_FORMULA -> std_ppcmds;; +val fID : ct_ID -> std_ppcmds;; +val fSTRING : ct_STRING -> std_ppcmds;; +val fINT : ct_INT -> std_ppcmds;; +val fRULE_LIST : ct_RULE_LIST -> std_ppcmds;; +val fRULE : ct_RULE -> std_ppcmds;; +val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> std_ppcmds;; +val fPREMISES_LIST : ct_PREMISES_LIST -> std_ppcmds;; +val fID_LIST : ct_ID_LIST -> std_ppcmds;; +val fTEXT : ct_TEXT -> std_ppcmds;; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index df03a579..7d1f57fe 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -15,12 +15,6 @@ open Libnames;; open Goptions;; -let in_coq_ref = ref false;; - -let declare_in_coq () = in_coq_ref:=true;; - -let in_coq () = !in_coq_ref;; - (* // Verify whether this is dead code, as of coq version 7 *) (* The following three sentences have been added to cope with a change of strategy from the Coq team in the way rules construct ast's. The @@ -203,6 +197,10 @@ let xlate_int_or_var_opt_to_int_opt = function | Some (ArgVar _) -> xlate_error "int_or_var: TODO" | None -> CT_coerce_NONE_to_INT_OPT CT_none +let apply_or_by_notation f = function + | AN x -> f x + | ByNotation _ -> xlate_error "TODO: ByNotation" + let tac_qualid_to_ct_ID ref = CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref))) @@ -307,14 +305,10 @@ let make_fix_struct (n,bl) = let names = names_of_local_assums bl in let nn = List.length names in if nn = 1 || n = None then ctv_ID_OPT_NONE - else - let n = out_some n in - if n < nn then xlate_id_opt(List.nth names n) - else xlate_error "unexpected result of parsing for Fixpoint";; - + else ctf_ID_OPT_SOME(CT_ident (string_of_id (snd (Option.get n))));; let rec xlate_binder = function - (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) + (l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) and xlate_return_info = function | (Some Anonymous, None) | (None, None) -> CT_coerce_NONE_to_RETURN_INFO CT_none @@ -327,7 +321,7 @@ and xlate_formula_opt = | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e) and xlate_binder_l = function - LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) + LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) | LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n, xlate_formula v)) and @@ -336,7 +330,7 @@ and | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, List.map xlate_match_pattern l) and translate_one_equation = function - (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a) + (_,[_,lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a) | _ -> xlate_error "TODO: disjunctive multiple patterns" and xlate_binder_ne_list = function @@ -379,8 +373,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function (xlate_formula f, List.map xlate_formula_expl l')) | CApp(_, (_,f), l) -> CT_appc(xlate_formula f, xlate_formula_expl_ne_list l) - | CCases (_, _, [], _) -> assert false - | CCases (_, ret_type, tm::tml, eqns)-> + | CCases (_, _, _, [], _) -> assert false + | CCases (_, _, ret_type, tm::tml, eqns)-> CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm, List.map xlate_matched_formula tml), xlate_formula_opt ret_type, @@ -418,23 +412,16 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s)) | CPatVar (_, (true, s)) -> xlate_error "Second order variable not supported" - | CEvar (_, _) -> xlate_error "CEvar not supported" + | CEvar _ -> xlate_error "CEvar not supported" | CCoFix (_, (_, id), lm::lmi) -> - let strip_mutcorec (fid, bl,arf, ardef) = + let strip_mutcorec ((_, fid), bl,arf, ardef) = CT_cofix_rec (xlate_ident fid, xlate_binder_list bl, xlate_formula arf, xlate_formula ardef) in CT_cofixc(xlate_ident id, (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))) | CFix (_, (_, id), lm::lmi) -> - let strip_mutrec (fid, (n, ro), bl, arf, ardef) = - let (struct_arg,bl,arf,ardef) = - (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) - (* By the way, how could [bl = []] happen in V8 syntax ? *) - if bl = [] then - let n = out_some n in - let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in - (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef) - else (make_fix_struct (n, bl),bl,arf,ardef) in + let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) = + let struct_arg = make_fix_struct (n, bl) in let arf = xlate_formula arf in let ardef = xlate_formula ardef in match xlate_binder_list bl with @@ -461,7 +448,7 @@ and xlate_matched_formula = function CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f) and xlate_formula_expl = function (a, None) -> xlate_formula a - | (a, Some (_,ExplByPos i)) -> + | (a, Some (_,ExplByPos (i, _))) -> xlate_error "explicitation of implicit by rank not supported" | (a, Some (_,ExplByName i)) -> CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a) @@ -477,24 +464,31 @@ let (xlate_ident_or_metaid: AI (_, x) -> xlate_ident x | MetaId(_, x) -> CT_metaid x;; +let nums_of_occs (b,nums) = + if b then nums + else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums + let xlate_hyp = function | AI (_,id) -> xlate_ident id | MetaId _ -> xlate_error "MetaId should occur only in quotations" let xlate_hyp_location = function - | (nums, AI (_,id)), InHypTypeOnly -> - CT_intype(xlate_ident id, nums_or_var_to_int_list nums) - | (nums, AI (_,id)), InHypValueOnly -> - CT_invalue(xlate_ident id, nums_or_var_to_int_list nums) - | ([], AI (_,id)), InHyp -> + | (occs, AI (_,id)), InHypTypeOnly -> + CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) + | (occs, AI (_,id)), InHypValueOnly -> + CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) + | (occs, AI (_,id)), InHyp when occs = all_occurrences_expr -> CT_coerce_UNFOLD_to_HYP_LOCATION (CT_coerce_ID_to_UNFOLD (xlate_ident id)) - | (a::l, AI (_,id)), InHyp -> + | ((_,a::l as occs), AI (_,id)), InHyp -> + let nums = nums_of_occs occs in + let a = List.hd nums and l = List.tl nums in CT_coerce_UNFOLD_to_HYP_LOCATION (CT_unfold_occ (xlate_ident id, CT_int_ne_list(num_or_var_to_int a, nums_or_var_to_int_list_aux l))) + | (_, AI (_,id)), InHyp -> xlate_error "Unused" (* (true,]) *) | (_, MetaId _),_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" @@ -507,7 +501,7 @@ let xlate_clause cls = | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in CT_clause (hyps_info, - if cls.onconcl then + if cls.concl_occs <> no_occurrences_expr then CT_coerce_STAR_to_STAR_OPT CT_star else CT_coerce_NONE_to_STAR_OPT CT_none) @@ -606,14 +600,15 @@ let strip_targ_intropatt = | _ -> xlate_error "strip_targ_intropatt";; let get_flag r = - let conv_flags, red_ids = + let conv_flags, red_ids = + let csts = List.map (apply_or_by_notation tac_qualid_to_ct_ID) r.rConst in if r.rDelta then - [CT_delta], CT_unfbut (List.map tac_qualid_to_ct_ID r.rConst) + [CT_delta], CT_unfbut csts else (if r.rConst = [] then (* probably useless: just for compatibility *) [] else [CT_delta]), - CT_unf (List.map tac_qualid_to_ct_ID r.rConst) in + CT_unf csts in let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in @@ -633,6 +628,8 @@ let rec xlate_intro_pattern = | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" ) | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c) | IntroAnonymous -> xlate_error "TODO: IntroAnonymous" + | IntroFresh _ -> xlate_error "TODO: IntroFresh" + | IntroRewrite _ -> xlate_error "TODO: IntroRewrite" let compute_INV_TYPE = function FullInversionClear -> CT_inv_clear @@ -663,7 +660,8 @@ let xlate_largs_to_id_opt largs = | _ -> assert false;; let xlate_int_or_constr = function - ElimOnConstr a -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a) + ElimOnConstr (a,NoBindings) -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a) + | ElimOnConstr _ -> xlate_error "TODO: ElimOnConstr with bindings" | ElimOnIdent(_,i) -> CT_coerce_ID_OR_INT_to_FORMULA_OR_INT (CT_coerce_ID_to_ID_OR_INT(xlate_ident i)) @@ -676,9 +674,13 @@ let xlate_using = function | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);; let xlate_one_unfold_block = function - ([],qid) -> CT_coerce_ID_to_UNFOLD(tac_qualid_to_ct_ID qid) - | (n::nums, qid) -> - CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_or_var_to_int_ne_list n nums) + ((true,[]),qid) -> + CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid) + | (((_,_::_) as occs), qid) -> + let l = nums_of_occs occs in + CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, + nums_or_var_to_int_ne_list (List.hd l) (List.tl l)) + | ((false,[]), qid) -> xlate_error "Unused" ;; let xlate_with_names = function @@ -739,7 +741,8 @@ and xlate_red_tactic = | CbvVm -> CT_cbvvm | Hnf -> CT_hnf | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE - | Simpl (Some (l,c)) -> + | Simpl (Some (occs,c)) -> + let l = nums_of_occs occs in CT_simpl (CT_coerce_PATTERN_to_PATTERN_OPT (CT_pattern_occ @@ -758,9 +761,9 @@ and xlate_red_tactic = | Fold formula_list -> CT_fold(CT_formula_list(List.map xlate_formula formula_list)) | Pattern l -> - let pat_list = List.map (fun (nums,c) -> + let pat_list = List.map (fun (occs,c) -> CT_pattern_occ - (CT_int_list (nums_or_var_to_int_list_aux nums), + (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)), xlate_formula c)) l in (match pat_list with | first :: others -> CT_pattern (CT_pattern_ne_list (first, others)) @@ -770,21 +773,23 @@ and xlate_red_tactic = and xlate_local_rec_tac = function (* TODO LATER: local recursive tactics and global ones should be handled in the same manner *) - | ((_,x),(argl,tac)) -> + | ((_,x),Tacexp (TacFun (argl,tac))) -> let fst, rest = xlate_largs_to_id_opt argl in CT_rec_tactic_fun(xlate_ident x, CT_id_opt_ne_list(fst, rest), xlate_tactic tac) + | _ -> xlate_error "TODO: more general argument of 'let rec in'" and xlate_tactic = function | TacFun (largs, t) -> let fst, rest = xlate_largs_to_id_opt largs in CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t) - | TacThen (t1,t2) -> + | 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])) + | TacThen _ -> xlate_error "TacThen generalization TODO" | TacThens(t1,[]) -> assert false | TacThens(t1,t::l) -> let ct = xlate_tactic t in @@ -831,36 +836,31 @@ and xlate_tactic = | TacMatchContext (false,true,rule1::rules) -> CT_match_context_reverse(xlate_context_rule rule1, List.map xlate_context_rule rules) - | TacLetIn (l, t) -> + | TacLetIn (false, l, t) -> let cvt_clause = function - ((_,s),None,ConstrMayEval v) -> + ((_,s),ConstrMayEval v) -> CT_let_clause(xlate_ident s, CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_DEF_BODY_to_LET_VALUE (formula_to_def_body v)) - | ((_,s),None,Tacexp t) -> + | ((_,s),Tacexp t) -> CT_let_clause(xlate_ident s, CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_TACTIC_COM_to_LET_VALUE (xlate_tactic t)) - | ((_,s),None,t) -> + | ((_,s),t) -> CT_let_clause(xlate_ident s, CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_TACTIC_COM_to_LET_VALUE - (xlate_call_or_tacarg t)) - | ((_,s),Some c,t) -> - CT_let_clause(xlate_ident s, - CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c), - CT_coerce_TACTIC_COM_to_LET_VALUE - (xlate_call_or_tacarg t)) in + (xlate_call_or_tacarg t)) in let cl_l = List.map cvt_clause l in (match cl_l with | [] -> assert false | fst::others -> CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t)) - | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition" - | TacLetRecIn(f1::l, t) -> + | TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition" + | TacLetIn(true, f1::l, t) -> let tl = CT_rec_tactic_fun_list (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in CT_rec_tactic_in(tl, xlate_tactic t) @@ -917,6 +917,7 @@ and xlate_tac = | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b) | TacChange (Some(l,c), f, b) -> (* TODO LATER: combine with other constructions of pattern_occ *) + let l = nums_of_occs l in CT_change_local( CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), xlate_formula c), @@ -946,18 +947,22 @@ and xlate_tac = xlate_error "TODO: injection as" | TacFix (idopt, n) -> CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list []) - | TacMutualFix (id, n, fixtac_list) -> + | TacMutualFix (false, id, n, fixtac_list) -> let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in CT_fixtactic (ctf_ID_OPT_SOME (xlate_ident id), CT_int n, CT_fix_tac_list (List.map f fixtac_list)) + | TacMutualFix (true, id, n, fixtac_list) -> + xlate_error "TODO: non user-visible fix" | TacCofix idopt -> CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list []) - | TacMutualCofix (id, cofixtac_list) -> + | TacMutualCofix (false, id, cofixtac_list) -> let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in CT_cofixtactic (CT_coerce_ID_to_ID_OPT (xlate_ident id), CT_cofix_tac_list (List.map f cofixtac_list)) + | TacMutualCofix (true, id, cofixtac_list) -> + xlate_error "TODO: non user-visible cofix" | TacIntrosUntil (NamedHyp id) -> CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id)) | TacIntrosUntil (AnonHyp n) -> @@ -975,10 +980,12 @@ and xlate_tac = | TacIntroMove (Some id, None) -> CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)]) | TacIntroMove (None, None) -> CT_intro (CT_coerce_NONE_to_ID_OPT CT_none) - | TacLeft bindl -> CT_left (xlate_bindings bindl) - | TacRight bindl -> CT_right (xlate_bindings bindl) - | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl) - | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl) + | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl) + | TacRight (false,bindl) -> CT_right (xlate_bindings bindl) + | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl) + | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl) + | TacSplit _ | TacRight _ | TacLeft _ -> + xlate_error "TODO: esplit, eright, etc" | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) -> let c1 = xlate_formula (out_gen rawwit_constr c1) in let c2 = xlate_formula (out_gen rawwit_constr c2) in @@ -991,7 +998,7 @@ and xlate_tac = let cl_as_xlate_arg = {cl_as_clause with Tacexpr.onhyps = - option_map + Option.map (fun l -> List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l ) @@ -1009,12 +1016,15 @@ and xlate_tac = CT_coerce_TACTIC_COM_to_TACTIC_OPT tac in CT_replace_with (c1, c2,cl,tac_opt) - | TacRewrite(b,cbindl,cl) -> + | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) -> let cl = xlate_clause cl and c = xlate_formula (fst cbindl) and bindl = xlate_bindings (snd cbindl) in if b then CT_rewrite_lr (c, bindl, cl) else CT_rewrite_rl (c, bindl, cl) + | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by" + | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once" + | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite" | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) -> let t = out_gen rawwit_main_tactic t in let b = out_gen Extraargs.rawwit_orient b in @@ -1127,10 +1137,9 @@ and xlate_tac = (match out_gen rawwit_int_or_var n with | ArgVar _ -> xlate_error "" | ArgArg n -> CT_prolog (CT_formula_list cl, CT_int n)) - | TacExtend (_,"eapply", [cbindl]) -> - let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in - let c = xlate_formula c and bindl = xlate_bindings bindl in - CT_eapply (c, bindl) + (* eapply now represented by TacApply (true,cbindl) + | TacExtend (_,"eapply", [cbindl]) -> +*) | TacTrivial ([],Some []) -> CT_trivial | TacTrivial ([],None) -> CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star) @@ -1141,25 +1150,36 @@ and xlate_tac = xlate_error "TODO: trivial using" | TacReduce (red, l) -> CT_reduce (xlate_red_tactic red, xlate_clause l) - | TacApply (c,bindl) -> + | TacApply (true,false,(c,bindl)) -> CT_apply (xlate_formula c, xlate_bindings bindl) - | TacConstructor (n_or_meta, bindl) -> + | TacApply (true,true,(c,bindl)) -> + CT_eapply (xlate_formula c, xlate_bindings bindl) + | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply" + | TacConstructor (false,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) + | TacConstructor _ -> xlate_error "TODO: econstructor" | TacSpecialize (nopt, (c,sl)) -> CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl) | TacGeneralize [] -> xlate_error "" - | TacGeneralize (first :: cl) -> + | TacGeneralize ((((true,[]),first),Anonymous) :: cl) + when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr + & na = Anonymous) cl -> CT_generalize - (CT_formula_ne_list (xlate_formula first, List.map xlate_formula cl)) + (CT_formula_ne_list (xlate_formula first, + List.map (fun ((_,c),_) -> xlate_formula c) cl)) + | TacGeneralize _ -> xlate_error "TODO: Generalize at and as" | TacGeneralizeDep c -> CT_generalize_dependent (xlate_formula c) | TacElimType c -> CT_elim_type (xlate_formula c) | TacCaseType c -> CT_case_type (xlate_formula c) - | TacElim ((c1,sl), u) -> + | TacElim (false,(c1,sl), u) -> CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u) - | TacCase (c1,sl) -> + | TacCase (false,(c1,sl)) -> CT_casetac (xlate_formula c1, xlate_bindings sl) + | TacElim (true,_,_) | TacCase (true,_) + | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) -> + xlate_error "TODO: eelim, ecase, edestruct, einduction" | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h) | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h) | TacCut c -> CT_cut (xlate_formula c) @@ -1167,8 +1187,8 @@ and xlate_tac = | TacDecompose ([],c) -> xlate_error "Decompose : empty list of identifiers?" | TacDecompose (id::l,c) -> - let id' = tac_qualid_to_ct_ID id in - let l' = List.map tac_qualid_to_ct_ID l in + let id' = apply_or_by_notation tac_qualid_to_ct_ID id in + let l' = List.map (apply_or_by_notation tac_qualid_to_ct_ID) l in CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c) | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c) | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c) @@ -1178,6 +1198,7 @@ and xlate_tac = let idl' = List.map xlate_hyp idl in CT_clear (CT_id_ne_list (xlate_hyp id, idl')) | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'" + | TacRevert _ -> xlate_error "TODO: revert" | (*For translating tactics/Inv.v *) TacInversion (NonDepInversion (k,idl,l),quant_hyp) -> CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp, @@ -1192,30 +1213,36 @@ and xlate_tac = CT_use_inversion (id, xlate_formula c, CT_id_list (List.map xlate_hyp idlist)) | TacExtend (_,"omega", []) -> CT_omega - | TacRename (id1, id2) -> CT_rename(xlate_hyp id1, xlate_hyp id2) + | TacRename [id1, id2] -> CT_rename(xlate_hyp id1, xlate_hyp id2) + | TacRename _ -> xlate_error "TODO: add support for n-ary rename" | TacClearBody([]) -> assert false | TacClearBody(a::l) -> CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l)) - | TacDAuto (a, b) -> + | TacDAuto (a, b, []) -> CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) - | TacNewDestruct(a,b,c) -> - CT_new_destruct (* Julien F. : est-ce correct *) + | TacDAuto (a, b, _) -> + xlate_error "TODO: dauto using" + | TacNewDestruct(false,a,b,c,None) -> + CT_new_destruct (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) - | TacNewInduction(a,b,c) -> - CT_new_induction (* Pierre C. : est-ce correct *) + | TacNewInduction(false,a,b,c,None) -> + CT_new_induction (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) + | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in" + | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in" (*| TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, assert false) *) - | TacLetTac (na, c, cl) when cl = nowhere -> + | TacLetTac (na, c, cl, true) when cl = nowhere -> CT_pose(xlate_id_opt_aux na, xlate_formula c) - | TacLetTac (na, c, cl) -> + | TacLetTac (na, c, cl, true) -> CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, (* TODO LATER: This should be shared with Unfold, but the structures are different *) xlate_clause cl) + | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember" | TacAssert (None, IntroIdentifier id, c) -> CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c) | TacAssert (None, IntroAnonymous, c) -> @@ -1226,16 +1253,18 @@ and xlate_tac = CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c) | TacAssert _ -> xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'" - | TacAnyConstructor(Some tac) -> + | TacAnyConstructor(false,Some tac) -> CT_any_constructor (CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac)) - | TacAnyConstructor(None) -> + | TacAnyConstructor(false,None) -> CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none) + | TacAnyConstructor _ -> xlate_error "TODO: econstructor" | TacExtend(_, "ring", [args]) -> CT_ring (CT_formula_list (List.map xlate_formula (out_gen (wit_list0 rawwit_constr) args))) + | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal" | TacExtend (_,id, l) -> print_endline ("Extratactics : "^ id); CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l)) @@ -1299,7 +1328,7 @@ and coerce_genarg_to_TARG x = (snd (out_gen (rawwit_open_constr_gen b) x)))) | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> - let n = out_some (Pcoq.tactic_genarg_level s) in + let n = Option.get (Pcoq.tactic_genarg_level s) in let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in CT_coerce_TACTIC_COM_to_TARG t | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" @@ -1392,7 +1421,7 @@ let coerce_genarg_to_VARG x = | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> - let n = out_some (Pcoq.tactic_genarg_level s) in + let n = Option.get (Pcoq.tactic_genarg_level s) in let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t) | OpenConstrArgType _ -> xlate_error "TODO: generic open constr" @@ -1563,7 +1592,9 @@ let rec xlate_module_type = function | CWith_Module((_, idl), (_, qid)) -> CT_module_type_with_mod(mty1, CT_id_list (List.map xlate_ident idl), - CT_ident (xlate_qualid qid)));; + CT_ident (xlate_qualid qid))) + | CMTEapply (_,_) -> xlate_error "TODO: Funsig application";; + let xlate_module_binder_list (l:module_binder list) = CT_module_binder_list @@ -1596,8 +1627,8 @@ let rec xlate_vernac = | VernacDeclareTacticDefinition (true, tacs) -> (match List.map (function - ((_, id), body) -> - CT_tac_def(CT_ident (string_of_id id), xlate_tactic body)) + (id, _, body) -> + CT_tac_def(reference_to_ct_ID id, xlate_tactic body)) tacs with [] -> assert false | fst::tacs1 -> @@ -1714,7 +1745,7 @@ let rec xlate_vernac = CT_id_ne_list(n1, names), dblist) | HintsExtern (n, c, t) -> CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist) - | HintsResolve l | HintsImmediate l -> + | HintsImmediate l -> let f1, formulas = match List.map xlate_formula l with a :: tl -> a, tl | _ -> failwith "" in @@ -1731,6 +1762,23 @@ let rec xlate_vernac = HintsResolve _ -> CT_hints_resolve(l', dblist) | HintsImmediate _ -> CT_hints_immediate(l', dblist) | _ -> assert false) + | HintsResolve l -> + let f1, formulas = match List.map xlate_formula (List.map snd l) with + a :: tl -> a, tl + | _ -> failwith "" in + let l' = CT_formula_ne_list(f1, formulas) in + if local then + (match h with + HintsResolve _ -> + CT_local_hints_resolve(l', dblist) + | HintsImmediate _ -> + CT_local_hints_immediate(l', dblist) + | _ -> assert false) + else + (match h with + HintsResolve _ -> CT_hints_resolve(l', dblist) + | HintsImmediate _ -> CT_hints_immediate(l', dblist) + | _ -> assert false) | HintsUnfold l -> let n1, names = match List.map loc_qualid_to_ct_ID l with n1 :: names -> n1, names @@ -1766,13 +1814,11 @@ let rec xlate_vernac = ctf_ID_OPT_SOME (xlate_ident s)) | VernacEndProof Admitted -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE) - | VernacSetOpacity (false, id :: idl) -> - CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id, - List.map loc_qualid_to_ct_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" + | VernacSetOpacity (_,l) -> + CT_strategy(CT_level_list + (List.map (fun (l,q) -> + (level_to_ct_LEVEL l, + CT_id_list(List.map loc_qualid_to_ct_ID q))) l)) | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n)) | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt) | VernacShow ShowNode -> CT_show_node @@ -1799,7 +1845,7 @@ let rec xlate_vernac = | PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id) | PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id) | PrintModules -> CT_print_modules - | PrintGrammar (phylum, name) -> CT_print_grammar CT_grammar_none + | PrintGrammar name -> CT_print_grammar CT_grammar_none | PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star) | PrintHintDbName id -> CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id)) @@ -1819,6 +1865,12 @@ let rec xlate_vernac = CT_print_path (xlate_class id1, xlate_class id2) | PrintCanonicalConversions -> xlate_error "TODO: Print Canonical Structures" + | PrintAssumptions _ -> + xlate_error "TODO: Print Needed Assumptions" + | PrintInstances _ -> + xlate_error "TODO: Print Instances" + | PrintTypeClasses -> + xlate_error "TODO: Print TypeClasses" | PrintInspect n -> CT_inspect (CT_int n) | PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s) | PrintSetoids -> CT_print_setoids @@ -1837,12 +1889,14 @@ let rec xlate_vernac = | VernacBeginSection (_,id) -> CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id)) | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id) - | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) -> + | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) -> CT_coerce_THEOREM_GOAL_to_COMMAND( CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s, xlate_binder_list bl, xlate_formula c)) + | VernacStartTheoremProof _ -> + xlate_error "TODO: Mutually dependent theorems" | VernacSuspend -> CT_suspend - | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt)) + | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt)) | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) -> CT_coerce_THEOREM_GOAL_to_COMMAND (CT_theorem_goal @@ -1853,8 +1907,9 @@ let rec xlate_vernac = (xlate_defn kind, xlate_ident s, xlate_binder_list bl, cvt_optional_eval_for_definition c red_option, xlate_formula_opt typ_opt) - | VernacAssumption (kind, b) -> - CT_variable (xlate_var kind, cvt_vernac_binders b) + | VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline" + (*inline : bool -> automatic delta reduction at fonctor application*) + (* CT_variable (xlate_var kind, cvt_vernac_binders b)*) | VernacCheckMayEval (None, numopt, c) -> CT_check (xlate_formula c) | VernacSearch (s,x) -> @@ -1884,7 +1939,7 @@ let rec xlate_vernac = (_, (add_coercion, (_,s)), binders, c1, rec_constructor_or_none, field_list) -> let record_constructor = - xlate_ident_opt (option_map snd rec_constructor_or_none) in + xlate_ident_opt (Option.map snd rec_constructor_or_none) in CT_record ((if add_coercion then CT_coercion_atm else CT_coerce_NONE_to_COERCION_OPT(CT_none)), @@ -1902,15 +1957,8 @@ let rec xlate_vernac = (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi)) | VernacFixpoint ([],_) -> xlate_error "mutual recursive" | VernacFixpoint ((lm :: lmi),boxed) -> - let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) = - let (struct_arg,bl,arf,ardef) = - (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) - (* By the way, how could [bl = []] happen in V8 syntax ? *) - if bl = [] then - let n = out_some n in - let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in - (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef) - else (make_fix_struct (n, bl),bl,arf,ardef) in + let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) = + let struct_arg = make_fix_struct (n, bl) in let arf = xlate_formula arf in let ardef = xlate_formula ardef in match xlate_binder_list bl with @@ -1922,26 +1970,35 @@ let rec xlate_vernac = (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi)) | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive" | VernacCoFixpoint ((lm :: lmi),boxed) -> - let strip_mutcorec ((fid, bl, arf, ardef), _ntn) = + let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) = CT_cofix_rec (xlate_ident fid, xlate_binder_list bl, xlate_formula arf, xlate_formula ardef) in CT_cofix_decl (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)) | VernacScheme [] -> xlate_error "induction scheme" | VernacScheme (lm :: lmi) -> - let strip_ind ((_,id), depstr, inde, sort) = + let strip_ind = function + | (Some (_,id), InductionScheme (depstr, inde, sort)) -> CT_scheme_spec (xlate_ident id, xlate_dep depstr, CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), - xlate_sort sort) in + xlate_sort sort) + | (None, InductionScheme (depstr, inde, sort)) -> + CT_scheme_spec + (xlate_ident (id_of_string ""), xlate_dep depstr, + CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), + xlate_sort sort) + | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) - | VernacSyntacticDefinition (id, c, false, _) -> + | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" + | VernacSyntacticDefinition ((_,id), ([],c), false, _) -> CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None) - | VernacSyntacticDefinition (id, c, true, _) -> - xlate_error "TODO: Local abbreviations" + | VernacSyntacticDefinition ((_,id), _, _, _) -> + xlate_error"TODO: Local abbreviations and abbreviations with parameters" (* Modules and Module Types *) - | VernacDeclareModuleType((_, id), bl, mty_o) -> + | VernacInclude (_) -> xlate_error "TODO : Include " + | VernacDeclareModuleType((_, id), bl, mty_o) -> CT_module_type_decl(xlate_ident id, xlate_module_binder_list bl, match mty_o with @@ -2051,6 +2108,12 @@ let rec xlate_vernac = | Local -> CT_local in CT_coercion (local_opt, id_opt, xlate_ident id1, xlate_class id2, xlate_class id3) + + (* Type Classes *) + | VernacDeclareInstance _|VernacContext _| + VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) -> + xlate_error "TODO: Type Classes commands" + | VernacResetName id -> CT_reset (xlate_ident (snd id)) | VernacResetInitial -> CT_restore_state (CT_ident "Initial") | VernacExtend (s, l) -> @@ -2073,10 +2136,10 @@ let rec xlate_vernac = CT_coerce_ID_LIST_to_ID_LIST_OPT (CT_id_list (List.map - (function ExplByPos x + (function ExplByPos (x,_), _, _ -> xlate_error "explication argument by rank is obsolete" - | ExplByName id -> CT_ident (string_of_id id)) l))) + | ExplByName id, _, _ -> CT_ident (string_of_id id)) l))) | VernacDeclareImplicits(false, id, opt_positions) -> xlate_error "TODO: Implicit Arguments Global" | VernacReserve((_,a)::l, f) -> @@ -2096,13 +2159,15 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_set_option(table1) | VernacSetOption (table, v) -> let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in let value = match v with | BoolValue _ -> assert false @@ -2115,7 +2180,8 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_unset_option(table1) | VernacAddOption (table, l) -> let values = @@ -2130,7 +2196,8 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1)) | VernacImport(true, a::l) -> CT_export_id(CT_id_ne_list(reference_to_ct_ID a, @@ -2140,13 +2207,17 @@ let rec xlate_vernac = List.map reference_to_ct_ID l)) | VernacImport(_, []) -> assert false | VernacProof t -> CT_proof_with(xlate_tactic t) - | VernacVar _ -> xlate_error "Grammar vernac obsolete" | (VernacGlobalCheck _|VernacPrintOption _| VernacMemOption (_, _)|VernacRemoveOption (_, _) | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _| VernacSolveExistential (_, _)|VernacCanonical _ | - VernacTacticNotation _) - -> xlate_error "TODO: vernac";; + VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _) + -> xlate_error "TODO: vernac" +and level_to_ct_LEVEL = function + Conv_oracle.Opaque -> CT_Opaque + | Conv_oracle.Level n -> CT_Level (CT_int n) + | Conv_oracle.Expand -> CT_Expand;; + let rec xlate_vernac_list = function diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli index bedb4ac8..2e2b95fe 100644 --- a/contrib/interface/xlate.mli +++ b/contrib/interface/xlate.mli @@ -6,4 +6,3 @@ val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;; val xlate_ident : Names.identifier -> ct_ID;; val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;; -val declare_in_coq : (unit -> unit);; |