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/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/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 diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index 62172539..ae1a43c3 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -1,486 +1,726 @@ (* Functions for printing the typed AST. *) -open Hipcore +open Hipcore_common open Typedhip 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) +type 'a to_document = 'a -> PPrint.document + +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)))) + +(** 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 -> 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 +} + +(** 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 -> 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; + (* 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 _self _ op -> match op with + | GT -> string ">" + | LT -> string "<" + | EQ -> string "=" + | GTEQ -> string ">=" + | LTEQ -> string "<=" + end; + pp_bin_term_op = begin + 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 _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 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 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 ^ ")" - 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) + let rendered_body = match body with + | Some body -> self.pp_core_lang self ctx body + | None -> underscore 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 - 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) -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) - -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 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 + group (func_token ^^ blank 1 ^^ rendered_args ^^ nest 2 (break 1 ^^ rendered_spec ^^ break 1 ^^ rendered_body)) + end; + pp_term = begin + (* 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 - pp_print_list pp_handler + (* 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 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 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) -> + let arg = match arg with + | Some arg -> self.pp_term self (ctx |> with_binding Negative_inf) arg + | None -> string "()" + in + 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_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_handler _ = + (* not sure what the right syntax here should be... *) + string "[effect handler]" + in + 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 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 + (* 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) -> + (string "req") ^^ nest 2 (space ^^ parens (self.pp_state self (ctx |> with_binding Negative_inf) (p, k))) + | NormalReturn (p, k) -> + (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) -> + (* 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 - 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 + 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 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 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 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 = + let open PPrint in + { + pp with + pp_binder = begin fun self ctx 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 -> + 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 -> + 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 + } + +(** {1 Printer configuration} *) + +type config = { + cfg_print_types : 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_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} + +let pp_with_config cfg pp = + if cfg.cfg_print_types + then add_type_annotations pp + else pp + +(** { 1 Printing functions }*) + +module type Printers_internal = sig + 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 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 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 print_document cfg doc = + 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 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 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 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 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 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 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 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 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 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 + +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 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 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 = + let pp_constr (name, arg_types) = + if List.is_empty arg_types + then string name + else (string name) ^^ string "of" ^^ prefixed_list 1 (string "*") (List.map M.pp_typ arg_types) + in + prefixed_list 1 (string "|") (List.map pp_constr constrs) + in + let pp_record _r = string "record" in + let pp_kind kind = + match kind with + | Tdecl_inductive constrs -> pp_inductive constrs + | Tdecl_record r -> pp_record r + in + 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 m = + let open PPrint in + let pp_element (k, v) = + (pp_key k) ^^ space ^^ string "->" ^^ space ^^ (pp_value v) + in + 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 + 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 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 + print_string (string_of_staged_spec ~config:(default_config |> set_types_display) f1); + [%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 {| 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 {| + 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 {| + 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 {| expanded: 1 + 2 |}];; diff --git a/lib/hipcore_typed/Pretty.mli b/lib/hipcore_typed/Pretty.mli new file mode 100644 index 00000000..90f789fb --- /dev/null +++ b/lib/hipcore_typed/Pretty.mli @@ -0,0 +1,60 @@ +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 + +(** 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 [Typedhip.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/dune b/lib/hipcore_typed/dune index 0e7dc019..57e94274 100644 --- a/lib/hipcore_typed/dune +++ b/lib/hipcore_typed/dune @@ -1,7 +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) - (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/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..801c60d9 --- /dev/null +++ b/lib/hipcore_typed/dynamic_typing.mli @@ -0,0 +1,24 @@ +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]. + + 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 + +(** 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 diff --git a/lib/hipcore_typed/patterns.ml b/lib/hipcore_typed/patterns.ml index 534072ac..381bd97f 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)} @@ -252,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" = @@ -268,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{| |}]; @@ -284,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 cc16d449..ed12a439 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 @@ -52,7 +51,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 = @@ -200,7 +200,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) @@ -208,7 +208,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) @@ -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/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/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 5da18f31..35694cd0 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -99,14 +99,14 @@ let normal_report ~kind ~name ~inferred_spec ~given_spec ~result = let header = report_header ~kind ~name 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 @@ -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/lib/hiplib/tests.ml b/lib/hiplib/tests.ml index 1010f47f..8110e795 100644 --- a/lib/hiplib/tests.ml +++ b/lib/hiplib/tests.ml @@ -56,41 +56,41 @@ 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")); [%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 68dcccdb..b55c459c 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 @@ -237,6 +236,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 @@ -266,7 +267,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 @@ -497,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 @@ -520,7 +521,7 @@ let%expect_test _ = right branch *** search | _9 - ens emp |- ens emp + ens (T /\ emp) |- ens (T /\ emp) *** ens ens | _10 ok @@ -529,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 @@ -546,7 +547,7 @@ let%expect_test _ = right branch ***** search | _18 - ens emp |- ens emp + ens (T /\ emp) |- ens (T /\ emp) ***** ens ens | _19 ok @@ -564,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: [] @@ -823,11 +824,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 @@ -1131,7 +1136,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 @@ -1155,7 +1160,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 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 e90a2d6b..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,20 +1100,20 @@ 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 *) 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 = @@ -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 @@ -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 (Pretty.string_of_list ~sep:", " string_of_pattern a) let v s = Var s let and_ p1 p2 = Constr ("and", [p1; p2]) @@ -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 |}];; diff --git a/main/hip.ml b/main/hip.ml index 06d194de..f66fe27e 100644 --- a/main/hip.ml +++ b/main/hip.ml @@ -18,10 +18,19 @@ 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 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"); 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"