Haskell2Isabelle: treatment of (non-)strict datatypes and newtypes

[till]

As explained in the Haskell report, section 4.2.3, the following four Haskell declarations

 data D1 = D1 Int
 data D2 = D2 !Int
 type S = Int
 newtype N = N Int

have four different semantics. Indeed, the correct translation to Isabelle is as follows:

domain D1 = D1 (lazy D1_1::"dInt")
domain D2 = D2 (D2_1::"dInt")
types S = "dInt"
pcpodef N = "{x:: dInt . True}"
by auto

The "constructor" for N is Abs_N, the selector Rep_N. Patterns involving the constructor N must be translated to variables. The encapsulated value can be obtained by applying the selector (Rep_N) to the variable. The complete example and the correct translation is attached.

[till]

Haskell source from Haskell report, section 4.2.3

[till]

intended translation to Isabelle/HOLCF