reduce idem(x:int): f ( f x ) => f x;Specifies f is idempotent, and f(f(x)) should be reduced to just f(x). Reductions are performed after inlining, and applied repeatly to all expressions until code is fully reduced. The name of a reduction is not significiant, it is for documentation only. Of course, reductions can be polymorphic.
Axioms are statements of laws, for example
axiom symmetry (x:int,y:int): x + y == y + x;states that integer addition is symmetric. Axioms can be checked by providing test cases via calls to the pseudo function 'axiom_check'.
var i:int; forall i in 1 upto 5 do axiom_check (i,2); done;Axiom checks can be disable by the flxg compiler switch
--no-axiom-checksotherwise every axiom is matched against every test case, and each on the matches generates an assertion. An error is printed and the program aborted if any check fails.
1: #line 2546 "./lpsrc/flx_tutorial.pak" 2: #import <flx.flxh> 3: 4: noinline fun f(x:int):int = { print "Cheat"; endl; return x; } 5: 6: reduce idem(x:int): f ( f x ) => f x; 7: 8: var x = f(f(f(f(1)))); 9: print x; endl; 10: 11: axiom symmetry (x:int,y:int): x + y == y + x; 12: axiom associativity (x:int, y:int, z:int): (x + y) + z == x + (y + z); 13: reduce additive_unit(x:int): x + 0 => x; 14: reduce multiplicative_unit(x:int): x * 0 => 0; 15: reduce additive_unit(x:int): 0 + x => x; 16: reduce multiplicative_unit(x:int): 0 * x=> 0; 17: 18: //axiom wrong(x:int,y:int): x == y; 19: fun hh(x:int)=>x; 20: 21: reduce silly (x:int): hh x => x; 22: 23: axiom_check (1,2,3); 24: 25: var i:int; forall i in 1 upto 5 do axiom_check (i,2); done; 26: 27: axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t): 28: sym(x,y) == sym(y,x) 29: ; 30: 31: // this axiom is only right if 'add' is symmetric 32: axiom_check (add of (int * int), eq of (int * int), 1,2); 33: