WIP: first stab at 2nd class modules with type components

samples/ListClient.as

@@ -0,0 +1,7 @@
+let List = import "ListLib.as"; // todo: make local so not re-exported in type!
+
+type Stack = List.List<Int>;
+
+func push(x : Int, s : Stack) : Stack = List.cons<Int>(x, s);
+
+let empty = List.nil<Int>();

samples/ListClient.txt

@@ -0,0 +1,12 @@
+-- Parsing ListClient.as:
+-- Parsing ListLib.as:
+-- Checking ListLib.as:
+-- Checking ListClient.as:
+type Stack = List<Int>
+let List : module {type List<T> = ?(T, List<T>); cons : <T>(T, List<T>) -> List<T>; nil : <T>() -> List<T>}
+let empty : ?(Int, List<Int>)
+let push : (Int, Stack) -> Stack
+-- Interpreting ListLib.as:
+-- Interpreting ListClient.as:
+nil()
+  <= null

samples/ListLib.as

@@ -0,0 +1,3 @@
+type List<T> = ?(T, List<T>);
+func nil<T>() : List<T> = null;
+func cons<T>(x : T, l : List<T>) : List<T> = ?(x, l);

samples/ListLib.txt

@@ -0,0 +1,6 @@
+-- Parsing ListLib.as:
+-- Checking ListLib.as:
+type List<T> = ?(T, List<T>)
+let cons : <T>(T, List<T>) -> List<T>
+let nil : <T>() -> List<T>
+-- Interpreting ListLib.as:

samples/modules.as

@@ -0,0 +1,15 @@
+module Collections = {
+  module List = {
+    type List<T> = ?(T, List<T>);
+    func nil<T>() : List<T> = null;
+    func cons<T>(x : T, l : List<T>) : List<T> = ?(x, l);
+  };
+};
+
+let List = Collections.List;
+
+type Stack = List.List<Int>;
+
+let empty : Stack = List.nil<Int>();
+func push(x : Int, s : Stack) : Stack = List.cons<Int>(x, s);
+

samples/modules.txt

@@ -0,0 +1,11 @@
+-- Parsing modules.as:
+-- Checking modules.as:
+type List<T> = ?(T, List<T>)
+type Stack = List<Int>
+let Collections : module {List : module {type List<T> = ?(T, List<T>); cons : <T>(T, List<T>) -> List<T>; nil : <T>() -> List<T>}}
+let List : module {type List<T> = ?(T, List<T>); cons : <T>(T, List<T>) -> List<T>; nil : <T>() -> List<T>}
+let empty : ?(Int, List<Int>)
+let push : (Int, Stack) -> Stack
+-- Interpreting modules.as:
+nil()
+  <= null

src/arrange.ml

@@ -128,6 +128,7 @@ and control c = match c with
 and obj_sort' s = match s with
   | Type.Object sh -> Atom ("Object " ^ sharing sh)
   | Type.Actor -> Atom "Actor"
+  | Type.Module -> Atom "Module"
 
 and obj_sort s = obj_sort' s.it
 
@@ -153,6 +154,10 @@ and exp_field (ef : exp_field)
 
 and operator_type t = Atom (Type.string_of_typ t)
 
+and path p = match p.it with
+  | IdH i -> "IdH" $$ [id i]
+  | DotH (p,i) -> "DotH" $$ [path p; id i]
+
 and typ t = match t.it with
   | VarT (s, ts)        -> "VarT" $$ [id s] @ List.map typ ts
   | PrimT p             -> "PrimT" $$ [Atom p]
@@ -164,6 +169,7 @@ and typ t = match t.it with
   | FuncT (s, tbs, at, rt) -> "FuncT" $$ [Atom (sharing s.it)] @ List.map typ_bind tbs @ [ typ at; typ rt]
   | AsyncT t            -> "AsyncT" $$ [typ t]
   | ParT t              -> "ParT" $$ [typ t]
+  | PathT (p, i, ts)         -> "PathT" $$ [path p; id i] @ List.map typ ts
 
 and dec d = match d.it with
   | ExpD e -> "ExpD" $$ [exp e ]
@@ -173,5 +179,7 @@ and dec d = match d.it with
     "TypD" $$ [id x] @ List.map typ_bind tp @ [typ t]
   | ClassD (x, tp, s, p, i', efs) ->
     "ClassD" $$ id x :: List.map typ_bind tp @ [obj_sort s; pat p; id i'] @ List.map exp_field efs
+  | ModuleD (i,ds) ->
+    "ModuleD" $$  [id i] @ List.map dec ds
 
 and prog prog = "BlockE"  $$ List.map dec prog.it

src/arrange_type.ml

@@ -17,6 +17,7 @@ let control c = match c with
 let obj_sort s = match s with
   | Type.Object sh -> Atom ("Object " ^ sharing sh)
   | Type.Actor -> Atom "Actor"
+  | Type.Module -> Atom "Module"
 
 let prim p = match p with
   | Null -> Atom "Null"
@@ -50,6 +51,7 @@ let rec typ (t:Type.typ) = match t with
   | Any                   -> Atom "Any"
   | Non                   -> Atom "Non"
   | Pre                   -> Atom "Pre"
+  | Kind (c,k)            -> Atom "Kind ..." (* TBC *)
 
 and typ_bind (tb : Type.bind) =
   tb.var $$ [typ tb.bound]

src/async.ml

@@ -167,6 +167,7 @@ module Transform() = struct
     | Any -> Any
     | Non -> Non
     | Pre -> Pre
+    | Kind (c,k) -> Kind (t_con c, t_kind k)
 
   and t_bind {var; bound} =
     {var; bound = t_typ bound}

src/check_ir.ml

@@ -87,12 +87,11 @@ let add_typs c cs =
 let adjoin c scope =
   { c with
     vals = T.Env.adjoin c.vals scope.val_env;
-    cons = T.ConSet.disjoint_union c.cons scope.con_env;
+    cons = T.ConSet.(*disjoint_*)union c.cons scope.con_env;
   }
 
 let adjoin_vals c ve = {c with vals = T.Env.adjoin c.vals ve}
 
-
 let adjoin_cons c ce =
   { c with
     cons = T.ConSet.disjoint_union c.cons ce;
@@ -178,14 +177,17 @@ let rec check_typ env typ : unit =
     let t' = T.promote typ in
     check_shared env no_region t'
   | T.Obj (sort, fields) ->
-    let rec sorted = function
-      | [] | [_] -> true
+    let rec strictly_sorted fields =
+      match fields with
+      | []
+      | [_] -> true
       | f1::((f2::_) as fields') ->
-        T.compare_field f1 f2  < 0 && sorted fields'
+        T.compare_field f1 f2  < 0 && strictly_sorted fields'
     in
-    check_ids env (List.map (fun (field : T.field) -> field.T.lab) fields);
     List.iter (check_typ_field env sort) fields;
-    check env no_region (sorted fields) "object type's fields are not sorted"
+    (* fields strictly sorted (and) distinct *)
+    if (not (strictly_sorted fields)) then
+      error env no_region "object type's fields are not distinct and sorted %s" (T.string_of_typ typ)
   | T.Variant cts ->
     let rec sorted = function
       | [] | [_] -> true
@@ -202,6 +204,19 @@ let rec check_typ env typ : unit =
       "Serialized in non-serialized flavor";
     check_typ env typ;
     check_sub env no_region typ T.Shared
+  | T.Kind (c,k) ->
+    check_kind env k
+
+and check_kind env k =
+  let (binds,typ) =
+    match k with
+    | T.Abs(binds,typ)
+      | T.Def(binds,typ) -> (binds,typ)
+  in
+  let cs,ce = check_typ_binds env binds in
+  let ts = List.map (fun c -> T.Con(c,[])) cs in
+  let env' = adjoin_cons env ce in
+  check_typ env' (T.open_ ts  typ);
 
 and check_typ_field env s typ_field : unit =
   let T.{lab; typ} = typ_field in
@@ -210,7 +225,7 @@ and check_typ_field env s typ_field : unit =
      (s <> T.Actor || T.is_func (T.promote typ))
     "actor field has non-function type";
   check env no_region
-     (s = T.Object T.Local || T.sub typ T.Shared)
+     (s = T.Object T.Local || s = T.Module || T.sub typ T.Shared)
     "shared object or actor field has non-shared type"
 
 and check_typ_summand env (c, typ) : unit =
@@ -358,10 +373,10 @@ let rec check_exp env (exp:Ir.exp) : unit =
              | ActorDotE _ -> sort = T.Actor
              | DotE _ -> sort <> T.Actor
              | _ -> false) "sort mismatch";
-      match List.find_opt (fun T.{lab; _} -> lab = n) tfs with
-      | Some {T.typ = tn;_} ->
+      match T.lookup_field n tfs with (*CRUSSO: FIX ME*)
+      | tn ->
         tn <~ t
-      | None ->
+      | exception _ ->
         error env exp1.at "field name %s does not exist in type\n  %s"
           n (T.string_of_typ_expand t1)
     end
@@ -539,11 +554,18 @@ let rec check_exp env (exp:Ir.exp) : unit =
     t1 <: t0;
     t0 <: t;
   | NewObjE (s, fs, t0) ->
-    let t1 = type_obj env s fs in
     check (T.is_obj t0) "bad annotation (object type expected)";
+    let is_typ_field {T.lab;T.typ} =
+      match typ with T.Kind _ -> true | _ -> false
+    in
+    let (_s,tfs0) = T.as_obj t0 in
+    let typ_tfs0, val_tfs0 = List.partition is_typ_field tfs0
+    in
+    let t1 = type_obj env s fs in
+    let (_s, tfs1) = T.as_obj t1 in
+    let t1 = T.Obj(s, List.sort T.compare_field (typ_tfs0 @ tfs1)) in
     t1 <: t0;
     t0 <: t
-
 (* Cases *)
 
 and check_cases env t_pat t cases =
@@ -670,7 +692,7 @@ and type_exp_field env s f : T.field =
   check_sub env f.at t f.note;
   check env f.at ((s = T.Actor) ==> T.is_func t)
     "public actor field is not a function";
-  check env f.at ((s <> T.Object T.Local) ==> T.sub t T.Shared)
+  check env f.at ((s <> T.Object T.Local && s <> T.Module) ==> T.sub t T.Shared)
     "public shared object or actor field has non-shared type";
   T.{lab = name; typ = t}
 
@@ -722,9 +744,10 @@ and gather_block_decs env decs =
 
 and gather_dec env scope dec : scope =
   match dec.it with
-  | LetD (pat, _) ->
+  | LetD (pat, exp) ->
     let ve = gather_pat env scope.val_env pat in
-    { scope with val_env = ve}
+    let ce' = gather_typ env scope.con_env exp.note.note_typ in
+    { val_env = ve; con_env = ce'}
   | VarD (id, exp) ->
     check env dec.at
       (not (T.Env.mem id.it scope.val_env))
@@ -738,6 +761,16 @@ and gather_dec env scope dec : scope =
     let ce' = T.ConSet.disjoint_add c scope.con_env in
     { scope with con_env = ce' }
 
+and gather_typ env ce typ =
+   match typ with
+   | T.Obj(T.Module,fs) ->
+     List.fold_right (fun {T.lab;T.typ = typ1} ce ->
+         match typ1 with
+         | T.Kind (c, k) -> T.ConSet.add c ce
+         | _ -> gather_typ env ce typ1
+       ) fs ce
+   | _ -> ce
+
 (* Programs *)
 
 let check_prog scope phase (((ds, exp), flavor) as prog) : unit =

src/compile.ml

@@ -2826,6 +2826,7 @@ module Serialization = struct
         | Obj (_, fs) -> List.for_all (fun f -> go f.typ) fs
         | Mut t -> go t
         | Serialized t -> go t
+        | Kind (_c,_k) -> false
       end
     in go t
 
@@ -4531,8 +4532,8 @@ and compile_exp (env : E.t) exp =
     let prelude_names = find_prelude_names env in
     if Freevars.M.is_empty (Freevars.diff captured prelude_names)
     then actor_lit env i ds fs exp.at
-    else todo_trap env "non-closed actor" (Arrange_ir.exp exp) 
-  | NewObjE (Type.Object _ (*sharing*), fs, _) ->
+    else todo_trap env "non-closed actor" (Arrange_ir.exp exp)
+  | NewObjE ((Type.Object _ (*sharing*) | Type.Module), fs, _) ->
     SR.Vanilla,
     let fs' = fs |> List.map
       (fun (f : Ir.field) -> (f.it.name, fun env ->

src/con.ml

@@ -34,3 +34,4 @@ let to_string c =
 
 let eq c1 c2 = (c1.name, c1.stamp) = (c2.name, c2.stamp)
 let compare c1 c2 = compare (c1.name, c1.stamp) (c2.name, c2.stamp)
+

src/definedness.ml

@@ -155,6 +155,9 @@ and dec msgs d = match d.it with
   | TypD (i, tp, t) -> (M.empty, S.empty)
   | ClassD (i, tp, s, p, i', efs) ->
     (M.empty, S.singleton i.it) +++ delayify (exp_fields msgs efs /// pat msgs p // i'.it)
+  | ModuleD (i, ds) ->
+    (M.empty, S.singleton i.it) +++ decs msgs ds    (* TBR *)
+
 
 and decs msgs decs : f =
   (* Annotate the declarations with the analysis results *)