diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-19 18:16:23 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-19 18:16:23 +0000 |
commit | 51684142c40fced940bb870742bc7f75c3e2fd52 (patch) | |
tree | 9a8e883e7c53d2fa23ef8f0d9deffabeccfeb56e /lib | |
parent | 09d7951e0c0009e4ac55091cede25b88576759d2 (diff) |
Modulification and removing of structural equality in Stateid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r-- | lib/interface.mli | 2 | ||||
-rw-r--r-- | lib/serialize.ml | 10 | ||||
-rw-r--r-- | lib/stateid.ml | 29 | ||||
-rw-r--r-- | lib/stateid.mli | 30 |
4 files changed, 37 insertions, 34 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 274dbbb77..560d80d83 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -117,7 +117,7 @@ type message = { (** Coq "semantic" infos obtained during parsing/execution *) type edit_id = int -type state_id = Stateid.state_id +type state_id = Stateid.t type edit_or_state_id = Edit of edit_id | State of state_id type feedback_content = diff --git a/lib/serialize.ml b/lib/serialize.ml index 6636c24f0..c6eaa4eda 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -355,9 +355,9 @@ let to_edit_id = function | _ -> raise Marshal_error let of_state_id id = - try Stateid.of_state_id id with Invalid_argument _ -> raise Marshal_error + try Stateid.to_xml id with Invalid_argument _ -> raise Marshal_error let to_state_id xml = - try Stateid.to_state_id xml with Invalid_argument _ -> raise Marshal_error + try Stateid.of_xml xml with Invalid_argument _ -> raise Marshal_error let of_edit_or_state_id = function | Interface.Edit id -> ["object","edit"], of_edit_id id @@ -727,7 +727,7 @@ let pr_call = function let raw = if r then "RAW" else "" in let verb = if b then "" else "SILENT" in "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]" - | Backto i -> "BACKTO "^(Stateid.string_of_state_id i) + | Backto i -> "BACKTO "^(Stateid.to_string i) | Goal _ -> "GOALS" | Evars _ -> "EVARS" | Hints _ -> "HINTS" @@ -744,9 +744,9 @@ let pr_call = function | Init _ -> "INIT" let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.string_of_state_id id^" ["^str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]" | Fail (id,Some(i,j),str) -> - "FAIL "^Stateid.string_of_state_id id^ + "FAIL "^Stateid.to_string id^ " ("^string_of_int i^","^string_of_int j^")["^str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value call value = diff --git a/lib/stateid.ml b/lib/stateid.ml index 3abd80cfb..1eac4bf3f 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -8,18 +8,18 @@ open Xml_datatype -type state_id = int -let initial_state_id = 1 -let dummy_state_id = 0 -let fresh_state_id, in_range = - let cur = ref initial_state_id in +type t = int +let initial = 1 +let dummy = 0 +let fresh, in_range = + let cur = ref initial in (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) -let string_of_state_id = string_of_int -let state_id_of_int id = assert(in_range id); id -let int_of_state_id id = id +let to_string = string_of_int +let of_int id = assert(in_range id); id +let to_int id = id let newer_than id1 id2 = id1 > id2 -let to_state_id = function +let of_xml = function | Element ("state_id",["val",i],[]) -> let id = int_of_string i in (* Coqide too to parse ids too, but cannot check if they are valid. @@ -27,11 +27,12 @@ let to_state_id = function if !Flags.ide_slave then assert(in_range id); id | _ -> raise (Invalid_argument "to_state_id") -let of_state_id i = Element ("state_id",["val",string_of_int i],[]) +let to_xml i = Element ("state_id",["val",string_of_int i],[]) -let state_id_info : (state_id * state_id) Exninfo.t = Exninfo.make () -let add_state_id exn ?(valid = initial_state_id) id = +let state_id_info : (t * t) Exninfo.t = Exninfo.make () +let add exn ?(valid = initial) id = Exninfo.add exn state_id_info (valid, id) -let get_state_id exn = Exninfo.get exn state_id_info +let get exn = Exninfo.get exn state_id_info -module StateidOrderedType = struct type t = state_id let compare = compare end +let equal = Int.equal +let compare = Int.compare diff --git a/lib/stateid.mli b/lib/stateid.mli index 978f12691..27b083efd 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -8,24 +8,26 @@ open Xml_datatype -type state_id -val initial_state_id : state_id -val dummy_state_id : state_id -val fresh_state_id : unit -> state_id -val string_of_state_id : state_id -> string -val state_id_of_int : int -> state_id -val int_of_state_id : state_id -> int -val newer_than : state_id -> state_id -> bool +type t + +val equal : t -> t -> bool +val compare : t -> t -> int + +val initial : t +val dummy : t +val fresh : unit -> t +val to_string : t -> string +val of_int : int -> t +val to_int : t -> int +val newer_than : t -> t -> bool (* XML marshalling *) -val of_state_id : state_id -> xml -val to_state_id : xml -> state_id +val to_xml : t -> xml +val of_xml : xml -> t (* Attaches to an exception the concerned state id, plus an optional * state id that is a valid state id before the error. * Backtracking to the valid id is safe. * The initial_state_id is assumed to be safe. *) -val add_state_id : exn -> ?valid:state_id -> state_id -> exn -val get_state_id : exn -> (state_id * state_id) option - -module StateidOrderedType : Map.OrderedType with type t = state_id +val add : exn -> ?valid:t -> t -> exn +val get : exn -> (t * t) option |