SListForYCombinatorian

SList.idr

--module Queue
 
import Syntax.WithProof
 
%default total
   
data State = Empty | NonEmpty
 
Eq State where
  Empty == Empty = True
  NonEmpty == NonEmpty = True
  _ == _ = False
 
Ord State where
  compare Empty NonEmpty = LT
  compare NonEmpty Empty = GT
  compare _ _ = EQ
 
data SList : (s : State) -> (a : Type) -> Type where
  Nil : SList Empty a
  (::) : {s : State} -> a -> SList s a -> SList NonEmpty a
 
data Queue : (y : State) -> (a : Type) -> Type where
  Q : (e : SList y a) ->
      (d : SList z a) ->
      {auto p : y >= z = True} ->
      Queue y a
 
head : Queue NonEmpty a -> a
head (Q (x::_) _) = x
 
maxId : (s : State) -> max s Empty = s
maxId Empty = Refl
maxId NonEmpty = Refl
 
maxDom : (s : State) -> max s NonEmpty = NonEmpty
maxDom Empty = Refl
maxDom NonEmpty = Refl
 
append : {y,z : State} -> (a : SList y v) -> (b : SList z v) -> SList (max y z) v
append [] [] = [] 
append [] (x :: xs) = (x :: xs) -- added in the extra case here, most recent version of Idris 2 was complaining.
append a [] = rewrite maxId y in a
append (x::xs) b@(_::_) = x :: (xs `append` b) -- need explicit parens here in latest version of Idris 2.
 
getState : {s : State} -> SList s v -> State
getState {s} _ = s
 
isState : (a : SList s v) -> getState a = s
isState a = Refl
 
appendDom : (a : SList s v) -> (b : SList NonEmpty v) -> getState (a `append` b) = NonEmpty
appendDom [] b = Refl
appendDom (x::xs) b = Refl
 
rev : SList s a -> SList s a
rev [] = []
rev (x::xs) with (@@ (getState xs))
  rev (x::xs) | (Empty ** Refl) = [x] -- we *must* type in the `rev (x :: xs)` on each line of the with now.
  rev (x::xs) | (NonEmpty ** Refl) = (rev xs) `append` [x] -- we have lost the | syntax from Idris1.