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 3125 "./lpsrc/flx_tutorial.pak" 2: //Check axioms 3: //Check reductions 4: #import <flx.flxh> 5: 6: noinline fun f(x:int):int = { print "Cheat"; endl; return x; } 7: 8: reduce idem(x:int): f ( f x ) => f x; 9: 10: var x = f(f(f(f(1)))); 11: print x; endl; 12: 13: axiom symmetry (x:int,y:int): x + y == y + x; 14: axiom associativity (x:int, y:int, z:int): (x + y) + z == x + (y + z); 15: reduce additive_unit(x:int): x + int 0 => x; 16: reduce multiplicative_unit(x:int): x * int 0 => 0; 17: reduce additive_unit(x:int): int 0 + x => x; 18: reduce multiplicative_unit(x:int): int 0 * x=> int 0; 19: 20: //axiom wrong(x:int,y:int): x == y; 21: fun hh(x:int)=>x; 22: 23: reduce silly (x:int): hh x => x; 24: 25: axiom_check (1,2,3); 26: 27: var i:int=1; 28: lab:> 29: axiom_check (i,2); 30: i=i+1; 31: if i <= 5 goto lab; 32: 33: axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t): 34: sym(x,y) == sym(y,x) 35: ; 36: 37: axiom_check (add of (int * int), eq of (int * int), 1,2); 38: 39:
1: Cheat 2: 1