%%% Assignment 5
%%% Out: Wed 17 Oct
%%% Due: Wed 24 Oct 
%
% Use tutch to check your implementations in the following problems.
% A sample solution looks like this:
%
% S. Double a Natural Number
% 
%  Give a specification and implementation for the function double,
%  which doubles a natural number.

val double : nat -> nat

% Solution:
%
% specification:
%
%  double : nat -> nat
%  double 0 = 0
%  double sx = ss(double x)
%
% implementation:
%{
val double : nat -> nat =
 fn x => rec x
  of f0 => 0
  | f(sx') => ss(fx')
  end;
}%
% 1. Boolean functions
% 
%  Give specifications and term implementations
%  for the following usual boolean operations:
%
%  not, and, or, implies, iff, xor (exclusive or).
%

val not : bool -> bool

val and : bool -> bool -> bool

val or : bool -> bool -> bool

val implies : bool -> bool -> bool

val iff : bool -> bool -> bool

val xor : bool -> bool -> bool

% 2. Using the function half defined in class,
%   explicitely compute half3.
%
% 3. Recursion on nat
%
%  Give specification and term implementations
%  for the following functions on natural numbers.
%  Follow the example of double given in class.
%
%  (factorial) fact : nat -> nat  should compute n!,
%  i.e. the product of the first n+1 numbers except 0
%  (set 0! = 1).

val fact : nat -> nat

%  (equality) eq : nat -> nat -> bool such that
%  eq n m returns true if and only if n = m.

val eq : nat -> nat -> bool

%  (exponentiation) exp : nat -> nat -> nat such that
%  exp n m is m raised to the n-th power.

val exp : nat -> nat -> nat

%  (even) even: nat -> bool such that
%  even n is true just in case n is even.

val even: nat -> bool 

%
% 4. Lists
%
%  Specify and implement the following operations on lists.
%
% drop l i 
% returns what is left after dropping the first i elements of the list l. 

val drop : tau list -> nat -> tau list

% take i l 
%    returns the first i elements of the list l. 
%    return nil in any other case

val take : nat -> tau list -> tau list

%{
% 5. Expressions
%
%  Define an inductive data type express of arithmetical expressions
%  over natural numbers, the terms of which are expressions like
%   2*(3+1) + (4+22)*(3+9), etc.
%
%  Give formation, introduction, and elimination rules
%  involving two constructors Pxy and Txy (for plus and times).
%
%  Give specification and implementations for each of the following functions.
%
%  count e is the number of numerals in the expression e

 count : express -> nat

%  val e is the value of the expression upon evaluation of
%  Pxy as x+y and Txy as x*y

 val : express -> nat
}%

% Have fun!