Optional params (#122)

Co-authored-by: Zieliński Patryk <[email protected]>
Co-authored-by: Piotr Polesiuk <[email protected]>

.gitignore

@@ -1,3 +1,4 @@
 _build
 
 dbl.opam
+.ocamlformat

src/DblParser/Desugar.ml

@@ -109,7 +109,7 @@ let rec find_self_arg args =
 let ident_of_name ~public (name : Raw.name) =
   match name with
   | NLabel      -> IdLabel
-  | NVar x      -> IdVar(public, x)
+  | NVar x | NOptionalVar x -> IdVar(public, x)
   | NImplicit n -> IdImplicit(public, n)
   | NMethod   n -> IdMethod(public, n)
 
@@ -632,10 +632,10 @@ and tr_explicit_inst (fld : Raw.field) =
   | FldName n ->
     let pe =
       match n with
-      | NLabel      -> Error.fatal (Error.desugar_error fld.pos)
-      | NVar      x -> make (EVar (NPName x))
-      | NImplicit n -> make (EImplicit (NPName n))
-      | NMethod   n -> Error.fatal (Error.desugar_error fld.pos)
+      | NLabel       -> Error.fatal (Error.desugar_error fld.pos)
+      | NVar x | NOptionalVar x -> make (EVar (NPName x))
+      | NImplicit n  -> make (EImplicit (NPName n))
+      | NMethod   n  -> Error.fatal (Error.desugar_error fld.pos)
     in
     Either.Right (make (n, make (EPoly(pe, [], []))))
   | FldNameVal(n, e) ->
@@ -871,7 +871,7 @@ and create_accessor_method ~public named_type_args pattern_gen scheme =
       [],
       make (EFn(pattern_gen field, e))))
     |> Option.some
-  | (NLabel | NImplicit _ | NMethod _), _ ->
+  | (NLabel | NImplicit _ | NMethod _ | NOptionalVar _), _ ->
     Error.warn (Error.ignored_field_in_record scheme.pos);
     None
 

src/DblParser/Lexer.mll

@@ -161,6 +161,7 @@ rule token = parse
   | lid_start var_char* as x { tokenize_ident x }
   | uid_start var_char* as x { YaccParser.UID x }
   | '`' lid_start var_char* as x { YaccParser.TLID x }
+  | '?' (lid_start var_char* as x) { YaccParser.QLID x }
   | '\'' (char as ch) '\'' { parse_char ch }
   | digit var_char* as x { tokenize_number lexbuf.Lexing.lex_start_p x }
   | '"' {

src/DblParser/Raw.ml

@@ -31,9 +31,10 @@ type var_id =
 (** Name of a named parameter *)
 type name = Lang.Surface.name =
   | NLabel
-  | NVar      of var
-  | NImplicit of iname
-  | NMethod   of method_name
+  | NVar         of var
+  | NOptionalVar of var
+  | NImplicit    of iname
+  | NMethod      of method_name
 
 (** Names of constructors of ADTs *)
 type ctor_name =

src/DblParser/YaccParser.mly

@@ -4,7 +4,7 @@
 
 /** Yacc-generated parser */
 
-%token<string> LID UID TLID
+%token<string> LID UID TLID QLID
 %token<string> OP_0 OP_20 OP_30 OP_40 OP_50 OP_60 OP_70 OP_80 OP_90 OP_100
 %token<int> NUM
 %token<int64> NUM64
@@ -69,6 +69,7 @@ var_id
 name
 : KW_LABEL  { NLabel       }
 | LID       { NVar $1      }
+| QLID      { NOptionalVar $1 }
 | TLID      { NImplicit $1 }
 | KW_METHOD LID { NMethod $2   }
 ;

src/Lang/Surface.ml

@@ -43,9 +43,10 @@ type tname =
 (** Name of a named parameter *)
 type name =
   | NLabel
-  | NVar      of var
-  | NImplicit of iname
-  | NMethod   of method_name 
+  | NVar         of var
+  | NOptionalVar of var
+  | NImplicit    of iname
+  | NMethod      of method_name 
 
 (** Visibility of definition *)
 type is_public = bool

src/Lang/Unif.mli

@@ -46,6 +46,9 @@ type name =
   | NVar      of string
     (** Regular named parameter *)
 
+  | NOptionalVar of string
+    (** Optional named parameter *)
+
   | NImplicit of string
     (** Implicit parameter *)
 

src/Lang/UnifPriv/Name.ml

@@ -19,6 +19,10 @@ module Ordered = struct
     | NVar _,  _       -> -1
     | _,       NVar _  -> 1
 
+    | NOptionalVar x1, NOptionalVar x2 -> String.compare x1 x2
+    | NOptionalVar _,  _       -> -1
+    | _,       NOptionalVar _  -> 1
+
     | NMethod n1, NMethod n2 -> String.compare n1 n2
     | NMethod _, _ -> -1
     | _, NMethod _ -> 1
@@ -34,6 +38,9 @@ let equal n1 n2 =
   | NVar x1, NVar x2 -> x1 = x2
   | NVar _, _ -> false
 
+  | NOptionalVar x1, NOptionalVar x2 -> x1 = x2
+  | NOptionalVar _, _ -> false
+
   | NMethod n1, NMethod n2 -> n1 = n2
   | NMethod _, _ -> false
 

src/Lang/UnifPriv/Subst.ml

@@ -53,7 +53,7 @@ let in_uvar sub p u =
 
 let in_name sub n =
   match n with
-  | NLabel | NVar _ | NImplicit _ | NMethod _ -> n
+  | NLabel | NVar _ | NOptionalVar _ | NImplicit _ | NMethod _ -> n
 
 (* Substitute in variable of kind [effect]. Since kind [effect] can contain
   only ground effects, substituted type is always (in some sense) a set of

src/Lang/UnifPriv/TypeBase.ml

@@ -18,9 +18,10 @@ type named_tvar = tname * tvar
 
 type name =
   | NLabel
-  | NVar      of string
-  | NImplicit of string
-  | NMethod   of string
+  | NVar         of string
+  | NOptionalVar of string
+  | NImplicit    of string
+  | NMethod      of string
 
 type uvar = {
   uid   : UID.t;
@@ -90,7 +91,7 @@ let t_app tp1 tp2 = TApp(tp1, tp2)
 
 let perm_name p n =
   match n with
-  | NLabel | NVar _ | NImplicit _ | NMethod _ -> n
+  | NLabel | NVar _ | NOptionalVar _ | NImplicit _ | NMethod _ -> n
 
 let perm_named_tvar p (n, x) =
   (n, TVar.Perm.apply p x)

src/Lang/UnifPriv/TypeBase.mli

@@ -19,9 +19,10 @@ type named_tvar = tname * tvar
 
 type name =
   | NLabel
-  | NVar      of string
-  | NImplicit of string
-  | NMethod   of string
+  | NVar         of string
+  | NOptionalVar of string
+  | NImplicit    of string
+  | NMethod      of string
 
 type typ
 

src/TypeInference/Error.ml

@@ -33,9 +33,10 @@ let rec string_of_path (p : string Lang.Surface.path) =
 let string_of_name (name : Lang.Unif.name) =
   match name with
   | NLabel -> "the effect label"
-  | NImplicit n -> Printf.sprintf "implicit parameter %s" n
-  | NVar x      -> Printf.sprintf "named parameter %s" x
-  | NMethod n   -> Printf.sprintf "method %s" n
+  | NImplicit n    -> Printf.sprintf "implicit parameter %s" n
+  | NVar x         -> Printf.sprintf "named parameter %s" x
+  | NOptionalVar x -> Printf.sprintf "optional named parameter %s" x
+  | NMethod n      -> Printf.sprintf "method %s" n
 
 let kind_mismatch ~pos k1 k2 =
   let pp_ctx = Pretty.empty_context () in
@@ -106,6 +107,13 @@ let unbound_method ~pos ~env x name =
     name
   in (pos, msg ^ Pretty.additional_info pp_ctx, [])
 
+let unbound_adt ~pos ~env x =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "There is no ADT assigned to this type var %s"
+    (Pretty.tvar_to_string pp_ctx env x)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
+
 let method_fn_without_arg ~pos x name =
   (pos, Printf.sprintf
     ("Variable %s is registered as method %s"
@@ -356,6 +364,9 @@ let non_polymorphic_pattern ~pos =
 let polymorphic_label ~pos =
   (pos, "Labels cannot be polymorphic", [])
 
+let polymorphic_optional_parameter ~pos =
+  (pos, "Optional parameters cannot be polymorphic", [])
+
 let label_type_mismatch ~pos =
   (pos, "Labels cannot have non-label type", [])
 
@@ -395,10 +406,11 @@ let type_inst_redefinition ~pos ~ppos (name : Lang.Surface.tname) =
 let inst_redefinition ~pos ~ppos (name : Lang.Surface.name) =
   let nn =
     match name with
-    | NLabel      -> Printf.sprintf "The label"
-    | NImplicit n -> Printf.sprintf "Implicit parameter %s" n
-    | NVar      x -> Printf.sprintf "Named parameter %s" x
-    | NMethod   n -> Printf.sprintf "Method %s" n
+    | NLabel         -> Printf.sprintf "The label"
+    | NImplicit    n -> Printf.sprintf "Implicit parameter %s" n
+    | NVar         x -> Printf.sprintf "Named parameter %s" x
+    | NOptionalVar x -> Printf.sprintf "Optional named parameter %s" x
+    | NMethod      n -> Printf.sprintf "Method %s" n
   in
   (pos, Printf.sprintf "%s is provided more than once" nn,
     [ ppos, "Here is a previous definition" ])
@@ -417,10 +429,11 @@ let ctor_type_arg_same_as_data_arg ~pos (name : Lang.Surface.tname) =
 let multiple_inst_patterns ~pos ~ppos (name : Lang.Surface.name) =
   let nn =
     match name with
-    | NLabel      -> Printf.sprintf "The label"
-    | NImplicit n -> Printf.sprintf "Implicit parameter %s" n
-    | NVar      x -> Printf.sprintf "Named parameter %s" x
-    | NMethod   n -> Printf.sprintf "Method %s" n
+    | NLabel         -> Printf.sprintf "The label"
+    | NImplicit    n -> Printf.sprintf "Implicit parameter %s" n
+    | NVar         x -> Printf.sprintf "Named parameter %s" x
+    | NOptionalVar x -> Printf.sprintf "Optional named parameter %s" x
+    | NMethod      n -> Printf.sprintf "Method %s" n
   in
   (pos,
     Printf.sprintf "%s is provided more than once" nn,
@@ -465,3 +478,10 @@ let redundant_named_pattern ~pos name =
     "Providing %s to a constructor that do not expect it"
     (string_of_name name),
     [])
+
+let invalid_whnf_form ~pos ~env tp =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "Got invalid whnf form when converting type %s"
+    (Pretty.type_to_string pp_ctx env tp)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])

src/TypeInference/Error.mli

@@ -35,6 +35,7 @@ val unbound_module : pos:Position.t -> S.module_name S.path -> t
 val unbound_the_effect : pos:Position.t -> t
 val unbound_named_param : pos:Position.t -> S.var -> t
 val unbound_the_label : pos:Position.t -> t
+val unbound_adt : pos:Position.t -> env:Env.t -> T.tvar -> t
 
 val unbound_method :
   pos:Position.t -> env:Env.t -> T.tvar -> S.method_name -> t
@@ -103,6 +104,7 @@ val non_polymorphic_pattern : pos:Position.t -> t
 
 val polymorphic_label : pos:Position.t -> t
 val label_type_mismatch : pos:Position.t -> t
+val polymorphic_optional_parameter : pos:Position.t -> t
 
 val label_pattern_type_mismatch : pos:Position.t -> env:Env.t -> T.typ -> t
 
@@ -139,3 +141,4 @@ val ctor_arity_mismatch :
 val redundant_named_type : pos:Position.t -> T.tname -> t
 val redundant_named_parameter : pos:Position.t -> T.name -> t
 val redundant_named_pattern : pos:Position.t -> T.name -> t
+val invalid_whnf_form : pos:Position.t -> env:Env.t -> T.typ -> t

src/TypeInference/ExprUtils.ml

@@ -155,6 +155,11 @@ and instantiate_named_param ~nset ~inst env (e : T.expr) (name, isch) =
   | None, T.NVar x ->
     (* TODO: we could provide freshly bound parameters here *)
     Error.fatal (Error.unbound_named_param ~pos:e.pos x)
+  | None, T.NOptionalVar x ->
+    assert (T.Scheme.is_monomorphic isch);
+    let arg = PreludeTypes.mk_None ~env ~pos:e.pos isch.sch_body in
+    { T.pos = e.pos; T.data = T.EApp(e, arg) }
+
 
 let instantiate_named_params env e ims inst =
   instantiate_named_params_loop ~nset:T.Name.Set.empty ~inst env e ims

src/TypeInference/ImplicitEnv.ml

@@ -120,7 +120,7 @@ let shadow_names ienv names =
   T.Name.Map.fold
     (fun name _ ienv ->
       match name with
-      | T.NLabel | T.NVar _ | T.NMethod _ -> ienv
+      | T.NLabel | T.NVar _ | T.NOptionalVar _ | T.NMethod _ -> ienv
       | T.NImplicit n -> shadow ienv n)
     names ienv
 

src/TypeInference/Name.ml

@@ -14,7 +14,8 @@ let tr_tname (name : S.tname) =
 
 let tr_name env (name : S.name) =
   match name with
-  | NLabel      -> T.NLabel
-  | NVar x      -> T.NVar x
-  | NImplicit n -> T.NImplicit n
-  | NMethod   n -> T.NMethod   n 
+  | NLabel         -> T.NLabel
+  | NVar x         -> T.NVar x
+  | NOptionalVar x -> T.NOptionalVar x
+  | NImplicit n    -> T.NImplicit n
+  | NMethod   n    -> T.NMethod   n 

src/TypeInference/Pattern.ml

@@ -84,7 +84,7 @@ let introduce_implicit_name ~pos env (name : T.name) sch =
     (* Do not introduce anything. Just create a fresh variable *)
     (env, T.Name.Map.empty, Var.fresh ~name:"label" ())
 
-  | NVar x ->
+  | NVar x | NOptionalVar x ->
     (* Do not introduce anything. Just create a fresh variable *)
     (env, T.Name.Map.empty, Var.fresh ~name:x ())
 
@@ -168,6 +168,7 @@ let open_named_arg ~pos ~public ~sub env (name, sch) =
     match name with
     | T.NLabel -> Env.add_the_label_sch env sch
     | T.NVar x -> Env.add_poly_var ~public env x sch
+    | T.NOptionalVar x -> Env.add_mono_var ~public env x sch.sch_body
     | T.NImplicit n -> Env.add_poly_implicit ~public env n sch ignore
     | T.NMethod   n ->
       let owner = TypeUtils.method_owner_of_scheme ~pos ~env sch in
@@ -330,6 +331,30 @@ and check_pattern_schemes ~env ~scope pats schs =
 
   | [], _ :: _ | _ :: _, [] -> assert false
 
+(** Infer type-scheme of given formal optional argument. Returns extended
+  environment, a pattern that represents an argument, its scheme, and the
+  effect of pattern-matching *)
+let infer_optional_arg_scheme env (arg : S.arg) =
+  match arg with
+  | ArgAnnot(pat, sch) ->
+    let sch_pos = sch.sch_pos in
+    let sch = Type.tr_scheme env sch in
+    if not (T.Scheme.is_monomorphic sch) then
+      Error.fatal (Error.polymorphic_optional_parameter ~pos:sch_pos);
+    let sch = T.Scheme.of_type 
+      (PreludeTypes.mk_Option ~env ~pos:sch_pos sch.sch_body)
+    in
+    let scope = Env.scope env in
+    let (env, pat, _, r_eff) =
+      check_scheme ~env ~scope pat sch in
+    (env, pat, sch, r_eff)
+  | ArgPattern pat ->
+    let tp = Env.fresh_uvar env T.Kind.k_type in
+    let tp = (PreludeTypes.mk_Option ~env ~pos:pat.pos tp) in
+    let scope = Env.scope env in
+    let (env, pat, _, r_eff) = check_type ~env ~scope pat tp in
+    (env, pat, T.Scheme.of_type tp, r_eff)
+
 let infer_arg_scheme env (arg : S.arg) =
   match arg with
   | ArgAnnot(pat, sch) ->
@@ -363,7 +388,12 @@ let check_arg_scheme env (arg : S.arg) sch =
 let infer_named_arg_scheme env (na : S.named_arg) =
   let (name, arg) = na.data in
   let name = Name.tr_name env name in
-  let (env, pat, sch, r_eff) = infer_arg_scheme env arg in
+  let (env, pat, sch, r_eff) = 
+    begin match name with
+    | NOptionalVar x -> infer_optional_arg_scheme env arg
+    | _ -> infer_arg_scheme env arg
+    end
+  in
   begin match name with
   | NLabel ->
     let { T.sch_targs; sch_named; sch_body } = sch in
@@ -376,7 +406,7 @@ let infer_named_arg_scheme env (na : S.named_arg) =
     | L_No ->
       Error.fatal (Error.label_type_mismatch ~pos:na.pos)
     end
-  | NVar _ | NImplicit _ | NMethod _ -> ()
+  | NVar _ | NOptionalVar _ | NImplicit _ | NMethod _ -> ()
   end;
   (env, (name, pat, sch), r_eff)