diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 6202d262f0..4dbde7a143 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -219,6 +219,7 @@ type pat = { status: status_pat, ty: Typ.t, constraint_: Constraint.t, + lifted_ty: option(Typ.t) /* Type static-level elaboration */ }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -669,6 +670,7 @@ let derived_pat = ~ancestors, ~self, ~constraint_, + ~lifted_ty: option(Typ.t), ) : pat => { let cls = Cls.Pat(UPat.cls_of_term(upat.term)); @@ -687,6 +689,7 @@ let derived_pat = ancestors, term: upat, constraint_, + lifted_ty, }; }; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index dc7b8b809e..e2f39597d2 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -234,7 +234,6 @@ and uexp_to_info_map = ); let go_pat = upat_to_info_map(~ctx, ~ancestors); let elaborate_singleton_tuple = (uexp: Exp.t, inner_ty, l, m) => { - print_endline("Elaborating singleton tuple"); let (term, rewrap) = UExp.unwrap(uexp); let original_expression = Exp.fresh(term); let (original_info, m) = @@ -752,6 +751,7 @@ and uexp_to_info_map = // Mark patterns as redundant at the top level // because redundancy doesn't make sense in a smaller context ~constraint_=p_constraint, + ~lifted_ty=None, ); ( // Override the info for the single upat @@ -882,7 +882,7 @@ and upat_to_info_map = m: Map.t, ) : (Info.pat, Map.t) => { - let add = (~self, ~ctx, ~constraint_, m) => { + let add = (~self, ~ctx, ~constraint_, ~lifted_ty=?, m) => { let prev_synswitch = switch (Id.Map.find_opt(Pat.rep_id(upat), m)) { | Some(Info.InfoPat({mode: Syn | SynFun, ty, _})) => Some(ty) @@ -900,6 +900,7 @@ and upat_to_info_map = ~ancestors, ~self=Common(self), ~constraint_, + ~lifted_ty, ); (info, add_info(ids, InfoPat(info), m)); }; @@ -942,122 +943,186 @@ and upat_to_info_map = (ctx, [], [], m), ); let hole = self => atomic(self, Constraint.Hole); - switch (term) { - | MultiHole(tms) => - let (_, m) = multi(~ctx, ~ancestors, m, tms); - add(~self=IsMulti, ~ctx, ~constraint_=Constraint.Hole, m); - | Invalid(token) => hole(BadToken(token)) - | EmptyHole => hole(Just(unknown)) - | Int(int) => atomic(Just(Int |> Typ.temp), Constraint.Int(int)) - | Float(float) => - atomic(Just(Float |> Typ.temp), Constraint.Float(float)) - | Tuple([]) => atomic(Just(Prod([]) |> Typ.temp), Constraint.Truth) - | Bool(bool) => - atomic( - Just(Bool |> Typ.temp), - bool - ? Constraint.InjL(Constraint.Truth) - : Constraint.InjR(Constraint.Truth), - ) - | String(string) => - atomic(Just(String |> Typ.temp), Constraint.String(string)) - | Label(name) => atomic(Just(Label(name) |> Typ.temp), Constraint.Truth) - | ListLit(ps) => - let ids = List.map(UPat.rep_id, ps); - let modes = Mode.of_list_lit(ctx, List.length(ps), mode); - let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); - let rec cons_fold_list = cs => - switch (cs) { - | [] => Constraint.InjL(Constraint.Truth) // Left = nil, Right = cons - | [hd, ...tl] => - Constraint.InjR(Constraint.Pair(hd, cons_fold_list(tl))) - }; - add( - ~self=Self.listlit(~empty=unknown, ctx, tys, ids), - ~ctx, - ~constraint_=cons_fold_list(cons), - m, - ); - | Cons(hd, tl) => - let (hd, m) = go(~ctx, ~mode=Mode.of_cons_hd(ctx, mode), hd, m); - let (tl, m) = - go(~ctx=hd.ctx, ~mode=Mode.of_cons_tl(ctx, mode, hd.ty), tl, m); - add( - ~self=Just(List(hd.ty) |> Typ.temp), - ~ctx=tl.ctx, - ~constraint_= - Constraint.InjR(Constraint.Pair(hd.constraint_, tl.constraint_)), - m, - ); - | Wild => atomic(Just(unknown), Constraint.Truth) - | Var(name) => - /* NOTE: The self type assigned to pattern variables (Unknown) - may be SynSwitch, but SynSwitch is never added to the context; - Unknown(Internal) is used in this case */ - let ctx_typ = - Info.fixed_typ_pat( - ctx, - mode, - Common(Just(Unknown(Internal) |> Typ.temp)), + let elaborate_singleton_tuple = (upat: Pat.t, inner_ty, l, m) => { + print_endline("elaborating singleton tuple: " ++ Pat.show(upat)); + let (term, rewrap) = UPat.unwrap(upat); + let original_expression = Pat.fresh(term); + let (original_info, m) = + upat_to_info_map( + ~ctx, + ~co_ctx, + ~is_synswitch, + ~ancestors, + ~mode=Mode.Ana(inner_ty), + original_expression, + m, ); - let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ}); - add( - ~self=Just(unknown), - ~ctx=Ctx.extend(ctx, entry), - ~constraint_=Constraint.Truth, - m, - ); - | TupLabel(label, p) => - let (labmode, mode) = Mode.of_label(ctx, mode); - let (lab, m) = go(~ctx, ~mode=labmode, label, m); - let (p, m) = go(~ctx, ~mode, p, m); - add( - ~self=Just(TupLabel(lab.ty, p.ty) |> Typ.temp), - ~ctx=p.ctx, - ~constraint_=Constraint.TupLabel(lab.constraint_, p.constraint_), - m, - ); - | Tuple(ps) => - let (ps, modes) = - Mode.of_prod(ctx, mode, ps, UPat.get_label, (name, b) => - TupLabel(Label(name) |> UPat.fresh, b) |> UPat.fresh + let elaborated_pat = + rewrap( + Tuple([ + TupLabel(Label(l) |> Pat.fresh, original_expression) |> Pat.fresh, + ]), + ); + let (info, m) = + upat_to_info_map( + ~ctx, + ~co_ctx, + ~is_synswitch, + ~ancestors, + ~mode, + elaborated_pat, + m, ); - let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); - let rec cons_fold_tuple = cs => - switch (cs) { - | [] => Constraint.Truth - | [elt] => elt - | [hd, ...tl] => Constraint.Pair(hd, cons_fold_tuple(tl)) + + // We need to keep the original status of the expression to get error messages on the unelaborated expression + let info = { + ...info, + status: original_info.status, + lifted_ty: Some(info.ty), + }; + + (info, add_info(elaborated_pat.ids, InfoPat(info), m)); + }; + + let default_case = () => + switch (term) { + | MultiHole(tms) => + let (_, m) = multi(~ctx, ~ancestors, m, tms); + add(~self=IsMulti, ~ctx, ~constraint_=Constraint.Hole, m); + | Invalid(token) => hole(BadToken(token)) + | EmptyHole => hole(Just(unknown)) + | Int(int) => atomic(Just(Int |> Typ.temp), Constraint.Int(int)) + | Float(float) => + atomic(Just(Float |> Typ.temp), Constraint.Float(float)) + | Tuple([]) => atomic(Just(Prod([]) |> Typ.temp), Constraint.Truth) + | Bool(bool) => + atomic( + Just(Bool |> Typ.temp), + bool + ? Constraint.InjL(Constraint.Truth) + : Constraint.InjR(Constraint.Truth), + ) + | String(string) => + atomic(Just(String |> Typ.temp), Constraint.String(string)) + | Label(name) => + atomic(Just(Label(name) |> Typ.temp), Constraint.Truth) + | ListLit(ps) => + let ids = List.map(UPat.rep_id, ps); + let modes = Mode.of_list_lit(ctx, List.length(ps), mode); + let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); + let rec cons_fold_list = cs => + switch (cs) { + | [] => Constraint.InjL(Constraint.Truth) // Left = nil, Right = cons + | [hd, ...tl] => + Constraint.InjR(Constraint.Pair(hd, cons_fold_list(tl))) + }; + add( + ~self=Self.listlit(~empty=unknown, ctx, tys, ids), + ~ctx, + ~constraint_=cons_fold_list(cons), + m, + ); + | Cons(hd, tl) => + let (hd, m) = go(~ctx, ~mode=Mode.of_cons_hd(ctx, mode), hd, m); + let (tl, m) = + go(~ctx=hd.ctx, ~mode=Mode.of_cons_tl(ctx, mode, hd.ty), tl, m); + add( + ~self=Just(List(hd.ty) |> Typ.temp), + ~ctx=tl.ctx, + ~constraint_= + Constraint.InjR(Constraint.Pair(hd.constraint_, tl.constraint_)), + m, + ); + | Wild => atomic(Just(unknown), Constraint.Truth) + | Var(name) => + /* NOTE: The self type assigned to pattern variables (Unknown) + may be SynSwitch, but SynSwitch is never added to the context; + Unknown(Internal) is used in this case */ + let ctx_typ = + Info.fixed_typ_pat( + ctx, + mode, + Common(Just(Unknown(Internal) |> Typ.temp)), + ); + let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ}); + add( + ~self=Just(unknown), + ~ctx=Ctx.extend(ctx, entry), + ~constraint_=Constraint.Truth, + m, + ); + | TupLabel(label, p) => + let (labmode, mode) = Mode.of_label(ctx, mode); + let (lab, m) = go(~ctx, ~mode=labmode, label, m); + let (p, m) = go(~ctx, ~mode, p, m); + add( + ~self=Just(TupLabel(lab.ty, p.ty) |> Typ.temp), + ~ctx=p.ctx, + ~constraint_=Constraint.TupLabel(lab.constraint_, p.constraint_), + m, + ); + | Tuple(ps) => + let (ps, modes) = + Mode.of_prod(ctx, mode, ps, UPat.get_label, (name, b) => + TupLabel(Label(name) |> UPat.fresh, b) |> UPat.fresh + ); + let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); + let rec cons_fold_tuple = cs => + switch (cs) { + | [] => Constraint.Truth + | [elt] => elt + | [hd, ...tl] => Constraint.Pair(hd, cons_fold_tuple(tl)) + }; + add( + ~self=Just(Prod(tys) |> Typ.temp), + ~ctx, + ~constraint_=cons_fold_tuple(cons), + m, + ); + | Parens(p) => + let (p, m) = go(~ctx, ~mode, p, m); + add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m); + | Constructor(ctr, _) => + let self = Self.of_ctr(ctx, ctr); + atomic(self, Constraint.of_ctr(ctx, mode, ctr, self)); + | Ap(fn, arg) => + let ctr = UPat.ctr_name(fn); + let fn_mode = Mode.of_ap(ctx, mode, ctr); + let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m); + let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty); + let (arg, m) = go(~ctx, ~mode=Ana(ty_in), arg, m); + add( + ~self=Just(ty_out), + ~ctx=arg.ctx, + ~constraint_= + Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)), + m, + ); + | Cast(p, ann, _) => + let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m); + let (p, m) = go(~ctx, ~mode=Ana(ann.term), p, m); + add(~self=Just(ann.term), ~ctx=p.ctx, ~constraint_=p.constraint_, m); + }; + // This is to allow lifting single values into a singleton labeled tuple when the label is not present + + print_endline("upat_to_info_map: " ++ UPat.show(upat)); + print_endline("mode: " ++ Mode.show(mode)); + switch (mode) { + | Ana(ty) => + switch (Typ.weak_head_normalize(ctx, ty).term) { + | Prod([{term: TupLabel({term: Label(l1), _}, ana_ty), _}]) => + // We can flatten this by pulling it up on the case match but since OCaml is strict it'll be evaluated. + // So for performance reasons we'll just do it here. + let (e, m) = go(~mode=Mode.Syn, ~ctx, upat, m); + + switch (Typ.weak_head_normalize(ctx, e.ty).term) { + | Prod([{term: TupLabel({term: Label(l2), _}, _), _}]) when l1 == l2 => + default_case() + | _ => elaborate_singleton_tuple(upat, ana_ty, l1, m) }; - add( - ~self=Just(Prod(tys) |> Typ.temp), - ~ctx, - ~constraint_=cons_fold_tuple(cons), - m, - ); - | Parens(p) => - let (p, m) = go(~ctx, ~mode, p, m); - add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m); - | Constructor(ctr, _) => - let self = Self.of_ctr(ctx, ctr); - atomic(self, Constraint.of_ctr(ctx, mode, ctr, self)); - | Ap(fn, arg) => - let ctr = UPat.ctr_name(fn); - let fn_mode = Mode.of_ap(ctx, mode, ctr); - let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m); - let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty); - let (arg, m) = go(~ctx, ~mode=Ana(ty_in), arg, m); - add( - ~self=Just(ty_out), - ~ctx=arg.ctx, - ~constraint_= - Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)), - m, - ); - | Cast(p, ann, _) => - let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m); - let (p, m) = go(~ctx, ~mode=Ana(ann.term), p, m); - add(~self=Just(ann.term), ~ctx=p.ctx, ~constraint_=p.constraint_, m); + | _ => default_case() + } + | _ => default_case() }; } and utyp_to_info_map = diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index 23aaf3cd77..58f4a46fec 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -11,7 +11,11 @@ let evaluation_test = (msg, expected, unevaluated) => snd(Evaluator.evaluate(Builtins.env_init, {d: unevaluated})), ), ); - +let parse_exp = (s: string) => + MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; +let dhexp_of_uexp = u => + Elaborator.elaborate(Statics.mk(CoreSettings.on, Builtins.ctx_init, u), u) + |> fst; let test_int = () => evaluation_test("8", Int(8) |> Exp.fresh, Int(8) |> Exp.fresh); @@ -196,4 +200,24 @@ let tests = [ test_case("Function application", `Quick, test_function_application), test_case("Function deferral", `Quick, test_function_deferral), test_case("Deferral applied to hole", `Quick, tet_ap_of_hole_deferral), + test_case("Elaborated Pattern for labeled tuple", `Quick, () => + check( + dhexp_typ, + {|let x : (a=Int) -> Int = fun a -> a in x(2)|}, + Int(2) |> Exp.fresh, + Evaluator.Result.unbox( + snd( + Evaluator.evaluate( + Builtins.env_init, + { + d: + dhexp_of_uexp( + parse_exp("let x : (a=Int) -> Int = fun a -> a in x(2)"), + ), + }, + ), + ), + ), + ) + ), ]; diff --git a/test/Test_Statics.re b/test/Test_Statics.re index f1eedd487a..59ba23283e 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -677,4 +677,10 @@ let tests = ) |> Exp.fresh, ), + fully_consistent_typecheck( + "Singleton labeled argument not labeled in pattern", + {|let x : (a=Int) -> Int = fun a -> a in x(2)|}, + Some(int), + parse_exp("let x : (a=Int) -> Int = fun a -> a in x(2)"), + ), ]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 15c226f73d..b9cbea0c0a 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -5,12 +5,12 @@ let (suite, _) = ~and_exit=false, "HazelTests", [ - ("Elaboration", Test_Elaboration.elaboration_tests), + ("MakeTerm", Test_MakeTerm.tests), ("LabeledTuple", Test_LabeledTuple.tests), ("Statics", Test_Statics.tests), + ("Elaboration", Test_Elaboration.elaboration_tests), ("Evaluator", Test_Evaluator.tests), Test_ListUtil.tests, - ("MakeTerm", Test_MakeTerm.tests), ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml");