type name = Name.t Asai.Range.located
type local_name = Name.local Asai.Range.located

type arg = local_name * expr

and raw_expr =
  | Var of Name.t
  | Check of expr * expr
  | Pi of arg * expr
  | Fun of expr * expr
  | Lam of local_name * expr
  | App of expr * expr
  | Sg of arg * expr
  | Prod of expr * expr
  | Pair of expr * expr
  | Fst of expr
  | Snd of expr
  | Type
  | Bool
  | True
  | False
  | BoolElim of {
      motive_var : local_name;
      motive_body : expr;
      true_case : expr;
      false_case : expr;
      scrut : expr;
    }

and expr = raw_expr Asai.Range.located

type item =
  | Def of {
      name : name;
      args : arg List.t;
      tp : expr;
      tm : expr;
    }

type file = item List.t

let dump_name fmt ({ value; _ } : name) = Name.pp fmt value

let dump_local_name fmt ({ value; _ } : local_name) = match value with
  | Some name -> Format.pp_print_string fmt name
  | None -> Format.pp_print_char fmt '_'

let rec dump_arg fmt ((name, tp) : arg) =
  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_local_name name dump_expr tp

and dump_raw_expr fmt = function
  | Var name -> Format.fprintf fmt "Var @[%a@]" Name.pp name
  | Check (tm, tp) -> Format.fprintf fmt "@[%a@] : @[%a@]" dump_expr tm dump_expr tp
  | Bool -> Format.pp_print_string fmt "Bool"
  | True -> Format.pp_print_string fmt "True"
  | False -> Format.pp_print_string fmt "False"
  | BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
    Format.fprintf fmt
      "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]"
      dump_local_name motive_var
      dump_expr motive_body
      dump_expr true_case
      dump_expr false_case
      dump_expr scrut
  | Pi (dom, cod) ->
    Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
  | Fun (dom, cod) ->
    Format.fprintf fmt "@[<5>Fun (@[%a@],@ @[%a@])@]" dump_expr dom dump_expr cod
  | Lam (var, body) ->
    Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_local_name var dump_expr body
  | App (fn, arg) ->
    Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
  | Sg (fst, snd) ->
    Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd
  | Prod (fst, snd) ->
    Format.fprintf fmt "@[<6>Prod (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd
  | Pair (fst, snd) ->
    Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd
  | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p
  | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p
  | Type -> Format.pp_print_string fmt "Type"

and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value