Some Con-related cleanups.

src/arrange_ir.ml

@@ -68,7 +68,7 @@ and dec d = match d.it with
   | FuncD (cc, i, tp, p, t, e) ->
     "FuncD" $$ [call_conv cc; id i] @ List.map typ_bind tp @ [pat p; typ t; exp e]
   | TypD c ->
-    "TypD" $$ [con c; kind (Type.kind c)]
+    "TypD" $$ [con c; kind (Con.kind c)]
 
 and typ_bind (tb : typ_bind) =
   Con.to_string tb.it.con $$ [typ tb.it.bound]

src/async.ml

@@ -8,9 +8,12 @@ open T
 open Construct
 
 (* lower the async type itself
-   - adds a final callback argument to every awaitable shared function, replace the result by unit
-   - transforms types, introductions and eliminations awaitable shared functions only, leaving non-awaitable shared functions unchanged.
-   - ensures every call to an awaitable shared function that takes a tuple has a manifest tuple argument.
+   - adds a final callback argument to every awaitable shared function, replace
+     the result by unit
+   - transforms types, introductions and eliminations awaitable shared
+     functions only, leaving non-awaitable shared functions unchanged.
+   - ensures every call to an awaitable shared function that takes a tuple has
+     a manifest tuple argument.
 
    (for debugging, the `flattening` function can be used to disable argument flattening and use uniform pairing instead)
  *)
@@ -23,12 +26,13 @@ module Transform() = struct
 
   (* the state *)
 
-  (* maps constructors to clones with the same stamp & name,
-     but fresh annotation state (think parallel universe ;->) *)
+  (* maps constructors to new constructors (name name, new stamp, new kind)
+     it is initialized with the type constructors defined outside here, which are
+     not rewritten.
 
-  (* ensures that program fragments from corresponding passes have consistent constructor
-     definitions
-     (note, the actual state of the definition may be duplicated but always should be equivalent
+     If we run this translation on two program fragments (e.g. prelude and program)
+     we would have to pass down the `con_renaming`. But this is simply the right thing
+     to do for a pass that changes the context.
   *)
 
   let con_renaming = ref ConRenaming.empty
@@ -197,9 +201,10 @@ module Transform() = struct
     match  ConRenaming.find_opt c (!con_renaming) with
     | Some c' -> c'
     | None ->
-      let clone = T.clone_con c (T.kind c) in
+      let clone = Con.clone c (Abs ([],Pre)) in
       con_renaming := ConRenaming.add c clone (!con_renaming);
-      T.modify_kind clone t_kind;
+      (* Need to extend con_renaming before traversing the kind *)
+      Type.set_kind clone (t_kind (Con.kind c));
       clone
 
   and t_operator_type ot =
@@ -414,6 +419,12 @@ module Transform() = struct
 
 end
 
-let transform prog =
-  let module T = Transform()
-  in T.t_prog prog
+let transform env prog =
+  let module T = Transform() in
+  (*
+  Initialized the con_renaming with those type constructors already in scope.
+  Eventually, pipeline will allow us to pass the con_renaming to downstream program
+  fragments, then we would simply start with an empty con_renaming and the prelude.
+  *)
+  Type.ConSet.iter (fun c -> T.con_renaming := T.ConRenaming.add c c (!T.con_renaming)) env.Typing.con_env;
+  T.t_prog prog

src/async.mli

@@ -1,3 +1,3 @@
 (* lower uses of async type appropriately *)
 
-val transform : Ir.prog -> Ir.prog
+val transform : Typing.scope -> Ir.prog -> Ir.prog

src/check_ir.ml

@@ -132,7 +132,7 @@ let rec check_typ env typ : unit =
   | T.Con (c,typs) ->
     if not (T.ConSet.mem c env.cons) then
        error env no_region "free type constructor %s" (Con.name c);
-    (match T.kind c with | T.Def (tbs, t) | T.Abs (tbs, t)  ->
+    (match Con.kind c with | T.Def (tbs, t) | T.Abs (tbs, t)  ->
       check_typ_bounds env tbs typs no_region
     )
   | T.Any -> ()
@@ -720,7 +720,7 @@ and check_dec env dec  =
   | TypD c ->
     check (T.ConSet.mem c env.cons) "free type constructor";
     let (binds,typ) =
-      match T.kind c with
+      match Con.kind c with
       | T.Abs(binds,typ)
       | T.Def(binds,typ) -> (binds,typ)
     in

src/con.ml

@@ -1,27 +1,44 @@
-type 'a con = {name : string; stamp : int; kind : 'a}
+(*
+The kind field is a reference to break the recursion in open_binds,
+and to allow the multiple passes in typing. These go through Type.set_kind
+with additional safeguards.
+
+Besides these two use-cases, the kind should not be mutated, and treated like
+immutable data.
+
+This module interface guarantees that constructors with the same stamp have the
+same ref.
+*)
+
+type 'a con = {name : string; stamp : int; kind : 'a ref}
 type 'a t = 'a con
 
 module Stamps = Env.Make(String)
 
 let stamps : int Stamps.t ref = ref Stamps.empty
 
-let fresh name kind =
+let fresh_stamp name =
   let n =
     match Stamps.find_opt name !stamps with
     | Some n -> n
     | None -> 0
   in
   stamps := Stamps.add name (n + 1) !stamps;
-  {name; stamp = n; kind}
+  n
+
+let fresh name k =
+  {name; stamp = fresh_stamp name; kind = ref k}
+let clone c k =
+  { c with stamp = fresh_stamp c.name; kind = ref k } (* Does not change the stamp! *)
 
 let name c = c.name
 
-let kind c = c.kind
+let kind c = !(c.kind)
+let unsafe_set_kind c k = c.kind := k
 
 let to_string c =
   if c.stamp = 0 then c.name else Printf.sprintf "%s/%i" c.name c.stamp
 
 let compare c1 c2 = compare (c1.name, c1.stamp) (c2.name, c2.stamp)
 let eq c1 c2 = (c1.name, c1.stamp) = (c2.name, c2.stamp)
 
-let clone c k = { c with kind = k }

src/con.mli

@@ -3,9 +3,13 @@
 type 'a t
 
 val fresh : string -> 'a -> 'a t
-val kind : 'a t -> 'a
+val clone: 'a t -> 'a -> 'a t
+
 val name : 'a t -> string
 val to_string : 'a t -> string
+
+val kind : 'a t -> 'a
+val unsafe_set_kind : 'a t -> 'a -> unit (* cf. Type.set_kind *)
+
 val eq : 'a t -> 'a t -> bool
 val compare : 'a t -> 'a t -> int
-val clone: 'a t -> 'a -> 'a t

src/pipeline.ml

@@ -17,7 +17,7 @@ let error at cat text =
 
 let print_ce =
   Type.ConSet.iter (fun c ->
-    let eq, params, typ = Type.strings_of_kind (Type.kind c) in
+    let eq, params, typ = Type.strings_of_kind (Con.kind c) in
     printf "type %s%s %s %s\n" (Con.to_string c) params eq typ
   )
 
@@ -121,21 +121,21 @@ let transform_ir transform_name transform flag env prog name =
   if flag then
     begin
       phase transform_name name;
-      let prog' : Ir.prog = transform prog in
+      let prog' : Ir.prog = transform env prog in
       dump_ir Flags.dump_lowering prog';
-      Check_ir.check_prog env transform_name prog;
+      Check_ir.check_prog env transform_name prog';
       prog'
     end
   else prog
 
 let await_lowering =
-  transform_ir "Await Lowering" Await.transform
+  transform_ir "Await Lowering" (fun _ -> Await.transform)
 
 let async_lowering =
   transform_ir "Async Lowering" Async.transform
 
 let tailcall_optimization =
-  transform_ir "Tailcall optimization" Tailcall.transform
+  transform_ir "Tailcall optimization" (fun _ -> Tailcall.transform)
 
 let check_with parse infer senv name : check_result =
   match parse name with

src/type.ml

@@ -36,8 +36,7 @@ and typ =
   | Non                                       (* bottom *)
   | Pre                                       (* pre-type *)
 
-and con_annot = kind ref (* the con annotation is abstract to the outside world *)
-and con = con_annot Con.t
+and con = kind Con.t
 
 and bind = {var : string; bound : typ}
 and field = {name : string; typ : typ}
@@ -48,15 +47,8 @@ and kind =
 
 (* cons *)
 
-(* The con field is a reference to break the recursion in open_binds,
-   and to allow the multiple passes in typing *)
-let kind con = !(Con.kind con)
-
-let fresh_con n k = Con.fresh n (ref k)
-let modify_kind c f = Con.kind c := f !(Con.kind c)
-let clone_con c (k:kind)  = Con.clone c (ref k)
-let set_kind c k = match !(Con.kind c) with
-  | Abs (_, Pre) -> Con.kind c := k
+let set_kind c k = match Con.kind c with
+  | Abs (_, Pre) -> Con.unsafe_set_kind c k
   | _ -> raise (Invalid_argument "set_kind")
 
 (* field ordering *)
@@ -220,10 +212,10 @@ let open_ ts t =
 
 let open_binds tbs =
   if tbs = [] then [] else
-  let cs = List.map (fun {var; _} -> fresh_con var (Abs ([], Pre))) tbs in
+  let cs = List.map (fun {var; _} -> Con.fresh var (Abs ([], Pre))) tbs in
   let ts = List.map (fun con -> Con (con, [])) cs in
   let ks = List.map (fun {bound; _} -> Abs ([], open_ ts bound)) tbs in
-  List.iter2 (fun c k -> Con.kind c := k) cs ks;
+  List.iter2 (fun c k -> set_kind c k) cs ks;
   ts
 
 
@@ -235,7 +227,7 @@ let reduce tbs t ts =
 
 let rec normalize = function
   | Con (con, ts) as t ->
-    (match kind con with
+    (match Con.kind con with
     | Def (tbs, t) -> normalize (reduce tbs t ts)
     | _ -> t
     )
@@ -244,7 +236,7 @@ let rec normalize = function
 
 let rec promote = function
   | Con (con, ts) ->
-    let Def (tbs, t) | Abs (tbs, t) = kind con
+    let Def (tbs, t) | Abs (tbs, t) = Con.kind con
     in promote (reduce tbs t ts)
   | t -> t
 
@@ -362,14 +354,14 @@ let rec avoid' cons = function
   | (Prim _ | Var _ | Any | Non | Shared | Pre) as t -> t
   | Con (c, ts) ->
     if ConSet.mem c cons
-    then match kind c with
+    then match Con.kind c with
       | Abs _ -> raise (Unavoidable c)
       | Def (tbs, t) -> avoid' cons (reduce tbs t ts)
     else
       begin try
         Con (c, List.map (avoid' cons) ts)
       with Unavoidable d ->
-        begin match kind c with
+        begin match Con.kind c with
         | Def (tbs, t) -> avoid' cons (reduce tbs t ts)
         | Abs _ -> raise (Unavoidable d)
         end
@@ -419,7 +411,7 @@ let rec rel_typ rel eq t1 t2 =
   | Non, _ when rel != eq ->
     true
   | Con (con1, ts1), Con (con2, ts2) ->
-    (match kind con1, kind con2 with
+    (match Con.kind con1, Con.kind con2 with
     | Def (tbs, t), _ -> (* TBR this may fail to terminate *)
       rel_typ rel eq (open_ ts1 t) t2
     | _, Def (tbs, t) -> (* TBR this may fail to terminate *)
@@ -432,15 +424,15 @@ let rec rel_typ rel eq t1 t2 =
       false
     )
   | Con (con1, ts1), t2 ->
-    (match kind con1, t2 with
+    (match Con.kind con1, t2 with
     | Def (tbs, t), _ -> (* TBR this may fail to terminate *)
       rel_typ rel eq (open_ ts1 t) t2
     | Abs (tbs, t), _ when rel != eq ->
       rel_typ rel eq (open_ ts1 t) t2
     | _ -> false
     )
   | t1, Con (con2, ts2) ->
-    (match kind con2 with
+    (match Con.kind con2 with
     | Def (tbs, t) -> (* TBR this may fail to terminate *)
       rel_typ rel eq t1 (open_ ts2 t)
     | _ -> false
@@ -712,7 +704,7 @@ let rec string_of_typ_expand t =
   let s = string_of_typ t in
   match t with
   | Con (c, ts) ->
-    (match kind c with
+    (match Con.kind c with
     | Abs _ -> s
     | Def _ ->
       match normalize t with

src/type.mli

@@ -41,18 +41,12 @@ and field = {name : string; typ : typ}
 
 (* cons and kinds *)
 
-and con_annot (* abstract *)
-and con = con_annot Con.t
+and con = kind Con.t
 and kind =
   | Def of bind list * typ
   | Abs of bind list * typ
 
-
-val kind : con -> kind
-val fresh_con : string -> kind -> con
 val set_kind : con -> kind -> unit
-val modify_kind : con -> (kind -> kind) -> unit
-val clone_con : con -> kind -> con
 
 module ConSet :
 sig

src/typing.ml

@@ -136,7 +136,7 @@ and check_typ' env typ : T.typ =
   | VarT (id, typs) ->
     (match T.Env.find_opt id.it env.typs with
     | Some con ->
-      let kind = T.kind con in
+      let kind = Con.kind con in
       let T.Def (tbs, t) | T.Abs (tbs, t) = kind in
       let ts = check_typ_bounds env tbs typs typ.at in
       T.Con (con, ts)
@@ -208,7 +208,7 @@ and check_typ_field env s typ_field : T.field =
 
 and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env =
   let xs = List.map (fun typ_bind -> typ_bind.it.var.it) typ_binds in
-  let cs = List.map (fun n -> T.fresh_con n (T.Abs ([], T.Pre))) xs in
+  let cs = List.map (fun n -> Con.fresh n (T.Abs ([], T.Pre))) xs in
   let te = List.fold_left2 (fun te typ_bind c ->
       let id = typ_bind.it.var in
       if T.Env.mem id.it te then
@@ -1074,11 +1074,11 @@ and gather_dec_typdecs env scope dec : scope =
       error env dec.at "duplicate definition for type %s in block" con_id.it;
     let pre_tbs = List.map (fun bind -> {T.var = bind.it.var.it; bound = T.Pre}) binds in
     let pre_k = T.Abs (pre_tbs, T.Pre) in
-    let c = T.fresh_con con_id.it pre_k in
+    let c = Con.fresh con_id.it pre_k in
     let ve' =
       match dec.it with
       | ClassD (id, _, _ , _, _, _, _) ->
-        let cs = List.map (fun (bind : typ_bind) -> T.fresh_con bind.it.var.it (T.Abs ([], T.Pre))) binds in
+        let cs = List.map (fun (bind : typ_bind) -> Con.fresh bind.it.var.it (T.Abs ([], T.Pre))) binds in
         let t2 = T.Con (c, List.map (fun c' -> T.Con (c', [])) cs) in
         T.Env.add id.it (T.Func (T.Local, T.Returns, pre_tbs, [T.Pre], [t2])) scope.val_env
       | _ -> scope.val_env in
@@ -1103,7 +1103,7 @@ and infer_dec_typdecs firstPass env dec : con_env =
         T.set_kind c k;
         con_id.note <- Some c
       end
-    else assert (T.eq_kind (T.kind c) k)
+    else assert (T.eq_kind (Con.kind c) k)
   in
   match dec.it with
   | ExpD _ | LetD _ | VarD _ | FuncD _ ->

test/run-dfinity/ok/counter-class.wasm.stderr.ok

@@ -63,5 +63,5 @@ non-closed actor: (ActorE
     Const
     Public
   )
-  Counter
+  Counter/1
 )