module ConnecteurDonneesAppel
  [@java:package:fr.parcoursup.whyml.ordreappel.donnees]
  [@java:class_kind:interface]

  use int.Int
  use mach.java.lang.Integer
  use proofs.ordre_appel.specs.GroupeClassementValideProperties

  use fr.parcoursup.whyml.exceptions.acces_donnees_exception.AccesDonneesException
  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_entree.AlgoOrdreAppelEntree
  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_sortie.AlgoOrdreAppelSortie
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement.GroupeClassement
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide

  type t

  (* utilisés pour le calcul de l'ordre d'appel *)
  val recupererDonneesOrdreAppel (self [@W:unused_variable:N] : t) : AlgoOrdreAppelEntree.t
    raises { AccesDonneesException.E }

  (* récupère les données d'appel d'un gorupe unique *)
  val recupererDonneesOrdreAppelGroupe (self [@W:unused_variable:N] : t)
                                       (gTaCod [@W:unused_variable:N] : integer) : GroupeClassement.t
    raises { AccesDonneesException.E }

  (* export des données *)
  val exporterDonneesOrdresAppel (self [@W:unused_variable:N] : t)
                                 (donnees [@W:unused_variable:N] : AlgoOrdreAppelSortie.t) : unit
    requires { algo_ordre_appel_sortie_ok donnees }
    raises { AccesDonneesException.E }
end

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