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

samples/modules.as

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

samples/modules.txt

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

src/arrange.ml

@@ -119,6 +119,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
 
@@ -141,6 +142,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]
@@ -151,6 +156,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 ]
@@ -160,5 +166,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"
@@ -48,6 +49,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

@@ -179,6 +179,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

@@ -81,12 +81,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;
@@ -98,15 +97,6 @@ let disjoint_union env at fmt env1 env2 =
 
 (* Types *)
 
-let check_ids env ids = ignore
-  (List.fold_left
-    (fun dom id ->
-      if List.mem id dom
-      then error env no_region "duplicate field name %s in object type" id
-      else id::dom
-    ) [] ids
-  )
-
 let check env at p =
   if p then ignore
   else error env at
@@ -125,7 +115,7 @@ let rec check_typ env typ : unit =
     error env no_region "free type variable %s, index %i" s  i
   | T.Con (c, typs) ->
     if not (T.ConSet.mem c env.cons) then
-       error env no_region "free type constructor %s" (Con.name c);
+       error env no_region "free type constructor %s" (Con.to_string c);
     (match Con.kind c with | T.Def (tbs, t) | T.Abs (tbs, t)  ->
       check_typ_bounds env tbs typs no_region
     )
@@ -170,18 +160,32 @@ let rec check_typ env typ : unit =
     let t' = T.promote typ in
     check_sub env no_region t' T.Shared
   | T.Obj (sort, fields) ->
-    let rec sorted fields =
+    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.Mut typ ->
     check_typ env typ
+  | 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
@@ -190,7 +194,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"
 
 
@@ -327,10 +331,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
@@ -538,11 +542,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 =
@@ -564,7 +575,7 @@ and gather_pat env ve0 pat : val_env =
     | LitP _ ->
       ve
     | VarP id ->
-      if T.Env.mem id.it ve0 then
+      if T.Env.mem id.it ve then
         error env pat.at "duplicate binding for %s in block" id.it;
       T.Env.add id.it pat.note ve (*TBR*)
     | TupP pats ->
@@ -636,7 +647,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}
 
@@ -688,9 +699,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))
@@ -704,6 +716,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

@@ -3686,7 +3686,7 @@ and compile_exp (env : E.t) exp =
     if Freevars.M.is_empty (Freevars.diff captured prelude_names)
     then actor_lit env i ds fs exp.at
     else todo "non-closed actor" (Arrange_ir.exp exp) G.i Unreachable
-  | NewObjE (Type.Object _ (*sharing*), fs, _) ->
+  | 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

@@ -38,3 +38,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,8 @@ 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 (close (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 *)

src/desugar.ml

@@ -83,19 +83,21 @@ and exp' at note = function
 
 and obj at s self_id es obj_typ =
   match s.it with
-  | Type.Object _ -> build_obj at s self_id es obj_typ
+  | Type.Object _ | T.Module -> build_obj at s self_id es obj_typ
   | Type.Actor -> build_actor at self_id es obj_typ
 
+and build_field {Type.lab; Type.typ} =
+  { it = { I.name = I.Name lab @@ no_region
+         ; I.var = lab @@ no_region
+         }
+  ; at = no_region
+  ; note = typ
+  }
+
 and build_fields obj_typ =
     match obj_typ with
     | Type.Obj (_, fields) ->
-      List.map (fun {Type.lab; Type.typ} ->
-        { it = { I.name = I.Name lab @@ no_region
-               ; I.var = lab @@ no_region
-               }
-        ; at = no_region
-        ; note = typ
-        }) fields
+      List.map build_field fields
     | _ -> assert false
 
 and build_actor at self_id es obj_typ =
@@ -198,6 +200,24 @@ and dec' at n d = match d with
       note = { S.note_typ = fun_typ; S.note_eff = T.Triv }
     } in
     I.LetD (varPat, fn)
+  | S.ModuleD(id, ds) ->
+    (build_module id ds (n.S.note_typ)).it
+
+
+and field_typ_to_obj_entry (f: T.field) =
+  match f.T.typ with
+  | T.Kind _ -> []
+  | _ -> [ build_field f ]
+
+and build_module id ds typ =
+  let self = idE id typ in
+  let (s, fs) = T.as_obj typ in
+  letD self
+    (blockE
+       (decs ds)
+       (newObjE T.Module
+          (List.concat (List.map field_typ_to_obj_entry fs)) typ));
+          (* ^^^^ TBR: do these need to be sorted? *)
 
 and cases cs = List.map case cs
 

src/effect.ml

@@ -101,6 +101,10 @@ and infer_effect_dec dec =
   | TypD _
   | ClassD _ ->
     T.Triv
+  | ModuleD (_,decs) ->
+    let es = List.map effect_dec decs in
+    List.fold_left max_eff Type.Triv es
+
 
 (* effect inference on Ir *)
 

src/env.ml

@@ -32,4 +32,5 @@ struct
   let disjoint_union env1 env2 = union (fun k _ _ -> raise (Clash k)) env1 env2
   let disjoint_unions envs = List.fold_left disjoint_union empty envs
   let disjoint_add k x env = disjoint_union env (singleton k x)
+
 end

src/interpret.ml

@@ -565,6 +565,7 @@ and declare_dec dec : val_env =
   | LetD (pat, _) -> declare_pat pat
   | VarD (id, _) -> declare_id id
   | ClassD (id, _, _, _, _, _) -> declare_id {id with note = ()}
+  | ModuleD (id, _) -> declare_id id
 
 and declare_decs decs ve : val_env =
   match decs with
@@ -601,6 +602,12 @@ and interpret_dec env dec (k : V.value V.cont) =
     let v = V.Func (V.call_conv_of_typ dec.note.note_typ, f) in
     define_id env {id with note = ()} v;
     k v
+  | ModuleD (id, decs) ->
+    let ve = ref V.Env.empty in
+    interpret_block env decs (Some ve) (fun v ->
+        let v = V.Obj (V.Env.map Lib.Promise.value (!ve)) in
+        define_id env id v;
+        k v)
 
 and interpret_decs env decs (k : V.value V.cont) =
   match decs with

src/lexer.mll

@@ -191,6 +191,7 @@ rule token mode = parse
   | "func" { FUNC }
   | "if" { IF }
   | "in" { IN }
+  | "module" { MODULE }
   | "new" { NEW }
   | "not" { NOT }
   | "null" { NULL }