(** 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 *)
  (* A C enum: an i32 at run time, but its own type, so a keyword at a call
     site has something to resolve against and a plain integer does not fit. *)
  | Enum   of string
  | 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) *)
  (* [Allocator]: a builtin opaque type, the way [string] is a builtin
     ptr+len. It is a [Types.t] case with no user-writable constructor, which
     is what lets spec-memory.md's "procedure plus an opaque data pointer" be
     expressed with none of milestone 5's function values — the procedure is a
     C symbol the emitter names and no Flan type ever mentions it. At run time
     it is a pointer to the runtime's [flan_allocator], never a copy of one:
     the capability set and the epoch have to be shared by every container
     made from it, and a copy would give each its own. *)
  | Alloc
  (* [(Vec T)]: ptr + len + cap + allocator, owning and move-only. One
     type-erased runtime over (size, align) stands behind every instantiation,
     so this is a container without generics — the concrete type is known only
     at the call site, which is exactly where the two numbers are produced. *)
  | Vec    of 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

(* Every name the resolver accepts as a primitive type. The list exists so a
   near-miss can be reported as the typo it is. *)
let primitive_names =
  [ "i8"; "i16"; "i32"; "i64"; "u8"; "u16"; "u32"; "u64";
    "f32"; "f64"; "bool"; "string"; "Unit"; "Never"; "Allocator" ]

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 | Enum x, Enum 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
  | Alloc, Alloc -> true
  | Vec x, Vec 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 | Enum 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 ^ ")"
  | Alloc -> "Allocator"
  | Vec t -> "(Vec " ^ 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

(* Move-only: binding, passing or returning one transfers ownership and the
   source binding is dead afterwards (spec-memory.md, "The four container
   types"). That rule is what makes a double free unrepresentable, which is why
   [free] needs no analysis of its own. A struct that owns one is move-only
   too; that arrives with [drop], which is the step after this one. *)
let rec is_move_only = function
  | Vec _ -> true
  | Option t -> is_move_only t
  | Array (_, t) -> is_move_only t
  | _ -> 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 = function Enum _ -> true | t -> is_numeric t

(* [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