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

  use ref.Ref
  use int.Int
  use seq.Seq
  use seq.Permut
  use mach.java.lang.Long
  use mach.java.lang.Integer
  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.util.List as L
  use mach.java.util.UnmodifiableList as UL

  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use proofs.ordre_appel.specs.Invariants_Snoc
  use proofs.ordre_appel.invariants.iq0.IQ0_Lemmas
  use proofs.ordre_appel.specs.GroupeClassementValideProperties

  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException

  use proofs.ordre_appel.eligibles.Eligibles
  use proofs.ordre_appel.eligibles.ValidEligibles
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.PQueueVoeuxClasses as PQueue

  let function int_to_type_candidat [@java:visibility:private] (i : integer) : (r : type_candidat)
    requires { 1 <= i <= 4 }
    ensures { i = 1 -> r = BOURSIER_DU_SECTEUR }
    ensures { i = 2 -> r = BOURSIER_HORS_SECTEUR }
    ensures { i = 3 -> r = NON_BOURSIER_DU_SECTEUR }
    ensures { i = 4 -> r = NON_BOURSIER_HORS_SECTEUR }
  =
    if i = 1 then BOURSIER_DU_SECTEUR
    else if i = 2 then BOURSIER_HORS_SECTEUR
    else if i = 3 then NON_BOURSIER_DU_SECTEUR
    else begin
      assert { i = 4 };
      NON_BOURSIER_HORS_SECTEUR
    end

  let ghost function type_candidat_to_int (tc : type_candidat) : (i : integer)
    ensures { 1 <= i <= 4 }
    ensures { int_to_type_candidat i = tc }
  = match tc with
    | BOURSIER_DU_SECTEUR -> 1
    | BOURSIER_HORS_SECTEUR -> 2
    | NON_BOURSIER_DU_SECTEUR -> 3
    | NON_BOURSIER_HORS_SECTEUR -> 4
    end

  let calcul_eligibles [@java:visibility:private] (cB cR : bool) (files_attente : EnumMap.t) : PQueue.t
    requires { [@expl:pre/files_attente not empty] not enummap_is_empty files_attente }
    requires { [@expl:pre/alld(files_attente)] enummap_all_distincts files_attente }
    requires { [@expl:pre/constraints ->remains] eligibles_constraints_imp_remain cB cR files_attente }

    ensures { eligibles_contains_eligible_heads cB cR files_attente result }
    ensures { valid_eligibles cB cR files_attente result }
  =
    let eligibles = PQueue.create () in

    for i = 1 to 4 do
      invariant { forall k : integer. 1 <= k < i <= 5 ->
                         let t = int_to_type_candidat k in
                         let q = get_queue files_attente t in
                           q <> Seq.empty ->
                           let v = Seq.get q 0 in est_eligible_p cB cR v -> Fset.mem v eligibles }
      invariant { forall v. (Fset.mem v eligibles) -> (enummap_v_is_head files_attente v /\ est_eligible_p cB cR v)}
      let t = int_to_type_candidat i in
      if EnumMap.queue_is_empty files_attente t then
        assert { Seq.(==) (get_queue files_attente t) Seq.empty }
      else
        let voe = EnumMap.peek files_attente t in
        if ((est_boursier voe || not cB) && (est_du_secteur voe || not cR)) then
        begin
          assert { est_eligible_p cB cR voe };
          assert { enummap_v_is_head files_attente voe /\ est_eligible_p cB cR voe };
          PQueue.add eligibles voe;
        end;
    done;
    assert { forall v. (enummap_v_is_head files_attente v /\ est_eligible_p cB cR v)
              -> (Fset.mem v eligibles)  };
    eligibles_conditions cB cR files_attente;
    eligibles

  let selectionner_meilleur_voeu [@java:visibility:private] (cB cR : bool)
                                 (nb_b nb_ds : integer) (tx_b tx_ds : Taux.t)
                                 (grp : UL.ulist VoeuClasse.t)
                                 (oa : L.list VoeuClasse.t)
                                 (files_attente : EnumMap.t) : (meilleur : VoeuClasse.t)
    requires { [@expl:grp ok] seq_groupe_ok grp }
    requires { [@expl:grp sorted] seq_rangs_sorted grp }
    requires { [@expl:InvAlgo] invariants_algo nb_b nb_ds tx_b tx_ds grp oa files_attente }
    requires { [@expl:files_attente not empty] not enummap_is_empty files_attente }
    requires { [@expl:cB implies constraint on tx_b] cB -> taux_b_contraignant tx_b oa nb_b }
    requires { [@expl:constraint on tx_b implies cB] taux_b_contraignant tx_b oa nb_b -> cB }
    requires { [@expl:cR implies constraint on tx_ds] cR -> taux_ds_contraignant tx_ds oa nb_ds }
    requires { [@expl:constraint on tx_ds implies cR] taux_ds_contraignant tx_ds oa nb_ds -> cR }

    ensures {[@expl:InvAlgo(oak.res)] invariants_algo nb_b nb_ds tx_b tx_ds grp (snoc oa meilleur) files_attente }
  =
    let eligibles = calcul_eligibles cB cR files_attente in
    let meilleur =
      if not PQueue.is_empty eligibles then
        let r = PQueue.peek eligibles in begin
          assert { enummap_v_is_head files_attente r };
          assert { meilleur_eligible cB cR files_attente eligibles r };
          r
        end
      else begin
        assert { cB \/ cR };
        assert { (EnumMap.get_queue files_attente BOURSIER_DU_SECTEUR) == Seq.empty };
        assert { not EnumMap.queue_is_empty files_attente BOURSIER_HORS_SECTEUR };
        let r = EnumMap.peek files_attente BOURSIER_HORS_SECTEUR in
        assert { meilleur_eligible cB cR files_attente eligibles r };
        r
      end in
    assert { meilleur_eligible cB cR files_attente eligibles meilleur };
    let poll = EnumMap.pop files_attente (get_type_candidat meilleur) in
    assert { [@expl:meilleur is popped] poll = meilleur };
    meilleur

  let contrainte_taux [@java:visibility:private] (x_total x_appeles nb_appeles : integer) (taux_x : Taux.t) : bool
    requires { [@expl:#x appeles <= #appeles] 0 <= x_appeles <= nb_appeles }
    requires { [@expl:#X appeles <= #x total] 0 <= x_appeles <= x_total }
    ensures { result = (x_appeles < x_total && x_appeles * 100 < taux_x * (1 + nb_appeles)) }
  = let x_appeles_long = Long.of_integer x_appeles in
    let nb_appeles_long = Long.of_integer nb_appeles in
    let taux_x_long = Long.of_integer taux_x.tx in
    x_appeles < x_total && x_appeles_long * 100 < taux_x_long * (1 + nb_appeles_long)

 let calcul_ordre_appel [@java:visibility:private] (g : GroupeClassementValide.t) : (oa: L.list VoeuClasse.t)
    ensures { Properties.ordre_appel_properties
                (nb_boursiers g) (nb_du_secteur g)
                (get_taux_min_boursiers g) (get_taux_min_du_secteur g)
                (get_ordre_pedagogique g) oa
             }
    ensures { permut_all g oa }
  =
    let ordre_pedago = get_ordre_pedagogique g in
    let ordre_appel : L.list VoeuClasse.t = L.empty  () in
    let nb_voeux = GroupeClassementValide.get_nb_voeux_classes g in
    let tx_b = GroupeClassementValide.get_taux_min_boursiers g in
    let tx_r = GroupeClassementValide.get_taux_min_du_secteur g in
    let nb_appeles : ref integer = ref 0 in
    let nb_boursiers_appeles : ref integer = ref 0 in
    let nb_residents_appeles : ref integer = ref 0 in
    let files_attente : EnumMap.t = EnumMap.from_groupe ordre_pedago in
    let nb_boursiers_total : integer = EnumMap.get_nb_boursiers files_attente in
    let nb_residents_total : integer = EnumMap.get_nb_du_secteur files_attente in

    assert { nb_boursiers_total <= nb_voeux };
    assert { nb_residents_total <= nb_voeux };

    while L.size ordre_appel < nb_voeux do
      invariant { [@expl:InvAlgo] invariants_algo nb_boursiers_total nb_residents_total tx_b tx_r ordre_pedago ordre_appel files_attente }
      invariant { [@expl:#App] !nb_appeles = Seq.length ordre_appel }
      invariant { [@expl:#B App] !nb_boursiers_appeles = nb_boursiers ordre_appel }
      invariant { [@expl:#DS App] !nb_residents_appeles = nb_du_secteur ordre_appel }
      invariant { [@expl:#App bounds] !nb_appeles <= nb_voeux }
      invariant { [@expl:#B bounds] !nb_boursiers_appeles <= nb_boursiers_total && !nb_boursiers_appeles <= !nb_appeles }
      invariant { [@expl:#DS bounds] !nb_residents_appeles <= nb_residents_total && !nb_residents_appeles <= !nb_appeles }
      variant { nb_voeux - Seq.length ordre_appel }

      let contrainte_taux_boursier = contrainte_taux nb_boursiers_total !nb_boursiers_appeles !nb_appeles tx_b in
      let contrainte_taux_resident = contrainte_taux nb_residents_total !nb_residents_appeles !nb_appeles tx_r in
      let meilleur : VoeuClasse.t =
        selectionner_meilleur_voeu contrainte_taux_boursier contrainte_taux_resident
                                   nb_boursiers_total nb_residents_total
                                   tx_b tx_r
                                   ordre_pedago ordre_appel files_attente in
      assert { invariants_algo nb_boursiers_total nb_residents_total tx_b tx_r ordre_pedago
                               (snoc ordre_appel meilleur) files_attente };
      let _ = L.add ordre_appel meilleur in

      nb_appeles := !nb_appeles + 1;

      if est_boursier meilleur then
        nb_boursiers_appeles := !nb_boursiers_appeles + 1;

      if est_du_secteur meilleur then
        nb_residents_appeles := !nb_residents_appeles + 1;
    done;
    iq0_m_empty (UL.content ordre_pedago) (L.content ordre_appel) files_attente;
    ordre_appel

  let calculer_ordre_appel (grp : GroupeClassementValide.t) : (res : GroupeClassementValide.t)
    ensures { [@expl:res ok] groupe_ok res }
    ensures { [@expl:ra >= 1] seq_rangs_appel_ge_1 res }
    ensures { [@expl:ra uniques] seq_rangs_appel_uniques res }
    ensures { [@expl:grp = res (mod ra)] seq_voeu_permut_up_to_rang_appel grp res }
    ensures { [@expl:op(grp) = op(res) (mod ra)] seq_voeu_permut_up_to_rang_appel (get_ordre_pedagogique grp) (get_ordre_pedagogique res) }
    ensures { [@expl:specs res] ordre_appel_properties res }
    ensures { [@expl:c_gp_cod grp = res] c_gp_cod grp = c_gp_cod res }
    ensures { [@expl:|grp| = |res|] get_nb_voeux_classes grp = get_nb_voeux_classes res }
    ensures { [@expl:tx_b grp = res] get_taux_min_boursiers_pourcents grp = get_taux_min_boursiers_pourcents res }
    ensures { [@expl:tx_r grp = res] get_taux_min_du_secteur_pourcents grp = get_taux_min_du_secteur_pourcents res }
    ensures { ordre_appel_contiguous res }
  =
    try
      let tmp = calcul_ordre_appel grp in
      assert { seq_groupe_ok tmp };
      let nb_v = L.size tmp in
      let oa = L.empty () in
      for i = 0 to nb_v - 1 do
        invariant { i = L.size oa }
        invariant { forall k. 0 <= k < i -> oa[k].rang_appel = (k+1) >=1 }
        invariant { seq_field_ge_x_loc oa get_rang_appel 1 i }
        invariant { forall k l. 0 <= k < l < i -> oa[k].rang_appel < oa[l].rang_appel }
        invariant { forall k. 0 <= k < i -> eq_up_to_rang_appel tmp[k] oa[k] }
          let v = L.get tmp i in
          let nv = set_rang_appel v (i+1) in
          alld_snoc nv (L.content oa);
          label H in
          let _ = L.add oa nv in
          assert { oa[i].rang_appel = (i+1) /\ oa = snoc (oa at H) nv };
          assert { tmp[..i+1] = snoc tmp[..i] v /\ eq_up_to_rang_appel v nv /\ v = tmp[i] /\ nv = oa[i] };
      done;
      assert { seq_field_ge_x_loc oa get_rang_appel 1 nb_v };
      assert { [@expl:oa / ra >= 1] seq_rangs_appel_ge_1 oa };
      assert { [@expl:tmp = oa (mod ra)] seq_voeu_eq_up_to_rang_appel tmp oa };
      assert { forall k l. 0 <= k < l < nb_v -> oa[k].rang_appel < oa[l].rang_appel };
      assert { [@expl:oa / sorted] seq_rangs_appel_sorted_loc oa nb_v };
      assert { [@expl:oa / sorted] seq_rangs_appel_sorted oa };
      assert { [@expl:oa / ra uniques] seq_rangs_appel_uniques oa };
      assert { [@expl:oa / groupe ok oa] seq_groupe_ok oa };

      assert { [@expl:alld(oa)] all_distincts oa };
      let res = groupe_classement_valide_from_oa grp oa in
      assert { [@expl:op grp = op res (mod ra)]
               seq_voeu_eq_up_to_rang_appel (get_ordre_pedagogique grp) (get_ordre_pedagogique res) };
      oap_up_to_rang_appel_groupe grp (L.content oa) res;
      res
    with
      VerificationException.E _ -> absurd
      | IndexOutOfBoundsException.E _ -> absurd
    end;

end

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