diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cUnix.ml | 108 | ||||
| -rw-r--r-- | lib/cUnix.mli | 32 | ||||
| -rw-r--r-- | lib/clib.mllib | 8 | ||||
| -rw-r--r-- | lib/envars.ml | 72 | ||||
| -rw-r--r-- | lib/envars.mli | 9 | ||||
| -rw-r--r-- | lib/interface.mli | 93 | ||||
| -rw-r--r-- | lib/lib.mllib | 5 | ||||
| -rw-r--r-- | lib/serialize.ml | 447 | ||||
| -rw-r--r-- | lib/serialize.mli | 89 | ||||
| -rw-r--r-- | lib/system.ml | 153 | ||||
| -rw-r--r-- | lib/system.mli | 36 | ||||
| -rw-r--r-- | lib/xml_parser.ml | 2 | ||||
| -rw-r--r-- | lib/xml_parser.mli | 4 | ||||
| -rw-r--r-- | lib/xml_utils.ml | 2 |
14 files changed, 855 insertions, 205 deletions
diff --git a/lib/cUnix.ml b/lib/cUnix.ml new file mode 100644 index 000000000..ad5f0587d --- /dev/null +++ b/lib/cUnix.ml @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Files and load path. *) + +type physical_path = string +type load_path = physical_path list + +let physical_path_of_string s = s +let string_of_physical_path p = p + +let path_to_list p = + let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in + Str.split sep p + +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + let l = String.length p in + if l > n && String.sub p 0 n = curdir then + let n' = + let sl = String.length Filename.dir_sep in + let i = ref n in + while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in + remove_path_dot (String.sub p n' (l - n')) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + let l = String.length p in + if l > n && String.sub p 0 n = cwd then + let n' = + let sl = String.length Filename.dir_sep in + let i = ref n in + while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in + remove_path_dot (String.sub p n' (l - n')) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + +let make_suffix name suffix = + if Filename.check_suffix name suffix then name else (name ^ suffix) + +let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f + +let file_readable_p name = + try Unix.access name [Unix.R_OK];true with Unix.Unix_error (_, _, _) -> false + +let run_command converter f c = + let result = Buffer.create 127 in + let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in + let buff = String.make 127 ' ' in + let buffe = String.make 127 ' ' in + let n = ref 0 in + let ne = ref 0 in + + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; + !n+ !ne <> 0 + do + let r = converter (String.sub buff 0 !n) in + f r; + Buffer.add_string result r; + let r = converter (String.sub buffe 0 !ne) in + f r; + Buffer.add_string result r + done; + (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) + +(* + checks if two file names refer to the same (existing) file by + comparing their device and inode. + It seems that under Windows, inode is always 0, so we cannot + accurately check if + +*) +(* Optimised for partial application (in case many candidates must be + compared to f1). *) +let same_file f1 = + try + let s1 = Unix.stat f1 in + (fun f2 -> + try + let s2 = Unix.stat f2 in + s1.Unix.st_dev = s2.Unix.st_dev && + if Sys.os_type = "Win32" then f1 = f2 + else s1.Unix.st_ino = s2.Unix.st_ino + with + Unix.Unix_error _ -> false) + with + Unix.Unix_error _ -> (fun _ -> false) diff --git a/lib/cUnix.mli b/lib/cUnix.mli new file mode 100644 index 000000000..00419bc97 --- /dev/null +++ b/lib/cUnix.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** {5 System utilities} *) + +type physical_path = string +type load_path = physical_path list + +val canonical_path_name : string -> string + +val physical_path_of_string : string -> physical_path +val string_of_physical_path : physical_path -> string + +val path_to_list : string -> string list + +val make_suffix : string -> string -> string +val file_readable_p : string -> bool + +(** {6 Executing commands } *) +(** [run_command converter f com] launches command [com], and returns + the contents of stdout and stderr that have been processed with + [converter]; the processed contents of stdout and stderr is also + passed to [f] *) + +val run_command : (string -> string) -> (string -> unit) -> string -> + Unix.process_status * string + diff --git a/lib/clib.mllib b/lib/clib.mllib new file mode 100644 index 000000000..65d3a1562 --- /dev/null +++ b/lib/clib.mllib @@ -0,0 +1,8 @@ +Coq_config +Segmenttree +Unicodetable +Util +Serialize +Flags +CUnix +Envars diff --git a/lib/envars.ml b/lib/envars.ml index 611b81a7e..4b0f57ada 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -9,8 +9,52 @@ (* This file gathers environment variables needed by Coq to run (such as coqlib) *) +let getenv_else s dft = try Sys.getenv s with Not_found -> dft () + +let safe_getenv warning n = getenv_else n (fun () -> + let () = warning ("Environment variable "^n^" not found: using '$"^n^"' .") + in ("$"^n)) + +(* Expanding shell variables and home-directories *) + +(* On win32, the home directory is probably not in $HOME, but in + some other environment variable *) + +let home ~warn = + getenv_else "HOME" (fun () -> + try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> + getenv_else "USERPROFILE" (fun () -> + warn ("Cannot determine user home directory, using '.' ."); + Filename.current_dir_name)) + +let expand_path_macros ~warn s = + let rec expand_atom s i = + let l = String.length s in + if i<l && (Util.is_digit s.[i] or Util.is_letter s.[i] or s.[i] = '_') + then expand_atom s (i+1) + else i in + let rec expand_macros s i = + let l = String.length s in + if i=l then s else + match s.[i] with + | '$' -> + let n = expand_atom s (i+1) in + let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in + let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in + expand_macros s (i + String.length v) + | '~' when i = 0 -> + let n = expand_atom s (i+1) in + let v = + if n=i+1 then home ~warn + else (Unix.getpwnam (String.sub s (i+1) (n-i-1))).Unix.pw_dir + in + let s = v^(String.sub s n (l-n)) in + expand_macros s (String.length v) + | c -> expand_macros s (i+1) + in expand_macros s 0 + let coqbin = - System.canonical_path_name (Filename.dirname Sys.executable_name) + CUnix.canonical_path_name (Filename.dirname Sys.executable_name) (* The following only makes sense when executables are running from source tree (e.g. during build or in local mode). *) @@ -21,14 +65,14 @@ let coqroot = Filename.dirname coqbin let _ = if Coq_config.arch = "win32" then - Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "") + Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> "")) let reldir instdir testfile oth = let rpath = if Coq_config.local then [] else instdir in let out = List.fold_left Filename.concat coqroot rpath in if Sys.file_exists (Filename.concat out testfile) then out else oth () -let guess_coqlib () = +let guess_coqlib fail = let file = "states/initial.coq" in reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file (fun () -> @@ -38,11 +82,11 @@ let guess_coqlib () = in if Sys.file_exists (Filename.concat coqlib file) then coqlib - else Errors.error "cannot guess a path for Coq libraries; please use -coqlib option") + else fail "cannot guess a path for Coq libraries; please use -coqlib option") -let coqlib () = +let coqlib ~fail = if !Flags.coqlib_spec then !Flags.coqlib else - (if !Flags.boot then coqroot else guess_coqlib ()) + (if !Flags.boot then coqroot else guess_coqlib fail) let docdir () = reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" (fun () -> Coq_config.docdir) @@ -51,14 +95,14 @@ let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in Util.split_string_at sep p -let xdg_data_home = +let xdg_data_home warning = Filename.concat - (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share")) + (getenv_else "XDG_DATA_HOME" (fun () -> Filename.concat (home warning) ".local/share")) "coq" -let xdg_config_home = +let xdg_config_home ~warn = Filename.concat - (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config")) + (getenv_else "XDG_CONFIG_HOME" (fun () -> Filename.concat (home ~warn) ".config")) "coq" let xdg_data_dirs = @@ -67,8 +111,8 @@ let xdg_data_dirs = with Not_found -> "/usr/local/share/coq" :: "/usr/share/coq" :: (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir]) -let xdg_dirs = - let dirs = xdg_data_home :: xdg_data_dirs +let xdg_dirs ~warn = + let dirs = xdg_data_home warn :: xdg_data_dirs in List.rev (List.filter Sys.file_exists dirs) @@ -107,7 +151,7 @@ let camllib () = else let camlbin = camlbin () in let com = (Filename.concat camlbin "ocamlc") ^ " -where" in - let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + let _,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res let camlp4bin () = @@ -123,7 +167,7 @@ let camlp4lib () = else let camlp4bin = camlp4bin () in let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in - let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + let _,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res diff --git a/lib/envars.mli b/lib/envars.mli index 0c80492f8..ff4cf4a56 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -9,14 +9,17 @@ (** This file gathers environment variables needed by Coq to run (such as coqlib) *) -val coqlib : unit -> string +val expand_path_macros : warn:(string -> unit) -> string -> string +val home : warn:(string -> unit) -> string + +val coqlib : fail:(string -> string) -> string val docdir : unit -> string val coqbin : string val coqroot : string (* coqpath is stored in reverse order, since that is the order it * gets added to the searc path *) -val xdg_config_home : string -val xdg_dirs : string list +val xdg_config_home : warn:(string -> unit) -> string +val xdg_dirs : warn:(string -> unit) -> string list val coqpath : string list val camlbin : unit -> string diff --git a/lib/interface.mli b/lib/interface.mli new file mode 100644 index 000000000..f2aba72e9 --- /dev/null +++ b/lib/interface.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Declarative part of the interface of CoqIde calls to Coq *) + +(** * Generic structures *) + +type raw = bool +type verbose = bool + +(** The type of coqtop goals *) +type goal = { + goal_hyp : string list; + (** List of hypotheses *) + goal_ccl : string; + (** Goal conclusion *) +} + +type evar = { + evar_info : string; + (** A string describing an evar: type, number, environment *) +} + +type status = { + status_path : string list; + (** Module path of the current proof *) + status_proofname : string option; + (** Current proof name. [None] if no focussed proof is in progress *) + status_allproofs : string list; + (** List of all pending proofs. Order is not significant *) + status_statenum : int; + (** A unique id describing the state of coqtop *) + status_proofnum : int; + (** An id describing the state of the current proof. *) +} + +type goals = { + fg_goals : goal list; + (** List of the focussed goals *) + bg_goals : goal list; + (** List of the background goals *) +} + +type hint = (string * string) list +(** A list of tactics applicable and their appearance *) + +type option_name = string list + +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +(** Summary of an option status *) +type option_state = { + opt_sync : bool; + (** Whether an option is synchronous *) + opt_depr : bool; + (** Wheter an option is deprecated *) + opt_name : string; + (** A short string that is displayed when using [Test] *) + opt_value : option_value; + (** The current value of the option *) +} + +(** * Coq answers to CoqIde *) + +type location = (int * int) option (* start and end of the error *) + +type 'a value = + | Good of 'a + | Fail of (location * string) + +(** * The structure that coqtop should implement *) + +type handler = { + interp : raw * verbose * string -> string; + rewind : int -> int; + goals : unit -> goals option; + evars : unit -> evar list option; + hints : unit -> (hint list * hint) option; + status : unit -> status; + get_options : unit -> (option_name * option_state) list; + set_options : (option_name * option_value) list -> unit; + inloadpath : string -> bool; + mkcases : string -> string list list; + handle_exn : exn -> location * string; +} diff --git a/lib/lib.mllib b/lib/lib.mllib index eb834af78..77fc4ab09 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,17 +3,12 @@ Xml_parser Xml_utils Pp_control Compat -Flags Pp -Segmenttree -Unicodetable Errors -Util Bigint Hashcons Dyn System -Envars Gmap Fset Fmap diff --git a/lib/serialize.ml b/lib/serialize.ml new file mode 100644 index 000000000..96cdc6c2c --- /dev/null +++ b/lib/serialize.ml @@ -0,0 +1,447 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Interface of calls to Coq by CoqIde *) + +open Interface + +type xml = + | Element of (string * (string * string) list * xml list) + | PCData of string + +(** We use phantom types and GADT to protect ourselves against wild casts *) + +type 'a call = + | Interp of raw * verbose * string + | Rewind of int + | Goal + | Evars + | Hints + | Status + | GetOptions + | SetOptions of (option_name * option_value) list + | InLoadPath of string + | MkCases of string + +(** The actual calls *) + +let interp (r,b,s) : string call = Interp (r,b,s) +let rewind i : int call = Rewind i +let goals : goals option call = Goal +let evars : evar list option call = Evars +let hints : (hint list * hint) option call = Hints +let status : status call = Status +let get_options : (option_name * option_state) list call = GetOptions +let set_options l : unit call = SetOptions l +let inloadpath s : bool call = InLoadPath s +let mkcases s : string list list call = MkCases s + +(** * Coq answers to CoqIde *) + +let abstract_eval_call handler c = + try + let res = match c with + | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string) + | Rewind i -> Obj.magic (handler.rewind i : int) + | Goal -> Obj.magic (handler.goals () : goals option) + | Evars -> Obj.magic (handler.evars () : evar list option) + | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) + | Status -> Obj.magic (handler.status () : status) + | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) + | SetOptions opts -> Obj.magic (handler.set_options opts : unit) + | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) + | MkCases s -> Obj.magic (handler.mkcases s : string list list) + in Good res + with e -> + let (l, str) = handler.handle_exn e in + Fail (l,str) + +(** * XML data marshalling *) + +exception Marshal_error + +(** Utility functions *) + +let massoc x l = + try List.assoc x l + with Not_found -> raise Marshal_error + +let constructor t c args = Element (t, ["val", c], args) + +let do_match constr t mf = match constr with +| Element (s, attrs, args) -> + if s = t then + let c = massoc "val" attrs in + mf c args + else raise Marshal_error +| _ -> raise Marshal_error + +let pcdata = function +| PCData s -> s +| _ -> raise Marshal_error + +let singleton = function +| [x] -> x +| _ -> raise Marshal_error + +let raw_string = function +| [] -> "" +| [PCData s] -> s +| _ -> raise Marshal_error + +let bool_arg tag b = if b then [tag, ""] else [] + +(** Base types *) + +let of_bool b = + if b then constructor "bool" "true" [] + else constructor "bool" "false" [] + +let to_bool xml = do_match xml "bool" + (fun s _ -> match s with + | "true" -> true + | "false" -> false + | _ -> raise Marshal_error) + +let of_list f l = + Element ("list", [], List.map f l) + +let to_list f = function +| Element ("list", [], l) -> + List.map f l +| _ -> raise Marshal_error + +let of_option f = function +| None -> Element ("option", ["val", "none"], []) +| Some x -> Element ("option", ["val", "some"], [f x]) + +let to_option f = function +| Element ("option", ["val", "none"], []) -> None +| Element ("option", ["val", "some"], [x]) -> Some (f x) +| _ -> raise Marshal_error + +let of_string s = Element ("string", [], [PCData s]) + +let to_string = function +| Element ("string", [], l) -> raw_string l +| _ -> raise Marshal_error + +let of_int i = Element ("int", [], [PCData (string_of_int i)]) + +let to_int = function +| Element ("int", [], [PCData s]) -> int_of_string s +| _ -> raise Marshal_error + +let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) + +let to_pair f g = function +| Element ("pair", [], [x; y]) -> (f x, g y) +| _ -> raise Marshal_error + +(** More elaborate types *) + +let of_option_value = function +| IntValue i -> + constructor "option_value" "intvalue" [of_option of_int i] +| BoolValue b -> + constructor "option_value" "boolvalue" [of_bool b] +| StringValue s -> + constructor "option_value" "stringvalue" [of_string s] + +let to_option_value xml = do_match xml "option_value" + (fun s args -> match s with + | "intvalue" -> IntValue (to_option to_int (singleton args)) + | "boolvalue" -> BoolValue (to_bool (singleton args)) + | "stringvalue" -> StringValue (to_string (singleton args)) + | _ -> raise Marshal_error + ) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value] + ) + +let to_option_state = function +| Element ("option_state", [], [sync; depr; name; value]) -> + { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value; + } +| _ -> raise Marshal_error + +let of_value f = function +| Good x -> Element ("value", ["val", "good"], [f x]) +| Fail (loc, msg) -> + let loc = match loc with + | None -> [] + | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] + in + Element ("value", ["val", "fail"] @ loc, [PCData msg]) + +let to_value f = function +| Element ("value", attrs, l) -> + let ans = massoc "val" attrs in + if ans = "good" then Good (f (singleton l)) + else if ans = "fail" then + let loc = + try + let loc_s = int_of_string (List.assoc "loc_s" attrs) in + let loc_e = int_of_string (List.assoc "loc_e" attrs) in + Some (loc_s, loc_e) + with _ -> None + in + let msg = raw_string l in + Fail (loc, msg) + else raise Marshal_error +| _ -> raise Marshal_error + +let of_call = function +| Interp (raw, vrb, cmd) -> + let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in + Element ("call", ("val", "interp") :: flags, [PCData cmd]) +| Rewind n -> + Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) +| Goal -> + Element ("call", ["val", "goal"], []) +| Evars -> + Element ("call", ["val", "evars"], []) +| Hints -> + Element ("call", ["val", "hints"], []) +| Status -> + Element ("call", ["val", "status"], []) +| GetOptions -> + Element ("call", ["val", "getoptions"], []) +| SetOptions opts -> + let args = List.map (of_pair (of_list of_string) of_option_value) opts in + Element ("call", ["val", "setoptions"], args) +| InLoadPath file -> + Element ("call", ["val", "inloadpath"], [PCData file]) +| MkCases ind -> + Element ("call", ["val", "mkcases"], [PCData ind]) + +let to_call = function +| Element ("call", attrs, l) -> + let ans = massoc "val" attrs in + begin match ans with + | "interp" -> + let raw = List.mem_assoc "raw" attrs in + let vrb = List.mem_assoc "verbose" attrs in + Interp (raw, vrb, raw_string l) + | "rewind" -> + let steps = int_of_string (massoc "steps" attrs) in + Rewind steps + | "goal" -> Goal + | "evars" -> Evars + | "status" -> Status + | "getoptions" -> GetOptions + | "setoptions" -> + let args = List.map (to_pair (to_list to_string) to_option_value) l in + SetOptions args + | "inloadpath" -> InLoadPath (raw_string l) + | "mkcases" -> MkCases (raw_string l) + | "hints" -> Hints + | _ -> raise Marshal_error + end +| _ -> raise Marshal_error + +let of_status s = + let of_so = of_option of_string in + let of_sl = of_list of_string in + Element ("status", [], + [ + of_sl s.status_path; + of_so s.status_proofname; + of_sl s.status_allproofs; + of_int s.status_statenum; + of_int s.status_proofnum; + ] + ) + +let to_status = function +| Element ("status", [], [path; name; prfs; snum; pnum]) -> + { + status_path = to_list to_string path; + status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_statenum = to_int snum; + status_proofnum = to_int pnum; + } +| _ -> raise Marshal_error + +let of_evar s = + Element ("evar", [], [PCData s.evar_info]) + +let to_evar = function +| Element ("evar", [], data) -> { evar_info = raw_string data; } +| _ -> raise Marshal_error + +let of_goal g = + let hyp = of_list of_string g.goal_hyp in + let ccl = of_string g.goal_ccl in + Element ("goal", [], [hyp; ccl]) + +let to_goal = function +| Element ("goal", [], [hyp; ccl]) -> + let hyp = to_list to_string hyp in + let ccl = to_string ccl in + { goal_hyp = hyp; goal_ccl = ccl } +| _ -> raise Marshal_error + +let of_goals g = + let fg = of_list of_goal g.fg_goals in + let bg = of_list of_goal g.bg_goals in + Element ("goals", [], [fg; bg]) + +let to_goals = function +| Element ("goals", [], [fg; bg]) -> + let fg = to_list to_goal fg in + let bg = to_list to_goal bg in + { fg_goals = fg; bg_goals = bg; } +| _ -> raise Marshal_error + +let of_hints = + let of_hint = of_list (of_pair of_string of_string) in + of_option (of_pair (of_list of_hint) of_hint) + +let of_answer (q : 'a call) (r : 'a value) = + let convert = match q with + | Interp _ -> Obj.magic (of_string : string -> xml) + | Rewind _ -> Obj.magic (of_int : int -> xml) + | Goal -> Obj.magic (of_option of_goals : goals option -> xml) + | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) + | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) + | Status -> Obj.magic (of_status : status -> xml) + | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) + | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) + | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) + | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) + in + of_value convert r + +let to_answer xml = + let rec convert elt = match elt with + | Element (tpe, attrs, l) -> + begin match tpe with + | "unit" -> Obj.magic () + | "string" -> Obj.magic (to_string elt : string) + | "int" -> Obj.magic (to_int elt : int) + | "status" -> Obj.magic (to_status elt : status) + | "bool" -> Obj.magic (to_bool elt : bool) + | "list" -> Obj.magic (to_list convert elt : 'a list) + | "option" -> Obj.magic (to_option convert elt : 'a option) + | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) + | "goals" -> Obj.magic (to_goals elt : goals) + | "evar" -> Obj.magic (to_evar elt : evar) + | "option_value" -> Obj.magic (to_option_value elt : option_value) + | "option_state" -> Obj.magic (to_option_state elt : option_state) + | _ -> raise Marshal_error + end + | _ -> raise Marshal_error + in + to_value convert xml + +(** * Debug printing *) + +let pr_option_value = function +| IntValue None -> "none" +| IntValue (Some i) -> string_of_int i +| StringValue s -> s +| BoolValue b -> if b then "true" else "false" + +let rec pr_setoptions opts = + let map (key, v) = + let key = String.concat " " key in + key ^ " := " ^ (pr_option_value v) + in + String.concat "; " (List.map map opts) + +let pr_getoptions opts = + let map (key, s) = + let key = String.concat " " key in + Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n" + key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + in + "\n" ^ String.concat "" (List.map map opts) + +let pr_call = function + | Interp (r,b,s) -> + let raw = if r then "RAW" else "" in + let verb = if b then "" else "SILENT" in + "INTERP"^raw^verb^" ["^s^"]" + | Rewind i -> "REWIND "^(string_of_int i) + | Goal -> "GOALS" + | Evars -> "EVARS" + | Hints -> "HINTS" + | Status -> "STATUS" + | GetOptions -> "GETOPTIONS" + | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" + | InLoadPath s -> "INLOADPATH "^s + | MkCases s -> "MKCASES "^s + +let pr_value_gen pr = function + | Good v -> "GOOD " ^ pr v + | Fail (_,str) -> "FAIL ["^str^"]" + +let pr_value v = pr_value_gen (fun _ -> "") v + +let pr_string s = "["^s^"]" +let pr_bool b = if b then "true" else "false" + +let pr_status s = + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" + in + let name = match s.status_proofname with + | None -> "no proof;" + | Some n -> "proof = " ^ n ^ ";" + in + "Status: " ^ path ^ name + +let pr_mkcases l = + let l = List.map (String.concat " ") l in + "[" ^ String.concat " | " l ^ "]" + +let pr_goals_aux g = + if g.fg_goals = [] then + if g.bg_goals = [] then "Proof completed." + else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) + else + let pr_menu s = s in + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]" + in + String.concat " " (List.map pr_goal g.fg_goals) + +let pr_goals = function +| None -> "No proof in progress." +| Some g -> pr_goals_aux g + +let pr_evar ev = "[" ^ ev.evar_info ^ "]" + +let pr_evars = function +| None -> "No proof in progress." +| Some evars -> String.concat " " (List.map pr_evar evars) + +let pr_full_value call value = + match call with + | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value) + | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value) + | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value) + | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) + | Hints -> pr_value value + | Status -> pr_value_gen pr_status (Obj.magic value : status value) + | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) + | SetOptions _ -> pr_value value + | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) + | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) diff --git a/lib/serialize.mli b/lib/serialize.mli new file mode 100644 index 000000000..2ab557c53 --- /dev/null +++ b/lib/serialize.mli @@ -0,0 +1,89 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Applicative part of the interface of CoqIde calls to Coq *) + +open Interface + +type xml = + | Element of (string * (string * string) list * xml list) + | PCData of string + +type 'a call + +(** Running a command (given as a string). + - The 1st flag indicates whether to use "raw" mode + (less sanity checks, no impact on the undo stack). + Suitable e.g. for queries, or for the Set/Unset + of display options that coqide performs all the time. + - The 2nd flag controls the verbosity. + - The returned string contains the messages produced + by this command, but not the updated goals (they are + to be fetch by a separated [current_goals]). *) +val interp : raw * verbose * string -> string call + +(** Backtracking by at least a certain number of phrases. + No finished proofs will be re-opened. Instead, + we continue backtracking until before these proofs, + and answer the amount of extra backtracking performed. + Backtracking by more than the number of phrases already + interpreted successfully (and not yet undone) will fail. *) +val rewind : int -> int call + +(** Fetching the list of current goals. Return [None] if no proof is in + progress, [Some gl] otherwise. *) +val goals : goals option call + +(** Retrieving the tactics applicable to the current goal. [None] if there is + no proof in progress. *) +val hints : (hint list * hint) option call + +(** The status, for instance "Ready in SomeSection, proving Foo" *) +val status : status call + +(** Is a directory part of Coq's loadpath ? *) +val inloadpath : string -> bool call + +(** Create a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. *) +val mkcases : string -> string list list call + +(** Retrieve the list of unintantiated evars in the current proof. [None] if no + proof is in progress. *) +val evars : evar list option call + +(** Retrieve the list of options of the current toplevel, together with their + state. *) +val get_options : (option_name * option_state) list call + +(** Set the options to the given value. Warning: this is not atomic, so whenever + the call fails, the option state can be messed up... This is the caller duty + to check that everything is correct. *) +val set_options : (option_name * option_value) list -> unit call + +val abstract_eval_call : handler -> 'a call -> 'a value + +(** * XML data marshalling *) + +exception Marshal_error + +val of_value : ('a -> xml) -> 'a value -> xml +val to_value : (xml -> 'a) -> xml -> 'a value + +val of_call : 'a call -> xml +val to_call : xml -> 'a call + +val of_answer : 'a call -> 'a value -> xml +val to_answer : xml -> 'a value + +(** * Debug printing *) + +val pr_call : 'a call -> string +val pr_value : 'a value -> string +val pr_full_value : 'a call -> 'a value -> string diff --git a/lib/system.ml b/lib/system.ml index 7e0347530..1537f4892 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -13,123 +13,6 @@ open Errors open Util open Unix -(* Expanding shell variables and home-directories *) - -let safe_getenv_def var def = - try - Sys.getenv var - with Not_found -> - warning ("Environment variable "^var^" not found: using '"^def^"' ."); - flush_all (); - def - -let getenv_else s dft = try Sys.getenv s with Not_found -> dft - -(* On win32, the home directory is probably not in $HOME, but in - some other environment variable *) - -let home = - try Sys.getenv "HOME" with Not_found -> - try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> - try Sys.getenv "USERPROFILE" with Not_found -> - warning ("Cannot determine user home directory, using '.' ."); - flush_all (); - Filename.current_dir_name - -let safe_getenv n = safe_getenv_def n ("$"^n) - -let rec expand_atom s i = - let l = String.length s in - if i<l && (is_digit s.[i] or is_letter s.[i] or s.[i] = '_') - then expand_atom s (i+1) - else i - -let rec expand_macros s i = - let l = String.length s in - if i=l then s else - match s.[i] with - | '$' -> - let n = expand_atom s (i+1) in - let v = safe_getenv (String.sub s (i+1) (n-i-1)) in - let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in - expand_macros s (i + String.length v) - | '~' when i = 0 -> - let n = expand_atom s (i+1) in - let v = - if n=i+1 then home - else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir - in - let s = v^(String.sub s n (l-n)) in - expand_macros s (String.length v) - | c -> expand_macros s (i+1) - -let expand_path_macros s = expand_macros s 0 - -(* Files and load path. *) - -type physical_path = string -type load_path = physical_path list - -let physical_path_of_string s = s -let string_of_physical_path p = p - -(* - * Split a path into a list of directories. A one-liner with Str, but Coq - * doesn't seem to use this library at all, so here is a slighly longer version. - *) - -let lpath_from_path path path_separator = - let n = String.length path in - let rec aux i l = - if i < n then - let j = - try String.index_from path i path_separator - with Not_found -> n - in - let dir = String.sub path i (j-i) in - aux (j+1) (dir::l) - else - l - in List.rev (aux 0 []) - -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - let l = String.length p in - if l > n && String.sub p 0 n = curdir then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - let l = String.length p in - if l > n && String.sub p 0 n = cwd then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p - (* All subdirectories, recursively *) let exists_dir dir = @@ -212,17 +95,11 @@ let is_in_path lpath filename = let path_separator = if Sys.os_type = "Unix" then ':' else ';' let is_in_system_path filename = - let path = try Sys.getenv "PATH" + let path = try Sys.getenv "PATH" with Not_found -> error "system variable PATH not found" in - let lpath = lpath_from_path path path_separator in + let lpath = CUnix.path_to_list path in is_in_path lpath filename -let make_suffix name suffix = - if Filename.check_suffix name suffix then name else (name ^ suffix) - -let file_readable_p name = - try access name [R_OK];true with Unix_error (_, _, _) -> false - let open_trapping_failure name = try open_out_bin name with _ -> error ("Can't open " ^ name) @@ -240,7 +117,7 @@ exception Bad_magic_number of string let raw_extern_intern magic suffix = let extern_state name = - let filename = make_suffix name suffix in + let filename = CUnix.make_suffix name suffix in let channel = open_trapping_failure filename in output_binary_int channel magic; filename,channel @@ -265,7 +142,7 @@ let extern_intern ?(warn=true) magic suffix = with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in + let _,filename = find_file_in_path ~warn paths (CUnix.make_suffix name suffix) in let channel = raw_intern filename in let v = marshal_in channel in close_in channel; @@ -279,7 +156,7 @@ let with_magic_number_check f a = try f a with Bad_magic_number fname -> errorlabstrm "with_magic_number_check" - (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ + (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") (* Communication through files with another executable *) @@ -318,26 +195,6 @@ let connect writefun readfun com = unlink tmp_to; a -let run_command converter f c = - let result = Buffer.create 127 in - let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in - let buff = String.make 127 ' ' in - let buffe = String.make 127 ' ' in - let n = ref 0 in - let ne = ref 0 in - - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; - !n+ !ne <> 0 - do - let r = converter (String.sub buff 0 !n) in - f r; - Buffer.add_string result r; - let r = converter (String.sub buffe 0 !ne) in - f r; - Buffer.add_string result r - done; - (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) - (* Time stamps. *) type time = float * float * float diff --git a/lib/system.mli b/lib/system.mli index fae7fd1ed..89fd9df60 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** System utilities *) +(** {5 Coqtop specific system utilities} *) (** {6 Files and load paths} *) @@ -14,32 +14,17 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -type physical_path = string -type load_path = physical_path list - -val canonical_path_name : string -> string - val exclude_search_in_dirname : string -> unit -val all_subdirs : unix_path:string -> (physical_path * string list) list -val is_in_path : load_path -> string -> bool +val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list +val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool -val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string - -val physical_path_of_string : string -> physical_path -val string_of_physical_path : physical_path -> string - -val make_suffix : string -> string -> string -val file_readable_p : string -> bool - -val expand_path_macros : string -> string -val getenv_else : string -> string -> string -val home : string +val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string val exists_dir : string -> bool val find_file_in_path : - ?warn:bool -> load_path -> string -> physical_path * string + ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number @@ -55,7 +40,7 @@ val raw_extern_intern : int -> string -> (string -> string * out_channel) * (string -> in_channel) val extern_intern : ?warn:bool -> int -> string -> - (string -> 'a -> unit) * (load_path -> string -> 'a) + (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b @@ -63,15 +48,6 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a -(** {6 Executing commands } *) -(** [run_command converter f com] launches command [com], and returns - the contents of stdout and stderr that have been processed with - [converter]; the processed contents of stdout and stderr is also - passed to [f] *) - -val run_command : (string -> string) -> (string -> unit) -> string -> - Unix.process_status * string - (** {6 Time stamps.} *) type time diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index bf931d75b..014331202 100644 --- a/lib/xml_parser.ml +++ b/lib/xml_parser.ml @@ -20,7 +20,7 @@ open Printf -type xml = +type xml = Serialize.xml = | Element of (string * (string * string) list * xml list) | PCData of string diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index e3e7ac4dc..2c83eee9d 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -27,9 +27,7 @@ (** An Xml node is either [Element (tag-name, attributes, children)] or [PCData text] *) -type xml = - | Element of (string * (string * string) list * xml list) - | PCData of string +type xml = Serialize.xml (** Abstract type for an Xml parser. *) type t diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml index 310035862..1d09b1723 100644 --- a/lib/xml_utils.ml +++ b/lib/xml_utils.ml @@ -18,7 +18,7 @@ *) open Printf -open Xml_parser +open Serialize exception Not_element of xml exception Not_pcdata of xml |