remove id_origin which had no precise meaning

src/core/ident.ml

@@ -27,17 +27,12 @@ type label = string
 (** Identifiers *)
 
 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 *)
+  id_string : string;               (* non-unique name *)
+  id_label  : label list;           (* identifier labels *)
+  id_loc    : Loc.position option;  (* optional location *)
+  id_tag    : Hashweak.tag;         (* unique magical tag *)
 }
 
-and origin =
-  | User of Loc.position
-  | Derived of ident
-  | Fresh
-
 module Id = WeakStructMake (struct
   type t = ident
   let tag id = id.id_tag
@@ -58,33 +53,24 @@ 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 labels = {
+let create_ident name labels loc = {
   id_string = name;
-  id_origin = origin;
   id_label  = labels;
+  id_loc    = loc;
   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_fresh ?(label = []) ?loc nm =
+  create_ident nm label loc
 
-let id_dup ?(labels = []) id =
-  create_ident id.id_string id.id_origin (labels @ id.id_label)
+let id_user ?(label = []) nm loc =
+  create_ident nm label (Some loc)
 
-let rec id_derived_from i1 i2 = id_equal i1 i2 ||
-  (match i1.id_origin with
-    | Derived i3 -> id_derived_from i3 i2
-    | _ -> false)
+let id_clone ?(label = []) id =
+  create_ident id.id_string (label @ id.id_label) id.id_loc
 
-let rec id_from_user i =
-  match i.id_origin with
-    | Derived i -> id_from_user i
-    | User l -> Some l
-    | Fresh -> None
+let id_derive ?(label = []) nm id =
+  create_ident nm (label @ id.id_label) id.id_loc
 
 (** Unique names for pretty printing *)
 

src/core/ident.mli

@@ -28,17 +28,12 @@ type label = string
 (** {2 Identifiers} *)
 
 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 *)
+  id_string : string;               (* non-unique name *)
+  id_label  : label list;           (* identifier labels *)
+  id_loc    : Loc.position option;  (* optional location *)
+  id_tag    : Hashweak.tag;         (* unique magical tag *)
 }
 
-and origin =
-  | User of Loc.position
-  | Derived of ident
-  | Fresh
-
 module Mid : Map.S with type key = ident
 module Sid : Mid.Set
 module Hid : Hashtbl.S with type key = ident
@@ -50,29 +45,21 @@ val id_hash : ident -> int
 (* a user-created type of unregistered identifiers *)
 type preid
 
-(* register a pre-ident (never use this function) *)
+(* register a pre-ident (you should never use this function) *)
 val id_register : preid -> ident
 
 (* create a fresh pre-ident *)
-val id_fresh : ?labels:(label list) -> string -> preid
+val id_fresh : ?label:(label list) -> ?loc:Loc.position -> string -> preid
 
 (* create a localized pre-ident *)
-val id_user : ?labels:(label list) -> string -> Loc.position -> preid
-
-(* create a derived pre-ident *)
-val id_derive : ?labels:(label list) -> string -> ident -> preid
-
-(* create a derived pre-ident with the same name and labels *)
-val id_clone : ?labels:(label list) -> ident -> preid
+val id_user : ?label:(label list) -> string -> Loc.position -> preid
 
 (* create a duplicate pre-ident *)
-val id_dup : ?labels:(label list) -> ident -> preid
+val id_clone : ?label:(label list) -> ident -> preid
 
-(* id_derived_from i1 i2 <=> i1 is derived from i2 *)
-val id_derived_from : ident -> ident -> bool
+(* create a derived pre-ident (inherit labels and location) *)
+val id_derive : ?label:(label list) -> string -> ident -> preid
 
-(* id_derived_from i1 i2 <=> i1 is derived from i2 *)
-val id_from_user : ident -> Loc.position option
 
 (** Unique persistent names for pretty printing *)
 

src/core/term.ml

@@ -810,7 +810,7 @@ let f_close_quant vl tl f =
 (* open bindings *)
 
 let gen_fresh_vsymbol fnT v =
-  create_vsymbol (id_dup v.vs_name) (fnT v.vs_ty)
+  create_vsymbol (id_clone v.vs_name) (fnT v.vs_ty)
 
 let gen_vs_rename fnT h v =
   let u = gen_fresh_vsymbol fnT v in

src/core/theory.ml

@@ -443,7 +443,7 @@ let rec cl_find_ts cl ts =
   else try Mts.find ts cl.ts_table
   with Not_found ->
     let td' = option_map (cl_trans_ty cl) ts.ts_def in
-    let ts' = create_tysymbol (id_dup ts.ts_name) ts.ts_args td' in
+    let ts' = create_tysymbol (id_clone ts.ts_name) ts.ts_args td' in
     cl.ts_table <- Mts.add ts ts' cl.ts_table;
     ts'
 
@@ -455,7 +455,7 @@ let cl_find_ls cl ls =
   with Not_found ->
     let ta' = List.map (cl_trans_ty cl) ls.ls_args in
     let vt' = option_map (cl_trans_ty cl) ls.ls_value in
-    let ls' = create_lsymbol (id_dup ls.ls_name) ta' vt' in
+    let ls' = create_lsymbol (id_clone ls.ls_name) ta' vt' in
     cl.ls_table <- Mls.add ls ls' cl.ls_table;
     ls'
 
@@ -465,7 +465,7 @@ let cl_find_pr cl pr =
   if not (Sid.mem pr.pr_name cl.cl_local) then pr
   else try Mpr.find pr cl.pr_table
   with Not_found ->
-    let pr' = create_prsymbol (id_dup pr.pr_name) in
+    let pr' = create_prsymbol (id_clone pr.pr_name) in
     cl.pr_table <- Mpr.add pr pr' cl.pr_table;
     pr'
 

src/ide/gmain.ml

@@ -209,9 +209,9 @@ let read_file fn =
   let theories =
     Theory.Mnm.fold
       (fun name th acc ->
-         match th.Theory.th_name.Ident.id_origin with
-           | Ident.User l -> (l,name,th)::acc
-           | _ -> (Loc.dummy_position,name,th)::acc)
+         match th.Theory.th_name.Ident.id_loc with
+           | Some l -> (l,name,th)::acc
+           | None   -> (Loc.dummy_position,name,th)::acc)
       theories []
   in
   let theories = List.sort
@@ -2046,8 +2046,8 @@ let color_loc (v:GSourceView2.source_view) l b e =
   buf#apply_tag ~start ~stop orange_bg
 
 let scroll_to_id id =
-  match id.Ident.id_origin with
-    | Ident.User loc ->
+  match id.Ident.id_loc with
+    | Some loc ->
         let (f,l,b,e) = Loc.get loc in
         if f <> !current_file then
           begin
@@ -2057,13 +2057,9 @@ let scroll_to_id id =
         move_to_line source_view (l-1);
         erase_color_loc source_view;
         color_loc source_view l b e
-    | Ident.Fresh ->
-        source_view#source_buffer#set_text
-          "Fresh ident (no position available)\n";
-        set_current_file ""
-    | Ident.Derived _ ->
+    | None ->
         source_view#source_buffer#set_text
-          "Derived ident (no position available)\n";
+          "Non-localized ident (no position available)\n";
         set_current_file ""
 
 let color_loc loc =

src/ide/session.ml

@@ -658,9 +658,9 @@ let read_file fn =
   let theories =
     Theory.Mnm.fold
       (fun name th acc ->
-         match th.Theory.th_name.Ident.id_origin with
-           | Ident.User l -> (l,name,th)::acc
-           | _ -> (Loc.dummy_position,name,th)::acc)
+         match th.Theory.th_name.Ident.id_loc with
+           | Some l -> (l,name,th)::acc
+           | None   -> (Loc.dummy_position,name,th)::acc)
       theories []
   in
   List.sort

src/parser/denv.ml

@@ -134,8 +134,8 @@ let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
     | Lstr l -> l::ll, p
     | Lpos p -> ll, Some p
   in
-  let labels,p = List.fold_left get_labels ([],None) ll in
-  id_user ~labels x (default_option loc p)
+  let label,p = List.fold_left get_labels ([],None) ll in
+  id_user ~label x (default_option loc p)
 
 let create_user_vs id ty = create_vsymbol (create_user_id id) ty
 
@@ -297,10 +297,8 @@ let specialize_lsymbol ~loc s =
 let ident_of_vs ~loc vs =
   { id     = vs.vs_name.id_string;
     id_lab = List.map (fun l -> Lstr l) vs.vs_name.id_label;
-    id_loc = match vs.vs_name.id_origin with
-      (* FIXME: should we add this loc to id_lab? *)
-      | User loc -> loc
-      | _ -> loc }
+    (* FIXME: should we add this loc to id_lab? *)
+    id_loc = Util.default_option loc vs.vs_name.Ident.id_loc }
 
 let rec specialize_pattern ~loc htv p =
   { dp_node = specialize_pattern_node  ~loc htv p.pat_node;

src/parser/typing.ml

@@ -20,8 +20,8 @@
 open Util
 open Format
 open Pp
-open Ptree
 open Ident
+open Ptree
 open Ty
 open Term
 open Decl
@@ -1025,9 +1025,7 @@ let add_prop k loc s f th =
   try add_prop_decl th k pr (type_fmla (create_denv th) Mstr.empty f)
   with ClashSymbol s -> error ~loc (Clash s)
 
-let loc_of_id id = match id.id_origin with
-  | User loc -> loc
-  | _ -> assert false
+let loc_of_id id = of_option id.Ident.id_loc
 
 let add_inductives dl th =
   (* 1. create all symbols and make an environment with these symbols *)

src/printer/simplify.ml

@@ -166,7 +166,7 @@ let print_decl info fmt d = match d.d_node with
       true
   | Dprop (Pgoal, pr, f) ->
       fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
-      begin match id_from_user pr.pr_name with
+      begin match pr.pr_name.id_loc with
         | None -> ()
         | Some loc -> fprintf fmt " @[;; %a@]@\n"
             Loc.gen_report_position loc

src/printer/smt.ml

@@ -211,7 +211,7 @@ let print_decl info fmt d = match d.d_node with
   | Dprop (Pgoal, pr, f) ->
       fprintf fmt "@[:formula@\n";
       fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
-      (match id_from_user pr.pr_name with
+      (match pr.pr_name.id_loc with
         | None -> ()
         | Some loc -> fprintf fmt " @[;; %a@]@\n"
             Loc.gen_report_position loc);

src/printer/smt2.ml

@@ -282,7 +282,7 @@ let print_decl info fmt d = match d.d_node with
     find_complex_type info fmt f;
       fprintf fmt "@[(assert@\n";
       fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
-      (match id_from_user pr.pr_name with
+      (match pr.pr_name.id_loc with
         | None -> ()
         | Some loc -> fprintf fmt " @[;; %a@]@\n"
             Loc.gen_report_position loc);

src/programs/pgm_typing.ml

@@ -104,14 +104,9 @@ let specialize_post ~loc htv ((v, f), ql) =
   let f = specialize_fmla ~loc htv f in
   (ty, f), List.map specialize_exn ql
 
-let rec loc_of_id id = match id.id_origin with
-  | User loc -> loc
-  | Derived id -> loc_of_id id
-  | _ -> assert false
+let loc_of_id id = Util.of_option id.Ident.id_loc
 
-let loc_of_ls ls = match ls.ls_name.id_origin with
-  | User loc -> Some loc
-  | _ -> None (* FIXME: loc for recursive functions *)
+let loc_of_ls ls = ls.ls_name.Ident.id_loc
 
 let dcurrying tyl ty =
   let make_arrow_type ty1 ty2 = dty_app (ts_arrow, [ty1; ty2]) in
@@ -142,9 +137,7 @@ and specialize_binder ~loc htv v =
     id = v.pv_name.id_string;
     id_lab = List.map (fun l -> Lstr l) v.pv_name.id_label;
     (* FIXME? We do the same here as in Denv.ident_of_vs *)
-    id_loc = match v.pv_name.id_origin with
-      | User loc -> loc
-      | _ -> loc }
+    id_loc = Util.default_option loc v.pv_name.Ident.id_loc }
   in
   let v = specialize_type_v ~loc htv v.pv_tv in
   id, dpurify_type_v v, v

src/programs/pgm_wp.ml

@@ -492,11 +492,8 @@ and f_btop env f = match f.f_node with
 
 let add_wp_decl ps f uc =
   let s = "WP_" ^ ps.p_name.id_string in
-  let labels = ["expl:correctness of " ^ ps.p_name.id_string] in
-  let id = match id_from_user ps.p_name with
-    | None -> id_fresh ~labels s
-    | Some loc -> id_user ~labels s loc
-  in
+  let label = ["expl:correctness of " ^ ps.p_name.id_string] in
+  let id = id_fresh ~label ?loc:ps.p_name.id_loc s in
   let f = f_btop uc f in
   (* printf "wp: f=%a@." print_fmla f; *)
   let pr = create_prsymbol id in

src/transform/encoding_bridge.ml

@@ -112,7 +112,7 @@ let conv_ty tenv ty =
 let conv_vs tenv vs =
   let ty = conv_ty tenv vs.vs_ty in
   if ty_equal ty vs.vs_ty then vs else
-      create_vsymbol (id_dup vs.vs_name) ty
+      create_vsymbol (id_clone vs.vs_name) ty
 
 (* Convert a logic symbols to the encoded one *)
 let conv_ls tenv ls =

src/transform/encoding_sort.ml

@@ -41,7 +41,7 @@ let conv_ts tenv undefined name ty =
     try
       Hty.find tenv.specials ty
     with Not_found ->
-      let ts = create_tysymbol (id_dup name) [] None in
+      let ts = create_tysymbol (id_clone name) [] None in
       Hty.add tenv.specials ty ts;
       ts in
   Hts.replace undefined ts ();
@@ -60,7 +60,7 @@ let conv_ty tenv undefined ty =
 let conv_vs tenv ud vs =
   let ty = conv_ty tenv ud vs.vs_ty in
   if ty_equal ty vs.vs_ty then vs else
-  create_vsymbol (id_dup vs.vs_name) ty
+  create_vsymbol (id_clone vs.vs_name) ty
 
 (* Convert a logic symbol to the encoded one *)
 let conv_ls tenv ud ls =