From 3154c8ae825e874470846d62f942087d79909700 Mon Sep 17 00:00:00 2001 From: bertot Date: Tue, 18 Dec 2001 14:02:29 +0000 Subject: Integrating the Ltac language and the Blast tool into the interface capabilities: The Ltac language is the language that makes it possible to define new tactics without using the ocaml language (already present in coq for a few months). The Blast tool is a tool that checks whether the goals could be solve automatically and proposes the proof trace to the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2313 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/parse.ml | 202 +++++++++++++++++++++++++-------------------- 1 file changed, 114 insertions(+), 88 deletions(-) (limited to 'contrib/interface/parse.ml') diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index fad5c1e34..671338002 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -43,24 +43,29 @@ let print_parse_results n msg = flush stdout;; let ctf_SyntaxErrorMessage reqid pps = - (fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ int reqid ++ fnl () ++ - pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ + int reqid ++ fnl () ++ + pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; let ctf_SyntaxWarningMessage reqid pps = - (fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ int reqid ++ fnl () ++ - pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ + int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; let ctf_FileErrorMessage reqid pps = - (fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ int reqid ++ fnl () ++ - pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ + int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ + fnl ();; (*In the code for CoqV6.2, the require_module call is encapsulated in a function "without_mes_ambig". Here I have supposed that this function has no effect on parsing *) let try_require_module import specif name fname = - try Library.require_module (if specif = "UNSPECIFIED" then None - else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT") + try Library.require_module + (if specif = "UNSPECIFIED" then None + else Some (specif = "SPECIFICATION")) + (Nametab.make_short_qualid (Names.id_of_string name)) + fname (import = "IMPORT") with - | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");; + | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");; let execute_when_necessary ast = (match ast with @@ -82,20 +87,24 @@ let parse_to_dot = let rec dot st = match Stream.next st with | ("", ".") -> () | ("EOI", "") -> raise End_of_file - | _ -> dot st - in - Gram.Entry.of_parser "Coqtoplevel.dot" dot;; + | _ -> dot st in + Gram.Entry.of_parser "Coqtoplevel.dot" dot;; let rec discard_to_dot stream = try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with | Stdpp.Exc_located(_, Token.Error _) -> discard_to_dot stream;; -let rec decompose_string s n = +let rec decompose_string_aux s n = try let index = String.index_from s n '\n' in (Ctast.str (String.sub s n (index - n))):: - (decompose_string s (index + 1)) + (decompose_string_aux s (index + 1)) with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];; +let decompose_string s n = + match decompose_string_aux s n with + (Ctast.Str(_,""))::tl -> tl + | a -> a;; + let make_string_list file_chan fst_pos snd_pos = let len = (snd_pos - fst_pos) in let s = String.create len in @@ -146,15 +155,17 @@ let parse_command_list reqid stream string_list = let rec parse_whole_stream () = let this_pos = Stream.count stream in let first_ast = - try option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) + try option_app + Ctast.ast_to_ct (Gram.Entry.parse + Pcoq.main_entry (Gram.parsable stream)) with | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> begin msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e)); try discard_to_dot stream; - msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ int - (Stream.count stream)); + msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ + int (Stream.count stream)); Some( Node(l, "PARSING_ERROR", List.map Ctast.str (get_substring_list string_list this_pos @@ -172,7 +183,13 @@ let parse_command_list reqid stream string_list = match first_ast with | Some ast -> let ast0 = (execute_when_necessary ast) in - xlate_vernac ast::parse_whole_stream() + (try xlate_vernac ast + with e -> + xlate_vernac + (Node((0,0), "PARSING_ERROR2", + List.map Ctast.str + (get_substring_list string_list this_pos + (Stream.count stream)))))::parse_whole_stream() | None -> [] in match parse_whole_stream () with | first_one::tail -> (P_cl (CT_command_list(first_one, tail))) @@ -239,56 +256,75 @@ let parse_file_action reqid file_name = let file_chan_err = open_in file_name in let stream = Stream.of_channel file_chan in let stream_err = Stream.of_channel file_chan_err in - match let rec parse_whole_file () = - let this_pos = Stream.count stream in - match - try - let this_ast = - option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in - this_ast - with - | Stdpp.Exc_located(l,Stream.Error txt ) -> - msgnl (ctf_SyntaxWarningMessage reqid - (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn - (Stdpp.Exc_located(l,Stream.Error txt)))); - let rec discard_to_dot () = - try Gram.Entry.parse parse_to_dot (Gram.parsable stream) - with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() - in (try - discard_to_dot (); - Some( Node(l, "PARSING_ERROR", - (make_string_list file_chan_err this_pos - (Stream.count stream)))) - with End_of_file -> None) - | e -> - begin - Gram.Entry.parse parse_to_dot (Gram.parsable stream); - Some( Node((0,0), "PARSING_ERROR2", - (make_string_list file_chan this_pos - (Stream.count stream)))) - end - - with - | Some ast -> let ast0=(execute_when_necessary ast) in - xlate_vernac ast::parse_whole_file () - | None -> [] in - parse_whole_file () with - | first_one :: tail -> - print_parse_results reqid - (P_cl (CT_command_list (first_one, tail))) - | [] -> raise (UserError ("parse_file_action", (str "empty file."))) - with - | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> - msgnl - (ctf_SyntaxErrorMessage reqid - (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")))) - | e -> - msgnl - (ctf_SyntaxErrorMessage reqid - (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn e));; + let rec discard_to_dot () = + try Gram.Entry.parse parse_to_dot (Gram.parsable stream) + with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in + match let rec parse_whole_file () = + let this_pos = Stream.count stream in + match + try + let this_ast = + option_app Ctast.ast_to_ct + (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in + this_ast + with + | Stdpp.Exc_located(l,Stream.Error txt) -> + msgnl (ctf_SyntaxWarningMessage reqid + (str "Error with file" ++ spc () ++ + str file_name ++ fnl () ++ + Errors.explain_exn + (Stdpp.Exc_located(l,Stream.Error txt)))); + (try + begin + discard_to_dot (); + Some( Node(l, "PARSING_ERROR", + (make_string_list file_chan_err this_pos + (Stream.count stream)))) + end + with End_of_file -> None) + | e -> + begin + Gram.Entry.parse parse_to_dot (Gram.parsable stream); + Some(Node((0,0), "PARSING_ERROR2", + (make_string_list file_chan this_pos + (Stream.count stream)))) + end + + with + | Some ast -> + let ast0=(execute_when_necessary ast) in + let term = + (try xlate_vernac ast + with e -> + print_string ("translation error between " ^ + (string_of_int this_pos) ^ + " " ^ + (string_of_int (Stream.count stream)) ^ + "\n"); + xlate_vernac + (Node((0,0), "PARSING_ERROR2", + (make_string_list file_chan_err this_pos + (Stream.count stream))))) in + term::parse_whole_file () + | None -> [] in + parse_whole_file () with + | first_one :: tail -> + print_parse_results reqid + (P_cl (CT_command_list (first_one, tail))) + | [] -> raise (UserError ("parse_file_action", str "empty file.")) + with + | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> + msgnl + (ctf_SyntaxErrorMessage reqid + (str "Error with file" ++ spc () ++ str file_name ++ + fnl () ++ + Errors.explain_exn + (Stdpp.Exc_located(l,Stream.Error "match failure")))) + | e -> + msgnl + (ctf_SyntaxErrorMessage reqid + (str "Error with file" ++ spc () ++ str file_name ++ + fnl () ++ Errors.explain_exn e));; (* This function is taken from Mltop.add_path *) @@ -302,7 +338,7 @@ let add_path dir coq_dirpath = let convert_string d = try Names.id_of_string d - with _ -> failwith "caught" + with _ -> failwith ("could not convert " ^ d) let add_rec_path dir coq_dirpath = let dirs = all_subdirs dir in @@ -345,11 +381,12 @@ let load_syntax_action reqid module_name = msgnl (mt ()); msgnl (fnl () ++ str "error while loading syntax module " ++ str module_name ++ - str ": " ++ str label ++ fnl () ++ pp_stream) + str ": " ++ str label ++ fnl () ++ pp_stream) | e -> msgnl (mt ()); msgnl - (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ int reqid ++ fnl ()); + (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ + int reqid ++ fnl ()); ();; let coqparser_loop inchan = @@ -373,25 +410,14 @@ Libobject.relax true; else (msgnl (str "could not find the value of COQDIR"); exit 1) in begin - add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]); - add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]); - add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]); + add_rec_path (Filename.concat coqdir "theories") + (Names.make_dirpath [Nameops.coq_root]); + add_path (Filename.concat coqdir "tactics") + (Names.make_dirpath [Nameops.coq_root]); + add_rec_path (Filename.concat coqdir "contrib") + (Names.make_dirpath [Nameops.coq_root]); List.iter (fun a -> msgnl (str a)) (get_load_path()) end; -(try - (match create_entry (get_univ "nat") "number" ETast with - (Ast number) -> - Gram.extend number None - [None, None, - [[Gramext.Stoken ("INT", "")], - Gramext.action - (fun s loc -> - Node((0,0),"XTRA",[Str((0,0),"omega_integer_for_ctcoq"); - Num((0,0),int_of_string s)]))]] - | _ -> msgnl (str "unpredicted behavior of Grammar.extend")) - - with - e -> msgnl (str "could not add a parser for numbers")); (let vernacrc = try Sys.getenv "VERNACRC" -- cgit v1.2.3