Rewrite pretty printer

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`.

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))))

heifer.opam

@@ -20,6 +20,7 @@ depends: [
   "js_of_ocaml" {>= "5.4.0"}
   "unionFind" {>= "20220122"}
   "visitors" {>= "20210608"}
+  "pprint" {>= "20230830"}
   "odoc" {with-doc}
 ]
 build: [

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) |}]

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