Mercurial > hg > Members > atton > agda-proofs
diff cbc/stack-subtype.agda @ 56:ddcd652969e0
Add executable subtype-stack
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 11 Jan 2017 20:11:01 +0000 |
parents | 81c6779583b6 |
children | bd428bd6b394 |
line wrap: on
line diff
--- a/cbc/stack-subtype.agda Wed Jan 11 13:37:23 2017 +0000 +++ b/cbc/stack-subtype.agda Wed Jan 11 20:11:01 2017 +0000 @@ -97,49 +97,11 @@ popSingleLinkedStackCS = M.cs popSingleLinkedStack - - - --- sample - -record Num : Set where - field - num : ℕ +-- for sample -instance - NumIsNormalDataSegment : N.DataSegment Num - NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c}) - ; set = (\c n -> record c {n = Num.num n})} - - -plus3 : Num -> Num -plus3 record { num = n } = record {num = n + 3} - -plus3CS : N.CodeSegment Num Num -plus3CS = N.cs plus3 +firstContext : Context +firstContext = record { element = nothing ; n = 0} -setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}} - -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context) -setNext c = M.cs (\mc -> record mc {nextCS = liftContext c}) - -setElement : A -> M.CodeSegment (MetaContext Context) (MetaContext Context) -setElement x = M.cs (\mc -> record mc {context = record (MetaContext.context mc) {element = just x}}) - -pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context) -pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS) - -plus5AndPush : {mc : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} - -> M.CodeSegment Num (MetaContext Context) -plus5AndPush {mc} {{nn}} = M.cs (\n -> record {context = con ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) - where - con = MetaContext.context mc - st = MetaContext.stack mc - - -push-sample : {{_ : M.DataSegment Num}} -> MetaContext Context -push-sample = M.exec (plus5AndPush {mc}) mc - where - con = record { n = 4 ; element = nothing} - code = N.cs (\c -> c) - mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} +firstMetaContext : MetaContext Context +firstMetaContext = record {stack = emptySingleLinkedStack ; nextCS = (N.cs (\m -> m)) ; context = firstContext}