Added typing flag for sized typing similar to issue coq#10291; remove…

…d sized_typing plugin that did the same thing.

META.coq.in

@@ -493,16 +493,4 @@ package "plugins" (
     archive(byte)    = "ssreflect_plugin.cmo"
     archive(native)  = "ssreflect_plugin.cmx"
   )
-
-  package "sized_typing" (
-
-    description = "Coq sized typing plugin"
-    version     = "8.10"
-
-    requires    = ""
-    directory   = "sized_typing"
-
-    archive(byte)   = "sized_typing_plugin.cmo"
-    archive(native) = "sized_typing_plugin.cmx"
-  )
 )

Makefile.common

@@ -103,7 +103,7 @@ PLUGINDIRS:=\
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
-  sized_typing   ssrmatching	ltac		ssr
+  ssrmatching	ltac		ssr
 
 USERCONTRIBDIRS:=\
 	Ltac2
@@ -152,7 +152,6 @@ SYNTAXCMO:=$(addprefix plugins/syntax/, \
 	string_notation_plugin.cmo)
 DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
-SIZEDTYPINGCMO:=plugins/sized_typing/sized_typing_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
@@ -162,7 +161,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-	$(DERIVECMO) $(SIZEDTYPINGCMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)

checker/checkInductive.ml

@@ -140,16 +140,17 @@ let check_inductive env mind mb =
   let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
         mind_nparams; mind_nparams_rec; mind_params_ctxt;
         mind_universes; mind_variance;
-        mind_private; mind_typing_flags; }
-    =
+        mind_private; mind_typing_flags; } =
     (* Locally set typing flags for further typechecking *)
     let mb_flags = mb.mind_typing_flags in
-    let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded;
-                                                                  check_positive = mb_flags.check_positive;
-                                                                  check_universes = mb_flags.check_universes;
-                                                                  conv_oracle = mb_flags.conv_oracle} env in
-    Indtypes.check_inductive env mind entry
-  in
+    let env = Environ.set_typing_flags
+      { env.env_typing_flags with
+        check_guarded   = mb_flags.check_guarded;
+        check_sized     = mb_flags.check_sized;
+        check_positive  = mb_flags.check_positive;
+        check_universes = mb_flags.check_universes;
+        conv_oracle     = mb_flags.conv_oracle } env in
+    Indtypes.check_inductive env mind entry in
   let check = check mind in
 
   Array.iter2 (check_packet env mind) mb.mind_packets mind_packets;

checker/check_stat.ml

@@ -52,6 +52,11 @@ let pr_unguarded env =
   let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in
   pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts
 
+let pr_unsized env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_sized then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_sized then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints with respect to sized typing" csts
+
 let pr_nonpositive env =
   let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
   pr_assumptions "Inductives whose positivity is assumed" inds
@@ -67,6 +72,7 @@ let print_context env =
       str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_unsized env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_nonpositive env)))
   end
 

checker/mod_checking.ml

@@ -19,12 +19,11 @@ let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   let cb_flags = cb.const_typing_flags in
   let env = Environ.set_typing_flags
-      {env.env_typing_flags with
-       check_guarded = cb_flags.check_guarded;
-       check_universes = cb_flags.check_universes;
-       conv_oracle = cb_flags.conv_oracle;}
-      env
-  in
+    { env.env_typing_flags with
+      check_guarded   = cb_flags.check_guarded;
+      check_sized     = cb_flags.check_sized;
+      check_universes = cb_flags.check_universes;
+      conv_oracle     = cb_flags.conv_oracle; } env in
   let poly, env =
     match cb.const_universes with
     | Monomorphic ctx ->

checker/values.ml

@@ -219,7 +219,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 

kernel/safe_typing.ml

@@ -198,6 +198,10 @@ let set_check_guarded b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with check_guarded = b } senv
 
+let set_check_sized b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_sized = b } senv
+
 let set_check_positive b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with check_positive = b } senv

kernel/safe_typing.mli

@@ -131,6 +131,7 @@ val set_indices_matter : bool -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
 val set_check_guarded : bool -> safe_transformer0
+val set_check_sized : bool -> safe_transformer0
 val set_check_positive : bool -> safe_transformer0
 val set_check_universes : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0

library/global.ml

@@ -90,6 +90,7 @@ let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
+let set_check_sized c = globalize0 (Safe_typing.set_check_sized c)
 let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
 let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
 let typing_flags () = Environ.typing_flags (env ())

library/global.mli

@@ -32,6 +32,7 @@ val set_engagement : Declarations.engagement -> unit
 val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
 val set_check_guarded : bool -> unit
+val set_check_sized : bool -> unit
 val set_check_positive : bool -> unit
 val set_check_universes : bool -> unit
 val typing_flags : unit -> Declarations.typing_flags

printing/printer.ml

@@ -854,6 +854,7 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Sized of GlobRef.t (* a constant whose (co)fixpoints have been assumed to satisfy sized typing *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
@@ -875,6 +876,8 @@ struct
         MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
         GlobRef.Ordered.compare k1 k2
+    | Sized k1 , Sized k2 ->
+        GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
     | _ -> -1
@@ -937,6 +940,8 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded gr ->
           hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
+      | Sized gr ->
+          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to satisfy sized typing.")
       | TypeInType gr ->
          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
@@ -1015,5 +1020,6 @@ let print_and_diff oldp newp =
 
 let pr_typing_flags flags =
   str "check_guarded: " ++ bool flags.check_guarded ++ fnl ()
+  ++ str "check_sized: " ++ bool flags.check_sized ++ fnl ()
   ++ str "check_positive: " ++ bool flags.check_positive ++ fnl ()
   ++ str "check_universes: " ++ bool flags.check_universes

printing/printer.mli

@@ -192,6 +192,7 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Sized of GlobRef.t (* a constant whose (co)fixpoints have been assumed to satisfy sized typing *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =

test-suite/success/typing_flags.v

@@ -41,3 +41,40 @@ Inductive Box :=
 | box : forall n, f n = n -> g 2 -> Box.
 
 Print Assumptions Box.
+
+Unset Guard Checking.
+Set Sized Typing.
+
+(* Fails with guard checking but not with sized typing *)
+Fixpoint div x y :=
+  match x with
+  | O => O
+  | S x' => S (div (minus x' y) y)
+  end.
+
+(* The below are lifted from theories/Init/Nat.v *)
+
+Fixpoint divmod x y q u :=
+  match x with
+  | 0 => (q,u)
+  | S x' =>
+    match u with
+    | 0 => divmod x' y (S q) y
+    | S u' => divmod x' y q u'
+    end
+  end.
+
+Definition modulo x y :=
+  match y with
+  | 0 => y
+  | S y' => y' - snd (divmod x y' 0 y')
+  end.
+
+Infix "mod" := modulo (at level 40, no associativity) : nat_scope.
+
+(* Fails with sized typing but not with guard checking *)
+Fail Fixpoint gcd a b :=
+  match a with
+  | O => b
+  | S a' => gcd (b mod (S a')) (S a')
+  end.

vernac/assumptions.ml

@@ -315,6 +315,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu
       in
+      let accu =
+        if cb.const_typing_flags.check_sized then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (Sized obj, l)) Constr.mkProp accu
+      in
       let accu =
         if cb.const_typing_flags.check_universes then accu
         else
@@ -347,6 +353,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu
       in
+      let accu =
+        if mind.mind_typing_flags.check_sized then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (Sized obj, l)) Constr.mkProp accu
+      in
       let accu =
         if mind.mind_typing_flags.check_universes then accu
         else

vernac/vernacentries.ml

@@ -1732,6 +1732,14 @@ let _ =
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
       optwrite = (fun b -> Global.set_check_guarded b) }
 
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "sized typing";
+      optkey   = ["Sized"; "Typing"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_sized);
+      optwrite = (fun b -> Global.set_check_sized b) }
+
 let _ =
   declare_bool_option
     { optdepr  = false;