Hide Ascriptions

src/CLI/Print.re

@@ -8,6 +8,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
   fold_case_clauses: false,
   fold_fn_bodies: `NoFold,
   hide_fixpoints: false,
+  show_ascriptions: true,
   show_filters: true,
   show_unknown_as_hole: true,
 };

src/haz3lcore/pretty/ExpToSegment.re

@@ -42,6 +42,7 @@ module Settings = {
     ],
     hide_fixpoints: bool,
     show_filters: bool,
+    show_ascriptions: bool,
     show_unknown_as_hole: bool,
   };
 
@@ -50,6 +51,7 @@ module Settings = {
     parenthesization: Defensive,
     label_format: QuoteWhenNecessary,
     inline,
+    show_ascriptions: settings.evaluation.show_ascriptions,
     fold_case_clauses: !settings.evaluation.show_case_clauses,
     fold_fn_bodies:
       fold_fn_bodies
@@ -69,6 +71,7 @@ module Settings = {
       inline,
       fold_case_clauses: false,
       fold_fn_bodies: `NoFold,
+      show_ascriptions: true,
       hide_fixpoints: false,
       show_filters: true,
       show_unknown_as_hole: true,
@@ -311,13 +314,17 @@ let rec parenthesize =
         (
           ~parenthesization: Settings.parenthesization,
           ~show_filters: bool,
+          ~show_ascriptions: bool,
           ~already_paren=false,
           exp: Exp.t,
         )
         : Exp.t => {
-  let parenthesize = parenthesize(~parenthesization, ~show_filters);
-  let parenthesize_pat = parenthesize_pat(~parenthesization, ~show_filters);
-  let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
+  let parenthesize =
+    parenthesize(~parenthesization, ~show_filters, ~show_ascriptions);
+  let parenthesize_pat =
+    parenthesize_pat(~parenthesization, ~show_filters, ~show_ascriptions);
+  let parenthesize_typ =
+    parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
   let paren_at = paren_at(~parenthesization);
   let paren_assoc_at = paren_assoc_at(~parenthesization);
   let paren_pat_at = paren_pat_at(~parenthesization);
@@ -499,12 +506,13 @@ let rec parenthesize =
       parenthesize(e2) |> paren_assoc_at(Precedence.semi),
     )
     |> rewrap
-  | Asc(e, t) =>
+  | Asc(e, t) when show_ascriptions =>
     Asc(
       parenthesize(e) |> paren_assoc_at(Precedence.asc),
       parenthesize_typ(t) |> paren_typ_at(Precedence.asc),
     )
     |> rewrap
+  | Asc(e, _) => parenthesize(e) // skip ascription if not showing
   | Test(e) => Test(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
   | HintedTest(e, hint) =>
     HintedTest(parenthesize(e) |> paren_at(Precedence.min), hint) |> rewrap
@@ -565,7 +573,10 @@ let rec parenthesize =
     |> rewrap
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
   };
@@ -574,12 +585,15 @@ and parenthesize_pat =
     (
       ~parenthesization: Settings.parenthesization,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       ~already_paren=false,
       pat: Pat.t,
     )
     : Pat.t => {
-  let parenthesize_pat = parenthesize_pat(~parenthesization, ~show_filters);
-  let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
+  let parenthesize_pat =
+    parenthesize_pat(~parenthesization, ~show_filters, ~show_ascriptions);
+  let parenthesize_typ =
+    parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
   let paren_pat_at = paren_pat_at(~parenthesization);
   let paren_pat_assoc_at = paren_pat_assoc_at(~parenthesization);
   let paren_typ_at = paren_typ_at(~parenthesization);
@@ -641,27 +655,33 @@ and parenthesize_pat =
     |> rewrap
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
-  | Asc(p, t) =>
+  | Asc(p, t) when show_ascriptions =>
     Asc(
       parenthesize_pat(p) |> paren_pat_assoc_at(Precedence.asc),
       parenthesize_typ(t) |> paren_typ_at(Precedence.max) // Hack[Matt]: always add parens to get the arrows right
     )
     |> rewrap
+  | Asc(p, _) => parenthesize_pat(p) // skip ascription if not showing
   };
 }
 
 and parenthesize_typ =
     (
       ~parenthesization: Settings.parenthesization,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       ~already_paren=false,
       typ: Typ.t,
     )
     : Typ.t => {
-  let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
+  let parenthesize_typ =
+    parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
   let paren_typ_at = paren_typ_at(~parenthesization);
   let paren_typ_assoc_at = paren_typ_assoc_at(~parenthesization);
   let paren_at = paren_at(~parenthesization);
@@ -749,7 +769,7 @@ and parenthesize_typ =
     |> rewrap
   | ProofOf(e) =>
     ProofOf(
-      parenthesize(~parenthesization, ~show_filters, e)
+      parenthesize(~parenthesization, ~show_ascriptions, ~show_filters, e)
       |> paren_at(Precedence.min),
     )
     |> rewrap
@@ -774,7 +794,14 @@ and parenthesize_typ =
     Unknown(
       Hole(
         MultiHole(
-          List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+          List.map(
+            parenthesize_any(
+              ~parenthesization,
+              ~show_ascriptions,
+              ~show_filters,
+            ),
+            xs,
+          ),
         ),
       ),
     )
@@ -786,6 +813,7 @@ and parenthesize_tpat =
     (
       ~parenthesization: Settings.parenthesization,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       tpat: TPat.t,
     )
     : TPat.t => {
@@ -799,7 +827,10 @@ and parenthesize_tpat =
   // Other forms
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
   };
@@ -808,6 +839,7 @@ and parenthesize_tpat =
 and parenthesize_rul =
     (
       ~parenthesization: Settings.parenthesization,
+      ~show_ascriptions: bool,
       ~show_filters: bool,
       rul: Rul.t,
     )
@@ -820,20 +852,33 @@ and parenthesize_rul =
   // Other forms
   | Rules(e, ps) =>
     Rules(
-      parenthesize(~parenthesization, ~show_filters, e),
+      parenthesize(~parenthesization, ~show_ascriptions, ~show_filters, e),
       List.map(
         ((p, e)) =>
           (
-            parenthesize_pat(~parenthesization, ~show_filters, p),
-            parenthesize(~parenthesization, ~show_filters, e),
+            parenthesize_pat(
+              ~parenthesization,
+              ~show_ascriptions,
+              ~show_filters,
+              p,
+            ),
+            parenthesize(
+              ~parenthesization,
+              ~show_ascriptions,
+              ~show_filters,
+              e,
+            ),
           ),
         ps,
       ),
     )
     |> rewrap
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
   };
@@ -844,22 +889,59 @@ and parenthesize_any =
       ~parenthesization: Settings.parenthesization,
       ~already_paren=false,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       any: Any.t,
     )
     : Any.t =>
   switch (any) {
   | Exp(e) =>
-    Exp(parenthesize(~parenthesization, ~already_paren, ~show_filters, e))
+    Exp(
+      parenthesize(
+        ~parenthesization,
+        ~already_paren,
+        ~show_ascriptions,
+        ~show_filters,
+        e,
+      ),
+    )
   | Pat(p) =>
     Pat(
-      parenthesize_pat(~parenthesization, ~already_paren, ~show_filters, p),
+      parenthesize_pat(
+        ~parenthesization,
+        ~already_paren,
+        ~show_ascriptions,
+        ~show_filters,
+        p,
+      ),
     )
   | Typ(t) =>
     Typ(
-      parenthesize_typ(~parenthesization, ~already_paren, ~show_filters, t),
+      parenthesize_typ(
+        ~parenthesization,
+        ~already_paren,
+        ~show_ascriptions,
+        ~show_filters,
+        t,
+      ),
+    )
+  | TPat(tp) =>
+    TPat(
+      parenthesize_tpat(
+        ~parenthesization,
+        ~show_ascriptions,
+        ~show_filters,
+        tp,
+      ),
+    )
+  | Rul(r) =>
+    Rul(
+      parenthesize_rul(
+        ~parenthesization,
+        ~show_ascriptions,
+        ~show_filters,
+        r,
+      ),
     )
-  | TPat(tp) => TPat(parenthesize_tpat(~parenthesization, ~show_filters, tp))
-  | Rul(r) => Rul(parenthesize_rul(~parenthesization, ~show_filters, r))
   | Any(_) => any
   };
 
@@ -1258,6 +1340,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
         Pat.fresh(Asc(p, t))
         |> parenthesize_pat(
              ~parenthesization=settings.parenthesization,
+             ~show_ascriptions=settings.show_ascriptions,
              ~show_filters=settings.show_filters,
            );
       };
@@ -2114,6 +2197,7 @@ let exp_to_segment =
          ~parenthesization=settings.parenthesization,
          ~already_paren,
          ~show_filters=settings.show_filters,
+         ~show_ascriptions=settings.show_ascriptions,
        );
   let p = exp_to_pretty(~settings, exp);
   p |> PrettySegment.select;
@@ -2125,6 +2209,7 @@ let typ_to_segment = (~settings: Settings.t, typ: Typ.t): Segment.t => {
     |> parenthesize_typ(
          ~parenthesization=settings.parenthesization,
          ~show_filters=settings.show_filters,
+         ~show_ascriptions=settings.show_ascriptions,
        );
   let p = typ_to_pretty(~settings, typ);
   p |> PrettySegment.select;
@@ -2138,6 +2223,7 @@ let any_to_segment =
          ~parenthesization=settings.parenthesization,
          ~already_paren,
          ~show_filters=settings.show_filters,
+         ~show_ascriptions=settings.show_ascriptions,
        );
   let p = any_to_pretty(~settings, any);
   p |> PrettySegment.select;

src/haz3lcore/zipper/action/Introduce.re

@@ -245,6 +245,7 @@ module Make =
           label_format: QuoteWhenNecessary,
           inline: true,
           fold_case_clauses: false,
+          show_ascriptions: true,
           fold_fn_bodies: `NoFold,
           hide_fixpoints: false,
           show_filters: true,

src/language/CoreSettings.re

@@ -7,6 +7,7 @@ module Evaluation = {
     show_fn_bodies: bool,
     show_fixpoints: bool,
     show_ascription_steps: bool,
+    show_ascriptions: bool,
     show_case_steps: bool,
     show_lookup_steps: bool,
     show_stepper_filters: bool,
@@ -22,6 +23,7 @@ module Evaluation = {
     show_fn_bodies: false,
     show_fixpoints: false,
     show_ascription_steps: false,
+    show_ascriptions: false,
     show_case_steps: false,
     show_lookup_steps: false,
     show_stepper_filters: false,

src/web/Settings.re

@@ -31,6 +31,7 @@ module Model = {
         show_fn_bodies: false,
         show_fixpoints: false,
         show_ascription_steps: false,
+        show_ascriptions: false,
         show_case_steps: false,
         show_lookup_steps: false,
         show_stepper_filters: false,
@@ -96,6 +97,7 @@ module Update = {
     | ShowCaseClauses
     | ShowFnBodies
     | ShowAscriptionSteps
+    | ShowAscriptions
     | ShowCaseSteps
     | ShowFixpoints
     | ShowLookups
@@ -210,6 +212,10 @@ module Update = {
               ...evaluation,
               show_ascription_steps: !evaluation.show_ascription_steps,
             }
+          | ShowAscriptions => {
+              ...evaluation,
+              show_ascriptions: !evaluation.show_ascriptions,
+            }
           | ShowCaseSteps => {
               ...evaluation,
               show_case_steps: !evaluation.show_case_steps,

src/web/app/editors/SettingsModal.re

@@ -41,6 +41,12 @@ let view =
         settings.show_case_clauses,
         Evaluation(ShowCaseClauses),
       ),
+      setting(
+        "⇨",
+        "show case steps",
+        settings.show_case_steps,
+        Evaluation(ShowCaseSteps),
+      ),
       setting(
         "λ",
         "show function bodies",
@@ -53,6 +59,12 @@ let view =
         settings.show_fixpoints,
         Evaluation(ShowFixpoints),
       ),
+      setting(
+        ":",
+        "show ascriptions",
+        settings.show_ascriptions,
+        Evaluation(ShowAscriptions),
+      ),
       setting(
         "⇨",
         "show ascription steps",