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:
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: