Introduce IR.FuncE (AST-26)

src/arrange_ir.ml

@@ -40,6 +40,8 @@ let rec exp e = match e.it with
   | PrimE p             -> "PrimE"   $$ [Atom p]
   | DeclareE (i, t, e1) -> "DeclareE" $$ [id i; exp e1]
   | DefineE (i, m, e1)  -> "DefineE" $$ [id i; Arrange.mut m; exp e1]
+  | FuncE (x, cc, tp, p, t, e) ->
+    "FuncE" $$ [Atom x; call_conv cc] @ List.map typ_bind tp @ [pat p; typ t; exp e]
   | NewObjE (s, nameids, t)-> "NewObjE" $$ (Arrange.obj_sort' s ::
                                               List.fold_left (fun flds (n,i) ->
                                                   Atom (name n)::(id i):: flds) [typ t] nameids)
@@ -66,8 +68,6 @@ and dec d = match d.it with
   | ExpD e ->      "ExpD" $$ [exp e ]
   | LetD (p, e) -> "LetD" $$ [pat p; exp e]
   | VarD (i, e) -> "VarD" $$ [id i; exp e]
-  | 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 (Con.kind c)]
 

src/async.ml

@@ -72,8 +72,6 @@ module Transform() = struct
     let fullfill = fresh_var (typ (projE call_new_async 1)) in
     (async,fullfill),call_new_async
 
-  let letP p e = {it = LetD(p, e); at = no_region; note = e.note}
-
   let new_nary_async_reply t1 =
     let (unary_async,unary_fullfill),call_new_async = new_async t1 in
     let v' = fresh_var t1 in
@@ -326,33 +324,17 @@ module Transform() = struct
       DeclareE (id, t_typ typ, t_exp exp1)
     | DefineE (id, mut ,exp1) ->
       DefineE (id, mut, t_exp exp1)
-    | NewObjE (sort, ids, t) ->
-      NewObjE (sort, ids, t_typ t)
-
-  and t_dec dec =
-    { it = t_dec' dec.it;
-      note = { note_typ = t_typ dec.note.note_typ;
-               note_eff = dec.note.note_eff };
-      at = dec.at }
-
-  and t_dec' dec' =
-    match dec' with
-    | ExpD exp -> ExpD (t_exp exp)
-    | TypD con_id ->
-      TypD (t_con con_id)
-    | LetD (pat,exp) -> LetD (t_pat pat,t_exp exp)
-    | VarD (id,exp) -> VarD (id,t_exp exp)
-    | FuncD (cc, id, typbinds, pat, typT, exp) ->
+    | FuncE (x, cc, typbinds, pat, typT, exp) ->
       let s = cc.Value.sort in
       begin
         match s with
         | T.Local  ->
-          FuncD (cc, id, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
+          FuncE (x, cc, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
         | T.Sharable ->
           begin
             match typ exp with
             | T.Tup [] ->
-              FuncD (cc, id, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
+              FuncE (x, cc, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
             | T.Async res_typ ->
               let cc' = Value.message_cc (cc.Value.n_args + 1) in
               let res_typ = t_typ res_typ in
@@ -362,23 +344,39 @@ module Transform() = struct
               let k = fresh_var reply_typ in
               let pat',d = extendTupP pat (varP k) in
               let typbinds' = t_typ_binds typbinds in
-              let x = fresh_var res_typ in
+              let y = fresh_var res_typ in
               let exp' =
                 match exp.it with
                 | CallE(_, async,_,cps) ->
                   begin
                     match async.it with
                     | PrimE("@async") ->
                       blockE
-                        (d [expD ((t_exp cps) -*- (x --> (k -*- x)))])
+                        (d [expD ((t_exp cps) -*- (y --> (k -*- y)))])
                     | _ -> assert false
                   end
                 | _ -> assert false
               in
-              FuncD (cc', id, typbinds', pat', typ', exp')
+              FuncE (x, cc', typbinds', pat', typ', exp')
             | _ -> assert false
           end
       end
+    | NewObjE (sort, ids, t) ->
+      NewObjE (sort, ids, t_typ t)
+
+  and t_dec dec =
+    { it = t_dec' dec.it;
+      note = { note_typ = t_typ dec.note.note_typ;
+               note_eff = dec.note.note_eff };
+      at = dec.at }
+
+  and t_dec' dec' =
+    match dec' with
+    | ExpD exp -> ExpD (t_exp exp)
+    | TypD con_id ->
+      TypD (t_con con_id)
+    | LetD (pat,exp) -> LetD (t_pat pat,t_exp exp)
+    | VarD (id,exp) -> VarD (id,t_exp exp)
 
   and t_decs decs = List.map t_dec decs
 

src/await.ml

@@ -137,6 +137,9 @@ and t_exp' context exp' =
     DeclareE (id, typ, t_exp context exp1)
   | DefineE (id, mut ,exp1) ->
     DefineE (id, mut, t_exp context exp1)
+  | FuncE (x, s, typbinds, pat, typ, exp) ->
+    let context' = LabelEnv.add id_ret Label LabelEnv.empty in
+    FuncE (x, s, typbinds, pat, typ,t_exp context' exp)
   | NewObjE (sort, ids, typ) -> exp'
 
 and t_dec context dec =
@@ -147,9 +150,6 @@ and t_dec' context dec' =
   | TypD _ -> dec'
   | LetD (pat, exp) -> LetD (pat, t_exp context exp)
   | VarD (id, exp) -> VarD (id, t_exp context exp)
-  | FuncD (s, id, typbinds, pat, typ, exp) ->
-    let context' = LabelEnv.add id_ret Label LabelEnv.empty in
-    FuncD (s, id, typbinds, pat, typ,t_exp context' exp)
 
 and t_decs context decs = List.map (t_dec context) decs
 
@@ -317,7 +317,8 @@ and c_exp' context exp k =
     k -@- (t_exp context exp)
   | PrimE _
   | VarE _
-  | LitE _ ->
+  | LitE _
+  | FuncE _ ->
     assert false
   | UnE (ot, op, exp1) ->
     unary context k (fun v1 -> e (UnE (ot, op, v1))) exp1
@@ -460,13 +461,6 @@ and c_dec context dec (k:kont) =
           (meta (typ exp)
              (fun v -> k -@- define_idE id varM v))
     end
-  | FuncD  (_, id, _ (* typbinds *), _ (* pat *), _ (* typ *), _ (* exp *) ) ->
-    let func_typ = typ dec in
-    let v = fresh_var func_typ in
-    let u = fresh_var T.unit in
-    blockE [letD v (decE (t_dec context dec));
-            letD u (define_idE id constM v);
-            expD (k -@- v)]
 
 
 and c_decs context decs k =
@@ -485,7 +479,6 @@ and declare_dec dec exp : exp =
   | TypD _ -> exp
   | LetD (pat, _) -> declare_pat pat exp
   | VarD (id, exp1) -> declare_id id (T.Mut (typ exp1)) exp
-  | FuncD (_, id, _, _, _, _) -> declare_id id (typ dec) exp
 
 and declare_decs decs exp : exp =
   match decs with

src/check_ir.ml

@@ -262,9 +262,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
   (* helpers *)
   let check p = check env exp.at p in
   let (<:) t1 t2 = check_sub env exp.at t1 t2 in
-  let (<~) t1 t2 =
-    (if T.is_mut t2 then t1 else T.as_immut t1) <: t2
-  in
+  let (<~) t1 t2 = (if T.is_mut t2 then t1 else T.as_immut t1) <: t2 in
   (* check effect *)
   check (E.Ir.infer_effect_exp exp <= E.eff exp)
     "inferred effect not a subtype of expected effect";
@@ -387,6 +385,12 @@ let rec check_exp env (exp:Ir.exp) : unit =
     (typ exp2) <: T.open_ insts t2;
     T.open_ insts t3 <: t;
   | BlockE decs ->
+    (* Really, this should be a tuple of decs and an expression now *)
+    check (decs <> []) "BlockE [] is invalid";
+    begin match (Lib.List.last decs).it with
+      | ExpD _ -> ()
+      | _ -> error env exp.at "last entry in a BlockE must be an expression"
+    end;
     let t1, scope = type_block env decs exp.at in
     t1 <: t;
   | IfE (exp1, exp2, exp3) ->
@@ -512,6 +516,29 @@ let rec check_exp env (exp:Ir.exp) : unit =
           typ exp1 <: t0
     end;
     T.unit <: t
+  | FuncE (x, cc, typ_binds, pat, ret_ty, exp) ->
+    let cs,ce = check_open_typ_binds env typ_binds in
+    let arg_ty, ret_ty = match t with
+      | T.Func (cc, _, _, ts1, ts2) ->
+        let ts = List.map (fun c -> T.Con (c, [])) cs in
+        let ts1 = List.map (T.open_ ts) ts1 in
+        let ts2 = List.map (T.open_ ts) ts2 in
+        T.seq ts1, T.seq ts2
+      | _ -> error env exp.at "FuncE not annotated with a function type"
+    in
+    let env' = adjoin_cons env ce in
+    let ve = check_pat_exhaustive env' pat in
+    check (cc = Value.call_conv_of_typ t) "different calling convention in FuncE and its type";
+    check_typ env' arg_ty;
+    check_typ env' ret_ty;
+    check ((cc.Value.sort = T.Sharable && Type.is_async ret_ty)
+           ==> isAsyncE exp)
+      "shared function with async type has non-async body";
+    let env'' =
+      {env' with labs = T.Env.empty; rets = Some ret_ty; async = false} in
+    check_exp (adjoin_vals env'' ve) exp;
+    check_sub env' exp.at arg_ty pat.note;
+    check_sub env' exp.at (typ exp) ret_ty
   | NewObjE (sort, labids, t0) ->
     let t1 =
       T.Obj(sort,
@@ -624,12 +651,7 @@ and type_exp_fields env s id t fields : T.field list * val_env =
 
 and is_func_exp exp =
   match exp.it with
-  | BlockE [dec]-> is_func_dec dec
-  | _ -> false
-
-and is_func_dec dec =
-  match dec.it with
-  | FuncD _ -> true
+  | FuncE _ -> true
   | _ -> false
 
 and type_exp_field env s (tfs, ve) field : T.field list * val_env =
@@ -690,32 +712,24 @@ and check_dec env dec  =
   (* helpers *)
   let check p = check env dec.at p in
   let (<:) t1 t2 = check_sub env dec.at t1 t2 in
+  let (<~) t1 t2 = (if T.is_mut t2 then t1 else T.as_immut t1) <: t2 in
   (* check effect *)
   check (E.Ir.infer_effect_dec dec <= E.eff dec)
     "inferred effect not a subtype of expected effect";
   (* check typing *)
   let t = typ dec in
   match dec.it with
-  | ExpD exp | LetD (_, exp) ->
+  | ExpD exp ->
     check_exp env exp;
-    (typ exp) <: t
+    typ exp <: t
+  | LetD (pat, exp) ->
+    ignore (check_pat_exhaustive env pat);
+    check_exp env exp;
+    typ exp <~ pat.note;
+    T.unit <: t
   | VarD (_, exp) ->
     check_exp env exp;
     T.unit <: t
-  | FuncD (cc, id, typ_binds, pat, t2, exp) ->
-    let t0 = T.Env.find id.it env.vals in
-    let _cs,ce = check_open_typ_binds env typ_binds in
-    let env' = adjoin_cons env ce in
-    let ve = check_pat_exhaustive env' pat in
-    check_typ env' t2;
-    check ((cc.Value.sort = T.Sharable && Type.is_async t2)
-           ==> isAsyncE exp)
-      "shared function with async type has non-async body";
-    let env'' =
-      {env' with labs = T.Env.empty; rets = Some t2; async = false} in
-    check_exp (adjoin_vals env'' ve) exp;
-    check_sub env' dec.at (typ exp) t2;
-    t0 <: t;
   | TypD c ->
     check (T.ConSet.mem c env.cons) "free type constructor";
     let (binds,typ) =
@@ -762,28 +776,6 @@ and gather_dec env scope dec : scope =
       "duplicate variable definition in block";
     let ve =  T.Env.add id.it (T.Mut (typ exp)) scope.val_env in
     { scope with val_env = ve}
-  | FuncD (call_conv, id, typ_binds, pat, typ, exp) ->
-    let func_sort = call_conv.Value.sort in
-    let cs = List.map (fun tb -> tb.it.con) typ_binds in
-    let t1 = pat.note in
-    let t2 = typ in
-    let ts1 = match call_conv.Value.n_args with
-      | 1 -> [t1]
-      | _ -> T.as_seq t1
-    in
-    let ts2 = match call_conv.Value.n_res  with
-      | 1 -> [t2]
-      | _ -> T.as_seq t2
-    in
-    let c = match func_sort, t2 with
-      | T.Sharable, (T.Async _) -> T.Promises  (* TBR: do we want this for T.Local too? *)
-      | _ -> T.Returns
-    in
-    let ts = List.map (fun typbind -> typbind.it.bound) typ_binds in
-    let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in
-    let t = T.Func (func_sort, c, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2) in
-    let ve' =  T.Env.add id.it t scope.val_env in
-    { scope with val_env = ve' }
   | TypD c ->
     check env dec.at
       (not (T.ConSet.mem c scope.con_env))