Merge branch 'haz3l-case-redundancy' into haz3l-case-advanced-ui

src/haz3lcore/dynamics/Constraint.re

@@ -16,56 +16,18 @@ type t =
   | InjL(t)
   | InjR(t)
   | Pair(t, t);
-// | Tuple(list(t));
-
-// Unused
-let rec constrains = (c: t, ty: Typ.t): bool =>
-  switch (c, Typ.weak_head_normalize(Builtins.ctx_init, ty)) {
-  | (Truth, _)
-  | (Falsity, _)
-  | (Hole, _) => true
-  | (Int(_) | NotInt(_), Int) => true
-  | (Int(_) | NotInt(_), _) => false
-  | (Float(_) | NotFloat(_), Float) => true
-  | (Float(_) | NotFloat(_), _) => false
-  | (String(_) | NotString(_), String) => true
-  | (String(_) | NotString(_), _) => false
-  | (And(c1, c2), _) => constrains(c1, ty) && constrains(c2, ty)
-  | (Or(c1, c2), _) => constrains(c1, ty) && constrains(c2, ty)
-  // Treates sum as if it is left associative
-  | (InjL(c1), Sum(map)) =>
-    switch (List.hd(map)) {
-    | (_, Some(ty1)) => constrains(c1, ty1)
-    | _ => false
-    }
-  | (InjL(_), _) => false
-  | (InjR(c2), Sum(map)) =>
-    switch (List.tl(map)) {
-    | [] => false
-    | [(_, Some(ty2))] => constrains(c2, ty2)
-    | map' => constrains(c2, Sum(map'))
-    }
-  | (InjR(_), _) => false
-  | (Pair(c1, c2), Prod([ty_hd, ...ty_tl])) =>
-    constrains(c1, ty_hd) && constrains(c2, Prod(ty_tl))
-  | (Pair(_), _) => false
-  // | (Tuple(cs), Prod(tys)) when List.length(cs) == List.length(tys) =>
-  //   List.for_all2(constrains, cs, tys)
-  // | (Tuple(_), _) => false
-  };
 
 let rec dual = (c: t): t =>
   switch (c) {
   | Truth => Falsity
   | Falsity => Truth
-  // The complement of an indeterministic set is still indeterministic
   | Hole => Hole
   | Int(n) => NotInt(n)
   | NotInt(n) => Int(n)
   | Float(n) => NotFloat(n)
   | NotFloat(n) => Float(n)
-  | String(n) => NotString(n)
-  | NotString(n) => String(n)
+  | String(s) => NotString(s)
+  | NotString(s) => String(s)
   | And(c1, c2) => Or(dual(c1), dual(c2))
   | Or(c1, c2) => And(dual(c1), dual(c2))
   | InjL(c1) => Or(InjL(dual(c1)), InjR(Truth))
@@ -75,7 +37,6 @@ let rec dual = (c: t): t =>
       Pair(c1, dual(c2)),
       Or(Pair(dual(c1), c2), Pair(dual(c1), dual(c2))),
     )
-  // | Tuple(cs) => // TODO
   };
 
 /** substitute Truth for Hole */
@@ -116,13 +77,12 @@ let rec falsify = (c: t): t =>
   | Pair(c1, c2) => Pair(falsify(c1), falsify(c2))
   };
 
-// temporary name
-let is_inl =
+let is_injL =
   fun
   | InjL(_) => true
   | _ => false;
 
-let is_inr =
+let is_injR =
   fun
   | InjR(_) => true
   | _ => false;

src/haz3lcore/dynamics/Elaborator.re

@@ -238,7 +238,8 @@ let rec dhexp_of_uexp =
                );
           Let(dp, FixF(self_id, ty, substituted_def), dbody);
         };
-      | Ap(fn, arg) =>
+      | Ap(fn, arg)
+      | Pipeline(arg, fn) =>
         let* c_fn = dhexp_of_uexp(m, fn);
         let+ c_arg = dhexp_of_uexp(m, arg);
         DHExp.Ap(c_fn, c_arg);

src/haz3lcore/dynamics/Incon.re

@@ -37,8 +37,8 @@ let is_inconsistent_string = (xis: list(Constraint.t)): bool => {
     List.fold_left(
       ((string_set, not_string_list), xi: Constraint.t) =>
         switch (xi) {
-        | String(n) => (StringSet.add(n, string_set), not_string_list)
-        | NotString(n) => (string_set, [n, ...not_string_list])
+        | String(s) => (StringSet.add(s, string_set), not_string_list)
+        | NotString(s) => (string_set, [s, ...not_string_list])
         | _ => failwith("input can only be String | NotString")
         },
       (StringSet.empty, []),
@@ -53,8 +53,8 @@ let rec is_inconsistent = (xis: list(Constraint.t)): bool =>
   | [] => false
   | _
       when
-        List.exists(Constraint.is_inl, xis)
-        && List.exists(Constraint.is_inr, xis) =>
+        List.exists(Constraint.is_injL, xis)
+        && List.exists(Constraint.is_injR, xis) =>
     true
   | [xi, ...xis'] =>
     switch (xi) {
@@ -65,13 +65,13 @@ let rec is_inconsistent = (xis: list(Constraint.t)): bool =>
     | Or(xi1, xi2) =>
       is_inconsistent([xi1, ...xis']) && is_inconsistent([xi2, ...xis'])
     | InjL(_) =>
-      switch (List.partition(Constraint.is_inl, xis)) {
+      switch (List.partition(Constraint.is_injL, xis)) {
       | (injLs, []) =>
         injLs |> List.map(Constraint.unwrapL) |> is_inconsistent
       | (injLs, others) => is_inconsistent(others @ injLs)
       }
     | InjR(_) =>
-      switch (List.partition(Constraint.is_inr, xis)) {
+      switch (List.partition(Constraint.is_injR, xis)) {
       | (injRs, []) =>
         injRs |> List.map(Constraint.unwrapR) |> is_inconsistent
       | (injRs, others) => is_inconsistent(others @ injRs)

src/haz3lcore/lang/Form.re

@@ -242,13 +242,15 @@ let forms: list((string, t)) = [
   ("logical_and", mk_infix("&&", Exp, P.and_)),
   //("bitwise_or", mk_infix("|", Exp, 5)),
   ("logical_or_", mk_nul_infix("\\", P.eqs)), // HACK: SUBSTRING REQ
-  ("logical_or", mk_infix("\\/", Exp, P.or_)),
+  ("logical_or", mk_infix("||", Exp, P.or_)),
   ("dot", mk(ss, ["."], mk_op(Any, []))), // HACK: SUBSTRING REQ (floats)
   ("unary_minus", mk(ss, ["-"], mk_pre(P.neg, Exp, []))),
   ("comma_exp", mk_infix(",", Exp, P.prod)),
   ("comma_pat", mk_infix(",", Pat, P.prod)),
   ("comma_typ", mk_infix(",", Typ, P.prod)),
   ("type-arrow", mk_infix("->", Typ, 6)),
+  ("pipeline_aux", mk_infix("|", Exp, P.eqs)), // hack (all Hazel ops have to be valid, even when in a partial state)
+  ("pipeline", mk_infix("|>", Exp, P.eqs)), // in OCaml, pipeline precedence is in same class as '=', '<', etc.
   ("parens_exp", mk(ii, ["(", ")"], mk_op(Exp, [Exp]))),
   ("parens_pat", mk(ii, ["(", ")"], mk_op(Pat, [Pat]))),
   ("parens_typ", mk(ii, ["(", ")"], mk_op(Typ, [Typ]))),
@@ -267,7 +269,7 @@ let forms: list((string, t)) = [
   (
     "rule",
     mk(
-      ii,
+      di,
       ["|", "=>"],
       {
         out: Rul,

src/haz3lcore/statics/MakeTerm.re

@@ -233,11 +233,12 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           | (["==."], []) => BinOp(Float(Equals), l, r)
           | (["!=."], []) => BinOp(Float(NotEquals), l, r)
           | (["&&"], []) => BinOp(Bool(And), l, r)
-          | (["\\/"], []) => BinOp(Bool(Or), l, r)
+          | (["||"], []) => BinOp(Bool(Or), l, r)
           | (["::"], []) => Cons(l, r)
           | ([";"], []) => Seq(l, r)
           | (["++"], []) => BinOp(String(Concat), l, r)
           | (["$=="], []) => BinOp(String(Equals), l, r)
+          | (["|>"], []) => Pipeline(l, r)
           | (["@"], []) => ListConcat(l, r)
           | _ => hole(tm)
           },

src/haz3lcore/statics/Statics.re

@@ -226,7 +226,8 @@ and uexp_to_info_map =
     let (e2, m) = go(~mode, e2, m);
     add(~self=Just(e2.ty), ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]), m);
   | Constructor(ctr) => atomic(Self.of_ctr(ctx, ctr))
-  | Ap(fn, arg) =>
+  | Ap(fn, arg)
+  | Pipeline(arg, fn) =>
     let fn_mode = Mode.of_ap(ctx, mode, UExp.ctr_name(fn));
     let (fn, m) = go(~mode=fn_mode, fn, m);
     let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);

src/haz3lcore/statics/Term.re

@@ -436,6 +436,7 @@ module UExp = {
     | Let
     | TyAlias
     | Ap
+    | Pipeline
     | If
     | Seq
     | Test
@@ -475,6 +476,7 @@ module UExp = {
     | Let(_) => Let
     | TyAlias(_) => TyAlias
     | Ap(_) => Ap
+    | Pipeline(_) => Pipeline
     | If(_) => If
     | Seq(_) => Seq
     | Test(_) => Test
@@ -561,6 +563,7 @@ module UExp = {
     | Let => "Let expression"
     | TyAlias => "Type Alias definition"
     | Ap => "Application"
+    | Pipeline => "Pipeline expression"
     | If => "If expression"
     | Seq => "Sequence expression"
     | Test => "Test"
@@ -589,6 +592,7 @@ module UExp = {
     | Let(_)
     | TyAlias(_)
     | Ap(_)
+    | Pipeline(_)
     | If(_)
     | Seq(_)
     | Test(_)
@@ -621,6 +625,7 @@ module UExp = {
       | Let(_)
       | TyAlias(_)
       | Ap(_)
+      | Pipeline(_)
       | If(_)
       | Seq(_)
       | Test(_)

src/haz3lcore/statics/TermBase.re

@@ -115,6 +115,7 @@ and UExp: {
     | Let(UPat.t, t, t)
     | TyAlias(UTPat.t, UTyp.t, t)
     | Ap(t, t)
+    | Pipeline(t, t)
     | If(t, t, t)
     | Seq(t, t)
     | Test(t)
@@ -211,6 +212,7 @@ and UExp: {
     | Let(UPat.t, t, t)
     | TyAlias(UTPat.t, UTyp.t, t)
     | Ap(t, t)
+    | Pipeline(t, t)
     | If(t, t, t)
     | Seq(t, t)
     | Test(t)
@@ -229,7 +231,7 @@ and UExp: {
   let bool_op_to_string = (op: op_bin_bool): string => {
     switch (op) {
     | And => "&&"
-    | Or => "\\/"
+    | Or => "||"
     };
   };
 

src/haz3lcore/zipper/EditorUtil.re

@@ -68,6 +68,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Tuple(_)
   | Var(_)
   | Ap(_)
+  | Pipeline(_)
   | If(_)
   | Test(_)
   | Parens(_)

src/haz3lweb/LangDocMessages.re

@@ -92,6 +92,7 @@ let logical_or = () => Example.mk_monotile(Form.get("logical_or"));
 let comma_exp = () => Example.mk_monotile(Form.get("comma_exp"));
 let comma_pat = () => Example.mk_monotile(Form.get("comma_pat"));
 let comma_typ = () => Example.mk_monotile(Form.get("comma_typ"));
+let pipeline = () => Example.mk_monotile(Form.get("pipeline"));
 let nil = () => exp("[]");
 let typeann = () => Example.mk_monotile(Form.get("typeann"));
 let mk_fun = Example.mk_tile(Form.get("fun_"));
@@ -1587,6 +1588,34 @@ let conapp_exp: form = {
   };
 };
 
+let pipeline_exp_group = "pipeline_exp_group";
+let pipeline_exp_ex = {
+  sub_id: "pipeline_exp_ex",
+  term: mk_example("1 |> fun x -> x + 1"),
+  message: "The argument 1 is passed to an increment function, and the entire expression evaluates to 2. The pipeline operator is useful for chaining functions together.",
+  feedback: Unselected,
+};
+let _exp_arg = exp("e_arg");
+let _exp_fun = exp("e_fun");
+let pipeline_exp_coloring_ids =
+    (~arg_id: Id.t, ~fn_id: Id.t): list((Id.t, Id.t)) => [
+  (Piece.id(_exp_arg), arg_id),
+  (Piece.id(_exp_fun), fn_id),
+];
+let pipeline_exp: form = {
+  let explanation = {
+    message: "Pipeline operator. Pass the [*argument*](%i) to the [*function*](%i).",
+    feedback: Unselected,
+  };
+  {
+    id: "pipeline_exp",
+    syntactic_form: [_exp_arg, space(), pipeline(), space(), _exp_fun],
+    expandable_id: None,
+    explanation,
+    examples: [pipeline_exp_ex],
+  };
+};
+
 let if_exp_group = "if_exp_group";
 let if_basic1_exp_ex = {
   sub_id: "if_basic1_exp_ex",
@@ -2003,13 +2032,13 @@ let bool_and2_ex = {
 };
 let bool_or1_ex = {
   sub_id: "bool_or1_ex",
-  term: mk_example("false \\/ 2 < 1"),
+  term: mk_example("false || 2 < 1"),
   message: "The left operand evaluates to false, so evaluate the right operand. Since the right operand also evaluates to false, the whole expression evaluates to false.",
   feedback: Unselected,
 };
 let bool_or2_ex = {
   sub_id: "bool_or2_ex",
-  term: mk_example("3 < 4 \\/ false"),
+  term: mk_example("3 < 4 || false"),
   message: "The left operand evalutes to true, so the right operand is not evaluated. The whole expression evaluates to true.",
   feedback: Unselected,
 };
@@ -3521,6 +3550,7 @@ let init = {
     tyalias_base_exp,
     funapp_exp,
     conapp_exp,
+    pipeline_exp,
     if_exp,
     seq_exp,
     test_exp,
@@ -3887,6 +3917,7 @@ let init = {
     (funapp_exp_group, init_options([(funapp_exp.id, [])])),
     (conapp_exp_group, init_options([(conapp_exp.id, [])])),
     (if_exp_group, init_options([(if_exp.id, [])])),
+    (pipeline_exp_group, init_options([(pipeline_exp.id, [])])),
     (seq_exp_group, init_options([(seq_exp.id, [])])),
     (test_group, init_options([(test_exp.id, [])])),
     (cons_exp_group, init_options([(cons_exp.id, [])])),

src/haz3lweb/view/LangDoc.re

@@ -1907,6 +1907,25 @@ let get_doc =
             LangDocMessages.funapp_exp_coloring_ids,
           );
         };
+      | Pipeline(arg, fn) =>
+        let (doc, options) =
+          LangDocMessages.get_form_and_options(
+            LangDocMessages.pipeline_exp_group,
+            docs,
+          );
+        let arg_id = List.nth(arg.ids, 0);
+        let fn_id = List.nth(fn.ids, 0);
+        get_message(
+          doc,
+          options,
+          LangDocMessages.pipeline_exp_group,
+          Printf.sprintf(
+            Scanf.format_from_string(doc.explanation.message, "%s%s"),
+            arg_id |> Id.to_string,
+            fn_id |> Id.to_string,
+          ),
+          LangDocMessages.pipeline_exp_coloring_ids(~arg_id, ~fn_id),
+        );
       | If(cond, then_, else_) =>
         let (doc, options) =
           LangDocMessages.get_form_and_options(