|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
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'
let cut_ident skip_quote s =
let s = Id.to_string s in
let slen = String.length s in
(* [n'] is the position of the first non nullary digit *)
let rec numpart n n' =
if Int.equal n 0 then
(* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
slen
else
let c = Char.code (String.get s (n-1)) in
if Int.equal c code_of_0 && not (Int.equal n slen) then
numpart (n-1) n'
else if code_of_0 <= c && c <= code_of_9 then
numpart (n-1) (n-1)
else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then
numpart (n-1) (n-1)
else
n'
in
numpart slen slen
let repr_ident s =
let numstart = cut_ident false s in
let s = Id.to_string s in
let slen = String.length s in
if Int.equal numstart slen then
(s, None)
else
(String.sub s 0 numstart,
Some (int_of_string (String.sub s numstart (slen - numstart))))
let make_ident sa = function
| Some n ->
let c = Char.code (String.get sa (String.length sa -1)) in
let s =
if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n)
else sa ^ "_" ^ (string_of_int n) in
Id.of_string s
| None -> Id.of_string sa
let root_of_id id =
let suffixstart = cut_ident true id in
Id.of_string (String.sub (Id.to_string id) 0 suffixstart)
(* 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.
Example mappings:
[bar] ↦ [bar0]
[bar0] ↦ [bar1]
[bar00] ↦ [bar01]
[bar1] ↦ [bar2]
[bar01] ↦ [bar02]
[bar9] ↦ [bar10]
[bar09] ↦ [bar10]
[bar99] ↦ [bar100]
*)
let increment_subscript id =
let id = Id.to_string id in
let len = String.length id in
let rec add carrypos =
let c = id.[carrypos] in
if is_digit c then
if Int.equal (Char.code c) (Char.code '9') then begin
assert (carrypos>0);
add (carrypos-1)
end
else begin
let newid = Bytes.of_string id in
Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
Bytes.set newid carrypos (Char.chr (Char.code c + 1));
newid
end
else begin
let newid = Bytes.of_string (id^"0") in
if carrypos < len-1 then begin
Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
Bytes.set newid (carrypos+1) '1'
end;
newid
end
in Id.of_bytes (add (len-1))
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
String.blit (Id.to_string id) 0 newid 0 numstart;
(Id.of_bytes newid)
let add_suffix id s = Id.of_string (Id.to_string id ^ s)
let add_prefix s id = Id.of_string (s ^ Id.to_string id)
let atompart_of_id id = fst (repr_ident id)
(* Names *)
module type ExtName =
sig
include module type of struct include Names.Name end
exception IsAnonymous
val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a
val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
val iter : (Id.t -> unit) -> t -> unit
val map : (Id.t -> Id.t) -> t -> t
val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
val get_id : t -> Id.t
val pick : t -> t -> t
val pick_annot : t Context.binder_annot -> t Context.binder_annot -> t Context.binder_annot
val cons : t -> Id.t list -> Id.t list
val to_option : Name.t -> Id.t option
end
module Name : ExtName =
struct
include Names.Name
exception IsAnonymous
let fold_left f a = function
| Name id -> f a id
| Anonymous -> a
let fold_right f na a =
match na with
| Name id -> f id a
| Anonymous -> a
let iter f na = fold_right (fun x () -> f x) na ()
let map f = function
| Name id -> Name (f id)
| Anonymous -> Anonymous
let fold_left_map f a = function
| Name id -> let (a, id) = f a id in (a, Name id)
| Anonymous -> a, Anonymous
let fold_right_map f na a = match na with
| Name id -> let (id, a) = f id a in (Name id, a)
| Anonymous -> Anonymous, a
let get_id = function
| Name id -> id
| Anonymous -> raise IsAnonymous
let pick na1 na2 =
match na1 with
| Name _ -> na1
| Anonymous -> na2
let pick_annot na1 na2 =
let open Context in
match na1.binder_name with
| Name _ -> na1 | Anonymous -> na2
let cons na l =
match na with
| Anonymous -> l
| Name id -> id::l
let to_option = function
| Anonymous -> None
| Name id -> Some id
end
(* Metavariables *)
let pr_meta = Pp.int
let string_of_meta = string_of_int
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
