diff options
-rw-r--r-- | checker/check.mllib | 2 | ||||
-rw-r--r-- | dev/printers.mllib | 2 | ||||
-rw-r--r-- | kernel/csymtable.ml | 6 | ||||
-rw-r--r-- | kernel/entries.mli | 2 | ||||
-rw-r--r-- | kernel/pre_env.ml | 8 | ||||
-rw-r--r-- | kernel/pre_env.mli | 2 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
-rw-r--r-- | kernel/term_typing.ml | 4 | ||||
-rw-r--r-- | lib/cEphemeron.ml (renamed from lib/ephemeron.ml) | 0 | ||||
-rw-r--r-- | lib/cEphemeron.mli (renamed from lib/ephemeron.mli) | 0 | ||||
-rw-r--r-- | lib/future.ml | 8 | ||||
-rw-r--r-- | lib/lib.mllib | 2 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
-rw-r--r-- | proofs/proof_global.ml | 28 | ||||
-rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
-rw-r--r-- | toplevel/obligations.ml | 16 |
18 files changed, 46 insertions, 46 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 0d36e3a0f..902ab9ddf 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -32,7 +32,7 @@ CStack Util Ppstyle Errors -Ephemeron +CEphemeron Future CUnix System diff --git a/dev/printers.mllib b/dev/printers.mllib index ab7e9fc34..ad9a5d75e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -48,7 +48,7 @@ Rtree Heap Genarg Stateid -Ephemeron +CEphemeron Future RemoteCounter Monad diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index fc7e1b937..7e1a5d5b7 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -131,8 +131,8 @@ let key rk = match !rk with | None -> raise NotEvaluated | Some k -> - try Ephemeron.get k - with Ephemeron.InvalidKey -> raise NotEvaluated + try CEphemeron.get k + with CEphemeron.InvalidKey -> raise NotEvaluated (************************) (* traduction des patch *) @@ -171,7 +171,7 @@ let rec slot_for_getglobal env kn = | BCconstant -> set_global (val_of_constant kn) in (*Pp.msgnl(str"value stored at: "++int pos);*) - rk := Some (Ephemeron.create pos); + rk := Some (CEphemeron.create pos); pos and slot_for_fv env fv = diff --git a/kernel/entries.mli b/kernel/entries.mli index b2a77dd95..f94068f31 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -104,7 +104,7 @@ type side_eff = | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string type side_effect = { - from_env : Declarations.structure_body Ephemeron.key; + from_env : Declarations.structure_body CEphemeron.key; eff : side_eff; } diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index e1fe02595..df3495569 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -25,7 +25,7 @@ open Declarations (* The key attached to each constant is used by the VM to retrieve previous *) (* evaluations of the constant. It is essentially an index in the symbols table *) (* used by the VM. *) -type key = int Ephemeron.key option ref +type key = int CEphemeron.key option ref (** Linking information for the native compiler. *) @@ -50,17 +50,17 @@ type stratification = { } type val_kind = - | VKvalue of (values * Id.Set.t) Ephemeron.key + | VKvalue of (values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref let force_lazy_val vk = match !vk with | VKnone -> None -| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None let dummy_lazy_val () = ref VKnone -let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key) +let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) type named_vals = (Id.t * lazy_val) list diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 23f9a3f41..99d3e2e25 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -19,7 +19,7 @@ type link_info = | LinkedInteractive of string | NotLinked -type key = int Ephemeron.key option ref +type key = int CEphemeron.key option ref type constant_key = constant_body * (link_info ref * key) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4c3264861..0926d35f6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -231,11 +231,11 @@ let constant_entry_of_private_constant = function let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - { Entries.from_env = Ephemeron.create env.revstruct; + { Entries.from_env = CEphemeron.create env.revstruct; Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } let private_con_of_scheme ~kind env cl = - { Entries.from_env = Ephemeron.create env.revstruct; + { Entries.from_env = CEphemeron.create env.revstruct; Entries.eff = Entries.SEscheme( List.map (fun (i,c) -> let cbo = Environ.lookup_constant c env.env in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 510f43542..fdbd1e3b1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -126,14 +126,14 @@ let check_signatures curmb sl = | None -> None, None | Some curmb -> try - let mb = Ephemeron.get mb in + let mb = CEphemeron.get mb in match sl with | None -> sl, None | Some n -> if List.length mb >= how_many && CList.skipn how_many mb == curmb then Some (n + how_many), Some mb else None, None - with Ephemeron.InvalidKey -> None, None in + with CEphemeron.InvalidKey -> None, None in let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in sl diff --git a/lib/ephemeron.ml b/lib/cEphemeron.ml index a38ea11e1..a38ea11e1 100644 --- a/lib/ephemeron.ml +++ b/lib/cEphemeron.ml diff --git a/lib/ephemeron.mli b/lib/cEphemeron.mli index 1200e4e20..1200e4e20 100644 --- a/lib/ephemeron.mli +++ b/lib/cEphemeron.mli diff --git a/lib/future.ml b/lib/future.ml index 5cd2beba9..e8f33db5e 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -62,7 +62,7 @@ and 'a comp = | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = - | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key + | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key | Finished of 'a and 'a computation = 'a comput ref @@ -70,13 +70,13 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x))) + ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None)) | Ongoing (name, x) -> - try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c - with Ephemeron.InvalidKey -> + try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c + with CEphemeron.InvalidKey -> name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null)) type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] diff --git a/lib/lib.mllib b/lib/lib.mllib index f3f6ad8fc..6805ce491 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -15,6 +15,6 @@ Rtree Heap Unionfind Genarg -Ephemeron +CEphemeron Future RemoteCounter diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c47602bda..18200307a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -291,7 +291,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true, Ephemeron.create hook + get_proof_clean true, CEphemeron.create hook end diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index aa47e2619..2449678a1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 23f1da1ba..e5c756f56 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - unit Lemmas.declaration_hook Ephemeron.key -> unit + unit Lemmas.declaration_hook CEphemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f22cdbcc8..541f299d4 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -36,7 +36,7 @@ let find_proof_mode n = Errors.error (Format.sprintf "No proof mode named \"%s\"." n) let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (Ephemeron.create m) + Hashtbl.add proof_modes n (CEphemeron.create m) (* initial mode: standard mode *) let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } @@ -52,7 +52,7 @@ let _ = optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; optread = begin fun () -> - (Ephemeron.default !default_proof_mode standard).name + (CEphemeron.default !default_proof_mode standard).name end; optwrite = begin fun n -> default_proof_mode := find_proof_mode n @@ -83,12 +83,12 @@ type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; - terminator : proof_terminator Ephemeron.key; + terminator : proof_terminator CEphemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; - mode : proof_mode Ephemeron.key; + mode : proof_mode CEphemeron.key; universe_binders: universe_binders option; } @@ -103,11 +103,11 @@ let current_proof_mode = ref !default_proof_mode let update_proof_mode () = match !pstates with | { mode = m } :: _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := m; - Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ()) + CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) | _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := find_proof_mode "No" (* combinators for the current_proof lists *) @@ -215,9 +215,9 @@ let set_proof_mode mn = set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) let activate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) let disactivate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) (** [start_proof sigma id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and @@ -230,7 +230,7 @@ let disactivate_proof_mode mode = let start_proof sigma id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.start sigma goals; endline_tactic = None; section_vars = None; @@ -242,7 +242,7 @@ let start_proof sigma id ?pl str goals terminator = let start_dependent_proof id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.dependent_start goals; endline_tactic = None; section_vars = None; @@ -375,7 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, - fun pr_ending -> Ephemeron.get terminator pr_ending + fun pr_ending -> CEphemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -423,11 +423,11 @@ let close_proof ~keep_body_ucst_separate fix_exn = (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator +let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator let set_terminator hook = match !pstates with | [] -> raise NoCurrentProof - | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps + | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cc9732604..5f018ec39 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -314,7 +314,7 @@ module Make(T : Task) = struct let response = slave_respond request in report_status "Idle"; marshal_response (Option.get !slave_oc) response; - Ephemeron.clear () + CEphemeron.clear () with | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 7e0d30a63..615257a1c 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -324,11 +324,11 @@ type program_info_aux = { prg_sign: named_context_val; } -type program_info = program_info_aux Ephemeron.key +type program_info = program_info_aux CEphemeron.key let get_info x = - try Ephemeron.get x - with Ephemeron.InvalidKey -> + try CEphemeron.get x + with CEphemeron.InvalidKey -> Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker") let assumption_message = Declare.assumption_message @@ -461,7 +461,7 @@ let subst_deps_obl obls obl = module ProgMap = Map.Make(Id) -let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m) +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] @@ -682,7 +682,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m; + if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; !i exception Found of program_info @@ -690,7 +690,7 @@ exception Found of program_info let map_first m = try ProgMap.iter (fun _ v -> - if snd (Ephemeron.get v).prg_obligations > 0 then + if snd (CEphemeron.get v).prg_obligations > 0 then raise (Found v)) m; assert(false) with Found x -> x @@ -1016,7 +1016,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit else ( let len = Array.length obls in let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in - progmap_add n (Ephemeron.create prg); + progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res @@ -1030,7 +1030,7 @@ let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(r (fun (n, b, t, imps, obls) -> let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook - in progmap_add n (Ephemeron.create prg)) l; + in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> if finished then finished |