Translation Tables

A translation table for Specware types and ops is introduced by a line beginning proof Isa Thy_Morphism followed optionally by an Isabelle theory (which will be imported into the translated spec), and terminated by the string end-proof. Each line gives the translation of a type or op. For example, for the Specware Integer theory we have:

proof Isa Thy_Morphism Presburger type Integer.Integer -> int type Integer.Nat -> nat (int,nat) [+,*,div,rem,<=,<,>=,>,abs,min,max] Integer.+ -> + Left 25 Integer.- -> - Left 25 IntegerAux.- -> - Integer.* -> * Left 27 Integer.div -> * Left 27 Integer.rem -> * Left 27 Integer.<= -> \<le> Left 20 Integer.< -> < Left 20 Integer.>= -> \<ge> Left 20 Integer.> -> > Left 20 Integer.min -> min curried Integer.max -> max curried end-proof

A type translation begins with the word type followed by the fully-qualified Specware name, -> and the Isabelle name. If the Specware type is a sub-type, you can specify coercion functions to and from the super-type in parentheses separated by commas. Note that by default, sub-types are represented by their super-type, so you would only specify a translation if you wanted them to be different, in which case coercion functions are necessary. Following the coercions functions can appear a list of overloaded functions within square brackets. These are used to minimize coercions back and forth between the two types.

An op translation begins with the fully-qualified Specware name, followed by -> and the Isabelle constant name. If the Isabelle constant is an infix operator, then it should be followed by Left or Right depending on whether it is left or right associative and a precedence number. Note that the precedence number is relative to Specware's precedence ranking, not Isabelle's. Also, an uncurried Specware op can be mapped to a curried Isabelle constant by putting curried after the Isabelle name, and a binary op can be mapped with the arguments reversed by appending reversed to the line.