From eb79d56b276678e9a8c3d24b46d32722f7896f79 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 11:51:58 +0800 Subject: [PATCH 01/15] create dynamic typing module --- lib/hipcore_typed/dune | 3 ++- lib/hipcore_typed/dynamic_typing.ml | 34 ++++++++++++++++++++++++++++ lib/hipcore_typed/dynamic_typing.mli | 23 +++++++++++++++++++ 3 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 lib/hipcore_typed/dynamic_typing.ml create mode 100644 lib/hipcore_typed/dynamic_typing.mli diff --git a/lib/hipcore_typed/dune b/lib/hipcore_typed/dune index 0e7dc019..13630879 100644 --- a/lib/hipcore_typed/dune +++ b/lib/hipcore_typed/dune @@ -1,7 +1,8 @@ (library (name hipcore_typed) (public_name heifer.hipcore_typed) - (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast) + (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast + dynamic_typing) (libraries debug unionFind str utils hipcore) (inline_tests) (preprocess (pps ppx_expect ppx_deriving.std visitors.ppx))) diff --git a/lib/hipcore_typed/dynamic_typing.ml b/lib/hipcore_typed/dynamic_typing.ml new file mode 100644 index 00000000..6ead1ac5 --- /dev/null +++ b/lib/hipcore_typed/dynamic_typing.ml @@ -0,0 +1,34 @@ +open Typedhip + +let status = ref false + +let set_dynamic_typing () = status := true + +let dynamic_typing_enabled () = !status + +let spec_visitor f = object + inherit [_] map_spec + + method! visit_typ _ t = f t +end + +let type_with_any_spec s = (spec_visitor (fun _ -> Any))#visit_staged_spec () s + +let instantiate_any_types_pi p = (spec_visitor (fun _ -> TVar (Variables.fresh_variable ())))#visit_pi () p + +let check_for_untyped_visitor = object + inherit [_] reduce_spec + + method zero = false + method plus = (||) + + method! visit_CShift _ _ _ _ = true + method! visit_CReset _ _ = true + + method! visit_Shift _ _ _ _ _ _ = true + method! visit_Reset _ _ = true +end + +let uses_untyped_extensions_spec s = check_for_untyped_visitor#visit_staged_spec () s + +let uses_untyped_extensions_core c = check_for_untyped_visitor#visit_core_lang () c diff --git a/lib/hipcore_typed/dynamic_typing.mli b/lib/hipcore_typed/dynamic_typing.mli new file mode 100644 index 00000000..c64dea7c --- /dev/null +++ b/lib/hipcore_typed/dynamic_typing.mli @@ -0,0 +1,23 @@ +open Typedhip + +(** Enable dynamic typing. This disables all type checks before translation to SMT. + This does not do anything by itself; relevant areas of the library whose + behaviors differ between untyped and typed mode must check this flag + using [dynamic_typing_enabled]. + + This must be called before any input is processed. *) +val set_dynamic_typing : unit -> unit + +val dynamic_typing_enabled : unit -> bool + +(** Replace all types in this specification with [Any]. *) +val type_with_any_spec : staged_spec -> staged_spec + +(** Replace all [Any] types in this pure formula with fresh type variables. + Inferring these types can be done using one of the [Infer_types] endpoints. *) +val instantiate_any_types_pi : pi -> pi + +(* Currently, the only untyped extensions are shift/reset. *) + +val uses_untyped_extensions_spec : staged_spec -> bool +val uses_untyped_extensions_core : core_lang -> bool From e8c85676e070addf5238a7e15f03b757cd88e47d Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 13:49:23 +0800 Subject: [PATCH 02/15] fail non-term substs when given a non-var --- lib/hipcore_typed/subst.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml index cc16d449..29dfbe44 100644 --- a/lib/hipcore_typed/subst.ml +++ b/lib/hipcore_typed/subst.ml @@ -52,7 +52,8 @@ let reduce_visitor_function (type ctx_type) reduce_visitor (ctx_type : ctx_type let find_non_term_binding x bindings = match List.assoc_opt x bindings with | Some {term_desc = Var name; _} -> name - | _ -> x + | Some _ -> failwith "Expected (Var _) for non-term substitution" + | None -> x let types_of_free_vars (type ctx_type) (ctx_type : ctx_type subst_context) (ctx : ctx_type) = let visitor = From 0f39bb51d92f1acc62ea6b625e2eba5ac63ae850 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:01:34 +0800 Subject: [PATCH 03/15] add dynamic typing switch in frontend --- lib/hiplib/hiplib.ml | 38 ++++++++++++++++++++++++++++++++++++-- main/hip.ml | 4 ++++ 2 files changed, 40 insertions(+), 2 deletions(-) diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml index 5da18f31..14298fb8 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -179,6 +179,12 @@ let check_method prog inferred given = let infer_and_check_method (prog : core_program) (meth : meth_def) (given_spec : staged_spec option) = let inferred_spec = infer_spec prog meth in + let inferred_spec, given_spec = + let open Dynamic_typing in + if dynamic_typing_enabled () + then type_with_any_spec inferred_spec, Option.map type_with_any_spec given_spec + else inferred_spec, given_spec + in let result = check_method prog inferred_spec given_spec in inferred_spec, result @@ -271,9 +277,33 @@ let process_pure_fn_info ({m_name; m_params; m_body; _}) = function in Globals.define_pure_fn m_name pf +let type_with_any_binder b = ident_of_binder b, Any + +(** Substitute Any into the types of this lemma if dynamic typing is enabled. *) +let use_dynamic_types_if_enabled_lem (l : Typedhip.lemma) = + let open Dynamic_typing in + if dynamic_typing_enabled () + then {l with + l_params = l.l_params |> List.map type_with_any_binder; + l_left = type_with_any_spec l.l_left; + l_right = type_with_any_spec l.l_right} + else l + +(** Substitute Any into the types of this method if dynamic typing is enabled. + + {b Note:} This does not dynamically type core language expressions (which need + to be dynamically typed later), due to the forward verification process needing some + type information (e.g. during pattern matching.) *) +let use_dynamic_types_if_enabled_meth (m : meth_def) = + let open Dynamic_typing in + if dynamic_typing_enabled () + then {m with m_params = List.map type_with_any_binder m.m_params; + m_spec = Option.map type_with_any_spec m.m_spec} + else m + let process_intermediates (it : Typedhip.intermediate) prog : binder list * core_program = - (* Format.printf "%s\n" (Pretty.string_of_intermediate it); - ([], prog) *) + (* This is the point where dynamic typing, if enabled, is applied; when filling out a case, + make sure to handle this. *) let open Typedhip in match it with (* | LogicTypeDecl (name, params, ret, path, lname) -> @@ -307,6 +337,7 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core debug ~at:4 ~title:(Format.asprintf "added lemma %s" l.l_name) "%s" (string_of_lemma l); *) (* add to environment regardless of failure *) (* we need to prove the lemma *) + let l = use_dynamic_types_if_enabled_lem l in let@ _ = Debug.span (fun _ -> debug ~at:1 ~title:(Format.sprintf "verifying lemma: %s" l.l_name) "") in @@ -334,6 +365,9 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core | Meth (m_name, m_params, m_spec, m_body, m_tactics, pure_fn_info) -> let meth : meth_def = {m_name; m_params; m_spec; m_body; m_tactics} in process_pure_fn_info meth pure_fn_info; + (* Apply dynamic typing _after_ doing pure function processing; since pure functions need to be + handled by SMT (and so need to be always typed anyway.) *) + let meth = use_dynamic_types_if_enabled_meth meth in let@ _ = Debug.span (fun _ -> debug ~at:1 ~title:(Format.asprintf "verifying function: %s" meth.m_name) "") in diff --git a/main/hip.ml b/main/hip.ml index 06d194de..bb6376ef 100644 --- a/main/hip.ml +++ b/main/hip.ml @@ -18,6 +18,10 @@ let () = Hiplib.(file_mode := (Option.bind (Sys.getenv_opt "FILE") int_of_string_opt |> Option.value ~default:0) > 0); + begin + if Option.bind (Sys.getenv_opt "NOTYPES") int_of_string_opt |> Option.value ~default:0 > 0 + then Hipcore_typed.Dynamic_typing.set_dynamic_typing () + end; let ctf = Option.bind (Sys.getenv_opt "CTF") int_of_string_opt |> Option.value ~default:0 > 0 From 289e1e807c83e5e3af72a1b806feaf4ae5c92d02 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:39:42 +0800 Subject: [PATCH 04/15] instantiate all Any types before SMT check --- lib/hipprover/entail.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index 68dcccdb..05dec1dc 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -237,6 +237,8 @@ let check_pure_obligation left right = the untyped extensions. Perform another typechecking phase to perform these unifications. *) let (left, right), _ = + let left = Dynamic_typing.instantiate_any_types_pi left in + let right = Dynamic_typing.instantiate_any_types_pi right in let open Infer_types in with_empty_env begin let* left, right = infer_types_pair_pi left right in From d2a1e631b627ad91056dc627c1dbb7c546cce599 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:39:58 +0800 Subject: [PATCH 05/15] suppress Infer_types.Unification_failure during entailment this should probably only be done in untyped mode, though currently the `can_unify_with` check eliminates all ill-typed instantiations in typed mode so it won't change anything for now --- lib/hipprover/entail.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index 05dec1dc..f361a7c7 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -825,11 +825,15 @@ let suppress_exn ~title ~default (f : unit -> 'a) : 'a = debug ~at:5 ~title "%s" (Printexc.to_string e); default -let suppress_some_exn ~title ~default (f : unit -> 'a) : 'a = +(** Suppress type errors from the prover backends and type checker, instead outputting + a debug log message (whose title is [title]) and returning [default]. These are usually + caused by the instantiation heuristic not catching ill-typed instantiations (especially + when in untyped mode), and are useful to let those instantiations act as a failing branch instead. *) +let suppress_type_exn ~title ~default (f : unit -> 'a) : 'a = try f () with - | Z3.Error _ | Infer_types.Cyclic_type _ as e -> + | Z3.Error _ | Infer_types.Cyclic_type _ | Infer_types.Unification_failure _ as e -> debug ~at:5 ~title "%s" (Printexc.to_string e); default @@ -1133,7 +1137,7 @@ let rec apply_ent_rule ?name : tactic = (* copy the binder's type to allow for polymorphic constants in try_constants *) let f4 = Subst.subst_free_vars [(ident_of_binder x, term c.term_desc (type_of_binder x))] f4 in fun k1 -> - let@ _ = suppress_some_exn + let@ _ = suppress_type_exn ~title:"ERROR: exists on the right, entailment step" ~default:fail in @@ -1157,7 +1161,7 @@ let rec apply_ent_rule ?name : tactic = if Hipcore.Types.can_unify_with c.term_type (type_of_binder x) then let f3 = Subst.subst_free_vars [((ident_of_binder x), term c.term_desc (type_of_binder x))] f3 in fun k1 -> - let@ _ = suppress_some_exn + let@ _ = suppress_type_exn ~title:"ERROR: forall on the left, entailment step" ~default:fail in From 117ffb71d982dfbd7fbca35a6fc7631857471a28 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:58:07 +0800 Subject: [PATCH 06/15] add docs --- docs/development.md | 7 +++++++ lib/hipcore_typed/dynamic_typing.mli | 3 ++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/development.md b/docs/development.md index dd1452cc..dafb2e86 100644 --- a/docs/development.md +++ b/docs/development.md @@ -74,6 +74,13 @@ Some of the environment variables Heifer interprets may be useful for testing. Setting `TEST=1` causes Heifer to print only whether a test has failed, which is useful for integration tests. A test in this context is a function whose main entailment proof must succeed; if its name has the suffix `_false`, the entailment must fail. +## Untyped extensions + +Some extensions not supported by mainline OCaml are supported. Currently, this only includes delimited continuation operators (ala [OchaCaml](https://www.is.ocha.ac.jp/~asai/OchaCaml/)), but more may be supported. + +Setting `NOTYPES=1` will defer all typechecking during entailment checks until necessary (i.e. before SMT translation). This may be useful to ease development of extensions +outside of those typechecked by OCaml. + ## Logging and tracing View log output by setting `DEBUG=n`. diff --git a/lib/hipcore_typed/dynamic_typing.mli b/lib/hipcore_typed/dynamic_typing.mli index c64dea7c..801c60d9 100644 --- a/lib/hipcore_typed/dynamic_typing.mli +++ b/lib/hipcore_typed/dynamic_typing.mli @@ -5,7 +5,8 @@ open Typedhip behaviors differ between untyped and typed mode must check this flag using [dynamic_typing_enabled]. - This must be called before any input is processed. *) + For a declaration to be processed in untyped mode, this must be called before + the declaration is processed. *) val set_dynamic_typing : unit -> unit val dynamic_typing_enabled : unit -> bool From a84d907e15784fb482624c6d9387dc5079346777 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Thu, 28 Aug 2025 15:43:09 +0800 Subject: [PATCH 07/15] start on pretty-print rewrite need to check tests if the changes are only format-wise --- lib/hipcore_typed/Pretty.ml | 931 ++++++++++++++-------------- lib/hipcore_typed/Pretty.mli | 54 ++ lib/hipcore_typed/typed_core_ast.ml | 19 + lib/hiplib/hiplib.ml | 1 + lib/hipprover/entail.ml | 2 +- lib/hipprover/rewriting.ml | 14 +- 6 files changed, 541 insertions(+), 480 deletions(-) create mode 100644 lib/hipcore_typed/Pretty.mli diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index 62172539..a7bc79c5 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -6,481 +6,468 @@ open Types open Utils.Misc open Utils.Hstdlib -exception Foo of string - -let colours = Pretty.colours - -let string_of_type = Pretty.string_of_type - -let red = Pretty.red -let green = Pretty.green -let yellow = Pretty.yellow - -let string_of_binder ((ident, typ) : binder) = - Format.sprintf "(%s : %s)" ident (string_of_type typ) -let string_of_constr_call n args = - match n, args with - | "[]", _ -> "[]" - | "::", [a1; a2] -> Format.asprintf "%s :: %s" (string_of_binder a1) (string_of_binder a2) - | _ -> Format.asprintf "%s(%s)" n (String.concat ", " (List.map string_of_binder args)) - -let rec string_of_term t : string = - Pretty.string_of_term (Untypehip.untype_term t) - -and string_of_staged_spec s = Pretty.string_of_staged_spec (Untypehip.untype_staged_spec s) - -and string_of_kappa (k:kappa) : string = - match k with - | EmptyHeap -> "emp" - | PointsTo (str, args) -> Format.sprintf "%s->%s" str (List.map string_of_term [args] |> String.concat ", ") - | SepConj (k1, k2) -> string_of_kappa k1 ^ "*" ^ string_of_kappa k2 - (*| MagicWand (k1, k2) -> "(" ^ string_of_kappa k1 ^ "-*" ^ string_of_kappa k2 ^ ")" *) - (* | Implication (k1, k2) -> string_of_kappa k1 ^ "-*" ^ string_of_kappa k2 *) - -and string_of_state (p, h) : string = - match h, p with - | _, True -> string_of_kappa h - | EmptyHeap, _ -> string_of_pi p - | _ -> - Format.asprintf "%s/\\%s" (string_of_kappa h) (string_of_pi p) - (* Format.asprintf "%s*%s" (string_of_kappa h) (string_of_pi p) *) - -and string_of_bin_op op = Pretty.string_of_bin_op op - -and string_of_args : 'a. ('a -> string) -> 'a list -> string = Pretty.string_of_args - -and string_of_pi pi : string = - match pi with - | True -> "T" - | False -> "F" - | Atomic (op, t1, t2) -> string_of_term t1 ^ string_of_bin_op op ^ string_of_term t2 - | And (p1, p2) -> string_of_pi p1 ^ "/\\" ^ string_of_pi p2 - | Or (p1, p2) -> string_of_pi p1 ^ "\\/" ^ string_of_pi p2 - | Imply (p1, p2) -> string_of_pi p1 ^ "=>" ^ string_of_pi p2 - | Not p -> "not(" ^ string_of_pi p ^ ")" - | Predicate (str, t) -> str ^ "(" ^ (string_of_args string_of_term t) ^ ")" - | Subsumption (a, b) -> Format.asprintf "%s <: %s" (string_of_term a) (string_of_term b) - -and string_of_try_catch_lemma (x:tryCatchLemma) : string = - let (tcl_head, tcl_handledCont, (*(h_normal, h_ops),*) tcl_summary) = x in - "TRY " - ^ - string_of_staged_spec tcl_head - - ^ (match tcl_handledCont with - | None -> "" | Some conti -> " # " ^ string_of_staged_spec conti) - - - ^ " CATCH \n" (*^ string_of_handlingcases (h_normal, h_ops ) *) - ^ "=> " ^ string_of_staged_spec tcl_summary - -and string_of_handler_type (h:handler_type) : string = - match h with - | Deep -> "d" - | Shallow -> "s" - -and string_of_core_lang (e:core_lang) :string = Pretty.string_of_core_lang (Untypehip.untype_core_lang e) - -let find_rec p_name = - object(self) - inherit [_] reduce_spec as super - method zero = false - method plus = (||) - - method! visit_HigherOrder _ f a = - self#plus (f = p_name) (super#visit_HigherOrder () f a) - - method! visit_Atomic () op a b = - match op with - | EQ -> (match (a.term_desc, b.term_desc) with - | (Var x, Var y) -> x = p_name || y = p_name - | _ -> false) - | _ -> false - end - -(**********************************************) -let string_of_existentials vs = - match vs with - | [] -> "" - | _ :: _ -> Format.asprintf "ex %s. " (String.concat "," (List.map string_of_binder vs)) - -let string_of_res b = if b then green "true" else red "false" - -let string_of_option to_s o : string = - match o with Some a -> "Some " ^ to_s a | None -> "None" - -let string_of_lemma l = - Format.asprintf "%s: forall %s, %s <: %s" l.l_name (string_of_list string_of_binder l.l_params) (string_of_staged_spec l.l_left) (string_of_staged_spec l.l_right) - -(* let string_of_time = string_of_float *) -let string_of_time = Format.asprintf "%.0f" - -let string_of_sset s = - Format.asprintf "{%s}" (String.concat ", " (SSet.elements s)) - -let string_of_smap pp s = - Format.asprintf "{%s}" (String.concat ", " (List.map (fun (k, v) -> Format.asprintf "%s -> %s" k (pp v)) (SMap.bindings s))) - -let conj xs = - match xs with - | [] -> True - | x :: xs -> List.fold_right (fun c t -> And (c, t)) xs x - -let string_of_pure_fn ({ pf_name; pf_params; pf_ret_type; pf_body } : pure_fn_def) : string = - Format.asprintf "let %s %s : %s = %s" pf_name (String.concat " " (List.map (fun (p, t) -> Format.asprintf "(%s:%s)" p (string_of_type t)) pf_params)) (string_of_type pf_ret_type) (string_of_core_lang pf_body) - -let string_of_tmap pp s = - Format.asprintf "{%s}" (String.concat ", " (List.map (fun (k, v) -> Format.asprintf "%s -> %s" (string_of_type k) (pp v)) (TMap.bindings s))) - -let string_of_abs_env t = Pretty.string_of_abs_env t - (* "" *) - -let string_of_typ_env t = - Format.asprintf "%s" (string_of_smap string_of_type t) - - -let string_of_quantified to_s (vs, e) = - match vs with - | [] -> to_s e - | _ :: _ -> Format.asprintf "ex %s. %s" (String.concat " " vs) (to_s e) - -let string_of_instantiations pv kvs = - List.map (fun (k, v) -> Format.asprintf "%s := %s" k (pv v)) kvs - |> String.concat ", " |> Format.asprintf "[%s]" - -let string_of_bindings = string_of_instantiations - -let string_of_meth_def m = - Format.asprintf "let rec %s %s\n%s=\n%s" m.m_name - (match m.m_params with | [] -> "()" | _ -> String.concat " " (List.map string_of_binder m.m_params)) - ((match m.m_spec with None -> "" | Some s -> s |> string_of_staged_spec |> (Format.asprintf "(*@@ %s @@*)\n"))) - (string_of_core_lang m.m_body) - -let string_of_program (cp:core_program) :string = - List.map string_of_meth_def cp.cp_methods |> String.concat "\n\n" - -let string_of_pattern p = Pretty.string_of_pattern (Untypehip.untype_pattern p) - -(* make these declarations available here as well *) -let string_of_type_declaration tdecl = Pretty.string_of_type_declaration tdecl - -let string_of_pred pred_def = Pretty.string_of_pred (Untypehip.untype_pred_def pred_def) - -let string_of_bin_term_op = Pretty.string_of_bin_term_op - -let string_of_constant = Pretty.string_of_constant - -module With_types = struct - let rec string_of_term t : string = - let term_str = match t.term_desc with - | Const c -> string_of_constant c - | BinOp (op, lhs, rhs) -> Format.asprintf "(%s %s %s)" (string_of_term lhs) (string_of_bin_term_op op) (string_of_term rhs) - | TNot a -> Format.asprintf "not(%s)" (string_of_term a) - | Var str -> str - | Rel (bop, t1, t2) -> - "(" ^ string_of_term t1 ^ (match bop with | EQ -> "==" | _ -> string_of_bin_op bop) ^ string_of_term t2 ^ ")" - | TApp (op, args) -> Format.asprintf "%s%s" op (string_of_args string_of_term args) - | Construct (name, args) -> Format.asprintf "%s%s" name (string_of_args string_of_term args) - | TLambda (_name, params, sp, body) -> - let body = - match body with - | None -> "" - | Some b -> Format.asprintf "-> %s" (string_of_core_lang b) - in - let param_list = params |> List.map string_of_binder |> String.concat " " in - Format.asprintf "(fun %s (*@@ %s @@*) %s)" param_list (Option.map string_of_staged_spec sp |> Option.value ~default:"") body - | TTuple nLi -> - let rec helper li = - match li with - | [] -> "" - | [x] -> string_of_term x - | x:: xs -> string_of_term x ^","^ helper xs - in "(" ^ helper nLi ^ ")" +type 'a fmt = Format.formatter -> 'a -> unit + +let pp_sep_comma ppf () = Format.fprintf ppf ",@ " +let pp_space ppf () = Format.fprintf ppf " " +let pp_call_like : 'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> string -> 'a list -> unit = + fun pp_arg ppf name args -> + let open Format in + fprintf ppf "%s(%a)" + name + (pp_print_list ~pp_sep:pp_space pp_arg) args + +(* we use records-as-objects instead of classes to make it easier + to dynamically stack modifications *) +type pretty_printer = { + pp_typ : pretty_printer -> typ fmt; + pp_binder : pretty_printer -> binder fmt; + pp_bin_op : pretty_printer -> bin_rel_op fmt; + pp_bin_term_op : pretty_printer -> bin_term_op fmt; + pp_constant : pretty_printer -> const fmt; + pp_lambda_like : pretty_printer -> (binder list * staged_spec option * core_lang option) fmt; + pp_term : pretty_printer -> term fmt; + pp_core_lang : pretty_printer -> core_lang fmt; + pp_staged_spec : pretty_printer -> staged_spec fmt; + pp_kappa : pretty_printer -> kappa fmt; + pp_pi : pretty_printer -> pi fmt; + pp_state : pretty_printer -> state fmt; + pp_pattern : pretty_printer -> pattern fmt; +} + +let default_printer = { + pp_typ = begin fun self ppf t -> + let open Types in + let open Format in + match t with + | Any -> pp_print_string ppf "" + | TyString -> pp_print_string ppf "string" + | Int -> pp_print_string ppf "int" + | Unit -> pp_print_string ppf "unit" + | TConstr (name, args) -> + if List.is_empty args + then pp_print_string ppf name + else Format.fprintf ppf "(%a) %s" + (pp_print_list ~pp_sep:pp_sep_comma (self.pp_typ self)) args + name + | Bool -> pp_print_string ppf "bool" + | Lamb -> pp_print_string ppf "lambda" + | TVar v -> Format.fprintf ppf "'%s" v + | Arrow (t1, t2) -> Format.fprintf ppf "%a->%a" (self.pp_typ self) t1 (self.pp_typ self) t2 + end; + pp_binder = begin fun _ ppf binder -> + Format.pp_print_string ppf (ident_of_binder binder) + end; + pp_bin_op = begin + fun _ ppf op -> + let s = match op with + | GT -> ">" + | LT -> "<" + | EQ -> "=" + | GTEQ -> ">=" + | LTEQ -> "<=" in - "(" ^ term_str ^ " : " ^ (string_of_type t.term_type) ^ ")" - and string_of_pi pi : string = - match pi with - | True -> "T" - | False -> "F" - | Atomic (op, t1, t2) -> string_of_term t1 ^ string_of_bin_op op ^ string_of_term t2 - | And (p1, p2) -> string_of_pi p1 ^ "/\\" ^ string_of_pi p2 - | Or (p1, p2) -> string_of_pi p1 ^ "\\/" ^ string_of_pi p2 - | Imply (p1, p2) -> string_of_pi p1 ^ "=>" ^ string_of_pi p2 - | Not p -> "not(" ^ string_of_pi p ^ ")" - | Predicate (str, t) -> str ^ "(" ^ (string_of_args string_of_term t) ^ ")" - | Subsumption (a, b) -> Format.asprintf "%s <: %s" (string_of_term a) (string_of_term b) - and string_of_kappa (k:kappa) : string = - match k with - | EmptyHeap -> "emp" - | PointsTo (str, args) -> Format.sprintf "%s->%s" str (List.map string_of_term [args] |> String.concat ", ") - | SepConj (k1, k2) -> string_of_kappa k1 ^ "*" ^ string_of_kappa k2 - and string_of_core_lang e = - match e.core_desc with - | CValue v -> string_of_term v - | CLet (v, e, e1) -> Format.sprintf "let %s = %s in\n%s" (string_of_binder v) (string_of_core_lang e) (string_of_core_lang e1) | CSequence (e1, e2) -> Format.sprintf "%s;\n%s" (string_of_core_lang e1) (string_of_core_lang e2) - | CIfElse (pi, t, e) -> Format.sprintf "if %s then %s else (%s)" (string_of_pi pi) (string_of_core_lang t) (string_of_core_lang e) - | CFunCall (f, [a; b]) when not (Pretty.is_alpha (String.get f 0)) -> Format.sprintf "%s %s %s" (string_of_term a) f (string_of_term b) - | CFunCall (f, xs) -> Format.sprintf "%s %s" f (List.map string_of_term xs |> String.concat " ") - | CWrite (v, e) -> Format.sprintf "%s := %s" v (string_of_term e) - | CRef v -> Format.sprintf "ref %s" (string_of_term v) - | CRead v -> Format.sprintf "!%s" v - | CAssert (p, h) -> Format.sprintf "assert (%s && %s)" (string_of_pi p) (string_of_kappa h) - | CPerform (eff, Some arg) -> Format.sprintf "perform %s %s" eff (string_of_term arg) - | CPerform (eff, None) -> Format.sprintf "perform %s" eff - | CMatch (typ, spec, e, hs, cs) -> Format.sprintf "match[%s] %s%s with\n%s%s" - (string_of_handler_type typ) - (Option.map string_of_try_catch_lemma spec |> Option.value ~default:"") - (string_of_core_lang e) - (match hs with | [] -> "" | _ :: _ -> string_of_core_handler_ops hs ^ "\n") - (match cs with [] -> "" | _ :: _ -> string_of_constr_cases cs) - | CResume tList -> Format.sprintf "continue %s" (List.map string_of_term tList |> String.concat " ") - | CLambda (xs, spec, e) -> Format.sprintf "fun %s%s -> %s" (xs |> List.map string_of_binder |> List.map (fun s -> "(" ^ s ^ ")") |> String.concat " ") - (match spec with None -> "" | Some ds -> Format.asprintf " (*@@ %s @@*)" (string_of_staged_spec ds)) (string_of_core_lang e) - | CShift (b, k, e) -> Format.sprintf "Shift%s %s -> %s" (if b then "" else "0") (string_of_binder k) (string_of_core_lang e) - | CReset (e) -> Format.sprintf "<%s>" (string_of_core_lang e) - and string_of_constr_cases cs = - cs - |> List.map (fun case -> Format.asprintf "| %s%s -> %s" - (string_of_pattern case.ccase_pat) - (match case.ccase_guard with - | None -> "" - | Some guard -> Format.asprintf " when %s" (string_of_term guard)) - (string_of_core_lang case.ccase_expr)) - |> String.concat "\n" - - and string_of_core_handler_ops hs = - List.map (fun (name, v, spec, body) -> - let spec = spec |> Option.map (fun s -> Format.asprintf " (*@@ %s @@*)" (string_of_staged_spec s)) |> Option.value ~default:"" in - Format.asprintf "| effect %s k%s -> %s" - (match v with None -> name | Some v -> Format.asprintf "(%s %s)" name v) spec (string_of_core_lang body)) hs |> String.concat "\n" - and string_of_state (p, h) : string = - match h, p with - | _, True -> string_of_kappa h - | EmptyHeap, _ -> string_of_pi p - | _ -> - Format.asprintf "%s/\\%s" (string_of_kappa h) (string_of_pi p) - and string_of_staged_spec (st:staged_spec) : string = - match st with - | Shift (nz, k, spec, x, cont) -> - (* TODO: shiftc *) - let zero = if nz then "" else "0" in - let cont_s = match cont with - | NormalReturn (Atomic (EQ, {term_desc = Var "res"; _}, {term_desc = Var y; _}), EmptyHeap) when (ident_of_binder x) = y -> "" - | _ -> Format.asprintf ", %s. %s" (string_of_binder x) (string_of_staged_spec cont) - in - Format.asprintf "shift%s(%s. %s%s)" zero (string_of_binder k) (string_of_staged_spec spec) cont_s - | Reset spec -> - Format.asprintf "reset(%s)" (string_of_staged_spec spec) - | Require (p, h) -> - Format.asprintf "req %s" (string_of_state (p, h)) - | HigherOrder (f, args) -> - Format.asprintf "%s(%s)" f (String.concat ", " (List.map string_of_term args)) - | NormalReturn (pi, heap) -> - Format.asprintf "ens %s" (string_of_state (pi, heap)) - | RaisingEff (pi, heap, (name, args), ret) -> - - Format.asprintf "%s(%s, %s, %s)" name (string_of_state (pi, heap)) (string_of_args string_of_term args) (string_of_term ret) - | Exists (vs, spec) -> - Format.asprintf "ex %s. (%s)" (string_of_binder vs) (string_of_staged_spec spec) - | ForAll (vs, spec) -> - Format.asprintf "forall %s. (%s)" (string_of_binder vs) (string_of_staged_spec spec) - (* | IndPred {name; args} -> *) - (* Format.asprintf "%s(%s)" name (String.concat " " (List.map string_of_term args)) *) - | TryCatch (pi, h, ( src, ((normP, normSpec), ops)), ret) -> - let string_of_normal_case = normP ^ ": " ^ string_of_staged_spec (normSpec) in - let string_of_eff_case (eName, param, eSpec)= eName ^ - (match param with | None -> " " | Some p -> "("^ p ^ ") ")^ ": " ^ string_of_staged_spec eSpec in - let string_of_eff_cases ops = List.fold_left (fun acc a -> acc ^ ";\n" ^string_of_eff_case a) "" ops in - Format.asprintf "ens %s; \n(TRY \n(%s)\nCATCH \n{%s%s}[%s])\n" (string_of_state (pi, h)) (string_of_staged_spec src) (string_of_normal_case) (string_of_eff_cases ops) (string_of_term ret) - | Sequence (s1, s2) -> Format.sprintf "%s; %s" (string_of_staged_spec s1) (string_of_staged_spec s2) - | Bind (v, expr, body) -> Format.sprintf "let %s = (%s) in (%s)" (string_of_binder v) (string_of_staged_spec expr) (string_of_staged_spec body) - | Disjunction (lhs, rhs) -> Format.sprintf "(%s) \\/ (%s)" (string_of_staged_spec lhs) (string_of_staged_spec rhs) - and string_of_pattern (p : pattern) : string = - let desc = match p.pattern_desc with - | PAny -> "_" - | PVar s -> (ident_of_binder s) - | PConstr (name, args) -> Format.sprintf "%s(%s)" name (List.map string_of_pattern args |> String.concat ", ") - | PConstant c -> Format.sprintf "%s" (string_of_constant c) - | PAlias (p, s) -> Format.sprintf "(%s) as %s" (string_of_pattern p) s + Format.pp_print_string ppf s + end; + pp_bin_term_op = begin + fun _ ppf op -> + let s = match op with + | Plus -> "+" + | Minus -> "-" + | SConcat -> "++" + | TAnd -> "&&" + | TPower -> "^" + | TTimes -> "*" + | TDiv -> "/" + | TOr -> "||" + | TCons -> "::" in - Format.sprintf "%s : %s" desc (string_of_type p.pattern_type) - - let string_of_pred ({p_name; p_params; p_body; _}) = - Format.asprintf "%s(%s) == %s" p_name (p_params |> List.map string_of_binder |> String.concat ", ") (string_of_staged_spec p_body) + Format.pp_print_string ppf s + end; + pp_constant = begin + fun _ ppf c -> + let open Format in + match c with + | ValUnit -> pp_print_string ppf "()" + | Num n -> pp_print_int ppf n + | TStr s -> pp_print_string ppf ("\"" ^ s ^ "\"") + | Nil -> pp_print_string ppf "[]" + | TTrue -> pp_print_string ppf "true" + | TFalse -> pp_print_string ppf "false" + end; + pp_lambda_like = begin + fun self ppf (params, spec, body) -> + let open Format in + fprintf ppf "(fun %a (*@@ %a @@*) %a)" + (pp_print_list ~pp_sep:pp_sep_comma (self.pp_binder self)) params + (pp_print_option (self.pp_staged_spec self)) spec + (pp_print_option (fun ppf body -> fprintf ppf "-> %a" (self.pp_core_lang self) body)) body + end; + pp_term = begin + fun self ppf t -> + let open Format in + match t.term_desc with + | Const c -> self.pp_constant self ppf c + | BinOp (op, lhs, rhs) -> fprintf ppf "(%a %a %a)" (self.pp_term self) lhs (self.pp_bin_term_op self) op (self.pp_term self) rhs + | TNot a -> fprintf ppf "not(%a)" (self.pp_term self) a + | Var str -> pp_print_string ppf str + | Rel (bop, t1, t2) -> fprintf ppf "(%a %a %a)" (self.pp_term self) t1 (self.pp_bin_op self) bop (self.pp_term self) t2 + | Construct (op, args) | TApp (op, args) -> pp_call_like (self.pp_term self) ppf op args + | TTuple elems + -> fprintf ppf "(%a)" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",") (self.pp_term self)) elems + | TLambda (_, params, spec, body) -> (self.pp_lambda_like self) ppf (params, spec, body) + end; + pp_pattern = begin + fun self ppf pat -> + match pat.pattern_desc with + | PAny -> Format.pp_print_string ppf "_" + | PVar v -> Format.fprintf ppf "@[%s@]" (fst v) + | PConstr (name, args) -> pp_call_like (self.pp_pattern self) ppf name args + | PConstant c -> (self.pp_constant self) ppf c + | PAlias (p, s) -> Format.fprintf ppf "@[%a@ as@ %s@]" (self.pp_pattern self) p s + end; + pp_core_lang = begin + fun self ppf core -> + let open Format in + match core.core_desc with + | CValue v -> fprintf ppf "@[%a@]" (self.pp_term self) v + | CLet (v, e1, e2) -> + fprintf ppf "@[let@ %a@ =@ @[%a@]@;in@ @[(%a)@]@]" + (self.pp_binder self) v + (self.pp_core_lang self) e1 + (self.pp_core_lang self) e2 + | CSequence (e1, e2) -> + fprintf ppf "@[%a;@ %a@]" + (self.pp_core_lang self) e1 + (self.pp_core_lang self) e2 + | CIfElse (pi, t, e) -> fprintf ppf "@[if@ %a@ then@ @[%a@]@ else@ @[%a@]@]" + (self.pp_pi self) pi (self.pp_core_lang self) t (self.pp_core_lang self) e + | CFunCall (f, xs) -> pp_call_like (self.pp_term self) ppf f xs + | CWrite (v, e) -> fprintf ppf "@[%s@ :=@ %a@]" v (self.pp_term self) e + | CRef v -> fprintf ppf "@[ref@ %a@]" (self.pp_term self) v + | CRead v -> fprintf ppf "@[!%s]" v + | CAssert (p, h) -> fprintf ppf "@[assert@ (@[%a@ /\\@ %a@])@]" + (self.pp_pi self) p (self.pp_kappa self) h + | CPerform (eff, arg) -> + fprintf ppf "@[perform@ %s@ %a@]" eff (pp_print_option (self.pp_term self)) arg + | CMatch (typ, spec, e, hs, cs) -> + let pp_core_handler_ops = + let pp_handler ppf (name, v, spec, body) = + fprintf ppf "|@ %a@ k@ %a@ ->@ %a@]" + (fun ppf (name, v) -> match v with + | None -> pp_print_string ppf name + | Some v -> fprintf ppf "(%s@ %s)" name v) (name, v) + (pp_print_option (self.pp_staged_spec self)) spec + (self.pp_core_lang self) body + in + pp_print_list pp_handler + in + let pp_handler_type ppf h = + match h with + | Deep -> pp_print_string ppf "d" + | Shallow -> pp_print_string ppf "s" + in + let pp_constr_case ppf case = + Format.(fprintf ppf "@[@ |@ %a%a@ ->@ %a@]" + (self.pp_pattern self) case.ccase_pat + (pp_print_option (self.pp_term self)) case.ccase_guard + (self.pp_core_lang self) case.ccase_expr) + in + let pp_constr_cases ppf cases = + let open Format in + pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "@,") pp_constr_case ppf cases + in + let pp_placeholder s = fun ppf _ -> pp_print_string ppf s in + let pp_try_catch_lemma = pp_placeholder "[try-catch lemma]" in + fprintf ppf "@[match[%a]@ (%a)@ with@,%a@,%a@,%a@]" + pp_handler_type typ + (pp_print_option pp_try_catch_lemma) spec + (self.pp_core_lang self) e + pp_core_handler_ops hs + pp_constr_cases cs + | CResume args -> fprintf ppf "@[continue@ %a@]" (pp_print_list (self.pp_term self)) args + | CLambda (xs, spec, e) -> (self.pp_lambda_like self) ppf (xs, spec, Some e) + | CShift (b, k, e) -> fprintf ppf "@[%s@ %a@ ->@ %a@]" + (if b then "Shift" else "Shift0") + (self.pp_binder self) k + (self.pp_core_lang self) e + | CReset e -> fprintf ppf "@[@<%a@>@]" (self.pp_core_lang self) e + end; + pp_staged_spec = begin + fun self ppf f -> + let open Format in + match f with + | Exists (v, spec) -> + fprintf ppf "@[ex@ %a.@ @[%a@]@]" + (self.pp_binder self) v + (self.pp_staged_spec self) spec + | ForAll (v, spec) -> + fprintf ppf "@[ex@ %a.@ @[%a@]@]" + (self.pp_binder self) v + (self.pp_staged_spec self) spec + | Require (p, k) -> + fprintf ppf "@[req@ (@[%a@ /\\@ %a@])@]" + (self.pp_pi self) p (self.pp_kappa self) k + | NormalReturn (p, k) -> + fprintf ppf "@[ens@ (@[%a@ /\\@ %a@])@]" + (self.pp_pi self) p (self.pp_kappa self) k + | HigherOrder (f, args) -> pp_call_like (self.pp_term self) ppf f args + | Shift (z, k, spec, _x, _cont) -> + fprintf ppf "@[%s(@[%a.@ %a@])@]" + (if z then "sh" else "sh0") + (self.pp_binder self) k + (self.pp_staged_spec self) spec + | Reset spec -> + fprintf ppf "@[%s(@[%a@])@]" + "rs" + (self.pp_staged_spec self) spec + | Sequence (s1, s2) -> + fprintf ppf "@[(%a;@ %a)@]" + (self.pp_staged_spec self) s1 + (self.pp_staged_spec self) s2 + | Bind (v, s1, s2) -> + fprintf ppf "@[let@ %a@ =@ @[%a@]@ in@ @[(%a)@]@]" + (self.pp_binder self) v + (self.pp_staged_spec self) s1 + (self.pp_staged_spec self) s2 + | Disjunction (s1, s2) -> + fprintf ppf "@[(%a@ \\/@ %a@]" + (self.pp_staged_spec self) s1 + (self.pp_staged_spec self) s2 + (* TODO *) + | RaisingEff _ -> pp_print_string ppf "[effect stage]" + | TryCatch _ -> pp_print_string ppf "[trycatch stage]" + end; + pp_pi = begin + fun self ppf p -> + let open Format in + match p with + | True -> fprintf ppf "true" + | False -> fprintf ppf "false" + | And (p1, p2) -> fprintf ppf "@[%a@ /\\@ %a@]" + (self.pp_pi self) p1 (self.pp_pi self) p2 + | Or (p1, p2) -> fprintf ppf "@[%a@ \\/@ %a@]" + (self.pp_pi self) p1 (self.pp_pi self) p2 + | Not p -> fprintf ppf "@[~(%a)@]" + (self.pp_pi self) p + | Imply (p1, p2) -> fprintf ppf "@[(%a)@]@ =>@ @[(%a)@]" + (self.pp_pi self) p1 (self.pp_pi self) p2 + | Predicate (name, args) -> pp_call_like (self.pp_term self) ppf name args + | Subsumption (t1, t2) -> fprintf ppf "@[(%a)@]@ <:@ @[(%a)@]" + (self.pp_term self) t1 (self.pp_term self) t2 + | Atomic (rel, t1, t2) -> fprintf ppf "@[(%a@ %a@ %a)@]" + (self.pp_term self) t1 (self.pp_bin_op self) rel (self.pp_term self) t2 + end; + pp_kappa = begin + fun self ppf k -> + let open Format in + match k with + | EmptyHeap -> fprintf ppf "emp" + | PointsTo (loc, t) -> fprintf ppf "@[%s@ ->@ @[(%a)@]@]" loc (self.pp_term self) t + | SepConj (k1, k2) -> fprintf ppf "@[(%a)@]@ *@ @[(%a)@]" + (self.pp_kappa self) k1 (self.pp_kappa self) k2 + end; + pp_state = begin + fun self ppf (p, k) -> + Format.fprintf ppf "(%a@ /\\@ %a)" (self.pp_kappa self) k (self.pp_pi self) p + end +} + +let add_type_annotations (pp : pretty_printer) : pretty_printer = +(* TODO add annotations to terms, patterns, core lang, etc.. *) + { pp with + pp_binder = + fun self ppf b -> + Format.fprintf ppf "(%s : %a)" + (ident_of_binder b) + (self.pp_typ self) (type_of_binder b)} + +type config = { + cfg_print_types : bool; + cfg_print_spacing : bool +} + +let default_config () = { + cfg_print_types = false; + cfg_print_spacing = true +} + +let set_single_line ?(enabled = true) cfg = {cfg with cfg_print_spacing = not enabled} +let set_types_display ?(enabled = true) cfg = {cfg with cfg_print_types = enabled} + +let pp_with_config cfg pp = + let pp = + if cfg.cfg_print_types + then add_type_annotations pp + else pp + in + pp + +let with_changed_out_functions ppf wrapper f = + let out_functions = Format.pp_get_formatter_out_functions ppf () in + Format.pp_set_formatter_out_functions ppf (wrapper out_functions); + let result = f ppf in + Format.pp_set_formatter_out_functions ppf out_functions; + result + +let with_compact_spacing out_functions = + let do_nothing _ = () in + Format.{ + out_functions with + out_newline = do_nothing; + out_indent = (fun _ -> out_functions.out_indent 1); + out_spaces = (fun _ -> out_functions.out_spaces 1); +} + +let format_with_config ppf cfg f = + if cfg.cfg_print_spacing + then f ppf + else + let@ ppf = with_changed_out_functions ppf with_compact_spacing in + f ppf + +(* We define a separate internal module type for printers, so that + the string_of functions can still derive from [obtain_printers_internal], + while still exposing only the Printers type and the [obtain_printers] function + to the outside. *) + +module type Printers_internal = sig + val pp_staged_spec : staged_spec fmt + val pp_binder : binder fmt + val pp_typ : typ fmt + val pp_term : term fmt + val pp_pi : pi fmt + val pp_kappa : kappa fmt + val pp_state : state fmt + val pp_pattern : pattern fmt + val pp_core_lang : core_lang fmt end -(** formatters, more fit for external output *) - -let pp_bin_op ppf op = - Format.fprintf ppf "%s" (string_of_bin_op op) - -let pp_binder ppf (str, typ) = - Format.fprintf ppf "%s@ :@ %s" str (string_of_type typ) - -let pp_bin_term_op ppf op = - Format.fprintf ppf "%s" (string_of_bin_term_op op) - -let pp_constant ppf c = - Format.fprintf ppf "%s" (string_of_constant c) +module type Printers = sig + val pp_staged_spec : Format.formatter -> staged_spec -> unit +end -let rec pp_term ppf t = - let open Format in - match t.term_desc with - | Const c -> fprintf ppf "%a" pp_constant c - | BinOp (op, lhs, rhs) -> fprintf ppf "@[(%a@ %a@ %a)@]" - pp_term lhs pp_bin_term_op op pp_term rhs - | Rel (op, lhs, rhs) -> fprintf ppf "@[(%a@ %a@ %a)@]" - pp_term lhs pp_bin_op op pp_term rhs - | TNot t -> fprintf ppf "@[~(%a)@]" pp_term t - | Var v -> fprintf ppf "%s" v - | TApp (op, args) -> pp_call_like pp_term ppf (op, args) - | Construct (name, args) -> pp_call_like pp_term ppf (name, args) - | TLambda (_name, params, sp, body) -> pp_lambda_like ppf (params, sp, body) - (* | TList args -> - fprintf ppf "[@[%a@]]" - (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";@ ") pp_term) args *) - | TTuple args -> - fprintf ppf "(@[%a@])" - (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",@ ") pp_term) args -and pp_call_like : 'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> string * 'a list -> unit - = fun pp_arg ppf (f, args) -> - let open Format in - fprintf ppf "@[%s(@[%a@])@]" f - (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",@ ") pp_arg) args -and pp_lambda_like ppf (params, spec, body) = - let open Format in - fprintf ppf "@[(fun@ %a@ @[@ (*@@@ %a@ @@*)@ %a@])@]" - (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",@ ") pp_binder) params - (pp_print_option pp_staged_spec) spec - (pp_print_option (fun ppf body -> fprintf ppf "@ ->@ %a" pp_core_lang body)) body -and pp_pi ppf p = - let open Format in - match p with - | True -> fprintf ppf "true" - | False -> fprintf ppf "false" - | And (p1, p2) -> fprintf ppf "@[%a@ /\\@ %a@]" - pp_pi p1 pp_pi p2 - | Or (p1, p2) -> fprintf ppf "@[%a@ \\/@ %a@]" - pp_pi p1 pp_pi p2 - | Not p -> fprintf ppf "@[~(%a)@]" - pp_pi p - | Imply (p1, p2) -> fprintf ppf "@[(%a)@]@ =>@ @[(%a)@]" - pp_pi p1 pp_pi p2 - | Predicate (name, args) -> pp_call_like pp_term ppf (name, args) - | Subsumption (t1, t2) -> fprintf ppf "@[(%a)@]@ <:@ @[(%a)@]" - pp_term t1 pp_term t2 - | Atomic (rel, t1, t2) -> fprintf ppf "@[(%a@ %a@ %a)@]" - pp_term t1 pp_bin_op rel pp_term t2 -and pp_kappa ppf k = +let cast_from_internal (module M : Printers_internal) : (module Printers) = + (module struct + let pp_staged_spec = M.pp_staged_spec + end) + +let obtain_printers_internal cfg : (module Printers_internal) = + let pp = pp_with_config cfg default_printer in + (module struct + let pp_staged_spec ppf f = + let@ ppf = format_with_config ppf cfg in + pp.pp_staged_spec pp ppf f + let pp_binder ppf f = + let@ ppf = format_with_config ppf cfg in + pp.pp_binder pp ppf f + let pp_typ ppf t = + let@ ppf = format_with_config ppf cfg in + pp.pp_typ pp ppf t + let pp_term ppf t = + let@ ppf = format_with_config ppf cfg in + pp.pp_term pp ppf t + let pp_pi ppf p = + let@ ppf = format_with_config ppf cfg in + pp.pp_pi pp ppf p + let pp_kappa ppf k = + let@ ppf = format_with_config ppf cfg in + pp.pp_kappa pp ppf k + let pp_state ppf st = + let@ ppf = format_with_config ppf cfg in + pp.pp_state pp ppf st + let pp_pattern ppf pat = + let@ ppf = format_with_config ppf cfg in + pp.pp_pattern pp ppf pat + let pp_core_lang ppf core = + let@ ppf = format_with_config ppf cfg in + pp.pp_core_lang pp ppf core + end) + +let obtain_printers cfg = cast_from_internal (obtain_printers_internal cfg) + +module Default_internal = (val obtain_printers_internal (default_config ()) : Printers_internal) +module Default = (val obtain_printers (default_config ()) : Printers) + +let string_of_binder ?(config = default_config ()) b = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_binder b + +let string_of_type ?(config = default_config ()) t = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_typ t + +let string_of_pi ?(config = default_config ()) p = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_pi p + +let string_of_kappa ?(config = default_config ()) k = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_kappa k + +let string_of_state ?(config = default_config ()) st = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_state st + +let string_of_pattern ?(config = default_config ()) pat = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_pattern pat + +let string_of_term ?(config = default_config ()) t = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_term t + +let string_of_core_lang ?(config = default_config ()) core = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_core_lang core + +let string_of_staged_spec ?(config = default_config ()) f = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%a" M.pp_staged_spec f + +let string_of_option ?(none = "") some opt = + match opt with + | Some v -> some v + | None -> none + +let string_of_list ?(sep=", ") pp elems = + List.map pp elems |> String.concat sep + +let string_of_pred ?(config = default_config ()) pred = + let module M = (val obtain_printers_internal config : Printers_internal) in + Format.asprintf "%s(%s)@, =@ %a" pred.p_name (string_of_list (string_of_binder ~config) pred.p_params) M.pp_staged_spec pred.p_body + +let string_of_type_declaration ?(config = default_config ()) tdecl = + let module M = (val obtain_printers_internal config : Printers_internal) in let open Format in - match k with - | EmptyHeap -> fprintf ppf "emp" - | PointsTo (loc, t) -> fprintf ppf "@[%s@ ->@ @[(%a)@]@]" loc pp_term t - | SepConj (k1, k2) -> fprintf ppf "@[(%a)@]@ *@ @[(%a)@]" - pp_kappa k1 pp_kappa k2 -and pp_staged_spec ppf spec = - let open Format in - match spec with - | Exists (v, spec) -> - fprintf ppf "@[ex@ %a.@ @[%a@]@]" - pp_binder v - pp_staged_spec spec - | Require (p, k) -> - fprintf ppf "@[req@ (@[%a@ /\\@ %a@])@]" - pp_pi p pp_kappa k - | NormalReturn (p, k) -> - fprintf ppf "@[ens@ (@[%a@ /\\@ %a@])@]" - pp_pi p pp_kappa k - | HigherOrder (f, args) -> pp_call_like pp_term ppf (f, args) - | Shift (z, k, spec, _x, _cont) -> - fprintf ppf "@[%s(@[%a.@ %a@])@]" - (if z then "sh" else "sh0") - pp_binder k - pp_staged_spec spec - | Reset spec -> - fprintf ppf "@[%s(@[%a@])@]" - "rs" - pp_staged_spec spec - | Sequence (s1, s2) -> - fprintf ppf "@[(%a;@ %a)@]" - pp_staged_spec s1 - pp_staged_spec s2 - | Bind (v, s1, s2) -> - fprintf ppf "@[let@ %a@ =@ @[%a@]@ in@ @[(%a)@]@]" - pp_binder v - pp_staged_spec s1 - pp_staged_spec s2 - | Disjunction (s1, s2) -> - fprintf ppf "@[(%a@ \\/@ %a@]" - pp_staged_spec s1 - pp_staged_spec s2 - (* the remaining cases are effect-related, no need to prettify for now *) -| s -> pp_print_string ppf (string_of_staged_spec s) -and pp_try_catch_lemma ppf (head, cont, summary) = - Format.(fprintf ppf "@[TRY@ %a@ %a@ =>@ %a@]" - pp_staged_spec head - (pp_print_option (fun ppf spec -> fprintf ppf "#@ %a" pp_staged_spec spec)) cont - pp_staged_spec summary) -and pp_pattern ppf pat = - match pat.pattern_desc with - | PAny -> Format.pp_print_string ppf "_" - | PVar v -> Format.fprintf ppf "@[%s@]" (fst v) - | PConstr (name, args) -> pp_call_like pp_pattern ppf (name, args) - | PConstant c -> pp_constant ppf c - | PAlias (p, s) -> Format.fprintf ppf "@[%a@ as@ %s@]" pp_pattern p s -and pp_constr_case ppf case = - Format.(fprintf ppf "@[@ |@ %a%a@ ->@ %a@]" - pp_pattern case.ccase_pat - (pp_print_option pp_term) case.ccase_guard - pp_core_lang case.ccase_expr) -and pp_constr_cases ppf cases = - let open Format in - pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "@,") pp_constr_case ppf cases -and pp_core_lang ppf core = - let open Format in - match core.core_desc with - | CValue v -> fprintf ppf "@[%a@]" pp_term v - | CLet (v, e1, e2) -> - fprintf ppf "@[let@ %a@ =@ @[%a@]@;in@ @[(%a)@]@]" - pp_binder v - pp_core_lang e1 - pp_core_lang e2 - | CSequence (e1, e2) -> - fprintf ppf "@[%a;@ %a@]" - pp_core_lang e1 - pp_core_lang e2 - | CIfElse (pi, t, e) -> fprintf ppf "@[if@ %a@ then@ @[%a@]@ else@ @[%a@]@]" - pp_pi pi pp_core_lang t pp_core_lang e - | CFunCall (f, xs) -> pp_call_like pp_term ppf (f, xs) - | CWrite (v, e) -> fprintf ppf "@[%s@ :=@ %a@]" v pp_term e - | CRef v -> fprintf ppf "@[ref@ %a@]" pp_term v - | CRead v -> fprintf ppf "@[!%s]" v - | CAssert (p, h) -> fprintf ppf "@[assert@ (@[%a@ /\\@ %a@])@]" - pp_pi p pp_kappa h - | CPerform (eff, arg) -> - fprintf ppf "@[perform@ %s@ %a@]" eff (pp_print_option pp_term) arg - | CMatch (typ, spec, e, hs, cs) -> - let pp_core_handler_ops = - let pp_handler ppf (name, v, spec, body) = - fprintf ppf "|@ %a@ k@ %a@ ->@ %a@]" - (fun ppf (name, v) -> match v with - | None -> pp_print_string ppf name - | Some v -> fprintf ppf "(%s@ %s)" name v) (name, v) - (pp_print_option pp_staged_spec) spec - pp_core_lang body - in - pp_print_list pp_handler - in - fprintf ppf "@[match[%s]@ (%a)@ with@,%a@,%a@,%a@]" - (string_of_handler_type typ) - (pp_print_option pp_try_catch_lemma) spec - pp_core_lang e - pp_core_handler_ops hs - pp_constr_cases cs - | CResume args -> fprintf ppf "@[continue@ %a@]" (pp_print_list pp_term) args - | CLambda (xs, spec, e) -> pp_lambda_like ppf (xs, spec, Some e) - | CShift (b, k, e) -> fprintf ppf "@[%s@ %a@ ->@ %a@]" - (if b then "Shift" else "Shift0") - pp_binder k - pp_core_lang e - | CReset e -> fprintf ppf "@[<%a>@]" pp_core_lang e + let pp_inductive ppf constrs = + let pp_constr ppf (name, arg_types) = + if List.is_empty arg_types + then fprintf ppf "@[| %s@]" name + else fprintf ppf "@[| %s of@ %a@]" name + (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf "@ * ") M.pp_typ) arg_types + in + pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf "@,") pp_constr ppf constrs + in + let pp_record ppf _r = pp_print_string ppf "record" in + let pp_kind ppf kind = + match kind with + | Tdecl_inductive constrs -> pp_inductive ppf constrs + | Tdecl_record r -> pp_record ppf r + in + Format.asprintf "type@ (%s)@ %s@ =@,@[%a@]" (string_of_list (string_of_type ~config) tdecl.tdecl_params) + tdecl.tdecl_name + pp_kind tdecl.tdecl_kind + +let pp_assoc_list pp_key pp_value ppf m = + let pp_element ppf (k, v) = + Format.fprintf ppf "@[%a -> %a@]" pp_key k pp_value v + in + Format.fprintf ppf "@[{%a}@]" (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ") pp_element) m + +let string_of_abs_env ?(config = default_config ()) abs_env = + let module M = (val obtain_printers_internal config : Printers_internal) in + let variable_types = abs_env.vartypes |> SMap.bindings in + let type_eqs = (TMap.map (fun t -> U.get t) !(abs_env.equalities)) |> TMap.bindings in + Format.asprintf "@[vars:@ %a,@ eqs:@ %a@]" (pp_assoc_list Format.pp_print_string M.pp_typ) variable_types (pp_assoc_list M.pp_typ M.pp_typ) type_eqs + diff --git a/lib/hipcore_typed/Pretty.mli b/lib/hipcore_typed/Pretty.mli new file mode 100644 index 00000000..9a7b89a6 --- /dev/null +++ b/lib/hipcore_typed/Pretty.mli @@ -0,0 +1,54 @@ +open Typedhip + +(** { 1 Pretty-printer configuration } *) + +type config + +val default_config : unit -> config + +val set_single_line : ?enabled:bool -> config -> config + +val set_types_display : ?enabled:bool -> config -> config + +(* what else would be useful... set_unicode? set_colors? *) + +(* example... *) + +(** {1 Pretty-printing functions } *) + +(** The pretty-printers are packaged into a module, parametrized by + the configuration. If you only need the default configuration, + the associated printers are available under [Default].*) + +module type Printers = sig + val pp_staged_spec : Format.formatter -> staged_spec -> unit +end + +module Default : Printers + +val obtain_printers : config -> (module Printers) + +(** { 1 String converters } *) + +(** Note that this is intended to display human-readable output. If + you need to obtain the underlying identifier, use [ident_of_binder] instead. *) +val string_of_binder : ?config:config -> binder -> string + +val string_of_type : ?config:config -> typ -> string +val string_of_term : ?config:config -> term -> string +val string_of_pi : ?config:config -> pi -> string +val string_of_kappa : ?config:config -> kappa -> string +val string_of_state : ?config:config -> state -> string +val string_of_pattern : ?config:config -> pattern -> string +val string_of_core_lang : ?config:config -> core_lang -> string +val string_of_staged_spec : ?config:config -> staged_spec -> string + + +(* some other combinators *) +val string_of_option : ?none:string -> ('a -> string) -> 'a option -> string +val string_of_list : ?sep:string -> ('a -> string) -> 'a list -> string + +(* these don't really belong here... in common maybe? *) +val string_of_pred : ?config:config -> pred_def -> string +val string_of_abs_env : ?config:config -> Hipcore_common.Types.abs_typ_env -> string +val string_of_type_declaration : ?config:config -> Hipcore_common.Types.type_declaration -> string diff --git a/lib/hipcore_typed/typed_core_ast.ml b/lib/hipcore_typed/typed_core_ast.ml index 32dd6db2..42f169c7 100644 --- a/lib/hipcore_typed/typed_core_ast.ml +++ b/lib/hipcore_typed/typed_core_ast.ml @@ -152,3 +152,22 @@ and typ = Types.typ = visitors { variety = "reduce"; name = "reduce_spec" }, visitors { variety = "mapreduce"; name = "mapreduce_spec" }, ord] + +let spec_calls_func spec f_name = + let go = object(self) + inherit [_] reduce_spec as super + method zero = false + method plus = (||) + + method! visit_HigherOrder _ f a = + self#plus (f = f_name) (super#visit_HigherOrder () f a) + + method! visit_Atomic () op a b = + match op with + | EQ -> (match (a.term_desc, b.term_desc) with + | (Var x, Var y) -> x = f_name || y = f_name + | _ -> false) + | _ -> false + end + in + go#visit_staged_spec () spec diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml index 14298fb8..d02e3227 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -97,6 +97,7 @@ let report_header ~kind ~name = let normal_report ~kind ~name ~inferred_spec ~given_spec ~result = let header = report_header ~kind ~name in + let open Default in let inferred_spec_string = Format.asprintf "[ Inferred specification ]\n%a\n" diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index f361a7c7..0241b16e 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -268,7 +268,7 @@ let derive_predicate m_name m_params f = p_name = m_name; p_params = m_params; p_body = new_spec; - p_rec = (find_rec m_name)#visit_staged_spec () new_spec; + p_rec = spec_calls_func new_spec m_name; } in res diff --git a/lib/hipprover/rewriting.ml b/lib/hipprover/rewriting.ml index e90a2d6b..52ae8077 100644 --- a/lib/hipprover/rewriting.ml +++ b/lib/hipprover/rewriting.ml @@ -1107,13 +1107,13 @@ let%expect_test "rewriting" = (* type-aware rewriting *) let string_of_uterm_with_types t = - let open Pretty.With_types in + let config = default_config () |> set_types_display in match t with - | Staged s -> string_of_staged_spec s - | Pure p -> string_of_pi p - | Heap h -> string_of_kappa h - | Term t -> string_of_term t - | Binder s -> (ident_of_binder s) + | Staged s -> string_of_staged_spec ~config s + | Pure p -> string_of_pi ~config p + | Heap h -> string_of_kappa ~config h + | Term t -> string_of_term ~config t + | Binder s -> string_of_binder ~config s | Type t -> string_of_type t in let string_of_rule_with_types r = @@ -1350,7 +1350,7 @@ module Deep = struct | Var s -> s | Inst _ -> "" | Constr (f, a) -> - Format.asprintf "%s%s" f (string_of_args string_of_pattern a) + Format.asprintf "%s%s" f (string_of_list ~sep:", " string_of_pattern a) let v s = Var s let and_ p1 p2 = Constr ("and", [p1; p2]) From c257ae07df6b9f452b09e984b75d302b104f1261 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Fri, 29 Aug 2025 17:47:58 +0800 Subject: [PATCH 08/15] tweak formatting and add tests currently unsure if a Format-based approach can still be salvaged or if a handrolled one is needed to achieve the desired outputs all the tests are broken but Trust Me BroTM it's just formatting changes --- lib/hipcore_typed/Pretty.ml | 87 ++++++++++++++++++++++------------- lib/hipcore_typed/patterns.ml | 14 +++--- lib/hipcore_typed/subst.ml | 4 +- 3 files changed, 66 insertions(+), 39 deletions(-) diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index a7bc79c5..f3be2eed 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -9,13 +9,12 @@ open Utils.Hstdlib type 'a fmt = Format.formatter -> 'a -> unit let pp_sep_comma ppf () = Format.fprintf ppf ",@ " -let pp_space ppf () = Format.fprintf ppf " " let pp_call_like : 'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> string -> 'a list -> unit = fun pp_arg ppf name args -> let open Format in - fprintf ppf "%s(%a)" + fprintf ppf "@[%s(%a)@]" name - (pp_print_list ~pp_sep:pp_space pp_arg) args + (pp_print_list ~pp_sep:pp_sep_comma pp_arg) args (* we use records-as-objects instead of classes to make it easier to dynamically stack modifications *) @@ -108,10 +107,10 @@ let default_printer = { let open Format in match t.term_desc with | Const c -> self.pp_constant self ppf c - | BinOp (op, lhs, rhs) -> fprintf ppf "(%a %a %a)" (self.pp_term self) lhs (self.pp_bin_term_op self) op (self.pp_term self) rhs + | BinOp (op, lhs, rhs) -> fprintf ppf "@[(%a@ %a@ %a)@]" (self.pp_term self) lhs (self.pp_bin_term_op self) op (self.pp_term self) rhs | TNot a -> fprintf ppf "not(%a)" (self.pp_term self) a | Var str -> pp_print_string ppf str - | Rel (bop, t1, t2) -> fprintf ppf "(%a %a %a)" (self.pp_term self) t1 (self.pp_bin_op self) bop (self.pp_term self) t2 + | Rel (bop, t1, t2) -> fprintf ppf "@[(%a@ %a@ %a)@]" (self.pp_term self) t1 (self.pp_bin_op self) bop (self.pp_term self) t2 | Construct (op, args) | TApp (op, args) -> pp_call_like (self.pp_term self) ppf op args | TTuple elems -> fprintf ppf "(%a)" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",") (self.pp_term self)) elems @@ -132,7 +131,7 @@ let default_printer = { match core.core_desc with | CValue v -> fprintf ppf "@[%a@]" (self.pp_term self) v | CLet (v, e1, e2) -> - fprintf ppf "@[let@ %a@ =@ @[%a@]@;in@ @[(%a)@]@]" + fprintf ppf "@[let@ %a@ =@ @[< 1>%a@]@;in@ @[< 1>(%a)@]@]" (self.pp_binder self) v (self.pp_core_lang self) e1 (self.pp_core_lang self) e2 @@ -140,13 +139,13 @@ let default_printer = { fprintf ppf "@[%a;@ %a@]" (self.pp_core_lang self) e1 (self.pp_core_lang self) e2 - | CIfElse (pi, t, e) -> fprintf ppf "@[if@ %a@ then@ @[%a@]@ else@ @[%a@]@]" + | CIfElse (pi, t, e) -> fprintf ppf "@[if@ %a@ then@ @[<>%a@]@ else@ @[<>%a@]@]" (self.pp_pi self) pi (self.pp_core_lang self) t (self.pp_core_lang self) e | CFunCall (f, xs) -> pp_call_like (self.pp_term self) ppf f xs | CWrite (v, e) -> fprintf ppf "@[%s@ :=@ %a@]" v (self.pp_term self) e | CRef v -> fprintf ppf "@[ref@ %a@]" (self.pp_term self) v | CRead v -> fprintf ppf "@[!%s]" v - | CAssert (p, h) -> fprintf ppf "@[assert@ (@[%a@ /\\@ %a@])@]" + | CAssert (p, h) -> fprintf ppf "@[assert@ (@[<>%a@ /\\@ %a@])@]" (self.pp_pi self) p (self.pp_kappa self) h | CPerform (eff, arg) -> fprintf ppf "@[perform@ %s@ %a@]" eff (pp_print_option (self.pp_term self)) arg @@ -198,40 +197,40 @@ let default_printer = { let open Format in match f with | Exists (v, spec) -> - fprintf ppf "@[ex@ %a.@ @[%a@]@]" + fprintf ppf "@[< 1>ex@ %a.@ @[< 1>%a@]@]" (self.pp_binder self) v (self.pp_staged_spec self) spec | ForAll (v, spec) -> - fprintf ppf "@[ex@ %a.@ @[%a@]@]" + fprintf ppf "@[< 1>ex@ %a.@ @[< 1>%a@]@]" (self.pp_binder self) v (self.pp_staged_spec self) spec | Require (p, k) -> - fprintf ppf "@[req@ (@[%a@ /\\@ %a@])@]" + fprintf ppf "@[req@ (@[< 1>%a@ /\\@ %a@])@]" (self.pp_pi self) p (self.pp_kappa self) k | NormalReturn (p, k) -> - fprintf ppf "@[ens@ (@[%a@ /\\@ %a@])@]" + fprintf ppf "@[ens@ (@[< 1>%a@ /\\@ %a@])@]" (self.pp_pi self) p (self.pp_kappa self) k | HigherOrder (f, args) -> pp_call_like (self.pp_term self) ppf f args | Shift (z, k, spec, _x, _cont) -> - fprintf ppf "@[%s(@[%a.@ %a@])@]" + fprintf ppf "@[%s(@[< 1>%a.@ %a@])@]" (if z then "sh" else "sh0") (self.pp_binder self) k (self.pp_staged_spec self) spec | Reset spec -> - fprintf ppf "@[%s(@[%a@])@]" + fprintf ppf "@[%s(@[< 1>%a@])@]" "rs" (self.pp_staged_spec self) spec | Sequence (s1, s2) -> - fprintf ppf "@[(%a;@ %a)@]" + fprintf ppf "@[< 1>(%a;@ %a)@]" (self.pp_staged_spec self) s1 (self.pp_staged_spec self) s2 | Bind (v, s1, s2) -> - fprintf ppf "@[let@ %a@ =@ @[%a@]@ in@ @[(%a)@]@]" + fprintf ppf "@[< 1>let@ %a@ =@ @[< 1>%a@]@ in@ @[< 1>(%a)@]@]" (self.pp_binder self) v (self.pp_staged_spec self) s1 (self.pp_staged_spec self) s2 | Disjunction (s1, s2) -> - fprintf ppf "@[(%a@ \\/@ %a@]" + fprintf ppf "@[(%a@ \\/@ %a)@]" (self.pp_staged_spec self) s1 (self.pp_staged_spec self) s2 (* TODO *) @@ -242,20 +241,20 @@ let default_printer = { fun self ppf p -> let open Format in match p with - | True -> fprintf ppf "true" - | False -> fprintf ppf "false" - | And (p1, p2) -> fprintf ppf "@[%a@ /\\@ %a@]" + | True -> fprintf ppf "T" + | False -> fprintf ppf "F" + | And (p1, p2) -> fprintf ppf "@[< 1>%a@ /\\@ %a@]" (self.pp_pi self) p1 (self.pp_pi self) p2 - | Or (p1, p2) -> fprintf ppf "@[%a@ \\/@ %a@]" + | Or (p1, p2) -> fprintf ppf "@[< 1>%a@ \\/@ %a@]" (self.pp_pi self) p1 (self.pp_pi self) p2 - | Not p -> fprintf ppf "@[~(%a)@]" + | Not p -> fprintf ppf "@[< 1>~(%a)@]" (self.pp_pi self) p - | Imply (p1, p2) -> fprintf ppf "@[(%a)@]@ =>@ @[(%a)@]" + | Imply (p1, p2) -> fprintf ppf "@[< 1>(%a)@]@ =>@ @[<>(%a)@]" (self.pp_pi self) p1 (self.pp_pi self) p2 | Predicate (name, args) -> pp_call_like (self.pp_term self) ppf name args - | Subsumption (t1, t2) -> fprintf ppf "@[(%a)@]@ <:@ @[(%a)@]" + | Subsumption (t1, t2) -> fprintf ppf "@[< 1>(%a)@]@ <:@ @[<>(%a)@]" (self.pp_term self) t1 (self.pp_term self) t2 - | Atomic (rel, t1, t2) -> fprintf ppf "@[(%a@ %a@ %a)@]" + | Atomic (rel, t1, t2) -> fprintf ppf "@[< 1>(%a@ %a@ %a)@]" (self.pp_term self) t1 (self.pp_bin_op self) rel (self.pp_term self) t2 end; pp_kappa = begin @@ -263,8 +262,8 @@ let default_printer = { let open Format in match k with | EmptyHeap -> fprintf ppf "emp" - | PointsTo (loc, t) -> fprintf ppf "@[%s@ ->@ @[(%a)@]@]" loc (self.pp_term self) t - | SepConj (k1, k2) -> fprintf ppf "@[(%a)@]@ *@ @[(%a)@]" + | PointsTo (loc, t) -> fprintf ppf "@[%s@ ->@ @[< 1>(%a)@]@]" loc (self.pp_term self) t + | SepConj (k1, k2) -> fprintf ppf "@[< 1>(%a)@]@ *@ @[<>(%a)@]" (self.pp_kappa self) k1 (self.pp_kappa self) k2 end; pp_state = begin @@ -276,11 +275,17 @@ let default_printer = { let add_type_annotations (pp : pretty_printer) : pretty_printer = (* TODO add annotations to terms, patterns, core lang, etc.. *) { pp with - pp_binder = + pp_binder = begin fun self ppf b -> Format.fprintf ppf "(%s : %a)" (ident_of_binder b) - (self.pp_typ self) (type_of_binder b)} + (self.pp_typ self) (type_of_binder b) + end; + pp_term = begin + fun self ppf t -> + Format.fprintf ppf "%a : %a" + (pp.pp_term self) t (pp.pp_typ self) t.term_type + end;} type config = { cfg_print_types : bool; @@ -311,10 +316,9 @@ let with_changed_out_functions ppf wrapper f = result let with_compact_spacing out_functions = - let do_nothing _ = () in Format.{ out_functions with - out_newline = do_nothing; + out_newline = ignore; out_indent = (fun _ -> out_functions.out_indent 1); out_spaces = (fun _ -> out_functions.out_spaces 1); } @@ -471,3 +475,24 @@ let string_of_abs_env ?(config = default_config ()) abs_env = let type_eqs = (TMap.map (fun t -> U.get t) !(abs_env.equalities)) |> TMap.bindings in Format.asprintf "@[vars:@ %a,@ eqs:@ %a@]" (pp_assoc_list Format.pp_print_string M.pp_typ) variable_types (pp_assoc_list M.pp_typ M.pp_typ) type_eqs +let%expect_test "syntax of output" = + let module With_types = (val obtain_printers (default_config () |> set_types_display) : Printers) in + let module Compact = (val obtain_printers (default_config () |> set_single_line) : Printers) in + let int_var v = {term_desc = Var v; term_type = Int} in + let cint c = {term_desc = Const (Num c); term_type = Int} in + let (+~) a b = {term_desc = BinOp (Plus, a, b); term_type = Int} in + let (=~) a b = Atomic (EQ, a, b) in + let f1 = NormalReturn (int_var "res" =~ cint 0, EmptyHeap) in + Format.printf "%a" With_types.pp_staged_spec f1; + [%expect {| |}]; + + (* f2 can be any output long enough to force default Format behavior to break lines *) + let to_sum = List.init 20 Fun.id |> List.map cint in + let f2 = NormalReturn (int_var "res" =~ List.fold_left (+~) (cint 0) to_sum, EmptyHeap) in + Format.printf "compacted: %a" Compact.pp_staged_spec f2; + [%expect {| |}]; + + let subpat = List.init 40 (Fun.const {pattern_desc = PAny; pattern_type = Int}) in + let p1 = {pattern_desc = PConstr ("with_lots_of_arguments", subpat); pattern_type = TConstr ("big_type", [])} in + Format.printf "expanded: %s\ncompacted: %s\n" (string_of_pattern p1) (string_of_pattern ~config:(default_config () |> set_single_line) p1); + [%expect {| |}];; diff --git a/lib/hipcore_typed/patterns.ml b/lib/hipcore_typed/patterns.ml index 534072ac..9c70e0d4 100644 --- a/lib/hipcore_typed/patterns.ml +++ b/lib/hipcore_typed/patterns.ml @@ -223,12 +223,14 @@ module Testing = struct ] } open Pretty - let output pats = String.concat " | " (List.map - (fun (pat, guard) -> - if guard = ctrue - then string_of_pattern pat - else Printf.sprintf "%s when %s" (string_of_pattern pat) (string_of_term guard)) - pats) |> print_string + let output pats = + let config = default_config () |> set_single_line in + String.concat " | " (List.map + (fun (pat, guard) -> + if guard = ctrue + then string_of_pattern ~config pat + else Printf.sprintf "%s when %s" (string_of_pattern ~config pat) (string_of_term ~config guard)) + pats) |> print_string let any ?(args = []) typ = {pattern_desc = PAny; pattern_type = TConstr (typ, args)} let constr ~typ ?(typ_args = []) ctr args = {pattern_desc = PConstr (ctr, args); pattern_type = TConstr (typ, typ_args)} diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml index 29dfbe44..7a1acba6 100644 --- a/lib/hipcore_typed/subst.ml +++ b/lib/hipcore_typed/subst.ml @@ -201,7 +201,7 @@ let%expect_test "subst" = reset_counter 0; let test bs f1 = let f2 = subst_free_vars bs f1 in - Format.printf "(%s)%s = %s@." (string_of_staged_spec f1) + Format.printf "(%s)[%s] = %s@." (string_of_staged_spec f1) (string_of_list (fun (x, t) -> Format.asprintf "%s/%s" (string_of_term t) x) bs) @@ -209,7 +209,7 @@ let%expect_test "subst" = in let test_term bs f1 = let f2 = subst_free_vars_term bs f1 in - Format.printf "(%s)%s = %s@." (string_of_term f1) + Format.printf "(%s)[%s] = %s@." (string_of_term f1) (string_of_list (fun (x, t) -> Format.asprintf "%s/%s" (string_of_term t) x) bs) From f79384e7888003c7a1a6fe4ac241a9c1d36f45a4 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 10:45:45 +0800 Subject: [PATCH 09/15] Rewrite pretty printing --- dune-project | 3 +- heifer.opam | 1 + lib/hipcore_typed/Pretty.ml | 920 ++++++++++++++++++++------------- lib/hipcore_typed/Pretty.mli | 18 +- lib/hipcore_typed/dune | 5 +- lib/hipcore_typed/subst.ml | 1 - lib/hipcore_typed/variables.ml | 12 +- lib/hiplib/hiplib.ml | 9 +- lib/hiplib/tests.ml | 6 +- lib/hipprover/entail.ml | 1 - lib/hipprover/rewriting.ml | 2 +- 11 files changed, 582 insertions(+), 396 deletions(-) diff --git a/dune-project b/dune-project index caccae12..16fe1c96 100644 --- a/dune-project +++ b/dune-project @@ -31,4 +31,5 @@ (why3-ide (>= 1.8.0)) (js_of_ocaml (>= 5.4.0)) (unionFind (>= 20220122)) - (visitors (>= 20210608)))) + (visitors (>= 20210608)) + (pprint (>= 20230830)))) diff --git a/heifer.opam b/heifer.opam index 75caa6fc..7b9f49dc 100644 --- a/heifer.opam +++ b/heifer.opam @@ -20,6 +20,7 @@ depends: [ "js_of_ocaml" {>= "5.4.0"} "unionFind" {>= "20220122"} "visitors" {>= "20210608"} + "pprint" {>= "20230830"} "odoc" {with-doc} ] build: [ diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index f3be2eed..be92948a 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -1,433 +1,620 @@ (* Functions for printing the typed AST. *) -open Hipcore +open Hipcore_common open Typedhip open Types -open Utils.Misc open Utils.Hstdlib -type 'a fmt = Format.formatter -> 'a -> unit +type 'a to_document = 'a -> PPrint.document -let pp_sep_comma ppf () = Format.fprintf ppf ",@ " -let pp_call_like : 'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> string -> 'a list -> unit = - fun pp_arg ppf name args -> - let open Format in - fprintf ppf "@[%s(%a)@]" - name - (pp_print_list ~pp_sep:pp_sep_comma pp_arg) args +let pp_call_like : 'a. 'a to_document -> ?sep:PPrint.document -> (string * 'a list) to_document = + let open PPrint in + fun arg_fmt ?(sep = comma ^^ break 1) (f, args) -> + group (string f ^^ parens (nest 2 (flow sep (List.map arg_fmt args)))) -(* we use records-as-objects instead of classes to make it easier - to dynamically stack modifications *) +(** The main set of pretty-printing functions. + + We use records-as-objects instead of classes to make it easier + to dynamically stack modifications. *) type pretty_printer = { - pp_typ : pretty_printer -> typ fmt; - pp_binder : pretty_printer -> binder fmt; - pp_bin_op : pretty_printer -> bin_rel_op fmt; - pp_bin_term_op : pretty_printer -> bin_term_op fmt; - pp_constant : pretty_printer -> const fmt; - pp_lambda_like : pretty_printer -> (binder list * staged_spec option * core_lang option) fmt; - pp_term : pretty_printer -> term fmt; - pp_core_lang : pretty_printer -> core_lang fmt; - pp_staged_spec : pretty_printer -> staged_spec fmt; - pp_kappa : pretty_printer -> kappa fmt; - pp_pi : pretty_printer -> pi fmt; - pp_state : pretty_printer -> state fmt; - pp_pattern : pretty_printer -> pattern fmt; + pp_typ : pretty_printer -> printing_context -> typ to_document; + pp_binder : pretty_printer -> printing_context -> binder to_document; + pp_bin_op : pretty_printer -> printing_context -> bin_rel_op to_document; + pp_bin_term_op : pretty_printer -> printing_context -> bin_term_op to_document; + pp_constant : pretty_printer -> printing_context -> const to_document; + pp_lambda_like : pretty_printer -> printing_context -> (binder list * staged_spec option * core_lang option) to_document; + pp_term : pretty_printer -> printing_context -> term to_document; + pp_core_lang : pretty_printer -> printing_context -> core_lang to_document; + pp_staged_spec : pretty_printer -> printing_context -> staged_spec to_document; + pp_kappa : pretty_printer -> printing_context -> kappa to_document; + pp_pi : pretty_printer -> printing_context -> pi to_document; + pp_state : pretty_printer -> printing_context -> state to_document; + pp_pattern : pretty_printer -> printing_context -> pattern to_document; +} +and printing_context = { + (** The "binding power" of the parent AST node, analogous to operator precedence. + Printers for AST nodes that use parentheses to disambiguate between different nestings of operators + can use this context to determine whether or not they should parenthesize their own output. + (When unsure, it might be best to parenthesize anyway, for clarity.) *) + ppc_parent_binding : binding_power +} +and binding_power = + (* Used to inform the child that the parent is irrelevant to deciding whether or not to parenthesize. *) + | Negative_inf + | Finite of int + +let default_printing_context () = { + ppc_parent_binding = Negative_inf } -let default_printer = { - pp_typ = begin fun self ppf t -> - let open Types in - let open Format in +(** Returns [true] iff [a] denotes a lower binding power then [b]. *) +let lower_precedence a b = + match a, b with + | Negative_inf, Finite _ -> true + | Finite x, Finite y when x < y -> true + | _, _ -> false + +let with_binding power pp_context = + {pp_context with ppc_parent_binding = power} + [@warning "-23"] (* suppress this, since more fields might be added to printing_context in the future *) + +let parent_binding_power ctx = ctx.ppc_parent_binding + +(** Wrap [doc] with parentheses if the given binding power [binding] is less than the binding power in [ctx]. *) +let parens_if_needed ctx binding doc = + if lower_precedence binding (parent_binding_power ctx) + then PPrint.parens doc + else doc + +let rec flatten_binary_syntax ~(destruct : 'a -> ('a * 'a) option) (node : 'a) : 'a list = + match destruct node with + | Some (a, b) -> (flatten_binary_syntax ~destruct a) @ (flatten_binary_syntax ~destruct b) + | None -> [node] + +(** Like [PPrint.infix], but, in normal mode, puts the infix operator after the newline, and sets + an alignment point for the right operand. *) +let infix_on_newline b op lhs rhs = + PPrint.(group (lhs ^^ break b ^^ op ^^ blank b ^^ align (nest 1 rhs))) + +let rec flatten_unary_syntax_right ~(destruct : 'a -> ('b * 'a) option) (node : 'a) : 'b list * 'a = + match destruct node with + | Some (b, a) -> + let remaining, a = flatten_unary_syntax_right ~destruct a in + ([b] @ remaining, a) + | None -> ([], node) + +(** Tries to put [elems] on one line, separated by [op] (with [b] spaces before and after). If an + element does not fit, place it (and the operator) on a separate line, aligned to the end of [op] (including spacing.) *) +let prefixed_list b op elems = + let open PPrint in + flow (break b ^^ op ^^ blank b) (List.map align elems) + +let suffixed_list before after op elems = + let open PPrint in + flow (blank before ^^ op ^^ break after) (List.map align elems) + +(* For some AST nodes (e.g. Construct, BinOp), we want to format them as infix operators + depending on the name of the function being called. Check if this function name is + one of those operators. *) +let is_infix f = + match f with + | "::" | "+" | "-" | "*" | "=" | "&&" | "||" | ">" | "<" | ">=" | "<=" | "^" -> true + | _ -> false + +(** Given an AST node, break it up into subnodes as much as possible using [destruct], convert them + into documents using [renderer], then combine them into one document using [prefixed_list] and the + given spacing and separator. This is most useful for flattening the tree when encountering an + associative operator. *) +let format_as_prefixed_list ?(spacing = 1) ~(sep : PPrint.document) ~(destruct : 'a -> ('a * 'a) option) ~(renderer : 'a to_document) : 'a to_document = + fun node -> + let elements = flatten_binary_syntax ~destruct node in + let formatted = List.map renderer elements in + prefixed_list spacing sep formatted + +let format_as_suffixed_list ?(before = 0) ?(after = 1) ~(sep : PPrint.document) ~(destruct : 'a -> ('a * 'a) option) ~(renderer: 'a to_document) : 'a to_document = + fun node -> + let elements = flatten_binary_syntax ~destruct node in + let formatted = List.map renderer elements in + suffixed_list before after sep formatted + +let conj = PPrint.string "/\\" +let disj = PPrint.string "\\/" +let sep_arrow = PPrint.string "->" +let sep_conj = PPrint.star +let implies = PPrint.string "=>" +let subsumes = PPrint.string "<:" +let pure_not = PPrint.tilde + +let default_printer = + let open PPrint in { + pp_typ = begin fun self ctx t -> + let open PPrint in match t with - | Any -> pp_print_string ppf "" - | TyString -> pp_print_string ppf "string" - | Int -> pp_print_string ppf "int" - | Unit -> pp_print_string ppf "unit" - | TConstr (name, args) -> - if List.is_empty args - then pp_print_string ppf name - else Format.fprintf ppf "(%a) %s" - (pp_print_list ~pp_sep:pp_sep_comma (self.pp_typ self)) args - name - | Bool -> pp_print_string ppf "bool" - | Lamb -> pp_print_string ppf "lambda" - | TVar v -> Format.fprintf ppf "'%s" v - | Arrow (t1, t2) -> Format.fprintf ppf "%a->%a" (self.pp_typ self) t1 (self.pp_typ self) t2 + | Any -> string "any" + | Unit -> string "unit" + | Int -> string "int" + | Bool -> string "bool" + | TyString -> string "string" + | Lamb -> string "(? -> ?)" + | TVar v -> string "'" ^^ string v + | TConstr (name, args) -> begin match args with + | [] -> string name + | [arg] -> (self.pp_typ self ctx arg) ^^ space ^^ string name + | args -> parens (separate (comma ^^ break 1) (List.map (self.pp_typ self ctx) args)) ^^ space ^^ string name + end + | Arrow _ -> + let args, ret = flatten_unary_syntax_right ~destruct:(function Arrow (a, b) -> Some (a, b) | _ -> None) t in + prefixed_list 1 (string "->") (List.map (self.pp_typ self (ctx |> with_binding (Finite 20))) (args @ [ret])) + |> parens_if_needed ctx (Finite 10) end; - pp_binder = begin fun _ ppf binder -> - Format.pp_print_string ppf (ident_of_binder binder) + (* binders, bin ops and constants are atomic, and thus do not need parenthesization *) + pp_binder = begin + fun _self _ b -> string (ident_of_binder b) end; - pp_bin_op = begin - fun _ ppf op -> - let s = match op with - | GT -> ">" - | LT -> "<" - | EQ -> "=" - | GTEQ -> ">=" - | LTEQ -> "<=" - in - Format.pp_print_string ppf s + pp_bin_op = begin + fun _self _ op -> match op with + | GT -> string ">" + | LT -> string "<" + | EQ -> string "=" + | GTEQ -> string ">=" + | LTEQ -> string "<=" end; pp_bin_term_op = begin - fun _ ppf op -> - let s = match op with - | Plus -> "+" - | Minus -> "-" - | SConcat -> "++" - | TAnd -> "&&" - | TPower -> "^" - | TTimes -> "*" - | TDiv -> "/" - | TOr -> "||" - | TCons -> "::" - in - Format.pp_print_string ppf s + fun _self _ op -> match op with + | Plus -> string "+" + | Minus -> string "-" + | SConcat -> string "++" + | TAnd -> string "&&" + | TPower -> string "^" + | TTimes -> string "*." + | TDiv -> string "/" + | TOr -> string "||" + | TCons -> string "::" end; pp_constant = begin - fun _ ppf c -> - let open Format in - match c with - | ValUnit -> pp_print_string ppf "()" - | Num n -> pp_print_int ppf n - | TStr s -> pp_print_string ppf ("\"" ^ s ^ "\"") - | Nil -> pp_print_string ppf "[]" - | TTrue -> pp_print_string ppf "true" - | TFalse -> pp_print_string ppf "false" + fun _self _ c -> match c with + | ValUnit -> string "()" + | Num n -> string (string_of_int n) + | TStr s -> dquotes (string s) + | Nil -> string "[]" + | TTrue -> string "true" + | TFalse -> string "false" end; pp_lambda_like = begin - fun self ppf (params, spec, body) -> - let open Format in - fprintf ppf "(fun %a (*@@ %a @@*) %a)" - (pp_print_list ~pp_sep:pp_sep_comma (self.pp_binder self)) params - (pp_print_option (self.pp_staged_spec self)) spec - (pp_print_option (fun ppf body -> fprintf ppf "-> %a" (self.pp_core_lang self) body)) body + fun self ctx (args, spec, body) -> + let func_token = string "fun" in + let rendered_args = align ((List.map (self.pp_binder self ctx) args @ [string "->"]) |> flow (break 1)) in + let rendered_spec = match spec with + | Some spec -> + let spec_open = string "(*@" in + let spec_close = string "@*)" in + group (spec_open ^^ space ^^ align (group (self.pp_staged_spec self (ctx |> with_binding Negative_inf) spec ^^ break 1 ^^ spec_close))) + | None -> empty + in + let rendered_body = match body with + | Some body -> self.pp_core_lang self ctx body + | None -> underscore + in + group (func_token ^^ blank 1 ^^ rendered_args ^^ nest 2 (break 1 ^^ rendered_spec ^^ break 1 ^^ rendered_body)) end; pp_term = begin - fun self ppf t -> - let open Format in - match t.term_desc with - | Const c -> self.pp_constant self ppf c - | BinOp (op, lhs, rhs) -> fprintf ppf "@[(%a@ %a@ %a)@]" (self.pp_term self) lhs (self.pp_bin_term_op self) op (self.pp_term self) rhs - | TNot a -> fprintf ppf "not(%a)" (self.pp_term self) a - | Var str -> pp_print_string ppf str - | Rel (bop, t1, t2) -> fprintf ppf "@[(%a@ %a@ %a)@]" (self.pp_term self) t1 (self.pp_bin_op self) bop (self.pp_term self) t2 - | Construct (op, args) | TApp (op, args) -> pp_call_like (self.pp_term self) ppf op args - | TTuple elems - -> fprintf ppf "(%a)" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",") (self.pp_term self)) elems - | TLambda (_, params, spec, body) -> (self.pp_lambda_like self) ppf (params, spec, body) + (* Relevant precedence levels for terms (higher = stronger binding power): + - 120: TPower, SConcat, TCons + - 110: TTimes, TDiv + - 100: TPlus, TMinus + - 90: TNot + - 80: TAnd + - 70: TOr *) + (* TApp, Construct and TLambda all delimit their own children in other ways, so there's no need to parenthesize them *) + fun self ctx t -> match t.term_desc with + | Const c -> self.pp_constant self (ctx |> with_binding Negative_inf) c + | Var s -> string s + | Rel (op, a, b) -> + (* special case to print propositional equality using only one equal sign. + this helps distinguish it from boolean equality in expressions like (n == 0) = true *) + let rendered_op = + match op with + | EQ -> string "==" + | _ -> self.pp_bin_op self ctx op + in + group (infix 2 1 rendered_op (self.pp_term self (ctx |> with_binding Negative_inf) a) (self.pp_term self (ctx |> with_binding Negative_inf) b)) + | BinOp (op, a, b) -> begin + let self_precedence = Finite (match op with + | TPower | SConcat | TCons -> 120 + | TTimes | TDiv -> 110 + | Plus | Minus -> 100 + | TAnd -> 80 + | TOr -> 70) + in + let rendered = match op with + (* handle associative operators separately, to flatten them *) + | TCons | SConcat | TTimes | Plus | TAnd | TOr -> + format_as_prefixed_list ~sep:(self.pp_bin_term_op self ctx op) + ~destruct:(fun t -> match t.term_desc with BinOp (o, lhs, rhs) when o = op -> Some (lhs, rhs) | _ -> None) + ~renderer:(self.pp_term self (ctx |> with_binding self_precedence)) t + | _ -> group (infix 2 1 (self.pp_bin_term_op self ctx op) + (self.pp_term self (ctx |> with_binding self_precedence) a) + (self.pp_term self (ctx |> with_binding self_precedence) b)) + in + (* decide whether or not to wrap this in parentheses *) + parens_if_needed ctx self_precedence rendered + end + | TNot t -> precede (string "not ") (self.pp_term self (ctx |> with_binding (Finite 90)) t) + | TApp (f, args) -> pp_call_like (self.pp_term self (ctx |> with_binding Negative_inf)) (f, args) + | Construct (f, args) -> + (* we need some additional logic to improve output when the constructor has no args, or is an infix op *) + begin + match args with + | [] -> string f + | [a; b] when is_infix f -> + (* the only possible infix op here is :: *) + (* format this as if it's BinOp(TCons, a, b), with the proper precedence*) + let infix_precedence = Finite 120 in + group (infix 0 1 (string f) (self.pp_term self (ctx |> with_binding infix_precedence) a) (self.pp_term self (ctx |> with_binding infix_precedence) b)) + | _ -> pp_call_like (self.pp_term self (ctx |> with_binding Negative_inf)) (f, args) + end + | TLambda (_name, args, spec, body) -> + (* if it does not fit into one line, first, break it as + fun (args...) -> + (*@@ spec @@*) + body + the args can be broken up further, as long as they are aligned with the first one + the spec can be broken up further, as long as it's aligned with the opening tag + *) + self.pp_lambda_like self (ctx |> with_binding Negative_inf) (args, spec, body) |> parens + (* TODO shift_reset_progs/state_monad.ml generates a spec during debugging with lots of nested (fun k -> (*@ ens emp /\ res = (fun k -> ... ) @*)) + and it causes an ugly pyramid... is there a better way? *) + | TTuple args -> ignore args; string "tup" end; - pp_pattern = begin - fun self ppf pat -> - match pat.pattern_desc with - | PAny -> Format.pp_print_string ppf "_" - | PVar v -> Format.fprintf ppf "@[%s@]" (fst v) - | PConstr (name, args) -> pp_call_like (self.pp_pattern self) ppf name args - | PConstant c -> (self.pp_constant self) ppf c - | PAlias (p, s) -> Format.fprintf ppf "@[%a@ as@ %s@]" (self.pp_pattern self) p s + pp_pattern = begin fun self ctx pat -> match pat.pattern_desc with + | PAny -> underscore + | PConstant c -> self.pp_constant self ctx c + | PVar v -> self.pp_binder self ctx v + | PAlias (pat, s) -> self.pp_pattern self ctx pat ^^ blank 1 ^^ string "as" ^^ blank 1 ^^ string s + | PConstr (name, args) -> + match args with + | [] -> string name + | [a; b] when is_infix name -> + group (infix 0 1 (string name) (self.pp_pattern self ctx a) (self.pp_pattern self ctx b)) + | _ -> pp_call_like (self.pp_pattern self ctx) (name, args) end; - pp_core_lang = begin - fun self ppf core -> - let open Format in - match core.core_desc with - | CValue v -> fprintf ppf "@[%a@]" (self.pp_term self) v - | CLet (v, e1, e2) -> - fprintf ppf "@[let@ %a@ =@ @[< 1>%a@]@;in@ @[< 1>(%a)@]@]" - (self.pp_binder self) v - (self.pp_core_lang self) e1 - (self.pp_core_lang self) e2 - | CSequence (e1, e2) -> - fprintf ppf "@[%a;@ %a@]" - (self.pp_core_lang self) e1 - (self.pp_core_lang self) e2 - | CIfElse (pi, t, e) -> fprintf ppf "@[if@ %a@ then@ @[<>%a@]@ else@ @[<>%a@]@]" - (self.pp_pi self) pi (self.pp_core_lang self) t (self.pp_core_lang self) e - | CFunCall (f, xs) -> pp_call_like (self.pp_term self) ppf f xs - | CWrite (v, e) -> fprintf ppf "@[%s@ :=@ %a@]" v (self.pp_term self) e - | CRef v -> fprintf ppf "@[ref@ %a@]" (self.pp_term self) v - | CRead v -> fprintf ppf "@[!%s]" v - | CAssert (p, h) -> fprintf ppf "@[assert@ (@[<>%a@ /\\@ %a@])@]" - (self.pp_pi self) p (self.pp_kappa self) h + pp_core_lang = begin fun self ctx core -> match core.core_desc with + | CValue value -> self.pp_term self ctx value + | CLet (b, c1, c2) -> + let header = group ( + string "let" ^^ space ^^ (self.pp_binder self (ctx |> with_binding Negative_inf) b) ^^ space ^^ equals + ^^ nest 2 (break 1 ^^ self.pp_core_lang self (ctx |> with_binding Negative_inf) c1 + ^^ break 1 ^^ string "in") + ) in + group (header ^^ break 1 ^^ self.pp_core_lang self (ctx |> with_binding Negative_inf) c2) + | CSequence (c1, c2) -> group (infix 0 0 semi + (self.pp_core_lang self (ctx |> with_binding Negative_inf) c1) + (self.pp_core_lang self (ctx |> with_binding Negative_inf) c2)) + | CIfElse (cond, c1, c2) -> + (* TODO a special case for if-else chains could be good here *) + string "if" ^^ nest 2 (break 1 ^^ self.pp_pi self (ctx |> with_binding Negative_inf) cond) + ^^ break 1 ^^ string "then" ^^ blank 1 ^^ nest 2 (self.pp_core_lang self (ctx |> with_binding Negative_inf) c1) + ^^ break 1 ^^ string "else" ^^ blank 1 ^^ nest 2 (self.pp_core_lang self (ctx |> with_binding Negative_inf) c2) + | CFunCall (f, args) -> + (* for these function calls, we mirror OCaml syntax *) + string f ^^ nest 2 (space ^^ flow (break 1) (List.map (self.pp_term self (ctx |> with_binding Negative_inf)) args)) + |> parens + | CWrite (loc, v) -> string loc ^^ space ^^ string "<-" ^^ nest 2 (break 1 ^^ self.pp_term self (ctx |> with_binding Negative_inf) v) + | CRef v -> string "ref" ^^ space ^^ parens (self.pp_term self (ctx |> with_binding Negative_inf) v) + | CRead loc -> string "!" ^^ string loc + | CAssert (p, k) -> + (* follows how req/ens is formatted *) + (string "assert") ^^ nest 2 (space ^^ parens (self.pp_state self (ctx |> with_binding Negative_inf) (p, k))) | CPerform (eff, arg) -> - fprintf ppf "@[perform@ %s@ %a@]" eff (pp_print_option (self.pp_term self)) arg - | CMatch (typ, spec, e, hs, cs) -> - let pp_core_handler_ops = - let pp_handler ppf (name, v, spec, body) = - fprintf ppf "|@ %a@ k@ %a@ ->@ %a@]" - (fun ppf (name, v) -> match v with - | None -> pp_print_string ppf name - | Some v -> fprintf ppf "(%s@ %s)" name v) (name, v) - (pp_print_option (self.pp_staged_spec self)) spec - (self.pp_core_lang self) body - in - pp_print_list pp_handler + let arg = match arg with + | Some arg -> self.pp_term self (ctx |> with_binding Negative_inf) arg + | None -> string "()" in - let pp_handler_type ppf h = - match h with - | Deep -> pp_print_string ppf "d" - | Shallow -> pp_print_string ppf "s" + string "perform" ^^ (parens (string eff ^^ break 1 ^^ arg)) + | CMatch (handler_type, _tcl, e, handlers, cases) -> + let match_token = + match handlers with + | [] -> string "match" + | _ -> match handler_type with + | Deep -> string "match[s]" | Shallow -> string "match[d]" in - let pp_constr_case ppf case = - Format.(fprintf ppf "@[@ |@ %a%a@ ->@ %a@]" - (self.pp_pattern self) case.ccase_pat - (pp_print_option (self.pp_term self)) case.ccase_guard - (self.pp_core_lang self) case.ccase_expr) + let pp_case case = + let pattern = self.pp_pattern self (ctx |> with_binding Negative_inf) case.ccase_pat in + let guard = match case.ccase_guard with + | Some guard -> blank 1 ^^ group (string "when" ^^ group (self.pp_term self (ctx |> with_binding Negative_inf) guard)) + | None -> empty + in + let expr = self.pp_core_lang self (ctx |> with_binding Negative_inf) case.ccase_expr in + string "|" ^^ space ^^ align (group ( + group (pattern + ^^ guard ^^ blank 1 ^^ string "->") + ^^ nest 2 (break 1 ^^ expr))) in - let pp_constr_cases ppf cases = - let open Format in - pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "@,") pp_constr_case ppf cases + let pp_handler _ = + (* not sure what the right syntax here should be... *) + string "[effect handler]" in - let pp_placeholder s = fun ppf _ -> pp_print_string ppf s in - let pp_try_catch_lemma = pp_placeholder "[try-catch lemma]" in - fprintf ppf "@[match[%a]@ (%a)@ with@,%a@,%a@,%a@]" - pp_handler_type typ - (pp_print_option pp_try_catch_lemma) spec - (self.pp_core_lang self) e - pp_core_handler_ops hs - pp_constr_cases cs - | CResume args -> fprintf ppf "@[continue@ %a@]" (pp_print_list (self.pp_term self)) args - | CLambda (xs, spec, e) -> (self.pp_lambda_like self) ppf (xs, spec, Some e) - | CShift (b, k, e) -> fprintf ppf "@[%s@ %a@ ->@ %a@]" - (if b then "Shift" else "Shift0") - (self.pp_binder self) k - (self.pp_core_lang self) e - | CReset e -> fprintf ppf "@[@<%a@>@]" (self.pp_core_lang self) e + group ( + group ( + match_token ^^ nest 2 (break 1 ^^ self.pp_core_lang self (ctx |> with_binding Negative_inf) e) ^^ break 1 ^^ string "with" + ) + ^^ break 1 ^^ + separate (break 1) (List.map pp_case cases @ List.map pp_handler handlers) + ) + |> parens (* match statements having no ending delimiter was a mistake in ocaml syntax... *) + | CResume (args) -> + string "resume" ^^ nest 2 (space ^^ flow (break 1) (List.map (self.pp_term self (ctx |> with_binding Negative_inf)) args)) + | CLambda (args, spec, body) -> parens (self.pp_lambda_like self (ctx |> with_binding Negative_inf) (args, spec, Some body)) + | CShift (not_zero, k, body) -> + let shift_ident = if not_zero then "shift" else "shift0" in + string shift_ident ^^ space ^^ nest 2 (parens (self.pp_lambda_like self (ctx |> with_binding Negative_inf) ([k], None, Some body))) + | CReset body -> string "reset" ^^ space ^^ nest 2 (parens (self.pp_core_lang self (ctx |> with_binding Negative_inf) body)) end; - pp_staged_spec = begin - fun self ppf f -> - let open Format in + pp_staged_spec = begin fun self ctx f -> + (* precedence in the parser is exists/forall, disjunction, req, ens, fn, shift, reset, sequence, bind, parens *) + (* + i observe that usually, specs take the form of disjunction of sequences of quantifiers of binds of req/ens/fn/shift/reset + i want sequence -> quantify -> bind to naturally read like a string of lines + so that's the natural precedence + + but i need to be careful, since bind-association isn't proven + + - 90: Sequencing + - 80: Conjunction (used by state) + - 70: Disjunction + - 60: Bind? + *) match f with - | Exists (v, spec) -> - fprintf ppf "@[< 1>ex@ %a.@ @[< 1>%a@]@]" - (self.pp_binder self) v - (self.pp_staged_spec self) spec - | ForAll (v, spec) -> - fprintf ppf "@[< 1>ex@ %a.@ @[< 1>%a@]@]" - (self.pp_binder self) v - (self.pp_staged_spec self) spec + (* try to put as many Exists/ForAll on one line as possible to improve output on chains of quantifiers *) + | Exists _ | ForAll _ -> + (* flatten syntax to extract any quantifier chain *) + let quantifiers, body = flatten_unary_syntax_right + ~destruct:(function Exists (b, s) -> Some (`Exists b, s) | ForAll (b, s) -> Some (`ForAll b, s) | _ -> None) f in + let rendered_qs = List.map (fun v -> + match v with + | `Exists b -> concat [string "ex"; space; self.pp_binder self ctx b; dot] + | `ForAll b -> concat [string "forall"; space; self.pp_binder self ctx b; dot]) quantifiers in + (* print the body with parens and indent to make the scope of the bindings clear *) + let rendered_body = parens (align (self.pp_staged_spec self (ctx |> with_binding Negative_inf) body)) in + group (flow (break 1) rendered_qs ^^ nest 2 (break 1 ^^ rendered_body)) | Require (p, k) -> - fprintf ppf "@[req@ (@[< 1>%a@ /\\@ %a@])@]" - (self.pp_pi self) p (self.pp_kappa self) k + (string "req") ^^ nest 2 (space ^^ parens (self.pp_state self (ctx |> with_binding Negative_inf) (p, k))) | NormalReturn (p, k) -> - fprintf ppf "@[ens@ (@[< 1>%a@ /\\@ %a@])@]" - (self.pp_pi self) p (self.pp_kappa self) k - | HigherOrder (f, args) -> pp_call_like (self.pp_term self) ppf f args - | Shift (z, k, spec, _x, _cont) -> - fprintf ppf "@[%s(@[< 1>%a.@ %a@])@]" - (if z then "sh" else "sh0") - (self.pp_binder self) k - (self.pp_staged_spec self) spec - | Reset spec -> - fprintf ppf "@[%s(@[< 1>%a@])@]" - "rs" - (self.pp_staged_spec self) spec - | Sequence (s1, s2) -> - fprintf ppf "@[< 1>(%a;@ %a)@]" - (self.pp_staged_spec self) s1 - (self.pp_staged_spec self) s2 + (string "ens") ^^ nest 2 (space ^^ parens (self.pp_state self (ctx |> with_binding Negative_inf) (p, k))) + | HigherOrder (f, args) -> pp_call_like (self.pp_term self ctx) (f, args) + | Disjunction _ -> + (* flatten the structure of a set of disjuncts, so they can always be rendered as a flat list *) + let disj_precedence = Finite 70 in + format_as_prefixed_list ~sep:disj + ~destruct:(function Disjunction (s1, s2) -> Some (s1, s2) | _ -> None) + ~renderer:(self.pp_staged_spec self (ctx |> with_binding disj_precedence)) f + |> parens_if_needed ctx disj_precedence + | Sequence _ -> + (* group (infix 0 0 (semi ^^ blank 1) (self.pp_staged_spec self ctx s1) (self.pp_staged_spec self ctx s2)) *) + let seq_precedence = Finite 90 in + format_as_suffixed_list ~sep:semi + ~destruct:(function Sequence (s1, s2) -> Some (s1, s2) | _ -> None) + ~renderer:(self.pp_staged_spec self (ctx |> with_binding seq_precedence)) f + |> parens_if_needed ctx seq_precedence | Bind (v, s1, s2) -> - fprintf ppf "@[< 1>let@ %a@ =@ @[< 1>%a@]@ in@ @[< 1>(%a)@]@]" - (self.pp_binder self) v - (self.pp_staged_spec self) s1 - (self.pp_staged_spec self) s2 - | Disjunction (s1, s2) -> - fprintf ppf "@[(%a@ \\/@ %a)@]" - (self.pp_staged_spec self) s1 - (self.pp_staged_spec self) s2 - (* TODO *) - | RaisingEff _ -> pp_print_string ppf "[effect stage]" - | TryCatch _ -> pp_print_string ppf "[trycatch stage]" + (* this can be rendered as: + - if it fits into one line, (s1); v. s2 + - otherwise, render s2 on its own line + - if the bound value doesn't fit, break into its own lines, and indent by two *) + let bind_precedence = Finite 60 in + let header = group (lparen ^^ nest 2 (break 0 ^^ self.pp_staged_spec self ctx s1) ^^ break 0 ^^ rparen ^^ semi + ^^ space ^^ (self.pp_binder self (ctx |> with_binding Negative_inf) v)) ^^ dot in + let body = parens_if_needed ctx bind_precedence (self.pp_staged_spec self (ctx |> with_binding bind_precedence) s2) in + group (header ^^ break 1 ^^ body) + | Shift (non_zero, cont_binder, metacont, hole_binder, partial_cont) -> + let call_name = if non_zero then "shift" else "shift0" in + (* special case to hide the partial continuation if it is just the identity (i.e. it has not absorbed + any of the context yet) *) + let partial_cont_is_empty = + match partial_cont with + | NormalReturn (p, EmptyHeap) -> begin + match Variables.eq_res_term p with + | Some {term_desc = Var v; _} -> v = (ident_of_binder hole_binder) + | _ -> false + end + | _ -> false + in + if partial_cont_is_empty + then pp_call_like (self.pp_lambda_like self ctx) ~sep:(semi ^^ break 1) + (call_name, [[cont_binder], Some metacont, None]) + else + pp_call_like (self.pp_lambda_like self ctx) ~sep:(semi ^^ break 1) + (call_name, [[cont_binder], Some metacont, None; [hole_binder], Some partial_cont, None]) + | Reset r -> + angles (self.pp_staged_spec self ctx r) + | _ -> string "[other stage]" end; pp_pi = begin - fun self ppf p -> - let open Format in - match p with - | True -> fprintf ppf "T" - | False -> fprintf ppf "F" - | And (p1, p2) -> fprintf ppf "@[< 1>%a@ /\\@ %a@]" - (self.pp_pi self) p1 (self.pp_pi self) p2 - | Or (p1, p2) -> fprintf ppf "@[< 1>%a@ \\/@ %a@]" - (self.pp_pi self) p1 (self.pp_pi self) p2 - | Not p -> fprintf ppf "@[< 1>~(%a)@]" - (self.pp_pi self) p - | Imply (p1, p2) -> fprintf ppf "@[< 1>(%a)@]@ =>@ @[<>(%a)@]" - (self.pp_pi self) p1 (self.pp_pi self) p2 - | Predicate (name, args) -> pp_call_like (self.pp_term self) ppf name args - | Subsumption (t1, t2) -> fprintf ppf "@[< 1>(%a)@]@ <:@ @[<>(%a)@]" - (self.pp_term self) t1 (self.pp_term self) t2 - | Atomic (rel, t1, t2) -> fprintf ppf "@[< 1>(%a@ %a@ %a)@]" - (self.pp_term self) t1 (self.pp_bin_op self) rel (self.pp_term self) t2 + fun self ctx p -> match p with + (* precedences: + - 100: Not + - 90: Subsumption, atomics + - 80: Conjunction + - 70: Disjunction + - 60: Implication + *) + (* precedence is True, False, atoms, (subsumes), conj, (disjunction), (implication), not, parens *) + | True -> string "T" + | False -> string "F" + | And _ -> + let and_precedence = Finite 80 in + format_as_prefixed_list ~sep:conj + ~destruct:(function And (p1, p2) -> Some (p1, p2) | _ -> None) + ~renderer:(self.pp_pi self (ctx |> with_binding and_precedence)) p + |> parens_if_needed ctx and_precedence + | Or _ -> + let or_precedence = Finite 70 in + format_as_prefixed_list ~sep:disj + ~destruct:(function Or (p1, p2) -> Some (p1, p2) | _ -> None) + ~renderer:(self.pp_pi self (ctx |> with_binding or_precedence)) p + |> parens_if_needed ctx or_precedence + | Imply (p1, p2) -> + let imply_precedence = Finite 60 in + infix 2 1 implies (self.pp_pi self (ctx |> with_binding imply_precedence) p1) + (self.pp_pi self (ctx |> with_binding imply_precedence) p2) + |> parens_if_needed ctx imply_precedence + | Not p -> + let not_precedence = Finite 100 in + pure_not ^^ (self.pp_pi self (ctx |> with_binding not_precedence) p) + |> parens_if_needed ctx not_precedence + | Predicate (f, args) -> pp_call_like (self.pp_term self (ctx |> with_binding Negative_inf)) (f, args) + | Atomic (op, a, b) -> + let atom_precedence = Finite 90 in + infix 2 1 (self.pp_bin_op self ctx op) + (self.pp_term self (ctx |> with_binding atom_precedence) a) + (self.pp_term self (ctx |> with_binding atom_precedence) b) + |> parens_if_needed ctx atom_precedence + | Subsumption (p1, p2) -> + let subsume_precedence = Finite 90 in + infix 2 1 subsumes (self.pp_term self (ctx |> with_binding subsume_precedence) p1) + (self.pp_term self (ctx |> with_binding subsume_precedence) p2) + |> parens_if_needed ctx subsume_precedence end; pp_kappa = begin - fun self ppf k -> - let open Format in - match k with - | EmptyHeap -> fprintf ppf "emp" - | PointsTo (loc, t) -> fprintf ppf "@[%s@ ->@ @[< 1>(%a)@]@]" loc (self.pp_term self) t - | SepConj (k1, k2) -> fprintf ppf "@[< 1>(%a)@]@ *@ @[<>(%a)@]" - (self.pp_kappa self) k1 (self.pp_kappa self) k2 + fun self ctx k -> match k with + | EmptyHeap -> string "emp" + | PointsTo (loc, v) -> group ((string loc) ^^ space ^^ sep_arrow ^^ break 1 ^^ (self.pp_term self ctx v)) + | SepConj _ -> + format_as_prefixed_list ~sep:sep_conj + ~destruct:(function SepConj (k1, k2) -> Some (k1, k2) | _ -> None) + ~renderer:(self.pp_kappa self ctx) k end; pp_state = begin - fun self ppf (p, k) -> - Format.fprintf ppf "(%a@ /\\@ %a)" (self.pp_kappa self) k (self.pp_pi self) p - end + fun self ctx (p, k) -> + let conj_precedence = Finite 80 in + match (p, k) with + (* special case to make return stages play nicely with indentation. related: github issue #31 *) + | (Atomic (EQ, {term_desc = Var "res"; _}, t), EmptyHeap) -> + group (string "res" ^^ blank 1 ^^ equals ^^ break 1 ^^ nest 2 (self.pp_term self (ctx |> with_binding conj_precedence) t)) + (* general case *) + | _ -> infix_on_newline 1 conj (self.pp_pi self (ctx |> with_binding conj_precedence) p) + (self.pp_kappa self (ctx |> with_binding conj_precedence) k) + end; } +(** Modify the pretty printer to also output type annotations. + + {b Note}: This function is NOT idempotent; applying this multiple times + will lead to type annotations being repeated in the output. *) let add_type_annotations (pp : pretty_printer) : pretty_printer = -(* TODO add annotations to terms, patterns, core lang, etc.. *) - { pp with - pp_binder = begin - fun self ppf b -> - Format.fprintf ppf "(%s : %a)" - (ident_of_binder b) - (self.pp_typ self) (type_of_binder b) + let open PPrint in + { + pp with + pp_binder = begin fun self ctx b -> + parens (pp.pp_binder self (ctx |> with_binding Negative_inf) b ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx (type_of_binder b))) + end; + pp_term = begin fun self ctx t -> + parens (pp.pp_term self (ctx |> with_binding Negative_inf) t ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx t.term_type)) end; - pp_term = begin - fun self ppf t -> - Format.fprintf ppf "%a : %a" - (pp.pp_term self) t (pp.pp_typ self) t.term_type - end;} + pp_core_lang = begin fun self ctx core -> + parens (pp.pp_core_lang self (ctx |> with_binding Negative_inf) core ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx core.core_type)) + end + } + +(** {1 Printer configuration} *) type config = { cfg_print_types : bool; - cfg_print_spacing : bool + cfg_print_spacing : bool; + cfg_column_width : int; + cfg_ribbon_width : float; } let default_config () = { cfg_print_types = false; - cfg_print_spacing = true + cfg_print_spacing = true; + cfg_column_width = 80; + cfg_ribbon_width = 1.0 } let set_single_line ?(enabled = true) cfg = {cfg with cfg_print_spacing = not enabled} let set_types_display ?(enabled = true) cfg = {cfg with cfg_print_types = enabled} +let set_column_width w cfg = {cfg with cfg_column_width = w} let pp_with_config cfg pp = - let pp = - if cfg.cfg_print_types - then add_type_annotations pp - else pp - in - pp - -let with_changed_out_functions ppf wrapper f = - let out_functions = Format.pp_get_formatter_out_functions ppf () in - Format.pp_set_formatter_out_functions ppf (wrapper out_functions); - let result = f ppf in - Format.pp_set_formatter_out_functions ppf out_functions; - result - -let with_compact_spacing out_functions = - Format.{ - out_functions with - out_newline = ignore; - out_indent = (fun _ -> out_functions.out_indent 1); - out_spaces = (fun _ -> out_functions.out_spaces 1); -} + if cfg.cfg_print_types + then add_type_annotations pp + else pp -let format_with_config ppf cfg f = - if cfg.cfg_print_spacing - then f ppf - else - let@ ppf = with_changed_out_functions ppf with_compact_spacing in - f ppf - -(* We define a separate internal module type for printers, so that - the string_of functions can still derive from [obtain_printers_internal], - while still exposing only the Printers type and the [obtain_printers] function - to the outside. *) +(** { 1 Printing functions }*) module type Printers_internal = sig - val pp_staged_spec : staged_spec fmt - val pp_binder : binder fmt - val pp_typ : typ fmt - val pp_term : term fmt - val pp_pi : pi fmt - val pp_kappa : kappa fmt - val pp_state : state fmt - val pp_pattern : pattern fmt - val pp_core_lang : core_lang fmt -end - -module type Printers = sig - val pp_staged_spec : Format.formatter -> staged_spec -> unit + val pp_staged_spec : staged_spec to_document + val pp_binder : binder to_document + val pp_typ : typ to_document + val pp_term : term to_document + val pp_pi : pi to_document + val pp_kappa : kappa to_document + val pp_state : state to_document + val pp_pattern : pattern to_document + val pp_core_lang : core_lang to_document end -let cast_from_internal (module M : Printers_internal) : (module Printers) = - (module struct - let pp_staged_spec = M.pp_staged_spec - end) - let obtain_printers_internal cfg : (module Printers_internal) = + let ctx = default_printing_context () in let pp = pp_with_config cfg default_printer in (module struct - let pp_staged_spec ppf f = - let@ ppf = format_with_config ppf cfg in - pp.pp_staged_spec pp ppf f - let pp_binder ppf f = - let@ ppf = format_with_config ppf cfg in - pp.pp_binder pp ppf f - let pp_typ ppf t = - let@ ppf = format_with_config ppf cfg in - pp.pp_typ pp ppf t - let pp_term ppf t = - let@ ppf = format_with_config ppf cfg in - pp.pp_term pp ppf t - let pp_pi ppf p = - let@ ppf = format_with_config ppf cfg in - pp.pp_pi pp ppf p - let pp_kappa ppf k = - let@ ppf = format_with_config ppf cfg in - pp.pp_kappa pp ppf k - let pp_state ppf st = - let@ ppf = format_with_config ppf cfg in - pp.pp_state pp ppf st - let pp_pattern ppf pat = - let@ ppf = format_with_config ppf cfg in - pp.pp_pattern pp ppf pat - let pp_core_lang ppf core = - let@ ppf = format_with_config ppf cfg in - pp.pp_core_lang pp ppf core + let pp_staged_spec f = pp.pp_staged_spec pp ctx f + let pp_binder f = pp.pp_binder pp ctx f + let pp_typ t = pp.pp_typ pp ctx t + let pp_term t = pp.pp_term pp ctx t + let pp_pi p = pp.pp_pi pp ctx p + let pp_kappa k = pp.pp_kappa pp ctx k + let pp_state st = pp.pp_state pp ctx st + let pp_pattern pat = pp.pp_pattern pp ctx pat + let pp_core_lang core = pp.pp_core_lang pp ctx core end) -let obtain_printers cfg = cast_from_internal (obtain_printers_internal cfg) - -module Default_internal = (val obtain_printers_internal (default_config ()) : Printers_internal) -module Default = (val obtain_printers (default_config ()) : Printers) +let print_document cfg doc = + (* Note that it is not recommended to use the Format functions for these purposes; see {{:github.com/fpottier/pprint/issues/9}this issue}. *) + let buf = Buffer.create 256 in + begin + if cfg.cfg_print_spacing + then PPrint.ToBuffer.pretty cfg.cfg_ribbon_width cfg.cfg_column_width buf doc + else PPrint.ToBuffer.compact buf doc + end; + Buffer.contents buf let string_of_binder ?(config = default_config ()) b = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_binder b + M.pp_binder b |> print_document config let string_of_type ?(config = default_config ()) t = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_typ t + M.pp_typ t |> print_document config let string_of_pi ?(config = default_config ()) p = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_pi p + M.pp_pi p |> print_document config let string_of_kappa ?(config = default_config ()) k = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_kappa k + M.pp_kappa k |> print_document config let string_of_state ?(config = default_config ()) st = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_state st + M.pp_state st |> print_document config let string_of_pattern ?(config = default_config ()) pat = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_pattern pat + M.pp_pattern pat |> print_document config let string_of_term ?(config = default_config ()) t = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_term t + M.pp_term t |> print_document config let string_of_core_lang ?(config = default_config ()) core = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_core_lang core + M.pp_core_lang core |> print_document config let string_of_staged_spec ?(config = default_config ()) f = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%a" M.pp_staged_spec f + M.pp_staged_spec f |> print_document config let string_of_option ?(none = "") some opt = match opt with @@ -439,60 +626,73 @@ let string_of_list ?(sep=", ") pp elems = let string_of_pred ?(config = default_config ()) pred = let module M = (val obtain_printers_internal config : Printers_internal) in - Format.asprintf "%s(%s)@, =@ %a" pred.p_name (string_of_list (string_of_binder ~config) pred.p_params) M.pp_staged_spec pred.p_body + let open PPrint in + pp_call_like M.pp_binder (pred.p_name, pred.p_params) ^^ space ^^ equals ^^ nest 2 (break 1 ^^ M.pp_staged_spec pred.p_body) + |> print_document config let string_of_type_declaration ?(config = default_config ()) tdecl = let module M = (val obtain_printers_internal config : Printers_internal) in - let open Format in - let pp_inductive ppf constrs = - let pp_constr ppf (name, arg_types) = + let open PPrint in + let pp_inductive constrs = + let pp_constr (name, arg_types) = if List.is_empty arg_types - then fprintf ppf "@[| %s@]" name - else fprintf ppf "@[| %s of@ %a@]" name - (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf "@ * ") M.pp_typ) arg_types + then string name + else (string name) ^^ string "of" ^^ prefixed_list 1 (string "*") (List.map M.pp_typ arg_types) in - pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf "@,") pp_constr ppf constrs + prefixed_list 1 (string "|") (List.map pp_constr constrs) in - let pp_record ppf _r = pp_print_string ppf "record" in - let pp_kind ppf kind = + let pp_record _r = string "record" in + let pp_kind kind = match kind with - | Tdecl_inductive constrs -> pp_inductive ppf constrs - | Tdecl_record r -> pp_record ppf r + | Tdecl_inductive constrs -> pp_inductive constrs + | Tdecl_record r -> pp_record r in - Format.asprintf "type@ (%s)@ %s@ =@,@[%a@]" (string_of_list (string_of_type ~config) tdecl.tdecl_params) - tdecl.tdecl_name - pp_kind tdecl.tdecl_kind + group (string "type" ^^ space ^^ M.pp_typ (TConstr (tdecl.tdecl_name, tdecl.tdecl_params)) ^^ space ^^ break 1 ^^ + pp_kind tdecl.tdecl_kind) + |> print_document config -let pp_assoc_list pp_key pp_value ppf m = - let pp_element ppf (k, v) = - Format.fprintf ppf "@[%a -> %a@]" pp_key k pp_value v +let pp_assoc_list pp_key pp_value m = + let open PPrint in + let pp_element (k, v) = + (pp_key k) ^^ space ^^ string "->" ^^ space ^^ (pp_value v) in - Format.fprintf ppf "@[{%a}@]" (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ") pp_element) m + braces (flow (semi ^^ blank 1) (List.map pp_element m)) let string_of_abs_env ?(config = default_config ()) abs_env = let module M = (val obtain_printers_internal config : Printers_internal) in + let open PPrint in let variable_types = abs_env.vartypes |> SMap.bindings in let type_eqs = (TMap.map (fun t -> U.get t) !(abs_env.equalities)) |> TMap.bindings in - Format.asprintf "@[vars:@ %a,@ eqs:@ %a@]" (pp_assoc_list Format.pp_print_string M.pp_typ) variable_types (pp_assoc_list M.pp_typ M.pp_typ) type_eqs + brackets (group (string "vars:" ^^ space ^^ pp_assoc_list string M.pp_typ variable_types ^^ comma ^^ break 1 + ^^ string "eqs:" ^^ pp_assoc_list M.pp_typ M.pp_typ type_eqs)) + |> print_document config + +(* tests *) let%expect_test "syntax of output" = - let module With_types = (val obtain_printers (default_config () |> set_types_display) : Printers) in - let module Compact = (val obtain_printers (default_config () |> set_single_line) : Printers) in let int_var v = {term_desc = Var v; term_type = Int} in let cint c = {term_desc = Const (Num c); term_type = Int} in let (+~) a b = {term_desc = BinOp (Plus, a, b); term_type = Int} in let (=~) a b = Atomic (EQ, a, b) in let f1 = NormalReturn (int_var "res" =~ cint 0, EmptyHeap) in - Format.printf "%a" With_types.pp_staged_spec f1; + print_string (string_of_staged_spec ~config:(default_config () |> set_types_display) f1); [%expect {| |}]; (* f2 can be any output long enough to force default Format behavior to break lines *) let to_sum = List.init 20 Fun.id |> List.map cint in let f2 = NormalReturn (int_var "res" =~ List.fold_left (+~) (cint 0) to_sum, EmptyHeap) in - Format.printf "compacted: %a" Compact.pp_staged_spec f2; + print_string (string_of_staged_spec ~config:(default_config () |> set_single_line) f2); + [%expect {| |}]; + + (* now test that the column width can change the output *) + print_string (string_of_staged_spec ~config:(default_config () |> set_column_width 20) f2); [%expect {| |}]; let subpat = List.init 40 (Fun.const {pattern_desc = PAny; pattern_type = Int}) in let p1 = {pattern_desc = PConstr ("with_lots_of_arguments", subpat); pattern_type = TConstr ("big_type", [])} in Format.printf "expanded: %s\ncompacted: %s\n" (string_of_pattern p1) (string_of_pattern ~config:(default_config () |> set_single_line) p1); + [%expect {| |}]; + + let t = (cint 1 +~ cint 2) in + Format.printf "expanded: %s\n" (string_of_term t); [%expect {| |}];; diff --git a/lib/hipcore_typed/Pretty.mli b/lib/hipcore_typed/Pretty.mli index 9a7b89a6..12b02c4f 100644 --- a/lib/hipcore_typed/Pretty.mli +++ b/lib/hipcore_typed/Pretty.mli @@ -10,23 +10,7 @@ val set_single_line : ?enabled:bool -> config -> config val set_types_display : ?enabled:bool -> config -> config -(* what else would be useful... set_unicode? set_colors? *) - -(* example... *) - -(** {1 Pretty-printing functions } *) - -(** The pretty-printers are packaged into a module, parametrized by - the configuration. If you only need the default configuration, - the associated printers are available under [Default].*) - -module type Printers = sig - val pp_staged_spec : Format.formatter -> staged_spec -> unit -end - -module Default : Printers - -val obtain_printers : config -> (module Printers) +val set_column_width : int -> config -> config (** { 1 String converters } *) diff --git a/lib/hipcore_typed/dune b/lib/hipcore_typed/dune index 13630879..57e94274 100644 --- a/lib/hipcore_typed/dune +++ b/lib/hipcore_typed/dune @@ -1,8 +1,7 @@ (library (name hipcore_typed) (public_name heifer.hipcore_typed) - (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast - dynamic_typing) - (libraries debug unionFind str utils hipcore) + (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast dynamic_typing) + (libraries debug unionFind str utils hipcore pprint) (inline_tests) (preprocess (pps ppx_expect ppx_deriving.std visitors.ppx))) diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml index 7a1acba6..7cb873b6 100644 --- a/lib/hipcore_typed/subst.ml +++ b/lib/hipcore_typed/subst.ml @@ -4,7 +4,6 @@ open Hipcore.Types open Hipcore.Variables open Rewrite_context open Utils.Hstdlib -open Utils.Misc type 'a subst_context = | Sctx_staged : staged_spec subst_context diff --git a/lib/hipcore_typed/variables.ml b/lib/hipcore_typed/variables.ml index 8aeb6268..03d615f3 100644 --- a/lib/hipcore_typed/variables.ml +++ b/lib/hipcore_typed/variables.ml @@ -5,10 +5,14 @@ let res_var ~typ = var "res" ~typ let eq_res ?(typ = Any) t = eq (res_var ~typ) t -let is_eq_res = function - | Atomic (EQ, {term_desc = Var "res"; _}, _) - | Atomic (EQ, _, {term_desc = Var "res"; _}) -> true - | _ -> false +(** Given a pure formula of the form [res = t], return [Some t]. + Return [None] instead of it is not of this form. *) +let eq_res_term = function + | Atomic (EQ, {term_desc = Var "res"; _}, t) + | Atomic (EQ, t, {term_desc = Var "res"; _}) -> Some t + | _ -> None + +let is_eq_res t = eq_res_term t |> Option.is_some (* share these functions with the untyped module *) let counter = Hipcore.Variables.counter diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml index d02e3227..35694cd0 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -97,17 +97,16 @@ let report_header ~kind ~name = let normal_report ~kind ~name ~inferred_spec ~given_spec ~result = let header = report_header ~kind ~name in - let open Default in let inferred_spec_string = Format.asprintf - "[ Inferred specification ]\n%a\n" - pp_staged_spec inferred_spec + "[ Inferred specification ]\n%s\n" + (string_of_staged_spec inferred_spec) in let given_spec_string = match given_spec with | Some given_spec -> Format.asprintf - "[ Given specification ]\n%a\n" - pp_staged_spec given_spec + "[ Given specification ]\n%s\n" + (string_of_staged_spec given_spec) | None -> "" in diff --git a/lib/hiplib/tests.ml b/lib/hiplib/tests.ml index 1010f47f..f625e68a 100644 --- a/lib/hiplib/tests.ml +++ b/lib/hiplib/tests.ml @@ -56,9 +56,9 @@ let%expect_test "rewriting" = let spec s = pipeline (Ocamlfrontend.Annotation.parse_staged_spec, Hipcore_typed.Retypehip.retype_staged_spec, Hipprover.Infer_types.infer_types_staged_spec) s in let test rule target = let b1 = rewrite_all rule target in - Format.printf "rewrite %s@." (string_of_uterm target); - Format.printf "with %s@." (string_of_rule rule); - Format.printf "result: %s@." (string_of_uterm b1) + Printf.printf "rewrite %s\n" (string_of_uterm target); + Printf.printf "with %s\n" (string_of_rule rule); + Printf.printf "result: %s\n" (string_of_uterm b1) in test Staged.("ens emp" ==> "ens false") (Staged (spec "ens emp; ens emp")); diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index 0241b16e..4b319872 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -1,7 +1,6 @@ open Hipcore_typed open Typedhip open Pretty -open With_types open Hipcore.Types open Debug open Utils diff --git a/lib/hipprover/rewriting.ml b/lib/hipprover/rewriting.ml index 52ae8077..022df21a 100644 --- a/lib/hipprover/rewriting.ml +++ b/lib/hipprover/rewriting.ml @@ -1350,7 +1350,7 @@ module Deep = struct | Var s -> s | Inst _ -> "" | Constr (f, a) -> - Format.asprintf "%s%s" f (string_of_list ~sep:", " string_of_pattern a) + Format.asprintf "%s%s" f (Pretty.string_of_list ~sep:", " string_of_pattern a) let v s = Var s let and_ p1 p2 = Constr ("and", [p1; p2]) From 2bbf9f94c3179d482c95fcee791c78081f8aecdd Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Fri, 5 Sep 2025 16:42:35 +0800 Subject: [PATCH 10/15] expose globally configurable output --- lib/hipcore_typed/Pretty.ml | 52 +++++++++++++++++++++++------------ lib/hipcore_typed/Pretty.mli | 26 ++++++++++++++++-- lib/hipcore_typed/patterns.ml | 2 +- lib/hipprover/rewriting.ml | 2 +- 4 files changed, 60 insertions(+), 22 deletions(-) diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index be92948a..98af9af2 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -525,13 +525,19 @@ type config = { cfg_ribbon_width : float; } -let default_config () = { +let default_config = { cfg_print_types = false; cfg_print_spacing = true; cfg_column_width = 80; cfg_ribbon_width = 1.0 } +let current_config_ = ref default_config + +let current_config () = !current_config_ + +let set_current_config f = current_config_ := f !current_config_ + let set_single_line ?(enabled = true) cfg = {cfg with cfg_print_spacing = not enabled} let set_types_display ?(enabled = true) cfg = {cfg with cfg_print_types = enabled} let set_column_width w cfg = {cfg with cfg_column_width = w} @@ -571,7 +577,6 @@ let obtain_printers_internal cfg : (module Printers_internal) = end) let print_document cfg doc = - (* Note that it is not recommended to use the Format functions for these purposes; see {{:github.com/fpottier/pprint/issues/9}this issue}. *) let buf = Buffer.create 256 in begin if cfg.cfg_print_spacing @@ -580,39 +585,48 @@ let print_document cfg doc = end; Buffer.contents buf -let string_of_binder ?(config = default_config ()) b = +let string_of_binder ?config b = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_binder b |> print_document config -let string_of_type ?(config = default_config ()) t = +let string_of_type ?config t = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_typ t |> print_document config -let string_of_pi ?(config = default_config ()) p = +let string_of_pi ?config p = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_pi p |> print_document config -let string_of_kappa ?(config = default_config ()) k = +let string_of_kappa ?config k = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_kappa k |> print_document config -let string_of_state ?(config = default_config ()) st = +let string_of_state ?config st = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_state st |> print_document config -let string_of_pattern ?(config = default_config ()) pat = +let string_of_pattern ?config pat = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_pattern pat |> print_document config -let string_of_term ?(config = default_config ()) t = +let string_of_term ?config t = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_term t |> print_document config -let string_of_core_lang ?(config = default_config ()) core = +let string_of_core_lang ?config core = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_core_lang core |> print_document config -let string_of_staged_spec ?(config = default_config ()) f = +let string_of_staged_spec ?config f = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in M.pp_staged_spec f |> print_document config @@ -624,13 +638,15 @@ let string_of_option ?(none = "") some opt = let string_of_list ?(sep=", ") pp elems = List.map pp elems |> String.concat sep -let string_of_pred ?(config = default_config ()) pred = +let string_of_pred ?config pred = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in let open PPrint in pp_call_like M.pp_binder (pred.p_name, pred.p_params) ^^ space ^^ equals ^^ nest 2 (break 1 ^^ M.pp_staged_spec pred.p_body) |> print_document config -let string_of_type_declaration ?(config = default_config ()) tdecl = +let string_of_type_declaration ?config tdecl = + let config = Option.value config ~default:(current_config ()) in let module M = (val obtain_printers_internal config : Printers_internal) in let open PPrint in let pp_inductive constrs = @@ -658,7 +674,7 @@ let pp_assoc_list pp_key pp_value m = in braces (flow (semi ^^ blank 1) (List.map pp_element m)) -let string_of_abs_env ?(config = default_config ()) abs_env = +let string_of_abs_env ?(config = default_config) abs_env = let module M = (val obtain_printers_internal config : Printers_internal) in let open PPrint in let variable_types = abs_env.vartypes |> SMap.bindings in @@ -675,22 +691,22 @@ let%expect_test "syntax of output" = let (+~) a b = {term_desc = BinOp (Plus, a, b); term_type = Int} in let (=~) a b = Atomic (EQ, a, b) in let f1 = NormalReturn (int_var "res" =~ cint 0, EmptyHeap) in - print_string (string_of_staged_spec ~config:(default_config () |> set_types_display) f1); + print_string (string_of_staged_spec ~config:(default_config |> set_types_display) f1); [%expect {| |}]; (* f2 can be any output long enough to force default Format behavior to break lines *) let to_sum = List.init 20 Fun.id |> List.map cint in let f2 = NormalReturn (int_var "res" =~ List.fold_left (+~) (cint 0) to_sum, EmptyHeap) in - print_string (string_of_staged_spec ~config:(default_config () |> set_single_line) f2); + print_string (string_of_staged_spec ~config:(default_config |> set_single_line) f2); [%expect {| |}]; (* now test that the column width can change the output *) - print_string (string_of_staged_spec ~config:(default_config () |> set_column_width 20) f2); + print_string (string_of_staged_spec ~config:(default_config |> set_column_width 20) f2); [%expect {| |}]; let subpat = List.init 40 (Fun.const {pattern_desc = PAny; pattern_type = Int}) in let p1 = {pattern_desc = PConstr ("with_lots_of_arguments", subpat); pattern_type = TConstr ("big_type", [])} in - Format.printf "expanded: %s\ncompacted: %s\n" (string_of_pattern p1) (string_of_pattern ~config:(default_config () |> set_single_line) p1); + Format.printf "expanded: %s\ncompacted: %s\n" (string_of_pattern p1) (string_of_pattern ~config:(default_config |> set_single_line) p1); [%expect {| |}]; let t = (cint 1 +~ cint 2) in diff --git a/lib/hipcore_typed/Pretty.mli b/lib/hipcore_typed/Pretty.mli index 12b02c4f..90f789fb 100644 --- a/lib/hipcore_typed/Pretty.mli +++ b/lib/hipcore_typed/Pretty.mli @@ -1,21 +1,43 @@ open Typedhip +(** Functions for rendering formulas, terms, etc. with spacing and indentation. + + {b Note:} The underlying library used to implement these pretty-printers is incompatible with [Format] + (see {{:github.com/fpottier/pprint/issues/9}this issue} for details). Using their output within + [Format]'s printing functions may lead to unintuitive line break placements. +*) + (** { 1 Pretty-printer configuration } *) type config -val default_config : unit -> config +(** A reasonable starting configuration, with formatting enabled, a column width of 80 + and type annotations disabled. *) +val default_config : config + +(** The current global configuration. This is initialized to [default_config], and + can be changed using [set_current_config]. *) +val current_config : unit -> config +(** Mutate the current configuration. *) +val set_current_config : (config -> config) -> unit + +(** Disable line breaks and indentation, leaving all output on a single line. + This overrides [set_column_width]. *) val set_single_line : ?enabled:bool -> config -> config +(** Enable type annotations (of terms, binders, etc.) in the output. *) val set_types_display : ?enabled:bool -> config -> config +(** Set the maximum length of one line of the printer's output. *) val set_column_width : int -> config -> config (** { 1 String converters } *) +(** All converters accept an optional [?config] argument, which defaults to [current_config]. *) + (** Note that this is intended to display human-readable output. If - you need to obtain the underlying identifier, use [ident_of_binder] instead. *) + you need to obtain the underlying identifier, use [Typedhip.ident_of_binder] instead. *) val string_of_binder : ?config:config -> binder -> string val string_of_type : ?config:config -> typ -> string diff --git a/lib/hipcore_typed/patterns.ml b/lib/hipcore_typed/patterns.ml index 9c70e0d4..1421c17a 100644 --- a/lib/hipcore_typed/patterns.ml +++ b/lib/hipcore_typed/patterns.ml @@ -224,7 +224,7 @@ module Testing = struct } open Pretty let output pats = - let config = default_config () |> set_single_line in + let config = default_config |> set_single_line in String.concat " | " (List.map (fun (pat, guard) -> if guard = ctrue diff --git a/lib/hipprover/rewriting.ml b/lib/hipprover/rewriting.ml index 022df21a..3b6b4daa 100644 --- a/lib/hipprover/rewriting.ml +++ b/lib/hipprover/rewriting.ml @@ -1107,7 +1107,7 @@ let%expect_test "rewriting" = (* type-aware rewriting *) let string_of_uterm_with_types t = - let config = default_config () |> set_types_display in + let config = default_config |> set_types_display in match t with | Staged s -> string_of_staged_spec ~config s | Pure p -> string_of_pi ~config p From b09544ac452d300bd9373447f2b4b09a84fc8abd Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Fri, 5 Sep 2025 17:03:16 +0800 Subject: [PATCH 11/15] toggle output of types using env var --- main/hip.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/main/hip.ml b/main/hip.ml index bb6376ef..f66fe27e 100644 --- a/main/hip.ml +++ b/main/hip.ml @@ -26,6 +26,11 @@ let () = Option.bind (Sys.getenv_opt "CTF") int_of_string_opt |> Option.value ~default:0 > 0 in + begin + if Option.bind (Sys.getenv_opt "SHOW_TYPES") int_of_string_opt + |> Option.value ~default:0 > 0 + then Hipcore_typed.Pretty.(set_current_config set_types_display) + end; if Unix.isatty Unix.stdout && not !Hiplib.file_mode && not ctf then Hipcore.Pretty.colours := `Ansi; Hiplib.Debug.init ~ctf ~org:!Hiplib.file_mode (Sys.getenv_opt "DEBUG"); From 8b4f390f5e66977d40f75abe5c1f456a3338db89 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Fri, 5 Sep 2025 17:09:49 +0800 Subject: [PATCH 12/15] change formatting of tests --- lib/hipcore_typed/Pretty.ml | 22 ++++++++--- lib/hipcore_typed/patterns.ml | 12 +++--- lib/hipcore_typed/subst.ml | 4 +- lib/hiplib/tests.ml | 24 ++++++------ lib/hipprover/biab.ml | 12 +++--- lib/hipprover/entail.ml | 18 ++++----- lib/hipprover/infer_types.ml | 18 ++++----- lib/hipprover/normalize.ml | 27 ++++++------- lib/hipprover/rewriting.ml | 72 +++++++++++++++++------------------ lib/hipprover/rewriting2.ml | 8 ++-- lib/hipprover/simpl.ml | 10 ++--- 11 files changed, 118 insertions(+), 109 deletions(-) diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index 98af9af2..b2c2511c 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -692,23 +692,35 @@ let%expect_test "syntax of output" = let (=~) a b = Atomic (EQ, a, b) in let f1 = NormalReturn (int_var "res" =~ cint 0, EmptyHeap) in print_string (string_of_staged_spec ~config:(default_config |> set_types_display) f1); - [%expect {| |}]; + [%expect {| ens (res = (0 : int)) |}]; (* f2 can be any output long enough to force default Format behavior to break lines *) let to_sum = List.init 20 Fun.id |> List.map cint in let f2 = NormalReturn (int_var "res" =~ List.fold_left (+~) (cint 0) to_sum, EmptyHeap) in print_string (string_of_staged_spec ~config:(default_config |> set_single_line) f2); - [%expect {| |}]; + [%expect {| ens (res = 0 + 0 + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19) |}]; (* now test that the column width can change the output *) print_string (string_of_staged_spec ~config:(default_config |> set_column_width 20) f2); - [%expect {| |}]; + [%expect {| + ens (res = + 0 + 0 + 1 + 2 + 3 + + 4 + 5 + 6 + 7 + + 8 + 9 + 10 + + 11 + 12 + 13 + + 14 + 15 + 16 + + 17 + 18 + 19) + |}]; let subpat = List.init 40 (Fun.const {pattern_desc = PAny; pattern_type = Int}) in let p1 = {pattern_desc = PConstr ("with_lots_of_arguments", subpat); pattern_type = TConstr ("big_type", [])} in Format.printf "expanded: %s\ncompacted: %s\n" (string_of_pattern p1) (string_of_pattern ~config:(default_config |> set_single_line) p1); - [%expect {| |}]; + [%expect {| + expanded: with_lots_of_arguments(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, + _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _) + compacted: with_lots_of_arguments(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _) + |}]; let t = (cint 1 +~ cint 2) in Format.printf "expanded: %s\n" (string_of_term t); - [%expect {| |}];; + [%expect {| expanded: 1 + 2 |}];; diff --git a/lib/hipcore_typed/patterns.ml b/lib/hipcore_typed/patterns.ml index 1421c17a..381bd97f 100644 --- a/lib/hipcore_typed/patterns.ml +++ b/lib/hipcore_typed/patterns.ml @@ -254,14 +254,14 @@ let%expect_test "complement" = let __ = Testing.any ~args:[Int] "test_type" in output (complement (guarded (b __))); - [%expect{| A() | D(_, _) |}]; + [%expect{| A | D(_, _) |}]; output (complement (guarded (d (b __, a)))); - [%expect{| A() | B(_) | D(B(_), B(_)) | D(B(_), D(_, _)) | D(A(), A()) | D(A(), B(_)) | D(A(), D(_, _)) | D(D(_, _), A()) | D(D(_, _), B(_)) | D(D(_, _), D(_, _)) |}]; + [%expect{| A | B(_) | D(B(_), B(_)) | D(B(_), D(_, _)) | D(A, A) | D(A, B(_)) | D(A, D(_, _)) | D(D(_, _), A) | D(D(_, _), B(_)) | D(D(_, _), D(_, _)) |}]; let __ = Testing.any "nat" in output (complement (guarded (s (as_ ~name:"s" (s __))))); - [%expect{| Z() | S((Z()) as s) |}]; + [%expect{| Z | S(Z as s) |}]; ;; let%expect_test "intersect" = @@ -270,7 +270,7 @@ let%expect_test "intersect" = let __ = Testing.any ~args:[Int] "test_type" in output (intersect [guarded (d (pvar "a", pvar "b"))] [guarded (b (pvar "x")); guarded (d (__, d (__, pvar "d")))]); - [%expect{| D(a, (D(_, d)) as b) |}]; + [%expect{| D(a, D(_, d) as b) |}]; output (intersect [guarded (b __)] [guarded (d (__, __))]); [%expect{| |}]; @@ -286,12 +286,12 @@ let%expect_test "exclude" = let __ = Testing.any ~args:[Int] "test_type" in output (exclude (guarded (d (__, __))) [guarded a; guarded (d (b __, __))]); - [%expect{| D(A(), _) | D(D(_, _), _) |}]; + [%expect{| D(A, _) | D(D(_, _), _) |}]; output (exclude (guarded (b __)) []); [%expect{| B(_) |}]; let __ = Testing.any "nat" in output (exclude (guarded (s (as_ ~name:"s" z)) ~condition:(rel EQ (var "s") (var "t") )) [guarded z; guarded (s (as_ ~name:"s" (s __)))]); - [%expect{| S(((Z()) as patd2) as s) when (s==t) |}]; + [%expect{| S(Z as patd2 as s) when s == t |}]; ;; diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml index 7cb873b6..ed12a439 100644 --- a/lib/hipcore_typed/subst.ml +++ b/lib/hipcore_typed/subst.ml @@ -232,7 +232,7 @@ let%expect_test "subst" = ens ~p:(eq (v "x") (v "x")) (); Exists (("x", Int), ens ~p:(eq (v "x") (num 1)) ()); ]); - [%expect {| (ens x=x; ex x. (ens x=1))[y/x] = ens y=y; ex x. (ens x=1) |}]; + [%expect {| (ens (x = x /\ emp); ex x. (ens (x = 1 /\ emp)))[y/x] = ens (y = y /\ emp); ex x. (ens (x = 1 /\ emp)) |}]; test [("x", v "z")] (Exists (("z", Int), ens ~p:(eq (v "z") (v "x")) ())); - [%expect {| (ex z. (ens z=x))[z/x] = ex z0. (ens z0=z) |}] + [%expect {| (ex z. (ens (z = x /\ emp)))[z/x] = ex z0. (ens (z0 = z /\ emp)) |}] diff --git a/lib/hiplib/tests.ml b/lib/hiplib/tests.ml index f625e68a..8110e795 100644 --- a/lib/hiplib/tests.ml +++ b/lib/hiplib/tests.ml @@ -64,33 +64,33 @@ let%expect_test "rewriting" = test Staged.("ens emp" ==> "ens false") (Staged (spec "ens emp; ens emp")); [%expect {| - rewrite ens emp; ens emp - with ens emp ==> ens F - result: ens F; ens F + rewrite ens (T /\ emp); ens (T /\ emp) + with ens (T /\ emp) ==> ens (F /\ emp) + result: ens (F /\ emp); ens (F /\ emp) |}]; test Pure.("true" ==> "false") (Staged (spec "ens emp; ens emp")); [%expect {| - rewrite ens emp; ens emp + rewrite ens (T /\ emp); ens (T /\ emp) with T ==> F - result: ens F; ens F + result: ens (F /\ emp); ens (F /\ emp) |}]; test Heap.("x->1" ==> "x->2") (Staged (spec "ens x->1; ens emp")); [%expect {| - rewrite ens x->1; ens emp - with x->1 ==> x->2 - result: ens x->2; ens emp + rewrite ens (T /\ x -> 1); ens (T /\ emp) + with x -> 1 ==> x -> 2 + result: ens (T /\ x -> 2); ens (T /\ emp) |}]; test Term.("1" ==> "2") (Staged (spec "ens x->1; ens emp")); [%expect {| - rewrite ens x->1; ens emp + rewrite ens (T /\ x -> 1); ens (T /\ emp) with 1 ==> 2 - result: ens x->2; ens emp + result: ens (T /\ x -> 2); ens (T /\ emp) |}] let%expect_test "autorewrite" = @@ -106,8 +106,8 @@ let%expect_test "autorewrite" = test db (Staged (spec "ens x=true/\\true/\\true/\\true")); [%expect {| - start: ens x=true/\T/\T/\T - result: ens x=true/\T + start: ens (x = true /\ T /\ T /\ T /\ emp) + result: ens (x = true /\ T /\ emp) |}] (* diff --git a/lib/hipprover/biab.ml b/lib/hipprover/biab.ml index d2535a9b..a6bfe6eb 100644 --- a/lib/hipprover/biab.ml +++ b/lib/hipprover/biab.ml @@ -79,7 +79,7 @@ let%expect_test _ = test emp_biab_ctx h1 h2; [%expect {| - emp * x->1 |- x->1 * emp + emp * x -> 1 |- x -> 1 * emp T |}] in @@ -89,7 +89,7 @@ let%expect_test _ = test emp_biab_ctx h1 h2; [%expect {| - y->2 * emp |- emp * x->1 + y -> 2 * emp |- emp * x -> 1 T |}] in @@ -99,8 +99,8 @@ let%expect_test _ = test emp_biab_ctx h1 h2; [%expect {| - emp * x->a |- x->a * emp - a=1 + emp * x -> a |- x -> a * emp + a = 1 |}] in let _ = @@ -109,8 +109,8 @@ let%expect_test _ = test emp_biab_ctx h1 h2; [%expect {| - emp * v14->0*v15->2 |- v14->0*v15->2 * emp - 2=(1 + 1) + emp * v14 -> 0 * v15 -> 2 |- v14 -> 0 * v15 -> 2 * emp + 2 = 1 + 1 |}] in () diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index 4b319872..b55c459c 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -498,19 +498,19 @@ let%expect_test _ = [%expect {| * search | _1 - (ens emp) \/ (ens emp) |- (ens F) \/ (ens emp) + ens (T /\ emp) \/ ens (T /\ emp) |- ens (F /\ emp) \/ ens (T /\ emp) * disj left | _2 left branch ** search | _3 - ens emp |- (ens F) \/ (ens emp) + ens (T /\ emp) |- ens (F /\ emp) \/ ens (T /\ emp) ** disj right | _4 left branch *** search | _5 - ens emp |- ens F + ens (T /\ emp) |- ens (F /\ emp) *** STUCK | _6 @@ -521,7 +521,7 @@ let%expect_test _ = right branch *** search | _9 - ens emp |- ens emp + ens (T /\ emp) |- ens (T /\ emp) *** ens ens | _10 ok @@ -530,13 +530,13 @@ let%expect_test _ = right branch **** search | _12 - ens emp |- (ens F) \/ (ens emp) + ens (T /\ emp) |- ens (F /\ emp) \/ ens (T /\ emp) **** disj right | _13 left branch ***** search | _14 - ens emp |- ens F + ens (T /\ emp) |- ens (F /\ emp) ***** STUCK | _15 @@ -547,7 +547,7 @@ let%expect_test _ = right branch ***** search | _18 - ens emp |- ens emp + ens (T /\ emp) |- ens (T /\ emp) ***** ens ens | _19 ok @@ -565,9 +565,9 @@ let%expect_test _ = left branch * done | _24 - (ens emp) \/ (ens emp) + ens (T /\ emp) \/ ens (T /\ emp) ⊑ - (ens F) \/ (ens emp) + ens (F /\ emp) \/ ens (T /\ emp) <============================================================ constants: [] diff --git a/lib/hipprover/infer_types.ml b/lib/hipprover/infer_types.ml index 64616ad5..9639a55f 100644 --- a/lib/hipprover/infer_types.ml +++ b/lib/hipprover/infer_types.ml @@ -608,10 +608,10 @@ let%expect_test "unification with type constructors" = let _, env = unify_types t3 t4 env in output_simplified_types env [t1; t2; t3; t4]; [%expect {| - t0: ((int) list) list - t1: ((int) list) list - t2: (int) list - t3: (int) list + t0: int list list + t1: int list list + t2: int list + t3: int list |}] let%expect_test "unification" = @@ -626,10 +626,10 @@ let%expect_test "unification" = let _, env = unify_types t5 t3 env in output_simplified_types env [t1; t2; t3; t4; t5]; [%expect {| - t0: (int) list - t1: (int) list + t0: int list + t1: int list t2: unit - t3: (int) list + t3: int list t4: unit |}] @@ -640,7 +640,7 @@ let%expect_test "unsolvable unification: cyclic solution" = let t2 = TConstr ("list", [TVar "a"]) in let _ = unify_types t1 t2 env in output_simplified_types env [t1; t2]; - [@@expect.uncaught_exn {| ("Cyclic_type('a, ('a) list)") |}] + [@@expect.uncaught_exn {| ("Cyclic_type('a, 'a list)") |}] let%expect_test "unsolvable unification: cycle in environment" = Printexc.record_backtrace false; @@ -650,7 +650,7 @@ let%expect_test "unsolvable unification: cycle in environment" = let t2 = TConstr ("list", [TVar "b"]) in let _ = unify_types t1 t2 env in output_simplified_types env [t1; t2] - [@@expect.uncaught_exn {| ("Cyclic_type('a, ('a) list)") |}] + [@@expect.uncaught_exn {| ("Cyclic_type('a, 'a list)") |}] let%expect_test "unsolvable unification: incompatible types" = diff --git a/lib/hipprover/normalize.ml b/lib/hipprover/normalize.ml index 97df2019..9f1f6ca1 100644 --- a/lib/hipprover/normalize.ml +++ b/lib/hipprover/normalize.ml @@ -349,7 +349,10 @@ let%expect_test "rules" = (* let output = disj [bind "x" f1 fk; bind "x" f2 fk] in *) test norm_bind_disj input; [%expect - {| (let x = (ens res=1) in (ens res=(x + 1))) \/ (let x = (ens res=2) in (ens res=(x + 1))) |}] + {| + (ens (res = 1)); x. (ens (res = x + 1)) + \/ (ens (res = 2)); x. (ens (res = x + 1)) + |}] in let _ = let f = ens ~p:(eq res_var (num 1)) () in @@ -357,7 +360,7 @@ let%expect_test "rules" = let input = bind ("x", Int) (seq [f; f]) fk in test norm_bind_seq_ens input; [%expect - {| ens res=1; let x = (ens res=1) in (ens res=(x + 1)) |}] + {| ens (res = 1); (ens (res = 1)); x. (ens (res = x + 1)) |}] in let _ = let ens_heap = NormalReturn (True, PointsTo ("x", num 1)) in @@ -365,9 +368,7 @@ let%expect_test "rules" = let input = seq [ens_heap; ens_pure] in test norm_ens_heap_ens_pure input; [%expect - {| - ens x=1; ens x->1 - |}] + {| ens (x = 1 /\ emp); ens (T /\ x -> 1) |}] in let _ = let ens_heap = NormalReturn (True, PointsTo ("x", num 1)) in @@ -375,9 +376,7 @@ let%expect_test "rules" = let input = seq [ens_heap; ens_res] in test norm_ens_heap_ens_pure input; [%expect - {| - ens x->1; ens res=69 - |}] + {| ens (T /\ x -> 1); ens (res = 69) |}] in let _ = let ens_heap = NormalReturn (True, PointsTo ("x", num 1)) in @@ -386,31 +385,29 @@ let%expect_test "rules" = let input = seq [ens_heap; ens_res; f] in test norm_seq_ens_heap_ens_pure input; [%expect - {| - ens x->1; ens res=69; ens res=42 - |}] + {| ens (T /\ x -> 1); ens (res = 69); ens (res = 42) |}] in let _ = let input = Bind (("x", Int), Exists (("y", Int), (ens ~p:(eq (v "res") (num 2)) ())), ens ~p:(eq (v "x") (num 1)) ()) in test norm_bind_ex input; [%expect - {| ex y. (let x = (ens res=2) in (ens x=1)) |}] + {| ex y. ((ens (res = 2)); x. ens (x = 1 /\ emp)) |}] in let _ = let input = Bind (("x", Int), ForAll (("y", Int), (ens ~p:(eq (v "res") (num 2)) ())), ens ~p:(eq (v "x") (num 1)) ()) in test norm_bind_all input; [%expect - {| forall y. (let x = (ens res=2) in (ens x=1)) |}] + {| forall y. ((ens (res = 2)); x. ens (x = 1 /\ emp)) |}] in let _ = let input = Bind (("x", Int), ens ~p:(eq (v "y") (num 2)) (), ens ~p:(eq (v "res") (v "x")) ()) in test norm_bind_trivial input; [%expect - {| ens y=2 |}]; + {| ens (y = 2 /\ emp) |}]; let input = Bind (("z", Int), ens ~p:(eq (v "y") (num 2)) (), ens ~p:(eq (v "res") (v "x")) ()) in test norm_bind_trivial input; [%expect - {| let z = (ens y=2) in (ens res=x) |}] + {| (ens (y = 2 /\ emp)); z. ens (res = x) |}] in () diff --git a/lib/hipprover/rewriting.ml b/lib/hipprover/rewriting.ml index 3b6b4daa..fb683796 100644 --- a/lib/hipprover/rewriting.ml +++ b/lib/hipprover/rewriting.ml @@ -973,7 +973,7 @@ let%expect_test "unification and substitution" = let a = Staged (seq [uvar "n"; ens ()]) in let b = Staged (seq [ens ~p:(And (True, False)) (); ens ()]) in test a b; - [%expect {| ens T/\F; ens emp |}]; + [%expect {| ens (T /\ F /\ emp); ens (T /\ emp) |}]; let a = Staged (seq [uvar "n"; uvar "n"; ens ()]) in let b = @@ -982,7 +982,7 @@ let%expect_test "unification and substitution" = [ens ~p:(And (True, False)) (); ens ~p:(And (True, False)) (); ens ()]) in test a b; - [%expect {| ens T/\F; ens T/\F; ens emp |}] + [%expect {| ens (T /\ F /\ emp); ens (T /\ F /\ emp); ens (T /\ emp) |}] let%expect_test "rewriting" = let open Syntax in @@ -1000,25 +1000,25 @@ let%expect_test "rewriting" = (Staged (seq [ens ~p:(Not True) (); ens ~p:(And (True, False)) (); ens ()])); [%expect {| - rewrite ens not(T); ens T/\F; ens emp - with __n(); ens emp ==> __n(); __n(); ens F - result: ens not(T); ens T/\F; ens T/\F; ens F + rewrite ens (~T /\ emp); ens (T /\ F /\ emp); ens (T /\ emp) + with __n(); ens (T /\ emp) ==> __n(); __n(); ens (F /\ emp) + result: ens (~T /\ emp); ens (T /\ F /\ emp); ens (T /\ F /\ emp); ens (F /\ emp) |}]; test (Staged.rule (ens ()) (ens ~p:False ())) (Staged (seq [ens (); ens ()])); [%expect {| - rewrite ens emp; ens emp - with ens emp ==> ens F - result: ens F; ens F + rewrite ens (T /\ emp); ens (T /\ emp) + with ens (T /\ emp) ==> ens (F /\ emp) + result: ens (F /\ emp); ens (F /\ emp) |}]; test (Pure.rule True False) (Staged (seq [ens (); ens ()])); [%expect {| - rewrite ens emp; ens emp + rewrite ens (T /\ emp); ens (T /\ emp) with T ==> F - result: ens F; ens F + result: ens (F /\ emp); ens (F /\ emp) |}]; test @@ -1026,9 +1026,9 @@ let%expect_test "rewriting" = (Staged (seq [ens ~h:(PointsTo ("x", num 1)) (); ens ()])); [%expect {| - rewrite ens x->1; ens emp - with x->1 ==> x->2 - result: ens x->2; ens emp + rewrite ens (T /\ x -> 1); ens (T /\ emp) + with x -> 1 ==> x -> 2 + result: ens (T /\ x -> 2); ens (T /\ emp) |}]; test @@ -1036,9 +1036,9 @@ let%expect_test "rewriting" = (Staged (seq [ens ~h:(PointsTo ("x", num 1)) (); ens ()])); [%expect {| - rewrite ens x->1; ens emp + rewrite ens (T /\ x -> 1); ens (T /\ emp) with 1 ==> 2 - result: ens x->2; ens emp + result: ens (T /\ x -> 2); ens (T /\ emp) |}]; test @@ -1062,9 +1062,9 @@ let%expect_test "rewriting" = ])); [%expect {| - rewrite ens emp; let y = (ens res=1) in (ens res=y) - with let __x = (ens res=__r) in (__f()) ==> - result: ens emp; ens res=1 + rewrite ens (T /\ emp); (ens (res = 1)); y. (ens (res = y)) + with (ens (res = __r)); __x. __f() ==> + result: ens (T /\ emp); ens (res = 1) |}]; test @@ -1100,9 +1100,9 @@ let%expect_test "rewriting" = so capture-avoidance doesn't work properly *) [%expect {| - rewrite let x = (ex y. (ens res=y)) in (ens x=1) - with let __x = (ex __x1. (__f())) in (__fk()) ==> ex __x1. (let __x = (__f()) in (__fk())) - result: ex y2. (let x3 = (ens res=y) in (ens x=1)) + rewrite (ex y. (ens (res = y))); x. ens (x = 1 /\ emp) + with (ex __x1. (__f())); __x. __fk() ==> ex __x1. ((__f()); __x. __fk()) + result: ex y2. ((ens (res = y)); x3. ens (x = 1 /\ emp)) |}]; (* type-aware rewriting *) @@ -1134,8 +1134,8 @@ let%expect_test "rewriting" = [%expect {| rewrite id((n : int)) - with id((__n : '__t)) ==> ens (res : '__t)=(__n : '__t) - result: ens (res : int)=(n : int) + with id((__n : '__t)) ==> ens (res = (__n : '__t)) + result: ens (res = (n : int)) |}] let%expect_test "unify modulo alpha-equivalence" = @@ -1158,13 +1158,13 @@ let%expect_test "unify modulo alpha-equivalence" = let a = Staged (Bind (("x", Any), res_eq_1, ens ~p:(eq (var_any "res") (var_any "x")) ())) in let b = Staged (Bind (("y", Any), res_eq_1, ens ~p:(eq (var_any "res") (var_any "y")) ())) in test a b; - [%expect{| let x0 = (ens res=1) in (ens res=x0) |}] + [%expect{| (ens (res = 1)); x0. ens (res = x0) |}] in let () = let a = Staged (Exists (("x", Any), ens ~p:(eq (var_any "res") (var_any "x")) ())) in let b = Staged (Exists (("y", Any), ens ~p:(eq (var_any "res") (var_any "y")) ())) in test a b; - [%expect{| ex x1. (ens res=x1) |}] + [%expect{| ex x1. (ens (res = x1)) |}] in () @@ -1188,9 +1188,9 @@ let%expect_test "rewriting modulo alpha-equivalence" = let ut = Staged (Bind (("y", Any), res_eq_1, ens ~p:(eq (var_any "res") (var_any "y")) ())) in test rule ut; [%expect{| - rewrite let y = (ens res=1) in (ens res=y) - with let x = (ens res=1) in (ens res=x) ==> ens res=1 - result: ens res=1 + rewrite (ens (res = 1)); y. ens (res = y) + with (ens (res = 1)); x. ens (res = x) ==> ens (res = 1) + result: ens (res = 1) |}] in () @@ -1240,15 +1240,15 @@ let%expect_test "autorewrite" = test norm_db (Staged (ens ~p:(conj [True; eq (v "x") (ctrue); True; True]) ())); [%expect {| - start: ens T/\x=true/\T/\T - result: ens x=true + start: ens (T /\ x = true /\ T /\ T /\ emp) + result: ens (x = true /\ emp) |}]; test norm_db (Staged (ens ~p:(conj [True; eq (v "x") (v "x"); True; True]) ())); [%expect {| - start: ens T/\x=x/\T/\T - result: ens emp + start: ens (T /\ x = x /\ T /\ T /\ emp) + result: ens (T /\ emp) |}] (** Named after the ppxlib module. See Rewriting2 for a full-scale @@ -1300,7 +1300,7 @@ module Ast_pattern = struct let p1 = and_ true_ __ in let r = match_ p1 (And (True, True)) in Format.printf "%s@." (string_of_option string_of_pi r); - [%expect {| Some T |}] + [%expect {| T |}] let rewrite_rooted (T p) u k = p u k @@ -1311,7 +1311,7 @@ module Ast_pattern = struct in let r = Iter.head_exn (rule (And (True, False))) in Format.printf "%s@." (string_of_pi r); - [%expect {| F/\T |}] + [%expect {| F /\ T |}] let rewrite_all_pure lhs krhs = let visitor = @@ -1336,7 +1336,7 @@ module Ast_pattern = struct #visit_staged_spec () target in Format.printf "%s@." (string_of_staged_spec r); - [%expect {| ens F/\T |}] + [%expect {| ens (F /\ T /\ emp) |}] end module Deep = struct @@ -1440,5 +1440,5 @@ module Deep = struct let p2 = and_ (v "a") true_ in let r = rewrite_rooted p1 p2 (Pure (And (True, False))) in Format.printf "%s@." (string_of_option string_of_uterm r); - [%expect {| Some F/\T |}] + [%expect {| F /\ T |}] end diff --git a/lib/hipprover/rewriting2.ml b/lib/hipprover/rewriting2.ml index ad286b3c..06f82e1a 100644 --- a/lib/hipprover/rewriting2.ml +++ b/lib/hipprover/rewriting2.ml @@ -189,7 +189,7 @@ let%expect_test "rewrite" = ~target:(And (True, False)) in Format.printf "%s@." (string_of_pi res); - [%expect {| F/\T |}]; + [%expect {| F /\ T |}]; let res = rewrite_rooted ~lhs:(and_ __ __) @@ -197,7 +197,7 @@ let%expect_test "rewrite" = ~target:(And (True, False)) in Format.printf "%s@." (string_of_pi res); - [%expect {| F/\T |}] + [%expect {| F /\ T |}] let pi_visitor lhs krhs = object (_self) @@ -250,7 +250,7 @@ let%expect_test "rewrite all" = (rewrite_all pi_in_staged (and_ true_ __) (fun a -> And (a, True))) target in Format.printf "%s@." (string_of_staged_spec r); - [%expect {| ens F/\T |}] + [%expect {| ens (F /\ T /\ emp) |}] type ('a, 'k) rule = ('a, 'k, 'a) pattern * 'k @@ -294,4 +294,4 @@ let%expect_test _ = let r = autorewrite pi_in_staged db Syntax.(ens ~p:(And (True, False)) ()) in Format.printf "%s@." (string_of_staged_spec r); - [%expect {| ens F |}] + [%expect {| ens (F /\ emp) |}] diff --git a/lib/hipprover/simpl.ml b/lib/hipprover/simpl.ml index f71c0837..f5760af3 100644 --- a/lib/hipprover/simpl.ml +++ b/lib/hipprover/simpl.ml @@ -99,8 +99,8 @@ let%expect_test "simplify tests" = let h1 = (SepConj (EmptyHeap, SepConj (PointsTo ("x", num 1), EmptyHeap))) in test simplify_kappa Pretty.string_of_kappa h1; [%expect {| - simplify: emp*x->1*emp - result: x->1 + simplify: emp * x -> 1 * emp + result: x -> 1 |}]; let ( -@ ) = binop Minus in @@ -109,13 +109,13 @@ let%expect_test "simplify tests" = let t = (num 5) *@ ((num 6) +@ ((num 10) -@ (num 3))) in test simplify_term Pretty.string_of_term t; [%expect {| - simplify: (5 * (6 + (10 - 3))) + simplify: 5 *. (6 + 10 - 3) result: 65 |}]; let p1 = And (True, Or ( And (False, eq (var "a") (var "b")), eq (var "x") (var "y"))) in test simplify_pure Pretty.string_of_pi p1; [%expect {| - simplify: T/\F/\a=b\/x=y - result: x=y + simplify: T /\ (F /\ a = b \/ x = y) + result: x = y |}];; From 0c7192b530a0cc6c1fd1a5f599f856fe4418fe14 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Fri, 5 Sep 2025 17:21:52 +0800 Subject: [PATCH 13/15] deprecate untyped subst all code has already been ported over to typed subst --- lib/hipcore/subst.ml | 216 ------------------------------------------ lib/hipcore/subst.mli | 17 ---- 2 files changed, 233 deletions(-) diff --git a/lib/hipcore/subst.ml b/lib/hipcore/subst.ml index 7cf3bf4f..e69de29b 100644 --- a/lib/hipcore/subst.ml +++ b/lib/hipcore/subst.ml @@ -1,216 +0,0 @@ -open Hiptypes -open Syntax -open Pretty -open Utils.Hstdlib -open Utils.Misc - -type 'a subst_context = - | Staged : staged_spec subst_context - | Term : term subst_context - | Pure : pi subst_context - | Heap : kappa subst_context - -let free_vars (type ctx_type) (ctx_type : ctx_type subst_context) (ctx : ctx_type) = - let visitor = - object (_) - inherit [_] reduce_spec as super - method zero = SSet.empty - method plus = SSet.union - - method! visit_Exists () x f = - let b = super#visit_Exists () x f in - SSet.remove x b - - method! visit_ForAll () x f = - let b = super#visit_ForAll () x f in - SSet.remove x b - - method! visit_TLambda () h ps sp b = - let b = super#visit_TLambda () h ps sp b in - List.fold_right (fun c t -> SSet.remove c t) ps b - - method! visit_Bind () x f1 f2 = - let b = super#visit_Bind () x f1 f2 in - SSet.remove x b - - method! visit_HigherOrder () f v = - let b = super#visit_HigherOrder () f v in - SSet.add f b - - method! visit_Var () x = SSet.singleton x - end - in - match ctx_type with - | Staged -> visitor#visit_staged_spec () ctx - | Term -> visitor#visit_term () ctx - | Heap -> visitor#visit_kappa () ctx - | Pure -> visitor#visit_pi () ctx - - -let%expect_test "free vars" = - let test s = Format.printf "%s@." (Pretty.string_of_sset s) in - - free_vars Staged (HigherOrder ("x", [Var "z"])) |> test; - [%expect {| {x, z} |}]; - - free_vars Staged (ens ~p:(eq (v "res") (num 1)) ()) |> test; - [%expect {| {res} |}] - -let rec find_binding x bindings = - match bindings with - | [] -> Var x - | (name, v) :: xs -> if String.equal name x then v else find_binding x xs - -(* replaces free variables *) -let subst_free_term_vars (type ctx_type) (ctx_type : ctx_type subst_context) bs (ctx : ctx_type) = - let subst_visitor free = - object (self) - inherit [_] map_spec - - (* most of the work done by this visitor is done here *) - method! visit_Var bindings v = find_binding v bindings - - (* a few other constructs contain implicit variables *) - method! visit_HigherOrder bindings f v = - let v1 = self#visit_list self#visit_term bindings v in - match find_binding f bindings with - | Var f1 -> HigherOrder (f1, v1) - | _ -> failwith "invalid" - - method! visit_PointsTo bindings x v = - let v1 = self#visit_term bindings v in - match find_binding x bindings with - | Var f1 -> PointsTo (f1, v1) - | _ -> failwith "invalid" - - (* the remaining cases handle capture-avoidance in binders *) - method! visit_Shift bindings nz k body x cont = - let k1, body1 = - if SSet.mem k free then - let y = Variables.fresh_variable ~v:k () in - (y, self#visit_staged_spec [(k, Var y)] body) - else - (k, body) - in - let x1, cont1 = - if SSet.mem x free then - let y = Variables.fresh_variable ~v:x () in - (y, self#visit_staged_spec [(x, Var y)] body) - else - (x, cont) - in - let bs_k = List.filter (fun (b, _) -> b <> k1) bindings in - let bs_x = List.filter (fun (b, _) -> b <> x1) bindings in - Shift (nz, k1, self#visit_staged_spec bs_k body1, x1, self#visit_staged_spec bs_x cont1) - - method! visit_Exists bindings x f = - let x1, f1 = - if SSet.mem x free then - let y = Variables.fresh_variable ~v:x () in - (y, self#visit_staged_spec [(x, Var y)] f) - else (x, f) - in - let bs = List.filter (fun (b, _) -> b <> x1) bindings in - Exists (x1, self#visit_staged_spec bs f1) - - method! visit_ForAll bindings x f = - let x1, f1 = - if SSet.mem x free then - let y = Variables.fresh_variable ~v:x () in - (y, self#visit_staged_spec [(x, Var y)] f) - else (x, f) - in - let bs = List.filter (fun (b, _) -> b <> x1) bindings in - ForAll (x1, self#visit_staged_spec bs f1) - - method! visit_Bind bindings x f1 f2 = - let x1, f2 = - if SSet.mem x free then - let y = Variables.fresh_variable ~v:x () in - (y, self#visit_staged_spec [(x, Var y)] f2) - else (x, f2) - in - let bs = List.filter (fun (b, _) -> b <> x1) bindings in - Bind (x1, self#visit_staged_spec bs f1, self#visit_staged_spec bs f2) - - method! visit_TLambda bindings name params sp body = - let params1, sp1, body1 = - List.fold_right - (fun p (ps, sp, body) -> - if SSet.mem p free then - let y = Variables.fresh_variable ~v:p () in - ( p :: ps, - self#visit_option self#visit_staged_spec [(p, Var y)] sp, - self#visit_option self#visit_core_lang [(p, Var y)] body ) - else (p :: ps, sp, body)) - params ([], sp, body) - in - let bs = - List.filter (fun (b, _) -> not (List.mem b params1)) bindings - in - TLambda - ( name, - params1, - self#visit_option self#visit_staged_spec bs sp1, - self#visit_option self#visit_core_lang bs body1 ) - - method! visit_CLambda bindings params sp body = - let params1, sp1, body1 = - List.fold_right - (fun p (ps, sp, body) -> - if SSet.mem p free then - let y = Variables.fresh_variable ~v:p () in - ( p :: ps, - self#visit_option self#visit_staged_spec [(p, Var y)] sp, - self#visit_core_lang [(p, Var y)] body ) - else (p :: ps, sp, body)) - params ([], sp, body) - in - let bs = - List.filter (fun (b, _) -> not (List.mem b params1)) bindings - in - CLambda - ( params1, - self#visit_option self#visit_staged_spec bs sp1, - self#visit_core_lang bs body1 ) - end - in - let free = List.map snd bs |> List.map (free_vars Term) |> SSet.concat in - let result : ctx_type = match ctx_type with - | Staged -> (subst_visitor free)#visit_staged_spec bs ctx - | Term -> (subst_visitor free)#visit_term bs ctx - | Pure -> (subst_visitor free)#visit_pi bs ctx - | Heap -> (subst_visitor free)#visit_kappa bs ctx in - result - -let subst_free_vars = subst_free_term_vars Staged - -let%expect_test "subst" = - Variables.reset_counter 0; - let test bs f1 = - let f2 = subst_free_vars bs f1 in - Format.printf "(%s)%s = %s@." (string_of_staged_spec f1) - (string_of_list - (fun (x, t) -> Format.asprintf "%s/%s" (string_of_term t) x) - bs) - (string_of_staged_spec f2) - in - - test [("z", v "a")] (HigherOrder ("x", [v "z"])); - [%expect {| (x(z))[a/z] = x(a) |}]; - - test [("x", v "y")] (HigherOrder ("x", [v "z"])); - [%expect {| (x(z))[y/x] = y(z) |}]; - - (* capture-avoidance *) - test - [("x", v "y")] - (seq - [ - ens ~p:(eq (v "x") (v "x")) (); - Exists ("x", ens ~p:(eq (v "x") (num 1)) ()); - ]); - [%expect {| (ens x=x; ex x. (ens x=1))[y/x] = ens y=y; ex x. (ens x=1) |}]; - - test [("x", v "z")] (Exists ("z", ens ~p:(eq (v "z") (v "x")) ())); - [%expect {| (ex z. (ens z=x))[z/x] = ex z0. (ens z0=z) |}] diff --git a/lib/hipcore/subst.mli b/lib/hipcore/subst.mli index 28f2298b..e69de29b 100644 --- a/lib/hipcore/subst.mli +++ b/lib/hipcore/subst.mli @@ -1,17 +0,0 @@ -open Hiptypes -open Utils.Hstdlib - -type 'a subst_context = - | Staged : staged_spec subst_context - | Term : term subst_context - | Pure : pi subst_context - | Heap : kappa subst_context - -(** Alias for [subst_free_term_vars Staged]. *) -val subst_free_vars : (string * term) list -> staged_spec -> staged_spec - -(** Substitute out free variables for a list of terms in a given context. - (The target locations may not necessarily be terms, e.g. locations in a heap formula.) *) -val subst_free_term_vars : 'a. 'a subst_context -> (string * term) list -> 'a -> 'a - -val free_vars : 'a. 'a subst_context -> 'a -> SSet.t From 6d958697fea4b933d811a401c86a9999a19e609e Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Fri, 5 Sep 2025 18:00:05 +0800 Subject: [PATCH 14/15] fix linebreaks on type annotations done by adding a group to wrap the annotations, to make the split choice independent of the context --- lib/hipcore_typed/Pretty.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index b2c2511c..ae1a43c3 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -506,13 +506,13 @@ let add_type_annotations (pp : pretty_printer) : pretty_printer = { pp with pp_binder = begin fun self ctx b -> - parens (pp.pp_binder self (ctx |> with_binding Negative_inf) b ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx (type_of_binder b))) + group (parens (pp.pp_binder self (ctx |> with_binding Negative_inf) b ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx (type_of_binder b)))) end; pp_term = begin fun self ctx t -> - parens (pp.pp_term self (ctx |> with_binding Negative_inf) t ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx t.term_type)) + group (parens (pp.pp_term self (ctx |> with_binding Negative_inf) t ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx t.term_type))) end; pp_core_lang = begin fun self ctx core -> - parens (pp.pp_core_lang self (ctx |> with_binding Negative_inf) core ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx core.core_type)) + group (parens (pp.pp_core_lang self (ctx |> with_binding Negative_inf) core ^^ space ^^ colon ^^ break 1 ^^ (self.pp_typ self ctx core.core_type))) end } From ec600d5d1531b878bfc1cae2e25f5cc545aa8bbf Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Mon, 8 Sep 2025 15:39:47 +0800 Subject: [PATCH 15/15] fix web build --- main/hipjs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/main/hipjs.ml b/main/hipjs.ml index 52c050f8..7f0c8bf9 100644 --- a/main/hipjs.ml +++ b/main/hipjs.ml @@ -12,7 +12,7 @@ let ready () = ()) let main () = - Hipcore_typed.Pretty.colours := `Html; + Hipcore.Pretty.colours := `Html; (* Console.(log [str "DOM content loaded."]); *) Jv.set Jv.global "ocaml_ready" (Jv.callback ~arity:1 ready); Jv.set Jv.global "hip_run_string"