1(*****************************************************************************) 2(* High level (TFL) specification and implementation of factorial *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* START BOILERPLATE *) 7(*****************************************************************************) 8 9(****************************************************************************** 10* Load theories 11******************************************************************************) 12(* For working interactively 13quietdec := true; 14loadPath :="dff" :: !loadPath; 15app load ["compile","vsynth"]; 16open arithmeticTheory pairLib pairTheory PairRules combinTheory 17 devTheory composeTheory compileTheory compile vsynth; 18infixr 3 THENR; 19infixr 3 ORELSER; 20val _ = numLib.prefer_num(); 21quietdec := false; 22*) 23 24(****************************************************************************** 25 * Boilerplate needed for compilation. Batch mode. 26 ******************************************************************************) 27 28open HolKernel Parse boolLib bossLib; 29 30(****************************************************************************** 31 * Open theories. Batch mode. 32 ******************************************************************************) 33open arithmeticTheory pairLib pairTheory PairRules combinTheory 34 composeTheory compile vsynth; 35infixr 3 THENR; 36infixr 3 ORELSER; 37 38(****************************************************************************** 39 * Set default parsing to natural numbers rather than integers 40 ******************************************************************************) 41 42val _ = numLib.prefer_num(); 43 44(*****************************************************************************) 45(* END BOILERPLATE *) 46(*****************************************************************************) 47 48(*****************************************************************************) 49(* Start new theory "Fact" *) 50(*****************************************************************************) 51 52val _ = new_theory "Fact"; 53 54(*****************************************************************************) 55(* Define arithmetic operators used and associate them with their Verilog *) 56(* implementations. *) 57(*****************************************************************************) 58 59val _ = AddBinop ("ADD", (``UNCURRY $+ : num#num->num``, "+")); 60val _ = AddBinop ("SUB", (``UNCURRY $- : num#num->num``, "-")); 61val _ = AddBinop ("LESS", (``UNCURRY $< : num#num->bool``, "<")); 62val _ = AddBinop ("EQ", (``UNCURRY $= : num#num->bool``, "==")); 63 64(*****************************************************************************) 65(* Implement iterative function as a step to implementing factorial *) 66(*****************************************************************************) 67 68val (FactIter,FactIter_ind,FactIter_dev) = 69 hwDefine 70 `FactIter (n,acc:num) = 71 if n = 0 then (n,acc) else FactIter (n - 1, n * acc)`; 72 73(*****************************************************************************) 74(* Lemma showing how FactIter computes factorial *) 75(*****************************************************************************) 76 77val FactIterRecThm = (* proof from KXS *) 78 Q.store_thm 79 ("FactIterRecThm", 80 `!n acc. SND(FactIter (n,acc)) = acc * FACT n`, 81 recInduct FactIter_ind THEN RW_TAC arith_ss [] 82 THEN RW_TAC arith_ss [Once FactIter,FACT] 83 THEN Cases_on `n` 84 THEN RW_TAC std_ss [FACT, AC MULT_ASSOC MULT_SYM]); 85 86(*****************************************************************************) 87(* Implement a function Fact to compute SND(FactIter (n,1)) *) 88(*****************************************************************************) 89 90val (Fact,_,Fact_dev) = hwDefine `Fact n = SND(FactIter (n,1))`; 91 92(*****************************************************************************) 93(* Verify Fact is indeed the factorial function *) 94(*****************************************************************************) 95 96val FactThm = 97 Q.store_thm 98 ("FactThm", 99 `Fact = FACT`, 100 RW_TAC arith_ss [FUN_EQ_THM,Fact,FactIterRecThm]); 101 102(*****************************************************************************) 103(* To implement ``$*`` we build a naive iterative multiplier function *) 104(* (works by repeated addition) *) 105(*****************************************************************************) 106 107val (MultIter,MultIter_ind,MultIter_dev) = 108 hwDefine 109 `MultIter (m,n:num,acc:num) = 110 if m = 0n then (0,n,acc) else MultIter(m-1,n,n + acc)`; 111 112 113(*****************************************************************************) 114(* Two argument multiplication, defined in terms of MultIter *) 115(*****************************************************************************) 116 117val (Mult,_,Mult_dev) = 118 hwDefine 119 `Mult(m,n) = SND(SND(MultIter(m,n,0)))`; 120 121(*****************************************************************************) 122(* Verify that MultIter does compute accumulator-style multiplication *) 123(*****************************************************************************) 124 125val MultIterRecThm = (* proof adapted from similar one from KXS *) 126 Q.store_thm 127 ("MultIterRecThm", 128 `!m n acc. SND(SND(MultIter (m,n,acc))) = (m * n) + acc`, 129 recInduct MultIter_ind THEN RW_TAC std_ss [] 130 THEN RW_TAC arith_ss [Once MultIter] 131 THEN Cases_on `m` 132 THEN FULL_SIMP_TAC arith_ss [MULT]); 133 134(*****************************************************************************) 135(* Verify Mult is actually multiplication *) 136(*****************************************************************************) 137 138val MultThm = 139 Q.store_thm 140 ("MultThm", 141 `Mult = UNCURRY $*`, 142 RW_TAC arith_ss [FUN_EQ_THM,FORALL_PROD,Mult,MultIterRecThm]); 143 144(*****************************************************************************) 145(* Theorem used in an example in the README file *) 146(*****************************************************************************) 147 148val FactIter_TOTAL = 149 store_thm 150 ("FactIter_TOTAL", 151 ``TOTAL((\(n:num,acc:num). n = 0), 152 (\(n:num,acc:num). (n,acc)), 153 (\(n:num,acc:num). (n - 1,n * acc)))``, 154 RW_TAC list_ss [TOTAL_def] 155 THEN Q.EXISTS_TAC `\(x,y).x` 156 THEN GEN_BETA_TAC 157 THEN DECIDE_TAC); 158 159(*****************************************************************************) 160(* Use Mult_dev to refine ``DEV (UNCURRY $* )`` in FactIter_dev *) 161(*****************************************************************************) 162 163val FactIter1_dev = 164 REFINE (DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev])) FactIter_dev; 165 166(*****************************************************************************) 167(* Use MultIter_dev to refine ``DEV MultIter`` in FactIter1_dev *) 168(*****************************************************************************) 169 170val FactIter2_dev = 171 REFINE (DEPTHR(LIB_REFINE[MultIter_dev])) FactIter1_dev; 172 173(*****************************************************************************) 174(* Use FactIter2_dev to refine ``DEV FactIter`` in Fact_dev *) 175(*****************************************************************************) 176 177val Fact1_dev = 178 REFINE (DEPTHR(LIB_REFINE[FactIter2_dev])) Fact_dev; 179 180(*****************************************************************************) 181(* REFINE all remaining DEVs to ATM *) 182(*****************************************************************************) 183 184val Fact2_dev = REFINE (DEPTHR ATM_REFINE) Fact1_dev; 185 186(*****************************************************************************) 187(* Alternative derivation using refinement combining combinators *) 188(*****************************************************************************) 189 190val Fact3_dev = 191 REFINE 192 (DEPTHR(LIB_REFINE[FactIter_dev]) 193 THENR DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev]) 194 THENR DEPTHR(LIB_REFINE[MultIter_dev]) 195 THENR DEPTHR ATM_REFINE) 196 Fact_dev; 197 198(*****************************************************************************) 199(* Finally, create implementation of FACT (HOL's native factorial function) *) 200(*****************************************************************************) 201 202val FACT_dev = 203 save_thm 204 ("FACT_dev", 205 REWRITE_RULE [FactThm] Fact3_dev); 206 207val FACT_net = 208 save_thm 209 ("Fact_net", 210 Count.apply MAKE_NETLIST FACT_dev); 211 212val FACT_cir = 213 save_thm 214 ("Fact_cir", 215 time MAKE_CIRCUIT FACT_dev); 216 217(*****************************************************************************) 218(* Print Verilog to file FACT.vl *) 219(*****************************************************************************) 220 221val _ = PRINT_VERILOG FACT_cir; (* N.B. FACT.vl overwritten by stuff below! *) 222 223(*****************************************************************************) 224(* Print Verilog + a simulation environment to FACT.vl *) 225(* Run using: iverilog -o FACT.vvp FACT.vl; vvp FACT.vvp *) 226(*****************************************************************************) 227 228(* 229 iverilog -o FACT.vvp FACT.vl; 230 vvp FACT.vvp; 231 gtkwave FACT.vcd 232*) 233 234(*****************************************************************************) 235(* Temporary hack to work around a system prettyprinter bug *) 236(*****************************************************************************) 237 238val _ = temp_overload_on(" * ", numSyntax.mult_tm); 239 240val _ = export_theory(); 241