Skip to content

New IR.ActorE AST-58 #201

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nomeata merged 2 commits into from
Mar 3, 2019
Merged

New IR.ActorE AST-58 #201

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f613cc7
Normalize test suite output more
nomeata Feb 26, 2019
2dbcbd3
Refactor IR.ActorE
nomeata Feb 28, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 5 additions & 7 deletions src/arrange_ir.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ let rec exp e = match e.it with
| RelE (t, e1, ro, e2)-> "RelE" $$ [typ t; exp e1; Arrange.relop ro; exp e2]
| TupE es -> "TupE" $$ List.map exp es
| ProjE (e, i) -> "ProjE" $$ [exp e; Atom (string_of_int i)]
| ActorE (i, efs, t) -> "ActorE" $$ [id i] @ List.map exp_field efs @ [typ t]
| DotE (e, n) -> "DotE" $$ [exp e; Atom (name n)]
| ActorDotE (e, n) -> "ActorDotE" $$ [exp e; Atom (name n)]
| AssignE (e1, e2) -> "AssignE" $$ [exp e1; exp e2]
Expand All @@ -42,9 +41,11 @@ let rec exp e = match e.it with
| 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)
| ActorE (i, ds, fs, t) -> "ActorE" $$ [id i] @ List.map dec ds @ fields fs @ [typ t]
| NewObjE (s, fs, t) -> "NewObjE" $$ (Arrange.obj_sort' s :: fields fs @ [typ t])

and fields fs = List.fold_left (fun flds f -> (name f.it.name $$ [ id f.it.var ]):: flds) [] fs


and pat p = match p.it with
| WildP -> Atom "WildP"
Expand All @@ -56,9 +57,6 @@ and pat p = match p.it with

and case c = "case" $$ [pat c.it.pat; exp c.it.exp]

and exp_field (ef : exp_field)
= name ef.it.name $$ [id ef.it.id; exp ef.it.exp; Arrange.mut ef.it.mut; Arrange.vis ef.it.vis]

and name n = match n.it with
| Name l -> l

Expand Down
16 changes: 7 additions & 9 deletions src/async.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ module Transform() = struct
end
| Opt t -> Opt (t_typ t)
| Async t -> t_async nary (t_typ t)
| Obj (s, fs) -> Obj (s, List.map t_field fs)
| Obj (s, fs) -> Obj (s, List.map t_field fs)
| Mut t -> Mut (t_typ t)
| Shared -> Shared
| Any -> Any
Expand Down Expand Up @@ -210,6 +210,7 @@ module Transform() = struct

and t_field {lab; typ} =
{ lab; typ = t_typ typ }

let rec t_exp (exp: exp) =
{ it = t_exp' exp;
note = { note_typ = t_typ exp.note.note_typ;
Expand All @@ -234,9 +235,6 @@ module Transform() = struct
OptE (t_exp exp1)
| ProjE (exp1, n) ->
ProjE (t_exp exp1, n)
| ActorE (id, fields, typ) ->
let fields' = t_fields fields in
ActorE (id, fields', t_typ typ)
| DotE (exp1, id) ->
DotE (t_exp exp1, id)
| ActorDotE (exp1, id) ->
Expand Down Expand Up @@ -361,8 +359,10 @@ module Transform() = struct
| _ -> assert false
end
end
| ActorE (id, ds, fs, typ) ->
ActorE (id, t_decs ds, t_fields fs, t_typ typ)
| NewObjE (sort, ids, t) ->
NewObjE (sort, ids, t_typ t)
NewObjE (sort, t_fields ids, t_typ t)

and t_dec dec = { dec with it = t_dec' dec.it }

Expand All @@ -378,10 +378,8 @@ module Transform() = struct

and t_block (ds, exp) = (t_decs ds, t_exp exp)

and t_fields fields =
List.map (fun (field:exp_field) ->
{ field with it = { field.it with exp = t_exp field.it.exp } })
fields
and t_fields fs =
List.map (fun f -> { f with note = t_typ f.note }) fs

and t_pat pat =
{ pat with
Expand Down
12 changes: 3 additions & 9 deletions src/await.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,9 +74,6 @@ and t_exp' context exp' =
OptE (t_exp context exp1)
| ProjE (exp1, n) ->
ProjE (t_exp context exp1, n)
| ActorE (id, fields, typ) ->
let fields' = t_fields context fields in
ActorE (id, fields', typ)
| DotE (exp1, id) ->
DotE (t_exp context exp1, id)
| ActorDotE (exp1, id) ->
Expand Down Expand Up @@ -140,6 +137,8 @@ and t_exp' context exp' =
| 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)
| ActorE (id, ds, ids, t) ->
ActorE (id, t_decs context ds, ids, t)
| NewObjE (sort, ids, typ) -> exp'

and t_dec context dec =
Expand All @@ -155,11 +154,6 @@ and t_decs context decs = List.map (t_dec context) decs

and t_block context (ds, exp) = (t_decs context ds, t_exp context exp)

and t_fields context fields =
List.map (fun (field:exp_field) ->
{ field with it = { field.it with exp = t_exp context field.it.exp }})
fields

(* non-trivial translation of possibly impure terms (eff = T.Await) *)

and unary context k unE e1 =
Expand Down Expand Up @@ -334,7 +328,7 @@ and c_exp' context exp k =
unary context k (fun v1 -> e (OptE v1)) exp1
| ProjE (exp1, n) ->
unary context k (fun v1 -> e (ProjE (v1, n))) exp1
| ActorE (id, fields, t) ->
| ActorE _ ->
assert false; (* ActorE fields cannot await *)
| DotE (exp1, id) ->
unary context k (fun v1 -> e (DotE (v1, id))) exp1
Expand Down
92 changes: 26 additions & 66 deletions src/check_ir.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,6 @@ let error env at fmt =


let add_lab c x t = {c with labs = T.Env.add x t c.labs}
let add_val c x t = {c with vals = T.Env.add x t c.vals}

let add_typs c cs =
{ c with
Expand Down Expand Up @@ -118,11 +117,6 @@ let check_sub env at t1 t2 =
else error env at "subtype violation:\n %s\n %s\n"
(T.string_of_typ_expand t1) (T.string_of_typ_expand t2)

let make_mut mut : T.typ -> T.typ =
match mut.it with
| Syntax.Const -> fun t -> t
| Syntax.Var -> fun t -> T.Mut t

let rec check_typ env typ : unit =
match typ with
| T.Pre ->
Expand Down Expand Up @@ -316,12 +310,6 @@ let rec check_exp env (exp:Ir.exp) : unit =
n (T.string_of_typ_expand t1) in
tn <: t
end
| ActorE ( id, fields, t0) ->
let env' = { env with async = false } in
let t1 = type_obj env' T.Actor id t fields in
check (T.is_obj t0) "bad annotation (object type expected)";
t1 <: t0;
t0 <: t;
| ActorDotE(exp1,{it = Name n;_})
| DotE (exp1, {it = Name n;_}) ->
begin
Expand Down Expand Up @@ -537,16 +525,21 @@ let rec check_exp env (exp:Ir.exp) : unit =
, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2
) in
fun_ty <: t
| NewObjE (sort, labids, t0) ->
let t1 =
T.Obj(sort,
List.sort T.compare_field (List.map (fun (name, id) ->
let Name lab = name.it in
T.{lab; typ = T.Env.find id.it env.vals}) labids))
in
| ActorE (id, ds, fs, t0) ->
Copy link
Contributor

@crusso crusso Mar 2, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This code should probably check that t0 is well-formed in env (ie. no escape of types in ds)

Copy link
Contributor Author

@nomeata nomeata Mar 3, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point. Same with BlockE then, right?

In fact, shouldn’t we simply insert a check_typ env (typ exp) at the top of check_exp, to always check the annotation in the outer scope? Will see if that works…

Copy link
Contributor Author

@nomeata nomeata Mar 3, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Works without issues, 1da41fe.

Copy link
Contributor Author

@nomeata nomeata Mar 3, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Darn, tested the wrong binary. Actually shows issues with the output of tailcall. Let’s see if they are already on master…

Copy link
Contributor Author

@nomeata nomeata Mar 3, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

They are, see #208.

So I guess the present PR is not a regression. Will undo the extension of check_typ again and merge this.

let env' = { env with async = false } in
let ve0 = T.Env.singleton id.it t0 in
let scope0 = { empty_scope with val_env = ve0 } in
let scope1 = List.fold_left (gather_dec env') scope0 ds in
let env'' = adjoin env' scope1 in
let t1 = type_obj env'' T.Actor fs in
check (T.is_obj t0) "bad annotation (object type expected)";
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)";
t1 <: t0;
t0 <: t

(* Cases *)

Expand Down Expand Up @@ -624,59 +617,26 @@ and check_pats at env pats ve : val_env =

(* Objects *)

and type_obj env s id t fields : T.typ =
let ve = gather_exp_fields env id.it t fields in
let env' = adjoin_vals env ve in
let tfs, _ve = type_exp_fields env' s id.it t fields in
and type_obj env s fs : T.typ =
let tfs = type_exp_fields env s fs in
T.Obj (s, tfs)

and gather_exp_fields env id t fields : val_env =
let ve0 = T.Env.singleton id t in
List.fold_left (gather_exp_field env) ve0 fields

and gather_exp_field env ve field : val_env =
let {id; exp; mut; vis; _} : exp_field' = field.it in
if T.Env.mem id.it ve then
error env id.at "duplicate field name %s in object" id.it;
T.Env.add id.it ( make_mut mut (typ exp)) ve

and type_exp_fields env s id t fields : T.field list * val_env =
let env' = add_val env id t in
let tfs, ve =
List.fold_left (type_exp_field env' s) ([], T.Env.empty) fields in
List.sort T.compare_field tfs, ve
and type_exp_fields env s fs : T.field list =
let tfs = List.map (type_exp_field env s) fs in
List.sort T.compare_field tfs

and is_func_exp exp =
match exp.it with
| FuncE _ -> true
| _ -> false

and type_exp_field env s (tfs, ve) field : T.field list * val_env =
let {id; name = {it = Name name; _}; exp; mut; vis} = field.it in
let t = try T.Env.find id.it env.vals with
| Not_found -> error env field.at "field typing not found"
and type_exp_field env s f : T.field =
let {name = {it = Name name; _}; var} = f.it in
let t = try T.Env.find var.it env.vals with
| Not_found -> error env f.at "field typing not found"
in
assert (t <> T.Pre);
check_exp (adjoin_vals env ve) exp;
check_sub env field.at (typ exp) (T.as_immut t);
check env field.at ((mut.it = Syntax.Var) = T.is_mut t)
"inconsistent mutability of field and field type";
check env field.at
((s = T.Actor && vis.it = Syntax.Public) ==>
is_func_exp exp)
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 field.at
(if (s <> T.Object T.Local && vis.it = Syntax.Public)
then T.sub t T.Shared
else true)
check env f.at ((s <> T.Object T.Local) ==> T.sub t T.Shared)
"public shared object or actor field has non-shared type";
let ve' = T.Env.add id.it t ve in
let tfs' =
if vis.it = Syntax.Private
then tfs
else T.{lab = name; typ = t} :: tfs
in tfs', ve'

T.{lab = name; typ = t}

(* Declarations *)

Expand Down Expand Up @@ -748,7 +708,7 @@ and gather_dec env scope dec : scope =

(* Programs *)

let check_prog scope phase (((ds,exp), flavor) as prog) : unit =
let check_prog scope phase (((ds, exp), flavor) as prog) : unit =
let env = env_of_scope scope flavor in
try
let scope = gather_block_decs env ds in
Expand Down
Loading