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