Skip to content

Commit 8204148

Browse files
strubstrub
committed
uni -> tyuni/tcuni
1 parent 6eddaa5 commit 8204148

File tree

14 files changed

+190
-110
lines changed

14 files changed

+190
-110
lines changed

‎src/ecAst.ml‎

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ open EcUtils
33
open EcSymbols
44
open EcIdent
55
open EcPath
6-
open EcUid
76

87
module BI = EcBigInt
98

@@ -41,6 +40,13 @@ type 'a use_restr = {
4140
type mr_xpaths = EcPath.Sx.t use_restr
4241
type mr_mpaths = EcPath.Sm.t use_restr
4342

43+
(* -------------------------------------------------------------------- *)
44+
module TyUni = EcUid.CoreGen ()
45+
module TcUni = EcUid.CoreGen ()
46+
47+
type tyuni = TyUni.uid
48+
type tcuni = TcUni.uid
49+
4450
(* -------------------------------------------------------------------- *)
4551
type ty = {
4652
ty_node : ty_node;
@@ -50,7 +56,7 @@ type ty = {
5056

5157
and ty_node =
5258
| Tglob of EcIdent.t (* The tuple of global variable of the module *)
53-
| Tunivar of EcUid.uid
59+
| Tunivar of tyuni
5460
| Tvar of EcIdent.t
5561
| Ttuple of ty list
5662
| Tconstr of EcPath.path * etyarg list
@@ -60,7 +66,7 @@ and ty_node =
6066
and etyarg = ty * tcwitness list
6167

6268
and tcwitness =
63-
| TCIUni of EcUid.uid
69+
| TCIUni of tcuni
6470

6571
| TCIConcrete of {
6672
path: EcPath.path;
@@ -403,7 +409,7 @@ let etyargs_fv (tyargs : etyarg list) =
403409
let rec tcw_equal (tcw1 : tcwitness) (tcw2 : tcwitness) =
404410
match tcw1, tcw2 with
405411
| TCIUni uid1, TCIUni uid2 ->
406-
uid_equal uid1 uid2
412+
TcUni.uid_equal uid1 uid2
407413

408414
| TCIConcrete tcw1, TCIConcrete tcw2 ->
409415
EcPath.p_equal tcw1.path tcw2.path
@@ -866,7 +872,7 @@ module Hsty = Why3.Hashcons.Make (struct
866872
EcIdent.id_equal m1 m2
867873

868874
| Tunivar u1, Tunivar u2 ->
869-
uid_equal u1 u2
875+
TyUni.uid_equal u1 u2
870876

871877
| Tvar v1, Tvar v2 ->
872878
id_equal v1 v2
@@ -885,7 +891,7 @@ module Hsty = Why3.Hashcons.Make (struct
885891
let hash ty =
886892
match ty.ty_node with
887893
| Tglob m -> EcIdent.id_hash m
888-
| Tunivar u -> u
894+
| Tunivar u -> Hashtbl.hash u
889895
| Tvar id -> EcIdent.tag id
890896
| Ttuple tl -> Why3.Hashcons.combine_list ty_hash 0 tl
891897
| Tconstr (p, tl) -> Why3.Hashcons.combine_list etyarg_hash p.p_tag tl

‎src/ecAst.mli‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,13 @@ type mr_xpaths = EcPath.Sx.t use_restr
3737

3838
type mr_mpaths = EcPath.Sm.t use_restr
3939

40+
(* -------------------------------------------------------------------- *)
41+
module TyUni : EcUid.ICore with type uid = private EcUid.uid
42+
module TcUni : EcUid.ICore with type uid = private EcUid.uid
43+
44+
type tyuni = TyUni.uid
45+
type tcuni = TcUni.uid
46+
4047
(* -------------------------------------------------------------------- *)
4148
type ty = private {
4249
ty_node : ty_node;
@@ -46,7 +53,7 @@ type ty = private {
4653

4754
and ty_node =
4855
| Tglob of EcIdent.t (* The tuple of global variable of the module *)
49-
| Tunivar of EcUid.uid
56+
| Tunivar of tyuni
5057
| Tvar of EcIdent.t
5158
| Ttuple of ty list
5259
| Tconstr of EcPath.path * etyarg list
@@ -56,7 +63,7 @@ and ty_node =
5663
and etyarg = ty * tcwitness list
5764

5865
and tcwitness =
59-
| TCIUni of EcUid.uid
66+
| TCIUni of tcuni
6067

6168
| TCIConcrete of {
6269
path: EcPath.path;

‎src/ecCoreEqTest.ml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,8 @@ let rec for_type env t1 t2 =
2121
(* -------------------------------------------------------------------- *)
2222
and for_type_r env t1 t2 =
2323
match t1.ty_node, t2.ty_node with
24-
| Tunivar uid1, Tunivar uid2 -> EcUid.uid_equal uid1 uid2
24+
| Tunivar uid1, Tunivar uid2 ->
25+
EcAst.TyUni.uid_equal uid1 uid2
2526

2627
| Tvar i1, Tvar i2 -> i1 = i2
2728

@@ -63,7 +64,7 @@ and for_etyargs env (tyargs1 : etyarg list) (tyargs2 : etyarg list) =
6364
and for_tcw env (tcw1 : tcwitness) (tcw2 : tcwitness) =
6465
match tcw1, tcw2 with
6566
| TCIUni uid1, TCIUni uid2 ->
66-
EcUid.uid_equal uid1 uid2
67+
EcAst.TcUni.uid_equal uid1 uid2
6768

6869
| TCIConcrete tcw1, TCIConcrete tcw2 ->
6970
EcPath.p_equal tcw1.path tcw2.path

‎src/ecCorePrinting.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,8 @@ module type PrinterAPI = sig
5959
val pp_mem : PPEnv.t -> EcIdent.t pp
6060
val pp_memtype : PPEnv.t -> EcMemory.memtype pp
6161
val pp_tyvar : PPEnv.t -> ident pp
62-
val pp_tyunivar : PPEnv.t -> EcUid.uid pp
62+
val pp_tyunivar : PPEnv.t -> EcAst.tyuni pp
63+
val pp_tcunivar : PPEnv.t -> EcAst.tcuni pp
6364
val pp_path : path pp
6465

6566
(* ------------------------------------------------------------------ *)

‎src/ecCoreSubst.ml‎

Lines changed: 23 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ type mod_extra = {
1717
(* -------------------------------------------------------------------- *)
1818
type f_subst = {
1919
fs_freshen : bool; (* true means freshen locals *)
20-
fs_u : ty Muid.t;
21-
fs_utc : tcwitness Muid.t;
20+
fs_u : ty TyUni.Muid.t;
21+
fs_utc : tcwitness TcUni.Muid.t;
2222
fs_v : etyarg Mid.t;
2323
fs_mod : EcPath.mpath Mid.t;
2424
fs_modex : mod_extra Mid.t;
@@ -50,13 +50,14 @@ let fv_Mid (type a)
5050

5151
(* -------------------------------------------------------------------- *)
5252
type unisubst = {
53-
uvars : ty Muid.t;
54-
utcvars : tcwitness Muid.t;
53+
uvars : ty TyUni.Muid.t;
54+
utcvars : tcwitness TcUni.Muid.t;
5555
}
5656

5757
(* -------------------------------------------------------------------- *)
5858
let unisubst0 : unisubst = {
59-
uvars = Muid.empty; utcvars = Muid.empty;
59+
uvars = TyUni.Muid.empty;
60+
utcvars = TcUni.Muid.empty;
6061
}
6162

6263
(* -------------------------------------------------------------------- *)
@@ -69,8 +70,8 @@ let f_subst_init
6970
=
7071

7172
let fv = Mid.empty in
72-
let fv = Muid.fold (fun _ t s -> fv_union s (ty_fv t)) tu.uvars fv in
73-
let fv = Muid.fold (fun _ t s -> fv_union s (tcw_fv t)) tu.utcvars fv in
73+
let fv = TyUni.Muid.fold (fun _ t s -> fv_union s (ty_fv t)) tu.uvars fv in
74+
let fv = TcUni.Muid.fold (fun _ t s -> fv_union s (tcw_fv t)) tu.utcvars fv in
7475
let fv = fv_Mid etyarg_fv tv fv in
7576
let fv = fv_Mid e_fv esloc fv in
7677

@@ -168,7 +169,8 @@ let f_rem_mod (s : f_subst) (x : ident) : f_subst =
168169
(* -------------------------------------------------------------------- *)
169170
let is_ty_subst_id (s : f_subst) : bool =
170171
Mid.is_empty s.fs_mod
171-
&& Muid.is_empty s.fs_u
172+
&& TyUni.Muid.is_empty s.fs_u
173+
&& TcUni.Muid.is_empty s.fs_utc
172174
&& Mid.is_empty s.fs_v
173175

174176
(* -------------------------------------------------------------------- *)
@@ -180,7 +182,7 @@ let rec ty_subst (s : f_subst) (ty : ty) : ty =
180182
|> Option.value ~default:ty
181183

182184
| Tunivar id ->
183-
Muid.find_opt id s.fs_u
185+
TyUni.Muid.find_opt id s.fs_u
184186
|> Option.map (ty_subst s)
185187
|> Option.value ~default:ty
186188

@@ -206,7 +208,7 @@ let rec ty_subst (s : f_subst) (ty : ty) : ty =
206208
and tcw_subst (s : f_subst) (tcw : tcwitness) : tcwitness =
207209
match tcw with
208210
| TCIUni uid ->
209-
Muid.find_opt uid s.fs_utc
211+
TcUni.Muid.find_opt uid s.fs_utc
210212
|> Option.value ~default:tcw
211213

212214
| TCIConcrete ({ etyargs = etyargs0 } as rtcw) ->
@@ -785,34 +787,34 @@ module Tuni = struct
785787
let subst (uidmap : unisubst) : f_subst =
786788
f_subst_init ~tu:uidmap ()
787789
788-
let subst1 ((id, t) : uid * ty) : f_subst =
789-
subst { unisubst0 with uvars = Muid.singleton id t }
790+
let subst1 ((id, t) : tyuni * ty) : f_subst =
791+
subst { unisubst0 with uvars = TyUni.Muid.singleton id t }
790792
791793
let subst_dom (uidmap : unisubst) (dom : dom) : dom =
792794
List.map (ty_subst (subst uidmap)) dom
793795
794-
let occurs (u : uid) : ty -> bool =
796+
let occurs (u : tyuni) : ty -> bool =
795797
let rec aux t =
796798
match t.ty_node with
797-
| Tunivar u' -> uid_equal u u'
799+
| Tunivar u' -> TyUni.uid_equal u u'
798800
| _ -> ty_sub_exists aux t in
799801
aux
800802
801-
let univars : ty -> Suid.t =
803+
let univars : ty -> TyUni.Suid.t =
802804
let rec doit univars t =
803805
match t.ty_node with
804-
| Tunivar uid -> Suid.add uid univars
806+
| Tunivar uid -> TyUni.Suid.add uid univars
805807
| _ -> ty_fold doit univars t
806808
807-
in fun t -> doit Suid.empty t
809+
in fun t -> doit TyUni.Suid.empty t
808810
809-
let rec fv_rec (fv : Suid.t) (t : ty) : Suid.t =
811+
let rec fv_rec (fv : TyUni.Suid.t) (t : ty) : TyUni.Suid.t =
810812
match t.ty_node with
811-
| Tunivar id -> Suid.add id fv
813+
| Tunivar id -> TyUni.Suid.add id fv
812814
| _ -> ty_fold fv_rec fv t
813815
814-
let fv (ty : ty) : Suid.t =
815-
fv_rec Suid.empty ty
816+
let fv (ty : ty) : TyUni.Suid.t =
817+
fv_rec TyUni.Suid.empty ty
816818
end
817819
818820
(* -------------------------------------------------------------------- *)

‎src/ecCoreSubst.mli‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
(* -------------------------------------------------------------------- *)
2-
open EcUid
32
open EcIdent
43
open EcPath
54
open EcAst
@@ -18,7 +17,8 @@ type 'a subst_binder = f_subst -> 'a -> f_subst * 'a
1817

1918
(* -------------------------------------------------------------------- *)
2019
type unisubst = {
21-
uvars : ty Muid.t; utcvars : tcwitness Muid.t;
20+
uvars : ty TyUni.Muid.t;
21+
utcvars : tcwitness TcUni.Muid.t;
2222
}
2323

2424
(* -------------------------------------------------------------------- *)
@@ -32,12 +32,12 @@ val f_subst_init :
3232

3333
(* -------------------------------------------------------------------- *)
3434
module Tuni : sig
35-
val univars : ty -> Suid.t
36-
val subst1 : (uid * ty) -> f_subst
35+
val univars : ty -> TyUni.Suid.t
36+
val subst1 : (tyuni * ty) -> f_subst
3737
val subst : unisubst -> f_subst
3838
val subst_dom : unisubst -> dom -> dom
39-
val occurs : uid -> ty -> bool
40-
val fv : ty -> Suid.t
39+
val occurs : tyuni -> ty -> bool
40+
val fv : ty -> TyUni.Suid.t
4141
end
4242

4343
(* -------------------------------------------------------------------- *)

‎src/ecPrinting.ml‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -335,7 +335,7 @@ module PPEnv = struct
335335

336336
exception FoundUnivarSym of symbol
337337

338-
let tyunivar (ppe : t) i =
338+
let univar (ppe : t) (i : EcUid.uid) =
339339
if not (Mint.mem i (fst !(ppe.ppe_univar))) then begin
340340
let alpha = "abcdefghijklmnopqrstuvwxyz" in
341341

@@ -469,8 +469,12 @@ let pp_tyvar ppe fmt x =
469469
Format.fprintf fmt "%s" (PPEnv.tyvar ppe x)
470470

471471
(* -------------------------------------------------------------------- *)
472-
let pp_tyunivar ppe fmt x =
473-
Format.fprintf fmt "%s" (PPEnv.tyunivar ppe x)
472+
let pp_tyunivar (ppe : PPEnv.t) (fmt : Format.formatter) (a : tyuni) =
473+
Format.fprintf fmt "%s" (PPEnv.univar ppe (a :> EcUid.uid))
474+
475+
(* -------------------------------------------------------------------- *)
476+
let pp_tcunivar (ppe : PPEnv.t) (fmt : Format.formatter) (a : tcuni) =
477+
Format.fprintf fmt "%s" (PPEnv.univar ppe (a :> EcUid.uid))
474478

475479
(* -------------------------------------------------------------------- *)
476480
let pp_tyname ppe fmt p =
@@ -959,7 +963,7 @@ and pp_etyargs (ppe : PPEnv.t) (fmt : Format.formatter) (etys : etyarg list) =
959963
and pp_tcw (ppe : PPEnv.t) (fmt : Format.formatter) (tcw : tcwitness) =
960964
match tcw with
961965
| TCIUni uid ->
962-
Format.fprintf fmt "%a" (pp_tyunivar ppe) uid
966+
Format.fprintf fmt "%a" (pp_tcunivar ppe) uid
963967

964968
| TCIConcrete { path; etyargs } ->
965969
Format.fprintf fmt "%a[%a]"

‎src/ecTypes.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ let rec dump_ty ty =
4242
EcIdent.tostring p
4343

4444
| Tunivar i ->
45-
Printf.sprintf "#%d" i
45+
Printf.sprintf "#%d" (i :> int)
4646

4747
| Tvar id ->
4848
EcIdent.tostring id

‎src/ecTypes.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ val dump_ty : ty -> string
2929
val ty_equal : ty -> ty -> bool
3030
val ty_hash : ty -> int
3131

32-
val tuni : EcUid.uid -> ty
32+
val tuni : tyuni -> ty
3333
val tvar : EcIdent.t -> ty
3434
val ttuple : ty list -> ty
3535
val tconstr : EcPath.path -> ty list -> ty

‎src/ecTyping.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2346,7 +2346,7 @@ and fundef_add_symbol env (memenv : memenv) xtys : memenv =
23462346

23472347
and fundef_check_type subst_uni env os (ty, loc) =
23482348
let ty = subst_uni ty in
2349-
if not (EcUid.Suid.is_empty (Tuni.fv ty)) then
2349+
if not (TyUni.Suid.is_empty (Tuni.fv ty)) then
23502350
tyerror loc env (OnlyMonoTypeAllowed os);
23512351
ty
23522352

0 commit comments

Comments
 (0)