open import Level hiding (lift)
open import Data.Maybe
open import Data.Product
open import Data.Nat hiding (suc)
open import Function

module stack-subtype (A : Set) where

-- data definitions

data Element (a : Set) : Set where
  cons : a @$\rightarrow$@ Maybe (Element a) @$\rightarrow$@ Element a

datum : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ a
datum (cons a _) = a

next : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ Maybe (Element a)
next (cons _ n) = n

record SingleLinkedStack (a : Set) : Set where
  field
    top : Maybe (Element a)
open SingleLinkedStack

record Context : Set where
  field
    -- fields for concrete data segments
    n       : @$\mathbb{N}$@ 
    -- fields for stack
    element : Maybe A





open import subtype Context as N

instance
  ContextIsDataSegment : N.DataSegment Context
  ContextIsDataSegment = record {get = (\c @$\rightarrow$@ c) ; set = (\_ c @$\rightarrow$@ c)}


record Meta  : Set@$\_{1}$@ where
  field
    -- context as set of data segments
    context : Context
    stack   : SingleLinkedStack A  
    nextCS  : N.CodeSegment Context Context
    

    

open import subtype Meta as M

instance
  MetaIncludeContext : M.DataSegment Context
  MetaIncludeContext = record { get = Meta.context
                              ; set = (\m c @$\rightarrow$@ record m {context = c}) }

  MetaIsMetaDataSegment : M.DataSegment Meta
  MetaIsMetaDataSegment  = record { get = (\m @$\rightarrow$@ m) ; set = (\_ m @$\rightarrow$@ m) }


liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ M.CodeSegment X Y
liftMeta (N.cs f) = M.cs f

liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ N.CodeSegment Context Context
liftContext {{x}} {{y}} (N.cs f) = N.cs (\c @$\rightarrow$@ N.DataSegment.set y c (f (N.DataSegment.get x c)))
 
-- definition based from Gears(209:5708390a9d88) src/parallel_execution

emptySingleLinkedStack : SingleLinkedStack A
emptySingleLinkedStack = record {top = nothing}


pushSingleLinkedStack : Meta @$\rightarrow$@ Meta
pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
  where
    n = Meta.nextCS m
    s = Meta.stack  m
    e = Context.element (Meta.context m)
    push : SingleLinkedStack A @$\rightarrow$@ Maybe A @$\rightarrow$@ SingleLinkedStack A
    push s nothing  = s
    push s (just x) = record {top = just (cons x (top s))}



popSingleLinkedStack : Meta @$\rightarrow$@ Meta
popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
  where
    n = Meta.nextCS m
    con  = Meta.context m
    elem : Meta @$\rightarrow$@ Maybe A
    elem record {stack = record { top = (just (cons x _)) }} = just x
    elem record {stack = record { top = nothing           }} = nothing
    st : Meta @$\rightarrow$@ SingleLinkedStack A
    st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
    st record {stack = record { top = nothing           }} = record {top = nothing}
   



pushSingleLinkedStackCS : M.CodeSegment Meta Meta
pushSingleLinkedStackCS = M.cs pushSingleLinkedStack

popSingleLinkedStackCS : M.CodeSegment Meta Meta
popSingleLinkedStackCS = M.cs popSingleLinkedStack


-- for sample

firstContext : Context
firstContext = record {element = nothing ; n = 0}


firstMeta : Meta 
firstMeta = record { context = firstContext
                   ; stack = emptySingleLinkedStack
                   ; nextCS = (N.cs (\m @$\rightarrow$@ m))
                   }