# HG changeset patch # User Andreas Lochbihler # Date 1526535753 -7200 # Node ID 5859c688102a335acc2edd7580cac425b4483982 # Parent f551dd2178ab9ac37c5a3d7e74b9127d613b4c67 NEWS and CONTRIBUTORS for 8b50f29a1992 diff -r f551dd2178ab -r 5859c688102a CONTRIBUTORS --- a/CONTRIBUTORS Wed May 16 23:13:33 2018 +0200 +++ b/CONTRIBUTORS Thu May 17 07:42:33 2018 +0200 @@ -14,6 +14,10 @@ * May 2018: Florian Haftmann Consolidation of string-like types in HOL. +* May 2018: Andreas Lochbihler (Digital Asset), + Pascal Stoop (ETH Zurich) + Code generation with lazy evaluation semantics. + * March 2018: Florian Haftmann Abstract bit operations push_bit, take_bit, drop_bit, alongside with an algebraic foundation for bit strings and word types in diff -r f551dd2178ab -r 5859c688102a NEWS --- a/NEWS Wed May 16 23:13:33 2018 +0200 +++ b/NEWS Thu May 17 07:42:33 2018 +0200 @@ -262,6 +262,11 @@ parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for some examples. +* A new preprocessor for the code generator to generate code for algebraic + types with lazy evaluation semantics even in call-by-value target languages. + See theory HOL-Library.Code_Lazy for the implementation and + HOL-Codegenerator_Test.Code_Lazy_Test for examples. + * SMT module: - The 'smt_oracle' option is now necessary when using the 'smt' method with a solver other than Z3. INCOMPATIBILITY.