% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%                                                                           %
% File:            graycode.dtr                                             %
% Purpose:         FSTs map a Gray code to binary, and vice versa           %
% Author:          Gerald Gazdar, August 1994                               %
% Email:           geraldg@cogs.sussex.ac.uk                                %
% Address:         COGS, Sussex University, Brighton BN1 9QH, UK            %
% Version:         1.0                                                      %
%                                                                           %
%      Copyright (c) University of Sussex 1994.  All rights reserved.       %
%                                                                           %
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% Gray codes are a (family of) number representations that have the
% interesting (and possibly useful) property that N and N+1 will always
% differ by exactly one bit.
%
% See Thomas L. Floyd (1990) Digital Fundamentals, 4th Edition.  Columbus:
% Merrill, pages 78-80.

# vars $bin0 $bin1: 0 1 .

Add:
    <> == 0
    <1 0> == 1
    <0 1> == 1.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% Bin2Gray is a function that maps binary integers to a partcular Gray code
% representation:

Bin2Gray:
    <$bin0> == $bin0 B2G:<$bin0>.

B2G:
    <$bin0> ==
    <$bin0 $bin1> == Add B2G:<$bin1>.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% Gray2Bin is a function that maps integers represented in the above Gray
% code back into binary: 

Gray2Bin:
    <$bin0> == $bin0 G2B:<$bin0>.

G2B:
    <$bin0> ==
    <$bin0 $bin1> == Add G2B:<Add>.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% Some example theorems:
% 
% Bin2Gray:
%   <1 0 1 1 0> = 1 1 1 0 1
%   <1 1 0 1 1> = 1 0 1 1 0
%   <1 1 1 0 1> = 1 0 0 1 1
%   <1 0 0 1 0> = 1 1 0 1 1.
% 
% Gray2Bin:
%   <1 0 1 1 0> = 1 1 0 1 1
%   <1 1 0 1 1> = 1 0 0 1 0
%   <1 1 1 0 1> = 1 0 1 1 0
%   <1 0 0 1 0> = 1 1 1 0 0.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# hide Add B2G G2B.

# show
    <1 0 1 1 0>
    <1 1 0 1 1>
    <1 1 1 0 1>
    <1 0 0 1 0>.

% The next line is the Revision Control System Id: do not delete it.
% $Id: archive.dtr,v 1.1 1997/04/09 20:40:33 root Exp $