[Hol-checkins] CVS: hol98/examples/dev compile.sml,1.69,1.70

[Konrad S. <sl...@us...>]

Update of /cvsroot/hol/hol98/examples/dev
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4758

Modified Files:
	compile.sml 
Log Message:
Catching up MAKE_NETLIST to recent changes.



Index: compile.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/dev/compile.sml,v
retrieving revision 1.69
retrieving revision 1.70
diff -b -C2 -d -r1.69 -r1.70
*** compile.sml	9 Feb 2006 15:45:10 -0000	1.69
--- compile.sml	18 Feb 2006 08:22:59 -0000	1.70
***************
*** 2013,2020 ****
  val MAKE_NETLIST =
   ((ptime "9" (CONV_RULE(RATOR_CONV(RAND_CONV EXISTS_OUT_CONV)))) o
!   (ptime "8" (PURE_REWRITE_RULE (!combinational_components))) o
    (ptime "7" (CONV_RULE(RATOR_CONV(RAND_CONV(REDEPTH_CONV(COMB_SYNTH_CONV)))))) o
    (ptime "6" (PURE_REWRITE_RULE [UNCURRY,FST,SND])) o
    (ptime "5" (CONV_RULE (CIRC_CONV (ONCE_DEPTH_CONV STEP5_CONV)))) o
    (ptime "4" STEP4) o 
    (ptime "3" GEN_BETA_RULE)  o
--- 2013,2023 ----
  val MAKE_NETLIST =
   ((ptime "9" (CONV_RULE(RATOR_CONV(RAND_CONV EXISTS_OUT_CONV)))) o
!   (ptime "8" (PURE_REWRITE_RULE[DEL_CONCAT,GSYM COMB_NOT, 
!                      GSYM COMB_AND, GSYM COMB_OR, GSYM COMB_MUX])) o 
    (ptime "7" (CONV_RULE(RATOR_CONV(RAND_CONV(REDEPTH_CONV(COMB_SYNTH_CONV)))))) o
    (ptime "6" (PURE_REWRITE_RULE [UNCURRY,FST,SND]))                o
+   (ptime "5-6" (REWRITE_RULE [DFF_IMP_def,POSEDGE_IMP_def,LATCH_def]))  o
    (ptime "5" (CONV_RULE (CIRC_CONV (ONCE_DEPTH_CONV STEP5_CONV)))) o
+   (ptime "4-5" (DEV_IMP (DEPTH_IMP DFF_IMP_INTRO)))                o
    (ptime "4" STEP4)          o 
    (ptime "3" GEN_BETA_RULE)  o
***************
*** 2171,2185 ****
    (ptime "12" (at_SPEC_ALL ``clk:num->bool``))                               o
    (ptime "11" GEN_ALL)                                                       o
- (* (ptime"10"(Ho_Rewrite.REWRITE_RULE[GSYM LEFT_FORALL_IMP_THM,DEL_CONCAT])) o *)
    (ptime "10-11" (CONV_RULE EXISTSL_CONV)) o
!   (ptime "10" (PURE_REWRITE_RULE[DEL_CONCAT])) o 
    (ptime "9" (CONV_RULE(RATOR_CONV(RAND_CONV EXISTS_OUT_CONV)))) o
-   (ptime "8" (PURE_REWRITE_RULE (!combinational_components))) o
    (ptime "7" (CONV_RULE(RATOR_CONV(RAND_CONV(REDEPTH_CONV(COMB_SYNTH_CONV)))))) o
- (*  SIMP_RULE std_ss [UNCURRY]                                                 o
-   Ho_Rewrite.REWRITE_RULE
-    [BUS_CONCAT_ELIM,DFF_IMP_def,POSEDGE_IMP_def,LATCH_def]                   o
- *)
- (*  (ptime "6-7" (Ho_Rewrite.REWRITE_RULE [UNCURRY,FST,SND]))           o *)
    (ptime "6-7" (PURE_REWRITE_RULE [UNCURRY,FST,SND]))           o
    (ptime "6" (REWRITE_RULE [DFF_IMP_def,POSEDGE_IMP_def,LATCH_def]))  o
--- 2174,2182 ----
    (ptime "12" (at_SPEC_ALL ``clk:num->bool``))                               o
    (ptime "11" GEN_ALL)                                                       o
    (ptime "10-11" (CONV_RULE EXISTSL_CONV)) o
!   (ptime "10" (PURE_REWRITE_RULE[DEL_CONCAT,GSYM COMB_NOT, GSYM COMB_AND, 
!                GSYM COMB_OR, GSYM COMB_MUX])) o 
    (ptime "9" (CONV_RULE(RATOR_CONV(RAND_CONV EXISTS_OUT_CONV)))) o
    (ptime "7" (CONV_RULE(RATOR_CONV(RAND_CONV(REDEPTH_CONV(COMB_SYNTH_CONV)))))) o
    (ptime "6-7" (PURE_REWRITE_RULE [UNCURRY,FST,SND]))                 o
    (ptime "6" (REWRITE_RULE [DFF_IMP_def,POSEDGE_IMP_def,LATCH_def]))  o
***************
*** 2219,2220 ****
--- 2216,2227 ----
   end;
  
+ (*---------------------------------------------------------------------------*)
+ (* Don't go all the way to circuits. Instead stop at netlists built from     *)
+ (* COMB, CONSTANT, DEL and DELT.                                             *)
+ (*---------------------------------------------------------------------------*)
+ 
+ fun netDefine qdef =
+  let val (def,ind,dev) = hwDefine qdef
+  in
+    (def,ind,MAKE_NETLIST(EXPAND_COMPONENTS(REFINE_ALL dev)))
+  end;