# HG changeset patch # User Nozomi Teruya # Date 1515233223 -32400 # Node ID d7b8a5d1252fb345673ca1f49afd07f137dc39cb # Parent a2aaf1d0bf019738abe974307f0f7827a60ad41f remove file diff -r a2aaf1d0bf01 -r d7b8a5d1252f index.mm --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/index.mm Sat Jan 06 19:07:03 2018 +0900 @@ -0,0 +1,90 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/agda.tex --- a/paper/agda.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,629 +0,0 @@ -\chapter{証明支援系言語 Agda による証明手法} -\label{chapter:agda} -\ref{chapter:type}章ではCbCにおける CodeSegment と DataSegment が部分型で定義できることを示した。 - -型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。 -依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。 - -% {{{ 依存型を持つ証明支援系言語 Agda - -\section{依存型を持つ証明支援系言語 Agda} -型システムを用いて証明を行なうことができる言語に Agda~\cite{agda} が存在する。 -Agda は依存型という強力な型システムを持っている。 -依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述できる。 -この節では Agda の文法的な紹介を行なう~\cite{Norell:2009:DTP:1481861.1481862}~\cite{agda-documentation}。 - -Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。 -また、非常に多くの記号を利用できる言語であり、スペースの有無は厳格にチェックされる。 -なお、 \verb/--/ の後はコメントである。 - -まず、Agda のプログラムを記述するファイルを作成する。 -Agda のプログラムは全てモジュール内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。 -トップレベルのモジュールはファイル名と同一となる。 -例えば \verb/AgdaBasics.agda/ を作成する時のモジュール名はリスト~\ref{src:agda-module}のように定義する。 - -\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda.replaced} - -Agda における型指定は $:$ を用いて行なう。 -例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。 - -データ型は Haskell や ML に似た代数的なデータ構造である。 -データ型の定義は \verb/data/ キーワードを用いる。 -\verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。 -例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。 -Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。 -Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。 -Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。 - -\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced} - - -関数の定義は Haskell に近い。 -関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。 -関数の型は $ \rightarrow $ を用いる。 -なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。 -例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。 -Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 - -\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced} - -引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 -これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 -例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 - -\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} - -パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。 -例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 -なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 -例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 -なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。 - -\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced} - -関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。 -これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。 -例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。 -関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 - -\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda.replaced} - -Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。 -これは関数内部の冗長な記述を省略するのに活用できる。 -スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 -例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。 -これは \verb/f'/ と同様の動作をする。 -\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 - -\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} - - -データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。 -自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。 -例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。 - -\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced} - -自然数に対する演算は再帰関数として定義できる。 -例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。 - -この二項演算子は正確には中置関数である。 -前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置や後置演算子のように振る舞う。 -例えば \verb/!_/ 関数を定義すると \verb/! true/ のように利用でき、\verb/_~/ 関数を定義すると \verb/false ~/ のように利用できる。 - -また、Agda は再帰関数が停止するかを判定できる。 -この加算の二項演算子は左側がゼロに対しては明らかに停止する。 -左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。 -もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。 - -\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda.replaced} - -次に依存型について見ていく。 -依存型で最も基本的なものは関数型である。 -依存型を利用した関数は引数の型に依存して返す型を決定できる。 - -Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。 -ここで B の中で x を扱っても良い。 -例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。 - -\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda.replaced} - -この恒等関数 \verb/identitiy/ は任意の型に適用可能である。 -実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。 - -多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。 -Agda はこのような推論をサポートしており、推論可能な引数は省略できる。 -推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。 - -例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{src:agda-implicit-id}のようになる。 -この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。 -よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。 -なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。 -適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。 - -\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda.replaced} - -Agda には C における構造体に相当するレコード型も存在する。 -定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。 -例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。 -レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。 -複数の値を列挙する際は \verb/;/ で区切る。 - -\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced} - -構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。 -なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。 -また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。 -Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。 - -\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda.replaced} - -Agda における部分型のように振る舞う機能として Instance Arguments が存在する。 -これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。 -Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。 -例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。 -具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。 - -\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda.replaced} - -ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。 -型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。 - -\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda.replaced} - -これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。 -例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。 -部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。 -なお、名前部分は必須である。 -仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。 -部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。 - -\lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda.replaced} - -この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。 -Nat型の要素を持つリストの内部に4が含まれるか確認している。 -この \verb/listHas4/ は \verb/true/ に評価される。 - -\lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced} - -最後にモジュールについて述べる。 -モジュールはほとんど名前空間として作用する。 -なお、依存型の解決はモジュールのインポート時に行なわれる。 -モジュールをインポートする時は \verb/import/ キーワードを指定する。 -また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 -モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。 -なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。 -モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 - -\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced} - -また、モジュールには値を渡すことができる。 -そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。 -例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。 -そのモジュールは引数に型Aと二項演算子 \verb/ Bool -f x = true diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaId.agda --- a/paper/src/AgdaId.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaImplicitId.agda --- a/paper/src/AgdaImplicitId.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaImport.agda --- a/paper/src/AgdaImport.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaInstance.agda --- a/paper/src/AgdaInstance.agda Sat Jan 06 19:04:39 2018 +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_} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaLambda.agda --- a/paper/src/AgdaLambda.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaModusPonens.agda --- a/paper/src/AgdaModusPonens.agda Sat Jan 06 19:04:39 2018 +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) diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaNPushNPop.agda --- a/paper/src/AgdaNPushNPop.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaNPushNPopProof.agda --- a/paper/src/AgdaNPushNPopProof.agda Sat Jan 06 19:04:39 2018 +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 - ∎ diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaNat.agda --- a/paper/src/AgdaNat.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Nat : Set where - zero : Nat - suc : Nat -> Nat diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaNot.agda --- a/paper/src/AgdaNot.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -not : Bool -> Bool -not true = false -not false = true diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaParameterizedModule.agda --- a/paper/src/AgdaParameterizedModule.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaPattern.agda --- a/paper/src/AgdaPattern.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -not : Bool -> Bool -not false = true -not x = false diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaPlus.agda --- a/paper/src/AgdaPlus.agda Sat Jan 06 19:04:39 2018 +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) diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaProduct.agda --- a/paper/src/AgdaProduct.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaProp.agda --- a/paper/src/AgdaProp.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -prop : Bool -prop = true diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaPushPop.agda --- a/paper/src/AgdaPushPop.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaPushPopProof.agda --- a/paper/src/AgdaPushPopProof.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaRecord.agda --- a/paper/src/AgdaRecord.agda Sat Jan 06 19:04:39 2018 +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 } diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaRecordProj.agda --- a/paper/src/AgdaRecordProj.agda Sat Jan 06 19:04:39 2018 +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} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaStack.agda --- a/paper/src/AgdaStack.agda Sat Jan 06 19:04:39 2018 +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) - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaStackDS.agda --- a/paper/src/AgdaStackDS.agda Sat Jan 06 19:04:39 2018 +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 - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaTypeClass.agda --- a/paper/src/AgdaTypeClass.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/AgdaWhere.agda --- a/paper/src/AgdaWhere.agda Sat Jan 06 19:04:39 2018 +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) diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/CodeSegment.agda --- a/paper/src/CodeSegment.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/CodeSegments.agda --- a/paper/src/CodeSegments.agda Sat Jan 06 19:04:39 2018 +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}) - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/DataSegment.agda --- a/paper/src/DataSegment.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Eq.Agda --- a/paper/src/Eq.Agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Equiv.agda --- a/paper/src/Equiv.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Exec.agda --- a/paper/src/Exec.agda Sat Jan 06 19:04:39 2018 +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)) - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Goto.agda --- a/paper/src/Goto.agda Sat Jan 06 19:04:39 2018 +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 - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Maybe.agda --- a/paper/src/Maybe.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/MetaCodeSegment.agda --- a/paper/src/MetaCodeSegment.agda Sat Jan 06 19:04:39 2018 +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 - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/MetaDataSegment.agda --- a/paper/src/MetaDataSegment.agda Sat Jan 06 19:04:39 2018 +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 - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/MetaMetaCodeSegment.agda --- a/paper/src/MetaMetaCodeSegment.agda Sat Jan 06 19:04:39 2018 +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)} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/MetaMetaDataSegment.agda --- a/paper/src/MetaMetaDataSegment.agda Sat Jan 06 19:04:39 2018 +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 --- 以下よりメタメタレベルのプログラムを記述できる diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Nat.agda --- a/paper/src/Nat.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/NatAdd.agda --- a/paper/src/NatAdd.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/NatAddSym.agda --- a/paper/src/NatAddSym.agda Sat Jan 06 19:04:39 2018 +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) = {!!} -- 後述 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/PushPopType.agda --- a/paper/src/PushPopType.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/Reasoning.agda --- a/paper/src/Reasoning.agda Sat Jan 06 19:04:39 2018 +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) ∎ diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/SingleLinkedStack.cbc --- a/paper/src/SingleLinkedStack.cbc Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -#include "../context.h" -#include "../origin_cs.h" -#include - -// 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(...); -} - - - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/ThreePlusOne.agda --- a/paper/src/ThreePlusOne.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/akashaContext.h --- a/paper/src/akashaContext.h Sat Jan 06 19:04:39 2018 +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; -}; - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/akashaMeta.c --- a/paper/src/akashaMeta.c Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/assert.c --- a/paper/src/assert.c Sat Jan 06 19:04:39 2018 +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); -} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/atton-master-meta-sample.agda --- a/paper/src/atton-master-meta-sample.agda Sat Jan 06 19:04:39 2018 +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)} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/atton-master-sample.agda --- a/paper/src/atton-master-sample.agda Sat Jan 06 19:04:39 2018 +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}) diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/cbmc-assert.c --- a/paper/src/cbmc-assert.c Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/context.h --- a/paper/src/context.h Sat Jan 06 19:04:39 2018 +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; -}; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/enumerate-inputs.c --- a/paper/src/enumerate-inputs.c Sat Jan 06 19:04:39 2018 +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); -} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/expr-term.txt --- a/paper/src/expr-term.txt Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/factrial.cbc --- a/paper/src/factrial.cbc Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/getMinHeight.c --- a/paper/src/getMinHeight.c Sat Jan 06 19:04:39 2018 +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); -} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/goto.cbc --- a/paper/src/goto.cbc Sat Jan 06 19:04:39 2018 +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); -} diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/initLLRBContext.c --- a/paper/src/initLLRBContext.c Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/insertCase2.c --- a/paper/src/insertCase2.c Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/meta.c --- a/paper/src/meta.c Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/rbtreeContext.h --- a/paper/src/rbtreeContext.h Sat Jan 06 19:04:39 2018 +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; -}; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/singleLinkedStack.c --- a/paper/src/singleLinkedStack.c Sat Jan 06 19:04:39 2018 +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, ...); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/stack-product.agda --- a/paper/src/stack-product.agda Sat Jan 06 19:04:39 2018 +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 --} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/stack-subtype-sample.agda --- a/paper/src/stack-subtype-sample.agda Sat Jan 06 19:04:39 2018 +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 - ∎ - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/stack-subtype.agda --- a/paper/src/stack-subtype.agda Sat Jan 06 19:04:39 2018 +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)) - } - - - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/stack.h --- a/paper/src/stack.h Sat Jan 06 19:04:39 2018 +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; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/struct-init.c --- a/paper/src/struct-init.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -struct Point p = {100 , 200}; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/struct.c --- a/paper/src/struct.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -struct Point { - int x; - int y; -}; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/stub.cbc --- a/paper/src/stub.cbc Sat Jan 06 19:04:39 2018 +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); -} - - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/subtype.agda --- a/paper/src/subtype.agda Sat Jan 06 19:04:39 2018 +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 diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/type-cs.c --- a/paper/src/type-cs.c Sat Jan 06 19:04:39 2018 +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); -} - diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/type-ds.h --- a/paper/src/type-ds.h Sat Jan 06 19:04:39 2018 +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; -}; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/src/type-mds.h --- a/paper/src/type-mds.h Sat Jan 06 19:04:39 2018 +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 */ -}; diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/副本.pdf Binary file paper/副本.pdf has changed diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/正本.pdf Binary file paper/正本.pdf has changed diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/背表紙.pdf Binary file paper/背表紙.pdf has changed diff -r a2aaf1d0bf01 -r d7b8a5d1252f paper/表紙.pdf Binary file paper/表紙.pdf has changed