From 9c00d536a122ee12722311df04f63268e3973eaa Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 19 Aug 2025 16:14:05 +0800 Subject: [PATCH 1/9] use higher order func types to infer param types --- lib/hipcore/types.ml | 2 ++ lib/hipprover/infer_types.ml | 33 +++++++++++++++++++++++++-------- 2 files changed, 27 insertions(+), 8 deletions(-) diff --git a/lib/hipcore/types.ml b/lib/hipcore/types.ml index ca016863..4f815830 100644 --- a/lib/hipcore/types.ml +++ b/lib/hipcore/types.ml @@ -69,6 +69,8 @@ let rec params_of_arrow_type t = t1 :: params, result | _ -> [], t +let arrow_type_of_params params result = List.fold_right (fun typ acc -> Arrow (typ, acc)) params result + let concrete_types = [Unit; Int; Bool; Lamb] let new_type_var : ?name:string -> unit -> typ = diff --git a/lib/hipprover/infer_types.ml b/lib/hipprover/infer_types.ml index d07794d9..748be5d5 100644 --- a/lib/hipprover/infer_types.ml +++ b/lib/hipprover/infer_types.ml @@ -464,20 +464,37 @@ and infer_types_staged_spec ss : (staged_spec * typ option) using_env = let* result_type = type_of_result_of_state (p, k) in return (NormalReturn (p, k), result_type) | HigherOrder (f, args) -> - let* args = State.map_list ~f:infer_types_term args in - let* result_type = + let* f_type = match get_primitive_type_opt f with - | Some (_, result_type) -> return result_type + | Some (arg_types, result_type) -> return (arrow_type_of_params arg_types result_type) | None -> begin let* f_type = type_of_var_opt f in match f_type with - | Some typ -> - let _, result_type = params_of_arrow_type typ in - return result_type - | None -> - failwith (Format.sprintf "Infer_types: unknown function name %s" f) + | Some typ -> return typ + | None -> failwith (Format.sprintf "Infer_types: unknown function name %s" f) end in + (* given the type of f as a function, infer its argument's types + note that we may see more arguments than expected from f's type, + which means we need to unify f's type with some function type *) + let rec unify_arg_types f_type args : (term list * typ) using_env = + match f_type, args with + (* match a parameter with an input type *) + | Arrow (func_arg_type, func_arg_types), (arg :: args) -> + let* arg = infer_types_term ~hint:func_arg_type arg in + let* args, result_type = unify_arg_types func_arg_types args in + return (arg::args, result_type) + (* no inputs left, whatever type we have must be the output *) + | typ, [] -> return ([], typ) + (* some inputs left, typ must be unified with some function type *) + | typ, args -> + let output_type = fresh_type_var () in + let* args = State.map_list ~f:infer_types_term args in + let function_type = arrow_type_of_params (List.map (fun t -> t.term_type) args) output_type in + let* () = unify_types typ function_type in + return (args, function_type) + in + let* args, result_type = unify_arg_types f_type args in return (HigherOrder (f, args), Some result_type) | Shift (b, k, spec, x, cont) -> let* spec, _ = infer_types_staged_spec spec in From 15366ba14bc4803399e3ee1ea7432e3255d5da9c Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 19 Aug 2025 16:14:47 +0800 Subject: [PATCH 2/9] set type unification to debug lv 10 --- lib/hipprover/infer_types.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/lib/hipprover/infer_types.ml b/lib/hipprover/infer_types.ml index 748be5d5..3ae06d5b 100644 --- a/lib/hipprover/infer_types.ml +++ b/lib/hipprover/infer_types.ml @@ -36,7 +36,7 @@ let () = let rec unify_types t1 t2 : unit using_env = fun env -> - debug ~at:5 ~title:"unify" "%s ~ %s" (string_of_type t1) (string_of_type t2); + debug ~at:10 ~title:"unify_types" "%s ~ %s" (string_of_type t1) (string_of_type t2); match TEnv.(simplify env.equalities t1, simplify env.equalities t2) with (* case where one of t1, t2 is a type variable: *) | TVar var_name as var, simp | simp, (TVar var_name as var) -> @@ -272,7 +272,7 @@ and infer_types_constant ?(hint : typ option) const : typ = and infer_types_term ?(hint : typ option) term : term using_env = let@ _ = span_env (fun r -> - debug ~at:5 ~title:"infer_types" "%s : %s -| %s" (string_of_term term) + debug ~at:10 ~title:"infer_types" "%s : %s -| %s" (string_of_term term) (string_of_result string_of_term (State.Debug.presult_value r)) (string_of_result string_of_abs_env (State.Debug.presult_state r))) in @@ -382,7 +382,7 @@ and infer_types_constructor_like : and infer_types_pi pi : pi using_env = let@ _ = span_env (fun r -> - debug ~at:5 ~title:"infer_types_pi" "%s -| %s" (string_of_pi pi) + debug ~at:10 ~title:"infer_types_pi" "%s -| %s" (string_of_pi pi) (string_of_result string_of_abs_env (State.Debug.presult_state r))) in match pi with @@ -436,6 +436,11 @@ and infer_types_state (p, k) : state using_env = is the type, if any, returned by the computations satisfying this spec. *) and infer_types_staged_spec ss : (staged_spec * typ option) using_env = + let@ _ = + span_env (fun r -> + debug ~at:10 ~title:"infer_types_staged_spec" "%s -| %s" (string_of_staged_spec ss) + (string_of_result string_of_abs_env (State.Debug.presult_state r))) + in let type_of_result_of_pi p = let pi_free_vars = Subst.(types_of_free_vars Sctx_pure p) in SMap.find_opt "res" pi_free_vars |> Option.join From fc99584fc49d17b1201d7e94a989d8bf271a588e Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Tue, 19 Aug 2025 16:15:24 +0800 Subject: [PATCH 3/9] rewriting: substitute type uvars in more places --- lib/hipcore_typed/Pretty.ml | 3 +++ lib/hipprover/rewriting.ml | 23 ++++++++--------------- 2 files changed, 11 insertions(+), 15 deletions(-) diff --git a/lib/hipcore_typed/Pretty.ml b/lib/hipcore_typed/Pretty.ml index b67e3160..a03bd0e4 100644 --- a/lib/hipcore_typed/Pretty.ml +++ b/lib/hipcore_typed/Pretty.ml @@ -303,6 +303,9 @@ module With_types = struct | 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 *) diff --git a/lib/hipprover/rewriting.ml b/lib/hipprover/rewriting.ml index ed54eefb..e03d8bc4 100644 --- a/lib/hipprover/rewriting.ml +++ b/lib/hipprover/rewriting.ml @@ -440,16 +440,12 @@ let subst_uvars st (f, e : unifiable) : uterm = if is_uvar_name x then instantiate_uvar st e x |> uterm_to_binder else - (x, t) + (x, self#visit_typ () t) (* the remaining cases also handle capture-avoidance in addition to binder variables *) method! visit_Exists () x f = - let x = - if binder_is_uvar x then - UF.get st (SMap.find (ident_of_binder x) e) |> Option.get |> uterm_to_binder - else x - in + let x = self#visit_binder () x in (* avoid capture *) let f1 = self#visit_staged_spec () f in let x2, f2 = @@ -468,11 +464,7 @@ let subst_uvars st (f, e : unifiable) : uterm = (* other cases are copy-pasted *) method! visit_ForAll () x f = - let x = - if binder_is_uvar x then - UF.get st (SMap.find (ident_of_binder x) e) |> Option.get |> uterm_to_binder - else x - in + let x = self#visit_binder () x in let f1 = self#visit_staged_spec () f in let x2, f2 = let free = Subst.(free_vars Sctx_staged f1) in @@ -489,10 +481,8 @@ let subst_uvars st (f, e : unifiable) : uterm = method! visit_Bind () x f1 f2 = let x, f1, f2 = - if binder_is_uvar x then - let b = - UF.get st (SMap.find (ident_of_binder x) e) |> Option.get |> uterm_to_binder - in + let b = self#visit_binder () x in + if b <> x then ( b, Subst.subst_free_vars [(ident_of_binder x, var_of_binder b)] f1, Subst.subst_free_vars [(ident_of_binder x, var_of_binder b)] f2 ) @@ -514,6 +504,7 @@ let subst_uvars st (f, e : unifiable) : uterm = Bind (x2, f1, f2) method! visit_TLambda () name args spec_opt prog_opt = + let args = List.map (self#visit_binder ()) args in let renamed_args = List.map (fun arg -> (fresh_variable ~v:(ident_of_binder arg) (), type_of_binder arg)) args in let subst = List.map2 (fun arg new_arg -> (ident_of_binder arg, var_of_binder new_arg)) args renamed_args in let spec_opt = match spec_opt with @@ -528,6 +519,8 @@ let subst_uvars st (f, e : unifiable) : uterm = method! visit_Shift () b x_body f_body x_cont f_cont = (* we shall also rewrite in continuation I gues*) + let x_body = self#visit_binder () x_body in + let x_cont = self#visit_binder () x_cont in let x_body, f_body = let y = (fresh_variable ~v:(ident_of_binder x_body) (), type_of_binder x_body) in let f_body = Subst.subst_free_vars [(ident_of_binder x_body, var_of_binder y)] f_body in From 340e1b7132b707fadaa499368551934e9a2aa198 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Wed, 20 Aug 2025 16:16:25 +0800 Subject: [PATCH 4/9] change test specs to align with new HOF typechecks --- test/basic.t/run.t | 15 +++++++-------- test/basic.t/test_ho.ml | 22 ++++++++++++---------- test/basic.t/test_new_entail.ml | 6 +++--- 3 files changed, 22 insertions(+), 21 deletions(-) diff --git a/test/basic.t/run.t b/test/basic.t/run.t index 5d31330a..15a70995 100644 --- a/test/basic.t/run.t +++ b/test/basic.t/run.t @@ -29,8 +29,8 @@ if_let: true foo1: true foo2: true - goo1: false - goo2: false + goo1: true + goo2: true call_f_in_g: true call_ret: true test_non_rec_pred: true @@ -38,15 +38,14 @@ [1] $ check test_ho.ml - test1_true: false + test1_true: true test2_true: false test5_false: false (expected) - test3_true: false - test4_true: false - test6_true: false + test3_true: true + test4_true: true + test6_true: true test7_false: false (expected) - compose_true: false - compose_exists_true: false + compose_true: true [1] $ check test_lists.ml diff --git a/test/basic.t/test_ho.ml b/test/basic.t/test_ho.ml index a7eb636a..39d16656 100644 --- a/test/basic.t/test_ho.ml +++ b/test/basic.t/test_ho.ml @@ -1,6 +1,6 @@ let test1_true f - (*@ ex r. f(1, r); ens emp/\res=r @*) = + (*@ let r = f(1) in ens emp/\res=r@*) = f 1 (* disabled because this now raises an error due to g being undefined in the spec *) @@ -9,42 +9,43 @@ let test1_true f (* f 1 *) let test2_true f g - (*@ ex r s. f(1, r); g(1, s); ens emp/\res=s @*) = + (*@ let r = f(1) in let s = g(1) in ens emp/\res=s @*) = f 1; g 1 let test5_false f g - (*@ ex r s. f(1, r); g(2, s); ens emp/\res=s @*) = + (*@ let r = f(1) in let s = g(2) in ens emp /\ res=s @*) = f 1; g 1 let test3_true f g - (*@ ex r s. f(1, r); g(r, s); ens emp/\res=s @*) = + (*@ let r = f(1) in let s = g(r) in ens emp /\ res = s @*) = let x = f 1 in g x let rec test4_true () - (*@ ex r. test4_true((), r); ens emp/\res=r @*) = + (*@ let r = test4_true(()) in ens emp /\ res=r @*) = test4_true () let rec test6_true b n - (*@ ens emp/\res=0 \/ ex r. test6_true(b, n-1, r); ens emp/\res=r @*) = + (*@ ens emp/\res = 0 \/ let r = test6_true(b, n-1) in ens emp /\ res=r @*) = if b then 0 else test6_true b (n - 1) (* this is already unfolded *) let rec test7_false b n - (*@ ex r. test7_false(b, n, r); ens emp/\res=r @*) = + (*@ let r = test7_false(b, n) in ens emp/\res = r @*) = if b then 0 else test7_false b (n - 1) (* need explicit unfolding *) let compose_true f g x (*@ - ex r_g. g(x, r_g); - ex r_f. f(r_g, r_f); - ens emp/\res=r_f + let r_g = g(x) in + let r_f = f(r_g) in + ens emp/\res = r_f @*) = f (g x) +(* redundant due to examples being ported to use binds to invoke higher-order functions: let compose_exists_true f g x (*@ ex r_g r_f. @@ -53,5 +54,6 @@ let compose_exists_true f g x ens emp/\res=r_f @*) = f (g x) +*) (* the positions of existentials matter and have to match the implementation, due to the way proving is done at each stage. we optimize the positions of existentials automatically so this passes. *) diff --git a/test/basic.t/test_new_entail.ml b/test/basic.t/test_new_entail.ml index be6ca412..2a454e40 100644 --- a/test/basic.t/test_new_entail.ml +++ b/test/basic.t/test_new_entail.ml @@ -170,11 +170,11 @@ let foo1 xs = 1 let foo2 xs (*@ ens res=1 @*) = 1 let goo1 xs -(*@ ex t. foo1(xs, t); ens res=t @*) +(*@ let t = foo1(xs) in ens res=t @*) = foo1 xs let goo2 xs -(*@ ex t. foo2(xs, t); ens res=t @*) +(*@ let t = foo2(xs) in ens res=t @*) = foo2 xs let call_f_in_g () @@ -183,7 +183,7 @@ let call_f_in_g () let f x = x in f 5 -let call_ret f (* ex v; f(100,v); ens res=v *) = +let call_ret f (*@ let v = f(100) in ens res=v @*) = f 100 let test_non_rec_pred () From d239403535cd397bd97332e38cd3f1d1cdff41df Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Thu, 21 Aug 2025 12:57:27 +0800 Subject: [PATCH 5/9] create debug span for parsing ocaml code --- lib/hiplib/hiplib.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml index 4bbd06d7..04568781 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -344,7 +344,14 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core let process_ocaml_structure (items: Ocaml_common.Typedtree.structure) : unit = let process_ocaml_item (bound_names, prog) item = - match Ocamlfrontend.Core_lang_typed.transform_str bound_names item with + let intermediate = + let@ _ = Debug.(span (fun _ -> + debug ~at:3 ~title:"parsing next ocaml structure item" "" + )) + in + Ocamlfrontend.Core_lang_typed.transform_str bound_names item + in + match intermediate with | Some it -> let new_bound, prog = process_intermediates it prog in new_bound @ bound_names, prog From f3f8cbb18cc404324a9b3808eac4c245693d43a4 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Thu, 21 Aug 2025 12:57:41 +0800 Subject: [PATCH 6/9] make typing debug logging consistent --- lib/hipprover/infer_types.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/hipprover/infer_types.ml b/lib/hipprover/infer_types.ml index 3ae06d5b..cd4a14ee 100644 --- a/lib/hipprover/infer_types.ml +++ b/lib/hipprover/infer_types.ml @@ -272,7 +272,7 @@ and infer_types_constant ?(hint : typ option) const : typ = and infer_types_term ?(hint : typ option) term : term using_env = let@ _ = span_env (fun r -> - debug ~at:10 ~title:"infer_types" "%s : %s -| %s" (string_of_term term) + debug ~at:10 ~title:"infer_types_term" "%s : %s -| %s" (string_of_term term) (string_of_result string_of_term (State.Debug.presult_value r)) (string_of_result string_of_abs_env (State.Debug.presult_state r))) in From e6f202ce8527c62d118176f4d1daaaa00adfd862 Mon Sep 17 00:00:00 2001 From: Dan Baterisna Date: Thu, 21 Aug 2025 12:58:04 +0800 Subject: [PATCH 7/9] add common debug options to docs --- docs/development.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/docs/development.md b/docs/development.md index 7de2711a..e8952798 100644 --- a/docs/development.md +++ b/docs/development.md @@ -83,6 +83,12 @@ View log output by setting `DEBUG=n`. | 1 | Explanations, for users | | >= 2 | More and more detail, for developers | +Several built-in filtering options are available; these can be set by setting `DEBUG='n;