Commit 70750212 authored by Andrei Paskevich's avatar Andrei Paskevich

open up the Ident.preid type

parent d24283f3
......@@ -190,16 +190,14 @@ let dty_of_dterm dt = match dt.dt_dty with
let denv_empty = Mstr.empty
let denv_add_var denv id dty =
let n = preid_name id in
let denv_add_var denv {pre_name = n} dty =
Mstr.add n (DTvar (n, dty)) denv
let denv_add_let denv dt id =
let n = preid_name id in
let denv_add_let denv dt {pre_name = n} =
Mstr.add n (DTvar (n, dty_of_dterm dt)) denv
let denv_add_quant denv vl =
let add acc (id,dty) = let n = preid_name id in
let add acc ({pre_name = n}, dty) =
Mstr.add_new (DuplicateVar n) n (DTvar (n, dty)) acc in
let s = List.fold_left add Mstr.empty vl in
Mstr.set_union s denv
......@@ -244,9 +242,9 @@ let dpattern ?loc node =
let get_dty = function
| DPwild ->
dty_fresh (), Mstr.empty
| DPvar id ->
| DPvar {pre_name = n} ->
let dty = dty_fresh () in
dty, Mstr.singleton (preid_name id) dty
dty, Mstr.singleton n dty
| DPapp (ls,dpl) ->
let dtyl, dty = specialize_cs ls in
dty_unify_app ls dpat_expected_type dpl dtyl;
......@@ -260,8 +258,7 @@ let dpattern ?loc node =
"Variable %s has type %a,@ but is expected to have type %a"
n print_dty dty1 print_dty dty2 in
dp1.dp_dty, Mstr.union join dp1.dp_vars dp2.dp_vars
| DPas (dp,id) ->
let n = preid_name id in
| DPas (dp, {pre_name = n}) ->
dp.dp_dty, Mstr.add_new (DuplicateVar n) n dp.dp_dty dp.dp_vars in
let dty, vars = Loc.try1 ?loc get_dty node in
{ dp_node = node; dp_dty = dty; dp_vars = vars; dp_loc = loc }
......@@ -330,8 +327,7 @@ let dterm ?loc node =
let pattern ~strict env dp =
let acc = ref Mstr.empty in
let find_var id ty =
let n = preid_name id in
let find_var ({pre_name = n} as id) ty =
try Mstr.find n !acc with Not_found ->
let vs = create_vsymbol id ty in
acc := Mstr.add n vs !acc; vs in
......@@ -353,8 +349,7 @@ let pattern ~strict env dp =
Mstr.set_union !acc env, pat
let quant_vars ~strict env vl =
let add acc (id,dty) =
let n = preid_name id in
let add acc ({pre_name = n} as id, dty) =
let ty = ty_of_dty ~strict dty in
let vs = create_vsymbol id ty in
Mstr.add_new (DuplicateVar n) n vs acc, vs in
......@@ -419,7 +414,7 @@ let term ~strict ~keep_loc env prop dt =
let prop = prop || dty = None in
let t = get uloc env false dt in
let v = create_vsymbol id (t_type t) in
let env = Mstr.add (preid_name id) v env in
let env = Mstr.add id.pre_name v env in
let f = get uloc env prop df in
check_used_var f.t_vars v;
t_let_close v t f
......@@ -437,7 +432,7 @@ let term ~strict ~keep_loc env prop dt =
t_case (get uloc env false dt) (List.map branch bl)
| DTeps (id,dty,df) ->
let v = create_vsymbol id (ty_of_dty ~strict dty) in
let env = Mstr.add (preid_name id) v env in
let env = Mstr.add id.pre_name v env in
let f = get uloc env true df in
check_used_var f.t_vars v;
t_eps_close v f
......
......@@ -61,7 +61,11 @@ module Mid = Id.M
module Hid = Id.H
module Wid = Id.W
type preid = ident
type preid = {
pre_name : string;
pre_label : Slab.t;
pre_loc : Loc.position option;
}
let id_equal : ident -> ident -> bool = (==)
......@@ -69,14 +73,17 @@ let id_hash id = Weakhtbl.tag_hash id.id_tag
(* constructors *)
let id_register = let r = ref 0 in fun id ->
{ id with id_tag = (incr r; Weakhtbl.create_tag !r) }
let id_register = let r = ref 0 in fun id -> {
id_string = id.pre_name;
id_label = id.pre_label;
id_loc = id.pre_loc;
id_tag = (incr r; Weakhtbl.create_tag !r);
}
let create_ident name labels loc = {
id_string = name;
id_label = labels;
id_loc = loc;
id_tag = Weakhtbl.dummy_tag;
pre_name = name;
pre_label = labels;
pre_loc = loc;
}
let id_fresh ?(label = Slab.empty) ?loc nm =
......@@ -93,7 +100,7 @@ let id_derive ?(label = Slab.empty) nm id =
let ll = Slab.union label id.id_label in
create_ident nm ll id.id_loc
let preid_name id = id.id_string
let preid_name id = id.pre_name
(** Unique names for pretty printing *)
......
......@@ -47,7 +47,11 @@ val id_equal : ident -> ident -> bool
val id_hash : ident -> int
(* a user-created type of unregistered identifiers *)
type preid
type preid = {
pre_name : string;
pre_label : Slab.t;
pre_loc : Loc.position option;
}
(* register a pre-ident (you should never use this function) *)
val id_register : preid -> ident
......@@ -64,7 +68,7 @@ val id_clone : ?label:Slab.t -> ident -> preid
(* create a derived pre-ident (inherit labels and location) *)
val id_derive : ?label:Slab.t -> string -> ident -> preid
(* retrieve preid name without registering *)
(* DEPRECATED : retrieve preid name without registering *)
val preid_name : preid -> string
(** Unique persistent names for pretty printing *)
......
......@@ -106,7 +106,7 @@ let create_data_decl tdl =
(* build the projections, if any *)
let build_proj fd id =
try
let pj = Hstr.find projections (preid_name id) in
let pj = Hstr.find projections id.pre_name in
ity_equal_check pj.pl_value.fd_ity fd.fd_ity;
begin match pj.pl_value.fd_mut, fd.fd_mut with
| None, None -> ()
......@@ -119,7 +119,7 @@ let create_data_decl tdl =
with Not_found ->
let pj = create_plsymbol ~hidden id [res] fd in
news := news_id !news pj.pl_ls.ls_name;
Hstr.add projections (preid_name id) pj;
Hstr.add projections id.pre_name pj;
pj
in
cs, List.map (fun (id,fd) -> Opt.map (build_proj fd) id) al
......
......@@ -460,17 +460,17 @@ let free_user_vars frozen (argl,res) =
List.fold_left add (add Stv.empty res) argl
let denv_add_mono { frozen = frozen; locals = locals } id dvty =
let locals = Mstr.add (preid_name id) (None, dvty) locals in
let locals = Mstr.add id.pre_name (None, dvty) locals in
{ frozen = freeze_dvty frozen dvty; locals = locals }
let denv_add_poly { frozen = frozen; locals = locals } id dvty =
let ftvs = free_vars frozen dvty in
let locals = Mstr.add (preid_name id) (Some ftvs, dvty) locals in
let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
{ frozen = frozen; locals = locals }
let denv_add_rec { frozen = frozen; locals = locals } id dvty =
let ftvs = free_user_vars frozen dvty in
let locals = Mstr.add (preid_name id) (Some ftvs, dvty) locals in
let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
{ frozen = freeze_dtvs frozen dvty; locals = locals }
let denv_add_val denv (id,_,dtv) =
......@@ -488,7 +488,7 @@ let denv_add_fun denv (id,_,bl,{de_dvty = (argl,res)},_) =
denv_add_poly denv id (argl, res)
let denv_prepare_rec denv l =
let add s (id,_,_) = let n = preid_name id in
let add s ({pre_name = n},_,_) =
Sstr.add_new (Dterm.DuplicateVar n) n s in
let _ = try List.fold_left add Sstr.empty l with
| Dterm.DuplicateVar n -> (* TODO: loc *)
......@@ -502,7 +502,7 @@ let denv_verify_rec { frozen = frozen; locals = locals } id =
let check tv = if is_frozen frozen tv then Loc.errorm (* TODO: loc *)
"This function is expected to be polymorphic in type variable %a"
Pretty.print_tv tv in
match Mstr.find_opt (preid_name id) locals with
match Mstr.find_opt id.pre_name locals with
| Some (Some tvs, _) -> Stv.iter check tvs
| Some (None, _) -> assert false
| None -> assert false
......@@ -510,7 +510,7 @@ let denv_verify_rec { frozen = frozen; locals = locals } id =
let denv_add_args { frozen = frozen; locals = locals } bl =
let l = List.fold_left (fun l (_,_,_,t) -> t::l) frozen bl in
let add s (id,_,_,t) = match id with
| Some id -> let n = preid_name id in
| Some {pre_name = n} ->
Mstr.add_new (Dterm.DuplicateVar n) n (None, ([],t)) s
| None -> s in
let s = List.fold_left add Mstr.empty bl in
......
......@@ -139,15 +139,14 @@ let make_ppattern pp ?(ghost=false) ity =
let hv = Hstr.create 3 in
let gghost = ref false in
let find id ghost ity =
let nm = preid_name id in
try
let pv = Hstr.find hv nm in
let pv = Hstr.find hv id.pre_name in
ity_equal_check ity pv.pv_ity;
if (pv.pv_ghost <> ghost) then invalid_arg "Mlw_expr.make_ppattern";
pv
with Not_found ->
let pv = create_pvsymbol id ~ghost ity in
Hstr.add hv nm pv; pv
Hstr.add hv id.pre_name pv; pv
in
let make_app ls ppl ghost ity =
let patl = List.map (fun pp -> pp.ppat_pattern) ppl in
......
......@@ -163,7 +163,7 @@ type module_uc = {
let empty_module env n p = {
muc_theory = create_theory ~path:p n;
muc_name = Ident.preid_name n;
muc_name = n.Ident.pre_name;
muc_path = p;
muc_decls = [];
muc_prefix = [];
......
......@@ -1769,9 +1769,9 @@ let add_types ~wp uc tdl =
fty, match pj with
| None -> None
| Some id ->
try Hstr.find pjt (preid_name id) with Not_found ->
try Hstr.find pjt id.pre_name with Not_found ->
let pj = Some (create_fsymbol ~opaque id [ty] fty) in
Hstr.replace pjt (preid_name id) pj;
Hstr.replace pjt id.pre_name pj;
pj
in
let mk_constr (id,pjl) =
......
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