Add env var to disable typing of formulas during entailment checking

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

lib/hipcore_typed/dune

@@ -1,7 +1,8 @@
 (library
  (name hipcore_typed)
  (public_name heifer.hipcore_typed)
- (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast)
+ (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast
+   dynamic_typing)
  (libraries debug unionFind str utils hipcore)
  (inline_tests)
  (preprocess (pps ppx_expect ppx_deriving.std visitors.ppx)))

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

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

lib/hipcore_typed/subst.ml

@@ -52,7 +52,8 @@ let reduce_visitor_function (type ctx_type) reduce_visitor (ctx_type : ctx_type
 let find_non_term_binding x bindings =
   match List.assoc_opt x bindings with
   | Some {term_desc = Var name; _} -> name
-  | _ -> x
+  | Some _ -> failwith "Expected (Var _) for non-term substitution"
+  | None -> x
 
 let types_of_free_vars (type ctx_type) (ctx_type : ctx_type subst_context) (ctx : ctx_type) =
   let visitor =

lib/hiplib/hiplib.ml

@@ -179,6 +179,12 @@ let check_method prog inferred given =
 
 let infer_and_check_method (prog : core_program) (meth : meth_def) (given_spec : staged_spec option) =
   let inferred_spec = infer_spec prog meth in
+  let inferred_spec, given_spec =
+    let open Dynamic_typing in
+    if dynamic_typing_enabled ()
+    then type_with_any_spec inferred_spec, Option.map type_with_any_spec given_spec
+    else inferred_spec, given_spec
+  in
   let result = check_method prog inferred_spec given_spec in
   inferred_spec, result
 
@@ -271,9 +277,33 @@ let process_pure_fn_info ({m_name; m_params; m_body; _}) = function
       in
       Globals.define_pure_fn m_name pf
 
+let type_with_any_binder b = ident_of_binder b, Any
+
+(** Substitute Any into the types of this lemma if dynamic typing is enabled. *)
+let use_dynamic_types_if_enabled_lem (l : Typedhip.lemma) =
+  let open Dynamic_typing in
+  if dynamic_typing_enabled ()
+  then {l with
+          l_params = l.l_params |> List.map type_with_any_binder;
+          l_left = type_with_any_spec l.l_left;
+          l_right = type_with_any_spec l.l_right}
+  else l
+
+(** Substitute Any into the types of this method if dynamic typing is enabled.
+
+  {b Note:} This does not dynamically type core language expressions (which need
+  to be dynamically typed later), due to the forward verification process needing some
+  type information (e.g. during pattern matching.) *)
+let use_dynamic_types_if_enabled_meth (m : meth_def) =
+  let open Dynamic_typing in
+  if dynamic_typing_enabled ()
+  then {m with m_params = List.map type_with_any_binder m.m_params;
+        m_spec = Option.map type_with_any_spec m.m_spec}
+  else m
+
 let process_intermediates (it : Typedhip.intermediate) prog : binder list * core_program =
-  (* Format.printf "%s\n" (Pretty.string_of_intermediate it);
-  ([], prog) *)
+  (* This is the point where dynamic typing, if enabled, is applied; when filling out a case,
+     make sure to handle this. *)
   let open Typedhip in
   match it with
   (* | LogicTypeDecl (name, params, ret, path, lname) ->
@@ -307,6 +337,7 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core
       debug ~at:4 ~title:(Format.asprintf "added lemma %s" l.l_name) "%s" (string_of_lemma l); *)
       (* add to environment regardless of failure *)
       (* we need to prove the lemma *)
+      let l = use_dynamic_types_if_enabled_lem l in
       let@ _ = Debug.span (fun _ ->
         debug ~at:1 ~title:(Format.sprintf "verifying lemma: %s" l.l_name) "")
       in
@@ -334,6 +365,9 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core
   | Meth (m_name, m_params, m_spec, m_body, m_tactics, pure_fn_info) ->
       let meth : meth_def = {m_name; m_params; m_spec; m_body; m_tactics} in
       process_pure_fn_info meth pure_fn_info;
+      (* Apply dynamic typing _after_ doing pure function processing; since pure functions need to be
+         handled by SMT (and so need to be always typed anyway.) *)
+      let meth = use_dynamic_types_if_enabled_meth meth in
       let@ _ = Debug.span (fun _ ->
         debug ~at:1 ~title:(Format.asprintf "verifying function: %s" meth.m_name) "")
       in

lib/hipprover/entail.ml

@@ -237,6 +237,8 @@ let check_pure_obligation left right =
      the untyped extensions. Perform another typechecking phase to perform these
      unifications. *)
   let (left, right), _ =
+    let left = Dynamic_typing.instantiate_any_types_pi left in
+    let right = Dynamic_typing.instantiate_any_types_pi right in
     let open Infer_types in
     with_empty_env begin
       let* left, right = infer_types_pair_pi left right in
@@ -823,11 +825,15 @@ let suppress_exn ~title ~default (f : unit -> 'a) : 'a =
     debug ~at:5 ~title "%s" (Printexc.to_string e);
     default
 
-let suppress_some_exn ~title ~default (f : unit -> 'a) : 'a =
+(** Suppress type errors from the prover backends and type checker, instead outputting
+    a debug log message (whose title is [title]) and returning [default]. These are usually
+    caused by the instantiation heuristic not catching ill-typed instantiations (especially
+    when in untyped mode), and are useful to let those instantiations act as a failing branch instead. *)
+let suppress_type_exn ~title ~default (f : unit -> 'a) : 'a =
   try
     f ()
   with
-  | Z3.Error _ | Infer_types.Cyclic_type _ as e ->
+  | Z3.Error _ | Infer_types.Cyclic_type _ | Infer_types.Unification_failure _ as e ->
       debug ~at:5 ~title "%s" (Printexc.to_string e);
       default
 
@@ -1131,7 +1137,7 @@ let rec apply_ent_rule ?name : tactic =
           (* copy the binder's type to allow for polymorphic constants in try_constants *)
           let f4 = Subst.subst_free_vars [(ident_of_binder x, term c.term_desc (type_of_binder x))] f4 in
           fun k1 ->
-            let@ _ = suppress_some_exn
+            let@ _ = suppress_type_exn
               ~title:"ERROR: exists on the right, entailment step"
               ~default:fail
             in
@@ -1155,7 +1161,7 @@ let rec apply_ent_rule ?name : tactic =
           if Hipcore.Types.can_unify_with c.term_type (type_of_binder x) then
           let f3 = Subst.subst_free_vars [((ident_of_binder x), term c.term_desc (type_of_binder x))] f3 in
           fun k1 ->
-            let@ _ = suppress_some_exn
+            let@ _ = suppress_type_exn
               ~title:"ERROR: forall on the left, entailment step"
               ~default:fail
             in

main/hip.ml

@@ -18,6 +18,10 @@ let () =
   Hiplib.(file_mode :=
     (Option.bind (Sys.getenv_opt "FILE") int_of_string_opt
     |> Option.value ~default:0) > 0);
+  begin
+  if Option.bind (Sys.getenv_opt "NOTYPES") int_of_string_opt |> Option.value ~default:0 > 0
+  then Hipcore_typed.Dynamic_typing.set_dynamic_typing ()
+  end;
   let ctf =
     Option.bind (Sys.getenv_opt "CTF") int_of_string_opt
     |> Option.value ~default:0 > 0