From 9e5570a352f7ba08ea2d02078a124e40822f421e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 1 Oct 2024 13:25:55 -0400 Subject: [PATCH 01/10] Potentially fix deferrals --- src/haz3lcore/dynamics/Elaborator.re | 5 +++ src/haz3lcore/dynamics/Transition.re | 21 ++++++++----- test/Test_Evaluator.re | 46 ++++++++++++++++++---------- 3 files changed, 48 insertions(+), 24 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index c1f3aa12d7..0f2287bef4 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -350,6 +350,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { ((arg, _)) => Exp.is_deferral(arg), List.combine(args, ty_fargs), ); + // TODO Should this be a product in the singleton case or not + // let remaining_arg_ty = + // List.length(remaining_args) == 1 + // ? snd(List.hd(remaining_args)) + // : Prod(List.map(snd, remaining_args)) |> Typ.temp; let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp; DeferredAp(f'', args'') |> rewrap diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index a54c9d18d8..6a17a78d2f 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -333,9 +333,10 @@ module Transition = (EV: EV_MODE) => { ); Constructor; | Ap(dir, d1, d2) => + // TODO I don't know why this needs to be final let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = - req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) + req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) and. (d2', d2_is_value) = req_final_or_value( req(state, env), @@ -396,14 +397,22 @@ module Transition = (EV: EV_MODE) => { | DeferredAp(d3, d4s) => let n_args = List.length( - List.map( + List.filter( fun | {term: Deferral(_), _} => true | _ => false: Exp.t => bool, d4s, ), ); - let-unbox args = (Tuple(n_args), d2); + let-unbox args = + if (n_args == 1) { + ( + Tuple(n_args), + Tuple([d2]) |> fresh // TODO Should we not be going to a tuple? + ); + } else { + (Tuple(n_args), d2); + }; let new_args = { let rec go = (deferred, args) => switch ((deferred: list(Exp.t))) { @@ -424,11 +433,7 @@ module Transition = (EV: EV_MODE) => { }); | Cast(_) | FailedCast(_) => Indet - | FixF(_) => - print_endline(Exp.show(d1)); - print_endline(Exp.show(d1')); - print_endline("FIXF"); - failwith("FixF in Ap"); + | FixF(_) => failwith("FixF in Ap") | _ => Step({ expr: { diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index fc159425b2..c6417b5737 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -2,22 +2,6 @@ open Alcotest; open Haz3lcore; let dhexp_typ = testable(Fmt.using(Exp.show, Fmt.string), DHExp.fast_equal); -let ids = List.init(12, _ => Id.mk()); -let id_at = x => x |> List.nth(ids); -let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init); - -// Get the type from the statics -let type_of = f => { - let s = statics(f); - switch (Id.Map.find(IdTagged.rep_id(f), s)) { - | InfoExp({ty, _}) => Some(ty) - | _ => None - }; -}; - -let int_evaluation = - Evaluator.evaluate(Builtins.env_init, {d: Exp.Int(8) |> Exp.fresh}); - let evaluation_test = (msg, expected, unevaluated) => check( dhexp_typ, @@ -38,7 +22,37 @@ let test_sum = () => BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, ); +let test_function_application = () => + evaluation_test( + "float_of_int(1)", + Float(1.0) |> Exp.fresh, + Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh) + |> Exp.fresh, + ); + +let test_function_deferral = () => + evaluation_test( + "string_sub(\"hello\", 1, _)(2)", + String("el") |> Exp.fresh, + Ap( + Forward, + DeferredAp( + Var("string_sub") |> Exp.fresh, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, + Int(2) |> Exp.fresh, + ) + |> Exp.fresh, + ); + let tests = [ test_case("Integer literal", `Quick, test_int), test_case("Integer sum", `Quick, test_sum), + test_case("Function application", `Quick, test_function_application), + test_case("Function deferral", `Quick, test_function_deferral), ]; From 50440ea2ab3d92f4790b8f8711d9bfc9a31122de Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 2 Oct 2024 09:33:19 -0400 Subject: [PATCH 02/10] Fix function deferral for when there's a single remaining argument --- src/haz3lcore/dynamics/Elaborator.re | 10 +++---- src/haz3lcore/dynamics/Transition.re | 7 +++-- test/Test_Elaboration.re | 40 +++++++++++++++++++++++++++- 3 files changed, 48 insertions(+), 9 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 0f2287bef4..bdc5baf621 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -350,12 +350,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { ((arg, _)) => Exp.is_deferral(arg), List.combine(args, ty_fargs), ); - // TODO Should this be a product in the singleton case or not - // let remaining_arg_ty = - // List.length(remaining_args) == 1 - // ? snd(List.hd(remaining_args)) - // : Prod(List.map(snd, remaining_args)) |> Typ.temp; - let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp; + let remaining_arg_ty = + List.length(remaining_args) == 1 + ? snd(List.hd(remaining_args)) + : Prod(List.map(snd, remaining_args)) |> Typ.temp; DeferredAp(f'', args'') |> rewrap |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp); diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 6a17a78d2f..e0c278d2b7 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -333,7 +333,6 @@ module Transition = (EV: EV_MODE) => { ); Constructor; | Ap(dir, d1, d2) => - // TODO I don't know why this needs to be final let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) @@ -433,7 +432,11 @@ module Transition = (EV: EV_MODE) => { }); | Cast(_) | FailedCast(_) => Indet - | FixF(_) => failwith("FixF in Ap") + | FixF(_) => + print_endline(Exp.show(d1)); + print_endline(Exp.show(d1')); + print_endline("FIXF"); + failwith("FixF in Ap"); | _ => Step({ expr: { diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 2516f25227..d5d25d9334 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -180,6 +180,15 @@ let let_fun = () => let deferral = () => alco_check( "string_sub(\"hello\", 1, _)", + DeferredAp( + Var("string_sub") |> Exp.fresh, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, dhexp_of_uexp( DeferredAp( Var("string_sub") |> Exp.fresh, @@ -191,7 +200,13 @@ let deferral = () => ) |> Exp.fresh, ), - dhexp_of_uexp( + ); + +let ap_deferral_single_argument = () => + alco_check( + "string_sub(\"hello\", 1, _)(2)", + Ap( + Forward, DeferredAp( Var("string_sub") |> Exp.fresh, [ @@ -201,6 +216,24 @@ let deferral = () => ], ) |> Exp.fresh, + Int(2) |> Exp.fresh, + ) + |> Exp.fresh, + dhexp_of_uexp( + Ap( + Forward, + DeferredAp( + Var("string_sub") |> Exp.fresh, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, + Int(2) |> Exp.fresh, + ) + |> Exp.fresh, ), ); @@ -220,4 +253,9 @@ let elaboration_tests = [ `Quick, deferral, ), + test_case( + "Function application with a single remaining argument after deferral", + `Quick, + ap_deferral_single_argument, + ), ]; From 666b137ba0a9ddc5e9655a0de95184b3fdf847b8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 09:47:28 -0400 Subject: [PATCH 03/10] Make DeferredAp a Value --- src/haz3lcore/dynamics/Evaluator.re | 1 + src/haz3lcore/dynamics/EvaluatorStep.re | 2 ++ src/haz3lcore/dynamics/Transition.re | 5 +++-- src/haz3lcore/dynamics/ValueChecker.re | 1 + 4 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index fb877accd7..628b493e1d 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -118,6 +118,7 @@ module EvaluatorEVMode: { | (BoxedReady, Constructor) => (BoxedValue, c) | (IndetReady, Constructor) => (Indet, c) | (IndetBlocked, _) => (Indet, c) + | (_, Value) => (BoxedValue, c) | (_, Indet) => (Indet, c) }; }; diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index f25f25603f..0882fa223f 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -136,6 +136,7 @@ module Decompose = { | (undo, Result.BoxedValue, env, v) => switch (rl(v)) { | Constructor => Result.BoxedValue + | Value => Result.BoxedValue | Indet => Result.Indet | Step(s) => Result.Step([EvalObj.mk(Mark, env, undo, s.kind)]) // TODO: Actually show these exceptions to the user! @@ -187,6 +188,7 @@ module TakeStep = { state_update(); Some(expr); | Constructor + | Value | Indet => None }; diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index e0c278d2b7..d6b9fa7825 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -91,7 +91,8 @@ type rule = is_value: bool, }) | Constructor - | Indet; + | Indet + | Value; let (let-unbox) = ((request, v), f) => switch (Unboxing.unbox(request, v)) { @@ -331,7 +332,7 @@ module Transition = (EV: EV_MODE) => { (d2, ds) => DeferredAp2(d1, d2, ds) |> wrap_ctx, ds, ); - Constructor; + Value; | Ap(dir, d1, d2) => let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index 39f43daeed..c99a90db6f 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -69,6 +69,7 @@ module ValueCheckerEVMode: { | (_, _, Constructor) => r | (_, Expr, Indet) => Expr | (_, _, Indet) => Indet + | (_, _, Value) => Value | (true, _, Step(_)) => Expr | (false, _, Step(_)) => r }; From ab9f98182f2b097af4fdde616309a5e7db43c61c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 10:05:59 -0400 Subject: [PATCH 04/10] Remove invalid comment --- src/haz3lcore/dynamics/Transition.re | 1 - 1 file changed, 1 deletion(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index d6b9fa7825..7a9e8f16bf 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -393,7 +393,6 @@ module Transition = (EV: EV_MODE) => { } else { Indet; } - /* This case isn't currently used because deferrals are elaborated away */ | DeferredAp(d3, d4s) => let n_args = List.length( From 8d4ead15c678f20ef494ee1508bd00e5fa213a05 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 10:39:20 -0400 Subject: [PATCH 05/10] Add elavorator and evaluator tests for deferral applied to a hole --- test/Test_Elaboration.re | 87 ++++++++++++++++++++++++++++++ test/Test_Evaluator.re | 111 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 198 insertions(+) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index d5d25d9334..c515487535 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -237,6 +237,88 @@ let ap_deferral_single_argument = () => ), ); +let ap_of_deferral_of_hole = () => + alco_check( + "?(_, _, 3)(1., true)", + Ap( + Forward, + DeferredAp( + Cast( + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + Arrow( + Prod([ + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + [ + Deferral(InAp) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ], + ) + |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + dhexp_of_uexp( + Ap( + Forward, + DeferredAp( + EmptyHole |> Exp.fresh, + [ + Deferral(InAp) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + Int(3) |> Exp.fresh, + ], + ) + |> Exp.fresh, + Tuple([Float(1.) |> Exp.fresh, Bool(true) |> Exp.fresh]) + |> Exp.fresh, + ) + |> Exp.fresh, + ), + ); + let elaboration_tests = [ test_case("Single integer", `Quick, single_integer), test_case("Empty hole", `Quick, empty_hole), @@ -258,4 +340,9 @@ let elaboration_tests = [ `Quick, ap_deferral_single_argument, ), + test_case( + "Function application with a deferral of a hole", + `Quick, + ap_of_deferral_of_hole, + ), ]; diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index c6417b5737..ca85062226 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -50,9 +50,120 @@ let test_function_deferral = () => |> Exp.fresh, ); +let tet_ap_of_hole_deferral = () => + evaluation_test( + "?(_, _, 3)(1., true)", + Ap( + Forward, + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, + Prod([ + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ) + |> Exp.fresh, + Ap( + Forward, + DeferredAp( + Cast( + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + Arrow( + Prod([ + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, + [ + Deferral(InAp) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ], + ) + |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + ); + let tests = [ test_case("Integer literal", `Quick, test_int), test_case("Integer sum", `Quick, test_sum), 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), ]; From 1144e631fb9e26cddfeeb70c1f368a1f262fedac Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 4 Oct 2024 16:53:22 -0400 Subject: [PATCH 06/10] Switch to req_value --- src/haz3lcore/dynamics/Transition.re | 2 +- test/Test_Evaluator.re | 64 ++++++++++++++++------------ 2 files changed, 37 insertions(+), 29 deletions(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 7a9e8f16bf..5c936426b9 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -336,7 +336,7 @@ module Transition = (EV: EV_MODE) => { | Ap(dir, d1, d2) => let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = - req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) + req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) and. (d2', d2_is_value) = req_final_or_value( req(state, env), diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index ca85062226..37fcaba764 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -56,46 +56,54 @@ let tet_ap_of_hole_deferral = () => Ap( Forward, Cast( - EmptyHole |> Exp.fresh, - Unknown(Internal) |> Typ.fresh, + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, Arrow( Unknown(Internal) |> Typ.fresh, Unknown(Internal) |> Typ.fresh, ) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Tuple([ - Cast( - Float(1.) |> Exp.fresh, - Float |> Typ.fresh, + Arrow( + Prod([ Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Bool(true) |> Exp.fresh, - Bool |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Int(3) |> Exp.fresh, - Int |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - ]) - |> Exp.fresh, - Prod([ - Unknown(Internal) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ]) + ) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, ) |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, ) |> Exp.fresh, Ap( From 805b6ea5105d42d25d398b0382b4ee85cbf613a8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 8 Oct 2024 13:56:01 -0400 Subject: [PATCH 07/10] Run @ocaml-index as part of building --- Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index c1f5943d07..516016ddf8 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ setup-student: dev-helper: dune fmt --auto-promote || true - dune build @src/fmt --auto-promote src --profile dev + dune build @ocaml-index @src/fmt --auto-promote src --profile dev dev: setup-instructor dev-helper @@ -35,7 +35,7 @@ fmt: dune fmt --auto-promote watch: setup-instructor - dune build @src/fmt --auto-promote src --profile dev --watch + dune build @ocaml-index @src/fmt --auto-promote src --profile dev --watch watch-release: setup-instructor dune build @src/fmt --auto-promote src --profile release --watch @@ -60,11 +60,11 @@ repl: test: dune fmt --auto-promote || true - dune build @src/fmt @test/fmt --auto-promote src test --profile dev + dune build @ocaml-index @src/fmt @test/fmt --auto-promote src test --profile dev node $(TEST_DIR)/haz3ltest.bc.js watch-test: - dune build @fmt @runtest --auto-promote --watch + dune build @ocaml-index @fmt @runtest --auto-promote --watch clean: dune clean From 2003c7607e55a701eeaa4a8387b561bb7bd11f42 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 7 Oct 2024 10:39:39 -0400 Subject: [PATCH 08/10] Add MakeTerm tests to test regular hazel parsing --- test/Test_MakeTerm.re | 70 +++++++++++++++++++++++++++++++++++++++++++ test/haz3ltest.re | 1 + 2 files changed, 71 insertions(+) create mode 100644 test/Test_MakeTerm.re diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re new file mode 100644 index 0000000000..82eee683b6 --- /dev/null +++ b/test/Test_MakeTerm.re @@ -0,0 +1,70 @@ +/** + * This file contains tests to validate the `MakeTerm` module's ability to convert + * zippers into expressions. + */ +open Alcotest; +open Haz3lcore; + +let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal); + +// TODO Assertion if it doesn't parse +let parse_exp = (s: string) => + MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; +let exp_check = (expected, actual) => + check(exp_typ, actual, expected, parse_exp(actual)); + +let tests = [ + test_case("Integer Literal", `Quick, () => { + exp_check(Int(0) |> Exp.fresh, "0") + }), + test_case("Empty Hole", `Quick, () => { + exp_check(EmptyHole |> Exp.fresh, "?") + }), + test_case("Free Variable", `Quick, () => { + exp_check(Var("x") |> Exp.fresh, "x") + }), + test_case("Parenthesized Expression", `Quick, () => { + exp_check(Parens(Int(0) |> Exp.fresh) |> Exp.fresh, "(0)") + }), + test_case("Let Expression", `Quick, () => { + exp_check( + Let( + Var("x") |> Pat.fresh, + Int(1) |> Exp.fresh, + Var("x") |> Exp.fresh, + ) + |> Exp.fresh, + "let x = 1 in x", + ) + }), + test_case("Function Application", `Quick, () => { + exp_check( + Ap(Forward, Var("f") |> Exp.fresh, Var("x") |> Exp.fresh) |> Exp.fresh, + "f(x)", + ) + }), + test_case("Named Function Definition", `Quick, () => { + exp_check( + Let( + Var("f") |> Pat.fresh, + 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, + ) + |> Exp.fresh, + "let f = fun x -> x in 1", + ) + }), + test_case("Incomplete Function Definition", `Quick, () => { + exp_check( + Let( + EmptyHole |> Pat.fresh, + Fun(Var("x") |> Pat.fresh, EmptyHole |> Exp.fresh, None, None) + |> Exp.fresh, + EmptyHole |> Exp.fresh, + ) + |> Exp.fresh, + "let = fun x -> in ", + ) + }), +]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 3e13ae44b7..3c6cbb6098 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -8,6 +8,7 @@ let (suite, _) = ("Elaboration", Test_Elaboration.elaboration_tests), ("Statics", Test_Statics.tests), ("Evaluator", Test_Evaluator.tests), + ("MakeTerm", Test_MakeTerm.tests), ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From 5b82cae1ac1e4b56487301e85d91b57336bd3526 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 13 Oct 2024 09:54:38 -0400 Subject: [PATCH 09/10] Remove todo --- test/Test_MakeTerm.re | 1 - 1 file changed, 1 deletion(-) diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index 82eee683b6..be365e9edb 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -7,7 +7,6 @@ open Haz3lcore; let exp_typ = testable(Fmt.using(Exp.show, Fmt.string), Exp.fast_equal); -// TODO Assertion if it doesn't parse let parse_exp = (s: string) => MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; let exp_check = (expected, actual) => From bc19bf60845760683588eda83c90013e6459075e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 24 Oct 2024 10:58:23 -0400 Subject: [PATCH 10/10] Added additional tests --- test/Test_MakeTerm.re | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index be365e9edb..46818664a9 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -66,4 +66,17 @@ let tests = [ "let = fun x -> in ", ) }), + test_case("Constructor", `Quick, () => { + exp_check( + Constructor("A", Unknown(Internal) |> Typ.fresh) |> Exp.fresh, + "A", + ) + }), + test_case("Type Alias", `Quick, () => { + exp_check( + TyAlias(Var("x") |> TPat.fresh, Int |> Typ.fresh, Int(1) |> Exp.fresh) + |> Exp.fresh, + "type x = Int in 1", + ) + }), ];