BundleParser.sml

structure BundleParser :> BundleParser =
struct
  open HolKernel TypeBase Parse Term UIRLexer 
  open boolLib
  open finite_mapSyntax
  open listSyntax
  open pairSyntax
  open stringSyntax
  open sumSyntax
  open uvmErrorsTheory
  open uvmIRTheory
  open ParserHelpers
  open TypeParser
  open ValueParser
  open CodeParser

  val decls : string list = [
    "typedef", "const", "global", "funcsig", "funcdecl", "funcdef"
  ]

  val ty_env = mk_type("environment", [])
  val ty_bundle = ty_env --> or_error ty_env

  val ty_gln = mk_type("global_name", [])
  val ty_tyn = mk_type("type_name", [])
  val ty_sign = mk_type("sig_name", [])
  val ty_constn = mk_type("const_name", [])

  val t_env = mk_var("env", ty_env)

  (* Attempts to look up a member of one of the finite map fields of an
     ``:environment``. Assumes that t_env is already present in the current
     scope. Returns a term of type ``:^vty or_error``.
  *)
  fun get_env_member (field_name : string)
                     (kty : hol_type)
                     (vty : hol_type)
                     (key : term) : term =
    infer_comb("expect", [
      infer_comb("FLOOKUP", [
        infer_comb("environment_" ^ field_name, [t_env], mk_fmap_ty(kty, vty)),
        key
      ], mk_type("option", [vty])),
      infer_comb("InvalidIR",
        (* TODO: Include key in error message *)
        [fromMLstring (field_name ^ " lookup failed")],
        ty_err)
    ], or_error vty)

  fun get_env_type (name : string) : term =
    get_env_member "types" ty_tyn ty_type
      (infer_comb("TypeName", [fromMLstring name], ty_tyn))

  fun get_env_funcsig (name : string) : term =
    get_env_member "funcsigs" ty_sign ty_sig
      (infer_comb("SigName", [fromMLstring name], ty_sign))

  fun get_env_const (name : string) : term =
    mk_lift(
      mk_thy_const{Thy="pair", Name="SND", Ty=mk_prod(ty_type, ty_val) --> ty_val},
      get_env_member "constants" ty_constn (mk_prod(ty_type, ty_val))
        (infer_comb("ConstName", [fromMLstring name], ty_constn)))

  fun add_env_member (field_name : string)
                     (kty : hol_type)
                     (vty : hol_type)
                     (key : term)
                     (value : term) : term =
    let val t_f = mk_var("f", mk_fmap_ty(kty, vty)) in
      infer_comb("environment_" ^ field_name ^ "_fupd", [
        mk_abs(t_f,
          infer_comb("FUPDATE", [t_f, mk_pair(key, value)], mk_fmap_ty(kty, vty))),
        t_env
      ], ty_env)
    end

  fun add_env_type (name : string) (t : term) : term =
    add_env_member "types" ty_tyn ty_type
      (infer_comb("TypeName", [fromMLstring name], ty_tyn)) t

  fun add_env_funcsig (name : string) (s : term) : term =
    add_env_member "funcsigs" ty_sign ty_sig
      (infer_comb("SigName", [fromMLstring name], ty_sign)) s

  fun add_env_const (name : string) (ty : term) (value : term) : term =
    add_env_member "constants" ty_constn (mk_prod(ty_type, ty_val))
      (infer_comb("ConstName", [fromMLstring name], ty_constn)) (mk_pair(ty, value))

  val free_env_context = {
    get_type = get_env_type,
    get_funcsig = get_env_funcsig,
    get_global = get_env_const
  }

  type bundle = {
    types : term list,
    globals : term list,
    functions : term list
  }

  val empty_bundle : bundle = {
    types = [], globals = [], functions = []
  }

  fun parse_decl (lines : uir_token list list,
                  {types, globals, functions} : bundle)
                 : bundle =
    let
      val env = free_env_context
      val (header::other_lines) = filter (fn l => l <> []) lines
    in
      case header of
        Decl "typedef"::SSA (Global, name)::Eq::rhs =>
          if other_lines = [] then
            let
              val ty = mk_var("ty", ty_type)
              val def = mk_abs(t_env,
                mk_lift(mk_abs(ty, add_env_type name ty), parse_type env rhs))
            in
              {types = types @ [def], globals = globals, functions = functions}
            end
          else raise ParseError "non-declaration line after .typedef"
      | Decl "funcsig"::SSA (Global, name)::Eq::rhs =>
          if other_lines = [] then
            let
              val fs = mk_var("fs", ty_sig)
              val def = mk_abs(t_env,
                mk_lift(mk_abs(fs, add_env_funcsig name fs), parse_funcsig env rhs))
            in
              {types = types @ [def], globals = globals, functions = functions}
            end
          else raise ParseError "non-declaration line after .funcsig"
      | Decl "const"::SSA (Global, name)::Type ty::Eq::rhs =>
          (* TODO: Support multi-line constants (for structs, arrays, etc.) *)
          if other_lines = [] then
            let
              val ty' = mk_var("ty'", ty_type)
              val const = mk_var("const", ty_val)
              val def = mk_abs(t_env, 
                mk_bind(parse_type env ty,
                  mk_abs(ty', mk_lift(
                    mk_abs(const, add_env_const name ty' const),
                    beta_conv(mk_comb(parse_value rhs, ty'))))))
            in
              {types = types, globals = globals @ [def], functions = functions}
            end
          else raise ParseError "non-declaration line after .const"
      | [Decl "global", SSA (Global, name), Type ty] =>
          let
            val t_ty  = mk_var("ty", ty_type)
            val t_gln = infer_comb("Global", [fromMLstring name], ty_gln)
            val ty_gl = mk_prod(ty_gln, ty_type)
            val t_gls = mk_var("gls", ty_list ty_gl)
            val def = mk_abs(t_env, mk_lift(
              mk_abs(t_ty, 
                infer_comb("environment_globals_fupd", [
                  mk_abs(t_gls, infer_comb("CONS",
                    [mk_pair(t_gln, t_ty), t_gls], ty_list ty_gl)),
                  add_env_const name t_ty (infer_comb("RefV",
                    [t_ty, mk_some(infer_comb("GlobalAddr", [t_gln], ty_addr))], ty_val))
                ], ty_env)),
              parse_type env ty))
          in
            {types = types, globals = globals @ [def], functions = functions}
          end
      | [Decl "funcdecl", SSA (Global, name), Type fsig] =>
          (* TODO: funcdecl *)
          raise ParseError "funcdecl not yet supported"
      | [Decl "funcdef", SSA (Global, name), Word "VERSION", SSA (Local, v), Type fsig, OpenBrace] =>
          if exists (fn l => l = [CloseBrace]) other_lines then
            if List.last other_lines = [CloseBrace] then
              let
                val r = mk_const("REF", mk_type("ref_type", []))
                val ty_fno = mk_type("option", [ty_funcn])
                val fsig' = parse_funcsig env fsig
                val ty = mk_var("ty", ty_type)
                val fr = mk_var("fr", ty_val)
                val fref = mk_abs(t_env, list_mk_lift(
                  list_mk_abs([ty, fr], add_env_const name ty fr), [
                    mk_lift(infer_comb("FuncRef", [r], ty_sig --> ty_type), fsig'),
                    list_mk_lift(
                      infer_comb("FuncRefV", [r], ty_sig --> ty_fno --> ty_val), [fsig',
                        mk_return(infer_comb("SOME", [
                          infer_comb("Func", [fromMLstring name], ty_funcn)], ty_fno))])]))
                val fdef = mk_abs(t_env, mk_lift(
                  infer_comb("generate_function", [t_env, fromMLstring name],
                    mk_type("function", []) --> ty_env),
                  parse_func env fsig' (List.take(other_lines, length other_lines - 1))))
              in
                {types = types, globals = globals @ [fref], functions = functions @ [fdef]}
              end
            else raise ParseError "non-declaration line after .funcdef's }"
          else raise ParseError "unclosed { in .funcdef"
      | Decl d::_ =>
          if exists (fn x => x = d) decls then
            raise ParseError ("invalid parameters for ." ^ d)
          else
            raise ParseError ("." ^ d ^ " is not a toplevel declaration")
      | _ =>
          raise ParseError "expected toplevel declaration"
    end

  fun uir_bundle (quotation : 'a frag list) : term =
    let
      val ty_bind = or_error ty_env --> ty_bundle --> or_error ty_env
      val str = unquote_all quotation
      val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
      val decl_blocks = split_by_header (fn (Decl _::_) => true | _ => false)
        (filter (fn l => l <> []) lines)
      val {types, globals, functions} =
        foldl parse_decl empty_bundle decl_blocks
    in
      mk_abs(t_env, list_mk_comb(
        mk_thy_const{
          Thy="list",
          Name="FOLDL",
          Ty=ty_bind --> or_error ty_env --> ty_list ty_bundle --> or_error ty_env
        }, [
          mk_thy_const{Thy="sumMonad", Name="bind_left", Ty=ty_bind},
          mk_return t_env,
          mk_list(types @ globals @ functions, ty_bundle)
        ]))
    end
end