type variable = string

let globalIdentifier = ref 1

module VariableMap = Map.Make(String)
module VariableSet = Set.Make(String)

(* -------------------------------------------------------------------------- *)
(*                      polimporphic type checking types                      *)
(* -------------------------------------------------------------------------- *)

type id = int
type level = int

type type_f =
    IntegerTypeP
  | BooleanTypeP
  | TupleTypeP of type_f * type_f
  | VariableTypeP of variable_type ref
  | FunctionTypeP of type_f * type_f
  | ApplicationP of type_f * type_f
and variable_type =
    Unbound of id * level
  | Link of type_f
  | Generic of id

type env = type_f VariableMap.t
module IntegerMap = Map.Make(Int)

let pp_type_f (ty: type_f) : string =
  let id_name_map = ref IntegerMap.empty in
  let count = ref 0 in
  let next_name () =
    let i = !count in
    incr count;
    Utility.from_int_to_string i
  in
  let rec aux is_simple ty =
    match ty with
    | IntegerTypeP -> "Int"
    | BooleanTypeP -> "Bool"
    | TupleTypeP (ty1, ty2) ->
      "(" ^ aux is_simple ty1 ^ ", " ^ aux is_simple ty2 ^ ")"
    | ApplicationP (ty, ty_arg) ->
      aux true ty ^ "(" ^ aux false ty_arg ^ ")"
    | FunctionTypeP (ty_arg, ty) ->
      let ty_arg_str = aux true ty_arg in
      let ty_str = aux false ty in
      let str = ty_arg_str ^ " -> " ^ ty_str in
      if is_simple then "(" ^ str ^ ")" else str
    | VariableTypeP {contents = Generic id} -> (
        match IntegerMap.find_opt id !id_name_map with
        | Some a -> a
        | None ->
          let name = next_name () in
          id_name_map := IntegerMap.add id name !id_name_map;
          name
      )
    | VariableTypeP {contents = Unbound (id, _)} ->
      "_" ^ string_of_int id
    | VariableTypeP {contents = Link ty} ->
      aux is_simple ty
  in
  let ty_str = aux false ty in
  if !count > 0 then
    let var_names =
      IntegerMap.fold (fun _ value acc -> value :: acc) !id_name_map []
    in
    "∀ " ^ (String.concat " " (List.sort String.compare var_names))
    ^ ", " ^ ty_str
  else
    ty_str

(* -------------------------------------------------------------------------- *)

type ftype = (* type used for specification *)
    IntegerType
  | BooleanType
  | TupleType of ftype * ftype
  | FunctionType of ftype * ftype

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
]