self-contained code modules for Haskell

--HG--
extra : rebase_source : a3b1eacb5c9dd9b269251b2329a9eed2ec8eb2da

explicit model concerning files of generated code

isabelle update -u control_cartouches;

tuned -- prefer GHC.print_codepoint;

clarified signature;

proper datatype for 8-bit characters

dedicated case option for code generation to Scala

--HG--
extra : rebase_source : f4d2da47982250c33b66f81d009da3f3d0b48bbd

for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness

--HG--
extra : rebase_source : e408c1077f16249a98b1375329604e6e90339e0c

@{command_spec} is superseded by @{command_keyword};

modernized and more uniform style

allow multiple inheritance of targets

--HG--
extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011

more correct precedence of do-notation

always annotate potentially polymorphic Haskell numerals

--HG--
extra : rebase_source : afdd470c78d704a706fe6d34761f4251b2b79ec0

tuned data structure

--HG--
extra : rebase_source : 7cc408d038ae0cb3e103cd433b0b20a81851b688

enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)

centralized upper/lowercase name mangling

--HG--
extra : rebase_source : 9afb0b542ffd66bd6bcf3a4990fe5063573500be

explicit option for "open" code generation

more fine-grain notion of export

formal markup for public ingredients

restoring ancient string_classes option

--HG--
extra : rebase_source : 9b03c8e4430cf8460e78a06b0b0a434d0faba6c7

method names in instance declarations are always unqualified

--HG--
extra : rebase_source : a7e123bbd89d38cc04042c93bf9379879ac237bf

more suitable names, without any notion of "activating"

less clumsy namespace

avoid (now superfluous) indirect passing of constant names

prefer explicit code symbol type over ad-hoc name mangling

more abstract declaration of unqualified constant names in code printing context

proper PIDE markup for codegen arguments;

explicit hint for domain of class parameters in instance statements

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

bookkeeping and input syntax for exact specification of names of symbols in generated code

--HG--
extra : rebase_source : 60e91890f26f4c44ec2fa3a5be594fa7f2c1bdd0

two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one

--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17

evaluation: allow multiple code modules

restrict unqualified imports from Haskell Prelude to a small set of fundamental operations

prefer records with speaking labels over deeply nested tuples

--HG--
extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0

dropped sort constraints on datatype specifications

dropped dead code

outer syntax command definitions based on formal command_spec derived from theory header declarations;

syntactic improvements and tuning names in the code generator due to Florian's code review

tune indenting

create central list for language extensions used by the haskell code generator

call ghc with -XEmptyDataDecls

removing previous crude approximation to add type annotations to disambiguate types

adding minimalistic implementation for printing the type annotations

adding the body type as well to the code generation for constants as it is required for type annotations of constants

changing const type to pass along if typing annotations are necessary for disambigous terms

do not call ghc with -fglasgow-exts

simplified Name.variant -- discontinued builtin fold_map;

replaced File.check by specific File.check_file, File.check_dir;
clarified File.full_path -- include parts of former Thy_Load.get_file;
simplified Thy_Load.check_file -- do not read/digest yet;
merged Thy_Load.check_thy/deps_thy -- always read text and parse header;
clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator;
Thy_Info.check_deps etc.: File.read exactly once;

cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
determine swipl_version at runtime;

allow spaces in executable names;
simplified generated bash scripts;

program is separate argument to serializer

allocate intermediate directories in module hierarchy

less ghc-specific pragma

more basic Isabelle_System.mkdir;

more explicit Isabelle_System operations;

toplevel deresolving for flat module name space

only write ghc pragma when writing to a file

dropped ancient deresolve_base; plain_const_syntax also needs modification of instance statement

moved flat_program to code_namespace

Haskell uses generic flat_program combinator

added generic flat_program procedure

dropped names from serializer interface

hand out deresolver from serializer invocation

dropped superfluous presentation names

manage statement selection for presentation wholly through markup

formal markup of generated code for statements

removed namespace stuff from code_printer

formal framework for presentation of selected statements

tuned internally and made smlnj happy

dropped single_module parameter

record argument for serializers

removed serializer interface redundancies

more coherent naming of syntax data structures

tuned

tuned

tuned

eliminated some obscure higher-order arguments

trailing newline by default

width is a formal parameter of serialization

code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin

tuned serializer interface

tuned

traling newline on standard output

another refinement chapter in the neverending numeral story

distinguish different classes of const syntax

more consistent spacing in generated monadic code

braced needed in layout-insensitive syntax

use generic description slot for formal code checking

formal slot for code checker

check without explicit path

dropped ancient in-place compilation of SML

checking generated code for various target languages

once more a try with mkdir_leaf

revert to plain for now mkdir

mkdir_leaf -- avoiding surprises with typos in user-given paths

more precise code

transitive superclasses were also only a misunderstanding

formal introduction of transitive superclasses

drop function definitions of combinators

formal introduction of case cong

more consistent naming aroud type classes and instances

brackify_infix etc.: no break before infix operator -- eases survival in Scala

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

enclose case expression in brackets

more coherent naming with ML serializer

context theorem is optional

code literals: distinguish numeral classes by different entries

more correct handling of empty functions

take care for destructive print mode properly using dedicated pretty builders

improved crude deriving_show inference

repaired accident: do not forget module contents if there are no imports

each import resides in its own line

tuned

dropped some unused bindings

--HG--
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML
extra : rebase_source : f9974e246b201df041a994a3a755319b83bce2a3

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

always be qualified -- suspected smartness in fact never worked as expected

tuned whitespace

dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology

intro_base_names combinator

dropped dead code

cleaned up fundamental iml term functions

all variable names are optional

variable names in abstractions are optional

simplified binding concept

uniformly capitialized names for subdirectories

--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML