diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/nameops.ml | 85 | ||||
| -rw-r--r-- | engine/nameops.mli | 34 | ||||
| -rw-r--r-- | engine/proofview.ml | 6 | ||||
| -rw-r--r-- | engine/proofview.mli | 6 |
4 files changed, 127 insertions, 4 deletions
diff --git a/engine/nameops.ml b/engine/nameops.ml index 2047772cfe..31914f9cfa 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -13,6 +13,51 @@ open Names (* Utilities *) +module Subscript = +struct + +type t = { + ss_zero : int; + (** Number of leading zeros of the subscript *) + ss_subs : int; + (** Digital value of the subscript, zero meaning empty *) +} + +let rec overflow n = + Int.equal (n mod 10) 9 && (Int.equal (n / 10) 0 || overflow (n / 10)) + +let zero = { ss_subs = 0; ss_zero = 0 } + +let succ s = + if Int.equal s.ss_subs 0 then + if Int.equal s.ss_zero 0 then + (* [] -> [0] *) + { ss_zero = 1; ss_subs = 0 } + else + (* [0...00] -> [0..01] *) + { ss_zero = s.ss_zero - 1; ss_subs = 1 } + else if overflow s.ss_subs then + if Int.equal s.ss_zero 0 then + (* [9...9] -> [10...0] *) + { ss_zero = 0; ss_subs = 1 + s.ss_subs } + else + (* [0...009...9] -> [0...010...0] *) + { ss_zero = s.ss_zero - 1; ss_subs = 1 + s.ss_subs } + else + (* [0...0n] -> [0...0{n+1}] *) + { ss_zero = s.ss_zero; ss_subs = s.ss_subs + 1 } + +let equal s1 s2 = + Int.equal s1.ss_zero s2.ss_zero && Int.equal s1.ss_subs s2.ss_subs + +let compare s1 s2 = + (* Lexicographic order is reversed in order to ensure that [succ] is strictly + increasing. *) + let c = Int.compare s1.ss_subs s2.ss_subs in + if Int.equal c 0 then Int.compare s1.ss_zero s2.ss_zero else c + +end + let code_of_0 = Char.code '0' let code_of_9 = Char.code '9' @@ -104,6 +149,46 @@ let has_subscript id = let id = Id.to_string id in is_digit (id.[String.length id - 1]) +let get_subscript id = + let id0 = id in + let id = Id.to_string id in + let len = String.length id in + let rec get_suf accu pos = + if pos < 0 then (pos, accu) + else + let c = id.[pos] in + if is_digit c then get_suf (Char.code c - Char.code '0' :: accu) (pos - 1) + else (pos, accu) + in + let (pos, suf) = get_suf [] (len - 1) in + if Int.equal pos (len - 1) then (id0, Subscript.zero) + else + let id = String.sub id 0 (pos + 1) in + let rec compute_zeros accu = function + | [] -> (accu, []) + | 0 :: l -> compute_zeros (succ accu) l + | _ :: _ as l -> (accu, l) + in + let (ss_zero, suf) = compute_zeros 0 suf in + let rec compute_suf accu = function + | [] -> accu + | n :: l -> compute_suf (10 * accu + n) l + in + let ss_subs = compute_suf 0 suf in + (Id.of_string id, { Subscript.ss_subs; ss_zero; }) + +let add_subscript id ss = + if Subscript.equal Subscript.zero ss then id + else if Int.equal ss.Subscript.ss_subs 0 then + let id = Id.to_string id in + let pad = String.make ss.Subscript.ss_zero '0' in + Id.of_string (Printf.sprintf "%s%s" id pad) + else + let id = Id.to_string id in + let pad = String.make ss.Subscript.ss_zero '0' in + let suf = ss.Subscript.ss_subs in + Id.of_string (Printf.sprintf "%s%s%i" id pad suf) + let forget_subscript id = let numstart = cut_ident false id in let newid = Bytes.make (numstart+1) '0' in diff --git a/engine/nameops.mli b/engine/nameops.mli index 0e75fed045..222573450b 100644 --- a/engine/nameops.mli +++ b/engine/nameops.mli @@ -24,8 +24,42 @@ val add_prefix : string -> Id.t -> Id.t (** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *) +module Subscript : +sig + type t + (** Abstract datatype of subscripts. Isomorphic to a string of digits. *) + + val zero : t + (** Empty subscript *) + + val succ : t -> t + (** Guarantees that [x < succ x], but [succ x] might not be the smallest + element strictly above [x], generally it does not exist. Example mappings: + "" ↦ "0" + "0" ↦ "1" + "00" ↦ "01" + "1" ↦ "2" + "01" ↦ "02" + "9" ↦ "10" + "09" ↦ "10" + "99" ↦ "100" + *) + + val compare : t -> t -> int + (** Well-founded order. *) + + val equal : t -> t -> bool + +end + val has_subscript : Id.t -> bool +val get_subscript : Id.t -> Id.t * Subscript.t +(** Split an identifier into a base name and a subscript. *) + +val add_subscript : Id.t -> Subscript.t -> Id.t +(** Append the subscript to the identifier. *) + val increment_subscript : Id.t -> Id.t (** Return the same identifier as the original one but whose {i subscript} is incremented. If the original identifier does not have a suffix, [0] is appended to it. diff --git a/engine/proofview.ml b/engine/proofview.ml index 2d693e0259..316f02bc37 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -899,8 +899,8 @@ module Progress = struct (** Equality function on goals *) let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 (drop_state gl1) in - let evi2 = Evd.find evars2 (drop_state gl2) in + let evi1 = Evd.find evars1 gl1 in + let evi2 = Evd.find evars2 gl2 in eq_evar_info evars1 evars2 evi1 evi2 end @@ -918,7 +918,7 @@ let tclPROGRESS t = let test = quick_test || Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution i final.solution f + Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f) end initial.comb final.comb in if not test then diff --git a/engine/proofview.mli b/engine/proofview.mli index 680a93f0cc..c772525c86 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -395,10 +395,14 @@ val give_up : unit tactic (** {7 Control primitives} *) (** [tclPROGRESS t] checks the state of the proof after [t]. It it is - identical to the state before, then [tclePROGRESS t] fails, otherwise + identical to the state before, then [tclPROGRESS t] fails, otherwise it succeeds like [t]. *) val tclPROGRESS : 'a tactic -> 'a tactic +module Progress : sig + val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool +end + (** Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic |