aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/class.ml42
-rw-r--r--toplevel/command.ml50
-rw-r--r--toplevel/coqinit.ml8
-rw-r--r--toplevel/coqtop.ml8
-rw-r--r--toplevel/discharge.ml14
-rw-r--r--toplevel/errors.ml102
-rw-r--r--toplevel/fhimsg.ml248
-rw-r--r--toplevel/himsg.ml374
-rw-r--r--toplevel/metasyntax.ml4
-rw-r--r--toplevel/minicoq.ml20
-rw-r--r--toplevel/mltop.ml436
-rw-r--r--toplevel/protectedtoplevel.ml16
-rw-r--r--toplevel/record.ml26
-rwxr-xr-xtoplevel/recordobj.ml4
-rw-r--r--toplevel/toplevel.ml72
-rw-r--r--toplevel/vernac.ml4
-rw-r--r--toplevel/vernacentries.ml148
-rw-r--r--toplevel/vernacinterp.ml18
18 files changed, 598 insertions, 596 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 8ffb08c55..d9500b11d 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -87,29 +87,29 @@ exception CoercionError of coercion_error_kind
let explain_coercion_error g = function
| AlreadyExists ->
- [< Printer.pr_global g; 'sTR" is already a coercion" >]
+ (Printer.pr_global g ++ str" is already a coercion")
| NotAFunction ->
- [< Printer.pr_global g; 'sTR" is not a function" >]
+ (Printer.pr_global g ++ str" is not a function")
| NoSource ->
- [< Printer.pr_global g; 'sTR ": cannot find the source class" >]
+ (Printer.pr_global g ++ str ": cannot find the source class")
| NoSourceFunClass ->
- [< Printer.pr_global g; 'sTR ": FUNCLASS cannot be a source class" >]
+ (Printer.pr_global g ++ str ": FUNCLASS cannot be a source class")
| NoSourceSortClass ->
- [< Printer.pr_global g; 'sTR ": SORTCLASS cannot be a source class" >]
+ (Printer.pr_global g ++ str ": SORTCLASS cannot be a source class")
| NotUniform ->
- [< Printer.pr_global g;
- 'sTR" does not respect the inheritance uniform condition" >];
+ (Printer.pr_global g ++
+ str" does not respect the inheritance uniform condition");
| NoTarget ->
- [<'sTR"Cannot find the target class" >]
+ (str"Cannot find the target class")
| WrongTarget (clt,cl) ->
- [<'sTR"Found target class "; 'sTR(string_of_class cl);
- 'sTR " while "; 'sTR(string_of_class clt);
- 'sTR " is expected" >]
+ (str"Found target class " ++ str(string_of_class cl) ++
+ str " while " ++ str(string_of_class clt) ++
+ str " is expected")
| NotAClass ref ->
- [< 'sTR "Type of "; Printer.pr_global ref;
- 'sTR " does not end with a sort" >]
+ (str "Type of " ++ Printer.pr_global ref ++
+ str " does not end with a sort")
| NotEnoughClassArgs cl ->
- [< 'sTR"Wrong number of parameters for ";'sTR(string_of_class cl) >]
+ (str"Wrong number of parameters for " ++str(string_of_class cl))
(* Verifications pour l'ajout d'une classe *)
@@ -143,7 +143,7 @@ let try_add_class cl streopt fail_if_exists =
declare_class (cl,stre,p)
else
if fail_if_exists then errorlabstrm "try_add_new_class"
- [< 'sTR (string_of_class cl) ; 'sTR " is already a class" >]
+ (str (string_of_class cl) ++ str " is already a class")
(* Coercions *)
@@ -178,8 +178,8 @@ let class_of_ref = function
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
errorlabstrm "class_of_ref"
- [< 'sTR "Constructors, such as "; Printer.pr_global c;
- 'sTR " cannot be used as class" >]
+ (str "Constructors, such as " ++ Printer.pr_global c ++
+ str " cannot be used as class")
(*
lp est la liste (inverse'e) des arguments de la coercion
@@ -242,7 +242,7 @@ let get_strength stre ref cls clt =
let error_not_transparent source =
errorlabstrm "build_id_coercion"
- [< 'sTR ((string_of_class source)^" must be a transparent constant") >]
+ (str ((string_of_class source)^" must be a transparent constant"))
let build_id_coercion idf_opt source =
let env = Global.env () in
@@ -342,14 +342,14 @@ let try_add_new_coercion_subclass cl stre =
let coe_ref = build_id_coercion None cl in
try_add_new_coercion_core coe_ref stre (Some cl) None true
-let try_add_new_coercion_with_target ref stre source target =
+let try_add_new_coercion_with_target ref stre ~source ~target =
try_add_new_coercion_core ref stre (Some source) (Some target) false
-let try_add_new_identity_coercion id stre source target =
+let try_add_new_identity_coercion id stre ~source ~target =
let ref = build_id_coercion (Some id) source in
try_add_new_coercion_core ref stre (Some source) (Some target) true
-let try_add_new_coercion_with_source ref stre source =
+let try_add_new_coercion_with_source ref stre ~source =
try_add_new_coercion_core ref stre (Some source) None false
(* try_add_new_class : global_reference -> strength -> unit *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 400f12fa2..4a517144e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -70,7 +70,7 @@ let red_constant_entry ce = function
let declare_global_definition ident ce n local =
let sp = declare_constant ident (ConstantEntry ce,n) in
if local then
- wARNING [< pr_id ident; 'sTR" is declared as a global definition" >];
+ msg_warning (pr_id ident ++ str" is declared as a global definition");
if_verbose message ((string_of_id ident) ^ " is defined");
ConstRef sp
@@ -85,15 +85,15 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
let sp = declare_variable ident (Lib.cwd(), c, n) in
if_verbose message ((string_of_id ident) ^ " is defined");
if Pfedit.refining () then
- mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident;
- 'sTR" is not visible from current goals" >];
+ msgerrnl (str"Warning: Local definition " ++ pr_id ident ++
+ str" is not visible from current goals");
VarRef ident
end
else
declare_global_definition ident ce' n true
| NotDeclare ->
anomalylabstrm "Command.definition_body_red"
- [<'sTR "Strength NotDeclare not for Definition, only for Let" >]
+ (str "Strength NotDeclare not for Definition, only for Let")
let definition_body = definition_body_red None
@@ -112,8 +112,8 @@ let parameter_def_var ident c =
let declare_global_assumption ident c =
let sp = parameter_def_var ident c in
- wARNING [< pr_id ident; 'sTR" is declared as a parameter";
- 'sTR" because it is at a global level" >];
+ msg_warning (pr_id ident ++ str" is declared as a parameter" ++
+ str" because it is at a global level");
ConstRef sp
let hypothesis_def_var is_refining ident n c =
@@ -125,37 +125,37 @@ let hypothesis_def_var is_refining ident n c =
let sp = declare_variable ident (Lib.cwd(),SectionLocalAssum t,n) in
if_verbose message ((string_of_id ident) ^ " is assumed");
if is_refining then
- mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident;
- 'sTR" is not visible from current goals" >];
+ msgerrnl (str"Warning: Variable " ++ pr_id ident ++
+ str" is not visible from current goals");
VarRef ident
end
else
declare_global_assumption ident c
| NotDeclare ->
anomalylabstrm "Command.hypothesis_def_var"
- [<'sTR "Strength NotDeclare not for Variable, only for Let" >]
+ (str "Strength NotDeclare not for Variable, only for Let")
(* 3| Mutual Inductive definitions *)
let minductive_message = function
| [] -> error "no inductive definition"
- | [x] -> [< pr_id x; 'sTR " is defined">]
- | l -> hOV 0 [< prlist_with_sep pr_coma pr_id l;
- 'sPC; 'sTR "are defined">]
+ | [x] -> (pr_id x ++ str " is defined")
+ | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+ spc () ++ str "are defined")
let recursive_message v =
match Array.length v with
| 0 -> error "no recursive definition"
- | 1 -> [< Printer.pr_global v.(0); 'sTR " is recursively defined">]
- | _ -> hOV 0 [< prvect_with_sep pr_coma Printer.pr_global v;
- 'sPC; 'sTR "are recursively defined">]
+ | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+ | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+ spc () ++ str "are recursively defined")
let corecursive_message v =
match Array.length v with
| 0 -> error "no corecursive definition"
- | 1 -> [< Printer.pr_global v.(0); 'sTR " is corecursively defined">]
- | _ -> hOV 0 [< prvect_with_sep pr_coma Printer.pr_global v;
- 'sPC; 'sTR "are corecursively defined">]
+ | 1 -> (Printer.pr_global v.(0) ++ str " is corecursively defined")
+ | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+ spc () ++ str "are corecursively defined")
let interp_mutual lparams lnamearconstrs finite =
let allnames =
@@ -218,7 +218,7 @@ let declare_mutual_with_eliminations mie =
let lrecnames =
List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
let sp = declare_mind mie in
- if_verbose pPNL (minductive_message lrecnames);
+ if_verbose ppnl (minductive_message lrecnames);
Indrec.declare_eliminations sp;
sp
@@ -311,7 +311,7 @@ let build_recursive lnameargsardef =
in
(* declare the recursive definitions *)
let lrefrec = Array.mapi declare namerec in
- if_verbose pPNL (recursive_message lrefrec);
+ if_verbose ppnl (recursive_message lrefrec);
(* The others are declared as normal definitions *)
let var_subst id = (id, global_reference id) in
let _ =
@@ -374,7 +374,7 @@ let build_corecursive lnameardef =
(ConstRef sp)
in
let lrefrec = Array.mapi declare namerec in
- if_verbose pPNL (corecursive_message lrefrec);
+ if_verbose ppnl (corecursive_message lrefrec);
let var_subst id = (id, global_reference id) in
let _ =
List.fold_left
@@ -394,8 +394,8 @@ let inductive_of_ident qid =
match Nametab.global dummy_loc qid with
| IndRef ind -> ind
| ref -> errorlabstrm "inductive_of_ident"
- [< pr_id (id_of_global (Global.env()) ref);
- 'sPC; 'sTR "is not an inductive type">]
+ (pr_id (id_of_global (Global.env()) ref) ++
+ spc () ++ str "is not an inductive type")
let build_scheme lnamedepindsort =
let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
@@ -419,7 +419,7 @@ let build_scheme lnamedepindsort =
ConstRef sp :: lrecref
in
let lrecref = List.fold_right2 declare listdecl lrecnames [] in
- if_verbose pPNL (recursive_message (Array.of_list lrecref))
+ if_verbose ppnl (recursive_message (Array.of_list lrecref))
let start_proof_com sopt stre com =
let env = Global.env () in
@@ -428,7 +428,7 @@ let start_proof_com sopt stre com =
| Some id ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) then
- errorlabstrm "start_proof" [< pr_id id; 'sTR " already exists" >];
+ errorlabstrm "start_proof" (pr_id id ++ str " already exists");
id
| None ->
next_ident_away (id_of_string "Unnamed_thm")
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8bd52929e..8ddb5de78 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -40,14 +40,14 @@ let load_rcfile() =
else ()
(*
Options.if_verbose
- mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
- " found. Skipping rcfile loading.") >]
+ mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^
+ " found. Skipping rcfile loading."))
*)
with e ->
- (mSGNL [< 'sTR"Load of rcfile failed." >];
+ (msgnl (str"Load of rcfile failed.");
raise e)
else
- Options.if_verbose mSGNL [< 'sTR"Skipping rcfile loading." >]
+ Options.if_verbose msgnl (str"Skipping rcfile loading.")
let add_ml_include s =
Mltop.add_ml_dir s
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 864b2fa2c..3b98ce2f4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -111,7 +111,7 @@ let usage () =
flush stderr ;
exit 1
-let warning s = wARNING [< 'sTR s >]
+let warning s = msg_warning (str s)
let parse_args () =
let rec parse = function
@@ -198,9 +198,9 @@ let parse_args () =
try
Stream.empty s; exit 1
with Stream.Failure ->
- mSGNL (Errors.explain_exn e); exit 1
+ msgnl (Errors.explain_exn e); exit 1
end
- | e -> begin mSGNL (Errors.explain_exn e); exit 1 end
+ | e -> begin msgnl (Errors.explain_exn e); exit 1 end
(* To prevent from doing the initialization twice *)
@@ -227,7 +227,7 @@ let start () =
with e ->
flush_all();
if not !batch_mode then message "Error during initialization :";
- mSGNL (Toplevel.print_toplevel_error e);
+ msgnl (Toplevel.print_toplevel_error e);
exit 1
end;
if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 4c5e21b0a..6a3e135ff 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -149,20 +149,20 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
(* Discharge messages. *)
let constant_message id =
- Options.if_verbose pPNL [< pr_id id; 'sTR " is discharged." >]
+ Options.if_verbose ppnl (pr_id id ++ str " is discharged.")
let inductive_message inds =
Options.if_verbose
- pPNL
- (hOV 0
+ ppnl
+ (hov 0
(match inds with
| [] -> assert false
| [ind] ->
- [< pr_id ind.mind_entry_typename; 'sTR " is discharged." >]
+ (pr_id ind.mind_entry_typename ++ str " is discharged.")
| l ->
- [< prlist_with_sep pr_coma
- (fun ind -> pr_id ind.mind_entry_typename) l;
- 'sPC; 'sTR "are discharged.">]))
+ (prlist_with_sep pr_coma
+ (fun ind -> pr_id ind.mind_entry_typename) l ++
+ spc () ++ str "are discharged.")))
(* Discharge operations for the various objects of the environment. *)
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 623ebbfbb..da9ae4a4d 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -18,100 +18,100 @@ open Lexer
let print_loc loc =
if loc = dummy_loc then
- [< 'sTR"<unknown>" >]
+ (str"<unknown>")
else
- [< 'iNT (fst loc); 'sTR"-"; 'iNT (snd loc) >]
+ (int (fst loc) ++ str"-" ++ int (snd loc))
let guill s = "\""^s^"\""
let where s =
- if !Options.debug then [< 'sTR"in "; 'sTR s; 'sTR":"; 'sPC >] else [<>]
+ if !Options.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
-let report () = [< 'sTR "."; 'sPC; 'sTR "Please report." >]
+let report () = (str "." ++ spc () ++ str "Please report.")
(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
let rec explain_exn_default = function
| Stream.Failure ->
- hOV 0 [< 'sTR "Anomaly: Uncaught Stream.Failure." >]
+ hov 0 (str "Anomaly: Uncaught Stream.Failure.")
| Stream.Error txt ->
- hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >]
+ hov 0 (str "Syntax error: " ++ str txt)
| Token.Error txt ->
- hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >]
+ hov 0 (str "Syntax error: " ++ str txt)
| Sys_error msg ->
- hOV 0 [< 'sTR "Error: OS: "; 'sTR msg >]
+ hov 0 (str "Error: OS: " ++ str msg)
| UserError(s,pps) ->
- hOV 1 [< 'sTR"Error: "; where s; pps >]
+ hov 1 (str"Error: " ++ where s ++ pps)
| Out_of_memory ->
- hOV 0 [< 'sTR "Out of memory" >]
+ hov 0 (str "Out of memory")
| Stack_overflow ->
- hOV 0 [< 'sTR "Stack overflow" >]
+ hov 0 (str "Stack overflow")
| Ast.No_match s ->
- hOV 0 [< 'sTR "Anomaly: Ast matching error: "; 'sTR s; report () >]
+ hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ())
| Anomaly (s,pps) ->
- hOV 1 [< 'sTR "Anomaly: "; where s; pps; report () >]
+ hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ())
| Match_failure(filename,pos1,pos2) ->
- hOV 1 [< 'sTR "Anomaly: Match failure in file ";
- 'sTR (guill filename); 'sTR " from char #";
- 'iNT pos1; 'sTR " to #"; 'iNT pos2;
- report () >]
+ hov 1 (str "Anomaly: Match failure in file " ++
+ str (guill filename) ++ str " from char #" ++
+ int pos1 ++ str " to #" ++ int pos2 ++
+ report ())
| Not_found ->
- hOV 0 [< 'sTR "Anomaly: Search error"; report () >]
+ hov 0 (str "Anomaly: Search error" ++ report ())
| Failure s ->
- hOV 0 [< 'sTR "Anomaly: Failure "; 'sTR (guill s); report () >]
+ hov 0 (str "Anomaly: Failure " ++ str (guill s) ++ report ())
| Invalid_argument s ->
- hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >]
+ hov 0 (str "Anomaly: Invalid argument " ++ str (guill s) ++ report ())
| Sys.Break ->
- hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
+ hov 0 (fnl () ++ str"User Interrupt.")
| Univ.UniverseInconsistency ->
- hOV 0 [< 'sTR "Error: Universe Inconsistency." >]
+ hov 0 (str "Error: Universe Inconsistency.")
| TypeError(ctx,te) ->
- hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error ctx te >]
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
| PretypeError(ctx,te) ->
- hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >]
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
| InductiveError e ->
- hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >]
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
| Cases.PatternMatchingError (env,e) ->
- hOV 0
- [< 'sTR "Error:"; 'sPC; Himsg.explain_pattern_matching_error env e >]
+ hov 0
+ (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
| Logic.RefinerError e ->
- hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_refiner_error e >]
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
- hOV 0 [< 'sTR "Error:"; 'sPC;
- 'sTR "The reference"; 'sPC; Nametab.pr_qualid q;
- 'sPC ; 'sTR "was not found";
- 'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
+ hov 0 (str "Error:" ++ spc () ++
+ str "The reference" ++ spc () ++ Nametab.pr_qualid q ++
+ spc () ++ str "was not found" ++
+ spc () ++ str "in the current" ++ spc () ++ str "environment")
| Nametab.GlobalizationConstantError q ->
- hOV 0 [< 'sTR "Error:"; 'sPC;
- 'sTR "No constant of this name:"; 'sPC; Nametab.pr_qualid q >]
+ hov 0 (str "Error:" ++ spc () ++
+ str "No constant of this name:" ++ spc () ++ Nametab.pr_qualid q)
| Tacmach.FailError i ->
- hOV 0 [< 'sTR "Error: Fail tactic always fails (level ";
- 'iNT i; 'sTR")." >]
+ hov 0 (str "Error: Fail tactic always fails (level " ++
+ int i ++ str").")
| Stdpp.Exc_located (loc,exc) ->
- hOV 0 [< if loc = Ast.dummy_loc then [<>]
- else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
- explain_exn_default exc >]
+ hov 0 (if loc = Ast.dummy_loc then (mt ())
+ else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()) ++
+ explain_exn_default exc)
| Lexer.Error Illegal_character ->
- hOV 0 [< 'sTR "Syntax error: Illegal character." >]
+ hov 0 (str "Syntax error: Illegal character.")
| Lexer.Error Unterminated_comment ->
- hOV 0 [< 'sTR "Syntax error: Unterminated comment." >]
+ hov 0 (str "Syntax error: Unterminated comment.")
| Lexer.Error Unterminated_string ->
- hOV 0 [< 'sTR "Syntax error: Unterminated string." >]
+ hov 0 (str "Syntax error: Unterminated string.")
| Lexer.Error Undefined_token ->
- hOV 0 [< 'sTR "Syntax error: Undefined token." >]
+ hov 0 (str "Syntax error: Undefined token.")
| Lexer.Error (Bad_token s) ->
- hOV 0 [< 'sTR "Syntax error: Bad token"; 'sPC; 'sTR s; 'sTR "." >]
+ hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
| Assert_failure (s,b,e) ->
- hOV 0 [< 'sTR "Anomaly: assert failure"; 'sPC;
+ hov 0 (str "Anomaly: assert failure" ++ spc () ++
if s <> "" then
- [< 'sTR ("(file \"" ^ s ^ "\", characters ");
- 'iNT b; 'sTR "-"; 'iNT e; 'sTR ")" >]
+ (str ("(file \"" ^ s ^ "\", characters ") ++
+ int b ++ str "-" ++ int e ++ str ")")
else
- [< >];
- report () >]
+ (mt ()) ++
+ report ())
| reraise ->
- hOV 0 [< 'sTR "Anomaly: Uncaught exception ";
- 'sTR (Printexc.to_string reraise); report () >]
+ hov 0 (str "Anomaly: Uncaught exception " ++
+ str (Printexc.to_string reraise) ++ report ())
let raise_if_debug e =
if !Options.debug then raise e
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 2f248885b..c5294c0b7 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -26,13 +26,13 @@ module Make = functor (P : Printer) -> struct
let print_decl k env (s,typ) =
let ptyp = P.pr_term k env (body_of_type typ) in
- [< 'sPC; pr_id s; 'sTR" : "; ptyp >]
+ (spc () ++ pr_id s ++ str" : " ++ ptyp)
let print_binding k env = function
| Anonymous,ty ->
- [< 'sPC; 'sTR"_" ; 'sTR" : " ; P.pr_term k env (body_of_type ty) >]
+ (spc () ++ str"_" ++ str" : " ++ P.pr_term k env (body_of_type ty))
| Name id,ty ->
- [< 'sPC; pr_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >]
+ (spc () ++ pr_id id ++ str" : " ++ P.pr_term k env (body_of_type ty))
(****
let sign_it_with f sign e =
@@ -50,55 +50,55 @@ module Make = functor (P : Printer) -> struct
let sign_env =
fold_named_context
(fun env (id,_,t) pps ->
- let pidt = print_decl k env (id,t) in [< pps ; 'fNL ; pidt >])
- env [< >]
+ let pidt = print_decl k env (id,t) in (pps ++ fnl () ++ pidt))
+ env (mt ())
in
let db_env =
fold_rel_context
(fun env (na,_,t) pps ->
- let pnat = print_binding k env (na,t) in [< pps ; 'fNL ; pnat >])
- env [< >]
+ let pnat = print_binding k env (na,t) in (pps ++ fnl () ++ pnat))
+ env (mt ())
in
- [< sign_env; db_env >]
+ (sign_env ++ db_env)
let pr_ne_ctx header k env =
if rel_context env = [] && named_context env = [] then
- [< >]
+ (mt ())
else
- [< header; pr_env k env >]
+ (header ++ pr_env k env)
let explain_unbound_rel k ctx n =
- let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
- [< 'sTR"Unbound reference: "; pe; 'fNL;
- 'sTR"The reference "; 'iNT n; 'sTR" is free" >]
+ let pe = pr_ne_ctx (str"in environment") k ctx in
+ (str"Unbound reference: " ++ pe ++ fnl () ++
+ str"The reference " ++ int n ++ str" is free")
let explain_not_type k ctx c =
- let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
+ let pe = pr_ne_ctx (str"In environment") k ctx in
let pc = P.pr_term k ctx c in
- [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
- 'sTR"should be typed by Set, Prop or Type." >];;
+ (pe ++ cut () ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
+ str"should be typed by Set, Prop or Type.");;
let explain_bad_assumption k ctx c =
let pc = P.pr_term k ctx c in
- [< 'sTR "Cannot declare a variable or hypothesis over the term";
- 'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
+ (str "Cannot declare a variable or hypothesis over the term" ++
+ brk(1,1) ++ pc ++ spc () ++ str "because this term is not a type.");;
let explain_reference_variables id =
- [< 'sTR "the constant"; 'sPC; pr_id id; 'sPC;
- 'sTR "refers to variables which are not in the context" >]
+ (str "the constant" ++ spc () ++ pr_id id ++ spc () ++
+ str "refers to variables which are not in the context")
let msg_bad_elimination ctx k = function
| Some(ki,kp,explanation) ->
let pki = P.pr_term k ctx ki in
let pkp = P.pr_term k ctx kp in
- (hOV 0
- [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
- pki; 'bRK(1,0);
- 'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
- 'sTR "because"; 'sPC; 'sTR explanation >])
+ (hov 0
+ (fnl () ++ str "Elimination of an inductive object of sort : " ++
+ pki ++ brk(1,0) ++
+ str "is not allowed on a predicate in sort : " ++ pkp ++fnl () ++
+ str "because" ++ spc () ++ str explanation))
| None ->
- [<>]
+ (mt ())
let explain_elim_arity k ctx ind aritylst c pj okinds =
let pi = P.pr_term k ctx ind in
@@ -106,58 +106,58 @@ let explain_elim_arity k ctx ind aritylst c pj okinds =
let pc = P.pr_term k ctx c in
let pp = P.pr_term k ctx pj.uj_val in
let ppt = P.pr_term k ctx pj.uj_type in
- [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
- 'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
- 'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
- 'sTR "has type"; 'bRK(1,1); ppt; 'fNL;
- 'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
- msg_bad_elimination ctx k okinds >]
+ (str "Incorrect elimination of" ++ brk(1,1) ++ pc ++ spc () ++
+ str "in the inductive type" ++ brk(1,1) ++ pi ++ fnl () ++
+ str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
+ str "has type" ++ brk(1,1) ++ ppt ++ fnl () ++
+ str "It should be one of :" ++ brk(1,1) ++ hov 0 ppar ++ fnl () ++
+ msg_bad_elimination ctx k okinds)
let explain_case_not_inductive k ctx cj =
let pc = P.pr_term k ctx cj.uj_val in
let pct = P.pr_term k ctx cj.uj_type in
- [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC;
- 'sTR "has type"; 'bRK(1,1); pct; 'sPC;
- 'sTR "which is not an inductive definition" >]
+ (str "In Cases expression" ++ brk(1,1) ++ pc ++ spc () ++
+ str "has type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "which is not an inductive definition")
let explain_number_branches k ctx cj expn =
let pc = P.pr_term k ctx cj.uj_val in
let pct = P.pr_term k ctx cj.uj_val in
- [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
- 'sTR "of type"; 'bRK(1,1); pct; 'sPC;
- 'sTR "expects "; 'iNT expn; 'sTR " branches" >]
+ (str "Cases on term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "of type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "expects " ++ int expn ++ str " branches")
let explain_ill_formed_branch k ctx c i actty expty =
let pc = P.pr_term k ctx c in
let pa = P.pr_term k ctx actty in
let pe = P.pr_term k ctx expty in
- [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
- 'sPC; 'sTR "the branch " ; 'iNT (i+1);
- 'sTR " has type"; 'bRK(1,1); pa ; 'sPC;
- 'sTR "which should be:"; 'bRK(1,1); pe >]
+ (str "In Cases expression on term" ++ brk(1,1) ++ pc ++
+ spc () ++ str "the branch " ++ int (i+1) ++
+ str " has type" ++ brk(1,1) ++ pa ++ spc () ++
+ str "which should be:" ++ brk(1,1) ++ pe)
let explain_generalization k ctx (name,var) c =
- let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+ let pe = pr_ne_ctx (str"in environment") k ctx in
let pv = P.pr_term k ctx (body_of_type var) in
let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
- [< 'sTR"Illegal generalization: "; pe; 'fNL;
- 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
- 'sTR"over"; 'bRK(1,1); pc; 'sPC;
- 'sTR"which should be typed by Set, Prop or Type." >]
+ (str"Illegal generalization: " ++ pe ++ fnl () ++
+ str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
+ str"over" ++ brk(1,1) ++ pc ++ spc () ++
+ str"which should be typed by Set, Prop or Type.")
let explain_actual_type k ctx c ct pt =
- let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
+ let pe = pr_ne_ctx (str"In environment") k ctx in
let pc = P.pr_term k ctx c in
let pct = P.pr_term k ctx ct in
let pt = P.pr_term k ctx pt in
- [< pe; 'fNL;
- 'sTR"The term"; 'bRK(1,1); pc ; 'sPC ;
- 'sTR"does not have type"; 'bRK(1,1); pt; 'fNL;
- 'sTR"Actually, it has type" ; 'bRK(1,1); pct >]
+ (pe ++ fnl () ++
+ str"The term" ++ brk(1,1) ++ pc ++ spc () ++
+ str"does not have type" ++ brk(1,1) ++ pt ++ fnl () ++
+ str"Actually, it has type" ++ brk(1,1) ++ pct)
let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+ let pe = pr_ne_ctx (str"in environment") k ctx in
let pr = pr_term k ctx rator.uj_val in
let prt = pr_term k ctx (body_of_type rator.uj_type) in
let term_string = if List.length randl > 1 then "terms" else "term" in
@@ -166,20 +166,20 @@ let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
(fun c ->
let pc = pr_term k ctx c.uj_val in
let pct = pr_term k ctx (body_of_type c.uj_type) in
- hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
+ hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
- [< 'sTR"Illegal application (Type Error): "; pe; 'fNL;
- 'sTR"The term"; 'bRK(1,1); pr; 'sPC;
- 'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
- 'sTR("cannot be applied to the "^term_string); 'fNL;
- 'sTR" "; v 0 appl; 'fNL;
- 'sTR"The ";'iNT n; 'sTR (many^" term of type ");
- pr_term k ctx actualtyp;
- 'sTR" should be of type "; pr_term k ctx exptyp >]
+ (str"Illegal application (Type Error): " ++ pe ++ fnl () ++
+ str"The term" ++ brk(1,1) ++ pr ++ spc () ++
+ str"of type" ++ brk(1,1) ++ prt ++ spc () ++
+ str("cannot be applied to the "^term_string) ++ fnl () ++
+ str" " ++ v 0 appl ++ fnl () ++
+ str"The " ++int n ++ str (many^" term of type ") ++
+ pr_term k ctx actualtyp ++
+ str" should be of type " ++ pr_term k ctx exptyp)
let explain_cant_apply_not_functional k ctx rator randl =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+ let pe = pr_ne_ctx (str"in environment") k ctx in
let pr = pr_term k ctx rator.uj_val in
let prt = pr_term k ctx (body_of_type rator.uj_type) in
let term_string = if List.length randl > 1 then "terms" else "term" in
@@ -187,13 +187,13 @@ let explain_cant_apply_not_functional k ctx rator randl =
(fun c ->
let pc = pr_term k ctx c.uj_val in
let pct = pr_term k ctx (body_of_type c.uj_type) in
- hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
+ hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
- [< 'sTR"Illegal application (Non-functional construction): "; pe; 'fNL;
- 'sTR"The term"; 'bRK(1,1); pr; 'sPC;
- 'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
- 'sTR("cannot be applied to the "^term_string); 'fNL;
- 'sTR" "; v 0 appl; 'fNL >]
+ (str"Illegal application (Non-functional construction): " ++ pe ++ fnl () ++
+ str"The term" ++ brk(1,1) ++ pr ++ spc () ++
+ str"of type" ++ brk(1,1) ++ prt ++ spc () ++
+ str("cannot be applied to the "^term_string) ++ fnl () ++
+ str" " ++ v 0 appl ++ fnl ())
(* (co)fixpoints *)
let explain_ill_formed_rec_body k ctx err names i vdefs =
@@ -201,89 +201,89 @@ let explain_ill_formed_rec_body k ctx err names i vdefs =
(* Fixpoint guard errors *)
| NotEnoughAbstractionInFixBody ->
- [< 'sTR "Not enough abstractions in the definition" >]
+ (str "Not enough abstractions in the definition")
| RecursionNotOnInductiveType ->
- [< 'sTR "Recursive definition on a non inductive type" >]
+ (str "Recursive definition on a non inductive type")
| RecursionOnIllegalTerm ->
- [< 'sTR "Recursive call applied to an illegal term" >]
+ (str "Recursive call applied to an illegal term")
| NotEnoughArgumentsForFixCall ->
- [< 'sTR "Not enough arguments for the recursive call" >]
+ (str "Not enough arguments for the recursive call")
(* CoFixpoint guard errors *)
(* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
| CodomainNotInductiveType c ->
- [< 'sTR "The codomain is"; 'sPC; P.pr_term k ctx c; 'sPC;
- 'sTR "which should be a coinductive type" >]
+ (str "The codomain is" ++ spc () ++ P.pr_term k ctx c ++ spc () ++
+ str "which should be a coinductive type")
| NestedRecursiveOccurrences ->
- [< 'sTR "Nested recursive occurrences" >]
+ (str "Nested recursive occurrences")
| UnguardedRecursiveCall c ->
- [< 'sTR "Unguarded recursive call" >]
+ (str "Unguarded recursive call")
| RecCallInTypeOfAbstraction c ->
- [< 'sTR "Not allowed recursive call in the domain of an abstraction" >]
+ (str "Not allowed recursive call in the domain of an abstraction")
| RecCallInNonRecArgOfConstructor c ->
- [< 'sTR "Not allowed recursive call in a non-recursive argument of constructor" >]
+ (str "Not allowed recursive call in a non-recursive argument of constructor")
| RecCallInTypeOfDef c ->
- [< 'sTR "Not allowed recursive call in the type of a recursive definition" >]
+ (str "Not allowed recursive call in the type of a recursive definition")
| RecCallInCaseFun c ->
- [< 'sTR "Not allowed recursive call in a branch of cases" >]
+ (str "Not allowed recursive call in a branch of cases")
| RecCallInCaseArg c ->
- [< 'sTR "Not allowed recursive call in the argument of cases" >]
+ (str "Not allowed recursive call in the argument of cases")
| RecCallInCasePred c ->
- [< 'sTR "Not allowed recursive call in the type of cases in" >]
+ (str "Not allowed recursive call in the type of cases in")
| NotGuardedForm ->
- [< 'sTR "Definition not in guarded form" >]
+ (str "Definition not in guarded form")
in
let pvd = P.pr_term k ctx vdefs.(i) in
let s =
match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
- [< str; 'fNL; 'sTR"The ";
- if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
- 'sTR"recursive definition"; 'sPC; 'sTR s;
- 'sPC ; 'sTR":="; 'sPC ; pvd; 'sPC;
- 'sTR "is not well-formed" >]
+ (str ++ fnl () ++ str"The " ++
+ if Array.length vdefs = 1 then (mt ()) else (int (i+1) ++ str "-th ") ++
+ str"recursive definition" ++ spc () ++ str s ++
+ spc () ++ str":=" ++ spc () ++ pvd ++ spc () ++
+ str "is not well-formed")
let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in
let pvdt = P.pr_term k ctx (body_of_type (vdefj.(i)).uj_type) in
let pv = P.pr_term k ctx (body_of_type vargs.(i)) in
- [< 'sTR"The " ;
- if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
- 'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
- 'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
+ (str"The " ++
+ if Array.length vdefj = 1 then (mt ()) else (int (i+1) ++ str "-th") ++
+ str"recursive definition" ++ spc () ++ pvd ++ spc () ++
+ str "has type" ++ spc () ++ pvdt ++spc () ++ str "it should be" ++ spc () ++ pv)
let explain_not_inductive k ctx c =
let pc = P.pr_term k ctx c in
- [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
- 'sTR "is not an inductive definition" >]
+ (str"The term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "is not an inductive definition")
let explain_ml_case k ctx mes c ct br brt =
let pc = P.pr_term k ctx c in
let pct = P.pr_term k ctx ct in
let expln =
match mes with
- | "Inductive" -> [< pct; 'sTR "is not an inductive definition">]
- | "Predicate" -> [< 'sTR "ML case not allowed on a predicate">]
- | "Absurd" -> [< 'sTR "Ill-formed case expression on an empty type" >]
+ | "Inductive" -> (pct ++ str "is not an inductive definition")
+ | "Predicate" -> (str "ML case not allowed on a predicate")
+ | "Absurd" -> (str "Ill-formed case expression on an empty type")
| "Decomp" ->
let plf = P.pr_term k ctx br in
let pft = P.pr_term k ctx brt in
- [< 'sTR "The branch "; plf; 'wS 1; 'cUT; 'sTR "has type "; pft;
- 'wS 1; 'cUT;
- 'sTR "does not correspond to the inductive definition" >]
+ (str "The branch " ++ plf ++ 'wS 1 ++ cut () ++ str "has type " ++ pft ++
+ 'wS 1 ++ cut () ++
+ str "does not correspond to the inductive definition")
| "Dependent" ->
- [< 'sTR "ML case not allowed for a dependent case elimination">]
- | _ -> [<>]
+ (str "ML case not allowed for a dependent case elimination")
+ | _ -> (mt ())
in
- hOV 0 [< 'sTR "In ML case expression on "; pc; 'wS 1; 'cUT ;
- 'sTR "of type"; 'wS 1; pct; 'wS 1; 'cUT;
- 'sTR "which is an inductive predicate."; 'fNL; expln >]
+ hov 0 (str "In ML case expression on " ++ pc ++ 'wS 1 ++ cut () ++
+ str "of type" ++ 'wS 1 ++ pct ++ 'wS 1 ++ cut () ++
+ str "which is an inductive predicate." ++ fnl () ++ expln)
(*
let explain_cant_find_case_type loc k ctx c =
let pe = P.pr_term k ctx c in
Ast.user_err_loc
(loc,"pretype",
- hOV 3 [<'sTR "Cannot infer type of whole Case expression on";
- 'wS 1; pe >])
+ hov 3 (str "Cannot infer type of whole Case expression on" ++
+ 'wS 1 ++ pe))
*)
let explain_type_error k ctx = function
| UnboundRel n ->
@@ -321,41 +321,41 @@ let explain_type_error k ctx = function
explain_ml_case k ctx mes c ct br brt
*)
| _ ->
- [< 'sTR "Unknown type error (TODO)" >]
+ (str "Unknown type error (TODO)")
let explain_refiner_bad_type k ctx arg ty conclty =
errorlabstrm "Logic.conv_leq_goal"
- [< 'sTR"refiner was given an argument"; 'bRK(1,1);
- P.pr_term k ctx arg; 'sPC;
- 'sTR"of type"; 'bRK(1,1); P.pr_term k ctx ty; 'sPC;
- 'sTR"instead of"; 'bRK(1,1); P.pr_term k ctx conclty >]
+ (str"refiner was given an argument" ++ brk(1,1) ++
+ P.pr_term k ctx arg ++ spc () ++
+ str"of type" ++ brk(1,1) ++ P.pr_term k ctx ty ++ spc () ++
+ str"instead of" ++ brk(1,1) ++ P.pr_term k ctx conclty)
let explain_refiner_occur_meta k ctx t =
errorlabstrm "Logic.mk_refgoals"
- [< 'sTR"cannot refine with term"; 'bRK(1,1); P.pr_term k ctx t;
- 'sPC; 'sTR"because there are metavariables, and it is";
- 'sPC; 'sTR"neither an application nor a Case" >]
+ (str"cannot refine with term" ++ brk(1,1) ++ P.pr_term k ctx t ++
+ spc () ++ str"because there are metavariables, and it is" ++
+ spc () ++ str"neither an application nor a Case")
let explain_refiner_cannot_applt k ctx t harg =
errorlabstrm "Logic.mkARGGOALS"
- [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
- P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
- P.pr_term k ctx harg >]
+ (str"in refiner, a term of type " ++ brk(1,1) ++
+ P.pr_term k ctx t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
+ P.pr_term k ctx harg)
let explain_occur_check k ctx ev rhs =
let id = "?" ^ string_of_int ev in
let pt = P.pr_term k ctx rhs in
errorlabstrm "Trad.occur_check"
- [< 'sTR"Occur check failed: tried to define "; 'sTR id;
- 'sTR" with term"; 'bRK(1,1); pt >]
+ (str"Occur check failed: tried to define " ++ str id ++
+ str" with term" ++ brk(1,1) ++ pt)
let explain_not_clean k ctx sp t =
let c = mkRel (Intset.choose (free_rels t)) in
let id = string_of_id (Names.basename sp) in
let var = P.pr_term k ctx c in
errorlabstrm "Trad.not_clean"
- [< 'sTR"Tried to define "; 'sTR id;
- 'sTR" with a term using variable "; var; 'sPC;
- 'sTR"which is not in its scope." >]
+ (str"Tried to define " ++ str id ++
+ str" with a term using variable " ++ var ++ spc () ++
+ str"which is not in its scope.")
end
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 678ad6431..4af71a587 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -31,34 +31,34 @@ let guill s = "\""^s^"\""
let explain_unbound_rel ctx n =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_context_of [< 'sTR "In environment" >] ctx in
- [< 'sTR"Unbound reference: "; pe;
- 'sTR"The reference "; 'iNT n; 'sTR" is free" >]
+ let pe = pr_ne_context_of (str "In environment") ctx in
+ str"Unbound reference: " ++ pe ++
+ str"The reference " ++ int n ++ str " is free"
let explain_unbound_var ctx v =
let var = pr_id v in
- [< 'sTR"No such section variable or assumption : "; var >]
+ str"No such section variable or assumption : " ++ var
let explain_not_type ctx j =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_context_of [< 'sTR"In environment" >] ctx in
+ let pe = pr_ne_context_of (str"In environment") ctx in
let pc,pt = prjudge_env ctx j in
- [< pe; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
- 'sTR"has type"; 'sPC; pt; 'sPC;
- 'sTR"which should be Set, Prop or Type." >];;
+ pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
+ str"has type" ++ spc () ++ pt ++ spc () ++
+ str"which should be Set, Prop or Type."
let explain_bad_assumption ctx j =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_context_of [< 'sTR"In environment" >] ctx in
+ let pe = pr_ne_context_of (str"In environment") ctx in
let pc,pt = prjudge_env ctx j in
- [< pe; 'sTR "cannot declare a variable or hypothesis over the term";
- 'bRK(1,1); pc; 'sPC; 'sTR"of type"; 'sPC; pt; 'sPC;
- 'sTR "because this term is not a type." >];;
+ pe ++ str "cannot declare a variable or hypothesis over the term" ++
+ brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++
+ str "because this term is not a type."
let explain_reference_variables c =
let pc = prterm c in
- [< 'sTR "the constant"; 'sPC; pc; 'sPC;
- 'sTR "refers to variables which are not in the context" >]
+ str "the constant" ++ spc () ++ pc ++ spc () ++
+ str "refers to variables which are not in the context"
let explain_elim_arity ctx ind aritylst c pj okinds =
let pi = pr_inductive ctx ind in
@@ -77,68 +77,69 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
"strong elimination on non-small inductive types leads to paradoxes."
| WrongArity ->
"wrong arity" in
- (hOV 0
- [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
- pki; 'bRK(1,0);
- 'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
- 'sTR "because"; 'sPC; 'sTR explanation >])
+ (hov 0
+ (fnl () ++ str "Elimination of an inductive object of sort : " ++
+ pki ++ brk(1,0) ++
+ str "is not allowed on a predicate in sort : " ++ pkp ++fnl () ++
+ str "because" ++ spc () ++ str explanation))
| None ->
- [<>]
+ mt ()
in
- [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
- 'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
- 'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
- 'sTR "has type"; 'bRK(1,1); ppt; 'fNL;
- 'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
- msg >]
+ str "Incorrect elimination of" ++ brk(1,1) ++ pc ++ spc () ++
+ str "in the inductive type" ++ brk(1,1) ++ pi ++ fnl () ++
+ str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
+ str "has type" ++ brk(1,1) ++ ppt ++ fnl () ++
+ str "It should be one of :" ++ brk(1,1) ++ hov 0 ppar ++ fnl () ++
+ msg
let explain_case_not_inductive ctx cj =
let pc = prterm_env ctx cj.uj_val in
let pct = prterm_env ctx cj.uj_type in
- [< 'sTR "In Cases expression, the matched term"; 'bRK(1,1); pc; 'sPC;
- 'sTR "has type"; 'bRK(1,1); pct; 'sPC;
- 'sTR "which is not a (co-)inductive type" >]
+ str "In Cases expression, the matched term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "has type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "which is not a (co-)inductive type"
let explain_number_branches ctx cj expn =
let pc = prterm_env ctx cj.uj_val in
let pct = prterm_env ctx cj.uj_type in
- [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
- 'sTR "of type"; 'bRK(1,1); pct; 'sPC;
- 'sTR "expects "; 'iNT expn; 'sTR " branches" >]
+ str "Cases on term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "of type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "expects " ++ int expn ++ str " branches"
let explain_ill_formed_branch ctx c i actty expty =
let pc = prterm_env ctx c in
let pa = prterm_env ctx actty in
let pe = prterm_env ctx expty in
- [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
- 'sPC; 'sTR "the branch " ; 'iNT (i+1);
- 'sTR " has type"; 'bRK(1,1); pa ; 'sPC;
- 'sTR "which should be"; 'bRK(1,1); pe >]
+ str "In Cases expression on term" ++ brk(1,1) ++ pc ++
+ spc () ++ str "the branch " ++ int (i+1) ++
+ str " has type" ++ brk(1,1) ++ pa ++ spc () ++
+ str "which should be" ++ brk(1,1) ++ pe
let explain_generalization ctx (name,var) j =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_context_of [< 'sTR "In environment" >] ctx in
+ let pe = pr_ne_context_of (str "In environment") ctx in
let pv = prtype_env ctx var in
let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
- [< 'sTR"Illegal generalization: "; pe;
- 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
- 'sTR"over"; 'bRK(1,1); pc; 'sTR","; 'sPC; 'sTR"it has type"; 'sPC; pt;
- 'sPC; 'sTR"which should be Set, Prop or Type." >]
+ str"Illegal generalization: " ++ pe ++
+ str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
+ str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++
+ str"it has type" ++ spc () ++ pt ++
+ spc () ++ str"which should be Set, Prop or Type."
let explain_actual_type ctx j pt =
let ctx = make_all_name_different ctx in
- let pe = pr_ne_context_of [< 'sTR "In environment" >] ctx in
+ let pe = pr_ne_context_of (str "In environment") ctx in
let (pc,pct) = prjudge_env ctx j in
let pt = prterm_env ctx pt in
- [< pe;
- 'sTR "The term"; 'bRK(1,1); pc ; 'sPC ;
- 'sTR "has type" ; 'bRK(1,1); pct; 'bRK(1,1);
- 'sTR "while it is expected to have type"; 'bRK(1,1); pt >]
+ pe ++
+ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
+ str "while it is expected to have type" ++ brk(1,1) ++ pt
let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
let randl = Array.to_list randl in
let ctx = make_all_name_different ctx in
-(* let pe = pr_ne_context_of [< 'sTR"in environment" >] ctx in*)
+(* let pe = pr_ne_context_of (str"in environment") ctx in*)
let pr,prt = prjudge_env ctx rator in
let term_string1,term_string2 =
if List.length randl > 1 then
@@ -149,20 +150,20 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
let appl = prlist_with_sep pr_fnl
(fun c ->
let pc,pct = prjudge_env ctx c in
- hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
+ hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
- [< 'sTR"Illegal application (Type Error): "; (* pe; *) 'fNL;
- 'sTR"The term"; 'bRK(1,1); pr; 'sPC;
- 'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
- 'sTR("cannot be applied to the "^term_string1); 'fNL;
- 'sTR" "; v 0 appl; 'fNL; 'sTR (term_string2^" has type");
- 'bRK(1,1); prterm_env ctx actualtyp; 'sPC;
- 'sTR"which should be coercible to"; 'bRK(1,1); prterm_env ctx exptyp >]
+ str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
+ str"The term" ++ brk(1,1) ++ pr ++ spc () ++
+ str"of type" ++ brk(1,1) ++ prt ++ spc () ++
+ str("cannot be applied to the "^term_string1) ++ fnl () ++
+ str" " ++ v 0 appl ++ fnl () ++ str (term_string2^" has type") ++
+ brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++
+ str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
let explain_cant_apply_not_functional ctx rator randl =
let randl = Array.to_list randl in
let ctx = make_all_name_different ctx in
-(* let pe = pr_ne_context_of [< 'sTR"in environment" >] ctx in*)
+(* let pe = pr_ne_context_of (str"in environment") ctx in*)
let pr = prterm_env ctx rator.uj_val in
let prt = prterm_env ctx (body_of_type rator.uj_type) in
let term_string = if List.length randl > 1 then "terms" else "term" in
@@ -170,131 +171,133 @@ let explain_cant_apply_not_functional ctx rator randl =
(fun c ->
let pc = prterm_env ctx c.uj_val in
let pct = prterm_env ctx (body_of_type c.uj_type) in
- hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
+ hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
- [< 'sTR"Illegal application (Non-functional construction): "; (* pe; *) 'fNL;
- 'sTR"The expression"; 'bRK(1,1); pr; 'sPC;
- 'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
- 'sTR("cannot be applied to the "^term_string); 'fNL;
- 'sTR" "; v 0 appl >]
+ str"Illegal application (Non-functional construction): " ++
+ (* pe ++ *) fnl () ++
+ str"The expression" ++ brk(1,1) ++ pr ++ spc () ++
+ str"of type" ++ brk(1,1) ++ prt ++ spc () ++
+ str("cannot be applied to the "^term_string) ++ fnl () ++
+ str" " ++ v 0 appl
let explain_unexpected_type ctx actual_type expected_type =
let ctx = make_all_name_different ctx in
let pract = prterm_env ctx actual_type in
let prexp = prterm_env ctx expected_type in
- [< 'sTR"This type is"; 'sPC; pract; 'sPC; 'sTR "but is expected to be";
- 'sPC; prexp >]
+ str"This type is" ++ spc () ++ pract ++ spc () ++
+ str "but is expected to be" ++
+ spc () ++ prexp
let explain_not_product ctx c =
let ctx = make_all_name_different ctx in
let pr = prterm_env ctx c in
- [< 'sTR"The type of this term is a product,"; 'sPC;
- 'sTR"but it is casted with type";
- 'bRK(1,1); pr >]
+ str"The type of this term is a product," ++ spc () ++
+ str"but it is casted with type" ++
+ brk(1,1) ++ pr
(* TODO: use the names *)
(* (co)fixpoints *)
let explain_ill_formed_rec_body ctx err names i vdefs =
- let str = match err with
+ let st = match err with
(* Fixpoint guard errors *)
| NotEnoughAbstractionInFixBody ->
- [< 'sTR "Not enough abstractions in the definition" >]
+ str "Not enough abstractions in the definition"
| RecursionNotOnInductiveType ->
- [< 'sTR "Recursive definition on a non inductive type" >]
+ str "Recursive definition on a non inductive type"
| RecursionOnIllegalTerm ->
- [< 'sTR "Recursive call applied to an illegal term" >]
+ str "Recursive call applied to an illegal term"
| NotEnoughArgumentsForFixCall ->
- [< 'sTR "Not enough arguments for the recursive call" >]
+ str "Not enough arguments for the recursive call"
(* CoFixpoint guard errors *)
(* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
| CodomainNotInductiveType c ->
- [< 'sTR "The codomain is"; 'sPC; prterm c; 'sPC;
- 'sTR "which should be a coinductive type" >]
+ str "The codomain is" ++ spc () ++ prterm c ++ spc () ++
+ str "which should be a coinductive type"
| NestedRecursiveOccurrences ->
- [< 'sTR "Nested recursive occurrences" >]
+ str "Nested recursive occurrences"
| UnguardedRecursiveCall c ->
- [< 'sTR "Unguarded recursive call" >]
+ str "Unguarded recursive call"
| RecCallInTypeOfAbstraction c ->
- [< 'sTR "Not allowed recursive call in the domain of an abstraction" >]
+ str "Not allowed recursive call in the domain of an abstraction"
| RecCallInNonRecArgOfConstructor c ->
- [< 'sTR "Not allowed recursive call in a non-recursive argument of constructor" >]
+ str "Not allowed recursive call in a non-recursive argument of constructor"
| RecCallInTypeOfDef c ->
- [< 'sTR "Not allowed recursive call in the type of a recursive definition" >]
+ str "Not allowed recursive call in the type of a recursive definition"
| RecCallInCaseFun c ->
- [< 'sTR "Not allowed recursive call in a branch of cases" >]
+ str "Not allowed recursive call in a branch of cases"
| RecCallInCaseArg c ->
- [< 'sTR "Not allowed recursive call in the argument of cases" >]
+ str "Not allowed recursive call in the argument of cases"
| RecCallInCasePred c ->
- [< 'sTR "Not allowed recursive call in the type of cases in" >]
+ str "Not allowed recursive call in the type of cases in"
| NotGuardedForm ->
- [< 'sTR "Definition not in guarded form" >]
+ str "Definition not in guarded form"
in
let pvd = prterm_env ctx vdefs.(i) in
- let s =
- match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
- [< str; 'fNL; 'sTR"The ";
- if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
- 'sTR"recursive definition"; 'sPC; 'sTR s;
- 'sPC ; 'sTR":="; 'sPC ; pvd; 'sPC;
- 'sTR "is not well-formed" >]
+ let s = match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
+ st ++ fnl () ++ str"The " ++
+ (if Array.length vdefs = 1 then mt () else (int (i+1) ++ str "-th ")) ++
+ str"recursive definition" ++ spc () ++ str s ++
+ spc () ++ str":=" ++ spc () ++ pvd ++ spc () ++
+ str "is not well-formed"
let explain_ill_typed_rec_body ctx i names vdefj vargs =
let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
let pv = prterm_env ctx (body_of_type vargs.(i)) in
- [< 'sTR"The " ;
- if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
- 'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
- 'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
+ str"The " ++
+ (if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++
+ str"recursive definition" ++ spc () ++ pvd ++ spc () ++
+ str "has type" ++ spc () ++ pvdt ++spc () ++
+ str "it should be" ++ spc () ++ pv
let explain_not_inductive ctx c =
let pc = prterm_env ctx c in
- [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
- 'sTR "is not an inductive definition" >]
+ str"The term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "is not an inductive definition"
let explain_ml_case ctx mes =
let expln = match mes with
| MlCaseAbsurd ->
- [< 'sTR "Unable to infer a predicate for an elimination an empty type">]
+ str "Unable to infer a predicate for an elimination an empty type"
| MlCaseDependent ->
- [< 'sTR "Unable to infer a dependent elimination predicate">]
+ str "Unable to infer a dependent elimination predicate"
in
- hOV 0 [< 'sTR "Cannot infer ML Case predicate:"; 'fNL; expln >]
+ hov 0 (str "Cannot infer ML Case predicate:" ++ fnl () ++ expln)
let explain_cant_find_case_type ctx c =
let pe = prterm_env ctx c in
- hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]
+ hov 3 (str "Cannot infer type of whole Case expression on" ++ ws 1 ++ pe)
let explain_occur_check ctx ev rhs =
let id = "?" ^ string_of_int ev in
let pt = prterm_env ctx rhs in
- [< 'sTR"Occur check failed: tried to define "; 'sTR id;
- 'sTR" with term"; 'bRK(1,1); pt >]
+ str"Occur check failed: tried to define " ++ str id ++
+ str" with term" ++ brk(1,1) ++ pt
let explain_not_clean ctx ev t =
let c = mkRel (Intset.choose (free_rels t)) in
let id = "?" ^ string_of_int ev in
let var = prterm_env ctx c in
- [< 'sTR"Tried to define "; 'sTR id;
- 'sTR" with a term using variable "; var; 'sPC;
- 'sTR"which is not in its scope." >]
+ str"Tried to define " ++ str id ++
+ str" with a term using variable " ++ var ++ spc () ++
+ str"which is not in its scope."
let explain_var_not_found ctx id =
- [< 'sTR "The variable"; 'sPC; 'sTR (string_of_id id);
- 'sPC ; 'sTR "was not found";
- 'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
+ str "The variable" ++ spc () ++ str (string_of_id id) ++
+ spc () ++ str "was not found" ++
+ spc () ++ str "in the current" ++ spc () ++ str "environment"
let explain_wrong_case_info ctx ind ci =
let pi = prterm (mkInd ind) in
if ci.ci_ind = ind then
- [< 'sTR"Cases expression on an object of inductive"; 'sPC; pi;
- 'sPC; 'sTR"has invalid information" >]
+ str"Cases expression on an object of inductive" ++ spc () ++ pi ++
+ spc () ++ str"has invalid information"
else
let pc = prterm (mkInd ci.ci_ind) in
- [< 'sTR"A term of inductive type"; 'sPC; pi; 'sPC;
- 'sTR"was given to a Cases expression on the inductive type";
- 'sPC; pc >]
+ str"A term of inductive type" ++ spc () ++ pi ++ spc () ++
+ str"was given to a Cases expression on the inductive type" ++
+ spc () ++ pc
let explain_type_error ctx = function
@@ -353,52 +356,52 @@ let explain_pretype_error ctx = function
(* Refiner errors *)
let explain_refiner_bad_type arg ty conclty =
- [< 'sTR"refiner was given an argument"; 'bRK(1,1);
- prterm arg; 'sPC;
- 'sTR"of type"; 'bRK(1,1); prterm ty; 'sPC;
- 'sTR"instead of"; 'bRK(1,1); prterm conclty >]
+ str"refiner was given an argument" ++ brk(1,1) ++
+ prterm arg ++ spc () ++
+ str"of type" ++ brk(1,1) ++ prterm ty ++ spc () ++
+ str"instead of" ++ brk(1,1) ++ prterm conclty
let explain_refiner_occur_meta t =
- [< 'sTR"cannot refine with term"; 'bRK(1,1); prterm t;
- 'sPC; 'sTR"because there are metavariables, and it is";
- 'sPC; 'sTR"neither an application nor a Case" >]
+ str"cannot refine with term" ++ brk(1,1) ++ prterm t ++
+ spc () ++ str"because there are metavariables, and it is" ++
+ spc () ++ str"neither an application nor a Case"
let explain_refiner_occur_meta_goal t =
- [< 'sTR"generated subgoal"; 'bRK(1,1); prterm t;
- 'sPC; 'sTR"has metavariables in it" >]
+ str"generated subgoal" ++ brk(1,1) ++ prterm t ++
+ spc () ++ str"has metavariables in it"
let explain_refiner_cannot_applt t harg =
- [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
- prterm t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
- prterm harg >]
+ str"in refiner, a term of type " ++ brk(1,1) ++
+ prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
+ prterm harg
let explain_refiner_cannot_unify m n =
let pm = prterm m in
let pn = prterm n in
- [< 'sTR"Impossible to unify"; 'bRK(1,1) ; pm; 'sPC ;
- 'sTR"with"; 'bRK(1,1) ; pn >]
+ str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
+ str"with" ++ brk(1,1) ++ pn
let explain_refiner_cannot_generalize ty =
- [< 'sTR "Cannot find a well-typed generalisation of the goal with type : ";
- prterm ty >]
+ str "Cannot find a well-typed generalisation of the goal with type : " ++
+ prterm ty
let explain_refiner_not_well_typed c =
- [< 'sTR"The term " ; prterm c ; 'sTR" is not well-typed" >]
+ str"The term " ++ prterm c ++ str" is not well-typed"
let explain_refiner_bad_tactic_args s l =
- [< 'sTR "Internal tactic "; 'sTR s; 'sTR " cannot be applied to ";
- Tacmach.pr_tactic (s,l) >]
+ str "Internal tactic " ++ str s ++ str " cannot be applied to " ++
+ Tacmach.pr_tactic (s,l)
let explain_intro_needs_product () =
- [< 'sTR "Introduction tactics needs products" >]
+ str "Introduction tactics needs products"
let explain_does_not_occur_in c hyp =
- [< 'sTR "The term"; 'sPC; prterm c; 'sPC; 'sTR "does not occur in";
- 'sPC; pr_id hyp >]
+ str "The term" ++ spc () ++ prterm c ++ spc () ++ str "does not occur in" ++
+ spc () ++ pr_id hyp
let explain_non_linear_proof c =
- [< 'sTR "cannot refine with term"; 'bRK(1,1); prterm c;
- 'sPC; 'sTR"because a metavariable has several occurrences" >]
+ str "cannot refine with term" ++ brk(1,1) ++ prterm c ++
+ spc () ++ str"because a metavariable has several occurrences"
let explain_refiner_error = function
| BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
@@ -418,20 +421,20 @@ let explain_refiner_error = function
let error_non_strictly_positive env c v =
let pc = prterm_env env c in
let pv = prterm_env env v in
- [< 'sTR "Non strictly positive occurrence of "; pv; 'sTR " in";
- 'bRK(1,1); pc >]
+ str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
+ brk(1,1) ++ pc
let error_ill_formed_inductive env c v =
let pc = prterm_env env c in
let pv = prterm_env env v in
- [< 'sTR "Not enough arguments applied to the "; pv;
- 'sTR " in"; 'bRK(1,1); pc >]
+ str "Not enough arguments applied to the " ++ pv ++
+ str " in" ++ brk(1,1) ++ pc
let error_ill_formed_constructor env c v =
let pc = prterm_env env c in
let pv = prterm_env env v in
- [< 'sTR "The conclusion of"; 'bRK(1,1); pc; 'bRK(1,1);
- 'sTR "is not valid;"; 'bRK(1,1); 'sTR "it must be built from "; pv >]
+ str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++
+ str "is not valid ++" ++ brk(1,1) ++ str "it must be built from " ++ pv
let str_of_nth n =
(string_of_int n)^
@@ -445,38 +448,38 @@ let error_bad_ind_parameters env c n v1 v2 =
let pc = prterm_env_at_top env c in
let pv1 = prterm_env env v1 in
let pv2 = prterm_env env v2 in
- [< 'sTR ("The "^(str_of_nth n)^" argument of "); pv2; 'bRK(1,1);
- 'sTR "must be "; pv1; 'sTR " in"; 'bRK(1,1); pc >]
+ str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++
+ str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc
let error_same_names_types id =
- [< 'sTR "The name"; 'sPC; pr_id id; 'sPC;
- 'sTR "is used twice is the inductive types definition." >]
+ str "The name" ++ spc () ++ pr_id id ++ spc () ++
+ str "is used twice is the inductive types definition."
let error_same_names_constructors id cid =
- [< 'sTR "The constructor name"; 'sPC; pr_id cid; 'sPC;
- 'sTR "is used twice is the definition of type"; 'sPC;
- pr_id id >]
+ str "The constructor name" ++ spc () ++ pr_id cid ++ spc () ++
+ str "is used twice is the definition of type" ++ spc () ++
+ pr_id id
let error_not_an_arity id =
- [< 'sTR "The type of"; 'sPC; pr_id id; 'sPC; 'sTR "is not an arity." >]
+ str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity."
let error_bad_entry () =
- [< 'sTR "Bad inductive definition." >]
+ str "Bad inductive definition."
let error_not_allowed_case_analysis dep kind i =
- [< 'sTR (if dep then "Dependent" else "Non Dependent");
- 'sTR " case analysis on sort: "; print_sort kind; 'fNL;
- 'sTR "is not allowed for inductive definition: ";
- pr_inductive (Global.env()) i >]
+ str (if dep then "Dependent" else "Non Dependent") ++
+ str " case analysis on sort: " ++ print_sort kind ++ fnl () ++
+ str "is not allowed for inductive definition: " ++
+ pr_inductive (Global.env()) i
let error_bad_induction dep indid kind =
- [<'sTR (if dep then "Dependent" else "Non dependent");
- 'sTR " induction for type "; pr_id indid;
- 'sTR " and sort "; print_sort kind; 'sPC;
- 'sTR "is not allowed">]
+ str (if dep then "Dependent" else "Non dependent") ++
+ str " induction for type " ++ pr_id indid ++
+ str " and sort " ++ print_sort kind ++ spc () ++
+ str "is not allowed"
let error_not_mutual_in_scheme () =
- [< 'sTR "Induction schemes is concerned only with mutually inductive types" >]
+ str "Induction schemes is concerned only with mutually inductive types"
let explain_inductive_error = function
(* These are errors related to inductive constructions *)
@@ -499,59 +502,58 @@ let explain_inductive_error = function
let explain_bad_pattern ctx cstr ty =
let pt = prterm_env ctx ty in
let pc = pr_constructor ctx cstr in
- [< 'sTR "Found the constructor "; pc; 'bRK(1,1);
- 'sTR "while matching a term of type "; pt; 'bRK(1,1);
- 'sTR "which is not an inductive type" >]
+ str "Found the constructor " ++ pc ++ brk(1,1) ++
+ str "while matching a term of type " ++ pt ++ brk(1,1) ++
+ str "which is not an inductive type"
let explain_bad_constructor ctx cstr ind =
let pi = pr_inductive ctx ind in
(* let pc = pr_constructor ctx cstr in*)
let pt = pr_inductive ctx (inductive_of_constructor cstr) in
- [< 'sTR "Found a constructor of inductive type "; pt; 'bRK(1,1) ;
- 'sTR "while a constructor of " ; pi; 'bRK(1,1) ;
- 'sTR "is expected" >]
+ str "Found a constructor of inductive type " ++ pt ++ brk(1,1) ++
+ str "while a constructor of " ++ pi ++ brk(1,1) ++
+ str "is expected"
let explain_wrong_numarg_of_constructor ctx cstr n =
let pc = pr_constructor ctx cstr in
- [<'sTR "The constructor "; pc; 'sTR " expects " ;
- if n = 0 then [< 'sTR "no argument.">]
- else if n = 1 then [< 'sTR "1 argument.">]
- else [< 'iNT n ; 'sTR " arguments.">]
- >]
+ str "The constructor " ++ pc ++ str " expects " ++
+ (if n = 0 then str "no argument." else if n = 1 then str "1 argument."
+ else (int n ++ str " arguments."))
let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity=
let pp = prterm_env ctx pred in
- [<'sTR "The elimination predicate "; 'sPC; pp; 'fNL;
- 'sTR "should be of arity" ; 'sPC;
- prterm_env ctx nondep_arity ; 'sPC; 'sTR "(for non dependent case) or" ;
- 'sPC; prterm_env ctx dep_arity ; 'sPC; 'sTR "(for dependent case).">]
+ str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++
+ str "should be of arity" ++ spc () ++
+ prterm_env ctx nondep_arity ++ spc () ++
+ str "(for non dependent case) or" ++
+ spc () ++ prterm_env ctx dep_arity ++ spc () ++ str "(for dependent case)."
let explain_needs_inversion ctx x t =
let px = prterm_env ctx x in
let pt = prterm_env ctx t in
- [< 'sTR "Sorry, I need inversion to compile pattern matching of term ";
- px ; 'sTR " of type: "; pt>]
+ str "Sorry, I need inversion to compile pattern matching of term " ++
+ px ++ str " of type: " ++ pt
let explain_unused_clause env pats =
let s = if List.length pats > 1 then "s" else "" in
(* Without localisation
- [<'sTR ("Unused clause with pattern"^s); 'sPC;
- hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats); 'sTR ")" >]
+ (str ("Unused clause with pattern"^s) ++ spc () ++
+ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
*)
- [<'sTR "This clause is redundant" >]
+ str "This clause is redundant"
let explain_non_exhaustive env pats =
let s = if List.length pats > 1 then "s" else "" in
- [<'sTR ("Non exhaustive pattern-matching: no clause found for pattern"^s);
- 'sPC; hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats) >]
+ str ("Non exhaustive pattern-matching: no clause found for pattern"^s) ++
+ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats)
let explain_cannot_infer_predicate env typs =
let pr_branch (cstr,typ) =
let cstr,_ = decompose_app cstr in
- [< 'sTR "For "; prterm_env env cstr; 'sTR " : "; prterm_env env typ >]
+ str "For " ++ prterm_env env cstr ++ str " : " ++ prterm_env env typ
in
- [<'sTR "Unable to unify the types found in the branches:";
- 'sPC; hOV 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) >]
+ str "Unable to unify the types found in the branches:" ++
+ spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
let explain_pattern_matching_error env = function
| BadPattern (c,t) ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ec311d9ae..487c87bd4 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -226,10 +226,10 @@ let add_infix assoc n inf pr =
(* check the precedence *)
if n<1 or n>10 then
errorlabstrm "Metasyntax.infix_grammar_entry"
- [< 'sTR"Precedence must be between 1 and 10." >];
+ (str"Precedence must be between 1 and 10.");
if (assoc<>None) & (n<6 or n>9) then
errorlabstrm "Vernacentries.infix_grammar_entry"
- [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >];
+ (str"Associativity Precedence must be 6,7,8 or 9.");
(* check the grammar entry *)
let prefname = inf^"_infix" in
let gram_rule = gram_infix assoc n (split inf) prefname pr in
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 3ad4ab41c..610f8afa3 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -50,7 +50,7 @@ let check c =
let (j,u) = safe_infer !env c in
let ty = j_type j in
let pty = pr_term CCI (env_of_safe_env !env) ty in
- mSGNL (hOV 0 [< 'sTR" :"; 'sPC; hOV 0 pty; 'fNL >])
+ mSGNL (hov 0 (str" :" ++ spc () ++ hov 0 pty ++ fnl ()))
let definition id ty c =
let c = globalize [] c in
@@ -58,20 +58,20 @@ let definition id ty c =
let ce = { const_entry_body = c; const_entry_type = ty } in
let sp = make_path [] id CCI in
env := add_constant sp ce (locals()) !env;
- mSGNL (hOV 0 [< pr_id id; 'sPC; 'sTR"is defined"; 'fNL >])
+ mSGNL (hov 0 (pr_id id ++ spc () ++ str"is defined" ++ fnl ()))
let parameter id t =
let t = globalize [] t in
let sp = make_path [] id CCI in
env := add_parameter sp t (locals()) !env;
- mSGNL (hOV 0 [< 'sTR"parameter"; 'sPC; pr_id id;
- 'sPC; 'sTR"is declared"; 'fNL >])
+ mSGNL (hov 0 (str"parameter" ++ spc () ++ pr_id id ++
+ spc () ++ str"is declared" ++ fnl ()))
let variable id t =
let t = globalize [] t in
env := push_named_assum (id,t) !env;
- mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; pr_id id;
- 'sPC; 'sTR"is declared"; 'fNL >])
+ mSGNL (hov 0 (str"variable" ++ spc () ++ pr_id id ++
+ spc () ++ str"is declared" ++ fnl ()))
let inductive par inds =
let nparams = List.length par in
@@ -97,7 +97,7 @@ let inductive par inds =
let mi1 = List.hd inds in
make_path [] mi1.mind_entry_typename CCI in
env := add_mind sp mie (locals()) !env;
- mSGNL (hOV 0 [< 'sTR"inductive type(s) are declared"; 'fNL >])
+ mSGNL (hov 0 (str"inductive type(s) are declared" ++ fnl ()))
let execute = function
@@ -122,12 +122,12 @@ module Explain = Fhimsg.Make(struct let pr_term = pr_term end)
let rec explain_exn = function
| TypeError (k,ctx,te) ->
- mSGNL (hOV 0 [< 'sTR "type error:"; 'sPC;
- Explain.explain_type_error k ctx te; 'fNL >])
+ mSGNL (hov 0 (str "type error:" ++ spc () ++
+ Explain.explain_type_error k ctx te ++ fnl ()))
| Stdpp.Exc_located (_,exn) ->
explain_exn exn
| exn ->
- mSGNL (hOV 0 [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >])
+ mSGNL (hov 0 (str"error: " ++ str (Printexc.to_string exn) ++ fnl ()))
let top () =
let cs = Stream.of_channel stdin in
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 3fc937724..d9325a2e7 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -89,7 +89,7 @@ let ocaml_toploop () =
| _ -> ()
(*
errorlabstrm "Mltop.ocaml_toploop"
- [< 'sTR"Cannot access the ML toplevel" >]
+ [< str"Cannot access the ML toplevel" >]
*)
(* Dynamic loading of .cmo *)
@@ -101,11 +101,11 @@ let dir_ml_load s =
with
| (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
| _ -> errorlabstrm "Mltop.load_object"
- [< 'sTR"Cannot link ml-object "; 'sTR s;
- 'sTR" to Coq code." >]
+ [< str"Cannot link ml-object "; str s;
+ str" to Coq code." >]
else
errorlabstrm "Mltop.load_object"
- [< 'sTR"File not found on loadpath : "; 'sTR s >]
+ [< str"File not found on loadpath : "; str s >]
| WithoutTop ->
ifdef Byte then
(if is_in_path !coq_mlpath_copy s then
@@ -119,14 +119,14 @@ let dir_ml_load s =
with
| Dynlink.Error(a) ->
errorlabstrm "Mltop.load_object"
- [< 'sTR (Dynlink.error_message a) >]
+ [< str (Dynlink.error_message a) >]
else errorlabstrm "Mltop.load_object"
- [< 'sTR"File not found on loadpath : "; 'sTR s >])
+ [< str"File not found on loadpath : "; str s >])
else
()
| Native ->
errorlabstrm "Mltop.no_load_object"
- [< 'sTR"Loading of ML object file forbidden in a native Coq" >]
+ [< str"Loading of ML object file forbidden in a native Coq" >]
(* Dynamic interpretation of .ml *)
let dir_ml_use s =
@@ -147,14 +147,14 @@ let add_rec_ml_dir dir =
(* Adding files to Coq and ML loadpath *)
-let add_path dir coq_dirpath =
+let add_path ~unix_path:dir ~coq_root:coq_dirpath =
if exists_dir dir then
begin
add_ml_dir dir;
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
@@ -164,7 +164,7 @@ let convert_string d =
flush_all ();
failwith "caught"
-let add_rec_path dir coq_dirpath =
+let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
let dirs = all_subdirs dir in
let prefix = Names.repr_dirpath coq_dirpath in
if dirs <> [] then
@@ -177,7 +177,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) >]
(* convertit un nom quelconque en nom de fichier ou de module *)
let mod_of_name name =
@@ -244,7 +244,7 @@ let unfreeze_ml_modules x =
load_object mname fname
else
errorlabstrm "Mltop.unfreeze_ml_modules"
- [< 'sTR"Loading of ML object file forbidden in a native Coq" >];
+ [< str"Loading of ML object file forbidden in a native Coq" >];
add_loaded_module mname)
x
@@ -266,11 +266,11 @@ let cache_ml_module_object (_,{mnames=mnames}) =
begin
try
if_verbose
- mSG [< 'sTR"[Loading ML file "; 'sTR fname; 'sTR" ..." >];
+ msg [< str"[Loading ML file "; str fname; str" ..." >];
load_object mname fname;
- if_verbose mSGNL [< 'sTR"done]" >]
+ if_verbose msgnl [< str"done]" >]
with e ->
- if_verbose mSGNL [< 'sTR"failed]" >];
+ if_verbose msgnl [< str"failed]" >];
raise e
end;
add_loaded_module mname)
@@ -290,11 +290,11 @@ let declare_ml_modules l =
let print_ml_path () =
let l = !coq_mlpath_copy in
- pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR" ";
- hV 0 (prlist_with_sep pr_fnl pr_str l) >]
+ ppnl [< str"ML Load Path:"; fnl (); str" ";
+ hv 0 (prlist_with_sep pr_fnl pr_str l) >]
(* Printing of loaded ML modules *)
let print_ml_modules () =
let l = get_loaded_modules () in
- pP [< 'sTR"Loaded ML Modules: " ; pr_vertical_list pr_str l >]
+ pp [< str"Loaded ML Modules: " ; pr_vertical_list pr_str l >]
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index 66a41e2c1..730b6768d 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -32,7 +32,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 () =
let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun _ -> raise Sys.Break)) in
@@ -50,14 +50,14 @@ let global_request_id = ref 013
let acknowledge_command_ref =
ref(fun request_id command_count opt_exn
- -> [<'fNL; 'sTR "acknowledge command number ";
- 'iNT request_id; 'fNL;
- 'sTR "successfully executed "; 'iNT command_count; 'fNL;
- 'sTR "error message"; 'fNL;
+ -> (fnl () ++ str "acknowledge command number " ++
+ int request_id ++ fnl () ++
+ str "successfully executed " ++ int command_count ++ fnl () ++
+ str "error message" ++ 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>])
+ | None -> (mt ())) ++ fnl () ++
+ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ()))
let set_acknowledge_command f =
acknowledge_command_ref := f
@@ -168,6 +168,6 @@ let protected_loop input_chan =
explain_and_restart e
| e -> explain_and_restart e in
begin
- mSGNL [<'sTR "Starting Centaur Specialized loop" >];
+ msgnl (str "Starting Centaur Specialized loop");
looprec input_chan
end
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 2f294af98..71443abb5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -76,26 +76,26 @@ let warning_or_error coe indsp err =
let st = match err with
| MissingProj (fi,projs) ->
let s,have = if List.length projs > 1 then "s","have" else "","has" in
- [< 'sTR(string_of_id fi);
- 'sTR" cannot be defined because the projection"; 'sTR s; 'sPC;
- prlist_with_sep pr_coma pr_id projs; 'sPC; 'sTR have; 'sTR "n't." >]
+ (str(string_of_id fi) ++
+ str" cannot be defined because the projection" ++ str s ++ spc () ++
+ prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ str "n't.")
| BadTypedProj (fi,ctx,te) ->
match te with
| ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
- [<'sTR (string_of_id fi);
- 'sTR" cannot be defined because it is informative and ";
- Printer.pr_inductive (Global.env()) indsp;
- 'sTR " is not." >]
+ (str (string_of_id fi) ++
+ str" cannot be defined because it is informative and " ++
+ Printer.pr_inductive (Global.env()) indsp ++
+ str " is not.")
| ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
- [<'sTR (string_of_id fi);
- 'sTR" cannot be defined because it is large and ";
- Printer.pr_inductive (Global.env()) indsp;
- 'sTR " is not." >]
+ (str (string_of_id fi) ++
+ str" cannot be defined because it is large and " ++
+ Printer.pr_inductive (Global.env()) indsp ++
+ str " is not.")
| _ ->
- [<'sTR " cannot be defined because it is not typable" >]
+ (str " cannot be defined because it is not typable")
in
if coe then errorlabstrm "structure" st;
- Options.if_verbose pPNL (hOV 0 [< 'sTR"Warning: "; st >])
+ Options.if_verbose ppnl (hov 0 (str"Warning: " ++ st))
(* We build projections *)
let declare_projections indsp coers fields =
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index b065d7b57..50f2ef83b 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -31,8 +31,8 @@ let typ_lams_of t =
let objdef_err ref =
errorlabstrm "object_declare"
- [< pr_id (Termops.id_of_global (Global.env()) ref);
- 'sTR" is not a structure object" >]
+ (pr_id (Termops.id_of_global (Global.env()) ref) ++
+ str" is not a structure object")
let objdef_declare ref =
let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 00be368af..972fd22b4 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -55,7 +55,7 @@ let prompt_char ic ibuf count =
| ll::_ -> ibuf.len == ll
| [] -> ibuf.len == 0
in
- if bol then mSGERR [< 'sTR (ibuf.prompt()) >];
+ if bol then msgerr (str (ibuf.prompt()));
try
let c = input_char ic in
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -109,31 +109,31 @@ let print_highlight_location ib (bp,ep) =
let highlight_lines =
match get_bols_of_loc ib (bp,ep) with
| ([],(bl,el)) ->
- [< 'sTR"> "; 'sTR(String.sub ib.str bl (el-bl-1)); 'fNL;
- 'sTR"> "; 'sTR(String.make (bp-bl) ' ');
- 'sTR(String.make (ep-bp) '^') >]
+ (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++
+ str"> " ++ str(String.make (bp-bl) ' ') ++
+ str(String.make (ep-bp) '^'))
| ((b1,e1)::ml,(bn,en)) ->
let (d1,s1) = dotted_location (b1,bp) in
let (dn,sn) = dotted_location (ep,en) in
- let l1 = [< 'sTR"> "; 'sTR d1; 'sTR s1;
- 'sTR(String.sub ib.str bp (e1-bp)) >] in
+ let l1 = (str"> " ++ str d1 ++ str s1 ++
+ str(String.sub ib.str bp (e1-bp))) in
let li =
prlist (fun (bi,ei) ->
- [< 'sTR"> "; 'sTR(String.sub ib.str bi (ei-bi)) >]) ml in
- let ln = [< 'sTR"> "; 'sTR(String.sub ib.str bn (ep-bn));
- 'sTR sn; 'sTR dn >] in
- [< l1; li; ln >]
+ (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in
+ let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++
+ str sn ++ str dn) in
+ (l1 ++ li ++ ln)
in
- [< 'sTR"Toplevel input, characters "; Errors.print_loc (bp,ep); 'fNL;
- highlight_lines; 'fNL >]
+ (str"Toplevel input, characters " ++ Errors.print_loc (bp,ep) ++ fnl () ++
+ highlight_lines ++ fnl ())
(* Functions to report located errors in a file. *)
let print_location_in_file s fname (bp,ep) =
- let errstrm = [< 'sTR"Error while reading "; 'sTR s; 'sTR" :"; 'fNL;
- 'sTR"File "; 'sTR ("\""^fname^"\"") >] in
+ let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl () ++
+ str"File " ++ str ("\""^fname^"\"")) in
if (bp,ep) = Ast.dummy_loc then
- [< errstrm; 'sTR", unknown location."; 'fNL >]
+ (errstrm ++ str", unknown location." ++ fnl ())
else
let ic = open_in fname in
let rec line_of_pos lin bol cnt =
@@ -146,16 +146,16 @@ let print_location_in_file s fname (bp,ep) =
try
let (line, bol) = line_of_pos 1 0 0 in
close_in ic;
- [< errstrm; 'sTR", line "; 'iNT line;
- 'sTR", characters "; Errors.print_loc (bp-bol,ep-bol); 'fNL >]
- with e -> (close_in ic; [< errstrm; 'sTR", invalid location."; 'fNL >])
+ (errstrm ++ str", line " ++ int line ++
+ str", characters " ++ Errors.print_loc (bp-bol,ep-bol) ++ fnl ())
+ with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ()))
let print_command_location ib dloc =
match dloc with
| Some (bp,ep) ->
- [< 'sTR"Error during interpretation of command:"; 'fNL;
- 'sTR(String.sub ib.str (bp-ib.start) (ep-bp)); 'fNL >]
- | None -> [<>]
+ (str"Error during interpretation of command:" ++ fnl () ++
+ str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
+ | None -> (mt ())
let valid_loc dloc (b,e) =
(b,e) <> Ast.dummy_loc
@@ -185,7 +185,7 @@ let top_buffer =
str = "";
len = 0;
bols = [];
- tokens = Gram.parsable [<>];
+ tokens = Gram.parsable (Stream.of_list []);
start = 0 }
let set_prompt prompt =
@@ -217,32 +217,32 @@ let print_toplevel_error exc =
if valid_buffer_loc top_buffer dloc loc then
(print_highlight_location top_buffer loc, ie)
else
- ([<>] (* print_command_location top_buffer dloc *), ie)
+ ((mt ()) (* print_command_location top_buffer dloc *), ie)
| Error_in_file (s, (fname, loc), ie) ->
(print_location_in_file s fname loc, ie)
| _ ->
- ([<>] (* print_command_location top_buffer dloc *), exc)
+ ((mt ()) (* print_command_location top_buffer dloc *), exc)
in
match exc with
| End_of_input ->
- mSGERRNL [<>]; pp_flush(); exit 0
+ msgerrnl (mt ()); pp_flush(); exit 0
| Vernacinterp.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise Vernacinterp.Drop;
- [< 'sTR"Error: There is no ML toplevel."; 'fNL >]
+ (str"Error: There is no ML toplevel." ++ fnl ())
| Vernacinterp.ProtectedLoop ->
raise Vernacinterp.ProtectedLoop
| Vernacinterp.Quit ->
raise Vernacinterp.Quit
| _ ->
- [< if is_pervasive_exn exc then [<>] else locstrm;
- Errors.explain_exn exc >]
+ (if is_pervasive_exn exc then (mt ()) else locstrm ++
+ Errors.explain_exn exc)
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
- let rec dot = parser
- | [< '("", ".") >] -> ()
- | [< '("EOI", "") >] -> raise End_of_input
- | [< '_; s >] -> dot s
+ let rec dot st = match Stream.next st with
+ | ("", ".") -> ()
+ | ("EOI", "") -> raise End_of_input
+ | _ -> dot st
in
Gram.Entry.of_parser "Coqtoplevel.dot" dot
@@ -275,13 +275,13 @@ let process_error = function
Otherwise, exit.
End_of_input: Ctrl-D was typed in, we will quit *)
let do_vernac () =
- mSGERRNL [<>];
+ msgerrnl (mt ());
resynch_buffer top_buffer;
begin
try
raw_do_vernac top_buffer.tokens
with e ->
- mSGNL (print_toplevel_error (process_error e))
+ msgnl (print_toplevel_error (process_error e))
end;
flush_all()
@@ -309,10 +309,10 @@ let rec coq_switch b =
| Vernacinterp.ProtectedLoop ->
Lib.declare_initial_state();
coq_switch false
- | End_of_input -> mSGERRNL [<>]; pp_flush(); exit 0
+ | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
| Vernacinterp.Quit -> exit 0
| e ->
- mSGERRNL [< 'sTR"Anomaly: toplevel loop. Please report." >];
+ msgerrnl (str"Anomaly: toplevel loop. Please report.");
coq_switch b
let loop () = coq_switch true
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b7d34070a..3562acd7a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -111,8 +111,8 @@ let rec vernac interpfun input =
let tstart = System.get_time() in
interp v;
let tend = System.get_time() in
- mSGNL [< 'sTR"Finished transaction in " ;
- System.fmt_time_difference tstart tend >]
+ msgnl (str"Finished transaction in " ++
+ System.fmt_time_difference tstart tend)
| _ -> if not !just_parsing then interpfun com
in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1ce0e27a1..d5366f8c6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -58,85 +58,85 @@ let show_script () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- mSGNL(Refiner.print_script true evc (Global.named_context()) pf)
+ msgnl(Refiner.print_script true evc (Global.named_context()) pf)
let show_prooftree () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- mSG(Refiner.print_proof evc (Global.named_context()) pf)
+ msg(Refiner.print_proof evc (Global.named_context()) pf)
let show_open_subgoals () =
let pfts = get_pftreestate () in
- mSG(pr_subgoals_of_pfts pfts)
+ msg(pr_subgoals_of_pfts pfts)
let show_nth_open_subgoal n =
let pf = proof_of_pftreestate (get_pftreestate ()) in
- mSG(pr_subgoal n (fst(frontier pf)))
+ msg(pr_subgoal n (fst(frontier pf)))
let show_open_subgoals_focused () =
let pfts = get_pftreestate () in
match focus() with
| 0 ->
- mSG(pr_subgoals_of_pfts pfts)
+ msg(pr_subgoals_of_pfts pfts)
| n ->
let pf = proof_of_pftreestate pfts in
let gls = fst(frontier pf) in
if n > List.length gls then
- (make_focus 0; mSG(pr_subgoals_of_pfts pfts))
+ (make_focus 0; msg(pr_subgoals_of_pfts pfts))
else if List.length gls < 2 then
- mSG(pr_subgoal n gls)
+ msg(pr_subgoal n gls)
else
- mSG (v 0 [< 'iNT(List.length gls); 'sTR" subgoals"; 'cUT;
- pr_subgoal n gls >])
+ msg (v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
+ pr_subgoal n gls))
let show_node () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and cursor = cursor_of_pftreestate pts in
- mSG [< prlist_with_sep pr_spc pr_int (List.rev cursor); 'fNL ;
- prgl pf.goal ; 'fNL ;
+ msg (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
+ prgl pf.goal ++ fnl () ++
(match pf.ref with
- | None -> [< 'sTR"BY <rule>" >]
+ | None -> (str"BY <rule>")
| Some(r,spfl) ->
- [< 'sTR"BY "; Refiner.pr_rule r; 'fNL; 'sTR" ";
- hOV 0 (prlist_with_sep pr_fnl prgl
- (List.map (fun p -> p.goal) spfl)) >]);
- 'fNL >]
+ (str"BY " ++ Refiner.pr_rule r ++ fnl () ++ str" " ++
+ hov 0 (prlist_with_sep pr_fnl prgl
+ (List.map (fun p -> p.goal) spfl)))) ++
+ fnl ())
let show_top_evars () =
let pfts = get_pftreestate () in
let gls = top_goal_of_pftreestate pfts in
let sigma = project gls in
- mSG (pr_evars_int 1 (Evd.non_instantiated sigma))
+ msg (pr_evars_int 1 (Evd.non_instantiated sigma))
let locate_file f =
try
let _,file =
System.where_in_path (Library.get_load_path()) f in
- mSG [< 'sTR file; 'fNL >]
+ msg (str file ++ fnl ())
with Not_found ->
- mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC;
- 'sTR"on loadpath"; 'fNL >])
+ msg (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
+ str"on loadpath" ++ fnl ()))
let print_located_qualid qid =
try
let sp = Nametab.sp_of_global (Global.env()) (Nametab.locate qid) in
- mSG [< pr_sp sp; 'fNL >]
+ msg (pr_sp sp ++ fnl ())
with Not_found ->
try
- mSG [< pr_sp (Syntax_def.locate_syntactic_definition qid); 'fNL >]
+ msg (pr_sp (Syntax_def.locate_syntactic_definition qid) ++ fnl ())
with Not_found ->
error ((Nametab.string_of_qualid qid) ^ " is not a defined object")
let print_path_entry (s,l) =
- [< 'sTR s; 'tBRK (0,2); 'sTR (string_of_dirpath l) >]
+ (str s ++ tbrk (0,2) ++ str (string_of_dirpath l))
let print_loadpath () =
let l = Library.get_full_load_path () in
- mSGNL (Pp.t [< 'sTR "Physical path: ";
- 'tAB; 'sTR "Logical Path:"; 'fNL;
- prlist_with_sep pr_fnl print_path_entry l >])
+ msgnl (Pp.t (str "Physical path: " ++
+ tab () ++ str "Logical Path:" ++ fnl () ++
+ prlist_with_sep pr_fnl print_path_entry l))
let get_current_context_of_args = function
| [VARG_NUMBER n] -> get_goal_context n
@@ -157,21 +157,21 @@ let _ =
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->
- mSG [< pr_dirpath fulldir; 'sTR " has been loaded from file"; 'fNL;
- 'sTR file; 'fNL >]
+ msg (pr_dirpath fulldir ++ str " has been loaded from file" ++ fnl () ++
+ str file ++ fnl ())
| Library.LibInPath, fulldir, file ->
- mSG [< pr_dirpath fulldir; 'sTR " is bound to file "; 'sTR file; 'fNL >]
+ msg (pr_dirpath fulldir ++ str " is bound to file " ++ str file ++ fnl ())
let msg_notfound_library qid = function
| Library.LibUnmappedDir ->
let dir = fst (Nametab.repr_qualid qid) in
errorlabstrm "locate_library"
- [< 'sTR "Cannot find a physical path bound to logical path ";
- pr_dirpath dir; 'fNL >]
+ (str "Cannot find a physical path bound to logical path " ++
+ pr_dirpath dir ++ fnl ())
| Library.LibNotFound ->
- mSG (hOV 0
- [< 'sTR"Unable to locate library";
- 'sPC; Nametab.pr_qualid qid; 'fNL >])
+ msg (hov 0
+ (str"Unable to locate library" ++
+ spc () ++ Nametab.pr_qualid qid ++ fnl ()))
| e -> assert false
let _ =
@@ -375,10 +375,10 @@ let _ =
and loaded = Library.loaded_modules () in
let loaded_opened = list_intersect loaded opened
and only_loaded = list_subtract loaded opened in
- mSG [< 'sTR"Loaded and imported modules: ";
- pr_vertical_list pr_dirpath loaded_opened; 'fNL;
- 'sTR"Loaded and not imported modules: ";
- pr_vertical_list pr_dirpath only_loaded >])
+ msg (str"Loaded and imported modules: " ++
+ pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++
+ str"Loaded and not imported modules: " ++
+ pr_vertical_list pr_dirpath only_loaded))
| _ -> bad_vernac_args "PrintModules")
(* Sections *)
@@ -516,7 +516,7 @@ let coercion_of_qualid loc qid =
let coe = Classops.coe_of_reference ref in
if not (Classops.coercion_exists coe) then
errorlabstrm "try_add_coercion"
- [< Printer.pr_global ref; 'sTR" is not a coercion" >];
+ (Printer.pr_global ref ++ str" is not a coercion");
coe
let _ = declare_bool_option
@@ -675,14 +675,14 @@ let _ =
let cursor = cursor_of_pftreestate pts in
let evc = evc_of_pftreestate pts in
let (pfterm,meta_types) = extract_open_pftreestate pts in
- mSGNL [< 'sTR"LOC: " ;
- prlist_with_sep pr_spc pr_int (List.rev cursor); 'fNL ;
- 'sTR"Subgoals" ; 'fNL ;
+ msgnl (str"LOC: " ++
+ prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
+ str"Subgoals" ++ fnl () ++
prlist
(fun (mv,ty) ->
- [< 'iNT mv ; 'sTR" -> " ; prtype ty ; 'fNL >])
- meta_types;
- 'sTR"Proof: " ; prterm (Evarutil.nf_evar evc pfterm) >])
+ (int mv ++ str" -> " ++ prtype ty ++ fnl ()))
+ meta_types ++
+ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm)))
| _ -> bad_vernac_args "ShowProof")
let _ =
@@ -698,11 +698,11 @@ let _ =
try
Inductiveops.control_only_guard (Evarutil.evar_env pf.goal)
pfterm;
- [< 'sTR "The condition holds up to here" >]
+ (str "The condition holds up to here")
with UserError(_,s) ->
- [< 'sTR ("Condition violated : ") ;s >]
+ (str ("Condition violated : ") ++s)
in
- mSGNL message)
+ msgnl message)
| _ -> bad_vernac_args "CheckGuard")
let _ =
@@ -729,7 +729,7 @@ let _ =
| (n::l) -> aux (Tacmach.traverse n pts) l in
let pts = aux pts (l@[-1]) in
let pf = proof_of_pftreestate pts in
- mSG (Refiner.print_script true evc (Global.named_context()) pf))
+ msg (Refiner.print_script true evc (Global.named_context()) pf))
let _ =
add "ExplainProofTree"
@@ -743,26 +743,26 @@ let _ =
| (n::l) -> aux (Tacmach.traverse n pts) l in
let pts = aux pts (l@[-1]) in
let pf = proof_of_pftreestate pts in
- mSG (Refiner.print_proof evc (Global.named_context()) pf))
+ msg (Refiner.print_proof evc (Global.named_context()) pf))
let _ =
add "ShowProofs"
(function [] ->
(fun () ->
let l = Pfedit.get_all_proof_names() in
- mSGNL (prlist_with_sep pr_spc pr_id l))
+ msgnl (prlist_with_sep pr_spc pr_id l))
| _ -> bad_vernac_args "ShowProofs")
let _ =
add "PrintAll"
(function
- | [] -> (fun () -> mSG(print_full_context_typ ()))
+ | [] -> (fun () -> msg(print_full_context_typ ()))
| _ -> bad_vernac_args "PrintAll")
let _ =
add "PRINT"
(function
- | [] -> (fun () -> mSG(print_local_context()))
+ | [] -> (fun () -> msg(print_local_context()))
| _ -> bad_vernac_args "PRINT")
(* Pris en compte dans PrintOption *)
@@ -770,19 +770,19 @@ let _ =
let _ =
add "PrintId"
(function
- | [VARG_QUALID qid] -> (fun () -> mSG(print_name qid))
+ | [VARG_QUALID qid] -> (fun () -> msg(print_name qid))
| _ -> bad_vernac_args "PrintId")
let _ =
add "PrintOpaqueId"
(function
- | [VARG_QUALID qid] -> (fun () -> mSG(print_opaque_name qid))
+ | [VARG_QUALID qid] -> (fun () -> msg(print_opaque_name qid))
| _ -> bad_vernac_args "PrintOpaqueId")
let _ =
add "PrintSec"
(function
- | [VARG_QUALID qid] -> (fun () -> mSG(print_sec_context_typ qid))
+ | [VARG_QUALID qid] -> (fun () -> msg(print_sec_context_typ qid))
| _ -> bad_vernac_args "PrintSec")
let _ = declare_bool_option
@@ -824,8 +824,8 @@ let _ =
fun () ->
begin
if (kind = "LETTOP") && not(refining ()) then
- errorlabstrm "Vernacentries.StartProof" [< 'sTR
- "Let declarations can only be used in proof editing mode" >];
+ errorlabstrm "Vernacentries.StartProof" (str
+ "Let declarations can only be used in proof editing mode");
start_proof_com (Some s) stre com;
if_verbose show_open_subgoals ()
end
@@ -863,15 +863,15 @@ let _ =
()
with e ->
if (is_unsafe "proof") && not (kind = "LETTOP") then begin
- mSGNL [< 'sTR "Warning: checking of theorem "; pr_id id;
- 'sPC; 'sTR "failed";
- 'sTR "... converting to Axiom" >];
+ msgnl (str "Warning: checking of theorem " ++ pr_id id ++
+ spc () ++ str "failed" ++
+ str "... converting to Axiom");
delete_proof id;
let _ = parameter_def_var id com in ()
end else
errorlabstrm "Vernacentries.TheoremProof"
- [< 'sTR "checking of theorem "; pr_id id; 'sPC;
- 'sTR "failed... aborting" >])
+ (str "checking of theorem " ++ pr_id id ++ spc () ++
+ str "failed... aborting"))
| _ -> bad_vernac_args "TheoremProof")
let _ =
@@ -964,7 +964,7 @@ let _ =
| VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g ->
let (evmap,sign) = get_current_context_of_args g in
let redfun = print_eval (reduction_of_redexp redexp) sign in
- fun () -> mSG (redfun (judgment_of_rawconstr evmap sign c))
+ fun () -> msg (redfun (judgment_of_rawconstr evmap sign c))
| _ -> bad_vernac_args "Eval")
let _ =
@@ -977,14 +977,14 @@ let _ =
let c = interp_constr evmap env c in
let senv = Global.safe_env() in
let j = Safe_typing.typing senv c in
- mSG (print_safe_judgment env j))
+ msg (print_safe_judgment env j))
| VARG_STRING "CHECK" :: VARG_CONSTR c :: g ->
(fun () ->
let (evmap, env) = get_current_context_of_args g in
let c = interp_constr evmap env c in
let (j,cst) = Typeops.infer env c in
let _ = Environ.add_constraints cst env in
- mSG (print_judgment env j))
+ msg (print_judgment env j))
| _ -> bad_vernac_args "Check")
@@ -1031,7 +1031,7 @@ let _ =
let _ =
add "INSPECT"
(function
- | [VARG_NUMBER n] -> (fun () -> mSG(inspect n))
+ | [VARG_NUMBER n] -> (fun () -> msg(inspect n))
| _ -> bad_vernac_args "INSPECT")
let _ =
@@ -1340,19 +1340,19 @@ let _ =
let _ =
add "PrintGRAPH"
(function
- | [] -> (fun () -> pPNL (Prettyp.print_graph()))
+ | [] -> (fun () -> ppnl (Prettyp.print_graph()))
| _ -> bad_vernac_args "PrintGRAPH")
let _ =
add "PrintCLASSES"
(function
- | [] -> (fun () -> pPNL (Prettyp.print_classes()))
+ | [] -> (fun () -> ppnl (Prettyp.print_classes()))
| _ -> bad_vernac_args "PrintCLASSES")
let _ =
add "PrintCOERCIONS"
(function
- | [] -> (fun () -> pPNL (Prettyp.print_coercions()))
+ | [] -> (fun () -> ppnl (Prettyp.print_coercions()))
| _ -> bad_vernac_args "PrintCOERCIONS")
let _ =
@@ -1360,7 +1360,7 @@ let _ =
(function
| [VARG_QUALID qids;VARG_QUALID qidt] ->
(fun () ->
- pPNL (Prettyp.print_path_between
+ ppnl (Prettyp.print_path_between
(cl_of_qualid qids) (cl_of_qualid qidt)))
| _ -> bad_vernac_args "PrintPATH")
@@ -1702,7 +1702,7 @@ let _ =
if (string_of_id t) = "Tables" then
print_tables ()
else
- mSG(print_name (Nametab.make_short_qualid t)))
+ msg(print_name (Nametab.make_short_qualid t)))
| _ -> bad_vernac_args "TableField")
@@ -1792,13 +1792,13 @@ let _ = vinterp_add "PrintMLModules"
let _ = vinterp_add "DumpUniverses"
(function
- | [] -> (fun () -> pP (Univ.pr_universes (Global.universes ())))
+ | [] -> (fun () -> pp (Univ.pr_universes (Global.universes ())))
| [VARG_STRING s] ->
(fun () -> let output = open_out s in
try
Univ.dump_universes output (Global.universes ());
close_out output;
- mSG [<'sTR ("Universes written to file \""^s^"\"."); 'fNL >]
+ msg (str ("Universes written to file \""^s^"\".") ++ fnl ())
with
e -> close_out output; raise e
)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 0b32cd141..039a42766 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -23,7 +23,7 @@ exception Quit
let disable_drop e =
if e <> Drop then e
- else UserError("Vernac.disable_drop",[< 'sTR"Drop is forbidden." >])
+ else UserError("Vernac.disable_drop",(str"Drop is forbidden."))
type vernac_arg =
| VARG_VARGLIST of vernac_arg list
@@ -54,7 +54,7 @@ let vinterp_add s f =
Hashtbl.add vernac_tab s f
with Failure _ ->
errorlabstrm "vinterp_add"
- [< 'sTR"Cannot add the vernac command " ; 'sTR s ; 'sTR" twice" >]
+ (str"Cannot add the vernac command " ++ str s ++ str" twice")
let overwriting_vinterp_add s f =
begin
@@ -69,7 +69,7 @@ let vinterp_map s =
Hashtbl.find vernac_tab s
with Not_found ->
errorlabstrm "Vernac Interpreter"
- [< 'sTR"Cannot find vernac command " ; 'sTR s >]
+ (str"Cannot find vernac command " ++ str s)
let vinterp_init () = Hashtbl.clear vernac_tab
@@ -110,8 +110,8 @@ let rec cvt_varg ast =
VARG_TACTIC_ARG (interp_tacarg ist targ)
| Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
| _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
- [< 'sTR "Unrecognizable ast node of vernac arg:";
- 'bRK(1,0); print_ast ast >])
+ (str "Unrecognizable ast node of vernac arg:" ++
+ brk(1,0) ++ print_ast ast))
(* Interpretation of a vernac command *)
@@ -128,7 +128,7 @@ let call (opn,converted_args) =
| ProtectedLoop -> raise ProtectedLoop
| e ->
if !Options.debug then
- mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR !loc >];
+ msgnl (str"Vernac Interpreter " ++ str !loc);
raise e
let interp = function
@@ -138,14 +138,14 @@ let interp = function
List.map cvt_varg argl
with e ->
if !Options.debug then
- mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR"Converting arguments" >];
+ msgnl (str"Vernac Interpreter " ++ str"Converting arguments");
raise e
in
call (opn,converted_args)
| cmd ->
errorlabstrm "Vernac Interpreter"
- [< 'sTR"Malformed vernac AST : " ; print_ast cmd >]
+ (str"Malformed vernac AST : " ++ print_ast cmd)
let bad_vernac_args s =
anomalylabstrm s
- [< 'sTR"Vernac "; 'sTR s; 'sTR" called with bad arguments" >]
+ (str"Vernac " ++ str s ++ str" called with bad arguments")
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 07:22:48 +0000