Skip to content

Commit 6c7776b

Browse files
kdxukdxu
committed
added LISENCE
1 parent f1a5c94 commit 6c7776b

File tree

3 files changed

+135
-10
lines changed

3 files changed

+135
-10
lines changed

‎LICENSE.txt

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
Copyright (c) 2015 Kyoko Kadowaki
2+
3+
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
13+
14+
The above copyright notice and this permission notice shall be included in
15+
all copies or substantial portions of the Software.
16+
17+
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
25+
THE SOFTWARE.
26+

‎README.ja.md

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
InferAgda
2+
=========
3+
Agdaによる'正当性が保証された'型推論器です。
4+
型推論のアルゴリズムとしてW-アルゴリズムを採用しています。
5+
6+
Agdaのインストール・セットアップ方法
7+
------
8+
9+
##1. cabal から Agda をインストール ##
10+
11+
```
12+
$ cabal install agda
13+
$ agda-mode setup
14+
```
15+
##2. agda-wiki から standard library をダウンロードする##
16+
17+
http://wiki.portal.chalmers.se/agda/pmwiki.php
18+
19+
##3. ダウンロードした standard library を aquamacsにセット##
20+
21+
+ open emacs
22+
+ `M-x load-library agda2-mode`
23+
+ `M-x customize-group agda2`
24+
+ specify "Agda include dirs" e.g. `/users/kyoko/agda-stdlib/src`
25+
+ select `Save for Future Sessions`
26+
27+
you can compile and load agda file with `C-c C-l`.
28+
29+
30+
このソースコードの構造
31+
-----
32+
33+
このソースコードは、`infer.agda`、`term.agda`、`mgu.agda`の三つから構成されています。
34+
それぞれの役割は以下のとおりです。
35+
36+
## infer.agda
37+
38+
## term.agda
39+
40+
このモジュールでは、型推論を行う well-scoped な term と well-typed な term を定義しています。
41+
42+
### well-scoped term
43+
44+
the word 'well-scoped' implies all terms have a parameter `n` that counts
45+
free variables with type level.(a simple example of dependant types)
46+
47+
#### definition
48+
49+
WellScopedTerm n :=
50+
Var : Fin n → WellScopedTerm n
51+
Lam : (s : WellScopedTerm (suc n)) WellScopedTerm n
52+
App : (s1 : WellScopedTerm n) (s2 : WellScopedTerm n) WellScopedTerm n
53+
Fst : WellScopedTerm n WellScopedTerm n
54+
Snd : WellScopedTerm n WellScopedTerm n
55+
Cons : WellScopedTerm n WellScopedTerm n WellScopedTerm nm (suc n)) → WellScopedTerm n
56+
App : (s1 : WellScopedTerm n) → (s2 : WellScopedTerm n) → WellScopedTerm n
57+
Fst : WellScopedTerm n → WellScopedTerm n
58+
Snd : WellScopedTerm n → WellScopedTerm n
59+
Cons : WellScopedTerm n → WellScopedTerm n → WellScopedTerm n
60+
61+
note: the type `Fin n` explains 'finite set', has a finite set of 0 ~ n-1.
62+
63+
64+
### well-typed term
65+
66+
this term has two parameters with type level, type context and type.
67+
so, this term is certified that has correct type `t` with the context `Γ `.
68+
69+
#### definition
70+
71+
WellTypedTerm (Γ : Cxt n) (t : Type m) :=
72+
Var : (x : Fin n) → WellTypedTerm Γ (lookup x Γ)
73+
Lam : (t : Type m) → {t' : Type m} → WellTypedTerm (t ∷ Γ) t' →
74+
WellTypedTerm Γ (t ⇒ t')
75+
App : {t t' : Type m} → WellTypedTerm Γ (t ⇒ t') → WellTypedTerm Γ t →
76+
WellTypedTerm Γ t'
77+
Fst : {t1 t2 : Type m} → WellTypedTerm Γ (t1 ∏ t2) → WellTypedTerm Γ t1
78+
Snd : {t1 t2 : Type m} → WellTypedTerm Γ (t1 ∏ t2) → WellTypedTerm Γ t2
79+
Cons : {t1 t2 : Type m} → WellTypedTerm Γ t1 → WellTypedTerm Γ t2 → WellTypedTerm Γ (t1 ∏ t2)
80+
81+
the type `Type` is discribed in the module mgu.
82+
83+
## mgu.agda
84+
85+
86+
型推論とその定式化の仕組み
87+
-----
88+
89+
90+
License
91+
-----
92+
MIT

‎README.md

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,30 +3,32 @@ InferAgda
33
The certified type-inference by agda.
44
We use W-algorithm for type inference algorithm.
55

6-
# how to setup agda
6+
how to setup agda
7+
------
78

8-
##1. install agda from cabal.
9+
##1. install agda from cabal. ##
910

1011
```
1112
$ cabal install agda
1213
$ agda-mode setup
1314
```
14-
##2. download a standard library from agda-wiki.
15+
##2. download a standard library from agda-wiki.##
1516

1617
http://wiki.portal.chalmers.se/agda/pmwiki.php
1718

18-
##3. apply agda standard library dirs.
19+
##3. apply agda standard library dirs.##
1920

20-
open emacs
21-
`M-x load-library agda2-mode`
22-
`M-x customize-group agda2`
23-
specify "Agda include dirs" e.g. `/users/kyoko/agda-stdlib/src`
24-
select `Save for Future Sessions`
21+
+ open emacs
22+
+ `M-x load-library agda2-mode`
23+
+ `M-x customize-group agda2`
24+
+ specify "Agda include dirs" e.g. `/users/kyoko/agda-stdlib/src`
25+
+ select `Save for Future Sessions`
2526

2627
you can compile and load agda file with `C-c C-l`.
2728

2829

29-
# structures
30+
structures
31+
-----
3032

3133
## infer.agda
3234

@@ -77,3 +79,8 @@ WellTypedTerm (Γ : Cxt n) (t : Type m) :=
7779
the type `Type` is discribed in the module mgu.
7880

7981
## mgu.agda
82+
83+
84+
License
85+
-----
86+
MIT

0 commit comments

Comments
 (0)