diff --git a/src/arrange.ml b/src/arrange.ml index d91a394d7b7..fef1d1d0fd8 100644 --- a/src/arrange.ml +++ b/src/arrange.ml @@ -56,6 +56,7 @@ and pat p = match p.it with | WildP -> Atom "WildP" | VarP x -> "VarP" $$ [id x] | TupP ps -> "TupP" $$ List.map pat ps + | ObjP ps -> "ObjP" $$ List.map pat_field ps | AnnotP (p, t) -> "AnnotP" $$ [pat p; typ t] | LitP l -> "LitP" $$ [lit !l] | SignP (uo, l) -> "SignP" $$ [unop uo ; lit !l] @@ -110,6 +111,8 @@ and relop ro = match ro with and case c = "case" $$ [pat c.it.pat; exp c.it.exp] +and pat_field pf = pf.it.id.it $$ [pat pf.it.pat] + and prim p = Atom (Type.string_of_prim p) and sharing sh = match sh with diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml index 3e883aaecb5..a2e4505d441 100644 --- a/src/arrange_ir.ml +++ b/src/arrange_ir.ml @@ -42,7 +42,7 @@ let rec exp e = match e.it with | ActorE (i, ds, fs, t) -> "ActorE" $$ [id i] @ List.map dec ds @ fields fs @ [typ t] | NewObjE (s, fs, t) -> "NewObjE" $$ (Arrange.obj_sort' s :: fields fs @ [typ t]) -and fields fs = List.fold_left (fun flds f -> (name f.it.name $$ [ id f.it.var ]):: flds) [] fs +and fields fs = List.fold_left (fun flds (f : field) -> (name f.it.name $$ [ id f.it.var ]):: flds) [] fs and args = function | [] -> [] @@ -54,11 +54,14 @@ and pat p = match p.it with | WildP -> Atom "WildP" | VarP i -> "VarP" $$ [ id i ] | TupP ps -> "TupP" $$ List.map pat ps + | ObjP pfs -> "ObjP" $$ List.map pat_field pfs | LitP l -> "LitP" $$ [ Arrange.lit l ] | OptP p -> "OptP" $$ [ pat p ] | VariantP (i, p) -> "VariantP" $$ [ id i; pat p ] | AltP (p1,p2) -> "AltP" $$ [ pat p1; pat p2 ] +and pat_field pf = name pf.it.name $$ [pat pf.it.pat] + and case c = "case" $$ [pat c.it.pat; exp c.it.exp] and name n = match n.it with diff --git a/src/async.ml b/src/async.ml index 0b179293941..82adff0b8e2 100644 --- a/src/async.ml +++ b/src/async.ml @@ -380,6 +380,8 @@ module Transform() = struct pat | TupP pats -> TupP (List.map t_pat pats) + | ObjP pfs -> + ObjP (map_obj_pat t_pat pfs) | OptP pat1 -> OptP (t_pat pat1) | VariantP (i, pat1) -> diff --git a/src/await.ml b/src/await.ml index 4246bd4ff6a..5a52cbd31db 100644 --- a/src/await.ml +++ b/src/await.ml @@ -405,6 +405,7 @@ and declare_pat pat exp : exp = | WildP | LitP _ -> exp | VarP id -> declare_id id pat.note exp | TupP pats -> declare_pats pats exp + | ObjP pfs -> declare_pats (pats_of_obj_pat pfs) exp | OptP pat1 | VariantP (_, pat1) -> declare_pat pat1 exp | AltP (pat1, pat2) -> declare_pat pat1 exp @@ -430,6 +431,10 @@ and rename_pat' pat = | TupP pats -> let (patenv,pats') = rename_pats pats in (patenv,TupP pats') + | ObjP pfs -> + let (patenv, pats') = rename_pats (pats_of_obj_pat pfs) in + let pfs' = replace_obj_pat pfs pats' in + (patenv, ObjP pfs') | OptP pat1 -> let (patenv,pat1) = rename_pat pat1 in (patenv, OptP pat1) @@ -457,6 +462,7 @@ and define_pat patenv pat : dec list = | VarP id -> [ expD (define_idE id constM (PatEnv.find id.it patenv)) ] | TupP pats -> define_pats patenv pats + | ObjP pfs -> define_pats patenv (pats_of_obj_pat pfs) | OptP pat1 | VariantP (_, pat1) -> define_pat patenv pat1 | AltP (pat1, pat2) -> diff --git a/src/check_ir.ml b/src/check_ir.ml index 6da79a6eb57..4cbb8de5f6d 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -8,7 +8,7 @@ module E = Effect (* TODO: make note immutable, perhaps just using type abstraction *) (* TODO: - dereferencing is still implicit in the IR (see immut_typ below) - consider making it explicit as part of desugaring. + dereferencing is still implicit in the IR (see immut_typ below) - consider making it explicit as part of desugaring. *) (* TODO: enforce second-class nature of T.Mut? in check_typ *) @@ -575,6 +575,8 @@ and gather_pat env ve0 pat : val_env = T.Env.add id.it pat.note ve (*TBR*) | TupP pats -> List.fold_left go ve pats + | ObjP pfs -> + List.fold_left go ve (pats_of_obj_pat pfs) | AltP (pat1, pat2) -> ve | OptP pat1 @@ -601,7 +603,11 @@ and check_pat env pat : val_env = | 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; + t <: T.Tup ts; + ve + | ObjP pfs -> + let ve = check_pats pat.at env (pats_of_obj_pat pfs) T.Env.empty in + check_pat_fields env t pfs; ve | OptP pat1 -> let ve = check_pat env pat1 in @@ -628,6 +634,17 @@ and check_pats at env pats ve : val_env = let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in check_pats at env pats' ve' +and check_pat_fields env t = List.iter (check_pat_field env t) + +and check_pat_field env t (pf : pat_field) = + let Name lab = pf.it.name.it in + let tf = T.{lab; typ=pf.it.pat.note} in + let s, tfs = T.as_obj_sub lab t in + let (<:) = check_sub env pf.it.pat.at in + t <: T.Obj (s, [tf]); + if T.is_mut (T.lookup_field lab tfs) + then error env pf.it.pat.at "cannot match mutable field %s" lab + (* Objects *) and type_obj env s fs : T.typ = diff --git a/src/compile.ml b/src/compile.ml index 962291b0412..3c5d8bb52bf 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -4091,6 +4091,16 @@ let compile_relop env t op = compile_comparison env t1 op1 | _ -> todo_trap env "compile_relop" (Arrange.relop op) +(* compile_load_field performs a tag check if the projection's domain + is ambiguous, then calls the appropriate accessor *) +let compile_load_field env typ ({it=(Name n); _} as name) = + let selective tag = function + | None -> [] | Some code -> [ tag, code ] in + Tagged.branch_with env (ValBlockType (Some I32Type)) + (List.concat [ [Tagged.Object, Object.load_idx env typ name] + ; selective Tagged.Array (Array.fake_object_idx env n) + ; selective Tagged.Text (Text.fake_object_idx env n)]) + (* compile_lexp is used for expressions on the left of an assignment operator, produces some code (with side effect), and some pure code *) let rec compile_lexp (env : E.t) exp = @@ -4122,15 +4132,10 @@ and compile_exp (env : E.t) exp = G.i (Convert (Wasm.Values.I32 I32Op.WrapI64)) ^^ Array.idx env ^^ load_ptr - | DotE (e, ({it = Name n;_} as name)) -> + | DotE (e, name) -> SR.Vanilla, compile_exp_vanilla env e ^^ - let selective tag = function - | None -> [] | Some code -> [ tag, code ] - in Tagged.branch_with env (ValBlockType (Some I32Type)) - (List.concat [ [Tagged.Object, Object.load_idx env e.note.note_typ name] - ; selective Tagged.Array (Array.fake_object_idx env n) - ; selective Tagged.Text (Text.fake_object_idx env n)]) + compile_load_field env e.note.note_typ name | ActorDotE (e, ({it = Name n;_} as name)) -> SR.UnboxedReference, if E.mode env <> DfinityMode then G.i Unreachable else @@ -4412,9 +4417,7 @@ and compile_exp (env : E.t) exp = let rec go env cs = match cs with | [] -> CanFail (fun k -> k) - | (c::cs) -> - let pat = c.it.pat in - let e = c.it.exp in + | {it={pat; exp=e}; _}::cs -> let (env1, code) = compile_pat_local env pat in orElse ( CannotFail get_i ^^^ code ^^^ CannotFail (compile_exp_vanilla env1 e) ^^^ CannotFail set_j) @@ -4574,15 +4577,23 @@ and fill_pat env pat : patternCode = CannotFail (Var.set_val env name.it) | TupP ps -> let (set_i, get_i) = new_local env "tup_scrut" in - let rec go i ps env = match ps with + let rec go i = function | [] -> CannotFail G.nop - | (p::ps) -> + | p::ps -> let code1 = fill_pat env p in - let code2 = go (i+1) ps env in - ( CannotFail (get_i ^^ Tuple.load_n (Int32.of_int i)) ^^^ - code1 ^^^ - code2 ) in - CannotFail set_i ^^^ go 0 ps env + let code2 = go (Int32.add i 1l) ps in + CannotFail (get_i ^^ Tuple.load_n i) ^^^ code1 ^^^ code2 in + CannotFail set_i ^^^ go 0l ps + | ObjP pfs -> + let project = compile_load_field env pat.note in + let (set_i, get_i) = new_local env "obj_scrut" in + let rec go = function + | [] -> CannotFail G.nop + | {it={name; pat}; _}::pfs' -> + let code1 = fill_pat env pat in + let code2 = go pfs' in + CannotFail (get_i ^^ project name) ^^^ code1 ^^^ code2 in + CannotFail set_i ^^^ go pfs | AltP (p1, p2) -> let code1 = fill_pat env p1 in let code2 = fill_pat env p2 in diff --git a/src/coverage.ml b/src/coverage.ml index 1460cd9f35a..418be63b465 100644 --- a/src/coverage.ml +++ b/src/coverage.ml @@ -12,6 +12,7 @@ type desc = | Val of V.value | NotVal of ValSet.t | Tup of desc list + | Object of desc list | Opt of desc | Tag of desc * id | NotTag of TagSet.t @@ -20,6 +21,7 @@ type ctxt = | InOpt of ctxt | InTag of ctxt * id | InTup of ctxt * desc list * desc list * pat list * Type.typ list + | InObject of ctxt * desc list * desc list * pat_field list * Type.field list | InAlt1 of ctxt * Source.region * pat * Type.typ | InAlt2 of ctxt * Source.region | InCase of Source.region * case list * Type.typ @@ -77,6 +79,20 @@ let rec match_pat ctxt desc pat t sets = | Any -> List.map (fun _ -> Any) pats | _ -> assert false in match_tup ctxt [] descs pats ts sets + | ObjP pfs -> + let t' = Type.promote t in + let sensible (pf : pat_field) = + List.exists (fun {Type.lab; _} -> pf.it.id.it = lab) (snd (Type.as_obj_sub pf.it.id.it t')) in + let pfs' = List.filter sensible pfs in + let tf_of_pf (pf : pat_field) = + List.find (fun {Type.lab; _} -> pf.it.id.it = lab) (snd (Type.as_obj_sub pf.it.id.it t')) in + let tfs' = List.map tf_of_pf pfs' in + let descs = + match desc with + | Object descs -> descs + | Any -> List.map (fun _ -> Any) pfs' + | _ -> assert false + in match_object ctxt [] descs pfs' tfs' sets | OptP pat1 -> let t' = Type.as_opt (Type.promote t) in (match desc with @@ -152,6 +168,14 @@ and match_tup ctxt descs_r descs pats ts sets = | _ -> assert false +and match_object ctxt descs_r descs (pfs : pat_field list) tfs sets = + match descs, pfs, tfs with + | [], [], [] -> + succeed ctxt (Object (List.rev descs_r)) sets + | desc::descs', pf::pfs', Type.{lab; typ}::tfs' -> + match_pat (InObject (ctxt, descs_r, descs', pfs', tfs')) desc pf.it.pat typ sets + | _ -> + assert false and succeed ctxt desc sets : bool = match ctxt with @@ -161,6 +185,8 @@ and succeed ctxt desc sets : bool = succeed ctxt' (Tag (desc, t)) sets | InTup (ctxt', descs_r, descs, pats, ts) -> match_tup ctxt' (desc::descs_r) descs pats ts sets + | InObject (ctxt', descs_r, descs, pfs, tfs) -> + match_object ctxt' (desc::descs_r) descs pfs tfs sets | InAlt1 (ctxt', at1, _pat2, _t) -> sets.reached_alts <- AtSet.add at1 sets.reached_alts; succeed ctxt' desc sets @@ -187,6 +213,8 @@ and fail ctxt desc sets : bool = fail ctxt' (Tag (desc, id)) sets | InTup (ctxt', descs', descs, pats, _ts) -> fail ctxt' (Tup (List.rev descs' @ [desc] @ descs)) sets + | InObject (ctxt', descs', descs, pats, _ts) -> + fail ctxt' (Object (List.rev descs' @ [desc] @ descs)) sets | InAlt1 (ctxt', at1, pat2, t) -> match_pat (InAlt2 (ctxt', pat2.at)) desc pat2 t sets | InAlt2 (ctxt', at2) -> diff --git a/src/definedness.ml b/src/definedness.ml index a6a91cbfc4c..1add9728bcb 100644 --- a/src/definedness.ml +++ b/src/definedness.ml @@ -45,15 +45,15 @@ type fd = f * defs (* Operations: *) (* This adds a set of free variables to a combined set *) -let (+++) ((f,d) : fd) x = ((++) f x, d) +let (+++) ((f, d) : fd) x = ((++) f x, d) (* This takes the union of two combined sets *) -let (++++) (f1, d1) (f2,d2) = ((++) f1 f2, S.union d1 d2) +let (++++) (f1, d1) (f2, d2) = ((++) f1 f2, S.union d1 d2) let union_binders f xs = List.fold_left (++++) (M.empty, S.empty) (List.map f xs) let diff f d = M.filter (fun k _ -> not (S.mem k d)) f (* The bound variables from the second argument scope over the first *) -let (///) (x : f) ((f,d) : fd) = f ++ diff x d +let (///) (x : f) ((f, d) : fd) = f ++ diff x d (* Usage tracking. We distinguish between eager and delayed variable use. Eager variables become delayed @@ -126,6 +126,7 @@ and pat msgs p : fd = match p.it with | WildP -> (M.empty, S.empty) | VarP i -> (M.empty, S.singleton i.it) | TupP ps -> pats msgs ps + | ObjP pfs -> pat_fields msgs pfs | AnnotP (p, _) | ParP p -> pat msgs p | LitP l -> (M.empty, S.empty) @@ -136,6 +137,8 @@ and pat msgs p : fd = match p.it with and pats msgs ps : fd = union_binders (pat msgs) ps +and pat_fields msgs pfs = union_binders (fun (pf : pat_field) -> pat msgs pf.it.pat) pfs + and case msgs (c : case) = exp msgs c.it.exp /// pat msgs c.it.pat and cases msgs cs : f = unions (case msgs) cs diff --git a/src/desugar.ml b/src/desugar.ml index 3e04fd98494..1151a7b8bff 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -4,7 +4,7 @@ module I = Ir module T = Type open Construct -(* Combinators used in the desguaring *) +(* Combinators used in the desugaring *) let trueE : Ir.exp = boolE true let falseE : Ir.exp = boolE false @@ -218,12 +218,18 @@ and pat' = function | S.LitP l -> I.LitP !l | S.SignP (o, l) -> I.LitP (apply_sign o !l) | S.TupP ps -> I.TupP (pats ps) + | S.ObjP pfs -> + I.ObjP (pat_fields pfs) | S.OptP p -> I.OptP (pat p) | S.VariantP (i, p) -> I.VariantP (i, pat p) | S.AltP (p1, p2) -> I.AltP (pat p1, pat p2) | S.AnnotP (p, _) | S.ParP p -> pat' p.it +and pat_fields pfs = List.map pat_field pfs + +and pat_field pf = phrase (fun S.{id; pat=p} -> I.{name=phrase (fun s -> Name s) id; pat=pat p}) pf + and to_arg p : (Ir.arg * (Ir.exp -> Ir.exp)) = match p.it with | S.AnnotP (p, _) -> to_arg p diff --git a/src/freevars.ml b/src/freevars.ml index 3eb015bdba6..d97e664f6d8 100644 --- a/src/freevars.ml +++ b/src/freevars.ml @@ -103,6 +103,7 @@ and pat p : fd = match p.it with | WildP -> (M.empty, S.empty) | VarP i -> (M.empty, S.singleton i.it) | TupP ps -> pats ps + | ObjP pfs -> pats (pats_of_obj_pat pfs) | LitP l -> (M.empty, S.empty) | OptP p -> pat p | VariantP (i, p) -> pat p diff --git a/src/interpret.ml b/src/interpret.ml index 9d55281fb6c..e223f8d2093 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -438,6 +438,7 @@ and declare_pat pat : val_env = | WildP | LitP _ | SignP _ -> V.Env.empty | VarP id -> declare_id id | TupP pats -> declare_pats pats V.Env.empty + | ObjP pfs -> declare_pat_fields pfs V.Env.empty | OptP pat1 | VariantP (_, pat1) | AltP (pat1, _) (* both have empty binders *) @@ -451,6 +452,12 @@ and declare_pats pats ve : val_env = let ve' = declare_pat pat in declare_pats pats' (V.Env.adjoin ve ve') +and declare_pat_fields pfs ve : val_env = + match pfs with + | [] -> ve + | pf::pfs' -> + let ve' = declare_pat pf.it.pat in + declare_pat_fields pfs' (V.Env.adjoin ve ve') and define_id env id v = Lib.Promise.fulfill (find id.it env.vals) v @@ -464,6 +471,7 @@ and define_pat env pat v = else () | VarP id -> define_id env id v | TupP pats -> define_pats env pats (V.as_tup v) + | ObjP pfs -> define_pat_fields env pfs (V.as_obj v) | OptP pat1 -> (match v with | V.Opt v1 -> define_pat env pat1 v1 @@ -478,6 +486,12 @@ and define_pat env pat v = and define_pats env pats vs = List.iter2 (define_pat env) pats vs +and define_pat_fields env pfs vs = + List.iter (define_pat_field env vs) pfs + +and define_pat_field env vs pf = + let v = V.Env.find pf.it.id.it vs in + define_pat env pf.it.pat v and match_lit lit v : bool = match !lit, v with @@ -508,6 +522,8 @@ and match_pat pat v : val_env option = match_pat {pat with it = LitP lit} (Operator.unop t op v) | TupP pats -> match_pats pats (V.as_tup v) V.Env.empty + | ObjP pfs -> + match_pat_fields pfs (V.as_obj v) V.Env.empty | OptP pat1 -> (match v with | V.Opt v1 -> match_pat pat1 v1 @@ -538,6 +554,15 @@ and match_pats pats vs ve : val_env option = ) | _ -> assert false +and match_pat_fields pfs vs ve : val_env option = + match pfs with + | [] -> Some ve + | pf::pfs' -> + let v = V.Env.find pf.it.id.it vs in + begin match match_pat pf.it.pat v with + | Some ve' -> match_pat_fields pfs' vs (V.Env.adjoin ve ve') + | None -> None + end (* Objects *) diff --git a/src/interpret_ir.ml b/src/interpret_ir.ml index bb0977391ee..fe15e523d18 100644 --- a/src/interpret_ir.ml +++ b/src/interpret_ir.ml @@ -418,7 +418,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = and interpret_fields env fs = let ve = List.fold_left - (fun ve f -> + (fun ve (f : field) -> let Name name = f.it.name.it in V.Env.disjoint_add name (Lib.Promise.value (find f.it.var.it env.vals)) ve ) V.Env.empty fs in @@ -464,6 +464,7 @@ and declare_pat pat : val_env = | WildP | LitP _ -> V.Env.empty | VarP id -> declare_id id | TupP pats -> declare_pats pats V.Env.empty + | ObjP pfs -> declare_pats (pats_of_obj_pat pfs) V.Env.empty | OptP pat1 | VariantP (_, pat1) -> declare_pat pat1 | AltP (pat1, pat2) -> declare_pat pat1 @@ -488,6 +489,7 @@ and define_pat env pat v = else () | VarP id -> define_id env id v | TupP pats -> define_pats env pats (V.as_tup v) + | ObjP pfs -> define_field_pats env pfs (V.as_obj v) | OptP pat1 -> (match v with | V.Opt v1 -> define_pat env pat1 v1 @@ -504,6 +506,12 @@ and define_pat env pat v = and define_pats env pats vs = List.iter2 (define_pat env) pats vs +and define_field_pats env pfs vs = + let define_field (pf : pat_field) = + let Name key = pf.it.name.it in + define_pat env pf.it.pat (V.Env.find key vs) in + List.iter define_field pfs + and match_lit lit v : bool = let open Syntax in @@ -535,6 +543,8 @@ and match_pat pat v : val_env option = else None | TupP pats -> match_pats pats (V.as_tup v) V.Env.empty + | ObjP pfs -> + match_pat_fields pfs (V.as_obj v) V.Env.empty | OptP pat1 -> (match v with | V.Opt v1 -> match_pat pat1 v1 @@ -562,6 +572,17 @@ and match_pats pats vs ve : val_env option = ) | _ -> assert false +and match_pat_fields pfs vs ve : val_env option = + match pfs with + | [] -> Some ve + | pf::pfs' -> + begin + let Name key = pf.it.name.it in + match match_pat pf.it.pat (V.Env.find key vs) with + | Some ve' -> match_pat_fields pfs' vs (V.Env.adjoin ve ve') + | None -> None + end + (* Blocks and Declarations *) and interpret_block env ro decs exp k = diff --git a/src/ir.ml b/src/ir.ml index 59b92e6637a..bbfe5cd7dd2 100644 --- a/src/ir.ml +++ b/src/ir.ml @@ -14,16 +14,23 @@ type relop = Syntax.relop type mut = Syntax.mut type vis = Syntax.vis +type name = name' Source.phrase +and name' = Name of string + type pat = (pat', Type.typ) Source.annotated_phrase and pat' = | WildP (* wildcard *) | VarP of id (* variable *) | LitP of lit (* literal *) | TupP of pat list (* tuple *) + | ObjP of pat_field list (* object *) | OptP of pat (* option *) | VariantP of id * pat (* variant *) | AltP of pat * pat (* disjunctive *) +and pat_field = pat_field' Source.phrase +and pat_field' = {name : name; pat : pat} + (* Like id, but with a type attached *) type arg = (string, Type.typ) Source.annotated_phrase @@ -68,9 +75,6 @@ and exp' = and field = (field', Type.typ) Source.annotated_phrase and field' = {name : name; var : id} (* the var is by reference, not by value *) -and name = name' Source.phrase -and name' = Name of string - and case = case' Source.phrase and case' = {pat : pat; exp : exp} @@ -104,3 +108,14 @@ type flavor = { (* Program *) type prog = (dec list * exp) * flavor + + +(* object pattern helpers *) + +let pats_of_obj_pat pfs = List.map (fun {Source.it={name; pat}; _} -> pat) pfs + +let map_obj_pat f pfs = + List.map (fun ({Source.it={name; pat}; _} as pf) -> {pf with Source.it={name; pat=f pat}}) pfs + +let replace_obj_pat pfs pats = + List.map2 (fun ({Source.it={name; pat=_}; _} as pf) pat -> {pf with Source.it={name; pat}}) pfs pats diff --git a/src/parser.mly b/src/parser.mly index 21d02937f67..d3a3593acfa 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -496,6 +496,8 @@ pat_nullary : { LitP(ref l) @! at $sloc } | LPAR ps=seplist(pat_bin, COMMA) RPAR { (match ps with [p] -> ParP(p) | _ -> TupP(ps)) @! at $sloc } + | LCURLY fps=seplist(pat_field, semicolon) RCURLY + { ObjP(fps) @! at $sloc } pat_un : | p=pat_nullary @@ -525,6 +527,12 @@ return_typ : return_typ_nullary : | COLON t=typ_nullary { t } +pat_field : + | x=id + { {id = x; pat = VarP x @! x.at} @@ at $sloc } + | x=id EQ p=pat + { {id = x; pat = p} @@ at $sloc } + (* Declarations *) diff --git a/src/rename.ml b/src/rename.ml index 2f5a9152d6c..4b88d5a9a4e 100644 --- a/src/rename.ml +++ b/src/rename.ml @@ -95,6 +95,9 @@ and pat' rho p = match p with (VarP i, rho') | TupP ps -> let (ps, rho') = pats rho ps in (TupP ps, rho') + | ObjP pfs -> + let (pats, rho') = pats rho (pats_of_obj_pat pfs) in + (ObjP (replace_obj_pat pfs pats), rho') | LitP l -> (p, rho) | OptP p -> let (p', rho') = pat rho p in (OptP p', rho') diff --git a/src/serialization.ml b/src/serialization.ml index 65454d1fb52..9363cef00b1 100644 --- a/src/serialization.ml +++ b/src/serialization.ml @@ -243,6 +243,8 @@ module Transform() = struct pat | TupP pats -> TupP (List.map t_pat pats) + | ObjP pfs -> + ObjP (map_obj_pat t_pat pfs) | OptP pat1 -> OptP (t_pat pat1) | VariantP (id, pat1) -> diff --git a/src/syntax.ml b/src/syntax.ml index 39d2af3d984..a2c228f5ebc 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -101,6 +101,7 @@ and pat' = | LitP of lit ref (* literal *) | SignP of unop * lit ref (* signed literal *) | TupP of pat list (* tuple *) + | ObjP of pat_field list (* object *) | OptP of pat (* option *) | VariantP of id * pat (* tagged variant *) | AltP of pat * pat (* disjunctive *) @@ -108,11 +109,10 @@ and pat' = | ParP of pat (* parenthesis *) (* | AsP of pat * pat (* conjunctive *) - | ObjP of pat_field list (* object *) +*) and pat_field = pat_field' Source.phrase and pat_field' = {id : id; pat : pat} -*) (* Expressions *) diff --git a/src/tailcall.ml b/src/tailcall.ml index 23be775a084..71802672351 100644 --- a/src/tailcall.ml +++ b/src/tailcall.ml @@ -147,11 +147,12 @@ and pat env p = env and pat' env p = match p with - | WildP -> env + | WildP -> env | VarP i -> let env1 = bind env i None in env1 | TupP ps -> pats env ps + | ObjP pfs -> pats env (pats_of_obj_pat pfs) | LitP l -> env | OptP p | VariantP (_, p) -> pat env p diff --git a/src/type.ml b/src/type.ml index f2261cc5c3e..ec116989157 100644 --- a/src/type.ml +++ b/src/type.ml @@ -498,6 +498,8 @@ let rec rel_typ rel eq t1 t2 = p1 = Nat && p2 = Int | Prim p1, Shared when rel != eq -> true + | Prim Text, Obj _ when rel != eq -> + rel_typ rel eq text_obj t2 | Obj (s1, tfs1), Obj (s2, tfs2) -> s1 = s2 && rel_fields rel eq tfs1 tfs2 @@ -527,7 +529,7 @@ let rec rel_typ rel eq t1 t2 = c1 = c2 && s1 = s2 && (* subtyping on shared functions needs to imply subtyping of the serialized arguments, i.e. the IDL. Until we have a real IDL, we are conservative - here and assum no subtyping in the IDL. This makes shared functions invariant. *) + here and assume no subtyping in the IDL. This makes shared functions invariant. *) let rel_param = if s1 = Sharable then eq_typ else rel_typ in (match rel_binds rel eq tbs1 tbs2 with diff --git a/src/typing.ml b/src/typing.ml index 3a243eb3efa..471731d7247 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -791,6 +791,9 @@ and infer_pat' env pat : T.typ * val_env = | TupP pats -> let ts, ve = infer_pats pat.at env pats [] T.Env.empty in T.Tup ts, ve + | ObjP pfs -> + let (s, tfs), ve = infer_pat_fields pat.at env pfs [] T.Env.empty in + T.Obj (s, tfs), ve | OptP pat1 -> let t1, ve = infer_pat env pat1 in T.Opt t1, ve @@ -818,6 +821,13 @@ and infer_pats at env pats ts ve : T.typ list * val_env = let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in infer_pats at env pats' (t::ts) ve' +and infer_pat_fields at env pfs ts ve : (T.obj_sort * T.field list) * val_env = + match pfs with + | [] -> (T.(Object Local), List.rev ts), ve + | pf::pfs' -> + let typ, ve1 = infer_pat env pf.it.pat in + let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in + infer_pat_fields at env pfs' (T.{ lab = pf.it.id.it; typ }::ts) ve' and check_pat_exhaustive env t pat : val_env = let ve = check_pat env t pat in @@ -861,6 +871,15 @@ and check_pat' env t pat : val_env = error env pat.at "tuple pattern cannot consume expected type\n %s" (T.string_of_typ_expand t) ) + | ObjP pfs -> + (try + let s, tfs = T.as_obj_sub "" t in + if s = T.Actor then error env pat.at "object pattern cannot destructure actors"; + check_pat_fields env tfs (List.stable_sort compare_pat_field pfs) T.Env.empty pat.at + with Invalid_argument _ -> + error env pat.at "object pattern cannot consume expected type\n %s" + (T.string_of_typ_expand t) + ) | OptP pat1 -> (try let t1 = T.as_opt t in @@ -911,6 +930,32 @@ and check_pats env ts pats ve at : val_env = error env at "tuple pattern has %i more components than expected type" (List.length ts) +and check_pat_fields env tfs pfs ve at : val_env = + let repeated l = function + | [] -> None + | (pf : pat_field)::_ -> if l = pf.it.id.it then Some pf.at else None in + match pfs, tfs with + | [], [] -> ve + | pf::pfs', T.{ lab; typ }::tfs' -> + begin match compare pf.it.id.it lab with + | 0 -> + if T.is_mut typ then error env pf.at "cannot pattern match mutable field %s" lab; + let ve1 = check_pat env typ pf.it.pat in + let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in + begin match repeated lab pfs' with + | None -> check_pat_fields env tfs' pfs' ve' at + | Some at -> error env at "cannot pattern match repeated field %s" lab + end + | c when c > 0 -> + check_pat_fields env tfs' pfs ve at + | _ -> + error env pf.at "object pattern field %s is not contained in expected type" pf.it.id.it + end + | [], _ -> ve + | pf::_, [] -> + error env pf.at "object pattern field %s is not contained in expected type" pf.it.id.it + +and compare_pat_field {it={id = l1; pat; _};_} {it={id = l2; pat; _};_} = compare l1.it l2.it (* Objects *) @@ -936,6 +981,7 @@ and pub_pat pat xs : region T.Env.t * region T.Env.t = | WildP | LitP _ | SignP _ -> xs | VarP id -> pub_val_id id xs | TupP pats -> List.fold_right pub_pat pats xs + | ObjP pfs -> List.fold_right pub_pat_field pfs xs | AltP (pat1, _) | OptP pat1 | VariantP (_, pat1) @@ -943,6 +989,9 @@ and pub_pat pat xs : region T.Env.t * region T.Env.t = | ParP pat1 -> pub_pat pat1 xs +and pub_pat_field pf xs = + pub_pat pf.it.pat xs + and pub_typ_id id (xs, ys) : region T.Env.t * region T.Env.t = (T.Env.add id.it id.at xs, ys) @@ -1165,8 +1214,12 @@ and gather_pat env ve pat : val_env = | WildP | LitP _ | SignP _ -> ve | VarP id -> gather_id env ve id | TupP pats -> List.fold_left (gather_pat env) ve pats + | ObjP pfs -> List.fold_left (gather_pat_field env) ve pfs | VariantP (_, pat1) | AltP (pat1, _) | OptP pat1 | AnnotP (pat1, _) | ParP pat1 -> gather_pat env ve pat1 +and gather_pat_field env ve pf : val_env = + gather_pat env ve pf.it.pat + and gather_id env ve id : val_env = if T.Env.mem id.it ve then error env id.at "duplicate definition for %s in block" id.it; diff --git a/test/fail/actor-match.as b/test/fail/actor-match.as new file mode 100644 index 00000000000..c647921fe1e --- /dev/null +++ b/test/fail/actor-match.as @@ -0,0 +1,10 @@ +let a : actor {f : () -> (); g : () -> ()} = actor { + f () {}; + g () {} +}; + +func foo () = switch a { + case {f; g} { f() } +}; + +assert ((switch (foo()) { case () 0 }) == 0) \ No newline at end of file diff --git a/test/fail/object-patterns.as b/test/fail/object-patterns.as new file mode 100644 index 00000000000..90c3496c3e1 --- /dev/null +++ b/test/fail/object-patterns.as @@ -0,0 +1,20 @@ + +// subtyping in patterns + +let q : {a : Int; b : Nat} = new {a = -42; b = 25}; + +func get_a () : Int = switch (q) { + case {a = 25 : Nat} 1; // NOT OK: Nat cannot consume all Ints + case {a = 42; b} b; // OK: 42 is Int by subtyping + case + {a = a : Int; + b = 25 : Int} a; // OK: Int can consume all Nats +}; + +// the above is analogous to the simpler: + +func (a : Int) = switch a { + case 25 (); // OK: 25 is Int by subtyping + case (25 : Int) (); // OK: 25 is Int by ascription + case (a : Nat) () // NOT OK: Nat cannot consume all Ints +}; diff --git a/test/fail/objpat-duplicate.as b/test/fail/objpat-duplicate.as new file mode 100644 index 00000000000..db6f6a53a20 --- /dev/null +++ b/test/fail/objpat-duplicate.as @@ -0,0 +1,11 @@ +switch "duplicate field names" { + case { len = l; chars; len } { + for (x in chars()) { printInt (l()); } + } +}; + +switch "duplicate bindings" { + case { len; chars = len } { + printInt (len()) + } +}; diff --git a/test/fail/objpat-infer.as b/test/fail/objpat-infer.as new file mode 100644 index 00000000000..b052e4deef1 --- /dev/null +++ b/test/fail/objpat-infer.as @@ -0,0 +1,33 @@ +// checks + +ignore (switch (shared {}) { case {a} 42 }); + +// checks + +for ({} in [shared {}].vals()) { print "hey" }; + +// infers + +func foo {} : Int = 42; + +// infers + +shared func baz {} : Int = 42; + +// call it + +ignore (foo (new {})); +ignore (foo (shared {})); +ignore (foo (actor {})); + +let a = actor { bar {} : async Nat = async 25 }; +ignore (foo a); + + +ignore (baz (new {})); +ignore (baz (shared {})); +ignore (baz (actor {})); + +ignore (a.bar (new {})); +ignore (a.bar (shared {})); +ignore (a.bar (actor {})); diff --git a/test/fail/objpat-mutable.as b/test/fail/objpat-mutable.as new file mode 100644 index 00000000000..0b708aa7b93 --- /dev/null +++ b/test/fail/objpat-mutable.as @@ -0,0 +1,9 @@ +type WithMut = { var x : Int; y : Text }; + +func reject (o : WithMut) = + switch o { + case { y = "good" } { print "good" }; + //case { x = -42 } { print "bad" }; // backend: Invalid_argument("unop") + //case { x = (42 : Int) } { print "bad" }; // tc: cannot consume expected + case { x } { printInt x } + }; diff --git a/test/fail/ok/actor-match.tc.ok b/test/fail/ok/actor-match.tc.ok new file mode 100644 index 00000000000..dc155ec9176 --- /dev/null +++ b/test/fail/ok/actor-match.tc.ok @@ -0,0 +1 @@ +actor-match.as:7.8-7.14: type error, object pattern cannot destructure actors diff --git a/test/fail/ok/object-patterns.tc.ok b/test/fail/ok/object-patterns.tc.ok new file mode 100644 index 00000000000..ce5874191ea --- /dev/null +++ b/test/fail/ok/object-patterns.tc.ok @@ -0,0 +1,8 @@ +object-patterns.as:7.13-7.21: type error, pattern of type + Nat +cannot consume expected type + Int +object-patterns.as:19.9-19.16: type error, pattern of type + Nat +cannot consume expected type + Int diff --git a/test/fail/ok/objpat-duplicate.tc.ok b/test/fail/ok/objpat-duplicate.tc.ok new file mode 100644 index 00000000000..fe1968cfa74 --- /dev/null +++ b/test/fail/ok/objpat-duplicate.tc.ok @@ -0,0 +1,2 @@ +objpat-duplicate.as:2.26-2.29: type error, cannot pattern match repeated field len +objpat-duplicate.as:8.8-8.28: type error, duplicate binding for len in pattern diff --git a/test/fail/ok/objpat-infer.tc.ok b/test/fail/ok/objpat-infer.tc.ok new file mode 100644 index 00000000000..30310a8c0d3 --- /dev/null +++ b/test/fail/ok/objpat-infer.tc.ok @@ -0,0 +1,33 @@ +objpat-infer.as:3.36-3.37: type error, object pattern field a is not contained in expected type +objpat-infer.as:15.17-15.19: type error, shared function has non-shared parameter type + {} +objpat-infer.as:20.14-20.23: type error, expression of type + shared {} +cannot produce expected type + {} +objpat-infer.as:21.14-21.22: type error, expression of type + actor {} +cannot produce expected type + {} +objpat-infer.as:23.21-23.23: type error, shared function has non-shared parameter type + {} +objpat-infer.as:24.13-24.14: type error, expression of type + actor {bar : shared {} -> async Nat} +cannot produce expected type + {} +objpat-infer.as:28.14-28.23: type error, expression of type + shared {} +cannot produce expected type + {} +objpat-infer.as:29.14-29.22: type error, expression of type + actor {} +cannot produce expected type + {} +objpat-infer.as:32.16-32.25: type error, expression of type + shared {} +cannot produce expected type + {} +objpat-infer.as:33.16-33.24: type error, expression of type + actor {} +cannot produce expected type + {} diff --git a/test/fail/ok/objpat-mutable.tc.ok b/test/fail/ok/objpat-mutable.tc.ok new file mode 100644 index 00000000000..156c10c52f3 --- /dev/null +++ b/test/fail/ok/objpat-mutable.tc.ok @@ -0,0 +1 @@ +objpat-mutable.as:8.12-8.13: type error, cannot pattern match mutable field x diff --git a/test/run-dfinity/shared-object.as b/test/run-dfinity/shared-object.as new file mode 100644 index 00000000000..d65e633483f --- /dev/null +++ b/test/run-dfinity/shared-object.as @@ -0,0 +1,15 @@ +type Shob = shared { a : Int; b : { c : ?Nat } }; + +let foo : Shob = shared { a = 17; b = shared { c = ?25 } }; + +// check whether we can pattern match shared objects + +shared func baz (sh : Shob) : async Int = async (switch sh { + case { a; b = { c = null } } a; + case { a; b = { c = ?c } } (a + c) +}); + +async { + let b = await (baz foo); + assert (b == 42); +}; diff --git a/test/run/objects1.as b/test/run/objects1.as index f34d3a82657..faf19f324f9 100644 --- a/test/run/objects1.as +++ b/test/run/objects1.as @@ -13,3 +13,35 @@ let oo = object { func g() : T { f() + y }; private class C() {}; }; + +// pattern matching + +func get_b () : Int = switch (o) { + case {b = 11} 22; + case {b = result} result; + case {b = b : Int; a} b; + case {a} 42 +}; + +assert(get_b () == 0); + +// subtyping in patterns + +let q : {a : Int; b : Nat} = new {a = -42; b = 25}; + +func get_a () : Int = switch (q) { + case {a = 42; b} b; // OK: 42 is Int by subtyping + case {b = 25 : Nat; a = a : Int} a // OK: Int can consume all Nats +}; + +assert (get_a () == -42); + +// subtyping and tuple patterns for comparison + +let row : (Nat, Int, {c : Char; d : Text}) = (100, -42, new {c='C'; d="D"}); + +func foo () : Int = switch row { + case (a : Int, -42, {c} : {c : Char}) (word32ToNat(charToWord32 c)) // OK +}; + +assert (foo () == 67) diff --git a/test/run/objpat-iter.as b/test/run/objpat-iter.as new file mode 100644 index 00000000000..dcfa056416c --- /dev/null +++ b/test/run/objpat-iter.as @@ -0,0 +1,24 @@ +var y = 0; +switch ([1,2]) { + case ({ vals = iter }) { + for (x in iter()) { y := x; } + } +}; + +assert (y == 2); + +switch ([1,2]) { + case { vals; len } { + for (x in vals()) { y += x + len(); } + } +}; + +assert (y == 9); + +switch "Hi" { + case { chars; len } { + for (x in chars()) { y += 1 + len(); } + } +}; + +assert (y == 15); diff --git a/test/run/ok/objects1.run-ir.ok b/test/run/ok/objects1.run-ir.ok new file mode 100644 index 00000000000..73662fc5762 --- /dev/null +++ b/test/run/ok/objects1.run-ir.ok @@ -0,0 +1,4 @@ +objects1.as:22.3-22.26: warning, this case is never reached +objects1.as:23.3-23.14: warning, this case is never reached +objects1.as:32.23-35.2: warning, the cases in this switch do not cover all possible values +objects1.as:43.21-45.2: warning, the cases in this switch do not cover all possible values diff --git a/test/run/ok/objects1.run-low.ok b/test/run/ok/objects1.run-low.ok new file mode 100644 index 00000000000..73662fc5762 --- /dev/null +++ b/test/run/ok/objects1.run-low.ok @@ -0,0 +1,4 @@ +objects1.as:22.3-22.26: warning, this case is never reached +objects1.as:23.3-23.14: warning, this case is never reached +objects1.as:32.23-35.2: warning, the cases in this switch do not cover all possible values +objects1.as:43.21-45.2: warning, the cases in this switch do not cover all possible values diff --git a/test/run/ok/objects1.run.ok b/test/run/ok/objects1.run.ok new file mode 100644 index 00000000000..73662fc5762 --- /dev/null +++ b/test/run/ok/objects1.run.ok @@ -0,0 +1,4 @@ +objects1.as:22.3-22.26: warning, this case is never reached +objects1.as:23.3-23.14: warning, this case is never reached +objects1.as:32.23-35.2: warning, the cases in this switch do not cover all possible values +objects1.as:43.21-45.2: warning, the cases in this switch do not cover all possible values diff --git a/test/run/ok/objects1.tc.ok b/test/run/ok/objects1.tc.ok new file mode 100644 index 00000000000..73662fc5762 --- /dev/null +++ b/test/run/ok/objects1.tc.ok @@ -0,0 +1,4 @@ +objects1.as:22.3-22.26: warning, this case is never reached +objects1.as:23.3-23.14: warning, this case is never reached +objects1.as:32.23-35.2: warning, the cases in this switch do not cover all possible values +objects1.as:43.21-45.2: warning, the cases in this switch do not cover all possible values diff --git a/test/run/ok/objects1.wasm.stderr.ok b/test/run/ok/objects1.wasm.stderr.ok new file mode 100644 index 00000000000..73662fc5762 --- /dev/null +++ b/test/run/ok/objects1.wasm.stderr.ok @@ -0,0 +1,4 @@ +objects1.as:22.3-22.26: warning, this case is never reached +objects1.as:23.3-23.14: warning, this case is never reached +objects1.as:32.23-35.2: warning, the cases in this switch do not cover all possible values +objects1.as:43.21-45.2: warning, the cases in this switch do not cover all possible values