type raw_ident = string
type ident = raw_ident Asai.Range.located

type raw_arg = { name : ident; ty : expr }
and arg = raw_arg Asai.Range.located

and raw_expr =
  | Var of raw_ident
  | Pi of arg * expr
  | Lam of ident * expr
  | App of expr * expr
  | Sg of arg * expr
  | Pair of expr * expr
  | Fst of expr
  | Snd of expr
  | Type
  | Bool
  | True
  | False
  | BoolElim of {
      motive_var : ident;
      motive_body : expr;
      true_case : expr;
      false_case : expr;
      scrut : expr;
    }

and expr = raw_expr Asai.Range.located

let pp_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id
let pp_ident fmt ({ value; _ } : ident) = pp_raw_ident fmt value

let rec pp_raw_arg fmt ({ name; ty } : raw_arg) =
  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" pp_ident name pp_expr ty

and pp_arg fmt ({ value; _ } : arg) = pp_raw_arg fmt value

and pp_raw_expr fmt = function
  | Var id -> Format.fprintf fmt "Var @[%a@]" pp_raw_ident id
  | 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@])@]" pp_ident
        motive_var pp_expr motive_body pp_expr true_case pp_expr
        false_case pp_expr scrut
  | Pi (dom, cod) ->
      Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" pp_arg dom pp_expr cod
  | Lam (var, body) ->
      Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" pp_ident var pp_expr
        body
  | App (fn, arg) ->
      Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" pp_expr fn pp_expr arg
  | Sg (fst, snd) ->
      Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" pp_arg fst pp_expr snd
  | Pair (fst, snd) ->
      Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" pp_expr fst pp_expr
        snd
  | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" pp_expr p
  | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" pp_expr p
  | Type -> Format.pp_print_string fmt "Type"

and pp_expr fmt ({ value; _ } : expr) = pp_raw_expr fmt value