Case expression exhaustiveness & redundancy checking

src/haz3lcore/dynamics/Constraint.re

@@ -0,0 +1,153 @@
+open Sexplib.Std;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t =
+  | Truth
+  | Falsity
+  | Hole
+  | Int(int)
+  | NotInt(int)
+  | Float(float)
+  | NotFloat(float)
+  | String(string)
+  | NotString(string)
+  | And(t, t)
+  | Or(t, t)
+  | InjL(t)
+  | InjR(t)
+  | Pair(t, t);
+
+let rec dual = (c: t): t =>
+  switch (c) {
+  | Truth => Falsity
+  | Falsity => Truth
+  | Hole => Hole
+  | Int(n) => NotInt(n)
+  | NotInt(n) => Int(n)
+  | Float(n) => NotFloat(n)
+  | NotFloat(n) => Float(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))
+  | InjR(c2) => Or(InjR(dual(c2)), InjL(Truth))
+  | Pair(c1, c2) =>
+    Or(
+      Pair(c1, dual(c2)),
+      Or(Pair(dual(c1), c2), Pair(dual(c1), dual(c2))),
+    )
+  };
+
+/** substitute Truth for Hole */
+let rec truify = (c: t): t =>
+  switch (c) {
+  | Hole => Truth
+  | Truth
+  | Falsity
+  | Int(_)
+  | NotInt(_)
+  | Float(_)
+  | NotFloat(_)
+  | String(_)
+  | NotString(_) => c
+  | And(c1, c2) => And(truify(c1), truify(c2))
+  | Or(c1, c2) => Or(truify(c1), truify(c2))
+  | InjL(c) => InjL(truify(c))
+  | InjR(c) => InjR(truify(c))
+  | Pair(c1, c2) => Pair(truify(c1), truify(c2))
+  };
+
+/** substitute Falsity for Hole */
+let rec falsify = (c: t): t =>
+  switch (c) {
+  | Hole => Falsity
+  | Truth
+  | Falsity
+  | Int(_)
+  | NotInt(_)
+  | Float(_)
+  | NotFloat(_)
+  | String(_)
+  | NotString(_) => c
+  | And(c1, c2) => And(falsify(c1), falsify(c2))
+  | Or(c1, c2) => Or(falsify(c1), falsify(c2))
+  | InjL(c) => InjL(falsify(c))
+  | InjR(c) => InjR(falsify(c))
+  | Pair(c1, c2) => Pair(falsify(c1), falsify(c2))
+  };
+
+let is_injL =
+  fun
+  | InjL(_) => true
+  | _ => false;
+
+let is_injR =
+  fun
+  | InjR(_) => true
+  | _ => false;
+
+let unwrapL =
+  fun
+  | InjL(c) => c
+  | _ => failwith("input can only be InjL(_)");
+
+let unwrapR =
+  fun
+  | InjR(c) => c
+  | _ => failwith("input can only be InjR(_)");
+
+let unwrap_pair =
+  fun
+  | Pair(c1, c2) => (c1, c2)
+  | _ => failwith("input can only be pair(_, _)");
+
+let rec or_constraints = (lst: list(t)): t =>
+  switch (lst) {
+  | [] => Falsity
+  | [xi] => xi
+  | [xi, ...xis] => Or(xi, or_constraints(xis))
+  };
+
+let rec ctr_of_nth_variant = (num_variants, nth): (t => t) =>
+  if (num_variants == 1) {
+    Fun.id;
+  } else if (nth == 0) {
+    xi => InjL(xi);
+  } else {
+    xi => InjR(xi |> ctr_of_nth_variant(num_variants - 1, nth - 1));
+  };
+
+let of_ap = (ctx, mode, ctr: option(Constructor.t), arg: t, syn_ty): t =>
+  switch (ctr) {
+  | Some(name) =>
+    let ty =
+      switch (mode) {
+      | Mode.Ana(ty) => Some(ty)
+      | Syn => syn_ty
+      | _ => None
+      };
+    switch (ty) {
+    | Some(ty) =>
+      switch (Typ.weak_head_normalize(ctx, ty)) {
+      | Sum(map) =>
+        let num_variants = ConstructorMap.cardinal(map);
+        switch (ConstructorMap.nth(map, name)) {
+        | Some(nth) => arg |> ctr_of_nth_variant(num_variants, nth)
+        | None => Falsity
+        };
+      | _ => Falsity
+      }
+    | None => Falsity
+    };
+  | None => Falsity
+  };
+
+let of_ctr = (ctx, mode, name, self) => {
+  let syn_ty =
+    switch (self) {
+    | Self.IsConstructor({syn_ty, _}) => syn_ty
+    | _ => assert(false) // impossible
+    };
+  of_ap(ctx, mode, Some(name), Truth, syn_ty);
+};

src/haz3lcore/dynamics/Elaborator.re

@@ -376,7 +376,8 @@ let rec dhexp_of_uexp =
           |> OptUtil.sequence;
         let d = DHExp.Case(d_scrut, d_rules, 0);
         switch (err_status) {
-        | InHole(Common(Inconsistent(Internal(_)))) =>
+        | InHole(Common(Inconsistent(Internal(_))))
+        | InHole(InexhaustiveMatch(Some(Inconsistent(Internal(_))))) =>
           DHExp.InconsistentBranches(id, 0, d)
         | _ => ConsistentCase(d)
         };
@@ -393,6 +394,13 @@ let rec dhexp_of_uexp =
 and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
   switch (Id.Map.find_opt(Term.UPat.rep_id(upat), m)) {
   | Some(InfoPat({mode, self, ctx, _})) =>
+    // NOTE: for the current implementation, redundancy is considered a static error
+    // but not a runtime error.
+    let self =
+      switch (self) {
+      | Redundant(self) => self
+      | _ => self
+      };
     let err_status = Info.status_pat(ctx, mode, self);
     let maybe_reason: option(ErrStatus.HoleReason.t) =
       switch (err_status) {

src/haz3lcore/dynamics/Incon.re

@@ -0,0 +1,145 @@
+open Sets;
+
+let is_inconsistent_int = (xis: list(Constraint.t)): bool => {
+  let (int_set, not_int_list) =
+    List.fold_left(
+      ((int_set, not_int_list), xi: Constraint.t) =>
+        switch (xi) {
+        | Int(n) => (IntSet.add(n, int_set), not_int_list)
+        | NotInt(n) => (int_set, [n, ...not_int_list])
+        | _ => failwith("input can only be Int | NotInt")
+        },
+      (IntSet.empty, []),
+      xis,
+    );
+  IntSet.cardinal(int_set) > 1
+  || List.exists(IntSet.mem(_, int_set), not_int_list);
+};
+
+let is_inconsistent_float = (xis: list(Constraint.t)): bool => {
+  let (float_set, not_float_list) =
+    List.fold_left(
+      ((float_set, not_float_list), xi: Constraint.t) =>
+        switch (xi) {
+        | Float(n) => (FloatSet.add(n, float_set), not_float_list)
+        | NotFloat(n) => (float_set, [n, ...not_float_list])
+        | _ => failwith("input can only be Float | NotFloat")
+        },
+      (FloatSet.empty, []),
+      xis,
+    );
+  FloatSet.cardinal(float_set) > 1
+  || List.exists(FloatSet.mem(_, float_set), not_float_list);
+};
+
+let is_inconsistent_string = (xis: list(Constraint.t)): bool => {
+  let (string_set, not_string_list) =
+    List.fold_left(
+      ((string_set, not_string_list), xi: Constraint.t) =>
+        switch (xi) {
+        | 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, []),
+      xis,
+    );
+  StringSet.cardinal(string_set) > 1
+  || List.exists(StringSet.mem(_, string_set), not_string_list);
+};
+
+let rec is_inconsistent = (xis: list(Constraint.t)): bool =>
+  switch (xis) {
+  | [] => false
+  | _
+      when
+        List.exists(Constraint.is_injL, xis)
+        && List.exists(Constraint.is_injR, xis) =>
+    true
+  | [xi, ...xis'] =>
+    switch (xi) {
+    | Truth => is_inconsistent(xis')
+    | Falsity => true
+    | Hole => assert(false) // Impossible
+    | And(xi1, xi2) => is_inconsistent([xi1, xi2, ...xis'])
+    | Or(xi1, xi2) =>
+      is_inconsistent([xi1, ...xis']) && is_inconsistent([xi2, ...xis'])
+    | InjL(_) =>
+      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_injR, xis)) {
+      | (injRs, []) =>
+        injRs |> List.map(Constraint.unwrapR) |> is_inconsistent
+      | (injRs, others) => is_inconsistent(others @ injRs)
+      }
+    | Int(_)
+    | NotInt(_) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.Int(_)
+          | NotInt(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (ns, []) => is_inconsistent_int(ns)
+      | (ns, others) => is_inconsistent(others @ ns)
+      }
+    | Float(_)
+    | NotFloat(_) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.Float(_)
+          | NotFloat(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (fs, []) => is_inconsistent_float(fs)
+      | (fs, others) => is_inconsistent(others @ fs)
+      }
+    | String(_)
+    | NotString(_) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.String(_)
+          | NotString(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (ss, []) => is_inconsistent_string(ss)
+      | (ss, others) => is_inconsistent(others @ ss)
+      }
+    | Pair(_, _) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.Pair(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (pairs, []) =>
+        let (xisL, xisR) =
+          pairs |> List.map(Constraint.unwrap_pair) |> List.split;
+        is_inconsistent(xisL) || is_inconsistent(xisR);
+      | (pairs, others) => is_inconsistent(others @ pairs)
+      }
+    }
+  };
+
+let is_redundant = (xi_cur: Constraint.t, xi_pre: Constraint.t): bool =>
+  is_inconsistent(
+    Constraint.[And(truify(xi_cur), dual(falsify(xi_pre)))],
+  );
+
+let is_exhaustive = (xi: Constraint.t): bool =>
+  is_inconsistent(Constraint.[dual(truify(xi))]);

src/haz3lcore/dynamics/Sets.re

@@ -0,0 +1,23 @@
+module IntSet =
+  Set.Make({
+    type t = int;
+    let compare = compare;
+  });
+
+module BoolSet =
+  Set.Make({
+    type t = bool;
+    let compare = compare;
+  });
+
+module FloatSet =
+  Set.Make({
+    type t = float;
+    let compare = compare;
+  });
+
+module StringSet =
+  Set.Make({
+    type t = string;
+    let compare = compare;
+  });

src/haz3lcore/statics/ConstructorMap.re

@@ -99,3 +99,12 @@ let rec is_ground = (is_ground_value: 'a => bool, map: t('a)): bool =>
   | [(_, head), ...tail] =>
     is_ground_value(head) && tail |> is_ground(is_ground_value)
   };
+
+let nth = (map: t('a), ctr: Constructor.t): option(int) => {
+  // TODO: use List.find_index instead, which is available for OCaml 5.1
+  let ctrs_sorted = map |> sort |> ctrs_of;
+  List.find_opt(
+    nth => List.nth(ctrs_sorted, nth) == ctr,
+    List.init(List.length(ctrs_sorted), Fun.id),
+  );
+};