Skip to content

Commit 5aea420

Browse files
NegabinaryNegabinary
committed
hide ascriptions
1 parent f3da8a1 commit 5aea420

File tree

10 files changed

+120
-22
lines changed

10 files changed

+120
-22
lines changed

‎src/CLI/Print.re‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
88
fold_case_clauses: false,
99
fold_fn_bodies: `NoFold,
1010
hide_fixpoints: false,
11+
show_ascriptions: true,
1112
show_filters: true,
1213
show_unknown_as_hole: true,
1314
};

‎src/haz3lcore/pretty/ExpToSegment.re‎

Lines changed: 108 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ module Settings = {
4242
],
4343
hide_fixpoints: bool,
4444
show_filters: bool,
45+
show_ascriptions: bool,
4546
show_unknown_as_hole: bool,
4647
};
4748

@@ -50,6 +51,7 @@ module Settings = {
5051
parenthesization: Defensive,
5152
label_format: QuoteWhenNecessary,
5253
inline,
54+
show_ascriptions: settings.evaluation.show_ascriptions,
5355
fold_case_clauses: !settings.evaluation.show_case_clauses,
5456
fold_fn_bodies:
5557
fold_fn_bodies
@@ -69,6 +71,7 @@ module Settings = {
6971
inline,
7072
fold_case_clauses: false,
7173
fold_fn_bodies: `NoFold,
74+
show_ascriptions: true,
7275
hide_fixpoints: false,
7376
show_filters: true,
7477
show_unknown_as_hole: true,
@@ -311,13 +314,17 @@ let rec parenthesize =
311314
(
312315
~parenthesization: Settings.parenthesization,
313316
~show_filters: bool,
317+
~show_ascriptions: bool,
314318
~already_paren=false,
315319
exp: Exp.t,
316320
)
317321
: Exp.t => {
318-
let parenthesize = parenthesize(~parenthesization, ~show_filters);
319-
let parenthesize_pat = parenthesize_pat(~parenthesization, ~show_filters);
320-
let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
322+
let parenthesize =
323+
parenthesize(~parenthesization, ~show_filters, ~show_ascriptions);
324+
let parenthesize_pat =
325+
parenthesize_pat(~parenthesization, ~show_filters, ~show_ascriptions);
326+
let parenthesize_typ =
327+
parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
321328
let paren_at = paren_at(~parenthesization);
322329
let paren_assoc_at = paren_assoc_at(~parenthesization);
323330
let paren_pat_at = paren_pat_at(~parenthesization);
@@ -499,12 +506,13 @@ let rec parenthesize =
499506
parenthesize(e2) |> paren_assoc_at(Precedence.semi),
500507
)
501508
|> rewrap
502-
| Asc(e, t) =>
509+
| Asc(e, t) when show_ascriptions =>
503510
Asc(
504511
parenthesize(e) |> paren_assoc_at(Precedence.asc),
505512
parenthesize_typ(t) |> paren_typ_at(Precedence.asc),
506513
)
507514
|> rewrap
515+
| Asc(e, _) => parenthesize(e) // skip ascription if not showing
508516
| Test(e) => Test(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
509517
| HintedTest(e, hint) =>
510518
HintedTest(parenthesize(e) |> paren_at(Precedence.min), hint) |> rewrap
@@ -565,7 +573,10 @@ let rec parenthesize =
565573
|> rewrap
566574
| MultiHole(xs) =>
567575
MultiHole(
568-
List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
576+
List.map(
577+
parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
578+
xs,
579+
),
569580
)
570581
|> rewrap
571582
};
@@ -574,12 +585,15 @@ and parenthesize_pat =
574585
(
575586
~parenthesization: Settings.parenthesization,
576587
~show_filters: bool,
588+
~show_ascriptions: bool,
577589
~already_paren=false,
578590
pat: Pat.t,
579591
)
580592
: Pat.t => {
581-
let parenthesize_pat = parenthesize_pat(~parenthesization, ~show_filters);
582-
let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
593+
let parenthesize_pat =
594+
parenthesize_pat(~parenthesization, ~show_filters, ~show_ascriptions);
595+
let parenthesize_typ =
596+
parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
583597
let paren_pat_at = paren_pat_at(~parenthesization);
584598
let paren_pat_assoc_at = paren_pat_assoc_at(~parenthesization);
585599
let paren_typ_at = paren_typ_at(~parenthesization);
@@ -641,27 +655,33 @@ and parenthesize_pat =
641655
|> rewrap
642656
| MultiHole(xs) =>
643657
MultiHole(
644-
List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
658+
List.map(
659+
parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
660+
xs,
661+
),
645662
)
646663
|> rewrap
647-
| Asc(p, t) =>
664+
| Asc(p, t) when show_ascriptions =>
648665
Asc(
649666
parenthesize_pat(p) |> paren_pat_assoc_at(Precedence.asc),
650667
parenthesize_typ(t) |> paren_typ_at(Precedence.max) // Hack[Matt]: always add parens to get the arrows right
651668
)
652669
|> rewrap
670+
| Asc(p, _) => parenthesize_pat(p) // skip ascription if not showing
653671
};
654672
}
655673

656674
and parenthesize_typ =
657675
(
658676
~parenthesization: Settings.parenthesization,
659677
~show_filters: bool,
678+
~show_ascriptions: bool,
660679
~already_paren=false,
661680
typ: Typ.t,
662681
)
663682
: Typ.t => {
664-
let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
683+
let parenthesize_typ =
684+
parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
665685
let paren_typ_at = paren_typ_at(~parenthesization);
666686
let paren_typ_assoc_at = paren_typ_assoc_at(~parenthesization);
667687
let paren_at = paren_at(~parenthesization);
@@ -749,7 +769,7 @@ and parenthesize_typ =
749769
|> rewrap
750770
| ProofOf(e) =>
751771
ProofOf(
752-
parenthesize(~parenthesization, ~show_filters, e)
772+
parenthesize(~parenthesization, ~show_ascriptions, ~show_filters, e)
753773
|> paren_at(Precedence.min),
754774
)
755775
|> rewrap
@@ -774,7 +794,14 @@ and parenthesize_typ =
774794
Unknown(
775795
Hole(
776796
MultiHole(
777-
List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
797+
List.map(
798+
parenthesize_any(
799+
~parenthesization,
800+
~show_ascriptions,
801+
~show_filters,
802+
),
803+
xs,
804+
),
778805
),
779806
),
780807
)
@@ -786,6 +813,7 @@ and parenthesize_tpat =
786813
(
787814
~parenthesization: Settings.parenthesization,
788815
~show_filters: bool,
816+
~show_ascriptions: bool,
789817
tpat: TPat.t,
790818
)
791819
: TPat.t => {
@@ -799,7 +827,10 @@ and parenthesize_tpat =
799827
// Other forms
800828
| MultiHole(xs) =>
801829
MultiHole(
802-
List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
830+
List.map(
831+
parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
832+
xs,
833+
),
803834
)
804835
|> rewrap
805836
};
@@ -808,6 +839,7 @@ and parenthesize_tpat =
808839
and parenthesize_rul =
809840
(
810841
~parenthesization: Settings.parenthesization,
842+
~show_ascriptions: bool,
811843
~show_filters: bool,
812844
rul: Rul.t,
813845
)
@@ -820,20 +852,33 @@ and parenthesize_rul =
820852
// Other forms
821853
| Rules(e, ps) =>
822854
Rules(
823-
parenthesize(~parenthesization, ~show_filters, e),
855+
parenthesize(~parenthesization, ~show_ascriptions, ~show_filters, e),
824856
List.map(
825857
((p, e)) =>
826858
(
827-
parenthesize_pat(~parenthesization, ~show_filters, p),
828-
parenthesize(~parenthesization, ~show_filters, e),
859+
parenthesize_pat(
860+
~parenthesization,
861+
~show_ascriptions,
862+
~show_filters,
863+
p,
864+
),
865+
parenthesize(
866+
~parenthesization,
867+
~show_ascriptions,
868+
~show_filters,
869+
e,
870+
),
829871
),
830872
ps,
831873
),
832874
)
833875
|> rewrap
834876
| MultiHole(xs) =>
835877
MultiHole(
836-
List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
878+
List.map(
879+
parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
880+
xs,
881+
),
837882
)
838883
|> rewrap
839884
};
@@ -844,22 +889,59 @@ and parenthesize_any =
844889
~parenthesization: Settings.parenthesization,
845890
~already_paren=false,
846891
~show_filters: bool,
892+
~show_ascriptions: bool,
847893
any: Any.t,
848894
)
849895
: Any.t =>
850896
switch (any) {
851897
| Exp(e) =>
852-
Exp(parenthesize(~parenthesization, ~already_paren, ~show_filters, e))
898+
Exp(
899+
parenthesize(
900+
~parenthesization,
901+
~already_paren,
902+
~show_ascriptions,
903+
~show_filters,
904+
e,
905+
),
906+
)
853907
| Pat(p) =>
854908
Pat(
855-
parenthesize_pat(~parenthesization, ~already_paren, ~show_filters, p),
909+
parenthesize_pat(
910+
~parenthesization,
911+
~already_paren,
912+
~show_ascriptions,
913+
~show_filters,
914+
p,
915+
),
856916
)
857917
| Typ(t) =>
858918
Typ(
859-
parenthesize_typ(~parenthesization, ~already_paren, ~show_filters, t),
919+
parenthesize_typ(
920+
~parenthesization,
921+
~already_paren,
922+
~show_ascriptions,
923+
~show_filters,
924+
t,
925+
),
926+
)
927+
| TPat(tp) =>
928+
TPat(
929+
parenthesize_tpat(
930+
~parenthesization,
931+
~show_ascriptions,
932+
~show_filters,
933+
tp,
934+
),
935+
)
936+
| Rul(r) =>
937+
Rul(
938+
parenthesize_rul(
939+
~parenthesization,
940+
~show_ascriptions,
941+
~show_filters,
942+
r,
943+
),
860944
)
861-
| TPat(tp) => TPat(parenthesize_tpat(~parenthesization, ~show_filters, tp))
862-
| Rul(r) => Rul(parenthesize_rul(~parenthesization, ~show_filters, r))
863945
| Any(_) => any
864946
};
865947

@@ -1258,6 +1340,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
12581340
Pat.fresh(Asc(p, t))
12591341
|> parenthesize_pat(
12601342
~parenthesization=settings.parenthesization,
1343+
~show_ascriptions=settings.show_ascriptions,
12611344
~show_filters=settings.show_filters,
12621345
);
12631346
};
@@ -2114,6 +2197,7 @@ let exp_to_segment =
21142197
~parenthesization=settings.parenthesization,
21152198
~already_paren,
21162199
~show_filters=settings.show_filters,
2200+
~show_ascriptions=settings.show_ascriptions,
21172201
);
21182202
let p = exp_to_pretty(~settings, exp);
21192203
p |> PrettySegment.select;
@@ -2125,6 +2209,7 @@ let typ_to_segment = (~settings: Settings.t, typ: Typ.t): Segment.t => {
21252209
|> parenthesize_typ(
21262210
~parenthesization=settings.parenthesization,
21272211
~show_filters=settings.show_filters,
2212+
~show_ascriptions=settings.show_ascriptions,
21282213
);
21292214
let p = typ_to_pretty(~settings, typ);
21302215
p |> PrettySegment.select;
@@ -2138,6 +2223,7 @@ let any_to_segment =
21382223
~parenthesization=settings.parenthesization,
21392224
~already_paren,
21402225
~show_filters=settings.show_filters,
2226+
~show_ascriptions=settings.show_ascriptions,
21412227
);
21422228
let p = any_to_pretty(~settings, any);
21432229
p |> PrettySegment.select;

‎src/haz3lcore/zipper/action/Introduce.re‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,7 @@ module Make =
245245
label_format: QuoteWhenNecessary,
246246
inline: true,
247247
fold_case_clauses: false,
248+
show_ascriptions: true,
248249
fold_fn_bodies: `NoFold,
249250
hide_fixpoints: false,
250251
show_filters: true,

‎src/language/CoreSettings.re‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module Evaluation = {
77
show_fn_bodies: bool,
88
show_fixpoints: bool,
99
show_ascription_steps: bool,
10+
show_ascriptions: bool,
1011
show_case_steps: bool,
1112
show_lookup_steps: bool,
1213
show_stepper_filters: bool,
@@ -22,6 +23,7 @@ module Evaluation = {
2223
show_fn_bodies: false,
2324
show_fixpoints: false,
2425
show_ascription_steps: false,
26+
show_ascriptions: false,
2527
show_case_steps: false,
2628
show_lookup_steps: false,
2729
show_stepper_filters: false,

‎src/web/Settings.re‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ module Model = {
3131
show_fn_bodies: false,
3232
show_fixpoints: false,
3333
show_ascription_steps: false,
34+
show_ascriptions: false,
3435
show_case_steps: false,
3536
show_lookup_steps: false,
3637
show_stepper_filters: false,

‎src/web/app/inspector/CursorInspector.re‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,7 @@ let code_view_settings: Haz3lcore.ExpToSegment.Settings.t = {
8383
fold_case_clauses: false,
8484
fold_fn_bodies: `NoFold,
8585
hide_fixpoints: false,
86+
show_ascriptions: true,
8687
show_filters: false,
8788
show_unknown_as_hole: true,
8889
};

‎src/web/view/ContextInspector.re‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ let context_entry_view = (~globals, entry: Language.Ctx.entry): Node.t => {
1919
fold_case_clauses: false,
2020
fold_fn_bodies: `NoFold,
2121
hide_fixpoints: false,
22+
show_ascriptions: true,
2223
show_filters: false,
2324
show_unknown_as_hole: true,
2425
},

‎src/web/view/Kind.re‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ let view = (~globals, kind: Language.Ctx.kind): Node.t =>
1818
fold_case_clauses: false,
1919
fold_fn_bodies: `NoFold,
2020
hide_fixpoints: false,
21+
show_ascriptions: true,
2122
show_filters: false,
2223
show_unknown_as_hole: true,
2324
},

0 commit comments

Comments
 (0)