From eb79d56b276678e9a8c3d24b46d32722f7896f79 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 11:51:58 +0800 Subject: [PATCH 1/6] create dynamic typing module --- lib/hipcore_typed/dune | 3 ++- lib/hipcore_typed/dynamic_typing.ml | 34 ++++++++++++++++++++++++++++ lib/hipcore_typed/dynamic_typing.mli | 23 +++++++++++++++++++ 3 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 lib/hipcore_typed/dynamic_typing.ml create mode 100644 lib/hipcore_typed/dynamic_typing.mli diff --git a/lib/hipcore_typed/dune b/lib/hipcore_typed/dune index 0e7dc019..13630879 100644 --- a/lib/hipcore_typed/dune +++ b/lib/hipcore_typed/dune @@ -1,7 +1,8 @@ (library (name hipcore_typed) (public_name heifer.hipcore_typed) - (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast) + (modules subst typedhip pretty untypehip retypehip patterns syntax patterns globals rewrite_context variables typed_core_ast + dynamic_typing) (libraries debug unionFind str utils hipcore) (inline_tests) (preprocess (pps ppx_expect ppx_deriving.std visitors.ppx))) diff --git a/lib/hipcore_typed/dynamic_typing.ml b/lib/hipcore_typed/dynamic_typing.ml new file mode 100644 index 00000000..6ead1ac5 --- /dev/null +++ b/lib/hipcore_typed/dynamic_typing.ml @@ -0,0 +1,34 @@ +open Typedhip + +let status = ref false + +let set_dynamic_typing () = status := true + +let dynamic_typing_enabled () = !status + +let spec_visitor f = object + inherit [_] map_spec + + method! visit_typ _ t = f t +end + +let type_with_any_spec s = (spec_visitor (fun _ -> Any))#visit_staged_spec () s + +let instantiate_any_types_pi p = (spec_visitor (fun _ -> TVar (Variables.fresh_variable ())))#visit_pi () p + +let check_for_untyped_visitor = object + inherit [_] reduce_spec + + method zero = false + method plus = (||) + + method! visit_CShift _ _ _ _ = true + method! visit_CReset _ _ = true + + method! visit_Shift _ _ _ _ _ _ = true + method! visit_Reset _ _ = true +end + +let uses_untyped_extensions_spec s = check_for_untyped_visitor#visit_staged_spec () s + +let uses_untyped_extensions_core c = check_for_untyped_visitor#visit_core_lang () c diff --git a/lib/hipcore_typed/dynamic_typing.mli b/lib/hipcore_typed/dynamic_typing.mli new file mode 100644 index 00000000..c64dea7c --- /dev/null +++ b/lib/hipcore_typed/dynamic_typing.mli @@ -0,0 +1,23 @@ +open Typedhip + +(** Enable dynamic typing. This disables all type checks before translation to SMT. + This does not do anything by itself; relevant areas of the library whose + behaviors differ between untyped and typed mode must check this flag + using [dynamic_typing_enabled]. + + This must be called before any input is processed. *) +val set_dynamic_typing : unit -> unit + +val dynamic_typing_enabled : unit -> bool + +(** Replace all types in this specification with [Any]. *) +val type_with_any_spec : staged_spec -> staged_spec + +(** Replace all [Any] types in this pure formula with fresh type variables. + Inferring these types can be done using one of the [Infer_types] endpoints. *) +val instantiate_any_types_pi : pi -> pi + +(* Currently, the only untyped extensions are shift/reset. *) + +val uses_untyped_extensions_spec : staged_spec -> bool +val uses_untyped_extensions_core : core_lang -> bool From e8c85676e070addf5238a7e15f03b757cd88e47d Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 13:49:23 +0800 Subject: [PATCH 2/6] fail non-term substs when given a non-var --- lib/hipcore_typed/subst.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml index cc16d449..29dfbe44 100644 --- a/lib/hipcore_typed/subst.ml +++ b/lib/hipcore_typed/subst.ml @@ -52,7 +52,8 @@ let reduce_visitor_function (type ctx_type) reduce_visitor (ctx_type : ctx_type let find_non_term_binding x bindings = match List.assoc_opt x bindings with | Some {term_desc = Var name; _} -> name - | _ -> x + | Some _ -> failwith "Expected (Var _) for non-term substitution" + | None -> x let types_of_free_vars (type ctx_type) (ctx_type : ctx_type subst_context) (ctx : ctx_type) = let visitor = From 0f39bb51d92f1acc62ea6b625e2eba5ac63ae850 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:01:34 +0800 Subject: [PATCH 3/6] add dynamic typing switch in frontend --- lib/hiplib/hiplib.ml | 38 ++++++++++++++++++++++++++++++++++++-- main/hip.ml | 4 ++++ 2 files changed, 40 insertions(+), 2 deletions(-) diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml index 5da18f31..14298fb8 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -179,6 +179,12 @@ let check_method prog inferred given = let infer_and_check_method (prog : core_program) (meth : meth_def) (given_spec : staged_spec option) = let inferred_spec = infer_spec prog meth in + let inferred_spec, given_spec = + let open Dynamic_typing in + if dynamic_typing_enabled () + then type_with_any_spec inferred_spec, Option.map type_with_any_spec given_spec + else inferred_spec, given_spec + in let result = check_method prog inferred_spec given_spec in inferred_spec, result @@ -271,9 +277,33 @@ let process_pure_fn_info ({m_name; m_params; m_body; _}) = function in Globals.define_pure_fn m_name pf +let type_with_any_binder b = ident_of_binder b, Any + +(** Substitute Any into the types of this lemma if dynamic typing is enabled. *) +let use_dynamic_types_if_enabled_lem (l : Typedhip.lemma) = + let open Dynamic_typing in + if dynamic_typing_enabled () + then {l with + l_params = l.l_params |> List.map type_with_any_binder; + l_left = type_with_any_spec l.l_left; + l_right = type_with_any_spec l.l_right} + else l + +(** Substitute Any into the types of this method if dynamic typing is enabled. + + {b Note:} This does not dynamically type core language expressions (which need + to be dynamically typed later), due to the forward verification process needing some + type information (e.g. during pattern matching.) *) +let use_dynamic_types_if_enabled_meth (m : meth_def) = + let open Dynamic_typing in + if dynamic_typing_enabled () + then {m with m_params = List.map type_with_any_binder m.m_params; + m_spec = Option.map type_with_any_spec m.m_spec} + else m + let process_intermediates (it : Typedhip.intermediate) prog : binder list * core_program = - (* Format.printf "%s\n" (Pretty.string_of_intermediate it); - ([], prog) *) + (* This is the point where dynamic typing, if enabled, is applied; when filling out a case, + make sure to handle this. *) let open Typedhip in match it with (* | LogicTypeDecl (name, params, ret, path, lname) -> @@ -307,6 +337,7 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core debug ~at:4 ~title:(Format.asprintf "added lemma %s" l.l_name) "%s" (string_of_lemma l); *) (* add to environment regardless of failure *) (* we need to prove the lemma *) + let l = use_dynamic_types_if_enabled_lem l in let@ _ = Debug.span (fun _ -> debug ~at:1 ~title:(Format.sprintf "verifying lemma: %s" l.l_name) "") in @@ -334,6 +365,9 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core | Meth (m_name, m_params, m_spec, m_body, m_tactics, pure_fn_info) -> let meth : meth_def = {m_name; m_params; m_spec; m_body; m_tactics} in process_pure_fn_info meth pure_fn_info; + (* Apply dynamic typing _after_ doing pure function processing; since pure functions need to be + handled by SMT (and so need to be always typed anyway.) *) + let meth = use_dynamic_types_if_enabled_meth meth in let@ _ = Debug.span (fun _ -> debug ~at:1 ~title:(Format.asprintf "verifying function: %s" meth.m_name) "") in diff --git a/main/hip.ml b/main/hip.ml index 06d194de..bb6376ef 100644 --- a/main/hip.ml +++ b/main/hip.ml @@ -18,6 +18,10 @@ let () = Hiplib.(file_mode := (Option.bind (Sys.getenv_opt "FILE") int_of_string_opt |> Option.value ~default:0) > 0); + begin + if Option.bind (Sys.getenv_opt "NOTYPES") int_of_string_opt |> Option.value ~default:0 > 0 + then Hipcore_typed.Dynamic_typing.set_dynamic_typing () + end; let ctf = Option.bind (Sys.getenv_opt "CTF") int_of_string_opt |> Option.value ~default:0 > 0 From 289e1e807c83e5e3af72a1b806feaf4ae5c92d02 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:39:42 +0800 Subject: [PATCH 4/6] instantiate all Any types before SMT check --- lib/hipprover/entail.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index 68dcccdb..05dec1dc 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -237,6 +237,8 @@ let check_pure_obligation left right = the untyped extensions. Perform another typechecking phase to perform these unifications. *) let (left, right), _ = + let left = Dynamic_typing.instantiate_any_types_pi left in + let right = Dynamic_typing.instantiate_any_types_pi right in let open Infer_types in with_empty_env begin let* left, right = infer_types_pair_pi left right in From d2a1e631b627ad91056dc627c1dbb7c546cce599 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:39:58 +0800 Subject: [PATCH 5/6] suppress Infer_types.Unification_failure during entailment this should probably only be done in untyped mode, though currently the `can_unify_with` check eliminates all ill-typed instantiations in typed mode so it won't change anything for now --- lib/hipprover/entail.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index 05dec1dc..f361a7c7 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -825,11 +825,15 @@ let suppress_exn ~title ~default (f : unit -> 'a) : 'a = debug ~at:5 ~title "%s" (Printexc.to_string e); default -let suppress_some_exn ~title ~default (f : unit -> 'a) : 'a = +(** Suppress type errors from the prover backends and type checker, instead outputting + a debug log message (whose title is [title]) and returning [default]. These are usually + caused by the instantiation heuristic not catching ill-typed instantiations (especially + when in untyped mode), and are useful to let those instantiations act as a failing branch instead. *) +let suppress_type_exn ~title ~default (f : unit -> 'a) : 'a = try f () with - | Z3.Error _ | Infer_types.Cyclic_type _ as e -> + | Z3.Error _ | Infer_types.Cyclic_type _ | Infer_types.Unification_failure _ as e -> debug ~at:5 ~title "%s" (Printexc.to_string e); default @@ -1133,7 +1137,7 @@ let rec apply_ent_rule ?name : tactic = (* copy the binder's type to allow for polymorphic constants in try_constants *) let f4 = Subst.subst_free_vars [(ident_of_binder x, term c.term_desc (type_of_binder x))] f4 in fun k1 -> - let@ _ = suppress_some_exn + let@ _ = suppress_type_exn ~title:"ERROR: exists on the right, entailment step" ~default:fail in @@ -1157,7 +1161,7 @@ let rec apply_ent_rule ?name : tactic = if Hipcore.Types.can_unify_with c.term_type (type_of_binder x) then let f3 = Subst.subst_free_vars [((ident_of_binder x), term c.term_desc (type_of_binder x))] f3 in fun k1 -> - let@ _ = suppress_some_exn + let@ _ = suppress_type_exn ~title:"ERROR: forall on the left, entailment step" ~default:fail in From 117ffb71d982dfbd7fbca35a6fc7631857471a28 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 2 Sep 2025 14:58:07 +0800 Subject: [PATCH 6/6] add docs --- docs/development.md | 7 +++++++ lib/hipcore_typed/dynamic_typing.mli | 3 ++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/development.md b/docs/development.md index dd1452cc..dafb2e86 100644 --- a/docs/development.md +++ b/docs/development.md @@ -74,6 +74,13 @@ Some of the environment variables Heifer interprets may be useful for testing. Setting `TEST=1` causes Heifer to print only whether a test has failed, which is useful for integration tests. A test in this context is a function whose main entailment proof must succeed; if its name has the suffix `_false`, the entailment must fail. +## Untyped extensions + +Some extensions not supported by mainline OCaml are supported. Currently, this only includes delimited continuation operators (ala [OchaCaml](https://www.is.ocha.ac.jp/~asai/OchaCaml/)), but more may be supported. + +Setting `NOTYPES=1` will defer all typechecking during entailment checks until necessary (i.e. before SMT translation). This may be useful to ease development of extensions +outside of those typechecked by OCaml. + ## Logging and tracing View log output by setting `DEBUG=n`. diff --git a/lib/hipcore_typed/dynamic_typing.mli b/lib/hipcore_typed/dynamic_typing.mli index c64dea7c..801c60d9 100644 --- a/lib/hipcore_typed/dynamic_typing.mli +++ b/lib/hipcore_typed/dynamic_typing.mli @@ -5,7 +5,8 @@ open Typedhip behaviors differ between untyped and typed mode must check this flag using [dynamic_typing_enabled]. - This must be called before any input is processed. *) + For a declaration to be processed in untyped mode, this must be called before + the declaration is processed. *) val set_dynamic_typing : unit -> unit val dynamic_typing_enabled : unit -> bool