code generator changes
authorhaftmann
Fri Apr 20 11:21:33 2007 +0200 (2007-04-20)
changeset 22735cf627add250a
parent 22734 790f73fa8b36
child 22736 4948e2bd67e5
code generator changes
NEWS
     1.1 --- a/NEWS	Fri Apr 20 10:09:32 2007 +0200
     1.2 +++ b/NEWS	Fri Apr 20 11:21:33 2007 +0200
     1.3 @@ -63,6 +63,14 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* code generator: 
     1.8 +  - Isar "definition"s and primitive instance definitions are added explicitly
     1.9 +    to the table of defining equations
    1.10 +  - primitive definitions are not unfolded by default any longer
    1.11 +  - defining equations are now definitly restricted to meta "==" and object
    1.12 +        equality "="
    1.13 +  - HOL theories have been adopted accordingly
    1.14 +
    1.15  * class_package.ML offers a combination of axclasses and locales to
    1.16  achieve Haskell-like type classes in Isabelle. See
    1.17  HOL/ex/Classpackage.thy for examples.
    1.18 @@ -74,6 +82,8 @@
    1.19          code_gen <list of constants (term syntax)> (SML #)
    1.20      writing SML code to a file:
    1.21          code_gen <list of constants (term syntax)> (SML <filename>)
    1.22 +    writing OCaml code to a file:
    1.23 +        code_gen <list of constants (term syntax)> (OCaml <filename>)
    1.24      writing Haskell code to a bunch of files:
    1.25          code_gen <list of constants (term syntax)> (Haskell <filename>)
    1.26  
    1.27 @@ -86,7 +96,7 @@
    1.28      [code inline]:    select an equation theorem for unfolding (inlining) in place
    1.29      [code noinline]:  deselect an equation theorem for unfolding (inlining) in place
    1.30  
    1.31 -User-defined serializations (target in {SML, Haskell}):
    1.32 +User-defined serializations (target in {SML, OCaml, Haskell}):
    1.33  
    1.34      code_const <and-list of constants (term syntax)>
    1.35        {(target) <and-list of const target syntax>}+
    1.36 @@ -102,10 +112,10 @@
    1.37        {(target) <and-list of class target syntax>}+
    1.38          where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
    1.39  
    1.40 -For code_instance and code_class, target SML is silently ignored.
    1.41 -
    1.42 -See HOL theories and HOL/ex/Code*.thy for usage examples.  Doc/Isar/Advanced/Codegen/
    1.43 -provides a tutorial.
    1.44 +code_instance and code_class only apply to target Haskell.
    1.45 +
    1.46 +See HOL theories and HOL/ex/Codegenerator*.thy for usage examples.
    1.47 +Doc/Isar/Advanced/Codegen/ provides a tutorial.
    1.48  
    1.49  * Command 'no_translations' removes translation rules from theory
    1.50  syntax.
    1.51 @@ -505,6 +515,9 @@
    1.52  
    1.53  *** HOL ***
    1.54  
    1.55 +* Library/Commutative_Ring.thy: switched from recdef to function package;
    1.56 +    constants add, mul, pow now curried.  Infix syntax for algebraic operations.
    1.57 +
    1.58  * Some steps towards more uniform lattice theory development in HOL.
    1.59  
    1.60      constants "meet" and "join" now named "inf" and "sup"