From 24e5b9e55893195b769efeb58a68ab5d29641638 Mon Sep 17 00:00:00 2001
From: Michael Andreen <harv@ruin.nu>
Date: Fri, 10 Mar 2006 10:01:30 +0000
Subject: [PATCH] major update of the natural deduction

---
 documentation | 96 +++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 77 insertions(+), 19 deletions(-)

diff --git a/documentation b/documentation
index d649bba..2d64044 100644
--- a/documentation
+++ b/documentation
@@ -16,70 +16,128 @@ typing rules
 (t is little tau, T is large tau, E is 'in', and + is that other symbol)
 
 
-[Eq, Neq]
+[Eq, NEq]
 
-e:bool  <=  e1:t  &  e2:t
-where e is e1 Eq e2.
+T+ e1 Eq e2:bool  <=  T+ e1:t  &  T+ e2:t
+
+If e1 and e2 are of the same type, then Eq or NEq return bool
 
 
 [Plus, Minus, Times, Div]
 
-e:int  <=  e1:int  &  e2:int
-where e is e1 Plus e2.
+T+ e1 Plus e2:int  <=  T+ e1:int  &  T+ e2:int
+
+The operators Plus/Minus/Times/Div return int if both operands are ints
 
 
 [Lt, ELt, Gt, EGt]
 
-e:bool  <=  e1:int  &  e2:int
-where e is e1 Lt e2.
+T+ e1 Lt e2:bool  <=  T+ e1:int  &  T+ e2:int
+
+The operators Lt/ELt/Gt/EGt return bool if both operands are ints
 
 
 [Assignment]
 
 T+ i := e:t  <=  i:t E T  &  T+ e:t
-where the assignment is identifier i = expression e.
-
 
-[ExpT]
-
-u,e:t  <=  e:t  &  u:t
-where the expression is type u expression e.
+The assignemnt of e to i returns type t if both i and e have type t.
 
 
 [ENeg]
 
-e:int  <=  e:int
+T+ ENeg e:int  <=  T+ e:int
 
+ENeg e returns int if e is of type int
 
 [ENot]
 
-e:bool  <=  e:bool
+T+ ENot e:bool  <=  e:bool
+
+ENot e returns bool if e is of type bool
+
+[EVar]
+
+T+ i:t <= i:t E T
+
+i has type t if i is defined in the context with type t.
+
+[EInt]
+
+T+ n:int
+
+n has type int
+
+[EBool]
+
+T+ b:bool
+
+b has type bool
+
+[EReadI]
 
+T+ n:int
 
-[SExp, SBlock]
+EReadI returns an int
 
-S:NoType  <=  e:t
+[EReadB]
+
+T+ b:bool
+
+EReadB returns a bool
+
+[EPost]
+
+T+ EPost i:int <= i:int E T
+
+EPost i is of type int if i is defined in T with type int.
+
+[SExp]
+
+T+ e   <=  T+ e:t
+
+[SBlock]
+
+T+ s;SBlock ss <= T+ s => T' , T'+ ss => T''
+
+the first statment s, in the block, is typechecked in the context T and returns the context T', the rest of the block is then recursively typeckecked in the context T' 
 
 
 [SIf]
 
 T+ if e then s1 else s2  <=  T+ e:bool  &  T+ s1  &  T+ s2
 
+if e is of type bool and s1 and and s2 typechecks in the context T, then the same context is returned
+
 
 [SWhile]
 
 T+ while e do s  <=  T+ e:bool  &  T+ s
 
+If e is of type bool and s typechecks in context T then the same context is returned
+
+
 
 [SDecl]
 
-T+ i:t => T', i:t  <=  i!ET  &  e:t  &  u:t
+T+ t i = e => T,i:t  <=  i!ET  &  e:t 
+
+if i and e are of the same type and i is not declared in the current scope then i is added with type t to the context.
+
+[SDeclD]
 
-(Type u Ident i = Exp e)
+T+ t i => T,i:t  <=  i!ET
 
+if i is not declared in the current scope, then i is added to the context with type t
 
+[SNoop]
 
+T+ s
 
+SNoops does nothing so the same context is returned
 
+[SPrint]
 
+T+ e <= T+ e:t
 
+if e has type t then SPrint returns the same context
-- 
2.39.2