type variable = string

val globalIdentifier : int ref

module VariableMap : Map.S with type key = variable
module VariableSet : Set.S with type elt = string

type ftype =
    IntegerType
  | BooleanType
  | TupleType of ftype * ftype
  | PolimorphicType of variable
  | FunctionType of ftype * ftype
type fsubstitution = (* goes from polimorphic types to types *)
  ftype VariableMap.t
type fenvironment = (* goes from variables to types *)
  ftype VariableMap.t
type typingshape = (* tuple of a simple type environment and a simple type *)
  fenvironment * ftype

type intermediaryType =
    IInteger
  | IBoolean
  | IVariable of variable
  | IFunction of variable list * ftype list * intermediaryType
  | IApplication of intermediaryType * intermediaryType list
  | IPlus of intermediaryType * intermediaryType
  | IMinus of intermediaryType * intermediaryType
  | ITimes of intermediaryType * intermediaryType
  | IDivision of intermediaryType * intermediaryType
  | IModulo of intermediaryType * intermediaryType
  | IPower of intermediaryType * intermediaryType
  | IPowerMod of intermediaryType * intermediaryType * intermediaryType
  | IRand of intermediaryType
  | IBAnd of intermediaryType * intermediaryType
  | IBOr of intermediaryType * intermediaryType
  | IBNot of intermediaryType
  | ICmp of intermediaryType * intermediaryType
  | ICmpLess of intermediaryType * intermediaryType
  | ICmpLessEq of intermediaryType * intermediaryType
  | ICmpGreater of intermediaryType * intermediaryType
  | ICmpGreaterEq of intermediaryType * intermediaryType
  | IIfThenElse of intermediaryType * intermediaryType * intermediaryType
  | ILetIn of variable * ftype * intermediaryType * intermediaryType
  | ILetFun of variable * ftype * variable list * ftype list * intermediaryType * intermediaryType

type t_exp =
    Integer of int                                             (* x := a *)
  | Boolean of bool                                            (* v *)
  | Variable of variable                                       (* x *)
  | Tuple of t_exp * t_exp                                     (* (a, b) *)
  | Function of variable * ftype * t_exp                       (* lambda x: t. x *)
  | Application of t_exp * t_exp                               (* x x *)
  | Plus of t_exp * t_exp                                      (* x + x *)
  | Minus of t_exp * t_exp                                     (* x - x *)
  | Times of t_exp * t_exp                                     (* x * x *)
  | Division of t_exp * t_exp                                  (* x / x *)
  | Modulo of t_exp * t_exp                                    (* x % x *)
  | Power of t_exp * t_exp                                     (* x ^ x *)
  | PowerMod of t_exp * t_exp * t_exp                          (* (x ^ x) % x *)
  | Rand of t_exp                                              (* rand(0, x) *)
  | BAnd of t_exp * t_exp                                      (* x && x *)
  | BOr of t_exp * t_exp                                       (* x || x *)
  | BNot of t_exp                                              (* not x *)
  | First of t_exp                                             (* fst x *)
  | Second of t_exp                                            (* scn x *)
  | Cmp of t_exp * t_exp                                       (* x == x *)
  | CmpLess of t_exp * t_exp                                   (* x < x *)
  | CmpLessEq of t_exp * t_exp                                 (* x <= x *)
  | CmpGreater of t_exp * t_exp                                (* x > x *)
  | CmpGreaterEq of t_exp * t_exp                              (* x >= x *)
  | IfThenElse of t_exp * t_exp * t_exp                        (* if b then c else c *)
  | LetIn of variable * t_exp * t_exp                          (* let x = x in x *)
  | LetFun of variable * variable * ftype * t_exp * t_exp      (* let rec x. y: t. x in x*)

type permitted_values =
    IntegerPermitted  of int
  | BooleanPermitted  of bool
  | TuplePermitted    of permitted_values * permitted_values
  | FunctionPermitted of closure
and closure = {
  input: variable;
  body: t_exp;
  assignments: permitted_values VariableMap.t;
  recursiveness: variable option
}

type memory = {
  assignments: permitted_values VariableMap.t
}


type base_error = [
    `AbsentAssignment of string
  | `WrongType of string
]

type typechecking_error = [
  | base_error
  | `WrongTypeSpecification of string
]

type error = [
  | base_error
  | `DivisionByZero of string
]