Index: translator/examples/abstype.c
===================================================================
--- translator/examples/abstype.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/abstype.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,25 @@
+// "cfa-cpp -nx Abstype.c"
+
+type T | { T x( T ); };
+
+T y( T t ) {
+    T t_instance;
+    return x( t );
+}
+
+forall(type T) lvalue T	*?( T* );
+int ?++( int *);
+int ?=?( int*, int );
+forall(dtype DT) DT* ?=?( DT **, DT* );
+
+type U = int*;
+
+U x( U u ) {
+    U u_instance = u;
+    (*u)++;
+    return u;
+}
+
+int *break_abstraction( U u ) {
+    return u;
+}
Index: translator/examples/ctxts.c
===================================================================
--- translator/examples/ctxts.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/ctxts.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,9 @@
+context has_f( type T ) {
+    T f( T );
+};
+
+context has_g( type U | has_f( U ) ) {
+    U g( U );
+};
+
+forall( type V | has_g( V ) ) void h( V );
Index: translator/examples/esskaykay.c
===================================================================
--- translator/examples/esskaykay.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/esskaykay.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,11 @@
+// "./cfa-cpp -cn esskaykay.c"
+
+// forall (type A, type B, type C) C ess (C (*f) (A,B), B (*g) (A), A x) { return f(x,g(x)); }
+forall (type A, type B, type C) C ess (C (*(*f)(A))(B), B (*g)(A), A x) { return f(x)(g(x)); }
+
+// forall (type A, type B) A kay (A a, B b) { return a; }
+forall (type A, type B) A (*kay(A a))(B b);
+
+// Now is the following function well-typed, or not?
+
+forall (type A) A esskaykay (A x) { ess (kay, kay, x); }
Index: translator/examples/factorial.c
===================================================================
--- translator/examples/factorial.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/factorial.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,18 @@
+//#include <stdio.h>
+
+int
+factorial( int n )
+{
+  if( n ) {
+    return factorial( n - 1 );
+  } else {
+    return 1;
+  }
+}
+
+int
+main()
+{
+  printf( "result is %d\n", factorial( 6 ) );
+  return 0;
+}
Index: translator/examples/forall.c
===================================================================
--- translator/examples/forall.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/forall.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,46 @@
+// "./cfa forall.c"
+
+typedef forall ( type T ) int (*f)( int );
+
+forall( type T )
+    void swap( T left, T right ) {
+	T temp = left;
+	left = right;
+	right = temp;
+    }
+
+context sumable( type T ) {
+    const T 0;
+    T ?+?(T, T);
+    T ?++(T*);
+    [T] ?+=?(T*,T);
+};
+
+forall( type T | sumable( T ) )
+    T sum( int n, T a[] ) {
+	T total = 0;
+	int i;
+	for ( i = 0; i < n; i += 1 )
+	    total = total + a[i];
+	return total;
+    }
+
+forall( type T | { T ?+?(T, T); T ?++(T*); [T] ?+=?(T*,T); } )
+    T twice( T t ) {
+	return t + t;
+    }
+
+forall( type T | { const T 0; int ?!=?(T, T); int ?<?(T, T); } )
+    T min( T t1, T t2 ) {
+	return t1 < t2 ? t1 : t2;
+    }
+
+int main() {
+    int x = 1, y = 2, a[10];
+    float f;
+
+    swap( x, y );
+    twice( x );
+    f = min( 4.0, 3.0 );
+    sum( 10, a );
+}
Index: translator/examples/forward.c
===================================================================
--- translator/examples/forward.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/forward.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,12 @@
+// "./cfa-cpp -nc forward.c"
+
+forall(type T) lvalue T *?( T* );
+int ?=?( int*, int );
+
+struct q { int y; };
+struct q *x;
+
+void f()
+{
+	*x;
+}
Index: translator/examples/huge.c
===================================================================
--- translator/examples/huge.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/huge.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,7 @@
+int huge (int n, forall (type T) T (*f) (T))
+{
+    if (n <= 0)
+	return f(0);
+    else
+	return huge (n-1, f(f));
+}
Index: translator/examples/identity.c
===================================================================
--- translator/examples/identity.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/identity.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,15 @@
+// './cfa identity.c'
+
+extern "C" {
+    int printf( const char *fmt, ... );
+}
+
+forall( type T )
+T identity( T t ) {
+    return t;
+}
+
+int main() {
+    printf( "result of identity of 5 is %d\n", identity( 5 ) );
+    return 0;
+}
Index: translator/examples/it_out.c
===================================================================
--- translator/examples/it_out.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/it_out.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,102 @@
+# 1 "iterator.c"
+# 1 "<built-in>"
+# 1 "<command line>"
+# 1 "iterator.c"
+# 1 "iterator.h" 1
+
+
+
+# 1 "iostream.h" 1
+
+
+
+typedef unsigned long streamsize_type;
+
+
+
+context ostream( dtype os_type )
+{
+
+    os_type *write( os_type *, const char *, streamsize_type );
+
+
+    int fail( os_type * );
+};
+
+
+
+
+context writeable( type T )
+{
+    forall( dtype os_type | ostream( os_type ) ) os_type * ?<<?( os_type *, T );
+};
+
+
+
+forall( dtype os_type | ostream( os_type ) ) os_type * ?<<?( os_type *, char );
+forall( dtype os_type | ostream( os_type ) ) os_type * ?<<?( os_type *, int );
+forall( dtype os_type | ostream( os_type ) ) os_type * ?<<?( os_type *, const char * );
+
+
+
+
+context istream( dtype is_type )
+{
+
+    is_type *read( is_type *, char *, streamsize_type );
+
+
+    is_type *unread( is_type *, char );
+
+
+    int fail( is_type * );
+
+
+    int eof( is_type * );
+};
+
+
+
+
+context readable( type T )
+{
+    forall( dtype is_type | istream( is_type ) ) is_type * ?<<?( is_type *, T );
+};
+
+
+
+forall( dtype is_type | istream( is_type ) ) is_type * ?>>?( is_type *, char* );
+forall( dtype is_type | istream( is_type ) ) is_type * ?>>?( is_type *, int* );
+# 5 "iterator.h" 2
+
+
+context iterator( type iterator_type, type elt_type )
+{
+
+    iterator_type ?++( iterator_type* );
+    iterator_type ++?( iterator_type* );
+
+
+    int ?==?( iterator_type, iterator_type );
+    int ?!=?( iterator_type, iterator_type );
+
+
+    lvalue elt_type *?( iterator_type );
+};
+
+
+
+forall( type elt_type | writeable( elt_type ),
+        type iterator_type | iterator( iterator_type, elt_type ),
+        dtype os_type | ostream( os_type ) )
+void write_all( iterator_type begin, iterator_type end, os_type *os );
+# 2 "iterator.c" 2
+
+forall( type elt_type | writeable( elt_type ),
+        type iterator_type | iterator( iterator_type, elt_type ),
+        dtype os_type | ostream( os_type ) )
+void
+write_all( elt_type begin, iterator_type end, os_type *os )
+{
+    os << begin;
+}
Index: translator/examples/min.c
===================================================================
--- translator/examples/min.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/min.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,18 @@
+// "./cfa min.c"
+// "./cfa -CFA min.c > min_out.c"
+// "gcc32 -g min_out.c LibCfa/libcfa.a"
+
+extern "C" {
+    int printf( const char *, ... );
+}
+
+forall( type T | { const T 0; int ?!=?(T, T); int ?<?(T, T); } )
+T min( T t1, T t2 ) {
+    return t1 < t2 ? t1 : t2;
+}
+
+int main() {
+    float f;
+    f = min( 4.0, 3.0 );
+    printf( "result is %f\n", f );
+}
Index: translator/examples/new.c
===================================================================
--- translator/examples/new.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/new.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,15 @@
+// "./cfa-cpp -c new.c"
+
+forall( type T )
+void f( T *t ) {
+  t--;
+  *t;
+  ++t;
+  t += 2;
+  t + 2;
+  --t;
+  t -= 2;
+  t - 4;
+  t[7];
+  7[t];
+}
Index: translator/examples/prolog.c
===================================================================
--- translator/examples/prolog.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/prolog.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,32 @@
+// "./cfa prolog.c"
+
+extern "C" { extern int printf( const char *fmt, ... ); }
+
+void printResult( int x ) { printf( "int\n" ); }
+void printResult( double x ) { printf( "double\n" ); }
+void printResult( char * x ) { printf( "char*\n" ); }
+
+void is_arithmetic( int x ) {}
+void is_arithmetic( double x ) {}
+
+void is_integer( int x ) {}
+
+context ArithmeticType( type T ) {
+    void is_arithmetic( T );
+};
+
+context IntegralType( type T | ArithmeticType( T ) ) {
+    void is_integer( T );
+};
+
+forall( type T | IntegralType( T ) | { void printResult( T ); } )
+void hornclause( T param ) {
+    printResult( param );
+}
+
+int main() {
+    int x;
+    double x;
+    char * x;
+    hornclause( x );
+}
Index: translator/examples/quad.c
===================================================================
--- translator/examples/quad.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/quad.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,22 @@
+// "./cfa quad.c"
+// "./cfa -CFA quad.c > quad_out.c"
+// "gcc31 -g quad_out.c LibCfa/libcfa.a"
+
+extern "C" {
+#include <stdio.h>
+}
+
+forall( type T | { T ?*?( T, T ); } )
+T square( T t ) {
+    return t * t;
+}
+
+forall( type U | { U square( U ); } )
+U quad( U u ) {
+    return square( square( u ) );
+}
+
+int main() {
+    int N = 2;
+    printf( "result of quad of %d is %d\n", N, quad( N ) );
+}
Index: translator/examples/rodolfo1.c
===================================================================
--- translator/examples/rodolfo1.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/rodolfo1.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,7 @@
+// "./cfa-cpp -c rodolfo1.c"
+
+void f() {
+	int a, b = 4, c = 5;
+	a = b + c;
+	int d = a + 7;
+}
Index: translator/examples/rodolfo2.c
===================================================================
--- translator/examples/rodolfo2.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/rodolfo2.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,14 @@
+// "./cfa-cpp -c rodolfo2.c"
+
+extern "C" {
+    #include <assert.h>
+}
+
+int a = 7;
+
+void f() {
+    int b;
+    b = a;
+    int a = 8;
+    assert( b == 7 );
+}
Index: translator/examples/s.c
===================================================================
--- translator/examples/s.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/s.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,7 @@
+int ?!=?( int, int );
+int 0;
+
+void f()
+{
+    0 ? 4 : 5;
+}
Index: translator/examples/simple.c
===================================================================
--- translator/examples/simple.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/simple.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,21 @@
+// './cfa square.c'
+
+extern "C" {
+    int printf( const char *fmt, ... );
+}
+
+context has_star( type T ) {
+    T ?*?( T, T );
+};
+
+int ?*?( int, int );
+int ?=?( int*, int );
+
+forall( type T | has_star( T ) )
+T square( T t ) {
+    return t * t;
+}
+
+int main() {
+    printf( "result of square of 5 is %d\n", square( 5 ) );
+}
Index: translator/examples/simplePoly.c
===================================================================
--- translator/examples/simplePoly.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/simplePoly.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,17 @@
+// './cfa-cpp -nc < simplePoly.c'
+
+forall( type T, type U | { T f( T, U ); } )
+T q( T t, U u )
+{
+    return f( t, u );
+//  return t;
+}
+
+int f( int, double* );
+
+void g( void ) {
+    int y;
+    double x;
+//  if( y )
+    q( 3, &x );
+}
Index: translator/examples/simpler.c
===================================================================
--- translator/examples/simpler.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/simpler.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,7 @@
+// "./cfa-cpp -c simpler.c"
+
+forall( type T ) T id( T, T );
+
+int main() {
+    id( 0, 7 );
+}
Index: translator/examples/specialize.c
===================================================================
--- translator/examples/specialize.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/specialize.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,43 @@
+// "./cfa specialize.c"
+// "./cfa -g simple.c"
+// "./cfa -CFA simple.c > simple_out.c"
+
+/// void f( const int * );
+/// 
+/// void m()
+/// {
+///   f( 0 );
+/// }
+
+/// forall( dtype T ) T* f( T* );
+/// void g( int* (*)(int*) );
+/// 
+/// int m() {
+///   g( f );
+/// }
+
+/// void f1( void (*q)( forall( dtype U ) U* (*p)( U* ) ) );
+/// void g1( int* (*)(int*) );
+/// 
+/// int m1() {
+///   f1( g1 );
+/// }
+
+extern "C" {
+  int printf( const char*, ... );
+}
+
+forall( type T ) T f( T t )
+{
+  printf( "in f; sizeof T is %d\n", sizeof( T ) );
+  return t;
+}
+
+void g( int (*p)(int) )
+{
+  printf( "g: f(7) returned %d\n", f(7) );
+}
+
+int main() {
+  g( f );
+}
Index: translator/examples/square.c
===================================================================
--- translator/examples/square.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/square.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,14 @@
+// './cfa square.c'
+
+extern "C" {
+#include <stdio.h>
+}
+
+forall( type T | { T ?*?( T, T ); })
+T square( T t ) {
+    return t * t;
+}
+
+int main() {
+    printf( "result of square of 5 is %d\n", square( 5 ) );
+}
Index: translator/examples/square.cf
===================================================================
--- translator/examples/square.cf	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/square.cf	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,20 @@
+// './cfa square.c'
+
+#undef __cplusplus
+extern "C" {
+#include <stdio.h>
+}
+
+forall( type T | { T ?*?( T, T ); })
+T
+square( T t )
+{
+  return t * t;
+}
+
+int
+main()
+{
+  printf( "result of square of 5 is %d\n", square( 5 ) );
+  return 0;
+}
Index: translator/examples/sum.c
===================================================================
--- translator/examples/sum.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
+++ translator/examples/sum.c	(revision a0d9f9418e3d60d93ffe3e14a8865ad439ab16d9)
@@ -0,0 +1,31 @@
+// "./cfa -g sum.c"
+// "./cfa -CFA sum.c > sum_out.c"
+// "gcc32 -g sum_out.c LibCfa/libcfa.a"
+
+extern "C" {
+    int printf( const char *, ... );
+}
+
+context sumable( type T ) {
+    const T 0;
+    T ?+?(T, T);
+    T ?++(T*);
+    [T] ?+=?(T*,T);
+};
+
+forall( type T | sumable( T ) )
+T sum( int n, T a[] ) {
+    T total = 0;
+    int i;
+    for ( i = 0; i < n; i += 1 )
+	total = total + a[i];
+    return total;
+}
+
+int main() {
+    int a[10];
+    for ( int i = 0; i < 10; ++i ) {
+	a[i] = i;
+    }
+    printf( "the sum is %d\n", sum( 10, a ) );
+}