Merge branch 'dev' into parameterized_types

src/haz3lcore/dynamics/Elaborator.re

@@ -254,13 +254,13 @@ let rec dhexp_of_uexp =
           DHExp.Let(dp, add_name(Term.UPat.get_var(p), ddef), dbody)
         | Some([f]) =>
           /* simple recursion */
-          Let(dp, FixF(f, ty, add_name(Some(f), ddef)), dbody)
+          Let(dp, FixF(f, ty, add_name(Some(f ++ "+"), ddef)), dbody)
         | Some(fs) =>
           /* mutual recursion */
           let ddef =
             switch (ddef) {
             | Tuple(a) =>
-              DHExp.Tuple(List.map2(s => add_name(Some(s)), fs, a))
+              DHExp.Tuple(List.map2(s => add_name(Some(s ++ "+")), fs, a))
             | _ => ddef
             };
           let uniq_id = List.nth(def.ids, 0);

src/haz3lcore/dynamics/Stepper.re

@@ -417,6 +417,7 @@ let get_justification: step_kind => string =
   | VarLookup => "variable lookup"
   | CastAp
   | Cast => "cast calculus"
+  | FixClosure => "fixpoint closure"
   | CompleteFilter => "complete filter"
   | CompleteClosure => "complete closure"
   | FunClosure => "function closure"

src/haz3lcore/dynamics/Transition.re

@@ -52,6 +52,7 @@ type step_kind =
   | LetBind
   | FunClosure
   | FixUnwrap
+  | FixClosure
   | UpdateTest
   | TypFunAp
   | FunAp
@@ -230,15 +231,15 @@ module Transition = (EV: EV_MODE) => {
         kind: FunClosure,
         value: true,
       });
+    | FixF(f, _, Closure(env, d1)) =>
+      let. _ = otherwise(env, d);
+      let env' = evaluate_extend_env(Environment.singleton((f, d)), env);
+      Step({apply: () => Closure(env', d1), kind: FixUnwrap, value: false});
     | FixF(f, t, d1) =>
       let. _ = otherwise(env, FixF(f, t, d1));
       Step({
-        apply: () =>
-          Closure(
-            evaluate_extend_env(Environment.singleton((f, d1)), env),
-            d1,
-          ),
-        kind: FixUnwrap,
+        apply: () => FixF(f, t, Closure(env, d1)),
+        kind: FixClosure,
         value: false,
       });
     | Test(id, d) =>
@@ -716,9 +717,10 @@ let should_hide_step = (~settings: CoreSettings.Evaluation.t) =>
   | VarLookup => !settings.show_lookup_steps
   | CastAp
   | Cast => !settings.show_casts
+  | FixUnwrap => !settings.show_fixpoints
   | CaseNext
   | CompleteClosure
   | CompleteFilter
-  | FixUnwrap
   | BuiltinWrap
-  | FunClosure => true;
+  | FunClosure
+  | FixClosure => true;

src/haz3lcore/statics/TypBase.re

@@ -347,7 +347,7 @@ module rec Typ: {
     | (Unknown(p1), Unknown(p2)) =>
       Some(Unknown(join_type_provenance(p1, p2)))
     | (Unknown(_), ty)
-    | (ty, Unknown(Internal | SynSwitch)) => Some(ty)
+    | (ty, Unknown(_)) => Some(ty)
     | (Var(n1), Var(n2)) =>
       if (n1 == n2) {
         Some(Var(n1));

src/haz3lweb/explainthis/data/FunctionExp.re

@@ -254,7 +254,7 @@ let _exp = exp("e");
 let function_listlit_exp_coloring_ids =
   _pat_body_function_exp_coloring_ids(Piece.id(_pat), Piece.id(_exp));
 let function_listlit_exp: form = {
-  let explanation = "The only values that match the [*argument pattern*](%s) are lists with %n-elements, each matching the corresponding element pattern. When applied to an argument which matches the [*argument pattern*](%s), evaluates to the function [*body*](%s).";
+  let explanation = "The only values that match the [*argument pattern*](%s) are lists with %s-elements, each matching the corresponding element pattern. When applied to an argument which matches the [*argument pattern*](%s), evaluates to the function [*body*](%s).";
   let form = [mk_fun([[space(), _pat, space()]]), space(), _exp];
   {
     id: FunctionExp(ListLit),

src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re

@@ -126,7 +126,6 @@ let mk =
             chosen_step: option(step),
             next_steps: list((EvalCtx.t, int)),
             recent_subst: list(Var.t),
-            recursive_calls: list(Var.t),
           )
           : DHDoc.t => {
     open Doc;
@@ -138,12 +137,14 @@ let mk =
         | (FunAp, _) => []
         | (LetBind, Let(p, _, _)) => DHPat.bound_vars(p)
         | (LetBind, _) => []
-        | (FixUnwrap, _) // TODO[Matt]: Could do something here?
-        | (TypFunAp, _) // TODO: Could also do something here for type variable substitution?
+        | (FixUnwrap, FixF(f, _, _)) => [f]
+        | (FixUnwrap, _) => []
+        | (TypFunAp, _)
         | (InvalidStep, _)
         | (VarLookup, _)
         | (Sequence, _)
         | (FunClosure, _)
+        | (FixClosure, _)
         | (UpdateTest, _)
         | (CastAp, _)
         | (BuiltinWrap, _)
@@ -165,12 +166,24 @@ let mk =
         }
       | _ => recent_subst
       };
+    let substitution =
+      hidden_steps
+      |> List.find_opt(step =>
+           step.knd == VarLookup
+           // HACK[Matt]: to prevent substitutions hiding inside casts
+           && EvalCtx.fuzzy_mark(step.ctx)
+         );
+    let next_recent_subst =
+      switch (substitution) {
+      | Some({d_loc: BoundVar(v), _}) =>
+        List.filter(u => u != v, recent_subst)
+      | _ => recent_subst
+      };
     let go' =
         (
           ~env=env,
           ~enforce_inline=enforce_inline,
-          ~recent_subst=recent_subst,
-          ~recursive_calls=recursive_calls,
+          ~recent_subst=next_recent_subst,
           d,
           ctx,
         ) => {
@@ -194,7 +207,6 @@ let mk =
           next_steps,
         ),
         recent_subst,
-        recursive_calls,
       );
     };
     let parenthesize = (b, doc) =>
@@ -271,6 +283,8 @@ let mk =
     );
     let doc = {
       switch (d) {
+      | TypFun(_tpat, _dbody) =>
+        annot(DHAnnot.Collapsed, text("<anon typfn>"))
       | Closure(env', d') => go'(d', Closure, ~env=env')
       | Filter(flt, d') =>
         if (settings.show_stepper_filters) {
@@ -321,7 +335,6 @@ let mk =
       | InconsistentBranches(u, i, Case(dscrut, drs, _)) =>
         go_case(dscrut, drs, false)
         |> annot(DHAnnot.InconsistentBranches((u, i)))
-      | BoundVar(x) when List.mem(x, recursive_calls) => text(x)
       | BoundVar(x) when settings.show_lookup_steps => text(x)
       | BoundVar(x) =>
         switch (ClosureEnvironment.lookup(env, x)) {
@@ -331,7 +344,12 @@ let mk =
             hcats([
               go'(~env=ClosureEnvironment.empty, BoundVar(x), BoundVar)
               |> annot(DHAnnot.Substituted),
-              go'(~env=ClosureEnvironment.empty, d', BoundVar),
+              go'(
+                ~env=ClosureEnvironment.empty,
+                ~recent_subst=List.filter(u => u != x, next_recent_subst),
+                d',
+                BoundVar,
+              ),
             ]);
           } else {
             go'(~env=ClosureEnvironment.empty, d', BoundVar);
@@ -465,7 +483,7 @@ let mk =
               ~enforce_inline=false,
               ~env=ClosureEnvironment.without_keys(bindings, env),
               ~recent_subst=
-                List.filter(x => !List.mem(x, bindings), recent_subst),
+                List.filter(x => !List.mem(x, bindings), next_recent_subst),
               dbody,
               Let2,
             ),
@@ -520,101 +538,70 @@ let mk =
              ),
           DHDoc_common.Delim.mk(")"),
         ]);
-      | Fun(dp, ty, Closure(env', d), s) =>
-        if (settings.show_fn_bodies) {
-          let bindings = DHPat.bound_vars(dp);
-          let body_doc =
+      | Fun(dp, ty, dbody, s) when settings.show_fn_bodies =>
+        let bindings = DHPat.bound_vars(dp);
+        let body_doc =
+          switch (dbody) {
+          | Closure(env', dbody) =>
             go_formattable(
-              Closure(
-                ClosureEnvironment.without_keys(Option.to_list(s), env'),
-                d,
-              ),
+              Closure(env', dbody),
               ~env=
                 ClosureEnvironment.without_keys(
                   DHPat.bound_vars(dp) @ Option.to_list(s),
                   env,
                 ),
               ~recent_subst=
-                List.filter(x => !List.mem(x, bindings), recent_subst),
+                List.filter(x => !List.mem(x, bindings), next_recent_subst),
               Fun,
-            );
-          hcats(
-            [
-              DHDoc_common.Delim.sym_Fun,
-              DHDoc_Pat.mk(dp)
-              |> DHDoc_common.pad_child(
-                   ~inline_padding=(space(), space()),
-                   ~enforce_inline,
-                 ),
-            ]
-            @ (
-              settings.show_casts
-                ? [
-                  DHDoc_common.Delim.colon_Fun,
-                  space(),
-                  DHDoc_Typ.mk(~enforce_inline=true, ty),
-                  space(),
-                ]
-                : []
             )
-            @ [
-              DHDoc_common.Delim.arrow_Fun,
-              space(),
-              body_doc |> DHDoc_common.pad_child(~enforce_inline=false),
-            ],
-          );
-        } else {
-          switch (s) {
-          | None => annot(DHAnnot.Collapsed, text("<anon fn>"))
-          | Some(name) => annot(DHAnnot.Collapsed, text("<" ++ name ++ ">"))
-          };
-        }
-      | TypFun(_tpat, _dbody) =>
-        annot(DHAnnot.Collapsed, text("<anon typfn>"))
-      | Fun(dp, ty, dbody, s) =>
-        if (settings.show_fn_bodies) {
-          let bindings = DHPat.bound_vars(dp);
-          let body_doc =
+          | _ =>
             go_formattable(
               dbody,
               ~env=ClosureEnvironment.without_keys(bindings, env),
               ~recent_subst=
-                List.filter(x => !List.mem(x, bindings), recent_subst),
-              ~recursive_calls=Option.to_list(s) @ recursive_calls,
+                List.filter(x => !List.mem(x, bindings), next_recent_subst),
               Fun,
-            );
-          hcats(
-            [
-              DHDoc_common.Delim.sym_Fun,
-              DHDoc_Pat.mk(dp)
-              |> DHDoc_common.pad_child(
-                   ~inline_padding=(space(), space()),
-                   ~enforce_inline,
-                 ),
-            ]
-            @ (
-              settings.show_casts
-                ? [
-                  DHDoc_common.Delim.colon_Fun,
-                  space(),
-                  DHDoc_Typ.mk(~enforce_inline=true, ty),
-                  space(),
-                ]
-                : []
             )
-            @ [
-              DHDoc_common.Delim.arrow_Fun,
-              space(),
-              body_doc |> DHDoc_common.pad_child(~enforce_inline),
-            ],
-          );
-        } else {
+          };
+        hcats(
+          [
+            DHDoc_common.Delim.sym_Fun,
+            DHDoc_Pat.mk(dp)
+            |> DHDoc_common.pad_child(
+                 ~inline_padding=(space(), space()),
+                 ~enforce_inline,
+               ),
+          ]
+          @ (
+            settings.show_casts
+              ? [
+                DHDoc_common.Delim.colon_Fun,
+                space(),
+                DHDoc_Typ.mk(~enforce_inline=true, ty),
+                space(),
+              ]
+              : []
+          )
+          @ [
+            DHDoc_common.Delim.arrow_Fun,
+            space(),
+            body_doc |> DHDoc_common.pad_child(~enforce_inline=false),
+          ],
+        );
+      | Fun(_, _, _, s) =>
+        let name =
           switch (s) {
-          | None => annot(DHAnnot.Collapsed, text("<anon fn>"))
-          | Some(name) => annot(DHAnnot.Collapsed, text("<" ++ name ++ ">"))
+          | None => "anon fn"
+          | Some(name)
+              when
+                !settings.show_fixpoints
+                && String.ends_with(~suffix="+", name) =>
+            String.sub(name, 0, String.length(name) - 1)
+          | Some(name) => name
           };
-        }
-      | FixF(x, ty, dbody) when settings.show_fixpoints =>
+        annot(DHAnnot.Collapsed, text("<" ++ name ++ ">"));
+      | FixF(x, ty, dbody)
+          when settings.show_fn_bodies && settings.show_fixpoints =>
         let doc_body =
           go_formattable(
             dbody,
@@ -634,13 +621,13 @@ let mk =
               : []
           )
           @ [
+            space(),
             DHDoc_common.Delim.arrow_FixF,
             space(),
             doc_body |> DHDoc_common.pad_child(~enforce_inline),
           ],
         );
-      | FixF(x, _, d) =>
-        go'(~env=ClosureEnvironment.without_keys([x], env), d, FixF)
+      | FixF(x, _, _) => annot(DHAnnot.Collapsed, text("<" ++ x ++ ">"))
       };
     };
     let steppable =
@@ -649,13 +636,6 @@ let mk =
       chosen_step
       |> Option.map(x => x.ctx == Mark)
       |> Option.value(~default=false);
-    let substitution =
-      hidden_steps
-      |> List.find_opt(step =>
-           step.knd == VarLookup
-           // HACK[Matt]: to prevent substitutions hiding inside casts
-           && EvalCtx.fuzzy_mark(step.ctx)
-         );
     let doc =
       switch (substitution) {
       | Some({d_loc: BoundVar(v), _}) when List.mem(v, recent_subst) =>
@@ -683,6 +663,5 @@ let mk =
     chosen_step,
     List.mapi((idx, x: EvalObj.t) => (x.ctx, idx), next_steps),
     [],
-    [],
   );
 };

src/test/Test_Elaboration.re

@@ -265,7 +265,7 @@ let d9: DHExp.t =
         Var("x"),
         Int,
         BinIntOp(Plus, IntLit(1), BoundVar("x")),
-        Some("f"),
+        Some("f+"),
       ),
     ),
     IntLit(55),