# HG changeset patch # User mir3636 # Date 1479295267 -32400 # Node ID 3fdb3334c7a946ad7ae3309186e47aca1d7b58b9 # Parent 7cd629c290509b2d2466e9aba04ab8c1fe20e0c7 fix stack.cbc diff -r 7cd629c29050 -r 3fdb3334c7a9 src/parallel_execution/stack.agda --- 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 diff -r 7cd629c29050 -r 3fdb3334c7a9 src/parallel_execution/stack.cbc --- 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 +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); }