From 75490ba163863b2f2d4d9a51b79f37acd7249a72 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 8 Feb 2019 11:11:09 +0100 Subject: [PATCH 1/2] Base IR.typ_bound on `con`, not `var`. Previously, `IR.typ_bound` would mirror `Syntax.typ_bound`, with a `var` instead of a `con`. But post-typechecker, we only want to work with the stamped `con`. Previously, this was hidden away in the annotations (misusing `Type.typ` as `Con.t option). This patch cleans this up a bit, but introducting a `Type.open_bind` that binds a `Con.t` to its bound, and using that as part of `FuncD`. --- src/arrange_ir.ml | 3 +-- src/arrange_type.ml | 3 +++ src/async.ml | 15 +++++++++------ src/check_ir.ml | 10 +++++----- src/compile.ml | 4 ++-- src/desugar.ml | 15 ++++++++++----- src/ir.ml | 2 +- src/parser.mly | 4 ++-- src/syntax.ml | 2 +- src/tailcall.ml | 10 +++++----- src/type.ml | 4 ++++ src/type.mli | 2 ++ src/typing.ml | 2 +- 13 files changed, 46 insertions(+), 30 deletions(-) diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index 36b574c3b7e..efa7455b059 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -70,7 +70,6 @@ and dec d = match d.it with | TypD (c,k) -> "TypD" $$ [con c; kind k] -and typ_bind (tb : typ_bind) = - tb.it.Type.var $$ [typ tb.it.Type.bound] +and typ_bind (tb : typ_bind) = Arrange_type.open_typ_bind tb.it and prog prog = "BlockE" $$ List.map dec prog.it diff --git a/src/arrange_type.ml b/src/arrange_type.ml index fa1b4d5271d..8120714d1c1 100644 --- a/src/arrange_type.ml +++ b/src/arrange_type.ml @@ -52,6 +52,9 @@ let rec typ (t:Type.typ) = match t with and typ_bind (tb : Type.bind) = tb.var $$ [typ tb.bound] +and open_typ_bind (tb : Type.open_bind) = + Con.to_string tb.con $$ [typ tb.con_bound] + and typ_field (tf : Type.field) = tf.name $$ [typ tf.typ] diff --git a/src/async.ml b/src/async.ml index 5938bbfd8b9..3bf21c15346 100644 --- a/src/async.ml +++ b/src/async.ml @@ -317,12 +317,12 @@ and t_dec' dec' = begin match s with | T.Local -> - FuncD (cc, id, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp) + FuncD (cc, id, t_typ_open_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) + FuncD (cc, id, t_typ_open_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 @@ -331,7 +331,7 @@ and t_dec' dec' = let typ' = T.Tup [] in let k = fresh_id reply_typ in let pat',d = extendTupP pat (varP k) in - let typbinds' = t_typ_binds typbinds in + let typbinds' = t_typ_open_binds typbinds in let x = fresh_id res_typ in let exp' = match exp.it with @@ -375,10 +375,13 @@ and t_pat' pat = | AltP (pat1, pat2) -> AltP (t_pat pat1, t_pat pat2) -and t_typ_bind typ_bind = - { typ_bind with it = t_bind typ_bind.it } +and t_open_bind {con; con_bound} = + {con; con_bound = t_typ con_bound} -and t_typ_binds typbinds = List.map t_typ_bind typbinds +and t_typ_open_bind typ_bind = + { typ_bind with it = t_open_bind typ_bind.it } + +and t_typ_open_binds typbinds = List.map t_typ_open_bind typbinds and t_prog prog:prog = { prog with it = t_decs prog.it } diff --git a/src/check_ir.ml b/src/check_ir.ml index d4a3f2472b3..81f6a4eb607 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -693,10 +693,10 @@ and cons_of_typ_binds typ_binds = List.map con_of_typ_bind typ_binds and check_open_typ_binds env typ_binds = - let cs = cons_of_typ_binds typ_binds in - let ks = List.map (fun tp -> T.Abs([],tp.it.T.bound)) typ_binds in + let cs = List.map (fun tp -> tp.it.T.con) typ_binds in + let ks = List.map (fun tp -> T.Abs([],tp.it.T.con_bound)) typ_binds in let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in - let binds = T.close_binds cs (List.map (fun tb -> tb.it) typ_binds) in + let binds = T.close_open_binds cs (List.map (fun tb -> tb.it) typ_binds) in let _,_ = check_typ_binds env binds in cs,ce @@ -777,7 +777,7 @@ and gather_dec env scope dec : scope = { scope with val_env = ve} | FuncD (call_conv, id, typ_binds, pat, typ, exp) -> let func_sort = call_conv.Value.sort in - let cs = cons_of_typ_binds typ_binds in + let cs = List.map (fun tb -> tb.it.T.con) typ_binds in let t1 = pat.note in let t2 = typ in let ts1 = match call_conv.Value.n_args with @@ -792,7 +792,7 @@ and gather_dec env scope dec : scope = | 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.T.bound) typ_binds in + let ts = List.map (fun typbind -> typbind.it.T.con_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 diff --git a/src/compile.ml b/src/compile.ml index 7c77c1c4a15..6e58d5019cf 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -239,8 +239,8 @@ module E = struct This shoulds be extracte into Type.add_open_typ_binds and maybe we need a type open_typ_bind that can be used inside the IR. *) - let cs = Check_ir.cons_of_typ_binds typ_binds in - let ks = List.map (fun tp -> Type.Abs([],tp.it.Type.bound)) typ_binds in + let cs = List.map (fun tp -> tp.it.Type.con) typ_binds in + let ks = List.map (fun tp -> Type.Abs([],tp.it.Type.con_bound)) typ_binds in let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in { env with con_env = Con.Env.adjoin env.con_env ce } diff --git a/src/desugar.ml b/src/desugar.ml index 393c5994ae2..6f5744b25b1 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -128,9 +128,14 @@ and exp_field' (f : S.exp_field') = and typ_binds tbs = List.map typ_bind tbs and typ_bind tb = - phrase' typ_bind' tb - -and typ_bind' at n { S.var; S.bound } = { Type.var = var.it; Type.bound = bound.note } + let c = match tb.note with + | Some c -> c + | _ -> assert false + in + { it = { T.con = c; T.con_bound = tb.it.S.bound.note} + ; at = tb.at + ; note = () + } and decs ds = match ds with @@ -163,8 +168,8 @@ and dec' at n d = match d with let inst = List.map (fun tb -> match tb.note with - | Type.Pre -> assert false - | t -> t) + | None -> assert false + | Some c -> T.Con (c, [])) tbs in let obj_typ = match n.S.note_typ with diff --git a/src/ir.ml b/src/ir.ml index 69b1162163c..db727002b5c 100644 --- a/src/ir.ml +++ b/src/ir.ml @@ -3,7 +3,7 @@ type type_note = Syntax.typ_note = {note_typ : Type.typ; note_eff : Type.eff} type 'a phrase = ('a, Syntax.typ_note) Source.annotated_phrase -type typ_bind = (Type.bind, Type.typ) Source.annotated_phrase +type typ_bind = Type.open_bind Source.phrase type pat = (pat', Type.typ) Source.annotated_phrase and pat' = diff --git a/src/parser.mly b/src/parser.mly index 294e1cd3cd9..3d205e2c8c3 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -256,9 +256,9 @@ typ_field : typ_bind : | x=id SUB t=typ - { {var = x; bound = t} @! at $sloc } + { {var = x; bound = t} @= at $sloc } | x=id - { {var = x; bound = PrimT "Any" @! at $sloc} @! at $sloc } + { {var = x; bound = PrimT "Any" @! at $sloc} @= at $sloc } diff --git a/src/syntax.ml b/src/syntax.ml index eab511f8aad..01fa40b3ad1 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -42,7 +42,7 @@ and typ' = and typ_field = typ_field' Source.phrase and typ_field' = {id : id; typ : typ; mut : mut} -and typ_bind = (typ_bind', Type.typ) Source.annotated_phrase +and typ_bind = (typ_bind', Con.t option) Source.annotated_phrase and typ_bind' = {var : id; bound : typ} diff --git a/src/tailcall.ml b/src/tailcall.ml index 35f4df59122..8f0f2b2abea 100644 --- a/src/tailcall.ml +++ b/src/tailcall.ml @@ -64,10 +64,10 @@ let bind env i (info:func_info option) : env = let are_generic_insts tbs insts = List.for_all2 (fun tb inst -> - match tb.note, inst with - | Con(c1,[]), Con(c2,[]) -> c1 = c2 (* conservative, but safe *) - | Con(c1,[]), _ -> false - | _,_ -> assert false) tbs insts + match inst with + | Con(c2,[]) -> tb.it.Type.con = c2 (* conservative, but safe *) + | _ -> false + ) tbs insts let rec tailexp env e = {e with it = exp' env e} @@ -210,7 +210,7 @@ and dec' env d = in let env3 = pat env2 p in (* shadow id if necessary *) let exp0' = tailexp env3 exp0 in - let cs = List.map (fun tb -> tb.note) tbs in + let cs = List.map (fun tb -> Con (tb.it.Type.con, [])) tbs in if !tail_called then let ids = match typ d with | Func( _, _, _, dom, _) -> List.map (fun t -> fresh_id (open_ cs t)) dom diff --git a/src/type.ml b/src/type.ml index 33bb6a837f4..31fe318cae7 100644 --- a/src/type.ml +++ b/src/type.ml @@ -38,6 +38,7 @@ and typ = | Pre (* pre-type *) and bind = {var : string; bound : typ} +and open_bind = {con : con; con_bound : typ} and field = {name : string; typ : typ} (* field ordering *) @@ -173,6 +174,9 @@ let close_binds cs tbs = if cs = [] then tbs else List.map (fun {var; bound} -> {var; bound = close cs bound}) tbs +let close_open_binds cs tbs = + List.map (fun {con; con_bound} -> {var = Con.name con; bound = close cs con_bound}) tbs + let rec open' i ts t = match t with diff --git a/src/type.mli b/src/type.mli index 884ac714070..5d2ee4f814f 100644 --- a/src/type.mli +++ b/src/type.mli @@ -38,6 +38,7 @@ and typ = | Pre (* pre-type *) and bind = {var : string; bound : typ} +and open_bind = {con : con; con_bound : typ} and field = {name : string; typ : typ} (* field ordering *) @@ -129,6 +130,7 @@ val glb : con_env -> typ -> typ -> typ val close : con list -> typ -> typ val close_binds : con list -> bind list -> bind list +val close_open_binds : con list -> open_bind list -> bind list val open_ : typ list -> typ -> typ val open_binds : con_env -> bind list -> typ list * con_env diff --git a/src/typing.ml b/src/typing.ml index ad59595bef7..e5113c3ed5d 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -214,7 +214,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 x -> Con.fresh x) xs in - List.iter2 (fun typ_bind c -> typ_bind.note <- T.Con (c, [])) typ_binds cs; + List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs; 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 From a6bb1dce8e7b4316cc0ac0b98df523f265e5a6b9 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 8 Feb 2019 16:06:47 +0100 Subject: [PATCH 2/2] Put `IR.typ_bind` defininition into `Ir` as advised by Andreas. Also name some things more appropriately. --- src/arrange_ir.ml | 4 +++- src/arrange_type.ml | 3 --- src/async.ml | 16 ++++++++-------- src/check_ir.ml | 13 ++++++++----- src/compile.ml | 4 ++-- src/desugar.ml | 2 +- src/ir.ml | 3 ++- src/tailcall.ml | 4 ++-- src/type.ml | 4 ---- src/type.mli | 2 -- 10 files changed, 26 insertions(+), 29 deletions(-) diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index efa7455b059..58b8760f23d 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -70,6 +70,8 @@ and dec d = match d.it with | TypD (c,k) -> "TypD" $$ [con c; kind k] -and typ_bind (tb : typ_bind) = Arrange_type.open_typ_bind tb.it +and typ_bind (tb : typ_bind) = + Con.to_string tb.it.con $$ [typ tb.it.bound] + and prog prog = "BlockE" $$ List.map dec prog.it diff --git a/src/arrange_type.ml b/src/arrange_type.ml index 8120714d1c1..fa1b4d5271d 100644 --- a/src/arrange_type.ml +++ b/src/arrange_type.ml @@ -52,9 +52,6 @@ let rec typ (t:Type.typ) = match t with and typ_bind (tb : Type.bind) = tb.var $$ [typ tb.bound] -and open_typ_bind (tb : Type.open_bind) = - Con.to_string tb.con $$ [typ tb.con_bound] - and typ_field (tf : Type.field) = tf.name $$ [typ tf.typ] diff --git a/src/async.ml b/src/async.ml index 3bf21c15346..e91e6907cb4 100644 --- a/src/async.ml +++ b/src/async.ml @@ -317,12 +317,12 @@ and t_dec' dec' = begin match s with | T.Local -> - FuncD (cc, id, t_typ_open_binds typbinds, t_pat pat, t_typ typT, t_exp exp) + FuncD (cc, id, 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_open_binds typbinds, t_pat pat, t_typ typT, t_exp exp) + FuncD (cc, id, 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 @@ -331,7 +331,7 @@ and t_dec' dec' = let typ' = T.Tup [] in let k = fresh_id reply_typ in let pat',d = extendTupP pat (varP k) in - let typbinds' = t_typ_open_binds typbinds in + let typbinds' = t_typ_binds typbinds in let x = fresh_id res_typ in let exp' = match exp.it with @@ -375,13 +375,13 @@ and t_pat' pat = | AltP (pat1, pat2) -> AltP (t_pat pat1, t_pat pat2) -and t_open_bind {con; con_bound} = - {con; con_bound = t_typ con_bound} +and t_typ_bind' {con; bound} = + {con; bound = t_typ bound} -and t_typ_open_bind typ_bind = - { typ_bind with it = t_open_bind typ_bind.it } +and t_typ_bind typ_bind = + { typ_bind with it = t_typ_bind' typ_bind.it } -and t_typ_open_binds typbinds = List.map t_typ_open_bind typbinds +and t_typ_binds typbinds = List.map t_typ_bind typbinds and t_prog prog:prog = { prog with it = t_decs prog.it } diff --git a/src/check_ir.ml b/src/check_ir.ml index 81f6a4eb607..95be4d11026 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -693,13 +693,16 @@ and cons_of_typ_binds typ_binds = List.map con_of_typ_bind typ_binds and check_open_typ_binds env typ_binds = - let cs = List.map (fun tp -> tp.it.T.con) typ_binds in - let ks = List.map (fun tp -> T.Abs([],tp.it.T.con_bound)) typ_binds in + let cs = List.map (fun tp -> tp.it.con) typ_binds in + let ks = List.map (fun tp -> T.Abs([],tp.it.bound)) typ_binds in let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in - let binds = T.close_open_binds cs (List.map (fun tb -> tb.it) typ_binds) in + let binds = close_typ_binds cs (List.map (fun tb -> tb.it) typ_binds) in let _,_ = check_typ_binds env binds in cs,ce +and close_typ_binds cs tbs = + List.map (fun {con; bound} -> {Type.var = Con.name con; bound = Type.close cs bound}) tbs + and check_dec env dec = (* helpers *) let check p = check env dec.at p in @@ -777,7 +780,7 @@ and gather_dec env scope dec : scope = { 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.T.con) typ_binds 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 @@ -792,7 +795,7 @@ and gather_dec env scope dec : scope = | 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.T.con_bound) typ_binds 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 diff --git a/src/compile.ml b/src/compile.ml index 6e58d5019cf..94601a684f0 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -239,8 +239,8 @@ module E = struct This shoulds be extracte into Type.add_open_typ_binds and maybe we need a type open_typ_bind that can be used inside the IR. *) - let cs = List.map (fun tp -> tp.it.Type.con) typ_binds in - let ks = List.map (fun tp -> Type.Abs([],tp.it.Type.con_bound)) typ_binds in + let cs = List.map (fun tp -> tp.it.con) typ_binds in + let ks = List.map (fun tp -> Type.Abs([],tp.it.bound)) typ_binds in let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in { env with con_env = Con.Env.adjoin env.con_env ce } diff --git a/src/desugar.ml b/src/desugar.ml index 6f5744b25b1..becb43e73a9 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -132,7 +132,7 @@ and typ_bind tb = | Some c -> c | _ -> assert false in - { it = { T.con = c; T.con_bound = tb.it.S.bound.note} + { it = { Ir.con = c; Ir.bound = tb.it.S.bound.note} ; at = tb.at ; note = () } diff --git a/src/ir.ml b/src/ir.ml index db727002b5c..55b1aca6e63 100644 --- a/src/ir.ml +++ b/src/ir.ml @@ -3,7 +3,8 @@ type type_note = Syntax.typ_note = {note_typ : Type.typ; note_eff : Type.eff} type 'a phrase = ('a, Syntax.typ_note) Source.annotated_phrase -type typ_bind = Type.open_bind Source.phrase +and typ_bind' = {con : Con.t; bound : Type.typ} +type typ_bind = typ_bind' Source.phrase type pat = (pat', Type.typ) Source.annotated_phrase and pat' = diff --git a/src/tailcall.ml b/src/tailcall.ml index 8f0f2b2abea..00adecd6305 100644 --- a/src/tailcall.ml +++ b/src/tailcall.ml @@ -65,7 +65,7 @@ let bind env i (info:func_info option) : env = let are_generic_insts tbs insts = List.for_all2 (fun tb inst -> match inst with - | Con(c2,[]) -> tb.it.Type.con = c2 (* conservative, but safe *) + | Con(c2,[]) -> tb.it.con = c2 (* conservative, but safe *) | _ -> false ) tbs insts @@ -210,7 +210,7 @@ and dec' env d = in let env3 = pat env2 p in (* shadow id if necessary *) let exp0' = tailexp env3 exp0 in - let cs = List.map (fun tb -> Con (tb.it.Type.con, [])) tbs in + let cs = List.map (fun tb -> Con (tb.it.con, [])) tbs in if !tail_called then let ids = match typ d with | Func( _, _, _, dom, _) -> List.map (fun t -> fresh_id (open_ cs t)) dom diff --git a/src/type.ml b/src/type.ml index 31fe318cae7..33bb6a837f4 100644 --- a/src/type.ml +++ b/src/type.ml @@ -38,7 +38,6 @@ and typ = | Pre (* pre-type *) and bind = {var : string; bound : typ} -and open_bind = {con : con; con_bound : typ} and field = {name : string; typ : typ} (* field ordering *) @@ -174,9 +173,6 @@ let close_binds cs tbs = if cs = [] then tbs else List.map (fun {var; bound} -> {var; bound = close cs bound}) tbs -let close_open_binds cs tbs = - List.map (fun {con; con_bound} -> {var = Con.name con; bound = close cs con_bound}) tbs - let rec open' i ts t = match t with diff --git a/src/type.mli b/src/type.mli index 5d2ee4f814f..884ac714070 100644 --- a/src/type.mli +++ b/src/type.mli @@ -38,7 +38,6 @@ and typ = | Pre (* pre-type *) and bind = {var : string; bound : typ} -and open_bind = {con : con; con_bound : typ} and field = {name : string; typ : typ} (* field ordering *) @@ -130,7 +129,6 @@ val glb : con_env -> typ -> typ -> typ val close : con list -> typ -> typ val close_binds : con list -> bind list -> bind list -val close_open_binds : con list -> open_bind list -> bind list val open_ : typ list -> typ -> typ val open_binds : con_env -> bind list -> typ list * con_env