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