From 2b3225cc6603cbe9b58e189a6d84e52b5db9097e Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Wed, 8 Jan 2025 10:11:53 -0500 Subject: [PATCH] Track function argument types --- src/haz3lcore/dynamics/DHExp.re | 2 +- src/haz3lcore/dynamics/EvalCtx.re | 6 +- src/haz3lcore/dynamics/EvaluatorStep.re | 4 +- src/haz3lcore/dynamics/FilterMatcher.re | 2 +- src/haz3lcore/dynamics/Substitution.re | 6 +- src/haz3lcore/dynamics/Transition.re | 2 +- src/haz3lcore/dynamics/TypeAssignment.re | 9 ++- src/haz3lcore/dynamics/Unboxing.re | 4 +- src/haz3lcore/pretty/ExpToSegment.re | 7 +- src/haz3lcore/statics/Elaborator.re | 8 +- src/haz3lcore/statics/MakeTerm.re | 2 +- src/haz3lcore/statics/Mode.re | 16 ++-- src/haz3lcore/statics/Statics.re | 4 +- src/haz3lcore/statics/Term.re | 5 +- src/haz3lcore/statics/TermBase.re | 16 +++- src/haz3lmenhir/Conversion.re | 6 +- src/haz3lweb/app/explainthis/ExplainThis.re | 2 +- src/haz3lweb/exercises/SyntaxTest.re | 8 +- test/Test_Elaboration.re | 83 +++++---------------- test/Test_Evaluator.re | 5 +- test/Test_MakeTerm.re | 4 +- test/Test_Menhir.re | 5 +- test/Test_Statics.re | 4 + 23 files changed, 95 insertions(+), 115 deletions(-) diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re index d7cd9c7296..60ae666d2c 100644 --- a/src/haz3lcore/dynamics/DHExp.re +++ b/src/haz3lcore/dynamics/DHExp.re @@ -106,7 +106,7 @@ let rec strip_casts = let assign_name_if_none = (t, name) => { let (term, rewrap) = unwrap(t); switch (term) { - | Fun(arg, body, None) => Fun(arg, body, name) |> rewrap + | Fun(arg, body, typ, None) => Fun(arg, body, typ, name) |> rewrap | TypFun(utpat, body, None) => TypFun(utpat, body, name) |> rewrap | _ => t }; diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re index a2e62f4ab7..566cdea378 100644 --- a/src/haz3lcore/dynamics/EvalCtx.re +++ b/src/haz3lcore/dynamics/EvalCtx.re @@ -8,7 +8,7 @@ type term = | Seq2(DHExp.t, t) | Let1(Pat.t, t, DHExp.t) | Let2(Pat.t, DHExp.t, t) - | Fun(Pat.t, t, option(Var.t)) + | Fun(Pat.t, t, option(Typ.t), option(Var.t)) | FixF(Pat.t, t, option(ClosureEnvironment.t)) | TypAp(t, Typ.t) | Ap1(Operators.ap_direction, t, DHExp.t) @@ -124,9 +124,9 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => { | Let2(dp, d1, ctx) => let d = compose(ctx, d); Let(dp, d1, d) |> wrap; - | Fun(dp, ctx, v) => + | Fun(dp, ctx, typ, v) => let d = compose(ctx, d); - Fun(dp, d, v) |> wrap; + Fun(dp, d, typ, v) |> wrap; | FixF(v, ctx, env) => let d = compose(ctx, d); FixF(v, d, env) |> wrap; diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index 3f4c38f0f9..bbdbfaaf43 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -93,10 +93,10 @@ let rec matches = | Let2(d1, d2, ctx) => let+ ctx = matches(env, flt, ctx, exp, act, idx); Let2(d1, d2, ctx) |> rewrap; - | Fun(dp, ctx, name) => + | Fun(dp, ctx, ty, name) => // TODO: Should this env include the bound variables? let+ ctx = matches(env, flt, ctx, exp, act, idx); - Fun(dp, ctx, name) |> rewrap; + Fun(dp, ctx, ty, name) |> rewrap; | FixF(name, ctx, env') => let+ ctx = matches(Option.value(~default=env, env'), flt, ctx, exp, act, idx); diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d0c1f577f4..8b44dbf2e2 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -228,7 +228,7 @@ let rec matches_exp = | (TypFun(pat1, d1, s1), TypFun(pat2, d2, s2)) => s1 == s2 && matches_utpat(pat1, pat2) && matches_exp(d1, d2) | (TypFun(_), _) => false - | (Fun(dp1, d1, _), Fun(fp1, f1, _)) => + | (Fun(dp1, d1, _, _), Fun(fp1, f1, _, _)) => matches_fun(~denv, dp1, d1, ~fenv, fp1, f1) | (Fun(_), _) => false diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re index d342a4767c..ace08f335c 100644 --- a/src/haz3lcore/dynamics/Substitution.re +++ b/src/haz3lcore/dynamics/Substitution.re @@ -65,12 +65,12 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => { subst_var(m, d1, x, d3); }; FixF(y, d3, env') |> rewrap; - | Fun(dp, d3, s) => + | Fun(dp, d3, ty, s) => if (binds_var(m, x, dp)) { - Fun(dp, d3, s) |> rewrap; + Fun(dp, d3, ty, s) |> rewrap; } else { let d3 = subst_var(m, d1, x, d3); - Fun(dp, d3, s) |> rewrap; + Fun(dp, d3, ty, s) |> rewrap; } | TypFun(tpat, d3, s) => TypFun(tpat, subst_var(m, d1, x, d3), s) |> rewrap diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index fdee27c278..bea28dfd04 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -229,7 +229,7 @@ module Transition = (EV: EV_MODE) => { is_value: false, }); | TypFun(_) - | Fun(_, _, _) => + | Fun(_, _, _, _) => let. _ = otherwise(env, d); let.wrap_closure _ = env; Value; diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index 678a041e8c..6bd403a9c4 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -152,8 +152,13 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => }; let* ctx = dhpat_extend_ctx(dhp, ty_p, ctx); typ_of_dhexp(ctx, m, d); - | Fun(dhp, d, _) => - let* ty_p = dhpat_synthesize(dhp, ctx); + | Fun(dhp, d, ty, _) => + let* ty_p = + switch (ty) { + | None => dhpat_synthesize(dhp, ctx) + | Some(t) => Some(t) + }; + let* ctx = dhpat_extend_ctx(dhp, ty_p, ctx); let* ty2 = typ_of_dhexp(ctx, m, d); Some(Arrow(ty_p, ty2) |> Typ.temp); diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re index 0b763195d9..f3c16b94cd 100644 --- a/src/haz3lcore/dynamics/Unboxing.re +++ b/src/haz3lcore/dynamics/Unboxing.re @@ -150,7 +150,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = /* Function-like things can look like the following when values */ | (Fun, Constructor(name, _)) => Matches(Constructor(name)) // Perhaps we should check if the constructor actually is a function? - | (Fun, Closure(env', {term: Fun(dp, d3, _), _})) => + | (Fun, Closure(env', {term: Fun(dp, d3, _, _), _})) => Matches(FunEnv(dp, d3, env')) | ( Fun, @@ -221,7 +221,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = Invalid(_) | Undefined | EmptyHole | MultiHole(_) | DynamicErrorHole(_) | Var(_) | Let(_) | - Fun(_, _, _) | + Fun(_, _, _, _) | FixF(_) | TyAlias(_) | Ap(_) | diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re index 63744554f7..e35b9881fe 100644 --- a/src/haz3lcore/pretty/ExpToSegment.re +++ b/src/haz3lcore/pretty/ExpToSegment.re @@ -233,7 +233,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => { let id = exp |> Exp.rep_id; let+ es = es |> List.map(any_to_pretty(~settings)) |> all; ListUtil.flat_intersperse(Grout({id, shape: Concave}), es); - | Parens({term: Fun(p, e, _), _} as inner_exp) => + | Parens({term: Fun(p, e, _, _), _} as inner_exp) => // TODO: Add optional newlines let id = inner_exp |> Exp.rep_id; let+ p = pat_to_pretty(~settings: Settings.t, p) @@ -249,7 +249,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => { let fun_form = [mk_form("fun_", id, [p])] @ e; [mk_form("parens_exp", exp |> Exp.rep_id, [fun_form])] |> fold_fun_if(settings.fold_fn_bodies, name); - | Fun(p, e, _) => + | Fun(p, e, _, _) => // TODO: Add optional newlines let id = exp |> Exp.rep_id; let+ p = pat_to_pretty(~settings: Settings.t, p) @@ -850,10 +850,11 @@ let rec parenthesize = (~show_filters: bool, exp: Exp.t): Exp.t => { // Other forms | Constructor(c, t) => Constructor(c, paren_typ_at(Precedence.cast, t)) |> rewrap - | Fun(p, e, n) => + | Fun(p, e, typ, n) => Fun( parenthesize_pat(p) |> paren_pat_at(Precedence.min), parenthesize(e) |> paren_assoc_at(Precedence.fun_), + typ, // this typ is currently never output n, ) |> rewrap diff --git a/src/haz3lcore/statics/Elaborator.re b/src/haz3lcore/statics/Elaborator.re index 2ee7d0f723..ed2df96013 100644 --- a/src/haz3lcore/statics/Elaborator.re +++ b/src/haz3lcore/statics/Elaborator.re @@ -255,10 +255,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => { }; let t = t |> Typ.normalize(ctx) |> Typ.all_ids_temp; Constructor(c, t) |> rewrap |> cast_from(t); - | Fun(p, e, n) => + | Fun(p, e, _, n) => let (p', typ) = elaborate_pattern(m, p); let (e', tye) = elaborate(m, e); - Fun(p', e', n) |> rewrap |> cast_from(Arrow(typ, tye) |> Typ.temp); + Fun(p', e', Some(typ), n) + |> rewrap + |> cast_from(Arrow(typ, tye) |> Typ.temp); | TypFun(tpat, e, name) => let (e', tye) = elaborate(m, e); TypFun(tpat, e', name) @@ -281,7 +283,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => { (name, exp) => { let (term, rewrap) = DHExp.unwrap(exp); switch (term) { - | Fun(p, e, _) => Fun(p, e, name) |> rewrap + | Fun(p, e, t, _) => Fun(p, e, t, name) |> rewrap | TypFun(tpat, e, _) => TypFun(tpat, e, name) |> rewrap | _ => exp }; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 8ebd6836b8..9c28029e00 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -216,7 +216,7 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = { | (["$"], []) => UnOp(Meta(Unquote), r) | (["-"], []) => UnOp(Int(Minus), r) | (["!"], []) => UnOp(Bool(Not), r) - | (["fun", "->"], [Pat(pat)]) => Fun(pat, r, None) + | (["fun", "->"], [Pat(pat)]) => Fun(pat, r, None, None) | (["fix", "->"], [Pat(pat)]) => FixF(pat, r, None) | (["typfun", "->"], [TPat(tpat)]) => TypFun(tpat, r, None) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re index 7cb288e637..d87d0eb172 100644 --- a/src/haz3lcore/statics/Mode.re +++ b/src/haz3lcore/statics/Mode.re @@ -38,12 +38,16 @@ let ty_of: t => Typ.t = Forall(Var("syntypfun") |> TPat.fresh, Unknown(SynSwitch) |> Typ.temp) |> Typ.temp; /* TODO: naming the type variable? */ -let of_arrow = (ctx: Ctx.t, mode: t): (t, t) => - switch (mode) { - | Syn - | SynFun - | SynTypFun => (Syn, Syn) - | Ana(ty) => ty |> Typ.matched_arrow(ctx) |> TupleUtil.map2(ana) +// ty is Some if the expression is an annotated lambda +let of_arrow = (ctx: Ctx.t, mode: t, ty: option(Typ.t)): (t, t) => + switch (mode, ty) { + | (Syn | SynFun | SynTypFun, None) => (Syn, Syn) + | (Syn | SynFun | SynTypFun, Some(ty)) => (Ana(ty), Syn) + | (Ana(ty), None) => ty |> Typ.matched_arrow(ctx) |> TupleUtil.map2(ana) + | (Ana(ty), Some(ty')) => + let (t1, t2) = ty |> Typ.matched_arrow(ctx); + (Typ.join(~fix=true, ctx, t1, ty') |> Option.value(~default=ty'), t2) + |> TupleUtil.map2(ana); }; let of_forall = (ctx: Ctx.t, name_opt: option(string), mode: t): t => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index ffecf4f285..2fcec9964f 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -360,8 +360,8 @@ and uexp_to_info_map = let (args, m) = map_m_go(m, modes, args); let arg_co_ctx = CoCtx.union(List.map(Info.exp_co_ctx, args)); add'(~self, ~co_ctx=CoCtx.union([fn.co_ctx, arg_co_ctx]), m); - | Fun(p, e, _) => - let (mode_pat, mode_body) = Mode.of_arrow(ctx, mode); + | Fun(p, e, typ, _) => + let (mode_pat, mode_body) = Mode.of_arrow(ctx, mode, typ); let (p', _) = go_pat(~is_synswitch=false, ~co_ctx=CoCtx.empty, ~mode=mode_pat, p, m); let (e, m) = go'(~ctx=p'.ctx, ~mode=mode_body, e, m); diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index f022e8617a..f4013a3f25 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -618,7 +618,7 @@ module Exp = { new_bound_vars, e, ) - | Fun(p, e, n) => + | Fun(p, e, t, n) => let pat_bound_vars = Pat.bound_vars(p); Fun( p, @@ -628,6 +628,7 @@ module Exp = { pat_bound_vars @ new_bound_vars, e, ), + t, n, ) |> rewrap; @@ -742,7 +743,7 @@ module Exp = { let rec get_fn_name = (e: t) => { switch (e.term) { - | Fun(_, _, n) => n + | Fun(_, _, _, n) => n | FixF(_, e, _) => get_fn_name(e) | Parens(e) => get_fn_name(e) | TypFun(_, _, n) => n diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 544c7ebb48..88a0a3ac30 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -69,7 +69,7 @@ and exp_term = | String(string) | ListLit(list(exp_t)) | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic expressions - | Fun(pat_t, exp_t, option(Var.t)) + | Fun(pat_t, exp_t, option(typ_t), option(Var.t)) // typ_t field is only used to display types in results | TypFun(tpat_t, exp_t, option(Var.t)) | Tuple(list(exp_t)) | Var(Var.t) @@ -304,7 +304,13 @@ and Exp: { | FailedCast(e, t1, t2) => FailedCast(exp_map_term(e), typ_map_term(t1), typ_map_term(t2)) | ListLit(ts) => ListLit(List.map(exp_map_term, ts)) - | Fun(p, e, f) => Fun(pat_map_term(p), exp_map_term(e), f) + | Fun(p, e, t, f) => + Fun( + pat_map_term(p), + exp_map_term(e), + Option.map(typ_map_term, t), + f, + ) | TypFun(tp, e, f) => TypFun(tpat_map_term(tp), exp_map_term(e), f) | Tuple(xs) => Tuple(List.map(exp_map_term, xs)) | Let(p, e1, e2) => @@ -369,8 +375,10 @@ and Exp: { List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys) | (Constructor(c1, ty1), Constructor(c2, ty2)) => c1 == c2 && Typ.fast_equal(ty1, ty2) - | (Fun(p1, e1, _), Fun(p2, e2, _)) => - Pat.fast_equal(p1, p2) && fast_equal(e1, e2) + | (Fun(p1, e1, t1, _), Fun(p2, e2, t2, _)) => + Pat.fast_equal(p1, p2) + && fast_equal(e1, e2) + && Option.equal(Typ.fast_equal, t1, t2) | (TypFun(tp1, e1, _), TypFun(tp2, e2, _)) => TPat.fast_equal(tp1, tp2) && fast_equal(e1, e2) | (Tuple(xs), Tuple(ys)) => diff --git a/src/haz3lmenhir/Conversion.re b/src/haz3lmenhir/Conversion.re index b06f1e4725..1941e4be0f 100644 --- a/src/haz3lmenhir/Conversion.re +++ b/src/haz3lmenhir/Conversion.re @@ -225,8 +225,8 @@ module rec Exp: { | Fun(p, e, name_opt) => switch (name_opt) { | Some(name_str) => - Fun(Pat.of_menhir_ast(p), of_menhir_ast(e), Some(name_str)) - | None => Fun(Pat.of_menhir_ast(p), of_menhir_ast(e), None) + Fun(Pat.of_menhir_ast(p), of_menhir_ast(e), None, Some(name_str)) + | None => Fun(Pat.of_menhir_ast(p), of_menhir_ast(e), None, None) } | ApExp(e1, args) => switch (args) { @@ -350,7 +350,7 @@ module rec Exp: { | Constructor(s, typ) => Constructor(s, Typ.of_core(typ)) | DeferredAp(e, es) => ApExp(of_core(e), TupleExp(List.map(of_core, es))) - | Fun(p, e, name_opt) => Fun(Pat.of_core(p), of_core(e), name_opt) + | Fun(p, e, _, name_opt) => Fun(Pat.of_core(p), of_core(e), name_opt) | Ap(Reverse, _, _) => raise(Failure("Reverse not supported")) }; }; diff --git a/src/haz3lweb/app/explainthis/ExplainThis.re b/src/haz3lweb/app/explainthis/ExplainThis.re index ea83170f66..3388bbb3ba 100644 --- a/src/haz3lweb/app/explainthis/ExplainThis.re +++ b/src/haz3lweb/app/explainthis/ExplainThis.re @@ -608,7 +608,7 @@ let get_doc = }; /* TODO: More could be done here probably for different patterns. */ basic(TypFunctionExp.type_functions_basic); - | Fun(pat, body, _) => + | Fun(pat, body, _, _) => let basic = group_id => { let pat_id = List.nth(pat.ids, 0); let body_id = List.nth(body.ids, 0); diff --git a/src/haz3lweb/exercises/SyntaxTest.re b/src/haz3lweb/exercises/SyntaxTest.re index da71ab1760..9465ac6abf 100644 --- a/src/haz3lweb/exercises/SyntaxTest.re +++ b/src/haz3lweb/exercises/SyntaxTest.re @@ -88,7 +88,7 @@ let rec find_fn = (name: string, uexp: Exp.t, l: list(Exp.t)): list(Exp.t) => { List.fold_left((acc, u1) => {find_fn(name, u1, acc)}, l, ul) | TypFun(_, body, _) | FixF(_, body, _) - | Fun(_, body, _) => l |> find_fn(name, body) + | Fun(_, body, _, _) => l |> find_fn(name, body) | TypAp(u1, _) | Parens(u1) | Cast(u1, _, _) @@ -178,7 +178,7 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => { | Constructor(_) | Undefined | Deferral(_) => false - | Fun(args, body, _) => + | Fun(args, body, _, _) => var_mention_upat(name, args) ? false : var_mention(name, body) | ListLit(l) | Tuple(l) => @@ -239,7 +239,7 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => { | Constructor(_) | Undefined | Deferral(_) => false - | Fun(args, body, _) + | Fun(args, body, _, _) | FixF(args, body, _) => var_mention_upat(name, args) ? false : var_applied(name, body) | ListLit(l) @@ -332,7 +332,7 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => { | Var(_) | BuiltinFun(_) => true | FixF(args, body, _) - | Fun(args, body, _) => + | Fun(args, body, _, _) => var_mention_upat(name, args) ? false : tail_check(name, body) | Let(p, def, body) => var_mention_upat(name, p) || var_mention(name, def) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 454dfa1e40..7c461c5140 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -87,15 +87,28 @@ module PlainTests = { BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, None, + None, + ) + |> Exp.fresh; + + let f' = + Fun( + Var("x") |> Pat.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + Some(Unknown(Hole(EmptyHole)) |> Typ.fresh), + None, ) |> Exp.fresh; let unapplied_function = () => - alco_check("A function", f, dhexp_of_uexp(f)); + alco_check("A function", f', dhexp_of_uexp(f)); let u7: Exp.t = Ap(Forward, f, Var("y") |> Exp.fresh) |> Exp.fresh; + let d7: Exp.t = Ap(Forward, f', Var("y") |> Exp.fresh) |> Exp.fresh; + let ap_fun = () => - alco_check("Application of a function", u7, dhexp_of_uexp(u7)); + alco_check("Application of a function", d7, dhexp_of_uexp(u7)); let u8: Exp.t = Match( @@ -155,6 +168,7 @@ module PlainTests = { BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x") |> Exp.fresh) |> Exp.fresh, None, + None, ) |> Exp.fresh, Int(55) |> Exp.fresh, @@ -168,6 +182,7 @@ module PlainTests = { Var("x") |> Pat.fresh, BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x") |> Exp.fresh) |> Exp.fresh, + Some(Int |> Typ.fresh), Some("f"), ) |> Exp.fresh, @@ -364,40 +379,6 @@ module MenhirElaborationTests = { dhexp_of_uexp(uexp), ); - //Test for a let function - let let_fun_uexp: Exp.t = - Let( - Cast( - Var("f") |> Pat.fresh, - Arrow(Int |> Typ.fresh, Int |> Typ.fresh) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, - ) - |> Pat.fresh, - Fun( - Var("x") |> Pat.fresh, - BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x") |> Exp.fresh) - |> Exp.fresh, - None, - ) - |> Exp.fresh, - Int(55) |> Exp.fresh, - ) - |> Exp.fresh; - - let let_fun_str = " -let f = - named_fun f x -> - 1 + x - in -55"; - - let let_fun_menhir = () => - alco_check_menhir( - "Let expression for a function which is not recursive (menhir)", - let_fun_str, - let_fun_uexp, - ); - //Test for an empty hole let empty_hole_str = "?"; let empty_hole_uexp: Exp.t = { @@ -459,30 +440,6 @@ let f = inconsistent_case_uexp, ); - //Function free var application menhir test - let ap_fun_uexp: Exp.t = - Ap( - Forward, - Fun( - Var("x") |> Pat.fresh, - BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) - |> Exp.fresh, - None, - ) - |> Exp.fresh, - Var("y") |> Exp.fresh, - ) - |> Exp.fresh; - let ap_fun_str = " - (fun x -> 4 + 5)(y) -"; - let ap_fun_menhir = () => - alco_check_menhir( - "Application of a function (menhir)", - ap_fun_str, - dhexp_of_uexp(ap_fun_uexp), - ); - //Consistent if statement menhir test let consistent_if_uexp: Exp.t = If(Bool(false) |> Exp.fresh, Int(8) |> Exp.fresh, Int(6) |> Exp.fresh) @@ -732,16 +689,10 @@ x test_case("Type ap test (menhir)", `Quick, typ_ap_menhir), test_case("Let expression for a tuple (menhir)", `Quick, let_exp_menhir), test_case("Single integer (menhir)", `Quick, single_integer_menhir), - test_case( - "Let expression for a function (menhir)", - `Quick, - let_fun_menhir, - ), test_case("Empty hole (menhir)", `Quick, empty_hole_menhir), test_case("Free var (menhir)", `Quick, free_var_menhir), test_case("Bin op (menhir)", `Quick, bin_op_menhir), test_case("Inconsistent case (menhir)", `Quick, inconsistent_case_menhir), - test_case("ap fun (menhir)", `Quick, ap_fun_menhir), test_case("Consistent if (menhir)", `Quick, consistent_if_menhir), test_case("Undefined test (menhir)", `Quick, undefined_menhir), test_case("List exp (menhir)", `Quick, list_exp_menhir), diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index 6bfc2b42e9..a1afdaf510 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -171,7 +171,7 @@ let test_variable_capture = () => Int(5) |> Exp.fresh, Let( Var("f") |> Pat.fresh, - Fun(Tuple([]) |> Pat.fresh, Var("u") |> Exp.fresh, None) + Fun(Tuple([]) |> Pat.fresh, Var("u") |> Exp.fresh, None, None) |> Exp.fresh, Let( Var("u") |> Pat.fresh, @@ -192,7 +192,8 @@ let test_unbound_lookup = () => Var("x") |> Exp.fresh, Ap( Forward, - Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None) |> Exp.fresh, + Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None) + |> Exp.fresh, Var("x") |> Exp.fresh, ) |> Exp.fresh, diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index 9acbe0ec98..003ce7ca65 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -49,7 +49,7 @@ let tests = ( exp_check( Let( Var("f") |> Pat.fresh, - Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None) // It seems as though the function naming happens during elaboration and not during parsing + Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None) // It seems as though the function naming happens during elaboration and not during parsing |> Exp.fresh, Int(1) |> Exp.fresh, ) @@ -61,7 +61,7 @@ let tests = ( exp_check( Let( EmptyHole |> Pat.fresh, - Fun(Var("x") |> Pat.fresh, EmptyHole |> Exp.fresh, None) + Fun(Var("x") |> Pat.fresh, EmptyHole |> Exp.fresh, None, None) |> Exp.fresh, EmptyHole |> Exp.fresh, ) diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re index 66a1501110..94ce4edffa 100644 --- a/test/Test_Menhir.re +++ b/test/Test_Menhir.re @@ -175,7 +175,8 @@ let tests = ( full_parser_test("Integer Literal", Int(8) |> Exp.fresh, "8"), full_parser_test( "Fun", - Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None) |> Exp.fresh, + Fun(Var("x") |> Pat.fresh, Var("x") |> Exp.fresh, None, None) + |> Exp.fresh, "fun x -> x", ), full_parser_test( @@ -430,6 +431,7 @@ let tests = ( (Var("x"): Pat.term) |> Pat.fresh, BinOp(Int(Plus), Var("x") |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, + None, Some("f"), ) |> Exp.fresh, @@ -483,6 +485,7 @@ let tests = ( |> Pat.fresh, EmptyHole |> Exp.fresh, None, + None, ) |> Exp.fresh, "fun (b : ? -> ?) -> ?", diff --git a/test/Test_Statics.re b/test/Test_Statics.re index 8ea3dc7748..7bbf7db481 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -34,6 +34,7 @@ let unapplied_function = () => BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, None, + None, ) |> Exp.fresh, ), @@ -52,6 +53,7 @@ let tests = ( BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, None, + None, ) |> Exp.fresh, ), @@ -67,6 +69,7 @@ let tests = ( BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, None, + None, ) |> Exp.fresh, ), @@ -88,6 +91,7 @@ let tests = ( BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh) |> Exp.fresh, None, + None, ) |> Exp.fresh, ),