Mercurial > hg > Papers > 2019 > oshiro-thesis
changeset 16:2a59b68bb2f3
remove srcdir
| author | e155702 |
|---|---|
| date | Mon, 18 Feb 2019 01:47:44 +0900 |
| parents | 0246ab5f42f7 |
| children | 7d2b1d8309ba |
| files | final_main/src/AgdaBasics.agda final_main/src/AgdaBasics.agda.replaced final_main/src/AgdaBool.agda final_main/src/AgdaDebug.agda final_main/src/AgdaDebug.agdai final_main/src/AgdaElem.agda final_main/src/AgdaElemApply.agda final_main/src/AgdaFunction.agda final_main/src/AgdaId.agda final_main/src/AgdaImplicitId.agda final_main/src/AgdaImport.agda final_main/src/AgdaInstance.agda final_main/src/AgdaInterface.agda final_main/src/AgdaInterface.agda.replaced final_main/src/AgdaInterface.agdai final_main/src/AgdaLambda.agda final_main/src/AgdaModusPonens.agda final_main/src/AgdaNPushNPop.agda final_main/src/AgdaNPushNPopProof.agda final_main/src/AgdaNat.agda final_main/src/AgdaNot.agda final_main/src/AgdaParameterizedModule.agda final_main/src/AgdaPattern.agda final_main/src/AgdaPlus.agda final_main/src/AgdaProduct.agda final_main/src/AgdaProp.agda final_main/src/AgdaPushPop.agda final_main/src/AgdaPushPopProof.agda final_main/src/AgdaRecord.agda final_main/src/AgdaRecordProj.agda final_main/src/AgdaSingleLinkedStack.agda final_main/src/AgdaSingleLinkedStack.agda.replaced final_main/src/AgdaStack.agda final_main/src/AgdaStackDS.agda final_main/src/AgdaStackImpl.agda final_main/src/AgdaStackImpl.agda.replaced final_main/src/AgdaStackSomeState.agda final_main/src/AgdaStackSomeState.agda.replaced final_main/src/AgdaStackTest.agda final_main/src/AgdaStackTest.agda.replaced final_main/src/AgdaStackTest.agdai final_main/src/AgdaTree.Agda final_main/src/AgdaTree.agda.replaced final_main/src/AgdaTreeDebug.agda final_main/src/AgdaTreeDebug.agda.replaced final_main/src/AgdaTreeDebugReturnNode4.agda final_main/src/AgdaTreeImpl.agda final_main/src/AgdaTreeImpl.agda.replaced final_main/src/AgdaTreeProof.agda final_main/src/AgdaTreeProof.agda.replaced final_main/src/AgdaTreeTest.agda final_main/src/AgdaTypeClass.agda final_main/src/AgdaWhere.agda final_main/src/CodeSegment.agda final_main/src/CodeSegment.agda.replaced final_main/src/CodeSegments.agda final_main/src/DataSegment.agda final_main/src/DataSegment.agda.replaced final_main/src/Eq.Agda final_main/src/Equiv.agda final_main/src/Exec.agda final_main/src/Goto.agda final_main/src/Goto.agda.replaced final_main/src/Maybe.agda final_main/src/MetaCodeSegment.agda final_main/src/MetaDataSegment.agda final_main/src/MetaMetaCodeSegment.agda final_main/src/MetaMetaDataSegment.agda final_main/src/Nat.agda final_main/src/NatAdd.agda final_main/src/NatAddSym.agda final_main/src/PushPopType.agda final_main/src/Reasoning.agda final_main/src/RedBlackTree.agda final_main/src/RedBlackTree.agdai final_main/src/SingleLinkedStack.cbc final_main/src/ThreePlusOne.agda final_main/src/akashaContext.h final_main/src/akashaMeta.c final_main/src/assert.c final_main/src/atton-master-meta-sample.agda final_main/src/atton-master-sample.agda final_main/src/cbmc-assert.c final_main/src/context.h final_main/src/enumerate-inputs.c final_main/src/escape_agda.rb final_main/src/expr-term.txt final_main/src/factrial.cbc final_main/src/getMinHeight.c final_main/src/goto.cbc final_main/src/initLLRBContext.c final_main/src/insertCase2.c final_main/src/interface.cbc final_main/src/meta.c final_main/src/rbtreeContext.h final_main/src/redBlackTreeTest.agda final_main/src/singleLinkedStack.c final_main/src/singleLinkedStackInterface.cbc final_main/src/stack-product.agda final_main/src/stack-subtype-sample.agda final_main/src/stack-subtype.agda final_main/src/stack.agda final_main/src/stack.agdai final_main/src/stack.h final_main/src/stackImpl.agda final_main/src/stackTest.agda final_main/src/stackTest.agdai final_main/src/struct-init.c final_main/src/struct.c final_main/src/stub.cbc final_main/src/subtype.agda final_main/src/type-cs.c final_main/src/type-ds.h final_main/src/type-mds.h |
| diffstat | 114 files changed, 0 insertions(+), 3042 deletions(-) [+] |
line wrap: on
line diff
--- a/final_main/src/AgdaBasics.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -module AgdaBasics where
--- a/final_main/src/AgdaBasics.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -module AgdaBasics where
--- a/final_main/src/AgdaBool.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Bool : Set where - true : Bool - false : Bool
--- a/final_main/src/AgdaDebug.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -open import Level renaming (suc to succ ; zero to Zero ) - -module AgdaDebug where - -open import stack - -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Data.Nat -open import Function - - -open SingleLinkedStack -open Stack - -testStack07 : {m : Level } -> Maybe (Element ℕ) -testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s -> pushSingleLinkedStack s 2 (\s -> top s)) - -testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 - $ \s -> pushSingleLinkedStack s 2 - $ \s -> pushSingleLinkedStack s 3 - $ \s -> pushSingleLinkedStack s 4 - $ \s -> pushSingleLinkedStack s 5 - $ \s -> top s - - -testStack10 = pushStack emptySingleLinkedStack 1 - $ \s -> pushStack 2 - $ \s -> pushStack 3 - $ \s -> pushStack 4 - $ \s -> pushStack 5 - $ \s -> top s
--- a/final_main/src/AgdaElem.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool -elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) -elem x [] = false
--- a/final_main/src/AgdaElemApply.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -listHas4 : Bool -listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true -
--- a/final_main/src/AgdaFunction.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -f : Bool -> Bool -f x = true
--- a/final_main/src/AgdaId.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -identity : (A : Set) -> A -> A -identity A x = x - -identity-zero : Nat -identity-zero = identity Nat zero
--- a/final_main/src/AgdaImplicitId.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -id : {A : Set} -> A -> A -id x = x - -id-zero : Nat -id-zero = id zero - -id' : {A : Set} -> A -> A -id' {A} x = x - -id-true : Bool -id-true = id {Bool} true
--- a/final_main/src/AgdaImport.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -import Data.Nat -- import module -import Data.Bool as B -- renamed module -import Data.List using (head) -- import Data.head function -import Level renaming (suc to S) -- import module with rename suc to S -import Data.String hiding (_++_) -- import module without _++_ -open import Data.List -- import and expand Data.List
--- a/final_main/src/AgdaInstance.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -_==Nat_ : Nat -> Nat -> Bool -zero ==Nat zero = true -(suc n) ==Nat zero = false -zero ==Nat (suc m) = false -(suc n) ==Nat (suc m) = n ==Nat m - -instance - natHas== : Eq Nat - natHas== = record { _==_ = _==Nat_}
--- a/final_main/src/AgdaInterface.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module AgdaInterface where - -data Maybe {n : Level } (a : Set n) : Set n where - Nothing : Maybe a - Just : a -> Maybe a - -record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where - field - push : stackImpl -> a -> (stackImpl -> t) -> t - pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t - pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - get : stackImpl -> (stackImpl -> Maybe a -> t) -> t - get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - clear : stackImpl -> (stackImpl -> t) -> t -open StackMethods - -record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where - field - stack : si - stackMethods : StackMethods {n} {m} a {t} si - pushStack : a -> (Stack a si -> t) -> t - pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - popStack : (Stack a si -> Maybe a -> t) -> t - popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack a si -> Maybe a -> t) -> t - getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si -> t) -> t - clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - -open Stack
--- a/final_main/src/AgdaInterface.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module AgdaInterface where - -data Maybe {n : Level } (a : Set n) : Set n where - Nothing : Maybe a - Just : a @$\rightarrow$@ Maybe a - -record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where - field - push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t - pop : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - get : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t -open StackMethods - -record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where - field - stack : si - stackMethods : StackMethods {n} {m} a {t} si - pushStack : a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t - pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } )) - popStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t - clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } )) - -open Stack
--- a/final_main/src/AgdaLambda.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -not-apply : Bool -> Bool -not-apply = (\b -> not b) -- use lambda - -not-apply : Bool -> Bool -not-appy b = not b -- not use lambda
--- a/final_main/src/AgdaModusPonens.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C) -f = \p x -> (snd p) ((fst p) x)
--- a/final_main/src/AgdaNPushNPop.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) - -n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) - -pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta - ≡ M.exec (n-push {meta} n) meta - where - meta = id-meta cn ce s
--- a/final_main/src/AgdaNPushNPopProof.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ -pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta - ≡ M.exec (n-push n) meta - where - meta = id-meta cn ce s - -pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s -pop-n-push zero cn ce s = refl -pop-n-push (suc n) cn ce s = begin - M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ - M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ - M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) - ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ - M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ - M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ refl ⟩ - M.exec (n-push n) (pushOnce (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push (suc n)) (id-meta cn ce s) - ∎ - - - -n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta - where - meta = id-meta cn ce st - -n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s -n-push-pop zero cn ce s = refl -n-push-pop (suc n) cn ce s = begin - M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) ⟩ - M.exec (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) - ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩ - M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ - M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) - ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ - M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) - ≡⟨ n-push-pop n cn ce s ⟩ - id-meta cn ce s - ∎
--- a/final_main/src/AgdaNat.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Nat : Set where - zero : Nat - suc : Nat -> Nat
--- a/final_main/src/AgdaNot.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -not : Bool -> Bool -not true = false -not false = true
--- a/final_main/src/AgdaParameterizedModule.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -module Sort (A : Set) (_<_ : A -> A -> Bool) where -sort : List A -> List A -sort = -- 実装は省略 ... - --- Parameterized Module により N.sort や B.sort が可能 -open import Sort Nat Nat._<_ as N -open import Sort Bool Bool._<_ as B
--- a/final_main/src/AgdaPattern.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -not : Bool -> Bool -not false = true -not x = false
--- a/final_main/src/AgdaPlus.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -_+_ : Nat -> Nat -> Nat -zero + m = m -suc n + m = suc (n + m)
--- a/final_main/src/AgdaProduct.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -data _×_ (A B : Set) : Set where - <_,_> : A -> B -> A × B - -fst : {A B : Set} -> A × B -> A -fst < a , _ > = a - -snd : {A B : Set} -> A × B -> B -snd < _ , b > = b
--- a/final_main/src/AgdaProp.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -prop : Bool -prop = true
--- a/final_main/src/AgdaPushPop.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -pushSingleLinkedStack : Meta -> Meta -pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) - where - n = Meta.nextCS m - s = Meta.stack m - e = Context.element (Meta.context m) - push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A - push s nothing = s - push s (just x) = record {top = just (cons x (top s))} - -popSingleLinkedStack : Meta -> Meta -popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) - where - n = Meta.nextCS m - con = Meta.context m - elem : Meta -> Maybe A - elem record {stack = record { top = (just (cons x _)) }} = just x - elem record {stack = record { top = nothing }} = nothing - st : Meta -> 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 Meta Meta -pushSingleLinkedStackCS = M.cs pushSingleLinkedStack - -popSingleLinkedStackCS : M.CodeSegment Meta Meta -popSingleLinkedStackCS = M.cs popSingleLinkedStack
--- a/final_main/src/AgdaPushPopProof.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta -id-meta n e s = record { context = record {n = n ; element = just e} - ; nextCS = (N.cs id) ; stack = s} - -push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ -push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta - where - meta = id-meta n e record {top = just (cons x (just s))} - -push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s -push-pop n e x s = refl
--- a/final_main/src/AgdaRecord.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -record Point : Set where - field - x : Nat - y : Nat - -makePoint : Nat -> Nat -> Point -makePoint a b = record { x = a ; y = b }
--- a/final_main/src/AgdaRecordProj.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -getX : Point -> Nat -getX p = Point.x p - -getY : Point -> Nat -getY record { x = a ; y = b} = b - -xPlus5 : Point -> Point -xPlus5 p = record p { x = (Point.x p) + 5}
--- a/final_main/src/AgdaSingleLinkedStack.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) -singleLinkedStackSpec = record { -push = pushSingleLinkedStack -; pop = popSingleLinkedStack -; pop2 = pop2SingleLinkedStack -; get = getSingleLinkedStack -; get2 = get2SingleLinkedStack -; clear = clearSingleLinkedStack -} - -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) -createSingleLinkedStack = record { -stack = emptySingleLinkedStack ; -stackMethods = singleLinkedStackSpec -} - --- Implementation - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t -pushSingleLinkedStack stack datum next = next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - - -popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t -popSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack1 (Just data1) - where - data1 = datum d - stack1 = record { top = (next d) } - -pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t -pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = pop2SingleLinkedStack' {n} {m} stack cs - where - pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t - pop2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1)) - - -getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t -getSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack (Just data1) - where - data1 = datum d - -get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t -get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = get2SingleLinkedStack' {n} {m} stack cs - where - get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t - get2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1)) - -clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t -clearSingleLinkedStack stack next = next (record {top = Nothing})
--- a/final_main/src/AgdaSingleLinkedStack.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a) -singleLinkedStackSpec = record { -push = pushSingleLinkedStack -; pop = popSingleLinkedStack -; pop2 = pop2SingleLinkedStack -; get = getSingleLinkedStack -; get2 = get2SingleLinkedStack -; clear = clearSingleLinkedStack -} - -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a) -createSingleLinkedStack = record { -stack = emptySingleLinkedStack ; -stackMethods = singleLinkedStackSpec -} - --- Implementation - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t -pushSingleLinkedStack stack datum next = next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - - -popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t -popSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack1 (Just data1) - where - data1 = datum d - stack1 = record { top = (next d) } - -pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t -pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = pop2SingleLinkedStack' {n} {m} stack cs - where - pop2SingleLinkedStack' : {n m : Level } {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t - pop2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1)) - - -getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t -getSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack (Just data1) - where - data1 = datum d - -get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t -get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = get2SingleLinkedStack' {n} {m} stack cs - where - get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t - get2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1)) - -clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t -clearSingleLinkedStack stack next = next (record {top = Nothing})
--- a/final_main/src/AgdaStack.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -data Element (a : Set) : Set where - cons : a -> Maybe (Element a) -> Element a - -datum : {a : Set} -> Element a -> a -datum (cons a _) = a - -next : {a : Set} -> Element a -> Maybe (Element a) -next (cons _ n) = n - -record SingleLinkedStack (a : Set) : Set where - field - top : Maybe (Element a) -
--- a/final_main/src/AgdaStackDS.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -record Context : Set where - field - -- fields for stack - element : Maybe A - - -open import subtype Context as N - -record Meta : Set₁ where - field - -- context as set of data segments - context : Context - stack : SingleLinkedStack A - nextCS : N.CodeSegment Context Context - -open import subtype Meta as M -
--- a/final_main/src/AgdaStackImpl.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -record SingleLinkedStack {n : Level } (a : Set n) : Set n where - field - top : Maybe (Element a) -open SingleLinkedStack - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t -pushSingleLinkedStack stack datum next = next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - --- Basic stack implementations are specifications of a Stack - -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) -singleLinkedStackSpec = record { - push = pushSingleLinkedStack - ; pop = popSingleLinkedStack - ; pop2 = pop2SingleLinkedStack - ; get = getSingleLinkedStack - ; get2 = get2SingleLinkedStack - ; clear = clearSingleLinkedStack - } - -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) -createSingleLinkedStack = record { - stack = emptySingleLinkedStack ; - stackMethods = singleLinkedStackSpec - }
--- a/final_main/src/AgdaStackImpl.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -record SingleLinkedStack {n : Level } (a : Set n) : Set n where - field - top : Maybe (Element a) -open SingleLinkedStack - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t -pushSingleLinkedStack stack datum next = next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - --- Basic stack implementations are specifications of a Stack - -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a) -singleLinkedStackSpec = record { - push = pushSingleLinkedStack - ; pop = popSingleLinkedStack - ; pop2 = pop2SingleLinkedStack - ; get = getSingleLinkedStack - ; get2 = get2SingleLinkedStack - ; clear = clearSingleLinkedStack - } - -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a) -createSingleLinkedStack = record { - stack = emptySingleLinkedStack ; - stackMethods = singleLinkedStackSpec - }
--- a/final_main/src/AgdaStackSomeState.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t} ( SingleLinkedStack D ) -stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec } - -push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -> -pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) )) -push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- a/final_main/src/AgdaStackSomeState.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) @$\rightarrow$@ Stack {l} {m} D {t} ( SingleLinkedStack D ) -stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec } - -push@$\rightarrow$@push@$\rightarrow$@pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) @$\rightarrow$@ pushStack (stackInSomeState s) x (\s1 @$\rightarrow$@ pushStack s1 y (\s2 @$\rightarrow$@ pop2Stack s2 (\s3 y1 x1 @$\rightarrow$@ - (Just x @$\equiv$@ x1) ∧ (Just y @$\equiv$@ y1)))) -push@$\rightarrow$@push@$\rightarrow$@pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- a/final_main/src/AgdaStackTest.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module AgdaStackTest where - -open import stack - -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Data.Nat -open import Function - - -open SingleLinkedStack -open Stack - - --- after push 1 and 2, pop2 get 1 and 2 - -testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m} -testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs) - - -testStack031 : (d1 d2 : ℕ ) -> Bool {Zero} -testStack031 2 1 = True -testStack031 _ _ = False - -testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero} -testStack032 (Just d1) (Just d2) = testStack031 d1 d2 -testStack032 _ _ = False - -testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m} -testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 ) - -testStack04 : Bool -testStack04 = testStack02 (\s -> testStack03 s testStack032) - -testStack05 : testStack04 ≡ True -testStack05 = refl
--- a/final_main/src/AgdaStackTest.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ --- after push 1 and 2, pop2 get 1 and 2 - -testStack02 : {m : Level } @$\rightarrow$@ ( Stack @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m} -testStack02 cs = pushStack createSingleLinkedStack 1 (\s @$\rightarrow$@ pushStack s 2 cs) - - -testStack031 : (d1 d2 : $\mathbb{N}$ ) @$\rightarrow$@ Bool {Zero} -testStack031 2 1 = True -testStack031 _ _ = False - -testStack032 : (d1 d2 : Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {Zero} -testStack032 (Just d1) (Just d2) = testStack031 d1 d2 -testStack032 _ _ = False - -testStack03 : {m : Level } @$\rightarrow$@ Stack @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ ((Maybe @$\mathbb{N}$@) @$\rightarrow$@ (Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m} -testStack03 s cs = pop2Stack s (\s d1 d2 @$\rightarrow$@ cs d1 d2 ) - -testStack04 : Bool -testStack04 = testStack02 (\s @$\rightarrow$@ testStack03 s testStack032) - -testStack05 : testStack04 @$\equiv$@ True -testStack05 = refl
--- a/final_main/src/AgdaTree.Agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where - field - putImpl : treeImpl -> a -> (treeImpl -> t) -> t - getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t -open TreeMethods - -record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where - field - tree : treeImpl - treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a -> (Tree treeImpl -> t) -> t - putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl -> Maybe a -> t) -> t - getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) - -open Tree -
--- a/final_main/src/AgdaTree.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where - field - putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t - getImpl : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t -open TreeMethods - -record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where - field - tree : treeImpl - treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t - putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d ) - -open Tree -
--- a/final_main/src/AgdaTreeDebug.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 - $ \t -> putTree1 t 2 2 - $ \t -> putTree1 t 3 3 - $ \t -> putTree1 t 4 4 - $ \t -> getRedBlackTree t 4 - $ \t x -> x - --- Just --- (record --- { key = 4 --- ; value = 4 --- ; right = Nothing --- ; left = Nothing --- ; color = Red --- })
--- a/final_main/src/AgdaTreeDebug.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1 - $ \t @$\rightarrow$@ putTree1 t 2 2 - $ \t @$\rightarrow$@ putTree1 t 3 3 - $ \t @$\rightarrow$@ putTree1 t 4 4 - $ \t @$\rightarrow$@ getRedBlackTree t 4 - $ \t x @$\rightarrow$@ x - --- Just --- (record --- { key = 4 --- ; value = 4 --- ; right = Nothing --- ; left = Nothing --- ; color = Red --- })
--- a/final_main/src/AgdaTreeDebugReturnNode4.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 -$ \t -> putTree1 t 2 2 -$ \t -> putTree1 t 3 3 -$ \t -> putTree1 t 4 4 -$ \t -> getRedBlackTree t 4 -$ \t x -> x - --- C-c C-n test31 return - -- Just - -- (record - -- { key = 4 - -- ; value = 4 - -- ; right = Nothing - -- ; left = Nothing - -- ; color = Red - -- })
--- a/final_main/src/AgdaTreeImpl.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -record Node {n : Level } (a k : Set n) : Set n where - inductive - field - key : k - value : a - right : Maybe (Node a k) - left : Maybe (Node a k) - color : Color {n} -open Node - -leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k -leafNode k1 value = record { - key = k1 ; - value = value ; - right = Nothing ; - left = Nothing ; - color = Red - } -open leafNode - -record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where - field - root : Maybe (Node a k) - nodeStack : SingleLinkedStack (Node a k) - compare : k -> k -> CompareResult {n} -open RedBlackTree - -putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t -putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) - --- 以下省略
--- a/final_main/src/AgdaTreeImpl.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where - field - putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t - getImpl : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t -open TreeMethods - -record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where - field - tree : treeImpl - treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t - putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d ) -open Tree - -record Node {n : Level } (a k : Set n) : Set n where - inductive - field - key : k - value : a - right : Maybe (Node a k) - left : Maybe (Node a k) - color : Color {n} -open Node - -leafNode : {n : Level } {a k : Set n} @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k -leafNode k1 value = record { - key = k1 ; - value = value ; - right = Nothing ; - left = Nothing ; - color = Red - } -record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where - field - root : Maybe (Node a k) - nodeStack : SingleLinkedStack (Node a k) - compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n} -open RedBlackTree - -putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t -putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next)) - --- 以下省略
--- a/final_main/src/AgdaTreeProof.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ -redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } - -putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) - -> (k : ℕ) (x : ℕ) - -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x - (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True)) -putTest1 n k x with n -... | Just n1 = lemma2 ( record { top = Nothing } ) - where - lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → - GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) - lemma2 s with compare2 k (key n1) - ... | EQ = lemma3 {!!} - where - lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { - key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black - } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) - lemma3 eq with compare2 x x | putTest1Lemma2 x - ... | EQ | refl with compare2 k (key n1) | eq - ... | EQ | refl with compare2 x x | putTest1Lemma2 x - ... | EQ | refl = refl - ... | GT = {!!} - ... | LT = {!!} - -... | Nothing = lemma1 - where - lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { - key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red - } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k - ( \ t x1 -> check2 x1 x ≡ True) - lemma1 with compare2 k k | putTest1Lemma2 k - ... | EQ | refl with compare2 x x | putTest1Lemma2 x - ... | EQ | refl = refl
--- a/final_main/src/AgdaTreeProof.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@ -redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } - -putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)) - @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@) - @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x - (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)) -putTest1 n k x with n -... | Just n1 = lemma2 ( record { top = Nothing } ) - where - lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → - GetRedBlackTree.checkNode t k (λ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t)) - lemma2 s with compare2 k (key n1) - ... | EQ = lemma3 {!!} - where - lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { - key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black - } ) ; nodeStack = s ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) - lemma3 eq with compare2 x x | putTest1Lemma2 x - ... | EQ | refl with compare2 k (key n1) | eq - ... | EQ | refl with compare2 x x | putTest1Lemma2 x - ... | EQ | refl = refl - ... | GT = {!!} - ... | LT = {!!} - -... | Nothing = lemma1 - where - lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { - key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red - } ) ; nodeStack = record { top = Nothing } ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k - ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) - lemma1 with compare2 k k | putTest1Lemma2 k - ... | EQ | refl with compare2 x x | putTest1Lemma2 x - ... | EQ | refl = refl
--- a/final_main/src/AgdaTreeTest.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 -$ \t -> putTree1 t 2 2 -$ \t -> putTree1 t 3 3 -$ \t -> putTree1 t 4 4 -$ \t -> getRedBlackTree t 4 -$ \t x -> x
--- a/final_main/src/AgdaTypeClass.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -record Eq (A : Set) : Set where - field - _==_ : A -> A -> Bool
--- a/final_main/src/AgdaWhere.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -f : Int -> Int -> Int -f a b c = (t a) + (t b) + (t c) - where - t x = x + x + x - -f' : Int -> Int -> Int -f' a b c = (a + a + a) + (b + b + b) + (c + c + c)
--- a/final_main/src/CodeSegment.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where - cs : (I -> O) -> CodeSegment I O
--- a/final_main/src/CodeSegment.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l @$\sqcup$@ l1 @$\sqcup$@ l2) where - cs : (I @$\rightarrow$@ O) @$\rightarrow$@ CodeSegment I O
--- a/final_main/src/CodeSegments.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -cs2 : CodeSegment ds1 ds1 -cs2 = cs id - -cs1 : CodeSegment ds1 ds1 -cs1 = cs (\d -> goto cs2 d) - -cs0 : CodeSegment ds0 ds1 -cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - -main : ds1 -main = goto cs0 (record {a = 100 ; b = 50}) -
--- a/final_main/src/DataSegment.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int
--- a/final_main/src/DataSegment.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int
--- a/final_main/src/Eq.Agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -module Eq where -open import Data.Nat -open import Data.Bool -open import Data.List - -record Eq (A : Set) : Set where - field - _==_ : A -> A -> Bool - -_==Nat_ : ℕ -> ℕ -> Bool -zero ==Nat zero = true -(suc n) ==Nat zero = false -zero ==Nat (suc m) = false -(suc n) ==Nat (suc m) = n ==Nat m - - -instance - _ : Eq ℕ - _ = record { _==_ = _==Nat_} - -_||_ : Bool -> Bool -> Bool -true || _ = true -false || x = x - -elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool -elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) -elem x [] = false - -listHas4 : Bool -listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true
--- a/final_main/src/Equiv.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x \ No newline at end of file
--- a/final_main/src/Exec.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} - {{_ : DataSegment I}} {{_ : DataSegment O}} - -> CodeSegment I O -> Context -> Context -exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) -
--- a/final_main/src/Goto.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} - -> CodeSegment I O -> I -> O -goto (cs b) i = b i -
--- a/final_main/src/Goto.agda.replaced Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} - @$\rightarrow$@ CodeSegment I O @$\rightarrow$@ I @$\rightarrow$@ O -goto (cs b) i = b i -
--- a/final_main/src/Maybe.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Maybe {a} (A : Set a) : Set a where - just : (x : A) -> Maybe A - nothing : Maybe A
--- a/final_main/src/MetaCodeSegment.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -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 -
--- a/final_main/src/MetaDataSegment.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -module subtype {l : Level} (Context : Set l) where - -record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where - field - get : Context -> A - set : Context -> A -> Context -
--- a/final_main/src/MetaMetaCodeSegment.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ --- meta level -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))) - -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 - -gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta -gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) - -push : M.CodeSegment Meta Meta -push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) - --- normal level - -cs2 : N.CodeSegment ds1 ds1 -cs2 = N.cs id - -cs1 : N.CodeSegment ds1 ds1 -cs1 = N.cs (\d -> N.goto cs2 d) - -cs0 : N.CodeSegment ds0 ds1 -cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - --- meta level (with extended normal) -main : Meta -main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) --- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)} -
--- a/final_main/src/MetaMetaDataSegment.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ --- 上で各 DataSegement の定義を行なっているとする -open import subtype Context as N -- Meta Datasegment を定義 - --- Meta DataSegment を持つ Meta Meta DataSegment を定義できる -record Meta : Set where - field - context : Context - c' : Int - next : N.CodeSegment Context Context - -open import subtype Meta as M --- 以下よりメタメタレベルのプログラムを記述できる
--- a/final_main/src/Nat.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -module nat where - -data Nat : Set where - O : Nat - S : Nat -> Nat \ No newline at end of file
--- a/final_main/src/NatAdd.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -open import nat -module nat_add where - -_+_ : Nat -> Nat -> Nat -O + m = m -(S n) + m = S (n + m) \ No newline at end of file
--- a/final_main/src/NatAddSym.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -open import Relation.Binary.PropositionalEquality -open import nat -open import nat_add -open ≡-Reasoning - -module nat_add_sym where - -addSym : (n m : Nat) -> n + m ≡ m + n -addSym O O = refl -addSym O (S m) = cong S (addSym O m) -addSym (S n) O = cong S (addSym n O) -addSym (S n) (S m) = {!!} -- 後述
--- a/final_main/src/PushPopType.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -pushOnce : Meta -> Meta -pushOnce m = M.exec pushSingleLinkedStackCS m - -popOnce : Meta -> Meta -popOnce m = M.exec popSingleLinkedStackCS m - -push-pop-type : Meta -> Set₁ -push-pop-type meta = - M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
--- a/final_main/src/Reasoning.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -open import Relation.Binary.PropositionalEquality -open import nat -open import nat_add -open ≡-Reasoning - -module nat_add_sym_reasoning where - -addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m) -addToRight O m = refl -addToRight (S n) m = cong S (addToRight n m) - -addSym : (n m : Nat) -> n + m ≡ m + n -addSym O O = refl -addSym O (S m) = cong S (addSym O m) -addSym (S n) O = cong S (addSym n O) -addSym (S n) (S m) = begin - (S n) + (S m) ≡⟨ refl ⟩ - S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩ - S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ - S (m + S n) ≡⟨ refl ⟩ - (S m) + (S n) ∎
--- a/final_main/src/RedBlackTree.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,231 +0,0 @@ -module RedBlackTree where - -open import stack -open import Level hiding (zero) -record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where - field - putImpl : treeImpl -> a -> (treeImpl -> t) -> t - getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t -open TreeMethods - -record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where - field - tree : treeImpl - treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a -> (Tree treeImpl -> t) -> t - putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl -> Maybe a -> t) -> t - getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) - -open Tree - -data Color {n : Level } : Set n where - Red : Color - Black : Color - -data CompareResult {n : Level } : Set n where - LT : CompareResult - GT : CompareResult - EQ : CompareResult - -record Node {n : Level } (a k : Set n) : Set n where - inductive - field - key : k - value : a - right : Maybe (Node a k) - left : Maybe (Node a k) - color : Color {n} -open Node - -record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where - field - root : Maybe (Node a k) - nodeStack : SingleLinkedStack (Node a k) - compare : k -> k -> CompareResult {n} - -open RedBlackTree - -open SingleLinkedStack - --- --- put new node at parent node, and rebuild tree to the top --- -{-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html -replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t -replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( - \s parent -> replaceNode1 s parent) - where - replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t - replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) - replaceNode1 s (Just n1) with compare tree (key n1) (key n0) - ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next - ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next - ... | LT = replaceNode tree s ( record n1 { right = Just n0 } ) next - - -rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t -rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext) - where - rotateRight1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t - rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 - ... | Nothing = rotateNext tree s Nothing n0 - ... | Just n1 with parent - ... | Nothing = rotateNext tree s (Just n1 ) n0 - ... | Just parent1 with left parent1 - ... | Nothing = rotateNext tree s (Just n1) Nothing - ... | Just leftParent with compare tree (key n1) (key leftParent) - ... | EQ = rotateNext tree s (Just n1) parent - ... | _ = rotateNext tree s (Just n1) parent - - -rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t -rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext) - where - rotateLeft1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t - rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 - ... | Nothing = rotateNext tree s Nothing n0 - ... | Just n1 with parent - ... | Nothing = rotateNext tree s (Just n1) Nothing - ... | Just parent1 with right parent1 - ... | Nothing = rotateNext tree s (Just n1) Nothing - ... | Just rightParent with compare tree (key n1) (key rightParent) - ... | EQ = rotateNext tree s (Just n1) parent - ... | _ = rotateNext tree s (Just n1) parent - -{-# TERMINATING #-} -insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t -insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next) - where - insertCase51 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k -> t) -> t - insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0 - ... | Nothing = next tree - ... | Just n1 with parent | grandParent - ... | Nothing | _ = next tree - ... | _ | Nothing = next tree - ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1 - ... | Nothing | _ = next tree - ... | _ | Nothing = next tree - ... | Just leftParent1 | Just leftGrandParent1 - with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1) - ... | EQ | EQ = rotateRight tree s n0 parent - (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) - ... | _ | _ = rotateLeft tree s n0 parent - (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) - -insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t -insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next - with (right parent) | (left grandParent) -... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next -... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next -... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) -... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent) - (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next)) -... | _ | _ = insertCase41 tree s n0 parent grandParent next - where - insertCase41 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t - insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next - with (left parent) | (right grandParent) - ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next - ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next - ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent) - ... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent) - (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next)) - ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next - -colorNode : {n : Level } {a k : Set n} -> Node a k -> Color -> Node a k -colorNode old c = record old { color = c } - -{-# TERMINATING #-} -insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t -insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0) - where - insertCase1 : Node a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion - -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html - insertCase3 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t - insertCase3 s n0 parent grandParent with left grandParent | right grandParent - ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next - ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next - ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) - ... | EQ = insertCase4 tree s n0 parent grandParent next - ... | _ with color uncle - ... | Red = pop2SingleLinkedStack s ( \s p0 p1 -> insertCase1 ( - record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s p0 p1 ) - ... | Black = insertCase4 tree s n0 parent grandParent next - insertCase2 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t - insertCase2 s n0 parent grandParent with color parent - ... | Black = replaceNode tree s n0 next - ... | Red = insertCase3 s n0 parent grandParent - insertCase1 n0 s Nothing Nothing = next tree - insertCase1 n0 s Nothing (Just grandParent) = next tree - insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next - insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent - ----- --- find node potition to insert or to delete, the path will be in the stack --- -findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t -findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1) - where - findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t - findNode2 s Nothing = next tree s n0 - findNode2 s (Just n) = findNode tree s n0 n next - findNode1 : SingleLinkedStack (Node a k) -> (Node a k) -> t - findNode1 s n1 with (compare tree (key n0) (key n1)) - ... | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) ) - ... | GT = findNode2 s (right n1) - ... | LT = findNode2 s (left n1) - - -leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k -leafNode k1 value = record { - key = k1 ; - value = value ; - right = Nothing ; - left = Nothing ; - color = Red - } - -putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t -putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) - -getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t -getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree) - module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html - search : Node a k -> t - checkNode : Maybe (Node a k) -> t - checkNode Nothing = cs tree Nothing - checkNode (Just n) = search n - search n with compare tree k1 (key n) - search n | LT = checkNode (left n) - search n | GT = checkNode (right n) - search n | EQ = cs tree (Just n) - -open import Data.Nat hiding (compare) - -compareℕ : ℕ → ℕ → CompareResult {Level.zero} -compareℕ x y with Data.Nat.compare x y -... | less _ _ = LT -... | equal _ = EQ -... | greater _ _ = GT - -compare2 : (x y : ℕ ) -> CompareResult {Level.zero} -compare2 zero zero = EQ -compare2 (suc _) zero = GT -compare2 zero (suc _) = LT -compare2 (suc x) (suc y) = compare2 x y - - -createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ -createEmptyRedBlackTreeℕ {m} a {t} = record { - root = Nothing - ; nodeStack = emptySingleLinkedStack - ; compare = compare2 - } -
--- a/final_main/src/SingleLinkedStack.cbc Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -#include "../context.h" -#include "../origin_cs.h" -#include <stdio.h> - -// typedef struct SingleLinkedStack { -// struct Element* top; -// } SingleLinkedStack; - -Stack* createSingleLinkedStack(struct Context* context) { - struct Stack* stack = new Stack(); - struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack(); - stack->stack = (union Data*)singleLinkedStack; - singleLinkedStack->top = NULL; - stack->push = C_pushSingleLinkedStack; - stack->pop = C_popSingleLinkedStack; - stack->pop2 = C_pop2SingleLinkedStack; - stack->get = C_getSingleLinkedStack; - stack->get2 = C_get2SingleLinkedStack; - stack->isEmpty = C_isEmptySingleLinkedStack; - stack->clear = C_clearSingleLinkedStack; - return stack; -} - -void printStack1(union Data* data) { - struct Node* node = &data->Element.data->Node; - if (node == NULL) { - printf("NULL"); - } else { - printf("key = %d ,", node->key); - printStack1((union Data*)data->Element.next); - } -} - -void printStack(union Data* data) { - printStack1(data); - printf("\n"); -} - -__code clearSingleLinkedStack(struct SingleLinkedStack* stack,__code next(...)) { - stack->top = NULL; - goto next(...); -} - -__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { - Element* element = new Element(); - element->next = stack->top; - element->data = data; - stack->top = element; - goto next(...); -} - -__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { - if (stack->top) { - data = stack->top->data; - stack->top = stack->top->next; - } else { - data = NULL; - } - goto next(data, ...); -} - -__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { - if (stack->top) { - data = stack->top->data; - stack->top = stack->top->next; - } else { - data = NULL; - } - if (stack->top) { - data1 = stack->top->data; - stack->top = stack->top->next; - } else { - data1 = NULL; - } - goto next(data, data1, ...); -} - - -__code getSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { - if (stack->top) - data = stack->top->data; - else - data = NULL; - goto next(data, ...); -} - -__code get2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { - if (stack->top) { - data = stack->top->data; - if (stack->top->next) { - data1 = stack->top->next->data; - } else { - data1 = NULL; - } - } else { - data = NULL; - data1 = NULL; - } - goto next(data, data1, ...); -} - -__code isEmptySingleLinkedStack(struct SingleLinkedStack* stack, __code next(...), __code whenEmpty(...)) { - if (stack->top) - goto next(...); - else - goto whenEmpty(...); -} - - -
--- a/final_main/src/ThreePlusOne.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -open import Relation.Binary.PropositionalEquality -open import nat -open import nat_add - -module three_plus_one where - -3+1 : (S (S (S O))) + (S O) ≡ (S (S (S (S O)))) -3+1 = refl \ No newline at end of file
--- a/final_main/src/akashaContext.h Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -// Data Segment -union Data { - struct Tree { /* ... 赤黒木の定義と同様 */ } tree; - struct Node { /* ... 赤黒木の定義と同様 */ } node; - - /* for verification */ - struct IterElem { - unsigned int val; - struct IterElem* next; - } iterElem; - struct Iterator { - struct Tree* tree; - struct Iterator* previousDepth; - struct IterElem* head; - struct IterElem* last; - unsigned int iteratedValue; - unsigned long iteratedPointDataNum; - void* iteratedPointHeap; - } iterator; - struct AkashaInfo { - unsigned int minHeight; - unsigned int maxHeight; - struct AkashaNode* akashaNode; - } akashaInfo; - struct AkashaNode { - unsigned int height; - struct Node* node; - struct AkashaNode* nextAkashaNode; - } akashaNode; -}; -
--- a/final_main/src/akashaMeta.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -__code meta(struct Context* context, enum Code next) { - struct Iterator* iter = &context->data[Iter]->iterator; - - switch (context->prev) { - case GoToPreviousDepth: - if (iter->iteratedPointDataNum == 0) break; - if (iter->iteratedPointHeap == NULL) break; - - unsigned int diff =(unsigned long)context->heap - (unsigned long)iter->iteratedPointHeap; - memset(iter->iteratedPointHeap, 0, diff); - context->dataNum = iter->iteratedPointDataNum; - context->heap = iter->iteratedPointHeap; - break; - default: - break; - } - switch (next) { - case PutAndGoToNextDepth: // with assert check - if (context->prev == GoToPreviousDepth) break; - if (iter->previousDepth == NULL) break; - iter->previousDepth->iteratedPointDataNum = context->dataNum; - iter->previousDepth->iteratedPointHeap = context->heap; - break; - default: - break; - } - - context->prev = next; - goto (context->code[next])(context); -} -
--- a/final_main/src/assert.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -__code verifySpecificationFinish(struct Context* context) { - if (context->data[AkashaInfo]->akashaInfo.maxHeight > 2*context->data[AkashaInfo]->akashaInfo.minHeight) { - context->next = Exit; - goto meta(context, ShowTrace); - } - goto meta(context, DuplicateIterator); -}
--- a/final_main/src/atton-master-meta-sample.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,77 +0,0 @@ -module atton-master-meta-sample where - -open import Data.Nat -open import Data.Unit -open import Function -Int = ℕ - -record Context : Set where - field - a : Int - b : Int - c : Int - -open import subtype Context as N - -record Meta : Set where - field - context : Context - c' : Int - next : N.CodeSegment Context Context - -open import subtype Meta as M - -instance - _ : N.DataSegment Context - _ = record { get = id ; set = (\_ c -> c) } - _ : M.DataSegment Context - _ = record { get = (\m -> Meta.context m) ; - set = (\m c -> record m {context = c}) } - _ : M.DataSegment Meta - _ = record { get = id ; set = (\_ m -> m) } - - -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))) - -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 - - -gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta -gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) - -push : M.CodeSegment Meta Meta -push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) - - -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int - -instance - _ : N.DataSegment ds0 - _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) - ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} - _ : N.DataSegment ds1 - _ = record { set = (\c d -> record c {c = (ds1.c d)}) - ; get = (\c -> record { c = (Context.c c)})} - -cs2 : N.CodeSegment ds1 ds1 -cs2 = N.cs id - -cs1 : N.CodeSegment ds1 ds1 -cs1 = N.cs (\d -> N.goto cs2 d) - -cs0 : N.CodeSegment ds0 ds1 -cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - - -main : Meta -main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) --- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
--- a/final_main/src/atton-master-sample.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,46 +0,0 @@ -module atton-master-sample where - -open import Data.Nat -open import Data.Unit -open import Function -Int = ℕ - -record Context : Set where - field - a : Int - b : Int - c : Int - - -open import subtype Context - - - -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int - -instance - _ : DataSegment ds0 - _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) - ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} - _ : DataSegment ds1 - _ = record { set = (\c d -> record c {c = (ds1.c d)}) - ; get = (\c -> record { c = (Context.c c)})} - -cs2 : CodeSegment ds1 ds1 -cs2 = cs id - -cs1 : CodeSegment ds1 ds1 -cs1 = cs (\d -> goto cs2 d) - -cs0 : CodeSegment ds0 ds1 -cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - -main : ds1 -main = goto cs0 (record {a = 100 ; b = 50})
--- a/final_main/src/cbmc-assert.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -void verifySpecification(struct Context* context, - struct Tree* tree) { - assert(!(maxHeight(tree->root, 1) > - 2*minHeight(tree->root, 1))); - return meta(context, EnumerateInputs); -} -
--- a/final_main/src/context.h Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -/* Context definition */ - -#define ALLOCATE_SIZE 1024 - -enum Code { - Code1, - Code2, - Allocator, -}; - -enum UniqueData { - Allocate, - Tree, -}; - -struct Context { - int codeNum; - __code (**code) (struct Context *); - void* heap_start; - void* heap; - long dataSize; - int dataNum; - union Data **data; -}; - -union Data { - struct Tree { - union Data* root; - union Data* current; - union Data* prev; - int result; - } tree; - struct Node { - int key; - int value; - enum Color { - Red, - Black, - } color; - union Data* left; - union Data* right; - } node; - struct Allocate { - long size; - enum Code next; - } allocate; -};
--- a/final_main/src/enumerate-inputs.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -void enumerateInputs(struct Context* context, - struct Node* node) { - if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) { - return meta(context, Exit); - } - - node->key = nondet_int(); - node->value = node->key; - context->next = VerifySpecification; - context->loopCount++; - - return meta(context, Put); -}
--- a/final_main/src/escape_agda.rb Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -#!/usr/bin/env ruby -# coding: utf-8 - -Suffix = '.agda.replaced' -EscapeChar = '@' -FileName = ARGV.first - -ReplaceTable = { - '->' => 'rightarrow', - '⊔' => 'sqcup', - '∷' => 'text{::}', - '∙' => 'circ', - '≡' => 'equiv', - '×' => 'times', - '⟨' => 'langle', - '⟩' => 'rangle', - '₁' => 'text{1}', - 'ℕ' => 'mathbb{N}', - '∎' => 'blacksquare' -} - -code = File.read(FileName) -ReplaceTable.each do |k, v| - escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar - code = code.gsub(k, escaped_str) -end - -File.write(FileName.sub(/.agda$/, Suffix), code)
--- a/final_main/src/expr-term.txt Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -t ::= - true - false - if t then t else t - 0 - succ t - pred t - iszero t
--- a/final_main/src/factrial.cbc Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -__code print_factorial(int prod) -{ - printf("factorial = %d\n", prod); - exit(0); -} - -__code factorial0(int prod, int x) -{ - if (x >= 1) { - goto factorial0(prod*x, x-1); - } else { - goto print_factorial(prod); - } - -} - -__code factorial(int x) -{ - goto factorial0(1, x); -} - -int main(int argc, char **argv) -{ - int i; - i = atoi(argv[1]); - - goto factorial(i); -} -
--- a/final_main/src/getMinHeight.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -__code getMinHeight_stub(struct Context* context) { - goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); -} - -__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { - const struct AkashaNode* akashaNode = akashaInfo->akashaNode; - - if (akashaNode == NULL) { - allocate->size = sizeof(struct AkashaNode); - allocator(context); - akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum]; - - akashaInfo->akashaNode->height = 1; - akashaInfo->akashaNode->node = context->data[Tree]->tree.root; - - goto getMaxHeight_stub(context); - } - - const struct Node* node = akashaInfo->akashaNode->node; - if (node->left == NULL && node->right == NULL) { - if (akashaInfo->minHeight > akashaNode->height) { - akashaInfo->minHeight = akashaNode->height; - akashaInfo->akashaNode = akashaNode->nextAkashaNode; - goto getMinHeight_stub(context); - } - } - - akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode; - - if (node->left != NULL) { - allocate->size = sizeof(struct AkashaNode); - allocator(context); - struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum]; - left->height = akashaNode->height+1; - left->node = node->left; - left->nextAkashaNode = akashaInfo->akashaNode; - akashaInfo->akashaNode = left; - } - - if (node->right != NULL) { - allocate->size = sizeof(struct AkashaNode); - allocator(context); - struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum]; - right->height = akashaNode->height+1; - right->node = node->right; - right->nextAkashaNode = akashaInfo->akashaNode; - akashaInfo->akashaNode = right; - } - - goto getMinHeight_stub(context); -}
--- a/final_main/src/goto.cbc Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -__code cs0(int a, int b){ - goto cs1(a+b); -} - -__code cs1(int c){ - goto cs2(c); -}
--- a/final_main/src/initLLRBContext.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -__code initLLRBContext(struct Context* context, int num) { - context->heapLimit = sizeof(union Data)*ALLOCATE_SIZE; - context->code = malloc(sizeof(__code*)*ALLOCATE_SIZE); - context->data = malloc(sizeof(union Data*)*ALLOCATE_SIZE); - context->heapStart = malloc(context->heapLimit); - - context->codeNum = Exit; - - context->code[Code1] = code1_stub; - context->code[Code2] = code2_stub; - context->code[Code3] = code3_stub; - context->code[Code4] = code4; - context->code[Code5] = code5; - context->code[Find] = find; - context->code[Not_find] = not_find; - context->code[Code6] = code6; - context->code[Put] = put_stub; - context->code[Replace] = replaceNode_stub; - context->code[Insert] = insertNode_stub; - context->code[RotateL] = rotateLeft_stub; - context->code[RotateR] = rotateRight_stub; - context->code[InsertCase1] = insert1_stub; - context->code[InsertCase2] = insert2_stub; - context->code[InsertCase3] = insert3_stub; - context->code[InsertCase4] = insert4_stub; - context->code[InsertCase4_1] = insert4_1_stub; - context->code[InsertCase4_2] = insert4_2_stub; - context->code[InsertCase5] = insert5_stub; - context->code[StackClear] = stackClear_stub; - context->code[Exit] = exit_code; - - context->heap = context->heapStart; - - context->data[Allocate] = context->heap; - context->heap += sizeof(struct Allocate); - - context->data[Tree] = context->heap; - context->heap += sizeof(struct Tree); - - context->data[Node] = context->heap; - context->heap += sizeof(struct Node); - - context->dataNum = Node; - - struct Tree* tree = &context->data[Tree]->tree; - tree->root = 0; - tree->current = 0; - tree->deleted = 0; - - context->node_stack = stack_init(sizeof(struct Node*), 100); - context->code_stack = stack_init(sizeof(enum Code), 100); -} -
--- a/final_main/src/insertCase2.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -__code insertCase2(struct Context* context, struct Node* current) { - struct Node* parent; - stack_pop(context->node_stack, &parent); - - if (parent->color == Black) { - stack_pop(context->code_stack, &context->next); - goto meta(context, context->next); - } - - stack_push(context->node_stack, &parent); - goto meta(context, InsertCase3); -} - -__code insert2_stub(struct Context* context) { - goto insertCase2(context, context->data[Tree]->tree.current); -} -
--- a/final_main/src/interface.cbc Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -typedef struct Stack<Type, Impl>{ - union Data* stack; - union Data* data; - union Data* data1; - - __code whenEmpty(...); - __code clear(Impl* stack,__code next(...)); - __code push(Impl* stack,Type* data, __code next(...)); - __code pop(Impl* stack, __code next(Type* data, ...)); - __code pop2(Impl* stack, __code next(Type* data, Type* data1, ...)); - __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); - __code get(Impl* stack, __code next(Type* data, ...)); - __code get2(Impl* stack, __code next(Type* data, Type* data1, ...)); - __code next(...); -} Stack;
--- a/final_main/src/meta.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -__code meta(struct Context* context, enum Code next) { - goto (context->code[next])(context); -} -
--- a/final_main/src/rbtreeContext.h Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -// DataSegments for Red-Black Tree -union Data { - struct Comparable { // interface - enum Code compare; - union Data* data; - } compare; - struct Count { - enum Code next; - long i; - } count; - struct Tree { - enum Code next; - struct Node* root; - struct Node* current; - struct Node* deleted; - int result; - } tree; - struct Node { - // need to tree - enum Code next; - int key; // comparable data segment - int value; - struct Node* left; - struct Node* right; - // need to balancing - enum Color { - Red, - Black, - } color; - } node; - struct Allocate { - enum Code next; - long size; - } allocate; -}; - - -// Meta DataSegment -struct Context { - enum Code next; - int codeNum; - __code (**code) (struct Context*); - void* heapStart; - void* heap; - long heapLimit; - int dataNum; - stack_ptr code_stack; - stack_ptr node_stack; - union Data **data; -};
--- a/final_main/src/redBlackTreeTest.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,196 +0,0 @@ -module redBlackTreeTest where - -open import RedBlackTree -open import stack -open import Level hiding (zero) - -open import Data.Nat - -open Tree -open Node -open RedBlackTree.RedBlackTree -open Stack - --- tests - -putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t -putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next)) - -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Function - - -check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} -check1 Nothing _ = False -check1 (Just n) x with Data.Nat.compare (value n) x -... | equal _ = True -... | _ = False - -check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} -check2 Nothing _ = False -check2 (Just n) x with compare2 (value n) x -... | EQ = True -... | _ = False - -test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True )) -test1 = refl - -test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( - \t -> putTree1 t 2 2 ( - \t -> getRedBlackTree t 1 ( - \t x -> check2 x 1 ≡ True ))) -test2 = refl - -open ≡-Reasoning -test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 - $ \t -> putTree1 t 2 2 - $ \t -> putTree1 t 3 3 - $ \t -> putTree1 t 4 4 - $ \t -> getRedBlackTree t 1 - $ \t x -> check2 x 1 ≡ True -test3 = begin - check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 - ≡⟨ refl ⟩ - True - ∎ - -test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 - $ \t -> putTree1 t 2 2 - $ \t -> putTree1 t 3 3 - $ \t -> putTree1 t 4 4 - $ \t -> getRedBlackTree t 4 - $ \t x -> x - --- test5 : Maybe (Node ℕ ℕ) -test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 - $ \t -> putTree1 t 6 6 - $ \t0 -> clearSingleLinkedStack (nodeStack t0) - $ \s -> findNode1 t0 s (leafNode 3 3) ( root t0 ) - $ \t1 s n1 -> replaceNode t1 s n1 - $ \t -> getRedBlackTree t 3 - -- $ \t x -> SingleLinkedStack.top (stack s) - -- $ \t x -> n1 - $ \t x -> root t - where - findNode1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t - findNode1 t s n1 Nothing next = next t s n1 - findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next - --- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> --- putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) --- test51 = refl - -test6 : Maybe (Node ℕ ℕ) -test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) - - -test7 : Maybe (Node ℕ ℕ) -test7 = clearSingleLinkedStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t)) - where - tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} - k1 = 1 - n2 = leafNode 0 0 - value1 = 1 - -test8 : Maybe (Node ℕ ℕ) -test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 - $ \t -> putTree1 t 2 2 (\ t -> root t) - - -test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True )) -test9 = refl - -test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( - \t -> putRedBlackTree t 2 2 ( - \t -> getRedBlackTree t 1 ( - \t x -> check2 x 1 ≡ True ))) -test10 = refl - -test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 - $ \t -> putRedBlackTree t 2 2 - $ \t -> putRedBlackTree t 3 3 - $ \t -> getRedBlackTree t 2 - $ \t x -> root t - - -redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ -redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } - --- compare2 : (x y : ℕ ) -> compareresult --- compare2 zero zero = eq --- compare2 (suc _) zero = gt --- compare2 zero (suc _) = lt --- compare2 (suc x) (suc y) = compare2 x y - -putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ -putTest1Lemma2 zero = refl -putTest1Lemma2 (suc k) = putTest1Lemma2 k - -putTest1Lemma1 : (x y : ℕ) -> compareℕ x y ≡ compare2 x y -putTest1Lemma1 zero zero = refl -putTest1Lemma1 (suc m) zero = refl -putTest1Lemma1 zero (suc n) = refl -putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n -putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m - where - lemma1 : (m : ℕ) -> LT ≡ compare2 m (ℕ.suc (m + k)) - lemma1 zero = refl - lemma1 (suc y) = lemma1 y -putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m - where - lemma1 : (m : ℕ) -> EQ ≡ compare2 m m - lemma1 zero = refl - lemma1 (suc y) = lemma1 y -putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m - where - lemma1 : (m : ℕ) -> GT ≡ compare2 (ℕ.suc (m + k)) m - lemma1 zero = refl - lemma1 (suc y) = lemma1 y - -putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ -putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) - -compareLemma1 : {x y : ℕ} -> compare2 x y ≡ EQ -> x ≡ y -compareLemma1 {zero} {zero} refl = refl -compareLemma1 {zero} {suc _} () -compareLemma1 {suc _} {zero} () -compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) ) - where - lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y - lemma2 = refl - - -putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) - -> (k : ℕ) (x : ℕ) - -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x - (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True)) -putTest1 n k x with n -... | Just n1 = lemma2 ( record { top = Nothing } ) - where - lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → - GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) - lemma2 s with compare2 k (key n1) - ... | EQ = lemma3 {!!} - where - lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { - key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black - } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) - lemma3 eq with compare2 x x | putTest1Lemma2 x - ... | EQ | refl with compare2 k (key n1) | eq - ... | EQ | refl with compare2 x x | putTest1Lemma2 x - ... | EQ | refl = refl - ... | GT = {!!} - ... | LT = {!!} - -... | Nothing = lemma1 - where - lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { - key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red - } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k - ( \ t x1 -> check2 x1 x ≡ True) - lemma1 with compare2 k k | putTest1Lemma2 k - ... | EQ | refl with compare2 x x | putTest1Lemma2 x - ... | EQ | refl = refl
--- a/final_main/src/singleLinkedStack.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { - Element* element = new Element(); - element->next = stack->top; - element->data = data; - stack->top = element; - goto next(...); -} - -__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { - if (stack->top) { - data = stack->top->data; - stack->top = stack->top->next; - } else { - data = NULL; - } - goto next(data, ...); -} -
--- a/final_main/src/singleLinkedStackInterface.cbc Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -Stack* createSingleLinkedStack(struct Context* context) { - struct Stack* stack = new Stack(); - struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack(); - stack->stack = (union Data*)singleLinkedStack; - singleLinkedStack->top = NULL; - stack->push = C_pushSingleLinkedStack; - stack->pop = C_popSingleLinkedStack; - stack->pop2 = C_pop2SingleLinkedStack; - stack->get = C_getSingleLinkedStack; - stack->get2 = C_get2SingleLinkedStack; - stack->isEmpty = C_isEmptySingleLinkedStack; - stack->clear = C_clearSingleLinkedStack; - return stack; -} \ No newline at end of file
--- a/final_main/src/stack-product.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,158 +0,0 @@ -module stack-product where - -open import product -open import Data.Product -open import Data.Nat -open import Function using (id) -open import Relation.Binary.PropositionalEquality - --- definition based from Gears(209:5708390a9d88) src/parallel_execution -goto = executeCS - -data Bool : Set where - True : Bool - False : Bool - -data Maybe (a : Set) : Set where - Nothing : Maybe a - Just : a -> Maybe a - - -record Stack {a t : Set} (stackImpl : Set) : Set where - field - stack : stackImpl - push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t - pop : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t - - -data Element (a : Set) : Set where - cons : a -> Maybe (Element a) -> Element a - -datum : {a : Set} -> Element a -> a -datum (cons a _) = a - -next : {a : Set} -> Element a -> Maybe (Element a) -next (cons _ n) = n - -record SingleLinkedStack (a : Set) : Set where - field - top : Maybe (Element a) -open SingleLinkedStack - -emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a -emptySingleLinkedStack = record {top = Nothing} - - - - -pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t -pushSingleLinkedStack = cs push - where - push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t - push (stack , datum , next) = goto next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - -popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) t -popSingleLinkedStack = cs pop - where - pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t - pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) - pop (record { top = Just x } , nextCS) = goto nextCS (stack1 , (Just datum1)) - where - datum1 = datum x - stack1 = record { top = (next x) } - - - - - -createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) -createSingleLinkedStack = record { stack = emptySingleLinkedStack - ; push = pushSingleLinkedStack - ; pop = popSingleLinkedStack - } - - - - -test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool -test01 = cs test01' - where - test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool - test01' (record { top = Nothing } , _) = False - test01' (record { top = Just x } , _) = True - - -test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a) -test02 = cs test02' - where - test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a) - test02' stack = goto popSingleLinkedStack (stack , (cs id)) - - -test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a) -test03 = cs test03' - where - test03' : {a : Set} -> a -> SingleLinkedStack a - test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id)) - - -lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False -lemma = refl - - -n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A) -n-push {A} {a} = cs (push {A} {a}) - 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 - - -{- - -n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A -n-push zero s = s -n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s) - -n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A -n-pop zero s = s -n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) - -open ≡-Reasoning - -push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s -push-pop-equiv s = refl - -push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s -push-and-n-pop zero s = refl -push-and-n-pop {A} {a} (suc n) s = begin - n-pop (suc (suc n)) (pushSingleLinkedStack s a id) - ≡⟨ refl ⟩ - popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) - ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩ - popSingleLinkedStack (n-pop n s) (\s _ -> s) - ≡⟨ refl ⟩ - n-pop (suc n) s - ∎ - - -n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s -n-push-pop-equiv zero s = refl -n-push-pop-equiv {A} {a} (suc n) s = begin - n-pop (suc n) (n-push (suc n) s) - ≡⟨ refl ⟩ - n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) - ≡⟨ push-and-n-pop n (n-push n s) ⟩ - n-pop n (n-push n s) - ≡⟨ n-push-pop-equiv n s ⟩ - s - ∎ - - -n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack -n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack --} -
--- a/final_main/src/stack-subtype-sample.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,212 +0,0 @@ -module stack-subtype-sample where - -open import Level renaming (suc to S ; zero to O) -open import Function -open import Data.Nat -open import Data.Maybe -open import Relation.Binary.PropositionalEquality - -open import stack-subtype ℕ -open import subtype Context as N -open import subtype Meta as M - - -record Num : Set where - field - num : ℕ - -instance - NumIsNormalDataSegment : N.DataSegment Num - NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c}) - ; set = (\c n -> record c {n = Num.num n})} - NumIsMetaDataSegment : M.DataSegment Num - NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)}) - ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})} - - -plus3 : Num -> Num -plus3 record { num = n } = record {num = n + 3} - -plus3CS : N.CodeSegment Num Num -plus3CS = N.cs plus3 - - - -plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}} - -> M.CodeSegment Num (Meta) -plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) - where - co = Meta.context mc - con : Num -> Context - con record { num = num } = N.DataSegment.set nn co record {num = num + 5} - st = Meta.stack mc - - - - -push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta -push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc - where - con = record { n = 4 ; element = just 0} - code = N.cs (\c -> c) - mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} - - -push-sample-equiv : push-sample ≡ record { nextCS = liftContext plus3CS - ; stack = record { top = nothing} - ; context = record { n = 9} } -push-sample-equiv = refl - - -pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta -pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc - where - con = record { n = 4 ; element = just 0} - code = N.cs (\c -> c) - mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} - - - -pushed-sample-equiv : {m : Meta} -> - pushed-sample {m} ≡ record { nextCS = liftContext plus3CS - ; stack = record { top = just (cons 0 nothing) } - ; context = record { n = 12} } -pushed-sample-equiv = refl - - - -pushNum : N.CodeSegment Context Context -pushNum = N.cs pn - where - pn : Context -> Context - pn record { n = n } = record { n = pred n ; element = just n} - - -pushOnce : Meta -> Meta -pushOnce m = M.exec pushSingleLinkedStackCS m - -n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) - -popOnce : Meta -> Meta -popOnce m = M.exec popSingleLinkedStackCS m - -n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) - - - -initMeta : ℕ -> Maybe ℕ -> N.CodeSegment Context Context -> Meta -initMeta n mn code = record { context = record { n = n ; element = mn} - ; stack = emptySingleLinkedStack - ; nextCS = code - } - -n-push-cs-exec = M.exec (n-push {meta} 3) meta - where - meta = (initMeta 5 (just 9) pushNum) - - -n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum - ; context = record {n = 2 ; element = just 3} - ; stack = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}} -n-push-cs-exec-equiv = refl - - -n-pop-cs-exec = M.exec (n-pop {meta} 4) meta - where - meta = record { nextCS = N.cs id - ; context = record { n = 0 ; element = nothing} - ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))} - } - -n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id - ; context = record { n = 0 ; element = just 6} - ; stack = record { top = just (cons 5 nothing)} - } - -n-pop-cs-exec-equiv = refl - - -open ≡-Reasoning - -id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta -id-meta n e s = record { context = record {n = n ; element = just e} - ; nextCS = (N.cs id) ; stack = s} - -exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m) -exec-comp (M.cs x) (M.cs _) m = refl - - -push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ -push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta - where - meta = id-meta n e record {top = just (cons x (just s))} - -push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s -push-pop n e x s = refl - - - -pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta - ≡ M.exec (n-push {meta} n) meta - where - meta = id-meta cn ce s - -pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s - -pop-n-push zero cn ce s = refl -pop-n-push (suc n) cn ce s = begin - M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ - M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ - M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) - ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ - M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ - M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ refl ⟩ - M.exec (n-push n) (pushOnce (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) - ∎ - - - -n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta - where - meta = id-meta cn ce st - -n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s -n-push-pop zero cn ce s = refl -n-push-pop (suc n) cn ce s = begin - M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s} (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp {id-meta cn ce s} (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) ⟩ - M.exec (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) - ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) ⟩ - M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (pop-n-push n cn ce s) ⟩ - M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) - ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ - M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) - ≡⟨ n-push-pop n cn ce s ⟩ - id-meta cn ce s - ∎ -
--- a/final_main/src/stack-subtype.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,123 +0,0 @@ -open import Level hiding (lift) -open import Data.Maybe -open import Data.Product -open import Data.Nat hiding (suc) -open import Function - -module stack-subtype (A : Set) where - --- data definitions - -data Element (a : Set) : Set where - cons : a -> Maybe (Element a) -> Element a - -datum : {a : Set} -> Element a -> a -datum (cons a _) = a - -next : {a : Set} -> Element a -> Maybe (Element a) -next (cons _ n) = n - -record SingleLinkedStack (a : Set) : Set where - field - top : Maybe (Element a) -open SingleLinkedStack - -record Context : Set where - field - -- fields for concrete data segments - n : ℕ - -- fields for stack - element : Maybe A - - - - - -open import subtype Context as N - -instance - ContextIsDataSegment : N.DataSegment Context - ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)} - - -record Meta : Set₁ where - field - -- context as set of data segments - context : Context - stack : SingleLinkedStack A - nextCS : N.CodeSegment Context Context - - - - -open import subtype Meta as M - -instance - MetaIncludeContext : M.DataSegment Context - MetaIncludeContext = record { get = Meta.context - ; set = (\m c -> record m {context = c}) } - - MetaIsMetaDataSegment : M.DataSegment Meta - MetaIsMetaDataSegment = 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 : Meta -> Meta -pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) - where - n = Meta.nextCS m - s = Meta.stack m - e = Context.element (Meta.context m) - push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A - push s nothing = s - push s (just x) = record {top = just (cons x (top s))} - - - -popSingleLinkedStack : Meta -> Meta -popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) - where - n = Meta.nextCS m - con = Meta.context m - elem : Meta -> Maybe A - elem record {stack = record { top = (just (cons x _)) }} = just x - elem record {stack = record { top = nothing }} = nothing - st : Meta -> 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 Meta Meta -pushSingleLinkedStackCS = M.cs pushSingleLinkedStack - -popSingleLinkedStackCS : M.CodeSegment Meta Meta -popSingleLinkedStackCS = M.cs popSingleLinkedStack - - --- for sample - -firstContext : Context -firstContext = record {element = nothing ; n = 0} - - -firstMeta : Meta -firstMeta = record { context = firstContext - ; stack = emptySingleLinkedStack - ; nextCS = (N.cs (\m -> m)) - } - - -
--- a/final_main/src/stack.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,149 +0,0 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module stack where - -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Data.Nat - -ex : 1 + 2 ≡ 3 -ex = refl - -data Bool {n : Level } : Set n where - True : Bool - False : Bool - -record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where - field - pi1 : a - pi2 : b - -data Maybe {n : Level } (a : Set n) : Set n where - Nothing : Maybe a - Just : a -> Maybe a - -record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where - field - push : stackImpl -> a -> (stackImpl -> t) -> t - pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t - pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - get : stackImpl -> (stackImpl -> Maybe a -> t) -> t - get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - clear : stackImpl -> (stackImpl -> t) -> t -open StackMethods - -record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where - field - stack : si - stackMethods : StackMethods {n} {m} a {t} si - pushStack : a -> (Stack a si -> t) -> t - pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - popStack : (Stack a si -> Maybe a -> t) -> t - popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack a si -> Maybe a -> t) -> t - getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si -> t) -> t - clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - -open Stack - -{-- -data Element {n : Level } (a : Set n) : Set n where - cons : a -> Maybe (Element a) -> Element a - - -datum : {n : Level } {a : Set n} -> Element a -> a -datum (cons a _) = a - -next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a) -next (cons _ n) = n ---} - - --- cannot define recrusive record definition. so use linked list with maybe. -record Element {l : Level} (a : Set l) : Set l where - inductive - constructor cons - field - datum : a -- `data` is reserved by Agda. - next : Maybe (Element a) - -open Element - - -record SingleLinkedStack {n : Level } (a : Set n) : Set n where - field - top : Maybe (Element a) -open SingleLinkedStack - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t -pushSingleLinkedStack stack datum next = next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - - -popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t -popSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack1 (Just data1) - where - data1 = datum d - stack1 = record { top = (next d) } - -pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t -pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = pop2SingleLinkedStack' {n} {m} stack cs - where - pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t - pop2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1)) - - -getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t -getSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack (Just data1) - where - data1 = datum d - -get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t -get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = get2SingleLinkedStack' {n} {m} stack cs - where - get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t - get2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1)) - -clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t -clearSingleLinkedStack stack next = next (record {top = Nothing}) - - -emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a -emptySingleLinkedStack = record {top = Nothing} - ------ --- Basic stack implementations are specifications of a Stack --- -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) -singleLinkedStackSpec = record { - push = pushSingleLinkedStack - ; pop = popSingleLinkedStack - ; pop2 = pop2SingleLinkedStack - ; get = getSingleLinkedStack - ; get2 = get2SingleLinkedStack - ; clear = clearSingleLinkedStack - } - -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) -createSingleLinkedStack = record { - stack = emptySingleLinkedStack ; - stackMethods = singleLinkedStackSpec - }
--- a/final_main/src/stack.h Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -struct SingleLinkedStack { - struct Element* top; -} SingleLinkedStack; -struct Element { - union Data* data; - struct Element* next; -} Element;
--- a/final_main/src/stackImpl.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -record Element {l : Level} (a : Set l) : Set l where - inductive - constructor cons - field - datum : a -- `data` is reserved by Agda. - next : Maybe (Element a) -open Element - -record SingleLinkedStack {n : Level } (a : Set n) : Set n where - field - top : Maybe (Element a) -open SingleLinkedStack - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t -pushSingleLinkedStack stack datum next = next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - --- push 以下は省略 - --- Basic stack implementations are specifications of a Stack - -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) -singleLinkedStackSpec = record { - push = pushSingleLinkedStack - ; pop = popSingleLinkedStack - ; pop2 = pop2SingleLinkedStack - ; get = getSingleLinkedStack - ; get2 = get2SingleLinkedStack - ; clear = clearSingleLinkedStack - } - -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) -createSingleLinkedStack = record { - stack = emptySingleLinkedStack ; - stackMethods = singleLinkedStackSpec - }
--- a/final_main/src/stackTest.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,144 +0,0 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module stackTest where - -open import stack - -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Data.Nat -open import Function - - -open SingleLinkedStack -open Stack - ----- --- --- proof of properties ( concrete cases ) --- - -test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n} -test01 stack _ with (top stack) -... | (Just _) = True -... | Nothing = False - - -test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool -test02 stack = popSingleLinkedStack stack test01 - -test03 : {n : Level } {a : Set n} -> a -> Bool -test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 - --- after a push and a pop, the stack is empty -lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False -lemma = refl - -testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m} -testStack01 v = pushStack createSingleLinkedStack v ( - \s -> popStack s (\s1 d1 -> True)) - --- after push 1 and 2, pop2 get 1 and 2 - -testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m} -testStack02 cs = pushStack createSingleLinkedStack 1 ( - \s -> pushStack s 2 cs) - - -testStack031 : (d1 d2 : ℕ ) -> Bool {Zero} -testStack031 2 1 = True -testStack031 _ _ = False - -testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero} -testStack032 (Just d1) (Just d2) = testStack031 d1 d2 -testStack032 _ _ = False - -testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m} -testStack03 s cs = pop2Stack s ( - \s d1 d2 -> cs d1 d2 ) - -testStack04 : Bool -testStack04 = testStack02 (\s -> testStack03 s testStack032) - -testStack05 : testStack04 ≡ True -testStack05 = refl - -testStack06 : {m : Level } -> Maybe (Element ℕ) -testStack06 = pushStack createSingleLinkedStack 1 ( - \s -> pushStack s 2 (\s -> top (stack s))) - -testStack07 : {m : Level } -> Maybe (Element ℕ) -testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 ( - \s -> pushSingleLinkedStack s 2 (\s -> top s)) - -testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 - $ \s -> pushSingleLinkedStack s 2 - $ \s -> pushSingleLinkedStack s 3 - $ \s -> pushSingleLinkedStack s 4 - $ \s -> pushSingleLinkedStack s 5 - $ \s -> top s - ------- --- --- proof of properties with indefinite state of stack --- --- this should be proved by properties of the stack inteface, not only by the implementation, --- and the implementation have to provides the properties. --- --- we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok. --- anyway some implementations may result s != s3 --- - -stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t} ( SingleLinkedStack D ) -stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec } - -push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -> - pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) )) -push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } - - --- id : {n : Level} {A : Set n} -> A -> A --- id a = a - --- push a, n times - -n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A -n-push zero s = s -n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) - -n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A -n-pop zero s = s -n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s ) - -open ≡-Reasoning - -push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s -push-pop-equiv s = refl - -push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {_} {A} {a} n s -push-and-n-pop zero s = refl -push-and-n-pop {_} {A} {a} (suc n) s = begin - n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id) - ≡⟨ refl ⟩ - popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) - ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ - popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s) - ≡⟨ refl ⟩ - n-pop {_} {A} {a} (suc n) s - ∎ - - -n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s -n-push-pop-equiv zero s = refl -n-push-pop-equiv {_} {A} {a} (suc n) s = begin - n-pop {_} {A} {a} (suc n) (n-push (suc n) s) - ≡⟨ refl ⟩ - n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) - ≡⟨ push-and-n-pop n (n-push n s) ⟩ - n-pop {_} {A} {a} n (n-push n s) - ≡⟨ n-push-pop-equiv n s ⟩ - s - ∎ - - -n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack -n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
--- a/final_main/src/struct-init.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -struct Point p = {100 , 200};
--- a/final_main/src/struct.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -struct Point { - int x; - int y; -};
--- a/final_main/src/stub.cbc Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -__code put(struct Context* context, - struct Tree* tree, - struct Node* root, - struct Allocate* allocate) -{ - /* 実装コードは省略 */ -} - -__code put_stub(struct Context* context) -{ - goto put(context, - &context->data[Tree]->tree, - context->data[Tree]->tree.root, - &context->data[Allocate]->allocate); -} - -
--- a/final_main/src/subtype.agda Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ -open import Level -open import Relation.Binary.PropositionalEquality - -module subtype {l : Level} (Context : Set l) where - - -record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where - field - get : Context -> A - set : Context -> A -> Context -open DataSegment - -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 - -goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O -goto (cs b) i = b i - -exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} - -> CodeSegment I O -> Context -> Context -exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) - - -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} -> {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) - = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f) - - - -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) - -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a -comp-associative (cs _) (cs _) (cs _) = refl
--- a/final_main/src/type-cs.c Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -__code getMinHeight_stub(struct Context* context) { - goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); -} - -__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { - /* ... */ - goto getMinHeight_stub(context); -} -
--- a/final_main/src/type-ds.h Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -struct AkashaInfo { - unsigned int minHeight; - unsigned int maxHeight; - struct AkashaNode* akashaNode; -};
--- a/final_main/src/type-mds.h Mon Feb 18 01:46:57 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -struct Data { /* data segments as types */ - struct Tree { /* ... */ } tree; - struct Node { /* ... */ } node; - - struct IterElem { /* ... */ } iterElem; - struct Iterator { /* ... */ } iterator; - struct AkashaInfo { /* ... */} akashaInfo; - struct AkashaNode { /* ... */} akashaNode; -}; - - -struct Context { /* meta data segment as subtype */ - /* ... fields for meta computations ... */ - struct Data **data; /* data segments */ -};