Account for types of higher-order functions during typechecking

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; <option 1>; <option 2>; ...`. See the documentation of `debug.mli` for more details.
+
+Some helpful options:
+- `h rewrite_*` filters out all logs related to the rewrite libraries (which appear at level 5 and above).
+- `h unify_types; h infer_types*` filters out all logs related to type inference (which appear at level 10 and above).
+
 Set `FILE=1` to direct logs to an org-mode file, which is useful for structural navigation.
 
 Set `CTF=1` to produce a trace file that can be viewed with [Perfetto](https://ui.perfetto.dev/), queried with [PerfettoSQL](https://perfetto.dev/docs/quickstart/trace-analysis), etc. This is useful for profiling.

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 =

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

lib/hiplib/hiplib.ml

@@ -343,15 +343,20 @@ let process_intermediates (it : Typedhip.intermediate) prog : binder list * core
       [m_name, function_type], prog
 
 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 untyped_items = Untypeast.untype_structure items in
+  let process_ocaml_item (bound_names, prog) (item_untyped, item) =
+    let@ _ = Debug.(span (fun _ -> 
+      debug ~at:3 ~title:"processing next ocaml structure item" "%s" (Pprintast.string_of_structure [item_untyped])
+    )) in
+    let intermediate = 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
     | None ->
         bound_names, prog
   in
-  ignore (List.fold_left process_ocaml_item ([], empty_program) items.str_items)
+  ignore (List.fold_left process_ocaml_item ([], empty_program) (List.combine untyped_items items.str_items))
 
 let run_ocaml_string s =
   (** Parse and typecheck the code, before converting it into a core language program.

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_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
@@ -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
@@ -464,20 +469,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

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 = self#visit_list 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

test/basic.t/run.t

@@ -29,24 +29,23 @@
                 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
              test_read: true
   [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

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

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