module til-typecheck-exp
imports TIL
strategies

  typecheck-exp(typecheck-var) = 
    bottomup(try(
      typecheck-var <+ TypecheckAdd <+ TypecheckMul <+ TypecheckSub <+ TypecheckDiv <+ TypecheckMod
      <+ TypecheckLeq <+ TypecheckGeq <+ TypecheckLt <+ TypecheckGt <+ TypecheckEqu <+ TypecheckNeq
      <+ TypecheckOr <+ TypecheckAnd
      <+ TypecheckInt <+ TypecheckString <+ TypecheckBool
    ))

rules

  typeof :
    e{t*} -> t
    where <fetch-elem(is-type)> t* => t
    
  is-type = 
    ?TypeName(_)
    
  TypecheckInt :
    Int(i) -> Int(i){TypeName("int")}

  TypecheckString :
    String(x) -> String(x){TypeName("string")}

  TypecheckBool :
    True() -> True(){TypeName("bool")}
    
  TypecheckBool :
    False() -> False(){TypeName("bool")}
    
  TypecheckAdd :
    Add(e1, e2) -> Add(e1, e2){TypeName("string")}
    where <typeof> e1 => TypeName("string")
        ; <typeof> e2 => TypeName("string")

  TypecheckAdd :
    Add(e1, e2) -> Add(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckMul :
    Mul(e1, e2) -> Mul(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckSub :
    Sub(e1, e2) -> Sub(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckDiv :
    Div(e1, e2) -> Div(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
 
  TypecheckMod :
    Mod(e1, e2) -> Mod(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckLt :
    Lt(e1, e2) -> Lt(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckGt :
    Gt(e1, e2) -> Gt(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
   
  TypecheckLeq :
    Leq(e1, e2) -> Leq(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
        
  TypecheckGeq :
    Geq(e1, e2) -> Geq(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
 
  TypecheckEqu :
    Equ(e1, e2) -> Equ(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
        
  TypecheckNeq :
    Neq(e1, e2) -> Neq(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
           
  TypecheckAnd :
    And(e1, e2) -> And(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("bool")
        ; <typeof> e2 => TypeName("bool")
           
  TypecheckOr :
    Or(e1, e2) -> Or(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("bool")
        ; <typeof> e2 => TypeName("bool")