module GroupeClassementValide
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]

  use int.Int
  use seq.Seq
  use seq.FreeMonoid
  use ref.Refint
  use mach.java.lang.Integer
  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.util.UnmodifiableList as UL
  use mach.java.util.List as L
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.candidat_classe.CandidatClasse as CC
  use fr.parcoursup.whyml.ordreappel.algo.ordre_appel.OrdreAppel as OA
  use fr.parcoursup.whyml.ordreappel.algo.list_voeu_classe_rang.ListVoeuClasseRang
  use fr.parcoursup.whyml.ordreappel.algo.list_voeu_classe_appel.ListVoeuClasseAppel
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement.GroupeClassement as GC
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  type t [@java:visibility:package] = {
    c_gp_cod : integer;
    taux_min_boursiers_pourcents : Taux.t;
    taux_min_du_secteur_pourcents : Taux.t;
    voeux_classes : UL.ulist VoeuClasse.t;
  } invariant {
    seq_groupe_ok voeux_classes
  } by {
    c_gp_cod = 0;
    taux_min_boursiers_pourcents = Taux.taux_zero ();
    taux_min_du_secteur_pourcents = Taux.taux_zero ();
    voeux_classes = UL.empty ()
  }

  let ghost function seq_voeux_classes[@java:ignore] (self : t) : (s : Seq.seq VoeuClasse.t)
    ensures { s = self.voeux_classes  }
  =
    UL.content self.voeux_classes

  meta coercion function seq_voeux_classes

  let function get_c_gp_cod (self : t) : integer
  =
    self.c_gp_cod

  let function get_nb_voeux_classes (self : t) : integer
  =
    UL.size self.voeux_classes

  let 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] }
  =
    try
      UL.get self.voeux_classes i
    with
      IndexOutOfBoundsException.E _ -> absurd
    end

  let function get_taux_min_boursiers_pourcents (self :t) : integer
    ensures { 0 <= result <= 100 }
  =
    self.taux_min_boursiers_pourcents.tx

  let function get_taux_min_du_secteur_pourcents (self :t) : integer
    ensures { 0 <= result <= 100 }
  =
    self.taux_min_du_secteur_pourcents.tx

  let function get_taux_min_boursiers (self :t) : Taux.t
    ensures { 0 <= result <= 100 }
  =
    self.taux_min_boursiers_pourcents

  let function get_taux_min_du_secteur (self :t) : Taux.t
  =
    self.taux_min_du_secteur_pourcents

  clone export fr.parcoursup.whyml.ordreappel.algo.groupe_classement_clone.GroupeClassementClone with type t = t,
    val get_c_gp_cod = get_c_gp_cod,
    val get_nb_voeux_classes = get_nb_voeux_classes,
    val get_ith_voeu_classe_safe = get_ith_voeu_classe_safe,
    val get_taux_min_boursiers_pourcents = get_taux_min_boursiers_pourcents,
    val get_taux_min_du_secteur_pourcents = get_taux_min_du_secteur_pourcents,
    val seq_voeux_classes = seq_voeux_classes

  predicate gcv_eq_gc (gcv : t) (gc : GC.t) =
      (get_c_gp_cod gcv = GC.get_c_gp_cod gc) &&
      (get_nb_voeux_classes gcv = GC.get_nb_voeux_classes gc) &&
      (get_taux_min_boursiers_pourcents gcv = GC.get_taux_min_boursiers_pourcents gc) &&
      (get_taux_min_du_secteur_pourcents gcv = GC.get_taux_min_du_secteur_pourcents gc) &&
      (seq_voeux_classes gcv == GC.seq_voeux_classes gc)

  let groupe_classement_valide [@java:constructor] (grp : GC.t) : t
    ensures { gcv_eq_gc result grp }
    ensures { groupe_ok result }
    raises { VerificationException.E _ -> not (GC.groupe_ok grp) }
  =
    GC.verifier_groupe_ok grp;
    let res = {
      c_gp_cod = GC.get_c_gp_cod grp;
      taux_min_boursiers_pourcents = taux (GC.get_taux_min_boursiers_pourcents grp);
      taux_min_du_secteur_pourcents = taux (GC.get_taux_min_du_secteur_pourcents grp);
      voeux_classes = List.copy_of (GC.voeux_classes grp);
    } in
    res

  let groupe_classement_valide_from_oa [@java:constructor] [@java:visibility:package] (grp : t) (oa: L.list VoeuClasse.t) : (res : t)
    requires { seq_groupe_ok oa }
    ensures { get_c_gp_cod res = get_c_gp_cod grp }
    ensures { get_taux_min_boursiers res = get_taux_min_boursiers grp }
    ensures { get_taux_min_du_secteur res = get_taux_min_du_secteur grp }
    ensures { get_nb_voeux_classes res = L.size oa }
    ensures { oa == res }
  =
    let res = {
      c_gp_cod = get_c_gp_cod grp;
      taux_min_boursiers_pourcents = get_taux_min_boursiers grp;
      taux_min_du_secteur_pourcents = get_taux_min_du_secteur grp;
      voeux_classes = L.copy_of oa;
    } in
    res

  predicate oa_eq_oa_list (oa : OA.t) (oal : UL.ulist VoeuClasse.t) =
     UL.size oal = OA.get_nb_candidats oa /\
     forall i. 0 <= i < UL.size oal -> CC.est_voeu_classe oa[i] oal[i]

  let lemma goa (self : t) (oa : OA.t) (oal : UL.ulist VoeuClasse.t) (i : int) : (res : int)
    requires { oa_eq_oa_list oa oal }
    requires { get_nb_voeux_classes self = UL.size oal = OA.get_nb_candidats oa }
    requires { 0 <= i < get_nb_voeux_classes self }
    requires { exists j. 0 <= j < UL.size oal /\ self[i] = oal[j] }
    ensures { 0 <= res < OA.get_nb_candidats oa }
    ensures { CC.est_voeu_classe oa[res] self[i] }
  =
    let j = any (r: int) ensures { 0 <= r < UL.size oal /\ self[i] = oal[r] } in
    j

  use seq.Permut

  let function get_ordre_appel_list (self : t) : (oa : UL.ulist VoeuClasse.t)
    ensures { permut_all self oa}
    ensures { get_nb_voeux_classes self = UL.size oa }
    ensures { seq_g_cn_cod_ge_0 oa }
    ensures { seq_g_cn_cod_uniques oa }
    ensures { seq_rangs_appel_ge_1 oa }
    ensures { seq_rangs_appel_sorted oa }
  =
    if ListVoeuClasseAppel.is_sorted self.voeux_classes then
      return self.voeux_classes;

    let nb_voeux = get_nb_voeux_classes self in
    assert { forall i j. 0 <= i < nb_voeux -> 0 <= j < nb_voeux -> i <> j -> get_g_cn_cod self[i] <> get_g_cn_cod self[j] };
    let res : L.list VoeuClasse.t = L.empty () in
    for i = 0 to get_nb_voeux_classes self - 1 do
      invariant { L.size res = i }
      invariant { forall j. 0 <= j < i -> res[j] = self[j] }
      invariant { seq_field_uniques_loc res get_g_cn_cod i }
      let _ = L.add res (get_ith_voeu_classe_safe self i) in ()
    done;
    assert { self == res };
    ListVoeuClasseAppel.sort_list res

  let function get_ordre_appel (self : t) : (res : OA.t)
    ensures { get_nb_voeux_classes self = OA.get_nb_candidats res }
    ensures { oa_eq_oa_list res (get_ordre_appel_list self) }
    ensures { forall i. 0 <= i < get_nb_voeux_classes self ->
                exists j. 0 <= j < OA.get_nb_candidats res /\ CC.est_voeu_classe res[j] self[i] }
    ensures { forall i. 0 <= i < OA.get_nb_candidats res ->
                exists j. 0 <= j < get_nb_voeux_classes self /\ CC.est_voeu_classe res[i] self[j] }
    ensures { forall i. 0 <= i < get_nb_voeux_classes self ->
                exists j. 0 <= j < OA.get_nb_candidats res /\
                  CC.get_rang_appel res[j] = get_rang_appel self[i] /\ CC.get_g_cn_cod res[j] = get_g_cn_cod self[i] }
    ensures { forall i. 0 <= i < OA.get_nb_candidats res ->
                exists j. 0 <= j < get_nb_voeux_classes self /\
                  CC.get_rang_appel res[i] = get_rang_appel self[j] /\ CC.get_g_cn_cod res[i] = get_g_cn_cod self[j] }
  =
    OA.ordre_appel (get_ordre_appel_list self)

  let function get_ordre_pedagogique (self : t) : (op: UL.ulist VoeuClasse.t)
      ensures { seq_groupe_ok op}
      ensures { seq_rangs_sorted op }
      ensures { permut_all self op }
      ensures { nb_boursiers self = nb_boursiers op }
      ensures { nb_du_secteur self = nb_du_secteur op }
  =
    ListVoeuClasseRang.sort_ulist self.voeux_classes

end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)