Mis-ordering of definitions in Coq output

[sweirich]

Sometimes we get Coq output that is not in dependency order for the grammar definitions.

For example, with this input file

grammar

sort :: '' ::=
   | Tm     ::    :: Tm

context, G :: 'ctx_' ::=  {{ coq list ( nat * sort ) }}
   | empty  ::    :: Empty {{ coq nil }}

role_sort :: '' ::=
   | Nm     ::    :: Nm

role_context, W :: 'rctx_'  ::=  {{ coq list ( nat * role_sort ) }}
   | emptyR ::    :: Empty  {{ coq nil }}

sig_sort :: '' ::=
   | Cs     ::    :: Cs

sig, S :: 'sig_' ::= {{ coq list (nat * sig_sort) }}
   | emptyS ::    :: Empty   {{ coq nil }}

and the command

huntsman-ve502-0054:Desktop sweirich$ ott -i TestOrderDep.ott -o TestOrderDep.v
Ott version 0.25   distribution of Thu Sep 4 18:04:34 BST 2014

I get the output

(* generated by Ott 0.25 from: TestOrderDep.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.

Inductive role_sort : Set := 
 | Nm : role_sort.

Inductive sort : Set := 
 | Tm : sort.

Definition sig : Set := list (nat * sig_sort).

Definition role_context : Set := list ( nat * role_sort ).

Definition context : Set := list ( nat * sort ).

Inductive sig_sort : Set := 
 | Cs : sig_sort.

But, this output does not compile with Coq because the definition of the sig_sort type comes after the definition of sig.

I'm not sure why this happens; we've tried minimizing the input and the problem sometimes goes away under some reorderings of the Ott grammar (should this matter?) or if we remove some of the grammar productions. However, it is unpredictable. Is there a workaround for this bug?

Thanks!

[PeterSewell]

Hi Stephanie,

On 27 October 2017 at 14:03, Stephanie Weirich notifications@github.com wrote:

Sometimes we get Coq output that is not in dependency order for the grammar definitions.

For example, with this input file

grammar

sort :: '' ::= | Tm :: :: Tm

context, G :: 'ctx_' ::= {{ coq list ( nat * sort ) }} | empty :: :: Empty {{ coq nil }}

role_sort :: '' ::= | Nm :: :: Nm

rolecontext, W :: 'rctx' ::= {{ coq list ( nat * role_sort ) }} | emptyR :: :: Empty {{ coq nil }}

sig_sort :: '' ::= | Cs :: :: Cs

sig, S :: 'sig_' ::= {{ coq list (nat * sig_sort) }} | emptyS :: :: Empty {{ coq nil }}

and the command

huntsman-ve502-0054:Desktop sweirich$ ott -i TestOrderDep.ott -o TestOrderDep.v Ott version 0.25 distribution of Thu Sep 4 18:04:34 BST 2014

I get the output

( generated by Ott 0.25 from: TestOrderDep.ott )

Require Import Arith. Require Import Bool. Require Import List.

Inductive role_sort : Set := | Nm : role_sort.

Inductive sort : Set := | Tm : sort.

Definition sig : Set := list (nat * sig_sort).

Definition role_context : Set := list ( nat * role_sort ).

Definition context : Set := list ( nat * sort ).

Inductive sig_sort : Set := | Cs : sig_sort.

But, this output does not compile with Coq because the definition of the sig_sort type comes after the definition of sig.

I'm not sure why this happens; we've tried minimizing the input and the problem sometimes goes away under some reorderings of the Ott grammar (should this matter?) or if we remove some of the grammar productions. However, it is unpredictable. Is there a workaround for this bug?

IIRC Ott doesn't try to look inside the coq type homs for extra dependencies, and in the productions here sig doesn't depend on sig_sort. Possible workarounds:

• add "-sort false" to the command line, to turn off topological sorting entirely
• add some fake productions that do introduce dependencies - then make them sugar productions and use -tex_suppress_ntr to make them go away in the output (bit horrid)
• invent a new kind of hom on rules to let the user add explicit dependency info.

do any of those suffice? best, Peter

Thanks!

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ott-lang/ott/issues/16, or mute the thread https://github.com/notifications/unsubscribe-auth/AErM5jTATnobzyoacrL2zC0yQOUb-35Hks5swdSEgaJpZM4QJBp- .

[francesco-zappa-nardelli]

Hi Stephanie & Peter & all

Sometimes we get Coq output that is not in dependency order for the grammar definitions.

IIRC Ott doesn't try to look inside the coq type homs for extra dependencies, and in the productions here sig doesn't depend on sig_sort.

Peter is right, this is the source of the problem.

I'm not sure why this happens; we've tried minimizing the input and the problem sometimes goes away under some reorderings of the Ott grammar (should this matter?) or if we remove some of the grammar productions. However, it is unpredictable. Is there a workaround for this bug?

I can see the usability nightmare here: Ott uses ocamlgraph to compute a topological sort of the dependency graph, it is likely that adding or removing one production results in wildly different sortings (should still be deterministic).

Possible workarounds:

• add "-sort false" to the command line, to turn off topological sorting entirely

Not sure this would work at all: if the development relies on Ott generated types, I wonder where these end up in the output.

• add some fake productions that do introduce dependencies - then make them sugar productions and use -tex_suppress_ntr to make them go away in the output (bit horrid)

• invent a new kind of hom on rules to let the user add explicit dependency info.

One more option:

• modify Ott to look into homs, and if by any chance any string in a hom looks like a non-terminal name, add implicitly a dependency?

-francesco

[PeterSewell]

On 28 October 2017 at 18:41, francesco-zappa-nardelli < notifications@github.com> wrote:

Hi Stephanie & Peter & all

Sometimes we get Coq output that is not in dependency order for the grammar definitions.

IIRC Ott doesn't try to look inside the coq type homs for extra dependencies, and in the productions here sig doesn't depend on sig_sort.

Peter is right, this is the source of the problem.

I'm not sure why this happens; we've tried minimizing the input and the problem sometimes goes away under some reorderings of the Ott grammar (should this matter?) or if we remove some of the grammar productions. However, it is unpredictable. Is there a workaround for this bug?

I can see the usability nightmare here: Ott uses ocamlgraph to compute a topological sort of the dependency graph, it is likely that adding or removing one production results in wildly different sortings (should still be deterministic).

Possible workarounds:

• add "-sort false" to the command line, to turn off topological sorting entirely

Not sure this would work at all: if the development relies on Ott generated types, I wonder where these end up in the output.

I'd expect in the same order as the source, but I didn't check.

• add some fake productions that do introduce dependencies - then make them sugar productions and use -tex_suppress_ntr to make them go away in the output (bit horrid)

• invent a new kind of hom on rules to let the user add explicit dependency info.

One more option:

• modify Ott to look into homs, and if by any chance any string in a hom looks like a non-terminal name, add implicitly a dependency?

Then we have to at least lex, if not parse, all the targets.

-francesco

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ott-lang/ott/issues/16#issuecomment-340207797, or mute the thread https://github.com/notifications/unsubscribe-auth/AErM5hKwKPpP5zTG_biwIj82aXX7gIMGks5sw2c3gaJpZM4QJBp- .

[didriklundberg]

In case someone else finds this helpful, I encountered a problem similar to the one above and solved it by inserting

embed
{{ coq

}}
grammar

between the problematic rules, i.e., in the example above this would be inserted between sig_sort and sig. I figure this works as a sort-of fence for reordering between the two grammar declarations on either side of the embed.