1.2.27. test/regress/rt-1.01.27

     1: #line 1044 "./lpsrc/flx_regress.pak"
     2: //Check reductions
     3: #line 1044 "./lpsrc/flx_regress.pak"
     4: //Check axioms
Start felix section to test/regress/rt-1.01.27-0.flx[1 /1 ]
     5: type int = "int";
     6: type string = "std::string";
     7: 
     8: typedef bool = 2;
     9: 
    10: fun add: int * int -> int = "$1+$2";
    11: fun mul: int * int -> int = "$1*$2";
    12: fun le: int * int -> bool = "$1<=$2";
    13: fun eq: int * int -> bool = "$1==$2";
    14: 
    15: header '#include <iostream>';
    16: header '#include <string>';
    17: proc print[t]: t = "std::cout<<$1;";
    18: proc endl: 1 = "std::cout<<std::endl;";
    19: 
    20: noinline fun f(x:int):int = { print "Cheat"; endl; return x; }
    21: 
    22: reduce idem(x:int): f ( f x ) => f x;
    23: 
    24: var x = f(f(f(f(1))));
    25: print x; endl;
    26: 
    27: axiom symmetry (x:int,y:int): x + y == y + x;
    28: axiom associativity (x:int, y:int, z:int): (x + y) + z == x + (y + z);
    29: reduce additive_unit(x:int): x + 0 => x;
    30: reduce multiplicative_unit(x:int): x * 0 => 0;
    31: reduce additive_unit(x:int): 0 + x => x;
    32: reduce multiplicative_unit(x:int): 0 * x=> 0;
    33: 
    34: //axiom wrong(x:int,y:int): x == y;
    35: fun hh(x:int)=>x;
    36: 
    37: reduce silly (x:int): hh x => x;
    38: 
    39: axiom_check (1,2,3);
    40: 
    41: var i:int=1;
    42: lab:>
    43:   axiom_check (i,2);
    44:   i=i+1;
    45:   if i <= 5  goto lab;
    46: 
    47: axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t):
    48:   sym(x,y) == sym(y,x)
    49: ;
    50: 
    51: axiom_check (add of (int * int), eq of (int * int), 1,2);
    52: 
End felix section to test/regress/rt-1.01.27-0.flx[1]
Start data section to test/regress/rt-1.01.27-0.expect[1 /1 ]
     1: Cheat
     2: 1
End data section to test/regress/rt-1.01.27-0.expect[1]