From 78d1c75322684eaa7e0ef753ee56d9c6140ec830 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 13 Dec 2001 09:03:13 +0000 Subject: compat ocaml 3.03 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenv.ml | 34 +++++----- proofs/logic.ml | 58 ++++++++--------- proofs/pfedit.ml | 36 +++++----- proofs/proof_trees.ml | 74 ++++++++++----------- proofs/refiner.ml | 106 +++++++++++++++--------------- proofs/tacinterp.ml | 174 ++++++++++++++++++++++++------------------------- proofs/tacmach.ml | 22 +++---- proofs/tactic_debug.ml | 27 ++++---- 8 files changed, 265 insertions(+), 266 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d73264e924..1a2ebd32ff 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -430,8 +430,8 @@ let clenv_assign mv rhs clenv = (* Streams are lazy, force evaluation of id to catch Not_found*) let id = Intmap.find mv clenv.namenv in errorlabstrm "clenv_assign" - [< 'sTR "An incompatible instantiation has already been found for "; - pr_id id >] + (str "An incompatible instantiation has already been found for " ++ + pr_id id) with Not_found -> anomaly "clenv_assign: non dependent metavar already assigned" else @@ -907,7 +907,7 @@ let clenv_lookup_name clenv id = match intmap_inv clenv.namenv id with | [] -> errorlabstrm "clenv_lookup_name" - [< 'sTR"No such bound variable "; pr_id id >] + (str"No such bound variable " ++ pr_id id) | [n] -> n | _ -> @@ -926,18 +926,18 @@ let clenv_match_args s clause = | Dep s -> if List.mem_assoc b t then errorlabstrm "clenv_match_args" - [< 'sTR "The variable "; pr_id s; - 'sTR " occurs more than once in binding" >] + (str "The variable " ++ pr_id s ++ + str " occurs more than once in binding") else clenv_lookup_name clause s | NoDep n -> if List.mem_assoc b t then errorlabstrm "clenv_match_args" - [< 'sTR "The position "; 'iNT n ; - 'sTR " occurs more than once in binding" >]; + (str "The position " ++ int n ++ + str " occurs more than once in binding"); (try List.nth mvs (n-1) with Failure "item" -> errorlabstrm "clenv_match_args" - [< 'sTR"No such binder" >]) + (str"No such binder")) | Com -> anomaly "No free term in clenv_match_args") in let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k) @@ -1092,7 +1092,7 @@ let make_clenv_binding_apply wc n (c,t) lbind = clenv_match_args lbind clause else errorlabstrm "make_clenv_bindings" - [<'sTR "Cannot mix bindings and free associations">] + (str "Cannot mix bindings and free associations") let make_clenv_binding wc (c,t) lbind = let largs = collect_com lbind in @@ -1105,7 +1105,7 @@ let make_clenv_binding wc (c,t) lbind = clenv_match_args lbind clause else errorlabstrm "make_clenv_bindings" - [<'sTR "Cannot mix bindings and free associations">] + (str "Cannot mix bindings and free associations") open Printer @@ -1113,15 +1113,15 @@ let pr_clenv clenv = let pr_name mv = try let id = Intmap.find mv clenv.namenv in - [< 'sTR"[" ; pr_id id ; 'sTR"]" >] - with Not_found -> [< >] + (str"[" ++ pr_id id ++ str"]") + with Not_found -> (mt ()) in let pr_meta_binding = function | (mv,Cltyp b) -> - hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " : " ; prterm b.rebus ; 'fNL >] + hov 0 (int mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ()) | (mv,Clval(b,_)) -> - hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " := " ; prterm b.rebus ; 'fNL >] + hov 0 (int mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ()) in - [< 'sTR"TEMPL: " ; prterm clenv.templval.rebus ; - 'sTR" : " ; prterm clenv.templtyp.rebus ; 'fNL ; - (prlist pr_meta_binding (intmap_to_list clenv.env)) >] + (str"TEMPL: " ++ prterm clenv.templval.rebus ++ + str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++ + (prlist pr_meta_binding (intmap_to_list clenv.env))) diff --git a/proofs/logic.ml b/proofs/logic.ml index 61edd06bf6..ea524791a4 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -180,8 +180,8 @@ and mk_casegoals sigma goal goalacc p c = let error_use_instantiate () = errorlabstrm "Logic.prim_refiner" - [< 'sTR"cannot intro when there are open metavars in the domain type"; - 'sPC; 'sTR"- use Instantiate" >] + (str"cannot intro when there are open metavars in the domain type" ++ + spc () ++ str"- use Instantiate") (* Auxiliary functions for primitive MOVE tactic * @@ -257,7 +257,7 @@ let apply_to_hyp2 env id f = found := true; f env d tail end else push_named_decl d env) - (named_context env) (reset_context env) + (named_context env) ~init:(reset_context env) in if (not !check) || !found then env' else error "No such assumption" @@ -363,7 +363,7 @@ let remove_hyp_body env sigma id = let b' = mkCast (b,t) in recheck_typability (Some id',id) env'' sigma b'); push_named_decl d env'') - tail env'); + tail ~init:env'); env') (* Primitive tactics are handled here *) @@ -667,67 +667,67 @@ open Printer let pr_prim_rule = function | {name=Intro;newids=[id]} -> - [< 'sTR"Intro " ; pr_id id >] + str"Intro " ++ pr_id id | {name=Intro_after;newids=[id]} -> - [< 'sTR"intro after " ; pr_id id >] + str"intro after " ++ pr_id id | {name=Intro_replacing;newids=[id]} -> - [< 'sTR"intro replacing " ; pr_id id >] + (str"intro replacing " ++ pr_id id) | {name=Cut b;terms=[t];newids=[id]} -> if b then - [< 'sTR"TrueCut "; prterm t >] + (str"TrueCut " ++ prterm t) else - [< 'sTR"Cut "; prterm t; 'sTR ";[Intro "; pr_id id; 'sTR "|Idtac]" >] + (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]") | {name=FixRule;newids=[f];params=[Num(_,n)]} -> - [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>] + (str"Fix " ++ pr_id f ++ str"/" ++ int n) | {name=FixRule;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> let rec print_mut = function (f::lf),((Num(_,n))::ln),(ar::lar) -> - [< pr_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar; - print_mut (lf,ln,lar)>] - | _ -> [<>] in - [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n; - 'sTR" with "; print_mut (lf,ln,lar) >] + pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ + print_mut (lf,ln,lar) + | _ -> (mt ()) in + (str"Fix " ++ pr_id f ++ str"/" ++ int n ++ + str" with " ++ print_mut (lf,ln,lar)) | {name=Cofix;newids=[f];terms=[]} -> - [< 'sTR"Cofix "; pr_id f >] + (str"Cofix " ++ pr_id f) | {name=Cofix;newids=(f::lf);terms=lar} -> let rec print_mut = function (f::lf),(ar::lar) -> - [< pr_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>] - | _ -> [<>] + (pr_id f ++ str" : " ++ prterm ar ++ print_mut (lf,lar)) + | _ -> (mt ()) in - [< 'sTR"Cofix "; pr_id f; 'sTR" with "; print_mut (lf,lar) >] + (str"Cofix " ++ pr_id f ++ str" with " ++ print_mut (lf,lar)) | {name=Refine;terms=[c]} -> - [< 'sTR(if occur_meta c then "Refine " else "Exact ") ; prterm c >] + (str(if occur_meta c then "Refine " else "Exact ") ++ prterm c) | {name=Convert_concl;terms=[c]} -> - [< 'sTR"Change " ; prterm c >] + (str"Change " ++ prterm c) | {name=Convert_hyp;hypspecs=[id];terms=[c]} -> - [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >] + (str"Change " ++ prterm c ++ spc () ++ str"in " ++ pr_id id) | {name=Convert_defbody;hypspecs=[id];terms=[c]} -> - [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >] + (str"Change " ++ prterm c ++ spc () ++ str"in " ++ pr_id id) | {name=Convert_deftype;hypspecs=[id];terms=[c]} -> - [< 'sTR"Change " ; prterm c ; 'sPC ; - 'sTR"in (Type of " ; pr_id id; 'sTR ")" >] + (str"Change " ++ prterm c ++ spc () ++ + str"in (Type of " ++ pr_id id ++ str ")") | {name=Thin;hypspecs=ids} -> - [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >] + (str"Clear " ++ prlist_with_sep pr_spc pr_id ids) | {name=ThinBody;hypspecs=ids} -> - [< 'sTR"ClearBody " ; prlist_with_sep pr_spc pr_id ids >] + (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids) | {name=Move withdep;hypspecs=[id1;id2]} -> - [< 'sTR (if withdep then "Dependent " else ""); - 'sTR"Move " ; pr_id id1; 'sTR " after "; pr_id id2 >] + (str (if withdep then "Dependent " else "") ++ + str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2) | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule" diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b148c019af..610e99b9f8 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -43,13 +43,13 @@ let get_all_proof_names () = Edit.dom proof_edits let msg_proofs use_resume = match Edit.dom proof_edits with - | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >] - | l -> [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ; - (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ; - 'sTR"." ; - (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >] - else [< >]) - >] + | [] -> (spc () ++ str"(No proof-editing in progress).") + | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ + (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++ + str"." ++ + (if use_resume then (fnl () ++ str"Use \"Resume\" first.") + else (mt ())) +) let undo_default = 12 let undo_limit = ref undo_default @@ -61,7 +61,7 @@ let undo_limit = ref undo_default let get_state () = match Edit.read proof_edits with | None -> errorlabstrm "Pfedit.get_state" - [< 'sTR"No focused proof"; msg_proofs true >] + (str"No focused proof" ++ msg_proofs true) | Some(_,pfs,ts) -> (pfs,ts) let get_topstate () = snd(get_state()) @@ -79,7 +79,7 @@ let set_current_proof s = Edit.focus proof_edits s with Invalid_argument "Edit.focus" -> errorlabstrm "Pfedit.set_proof" - [< 'sTR"No such proof" ; (msg_proofs false) >] + (str"No such proof" ++ (msg_proofs false)) let resume_proof = set_current_proof @@ -88,12 +88,12 @@ let suspend_proof () = Edit.unfocus proof_edits with Invalid_argument "Edit.unfocus" -> errorlabstrm "Pfedit.suspend_current_proof" - [< 'sTR"No active proof" ; (msg_proofs true) >] + (str"No active proof" ++ (msg_proofs true)) let resume_last_proof () = match (Edit.last_focused proof_edits) with | None -> - errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >] + errorlabstrm "resume_last" (str"No proof-editing in progress.") | Some p -> Edit.focus proof_edits p @@ -101,7 +101,7 @@ let get_current_proof_name () = match Edit.read proof_edits with | None -> errorlabstrm "Pfedit.get_proof" - [< 'sTR"No focused proof" ; msg_proofs true >] + (str"No focused proof" ++ msg_proofs true) | Some(na,_,_) -> na let add_proof (na,pfs,ts) = @@ -112,7 +112,7 @@ let delete_proof na = Edit.delete proof_edits na with (UserError ("Edit.delete",_)) -> errorlabstrm "Pfedit.delete_proof" - [< 'sTR"No such proof" ; msg_proofs false >] + (str"No such proof" ++ msg_proofs false) let init_proofs () = Edit.clear proof_edits @@ -121,7 +121,7 @@ let mutate f = Edit.mutate proof_edits (fun _ pfs -> f pfs) with Invalid_argument "Edit.mutate" -> errorlabstrm "Pfedit.mutate" - [< 'sTR"No focused proof" ; msg_proofs true >] + (str"No focused proof" ++ msg_proofs true) let start (na,ts) = let pfs = mk_pftreestate ts.top_goal in @@ -131,7 +131,7 @@ let restart_proof () = match Edit.read proof_edits with | None -> errorlabstrm "Pfedit.restart" - [< 'sTR"No focused proof to restart" ; msg_proofs true >] + (str"No focused proof to restart" ++ msg_proofs true) | Some(na,_,ts) -> delete_proof na; start (na,ts); @@ -166,7 +166,7 @@ let undo n = subtree - this solution only works properly if undoing one step *) if subtree_solved() then Edit.undo proof_edits 1 with (Invalid_argument "Edit.undo") -> - errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >] + errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) (*********************************************************************) (* Proof cooking *) @@ -193,8 +193,8 @@ let refining () = [] <> (Edit.dom proof_edits) let check_no_pending_proofs () = if refining () then errorlabstrm "check_no_pending_proofs" - [< 'sTR"Proof editing in progress" ; (msg_proofs false) ; - 'sTR"Use \"Abort All\" first or complete proof(s)." >] + (str"Proof editing in progress" ++ (msg_proofs false) ++ + str"Use \"Abort All\" first or complete proof(s).") let delete_current_proof () = delete_proof (get_current_proof_name ()) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index af106b1c4b..8e2a9b0eaf 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -116,36 +116,36 @@ let pr_goal g = let env = evar_env g in let penv = pr_context_of env in let pc = prterm_env_at_top env g.evar_concl in - [< 'sTR" "; hV 0 [< penv; 'fNL; - 'sTR (emacs_str (String.make 1 (Char.chr 253))) ; - 'sTR "============================"; 'fNL ; - 'sTR" " ; pc>]; 'fNL>] + str" " ++ hv 0 (penv ++ fnl () ++ + str (emacs_str (String.make 1 (Char.chr 253))) ++ + str "============================" ++ fnl () ++ + str" " ++ pc) ++ fnl () let pr_concl n g = let env = evar_env g in let pc = prterm_env_at_top env g.evar_concl in - [< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ; - 'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >] + str (emacs_str (String.make 1 (Char.chr 253))) ++ + str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc (* print the subgoals but write Subtree proved! even in case some existential variables remain unsolved, pr_subgoals_existential is a safer version of pr_subgoals *) let pr_subgoals = function - | [] -> [< 'sTR"Subtree proved!" ; 'fNL >] + | [] -> (str"Subtree proved!" ++ fnl ()) | [g] -> - let pg = pr_goal g in v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >] + let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg) | g1::rest -> let rec pr_rec n = function - | [] -> [< >] + | [] -> (mt ()) | g::rest -> let pg = pr_concl n g in let prest = pr_rec (n+1) rest in - [< 'cUT; pg; prest >] + (cut () ++ pg ++ prest) in let pg1 = pr_goal g1 in let pgr = pr_rec 2 rest in - v 0 [< 'iNT(List.length rest+1) ; 'sTR" subgoals" ;'cUT; pg1; pgr >] + v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ pgr) let pr_subgoal n = let rec prrec p = function @@ -153,7 +153,7 @@ let pr_subgoal n = | g::rest -> if p = 1 then let pg = pr_goal g in - v 0 [< 'sTR "subgoal ";'iNT n;'sTR " is:"; 'cUT; pg >] + v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg) else prrec (p-1) rest in @@ -165,85 +165,85 @@ let pr_seq evd = in let pdcl = pr_named_context_of env in let pcl = prterm_env_at_top env cl in - hOV 0 [< pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >] + hov 0 (pdcl ++ spc () ++ hov 0 (str"|- " ++ pcl)) let prgl gl = let pgl = pr_seq gl in - [< 'sTR"[" ; pgl ; 'sTR"]" ; 'sPC >] + (str"[" ++ pgl ++ str"]" ++ spc ()) let pr_evgl gl = let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in let pc = prterm gl.evar_concl in - hOV 0 [< 'sTR"[" ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >] + hov 0 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pc ++ str"]") let pr_evgl_sign gl = let ps = pr_named_context_of (evar_env gl) in let pc = prterm gl.evar_concl in - hOV 0 [< 'sTR"[" ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >] + hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]") (* evd.evgoal.lc seems to be printed twice *) let pr_decl evd = let pevgl = pr_evgl evd in let pb = match evd.evar_body with - | Evar_empty -> [< 'fNL >] - | Evar_defined c -> let pc = prterm c in [< 'sTR" => " ; pc; 'fNL >] + | Evar_empty -> (fnl ()) + | Evar_defined c -> let pc = prterm c in (str" => " ++ pc ++ fnl ()) in - h 0 [< pevgl; pb >] + h 0 (pevgl ++ pb) let pr_evd evd = prlist_with_sep pr_fnl (fun (ev,evd) -> let pe = pr_decl evd in - h 0 [< pr_id (id_of_existential ev) ; 'sTR"==" ; pe >]) + h 0 (pr_id (id_of_existential ev) ++ str"==" ++ pe)) (Evd.to_list evd) let pr_decls decls = pr_evd decls let pr_evc evc = let pe = pr_evd evc.sigma in - [< pe >] + (pe) let pr_evars = prlist_with_sep pr_fnl (fun (ev,evd) -> let pegl = pr_evgl_sign evd in - [< pr_id (id_of_existential ev); 'sTR " : "; pegl >]) + (pr_id (id_of_existential ev) ++ str " : " ++ pegl)) (* Print an enumerated list of existential variables *) let rec pr_evars_int i = function - | [] -> [< >] + | [] -> (mt ()) | (ev,evd)::rest -> let pegl = pr_evgl_sign evd in let pei = pr_evars_int (i+1) rest in - [< (hOV 0 [< 'sTR "Existential "; 'iNT i; 'sTR " ="; 'sPC; - pr_id (id_of_existential ev) ; 'sTR " : "; pegl >]); - 'fNL ; pei >] + (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ + pr_id (id_of_existential ev) ++ str " : " ++ pegl)) ++ + fnl () ++ pei let pr_subgoals_existential sigma = function | [] -> let exl = Evd.non_instantiated sigma in if exl = [] then - [< 'sTR"Subtree proved!" ; 'fNL >] + (str"Subtree proved!" ++ fnl ()) else let pei = pr_evars_int 1 exl in - [< 'sTR "No more subgoals but non-instantiated existential "; - 'sTR "variables :" ;'fNL; (hOV 0 pei) >] + (str "No more subgoals but non-instantiated existential " ++ + str "variables :" ++fnl () ++ (hov 0 pei)) | [g] -> let pg = pr_goal g in - v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >] + v 0 (str ("1 "^"subgoal") ++cut () ++ pg) | g1::rest -> let rec pr_rec n = function - | [] -> [< >] + | [] -> (mt ()) | g::rest -> let pc = pr_concl n g in let prest = pr_rec (n+1) rest in - [< 'cUT; pc; prest >] + (cut () ++ pc ++ prest) in let pg1 = pr_goal g1 in let prest = pr_rec 2 rest in - v 0 [< 'iNT(List.length rest+1) ; 'sTR" subgoals" ;'cUT; pg1; prest; - 'fNL >] + v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () + ++ pg1 ++ prest ++ fnl ()) open Ast open Termast @@ -308,7 +308,7 @@ let ast_of_cvt_redexp = function let ast_of_cvt_arg = function | Identifier id -> nvar id | Qualid qid -> ast_of_qualid qid - | Quoted_string s -> str s + | Quoted_string s -> string s | Integer n -> num n | Command c -> ope ("COMMAND",[c]) | Constr c -> @@ -316,8 +316,8 @@ let ast_of_cvt_arg = function | OpenConstr (_,c) -> ope ("COMMAND",[ast_of_constr false (Global.env ()) c]) | Constr_context _ -> - anomalylabstrm "ast_of_cvt_arg" [<'sTR - "Constr_context argument could not be used">] + anomalylabstrm "ast_of_cvt_arg" (str + "Constr_context argument could not be used") | Clause idl -> let transl = function | InHyp id -> ope ("INHYP", [nvar id]) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a645cf0f04..6806cf2b6b 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -91,7 +91,7 @@ let rec frontier p = p' else errorlabstrm "Refiner.frontier" - [< 'sTR"frontier was handed back a ill-formed proof." >])) + (str"frontier was handed back a ill-formed proof."))) | Some(r,pfl) -> let gll,vl = List.split(List.map frontier pfl) in (List.flatten gll, @@ -131,7 +131,7 @@ let tac_tab = Hashtbl.create 17 let add_tactic s t = if Hashtbl.mem tac_tab s then errorlabstrm ("Refiner.add_tactic: "^s) - [<'sTR "Cannot redeclare a tactic.">]; + (str "Cannot redeclare a tactic."); Hashtbl.add tac_tab s t let overwriting_add_tactic s t = @@ -146,13 +146,13 @@ let lookup_tactic s = Hashtbl.find tac_tab s with Not_found -> errorlabstrm "Refiner.lookup_tactic" - [< 'sTR"The tactic " ; 'sTR s ; 'sTR" is not installed" >] + (str"The tactic " ++ str s ++ str" is not installed") (* refiner r is a tactic applying the rule r *) let bad_subproof () = - anomalylabstrm "Refiner.refiner" [< 'sTR"Bad subproof in validation.">] + anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.") let check_subproof_connection gl spfl = if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) @@ -290,7 +290,7 @@ let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} let tclIDTAC gls = (goal_goal_list gls, idtac_valid) (* General failure tactic *) -let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" [< 'sTR s>] +let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) exception FailError of int @@ -308,7 +308,7 @@ let thens_tac tac2l taci (sigr,gs,p) = let (gl,gi) = try list_chop (List.length tac2l) gs with Failure _ -> errorlabstrm "Refiner.combine_tactics" - [<'sTR "Wrong number of tactics.">] in + (str "Wrong number of tactics.") in let tac2gl = List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 1 gi in let gll,pl = @@ -321,14 +321,14 @@ let then_tac tac = thens_tac [] (fun _ -> tac) let non_existent_goal n = errorlabstrm ("No such goal: "^(string_of_int n)) - [< 'sTR"Trying to apply a tactic to a non existent goal" >] + (str"Trying to apply a tactic to a non existent goal") (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from the last goal (i=-1). *) let theni_tac i tac ((_,gl,_) as subgoals) = let nsg = List.length gl in let k = if i < 0 then nsg + i + 1 else i in - if nsg < 1 then errorlabstrm "theni_tac" [< 'sTR"No more subgoals.">] + if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.") else if k >= 1 & k <= nsg then thens_tac [] (fun i -> if i = k then tac else tclIDTAC) subgoals else non_existent_goal k @@ -398,14 +398,14 @@ the goal unchanged *) let tclPROGRESS tac ptree = let rslt = tac ptree in if progress (fst rslt) ptree then rslt - else errorlabstrm "Refiner.PROGRESS" [< 'sTR"Failed to progress.">] + else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.") (* weak_PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged, possibly modifying sigma *) let tclWEAK_PROGRESS tac ptree = let rslt = tac ptree in if weak_progress (fst rslt) ptree then rslt - else errorlabstrm "Refiner.tclWEAK_PROGRESS" [< 'sTR"Failed to progress.">] + else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.") (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, @@ -415,7 +415,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let gls = (fst rslt).it in if List.exists (same_goal goal.it) gls then errorlabstrm "Refiner.tclNOTSAMEGOAL" - [< 'sTR"Tactic generated a subgoal identical to the original goal.">] + (str"Tactic generated a subgoal identical to the original goal.") else rslt @@ -461,7 +461,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) let tclDO n t = let rec dorec k = if k < 0 then errorlabstrm "Refiner.tclDO" - [<'sTR"Wrong argument : Do needs a positive integer.">]; + (str"Wrong argument : Do needs a positive integer."); if k = 0 then tclIDTAC else if k = 1 then t else (tclTHEN t (dorec (k-1))) in @@ -660,12 +660,12 @@ let extract_open_pftreestate pts = let extract_pftreestate pts = if pts.tstack <> [] then errorlabstrm "extract_pftreestate" - [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ; - 'sPC; 'sTR"Please ascend to the root" >]; + (str"Cannot extract from a proof-tree in which we have descended;" ++ + spc () ++ str"Please ascend to the root"); let pfterm,subgoals = extract_open_pftreestate pts in if subgoals <> [] then errorlabstrm "extract_proof" - [< 'sTR "Attempt to save an incomplete proof" >]; + (str "Attempt to save an incomplete proof"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in strong whd_betaiotaevar env pts.tpfsigma pfterm (*** @@ -676,7 +676,7 @@ let extract_pftreestate pts = let rec first_unproven pts = let pf = (proof_of_pftreestate pts) in if is_complete_proof pf then - errorlabstrm "first_unproven" [< 'sTR"No unproven subgoals" >]; + errorlabstrm "first_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then pts else @@ -693,7 +693,7 @@ let rec first_unproven pts = let rec last_unproven pts = let pf = proof_of_pftreestate pts in if is_complete_proof pf then - errorlabstrm "last_unproven" [< 'sTR"No unproven subgoals" >]; + errorlabstrm "last_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then pts else @@ -710,17 +710,17 @@ let rec last_unproven pts = let rec nth_unproven n pts = let pf = proof_of_pftreestate pts in if is_complete_proof pf then - errorlabstrm "nth_unproven" [< 'sTR"No unproven subgoals" >]; + errorlabstrm "nth_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then if n = 1 then pts else - errorlabstrm "nth_unproven" [< 'sTR"Not enough unproven subgoals" >] + errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") else let children = children_of_proof pf in let rec process i k = function | [] -> - errorlabstrm "nth_unproven" [< 'sTR"Not enough unproven subgoals" >] + errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") | pf1::rest -> let k1 = nb_unsolved_goals pf1 in if k1 < k then @@ -789,17 +789,17 @@ let pr_tactic (s,l) = let pr_rule = function | Prim r -> pr_prim_rule r - | Tactic texp -> hOV 0 (pr_tactic texp) + | Tactic texp -> hov 0 (pr_tactic texp) | Change_evars -> (* This is internal tactic and cannot be replayed at user-level. Function pr_rule_dot below is used when we want to hide Change_evars *) - [< 'sTR"Evar change" >] + str "Evar change" (* Does not print change of evars *) let pr_rule_dot = function - | Change_evars -> [<>] - | r -> [< pr_rule r; 'sTR"." ; 'fNL >] + | Change_evars -> (mt ()) + | r -> (pr_rule r ++ str"." ++ fnl ()) exception Different @@ -819,69 +819,68 @@ let rec print_proof sigma osign pf = let hyps' = thin_sign osign hyps in match pf.ref with | None -> - hOV 0 [< pr_seq {evar_hyps=hyps'; evar_concl=cl; - evar_body=body} >] + hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) | Some(r,spfl) -> - hOV 0 [< hOV 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; - evar_body=body}); - 'sPC ; 'sTR" BY "; - hOV 0 [< pr_rule r >]; 'fNL ; - 'sTR" "; - hOV 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) - >] + hov 0 + (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ + spc () ++ str" BY " ++ + hov 0 (pr_rule r) ++ fnl () ++ + str" " ++ + hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) +) -let pr_change gl = [< 'sTR"Change " ; prterm gl.evar_concl ; 'sTR"." ; 'fNL>] +let pr_change gl = (str"Change " ++ prterm gl.evar_concl ++ str"." ++ fnl ()) let rec print_script nochange sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in match pf.ref with | None -> if nochange then - [< 'sTR"" >] + (str"") else pr_change pf.goal | Some(r,spfl) -> - [< (if nochange then [< >] else (pr_change pf.goal)); - pr_rule_dot r; + ((if nochange then (mt ()) else (pr_change pf.goal)) ++ + pr_rule_dot r ++ prlist_with_sep pr_fnl - (print_script nochange sigma sign) spfl >] + (print_script nochange sigma sign) spfl) let rec print_treescript sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in match pf.ref with - | None -> [< >] + | None -> (mt ()) | Some(r,spfl) -> - [< pr_rule_dot r ; + (pr_rule_dot r ++ let prsub = prlist_with_sep pr_fnl (print_treescript sigma sign) spfl in if List.length spfl > 1 then - [< 'sTR" "; hOV 0 prsub >] + (str" " ++ hov 0 prsub) else prsub - >] +) let rec print_info_script sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in match pf.ref with - | None -> [< >] + | None -> (mt ()) | Some(Change_evars,[spf]) -> print_info_script sigma osign spf | Some(r,spfl) -> - [< pr_rule r ; + (pr_rule r ++ match spfl with | [pf1] -> if pf1.ref = None then - [<'sTR "."; 'fNL >] + (str "." ++ fnl ()) else - [< 'sTR";" ; 'bRK(1,3) ; - print_info_script sigma sign pf1 >] - | _ -> [< 'sTR"." ; 'fNL ; + (str";" ++ brk(1,3) ++ + print_info_script sigma sign pf1) + | _ -> (str"." ++ fnl () ++ prlist_with_sep pr_fnl - (print_info_script sigma sign) spfl >] >] + (print_info_script sigma sign) spfl)) let format_print_info_script sigma osign pf = - hOV 0 (print_info_script sigma osign pf) + hov 0 (print_info_script sigma osign pf) let print_subscript sigma sign pf = if is_tactic_proof pf then @@ -894,10 +893,9 @@ let tclINFO (tac : tactic) gls = begin try let pf = v (List.map leaf (sig_it sgl)) in let sign = (sig_it gls).evar_hyps in - mSGNL(hOV 0 [< 'sTR" == "; - print_subscript - (sig_sig gls) sign pf >]) + msgnl (hov 0 (str" == " ++ + print_subscript (sig_sig gls) sign pf)) with e when catchable_exception e -> - mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >]) + msgnl (hov 0 (str "Info failed to apply validation")) end; res diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 56fe36890a..08535e6415 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -37,7 +37,7 @@ open Safe_typing let err_msg_tactic_not_found macro_loc macro = user_err_loc (macro_loc,"macro_expand", - [<'sTR "Tactic macro "; 'sTR macro; 'sPC; 'sTR "not found">]) + (str "Tactic macro " ++ str macro ++ spc () ++ str "not found")) (* Values for interpretation *) type value = @@ -74,24 +74,24 @@ let tactic_of_value vle g = let id_of_Identifier = function | Identifier id -> id | _ -> - anomalylabstrm "id_of_Identifier" [<'sTR "Not an IDENTIFIER tactic_arg">] + anomalylabstrm "id_of_Identifier" (str "Not an IDENTIFIER tactic_arg") (* Gives the constr corresponding to a Constr tactic_arg *) let constr_of_Constr = function | Constr c -> c - | _ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a Constr tactic_arg">] + | _ -> anomalylabstrm "constr_of_Constr" (str "Not a Constr tactic_arg") (* Gives the constr corresponding to a Constr_context tactic_arg *) let constr_of_Constr_context = function | Constr_context c -> c | _ -> - anomalylabstrm "constr_of_Constr_context" [<'sTR - "Not a Constr_context tactic_arg">] + anomalylabstrm "constr_of_Constr_context" (str + "Not a Constr_context tactic_arg") (* Gives the qualid corresponding to a Qualid tactic_arg *) let qualid_of_Qualid = function | Qualid id -> id - | _ -> anomalylabstrm "qualid_of_Qualid" [<'sTR "Not a Qualid tactic_arg">] + | _ -> anomalylabstrm "qualid_of_Qualid" (str "Not a Qualid tactic_arg") (* Gives identifiers and makes the possible injection constr -> ident *) let make_ids ast = function @@ -100,9 +100,9 @@ let make_ids ast = function (try destVar c with | Invalid_argument "destVar" -> anomalylabstrm "make_ids" - [<'sTR "This term cannot be reduced to an identifier"; 'fNL; - print_ast ast>]) - | _ -> anomalylabstrm "make_ids" [< 'sTR "Not an identifier" >] + (str "This term cannot be reduced to an identifier" ++ fnl () ++ + print_ast ast)) + | _ -> anomalylabstrm "make_ids" (str "Not an identifier") (* Gives Qualid's and makes the possible injection identifier -> qualid *) let make_qid = function @@ -111,8 +111,8 @@ let make_qid = function | VArg (Constr c) -> (match (kind_of_term c) with | Const cst -> VArg (Qualid (qualid_of_sp cst)) - | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >]) - | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >] + | _ -> anomalylabstrm "make_qid" (str "Not a Qualid")) + | _ -> anomalylabstrm "make_qid" (str "Not a Qualid") (* Transforms a named_context into a (string * constr) list *) let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ)) @@ -160,10 +160,10 @@ let tacticOut = function if (tag d) = "tactic" then tactic_out d else - anomalylabstrm "tacticOut" [<'sTR "Dynamic tag should be tactic">] + anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") | ast -> anomalylabstrm "tacticOut" - [<'sTR "Not a Dynamic ast: "; print_ast ast>] + (str "Not a Dynamic ast: " ++ print_ast ast) let valueIn t = Dynamic (dummy_loc,value_in t) let valueOut = function @@ -171,10 +171,10 @@ let valueOut = function if (tag d) = "value" then value_out d else - anomalylabstrm "valueOut" [<'sTR "Dynamic tag should be value">] + anomalylabstrm "valueOut" (str "Dynamic tag should be value") | ast -> anomalylabstrm "valueOut" - [<'sTR "Not a Dynamic ast: "; print_ast ast>] + (str "Not a Dynamic ast: " ++ print_ast ast) let constrIn = constrIn let constrOut = constrOut @@ -192,8 +192,8 @@ let interp_add (ast_typ,interp_fun) = with Failure _ -> errorlabstrm "interp_add" - [<'sTR "Cannot add the interpretation function for "; 'sTR ast_typ; - 'sTR " twice">] + (str "Cannot add the interpretation function for " ++ str ast_typ ++ + str " twice") (* Adds a possible existing interpretation function *) let overwriting_interp_add (ast_typ,interp_fun) = @@ -249,7 +249,7 @@ let _ = (* Unboxes the tactic_arg *) let unvarg = function | VArg a -> a - | _ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">] + | _ -> errorlabstrm "unvarg" (str "Not a tactic argument") (* Unboxes VRec *) let unrec = function @@ -259,7 +259,7 @@ let unrec = function (* Unboxes REDEXP *) let unredexp = function | Redexp c -> c - | _ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">] + | _ -> errorlabstrm "unredexp" (str "Not a REDEXP tactic_arg") (* Reads the head of Fun *) let read_fun ast = @@ -268,12 +268,12 @@ let read_fun ast = | Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl) | [] -> [] | _ -> - anomalylabstrm "Tacinterp.read_fun_rec" [<'sTR "Fun not well formed">] + anomalylabstrm "Tacinterp.read_fun_rec" (str "Fun not well formed") in match ast with | Node(_,"FUNVAR",l) -> read_fun_rec l | _ -> - anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">] + anomalylabstrm "Tacinterp.read_fun" (str "Fun not well formed") (* Reads the clauses of a Rec *) let rec read_rec_clauses = function @@ -282,7 +282,7 @@ let rec read_rec_clauses = function (name,it,body)::(read_rec_clauses tl) |_ -> anomalylabstrm "Tacinterp.read_rec_clauses" - [<'sTR "Rec not well formed">] + (str "Rec not well formed") (* Associates variables with values and gives the remaining variables and values *) @@ -322,8 +322,8 @@ let give_context ctxt = function let ast_of_command = function | Node(_,"COMMAND",[c]) -> c | ast -> - anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR - "Not a COMMAND ast node: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",(str + "Not a COMMAND ast node: " ++ print_ast ast)) (* Reads a pattern *) let read_pattern evc env lfun = function @@ -336,8 +336,8 @@ let read_pattern evc env lfun = function | Node(_,"TERM",[pc]) -> Term (snd (interp_constrpattern_gen evc env lfun (ast_of_command pc))) | ast -> - anomaly_loc (Ast.loc ast, "Tacinterp.read_pattern",[<'sTR - "Not a pattern ast node: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.read_pattern",(str + "Not a pattern ast node: " ++ print_ast ast)) (* Reads the hypotheses of a Match Context rule *) let rec read_match_context_hyps evc env lfun = function @@ -348,8 +348,8 @@ let rec read_match_context_hyps evc env lfun = function (Hyp (s,read_pattern evc env lfun mp))::(read_match_context_hyps evc env lfun tl) | ast::tl -> - anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR - "Not a MATCHCONTEXTHYP ast node: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",(str + "Not a MATCHCONTEXTHYP ast node: " ++ print_ast ast)) | [] -> [] (* Reads the rules of a Match Context *) @@ -362,8 +362,8 @@ let rec read_match_context_rule evc env lfun = function rl))),read_pattern evc env lfun (List.nth rl 1),List.hd rl))::(read_match_context_rule evc env lfun tl) | ast::tl -> - anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR - "Not a MATCHCONTEXTRULE ast node: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",(str + "Not a MATCHCONTEXTRULE ast node: " ++ print_ast ast)) | [] -> [] (* Reads the rules of a Match *) @@ -374,8 +374,8 @@ let rec read_match_rule evc env lfun = function (Pat ([],read_pattern evc env lfun mp,te))::(read_match_rule evc env lfun tl) | ast::tl -> - anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR - "Not a MATCHRULE ast node: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",(str + "Not a MATCHRULE ast node: " ++ print_ast ast)) | [] -> [] (* For Match Context and Match *) @@ -472,8 +472,8 @@ let get_debug () = !debug (* Interprets any expression *) let rec val_interp ist ast = -(* mSGNL []; *) -(* mSGNL [] *) +(* mSGNL (print_ast ast); *) +(* mSGNL (print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)) *) let value_interp ist = match ast with @@ -574,10 +574,10 @@ let rec val_interp ist ast = VArg (Constr (Pretyping.constr_out t)) else anomaly_loc (Ast.loc ast, "Tacinterp.val_interp", - [<'sTR "Unknown dynamic ast: "; print_ast ast>]) + (str "Unknown dynamic ast: " ++ print_ast ast)) | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.val_interp", - [<'sTR "Unrecognizable ast: "; print_ast ast>]) in + (str "Unrecognizable ast: " ++ print_ast ast)) in if ist.debug = DebugOn then match debug_prompt ist.goalopt ast with | Exit -> VTactic tclIDTAC @@ -601,7 +601,7 @@ and app_interp ist fv largs ast = VFun(olfun@newlfun,lvar,body) | _ -> user_err_loc (Ast.loc ast, "Tacinterp.app_interp", - [<'sTR"Illegal tactic application: "; print_ast ast>]) + (str"Illegal tactic application: " ++ print_ast ast)) (* Interprets recursive expressions *) and rec_interp ist ast = function @@ -626,7 +626,7 @@ and rec_interp ist ast = function end | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp", - [<'sTR"Rec not well formed: "; print_ast ast>]) + (str"Rec not well formed: " ++ print_ast ast)) (* Interprets the clauses of a Let *) and let_interp ist ast = function @@ -635,7 +635,7 @@ and let_interp ist ast = function (id,val_interp ist t)::(let_interp ist ast tl) | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.let_interp", - [<'sTR"Let not well formed: "; print_ast ast>]) + (str"Let not well formed: " ++ print_ast ast)) (* Interprets the clauses of a LetCutIn *) and letin_interp ist ast = function @@ -654,7 +654,7 @@ and letin_interp ist ast = function (letin_interp ist ast tl) with | Not_found -> errorlabstrm "Tacinterp.letin_interp" - [< 'sTR "Term or tactic expected" >]) + (str "Term or tactic expected")) | _ -> (try let t = tactic_of_value tac in @@ -671,10 +671,10 @@ and letin_interp ist ast = function with | NotTactic -> delete_proof id; errorlabstrm "Tacinterp.letin_interp" - [< 'sTR "Term or tactic expected" >])) + (str "Term or tactic expected"))) | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.letin_interp", - [<'sTR "LetIn not well formed: "; print_ast ast>]) + (str "LetIn not well formed: " ++ print_ast ast)) (* Interprets the clauses of a LetCut *) and letcut_interp ist ast = function @@ -685,8 +685,8 @@ and letcut_interp ist ast = function and (ndc,ccl) = match ist.goalopt with | None -> - errorlabstrm "Tacinterp.letcut_interp" [< 'sTR - "Do not use Let for toplevel definitions, use Lemma, ... instead" >] + errorlabstrm "Tacinterp.letcut_interp" (str + "Do not use Let for toplevel definitions, use Lemma, ... instead") | Some g -> (pf_hyps g,pf_concl g) in (match tac with | VArg (Constr csr) -> @@ -709,7 +709,7 @@ and letcut_interp ist ast = function (letcut_interp ist ast tl);exat] with | Not_found -> errorlabstrm "Tacinterp.letin_interp" - [< 'sTR "Term or tactic expected" >]) + (str "Term or tactic expected")) | _ -> (try let t = tactic_of_value tac in @@ -730,18 +730,18 @@ and letcut_interp ist ast = function with | NotTactic -> delete_proof id; errorlabstrm "Tacinterp.letcut_interp" - [< 'sTR "Term or tactic expected" >])) + (str "Term or tactic expected"))) | _ -> - anomaly_loc (Ast.loc ast, "Tacinterp.letcut_interp",[<'sTR - "LetCut not well formed: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.letcut_interp",(str + "LetCut not well formed: " ++ print_ast ast)) (* Interprets the Match Context expressions *) and match_context_interp ist ast lmr = (* let goal = (match goalopt with | None -> - errorlabstrm "Tacinterp.apply_match_context" [< 'sTR - "No goal available" >] + errorlabstrm "Tacinterp.apply_match_context" (str + "No goal available") | Some g -> g) in*) let rec apply_goal_sub ist goal nocc (id,c) csr mt mhyps hyps = @@ -793,8 +793,8 @@ and match_context_interp ist ast lmr = with | No_match | _ -> apply_match_context ist goal tl)) | _ -> - errorlabstrm "Tacinterp.apply_match_context" [<'sTR - "No matching clauses for Match Context">] in + errorlabstrm "Tacinterp.apply_match_context" (str + "No matching clauses for Match Context") in let app_wo_goal = (fun ist goal -> apply_match_context ist goal @@ -855,8 +855,8 @@ and apply_hyps_context ist mt lgmatch mhyps hyps = (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1)))) end | [] -> - anomalylabstrm "apply_hyps_context_rec" [<'sTR - "Empty list should not occur" >] in + anomalylabstrm "apply_hyps_context_rec" (str + "Empty list should not occur") in apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None (* Interprets a VContext value *) @@ -925,8 +925,8 @@ and match_interp ist ast lmr = with | No_match -> apply_match ist csr tl)) | _ -> - errorlabstrm "Tacinterp.apply_match" [<'sTR - "No matching clauses for Match">] in + errorlabstrm "Tacinterp.apply_match" (str + "No matching clauses for Match") in let csr = constr_of_Constr (unvarg (val_interp ist (List.hd lmr))) and ilr = read_match_rule ist.evc ist.env (constr_list ist.goalopt ist.lfun) (List.tl lmr) in @@ -943,19 +943,19 @@ and tac_interp lfun lmatch debug ast g = goalopt=Some g; debug=debug } in try tactic_of_value (val_interp ist ast) g with | NotTactic -> - errorlabstrm "Tacinterp.tac_interp" [<'sTR - "Must be a command or must give a tactic value">] + errorlabstrm "Tacinterp.tac_interp" (str + "Must be a command or must give a tactic value") -(* errorlabstrm "Tacinterp.tac_interp" [<'sTR - "Interpretation gives a non-tactic value">] *) +(* errorlabstrm "Tacinterp.tac_interp" (str + "Interpretation gives a non-tactic value") *) (* match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with | VTactic tac -> (tac g) | VFTactic (largs,f) -> (f largs g) | VRTactic res -> res | _ -> - errorlabstrm "Tacinterp.tac_interp" [<'sTR - "Interpretation gives a non-tactic value">]*) + errorlabstrm "Tacinterp.tac_interp" (str + "Interpretation gives a non-tactic value")*) (* Interprets a primitive tactic *) and interp_atomic opn args = vernac_tactic(opn,args) @@ -985,8 +985,8 @@ and bind_interp ist = function (val_interp ist (Node(loc,"COMMAND",[c]))))) | x -> - errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; - print_ast x>] + errorlabstrm "bind_interp" (str "Not the expected form in binding" ++ + print_ast x) (* Interprets a COMMAND expression (in case of failure, returns Command) *) and com_interp ist com = @@ -1002,8 +1002,8 @@ and com_interp ist com = subst_meta [-1,ic] ctxt with | Not_found -> - errorlabstrm "com_interp" [<'sTR "Unbound context identifier"; - print_ast ast>]) + errorlabstrm "com_interp" (str "Unbound context identifier" ++ + print_ast ast)) | c -> interp_constr ist c None in begin db_constr ist.debug ist.env csr; @@ -1027,14 +1027,14 @@ and cast_com_interp ist com = and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in begin - wARNING [<'sTR - "Cannot pre-constrain the context expression with goal">]; + warning + "Cannot pre-constrain the context expression with goal"; subst_meta [-1,ic] ctxt end with | Not_found -> - errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier"; - print_ast ast>]) + errorlabstrm "cast_com_interp" (str "Unbound context identifier" ++ + print_ast ast)) | c -> interp_constr ist c (Some (pf_concl gl)) in begin @@ -1042,7 +1042,7 @@ and cast_com_interp ist com = VArg (Constr csr) end | None -> - errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] + errorlabstrm "val_interp" (str "Cannot cast a constr without goal") (* Interprets a CASTEDOPENCOMMAND expression *) and cast_opencom_interp ist com = @@ -1060,19 +1060,19 @@ and cast_opencom_interp ist com = and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in begin - wARNING [<'sTR - "Cannot pre-constrain the context expression with goal">]; + warning + "Cannot pre-constrain the context expression with goal"; VArg (Constr (subst_meta [-1,ic] ctxt)) end with | Not_found -> - errorlabstrm "cast_opencom_interp" [<'sTR "Unbound context identifier"; - print_ast ast>]) + errorlabstrm "cast_opencom_interp" (str "Unbound context identifier" ++ + print_ast ast)) | c -> VArg (OpenConstr (interp_openconstr ist c (Some (pf_concl gl))))) | None -> - errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] + errorlabstrm "val_interp" (str "Cannot cast a constr without goal") (* Interprets a qualified name. This can be a metavariable to be injected *) and qid_interp ist = function @@ -1080,8 +1080,8 @@ and qid_interp ist = function | Node(loc,"QUALIDMETA",[Num(_,n)]) -> Nametab.qualid_of_sp (destConst(List.assoc n ist.lmatch)) | ast -> - anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR - "Unrecognizable qualid ast: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",(str + "Unrecognizable qualid ast: " ++ print_ast ast)) and cvt_pattern ist = function | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> @@ -1136,7 +1136,7 @@ and flag_of_ast ist lf = | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf | Node(loc,("Unf"|"UnfBut"),l)::_ -> user_err_loc(loc,"flag_of_ast", - [<'sTR "Delta must be specified just before">]) + (str "Delta must be specified just before")) | arg::_ -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") in @@ -1167,8 +1167,8 @@ and cvt_intro_pattern ist = function ListPat (List.map (cvt_intro_pattern ist) l) | x -> errorlabstrm "cvt_intro_pattern" - [<'sTR "Not the expected form for an introduction pattern!";'fNL; - print_ast x>] + (str "Not the expected form for an introduction pattern!" ++fnl () ++ + print_ast x) (* Interprets a pattern of Let *) and cvt_letpattern ist (o,l) = function @@ -1199,13 +1199,13 @@ let interp = fun ast -> tac_interp [] [] !debug ast let hide_interp = let htac = hide_tactic "Interp" (function [Tacexp t] -> interp t - | _ -> anomalylabstrm "hide_interp" [<'sTR "Not a tactic AST">]) in + | _ -> anomalylabstrm "hide_interp" (str "Not a tactic AST")) in fun ast -> htac [Tacexp ast] (* For bad tactic calls *) let bad_tactic_args s = anomalylabstrm s - [<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">] + (str "Tactic " ++ str s ++ str " called with bad arguments") (* Declaration of the TAC-DEFINITION object *) let (inMD,outMD) = @@ -1227,9 +1227,9 @@ let add_tacdef na vbody = begin if Gmap.mem na !mactab then errorlabstrm "Tacinterp.add_tacdef" - [< 'sTR - "There is already a Meta Definition or a Tactic Definition named "; - pr_id na>]; + (str "There is already a Meta Definition or a Tactic Definition named " + ++ + pr_id na); let _ = Lib.add_leaf na (inMD (na,vbody)) in - Options.if_verbose mSGNL [< pr_id na; 'sTR " is defined" >] + Options.if_verbose msgnl (pr_id na ++ str " is defined") end diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 377893fd27..adb4df3d53 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -482,25 +482,25 @@ let pr_com sigma goal com = (Astterm.interp_constr sigma (Evarutil.evar_env goal) com)) let pr_one_binding sigma goal = function - | (Dep id,com) -> [< pr_id id ; 'sTR":=" ; pr_com sigma goal com >] - | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >] - | (Com,com) -> [< pr_com sigma goal com >] + | (Dep id,com) -> pr_id id ++ str ":=" ++ pr_com sigma goal com + | (NoDep n,com) -> int n ++ str ":=" ++ pr_com sigma goal com + | (Com,com) -> pr_com sigma goal com let pr_bindings sigma goal lb = let prf = pr_one_binding sigma goal in match lb with - | [] -> [< prlist_with_sep pr_spc prf lb >] - | _ -> [<'sTR"with";'sPC;prlist_with_sep pr_spc prf lb >] + | [] -> prlist_with_sep pr_spc prf lb + | _ -> str "with" ++ spc () ++ prlist_with_sep pr_spc prf lb let rec pr_list f = function - | [] -> [<>] - | a::l1 -> [< (f a) ; pr_list f l1>] + | [] -> mt () + | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hOV 0 [< pr_decls (sig_sig gls) ; 'fNL ; pr_seq (sig_it gls) >] + hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls)) let pr_glls glls = - hOV 0 [< pr_decls (sig_sig glls) ; 'fNL ; - prlist_with_sep pr_fnl pr_seq (sig_it glls) >] - + hov 0 (pr_decls (sig_sig glls) ++ fnl () ++ + prlist_with_sep pr_fnl pr_seq (sig_it glls)) + let pr_tactic = Refiner.pr_tactic diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 08446d0112..61ccbcac7c 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -21,26 +21,27 @@ type debug_info = (* Prints the goal if it exists *) let db_pr_goal = function - | None -> mSGNL [< 'sTR "No goal" >] + | None -> + msgnl (str "No goal") | Some g -> - mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >] + msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g)) (* Prints the commands *) let help () = - mSGNL [< 'sTR "Commands: =Continue, h=Help, s=Skip, x=Exit" >] + msgnl (str "Commands: =Continue, h=Help, s=Skip, x=Exit") (* Prints the state and waits for an instruction *) let debug_prompt goalopt tac_ast = db_pr_goal goalopt; - mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL >]; -(* 'sTR "Commands: =Continue, s=Skip, x=Exit" >];*) -(* mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL; - 'sTR "----=Continue----s=Skip----x=Exit----" >];*) + msg (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl ()); +(* str "Commands: =Continue, s=Skip, x=Exit" >];*) +(* mSG (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl () ++ fnl () ++ + str "----=Continue----s=Skip----x=Exit----");*) let rec prompt () = - mSG [<'fNL; 'sTR "TcDebug > " >]; + msg (fnl () ++ str "TcDebug > "); flush stdout; let inst = read_line () in -(* mSGNL [<>];*) +(* mSGNL (mt ());*) match inst with | "" -> DebugOn | "s" -> DebugOff @@ -56,15 +57,15 @@ let debug_prompt goalopt tac_ast = (* Prints a constr *) let db_constr debug env c = if debug = DebugOn then - mSGNL [< 'sTR "Evaluated term --> "; prterm_env env c >] + msgnl (str "Evaluated term --> " ++ prterm_env env c) (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,c) = if debug = DebugOn then - mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": "); - prterm_env env c >] + msgnl (str "Matched hypothesis --> " ++ str (id^": ") ++ + prterm_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = if debug = DebugOn then - mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >] + msgnl (str "Matched goal --> " ++ prterm_env env c) -- cgit v1.2.3