allow binding both an explicit and an implicit name

With placeholder syntax

Author: christoph-dfinity

src/lowering/desugar.ml

@@ -1045,6 +1045,7 @@ and pat p = phrase pat' p
 
 and pat' = function
   | S.VarP v -> I.VarP v.it
+  | S.GivenP { id; _ } -> I.VarP id.it
   | S.WildP -> I.WildP
   | S.LitP l -> I.LitP (lit !l)
   | S.SignP (o, l) -> I.LitP (lit (apply_sign o (!l)))

src/mo_def/syntax.ml

@@ -107,6 +107,7 @@ type pat = (pat', Type.typ) Source.annotated_phrase
 and pat' =
   | WildP                                      (* wildcard *)
   | VarP of id                                 (* variable *)
+  | GivenP of given                            (* implicit *)
   | LitP of lit ref                            (* literal *)
   | SignP of unop * lit ref                    (* signed literal *)
   | TupP of pat list                           (* tuple *)
@@ -120,6 +121,8 @@ and pat' =
   | AsP of pat * pat                           (* conjunctive *)
 *)
 
+and given = { implicit : id; id : id }
+
 and pat_field = pat_field' Source.phrase
 and pat_field' =
   | ValPF of id * pat

src/mo_frontend/coverage.ml

@@ -192,7 +192,7 @@ let skip_pat at sets =
 let rec match_pat ctxt desc pat t sets =
   T.span t = Some 0 && skip_pat pat.at sets ||
   match pat.it with
-  | WildP | VarP _ ->
+  | WildP | VarP _ | GivenP _ ->
     if T.inhabited t then
       succeed ctxt desc sets
     else

src/mo_frontend/definedness.ml

@@ -148,7 +148,7 @@ and exp_field msgs ef : f = exp msgs ef.it.exp
 
 and pat msgs p : fd = match p.it with
   | WildP         -> (M.empty, S.empty)
-  | VarP i        -> (M.empty, S.singleton i.it)
+  | VarP id | GivenP { id;_ } -> (M.empty, S.singleton id.it)
   | TupP ps       -> pats msgs ps
   | ObjP pfs      -> pat_fields msgs pfs
   | AnnotP (p, _)

src/mo_frontend/parser.mly

@@ -905,6 +905,8 @@ pat_plain :
     { WildP @! at $sloc }
   | x=id
     { VarP(x) @! at $sloc }
+  | x=id WITH y=id
+    { GivenP { id = x; implicit = y } @! at $sloc }
   | l=lit
     { LitP(ref l) @! at $sloc }
   | LPAR ps=seplist(pat_bin, COMMA) RPAR

src/mo_frontend/typing.ml

@@ -1066,7 +1066,7 @@ let is_explicit_lit l =
 
 let rec is_explicit_pat p =
   match p.it with
-  | WildP | VarP _ -> false
+  | WildP | VarP _ | GivenP _ -> false
   | LitP l | SignP (_, l) -> is_explicit_lit !l
   | OptP p1 | TagP (_, p1) | ParP p1 -> is_explicit_pat p1
   | TupP ps -> List.for_all is_explicit_pat ps
@@ -1313,6 +1313,7 @@ and combine_pat_srcs env t pat : unit =
   match pat.it with
   | WildP -> ()
   | VarP id -> combine_id_srcs env t id
+  | GivenP id -> combine_id_srcs env t id.id
   | LitP _ -> ()
   | SignP _ -> ()
   | TupP pats ->
@@ -3186,7 +3187,7 @@ and infer_pat' name_types env pat : T.typ * Scope.val_env =
   match pat.it with
   | WildP ->
     error env pat.at "M0102" "cannot infer type of wildcard"
-  | VarP _ ->
+  | VarP _ | GivenP _ ->
     error env pat.at "M0103" "cannot infer type of variable"
   | LitP lit ->
     T.Prim (infer_lit env lit pat.at), T.Env.empty
@@ -3304,6 +3305,8 @@ and check_pat_aux' env t pat val_kind : Scope.val_env =
     T.Env.empty
   | VarP id ->
     T.Env.singleton id.it (None, t, id.at, val_kind)
+  | GivenP { id; implicit } ->
+    T.Env.singleton id.it (Some implicit.it, t, id.at, val_kind)
   | LitP lit ->
     if not env.pre then begin
       let t' = if eq env pat.at t T.nat then T.int else t in  (* account for Nat <: Int *)
@@ -3584,7 +3587,7 @@ and vis_dec src dec xs : visibility_env =
 and vis_pat src pat xs : visibility_env =
   match pat.it with
   | WildP | LitP _ | SignP _ -> xs
-  | VarP id -> vis_val_id src id xs
+  | VarP id | GivenP { id; _} -> vis_val_id src id xs
   | TupP pats -> List.fold_right (vis_pat src) pats xs
   | ObjP pfs -> List.fold_right (vis_pat_field src) pfs xs
   | AltP (pat1, _)
@@ -4282,7 +4285,7 @@ and gather_dec env scope dec : Scope.t =
       | VarP id -> Scope.adjoin scope (Scope.mixin id.it (imports, args, t, decs))
       | _ -> error env pat.at "M0229" "mixins may only be imported by binding to a name"
   )
-  | VarD (id, _) -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id Scope.Declaration)
+  | VarD (id, _) -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id None Scope.Declaration)
   | TypD (id, binds, _) | ClassD (_, _, _, id, binds, _, _, _, _) ->
     let open Scope in
     if T.Env.mem id.it scope.typ_env then
@@ -4342,7 +4345,8 @@ and gather_pat env (scope : Scope.t) pat : Scope.t =
 and gather_pat_aux env val_kind scope pat : Scope.t =
   match pat.it with
   | WildP | LitP _ | SignP _ -> scope
-  | VarP id -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id val_kind)
+  | VarP id -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id None val_kind)
+  | GivenP { id; implicit } -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id (Some implicit.it) val_kind)
   | TupP pats -> List.fold_left (gather_pat env) scope pats
   | ObjP pfs -> List.fold_left (gather_pat_field env) scope pfs
   | TagP (_, pat1) | AltP (pat1, _) | OptP pat1
@@ -4354,11 +4358,10 @@ and gather_pat_field env scope pf : Scope.t =
   | ValPF (id, pat) -> gather_pat_aux env val_kind scope pat
   | TypPF id -> gather_typ_id env scope id
 
-and gather_id env ve id val_kind : Scope.val_env =
+and gather_id env ve id implicit val_kind : Scope.val_env =
   if T.Env.mem id.it ve then
     error_duplicate env "" id;
-  (* TODO *)
-  T.Env.add id.it (None, T.Pre, id.at, val_kind) ve
+  T.Env.add id.it (implicit, T.Pre, id.at, val_kind) ve
 
 and gather_typ_id env scope id : Scope.t =
   let open Scope in
@@ -4423,13 +4426,17 @@ and infer_dec_typdecs env dec : Scope.t =
     (match infer_val_path env exp with
      | None -> Scope.empty
      | Some t ->
-       let open Scope in
-       (* TODO *)
        match T.promote t with
-       | T.Obj (_, _) as t' -> { Scope.empty with val_env = singleton id None t' }
-       | _ -> { Scope.empty with val_env = singleton id None T.Pre }
-    )
-           end
+       | T.Obj (_, _) as t' -> Scope.{ empty with val_env = singleton id None t' }
+       | _ -> Scope.{ empty with val_env = singleton id None T.Pre }
+    ) end
+  | LetD ({it = GivenP { id; implicit }; _}, exp, _) ->
+    (match infer_val_path env exp with
+     | None -> Scope.empty
+     | Some t ->
+       match T.promote t with
+       | T.Obj (_, _) as t' -> Scope.{ empty with val_env = singleton id (Some implicit.it) t' }
+       | _ -> Scope.{ empty with val_env = singleton id (Some implicit.it) T.Pre })
   | LetD (pat, exp, _) ->
        begin match infer_val_path env exp with
        | Some t ->

src/mo_interpreter/interpret.ml

@@ -827,7 +827,7 @@ and declare_id id =
 and declare_pat pat : val_env =
   match pat.it with
   | WildP | LitP _ | SignP _ ->  V.Env.empty
-  | VarP id -> declare_id id
+  | VarP id | GivenP { id; _ } -> declare_id id
   | TupP pats -> declare_pats pats V.Env.empty
   | ObjP pfs -> declare_pat_fields pfs V.Env.empty
   | OptP pat1
@@ -896,7 +896,7 @@ and match_lit lit v : bool =
 and match_pat pat v : val_env option =
   match pat.it with
   | WildP -> Some V.Env.empty
-  | VarP id -> Some (V.Env.singleton id.it (Lib.Promise.make_fulfilled v))
+  | VarP id | GivenP { id; _ } -> Some (V.Env.singleton id.it (Lib.Promise.make_fulfilled v))
   | LitP lit ->
     if match_lit lit v
     then Some V.Env.empty

test/run/implicit-pat.mo

@@ -0,0 +1,16 @@
+let z with value : Nat = 0;
+
+func addOne(value : (implicit : Int)) : Int {
+  value + 1
+};
+
+func two() {
+  switch (+1) {
+    case x with value {
+      assert addOne() == 2;
+    };
+  };
+};
+
+two();
+assert addOne() == 1;