| #
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
| #
515bdf02 |
|
14-Dec-2017 |
haftmann <none@none> |
dedicated case option for code generation to Scala
--HG--
extra : rebase_source : f4d2da47982250c33b66f81d009da3f3d0b48bbd
|
| #
430c70a9 |
|
02-Aug-2017 |
haftmann <none@none> |
tuned
--HG--
extra : rebase_source : 5fe223879d21e15dec10febab3da774a4ccafa27
|
| #
59dbe85e |
|
02-Aug-2017 |
haftmann <none@none> |
work around weakness in export calculation when generating OCaml code
--HG--
extra : rebase_source : 2dadb2d23e02c906488bff35c994b6011b208982
|
| #
1a3088a0 |
|
14-Jun-2016 |
haftmann <none@none> |
explicit resolution of ambiguous dictionaries
|
| #
6989cd63 |
|
29-May-2016 |
haftmann <none@none> |
do not export abstract constructors in code_reflect
|
| #
1c0ca99b |
|
18-Apr-2016 |
haftmann <none@none> |
environment variable check has become pointless after 771b8ad5c7fc
--HG--
extra : rebase_source : 0725d5a5ce69e28d0ecbf0059e71f11525dc4521
|
| #
b5235f1f |
|
13-Apr-2016 |
wenzelm <none@none> |
tuned;
|
| #
1f59160a |
|
16-Mar-2016 |
wenzelm <none@none> |
less physical "logic" argument, with option -l like "isabelle console" etc.;
|
| #
00eb33e4 |
|
09-Mar-2016 |
wenzelm <none@none> |
isabelle_process is superseded by "isabelle process" tool;
tuned tool usage;
misc updates and tuning of "system" manual;
--HG--
rename : bin/isabelle_process => lib/Tools/process
|
| #
069a632f |
|
09-Mar-2016 |
wenzelm <none@none> |
isabelle.Build uses ML_Process directly;
isabelle_process is for batch mode only;
removed unused feeder (already part of "isabelle console");
|
| #
8930b173 |
|
08-Mar-2016 |
haftmann <none@none> |
explicit record values for dictionary variables
|
| #
affdd36f |
|
03-Mar-2016 |
wenzelm <none@none> |
simplified;
|
| #
bed2392b |
|
29-Feb-2016 |
wenzelm <none@none> |
isabelle_process executable no longer supports writable heap images;
|
| #
b5ee6de0 |
|
06-Sep-2015 |
haftmann <none@none> |
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
with explicit regression setup
|
| #
a4bddffc |
|
28-Jan-2015 |
haftmann <none@none> |
string printing conformant to both (S)ML and Isabelle/ML
--HG--
extra : rebase_source : 9f97a23d95843152a39bc16ac8b015e5f3f5fb56
|
| #
0285f5b6 |
|
09-Jan-2015 |
haftmann <none@none> |
modernized and more uniform style
|
| #
0976a200 |
|
05-Dec-2014 |
haftmann <none@none> |
allow multiple inheritance of targets
--HG--
extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011
|
| #
b7f1a757 |
|
02-May-2014 |
haftmann <none@none> |
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
|
| #
5607f158 |
|
01-May-2014 |
haftmann <none@none> |
centralized upper/lowercase name mangling
--HG--
extra : rebase_source : 9afb0b542ffd66bd6bcf3a4990fe5063573500be
|
| #
32a521c9 |
|
27-Feb-2014 |
haftmann <none@none> |
amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
|
| #
217fdae1 |
|
23-Feb-2014 |
haftmann <none@none> |
keep only identifiers public which are explicitly requested or demanded by dependencies
|
| #
34a077b1 |
|
23-Feb-2014 |
haftmann <none@none> |
explicit option for "open" code generation
|
| #
672d641b |
|
23-Feb-2014 |
haftmann <none@none> |
tuned
|
| #
950cc03c |
|
23-Feb-2014 |
haftmann <none@none> |
more fine-grain notion of export
|
| #
8b24d313 |
|
23-Feb-2014 |
haftmann <none@none> |
formal markup for public ingredients
|
| #
db656806 |
|
23-Feb-2014 |
haftmann <none@none> |
dropped long-unused option
|
| #
efe3ed51 |
|
21-Feb-2014 |
haftmann <none@none> |
dropped dead code
|
| #
07ad0bb4 |
|
25-Jan-2014 |
haftmann <none@none> |
less clumsy namespace
|
| #
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
| #
85e946f2 |
|
25-Jan-2014 |
haftmann <none@none> |
more abstract declaration of unqualified constant names in code printing context
|
| #
3e492425 |
|
04-Jul-2013 |
haftmann <none@none> |
explicit hint for domain of class parameters in instance statements
|
| #
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
| #
8efa9794 |
|
24-May-2013 |
haftmann <none@none> |
bookkeeping and input syntax for exact specification of names of symbols in generated code
--HG--
extra : rebase_source : 60e91890f26f4c44ec2fa3a5be594fa7f2c1bdd0
|
| #
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
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
|
| #
7b856d91 |
|
13-Feb-2013 |
haftmann <none@none> |
another attempt for a uniform abort on code generation errors
|
| #
250a6691 |
|
27-Dec-2012 |
haftmann <none@none> |
more explicit name
|
| #
b9e867a7 |
|
17-Nov-2012 |
wenzelm <none@none> |
more portable process exit;
|
| #
1c7c2719 |
|
07-Nov-2012 |
haftmann <none@none> |
restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
restore more conventional namespace during check (relevant for Imperative-HOL)
|
| #
c3e8fd6a |
|
27-Jul-2012 |
haftmann <none@none> |
evaluation: allow multiple code modules
|
| #
dc977d45 |
|
04-Jun-2012 |
haftmann <none@none> |
prefer records with speaking labels over deeply nested tuples
--HG--
extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0
|
| #
8ceda7e9 |
|
28-May-2012 |
haftmann <none@none> |
dropped sort constraints on datatype specifications
|
| #
070c6dd5 |
|
19-Apr-2012 |
haftmann <none@none> |
dropped dead code
|
| #
d8b8c922 |
|
19-Apr-2012 |
haftmann <none@none> |
dropped dead code;
tuned
--HG--
extra : rebase_source : 3548e686e93188249306305b2ce26a36c18ce819
|
| #
5a712294 |
|
20-Sep-2011 |
bulwahn <none@none> |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
| #
20767fdb |
|
07-Sep-2011 |
bulwahn <none@none> |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
| #
0b9a2ceb |
|
07-Sep-2011 |
bulwahn <none@none> |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
| #
3922aad1 |
|
09-Jun-2011 |
bulwahn <none@none> |
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
|
| #
1a5a42ee |
|
09-Jun-2011 |
wenzelm <none@none> |
simplified Name.variant -- discontinued builtin fold_map;
|
| #
283d71ab |
|
02-May-2011 |
bulwahn <none@none> |
improving naming of fresh variables in OCaml serializer
|
| #
b82e3883 |
|
13-Mar-2011 |
wenzelm <none@none> |
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
determine swipl_version at runtime;
|
| #
9ad65a83 |
|
13-Mar-2011 |
wenzelm <none@none> |
allow spaces in executable names;
simplified generated bash scripts;
|
| #
98274748 |
|
21-Dec-2010 |
haftmann <none@none> |
program is separate argument to serializer
|
| #
095d592f |
|
13-Dec-2010 |
haftmann <none@none> |
separated dictionary weakning into separate type
|
| #
e48262e7 |
|
09-Dec-2010 |
haftmann <none@none> |
dictionary constants must permit explicit weakening of classes;
tuned names
|
| #
14e6bac1 |
|
19-Nov-2010 |
wenzelm <none@none> |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
| #
dfb16b2f |
|
04-Sep-2010 |
haftmann <none@none> |
printing combinator for hierarchical programs
|
| #
e0e92b2c |
|
04-Sep-2010 |
haftmann <none@none> |
dropped names from serializer interface
|
| #
6d96da30 |
|
02-Sep-2010 |
haftmann <none@none> |
hand out deresolver from serializer invocation
|
| #
1d35f8ec |
|
02-Sep-2010 |
haftmann <none@none> |
swapped slip
|
| #
fef022c6 |
|
02-Sep-2010 |
haftmann <none@none> |
restored and added surpression of case combinators
|
| #
29dcd16b |
|
02-Sep-2010 |
haftmann <none@none> |
dropped superfluous presentation names
|
| #
c63f8622 |
|
02-Sep-2010 |
haftmann <none@none> |
manage statement selection for presentation wholly through markup
|
| #
760b2c60 |
|
02-Sep-2010 |
haftmann <none@none> |
formal markup of generated code for statements
|
| #
6d9e22df |
|
01-Sep-2010 |
haftmann <none@none> |
formal framework for presentation of selected statements
|
| #
ad0c4d3d |
|
02-Sep-2010 |
haftmann <none@none> |
dropped dead code; tuned
|
| #
93091375 |
|
02-Sep-2010 |
haftmann <none@none> |
use code_namespace module for SML and OCaml code
|
| #
94cad23a |
|
01-Sep-2010 |
haftmann <none@none> |
tuned internally and made smlnj happy
|
| #
bc797659 |
|
31-Aug-2010 |
haftmann <none@none> |
avoid strange special treatment of empty module names
|
| #
13daea3e |
|
31-Aug-2010 |
haftmann <none@none> |
dropped single_module parameter
|
| #
c2bf7b3b |
|
31-Aug-2010 |
haftmann <none@none> |
record argument for serializers
|
| #
df6809b2 |
|
31-Aug-2010 |
haftmann <none@none> |
removed serializer interface redundancies
|
| #
7a8d28bc |
|
31-Aug-2010 |
haftmann <none@none> |
more coherent naming of syntax data structures
|
| #
badd5aa1 |
|
31-Aug-2010 |
haftmann <none@none> |
Code_Printer.tuplify
|
| #
4c26294e |
|
31-Aug-2010 |
haftmann <none@none> |
dropped legacy interfaces
|
| #
0017b558 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
82283147 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
7faeece9 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
fa897977 |
|
30-Aug-2010 |
haftmann <none@none> |
eliminated some obscure higher-order arguments
|
| #
8ee2a45e |
|
30-Aug-2010 |
haftmann <none@none> |
width is a formal parameter of serialization
|
| #
93bcf928 |
|
30-Aug-2010 |
haftmann <none@none> |
code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
|
| #
019ea561 |
|
26-Aug-2010 |
haftmann <none@none> |
proper passing of optional module name
|
| #
6ab291e0 |
|
26-Aug-2010 |
haftmann <none@none> |
tuned serializer interface
|
| #
166cb6bc |
|
25-Aug-2010 |
haftmann <none@none> |
private version of commas, cf. printmode
|
| #
f9e73cbd |
|
28-Jul-2010 |
haftmann <none@none> |
rebinding ref is illegal
|
| #
1ad44b2b |
|
24-Jul-2010 |
haftmann <none@none> |
another refinement chapter in the neverending numeral story
|
| #
6728ff4f |
|
14-Jul-2010 |
haftmann <none@none> |
use generic description slot for formal code checking
|
| #
c54f63c8 |
|
14-Jul-2010 |
haftmann <none@none> |
formal slot for code checker
|
| #
134c2b0f |
|
14-Jul-2010 |
haftmann <none@none> |
check without explicit path
|
| #
b5520044 |
|
08-Jul-2010 |
haftmann <none@none> |
dropped ancient in-place compilation of SML
|
| #
515be4d6 |
|
08-Jul-2010 |
haftmann <none@none> |
checking generated code for various target languages
|
| #
293b817b |
|
17-Jun-2010 |
haftmann <none@none> |
more precise code
|
| #
3032d8aa |
|
17-Jun-2010 |
haftmann <none@none> |
transitive superclasses were also only a misunderstanding
|
| #
233f64f3 |
|
17-Jun-2010 |
haftmann <none@none> |
formal introduction of transitive superclasses
|
| #
7f4e9daa |
|
17-Jun-2010 |
haftmann <none@none> |
dropped obscure type argument weakening mapping -- was only a misunderstanding
|
| #
d7eae967 |
|
15-Jun-2010 |
haftmann <none@none> |
drop function definitions of combinators
|
| #
93fbbd8f |
|
15-Jun-2010 |
haftmann <none@none> |
formal introduction of case cong
|
| #
5c97a57f |
|
07-Jun-2010 |
haftmann <none@none> |
more consistent naming aroud type classes and instances
|
| #
7828de15 |
|
01-Jun-2010 |
haftmann <none@none> |
brackify_infix etc.: no break before infix operator -- eases survival in Scala
|
| #
c05a2b45 |
|
29-Apr-2010 |
haftmann <none@none> |
fixed underscore typo
|
| #
a9c6d942 |
|
28-Apr-2010 |
haftmann <none@none> |
exported print_tuple
|
| #
3161d8fa |
|
19-Feb-2010 |
haftmann <none@none> |
context theorem is optional
|
| #
a22630a8 |
|
22-Jan-2010 |
haftmann <none@none> |
code literals: distinguish numeral classes by different entries
|
| #
bd3d2740 |
|
04-Jan-2010 |
haftmann <none@none> |
dropped redundant name declarations
|
| #
f91f53e6 |
|
23-Dec-2009 |
haftmann <none@none> |
take care for destructive print mode properly using dedicated pretty builders
|
| #
0a04845e |
|
11-Dec-2009 |
haftmann <none@none> |
default_code_width is now proper theory data
|
| #
71ba7350 |
|
08-Dec-2009 |
haftmann <none@none> |
simplified notion of empty module name
|
| #
f62da38e |
|
07-Dec-2009 |
haftmann <none@none> |
split off evaluation mechanisms in separte module Code_Eval
--HG--
rename : src/Tools/Code/code_ml.ML => src/Tools/Code/code_eval.ML
|
| #
afa4190e |
|
04-Dec-2009 |
haftmann <none@none> |
signatures for generated code; tuned
|
| #
731e0eac |
|
12-Nov-2009 |
haftmann <none@none> |
accomplish mutual recursion between fun and inst
|
| #
dfa769e1 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Generic_Data, Proof_Data;
tuned;
|
| #
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
| #
cdb821b6 |
|
13-Oct-2009 |
haftmann <none@none> |
tuned whitespace
|
| #
3be2cdc1 |
|
14-Oct-2009 |
haftmann <none@none> |
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
|
| #
8bf989cc |
|
12-Oct-2009 |
haftmann <none@none> |
intro_base_names combinator
|
| #
8f48396e |
|
11-Oct-2009 |
haftmann <none@none> |
factored out Code_Printer.aux_params
|
| #
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
| #
58689e08 |
|
21-Jul-2009 |
haftmann <none@none> |
integrated add_triv_classes into evaluation stack
|
| #
392b8944 |
|
03-Jul-2009 |
haftmann <none@none> |
cleaned up fundamental iml term functions
|
| #
d811f2f3 |
|
30-Jun-2009 |
haftmann <none@none> |
all variable names are optional
|
| #
4f0af429 |
|
30-Jun-2009 |
haftmann <none@none> |
simplified binding concept
|
| #
d18d6a07 |
|
22-Jun-2009 |
haftmann <none@none> |
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
|