diff options
| author | lmamane | 2007-01-10 15:44:44 +0000 |
|---|---|---|
| committer | lmamane | 2007-01-10 15:44:44 +0000 |
| commit | bce104e3bb510fb10df2ecddebb47514328f2b8d (patch) | |
| tree | 69b2d6f827128ec3a769f3af9e58ffd8a6670b22 /contrib/interface | |
| parent | fa49da538d1d65f34d7b7fd3c32e51ef7ff578a3 (diff) | |
Merge from Lionel Elie Mamane's private branch:
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not
recompile the whole standard library just because the coq binaries
got rebuilt.
- Infrastructure to change the object pretty-printers at runtime.
- Use that infrastructure to make coqtop-protocol with Pcoq trees and
Pcoq-protocol with pretty-printed terms possible in coq-interface.
- Make "Back(track)" into closed sections, modules and module types
"Just Workâ„¢".
- Modernise/generalise Pcoq protocol a bit, make some of its warts
optional.
- Implement "Show." in Pcoq mode.
- Add Rpow_def.vo to REALSBASEVO so that its dependencies are
computed (and used).
- "make revision" now handles GNU Arch / tla in addition to svn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/COPYRIGHT | 4 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml4 | 357 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.mli | 4 | ||||
| -rw-r--r-- | contrib/interface/parse.ml | 25 | ||||
| -rw-r--r-- | contrib/interface/translate.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/translate.mli | 1 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 1563 | ||||
| -rw-r--r-- | contrib/interface/vtp.mli | 27 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 | ||||
| -rw-r--r-- | contrib/interface/xlate.mli | 1 |
10 files changed, 1084 insertions, 907 deletions
diff --git a/contrib/interface/COPYRIGHT b/contrib/interface/COPYRIGHT index 2fb11c6bcf..ff567a5466 100644 --- a/contrib/interface/COPYRIGHT +++ b/contrib/interface/COPYRIGHT @@ -3,6 +3,7 @@ (* Coq support for the Pcoq Graphical Interface of Coq *) (* *) (* Copyright (C) 1999-2004 INRIA Sophia-Antipolis (Lemme team) *) +(* Copyright (C) 2006 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/centaur.ml4 b/contrib/interface/centaur.ml4 index 730e055b4e..30c96f939c 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -1,11 +1,23 @@ (*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 + *) + (*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 +55,7 @@ open Showproof;; open Showproof_ct;; open Tacexpr;; open Vernacexpr;; +open Printer;; let pcoq_started = ref None;; @@ -51,6 +64,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,6 +103,29 @@ 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 = @@ -97,14 +138,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 +173,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 +202,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 +247,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 +299,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 +339,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 @@ -491,19 +501,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 +525,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 +544,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 +596,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 +627,127 @@ 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 TACTIC EXTEND pbp | [ "pbp" ident_opt(idopt) natural_list(nl) ] -> @@ -635,7 +769,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 +782,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(); + Options.print_emacs := false; Pp.make_pp_nonemacs(); end;; @@ -681,3 +816,19 @@ 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 StopPcoqHistory +| [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ] +END diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli index b8c2d7dc71..f9e83b5e1e 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 0278a16cd5..b551b143c2 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 = diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml index 6e4782be09..559860b2fc 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 65d8331b2d..34841fc4b6 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 166a0cbf63..f55eee07d5 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,479 @@ 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; + 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 +592,98 @@ 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_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; + 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 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 +693,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 +750,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 +806,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 +902,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 +954,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 +979,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 +988,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 +1040,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 +1063,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 +1189,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 +1210,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 +1224,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 +1376,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 +1390,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 +1401,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; 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 +1841,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 +1935,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 fe30b317a7..d7bd8db53c 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 6019522929..5224190301 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 diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli index bedb4ac82b..2e2b95fe7d 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);; |