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

  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use mach.java.util.List
  use mach.java.util.UnmodifiableList
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use proofs.ordre_appel.rv_specs.RuntimeVerificationSpec_Lemmas as RVSpec
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_entree.AlgoOrdreAppelEntree as AOAE
  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_sortie.AlgoOrdreAppelSortie as AOAS
  use fr.parcoursup.whyml.ordreappel.algo.calcul_ordre_appel_groupe.CalculOrdreAppelGroupe
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.verification.verifications_resultats_algo_ordre_appel.VerificationsResultatsAlgoOrdreAppel

  let calculerOrdresAppels (entree : AOAE.t) : (r : AOAS.t)
    ensures { AOAS.algo_ordre_appel_entree_sortie_ok entree r }
    ensures { AOAS.algo_ordre_appel_sortie_ok r }
  =
    try
      let resultat = AOAS.algo_ordre_appel_sortie () in
      let len = AOAE.get_nb_groupes entree in
      for i = 0 to len - 1 do
          invariant { AOAS.get_nb_groupes resultat = i }
          invariant { forall k. 0 <= k < i -> get_c_gp_cod resultat[k] = get_c_gp_cod entree[k] }
          invariant { forall k. 0 <= k < i -> 0 <= k < i -> ordre_appel_properties resultat[k] }
          invariant { forall k. 0 <= k < i -> RVSpec.grp_eq_up_to_rang_appel entree[k] resultat[k]  }
          invariant { forall k. 0 <= k < i -> RVSpec.group_satisfies_specs resultat[k]  }
        let grp = AOAE.get_ith_groupe_safe entree i  in
        let oa = CalculOrdreAppelGroupe.calculer_ordre_appel grp in
        assert { get_c_gp_cod grp = get_c_gp_cod oa };
        AOAS.add_groupe_valide resultat oa;
        RVSpec.spec_imply_rv (AOAS.get_ith_groupe_safe resultat i);
      done;

      assert { RVSpec.donnees_entree_eq_sortie entree resultat };
      assert { RVSpec.groups_satisfy_specs resultat };
      VerificationsResultatsAlgoOrdreAppel.verifier entree resultat;
      resultat
    with
      | VerificationException.E _ -> absurd
    end;
end

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