Locally Nameless Coq export: allow embed-like functionality that exports before ott commands (instead of after)

[sweirich]

This is similar to a related non-issue for LaTeX. However, I don't have a good workaround other than a call to sed in my Makefile.

I'd like to be able to add Coq imports that I use for meta productions in my grammar. For example, I have a system that is parameterized over an arbitrary lattice and I've specified the properties of this lattice in a separate module. Then I have a grammar element that uses lattice operations.

grammar 

grade, psi, phi :: 'q_' ::=   {{ coq grade }}
  | top                           :: M :: Top {{ tex { \color{black}{\top} } }} {{ coq q_Top }}
  | bot                           :: M :: Bot {{ tex { \color{black}{\bot} } }} {{ coq q_Bot }}
  | psi1 \/ psi2               :: M :: Join {{ tex [[psi1]] \vee [[psi2]] }} {{ coq (q_join [[psi1]] [[psi2]]) }}
  | psi1 /\ psi2               :: M :: Meet {{ tex [[psi1]] \wedge [[psi2]] }} {{ coq (q_meet [[psi1]] [[psi2]]) }}
  | ( psi )                       :: M :: paren {{ tex [[ psi ]] }} {{ coq ([[psi]]) }}

What I need is a way to import this library Require Export Qual.grade_sig. before the grammar definitions.

[palmskog]

Maybe I'm missing something, but why not use embed before grammar, as in the following:

embed
{{ coq
Require Export Qual.grade_sig.
}}

grammar 

grade, psi, phi :: 'q_' ::=   {{ coq grade }}
  | top                           :: M :: Top {{ tex { \color{black}{\top} } }} {{ coq q_Top }}
...

For me, this always makes my Require Import commands end up in the right place in exported Coq files.

[sweirich]

When I try that with the locally nameless backend, the import shows up after the definition of substitution.

[palmskog]

In that case, this sounds to me like bug specific to the locally nameless backend and Coq exporter. Maybe you can edit the issue name to reflect this?

[sweirich]

Done

[palmskog]

Thanks, I did a pass over that export code a while ago, so I might take a look at it in the near future. From memory, the problem is that there is an OCaml string that accumulates all the locally nameless Coq definitions which is treated differently from other kinds of embeds, etc.

[rogerbosman]

I think the problem is a bit bigger than just the very top of the file, the locations of any embed block is no longer respected with the LN backend as far as I can determine with my testing. This also introduces problems like no longer being able to define something like Definition Fresh a Env := (InEnv a Env -> False) where InEnv is defined above the embed block, and Fresh is used in productions after. Defining this using a formula is possible, but then the definitions will use the rhs instead of the definition itself

[palmskog]

@sweirich it turns out there is an undocumented coq-preamble directive that appears to solve your problems. Can you please try the following and see how it works out:

embed
{{ coq-preamble
Require Export Qual.grade_sig.
}}

grammar 

grade, psi, phi :: 'q_' ::=   {{ coq grade }}
  | top                           :: M :: Top {{ tex { \color{black}{\top} } }} {{ coq q_Top }}
...

[sweirich]

That works! Thanks.

[palmskog]

Great. Then I will take the liberty to close this issue and open a new one on the missing documentation of coq-preamble, hol-preamble, and isa-preamble. Actually, there is already some paragraph in the manual, but it's commented out.