diff --git a/README.md b/README.md index 740bc2d91e9..7ef013c7ad6 100644 --- a/README.md +++ b/README.md @@ -250,7 +250,7 @@ and open the path printed on the last line of that command. * Conditionals and switches - `if b ...` - `if b ... else ...` - - `switch x case 1 ... case 2 ... case _ ...` + - `switch x { case 1 ...; case 2 ...; case _ ...}` * While loops and iterations - `while (p()) ...` diff --git a/src/arrange.ml b/src/arrange.ml index f2ac44ae9a0..b94024667e2 100644 --- a/src/arrange.ml +++ b/src/arrange.ml @@ -59,6 +59,7 @@ and pat p = match p.it with | SignP (uo, l) -> "SignP" $$ [unop uo ; lit !l] | OptP p -> "OptP" $$ [pat p] | AltP (p1,p2) -> "AltP" $$ [pat p1; pat p2] + | ParP p -> "ParP" $$ [pat p] and lit (l:lit) = match l with | NullLit -> Atom "NullLit" diff --git a/src/coverage.ml b/src/coverage.ml index 3a278091253..e70a5ae001b 100644 --- a/src/coverage.ml +++ b/src/coverage.ml @@ -90,7 +90,8 @@ let rec match_pat ctxt desc pat t sets = | AltP (pat1, pat2) -> sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts); match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets - | AnnotP (pat1, _) -> + | AnnotP (pat1, _) + | ParP pat1 -> match_pat ctxt desc pat1 t sets and match_lit ctxt desc v t sets = diff --git a/src/definedness.ml b/src/definedness.ml index 3ec59b5e5ec..f2424e51bf4 100644 --- a/src/definedness.ml +++ b/src/definedness.ml @@ -131,7 +131,8 @@ 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 - | AnnotP (p, t) -> pat msgs p + | AnnotP (p, _) + | ParP p -> pat msgs p | LitP l -> (M.empty, S.empty) | SignP (uo, l) -> (M.empty, S.empty) | OptP p -> pat msgs p diff --git a/src/desugar.ml b/src/desugar.ml index 77b33e93684..652dfb7d6e7 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -56,7 +56,7 @@ and exp' at note = function | S.IdxE (e1, e2) -> I.IdxE (exp e1, exp e2) | S.FuncE (name, s, tbs, p, ty, e) -> let cc = Value.call_conv_of_typ note.S.note_typ in - I.FuncE (name, cc, typ_binds tbs, pat p, ty.note, exp e) + I.FuncE (name, cc, typ_binds tbs, param p, ty.note, exp e) | 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.note) inst in @@ -154,6 +154,12 @@ and decs ds = and dec d = { (phrase' dec' d) with note = () } +and param p = + pat (match p.it, p.note with + | S.ParP p1, _ -> p1 + | S.TupP [p1], Type.Tup [n] -> { p with it = p1.it; note = n } + | _ -> p) + and dec' at n d = match d with | S.ExpD e -> I.ExpD (exp e) | S.LetD (p, e) -> @@ -188,7 +194,7 @@ and dec' at n d = match d with in let varPat = {it = I.VarP id'; at = at; note = fun_typ } in let fn = { - it = I.FuncE (id.it, cc, typ_binds tbs, pat p, obj_typ, + it = I.FuncE (id.it, cc, typ_binds tbs, param p, obj_typ, { it = obj at s (Some self_id) es obj_typ; at = at; note = { S.note_typ = obj_typ; S.note_eff = T.Triv } }); @@ -215,7 +221,8 @@ and pat' = function | 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 + | S.AnnotP (p, _) + | S.ParP p -> pat' p.it and prog (p : Syntax.prog) : Ir.prog = begin match p.it with diff --git a/src/interpret.ml b/src/interpret.ml index 0a694111661..b1fc5c9d43c 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -436,9 +436,10 @@ 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 - | OptP pat1 -> declare_pat pat1 - | AltP (pat1, pat2) -> declare_pat pat1 - | AnnotP (pat1, _typ) -> declare_pat pat1 + | OptP pat1 + | AltP (pat1, _) (* both have empty binders *) + | AnnotP (pat1, _) + | ParP pat1 -> declare_pat pat1 and declare_pats pats ve : val_env = match pats with @@ -467,7 +468,8 @@ and define_pat env pat v = trap pat.at "value %s does not match pattern" (V.string_of_val v) | _ -> assert false ) - | AnnotP (pat1, _typ) -> define_pat env pat1 v + | AnnotP (pat1, _) + | ParP pat1 -> define_pat env pat1 v and define_pats env pats vs = List.iter2 (define_pat env) pats vs @@ -513,8 +515,9 @@ and match_pat pat v : val_env option = | None -> match_pat pat2 v | some -> some ) - | AnnotP (pat1, _typ) -> - match_pat pat1 v + | AnnotP (pat1, _) + | ParP pat1 -> + match_pat pat1 v and match_pats pats vs ve : val_env option = match pats, vs with diff --git a/src/parser.mly b/src/parser.mly index 7694adf4451..7d494ce5a62 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -483,7 +483,10 @@ pat_nullary : | l=lit { LitP(ref l) @! at $sloc } | LPAR p=pat RPAR - { p } + { match p.it with + | TupP _ -> ParP(p) @! at $sloc + | _ -> ParP(p) @! p.at + } | LPAR ps=seplist1(pat_bin, COMMA) RPAR { TupP(ps) @! at $sloc } diff --git a/src/syntax.ml b/src/syntax.ml index 81896a954b6..97d98aa762e 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -103,6 +103,7 @@ and pat' = | OptP of pat (* option *) | AltP of pat * pat (* disjunctive *) | AnnotP of pat * typ (* type annotation *) + | ParP of pat (* parenthesis *) (* | AsP of pat * pat (* conjunctive *) | ObjP of pat_field list (* object *) diff --git a/src/typing.ml b/src/typing.ml index c6de0bd7ceb..74e62b2fd37 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -772,6 +772,8 @@ and infer_pat' env pat : T.typ * val_env = | AnnotP (pat1, typ) -> let t = check_typ env typ in t, check_pat env t pat1 + | ParP pat1 -> + infer_pat env pat1 and infer_pats at env pats ts ve : T.typ list * val_env = match pats with @@ -838,6 +840,8 @@ and check_pat' env t pat : val_env = if ve1 <> T.Env.empty || ve2 <> T.Env.empty then error env pat.at "variables are not allowed in pattern alternatives"; T.Env.empty + | ParP pat1 -> + check_pat env t pat1 | _ -> let t', ve = infer_pat env pat in if not (T.sub t t') then @@ -887,7 +891,9 @@ and pub_pat pat xs : region T.Env.t * region T.Env.t = | TupP pats -> List.fold_right pub_pat pats xs | AltP (pat1, _) | OptP pat1 - | AnnotP (pat1, _) -> pub_pat pat1 xs + | AnnotP (pat1, _) + | ParP pat1 + -> pub_pat pat1 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) @@ -1109,7 +1115,7 @@ 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 - | AltP (pat1, _) | OptP pat1 | AnnotP (pat1, _) -> gather_pat env ve pat1 + | AltP (pat1, _) | OptP pat1 | AnnotP (pat1, _) | ParP pat1 -> gather_pat env ve pat1 and gather_id env ve id : val_env = if T.Env.mem id.it ve then diff --git a/test/fail/ok/one-tuple-ambiguity.tc.ok b/test/fail/ok/one-tuple-ambiguity.tc.ok new file mode 100644 index 00000000000..d81f6ed4b3b --- /dev/null +++ b/test/fail/ok/one-tuple-ambiguity.tc.ok @@ -0,0 +1,14 @@ +one-tuple-ambiguity.as:10.2-10.7: type error, expression of type + ((),) +cannot produce expected type + () +one-tuple-ambiguity.as:16.3-16.5: type error, literal of type + Nat +does not have expected type + (Nat, Bool) +one-tuple-ambiguity.as:16.1-16.5: type error, expected function type, but expression produces type + () +one-tuple-ambiguity.as:21.2-21.16: type error, expression of type + ((Nat, Bool),) +cannot produce expected type + (Nat, Bool) diff --git a/test/fail/one-tuple-ambiguity.as b/test/fail/one-tuple-ambiguity.as new file mode 100644 index 00000000000..170de85d256 --- /dev/null +++ b/test/fail/one-tuple-ambiguity.as @@ -0,0 +1,22 @@ +func g(()) {}; +let h = g : ((),) -> (); + +// this is accepted +h(()); + +// This is rejected, even if it could be seen +// as passing the single argument which is unit. +// It is interpreted as passing the one tuple containing unit. +h((),); + + +func k((a : Nat, b : Bool)) {}; +let l : ((Nat, Bool),) -> () = k; + +l 42 false; // rejected, 42 is not of type (Nat, Bool) + +l(42, false); // accepted, first-class pair implicitly converted to argument of call +l((42, false)); // accepted, parenthesis around values is redundant + +l((42, false),); // rejected, implicitly converted to passing + // first class one-tuple (enclosing pair) as the sole argument. \ No newline at end of file diff --git a/test/run/AST-56.as b/test/run/AST-56.as new file mode 100644 index 00000000000..7c246c5d20e --- /dev/null +++ b/test/run/AST-56.as @@ -0,0 +1,6 @@ +func p((),) {}; +func p1(()) {}; +func p2((())) {}; +func p3(((()))) {}; + +let ps : [((),) -> ()] = [p, p1, p2, p3]; diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index 1755cf1e22d..e3da0a23a6c 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -1,9 +1,87 @@ func f() {}; func g(()) {}; +func g1((())) {}; // only top-level parenthesis signifies arity func h(u:()) {}; +func h1((u:())) {}; // dito, intermediate parentheses are redundant + let _ = f : () -> (); -let _ = g : () -> (); +let _ = g : (()) -> (); let _ = h : (()) -> (); + +let _ : [() -> ()] = [f, func () {}, func f1 () {}]; +let gh : [(()) -> ()] = [g, g1, h, h1, func (()) {}, func g2 (()) {}]; + f(); -g(); -h(); +g(); // accepted, because "At calls there is an implicit coercion + // between tuples and n-ary arguments" +h(); // dito +gh[0](); // dito +gh[1](); // dito + +// Correct: +g(()); +h(()); +h1(()); +gh[0](()); +gh[1](()); +gh[2](()); +gh[3](()); + +func j(a:Int) {}; +func k(a:(Int)) {}; +func l(a:((Int))) {}; + +let jkl : [Int -> ()] = [j, k, l, func l1(a:((Int))) {}]; + +j(5); +k(8); +l(13); +jkl[1](21); + +func m((a:Int, b:Bool)) {}; +func m1((a:Int, b:Bool,)) {}; +let ms : [((Int, Bool)) -> ()] = [m, m1]; + +func n(a:Int, b:Bool) {}; +func n1(a:Int, b:Bool,) {}; + +let ns : [(Int, Bool) -> ()] = [n, n1]; + +func o((a:Int,)) {}; +let os : [((Int,)) -> ()] = [o]; + +// class tests, these have the same argument regime +class F() {}; +class G(()) {}; +class H(a:()) {}; +class G1((())) {}; +class H1((u:())) {}; +let _ : [() -> F] = [F]; +let _ : [(()) -> G] = [G]; +let _ : [(()) -> G1] = [G1]; +let _ : [(()) -> H] = [H]; +let _ : [(()) -> H1] = [H1]; + +func annih(f : A -> B) : (A -> ()) { func (a : A) { ignore (f a) } }; +let _ : [(()) -> ()] = [annih<(),G> G, annih<(),G1> G1, annih<(),H> H, annih<(),H1> H1]; + + +// test that parens are not significant deeper into the pattern, +// even around tuples + +func p(a:Int, () ) {}; +func q(a:Int, (())) {}; +func r(a:Int, (b:Int,) ) {}; +func s(a:Int, ((b:Int,))) {}; +let _ : [(Int, ()) -> ()] = [p, q]; +let _ : [(Int, (Int,)) -> ()] = [r, s]; + +// redundant parens for anonymous functions + +let _ = (func (a:Nat, ()) : Nat { a }) (42, ()); +let _ = (func ((a:Nat, (()))) : Nat { a }) (42, ()); + +// test that switch expressions also behave correctly with redundant parens + +let _ = switch (42,) { case (3,) 3; case ((5,)) 5; case (a,) a}; +let _ = switch (42,) { case (3,) 3; case ((5,)) 5; case (((a,))) a};