feat(term): add App_uncurried constructor

sometimes currying is really costly. For example, in boolean formulas,
the formula `/\_i=1^100 a_i` has 100 atoms as subterms, but if
represented curried with binary `/\` it also has 98 intermediate
conjunctions as subterms. With how the rest of sidekick works, this
means each of these gets its own atom and CNF; instead we're going to
use App_uncurried.

src/core-logic/term.ml

@@ -10,6 +10,7 @@ type view = term_view =
   | E_bound_var of bvar
   | E_const of const
   | E_app of term * term
+  | E_app_uncurried of { c: const; ty: term; args: term list }
   | E_lam of string * term * term
   | E_pi of string * term * term
 
@@ -74,6 +75,10 @@ let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
       Fmt.fprintf out "(@[\\_:@[%a@].@ %a@])" pp' _ty
         (loop (k + 1) ~depth:(depth + 1) ("" :: names))
         bod
+    | E_app_uncurried { c; args; ty = _ } ->
+      Fmt.fprintf out "(@[%a" Const.pp c;
+      List.iter (fun x -> Fmt.fprintf out "@ %a" pp' x) args;
+      Fmt.fprintf out "@])"
     | E_lam (n, _ty, bod) ->
       Fmt.fprintf out "(@[\\%s:@[%a@].@ %a@])" n pp' _ty
         (loop (k + 1) ~depth:(depth + 1) (n :: names))
@@ -123,12 +128,14 @@ module Hcons = Hashcons.Make (struct
     | E_var v1, E_var v2 -> Var.equal v1 v2
     | E_bound_var v1, E_bound_var v2 -> Bvar.equal v1 v2
     | E_app (f1, a1), E_app (f2, a2) -> equal f1 f2 && equal a1 a2
+    | E_app_uncurried a1, E_app_uncurried a2 ->
+      Const.equal a1.c a2.c && List.equal equal a1.args a2.args
     | E_lam (_, ty1, bod1), E_lam (_, ty2, bod2) ->
       equal ty1 ty2 && equal bod1 bod2
     | E_pi (_, ty1, bod1), E_pi (_, ty2, bod2) ->
       equal ty1 ty2 && equal bod1 bod2
-    | ( ( E_type _ | E_const _ | E_var _ | E_bound_var _ | E_app _ | E_lam _
+    | ( ( E_type _ | E_const _ | E_var _ | E_bound_var _ | E_app _
-        | E_pi _ ),
+        | E_app_uncurried _ | E_lam _ | E_pi _ ),
         _ ) ->
       false
 
@@ -139,6 +146,8 @@ module Hcons = Hashcons.Make (struct
     | E_var v -> H.combine2 30 (Var.hash v)
     | E_bound_var v -> H.combine2 40 (Bvar.hash v)
     | E_app (f, a) -> H.combine3 50 (hash f) (hash a)
+    | E_app_uncurried a ->
+      H.combine3 55 (Const.hash a.c) (Hash.list hash a.args)
     | E_lam (_, ty, bod) -> H.combine3 60 (hash ty) (hash bod)
     | E_pi (_, ty, bod) -> H.combine3 70 (hash ty) (hash bod)
 
@@ -180,6 +189,9 @@ let iter_shallow ~f (e : term) : unit =
     | E_app (hd, a) ->
       f false hd;
       f false a
+    | E_app_uncurried { ty; args; _ } ->
+      f false ty;
+      List.iter (fun u -> f false u) args
     | E_lam (_, tyv, bod) | E_pi (_, tyv, bod) ->
       f false tyv;
       f true bod)
@@ -206,6 +218,13 @@ let map_shallow_ ~make ~f (e : term) : term =
       e
     else
       make (E_app (f false hd, f false a))
+  | E_app_uncurried { args = l; c; ty } ->
+    let l' = List.map (fun u -> f false u) l in
+    let ty' = f false ty in
+    if equal ty ty' && CCList.equal equal l l' then
+      e
+    else
+      make (E_app_uncurried { c; ty = ty'; args = l' })
   | E_lam (n, tyv, bod) ->
     let tyv' = f false tyv in
     let bod' = f true bod in
@@ -285,6 +304,8 @@ module Make_ = struct
         | E_type _ | E_const _ | E_var _ -> 0
         | E_bound_var v -> v.bv_idx + 1
         | E_app (a, b) -> max (db_depth a) (db_depth b)
+        | E_app_uncurried { args; _ } ->
+          List.fold_left (fun x u -> max x (db_depth u)) 0 args
         | E_lam (_, ty, bod) | E_pi (_, ty, bod) ->
           max (db_depth ty) (max 0 (db_depth bod - 1))
       in
@@ -301,6 +322,7 @@ module Make_ = struct
       | E_var _ -> true
       | E_type _ | E_bound_var _ | E_const _ -> false
       | E_app (a, b) -> has_fvars a || has_fvars b
+      | E_app_uncurried { args; _ } -> List.exists has_fvars args
       | E_lam (_, ty, bod) | E_pi (_, ty, bod) -> has_fvars ty || has_fvars bod
 
   let universe_ (e : term) : int =
@@ -428,6 +450,7 @@ module Make_ = struct
           "@[<2>cannot apply %a@ (to %a),@ must have Pi type, but actual type \
            is %a@]"
           pp_debug f pp_debug a pp_debug ty_f)
+    | E_app_uncurried { ty; _ } -> ty
     | E_pi (_, ty, bod) ->
       (* TODO: check the actual triplets for COC *)
       (*Fmt.printf "pi %a %a@." pp_debug ty pp_debug bod;*)
@@ -478,6 +501,9 @@ module Make_ = struct
   let app store f a = make_ store (E_app (f, a))
   let app_l store f l = List.fold_left (app store) f l
 
+  let app_uncurried store c args ~ty : t =
+    make_ store (E_app_uncurried { c; args; ty })
+
   type cache = t T_int_tbl.t
 
   let create_cache : int -> cache = T_int_tbl.create

src/core-logic/term.mli

@@ -32,6 +32,7 @@ type view = term_view =
   | E_bound_var of bvar
   | E_const of const
   | E_app of t * t
+  | E_app_uncurried of { c: const; ty: term; args: term list }
   | E_lam of string * t * t
   | E_pi of string * t * t
 
@@ -117,6 +118,7 @@ val bvar_i : store -> int -> ty:t -> t
 val const : store -> const -> t
 val app : store -> t -> t -> t
 val app_l : store -> t -> t list -> t
+val app_uncurried : store -> const -> t list -> ty:t -> t
 val lam : store -> var -> t -> t
 val pi : store -> var -> t -> t
 val arrow : store -> t -> t -> t

src/core-logic/types_.ml

@@ -16,6 +16,7 @@ type term_view =
   | E_bound_var of bvar
   | E_const of const
   | E_app of term * term
+  | E_app_uncurried of { c: const; ty: term; args: term list }
   | E_lam of string * term * term
   | E_pi of string * term * term
 

src/core/t_printer.ml

@@ -49,6 +49,10 @@ let expr_pp_with_ ~max_depth ~hooks out (e : term) : unit =
       | E_app _ ->
         let f, args = unfold_app e in
         Fmt.fprintf out "(%a@ %a)" pp' f (Util.pp_list pp') args
+      | E_app_uncurried { c; args; ty = _ } ->
+        Fmt.fprintf out "(@[%a" Const.pp c;
+        List.iter (fun x -> Fmt.fprintf out "@ %a" pp' x) args;
+        Fmt.fprintf out "@])"
       | E_lam ("", _ty, bod) ->
         Fmt.fprintf out "(@[\\_:@[%a@].@ %a@])" pp' _ty
           (loop (k + 1) ~depth:(depth + 1) ("" :: names))
@@ -74,7 +78,7 @@ let expr_pp_with_ ~max_depth ~hooks out (e : term) : unit =
           bod
     )
   in
-  Fmt.fprintf out "@[%a@]" (loop 0 ~depth:0 []) e
+  Fmt.fprintf out "@[<1>%a@]" (loop 0 ~depth:0 []) e
 
 let pp_with hooks out e : unit = expr_pp_with_ ~max_depth:max_int ~hooks out e
 let pp out e = pp_with !default_hooks out e