diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml index 9073427d..59df2bc1 100644 --- a/src/DblParser/Desugar.ml +++ b/src/DblParser/Desugar.ml @@ -632,11 +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)) - | NOptionalVar x -> Error.fatal (Error.desugar_error fld.pos) - | 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) -> diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly index c0ae1fa1..0f23327c 100644 --- a/src/DblParser/YaccParser.mly +++ b/src/DblParser/YaccParser.mly @@ -69,7 +69,7 @@ var_id name : KW_LABEL { NLabel } | LID { NVar $1 } -| QLID { NOptionalVar $1 } +| QLID { NOptionalVar $1 } | TLID { NImplicit $1 } | KW_METHOD LID { NMethod $2 } ; diff --git a/src/TypeInference/Pattern.ml b/src/TypeInference/Pattern.ml index f529fbe1..7cc5c978 100644 --- a/src/TypeInference/Pattern.ml +++ b/src/TypeInference/Pattern.ml @@ -331,25 +331,28 @@ 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 - assert (T.Scheme.is_monomorphic sch); - 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) + match arg with + | ArgAnnot(pat, sch) -> + let sch_pos = sch.sch_pos in + let sch = Type.tr_scheme env sch in + assert (T.Scheme.is_monomorphic sch); + 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 diff --git a/src/TypeInference/Pattern.mli b/src/TypeInference/Pattern.mli index 4e47bcf2..2dded9ca 100644 --- a/src/TypeInference/Pattern.mli +++ b/src/TypeInference/Pattern.mli @@ -23,12 +23,6 @@ val check_type : val infer_arg_scheme : Env.t -> S.arg -> Env.t * T.pattern * T.scheme * ret_effect -(** 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 *) -val infer_optional_arg_scheme : - Env.t -> S.arg -> Env.t * T.pattern * T.scheme * ret_effect - (** Check if given argument has given type scheme. Returns extended environment, translated argument as pattern, and the effect of pattern-matching *) diff --git a/src/TypeInference/PreludeTypes.ml b/src/TypeInference/PreludeTypes.ml index 51b6aed1..b165fbee 100644 --- a/src/TypeInference/PreludeTypes.ml +++ b/src/TypeInference/PreludeTypes.ml @@ -38,7 +38,7 @@ let mk_Some ~env ~pos tp_arg expr_arg : T.expr = let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in match List.find_index - (fun (ctor_decl : T.ctor_decl) -> String.compare ctor_decl.ctor_name "Some" == 0) + (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name = "Some") adt_ctors with | Some idx -> @@ -60,7 +60,7 @@ let mk_None ~env ~pos option_tp : T.expr = let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in match List.find_index - (fun (ctor_decl : T.ctor_decl) -> String.compare ctor_decl.ctor_name "None" == 0) + (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name = "None") adt_ctors with | Some idx -> diff --git a/src/TypeInference/TypeUtils.ml b/src/TypeInference/TypeUtils.ml index 279795e4..5a39191e 100644 --- a/src/TypeInference/TypeUtils.ml +++ b/src/TypeInference/TypeUtils.ml @@ -48,8 +48,7 @@ let open_scheme ~pos (env : Env.t) (sch : T.scheme) = let (env, x) = match name with | T.NLabel -> Env.add_the_label_sch env sch - | T.NVar x -> Env.add_poly_var env x sch - | T.NOptionalVar x -> Env.add_mono_var env x sch.sch_body + | T.NVar x | T.NOptionalVar x -> Env.add_poly_var env x sch | T.NImplicit n -> Env.add_poly_implicit env n sch ignore | T.NMethod n -> let owner = method_owner_of_scheme ~pos ~env sch in diff --git a/test/ok/ok0109_optionalParams.fram b/test/ok/ok0111_optionalParams.fram similarity index 62% rename from test/ok/ok0109_optionalParams.fram rename to test/ok/ok0111_optionalParams.fram index b5d19adc..0df5ea55 100644 --- a/test/ok/ok0109_optionalParams.fram +++ b/test/ok/ok0111_optionalParams.fram @@ -7,17 +7,18 @@ let a = f let b = f {x=2} let g {?x : Int} () = -match x with -| Some n => n + 2 -| None => 42 -end + match x with + | Some n => n + 2 + | None => 42 + end let c = g () let d = g {x=2} () let e = g {?x = Some 2} () -let h {?x} () = match x with -| Some n => n -| None => None -end +let h {?x} () = + match x with + | Some n => n + | None => None + end -let a = h {x=Some 2} \ No newline at end of file +let a = h {x=Some 2}