-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of CCSLNaturals is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

open import Data.Nat hiding (compare)
open import Data.Nat.Induction
open import Data.Nat.Properties 
open import Relation.Binary hiding (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary hiding (_⇒_)
open import Relation.Nullary
open import Data.Product
open import Function
open import Data.Empty
open import Data.Sum renaming (swap to swap⊎)
open import Relation.Nullary.Negation
open import Induction.WellFounded

module CCSLNaturals where

precedent :  {} {P : Pred  }  Decidable P  (j :  P) 
  (∀ {x}  x < proj₁ j  ¬ P x)   \(i :  P)
     proj₁ i < proj₁ j × (∀ {x}  proj₁ i < x  x < proj₁ j  ¬ P x)
precedent _ (zero , _) = inj₁ \()
precedent dp (suc j , tj) = aux dp j (suc j) tj (n<1+n _)
  λ j<x  ⊥-elim  (<-irrefl {suc j} refl)  (<-transʳ j<x) where
    aux :  {} {P : Pred  } (dp : Decidable P)
      (i j : ) (pc : P j) (i<j : i < j) 
      (∀ {x}  i < x  x < j  ¬ P x)
       (∀ {x}  x < j  ¬ P x) 
       \(k :  P)  proj₁ k < j ×
      (∀ {x}  proj₁ k < x  x < j  ¬ P x)
    aux dp i j pc i≺j p with dp i
    aux dp zero j pc i≺j p | no ¬p = inj₁ λ {
      {zero} x<j tx  ⊥-elim (¬p tx) ;
      {suc _} x<j tx  p (s≤s z≤n) x<j tx}
    aux dp (suc i) j pc i≺j p | no ¬p =
      aux dp i j pc (<-trans (n<1+n i) i≺j)
        λ i<x x<j tx  case m≤n⇒m<n∨m≡n i<x of
          λ {(inj₁ si<x)  p si<x x<j tx ; (inj₂ refl)  ¬p tx}
    aux dp i j pc i≺j p | yes p₁ = inj₂ ((i , p₁) , i≺j , p)

wf-<P :  {} {P : Pred  }  Decidable P
   WellFounded {A =  P} (_<_ on proj₁)
wf-<P {P = P} dec x = aux x (<-wellFounded (proj₁ x))
  where
    aux :  (i :  P)  Acc _<_ (proj₁ i)  Acc (_<_ on proj₁) i
    aux i ai with precedent dec i
    aux i ai | inj₁ p = acc  j j≺i  ⊥-elim (p j≺i (proj₂ j)))
    aux i (acc q) | inj₂ (j , j≺i , p) with aux j (q _ j≺i)
    aux i ai | inj₂ (j , j≺i , p) | acc rs =
      acc λ y y≺i  case <-cmp (proj₁ j) (proj₁ y) of λ {
        (tri< a _ _)  ⊥-elim ((p a y≺i) (proj₂ y)) ;
        (tri≈ _ refl _)  acc rs ;
        (tri> _ _ c)  rs y c}

initial :  {} {P : Pred  }  Decidable P
    P   λ (x :  P)   (y :  P)  proj₁ x  proj₁ y
initial {P = P} dec p = aux p (<-wellFounded _)
  where
    aux : (i :  P)  Acc _<_ (proj₁ i) 
       λ (x :  P)   (y :  P)  proj₁ x  proj₁ y
    aux i (acc p) with precedent dec i
    aux i (acc p) | inj₁ x = i , λ y 
      case <-cmp (proj₁ i) (proj₁ y) of λ {
        (tri< a _ _)  <⇒≤ a ;
        (tri≈ _ refl _)  ≤-refl ;
        (tri> _ _ c)  ⊥-elim (x c (proj₂ y))}
    aux i (acc p) | inj₂ (y , z , _) = aux y (p _ z)

open import CCSL
  (record {
    isStrictPartialOrder = <-isStrictPartialOrder })
open Clock

record Clock-¬∅-Dec : Set₁ where
  field
    clock : Clock
    non-empty :  (Ticks clock)
    decidable : Decidable (Ticks clock)

  wf-≺ : _
  wf-≺ = wf-<P decidable

  birth : _
  birth = let (i , p) = initial decidable non-empty in
    i , swap⊎  m≤n⇒m<n∨m≡n  p

  toWf : WFClock
  toWf = record { clock = clock ; wf-≺ = wf-≺ }

  toIn : InitialClock
  toIn = record { clock = clock ; first = birth }