diff --git a/src/core/ident.ml b/src/core/ident.ml index e914a4960d4ea0f5f8f5c7e099668fb33998cdb4..910f56dc38814ce9428925f47e8c861400a1bee0 100644 --- a/src/core/ident.ml +++ b/src/core/ident.ml @@ -140,6 +140,9 @@ let id_fresh ?(label = Slab.empty) ?loc nm = let id_user ?(label = Slab.empty) nm loc = create_ident nm label (Some loc) +let id_lab label id = + create_ident id.id_string label id.id_loc + let id_clone ?(label = Slab.empty) id = let ll = Slab.union label id.id_label in create_ident id.id_string ll id.id_loc diff --git a/src/core/ident.mli b/src/core/ident.mli index d51719e669d0dfb8b0f0bd03554dfbd4ea5374ca..e848eaa8ec9d3d1f9bf5ca5ac49285b9122c6e29 100644 --- a/src/core/ident.mli +++ b/src/core/ident.mli @@ -87,6 +87,9 @@ val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid (* create a localized pre-ident *) val id_user : ?label:Slab.t -> string -> Loc.position -> preid +(* create a duplicate pre-ident with given labels *) +val id_lab : Slab.t -> ident -> preid + (* create a duplicate pre-ident *) val id_clone : ?label:Slab.t -> ident -> preid diff --git a/src/transform/eval_match.ml b/src/transform/eval_match.ml index cdc10a77137e2a0fb85c033926964f313c9b15fa..c289cb0eacd724ed749af8d5a3527c5dd74ab694 100644 --- a/src/transform/eval_match.ml +++ b/src/transform/eval_match.ml @@ -77,7 +77,7 @@ let rec add_quant kn (vl,tl,f) v = end in let label = Ident.append_to_model_element_name ~labels:v.vs_name.id_label ~to_append:("." ^ field_name) in - create_vsymbol (id_clone ~label v.vs_name) (ty_inst s ty) in + create_vsymbol (id_lab label v.vs_name) (ty_inst s ty) in let nvl = List.map2 mk_v ls.ls_args pjl in let t = fs_app ls (List.map t_var nvl) ty in