-
Notifications
You must be signed in to change notification settings - Fork 0
/
rules.txt
25 lines (22 loc) · 4.03 KB
/
rules.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
A |- c :: a B |- t :: b C |- e :: c
--------------------------------------------------------------------------------------------------------------------------------- [COND]
merge(A, B, C)[unif(Bool, a)][unif(b, c)] |- if c then t else e :: b[unif(A, B)][unif(merge(A, B), C)][unif(Bool, a)][unif(b, c)]
------------------- a is a new f.v. [IDENT]
{}.x :: a |- x :: a
A |- f :: a B |- es :: bs
------------------------------------------------------------- c is a new f.v. [APPLY]
merge(A, B)[unif(bs -> c, a)] |- f(es) :: c[unif(bs -> c, a)]
------------------------- ---------------------
{}.tail :: l |- tail :: l {}.xs :: m |- xs :: m
------------------------- --------------------- ------------------- -----------------------------------------------
{}.head :: f |- head :: f {}.xs :: g |- xs :: g {}.f :: k |- f :: k {}.tail :: m -> n.xs :: m |- tail(xs) :: n
------------------- ----------------------------------------------- ----------------------- -----------------------------------------------------------------
{}.f :: e |- f :: e {}.head :: g -> h.xs :: g |- head(xs) :: h {}.map :: j |- map :: j {}.f :: k.tail :: m -> n.xs :: m |- (f, tail(xs)) :: (k, n)
---------------------------------------------------------------- --------------------------------------------------------------------------------------
{}.f :: h -> i.head :: g -> h.xs :: g |- f(head(xs)) :: i {}.map :: k x n -> o.f :: k.tail :: m -> n.xs :: m |- map(f, tail(xs)) :: o
------------------------- --------------------- ---------------------------- ------------------------- --------------------------------------------------------------------------------------------------------------------------------------------------
{}.null :: a |- null :: a {}.xs :: b |- xs :: b {} |- [] :: forall a. List a {}.cons :: p |- cons :: p {}.head :: g -> h.f :: h -> i.xs :: g.map :: (h -> i) x n -> o.tail :: g -> n |- (f(head(xs)), map(f, tail(xs))) :: (i, o)
----------------------------------------------- ---------------------------- ----------------------------------------------------------------------------------------------------------------------------------------------------------------
{}.null :: b -> c.xs :: b |- null(xs) :: c {} |- [] :: List d {}.cons :: i x o -> q.head :: g -> h.f :: h -> i.xs :: g.map :: (h -> i) x n -> o.tail :: g -> n |- cons(f(head(xs)), map(f, tail(xs))) :: q
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
{}.null :: b -> Bool.xs :: b.cons :: i x o -> List d.head :: b -> h.f :: h -> i.map :: (h -> i) x n -> o.tail :: b -> n |- if null(xs) then [] else cons(f(head(xs)), map(f, tail(xs))) :: List d