------------------------------------------------------------------------
-- Some examples which are used to illustrate properties of modality
-- instances
------------------------------------------------------------------------

open import Definition.Typed.Restrictions

import Graded.Modality

module Graded.Modality.Instances.Examples
  {a} {M : Set a}
  (open Graded.Modality M)
  {𝕄 : Modality}
  (open Modality 𝕄)
  (R : Type-restrictions 𝕄)
  (open Type-restrictions R)
  -- It is assumed that "Ξ Β πŸ™Β , 𝟘" is allowed.
  (Ξ -πŸ™-𝟘 : Ξ -allowed πŸ™ 𝟘)
  where

open import Tools.Fin
open import Tools.Function
import Tools.Reasoning.PartialOrder

open import Definition.Typed R
open import Definition.Untyped M

private

  -- Some lemmas used below.

  βŠ’β„• : ⊒ Ξ΅ βˆ™ β„•
  βŠ’β„•  = Ξ΅ βˆ™ β„•β±Ό Ξ΅

  βŠ’β„•β„• : ⊒ Ξ΅ βˆ™ β„• βˆ™ β„•
  βŠ’β„•β„• = βŠ’β„• βˆ™ β„•β±Ό βŠ’β„•

  βŠ’β„•β„•β„• : ⊒ Ξ΅ βˆ™ β„• βˆ™ β„• βˆ™ β„•
  βŠ’β„•β„•β„• = βŠ’β„•β„• βˆ™ β„•β±Ό βŠ’β„•β„•

  βŠ’β„•β„•β„•β„• : ⊒ Ξ΅ βˆ™ β„• βˆ™ β„• βˆ™ β„• βˆ™ β„•
  βŠ’β„•β„•β„•β„• = βŠ’β„•β„•β„• βˆ™ β„•β±Ό βŠ’β„•β„•β„•

-- A program that takes a natural number and adds it to itself:
-- λ n. n + n. This program should presumably not be seen as linear,
-- because the variable "n" is used twice.

double : Term 0
double = lam πŸ™ (natrec 𝟘 𝟘 πŸ™ β„• (var x0) (suc (var x0)) (var x0))

-- The term double is well-typed.
--
-- Note that the term can be given a linear type.
--
-- With a certain "linearity" modality the term is also
-- well-resourced, see
-- Graded.Modality.Instances.Linearity.Bad.β–Έdouble. However, with
-- another linearity modality the term is not well-resourced, see
-- Graded.Modality.Instances.Linearity.Good.Β¬β–Έdouble.

⊒double : Ξ΅ ⊒ double ∷ Ξ  πŸ™ , 𝟘 β–· β„• β–Ή β„•
⊒double =
  flip (lamβ±Ό (β„•β±Ό Ξ΅)) Ξ -πŸ™-𝟘 $
  natrecβ±Ό (β„•β±Ό βŠ’β„•β„•) (var βŠ’β„• here)
    (sucβ±Ό (var βŠ’β„•β„•β„• here))
    (var βŠ’β„• here)

-- A program that takes two natural numbers and adds them:
-- λ m n. m + n. It might make sense to see this program as linear in
-- both arguments.

plus : Term 0
plus = lam πŸ™ $ lam πŸ™ $ natrec 𝟘 𝟘 πŸ™ β„• (var x0) (suc (var x0)) (var x1)

-- The term plus is well-typed.
--
-- With a certain linearity modality the term is also well-resourced,
-- see Graded.Modality.Instances.Linearity.Good.β–Έplus. However, with
-- another "linearity" modality the term is not well-resourced, see
-- Graded.Modality.Instances.Linearity.Bad.Β¬β–Έplus.

⊒plus : Ξ΅ ⊒ plus ∷ Ξ  πŸ™ , 𝟘 β–· β„• β–Ή Ξ  πŸ™ , 𝟘 β–· β„• β–Ή β„•
⊒plus =
  flip (lamβ±Ό (β„•β±Ό Ξ΅)) Ξ -πŸ™-𝟘 $
  flip (lamβ±Ό (β„•β±Ό βŠ’β„•)) Ξ -πŸ™-𝟘 $
  natrecβ±Ό (β„•β±Ό βŠ’β„•β„•β„•) (var βŠ’β„•β„• here)
    (sucβ±Ό (var βŠ’β„•β„•β„•β„• here))
    (var βŠ’β„•β„• (there here))