Mercurial > hg > Papers > 2021 > soto-prosym
view Paper/src/stack-subtype.agda.replaced @ 5:339fb67b4375
INIT rbt.agda
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Nov 2021 00:51:16 +0900 |
parents | c59202657321 |
children |
line wrap: on
line source
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)) }