Experiment: optimized representation for nat constants (a zarith Z.t values)

checker/checkInductive.ml

@@ -105,6 +105,7 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_universes;
     mind_entry_variance;
     mind_entry_private = mb.mind_private;
+    mind_entry_is_nat = mb.mind_is_nat;
   }
 
 let check_abstract_uctx a b =
@@ -210,7 +211,9 @@ let check_inductive env mind mb =
   let { mind_packets; mind_finite; mind_hyps; mind_univ_hyps;
         mind_nparams; mind_nparams_rec; mind_params_ctxt;
         mind_universes; mind_template; mind_variance; mind_sec_variance;
-        mind_private; mind_typing_flags; }
+        mind_private; mind_typing_flags;
+        mind_is_nat;
+      }
     =
     (* Locally set typing flags for further typechecking *)
     let env = CheckFlags.set_local_flags mb.mind_typing_flags env in
@@ -241,6 +244,8 @@ let check_inductive env mind mb =
   ignore mind_typing_flags;
   (* TODO non oracle flags *)
 
+  check "mind_is_nat" (Bool.equal mb.mind_is_nat mind_is_nat);
+
   add_mind mind mb env
 
 let check_inductive env mind mb : Environ.env =

checker/values.ml

@@ -243,6 +243,9 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 let v_uint63 =
   if Sys.word_size == 64 then v_int else v_int64
 
+(* TODO *)
+let v_z = v_any
+
 let v_constr =
   fix (fun v_constr ->
 let v_prec =
@@ -275,7 +278,8 @@ let v_case_return = v_tuple_c ("case_return", [|v_tuple_c ("case_return'", [|v_a
     [|v_uint63|]; (* v_int *)
     [|v_float64|]; (* Float *)
     [|v_string|]; (* v_string *)
-    [|v_instance;v_array v_constr;v_constr;v_constr|] (* v_array *)
+    [|v_instance;v_array v_constr;v_constr;v_constr|]; (* v_array *)
+    [|v_ind;v_z|]; (* nat *)
   |]))
 
 let v_rdecl = v_sum "rel_declaration" 0
@@ -483,7 +487,9 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_opt (v_array v_variance);
     v_opt (v_array v_variance);
     v_opt v_bool;
-    v_typing_flags|]
+    v_typing_flags;
+    v_bool;
+  |]
 
 let v_prim_ind = v_enum "prim_ind" 6
 (* Number of "Register ... as kernel.ind_..." in Primv_int63.v and PrimFloat.v *)
@@ -495,6 +501,7 @@ let v_retro_action =
   v_sum "retro_action" 0 [|
     [|v_prim_ind; v_ind|];
     [|v_prim_type; v_cst|];
+    [|v_ind|]
   |]
 
 let v_retroknowledge =

dev/bench/bench.sh

@@ -54,7 +54,7 @@ check_variable () {
 
 # example: coq-hott.dev git+https://github.com/some-user/coq-hott#some-branch
 # (make sure to include the version for the opam package, note that just https won't work)
-: "${new_opam_override_urls:=}"
+: "${new_opam_override_urls:=rocq-elpi.dev git+https://github.com/skyskimmer/coq-elpi#bignat rocq-equations.dev git+https://github.com/skyskimmer/coq-equations#bignat}"
 : "${old_opam_override_urls:=}"
 
 if [ "$CI" ]; then

dev/ci/user-overlays/21729-SkySkimmer-bignat.sh

@@ -0,0 +1,3 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi bignat 21729
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations bignat 21729

dev/top_printers.ml

@@ -402,6 +402,7 @@ let constr_display csr =
       ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
         then (";"^i) else "")) lna "")^","
       ^(array_display bl)^")"
+  | Nat (ind,n) -> "Nat("^(MutInd.to_string (fst ind))^Z.to_string n^")"
   | Int i ->
       "Int("^(Uint63.to_string i)^")"
   | Float f ->
@@ -563,6 +564,8 @@ let print_pure_constr csr =
           print_cut();
         done
       in print_string"{"; print_fix (); print_string"}"
+  | Nat (ind,n) ->
+     print_string ("Nat("^MutInd.to_string (fst ind)^(Z.to_string n)^")")
   | Int i ->
      print_string ("Int("^(Uint63.to_string i)^")")
   | Float f ->

dev/vm_printers.ml

@@ -76,6 +76,7 @@ and ppwhd whd =
   | Vcofix _ -> print_string "cofix"
   | Vconst i -> print_string "C(";print_int i;print_string")"
   | Vblock b -> ppvblock b
+  | Vnat n -> printf "nat(%s)" (Z.to_string n)
   | Vint64 i -> printf "int64(%LiL)" i
   | Vfloat64 f -> printf "float64(%.17g)" f
   | Vstring s -> printf "string(%S)" (Pstring.to_string s)

engine/eConstr.ml

@@ -99,7 +99,7 @@ struct
     (* Despite the type, the sparse list contains no default element *)
     SList.Skip.iter (f h) args
   | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-  | Construct _ | Int _ | Float _ | String _ -> ()
+  | Construct _ | Nat _ | Int _ | Float _ | String _ -> ()
   | Cast (c, _, t) -> f h c; f h t
   | Prod (_, t, c) -> f h t; f (liftn_handle 1 h) c
   | Lambda (_, t, c) -> f h t; f (liftn_handle 1 h) c
@@ -128,7 +128,7 @@ struct
     (* Despite the type, the sparse list contains no default element *)
     SList.Skip.iter (f l h) args
   | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-  | Construct _ | Int _ | Float _ | String _ -> ()
+  | Construct _ | Nat _ | Int _ | Float _ | String _ -> ()
   | Cast (c, _, t) -> f l h c; f l h t
   | Prod (_, t, c) -> f l h t; f (g l) (liftn_handle 1 h) c
   | Lambda (_, t, c) -> f l h t; f (g l) (liftn_handle 1 h) c
@@ -209,6 +209,7 @@ let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, r, c) = of_kind (Proj (p, r, c))
 let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
 let mkArrowR t1 t2 = mkArrow t1 ERelevance.relevant t2
+let mkNat ind n = of_kind (Nat (ind,n))
 let mkInt i = of_kind (Int i)
 let mkFloat f = of_kind (Float f)
 let mkString s = of_kind (String s)
@@ -350,6 +351,13 @@ let destRef sigma c = let open GlobRef in match kind sigma c with
   | Construct (c,u) -> ConstructRef c, u
   | _ -> raise DestKO
 
+let kind_nonat sigma c =
+  match kind sigma c with
+  | Nat (ind,n) ->
+    if Z.equal n Z.zero then Construct (in_punivs (ind,1))
+    else App (of_kind (Construct (in_punivs (ind,2))), [|of_kind (Nat (ind,Z.pred n))|])
+  | k -> k
+
 let decompose_app sigma c =
   match kind sigma c with
   | App (f,cl) -> (f, cl)
@@ -659,11 +667,13 @@ let contract_case env _sigma (ci, (p,r), iv, c, bl) =
   let bl = of_branches bl in
   (ci, u, pms, p, iv, c, bl)
 
+let unfold_nat ind n = of_constr @@ unfold_nat ind n
+
 let iter_with_full_binders env sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _ | Float _ | String _) -> ()
+    | Construct _ | Nat _ | Int _ | Float _ | String _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
@@ -1252,7 +1262,7 @@ let kind_of_type sigma t = match kind sigma t with
   | (Rel _ | Meta _ | Var _ | Evar _ | Const _
   | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
     -> AtomicType (t,[||])
-  | (Lambda _ | Construct _ | Int _ | Float _ | String _ | Array _) -> failwith "Not a type"
+  | (Lambda _ | Construct _ | Nat _ | Int _ | Float _ | String _ | Array _) -> failwith "Not a type"
 
 module Unsafe =
 struct

engine/eConstr.mli

@@ -117,6 +117,8 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t, ERelevance.t) Cons
 val kind_upto : Evd.evar_map -> Constr.t ->
   (Constr.t, Constr.t, Sorts.t, UVars.Instance.t, Sorts.relevance) Constr.kind_of_term
 
+val kind_nonat : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term
+
 val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
 (** Returns the evar-normal form of the argument. Note that this
    function is supposed to be called when the original term has not
@@ -179,6 +181,7 @@ val mkFix : (t, t, ERelevance.t) pfixpoint -> t
 val mkCoFix : (t, t, ERelevance.t) pcofixpoint -> t
 val mkArrow : t -> ERelevance.t  -> t -> t
 val mkArrowR : t -> t -> t
+val mkNat : inductive -> Z.t -> t
 val mkInt : Uint63.t -> t
 val mkFloat : Float64.t -> t
 val mkString : Pstring.t -> t
@@ -463,6 +466,8 @@ val expand_branch : Environ.env -> Evd.evar_map ->
 val contract_case : Environ.env -> Evd.evar_map ->
   (t,t,ERelevance.t) Inductive.pexpanded_case -> case
 
+val unfold_nat : inductive -> Z.t -> constr
+
 (** {5 Extra} *)
 
 val of_existential : Constr.existential -> existential

engine/evd.ml

@@ -1598,7 +1598,7 @@ let rec kind sigma h c = match Constr.kind c with
   end
 | Meta _ | Sort _ | Cast _  | Prod _ | Lambda _ | LetIn _ | App _
 | Const _ | Ind _ | Construct _ | Case _ | Fix _ | CoFix _ | Proj _
-| Int _ | Float _ | String _ | Array _ as c0 ->
+| Nat _ | Int _ | Float _ | String _ | Array _ as c0 ->
   (h, c0)
 
 let expand0 sigma h c =

engine/namegen.ml

@@ -119,6 +119,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
     | Cast (c,_,_) | App (c,_) -> hdrec c
     | Proj (kn,_,_) -> Some (Constant.label (Projection.constant kn))
+    | Nat (ind,n) -> Some (Nametab.basename_of_global (ConstructRef (ctor_of_nat ind n)))
     | Const _ | Ind _ | Construct _ | Var _ as c ->
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
@@ -156,6 +157,7 @@ let hdchar env sigma c =
     | Const (kn,_) -> lowercase_first_char (Constant.label kn)
     | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Nat (ind,n) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef (ctor_of_nat ind n))) with _ when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->

engine/termops.ml

@@ -544,9 +544,9 @@ let map_left2 f a g b =
 let map_constr_with_binders_left_to_right env sigma g f l c =
   let open RelDecl in
   let open EConstr in
-  match EConstr.kind sigma c with
+  match EConstr.kind_nonat sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _ | Float _ | String _) -> c
+    | Construct _ | Nat _ | Int _ | Float _ | String _) -> c
   | Cast (b,k,t) ->
     let b' = f l b in
     let t' = f l t in
@@ -622,7 +622,7 @@ let map_constr_with_full_binders env sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _ | Float _ | String _) -> cstr
+    | Construct _ | Nat _ | Int _ | Float _ | String _) -> cstr
   | Cast (c,k, t) ->
       let c' = f l c in
       let t' = f l t in
@@ -694,7 +694,7 @@ let fold_constr_with_full_binders env sigma g f n acc c =
   let open EConstr.Vars in
   let open Context.Rel.Declaration in
   match EConstr.kind sigma c with
-  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ | String _ -> acc
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Nat _ | Int _ | Float _ | String _ -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
   | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c

interp/constrextern.ml

@@ -1041,6 +1041,12 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r =
     let c = extern depth true (fst scopes,(scl, snd (snd scopes))) eenv c in
     CCast (c, k, c')
 
+  | GNat (_,n) ->
+    (* XXX should use the inductive!! *)
+     extern_prim_token_delimiter_if_required
+       (Number NumTok.(Signed.of_bigint CHex n))
+       "nat" "nat_scope" (snd scopes)
+
   | GInt i ->
      extern_prim_token_delimiter_if_required
        (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i))))
@@ -1510,6 +1516,7 @@ let rec glob_of_pat
   | PSort (Qual (QConstant QProp)) -> GSort Glob_ops.glob_Prop_sort
   | PSort (Qual (QConstant QType | QVar _)) -> GSort Glob_ops.glob_Type_sort
   | PSort Set -> GSort Glob_ops.glob_Set_sort
+  | PNat (ind,n) -> GNat (ind,n)
   | PInt i -> GInt i
   | PFloat f -> GFloat f
   | PString s -> GString s

interp/constrintern.ml

@@ -880,7 +880,7 @@ let rec adjust_env env = function
   | NCast (c,_,_) -> adjust_env env c
   | NApp _ -> restart_no_binders env
   | NVar _ | NRef _ | NHole _ | NGenarg _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NProj _ | NInt _ | NFloat _ | NString _ | NArray _
+  | NRec _ | NSort _ | NProj _ | NNat _ | NInt _ | NFloat _ | NString _ | NArray _
   | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *)
 
 let subst_var loc intern_pat intern ntnvars binders (terms, binderopt, _terminopt) (renaming, env) id =
@@ -1784,6 +1784,15 @@ type global_reference_test = {
   test_kind : ?loc:Loc.t -> GlobRef.t -> unit
 }
 
+let rcp_of_nat ?loc ind n =
+  assert (Z.leq Z.zero n);
+  let ctor_S = GlobRef.ConstructRef (ind,2) in
+  let rec aux acc n =
+    if Z.equal n Z.zero then acc
+    else aux (RCPatCstr (ctor_S, [DAst.make ?loc acc])) (Z.pred n)
+  in
+  aux (RCPatCstr (ConstructRef (ind,1), [])) n
+
 let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
      only constructor are allowed *)
@@ -1815,12 +1824,14 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
           List.iter (check_allowed_ref_in_pat test_kind_inner) l
         | _ -> raise Not_found
         end
+      | GNat _ -> ()
       | _ -> raise Not_found)) in
   (* Interpret a primitive notation (part of Glob_ops.cases_pattern_of_glob_constr) *)
   let rec rcp_of_glob scopes x = DAst.(map_with_loc (fun ?loc -> function
     | GVar id -> RCPatAtom (Some (CAst.make ?loc id,scopes))
     | GHole _ -> RCPatAtom None
     | GRef (g,_) -> RCPatCstr (g, in_patargs ?loc scopes g ~expanded:true ~no_impl:false [] [])
+    | GNat (ind,n) -> rcp_of_nat ?loc ind n
     | GApp (r, l) ->
       begin match DAst.get r with
       | GRef (g,_) ->
@@ -1989,6 +2000,11 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
     | NRef (g,_) ->
       ensure_kind test_kind ?loc g;
       DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g ~expanded:true ~no_impl:false [] args)
+    | NNat (ind,n) ->
+      (* test_kind should return the same on all constructors of nat
+         so no need to call multiple times *)
+      ensure_kind test_kind ?loc (ConstructRef (ctor_of_nat ind n));
+      DAst.make ?loc @@ rcp_of_nat ?loc ind n
     | NApp (NRef (g,_),ntnpl) ->
       ensure_kind test_kind ?loc g;
       let ntnpl = List.map (in_not test_kind_inner loc scopes fullsubst []) ntnpl in

interp/impargs.ml

@@ -240,7 +240,7 @@ let rec is_rigid_head sigma t = match kind sigma t with
         | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
         | _ -> is_rigid_head sigma f)
   | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
-  | Prod _ | Meta _ | Cast _ | Int _ | Float _ | String _ | Array _ -> assert false
+  | Prod _ | Meta _ | Cast _ | Nat _ | Int _ | Float _ | String _ | Array _ -> assert false
 
 let is_rigid env sigma t =
   let open Context.Rel.Declaration in

interp/notation.ml

@@ -341,6 +341,9 @@ let glob_prim_constr_key c = match DAst.get c with
     | _ -> None
     end
   | GProj ((cst,_), _, _) -> Some (canonical_gr (GlobRef.ConstRef cst))
+  | GNat (ind,n) ->
+    let c = Constr.ctor_of_nat ind n in
+    Some (canonical_gr (GlobRef.ConstructRef c))
   | _ -> None
 
 let check_required_module ?loc sc (sp,d) =

interp/notation_ops.ml

@@ -255,6 +255,7 @@ let compare_notation_constr lt var_eq_hole (vars1,vars2) t1 t2 =
     aux vars renaming c1 c2;
     if not (Option.equal cast_kind_eq k1 k2) then raise_notrace Exit;
     aux vars renaming t1 t2
+  | NNat (ind1,n1), NNat (ind2,n2) when Z.equal n1 n2 && Ind.CanOrd.equal ind1 ind2 -> ()
   | NInt i1, NInt i2 when Uint63.equal i1 i2 -> ()
   | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> ()
   | NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
@@ -263,7 +264,7 @@ let compare_notation_constr lt var_eq_hole (vars1,vars2) t1 t2 =
     aux vars renaming ty1 ty2
   | (NRef _ | NVar _ | NApp _ | NProj _ | NHole _ | NGenarg _ | NList _ | NLambda _ | NProd _
     | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-    | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NString _ | NArray _), _ -> raise_notrace Exit in
+    | NRec _ | NSort _ | NCast _ | NNat _ | NInt _ | NFloat _ | NString _ | NArray _), _ -> raise_notrace Exit in
   try
     let _ = aux (vars1,vars2) [] t1 t2 in
     if not lt then
@@ -466,6 +467,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
   | NHole x  -> GHole x
   | NGenarg arg -> GGenarg arg
   | NRef (x,u) -> GRef (x,u)
+  | NNat (ind,n) -> GNat (ind,n)
   | NInt i -> GInt i
   | NFloat f -> GFloat f
   | NString s -> GString s
@@ -700,6 +702,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
     if Option.is_empty k then forgetful := { !forgetful with forget_volatile_cast = true };
     NCast (aux c, k, aux t)
   | GSort s -> NSort s
+  | GNat (ind,n) -> NNat (ind,n)
   | GInt i -> NInt i
   | GFloat f -> NFloat f
   | GString s -> NString s
@@ -908,6 +911,7 @@ let rec subst_notation_constr subst bound raw =
           NRec (fk,idl,dll',tl',bl')
 
   | NSort _ -> raw
+  | NNat _ -> raw
   | NInt _ -> raw
   | NFloat _ -> raw
   | NString _ -> raw
@@ -1629,7 +1633,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GProj _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GGenarg _
-     | GCast _ | GInt _ | GFloat _ | GString _ | GArray _), _ -> raise No_match
+     | GCast _ | GNat _ | GInt _ | GFloat _ | GString _ | GArray _), _ -> raise No_match
 
 and match_in_type u alp metas sigma t = function
   | None -> sigma

interp/notation_term.mli

@@ -44,6 +44,7 @@ type notation_constr =
       notation_constr array * notation_constr array
   | NSort of glob_sort
   | NCast of notation_constr * Constr.cast_kind option * notation_constr
+  | NNat of inductive * Z.t
   | NInt of Uint63.t
   | NFloat of Float64.t
   | NString of Pstring.t