experiment: add implicit keyword and dedicated grammar

doc/docusaurus/src/theme/CodeBlock/hljs_run.js

@@ -78,7 +78,7 @@ export function registerMotoko() {
         $pattern: "[a-zA-Z_]\\w*",
         keyword:
           "actor and await break case catch class" +
-          " continue composite debug do else finally for func if in import" +
+          " continue composite debug do else finally for func if in import implicit" +
           " module not object or label let loop persistent private" +
           " public return shared transient try throw query switch" +
           " type var weak while with stable flexible system debug_show assert ignore from_candid to_candid" +

doc/md/16-language-manual.md

@@ -91,7 +91,7 @@ The following keywords are reserved and may not be used as identifiers:
 ``` bnf
 actor and assert async async* await await? await* break case catch class
 composite continue debug debug_show do else false flexible finally for
-from_candid func if ignore import in module not null persistent object or label
+from_candid func if ignore import implicit in module not null persistent object or label
 let loop private public query return shared stable switch system throw
 to_candid true transient try type var weak while with
 ```

doc/md/examples/grammar.txt

@@ -7,6 +7,9 @@
     X
     X SEP <list(X, SEP)>
 
+<implicit> ::= 
+    'implicit'
+
 <id_wild> ::= 
     '_'
 
@@ -65,6 +68,7 @@
 
 <typ> ::= 
     <typ_nobin>
+    <implicit> <typ_nobin>
     <typ> 'and' <typ>
     <typ> 'or' <typ>
 

src/gen-grammar/grammar.sed

@@ -43,6 +43,7 @@ s/ACTOR/\'actor\'/g
 s/COMPOSITE/\'composite\'/g
 s/IGNORE/\'ignore\'/g
 s/IMPORT/\'import\'/g
+s/IMPLICIT/\'implicit\'/g
 s/XOROP/\'^\'/g
 s/XORASSIGN/\'^=\'/g
 s/WHILE/\'while\'/g

src/idllib/escape.ml

@@ -82,6 +82,7 @@ let is_motoko_keyword = function
   | "ignore"
   | "in"
   | "import"
+  | "implicit"
   | "module"
   | "not"
   | "null"

src/mo_frontend/error_reporting.ml

@@ -82,6 +82,7 @@ let terminal2token (type a) (symbol : a terminal) : token =
       | T_IGNORE -> IGNORE
       | T_IF -> IF
       | T_ID -> ID "<id>"
+      | T_IMPLICIT -> IMPLICIT
       | T_HASH -> HASH
       | T_GTOP -> GTOP
       | T_GT -> GT

src/mo_frontend/parser.mly

@@ -223,7 +223,7 @@ and objblock eo s id ty dec_fields =
 %token LET VAR
 %token LPAR RPAR LBRACKET RBRACKET LCURLY RCURLY
 %token AWAIT AWAITSTAR AWAITQUEST ASYNC ASYNCSTAR BREAK CASE CATCH CONTINUE DO LABEL DEBUG
-%token IF IGNORE IN ELSE SWITCH LOOP WHILE FOR RETURN TRY THROW FINALLY WITH
+%token IF IGNORE IN IMPLICIT ELSE SWITCH LOOP WHILE FOR RETURN TRY THROW FINALLY WITH
 %token ARROW ASSIGN
 %token FUNC TYPE OBJECT ACTOR CLASS PUBLIC PRIVATE SHARED SYSTEM QUERY
 %token SEMICOLON SEMICOLON_EOL COMMA COLON SUB DOT QUEST BANG
@@ -366,6 +366,9 @@ seplist1(X, SEP) :
 %inline id :
   | id=ID { id @@ at $sloc }
 
+%inline implicit :
+  | IMPLICIT { "implicit" @@ at $sloc }
+
 %inline id_wild :
   | UNDERSCORE { "_" @@ at $sloc }
 
@@ -455,7 +458,6 @@ typ_un :
   | WEAK t=typ_un
     { WeakT(t) @! at $sloc }
 
-
 typ_pre :
   | t=typ_un
     { t }
@@ -479,6 +481,8 @@ typ_nobin :
 typ :
   | t=typ_nobin
     { t }
+  | i=implicit t = typ_nobin
+    { NamedT(i, t) @! at $sloc }
   | t1=typ AND t2=typ
     { AndT(t1, t2) @! at $sloc }
   | t1=typ OR t2=typ

src/mo_frontend/printers.ml

@@ -116,6 +116,7 @@ let repr_of_symbol : xsymbol -> (string * string) =
   | X (T T_LABEL) -> simple_token "label"
   | X (T T_IN) -> simple_token "in"
   | X (T T_IMPORT) -> simple_token "import"
+  | X (T T_IMPLICIT) -> simple_token "implicit"
   | X (T T_IGNORE) -> simple_token "ignore"
   | X (T T_IF) -> simple_token "if"
   | X (T T_ID) -> simple_token "<id>"

src/mo_frontend/source_lexer.mll

@@ -225,6 +225,7 @@ rule token mode = parse
   | "in" { IN }
   | "invariant" as s { if mode.verification then INVARIANT else ID s }
   | "implies" as s { if mode.verification then IMPLIES else ID s }
+  | "implicit" { IMPLICIT }
   | "old" as s { if mode.verification then OLD else ID s }
   | "import" { IMPORT }
   | "include" { INCLUDE }

src/mo_frontend/source_token.ml

@@ -28,6 +28,7 @@ type token =
   | IF
   | IGNORE
   | IN
+  | IMPLICIT
   | ELSE
   | SWITCH
   | LOOP
@@ -163,6 +164,7 @@ let to_parser_token :
   | IF -> Ok Parser.IF
   | IGNORE -> Ok Parser.IGNORE
   | IN -> Ok Parser.IN
+  | IMPLICIT -> Ok Parser.IMPLICIT
   | ELSE -> Ok Parser.ELSE
   | SWITCH -> Ok Parser.SWITCH
   | LOOP -> Ok Parser.LOOP
@@ -298,6 +300,7 @@ let string_of_parser_token = function
   | Parser.IF -> "IF"
   | Parser.IGNORE -> "IGNORE"
   | Parser.IN -> "IN"
+  | Parser.IMPLICIT -> "IMPLICIT"
   | Parser.ELSE -> "ELSE"
   | Parser.SWITCH -> "SWITCH"
   | Parser.LOOP -> "LOOP"

src/mo_types/type.ml

@@ -2071,6 +2071,8 @@ and sequence pp ppf ts =
 
 and pp_typ_nobin vs ppf t =
   match t with
+  | Named ("implicit", t) ->
+    fprintf ppf "@[<1>implicit %a@]" (pp_typ_nobin vs) t
   | Func (s, c, tbs, ts1, ts2) ->
     let sugar = can_sugar t in
     let vs' = vars_of_binds vs tbs in

test/fail/core-stub/src/Map.mo

@@ -23,7 +23,7 @@ module {
     }
   };
 
-  public func get<K, V>(map : Map<K, V>, compare : (implicit : (K, K) -> Types.Order), key : K) : ?V {
+  public func get<K, V>(map : Map<K, V>, compare : implicit (K, K) -> Types.Order, key : K) : ?V {
     switch (map.root) {
       case (#internal _) { null };
       case (#leaf(leafNode)) {
@@ -33,7 +33,7 @@ module {
     }
   };
 
-  public func add<K, V>(map : Map<K, V>, compare : (implicit : (K, K) -> Types.Order), key : K, value : V) {
+  public func add<K, V>(map : Map<K, V>, compare : implicit (K, K) -> Types.Order, key : K, value : V) {
     switch (map.root) {
       case (#internal _) { };
       case (#leaf(leafNode)) {

test/fail/implicit-best-candidate.mo

@@ -23,7 +23,7 @@ module Contravariant {
     public func cmp(_ : C, _ : C) : Nat = 3;
   };
 
-  func cmp<T>(x : T, y : T, cmp : (implicit : (T, T) -> Nat)) : Nat {
+  func cmp<T>(x : T, y : T, cmp : implicit (T, T) -> Nat) : Nat {
     cmp(x, y);
   };
 
@@ -49,7 +49,7 @@ module Covariant {
     public let default : C = { a = 0; b = "" };
   };
 
-  func default<T>(default : (implicit : T)) : T = default;
+  func default<T>(default : implicit T) : T = default;
 
   public func diamond() {
     ignore default<B>();

test/fail/implicit.mo

@@ -33,15 +33,15 @@ module N {
   };
 };
 
-func f1(n : Nat, m : Nat, c : (implicit : (Nat, Nat) -> Order)) {
+func f1(n : Nat, m : Nat, c : implicit (Nat, Nat) -> Order) {
   ignore c(n, m);
 };
 
-func f2<T>(n : T, m : T, c : (implicit : (T, T) -> Order)) {
+func f2<T>(n : T, m : T, c : implicit (T, T) -> Order) {
   ignore c(n, m);
 };
 
-func f3(n : Nat, m : Nat, d : (implicit : Nat -> Order)) {
+func f3(n : Nat, m : Nat, d : implicit Nat -> Order) {
 };
 
 
@@ -59,17 +59,17 @@ f2(true, true); // reject
 
 f3(1, 1); // reject
 
-func f4(n : Nat, m : Nat, bogus : (implicit : (Nat, Nat) -> Order)) {
+func f4(n : Nat, m : Nat, bogus : implicit (Nat, Nat) -> Order) {
 };
 
 f4(1, 1); // reject
 
 // retype f4 with as f4 with different implicit name
-let f5 : (Nat, Nat, (c : (implicit : (Nat, Nat) -> Order))) -> () = f4;
+let f5 : (Nat, Nat, c : implicit (Nat, Nat) -> Order) -> () = f4;
 
 f5(1, 1); // accept
 
-func f6(n : Nat, m : Nat, ambiguous : (implicit : (Nat, Nat) -> Order)) {
+func f6(n : Nat, m : Nat, ambiguous : implicit (Nat, Nat) -> Order) {
 };
 
 f6(1, 1); // reject
@@ -85,16 +85,16 @@ module XZ {
   public let zero : XZ = { x = 0; z = 0 };
 };
 
-func mkZero<T>(zero : (implicit : T)) : T {
+func mkZero<T>(zero : implicit T) : T {
   zero
 };
 
 ignore mkZero<{ x : Nat }>();
 
 // tricky case: if we have two implicit arguments of the same name we currently need to add a second type annotation
 func c <T, U>(p1 : (T, U), p2 : (T, U),
-   cT : (implicit : (c : (T, T) -> Order)),
-   cU : (implicit : (c : (U, U) -> Order)))
+   cT : implicit (c : (T, T) -> Order),
+   cU : implicit (c : (U, U) -> Order))
    : Order {
    switch (cT(p1.0, p2.0)) {
      case (#equal) { cU(p1.1, p2.1) };
@@ -104,7 +104,7 @@ func c <T, U>(p1 : (T, U), p2 : (T, U),
 
 ignore c((1,"a"),(0,"b")); // accepted
 
-func tuple(pair : (Nat, Nat), c : (implicit : (Nat, Nat) -> Order)) : Order {
+func tuple(pair : (Nat, Nat), c : implicit (Nat, Nat) -> Order) : Order {
   c(pair.0, pair.1)
 };
 

test/fail/ok/implicit-import-hint-dot.tc.ok

@@ -1,8 +1,7 @@
 implicit-import-hint-dot.mo:13.3-13.12: type error [M0098], cannot implicitly instantiate function of type
-  <K, V>(map : Map<K, V>, compare : (implicit : (K, K) -> Order), key : K) ->
-    ?V
+  <K, V>(map : Map<K, V>, compare : implicit (K, K) -> Order, key : K) -> ?V
 to argument of type
-  (compare : (implicit : (K, K) -> Order), key : K)
+  (compare : implicit (K, K) -> Order, key : K)
 to produce result of type
   ()
 because no instantiation of K, V makes

test/run/implicit-best-candidate.mo

@@ -19,7 +19,7 @@ module Contravariant {
     public func cmp(_ : C, _ : C) : Nat = 3;
   };
 
-  func cmp<T>(x : T, y : T, cmp : (implicit : (T, T) -> Nat)) : Nat {
+  func cmp<T>(x : T, y : T, cmp : implicit (T, T) -> Nat) : Nat {
     cmp(x, y);
   };
 
@@ -43,7 +43,7 @@ module Covariant {
     public let default : C = { a = 0; b = "" };
   };
 
-  func default<T>(default : (implicit : T)) : T = default;
+  func default<T>(default : implicit T) : T = default;
 
   public func test() {
     assert default<A>() == a;

test/run/implicit-map.mo

@@ -6,7 +6,7 @@ module Map {
 
   public type Self<T, U> = Map<T, U>;
 
-  public func get<T, U>(map : Self<T, U>, x : T, compare : (implicit : (T, T) -> Int)) : ?U {
+  public func get<T, U>(map : Self<T, U>, x : T, compare : implicit (T, T) -> Int) : ?U {
     if (compare(map.k, x) == 0) ?map.u else null;
   };
 };

test/run/implicit.mo

@@ -20,15 +20,15 @@ module N {
 
 };
 
-func f1(n : Nat, m : Nat, c : (implicit : (Nat, Nat) -> Order)) {
+func f1(n : Nat, m : Nat, c : implicit (Nat, Nat) -> Order) {
   ignore c(n, m);
 };
 
-func f2<T>(n : T, m : T, c : (implicit : (T, T) -> Order)) {
+func f2<T>(n : T, m : T, c : implicit (T, T) -> Order) {
   ignore c(n, m);
 };
 
-func f3(n : Nat, m : Nat, _ : (implicit : Nat -> Order)) {
+func f3(n : Nat, m : Nat, _ : implicit Nat -> Order) {
 };
 
 
@@ -58,13 +58,13 @@ do {
 
 //f3(1, 1); // reject
 
-func unary<T>(c : (implicit : (T, T) -> Order), t : T) {
+func unary<T>(c : implicit (T, T) -> Order, t : T) {
   ignore c(t, t)
 };
 
 unary(10);
 
-func nullary<T>(c : (implicit : (T, T) -> Order)) {
+func nullary<T>(c : implicit (T, T) -> Order) {
   ignore c;
 };
 nullary<Nat>();
@@ -83,13 +83,13 @@ module Int {
   };
 };
 
-func isEq<T>(x : T, y : T, eq : (implicit : (T, T) -> Bool)) : Bool {
+func isEq<T>(x : T, y : T, eq : implicit (T, T) -> Bool) : Bool {
   eq(x, y)
 };
 
 assert isEq<Nat>(3, 3);
 
-func tuple(pair : (Nat, Nat), eq : (implicit : (Nat, Nat) -> Bool)) : Bool {
+func tuple(pair : (Nat, Nat), eq : implicit (Nat, Nat) -> Bool) : Bool {
   eq(pair.0, pair.1)
 };
 

test/run/implicits-example.mo

@@ -12,7 +12,7 @@ module Int {
 
 module Array {
 
-  public func toText<T>(as : [T], toText: (implicit : T -> Text)) : Text {
+  public func toText<T>(as : [T], toText : implicit T -> Text) : Text {
      var t = "";
      for (a in as.vals()) {
        t := t # (toText(a));
@@ -27,8 +27,8 @@ module Pair {
 
   public func toText<T,U>(
     p : (T, U),
-    toTextT : (implicit : (toText : T -> Text)),
-    toTextU : (implicit : (toText : U -> Text)),
+    toTextT : implicit (toText : T -> Text),
+    toTextU : implicit (toText : U -> Text),
     )
     : Text {
       "(" # toTextT(p.0) # "," # toTextU(p.1) # ")"

test/viper/label-break-continue.mo

@@ -5,7 +5,7 @@ actor LabelBreakContinue {
     let simple_label = label simple : Int break simple(42);
     assert:system simple_label == 42;
 
-    let implicit_leave = label implicit : Int 42;
+    let implicit_leave = label implicit_ : Int 42;
     assert:system implicit_leave == 42;
 
     let block_label_early_expr = label block : (Int, Int) {

test/viper/ok/label-break-continue.vpr.ok

@@ -50,8 +50,8 @@ method label_expressions($Self: Ref)
       label $lbl$simple;
       assert (simple_label == 42);
       implicit_leave := 42;
-      goto $lbl$implicit;
-      label $lbl$implicit;
+      goto $lbl$implicit_;
+      label $lbl$implicit_;
       assert (implicit_leave == 42);
       if (true)
          {