Cannot generate menhir parser when using locally nameless

[dorchard]

I'm using the locally nameless approach as it makes a bunch of stuff work a lot better for me in Rocq. But I'd also like to be able to get the menhir parser, however, they seem incompatible.

MWE:

embed
{{ coq
Require Import String.
Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Metalib.Metatheory.
Open Scope string_scope.

}}

metavar x ::= {{ repr-locally-nameless }} {{ com  term variable  }}
indexvar index, i, n, m ::= {{ coq nat }}

grammar

t , v :: 'Term_' ::=  {{ com Terms }}
  | t1 t2   :: :: App {{ com Application }} 
  | \ x . t :: :: Abs (+ bind x in t +) {{ com Function }} {{ tex \lambda [[ x ]] . [[ t ]] }}
  | x       :: :: Var {{ com Variable }}
  | unit    :: :: Unit {{ com Unit expression }}

% Meta operations
 | { t1 / x } t2        :: M :: tsub    {{ coq (open_t_wrt_t [[t1]] [[x  t2]]) }} {{ ocaml [[t2]] }}

  | ( t ) :: M :: Bracket
    {{ com Bracketing }}
    {{ coq [[t]] }}
    {{ ocaml [[t]] }}

Running:

ott -i system.ott -o system_ast.ml -o system_parser.mly -picky_multiple_parses false 2>&1

Produces:

Ott version 0.34   distribution of Mon Dec 30 10:12:45 GMT 2024
Error: internal: pp_systemdefn_core_io, locally nameless with a non-coq backend

[PeterSewell]

In the menhir experiment, I didn't try to make those work together, sorry. I don't know what would be involved - probably non-trivial but not huge.

[dorchard]

I can have a go after the ICFP deadline...