structure ParserHelpers :> ParserHelpers =
struct
  open HolKernel Term Parse TypeBase
  open sumSyntax
  open listSyntax
  open sumMonadTheory
  open uvmTypesTheory
  open uvmErrorsTheory
  open uvmValuesTheory
  open uvmMemoryTheory

  exception ParseError of string
  type env_context = {
    get_type: string -> term,
    get_funcsig: string -> term,
    get_global: string -> term
  }

  val mock_context = {
    get_type = fn _ => ``ARB``,
    get_funcsig = fn name =>
      case name of
        "sig" => ``OK (<| arg_types := []; return_types := [] |>): funcsig or_error``
      | _ => ``ARB``,
    get_global = fn _ => ``ARB``
  }
  
  val ty_num = mk_type("num", [])
  val ty_str = ``:string``
  val ty_type = mk_type("uvm_type", [])
  val ty_reft = mk_type("ref_type", [])
  val ty_sig  = mk_type("funcsig", [])
  val ty_addr = mk_type("addr", [])
  val ty_funcn = mk_type("func_name", [])
  val ty_sid = mk_type("stack_id", [])
  val ty_tid = mk_type("thread_id", [])
  val ty_iaddr = mk_type("gen_iaddr", [ty_addr])
  val ty_err = mk_type("gen_uvm_error", [ty_addr, ty_funcn])
  val ty_val = mk_type("gen_value", [ty_addr, ty_funcn, ty_sid, ty_tid])
  fun ty_list ty = mk_type("list", [ty])
  fun or_error ty = sumSyntax.mk_sum(ty, ty_err)
  
  fun infer_comb(name : string, args : term list, out_ty : hol_type) =
    let
      val ty = foldr (op -->) out_ty (map type_of args)
      val f = mk_const(name, ty) handle HOL_ERR err => (
        print ("\nTYPE ERROR for " ^ name);
        print ("\nInvalid type: " ^ type_to_string ty);
        print "\nArgs:";
        List.app (fn t => print ("\n -  " ^ term_to_string t)) args;
        print "\n";
        raise HOL_ERR {
          message="Function " ^ name ^ " is not of type " ^ type_to_string ty,
          origin_function="infer_comb",
          origin_structure="ParseUIR"
        })
    in list_mk_comb(f, args) end

  fun mk_some x =
    let val ty = type_of x
    in mk_comb(mk_const("SOME", ty --> mk_type("option", [ty])), x) end

  fun mk_return t = infer_comb("INL", [t], or_error (type_of t))

  fun mk_bind(lhs, rhs) =
    let val (_, ty_out) = strip_fun (type_of rhs) in
      infer_comb("bind_left", [lhs, rhs], ty_out)
    end

  fun mk_sequence(xs, ty) =
    infer_comb("sequence_left", [mk_list(xs, or_error ty)], or_error (ty_list ty))

  local open List in
    fun mk_lift(f, x) =
      let
        val (ty_f_init, ty_f_last) = strip_fun(type_of f)
        val ty_out = foldr (op -->) ty_f_last (drop(ty_f_init, 1))
      in
        infer_comb("lift_left", [f, x], or_error ty_out)
      end

    fun list_mk_lift(f, (x::ys)) =
          let val (ty_ins, ty_out) = strip_fun (type_of f) in
            foldl
              (fn ((arg, ty), acc) => list_mk_comb(
                mk_thy_const{
                  Thy="sumMonad",
                  Name="ap_left",
                  Ty=type_of acc --> type_of arg --> or_error ty
                }, [acc, arg]))
              (mk_lift(f, x))
              (tabulate(length ys, fn n => (
                nth(ys, n),
                foldr (op -->) ty_out (drop(ty_ins, n+2)))))
          end
      | list_mk_lift(f, []) = mk_return f

    fun lift_record(ty : hol_type, fields : (string * term) list) =
      let
        val vs = map (fn (s, t) => mk_var(s, #1 (sumSyntax.dest_sum (type_of t)))) fields
      in
        list_mk_lift(
          list_mk_abs(vs, mk_record(ty, tabulate(length fields,
            fn n => (#1 (nth(fields, n)), nth(vs, n))))),
          map #2 fields)
      end
  end

  fun ty_pat (name : string) (xs : term list) =
    list_mk_comb(mk_thy_const{
      Thy="uvmTypes", Name=name, Ty=foldr (op -->) ty_type (map type_of xs)
    }, xs)

  (* Converts a QUOTE into a string, removing the leading location comment *)
  fun unquote (QUOTE str) = (
        case CharVector.findi (fn (_, c) => c = #")") str of
          SOME (i, _) => String.extract(str, i + 1, NONE)
        | NONE => str)
    | unquote (ANTIQUOTE _) = raise ParseError "antiquote not supported"

  (* Unquotes and concatenates a list of QUOTEs. *)
  fun unquote_all (quotes : 'a frag list) : string =
    String.concat (map unquote quotes)

  exception StartsWithNonHeader

  fun split_by_header (is_header : 'a -> bool) (xs : 'a list) : 'a list list =
    let
      fun split_fold ((next, (acc, out)) : 'a * ('a list * 'a list list))
                     : 'a list * 'a list list =
        if is_header next then ([], (next::acc)::out) else (next::acc, out)
      val (remaining : 'a list, out : 'a list list) =
        List.foldr split_fold ([], []) xs
    in
      case remaining of [] => out | _ => raise StartsWithNonHeader
    end
end