Merge branch 'haz3l-case-exhaustiveness' into haz3l-case-redundancy

src/haz3lcore/dynamics/DH.re

@@ -333,33 +333,25 @@ and ClosureEnvironment: {
 
   let to_list: t => list((Var.t, DHExp.t));
 
-  let of_environment:
-    (Environment.t, EnvironmentIdGen.t) => (t, EnvironmentIdGen.t);
+  let of_environment: Environment.t => t;
 
   let id_equal: (t, t) => bool;
 
-  let empty: EnvironmentIdGen.t => (t, EnvironmentIdGen.t);
+  let empty: t;
   let is_empty: t => bool;
   let length: t => int;
 
   let lookup: (t, Var.t) => option(DHExp.t);
   let contains: (t, Var.t) => bool;
-  let update:
-    (Environment.t => Environment.t, t, EnvironmentIdGen.t) =>
-    (t, EnvironmentIdGen.t);
+  let update: (Environment.t => Environment.t, t) => t;
   let update_keep_id: (Environment.t => Environment.t, t) => t;
-  let extend:
-    (t, (Var.t, DHExp.t), EnvironmentIdGen.t) => (t, EnvironmentIdGen.t);
+  let extend: (t, (Var.t, DHExp.t)) => t;
   let extend_keep_id: (t, (Var.t, DHExp.t)) => t;
-  let union: (t, t, EnvironmentIdGen.t) => (t, EnvironmentIdGen.t);
+  let union: (t, t) => t;
   let union_keep_id: (t, t) => t;
-  let map:
-    (((Var.t, DHExp.t)) => DHExp.t, t, EnvironmentIdGen.t) =>
-    (t, EnvironmentIdGen.t);
+  let map: (((Var.t, DHExp.t)) => DHExp.t, t) => t;
   let map_keep_id: (((Var.t, DHExp.t)) => DHExp.t, t) => t;
-  let filter:
-    (((Var.t, DHExp.t)) => bool, t, EnvironmentIdGen.t) =>
-    (t, EnvironmentIdGen.t);
+  let filter: (((Var.t, DHExp.t)) => bool, t) => t;
   let filter_keep_id: (((Var.t, DHExp.t)) => bool, t) => t;
   let fold: (((Var.t, DHExp.t), 'b) => 'b, 'b, t) => 'b;
 
@@ -386,9 +378,9 @@ and ClosureEnvironment: {
 
   let to_list = env => env |> map_of |> Environment.to_listo;
 
-  let of_environment = (map, eig) => {
-    let (ei, eig) = EnvironmentIdGen.next(eig);
-    (wrap(ei, map), eig);
+  let of_environment = map => {
+    let ei = Id.mk();
+    wrap(ei, map);
   };
 
   /* Equals only needs to check environment id's (faster than structural equality

src/haz3lcore/dynamics/Elaborator.re

@@ -206,14 +206,14 @@ let rec dhexp_of_uexp =
         let* dp = dhpat_of_upat(m, p);
         let* ddef = dhexp_of_uexp(m, def);
         let* dbody = dhexp_of_uexp(m, body);
-        let+ ty_body = fixed_exp_typ(m, body);
+        let+ ty = fixed_pat_typ(m, p);
         switch (Term.UPat.get_recursive_bindings(p)) {
         | None =>
           /* not recursive */
           DHExp.Let(dp, add_name(Term.UPat.get_var(p), ddef), dbody)
         | Some([f]) =>
           /* simple recursion */
-          Let(dp, FixF(f, ty_body, add_name(Some(f), ddef)), dbody)
+          Let(dp, FixF(f, ty, add_name(Some(f), ddef)), dbody)
         | Some(fs) =>
           /* mutual recursion */
           let ddef =
@@ -235,7 +235,7 @@ let rec dhexp_of_uexp =
                  },
                  (0, ddef),
                );
-          Let(dp, FixF(self_id, ty_body, substituted_def), dbody);
+          Let(dp, FixF(self_id, ty, substituted_def), dbody);
         };
       | Ap(fn, arg) =>
         let* c_fn = dhexp_of_uexp(m, fn);

src/haz3lcore/dynamics/EnvironmentId.re

@@ -1,10 +1 @@
-open Sexplib.Std;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = int;
-
-let init = 0;
-let equal = (==);
-
-let invalid = (-1);
-let is_invalid = equal(invalid);
+include Id;

src/haz3lcore/dynamics/EnvironmentId.rei

@@ -1,29 +1 @@
-/**
-  Identifier for environments.
- */
-
-/**
-  The type for identifiers.
- */
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = int;
-
-/**
-  [init] is the initial identifier.
- */
-let init: t;
-
-/**
-  [equal ei ei'] is true if and only if [ei] and [ei'] are equal.
- */
-let equal: (t, t) => bool;
-
-/**
-  [invalid] is an invalid identifier.
- */
-let invalid: t;
-
-/**
-  [is_invalid ei] is [equal invalid ei].
- */
-let is_invalid: t => bool;
+include (module type of Id);

src/haz3lcore/dynamics/EnvironmentIdMap.re

@@ -1 +1 @@
-include Util.IntMap;
+include Id.Map;

src/haz3lcore/dynamics/EnvironmentIdMap.rei

@@ -2,4 +2,4 @@
 
    Used in HoleInstanceInfo_.re
    */
-include (module type of Util.IntMap);
+include (module type of Id.Map);

src/haz3lcore/dynamics/Evaluator.re

@@ -662,13 +662,13 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
         | IndetMatch
         | DoesNotMatch => Indet(Closure(env, Let(dp, d1, d2))) |> return
         | Matches(env') =>
-          let* env = evaluate_extend_env(env', env);
+          let env = evaluate_extend_env(env', env);
           evaluate(env, d2);
         }
       };
 
     | FixF(f, _, d') =>
-      let* env' = evaluate_extend_env(Environment.singleton((f, d)), env);
+      let env' = evaluate_extend_env(Environment.singleton((f, d)), env);
       evaluate(env', d');
 
     | Fun(_) => BoxedValue(Closure(env, d)) |> return
@@ -694,7 +694,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
           | Matches(env') =>
             // evaluate a closure: extend the closure environment with the
             // new bindings introduced by the function application.
-            let* env = evaluate_extend_env(env', closure_env);
+            let env = evaluate_extend_env(env', closure_env);
             evaluate(env, d3);
           }
         };
@@ -1158,7 +1158,7 @@ and eval_rule =
       |> return;
     | Matches(env') =>
       // extend environment with new bindings introduced
-      let* env = evaluate_extend_env(env', env);
+      let env = evaluate_extend_env(env', env);
       evaluate(env, d);
     // by the rule and evaluate the expression.
     | DoesNotMatch =>
@@ -1172,10 +1172,11 @@ and eval_rule =
  */
 and evaluate_extend_env =
     (new_bindings: Environment.t, to_extend: ClosureEnvironment.t)
-    : m(ClosureEnvironment.t) => {
-  let map =
-    Environment.union(new_bindings, ClosureEnvironment.map_of(to_extend));
-  map |> ClosureEnvironment.of_environment |> with_eig;
+    : ClosureEnvironment.t => {
+  to_extend
+  |> ClosureEnvironment.map_of
+  |> Environment.union(new_bindings)
+  |> ClosureEnvironment.of_environment;
 }
 
 /**
@@ -1274,7 +1275,6 @@ and evaluate_test_eq =
 
 let evaluate = (env, d) => {
   let es = EvaluatorState.init;
-  let (env, es) =
-    es |> EvaluatorState.with_eig(ClosureEnvironment.of_environment(env));
+  let env = ClosureEnvironment.of_environment(env);
   evaluate(env, d, es);
 };

src/haz3lcore/dynamics/EvaluatorMonad.re

@@ -2,10 +2,6 @@ include Util.StateMonad.Make(EvaluatorState);
 
 open Syntax;
 
-let get_eig = get >>| EvaluatorState.get_eig;
-let put_eig = eig => modify(EvaluatorState.put_eig(eig));
-let with_eig = f => modify'(EvaluatorState.with_eig(f));
-
 let take_step = get >>= (state => put(EvaluatorState.take_step(state)));
 
 let add_test = (id, report) =>

src/haz3lcore/dynamics/EvaluatorMonad.rei

@@ -4,21 +4,6 @@
 
 include Util.StateMonad.S with type state = EvaluatorState.t;
 
-/**
-  See {!val:EvaluatorState.get_eig}.
- */
-let get_eig: t(EnvironmentIdGen.t);
-
-/**
-  See {!val:EvaluatorState.put_eig}.
- */
-let put_eig: EnvironmentIdGen.t => t(unit);
-
-/**
-  See {!val:EvaluatorState.with_eig}.
- */
-let with_eig: (EnvironmentIdGen.t => ('a, EnvironmentIdGen.t)) => t('a);
-
 /**
   See {!val:EvaluatorState.take_step}
  */

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -1,31 +1,19 @@
 module PpMonad = {
   include Util.StateMonad.Make({
     [@deriving sexp]
-    type t = (
-      EnvironmentIdMap.t(ClosureEnvironment.t),
-      HoleInstanceInfo_.t,
-      EnvironmentIdGen.t,
-    );
+    type t = (EnvironmentIdMap.t(ClosureEnvironment.t), HoleInstanceInfo_.t);
   });
 
   open Syntax;
 
-  let get_pe = get >>| (((pe, _, _)) => pe);
+  let get_pe = get >>| (((pe, _)) => pe);
   let pe_add = (ei, env) =>
-    modify(((pe, hii, eig)) =>
-      (pe |> EnvironmentIdMap.add(ei, env), hii, eig)
-    );
+    modify(((pe, hii)) => (pe |> EnvironmentIdMap.add(ei, env), hii));
 
   let hii_add_instance = (u, env) =>
-    modify'(((pe, hii, eig)) => {
+    modify'(((pe, hii)) => {
       let (hii, i) = HoleInstanceInfo_.add_instance(hii, u, env);
-      (i, (pe, hii, eig));
-    });
-
-  let with_eig = f =>
-    modify'(((pe, hii, eig)) => {
-      let (x, eig) = f(eig);
-      (x, (pe, hii, eig));
+      (i, (pe, hii));
     });
 };
 
@@ -242,7 +230,7 @@ and pp_eval_env = (env: ClosureEnvironment.t): m(ClosureEnvironment.t) => {
                  FixF(f, ty, d1);
                | d => pp_eval(d)
                };
-             with_eig(ClosureEnvironment.extend(env', (x, d')));
+             ClosureEnvironment.extend(env', (x, d')) |> return;
            },
            Environment.empty |> ClosureEnvironment.wrap(ei) |> return,
          );
@@ -551,13 +539,11 @@ let track_children = (hii: HoleInstanceInfo.t): HoleInstanceInfo.t =>
     hii,
   );
 
-let postprocess =
-    (d: DHExp.t, eig: EnvironmentIdGen.t)
-    : ((HoleInstanceInfo.t, DHExp.t), EnvironmentIdGen.t) => {
+let postprocess = (d: DHExp.t): (HoleInstanceInfo.t, DHExp.t) => {
   /* Substitution and hole numbering postprocessing */
-  let ((_, hii, eig), d) =
+  let ((_, hii), d) =
     Util.TimeUtil.measure_time("pp_eval", true, () =>
-      pp_eval(d, (EnvironmentIdMap.empty, HoleInstanceInfo_.empty, eig))
+      pp_eval(d, (EnvironmentIdMap.empty, HoleInstanceInfo_.empty))
     );
 
   /* Build hole instance info. */
@@ -591,5 +577,5 @@ let postprocess =
     );
 
   /* Perform hole parent tracking. */
-  ((hii, d), eig);
+  (hii, d);
 };

src/haz3lcore/dynamics/EvaluatorPost.rei

@@ -68,6 +68,4 @@ exception Exception(error);
 
   See also HoleInstanceInfo.rei/HoleInstanceInfo_.rei.
  */
-let postprocess:
-  (DHExp.t, EnvironmentIdGen.t) =>
-  ((HoleInstanceInfo.t, DHExp.t), EnvironmentIdGen.t);
+let postprocess: DHExp.t => (HoleInstanceInfo.t, DHExp.t);

src/haz3lcore/dynamics/EvaluatorState.re

@@ -1,22 +1,10 @@
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t = {
-  eig: EnvironmentIdGen.t,
   stats: EvaluatorStats.t,
   tests: TestMap.t,
 };
 
-let init = {
-  eig: EnvironmentIdGen.init,
-  stats: EvaluatorStats.initial,
-  tests: TestMap.empty,
-};
-
-let get_eig = ({eig, _}) => eig;
-let put_eig = (eig, es) => {...es, eig};
-let with_eig = (f, es) => {
-  let (x, eig) = es |> get_eig |> f;
-  (x, es |> put_eig(eig));
-};
+let init = {stats: EvaluatorStats.initial, tests: TestMap.empty};
 
 let take_step = ({stats, _} as es) => {
   ...es,

src/haz3lcore/dynamics/EvaluatorState.rei

@@ -16,22 +16,6 @@ type t;
  */
 let init: t;
 
-/**
-  [get_eig es] is current environment id generator.
- */
-let get_eig: t => EnvironmentIdGen.t;
-
-/**
-  [put_eig eig es] is [es] with the environment id generator [eig].
- */
-let put_eig: (EnvironmentIdGen.t, t) => t;
-
-/**
-  [with_eig f es] calls [f] with the current environment id generator, updating
-  [es] afterwards.
- */
-let with_eig: (EnvironmentIdGen.t => ('a, EnvironmentIdGen.t), t) => ('a, t);
-
 /**
   [take_step es] is [es] with the updated step count.
  */