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

  use int.Int
  use mach.java.lang.Integer
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  type type_candidat =
      BOURSIER_DU_SECTEUR
    | BOURSIER_HORS_SECTEUR
    | NON_BOURSIER_DU_SECTEUR
    | NON_BOURSIER_HORS_SECTEUR

  predicate type_candidat_eq (t1 : type_candidat) (t2 : type_candidat) =
    match t1, t2 with
      | BOURSIER_DU_SECTEUR, BOURSIER_DU_SECTEUR
      | BOURSIER_HORS_SECTEUR, BOURSIER_HORS_SECTEUR
      | NON_BOURSIER_DU_SECTEUR, NON_BOURSIER_DU_SECTEUR
      | NON_BOURSIER_HORS_SECTEUR, NON_BOURSIER_HORS_SECTEUR -> true
      | _ -> false
    end

  predicate type_est_boursier (t : type_candidat) =
    match t with
      | BOURSIER_DU_SECTEUR | BOURSIER_HORS_SECTEUR -> true
      | _ -> false
    end

  predicate type_est_du_secteur (t : type_candidat) =
    match t with
      | BOURSIER_DU_SECTEUR | NON_BOURSIER_DU_SECTEUR -> true
      | _ -> false
    end

  type t [@java:visibility:private] = {
    type_candidat : type_candidat;
    g_cn_cod : integer;
    rang : integer;
    rang_appel : integer;
  } invariant {
    rang >= 0
  } invariant {
    rang_appel >= 0
  } by {
    type_candidat = BOURSIER_DU_SECTEUR; g_cn_cod = 0; rang = 0; rang_appel = 0;
  }

  let function get_rang_appel (self : t) : integer = self.rang_appel

  let function get_g_cn_cod (self : t) : integer = self.g_cn_cod

  let function get_rang (self : t) : integer = self.rang

  let function get_type_candidat (self : t) : type_candidat = self.type_candidat

  let function est_boursier (self : t) : bool =
    match self.type_candidat with
    | BOURSIER_DU_SECTEUR | BOURSIER_HORS_SECTEUR -> true
    | _ -> false
    end

  let function est_du_secteur (self : t) : bool =
    match self.type_candidat with
    | BOURSIER_DU_SECTEUR | NON_BOURSIER_DU_SECTEUR -> true
    | _ -> false
    end

  let function compare_to (self : t) (o : t) : integer = self.rang - o.rang

  let voeu_classe [@java:constructor] (cod : integer) (rang : integer)
                                      (boursier : bool) (du_secteur : bool): t
    ensures { get_rang result = rang >= 0 }
    ensures { boursier = est_boursier result }
    ensures { du_secteur = est_du_secteur result }
    ensures { cod = get_g_cn_cod result }
    ensures { get_rang_appel result = get_rang result }
    raises { VerificationException.E _ -> rang < 0 }
  =
    if rang < 0 then
      raise VerificationException.E (VerificationException.crtX2 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_RANG_NEGATIF cod rang);
    let type_candidat =
      if boursier then
        if du_secteur then BOURSIER_DU_SECTEUR else BOURSIER_HORS_SECTEUR
      else
        if du_secteur then NON_BOURSIER_DU_SECTEUR else NON_BOURSIER_HORS_SECTEUR
    in
      { type_candidat = type_candidat; g_cn_cod = cod; rang = rang; rang_appel = rang; }

  let function has_type (self : t) (ty : type_candidat) : bool
    ensures { result <-> type_candidat_eq (get_type_candidat self) ty }
  = match ty with
    | BOURSIER_DU_SECTEUR -> est_boursier self && est_du_secteur self
    | BOURSIER_HORS_SECTEUR -> est_boursier self && (not est_du_secteur self)
    | NON_BOURSIER_DU_SECTEUR -> (not est_boursier self) && est_du_secteur self
    | NON_BOURSIER_HORS_SECTEUR -> (not est_boursier self) && (not est_du_secteur self)
    end

  let function types_identiques (v1 : t) (v2 : t) : bool
    ensures { result <-> type_candidat_eq (get_type_candidat v1) (get_type_candidat v2) }
  =
    has_type v1 (get_type_candidat v2)

  let function eq_up_to_rang_appel (v1 : t) (v2 : t) : bool
    ensures { result <-> (
              get_g_cn_cod v1 = get_g_cn_cod v2 && get_rang v1 = get_rang v2
              && types_identiques v1 v2)
               }
  = (get_g_cn_cod v1 = get_g_cn_cod v2) &&
    (get_rang v1 = get_rang v2) &&
    types_identiques v1 v2

  let set_rang_appel [@java:constructor] (vc : t) (ra : integer) : t
    ensures { get_rang result = get_rang vc }
    ensures { est_boursier result = est_boursier vc }
    ensures { est_du_secteur result = est_du_secteur vc }
    ensures { get_g_cn_cod result = get_g_cn_cod vc }
    ensures { get_rang_appel result = ra }
    ensures { eq_up_to_rang_appel vc result }
    raises { VerificationException.E _ -> ra < 0 }
  =
    if ra < 0 then
      raise VerificationException.E (crtX2 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_RANG_APPEL_NEGATIF vc.g_cn_cod ra);
    { type_candidat = vc.type_candidat; g_cn_cod = vc.g_cn_cod; rang = vc.rang; rang_appel = ra; }
end

module VoeuClasse_Props
  use int.Int
  use mach.java.lang.Integer
  use VoeuClasse

  predicate voeux_classes_eq_up_to_rang_appel (v1 : VoeuClasse.t) (v2 : VoeuClasse.t) =
    (get_g_cn_cod v1 = get_g_cn_cod v2) /\
    (get_rang v1 = get_rang v2) /\
    type_candidat_eq (get_type_candidat v1)  (get_type_candidat v2)

  predicate voeu_lt (v1 v2 : VoeuClasse.t) =
    compare_to v1 v2 < 0

  predicate voeu_le (v1 v2 : VoeuClasse.t) =
    compare_to v1 v2 <= 0

  predicate voeu_distinct (v1 v2 : VoeuClasse.t) =
    voeu_lt v1 v2 \/ voeu_lt v2 v1

  predicate voeu_has_type (v : t) (t : type_candidat) =
    has_type v t

  predicate voeu_eq (v1 v2 : VoeuClasse.t) = v1 = v2

  function same_type (v1 v2 : VoeuClasse.t) : bool =
      get_type_candidat v1 = get_type_candidat v2

  let lemma eq_up_to_rang_appel_if_eq (v1 v2 : VoeuClasse.t)
    requires { v1 = v2 }
    ensures { eq_up_to_rang_appel v1 v2 }
  =
    ()

  let lemma eq_up_to_rang_appel_symm (v1 v2 : VoeuClasse.t)
    requires { eq_up_to_rang_appel v1 v2 }
    ensures { eq_up_to_rang_appel v2 v1 }
  =
    ()

  let lemma eq_up_to_rang_appel_trans (v1 v2 v3 : VoeuClasse.t)
    requires { eq_up_to_rang_appel v1 v2 }
    requires { eq_up_to_rang_appel v2 v3 }
    ensures { eq_up_to_rang_appel v1 v3 }
  =
    ()
end

module PQueueVoeuxClasses
  use VoeuClasse

  clone export mach.java.util.PriorityQueue with
    type elt = VoeuClasse.t,
    function cmp = VoeuClasse.compare_to
end

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