[isabelle] Trying to fix pretty printing for "syntax" & "translations"



Hi,

I used this from List.thy as a template:

syntax
  "_list" :: "args => 'a list"    ("[(_)]")
translations
  "[x, xs]" == "x#[xs]"
  "[x]" == "x#[]"

In the past, I've used this (without the "f" in the syntax), and the "value" commands below show that it preserves the braces syntax:

typedecl sT
consts upS :: "sT => sT => sT"
syntax "_upS" :: "args => sT" ("f\<lbrace>(_)\<rbrace>")
  translations
  "f\<lbrace>x,y\<rbrace>" == "CONST upS x y"
  "f\<lbrace>x\<rbrace>"   => "f\<lbrace>x,x\<rbrace>"
  value "f\<lbrace>x,y\<rbrace>"
  value "f\<lbrace>x\<rbrace>"

But I changed to where my function takes a "sT list", so I have this, and all my theorems work with it:

consts fiS :: "sT list => sT"
syntax "_fiS" :: "args => sT" ("\<lbrace>(_)\<rbrace>")
  translations
  "\<lbrace>x,xs\<rbrace>" == "CONST fiS (x # [xs])"
  "\<lbrace>x\<rbrace>"    => "\<lbrace>x,x\<rbrace>"
  value "\<lbrace>x,y,z\<rbrace>"
  value "\<lbrace>x\<rbrace>"

However, with this, the output of the "value" command shows that it doesn't preserve the braces syntax, and I get function notation like this:

"fiS [x, y, z]" :: "sT"

I haven't figure out how "syntax" works. I can change "args => sT list" to anything, like, "args => nat", and it doesn't make any difference.

I change "CONST fiS (x # [xs])" to "CONST fiS x # [xs]" and I get the braces in the output, but then the type is "sT list" instead of "sT".

I'm assuming it has something to do with the fact that "list" in List.thy already has "syntax" and "translations" used as shown above.

I include the complete theory below in case someone has time to tell me how to fix it.

Thanks,
GB


theory sTs__130201
imports Complex_Main
begin

typedecl sT
consts upS :: "sT => sT => sT"
syntax "_upS" :: "args => sT" ("f\<lbrace>(_)\<rbrace>")
  translations
  "f\<lbrace>x,y\<rbrace>" == "CONST upS x y"
  "f\<lbrace>x\<rbrace>"   => "f\<lbrace>x,x\<rbrace>"
  value "f\<lbrace>x,y\<rbrace>"
  value "f\<lbrace>x\<rbrace>"

consts fiS :: "sT list => sT"
syntax "_fiS" :: "args => sT" ("\<lbrace>(_)\<rbrace>")
  translations
  "\<lbrace>x,xs\<rbrace>" == "CONST fiS (x # [xs])"
  "\<lbrace>x\<rbrace>"    => "\<lbrace>x,x\<rbrace>"
  value "\<lbrace>x,y,z\<rbrace>"
  value "\<lbrace>x\<rbrace>"

end





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