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
- with Unix.Unix_error _ -> false
-
-let is_regular fname =
- try
- (Unix.stat fname).Unix.st_kind = Unix.S_REG
- with Unix.Unix_error _ -> false
-
-let input_file fname =
- let size = (Unix.stat fname).Unix.st_size in
- let buf = Buffer.create size in
- let ic = open_in fname in
- Buffer.add_channel buf ic size;
- 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 is_dir_empty d =
+ try
+ let od = Unix.opendir d in
+ try
+ ignore (Unix.readdir od);
+ ignore (Unix.readdir od);
+ ignore (Unix.readdir od);
+ Unix.closedir od;
+ false
+ with End_of_file ->
+ Unix.closedir od;
+ true
+ with Unix.Unix_error _ -> true
+
+let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
+
+let rec rmdir_descend d =
+ if is_dir_empty d then
+ begin
+ safe_rmdir d;
+ rmdir_descend (Filename.dirname d)
+ end
let absolute_path file =
if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
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 trim_blanks =
- let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in
- fun s -> (Pcre.extract ~rex s).(1)
-
-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 () =
+let empty_mathml = lazy (
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
- ~qualifiedName:(Gdome.domString "math") ~doctype:None
+ ~qualifiedName:(Gdome.domString "math") ~doctype:None)
-let empty_boxml () =
+let empty_boxml = lazy (
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns)
- ~qualifiedName:(Gdome.domString "box") ~doctype:None
+ ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+
+let closed_goal_mathml = lazy (
+ DomMisc.domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
exception History_failure
let instance = lazy (f ()) in
fun () -> Lazy.force instance
-let get_proof_status status =
+let get_current_proof status =
match status.proof_status with
- | Incomplete_proof s -> s
+ | Incomplete_proof { proof = p } -> p
| _ -> statement_error "no ongoing proof"
let get_proof_metasenv status =
match status.proof_status with
| No_proof -> []
- | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv
- | Proof (_, metasenv, _, _) -> metasenv
- | Intermediate m -> m
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
-let get_proof_context status =
+let get_proof_context status goal =
match status.proof_status with
- | Incomplete_proof ((_, metasenv, _, _), goal) ->
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
context
| _ -> []
-let get_proof_conclusion status =
+let get_proof_conclusion status goal =
match status.proof_status with
- | Incomplete_proof ((_, metasenv, _, _), goal) ->
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
conclusion
| _ -> statement_error "no ongoing proof"
+
+let get_stack status =
+ match status.proof_status with
+ | Incomplete_proof p -> p.stack
+ | Proof _ -> Continuationals.Stack.empty
+ | _ -> assert false
+
+let set_stack stack status =
+ match status.proof_status with
+ | Incomplete_proof p ->
+ { status with proof_status = Incomplete_proof { p with stack = stack } }
+ | Proof _ ->
+ assert (Continuationals.Stack.is_empty stack);
+ status
+ | _ -> assert false
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 baseuri = baseuri_of_file f in
obj_file_of_baseuri baseuri
-let rec list_uniq = function
- | [] -> []
- | h::[] -> [h]
- | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl)
- | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
-
let list_tl_at ?(equality=(==)) e l =
let rec aux =
function
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
-
projects / helm.git / blobdiff