%%% 
%%% Author : Frank Pfenning, Brigitte Pientka
%%% queries: sample programs for binary arithmentic and 
%%% refinement types. 

% Examples from paper + own examples
% to do: 
% seperate out unprovable queries / provable queries
% 

%querytabled * 5 
  check (lam [x] x 0) (bit => bit & pos => pos).

%querytabled * 15 
  check std (bit => nat).

%querytabled * *
  check std (zero => zero & nat => nat & pos => pos & nat => bit).

%querytabled * 4 
   check test1 pos.

%querytabled * * 
   check shiftl (zero => zero).

%querytabled * * 
   check shiftl (zero => nat).

%querytabled * 3
    check shiftl (nat => nat).

%querytabled * 7 
    check shiftl (bit => bit).

%querytabled * 7 
  check shiftl (pos => nat).

%querytabled * 7
  check shiftl (nat => nat).

%querytabled * 7 
  check shiftl ((nat => nat) & (pos => pos) & (pos => nat) & (bit => bit)).

%querytabled * * 
     check inc (pos => pos & nat => nat & nat => pos).

%querytabled * * 
      check inc (zero => pos & nat => nat & nat => pos).

%querytabled * 5  
   check inc (nat => pos).

%querytabled * * 
      check inc (zero => pos).

% working
%querytabled * 9
  check ge (nat => nat => bool).

%querytabled * 9
  check ge (bit => bit => bool).

%querytabled * 9
  check ge (pos => nat => bool & nat => nat => bool & nat => pos => bool & bit => bit => bool).

%querytabled * 4
  check (lam [plus] app (app plus (e 1)) (e 1))
           ((nat => nat => nat &
	       nat => pos => pos &
	       pos => nat => pos &
	       pos => pos => pos) => bit).

%querytabled * 15
  check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => pos => pos).

%querytabled * 4
  check (lam [plus] app (app plus (e 1)) (e 1))
(((nat => nat => nat)
    & (nat => pos => pos)
    & (pos => nat => pos)
    & (pos => pos => pos)) => nat).

%querytabled * 5
  check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat
	      & nat => pos => pos).

%querytabled * 15
  check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat       % *3 (3 ways to prove nat)
	      & nat => pos => pos   % *2 (2 ways to prove pos)
	      & pos => nat => pos). % *2 (2 ways to prove pos)

%querytabled * 15
  check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat		% *4 ways to prove nat
	      & nat => pos => pos	% *3 ways to prove pos
	      & pos => nat => pos	% *3 ways to prove pos
	      & pos => pos => pos).	% *3 ways to prove pos

%querytabled * 5
synth ((fix [inc] lam [n]
	case n
	(e 1)
	([x] x 1)
	([x] (app inc x) 0)) # nat => pos) A.


%querytabled * 9
  check (fix [plus] lam [n] lam [m]
	 (case n m ([x] x 1) ([y] y 1)))
(nat => nat => nat &
   nat => pos => pos &
   pos => nat => pos &
   pos => pos => pos).

%querytabled * 14
  check (fix [plus] lam [n] lam [m]
	 (case n
	    m 
	    ([x] case m (x 0) ([y] y 1) ([y] y 1))
	    ([x] x 1)))
(nat => nat => nat &
   nat => pos => pos &
   pos => nat => pos &
   pos => pos => pos).

%querytabled * 16
  check (fix [plus] lam [n] lam [m]
	 (case n
	    m 
	    ([x] case m
	       (x 0)
	       ([y] y 1)
	       ([y] y 1))
	    ([x] case m
	       (x 1)
	       ([y] y 1)
	       ([y] y 1))))
(nat => nat => nat &
   nat => pos => pos &
   pos => nat => pos &
   pos => pos => pos).

%querytabled * 50
  check plus' (nat => nat => nat &
	     nat => pos => pos &
	     pos => nat => pos &
	     pos => pos => pos).

%querytabled * 35
     check plus (nat => nat => nat &
	    nat => pos => pos &
	    pos => nat => pos &
	    pos => pos => pos).

%%%% so far "old tests"
%{
% sub' produces a bit number,i.e. it might have leading zeros!
% sub standardizes the result of sub', i.e. we get a nat (without leading zeros)
}%

%querytabled * *
    check sub' (zero => nat => zero).

%querytabled * *
    check sub' (nat => zero => nat).

%querytabled * *
    check sub' (nat => zero => nat & zero => nat => zero & bit => bit => bit).

%querytabled * *
  check sub (bit => bit => bit).

%querytabled * *
    check sub (zero => nat => zero).

%querytabled * *
    check sub (nat => zero => nat).

%querytabled * *
    check sub (nat => zero => nat & zero => nat => zero & bit => bit => bit).

%querytabled * *
    check sub (nat => zero => nat & 
	     zero => nat => zero & 
	     nat => nat => nat).

%querytabled * *
    check sub' (nat => zero => nat & zero => nat => zero & bit => bit => bit).

 
%querytabled * *
    check sub (pos => pos => nat).

%querytabled * *
  check sub ((nat => pos => nat) & (pos => nat => nat) & (pos => pos => nat) & nat => nat => nat).

%querytabled * *
   check mult (nat => zero => zero).

% all are provable 

%querytabled * *
  check mult (nat => nat => nat).

%querytabled * *
  check mult (pos => nat => nat).

%querytabled * *
  check mult ((pos => nat => nat) & (nat => nat => nat) & (nat => pos => nat)).

%querytabled * *
  check mult ((pos => nat => nat) & (nat => nat => nat) & (nat => pos => nat) & (pos => pos => pos)).

%querytabled * *
  check mult' (bit => bit => bit).
                      
%querytabled * 16
   check mult' (bit => bit => bit).

%querytabled * *
  check square' (bit => bit).

%querytabled * *
  check square (pos => nat & nat => nat).

%querytabled * *
  check square (pos => pos).