<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

(* Universes are stratified by a partial ordering $\le$.
   Let $\~{}$ be the associated equivalence. We also have a strict ordering
   $<$ between equivalence classes, and we maintain that $<$ is acyclic,
   and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$.

   At every moment, we have a finite number of universes, and we
   maintain the ordering in the presence of assertions $U<V$ and $U\le V$.

   The equivalence $\~{}$ is represented by a tree structure, as in the
   union-find algorithm. The assertions $<$ and $\le$ are represented by
   adjacency lists *)

open Pp
open Util

(* An algebraic universe [universe] is either a universe variable
   [universe_level] or a formal universe known to be greater than some
   universe variables and strictly greater than some (other) universe
   variables

   Universes variables denote universes initially present in the term
   to type-check and non variable algebraic universes denote the
   universes inferred while type-checking: it is either the successor
   of a universe present in the initial term to type-check or the
   maximum of two algebraic universes
 *)

type universe_level =
    { u_mod : Names.dir_path;
      u_num : int }

type universe =
  | Variable of universe_level
  | Max of universe_level list * universe_level list
  
module UniverseOrdered = struct
  type t = universe_level
  let compare = Pervasives.compare
end

let string_of_univ_level u =
  Names.string_of_dirpath u.u_mod^"."^string_of_int u.u_num

let make_univ (m,n) = Variable { u_mod=m; u_num=n }

let pr_uni_level u = str (string_of_univ_level u)

let pr_uni = function
  | Variable u -> 
      pr_uni_level u
  | Max ([],[]) ->
      int 1
  | Max (gel,gtl) ->
      str "max(" ++ 
      prlist_with_sep pr_coma pr_uni_level gel ++
      (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
      prlist_with_sep pr_coma
	(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
      str ")"

(* Returns the formal universe that lies juste above the universe variable u.
   Used to type the sort u. *)
let super = function
  | Variable u -> 
      Max ([],[u])
  | Max _ ->
      anomaly ("Cannot take the successor of a non variable universes:\n"^
       "you are probably typing a type already known to be the type\n"^
       "of a user-provided term; if you really need this, please report")

(* Returns the formal universe that is greater than the universes u and v.
   Used to type the products. *)
let sup u v = 
  match u,v with<commit_msg>Simplification message d'anomalie<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

(* Universes are stratified by a partial ordering $\le$.
   Let $\~{}$ be the associated equivalence. We also have a strict ordering
   $<$ between equivalence classes, and we maintain that $<$ is acyclic,
   and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$.

   At every moment, we have a finite number of universes, and we
   maintain the ordering in the presence of assertions $U<V$ and $U\le V$.

   The equivalence $\~{}$ is represented by a tree structure, as in the
   union-find algorithm. The assertions $<$ and $\le$ are represented by
   adjacency lists *)

open Pp
open Util

(* An algebraic universe [universe] is either a universe variable
   [universe_level] or a formal universe known to be greater than some
   universe variables and strictly greater than some (other) universe
   variables

   Universes variables denote universes initially present in the term
   to type-check and non variable algebraic universes denote the
   universes inferred while type-checking: it is either the successor
   of a universe present in the initial term to type-check or the
   maximum of two algebraic universes
 *)

type universe_level =
    { u_mod : Names.dir_path;
      u_num : int }

type universe =
  | Variable of universe_level
  | Max of universe_level list * universe_level list
  
module UniverseOrdered = struct
  type t = universe_level
  let compare = Pervasives.compare
end

let string_of_univ_level u =
  Names.string_of_dirpath u.u_mod^"."^string_of_int u.u_num

let make_univ (m,n) = Variable { u_mod=m; u_num=n }

let pr_uni_level u = str (string_of_univ_level u)

let pr_uni = function
  | Variable u -> 
      pr_uni_level u
  | Max ([],[]) ->
      int 1
  | Max (gel,gtl) ->
      str "max(" ++ 
      prlist_with_sep pr_coma pr_uni_level gel ++
      (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
      prlist_with_sep pr_coma
	(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
      str ")"

(* Returns the formal universe that lies juste above the universe variable u.
   Used to type the sort u. *)
let super = function
  | Variable u -> 
      Max ([],[u])
  | Max _ ->
      anomaly ("Cannot take the successor of a non variable universes:\n"^
               "(maybe a bugged tactic)")

(* Returns the formal universe that is greater than the universes u and v.
   Used to type the products. *)
let sup u v = 
  match u,v with
{'fraction_non_alphanumeric': 0.1556510244547257, 'fraction_numerical': 0.0013218770654329147, 'mean_word_length': 3.2656800563777306, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2828126', 'n_tokens_mistral': 1789, 'n_tokens_neox': 1692, 'n_words': 710}