Merge branch 'dev' into omd-dependency-update

INSTALL.md

@@ -119,16 +119,16 @@ follow these instructions instead of the shorter instructions in the
   opam update
   ```
 
-- Install OCaml 5.0.0 (some older versions may also work; see the
+- Install OCaml 5.2.0 (some older versions may also work; see the
   ["Current version" section of `Updating.md`](docs/Updating-OCaml-Version.md) for
   why we may not use the newest version of OCaml).
 
   ```sh
-   opam switch create 5.0.0 ocaml-base-compiler.5.0.0
+   opam switch create 5.2.0 ocaml-base-compiler.5.2.0
   ```
 - Update the current switch environment
   ```sh
-  eval $(opam env --switch=5.0.0)
+  eval $(opam env --switch=5.2.0)
   ```
 ## Clone the Source Code
 

Makefile

@@ -12,6 +12,7 @@ deps:
 
 change-deps:
 	opam switch export opam.export
+	sed -i '' '/host-/d' opam.export # remove host- lines which are arch-specific
 
 setup-instructor:
 	cp src/haz3lweb/ExerciseSettings_instructor.re src/haz3lweb/ExerciseSettings.re

README.md

@@ -17,7 +17,7 @@ can also be accessed at:
 
 ### Short version
 
-If you already have `ocaml` version 5.0.0 and least version 2.0 of `opam`
+If you already have `ocaml` version 5.2.0 and at least version 2.0 of `opam`
 installed, you can build Hazel by running the following commands.
 
 - `git clone [email protected]:hazelgrove/hazel.git`
@@ -155,7 +155,7 @@ To obtain an clean build, you may need to:
 
   ```sh
   # opam switch remove ./
-  opam switch create ./ 5.0.0
+  opam switch create ./ 5.2.0
   eval $(opam env)
   make deps
   make
@@ -205,3 +205,12 @@ that will build that branch (in `release` mode) and deploy it to the URL
 It usually takes about 2 minutes if the build environment cache hits, or 
 20+ minutes if not. You can view the status of the build in the [Actions 
 tab on Github](https://github.com/hazelgrove/hazel/actions).
+
+Builds prior to July 2024 are archived at `https://hazel.org/build/<branch name>`.
+
+Note: If another archive needs to be performed, make sure to redeploy the following
+branches manually since we refer to them in various public material (websites and
+published papers):
+
+  dev
+  livelits

docs/Updating-OCaml-Version.md

@@ -2,7 +2,7 @@
 
 ## Current version
 
-The most recent version that we use is Ocaml 5.0.0.
+The most recent version that we use is Ocaml 5.2.0.
 If there are known issues with more recent version of OCaml, we will list them here.
 
 ## How to update Hazel to use a new version of ocaml
@@ -16,15 +16,15 @@ To update do the following:
 - `opam switch list-available`
 
 - Choose the most recent version, but no later than the public release on 
-  ocaml.org (e.g., `5.0.0`).
+  ocaml.org (e.g., `5.2.0`).
 
 - Create a new branch called `update_ocaml_VERSION` where VERSION is the 
   version of OCaml you intend to upgrade to. 
 
     `git checkout -b update_ocaml_VERSION`
 
 - `opam switch create VERSION`, where `VERSION` is the most recent OCaml version
-  that does not contain a `+` character (e.g., `4.12.1`).
+  that does not contain a `+` character (e.g., `5.2.0`).
 
 - `make deps`
 
@@ -59,10 +59,23 @@ To update do the following:
       
       - Merge your branch with either `dev` or `update_ocaml_VERSION` if that is tricky.
 
-      - Update your OCaml installation by running the following:
+      - Update your `opam`.
 
         ```
         opam update
+        ```
+
+        If you get the following warning:
+
+        ```
+        [WARNING] opam is out-of-date. Please consider updating it (https://opam.ocaml.org/doc/Install.html)
+        ```
+
+        You may want to update opam by following the instructions for your platform at that link.
+
+      - Update your OCaml installation by running the following:
+
+        ```
         opam switch create VERSION
         eval $(opam env)
         make deps

opam.export

@@ -1,26 +1,13 @@
 opam-version: "2.0"
-compiler: [
-  "base-bigarray.base"
-  "base-domains.base"
-  "base-nnp.base"
-  "base-threads.base"
-  "base-unix.base"
-  "host-arch-arm64.1"
-  "host-system-other.1"
-  "ocaml.5.2.0"
-  "ocaml-base-compiler.5.2.0"
-  "ocaml-config.3"
-  "ocaml-options-vanilla.1"
-]
+compiler: ["ocaml-base-compiler.5.2.0"]
 roots: [
   "core.v0.16.2"
   "ezjs_idb.0.1.1"
   "ezjs_min.0.3.0"
   "incr_dom.v0.16.0"
   "js_of_ocaml-ppx.5.8.2"
-  "merlin.5.1-502"
+  "junit_alcotest.2.0.2"
   "ocaml-base-compiler.5.2.0"
-  "ocaml-lsp-server.1.18.0~5.2preview"
   "ocamlformat.0.26.2"
   "omd.2.0.0~alpha4"
   "ppx_deriving.6.0.2"
@@ -36,6 +23,7 @@ roots: [
 ]
 installed: [
   "abstract_algebra.v0.16.0"
+  "alcotest.1.8.0"
   "angstrom.0.16.0"
   "astring.0.8.5"
   "async_js.v0.16.0"
@@ -71,11 +59,10 @@ installed: [
   "ezjs_min.0.3.0"
   "fieldslib.v0.16.0"
   "fix.20230505"
+  "fmt.0.9.0"
   "fpath.0.7.3"
   "gen.1.1"
   "gen_js_api.1.1.2"
-  "host-arch-arm64.1"
-  "host-system-other.1"
   "incr_dom.v0.16.0"
   "incr_map.v0.16.0"
   "incr_select.v0.16.0"
@@ -88,6 +75,8 @@ installed: [
   "js_of_ocaml-ppx.5.8.2"
   "js_of_ocaml_patches.v0.16.0"
   "jst-config.v0.16.0"
+  "junit.2.0.2"
+  "junit_alcotest.2.0.2"
   "lambdasoup.1.0.0"
   "markup.1.0.3"
   "menhir.20231231"
@@ -153,6 +142,7 @@ installed: [
   "ppx_yojson_conv_lib.v0.16.0"
   "ppxlib.0.32.1"
   "protocol_version_header.v0.16.0"
+  "ptime.1.1.0"
   "ptmap.2.0.5"
   "re.1.11.0"
   "reason.3.11.0"

src/haz3lcore/dynamics/Constraint.re

@@ -130,6 +130,7 @@ let of_ap = (ctx, mode, ctr: option(Constructor.t), arg: t, syn_ty): t =>
     switch (ty) {
     | Some(ty) =>
       switch (Typ.weak_head_normalize(ctx, ty)) {
+      | Rec(_, Sum(map))
       | Sum(map) =>
         let num_variants = ConstructorMap.cardinal(map);
         switch (ConstructorMap.nth(map, name)) {

src/haz3lcore/dynamics/DH.re

@@ -15,6 +15,7 @@ module rec DHExp: {
     | InconsistentBranches(MetaVar.t, HoleInstanceId.t, case)
     | Closure([@opaque] ClosureEnvironment.t, t)
     | Filter(DHFilter.t, t)
+    | Undefined
     | BoundVar(Var.t)
     | Sequence(t, t)
     | Let(DHPat.t, t, t)
@@ -39,7 +40,7 @@ module rec DHExp: {
     | ListConcat(t, t)
     | Tuple(list(t))
     | Prj(t, int)
-    | Constructor(string)
+    | Constructor(string, Typ.t)
     | ConsistentCase(case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
@@ -76,6 +77,7 @@ module rec DHExp: {
     | Closure(ClosureEnvironment.t, t)
     | Filter(DHFilter.t, t)
     /* Other expressions forms */
+    | Undefined
     | BoundVar(Var.t)
     | Sequence(t, t)
     | Let(DHPat.t, t, t)
@@ -100,7 +102,7 @@ module rec DHExp: {
     | ListConcat(t, t)
     | Tuple(list(t))
     | Prj(t, int)
-    | Constructor(string)
+    | Constructor(string, Typ.t)
     | ConsistentCase(case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
@@ -117,6 +119,7 @@ module rec DHExp: {
     | NonEmptyHole(_, _, _, _) => "NonEmptyHole"
     | FreeVar(_, _, _) => "FreeVar"
     | InvalidText(_) => "InvalidText"
+    | Undefined => "Undefined"
     | BoundVar(_) => "BoundVar"
     | Sequence(_, _) => "Sequence"
     | Filter(_, _) => "Filter"
@@ -208,6 +211,7 @@ module rec DHExp: {
     | EmptyHole(_) as d
     | FreeVar(_) as d
     | InvalidText(_) as d
+    | Undefined as d
     | BoundVar(_) as d
     | BoolLit(_) as d
     | IntLit(_) as d
@@ -226,6 +230,7 @@ module rec DHExp: {
 
   let rec fast_equal = (d1: t, d2: t): bool => {
     switch (d1, d2) {
+    | (Undefined, _)
     /* Primitive forms: regular structural equality */
     | (BoundVar(_), _)
     /* TODO: Not sure if this is right... */
@@ -404,6 +409,7 @@ module rec DHExp: {
     | FreeVar(_, _, _)
     | InvalidText(_, _, _)
     | Constructor(_)
+    | Undefined
     | BoundVar(_)
     | BoolLit(_)
     | IntLit(_)

src/haz3lcore/dynamics/DHPat.re

@@ -15,7 +15,7 @@ type t =
   | ListLit(Typ.t, list(t))
   | Cons(t, t)
   | Tuple(list(t))
-  | Constructor(string)
+  | Constructor(string, Typ.t)
   | Ap(t, t);
 
 let mk_tuple: list(t) => t =

src/haz3lcore/dynamics/Delta.re

@@ -4,5 +4,9 @@ type hole_sort =
   | PatternHole;
 
 [@deriving sexp]
-type t = MetaVarMap.t((hole_sort, Typ.t, VarCtx.t));
+type val_ty = (hole_sort, Typ.t, Ctx.t);
+
+[@deriving sexp]
+type t = MetaVarMap.t(val_ty);
+
 let empty: t = (MetaVarMap.empty: t);

src/haz3lcore/dynamics/Delta.rei

@@ -4,6 +4,9 @@ type hole_sort =
   | PatternHole;
 
 [@deriving sexp]
-type t = MetaVarMap.t((hole_sort, Typ.t, VarCtx.t));
+type val_ty = (hole_sort, Typ.t, Ctx.t);
+
+[@deriving sexp]
+type t = MetaVarMap.t(val_ty);
 
 let empty: t;

src/haz3lcore/dynamics/Elaborator.re

@@ -96,6 +96,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | EmptyHole(_)
     | NonEmptyHole(_) => d
     /* DHExp-specific forms: Don't cast */
+    | Undefined
     | Cast(_)
     | Closure(_)
     | Filter(_)
@@ -155,6 +156,7 @@ let rec dhexp_of_uexp =
            Make sure new dhexp form is properly considered Indet
            to avoid casting issues. */
         Some(EmptyHole(id, 0))
+      | Undefined => Some(Undefined)
       | Triv => Some(Tuple([]))
       | Deferral(_) => Some(DHExp.InvalidText(id, 0, "_"))
       | Bool(b) => Some(BoolLit(b))
@@ -170,6 +172,7 @@ let rec dhexp_of_uexp =
         let* dp = dhpat_of_upat(m, p);
         let* d1 = dhexp_of_uexp(m, body);
         let+ ty = fixed_pat_typ(m, p);
+        let ty = Typ.normalize(ctx, ty);
         DHExp.Fun(dp, ty, d1, None);
       | TypFun(tpat, body) =>
         let+ d1 = dhexp_of_uexp(m, body);
@@ -187,8 +190,10 @@ let rec dhexp_of_uexp =
         DHExp.ListConcat(dc1, dc2);
       | UnOp(Meta(Unquote), e) =>
         switch (e.term) {
-        | Var("e") when in_filter => Some(Constructor("$e"))
-        | Var("v") when in_filter => Some(Constructor("$v"))
+        | Var("e") when in_filter =>
+          Some(Constructor("$e", Unknown(Internal)))
+        | Var("v") when in_filter =>
+          Some(Constructor("$v", Unknown(Internal)))
         | _ => Some(DHExp.EmptyHole(id, 0))
         }
       | UnOp(Int(Minus), e) =>
@@ -233,7 +238,17 @@ let rec dhexp_of_uexp =
         switch (err_status) {
         | InHole(Common(NoType(FreeConstructor(_)))) =>
           Some(FreeVar(id, 0, name))
-        | _ => Some(Constructor(name))
+        | _ =>
+          let ty =
+            switch (Ctx.lookup_ctr(ctx, name)) {
+            | None => Typ.Unknown(Internal)
+            | Some({typ, _}) => Typ.normalize(ctx, typ)
+            };
+          switch (mode) {
+          | Ana(ana_ty) =>
+            Some(Constructor(name, Typ.normalize(ctx, ana_ty)))
+          | _ => Some(Constructor(name, ty))
+          };
         }
       | Let(p, def, body) =>
         let add_name: (option(string), DHExp.t) => DHExp.t = (
@@ -260,6 +275,7 @@ let rec dhexp_of_uexp =
             dbody,
           );
         } else {
+          let ty = Typ.normalize(ctx, ty);
           switch (Term.UPat.get_bindings(p) |> Option.get) {
           | [f] =>
             /* simple recursion */
@@ -438,7 +454,19 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
       switch (err_status) {
       | InHole(Common(NoType(FreeConstructor(_)))) =>
         Some(BadConstructor(u, 0, name))
-      | _ => wrap(Constructor(name))
+      | _ =>
+        let ty =
+          switch (Ctx.lookup_ctr(ctx, name)) {
+          | None => Typ.Unknown(Internal)
+          | Some({typ, _}) => Typ.normalize(ctx, typ)
+          };
+        let dc =
+          switch (mode) {
+          | Ana(ana_ty) =>
+            DHPat.Constructor(name, Typ.normalize(ctx, ana_ty))
+          | _ => DHPat.Constructor(name, ty)
+          };
+        wrap(dc);
       }
     | Cons(hd, tl) =>
       let* d_hd = dhpat_of_upat(m, hd);

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -46,6 +46,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | IntLit(_)
   | FloatLit(_)
   | StringLit(_)
+  | Undefined
   | Constructor(_) => d |> return
 
   | Sequence(d1, d2) =>
@@ -278,6 +279,7 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
   | IntLit(_)
   | FloatLit(_)
   | StringLit(_)
+  | Undefined
   | Constructor(_) => d |> return
 
   | Test(id, d1) =>
@@ -471,6 +473,7 @@ let rec track_children_of_hole =
   | FloatLit(_)
   | StringLit(_)
   | BuiltinFun(_)
+  | Undefined
   | BoundVar(_) => hii
   | Test(_, d)
   | FixF(_, _, d)