(** Resolved types: what [Ast.texpr] means once names are looked up.

    The AST's type expressions are surface syntax — [Tname "Ptr"] and
    [Tapp ("Option", ...)] are just names there. Here they are the real thing,
    and two types are the same type exactly when they are structurally equal.

    Milestone 2 has no generics, so there is no unification and no substitution:
    a type variable is parsed, carried, and rejected the moment a value would
    have to have it. That rejection lives in [Check]; this module only names
    the shape. *)

(* Machine integer types. Signedness and width are both part of the type —
   there is no implicit widening anywhere, per plan.org. *)
type ikind = I8 | I16 | I32 | I64 | U8 | U16 | U32 | U64

type fkind = F32 | F64

type t =
  | Int    of ikind
  | Float  of fkind
  | Bool
  | String
  | Unit                              (* the zero-sized type, not C's void *)
  | Never                             (* return, exit, error: no value at all *)
  | Named  of string                  (* a struct or union declared in the file *)
  | Slice  of t                       (* [T]     ptr+len, non-owning *)
  | Array  of int64 * t               (* [n T]   inline, a value, copies *)
  | Map    of t * t                   (* {K V} *)
  | Ptr    of t                       (* (Ptr T) *)
  | Option of t                       (* (Option T) *)
  | Fn     of t list * t              (* (Fn [T ...] R) *)
  | Var    of string                  (* a type variable — milestone 5 *)

let signed = function
  | I8 | I16 | I32 | I64 -> true
  | U8 | U16 | U32 | U64 -> false

let bits = function
  | I8 | U8 -> 8 | I16 | U16 -> 16 | I32 | U32 -> 32 | I64 | U64 -> 64

let bits_f = function F32 -> 32 | F64 -> 64

let ikind_of_name = function
  | "i8" -> Some I8 | "i16" -> Some I16 | "i32" -> Some I32 | "i64" -> Some I64
  | "u8" -> Some U8 | "u16" -> Some U16 | "u32" -> Some U32 | "u64" -> Some U64
  | _ -> None

let fkind_of_name = function
  | "f32" -> Some F32 | "f64" -> Some F64 | _ -> None

let ikind_name k =
  (if signed k then "i" else "u") ^ string_of_int (bits k)

let fkind_name = function F32 -> "f32" | F64 -> "f64"

(* Structural equality is the whole story: no subtyping, no coercion between
   machine types, no variance. Written out rather than using [=] so that adding
   a case with a function or a mutable field cannot silently break it. *)
let rec equal a b =
  match a, b with
  | Int x, Int y -> x = y
  | Float x, Float y -> x = y
  | Bool, Bool | String, String | Unit, Unit | Never, Never -> true
  | Named x, Named y -> String.equal x y
  | Slice x, Slice y -> equal x y
  | Array (n, x), Array (m, y) -> Int64.equal n m && equal x y
  | Map (k, v), Map (k', v') -> equal k k' && equal v v'
  | Ptr x, Ptr y -> equal x y
  | Option x, Option y -> equal x y
  | Fn (ps, r), Fn (ps', r') ->
    List.length ps = List.length ps'
    && List.for_all2 equal ps ps'
    && equal r r'
  | Var x, Var y -> String.equal x y
  | _ -> false

let rec to_string = function
  | Int k -> ikind_name k
  | Float k -> fkind_name k
  | Bool -> "bool"
  | String -> "string"
  | Unit -> "Unit"
  | Never -> "Never"
  | Named n -> n
  | Slice t -> "[" ^ to_string t ^ "]"
  | Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t)
  | Map (k, v) -> Printf.sprintf "{%s %s}" (to_string k) (to_string v)
  | Ptr t -> "(Ptr " ^ to_string t ^ ")"
  | Option t -> "(Option " ^ to_string t ^ ")"
  | Fn (ps, r) ->
    Printf.sprintf "(Fn [%s] %s)"
      (String.concat " " (List.map to_string ps)) (to_string r)
  | Var n -> n

let is_numeric = function Int _ | Float _ -> true | _ -> false

(* Ordering and equality are defined on machine types and on nothing else at
   milestone 2 — strings, structs and slices have no built-in [=], because an
   unconstrained type supports only what every type supports (plan.org, Types). *)
let is_comparable = is_numeric

(* [Never] is the type of an expression that does not produce a value: return,
   an early-returning `some`, exit. It fits anywhere, and that is the only
   place anything resembling subtyping exists. *)
let fits ~expected ~actual =
  match actual with Never -> true | _ -> equal expected actual