From 63d88e87733bfee0fedfcf585f6ee4d26ae6ac73 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 12:58:11 -0400 Subject: [PATCH 01/53] [IN-PROGRESS] Working on adding code coverage --- .gitignore | 60 ++++++++++++++++++++++++++++++++++++++++++++++ dune-project | 3 ++- hazel.opam | 3 ++- hazel.opam.locked | 20 ++++++++-------- src/haz3lcore/dune | 2 ++ src/haz3lweb/dune | 4 ++++ src/pretty/dune | 2 ++ src/util/dune | 2 ++ test/dune | 4 ++-- test/haz3ltest.re | 1 + 10 files changed, 87 insertions(+), 14 deletions(-) diff --git a/.gitignore b/.gitignore index ec464113b6..ccfcb18745 100644 --- a/.gitignore +++ b/.gitignore @@ -56,3 +56,63 @@ setup.log # Backup of opam lock file hazel.opam.locked.old +_coverage/coverage.css +_coverage/coverage.js +_coverage/highlight.pack.js +_coverage/index.html +_coverage/src/haz3lcore/StructureShareSexp.re.html +_coverage/src/haz3lcore/VarMap.re.html +_coverage/src/haz3lcore/dynamics/Builtins.re.html +_coverage/src/haz3lcore/dynamics/Casts.re.html +_coverage/src/haz3lcore/dynamics/Constraint.re.html +_coverage/src/haz3lcore/dynamics/Delta.re.html +_coverage/src/haz3lcore/dynamics/DHExp.re.html +_coverage/src/haz3lcore/dynamics/DHPat.re.html +_coverage/src/haz3lcore/dynamics/Elaborator.re.html +_coverage/src/haz3lcore/dynamics/Environment.re.html +_coverage/src/haz3lcore/dynamics/EvaluatorError.re.html +_coverage/src/haz3lcore/dynamics/FilterAction.re.html +_coverage/src/haz3lcore/dynamics/Incon.re.html +_coverage/src/haz3lcore/dynamics/InvalidOperationError.re.html +_coverage/src/haz3lcore/dynamics/Sets.re.html +_coverage/src/haz3lcore/dynamics/VarBstMap.re.html +_coverage/src/haz3lcore/lang/Form.re.html +_coverage/src/haz3lcore/lang/Operators.re.html +_coverage/src/haz3lcore/lang/Precedence.re.html +_coverage/src/haz3lcore/lang/Sort.re.html +_coverage/src/haz3lcore/lang/term/Any.re.html +_coverage/src/haz3lcore/lang/term/Cls.re.html +_coverage/src/haz3lcore/lang/term/Exp.re.html +_coverage/src/haz3lcore/lang/term/IdTagged.re.html +_coverage/src/haz3lcore/lang/term/Pat.re.html +_coverage/src/haz3lcore/lang/term/Rul.re.html +_coverage/src/haz3lcore/lang/term/TPat.re.html +_coverage/src/haz3lcore/lang/term/Typ.re.html +_coverage/src/haz3lcore/prog/CoreSettings.re.html +_coverage/src/haz3lcore/statics/CoCtx.re.html +_coverage/src/haz3lcore/statics/Constructor.re.html +_coverage/src/haz3lcore/statics/ConstructorMap.re.html +_coverage/src/haz3lcore/statics/Ctx.re.html +_coverage/src/haz3lcore/statics/Info.re.html +_coverage/src/haz3lcore/statics/Mode.re.html +_coverage/src/haz3lcore/statics/Self.re.html +_coverage/src/haz3lcore/statics/Statics.re.html +_coverage/src/haz3lcore/statics/Term.re.html +_coverage/src/haz3lcore/statics/TermBase.re.html +_coverage/src/haz3lcore/statics/Var.re.html +_coverage/src/haz3lcore/statics/uterm/UExp.re.html +_coverage/src/haz3lcore/statics/uterm/UPat.re.html +_coverage/src/haz3lcore/statics/uterm/UTyp.re.html +_coverage/src/haz3lcore/tiles/Id.re.html +_coverage/src/haz3lcore/tiles/Mold.re.html +_coverage/src/haz3lcore/tiles/Nib.re.html +_coverage/src/haz3lcore/tiles/Nibs.re.html +_coverage/src/haz3lcore/tiles/Secondary.re.html +_coverage/src/haz3lcore/tiles/Token.re.html +_coverage/src/util/Direction.re.html +_coverage/src/util/IntMap.re.html +_coverage/src/util/ListUtil.re.html +_coverage/src/util/OptUtil.re.html +_coverage/src/util/StringUtil.re.html +_coverage/src/util/TupleUtil.re.html +_coverage/src/util/Util.re.html diff --git a/dune-project b/dune-project index 5e71bc4ee5..4e17ae067c 100644 --- a/dune-project +++ b/dune-project @@ -25,10 +25,11 @@ (menhir (>= 2.0)) yojson - reason + (reason (>= 3.12.0)) ppx_yojson_conv_lib ppx_yojson_conv incr_dom + bisect_ppx (omd (>= 2.0.0~alpha4)) ezjs_idb virtual_dom diff --git a/hazel.opam b/hazel.opam index 36a81b933a..ad9af541a1 100644 --- a/hazel.opam +++ b/hazel.opam @@ -11,10 +11,11 @@ depends: [ "ocaml" {>= "5.2.0"} "menhir" {>= "2.0"} "yojson" - "reason" + "reason" {>= "3.12.0"} "ppx_yojson_conv_lib" "ppx_yojson_conv" "incr_dom" + "bisect_ppx" "omd" {>= "2.0.0~alpha4"} "ezjs_idb" "virtual_dom" diff --git a/hazel.opam.locked b/hazel.opam.locked index 8672b0816a..8c7a594892 100644 --- a/hazel.opam.locked +++ b/hazel.opam.locked @@ -27,14 +27,14 @@ depends: [ "base_bigstring" {= "v0.16.0"} "base_quickcheck" {= "v0.16.0"} "bignum" {= "v0.16.0"} - "bigstringaf" {= "0.10.0"} + "bigstringaf" {= "0.9.1"} "bin_prot" {= "v0.16.0"} + "bisect_ppx" {= "2.8.3"} "camlp-streams" {= "5.0.1"} "chrome-trace" {= "3.16.0"} "cmdliner" {= "1.3.0"} "conf-bash" {= "1"} "conf-gmp" {= "4"} - "conf-pkg-config" {= "3"} "core" {= "v0.16.2"} "core_kernel" {= "v0.16.0"} "cppo" {= "1.6.9"} @@ -74,13 +74,13 @@ depends: [ "lsp" {= "1.19.0"} "lwt" {= "5.7.0"} "markup" {= "1.0.3"} - "menhir" {= "20240715"} - "menhirCST" {= "20240715"} - "menhirLib" {= "20240715"} - "menhirSdk" {= "20240715"} + "menhir" {= "20231231"} + "menhirCST" {= "20231231"} + "menhirLib" {= "20231231"} + "menhirSdk" {= "20231231"} "merlin-extend" {= "0.6.1"} "merlin-lib" {= "5.1-502"} - "num" {= "1.5-1"} + "num" {= "1.5"} "ocaml" {= "5.2.0"} "ocaml-base-compiler" {= "5.2.0"} "ocaml-compiler-libs" {= "v0.17.0"} @@ -90,7 +90,7 @@ depends: [ "ocaml-options-vanilla" {= "1"} "ocaml-syntax-shims" {= "1.0.0"} "ocaml-version" {= "3.6.7"} - "ocamlbuild" {= "0.15.0"} + "ocamlbuild" {= "0.14.3"} "ocamlc-loc" {= "3.16.0"} "ocamlfind" {= "1.9.6"} "ocamlformat" {= "0.26.2"} @@ -143,7 +143,7 @@ depends: [ "ppx_variants_conv" {= "v0.16.0"} "ppx_yojson_conv" {= "v0.16.0"} "ppx_yojson_conv_lib" {= "v0.16.0"} - "ppxlib" {= "0.33.0"} + "ppxlib" {= "0.32.1"} "protocol_version_header" {= "v0.16.0"} "ptime" {= "1.1.0" & with-test} "ptmap" {= "2.0.5"} @@ -179,7 +179,7 @@ depends: [ "virtual_dom" {= "v0.16.0"} "xdg" {= "3.16.0"} "yojson" {= "2.2.2"} - "zarith" {= "1.14"} + "zarith" {= "1.13"} "zarith_stubs_js" {= "v0.16.1"} ] build: [ diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index 77e2ca3fe1..a0d9770816 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -4,6 +4,8 @@ (name haz3lcore) (libraries util sexplib unionFind uuidm virtual_dom yojson core) (js_of_ocaml) + (instrumentation + (backend bisect_ppx)) (preprocess (pps ppx_yojson_conv diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index 8d25155dc5..84023f76a5 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -8,6 +8,8 @@ (library (name workerServer) (modules WorkerServer) + (instrumentation + (backend bisect_ppx)) (libraries incr_dom virtual_dom.input_widgets @@ -28,6 +30,8 @@ (library (name haz3lweb) + (instrumentation + (backend bisect_ppx)) (modules (:standard \ Main) \ diff --git a/src/pretty/dune b/src/pretty/dune index 868d03defc..c131965aff 100644 --- a/src/pretty/dune +++ b/src/pretty/dune @@ -3,6 +3,8 @@ (library (name pretty) (libraries util sexplib) + (instrumentation + (backend bisect_ppx)) (preprocess (pps ppx_let ppx_sexp_conv))) diff --git a/src/util/dune b/src/util/dune index 889c95bd2c..8fbebea70b 100644 --- a/src/util/dune +++ b/src/util/dune @@ -2,6 +2,8 @@ (name util) (libraries re base ptmap incr_dom virtual_dom yojson) (js_of_ocaml) + (instrumentation + (backend bisect_ppx)) (preprocess (pps ppx_yojson_conv diff --git a/test/dune b/test/dune index 832c9689f2..3b9dc8bb2e 100644 --- a/test/dune +++ b/test/dune @@ -2,7 +2,7 @@ (test (name haz3ltest) - (libraries haz3lcore alcotest junit junit_alcotest) + (libraries haz3lcore alcotest junit junit_alcotest bisect_ppx.runtime) (modes js) (preprocess - (pps js_of_ocaml-ppx))) + (pps js_of_ocaml-ppx ppx_deriving.show))) diff --git a/test/haz3ltest.re b/test/haz3ltest.re index e405fba7b8..e346e20556 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -7,3 +7,4 @@ let (suite, _) = [("Elaboration", Test_Elaboration.elaboration_tests)], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); +Bisect.Runtime.write_coverage_data(); \ No newline at end of file From 484e3f07521d22cfc3824e4a44b1990c98fe264b Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 13:00:00 -0400 Subject: [PATCH 02/53] Fix git ignore --- .gitignore | 63 +++--------------------------------------------------- 1 file changed, 3 insertions(+), 60 deletions(-) diff --git a/.gitignore b/.gitignore index ccfcb18745..87b0876181 100644 --- a/.gitignore +++ b/.gitignore @@ -56,63 +56,6 @@ setup.log # Backup of opam lock file hazel.opam.locked.old -_coverage/coverage.css -_coverage/coverage.js -_coverage/highlight.pack.js -_coverage/index.html -_coverage/src/haz3lcore/StructureShareSexp.re.html -_coverage/src/haz3lcore/VarMap.re.html -_coverage/src/haz3lcore/dynamics/Builtins.re.html -_coverage/src/haz3lcore/dynamics/Casts.re.html -_coverage/src/haz3lcore/dynamics/Constraint.re.html -_coverage/src/haz3lcore/dynamics/Delta.re.html -_coverage/src/haz3lcore/dynamics/DHExp.re.html -_coverage/src/haz3lcore/dynamics/DHPat.re.html -_coverage/src/haz3lcore/dynamics/Elaborator.re.html -_coverage/src/haz3lcore/dynamics/Environment.re.html -_coverage/src/haz3lcore/dynamics/EvaluatorError.re.html -_coverage/src/haz3lcore/dynamics/FilterAction.re.html -_coverage/src/haz3lcore/dynamics/Incon.re.html -_coverage/src/haz3lcore/dynamics/InvalidOperationError.re.html -_coverage/src/haz3lcore/dynamics/Sets.re.html -_coverage/src/haz3lcore/dynamics/VarBstMap.re.html -_coverage/src/haz3lcore/lang/Form.re.html -_coverage/src/haz3lcore/lang/Operators.re.html -_coverage/src/haz3lcore/lang/Precedence.re.html -_coverage/src/haz3lcore/lang/Sort.re.html -_coverage/src/haz3lcore/lang/term/Any.re.html -_coverage/src/haz3lcore/lang/term/Cls.re.html -_coverage/src/haz3lcore/lang/term/Exp.re.html -_coverage/src/haz3lcore/lang/term/IdTagged.re.html -_coverage/src/haz3lcore/lang/term/Pat.re.html -_coverage/src/haz3lcore/lang/term/Rul.re.html -_coverage/src/haz3lcore/lang/term/TPat.re.html -_coverage/src/haz3lcore/lang/term/Typ.re.html -_coverage/src/haz3lcore/prog/CoreSettings.re.html -_coverage/src/haz3lcore/statics/CoCtx.re.html -_coverage/src/haz3lcore/statics/Constructor.re.html -_coverage/src/haz3lcore/statics/ConstructorMap.re.html -_coverage/src/haz3lcore/statics/Ctx.re.html -_coverage/src/haz3lcore/statics/Info.re.html -_coverage/src/haz3lcore/statics/Mode.re.html -_coverage/src/haz3lcore/statics/Self.re.html -_coverage/src/haz3lcore/statics/Statics.re.html -_coverage/src/haz3lcore/statics/Term.re.html -_coverage/src/haz3lcore/statics/TermBase.re.html -_coverage/src/haz3lcore/statics/Var.re.html -_coverage/src/haz3lcore/statics/uterm/UExp.re.html -_coverage/src/haz3lcore/statics/uterm/UPat.re.html -_coverage/src/haz3lcore/statics/uterm/UTyp.re.html -_coverage/src/haz3lcore/tiles/Id.re.html -_coverage/src/haz3lcore/tiles/Mold.re.html -_coverage/src/haz3lcore/tiles/Nib.re.html -_coverage/src/haz3lcore/tiles/Nibs.re.html -_coverage/src/haz3lcore/tiles/Secondary.re.html -_coverage/src/haz3lcore/tiles/Token.re.html -_coverage/src/util/Direction.re.html -_coverage/src/util/IntMap.re.html -_coverage/src/util/ListUtil.re.html -_coverage/src/util/OptUtil.re.html -_coverage/src/util/StringUtil.re.html -_coverage/src/util/TupleUtil.re.html -_coverage/src/util/Util.re.html + +# Code coverage +_coverage/ From 39f6d594cd1fe7e8744ec05b8a417b3bd520ead4 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 12 Aug 2024 16:10:15 -0400 Subject: [PATCH 03/53] formatting --- test/haz3ltest.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/haz3ltest.re b/test/haz3ltest.re index e346e20556..6e152b2fe8 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -7,4 +7,4 @@ let (suite, _) = [("Elaboration", Test_Elaboration.elaboration_tests)], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); -Bisect.Runtime.write_coverage_data(); \ No newline at end of file +Bisect.Runtime.write_coverage_data(); From 8c38c1bc22b4281d8b19d6400ba2fb4ca8e46aea Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 16 Aug 2024 11:18:05 -0400 Subject: [PATCH 04/53] Add coverage command to makefile --- Makefile | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Makefile b/Makefile index 455ff6e441..e5851f1ecf 100644 --- a/Makefile +++ b/Makefile @@ -61,5 +61,13 @@ test: dune build @src/fmt @test/fmt --auto-promote src test --profile dev node $(TEST_DIR)/haz3ltest.bc.js +coverage: + dune build @src/fmt @test/fmt --auto-promote src test --profile dev + dune runtest --instrument-with bisect_ppx --force + bisect-ppx-report summary + +generate-coverage-html: + bisect-ppx-report html + clean: dune clean From a85fb7e83717c373ef6e2294f61ad3bb0c44a4d2 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 16 Aug 2024 11:21:34 -0400 Subject: [PATCH 05/53] Add coverage to Readme --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index a15bdd424e..15caf27308 100644 --- a/README.md +++ b/README.md @@ -197,6 +197,9 @@ You can run all of the unit tests located in `test` by running `make test`. Unit tests are written using the [Alcotest framework](https://github.com/mirage/alcotest). +#### Coverage +Code coverage is provided by [bisect_ppx](https://github.com/aantron/bisect_ppx). To collect coverage statistics from tests run `make coverage`. After coverage statistics are generated, running `make generate-coverage-html` will generate a local webpage at `_coverage/index.html` that can be viewed to see line coverage per module. + ### Continuous Integration When you push your branch to the main `hazelgrove/hazel` repository, we From 04d63981dce075b19fc45aea7013cf9d83b65178 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 12:47:24 -0400 Subject: [PATCH 06/53] Starting adding tests for util modules --- test/Test_ListUtil.re | 29 +++++++++++++++++++++++++++++ test/haz3ltest.re | 7 +++++-- 2 files changed, 34 insertions(+), 2 deletions(-) create mode 100644 test/Test_ListUtil.re diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re new file mode 100644 index 0000000000..76881fcb75 --- /dev/null +++ b/test/Test_ListUtil.re @@ -0,0 +1,29 @@ +open Alcotest; +open Util; + +let tests = ( + "ListUtil", + [ + Alcotest.test_case( + "rev_if with false", + `Quick, + () => { + let xs = [1, 2, 3]; + check(list(int), "Same list", ListUtil.rev_if(false, xs), xs); + }, + ), + Alcotest.test_case( + "rev_if with true", + `Quick, + () => { + let xs = [1, 2, 3]; + check( + list(int), + "Reversed list", + ListUtil.rev_if(true, xs), + [3, 2, 1], + ); + }, + ), + ], +); diff --git a/test/haz3ltest.re b/test/haz3ltest.re index e405fba7b8..fbef084c43 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -3,7 +3,10 @@ open Junit_alcotest; let (suite, _) = run_and_report( ~and_exit=false, - "Dynamics", - [("Elaboration", Test_Elaboration.elaboration_tests)], + "HazelTests", + [ + ("Elaboration", Test_Elaboration.elaboration_tests), + Test_ListUtil.tests, + ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From 0990af40c2d63c3d57ea602ee24efdaf66c0d3ab Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 13:49:46 -0400 Subject: [PATCH 07/53] Mas tests --- src/util/ListUtil.re | 2 ++ test/Test_ListUtil.re | 41 +++++++++++++++++++++++++++++++++++++++-- 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 9c6bed90b0..f01a5c1af1 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -1,5 +1,6 @@ let rev_if = (b: bool) => b ? List.rev : Fun.id; +// TODO: Replace with dedup_f((==)); let dedup = xs => List.fold_right( (x, deduped) => List.mem(x, deduped) ? deduped : [x, ...deduped], @@ -14,6 +15,7 @@ let dedup_f = (f, xs) => [], ); +// TODO: Rename is_unique? let are_duplicates = xs => List.length(List.sort_uniq(compare, xs)) == List.length(xs); diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 76881fcb75..57ad521c7b 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -9,7 +9,7 @@ let tests = ( `Quick, () => { let xs = [1, 2, 3]; - check(list(int), "Same list", ListUtil.rev_if(false, xs), xs); + check(list(int), "Same list", xs, ListUtil.rev_if(false, xs)); }, ), Alcotest.test_case( @@ -20,10 +20,47 @@ let tests = ( check( list(int), "Reversed list", - ListUtil.rev_if(true, xs), [3, 2, 1], + ListUtil.rev_if(true, xs), ); }, ), + Alcotest.test_case( + "dedup", + `Quick, + () => { + let xs = [1, 2, 3, 2]; + check(list(int), "Unique list", [1, 3, 2], ListUtil.dedup(xs)); // TODO: Interesting the order here is messed up because of fold_right + }, + ), + Alcotest.test_case( + "dedup_f", + `Quick, + () => { + let xs = [1, 2, 3, 2]; + check( + list(int), + "Unique list", + [1, 3, 2], + ListUtil.dedup_f((==), xs), + ); // TODO: Interesting the order here is messed up because of fold_right + }, + ), + Alcotest.test_case( + "are_duplicates has duplicates", + `Quick, + () => { + let xs = [1, 2, 3, 2]; + check(bool, "Returns false", false, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right + }, + ), + Alcotest.test_case( + "are_duplicates has no duplicates", + `Quick, + () => { + let xs = [1, 2, 3]; + check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right + }, + ), ], ); From 1ad604f2247ec43ee5eaf91674976a1c5f31ea74 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 21:22:37 -0400 Subject: [PATCH 08/53] Tests --- src/util/ListUtil.re | 3 +- test/Test_ListUtil.re | 114 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 116 insertions(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index f01a5c1af1..7deb4d41d8 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -19,6 +19,7 @@ let dedup_f = (f, xs) => let are_duplicates = xs => List.length(List.sort_uniq(compare, xs)) == List.length(xs); +// TODO Interesting that this reverses the list inside the groups let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) => List.fold_left( (grouped, x) => { @@ -34,7 +35,7 @@ let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) => xs, ); -let rec range = (~lo=0, hi) => +let rec range = (~lo: int=0, hi: int) => if (lo > hi) { raise(Invalid_argument("ListUtil.range")); } else if (lo == hi) { diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 57ad521c7b..7714342b8c 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -62,5 +62,119 @@ let tests = ( check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), + Alcotest.test_case( + "group_by with constant function preserves list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + list(pair(unit, list(int))), + "singleton group", + [((), List.rev(xs))], + ListUtil.group_by(__ => (), xs), + ); + }, + ), + Alcotest.test_case( + "group_by groups into evens/odds", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + list(pair(int, list(int))), + "odds and evens", + [(1, [5, 3, 1]), (0, [4, 2])], + ListUtil.group_by(x => x mod 2, xs), + ); + }, + ), + Alcotest.test_case("range generates sequential integers [1,6)", `Quick, () => { + check(list(int), "1-5", [1, 2, 3, 4, 5], ListUtil.range(~lo=1, 6)) + }), + Alcotest.test_case("range defaults lower bound to 0", `Quick, () => { + check(list(int), "0-5", [0, 1, 2, 3, 4, 5], ListUtil.range(6)) + }), + Alcotest.test_case("range lo = hi is empty", `Quick, () => { + check(list(int), "empty list", [], ListUtil.range(~lo=1, 1)) + }), + Alcotest.test_case("Invalid range raises error", `Quick, () => { + check_raises( + "Invalid range", + Invalid_argument("ListUtil.range"), + () => { + let _ = ListUtil.range(~lo=2, 1); + (); + }, + ) + }), + Alcotest.test_case( + "mk_frame creates a frame from the beginning", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + ([], xs), + ListUtil.mk_frame(0, xs), + ); + }, + ), + Alcotest.test_case( + "mk_frame creates a frame from the end", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + (List.rev(xs), []), + ListUtil.mk_frame(5, xs), + ); + }, + ), + Alcotest.test_case( + "mk_frame raises when making a frame past the end", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.mk_frame"), + () => { + let _ = ListUtil.mk_frame(6, xs); + (); + }, + ); + }, + ), + Alcotest.test_case( + "mk_frame raises when making a frame before the beginning", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.mk_frame"), + () => { + let _ = ListUtil.mk_frame(-1, xs); + (); + }, + ); + }, + ), + Alcotest.test_case( + "mk_frame makes a frame splitting the list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + (List.rev([1, 2, 3]), [4, 5]), + ListUtil.mk_frame(3, xs), + ); + }, + ), ], ); From 2a83a0451ad1581f3d99eaf85015f85de7c06f59 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 10 Aug 2024 22:03:13 -0400 Subject: [PATCH 09/53] Stop qualifying import and even more tests --- test/Test_ListUtil.re | 86 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 69 insertions(+), 17 deletions(-) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 7714342b8c..c0618dd6f5 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -4,7 +4,7 @@ open Util; let tests = ( "ListUtil", [ - Alcotest.test_case( + test_case( "rev_if with false", `Quick, () => { @@ -12,7 +12,7 @@ let tests = ( check(list(int), "Same list", xs, ListUtil.rev_if(false, xs)); }, ), - Alcotest.test_case( + test_case( "rev_if with true", `Quick, () => { @@ -25,7 +25,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "dedup", `Quick, () => { @@ -33,7 +33,7 @@ let tests = ( check(list(int), "Unique list", [1, 3, 2], ListUtil.dedup(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "dedup_f", `Quick, () => { @@ -46,7 +46,7 @@ let tests = ( ); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "are_duplicates has duplicates", `Quick, () => { @@ -54,7 +54,7 @@ let tests = ( check(bool, "Returns false", false, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "are_duplicates has no duplicates", `Quick, () => { @@ -62,7 +62,7 @@ let tests = ( check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right }, ), - Alcotest.test_case( + test_case( "group_by with constant function preserves list", `Quick, () => { @@ -75,7 +75,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "group_by groups into evens/odds", `Quick, () => { @@ -88,16 +88,16 @@ let tests = ( ); }, ), - Alcotest.test_case("range generates sequential integers [1,6)", `Quick, () => { + test_case("range generates sequential integers [1,6)", `Quick, () => { check(list(int), "1-5", [1, 2, 3, 4, 5], ListUtil.range(~lo=1, 6)) }), - Alcotest.test_case("range defaults lower bound to 0", `Quick, () => { + test_case("range defaults lower bound to 0", `Quick, () => { check(list(int), "0-5", [0, 1, 2, 3, 4, 5], ListUtil.range(6)) }), - Alcotest.test_case("range lo = hi is empty", `Quick, () => { + test_case("range lo = hi is empty", `Quick, () => { check(list(int), "empty list", [], ListUtil.range(~lo=1, 1)) }), - Alcotest.test_case("Invalid range raises error", `Quick, () => { + test_case("Invalid range raises error", `Quick, () => { check_raises( "Invalid range", Invalid_argument("ListUtil.range"), @@ -107,7 +107,7 @@ let tests = ( }, ) }), - Alcotest.test_case( + test_case( "mk_frame creates a frame from the beginning", `Quick, () => { @@ -120,7 +120,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame creates a frame from the end", `Quick, () => { @@ -133,7 +133,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame raises when making a frame past the end", `Quick, () => { @@ -148,7 +148,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame raises when making a frame before the beginning", `Quick, () => { @@ -163,7 +163,7 @@ let tests = ( ); }, ), - Alcotest.test_case( + test_case( "mk_frame makes a frame splitting the list", `Quick, () => { @@ -176,5 +176,57 @@ let tests = ( ); }, ), + test_case( + "mk_frame makes a frame splitting the list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "frame", + (List.rev([1, 2, 3]), [4, 5]), + ListUtil.mk_frame(3, xs), + ); + }, + ), + test_case( + "split with no found element returns the original list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), option(int), list(int)), + "split", + (xs, None, []), + ListUtil.split(xs, __ => false), + ); + }, + ), + test_case( + "split with first found returns the head and tail", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), option(int), list(int)), + "split", + ([], Some(1), [2, 3, 4, 5]), + ListUtil.split(xs, __ => true), + ); + }, + ), + test_case( + "splits on the middle element", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), option(int), list(int)), + "split", + ([1, 2], Some(3), [4, 5]), + ListUtil.split(xs, (==)(3)), + ); + }, + ), ], ); From 701bf5c07d755c21fbcfdd78a4279679cf8b2c35 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 13 Aug 2024 14:47:51 -0400 Subject: [PATCH 10/53] Another test --- test/Test_ListUtil.re | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index c0618dd6f5..bb22b4fe1c 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -228,5 +228,29 @@ let tests = ( ); }, ), + test_case( + "combine_opt", + `Quick, + () => { + check( + option(list(pair(string, int))), + "Same size lists", + Some([("a", 1), ("b", 2), ("c", 3)]), + ListUtil.combine_opt(["a", "b", "c"], [1, 2, 3]), + ); + check( + option(list(pair(string, int))), + "Empty Lists", + Some([]), + ListUtil.combine_opt([], []), + ); + check( + option(list(pair(string, int))), + "Inconsistent size lists", + None, + ListUtil.combine_opt(["a"], [1, 2]), + ); + }, + ), ], ); From 4a7570e29b8f11dc92c6a473d252b8980ae0a8a1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 15:38:18 -0400 Subject: [PATCH 11/53] Additional tests --- test/Test_ListUtil.re | 48 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index bb22b4fe1c..4a3c0f519e 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -252,5 +252,53 @@ let tests = ( ); }, ), + test_case( + "is_empty with empty list", + `Quick, + () => { + let xs = []; + check(bool, "Returns true", true, ListUtil.is_empty(xs)); + }, + ), + test_case( + "is_empty with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + check(bool, "Returns false", false, ListUtil.is_empty(xs)); + }, + ), + test_case( + "flat_map with empty list", + `Quick, + () => { + let xs = []; + let f = x => [x, x]; + check(list(int), "Empty list", [], ListUtil.flat_map(f, xs)); + }, + ), + test_case( + "flat_map with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + let f = x => [x, x]; + check( + list(int), + "Doubled list", + [1, 1, 2, 2, 3, 3], + ListUtil.flat_map(f, xs), + ); + }, + ), + test_case( + "flat_map with non-empty list and empty result", + `Quick, + () => { + let xs = [1, 2, 3]; + let f = _ => []; + check(list(int), "Empty list", [], ListUtil.flat_map(f, xs)); + }, + ), ], ); From 3e2bc890bed624905e32701d572a34bd460d0cb1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 15:53:29 -0400 Subject: [PATCH 12/53] Add tests for ListUtil module --- src/util/ListUtil.re | 2 +- test/Test_ListUtil.re | 320 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 321 insertions(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 7deb4d41d8..aed1539298 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -174,7 +174,7 @@ let split_sublist_opt = let split_sublist = (i: int, j: int, xs: list('x)): (list('x), list('x), list('x)) => switch (split_sublist_opt(i, j, xs)) { - | None => raise(Invalid_argument("ListUtil.split_sublist")) + | None => raise(Invalid_argument("ListUtil.split_sublist: " ++ string_of_int(i) ++ ", " ++ string_of_int(j))) | Some(r) => r }; let sublist = ((i, j), xs: list('x)): list('x) => { diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 4a3c0f519e..509fa9f634 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -300,5 +300,325 @@ let tests = ( check(list(int), "Empty list", [], ListUtil.flat_map(f, xs)); }, ), + test_case( + "join with empty list", + `Quick, + () => { + let xs = []; + check(list(string), "Empty list", ListUtil.join(",", xs), []); + }, + ), + test_case( + "join with single element list", + `Quick, + () => { + let xs = ["a"]; + check(list(string), "Single element list", ListUtil.join(",", xs), ["a"]); + }, + ), + test_case( + "join with multiple element list", + `Quick, + () => { + let xs = ["a", "b", "c"]; + check( + list(string), + "Multiple element list", + ListUtil.join(",", xs), + ["a", ",", "b", ",", "c"], + ); + }, + ), + test_case( + "hd_opt with empty list", + `Quick, + () => { + let xs = []; + check(option(int), "None", None, ListUtil.hd_opt(xs)); + }, + ), + test_case( + "hd_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + check(option(int), "Some", Some(1), ListUtil.hd_opt(xs)); + }, + ), + test_case( + "nth_opt with empty list", + `Quick, + () => { + let xs = []; + check(option(int), "None", None, ListUtil.nth_opt(0, xs)); + }, + ), + test_case( + "nth_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3]; + check(option(int), "Some", Some(2), ListUtil.nth_opt(1, xs)); + }, + ), + test_case( + "nth_opt with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3]; + check(option(int), "None", None, ListUtil.nth_opt(3, xs)); + }, + ), + test_case( + "split_n_opt with empty list", + `Quick, + () => { + let xs = []; + check( + option(pair(list(int), list(int))), + "Empty list", + Some(([], [])), + ListUtil.split_n_opt(0, xs), + ); + }, + ), + test_case( + "split_n_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(pair(list(int), list(int))), + "Split list", + Some(([1, 2, 3], [4, 5])), + ListUtil.split_n_opt(3, xs), + ); + }, + ), + test_case( + "split_n_opt with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(pair(list(int), list(int))), + "None", + None, + ListUtil.split_n_opt(6, xs), + ); + }, + ), + test_case( + "split_n_opt with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(pair(list(int), list(int))), + "Empty first part", + Some(([], xs)), + ListUtil.split_n_opt(0, xs), + ); + }, + ), + // split_n + test_case( + "split_n with empty list", + `Quick, + () => { + let xs = []; + check( + pair(list(int), list(int)), + "Empty list", + ([], []), + ListUtil.split_n(0, xs), + ); + }, + ), + test_case( + "split_n with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "Split list", + ([1, 2, 3], [4, 5]), + ListUtil.split_n(3, xs), + ); + }, + ), + test_case( + "split_n with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.split_n: 6"), + () => { + let _ = ListUtil.split_n(6, xs); + (); + }, + ); + }, + ), + test_case( + "split_n with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + pair(list(int), list(int)), + "Empty first part", + ([], xs), + ListUtil.split_n(0, xs), + ); + }, + ), + // split_sublist_opt + test_case( + "split_sublist_opt with empty list", + `Quick, + () => { + let xs = []; + check( + option(triple(list(int), list(int), list(int))), + "Empty list", + Some(([], [], [])), + ListUtil.split_sublist_opt(0, 0, xs), + ); + }, + ), + test_case( + "split_sublist_opt with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(triple(list(int), list(int), list(int))), + "Split list", + Some(([1, 2], [3, 4], [5])), + ListUtil.split_sublist_opt(2, 4, xs), + ); + }, + ), + test_case( + "split_sublist_opt with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(triple(list(int), list(int), list(int))), + "None", + None, + ListUtil.split_sublist_opt(6, 7, xs), + ); + }, + ), + test_case( + "split_sublist_opt with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + option(triple(list(int), list(int), list(int))), + "Empty first part", + Some(([], [], xs)), + ListUtil.split_sublist_opt(0, 0, xs), + ); + }, + ), + test_case( + "split_sublist with empty list", + `Quick, + () => { + let xs = []; + check( + triple(list(int), list(int), list(int)), + "Empty list", + ([], [], []), + ListUtil.split_sublist(0, 0, xs), + ); + }, + ), + test_case( + "split_sublist with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), list(int), list(int)), + "Split list", + ([1, 2], [3, 4], [5]), + ListUtil.split_sublist(2, 4, xs), + ); + }, + ), + test_case( + "split_sublist with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.split_sublist: 6, 7"), + () => { + let _ = ListUtil.split_sublist(6, 7, xs); + (); + }, + ); + }, + ), + test_case( + "split_sublist with zero index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + triple(list(int), list(int), list(int)), + "Empty first part", + ([], [], xs), + ListUtil.split_sublist(0, 0, xs), + ); + }, + ), + //sublist + test_case( + "sublist with empty list", + `Quick, + () => { + let xs = []; + check(list(int), "Empty list", [], ListUtil.sublist((0, 0), xs)); + }, + ), + test_case( + "sublist with non-empty list", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check( + list(int), + "Sublist", + [2, 3, 4], + ListUtil.sublist((1, 4), xs), + ); + }, + ), + test_case( + "sublist with out of bounds index", + `Quick, + () => { + let xs = [1, 2, 3, 4, 5]; + check_raises( + "raises invalid argument", + Invalid_argument("ListUtil.split_sublist: 6, 7"), + () => { + let _ = ListUtil.sublist((6, 7), xs); + (); + }, + ); + }, + ), ], ); From 0826944e3a8663ea9f05aa5c8cd39ec3c43e17fe Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 16:00:30 -0400 Subject: [PATCH 13/53] Formatting --- src/util/ListUtil.re | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index aed1539298..f7162e5ace 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -174,7 +174,15 @@ let split_sublist_opt = let split_sublist = (i: int, j: int, xs: list('x)): (list('x), list('x), list('x)) => switch (split_sublist_opt(i, j, xs)) { - | None => raise(Invalid_argument("ListUtil.split_sublist: " ++ string_of_int(i) ++ ", " ++ string_of_int(j))) + | None => + raise( + Invalid_argument( + "ListUtil.split_sublist: " + ++ string_of_int(i) + ++ ", " + ++ string_of_int(j), + ), + ) | Some(r) => r }; let sublist = ((i, j), xs: list('x)): list('x) => { From db7eb961a3fe31fcc009426f4defc80aa571a436 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 17 Aug 2024 16:10:10 -0400 Subject: [PATCH 14/53] Remove comments --- test/Test_ListUtil.re | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 509fa9f634..a21ef071d7 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -313,7 +313,12 @@ let tests = ( `Quick, () => { let xs = ["a"]; - check(list(string), "Single element list", ListUtil.join(",", xs), ["a"]); + check( + list(string), + "Single element list", + ListUtil.join(",", xs), + ["a"], + ); }, ), test_case( @@ -421,7 +426,6 @@ let tests = ( ); }, ), - // split_n test_case( "split_n with empty list", `Quick, @@ -476,7 +480,6 @@ let tests = ( ); }, ), - // split_sublist_opt test_case( "split_sublist_opt with empty list", `Quick, @@ -583,7 +586,6 @@ let tests = ( ); }, ), - //sublist test_case( "sublist with empty list", `Quick, From 1cddc4ef668d895189cbe171f436cd8f48631d9b Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 19 Aug 2024 11:41:54 -0400 Subject: [PATCH 15/53] TODOne --- src/util/ListUtil.re | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index f7162e5ace..d2c9a4bbef 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -1,13 +1,5 @@ let rev_if = (b: bool) => b ? List.rev : Fun.id; -// TODO: Replace with dedup_f((==)); -let dedup = xs => - List.fold_right( - (x, deduped) => List.mem(x, deduped) ? deduped : [x, ...deduped], - xs, - [], - ); - let dedup_f = (f, xs) => List.fold_right( (x, deduped) => List.exists(f(x), deduped) ? deduped : [x, ...deduped], @@ -15,11 +7,25 @@ let dedup_f = (f, xs) => [], ); -// TODO: Rename is_unique? +let dedup = xs => dedup_f((==), xs); + let are_duplicates = xs => List.length(List.sort_uniq(compare, xs)) == List.length(xs); -// TODO Interesting that this reverses the list inside the groups +/** + Groups elements of a list by a specified key. + + {b Note: The groups are not guaranteed to preserve the order of elements from the original list. } + + @param key + The key function used to determine the grouping key. + + @param xs + The list of elements to be grouped. + + @return + A list of tuples where each tuple contains the grouping key and a list of elements that belong to that group. +*/ let group_by = (key: 'x => 'k, xs: list('x)): list(('k, list('x))) => List.fold_left( (grouped, x) => { From b93ba919be6fba07adaa53acf1f4255a8260ae4c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 19 Aug 2024 11:56:30 -0400 Subject: [PATCH 16/53] Remove unnecessary whitespace in ListUtil.re --- src/util/ListUtil.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index d2c9a4bbef..39a2d5994e 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -16,7 +16,7 @@ let are_duplicates = xs => Groups elements of a list by a specified key. {b Note: The groups are not guaranteed to preserve the order of elements from the original list. } - + @param key The key function used to determine the grouping key. From 2eddbdc1696ef48e16c9424abc627fbd850a4415 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 19 Aug 2024 12:01:45 -0400 Subject: [PATCH 17/53] Remove comment --- test/Test_ListUtil.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index a21ef071d7..017c2e6d96 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -59,7 +59,7 @@ let tests = ( `Quick, () => { let xs = [1, 2, 3]; - check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right + check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); }, ), test_case( From 3912fa46cbf4b35eefb25cf4e73baa2872b27aa0 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 20 Aug 2024 17:05:00 -0400 Subject: [PATCH 18/53] Mark warnings as errors in release and warnings in dev - Just set it in all the dune files for now --- src/haz3lcore/dune | 4 ++++ src/haz3lschool/dune | 4 ++++ src/haz3lweb/dune | 4 ++++ src/pretty/dune | 4 ++++ src/util/dune | 2 ++ 5 files changed, 18 insertions(+) diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index 77e2ca3fe1..4958c24a03 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -14,8 +14,12 @@ (env (dev + (flags + (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release + (flags + (:standard -warn-error +A)) (js_of_ocaml (flags :standard)))) diff --git a/src/haz3lschool/dune b/src/haz3lschool/dune index a9f7575c78..7523b3b8a5 100644 --- a/src/haz3lschool/dune +++ b/src/haz3lschool/dune @@ -16,8 +16,12 @@ (env (dev + (flags + (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release + (flags + (:standard -warn-error +A)) (js_of_ocaml (flags :standard)))) diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index 8d25155dc5..6bd33aca80 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -78,8 +78,12 @@ (env (dev + (flags + (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release + (flags + (:standard -warn-error +A)) (js_of_ocaml (flags (:standard))))) diff --git a/src/pretty/dune b/src/pretty/dune index 868d03defc..6c6b5ac562 100644 --- a/src/pretty/dune +++ b/src/pretty/dune @@ -8,8 +8,12 @@ (env (dev + (flags + (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release + (flags + (:standard -warn-error +A)) (js_of_ocaml (flags :standard)))) diff --git a/src/util/dune b/src/util/dune index 889c95bd2c..8efc41a81c 100644 --- a/src/util/dune +++ b/src/util/dune @@ -12,8 +12,10 @@ (env (dev + (flags :standard -warn-error -A) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release + (flags :standard -warn-error +A) (js_of_ocaml (flags :standard)))) From abb64a3112f67f15a8372e7d02e72cbd47eb58b4 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 20 Aug 2024 17:16:59 -0400 Subject: [PATCH 19/53] Ignore warning 58 no-cmx-file --- src/haz3lcore/dune | 2 +- src/haz3lschool/dune | 2 +- src/haz3lweb/dune | 2 +- src/pretty/dune | 2 +- src/util/dune | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index 4958c24a03..41cb346136 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -20,6 +20,6 @@ (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release (flags - (:standard -warn-error +A)) + (:standard -warn-error +A-58)) (js_of_ocaml (flags :standard)))) diff --git a/src/haz3lschool/dune b/src/haz3lschool/dune index 7523b3b8a5..12b063be39 100644 --- a/src/haz3lschool/dune +++ b/src/haz3lschool/dune @@ -22,6 +22,6 @@ (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release (flags - (:standard -warn-error +A)) + (:standard -warn-error +A-58)) (js_of_ocaml (flags :standard)))) diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index 6bd33aca80..121bcd65de 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -84,6 +84,6 @@ (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release (flags - (:standard -warn-error +A)) + (:standard -warn-error +A-58)) (js_of_ocaml (flags (:standard))))) diff --git a/src/pretty/dune b/src/pretty/dune index 6c6b5ac562..ad6e9ea4fd 100644 --- a/src/pretty/dune +++ b/src/pretty/dune @@ -14,6 +14,6 @@ (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release (flags - (:standard -warn-error +A)) + (:standard -warn-error +A-58)) (js_of_ocaml (flags :standard)))) diff --git a/src/util/dune b/src/util/dune index 8efc41a81c..a97c31face 100644 --- a/src/util/dune +++ b/src/util/dune @@ -16,6 +16,6 @@ (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release - (flags :standard -warn-error +A) + (flags :standard -warn-error +A-58) (js_of_ocaml (flags :standard)))) From 245ab137250a047081f8a11b658e9c2eecf631d1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 20 Aug 2024 21:00:53 -0400 Subject: [PATCH 20/53] Move flags to dune-workspace --- dune-workspace | 9 +++++++++ src/haz3lcore/dune | 4 ---- src/haz3lschool/dune | 4 ---- src/haz3lweb/dune | 4 ---- src/pretty/dune | 4 ---- 5 files changed, 9 insertions(+), 16 deletions(-) create mode 100644 dune-workspace diff --git a/dune-workspace b/dune-workspace new file mode 100644 index 0000000000..480ccb1514 --- /dev/null +++ b/dune-workspace @@ -0,0 +1,9 @@ +(lang dune 3.16) + +(env + (dev + (flags + (:standard -warn-error -A))) + (release + (flags + (:standard -warn-error +A-58)))) diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index 41cb346136..77e2ca3fe1 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -14,12 +14,8 @@ (env (dev - (flags - (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release - (flags - (:standard -warn-error +A-58)) (js_of_ocaml (flags :standard)))) diff --git a/src/haz3lschool/dune b/src/haz3lschool/dune index 12b063be39..a9f7575c78 100644 --- a/src/haz3lschool/dune +++ b/src/haz3lschool/dune @@ -16,12 +16,8 @@ (env (dev - (flags - (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release - (flags - (:standard -warn-error +A-58)) (js_of_ocaml (flags :standard)))) diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index 121bcd65de..8d25155dc5 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -78,12 +78,8 @@ (env (dev - (flags - (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release - (flags - (:standard -warn-error +A-58)) (js_of_ocaml (flags (:standard))))) diff --git a/src/pretty/dune b/src/pretty/dune index ad6e9ea4fd..868d03defc 100644 --- a/src/pretty/dune +++ b/src/pretty/dune @@ -8,12 +8,8 @@ (env (dev - (flags - (:standard -warn-error -A)) (js_of_ocaml (flags :standard --debuginfo --noinline --dynlink --linkall --sourcemap))) (release - (flags - (:standard -warn-error +A-58)) (js_of_ocaml (flags :standard)))) From fb5b2eb71a67899338f447a8879e91d65a76c0f5 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 23 Aug 2024 16:48:22 -0400 Subject: [PATCH 21/53] Removed are_duplicates --- src/util/ListUtil.re | 3 --- test/Test_ListUtil.re | 16 ---------------- 2 files changed, 19 deletions(-) diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index 39a2d5994e..8481df4f0a 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -9,9 +9,6 @@ let dedup_f = (f, xs) => let dedup = xs => dedup_f((==), xs); -let are_duplicates = xs => - List.length(List.sort_uniq(compare, xs)) == List.length(xs); - /** Groups elements of a list by a specified key. diff --git a/test/Test_ListUtil.re b/test/Test_ListUtil.re index 017c2e6d96..9abfca4f07 100644 --- a/test/Test_ListUtil.re +++ b/test/Test_ListUtil.re @@ -46,22 +46,6 @@ let tests = ( ); // TODO: Interesting the order here is messed up because of fold_right }, ), - test_case( - "are_duplicates has duplicates", - `Quick, - () => { - let xs = [1, 2, 3, 2]; - check(bool, "Returns false", false, ListUtil.are_duplicates(xs)); // TODO: Interesting the order here is messed up because of fold_right - }, - ), - test_case( - "are_duplicates has no duplicates", - `Quick, - () => { - let xs = [1, 2, 3]; - check(bool, "Returns true", true, ListUtil.are_duplicates(xs)); - }, - ), test_case( "group_by with constant function preserves list", `Quick, From a07e1153f24b6d46e739474633fa9f3f6312e0cf Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 12 Sep 2024 11:15:46 -0400 Subject: [PATCH 22/53] In progress commit --- src/haz3lcore/dynamics/FilterEnvironment.re | 2 +- src/haz3lcore/lang/term/TPat.re | 2 +- src/haz3lcore/lang/term/Typ.re | 5 +- src/haz3lcore/statics/Ctx.re | 15 +- src/haz3lcore/statics/Term.re | 6 +- src/haz3lcore/statics/TermBase.re | 439 ++++++++------------ 6 files changed, 179 insertions(+), 290 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterEnvironment.re b/src/haz3lcore/dynamics/FilterEnvironment.re index 284e7353d3..ac59a874bc 100644 --- a/src/haz3lcore/dynamics/FilterEnvironment.re +++ b/src/haz3lcore/dynamics/FilterEnvironment.re @@ -1,2 +1,2 @@ -type t = list(TermBase.StepperFilterKind.filter); +type t = list(TermBase.filter); let extends = (flt, env) => [flt, ...env]; diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re index 3dade36b54..583f805851 100644 --- a/src/haz3lcore/lang/term/TPat.re +++ b/src/haz3lcore/lang/term/TPat.re @@ -10,7 +10,7 @@ include TermBase.TPat; let rep_id: t => Id.t = IdTagged.rep_id; let fresh: term => t = IdTagged.fresh; -let hole = (tms: list(TermBase.Any.t)) => +let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term => switch (tms) { | [] => EmptyHole | [_, ..._] => MultiHole(tms) diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re index 5dc0b73aaa..c9a6f0c204 100644 --- a/src/haz3lcore/lang/term/Typ.re +++ b/src/haz3lcore/lang/term/Typ.re @@ -34,7 +34,7 @@ let fresh: term => t = IdTagged.fresh; let temp: term => t = term => {term, ids: [Id.invalid], copied: false}; let rep_id: t => Id.t = IdTagged.rep_id; -let hole = (tms: list(TermBase.Any.t)) => +let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term => switch (tms) { | [] => Unknown(Hole(EmptyHole)) | [_, ..._] => Unknown(Hole(MultiHole(tms))) @@ -137,7 +137,8 @@ let of_source = List.map((source: source) => source.ty); but right now TypeHole strictly predominates over Internal which strictly predominates over SynSwitch. */ let join_type_provenance = - (p1: type_provenance, p2: type_provenance): type_provenance => + (p1: TermBase.type_provenance, p2: TermBase.type_provenance) + : TermBase.type_provenance => switch (p1, p2) { | (Hole(h1), Hole(h2)) when h1 == h2 => Hole(h1) | (Hole(EmptyHole), Hole(EmptyHole) | SynSwitch) diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re index 9791b6cd0f..f213a18cb7 100644 --- a/src/haz3lcore/statics/Ctx.re +++ b/src/haz3lcore/statics/Ctx.re @@ -2,14 +2,14 @@ open Util; [@deriving (show({with_path: false}), sexp, yojson)] type kind = - | Singleton(TermBase.Typ.t) + | Singleton(TermBase.typ_t) | Abstract; [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { name: Var.t, id: Id.t, - typ: TermBase.Typ.t, + typ: TermBase.typ_t, }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -99,7 +99,9 @@ let lookup_alias = (ctx: t, name: string): option(TermBase.Typ.t) => | Some(Singleton(ty)) => Some(ty) | Some(Abstract) => None | None => - Some(TermBase.Typ.Unknown(Hole(Invalid(name))) |> IdTagged.fresh) + Some( + (Unknown(Hole(Invalid(name))): TermBase.Typ.term) |> IdTagged.fresh, + ) }; let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t => @@ -112,11 +114,10 @@ let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t = id, typ: switch (typ) { - | None => TermBase.Typ.Var(name) |> IdTagged.fresh + | None => (Var(name): TermBase.typ_term) |> IdTagged.fresh | Some(typ) => - TermBase.Typ.Arrow( - typ, - TermBase.Typ.Var(name) |> IdTagged.fresh, + ( + Arrow(typ, (Var(name): TermBase.typ_term) |> IdTagged.fresh): TermBase.typ_term ) |> IdTagged.fresh }, diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 0493150865..92eef8161e 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -31,7 +31,7 @@ module Pat = { let fresh: term => t = IdTagged.fresh; - let hole = (tms: list(TermBase.Any.t)) => + let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term => switch (tms) { | [] => EmptyHole | [_, ..._] => MultiHole(tms) @@ -597,7 +597,7 @@ module Any = { | Typ(t) => Some(t) | _ => None; - let rec ids = + let rec ids: TermBase.any_t => list(Id.t) = fun | Exp(tm) => tm.ids | Pat(tm) => tm.ids @@ -620,7 +620,7 @@ module Any = { // (This would change for n-tuples if we decided parentheses are necessary.) let rep_id = fun - | Exp(tm) => Exp.rep_id(tm) + | (Exp(tm): TermBase.any_t) => Exp.rep_id(tm) | Pat(tm) => Pat.rep_id(tm) | Typ(tm) => Typ.rep_id(tm) | TPat(tm) => TPat.rep_id(tm) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index f0585955c6..67e6f1ecde 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -2,6 +2,10 @@ open Util; let continue = x => x; let stop = (_, x) => x; +[@deriving (show({with_path: false}), sexp, yojson)] +type deferral_position = + | InAp + | OutsideAp; /* This megafile contains the definitions of the expression data types in @@ -42,16 +46,126 @@ let stop = (_, x) => x; the id of the closure. */ +[@deriving (show({with_path: false}), sexp, yojson)] +type any_t = + | Exp(exp_t) + | Pat(pat_t) + | Typ(typ_t) + | TPat(tpat_t) + | Rul(rul_t) + | Nul(unit) + | Any(unit) +and exp_term = + | Invalid(string) + | EmptyHole + | MultiHole(list(any_t)) + | DynamicErrorHole(exp_t, InvalidOperationError.t) + | FailedCast(exp_t, typ_t, typ_t) + | Deferral(deferral_position) + | Undefined + | Bool(bool) + | Int(int) + | Float(float) + | String(string) + | ListLit(list(exp_t)) + | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic expressions + | Fun( + pat_t, + exp_t, + [@show.opaque] option(closure_environment_t), + option(Var.t), + ) + | TypFun(tpat_t, exp_t, option(Var.t)) + | Tuple(list(exp_t)) + | Var(Var.t) + | Let(pat_t, exp_t, exp_t) + | FixF(pat_t, exp_t, option(closure_environment_t)) + | TyAlias(tpat_t, typ_t, exp_t) + | Ap(Operators.ap_direction, exp_t, exp_t) + | TypAp(exp_t, typ_t) + | DeferredAp(exp_t, list(exp_t)) + | If(exp_t, exp_t, exp_t) + | Seq(exp_t, exp_t) + | Test(exp_t) + | Filter(stepper_filter_kind_t, exp_t) + | Closure([@show.opaque] closure_environment_t, exp_t) + | Parens(exp_t) // ( + | Cons(exp_t, exp_t) + | ListConcat(exp_t, exp_t) + | UnOp(Operators.op_un, exp_t) + | BinOp(Operators.op_bin, exp_t, exp_t) + | BuiltinFun(string) + | Match(exp_t, list((pat_t, exp_t))) + /* INVARIANT: in dynamic expressions, casts must be between + two consistent types. Both types should be normalized in + dynamics for the cast calculus to work right. */ + | Cast(exp_t, typ_t, typ_t) +and exp_t = IdTagged.t(exp_term) +and pat_term = + | Invalid(string) + | EmptyHole + | MultiHole(list(any_t)) + | Wild + | Int(int) + | Float(float) + | Bool(bool) + | String(string) + | ListLit(list(pat_t)) + | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic patterns + | Cons(pat_t, pat_t) + | Var(Var.t) + | Tuple(list(pat_t)) + | Parens(pat_t) + | Ap(pat_t, pat_t) + | Cast(pat_t, typ_t, typ_t) +and pat_t = IdTagged.t(pat_term) +and typ_term = + | Unknown(type_provenance) + | Int + | Float + | Bool + | String + | Var(string) + | List(typ_t) + | Arrow(typ_t, typ_t) + | Sum(ConstructorMap.t(typ_t)) + | Prod(list(typ_t)) + | Parens(typ_t) + | Ap(typ_t, typ_t) + | Rec(tpat_t, typ_t) + | Forall(tpat_t, typ_t) +and typ_t = IdTagged.t(typ_term) +and tpat_term = + | Invalid(string) + | EmptyHole + | MultiHole(list(any_t)) + | Var(string) +and tpat_t = IdTagged.t(tpat_term) +and rul_term = + | Invalid(string) + | Hole(list(any_t)) + | Rules(exp_t, list((pat_t, exp_t))) +and rul_t = IdTagged.t(rul_term) +and environment_t = VarBstMap.Ordered.t_(exp_t) +and closure_environment_t = (Id.t, environment_t) +and stepper_filter_kind_t = + | Filter(filter) + | Residue(int, FilterAction.t) +and type_hole = + | Invalid(string) + | EmptyHole + | MultiHole(list(any_t)) +and type_provenance = + | SynSwitch + | Hole(type_hole) + | Internal +and filter = { + pat: exp_t, + act: FilterAction.t, +}; + module rec Any: { - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Exp(Exp.t) - | Pat(Pat.t) - | Typ(Typ.t) - | TPat(TPat.t) - | Rul(Rul.t) - | Nul(unit) - | Any(unit); + type t = any_t; let map_term: ( @@ -67,15 +181,7 @@ module rec Any: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Exp(Exp.t) - | Pat(Pat.t) - | Typ(Typ.t) - | TPat(TPat.t) - | Rul(Rul.t) - | Nul(unit) - | Any(unit); + type t = any_t; let map_term = ( @@ -126,58 +232,8 @@ module rec Any: { }; } and Exp: { - [@deriving (show({with_path: false}), sexp, yojson)] - type deferral_position = - | InAp - | OutsideAp; - - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | DynamicErrorHole(t, InvalidOperationError.t) - | FailedCast(t, Typ.t, Typ.t) - | Deferral(deferral_position) - | Undefined - | Bool(bool) - | Int(int) - | Float(float) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic expressions - | Fun( - Pat.t, - t, - [@show.opaque] option(ClosureEnvironment.t), - option(Var.t), - ) - | TypFun(TPat.t, t, option(Var.t)) - | Tuple(list(t)) - | Var(Var.t) - | Let(Pat.t, t, t) - | FixF(Pat.t, t, option(ClosureEnvironment.t)) - | TyAlias(TPat.t, Typ.t, t) - | Ap(Operators.ap_direction, t, t) - | TypAp(t, Typ.t) - | DeferredAp(t, list(t)) - | If(t, t, t) - | Seq(t, t) - | Test(t) - | Filter(StepperFilterKind.t, t) - | Closure([@show.opaque] ClosureEnvironment.t, t) - | Parens(t) // ( - | Cons(t, t) - | ListConcat(t, t) - | UnOp(Operators.op_un, t) - | BinOp(Operators.op_bin, t, t) - | BuiltinFun(string) - | Match(t, list((Pat.t, t))) - /* INVARIANT: in dynamic expressions, casts must be between - two consistent types. Both types should be normalized in - dynamics for the cast calculus to work right. */ - | Cast(t, Typ.t, Typ.t) // first Typ.t field is only meaningful in dynamic expressions - and t = IdTagged.t(term); + type term = exp_term; + type t = exp_t; let map_term: ( @@ -193,55 +249,8 @@ and Exp: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type deferral_position = - | InAp - | OutsideAp; - - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | DynamicErrorHole(t, InvalidOperationError.t) - | FailedCast(t, Typ.t, Typ.t) - | Deferral(deferral_position) - | Undefined - | Bool(bool) - | Int(int) - | Float(float) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) - | Fun( - Pat.t, - t, - [@show.opaque] option(ClosureEnvironment.t), - option(Var.t), - ) - | TypFun(TPat.t, t, option(string)) - | Tuple(list(t)) - | Var(Var.t) - | Let(Pat.t, t, t) - | FixF(Pat.t, t, [@show.opaque] option(ClosureEnvironment.t)) - | TyAlias(TPat.t, Typ.t, t) - | Ap(Operators.ap_direction, t, t) // note: function is always first then argument; even in pipe mode - | TypAp(t, Typ.t) - | DeferredAp(t, list(t)) - | If(t, t, t) - | Seq(t, t) - | Test(t) - | Filter(StepperFilterKind.t, t) - | Closure([@show.opaque] ClosureEnvironment.t, t) - | Parens(t) - | Cons(t, t) - | ListConcat(t, t) - | UnOp(Operators.op_un, t) - | BinOp(Operators.op_bin, t, t) - | BuiltinFun(string) /// Doesn't currently have a distinguishable syntax - | Match(t, list((Pat.t, t))) - | Cast(t, Typ.t, Typ.t) - and t = IdTagged.t(term); + type term = exp_term; + type t = exp_t; let map_term = ( @@ -447,25 +456,8 @@ and Exp: { }; } and Pat: { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Wild - | Int(int) - | Float(float) - | Bool(bool) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic patterns - | Cons(t, t) - | Var(Var.t) - | Tuple(list(t)) - | Parens(t) - | Ap(t, t) - | Cast(t, Typ.t, Typ.t) // The second Typ.t field is only meaningful in dynamic patterns - and t = IdTagged.t(term); + type term = pat_term; // The second Typ.t field is only meaningful in dynamic patterns + type t = pat_t; let map_term: ( @@ -481,25 +473,8 @@ and Pat: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Wild - | Int(int) - | Float(float) - | Bool(bool) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) - | Cons(t, t) - | Var(Var.t) - | Tuple(list(t)) - | Parens(t) - | Ap(t, t) - | Cast(t, Typ.t, Typ.t) // The second one is hidden from the user - and t = IdTagged.t(term); + type term = pat_term; + type t = pat_t; let map_term = ( @@ -543,7 +518,7 @@ and Pat: { x |> f_pat(rec_call); }; - let rec fast_equal = (p1, p2) => + let rec fast_equal = (p1: t, p2: t) => switch (p1 |> IdTagged.term_of, p2 |> IdTagged.term_of) { | (Parens(x), _) => fast_equal(x, p2) | (_, Parens(x)) => fast_equal(p1, x) @@ -588,38 +563,9 @@ and Pat: { } and Typ: { [@deriving (show({with_path: false}), sexp, yojson)] - type type_hole = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)); - - /* TYPE_PROVENANCE: From whence does an unknown type originate? - Is it generated from an unannotated pattern variable (SynSwitch), - a pattern variable annotated with a type hole (TypeHole), or - generated by an internal judgement (Internal)? */ - [@deriving (show({with_path: false}), sexp, yojson)] - type type_provenance = - | SynSwitch - | Hole(type_hole) - | Internal; - + type term = typ_term; [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Unknown(Typ.type_provenance) - | Int - | Float - | Bool - | String - | Var(string) - | List(t) - | Arrow(t, t) - | Sum(ConstructorMap.t(t)) - | Prod(list(t)) - | Parens(t) - | Ap(t, t) - | Rec(TPat.t, t) - | Forall(TPat.t, t) - and t = IdTagged.t(term); + type t = typ_t; type sum_map = ConstructorMap.t(t); @@ -640,38 +586,9 @@ and Typ: { let fast_equal: (t, t) => bool; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type type_hole = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)); - - /* TYPE_PROVENANCE: From whence does an unknown type originate? - Is it generated from an unannotated pattern variable (SynSwitch), - a pattern variable annotated with a type hole (TypeHole), or - generated by an internal judgement (Internal)? */ + type term = typ_term; [@deriving (show({with_path: false}), sexp, yojson)] - type type_provenance = - | SynSwitch - | Hole(type_hole) - | Internal; - - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Unknown(Typ.type_provenance) - | Int - | Float - | Bool - | String - | Var(string) - | List(t) - | Arrow(t, t) - | Sum(ConstructorMap.t(t)) - | Prod(list(t)) - | Parens(t) - | Ap(t, t) - | Rec(TPat.t, t) - | Forall(TPat.t, t) - and t = IdTagged.t(term); + type t = typ_t; type sum_map = ConstructorMap.t(t); @@ -729,12 +646,12 @@ and Typ: { x |> f_typ(rec_call); }; - let rec subst = (s: t, x: TPat.t, ty: t) => { + let rec subst = (s: t, x: TPat.t, ty: t): typ_t => { switch (TPat.tyvar_of_utpat(x)) { | Some(str) => let (term, rewrap) = IdTagged.unwrap(ty); switch (term) { - | Int => Int |> rewrap + | Int => (Int: typ_term) |> rewrap | Float => Float |> rewrap | Bool => Bool |> rewrap | String => String |> rewrap @@ -811,12 +728,8 @@ and Typ: { } and TPat: { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Var(string) - and t = IdTagged.t(term); + type term = tpat_term; + type t = tpat_t; let map_term: ( @@ -835,12 +748,8 @@ and TPat: { let fast_equal: (t, t) => bool; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Var(string) - and t = IdTagged.t(term); + type term = tpat_term; + type t = tpat_t; let map_term = ( @@ -889,11 +798,8 @@ and TPat: { } and Rul: { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | Hole(list(Any.t)) - | Rules(Exp.t, list((Pat.t, Exp.t))) - and t = IdTagged.t(term); + type term = rul_term; + type t = rul_t; let map_term: ( @@ -910,11 +816,9 @@ and Rul: { let fast_equal: (t, t) => bool; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | Hole(list(Any.t)) - | Rules(Exp.t, list((Pat.t, Exp.t))) - and t = IdTagged.t(term); + type term = rul_term; + [@deriving (show({with_path: false}), sexp, yojson)] + type t = rul_t; let map_term = ( @@ -977,13 +881,11 @@ and Environment: { (module type of VarBstMap.Ordered) with type t_('a) = VarBstMap.Ordered.t_('a); - [@deriving (show({with_path: false}), sexp, yojson)] - type t = t_(Exp.t); + type t = environment_t; } = { include VarBstMap.Ordered; - [@deriving (show({with_path: false}), sexp, yojson)] - type t = t_(Exp.t); + type t = environment_t; } and ClosureEnvironment: { @@ -999,7 +901,7 @@ and ClosureEnvironment: { let of_environment: Environment.t => t; - let id_equal: (t, t) => bool; + let id_equal: (closure_environment_t, closure_environment_t) => bool; let empty: t; let is_empty: t => bool; @@ -1025,7 +927,7 @@ and ClosureEnvironment: { } = { module Inner: { [@deriving (show({with_path: false}), sexp, yojson)] - type t; + type t = closure_environment_t; let wrap: (Id.t, Environment.t) => t; @@ -1033,7 +935,7 @@ and ClosureEnvironment: { let map_of: t => Environment.t; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type t = (Id.t, Environment.t); + type t = closure_environment_t; let wrap = (ei, map): t => (ei, map); @@ -1099,16 +1001,7 @@ and ClosureEnvironment: { let without_keys = keys => update(Environment.without_keys(keys)); } and StepperFilterKind: { - [@deriving (show({with_path: false}), sexp, yojson)] - type filter = { - pat: Exp.t, - act: FilterAction.t, - }; - - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Filter(filter) - | Residue(int, FilterAction.t); + type t = stepper_filter_kind_t; let map_term: ( @@ -1126,18 +1019,9 @@ and StepperFilterKind: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type filter = { - pat: Exp.t, - act: FilterAction.t, - }; + type t = stepper_filter_kind_t; - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Filter(filter) - | Residue(int, FilterAction.t); - - let map = (mapper, filter) => { + let map = (mapper, filter: t): t => { switch (filter) { | Filter({act, pat}) => Filter({act, pat: mapper(pat)}) | Residue(idx, act) => Residue(idx, act) @@ -1155,12 +1039,15 @@ and StepperFilterKind: { ) => { let exp_map_term = Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any); - fun - | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act}) - | Residue(i, a) => Residue(i, a); + ( + fun + | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act}) + | Residue(i, a) => Residue(i, a): + t => t + ); }; - let fast_equal = (f1, f2) => + let fast_equal = (f1: t, f2: t) => switch (f1, f2) { | (Filter({pat: e1, act: a1}), Filter({pat: e2, act: a2})) => Exp.fast_equal(e1, e2) && a1 == a2 From 370e7aa06979aac3463ca9aa71768e2fd73b72b1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 12 Sep 2024 12:29:28 -0400 Subject: [PATCH 23/53] Finished the refactor --- src/haz3lcore/dynamics/Builtins.re | 21 ++- src/haz3lcore/dynamics/Casts.re | 18 +- src/haz3lcore/dynamics/Elaborator.re | 77 ++++----- src/haz3lcore/dynamics/EvalCtx.re | 199 +++++++++++------------ src/haz3lcore/dynamics/FilterMatcher.re | 32 ++-- src/haz3lcore/dynamics/TypeAssignment.re | 12 +- src/haz3lcore/dynamics/ValueChecker.re | 1 - src/haz3lcore/prog/CachedStatics.re | 6 +- src/haz3lcore/statics/MakeTerm.re | 10 +- src/haz3lcore/statics/Mode.re | 3 +- src/haz3lcore/statics/Statics.re | 17 +- src/haz3lcore/statics/TermBase.re | 26 ++- src/haz3lcore/zipper/Editor.re | 6 +- src/haz3lcore/zipper/EditorUtil.re | 94 ++++++----- src/haz3lschool/Exercise.re | 33 ++-- src/haz3lweb/view/Cell.re | 2 +- src/haz3lweb/view/ExplainThis.re | 6 +- src/haz3lweb/view/Type.re | 4 +- 18 files changed, 285 insertions(+), 282 deletions(-) diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index 4479989fd5..c47617edc6 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -41,13 +41,13 @@ let fn = module Pervasives = { module Impls = { /* constants */ - let infinity = DHExp.Float(Float.infinity) |> fresh; - let neg_infinity = DHExp.Float(Float.neg_infinity) |> fresh; - let nan = DHExp.Float(Float.nan) |> fresh; - let epsilon_float = DHExp.Float(epsilon_float) |> fresh; - let pi = DHExp.Float(Float.pi) |> fresh; - let max_int = DHExp.Int(Int.max_int) |> fresh; - let min_int = DHExp.Int(Int.min_int) |> fresh; + let infinity = Float(Float.infinity) |> fresh; + let neg_infinity = Float(Float.neg_infinity) |> fresh; + let nan = Float(Float.nan) |> fresh; + let epsilon_float = Float(epsilon_float) |> fresh; + let pi = Float(Float.pi) |> fresh; + let max_int = Int(Int.max_int) |> fresh; + let min_int = Int(Int.min_int) |> fresh; let unary = (f: DHExp.t => result, d: DHExp.t) => { switch (f(d)) { @@ -180,8 +180,8 @@ module Pervasives = { switch (convert(s)) { | Some(n) => Ok(wrap(n)) | None => - let d' = DHExp.BuiltinFun(name) |> DHExp.fresh; - let d' = DHExp.Ap(Forward, d', d) |> DHExp.fresh; + let d' = BuiltinFun(name) |> DHExp.fresh; + let d' = Ap(Forward, d', d) |> DHExp.fresh; let d' = DynamicErrorHole(d', InvalidOfString) |> DHExp.fresh; Ok(d'); } @@ -204,8 +204,7 @@ module Pervasives = { Ok( fresh( DynamicErrorHole( - DHExp.Ap(Forward, DHExp.BuiltinFun(name) |> fresh, d1) - |> fresh, + Ap(Forward, BuiltinFun(name) |> fresh, d1) |> fresh, DivideByZero, ), ), diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re index 170d057e76..a69f560dd5 100644 --- a/src/haz3lcore/dynamics/Casts.re +++ b/src/haz3lcore/dynamics/Casts.re @@ -39,7 +39,7 @@ let grounded_Forall = ); let grounded_Prod = length => NotGroundOrHole( - Prod(ListUtil.replicate(length, Typ.Unknown(Internal) |> Typ.temp)) + Prod(ListUtil.replicate(length, Unknown(Internal) |> Typ.temp)) |> Typ.temp, ); let grounded_Sum: unit => Typ.sum_map = @@ -50,7 +50,7 @@ let grounded_List = let rec ground_cases_of = (ty: Typ.t): ground_cases => { let is_hole: Typ.t => bool = fun - | {term: Typ.Unknown(_), _} => true + | {term: Unknown(_), _} => true | _ => false; switch (Typ.term_of(ty)) { | Unknown(_) => Hole @@ -67,7 +67,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Prod(tys) => if (List.for_all( fun - | ({term: Typ.Unknown(_), _}: Typ.t) => true + | ({term: Unknown(_), _}: Typ.t) => true | _ => false, tys, )) { @@ -132,12 +132,12 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => { | Some(d1) => d1 | None => inner_cast }; - Some(DHExp.Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh); + Some(Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh); | (NotGroundOrHole(t1_grounded), Hole) => /* ITGround rule */ Some( - DHExp.Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2) + Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2) |> DHExp.fresh, ) @@ -187,7 +187,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => { let (p1, d1) = unwrap_casts(p1); ( p1, - {term: DHExp.Cast(d1, t1, t2), copied: p.copied, ids: p.ids} + {term: Cast(d1, t1, t2), copied: p.copied, ids: p.ids} |> transition_multiple, ); | _ => (p, hole) @@ -198,13 +198,13 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => { | EmptyHole => p | Cast(d1, t1, t2) => let p1 = rewrap_casts((p, d1)); - {term: DHPat.Cast(p1, t1, t2), copied: d.copied, ids: d.ids}; + {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids}; | FailedCast(d1, t1, t2) => let p1 = rewrap_casts((p, d1)); { term: - DHPat.Cast( - DHPat.Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh, + Cast( + Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh, Typ.fresh(Unknown(Internal)), t2, ), diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index c1f3aa12d7..d50d462064 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -23,10 +23,10 @@ let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): DHExp.t => { ? d : { let d' = - DHExp.Cast(d, t1, Typ.temp(Unknown(Internal))) + Cast(d, t1, Typ.temp(Unknown(Internal))) |> DHExp.fresh |> Casts.transition_multiple; - DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2) + Cast(d', Typ.temp(Unknown(Internal)), t2) |> DHExp.fresh |> Casts.transition_multiple; }; @@ -63,11 +63,11 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => { | Syn => self_ty | SynFun => let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty); - Typ.Arrow(ty1, ty2) |> Typ.temp; + Arrow(ty1, ty2) |> Typ.temp; | SynTypFun => let (tpat, ty) = Typ.matched_forall(ctx, self_ty); let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole)); - Typ.Forall(tpat, ty) |> Typ.temp; + Forall(tpat, ty) |> Typ.temp; // We need to remove the synswitches from this type. | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty) }; @@ -90,11 +90,11 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => { | Syn => self_ty | SynFun => let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty); - Typ.Arrow(ty1, ty2) |> Typ.temp; + Arrow(ty1, ty2) |> Typ.temp; | SynTypFun => let (tpat, ty) = Typ.matched_forall(ctx, self_ty); let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole)); - Typ.Forall(tpat, ty) |> Typ.temp; + Forall(tpat, ty) |> Typ.temp; | Ana(ana_ty) => switch (prev_synswitch) { | None => ana_ty @@ -125,9 +125,7 @@ let rec elaborate_pattern = |> List.map2((p, t) => fresh_pat_cast(p, t, inner_type), _, tys) |> ( ps' => - DHPat.ListLit(ps') - |> rewrap - |> cast_from(List(inner_type) |> Typ.temp) + ListLit(ps') |> rewrap |> cast_from(List(inner_type) |> Typ.temp) ); | Cons(p1, p2) => let (p1', ty1) = elaborate_pattern(m, p1); @@ -138,19 +136,17 @@ let rec elaborate_pattern = |> Option.value(~default=Typ.temp(Unknown(Internal))); let p1'' = fresh_pat_cast(p1', ty1, ty_inner); let p2'' = fresh_pat_cast(p2', ty2, List(ty_inner) |> Typ.temp); - DHPat.Cons(p1'', p2'') - |> rewrap - |> cast_from(List(ty_inner) |> Typ.temp); + Cons(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp); | Tuple(ps) => let (ps', tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip; - DHPat.Tuple(ps') |> rewrap |> cast_from(Typ.Prod(tys) |> Typ.temp); + Tuple(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp); | Ap(p1, p2) => let (p1', ty1) = elaborate_pattern(m, p1); let (p2', ty2) = elaborate_pattern(m, p2); let (ty1l, ty1r) = Typ.matched_arrow(ctx, ty1); let p1'' = fresh_pat_cast(p1', ty1, Arrow(ty1l, ty1r) |> Typ.temp); let p2'' = fresh_pat_cast(p2', ty2, ty1l); - DHPat.Ap(p1'', p2'') |> rewrap |> cast_from(ty1r); + Ap(p1'', p2'') |> rewrap |> cast_from(ty1r); | Invalid(_) | EmptyHole | MultiHole(_) @@ -213,7 +209,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { switch (term) { | Invalid(_) | Undefined - | EmptyHole => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal))) + | EmptyHole => uexp |> cast_from(Typ.temp(Unknown(Internal))) | MultiHole(stuff) => Any.map_term( ~f_exp=(_, exp) => {elaborate(m, exp) |> fst}, @@ -223,9 +219,9 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { |> List.map(_, stuff) |> ( stuff => - DHExp.MultiHole(stuff) + MultiHole(stuff) |> rewrap - |> cast_from(Typ.temp(Typ.Unknown(Internal))) + |> cast_from(Typ.temp(Unknown(Internal))) ) | DynamicErrorHole(e, err) => let (e', _) = elaborate(m, e); @@ -245,10 +241,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { | ListLit(es) => let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip; let inner_type = - Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, tys) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, tys) + |> Option.value(~default=Typ.temp(Unknown(Internal))); let ds' = List.map2((d, t) => fresh_cast(d, t, inner_type), ds, tys); - Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp); + ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp); | Constructor(c, _) => let mode = switch (Id.Map.find_opt(Exp.rep_id(uexp), m)) { @@ -266,23 +262,23 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { | Fun(p, e, env, n) => let (p', typ) = elaborate_pattern(m, p); let (e', tye) = elaborate(m, e); - Exp.Fun(p', e', env, n) + Fun(p', e', env, n) |> rewrap |> cast_from(Arrow(typ, tye) |> Typ.temp); | TypFun(tpat, e, name) => let (e', tye) = elaborate(m, e); - Exp.TypFun(tpat, e', name) + TypFun(tpat, e', name) |> rewrap - |> cast_from(Typ.Forall(tpat, tye) |> Typ.temp); + |> cast_from(Forall(tpat, tye) |> Typ.temp); | Tuple(es) => let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip; - Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp); + Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp); | Var(v) => uexp |> cast_from( Ctx.lookup_var(ctx, v) |> Option.map((x: Ctx.var_entry) => x.typ |> Typ.normalize(ctx)) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))), + |> Option.value(~default=Typ.temp(Unknown(Internal))), ) | Let(p, def, body) => let add_name: (option(string), DHExp.t) => DHExp.t = ( @@ -305,9 +301,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let def = add_name(Pat.get_var(p), def); let (def, ty2) = elaborate(m, def); let (body, ty) = elaborate(m, body); - Exp.Let(p, fresh_cast(def, ty2, ty1), body) - |> rewrap - |> cast_from(ty); + Let(p, fresh_cast(def, ty2, ty1), body) |> rewrap |> cast_from(ty); } else { // TODO: Add names to mutually recursive functions // TODO: Don't add fixpoint if there already is one @@ -315,14 +309,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (def, ty2) = elaborate(m, def); let (body, ty) = elaborate(m, body); let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh; - Exp.Let(p, fixf, body) |> rewrap |> cast_from(ty); + Let(p, fixf, body) |> rewrap |> cast_from(ty); }; | FixF(p, e, env) => let (p', typ) = elaborate_pattern(m, p); let (e', tye) = elaborate(m, e); - Exp.FixF(p', fresh_cast(e', tye, typ), env) - |> rewrap - |> cast_from(typ); + FixF(p', fresh_cast(e', tye, typ), env) |> rewrap |> cast_from(typ); | TyAlias(_, _, e) => let (e', tye) = elaborate(m, e); e' |> cast_from(tye); @@ -332,7 +324,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf); let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp); let a'' = fresh_cast(a', tya, tyf1); - Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2); + Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2); | DeferredAp(f, args) => let (f', tyf) = elaborate(m, f); let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip; @@ -371,11 +363,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (f', tyf) = elaborate(m, f); let ty = Typ.join(~fix=false, ctx, tyt, tyf) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + |> Option.value(~default=Typ.temp(Unknown(Internal))); let c'' = fresh_cast(c', tyc, Bool |> Typ.temp); let t'' = fresh_cast(t', tyt, ty); let f'' = fresh_cast(f', tyf, ty); - Exp.If(c'', t'', f'') |> rewrap |> cast_from(ty); + If(c'', t'', f'') |> rewrap |> cast_from(ty); | Seq(e1, e2) => let (e1', _) = elaborate(m, e1); let (e2', ty2) = elaborate(m, e2); @@ -427,10 +419,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { Constructor("$e", Unknown(Internal) |> Typ.temp) |> rewrap | Var("v") => Constructor("$v", Unknown(Internal) |> Typ.temp) |> rewrap - | _ => - DHExp.EmptyHole - |> rewrap - |> cast_from(Typ.temp(Typ.Unknown(Internal))) + | _ => EmptyHole |> rewrap |> cast_from(Typ.temp(Unknown(Internal))) } | UnOp(Int(Minus), e) => let (e', t) = elaborate(m, e); @@ -533,7 +522,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { |> cast_from( Ctx.lookup_var(Builtins.ctx_init, fn) |> Option.map((x: Ctx.var_entry) => x.typ) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))), + |> Option.value(~default=Typ.temp(Unknown(Internal))), ) | Match(e, cases) => let (e', t) = elaborate(m, e); @@ -541,15 +530,15 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (ps', ptys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip; let joined_pty = - Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, ptys) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, ptys) + |> Option.value(~default=Typ.temp(Unknown(Internal))); let ps'' = List.map2((p, t) => fresh_pat_cast(p, t, joined_pty), ps', ptys); let e'' = fresh_cast(e', t, joined_pty); let (es', etys) = List.map(elaborate(m), es) |> ListUtil.unzip; let joined_ety = - Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, etys) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, etys) + |> Option.value(~default=Typ.temp(Unknown(Internal))); let es'' = List.map2((e, t) => fresh_cast(e, t, joined_ety), es', etys); Match(e'', List.combine(ps'', es'')) diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re index bed931c8d3..1f60bfa70a 100644 --- a/src/haz3lcore/dynamics/EvalCtx.re +++ b/src/haz3lcore/dynamics/EvalCtx.re @@ -51,106 +51,103 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => { | Mark => d | Term({term, ids}) => let wrap = DHExp.mk(ids); - DHExp.( - switch (term) { - | Closure(env, ctx) => - let d = compose(ctx, d); - Closure(env, d) |> wrap; - | Filter(flt, ctx) => - let d = compose(ctx, d); - Filter(flt, d) |> wrap; - | Seq1(ctx, d2) => - let d1 = compose(ctx, d); - Seq(d1, d2) |> wrap; - | Seq2(d1, ctx) => - let d2 = compose(ctx, d); - Seq(d1, d2) |> wrap; - | Ap1(dir, ctx, d2) => - let d1 = compose(ctx, d); - Ap(dir, d1, d2) |> wrap; - | Ap2(dir, d1, ctx) => - let d2 = compose(ctx, d); - Ap(dir, d1, d2) |> wrap; - | DeferredAp1(ctx, d2s) => - let d1 = compose(ctx, d); - DeferredAp(d1, d2s) |> wrap; - | DeferredAp2(d1, ctx, (ld, rd)) => - let d2 = compose(ctx, d); - DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap; - | If1(ctx, d2, d3) => - let d' = compose(ctx, d); - If(d', d2, d3) |> wrap; - | If2(d1, ctx, d3) => - let d' = compose(ctx, d); - If(d1, d', d3) |> wrap; - | If3(d1, d2, ctx) => - let d' = compose(ctx, d); - If(d1, d2, d') |> wrap; - | Test(ctx) => - let d1 = compose(ctx, d); - Test(d1) |> wrap; - | UnOp(op, ctx) => - let d1 = compose(ctx, d); - UnOp(op, d1) |> wrap; - | BinOp1(op, ctx, d2) => - let d1 = compose(ctx, d); - BinOp(op, d1, d2) |> wrap; - | BinOp2(op, d1, ctx) => - let d2 = compose(ctx, d); - BinOp(op, d1, d2) |> wrap; - | Cons1(ctx, d2) => - let d1 = compose(ctx, d); - Cons(d1, d2) |> wrap; - | Cons2(d1, ctx) => - let d2 = compose(ctx, d); - Cons(d1, d2) |> wrap; - | ListConcat1(ctx, d2) => - let d1 = compose(ctx, d); - ListConcat(d1, d2) |> wrap; - | ListConcat2(d1, ctx) => - let d2 = compose(ctx, d); - ListConcat(d1, d2) |> wrap; - | Tuple(ctx, (ld, rd)) => - let d = compose(ctx, d); - Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; - | ListLit(ctx, (ld, rd)) => - let d = compose(ctx, d); - ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; - | MultiHole(ctx, (ld, rd)) => - let d = compose(ctx, d); - MultiHole(ListUtil.rev_concat(ld, [TermBase.Any.Exp(d), ...rd])) - |> wrap; - | Let1(dp, ctx, d2) => - let d = compose(ctx, d); - Let(dp, d, d2) |> wrap; - | Let2(dp, d1, ctx) => - let d = compose(ctx, d); - Let(dp, d1, d) |> wrap; - | Fun(dp, ctx, env, v) => - let d = compose(ctx, d); - Fun(dp, d, env, v) |> wrap; - | FixF(v, ctx, env) => - let d = compose(ctx, d); - FixF(v, d, env) |> wrap; - | Cast(ctx, ty1, ty2) => - let d = compose(ctx, d); - Cast(d, ty1, ty2) |> wrap; - | FailedCast(ctx, ty1, ty2) => - let d = compose(ctx, d); - FailedCast(d, ty1, ty2) |> wrap; - | DynamicErrorHole(ctx, err) => - let d = compose(ctx, d); - DynamicErrorHole(d, err) |> wrap; - | MatchScrut(ctx, rules) => - let d = compose(ctx, d); - Match(d, rules) |> wrap; - | MatchRule(scr, p, ctx, (lr, rr)) => - let d = compose(ctx, d); - Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap; - | TypAp(ctx, ty) => - let d = compose(ctx, d); - TypAp(d, ty) |> wrap; - } - ); + switch (term) { + | Closure(env, ctx) => + let d = compose(ctx, d); + Closure(env, d) |> wrap; + | Filter(flt, ctx) => + let d = compose(ctx, d); + Filter(flt, d) |> wrap; + | Seq1(ctx, d2) => + let d1 = compose(ctx, d); + Seq(d1, d2) |> wrap; + | Seq2(d1, ctx) => + let d2 = compose(ctx, d); + Seq(d1, d2) |> wrap; + | Ap1(dir, ctx, d2) => + let d1 = compose(ctx, d); + Ap(dir, d1, d2) |> wrap; + | Ap2(dir, d1, ctx) => + let d2 = compose(ctx, d); + Ap(dir, d1, d2) |> wrap; + | DeferredAp1(ctx, d2s) => + let d1 = compose(ctx, d); + DeferredAp(d1, d2s) |> wrap; + | DeferredAp2(d1, ctx, (ld, rd)) => + let d2 = compose(ctx, d); + DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap; + | If1(ctx, d2, d3) => + let d' = compose(ctx, d); + If(d', d2, d3) |> wrap; + | If2(d1, ctx, d3) => + let d' = compose(ctx, d); + If(d1, d', d3) |> wrap; + | If3(d1, d2, ctx) => + let d' = compose(ctx, d); + If(d1, d2, d') |> wrap; + | Test(ctx) => + let d1 = compose(ctx, d); + Test(d1) |> wrap; + | UnOp(op, ctx) => + let d1 = compose(ctx, d); + UnOp(op, d1) |> wrap; + | BinOp1(op, ctx, d2) => + let d1 = compose(ctx, d); + BinOp(op, d1, d2) |> wrap; + | BinOp2(op, d1, ctx) => + let d2 = compose(ctx, d); + BinOp(op, d1, d2) |> wrap; + | Cons1(ctx, d2) => + let d1 = compose(ctx, d); + Cons(d1, d2) |> wrap; + | Cons2(d1, ctx) => + let d2 = compose(ctx, d); + Cons(d1, d2) |> wrap; + | ListConcat1(ctx, d2) => + let d1 = compose(ctx, d); + ListConcat(d1, d2) |> wrap; + | ListConcat2(d1, ctx) => + let d2 = compose(ctx, d); + ListConcat(d1, d2) |> wrap; + | Tuple(ctx, (ld, rd)) => + let d = compose(ctx, d); + Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; + | ListLit(ctx, (ld, rd)) => + let d = compose(ctx, d); + ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; + | MultiHole(ctx, (ld, rd)) => + let d = compose(ctx, d); + MultiHole(ListUtil.rev_concat(ld, [Exp(d), ...rd])) |> wrap; + | Let1(dp, ctx, d2) => + let d = compose(ctx, d); + Let(dp, d, d2) |> wrap; + | Let2(dp, d1, ctx) => + let d = compose(ctx, d); + Let(dp, d1, d) |> wrap; + | Fun(dp, ctx, env, v) => + let d = compose(ctx, d); + Fun(dp, d, env, v) |> wrap; + | FixF(v, ctx, env) => + let d = compose(ctx, d); + FixF(v, d, env) |> wrap; + | Cast(ctx, ty1, ty2) => + let d = compose(ctx, d); + Cast(d, ty1, ty2) |> wrap; + | FailedCast(ctx, ty1, ty2) => + let d = compose(ctx, d); + FailedCast(d, ty1, ty2) |> wrap; + | DynamicErrorHole(ctx, err) => + let d = compose(ctx, d); + DynamicErrorHole(d, err) |> wrap; + | MatchScrut(ctx, rules) => + let d = compose(ctx, d); + Match(d, rules) |> wrap; + | MatchRule(scr, p, ctx, (lr, rr)) => + let d = compose(ctx, d); + Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap; + | TypAp(ctx, ty) => + let d = compose(ctx, d); + TypAp(d, ty) |> wrap; + }; }; }; diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d6d0bcc543..61fd72f1bd 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -24,7 +24,9 @@ let evaluate_extend_env_with_pat = { ids, copied, - IdTagged.term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), + IdTagged.term: ( + FixF(pat, exp, Some(to_extend)): TermBase.exp_term + ), }, )), to_extend, @@ -36,14 +38,12 @@ let evaluate_extend_env_with_pat = binding => ( binding, - TermBase.Exp.Let( - pat, - { - ids, - copied, - term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), - }, - TermBase.Exp.Var(binding) |> IdTagged.fresh, + ( + Let( + pat, + {ids, copied, term: FixF(pat, exp, Some(to_extend))}, + (Var(binding): TermBase.exp_term) |> IdTagged.fresh, + ): TermBase.exp_term ) |> IdTagged.fresh, ), @@ -75,13 +75,13 @@ let tangle = let denv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), dvars, ); let fenv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), fvars, ); let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); @@ -356,13 +356,13 @@ and matches_fun = let denv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), dvars, ); let fenv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), fvars, ); let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); @@ -387,11 +387,7 @@ and matches_utpat = (d: TPat.t, f: TPat.t): bool => { }; let matches = - ( - ~env: ClosureEnvironment.t, - ~exp: DHExp.t, - ~flt: TermBase.StepperFilterKind.filter, - ) + (~env: ClosureEnvironment.t, ~exp: DHExp.t, ~flt: TermBase.filter) : option(FilterAction.t) => if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) { Some(flt.act); diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index f4979d94bf..59b58aa56f 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -161,16 +161,16 @@ 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); let* ty2 = typ_of_dhexp(ctx, m, d); - Some(Typ.Arrow(ty_p, ty2) |> Typ.temp); + Some(Arrow(ty_p, ty2) |> Typ.temp); | TypFun({term: Var(name), _} as utpat, d, _) when !Ctx.shadows_typ(ctx, name) => let ctx = Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract}); let* ty = typ_of_dhexp(ctx, m, d); - Some(Typ.Forall(utpat, ty) |> Typ.temp); + Some(Forall(utpat, ty) |> Typ.temp); | TypFun(_, d, _) => let* ty = typ_of_dhexp(ctx, m, d); - Some(Typ.Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp); + Some(Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp); | TypAp(d, ty1) => let* ty = typ_of_dhexp(ctx, m, d); let* (name, ty2) = Typ.matched_forall_strict(ctx, ty); @@ -209,8 +209,8 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => |> OptUtil.sequence; switch (tys) { | [] => Some(tyr) - | [ty] => Some(Typ.Arrow(ty, tyr) |> Typ.temp) - | tys => Some(Typ.Arrow(Prod(tys) |> Typ.temp, tyr) |> Typ.temp) + | [ty] => Some(Arrow(ty, tyr) |> Typ.temp) + | tys => Some(Arrow(Prod(tys) |> Typ.temp, tyr) |> Typ.temp) }; } else { None; @@ -221,7 +221,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => Some(var.typ); | Test(dtest) => let* ty = typ_of_dhexp(ctx, m, dtest); - Typ.eq(ty, Bool |> Typ.temp) ? Some(Typ.Prod([]) |> Typ.temp) : None; + Typ.eq(ty, Bool |> Typ.temp) ? Some(Prod([]) |> Typ.temp) : None; | Bool(_) => Some(Bool |> Typ.temp) | Int(_) => Some(Int |> Typ.temp) | Float(_) => Some(Float |> Typ.temp) diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index 39f43daeed..d6af00f4a4 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -1,4 +1,3 @@ -open DHExp; open Transition; type t = diff --git a/src/haz3lcore/prog/CachedStatics.re b/src/haz3lcore/prog/CachedStatics.re index f2bc13d113..3df0669dc3 100644 --- a/src/haz3lcore/prog/CachedStatics.re +++ b/src/haz3lcore/prog/CachedStatics.re @@ -8,7 +8,11 @@ type statics = { }; let empty_statics: statics = { - term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])}, + term: { + ids: [Id.invalid], + copied: false, + term: Tuple([]), + }, info_map: Id.Map.empty, error_ids: [], }; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 673af0bb89..d1edb9d16a 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -61,11 +61,11 @@ let is_grout = tiles => let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => { open OptUtil.Syntax; let+ ps = - ts + (ts: list(tile)) |> List.map( fun - | (_, (["|", "=>"], [Any.Pat(p)])) => Some(p) - | _ => None, + | (_, (["|", "=>"], [Pat(p)])) => Some(p) + | _ => None: tile => option(TermBase.pat_t), ) |> OptUtil.sequence and+ clauses = @@ -73,7 +73,7 @@ let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => { |> List.map( fun | Exp(clause) => Some(clause) - | _ => None, + | _ => None: TermBase.any_t => option(TermBase.exp_t), ) |> OptUtil.sequence; Aba.mk(ps, clauses); @@ -494,7 +494,7 @@ and tpat_term: unsorted => TPat.term = { // return(r => Rul(r), ids, {ids, term}); // } and rul = (unsorted: unsorted): Rul.t => { - let hole = Rul.Hole(kids_of_unsorted(unsorted)); + let hole: Rul.term = Hole(kids_of_unsorted(unsorted)); switch (exp(unsorted)) { | {term: MultiHole(_), _} => switch (unsorted) { diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re index 5a85dbecd9..2415399627 100644 --- a/src/haz3lcore/statics/Mode.re +++ b/src/haz3lcore/statics/Mode.re @@ -152,6 +152,7 @@ let typap_mode: t = SynTypFun; let of_deferred_ap_args = (length: int, ty_ins: list(Typ.t)): list(t) => ( List.length(ty_ins) == length - ? ty_ins : List.init(length, _ => Typ.Unknown(Internal) |> Typ.temp) + ? ty_ins + : List.init(length, _ => (Unknown(Internal): Typ.term) |> Typ.temp) ) |> List.map(ty => Ana(ty)); diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index aca1ce0389..443c94155b 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -276,13 +276,13 @@ and uexp_to_info_map = copied: false, term: switch (e.term) { - | Var("e") => UExp.Constructor("$e", Unknown(Internal) |> Typ.temp) - | Var("v") => UExp.Constructor("$v", Unknown(Internal) |> Typ.temp) + | Var("e") => Constructor("$e", Unknown(Internal) |> Typ.temp) + | Var("v") => Constructor("$v", Unknown(Internal) |> Typ.temp) | _ => e.term }, }; - let ty_in = Typ.Var("$Meta") |> Typ.temp; - let ty_out = Typ.Unknown(Internal) |> Typ.temp; + let ty_in = Var("$Meta") |> Typ.temp; + let ty_out = Unknown(Internal) |> Typ.temp; let (e, m) = go(~mode=Ana(ty_in), e, m); add(~self=Just(ty_out), ~co_ctx=e.co_ctx, m); | UnOp(op, e) => @@ -426,8 +426,7 @@ and uexp_to_info_map = let def_ctx = p_ana'.ctx; let (def_base2, _) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m); let ana_ty_fn = ((ty_fn1, ty_fn2), ty_p) => { - Typ.term_of(ty_p) == Typ.Unknown(SynSwitch) - && !Typ.eq(ty_fn1, ty_fn2) + Typ.term_of(ty_p) == Unknown(SynSwitch) && !Typ.eq(ty_fn1, ty_fn2) ? ty_fn1 : ty_p; }; let ana = @@ -438,7 +437,7 @@ and uexp_to_info_map = | ((Prod(ty_fns1), Prod(ty_fns2)), Prod(ty_ps)) => let tys = List.map2(ana_ty_fn, List.combine(ty_fns1, ty_fns2), ty_ps); - Typ.Prod(tys) |> Typ.temp; + Prod(tys) |> Typ.temp; | ((_, _), _) => ana_ty_fn((def_base.ty, def_base2.ty), p_syn.ty) }; let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(ana), def, m); @@ -616,7 +615,7 @@ and uexp_to_info_map = use a different name than the alias for the recursive parameter */ //let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre)); let ty_rec = - Typ.Rec(TPat.Var(name) |> IdTagged.fresh, utyp) |> Typ.temp; + Rec((Var(name): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp; let ctx_def = Ctx.extend_alias(ctx, name, TPat.rep_id(typat), ty_rec); (ty_rec, ctx_def, ctx_def); @@ -697,7 +696,7 @@ and upat_to_info_map = let atomic = (self, constraint_) => add(~self, ~ctx, ~constraint_, m); let ancestors = [UPat.rep_id(upat)] @ ancestors; let go = upat_to_info_map(~is_synswitch, ~ancestors, ~co_ctx); - let unknown = Typ.Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp; + let unknown = Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp; let ctx_fold = (ctx: Ctx.t, m) => List.fold_left2( ((ctx, tys, cons, m), e, mode) => diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 67e6f1ecde..02bd8400d4 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -3,7 +3,7 @@ open Util; let continue = x => x; let stop = (_, x) => x; [@deriving (show({with_path: false}), sexp, yojson)] -type deferral_position = +type deferral_position_t = | InAp | OutsideAp; @@ -61,7 +61,7 @@ and exp_term = | MultiHole(list(any_t)) | DynamicErrorHole(exp_t, InvalidOperationError.t) | FailedCast(exp_t, typ_t, typ_t) - | Deferral(deferral_position) + | Deferral(deferral_position_t) | Undefined | Bool(bool) | Int(int) @@ -165,6 +165,7 @@ and filter = { }; module rec Any: { + [@deriving (show({with_path: false}), sexp, yojson)] type t = any_t; let map_term: @@ -181,6 +182,7 @@ module rec Any: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type t = any_t; let map_term = @@ -232,9 +234,12 @@ module rec Any: { }; } and Exp: { + [@deriving (show({with_path: false}), sexp, yojson)] type term = exp_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = exp_t; - + [@deriving (show({with_path: false}), sexp, yojson)] + type deferral_position = deferral_position_t; let map_term: ( ~f_exp: (Exp.t => Exp.t, Exp.t) => Exp.t=?, @@ -249,8 +254,12 @@ and Exp: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type term = exp_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = exp_t; + [@deriving (show({with_path: false}), sexp, yojson)] + type deferral_position = deferral_position_t; let map_term = ( @@ -456,7 +465,9 @@ and Exp: { }; } and Pat: { + [@deriving (show({with_path: false}), sexp, yojson)] type term = pat_term; // The second Typ.t field is only meaningful in dynamic patterns + [@deriving (show({with_path: false}), sexp, yojson)] type t = pat_t; let map_term: @@ -473,7 +484,9 @@ and Pat: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type term = pat_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = pat_t; let map_term = @@ -729,6 +742,7 @@ and Typ: { and TPat: { [@deriving (show({with_path: false}), sexp, yojson)] type term = tpat_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = tpat_t; let map_term: @@ -749,6 +763,7 @@ and TPat: { } = { [@deriving (show({with_path: false}), sexp, yojson)] type term = tpat_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = tpat_t; let map_term = @@ -799,6 +814,7 @@ and TPat: { and Rul: { [@deriving (show({with_path: false}), sexp, yojson)] type term = rul_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = rul_t; let map_term: @@ -890,7 +906,7 @@ and Environment: { and ClosureEnvironment: { [@deriving (show({with_path: false}), sexp, yojson)] - type t; + type t = closure_environment_t; let wrap: (Id.t, Environment.t) => t; @@ -1001,6 +1017,7 @@ and ClosureEnvironment: { let without_keys = keys => update(Environment.without_keys(keys)); } and StepperFilterKind: { + [@deriving (show({with_path: false}), sexp, yojson)] type t = stepper_filter_kind_t; let map_term: @@ -1019,6 +1036,7 @@ and StepperFilterKind: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type t = stepper_filter_kind_t; let map = (mapper, filter: t): t => { diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index cd05476fd9..bdb3e014cc 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -8,7 +8,11 @@ module CachedStatics = { }; let empty: t = { - term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])}, + term: { + ids: [Id.invalid], + copied: false, + term: Tuple([]), + }, info_map: Id.Map.empty, error_ids: [], }; diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re index ff59e48f55..23265f8a2a 100644 --- a/src/haz3lcore/zipper/EditorUtil.re +++ b/src/haz3lcore/zipper/EditorUtil.re @@ -1,50 +1,48 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => { - Exp.( - switch (e1.term) { - | EmptyHole - | Invalid(_) - | MultiHole(_) - | DynamicErrorHole(_) - | FailedCast(_) - | Undefined - | Deferral(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) - | ListLit(_) - | Constructor(_) - | Closure(_) - | Fun(_) - | TypFun(_) - | FixF(_) - | Tuple(_) - | Var(_) - | Ap(_) - | TypAp(_) - | DeferredAp(_) - | If(_) - | Test(_) - | Parens(_) - | Cons(_) - | ListConcat(_) - | UnOp(_) - | BinOp(_) - | BuiltinFun(_) - | Cast(_) - | Match(_) => Exp.{ids: [Id.mk()], copied: false, term: Seq(e1, e2)} - | Seq(e11, e12) => - let e12' = append_exp(e12, e2); - {ids: e1.ids, copied: false, term: Seq(e11, e12')}; - | Filter(kind, ebody) => - let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: Filter(kind, ebody')}; - | Let(p, edef, ebody) => - let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: Let(p, edef, ebody')}; - | TyAlias(tp, tdef, ebody) => - let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')}; - } - ); + switch (e1.term) { + | EmptyHole + | Invalid(_) + | MultiHole(_) + | DynamicErrorHole(_) + | FailedCast(_) + | Undefined + | Deferral(_) + | Bool(_) + | Int(_) + | Float(_) + | String(_) + | ListLit(_) + | Constructor(_) + | Closure(_) + | Fun(_) + | TypFun(_) + | FixF(_) + | Tuple(_) + | Var(_) + | Ap(_) + | TypAp(_) + | DeferredAp(_) + | If(_) + | Test(_) + | Parens(_) + | Cons(_) + | ListConcat(_) + | UnOp(_) + | BinOp(_) + | BuiltinFun(_) + | Cast(_) + | Match(_) => {ids: [Id.mk()], copied: false, term: Seq(e1, e2)} + | Seq(e11, e12) => + let e12' = append_exp(e12, e2); + {ids: e1.ids, copied: false, term: Seq(e11, e12')}; + | Filter(kind, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: Filter(kind, ebody')}; + | Let(p, edef, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: Let(p, edef, ebody')}; + | TyAlias(tp, tdef, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')}; + }; }; diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index b5e7dfc76d..01050d5e7b 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -568,23 +568,22 @@ module F = (ExerciseEnv: ExerciseEnv) => { hidden_tests: 'a, }; - let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => - Exp.{ - term: - Exp.Filter( - Filter({ - act: FilterAction.(act, One), - pat: { - term: Constructor("$e", Unknown(Internal) |> Typ.temp), - copied: false, - ids: [Id.mk()], - }, - }), - term, - ), - copied: false, - ids: [Id.mk()], - }; + let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => { + term: + Filter( + Filter({ + act: FilterAction.(act, One), + pat: { + term: Constructor("$e", Unknown(Internal) |> Typ.temp), + copied: false, + ids: [Id.mk()], + }, + }), + term, + ), + copied: false, + ids: [Id.mk()], + }; let term_of = (editor: Editor.t): UExp.t => MakeTerm.from_zip_for_sem(editor.state.zipper).term; diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 65c01e1a6f..ba06d2a29e 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -409,7 +409,7 @@ let locked = statics.info_map, statics.term, ) - : DHExp.Bool(true) |> DHExp.fresh; + : Bool(true) |> DHExp.fresh; let elab: Elaborator.Elaboration.t = {d: elab}; let result: ModelResult.t = settings.core.dynamics diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index cbfdf4df9f..a74a5187d8 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -533,7 +533,7 @@ let get_doc = (term) : (list(Node.t), (list(Node.t), ColorSteps.t), list(Node.t)) => switch ((term: Exp.term)) { - | Exp.Invalid(_) => simple("Not a valid expression") + | Invalid(_) => simple("Not a valid expression") | DynamicErrorHole(_) | FailedCast(_) | Closure(_) @@ -1980,7 +1980,7 @@ let get_doc = doc, ); switch (tl.term) { - | Pat.Cons(hd2, tl2) => + | Cons(hd2, tl2) => if (ListPat.cons2_pat.id == get_specificity_level(ListPat.cons2)) { let hd2_id = List.nth(hd2.ids, 0); let tl2_id = List.nth(tl2.ids, 0); @@ -2201,7 +2201,7 @@ let get_doc = doc, ); switch (result.term) { - | Typ.Arrow(arg2, result2) => + | Arrow(arg2, result2) => if (ArrowTyp.arrow3_typ.id == get_specificity_level(ArrowTyp.arrow3)) { let arg2_id = List.nth(arg2.ids, 0); let result2_id = List.nth(result2.ids, 0); diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index 622dcf766e..82dfd0a9e3 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -21,7 +21,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => div( ~attrs=[ clss(["typ-view", "atom", "unknown"]), - Attr.title(Typ.show_type_provenance(prov)), + Attr.title(TermBase.show_type_provenance(prov)), ], [text("?") /*, prov_view(prov)*/], ) @@ -98,7 +98,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => div( ~attrs=[ clss(["typ-view", "atom", "unknown"]), - Attr.title(Typ.show_type_provenance(Internal)), + Attr.title(TermBase.show_type_provenance(Internal)), ], [text("?") /*, prov_view(prov)*/], ) From 9171acb8acb2b6e044ddd2ef24c5f25dfd103f87 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 19 Sep 2024 16:44:28 -0400 Subject: [PATCH 24/53] Experiment with switching to Bonsai --- src/haz3lweb/Main.re | 141 +++++++++++++++++++++++------------------- src/haz3lweb/Model.re | 3 +- src/haz3lweb/dune | 9 ++- src/util/dune | 2 +- 4 files changed, 88 insertions(+), 67 deletions(-) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index cf0269bf45..ed72a99a5a 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -1,6 +1,5 @@ open Util; open Js_of_ocaml; -open Incr_dom; open Haz3lweb; let scroll_to_caret = ref(true); @@ -36,7 +35,7 @@ let restart_caret_animation = () => | _ => () }; -let apply = (model, action, state, ~schedule_action): Model.t => { +let apply = (model, action, ~schedule_action): Model.t => { restart_caret_animation(); if (UpdateAction.is_edit(action)) { last_edit_action := JsUtil.timestamp(); @@ -48,7 +47,7 @@ let apply = (model, action, state, ~schedule_action): Model.t => { last_edit_action := JsUtil.timestamp(); switch ( try({ - let new_model = Update.apply(model, action, state, ~schedule_action); + let new_model = Update.apply(model, action, (), ~schedule_action); Log.update(action); new_model; }) { @@ -70,74 +69,92 @@ let apply = (model, action, state, ~schedule_action): Model.t => { }; }; +let on_startup = + ( + ~inject: UpdateAction.t => Ui_effect.t(unit), + ~schedule_event: Ui_effect.t(unit) => unit, + m: Model.t, + ) + : Model.t => { + let schedule_action = action => schedule_event(inject(action)); + let _ = + observe_font_specimen("font-specimen", fm => + schedule_action(Haz3lweb.Update.SetMeta(FontMetrics(fm))) + ); + NinjaKeys.initialize(NinjaKeys.options(schedule_action)); + JsUtil.focus_clipboard_shim(); + /* initialize state. */ + /* Initial evaluation on a worker */ + Update.schedule_evaluation(~schedule_action, m); + Os.is_mac := + Dom_html.window##.navigator##.platform##toUpperCase##indexOf( + Js.string("MAC"), + ) + >= 0; + m; +}; + module App = { module Model = Model; module Action = Update; module State = State; + // let create = + // ( + // model: Incr.t(Haz3lweb.Model.t), + // ~old_model as _: Incr.t(Haz3lweb.Model.t), + // ~inject, + // ) => { + // open Incr.Let_syntax; + // let%map model = model; + // /* Note: mapping over the old_model here may + // trigger an additional redraw */ + // Component.create( + // ~apply_action=apply(model), + // model, + // Haz3lweb.Page.view(~inject, model), + // ~on_display=(_, ~schedule_action) => { + // if (edit_action_applied^ + // && JsUtil.timestamp() + // -. last_edit_action^ > 1000.0) { + // /* If an edit action has been applied, but no other edit action + // has been applied for 1 second, save the model. */ + // edit_action_applied := false; + // print_endline("Saving..."); + // schedule_action(Update.Save); + // }; + // if (scroll_to_caret.contents) { + // scroll_to_caret := false; + // JsUtil.scroll_cursor_into_view_if_needed(); + // }; + // }, + // ); + // }; + // }; +}; - let on_startup = (~schedule_action, m: Model.t) => { - let _ = - observe_font_specimen("font-specimen", fm => - schedule_action(Haz3lweb.Update.SetMeta(FontMetrics(fm))) - ); - - NinjaKeys.initialize(NinjaKeys.options(schedule_action)); - JsUtil.focus_clipboard_shim(); - - /* initialize state. */ - let state = State.init(); - - /* Initial evaluation on a worker */ - Update.schedule_evaluation(~schedule_action, m); +let app = + Bonsai.state_machine0( + (module Model), + (module Update), + ~apply_action= + (~inject, ~schedule_event) => + apply(~schedule_action=x => schedule_event(inject(x))), + ~default_model=Model.load(Model.blank), + ~reset=on_startup, + ); - Os.is_mac := - Dom_html.window##.navigator##.platform##toUpperCase##indexOf( - Js.string("MAC"), - ) - >= 0; - Async_kernel.Deferred.return(state); - }; +open Bonsai.Let_syntax; - let create = - ( - model: Incr.t(Haz3lweb.Model.t), - ~old_model as _: Incr.t(Haz3lweb.Model.t), - ~inject, - ) => { - open Incr.Let_syntax; - let%map model = model; - /* Note: mapping over the old_model here may - trigger an additional redraw */ - Component.create( - ~apply_action=apply(model), - model, - Haz3lweb.Page.view(~inject, model), - ~on_display=(_, ~schedule_action) => { - if (edit_action_applied^ - && JsUtil.timestamp() - -. last_edit_action^ > 1000.0) { - /* If an edit action has been applied, but no other edit action - has been applied for 1 second, save the model. */ - edit_action_applied := false; - print_endline("Saving..."); - schedule_action(Update.Save); - }; - if (scroll_to_caret.contents) { - scroll_to_caret := false; - JsUtil.scroll_cursor_into_view_if_needed(); - }; - }, - ); - }; +let view = { + let%sub app = app; + let%arr (model, inject) = app; + Haz3lweb.Page.view(~inject, model); + // Bonsai.Computation.map(app, ~f=((model, inject)) => + // Haz3lweb.Page.view(~inject, model) + // ); }; switch (JsUtil.Fragment.get_current()) { | Some("debug") => DebugMode.go() -| _ => - Incr_dom.Start_app.start( - (module App), - ~debug=false, - ~bind_to_element_with_id="container", - ~initial_model=Model.load(Model.blank), - ) +| _ => Bonsai_web.Start.start(view, ~bind_to_element_with_id="container") }; diff --git a/src/haz3lweb/Model.re b/src/haz3lweb/Model.re index 839c07a0c8..e4939b3af0 100644 --- a/src/haz3lweb/Model.re +++ b/src/haz3lweb/Model.re @@ -33,6 +33,7 @@ let ui_state_init = { mousedown: false, }; +[@deriving sexp] type t = { editors: Editors.t, settings: Settings.t, @@ -41,7 +42,7 @@ type t = { ui_state, }; -let cutoff = (===); +let equal = (===); let mk = (editors, results) => { editors, diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index 8d25155dc5..d3e42ec636 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -9,7 +9,8 @@ (name workerServer) (modules WorkerServer) (libraries - incr_dom + bonsai + bonsai.web virtual_dom.input_widgets util ppx_yojson_conv.expander @@ -38,7 +39,8 @@ ezjs_idb workerServer str - incr_dom + bonsai + bonsai.web virtual_dom.input_widgets util ppx_yojson_conv.expander @@ -66,7 +68,8 @@ js_of_ocaml-ppx ppx_let ppx_sexp_conv - ppx_deriving.show))) + ppx_deriving.show + bonsai.ppx_bonsai))) (executable (name worker) diff --git a/src/util/dune b/src/util/dune index 889c95bd2c..743b3009d9 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,6 +1,6 @@ (library (name util) - (libraries re base ptmap incr_dom virtual_dom yojson) + (libraries re base ptmap bonsai bonsai.web virtual_dom yojson) (js_of_ocaml) (preprocess (pps From 2e2aa4c7c6200852bad1bb7f070810d2340e1ff2 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 26 Sep 2024 09:41:51 -0400 Subject: [PATCH 25/53] on_startup first attempt --- src/haz3lweb/Main.re | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index ed72a99a5a..0bfbd505ae 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -70,13 +70,8 @@ let apply = (model, action, ~schedule_action): Model.t => { }; let on_startup = - ( - ~inject: UpdateAction.t => Ui_effect.t(unit), - ~schedule_event: Ui_effect.t(unit) => unit, - m: Model.t, - ) - : Model.t => { - let schedule_action = action => schedule_event(inject(action)); + (~inject: UpdateAction.t => Ui_effect.t(unit), m: Model.t) + : Ui_effect.t(unit) => { let _ = observe_font_specimen("font-specimen", fm => schedule_action(Haz3lweb.Update.SetMeta(FontMetrics(fm))) @@ -91,7 +86,7 @@ let on_startup = Js.string("MAC"), ) >= 0; - m; + Ui_effect.Ignore; }; module App = { @@ -140,18 +135,26 @@ let app = (~inject, ~schedule_event) => apply(~schedule_action=x => schedule_event(inject(x))), ~default_model=Model.load(Model.blank), - ~reset=on_startup, ); open Bonsai.Let_syntax; let view = { + let startup_completed = Bonsai.toggle'(~default_model=false); + let%sub startup_completed = startup_completed; let%sub app = app; + let%sub after_display = { + switch%sub (startup_completed) { + | {state: false, set_state, _} => + let%arr (model, inject) = app + and set_state = set_state; + Bonsai.Effect.Many([on_startup(~inject, model), set_state(true)]); + | {state: true, _} => Bonsai.Computation.return(Ui_effect.Ignore) + }; + }; + let%sub () = Bonsai.Edge.lifecycle(~after_display, ()); let%arr (model, inject) = app; Haz3lweb.Page.view(~inject, model); - // Bonsai.Computation.map(app, ~f=((model, inject)) => - // Haz3lweb.Page.view(~inject, model) - // ); }; switch (JsUtil.Fragment.get_current()) { From 644009954b82e5b1be5d8a19e3fff6112a755d8f Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 27 Sep 2024 11:58:15 -0400 Subject: [PATCH 26/53] Make on_startup an action --- src/haz3lweb/Keyboard.re | 2 +- src/haz3lweb/Log.re | 3 ++- src/haz3lweb/Main.re | 41 ++---------------------------------- src/haz3lweb/Update.re | 38 +++++++++++++++++++++++++++++++++ src/haz3lweb/UpdateAction.re | 10 ++++++--- 5 files changed, 50 insertions(+), 44 deletions(-) diff --git a/src/haz3lweb/Keyboard.re b/src/haz3lweb/Keyboard.re index f0501a66a4..7e4e655f26 100644 --- a/src/haz3lweb/Keyboard.re +++ b/src/haz3lweb/Keyboard.re @@ -227,7 +227,7 @@ let shortcuts = (sys: Key.sys): list(shortcut) => ] @ (if (ExerciseSettings.show_instructor) {instructor_shortcuts} else {[]}); -let handle_key_event = (k: Key.t): option(Update.t) => { +let handle_key_event = (k: Key.t): option(UpdateAction.t) => { let now = (a: Action.t): option(UpdateAction.t) => Some(PerformAction(a)); switch (k) { diff --git a/src/haz3lweb/Log.re b/src/haz3lweb/Log.re index 4d98345dab..7c87a640f6 100644 --- a/src/haz3lweb/Log.re +++ b/src/haz3lweb/Log.re @@ -12,7 +12,8 @@ let is_action_logged: UpdateAction.t => bool = | FinishImportAll(_) | FinishImportScratchpad(_) | Benchmark(_) - | DebugConsole(_) => false + | DebugConsole(_) + | Startup => false | Reset | TAB | Set(_) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index 0bfbd505ae..653a709923 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -6,23 +6,6 @@ let scroll_to_caret = ref(true); let edit_action_applied = ref(true); let last_edit_action = ref(JsUtil.timestamp()); -let observe_font_specimen = (id, update) => - ResizeObserver.observe( - ~node=JsUtil.get_elem_by_id(id), - ~f= - (entries, _) => { - let specimen = Js.to_array(entries)[0]; - let rect = specimen##.contentRect; - update( - Haz3lweb.FontMetrics.{ - row_height: rect##.bottom -. rect##.top, - col_width: rect##.right -. rect##.left, - }, - ); - }, - (), - ); - let restart_caret_animation = () => // necessary to trigger reflow // @@ -69,26 +52,6 @@ let apply = (model, action, ~schedule_action): Model.t => { }; }; -let on_startup = - (~inject: UpdateAction.t => Ui_effect.t(unit), m: Model.t) - : Ui_effect.t(unit) => { - let _ = - observe_font_specimen("font-specimen", fm => - schedule_action(Haz3lweb.Update.SetMeta(FontMetrics(fm))) - ); - NinjaKeys.initialize(NinjaKeys.options(schedule_action)); - JsUtil.focus_clipboard_shim(); - /* initialize state. */ - /* Initial evaluation on a worker */ - Update.schedule_evaluation(~schedule_action, m); - Os.is_mac := - Dom_html.window##.navigator##.platform##toUpperCase##indexOf( - Js.string("MAC"), - ) - >= 0; - Ui_effect.Ignore; -}; - module App = { module Model = Model; module Action = Update; @@ -146,9 +109,9 @@ let view = { let%sub after_display = { switch%sub (startup_completed) { | {state: false, set_state, _} => - let%arr (model, inject) = app + let%arr (_model, inject) = app and set_state = set_state; - Bonsai.Effect.Many([on_startup(~inject, model), set_state(true)]); + Bonsai.Effect.Many([set_state(true), inject(Update.Startup)]); | {state: true, _} => Bonsai.Computation.return(Ui_effect.Ignore) }; }; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index de814c4561..26324a9c2e 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -1,8 +1,26 @@ open Util; +open Js_of_ocaml; open Haz3lcore; include UpdateAction; // to prevent circularity +let observe_font_specimen = (id, update) => + ResizeObserver.observe( + ~node=JsUtil.get_elem_by_id(id), + ~f= + (entries, _) => { + let specimen = Js.to_array(entries)[0]; + let rect = specimen##.contentRect; + update( + FontMetrics.{ + row_height: rect##.bottom -. rect##.top, + col_width: rect##.right -. rect##.left, + }, + ); + }, + (), + ); + let update_settings = (a: settings_action, {settings, _} as model: Model.t): Model.t => switch (a) { @@ -213,6 +231,25 @@ let schedule_evaluation = (~schedule_action, model: Model.t): unit => }; }; +let on_startup = + (~schedule_action: UpdateAction.t => unit, m: Model.t): Model.t => { + let _ = + observe_font_specimen("font-specimen", fm => + schedule_action(UpdateAction.SetMeta(FontMetrics(fm))) + ); + NinjaKeys.initialize(NinjaKeys.options(schedule_action)); + JsUtil.focus_clipboard_shim(); + /* initialize state. */ + /* Initial evaluation on a worker */ + schedule_evaluation(~schedule_action, m); + Os.is_mac := + Dom_html.window##.navigator##.platform##toUpperCase##indexOf( + Js.string("MAC"), + ) + >= 0; + m; +}; + let update_cached_data = (~schedule_action, update, m: Model.t): Model.t => { let update_dynamics = reevaluate_post_update(update); /* If we switch editors, or change settings which require statics @@ -373,6 +410,7 @@ let apply = }; let m: Result.t(Model.t) = switch (update) { + | Startup => Ok(on_startup(~schedule_action, model)) | Reset => Ok(Model.reset(model)) | Set(Evaluation(_) as s_action) => Ok(update_settings(s_action, model)) | Set(s_action) => diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re index b67861090f..cd2f145f3e 100644 --- a/src/haz3lweb/UpdateAction.re +++ b/src/haz3lweb/UpdateAction.re @@ -57,6 +57,7 @@ type export_action = [@deriving (show({with_path: false}), sexp, yojson)] type t = /* meta */ + | Startup | Reset | Set(settings_action) | SetMeta(set_meta) @@ -144,7 +145,8 @@ let is_edit: t => bool = | DebugConsole(_) | InitImportAll(_) | InitImportScratchpad(_) - | Benchmark(_) => false; + | Benchmark(_) + | Startup => false; let reevaluate_post_update: t => bool = fun @@ -197,7 +199,8 @@ let reevaluate_post_update: t => bool = | SwitchDocumentationSlide(_) | Reset | Undo - | Redo => true; + | Redo + | Startup => true; let should_scroll_to_caret = fun @@ -235,7 +238,8 @@ let should_scroll_to_caret = | Reset | Undo | Redo - | TAB => true + | TAB + | Startup => true | PerformAction(a) => switch (a) { | Move(_) From 31b690abc08302b9b6c74d0bce7114d180391ac1 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 27 Sep 2024 15:10:07 -0400 Subject: [PATCH 27/53] Finish converting to Bonsai --- src/haz3lweb/Main.re | 81 ++++++++++++++-------------------- src/haz3lweb/view/DebugMode.re | 31 +------------ 2 files changed, 36 insertions(+), 76 deletions(-) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index 653a709923..f884404d17 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -1,6 +1,7 @@ open Util; open Js_of_ocaml; open Haz3lweb; +open Bonsai.Let_syntax; let scroll_to_caret = ref(true); let edit_action_applied = ref(true); @@ -52,44 +53,6 @@ let apply = (model, action, ~schedule_action): Model.t => { }; }; -module App = { - module Model = Model; - module Action = Update; - module State = State; - // let create = - // ( - // model: Incr.t(Haz3lweb.Model.t), - // ~old_model as _: Incr.t(Haz3lweb.Model.t), - // ~inject, - // ) => { - // open Incr.Let_syntax; - // let%map model = model; - // /* Note: mapping over the old_model here may - // trigger an additional redraw */ - // Component.create( - // ~apply_action=apply(model), - // model, - // Haz3lweb.Page.view(~inject, model), - // ~on_display=(_, ~schedule_action) => { - // if (edit_action_applied^ - // && JsUtil.timestamp() - // -. last_edit_action^ > 1000.0) { - // /* If an edit action has been applied, but no other edit action - // has been applied for 1 second, save the model. */ - // edit_action_applied := false; - // print_endline("Saving..."); - // schedule_action(Update.Save); - // }; - // if (scroll_to_caret.contents) { - // scroll_to_caret := false; - // JsUtil.scroll_cursor_into_view_if_needed(); - // }; - // }, - // ); - // }; - // }; -}; - let app = Bonsai.state_machine0( (module Model), @@ -100,22 +63,46 @@ let app = ~default_model=Model.load(Model.blank), ); -open Bonsai.Let_syntax; - -let view = { - let startup_completed = Bonsai.toggle'(~default_model=false); - let%sub startup_completed = startup_completed; - let%sub app = app; +let on_startup = effect => { + let%sub startup_completed = Bonsai.toggle'(~default_model=false); let%sub after_display = { switch%sub (startup_completed) { | {state: false, set_state, _} => - let%arr (_model, inject) = app + let%arr effect = effect and set_state = set_state; - Bonsai.Effect.Many([set_state(true), inject(Update.Startup)]); + Bonsai.Effect.Many([set_state(true), effect]); | {state: true, _} => Bonsai.Computation.return(Ui_effect.Ignore) }; }; - let%sub () = Bonsai.Edge.lifecycle(~after_display, ()); + Bonsai.Edge.lifecycle(~after_display, ()); +}; + +let view = { + let%sub app = app; + let%sub () = { + on_startup( + Bonsai.Value.map(~f=((_model, inject)) => inject(Startup), app), + ); + }; + let%sub after_display = { + let%arr (_model, inject) = app; + if (scroll_to_caret.contents) { + scroll_to_caret := false; + JsUtil.scroll_cursor_into_view_if_needed(); + }; + if (edit_action_applied^ + && JsUtil.timestamp() + -. last_edit_action^ > 1000.0) { + /* If an edit action has been applied, but no other edit action + has been applied for 1 second, save the model. */ + edit_action_applied := false; + print_endline("Saving..."); + inject(Update.Save); + } else { + Ui_effect.Ignore; + }; + }; + let%sub () = Bonsai.Edge.after_display(after_display); let%arr (model, inject) = app; Haz3lweb.Page.view(~inject, model); }; diff --git a/src/haz3lweb/view/DebugMode.re b/src/haz3lweb/view/DebugMode.re index 543e7cc757..39cba26eb8 100644 --- a/src/haz3lweb/view/DebugMode.re +++ b/src/haz3lweb/view/DebugMode.re @@ -48,35 +48,8 @@ let view = { ); }; -module App = { - module Model = { - type t = unit; - let cutoff = (_, _) => false; - }; - module Action = { - type t = unit; - let sexp_of_t = _ => Sexplib.Sexp.unit; - }; - module State = { - type t = unit; - }; - let on_startup = (~schedule_action as _, _) => - Async_kernel.Deferred.return(); - let create = (_, ~old_model as _, ~inject as _) => - Incr_dom.Incr.return() - |> Incr_dom.Incr.map(~f=_ => - Incr_dom.Component.create( - ~apply_action=(_, _, ~schedule_action as _) => (), - (), - view, - ) - ); -}; - let go = () => - Incr_dom.Start_app.start( - (module App), - ~debug=false, + Bonsai_web.Start.start( + Bonsai.Computation.return(view), ~bind_to_element_with_id="container", - ~initial_model=(), ); From 7a2d9a7017488bbfe0e15732096f6ae854590750 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 27 Sep 2024 15:10:24 -0400 Subject: [PATCH 28/53] Update dune-project --- dune-project | 1 - 1 file changed, 1 deletion(-) diff --git a/dune-project b/dune-project index 335194ae48..fbc79765cc 100644 --- a/dune-project +++ b/dune-project @@ -29,7 +29,6 @@ reason ppx_yojson_conv_lib ppx_yojson_conv - incr_dom (omd (>= 2.0.0~alpha4)) ezjs_idb virtual_dom From ccc6dc16b67bbb8c56d88b19f33e4f1b0fa80c46 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 27 Sep 2024 15:17:45 -0400 Subject: [PATCH 29/53] Update dependencies --- dune-project | 2 +- hazel.opam | 3 +-- hazel.opam.locked | 58 ++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 57 insertions(+), 6 deletions(-) diff --git a/dune-project b/dune-project index fbc79765cc..dd2aafe478 100644 --- a/dune-project +++ b/dune-project @@ -31,7 +31,7 @@ ppx_yojson_conv (omd (>= 2.0.0~alpha4)) ezjs_idb - virtual_dom + bonsai ppx_deriving ptmap uuidm diff --git a/hazel.opam b/hazel.opam index 36a81b933a..03973e9189 100644 --- a/hazel.opam +++ b/hazel.opam @@ -14,10 +14,9 @@ depends: [ "reason" "ppx_yojson_conv_lib" "ppx_yojson_conv" - "incr_dom" "omd" {>= "2.0.0~alpha4"} "ezjs_idb" - "virtual_dom" + "bonsai" "ppx_deriving" "ptmap" "uuidm" diff --git a/hazel.opam.locked b/hazel.opam.locked index 31fd8b2c15..04c2cb9507 100644 --- a/hazel.opam.locked +++ b/hazel.opam.locked @@ -1,7 +1,7 @@ opam-version: "2.0" name: "hazel" -version: "~dev" +version: "dev" synopsis: "Hazel, a live functional programming environment with typed holes" maintainer: "Hazel Development Team" authors: "Hazel Development Team" @@ -13,9 +13,17 @@ depends: [ "alcotest" {= "1.8.0" & with-test} "angstrom" {= "0.16.0"} "astring" {= "0.8.5"} + "async" {= "v0.16.0"} + "async_durable" {= "v0.16.0"} + "async_extra" {= "v0.16.0"} "async_js" {= "v0.16.0"} "async_kernel" {= "v0.16.0"} "async_rpc_kernel" {= "v0.16.0"} + "async_rpc_websocket" {= "v0.16.0"} + "async_ssl" {= "v0.16.1"} + "async_unix" {= "v0.16.0"} + "async_websocket" {= "v0.16.0"} + "babel" {= "v0.16.0"} "base" {= "v0.16.3"} "base-bigarray" {= "base"} "base-bytes" {= "base"} @@ -26,53 +34,81 @@ depends: [ "base64" {= "3.5.1"} "base_bigstring" {= "v0.16.0"} "base_quickcheck" {= "v0.16.0"} + "bigarray-compat" {= "1.1.0"} "bignum" {= "v0.16.0"} "bigstringaf" {= "0.9.1"} "bin_prot" {= "v0.16.0"} + "bonsai" {= "v0.16.0"} "camlp-streams" {= "5.0.1"} "chrome-trace" {= "3.16.0"} "cmdliner" {= "1.3.0"} + "cohttp" {= "5.3.1"} + "cohttp-async" {= "5.3.0"} + "cohttp_async_websocket" {= "v0.16.0"} + "conduit" {= "7.0.0"} + "conduit-async" {= "7.0.0"} "conf-bash" {= "1"} "conf-gmp" {= "4"} + "conf-gmp-powm-sec" {= "3"} + "conf-libffi" {= "2.0.0"} + "conf-libssl" {= "4"} + "conf-pkg-config" {= "3"} + "conf-zlib" {= "1"} "core" {= "v0.16.2"} + "core_bench" {= "v0.16.0"} "core_kernel" {= "v0.16.0"} + "core_unix" {= "v0.16.0"} "cppo" {= "1.6.9"} "crunch" {= "3.3.1" & with-doc} + "cryptokit" {= "1.16.1"} "csexp" {= "1.5.2"} + "ctypes" {= "0.23.0"} + "ctypes-foreign" {= "0.23.0"} "diffable" {= "v0.16.0"} + "domain-name" {= "0.4.0"} "dune" {= "3.16.0"} "dune-build-info" {= "3.16.0"} "dune-configurator" {= "3.16.0"} "dune-rpc" {= "3.16.0"} "dyn" {= "3.16.0"} "either" {= "1.0.0"} + "expect_test_helpers_core" {= "v0.16.0"} "ezjs_idb" {= "0.1.1"} "ezjs_min" {= "0.3.0"} "fiber" {= "3.7.0"} "fieldslib" {= "v0.16.0"} "fix" {= "20230505"} - "fmt" {= "0.9.0" & with-test} + "fmt" {= "0.9.0"} "fpath" {= "0.7.3"} + "fuzzy_match" {= "v0.16.0"} "gen" {= "1.1"} "gen_js_api" {= "1.1.2"} "incr_dom" {= "v0.16.0"} "incr_map" {= "v0.16.0"} "incr_select" {= "v0.16.0"} "incremental" {= "v0.16.1"} + "indentation_buffer" {= "v0.16.0"} "int_repr" {= "v0.16.0"} + "integers" {= "0.7.0"} + "ipaddr" {= "5.6.0"} + "ipaddr-sexp" {= "5.6.0"} "jane-street-headers" {= "v0.16.0"} "janestreet_lru_cache" {= "v0.16.1"} "js_of_ocaml" {= "5.8.2"} "js_of_ocaml-compiler" {= "5.8.2"} "js_of_ocaml-ppx" {= "5.8.2"} "js_of_ocaml_patches" {= "v0.16.0"} + "jsonm" {= "1.0.2"} "jsonrpc" {= "1.19.0"} "jst-config" {= "v0.16.0"} "junit" {= "2.0.2" & with-test} "junit_alcotest" {= "2.0.2" & with-test} "lambdasoup" {= "1.0.0"} + "logs" {= "0.7.0"} "lsp" {= "1.19.0"} "lwt" {= "5.7.0"} + "macaddr" {= "5.6.0"} + "magic-mime" {= "1.3.1"} "markup" {= "1.0.3"} "menhir" {= "20231231"} "menhirCST" {= "20231231"} @@ -85,11 +121,13 @@ depends: [ "ocaml-base-compiler" {= "5.2.0"} "ocaml-compiler-libs" {= "v0.17.0"} "ocaml-config" {= "3"} + "ocaml-embed-file" {= "v0.16.0"} "ocaml-index" {= "1.0"} "ocaml-lsp-server" {= "1.19.0"} "ocaml-options-vanilla" {= "1"} "ocaml-syntax-shims" {= "1.0.0"} "ocaml-version" {= "3.6.7"} + "ocaml_intrinsics" {= "v0.16.1"} "ocamlbuild" {= "0.14.3"} "ocamlc-loc" {= "3.16.0"} "ocamlfind" {= "1.9.6"} @@ -104,7 +142,11 @@ depends: [ "ojs" {= "1.1.2"} "omd" {= "2.0.0~alpha4"} "ordering" {= "3.16.0"} + "ordinal_abbreviation" {= "v0.16.0"} "parsexp" {= "v0.16.0"} + "patdiff" {= "v0.16.1"} + "patience_diff" {= "v0.16.0"} + "polling_state_rpc" {= "v0.16.0"} "pp" {= "1.2.0"} "ppx_assert" {= "v0.16.0"} "ppx_base" {= "v0.16.0"} @@ -112,6 +154,7 @@ depends: [ "ppx_bin_prot" {= "v0.16.0"} "ppx_cold" {= "v0.16.0"} "ppx_compare" {= "v0.16.0"} + "ppx_css" {= "v0.16.0"} "ppx_custom_printf" {= "v0.16.0"} "ppx_derivers" {= "1.2.1"} "ppx_deriving" {= "6.0.2"} @@ -141,19 +184,24 @@ depends: [ "ppx_stable_witness" {= "v0.16.0"} "ppx_string" {= "v0.16.0"} "ppx_tydi" {= "v0.16.0"} + "ppx_typed_fields" {= "v0.16.0"} "ppx_typerep_conv" {= "v0.16.0"} "ppx_variants_conv" {= "v0.16.0"} "ppx_yojson_conv" {= "v0.16.0"} "ppx_yojson_conv_lib" {= "v0.16.0"} - "ppxlib" {= "0.32.1"} + "ppxlib" {= "0.33.0"} + "profunctor" {= "v0.16.0"} "protocol_version_header" {= "v0.16.0"} "ptime" {= "1.1.0" & with-test} "ptmap" {= "2.0.5"} "re" {= "1.11.0"} "reason" {= "3.12.0"} + "record_builder" {= "v0.16.0"} "result" {= "1.5"} "sedlex" {= "3.2"} "seq" {= "base"} + "sexp_grammar" {= "v0.16.0"} + "sexp_pretty" {= "v0.16.0"} "sexplib" {= "v0.16.0"} "sexplib0" {= "v0.16.0"} "spawn" {= "v0.15.1"} @@ -164,7 +212,11 @@ depends: [ "stored_reversed" {= "v0.16.0"} "streamable" {= "v0.16.1"} "stringext" {= "1.6.0"} + "textutils" {= "v0.16.0"} + "textutils_kernel" {= "v0.16.0"} + "tilde_f" {= "v0.16.0"} "time_now" {= "v0.16.0"} + "timezone" {= "v0.16.0"} "topkg" {= "1.0.7"} "typerep" {= "v0.16.0"} "tyxml" {= "4.6.0"} From 320611eb3da65a2ea8840e0f56297394659ad63d Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 27 Sep 2024 15:22:14 -0400 Subject: [PATCH 30/53] Tidy up --- src/haz3lweb/Main.re | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index f884404d17..0fe76fe63c 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -63,6 +63,8 @@ let app = ~default_model=Model.load(Model.blank), ); +/* This subcomponent is used to run an effect once when the app starts up, + After the first draw */ let on_startup = effect => { let%sub startup_completed = Bonsai.toggle'(~default_model=false); let%sub after_display = { @@ -74,7 +76,7 @@ let on_startup = effect => { | {state: true, _} => Bonsai.Computation.return(Ui_effect.Ignore) }; }; - Bonsai.Edge.lifecycle(~after_display, ()); + Bonsai.Edge.after_display(after_display); }; let view = { From 76d1b0a60ea5979c13f71f7e1dc6b0f0a8f4e16f Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 27 Sep 2024 15:28:41 -0400 Subject: [PATCH 31/53] Remove state from apply --- src/haz3lweb/Main.re | 2 +- src/haz3lweb/Update.re | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index 0fe76fe63c..af8058b770 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -31,7 +31,7 @@ let apply = (model, action, ~schedule_action): Model.t => { last_edit_action := JsUtil.timestamp(); switch ( try({ - let new_model = Update.apply(model, action, (), ~schedule_action); + let new_model = Update.apply(model, action, ~schedule_action); Log.update(action); new_model; }) { diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 26324a9c2e..1aacb159f3 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -397,9 +397,7 @@ let ui_state_update = }; }; -let apply = - (model: Model.t, update: t, _state: State.t, ~schedule_action) - : Result.t(Model.t) => { +let apply = (model: Model.t, update: t, ~schedule_action): Result.t(Model.t) => { let perform_action = (model: Model.t, a: Action.t): Result.t(Model.t) => { switch ( Editors.perform_action(~settings=model.settings.core, model.editors, a) From 503e2356ce6d5c3d0824d2939403029960cb6840 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 28 Sep 2024 15:56:49 -0400 Subject: [PATCH 32/53] Update dependencies and minimize changes post bonsai --- dune-project | 2 +- hazel.opam | 2 +- hazel.opam.locked | 52 +++++++++++++++++++++++------------------------ 3 files changed, 27 insertions(+), 29 deletions(-) diff --git a/dune-project b/dune-project index dd2aafe478..1194593485 100644 --- a/dune-project +++ b/dune-project @@ -34,7 +34,7 @@ bonsai ppx_deriving ptmap - uuidm + (uuidm (= 0.9.8)) ; 0.9.9 has breaking deprecated changes unionFind ocamlformat (junit_alcotest :with-test) diff --git a/hazel.opam b/hazel.opam index 03973e9189..e78b188325 100644 --- a/hazel.opam +++ b/hazel.opam @@ -19,7 +19,7 @@ depends: [ "bonsai" "ppx_deriving" "ptmap" - "uuidm" + "uuidm" {= "0.9.8"} "unionFind" "ocamlformat" "junit_alcotest" {with-test} diff --git a/hazel.opam.locked b/hazel.opam.locked index 04c2cb9507..b2cfce2cea 100644 --- a/hazel.opam.locked +++ b/hazel.opam.locked @@ -11,7 +11,7 @@ bug-reports: "https://github.com/hazelgrove/hazel/issues" depends: [ "abstract_algebra" {= "v0.16.0"} "alcotest" {= "1.8.0" & with-test} - "angstrom" {= "0.16.0"} + "angstrom" {= "0.16.1"} "astring" {= "0.8.5"} "async" {= "v0.16.0"} "async_durable" {= "v0.16.0"} @@ -36,7 +36,7 @@ depends: [ "base_quickcheck" {= "v0.16.0"} "bigarray-compat" {= "1.1.0"} "bignum" {= "v0.16.0"} - "bigstringaf" {= "0.9.1"} + "bigstringaf" {= "0.10.0"} "bin_prot" {= "v0.16.0"} "bonsai" {= "v0.16.0"} "camlp-streams" {= "5.0.1"} @@ -45,8 +45,8 @@ depends: [ "cohttp" {= "5.3.1"} "cohttp-async" {= "5.3.0"} "cohttp_async_websocket" {= "v0.16.0"} - "conduit" {= "7.0.0"} - "conduit-async" {= "7.0.0"} + "conduit" {= "7.1.0"} + "conduit-async" {= "7.1.0"} "conf-bash" {= "1"} "conf-gmp" {= "4"} "conf-gmp-powm-sec" {= "3"} @@ -58,7 +58,7 @@ depends: [ "core_bench" {= "v0.16.0"} "core_kernel" {= "v0.16.0"} "core_unix" {= "v0.16.0"} - "cppo" {= "1.6.9"} + "cppo" {= "1.7.0"} "crunch" {= "3.3.1" & with-doc} "cryptokit" {= "1.16.1"} "csexp" {= "1.5.2"} @@ -82,7 +82,7 @@ depends: [ "fpath" {= "0.7.3"} "fuzzy_match" {= "v0.16.0"} "gen" {= "1.1"} - "gen_js_api" {= "1.1.2"} + "gen_js_api" {= "1.1.3"} "incr_dom" {= "v0.16.0"} "incr_map" {= "v0.16.0"} "incr_select" {= "v0.16.0"} @@ -103,43 +103,41 @@ depends: [ "jst-config" {= "v0.16.0"} "junit" {= "2.0.2" & with-test} "junit_alcotest" {= "2.0.2" & with-test} - "lambdasoup" {= "1.0.0"} + "lambdasoup" {= "1.1.1"} "logs" {= "0.7.0"} "lsp" {= "1.19.0"} - "lwt" {= "5.7.0"} "macaddr" {= "5.6.0"} "magic-mime" {= "1.3.1"} "markup" {= "1.0.3"} - "menhir" {= "20231231"} - "menhirCST" {= "20231231"} - "menhirLib" {= "20231231"} - "menhirSdk" {= "20231231"} + "menhir" {= "20240715"} + "menhirCST" {= "20240715"} + "menhirLib" {= "20240715"} + "menhirSdk" {= "20240715"} "merlin-extend" {= "0.6.1"} - "merlin-lib" {= "5.1-502"} - "num" {= "1.5"} + "merlin-lib" {= "5.2.1-502"} + "num" {= "1.5-1"} "ocaml" {= "5.2.0"} "ocaml-base-compiler" {= "5.2.0"} "ocaml-compiler-libs" {= "v0.17.0"} "ocaml-config" {= "3"} "ocaml-embed-file" {= "v0.16.0"} - "ocaml-index" {= "1.0"} + "ocaml-index" {= "1.1"} "ocaml-lsp-server" {= "1.19.0"} "ocaml-options-vanilla" {= "1"} "ocaml-syntax-shims" {= "1.0.0"} - "ocaml-version" {= "3.6.7"} + "ocaml-version" {= "3.6.9"} "ocaml_intrinsics" {= "v0.16.1"} - "ocamlbuild" {= "0.14.3"} + "ocamlbuild" {= "0.15.0"} "ocamlc-loc" {= "3.16.0"} "ocamlfind" {= "1.9.6"} "ocamlformat" {= "0.26.2"} "ocamlformat-lib" {= "0.26.2"} "ocamlformat-rpc-lib" {= "0.26.2"} "ocp-indent" {= "1.8.1"} - "ocplib-endian" {= "1.2"} "octavius" {= "1.2.2"} - "odoc" {= "2.4.2" & with-doc} - "odoc-parser" {= "2.4.2" & with-doc} - "ojs" {= "1.1.2"} + "odoc" {= "2.4.3" & with-doc} + "odoc-parser" {= "2.4.3" & with-doc} + "ojs" {= "1.1.3"} "omd" {= "2.0.0~alpha4"} "ordering" {= "3.16.0"} "ordinal_abbreviation" {= "v0.16.0"} @@ -192,9 +190,9 @@ depends: [ "ppxlib" {= "0.33.0"} "profunctor" {= "v0.16.0"} "protocol_version_header" {= "v0.16.0"} - "ptime" {= "1.1.0" & with-test} + "ptime" {= "1.2.0" & with-test} "ptmap" {= "2.0.5"} - "re" {= "1.11.0"} + "re" {= "1.12.0"} "reason" {= "3.12.0"} "record_builder" {= "v0.16.0"} "result" {= "1.5"} @@ -224,16 +222,16 @@ depends: [ "unionFind" {= "20220122"} "uri" {= "4.4.0"} "uri-sexp" {= "4.4.0"} - "uucp" {= "15.1.0"} + "uucp" {= "16.0.0"} "uuidm" {= "0.9.8"} - "uunf" {= "15.1.0"} - "uuseg" {= "15.1.0"} + "uunf" {= "16.0.0"} + "uuseg" {= "16.0.0"} "uutf" {= "1.0.3"} "variantslib" {= "v0.16.0"} "virtual_dom" {= "v0.16.0"} "xdg" {= "3.16.0"} "yojson" {= "2.2.2"} - "zarith" {= "1.13"} + "zarith" {= "1.14"} "zarith_stubs_js" {= "v0.16.1"} ] build: [ From 202a0db565d62850ec27602475100801dde304b7 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 30 Sep 2024 15:33:02 -0400 Subject: [PATCH 33/53] Add some additional tests to be useful for the labeled tuples branch - Test_Statics for determining the type of the given expression - Test_Elaboration adds a unapplied function --- src/haz3lcore/lang/term/IdTagged.re | 5 + test/Test_Elaboration.re | 23 +++-- test/Test_Statics.re | 140 ++++++++++++++++++++++++++++ test/haz3ltest.re | 5 +- 4 files changed, 160 insertions(+), 13 deletions(-) create mode 100644 test/Test_Statics.re diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/haz3lcore/lang/term/IdTagged.re index 084a252de4..3812b0e83f 100644 --- a/src/haz3lcore/lang/term/IdTagged.re +++ b/src/haz3lcore/lang/term/IdTagged.re @@ -14,6 +14,11 @@ type t('a) = { term: 'a, }; +// To be used if you want to remove the id from the debug output +// let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit = +// (fmt_a, formatter, ta) => { +// fmt_a(formatter, ta.term); +// }; let fresh = term => { {ids: [Id.mk()], copied: false, term}; }; diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 1c5a7c7271..2bd2c5ef1a 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -74,20 +74,18 @@ let consistent_if = () => dhexp_of_uexp(u6), ); -let u7: Exp.t = - Ap( - Forward, - Fun( - Var("x") |> Pat.fresh, - BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) - |> Exp.fresh, - None, - None, - ) - |> Exp.fresh, - Var("y") |> Exp.fresh, +// x => 4 + 5 +let f = + Fun( + Var("x") |> Pat.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, + None, + None, ) |> Exp.fresh; +let unapplied_function = () => alco_check("A function", f, dhexp_of_uexp(f)); + +let u7: 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)); @@ -186,6 +184,7 @@ let elaboration_tests = [ test_case("Let expression", `Quick, let_exp), test_case("Inconsistent binary operation", `Quick, bin_op), test_case("Consistent if statement", `Quick, consistent_if), + test_case("An unapplied function", `Quick, unapplied_function), test_case("Application of function on free variable", `Quick, ap_fun), test_case("Inconsistent case statement", `Quick, inconsistent_case), test_case("Let expression for a function", `Quick, let_fun), diff --git a/test/Test_Statics.re b/test/Test_Statics.re new file mode 100644 index 0000000000..6b0189cf72 --- /dev/null +++ b/test/Test_Statics.re @@ -0,0 +1,140 @@ +open Alcotest; +open Haz3lcore; + +let testable_typ = testable(Fmt.using(Typ.show, Fmt.string), Typ.fast_equal); +module FreshId = { + let arrow = (a, b) => Arrow(a, b) |> Typ.fresh; + let unknown = a => Unknown(a) |> Typ.fresh; + let int = Typ.fresh(Int); + let float = Typ.fresh(Float); + let prod = a => Prod(a) |> Typ.fresh; + let string = Typ.fresh(String); +}; +let ids = List.init(12, _ => Id.mk()); +let id_at = x => x |> List.nth(ids); +let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init); +let alco_check = Alcotest.option(testable_typ) |> Alcotest.check; + +// 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 unapplied_function = () => + alco_check( + "Unknown param", + Some(FreshId.(arrow(unknown(Internal), int))), + type_of( + Fun( + Var("x") |> Pat.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + None, + None, + ) + |> Exp.fresh, + ), + ); + +let tests = [ + test_case("Function with unknown param", `Quick, () => + alco_check( + "x => 4 + 5", + Some(FreshId.(arrow(unknown(Internal), int))), + type_of( + Fun( + Var("x") |> Pat.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + None, + None, + ) + |> Exp.fresh, + ), + ) + ), + test_case("Function with known param", `Quick, () => + alco_check( + "x : Int => 4 + 5", + Some(FreshId.(arrow(int, int))), + type_of( + Fun( + Pat.Cast( + Var("x") |> Pat.fresh, + FreshId.int, + FreshId.unknown(Internal), + ) + |> Pat.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + None, + None, + ) + |> Exp.fresh, + ), + ) + ), + test_case("bifunction", `Quick, () => + alco_check( + "x : Int, y: Int => x + y", + Some(FreshId.(arrow(prod([int, int]), int))), + type_of( + Fun( + Pat.Tuple([ + Pat.Cast( + Var("x") |> Pat.fresh, + FreshId.int, + FreshId.unknown(Internal), + ) + |> Pat.fresh, + Pat.Cast( + Var("y") |> Pat.fresh, + FreshId.int, + FreshId.unknown(Internal), + ) + |> Pat.fresh, + ]) + |> Pat.fresh, + BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh) + |> Exp.fresh, + None, + None, + ) + |> Exp.fresh, + ), + ) + ), + test_case("function application", `Quick, () => + alco_check( + "float_of_int(1)", + Some(FreshId.(float)), + type_of( + Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh) + |> Exp.fresh, + ), + ) + ), + test_case("function deferral", `Quick, () => + alco_check( + "string_sub(\"hello\", 1, _)", + Some(FreshId.(string)), + type_of( + Ap( + Forward, + Var("string_sub") |> Exp.fresh, + Tuple([ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + ), + ) + ), +]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index e405fba7b8..10db05e656 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -4,6 +4,9 @@ let (suite, _) = run_and_report( ~and_exit=false, "Dynamics", - [("Elaboration", Test_Elaboration.elaboration_tests)], + [ + ("Elaboration", Test_Elaboration.elaboration_tests), + ("Statics", Test_Statics.tests), + ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From 0b2782eed183a793ee904409f4439fc012c47f58 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 30 Sep 2024 16:50:27 -0400 Subject: [PATCH 34/53] Remove unnecessary qualifiers --- test/Test_Statics.re | 172 ++++++++++++++++++++----------------------- 1 file changed, 80 insertions(+), 92 deletions(-) diff --git a/test/Test_Statics.re b/test/Test_Statics.re index 6b0189cf72..b8fe0b184e 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -40,101 +40,89 @@ let unapplied_function = () => ), ); -let tests = [ - test_case("Function with unknown param", `Quick, () => - alco_check( - "x => 4 + 5", - Some(FreshId.(arrow(unknown(Internal), int))), - type_of( - Fun( - Var("x") |> Pat.fresh, - BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) - |> Exp.fresh, - None, - None, - ) - |> Exp.fresh, - ), - ) - ), - test_case("Function with known param", `Quick, () => - alco_check( - "x : Int => 4 + 5", - Some(FreshId.(arrow(int, int))), - type_of( - Fun( - Pat.Cast( +let tests = + FreshId.[ + test_case("Function with unknown param", `Quick, () => + alco_check( + "x => 4 + 5", + Some(arrow(unknown(Internal), int)), + type_of( + Fun( Var("x") |> Pat.fresh, - FreshId.int, - FreshId.unknown(Internal), + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + None, + None, ) - |> Pat.fresh, - BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, - None, - None, - ) - |> Exp.fresh, - ), - ) - ), - test_case("bifunction", `Quick, () => - alco_check( - "x : Int, y: Int => x + y", - Some(FreshId.(arrow(prod([int, int]), int))), - type_of( - Fun( - Pat.Tuple([ - Pat.Cast( - Var("x") |> Pat.fresh, - FreshId.int, - FreshId.unknown(Internal), - ) - |> Pat.fresh, - Pat.Cast( - Var("y") |> Pat.fresh, - FreshId.int, - FreshId.unknown(Internal), - ) + ), + ) + ), + test_case("Function with known param", `Quick, () => + alco_check( + "x : Int => 4 + 5", + Some(arrow(int, int)), + type_of( + Fun( + Cast(Var("x") |> Pat.fresh, int, unknown(Internal)) |> Pat.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) + |> Exp.fresh, + None, + None, + ) + |> Exp.fresh, + ), + ) + ), + test_case("bifunction", `Quick, () => + alco_check( + "x : Int, y: Int => x + y", + Some(arrow(prod([int, int]), int)), + type_of( + Fun( + Tuple([ + Cast(Var("x") |> Pat.fresh, int, unknown(Internal)) + |> Pat.fresh, + Cast(Var("y") |> Pat.fresh, int, unknown(Internal)) + |> Pat.fresh, + ]) |> Pat.fresh, - ]) - |> Pat.fresh, - BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh) + BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh) + |> Exp.fresh, + None, + None, + ) |> Exp.fresh, - None, - None, - ) - |> Exp.fresh, - ), - ) - ), - test_case("function application", `Quick, () => - alco_check( - "float_of_int(1)", - Some(FreshId.(float)), - type_of( - Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh) - |> Exp.fresh, - ), - ) - ), - test_case("function deferral", `Quick, () => - alco_check( - "string_sub(\"hello\", 1, _)", - Some(FreshId.(string)), - type_of( - Ap( - Forward, - Var("string_sub") |> Exp.fresh, - Tuple([ - String("hello") |> Exp.fresh, - Int(1) |> Exp.fresh, - Deferral(InAp) |> Exp.fresh, - ]) + ), + ) + ), + test_case("function application", `Quick, () => + alco_check( + "float_of_int(1)", + Some(float), + type_of( + Ap(Forward, Var("float_of_int") |> Exp.fresh, Int(1) |> Exp.fresh) |> Exp.fresh, - ) - |> Exp.fresh, - ), - ) - ), -]; + ), + ) + ), + test_case("function deferral", `Quick, () => + alco_check( + "string_sub(\"hello\", 1, _)", + Some(string), + type_of( + Ap( + Forward, + Var("string_sub") |> Exp.fresh, + Tuple([ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + ), + ) + ), + ]; From 8fbfe3bb80758f256b54a5fce45dd95cb49a3d9e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 1 Oct 2024 11:10:51 -0400 Subject: [PATCH 35/53] Fix function deferral test --- test/Test_Statics.re | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/test/Test_Statics.re b/test/Test_Statics.re index b8fe0b184e..71fdafc8ba 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -109,17 +109,15 @@ let tests = test_case("function deferral", `Quick, () => alco_check( "string_sub(\"hello\", 1, _)", - Some(string), + Some(arrow(int, string)), type_of( - Ap( - Forward, + DeferredAp( Var("string_sub") |> Exp.fresh, - Tuple([ + [ String("hello") |> Exp.fresh, Int(1) |> Exp.fresh, Deferral(InAp) |> Exp.fresh, - ]) - |> Exp.fresh, + ], ) |> Exp.fresh, ), From 854edc88864ca3cb03c128dda8b5bc553dcd2731 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 1 Oct 2024 11:44:15 -0400 Subject: [PATCH 36/53] Add deferral elaboration test --- test/Test_Elaboration.re | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 2bd2c5ef1a..2516f25227 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -177,6 +177,33 @@ let let_fun = () => dhexp_of_uexp(u9), ); +let deferral = () => + alco_check( + "string_sub(\"hello\", 1, _)", + dhexp_of_uexp( + 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, + [ + String("hello") |> Exp.fresh, + Int(1) |> Exp.fresh, + Deferral(InAp) |> Exp.fresh, + ], + ) + |> Exp.fresh, + ), + ); + let elaboration_tests = [ test_case("Single integer", `Quick, single_integer), test_case("Empty hole", `Quick, empty_hole), @@ -188,4 +215,9 @@ let elaboration_tests = [ test_case("Application of function on free variable", `Quick, ap_fun), test_case("Inconsistent case statement", `Quick, inconsistent_case), test_case("Let expression for a function", `Quick, let_fun), + test_case( + "Function application with a deferred argument", + `Quick, + deferral, + ), ]; From 76ed41d82dc1fb426db80942fc72551ff6bcd28c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 1 Oct 2024 11:44:54 -0400 Subject: [PATCH 37/53] Add evaluation tests --- test/Test_Evaluator.re | 44 ++++++++++++++++++++++++++++++++++++++++++ test/haz3ltest.re | 1 + 2 files changed, 45 insertions(+) create mode 100644 test/Test_Evaluator.re diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re new file mode 100644 index 0000000000..fc159425b2 --- /dev/null +++ b/test/Test_Evaluator.re @@ -0,0 +1,44 @@ +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, + msg, + expected, + Evaluator.Result.unbox( + snd(Evaluator.evaluate(Builtins.env_init, {d: unevaluated})), + ), + ); + +let test_int = () => + evaluation_test("8", Int(8) |> Exp.fresh, Int(8) |> Exp.fresh); + +let test_sum = () => + evaluation_test( + "4 + 5", + Int(9) |> Exp.fresh, + BinOp(Int(Plus), Int(4) |> Exp.fresh, Int(5) |> Exp.fresh) |> Exp.fresh, + ); + +let tests = [ + test_case("Integer literal", `Quick, test_int), + test_case("Integer sum", `Quick, test_sum), +]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 10db05e656..3e13ae44b7 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -7,6 +7,7 @@ let (suite, _) = [ ("Elaboration", Test_Elaboration.elaboration_tests), ("Statics", Test_Statics.tests), + ("Evaluator", Test_Evaluator.tests), ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml"); From 33cd14f2cfbbf6c07377c3d1ce1396552e7b591e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 2 Oct 2024 14:44:48 -0400 Subject: [PATCH 38/53] Remove unnecessary print statement --- src/haz3lweb/Editors.re | 1 - 1 file changed, 1 deletion(-) diff --git a/src/haz3lweb/Editors.re b/src/haz3lweb/Editors.re index 7b5512fc10..f8fa4e0b06 100644 --- a/src/haz3lweb/Editors.re +++ b/src/haz3lweb/Editors.re @@ -56,7 +56,6 @@ let perform_action = CoreSettings.on | _ => settings }; - print_endline("action: " ++ Action.show(a)); switch (Perform.go(~settings, a, get_editor(editors))) { | Error(err) => Error(FailedToPerform(err)) | Ok(ed) => Ok(put_editor(ed, editors)) 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 39/53] 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 40/53] 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 41/53] 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 42/53] 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 43/53] 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 ad1c1b5ca5427991db7dadf3f221715df044b583 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 10:53:18 -0400 Subject: [PATCH 44/53] Readd warnings failing build in dev but exclude some unused warnings - The idea is to make development easier by allowing code to be built with unused warnings - We're still restrictive on some warnings because dune won't output all warnings on every build --- dune-workspace | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dune-workspace b/dune-workspace index 480ccb1514..6268c15bd9 100644 --- a/dune-workspace +++ b/dune-workspace @@ -1,9 +1,10 @@ (lang dune 3.16) +; List of warning codes found at https://ocaml.org/manual/5.2/comp.html#s:comp-options (env (dev (flags - (:standard -warn-error -A))) + (:standard -warn-error +A-26-27-32-33-34-35-38-39-58))) ; Disable some unused warnings. (release (flags (:standard -warn-error +A-58)))) From 518a33970fdbed09f80c0786bfee9af2a636a3fd Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 12:15:02 -0400 Subject: [PATCH 45/53] Fix module reference --- test/Test_Evaluator.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index fc159425b2..9e4ade6651 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -16,7 +16,7 @@ let type_of = f => { }; let int_evaluation = - Evaluator.evaluate(Builtins.env_init, {d: Exp.Int(8) |> Exp.fresh}); + Evaluator.evaluate(Builtins.env_init, {d: Int(8) |> Exp.fresh}); let evaluation_test = (msg, expected, unevaluated) => check( From 3e79efcc211f80806518f1d387bce4c4e5b3e553 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 16:15:48 -0400 Subject: [PATCH 46/53] Simplify disabled warnings --- dune-workspace | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dune-workspace b/dune-workspace index 6268c15bd9..93d6e50904 100644 --- a/dune-workspace +++ b/dune-workspace @@ -4,7 +4,7 @@ (env (dev (flags - (:standard -warn-error +A-26-27-32-33-34-35-38-39-58))) ; Disable some unused warnings. + (:standard -warn-error +A-26-27-K-58))) ; Disable some unused warnings. (release (flags (:standard -warn-error +A-58)))) 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 47/53] 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 48/53] 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 49/53] 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 50/53] 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 51/53] 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", + ) + }), ]; From 5200ef7c2856efafa96cce253d906bb70f834254 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 31 Oct 2024 11:51:46 -0400 Subject: [PATCH 52/53] Fix Saving --- src/haz3lweb/Main.re | 79 +++++++++++++++++++++++------------------- src/haz3lweb/Update.re | 4 ++- src/haz3lweb/dune | 3 +- src/util/BonsaiUtil.re | 42 ++++++++++++++++++++++ src/util/Util.re | 1 + src/util/dune | 3 +- 6 files changed, 94 insertions(+), 38 deletions(-) create mode 100644 src/util/BonsaiUtil.re diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index af8058b770..6491074920 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -4,8 +4,6 @@ open Haz3lweb; open Bonsai.Let_syntax; let scroll_to_caret = ref(true); -let edit_action_applied = ref(true); -let last_edit_action = ref(JsUtil.timestamp()); let restart_caret_animation = () => // necessary to trigger reflow @@ -19,16 +17,24 @@ let restart_caret_animation = () => | _ => () }; -let apply = (model, action, ~schedule_action): Model.t => { +let apply = (model, action, ~schedule_action, ~schedule_autosave): Model.t => { restart_caret_animation(); if (UpdateAction.is_edit(action)) { - last_edit_action := JsUtil.timestamp(); - edit_action_applied := true; + schedule_autosave( + BonsaiUtil.Alarm.Action.SetAlarm( + Core.Time_ns.add(Core.Time_ns.now(), Core.Time_ns.Span.of_sec(2.0)), + ), + ); + } else { + schedule_autosave( + BonsaiUtil.Alarm.Action.SnoozeAlarm( + Core.Time_ns.add(Core.Time_ns.now(), Core.Time_ns.Span.of_sec(2.0)), + ), + ); }; if (Update.should_scroll_to_caret(action)) { scroll_to_caret := true; }; - last_edit_action := JsUtil.timestamp(); switch ( try({ let new_model = Update.apply(model, action, ~schedule_action); @@ -53,16 +59,6 @@ let apply = (model, action, ~schedule_action): Model.t => { }; }; -let app = - Bonsai.state_machine0( - (module Model), - (module Update), - ~apply_action= - (~inject, ~schedule_event) => - apply(~schedule_action=x => schedule_event(inject(x))), - ~default_model=Model.load(Model.blank), - ); - /* This subcomponent is used to run an effect once when the app starts up, After the first draw */ let on_startup = effect => { @@ -80,31 +76,44 @@ let on_startup = effect => { }; let view = { - let%sub app = app; + let%sub save_scheduler = BonsaiUtil.Alarm.alarm; + let%sub app = + Bonsai.state_machine1( + (module Model), + (module Update), + ~apply_action= + (~inject, ~schedule_event, input) => { + let schedule_action = x => schedule_event(inject(x)); + let schedule_autosave = action => + switch (input) { + | Active((_, alarm_inject)) => + schedule_event(alarm_inject(action)) + | Inactive => () + }; + apply(~schedule_action, ~schedule_autosave); + }, + ~default_model=Model.load(Model.blank), + save_scheduler, + ); let%sub () = { on_startup( Bonsai.Value.map(~f=((_model, inject)) => inject(Startup), app), ); }; - let%sub after_display = { - let%arr (_model, inject) = app; - if (scroll_to_caret.contents) { - scroll_to_caret := false; - JsUtil.scroll_cursor_into_view_if_needed(); - }; - if (edit_action_applied^ - && JsUtil.timestamp() - -. last_edit_action^ > 1000.0) { - /* If an edit action has been applied, but no other edit action - has been applied for 1 second, save the model. */ - edit_action_applied := false; - print_endline("Saving..."); - inject(Update.Save); - } else { - Ui_effect.Ignore; - }; + let after_display = { + Bonsai.Effect.of_sync_fun( + () => + if (scroll_to_caret.contents) { + scroll_to_caret := false; + JsUtil.scroll_cursor_into_view_if_needed(); + }, + (), + ); }; - let%sub () = Bonsai.Edge.after_display(after_display); + let save_effect = Bonsai.Value.map(~f=((_, g)) => g(Update.Save), app); + let%sub () = BonsaiUtil.Alarm.listen(save_scheduler, ~event=save_effect); + let%sub () = + Bonsai.Edge.after_display(after_display |> Bonsai.Value.return); let%arr (model, inject) = app; Haz3lweb.Page.view(~inject, model); }; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 1aacb159f3..778df5114a 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -430,7 +430,9 @@ let apply = (model: Model.t, update: t, ~schedule_action): Result.t(Model.t) => | DebugConsole(key) => DebugConsole.print(model, key); Ok(model); - | Save => Model.save_and_return(model) + | Save => + print_endline("Saving..."); + Model.save_and_return(model); | InitImportAll(file) => JsUtil.read_file(file, data => schedule_action(FinishImportAll(data))); Ok(model); diff --git a/src/haz3lweb/dune b/src/haz3lweb/dune index d3e42ec636..d826004fca 100644 --- a/src/haz3lweb/dune +++ b/src/haz3lweb/dune @@ -55,7 +55,8 @@ ppx_let ppx_sexp_conv ppx_deriving.show - ppx_yojson_conv))) + ppx_yojson_conv + bonsai.ppx_bonsai))) (executable (name main) diff --git a/src/util/BonsaiUtil.re b/src/util/BonsaiUtil.re new file mode 100644 index 0000000000..127172ce21 --- /dev/null +++ b/src/util/BonsaiUtil.re @@ -0,0 +1,42 @@ +open Core; +open Bonsai; +open Bonsai.Let_syntax; + +module Alarm = { + module Action = { + [@deriving sexp] + type t = + | SetAlarm(Time_ns.Alternate_sexp.t) + | SnoozeAlarm(Time_ns.Alternate_sexp.t) + | UnsetAlarm; + }; + + let alarm = + state_machine0( + (module Time_ns.Alternate_sexp), + (module Action), + ~default_model=Time_ns.max_value_representable, + ~apply_action=(~inject as _, ~schedule_event as _, model, action) => { + switch (action) { + | SetAlarm(time) => time + | SnoozeAlarm(time) => Time_ns.max(time, model) + | UnsetAlarm => Time_ns.max_value_representable + } + }); + + let listen = (alarm, ~event) => { + let%sub before_or_after = Clock.at(alarm |> Value.map(~f=fst)); + Edge.on_change( + (module Clock.Before_or_after), + before_or_after, + ~callback={ + open Clock.Before_or_after; + let%map (_, inject) = alarm + and event = event; + fun + | After => Effect.Many([inject(Action.UnsetAlarm), event]) + | Before => Effect.Ignore; + }, + ); + }; +}; diff --git a/src/util/Util.re b/src/util/Util.re index c901907b60..2c7f084100 100644 --- a/src/util/Util.re +++ b/src/util/Util.re @@ -1,4 +1,5 @@ module Aba = Aba; +module BonsaiUtil = BonsaiUtil; module Direction = Direction; module Either = Either; module IntMap = IntMap; diff --git a/src/util/dune b/src/util/dune index a3494db579..07f7b7d8da 100644 --- a/src/util/dune +++ b/src/util/dune @@ -8,7 +8,8 @@ js_of_ocaml-ppx ppx_let ppx_sexp_conv - ppx_deriving.show))) + ppx_deriving.show + bonsai.ppx_bonsai))) (env (dev From 0b4eb934a2aa48b8a91d8242a7bf811375198269 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 31 Oct 2024 11:55:53 -0400 Subject: [PATCH 53/53] Switch back to 1s --- src/haz3lweb/Main.re | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re index 6491074920..16811a32cb 100644 --- a/src/haz3lweb/Main.re +++ b/src/haz3lweb/Main.re @@ -22,13 +22,13 @@ let apply = (model, action, ~schedule_action, ~schedule_autosave): Model.t => { if (UpdateAction.is_edit(action)) { schedule_autosave( BonsaiUtil.Alarm.Action.SetAlarm( - Core.Time_ns.add(Core.Time_ns.now(), Core.Time_ns.Span.of_sec(2.0)), + Core.Time_ns.add(Core.Time_ns.now(), Core.Time_ns.Span.of_sec(1.0)), ), ); } else { schedule_autosave( BonsaiUtil.Alarm.Action.SnoozeAlarm( - Core.Time_ns.add(Core.Time_ns.now(), Core.Time_ns.Span.of_sec(2.0)), + Core.Time_ns.add(Core.Time_ns.now(), Core.Time_ns.Span.of_sec(1.0)), ), ); };