Mercurial > hg > Papers > 2018 > ryokka-thesis
changeset 2:93d26c4576d3
add picture
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/pic/modus-ponens.xbb Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,8 @@ +%%Title: modus-ponens.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 96 684 500 799 +%%HiResBoundingBox: 96.082030 683.554700 499.886700 799.296900 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Mon Jan 29 15:58:01 2018 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaBasics.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,1 @@ +module AgdaBasics where
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaBool.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +data Bool : Set where + true : Bool + false : Bool
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaElem.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaElemApply.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +listHas4 : Bool +listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaFunction.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,2 @@ +f : Bool -> Bool +f x = true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaId.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,5 @@ +identity : (A : Set) -> A -> A +identity A x = x + +identity-zero : Nat +identity-zero = identity Nat zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaImplicitId.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,11 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaImport.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,6 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaInstance.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,9 @@ +_==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_}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaLambda.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,5 @@ +not-apply : Bool -> Bool +not-apply = (\b -> not b) -- use lambda + +not-apply : Bool -> Bool +not-appy b = not b -- not use lambda
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaModusPonens.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,2 @@ +f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C) +f = \p x -> (snd p) ((fst p) x)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaNPushNPop.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,13 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaNPushNPopProof.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,58 @@ +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 + ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaNat.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +data Nat : Set where + zero : Nat + suc : Nat -> Nat
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaNot.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +not : Bool -> Bool +not true = false +not false = true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaParameterizedModule.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaPattern.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +not : Bool -> Bool +not false = true +not x = false
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaPlus.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +_+_ : Nat -> Nat -> Nat +zero + m = m +suc n + m = suc (n + m)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaProduct.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,8 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaProp.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,2 @@ +prop : Bool +prop = true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaPushPop.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,28 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaPushPopProof.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,11 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaRecord.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +record Point : Set where + field + x : Nat + y : Nat + +makePoint : Nat -> Nat -> Point +makePoint a b = record { x = a ; y = b }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaRecordProj.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,8 @@ +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}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaStack.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,13 @@ +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) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaStackDS.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,17 @@ +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 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaTypeClass.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +record Eq (A : Set) : Set where + field + _==_ : A -> A -> Bool
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaWhere.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/CodeSegment.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,2 @@ +data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where + cs : (I -> O) -> CodeSegment I O
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/CodeSegments.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,12 @@ +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}) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/DataSegment.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,8 @@ +record ds0 : Set where + field + a : Int + b : Int + +record ds1 : Set where + field + c : Int
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Eq.Agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,30 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Equiv.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,1 @@ +data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Exec.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,5 @@ +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)) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Goto.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,4 @@ +goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} + -> CodeSegment I O -> I -> O +goto (cs b) i = b i +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Maybe.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,3 @@ +data Maybe {a} (A : Set a) : Set a where + just : (x : A) -> Maybe A + nothing : Maybe A
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/MetaCodeSegment.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,4 @@ +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 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/MetaDataSegment.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +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 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/MetaMetaCodeSegment.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,29 @@ +-- 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)} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/MetaMetaDataSegment.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,12 @@ +-- 上で各 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 +-- 以下よりメタメタレベルのプログラムを記述できる
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Nat.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,5 @@ +module nat where + +data Nat : Set where + O : Nat + S : Nat -> Nat \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/NatAdd.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,6 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/NatAddSym.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,12 @@ +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) = {!!} -- 後述
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/PushPopType.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,9 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/Reasoning.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,21 @@ +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) ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/SingleLinkedStack.cbc Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,110 @@ +#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(...); +} + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/ThreePlusOne.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,8 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/akashaContext.h Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,31 @@ +// 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; +}; +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/akashaMeta.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,31 @@ +__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); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/assert.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +__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); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/atton-master-meta-sample.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,77 @@ +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)}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/atton-master-sample.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,46 @@ +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})
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/cbmc-assert.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +void verifySpecification(struct Context* context, + struct Tree* tree) { + assert(!(maxHeight(tree->root, 1) > + 2*minHeight(tree->root, 1))); + return meta(context, EnumerateInputs); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/context.h Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,47 @@ +/* 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; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/enumerate-inputs.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,13 @@ +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); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/expr-term.txt Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,8 @@ +t ::= + true + false + if t then t else t + 0 + succ t + pred t + iszero t
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/factrial.cbc Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,29 @@ +__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); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/getMinHeight.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,51 @@ +__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); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/goto.cbc Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +__code cs0(int a, int b){ + goto cs1(a+b); +} + +__code cs1(int c){ + goto cs2(c); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/initLLRBContext.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,53 @@ +__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); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/insertCase2.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,17 @@ +__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); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/meta.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,4 @@ +__code meta(struct Context* context, enum Code next) { + goto (context->code[next])(context); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/rbtreeContext.h Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,50 @@ +// 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; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/singleLinkedStack.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,18 @@ +__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, ...); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/stack-product.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,158 @@ +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 +-} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/stack-subtype-sample.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,212 @@ +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 + ∎ +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/stack-subtype.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,123 @@ +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)) + } + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/stack.h Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,7 @@ +struct SingleLinkedStack { + struct Element* top; +} SingleLinkedStack; +struct Element { + union Data* data; + struct Element* next; +} Element;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/struct-init.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,1 @@ +struct Point p = {100 , 200};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/struct.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,4 @@ +struct Point { + int x; + int y; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/stub.cbc Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,17 @@ +__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); +} + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/subtype.agda Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,44 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/type-cs.c Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,9 @@ +__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); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/type-ds.h Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,5 @@ +struct AkashaInfo { + unsigned int minHeight; + unsigned int maxHeight; + struct AkashaNode* akashaNode; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/type-mds.h Thu Feb 01 01:17:55 2018 +0900 @@ -0,0 +1,15 @@ +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 */ +};