changeset 54:fa95e3070138

Define SingleLinkedStack using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 11 Jan 2017 10:56:13 +0000
parents 6af88ee5c4ca
children 81c6779583b6
files cbc/stack-product.agda cbc/stack-subtype.agda cbc/subtype.agda
diffstat 3 files changed, 96 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/cbc/stack-product.agda	Tue Jan 10 09:07:07 2017 +0000
+++ b/cbc/stack-product.agda	Wed Jan 11 10:56:13 2017 +0000
@@ -108,7 +108,7 @@
   where
     push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
     push {A} {a} (zero  , s) = (zero , s)
-    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , ? {- n-push -}) -- needs subtype
 
 
 {-
--- a/cbc/stack-subtype.agda	Tue Jan 10 09:07:07 2017 +0000
+++ b/cbc/stack-subtype.agda	Wed Jan 11 10:56:13 2017 +0000
@@ -1,7 +1,7 @@
-open import Level
+open import Level hiding (lift)
 open import Data.Maybe
 open import Data.Product
-open import Data.Nat
+open import Data.Nat hiding (suc)
 
 module stack-subtype (A : Set) where
 
@@ -23,54 +23,109 @@
 
 record Context : Set where
   field
-    stack   : SingleLinkedStack A
     element : Maybe A
-    n       : ℕ 
+    n       : ℕ
 
-open import subtype Context
+
+open import subtype Context as N
 
 instance
-  ContextIsDataSegment : DataSegment Context
-  ContextIsDataSegment = record {get = (\x -> x) ; set = (\_ c -> c)}
+  ContextIsDataSegment : N.DataSegment Context
+  ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
+
+
+record MetaContext (X : Set) {{_ : N.DataSegment X}} : Set₁ where
+  field
+    context : Context
+    stack   : SingleLinkedStack A
+    nextCS  : N.CodeSegment X X
 
 
 
+
+open import subtype (MetaContext Context) as M
+
+instance
+  MetaContextIncludeContext : M.DataSegment Context
+  MetaContextIncludeContext = record { get = MetaContext.context
+                                     ; set = (\m c -> record m {context = c}) }
+
+  MetaContextIsMetaDataSegment : M.DataSegment (MetaContext Context)
+  MetaContextIsMetaDataSegment  = record { get = (\m -> m) ; set = (\_ m -> m) }
+
+
+liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
+liftMeta (N.cs f) = M.cs f
+
+liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
+liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> 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 : Context -> Context
-pushSingleLinkedStack c = record c { stack = (push c) ; element = nothing}
+
+pushSingleLinkedStack :  MetaContext Context -> MetaContext Context
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
   where
-    push : Context -> SingleLinkedStack A
-    push record { stack = stack ; element = nothing }  = stack
-    push record { stack = stack ; element = (just x) } = stack1
-      where
-        el = cons x (top stack)
-        stack1 = record {top = just el}
+    n = MetaContext.nextCS m
+    e = Context.element (MetaContext.context m)
+    s = MetaContext.stack   m
+    push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
+    push s nothing  = s
+    push s (just x) = record {top = just (cons x (top s))}
+
+
 
-popSingleLinkedStack : Context -> Context
-popSingleLinkedStack c = record c {element = (elem c) ; stack =  (popdStack c)}
+popSingleLinkedStack : MetaContext Context -> MetaContext Context
+popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
   where
-    elem : Context -> Maybe A
-    elem record { stack = record { top = (just (cons x _)) } } = just x
-    elem record { stack = record { top = nothing } }           = nothing
-    popdStack : Context -> SingleLinkedStack A
-    popdStack record { stack = record { top = (just (cons _ s)) } } = record { top = s }
-    popdStack record { stack = record { top = nothing } }           = record { top = nothing }
+    n = MetaContext.nextCS m
+    con  = MetaContext.context m
+    elem : MetaContext Context -> Maybe A
+    elem record {stack = record { top = (just (cons x _)) }} = just x
+    elem record {stack = record { top = nothing           }} = nothing
+    st : MetaContext Context -> 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 (MetaContext Context) (MetaContext Context)
+pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
+
+popSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
+popSingleLinkedStackCS = M.cs popSingleLinkedStack
+
+
+
+
 
 -- sample
 
+record Num : Set where
+  field
+    num : ℕ
 
-pushCS = cs pushSingleLinkedStack
-popCS  = cs popSingleLinkedStack
+instance
+  NumIsNormalDataSegment : N.DataSegment Num
+  NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
+                                  ; set = (\c n -> record c {n = Num.num n})}
 
 
--- stack
-record Stack {X Y : Set} (stackImpl : Set -> Set) : Set where
-  field
-    stack : stackImpl A
-    push  : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
-    pop   : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
+plus3 : Num -> Num
+plus3 record { num = n } = record {num = n + 3}
+
+plus3CS : N.CodeSegment Num Num
+plus3CS = N.cs plus3
+
 
+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})
+
+
+
+
+
+pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context)
+pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS)
--- a/cbc/subtype.agda	Tue Jan 10 09:07:07 2017 +0000
+++ b/cbc/subtype.agda	Wed Jan 11 10:56:13 2017 +0000
@@ -1,16 +1,16 @@
 open import Level
 open import Relation.Binary.PropositionalEquality
 
-module subtype (Context : Set) where
+module subtype {l : Level} (Context : Set l) where
 
 
-record DataSegment (A : Set) : Set where
+record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
   field
     get : Context -> A
     set : Context -> A -> Context
 open DataSegment
 
-data CodeSegment (A B : Set) : Set where
+data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
   cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
 
 
@@ -18,11 +18,14 @@
 exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
 
 
-comp : {con : Context} -> {A B C D : Set} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+comp : {con : Context} -> {l1 l2 l3 l4 : Level}
+       {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
+       {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
        -> (C -> D) -> (A -> B) -> A -> D
 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
 
-csComp : {con : Context} {A B C D : Set}
+csComp : {con : Context} -> {l1 l2 l3 l4 : Level}
+         {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
          {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
        -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
@@ -30,7 +33,7 @@
 
 
 
-comp-associative : {A B C D E F : Set} {con : Context}
+comp-associative : {A B C D E F : Set l} {con : Context}
                    {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
                    {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
                    -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)