From 08e32c361df46851c4928540f380494257ddc2e8 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 19 Feb 2019 11:21:28 +0100 Subject: [PATCH 01/37] AST-38: add failing test --- test/fail/issue38.as | 9 +++++++++ test/fail/ok/issue38.tc.ok | 4 ++++ 2 files changed, 13 insertions(+) create mode 100644 test/fail/issue38.as create mode 100644 test/fail/ok/issue38.tc.ok diff --git a/test/fail/issue38.as b/test/fail/issue38.as new file mode 100644 index 00000000000..c419004f5f8 --- /dev/null +++ b/test/fail/issue38.as @@ -0,0 +1,9 @@ +func f() {}; +func g(()) {}; +func h(u:()) {}; + +let _ : [() -> ()] = [f, g, h]; + +f(); +g(); +h(); \ No newline at end of file diff --git a/test/fail/ok/issue38.tc.ok b/test/fail/ok/issue38.tc.ok new file mode 100644 index 00000000000..32fd767bf43 --- /dev/null +++ b/test/fail/ok/issue38.tc.ok @@ -0,0 +1,4 @@ +issue38.as:5.29-5.30: type error, expression of type + (()) -> () +cannot produce expected type + () -> () From 921c06a57c716395171d9fdcad8049d668295d49 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 19 Feb 2019 13:42:37 +0100 Subject: [PATCH 02/37] add Int arguments --- test/fail/issue38.as | 28 +++++++++++++++++++++++++--- test/fail/ok/issue38.tc.ok | 6 +++--- 2 files changed, 28 insertions(+), 6 deletions(-) diff --git a/test/fail/issue38.as b/test/fail/issue38.as index c419004f5f8..151d19688d8 100644 --- a/test/fail/issue38.as +++ b/test/fail/issue38.as @@ -2,8 +2,30 @@ func f() {}; func g(()) {}; func h(u:()) {}; -let _ : [() -> ()] = [f, g, h]; +let _ : [() -> ()] = [f]; +let gh : [(()) -> ()] = [g, h]; f(); -g(); -h(); \ No newline at end of file +g(); // why is this accepted? +h(); // dito +gh[0](); // dito +gh[1](); // dito + +// Correct: +g(()); +h(()); +gh[0](()); +gh[1](()); + + +func j(a:Int) {}; +func k(a:(Int)) {}; +func l(a:((Int))) {}; + +let jkl : [Int -> ()] = [j, k, l]; + +j(5); +k(8); +l(13); +jkl[1](21); + diff --git a/test/fail/ok/issue38.tc.ok b/test/fail/ok/issue38.tc.ok index 32fd767bf43..e9bdb45c5d6 100644 --- a/test/fail/ok/issue38.tc.ok +++ b/test/fail/ok/issue38.tc.ok @@ -1,4 +1,4 @@ -issue38.as:5.29-5.30: type error, expression of type - (()) -> () -cannot produce expected type +issue38.as:6.26-6.27: type error, expression of type () -> () +cannot produce expected type + (()) -> () From 7fcb0a5b17d1e7091285ade46fea5949b90fc328 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 11:16:14 +0100 Subject: [PATCH 03/37] AST-38: introduce ParP to indicate unary function and guide it through to type checker. Parser still not done, instead we explicitly write a 1-ary pattern at toplevel. --- src/arrange.ml | 9 +++++---- src/coverage.ml | 3 ++- src/definedness.ml | 3 ++- src/desugar.ml | 1 + src/interpret.ml | 4 ++++ src/parser.mly | 7 +++++-- src/syntax.ml | 1 + src/typing.ml | 4 +++- test/fail/issue38.as | 2 +- 9 files changed, 24 insertions(+), 10 deletions(-) diff --git a/src/arrange.ml b/src/arrange.ml index d2bc40e16c0..bda01e37525 100644 --- a/src/arrange.ml +++ b/src/arrange.ml @@ -8,17 +8,17 @@ let rec exp e = match e.it with | VarE i -> "VarE" $$ [id i] | LitE l -> "LitE" $$ [lit !l] | UnE (ot, uo, e) -> "UnE" $$ [operator_type !ot; unop uo; exp e] - | BinE (ot, e1, bo, e2) -> "BinE" $$ [operator_type !ot; exp e1; binop bo; exp e2] - | RelE (ot, e1, ro, e2) -> "RelE" $$ [operator_type !ot; exp e1; relop ro; exp e2] + | BinE (ot, e1, bo, e2) -> "BinE" $$ [operator_type !ot; exp e1; binop bo; exp e2] + | RelE (ot, e1, ro, e2) -> "RelE" $$ [operator_type !ot; exp e1; relop ro; exp e2] | 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, sr, n) -> "DotE" $$ [exp e; obj_sort' !sr; 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 typ ts @ [exp e2] - | BlockE (ds, ot) -> "BlockE" $$ List.map dec ds @ [operator_type (!ot)] + | 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] @@ -48,6 +48,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 16d2a2ff54a..930247d8f34 100644 --- a/src/coverage.ml +++ b/src/coverage.ml @@ -90,7 +90,8 @@ let rec match_pat ce ctxt desc pat t sets = | AltP (pat1, pat2) -> sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts); match_pat ce (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets - | AnnotP (pat1, _) -> + | AnnotP (pat1, _) + | ParP pat1 -> match_pat ce ctxt desc pat1 t sets and match_lit ce ctxt desc v t sets = diff --git a/src/definedness.ml b/src/definedness.ml index 0214dcb02d5..606280ff195 100644 --- a/src/definedness.ml +++ b/src/definedness.ml @@ -126,7 +126,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 7d8af75942f..5c584a6b839 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -203,6 +203,7 @@ and pat' = function | S.OptP p -> I.OptP (pat p) | S.AltP (p1, p2) -> I.AltP (pat p1, pat p2) | S.AnnotP (p, _) -> pat' p.it + | S.ParP p -> pat' p.it and prog p = (decs p.it, { I.has_await = true diff --git a/src/interpret.ml b/src/interpret.ml index a29eb38a2df..d26366369f2 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -435,6 +435,7 @@ and declare_pat pat : val_env = | OptP pat1 -> declare_pat pat1 | AltP (pat1, pat2) -> declare_pat pat1 | AnnotP (pat1, _typ) -> declare_pat pat1 + | ParP pat1 -> declare_pat pat1 and declare_pats pats ve : val_env = match pats with @@ -464,6 +465,7 @@ and define_pat env pat v = | _ -> assert false ) | AnnotP (pat1, _typ) -> define_pat env pat1 v + | ParP pat -> define_pat env pat v and define_pats env pats vs = List.iter2 (define_pat env) pats vs @@ -511,6 +513,8 @@ and match_pat pat v : val_env option = ) | AnnotP (pat1, _typ) -> match_pat pat1 v + | ParP pat -> + match_pat pat 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 3d205e2c8c3..d65246f2923 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -582,8 +582,11 @@ func_dec : | (true, e) -> (* body declared as immediate block *) match t.it with | AsyncT _ -> AsyncE(e) @? e.at - | _ -> e - in fun s x -> FuncD(s, x, tps, p, t, e) @? at $sloc } + | _ -> e in + let p2 = match p.it with + | TupP [p1] -> (*Printf.printf "Debug: %d\n" (List.length ps);*){ p with it = ParP p1 } + | _ -> p + in fun s x -> FuncD(s, x, tps, p2, t, e) @? at $sloc } func_body : | EQ e=exp { (false, e) } diff --git a/src/syntax.ml b/src/syntax.ml index 01fa40b3ad1..349876db21e 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -107,6 +107,7 @@ and pat' = | OptP of pat (* option *) | AltP of pat * pat (* disjunctive *) | AnnotP of pat * typ (* type annotation *) + | ParP of pat (* toplevel parenthesis *) (* | AsP of pat * pat (* conjunctive *) | ObjP of pat_field list (* object *) diff --git a/src/typing.ml b/src/typing.ml index 0d61df20c8e..0d0fd76e645 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -710,7 +710,8 @@ and gather_pat env ve0 pat : val_env = | AltP (pat1, pat2) -> go ve pat1 | OptP pat1 - | AnnotP (pat1, _) -> + | AnnotP (pat1, _) + | ParP pat1 -> go ve pat1 in T.Env.adjoin ve0 (go T.Env.empty pat) @@ -761,6 +762,7 @@ 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 diff --git a/test/fail/issue38.as b/test/fail/issue38.as index 151d19688d8..bcecd638f4b 100644 --- a/test/fail/issue38.as +++ b/test/fail/issue38.as @@ -1,5 +1,5 @@ func f() {}; -func g(()) {}; +func g((),) {}; func h(u:()) {}; let _ : [() -> ()] = [f]; From 67135bebdcf313ab9a002759f71670d55e4a3d06 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 11:23:33 +0100 Subject: [PATCH 04/37] no more type errors, TODO: non-fail --- test/fail/ok/issue38.tc.ok | 4 ---- 1 file changed, 4 deletions(-) delete mode 100644 test/fail/ok/issue38.tc.ok diff --git a/test/fail/ok/issue38.tc.ok b/test/fail/ok/issue38.tc.ok deleted file mode 100644 index e9bdb45c5d6..00000000000 --- a/test/fail/ok/issue38.tc.ok +++ /dev/null @@ -1,4 +0,0 @@ -issue38.as:6.26-6.27: type error, expression of type - () -> () -cannot produce expected type - (()) -> () From 3d3ee756ac9b4580bf22ea6eb4f518a4bad9cb8d Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 12:17:36 +0100 Subject: [PATCH 05/37] fix parser to remember significant parenthesis --- src/parser.mly | 18 ++++++++++++------ test/fail/issue38.as | 2 +- test/run/empty-tup-args.as | 2 +- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/src/parser.mly b/src/parser.mly index d65246f2923..2ec1a324f8d 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -475,6 +475,15 @@ exp_field : (* Patterns *) +pat_top : + | LPAR p=pat RPAR + { match p.it with + | TupP _ -> { p with it = ParP p } + | _ -> p + } + | p=pat_nullary + { p } + pat_nullary : | UNDERSCORE { WildP @! at $sloc } @@ -572,7 +581,7 @@ dec : LetD(p, ObjE(s, x, efs') @? r) @? r } func_dec : - | tps=typ_params_opt p=pat_nullary rt=return_typ? fb=func_body + | tps=typ_params_opt p=pat_top rt=return_typ? fb=func_body { 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 @@ -582,11 +591,8 @@ func_dec : | (true, e) -> (* body declared as immediate block *) match t.it with | AsyncT _ -> AsyncE(e) @? e.at - | _ -> e in - let p2 = match p.it with - | TupP [p1] -> (*Printf.printf "Debug: %d\n" (List.length ps);*){ p with it = ParP p1 } - | _ -> p - in fun s x -> FuncD(s, x, tps, p2, t, e) @? at $sloc } + | _ -> e + in fun s x -> FuncD(s, x, tps, p, t, e) @? at $sloc } func_body : | EQ e=exp { (false, e) } diff --git a/test/fail/issue38.as b/test/fail/issue38.as index bcecd638f4b..151d19688d8 100644 --- a/test/fail/issue38.as +++ b/test/fail/issue38.as @@ -1,5 +1,5 @@ func f() {}; -func g((),) {}; +func g(()) {}; func h(u:()) {}; let _ : [() -> ()] = [f]; diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index 1755cf1e22d..1e1f4f43dff 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -2,7 +2,7 @@ func f() {}; func g(()) {}; func h(u:()) {}; let _ = f : () -> (); -let _ = g : () -> (); +let _ = g : (()) -> (); let _ = h : (()) -> (); f(); g(); From 4fe6e09b153ef419c5acaba844bdde1b7f3df8b7 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 12:41:05 +0100 Subject: [PATCH 06/37] test successful --- test/{fail => run}/issue38.as | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename test/{fail => run}/issue38.as (100%) diff --git a/test/fail/issue38.as b/test/run/issue38.as similarity index 100% rename from test/fail/issue38.as rename to test/run/issue38.as From 2d8eac1d9d32c864609de3952cacccd36036137c Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 13:13:49 +0100 Subject: [PATCH 07/37] beef up the testing, discovering a subtle issue in wasm --- test/run/issue38.as | 27 +++++++++++++++++++++++++++ test/run/ok/issue38.wasm.stderr.ok | 5 +++++ 2 files changed, 32 insertions(+) create mode 100644 test/run/ok/issue38.wasm.stderr.ok diff --git a/test/run/issue38.as b/test/run/issue38.as index 151d19688d8..69e5dd22866 100644 --- a/test/run/issue38.as +++ b/test/run/issue38.as @@ -29,3 +29,30 @@ 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]; + +func p((),) {}; +let ps : [((),) -> ()] = [p]; + +/* the above is a curious case, failing in wasm: + +issue38: [tc] [run] [run-low] [run-ir] [wasm] +--- issue38.wasm.stderr (expected) ++++ issue38.wasm.stderr (actual) +@@ -0,0 +1,5 @@ ++Ill-typed intermediate code (use -v to see dumped IR): ++issue38.as:44.1-44.15: IR type error, subtype violation: ++ (((),)) -> () ++ (()) -> () ++ +*/ diff --git a/test/run/ok/issue38.wasm.stderr.ok b/test/run/ok/issue38.wasm.stderr.ok new file mode 100644 index 00000000000..1cbb20be970 --- /dev/null +++ b/test/run/ok/issue38.wasm.stderr.ok @@ -0,0 +1,5 @@ +Ill-typed intermediate code (use -v to see dumped IR): +issue38.as:44.1-44.15: IR type error, subtype violation: + (((),)) -> () + (()) -> () + From 1383827e7541248a6e6ad24c2a7867131f498e9c Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 13:35:26 +0100 Subject: [PATCH 08/37] review feedback --- src/interpret.ml | 7 +++---- src/parser.mly | 3 +++ test/run/issue38.as | 4 +++- test/run/ok/issue38.wasm.stderr.ok | 2 +- 4 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/interpret.ml b/src/interpret.ml index d26366369f2..4173851845e 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -511,10 +511,9 @@ and match_pat pat v : val_env option = | None -> match_pat pat2 v | some -> some ) - | AnnotP (pat1, _typ) -> - match_pat pat1 v - | ParP pat -> - match_pat pat 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 2ec1a324f8d..291bf5e6c0a 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -475,6 +475,9 @@ exp_field : (* Patterns *) +(* pat_top is needed because top-level parentheses around tuples (unit, 1-ary, pair, etc.) + are significant in function arguments, signifying a unary function which matches on a + first-class (i.e. consed) tuple *) pat_top : | LPAR p=pat RPAR { match p.it with diff --git a/test/run/issue38.as b/test/run/issue38.as index 69e5dd22866..cb15176e322 100644 --- a/test/run/issue38.as +++ b/test/run/issue38.as @@ -1,9 +1,11 @@ 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 gh : [(()) -> ()] = [g, h]; +let gh : [(()) -> ()] = [g, g1, h, h1]; f(); g(); // why is this accepted? diff --git a/test/run/ok/issue38.wasm.stderr.ok b/test/run/ok/issue38.wasm.stderr.ok index 1cbb20be970..469f203b497 100644 --- a/test/run/ok/issue38.wasm.stderr.ok +++ b/test/run/ok/issue38.wasm.stderr.ok @@ -1,5 +1,5 @@ Ill-typed intermediate code (use -v to see dumped IR): -issue38.as:44.1-44.15: IR type error, subtype violation: +issue38.as:46.1-46.15: IR type error, subtype violation: (((),)) -> () (()) -> () From 3f2e40567114ff230f2540aae2a7cfcff79f2efe Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 16:43:49 +0100 Subject: [PATCH 09/37] classes are basically functions and as such inherit the top-level arities --- src/parser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser.mly b/src/parser.mly index 291bf5e6c0a..bef8492a537 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -547,7 +547,7 @@ dec_nonvar : { (fd s (xf "func" $sloc)).it @? at $sloc } | 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 + | s=obj_sort_opt CLASS xf=id_opt tps=typ_params_opt p=pat_top xefs=class_body { let x, efs = xefs in let efs' = if s.it = Type.Object Type.Local From da9c08bc8ef924151a6cc9fbf4cde6bebb7e3175 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 20 Feb 2019 17:20:51 +0100 Subject: [PATCH 10/37] Factor out `pat_simple` so that `pat_top` and `pat_nullary` can share the common innards. This avoids the reduce/reduce conflicts reported by `menhir`. CAVEAT: I am not a grammar expert, so there may be better ways to accomplish this. Suggestions welcome. --- src/parser.mly | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/parser.mly b/src/parser.mly index bef8492a537..ec920b083eb 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -484,21 +484,25 @@ pat_top : | TupP _ -> { p with it = ParP p } | _ -> p } - | p=pat_nullary + | p=pat_simple { p } -pat_nullary : +pat_simple : | UNDERSCORE { WildP @! at $sloc } | x=id { VarP(x) @! at $sloc } | l=lit { LitP(ref l) @! at $sloc } - | LPAR p=pat RPAR - { p } | LPAR ps=seplist1(pat_bin, COMMA) RPAR { TupP(ps) @! at $sloc } +pat_nullary : + | LPAR p=pat RPAR + { p } + | p=pat_simple + { p } + pat_un : | p=pat_nullary { p } From 0d797e68a20952a80fe8908276e9c97fcb558717 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 16:27:36 +0100 Subject: [PATCH 11/37] more tests (classes) --- test/run/issue38.as | 39 ++++++++++++++++++++++++--------------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/test/run/issue38.as b/test/run/issue38.as index cb15176e322..740fa864317 100644 --- a/test/run/issue38.as +++ b/test/run/issue38.as @@ -8,7 +8,8 @@ let _ : [() -> ()] = [f]; let gh : [(()) -> ()] = [g, g1, h, h1]; f(); -g(); // why is this accepted? +g(); // accepted, because "At calls there is an implicit coercion + // between tuples and n-ary arguments" h(); // dito gh[0](); // dito gh[1](); // dito @@ -19,7 +20,6 @@ h(()); gh[0](()); gh[1](()); - func j(a:Int) {}; func k(a:(Int)) {}; func l(a:((Int))) {}; @@ -43,18 +43,27 @@ let ns : [(Int, Bool) -> ()] = [n, n1]; func o((a:Int,)) {}; let os : [((Int,)) -> ()] = [o]; -func p((),) {}; -let ps : [((),) -> ()] = [p]; +/* TODO +func q((?(a:Int),)) {}; +func q1((?((a:Int)),)) {}; +func q2(((?((a:Int)),))) {}; +let qs : [((?Int,)) -> ()] = [q, q1, q2] +*/ + -/* the above is a curious case, failing in wasm: +// 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]; -issue38: [tc] [run] [run-low] [run-ir] [wasm] ---- issue38.wasm.stderr (expected) -+++ issue38.wasm.stderr (actual) -@@ -0,0 +1,5 @@ -+Ill-typed intermediate code (use -v to see dumped IR): -+issue38.as:44.1-44.15: IR type error, subtype violation: -+ (((),)) -> () -+ (()) -> () -+ -*/ +func annih(f : A -> B) : (A -> ()) { func (a : A) { ignore (f a) } }; +//func annih(f : A -> B) : (A -> ()) { func (a : A) { let _ = f a; } }; +// fishy: let _ : [() -> ()] = [annih<(),F> F]; +let _ : [(()) -> ()] = [annih<(),G> G, annih<(),G1> G1, annih<(),H> H, annih<(),H1> H1]; From 53cb2ad8311a6f7cec8f5f659fa95eaae480a914 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 16:51:47 +0100 Subject: [PATCH 12/37] consolidate tests --- test/run/empty-tup-args.as | 58 ++++++++++++++++++++++++- test/run/issue38.as | 69 ------------------------------ test/run/ok/issue38.wasm.stderr.ok | 5 --- 3 files changed, 56 insertions(+), 76 deletions(-) delete mode 100644 test/run/issue38.as delete mode 100644 test/run/ok/issue38.wasm.stderr.ok diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index 1e1f4f43dff..78fffad42bf 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -1,9 +1,63 @@ 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 _ = h : (()) -> (); + +let _ : [() -> ()] = [f]; +let gh : [(()) -> ()] = [g, g1, h, h1]; + 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(()); +gh[0](()); +gh[1](()); + +func j(a:Int) {}; +func k(a:(Int)) {}; +func l(a:((Int))) {}; + +let jkl : [Int -> ()] = [j, k, l]; + +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]; diff --git a/test/run/issue38.as b/test/run/issue38.as deleted file mode 100644 index 740fa864317..00000000000 --- a/test/run/issue38.as +++ /dev/null @@ -1,69 +0,0 @@ -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 gh : [(()) -> ()] = [g, g1, h, h1]; - -f(); -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(()); -gh[0](()); -gh[1](()); - -func j(a:Int) {}; -func k(a:(Int)) {}; -func l(a:((Int))) {}; - -let jkl : [Int -> ()] = [j, k, l]; - -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]; - -/* TODO -func q((?(a:Int),)) {}; -func q1((?((a:Int)),)) {}; -func q2(((?((a:Int)),))) {}; -let qs : [((?Int,)) -> ()] = [q, q1, q2] -*/ - - -// 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) } }; -//func annih(f : A -> B) : (A -> ()) { func (a : A) { let _ = f a; } }; -// fishy: let _ : [() -> ()] = [annih<(),F> F]; -let _ : [(()) -> ()] = [annih<(),G> G, annih<(),G1> G1, annih<(),H> H, annih<(),H1> H1]; diff --git a/test/run/ok/issue38.wasm.stderr.ok b/test/run/ok/issue38.wasm.stderr.ok deleted file mode 100644 index 469f203b497..00000000000 --- a/test/run/ok/issue38.wasm.stderr.ok +++ /dev/null @@ -1,5 +0,0 @@ -Ill-typed intermediate code (use -v to see dumped IR): -issue38.as:46.1-46.15: IR type error, subtype violation: - (((),)) -> () - (()) -> () - From d31dcac67e587b37ef42ba279a2f88043aeae1d7 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 17:47:57 +0100 Subject: [PATCH 13/37] fix switch syntax in README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a13106b7fa2..dd32911f46b 100644 --- a/README.md +++ b/README.md @@ -243,7 +243,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()) ...` From b5b99254d1bf035e978c13b948890becec9861ae Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 18:41:17 +0100 Subject: [PATCH 14/37] simplify --- src/desugar.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/desugar.ml b/src/desugar.ml index 5c584a6b839..dbd59b85e4e 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -202,7 +202,7 @@ 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 = (decs p.it, From 71ccf02a683e3699a8ac1215b071e9b74421f0b0 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 18:44:11 +0100 Subject: [PATCH 15/37] tests for redundant parens deeper down in patterns --- test/run/empty-tup-args.as | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index 78fffad42bf..ce4fb2ebf8d 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -61,3 +61,24 @@ 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 are 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}; From de8f3a2ed3830ee334d17c3edb4baec4a3e42db3 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 18:50:01 +0100 Subject: [PATCH 16/37] more simplifications I smell a bug in declare_pat: ``` | AltP (pat1, pat2) -> declare_pat pat1 ``` here the pat2 is not considered. --- src/interpret.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/interpret.ml b/src/interpret.ml index 4173851845e..23a04b5ce2a 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -434,7 +434,7 @@ and declare_pat pat : val_env = | 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 + | AnnotP (pat1, _) | ParP pat1 -> declare_pat pat1 and declare_pats pats ve : val_env = @@ -464,8 +464,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 - | ParP pat -> define_pat env pat v + | AnnotP (pat1, _) + | ParP pat1 -> define_pat env pat1 v and define_pats env pats vs = List.iter2 (define_pat env) pats vs From 6f4ee64e1e10e774af8ef53b7746ecfc0c6417ab Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 19:18:20 +0100 Subject: [PATCH 17/37] roll back parser complications, materialising parens around tuples in the AST everywhere this comes at the slight cost of - growing the AST when the user inserts redundant parens - propagating the inference environment inwards of PatP Both are justified in face of keeping the parsing code cleaner, IMO. --- src/parser.mly | 29 ++++++++--------------------- src/typing.ml | 1 + 2 files changed, 9 insertions(+), 21 deletions(-) diff --git a/src/parser.mly b/src/parser.mly index ec920b083eb..6772b88597b 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -475,34 +475,21 @@ exp_field : (* Patterns *) -(* pat_top is needed because top-level parentheses around tuples (unit, 1-ary, pair, etc.) - are significant in function arguments, signifying a unary function which matches on a - first-class (i.e. consed) tuple *) -pat_top : - | LPAR p=pat RPAR - { match p.it with - | TupP _ -> { p with it = ParP p } - | _ -> p - } - | p=pat_simple - { p } - -pat_simple : +pat_nullary : | UNDERSCORE { WildP @! at $sloc } | x=id { VarP(x) @! at $sloc } | l=lit { LitP(ref l) @! at $sloc } + | LPAR p=pat RPAR + { match p.it with + | TupP _ -> { p with it = ParP p } + | _ -> p + } | LPAR ps=seplist1(pat_bin, COMMA) RPAR { TupP(ps) @! at $sloc } -pat_nullary : - | LPAR p=pat RPAR - { p } - | p=pat_simple - { p } - pat_un : | p=pat_nullary { p } @@ -551,7 +538,7 @@ dec_nonvar : { (fd s (xf "func" $sloc)).it @? at $sloc } | 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_top xefs=class_body + | s=obj_sort_opt CLASS xf=id_opt tps=typ_params_opt p=pat_nullary xefs=class_body { let x, efs = xefs in let efs' = if s.it = Type.Object Type.Local @@ -588,7 +575,7 @@ dec : LetD(p, ObjE(s, x, efs') @? r) @? r } func_dec : - | tps=typ_params_opt p=pat_top rt=return_typ? fb=func_body + | tps=typ_params_opt p=pat_nullary rt=return_typ? fb=func_body { 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 diff --git a/src/typing.ml b/src/typing.ml index 0d0fd76e645..1023446ecdc 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -829,6 +829,7 @@ 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 env.cons t t') then From 0d4844b385275829b9b1731ad9c3c7bfd08702d8 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 21 Feb 2019 20:24:34 +0100 Subject: [PATCH 18/37] merge snafu --- src/coverage.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coverage.ml b/src/coverage.ml index fee5d13b224..e70a5ae001b 100644 --- a/src/coverage.ml +++ b/src/coverage.ml @@ -92,7 +92,7 @@ let rec match_pat ctxt desc pat t sets = match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets | AnnotP (pat1, _) | ParP pat1 -> - match_pat ce ctxt desc pat1 t sets + match_pat ctxt desc pat1 t sets and match_lit ctxt desc v t sets = let desc_succ = Val v in From 7daa1601533f43fa6c99107253c07c355357a089 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 22 Feb 2019 13:47:53 +0100 Subject: [PATCH 19/37] desugar toplevel parentheses as TupP --- src/desugar.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/desugar.ml b/src/desugar.ml index c06f5a84185..004e11fe940 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -154,13 +154,17 @@ and decs ds = typD :: (phrase' dec' d) :: (decs ds) | _ -> (phrase' dec' d) :: (decs ds) -and dec' at n d = match d with +and dec' at n d = + let param p = match p.it with + | S.ParP p1 -> pat { p with it = S.TupP [p1] } + | _ -> pat p + in 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, typ_binds tbs, pat p, ty.note, exp e) + I.FuncD (cc, i, typ_binds tbs, param p, ty.note, exp e) | S.TypD (con_id, typ_bind, t) -> let c = Lib.Option.value con_id.note in I.TypD c @@ -179,7 +183,7 @@ and dec' at n d = match d with T.open_ inst rng | _ -> assert false in - I.FuncD (cc, fun_id, typ_binds tbs, pat p, obj_typ, (* TBR *) + I.FuncD (cc, fun_id, typ_binds tbs, param 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 } }) From 82f4f42b5190e2e0d7b069361bb540e33144f0e9 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 22 Feb 2019 14:12:32 +0100 Subject: [PATCH 20/37] accept IR problems for now --- test/run/ok/empty-tup-args.diff-ir.ok | 13 +++++++++++++ test/run/ok/empty-tup-args.run-ir.ok | 4 ++++ test/run/ok/empty-tup-args.wasm.stderr.ok | 5 +++++ 3 files changed, 22 insertions(+) create mode 100644 test/run/ok/empty-tup-args.diff-ir.ok create mode 100644 test/run/ok/empty-tup-args.run-ir.ok create mode 100644 test/run/ok/empty-tup-args.wasm.stderr.ok diff --git a/test/run/ok/empty-tup-args.diff-ir.ok b/test/run/ok/empty-tup-args.diff-ir.ok new file mode 100644 index 00000000000..7a5d2e5e065 --- /dev/null +++ b/test/run/ok/empty-tup-args.diff-ir.ok @@ -0,0 +1,13 @@ +--- empty-tup-args.run ++++ empty-tup-args.run-ir +@@ -0,0 +1,11 @@ ++(unknown location): internal error, File "interpret_ir.ml", line 559, characters 9-15: Assertion failed ++ ++Last environment: ++ ++Called from file "interpret_ir.ml", line 659, characters 8-23 ++Called from file "interpret_ir.ml", line 86, characters 8-23 ++Re-raised at file "interpret_ir.ml", line 83, characters 19-35 ++Called from file "interpret_ir.ml", line 90, characters 36-44 ++Called from file "interpret_ir.ml", line 689, characters 2-18 ++Called from file "pipeline.ml", line 172, characters 8-48 diff --git a/test/run/ok/empty-tup-args.run-ir.ok b/test/run/ok/empty-tup-args.run-ir.ok new file mode 100644 index 00000000000..949970c290c --- /dev/null +++ b/test/run/ok/empty-tup-args.run-ir.ok @@ -0,0 +1,4 @@ +(unknown location): internal error, File "interpret_ir.ml", line 559, characters 9-15: Assertion failed + +Last environment: + diff --git a/test/run/ok/empty-tup-args.wasm.stderr.ok b/test/run/ok/empty-tup-args.wasm.stderr.ok new file mode 100644 index 00000000000..8ffe2a156f6 --- /dev/null +++ b/test/run/ok/empty-tup-args.wasm.stderr.ok @@ -0,0 +1,5 @@ +Ill-typed intermediate code after desugaring (use -v to see dumped IR): +empty-tup-args.as:2.8-2.10: IR type error, subtype violation: + ((),) + () + From 922f757fb7e3a7d791efbbd16f42fce647aa9591 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 22 Feb 2019 15:27:52 +0100 Subject: [PATCH 21/37] WIP: it appears that running non-canonical patterns is still a problem so comment them out for now. --- test/run/empty-tup-args.as | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index ce4fb2ebf8d..103afc5fd65 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -12,17 +12,20 @@ let _ : [() -> ()] = [f]; let gh : [(()) -> ()] = [g, g1, h, h1]; f(); -g(); // accepted, because "At calls there is an implicit coercion +//g(); // accepted, because "At calls there is an implicit coercion // between tuples and n-ary arguments" h(); // dito -gh[0](); // dito -gh[1](); // dito +//gh[0](); // dito +//gh[1](); // dito // Correct: -g(()); +//g(()); h(()); -gh[0](()); -gh[1](()); +h1(()); +//gh[0](()); +//gh[1](()); +gh[2](()); +gh[3](()); func j(a:Int) {}; func k(a:(Int)) {}; @@ -76,7 +79,7 @@ let _ : [(Int, (Int,)) -> ()] = [r, s]; // redundant parens for anonymous functions let _ = (func (a:Nat, ()) : Nat { a }) (42, ()); -let _ = (func ((a:Nat, (()))) : Nat { a }) (42, ()); +//let _ = (func ((a:Nat, (()))) : Nat { a }) (42, ()); // test that switch expressions are also behave correctly with redundant parens From 88d6270fd2c1420f3a87e450dc2beb1ddabf3c1d Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 22 Feb 2019 15:31:35 +0100 Subject: [PATCH 22/37] remove .ok files --- test/run/ok/empty-tup-args.diff-ir.ok | 13 ------------- test/run/ok/empty-tup-args.run-ir.ok | 4 ---- 2 files changed, 17 deletions(-) delete mode 100644 test/run/ok/empty-tup-args.diff-ir.ok delete mode 100644 test/run/ok/empty-tup-args.run-ir.ok diff --git a/test/run/ok/empty-tup-args.diff-ir.ok b/test/run/ok/empty-tup-args.diff-ir.ok deleted file mode 100644 index 7a5d2e5e065..00000000000 --- a/test/run/ok/empty-tup-args.diff-ir.ok +++ /dev/null @@ -1,13 +0,0 @@ ---- empty-tup-args.run -+++ empty-tup-args.run-ir -@@ -0,0 +1,11 @@ -+(unknown location): internal error, File "interpret_ir.ml", line 559, characters 9-15: Assertion failed -+ -+Last environment: -+ -+Called from file "interpret_ir.ml", line 659, characters 8-23 -+Called from file "interpret_ir.ml", line 86, characters 8-23 -+Re-raised at file "interpret_ir.ml", line 83, characters 19-35 -+Called from file "interpret_ir.ml", line 90, characters 36-44 -+Called from file "interpret_ir.ml", line 689, characters 2-18 -+Called from file "pipeline.ml", line 172, characters 8-48 diff --git a/test/run/ok/empty-tup-args.run-ir.ok b/test/run/ok/empty-tup-args.run-ir.ok deleted file mode 100644 index 949970c290c..00000000000 --- a/test/run/ok/empty-tup-args.run-ir.ok +++ /dev/null @@ -1,4 +0,0 @@ -(unknown location): internal error, File "interpret_ir.ml", line 559, characters 9-15: Assertion failed - -Last environment: - From e646c9c7bda8a87fcd019484321cf20645472785 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Sun, 24 Feb 2019 14:18:04 +0100 Subject: [PATCH 23/37] fix nits --- src/interpret.ml | 4 ++-- src/syntax.ml | 2 +- src/typing.ml | 6 ++++-- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/interpret.ml b/src/interpret.ml index 23a04b5ce2a..25f0a05d123 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -432,8 +432,8 @@ 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 + | OptP pat1 + | AltP (pat1, _) (* both have empty binders *) | AnnotP (pat1, _) | ParP pat1 -> declare_pat pat1 diff --git a/src/syntax.ml b/src/syntax.ml index 30e4c564e14..8b27e931806 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -107,7 +107,7 @@ and pat' = | OptP of pat (* option *) | AltP of pat * pat (* disjunctive *) | AnnotP of pat * typ (* type annotation *) - | ParP of pat (* toplevel parenthesis *) + | 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 d768f2f6cc9..b7bd37d0abf 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -757,7 +757,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 + | ParP pat1 -> + infer_pat env pat1 and infer_pats at env pats ts ve : T.typ list * val_env = match pats with @@ -824,7 +825,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 + | ParP pat1 -> + check_pat' env t pat1 | _ -> let t', ve = infer_pat env pat in if not (T.sub t t') then From 02fd5eea5714bff74d77a0ac86edd5f0cbc1c3c0 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 25 Feb 2019 20:08:58 +0100 Subject: [PATCH 24/37] apply custom lowering to unary functions, stripping the outermost TupP --- src/desugar.ml | 7 +++++-- test/run/empty-tup-args.as | 14 +++++++------- test/run/ok/empty-tup-args.wasm.stderr.ok | 5 ----- 3 files changed, 12 insertions(+), 14 deletions(-) delete mode 100644 test/run/ok/empty-tup-args.wasm.stderr.ok diff --git a/src/desugar.ml b/src/desugar.ml index 80fb1e38ec7..3bade8cfed1 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -174,9 +174,12 @@ and decs ds = and dec d = phrase' dec' d and dec' at n d = + let fix_unary p = match p.it with + | S.TupP [p1] -> { p with it = p1.it } + | _ -> p in let param p = match p.it with - | S.ParP p1 -> pat { p with it = S.TupP [p1] } - | _ -> pat p + | S.ParP p1 -> pat (fix_unary { p with it = S.TupP [p1] }) + | _ -> pat (fix_unary p) in match d with | S.ExpD e -> I.ExpD (exp e) | S.LetD (p, e) -> I.LetD (pat p, exp e) diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index 103afc5fd65..fbc05c349d3 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -12,18 +12,18 @@ let _ : [() -> ()] = [f]; let gh : [(()) -> ()] = [g, g1, h, h1]; f(); -//g(); // accepted, because "At calls there is an implicit coercion +g(); // accepted, because "At calls there is an implicit coercion // between tuples and n-ary arguments" h(); // dito -//gh[0](); // dito -//gh[1](); // dito +gh[0](); // dito +gh[1](); // dito // Correct: -//g(()); +g(()); h(()); h1(()); -//gh[0](()); -//gh[1](()); +gh[0](()); +gh[1](()); gh[2](()); gh[3](()); @@ -79,7 +79,7 @@ let _ : [(Int, (Int,)) -> ()] = [r, s]; // redundant parens for anonymous functions let _ = (func (a:Nat, ()) : Nat { a }) (42, ()); -//let _ = (func ((a:Nat, (()))) : Nat { a }) (42, ()); +let _ = (func ((a:Nat, (()))) : Nat { a }) (42, ()); // test that switch expressions are also behave correctly with redundant parens diff --git a/test/run/ok/empty-tup-args.wasm.stderr.ok b/test/run/ok/empty-tup-args.wasm.stderr.ok deleted file mode 100644 index 8ffe2a156f6..00000000000 --- a/test/run/ok/empty-tup-args.wasm.stderr.ok +++ /dev/null @@ -1,5 +0,0 @@ -Ill-typed intermediate code after desugaring (use -v to see dumped IR): -empty-tup-args.as:2.8-2.10: IR type error, subtype violation: - ((),) - () - From 10547cbd81805e149a0c302e8c5547cbad84e4c9 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 25 Feb 2019 23:33:54 +0100 Subject: [PATCH 25/37] typo --- src/check_ir.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/check_ir.ml b/src/check_ir.ml index 9b9cf93a8d0..4655505c77f 100644 --- a/src/check_ir.ml +++ b/src/check_ir.ml @@ -740,7 +740,7 @@ and check_block_exps env t decs at = | [dec] -> check_dec env dec; check env at (T.is_unit t || T.sub (typ dec) t) - "declaration does not produce expect type" + "declaration does not produce expected type" | dec::decs' -> check_dec env dec; check_block_exps env t decs' at From f9ccad9191a963132466e673efdc8e1fd887fdae Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 25 Feb 2019 23:42:17 +0100 Subject: [PATCH 26/37] transform the type notes like the patterns --- src/desugar.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/desugar.ml b/src/desugar.ml index 3bade8cfed1..d1d53440e97 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -174,11 +174,11 @@ and decs ds = and dec d = phrase' dec' d and dec' at n d = - let fix_unary p = match p.it with - | S.TupP [p1] -> { p with it = p1.it } + let fix_unary p = match p.it, p.note with + | S.TupP [p1], Type.Tup [n] -> { p with it = p1.it; note = n } | _ -> p in let param p = match p.it with - | S.ParP p1 -> pat (fix_unary { p with it = S.TupP [p1] }) + | S.ParP p1 -> pat (fix_unary { p with it = S.TupP [p1]; note = Type.Tup [p.note] }) | _ -> pat (fix_unary p) in match d with | S.ExpD e -> I.ExpD (exp e) From 7cbdb577264e5f696cc1368cb1074cbaa7f9f27b Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 25 Feb 2019 23:44:07 +0100 Subject: [PATCH 27/37] grammar in comment --- test/run/empty-tup-args.as | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index fbc05c349d3..6403ecc783a 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -81,7 +81,7 @@ let _ : [(Int, (Int,)) -> ()] = [r, s]; let _ = (func (a:Nat, ()) : Nat { a }) (42, ()); let _ = (func ((a:Nat, (()))) : Nat { a }) (42, ()); -// test that switch expressions are also behave correctly with redundant parens +// 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}; From 9c29a4846541b93e9023653172483eb6b7c07466 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 26 Feb 2019 11:07:07 +0100 Subject: [PATCH 28/37] more precise Invalid_argument messages --- src/operator.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/operator.ml b/src/operator.ml index 1bdc2c27e4d..a7cbe3afb21 100644 --- a/src/operator.ml +++ b/src/operator.ml @@ -14,7 +14,7 @@ let word_unop fword8 fword16 fword32 fword64 = function | T.Word16 -> fun v -> Word16 (fword16 (as_word16 v)) | T.Word32 -> fun v -> Word32 (fword32 (as_word32 v)) | T.Word64 -> fun v -> Word64 (fword64 (as_word64 v)) - | _ -> raise (Invalid_argument "unop") + | _ -> raise (Invalid_argument "word_unop") let num_unop fint fword8 fword16 fword32 fword64 ffloat = function | T.Int -> fun v -> Int (fint (as_int v)) @@ -37,14 +37,14 @@ let unop t op = let text_binop ftext = function | T.Text -> fun v1 v2 -> Text (ftext (as_text v1) (as_text v2)) - | _ -> raise (Invalid_argument "binop") + | _ -> raise (Invalid_argument "text_binop") let word_binop fword8 fword16 fword32 fword64 = function | T.Word8 -> fun v1 v2 -> Word8 (fword8 (as_word8 v1) (as_word8 v2)) | T.Word16 -> fun v1 v2 -> Word16 (fword16 (as_word16 v1) (as_word16 v2)) | T.Word32 -> fun v1 v2 -> Word32 (fword32 (as_word32 v1) (as_word32 v2)) | T.Word64 -> fun v1 v2 -> Word64 (fword64 (as_word64 v1) (as_word64 v2)) - | _ -> raise (Invalid_argument "binop") + | _ -> raise (Invalid_argument "word_binop") let num_binop fnat fint fword8 fword16 fword32 fword64 ffloat = function | T.Nat -> fun v1 v2 -> Int (fnat (as_int v1) (as_int v2)) @@ -82,7 +82,7 @@ let word_relop fword8 fword16 fword32 fword64 = function | T.Word16 -> fun v1 v2 -> Bool (fword16 (as_word16 v1) (as_word16 v2)) | T.Word32 -> fun v1 v2 -> Bool (fword32 (as_word32 v1) (as_word32 v2)) | T.Word64 -> fun v1 v2 -> Bool (fword64 (as_word64 v1) (as_word64 v2)) - | _ -> raise (Invalid_argument "relop") + | _ -> raise (Invalid_argument "word_relop") let num_relop fnat fint fword8 fword16 fword32 fword64 ffloat = function | T.Nat -> fun v1 v2 -> Bool (fnat (as_int v1) (as_int v2)) From 2688aeb49f9a094519fdc9b7f84b030a65be5795 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 26 Feb 2019 12:11:07 +0100 Subject: [PATCH 29/37] use augmented source location --- src/parser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser.mly b/src/parser.mly index 3b98ed953eb..d1ed130cc7d 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -482,7 +482,7 @@ pat_nullary : { LitP(ref l) @! at $sloc } | LPAR p=pat RPAR { match p.it with - | TupP _ -> { p with it = ParP p } + | TupP _ -> { p with it = ParP p; at = at $sloc } | _ -> p } | LPAR ps=seplist1(pat_bin, COMMA) RPAR From 0b42e5edcc949ea9ce509014bba6cd72fee4f859 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 26 Feb 2019 12:12:19 +0100 Subject: [PATCH 30/37] test AST-56 --- test/run/AST-56.as | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test/run/AST-56.as 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]; From 92ea6b60e21b15ca1d5e926699cdb87cddb0b03a Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 28 Feb 2019 13:12:39 +0100 Subject: [PATCH 31/37] review feedback: fold 'fix_unary' into 'param' and move to toplevel --- src/desugar.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/desugar.ml b/src/desugar.ml index d1d53440e97..ebe92c51877 100644 --- a/src/desugar.ml +++ b/src/desugar.ml @@ -173,14 +173,13 @@ and decs ds = | _ -> (phrase' dec' d) :: (decs ds) and dec d = phrase' dec' d +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 = - let fix_unary p = match p.it, p.note with - | S.TupP [p1], Type.Tup [n] -> { p with it = p1.it; note = n } - | _ -> p in - let param p = match p.it with - | S.ParP p1 -> pat (fix_unary { p with it = S.TupP [p1]; note = Type.Tup [p.note] }) - | _ -> pat (fix_unary p) - in match d with + 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) From c67a0121f060eba2d3f3fa7c5fbff51eb88d6922 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 28 Feb 2019 14:33:28 +0100 Subject: [PATCH 32/37] Revert "more precise Invalid_argument messages" This reverts commit 9c29a4846541b93e9023653172483eb6b7c07466. --- src/operator.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/operator.ml b/src/operator.ml index a7cbe3afb21..1bdc2c27e4d 100644 --- a/src/operator.ml +++ b/src/operator.ml @@ -14,7 +14,7 @@ let word_unop fword8 fword16 fword32 fword64 = function | T.Word16 -> fun v -> Word16 (fword16 (as_word16 v)) | T.Word32 -> fun v -> Word32 (fword32 (as_word32 v)) | T.Word64 -> fun v -> Word64 (fword64 (as_word64 v)) - | _ -> raise (Invalid_argument "word_unop") + | _ -> raise (Invalid_argument "unop") let num_unop fint fword8 fword16 fword32 fword64 ffloat = function | T.Int -> fun v -> Int (fint (as_int v)) @@ -37,14 +37,14 @@ let unop t op = let text_binop ftext = function | T.Text -> fun v1 v2 -> Text (ftext (as_text v1) (as_text v2)) - | _ -> raise (Invalid_argument "text_binop") + | _ -> raise (Invalid_argument "binop") let word_binop fword8 fword16 fword32 fword64 = function | T.Word8 -> fun v1 v2 -> Word8 (fword8 (as_word8 v1) (as_word8 v2)) | T.Word16 -> fun v1 v2 -> Word16 (fword16 (as_word16 v1) (as_word16 v2)) | T.Word32 -> fun v1 v2 -> Word32 (fword32 (as_word32 v1) (as_word32 v2)) | T.Word64 -> fun v1 v2 -> Word64 (fword64 (as_word64 v1) (as_word64 v2)) - | _ -> raise (Invalid_argument "word_binop") + | _ -> raise (Invalid_argument "binop") let num_binop fnat fint fword8 fword16 fword32 fword64 ffloat = function | T.Nat -> fun v1 v2 -> Int (fnat (as_int v1) (as_int v2)) @@ -82,7 +82,7 @@ let word_relop fword8 fword16 fword32 fword64 = function | T.Word16 -> fun v1 v2 -> Bool (fword16 (as_word16 v1) (as_word16 v2)) | T.Word32 -> fun v1 v2 -> Bool (fword32 (as_word32 v1) (as_word32 v2)) | T.Word64 -> fun v1 v2 -> Bool (fword64 (as_word64 v1) (as_word64 v2)) - | _ -> raise (Invalid_argument "word_relop") + | _ -> raise (Invalid_argument "relop") let num_relop fnat fint fword8 fword16 fword32 fword64 ffloat = function | T.Nat -> fun v1 v2 -> Bool (fnat (as_int v1) (as_int v2)) From f93ecdc1f364fe8ea207594a24bf9ecbfb467ec8 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 4 Mar 2019 14:39:47 +0100 Subject: [PATCH 33/37] transform FuncE parameters in exp' --- src/desugar.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/desugar.ml b/src/desugar.ml index d552788d42b..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 From bffcea3c9e252e828235b6f4bdd84cd5feffbb44 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 4 Mar 2019 15:15:44 +0100 Subject: [PATCH 34/37] extend tests to include function expressions --- test/run/empty-tup-args.as | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/run/empty-tup-args.as b/test/run/empty-tup-args.as index 6403ecc783a..e3da0a23a6c 100644 --- a/test/run/empty-tup-args.as +++ b/test/run/empty-tup-args.as @@ -8,8 +8,8 @@ let _ = f : () -> (); let _ = g : (()) -> (); let _ = h : (()) -> (); -let _ : [() -> ()] = [f]; -let gh : [(()) -> ()] = [g, g1, h, h1]; +let _ : [() -> ()] = [f, func () {}, func f1 () {}]; +let gh : [(()) -> ()] = [g, g1, h, h1, func (()) {}, func g2 (()) {}]; f(); g(); // accepted, because "At calls there is an implicit coercion @@ -31,7 +31,7 @@ func j(a:Int) {}; func k(a:(Int)) {}; func l(a:((Int))) {}; -let jkl : [Int -> ()] = [j, k, l]; +let jkl : [Int -> ()] = [j, k, l, func l1(a:((Int))) {}]; j(5); k(8); From e4e7268dffa66c8f053f185fdb623f774ffbc057 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 4 Mar 2019 22:02:24 +0100 Subject: [PATCH 35/37] fix infer_pat' descent into PatP by calling `infer_pat`, so that the note gets updated for the subpattern --- src/typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typing.ml b/src/typing.ml index c18a4592bf3..74e62b2fd37 100644 --- a/src/typing.ml +++ b/src/typing.ml @@ -841,7 +841,7 @@ and check_pat' env t pat : val_env = error env pat.at "variables are not allowed in pattern alternatives"; T.Env.empty | ParP pat1 -> - check_pat' env t pat1 + check_pat env t pat1 | _ -> let t', ve = infer_pat env pat in if not (T.sub t t') then From c392aded0abd3d1a17a7d09ae653f26fcf385876 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 4 Mar 2019 22:26:31 +0100 Subject: [PATCH 36/37] experimental: always create ParP now that we correctly typecheck it. --- src/parser.mly | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/parser.mly b/src/parser.mly index c845d6651ac..7d494ce5a62 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -484,8 +484,8 @@ pat_nullary : { LitP(ref l) @! at $sloc } | LPAR p=pat RPAR { match p.it with - | TupP _ -> { p with it = ParP p; at = at $sloc } - | _ -> p + | TupP _ -> ParP(p) @! at $sloc + | _ -> ParP(p) @! p.at } | LPAR ps=seplist1(pat_bin, COMMA) RPAR { TupP(ps) @! at $sloc } From 81200bbb36cd683a65e16cfd9e054b15cb2a6f29 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 5 Mar 2019 23:14:44 +0100 Subject: [PATCH 37/37] review feedback: add negative tests --- test/fail/ok/one-tuple-ambiguity.tc.ok | 14 ++++++++++++++ test/fail/one-tuple-ambiguity.as | 22 ++++++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 test/fail/ok/one-tuple-ambiguity.tc.ok create mode 100644 test/fail/one-tuple-ambiguity.as 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