Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Random generation of UExps #1337

Draft
wants to merge 16 commits into
base: dev
Choose a base branch
from
Draft
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Version_autogenerated.re
# ocamlbuild working directory
_build/
_opam/
_coverage/

# ocamlbuild targets
*.byte
Expand Down Expand Up @@ -53,3 +54,4 @@ setup.log

# unit tests
*.xml
*.coverage
3 changes: 2 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,9 @@ repl:
dune utop src/haz3lcore

test:
dune build @src/fmt @test/fmt --auto-promote src test --profile dev
dune build @src/fmt @test/fmt --auto-promote src test --profile dev --instrument-with bisect_ppx
node $(TEST_DIR)/haz3ltest.bc.js
bisect-ppx-report html

clean:
dune clean
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ for a type named something else like `q`, it will be `show_q`.
If Hazel is hanging on load or when you perform certain actions, you can load into Debug Mode by appending `#debug` to the URL and reloading. From there, you have some buttons that will change settings or reset local storage. Refresh without the `#debug` flag and hopefully you can resolve the situation from there.

#### Testing
You can run all of the unit tests located in `test` by running `make test`.
You can run all of the unit tests and randomly generated tests located in `test` by running `make test`.

Unit tests are written using the [Alcotest framework](https://github.com/mirage/alcotest).

Expand Down
2 changes: 2 additions & 0 deletions opam.export
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ installed: [
"bignum.v0.16.0"
"bigstringaf.0.9.1"
"bin_prot.v0.16.0"
"bisect_ppx.2.8.3"
"camlp-streams.5.0.1"
"cmdliner.1.3.0"
"conf-bash.1"
Expand Down Expand Up @@ -144,6 +145,7 @@ installed: [
"protocol_version_header.v0.16.0"
"ptime.1.1.0"
"ptmap.2.0.5"
"qcheck-alcotest.0.21.3"
"re.1.11.0"
"reason.3.11.0"
"result.1.5"
Expand Down
2 changes: 2 additions & 0 deletions src/haz3lcore/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@
(library
(name haz3lcore)
(libraries util re sexplib unionFind uuidm yojson core)
(instrumentation
(backend bisect_ppx))
(js_of_ocaml
(flags
(:include js-of-ocaml-flags-%{profile})))
Expand Down
17 changes: 12 additions & 5 deletions src/haz3lcore/dynamics/TypeAssignment.re
Original file line number Diff line number Diff line change
Expand Up @@ -319,11 +319,18 @@ let rec typ_of_dhexp =
};
};

let property_test = (uexp_typ: Typ.t, dhexp: DHExp.t, m: Statics.Map.t): bool => {
let dhexp_typ = typ_of_dhexp(Builtins.ctx_init, m, dhexp);
let property_test =
(uexp_typ: option(Typ.t), dhexp: option(DHExp.t), m: Statics.Map.t)
: bool => {
let dhexp_typ =
switch (dhexp) {
| None => None
| Some(dhexp) => typ_of_dhexp(Builtins.ctx_init, m, dhexp)
};

switch (dhexp_typ) {
| None => false
| Some(dh_typ) => Typ.eq(dh_typ, uexp_typ)
switch (uexp_typ, dhexp_typ) {
| (None, None) => true
| (Some(uexp_typ), Some(dhexp_typ)) => Typ.eq(dhexp_typ, uexp_typ)
| _ => false
};
};
Comment on lines -322 to 336
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should move this to the test file.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Up to you but the property can also be written as:

let property_test =
    (uexp_typ: option(Typ.t), dhexp: option(DHExp.t), m: Statics.Map.t)
    : bool => {
  let dhexp_typ = Option.bind(dhexp, typ_of_dhexp(Builtins.ctx_init, m))

  Option.equal(Typ.eq, uexp_typ, dhexp_typ);
};

Loading
Loading