diff options
Diffstat (limited to 'contrib/interface')
-rw-r--r-- | contrib/interface/centaur.ml | 113 | ||||
-rw-r--r-- | contrib/interface/dad.ml | 2 | ||||
-rw-r--r-- | contrib/interface/debug_tac.ml | 38 | ||||
-rw-r--r-- | contrib/interface/name_to_ast.ml | 25 | ||||
-rw-r--r-- | contrib/interface/parse.ml | 113 | ||||
-rw-r--r-- | contrib/interface/showproof.ml | 2 | ||||
-rw-r--r-- | contrib/interface/showproof_ct.ml | 48 | ||||
-rw-r--r-- | contrib/interface/translate.ml | 9 |
8 files changed, 179 insertions, 171 deletions
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index eae99993f..00db51adf 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -54,11 +54,11 @@ set_flags := (function () -> (g_nat_syntax_flag := true; ()) else ());; -let guarded_force_eval_stream s = +let guarded_force_eval_stream (s : std_ppcmds) = let l = ref [] in let f elt = l:= elt :: !l in (try Stream.iter f s with - | _ -> f (sTR "error guarded_force_eval_stream")); + | _ -> f (Stream.next (str "error guarded_force_eval_stream"))); Stream.of_list (List.rev !l);; @@ -67,7 +67,7 @@ let rec string_of_path p = | i::p -> (string_of_int i)^" "^ (string_of_path p) ;; let print_path p = - output_results_nl [< 'sTR "Path:"; 'sTR (string_of_path p)>] + output_results_nl (str "Path:" ++ str (string_of_path p)) ;; let kill_proof_node index = @@ -83,7 +83,8 @@ let kill_proof_node index = (*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; 'iNT request_id; 'fNL >];; + fnl () ++ str "message" ++ fnl () ++ str message_name ++ fnl () ++ + int request_id ++ fnl ();; let ctf_acknowledge_command request_id command_count opt_exn = let goal_count, goal_index = @@ -94,14 +95,14 @@ let ctf_acknowledge_command request_id command_count opt_exn = g_count, (min g_count !current_goal_index) else (0, 0) in - [< ctf_header "acknowledge" request_id; - 'iNT command_count; 'fNL; - 'iNT goal_count; 'fNL; - 'iNT goal_index; 'fNL; - 'sTR !current_proof_name; 'fNL; - (match opt_exn with - Some e -> Errors.explain_exn e - | None -> [< >]); 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + (ctf_header "acknowledge" request_id ++ + int command_count ++ fnl () ++ + int goal_count ++ fnl () ++ + int goal_index ++ fnl () ++ + str !current_proof_name ++ fnl () ++ + (match opt_exn with + Some e -> Errors.explain_exn e + | None -> mt ()) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; let ctf_undoResults = ctf_header "undo_results";; @@ -116,35 +117,37 @@ let ctf_Location = ctf_header "location";; let ctf_StateMessage = ctf_header "state";; let ctf_PathGoalMessage () = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "single_goal"; 'fNL >];; + fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();; let ctf_GoalReqIdMessage = ctf_header "single_goal_state";; let ctf_NewStateMessage = ctf_header "fresh_state";; -let ctf_SavedMessage () = [< 'fNL; 'sTR "message"; 'fNL; 'sTR "saved"; 'fNL >];; +let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ str "saved" ++ fnl ();; let ctf_KilledMessage req_id ngoals = - [< ctf_header "killed" req_id; 'iNT ngoals; 'fNL >];; + ctf_header "killed" req_id ++ int ngoals ++ fnl ();; let ctf_AbortedAllMessage () = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "aborted_all"; 'fNL >];; + fnl () ++ str "message" ++ fnl () ++ str "aborted_all" ++ fnl ();; let ctf_AbortedMessage request_id na = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "aborted_proof"; 'fNL; 'iNT request_id; 'fNL; - 'sTR na; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + fnl () ++ str "message" ++ fnl () ++ str "aborted_proof" ++ fnl () ++ + int request_id ++ fnl () ++ + str na ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; let ctf_UserErrorMessage request_id stream = - let stream = guarded_force_eval_stream stream in - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "user_error"; 'fNL; 'iNT request_id; 'fNL; - stream; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + let stream = guarded_force_eval_stream stream in + fnl () ++ str "message" ++ fnl () ++ str "user_error" ++ fnl () ++ + int request_id ++ fnl () ++ + stream ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; let ctf_ResetInitialMessage () = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_initial"; 'fNL >];; + fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();; -let ctf_ResetIdentMessage request_id str = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_ident"; 'fNL; 'iNT request_id; 'fNL; - 'sTR str; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; +let ctf_ResetIdentMessage request_id s = + fnl () ++ str "message" ++ fnl () ++ str "reset_ident" ++ fnl () ++ int request_id ++ fnl () ++ + str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; type vtp_tree = | P_rl of ct_RULE_LIST @@ -175,7 +178,7 @@ 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; + msg stream; match vtp_tree with Some t -> print_tree t | None -> ();; @@ -184,7 +187,7 @@ let output_results_nl stream = let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> break_happened := true;())) in - mSGNL stream;; + msgnl stream;; let rearm_break () = @@ -216,7 +219,7 @@ let show_nth n = try let pf = proof_of_pftreestate (get_pftreestate()) in if (!text_proof_flag<>"off") then -(* errorlabstrm "debug" [< 'sTR "text printing unplugged" >]*) +(* errorlabstrm "debug" [< str "text printing unplugged" >]*) (if n=0 then output_results (ctf_TextMessage !global_request_id) (Some (P_text (show_proof !text_proof_flag []))) @@ -255,14 +258,14 @@ let add_search (global_reference:global_reference) assumptions cstr = CT_coerce_ID_to_FORMULA( CT_ident ("Error printing" ^ id_string))) in ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST - with e -> mSGNL [< 'sTR "add_search raised an exception" >]; raise e;; + with e -> msgnl (str "add_search raised an exception"); raise e;; let make_error_stream node_string = - [< 'sTR "The syntax of "; 'sTR node_string; - 'sTR " is inconsistent with the vernac interpreter entry" >];; + str "The syntax of " ++ str node_string ++ + str " is inconsistent with the vernac interpreter entry";; let ctf_EmptyGoalMessage id = - [< 'fNL; 'sTR "Empty Goal is a no-op. Fun oh fun."; 'fNL >];; + fnl () ++ str "Empty Goal is a no-op. Fun oh fun." ++ fnl ();; let print_check (ast, judg) = @@ -271,15 +274,17 @@ let print_check (ast, judg) = (try translate_constr (Global.env()) value with UserError(f,str) -> raise(UserError(f, - [< Ast.print_ast - (ast_of_constr true (Global.env()) value); - 'fNL; str >]))) in + Ast.print_ast + (ast_of_constr true (Global.env()) value) ++ + fnl () ++ str))) + in let type_ct_ast = (try translate_constr (Global.env()) typ with UserError(f,str) -> - raise(UserError(f, [< Ast.print_ast (ast_of_constr true (Global.env()) - value); - 'fNL; str >]))) in + raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env()) + value) ++ + fnl () ++ str))) + in ((ctf_SearchResults !global_request_id), (Some (P_pl (CT_premises_list @@ -318,16 +323,16 @@ let globcv = function let pbp_tac_pcoq = pbp_tac (function x -> output_results - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL; - 'iNT !global_request_id; 'fNL>] - (Some (P_t(xlate_tactic x))));; + (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++ + int !global_request_id ++ fnl ()) + (Some (P_t(xlate_tactic x))));; let dad_tac_pcoq = dad_tac(function x -> output_results - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL; - 'iNT !global_request_id; 'fNL >] + (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++ + int !global_request_id ++ fnl ()) (Some (P_t(xlate_tactic x))));; let search_output_results () = @@ -346,8 +351,8 @@ let debug_tac2_pcoq = function try let result = report_error ast the_goal the_ast the_path [] g in (errorlabstrm "DEBUG TACTIC" - [< 'sTR "no error here "; 'fNL; pr_goal (sig_it g); - 'fNL; 'sTR "the tactic is"; 'fNL ; Printer.gentacpr ast >]; + (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ + fnl () ++ str "the tactic is" ++ fnl () ++ Printer.gentacpr ast); result) with e -> @@ -481,9 +486,9 @@ let command_changes = [ begin if kind = "LETTOP" && not(refining ()) then errorlabstrm "StartProof" - [< 'sTR - "Let declarations can only be used in proof editing mode" - >]; + (str + "Let declarations can only be used in proof editing mode" + ); let str = (string_of_id s) in start_proof_com (Some s) stre c; History.start_proof str; @@ -563,7 +568,7 @@ let command_changes = [ (function () -> errorlabstrm "Begin Silent" - [< 'sTR "not available in Centaur mode" >]) + (str "not available in Centaur mode")) | _ -> errorlabstrm "BeginSilent" (make_error_stream "BeginSilent"))); ("EndSilent", @@ -572,7 +577,7 @@ let command_changes = [ (function () -> errorlabstrm "End Silent" - [< 'sTR "not available in Centaur mode" >]) + (str "not available in Centaur mode")) | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent"))); ("ABORT", @@ -633,7 +638,7 @@ let command_changes = [ (function () -> let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in output_results - [<'fNL; 'sTR "message"; 'fNL; 'sTR "PRINT_VALUE"; 'fNL >] + (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ()) (Some (P_cl results))) | _ -> errorlabstrm "PrintId" (make_error_stream "PrintId"))); @@ -646,7 +651,7 @@ let command_changes = [ match kind with | "CHECK" -> print_check | "PRINTTYPE" -> - errorlabstrm "PrintType" [< 'sTR "Not yet supported in CtCoq" >] + errorlabstrm "PrintType" (str "Not yet supported in CtCoq") | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK") in (function () -> let a,b = f (c, judgment_of_rawconstr evmap env c) in @@ -692,8 +697,8 @@ let command_changes = [ (fun () -> let results = dad_rule_names() in output_results - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "dad_rule_names"; 'fNL; - 'iNT !global_request_id; 'fNL >] + (fnl () ++ str "message" ++ fnl () ++ str "dad_rule_names" ++ fnl () ++ + int !global_request_id ++ fnl ()) (Some (P_ids (CT_id_list (List.map (fun s -> CT_ident s) results))))) diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 7f2ea95a4..ce3817404 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -254,7 +254,7 @@ vinterp_add "AddDadRule" let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com))) | _ -> errorlabstrm "AddDadRule1" - [< 'sTR "AddDadRule2">]); + [< str "AddDadRule2">]); add_dad_rule "distributivity-inv" (Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) [2; 2] diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml index b7542fa74..80d9d7201 100644 --- a/contrib/interface/debug_tac.ml +++ b/contrib/interface/debug_tac.ml @@ -183,7 +183,7 @@ and checked_thens: report_holder -> Coqast.t -> Coqast.t list -> tactic = | Recursive_fail tr -> Tree_fail tr | Fail -> Failed 1 | _ -> errorlabstrm "check_thens" - [< 'sTR "this case should not happen in check_thens">]):: + (str "this case should not happen in check_thens")):: !report_holder); result) @@ -297,8 +297,8 @@ let rec reconstruct_success_tac ast = | _ -> errorlabstrm "this error case should not happen on an unknown tactic" - [< 'sTR "error in reconstruction with "; 'fNL; - (gentacpr ast) >]);; + (str "error in reconstruction with " ++ fnl () ++ + (gentacpr ast)));; let rec path_to_first_error = function @@ -332,15 +332,16 @@ let debug_tac = function let clean_ast = expand_tactic ast in let report_tree = try List.hd !report with - Failure "hd" -> (mSGNL [< 'sTR "report is empty" >]; Failed 1) in + Failure "hd" -> (msgnl (str "report is empty"); Failed 1) in let success_tac = reconstruct_success_tac clean_ast report_tree in let compact_success_tac = flatten_then success_tac in - mSGNL [< 'fNL; 'sTR "========= Successful tactic ============="; - 'fNL; - gentacpr compact_success_tac; 'fNL; - 'sTR "========= End of successful tactic ============">]; + msgnl (fnl () ++ + str "========= Successful tactic =============" ++ + fnl () ++ + gentacpr compact_success_tac ++ fnl () ++ + str "========= End of successful tactic ============"); result) | _ -> error "wrong arguments for debug_tac";; @@ -427,10 +428,9 @@ let rec report_error with e -> if !the_count > 1 then - mSGNL - [< 'sTR "in branch no "; 'iNT !the_count; - 'sTR " after tactic "; - gentacpr a >]; + msgnl + (str "in branch no " ++ int !the_count ++ + str " after tactic " ++ gentacpr a); raise e) | Node(_, "TACTICLIST", a::b::c::tl) -> report_error (ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl)) @@ -458,16 +458,16 @@ let descr_first_error = function let the_path = ref ([] : int list) in try let result = report_error ast the_goal the_ast the_path [] g in - mSGNL [< 'sTR "no Error here" >]; + msgnl (str "no Error here"); result with e -> - (mSGNL [< 'sTR "Execution of this tactic raised message " ; 'fNL; - 'fNL; Errors.explain_exn e; 'fNL; - 'fNL; 'sTR "on goal" ; 'fNL; - pr_goal (sig_it (strip_some !the_goal)); 'fNL; - 'sTR "faulty tactic is"; 'fNL; 'fNL; - gentacpr (flatten_then !the_ast); 'fNL >]; + (msgnl (str "Execution of this tactic raised message " ++ fnl () ++ + fnl () ++ Errors.explain_exn e ++ fnl () ++ + fnl () ++ str "on goal" ++ fnl () ++ + pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++ + str "faulty tactic is" ++ fnl () ++ fnl () ++ + gentacpr (flatten_then !the_ast) ++ fnl ()); tclIDTAC g)) | _ -> error "wrong arguments for descr_first_error";; diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index e96106368..a7d5644f0 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -56,8 +56,8 @@ let impl_args_to_string = function let implicit_args_id_to_ast_list id l ast_list = (match impl_args_to_string l with None -> ast_list - | Some(s) -> (str("For " ^ (string_of_id id))):: - (str s):: + | Some(s) -> (string ("For " ^ (string_of_id id))):: + (string s):: ast_list);; (* This function construct an ast to enumerate the implicit positions for an @@ -125,7 +125,7 @@ let mutual_to_ast_list sp mib = Array.fold_right (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in (ope("MUTUALINDUCTIVE", - [str (if mib.mind_finite then "Inductive" else "CoInductive"); + [string (if mib.mind_finite then "Inductive" else "CoInductive"); ope("VERNACARGLIST", ast_list)]):: (implicit_args_to_ast_list sp mipv));; @@ -135,11 +135,11 @@ let constr_to_ast v = let implicits_to_ast_list implicits = (match (impl_args_to_string implicits) with None -> [] - | Some s -> [ope("COMMENT", [str s])]);; + | Some s -> [ope("COMMENT", [string s])]);; let make_variable_ast name typ implicits = (ope("VARIABLE", - [str "VARIABLE"; + [string "VARIABLE"; ope("BINDERLIST", [ope("BINDER", [(constr_to_ast (body_of_type typ)); @@ -148,7 +148,7 @@ let make_variable_ast name typ implicits = let make_definition_ast name c typ implicits = (ope("DEFINITION", - [str "DEFINITION"; + [string "DEFINITION"; nvar name; ope("COMMAND", [ope("CAST", @@ -193,8 +193,8 @@ let leaf_entry_to_ast_list (sp,lobj) = | (_, "INDUCTIVE") -> inductive_to_ast_list sp | (_, s) -> errorlabstrm - "print" [< 'sTR ("printing of unrecognized object " ^ - s ^ " has been required") >];; + "print" (str ("printing of unrecognized object " ^ + s ^ " has been required"));; @@ -232,10 +232,11 @@ let name_to_ast (qid:Nametab.qualid) = try let sp = Syntax_def.locate_syntactic_definition qid in errorlabstrm "print" - [< 'sTR "printing of syntax definitions not implemented" >] + (str "printing of syntax definitions not implemented") with Not_found -> errorlabstrm "print" - [< Nametab.pr_qualid qid; - 'sPC; 'sTR "not a defined object" >] in - ope("vernac_list", l);; + (Nametab.pr_qualid qid ++ + spc () ++ str "not a defined object") + in + ope("vernac_list", l);; diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 6b2e38873..fad5c1e34 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -2,10 +2,10 @@ open Util;; open System;; -open Pp;; - open Ctast;; +open Pp;; + open Library;; open Ascent;; @@ -43,15 +43,15 @@ let print_parse_results n msg = flush stdout;; let ctf_SyntaxErrorMessage reqid pps = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "syntax_error"; 'fNL; 'iNT reqid; 'fNL; - pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + (fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ int reqid ++ fnl () ++ + pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; let ctf_SyntaxWarningMessage reqid pps = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "syntax_warning"; 'fNL; 'iNT reqid; 'fNL; - pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + (fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ int reqid ++ fnl () ++ + pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; let ctf_FileErrorMessage reqid pps = - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "file_error"; 'fNL; 'iNT reqid; 'fNL; - pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + (fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ int reqid ++ fnl () ++ + pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; (*In the code for CoqV6.2, the require_module call is encapsulated in a function "without_mes_ambig". Here I have supposed that this @@ -60,7 +60,7 @@ let try_require_module import specif name fname = try Library.require_module (if specif = "UNSPECIFIED" then None else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT") with - | e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];; + | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");; let execute_when_necessary ast = (match ast with @@ -79,11 +79,12 @@ let execute_when_necessary ast = | _ -> ()); ast;; let parse_to_dot = - let rec dot = parser - [< '("", ".") >] -> () - | [< '("EOI", "") >] -> raise End_of_file - | [< '_; s >] -> dot s - in Gram.Entry.of_parser "Coqtoplevel.dot" dot;; + let rec dot st = match Stream.next st with + | ("", ".") -> () + | ("EOI", "") -> raise End_of_file + | _ -> dot st + in + Gram.Entry.of_parser "Coqtoplevel.dot" dot;; let rec discard_to_dot stream = try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with @@ -149,11 +150,11 @@ let parse_command_list reqid stream string_list = with | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> begin - mSGNL (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e)); + msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e)); try discard_to_dot stream; - mSGNL [< 'sTR "debug"; 'fNL; 'iNT this_pos; 'fNL; 'iNT - (Stream.count stream) >]; + msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ int + (Stream.count stream)); Some( Node(l, "PARSING_ERROR", List.map Ctast.str (get_substring_list string_list this_pos @@ -175,7 +176,7 @@ let parse_command_list reqid stream string_list = | None -> [] in match parse_whole_stream () with | first_one::tail -> (P_cl (CT_command_list(first_one, tail))) - | [] -> raise (UserError ("parse_string", [< 'sTR "empty text." >]));; + | [] -> raise (UserError ("parse_string", (str "empty text.")));; (*When parsing a string using a phylum, the string is first transformed into a Coq Ast using the regular Coq parser, then it is transformed into @@ -215,12 +216,12 @@ let parse_string_action reqid phylum char_stream string_list = with | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> flush_until_end_of_stream char_stream; - mSGNL (ctf_SyntaxErrorMessage reqid + msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")))) | e -> flush_until_end_of_stream char_stream; - mSGNL (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));; + msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));; let quiet_parse_string_action char_stream = @@ -247,10 +248,10 @@ let parse_file_action reqid file_name = this_ast with | Stdpp.Exc_located(l,Stream.Error txt ) -> - mSGNL (ctf_SyntaxWarningMessage reqid - [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL; + msgnl (ctf_SyntaxWarningMessage reqid + (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ Errors.explain_exn - (Stdpp.Exc_located(l,Stream.Error txt)) >]); + (Stdpp.Exc_located(l,Stream.Error txt)))); let rec discard_to_dot () = try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() @@ -276,18 +277,18 @@ let parse_file_action reqid file_name = | first_one :: tail -> print_parse_results reqid (P_cl (CT_command_list (first_one, tail))) - | [] -> raise (UserError ("parse_file_action", [< 'sTR "empty file." >])) + | [] -> raise (UserError ("parse_file_action", (str "empty file."))) with | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> - mSGNL + msgnl (ctf_SyntaxErrorMessage reqid - [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL; - Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")) >]) + (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ + Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")))) | e -> - mSGNL + msgnl (ctf_SyntaxErrorMessage reqid - [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL; - Errors.explain_exn e >]);; + (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ + Errors.explain_exn e));; (* This function is taken from Mltop.add_path *) @@ -297,7 +298,7 @@ let add_path dir coq_dirpath = Library.add_load_path_entry (dir,coq_dirpath) end else - wARNING [< 'sTR ("Cannot open " ^ dir) >] + msg_warning (str ("Cannot open " ^ dir)) let convert_string d = try Names.id_of_string d @@ -315,7 +316,7 @@ let add_rec_path dir coq_dirpath = List.iter Library.add_load_path_entry dirs end else - wARNING [< 'sTR ("Cannot open " ^ dir) >];; + msg_warning (str ("Cannot open " ^ dir));; let add_path_action reqid string_arg = let directory_name = glob string_arg in @@ -325,30 +326,30 @@ let add_path_action reqid string_arg = end;; let print_version_action () = - mSGNL [< >]; - mSGNL [< 'sTR "$Id$" >];; + msgnl (mt ()); + msgnl (str "$Id$");; let load_syntax_action reqid module_name = - mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >]; + msg (str "loading " ++ str module_name ++ str "... "); try (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in read_module qid; - mSG [< 'sTR "opening... ">]; + msg (str "opening... "); let fullname = Nametab.locate_loaded_library qid in import_module fullname; - mSGNL [< 'sTR "done"; 'fNL >]; + msgnl (str "done" ++ fnl ()); ()) with | UserError (label, pp_stream) -> (*This one may be necessary to make sure that the message won't be indented *) - mSGNL [< >]; - mSGNL - [< 'fNL; 'sTR "error while loading syntax module "; 'sTR module_name; - 'sTR ": "; 'sTR label; 'fNL; pp_stream >] + msgnl (mt ()); + msgnl + (fnl () ++ str "error while loading syntax module " ++ str module_name ++ + str ": " ++ str label ++ fnl () ++ pp_stream) | e -> - mSGNL [< >]; - mSGNL - [< 'fNL; 'sTR "message"; 'fNL; 'sTR "load_error"; 'fNL; 'iNT reqid; 'fNL >]; + msgnl (mt ()); + msgnl + (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ int reqid ++ fnl ()); ();; let coqparser_loop inchan = @@ -370,12 +371,12 @@ Libobject.relax true; if Sys.file_exists coqdir then coqdir else - (mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in + (msgnl (str "could not find the value of COQDIR"); exit 1) in begin add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]); add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]); add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]); - List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path()) + List.iter (fun a -> msgnl (str a)) (get_load_path()) end; (try (match create_entry (get_univ "nat") "number" ETast with @@ -387,10 +388,10 @@ Libobject.relax true; (fun s loc -> Node((0,0),"XTRA",[Str((0,0),"omega_integer_for_ctcoq"); Num((0,0),int_of_string s)]))]] - | _ -> mSGNL [< 'sTR "unpredicted behavior of Grammar.extend" >]) + | _ -> msgnl (str "unpredicted behavior of Grammar.extend")) with - e -> mSGNL [< 'sTR "could not add a parser for numbers" >]); + e -> msgnl (str "could not add a parser for numbers")); (let vernacrc = try Sys.getenv "VERNACRC" @@ -406,28 +407,28 @@ Libobject.relax true; with | End_of_file -> () | e -> - (mSGNL (Errors.explain_exn e); - mSGNL [< 'sTR "could not load the VERNACRC file" >]); + (msgnl (Errors.explain_exn e); + msgnl (str "could not load the VERNACRC file")); try - mSGNL [< 'sTR vernacrc >] + msgnl (str vernacrc) with e -> ()); (try let user_vernacrc = try Some(Sys.getenv "USERVERNACRC") with | Not_found as e -> - mSGNL [< 'sTR "no .vernacrc file" >]; None in + msgnl (str "no .vernacrc file"); None in (match user_vernacrc with Some f -> coqparser_loop (open_in f) | None -> ()) with | End_of_file -> () | e -> - mSGNL (Errors.explain_exn e); - mSGNL [< 'sTR "error in your .vernacrc file" >]); -mSGNL [< 'sTR "Starting Centaur Specialized Parser Loop" >]; + msgnl (Errors.explain_exn e); + msgnl (str "error in your .vernacrc file")); +msgnl (str "Starting Centaur Specialized Parser Loop"); try coqparser_loop stdin with | End_of_file -> () - | e -> mSGNL(Errors.explain_exn e)) + | e -> msgnl(Errors.explain_exn e)) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 5bfad2f52..c23394e8c 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1806,7 +1806,7 @@ let show_proof lang gpath = ;; let show_nproof path = - pP (sp_print (sph [spi; show_proof "fr" path]));; + pp (sp_print (sph [spi; show_proof "fr" path]));; vinterp_add "ShowNaturalProof" (fun _ -> diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml index e3bca2243..b689620e3 100644 --- a/contrib/interface/showproof_ct.ml +++ b/contrib/interface/showproof_ct.ml @@ -120,31 +120,31 @@ let sphv l = let rec prlist_with_sep f g l = match l with - [] -> hOV 0 [< >] - |x::l1 -> hOV 0 [< (g x); (f ()); (prlist_with_sep f g l1)>] + [] -> hov 0 (mt ()) + |x::l1 -> hov 0 ((g x) ++ (f ()) ++ (prlist_with_sep f g l1)) ;; let rec sp_print x = match x with - CT_coerce_ID_to_TEXT (CT_ident s) - -> (match s with - "\n" -> [< 'fNL >] - | "Retour chariot pour Show proof" -> [< 'fNL >] - |_ -> [< 'sTR s >]) - | CT_text_formula f -> [< prterm (Hashtbl.find ct_FORMULA_constr f) >] - | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove"); - CT_text_path (CT_signed_int_list p); - CT_coerce_ID_to_TEXT (CT_ident "goal"); - g] -> + | CT_coerce_ID_to_TEXT (CT_ident s) + -> (match s with + | "\n" -> fnl () + | "Retour chariot pour Show proof" -> fnl () + |_ -> str s) + | CT_text_formula f -> prterm (Hashtbl.find ct_FORMULA_constr f) + | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove"); + CT_text_path (CT_signed_int_list p); + CT_coerce_ID_to_TEXT (CT_ident "goal"); + g] -> let p=(List.map (fun y -> match y with (CT_coerce_INT_to_SIGNED_INT (CT_int x)) -> x | _ -> raise (Failure "sp_print")) p) in - h 0 [< 'sTR "<b>"; sp_print g; 'sTR "</b>">] + h 0 (str "<b>" ++ sp_print g ++ str "</b>") | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "uselemma"); CT_coerce_ID_to_TEXT (CT_ident intro); l;g] -> - h 0 [< 'sTR ("<i>("^intro^" "); sp_print l; 'sTR ")</i>"; sp_print g>] + h 0 (str ("<i>("^intro^" ") ++ sp_print l ++ str ")</i>" ++ sp_print g) | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp"); CT_text_path (CT_signed_int_list p); CT_coerce_ID_to_TEXT (CT_ident hyp); @@ -153,7 +153,7 @@ let rec sp_print x = (CT_coerce_INT_to_SIGNED_INT (CT_int x)) -> x | _ -> raise (Failure "sp_print")) p) in - h 0 [< 'sTR hyp>] + h 0 (str hyp) | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp_with_type"); CT_text_path (CT_signed_int_list p); @@ -163,23 +163,23 @@ let rec sp_print x = (CT_coerce_INT_to_SIGNED_INT (CT_int x)) -> x | _ -> raise (Failure "sp_print")) p) in - h 0 [< sp_print g; 'sPC; 'sTR "<i>("; 'sTR hyp;'sTR ")</i>">] + h 0 (sp_print g ++ spc () ++ str "<i>(" ++ str hyp ++ str ")</i>") | CT_text_h l -> - h 0 [< prlist_with_sep (fun () -> [< >]) - (fun y -> sp_print y) l>] + h 0 (prlist_with_sep (fun () -> mt ()) + (fun y -> sp_print y) l) | CT_text_v l -> - v 0 [< prlist_with_sep (fun () -> [< >]) - (fun y -> sp_print y) l>] + v 0 (prlist_with_sep (fun () -> mt ()) + (fun y -> sp_print y) l) | CT_text_hv l -> - h 0 [< prlist_with_sep (fun () -> [<>]) - (fun y -> sp_print y) l>] + h 0 (prlist_with_sep (fun () -> mt ()) + (fun y -> sp_print y) l) | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "shrink"); CT_text_op [CT_coerce_ID_to_TEXT (CT_ident info); t]] -> - h 0 [< 'sTR ("("^info^": "); sp_print t ;'sTR ")" >] + h 0 (str ("("^info^": ") ++ sp_print t ++ str ")") | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "root_of_text_proof"); t]-> sp_print t - | _ -> [< 'sTR "..." >] + | _ -> str "..." ;; diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml index 75cd7db38..c691ff912 100644 --- a/contrib/interface/translate.ml +++ b/contrib/interface/translate.ml @@ -56,12 +56,12 @@ let dbize_sp = | Invalid_argument _ | Failure _ -> anomaly_loc (loc, "Translate.dbize_sp (taken from Astterm)", - [< 'sTR "malformed section-path" >]) + [< str "malformed section-path" >]) end | ast -> anomaly_loc (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)", - [< 'sTR "not a section-path" >]);; + [< str "not a section-path" >]);; *) (* dead code: @@ -120,8 +120,9 @@ let translate_sign env = fold_named_context (fun env (id,v,c) l -> (CT_premise(CT_ident(string_of_id id), translate_constr env c))::l) - env [] in - CT_premises_list l;; + env ~init:[] + in + CT_premises_list l;; (* the function rev_and_compact performs two operations: 1- it reverses the list of integers given as argument |