From 1b886cc0dd3badc9b23caabea42cb808fa0d9e7f Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Tue, 5 Feb 2019 16:04:02 -0700 Subject: [PATCH 01/42] initial draft; the pass does nothing at all, yet --- src/pipeline.ml | 2 + src/simploop.ml | 95 ++++++++++++++++++++++++++++++++++++++++++++++++ src/simploop.mli | 2 + 3 files changed, 99 insertions(+) create mode 100644 src/simploop.ml create mode 100644 src/simploop.mli diff --git a/src/pipeline.ml b/src/pipeline.ml index 1906a01122b..4887a726b78 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -294,6 +294,8 @@ let compile_with check mode name : compile_result = let prog = await_lowering true initial_stat_env prog name in let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in + (* TEMP-Matthew: next line here just to get this module to compile *) + let _ = Simploop.transform initial_stat_env prog in phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_ diff --git a/src/simploop.ml b/src/simploop.ml new file mode 100644 index 00000000000..68d4858f497 --- /dev/null +++ b/src/simploop.ml @@ -0,0 +1,95 @@ +(* + Simplify loop constructs. + + Mapping each occurence of a looping construct to an infinite loop. + *) + +open Source +module I = Ir + +let phrase f x = { x with it = f x.it } + +let phrase' f x = { x with it = f x.at x.note x.it } + +let rec exps es = List.map exp es + +and exp e = phrase' exp' e + +and exp' at note = function + | I.AsyncE _ -> assert false + | I.AwaitE _ -> assert false + | I.PrimE p -> I.PrimE p + | I.VarE i -> I.VarE i + | I.LitE l -> I.LitE l + | I.UnE (ot, o, e) -> + I.UnE (ot, o, exp e) + | I.BinE (ot, e1, o, e2) -> + I.BinE (ot, exp e1, o, exp e2) + | I.RelE (ot, e1, o, e2) -> + I.RelE (ot, exp e1, o, exp e2) + | I.TupE es -> I.TupE (exps es) + | I.ProjE (e, i) -> I.ProjE (exp e, i) + | I.OptE e -> I.OptE (exp e) + | I.DotE (e, n) -> I.DotE(exp e, n) + | I.AssignE (e1, e2) -> I.AssignE (exp e1, exp e2) + | I.ArrayE (m, t, es) -> I.ArrayE (m, t, exps es) + | I.IdxE (e1, e2) -> I.IdxE (exp e1, exp e2) + | I.CallE (cc, e1, inst, e2) -> I.CallE (cc, exp e1, inst, exp e2) + | I.BlockE (ds, ot) -> I.BlockE (decs ds, ot) + | I.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3) + | I.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs) + | I.LabelE (l, t, e) -> I.LabelE (l, t, exp e) + | I.BreakE (l, e) -> I.BreakE (l, exp e) + | I.RetE e -> I.RetE (exp e) + | I.AssertE e -> I.AssertE (exp e) + | I.IsE (e1, e2) -> I.IsE (exp e1, exp e2) + | I.ActorDotE(e, n) -> I.ActorDotE(exp e, n) + | I.DeclareE(i, t, e) -> I.DeclareE(i, t, exp e) + | I.DefineE(i, m, e) -> I.DefineE(i, m, exp e) + | I.NewObjE(s, nis, t) -> I.NewObjE(s, nis, t) + | I.ActorE(i, fs, t) -> I.ActorE(i, exp_fields fs, t) + (*--- "Interesting" cases: The looping constructs. ---*) + | I.LoopE (e1, None) -> I.LoopE (exp e1, None) (* <-- This form is simplest, and preferred *) + | I.LoopE (e1, Some e2) -> I.LoopE (exp e1, Some (exp e2)) (* TODO: Transform this form to LoopE(_,None) *) + | I.WhileE (e1, e2) -> I.WhileE (exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) + | I.ForE (p, e1, e2) -> I.ForE (p, exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) + +and exp_fields fs = List.map exp_field fs + +and exp_field f = phrase exp_field' f + +and exp_field' (f : Ir.exp_field') = + Ir.{ I.name = f.name; I.id = f.id; I.exp = exp f.exp; I.mut = f.mut; I.priv = f.priv } + +and decs ds = + match ds with + | [] -> [] + | d::ds -> (phrase' dec' d) :: (decs ds) + +and dec' at n d = match d with + | I.ExpD e -> I.ExpD (exp e) + | I.LetD (p, e) -> I.LetD (p, exp e) + | I.VarD (i, e) -> I.VarD (i, exp e) + | I.FuncD (cc, i, tbs, p, ty, e) -> + I.FuncD (cc, i, tbs, p, ty, exp e) + | I.TypD (c,k) -> + I.TypD (c,k) + +and cases cs = List.map case cs + +and case c = phrase case' c + +and case' c = I.{ I.pat = c.pat; I.exp = exp c.exp } + +and prog p = phrase decs p + +(* validation *) + +let check_prog scope (prog:I.prog) = + let env = Check_ir.env_of_scope scope in + Check_ir.check_prog env prog + +let transform scope (p:I.prog) = + let p' = prog p in + check_prog scope p'; + p' diff --git a/src/simploop.mli b/src/simploop.mli new file mode 100644 index 00000000000..0b1e6e5e987 --- /dev/null +++ b/src/simploop.mli @@ -0,0 +1,2 @@ +val prog : Ir.prog -> Ir.prog +val transform : Typing.scope -> Ir.prog -> Ir.prog From 7b739f1ebbb9e7d6640af423985c767cb647e4b9 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Tue, 5 Feb 2019 16:29:54 -0700 Subject: [PATCH 02/42] sanity check: pipeline still passes all tests --- src/pipeline.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pipeline.ml b/src/pipeline.ml index 4887a726b78..901c2d7d166 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -295,7 +295,7 @@ let compile_with check mode name : compile_result = let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in (* TEMP-Matthew: next line here just to get this module to compile *) - let _ = Simploop.transform initial_stat_env prog in + let prog = Simploop.transform initial_stat_env prog in phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_ From c686ad0757bf3bac5830dc1628138995dfb03649 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Wed, 6 Feb 2019 10:28:33 -0700 Subject: [PATCH 03/42] notes and questions about the planned transforms; writing them out should be straightforward, given answers to the questions --- src/simploop.ml | 64 +++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 59 insertions(+), 5 deletions(-) diff --git a/src/simploop.ml b/src/simploop.ml index 68d4858f497..76284d8366f 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -1,7 +1,8 @@ -(* +(* Simplify loop constructs. Mapping each occurence of a looping construct to an infinite loop. + *) open Source @@ -50,9 +51,62 @@ and exp' at note = function | I.ActorE(i, fs, t) -> I.ActorE(i, exp_fields fs, t) (*--- "Interesting" cases: The looping constructs. ---*) | I.LoopE (e1, None) -> I.LoopE (exp e1, None) (* <-- This form is simplest, and preferred *) - | I.LoopE (e1, Some e2) -> I.LoopE (exp e1, Some (exp e2)) (* TODO: Transform this form to LoopE(_,None) *) - | I.WhileE (e1, e2) -> I.WhileE (exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) - | I.ForE (p, e1, e2) -> I.ForE (p, exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) + + (* Questions about the target of each transformation case below: + + 1. Do we need the loop { } expression _and_ the label; does the + label alone suffice? (Can we label any subexpression and make it + a jump target, or only loops?) + + 2. Related to 1, if we do need the loop constructs and the + labels, do we also need to use explicit "continue" expressions? + + 3. The rewrite for for-loops is the most involved, and involves a + subexpression with nontrivial (non-unit, non-boolean) type; + namely, the first subexpression of the for-loop must be an + iterator object. Doing this rewrite without first doing this + check would be wrong, but assuming the AST is typed, no extra + type information seems required to inform or guide the + transformation; it is "fully parametric" in all of the + sub-expressions, it seems. + + Hence, all of these rewrites could probably happen in the desugar + module, though they should only happen on a well-typed source + AST. + *) + + (* Transformation from loop-while to loop: *) + | I.LoopE (e1, Some e2) -> + (* + loop e1 while e2 + ~~> + label l: loop { e1 ; if e2 then break l else continue l } + *) + I.LoopE (exp e1, Some (exp e2)) (* TODO *) + + (* Transformation from while to loop: *) + | I.WhileE (e1, e2) -> + (* + while e1 e2 + ~~> + label l: loop { if e1 then { e2 ; continue l } else break l } + *) + I.WhileE (exp e1, exp e2) (* TODO *) + + (* Transformation from for to loop: *) + | I.ForE (p, e1, e2) -> + (* + for x in e1 e2 + ~~> + label l: loop { + switch e1.next() { + case null { break l }; + case x { e2 ; continue l }; + } + } + *) + I.ForE (p, exp e1, exp e2) (* TODO *) + and exp_fields fs = List.map exp_field fs @@ -72,7 +126,7 @@ and dec' at n d = match d with | I.VarD (i, e) -> I.VarD (i, exp e) | I.FuncD (cc, i, tbs, p, ty, e) -> I.FuncD (cc, i, tbs, p, ty, exp e) - | I.TypD (c,k) -> + | I.TypD (c,k) -> I.TypD (c,k) and cases cs = List.map case cs From df1f3c164e53e6ed24b98bef349c5dc444c55a90 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 04:15:43 -0700 Subject: [PATCH 04/42] move RHS's of loop transforms, stil pending, into Construct module --- src/construct.ml | 31 ++++++++++++++++++++++++- src/construct.mli | 4 ++++ src/simploop.ml | 59 +++++++++++++++++++++++++---------------------- 3 files changed, 66 insertions(+), 28 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 6b435a60268..656d878ede6 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -225,6 +225,36 @@ let loopE exp1 exp2Opt = S.note_typ = Type.Non } } +let loopWhileE' exp1 exp2 = + (* + loop e1 while e2 + ~~> + label l: loop { e1 ; if e2 then break l else continue l } + *) + LoopE(exp1,Some exp2) + +let whileE' exp1 exp2 = + (* + while e1 e2 + ~~> + label l: loop { if e1 then { e2 ; continue l } else break l } + *) + WhileE(exp1,exp2) + +let forE' pat exp1 exp2 = + (* + for x in e1 e2 + ~~> + label l: loop { + switch e1.next() { + case null { break l }; + case x { e2 ; continue l }; + } + } + *) + ForE(pat,exp1,exp2) + + let declare_idE x typ exp1 = { it = DeclareE (x, typ, exp1); at = no_region; @@ -391,4 +421,3 @@ let prim_async typ = let prim_await typ = primE "@await" (T.Func (T.Call T.Local, T.Returns, [], [T.Async typ; contT typ], [])) - diff --git a/src/construct.mli b/src/construct.mli index a948b69335d..41b2ba282fa 100644 --- a/src/construct.mli +++ b/src/construct.mli @@ -61,6 +61,10 @@ val assignE : exp -> exp -> exp val labelE : Syntax.id -> typ -> exp -> exp val loopE: exp -> exp option -> exp +val whileE' : exp -> exp -> exp' +val loopWhileE' : exp -> exp -> exp' +val forE' : pat -> exp -> exp -> exp' + val declare_idE : Syntax.id -> typ -> exp -> exp val define_idE : Syntax.id -> Syntax.mut -> exp -> exp val newObjE : Syntax.obj_sort -> (Syntax.name * Syntax.id) list -> typ -> exp diff --git a/src/simploop.ml b/src/simploop.ml index 76284d8366f..bbf6ecf2e2a 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -58,6 +58,8 @@ and exp' at note = function label alone suffice? (Can we label any subexpression and make it a jump target, or only loops?) + Cladio: No. Loops need not be labeled, except to break. + 2. Related to 1, if we do need the loop constructs and the labels, do we also need to use explicit "continue" expressions? @@ -73,40 +75,43 @@ and exp' at note = function Hence, all of these rewrites could probably happen in the desugar module, though they should only happen on a well-typed source AST. + + ---------------------------------------------------------------------------------------------------------- + Claudio's Answers, copied from here: https://github.com/dfinity-lab/actorscript/pull/146#commitcomment-32218790 + + - I believe you can label any expression and make it a jump target. + + (Matthew: Ok. But because I'd rather not loose all structure, I guess I'll label loops, and not try to create, e.g., strange non-structural loops) + + - There is no need to label the loop unless you do and early break or continue. + + (Matthew: Ok, I seem to need to break every loop that I create, so I guess each needs a label?) + + - The continue in the while translation is redundant, I think; just fall through. + + (Matthew: Ok.) + + - Continue isn't special IRCC, it's just a special named label ("continue-" or something like that) introduced by the parser. + (the loop(_,None) construct just loops forever, but you can still exit via break). + + - I would indeed just do this desugaring in the parser + + (Matthew: Ok, sounds good; I'll keep this separate until it works, then integrate there.) + + - you might even be able to extend construct_ir.ml with functions whileE etc for constructing primitive + loops and modify the transformation to use those instead of WhileE etc. + + (Matthew: Ok. I'll define the RHS of each rewrite in that module, for potential use elsewhere in the pipeline too.) *) (* Transformation from loop-while to loop: *) - | I.LoopE (e1, Some e2) -> - (* - loop e1 while e2 - ~~> - label l: loop { e1 ; if e2 then break l else continue l } - *) - I.LoopE (exp e1, Some (exp e2)) (* TODO *) + | I.LoopE (e1, Some e2) -> Construct.loopWhileE' (exp e1) (exp e2) (* Transformation from while to loop: *) - | I.WhileE (e1, e2) -> - (* - while e1 e2 - ~~> - label l: loop { if e1 then { e2 ; continue l } else break l } - *) - I.WhileE (exp e1, exp e2) (* TODO *) + | I.WhileE (e1, e2) -> Construct.whileE' (exp e1) (exp e2) (* Transformation from for to loop: *) - | I.ForE (p, e1, e2) -> - (* - for x in e1 e2 - ~~> - label l: loop { - switch e1.next() { - case null { break l }; - case x { e2 ; continue l }; - } - } - *) - I.ForE (p, exp e1, exp e2) (* TODO *) - + | I.ForE (p, e1, e2) -> Construct.forE' p (exp e1) (exp e2) and exp_fields fs = List.map exp_field fs From 24676788ab5dd1eeab2934116a00e8acdb44660b Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 04:51:29 -0700 Subject: [PATCH 05/42] 1/3 of the derived loop forms in Construct; triggering WASM test errors --- src/construct.ml | 81 ++++++++++++++++++++++++++++++------------------ 1 file changed, 50 insertions(+), 31 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 656d878ede6..0326a06ec8c 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -225,36 +225,6 @@ let loopE exp1 exp2Opt = S.note_typ = Type.Non } } -let loopWhileE' exp1 exp2 = - (* - loop e1 while e2 - ~~> - label l: loop { e1 ; if e2 then break l else continue l } - *) - LoopE(exp1,Some exp2) - -let whileE' exp1 exp2 = - (* - while e1 e2 - ~~> - label l: loop { if e1 then { e2 ; continue l } else break l } - *) - WhileE(exp1,exp2) - -let forE' pat exp1 exp2 = - (* - for x in e1 e2 - ~~> - label l: loop { - switch e1.next() { - case null { break l }; - case x { e2 ; continue l }; - } - } - *) - ForE(pat,exp1,exp2) - - let declare_idE x typ exp1 = { it = DeclareE (x, typ, exp1); at = no_region; @@ -299,7 +269,6 @@ let varD x exp = { it = VarD (x, exp); let expD exp = { exp with it = ExpD exp } - (* let expressions (derived) *) let letE x exp1 exp2 = blockE [letD x exp1; expD exp2] @@ -421,3 +390,53 @@ let prim_async typ = let prim_await typ = primE "@await" (T.Func (T.Call T.Local, T.Returns, [], [T.Async typ; contT typ], [])) + +(* derived loop forms; each can be expressed as an unconditional loop *) + +let loopWhileE exp1 exp2 = + (* loop e1 while e2 + ~~> label l: loop { + let () = e1 ; + let x2 = e2 ; + if x2 { break l x1 } else { } } + *) + let id2 = fresh_id exp2.note.S.note_typ in + let lab = fresh_lab () in + let ty1 = Type.unit in + labelE lab ty1 ( + loopE ( + blockE [ + expD exp1 ; + letD id2 exp2 ; + expD (ifE id2 + (breakE lab (tupE []) ty1) + (tupE []) + ty1 + ) + ] + ) None + ) + +(* LoopE(exp1,Some exp2) *) +let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it + +let whileE' exp1 exp2 = + (* + while e1 e2 + ~~> + label l: loop { if e1 then { e2 ; continue l } else break l } + *) + WhileE(exp1,exp2) + +let forE' pat exp1 exp2 = + (* + for x in e1 e2 + ~~> + label l: loop { + switch e1.next() { + case null { break l }; + case x { e2 ; continue l }; + } + } + *) + ForE(pat,exp1,exp2) From 517d2365f1e17d66fa3710ab20edef096969fd3f Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 04:54:32 -0700 Subject: [PATCH 06/42] minor: fix typo in comment --- src/construct.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/construct.ml b/src/construct.ml index 0326a06ec8c..c867d93a2b2 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -398,7 +398,7 @@ let loopWhileE exp1 exp2 = ~~> label l: loop { let () = e1 ; let x2 = e2 ; - if x2 { break l x1 } else { } } + if x2 { break l } else { } } *) let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in From 53fbdc1eb6beb9894df9309e02f8385a03bf2463 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 05:13:38 -0700 Subject: [PATCH 07/42] fix bug that I introduced; another xform case passes all tests --- src/construct.ml | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index c867d93a2b2..fb75580e6e3 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -269,6 +269,7 @@ let varD x exp = { it = VarD (x, exp); let expD exp = { exp with it = ExpD exp } + (* let expressions (derived) *) let letE x exp1 exp2 = blockE [letD x exp1; expD exp2] @@ -398,7 +399,7 @@ let loopWhileE exp1 exp2 = ~~> label l: loop { let () = e1 ; let x2 = e2 ; - if x2 { break l } else { } } + if x2 { } else { break } } *) let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in @@ -409,8 +410,8 @@ let loopWhileE exp1 exp2 = expD exp1 ; letD id2 exp2 ; expD (ifE id2 - (breakE lab (tupE []) ty1) (tupE []) + (breakE lab (tupE []) ty1) ty1 ) ] @@ -420,13 +421,30 @@ let loopWhileE exp1 exp2 = (* LoopE(exp1,Some exp2) *) let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it -let whileE' exp1 exp2 = +let whileE exp1 exp2 = (* while e1 e2 ~~> label l: loop { if e1 then { e2 ; continue l } else break l } *) - WhileE(exp1,exp2) + let ty1 = exp1.note.S.note_typ in + let id1 = fresh_id ty1 in + let lab = fresh_lab () in + let ty2 = Type.unit in + labelE lab ty2 ( + loopE ( + blockE [ + letD id1 exp1 ; + expD (ifE id1 + exp2 + (breakE lab (tupE []) ty2) + ty2 + ) + ] + ) None + ) + +let whileE' exp1 exp2 = (whileE exp1 exp2).it let forE' pat exp1 exp2 = (* From c28bf054473d6344e0a83dc68c281008ea7c4cbc Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 06:37:06 -0700 Subject: [PATCH 08/42] stuck: how to get the Con env where I need it? --- src/construct.ml | 75 +++++++++++++++++++++++++++++++++++++----------- 1 file changed, 59 insertions(+), 16 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index fb75580e6e3..944373c80fb 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -399,7 +399,7 @@ let loopWhileE exp1 exp2 = ~~> label l: loop { let () = e1 ; let x2 = e2 ; - if x2 { } else { break } } + if x2 { } else { break l } } *) let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in @@ -422,10 +422,10 @@ let loopWhileE exp1 exp2 = let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it let whileE exp1 exp2 = - (* - while e1 e2 - ~~> - label l: loop { if e1 then { e2 ; continue l } else break l } + (* while e1 e2 + ~~> label l: loop { + let x1 = e1 ; + if x1 then { e2 } else { break l } } *) let ty1 = exp1.note.S.note_typ in let id1 = fresh_id ty1 in @@ -435,7 +435,7 @@ let whileE exp1 exp2 = loopE ( blockE [ letD id1 exp1 ; - expD (ifE id1 + expD (ifE id1 exp2 (breakE lab (tupE []) ty2) ty2 @@ -446,15 +446,58 @@ let whileE exp1 exp2 = let whileE' exp1 exp2 = (whileE exp1 exp2).it -let forE' pat exp1 exp2 = +let forE pat exp1 exp2 = + (* for p in e1 e2 + ~~> + let x1 = e1 ; + let nxt = e1.next ; + label l: loop { + let x1' = nxt () ; + switch x1' { + case null { break l }; + case p { e2 }; + } + } *) + let lab = fresh_lab () in + let tyu = Type.unit in + let ty1 = exp1.note.S.note_typ in + + (* XXX: not sure how to get type info for `next` function... + - ...how to do I supply a non-empty con_env for `as_obj_sub` ? + *) + let _, tfs = Type.as_obj_sub "next" (Con.Env.from_list []) ty1 in + let tnxt = T.lookup_field "next" tfs in + let ty1_ret = match (T.as_func tnxt) with + | _,_,_,_,[x] -> x + | _ -> failwith "invalid return type" + in + + let id1 = fresh_id ty1 in + let nxt = fresh_id tnxt in + let id1' = fresh_id ty1_ret in (* - for x in e1 e2 - ~~> - label l: loop { - switch e1.next() { - case null { break l }; - case x { e2 ; continue l }; - } - } + Printf.eprintf "XXX ty1 = %s\n" (T.string_of_typ ty1); + Printf.eprintf "XXX tnxt = %s\n" (T.string_of_typ tnxt); + Printf.eprintf "XXX ty1_ret = %s\n" (T.string_of_typ ty1_ret); *) - ForE(pat,exp1,exp2) + blockE [ + letD id1 exp1 ; + letD nxt (dotE id1 (nameN "next") tnxt) ; + expD ( + labelE lab tyu ( + loopE ( + blockE [ + letD id1' (callE nxt [] (tupE []) ty1_ret); + expD ( + switch_optE id1 + (breakE lab (tupE []) tyu) + pat exp2 + tyu + ) + ] + ) None + ) + ) + ] + +let forE' pat exp1 exp2 = (forE pat exp1 exp2).it From 397fe7a31d50841266d99cba2238009f442a3385 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 8 Feb 2019 18:24:20 +0100 Subject: [PATCH 09/42] Bundle the kind with the con The benefit is that many passes no longer need to keep a `con_env` around, and many operations in `Type` are now always available, in partiuclar `Type.as_*_sub`, `promote` etc. The downside is that, because of the multi-pass approach in `typing.ml`, the annotation needs to be a `kind ref`. I tried using a `promise`, but it seems that certain things are run more than once in `typing` (the same has caused issues with recoverable error messages before). I am not sure if this is avoidable. If maybe the initialization can be made a bit cleaner in `typing`, then I think this will improve the life of those working on the `Ir` noticably. --- src/arrange_ir.ml | 2 +- src/arrange_type.ml | 2 +- src/async.ml | 8 +- src/check_ir.ml | 97 +++++++++--------- src/compile.ml | 27 +---- src/coverage.ml | 95 +++++++++--------- src/coverage.mli | 4 +- src/desugar.ml | 8 +- src/ir.ml | 2 +- src/syntax.ml | 4 +- src/tailcall.ml | 8 +- src/type.ml | 201 +++++++++++++++++++------------------ src/type.mli | 54 +++++----- src/typing.ml | 238 ++++++++++++++++++++++---------------------- 14 files changed, 374 insertions(+), 376 deletions(-) diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index 58b8760f23d..9ac3c6b19fe 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -71,7 +71,7 @@ and dec d = match d.it with "TypD" $$ [con c; kind k] and typ_bind (tb : typ_bind) = - Con.to_string tb.it.con $$ [typ tb.it.bound] + Con.to_string tb.it.con.Type.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 fa1b4d5271d..843961237d1 100644 --- a/src/arrange_type.ml +++ b/src/arrange_type.ml @@ -31,7 +31,7 @@ let prim p = match p with | Char -> Atom "Char" | Text -> Atom "Text" -let con c = Atom (Con.to_string c) +let con c = Atom (Con.to_string c.con) let rec typ (t:Type.typ) = match t with | Var (s, i) -> "Var" $$ [Atom s; Atom (string_of_int i)] diff --git a/src/async.ml b/src/async.ml index e91e6907cb4..dc53b466a30 100644 --- a/src/async.ml +++ b/src/async.ml @@ -175,6 +175,10 @@ and t_kind k = | T.Def(typ_binds,typ) -> T.Def(t_binds typ_binds, t_typ typ) +and t_con con = + con.kind := t_kind !(con.kind); + con + and t_operator_type ot = (* We recreate the reference here. That is ok, because it we run after type inference. Once we move async past desugaring, @@ -309,7 +313,7 @@ and t_dec' dec' = match dec' with | ExpD exp -> ExpD (t_exp exp) | TypD (con_id, k) -> - TypD (con_id, t_kind k) + TypD (t_con con_id, t_kind k) | 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) -> @@ -376,7 +380,7 @@ and t_pat' pat = AltP (t_pat pat1, t_pat pat2) and t_typ_bind' {con; bound} = - {con; bound = t_typ bound} + {con = t_con con; bound = t_typ bound} and t_typ_bind typ_bind = { typ_bind with it = t_typ_bind' typ_bind.it } diff --git a/src/check_ir.ml b/src/check_ir.ml index 95be4d11026..2ecc036059e 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -79,9 +79,9 @@ 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 ks = +let add_typs c cs = { c with - cons = List.fold_right2 Con.Env.add cs ks c.cons; + cons = List.fold_right (fun c -> Con.Env.add c.T.con (T.kind c)) cs c.cons; } let adjoin c scope = @@ -117,7 +117,7 @@ let check env at p = else error env at let check_sub env at t1 t2 = - if (T.sub env.cons t1 t2) + if T.sub t1 t2 then () else error env at "subtype violation %s %s" (T.string_of_typ t1) (T.string_of_typ t2) @@ -134,10 +134,8 @@ let rec check_typ env typ : unit = | T.Var (s,i) -> error env no_region "free type variable %s, index %i" s i | T.Con(c,typs) -> - (match Con.Env.find_opt c env.cons with - | Some (T.Def (tbs, t) | T.Abs (tbs, t)) -> + (match T.kind c with | T.Def (tbs, t) | T.Abs (tbs, t) -> check_typ_bounds env tbs typs no_region - | None -> error env no_region "unbound type constructor %s" (Con.to_string c) ) | T.Any -> () | T.Non -> () @@ -161,7 +159,7 @@ let rec check_typ env typ : unit = | _ -> let t2 = T.seq ts2 in error env no_region "promising function with non-async result type \n %s" - (T.string_of_typ_expand env'.cons t2) + (T.string_of_typ_expand t2) end; if sort = T.Sharable then begin let t1 = T.seq ts1 in @@ -171,12 +169,12 @@ let rec check_typ env typ : unit = | [T.Async t2] -> check_sub env' no_region t2 T.Shared; | _ -> error env no_region "shared function has non-async result type\n %s" - (T.string_of_typ_expand env'.cons (T.seq ts2)) + (T.string_of_typ_expand (T.seq ts2)) end | T.Opt typ -> check_typ env typ | T.Async typ -> - let t' = T.promote env.cons typ in + let t' = T.promote typ in check_sub env no_region t' T.Shared | T.Obj (sort, fields) -> let rec sorted fields = @@ -196,31 +194,30 @@ and check_typ_field env s typ_field : unit = let {T.name; T.typ} = typ_field in check_typ env typ; check env no_region - (s <> T.Actor || T.is_func (T.promote env.cons typ)) + (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 env.cons typ T.Shared) + (s = T.Object T.Local || T.sub typ T.Shared) "shared object or actor field has non-shared type" and check_typ_binds env typ_binds : T.con list * con_env = - let ts,ce = Type.open_binds env.cons typ_binds in + let ts = Type.open_binds typ_binds in let cs = List.map (function T.Con(c,[]) -> c | _ -> assert false) ts in - let ks = List.map2 (fun c t -> T.Abs ([], t)) cs ts in - let env' = add_typs env cs ks in + let env' = add_typs env cs in let _ = List.map (fun typ_bind -> let bd = T.open_ ts typ_bind.T.bound in check_typ env' bd) typ_binds in - cs, Con.Env.from_list2 cs ks + cs, Con.Env.from_list (List.map (fun c -> (c.T.con, T.kind c)) cs) and check_typ_bounds env (tbs : T.bind list) typs at : unit = match tbs, typs with | tb::tbs', typ::typs' -> check_typ env typ; - check env at (T.sub env.cons typ tb.T.bound) + check env at (T.sub typ tb.T.bound) "type argument does not match parameter bound"; check_typ_bounds env tbs' typs' at | [], [] -> () @@ -315,21 +312,21 @@ let rec check_exp env (exp:Ir.exp) : unit = | ProjE (exp1, n) -> begin check_exp env exp1; - let t1 = T.promote env.cons (immute_typ exp1) in - let ts = try T.as_tup_sub n env.cons t1 + let t1 = T.promote (immute_typ exp1) in + let ts = try T.as_tup_sub n t1 with Invalid_argument _ -> error env exp1.at "expected tuple type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) in + (T.string_of_typ_expand t1) in let tn = try List.nth ts n with | Invalid_argument _ -> error env exp.at "tuple projection %n is out of bounds for type\n %s" - n (T.string_of_typ_expand env.cons t1) in + 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 - let t2 = T.promote env.cons t in + let t2 = T.promote t in check (T.is_obj t2) "bad annotation (object type expected)"; t1 <: t2; t0 <: t; @@ -339,10 +336,10 @@ let rec check_exp env (exp:Ir.exp) : unit = check_exp env exp1; let t1 = typ exp1 in let sort, tfs = - try T.as_obj_sub n env.cons t1 with + try T.as_obj_sub n t1 with | Invalid_argument _ -> error env exp1.at "expected object type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) in check (match exp.it with | ActorDotE _ -> sort = T.Actor @@ -353,7 +350,7 @@ let rec check_exp env (exp:Ir.exp) : unit = tn <~ t | None -> error env exp1.at "field name %s does not exist in type\n %s" - n (T.string_of_typ_expand env.cons t1) + n (T.string_of_typ_expand t1) end | AssignE (exp1, exp2) -> check_exp env exp1; @@ -371,11 +368,11 @@ let rec check_exp env (exp:Ir.exp) : unit = | IdxE (exp1, exp2) -> check_exp env exp1; check_exp env exp2; - let t1 = T.promote env.cons (typ exp1) in - let t2 = try T.as_array_sub env.cons t1 with + let t1 = T.promote (typ exp1) in + let t2 = try T.as_array_sub t1 with | Invalid_argument _ -> error env exp1.at "expected array type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) in typ exp2 <: T.nat; t2 <~ t @@ -383,12 +380,12 @@ let rec check_exp env (exp:Ir.exp) : unit = check_exp env exp1; check_exp env exp2; (* TODO: check call_conv (assuming there's something to check) *) - let t1 = T.promote env.cons (typ exp1) in + let t1 = T.promote (typ exp1) in let tbs, t2, t3 = - try T.as_func_sub (List.length insts) env.cons t1 with + try T.as_func_sub (List.length insts) t1 with | Invalid_argument _ -> error env exp1.at "expected function type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) in check_inst_bounds env tbs insts exp.at; check_exp env exp2; @@ -396,9 +393,8 @@ let rec check_exp env (exp:Ir.exp) : unit = T.open_ insts t3 <: t; | BlockE (decs, t0) -> let t1, scope = type_block env decs exp.at in - let env' = adjoin env scope in check_typ env t0; - check (T.eq env.cons t T.unit || T.eq env'.cons t1 t0) "unexpected expected block type"; + check (T.eq t T.unit || T.eq t1 t0) "unexpected expected block type"; t0 <: t; | IfE (exp1, exp2, exp3) -> check_exp env exp1; @@ -409,7 +405,7 @@ let rec check_exp env (exp:Ir.exp) : unit = typ exp3 <: t; | SwitchE (exp1, cases) -> check_exp env exp1; - let t1 = T.promote env.cons (typ exp1) in + let t1 = T.promote (typ exp1) in (* if not env.pre then if not (Coverage.check_cases env.cons cases t1) then warn env exp.at "the cases in this switch do not cover all possible values"; @@ -434,13 +430,13 @@ let rec check_exp env (exp:Ir.exp) : unit = | ForE (pat, exp1, exp2) -> begin check_exp env exp1; - let t1 = T.promote env.cons (typ exp1) in + let t1 = T.promote (typ exp1) in try - let _, tfs = T.as_obj_sub "next" env.cons t1 in + let _, tfs = T.as_obj_sub "next" t1 in let t0 = T.lookup_field "next" tfs in - let t1, t2 = T.as_mono_func_sub env.cons t0 in + let t1, t2 = T.as_mono_func_sub t0 in T.unit <: t1; - let t2' = T.as_opt_sub env.cons t2 in + let t2' = T.as_opt_sub t2 in let ve = check_pat_exhaustive env pat in pat.note <: t2'; check_exp (adjoin_vals env ve) exp2; @@ -448,7 +444,7 @@ let rec check_exp env (exp:Ir.exp) : unit = T.unit <: t with Invalid_argument _ -> error env exp1.at "expected iterable type, but expression has type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) end; | LabelE (id, t0, exp1) -> assert (t0 <> T.Pre); @@ -487,11 +483,11 @@ let rec check_exp env (exp:Ir.exp) : unit = | AwaitE exp1 -> check env.async "misplaced await"; check_exp env exp1; - let t1 = T.promote env.cons (typ exp1) in - let t2 = try T.as_async_sub env.cons t1 + let t1 = T.promote (typ exp1) in + let t2 = try T.as_async_sub t1 with Invalid_argument _ -> error env exp1.at "expected async type, but expression has type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) in t2 <: t; | AssertE exp1 -> @@ -527,7 +523,7 @@ let rec check_exp env (exp:Ir.exp) : unit = {T.name = Syntax.string_of_name name.it; T.typ = T.Env.find id.it env.vals}) labids)) in - let t2 = T.promote env.cons t in + let t2 = T.promote t in check (T.is_obj t2) "bad annotation (object type expected)"; t1 <: t2; t0 <: t; @@ -541,7 +537,7 @@ and check_case env t_pat t {it = {pat; exp}; _} = let ve = check_pat env pat in check_sub env pat.at pat.note t_pat; check_exp (adjoin_vals env ve) exp; - if not (T.sub env.cons (typ exp) t) then + if not (T.sub (typ exp) t) then error env exp.at "bad case" (* Patterns *) @@ -656,7 +652,7 @@ and type_exp_field env s (tfs, ve) field : T.field list * val_env = "public actor field is not a function"; check env field.at (if (s <> T.Object T.Local && priv.it = Syntax.Public) - then T.sub env.cons t T.Shared + then T.sub t T.Shared else true) "public shared object or actor field has non-shared type"; let ve' = T.Env.add id.it t ve in @@ -694,14 +690,13 @@ and cons_of_typ_binds typ_binds = and check_open_typ_binds env typ_binds = 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 ce = List.fold_right (fun c -> Con.Env.add c.Type.con (Type.kind c)) cs Con.Env.empty 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 + List.map (fun {con; bound} -> {Type.var = Con.name con.T.con; bound = Type.close cs bound}) tbs and check_dec env dec = (* helpers *) @@ -756,7 +751,7 @@ and check_block_exps env t decs at = check_sub env at T.unit t | [dec] -> check_dec env dec; - check env at (T.is_unit t || T.sub env.cons (typ dec) t) + check env at (T.is_unit t || T.sub (typ dec) t) "declaration does not produce expect type" | dec::decs' -> check_dec env dec; @@ -796,15 +791,15 @@ and gather_dec env scope dec : scope = | _ -> 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 tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; 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, k) -> check env dec.at - (not (Con.Env.mem c scope.con_env)) + (not (Con.Env.mem c.T.con scope.con_env)) "duplicate definition of type in block"; - let ce' = Con.Env.add c k scope.con_env in + let ce' = Con.Env.add c.T.con k scope.con_env in {scope with con_env = ce'} (* Programs *) diff --git a/src/compile.ml b/src/compile.ml index 94601a684f0..1754cd8b109 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -155,7 +155,6 @@ module E = struct (* Immutable *) local_vars_env : t varloc NameEnv.t; (* variables ↦ their location *) - con_env : Type.con_env; (* Mutable *) func_types : func_type list ref; @@ -187,7 +186,6 @@ module E = struct mode; prelude; local_vars_env = NameEnv.empty; - con_env = Con.Env.empty; func_types = ref []; imports = ref []; exports = ref []; @@ -229,21 +227,6 @@ module E = struct let mode (env : t) = env.mode - let con_env (env : t) = env.con_env - - let add_con (env : t) c k = - { env with con_env = Con.Env.add c k env.con_env } - - let add_typ_binds (env : t) typ_binds = - (* There is some code duplication with Check_ir.check_open_typ_binds. - 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.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 } - let lookup_var env var = match NameEnv.find_opt var env.local_vars_env with | Some l -> Some l @@ -1323,7 +1306,7 @@ module Object = struct (* Determines whether the field is mutable (and thus needs an indirection) *) let is_mut_field env obj_type ({it = Syntax.Name s; _}) = - let _, fields = Type.as_obj_sub "" (E.con_env env) obj_type in + let _, fields = Type.as_obj_sub "" obj_type in let field_typ = Type.lookup_field s fields in let mut = Type.is_mut field_typ in mut @@ -3751,8 +3734,7 @@ and compile_dec pre_env how dec : E.t * G.t * (E.t -> (SR.t * G.t)) = (fun (sr, code) -> (sr, G.with_region dec.at code)) (mk_code env))) @@ match dec.it with | TypD (c,k) -> - let pre_env1 = E.add_con pre_env c k in - (pre_env1, G.nop, fun _ -> SR.unit, G.nop) + (pre_env, G.nop, fun _ -> SR.unit, G.nop) | ExpD e ->(pre_env, G.nop, fun env -> compile_exp env e) | LetD (p, e) -> let (pre_env1, alloc_code, pat_arity, fill_code) = compile_n_ary_pat pre_env how p in @@ -3779,9 +3761,8 @@ and compile_dec pre_env how dec : E.t * G.t * (E.t -> (SR.t * G.t)) = let (pre_env1, alloc_code, mk_code) = FuncDec.dec pre_env how name cc captured mk_pat mk_body dec.at in (pre_env1, alloc_code, fun env -> (* Bring type parameters into scope *) - let env1 = E.add_typ_binds env typ_binds in - let sr, code = Var.get_val env1 name.it in - sr, mk_code env1 ^^ code + let sr, code = Var.get_val env name.it in + sr, mk_code env ^^ code ) and compile_decs env decs : SR.t * G.t = diff --git a/src/coverage.ml b/src/coverage.ml index 16d2a2ff54a..3a278091253 100644 --- a/src/coverage.ml +++ b/src/coverage.ml @@ -55,92 +55,92 @@ let skip_pat pat sets = sets.alts <- AtSet.add pat.at sets.alts; true -let rec match_pat ce ctxt desc pat t sets = - Type.span ce t = Some 0 && skip_pat pat sets || +let rec match_pat ctxt desc pat t sets = + Type.span t = Some 0 && skip_pat pat sets || match pat.it with | WildP | VarP _ -> - succeed ce ctxt desc sets + succeed ctxt desc sets | LitP lit -> - match_lit ce ctxt desc (value_of_lit !lit) t sets + match_lit ctxt desc (value_of_lit !lit) t sets | SignP (op, lit) -> let f = Operator.unop pat.note op in - match_lit ce ctxt desc (f (value_of_lit !lit)) t sets + match_lit ctxt desc (f (value_of_lit !lit)) t sets | TupP pats -> - let ts = Type.as_tup (Type.promote ce t) in + let ts = Type.as_tup (Type.promote t) in let descs = match desc with | Tup descs -> descs | Any -> List.map (fun _ -> Any) pats | _ -> assert false - in match_tup ce ctxt [] descs pats ts sets + in match_tup ctxt [] descs pats ts sets | OptP pat1 -> - let t' = Type.as_opt (Type.promote ce t) in + let t' = Type.as_opt (Type.promote t) in (match desc with | Val Value.Null -> - fail ce ctxt desc sets + fail ctxt desc sets | NotVal vs when ValSet.mem Value.Null vs -> - match_pat ce (InOpt ctxt) Any pat1 t' sets + match_pat (InOpt ctxt) Any pat1 t' sets | Opt desc' -> - match_pat ce (InOpt ctxt) desc' pat1 t' sets + match_pat (InOpt ctxt) desc' pat1 t' sets | Any -> - fail ce ctxt (Val Value.Null) sets && - match_pat ce (InOpt ctxt) Any pat1 t' sets + fail ctxt (Val Value.Null) sets && + match_pat (InOpt ctxt) Any pat1 t' sets | _ -> assert false ) | AltP (pat1, pat2) -> sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts); - match_pat ce (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets + match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets | AnnotP (pat1, _) -> - match_pat ce ctxt desc pat1 t sets + match_pat ctxt desc pat1 t sets -and match_lit ce ctxt desc v t sets = +and match_lit ctxt desc v t sets = let desc_succ = Val v in let desc_fail vs = NotVal (ValSet.add v vs) in match desc with | Any -> - if Type.span ce t = Some 1 then - succeed ce ctxt desc_succ sets + if Type.span t = Some 1 then + succeed ctxt desc_succ sets else - succeed ce ctxt desc_succ sets && - fail ce ctxt (desc_fail ValSet.empty) sets + succeed ctxt desc_succ sets && + fail ctxt (desc_fail ValSet.empty) sets | Val v' -> if Value.equal v v' - then succeed ce ctxt desc sets - else fail ce ctxt desc sets + then succeed ctxt desc sets + else fail ctxt desc sets | NotVal vs -> if ValSet.mem v vs then - fail ce ctxt desc sets - else if Type.span ce t = Some (ValSet.cardinal vs + 1) then - succeed ce ctxt desc_succ sets + fail ctxt desc sets + else if Type.span t = Some (ValSet.cardinal vs + 1) then + succeed ctxt desc_succ sets else - succeed ce ctxt desc_succ sets && fail ce ctxt (desc_fail vs) sets + succeed ctxt desc_succ sets && fail ctxt (desc_fail vs) sets | Opt _ -> - fail ce ctxt desc sets + fail ctxt desc sets | _ -> assert false -and match_tup ce ctxt descs_r descs pats ts sets = +and match_tup ctxt descs_r descs pats ts sets = match descs, pats, ts with | [], [], [] -> - succeed ce ctxt (Tup (List.rev descs_r)) sets + succeed ctxt (Tup (List.rev descs_r)) sets | desc::descs', pat::pats', t::ts' -> - match_pat ce (InTup (ctxt, descs_r, descs', pats', ts')) desc pat t sets + match_pat (InTup (ctxt, descs_r, descs', pats', ts')) desc pat t sets | _ -> assert false -and succeed ce ctxt desc sets : bool = +and succeed ctxt desc sets : bool = match ctxt with | InOpt ctxt' -> - succeed ce ctxt' (Opt desc) sets + succeed ctxt' (Opt desc) sets | InTup (ctxt', descs_r, descs, pats, ts) -> - match_tup ce ctxt' (desc::descs_r) descs pats ts sets + match_tup ctxt' (desc::descs_r) descs pats ts sets | InAlt1 (ctxt', at1, _pat2, _t) -> sets.reached_alts <- AtSet.add at1 sets.reached_alts; - succeed ce ctxt' desc sets + succeed ctxt' desc sets | InAlt2 (ctxt', at2) -> sets.reached_alts <- AtSet.add at2 sets.reached_alts; - succeed ce ctxt' desc sets + succeed ctxt' desc sets | InCase (at, cases, _t) -> sets.reached_cases <- AtSet.add at sets.reached_cases; skip cases sets @@ -153,21 +153,21 @@ and skip cases sets : bool = sets.cases <- AtSet.add case.at sets.cases; skip cases' sets -and fail ce ctxt desc sets : bool = +and fail ctxt desc sets : bool = match ctxt with | InOpt ctxt' -> - fail ce ctxt' (Opt desc) sets + fail ctxt' (Opt desc) sets | InTup (ctxt', descs', descs, pats, _ts) -> - fail ce ctxt' (Tup (List.rev descs' @ [desc] @ descs)) sets + fail ctxt' (Tup (List.rev descs' @ [desc] @ descs)) sets | InAlt1 (ctxt', at1, pat2, t) -> - match_pat ce (InAlt2 (ctxt', pat2.at)) desc pat2 t sets + match_pat (InAlt2 (ctxt', pat2.at)) desc pat2 t sets | InAlt2 (ctxt', at2) -> - fail ce ctxt' desc sets + fail ctxt' desc sets | InCase (at, [], t) -> - Type.span ce t = Some 0 + Type.span t = Some 0 | InCase (at, case::cases, t) -> - Type.span ce t = Some 0 && skip (case::cases) sets || - match_pat ce (InCase (case.at, cases, t)) desc case.it.pat t sets + Type.span t = Some 0 && skip (case::cases) sets || + match_pat (InCase (case.at, cases, t)) desc case.it.pat t sets let warn at fmt = @@ -176,9 +176,9 @@ let warn at fmt = Printf.eprintf "%s: warning, %s\n%!" (Source.string_of_region at) s; ) fmt -let check_cases ce cases t : bool = +let check_cases cases t : bool = let sets = make_sets () in - let exhaustive = fail ce (InCase (Source.no_region, cases, t)) Any sets in + let exhaustive = fail (InCase (Source.no_region, cases, t)) Any sets in let unreached_cases = AtSet.diff sets.cases sets.reached_cases in let unreached_alts = AtSet.diff sets.alts sets.reached_alts in AtSet.iter (fun at -> warn at "this case is never reached") unreached_cases; @@ -188,6 +188,5 @@ let check_cases ce cases t : bool = let (@?) it at = {it; at; note = empty_typ_note} -let check_pat ce pat t : bool = - check_cases ce - [{pat; exp = TupE [] @? Source.no_region} @@ Source.no_region] t +let check_pat pat t : bool = + check_cases [{pat; exp = TupE [] @? Source.no_region} @@ Source.no_region] t diff --git a/src/coverage.mli b/src/coverage.mli index 60862fb0b49..b0833624403 100644 --- a/src/coverage.mli +++ b/src/coverage.mli @@ -1,2 +1,2 @@ -val check_pat : Type.con_env -> Syntax.pat -> Type.typ -> bool -val check_cases : Type.con_env -> Syntax.case list -> Type.typ -> bool +val check_pat : Syntax.pat -> Type.typ -> bool +val check_cases : Syntax.case list -> Type.typ -> bool diff --git a/src/desugar.ml b/src/desugar.ml index becb43e73a9..0f3a967b584 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -143,8 +143,8 @@ and decs ds = | d::ds -> match d.it with | S.ClassD(_, con_id, _, _, _, _, _) -> - let (c,k) = match con_id.note with Some p -> p | _ -> assert false in - let typD = { it = I.TypD (c,k); + let c = Lib.Option.value con_id.note in + let typD = { it = I.TypD (c,T.kind c); at = d.at; note = { S.note_typ = T.unit; S.note_eff = T.Triv } @@ -161,8 +161,8 @@ and dec' at n d = match d with let cc = Value.call_conv_of_typ n.S.note_typ in I.FuncD (cc, i, typ_binds tbs, pat p, ty.note, exp e) | S.TypD (con_id, typ_bind, t) -> - let (c,k) = Lib.Option.value con_id.note in - I.TypD (c,k) + let c = Lib.Option.value con_id.note in + I.TypD (c,T.kind c) | S.ClassD (fun_id, typ_id, tbs, s, p, self_id, es) -> let cc = Value.call_conv_of_typ n.S.note_typ in let inst = List.map diff --git a/src/ir.ml b/src/ir.ml index 55b1aca6e63..bbd6671e7ce 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 -and typ_bind' = {con : Con.t; bound : Type.typ} +type typ_bind' = {con : Type.con; bound : Type.typ} type typ_bind = typ_bind' Source.phrase type pat = (pat', Type.typ) Source.annotated_phrase diff --git a/src/syntax.ml b/src/syntax.ml index 01fa40b3ad1..a6060832601 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -7,7 +7,7 @@ let empty_typ_note = {note_typ = Type.Pre; note_eff = Type.Triv} (* Identifiers *) type id = string Source.phrase -type con_id = (string, (Type.con * Type.kind) option) Source.annotated_phrase +type con_id = (string, Type.con option) Source.annotated_phrase (* Names (not alpha-convertible), used for field and class names *) type name = name' Source.phrase @@ -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', Con.t option) Source.annotated_phrase +and typ_bind = (typ_bind', Type.con option) Source.annotated_phrase and typ_bind' = {var : id; bound : typ} diff --git a/src/tailcall.ml b/src/tailcall.ml index 00adecd6305..c242354f7de 100644 --- a/src/tailcall.ml +++ b/src/tailcall.ml @@ -62,10 +62,10 @@ let bind env i (info:func_info option) : env = | _ -> env (* preserve existing, non-shadowed info *) -let are_generic_insts tbs insts = - List.for_all2 (fun tb inst -> +let are_generic_insts (tbs : typ_bind list) insts = + List.for_all2 (fun (tb : typ_bind) inst -> match inst with - | Con(c2,[]) -> tb.it.con = c2 (* conservative, but safe *) + | Con(c2,[]) -> tb.it.con.Type.con = c2.Type.con (* 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.con, [])) tbs in + let cs = List.map (fun (tb : typ_bind) -> 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 33bb6a837f4..b0cbb4c18c9 100644 --- a/src/type.ml +++ b/src/type.ml @@ -1,6 +1,5 @@ (* Representation *) -type con = Con.t type control = Returns | Promises (* Returns a computed value or immediate promise *) type sharing = Local | Sharable type obj_sort = Object of sharing | Actor @@ -37,17 +36,26 @@ and typ = | Non (* bottom *) | Pre (* pre-type *) +and con = { con : Con.t; kind : kind ref } + and bind = {var : string; bound : typ} and field = {name : string; typ : typ} +and kind = + | Def of bind list * typ + | Abs of bind list * typ + +(* cons *) + +(* the promise is only there to break the recursion in open_bind *) +let kind con = !(con.kind) + +let fresh_con n = { con = Con.fresh n; kind = ref (Abs ([],Pre)) } + (* field ordering *) let compare_field {name=n;_} {name=m;_} = compare n m -type kind = - | Def of bind list * typ - | Abs of bind list * typ - type con_env = kind Con.Env.t let seq ts = @@ -135,7 +143,7 @@ let rec subst sigma t = | Prim _ | Var _ -> t | Con (c, ts) -> - (match Con.Env.find_opt c sigma with + (match Con.Env.find_opt c.con sigma with | Some t -> assert (List.length ts = 0); t | None -> Con (c, List.map (subst sigma) ts) ) @@ -165,8 +173,9 @@ and subst_field sigma {name; typ} = let close cs t = if cs = [] then t else - let ts = List.mapi (fun i c -> Var (Con.name c, i)) cs in - let sigma = List.fold_right2 Con.Env.add cs ts Con.Env.empty in + let bare_cons = List.map (fun c -> c.con) cs in + let ts = List.mapi (fun i c -> Var (Con.name c, i)) bare_cons in + let sigma = List.fold_right2 Con.Env.add bare_cons ts Con.Env.empty in subst sigma t let close_binds cs tbs = @@ -203,12 +212,14 @@ let open_ ts t = if ts = [] then t else open' 0 ts t -let open_binds env tbs = - if tbs = [] then [], env else +let open_binds tbs = + if tbs = [] then [] else let cs = List.map (fun {var; _} -> Con.fresh var) tbs in - let ts = List.map (fun c -> Con (c, [])) cs in + let ps = List.map (fun _ -> ref (Abs ([],Pre))) tbs in + let ts = List.map2 (fun con kind-> Con ({con;kind}, [])) cs ps in let ks = List.map (fun {bound; _} -> Abs ([], open_ ts bound)) tbs in - ts, List.fold_right2 Con.Env.add cs ks env + List.iter2 (fun p k -> p := k) ps ks; + ts (* Normalization and Classification *) @@ -217,21 +228,19 @@ let reduce tbs t ts = assert (List.length ts = List.length tbs); open_ ts t -let rec normalize env = function +let rec normalize = function | Con (con, ts) as t -> - (match Con.Env.find_opt con env with - | Some (Def (tbs, t)) -> normalize env (reduce tbs t ts) - | Some _ -> t - | None -> assert false + (match kind con with + | Def (tbs, t) -> normalize (reduce tbs t ts) + | _ -> t ) - | Mut t -> Mut (normalize env t) + | Mut t -> Mut (normalize t) | t -> t -let rec promote env = function +let rec promote = function | Con (con, ts) -> - (match Con.Env.find_opt con env with - | Some (Def (tbs, t) | Abs (tbs, t)) -> promote env (reduce tbs t ts) - | None -> assert false + (match kind con with + | Def (tbs, t) | Abs (tbs, t) -> promote (reduce tbs t ts) ) | t -> t @@ -263,43 +272,43 @@ let as_async = function Async t -> t | _ -> invalid "as_async" let as_mut = function Mut t -> t | _ -> invalid "as_mut" let as_immut = function Mut t -> t | t -> t -let as_prim_sub p env t = match promote env t with +let as_prim_sub p t = match promote t with | Prim p' when p = p' -> () | Non -> () | _ -> invalid "as_prim_sub" -let rec as_obj_sub name env t = match promote env t with +let rec as_obj_sub name t = match promote t with | Obj (s, tfs) -> s, tfs - | Array t -> as_obj_sub name env (array_obj t) + | Array t -> as_obj_sub name (array_obj t) | Non -> Object Sharable, [{name; typ = Non}] | _ -> invalid "as_obj_sub" -let as_array_sub env t = match promote env t with +let as_array_sub t = match promote t with | Array t -> t | Non -> Non | _ -> invalid "as_array_sub" -let as_opt_sub env t = match promote env t with +let as_opt_sub t = match promote t with | Opt t -> t | _ -> invalid "as_opt_sub" -let as_tup_sub n env t = match promote env t with +let as_tup_sub n t = match promote t with | Tup ts -> ts | Non -> Lib.List.make n Non | _ -> invalid "as_tup_sub" -let as_unit_sub env t = match promote env t with +let as_unit_sub t = match promote t with | Tup [] | Non -> () | _ -> invalid "as_unit_sub" -let as_pair_sub env t = match promote env t with +let as_pair_sub t = match promote t with | Tup [t1; t2] -> t1, t2 | Non -> Non, Non | _ -> invalid "as_pair_sub" -let as_func_sub n env t = match promote env t with +let as_func_sub n t = match promote t with | Func (_, _, tbs, ts1, ts2) -> tbs, seq ts1, seq ts2 | Non -> Lib.List.make n {var = "X"; bound = Any}, Any, Non | _ -> invalid "as_func_sub" -let as_mono_func_sub env t = match promote env t with +let as_mono_func_sub t = match promote t with | Func (_, _, [], ts1, ts2) -> seq ts1, seq ts2 | Non -> Any, Non | _ -> invalid "as_func_sub" -let as_async_sub env t = match promote env t with +let as_async_sub t = match promote t with | Async t -> t | Non -> Non | _ -> invalid "as_async_sub" @@ -312,9 +321,9 @@ let lookup_field name' tfs = (* Span *) -let rec span env = function +let rec span = function | Var _ | Pre -> assert false - | Con _ as t -> span env (promote env t) + | Con _ as t -> span (promote t) | Prim Null -> Some 1 | Prim Bool -> Some 2 | Prim (Nat | Int | Float | Text) -> None @@ -324,7 +333,7 @@ let rec span env = function | Obj _ | Tup _ | Async _ -> Some 1 | Array _ | Func _ | Shared | Any -> None | Opt _ -> Some 2 - | Mut t -> span env t + | Mut t -> span t | Non -> Some 0 @@ -335,14 +344,14 @@ exception Unavoidable of con let rec avoid' env env' = function | (Prim _ | Var _ | Any | Non | Shared | Pre) as t -> t | Con (c, ts) -> - (match Con.Env.find_opt c env' with + (match Con.Env.find_opt c.con env' with | Some (Abs _) -> raise (Unavoidable c) | Some (Def (tbs, t)) -> avoid' env env' (reduce tbs t ts) | None -> try Con (c, List.map (avoid' env env') ts) with Unavoidable _ -> - match Con.Env.find c env with + match Con.Env.find c.con env with | Abs _ -> raise (Unavoidable c) | Def (tbs, t) -> avoid' env env' (reduce tbs t ts) ) @@ -373,11 +382,11 @@ let avoid env env' t = module S = Set.Make (struct type t = typ * typ let compare = compare end) -let rel_list p env rel eq xs1 xs2 = - try List.for_all2 (p env rel eq) xs1 xs2 with Invalid_argument _ -> false +let rel_list p rel eq xs1 xs2 = + try List.for_all2 (p rel eq) xs1 xs2 with Invalid_argument _ -> false let str = ref (fun _ -> failwith "") -let rec rel_typ env rel eq t1 t2 = +let rec rel_typ rel eq t1 t2 = (*Printf.printf "[sub] %s == %s\n%!" (!str t1) (!str t2);*) t1 == t2 || S.mem (t1, t2) !rel || begin rel := S.add (t1, t2) !rel; @@ -391,30 +400,30 @@ let rec rel_typ env rel eq t1 t2 = | Non, _ when rel != eq -> true | Con (con1, ts1), Con (con2, ts2) -> - (match Con.Env.find con1 env, Con.Env.find con2 env with + (match kind con1, kind con2 with | Def (tbs, t), _ -> (* TBR this may fail to terminate *) - rel_typ env rel eq (open_ ts1 t) t2 + rel_typ rel eq (open_ ts1 t) t2 | _, Def (tbs, t) -> (* TBR this may fail to terminate *) - rel_typ env rel eq t1 (open_ ts2 t) + rel_typ rel eq t1 (open_ ts2 t) | _ when con1 = con2 -> - rel_list eq_typ env rel eq ts1 ts2 + rel_list eq_typ rel eq ts1 ts2 | Abs (tbs, t), _ when rel != eq -> - rel_typ env rel eq (open_ ts1 t) t2 + rel_typ rel eq (open_ ts1 t) t2 | _ -> false ) | Con (con1, ts1), t2 -> - (match Con.Env.find con1 env, t2 with + (match kind con1, t2 with | Def (tbs, t), _ -> (* TBR this may fail to terminate *) - rel_typ env rel eq (open_ ts1 t) t2 + rel_typ rel eq (open_ ts1 t) t2 | Abs (tbs, t), _ when rel != eq -> - rel_typ env rel eq (open_ ts1 t) t2 + rel_typ rel eq (open_ ts1 t) t2 | _ -> false ) | t1, Con (con2, ts2) -> - (match Con.Env.find con2 env with + (match kind con2 with | Def (tbs, t) -> (* TBR this may fail to terminate *) - rel_typ env rel eq t1 (open_ ts2 t) + rel_typ rel eq t1 (open_ ts2 t) | _ -> false ) | Prim p1, Prim p2 when p1 = p2 -> @@ -425,31 +434,31 @@ let rec rel_typ env rel eq t1 t2 = true | Obj (s1, tfs1), Obj (s2, tfs2) -> s1 = s2 && - rel_fields env rel eq tfs1 tfs2 + rel_fields rel eq tfs1 tfs2 | Obj (s, _), Shared when rel != eq -> s != Object Local | Array t1', Array t2' -> - rel_typ env rel eq t1' t2' + rel_typ rel eq t1' t2' | Array t1', Obj _ when rel != eq -> - rel_typ env rel eq (array_obj t1') t2 + rel_typ rel eq (array_obj t1') t2 | Array t, Shared when rel != eq -> - rel_typ env rel eq t Shared + rel_typ rel eq t Shared | Opt t1', Opt t2' -> - rel_typ env rel eq t1' t2' + rel_typ rel eq t1' t2' | Opt t1', Shared -> - rel_typ env rel eq t1' Shared + rel_typ rel eq t1' Shared | Prim Null, Opt t2' when rel != eq -> true | Tup ts1, Tup ts2 -> - rel_list rel_typ env rel eq ts1 ts2 + rel_list rel_typ rel eq ts1 ts2 | Tup ts1, Shared -> - rel_list rel_typ env rel eq ts1 (List.map (fun _ -> Shared) ts1) + rel_list rel_typ rel eq ts1 (List.map (fun _ -> Shared) ts1) | Func (s1, c1, tbs1, t11, t12), Func (s2, c2, tbs2, t21, t22) -> c1 = c2 && s1 = s2 && - (match rel_binds env rel eq tbs1 tbs2 with - | Some (ts, env') -> - rel_list rel_typ env' rel eq (List.map (open_ ts) t21) (List.map (open_ ts) t11) && - rel_list rel_typ env' rel eq (List.map (open_ ts) t12) (List.map (open_ ts) t22) + (match rel_binds rel eq tbs1 tbs2 with + | Some ts -> + rel_list rel_typ rel eq (List.map (open_ ts) t21) (List.map (open_ ts) t11) && + rel_list rel_typ rel eq (List.map (open_ ts) t12) (List.map (open_ ts) t22) | None -> false ) | Func (Sharable, _, _, _, _), Shared when rel != eq -> @@ -457,13 +466,13 @@ let rec rel_typ env rel eq t1 t2 = | Shared, Shared -> true | Async t1', Async t2' -> - rel_typ env rel eq t1' t2' + rel_typ rel eq t1' t2' | Mut t1', Mut t2' -> - eq_typ env rel eq t1' t2' + eq_typ rel eq t1' t2' | _, _ -> false end -and rel_fields env rel eq tfs1 tfs2 = +and rel_fields rel eq tfs1 tfs2 = (* Assume that tf1 and tf2 are sorted. *) match tfs1, tfs2 with | [], [] -> @@ -473,37 +482,37 @@ and rel_fields env rel eq tfs1 tfs2 = | tf1::tfs1', tf2::tfs2' -> (match compare_field tf1 tf2 with | 0 -> - rel_typ env rel eq tf1.typ tf2.typ && - rel_fields env rel eq tfs1' tfs2' + rel_typ rel eq tf1.typ tf2.typ && + rel_fields rel eq tfs1' tfs2' | -1 when rel != eq -> - rel_fields env rel eq tfs1' tfs2 + rel_fields rel eq tfs1' tfs2 | _ -> false ) | _, _ -> false -and rel_binds env rel eq tbs1 tbs2 = - let ts, env' = open_binds env tbs2 in - if rel_list (rel_bind ts) env' rel eq tbs2 tbs1 - then Some (ts, env') +and rel_binds rel eq tbs1 tbs2 = + let ts = open_binds tbs2 in + if rel_list (rel_bind ts) rel eq tbs2 tbs1 + then Some ts else None -and rel_bind ts env rel eq tb1 tb2 = - rel_typ env rel eq (open_ ts tb1.bound) (open_ ts tb2.bound) +and rel_bind ts rel eq tb1 tb2 = + rel_typ rel eq (open_ ts tb1.bound) (open_ ts tb2.bound) -and eq_typ env rel eq t1 t2 = rel_typ env eq eq t1 t2 +and eq_typ rel eq t1 t2 = rel_typ eq eq t1 t2 -and eq (env : con_env) t1 t2 : bool = - let eq = ref S.empty in eq_typ env eq eq t1 t2 -and sub (env : con_env) t1 t2 : bool = - rel_typ env (ref S.empty) (ref S.empty) t1 t2 +and eq t1 t2 : bool = + let eq = ref S.empty in eq_typ eq eq t1 t2 +and sub t1 t2 : bool = + rel_typ (ref S.empty) (ref S.empty) t1 t2 (* Least upper bound and greatest lower bound *) -let rec lub env t1 t2 = +let rec lub t1 t2 = if t1 == t2 then t1 else (* TBR: this is just a quick hack *) - match normalize env t1, normalize env t2 with + match normalize t1, normalize t2 with | _, Pre | Pre, _ -> Pre | _, Any @@ -512,19 +521,19 @@ let rec lub env t1 t2 = | Non, _ -> t2 | Prim Nat, Prim Int | Prim Int, Prim Nat -> Prim Int - | Opt t1', Opt t2' -> Opt (lub env t1' t2') + | Opt t1', Opt t2' -> Opt (lub t1' t2') | Prim Null, Opt t' | Opt t', Prim Null -> Opt t' - | Array t1', (Obj _ as t2) -> lub env (array_obj t1') t2 - | (Obj _ as t1), Array t2' -> lub env t1 (array_obj t2') - | t1', t2' when eq env t1' t2' -> t1 + | Array t1', (Obj _ as t2) -> lub (array_obj t1') t2 + | (Obj _ as t1), Array t2' -> lub t1 (array_obj t2') + | t1', t2' when eq t1' t2' -> t1 | _ -> Any -let rec glb env t1 t2 = +let rec glb t1 t2 = if t1 == t2 then t1 else (* TBR: this is just a quick hack *) - match normalize env t1, normalize env t2 with + match normalize t1, normalize t2 with | _, Pre | Pre, _ -> Pre | _, Any -> t1 @@ -533,10 +542,10 @@ let rec glb env t1 t2 = | Non, _ -> Non | Prim Nat, Prim Int | Prim Int, Prim Nat -> Prim Nat - | Opt t1', Opt t2' -> Opt (glb env t1' t2') + | Opt t1', Opt t2' -> Opt (glb t1' t2') | Prim Null, Opt _ | Opt _, Prim Null -> Prim Null - | t1', t2' when eq env t1' t2' -> t1 + | t1', t2' when eq t1' t2' -> t1 | _ -> Non @@ -575,9 +584,9 @@ let rec string_of_typ_nullary vs = function | Shared -> "Shared" | Prim p -> string_of_prim p | Var (s, i) -> (try string_of_var (List.nth vs i) with _ -> assert false) - | Con (c, []) -> string_of_con vs c + | Con (c, []) -> string_of_con vs c.con | Con (c, ts) -> - sprintf "%s<%s>" (string_of_con vs c) + sprintf "%s<%s>" (string_of_con vs c.con) (String.concat ", " (List.map (string_of_typ' vs) ts)) | Tup ts -> sprintf "(%s%s)" @@ -669,16 +678,16 @@ let string_of_kind k = sprintf "%s %s%s" op sbs st -let rec string_of_typ_expand env t = +let rec string_of_typ_expand t = let s = string_of_typ t in match t with | Con (c, ts) -> - (match Con.Env.find c env with + (match kind c with | Abs _ -> s | Def _ -> - match normalize env t with + match normalize t with | Prim _ | Any | Non -> s - | t' -> s ^ " = " ^ string_of_typ_expand env t' + | t' -> s ^ " = " ^ string_of_typ_expand t' ) | _ -> s diff --git a/src/type.mli b/src/type.mli index 884ac714070..11ca503d8c6 100644 --- a/src/type.mli +++ b/src/type.mli @@ -1,6 +1,5 @@ (* Representation *) -type con = Con.t type control = Returns | Promises (* returns a computed value or immediate promise *) type sharing = Local | Sharable type obj_sort = Object of sharing | Actor @@ -40,16 +39,23 @@ and typ = and bind = {var : string; bound : typ} and field = {name : string; typ : typ} -(* field ordering *) - -val compare_field : field -> field -> int +(* cons and kinds *) -type kind = +and con = { con : Con.t; kind : kind ref } +and kind = | Def of bind list * typ | Abs of bind list * typ type con_env = kind Con.Env.t +val kind : con -> kind +val fresh_con : string -> con + +(* field ordering *) + +val compare_field : field -> field -> int + + (* n-ary argument/result sequences *) val seq: typ list -> typ @@ -91,26 +97,26 @@ val as_async : typ -> typ val as_mut : typ -> typ val as_immut : typ -> typ -val as_prim_sub : prim -> con_env -> typ -> unit -val as_obj_sub : string -> con_env -> typ -> obj_sort * field list -val as_array_sub : con_env -> typ -> typ -val as_opt_sub : con_env -> typ -> typ -val as_tup_sub : int -> con_env -> typ -> typ list -val as_unit_sub : con_env -> typ -> unit -val as_pair_sub : con_env -> typ -> typ * typ -val as_func_sub : int -> con_env -> typ -> bind list * typ * typ -val as_mono_func_sub : con_env -> typ -> typ * typ -val as_async_sub : con_env -> typ -> typ +val as_prim_sub : prim -> typ -> unit +val as_obj_sub : string -> typ -> obj_sort * field list +val as_array_sub : typ -> typ +val as_opt_sub : typ -> typ +val as_tup_sub : int -> typ -> typ list +val as_unit_sub : typ -> unit +val as_pair_sub : typ -> typ * typ +val as_func_sub : int -> typ -> bind list * typ * typ +val as_mono_func_sub : typ -> typ * typ +val as_async_sub : typ -> typ val lookup_field : string -> field list -> typ -val span : con_env -> typ -> int option +val span : typ -> int option (* Normalization and Classification *) -val normalize : con_env -> typ -> typ -val promote : con_env -> typ -> typ +val normalize : typ -> typ +val promote : typ -> typ exception Unavoidable of con val avoid : con_env -> con_env -> typ -> typ (* raise Unavoidable *) @@ -118,11 +124,11 @@ val avoid : con_env -> con_env -> typ -> typ (* raise Unavoidable *) (* Equivalence and Subtyping *) -val eq : con_env -> typ -> typ -> bool -val sub : con_env -> typ -> typ -> bool +val eq : typ -> typ -> bool +val sub : typ -> typ -> bool -val lub : con_env -> typ -> typ -> typ -val glb : con_env -> typ -> typ -> typ +val lub : typ -> typ -> typ +val glb : typ -> typ -> typ (* First-order substitution *) @@ -131,7 +137,7 @@ val close : con list -> typ -> typ val close_binds : con list -> bind list -> bind list val open_ : typ list -> typ -> typ -val open_binds : con_env -> bind list -> typ list * con_env +val open_binds : bind list -> typ list (* Environments *) @@ -147,4 +153,4 @@ val string_of_typ : typ -> string val string_of_kind : kind -> string val strings_of_kind : kind -> string * string * string -val string_of_typ_expand : con_env -> typ -> string +val string_of_typ_expand : typ -> string diff --git a/src/typing.ml b/src/typing.ml index e5113c3ed5d..2274ecdfc95 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -93,7 +93,7 @@ let add_typ c x con k = let add_typs c xs cs ks = { c with typs = List.fold_right2 T.Env.add xs cs c.typs; - cons = List.fold_right2 Con.Env.add cs ks c.cons; + cons = List.fold_right2 Con.Env.add (List.map (fun c -> c.T.con) cs) ks c.cons; } let adjoin c scope = @@ -141,10 +141,11 @@ and check_typ' env typ : T.typ = match typ.it with | VarT (id, typs) -> (match T.Env.find_opt id.it env.typs with - | Some c -> - let T.Def (tbs, t) | T.Abs (tbs, t) = Con.Env.find c env.cons in + | Some con -> + let kind = Con.Env.find con.T.con env.cons in + let T.Def (tbs, t) | T.Abs (tbs, t) = kind in let ts = check_typ_bounds env tbs typs typ.at in - T.Con (c, ts) + T.Con (con, ts) | None -> error env id.at "unbound type identifier %s" id.it ) | PrimT "Any" -> T.Any @@ -169,29 +170,29 @@ and check_typ' env typ : T.typ = let c = match typs2 with [{it = AsyncT _; _}] -> T.Promises | _ -> T.Returns in if sort.it = T.Sharable then begin let t1 = T.seq ts1 in - if not (T.sub env'.cons t1 T.Shared) then + if not (T.sub t1 T.Shared) then error env typ1.at "shared function has non-shared parameter type\n %s" - (T.string_of_typ_expand env'.cons t1); + (T.string_of_typ_expand t1); (match ts2 with | [] -> () | [T.Async t2] -> - if not (T.sub env'.cons t2 T.Shared) then + if not (T.sub t2 T.Shared) then error env typ1.at "shared function has non-shared result type\n %s" - (T.string_of_typ_expand env'.cons t2); + (T.string_of_typ_expand t2); | _ -> error env typ1.at "shared function has non-async result type\n %s" - (T.string_of_typ_expand env'.cons (T.seq ts2)) + (T.string_of_typ_expand (T.seq ts2)) ) end; - let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = t}) cs ts in T.Func (sort.it, c, T.close_binds cs tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2) | OptT typ -> T.Opt (check_typ env typ) | AsyncT typ -> let t = check_typ env typ in - let t' = T.promote env.cons t in - if t' <> T.Pre && not (T.sub env.cons t' T.Shared) then + let t' = T.promote t in + if t' <> T.Pre && not (T.sub t' T.Shared) then error env typ.at "async type has non-shared parameter type\n %s" - (T.string_of_typ_expand env.cons t'); + (T.string_of_typ_expand t'); T.Async t | ObjT (sort, fields) -> check_ids env (List.map (fun (field : typ_field) -> field.it.id) fields); @@ -203,18 +204,17 @@ and check_typ' env typ : T.typ = and check_typ_field env s typ_field : T.field = let {id; mut; typ} = typ_field.it in let t = infer_mut mut (check_typ env typ) in - if s = T.Actor && not (T.is_func (T.promote env.cons t)) then + if s = T.Actor && not (T.is_func (T.promote t)) then error env typ.at "actor field %s has non-function type\n %s" - id.it (T.string_of_typ_expand env.cons t); - if s <> T.Object T.Local && not (T.sub env.cons t T.Shared) then + id.it (T.string_of_typ_expand t); + if s <> T.Object T.Local && not (T.sub t T.Shared) then error env typ.at "shared object or actor field %s has non-shared type\n %s" - id.it (T.string_of_typ_expand env.cons t); + id.it (T.string_of_typ_expand t); {T.name = id.it; typ = t} 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 <- Some c) typ_binds cs; + let cs = List.map T.fresh_con xs in 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 @@ -224,20 +224,22 @@ and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env let pre_ks = List.map (fun c -> T.Abs ([], T.Pre)) cs in let pre_env' = add_typs {env with pre = true} xs cs pre_ks in let ts = List.map (fun typ_bind -> check_typ pre_env' typ_bind.it.bound) typ_binds in - let ks = List.map2 (fun c t -> T.Abs ([], t)) cs ts in + let ks = List.map (fun t -> T.Abs ([], t)) ts in + List.iter2 (fun c k -> c.T.kind := k) cs ks; let env' = add_typs env xs cs ks in let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in - cs, ts, te, Con.Env.from_list2 cs ks + List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs; + cs, ts, te, Con.Env.from_list2 (List.map (fun c -> c.T.con) cs) ks and check_typ_bounds env (tbs : T.bind list) typs at : T.typ list = match tbs, typs with | tb::tbs', typ::typs' -> let t = check_typ env typ in if not env.pre then begin - if not (T.sub env.cons t tb.T.bound) then + if not (T.sub t tb.T.bound) then local_error env typ.at "type argument\n %s\ndoes not match parameter bound\n %s" - (T.string_of_typ_expand env.cons t) - (T.string_of_typ_expand env.cons tb.T.bound) + (T.string_of_typ_expand t) + (T.string_of_typ_expand tb.T.bound) end; let ts' = check_typ_bounds env tbs' typs' at in t::ts' @@ -291,7 +293,7 @@ let infer_lit env lit at : T.prim = assert false let check_lit env t lit at = - match T.normalize env.cons t, !lit with + match T.normalize t, !lit with | T.Opt _, NullLit -> () | T.Prim T.Nat, PreLit (s, T.Nat) -> lit := NatLit (check_nat env at s) @@ -309,9 +311,9 @@ let check_lit env t lit at = lit := FloatLit (check_float env at s) | t, _ -> let t' = T.Prim (infer_lit env lit at) in - if not (T.sub env.cons t' t) then + if not (T.sub t' t) then local_error env at "literal of type\n %s\ndoes not have expected type\n %s" - (T.string_of_typ t') (T.string_of_typ_expand env.cons t) + (T.string_of_typ t') (T.string_of_typ_expand t) (* Expressions *) @@ -329,10 +331,10 @@ let rec infer_exp env exp : T.typ = and infer_exp_promote env exp : T.typ = let t = infer_exp env exp in - let t' = T.promote env.cons t in + let t' = T.promote t in if t' = T.Pre then error env exp.at "cannot infer type of expression while trying to infer surrounding class type,\nbecause its type is a forward reference to type\n %s" - (T.string_of_typ_expand env.cons t); + (T.string_of_typ_expand t); t' and infer_exp_mut env exp : T.typ = @@ -341,7 +343,7 @@ and infer_exp_mut env exp : T.typ = assert (t <> T.Pre); if not env.pre then begin let e = A.infer_effect_exp exp in - exp.note <- {note_typ = T.normalize env.cons t; note_eff = e} + exp.note <- {note_typ = T.normalize t; note_eff = e} end; t @@ -366,33 +368,33 @@ and infer_exp' env exp : T.typ = assert (!ot = Type.Pre); if not (Operator.has_unop t op) then error env exp.at "operator is not defined for operand type\n %s" - (T.string_of_typ_expand env.cons t); + (T.string_of_typ_expand t); ot := t; end; t | BinE (ot, exp1, op, exp2) -> let t1 = infer_exp_promote env exp1 in let t2 = infer_exp_promote env exp2 in - let t = T.lub env.cons t1 t2 in + let t = T.lub t1 t2 in if not env.pre then begin assert (!ot = Type.Pre); if not (Operator.has_binop t op) then error env exp.at "operator not defined for operand types\n %s and\n %s" - (T.string_of_typ_expand env.cons t1) - (T.string_of_typ_expand env.cons t2); + (T.string_of_typ_expand t1) + (T.string_of_typ_expand t2); ot := t end; t | RelE (ot, exp1, op, exp2) -> let t1 = infer_exp_promote env exp1 in let t2 = infer_exp_promote env exp2 in - let t = T.lub env.cons t1 t2 in + let t = T.lub t1 t2 in if not env.pre then begin assert (!ot = Type.Pre); if not (Operator.has_relop t op) then error env exp.at "operator not defined for operand types\n %s and\n %s" - (T.string_of_typ_expand env.cons t1) - (T.string_of_typ_expand env.cons t2); + (T.string_of_typ_expand t1) + (T.string_of_typ_expand t2); ot := t; end; T.bool @@ -405,15 +407,15 @@ and infer_exp' env exp : T.typ = | ProjE (exp1, n) -> let t1 = infer_exp_promote env exp1 in (try - let ts = T.as_tup_sub n env.cons t1 in + let ts = T.as_tup_sub n t1 in match List.nth_opt ts n with | Some t -> t | None -> error env exp.at "tuple projection %n is out of bounds for type\n %s" - n (T.string_of_typ_expand env.cons t1) + n (T.string_of_typ_expand t1) with Invalid_argument _ -> error env exp1.at "expected tuple type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) ) | ObjE (sort, id, fields) -> let env' = if sort.it = T.Actor then {env with async = false} else env in @@ -421,16 +423,16 @@ and infer_exp' env exp : T.typ = | DotE (exp1, sr, {it = Name n; _}) -> let t1 = infer_exp_promote env exp1 in (try - let s, tfs = T.as_obj_sub n env.cons t1 in + let s, tfs = T.as_obj_sub n t1 in sr := s; match List.find_opt (fun {T.name; _} -> name = n) tfs with | Some {T.typ = t; _} -> t | None -> error env exp1.at "field name %s does not exist in type\n %s" - n (T.string_of_typ_expand env.cons t1) + n (T.string_of_typ_expand t1) with Invalid_argument _ -> error env exp1.at "expected object type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) ) | AssignE (exp1, exp2) -> if not env.pre then begin @@ -444,9 +446,9 @@ and infer_exp' env exp : T.typ = T.unit | ArrayE (mut, exps) -> let ts = List.map (infer_exp env) exps in - let t1 = List.fold_left (T.lub env.cons) T.Non ts in + let t1 = List.fold_left T.lub T.Non ts in if - t1 = T.Any && List.for_all (fun t -> T.promote env.cons t <> T.Any) ts + t1 = T.Any && List.for_all (fun t -> T.promote t <> T.Any) ts then warn env exp.at "this array has type %s because elements have inconsistent types" (T.string_of_typ (T.Array t1)); @@ -454,31 +456,31 @@ and infer_exp' env exp : T.typ = | IdxE (exp1, exp2) -> let t1 = infer_exp_promote env exp1 in (try - let t = T.as_array_sub env.cons t1 in + let t = T.as_array_sub t1 in if not env.pre then check_exp env T.nat exp2; t with Invalid_argument _ -> error env exp1.at "expected array type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) ) | CallE (exp1, insts, exp2) -> let t1 = infer_exp_promote env exp1 in (try - let tbs, t2, t = T.as_func_sub (List.length insts) env.cons t1 in + let tbs, t2, t = T.as_func_sub (List.length insts) t1 in let ts = check_inst_bounds env tbs insts exp.at in if not env.pre then check_exp env (T.open_ ts t2) exp2; T.open_ ts t with Invalid_argument _ -> error env exp1.at "expected function type, but expression produces type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) ) | BlockE (decs, ot) -> let t, scope = infer_block env decs exp.at in let t' = try T.avoid env.cons scope.con_env t with T.Unavoidable c -> error env exp.at "local class type %s is contained in inferred block type\n %s" - (Con.to_string c) - (T.string_of_typ_expand (Con.Env.adjoin env.cons scope.con_env) t) + (Con.to_string c.T.con) + (T.string_of_typ_expand t) in ot := t'; t' @@ -501,21 +503,21 @@ and infer_exp' env exp : T.typ = if not env.pre then check_exp env T.bool exp1; let t2 = infer_exp env exp2 in let t3 = infer_exp env exp3 in - let t = T.lub env.cons t2 t3 in + let t = T.lub t2 t3 in if t = T.Any && - T.promote env.cons t2 <> T.Any && T.promote env.cons t3 <> T.Any + T.promote t2 <> T.Any && T.promote t3 <> T.Any then warn env exp.at "this if has type %s because branches have inconsistent types,\ntrue produces\n %s\nfalse produces\n %s" (T.string_of_typ t) - (T.string_of_typ_expand env.cons t2) - (T.string_of_typ_expand env.cons t3); + (T.string_of_typ_expand t2) + (T.string_of_typ_expand t3); t | SwitchE (exp1, cases) -> let t1 = infer_exp_promote env exp1 in let t = infer_cases env t1 T.Non cases in if not env.pre then - if not (Coverage.check_cases env.cons cases t1) then + if not (Coverage.check_cases cases t1) then warn env exp.at "the cases in this switch do not cover all possible values"; t | WhileE (exp1, exp2) -> @@ -534,16 +536,16 @@ and infer_exp' env exp : T.typ = if not env.pre then begin let t1 = infer_exp_promote env exp1 in (try - let _, tfs = T.as_obj_sub "next" env.cons t1 in + let _, tfs = T.as_obj_sub "next" t1 in let t = T.lookup_field "next" tfs in - let t1, t2 = T.as_mono_func_sub env.cons t in - if not (T.sub env.cons T.unit t1) then raise (Invalid_argument ""); - let t2' = T.as_opt_sub env.cons t2 in + let t1, t2 = T.as_mono_func_sub t in + if not (T.sub T.unit t1) then raise (Invalid_argument ""); + let t2' = T.as_opt_sub t2 in let ve = check_pat_exhaustive env t2' pat in check_exp (adjoin_vals env ve) T.unit exp2 with Invalid_argument _ -> local_error env exp1.at "expected iterable type, but expression has type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) ); end; T.unit @@ -578,19 +580,19 @@ and infer_exp' env exp : T.typ = let env' = {env with labs = T.Env.empty; rets = Some T.Pre; async = true} in let t = infer_exp env' exp1 in - if not (T.sub env.cons t T.Shared) then + if not (T.sub t T.Shared) then error env exp1.at "async type has non-shared parameter type\n %s" - (T.string_of_typ_expand env.cons t); + (T.string_of_typ_expand t); T.Async t | AwaitE exp1 -> if not env.async then error env exp.at "misplaced await"; let t1 = infer_exp_promote env exp1 in (try - T.as_async_sub env.cons t1 + T.as_async_sub t1 with Invalid_argument _ -> error env exp1.at "expected async type, but expression has type\n %s" - (T.string_of_typ_expand env.cons t1) + (T.string_of_typ_expand t1) ) | AssertE exp1 -> if not env.pre then check_exp env T.bool exp1; @@ -604,7 +606,7 @@ and infer_exp' env exp : T.typ = let t' = try T.avoid env.cons scope.con_env t with T.Unavoidable c -> error env exp.at "local class name %s is contained in inferred declaration type\n %s" - (Con.to_string c) (T.string_of_typ_expand env.cons t) + (Con.to_string c.T.con) (T.string_of_typ_expand t) in ot := t'; t' @@ -613,7 +615,7 @@ and check_exp env t exp = assert (not env.pre); assert (exp.note.note_typ = T.Pre); assert (t <> T.Pre); - let t' = T.normalize env.cons t in + let t' = T.normalize t in check_exp' env t' exp; let e = A.infer_effect_exp exp in exp.note <- {note_typ = t'; note_eff = e} @@ -642,7 +644,7 @@ and check_exp' env t exp = if (mut.it = Var) <> T.is_mut t' then local_error env exp.at "%smutable array expression cannot produce expected type\n %s" (if mut.it = Const then "im" else "") - (T.string_of_typ_expand env.cons (T.Array t')); + (T.string_of_typ_expand (T.Array t')); List.iter (check_exp env (T.as_immut t')) exps | AsyncE exp1, T.Async t' -> let env' = {env with labs = T.Env.empty; rets = Some t'; async = true} in @@ -657,14 +659,14 @@ and check_exp' env t exp = | SwitchE (exp1, cases), _ -> let t1 = infer_exp_promote env exp1 in check_cases env t1 t cases; - if not (Coverage.check_cases env.cons cases t1) then + if not (Coverage.check_cases cases t1) then warn env exp.at "the cases in this switch do not cover all possible values"; | _ -> let t' = infer_exp env exp in - if not (T.sub env.cons t' t) then + if not (T.sub t' t) then local_error env exp.at "expression of type\n %s\ncannot produce expected type\n %s" - (T.string_of_typ_expand env.cons t') - (T.string_of_typ_expand env.cons t) + (T.string_of_typ_expand t') + (T.string_of_typ_expand t) (* Cases *) @@ -675,15 +677,15 @@ and infer_cases env t_pat t cases : T.typ = and infer_case env t_pat t {it = {pat; exp}; at; _} = let ve = check_pat env t_pat pat in let t' = recover_with T.Non (infer_exp (adjoin_vals env ve)) exp in - let t'' = T.lub env.cons t t' in + let t'' = T.lub t t' in if t'' = T.Any && - T.promote env.cons t <> T.Any && T.promote env.cons t' <> T.Any + T.promote t <> T.Any && T.promote t' <> T.Any then warn env at "the switch has type %s because branches have inconsistent types,\nthis case produces type\n %s\nthe previous produce type\n %s" (T.string_of_typ t'') - (T.string_of_typ_expand env.cons t) - (T.string_of_typ_expand env.cons t'); + (T.string_of_typ_expand t) + (T.string_of_typ_expand t'); t'' and check_cases env t_pat t cases = @@ -718,7 +720,7 @@ and gather_pat env ve0 pat : val_env = and infer_pat_exhaustive env pat : T.typ * val_env = let t, ve = infer_pat env pat in if not env.pre then - if not (Coverage.check_pat env.cons pat t) then + if not (Coverage.check_pat pat t) then warn env pat.at "this pattern does not cover all possible values"; t, ve @@ -726,7 +728,7 @@ and infer_pat env pat : T.typ * val_env = assert (pat.note = T.Pre); let t, ve = infer_pat' env pat in if not env.pre then - pat.note <- T.normalize env.cons t; + pat.note <- T.normalize t; t, ve and infer_pat' env pat : T.typ * val_env = @@ -743,7 +745,7 @@ and infer_pat' env pat : T.typ * val_env = let t = if t1 = T.Prim T.Nat then T.Prim T.Int else t1 in if not (Operator.has_unop t op) then local_error env pat.at "operator is not defined for operand type\n %s" - (T.string_of_typ_expand env.cons t); + (T.string_of_typ_expand t); t, T.Env.empty | TupP pats -> let ts, ve = infer_pats pat.at env pats [] T.Env.empty in @@ -754,7 +756,7 @@ and infer_pat' env pat : T.typ * val_env = | AltP (pat1, pat2) -> let t1, ve1 = infer_pat env pat1 in let t2, ve2 = infer_pat env pat2 in - let t = T.lub env.cons t1 t2 in + let t = T.lub t1 t2 in if ve1 <> T.Env.empty || ve2 <> T.Env.empty then error env pat.at "variables are not allowed in pattern alternatives"; t, T.Env.empty @@ -774,14 +776,14 @@ and infer_pats at env pats ts ve : T.typ list * val_env = and check_pat_exhaustive env t pat : val_env = let ve = check_pat env t pat in if not env.pre then - if not (Coverage.check_pat env.cons pat t) then + if not (Coverage.check_pat pat t) then warn env pat.at "this pattern does not cover all possible values"; ve and check_pat env t pat : val_env = assert (pat.note = T.Pre); if t = T.Pre then snd (infer_pat env pat) else - let t' = T.normalize env.cons t in + let t' = T.normalize t in let ve = check_pat' env t' pat in if not env.pre then pat.note <- t'; ve @@ -798,20 +800,20 @@ and check_pat' env t pat : val_env = T.Env.empty | SignP (op, lit) -> if not env.pre then begin - let t' = T.normalize env.cons t in + let t' = T.normalize t in if not (Operator.has_unop t op) then local_error env pat.at "operator cannot consume expected type\n %s" - (T.string_of_typ_expand env.cons t'); + (T.string_of_typ_expand t'); check_lit env t' lit pat.at end; T.Env.empty | TupP pats -> (try - let ts = T.as_tup_sub (List.length pats) env.cons t in + let ts = T.as_tup_sub (List.length pats) t in check_pats env ts pats T.Env.empty pat.at with Invalid_argument _ -> error env pat.at "tuple pattern cannot consume expected type\n %s" - (T.string_of_typ_expand env.cons t) + (T.string_of_typ_expand t) ) | OptP pat1 -> (try @@ -819,7 +821,7 @@ and check_pat' env t pat : val_env = check_pat env t1 pat1 with Invalid_argument _ -> error env pat.at "option pattern cannot consume expected type\n %s" - (T.string_of_typ_expand env.cons t) + (T.string_of_typ_expand t) ) | AltP (pat1, pat2) -> let ve1 = check_pat env t pat1 in @@ -829,10 +831,10 @@ and check_pat' env t pat : val_env = T.Env.empty | _ -> let t', ve = infer_pat env pat in - if not (T.sub env.cons t t') then + if not (T.sub t t') then error env pat.at "pattern of type\n %s\ncannot consume expected type\n %s" - (T.string_of_typ_expand env.cons t') - (T.string_of_typ_expand env.cons t); + (T.string_of_typ_expand t') + (T.string_of_typ_expand t); ve and check_pats env ts pats ve at : val_env = @@ -874,7 +876,7 @@ and check_obj env s tfs id fields at : T.typ = if not (T.Env.mem name ve) then error env at "%s expression without field %s cannot produce expected type\n %s" (if s = T.Actor then "actor" else "object") name - (T.string_of_typ_expand env.cons t); + (T.string_of_typ_expand t); T.Env.add name t ve ) pre_ve tfs in @@ -928,16 +930,16 @@ and infer_exp_field env s (tfs, ve) field : T.field list * val_env = "%smutable field %s cannot produce expected %smutable field of type\n %s" (if mut.it = Var then "" else "im") id.it (if T.is_mut t then "" else "im") - (T.string_of_typ_expand env.cons (T.as_immut t)) + (T.string_of_typ_expand (T.as_immut t)) end; t in if not env.pre then begin if s = T.Actor && priv.it = Public && not (is_func_exp exp) then error env field.at "public actor field is not a function"; - if s <> T.Object T.Local && priv.it = Public && not (T.sub env.cons t T.Shared) then + if s <> T.Object T.Local && priv.it = Public && not (T.sub t T.Shared) then error env field.at "public shared object or actor field %s has non-shared type\n %s" - (string_of_name name.it) (T.string_of_typ_expand env.cons t) + (string_of_name name.it) (T.string_of_typ_expand t) end; let ve' = T.Env.add id.it t ve in let tfs' = @@ -1009,9 +1011,9 @@ and check_block env t decs at : scope = and check_block_exps env t decs at = match decs with | [] -> - if not (T.sub env.cons T.unit t) then + if not (T.sub T.unit t) then local_error env at "empty block cannot produce expected type\n %s" - (T.string_of_typ_expand env.cons t) + (T.string_of_typ_expand t) | [dec] -> check_dec env t dec | dec::decs' -> @@ -1049,10 +1051,10 @@ and check_dec env t dec = | _ -> let t' = infer_dec env dec in (* TBR: special-case unit? *) - if not (T.eq env.cons t T.unit || T.sub env.cons t' t) then + if not (T.eq t T.unit || T.sub t' t) then local_error env dec.at "expression of type\n %s\ncannot produce expected type\n %s" - (T.string_of_typ_expand env.cons t') - (T.string_of_typ_expand env.cons t) + (T.string_of_typ_expand t') + (T.string_of_typ_expand t) (* and print_ce = Con.Env.iter (fun c k -> @@ -1088,19 +1090,19 @@ and gather_dec_typdecs env scope dec : scope = | TypD (con_id, binds, _) | ClassD (_, con_id, binds, _, _, _, _) -> if T.Env.mem con_id.it scope.typ_env then error env dec.at "duplicate definition for type %s in block" con_id.it; - let cs = - List.map (fun (bind : typ_bind) -> Con.fresh bind.it.var.it) binds in - let pre_tbs = List.map (fun c -> {T.var = Con.name c; bound = T.Pre}) cs in - let c = Con.fresh con_id.it in + let pre_tbs = List.map (fun bind -> {T.var = bind.it.var.it; bound = T.Pre}) binds in + let c = T.fresh_con con_id.it in let pre_k = T.Abs (pre_tbs, T.Pre) in + c.T.kind := pre_k; let ve' = match dec.it with | ClassD (id, _, _ , _, _, _, _) -> + let cs = List.map (fun (bind : typ_bind) -> T.fresh_con bind.it.var.it) binds in let t2 = T.Con (c, List.map (fun c' -> T.Con (c', [])) cs) in T.Env.add id.it (T.Func (T.Local, T.Returns, pre_tbs, [T.Pre], [t2])) scope.val_env | _ -> scope.val_env in let te' = T.Env.add con_id.it c scope.typ_env in - let ce' = Con.Env.add c pre_k scope.con_env in + let ce' = Con.Env.add c.T.con pre_k scope.con_env in {val_env = ve'; typ_env = te'; con_env = ce'} @@ -1122,10 +1124,11 @@ and infer_dec_typdecs env dec : con_env = let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in let env' = adjoin_typs env te ce in let t = check_typ env' typ in - let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in let k = T.Def (tbs, T.close cs t) in - con_id.note <- Some (c, k); - Con.Env.singleton c k + c.T.kind := k; + con_id.note <- Some c; + Con.Env.singleton c.T.con k | ClassD (id, con_id, binds, sort, pat, self_id, fields) -> let c = T.Env.find con_id.it env.typs in let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in @@ -1133,10 +1136,11 @@ and infer_dec_typdecs env dec : con_env = let _, ve = infer_pat env' pat in let self_typ = T.Con(c, List.map (fun c -> T.Con (c, [])) cs) in let t = infer_obj (adjoin_vals env' ve) sort.it self_id (Some self_typ) fields in - let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in let k = T.Abs (tbs, T.close cs t) in - con_id.note <- Some (c, k); - Con.Env.singleton c k + c.T.kind := k; + con_id.note <- Some c; + Con.Env.singleton c.T.con k (* Pass 4: collect value identifiers *) and gather_block_valdecs env decs : val_env = @@ -1179,19 +1183,19 @@ and infer_dec_valdecs env dec : val_env = let t1, _ = infer_pat {env' with pre = true} pat in let t2 = check_typ env' typ in if not env.pre && sort.it = T.Sharable then begin - if not (T.sub env'.cons t1 T.Shared) then + if not (T.sub t1 T.Shared) then error env pat.at "shared function has non-shared parameter type\n %s" - (T.string_of_typ_expand env'.cons t1); + (T.string_of_typ_expand t1); begin match t2 with | T.Tup [] -> () | T.Async t2 -> - if not (T.sub env'.cons t2 T.Shared) then + if not (T.sub t2 T.Shared) then error env typ.at "shared function has non-shared result type\n %s" - (T.string_of_typ_expand env'.cons t2); + (T.string_of_typ_expand t2); if not (isAsyncE exp) then error env dec.at "shared function with async type has non-async body" | _ -> error env typ.at "shared function has non-async result type\n %s" - (T.string_of_typ_expand env'.cons t2) + (T.string_of_typ_expand t2) end; end; let ts1 = match pat.it with TupP ps -> T.as_seq t1 | _ -> [t1] in @@ -1201,7 +1205,7 @@ and infer_dec_valdecs env dec : val_env = | T.Sharable, (AsyncT _) -> T.Promises (* TBR: do we want this for T.Local too? *) | _ -> T.Returns in - let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in T.Env.singleton id.it (T.Func (sort.it, c, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2)) | TypD _ -> @@ -1213,7 +1217,7 @@ and infer_dec_valdecs env dec : val_env = let t1, _ = infer_pat {env' with pre = true} pat in let ts1 = match pat.it with TupP _ -> T.as_seq t1 | _ -> [t1] in let t2 = T.Con (c, List.map (fun c -> T.Con (c, [])) cs) in - let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in T.Env.singleton id.it (T.Func (T.Local, T.Returns, tbs, List.map (T.close cs) ts1, [T.close cs t2])) From 0dde54475a1a704a51da6b228d3316ca5154decb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 8 Feb 2019 18:32:03 +0100 Subject: [PATCH 10/42] Simplify Ir.TypD the `kind` is already in the `con`, so no need having it here. --- src/arrange_ir.ml | 4 ++-- src/async.ml | 4 ++-- src/check_ir.ml | 8 ++++---- src/compile.ml | 2 +- src/desugar.ml | 4 ++-- src/effect.ml | 2 +- src/freevars.ml | 2 +- src/ir.ml | 2 +- src/rename.ml | 2 +- src/tailcall.ml | 2 +- 10 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index 9ac3c6b19fe..234826c81e2 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -67,8 +67,8 @@ and dec d = match d.it with | 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,k) -> - "TypD" $$ [con c; kind k] + | TypD c -> + "TypD" $$ [con c; kind (Type.kind c)] and typ_bind (tb : typ_bind) = Con.to_string tb.it.con.Type.con $$ [typ tb.it.bound] diff --git a/src/async.ml b/src/async.ml index dc53b466a30..8e7c6fc8f55 100644 --- a/src/async.ml +++ b/src/async.ml @@ -312,8 +312,8 @@ and t_dec dec = and t_dec' dec' = match dec' with | ExpD exp -> ExpD (t_exp exp) - | TypD (con_id, k) -> - TypD (t_con con_id, t_kind k) + | 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) -> diff --git a/src/check_ir.ml b/src/check_ir.ml index 2ecc036059e..895a8e8fa54 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -728,9 +728,9 @@ and check_dec env dec = check_exp (adjoin_vals env'' ve) exp; check_sub env' dec.at (typ exp) t2; t0 <: t; - | TypD (c, k) -> + | TypD c -> let (binds,typ) = - match k with + match T.kind c with | T.Abs(binds,typ) | T.Def(binds,typ) -> (binds,typ) in @@ -795,11 +795,11 @@ and gather_dec env scope dec : scope = 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, k) -> + | TypD c -> check env dec.at (not (Con.Env.mem c.T.con scope.con_env)) "duplicate definition of type in block"; - let ce' = Con.Env.add c.T.con k scope.con_env in + let ce' = Con.Env.add c.T.con (T.kind c) scope.con_env in {scope with con_env = ce'} (* Programs *) diff --git a/src/compile.ml b/src/compile.ml index 1754cd8b109..b2ceca047f7 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -3733,7 +3733,7 @@ and compile_dec pre_env how dec : E.t * G.t * (E.t -> (SR.t * G.t)) = (pre_env, G.with_region dec.at alloc_code, fun env -> (fun (sr, code) -> (sr, G.with_region dec.at code)) (mk_code env))) @@ match dec.it with - | TypD (c,k) -> + | TypD _ -> (pre_env, G.nop, fun _ -> SR.unit, G.nop) | ExpD e ->(pre_env, G.nop, fun env -> compile_exp env e) | LetD (p, e) -> diff --git a/src/desugar.ml b/src/desugar.ml index 0f3a967b584..9d4d24a65d4 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -144,7 +144,7 @@ and decs ds = match d.it with | S.ClassD(_, con_id, _, _, _, _, _) -> let c = Lib.Option.value con_id.note in - let typD = { it = I.TypD (c,T.kind c); + let typD = { it = I.TypD c; at = d.at; note = { S.note_typ = T.unit; S.note_eff = T.Triv } @@ -162,7 +162,7 @@ and dec' at n d = match d with I.FuncD (cc, i, typ_binds tbs, pat p, ty.note, exp e) | S.TypD (con_id, typ_bind, t) -> let c = Lib.Option.value con_id.note in - I.TypD (c,T.kind c) + I.TypD c | S.ClassD (fun_id, typ_id, tbs, s, p, self_id, es) -> let cc = Value.call_conv_of_typ n.S.note_typ in let inst = List.map diff --git a/src/effect.ml b/src/effect.ml index eec17c93a2a..deeae6e46a1 100644 --- a/src/effect.ml +++ b/src/effect.ml @@ -196,7 +196,7 @@ module Ir = | LetD (_,e) | VarD (_, e) -> effect_exp e - | TypD (c,k) -> + | TypD _ -> T.Triv | FuncD (s, v, tps, p, t, e) -> T.Triv diff --git a/src/freevars.ml b/src/freevars.ml index a12db427ecc..6ae4438b1b2 100644 --- a/src/freevars.ml +++ b/src/freevars.ml @@ -122,7 +122,7 @@ and dec d = match d.it with (M.empty, S.singleton i.it) +++ exp e | FuncD (cc, i, tp, p, t, e) -> (M.empty, S.singleton i.it) +++ under_lambda (exp e /// pat p) - | TypD (c,k) -> (M.empty, S.empty) + | TypD c -> (M.empty, S.empty) (* The variables captured by a function. May include the function itself! *) and captured p e = diff --git a/src/ir.ml b/src/ir.ml index bbd6671e7ce..1b15d6f99bf 100644 --- a/src/ir.ml +++ b/src/ir.ml @@ -72,7 +72,7 @@ and dec' = | VarD of Syntax.id * exp (* mutable *) | FuncD of (* function *) Value.call_conv * Syntax.id * typ_bind list * pat * Type.typ * exp - | TypD of Type.con * Type.kind (* type *) + | TypD of Type.con (* type *) (* Program *) diff --git a/src/rename.ml b/src/rename.ml index 8e14eccfef0..655ddec0f9f 100644 --- a/src/rename.ml +++ b/src/rename.ml @@ -145,7 +145,7 @@ and dec' rho d = match d with let e' = exp rho'' e in FuncD (s, i', tp, p', t, e')), rho - | TypD (c,k) -> (* we don't rename type names *) + | TypD c -> (* we don't rename type names *) (fun rho -> d), rho diff --git a/src/tailcall.ml b/src/tailcall.ml index c242354f7de..67fdbcf8733 100644 --- a/src/tailcall.ml +++ b/src/tailcall.ml @@ -238,7 +238,7 @@ and dec' env d = let e' = tailexp env2 e in FuncD(cc, i, tbs, p, t, e')), env - | TypD (_, _) -> + | TypD _ -> (fun env -> d.it), env From 4f146b5b36e05df131a345201470708dfabdfcc2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 9 Feb 2019 11:05:25 +0100 Subject: [PATCH 11/42] Make the representation of con.kind private so that the choice whether it is a `promise`, or a `ref`, or something else, private to `type.ml`. I tried to make it more promise-like, by trapping when the kind is set a second time to something different, but it seems that `k = k'` can loop. --- src/async.ml | 2 +- src/type.ml | 17 ++++++++++++++--- src/type.mli | 7 +++++-- src/typing.ml | 15 +++++++-------- 4 files changed, 27 insertions(+), 14 deletions(-) diff --git a/src/async.ml b/src/async.ml index 8e7c6fc8f55..98706670032 100644 --- a/src/async.ml +++ b/src/async.ml @@ -176,7 +176,7 @@ and t_kind k = T.Def(t_binds typ_binds, t_typ typ) and t_con con = - con.kind := t_kind !(con.kind); + T.modify_kind con t_kind; con and t_operator_type ot = diff --git a/src/type.ml b/src/type.ml index b0cbb4c18c9..0d5dcc5c84b 100644 --- a/src/type.ml +++ b/src/type.ml @@ -36,7 +36,8 @@ and typ = | Non (* bottom *) | Pre (* pre-type *) -and con = { con : Con.t; kind : kind ref } +and kind_field = kind ref (* abstract, only this module knows its a ref *) +and con = { con : Con.t; kind : kind_field } and bind = {var : string; bound : typ} and field = {name : string; typ : typ} @@ -47,10 +48,20 @@ and kind = (* cons *) -(* the promise is only there to break the recursion in open_bind *) +(* The con field is a reference to break the recursion in open_binds, + and to allow the multiple passes in typing *) let kind con = !(con.kind) -let fresh_con n = { con = Con.fresh n; kind = ref (Abs ([],Pre)) } +let fresh_con n k = { con = Con.fresh n; kind = ref k } +let set_kind c k = match !(c.kind) with + | Abs (_, Pre) -> c.kind := k + (* I wanted a safeguard against mutatig redefinitions, + but this equality runs out of memory. + | k' when k = k' -> () + | _ -> raise (Invalid_argument "set_kind") + *) + | _ -> c.kind := k +let modify_kind c f = c.kind := f !(c.kind) (* field ordering *) diff --git a/src/type.mli b/src/type.mli index 11ca503d8c6..91b4b0673b5 100644 --- a/src/type.mli +++ b/src/type.mli @@ -41,7 +41,8 @@ and field = {name : string; typ : typ} (* cons and kinds *) -and con = { con : Con.t; kind : kind ref } +and kind_field (* abstract *) +and con = { con : Con.t; kind : kind_field } and kind = | Def of bind list * typ | Abs of bind list * typ @@ -49,7 +50,9 @@ and kind = type con_env = kind Con.Env.t val kind : con -> kind -val fresh_con : string -> con +val fresh_con : string -> kind -> con +val set_kind : con -> kind -> unit +val modify_kind : con -> (kind -> kind) -> unit (* field ordering *) diff --git a/src/typing.ml b/src/typing.ml index 2274ecdfc95..50516840262 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 T.fresh_con xs in + let cs = List.map (fun n -> T.fresh_con n (T.Abs ([], T.Pre))) xs in 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 @@ -225,7 +225,7 @@ and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env let pre_env' = add_typs {env with pre = true} xs cs pre_ks in let ts = List.map (fun typ_bind -> check_typ pre_env' typ_bind.it.bound) typ_binds in let ks = List.map (fun t -> T.Abs ([], t)) ts in - List.iter2 (fun c k -> c.T.kind := k) cs ks; + List.iter2 T.set_kind cs ks; let env' = add_typs env xs cs ks in let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs; @@ -1091,13 +1091,12 @@ and gather_dec_typdecs env scope dec : scope = if T.Env.mem con_id.it scope.typ_env then error env dec.at "duplicate definition for type %s in block" con_id.it; let pre_tbs = List.map (fun bind -> {T.var = bind.it.var.it; bound = T.Pre}) binds in - let c = T.fresh_con con_id.it in - let pre_k = T.Abs (pre_tbs, T.Pre) in - c.T.kind := pre_k; + let pre_k = (T.Abs (pre_tbs, T.Pre)) in + let c = T.fresh_con con_id.it pre_k in let ve' = match dec.it with | ClassD (id, _, _ , _, _, _, _) -> - let cs = List.map (fun (bind : typ_bind) -> T.fresh_con bind.it.var.it) binds in + let cs = List.map (fun (bind : typ_bind) -> T.fresh_con bind.it.var.it (T.Abs ([], T.Pre))) binds in let t2 = T.Con (c, List.map (fun c' -> T.Con (c', [])) cs) in T.Env.add id.it (T.Func (T.Local, T.Returns, pre_tbs, [T.Pre], [t2])) scope.val_env | _ -> scope.val_env in @@ -1126,7 +1125,7 @@ and infer_dec_typdecs env dec : con_env = let t = check_typ env' typ in let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in let k = T.Def (tbs, T.close cs t) in - c.T.kind := k; + T.set_kind c k; con_id.note <- Some c; Con.Env.singleton c.T.con k | ClassD (id, con_id, binds, sort, pat, self_id, fields) -> @@ -1138,7 +1137,7 @@ and infer_dec_typdecs env dec : con_env = let t = infer_obj (adjoin_vals env' ve) sort.it self_id (Some self_typ) fields in let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in let k = T.Abs (tbs, T.close cs t) in - c.T.kind := k; + T.set_kind c k; con_id.note <- Some c; Con.Env.singleton c.T.con k From d5baf2bab1d99a65ef07c286e096815e973d6416 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 9 Feb 2019 11:16:44 +0100 Subject: [PATCH 12/42] Make set_kind check that the kind is not set a second time with a different value. A bit like a promise, but more compatible with `typing.ml` running `infer_dec_typdecs` multiple times. Not sure if it is worth the bother, though. --- src/type.ml | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/src/type.ml b/src/type.ml index 0d5dcc5c84b..bc9f524421c 100644 --- a/src/type.ml +++ b/src/type.ml @@ -53,14 +53,6 @@ and kind = let kind con = !(con.kind) let fresh_con n k = { con = Con.fresh n; kind = ref k } -let set_kind c k = match !(c.kind) with - | Abs (_, Pre) -> c.kind := k - (* I wanted a safeguard against mutatig redefinitions, - but this equality runs out of memory. - | k' when k = k' -> () - | _ -> raise (Invalid_argument "set_kind") - *) - | _ -> c.kind := k let modify_kind c f = c.kind := f !(c.kind) (* field ordering *) @@ -416,7 +408,7 @@ let rec rel_typ rel eq t1 t2 = rel_typ rel eq (open_ ts1 t) t2 | _, Def (tbs, t) -> (* TBR this may fail to terminate *) rel_typ rel eq t1 (open_ ts2 t) - | _ when con1 = con2 -> + | _ when con1.con = con2.con -> rel_list eq_typ rel eq ts1 ts2 | Abs (tbs, t), _ when rel != eq -> rel_typ rel eq (open_ ts1 t) t2 @@ -517,6 +509,23 @@ and eq t1 t2 : bool = and sub t1 t2 : bool = rel_typ (ref S.empty) (ref S.empty) t1 t2 +and eq_kind k1 k2 : bool = + let eq = ref S.empty in + match k1, k2 with + | Def (tbs1, t1), Def (tbs2, t2) + | Abs (tbs1, t1), Abs (tbs2, t2) -> + begin match rel_binds eq eq tbs1 tbs2 with + | Some ts -> eq_typ eq eq (open_ ts t1) (open_ ts t2) + | None -> false + end + | _ -> false + +(* Moved here to use eq_kind *) +let set_kind c k = match !(c.kind) with + | Abs (_, Pre) -> c.kind := k + (* This safeguards against mutating redefinitions *) + | k' when eq_kind k k' -> () + | _ -> raise (Invalid_argument "set_kind") (* Least upper bound and greatest lower bound *) From da7d6ae324d523551707738be5d9c59083648904 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 9 Feb 2019 11:23:15 +0100 Subject: [PATCH 13/42] Address nit --- src/type.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/type.ml b/src/type.ml index bc9f524421c..c08a52e7cf1 100644 --- a/src/type.ml +++ b/src/type.ml @@ -176,9 +176,9 @@ and subst_field sigma {name; typ} = let close cs t = if cs = [] then t else - let bare_cons = List.map (fun c -> c.con) cs in - let ts = List.mapi (fun i c -> Var (Con.name c, i)) bare_cons in - let sigma = List.fold_right2 Con.Env.add bare_cons ts Con.Env.empty in + let cons = List.map (fun c -> c.con) cs in + let ts = List.mapi (fun i c -> Var (Con.name c, i)) cons in + let sigma = List.fold_right2 Con.Env.add cons ts Con.Env.empty in subst sigma t let close_binds cs tbs = From a8f87dfc714fe5f24179de6a03ed23b8096f8e11 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 14:07:56 +0100 Subject: [PATCH 14/42] Refactor avoid to take a `con_set`, not a `con_env` --- src/con.ml | 3 +++ src/con.mli | 3 +++ src/type.ml | 61 +++++++++++++++++++++++++++------------------------ src/type.mli | 3 ++- src/typing.ml | 6 +++-- 5 files changed, 44 insertions(+), 32 deletions(-) diff --git a/src/con.ml b/src/con.ml index 7bc633d0756..8615b73652d 100644 --- a/src/con.ml +++ b/src/con.ml @@ -21,3 +21,6 @@ let to_string c = module Env = Env.Make(struct type t = con let compare = compare end) +module Set = Set.Make(struct type t = con let compare = compare end) + +let set_of_env m = Env.fold (fun v _ m -> Set.add v m) m Set.empty diff --git a/src/con.mli b/src/con.mli index 9f2718a530b..bdaac3463c3 100644 --- a/src/con.mli +++ b/src/con.mli @@ -7,3 +7,6 @@ val name : t -> string val to_string : t -> string module Env : Env.S with type key = t +module Set : Set.S with type elt = t + +val set_of_env : 'a Env.t -> Set.t diff --git a/src/type.ml b/src/type.ml index c08a52e7cf1..c4d9b027557 100644 --- a/src/type.ml +++ b/src/type.ml @@ -60,6 +60,7 @@ let modify_kind c f = c.kind := f !(c.kind) let compare_field {name=n;_} {name=m;_} = compare n m type con_env = kind Con.Env.t +type con_set = Con.Set.t let seq ts = match ts with @@ -344,41 +345,43 @@ let rec span = function exception Unavoidable of con -let rec avoid' env env' = function +let rec avoid' env to_avoid = function | (Prim _ | Var _ | Any | Non | Shared | Pre) as t -> t | Con (c, ts) -> - (match Con.Env.find_opt c.con env' with - | Some (Abs _) -> raise (Unavoidable c) - | Some (Def (tbs, t)) -> avoid' env env' (reduce tbs t ts) - | None -> - try - Con (c, List.map (avoid' env env') ts) + if Con.Set.mem c.con to_avoid + then match kind c with + | Abs _ -> raise (Unavoidable c) + | Def (tbs, t) -> avoid' env to_avoid (reduce tbs t ts) + else + begin try + Con (c, List.map (avoid' env to_avoid) ts) with Unavoidable _ -> - match Con.Env.find c.con env with - | Abs _ -> raise (Unavoidable c) - | Def (tbs, t) -> avoid' env env' (reduce tbs t ts) - ) - | Array t -> Array (avoid' env env' t) - | Tup ts -> Tup (List.map (avoid' env env') ts) + begin match Con.Env.find c.con env with + | Def (tbs, t) -> avoid' env to_avoid (reduce tbs t ts) + | Abs _ -> assert false (* c can only have parameters if it is a type def, or bound by Pre *) + end + end + | Array t -> Array (avoid' env to_avoid t) + | Tup ts -> Tup (List.map (avoid' env to_avoid) ts) | Func (s, c, tbs, ts1, ts2) -> Func (s, c, - List.map (avoid_bind env env') tbs, - List.map (avoid' env env') ts1, List.map (avoid' env env') ts2) - | Opt t -> Opt (avoid' env env' t) - | Async t -> Async (avoid' env env' t) - | Obj (s, fs) -> Obj (s, List.map (avoid_field env env') fs) - | Mut t -> Mut (avoid' env env' t) - -and avoid_bind env env' {var; bound} = - {var; bound = avoid' env env' bound} - -and avoid_field env env' {name; typ} = - {name; typ = avoid' env env' typ} - -let avoid env env' t = - if env' = Con.Env.empty then t else - avoid' env env' t + List.map (avoid_bind env to_avoid) tbs, + List.map (avoid' env to_avoid) ts1, List.map (avoid' env to_avoid) ts2) + | Opt t -> Opt (avoid' env to_avoid t) + | Async t -> Async (avoid' env to_avoid t) + | Obj (s, fs) -> Obj (s, List.map (avoid_field env to_avoid) fs) + | Mut t -> Mut (avoid' env to_avoid t) + +and avoid_bind env to_avoid {var; bound} = + {var; bound = avoid' env to_avoid bound} + +and avoid_field env to_avoid {name; typ} = + {name; typ = avoid' env to_avoid typ} + +let avoid env to_avoid t = + if to_avoid = Con.Set.empty then t else + avoid' env to_avoid t (* Equivalence & Subtyping *) diff --git a/src/type.mli b/src/type.mli index 91b4b0673b5..d7ce2e739e0 100644 --- a/src/type.mli +++ b/src/type.mli @@ -48,6 +48,7 @@ and kind = | Abs of bind list * typ type con_env = kind Con.Env.t +type con_set = Con.Set.t val kind : con -> kind val fresh_con : string -> kind -> con @@ -122,7 +123,7 @@ val normalize : typ -> typ val promote : typ -> typ exception Unavoidable of con -val avoid : con_env -> con_env -> typ -> typ (* raise Unavoidable *) +val avoid : con_env -> con_set -> typ -> typ (* raise Unavoidable *) (* Equivalence and Subtyping *) diff --git a/src/typing.ml b/src/typing.ml index 81261f4743e..23abed5adbb 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -477,7 +477,8 @@ and infer_exp' env exp : T.typ = | BlockE (decs, ot) -> let t, scope = infer_block env decs exp.at in let t' = - try T.avoid env.cons scope.con_env t with T.Unavoidable c -> + let to_avoid = Con.set_of_env scope.con_env in + try T.avoid env.cons to_avoid t with T.Unavoidable c -> error env exp.at "local class type %s is contained in inferred block type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) @@ -604,7 +605,8 @@ and infer_exp' env exp : T.typ = | DecE (dec, ot) -> let t, scope = infer_block env [dec] exp.at in let t' = - try T.avoid env.cons scope.con_env t with T.Unavoidable c -> + let to_avoid = Con.set_of_env scope.con_env in + try T.avoid env.cons to_avoid t with T.Unavoidable c -> error env exp.at "local class name %s is contained in inferred declaration type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) in From 0986cffb94caa0238109f70500a52a5693145c67 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 14:11:22 +0100 Subject: [PATCH 15/42] Drop con_env argument to Type.avoid (use kind inside) --- src/type.ml | 41 +++++++++++++++++++++-------------------- src/type.mli | 2 +- src/typing.ml | 4 ++-- 3 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/type.ml b/src/type.ml index c4d9b027557..5e9acd7d338 100644 --- a/src/type.ml +++ b/src/type.ml @@ -60,7 +60,6 @@ let modify_kind c f = c.kind := f !(c.kind) let compare_field {name=n;_} {name=m;_} = compare n m type con_env = kind Con.Env.t -type con_set = Con.Set.t let seq ts = match ts with @@ -345,43 +344,45 @@ let rec span = function exception Unavoidable of con -let rec avoid' env to_avoid = function +type con_set = Con.Set.t + +let rec avoid' to_avoid = function | (Prim _ | Var _ | Any | Non | Shared | Pre) as t -> t | Con (c, ts) -> if Con.Set.mem c.con to_avoid then match kind c with | Abs _ -> raise (Unavoidable c) - | Def (tbs, t) -> avoid' env to_avoid (reduce tbs t ts) + | Def (tbs, t) -> avoid' to_avoid (reduce tbs t ts) else begin try - Con (c, List.map (avoid' env to_avoid) ts) + Con (c, List.map (avoid' to_avoid) ts) with Unavoidable _ -> - begin match Con.Env.find c.con env with - | Def (tbs, t) -> avoid' env to_avoid (reduce tbs t ts) + begin match kind c with + | Def (tbs, t) -> avoid' to_avoid (reduce tbs t ts) | Abs _ -> assert false (* c can only have parameters if it is a type def, or bound by Pre *) end end - | Array t -> Array (avoid' env to_avoid t) - | Tup ts -> Tup (List.map (avoid' env to_avoid) ts) + | Array t -> Array (avoid' to_avoid t) + | Tup ts -> Tup (List.map (avoid' to_avoid) ts) | Func (s, c, tbs, ts1, ts2) -> Func (s, c, - List.map (avoid_bind env to_avoid) tbs, - List.map (avoid' env to_avoid) ts1, List.map (avoid' env to_avoid) ts2) - | Opt t -> Opt (avoid' env to_avoid t) - | Async t -> Async (avoid' env to_avoid t) - | Obj (s, fs) -> Obj (s, List.map (avoid_field env to_avoid) fs) - | Mut t -> Mut (avoid' env to_avoid t) + List.map (avoid_bind to_avoid) tbs, + List.map (avoid' to_avoid) ts1, List.map (avoid' to_avoid) ts2) + | Opt t -> Opt (avoid' to_avoid t) + | Async t -> Async (avoid' to_avoid t) + | Obj (s, fs) -> Obj (s, List.map (avoid_field to_avoid) fs) + | Mut t -> Mut (avoid' to_avoid t) -and avoid_bind env to_avoid {var; bound} = - {var; bound = avoid' env to_avoid bound} +and avoid_bind to_avoid {var; bound} = + {var; bound = avoid' to_avoid bound} -and avoid_field env to_avoid {name; typ} = - {name; typ = avoid' env to_avoid typ} +and avoid_field to_avoid {name; typ} = + {name; typ = avoid' to_avoid typ} -let avoid env to_avoid t = +let avoid to_avoid t = if to_avoid = Con.Set.empty then t else - avoid' env to_avoid t + avoid' to_avoid t (* Equivalence & Subtyping *) diff --git a/src/type.mli b/src/type.mli index d7ce2e739e0..c405e6a1920 100644 --- a/src/type.mli +++ b/src/type.mli @@ -123,7 +123,7 @@ val normalize : typ -> typ val promote : typ -> typ exception Unavoidable of con -val avoid : con_env -> con_set -> typ -> typ (* raise Unavoidable *) +val avoid : con_set -> typ -> typ (* raise Unavoidable *) (* Equivalence and Subtyping *) diff --git a/src/typing.ml b/src/typing.ml index 23abed5adbb..5a57c7a2f5c 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -478,7 +478,7 @@ and infer_exp' env exp : T.typ = let t, scope = infer_block env decs exp.at in let t' = let to_avoid = Con.set_of_env scope.con_env in - try T.avoid env.cons to_avoid t with T.Unavoidable c -> + try T.avoid to_avoid t with T.Unavoidable c -> error env exp.at "local class type %s is contained in inferred block type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) @@ -606,7 +606,7 @@ and infer_exp' env exp : T.typ = let t, scope = infer_block env [dec] exp.at in let t' = let to_avoid = Con.set_of_env scope.con_env in - try T.avoid env.cons to_avoid t with T.Unavoidable c -> + try T.avoid to_avoid t with T.Unavoidable c -> error env exp.at "local class name %s is contained in inferred declaration type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) in From 51fc8f78db27d798f748db1d7fd64379ac0158ee Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 14:34:43 +0100 Subject: [PATCH 16/42] Remove `con_env` from `scope` In `typing.ml`, we replace it with a `con_set`, so that we can still call `avoid`. In `check_ir.ml` we simply drop the field. --- src/check_ir.ml | 84 +++++++++++++++++-------------------------------- src/pipeline.ml | 13 +++++--- src/typing.ml | 67 +++++++++++++++++---------------------- src/typing.mli | 4 +-- 4 files changed, 67 insertions(+), 101 deletions(-) diff --git a/src/check_ir.ml b/src/check_ir.ml index 895a8e8fa54..31c1082cc52 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -29,17 +29,14 @@ type con_env = T.con_env type scope = { val_env : val_env; - con_env : con_env; } let empty_scope : scope = { val_env = T.Env.empty; - con_env = Con.Env.empty } let adjoin_scope scope1 scope2 = { val_env = T.Env.adjoin scope1.val_env scope2.val_env; - con_env = Con.Env.adjoin scope1.con_env scope2.con_env; } (* Contexts (internal) *) @@ -49,7 +46,6 @@ type ret_env = T.typ option type env = { vals : val_env; - cons : con_env; labs : lab_env; rets : ret_env; async : bool; @@ -60,7 +56,6 @@ type env = let env_of_scope scope : env = { vals = scope.Typing.val_env; - cons = scope.Typing.con_env; labs = T.Env.empty; rets = None; async = false; @@ -79,23 +74,12 @@ 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 - cons = List.fold_right (fun c -> Con.Env.add c.T.con (T.kind c)) cs c.cons; - } - let adjoin c scope = { c with vals = T.Env.adjoin c.vals scope.val_env; - cons = Con.Env.adjoin 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 = Con.Env.adjoin c.cons ce} -let adjoin_typs c ce = - { c with - cons = Con.Env.adjoin c.cons ce; - } let disjoint_union env at fmt env1 env2 = try T.Env.disjoint_union env1 env2 @@ -146,13 +130,12 @@ let rec check_typ env typ : unit = | T.Tup typs -> List.iter (check_typ env) typs | T.Func (sort, control, binds, ts1, ts2) -> - let cs, ce = check_typ_binds env binds in - let env' = adjoin_typs env ce in + let cs = check_typ_binds env binds in 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 - List.iter (check_typ env') ts1; - List.iter (check_typ env') ts2; + List.iter (check_typ env) ts1; + List.iter (check_typ env) ts2; if control = T.Promises then begin match ts2 with | [T.Async _ ] -> () @@ -163,11 +146,11 @@ let rec check_typ env typ : unit = end; if sort = T.Sharable then begin let t1 = T.seq ts1 in - check_sub env' no_region t1 T.Shared; + check_sub env no_region t1 T.Shared; match ts2 with | [] -> () | [T.Async t2] -> - check_sub env' no_region t2 T.Shared; + check_sub env no_region t2 T.Shared; | _ -> error env no_region "shared function has non-async result type\n %s" (T.string_of_typ_expand (T.seq ts2)) end @@ -201,17 +184,16 @@ and check_typ_field env s typ_field : unit = "shared object or actor field has non-shared type" -and check_typ_binds env typ_binds : T.con list * con_env = +and check_typ_binds env typ_binds : T.con list = let ts = Type.open_binds typ_binds in let cs = List.map (function T.Con(c,[]) -> c | _ -> assert false) ts in - let env' = add_typs env cs in let _ = List.map (fun typ_bind -> let bd = T.open_ ts typ_bind.T.bound in - check_typ env' bd) + check_typ env bd) typ_binds in - cs, Con.Env.from_list (List.map (fun c -> (c.T.con, T.kind c)) cs) + cs and check_typ_bounds env (tbs : T.bind list) typs at : unit = match tbs, typs with @@ -392,7 +374,7 @@ let rec check_exp env (exp:Ir.exp) : unit = (typ exp2) <: T.open_ insts t2; T.open_ insts t3 <: t; | BlockE (decs, t0) -> - let t1, scope = type_block env decs exp.at in + let t1 = type_block env decs exp.at in check_typ env t0; check (T.eq t T.unit || T.eq t1 t0) "unexpected expected block type"; t0 <: t; @@ -665,10 +647,9 @@ and type_exp_field env s (tfs, ve) field : T.field list * val_env = (* Blocks and Declarations *) -and type_block env decs at : T.typ * scope = +and type_block env decs at : T.typ = let scope = gather_block_decs env decs in - let t = type_block_exps (adjoin env scope) decs in - t, scope + type_block_exps (adjoin env scope) decs and type_block_exps env decs : T.typ = match decs with @@ -690,10 +671,9 @@ and cons_of_typ_binds typ_binds = and check_open_typ_binds env typ_binds = let cs = List.map (fun tp -> tp.it.con) typ_binds in - let ce = List.fold_right (fun c -> Con.Env.add c.Type.con (Type.kind c)) cs Con.Env.empty 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 + let _ = check_typ_binds env binds in + () and close_typ_binds cs tbs = List.map (fun {con; bound} -> {Type.var = Con.name con.T.con; bound = Type.close cs bound}) tbs @@ -716,17 +696,16 @@ and check_dec env dec = 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_typs env ce in - let ve = check_pat_exhaustive env' pat in - check_typ env' t2; + check_open_typ_binds env typ_binds; + 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 + {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; + check_sub env dec.at (typ exp) t2; t0 <: t; | TypD c -> let (binds,typ) = @@ -734,16 +713,14 @@ and check_dec env dec = | T.Abs(binds,typ) | T.Def(binds,typ) -> (binds,typ) in - let cs,ce = check_typ_binds env binds in + let cs = check_typ_binds env binds in let ts = List.map (fun c -> T.Con(c,[])) cs in - let env' = adjoin_typs env ce in - check_typ env' (T.open_ ts typ); + check_typ env (T.open_ ts typ); T.unit <: t; -and check_block env t decs at : scope = +and check_block env t decs at = let scope = gather_block_decs env decs in - check_block_exps (adjoin env scope) t decs at; - scope + check_block_exps (adjoin env scope) t decs at and check_block_exps env t decs at = match decs with @@ -757,7 +734,7 @@ and check_block_exps env t decs at = check_dec env dec; check_block_exps env t decs' at -and gather_block_decs env decs = +and gather_block_decs env decs : scope = List.fold_left (gather_dec env) empty_scope decs and gather_dec env scope dec : scope = @@ -766,13 +743,13 @@ and gather_dec env scope dec : scope = scope | LetD (pat, _) -> let ve = gather_pat env scope.val_env pat in - { scope with val_env = ve} + { val_env = ve} | VarD (id, exp) -> check env dec.at (not (T.Env.mem id.it scope.val_env)) "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} + { 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 @@ -794,16 +771,13 @@ and gather_dec env scope dec : scope = let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; 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'} + { val_env = ve' } | TypD c -> - check env dec.at - (not (Con.Env.mem c.T.con scope.con_env)) - "duplicate definition of type in block"; - let ce' = Con.Env.add c.T.con (T.kind c) scope.con_env in - {scope with con_env = ce'} + (* Do we want to check for duplicate type definitions? *) + scope (* Programs *) let check_prog env prog : unit = - ignore (check_block env T.unit prog.it prog.at) + check_block env T.unit prog.it prog.at diff --git a/src/pipeline.ml b/src/pipeline.ml index 2bb2f588a24..2d607d6c847 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -15,10 +15,13 @@ let phase heading name = let error at cat text = Error { Diag.sev = Diag.Error; at; cat; text } -let print_ce = - Con.Env.iter (fun c k -> - let eq, params, typ = Type.strings_of_kind k in +let print_cs = + Con.Set.iter (fun c -> + printf "temporary TODO" + (* + let eq, params, typ = Type.strings_of_kind (Type.kind c) in printf "type %s%s %s %s\n" (Con.to_string c) params eq typ + *) ) let print_stat_ve = @@ -38,7 +41,7 @@ let print_dyn_ve scope = ) let print_scope senv scope dve = - print_ce scope.Typing.con_env; + print_cs scope.Typing.con_set; print_dyn_ve senv dve let print_val _senv v t = @@ -108,7 +111,7 @@ let check_prog infer senv name prog if !Flags.trace && !Flags.verbose then begin match r with | Ok ((_, scope), _) -> - print_ce scope.Typing.con_env; + print_cs scope.Typing.con_set; print_stat_ve scope.Typing.val_env; dump_prog Flags.dump_tc prog; | Error _ -> () diff --git a/src/typing.ml b/src/typing.ml index 5a57c7a2f5c..63e96cf602f 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -19,24 +19,24 @@ let recover f y = recover_with () f y type val_env = T.typ T.Env.t type typ_env = T.con T.Env.t -type con_env = T.con_env +type con_set = T.con_set type scope = { val_env : val_env; typ_env : typ_env; - con_env : con_env; + con_set : con_set; } let empty_scope : scope = { val_env = T.Env.empty; typ_env = T.Env.empty; - con_env = Con.Env.empty + con_set = Con.Set.empty; } let adjoin_scope scope1 scope2 = { val_env = T.Env.adjoin scope1.val_env scope2.val_env; typ_env = T.Env.adjoin scope1.typ_env scope2.typ_env; - con_env = Con.Env.adjoin scope1.con_env scope2.con_env; + con_set = Con.Set.union scope1.con_set scope2.con_set; } (* Contexts (internal) *) @@ -47,7 +47,6 @@ type ret_env = T.typ option type env = { vals : val_env; typs : typ_env; - cons : con_env; labs : lab_env; rets : ret_env; async : bool; @@ -58,7 +57,6 @@ type env = let env_of_scope msgs scope = { vals = scope.val_env; typs = scope.typ_env; - cons = scope.con_env; labs = T.Env.empty; rets = None; async = false; @@ -90,25 +88,21 @@ let add_typ c x con k = } *) -let add_typs c xs cs ks = +let add_typs c xs cs = { c with typs = List.fold_right2 T.Env.add xs cs c.typs; - cons = List.fold_right2 Con.Env.add (List.map (fun c -> c.T.con) cs) ks c.cons; } let adjoin c scope = { c with vals = T.Env.adjoin c.vals scope.val_env; typs = T.Env.adjoin c.typs scope.typ_env; - cons = Con.Env.adjoin 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 = Con.Env.adjoin c.cons ce} let adjoin_typs c te ce = { c with typs = T.Env.adjoin c.typs te; - cons = Con.Env.adjoin c.cons ce; } let disjoint_union env at fmt env1 env2 = @@ -142,7 +136,7 @@ and check_typ' env typ : T.typ = | VarT (id, typs) -> (match T.Env.find_opt id.it env.typs with | Some con -> - let kind = Con.Env.find con.T.con env.cons in + let kind = T.kind con in let T.Def (tbs, t) | T.Abs (tbs, t) = kind in let ts = check_typ_bounds env tbs typs typ.at in T.Con (con, ts) @@ -212,7 +206,7 @@ and check_typ_field env s typ_field : T.field = id.it (T.string_of_typ_expand t); {T.name = id.it; typ = t} -and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env = +and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_set = let xs = List.map (fun typ_bind -> typ_bind.it.var.it) typ_binds in let cs = List.map (fun n -> T.fresh_con n (T.Abs ([], T.Pre))) xs in let te = List.fold_left2 (fun te typ_bind c -> @@ -221,15 +215,14 @@ and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env error env id.at "duplicate type name %s in type parameter list" id.it; T.Env.add id.it c te ) T.Env.empty typ_binds cs in - let pre_ks = List.map (fun c -> T.Abs ([], T.Pre)) cs in - let pre_env' = add_typs {env with pre = true} xs cs pre_ks in + let pre_env' = add_typs {env with pre = true} xs cs in let ts = List.map (fun typ_bind -> check_typ pre_env' typ_bind.it.bound) typ_binds in let ks = List.map (fun t -> T.Abs ([], t)) ts in List.iter2 T.set_kind cs ks; - let env' = add_typs env xs cs ks in + let env' = add_typs env xs cs in let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs; - cs, ts, te, Con.Env.from_list2 (List.map (fun c -> c.T.con) cs) ks + cs, ts, te, Con.Set.of_list (List.map (fun c -> c.T.con) cs) and check_typ_bounds env (tbs : T.bind list) typs at : T.typ list = match tbs, typs with @@ -477,8 +470,7 @@ and infer_exp' env exp : T.typ = | BlockE (decs, ot) -> let t, scope = infer_block env decs exp.at in let t' = - let to_avoid = Con.set_of_env scope.con_env in - try T.avoid to_avoid t with T.Unavoidable c -> + try T.avoid scope.con_set t with T.Unavoidable c -> error env exp.at "local class type %s is contained in inferred block type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) @@ -605,8 +597,7 @@ and infer_exp' env exp : T.typ = | DecE (dec, ot) -> let t, scope = infer_block env [dec] exp.at in let t' = - let to_avoid = Con.set_of_env scope.con_env in - try T.avoid to_avoid t with T.Unavoidable c -> + try T.avoid scope.con_set t with T.Unavoidable c -> error env exp.at "local class name %s is contained in inferred declaration type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) in @@ -1072,14 +1063,14 @@ and print_ve = and infer_block_decs env decs : scope = let scope = gather_block_typdecs env decs in let env' = adjoin {env with pre = true} scope in - let ce = infer_block_typdecs env' decs in - let env'' = adjoin env {scope with con_env = ce} in - let _ce' = infer_block_typdecs env'' decs in + let cs = infer_block_typdecs env' decs in + let env'' = adjoin env {scope with con_set = cs} in + let _cs' = infer_block_typdecs env'' decs in (* TBR: assertion does not work for types with binders, due to stamping *) (* assert (ce = ce'); *) let pre_ve' = gather_block_valdecs env decs in let ve = infer_block_valdecs (adjoin_vals env'' pre_ve') decs in - {scope with val_env = ve; con_env = ce} + {scope with val_env = ve; con_set = cs} (* Pass 1: collect type identifiers and their arity *) @@ -1103,23 +1094,21 @@ and gather_dec_typdecs env scope dec : scope = T.Env.add id.it (T.Func (T.Local, T.Returns, pre_tbs, [T.Pre], [t2])) scope.val_env | _ -> scope.val_env in let te' = T.Env.add con_id.it c scope.typ_env in - let ce' = Con.Env.add c.T.con pre_k scope.con_env in - {val_env = ve'; typ_env = te'; con_env = ce'} + let cs' = Con.Set.add c.T.con scope.con_set in + {val_env = ve'; typ_env = te'; con_set = cs'} (* Pass 2 and 3: infer type definitions *) -and infer_block_typdecs env decs : con_env = - let _env', ce = - List.fold_left (fun (env, ce) dec -> - let ce' = infer_dec_typdecs env dec in - adjoin_cons env ce', Con.Env.adjoin ce ce' - ) (env, Con.Env.empty) decs - in ce - -and infer_dec_typdecs env dec : con_env = +and infer_block_typdecs env decs : con_set = + List.fold_left (fun cs dec -> + let cs' = infer_dec_typdecs env dec in + Con.Set.union cs cs' + ) Con.Set.empty decs + +and infer_dec_typdecs env dec : con_set = match dec.it with | ExpD _ | LetD _ | VarD _ | FuncD _ -> - Con.Env.empty + Con.Set.empty | TypD (con_id, binds, typ) -> let c = T.Env.find con_id.it env.typs in let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in @@ -1129,7 +1118,7 @@ and infer_dec_typdecs env dec : con_env = let k = T.Def (tbs, T.close cs t) in T.set_kind c k; con_id.note <- Some c; - Con.Env.singleton c.T.con k + Con.Set.singleton c.T.con | ClassD (id, con_id, binds, sort, pat, self_id, fields) -> let c = T.Env.find con_id.it env.typs in let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in @@ -1141,7 +1130,7 @@ and infer_dec_typdecs env dec : con_env = let k = T.Def (tbs, T.close cs t) in T.set_kind c k; con_id.note <- Some c; - Con.Env.singleton c.T.con k + Con.Set.singleton c.T.con (* Pass 4: collect value identifiers *) and gather_block_valdecs env decs : val_env = diff --git a/src/typing.mli b/src/typing.mli index 35a71b49292..e4e2945c0f3 100644 --- a/src/typing.mli +++ b/src/typing.mli @@ -2,12 +2,12 @@ open Type type val_env = typ Env.t type typ_env = con Env.t -type con_env = Type.con_env +type con_set = Type.con_set type scope = { val_env : val_env; typ_env : typ_env; - con_env : con_env; + con_set : con_set; } val empty_scope : scope From 933c928f8abfaeb6045fd75dbfd06d4f2fb118b0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 14:51:38 +0100 Subject: [PATCH 17/42] Actually, get rid of `Typing.con_set` it is always the range of `typ_env` anyways. This simplifies a few more functions. --- src/con.ml | 2 -- src/con.mli | 2 -- src/pipeline.ml | 13 ++++----- src/typing.ml | 74 ++++++++++++++++++++++--------------------------- src/typing.mli | 2 -- 5 files changed, 38 insertions(+), 55 deletions(-) diff --git a/src/con.ml b/src/con.ml index 8615b73652d..7e250361582 100644 --- a/src/con.ml +++ b/src/con.ml @@ -22,5 +22,3 @@ let to_string c = module Env = Env.Make(struct type t = con let compare = compare end) module Set = Set.Make(struct type t = con let compare = compare end) - -let set_of_env m = Env.fold (fun v _ m -> Set.add v m) m Set.empty diff --git a/src/con.mli b/src/con.mli index bdaac3463c3..8c61cc07a0c 100644 --- a/src/con.mli +++ b/src/con.mli @@ -8,5 +8,3 @@ val to_string : t -> string module Env : Env.S with type key = t module Set : Set.S with type elt = t - -val set_of_env : 'a Env.t -> Set.t diff --git a/src/pipeline.ml b/src/pipeline.ml index 2d607d6c847..c611d6c999f 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -15,13 +15,10 @@ let phase heading name = let error at cat text = Error { Diag.sev = Diag.Error; at; cat; text } -let print_cs = - Con.Set.iter (fun c -> - printf "temporary TODO" - (* +let print_te = + Type.Env.iter (fun _ c -> let eq, params, typ = Type.strings_of_kind (Type.kind c) in - printf "type %s%s %s %s\n" (Con.to_string c) params eq typ - *) + printf "type %s%s %s %s\n" (Con.to_string c.Type.con) params eq typ ) let print_stat_ve = @@ -41,7 +38,7 @@ let print_dyn_ve scope = ) let print_scope senv scope dve = - print_cs scope.Typing.con_set; + print_te scope.Typing.typ_env; print_dyn_ve senv dve let print_val _senv v t = @@ -111,7 +108,7 @@ let check_prog infer senv name prog if !Flags.trace && !Flags.verbose then begin match r with | Ok ((_, scope), _) -> - print_cs scope.Typing.con_set; + print_te scope.Typing.typ_env; print_stat_ve scope.Typing.val_env; dump_prog Flags.dump_tc prog; | Error _ -> () diff --git a/src/typing.ml b/src/typing.ml index 63e96cf602f..bb0652e09b8 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -19,26 +19,25 @@ let recover f y = recover_with () f y type val_env = T.typ T.Env.t type typ_env = T.con T.Env.t -type con_set = T.con_set type scope = { val_env : val_env; typ_env : typ_env; - con_set : con_set; } let empty_scope : scope = { val_env = T.Env.empty; typ_env = T.Env.empty; - con_set = Con.Set.empty; } let adjoin_scope scope1 scope2 = { val_env = T.Env.adjoin scope1.val_env scope2.val_env; typ_env = T.Env.adjoin scope1.typ_env scope2.typ_env; - con_set = Con.Set.union scope1.con_set scope2.con_set; } +let cons_of_scope scope = + T.Env.fold (fun _name con s -> Con.Set.add con.T.con s) scope.typ_env Con.Set.empty + (* Contexts (internal) *) type lab_env = T.typ T.Env.t @@ -100,7 +99,7 @@ let adjoin c scope = } let adjoin_vals c ve = {c with vals = T.Env.adjoin c.vals ve} -let adjoin_typs c te ce = +let adjoin_typs c te = { c with typs = T.Env.adjoin c.typs te; } @@ -155,8 +154,8 @@ and check_typ' env typ : T.typ = | TupT typs -> T.Tup (List.map (check_typ env) typs) | FuncT (sort, binds, typ1, typ2) -> - let cs, ts, te, ce = check_typ_binds env binds in - let env' = adjoin_typs env te ce in + let cs, ts, te = check_typ_binds env binds in + let env' = adjoin_typs env te in let typs1 = as_seqT typ1 in let typs2 = as_seqT typ2 in let ts1 = List.map (check_typ env') typs1 in @@ -206,7 +205,7 @@ and check_typ_field env s typ_field : T.field = id.it (T.string_of_typ_expand t); {T.name = id.it; typ = t} -and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_set = +and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env = let xs = List.map (fun typ_bind -> typ_bind.it.var.it) typ_binds in let cs = List.map (fun n -> T.fresh_con n (T.Abs ([], T.Pre))) xs in let te = List.fold_left2 (fun te typ_bind c -> @@ -222,7 +221,7 @@ and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_set let env' = add_typs env xs cs in let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs; - cs, ts, te, Con.Set.of_list (List.map (fun c -> c.T.con) cs) + cs, ts, te and check_typ_bounds env (tbs : T.bind list) typs at : T.typ list = match tbs, typs with @@ -470,7 +469,7 @@ and infer_exp' env exp : T.typ = | BlockE (decs, ot) -> let t, scope = infer_block env decs exp.at in let t' = - try T.avoid scope.con_set t with T.Unavoidable c -> + try T.avoid (cons_of_scope scope) t with T.Unavoidable c -> error env exp.at "local class type %s is contained in inferred block type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) @@ -597,7 +596,7 @@ and infer_exp' env exp : T.typ = | DecE (dec, ot) -> let t, scope = infer_block env [dec] exp.at in let t' = - try T.avoid scope.con_set t with T.Unavoidable c -> + try T.avoid (cons_of_scope scope) t with T.Unavoidable c -> error env exp.at "local class name %s is contained in inferred declaration type\n %s" (Con.to_string c.T.con) (T.string_of_typ_expand t) in @@ -968,8 +967,8 @@ and infer_dec env dec : T.typ = | FuncD (sort, id, typ_binds, pat, typ, exp) -> let t = T.Env.find id.it env.vals in if not env.pre then begin - let _cs, _ts, te, ce = check_typ_binds env typ_binds in - let env' = adjoin_typs env te ce in + let _cs, _ts, te = check_typ_binds env typ_binds in + let env' = adjoin_typs env te in let _, ve = infer_pat_exhaustive env' pat in let t2 = check_typ env' typ in let env'' = @@ -980,8 +979,8 @@ and infer_dec env dec : T.typ = | ClassD (id, con_id, typ_binds, sort, pat, self_id, fields) -> let t = T.Env.find id.it env.vals in if not env.pre then begin - let cs, _ts, te, ce = check_typ_binds env typ_binds in - let env' = adjoin_typs env te ce in + let cs, _ts, te = check_typ_binds env typ_binds in + let env' = adjoin_typs env te in let _, ve = infer_pat_exhaustive env' pat in let env'' = {env' with labs = T.Env.empty; rets = None; async = false} in @@ -1063,14 +1062,14 @@ and print_ve = and infer_block_decs env decs : scope = let scope = gather_block_typdecs env decs in let env' = adjoin {env with pre = true} scope in - let cs = infer_block_typdecs env' decs in - let env'' = adjoin env {scope with con_set = cs} in - let _cs' = infer_block_typdecs env'' decs in + infer_block_typdecs env' decs; + let env'' = adjoin env scope in + infer_block_typdecs env'' decs; (* TBR: assertion does not work for types with binders, due to stamping *) (* assert (ce = ce'); *) let pre_ve' = gather_block_valdecs env decs in let ve = infer_block_valdecs (adjoin_vals env'' pre_ve') decs in - {scope with val_env = ve; con_set = cs} + {scope with val_env = ve} (* Pass 1: collect type identifiers and their arity *) @@ -1094,43 +1093,36 @@ and gather_dec_typdecs env scope dec : scope = T.Env.add id.it (T.Func (T.Local, T.Returns, pre_tbs, [T.Pre], [t2])) scope.val_env | _ -> scope.val_env in let te' = T.Env.add con_id.it c scope.typ_env in - let cs' = Con.Set.add c.T.con scope.con_set in - {val_env = ve'; typ_env = te'; con_set = cs'} + {val_env = ve'; typ_env = te'} (* Pass 2 and 3: infer type definitions *) -and infer_block_typdecs env decs : con_set = - List.fold_left (fun cs dec -> - let cs' = infer_dec_typdecs env dec in - Con.Set.union cs cs' - ) Con.Set.empty decs +and infer_block_typdecs env decs = + List.iter (infer_dec_typdecs env) decs -and infer_dec_typdecs env dec : con_set = +and infer_dec_typdecs env dec = match dec.it with - | ExpD _ | LetD _ | VarD _ | FuncD _ -> - Con.Set.empty + | ExpD _ | LetD _ | VarD _ | FuncD _ -> () | TypD (con_id, binds, typ) -> let c = T.Env.find con_id.it env.typs in - let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in - let env' = adjoin_typs env te ce in + let cs, ts, te = check_typ_binds {env with pre = true} binds in + let env' = adjoin_typs env te in let t = check_typ env' typ in let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in let k = T.Def (tbs, T.close cs t) in T.set_kind c k; - con_id.note <- Some c; - Con.Set.singleton c.T.con + con_id.note <- Some c | ClassD (id, con_id, binds, sort, pat, self_id, fields) -> let c = T.Env.find con_id.it env.typs in - let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in - let env' = adjoin_typs {env with pre = true} te ce in + let cs, ts, te = check_typ_binds {env with pre = true} binds in + let env' = adjoin_typs {env with pre = true} te in let _, ve = infer_pat env' pat in let self_typ = T.Con(c, List.map (fun c -> T.Con (c, [])) cs) in let t = infer_obj (adjoin_vals env' ve) sort.it self_id (Some self_typ) fields in let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in let k = T.Def (tbs, T.close cs t) in T.set_kind c k; - con_id.note <- Some c; - Con.Set.singleton c.T.con + con_id.note <- Some c (* Pass 4: collect value identifiers *) and gather_block_valdecs env decs : val_env = @@ -1168,8 +1160,8 @@ and infer_dec_valdecs env dec : val_env = let t = infer_exp {env with pre = true} exp in T.Env.singleton id.it (T.Mut t) | FuncD (sort, id, typ_binds, pat, typ, exp) -> - let cs, ts, te, ce = check_typ_binds env typ_binds in - let env' = adjoin_typs env te ce in + let cs, ts, te = check_typ_binds env typ_binds in + let env' = adjoin_typs env te in let t1, _ = infer_pat {env' with pre = true} pat in let t2 = check_typ env' typ in if not env.pre && sort.it = T.Sharable then begin @@ -1201,8 +1193,8 @@ and infer_dec_valdecs env dec : val_env = | TypD _ -> T.Env.empty | ClassD (id, con_id, typ_binds, sort, pat, self_id, fields) -> - let cs, ts, te, ce = check_typ_binds env typ_binds in - let env' = adjoin_typs env te ce in + let cs, ts, te = check_typ_binds env typ_binds in + let env' = adjoin_typs env te in let c = T.Env.find con_id.it env.typs in let t1, _ = infer_pat {env' with pre = true} pat in let ts1 = match pat.it with TupP _ -> T.as_seq t1 | _ -> [t1] in diff --git a/src/typing.mli b/src/typing.mli index e4e2945c0f3..639813ec489 100644 --- a/src/typing.mli +++ b/src/typing.mli @@ -2,12 +2,10 @@ open Type type val_env = typ Env.t type typ_env = con Env.t -type con_set = Type.con_set type scope = { val_env : val_env; typ_env : typ_env; - con_set : con_set; } val empty_scope : scope From 0838bc82e58db545b6b2b159e51abec61f862f23 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 14:52:55 +0100 Subject: [PATCH 18/42] Delete definition of `Type.con_env` --- src/check_ir.ml | 1 - src/type.ml | 2 -- src/type.mli | 1 - src/typing.ml | 19 ------------------- 4 files changed, 23 deletions(-) diff --git a/src/check_ir.ml b/src/check_ir.ml index 31c1082cc52..78a12e65aaf 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -25,7 +25,6 @@ let immute_typ p = (* Scope (the external interface) *) type val_env = T.typ T.Env.t -type con_env = T.con_env type scope = { val_env : val_env; diff --git a/src/type.ml b/src/type.ml index 5e9acd7d338..6a11baf380a 100644 --- a/src/type.ml +++ b/src/type.ml @@ -59,8 +59,6 @@ let modify_kind c f = c.kind := f !(c.kind) let compare_field {name=n;_} {name=m;_} = compare n m -type con_env = kind Con.Env.t - let seq ts = match ts with | [t] -> t diff --git a/src/type.mli b/src/type.mli index c405e6a1920..206a89d65b4 100644 --- a/src/type.mli +++ b/src/type.mli @@ -47,7 +47,6 @@ and kind = | Def of bind list * typ | Abs of bind list * typ -type con_env = kind Con.Env.t type con_set = Con.Set.t val kind : con -> kind diff --git a/src/typing.ml b/src/typing.ml index bb0652e09b8..ed53e2a9b52 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -78,14 +78,6 @@ let warn 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_con c con k = {c with cons = Con.Env.add con k c.cons} -let add_typ c x con k = - { c with - typs = T.Env.add x con c.typs; - cons = Con.Env.add con k c.cons; - } -*) let add_typs c xs cs = { c with @@ -1047,17 +1039,6 @@ and check_dec env t dec = local_error env dec.at "expression of type\n %s\ncannot produce expected type\n %s" (T.string_of_typ_expand t') (T.string_of_typ_expand t) -(* -and print_ce = - Con.Env.iter (fun c k -> - Printf.printf " type %s %s\n" (Con.to_string c) (Type.string_of_kind k) - ) -and print_ve = - Type.Env.iter (fun x t -> - Printf.printf " %s : %s\n" x (Type.string_of_typ t) - ) -*) - and infer_block_decs env decs : scope = let scope = gather_block_typdecs env decs in From 5eb9c5778a91fdea9d91699bc2fff5d440d9a58e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 15:23:49 +0100 Subject: [PATCH 19/42] Make `kind` a field and type parameter of `Con.t` --- src/arrange_ir.ml | 2 +- src/arrange_type.ml | 2 +- src/check_ir.ml | 4 ++-- src/con.ml | 15 ++++++++------- src/con.mli | 14 +++++++------- src/pipeline.ml | 2 +- src/tailcall.ml | 2 +- src/type.ml | 44 ++++++++++++++++++++++---------------------- src/type.mli | 5 +++-- src/typing.ml | 16 ++++++++-------- 10 files changed, 54 insertions(+), 52 deletions(-) diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index 234826c81e2..4ec61a9e6c0 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -71,7 +71,7 @@ and dec d = match d.it with "TypD" $$ [con c; kind (Type.kind c)] and typ_bind (tb : typ_bind) = - Con.to_string tb.it.con.Type.con $$ [typ tb.it.bound] + 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 843961237d1..fa1b4d5271d 100644 --- a/src/arrange_type.ml +++ b/src/arrange_type.ml @@ -31,7 +31,7 @@ let prim p = match p with | Char -> Atom "Char" | Text -> Atom "Text" -let con c = Atom (Con.to_string c.con) +let con c = Atom (Con.to_string c) let rec typ (t:Type.typ) = match t with | Var (s, i) -> "Var" $$ [Atom s; Atom (string_of_int i)] diff --git a/src/check_ir.ml b/src/check_ir.ml index 78a12e65aaf..43f0df5e793 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -675,7 +675,7 @@ and check_open_typ_binds env typ_binds = () and close_typ_binds cs tbs = - List.map (fun {con; bound} -> {Type.var = Con.name con.T.con; bound = Type.close cs bound}) tbs + List.map (fun {con; bound} -> {Type.var = Con.name con; bound = Type.close cs bound}) tbs and check_dec env dec = (* helpers *) @@ -767,7 +767,7 @@ and gather_dec env scope dec : scope = | _ -> 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.T.con; bound = T.close cs t}) cs ts 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 { val_env = ve' } diff --git a/src/con.ml b/src/con.ml index 7e250361582..48b264266b6 100644 --- a/src/con.ml +++ b/src/con.ml @@ -1,24 +1,25 @@ -type con = {name : string; stamp : int} -type t = con +type 'a con = {name : string; stamp : int; kind : 'a} +type 'a t = 'a con module Stamps = Env.Make(String) let stamps : int Stamps.t ref = ref Stamps.empty -let fresh name = +let fresh name kind = let n = match Stamps.find_opt name !stamps with | Some n -> n | None -> 0 in stamps := Stamps.add name (n + 1) !stamps; - {name; stamp = n} + {name; stamp = n; kind} let name c = c.name +let kind c = c.kind + let to_string c = if c.stamp = 0 then c.name else Printf.sprintf "%s/%i" c.name c.stamp - -module Env = Env.Make(struct type t = con let compare = compare end) -module Set = Set.Make(struct type t = con let compare = compare end) +let compare c1 c2 = compare (c1.name, c1.stamp) (c2.name, c2.stamp) +let eq c1 c2 = (c1.name, c1.stamp) = (c2.name, c2.stamp) diff --git a/src/con.mli b/src/con.mli index 8c61cc07a0c..4886cd36e0c 100644 --- a/src/con.mli +++ b/src/con.mli @@ -1,10 +1,10 @@ (* Generative constructors *) -type t +type 'a t -val fresh : string -> t -val name : t -> string -val to_string : t -> string - -module Env : Env.S with type key = t -module Set : Set.S with type elt = t +val fresh : string -> 'a -> 'a t +val kind : 'a t -> 'a +val name : 'a t -> string +val to_string : 'a t -> string +val eq : 'a t -> 'a t -> bool +val compare : 'a t -> 'a t -> int diff --git a/src/pipeline.ml b/src/pipeline.ml index c611d6c999f..f85252b9b39 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -18,7 +18,7 @@ let error at cat text = let print_te = Type.Env.iter (fun _ c -> let eq, params, typ = Type.strings_of_kind (Type.kind c) in - printf "type %s%s %s %s\n" (Con.to_string c.Type.con) params eq typ + printf "type %s%s %s %s\n" (Con.to_string c) params eq typ ) let print_stat_ve = diff --git a/src/tailcall.ml b/src/tailcall.ml index 67fdbcf8733..cb832b62015 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 : typ_bind list) insts = List.for_all2 (fun (tb : typ_bind) inst -> match inst with - | Con(c2,[]) -> tb.it.con.Type.con = c2.Type.con (* conservative, but safe *) + | Con(c2,[]) -> Con.eq tb.it.con c2 (* conservative, but safe *) | _ -> false ) tbs insts diff --git a/src/type.ml b/src/type.ml index 6a11baf380a..5109f6f8c16 100644 --- a/src/type.ml +++ b/src/type.ml @@ -37,7 +37,7 @@ and typ = | Pre (* pre-type *) and kind_field = kind ref (* abstract, only this module knows its a ref *) -and con = { con : Con.t; kind : kind_field } +and con = kind_field Con.t and bind = {var : string; bound : typ} and field = {name : string; typ : typ} @@ -50,10 +50,10 @@ and kind = (* The con field is a reference to break the recursion in open_binds, and to allow the multiple passes in typing *) -let kind con = !(con.kind) +let kind con = !(Con.kind con) -let fresh_con n k = { con = Con.fresh n; kind = ref k } -let modify_kind c f = c.kind := f !(c.kind) +let fresh_con n k = Con.fresh n (ref k) +let modify_kind c f = Con.kind c := f !(Con.kind c) (* field ordering *) @@ -138,20 +138,21 @@ and shift_field i n {name; typ} = (* First-order substitution *) +module ConEnv = Env.Make(struct type t = con let compare = Con.compare end) let rec subst sigma t = - if sigma = Con.Env.empty then t else + if sigma = ConEnv.empty then t else match t with | Prim _ | Var _ -> t | Con (c, ts) -> - (match Con.Env.find_opt c.con sigma with + (match ConEnv.find_opt c sigma with | Some t -> assert (List.length ts = 0); t | None -> Con (c, List.map (subst sigma) ts) ) | Array t -> Array (subst sigma t) | Tup ts -> Tup (List.map (subst sigma) ts) | Func (s, c, tbs, ts1, ts2) -> - let sigma' = Con.Env.map (shift 0 (List.length tbs)) sigma in + let sigma' = ConEnv.map (shift 0 (List.length tbs)) sigma in Func (s, c, List.map (subst_bind sigma') tbs, List.map (subst sigma') ts1, List.map (subst sigma') ts2) | Opt t -> Opt (subst sigma t) @@ -174,9 +175,8 @@ and subst_field sigma {name; typ} = let close cs t = if cs = [] then t else - let cons = List.map (fun c -> c.con) cs in - let ts = List.mapi (fun i c -> Var (Con.name c, i)) cons in - let sigma = List.fold_right2 Con.Env.add cons ts Con.Env.empty in + let ts = List.mapi (fun i c -> Var (Con.name c, i)) cs in + let sigma = List.fold_right2 ConEnv.add cs ts ConEnv.empty in subst sigma t let close_binds cs tbs = @@ -215,11 +215,10 @@ let open_ ts t = let open_binds tbs = if tbs = [] then [] else - let cs = List.map (fun {var; _} -> Con.fresh var) tbs in - let ps = List.map (fun _ -> ref (Abs ([],Pre))) tbs in - let ts = List.map2 (fun con kind-> Con ({con;kind}, [])) cs ps in + let cs = List.map (fun {var; _} -> fresh_con var (Abs ([],Pre))) tbs in + let ts = List.map (fun con -> Con (con, [])) cs in let ks = List.map (fun {bound; _} -> Abs ([], open_ ts bound)) tbs in - List.iter2 (fun p k -> p := k) ps ks; + List.iter2 (fun c k -> Con.kind c := k) cs ks; ts @@ -342,12 +341,13 @@ let rec span = function exception Unavoidable of con -type con_set = Con.Set.t +module ConSet = Set.Make(struct type t = con let compare = Con.compare end) +type con_set = ConSet.t let rec avoid' to_avoid = function | (Prim _ | Var _ | Any | Non | Shared | Pre) as t -> t | Con (c, ts) -> - if Con.Set.mem c.con to_avoid + if ConSet.mem c to_avoid then match kind c with | Abs _ -> raise (Unavoidable c) | Def (tbs, t) -> avoid' to_avoid (reduce tbs t ts) @@ -379,7 +379,7 @@ and avoid_field to_avoid {name; typ} = {name; typ = avoid' to_avoid typ} let avoid to_avoid t = - if to_avoid = Con.Set.empty then t else + if to_avoid = ConSet.empty then t else avoid' to_avoid t @@ -410,7 +410,7 @@ let rec rel_typ rel eq t1 t2 = rel_typ rel eq (open_ ts1 t) t2 | _, Def (tbs, t) -> (* TBR this may fail to terminate *) rel_typ rel eq t1 (open_ ts2 t) - | _ when con1.con = con2.con -> + | _ when Con.eq con1 con2 -> rel_list eq_typ rel eq ts1 ts2 | Abs (tbs, t), _ when rel != eq -> rel_typ rel eq (open_ ts1 t) t2 @@ -523,8 +523,8 @@ and eq_kind k1 k2 : bool = | _ -> false (* Moved here to use eq_kind *) -let set_kind c k = match !(c.kind) with - | Abs (_, Pre) -> c.kind := k +let set_kind c k = match !(Con.kind c) with + | Abs (_, Pre) -> Con.kind c := k (* This safeguards against mutating redefinitions *) | k' when eq_kind k k' -> () | _ -> raise (Invalid_argument "set_kind") @@ -606,9 +606,9 @@ let rec string_of_typ_nullary vs = function | Shared -> "Shared" | Prim p -> string_of_prim p | Var (s, i) -> (try string_of_var (List.nth vs i) with _ -> assert false) - | Con (c, []) -> string_of_con vs c.con + | Con (c, []) -> string_of_con vs c | Con (c, ts) -> - sprintf "%s<%s>" (string_of_con vs c.con) + sprintf "%s<%s>" (string_of_con vs c) (String.concat ", " (List.map (string_of_typ' vs) ts)) | Tup ts -> sprintf "(%s%s)" diff --git a/src/type.mli b/src/type.mli index 206a89d65b4..6fea48f3a7f 100644 --- a/src/type.mli +++ b/src/type.mli @@ -42,12 +42,13 @@ and field = {name : string; typ : typ} (* cons and kinds *) and kind_field (* abstract *) -and con = { con : Con.t; kind : kind_field } +and con = kind_field Con.t and kind = | Def of bind list * typ | Abs of bind list * typ -type con_set = Con.Set.t +module ConSet : Set.S with type elt = con +type con_set = ConSet.t val kind : con -> kind val fresh_con : string -> kind -> con diff --git a/src/typing.ml b/src/typing.ml index ed53e2a9b52..9d87691084f 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -36,7 +36,7 @@ let adjoin_scope scope1 scope2 = } let cons_of_scope scope = - T.Env.fold (fun _name con s -> Con.Set.add con.T.con s) scope.typ_env Con.Set.empty + T.Env.fold (fun _name con s -> T.ConSet.add con s) scope.typ_env T.ConSet.empty (* Contexts (internal) *) @@ -168,7 +168,7 @@ and check_typ' env typ : T.typ = (T.string_of_typ_expand (T.seq ts2)) ) end; - let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = t}) cs ts in T.Func (sort.it, c, T.close_binds cs tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2) | OptT typ -> T.Opt (check_typ env typ) @@ -463,7 +463,7 @@ and infer_exp' env exp : T.typ = let t' = try T.avoid (cons_of_scope scope) t with T.Unavoidable c -> error env exp.at "local class type %s is contained in inferred block type\n %s" - (Con.to_string c.T.con) + (Con.to_string c) (T.string_of_typ_expand t) in ot := t'; @@ -590,7 +590,7 @@ and infer_exp' env exp : T.typ = let t' = try T.avoid (cons_of_scope scope) t with T.Unavoidable c -> error env exp.at "local class name %s is contained in inferred declaration type\n %s" - (Con.to_string c.T.con) (T.string_of_typ_expand t) + (Con.to_string c) (T.string_of_typ_expand t) in ot := t'; t' @@ -1089,7 +1089,7 @@ and infer_dec_typdecs env dec = let cs, ts, te = check_typ_binds {env with pre = true} binds in let env' = adjoin_typs env te in let t = check_typ env' typ in - let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in let k = T.Def (tbs, T.close cs t) in T.set_kind c k; con_id.note <- Some c @@ -1100,7 +1100,7 @@ and infer_dec_typdecs env dec = let _, ve = infer_pat env' pat in let self_typ = T.Con(c, List.map (fun c -> T.Con (c, [])) cs) in let t = infer_obj (adjoin_vals env' ve) sort.it self_id (Some self_typ) fields in - let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in let k = T.Def (tbs, T.close cs t) in T.set_kind c k; con_id.note <- Some c @@ -1168,7 +1168,7 @@ and infer_dec_valdecs env dec : val_env = | T.Sharable, (AsyncT _) -> T.Promises (* TBR: do we want this for T.Local too? *) | _ -> T.Returns in - let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in T.Env.singleton id.it (T.Func (sort.it, c, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2)) | TypD _ -> @@ -1180,7 +1180,7 @@ and infer_dec_valdecs env dec : val_env = let t1, _ = infer_pat {env' with pre = true} pat in let ts1 = match pat.it with TupP _ -> T.as_seq t1 | _ -> [t1] in let t2 = T.Con (c, List.map (fun c -> T.Con (c, [])) cs) in - let tbs = List.map2 (fun c t -> {T.var = Con.name c.T.con; bound = T.close cs t}) cs ts in + let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in T.Env.singleton id.it (T.Func (T.Local, T.Returns, tbs, List.map (T.close cs) ts1, [T.close cs t2])) From 2b6da663734219a25f2242f54622e571fd287c3b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 Feb 2019 15:45:09 +0100 Subject: [PATCH 20/42] Write an .mli file for `Check_ir` which uncovers some dead code. --- src/async.ml | 7 ++++--- src/awaitopt.ml | 5 +++-- src/check_ir.ml | 24 ++++++------------------ src/check_ir.mli | 10 ++++++++++ 4 files changed, 23 insertions(+), 23 deletions(-) create mode 100644 src/check_ir.mli diff --git a/src/async.ml b/src/async.ml index 98706670032..ca61ad849e2 100644 --- a/src/async.ml +++ b/src/async.ml @@ -401,9 +401,10 @@ let check_typ env typ = | _ -> () let check_prog scope prog = - let env = { (Check_ir.env_of_scope scope) with - Check_ir.check_exp = check_exp; - Check_ir.check_typ = check_typ } + let env = + Check_ir.env_of_scope scope |> + Check_ir.with_check_exp check_exp |> + Check_ir.with_check_typ check_typ in Check_ir.check_prog env prog diff --git a/src/awaitopt.ml b/src/awaitopt.ml index a44c79be4ff..f9f86617398 100644 --- a/src/awaitopt.ml +++ b/src/awaitopt.ml @@ -569,8 +569,9 @@ let check_exp env exp = | _ -> () let check_prog scope prog = - let env = { (Check_ir.env_of_scope scope) with - Check_ir.check_exp = check_exp } + let env = + Check_ir.env_of_scope scope |> + Check_ir.with_check_exp check_exp in Check_ir.check_prog env prog diff --git a/src/check_ir.ml b/src/check_ir.ml index 43f0df5e793..46b8b077630 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -22,7 +22,7 @@ let immute_typ p = assert (not (T.is_mut (typ p))); (typ p) -(* Scope (the external interface) *) +(* Scope *) type val_env = T.typ T.Env.t @@ -34,11 +34,7 @@ let empty_scope : scope = { val_env = T.Env.empty; } -let adjoin_scope scope1 scope2 = - { val_env = T.Env.adjoin scope1.val_env scope2.val_env; - } - -(* Contexts (internal) *) +(* Contexts *) type lab_env = T.typ T.Env.t type ret_env = T.typ option @@ -53,7 +49,7 @@ type env = check_typ : env -> Type.typ -> unit; } -let env_of_scope scope : env = +let env_of_scope (scope : Typing.scope) : env = { vals = scope.Typing.val_env; labs = T.Env.empty; rets = None; @@ -62,6 +58,9 @@ let env_of_scope scope : env = check_typ = (fun _ _ -> ()); } +let with_check_exp check_exp env = { env with check_exp } +let with_check_typ check_typ env = { env with check_typ } + (* More error bookkeeping *) let type_error at text : Diag.message = Diag.{ sev = Diag.Error; at; cat = "IR type"; text } @@ -229,9 +228,6 @@ let type_lit env lit at : T.prim = open Ir -let string_of_exp exp = Wasm.Sexpr.to_string 80 (Arrange_ir.exp exp) -let string_of_dec exp = Wasm.Sexpr.to_string 80 (Arrange_ir.dec exp) - (* Expressions *) let isAsyncE exp = @@ -660,14 +656,6 @@ and type_block_exps env decs : T.typ = check_dec env dec; type_block_exps env decs' -and cons_of_typ_binds typ_binds = - let con_of_typ_bind tp = - match tp.note with - | T.Con(c,[]) -> c - | _ -> assert false (* TODO: remove me by tightening note to Con.t *) - in - List.map con_of_typ_bind typ_binds - and check_open_typ_binds env typ_binds = let cs = List.map (fun tp -> tp.it.con) typ_binds in let binds = close_typ_binds cs (List.map (fun tb -> tb.it) typ_binds) in diff --git a/src/check_ir.mli b/src/check_ir.mli new file mode 100644 index 00000000000..838af4dfbe7 --- /dev/null +++ b/src/check_ir.mli @@ -0,0 +1,10 @@ +type env + +val error : env -> Source.region -> ('b, unit, string, 'c) format4 -> 'b + +val env_of_scope : Typing.scope -> env + +val with_check_exp : (env -> Ir.exp -> unit) -> env -> env +val with_check_typ : (env -> Type.typ -> unit) -> env -> env + +val check_prog : env -> Ir.prog -> unit From ceff9e8350f537bf871cbb0c4918d63e0dede2e2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 14 Feb 2019 10:34:52 +0100 Subject: [PATCH 21/42] Address nits --- src/type.ml | 10 +++++----- src/typing.ml | 18 +++++------------- 2 files changed, 10 insertions(+), 18 deletions(-) diff --git a/src/type.ml b/src/type.ml index 5109f6f8c16..ae03dbae19b 100644 --- a/src/type.ml +++ b/src/type.ml @@ -57,7 +57,7 @@ let modify_kind c f = Con.kind c := f !(Con.kind c) (* field ordering *) -let compare_field {name=n;_} {name=m;_} = compare n m +let compare_field f1 f2 = compare f1.name f2.name let seq ts = match ts with @@ -139,6 +139,7 @@ and shift_field i n {name; typ} = (* First-order substitution *) module ConEnv = Env.Make(struct type t = con let compare = Con.compare end) + let rec subst sigma t = if sigma = ConEnv.empty then t else match t with @@ -215,7 +216,7 @@ let open_ ts t = let open_binds tbs = if tbs = [] then [] else - let cs = List.map (fun {var; _} -> fresh_con var (Abs ([],Pre))) tbs in + let cs = List.map (fun {var; _} -> fresh_con var (Abs ([], Pre))) tbs in let ts = List.map (fun con -> Con (con, [])) cs in let ks = List.map (fun {bound; _} -> Abs ([], open_ ts bound)) tbs in List.iter2 (fun c k -> Con.kind c := k) cs ks; @@ -239,9 +240,8 @@ let rec normalize = function let rec promote = function | Con (con, ts) -> - (match kind con with - | Def (tbs, t) | Abs (tbs, t) -> promote (reduce tbs t ts) - ) + let Def (tbs, t) | Abs (tbs, t) = kind con + in promote (reduce tbs t ts) | t -> t diff --git a/src/typing.ml b/src/typing.ml index 9d87691084f..e5414647345 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -78,11 +78,7 @@ let warn 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 xs cs = - { c with - typs = List.fold_right2 T.Env.add xs cs c.typs; - } +let add_typs c xs cs = {c with typs = List.fold_right2 T.Env.add xs cs c.typs} let adjoin c scope = { c with @@ -91,10 +87,7 @@ let adjoin c scope = } let adjoin_vals c ve = {c with vals = T.Env.adjoin c.vals ve} -let adjoin_typs c te = - { c with - typs = T.Env.adjoin c.typs te; - } +let adjoin_typs c te = {c with typs = T.Env.adjoin c.typs te} let disjoint_union env at fmt env1 env2 = try T.Env.disjoint_union env1 env2 @@ -127,8 +120,7 @@ and check_typ' env typ : T.typ = | VarT (id, typs) -> (match T.Env.find_opt id.it env.typs with | Some con -> - let kind = T.kind con in - let T.Def (tbs, t) | T.Abs (tbs, t) = kind in + let T.Def (tbs, t) | T.Abs (tbs, t) = T.kind con in let ts = check_typ_bounds env tbs typs typ.at in T.Con (con, ts) | None -> error env id.at "unbound type identifier %s" id.it @@ -1064,7 +1056,7 @@ and gather_dec_typdecs env scope dec : scope = if T.Env.mem con_id.it scope.typ_env then error env dec.at "duplicate definition for type %s in block" con_id.it; let pre_tbs = List.map (fun bind -> {T.var = bind.it.var.it; bound = T.Pre}) binds in - let pre_k = (T.Abs (pre_tbs, T.Pre)) in + let pre_k = T.Abs (pre_tbs, T.Pre) in let c = T.fresh_con con_id.it pre_k in let ve' = match dec.it with @@ -1078,7 +1070,7 @@ and gather_dec_typdecs env scope dec : scope = (* Pass 2 and 3: infer type definitions *) -and infer_block_typdecs env decs = +and infer_block_typdecs env decs = List.iter (infer_dec_typdecs env) decs and infer_dec_typdecs env dec = From 5ff49b51275c8e12eed751de48b51032d2367ae8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 14 Feb 2019 11:26:00 +0100 Subject: [PATCH 22/42] Better name for the abstract annotations on cons --- src/type.ml | 4 ++-- src/type.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/type.ml b/src/type.ml index 2fa63a594d2..5df393a2b4b 100644 --- a/src/type.ml +++ b/src/type.ml @@ -36,8 +36,8 @@ and typ = | Non (* bottom *) | Pre (* pre-type *) -and kind_field = kind ref (* abstract, only this module knows its a ref *) -and con = kind_field Con.t +and con_annot = kind ref (* the con annotation is abstract to the outside world *) +and con = con_annot Con.t and bind = {var : string; bound : typ} and field = {name : string; typ : typ} diff --git a/src/type.mli b/src/type.mli index 6fea48f3a7f..df790902563 100644 --- a/src/type.mli +++ b/src/type.mli @@ -41,8 +41,8 @@ and field = {name : string; typ : typ} (* cons and kinds *) -and kind_field (* abstract *) -and con = kind_field Con.t +and con_annot (* abstract *) +and con = con_annot Con.t and kind = | Def of bind list * typ | Abs of bind list * typ From ae896ef98c9a62b51ca94276bbddd3078066c008 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Tue, 5 Feb 2019 16:04:02 -0700 Subject: [PATCH 23/42] initial draft; the pass does nothing at all, yet --- src/pipeline.ml | 2 + src/simploop.ml | 95 ++++++++++++++++++++++++++++++++++++++++++++++++ src/simploop.mli | 2 + 3 files changed, 99 insertions(+) create mode 100644 src/simploop.ml create mode 100644 src/simploop.mli diff --git a/src/pipeline.ml b/src/pipeline.ml index f85252b9b39..b2ea64495bb 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -293,6 +293,8 @@ let compile_with check mode name : compile_result = let prog = await_lowering true initial_stat_env prog name in let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in + (* TEMP-Matthew: next line here just to get this module to compile *) + let _ = Simploop.transform initial_stat_env prog in phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_ diff --git a/src/simploop.ml b/src/simploop.ml new file mode 100644 index 00000000000..68d4858f497 --- /dev/null +++ b/src/simploop.ml @@ -0,0 +1,95 @@ +(* + Simplify loop constructs. + + Mapping each occurence of a looping construct to an infinite loop. + *) + +open Source +module I = Ir + +let phrase f x = { x with it = f x.it } + +let phrase' f x = { x with it = f x.at x.note x.it } + +let rec exps es = List.map exp es + +and exp e = phrase' exp' e + +and exp' at note = function + | I.AsyncE _ -> assert false + | I.AwaitE _ -> assert false + | I.PrimE p -> I.PrimE p + | I.VarE i -> I.VarE i + | I.LitE l -> I.LitE l + | I.UnE (ot, o, e) -> + I.UnE (ot, o, exp e) + | I.BinE (ot, e1, o, e2) -> + I.BinE (ot, exp e1, o, exp e2) + | I.RelE (ot, e1, o, e2) -> + I.RelE (ot, exp e1, o, exp e2) + | I.TupE es -> I.TupE (exps es) + | I.ProjE (e, i) -> I.ProjE (exp e, i) + | I.OptE e -> I.OptE (exp e) + | I.DotE (e, n) -> I.DotE(exp e, n) + | I.AssignE (e1, e2) -> I.AssignE (exp e1, exp e2) + | I.ArrayE (m, t, es) -> I.ArrayE (m, t, exps es) + | I.IdxE (e1, e2) -> I.IdxE (exp e1, exp e2) + | I.CallE (cc, e1, inst, e2) -> I.CallE (cc, exp e1, inst, exp e2) + | I.BlockE (ds, ot) -> I.BlockE (decs ds, ot) + | I.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3) + | I.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs) + | I.LabelE (l, t, e) -> I.LabelE (l, t, exp e) + | I.BreakE (l, e) -> I.BreakE (l, exp e) + | I.RetE e -> I.RetE (exp e) + | I.AssertE e -> I.AssertE (exp e) + | I.IsE (e1, e2) -> I.IsE (exp e1, exp e2) + | I.ActorDotE(e, n) -> I.ActorDotE(exp e, n) + | I.DeclareE(i, t, e) -> I.DeclareE(i, t, exp e) + | I.DefineE(i, m, e) -> I.DefineE(i, m, exp e) + | I.NewObjE(s, nis, t) -> I.NewObjE(s, nis, t) + | I.ActorE(i, fs, t) -> I.ActorE(i, exp_fields fs, t) + (*--- "Interesting" cases: The looping constructs. ---*) + | I.LoopE (e1, None) -> I.LoopE (exp e1, None) (* <-- This form is simplest, and preferred *) + | I.LoopE (e1, Some e2) -> I.LoopE (exp e1, Some (exp e2)) (* TODO: Transform this form to LoopE(_,None) *) + | I.WhileE (e1, e2) -> I.WhileE (exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) + | I.ForE (p, e1, e2) -> I.ForE (p, exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) + +and exp_fields fs = List.map exp_field fs + +and exp_field f = phrase exp_field' f + +and exp_field' (f : Ir.exp_field') = + Ir.{ I.name = f.name; I.id = f.id; I.exp = exp f.exp; I.mut = f.mut; I.priv = f.priv } + +and decs ds = + match ds with + | [] -> [] + | d::ds -> (phrase' dec' d) :: (decs ds) + +and dec' at n d = match d with + | I.ExpD e -> I.ExpD (exp e) + | I.LetD (p, e) -> I.LetD (p, exp e) + | I.VarD (i, e) -> I.VarD (i, exp e) + | I.FuncD (cc, i, tbs, p, ty, e) -> + I.FuncD (cc, i, tbs, p, ty, exp e) + | I.TypD (c,k) -> + I.TypD (c,k) + +and cases cs = List.map case cs + +and case c = phrase case' c + +and case' c = I.{ I.pat = c.pat; I.exp = exp c.exp } + +and prog p = phrase decs p + +(* validation *) + +let check_prog scope (prog:I.prog) = + let env = Check_ir.env_of_scope scope in + Check_ir.check_prog env prog + +let transform scope (p:I.prog) = + let p' = prog p in + check_prog scope p'; + p' diff --git a/src/simploop.mli b/src/simploop.mli new file mode 100644 index 00000000000..0b1e6e5e987 --- /dev/null +++ b/src/simploop.mli @@ -0,0 +1,2 @@ +val prog : Ir.prog -> Ir.prog +val transform : Typing.scope -> Ir.prog -> Ir.prog From 3917757ea312fecd6b911df5294d55fa99b19690 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Tue, 5 Feb 2019 16:29:54 -0700 Subject: [PATCH 24/42] sanity check: pipeline still passes all tests --- src/pipeline.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pipeline.ml b/src/pipeline.ml index b2ea64495bb..4be50d48fc8 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -294,7 +294,7 @@ let compile_with check mode name : compile_result = let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in (* TEMP-Matthew: next line here just to get this module to compile *) - let _ = Simploop.transform initial_stat_env prog in + let prog = Simploop.transform initial_stat_env prog in phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_ From 8758f77990809126f4fe0367653b5c92de7bc459 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Wed, 6 Feb 2019 10:28:33 -0700 Subject: [PATCH 25/42] notes and questions about the planned transforms; writing them out should be straightforward, given answers to the questions --- src/simploop.ml | 64 +++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 59 insertions(+), 5 deletions(-) diff --git a/src/simploop.ml b/src/simploop.ml index 68d4858f497..76284d8366f 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -1,7 +1,8 @@ -(* +(* Simplify loop constructs. Mapping each occurence of a looping construct to an infinite loop. + *) open Source @@ -50,9 +51,62 @@ and exp' at note = function | I.ActorE(i, fs, t) -> I.ActorE(i, exp_fields fs, t) (*--- "Interesting" cases: The looping constructs. ---*) | I.LoopE (e1, None) -> I.LoopE (exp e1, None) (* <-- This form is simplest, and preferred *) - | I.LoopE (e1, Some e2) -> I.LoopE (exp e1, Some (exp e2)) (* TODO: Transform this form to LoopE(_,None) *) - | I.WhileE (e1, e2) -> I.WhileE (exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) - | I.ForE (p, e1, e2) -> I.ForE (p, exp e1, exp e2) (* TODO: Transform this form to LoopE(_,None) *) + + (* Questions about the target of each transformation case below: + + 1. Do we need the loop { } expression _and_ the label; does the + label alone suffice? (Can we label any subexpression and make it + a jump target, or only loops?) + + 2. Related to 1, if we do need the loop constructs and the + labels, do we also need to use explicit "continue" expressions? + + 3. The rewrite for for-loops is the most involved, and involves a + subexpression with nontrivial (non-unit, non-boolean) type; + namely, the first subexpression of the for-loop must be an + iterator object. Doing this rewrite without first doing this + check would be wrong, but assuming the AST is typed, no extra + type information seems required to inform or guide the + transformation; it is "fully parametric" in all of the + sub-expressions, it seems. + + Hence, all of these rewrites could probably happen in the desugar + module, though they should only happen on a well-typed source + AST. + *) + + (* Transformation from loop-while to loop: *) + | I.LoopE (e1, Some e2) -> + (* + loop e1 while e2 + ~~> + label l: loop { e1 ; if e2 then break l else continue l } + *) + I.LoopE (exp e1, Some (exp e2)) (* TODO *) + + (* Transformation from while to loop: *) + | I.WhileE (e1, e2) -> + (* + while e1 e2 + ~~> + label l: loop { if e1 then { e2 ; continue l } else break l } + *) + I.WhileE (exp e1, exp e2) (* TODO *) + + (* Transformation from for to loop: *) + | I.ForE (p, e1, e2) -> + (* + for x in e1 e2 + ~~> + label l: loop { + switch e1.next() { + case null { break l }; + case x { e2 ; continue l }; + } + } + *) + I.ForE (p, exp e1, exp e2) (* TODO *) + and exp_fields fs = List.map exp_field fs @@ -72,7 +126,7 @@ and dec' at n d = match d with | I.VarD (i, e) -> I.VarD (i, exp e) | I.FuncD (cc, i, tbs, p, ty, e) -> I.FuncD (cc, i, tbs, p, ty, exp e) - | I.TypD (c,k) -> + | I.TypD (c,k) -> I.TypD (c,k) and cases cs = List.map case cs From 35ba3e0f78c759f09c5e9a5ecf2328c469a9875a Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Thu, 14 Feb 2019 09:20:59 -0800 Subject: [PATCH 26/42] rebase on joachims work; fixup --- src/construct.ml | 33 +++++++++++++++++++++++-- src/construct.mli | 4 +++ src/simploop.ml | 63 +++++++++++++++++++++++++---------------------- 3 files changed, 68 insertions(+), 32 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index f0d00e51cb7..78de4e488a7 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -225,6 +225,36 @@ let loopE exp1 exp2Opt = S.note_typ = Type.Non } } +let loopWhileE' exp1 exp2 = + (* + loop e1 while e2 + ~~> + label l: loop { e1 ; if e2 then break l else continue l } + *) + LoopE(exp1,Some exp2) + +let whileE' exp1 exp2 = + (* + while e1 e2 + ~~> + label l: loop { if e1 then { e2 ; continue l } else break l } + *) + WhileE(exp1,exp2) + +let forE' pat exp1 exp2 = + (* + for x in e1 e2 + ~~> + label l: loop { + switch e1.next() { + case null { break l }; + case x { e2 ; continue l }; + } + } + *) + ForE(pat,exp1,exp2) + + let declare_idE x typ exp1 = { it = DeclareE (x, typ, exp1); at = no_region; @@ -390,5 +420,4 @@ let prim_async typ = primE "@async" (T.Func (T.Local, T.Returns, [], [cpsT typ], [T.Async typ])) let prim_await typ = - primE "@await" (T.Func (T.Local, T.Returns, [], [T.Async typ; contT typ], [])) - + primE "@await" (T.Func (T.Call T.Local, T.Returns, [], [T.Async typ; contT typ], [])) diff --git a/src/construct.mli b/src/construct.mli index a948b69335d..41b2ba282fa 100644 --- a/src/construct.mli +++ b/src/construct.mli @@ -61,6 +61,10 @@ val assignE : exp -> exp -> exp val labelE : Syntax.id -> typ -> exp -> exp val loopE: exp -> exp option -> exp +val whileE' : exp -> exp -> exp' +val loopWhileE' : exp -> exp -> exp' +val forE' : pat -> exp -> exp -> exp' + val declare_idE : Syntax.id -> typ -> exp -> exp val define_idE : Syntax.id -> Syntax.mut -> exp -> exp val newObjE : Syntax.obj_sort -> (Syntax.name * Syntax.id) list -> typ -> exp diff --git a/src/simploop.ml b/src/simploop.ml index 76284d8366f..514316d704e 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -43,7 +43,6 @@ and exp' at note = function | I.BreakE (l, e) -> I.BreakE (l, exp e) | I.RetE e -> I.RetE (exp e) | I.AssertE e -> I.AssertE (exp e) - | I.IsE (e1, e2) -> I.IsE (exp e1, exp e2) | I.ActorDotE(e, n) -> I.ActorDotE(exp e, n) | I.DeclareE(i, t, e) -> I.DeclareE(i, t, exp e) | I.DefineE(i, m, e) -> I.DefineE(i, m, exp e) @@ -58,6 +57,8 @@ and exp' at note = function label alone suffice? (Can we label any subexpression and make it a jump target, or only loops?) + Cladio: No. Loops need not be labeled, except to break. + 2. Related to 1, if we do need the loop constructs and the labels, do we also need to use explicit "continue" expressions? @@ -73,40 +74,43 @@ and exp' at note = function Hence, all of these rewrites could probably happen in the desugar module, though they should only happen on a well-typed source AST. + + ---------------------------------------------------------------------------------------------------------- + Claudio's Answers, copied from here: https://github.com/dfinity-lab/actorscript/pull/146#commitcomment-32218790 + + - I believe you can label any expression and make it a jump target. + + (Matthew: Ok. But because I'd rather not loose all structure, I guess I'll label loops, and not try to create, e.g., strange non-structural loops) + + - There is no need to label the loop unless you do and early break or continue. + + (Matthew: Ok, I seem to need to break every loop that I create, so I guess each needs a label?) + + - The continue in the while translation is redundant, I think; just fall through. + + (Matthew: Ok.) + + - Continue isn't special IRCC, it's just a special named label ("continue-" or something like that) introduced by the parser. + (the loop(_,None) construct just loops forever, but you can still exit via break). + + - I would indeed just do this desugaring in the parser + + (Matthew: Ok, sounds good; I'll keep this separate until it works, then integrate there.) + + - you might even be able to extend construct_ir.ml with functions whileE etc for constructing primitive + loops and modify the transformation to use those instead of WhileE etc. + + (Matthew: Ok. I'll define the RHS of each rewrite in that module, for potential use elsewhere in the pipeline too.) *) (* Transformation from loop-while to loop: *) - | I.LoopE (e1, Some e2) -> - (* - loop e1 while e2 - ~~> - label l: loop { e1 ; if e2 then break l else continue l } - *) - I.LoopE (exp e1, Some (exp e2)) (* TODO *) + | I.LoopE (e1, Some e2) -> Construct.loopWhileE' (exp e1) (exp e2) (* Transformation from while to loop: *) - | I.WhileE (e1, e2) -> - (* - while e1 e2 - ~~> - label l: loop { if e1 then { e2 ; continue l } else break l } - *) - I.WhileE (exp e1, exp e2) (* TODO *) + | I.WhileE (e1, e2) -> Construct.whileE' (exp e1) (exp e2) (* Transformation from for to loop: *) - | I.ForE (p, e1, e2) -> - (* - for x in e1 e2 - ~~> - label l: loop { - switch e1.next() { - case null { break l }; - case x { e2 ; continue l }; - } - } - *) - I.ForE (p, exp e1, exp e2) (* TODO *) - + | I.ForE (p, e1, e2) -> Construct.forE' p (exp e1) (exp e2) and exp_fields fs = List.map exp_field fs @@ -126,8 +130,7 @@ and dec' at n d = match d with | I.VarD (i, e) -> I.VarD (i, exp e) | I.FuncD (cc, i, tbs, p, ty, e) -> I.FuncD (cc, i, tbs, p, ty, exp e) - | I.TypD (c,k) -> - I.TypD (c,k) + | I.TypD c -> I.TypD c and cases cs = List.map case cs From b4a96e180ca81f1d53d7a7beddbf952b88888872 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 04:15:43 -0700 Subject: [PATCH 27/42] move RHS's of loop transforms, stil pending, into Construct module --- src/construct.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/construct.ml b/src/construct.ml index 78de4e488a7..54b1862a781 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -420,4 +420,4 @@ let prim_async typ = primE "@async" (T.Func (T.Local, T.Returns, [], [cpsT typ], [T.Async typ])) let prim_await typ = - primE "@await" (T.Func (T.Call T.Local, T.Returns, [], [T.Async typ; contT typ], [])) + primE "@await" (T.Func (T.Local, T.Returns, [], [T.Async typ; contT typ], [])) From e646622e802315299acb6a32f0288cc805368263 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 04:51:29 -0700 Subject: [PATCH 28/42] 1/3 of the derived loop forms in Construct; triggering WASM test errors --- src/construct.ml | 85 ++++++++++++++++++++++++++++++------------------ 1 file changed, 54 insertions(+), 31 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 54b1862a781..e57272124d0 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -225,36 +225,6 @@ let loopE exp1 exp2Opt = S.note_typ = Type.Non } } -let loopWhileE' exp1 exp2 = - (* - loop e1 while e2 - ~~> - label l: loop { e1 ; if e2 then break l else continue l } - *) - LoopE(exp1,Some exp2) - -let whileE' exp1 exp2 = - (* - while e1 e2 - ~~> - label l: loop { if e1 then { e2 ; continue l } else break l } - *) - WhileE(exp1,exp2) - -let forE' pat exp1 exp2 = - (* - for x in e1 e2 - ~~> - label l: loop { - switch e1.next() { - case null { break l }; - case x { e2 ; continue l }; - } - } - *) - ForE(pat,exp1,exp2) - - let declare_idE x typ exp1 = { it = DeclareE (x, typ, exp1); at = no_region; @@ -299,7 +269,6 @@ let varD x exp = { it = VarD (x, exp); let expD exp = { exp with it = ExpD exp } - (* let expressions (derived) *) let letE x exp1 exp2 = blockE [letD x exp1; expD exp2] @@ -420,4 +389,58 @@ let prim_async typ = primE "@async" (T.Func (T.Local, T.Returns, [], [cpsT typ], [T.Async typ])) let prim_await typ = +<<<<<<< HEAD primE "@await" (T.Func (T.Local, T.Returns, [], [T.Async typ; contT typ], [])) +======= + primE "@await" (T.Func (T.Call T.Local, T.Returns, [], [T.Async typ; contT typ], [])) + +(* derived loop forms; each can be expressed as an unconditional loop *) + +let loopWhileE exp1 exp2 = + (* loop e1 while e2 + ~~> label l: loop { + let () = e1 ; + let x2 = e2 ; + if x2 { break l x1 } else { } } + *) + let id2 = fresh_id exp2.note.S.note_typ in + let lab = fresh_lab () in + let ty1 = Type.unit in + labelE lab ty1 ( + loopE ( + blockE [ + expD exp1 ; + letD id2 exp2 ; + expD (ifE id2 + (breakE lab (tupE []) ty1) + (tupE []) + ty1 + ) + ] + ) None + ) + +(* LoopE(exp1,Some exp2) *) +let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it + +let whileE' exp1 exp2 = + (* + while e1 e2 + ~~> + label l: loop { if e1 then { e2 ; continue l } else break l } + *) + WhileE(exp1,exp2) + +let forE' pat exp1 exp2 = + (* + for x in e1 e2 + ~~> + label l: loop { + switch e1.next() { + case null { break l }; + case x { e2 ; continue l }; + } + } + *) + ForE(pat,exp1,exp2) +>>>>>>> 1/3 of the derived loop forms in Construct; triggering WASM test errors From 669d5426fd97ea22e50cdab5295c21698cfe75ad Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 04:54:32 -0700 Subject: [PATCH 29/42] minor: fix typo in comment --- src/construct.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/construct.ml b/src/construct.ml index e57272124d0..bdaaca9885e 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -401,7 +401,7 @@ let loopWhileE exp1 exp2 = ~~> label l: loop { let () = e1 ; let x2 = e2 ; - if x2 { break l x1 } else { } } + if x2 { break l } else { } } *) let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in From 1a8e45e10fe52213c585521351f14a067e0ebf8b Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 05:13:38 -0700 Subject: [PATCH 30/42] fix bug that I introduced; another xform case passes all tests --- src/construct.ml | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index bdaaca9885e..6f6b4106e88 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -269,6 +269,7 @@ let varD x exp = { it = VarD (x, exp); let expD exp = { exp with it = ExpD exp } + (* let expressions (derived) *) let letE x exp1 exp2 = blockE [letD x exp1; expD exp2] @@ -401,7 +402,7 @@ let loopWhileE exp1 exp2 = ~~> label l: loop { let () = e1 ; let x2 = e2 ; - if x2 { break l } else { } } + if x2 { } else { break } } *) let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in @@ -412,8 +413,8 @@ let loopWhileE exp1 exp2 = expD exp1 ; letD id2 exp2 ; expD (ifE id2 - (breakE lab (tupE []) ty1) (tupE []) + (breakE lab (tupE []) ty1) ty1 ) ] @@ -423,13 +424,30 @@ let loopWhileE exp1 exp2 = (* LoopE(exp1,Some exp2) *) let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it -let whileE' exp1 exp2 = +let whileE exp1 exp2 = (* while e1 e2 ~~> label l: loop { if e1 then { e2 ; continue l } else break l } *) - WhileE(exp1,exp2) + let ty1 = exp1.note.S.note_typ in + let id1 = fresh_id ty1 in + let lab = fresh_lab () in + let ty2 = Type.unit in + labelE lab ty2 ( + loopE ( + blockE [ + letD id1 exp1 ; + expD (ifE id1 + exp2 + (breakE lab (tupE []) ty2) + ty2 + ) + ] + ) None + ) + +let whileE' exp1 exp2 = (whileE exp1 exp2).it let forE' pat exp1 exp2 = (* From 8bfd4d8b73a635f815eb6e7c6fd9d8a5457c834c Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Fri, 8 Feb 2019 06:37:06 -0700 Subject: [PATCH 31/42] stuck: how to get the Con env where I need it? --- src/construct.ml | 76 +++++++++++++++++++++++++++++++++++++----------- 1 file changed, 59 insertions(+), 17 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 6f6b4106e88..f571f45cbac 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -402,7 +402,7 @@ let loopWhileE exp1 exp2 = ~~> label l: loop { let () = e1 ; let x2 = e2 ; - if x2 { } else { break } } + if x2 { } else { break l } } *) let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in @@ -425,10 +425,10 @@ let loopWhileE exp1 exp2 = let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it let whileE exp1 exp2 = - (* - while e1 e2 - ~~> - label l: loop { if e1 then { e2 ; continue l } else break l } + (* while e1 e2 + ~~> label l: loop { + let x1 = e1 ; + if x1 then { e2 } else { break l } } *) let ty1 = exp1.note.S.note_typ in let id1 = fresh_id ty1 in @@ -438,7 +438,7 @@ let whileE exp1 exp2 = loopE ( blockE [ letD id1 exp1 ; - expD (ifE id1 + expD (ifE id1 exp2 (breakE lab (tupE []) ty2) ty2 @@ -449,16 +449,58 @@ let whileE exp1 exp2 = let whileE' exp1 exp2 = (whileE exp1 exp2).it -let forE' pat exp1 exp2 = +let forE pat exp1 exp2 = + (* for p in e1 e2 + ~~> + let x1 = e1 ; + let nxt = e1.next ; + label l: loop { + let x1' = nxt () ; + switch x1' { + case null { break l }; + case p { e2 }; + } + } *) + let lab = fresh_lab () in + let tyu = Type.unit in + let ty1 = exp1.note.S.note_typ in + + (* XXX: not sure how to get type info for `next` function... + - ...how to do I supply a non-empty con_env for `as_obj_sub` ? + *) + let _, tfs = Type.as_obj_sub "next" (Con.Env.from_list []) ty1 in + let tnxt = T.lookup_field "next" tfs in + let ty1_ret = match (T.as_func tnxt) with + | _,_,_,_,[x] -> x + | _ -> failwith "invalid return type" + in + + let id1 = fresh_id ty1 in + let nxt = fresh_id tnxt in + let id1' = fresh_id ty1_ret in (* - for x in e1 e2 - ~~> - label l: loop { - switch e1.next() { - case null { break l }; - case x { e2 ; continue l }; - } - } + Printf.eprintf "XXX ty1 = %s\n" (T.string_of_typ ty1); + Printf.eprintf "XXX tnxt = %s\n" (T.string_of_typ tnxt); + Printf.eprintf "XXX ty1_ret = %s\n" (T.string_of_typ ty1_ret); *) - ForE(pat,exp1,exp2) ->>>>>>> 1/3 of the derived loop forms in Construct; triggering WASM test errors + blockE [ + letD id1 exp1 ; + letD nxt (dotE id1 (nameN "next") tnxt) ; + expD ( + labelE lab tyu ( + loopE ( + blockE [ + letD id1' (callE nxt [] (tupE []) ty1_ret); + expD ( + switch_optE id1 + (breakE lab (tupE []) tyu) + pat exp2 + tyu + ) + ] + ) None + ) + ) + ] + +let forE' pat exp1 exp2 = (forE pat exp1 exp2).it From 1625513c5ec7fae50f4f3936bb8f26ce81689e69 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Mon, 11 Feb 2019 08:46:11 -0800 Subject: [PATCH 32/42] minor: typo --- src/construct.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/construct.ml b/src/construct.ml index f571f45cbac..9a2716a9692 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -453,7 +453,7 @@ let forE pat exp1 exp2 = (* for p in e1 e2 ~~> let x1 = e1 ; - let nxt = e1.next ; + let nxt = x1.next ; label l: loop { let x1' = nxt () ; switch x1' { From 2235771c7925a6f58613cb0ee3f68625ee0de375 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Thu, 14 Feb 2019 09:25:52 -0800 Subject: [PATCH 33/42] fix merge --- src/construct.ml | 7 ++----- src/simploop.ml | 9 --------- 2 files changed, 2 insertions(+), 14 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 9a2716a9692..1619a7ef83e 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -390,10 +390,7 @@ let prim_async typ = primE "@async" (T.Func (T.Local, T.Returns, [], [cpsT typ], [T.Async typ])) let prim_await typ = -<<<<<<< HEAD primE "@await" (T.Func (T.Local, T.Returns, [], [T.Async typ; contT typ], [])) -======= - primE "@await" (T.Func (T.Call T.Local, T.Returns, [], [T.Async typ; contT typ], [])) (* derived loop forms; each can be expressed as an unconditional loop *) @@ -468,7 +465,7 @@ let forE pat exp1 exp2 = (* XXX: not sure how to get type info for `next` function... - ...how to do I supply a non-empty con_env for `as_obj_sub` ? *) - let _, tfs = Type.as_obj_sub "next" (Con.Env.from_list []) ty1 in + let _, tfs = Type.as_obj_sub "next" ty1 in let tnxt = T.lookup_field "next" tfs in let ty1_ret = match (T.as_func tnxt) with | _,_,_,_,[x] -> x @@ -492,7 +489,7 @@ let forE pat exp1 exp2 = blockE [ letD id1' (callE nxt [] (tupE []) ty1_ret); expD ( - switch_optE id1 + switch_optE id1' (breakE lab (tupE []) tyu) pat exp2 tyu diff --git a/src/simploop.ml b/src/simploop.ml index a6d9dbac0cf..514316d704e 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -43,10 +43,6 @@ and exp' at note = function | I.BreakE (l, e) -> I.BreakE (l, exp e) | I.RetE e -> I.RetE (exp e) | I.AssertE e -> I.AssertE (exp e) -<<<<<<< HEAD -======= - | I.IsE (e1, e2) -> I.IsE (exp e1, exp e2) ->>>>>>> c28bf054473d6344e0a83dc68c281008ea7c4cbc | I.ActorDotE(e, n) -> I.ActorDotE(exp e, n) | I.DeclareE(i, t, e) -> I.DeclareE(i, t, exp e) | I.DefineE(i, m, e) -> I.DefineE(i, m, exp e) @@ -134,12 +130,7 @@ and dec' at n d = match d with | I.VarD (i, e) -> I.VarD (i, exp e) | I.FuncD (cc, i, tbs, p, ty, e) -> I.FuncD (cc, i, tbs, p, ty, exp e) -<<<<<<< HEAD | I.TypD c -> I.TypD c -======= - | I.TypD (c,k) -> - I.TypD (c,k) ->>>>>>> c28bf054473d6344e0a83dc68c281008ea7c4cbc and cases cs = List.map case cs From 15c03c115c3437504b09c4a24f429194f68ef0c5 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Thu, 14 Feb 2019 16:54:27 -0800 Subject: [PATCH 34/42] avoid new ANF forms in simploop; all passes dump, then check --- src/construct.ml | 10 +++------- src/pipeline.ml | 9 ++++++++- src/simploop.ml | 5 ++++- 3 files changed, 15 insertions(+), 9 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 1619a7ef83e..6366549b324 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -472,24 +472,20 @@ let forE pat exp1 exp2 = | _ -> failwith "invalid return type" in - let id1 = fresh_id ty1 in - let nxt = fresh_id tnxt in - let id1' = fresh_id ty1_ret in + let nxt = fresh_id tnxt in (* Printf.eprintf "XXX ty1 = %s\n" (T.string_of_typ ty1); Printf.eprintf "XXX tnxt = %s\n" (T.string_of_typ tnxt); Printf.eprintf "XXX ty1_ret = %s\n" (T.string_of_typ ty1_ret); *) blockE [ - letD id1 exp1 ; - letD nxt (dotE id1 (nameN "next") tnxt) ; + letD nxt (dotE exp1 (nameN "next") tnxt) ; expD ( labelE lab tyu ( loopE ( blockE [ - letD id1' (callE nxt [] (tupE []) ty1_ret); expD ( - switch_optE id1' + switch_optE (callE nxt [] (tupE []) ty1_ret) (breakE lab (tupE []) tyu) pat exp2 tyu diff --git a/src/pipeline.ml b/src/pipeline.ml index 4be50d48fc8..769e046de42 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -123,6 +123,10 @@ let transform_ir transform_name transform flag env prog name = phase transform_name name; let prog' = transform env prog in dump_ir Flags.dump_lowering prog'; + (* Matthew says: + the check_ir call should go here, not _before_ the dump happens: + when a pass introduces a type error, we want to see the offending AST. *) + Check_ir.check_prog (Check_ir.env_of_scope env) prog ; prog' end else prog @@ -136,6 +140,9 @@ let async_lowering = let tailcall_optimization = transform_ir "Tailcall optimization" Tailcall.transform +let simploop = + transform_ir "Simplify looping forms" Simploop.transform + let check_with parse infer senv name : check_result = match parse name with | Error e -> Error [e] @@ -294,7 +301,7 @@ let compile_with check mode name : compile_result = let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in (* TEMP-Matthew: next line here just to get this module to compile *) - let prog = Simploop.transform initial_stat_env prog in + let prog = simploop true initial_stat_env prog name in phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_ diff --git a/src/simploop.ml b/src/simploop.ml index 514316d704e..b3707f17c37 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -148,5 +148,8 @@ let check_prog scope (prog:I.prog) = let transform scope (p:I.prog) = let p' = prog p in - check_prog scope p'; + (* Matthew says: + the check_ir call should not go here, + but rather, in Pipeline, after the possibility of dumping the AST occurs. *) + (if false then check_prog scope p'); p' From 923b29c533f8e917208c10a2798c4743ae9b02e4 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 09:46:09 +0100 Subject: [PATCH 35/42] Make `check_ir` dump prog when it does not typecheck This is useful because `-v -dl` only dumps the IR output after `Check_ir` ran. This was cherry-picked from #171, and should probably just go to `master`. Maybe only with `-v`. --- src/check_ir.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/check_ir.ml b/src/check_ir.ml index 46b8b077630..59a9e623f95 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -63,10 +63,12 @@ let with_check_typ check_typ env = { env with check_typ } (* More error bookkeeping *) +exception CheckFailed of string + let type_error at text : Diag.message = Diag.{ sev = Diag.Error; at; cat = "IR type"; text } let error env at fmt = - Printf.ksprintf (fun s -> failwith (Diag.string_of_message (type_error at s))) fmt + Printf.ksprintf (fun s -> raise (CheckFailed (Diag.string_of_message (type_error at s)))) fmt let add_lab c x t = {c with labs = T.Env.add x t c.labs} @@ -101,7 +103,7 @@ let check env at p = let check_sub env at t1 t2 = if T.sub t1 t2 then () - else error env at "subtype violation %s %s" (T.string_of_typ t1) (T.string_of_typ t2) + else error env at "subtype violation (%s) (%s)" (T.string_of_typ_expand t1) (T.string_of_typ_expand t2) let make_mut mut : T.typ -> T.typ = match mut.it with @@ -766,5 +768,9 @@ and gather_dec env scope dec : scope = (* Programs *) let check_prog env prog : unit = - check_block env T.unit prog.it prog.at + try + check_block env T.unit prog.it prog.at + with CheckFailed s -> + Wasm.Sexpr.print 80 (Arrange_ir.prog prog); + failwith s From 295edc00bbb8ddb628e35a00f922e8211200639c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 09:47:46 +0100 Subject: [PATCH 36/42] Remove extra call to `Check_ir` from pipeline --- src/pipeline.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/pipeline.ml b/src/pipeline.ml index 769e046de42..60ac072e652 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -123,10 +123,6 @@ let transform_ir transform_name transform flag env prog name = phase transform_name name; let prog' = transform env prog in dump_ir Flags.dump_lowering prog'; - (* Matthew says: - the check_ir call should go here, not _before_ the dump happens: - when a pass introduces a type error, we want to see the offending AST. *) - Check_ir.check_prog (Check_ir.env_of_scope env) prog ; prog' end else prog From df93f3ab33ce05cf16770aa425776ec0b2352e98 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 09:48:08 +0100 Subject: [PATCH 37/42] Let Simploop handle `AsyncE` and `AwaitE` so that we can mix and match passes more easily. --- src/simploop.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simploop.ml b/src/simploop.ml index b3707f17c37..2e6dfd9da99 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -17,8 +17,8 @@ let rec exps es = List.map exp es and exp e = phrase' exp' e and exp' at note = function - | I.AsyncE _ -> assert false - | I.AwaitE _ -> assert false + | I.AsyncE e -> I.AsyncE (exp e) + | I.AwaitE e -> I.AwaitE (exp e) | I.PrimE p -> I.PrimE p | I.VarE i -> I.VarE i | I.LitE l -> I.LitE l From 80e459006babcc7cc55f519e3673b868e27fa321 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 09:52:47 +0100 Subject: [PATCH 38/42] Run simploop also in `-r -iR` mode for easier testing. --- src/pipeline.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pipeline.ml b/src/pipeline.ml index 60ac072e652..01d216c27d8 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -170,7 +170,8 @@ let interpret_prog (senv,denv) name prog : (Value.value * Interpret.scope) optio then let prog_ir = Desugar.transform senv prog in let prog_ir = await_lowering (!Flags.await_lowering) senv prog_ir name in - let prog_ir = async_lowering (!Flags.await_lowering && !Flags.async_lowering) senv prog_ir name in + let prog_ir = async_lowering (!Flags.await_lowering && !Flags.async_lowering) senv prog_ir name in + let prog_ir = simploop true senv prog_ir name in Interpret_ir.interpret_prog denv prog_ir else Interpret.interpret_prog denv prog in match vo with @@ -296,7 +297,6 @@ let compile_with check mode name : compile_result = let prog = await_lowering true initial_stat_env prog name in let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in - (* TEMP-Matthew: next line here just to get this module to compile *) let prog = simploop true initial_stat_env prog name in phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in From f59be98366a99f624ec571bd052f9145baa52528 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 10:01:12 +0100 Subject: [PATCH 39/42] Add call to check_prog back in simploop.ml --- src/simploop.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/simploop.ml b/src/simploop.ml index 2e6dfd9da99..74ae833300b 100644 --- a/src/simploop.ml +++ b/src/simploop.ml @@ -148,8 +148,5 @@ let check_prog scope (prog:I.prog) = let transform scope (p:I.prog) = let p' = prog p in - (* Matthew says: - the check_ir call should not go here, - but rather, in Pipeline, after the possibility of dumping the AST occurs. *) - (if false then check_prog scope p'); + check_prog scope p'; p' From 53d1e7861a19e0a7a672fa6034a33dcecddfcdf3 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 10:12:35 +0100 Subject: [PATCH 40/42] Make Check_ir dump the IR only upon `-v` (and tell the user about it) --- src/check_ir.ml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/check_ir.ml b/src/check_ir.ml index 59a9e623f95..d11b1763580 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -103,7 +103,7 @@ let check env at p = let check_sub env at t1 t2 = if T.sub t1 t2 then () - else error env at "subtype violation (%s) (%s)" (T.string_of_typ_expand t1) (T.string_of_typ_expand 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 @@ -771,6 +771,17 @@ let check_prog env prog : unit = try check_block env T.unit prog.it prog.at with CheckFailed s -> - Wasm.Sexpr.print 80 (Arrange_ir.prog prog); - failwith s + let bt = Printexc.get_backtrace () in + if !Flags.verbose + then begin + Printf.eprintf "Ill-typed intermediate code:\n"; + Printf.eprintf "%s" (Wasm.Sexpr.to_string 80 (Arrange_ir.prog prog)); + Printf.eprintf "%s" s; + Printf.eprintf "%s" bt; + end else begin + Printf.eprintf "Ill-typed intermediate code (use -v to see dumped IR):\n"; + Printf.eprintf "%s" s; + Printf.eprintf "%s" bt; + end; + exit 1 From 041c1ceaae78b50fb5224d51bbddebc6eedca3ff Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 15 Feb 2019 10:22:58 +0100 Subject: [PATCH 41/42] Fix Construct.labelE (it needs to set the return type) --- src/construct.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/construct.ml b/src/construct.ml index 6366549b324..6917c8205c5 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -213,7 +213,11 @@ let assignE exp1 exp2 = } let labelE l typ exp = - { exp with it = LabelE (l, typ, exp) } + { it = LabelE (l, typ, exp) + ; at = no_region + ; note = { S.note_eff = eff exp; + S.note_typ = typ } + } let loopE exp1 exp2Opt = { it = LoopE (exp1, exp2Opt); From 629b88121fc4064fc64c1e9097e1a742b885ca72 Mon Sep 17 00:00:00 2001 From: Matthew Hammer Date: Tue, 26 Feb 2019 07:00:11 -0700 Subject: [PATCH 42/42] simploop: move into desugar, use less ANF; Question about array-gen.as --- src/construct.ml | 23 ++++++----------------- src/desugar.ml | 6 +++--- src/pipeline.ml | 6 ++++-- 3 files changed, 13 insertions(+), 22 deletions(-) diff --git a/src/construct.ml b/src/construct.ml index 6917c8205c5..6a1dc81db4b 100644 --- a/src/construct.ml +++ b/src/construct.ml @@ -405,15 +405,13 @@ let loopWhileE exp1 exp2 = let x2 = e2 ; if x2 { } else { break l } } *) - let id2 = fresh_id exp2.note.S.note_typ in let lab = fresh_lab () in let ty1 = Type.unit in labelE lab ty1 ( loopE ( blockE [ expD exp1 ; - letD id2 exp2 ; - expD (ifE id2 + expD (ifE exp2 (tupE []) (breakE lab (tupE []) ty1) ty1 @@ -422,7 +420,7 @@ let loopWhileE exp1 exp2 = ) None ) -(* LoopE(exp1,Some exp2) *) +(* LoopE(exp1, Some exp2) *) let loopWhileE' exp1 exp2 = (loopWhileE exp1 exp2).it let whileE exp1 exp2 = @@ -431,15 +429,12 @@ let whileE exp1 exp2 = let x1 = e1 ; if x1 then { e2 } else { break l } } *) - let ty1 = exp1.note.S.note_typ in - let id1 = fresh_id ty1 in let lab = fresh_lab () in let ty2 = Type.unit in labelE lab ty2 ( loopE ( blockE [ - letD id1 exp1 ; - expD (ifE id1 + expD (ifE exp1 exp2 (breakE lab (tupE []) ty2) ty2 @@ -465,10 +460,6 @@ let forE pat exp1 exp2 = let lab = fresh_lab () in let tyu = Type.unit in let ty1 = exp1.note.S.note_typ in - - (* XXX: not sure how to get type info for `next` function... - - ...how to do I supply a non-empty con_env for `as_obj_sub` ? - *) let _, tfs = Type.as_obj_sub "next" ty1 in let tnxt = T.lookup_field "next" tfs in let ty1_ret = match (T.as_func tnxt) with @@ -477,12 +468,10 @@ let forE pat exp1 exp2 = in let nxt = fresh_id tnxt in - (* - Printf.eprintf "XXX ty1 = %s\n" (T.string_of_typ ty1); - Printf.eprintf "XXX tnxt = %s\n" (T.string_of_typ tnxt); - Printf.eprintf "XXX ty1_ret = %s\n" (T.string_of_typ ty1_ret); - *) blockE [ + (* Matthew says: When I avoid ANF and "inline" this Let binding for 'nxt', + the IR interpreter hangs on `array-gen.as`. + it's unclear to me why that apparent divergence happens. *) letD nxt (dotE exp1 (nameN "next") tnxt) ; expD ( labelE lab tyu ( diff --git a/src/desugar.ml b/src/desugar.ml index 9d4d24a65d4..e122667abe0 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -73,10 +73,10 @@ and exp' at note = function | S.OrE (e1, e2) -> I.IfE (exp e1, trueE, exp e2) | S.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3) | S.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs) - | S.WhileE (e1, e2) -> I.WhileE (exp e1, exp e2) + | S.WhileE (e1, e2) -> whileE' (exp e1) (exp e2) (* I.WhileE (exp e1, exp e2) *) | S.LoopE (e1, None) -> I.LoopE (exp e1, None) - | S.LoopE (e1, Some e2) -> I.LoopE (exp e1, Some (exp e2)) - | S.ForE (p, e1, e2) -> I.ForE (pat p, exp e1, exp e2) + | S.LoopE (e1, Some e2) -> loopWhileE' (exp e1) (exp e2) (* I.LoopE (exp e1, Some (exp e2)) *) + | S.ForE (p, e1, e2) -> forE' (pat p) (exp e1) (exp e2) (* I.ForE (pat p, exp e1, exp e2) *) | S.LabelE (l, t, e) -> I.LabelE (l, t.Source.note, exp e) | S.BreakE (l, e) -> I.BreakE (l, exp e) | S.RetE e -> I.RetE (exp e) diff --git a/src/pipeline.ml b/src/pipeline.ml index 01d216c27d8..0a938682f74 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -136,8 +136,10 @@ let async_lowering = let tailcall_optimization = transform_ir "Tailcall optimization" Tailcall.transform +(* let simploop = transform_ir "Simplify looping forms" Simploop.transform +*) let check_with parse infer senv name : check_result = match parse name with @@ -171,7 +173,7 @@ let interpret_prog (senv,denv) name prog : (Value.value * Interpret.scope) optio let prog_ir = Desugar.transform senv prog in let prog_ir = await_lowering (!Flags.await_lowering) senv prog_ir name in let prog_ir = async_lowering (!Flags.await_lowering && !Flags.async_lowering) senv prog_ir name in - let prog_ir = simploop true senv prog_ir name in + (* let prog_ir = simploop true senv prog_ir name in *) Interpret_ir.interpret_prog denv prog_ir else Interpret.interpret_prog denv prog in match vo with @@ -297,7 +299,7 @@ let compile_with check mode name : compile_result = let prog = await_lowering true initial_stat_env prog name in let prog = async_lowering true initial_stat_env prog name in let prog = tailcall_optimization true initial_stat_env prog name in - let prog = simploop true initial_stat_env prog name in + (* let prog = simploop true initial_stat_env prog name in *) phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_