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