a mess..

* converted to string to avoid breaking interface, would be fixed later
* tests would not check error messages now, as messages are not
  finalized

Cargo.lock

@@ -288,6 +288,15 @@ dependencies = [
  "proc-macro-hack",
 ]
 
+[[package]]
+name = "indoc"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e5a75aeaaef0ce18b58056d306c27b07436fbb34b8816c53094b76dd81803136"
+dependencies = [
+ "unindent",
+]
+
 [[package]]
 name = "indoc-impl"
 version = "0.3.6"
@@ -449,10 +458,12 @@ checksum = "0ee1c47aaa256ecabcaea351eae4a9b01ef39ed810004e298d2511ed284b1525"
 name = "nac3core"
 version = "0.1.0"
 dependencies = [
+ "indoc 1.0.3",
  "inkwell",
  "num-bigint",
  "num-traits",
  "rustpython-parser",
+ "thiserror",
 ]
 
 [[package]]
@@ -613,7 +624,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bf6bbbe8f70d179260b3728e5d04eb012f4f0c7988e58c11433dd689cecaa72e"
 dependencies = [
  "ctor",
- "indoc",
+ "indoc 0.3.6",
  "inventory",
  "libc",
  "parking_lot",
@@ -830,6 +841,26 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "thiserror"
+version = "1.0.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76cc616c6abf8c8928e2fdcc0dbfab37175edd8fb49a4641066ad1364fdab146"
+dependencies = [
+ "thiserror-impl",
+]
+
+[[package]]
+name = "thiserror-impl"
+version = "1.0.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9be73a2caec27583d0046ef3796c3794f868a5bc813db689eed00c7631275cd1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "thread_local"
 version = "1.0.1"

nac3core/Cargo.toml

@@ -7,5 +7,10 @@ edition = "2018"
 [dependencies]
 num-bigint = "0.3"
 num-traits = "0.2"
+thiserror = "1.0"
 inkwell = { git = "https://github.com/TheDan64/inkwell", branch = "master", features = ["llvm10-0"] }
 rustpython-parser = { git = "https://github.com/RustPython/RustPython", branch = "master" }
+
+[dev-dependencies]
+indoc = "1.0"
+

nac3core/src/lib.rs

@@ -5,12 +5,7 @@ extern crate num_bigint;
 extern crate inkwell;
 extern crate rustpython_parser;
 
-pub mod expression_inference;
-pub mod inference_core;
-mod magic_methods;
-pub mod primitives;
-pub mod typedef;
-pub mod context;
+pub mod type_check;
 
 use std::error::Error;
 use std::fmt;

nac3core/src/type_check/context/inference_context.rs

@@ -1,5 +1,5 @@
+use super::super::typedef::*;
 use super::TopLevelContext;
-use crate::typedef::*;
 use std::boxed::Box;
 use std::collections::HashMap;
 
@@ -22,14 +22,14 @@ pub struct InferenceContext<'a> {
     primitives: Vec<Type>,
     /// list of variable instances
     variables: Vec<Type>,
-    /// identifier to (type, readable) mapping.
-    /// an identifier might be defined earlier but has no value (for some code path), thus not
-    /// readable.
-    sym_table: HashMap<&'a str, (Type, bool)>,
+    /// identifier to type mapping.
+    sym_table: HashMap<&'a str, Type>,
     /// resolution function reference, that may resolve unbounded identifiers to some type
     resolution_fn: Box<dyn FnMut(&str) -> Result<Type, String>>,
     /// stack
     stack: ContextStack<'a>,
+    /// return type
+    result: Option<Type>,
 }
 
 // non-trivial implementations here
@@ -56,6 +56,7 @@ impl<'a> InferenceContext<'a> {
                 var_defs: Vec::new(),
                 sym_def: Vec::new(),
             },
+            result: None,
         }
     }
 
@@ -63,7 +64,7 @@ impl<'a> InferenceContext<'a> {
     /// variable assignment would be limited within the scope (not readable outside), and type
     /// variable type guard would be limited within the scope.
     /// returns the list of variables assigned within the scope, and the result of the function
-    pub fn with_scope<F, R>(&mut self, f: F) -> (Vec<&'a str>, R)
+    pub fn with_scope<F, R>(&mut self, f: F) -> (Vec<(&'a str, Type)>, R)
     where
         F: FnOnce(&mut Self) -> R,
     {
@@ -84,8 +85,8 @@ impl<'a> InferenceContext<'a> {
             let (_, level) = self.stack.sym_def.last().unwrap();
             if *level > self.stack.level {
                 let (name, _) = self.stack.sym_def.pop().unwrap();
-                self.sym_table.remove(name).unwrap();
-                poped_names.push(name);
+                let ty = self.sym_table.remove(name).unwrap();
+                poped_names.push((name, ty));
             } else {
                 break;
             }
@@ -96,19 +97,15 @@ impl<'a> InferenceContext<'a> {
     /// assign a type to an identifier.
     /// may return error if the identifier was defined but with different type
     pub fn assign(&mut self, name: &'a str, ty: Type) -> Result<Type, String> {
-        if let Some((t, x)) = self.sym_table.get_mut(name) {
+        if let Some(t) = self.sym_table.get_mut(name) {
             if t == &ty {
-                if !*x {
-                    self.stack.sym_def.push((name, self.stack.level));
-                }
-                *x = true;
                 Ok(ty)
             } else {
                 Err("different types".into())
             }
         } else {
             self.stack.sym_def.push((name, self.stack.level));
-            self.sym_table.insert(name, (ty.clone(), true));
+            self.sym_table.insert(name, ty.clone());
             Ok(ty)
         }
     }
@@ -122,12 +119,8 @@ impl<'a> InferenceContext<'a> {
     /// may return error if the identifier is not defined, and cannot be resolved with the
     /// resolution function.
     pub fn resolve(&mut self, name: &str) -> Result<Type, String> {
-        if let Some((t, x)) = self.sym_table.get(name) {
-            if *x {
-                Ok(t.clone())
-            } else {
-                Err("may not have value".into())
-            }
+        if let Some(t) = self.sym_table.get(name) {
+            Ok(t.clone())
         } else {
             self.resolution_fn.as_mut()(name)
         }
@@ -139,6 +132,10 @@ impl<'a> InferenceContext<'a> {
         std::mem::swap(self.top_level.var_defs.get_mut(id.0).unwrap(), &mut def);
         self.stack.var_defs.push((id.0, def, self.stack.level));
     }
+
+    pub fn set_result(&mut self, result: Option<Type>) {
+        self.result = result;
+    }
 }
 
 // trivial getters:
@@ -168,6 +165,9 @@ impl<'a> InferenceContext<'a> {
     pub fn get_type(&self, name: &str) -> Option<Type> {
         self.top_level.get_type(name)
     }
+    pub fn get_result(&self) -> Option<Type> {
+        self.result.clone()
+    }
 }
 
 impl TypeEnum {
@@ -215,7 +215,7 @@ impl TypeEnum {
         }
     }
 
-    pub fn get_base<'b: 'a, 'a>(&'a self, ctx: &'b InferenceContext) -> Option<&'b TypeDef> {
+    pub fn get_base<'a>(&'a self, ctx: &'a InferenceContext) -> Option<&'a TypeDef> {
         match self {
             TypeEnum::PrimitiveType(id) => Some(ctx.get_primitive_def(*id)),
             TypeEnum::ClassType(id) | TypeEnum::VirtualClassType(id) => {

nac3core/src/type_check/context/top_level_context.rs

@@ -1,4 +1,4 @@
-use crate::typedef::*;
+use super::super::typedef::*;
 use std::collections::HashMap;
 use std::rc::Rc;
 
@@ -130,7 +130,9 @@ impl<'a> TopLevelContext<'a> {
     }
 
     pub fn get_type(&self, name: &str) -> Option<Type> {
-        // TODO: handle parametric types
+        // TODO: handle name visibility
+        // possibly by passing a function from outside to tell what names are allowed, and what are
+        // not...
         self.sym_table.get(name).cloned()
     }
 }

nac3core/src/type_check/expression_inference.rs

@@ -1,8 +1,8 @@
-use crate::context::InferenceContext;
-use crate::inference_core::resolve_call;
-use crate::magic_methods::*;
-use crate::primitives::*;
-use crate::typedef::{Type, TypeEnum::*};
+use super::context::InferenceContext;
+use super::inference_core::resolve_call;
+use super::magic_methods::*;
+use super::primitives::*;
+use super::typedef::{Type, TypeEnum::*};
 use rustpython_parser::ast::{
     Comparison, Comprehension, ComprehensionKind, Expression, ExpressionType, Operator,
     UnaryOperator,
@@ -11,9 +11,9 @@ use std::convert::TryInto;
 
 type ParserResult = Result<Option<Type>, String>;
 
-pub fn infer_expr<'b: 'a, 'a>(
+pub fn infer_expr<'a>(
     ctx: &mut InferenceContext<'a>,
-    expr: &'b Expression,
+    expr: &'a Expression,
 ) -> ParserResult {
     match &expr.node {
         ExpressionType::Number { value } => infer_constant(ctx, value),
@@ -83,9 +83,9 @@ fn infer_identifier(ctx: &mut InferenceContext, name: &str) -> ParserResult {
     Ok(Some(ctx.resolve(name)?))
 }
 
-fn infer_list<'b: 'a, 'a>(
+fn infer_list<'a>(
     ctx: &mut InferenceContext<'a>,
-    elements: &'b [Expression],
+    elements: &'a [Expression],
 ) -> ParserResult {
     if elements.is_empty() {
         return Ok(Some(ParametricType(LIST_TYPE, vec![BotType.into()]).into()));
@@ -105,9 +105,9 @@ fn infer_list<'b: 'a, 'a>(
     Ok(Some(ParametricType(LIST_TYPE, vec![head.unwrap()]).into()))
 }
 
-fn infer_tuple<'b: 'a, 'a>(
+fn infer_tuple<'a>(
     ctx: &mut InferenceContext<'a>,
-    elements: &'b [Expression],
+    elements: &'a [Expression],
 ) -> ParserResult {
     let types: Result<Option<Vec<_>>, String> =
         elements.iter().map(|v| infer_expr(ctx, v)).collect();
@@ -164,11 +164,11 @@ fn infer_bool_ops<'a>(ctx: &mut InferenceContext<'a>, values: &'a [Expression])
     }
 }
 
-fn infer_bin_ops<'b: 'a, 'a>(
+fn infer_bin_ops<'a>(
     ctx: &mut InferenceContext<'a>,
     op: &Operator,
-    left: &'b Expression,
-    right: &'b Expression,
+    left: &'a Expression,
+    right: &'a Expression,
 ) -> ParserResult {
     let left = infer_expr(ctx, left)?.ok_or_else(|| "no value".to_string())?;
     let right = infer_expr(ctx, right)?.ok_or_else(|| "no value".to_string())?;
@@ -176,10 +176,10 @@ fn infer_bin_ops<'b: 'a, 'a>(
     resolve_call(ctx, Some(left), fun, &[right])
 }
 
-fn infer_unary_ops<'b: 'a, 'a>(
+fn infer_unary_ops<'a>(
     ctx: &mut InferenceContext<'a>,
     op: &UnaryOperator,
-    obj: &'b Expression,
+    obj: &'a Expression,
 ) -> ParserResult {
     let ty = infer_expr(ctx, obj)?.ok_or_else(|| "no value".to_string())?;
     if let UnaryOperator::Not = op {
@@ -193,10 +193,10 @@ fn infer_unary_ops<'b: 'a, 'a>(
     }
 }
 
-fn infer_compare<'b: 'a, 'a>(
+fn infer_compare<'a>(
     ctx: &mut InferenceContext<'a>,
-    vals: &'b [Expression],
-    ops: &'b [Comparison],
+    vals: &'a [Expression],
+    ops: &'a [Comparison],
 ) -> ParserResult {
     let types: Result<Option<Vec<_>>, _> = vals.iter().map(|v| infer_expr(ctx, v)).collect();
     let types = types?;
@@ -218,10 +218,10 @@ fn infer_compare<'b: 'a, 'a>(
     Ok(Some(boolean))
 }
 
-fn infer_call<'b: 'a, 'a>(
+fn infer_call<'a>(
     ctx: &mut InferenceContext<'a>,
-    args: &'b [Expression],
-    function: &'b Expression,
+    args: &'a [Expression],
+    function: &'a Expression,
 ) -> ParserResult {
     let types: Result<Option<Vec<_>>, _> = args.iter().map(|v| infer_expr(ctx, v)).collect();
     let types = types?;
@@ -240,10 +240,10 @@ fn infer_call<'b: 'a, 'a>(
     resolve_call(ctx, obj, fun.as_str(), &types.unwrap())
 }
 
-fn infer_subscript<'b: 'a, 'a>(
+fn infer_subscript<'a>(
     ctx: &mut InferenceContext<'a>,
-    a: &'b Expression,
-    b: &'b Expression,
+    a: &'a Expression,
+    b: &'a Expression,
 ) -> ParserResult {
     let a = infer_expr(ctx, a)?.ok_or_else(|| "no value".to_string())?;
     let t = if let ParametricType(LIST_TYPE, ls) = a.as_ref() {
@@ -283,11 +283,11 @@ fn infer_subscript<'b: 'a, 'a>(
     }
 }
 
-fn infer_if_expr<'b: 'a, 'a>(
+fn infer_if_expr<'a>(
     ctx: &mut InferenceContext<'a>,
-    test: &'b Expression,
-    body: &'b Expression,
-    orelse: &'b Expression,
+    test: &'a Expression,
+    body: &'a Expression,
+    orelse: &'a Expression,
 ) -> ParserResult {
     let test = infer_expr(ctx, test)?.ok_or_else(|| "no value".to_string())?;
     if test != ctx.get_primitive(BOOL_TYPE) {
@@ -303,8 +303,8 @@ fn infer_if_expr<'b: 'a, 'a>(
     }
 }
 
-fn infer_simple_binding<'a: 'b, 'b>(
-    ctx: &mut InferenceContext<'b>,
+pub fn infer_simple_binding<'a>(
+    ctx: &mut InferenceContext<'a>,
     name: &'a Expression,
     ty: Type,
 ) -> Result<(), String> {
@@ -337,10 +337,10 @@ fn infer_simple_binding<'a: 'b, 'b>(
     }
 }
 
-fn infer_list_comprehension<'b: 'a, 'a>(
+fn infer_list_comprehension<'a>(
     ctx: &mut InferenceContext<'a>,
-    element: &'b Expression,
-    comprehension: &'b Comprehension,
+    element: &'a Expression,
+    comprehension: &'a Comprehension,
 ) -> ParserResult {
     if comprehension.is_async {
         return Err("async is not supported".into());
@@ -370,9 +370,10 @@ fn infer_list_comprehension<'b: 'a, 'a>(
 
 #[cfg(test)]
 mod test {
-    use super::*;
-    use crate::context::*;
-    use crate::typedef::*;
+    use super::{
+        super::{context::*, typedef::*},
+        *,
+    };
     use rustpython_parser::parser::parse_expression;
     use std::collections::HashMap;
     use std::rc::Rc;
@@ -704,7 +705,7 @@ mod test {
 
         let ast = parse_expression("a == a == 1").unwrap();
         let result = infer_expr(&mut ctx, &ast);
-        assert_eq!(result, Err("not equal".into()));
+        assert_eq!(result, Err("different types".into()));
 
         let ast = parse_expression("True > False").unwrap();
         let result = infer_expr(&mut ctx, &ast);

nac3core/src/type_check/inference_core.rs

@@ -1,6 +1,21 @@
-use crate::context::InferenceContext;
-use crate::typedef::{TypeEnum::*, *};
+use super::context::InferenceContext;
+use super::typedef::{TypeEnum::*, *};
 use std::collections::HashMap;
+use thiserror::Error;
+
+#[derive(Error, Debug)]
+enum SubstError {
+    #[error("different type variables after substitution")]
+    DifferentSubstVar(VariableId, VariableId),
+    #[error("cannot substitute unbounded type variable into bounded one")]
+    UnboundedTypeVar(VariableId, VariableId),
+    #[error("incompatible bound for type variables")]
+    IncompatibleBound(VariableId, VariableId),
+    #[error("only subtype of virtual class can be substituted into virtual class type")]
+    NotVirtualClassSubtype(Type, ClassId),
+    #[error("different types")]
+    DifferentTypes(Type, Type),
+}
 
 fn find_subst(
     ctx: &InferenceContext,
@@ -8,8 +23,7 @@ fn find_subst(
     sub: &mut HashMap<VariableId, Type>,
     mut a: Type,
     mut b: Type,
-) -> Result<(), String> {
-    // TODO: fix error messages later
+) -> Result<(), SubstError> {
     if let TypeVariable(id) = a.as_ref() {
         if let Some((assumption_id, t)) = valuation {
             if assumption_id == id {
@@ -33,14 +47,14 @@ fn find_subst(
                 return if id_a == id_b {
                     Ok(())
                 } else {
-                    Err("different variables".to_string())
+                    Err(SubstError::DifferentSubstVar(*id_a, *id_b))
                 };
             }
             let v_a = ctx.get_variable_def(*id_a);
             let v_b = ctx.get_variable_def(*id_b);
             if !v_b.bound.is_empty() {
                 if v_a.bound.is_empty() {
-                    return Err("unbounded a".to_string());
+                    return Err(SubstError::UnboundedTypeVar(*id_a, *id_b));
                 } else {
                     let diff: Vec<_> = v_a
                         .bound
@@ -48,7 +62,7 @@ fn find_subst(
                         .filter(|x| !v_b.bound.contains(x))
                         .collect();
                     if !diff.is_empty() {
-                        return Err("different domain".to_string());
+                        return Err(SubstError::IncompatibleBound(*id_a, *id_b));
                     }
                 }
             }
@@ -60,7 +74,7 @@ fn find_subst(
             if v_a.bound.len() == 1 && v_a.bound[0].as_ref() == b.as_ref() {
                 Ok(())
             } else {
-                Err("different domain".to_string())
+                Err(SubstError::DifferentTypes(a.clone(), b.clone()))
             }
         }
         (_, TypeVariable(id_b)) => {
@@ -69,7 +83,7 @@ fn find_subst(
                 sub.insert(*id_b, a.clone());
                 Ok(())
             } else {
-                Err("different domain".to_string())
+                Err(SubstError::DifferentTypes(a.clone(), b.clone()))
             }
         }
         (_, VirtualClassType(id_b)) => {
@@ -82,7 +96,7 @@ fn find_subst(
                     parents = [*id_a].to_vec();
                 }
                 _ => {
-                    return Err("cannot substitute non-class type into virtual class".to_string());
+                    return Err(SubstError::NotVirtualClassSubtype(a.clone(), *id_b));
                 }
             };
             while !parents.is_empty() {
@@ -92,11 +106,11 @@ fn find_subst(
                 let c = ctx.get_class_def(parents.remove(0));
                 parents.extend_from_slice(&c.parents);
             }
-            Err("not subtype".to_string())
+            Err(SubstError::NotVirtualClassSubtype(a.clone(), *id_b))
         }
         (ParametricType(id_a, param_a), ParametricType(id_b, param_b)) => {
             if id_a != id_b || param_a.len() != param_b.len() {
-                Err("different parametric types".to_string())
+                Err(SubstError::DifferentTypes(a.clone(), b.clone()))
             } else {
                 for (x, y) in param_a.iter().zip(param_b.iter()) {
                     find_subst(ctx, valuation, sub, x.clone(), y.clone())?;
@@ -108,7 +122,7 @@ fn find_subst(
             if a == b {
                 Ok(())
             } else {
-                Err("not equal".to_string())
+                Err(SubstError::DifferentTypes(a.clone(), b.clone()))
             }
         }
     }
@@ -177,7 +191,7 @@ fn resolve_call_rec(
         return Err("incorrect parameter number".to_string());
     }
     for (a, b) in args.iter().zip(fun.args.iter()) {
-        find_subst(ctx, valuation, &mut subst, a.clone(), b.clone())?;
+        find_subst(ctx, valuation, &mut subst, a.clone(), b.clone()).map_err(|v| v.to_string())?;
     }
     let result = fun.result.as_ref().map(|v| v.subst(&subst));
     Ok(result.map(|result| {
@@ -200,9 +214,11 @@ pub fn resolve_call(
 
 #[cfg(test)]
 mod tests {
-    use super::*;
-    use crate::context::TopLevelContext;
-    use crate::primitives::*;
+    use super::{
+        super::{context::*, primitives::*},
+        *,
+    };
+    use std::matches;
     use std::rc::Rc;
 
     fn get_inference_context(ctx: TopLevelContext) -> InferenceContext {
@@ -243,25 +259,25 @@ mod tests {
             Ok(Some(ctx.get_primitive(FLOAT_TYPE)))
         );
 
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "float", &[ctx.get_primitive(BOOL_TYPE)]),
-            Err("different domain".to_string())
-        );
+            Err(..)
+        ));
 
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "float", &[]),
-            Err("incorrect parameter number".to_string())
-        );
+            Err(..)
+        ));
 
         assert_eq!(
             resolve_call(&ctx, None, "float", &[v1]),
             Ok(Some(ctx.get_primitive(FLOAT_TYPE)))
         );
 
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "float", &[v2]),
-            Err("different domain".to_string())
-        );
+            Err(..)
+        ));
     }
 
     #[test]
@@ -308,40 +324,40 @@ mod tests {
             Ok(Some(int64.clone()))
         );
 
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, Some(int32), "__add__", &[int64]),
-            Err("not equal".to_string())
-        );
+            Err(..)
+        ));
 
         // with type variables
         assert_eq!(
             resolve_call(&ctx, Some(v1.clone()), "__add__", &[v1.clone()]),
             Ok(Some(v1.clone()))
         );
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, Some(v0.clone()), "__add__", &[v2.clone()]),
-            Err("unbounded type var".to_string())
-        );
-        assert_eq!(
+            Err(..)
+        ));
+        assert!(matches!(
             resolve_call(&ctx, Some(v1.clone()), "__add__", &[v0]),
-            Err("different domain".to_string())
-        );
-        assert_eq!(
+            Err(..)
+        ));
+        assert!(matches!(
             resolve_call(&ctx, Some(v1.clone()), "__add__", &[v2]),
-            Err("different domain".to_string())
-        );
-        assert_eq!(
+            Err(..)
+        ));
+        assert!(matches!(
             resolve_call(&ctx, Some(v1.clone()), "__add__", &[v3.clone()]),
-            Err("different domain".to_string())
-        );
-        assert_eq!(
+            Err(..)
+        ));
+        assert!(matches!(
             resolve_call(&ctx, Some(v3.clone()), "__add__", &[v1]),
-            Err("no such function".to_string())
-        );
-        assert_eq!(
+            Err(..)
+        ));
+        assert!(matches!(
             resolve_call(&ctx, Some(v3.clone()), "__add__", &[v3]),
-            Err("no such function".to_string())
-        );
+            Err(..)
+        ));
     }
 
     #[test]
@@ -393,10 +409,10 @@ mod tests {
             resolve_call(&ctx, None, "foo", &[v2.clone(), v2.clone(), v3.clone()]),
             Ok(Some(v2.clone()))
         );
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "foo", &[v2.clone(), v3.clone(), v3.clone()]),
-            Err("different variables".to_string())
-        );
+            Err(..)
+        ));
 
         assert_eq!(
             resolve_call(
@@ -416,15 +432,15 @@ mod tests {
             ),
             Ok(Some(v2.clone()))
         );
-        assert_eq!(
+        assert!(matches!(
             resolve_call(
                 &ctx,
                 None,
                 "foo1",
                 &[ParametricType(TUPLE_TYPE, vec![v2, v3.clone(), v3]).into()]
             ),
-            Err("different variables".to_string())
-        );
+            Err(..)
+        ));
     }
 
     #[test]
@@ -478,15 +494,15 @@ mod tests {
             ),
             Ok(None)
         );
-        assert_eq!(
+        assert!(matches!(
             resolve_call(
                 &ctx,
                 Some(ParametricType(LIST_TYPE, vec![v0]).into()),
                 "append",
                 &[v1]
             ),
-            Err("different variables".to_string())
-        );
+            Err(..)
+        ));
     }
 
     #[test]
@@ -560,10 +576,10 @@ mod tests {
             Ok(None)
         );
 
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "foo", &[ClassType(bar).into()]),
-            Err("not subtype".to_string())
-        );
+            Err(..)
+        ));
 
         assert_eq!(
             resolve_call(&ctx, None, "foo1", &[ClassType(foo1).into()]),
@@ -575,10 +591,10 @@ mod tests {
             Ok(None)
         );
 
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "foo1", &[ClassType(foo).into()]),
-            Err("not subtype".to_string())
-        );
+            Err(..)
+        ));
 
         // virtual class substitution
         assert_eq!(
@@ -593,9 +609,9 @@ mod tests {
             resolve_call(&ctx, None, "foo", &[VirtualClassType(foo2).into()]),
             Ok(None)
         );
-        assert_eq!(
+        assert!(matches!(
             resolve_call(&ctx, None, "foo", &[VirtualClassType(bar).into()]),
-            Err("not subtype".to_string())
-        );
+            Err(..)
+        ));
     }
 }

nac3core/src/type_check/mod.rs

@@ -0,0 +1,9 @@
+pub mod context;
+pub mod expression_inference;
+pub mod inference_core;
+mod magic_methods;
+pub mod primitives;
+pub mod statement_check;
+pub mod typedef;
+pub mod signature;
+

nac3core/src/type_check/primitives.rs

@@ -1,7 +1,9 @@
+use super::context::*;
 use super::typedef::{TypeEnum::*, *};
-use crate::context::*;
 use std::collections::HashMap;
 
+pub const PRIMITIVES: [&str; 6] = ["int32", "int64", "float", "bool", "list", "tuple"];
+
 pub const TUPLE_TYPE: ParamId = ParamId(0);
 pub const LIST_TYPE: ParamId = ParamId(1);
 
@@ -17,8 +19,11 @@ fn impl_math(def: &mut TypeDef, ty: &Type) {
         result: result.clone(),
     };
     def.methods.insert("__add__", fun.clone());
+    def.methods.insert("__iadd__", fun.clone());
     def.methods.insert("__sub__", fun.clone());
+    def.methods.insert("__isub__", fun.clone());
     def.methods.insert("__mul__", fun.clone());
+    def.methods.insert("__imul__", fun.clone());
     def.methods.insert(
         "__neg__",
         FnDef {
@@ -33,9 +38,21 @@ fn impl_math(def: &mut TypeDef, ty: &Type) {
             result: Some(PrimitiveType(FLOAT_TYPE).into()),
         },
     );
+    if ty.as_ref() == &PrimitiveType(FLOAT_TYPE) {
+        def.methods.insert(
+            "__itruediv__",
+            FnDef {
+                args: vec![ty.clone()],
+                result: Some(PrimitiveType(FLOAT_TYPE).into()),
+            },
+        );
+    }
     def.methods.insert("__floordiv__", fun.clone());
+    def.methods.insert("__ifloordiv__", fun.clone());
     def.methods.insert("__mod__", fun.clone());
-    def.methods.insert("__pow__", fun);
+    def.methods.insert("__imod__", fun.clone());
+    def.methods.insert("__pow__", fun.clone());
+    def.methods.insert("__ipow__", fun);
 }
 
 fn impl_bits(def: &mut TypeDef, ty: &Type) {

nac3core/src/type_check/signature.rs

@@ -0,0 +1,423 @@
+/// obtain class and function signature from AST
+use super::context::TopLevelContext;
+use super::primitives::*;
+use super::typedef::*;
+use rustpython_parser::ast::{
+    ComprehensionKind, ExpressionType, Statement, StatementType, StringGroup,
+};
+use std::collections::HashMap;
+
+// TODO: fix condition checking, return error message instead of panic...
+
+fn typename_from_expr<'a>(typenames: &mut Vec<&'a str>, expr: &'a ExpressionType) {
+    match expr {
+        ExpressionType::Identifier { name } => typenames.push(&name),
+        ExpressionType::String { value } => match value {
+            StringGroup::Constant { value } => typenames.push(&value),
+            _ => unimplemented!(),
+        },
+        ExpressionType::Subscript { a, b } => {
+            typename_from_expr(typenames, &b.node);
+            typename_from_expr(typenames, &a.node)
+        }
+        _ => unimplemented!(),
+    }
+}
+
+fn typename_from_fn<'a>(typenames: &mut Vec<&'a str>, fun: &'a StatementType) {
+    match fun {
+        StatementType::FunctionDef { args, returns, .. } => {
+            for arg in args.args.iter() {
+                if let Some(ann) = &arg.annotation {
+                    typename_from_expr(typenames, &ann.node);
+                }
+            }
+            if let Some(returns) = &returns {
+                typename_from_expr(typenames, &returns.node);
+            }
+        }
+        _ => unreachable!(),
+    }
+}
+
+fn name_from_expr<'a>(expr: &'a ExpressionType) -> &'a str {
+    match &expr {
+        ExpressionType::Identifier { name } => &name,
+        ExpressionType::String { value } => match value {
+            StringGroup::Constant { value } => &value,
+            _ => unimplemented!(),
+        },
+        _ => unimplemented!(),
+    }
+}
+
+fn type_from_expr<'a>(ctx: &'a TopLevelContext, expr: &'a ExpressionType) -> Result<Type, String> {
+    match expr {
+        ExpressionType::Identifier { name } => {
+            ctx.get_type(name).ok_or_else(|| "no such type".into())
+        }
+        ExpressionType::String { value } => match value {
+            StringGroup::Constant { value } => {
+                ctx.get_type(&value).ok_or_else(|| "no such type".into())
+            }
+            _ => unimplemented!(),
+        },
+        ExpressionType::Subscript { a, b } => {
+            if let ExpressionType::Identifier { name } = &a.node {
+                match name.as_str() {
+                    "list" => {
+                        let ty = type_from_expr(ctx, &b.node)?;
+                        Ok(TypeEnum::ParametricType(LIST_TYPE, vec![ty]).into())
+                    }
+                    "tuple" => {
+                        if let ExpressionType::Tuple { elements } = &b.node {
+                            let ty_list: Result<Vec<_>, _> = elements
+                                .iter()
+                                .map(|v| type_from_expr(ctx, &v.node))
+                                .collect();
+                            Ok(TypeEnum::ParametricType(TUPLE_TYPE, ty_list?).into())
+                        } else {
+                            Err("unsupported format".into())
+                        }
+                    }
+                    _ => Err("no such parameterized type".into()),
+                }
+            } else {
+                // we require a to be an identifier, for a[b]
+                Err("unsupported format".into())
+            }
+        }
+        _ => Err("unsupported format".into()),
+    }
+}
+
+pub fn get_typenames<'a>(stmts: &'a [Statement]) -> (Vec<&'a str>, Vec<&'a str>) {
+    let mut classes = Vec::new();
+    let mut typenames = Vec::new();
+    for stmt in stmts.iter() {
+        match &stmt.node {
+            StatementType::ClassDef {
+                name, body, bases, ..
+            } => {
+                // check if class is not duplicated...
+                // and annotations
+                classes.push(&name[..]);
+                for base in bases.iter() {
+                    let name = name_from_expr(&base.node);
+                    typenames.push(name);
+                }
+                // may check if fields/functions are not duplicated
+                for stmt in body.iter() {
+                    match &stmt.node {
+                        StatementType::AnnAssign { annotation, .. } => {
+                            typename_from_expr(&mut typenames, &annotation.node)
+                        }
+                        StatementType::FunctionDef { .. } => {
+                            typename_from_fn(&mut typenames, &stmt.node);
+                        }
+                        _ => unimplemented!(),
+                    }
+                }
+            }
+            StatementType::FunctionDef { .. } => {
+                // may check annotations
+                typename_from_fn(&mut typenames, &stmt.node);
+            }
+            _ => (),
+        }
+    }
+    let mut unknowns = Vec::new();
+    for n in typenames {
+        if !PRIMITIVES.contains(&n) && !classes.contains(&n) && !unknowns.contains(&n) {
+            unknowns.push(n);
+        }
+    }
+    (classes, unknowns)
+}
+
+fn resolve_function<'a>(
+    ctx: &'a TopLevelContext,
+    fun: &'a StatementType,
+    method: bool,
+) -> Result<FnDef, String> {
+    if let StatementType::FunctionDef { args, returns, .. } = &fun {
+        let args = if method {
+            args.args[1..].iter()
+        } else {
+            args.args.iter()
+        };
+        let args: Result<Vec<_>, _> = args
+            .map(|arg| type_from_expr(ctx, &arg.annotation.as_ref().unwrap().node))
+            .collect();
+        let args = args?;
+        let result = match returns {
+            Some(v) => Some(type_from_expr(ctx, &v.node)?),
+            None => None,
+        };
+        Ok(FnDef { args, result })
+    } else {
+        unreachable!()
+    }
+}
+
+fn get_expression_unknowns<'a>(
+    defined: &[&'a str],
+    unknowns: &mut Vec<&'a str>,
+    expr: &'a ExpressionType,
+) {
+    match expr {
+        ExpressionType::BoolOp { values, .. } => {
+            for v in values.iter() {
+                get_expression_unknowns(defined, unknowns, &v.node)
+            }
+        }
+        ExpressionType::Binop { a, b, .. } => {
+            get_expression_unknowns(defined, unknowns, &a.node);
+            get_expression_unknowns(defined, unknowns, &b.node);
+        }
+        ExpressionType::Subscript { a, b } => {
+            get_expression_unknowns(defined, unknowns, &a.node);
+            get_expression_unknowns(defined, unknowns, &b.node);
+        }
+        ExpressionType::Unop { a, .. } => {
+            get_expression_unknowns(defined, unknowns, &a.node);
+        }
+        ExpressionType::Compare { vals, .. } => {
+            for v in vals.iter() {
+                get_expression_unknowns(defined, unknowns, &v.node)
+            }
+        }
+        ExpressionType::Attribute { value, .. } => {
+            get_expression_unknowns(defined, unknowns, &value.node);
+        }
+        ExpressionType::Call { function, args, .. } => {
+            get_expression_unknowns(defined, unknowns, &function.node);
+            for v in args.iter() {
+                get_expression_unknowns(defined, unknowns, &v.node)
+            }
+        }
+        ExpressionType::List { elements } => {
+            for v in elements.iter() {
+                get_expression_unknowns(defined, unknowns, &v.node)
+            }
+        }
+        ExpressionType::Tuple { elements } => {
+            for v in elements.iter() {
+                get_expression_unknowns(defined, unknowns, &v.node)
+            }
+        }
+        ExpressionType::Comprehension { kind, generators } => {
+            if generators.len() != 1 {
+                unimplemented!()
+            }
+            let g = &generators[0];
+            get_expression_unknowns(defined, unknowns, &g.iter.node);
+            let mut scoped = defined.to_owned();
+            get_expression_unknowns(defined, &mut scoped, &g.target.node);
+            for if_expr in g.ifs.iter() {
+                get_expression_unknowns(&scoped, unknowns, &if_expr.node);
+            }
+            match kind.as_ref() {
+                ComprehensionKind::List { element } => {
+                    get_expression_unknowns(&scoped, unknowns, &element.node);
+                }
+                _ => unimplemented!(),
+            }
+        }
+        ExpressionType::Slice { elements } => {
+            for v in elements.iter() {
+                get_expression_unknowns(defined, unknowns, &v.node);
+            }
+        }
+        ExpressionType::Identifier { name } => {
+            if !defined.contains(&name.as_str()) && !unknowns.contains(&name.as_str()) {
+                unknowns.push(name);
+            }
+        }
+        ExpressionType::IfExpression { test, body, orelse } => {
+            get_expression_unknowns(defined, unknowns, &test.node);
+            get_expression_unknowns(defined, unknowns, &body.node);
+            get_expression_unknowns(defined, unknowns, &orelse.node);
+        }
+        _ => (),
+    };
+}
+
+pub fn get_pattern_match_unknowns<'a>(
+    defined: &mut Vec<&'a str>,
+    unknowns: &mut Vec<&'a str>,
+    expr: &'a ExpressionType,
+) {
+    match expr {
+        ExpressionType::Identifier { name } => {
+            defined.push(&name.as_str());
+        }
+        ExpressionType::Tuple { elements } => {
+            for v in elements.iter() {
+                get_pattern_match_unknowns(defined, unknowns, &v.node);
+            }
+        }
+        _ => {
+            get_expression_unknowns(defined, unknowns, expr);
+        }
+    }
+}
+
+pub fn get_statement_unknowns<'a>(
+    defined: &mut Vec<&'a str>,
+    unknowns: &mut Vec<&'a str>,
+    stmts: &'a [Statement],
+) {
+    for stmt in stmts.iter() {
+        match &stmt.node {
+            StatementType::Return { value } => {
+                if let Some(v) = value {
+                    get_expression_unknowns(defined, unknowns, &v.node);
+                }
+            }
+            StatementType::Assign { targets, value } => {
+                get_expression_unknowns(defined, unknowns, &value.node);
+                for t in targets.iter() {
+                    get_pattern_match_unknowns(defined, unknowns, &t.node);
+                }
+            }
+            StatementType::AugAssign { target, value, .. } => {
+                get_expression_unknowns(defined, unknowns, &target.node);
+                get_expression_unknowns(defined, unknowns, &value.node);
+            }
+            StatementType::AnnAssign { target, value, .. } => {
+                if let Some(v) = value {
+                    get_expression_unknowns(defined, unknowns, &v.node);
+                }
+                get_pattern_match_unknowns(defined, unknowns, &target.node);
+            }
+            StatementType::Expression { expression } => {
+                get_expression_unknowns(defined, unknowns, &expression.node);
+            }
+            StatementType::If { test, body, orelse }
+            | StatementType::While { test, body, orelse } => {
+                get_expression_unknowns(defined, unknowns, &test.node);
+                get_statement_unknowns(defined, unknowns, body.as_slice());
+                if let Some(orelse) = orelse {
+                    get_statement_unknowns(defined, unknowns, orelse.as_slice());
+                }
+            }
+            StatementType::For { is_async, target, body, orelse, iter } => {
+                if *is_async {
+                    unimplemented!();
+                }
+                let mut scoped = defined.to_owned();
+                get_expression_unknowns(defined, unknowns, &iter.node);
+                get_expression_unknowns(defined, &mut scoped, &target.node);
+                get_statement_unknowns(&mut scoped, unknowns, body.as_slice());
+                if let Some(orelse) = orelse {
+                    get_statement_unknowns(&mut scoped, unknowns, orelse.as_slice());
+                }
+            }
+            StatementType::With { is_async, items, body } => {
+                if *is_async {
+                    unimplemented!();
+                }
+                let mut scoped = defined.to_owned();
+                for item in items.iter() {
+
+                }
+            }
+            _ => {}
+        }
+    }
+}
+
+pub fn resolve_signatures<'a>(ctx: &mut TopLevelContext<'a>, stmts: &'a [Statement]) {
+    for stmt in stmts.iter() {
+        match &stmt.node {
+            StatementType::ClassDef {
+                name, bases, body, ..
+            } => {
+                let mut parents = Vec::new();
+                for base in bases.iter() {
+                    let name = name_from_expr(&base.node);
+                    let c = ctx.get_type(name).unwrap();
+                    let id = if let TypeEnum::ClassType(id) = c.as_ref() {
+                        *id
+                    } else {
+                        unreachable!()
+                    };
+                    parents.push(id);
+                }
+
+                let mut fields = HashMap::new();
+                let mut functions = HashMap::new();
+
+                for stmt in body.iter() {
+                    match &stmt.node {
+                        StatementType::AnnAssign {
+                            target, annotation, ..
+                        } => {
+                            let name = name_from_expr(&target.node);
+                            let ty = type_from_expr(ctx, &annotation.node).unwrap();
+                            fields.insert(name, ty);
+                        }
+                        StatementType::FunctionDef { name, .. } => {
+                            functions.insert(
+                                &name[..],
+                                resolve_function(ctx, &stmt.node, true).unwrap(),
+                            );
+                        }
+                        _ => unimplemented!(),
+                    }
+                }
+
+                let class = ctx.get_type(name).unwrap();
+                let class = if let TypeEnum::ClassType(id) = class.as_ref() {
+                    ctx.get_class_def_mut(*id)
+                } else {
+                    unreachable!()
+                };
+                class.parents.extend_from_slice(&parents);
+                class.base.fields.clone_from(&fields);
+                class.base.methods.clone_from(&functions);
+            }
+            StatementType::FunctionDef { name, .. } => {
+                ctx.add_fn(&name[..], resolve_function(ctx, &stmt.node, false).unwrap());
+            }
+            _ => unimplemented!(),
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use indoc::indoc;
+    use rustpython_parser::parser::parse_program;
+
+    #[test]
+    fn test_get_classes() {
+        let ast = parse_program(indoc! {"
+            class Foo:
+                a: int32
+                b: Test
+
+                def test(self, a: int32) -> Test2:
+                    return b
+
+            class Bar(Foo, 'FooBar'):
+                def test2(self, a: list[Foo]) -> Test2:
+                    return b
+
+                def test3(self, a: list[FooBar2]) -> Test2:
+                    return b
+        " })
+        .unwrap();
+        let (mut classes, mut unknowns) = get_typenames(&ast.statements);
+        let classes_count = classes.len();
+        let unknowns_count = unknowns.len();
+        classes.sort();
+        unknowns.sort();
+        assert_eq!(classes.len(), classes_count);
+        assert_eq!(unknowns.len(), unknowns_count);
+        assert_eq!(&classes, &["Bar", "Foo"]);
+        assert_eq!(&unknowns, &["FooBar", "FooBar2", "Test", "Test2"]);
+    }
+}

nac3core/src/type_check/statement_check.rs

@@ -0,0 +1,572 @@
+use super::context::InferenceContext;
+use super::expression_inference::{infer_expr, infer_simple_binding};
+use super::inference_core::resolve_call;
+use super::magic_methods::binop_assign_name;
+use super::primitives::*;
+use super::typedef::{Type, TypeEnum::*};
+use rustpython_parser::ast::*;
+
+pub fn check_stmts<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    stmts: &'b [Statement],
+) -> Result<bool, String> {
+    for stmt in stmts.iter() {
+        match &stmt.node {
+            StatementType::Assign { targets, value } => {
+                check_assign(ctx, targets.as_slice(), &value)?;
+            }
+            StatementType::AugAssign { target, op, value } => {
+                check_aug_assign(ctx, &target, op, &value)?;
+            }
+            StatementType::If { test, body, orelse } => {
+                if check_if(ctx, test, body.as_slice(), orelse)? {
+                    return Ok(true);
+                }
+            }
+            StatementType::While { test, body, orelse } => {
+                check_while_stmt(ctx, test, body.as_slice(), orelse)?;
+            }
+            StatementType::For {
+                is_async,
+                target,
+                iter,
+                body,
+                orelse,
+            } => {
+                if *is_async {
+                    return Err("async for is not supported".to_string());
+                }
+                check_for_stmt(ctx, target, iter, body.as_slice(), orelse)?;
+            }
+            StatementType::Return { value } => {
+                let result = ctx.get_result();
+                let t = if let Some(value) = value {
+                    infer_expr(ctx, value)?
+                } else {
+                    None
+                };
+                return if t == result {
+                    Ok(true)
+                } else {
+                    Err("return type mismatch".to_string())
+                };
+            }
+            StatementType::Continue | StatementType::Break => {
+                continue;
+            }
+            _ => return Err("not supported".to_string()),
+        }
+    }
+    Ok(false)
+}
+
+fn get_target_type<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    target: &'b Expression,
+) -> Result<Type, String> {
+    match &target.node {
+        ExpressionType::Subscript { a, b } => {
+            let int32 = ctx.get_primitive(INT32_TYPE);
+            if infer_expr(ctx, &a)? == Some(int32) {
+                let b = get_target_type(ctx, &b)?;
+                if let ParametricType(LIST_TYPE, t) = b.as_ref() {
+                    Ok(t[0].clone())
+                } else {
+                    Err("subscript is only supported for list".to_string())
+                }
+            } else {
+                Err("subscript must be int32".to_string())
+            }
+        }
+        ExpressionType::Attribute { value, name } => {
+            let t = get_target_type(ctx, &value)?;
+            let base = t.get_base(ctx).ok_or_else(|| "no attributes".to_string())?;
+            Ok(base
+                .fields
+                .get(name.as_str())
+                .ok_or_else(|| "no such attribute")?
+                .clone())
+        }
+        ExpressionType::Identifier { name } => Ok(ctx.resolve(name.as_str())?),
+        _ => Err("not supported".to_string()),
+    }
+}
+
+fn check_stmt_binding<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    target: &'b Expression,
+    ty: Type,
+) -> Result<(), String> {
+    match &target.node {
+        ExpressionType::Identifier { name } => {
+            if name.as_str() == "_" {
+                Ok(())
+            } else {
+                match ctx.resolve(name.as_str()) {
+                    Ok(t) if t == ty => Ok(()),
+                    Err(_) => {
+                        ctx.assign(name.as_str(), ty).unwrap();
+                        Ok(())
+                    }
+                    _ => Err("conflicting type".into()),
+                }
+            }
+        }
+        ExpressionType::Tuple { elements } => {
+            if let ParametricType(TUPLE_TYPE, ls) = ty.as_ref() {
+                if ls.len() != elements.len() {
+                    return Err("incorrect pattern length".into());
+                }
+                for (x, y) in elements.iter().zip(ls.iter()) {
+                    check_stmt_binding(ctx, x, y.clone())?;
+                }
+                Ok(())
+            } else {
+                Err("pattern matching supports tuple only".into())
+            }
+        }
+        _ => {
+            let t = get_target_type(ctx, target)?;
+            if ty == t {
+                Ok(())
+            } else {
+                Err("type mismatch".into())
+            }
+        }
+    }
+}
+
+fn check_assign<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    targets: &'b [Expression],
+    value: &'b Expression,
+) -> Result<(), String> {
+    let ty = infer_expr(ctx, value)?.ok_or_else(|| "no value".to_string())?;
+    for t in targets.iter() {
+        check_stmt_binding(ctx, t, ty.clone())?;
+    }
+    Ok(())
+}
+
+fn check_aug_assign<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    target: &'b Expression,
+    op: &'b Operator,
+    value: &'b Expression,
+) -> Result<(), String> {
+    let left = infer_expr(ctx, target)?.ok_or_else(|| "no value".to_string())?;
+    let right = infer_expr(ctx, value)?.ok_or_else(|| "no value".to_string())?;
+    let fun = binop_assign_name(op);
+    resolve_call(ctx, Some(left), fun, &[right])?;
+    Ok(())
+}
+
+fn check_if<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    test: &'b Expression,
+    body: &'b [Statement],
+    orelse: &'b Option<Suite>,
+) -> Result<bool, String> {
+    let boolean = ctx.get_primitive(BOOL_TYPE);
+    let t = infer_expr(ctx, test)?;
+    if t == Some(boolean) {
+        let (names, result) = ctx.with_scope(|ctx| check_stmts(ctx, body));
+        let returned = result?;
+        if let Some(orelse) = orelse {
+            let (names2, result) = ctx.with_scope(|ctx| check_stmts(ctx, orelse.as_slice()));
+            let returned = returned && result?;
+            for (name, ty) in names.iter() {
+                for (name2, ty2) in names2.iter() {
+                    if *name == *name2 && ty == ty2 {
+                        ctx.assign(name, ty.clone()).unwrap();
+                    }
+                }
+            }
+            Ok(returned)
+        } else {
+            Ok(false)
+        }
+    } else {
+        Err("condition should be bool".to_string())
+    }
+}
+
+fn check_while_stmt<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    test: &'b Expression,
+    body: &'b [Statement],
+    orelse: &'b Option<Suite>,
+) -> Result<bool, String> {
+    let boolean = ctx.get_primitive(BOOL_TYPE);
+    let t = infer_expr(ctx, test)?;
+    if t == Some(boolean) {
+        // to check what variables are defined, we would have to do a graph analysis...
+        // not implemented now
+        let (_, result) = ctx.with_scope(|ctx| check_stmts(ctx, body));
+        result?;
+        if let Some(orelse) = orelse {
+            let (_, result) = ctx.with_scope(|ctx| check_stmts(ctx, orelse.as_slice()));
+            result?;
+        }
+        // to check whether the loop returned on every possible path, we need to analyse the graph,
+        // not implemented now
+        Ok(false)
+    } else {
+        Err("condition should be bool".to_string())
+    }
+}
+
+fn check_for_stmt<'b: 'a, 'a>(
+    ctx: &mut InferenceContext<'a>,
+    target: &'b Expression,
+    iter: &'b Expression,
+    body: &'b [Statement],
+    orelse: &'b Option<Suite>,
+) -> Result<bool, String> {
+    let ty = infer_expr(ctx, iter)?.ok_or_else(|| "no value".to_string())?;
+    if let ParametricType(LIST_TYPE, ls) = ty.as_ref() {
+        let (_, result) = ctx.with_scope(|ctx| {
+            infer_simple_binding(ctx, target, ls[0].clone())?;
+            check_stmts(ctx, body)
+        });
+        result?;
+        if let Some(orelse) = orelse {
+            let (_, result) = ctx.with_scope(|ctx| check_stmts(ctx, orelse.as_slice()));
+            result?;
+        }
+        // to check whether the loop returned on every possible path, we need to analyse the graph,
+        // not implemented now
+        Ok(false)
+    } else {
+        Err("only list can be iterated over".to_string())
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::{super::context::*, *};
+    use indoc::indoc;
+    use rustpython_parser::parser::parse_program;
+
+    fn get_inference_context(ctx: TopLevelContext) -> InferenceContext {
+        InferenceContext::new(ctx, Box::new(|_| Err("unbounded identifier".into())))
+    }
+
+    #[test]
+    fn test_assign() {
+        let ctx = basic_ctx();
+        let mut ctx = get_inference_context(ctx);
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = b * 2
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("unbounded identifier".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+
+        let ast = parse_program(indoc! {"
+            b = a = 1
+            b = b * 2
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            b = a = 1
+            b = [a]
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("conflicting type".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+    }
+
+    #[test]
+    fn test_if() {
+        let ctx = basic_ctx();
+        let mut ctx = get_inference_context(ctx);
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+            if b > a:
+                c = 1
+            else:
+                c = 0
+            d = c
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+            if b > a:
+                c = 1
+            else:
+                d = 0
+            d = c
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("unbounded identifier".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+            if b > a:
+                c = 1
+            d = c
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("unbounded identifier".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+            if a:
+                b = 0
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("condition should be bool".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+            if b > a:
+                c = 1
+            c = [1]
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = a * 2
+            if b > a:
+                c = 1
+            else:
+                c = 0
+            c = [1]
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("conflicting type".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+    }
+
+    #[test]
+    fn test_while() {
+        let ctx = basic_ctx();
+        let mut ctx = get_inference_context(ctx);
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = 1
+            while a < 10:
+                a += 1
+                b *= a
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = 1
+            while a < 10:
+                a += 1
+                b *= a
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = 1
+            while a < 10:
+                a += 1
+                b *= a
+            else:
+                a += 1
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = 1
+            while a:
+                a += 1
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("condition should be bool".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+
+        let ast = parse_program(indoc! {"
+            a = 1
+            b = 1
+            while a < 10:
+                a += 1
+                c = a*2
+            else:
+                c = a*2
+            b = c
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("unbounded identifier".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+    }
+
+    #[test]
+    fn test_for() {
+        let ctx = basic_ctx();
+        let mut ctx = get_inference_context(ctx);
+
+        let ast = parse_program(indoc! {"
+            b = 1
+            for a in [0, 1, 2, 3, 4, 5]:
+                b *= a
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            b = 1
+            for a, a1 in [(0, 1), (2, 3), (4, 5)]:
+                b *= a
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+    }
+
+    #[test]
+    fn test_return() {
+        let ctx = basic_ctx();
+        let mut ctx = get_inference_context(ctx);
+
+        let ast = parse_program(indoc! {"
+            b = 1
+            return
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(true), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            b = 1
+            if b > 0:
+                return
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            b = 1
+            if b > 0:
+                return
+            else:
+                return
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(true), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        let ast = parse_program(indoc! {"
+            b = 1
+            while b > 0:
+                return
+            else:
+                return
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            // with sophisticated analysis, this one should be Ok(true)
+            // but with our simple implementation, this is Ok(false)
+            // as we don't analyse the control flow
+            assert_eq!(Ok(false), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        ctx.set_result(Some(ctx.get_primitive(INT32_TYPE)));
+        let ast = parse_program(indoc! {"
+            b = 1
+            return 1
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(Ok(true), check_stmts(ctx, ast.statements.as_slice()));
+        });
+
+        ctx.set_result(Some(ctx.get_primitive(INT32_TYPE)));
+        let ast = parse_program(indoc! {"
+            b = 1
+            return [1]
+        " })
+        .unwrap();
+        ctx.with_scope(|ctx| {
+            assert_eq!(
+                Err("return type mismatch".to_string()),
+                check_stmts(ctx, ast.statements.as_slice())
+            );
+        });
+    }
+}

todo.txt

@@ -0,0 +1,23 @@
+Errors:
+- Not supported
+- Only * is supported
+- Expected * in *, but got *
+- Divergent type in (construct), (location 1), (location 2)
+- Unknown field
+- Unbounded variable
+- Different variable
+- Different domain
+- * is not subclass of *
+- Type not equal
+- Incorrect number of parameters
+
+Symbol Resolution:
+- Find class references, load them all in TopLevelContext.
+- Find unbounded identifiers/functions in functions.
+- `inspect.getmodule(x)` every unknown `x` if not primitive/list of primitives,
+  check their files recursively by getting their file path, cache with
+  (normalized) path as key.
+
+TopLevelContext/InferenceContext:
+- Restrict visibility by user defined function.
+