SometimesSquashed of quality set instead of list

coq · Nov 24, 2023 · f85461c · f85461c
1 parent e4bd892
commit f85461c
Show file tree

Hide file tree

Showing 7 changed files with 20 additions and 11 deletions.
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
@@ -117,7 +117,7 @@ let check_squashed orig generated = match orig, generated with
     | AlwaysSquashed, SometimesSquashed _ -> true
     | SometimesSquashed _, AlwaysSquashed -> false
     | SometimesSquashed s1, SometimesSquashed s2 ->
-      List.for_all (fun s2 -> List.exists (fun s1 -> Sorts.Quality.equal s1 s2) s1) s2
+      Sorts.Quality.Set.subset s2 s1
 
 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost
    the knowledge of who is the canonical version.

diff --git a/checker/values.ml b/checker/values.ml
@@ -281,7 +281,7 @@ let v_mono_ind_arity =
 let v_ind_arity = v_sum "inductive_arity" 0
   [|[|v_mono_ind_arity|];[|v_template_arity|]|]
 
-let v_squash_info = v_sum "squash_info" 1 [|[|List v_quality|]|]
+let v_squash_info = v_sum "squash_info" 1 [|[|v_set v_quality|]|]
 
 let v_one_ind = v_tuple "one_inductive_body"
   [|v_id;

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
@@ -166,7 +166,7 @@ type inductive_arity = (regular_inductive_arity, template_arity) declaration_ari
 
 type squash_info =
   | AlwaysSquashed
-  | SometimesSquashed of Sorts.Quality.t list
+  | SometimesSquashed of Sorts.Quality.Set.t
   (** A sort polymorphic inductive [I@{...|...|...} : ... -> Type@{ s|...}]
       is squashed at a given instantiation if any quality in the list is not smaller than [s].
 

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
@@ -82,11 +82,11 @@ type univ_info =
 
 let add_squash q info =
   match info.ind_squashed with
-  | None -> { info with ind_squashed = Some (SometimesSquashed [q]) }
+  | None -> { info with ind_squashed = Some (SometimesSquashed (Sorts.Quality.Set.singleton q)) }
   | Some AlwaysSquashed -> info
   | Some (SometimesSquashed qs) ->
     (* XXX dedup insertion *)
-    { info with ind_squashed = Some (SometimesSquashed (q::qs)) }
+    { info with ind_squashed = Some (SometimesSquashed (Sorts.Quality.Set.add q qs)) }
 
 (* This code can probably be simplified but I can't quite see how right now. *)
 let check_univ_leq ?(is_real_arg=false) env u info =
@@ -334,7 +334,12 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) =
   let squashed = Option.map (function
       | AlwaysSquashed -> AlwaysSquashed
       | SometimesSquashed qs ->
-        SometimesSquashed (List.map (UVars.subst_sort_level_quality usubst) qs))
+        let qs = Sorts.Quality.Set.fold (fun q qs ->
+            Sorts.Quality.Set.add (UVars.subst_sort_level_quality usubst q) qs)
+            qs
+            Sorts.Quality.Set.empty
+        in
+        SometimesSquashed qs)
       univ_info.ind_squashed
   in
 

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
@@ -342,8 +342,11 @@ let is_squashed ((_,mip),u) =
       | SometimesSquashed squash ->
         (* impredicative set squashes are always AlwaysSquashed,
            so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *)
-        let squash = List.map (UVars.subst_instance_quality u) squash in
-        if List.for_all (fun q -> quality_leq q indq) squash then None
+        if Sorts.Quality.Set.for_all (fun q ->
+            let q = UVars.subst_instance_quality u q in
+            quality_leq q indq)
+            squash
+        then None
         else Some (SquashToQuality indq)
 
 let is_allowed_elimination specifu s =

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
@@ -116,7 +116,7 @@ let check_variance error v1 v2 =
 
 let squash_info_equal s1 s2 = match s1, s2 with
   | AlwaysSquashed, AlwaysSquashed -> true
-  | SometimesSquashed s1, SometimesSquashed s2 -> List.equal Sorts.Quality.equal s1 s2
+  | SometimesSquashed s1, SometimesSquashed s2 -> Sorts.Quality.Set.equal s1 s2
   | (AlwaysSquashed | SometimesSquashed _), _ -> false
 
 (* for now we do not allow reorderings *)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
@@ -265,10 +265,11 @@ let is_squashed sigma ((_,mip),u) =
       | SometimesSquashed squash ->
         (* impredicative set squashes are always AlwaysSquashed,
            so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *)
-        if List.for_all (fun q ->
+        if Sorts.Quality.Set.for_all (fun q ->
             let q = UVars.subst_instance_quality u q in
             let q = UState.nf_quality (Evd.evar_universe_context sigma) q in
-            quality_leq q indq) squash then None
+            quality_leq q indq) squash
+        then None
         else Some (SquashToQuality indq)
 
 let is_allowed_elimination sigma ((mib,_),_ as specifu) s =