open Printf
open MatitaTypes
+let strip_trailing_slash =
+ let rex = Pcre.regexp "/$" in
+ fun s -> Pcre.replace ~rex s
+
+let baseuri_of_baseuri_decl st =
+ match st with
+ | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
+ Some buri
+ | _ -> None
+
+let baseuri_of_file file =
+ let uri = ref None in
+ let ic = open_in file in
+ let istream = Stream.of_channel ic in
+ (try
+ while true do
+ try
+ let stm = GrafiteParser.parse_statement istream in
+ match baseuri_of_baseuri_decl stm with
+ | Some buri ->
+ let u = strip_trailing_slash buri in
+ if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+ MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+ (try
+ ignore(Http_getter.resolve u)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | Http_getter_types.Key_not_found _ -> ());
+ uri := Some u;
+ raise End_of_file
+ | None -> ()
+ with
+ CicNotationParser.Parse_error _ as exn ->
+ prerr_endline ("Unable to parse: " ^ file);
+ prerr_endline (MatitaExcPp.to_string exn);
+ ()
+ done
+ with End_of_file -> close_in ic);
+ match !uri with
+ | Some uri -> uri
+ | None -> failwith ("No baseuri defined in " ^ file)
+
+let is_empty buri =
+ List.for_all
+ (function
+ Http_getter_types.Ls_section _ -> true
+ | Http_getter_types.Ls_object _ -> false)
+ (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
+
+let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
+
let is_dir fname =
try
(Unix.stat fname).Unix.st_kind = Unix.S_DIR
close_in ic;
Buffer.contents buf
+let output_file data file =
+ let oc = open_out file in
+ output_string oc data;
+ close_out oc
+
+
+let absolute_path file =
+ if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
+
let is_proof_script fname = true (** TODO Zack *)
let is_proof_object fname = true (** TODO Zack *)
else
s
+let mkdir path =
+ let components = Str.split (Str.regexp "/") path in
+ let rec aux where = function
+ | [] -> ()
+ | piece::tl ->
+ let path = where ^ "/" ^ piece in
+ (try
+ Unix.mkdir path 0o755
+ with
+ | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
+ | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
+ aux path tl
+ in
+ aux "" components
+
let strip_trailing_blanks =
let rex = Pcre.regexp "\\s*$" in
fun s -> Pcre.replace ~rex s
-let strip_trailing_slash =
- let rex = Pcre.regexp "/$" in
- fun s -> Pcre.replace ~rex s
+let split ?(char = ' ') s =
+ let pieces = ref [] in
+ let rec aux idx =
+ match (try Some (String.index_from s idx char) with Not_found -> None) with
+ | Some pos ->
+ pieces := String.sub s idx (pos - idx) :: !pieces;
+ aux (pos + 1)
+ | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces
+ in
+ aux 0;
+ List.rev !pieces
let empty_mathml () =
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
let instance = lazy (f ()) in
fun () -> Lazy.force instance
-let mkdir d =
- let errmsg = sprintf "Unable to create directory \"%s\"" d in
- try
- (match Unix.system ("mkdir -p " ^ d) with
- | Unix.WEXITED 0 -> ()
- | _ -> failwith errmsg)
- with Unix.Unix_error _ -> failwith errmsg
-
let get_proof_status status =
match status.proof_status with
| Incomplete_proof s -> s
context
| _ -> []
+let get_proof_conclusion status =
+ match status.proof_status with
+ | Incomplete_proof ((_, metasenv, _, _), goal) ->
+ let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
+ conclusion
+ | _ -> statement_error "no ongoing proof"
+
let get_proof_aliases status = status.aliases
-
+
let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
let unopt = function None -> failwith "unopt: None" | Some v -> v
let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
let end_ma_RE = Pcre.regexp "\\.ma$"
-let obj_file_of_script f = Pcre.replace ~rex:end_ma_RE ~templ:".moo" f
+
+let obj_file_of_baseuri baseuri =
+ let path =
+ Helm_registry.get "matita.basedir" ^ "/xml" ^
+ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri
+ in
+ path ^ ".moo"
+
+let obj_file_of_script f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+ let baseuri = baseuri_of_file f in
+ obj_file_of_baseuri baseuri
let rec list_uniq = function
| [] -> []
| h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl)
| h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
-let end_ma_RE = Pcre.regexp "\\.ma$"
+let list_tl_at ?(equality=(==)) e l =
+ let rec aux =
+ function
+ | [] -> raise Not_found
+ | hd :: tl as l when equality hd e -> l
+ | hd :: tl -> aux tl
+ in
+ aux l
+
+let debug_wrap name f =
+ prerr_endline (sprintf "debug_wrap: ==>> %s" name);
+ let res = f () in
+ prerr_endline (sprintf "debug_wrap: <<== %s" name);
+ res
+