use "nbe-f.sml";

val testterm1 = oabstr (1,ovar 1);

val testtype11 = (tvar 1) --> (tvar 1);

val testtype12 = ((tvar 1) --> (tvar 1)) 
                 --> (tvar 1) --> (tvar 1);

val testtype13 = (((tvar 1) --> (tvar 1)) 
                                --> (tvar 1) --> (tvar 1))
                 --> ((tvar 1) --> (tvar 1)) 
                                   --> (tvar 1) --> (tvar 1);
                                   
val testtype14 = ((all (1,((tvar 1) --> (tvar 1)))) 
                 --> (all (1,(tvar 1) --> (tvar 1))));

val testtype15 = ((all (1,((tvar 1) --> (tvar 1)))) 
                       --> (all (1,(tvar 1) --> (tvar 1))))
                 --> ((all (1,((tvar 1) --> (tvar 1)))) 
                       --> (all (1,(tvar 1) --> (tvar 1))));
                        
val testterm2 = oabstr (1,oappl (oTappl (ovar 1,(tvar 2) --> (tvar 2)),
                                 oTappl (ovar 1,(tvar 2))));
                                 
val testtype2 = (all (1, tvar 1)) --> (tvar 2);

val testterm3 = oTabstr (1, oabstr (1,oappl (oTappl (ovar 1,(tvar 2) --> (tvar 2)),
                                             oTappl (ovar 1,(tvar 2)))));

val testtype3 = (all (2, (all (1, tvar 1)) --> (tvar 2)));

val type_cn = (all (1, ((tvar 1) --> (tvar 1)) --> ((tvar 1) --> (tvar 1))));
              (*"(Va1.((a1 -> a1) -> (a1 -> a1)))"*)

val add = (oabstr (1, (oabstr (2, (oTabstr (1, (oabstr (3, (oabstr (4, (oappl (oappl (oTappl ((ovar 1),(tvar 1)),(ovar 3)),(oappl (oappl (oTappl ((ovar 2),(tvar 1)),(ovar 3)),(ovar 4)))))))))))))));

val mult = (oabstr (1, (oabstr (2, (oTabstr (1, (oabstr (3, (oappl (oTappl ((ovar 1),(tvar 1)), oappl (oTappl ((ovar 2),(tvar 1)),(ovar 3))))))))))));

val exp = (oabstr (1, (oabstr (2, (oTabstr (1, (oappl (oTappl ((ovar 1),(tvar 1)),oTappl ((ovar 2),(tvar 1))))))))));

val zero = (oTabstr (1, (oabstr (1, (oabstr (2, (ovar 2)))))));

val one = (oTabstr (1, (oabstr (1, (oabstr (2, (oappl ((ovar 1), (ovar 2)))))))));

val twice = (oabstr (1, (oappl (oappl (add, (ovar 1)),(ovar 1)))));

val two = (oappl (oappl (add,one),one));

val twoo = (oappl (twice, one));

val three = (oappl (oappl (add,one),two));

val four = (oappl (oappl (mult,two),two));

val eight = (oappl (oappl (exp,three),two));

val nine = (oappl (oappl (exp,two),three));

val two_to_ninth = (oappl (oappl (exp,nine),two));