Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

Commit a99c3c00 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

labels in idents

parent e41a8a2d
......@@ -30,6 +30,7 @@ let label ?loc s = (s,loc)
type ident = {
id_string : string; (* non-unique name *)
id_origin : origin; (* origin of the ident *)
id_label : label list; (* identifier labels *)
id_tag : Hashweak.tag; (* unique magical tag *)
}
......@@ -58,17 +59,22 @@ let id_hash id = Hashweak.tag_hash id.id_tag
let id_register = let r = ref 0 in fun id ->
{ id with id_tag = (incr r; Hashweak.create_tag !r) }
let create_ident name origin = {
let create_ident name origin labels = {
id_string = name;
id_origin = origin;
id_label = labels;
id_tag = Hashweak.dummy_tag;
}
let id_fresh nm = create_ident nm Fresh
let id_user nm loc = create_ident nm (User loc)
let id_derive nm id = create_ident nm (Derived id)
let id_clone id = create_ident id.id_string (Derived id)
let id_dup id = { id with id_tag = Hashweak.dummy_tag }
let id_fresh ?(labels = []) nm = create_ident nm Fresh labels
let id_user ?(labels = []) nm loc = create_ident nm (User loc) labels
let id_derive ?(labels = []) nm id = create_ident nm (Derived id) labels
let id_clone ?(labels = []) id =
create_ident id.id_string (Derived id) (labels @ id.id_label)
let id_dup ?(labels = []) id =
create_ident id.id_string id.id_origin (labels @ id.id_label)
let rec id_derived_from i1 i2 = id_equal i1 i2 ||
(match i1.id_origin with
......
......@@ -30,6 +30,7 @@ val label : ?loc:Loc.position -> string -> label
type ident = private {
id_string : string; (* non-unique name *)
id_origin : origin; (* origin of the ident *)
id_label : label list; (* identifier labels *)
id_tag : Hashweak.tag; (* unique magical tag *)
}
......@@ -53,19 +54,19 @@ type preid
val id_register : preid -> ident
(* create a fresh pre-ident *)
val id_fresh : string -> preid
val id_fresh : ?labels:(label list) -> string -> preid
(* create a localized pre-ident *)
val id_user : string -> Loc.position -> preid
val id_user : ?labels:(label list) -> string -> Loc.position -> preid
(* create a derived pre-ident *)
val id_derive : string -> ident -> preid
val id_derive : ?labels:(label list) -> string -> ident -> preid
(* create a derived pre-ident with the same name *)
val id_clone : ident -> preid
(* create a derived pre-ident with the same name and labels *)
val id_clone : ?labels:(label list) -> ident -> preid
(* create a duplicate pre-ident *)
val id_dup : ident -> preid
val id_dup : ?labels:(label list) -> ident -> preid
(* id_derived_from i1 i2 <=> i1 is derived from i2 *)
val id_derived_from : ident -> ident -> bool
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment