clarified header comments
authorhaftmann
Wed Oct 04 14:17:46 2006 +0200 (2006-10-04)
changeset 208559f60d493c8fe
parent 20854 f9cf9e62d11c
child 20856 9f7f0bf89e7d
clarified header comments
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Tools/codegen_consts.ML
src/Pure/Tools/codegen_data.ML
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Oct 04 14:17:38 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Oct 04 14:17:46 2006 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Code generator for inductive datatypes and type copies ("code types").
     1.8 +Code generator for inductive datatypes.
     1.9  *)
    1.10  
    1.11  signature DATATYPE_CODEGEN =
     2.1 --- a/src/HOL/Tools/typecopy_package.ML	Wed Oct 04 14:17:38 2006 +0200
     2.2 +++ b/src/HOL/Tools/typecopy_package.ML	Wed Oct 04 14:17:46 2006 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      ID:         $Id$
     2.5      Author:     Florian Haftmann, TU Muenchen
     2.6  
     2.7 -Introducing copies of types using trivial typedefs.
     2.8 +Introducing copies of types using trivial typedefs; datatype-like abstraction.
     2.9  *)
    2.10  
    2.11  signature TYPECOPY_PACKAGE =
     3.1 --- a/src/Pure/Tools/codegen_consts.ML	Wed Oct 04 14:17:38 2006 +0200
     3.2 +++ b/src/Pure/Tools/codegen_consts.ML	Wed Oct 04 14:17:46 2006 +0200
     3.3 @@ -2,8 +2,9 @@
     3.4      ID:         $Id$
     3.5      Author:     Florian Haftmann, TU Muenchen
     3.6  
     3.7 -Distinction of ad-hoc overloaded constants. Convenient data structures
     3.8 -for constants.
     3.9 +Identifying constants by name plus normalized type instantantiation schemes.
    3.10 +Type normalization is compatible with overloading discipline and user-defined
    3.11 +ad-hoc overloading. Convenient data structures for constants.
    3.12  *)
    3.13  
    3.14  signature CODEGEN_CONSTS =
     4.1 --- a/src/Pure/Tools/codegen_data.ML	Wed Oct 04 14:17:38 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_data.ML	Wed Oct 04 14:17:46 2006 +0200
     4.3 @@ -2,7 +2,8 @@
     4.4      ID:         $Id$
     4.5      Author:     Florian Haftmann, TU Muenchen
     4.6  
     4.7 -Basic code generator data structures; abstract executable content of theory.
     4.8 +Abstract executable content of theory. Management of data dependent on
     4.9 +executabl content.
    4.10  *)
    4.11  
    4.12  signature CODEGEN_DATA =
     5.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Wed Oct 04 14:17:38 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Wed Oct 04 14:17:46 2006 +0200
     5.3 @@ -2,7 +2,8 @@
     5.4      ID:         $Id$
     5.5      Author:     Florian Haftmann, TU Muenchen
     5.6  
     5.7 -Retrieving and structuring code function theorems.
     5.8 +Retrieving, normalizing and structuring code function theorems
     5.9 +in graph with explicit dependencies.
    5.10  *)
    5.11  
    5.12  signature CODEGEN_FUNCGR =
     6.1 --- a/src/Pure/Tools/codegen_names.ML	Wed Oct 04 14:17:38 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_names.ML	Wed Oct 04 14:17:46 2006 +0200
     6.3 @@ -3,7 +3,8 @@
     6.4      Author:     Florian Haftmann, TU Muenchen
     6.5  
     6.6  Name policies for code generation: prefixing any name by corresponding theory name,
     6.7 -conversion to alphanumeric representation. Mappings are incrementally cached.
     6.8 +conversion to alphanumeric representation, shallow name spaces.
     6.9 +Mappings are incrementally cached.
    6.10  *)
    6.11  
    6.12  signature CODEGEN_NAMES =
     7.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Oct 04 14:17:38 2006 +0200
     7.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Oct 04 14:17:46 2006 +0200
     7.3 @@ -2,8 +2,7 @@
     7.4      ID:         $Id$
     7.5      Author:     Florian Haftmann, TU Muenchen
     7.6  
     7.7 -Code generator from Isabelle theories to
     7.8 -intermediate language ("Thin-gol").
     7.9 +Code generator extraction kernel. Code generator Isar setup.
    7.10  *)
    7.11  
    7.12  signature CODEGEN_PACKAGE =
     8.1 --- a/src/Pure/Tools/codegen_thingol.ML	Wed Oct 04 14:17:38 2006 +0200
     8.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Wed Oct 04 14:17:46 2006 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4      ID:         $Id$
     8.5      Author:     Florian Haftmann, TU Muenchen
     8.6  
     8.7 -Intermediate language ("Thin-gol") for code extraction.
     8.8 +Intermediate language ("Thin-gol") representing extracted code.
     8.9  *)
    8.10  
    8.11  infix 8 `%%;