From d345600af2d7acf23a5a14315a4011b49718a1dc Mon Sep 17 00:00:00 2001 From: Michael Shulman Date: Sat, 1 Mar 2025 14:02:57 -0600 Subject: [PATCH] print_in_case as a flag rather than a function --- lib/parser/builtins.ml | 26 +++++++++++--------------- lib/parser/notation.ml | 14 ++++++++------ lib/parser/notation.mli | 5 ++--- lib/parser/print.ml | 23 ++++------------------- 4 files changed, 25 insertions(+), 43 deletions(-) diff --git a/lib/parser/builtins.ml b/lib/parser/builtins.ml index 74fc7ef..89ca738 100644 --- a/lib/parser/builtins.ml +++ b/lib/parser/builtins.ml @@ -511,10 +511,8 @@ let pp_abs cube space ppf obs ws = let () = set_processor abs (process_abs `Normal); set_processor cubeabs (process_abs `Cube); - set_print abs (pp_abs `Normal); - set_print cubeabs (pp_abs `Cube); - set_print_as_case abs (pp_abs `Normal); - set_print_as_case cubeabs (pp_abs `Cube) + set_print abs ~in_case:true (pp_abs `Normal); + set_print cubeabs ~in_case:true (pp_abs `Cube) (* ******************** The universe @@ -699,9 +697,7 @@ let pp_tuple space ppf obs ws = pp_ws space ppf wsrparen; pp_close_box ppf () -let () = - set_print parens pp_tuple; - set_print_as_case parens pp_tuple +let () = set_print parens ~in_case:true pp_tuple (* ******************** Comatches @@ -1392,11 +1388,11 @@ and pp_match box space ppf obs ws = (* Matches and comatches are only valid in case trees. *) let () = - set_print_as_case implicit_mtch (pp_match true); - set_print_as_case explicit_mtch (pp_match true); - set_print_as_case mtchlam (pp_match true); - set_print_as_case comatch (pp_match true); - set_print_as_case empty_co_match (pp_match true) + set_print implicit_mtch ~in_case:true (pp_match true); + set_print explicit_mtch ~in_case:true (pp_match true); + set_print mtchlam ~in_case:true (pp_match true); + set_print comatch ~in_case:true (pp_match true); + set_print empty_co_match ~in_case:true (pp_match true) (* ******************** Codatatypes @@ -1490,7 +1486,7 @@ let pp_codata space ppf obs ws = pp_ws space ppf wsrbrack; pp_close_box ppf () -let () = set_print codata pp_codata +let () = set_print codata ~in_case:true pp_codata (* ******************** Record types @@ -1649,7 +1645,7 @@ let pp_record space ppf obs ws = pp_ws space ppf wsrparen; pp_close_box ppf () -let () = set_print record pp_record +let () = set_print record ~in_case:true pp_record (* ******************** Datatypes @@ -1784,7 +1780,7 @@ let pp_data space ppf obs ws = pp_ws space ppf wsrbrack; pp_close_box ppf () -let () = set_print data pp_data +let () = set_print data ~in_case:true pp_data (* ******************** Forwards Lists diff --git a/lib/parser/notation.ml b/lib/parser/notation.ml index ca80f4f..f757929 100644 --- a/lib/parser/notation.ml +++ b/lib/parser/notation.ml @@ -167,9 +167,9 @@ and ('left, 'tight, 'right) notation = { (* The remaining fields are mutable because they have to be able to refer to the notation object itself, so we have a circular data structure. They aren't expected to mutate further after being set once. Thus we store them as options, to record whether they have been set. *) mutable tree : ('left, 'tight) notation_entry option; mutable processor : processor option; - (* Some notations only make sense in terms, others only make sense in case trees, and some make sense in either. Thus, a notation can supply either or both of these printing functions. *) mutable print : printer option; - mutable print_as_case : printer option; + (* Whether this notation can appear in a case tree. Otherwise, encountering it terminates the case tree in a leaf. *) + mutable print_in_case : bool; } module Notation = struct @@ -264,9 +264,11 @@ let set_processor n c = | None -> n.processor <- Some c let print n = n.print -let set_print n p = n.print <- Some p -let print_as_case n = n.print_as_case -let set_print_as_case n p = n.print_as_case <- Some p +let print_in_case n = n.print_in_case + +let set_print n ?(in_case = false) p = + n.print <- Some p; + n.print_in_case <- in_case (* Create a new notation with specified name, fixity, and tightness. Its mutable fields must be set later. *) let make : @@ -285,8 +287,8 @@ let make : right; tree = None; print = None; - print_as_case = None; processor = None; + print_in_case = false; } let rec split_last_whitespace (ws : Whitespace.alist) : Whitespace.alist * Whitespace.t list = diff --git a/lib/parser/notation.mli b/lib/parser/notation.mli index 1a154ff..838a91a 100644 --- a/lib/parser/notation.mli +++ b/lib/parser/notation.mli @@ -139,9 +139,8 @@ val set_tree : ('left, 'tight, 'right) notation -> ('left, 'tight) notation_entr val processor : ('left, 'tight, 'right) notation -> processor val set_processor : ('left, 'tight, 'right) notation -> processor -> unit val print : ('left, 'tight, 'right) notation -> printer option -val set_print : ('left, 'tight, 'right) notation -> printer -> unit -val print_as_case : ('left, 'tight, 'right) notation -> printer option -val set_print_as_case : ('left, 'tight, 'right) notation -> printer -> unit +val print_in_case : ('left, 'tight, 'right) notation -> bool +val set_print : ('left, 'tight, 'right) notation -> ?in_case:bool -> printer -> unit val make : string -> ('left, 'tight, 'right) fixity -> ('left, 'tight, 'right) notation val equal : ('l1, 't1, 'r1) notation -> ('l2, 't2, 'r2) notation -> bool diff --git a/lib/parser/print.ml b/lib/parser/print.ml index da022c6..318f778 100644 --- a/lib/parser/print.ml +++ b/lib/parser/print.ml @@ -121,12 +121,10 @@ let pp_ws (space : space) (ppf : formatter) (ws : Whitespace.t list) : unit = (* Print a parse tree. *) let rec pp_term (space : space) (ppf : formatter) (wtr : observation) : unit = let (Term tr) = wtr in - match state () with - | `Case -> ( - match tr.value with - | Notn n -> pp_notn_case space ppf (notn n) (args n) (whitespace n) - | _ -> as_term @@ fun () -> pp_term space ppf wtr) - | `Term -> ( + match tr.value with + | Notn n when print_in_case (notn n) -> pp_notn space ppf (notn n) (args n) (whitespace n) + | _ -> ( + Printconfig.as_term @@ fun () -> match tr.value with | Notn n -> pp_notn space ppf (notn n) (args n) (whitespace n) | App _ -> @@ -168,19 +166,6 @@ and pp_superscript ppf str = pp_utf_8 ppf str; pp_utf_8 ppf ")" -and pp_notn_case : - type left tight right. - space -> - formatter -> - (left, tight, right) notation -> - observation list -> - Whitespace.alist -> - unit = - fun space ppf n obs ws -> - match print_as_case n with - | Some pp -> pp space ppf obs ws - | None -> as_term @@ fun () -> pp_notn space ppf n obs ws - and pp_notn : type left tight right. space ->