Last active
May 29, 2021 12:14
-
-
Save denismerigoux/21de6dca3566ff0dea1aad89da1a4d61 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| type Enfant = { | |
| identifiant: integer | |
| obligation_scolaire: SituationObligationScolaire | |
| rémuneration_mensuelle: money | |
| date_de_naissance: date | |
| âge: integer | |
| prise_en_charge: PriseEnCharge | |
| a_déjà_ouvert_droit_aux_allocations_familiales: bool | |
| } | |
| type EnfantEntrée = { | |
| d_identifiant: integer | |
| d_rémuneration_mensuelle: money | |
| d_date_de_naissance: date | |
| d_prise_en_charge: PriseEnCharge | |
| d_a_déjà_ouvert_droit_aux_allocations_familiales: bool | |
| } | |
| type PriseEnCharge = | |
| | GardeAlternéePartageAllocations: unit | |
| | GardeAlternéeAllocataireUnique: unit | |
| | EffectiveEtPermanente: unit | |
| | ServicesSociauxAllocationVerséeÀLaFamille: unit | |
| | ServicesSociauxAllocationVerséeAuxServicesSociaux: unit | |
| type SituationObligationScolaire = | |
| | Avant: unit | |
| | Pendant: unit | |
| | Après: unit | |
| type Collectivité = | |
| | Guadeloupe: unit | |
| | Guyane: unit | |
| | Martinique: unit | |
| | LaRéunion: unit | |
| | SaintBarthélemy: unit | |
| | SaintMartin: unit | |
| | Métropole: unit | |
| | SaintPierreEtMiquelon: unit | |
| | Mayotte: unit | |
| type PriseEnCompte = | |
| | Complète: unit | |
| | Partagée: unit | |
| | Zéro: unit | |
| type VersementAllocations = | |
| | Normal: unit | |
| | AllocationVerséeAuxServicesSociaux: unit | |
| type ÉlémentPrestationsFamiliales = | |
| | PrestationAccueilJeuneEnfant: unit | |
| | AllocationsFamiliales: unit | |
| | ComplémentFamilial: unit | |
| | AllocationLogement: unit | |
| | AllocationÉducationEnfantHandicapé: unit | |
| | AllocationSoutienFamilial: unit | |
| | AllocationRentréeScolaire: unit | |
| | AllocationJournalièrePresenceParentale: unit | |
| let scope Smic (date_courante: date) (résidence: Collectivité) | |
| (brut_horaire: money) = | |
| let date_courante : date = reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let résidence : Collectivité = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let brut_horaire : money = | |
| reentrant or by default | |
| ⟨⟨date_courante >=@ 2021-01-01 && | |
| date_courante <=@ 2021-12-31 && résidence = Mayotte () ⊢ 7.74 €⟩, | |
| ⟨date_courante >=@ 2021-01-01 && | |
| date_courante <=@ 2021-12-31 && | |
| résidence = Métropole () || | |
| résidence = Guadeloupe () || | |
| résidence = Guyane () || | |
| résidence = Martinique () || | |
| résidence = LaRéunion () || | |
| résidence = SaintBarthélemy () || | |
| résidence = SaintMartin () || | |
| résidence = SaintPierreEtMiquelon () ⊢ 10.25 €⟩, | |
| ⟨date_courante >=@ 2020-01-01 && | |
| date_courante <=@ 2020-12-31 && résidence = Mayotte () ⊢ 7.66 €⟩, | |
| ⟨date_courante >=@ 2020-01-01 && | |
| date_courante <=@ 2020-12-31 && | |
| résidence = Métropole () || | |
| résidence = Guadeloupe () || | |
| résidence = Guyane () || | |
| résidence = Martinique () || | |
| résidence = LaRéunion () || | |
| résidence = SaintBarthélemy () || | |
| résidence = SaintMartin () || | |
| résidence = SaintPierreEtMiquelon () ⊢ 10.15 €⟩, | |
| ⟨date_courante >=@ 2019-01-01 && | |
| date_courante <=@ 2019-12-31 && résidence = Mayotte () ⊢ 7.57 €⟩, | |
| ⟨date_courante >=@ 2019-01-01 && | |
| date_courante <=@ 2019-12-31 && | |
| résidence = Métropole () || | |
| résidence = Guadeloupe () || | |
| résidence = Guyane () || | |
| résidence = Martinique () || | |
| résidence = LaRéunion () || | |
| résidence = SaintBarthélemy () || | |
| résidence = SaintMartin () || | |
| résidence = SaintPierreEtMiquelon () ⊢ 10.03 €⟩ | | |
| false ⊢ ∅ ⟩ in | |
| end scope | |
| let scope PrestationsFamiliales (droit_ouvert: Enfant → bool) | |
| (conditions_hors_âge: Enfant → bool) (plafond_l512_3_2: money) | |
| (âge_l512_3_2: integer) (régime_outre_mer_l751_1: bool) | |
| (date_courante: date) (prestation_courante: ÉlémentPrestationsFamiliales) | |
| (résidence: Collectivité) (base_mensuelle: money) = | |
| let âge_l512_3_2 : integer = | |
| reentrant or by default ⟨⟨true ⊢ 20⟩ | false ⊢ ∅ ⟩ in; | |
| let date_courante : date = reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let prestation_courante : ÉlémentPrestationsFamiliales = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let résidence : Collectivité = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let base_mensuelle : money = | |
| reentrant or by default | |
| ⟨⟨date_courante >=@ 2021-04-01 && date_courante <@ 2022-04-01 ⊢ 414.81 €⟩, | |
| ⟨date_courante >=@ 2020-04-01 && date_courante <@ 2021-04-01 ⊢ 414.04 €⟩, | |
| ⟨date_courante >=@ 2019-04-01 && date_courante <@ 2020-04-01 ⊢ 413.16 €⟩ | |
| | false ⊢ ∅ ⟩ in; | |
| let smic.date_courante : date = | |
| ⟨⟨true ⊢ date_courante⟩ | false ⊢ ∅ ⟩ in; | |
| let smic.résidence : Collectivité = | |
| ⟨⟨true ⊢ résidence⟩ | false ⊢ ∅ ⟩ in; | |
| call Smic[smic]; | |
| let régime_outre_mer_l751_1 : bool = | |
| reentrant or by default | |
| ⟨⟨résidence = Guadeloupe () || | |
| résidence = Guyane () || | |
| résidence = Martinique () || | |
| résidence = LaRéunion () || | |
| résidence = SaintBarthélemy () || résidence = SaintMartin () ⊢ true⟩ | |
| | true ⊢ false⟩ in; | |
| let plafond_l512_3_2 : money = | |
| reentrant or by default | |
| ⟨⟨⟨régime_outre_mer_l751_1 ⊢ smic.brut_horaire *$ 0.55 *$ 169.⟩ | |
| | true ⊢ smic.brut_horaire *$ 0.55 *$ 169.⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let conditions_hors_âge : Enfant → bool = | |
| reentrant or by default | |
| λ (param_228: Enfant) → error_empty | |
| ⟨⟨match param_228.obligation_scolaire with | |
| Avant → λ (__229: unit) → true | | |
| Pendant → λ (__230: unit) → false | | |
| Après → λ (__231: unit) → false | |
| || | |
| match param_228.obligation_scolaire with | |
| Avant → λ (__232: unit) → false | | |
| Pendant → λ (__233: unit) → true | | |
| Après → λ (__234: unit) → false | |
| || | |
| match param_228.obligation_scolaire with | |
| Avant → λ (__235: unit) → false | | |
| Pendant → λ (__236: unit) → false | | |
| Après → λ (__237: unit) → true | |
| && param_228.rémuneration_mensuelle <=$ plafond_l512_3_2 ⊢ true⟩ | |
| | true ⊢ false⟩ in; | |
| let droit_ouvert : Enfant → bool = | |
| reentrant or by default | |
| λ (param_238: Enfant) → error_empty | |
| ⟨⟨match param_238.obligation_scolaire with | |
| Avant → λ (__239: unit) → false | | |
| Pendant → λ (__240: unit) → false | | |
| Après → λ (__241: unit) → true | |
| && | |
| param_238.rémuneration_mensuelle <=$ plafond_l512_3_2 && | |
| param_238.âge < âge_l512_3_2 ⊢ true⟩, | |
| ⟨match param_238.obligation_scolaire with | |
| Avant → λ (__242: unit) → true | | |
| Pendant → λ (__243: unit) → false | | |
| Après → λ (__244: unit) → false | |
| || | |
| match param_238.obligation_scolaire with | |
| Avant → λ (__245: unit) → false | | |
| Pendant → λ (__246: unit) → true | | |
| Après → λ (__247: unit) → false ⊢ true⟩ | | |
| true ⊢ false⟩ in | |
| end scope | |
| let scope AllocationFamilialesAvril2008 | |
| (âge_minimum_alinéa_1_l521_3: integer) = | |
| let âge_minimum_alinéa_1_l521_3 : integer = | |
| reentrant or by default ⟨⟨true ⊢ 16⟩ | false ⊢ ∅ ⟩ in | |
| end scope | |
| let scope EnfantLePlusÂgé (enfants: Enfant array) (le_plus_âgé: Enfant) = | |
| let enfants : Enfant array = reentrant or by default ⟨false ⊢ ∅ ⟩ | |
| in; | |
| let le_plus_âgé : Enfant = | |
| reentrant or by default | |
| ⟨⟨true ⊢ let predicate_248 : any = | |
| λ (potentiel_plus_âgé_249: any) → | |
| potentiel_plus_âgé_249.âge | |
| in | |
| fold | |
| (λ (acc_250: any) (item_251: any) → if | |
| predicate_248 acc_250 > predicate_248 item_251 then | |
| acc_250 else item_251) | |
| Enfant { identifiant = - 1; | |
| obligation_scolaire = Pendant (); | |
| rémuneration_mensuelle = 0.00 €; | |
| date_de_naissance = 1900-01-01; âge = 0; | |
| prise_en_charge = EffectiveEtPermanente (); | |
| a_déjà_ouvert_droit_aux_allocations_familiales = false | |
| } | |
| enfants⟩ | false ⊢ ∅ ⟩ in | |
| end scope | |
| let scope AllocationsFamiliales | |
| (personne_charge_effective_permanente_est_parent: bool) | |
| (personne_charge_effective_permanente_remplit_titre_I: bool) | |
| (ressources_ménage: money) (résidence: Collectivité) | |
| (date_courante: date) (enfants_à_charge: Enfant array) | |
| (enfants_à_charge_droit_ouvert_prestation_familiale: Enfant array) | |
| (prise_en_compte: Enfant → PriseEnCompte) | |
| (versement: Enfant → VersementAllocations) (montant_versé: money) | |
| (droit_ouvert_base: bool) (montant_initial_base: money) | |
| (montant_initial_base_premier_enfant: money) | |
| (montant_initial_base_deuxième_enfant: money) | |
| (montant_initial_base_troisième_enfant_et_plus: money) | |
| (rapport_enfants_total_moyen: decimal) (nombre_moyen_enfants: decimal) | |
| (nombre_total_enfants: decimal) (montant_avec_garde_alternée_base: money) | |
| (montant_versé_base: money) (droit_ouvert_forfaitaire: Enfant → bool) | |
| (montant_versé_forfaitaire_par_enfant: money) | |
| (montant_versé_forfaitaire: money) | |
| (droit_ouvert_majoration: Enfant → bool) | |
| (montant_initial_métropole_majoration: Enfant → money) | |
| (montant_initial_majoration: Enfant → money) | |
| (montant_avec_garde_alternée_majoration: Enfant → money) | |
| (montant_versé_majoration: money) (droit_ouvert_complément: bool) | |
| (montant_base_complément_pour_base_et_majoration: money) | |
| (complément_dégressif: money → money) | |
| (montant_versé_complément_pour_base_et_majoration: money) | |
| (montant_versé_complément_pour_forfaitaire: money) | |
| (nombre_enfants_l521_1: integer) | |
| (âge_minimum_alinéa_1_l521_3: Enfant → integer) | |
| (nombre_enfants_alinéa_2_l521_3: integer) | |
| (est_enfant_le_plus_âgé: Enfant → bool) (plafond_I_d521_3: money) | |
| (plafond_II_d521_3: money) = | |
| let personne_charge_effective_permanente_est_parent : bool = | |
| reentrant or by default ⟨true ⊢ false⟩ in; | |
| let personne_charge_effective_permanente_remplit_titre_I : bool = | |
| reentrant or by default ⟨true ⊢ false⟩ in; | |
| let ressources_ménage : money = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let résidence : Collectivité = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let date_courante : date = reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let enfants_à_charge : Enfant array = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let prise_en_compte : Enfant → PriseEnCompte = | |
| reentrant or by default | |
| λ (param_252: Enfant) → error_empty | |
| ⟨⟨match param_252.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__253: unit) → false | | |
| GardeAlternéeAllocataireUnique → | |
| λ (__254: unit) → false | | |
| EffectiveEtPermanente → λ (__255: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__256: unit) → true | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__257: unit) → false ⊢ Complète | |
| ()⟩, | |
| ⟨match param_252.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__258: unit) → false | | |
| GardeAlternéeAllocataireUnique → λ (__259: unit) → false | |
| | EffectiveEtPermanente → λ (__260: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__261: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__262: unit) → true ⊢ Zéro | |
| ()⟩, | |
| ⟨match param_252.prise_en_charge with | |
| GardeAlternéePartageAllocations → λ (__263: unit) → true | |
| | | |
| GardeAlternéeAllocataireUnique → λ (__264: unit) → false | |
| | EffectiveEtPermanente → λ (__265: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__266: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__267: unit) → false ⊢ Partagée | |
| ()⟩, | |
| ⟨match param_252.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__268: unit) → false | | |
| GardeAlternéeAllocataireUnique → λ (__269: unit) → true | |
| | EffectiveEtPermanente → λ (__270: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__271: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__272: unit) → false ⊢ Complète | |
| ()⟩, | |
| ⟨match param_252.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__273: unit) → false | | |
| GardeAlternéeAllocataireUnique → λ (__274: unit) → false | |
| | EffectiveEtPermanente → λ (__275: unit) → true | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__276: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__277: unit) → false ⊢ Complète | |
| ()⟩ | false ⊢ ∅ ⟩ in; | |
| let versement : Enfant → VersementAllocations = | |
| reentrant or by default | |
| λ (param_278: Enfant) → error_empty | |
| ⟨⟨match param_278.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__279: unit) → false | | |
| GardeAlternéeAllocataireUnique → | |
| λ (__280: unit) → false | | |
| EffectiveEtPermanente → λ (__281: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__282: unit) → true | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__283: unit) → false ⊢ Normal | |
| ()⟩, | |
| ⟨match param_278.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__284: unit) → false | | |
| GardeAlternéeAllocataireUnique → λ (__285: unit) → false | |
| | EffectiveEtPermanente → λ (__286: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__287: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__288: unit) → true ⊢ AllocationVerséeAuxServicesSociaux | |
| ()⟩, | |
| ⟨match param_278.prise_en_charge with | |
| GardeAlternéePartageAllocations → λ (__289: unit) → true | |
| | | |
| GardeAlternéeAllocataireUnique → λ (__290: unit) → false | |
| | EffectiveEtPermanente → λ (__291: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__292: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__293: unit) → false ⊢ Normal | |
| ()⟩, | |
| ⟨match param_278.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__294: unit) → false | | |
| GardeAlternéeAllocataireUnique → λ (__295: unit) → true | |
| | EffectiveEtPermanente → λ (__296: unit) → false | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__297: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__298: unit) → false ⊢ Normal | |
| ()⟩, | |
| ⟨match param_278.prise_en_charge with | |
| GardeAlternéePartageAllocations → | |
| λ (__299: unit) → false | | |
| GardeAlternéeAllocataireUnique → λ (__300: unit) → false | |
| | EffectiveEtPermanente → λ (__301: unit) → true | | |
| ServicesSociauxAllocationVerséeÀLaFamille → | |
| λ (__302: unit) → false | | |
| ServicesSociauxAllocationVerséeAuxServicesSociaux → | |
| λ (__303: unit) → false ⊢ Normal | |
| ()⟩ | false ⊢ ∅ ⟩ in; | |
| let nombre_enfants_l521_1 : integer = | |
| reentrant or by default ⟨⟨true ⊢ 3⟩ | false ⊢ ∅ ⟩ in; | |
| let nombre_enfants_alinéa_2_l521_3 : integer = | |
| reentrant or by default ⟨⟨true ⊢ 3⟩ | false ⊢ ∅ ⟩ in; | |
| call AllocationFamilialesAvril2008[version_avril_2008]; | |
| let prestations_familiales.date_courante : date = | |
| ⟨⟨true ⊢ date_courante⟩ | false ⊢ ∅ ⟩ in; | |
| let prestations_familiales.prestation_courante : ÉlémentPrestationsFamiliales = | |
| ⟨⟨true ⊢ AllocationsFamiliales ()⟩ | false ⊢ ∅ ⟩ in; | |
| let prestations_familiales.résidence : Collectivité = | |
| ⟨⟨true ⊢ résidence⟩ | false ⊢ ∅ ⟩ in; | |
| call PrestationsFamiliales[prestations_familiales]; | |
| let enfant_le_plus_âgé.enfants : Enfant array = | |
| ⟨⟨true ⊢ enfants_à_charge⟩ | false ⊢ ∅ ⟩ in; | |
| call EnfantLePlusÂgé[enfant_le_plus_âgé]; | |
| let âge_minimum_alinéa_1_l521_3 : Enfant → integer = | |
| reentrant or by default | |
| λ (param_304: Enfant) → error_empty | |
| ⟨⟨⟨param_304.date_de_naissance +@ 11 years <=@ 2008-04-30 ⊢ version_avril_2008.âge_minimum_alinéa_1_l521_3⟩ | |
| | true ⊢ 14⟩ | false ⊢ ∅ ⟩ in; | |
| let enfants_à_charge_droit_ouvert_prestation_familiale : Enfant array = | |
| reentrant or by default | |
| ⟨⟨true ⊢ (λ (enfant_305: any) → | |
| prestations_familiales.droit_ouvert enfant_305) | |
| filter enfants_à_charge⟩ | false ⊢ ∅ ⟩ in; | |
| let est_enfant_le_plus_âgé : Enfant → bool = | |
| reentrant or by default | |
| λ (param_306: Enfant) → error_empty | |
| ⟨⟨true ⊢ enfant_le_plus_âgé.le_plus_âgé = param_306⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let plafond_II_d521_3 : money = | |
| reentrant or by default | |
| ⟨⟨⟨date_courante >=@ 2021-01-01 && date_courante <=@ 2021-12-31 ⊢ | |
| 81558.00 € +$ | |
| 5827.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩, | |
| ⟨date_courante >=@ 2020-01-01 && date_courante <=@ 2020-12-31 ⊢ | |
| 80831.00 € +$ | |
| 5775.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩, | |
| ⟨date_courante >=@ 2019-01-01 && date_courante <=@ 2019-12-31 ⊢ | |
| 79558.00 € +$ | |
| 5684.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩, | |
| ⟨date_courante >=@ 2018-01-01 && date_courante <=@ 2018-12-31 ⊢ | |
| 78770.00 € +$ | |
| 5628.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩ | | |
| true ⊢ 78300.00 € +$ | |
| 5595.00 € *$ | |
| int_to_rat | |
| length | |
| enfants_à_charge_droit_ouvert_prestation_familiale⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let plafond_I_d521_3 : money = | |
| reentrant or by default | |
| ⟨⟨⟨date_courante >=@ 2021-01-01 && date_courante <=@ 2021-12-31 ⊢ | |
| 58279.00 € +$ | |
| 5827.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩, | |
| ⟨date_courante >=@ 2020-01-01 && date_courante <=@ 2020-12-31 ⊢ | |
| 57759.00 € +$ | |
| 5775.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩, | |
| ⟨date_courante >=@ 2019-01-01 && date_courante <=@ 2019-12-31 ⊢ | |
| 56849.00 € +$ | |
| 5684.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩, | |
| ⟨date_courante >=@ 2018-01-01 && date_courante <=@ 2018-12-31 ⊢ | |
| 56286.00 € +$ | |
| 5628.00 € *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale⟩ | | |
| true ⊢ 55950.00 € +$ | |
| 5595.00 € *$ | |
| int_to_rat | |
| length | |
| enfants_à_charge_droit_ouvert_prestation_familiale⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let droit_ouvert_complément : bool = | |
| reentrant or by default | |
| ⟨⟨⟨prestations_familiales.régime_outre_mer_l751_1 && | |
| length enfants_à_charge_droit_ouvert_prestation_familiale = 1 ⊢ false⟩ | |
| | true ⊢ true⟩ | true ⊢ false⟩ in; | |
| let droit_ouvert_forfaitaire : Enfant → bool = | |
| reentrant or by default | |
| λ (param_307: Enfant) → error_empty | |
| ⟨⟨⟨prestations_familiales.régime_outre_mer_l751_1 && | |
| length enfants_à_charge_droit_ouvert_prestation_familiale = | |
| 1 ⊢ false⟩ | | |
| length enfants_à_charge >= nombre_enfants_alinéa_2_l521_3 && | |
| param_307.âge = prestations_familiales.âge_l512_3_2 && | |
| param_307.a_déjà_ouvert_droit_aux_allocations_familiales && | |
| prestations_familiales.conditions_hors_âge param_307 ⊢ true⟩ | |
| | true ⊢ false⟩ in; | |
| let nombre_total_enfants : decimal = | |
| reentrant or by default | |
| ⟨⟨true ⊢ int_to_rat | |
| length | |
| enfants_à_charge_droit_ouvert_prestation_familiale⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let nombre_moyen_enfants : decimal = | |
| reentrant or by default | |
| ⟨⟨true ⊢ fold | |
| (λ (acc_308: decimal) (enfant_309: any) → | |
| acc_308 +. | |
| match prise_en_compte enfant_309 with | |
| Complète → λ (__310: unit) → 1. | | |
| Partagée → λ (__311: unit) → 0.5 | | |
| Zéro → λ (__312: unit) → 0.) | |
| 0. enfants_à_charge_droit_ouvert_prestation_familiale⟩ | |
| | false ⊢ ∅ ⟩ in; | |
| let montant_initial_base_premier_enfant : money = | |
| reentrant or by default | |
| ⟨⟨length enfants_à_charge_droit_ouvert_prestation_familiale = 1 ⊢ | |
| prestations_familiales.base_mensuelle *$ 0.0588⟩, | |
| ⟨length enfants_à_charge_droit_ouvert_prestation_familiale != 1 ⊢ 0.00 €⟩ | |
| | false ⊢ ∅ ⟩ in; | |
| let droit_ouvert_base : bool = | |
| reentrant or by default | |
| ⟨⟨⟨prestations_familiales.régime_outre_mer_l751_1 && | |
| length enfants_à_charge_droit_ouvert_prestation_familiale >= | |
| 1 ⊢ true⟩ | | |
| length enfants_à_charge_droit_ouvert_prestation_familiale >= 2 ⊢ true⟩ | |
| | true ⊢ false⟩ in; | |
| let droit_ouvert_majoration : Enfant → bool = | |
| reentrant or by default | |
| λ (param_313: Enfant) → error_empty | |
| ⟨⟨⟨length enfants_à_charge_droit_ouvert_prestation_familiale | |
| >= nombre_enfants_alinéa_2_l521_3 && | |
| param_313.âge >= âge_minimum_alinéa_1_l521_3 param_313 ⊢ true⟩ | |
| | | |
| ~ est_enfant_le_plus_âgé param_313 && | |
| param_313.âge >= âge_minimum_alinéa_1_l521_3 param_313 ⊢ true⟩ | |
| | true ⊢ false⟩ in; | |
| let complément_dégressif : money → money = | |
| reentrant or by default | |
| λ (param_314: money) → error_empty | |
| ⟨⟨⟨ressources_ménage >$ plafond_II_d521_3 && | |
| ressources_ménage <=$ plafond_II_d521_3 +$ param_314 *$ 12. ⊢ | |
| plafond_II_d521_3 +$ param_314 *$ 12. -$ ressources_ménage *$ | |
| 1. /. 12.⟩, | |
| ⟨ressources_ménage >$ plafond_I_d521_3 && | |
| ressources_ménage <=$ plafond_I_d521_3 +$ param_314 *$ 12. ⊢ | |
| plafond_I_d521_3 +$ param_314 *$ 12. -$ ressources_ménage *$ | |
| 1. /. 12.⟩ | true ⊢ 0.00 €⟩ | false ⊢ ∅ ⟩ in; | |
| let montant_versé_forfaitaire_par_enfant : money = | |
| reentrant or by default | |
| ⟨⟨ressources_ménage >$ plafond_II_d521_3 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.0559⟩, | |
| ⟨ressources_ménage >$ plafond_I_d521_3 && | |
| ressources_ménage <=$ plafond_II_d521_3 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.1117⟩, | |
| ⟨ressources_ménage <=$ plafond_I_d521_3 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.20234⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_initial_base_troisième_enfant_et_plus : money = | |
| reentrant or by default | |
| ⟨⟨ressources_ménage >$ plafond_II_d521_3 ⊢ if | |
| length enfants_à_charge_droit_ouvert_prestation_familiale > 2 then | |
| prestations_familiales.base_mensuelle *$ 0.1025 *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale - 2 else | |
| 0.00 €⟩, | |
| ⟨ressources_ménage >$ plafond_I_d521_3 && | |
| ressources_ménage <=$ plafond_II_d521_3 ⊢ if | |
| length enfants_à_charge_droit_ouvert_prestation_familiale > 2 then | |
| prestations_familiales.base_mensuelle *$ 0.205 *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale - 2 else | |
| 0.00 €⟩, | |
| ⟨ressources_ménage <=$ plafond_I_d521_3 ⊢ if | |
| length enfants_à_charge_droit_ouvert_prestation_familiale > 2 then | |
| prestations_familiales.base_mensuelle *$ 0.41 *$ | |
| int_to_rat | |
| length enfants_à_charge_droit_ouvert_prestation_familiale - 2 else | |
| 0.00 €⟩ | false ⊢ ∅ ⟩ in; | |
| let montant_initial_base_deuxième_enfant : money = | |
| reentrant or by default | |
| ⟨⟨ressources_ménage >$ plafond_II_d521_3 ⊢ if | |
| length enfants_à_charge_droit_ouvert_prestation_familiale > 1 then | |
| prestations_familiales.base_mensuelle *$ 0.08 else 0.00 €⟩, | |
| ⟨ressources_ménage >$ plafond_I_d521_3 && | |
| ressources_ménage <=$ plafond_II_d521_3 ⊢ if | |
| length enfants_à_charge_droit_ouvert_prestation_familiale > 1 then | |
| prestations_familiales.base_mensuelle *$ 0.16 else 0.00 €⟩, | |
| ⟨ressources_ménage <=$ plafond_I_d521_3 ⊢ if | |
| length enfants_à_charge_droit_ouvert_prestation_familiale > 1 then | |
| prestations_familiales.base_mensuelle *$ 0.32 else 0.00 €⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let rapport_enfants_total_moyen : decimal = | |
| reentrant or by default | |
| ⟨⟨true ⊢ if nombre_total_enfants = 0. then 0. else | |
| nombre_moyen_enfants /. nombre_total_enfants⟩ | false ⊢ ∅ ⟩ | |
| in; | |
| let montant_initial_métropole_majoration : Enfant → money = | |
| reentrant or by default | |
| λ (param_315: Enfant) → error_empty | |
| ⟨⟨~ droit_ouvert_majoration param_315 ⊢ 0.00 €⟩, | |
| ⟨ressources_ménage >$ plafond_II_d521_3 && | |
| droit_ouvert_majoration param_315 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.04⟩, | |
| ⟨ressources_ménage >$ plafond_I_d521_3 && | |
| ressources_ménage <=$ plafond_II_d521_3 && | |
| droit_ouvert_majoration param_315 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.08⟩, | |
| ⟨ressources_ménage <=$ plafond_I_d521_3 && | |
| droit_ouvert_majoration param_315 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.16⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_versé_forfaitaire : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ montant_versé_forfaitaire_par_enfant *$ | |
| int_to_rat | |
| fold | |
| (λ (acc_316: integer) (enfant_317: any) → if | |
| droit_ouvert_forfaitaire enfant_317 then acc_316 + 1 | |
| else acc_316) | |
| 0 enfants_à_charge⟩ | false ⊢ ∅ ⟩ in; | |
| let montant_initial_base : money = | |
| reentrant or by default | |
| ⟨⟨⟨prestations_familiales.régime_outre_mer_l751_1 && | |
| length enfants_à_charge_droit_ouvert_prestation_familiale = 1 ⊢ montant_initial_base_premier_enfant⟩ | |
| | | |
| true ⊢ montant_initial_base_deuxième_enfant +$ | |
| montant_initial_base_troisième_enfant_et_plus⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_initial_majoration : Enfant → money = | |
| reentrant or by default | |
| λ (param_318: Enfant) → error_empty | |
| ⟨⟨⟨droit_ouvert_majoration param_318 && | |
| prestations_familiales.régime_outre_mer_l751_1 && | |
| length enfants_à_charge_droit_ouvert_prestation_familiale = | |
| 1 && param_318.âge >= 16 ⊢ prestations_familiales.base_mensuelle | |
| *$ 0.0567⟩, | |
| ⟨droit_ouvert_majoration param_318 && | |
| prestations_familiales.régime_outre_mer_l751_1 && | |
| length enfants_à_charge_droit_ouvert_prestation_familiale = | |
| 1 && param_318.âge >= 11 && param_318.âge < 16 ⊢ | |
| prestations_familiales.base_mensuelle *$ 0.0369⟩ | | |
| true ⊢ montant_initial_métropole_majoration param_318⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_versé_complément_pour_forfaitaire : money = | |
| reentrant or by default | |
| ⟨⟨⟨ressources_ménage >$ plafond_II_d521_3 && | |
| ressources_ménage <=$ | |
| plafond_II_d521_3 +$ montant_versé_forfaitaire *$ 12. ⊢ | |
| plafond_II_d521_3 +$ | |
| montant_versé_forfaitaire *$ 12. -$ ressources_ménage *$ | |
| 1. /. 12.⟩, | |
| ⟨ressources_ménage >$ plafond_I_d521_3 && | |
| ressources_ménage <=$ | |
| plafond_I_d521_3 +$ montant_versé_forfaitaire *$ 12. ⊢ | |
| plafond_I_d521_3 +$ | |
| montant_versé_forfaitaire *$ 12. -$ ressources_ménage *$ | |
| 1. /. 12.⟩ | true ⊢ 0.00 €⟩ | false ⊢ ∅ ⟩ in; | |
| let montant_avec_garde_alternée_base : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ montant_initial_base *$ rapport_enfants_total_moyen⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_avec_garde_alternée_majoration : Enfant → money = | |
| reentrant or by default | |
| λ (param_319: Enfant) → error_empty | |
| ⟨⟨true ⊢ montant_initial_majoration param_319 *$ | |
| match prise_en_compte param_319 with | |
| Complète → λ (__320: unit) → 1. | | |
| Partagée → λ (__321: unit) → 0.5 | | |
| Zéro → λ (__322: unit) → 0.⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_versé_base : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ if droit_ouvert_base then | |
| montant_avec_garde_alternée_base else 0.00 €⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_versé_majoration : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ if droit_ouvert_base then | |
| fold | |
| (λ (acc_323: money) (enfant_324: any) → | |
| acc_323 +$ montant_avec_garde_alternée_majoration enfant_324) | |
| 0.00 € enfants_à_charge else 0.00 €⟩ | false ⊢ ∅ ⟩ in; | |
| let montant_base_complément_pour_base_et_majoration : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ montant_versé_base +$ montant_versé_majoration⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_versé_complément_pour_base_et_majoration : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ if droit_ouvert_complément then | |
| complément_dégressif | |
| montant_base_complément_pour_base_et_majoration else 0.00 €⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| let montant_versé : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ if droit_ouvert_base then | |
| montant_versé_base +$ | |
| montant_versé_majoration +$ | |
| montant_versé_forfaitaire +$ | |
| montant_versé_complément_pour_base_et_majoration +$ | |
| montant_versé_complément_pour_forfaitaire else 0.00 €⟩ | | |
| false ⊢ ∅ ⟩ in; | |
| assert (personne_charge_effective_permanente_est_parent || | |
| ~ personne_charge_effective_permanente_est_parent && | |
| personne_charge_effective_permanente_remplit_titre_I) | |
| end scope | |
| let scope InterfaceAllocationsFamiliales (date_courante: date) | |
| (enfants: EnfantEntrée array) (enfants_à_charge: Enfant array) | |
| (ressources_ménage: money) (résidence: Collectivité) | |
| (montant_versé: money) | |
| (personne_charge_effective_permanente_est_parent: bool) | |
| (personne_charge_effective_permanente_remplit_titre_I: bool) = | |
| let date_courante : date = reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let enfants : EnfantEntrée array = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let ressources_ménage : money = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let résidence : Collectivité = | |
| reentrant or by default ⟨false ⊢ ∅ ⟩ in; | |
| let personne_charge_effective_permanente_est_parent : bool = | |
| reentrant or by default ⟨true ⊢ false⟩ in; | |
| let personne_charge_effective_permanente_remplit_titre_I : bool = | |
| reentrant or by default ⟨true ⊢ false⟩ in; | |
| let enfants_à_charge : Enfant array = | |
| reentrant or by default | |
| ⟨⟨true ⊢ (λ (enfant_325: any) → | |
| Enfant { identifiant = enfant_325.d_identifiant; | |
| obligation_scolaire = if | |
| enfant_325.d_date_de_naissance +@ 3 years | |
| >=@ date_courante then Avant () else | |
| if | |
| enfant_325.d_date_de_naissance +@ 16 years | |
| >=@ date_courante then Pendant () else | |
| Après (); | |
| rémuneration_mensuelle = enfant_325.d_rémuneration_mensuelle; | |
| date_de_naissance = enfant_325.d_date_de_naissance; | |
| âge = get_year | |
| 0000-01-01 +@ | |
| date_courante -@ | |
| enfant_325.d_date_de_naissance; | |
| prise_en_charge = enfant_325.d_prise_en_charge; | |
| a_déjà_ouvert_droit_aux_allocations_familiales = enfant_325.d_a_déjà_ouvert_droit_aux_allocations_familiales | |
| }) | |
| map enfants⟩ | false ⊢ ∅ ⟩ in; | |
| let allocations_familiales.personne_charge_effective_permanente_est_parent : bool = | |
| ⟨⟨personne_charge_effective_permanente_est_parent ⊢ true⟩ | | |
| true ⊢ false⟩ in; | |
| let allocations_familiales.personne_charge_effective_permanente_remplit_titre_I : bool = | |
| ⟨⟨personne_charge_effective_permanente_remplit_titre_I ⊢ true⟩ | | |
| true ⊢ false⟩ in; | |
| let allocations_familiales.ressources_ménage : money = | |
| ⟨⟨true ⊢ ressources_ménage⟩ | false ⊢ ∅ ⟩ in; | |
| let allocations_familiales.résidence : Collectivité = | |
| ⟨⟨true ⊢ résidence⟩ | false ⊢ ∅ ⟩ in; | |
| let allocations_familiales.date_courante : date = | |
| ⟨⟨true ⊢ date_courante⟩ | false ⊢ ∅ ⟩ in; | |
| let allocations_familiales.enfants_à_charge : Enfant array = | |
| ⟨⟨true ⊢ enfants_à_charge⟩ | false ⊢ ∅ ⟩ in; | |
| call AllocationsFamiliales[allocations_familiales]; | |
| let montant_versé : money = | |
| reentrant or by default | |
| ⟨⟨true ⊢ allocations_familiales.montant_versé⟩ | | |
| false ⊢ ∅ ⟩ in | |
| end scope |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment