{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import HetroVector
open import Ord
open import BoolOrd

module DescriptorsFull where

open import List public


-- Decoupledness Descriptors -- 

-- Rather than create a datatype for Dec, we use booleans so we can use existing
-- boolean proofs

Dec : Set
Dec = Bool

dec : Dec
dec = false

cau : Dec
cau = true


-- Initialisation Descriptors --

-- Rather than create a datatype for Init, we use booleans so we can use existing
-- boolean proofs

Init : Set
Init = Bool

ini : Init
ini = false

uni : Init
uni = true


-- Signal Descriptors --

-- We have two data types for signal descriptors, one for time0, one for time>0
-- We use the 0 suffix for Time0, and the R suffix (for 'running') after Time0

data SigDesc0 : Set where
  E : Set → SigDesc0
  C : Init → Set → SigDesc0

SVDesc0 : Set
SVDesc0 = List SigDesc0


data SigDescR : Set where
  E : Set → SigDescR
  C : Set → SigDescR

SVDescR : Set
SVDescR = List SigDescR


-- converting from time0 to Running

sd0toR : SigDesc0 → SigDescR
sd0toR (E A)   = E A
sd0toR (C _ A) = C A

svd0toR : SVDesc0 → SVDescR
svd0toR = map sd0toR


-- initc is needed for the type of switch

initcAux : SigDesc0 → SigDesc0
initcAux (E A)    = E A
initcAux (C _ A)  = C ini A

initc : SVDesc0 → SVDesc0
initc = map initcAux


-- Subtyping --

infix  _<:_ _<:'_

data _<:'_ : SigDesc0 → SigDesc0 → Set where
  subC : {i₁ i₂ : Init} → {A : Set} → i₁ ≤ i₂ → C i₁ A <:' C i₂ A
  subE : {A : Set} → E A <:' E A

_<:_ : Rel SVDesc0
_<:_ = All2 _<:'_

<:refl' : Reflexive _<:'_
<:refl' {E _}   = subE
<:refl' {C _ _} = subC ≤-refl

<:trans' : Transitive _<:'_
<:trans' (subC ab) (subC bc) = subC (≤-trans ab bc)
<:trans' subE bc = bc

<:trans : Transitive _<:_
<:trans = all2trans <:trans'

-- Properties of Signals --

InitSD : SigDesc0 → Set
InitSD (C true _) = False
InitSD _          = True

NotInitSD : SigDesc0 → Set
NotInitSD (C false _) = False
NotInitSD _           = True

InitSV : SVDesc0 → Set
InitSV = All InitSD

NotInitSV : SVDesc0 → Set
NotInitSV = All NotInitSD


-- Lemmas --

open import ListProps

initcsigIdem : {a : SigDesc0} → initcAux (initcAux a) ≡ initcAux a
initcsigIdem {E _}   = refl
initcsigIdem {C _ _} = refl

initcIdem : (as : SVDesc0) → initc (initc as) ≡ initc as
initcIdem = listIdem initcsigIdem

sd0toRinitcAux : {b : SigDesc0} → sd0toR (initcAux b) ≡ sd0toR b
sd0toRinitcAux {E _} = refl
sd0toRinitcAux {C _ _} = refl

open import Recursion

svd0toRinitc : (bs : SVDesc0) → svd0toR (initc bs) ≡ svd0toR bs
svd0toRinitc = listrec refl (∷-cong sd0toRinitcAux)


<:0toR' : {a a' : SigDesc0} → a <:' a' → sd0toR a ≡ sd0toR a'
<:0toR' (subC _) = refl
<:0toR' subE = refl

<:0toR : {as as' : SVDesc0} → as <: as' → svd0toR as ≡ svd0toR as'
<:0toR = fequivPred <:0toR'


<:initc' : {a : SigDesc0} → initcAux a <:' a
<:initc' {E _} = subE
<:initc' {C _ _} = subC ≤false 

<:initc : {as : SVDesc0} → initc as <: as
<:initc = hvec2L <:initc'


<:initc0toR : {as bs : SVDesc0} → initc as <: bs → svd0toR as ≡ svd0toR bs
<:initc0toR {as} sb = trans (sym (svd0toRinitc as)) (<:0toR sb)