Re: [isabelle] BNFs and sort constraints



Hi Lars,

> Could somebody shed some light onto how this works? I looked at some of
> the papers but didn't find anything.

I can answer Observation 4, which involves some of my code.

BNF type variables may not have sort constraints. "map_id" is part of the BNF structure, so it accordingly doesn't have sort constraints. More high-level theorems and constants are declared with the sort constraints. To overgeneralize a bit, Dmitriy's low-level BNF code doesn't like sort constraints, whereas my higher-level "(co)datatype" code copes with them to the extent possible. In the code, you'll see this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML".

I presume there's no deep reason for not supporting syntactic type class constraints in BNFs. It would complicate the composition operators for sure, and in a bunch of places we'd have to discharge 0 goals arising from syntactic type class instantiations. If you're up for putting in the effort, we won't stop you.

Incidentally, what is the motivation for your example? Is your application related to item 5 in the "Known Bugs and Limitations" of the "datatypes" document?

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.