changeset 158:3fdb3334c7a9

fix stack.cbc
author mir3636
date Wed, 16 Nov 2016 20:21:07 +0900
parents 7cd629c29050
children f2c77b0761fc
files src/parallel_execution/stack.agda src/parallel_execution/stack.cbc
diffstat 2 files changed, 15 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Tue Nov 15 22:34:48 2016 +0900
+++ b/src/parallel_execution/stack.agda	Wed Nov 16 20:21:07 2016 +0900
@@ -28,13 +28,13 @@
     stack1  = record {top = just element}
 
 
-popSingleLinkedStack : {a : Set} -> Maybe a -> (Code : Stack -> (Maybe a) -> T) -> T
-popSingleLinkedStack stack data next with (top stack) =
+popSingleLinkedStack : {a : Set} -> Stack -> (Code : Stack -> (Maybe a) -> T) -> T
+popSingleLinkedStack stack next with (top  stack) =
   ... | nothing = next stack nothing
-  ... | just a  = next stack1 data1
+  ... | just d  = next stack1 data1
     where
-      data1 = data a
-      stack1 = record { top = (next a)}
+      data1 = data d
+      stack1 = record { top = (next d)}
 
 
 test01 : Stack -> Maybe a -> T
@@ -48,4 +48,4 @@
 test03 = push createSingleLinkedStack true test02
 
 lemma : test01 == false
-lemma = refl
\ No newline at end of file
+lemma = refl
--- a/src/parallel_execution/stack.cbc	Tue Nov 15 22:34:48 2016 +0900
+++ b/src/parallel_execution/stack.cbc	Wed Nov 16 20:21:07 2016 +0900
@@ -3,6 +3,10 @@
 #include "origin_cs.h"
 #include <stdio.h>
 
+typedef struct SingleLinkedStack {
+    struct Element* top;
+} SingleLinkedStack;
+
 Stack* createSingleLinkedStack() {
     struct Stack* stack = new Stack();
     struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
@@ -38,15 +42,6 @@
     goto next(...);
 }
 
-
-
-/* Stack -> Data -> (Code : Stack -> ?) -> ?
-  pushSingleLinkedStack stack data next = next stack1
-    where
-       element = record {next = top stack; data = data}
-       stack1  = record {top = just element}
-*/
-
 __code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) {
     Element* element = new Element();
     element->next = stack->top;
@@ -55,27 +50,18 @@
     goto next(...);
 }
 
-/* Stack Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
-  popSingleLinkedStack stack data next with (top stack) =
-  ... | nothing = next stack nothing
-  ... | just a  = next stack1 data1
-    where
-      data1 = data a
-      stack1 = record { top = (next a)}
-*/
-
-__code popSingleLinkedStack(struct SingleLinkedStack* stack, union Data** data, __code next(...)) {
+__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(..., union Data*)) {
+    union Data* data; 
     if (stack->top) {
         *data = stack->top->data;
         stack->top = stack->top->next;
     } else {
         *data = NULL;
     }
-    goto next(...);
-    // goto next(data, ...);
+    goto next(..., data);
 }
 
-__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, union Data** data, union Data** data1, __code next(...)) {
+__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, union Data** data, union Data** data1, __code next(..., union Data**, union Data**)) {
     if (stack->top) {
         *data = stack->top->data;
         stack->top = stack->top->next;
@@ -88,7 +74,7 @@
     } else {
         *data1 = NULL;
     }
-    goto next(...);
+    goto next(..., data, data1);
 }