(*
 https://framagit.org/parcoursup/algorithmes-de-parcoursup/-/tree/master/src/main/java/fr/parcoursup/algos/ordreappel/algo/GroupeClassement.java
 *)
module GroupeClassementClone
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]

  use int.Int
  use seq.Seq
  use seq.Distinct
  use mach.java.lang.Integer
  use mach.java.util.Set
  use mach.java.util.List
  use proofs.lib.seq.Seq
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.exceptions.invalid_argument_exception.InvalidArgumentException
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  type t

  val ghost function seq_voeux_classes[@java:ignore] (_ : t) : Seq.seq VoeuClasse.t

  meta coercion function seq_voeux_classes

  val function get_c_gp_cod (self : t) : integer

  val function get_nb_voeux_classes (self : t) : integer
    ensures { result = Integer.enforced_integer (Seq.length self) }

  val get_ith_voeu_classe_safe [@java:visibility:package] (self : t) (i : integer) : VoeuClasse.t
    requires { 0 <= i < get_nb_voeux_classes self }
    ensures { result = self[i] }

  let get_ith_voeu_classe (self : t) (i : integer) : VoeuClasse.t
    ensures { result = self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_voeux_classes self)}
  =
    if (not (0 <= i && i < get_nb_voeux_classes self) ) then
      raise InvalidArgumentException.E (index_out_of_bounds i);
    get_ith_voeu_classe_safe self i

  let get_ith_rang_safe [@java:visibility:package] (self : t) (i : integer) : integer
    requires { 0 <= i < get_nb_voeux_classes self }
    ensures { result = get_rang self[i] }
  =
    VoeuClasse.get_rang (get_ith_voeu_classe_safe self i)

  let get_ith_rang (self : t) (i : integer) : integer
    ensures { result = get_rang self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_voeux_classes self) }
  =
    VoeuClasse.get_rang (get_ith_voeu_classe self i)

  let get_ith_rang_appel_safe [@java:visibility:package] (self : t) (i : integer) : integer
    requires { 0 <= i < get_nb_voeux_classes self }
    ensures { result = get_rang_appel self[i] }
  =
    VoeuClasse.get_rang_appel (get_ith_voeu_classe_safe self i)

  let get_ith_rang_appel (self : t) (i : integer) : integer
    ensures { result = get_rang_appel self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_voeux_classes self) }
  =
    VoeuClasse.get_rang_appel (get_ith_voeu_classe self i)

  let get_ith_g_cn_cod_safe [@java:visibility:package] (self : t) (i : integer) : integer
    requires { 0 <= i < get_nb_voeux_classes self }
    ensures { result = get_g_cn_cod self[i] }
  =
    VoeuClasse.get_g_cn_cod (get_ith_voeu_classe_safe self i)

  let get_ith_g_cn_cod (self : t) (i : integer) : integer
    ensures { result = get_g_cn_cod self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_voeux_classes self) }
  =
    VoeuClasse.get_g_cn_cod (get_ith_voeu_classe self i)

  val function get_taux_min_boursiers_pourcents (self : t) : integer

  val function get_taux_min_du_secteur_pourcents (self : t) : integer

  predicate field_in_set (self : t) (s : set integer) (get_r : VoeuClasse.t -> integer) (i : int) =
    forall k. 0 <= k < i -> Set.contains s (get_r self[k])

  predicate set_in_field (self : t) (s : set integer) (get_r : VoeuClasse.t -> integer) (i : int) =
    forall r : integer. Set.contains s r ->
      (exists k. 0 <= k < i && r = get_r self[k])

  predicate groupe_ok (self : t) =
       0 <= get_taux_min_boursiers_pourcents self <= 100
    /\ 0 <= get_taux_min_du_secteur_pourcents self <= 100
    /\ seq_groupe_ok self
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)