Mercurial > hg > GearsTemplate
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); }