#
3cb11ab1 |
|
16-Jun-2019 |
haftmann <none@none> |
more correct indicator --HG-- extra : rebase_source : ed57e2ab66df9a3711f69615a5e9611c8277b099
|
#
41867c3a |
|
22-Mar-2019 |
wenzelm <none@none> |
workaround for the sake of Windows;
|
#
d2bb940c |
|
20-Mar-2019 |
wenzelm <none@none> |
access OCaml tools and libraries via ISABELLE_OCAMLFIND; OPAM setup is optional: it requires odd development tools that are not available in default OS installations (e.g. make, m4); --HG-- rename : lib/scripts/ocamlexec => lib/scripts/ocamlfind
|
#
e4f9fed8 |
|
14-Mar-2019 |
haftmann <none@none> |
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
|
#
a7c0e049 |
|
10-Mar-2019 |
haftmann <none@none> |
migrated from Nums to Zarith as library for OCaml integer arithmetic --HG-- extra : rebase_source : 9da06716fa2cece20a04b2b74f042738c493e925
|
#
fc0f183a |
|
25-Jan-2019 |
haftmann <none@none> |
prefer proper strings in OCaml
|
#
28b11dd3 |
|
09-Jan-2019 |
haftmann <none@none> |
explicit model concerning files of generated code
|
#
220aa276 |
|
30-Oct-2018 |
wenzelm <none@none> |
clarified signature;
|
#
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
|