User:Rsimmons/primop.elf

From The Twelf Project
Jump to: navigation, search
% ============================================================
% == Bits and binary numbers                                ==
% ==                                                        ==
% == A binary number is a list of bits with the LEAST       ==
% == significant digit exposed. A cobinary number is a      ==
% == list of bits with the MOST significant bits exposed.   ==
% == This library assumes that binary numbers are used more ==
% == often than cobinary numbers, but cobinaries make it    ==
% == much easier to do certain operations.                  ==
% ============================================================

bit : type.

bit/0 : bit.
bit/1 : bit.

%abbrev b0 = bit/0.
%abbrev b1 = bit/1.

binary : nat -> type.

binary/nil : binary nat/z.
binary/cons : bit -> binary N -> binary (s N).

%abbrev $ = binary/cons. %infix right 4 $.
%abbrev $nil = binary/nil.
%abbrev 0 : binary N -> binary (s N) = [B] binary/cons bit/0 B.
%abbrev 1 : binary N -> binary (s N) = [B] binary/cons bit/1 B.

cobinary : nat -> type.

cobinary/nil : cobinary z.
cobinary/cons : bit -> cobinary N -> cobinary (s N).

%abbrev & = cobinary/cons. %infix right 4 &.
%abbrev &nil = cobinary/nil.








% = Section 1 : Bit-pushing =

% ============================================================
% == Conversion from binaries to cobinaries, and back       ==
% == 
% ==

binary->cobinary-help : nat-plus NA NB NC 
			 -> binary NA -> cobinary NB -> cobinary NC -> type.
%mode binary->cobinary-help +D +N1 +N2 -N3.
binary->cobinary-help/z : binary->cobinary-help nat-plus/z $nil N2 N2.
binary->cobinary-help/s : binary->cobinary-help (nat-plus/s D) (Bit $ A) B C
			   <- nat-plus/s-alt D D2
			   <- binary->cobinary-help D2 A (Bit & B) C.
%worlds () (binary->cobinary-help _ _ _ _).
%total T (binary->cobinary-help _ T _ _).

binary->cobinary : binary N -> cobinary N -> type.
%mode binary->cobinary +N1 -N2.
binary->cobinary/i : binary->cobinary N1 N2 
		      <- nat-plus/z-alt _ D
		      <- binary->cobinary-help D N1 &nil N2.
%worlds () (binary->cobinary _ _).
%total T (binary->cobinary T _).

cobinary->binary-help : nat-plus NA NB NC
			 -> cobinary NA -> binary NB -> binary NC -> type.
%mode cobinary->binary-help +D +N1 +N2 -N3.
cobinary->binary-help/z : cobinary->binary-help nat-plus/z &nil N2 N2.
cobinary->binary-help/s : cobinary->binary-help (nat-plus/s D) (Bit & A) B C
			   <- nat-plus/s-alt D D2
			   <- cobinary->binary-help D2 A (Bit $ B) C.
%worlds () (cobinary->binary-help _ _ _ _).
%total T (cobinary->binary-help _ T _ _).

cobinary->binary : cobinary N -> binary N -> type.
%mode cobinary->binary +N1 -N2.
cobinary->binary/i : cobinary->binary N1 N2 
		      <- nat-plus/z-alt _ D
		      <- cobinary->binary-help D N1 $nil N2.
%worlds () (cobinary->binary _ _).
%total T (cobinary->binary T _).


% ============================================================
% == The "get a zero of the right size" predicate           ==
% ============================================================

bin-zero : {N} binary N -> type.
%mode bin-zero +N -B.
bin-zero/z : bin-zero z $nil.
bin-zero/s : bin-zero (s N) (0 B) <- bin-zero N B.
%worlds () (bin-zero _ _).
%total T (bin-zero T _).

% ============================================================
% == The "are there more ones" test                         ==
% ==                                                        ==
% == Returns the 1 bit if there are more ones, 0 otherwise  ==
% ============================================================

bin-moreones : binary N -> bit -> type.
%mode bin-moreones +A -B.
bin-moreones/z : bin-moreones $nil bit/0.
bin-moreones/1 : bin-moreones (1 _) bit/1.
bin-moreones/0 : bin-moreones (0 B) R <- bin-moreones B R.
%worlds () (bin-moreones _ _).
%total T (bin-moreones T _).

% ============================================================
% == Truncate                                               ==
% ==                                                        ==
% == Takes a natural number N and a binary number B1, and   ==
% == returns a N-digit binary number that is B1 with either ==
% == higher-order 0's added or higer-order digits lopped    ==
% == off                                                    ==
% ============================================================

bin-truncate : {N} binary A -> binary N -> type.
%mode bin-truncate +N +B1 -B2.
bin-truncate/z : bin-truncate z _ $nil.
bin-truncate/s$nil : bin-truncate (s N) $nil (0 B) <- bin-truncate N $nil B.
bin-truncate/s0 : bin-truncate (s N) (0 B1) (0 B2) <- bin-truncate N B1 B2.
bin-truncate/s1 : bin-truncate (s N) (1 B1) (1 B2) <- bin-truncate N B1 B2.
%worlds () (bin-truncate _ _ _).
%total T (bin-truncate T _ _).

% ============================================================
% == Trim                                                   ==
% ==                                                        ==
% == Takes a binary number and returns another with all the ==
% == higher order 0's lopped off                            ==
% ============================================================

bin-trim-help : binary N -> bit -> binary M -> type.
%mode bin-trim-help +B1 +B -B2.
bin-trim : binary N -> binary M -> type.
%mode bin-trim +B1 -B2.

bin-trim/done : bin-trim-help B bit/0 $nil.
bin-trim/more : bin-trim-help B1 bit/1 B2
		 <- bin-trim B1 B2.

bin-trim/$nil : bin-trim $nil $nil.
bin-trim/0 : bin-trim (0 B1) B2 
	       <- bin-moreones B1 B 
	       <- bin-trim-help (0 B1) B B2.
bin-trim/1 : bin-trim (1 B1) (1 B2) 
	      <- bin-trim B1 B2.
%worlds () (bin-trim _ _) (bin-trim-help _ _ _).
% total (T1 T2) (bin-trim T1 _) (bin-trim-help T2 _ _).

% ============================================================
% == Equalize                                               ==
% == Takes two binary numbers and makes them equal in size  ==
% ============================================================

bin-eq-ize : binary N -> binary M -> binary P -> binary Q -> type.
%mode bin-eq-ize +B1 +B2 -B3 -B4.

bin-eq-ize/$$: bin-eq-ize $nil $nil $nil $nil.
bin-eq-ize/$0: bin-eq-ize $nil (0 B2) (0 B3) (0 B4)<- bin-eq-ize $nil B2 B3 B4.
bin-eq-ize/$1: bin-eq-ize $nil (1 B2) (0 B3) (1 B4)<- bin-eq-ize $nil B2 B3 B4.
bin-eq-ize/0$: bin-eq-ize (0 B1) $nil (0 B3) (0 B4)<- bin-eq-ize B1 $nil B3 B4.
bin-eq-ize/1$: bin-eq-ize (1 B1) $nil (1 B3) (0 B4)<- bin-eq-ize B1 $nil B3 B4.
bin-eq-ize/00: bin-eq-ize (0 B1) (0 B2) (0 B3) (0 B4)<- bin-eq-ize B1 B2 B3 B4.
bin-eq-ize/01: bin-eq-ize (0 B1) (1 B2) (0 B3) (1 B4)<- bin-eq-ize B1 B2 B3 B4.
bin-eq-ize/10: bin-eq-ize (1 B1) (0 B2) (1 B3) (0 B4)<- bin-eq-ize B1 B2 B3 B4.
bin-eq-ize/11: bin-eq-ize (1 B1) (1 B2) (1 B3) (1 B4)<- bin-eq-ize B1 B2 B3 B4.

%worlds () (bin-eq-ize _ _ _ _).
%total {T1 T2} (bin-eq-ize T1 T2 _ _).








% = Section 2 : Basic numerical operations  =

% ============================================================
% == Plain Vanilla binary addition (with carry)             ==
% == Always call with CARRY_IN = bit/0 in standard use      ==
% ==                                                        ==
% == Always call with CARRY_IN = bit/0 in standard use      ==
% == Call with CARRY_IN = bit/1 to increment N1             ==
% ============================================================

bin-plusc : binary N -> binary N -> bit -> binary N -> bit -> type.
%mode bin-plusc +N1 +N2 +CARRY_IN -N2 -CARRY_OUT.

bin-plusc/z : bin-plusc $nil $nil C $nil C.
bin-plusc/1 : bin-plusc (0 N1)(0 N2) b0 (0 N3) C  <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/2 : bin-plusc (0 N1)(0 N2) b1 (1 N3) C  <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/3 : bin-plusc (0 N1)(1 N2) b0 (1 N3) C  <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/4 : bin-plusc (0 N1)(1 N2) b1 (0 N3) C  <- bin-plusc N1 N2 b1 N3 C.
bin-plusc/5 : bin-plusc (1 N1)(0 N2) b0 (1 N3) C  <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/6 : bin-plusc (1 N1)(0 N2) b1 (0 N3) C  <- bin-plusc N1 N2 b1 N3 C.
bin-plusc/7 : bin-plusc (1 N1)(1 N2) b0 (0 N3) C  <- bin-plusc N1 N2 b1 N3 C.
bin-plusc/8 : bin-plusc (1 N1)(1 N2) b1 (1 N3) C  <- bin-plusc N1 N2 b1 N3 C.

%worlds () (bin-plusc _ _ _ _ _).
%total T (bin-plusc T _ _ _ _).

% ============================================================
% == Binary subtraction (with carry)                        ==
% ==                                                        ==
% == The "borrow-out" digit, the second output of binary    ==
% == subtraction, can be used as a less-than test.          ==
% ==                                                        ==
% == Always call with CARRY_IN = bit/0 in standard use      ==
% ==                                                        ==
% == If BORROW_OUT is 1, then N1 < N2 (N3 is undefined)     ==
% == If BORROW_OUT is 0, then N1 >= N2 and N3 = N1 - N2     ==
% ============================================================

bin-minus : binary N -> binary M -> bit -> binary N -> bit -> type.
%mode bin-minus +N1 +N2 +BORROW_IN -N2 -BORROW_OUT.

bin-minus/l1 : bin-minus $nil (B2 $ N2) b1 $nil b1.
bin-minus/l0 : bin-minus $nil (B2 $ N2) b0 $nil BOUT
		<- bin-moreones (B2 $ N2) BOUT.
bin-minus/g0 : bin-minus (B1 $ N1) $nil b0 (B1 $ N1) b0.
bin-minus/a5 : bin-minus (0 N1) $nil b1 (1 N3) C  <- bin-minus N1 $nil b1 N3 C.
bin-minus/a7 : bin-minus (1 N1) $nil b1 (0 N3) C  <- bin-minus N1 $nil b0 N3 C.

bin-minus/z : bin-minus $nil $nil C $nil C.
bin-minus/1 : bin-minus (0 N1)(0 N2) b0 (0 N3) C  <- bin-minus N1 N2 b0 N3 C.
bin-minus/2 : bin-minus (0 N1)(1 N2) b0 (1 N3) C  <- bin-minus N1 N2 b1 N3 C.
bin-minus/3 : bin-minus (1 N1)(0 N2) b0 (1 N3) C  <- bin-minus N1 N2 b0 N3 C.
bin-minus/4 : bin-minus (1 N1)(1 N2) b0 (0 N3) C  <- bin-minus N1 N2 b0 N3 C.
bin-minus/5 : bin-minus (0 N1)(0 N2) b1 (1 N3) C  <- bin-minus N1 N2 b1 N3 C.
bin-minus/6 : bin-minus (0 N1)(1 N2) b1 (0 N3) C  <- bin-minus N1 N2 b1 N3 C.
bin-minus/7 : bin-minus (1 N1)(0 N2) b1 (0 N3) C  <- bin-minus N1 N2 b0 N3 C.
bin-minus/8 : bin-minus (1 N1)(1 N2) b1 (1 N3) C  <- bin-minus N1 N2 b1 N3 C.

%worlds () (bin-minus _ _ _ _ _).
%total T (bin-minus T _ _ _ _).

% ===========================================================
% == Carryless binary addition (used for multiplcation)    ==
% ===========================================================

bin-plus : binary M -> binary M -> bit -> binary (s M) -> type.
%mode bin-plus +N1 +N2 +CARRY_IN -N2.

bin-plus/z0 : bin-plus $nil $nil b0 (0 $nil).
bin-plus/z1 : bin-plus $nil $nil b1 (1 $nil).
bin-plus/s0 : bin-plus (0 N1)(0 N2) b0 (0 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s1 : bin-plus (0 N1)(0 N2) b1 (1 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s2 : bin-plus (0 N1)(1 N2) b0 (1 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s3 : bin-plus (0 N1)(1 N2) b1 (0 N3) <- bin-plus N1 N2 b1 N3.
bin-plus/s4 : bin-plus (1 N1)(0 N2) b0 (1 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s5 : bin-plus (1 N1)(0 N2) b1 (0 N3) <- bin-plus N1 N2 b1 N3.
bin-plus/s6 : bin-plus (1 N1)(1 N2) b0 (0 N3) <- bin-plus N1 N2 b1 N3.
bin-plus/s7 : bin-plus (1 N1)(1 N2) b1 (1 N3) <- bin-plus N1 N2 b1 N3.

%worlds () (bin-plus _ _ _ _).
%total T (bin-plus _ T _ _).

% ===========================================================
% == Bitwise nand                                          ==
% ===========================================================

bin-nand : binary N -> binary N -> binary N -> type.
%mode bin-nand +A +B -C.
bin-nand/z : bin-nand $nil $nil $nil.
bin-nand/s0 : bin-nand (0 N1) (0 N2) (1 N3) <- bin-nand N1 N2 N3.
bin-nand/s1 : bin-nand (0 N1) (1 N2) (1 N3) <- bin-nand N1 N2 N3.
bin-nand/s2 : bin-nand (1 N1) (0 N2) (1 N3) <- bin-nand N1 N2 N3.
bin-nand/s3 : bin-nand (1 N1) (1 N2) (1 N3) <- bin-nand N1 N2 N3.








% = Section 3 : Advanced numerical operations  =

% ===========================================================
% == Full multiplcation                                    ==
% ==                                                       ==
% == Utilizes a helper function for multiplying the second ==
% == number by the high-order bit of a first number, and   == 
% == returning the first number without removing that bit  ==
% ===========================================================

bin-times-highbit : nat-plus NA NB NC
		     -> binary (s NA) -> binary NB 
                     -> binary NA -> binary NC -> type.
%mode bin-times-highbit +D +A +B -A' -C.
bin-times-highbit/0 
   : bin-times-highbit nat-plus/z (b0 $ $nil) B $nil Z <- bin-zero _ Z.
bin-times-highbit/1
   : bin-times-highbit nat-plus/z (b1 $ $nil) B $nil B.
bin-times-highbit/s
   : bin-times-highbit (nat-plus/s D) (Bit $ A) B (Bit $ A') (0 C)
      <- bin-times-highbit D A B A' C.
%worlds () (bin-times-highbit _ _ _ _ _).
%total T (bin-times-highbit T _ _ _ _).

bin-times : nat-plus N M P -> binary N -> binary M -> binary P -> type.
%mode bin-times +D +B1 +B2 -B3.

bin-times/z : bin-times nat-plus/z $nil A (Z: binary N) 
	       <- bin-zero N Z.
bin-times/s : bin-times (nat-plus/s (N:nat-plus NA NB NC)) A B C
	       <- bin-times-highbit N A B A2 B2
	       <- bin-times N A2 B C2
	       <- nat-plus-assoc N N'
	       <- bin-plus B2 C2 b0 C.
%worlds () (bin-times _ _ _ _).
%total T (bin-times T _ _ _).

% ===========================================================
% == Division with remainder                               ==
% ==                                                       ==
% == Division needs a helper lemma that chooses, given the ==
% == output of a call to minus(NUM,DIV,NOUT), to tack a    ==
% == 0 on to the result and proceed with NUM if            ==
% == subtraction failed, and to tack on a 1 and proceed    ==
% == with NOUT if subtraction failed.                      ==
% ==                                                       ==
% == The division altorithm is very confusing and will     ==
% == need exposition at a later time.                      ==
% ===========================================================

bin-longdiv-help : bit -> binary N -> binary N -> bit -> binary N -> type.
%mode bin-longdiv-help +BitOUT +NOUT +NUM -Bit -REMAINDER.

bin-longdiv-help/0 : bin-longdiv-help b0 NOUT _ b1 NOUT.
bin-longdiv-help/1 : bin-longdiv-help b1 _ NUM b0 NUM.

%worlds () (bin-longdiv-help _ _ _ _ _).
%total T (bin-longdiv-help T _ _ _ _).

bin-longdiv : nat-plus N1 (s N2) N3 
	       -> cobinary N1 -> binary (s N2) -> binary M 
               -> cobinary (s N1) -> binary N3 -> type.
%mode bin-longdiv +D +NUMERATOR1 +NUMERATOR2 +DIVISOR -QUOTIENT -REMAINDER.

bin-longdiv/z : bin-longdiv nat-plus/z &nil NUM DIV (Bit & &nil) REMAINDER
		<- bin-minus NUM DIV b0 NOUT BitOUT
		<- bin-longdiv-help BitOUT NOUT NUM Bit REMAINDER.
bin-longdiv/s : bin-longdiv (nat-plus/s D1) (Bit1 & N1) NUM DIV (Bit2 & QUOT) R
		 <- bin-minus NUM DIV b0 NOUT BitOUT
		 <- bin-longdiv-help BitOUT NOUT NUM Bit2 NUM2
		 <- nat-plus/s-alt D1 D2
		 <- bin-longdiv D2 N1 (Bit1 $ NUM2) DIV QUOT R.

%worlds () (bin-longdiv _ _ _ _ _ _).
%total T (bin-longdiv _ T _ _ _ _).


bin-divmod : binary N -> binary M -> binary N -> binary N -> type.
%mode bin-divmod +NUMERATOR +DIVISOR -QUOTIENT -REMAINDER.

bin-divmod/z : bin-divmod $nil _ $nil $nil.
bin-divmod/s : bin-divmod (NUM : binary (s N)) DIV QUOT REM
		<- binary->cobinary NUM (Bit & CONUM)
		<- nat-plus/z-alt _ D
		<- nat-plus/s-alt D D'
		<- bin-longdiv D' CONUM (Bit $ $nil) DIV COQUOT REM
		<- cobinary->binary COQUOT QUOT.

%worlds () (bin-divmod _ _ _ _).
%total T (bin-divmod T _ _ _).


% ***************************** TEST CASES *****************************

bin342 = [X] (0(1(1(0(1(0(1(0(1(0(0(0 X)))))))))))).
bin215 = (1(1(1(0(1(0(1(1(0(0(0 $nil))))))))))).
bin73530 = [X] (0(1(0(1(1(1(0(0(1(1(1(1(1(0(0(0(1 X))))))))))))))))).

deriv = nps(nps(nps(nps(nps(nps(nps(nps(nps(nps(nps(nps npz))))))))))).

%query 1 * Test : bin-times deriv (bin342 $nil) bin215 (bin73530 Zeroes).

%query 1 * Test : bin-divmod (bin73530 $nil) bin215 (bin342 Zeroes) R.