Changeset 1577


Ignore:
Timestamp:
Oct 1, 2020 9:17:01 AM (4 years ago)
Author:
magne
Message:

Makefile

  • Updated script to current context (executable and operation names).

Basic.FiniteInteger

  • Upgraded some axiom names.

BasicCxx.FloatCxx

  • Added exp10 to the implementations.

BasicCxxExamples.ArrayCxxDemo

  • Improved some function names.

BasicCxxRaw/CxxBoundedArrayRaw.hxx

  • Corrected an error in the defintions of operator=.

BasicGeneral.ArrayNumberCxx

  • Changed GenericCRCArrays to FreeModuleCRCArrays.
  • Added functions exp10.

Fundamentals.Exponents

  • Improved naming of some axioms.

Fundamentals.Monoid

  • Corrected a mistake in the proof for theorem uniqueNeutral.

Mathematics.IndexableNumber

  • Changed concept GenericCRCArrays to FreeModuleCRCArrays.
  • Added code for exp10.

Mathematics.Numbers

  • Added support for exp10.

TutorialExamples.Tutorial3Cxx

  • Added program stringingTogetherCxx.
Location:
trunk/magnolia-basic-library/src
Files:
12 edited

Legend:

Unmodified
Added
Removed

  • trunk/magnolia-basic-library/src/Basic/FiniteInteger.mg

    r1454 r1577  
    8282concept BoundedNatural = {
    8383  use BoundedInteger;
    84   axiom zero_bound () {
     84  axiom zero_bound_BoundedNaturalAxiom () {
    8585    assert minimum() == zero();
    8686  }
    … …  
    9191concept ModulusInteger = {
    9292  use TorusInteger;
    93   axiom zero_bound () {
     93  axiom zero_bound_ModulusIntegerAxiom () {
    9494    assert minimum() == zero();
    9595  }

  • trunk/magnolia-basic-library/src/BasicCxx/FloatCxx.mg

    r1454 r1577  
    8585    function trunc( x:Float ) : Float;
    8686    function zero() : Float;
     87    function one () : Float;
    8788    function floor( x:Float ) : Float;
    8889    function abs( x:Float ) : Float;
    8990    function uminus( x:Float ) : Float;
     91    function pow ( x:Float, y:Float ) : Float;
     92    function _+_ ( x:Float, y:Float ) : Float;
     93    function _*_ ( x:Float, y:Float ) : Float;
    9094    predicate _<=_ ( x:Float, y:Float );
    9195    function raw_plus( x:Float, y:Float ) : Float;
    … …  
    121125    end;
    122126 
     127  /** Powers of ten. */
     128  function exp10 ( b:Float ) : Float =
     129    pow ( (one()+one()+one())*(one()+one()+one())+one(), b );
     130
    123131 
    124132  /** Checks that a float is an integer. */

  • trunk/magnolia-basic-library/src/BasicCxxExamples/ArrayCxxDemo.mg

    r1454 r1577  
    2828
    2929/** Properties of {@link dynamicArrayFloatCxx}.
    30  * - The program dynamicArrayFloat satisfyes DynamicArray on floats.
     30 * - The program dynamicArrayFloat satisfies DynamicArray on floats.
    3131 * - Concatenation of arrays forms a monoid.
    32  * - Reversion is self dual.
     32 * - Reversion is an involution.
    3333 */
    3434satisfaction dynamicArrayFloatCxx_properties =
    … …  
    9696  function prod ( a:Float, b:Float ) : Float = a*b;
    9797  function sum ( a:Float, b:Float ) : Float = a+b;
    98   use dynamicArrayPrefixCxx[E=>Float][star => max, scan => maximum, bar_scan => bar_scanMax ];
    99   use dynamicArrayPrefixCxx[E=>Float][star => min, scan => minimum, bar_scan => bar_scanMin ];
    100   use dynamicArrayPrefixCxx[E=>Float][star => prod, scan => product, bar_scan => bar_scanProd ];
    101   use dynamicArrayPrefixCxx[E=>Float][star => sum, scan => summation, bar_scan => bar_scanSum ];
     98  use dynamicArrayPrefixCxx[E=>Float][star => max, scan => scan_max, bar_scan => bar_scanMax ];
     99  use dynamicArrayPrefixCxx[E=>Float][star => min, scan => scan_min, bar_scan => bar_scanMin ];
     100  use dynamicArrayPrefixCxx[E=>Float][star => prod, scan => scan_prod, bar_scan => bar_scanProd ];
     101  use dynamicArrayPrefixCxx[E=>Float][star => sum, scan => scan_sum, bar_scan => bar_scanSum ];
    102102} models {
    103   use ArrayParallelPrefix[E=>Float][star => max, scan => maximum ];
    104   use ArrayParallelPrefix[E=>Float][star => min, scan => minimum ];
    105   use ArrayParallelPrefix[E=>Float][star => prod, scan => product ];
    106   use ArrayParallelPrefix[E=>Float][star => sum, scan => summation ];
     103  use ArrayParallelPrefix[E=>Float][star => max, scan => scan_max ];
     104  use ArrayParallelPrefix[E=>Float][star => min, scan => scan_min ];
     105  use ArrayParallelPrefix[E=>Float][star => prod, scan => scan_prod ];
     106  use ArrayParallelPrefix[E=>Float][star => sum, scan => scan_sum ];
    107107};
    108108

  • trunk/magnolia-basic-library/src/BasicCxxRaw/CxxBoundedArrayRaw.hxx

    r1454 r1577  
    5454                        }
    5555
    56                         bar_A& operator=(const bar_A& a) {
     56                        void operator=(const bar_A& a) {
    5757                                Intex size = a.data_size;
    58                                 if(data_size < a.data_size) {
    59                                         // Magnolia::Assert::guardFailed("Source data size larger than target data size","","BasicCxxRaw.CxxBoundedArrayRaw.CxxBoundedArrayRaw_impl.operator=");
     58                                if(data_size != a.data_size) {
     59                                        // Magnolia::Assert::guardFailed("Source data size different from target data size","","BasicCxxRaw.CxxBoundedArrayRaw.CxxBoundedArrayRaw_impl.operator=");
    6060                                        // std::cerr << "operator= Resizing bar_A data from " << data_size << " to " << size << std::endl;
    6161                                        delete [] data;
    … …  
    6767                                }
    6868                        }
    69                         bar_A& operator=(bar_A&& a) {
     69                        void operator=(bar_A&& a) {
    7070                                delete [] data;
    7171                                data_size = a.data_size;

  • trunk/magnolia-basic-library/src/BasicGeneral/ArrayNumberCxx.mg

    r1454 r1577  
    188188  [ A => A, zeroA => zeroA, oneA => oneA, eA => eA, piA => piA ]
    189189  [ createA => createA, bar_A => bar_A, bar_createA => bar_createA ];
    190 satisfaction aGenericCRCDynamicArrayCxx_models_GenericCRCArrays =
     190satisfaction aGenericCRCDynamicArrayCxx_models_FreeModuleCRCArrays =
    191191  RCRC[ operators_to_names ]
    192192with aGenericCRCDynamicArrayCxx
    193 models GenericCRCArrays;
     193models FreeModuleCRCArrays;
    194194
    195195
    … …  
    325325
    326326
    327 /** Lifting the continuous real/complex operations (division, roots, trigonometry, exponentials, hyperboles) to arrays. */
     327/** Lifting the continuous real/complex operations (division, roots, trigonometry, exponentials, hyperbolics) to arrays. */
    328328implementation aCRCDynamicArrayCxx = {
    329329  /** Lifting of extended field operations to an array. */
    … …  
    359359    [ func => exp2, aibmc => aibmc_exp2 ];
    360360  extend unaryMapArrayDynamicArrayCxx[ createarray_to_createa_etc ]
     361    [ func => exp10, aibmc => aibmc_exp10 ];
     362  extend unaryMapArrayDynamicArrayCxx[ createarray_to_createa_etc ]
    361363    [ func => log, aibmc => aibmc_log ];
    362364  extend unaryMapArrayDynamicArrayCxx[ createarray_to_createa_etc ]
    … …  
    367369    [ func => pow, aibmc => aibmc_pow ];
    368370  function eA() : A = createA(eR());
    369   /*** Lifting of the trigonometric hyperbole operations. */
     371  /*** Lifting of the trigonometric hyperbolic operations. */
    370372  extend unaryMapArrayDynamicArrayCxx[ createarray_to_createa_etc ]
    371373    [ func => acosh, aibmc => aibmc_acosh ];

  • trunk/magnolia-basic-library/src/Fundamentals/Exponents.mg

    r1454 r1577  
    2020 */
    2121concept Logarithm = {
    22   use Isomorphism [ I=>T, J=>T, jFromI=>exp, iFromJ=>log ];
     22  use Isomorphism [ I=>T, J=>T, jFromI=>exp, iFromJ=>log ]
     23    [ section => logSectionAxiom, retraction => logRetractionAxiom ];
    2324  use Semiring;
    2425 
    25   axiom logHomomorphismMult ( a:T, b:T ) {
     26  axiom logHomomorphismMultAxiom ( a:T, b:T ) {
    2627    assert log(mult(a,b)) == plus(log(a),log(b));
    2728  };
    2829 
    29   axiom logHomomorphismOne () {
     30  axiom logHomomorphismOneAxiom () {
    3031    assert log(one()) == zero();
    3132  };
    3233 
    33 };
     34} [ logHomomorphismMultAxiom => logHomomorphismMultAxiom, logHomomorphismOneAxiom => logHomomorphismOneAxiom ]
     35  [ logSectionAxiom => logSectionAxiom, logRetractionAxiom => logRetractionAxiom ];
    3436
    3537/**
    … …  
    3840 */
    3941concept Exponent = {
    40   use Isomorphism [ I=>T, J=>T, jFromI=>exp, iFromJ=>log ];
     42  use Isomorphism [ I=>T, J=>T, jFromI=>exp, iFromJ=>log ]
     43    [ section => expSectionAxiom, retraction => expRetractionAxiom ];
    4144  use Semiring;
    4245 
    43   axiom expHomomorphismPlus ( a:T, b:T ) {
     46  axiom expHomomorphismPlusAxiom ( a:T, b:T ) {
    4447    assert exp(plus(a,b)) == mult(exp(a),exp(b));
    4548  };
    4649 
    47   axiom expHomomorphismZero () {
     50  axiom expHomomorphismZeroAxiom () {
    4851    assert exp(zero()) == one();
    4952  };
    5053 
    51 };
     54} [ expHomomorphismPlusAxiom => expHomomorphismPlusAxiom, expHomomorphismZeroAxiom => expHomomorphismZeroAxiom ]
     55  [ expSectionAxiom => expSectionAxiom, expRetractionAxiom => expRetractionAxiom ];
    5256
    5357/**

  • trunk/magnolia-basic-library/src/Fundamentals/Monoid.mg

    r1477 r1577  
    6060} models {
    6161  theorem uniqueNeutral() {
    62     assert binop(n(),m()) == m() by leftNeutral(n());
    63     assert binop(n(),m()) == n() by rightNeutral(m());
     62    assert binop(n(),m()) == m() by leftNeutral(m());
     63    assert binop(n(),m()) == n() by rightNeutral(n());
    6464    assert n() == m()          qed by simplify binop(n(),m());
    6565  }

  • trunk/magnolia-basic-library/src/Makefile

    r1576 r1577  
    1111
    1212compile:        $(cxxobj) $(cppobj)
    13         BasicCxxRaw/StringCxxRaw/stringHashCxxRaw_soundness stringHashCxxRaw_hashCode_repeatable_validation
    1413        test `BasicCxxRaw/FloatCxxRaw/ieee754float80rawCxx_approximates_RawRealInterface d_pow 2 1234` = inf && echo 80bit float NOT supported || echo 80bit float OK
    1514
    … …  
    2322run:
    2423        BasicCxxExamples/StringCxxDemo/helloWorlds hello -i1 BasicCxxExamples/LanguageMessages.txt '"en"'
    25         BasicCxxRaw/StringCxxRaw/stringHashCxxRaw_soundness stringHashCxxRaw_hashCode_repeatable_validation
     24        BasicCxxRaw/StringCxxRaw/stringHashCxxRaw_soundness stringHashCxxRaw_hashCode_repeatable_validation || echo You are not using g++
    2625        test `BasicCxxRaw/FloatCxxRaw/ieee754float80rawCxx_approximates_RawRealInterface d_pow 2 1234` = inf && echo 80bit float not supported || true
    2726        test `BasicCxxRaw/IntegerCxxRaw/int8rawCxx_models_2complement plus 45 30` -eq 75
    2827        test `BasicCxxRaw/FloatCxxRaw/ieee754float64rawCxx_approximates_RawRealInterface d_integer_maximum` = 9007199254740992
    2928        test `BasicCxxRaw/FloatCxxRaw/ieee754float32rawCxx_approximates_RawRealInterface d_abs -- -93` -eq 93
    30         test `BasicCxxRaw/RepetitionCountCxxRawTest/repetitionTest repeatq 7 7` -eq 112
    31         test `BasicCxxRaw/RepetitionCountCxxRawTest/repetitionTest repeatr 7 7` -eq -128
    32         test `BasicCxxRaw/RepetitionCountCxxRawTest/powerProductSum sum 7` -eq 28
    33         test `BasicCxxRaw/RepetitionCountCxxRawTest/powerProductSum product 5` -eq 120
    34         test `BasicCxxRaw/RepetitionCountCxxRawTest/powerProductSum raise 3 5` -eq 243
     29        test `BasicCxxRaw/RepetitionCountCxxRawTest/test_repetitionCxx repeatq 7 7` -eq 112
     30        test `BasicCxxRaw/RepetitionCountCxxRawTest/test_repetitionCxx repeatr 7 7` -eq -128
     31        test `BasicCxxRaw/RepetitionCountCxxRawTest/test_powerProductSumCxx sum 7` -eq 28
     32        test `BasicCxxRaw/RepetitionCountCxxRawTest/test_powerProductSumCxx product 5` -eq 120
     33        test `BasicCxxRaw/RepetitionCountCxxRawTest/test_powerProductSumCxx raise 3 5` -eq 243
    3534        BasicCxx/IntegerCxx/boundedInteger8bitCxx_is_BoundedInteger -- modLatticeAxiom 3 -4
    3635        BasicCxx/IntegerCxx/boundedInteger8bitCxx_is_BoundedInteger -- pmodLatticeAxiom 3 -4
    … …  
    7978        BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal pmodLatticeAxiom -- 1.456789 -9.876543
    8079        BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal remLatticeAxiom -- 1.456789 -9.876543
    81         BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal expHomomorphismZero
    82         BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal expHomomorphismPlus 19 3
     80        BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal expHomomorphismZeroAxiom
     81        BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal expHomomorphismPlusAxiom 19 3
    8382        #test `BasicGeneral/ArrayRingCxxDemo/arrayRingConstructionsDynamicArrayCxx_models_ArrayRingProperties_on_float64bitCxx idiv -- -45 -7` -eq `BasicGeneral/ArrayRingCxxDemo/arrayRingConstructionsDynamicArrayCxx_models_ArrayRingProperties_on_float64bitCxx idiv1 45 7`
    8483        #test `BasicGeneral/ArrayRingCxxDemo/freeModuleDynamicArrayCxx_models_FreeModule_on_float80bitCxx product '<FM#Intex.bar_FM>2<Array#>3 65 98 94</Array#></FM#Intex.bar_FM>'` -eq 6370

  • trunk/magnolia-basic-library/src/Mathematics/Group.mg

    r1454 r1577  
    33 *
    44 * A group has one type {@code T}, a binary operation {@code plus}, a unary function {@code uminus} and a constant {@code zero}.
    5  * These naming conventions gollow from mathematics.
     5 * These naming conventions follow from mathematics.
    66 * Some of the support concepts have slightly different notation.
    77 *

  • trunk/magnolia-basic-library/src/Mathematics/IndexableNumber.mg

    r1454 r1577  
    113113concept TorusToTorusIntegerArrays = TorusToTorusIntegerA[ I => Intex ];
    114114
    115 /** Dynamic generic CRC arrays: types A (suffix A) R (suffix R). */
    116 concept GenericCRCArrays = {
     115/** Free module on CRC arrays: types A (suffix A), Intex, R (suffix R). */
     116concept FreeModuleCRCArrays = {
    117117  use ACRC[ I => Intex ];
    118118  use FreeModule;
    … …  
    526526    use UnaryMapAR[ func => exp ];
    527527    use UnaryMapAR[ func => exp2 ];
     528    use UnaryMapAR[ func => exp10 ];
    528529    use UnaryMapAR[ func => log ];
    529530    use UnaryMapAR[ func => log2 ];

  • trunk/magnolia-basic-library/src/Mathematics/Numbers.mg

    r1576 r1577  
    546546  function exp(x : Number) : Number;           
    547547  /** Base 2 exponentiation. */
    548   function exp2(x : Number) : Number;           
     548  function exp2(x : Number) : Number;
     549  /** Base 10 exponentiation. */
     550  function exp10(x : Number) : Number;           
    549551  /** natural, base e, logarithm. */
    550552  function log(x : Number) : Number;
    … …  
    562564    use Exponent[ T => Number, exp => exp2, log => log2 ][ names_to_operators ];
    563565    use Logarithm[ T => Number, exp => exp2, log => log2 ][ names_to_operators ];
     566  /*** Properties of the base 10 exponentiation and logarithms. */
     567    use Exponent[ T => Number, exp => exp10, log => log10 ][ names_to_operators ];
     568    use Logarithm[ T => Number, exp => exp10, log => log10 ][ names_to_operators ];
    564569   
    565570  axiom naturalLogarithmAxiom () {
    … …  
    584589    var two:Number = one() + one();
    585590    var ten:Number = two + two * two * two;
    586     assert pow(ten,zero()) == one();
    587     assert pow(ten,one()) == ten;
     591    assert exp10(zero()) == one();
     592    assert exp10(one()) == ten;
    588593    assert log10(ten) == one();
    589594    assert log10(one()) == zero();
    … …  
    604609    assert exp(x) == exp2( x * log2(e()) );
    605610    assert log10(x) == log2(x) * log10(two);
    606     assert pow(ten,x) == exp2( x * log2(ten) );
     611    assert exp10(x) == exp2( x * log2(ten) );
    607612  };
    608613};

  • trunk/magnolia-basic-library/src/TutorialExamples/Tutorial3Cxx.mg

    r1576 r1577  
    6262};
    6363
    64 program strenging = {
    65   use stringCxx;
    66   use recurring
    67     [ T => String, binop => concatenate ]
    68     [ once => square, twice => cube, thrice => tesseract ];
    69 };
    7064
    7165/** Creating a simple implementation by combining implementations.
    … …  
    118112    [ once => max1, twice => max2, thrice => max3 ];
    119113
    120   function min5 ( a:Float, b:Float, c:Float, d:Float, e:Float ) : Float
    121   = min(min(min(a,b),min(b,c)),e);
    122 
    123114  /** Uses recurring directly on the power function.
    124115   * Notice how fast the function grows.
    … …  
    132123};
    133124
     125
     126/** And now for something completely different:
     127 * Using the implementation recurring with strings.
     128 * The renamings first match the requirements of recurring to the context,
     129 * then renames the defined functions according to their role in the combined context.
     130 * Example use (to make you happy):
     131     TutorialExamples/Tutorial3Cxx/stringingTogetherCxx quadruple '"😋"'
     132 * This shows that what we might have thought of as integer or numeric functions can be used with any type as long as we can match the operations.
     133 */
     134program stringingTogetherCxx = {
     135  use stringCxx;
     136  use recurring
     137    [ T => String, binop => concatenate ]
     138    [ once => double, twice => triple, thrice => quadruple ];
     139};
Note: See TracChangeset for help on using the changeset viewer.