Automatically generating Coq/Gallina code

Ecosystem
, ,
1

I’m trying to lift code from a low-level language into Gallina. My desired pipeline is:

  1. Read low-level code into AST
  2. Convert AST into Gallina AST
  3. Generate string repr of Gallina AST and print

I’ve already finished step 1, and have started digging around Coq’s sources to try and find an AST definition to reuse. I could define my own but I don’t think that’ll be as robust. On the other hand, There are a limited number of features I’d need so using Coq’s AST definition might be overcomplicated.

Regardless, I’d like to explore the option, but have noticed that Coq’s term.ml file doesn’t contain the “standard” AST definition you’d see when using OCaml for a language implementation:

type term = Integer of int | Identifier of string | Assignment of (string * term)

I’m not surprised given how complex the language is. But is there any standard way I can interface with the official description of Coq in a structured form?

2

Update: I’m able to inject simple definitions into the context, but I’ve hit a number of roadblocks with my approach:

let converter_test () =
  init_coq () ;
  let env = Global.env () in
  let sigma = Evd.from_env env in
  (* Create an identifier for the variable x *)
  let x_ident = Id.of_string "x" in
  (* let term = Constrexpr.String "Hello World!" in *)
  let term =
    Constrexpr.Number
      (NumTok.SPlus, NumTok.Unsigned.parse (Stream.of_string "5"))
  in
  (* Declare the definition in the environment *)
  let poly = true in
  let sigma, t =
    Constrintern.interp_constr_evars env sigma
      (CAst.make (Constrexpr.CPrim term))
  in
  let five_ref = declare_definition ~poly x_ident sigma t in
  (* Print the environment to see the effect *)
  let print r =
    Pp.app (Pp.strbrk "Defined ") (Pp.app (Printer.pr_global r) (Pp.strbrk "."))
  in
  print_endline (Pp.db_string_of_pp (print five_ref)) ;
  try
    let t =
      simple_body_access (Nametab.global (Libnames.qualid_of_string "x"))
    in
    Feedback.msg_notice (Printer.pr_econstr_env env sigma t) ;
    print_endline (Pp.db_string_of_pp (Printer.pr_econstr_env env sigma t))
  with Failure s -> CErrors.user_err (Pp.str s)

The biggest right now is printing this out as legal Gallina code, it seems like I’ve taken a wrong step in an effort to get something working. Another is imports: the coq-core documentation doesn’t talk about import statements, the closest I can find is scoping information, which doesn’t seem tied to the global environment for some reason. I was hoping the documentation would be more complete than this, but it does seem like I’m well outside of the general use-case for the API. The plugin tutorials have been a big help but are still fairly limited.

3

Are you trying to generate a user syntax term (constrexpr) or a kernel term (constr)?

4

@SkySkimmer I guess I’m not sure. The snippet above is me trying to get a hello world to compile. I just want whatever will work best for my use case listed above.