diff --git a/src/arrange.ml b/src/arrange.ml index bdcf92c657e..02d48394995 100644 --- a/src/arrange.ml +++ b/src/arrange.ml @@ -13,12 +13,12 @@ let rec exp e = match e.it with | TupE es -> "TupE" $$ List.map exp es | ProjE (e, i) -> "ProjE" $$ [exp e; Atom (string_of_int i)] | ObjE (s, i, efs) -> "ObjE" $$ [obj_sort s; id i] @ List.map exp_field efs - | DotE (e, n) -> "DotE" $$ [exp e; name n] + | DotE (e, sr, n) -> "DotE" $$ [exp e; obj_sort' !sr; name n] | AssignE (e1, e2) -> "AssignE" $$ [exp e1; exp e2] | ArrayE (m, es) -> "ArrayE" $$ [mut m] @ List.map exp es | IdxE (e1, e2) -> "IdxE" $$ [exp e1; exp e2] - | CallE (e1, ts, e2) -> "CallE" $$ [exp e1] @ List.map inst ts @ [exp e2] - | BlockE ds -> "BlockE" $$ List.map dec ds + | CallE (e1, ts, e2) -> "CallE" $$ [exp e1] @ List.map typ ts @ [exp e2] + | BlockE (ds, ot) -> "BlockE" $$ List.map dec ds @ [operator_type (!ot)] | NotE e -> "NotE" $$ [exp e] | AndE (e1, e2) -> "AndE" $$ [exp e1; exp e2] | OrE (e1, e2) -> "OrE" $$ [exp e1; exp e2] @@ -36,7 +36,7 @@ let rec exp e = match e.it with | AssertE e -> "AssertE" $$ [exp e] | IsE (e1, e2) -> "IsE" $$ [exp e1; exp e2] | AnnotE (e, t) -> "AnnotE" $$ [exp e; typ t] - | DecE d -> "DecE" $$ [dec d] + | DecE (d, ot) -> "DecE" $$ [dec d ; operator_type !ot] | OptE e -> "OptE" $$ [exp e] | PrimE p -> "PrimE" $$ [Atom p] | DeclareE (i, t, e1) -> "DeclareE" $$ [id i; exp e1] @@ -109,11 +109,13 @@ and sharing sh = match sh with and control c = match c with | Type.Returns -> "Returns" | Type.Promises -> "Promises" - -and obj_sort s = match s.it with + +and obj_sort' s = match s with | Type.Object sh -> Atom ("Object " ^ sharing sh) | Type.Actor -> Atom "Actor" +and obj_sort s = obj_sort' s.it + and func_sort s = match s.it with | Type.Call sh -> Atom ("Call " ^ sharing sh) | Type.Construct -> Atom "Construct" @@ -135,8 +137,6 @@ and typ_bind (tb : typ_bind) and exp_field (ef : exp_field) = (string_of_name ef.it.name.it) $$ [id ef.it.id; exp ef.it.exp; mut ef.it.mut; priv ef.it.priv] -and inst t = typ t.it - and operator_type t = Atom (Type.string_of_typ t) and typ t = match t.it with @@ -152,6 +152,7 @@ and typ t = match t.it with | ParT t -> "ParT" $$ [typ t] and id i = Atom i.it +and con_id i = Atom i.it and name n = Atom (string_of_name n.it) @@ -170,8 +171,8 @@ and dec d = match d.it with exp e ] | TypD (i, tp, t) -> - "TypD" $$ [id i] @ List.map typ_bind tp @ [typ t] + "TypD" $$ [con_id i] @ List.map typ_bind tp @ [typ t] | ClassD (i, j, tp, s, p, i', efs) -> - "ClassD" $$ id i :: id j :: List.map typ_bind tp @ [obj_sort s; pat p; id i'] @ List.map exp_field efs + "ClassD" $$ id i :: con_id j :: List.map typ_bind tp @ [obj_sort s; pat p; id i'] @ List.map exp_field efs -and prog prog = "BlockE" $$ List.map dec prog.it +and prog prog = "BlockE" $$ List.map dec prog.it diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index c461f77c8fd..56fc9253719 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -1,8 +1,12 @@ open Source +open Arrange_type (* currently not used *) open Ir open Wasm.Sexpr -let ($$) head inner = Node (head, inner) +(* for concision, we shadow the imported definition of [Arrange_type.typ] and pretty print types instead *) + +let typ t = Atom (Type.string_of_typ t) +let kind k = Atom (Type.string_of_kind k) let rec exp e = match e.it with | VarE i -> "VarE" $$ [id i] @@ -12,21 +16,21 @@ let rec exp e = match e.it with | RelE (t, e1, ro, e2)-> "RelE" $$ [typ t; exp e1; Arrange.relop ro; exp e2] | TupE es -> "TupE" $$ List.map exp es | ProjE (e, i) -> "ProjE" $$ [exp e; Atom (string_of_int i)] - | ActorE (i, efs) -> "ActorE" $$ [id i] @ List.map exp_field efs + | ActorE (i, efs, t) -> "ActorE" $$ [id i] @ List.map exp_field efs @ [typ t] | DotE (e, n) -> "DotE" $$ [exp e; name n] | ActorDotE (e, n) -> "ActorDotE" $$ [exp e; name n] | AssignE (e1, e2) -> "AssignE" $$ [exp e1; exp e2] - | ArrayE (m, es) -> "ArrayE" $$ [Arrange.mut m] @ List.map exp es + | ArrayE (m, t, es) -> "ArrayE" $$ [Arrange.mut m; typ t] @ List.map exp es | IdxE (e1, e2) -> "IdxE" $$ [exp e1; exp e2] - | CallE (cc, e1, ts, e2) -> "CallE" $$ [call_conv cc; exp e1] @ List.map Arrange.typ ts @ [exp e2] - | BlockE ds -> "BlockE" $$ List.map dec ds + | CallE (cc, e1, ts, e2) -> "CallE" $$ [call_conv cc; exp e1] @ List.map typ ts @ [exp e2] + | BlockE (ds, t) -> "BlockE" $$ List.map dec ds @ [typ t] | IfE (e1, e2, e3) -> "IfE" $$ [exp e1; exp e2; exp e3] | SwitchE (e, cs) -> "SwitchE" $$ [exp e] @ List.map case cs | WhileE (e1, e2) -> "WhileE" $$ [exp e1; exp e2] | LoopE (e1, None) -> "LoopE" $$ [exp e1] | LoopE (e1, Some e2) -> "LoopE" $$ [exp e1; exp e2] | ForE (p, e1, e2) -> "ForE" $$ [pat p; exp e1; exp e2] - | LabelE (i, t, e) -> "LabelE" $$ [id i; Arrange.typ t; exp e] + | LabelE (i, t, e) -> "LabelE" $$ [id i; typ t; exp e] | BreakE (i, e) -> "BreakE" $$ [id i; exp e] | RetE e -> "RetE" $$ [exp e] | AsyncE e -> "AsyncE" $$ [exp e] @@ -37,9 +41,9 @@ let rec exp e = match e.it with | PrimE p -> "PrimE" $$ [Atom p] | DeclareE (i, t, e1) -> "DeclareE" $$ [id i; exp e1] | DefineE (i, m, e1) -> "DefineE" $$ [id i; Arrange.mut m; exp e1] - | NewObjE (s, nameids)-> "NewObjE" $$ (Arrange.obj_sort s :: + | NewObjE (s, nameids, t)-> "NewObjE" $$ (Arrange.obj_sort s :: List.fold_left (fun flds (n,i) -> - (name n)::(id i):: flds) [] nameids) + (name n)::(id i):: flds) [typ t] nameids) and pat p = match p.it with | WildP -> Atom "WildP" @@ -51,13 +55,9 @@ and pat p = match p.it with and case c = "case" $$ [pat c.it.pat; exp c.it.exp] -and typ t = Atom (Type.string_of_typ t) - and exp_field (ef : exp_field) = (Syntax.string_of_name ef.it.name.it) $$ [id ef.it.id; exp ef.it.exp; Arrange.mut ef.it.mut; Arrange.priv ef.it.priv] -and id i = Atom i.it - and name n = Atom (Syntax.string_of_name n.it) and call_conv cc = Atom (Value.string_of_call_conv cc) @@ -67,8 +67,11 @@ and dec d = match d.it with | LetD (p, e) -> "LetD" $$ [pat p; exp e] | VarD (i, e) -> "VarD" $$ [id i; exp e] | FuncD (cc, i, tp, p, t, e) -> - "FuncD" $$ [call_conv cc; id i] @ List.map Arrange.typ_bind tp @ [pat p; Arrange.typ t; exp e] - | TypD (i, tp, t) -> - "TypD" $$ [id i] @ List.map Arrange.typ_bind tp @ [Arrange.typ t] + "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] + +and typ_bind (tb : typ_bind) = + tb.it.Type.var $$ [typ tb.it.Type.bound] and prog prog = "BlockE" $$ List.map dec prog.it diff --git a/src/arrange_type.ml b/src/arrange_type.ml new file mode 100644 index 00000000000..312eec3be4c --- /dev/null +++ b/src/arrange_type.ml @@ -0,0 +1,63 @@ +open Source +open Type +open Wasm.Sexpr + +let ($$) head inner = Node (head, inner) + +let id i = Atom i.it + +let rec sharing sh = match sh with + | Type.Local -> "Local" + | Type.Sharable -> "Sharable" + +and control c = match c with + | Type.Returns -> "Returns" + | Type.Promises -> "Promises" + +and obj_sort s = match s with + | Type.Object sh -> Atom ("Object " ^ sharing sh) + | Type.Actor -> Atom "Actor" + +and func_sort s = match s with + | Type.Call sh -> Atom ("Call " ^ sharing sh) + | Type.Construct -> Atom "Construct" + +and prim p = match p with + | Null -> Atom "Null" + | Bool -> Atom "Bool" + | Nat -> Atom "Nat" + | Int -> Atom "Int" + | Word8 -> Atom "Word8" + | Word16 -> Atom "Word16" + | Word32 -> Atom "Word32" + | Word64 -> Atom "Word64" + | Float -> Atom "Float" + | Char -> Atom "Char" + | Text -> Atom "Text" + +and 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)] + | Con (c,ts) -> "Con" $$ (con c::List.map typ ts) + | Prim p -> "Prim" $$ [prim p] + | Obj (s, ts) -> "Obj" $$ [obj_sort s] @ List.map typ_field ts + | Array t -> "Array" $$ [typ t] + | Opt t -> "Opt" $$ [typ t] + | Tup ts -> "Tup" $$ List.map typ ts + | Func (s, c, tbs, at, rt) -> "Func" $$ [func_sort s; Atom (control c)] @ List.map typ_bind tbs @ [ "" $$ (List.map typ at); "" $$ (List.map typ rt)] + | Async t -> "Async" $$ [typ t] + | Like t -> "Like" $$ [typ t] + | Mut t -> "Mut" $$ [typ t] + | Class -> Atom "Class" + | Shared -> Atom "Shared" + | Any -> Atom "Any" + | Non -> Atom "Non" + | Pre -> Atom "Pre" + +and typ_bind (tb : Type.bind) = + tb.var $$ [typ tb.bound] + +and typ_field (tf : Type.field) = + tf.name $$ [typ tf.typ] + diff --git a/src/async.ml b/src/async.ml index 44598d27c35..5ef8fdae3f7 100644 --- a/src/async.ml +++ b/src/async.ml @@ -33,14 +33,14 @@ let fullfillT as_seq typ = T.Func(T.Call T.Local, T.Returns, [], as_seq typ, []) let tupT ts = {it = TupT ts; at = no_region; - note = ()} + note = T.Tup (List.map (fun t -> t.note) ts)} let unitT = tupT [] let funcT(s,bds,t1,t2) = {it = FuncT (s, bds, t1, t2); at = no_region; - note = ()} + note = T.Pre} (* TBR: try harder *) let t_async as_seq t = T.Func (T.Call T.Local, T.Returns, [], [T.Func(T.Call T.Local, T.Returns, [],as_seq t,[])], []) @@ -56,17 +56,25 @@ let new_asyncT = let new_asyncE = idE ("@new_async"@@no_region) new_asyncT -let bogusT = PrimT "BogusT"@@no_region (* bogus, but we shouln't use it anymore *) +let bogusT t= + { it = PrimT "BogusT" (* bogus, but we shouln't use it anymore *); + at = no_region; + note = t; + } let new_async t1 = - let call_new_async = callE new_asyncE [{it = bogusT; at = no_region; note = ref t1} ] (tupE[]) (T.seq (new_async_ret unary t1)) in + let call_new_async = + callE new_asyncE + [bogusT t1] + (tupE[]) + (T.seq (new_async_ret unary t1)) in let async = fresh_id (typ (projE call_new_async 0)) in let fullfill = fresh_id (typ (projE call_new_async 1)) in (async,fullfill),call_new_async let letP p e = {it = LetD(p,e); at = no_region; - note = e.note} + note = {e.note with note_typ = T.unit}} let new_nary_async_reply t1 = let (unary_async,unary_fullfill),call_new_async = new_async t1 in @@ -102,20 +110,6 @@ let new_nary_async_reply t1 = let replyTT t = funcT(sharableS,[],t,unitT) -let shared_funcD f x e = - match f.it,x.it with - | VarE _, VarE _ -> - let note = {note_typ = T.Func(T.Call T.Sharable, T.Returns, [], as_seq (typ x), as_seq (typ e)); - note_eff = T.Triv} in - {it=FuncD(T.Sharable @@ no_region, (id_of_exp f), - [], - {it=VarP (id_of_exp x);at=no_region;note=x.note}, - PrimT "Any"@@no_region, (* bogus, but we shouldn't use it anymore *) - e); - at = no_region; - note;} - | _ -> assert false - let letEta e scope = match e.it with | VarE _ -> scope e (* pure, so reduce *) @@ -200,12 +194,24 @@ let rec t_typ (t:T.typ) = and t_bind {var; bound} = {var; bound = t_typ bound} +and t_kind k = match k with + | T.Abs(tbs,t) -> + T.Abs(List.map t_bind tbs, t_typ t) + | T.Def(tbs,t) -> + T.Def(List.map t_bind tbs, t_typ t) + 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, it will be a pure value anyways. *) ref (t_typ !ot) +and t_con_id con_id = + { it = con_id.it; + at = con_id.at; + note = Lib.Option.map (fun (c,k) -> (c,t_kind k)) con_id.note + } + and t_field {name; typ} = {name; typ = t_typ typ} let rec t_exp (exp:Syntax.exp) = @@ -235,14 +241,14 @@ and t_exp' (exp:Syntax.exp) = | ObjE (sort, id, fields) -> let fields' = t_fields fields in ObjE (sort, id, fields') - | DotE (exp1, id) -> - DotE (t_exp exp1, id) + | DotE (exp1, sr, id) -> + DotE (t_exp exp1, ref !sr, id) | AssignE (exp1, exp2) -> AssignE (t_exp exp1, t_exp exp2) | ArrayE (mut, exps) -> ArrayE (mut, List.map t_exp exps) | IdxE (exp1, exp2) -> - IdxE (t_exp exp1, t_exp exp2) + IdxE (t_exp exp1, t_exp exp2) | CallE ({it=PrimE "@await";_}, typs, exp2) -> begin match exp2.it with @@ -250,46 +256,46 @@ and t_exp' (exp:Syntax.exp) = | _ -> assert false end | CallE ({it=PrimE "@async";_}, typs, exp2) -> - let t1, contT = match typ exp2 with - | Func(_,_, - [], - [Func(_,_,[],ts1,[]) as contT], - []) -> (* TBR, why isn't this []? *) - (t_typ (T.seq ts1),t_typ contT) - | t -> assert false in - let k = fresh_id contT in - let v1 = fresh_id t1 in - let post = fresh_id (T.Func(T.Call T.Sharable,T.Returns,[],[],[])) in - let u = fresh_id T.unit in - let ((nary_async,nary_reply),def) = new_nary_async_reply t1 in - (blockE [letP (tupP [varP nary_async; varP nary_reply]) def; - funcD k v1 (nary_reply -*- v1); - shared_funcD post u (t_exp exp2 -*- k); - expD (post -*- tupE[]); - expD nary_async]) - .it + let t1, contT = match typ exp2 with + | Func(_,_, + [], + [Func(_,_,[],ts1,[]) as contT], + []) -> (* TBR, why isn't this []? *) + (t_typ (T.seq ts1),t_typ contT) + | t -> assert false in + let k = fresh_id contT in + let v1 = fresh_id t1 in + let post = fresh_id (T.Func(T.Call T.Sharable,T.Returns,[],[],[])) in + let u = fresh_id T.unit in + let ((nary_async,nary_reply),def) = new_nary_async_reply t1 in + (blockE [letP (tupP [varP nary_async; varP nary_reply]) def; + funcD k v1 (nary_reply -*- v1); + funcD post u (t_exp exp2 -*- k); + expD (post -*- tupE[]); + expD nary_async]) + .it | CallE (exp1, typs, exp2) when isAwaitableFunc exp1 -> - let ts1,t2 = - match typ exp1 with - | T.Func (T.Call T.Sharable,T.Promises,tbs,ts1,[T.Async t2]) -> - ts1, t_typ t2 - | _ -> assert(false) - in - let exp1' = t_exp exp1 in - let exp2' = t_exp exp2 in - let typs = List.map t_inst typs in - let ((nary_async,nary_reply),def) = new_nary_async_reply t2 in - let _ = letEta in - (blockE (letP (tupP [varP nary_async; varP nary_reply]) def:: - letEta exp1' (fun v1 -> - letSeq ts1 exp2' (fun vs -> - [expD (callE v1 typs (seqE (vs@[nary_reply])) T.unit); - expD nary_async])))) - .it + let ts1,t2 = + match typ exp1 with + | T.Func (T.Call T.Sharable,T.Promises,tbs,ts1,[T.Async t2]) -> + List.map t_typ ts1, t_typ t2 + | _ -> assert(false) + in + let exp1' = t_exp exp1 in + let exp2' = t_exp exp2 in + let typs = List.map t_typT typs in + let ((nary_async,nary_reply),def) = new_nary_async_reply t2 in + let _ = letEta in + (blockE (letP (tupP [varP nary_async; varP nary_reply]) def:: + letEta exp1' (fun v1 -> + letSeq ts1 exp2' (fun vs -> + [expD (callE v1 typs (seqE (vs@[nary_reply])) T.unit); + expD nary_async])))) + .it | CallE (exp1, typs, exp2) -> - CallE(t_exp exp1, List.map t_inst typs, t_exp exp2) - | BlockE decs -> - BlockE (t_decs decs) + CallE(t_exp exp1, List.map t_typT typs, t_exp exp2) + | BlockE (decs, ot) -> + BlockE (t_decs decs, ref (t_typ (!ot))) | NotE exp1 -> NotE (t_exp exp1) | AndE (exp1, exp2) -> @@ -325,8 +331,8 @@ and t_exp' (exp:Syntax.exp) = IsE (t_exp exp1, t_exp exp2) | AnnotE (exp1, typ) -> AnnotE (t_exp exp1, t_typT typ) - | DecE dec -> - DecE (t_dec dec) + | DecE (dec, ot) -> + DecE (t_dec dec, ref (t_typ (!ot))) | DeclareE (id, typ, exp1) -> DeclareE (id, t_typ typ, t_exp exp1) | DefineE (id, mut ,exp1) -> @@ -343,7 +349,8 @@ and t_dec dec = and t_dec' dec' = match dec' with | ExpD exp -> ExpD (t_exp exp) - | TypD _ -> dec' + | TypD (con_id, typbinds, typ) -> + TypD (t_con_id con_id, t_typbinds typbinds, t_typT typ) | LetD (pat,exp) -> LetD (t_pat pat,t_exp exp) | VarD (id,exp) -> VarD (id,t_exp exp) | FuncD (s, id, typbinds, pat, typT, exp) -> @@ -381,9 +388,9 @@ and t_dec' dec' = | _ -> assert false end end - | ClassD (id, lab, typbinds, sort, pat, id', fields) -> + | ClassD (id, con_id, typbinds, sort, pat, id', fields) -> let fields' = t_fields fields in - ClassD (id, lab, t_typbinds typbinds, sort, t_pat pat, id', fields') + ClassD (id, t_con_id con_id, t_typbinds typbinds, sort, t_pat pat, id', fields') and t_decs decs = List.map t_dec decs @@ -394,8 +401,7 @@ and t_fields fields = and t_pat pat = { pat with it = t_pat' pat.it; - note = {note_typ = t_typ pat.note.note_typ; - note_eff = pat.note.note_eff}} + note = t_typ pat.note} and t_pat' pat = match pat with @@ -421,14 +427,11 @@ and t_asyncT t = funcT(localS,[],t,unitT), unitT) - -and t_inst t : inst = - { it = t_typT t.it; - at = t.at; - note = ref (t_typ (!(t.note)))} - and t_typT t = - { t with it = t_typT' t.it } + { it = t_typT' t.it; + at = t.at; + note = t_typ t.note; + } and t_typT' t = match t with diff --git a/src/awaitopt.ml b/src/awaitopt.ml index 6f9887bcf41..f6b5e96c6aa 100644 --- a/src/awaitopt.ml +++ b/src/awaitopt.ml @@ -82,8 +82,8 @@ and t_exp' context exp' = | ObjE (sort, id, fields) -> let fields' = t_fields context fields in ObjE (sort, id, fields') - | DotE (exp1, id) -> - DotE (t_exp context exp1, id) + | DotE (exp1, sr, id) -> + DotE (t_exp context exp1, ref (!sr), id) | AssignE (exp1, exp2) -> AssignE (t_exp context exp1, t_exp context exp2) | ArrayE (mut, exps) -> @@ -92,8 +92,8 @@ and t_exp' context exp' = IdxE (t_exp context exp1, t_exp context exp2) | CallE (exp1, typs, exp2) -> CallE (t_exp context exp1, typs, t_exp context exp2) - | BlockE decs -> - BlockE (t_decs context decs) + | BlockE (decs, ot) -> + BlockE (t_decs context decs, ref (!ot)) | NotE exp1 -> NotE (t_exp context exp1) | AndE (exp1, exp2) -> @@ -146,8 +146,8 @@ and t_exp' context exp' = IsE (t_exp context exp1, t_exp context exp2) | AnnotE (exp1, typ) -> AnnotE (t_exp context exp1,typ) - | DecE dec -> - DecE (t_dec context dec) + | DecE (dec,ot) -> + DecE (t_dec context dec, ref (!ot)) | DeclareE (id, typ, exp1) -> DeclareE (id, typ, t_exp context exp1) | DefineE (id, mut ,exp1) -> @@ -339,7 +339,7 @@ and c_loop_some context k e1 e2 = and c_for context k pat e1 e2 = let v1 = fresh_id (typ e1) in - let next_typ = (T.Func(T.Call T.Local, T.Returns, [], [], [T.Opt (typ pat)])) in + let next_typ = (T.Func(T.Call T.Local, T.Returns, [], [], [T.Opt pat.note])) in let dotnext v = dotE v nextN next_typ -*- unitE in let loop = fresh_id (contT T.unit) in let v2 = fresh_id T.unit in @@ -407,8 +407,8 @@ and c_exp' context exp k = unary context k (fun v1 -> e (ProjE (v1, n))) exp1 | ObjE (sort, id, fields) -> c_obj context exp sort id fields k - | DotE (exp1, id) -> - unary context k (fun v1 -> e (DotE (v1, id))) exp1 + | DotE (exp1, sr, id) -> + unary context k (fun v1 -> e (DotE (v1, ref (!sr), id))) exp1 | AssignE (exp1, exp2) -> binary context k (fun v1 v2 -> e (AssignE (v1, v2))) exp1 exp2 | ArrayE (mut, exps) -> @@ -417,7 +417,7 @@ and c_exp' context exp k = binary context k (fun v1 v2 -> e (IdxE (v1, v2))) exp1 exp2 | CallE (exp1, typs, exp2) -> binary context k (fun v1 v2 -> e (CallE (v1, typs, v2))) exp1 exp2 - | BlockE decs -> + | BlockE (decs,t) -> c_block context decs k | NotE exp1 -> unary context k (fun v1 -> e (NotE v1)) exp1 @@ -498,7 +498,7 @@ and c_exp' context exp k = | AnnotE (exp1, typ) -> (* TBR just erase the annotation instead? *) unary context k (fun v1 -> e (AnnotE (v1,typ))) exp1 - | DecE dec -> + | DecE (dec, _) -> c_dec context dec k | DeclareE (id, typ, exp1) -> unary context k (fun v1 -> e (DeclareE (id, typ, v1))) exp1 @@ -588,7 +588,7 @@ and declare_id id typ exp = and declare_pat pat exp : exp = match pat.it with | WildP | LitP _ | SignP _ -> exp - | VarP id -> declare_id id (pat.note.note_typ) exp + | VarP id -> declare_id id pat.note exp | TupP pats -> declare_pats pats exp | OptP pat1 -> declare_pat pat1 exp | AltP (pat1, pat2) -> declare_pat pat1 exp @@ -609,7 +609,7 @@ and rename_pat' pat = | WildP -> (PatEnv.empty, pat.it) | LitP _ | SignP _ -> (PatEnv.empty, pat.it) | VarP id -> - let v = fresh_id pat.note.note_typ in + let v = fresh_id pat.note in (PatEnv.singleton id.it v, VarP (id_of_exp v)) | TupP pats -> diff --git a/src/check_ir.ml b/src/check_ir.ml new file mode 100644 index 00000000000..771354aa50f --- /dev/null +++ b/src/check_ir.ml @@ -0,0 +1,810 @@ +open Source +module T = Type +module E = Effect + +(* TODO: remove DecE from syntax, replace by BlockE [dec] *) +(* TODO: check constraint matching supports recursive bounds *) + +(* TODO: make note immutable, perhaps just using type abstraction *) + +(* TODO: + add type and term predicate to rule out constructs after passes, We could even compose these I guess.... + dereferencing is still implicit in the IR (see immut_typ below) - consider making it explicit as part of desugaring. + *) + +(* helpers *) +let (==>) p q = not p || q +let typ = E.typ + +let immute_typ p = + assert (not (T.is_mut (typ p))); + (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; + 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) *) + +type lab_env = T.typ T.Env.t +type ret_env = T.typ option + +type env = + { vals : val_env; + cons : con_env; + labs : lab_env; + rets : ret_env; + async : bool; + } + +let env_of_scope scope = + { vals = scope.Typing.val_env; + cons = scope.Typing.con_env; + labs = T.Env.empty; + rets = None; + async = false; + } + +(* More error bookkeeping *) + +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 + + +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 = + { c with + cons = List.fold_right2 Con.Env.add cs ks 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 + with T.Env.Clash k -> error env at fmt k + +(* Types *) + +let check_ids env ids = ignore + (List.fold_left + (fun dom id -> + if List.mem id dom + then error env no_region "duplicate field name %s in object type" id + else id::dom + ) [] ids + ) + +let check env at p = + if p then ignore + else error env at + +let check_sub env at t1 t2 = + if (T.sub env.cons t1 t2) + then () + else error env at "subtype violation %s %s" (T.string_of_typ t1) (T.string_of_typ t2) + +let make_mut mut : T.typ -> T.typ = + match mut.it with + | Syntax.Const -> fun t -> t + | Syntax.Var -> fun t -> T.Mut t + +let rec check_typ env typ : unit = + match typ with + | T.Pre -> + error env no_region "illegal T.Pre type" + | 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)) -> + 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 -> () + | T.Shared -> () + | T.Class -> () + | T.Prim _ -> () + | T.Array typ -> + check_typ env typ + | 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 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; + if control = T.Promises then begin + match ts2 with + | [T.Async _ ] -> () + | _ -> + 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) + end; + if sort = T.Call T.Sharable then begin + let t1 = T.seq ts1 in + check_sub env' no_region t1 T.Shared; + match ts2 with + | [] -> () + | [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)) + end + | T.Opt typ -> + check_typ env typ + | T.Async typ -> + let t' = T.promote env.cons typ in + check_sub env no_region t' T.Shared + | T.Like typ -> + check_typ env typ + | T.Obj (sort, fields) -> + let rec sorted fields = + match fields with + | [] + | [_] -> true + | f1::((f2::_) as fields') -> + T.compare_field f1 f2 < 0 && sorted fields' + in + check_ids env (List.map (fun (field : T.field) -> field.T.name) fields); + List.iter (check_typ_field env sort) fields; + check env no_region (sorted fields) "object type's fields are not sorted" + | T.Mut typ -> + check_typ env typ + +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)) + "actor field has non-function type"; + check env no_region + (s = T.Object T.Local || T.sub env.cons 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 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 _ = 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 + +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) + "type argument does not match parameter bound"; + check_typ_bounds env tbs' typs' at + | [], [] -> () + | [], _ -> error env at "too many type arguments" + | _, [] -> error env at "too few type arguments" + +and check_inst_bounds env tbs typs at = + check_typ_bounds env tbs typs at + +(* Literals *) + +let type_lit env lit at : T.prim = + let open Syntax in + match lit with + | NullLit -> T.Null + | BoolLit _ -> T.Bool + | NatLit _ -> T.Nat + | IntLit _ -> T.Int + | Word8Lit _ -> T.Word8 + | Word16Lit _ -> T.Word16 + | Word32Lit _ -> T.Word32 + | Word64Lit _ -> T.Word64 + | FloatLit _ -> T.Float + | CharLit _ -> T.Char + | TextLit _ -> T.Text + | PreLit (s,p) -> + error env at "unresolved literal %s of type\n %s" s (T.string_of_prim p) + +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 = + match exp.it with + | AsyncE _ -> true + | _ -> false + +let rec check_exp env (exp:Ir.exp) : unit = + (* helpers *) + let check p = check env exp.at p in + let (<:) t1 t2 = check_sub env exp.at t1 t2 in + let (<~) t1 t2 = + (if T.is_mut t2 then t1 else T.as_immut t1) <: t2 + in + (* check effect *) + check (E.Ir.infer_effect_exp exp <= E.eff exp) + "inferred effect not a subtype of expected effect"; + (* check typing *) + let t = E.typ exp in + match exp.it with + | PrimE _ -> () + | VarE id -> + let t0 = try T.Env.find id.it env.vals with + | Not_found -> error env id.at "unbound variable %s" id.it + in + t0 <~ t + | LitE lit -> + T.Prim (type_lit env lit exp.at) <: t + | UnE (ot, op, exp1) -> + check (Operator.has_unop ot op) "unary operator is not defined for operand type"; + check_exp env exp1; + typ exp1 <: ot; + ot <: t; + | BinE (ot, exp1, op, exp2) -> + check (Operator.has_binop ot op) "binary operator is not defined for operand type"; + check_exp env exp1; + check_exp env exp2; + typ exp1 <: ot; + typ exp2 <: ot; + ot <: t; + | RelE (ot,exp1, op, exp2) -> + check (Operator.has_relop ot op) "relational operator is not defined for operand type"; + check_exp env exp1; + check_exp env exp2; + typ exp1 <: ot; + typ exp2 <: ot; + T.bool <: t; + | TupE exps -> + List.iter (check_exp env) exps; + T.Tup (List.map typ exps) <: t; + | OptE exp1 -> + check_exp env exp1; + T.Opt (typ exp1) <: t; + | 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 + 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 + 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 + 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 + check (T.is_obj t2) "bad annotation (object type expected)"; + t1 <: t2; + t0 <: t; + | ActorDotE(exp1,{it = Syntax.Name n;_}) + | DotE (exp1, {it = Syntax.Name n;_}) -> + begin + check_exp env exp1; + let t1 = typ exp1 in + let sort, tfs = + try T.as_obj_sub n env.cons 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) + in + check (match exp.it with + | ActorDotE _ -> sort = T.Actor + | DotE _ -> sort <> T.Actor + | _ -> false) "sort mismatch"; + match List.find_opt (fun {T.name; _} -> name = n) tfs with + | Some {T.typ = tn;_} -> + 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) + end + | AssignE (exp1, exp2) -> + check_exp env exp1; + check_exp env exp2; + let t2 = try T.as_mut (typ exp1) with + Invalid_argument _ -> error env exp.at "expected mutable assignment target" + in + typ exp2 <: t2; + T.unit <: t; + | ArrayE (mut, t0, exps) -> + List.iter (check_exp env) exps; + List.iter (fun e -> typ e <: t0) exps; + let t1 = T.Array (match mut.it with Syntax.Const -> t0 | Syntax.Var -> T.Mut t0) in + t1 <: t; + | 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 + | Invalid_argument _ -> + error env exp1.at "expected array type, but expression produces type\n %s" + (T.string_of_typ_expand env.cons t1) + in + typ exp2 <: T.nat; + t2 <~ t + | CallE (call_conv, exp1, insts, exp2) -> + 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 tbs, t2, t3 = + try T.as_func_sub (List.length insts) env.cons 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) + in + check_inst_bounds env tbs insts exp.at; + check_exp env exp2; + (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 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"; + t0 <: t; + | IfE (exp1, exp2, exp3) -> + check_exp env exp1; + typ exp1 <: T.bool; + check_exp env exp2; + typ exp2 <: t; + check_exp env exp3; + typ exp3 <: t; + | SwitchE (exp1, cases) -> + check_exp env exp1; + let t1 = T.promote env.cons (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"; + *) + check_cases env t1 t cases; + | WhileE (exp1, exp2) -> + check_exp env exp1; + typ exp1 <: T.bool; + check_exp env exp2; + typ exp2 <: T.unit; + T.unit <: t; + | LoopE (exp1, expo) -> + check_exp env exp1; + typ exp1 <: T.unit; + begin match expo with + | Some exp2 -> + check_exp env exp2; + (typ exp2) <: T.bool; + | _ -> () + end; + T.Non <: t; (* vacuously true *) + | ForE (pat, exp1, exp2) -> + begin + check_exp env exp1; + let t1 = T.promote env.cons (typ exp1) in + try + let _, tfs = T.as_obj_sub "next" env.cons t1 in + let t0 = T.lookup_field "next" tfs in + let t1, t2 = T.as_mono_func_sub env.cons t0 in + T.unit <: t1; + let t2' = T.as_opt_sub env.cons t2 in + let ve = check_pat_exhaustive env pat in + pat.note <: t2'; + check_exp (adjoin_vals env ve) exp2; + typ exp2 <: T.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) + end; + | LabelE (id, t0, exp1) -> + assert (t0 <> T.Pre); + check_typ env t0; + check_exp (add_lab env id.it t0) exp1; + typ exp1 <: t0; + t0 <: t; + | BreakE (id, exp1) -> + begin + match T.Env.find_opt id.it env.labs with + | None -> + error env id.at "unbound label %s" id.it + | Some t1 -> + check_exp env exp1; + typ exp1 <: t1; + T.Non <: t1; (* vacuously true *) + end; + | RetE exp1 -> + begin + match env.rets with + | None -> + error env exp.at "misplaced return" + | Some t0 -> + assert (t0 <> T.Pre); + check_exp env exp1; + typ exp1 <: t0; + T.Non <: t; (* vacuously true *) + end; + | AsyncE exp1 -> + let t1 = typ exp1 in + let env' = + {env with labs = T.Env.empty; rets = Some t1; async = true} in + check_exp env' exp1; + t1 <: T.Shared; + T.Async t1 <: t + | 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 + with Invalid_argument _ -> + error env exp1.at "expected async type, but expression has type\n %s" + (T.string_of_typ_expand env.cons t1) + in + t2 <: t; + | AssertE exp1 -> + check_exp env exp1; + typ exp1 <: T.bool; + T.unit <: t; + | IsE (exp1, exp2) -> + (* TBR: restrict typ exp1 to objects? *) + check_exp env exp1; + check_exp env exp2; + typ exp2 <: T.Class; + T.bool <: t; + | DeclareE (id, t0, exp1) -> + check_typ env t0; + let env' = adjoin_vals env (T.Env.singleton id.it t0) in + check_exp env' exp1; + (typ exp1) <: t; + | DefineE (id, mut, exp1) -> + check_exp env exp1; + begin + match T.Env.find_opt id.it env.vals with + | None -> error env id.at "unbound variable %s" id.it + | Some t0 -> + match mut.it with + | Syntax.Const -> + typ exp1 <: t0 + | Syntax.Var -> + let t0 = try T.as_mut t0 with + | Invalid_argument _ -> + error env exp.at "expected mutable %s" (T.string_of_typ t0) + in + typ exp1 <: t0 + end; + T.unit <: t + | NewObjE (sort, labids, t0) -> + let t1 = + T.Obj(sort.it, + List.sort T.compare_field (List.map (fun (name,id) -> + {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 + check (T.is_obj t2) "bad annotation (object type expected)"; + t1 <: t2; + t0 <: t; + +(* Cases *) + +and check_cases env t_pat t cases = + List.iter (check_case env t_pat t) cases + +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 + error env exp.at "bad case" + +(* Patterns *) + +and gather_pat env ve0 pat : val_env = + let rec go ve pat = + match pat.it with + | WildP + | LitP _ -> + ve + | VarP id -> + if T.Env.mem id.it ve0 then + error env pat.at "duplicate binding for %s in block" id.it; + T.Env.add id.it pat.note ve (*TBR*) + | TupP pats -> + List.fold_left go ve pats + | AltP (pat1, pat2) -> + ve + | OptP pat1 -> + go ve pat1 + in T.Env.adjoin ve0 (go T.Env.empty pat) + +and check_pat_exhaustive env pat : val_env = + let ve = check_pat env pat in + (* TODO: actually check exhaustiveness *) + ve + +and check_pat env pat : val_env = + assert (pat.note <> T.Pre); + let (<:) = check_sub env pat.at in + let t = pat.note in + match pat.it with + | WildP -> T.Env.empty + | VarP id -> T.Env.singleton id.it pat.note + | LitP lit -> + let t1 = T.Prim (type_lit env lit pat.at) in + t1 <: t; + T.Env.empty + | TupP pats -> + let ve = check_pats pat.at env pats T.Env.empty in + let ts = List.map (fun pat -> pat.note) pats in + T.Tup ts <: t; + ve + | OptP pat1 -> + let ve = check_pat env pat1 in + T.Opt pat1.note <: t; + ve + | AltP (pat1, pat2) -> + let ve1 = check_pat env pat1 in + let ve2 = check_pat env pat2 in + pat1.note <: t; + pat2.note <: t; + check env pat.at (T.Env.is_empty ve1 && T.Env.is_empty ve2) + "variables are not allowed in pattern alternatives"; + T.Env.empty + +and check_pats at env pats ve : val_env = + match pats with + | [] -> ve + | pat::pats' -> + let ve1 = check_pat env pat in + let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in + check_pats at env pats' ve' + +(* Objects *) + +and type_obj env s id t fields : T.typ = + let ve = gather_exp_fields env id.it t fields in + let env' = adjoin_vals env ve in + let tfs, _ve = type_exp_fields env' s id.it t fields in + T.Obj(s,tfs) + +and gather_exp_fields env id t fields : val_env = + let ve0 = T.Env.singleton id t in + List.fold_left (gather_exp_field env) ve0 fields + +and gather_exp_field env ve field : val_env = + let {id; exp; mut; priv;_} : exp_field' = field.it in + if T.Env.mem id.it ve then + error env id.at "duplicate field name %s in object" id.it; + T.Env.add id.it ( make_mut mut (typ exp)) ve + +and type_exp_fields env s id t fields : T.field list * val_env = + let env' = add_val env id t in + let tfs, ve = + List.fold_left (type_exp_field env' s) ([], T.Env.empty) fields in + List.sort T.compare_field tfs, ve + +and is_func_exp exp = + match exp.it with + | BlockE ([dec],_)-> is_func_dec dec + | _ -> false + +and is_func_dec dec = + match dec.it with + | FuncD _ -> true + | _ -> false + +and type_exp_field env s (tfs, ve) field : T.field list * val_env = + let {id; name; exp; mut; priv} = field.it in + let t = try T.Env.find id.it env.vals with + | Not_found -> error env field.at "field typing not found" + in + assert (t <> T.Pre); + check_exp (adjoin_vals env ve) exp; + check_sub env field.at (typ exp) (T.as_immut t); + check env field.at ((mut.it = Syntax.Var) = T.is_mut t) + "inconsistent mutability of field and field type"; + check env field.at + ((s = T.Actor && priv.it = Syntax.Public) ==> + is_func_exp exp) + "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 + else true) + "public shared object or actor field has non-shared type"; + let ve' = T.Env.add id.it t ve in + let tfs' = + if priv.it = Syntax.Private + then tfs + else {T.name = Syntax.string_of_name name.it; typ = t} :: tfs + in tfs', ve' + + +(* Blocks and Declarations *) + +and type_block env decs at : T.typ * scope = + let scope = gather_block_decs env decs in + let t = type_block_exps (adjoin env scope) decs in + t, scope + +and type_block_exps env decs : T.typ = + match decs with + | [] -> T.unit + | [dec] -> + check_dec env dec; + typ dec; + | dec::decs' -> + 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 = cons_of_typ_binds typ_binds in + let ks = List.map (fun tp -> T.Abs([],tp.it.T.bound)) typ_binds in + let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in + let binds = T.close_binds cs (List.map (fun tb -> tb.it) typ_binds) in + let _,_ = check_typ_binds env binds in + cs,ce + +and check_dec env dec = + (* helpers *) + let check p = check env dec.at p in + let (<:) t1 t2 = check_sub env dec.at t1 t2 in + (* check effect *) + check (E.Ir.infer_effect_dec dec <= E.eff dec) + "inferred effect not a subtype of expected effect"; + (* check typing *) + let t = typ dec in + match dec.it with + | ExpD exp -> + check_exp env exp; + (typ exp) <: t + | LetD (_, exp) | VarD (_, exp) -> + check_exp env exp; + T.unit <: t + | FuncD (sort, 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 (Type.is_async t2 ==> isAsyncE exp) + "shared function with async type has non-async body"; + let env'' = + {env' with labs = T.Env.empty; rets = Some t2; async = false} in + check_exp (adjoin_vals env'' ve) exp; + check_sub env' dec.at (typ exp) t2; + t0 <: t; + | TypD (c, k) -> + let (binds,typ) = + match k with + | T.Abs(binds,typ) + | T.Def(binds,typ) -> (binds,typ) + in + let cs,ce = check_typ_binds env binds in + let ts = List.map (fun c -> T.Con(c,[])) cs in + let env' = adjoin_typs env ce in + check_typ env' (T.open_ ts typ); + T.unit <: t; + +and check_block env t decs at : scope = + let scope = gather_block_decs env decs in + check_block_exps (adjoin env scope) t decs at; + scope + +and check_block_exps env t decs at = + match decs with + | [] -> + 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) + "declaration does not produce expect type" + | dec::decs' -> + check_dec env dec; + check_block_exps env t decs' at + +and gather_block_decs env decs = + List.fold_left (gather_dec env) empty_scope decs + +and gather_dec env scope dec : scope = + match dec.it with + | ExpD _ -> + scope + | LetD (pat, _) -> + let ve = gather_pat env scope.val_env pat in + { scope with 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} + | FuncD (call_conv, id, typ_binds, pat, typ, exp) -> + let func_sort = call_conv.Value.sort in + let cs = cons_of_typ_binds typ_binds in + let t1 = pat.note in + let t2 = typ in + let ts1 = match call_conv.Value.n_args with + | 1 -> [t1] + | _ -> T.as_seq t1 + in + let ts2 = match call_conv.Value.n_res with + | 1 -> [t2] + | _ -> T.as_seq t2 + in + let c = match func_sort, t2 with + | T.Call T.Sharable, (T.Async _) -> T.Promises (* TBR: do we want this for T.Local too? *) + | _ -> T.Returns + in + let ts = List.map (fun typbind -> typbind.it.T.bound) typ_binds in + let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in + let t = T.Func (func_sort, c, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2) in + let ve' = T.Env.add id.it t scope.val_env in + {scope with val_env = ve'} + | TypD (c, k) -> + check env dec.at + (not (Con.Env.mem c scope.con_env)) + "duplicate definition of type in block"; + let ce' = Con.Env.add c k scope.con_env in + {scope with con_env = ce'} + +(* Programs *) + +let check_prog scope prog : scope = + let env = env_of_scope scope in + check_block env T.unit prog.it prog.at + +let type_prog scope prog : (T.typ * scope) = + let env = env_of_scope scope in + type_block env prog.it prog.at diff --git a/src/compile.ml b/src/compile.ml index 651a641175b..10ec16fabcc 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -3326,7 +3326,7 @@ and compile_exp (env : E.t) exp = G.i (Compare (Wasm.Values.I32 I32Op.Eq)) ) ] - | BlockE decs -> + | BlockE (decs,_) -> compile_decs env decs | LabelE (name, _ty, e) -> (* The value here can come from many places -- the expression, @@ -3381,9 +3381,9 @@ and compile_exp (env : E.t) exp = StackRep.Vanilla, compile_exp_vanilla env e1 ^^ (* offset to tuple (an array) *) Tuple.load_n (Int32.of_int n) - | ArrayE (m, es) -> + | ArrayE (m, t, es) -> StackRep.Vanilla, Array.lit env (List.map (compile_exp_vanilla env) es) - | ActorE (name, fs) -> + | ActorE (name, fs, _) -> StackRep.UnboxedReference, let captured = Freevars_ir.exp exp in let prelude_names = find_prelude_names env in @@ -3474,7 +3474,7 @@ and compile_exp (env : E.t) exp = StackRep.unit, compile_exp_vanilla env e ^^ Var.set_val env name.it - | NewObjE ({ it = Type.Object _ (*sharing*); _}, fs) -> + | NewObjE ({ it = Type.Object _ (*sharing*); _}, fs, _) -> StackRep.Vanilla, let fs' = List.map (fun (name, id) -> (name, fun env -> Var.get_val_ptr env id.it)) @@ -3778,7 +3778,7 @@ and compile_private_actor_field pre_env (f : Ir.exp_field) = and compile_public_actor_field pre_env (f : Ir.exp_field) = let (cc, name, _, pat, _rt, exp) = let find_func exp = match exp.it with - | BlockE [{it = FuncD (cc, name, ty_args, pat, rt, exp); _ }] -> + | BlockE ([{it = FuncD (cc, name, ty_args, pat, rt, exp); _ }],_) -> (cc, name, ty_args, pat, rt, exp) | _ -> assert false (* "public actor field not a function" *) in find_func f.it.exp in diff --git a/src/coverage.ml b/src/coverage.ml index 3d2b96337ee..16d2a2ff54a 100644 --- a/src/coverage.ml +++ b/src/coverage.ml @@ -63,7 +63,7 @@ let rec match_pat ce ctxt desc pat t sets = | LitP lit -> match_lit ce ctxt desc (value_of_lit !lit) t sets | SignP (op, lit) -> - let f = Operator.unop pat.note.note_typ op in + let f = Operator.unop pat.note op in match_lit ce ctxt desc (f (value_of_lit !lit)) t sets | TupP pats -> let ts = Type.as_tup (Type.promote ce t) in diff --git a/src/definedness.ml b/src/definedness.ml index 625377ef6e5..9d0cbfaf3e9 100644 --- a/src/definedness.ml +++ b/src/definedness.ml @@ -95,12 +95,12 @@ let rec exp msgs e : f = match e.it with | Type.Actor -> eagerify f | Type.Object _ -> f end - | DotE (e, i) -> exp msgs e + | DotE (e, _t, i) -> exp msgs e | AssignE (e1, e2) -> exps msgs [e1; e2] | ArrayE (m, es) -> exps msgs es | IdxE (e1, e2) -> exps msgs [e1; e2] | CallE (e1, ts, e2) -> eagerify (exps msgs [e1; e2]) - | BlockE ds -> decs msgs ds + | BlockE (ds, _) -> decs msgs ds | NotE e -> exp msgs e | AndE (e1, e2) -> exps msgs [e1; e2] | OrE (e1, e2) -> exps msgs [e1; e2] @@ -118,7 +118,7 @@ let rec exp msgs e : f = match e.it with | AssertE e -> exp msgs e | IsE (e, t) -> exp msgs e | AnnotE (e, t) -> exp msgs e - | DecE d -> close (dec msgs d) + | DecE (d, t) -> close (dec msgs d) | OptE e -> exp msgs e | DeclareE (i, t, e) -> exp msgs e // i.it | DefineE (i, m, e) -> id i ++ exp msgs e diff --git a/src/desugar.ml b/src/desugar.ml index d8ef7f918b3..dfa8b538d11 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -1,12 +1,21 @@ open Source module S = Syntax module I = Ir +module T = Type -(* Combinators used in the desguaring *) +(* TODO: clean me up when IrOps available, especially build_obj *) + +(* Combinators used in the desguaring *) -let true_lit : Ir.exp = I.LitE (S.BoolLit true) @@ no_region -let false_lit : Ir.exp = I.LitE (S.BoolLit false) @@ no_region +let bool_lit b : Ir.exp = + {Source.it = I.LitE (S.BoolLit b); + Source.at = no_region; + Source.note = {S.note_typ = T.bool; + S.note_eff = T.Triv} + } +let true_lit : Ir.exp = bool_lit true +let false_lit : Ir.exp = bool_lit false let apply_sign op l = Syntax.(match op, l with | PosOp, l -> l @@ -15,124 +24,196 @@ let apply_sign op l = Syntax.(match op, l with | _, _ -> raise (Invalid_argument "Invalid signed pattern") ) -let phrase ce f x = f ce x.it @@ x.at -let phrase' ce f x = f ce x.at x.note x.it @@ x.at +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 ce es = List.map (exp ce) es - and exp ce e = phrase' ce exp' e - and exp' ce at note = function + rec exps es = List.map (exp) es + and exp e = phrase' exp' e + and exp' at note = function | S.PrimE p -> I.PrimE p | S.VarE i -> I.VarE i | S.LitE l -> I.LitE !l | S.UnE (ot, o, e) -> - I.UnE (!ot, o, exp ce e) + I.UnE (!ot, o, exp e) | S.BinE (ot, e1, o, e2) -> - I.BinE (!ot, exp ce e1, o, exp ce e2) + I.BinE (!ot, exp e1, o, exp e2) | S.RelE (ot, e1, o, e2) -> - I.RelE (!ot, exp ce e1, o, exp ce e2) - | S.TupE es -> I.TupE (exps ce es) - | S.ProjE (e, i) -> I.ProjE (exp ce e, i) - | S.OptE e -> I.OptE (exp ce e) - | S.ObjE (s, i, es) -> obj ce at s None i es - | S.DotE (e, n) -> - begin match Type.as_immut (Type.promote ce (e.Source.note.S.note_typ)) with - | Type.Obj (Type.Actor, _) -> I.ActorDotE (exp ce e, n) - | Type.Obj (_, _) | Type.Array _ -> I.DotE (exp ce e, n) - | Type.Con _ -> raise (Invalid_argument ("Con in promoted type")) - | _ -> raise (Invalid_argument ("non-object in dot operator")) + I.RelE (!ot, exp e1, o, exp e2) + | S.TupE es -> I.TupE (exps es) + | S.ProjE (e, i) -> I.ProjE (exp e, i) + | S.OptE e -> I.OptE (exp e) + | S.ObjE (s, i, es) -> + let public_es = List.filter (fun e -> e.it.S.priv.it == Syntax.Public) es in + let obj_typ = + T.Obj(s.it, + List.sort T.compare_field + (List.map (fun {it = {Syntax.name;exp;mut;priv;_};_} -> + let t = exp.note.S.note_typ in + let t = if mut.it = Syntax.Var then Type.Mut t else t in + {Type.name = S.string_of_name name.it; + Type.typ = t}) public_es)) + in + obj at s None i es obj_typ + | S.DotE (e, sr, n) -> + begin match (!sr) with + | Type.Actor -> I.ActorDotE (exp e, n) + | _ -> I.DotE (exp e, n) end - | S.AssignE (e1, e2) -> I.AssignE (exp ce e1, exp ce e2) - | S.ArrayE (m, es) -> I.ArrayE (m, exps ce es) - | S.IdxE (e1, e2) -> I.IdxE (exp ce e1, exp ce e2) + | S.AssignE (e1, e2) -> I.AssignE (exp e1, exp e2) + | S.ArrayE (m, es) -> + let t = Type.as_array note.S.note_typ in + I.ArrayE (m, Type.as_immut t, exps es) + | S.IdxE (e1, e2) -> I.IdxE (exp e1, exp e2) | S.CallE (e1, inst, e2) -> let cc = Value.call_conv_of_typ e1.Source.note.S.note_typ in - let inst = List.map (fun t -> t.Source.it ) inst in - I.CallE (cc, exp ce e1, inst, exp ce e2) - | S.BlockE ds -> I.BlockE (decs ce ds) - | S.NotE e -> I.IfE (exp ce e, false_lit, true_lit) - | S.AndE (e1, e2) -> I.IfE (exp ce e1, exp ce e2, false_lit) - | S.OrE (e1, e2) -> I.IfE (exp ce e1, true_lit, exp ce e2) - | S.IfE (e1, e2, e3) -> I.IfE (exp ce e1, exp ce e2, exp ce e3) - | S.SwitchE (e1, cs) -> I.SwitchE (exp ce e1, cases ce cs) - | S.WhileE (e1, e2) -> I.WhileE (exp ce e1, exp ce e2) - | S.LoopE (e1, None) -> I.LoopE (exp ce e1, None) - | S.LoopE (e1, Some e2) -> I.LoopE (exp ce e1, Some (exp ce e2)) - | S.ForE (p, e1, e2) -> I.ForE (pat ce p, exp ce e1, exp ce e2) - | S.LabelE (l, t, e) -> I.LabelE (l, t, exp ce e) - | S.BreakE (l, e) -> I.BreakE (l, exp ce e) - | S.RetE e -> I.RetE (exp ce e) - | S.AsyncE e -> I.AsyncE (exp ce e) - | S.AwaitE e -> I.AwaitE (exp ce e) - | S.AssertE e -> I.AssertE (exp ce e) - | S.IsE (e1, e2) -> I.IsE (exp ce e1, exp ce e2) - | S.AnnotE (e, _) -> exp' ce at note e.it - | S.DecE d -> I.BlockE [dec ce d] - | S.DeclareE (i, t, e) -> I.DeclareE (i, t, exp ce e) - | S.DefineE (i, m, e) -> I.DefineE (i, m, exp ce e) - | S.NewObjE (s, fs) -> I.NewObjE (s, fs) - - and field_to_dec ce (f : S.exp_field) : Ir.dec = - match f.it.S.mut.it with - | S.Const -> I.LetD (I.VarP f.it.S.id @@ no_region, exp ce f.it.S.exp) @@ f.at - | S.Var -> I.VarD (f.it.S.id, exp ce f.it.S.exp) @@ f.at - + let inst = List.map (fun t -> t.Source.note) inst in + I.CallE (cc, exp e1, inst, exp e2) + | S.BlockE (ds, ot) -> I.BlockE (decs ds, !ot) + | S.NotE e -> I.IfE (exp e, false_lit, true_lit) + | S.AndE (e1, e2) -> I.IfE (exp e1, exp e2, false_lit) + | S.OrE (e1, e2) -> I.IfE (exp e1, true_lit, 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.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.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) + | S.AsyncE e -> I.AsyncE (exp e) + | S.AwaitE e -> I.AwaitE (exp e) + | S.AssertE e -> I.AssertE (exp e) + | S.IsE (e1, e2) -> I.IsE (exp e1, exp e2) + | S.AnnotE (e, _) -> exp' at note e.it + | S.DecE (d, ot) -> I.BlockE (decs [d], !ot) + | S.DeclareE (i, t, e) -> I.DeclareE (i, t, exp e) + | S.DefineE (i, m, e) -> I.DefineE (i, m, exp e) + | S.NewObjE (s, fs) -> I.NewObjE (s, fs, note.S.note_typ) + + and field_to_dec (f : S.exp_field) : Ir.dec = + let {it={S.id;S.exp=e;S.mut;_};at;note} = f in + let d = match mut.it with + | S.Const -> I.LetD ({it = I.VarP id; + at = no_region; + note = e.note.S.note_typ + }, + exp e) + | S.Var -> + I.VarD (id, exp e) + in + { it = d; + at; + note = { e.note with S.note_typ = T.unit} + } and field_to_obj_entry (f : S.exp_field) = match f.it.S.priv.it with | S.Private -> [] | S.Public -> [ (f.it.S.name, f.it.S.id) ] - and obj ce at s class_id self_id es = + and obj at s class_id self_id es obj_typ = match s.it with - | Type.Object _ -> build_obj ce at None self_id es - | Type.Actor -> I.ActorE (self_id, exp_fields ce es) + | Type.Object _ -> build_obj at None self_id es obj_typ + | Type.Actor -> I.ActorE (self_id, exp_fields es, obj_typ) - and build_obj ce at class_id self_id es = + and build_obj at class_id self_id es obj_typ = I.BlockE ( - List.map (field_to_dec ce) es @ - [ I.LetD ( - I.VarP self_id @@ at, - I.NewObjE - (Type.Object Type.Local @@ at, - List.concat (List.map field_to_obj_entry es)) @@ at - ) @@ at; - I.ExpD (I.VarE self_id @@ at) @@ at]) - - and exp_fields ce fs = List.map (exp_field ce) fs - and exp_field ce f = phrase ce exp_field' f - and exp_field' cd (f : S.exp_field') = - S.{ I.name = f.name; I.id = f.id; I.exp = exp cd f.exp; I.mut = f.mut; I.priv = f.priv} - - and decs ce ds = List.map (dec ce) ds - and dec ce d = phrase' ce dec' d - and dec' ce at n = function - | S.ExpD e -> I.ExpD (exp ce e) - | S.LetD (p, e) -> I.LetD (pat ce p, exp ce e) - | S.VarD (i, e) -> I.VarD (i, exp ce e) - | S.FuncD (s, i, tp, p, ty, e) -> + List.map (field_to_dec) es @ + [ {it = I.LetD ( + {it = I.VarP self_id; + at = at; + note = obj_typ + }, + {it = I.NewObjE + (Type.Object Type.Local @@ at, + List.concat (List.map field_to_obj_entry es), + obj_typ + ); + at = at; + note = {S.note_typ = obj_typ; S.note_eff = T.Triv}} + ); + at = no_region; + note = {S.note_typ = T.unit; + S.note_eff = T.Triv}}; + {it = I.ExpD {it = I.VarE self_id; + at; + note = {S.note_typ = obj_typ; + S.note_eff = T.Triv}}; + at = at; + note = {S.note_typ = obj_typ; + S.note_eff = T.Triv}}; + ], + obj_typ) + + and exp_fields fs = List.map (exp_field) fs + and exp_field f = phrase exp_field' f + and exp_field' (f : S.exp_field') = + S.{ I.name = f.name; I.id = f.id; I.exp = exp f.exp; I.mut = f.mut; I.priv = f.priv} + + + and typ_binds tbs = List.map (typ_bind) tbs + and typ_bind tb = + phrase' typ_bind' tb + and typ_bind' at n {S.var; S.bound} = {Type.var = var.it; Type.bound = bound.note} + and decs ds = + match ds with + | [] -> [] + | 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); + at = d.at; + note = {S.note_typ = T.unit; S.note_eff = T.Triv}} + in + typD::(phrase' dec' d)::(decs ds) + | _ -> (phrase' dec' d)::(decs ds) + and dec' at n d = match d with + | S.ExpD e -> I.ExpD (exp e) + | S.LetD (p, e) -> I.LetD (pat p, exp e) + | S.VarD (i, e) -> I.VarD (i, exp e) + | S.FuncD (s, i, tbs, p, ty, e) -> let cc = Value.call_conv_of_typ n.S.note_typ in - I.FuncD (cc, i, tp, pat ce p, ty, exp ce e) - | S.TypD (i, ty, t) -> I.TypD (i, ty, t) - | S.ClassD (fun_id, typ_id, tp, s, p, self_id, es) -> + 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) + | S.ClassD (fun_id, typ_id, tbs, s, p, self_id, es) -> let cc = Value.call_conv_of_typ n.S.note_typ in - I.FuncD (cc, fun_id, tp, pat ce p, S.PrimT "dummy" @@ at, - obj ce at s (Some fun_id) self_id es @@ at) - - and cases ce cs = List.map (case ce) cs - and case ce c = phrase ce case' c - and case' ce c = S.{ I.pat = pat ce c.pat; I.exp = exp ce c.exp} - - and pats ce ps = List.map (pat ce) ps - and pat ce p = phrase ce pat' p - and pat' ce = function + let inst = List.map + (fun tb -> + match tb.note with + | Type.Pre -> assert false + | t -> t) + tbs in + let obj_typ = + match n.S.note_typ with + | T.Func(s,c,bds,dom,[rng]) -> + assert(List.length inst = List.length bds); + T.open_ inst rng + | _ -> assert false + in + I.FuncD (cc, fun_id, typ_binds tbs, pat p, obj_typ, (* TBR *) + {it = obj at s (Some fun_id) self_id es obj_typ; + at = at; + note = {S.note_typ = obj_typ; S.note_eff = T.Triv}}) + + and cases cs = List.map (case) cs + and case c = phrase case' c + and case' c = S.{ I.pat = pat c.pat; I.exp = exp c.exp} + + and pats ps = List.map (pat) ps + and pat p = phrase pat' p + and pat' = function | S.VarP v -> I.VarP v | S.WildP -> I.WildP | S.LitP l -> I.LitP !l | S.SignP (o, l) -> I.LitP (apply_sign o !l) - | S.TupP ps -> I.TupP (pats ce ps) - | S.OptP p -> I.OptP (pat ce p) - | S.AltP (p1, p2) -> I.AltP (pat ce p1, pat ce p2) - | S.AnnotP (p, _) -> pat' ce p.it + | S.TupP ps -> I.TupP (pats ps) + | S.OptP p -> I.OptP (pat p) + | S.AltP (p1, p2) -> I.AltP (pat p1, pat p2) + | S.AnnotP (p, _) -> pat' p.it - and prog ce p = phrase ce decs p + and prog p = phrase decs p diff --git a/src/desugar.mli b/src/desugar.mli index e5b8ac30616..a2ec063ac2d 100644 --- a/src/desugar.mli +++ b/src/desugar.mli @@ -1 +1 @@ -val prog : Typing.con_env -> Syntax.prog -> Ir.prog +val prog : Syntax.prog -> Ir.prog diff --git a/src/diag.ml b/src/diag.ml index 33e4e12b4f9..bb7aa815896 100644 --- a/src/diag.ml +++ b/src/diag.ml @@ -23,11 +23,14 @@ let has_errors : messages -> bool = let fatal_error at text = { sev = Error; at; cat = "fatal"; text } -let print_message msg = +let string_of_message msg = let label = match msg.sev with | Error -> Printf.sprintf "%s error" msg.cat | Warning -> "warning" in - Printf.eprintf "%s: %s, %s\n%!" (Source.string_of_region msg.at) label msg.text + Printf.sprintf "%s: %s, %s\n" (Source.string_of_region msg.at) label msg.text + +let print_message msg = + Printf.eprintf "%s%!" (string_of_message msg) let print_messages = List.iter print_message diff --git a/src/diag.mli b/src/diag.mli index 2558b46c136..ddd3fe39efb 100644 --- a/src/diag.mli +++ b/src/diag.mli @@ -13,6 +13,7 @@ type messages = message list val fatal_error : Source.region -> string -> message +val string_of_message : message -> string val print_message : message -> unit val print_messages : messages -> unit diff --git a/src/effect.ml b/src/effect.ml index d8a8c1fcdad..ef7ee3e6d1a 100644 --- a/src/effect.ml +++ b/src/effect.ml @@ -13,51 +13,57 @@ let max_eff e1 e2 = | _ , T.Await -> T.Await | T.Await,_ -> T.Await -let effect_exp (exp:Syntax.exp) : T.eff = - exp.note.note_eff - -(* infer the effect of an expression, assuming all sub-expressions are correctly effect-annotated *) +let typ phrase = phrase.note.note_typ + +let eff phrase = phrase.note.note_eff + +let is_triv phrase = + eff phrase = T.Triv + +let effect_exp (exp:Syntax.exp) : T.eff = eff exp + +(* infer the effect of an expression, assuming all sub-expressions are correctly effect-annotated es*) let rec infer_effect_exp (exp:Syntax.exp) : T.eff = match exp.it with | PrimE _ - | VarE _ + | VarE _ | LitE _ -> T.Triv | UnE (_, _, exp1) | ProjE (exp1, _) | OptE exp1 - | DotE (exp1, _) + | DotE (exp1, _, _) | NotE exp1 - | AssertE exp1 - | LabelE (_, _, exp1) - | BreakE (_, exp1) - | RetE exp1 - | AnnotE (exp1, _) - | LoopE (exp1, None) -> - effect_exp exp1 + | AssertE exp1 + | LabelE (_, _, exp1) + | BreakE (_, exp1) + | RetE exp1 + | AnnotE (exp1, _) + | LoopE (exp1, None) -> + effect_exp exp1 | BinE (_, exp1, _, exp2) | IdxE (exp1, exp2) - | IsE (exp1, exp2) - | RelE (_, exp1, _, exp2) - | AssignE (exp1, exp2) - | CallE (exp1, _, exp2) + | IsE (exp1, exp2) + | RelE (_, exp1, _, exp2) + | AssignE (exp1, exp2) + | CallE (exp1, _, exp2) | AndE (exp1, exp2) - | OrE (exp1, exp2) - | WhileE (exp1, exp2) - | LoopE (exp1, Some exp2) + | OrE (exp1, exp2) + | WhileE (exp1, exp2) + | LoopE (exp1, Some exp2) | ForE (_, exp1, exp2)-> let t1 = effect_exp exp1 in let t2 = effect_exp exp2 in max_eff t1 t2 - | TupE exps + | TupE exps | ArrayE (_, exps) -> let es = List.map effect_exp exps in List.fold_left max_eff Type.Triv es - | BlockE decs -> + | BlockE (decs,_) -> let es = List.map effect_dec decs in - List.fold_left max_eff Type.Triv es + List.fold_left max_eff Type.Triv es | ObjE (_, _, efs) -> - effect_field_exps efs + effect_field_exps efs | IfE (exp1, exp2, exp3) -> let e1 = effect_exp exp1 in let e2 = effect_exp exp2 in @@ -70,8 +76,8 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff = | AsyncE exp1 -> T.Triv | AwaitE exp1 -> - T.Await - | DecE d -> + T.Await + | DecE (d, _) -> effect_dec d | DeclareE (_, _, exp1) -> effect_exp exp1 @@ -79,7 +85,7 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff = effect_exp exp1 | NewObjE _ -> T.Triv - + and effect_cases cases = match cases with | [] -> @@ -90,14 +96,14 @@ and effect_cases cases = and effect_field_exps efs = List.fold_left (fun e (fld:exp_field) -> max_eff e (effect_exp fld.it.exp)) T.Triv efs - + and effect_dec dec = dec.note.note_eff -and infer_effect_dec dec = +and infer_effect_dec dec = match dec.it with | ExpD e - | LetD (_,e) + | LetD (_,e) | VarD (_, e) -> effect_exp e | TypD (v, tps, t) -> @@ -107,10 +113,99 @@ and infer_effect_dec dec = | ClassD (v, l, tps, s, p, v', efs) -> T.Triv +(* effect inference on Ir *) -let typ phrase = phrase.note.note_typ +(* TODO: remove effect inference on Source once await.ml ported to work on IR + since effect inference is purely syntactic, we could roll this into desugaring +*) -let eff phrase = phrase.note.note_eff +module Ir = + struct + open Ir -let is_triv phrase = - eff phrase = T.Triv + let effect_exp (exp: exp) : T.eff = eff exp + + (* infer the effect of an expression, assuming all sub-expressions are correctly effect-annotated es*) + let rec infer_effect_exp (exp: exp) : T.eff = + match exp.it with + | PrimE _ + | VarE _ + | LitE _ -> + T.Triv + | UnE (_, _, exp1) + | ProjE (exp1, _) + | OptE exp1 + | DotE (exp1, _) + | ActorDotE (exp1, _) + | AssertE exp1 + | LabelE (_, _, exp1) + | BreakE (_, exp1) + | RetE exp1 + | LoopE (exp1, None) -> + effect_exp exp1 + | BinE (_, exp1, _, exp2) + | IdxE (exp1, exp2) + | IsE (exp1, exp2) + | RelE (_, exp1, _, exp2) + | AssignE (exp1, exp2) + | CallE (_, exp1, _, exp2) + | WhileE (exp1, exp2) + | LoopE (exp1, Some exp2) + | ForE (_, exp1, exp2) -> + let t1 = effect_exp exp1 in + let t2 = effect_exp exp2 in + max_eff t1 t2 + | TupE exps + | ArrayE (_, _, exps) -> + let es = List.map effect_exp exps in + List.fold_left max_eff Type.Triv es + | BlockE (decs,_) -> + let es = List.map effect_dec decs in + List.fold_left max_eff Type.Triv es + | IfE (exp1, exp2, exp3) -> + let e1 = effect_exp exp1 in + let e2 = effect_exp exp2 in + let e3 = effect_exp exp3 in + max_eff e1 (max_eff e2 e3) + | SwitchE (exp1, cases) -> + let e1 = effect_exp exp1 in + let e2 = effect_cases cases in + max_eff e1 e2 + | ActorE (_,efs,_) -> + effect_field_exps efs + | AsyncE exp1 -> + T.Triv + | AwaitE exp1 -> + T.Await + | DeclareE (_, _, exp1) -> + effect_exp exp1 + | DefineE (_, _, exp1) -> + effect_exp exp1 + | NewObjE _ -> + T.Triv + + and effect_cases cases = + match cases with + | [] -> + T.Triv + | {it = {pat; exp}; _}::cases' -> + let e = effect_exp exp in + max_eff e (effect_cases cases') + + and effect_field_exps efs = + List.fold_left (fun e (fld:exp_field) -> max_eff e (effect_exp fld.it.exp)) T.Triv efs + + and effect_dec dec = + dec.note.note_eff + + and infer_effect_dec (dec:Ir.dec) = + match dec.it with + | ExpD e + | LetD (_,e) + | VarD (_, e) -> + effect_exp e + | TypD (c,k) -> + T.Triv + | FuncD (s, v, tps, p, t, e) -> + T.Triv +end diff --git a/src/effect.mli b/src/effect.mli index c816396c645..5585f452ba8 100644 --- a/src/effect.mli +++ b/src/effect.mli @@ -1,15 +1,25 @@ -open Source +open Source open Syntax open Type val max_eff : eff -> eff -> eff -val effect_exp: exp -> eff +(* (incremental) effect inference on Source *) +(* TODO: delete once await.ml ported to IR *) +val effect_exp: exp -> eff val infer_effect_exp : exp -> eff val infer_effect_dec : dec -> eff val typ : ('a, typ_note) annotated_phrase -> typ val eff : ('a, typ_note) annotated_phrase -> eff -val is_triv : ('a, typ_note) annotated_phrase -> bool +val is_triv : ('a, typ_note) annotated_phrase -> bool + +(* (incremental) effect inference on IR *) + +module Ir : sig + val effect_exp: Ir.exp -> eff + val infer_effect_exp : Ir.exp -> eff + val infer_effect_dec : Ir.dec -> eff +end diff --git a/src/env.ml b/src/env.ml index b45cea3d94f..1749cb55b64 100644 --- a/src/env.ml +++ b/src/env.ml @@ -26,4 +26,5 @@ struct let disjoint_union env1 env2 = union (fun k _ _ -> raise (Clash k)) env1 env2 let disjoint_unions envs = List.fold_left disjoint_union empty envs let disjoint_add k x env = disjoint_union env (singleton k x) + end diff --git a/src/freevars.ml b/src/freevars.ml index b8a19adb741..7e1d3ac32ba 100644 --- a/src/freevars.ml +++ b/src/freevars.ml @@ -42,12 +42,12 @@ let rec exp e : f = match e.it with | TupE es -> exps es | ProjE (e, i) -> exp e | ObjE (s, i, efs) -> close (exp_fields efs) // i.it - | DotE (e, i) -> exp e + | DotE (e, _, i) -> exp e | AssignE (e1, e2) -> exps [e1; e2] | ArrayE (m, es) -> exps es | IdxE (e1, e2) -> exps [e1; e2] | CallE (e1, ts, e2) -> exps [e1; e2] - | BlockE ds -> close (decs ds) + | BlockE (ds, _) -> close (decs ds) | NotE e -> exp e | AndE (e1, e2) -> exps [e1; e2] | OrE (e1, e2) -> exps [e1; e2] @@ -65,7 +65,7 @@ let rec exp e : f = match e.it with | AssertE e -> exp e | IsE (e, t) -> exp e | AnnotE (e, t) -> exp e - | DecE d -> close (dec d) + | DecE (d, _ot) -> close (dec d) | OptE e -> exp e | DeclareE (i, t, e) -> exp e // i.it | DefineE (i, m, e) -> (id i) ++ exp e diff --git a/src/freevars_ir.ml b/src/freevars_ir.ml index b44e43c1ee1..d11a9e6b6df 100644 --- a/src/freevars_ir.ml +++ b/src/freevars_ir.ml @@ -67,14 +67,14 @@ let rec exp e : f = match e.it with | RelE (_, e1, ro, e2)-> exps [e1; e2] | TupE es -> exps es | ProjE (e, i) -> exp e - | ActorE (i, efs) -> close (exp_fields efs) // i.it + | ActorE (i, efs, _) -> close (exp_fields efs) // i.it | DotE (e, i) -> exp e | ActorDotE (e, i) -> exp e | AssignE (e1, e2) -> exps [e1; e2] - | ArrayE (m, es) -> exps es + | ArrayE (m, t, es) -> exps es | IdxE (e1, e2) -> exps [e1; e2] | CallE (_, e1, ts, e2) -> exps [e1; e2] - | BlockE ds -> close (decs ds) + | BlockE (ds, _) -> close (decs ds) | IfE (e1, e2, e3) -> exps [e1; e2; e3] | SwitchE (e, cs) -> exp e ++ cases cs | WhileE (e1, e2) -> exps [e1; e2] @@ -91,7 +91,7 @@ let rec exp e : f = match e.it with | OptE e -> exp e | DeclareE (i, t, e) -> exp e // i.it | DefineE (i, m, e) -> id i ++ exp e - | NewObjE (_,ids) -> unions id (List.map (fun (lab,id) -> id) ids) + | NewObjE (_, ids, _) -> unions id (List.map (fun (lab,id) -> id) ids) and exps es : f = unions exp es @@ -123,7 +123,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 (i, tp, t) -> (M.empty, S.empty) + | TypD (c,k) -> (M.empty, S.empty) (* The variables captured by a function. May include the function itself! *) and captured p e = diff --git a/src/interpret.ml b/src/interpret.ml index e5d5e2e15b4..a257353e2e3 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -289,7 +289,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = interpret_exp env exp1 (fun v1 -> k (List.nth (V.as_tup v1) n)) | ObjE (sort, id, fields) -> interpret_obj env sort id None fields k - | DotE (exp1, {it = Name n;_}) -> + | DotE (exp1, _, {it = Name n;_}) -> interpret_exp env exp1 (fun v1 -> let _, fs = V.as_obj v1 in k (try find n fs with _ -> assert false) @@ -331,7 +331,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = *) ) ) - | BlockE decs -> + | BlockE (decs, _)-> interpret_block env decs None k | NotE exp1 -> interpret_exp env exp1 (fun v1 -> k (V.Bool (not (V.as_bool v1)))) @@ -432,7 +432,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = ) | AnnotE (exp1, _typ) -> interpret_exp env exp1 k - | DecE dec -> + | DecE (dec, _) -> interpret_block env [dec] None k | DeclareE (id, typ, exp1) -> let env = adjoin_vals env (declare_id id) in @@ -548,7 +548,7 @@ and match_pat pat v : val_env option = then Some V.Env.empty else None | SignP (op, lit) -> - let t = T.as_immut pat.note.note_typ in + let t = T.as_immut pat.note in match_pat {pat with it = LitP lit} (Operator.unop t op v) | TupP pats -> match_pats pats (V.as_tup v) V.Env.empty diff --git a/src/ir.ml b/src/ir.ml index 944aacda41a..a6fed1e0286 100644 --- a/src/ir.ml +++ b/src/ir.ml @@ -1,6 +1,10 @@ (* Patterns *) -type pat = pat' Source.phrase +type 'a phrase = ('a, Syntax.typ_note) Source.annotated_phrase + +type typ_bind = (Type.bind, Type.typ) Source.annotated_phrase + +type pat = (pat', Type.typ) Source.annotated_phrase and pat' = | WildP (* wildcard *) | VarP of Syntax.id (* variable *) @@ -11,40 +15,45 @@ and pat' = (* Expressions *) -type exp = exp' Source.phrase +type exp = exp' phrase and exp' = | PrimE of string (* primitive *) | VarE of Syntax.id (* variable *) | LitE of Syntax.lit (* literal *) - | UnE of Type.typ * Syntax.unop * exp (* unary operator *) - | BinE of Type.typ * exp * Syntax.binop * exp (* binary operator *) - | RelE of Type.typ * exp * Syntax.relop * exp (* relational operator *) + | UnE of Type.typ * Syntax.unop * exp (* unary operator *) + | BinE of (* binary operator *) + Type.typ * exp * Syntax.binop * exp + | RelE of (* relational operator *) + Type.typ * exp * Syntax.relop * exp | TupE of exp list (* tuple *) | ProjE of exp * int (* tuple projection *) | OptE of exp (* option injection *) - | ActorE of Syntax.id * exp_field list (* actor *) + | ActorE of (* actor *) + Syntax.id * exp_field list * Type.typ | DotE of exp * Syntax.name (* object projection *) | ActorDotE of exp * Syntax.name (* actor field access *) | AssignE of exp * exp (* assignment *) - | ArrayE of Syntax.mut * exp list (* array *) + | ArrayE of Syntax.mut * Type.typ * exp list (* array *) | IdxE of exp * exp (* array indexing *) - | CallE of Value. call_conv * exp * Syntax.typ list * exp (* function call *) - | BlockE of dec list (* block *) + | CallE of (* function call *) + Value. call_conv * exp * Type.typ list * exp + | BlockE of dec list * Type.typ (* block *) | IfE of exp * exp * exp (* conditional *) | SwitchE of exp * case list (* switch *) | WhileE of exp * exp (* while-do loop *) | LoopE of exp * exp option (* do-while loop *) | ForE of pat * exp * exp (* iteration *) - | LabelE of Syntax.id * Syntax.typ * exp (* label *) + | LabelE of Syntax.id * Type.typ * exp (* label *) | BreakE of Syntax.id * exp (* break *) | RetE of exp (* return *) | AsyncE of exp (* async *) | AwaitE of exp (* await *) | AssertE of exp (* assertion *) | IsE of exp * exp (* instance-of *) - | DeclareE of Syntax.id * Type.typ * exp (* local promise (internal) *) - | DefineE of Syntax.id * Syntax.mut * exp (* promise fulfillment (internal) *) - | NewObjE of Syntax.obj_sort * (Syntax.name * Syntax.id) list (* make an object, preserving mutable identity (internal) *) + | DeclareE of Syntax.id * Type.typ * exp (* local promise *) + | DefineE of Syntax.id * Syntax.mut * exp (* promise fulfillment *) + | NewObjE of (* make an object, preserving mutable identity *) + Syntax.obj_sort * (Syntax.name * Syntax.id) list * Type.typ and exp_field = exp_field' Source.phrase and exp_field' = {name : Syntax.name; id : Syntax.id; exp : exp; mut : Syntax.mut; priv : Syntax.priv} @@ -55,13 +64,14 @@ and case' = {pat : pat; exp : exp} (* Declarations *) -and dec = dec' Source.phrase +and dec = dec' phrase and dec' = - | ExpD of exp (* plain expression *) - | LetD of pat * exp (* immutable *) - | VarD of Syntax.id * exp (* mutable *) - | FuncD of Value.call_conv * Syntax.id * Syntax.typ_bind list * pat * Syntax.typ * exp (* function *) - | TypD of Syntax.id * Syntax.typ_bind list * Syntax.typ (* type *) + | ExpD of exp (* plain expression *) + | LetD of pat * exp (* immutable *) + | 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 *) (* Program *) diff --git a/src/parser.mly b/src/parser.mly index 4f7cb35cc01..790010219b8 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -21,8 +21,10 @@ let positions_to_region position1 position2 = let at (startpos, endpos) = positions_to_region startpos endpos let (@?) it at = {it; at; note = empty_typ_note} -let (@!) it at = {it; at; note = ref None} +let (@!) it at = {it; at; note = Type.Pre} +let (@=) it at = {it; at; note = None} +let dummy_obj_sort() = ref (Type.Object Type.Local) let dup_var x = VarE (x.it @@ x.at) @? x.at let name_exp e = @@ -30,15 +32,15 @@ let name_exp e = | VarE x -> [], e, dup_var x | _ -> let x = ("anon-val-" ^ string_of_pos (e.at.left)) @@ e.at in - [LetD (VarP x @? x.at, e) @? e.at], dup_var x, dup_var x + [LetD (VarP x @! x.at, e) @? e.at], dup_var x, dup_var x let assign_op lhs rhs_f at = let ds, lhs', rhs' = match lhs.it with | VarE x -> [], lhs, dup_var x - | DotE (e1, x) -> + | DotE (e1, _, x) -> let ds, ex11, ex12 = name_exp e1 in - ds, DotE (ex11, x) @? lhs.at, DotE (ex12, x.it @@ x.at) @? lhs.at + ds, DotE (ex11, dummy_obj_sort(), x) @? lhs.at, DotE (ex12, dummy_obj_sort(), x.it @@ x.at) @? lhs.at | IdxE (e1, e2) -> let ds1, ex11, ex12 = name_exp e1 in let ds2, ex21, ex22 = name_exp e2 in @@ -49,14 +51,14 @@ let assign_op lhs rhs_f at = let e = AssignE (lhs', rhs_f rhs') @? at in match ds with | [] -> e - | ds -> BlockE (ds @ [ExpD e @? e.at]) @? at + | ds -> BlockE (ds @ [ExpD e @? e.at], ref Type.Pre) @? at let share_typ t = match t.it with | ObjT ({it = Type.Object Type.Local; _} as s, tfs) -> - ObjT ({s with it = Type.Object Type.Sharable}, tfs) @@ t.at + { t with it = ObjT ({s with it = Type.Object Type.Sharable}, tfs)} | FuncT ({it = Type.Call Type.Local; _} as s, tbs, t1, t2) -> - FuncT ({s with it = Type.Call Type.Sharable}, tbs, t1, t2) @@ t.at + { t with it = FuncT ({s with it = Type.Call Type.Sharable}, tbs, t1, t2)} | _ -> t let share_typfield tf = @@ -72,8 +74,8 @@ let share_exp e = match e.it with | ObjE ({it = Type.Object Type.Local; _} as s, x, efs) -> ObjE ({s with it = Type.Object Type.Sharable}, x, efs) @? e.at - | DecE d -> - DecE (share_dec d) @? e.at + | DecE (d, ot) -> + DecE (share_dec d, ot) @? e.at | _ -> e let share_expfield (ef : exp_field) = @@ -155,6 +157,9 @@ seplist1(X, SEP) : %inline id : | id=ID { id @@ at $sloc } +%inline con_id : + | id=ID { id @= at $sloc } + %inline id_opt : | id=ID { fun _ _ -> id @@ at $sloc } @@ -194,43 +199,43 @@ typ_obj : typ_nullary : | LPAR t=typ RPAR - { ParT(t) @@ at $loc } + { ParT(t) @! at $loc } | LPAR ts=seplist1(typ_item, COMMA) RPAR - { TupT(ts) @@ at $sloc } + { TupT(ts) @! at $sloc } | x=id tso=typ_args? - { VarT(x, Lib.Option.get tso []) @@ at $sloc } + { VarT(x, Lib.Option.get tso []) @! at $sloc } | LBRACKET m=var_opt t=typ RBRACKET - { ArrayT(m, t) @@ at $sloc } + { ArrayT(m, t) @! at $sloc } | tfs=typ_obj - { ObjT(Type.Object Type.Local @@ at $sloc, tfs) @@ at $sloc } + { ObjT(Type.Object Type.Local @@ at $sloc, tfs) @! at $sloc } typ_un : | t=typ_nullary { t } | QUEST t=typ_un - { OptT(t) @@ at $sloc } + { OptT(t) @! at $sloc } typ_pre : | t=typ_un { t } | PRIM s=TEXT - { PrimT(s) @@ at $sloc } + { PrimT(s) @! at $sloc } | ASYNC t=typ_pre - { AsyncT(t) @@ at $sloc } + { AsyncT(t) @! at $sloc } | LIKE t=typ_pre - { LikeT(t) @@ at $sloc } + { LikeT(t) @! at $sloc } | s=obj_sort tfs=typ_obj { let tfs' = if s.it = Type.Object Type.Local then tfs else List.map share_typfield tfs - in ObjT(s, tfs') @@ at $sloc } + in ObjT(s, tfs') @! at $sloc } typ : | t=typ_pre { t } | s=func_sort_opt tps=typ_params_opt t1=typ_un ARROW t2=typ - { FuncT(s, tps, t1, t2) @@ at $sloc } + { FuncT(s, tps, t1, t2) @! at $sloc } typ_item : | id COLON t=typ { t } @@ -248,14 +253,14 @@ typ_field : { {id = x; typ = t; mut} @@ at $sloc } | x=id tps=typ_params_opt t1=typ_nullary t2=return_typ { let t = FuncT(Type.Call Type.Local @@ no_region, tps, t1, t2) - @@ span x.at t2.at in + @! span x.at t2.at in {id = x; typ = t; mut = Const @@ no_region} @@ at $sloc } typ_bind : | x=id SUB t=typ { {var = x; bound = t} @! at $sloc } | x=id - { {var = x; bound = PrimT "Any" @@ at $sloc} @! at $sloc } + { {var = x; bound = PrimT "Any" @! at $sloc} @! at $sloc } @@ -322,7 +327,7 @@ lit : exp_block : | LCURLY ds=seplist(dec, semicolon) RCURLY - { BlockE(ds) @? at $sloc } + { BlockE(ds, ref Type.Pre) @? at $sloc } exp_nullary : | e=exp_block @@ -348,11 +353,10 @@ exp_post : | e=exp_post DOT s=NAT { ProjE (e, int_of_string s) @? at $sloc } | e=exp_post DOT x=id - { DotE(e, {x with it = Name x.it}) @? at $sloc } + { DotE(e, dummy_obj_sort(), {x with it = Name x.it}) @? at $sloc } | e1=exp_post tso=typ_args? e2=exp_nullary { let typ_args = Lib.Option.get tso [] in - let typ_insts = List.map (fun typ_arg -> {it = typ_arg; at = typ_arg.at; note = ref Type.Pre}) typ_args in - CallE(e1, typ_insts, e2) @? at $sloc } + CallE(e1, typ_args, e2) @? at $sloc } exp_un : | e=exp_post @@ -404,7 +408,7 @@ exp_nondec : { e } | LABEL x=id rt=return_typ_nullary? e=exp { let x' = ("continue " ^ x.it) @@ x.at in - let t = Lib.Option.get rt (TupT [] @@ at $sloc) in + let t = Lib.Option.get rt (TupT [] @! at $sloc) in let e' = match e.it with | WhileE (e1, e2) -> WhileE (e1, LabelE (x', t, e2) @? e2.at) @? e.at @@ -437,7 +441,7 @@ exp_nonvar : | e=exp_nondec { e } | d=dec_nonvar - { DecE(d) @? at $sloc } + { DecE(d, ref Type.Pre) @? at $sloc } (* TODO(andreas): hack, remove *) | s=obj_sort xf=id_opt EQ? efs=obj_body { let anon = if s.it = Type.Actor then "actor" else "object" in @@ -451,7 +455,7 @@ exp : | e=exp_nonvar { e } | d=dec_var - { DecE(d) @? at $sloc } + { DecE(d, ref Type.Pre) @? at $sloc } case : @@ -470,38 +474,38 @@ exp_field : {name = {x with it = Name x.it}; id = x; mut = m; priv = p; exp = e} @@ at $sloc } | priv=private_opt s=shared_opt x=id fd=func_dec { let d = fd s x in - let e = DecE(d) @? d.at in + let e = DecE(d, ref Type.Pre) @? d.at in {name = {x with it = Name x.it}; id = x; mut = Const @@ no_region; priv; exp = e} @@ at $sloc } (* Patterns *) pat_nullary : | UNDERSCORE - { WildP @? at $sloc } + { WildP @! at $sloc } | x=id - { VarP(x) @? at $sloc } + { VarP(x) @! at $sloc } | l=lit - { LitP(ref l) @? at $sloc } + { LitP(ref l) @! at $sloc } | LPAR p=pat RPAR { p } | LPAR ps=seplist1(pat_bin, COMMA) RPAR - { TupP(ps) @? at $sloc } + { TupP(ps) @! at $sloc } pat_un : | p=pat_nullary { p } | QUEST p=pat_un - { OptP(p) @? at $sloc } + { OptP(p) @! at $sloc } | op=unop l=lit - { SignP(op, ref l) @? at $sloc } + { SignP(op, ref l) @! at $sloc } pat_bin : | p=pat_un { p } | p1=pat_bin OR p2=pat_bin - { AltP(p1, p2) @? at $sloc } + { AltP(p1, p2) @! at $sloc } | p=pat_bin COLON t=typ - { AnnotP(p, t) @? at $sloc } + { AnnotP(p, t) @! at $sloc } pat : | p=pat_bin @@ -533,7 +537,7 @@ dec_var : dec_nonvar : | s=shared_opt FUNC xf=id_opt fd=func_dec { (fd s (xf "func" $sloc)).it @? at $sloc } - | TYPE x=id tps=typ_params_opt EQ t=typ + | TYPE x=con_id tps=typ_params_opt EQ t=typ { TypD(x, tps, t) @? at $sloc } | s=obj_sort_opt CLASS xf=id_opt tps=typ_params_opt p=pat_nullary xefs=class_body { let x, efs = xefs in @@ -542,8 +546,9 @@ dec_nonvar : then efs else List.map share_expfield efs in - let tid = xf "class" $sloc in - ClassD(xf "class" $sloc, tid, tps, s, p, x, efs') @? at $sloc } + let id = xf "class" $sloc in + let con_id = id.it @= at $sloc in + ClassD(id, con_id, tps, s, p, x, efs') @? at $sloc } dec : | d=dec_var @@ -560,12 +565,12 @@ dec : then efs else List.map share_expfield efs in - let p = VarP(xf anon $sloc) @? at $sloc in + let p = VarP(xf anon $sloc) @! at $sloc in LetD(p, ObjE(s, xf anon $sloc, efs') @? at $sloc) @? at $sloc } func_dec : | tps=typ_params_opt p=pat_nullary rt=return_typ? fb=func_body - { let t = Lib.Option.get rt (TupT([]) @@ no_region) in + { let t = Lib.Option.get rt (TupT([]) @! no_region) in (* This is a hack to support local func declarations that return a computed async. These should be defined using RHS syntax EQ e to avoid the implicit AsyncE introduction around bodies declared as blocks *) diff --git a/src/pipeline.ml b/src/pipeline.ml index c28dd9990c1..fc36ed21435 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -286,12 +286,12 @@ let compile_with check mode name : compile_result = | Error msgs -> Error msgs | Ok ((prog, _t, scope), msgs) -> Diag.print_messages msgs; - let prelude = Desugar.prog initial_stat_env.Typing.con_env prelude in + let prelude = Desugar.prog prelude in let prog = await_lowering true prog name in let prog = async_lowering true prog name in let prog = tailcall_optimization true prog name in - let scope' = Typing.adjoin_scope initial_stat_env scope in - let prog = Desugar.prog scope'.Typing.con_env prog in + let prog = Desugar.prog prog in + ignore (Check_ir.check_prog initial_stat_env prog); phase "Compiling" name; let module_ = Compile.compile mode name prelude [prog] in Ok module_ diff --git a/src/rename.ml b/src/rename.ml index 4127dda9182..4b9038857f3 100644 --- a/src/rename.ml +++ b/src/rename.ml @@ -34,12 +34,12 @@ and exp' rho e = match e with | TupE es -> TupE (List.map (exp rho) es) | ProjE (e, i) -> ProjE (exp rho e, i) | ObjE (s, i, efs) -> ObjE (s, i, exp_fields rho efs) - | DotE (e, i) -> DotE (exp rho e, i) + | DotE (e, sr, i) -> DotE (exp rho e, ref (!sr), i) | AssignE (e1, e2) -> AssignE (exp rho e1, exp rho e2) | ArrayE (m, es) -> ArrayE (m, exps rho es) | IdxE (e1, e2) -> IdxE (exp rho e1, exp rho e2) | CallE (e1, ts, e2) -> CallE (exp rho e1, ts, exp rho e2) - | BlockE ds -> BlockE (decs rho ds) + | BlockE (ds, ot) -> BlockE (decs rho ds, ot) | NotE e -> NotE (exp rho e) | AndE (e1, e2) -> AndE (exp rho e1, exp rho e2) | OrE (e1, e2) -> OrE (exp rho e1, exp rho e2) @@ -59,8 +59,8 @@ and exp' rho e = match e with | AssertE e -> AssertE (exp rho e) | IsE (e, t) -> IsE (exp rho e, t) | AnnotE (e, t) -> AnnotE (exp rho e, t) - | DecE d -> let mk_d, rho' = dec rho d in - DecE ({mk_d with it = mk_d.it rho'}) + | DecE (d,ot) -> let mk_d, rho' = dec rho d in + DecE ({mk_d with it = mk_d.it rho'}, ref (!ot)) | OptE e -> OptE (exp rho e) | DeclareE (i, t, e) -> let i',rho' = id_bind rho i in DeclareE (i', t, exp rho' e) diff --git a/src/syntax.ml b/src/syntax.ml index 943e2ab65ac..2a57b3d08dc 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -4,15 +4,15 @@ type typ_note = {note_typ : Type.typ; note_eff : Type.eff} 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 (* Names (not alpha-convertible), used for field and class names *) type name = name' Source.phrase -and name' = Name of string -let string_of_name (Name s ) = s +and name' = Name of string +let string_of_name (Name s ) = s (* Types *) @@ -24,7 +24,7 @@ type func_sort = Type.func_sort Source.phrase type mut = mut' Source.phrase and mut' = Const | Var -type typ = typ' Source.phrase +type typ = (typ',Type.typ) Source.annotated_phrase and typ' = | PrimT of string (* primitive *) | VarT of id * typ list (* constructor *) @@ -44,7 +44,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 ref) Source.annotated_phrase +and typ_bind = (typ_bind', Type.typ) Source.annotated_phrase and typ_bind' = {var : id; bound : typ} @@ -99,7 +99,7 @@ type relop = (* Patterns *) -type pat = (pat', typ_note) Source.annotated_phrase +type pat = (pat', Type.typ) Source.annotated_phrase and pat' = | WildP (* wildcard *) | VarP of id (* variable *) @@ -123,10 +123,7 @@ and pat_field' = {id : id; pat : pat} type priv = priv' Source.phrase and priv' = Public | Private -(* type instantiations *) -type inst = (typ, Type.typ ref) Source.annotated_phrase - -(* Filled in for overloaded operators during type checking. Initially Type.Pre. *) +(* Filled in for overloaded operators and blocks during type checking. Initially Type.Pre. *) type op_type = Type.typ ref type exp = (exp', typ_note) Source.annotated_phrase @@ -141,12 +138,12 @@ and exp' = | ProjE of exp * int (* tuple projection *) | OptE of exp (* option injection *) | ObjE of obj_sort * id * exp_field list (* object *) - | DotE of exp * name (* object projection *) + | DotE of exp * Type.obj_sort ref * name (* object projection *) | AssignE of exp * exp (* assignment *) | ArrayE of mut * exp list (* array *) | IdxE of exp * exp (* array indexing *) - | CallE of exp * inst list * exp (* function call *) - | BlockE of dec list (* block *) + | CallE of exp * typ list * exp (* function call *) + | BlockE of dec list * op_type (* block (with type after avoidance)*) | NotE of exp (* negation *) | AndE of exp * exp (* conjunction *) | OrE of exp * exp (* disjunction *) @@ -163,7 +160,7 @@ and exp' = | AssertE of exp (* assertion *) | IsE of exp * exp (* instance-of *) | AnnotE of exp * typ (* type annotation *) - | DecE of dec (* declaration *) + | DecE of dec * Type.typ ref (* declaration *) | DeclareE of id * Type.typ * exp (* local promise (internal) *) | DefineE of id * mut * exp (* promise fulfillment (internal) *) | NewObjE of obj_sort * (name * id) list (* make an object, preserving mutable identity (internal) *) @@ -185,12 +182,14 @@ and case' = {pat : pat; exp : exp} and dec = (dec', typ_note) Source.annotated_phrase and dec' = - | ExpD of exp (* plain expression *) - | LetD of pat * exp (* immutable *) - | VarD of id * exp (* mutable *) - | FuncD of sharing * id * typ_bind list * pat * typ * exp (* function *) - | TypD of id * typ_bind list * typ (* type *) - | ClassD of id (*term id*) * id (*type id*) * typ_bind list * obj_sort * pat * id * exp_field list (* class *) + | ExpD of exp (* plain expression *) + | LetD of pat * exp (* immutable *) + | VarD of id * exp (* mutable *) + | FuncD of (* function *) + sharing * id * typ_bind list * pat * typ * exp + | TypD of con_id * typ_bind list * typ (* type *) + | ClassD of (* class *) + id * con_id * typ_bind list * obj_sort * pat * id * exp_field list (* Program *) @@ -201,14 +200,16 @@ and prog' = dec list (* n-ary arguments/result sequences *) - let seqT ts = match ts with | [t] -> t - | ts -> {Source.it = TupT ts; at = Source.no_region; Source.note = ()} + | ts -> + {Source.it = TupT ts; + at = Source.no_region; + Source.note = Type.Tup (List.map (fun t -> t.Source.note) ts)} let as_seqT t = match t.Source.it with | TupT ts -> ts | _ -> [t] - + diff --git a/src/syntaxops.ml b/src/syntaxops.ml index 0f50b675592..91f3df0400c 100644 --- a/src/syntaxops.ml +++ b/src/syntaxops.ml @@ -51,11 +51,15 @@ let fresh_id typ = (* Patterns *) -let varP x = {x with it=VarP (id_of_exp x)} +let varP x = + { it=VarP (id_of_exp x); + at = x.at; + note = x.note.note_typ + } + let tupP pats = {it = TupP pats; - note = {note_typ = T.Tup (List.map typ pats); - note_eff = T.Triv}; + note = T.Tup (List.map (fun p -> p.note) pats); at = no_region} let seqP ps = @@ -89,7 +93,7 @@ let projE e n = } | _ -> failwith "projE" -let decE exp = {exp with it = DecE exp} +let decE dec = {dec with it = DecE (dec,ref dec.note.note_typ)} let rec typ_decs decs = match decs with @@ -101,7 +105,7 @@ let blockE decs = let es = List.map eff decs in let typ = typ_decs decs in let e = List.fold_left max_eff Type.Triv es in - { it = BlockE decs; + { it = BlockE (decs, ref typ); at = no_region; note = {note_typ = typ; note_eff = e} @@ -145,7 +149,7 @@ let ifE exp1 exp2 exp3 typ = } let dotE exp name typ = - { it = DotE (exp,name); + { it = DotE (exp,ref (T.Object T.Local), name); at = no_region; note = {note_typ = typ; note_eff = eff exp} @@ -155,15 +159,13 @@ let switch_optE exp1 exp2 pat exp3 typ = { it = SwitchE (exp1, [{it = {pat = {it = LitP (ref NullLit); at = no_region; - note = {note_typ = exp1.note.note_typ; - note_eff = T.Triv}}; + note = exp1.note.note_typ}; exp = exp2}; at = no_region; note = ()}; {it = {pat = {it = OptP pat; at = no_region; - note = {note_typ = exp1.note.note_typ; - note_eff = T.Triv}}; + note = exp1.note.note_typ}; exp = exp3}; at = no_region; note = ()}] @@ -214,7 +216,7 @@ let loopE exp1 exp2Opt = (match exp2Opt with | Some exp2 -> eff exp2 | None -> Type.Triv); - note_typ = Type.unit} + note_typ = Type.Non} } @@ -266,20 +268,20 @@ let expD exp = { exp with it = ExpD exp} let letE x exp1 exp2 = blockE [letD x exp1; expD exp2] -(* Mono-morphic function declaration *) +(* Mono-morphic function declaration, sharing inferred from f's type *) let funcD f x e = match f.it,x.it with | VarE _, VarE _ -> - let note = {note_typ = T.Func(T.Call T.Local, T.Returns, [], T.as_seq (typ x), T.as_seq (typ e)); - note_eff = T.Triv} in - assert (f.note = note); - {it=FuncD(T.Local @@ no_region, (id_of_exp f), + let sharing,t1,t2 = match f.note.note_typ with + | T.Func(T.Call sharing, _, _, ts1, ts2) -> sharing,T.seq ts1, T.seq ts2 + | _ -> assert false in + {it=FuncD(sharing @@ no_region, (id_of_exp f), [], - {it=VarP (id_of_exp x);at=no_region;note=x.note}, - PrimT "Any"@@no_region, (* bogus, but we shouldn't use it anymore *) + {it = VarP (id_of_exp x); at = no_region; note = t1}, + {it = PrimT "Any"; at = no_region; note = t2}, (* bogus, but we shouldn't use it anymore *) e); at = no_region; - note;} + note = f.note} | _ -> failwith "Impossible: funcD" @@ -287,15 +289,16 @@ let funcD f x e = let nary_funcD f xs e = match f.it,f.note.note_typ with | VarE _, - T.Func(T.Call sharing,_,_,_,_) -> + T.Func(T.Call sharing,_,_,_,ts2) -> + let t2 = T.seq ts2 in {it=FuncD(sharing @@ no_region, id_of_exp f, [], seqP (List.map varP xs), - PrimT "Any"@@no_region, (* bogus, but we shouldn't use it anymore *) + {it = PrimT "Any"; at = no_region; note = t2}, (* bogus, but we shouldn't use it anymore *) e); at = no_region; - note = f.note;} + note = f.note} | _,_ -> failwith "Impossible: funcD" diff --git a/src/syntaxops.mli b/src/syntaxops.mli index 96c9e16a1ac..6a920ce4078 100644 --- a/src/syntaxops.mli +++ b/src/syntaxops.mli @@ -49,7 +49,7 @@ val letE : var -> exp -> exp -> exp val unitE : exp val boolE : bool -> exp -val callE : exp -> Syntax.inst list -> exp -> typ -> exp +val callE : exp -> Syntax.typ list -> exp -> typ -> exp val ifE : exp -> exp -> exp -> typ -> exp val dotE : exp -> name -> typ -> exp diff --git a/src/tailcall.ml b/src/tailcall.ml index fe150feec4d..b76971c38de 100644 --- a/src/tailcall.ml +++ b/src/tailcall.ml @@ -64,10 +64,10 @@ let bind env i info = let are_generic_insts tbs insts = List.for_all2 (fun tb inst -> - match !(tb.note),!(inst.note) with - | Some c1, Con(c2,[]) -> c1 = c2 (* conservative, but safe *) - | Some c1, _ -> false - | None,_ -> assert false) tbs insts + match tb.note,inst.note with + | Con(c1,[]), Con(c2,[]) -> c1 = c2 (* conservative, but safe *) + | Con(c1,[]), _ -> false + | _,_ -> assert false) tbs insts let rec tailexp env e = {e with it = exp' env e} @@ -85,7 +85,7 @@ and exp' env e = match e.it with | TupE es -> TupE (List.map (exp env) es) | ProjE (e, i) -> ProjE (exp env e, i) | ObjE (s, i, efs) -> ObjE (s, i, exp_fields env efs) - | DotE (e, i) -> DotE (exp env e, i) + | DotE (e, sr, i) -> DotE (exp env e, ref (!sr), i) | AssignE (e1, e2) -> AssignE (exp env e1, exp env e2) | ArrayE (m,es) -> ArrayE (m,(exps env es)) | IdxE (e1, e2) -> IdxE (exp env e1, exp env e2) @@ -100,7 +100,7 @@ and exp' env e = match e.it with expD (breakE label (tupE []) (typ e))]).it | _,_-> CallE(exp env e1, insts, exp env e2) end - | BlockE ds -> BlockE (decs env ds) + | BlockE (ds,ot) -> BlockE (decs env ds, ref (!ot)) | NotE e -> NotE (exp env e) | AndE (e1, e2) -> AndE (exp env e1, tailexp env e2) | OrE (e1, e2) -> OrE (exp env e1, tailexp env e2) @@ -121,8 +121,8 @@ and exp' env e = match e.it with | AssertE e -> AssertE (exp env e) | IsE (e, t) -> IsE (exp env e, t) | AnnotE (e, t) -> AnnotE (exp env e, t) - | DecE d -> let mk_d, env1 = dec env d in - DecE ({mk_d with it = mk_d.it env1}) + | DecE (d, ot) -> let mk_d, env1 = dec env d in + DecE ({mk_d with it = mk_d.it env1},ref (!ot)) | OptE e -> OptE (exp env e) | DeclareE (i, t, e) -> let env1 = bind env i None in DeclareE (i, t, tailexp env1 e) @@ -206,7 +206,7 @@ and dec' env d = | FuncD (({it=Local;_} as s), id, tbs, p, typT, exp0) -> let env = bind env id None in (fun env1 -> - let temp = fresh_id (Mut (typ p)) in + let temp = fresh_id (Mut p.note) in let l = fresh_lab () in let tail_called = ref false in let env2 = {tail_pos = true; @@ -218,18 +218,22 @@ and dec' env d = in let env3 = pat env2 p in (* shadow id if necessary *) let exp0' = tailexp env3 exp0 in + let cs = List.map (fun tb -> tb.note) tbs in if !tail_called then let ids = match typ d with - | Func(_,_,_,dom,_) -> List.map fresh_id dom + | Func(_,_,_,dom,_) -> List.map (fun t -> fresh_id (open_ cs t)) dom | _ -> assert false in let args = seqP (List.map varP ids) in + let l_typ = + {it = Syntax.TupT []; at = no_region; note = Type.unit} + in let body = blockE [ varD (id_of_exp temp) (seqE ids); expD (loopE - (labelE l typT + (labelE l l_typ (blockE [letP p temp; - expD (retE exp0' unit)])) None) + expD (retE exp0' Type.unit)])) None) ] in FuncD (s, id, tbs, args, typT, body) else diff --git a/src/type.ml b/src/type.ml index 27d7f9f5b20..227dcf01971 100644 --- a/src/type.ml +++ b/src/type.ml @@ -43,6 +43,10 @@ and typ = and bind = {var : string; bound : typ} and field = {name : string; typ : typ} +(* field ordering *) + +let compare_field {name=n;_} {name=m;_} = compare n m + type kind = | Def of bind list * typ | Abs of bind list * typ @@ -57,7 +61,7 @@ let seq ts = let as_seq t = match t with | Tup ts -> ts - | t -> [t] + | t -> [t] (* Short-hands *) @@ -94,8 +98,8 @@ let array_obj t = let mut t = immut t @ [ {name = "set"; typ = Func (Call Local, Returns, [], [Prim Nat; t], [])} ] in match t with - | Mut t' -> Obj (Object Local, List.sort compare (mut t')) - | t -> Obj (Object Local, List.sort compare (immut t)) + | Mut t' -> Obj (Object Local, List.sort compare_field (mut t')) + | t -> Obj (Object Local, List.sort compare_field (immut t)) (* Shifting *) @@ -389,7 +393,7 @@ let rec rel_typ env rel eq t1 t2 = t1 == t2 || S.mem (t1, t2) !rel || begin rel := S.add (t1, t2) !rel; match t1, t2 with - | Any, Any -> + | Any, Any -> true | _, Any when rel != eq -> true @@ -453,8 +457,8 @@ let rec rel_typ env rel eq t1 t2 = rel_list rel_typ env rel eq ts1 (List.map (fun _ -> Shared) ts1) | Func (s1, c1, tbs1, t11, t12), Func (s2, c2, tbs2, t21, t22) -> (* TODO: not all classes should be sharable *) - c1 = c2 && - (s1 = s2 || rel != eq && s1 = Construct) && + c1 = c2 && + (s1 = s2 || rel != eq && s1 = Construct) && (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) && @@ -491,7 +495,7 @@ and rel_fields env rel eq tfs1 tfs2 = | _, [] when rel != eq -> true | tf1::tfs1', tf2::tfs2' -> - (match compare tf1.name tf2.name with + (match compare_field tf1 tf2 with | 0 -> rel_typ env rel eq tf1.typ tf2.typ && rel_fields env rel eq tfs1' tfs2' @@ -599,7 +603,7 @@ let rec string_of_typ_nullary vs = function | Shared -> "Shared" | Class -> "Class" | Prim p -> string_of_prim p - | Var (s, i) -> string_of_var (List.nth vs i) + | Var (s, i) -> (try string_of_var (List.nth vs i) with _ -> assert false) | Con (c, []) -> string_of_con vs c | Con (c, ts) -> sprintf "%s<%s>" (string_of_con vs c) @@ -622,25 +626,25 @@ and string_of_dom vs ts = | [Tup _] -> sprintf "(%s)" dom | _ -> dom - + and string_of_cod c vs ts = let cod = string_of_typ' vs (seq ts) in match ts with | [Tup _] -> sprintf "(%s)" cod - | [Async _] -> + | [Async _] -> (match c with | Returns -> sprintf "(%s)" cod | Promises -> sprintf "%s" cod ) | _ -> cod - + and string_of_typ' vs t = match t with | Func (s, c, [], ts1, ts2) -> sprintf "%s%s -> %s" (string_of_func_sort s) - (string_of_dom vs ts1) - (string_of_cod c vs ts2) + (string_of_dom vs ts1) + (string_of_cod c vs ts2) | Func (s, c, tbs, ts1, ts2) -> let vs' = names_of_binds vs tbs in sprintf "%s%s%s -> %s" @@ -712,4 +716,4 @@ let rec string_of_typ_expand env t = (* Environments *) -module Env = Env.Make(String) +module Env = Env.Make(String) diff --git a/src/type.mli b/src/type.mli index b57608b1051..4fea582590d 100644 --- a/src/type.mli +++ b/src/type.mli @@ -43,6 +43,10 @@ and typ = and bind = {var : string; bound : typ} and field = {name : string; typ : typ} +(* field ordering *) + +val compare_field : field -> field -> int + type kind = | Def of bind list * typ | Abs of bind list * typ @@ -50,7 +54,7 @@ type kind = type con_env = kind Con.Env.t (* n-ary argument/result sequences *) - + val seq: typ list -> typ val as_seq : typ -> typ list diff --git a/src/typing.ml b/src/typing.ml index 212d92990c3..f4ff1607f62 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -133,6 +133,11 @@ let infer_mut mut : T.typ -> T.typ = | Var -> fun t -> T.Mut t let rec check_typ env typ : T.typ = + let t = check_typ' env typ in + typ.note <- t; + t + +and check_typ' env typ : T.typ = match typ.it with | VarT (id, typs) -> (match T.Env.find_opt id.it env.typs with @@ -194,7 +199,7 @@ let rec check_typ env typ : T.typ = | ObjT (sort, fields) -> check_ids env (List.map (fun (field : typ_field) -> field.it.id) fields); let fs = List.map (check_typ_field env sort.it) fields in - T.Obj (sort.it, List.sort compare fs) + T.Obj (sort.it, List.sort T.compare_field fs) | ParT typ -> check_typ env typ @@ -212,7 +217,7 @@ and check_typ_field env s typ_field : T.field = and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env = let xs = List.map (fun typ_bind -> typ_bind.it.var.it) typ_binds in let cs = List.map (fun x -> Con.fresh x) xs in - List.iter2 (fun typ_bind c -> typ_bind.note := Some c) typ_binds cs; + List.iter2 (fun typ_bind c -> typ_bind.note <- T.Con(c,[])) typ_binds cs; let te = List.fold_left2 (fun te typ_bind c -> let id = typ_bind.it.var in if T.Env.mem id.it te then @@ -243,10 +248,8 @@ and check_typ_bounds env (tbs : T.bind list) typs at : T.typ list = | [], _ -> local_error env at "too many type arguments"; [] | _, [] -> error env at "too few type arguments" -and check_inst_bounds env tbs (insts:inst list) at = - let typs = List.map (fun inst -> inst.it) insts in +and check_inst_bounds env tbs typs at = let tys = check_typ_bounds env tbs typs at in - List.iter2 (fun inst ty -> inst.note := ty) insts tys; tys (* Literals *) @@ -305,7 +308,7 @@ let check_lit env t lit at = lit := Word32Lit (check_word32 env at s) | T.Prim T.Word64, PreLit (s, (T.Nat | T.Int)) -> lit := Word64Lit (check_word64 env at s) - | T.Prim T.Float, PreLit (s, (T.Nat | T.Int | T.Float)) -> + | T.Prim T.Float, PreLit (s, (T.Nat | T.Int | T.Float)) -> lit := FloatLit (check_float env at s) | t, _ -> let t' = T.Prim (infer_lit env lit at) in @@ -322,7 +325,10 @@ let isAsyncE exp = | _ -> false let rec infer_exp env exp : T.typ = - T.as_immut (infer_exp_mut env exp) + let t = T.as_immut (infer_exp_mut env exp) in + if not env.pre then + exp.note <- {exp.note with note_typ = T.as_immut exp.note.note_typ}; + t and infer_exp_promote env exp : T.typ = let t = infer_exp env exp in @@ -415,10 +421,11 @@ and infer_exp' env exp : T.typ = | ObjE (sort, id, fields) -> let env' = if sort.it = T.Actor then { env with async = false } else env in infer_obj env' sort.it id fields - | DotE (exp1, {it = Name n;_}) -> + | DotE (exp1, sr, {it = Name n;_}) -> let t1 = infer_exp_promote env exp1 in (try - let _, tfs = T.as_obj_sub n env.cons t1 in + let s, tfs = T.as_obj_sub n env.cons t1 in + sr := s; match List.find_opt (fun {T.name; _} -> name = n) tfs with | Some {T.typ = t; _} -> t | None -> @@ -468,13 +475,15 @@ and infer_exp' env exp : T.typ = error env exp1.at "expected function type, but expression produces type\n %s" (T.string_of_typ_expand env.cons t1) ) - | BlockE decs -> + | BlockE (decs,ot) -> let t, scope = infer_block env decs exp.at in - (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) - ) + 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) + in + ot := t'; + t' | NotE exp1 -> if not env.pre then check_exp env T.bool exp1; T.bool @@ -599,12 +608,15 @@ and infer_exp' env exp : T.typ = let t = check_typ env typ in if not env.pre then check_exp env t exp1; t - | DecE dec -> + | DecE (dec,ot) -> let t, scope = infer_block env [dec] exp.at in - (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) - ) + 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) + in + ot := t'; + t' (* DeclareE and DefineE should not occur in source code *) | DeclareE (id, typ, exp1) -> let env' = adjoin_vals env (T.Env.singleton id.it typ) in @@ -667,8 +679,9 @@ and check_exp' env t exp = | AsyncE exp1, T.Async t' -> let env' = {env with labs = T.Env.empty; rets = Some t'; async = true} in check_exp env' t' exp1 - | BlockE decs, _ -> - ignore (check_block env t decs exp.at) + | BlockE (decs, ot),_ -> + ignore (check_block env t decs exp.at); + ot := t | IfE (exp1, exp2, exp3), _ -> check_exp env T.bool exp1; check_exp env t exp2; @@ -743,10 +756,10 @@ and infer_pat_exhaustive env pat : T.typ * val_env = t, ve and infer_pat env pat : T.typ * val_env = - assert (pat.note.note_typ = T.Pre); + assert (pat.note = T.Pre); let t, ve = infer_pat' env pat in if not env.pre then - pat.note <- {note_typ = T.normalize env.cons t; note_eff = T.Triv}; + pat.note <- T.normalize env.cons t; t, ve and infer_pat' env pat : T.typ * val_env = @@ -799,11 +812,11 @@ and check_pat_exhaustive env t pat : val_env = ve and check_pat env t pat : val_env = - assert (pat.note.note_typ = T.Pre); + 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 ve = check_pat' env t pat in - if not env.pre then pat.note <- {note_typ = t'; note_eff = T.Triv}; + if not env.pre then pat.note <- t'; ve and check_pat' env t pat : val_env = @@ -918,11 +931,11 @@ and infer_exp_fields env s id t fields : T.field list * val_env = let env' = add_val env id t in let tfs, ve = List.fold_left (infer_exp_field env' s) ([], T.Env.empty) fields in - List.sort compare tfs, ve + List.sort T.compare_field tfs, ve and is_func_exp exp = match exp.it with - | DecE dec -> is_func_dec dec + | DecE (dec, _) -> is_func_dec dec | AnnotE (exp, _) -> is_func_exp exp | _ -> Printf.printf "[1]%!"; false @@ -988,10 +1001,10 @@ and infer_dec env dec : T.typ = | LetD (_, exp) | VarD (_, exp) -> if not env.pre then ignore (infer_exp env exp); T.unit - | FuncD (sort, id, typbinds, pat, typ, exp) -> + | 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 typbinds in + let _cs, _ts, te, ce = check_typ_binds env typ_binds in let env' = adjoin_typs env te ce in let _, ve = infer_pat_exhaustive env' pat in let t2 = check_typ env' typ in @@ -1000,10 +1013,10 @@ and infer_dec env dec : T.typ = check_exp (adjoin_vals env'' ve) t2 exp end; t - | ClassD (id, tid, typbinds, sort, pat, id', fields) -> + | ClassD (id, tid, typ_binds, sort, pat, 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 typbinds in + let _cs, _ts, te, ce = check_typ_binds env typ_binds in let env' = adjoin_typs env te ce in let _, ve = infer_pat_exhaustive env' pat in let env'' = @@ -1142,7 +1155,9 @@ and infer_dec_typdecs env dec : con_env = 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 - Con.Env.singleton c (T.Def (tbs, T.close cs t)) + let k = T.Def (tbs, T.close cs t) in + id.note <- Some (c,k); + Con.Env.singleton c k | ClassD (conid, id, binds, sort, pat, id', fields) -> let c = T.Env.find id.it env.typs in let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in @@ -1150,6 +1165,8 @@ and infer_dec_typdecs env dec : con_env = let _, ve = infer_pat env' pat in let t = infer_obj (adjoin_vals env' ve) sort.it id' fields in let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in + let k = T.Abs (tbs, T.close cs t) in + id.note <- Some (c,k); Con.Env.singleton c (T.Abs (tbs, T.close cs t)) @@ -1189,8 +1206,8 @@ and infer_dec_valdecs env dec : val_env = | VarD (id, exp) -> let t = infer_exp {env with pre = true} exp in T.Env.singleton id.it (T.Mut t) - | FuncD (sort, id, typbinds, pat, typ, exp) -> - let cs, ts, te, ce = check_typ_binds env typbinds in + | 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 t1, _ = infer_pat {env' with pre = true} pat in let t2 = check_typ env' typ in @@ -1218,7 +1235,6 @@ and infer_dec_valdecs env dec : val_env = | TupT _ -> T.as_seq t2 | _ -> [t2] in - let c = match sort.it, typ.it with | T.Sharable, (AsyncT _) -> T.Promises (* TBR: do we want this for T.Local too? *) | _ -> T.Returns @@ -1228,8 +1244,8 @@ and infer_dec_valdecs env dec : val_env = (T.Func (T.Call sort.it, c, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2)) | TypD _ -> T.Env.empty - | ClassD (conid, id, typbinds, sort, pat, id', fields) -> - let cs, ts, te, ce = check_typ_binds env typbinds in + | ClassD (conid, id, typ_binds, sort, pat, id', fields) -> + let cs, ts, te, ce = check_typ_binds env typ_binds in let env' = adjoin_typs env te ce in let c = T.Env.find id.it env.typs in let t1, _ = infer_pat {env' with pre = true} pat in diff --git a/src/value.ml b/src/value.ml index eff4e4c98f3..8d9f4f5859c 100644 --- a/src/value.ml +++ b/src/value.ml @@ -201,7 +201,7 @@ let call_conv_of_typ typ = match typ with | Type.Func(sort, control, tbds, dom, res) -> { sort; control; n_args = List.length dom; n_res = List.length res } - | _ -> raise (Invalid_argument "call_conv_of_typ") + | _ -> raise (Invalid_argument ("call_conv_of_typ"^T.string_of_typ typ)) type func = (value -> value cont -> unit) diff --git a/test/run-dfinity/ok/counter-class.wasm.stderr.ok b/test/run-dfinity/ok/counter-class.wasm.stderr.ok index 4a8a2f469a6..04999878853 100644 --- a/test/run-dfinity/ok/counter-class.wasm.stderr.ok +++ b/test/run-dfinity/ok/counter-class.wasm.stderr.ok @@ -8,12 +8,14 @@ non-closed actor: (ActorE (shared 0 -> 0) dec (TupP) - (TupT) + () (BlockE (ExpD (CallE ( 1 -> 0) (VarE show) (VarE c))) (ExpD (AssignE (VarE c) (BinE Int (VarE c) SubOp (LitE (IntLit 1))))) + () ) ) + shared () -> () ) Const Public @@ -25,7 +27,7 @@ non-closed actor: (ActorE (shared 1 -> 0) read (VarP $1) - (TupT) + () (BlockE (LetD (TupP) (TupE)) (ExpD @@ -36,25 +38,30 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $0) - (PrimT Any) - (CallE ( 1 -> 0) (VarE $0) (BlockE (ExpD (VarE c)))) + () + (CallE ( 1 -> 0) (VarE $0) (BlockE (ExpD (VarE c)) Int)) ) + (Int -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $2) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $1) (VarE $2)) ) + Int -> () ) ) ) + () ) ) + shared (shared Int -> ()) -> () ) Const Public ) + Counter ) diff --git a/test/run/ok/account.wasm.stderr.ok b/test/run/ok/account.wasm.stderr.ok index f1b111c40ed..a89c7973bc2 100644 --- a/test/run/ok/account.wasm.stderr.ok +++ b/test/run/ok/account.wasm.stderr.ok @@ -8,7 +8,7 @@ non-closed actor: (ActorE (shared 1 -> 0) getBalance (VarP $8) - (TupT) + () (BlockE (LetD (TupP) (TupE)) (ExpD @@ -19,29 +19,34 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $0) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $0) (BlockE (ExpD (RetE (CallE ( 1 -> 0) (VarE $0) (VarE balance)))) + Int ) ) ) + (Int -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $9) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $8) (VarE $9)) ) + Int -> () ) ) ) + () ) ) + shared (shared Int -> ()) -> () ) Const Public @@ -53,7 +58,7 @@ non-closed actor: (ActorE (shared 2 -> 0) split (TupP (VarP amount) (VarP $10)) - (TupT) + () (BlockE (ExpD (CallE @@ -63,7 +68,7 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $1) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $1) @@ -83,23 +88,28 @@ non-closed actor: (ActorE ) ) ) + Account ) ) ) + (Account -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $11) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $10) (VarE $11)) ) + Account -> () ) ) ) + () ) ) + shared (Int, shared Account -> ()) -> () ) Const Public @@ -111,7 +121,7 @@ non-closed actor: (ActorE (shared 1 -> 0) join (VarP account) - (TupT) + () (BlockE (ExpD (AssertE (IsE (VarE account) (VarE Account)))) (LetD (VarP amount) (VarE balance)) @@ -123,8 +133,10 @@ non-closed actor: (ActorE (TupE (VarE amount) (VarE Account)) ) ) + () ) ) + shared (like Account) -> () ) Const Public @@ -136,7 +148,7 @@ non-closed actor: (ActorE (shared 2 -> 0) credit (TupP (VarP amount) (VarP caller)) - (TupT) + () (BlockE (ExpD (AssertE (IsE (VarE this) (VarE caller)))) (ExpD @@ -145,8 +157,10 @@ non-closed actor: (ActorE (BinE Int (VarE balance) AddOp (VarE amount)) ) ) + () ) ) + shared (Int, Class) -> () ) Const Public @@ -158,7 +172,7 @@ non-closed actor: (ActorE (shared 2 -> 0) isCompatible (TupP (VarP account) (VarP $12)) - (TupT) + () (BlockE (ExpD (CallE @@ -168,7 +182,7 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $2) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $2) @@ -182,25 +196,31 @@ non-closed actor: (ActorE ) ) ) + Bool ) ) ) + (Bool -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $13) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $12) (VarE $13)) ) + Bool -> () ) ) ) + () ) ) + shared (like Account, shared Bool -> ()) -> () ) Const Public ) + Account ) diff --git a/test/run/ok/bank-example.wasm.stderr.ok b/test/run/ok/bank-example.wasm.stderr.ok index 45a674ee096..9279fc5c297 100644 --- a/test/run/ok/bank-example.wasm.stderr.ok +++ b/test/run/ok/bank-example.wasm.stderr.ok @@ -14,7 +14,7 @@ non-closed actor: (ActorE (shared 1 -> 0) getIssuer (VarP $32) - (TupT) + () (BlockE (LetD (TupP) (TupE)) (ExpD @@ -25,29 +25,34 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $0) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $0) (BlockE (ExpD (RetE (CallE ( 1 -> 0) (VarE $0) (VarE issuer)))) + Issuer ) ) ) + (Issuer -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $33) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $32) (VarE $33)) ) + Issuer -> () ) ) ) + () ) ) + shared (shared Issuer -> ()) -> () ) Const Public @@ -59,7 +64,7 @@ non-closed actor: (ActorE (shared 1 -> 0) getReserve (VarP $34) - (TupT) + () (BlockE (LetD (TupP) (TupE)) (ExpD @@ -70,33 +75,39 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $1) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $1) (BlockE (ExpD (RetE (CallE ( 1 -> 0) (VarE $1) (VarE reserve)))) + Account ) ) ) + (Account -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $35) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $34) (VarE $35)) ) + Account -> () ) ) ) + () ) ) + shared (shared Account -> ()) -> () ) Const Public ) + Bank ) non-closed actor: (ActorE self @@ -108,7 +119,7 @@ non-closed actor: (ActorE (shared 1 -> 0) getBalance (VarP $38) - (TupT) + () (BlockE (LetD (TupP) (TupE)) (ExpD @@ -119,29 +130,34 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $3) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $3) (BlockE (ExpD (RetE (CallE ( 1 -> 0) (VarE $3) (VarE balance)))) + Int ) ) ) + (Int -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $39) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $38) (VarE $39)) ) + Int -> () ) ) ) + () ) ) + shared (shared Int -> ()) -> () ) Const Public @@ -153,7 +169,7 @@ non-closed actor: (ActorE (shared 2 -> 0) split (TupP (VarP amount) (VarP $40)) - (TupT) + () (BlockE (ExpD (CallE @@ -163,7 +179,7 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $4) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $4) @@ -183,23 +199,28 @@ non-closed actor: (ActorE ) ) ) + Account ) ) ) + (Account -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $41) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $40) (VarE $41)) ) + Account -> () ) ) ) + () ) ) + shared (Int, shared Account -> ()) -> () ) Const Public @@ -211,7 +232,7 @@ non-closed actor: (ActorE (shared 1 -> 0) join (VarP account) - (TupT) + () (BlockE (ExpD (AssertE (IsE (VarE account) (VarE Account)))) (LetD (VarP amount) (VarE balance)) @@ -223,8 +244,10 @@ non-closed actor: (ActorE (TupE (VarE amount) (VarE Account)) ) ) + () ) ) + shared (like Account) -> () ) Const Public @@ -236,7 +259,7 @@ non-closed actor: (ActorE (shared 2 -> 0) credit (TupP (VarP amount) (VarP caller)) - (TupT) + () (BlockE (ExpD (AssertE (IsE (VarE self) (VarE caller)))) (ExpD @@ -245,8 +268,10 @@ non-closed actor: (ActorE (BinE Int (VarE balance) AddOp (VarE amount)) ) ) + () ) ) + shared (Int, Class) -> () ) Const Public @@ -258,7 +283,7 @@ non-closed actor: (ActorE (shared 2 -> 0) isCompatible (TupP (VarP account) (VarP $42)) - (TupT) + () (BlockE (ExpD (CallE @@ -268,7 +293,7 @@ non-closed actor: (ActorE ( 1 -> 0) $lambda (VarP $5) - (PrimT Any) + () (CallE ( 1 -> 0) (VarE $5) @@ -282,25 +307,31 @@ non-closed actor: (ActorE ) ) ) + Bool ) ) ) + (Bool -> ()) -> () ) (BlockE (FuncD ( 1 -> 0) $lambda (VarP $43) - (PrimT Any) + () (CallE (shared 1 -> 0) (VarE $42) (VarE $43)) ) + Bool -> () ) ) ) + () ) ) + shared (like Account, shared Bool -> ()) -> () ) Const Public ) + Account )