Merge branch 'dev' into fix-probe-duplication

Author: disconcision

CONTRIBUTING.md

@@ -88,6 +88,25 @@ This can be combined with using `make hot` rather than `make serve` to add hot r
 
 ## Debugging
 
+
+### Troubleshooting dependency updates and build failures
+
+- If Hazel fails to compile after you update or pull new dependencies, first run:
+  
+  ```sh
+  make deps
+  ```
+
+- If that doesn't work, your opam switch may be out of sync. Remove and recreate it, then reinstall deps:
+  
+  ```sh
+  # Replace 5.2.0 with the name of your switch
+  opam switch remove 5.2.0
+  ```
+  
+  Then recreate the switch following the steps in this guide (see "Install OCaml" and "Install Library Dependencies"), run `eval $(opam env)`, `make deps`, and rebuild.
+
+
 ### Printing
 You can print to the browser console using the standard `print_endline` function. This is probably the easiest method to debug right now.
 

src/haz3lcore/TyDi/ErrorPrint.re

@@ -30,7 +30,7 @@ module Print = {
     );
   };
 
-  let term = (term: Term.Any.t): string => {
+  let term = (term: Any.t): string => {
     let settings =
       ExpToSegment.Settings.of_core(~inline=false, CoreSettings.off);
     term |> ExpToSegment.any_to_pretty(~settings) |> seg(~holes="");
@@ -126,13 +126,52 @@ let typ_error: Info.error_typ => string =
     prn("Constructor %s already used in this sum", name)
   | WantLabel => "Expected a label"
   | ParseFailure => "Parse failure"
+  | InvalidLabel(name, labels) =>
+    prn(
+      "Label %s is not valid. Valid labels are: %s",
+      name,
+      String.concat(", ", labels),
+    )
   | DuplicateLabels(labels, ty) =>
     prn(
       "Duplicate labels in type %s: %s",
       Print.typ(ty),
       String.concat(", ", labels),
     )
-  | Duplicate(name, _) => prn("Type %s is already defined", name);
+  | Duplicate(name, _) => prn("Type %s is already defined", name)
+  | WantProduct(ty) =>
+    prn("Expected a tuple type, found type %s", Print.typ(ty));
+
+let underdetermined_typ: Info.underdetermined_typ => string =
+  fun
+  | ProdExtensionUnderdetermined(tys) =>
+    prn(
+      "Cannot determine type of tuple extension with argument types: %s",
+      List.map(Print.typ, tys) |> String.concat(", "),
+    )
+  | ProdProjectionMissingLabel(label, labels) =>
+    prn(
+      "Cannot project label %s. Valid labels are: %s",
+      label,
+      String.concat(", ", labels),
+    )
+  | ProdProjectionBadArgs({product, label}) =>
+    prn(
+      "Cannot determine projection type because %s",
+      String.concat(
+        " and ",
+        [
+          switch (product) {
+          | Some(ty) => "Type is not a tuple type: " ++ Print.typ(ty)
+          | None => ""
+          },
+          switch (label) {
+          | Some(ty) => "Label is not a valid label: " ++ Print.typ(ty)
+          | None => ""
+          },
+        ],
+      ),
+    );
 
 let tpat_error: Info.error_tpat => string =
   fun

src/haz3lcore/lang/Form.re

@@ -92,6 +92,7 @@ type atomic_form =
   | EmptyList
   | EmptyTuple
   | Deferral
+  | ExplicitNonlabel
   | TyVar
   | TyVarP
   | Ctr
@@ -148,6 +149,8 @@ type compound_form =
   | DotTyp
   | TypeAsc
   | TypPlus
+  | ProdProjection
+  | ProdExtension
   // UNARY PREFIX OPERATORS
   | Not
   | TypSumSingle
@@ -236,6 +239,8 @@ let get: compound_form => t =
   | TypeAsc => mk_infix(":", Exp, ~l=Exp, ~r=Typ, P.asc)
   | TupleExtension => mk_infix("...", Exp, P.plus)
   | TypPlus => mk_infix("+", Typ, P.type_plus)
+  | ProdProjection => mk_infix(".", Typ, P.dot)
+  | ProdExtension => mk_infix("...", Typ, P.ap)
   // UNARY PREFIX OPERATORS
   | Not => mk_prefix("!", Exp, P.not_)
   | TypSumSingle => mk_prefix("+", Typ, P.or_)
@@ -377,6 +382,7 @@ let get_atomic_form: atomic_form => (Token.t => bool, list(Mold.t)) =
   | EmptyList => (Token.is_empty_list, [op(Exp), op(Pat)])
   | EmptyTuple => (Token.is_empty_tuple, [op(Exp), op(Pat), op(Typ)])
   | Deferral => (Token.is_wild, [op(Exp)])
+  | ExplicitNonlabel => (Token.is_wild, [op(Typ)])
   | TyVar => (Token.is_typ_var, [op(Typ)])
   | TyVarP => (Token.is_typ_var, [op(TPat)])
   | Ctr => (Token.is_ctr, [op(Exp), op(Pat)])

src/haz3lcore/lang/MakeTerm.re

@@ -187,7 +187,7 @@ let mk_bad = (ctr, ids, value) => {
 let is_hole_label = (t: string) =>
   t == " " || Token.is_explicit_hole(t) || Token.is_llm_hole(t);
 
-let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t =>
+let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Any.t =>
   switch (s) {
   | Pat => Pat(pat(unsorted(Pat, skel, seg)))
   | TPat => TPat(tpat(unsorted(TPat, skel, seg)))
@@ -409,14 +409,13 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
         @ [r]
         |> List.map((child: Exp.t) => {
              switch (child) {
-             | {term: Tuple([{term: TupLabel(_) as tl, _}]), _} as tup =>
+             | {term: Tuple([{term: _ as tl, _}]), _} as tup =>
                // We use the Id for the tuple as the ids for the tuplabels
                let (_, rewrap) = IdTagged.unwrap(tup);
                rewrap(tl);
              | _ => child
              }
            });
-
       ret(Tuple(tuple_children));
     | None =>
       switch (tiles) {
@@ -454,6 +453,14 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
           | (["..."], []) => TupleExtension(l, r)
           | (["="], []) =>
             switch (l.term) {
+            | Deferral(_) =>
+              TupLabel(
+                {
+                  annotation: l.annotation,
+                  term: ExplicitNonlabel,
+                },
+                r,
+              ) // Unlabeled tuple using deferred ap in tuplabel
             | Var(name) =>
               TupLabel(
                 {
@@ -595,6 +602,16 @@ and pat_term: unsorted => (Pat.term, list(Id.t)) = {
       switch (tiles) {
       | ([(_id, (["="], []))], []) =>
         switch (l.term) {
+        | Wild =>
+          ret(
+            TupLabel(
+              {
+                annotation: l.annotation,
+                term: ExplicitNonlabel,
+              },
+              r,
+            ),
+          ) // Unlabeled tuple using deferred ap in tuplabel
         | Var(name) =>
           ret(
             TupLabel(
@@ -657,6 +674,7 @@ and typ_term: unsorted => (Typ.term, list(Id.t)) = {
         | (["Float"], []) => Atom(Float)
         | (["String"], []) => Atom(String)
         | (["Nat"], []) => Atom(Nat)
+        | (["_"], []) => ExplicitNonlabel
         | ([t], []) when Token.is_typ_var(t) => Var(t)
         | ([t], []) when Token.is_quoted_label(t) =>
           Label(Token.sub(t, 1, Token.length(t) - 2))
@@ -737,6 +755,21 @@ and typ_term: unsorted => (Typ.term, list(Id.t)) = {
           )
         | _ => ret(TupLabel(l, r))
         }
+      | ([(_id, (["."], []))], []) =>
+        switch (r.term) {
+        | Var(name) =>
+          ret(
+            ProdProjection(
+              l,
+              {
+                annotation: r.annotation,
+                term: Label(name),
+              },
+            ),
+          )
+        | _ => ret(ProdProjection(l, r))
+        }
+      | ([(_id, (["..."], []))], []) => ret(ProdExtension(l, r))
       | _ => ret(hole(tm))
       }
     }
@@ -808,7 +841,7 @@ and rul = (unsorted): Rul.t => {
 and unsorted = (sort: Sort.t, skel: Skel.t, seg: Segment.t): unsorted => {
   /* Remove projectors. We do this here as opposed to removing
    * them in an external call to save a whole-syntax pass. */
-  let tile_kids = (p: Piece.t): list(Term.Any.t) =>
+  let tile_kids = (p: Piece.t): list(Any.t) =>
     switch (p) {
     | Secondary(_)
     | Grout(_) => []