doc-src/Codegen/Thy/Adaptation.thy
changeset 39063 5f9692dd621f
parent 38506 03d767575713
child 39643 29cc021398fc
equal deleted inserted replaced
39062:9eb380ecf155 39063:5f9692dd621f
   270 
   270 
   271 subsection {* @{text Haskell} serialisation *}
   271 subsection {* @{text Haskell} serialisation *}
   272 
   272 
   273 text {*
   273 text {*
   274   For convenience, the default @{text HOL} setup for @{text Haskell}
   274   For convenience, the default @{text HOL} setup for @{text Haskell}
   275   maps the @{class eq} class to its counterpart in @{text Haskell},
   275   maps the @{class equal} class to its counterpart in @{text Haskell},
   276   giving custom serialisations for the class @{class eq} (by command
   276   giving custom serialisations for the class @{class equal} (by command
   277   @{command_def code_class}) and its operation @{const HOL.eq}
   277   @{command_def code_class}) and its operation @{const HOL.equal}
   278 *}
   278 *}
   279 
   279 
   280 code_class %quotett eq
   280 code_class %quotett equal
   281   (Haskell "Eq")
   281   (Haskell "Eq")
   282 
   282 
   283 code_const %quotett "op ="
   283 code_const %quotett "op ="
   284   (Haskell infixl 4 "==")
   284   (Haskell infixl 4 "==")
   285 
   285 
   286 text {*
   286 text {*
   287   \noindent A problem now occurs whenever a type which is an instance
   287   \noindent A problem now occurs whenever a type which is an instance
   288   of @{class eq} in @{text HOL} is mapped on a @{text
   288   of @{class equal} in @{text HOL} is mapped on a @{text
   289   Haskell}-built-in type which is also an instance of @{text Haskell}
   289   Haskell}-built-in type which is also an instance of @{text Haskell}
   290   @{text Eq}:
   290   @{text Eq}:
   291 *}
   291 *}
   292 
   292 
   293 typedecl %quote bar
   293 typedecl %quote bar
   294 
   294 
   295 instantiation %quote bar :: eq
   295 instantiation %quote bar :: equal
   296 begin
   296 begin
   297 
   297 
   298 definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
   298 definition %quote "HOL.equal (x\<Colon>bar) y \<longleftrightarrow> x = y"
   299 
   299 
   300 instance %quote by default (simp add: eq_bar_def)
   300 instance %quote by default (simp add: equal_bar_def)
   301 
   301 
   302 end %quote (*<*)
   302 end %quote (*<*)
   303 
   303 
   304 (*>*) code_type %quotett bar
   304 (*>*) code_type %quotett bar
   305   (Haskell "Integer")
   305   (Haskell "Integer")
   308   \noindent The code generator would produce an additional instance,
   308   \noindent The code generator would produce an additional instance,
   309   which of course is rejected by the @{text Haskell} compiler.  To
   309   which of course is rejected by the @{text Haskell} compiler.  To
   310   suppress this additional instance, use @{command_def "code_instance"}:
   310   suppress this additional instance, use @{command_def "code_instance"}:
   311 *}
   311 *}
   312 
   312 
   313 code_instance %quotett bar :: eq
   313 code_instance %quotett bar :: equal
   314   (Haskell -)
   314   (Haskell -)
   315 
   315 
   316 
   316 
   317 subsection {* Enhancing the target language context \label{sec:include} *}
   317 subsection {* Enhancing the target language context \label{sec:include} *}
   318 
   318