1(*****************************************************************************) 2(* High level (TFL) specification and implementation of factorial. *) 3(* Version for interactive use -- runs simulator and then waveform viewer. *) 4(*****************************************************************************) 5 6quietdec := true; 7val _ = set_trace "show_alias_printing_choices" 0; 8loadPath := "dff" :: !loadPath; 9app load ["compile","vsynth","dffTheory"]; 10open arithmeticTheory pairLib pairTheory PairRules combinTheory 11 devTheory composeTheory compileTheory compile vsynth dffTheory; 12infixr 3 THENR; 13infixr 3 ORELSER; 14quietdec := false; 15 16 17(*****************************************************************************) 18(* Start new theory "Fact" *) 19(*****************************************************************************) 20 21val _ = new_theory "Fact"; 22 23(*****************************************************************************) 24(* Define arithmetic operators used and their Verilog implementations. *) 25(*****************************************************************************) 26 27val _ = AddBinop ("ADD", (``UNCURRY $+ : num#num->num``, "+")); 28val _ = AddBinop ("SUB", (``UNCURRY $- : num#num->num``, "-")); 29val _ = AddBinop ("LESS", (``UNCURRY $< : num#num->bool``, "<")); 30val _ = AddBinop ("EQ", (``UNCURRY $= : num#num->bool``, "==")); 31 32(*****************************************************************************) 33(* To implement multiplication we use a naive iterative multiplier function *) 34(* (works by repeated addition) *) 35(*****************************************************************************) 36 37val (MultIter,MultIter_ind,MultIter_dev) = 38 hwDefine 39 `(MultIter (m:num,n:num,acc:num) = 40 if m = 0 then (0,n,acc) else MultIter(m-1,n,n + acc)) 41 measuring FST`; 42 43(*****************************************************************************) 44(* Create an implementation of a multiplier from MultIter *) 45(*****************************************************************************) 46 47val (Mult,_,Mult_dev) = 48 hwDefine 49 `Mult(m,n) = SND(SND(MultIter(m,n,0)))`; 50 51(*****************************************************************************) 52(* Implement iterative function as a step to implementing factorial *) 53(*****************************************************************************) 54 55val (FactIter_def,FactIter_ind,FactIter_dev) = 56 hwDefine 57 `(FactIter (n,acc) = 58 if n = 0 then (n,acc) else FactIter(n - 1, Mult(n,acc))) 59 measuring FST`; 60 61(*****************************************************************************) 62(* Implement a function Fact to compute SND(FactIter (n,1)) *) 63(*****************************************************************************) 64 65val (Fact,_,Fact_dev) = 66 hwDefine 67 `Fact n = SND(FactIter (n,1))`; 68 69(*****************************************************************************) 70(* Derivation using refinement combining combinators *) 71(*****************************************************************************) 72 73val FactImp_dev = REFINE_ALL Fact_dev; 74 75val Fact_cir = 76 save_thm 77 ("Fact_cir", 78 time MAKE_CIRCUIT FactImp_dev); 79 80(*****************************************************************************) 81(* This dumps changes to all variables. Set to false to dump just the *) 82(* changes to module FACT. *) 83(*****************************************************************************) 84 85dump_all_flag := false; 86 87(*****************************************************************************) 88(* Change these variables to select simulator and viewer. Commenting out the *) 89(* three assignments below will revert to the defaults: cver/dinotrace. *) 90(*****************************************************************************) 91(* 92iverilog_path := "/usr/bin/iverilog"; 93verilog_simulator := iverilog; 94waveform_viewer := gtkwave; 95 96(*****************************************************************************) 97(* Stop zillions of warning messages that HOL variables of type ``:num`` *) 98(* are being converted to Verilog wires or registers of type [31:0]. *) 99(*****************************************************************************) 100 101numWarning := false; 102 103SIMULATE Fact_cir [("inp","4")]; 104*) 105(*****************************************************************************) 106(* Verify that MultIter does compute multiplication *) 107(*****************************************************************************) 108 109val MultIterThm = (* proof adapted from similar one from KXS *) 110 save_thm 111 ("MultIterThm", 112 prove 113 (``!m n acc. MultIter (m,n,acc) = (0, n, (m * n) + acc)``, 114 recInduct MultIter_ind THEN RW_TAC std_ss [] 115 THEN RW_TAC arith_ss [Once MultIter] 116 THEN Cases_on `m` 117 THEN FULL_SIMP_TAC arith_ss [MULT])); 118 119(*****************************************************************************) 120(* Verify Mult is actually multiplication *) 121(*****************************************************************************) 122 123val MultThm = 124 store_thm 125 ("MultThm", 126 ``Mult = UNCURRY $*``, 127 RW_TAC arith_ss [FUN_EQ_THM,FORALL_PROD,Mult,MultIterThm]); 128 129(*****************************************************************************) 130(* Lemma showing how FactIter computes factorial *) 131(*****************************************************************************) 132 133val FactIterThm = (* proof from KXS *) 134 save_thm 135 ("FactIterThm", 136 prove 137 (``!n acc. FactIter (n,acc) = (0, acc * FACT n)``, 138 recInduct FactIter_ind THEN REPEAT STRIP_TAC 139 THEN RW_TAC arith_ss [Once FactIter_def] THENL 140 [RW_TAC arith_ss [FACT], 141 Cases_on `n` THENL 142 [FULL_SIMP_TAC arith_ss [FACT], 143 FULL_SIMP_TAC arith_ss [FACT,MultThm]]])); 144 145 146(*****************************************************************************) 147(* Verify Fact is indeed the factorial function *) 148(*****************************************************************************) 149 150val FactThm = 151 store_thm 152 ("FactThm", 153 ``Fact = FACT``, 154 RW_TAC arith_ss [FUN_EQ_THM,Fact,FactIterThm]); 155 156val _ = export_theory(); 157