1(*****************************************************************************) 2(* Very simple compiler, with programs represented as ML list of HOL *) 3(* definitions. *) 4(*****************************************************************************) 5 6signature compile = 7sig 8 9 include Abbrev 10 11(*****************************************************************************) 12(* Error reporting function *) 13(*****************************************************************************) 14 15val ERR : string -> string -> exn 16 17(*****************************************************************************) 18(* List of definitions (useful for rewriting) *) 19(*****************************************************************************) 20 21val SimpThms : thm list 22 23(*****************************************************************************) 24(* Destruct ``d1 ===> d2`` into (``d1``,``d2``) *) 25(*****************************************************************************) 26 27val dest_dev_imp : term -> term * term 28 29(*****************************************************************************) 30(* An expression is just a HOL term built using expressions defined earlier *) 31(* in a program (see description of programs below) and Seq, Par, *) 32(* Ite and Rec: *) 33(* *) 34(* expr := Seq expr expr *) 35(* | Par expr expr *) 36(* | Ite expr expr expr *) 37(* | Rec expr expr expr *) 38(* *) 39(*****************************************************************************) 40 41(*****************************************************************************) 42(* Convert_CONV ``\(x1,...,xn). tm[x1,...,xn]`` returns a theorem *) 43(* *) 44(* |- (\(x1,...,xn). tm[x1,...,xn]) = p *) 45(* *) 46(* where p is a combinatory expression built from the combinators *) 47(* Seq, Par and Ite. An example is: *) 48(* *) 49(* - Convert_CONV ``\(x,y). if x < y then y-x else x-y``; *) 50(* > val it = *) 51(* |- (\(x,y). (if x < y then y - x else x - y)) = *) 52(* Ite (Seq (Par (\(x,y). x) (\(x,y). y)) (UNCURRY $<)) *) 53(* (Seq (Par (\(x,y). y) (\(x,y). x)) (UNCURRY $-)) *) 54(* (Seq (Par (\(x,y). x) (\(x,y). y)) (UNCURRY $-)) *) 55(* *) 56(* Notice that curried operators are uncurried. *) 57(* *) 58(*****************************************************************************) 59 60val LET_SEQ_PAR_THM : thm 61val SEQ_PAR_I_THM : thm 62 63val Convert_CONV : term -> thm 64 65(*****************************************************************************) 66(* Predicate to test whether a term occurs in another term *) 67(*****************************************************************************) 68val occurs_in : term -> term -> bool 69 70(*****************************************************************************) 71(* Convert (|- f x = e) returns a theorem *) 72(* *) 73(* |- f = p *) 74(* *) 75(* where p is a combinatory expression built from the combinators Seq, Par *) 76(* and Ite. *) 77(*****************************************************************************) 78 79val Convert : thm -> thm 80 81(*****************************************************************************) 82(* RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) (|- TOTAL(f1,f2,f3)) *) 83(* returns a theorem *) 84(* *) 85(* |- f = Rec(p1,p2,p3) *) 86(* *) 87(* where p1, p2 and p3 are combinatory expressions built from the *) 88(* combinators Seq, Par and Ite. *) 89(* *) 90(* For example, given: *) 91(* *) 92(* FactIter; *) 93(* > val it = *) 94(* |- FactIter (n,acc) = *) 95(* (if n = 0 then (n,acc) else FactIter (n - 1,n * acc)) *) 96(* *) 97(* - FactIter_TOTAL; *) 98(* > val it = *) 99(* |- TOTAL *) 100(* ((\(n,acc). n = 0), *) 101(* (\(n,acc). (n,acc)), *) 102(* (\(n,acc). (n - 1,n * acc))) *) 103(* *) 104(* then: *) 105(* *) 106(* - RecConvert FactIter FactIter_TOTAL; *) 107(* > val it = *) 108(* |- FactIter = *) 109(* Rec (Seq (Par (\(n,acc). n) (\(n,acc). 0)) (UNCURRY $=)) *) 110(* (Par (\(n,acc). n) (\(n,acc). acc)) *) 111(* (Par (Seq (Par (\(n,acc). n) (\(n,acc). 1)) (UNCURRY $-)) *) 112(* (Seq (Par (\(n,acc). n) (\(n,acc). acc)) (UNCURRY $* ))) *) 113(* *) 114(*****************************************************************************) 115val RecConvert : thm -> thm -> thm 116 117(*---------------------------------------------------------------------------*) 118(* Extract totality predicate of the form TOTAL (f1,f2,f3) for a recursive *) 119(* function of the form f(x) = if f1(x) then f2(x) else f (f3(x)) *) 120(*---------------------------------------------------------------------------*) 121 122val total_tm : term 123 124val mk_total : term * term * term -> term 125val getTotal : thm -> term 126 127 128 129(*****************************************************************************) 130(* Check if term tm is a well-formed expression built out of Seq, Par, Ite, *) 131(* Rec or Let. If so return a pair (constructor, args), else return (tm,[]) *) 132(*****************************************************************************) 133val dest_exp : term -> term * term list 134 135(*****************************************************************************) 136(* A combinational term is one that only contains constants declared *) 137(* combinational by having their names included in the assignable list *) 138(* combinational_constants *) 139(*****************************************************************************) 140val combinational_constants : string list ref 141val add_combinational : string list -> unit 142val is_combinational : term -> bool 143val is_combinational_const : term -> bool 144 145(*****************************************************************************) 146(* CompileExp exp *) 147(* --> *) 148(* [REC assumption] |- <circuit> ===> DEV exp *) 149(*****************************************************************************) 150val CompileExp : term -> thm 151 152(*****************************************************************************) 153(* CompileProg prog tm --> rewrite tm with prog, then compiles the result *) 154(*****************************************************************************) 155val CompileProg : thm list -> term -> thm 156 157(*****************************************************************************) 158(* Compile (|- f args = bdy) = CompileProg [|- f args = bdy] ``f`` *) 159(*****************************************************************************) 160val Compile : thm -> thm 161 162(*****************************************************************************) 163(* ``(f = \(x1,x2,...,xn). B)`` *) 164(* --> *) 165(* |- (f = \(x1,x2,...,xn). B) = !x1 x2 ... xn. f(x1,x2,...,xn) = B *) 166(*****************************************************************************) 167val FUN_DEF_CONV : term -> thm 168val FUN_DEF_RULE : thm -> thm 169 170(*****************************************************************************) 171(* Simp prog thm rewrites thm using definitions in prog *) 172(*****************************************************************************) 173val Simp : thm list -> thm -> thm 174 175(*****************************************************************************) 176(* SimpExp prog term expands term using definitions in prog *) 177(*****************************************************************************) 178val SimpExp : thm list -> term -> thm 179 180(*****************************************************************************) 181(* |- TOTAL(f1,f2,f3) *) 182(* ------------------------------------------- *) 183(* |- TOTAL((\x. f1 x), (\x. f2 x), (\x. f3 x)) *) 184(*****************************************************************************) 185val UNPAIR_TOTAL : thm -> thm 186 187(*****************************************************************************) 188(* Convert a non-recursive definition to an expression and then compile it *) 189(*****************************************************************************) 190val CompileConvert : thm -> thm 191 192(*****************************************************************************) 193(* Convert a recursive definition to an expression and then compile it. *) 194(*****************************************************************************) 195val RecCompileConvert : thm -> thm -> thm 196 197 198(*---------------------------------------------------------------------------*) 199(* For termination prover. *) 200(*---------------------------------------------------------------------------*) 201 202(*---------------------------------------------------------------------------*) 203(* Single entrypoint for definitions where proof of termination will succeed *) 204(* Allows measure function to be indicated in same quotation as definition, *) 205(* or not. *) 206(* *) 207(* hwDefine `(eqns) measuring f` *) 208(* *) 209(* will use f as the measure function and attempt automatic termination *) 210(* proof. If successful, returns (|- eqns, |- ind, |- dev) *) 211(* NB. the recursion equations must be parenthesized; otherwise, strange *) 212(* parse errors result. Also, the name of the defined function must be *) 213(* alphanumeric. *) 214(* *) 215(* One can also omit the measure function, as in Define: *) 216(* *) 217(* hwDefine `eqns` *) 218(* *) 219(* which will accept either non-recursive or recursive specifications. It *) 220(* returns a triple (|- eqns, |- ind, |- dev) where the ind theorem should *) 221(* be ignored for now (it will be boolTheory.TRUTH). *) 222(* *) 223(* The results of hwDefine are stored in a reference hwDefineLib. *) 224(* *) 225(*---------------------------------------------------------------------------*) 226 227val hwDefineLib : (thm * thm * thm) list ref; 228val hwDefine : term frag list -> thm * thm * thm 229 230(*****************************************************************************) 231(* Recognisers, destructors and constructors for harware combinatory *) 232(* expressions. *) 233(*****************************************************************************) 234 235(*****************************************************************************) 236(* PRECEDE abstract syntax functions *) 237(*****************************************************************************) 238val is_PRECEDE : term -> bool 239val dest_PRECEDE : term -> term * term 240val mk_PRECEDE : term * term -> term 241 242(*****************************************************************************) 243(* FOLLOW abstract syntax functions *) 244(*****************************************************************************) 245val is_FOLLOW : term -> bool 246val dest_FOLLOW : term -> term * term 247val mk_FOLLOW : term * term -> term 248 249(*****************************************************************************) 250(* ATM *) 251(*****************************************************************************) 252val is_ATM : term -> bool 253val dest_ATM : term -> term 254val mk_ATM : term -> term 255 256(*****************************************************************************) 257(* SEQ *) 258(*****************************************************************************) 259val is_SEQ : term -> bool 260val dest_SEQ : term -> term * term 261val mk_SEQ : term * term -> term 262 263(*****************************************************************************) 264(* PAR *) 265(*****************************************************************************) 266val is_PAR : term -> bool 267val dest_PAR : term -> term * term 268val mk_PAR : term * term -> term 269 270(*****************************************************************************) 271(* ITE *) 272(*****************************************************************************) 273val is_ITE : term -> bool 274val dest_ITE : term -> term * term * term 275val mk_ITE : term * term * term -> term 276 277(*****************************************************************************) 278(* REC *) 279(*****************************************************************************) 280val is_REC : term -> bool 281val dest_REC : term -> term * term * term 282val mk_REC : term * term * term -> term 283 284(*****************************************************************************) 285(* Dev *) 286(*****************************************************************************) 287val is_DEV : term -> bool 288val dest_DEV : term -> term 289val mk_DEV : term -> term 290 291(*****************************************************************************) 292(* A refinement function is an ML function that maps a term ``DEV f`` to *) 293(* a theorem *) 294(* *) 295(* |- DEV g ===> DEV f *) 296(* *) 297(* it is a bit like a conversion, but for device implication (===>) *) 298(* instead of for equality (=) *) 299(*****************************************************************************) 300 301(*****************************************************************************) 302(* Refine a device to a combinational circuit (i.e. an ATM): *) 303(* *) 304(* ATM_REFINE ``DEV f`` = |- ATM f ===> DEV f : thm *) 305(* *) 306(*****************************************************************************) 307val ATM_REFINE : term -> thm 308 309(*****************************************************************************) 310(* LIB_REFINE *) 311(* [|- <circuit> ===> DEV f1, *) 312(* |- <circuit> ===> DEV f2 *) 313(* ... *) 314(* |- <circuit> ===> DEV fn] *) 315(* ``DEV fi`` *) 316(* *) 317(* returns the first theorem <circuit> ===> DEV fi *) 318(* that it finds in the supplied list (i.e. library). *) 319(* Fails if no refining theorem found. *) 320(*****************************************************************************) 321val LIB_REFINE : thm list -> term -> thm 322 323(*****************************************************************************) 324(* DEPTHR refine tm scans through a combinatory expression tm built *) 325(* from ATM, SEQ, PAR, ITE, REC and DEV and applies the refine to all *) 326(* arguments of DEV using *) 327(* *) 328(* |- !P1 P2 Q1 Q2. P1 ===> Q1 /\ P2 ===> Q2 ==> P1 ;; P2 ===> Q1 ;; Q2 *) 329(* *) 330(* |- !P1 P2 Q1 Q2. P1 ===> Q1 /\ P2 ===> Q2 ==> P1 || P2 ===> Q1 || Q2 *) 331(* *) 332(* |- !P1 P2 Q1 Q2. *) 333(* P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3 ==> *) 334(* ITE P1 P2 P3 ===> ITE Q1 Q2 Q3 *) 335(* *) 336(* |- !P1 P2 Q1 Q2. *) 337(* P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3 ==> *) 338(* REC P1 P2 P3 ===> REC Q1 Q2 Q3 *) 339(* *) 340(* to generate a theorem *) 341(* *) 342(* |- tm' ===> tm *) 343(* *) 344(* (if refine fails, then no action is taken, i.e. |- tm ===> tm used) *) 345(*****************************************************************************) 346 347val DEPTHR : (term -> thm) -> term -> thm 348 349(*****************************************************************************) 350(* REFINE refine (|- <circuit> ===> Dev f) applies refine to <circuit> *) 351(* to generate *) 352(* *) 353(* |- <circuit'> ===> <circuit> *) 354(* *) 355(* and then uses transitivity of ===> to deduce *) 356(* *) 357(* |- <circuit'> ===> Dev f *) 358(*****************************************************************************) 359 360val REFINE : (term -> thm) -> thm -> thm 361 362(*****************************************************************************) 363(* Naively implemented refinement combinators *) 364(*****************************************************************************) 365 366(*****************************************************************************) 367(* |- t2 ===> t1 *) 368(* --------------- refine t2 = |- t3 ===> t2 *) 369(* |- t3 ===> t1 *) 370(*****************************************************************************) 371 372val ANTE_REFINE : thm -> (term -> thm) -> thm 373 374(*****************************************************************************) 375(* Apply two refinements in succession; fail if either does. *) 376(*****************************************************************************) 377(*infixr 3 THENR;*) 378 379val THENR : ('a -> thm) * (term -> thm) -> 'a -> thm 380 381(*****************************************************************************) 382(* Apply refine1; if it raises a HOL_ERR then apply refine2. Note that *) 383(* interrupts and other exceptions will sail on through. *) 384(*****************************************************************************) 385(*infixr 3 ORELSER;*) 386 387val ORELSER : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b 388 389(*****************************************************************************) 390(* Identity refinement tm --> |- tm ===> tm *) 391(*****************************************************************************) 392 393val ALL_REFINE : term -> thm 394 395(*****************************************************************************) 396(* Repeat refine until no change *) 397(*****************************************************************************) 398 399val REPEATR : (term -> thm) -> term -> thm 400 401(*****************************************************************************) 402(* Refine using hwDefineLib and then convert all remaining DEVs to ATMs *) 403(*****************************************************************************) 404 405val REFINE_ALL : thm -> thm 406 407(*****************************************************************************) 408(* Some ancient code for normalising circuits (will need to be updated!) *) 409(*****************************************************************************) 410 411(*****************************************************************************) 412(* LIST_EXISTS_ALPHA_CONV s n ``?a b c ...`` = *) 413(* |- (?a b c ...) = ?sn sn+1 sn+2 ... *) 414(*****************************************************************************) 415 416val LIST_EXISTS_ALPHA_CONV : string -> int -> term -> thm 417 418(*****************************************************************************) 419(* Standardise apart all quantified variables to ``v0``, ``v1``, ... *) 420(* where "v" is given as an argument *) 421(*****************************************************************************) 422 423val OLD_STANDARDIZE_EXISTS_CONV : string -> term -> thm 424 425(*---------------------------------------------------------------------------*) 426(* A faster version of STANDARDIZE_EXISTS_CONV. *) 427(*---------------------------------------------------------------------------*) 428 429val STANDARDIZE_EXISTS_CONV : string -> term -> thm 430 431 432(*****************************************************************************) 433(* Hoist all existential quantifiers to the outside *) 434(* *) 435(* (?x. A) /\ B --> ?x. A /\ B (check x not free in B) *) 436(* A /\ (?x. B) --> ?x. A /\ B (check x not free in A) *) 437(* *) 438(* returns a pair consisting of a list of existentially quantified vars *) 439(* and a list of conjuncts *) 440(*****************************************************************************) 441 442val EXISTS_OUT : term -> term list * term list 443 444(*****************************************************************************) 445(* PRUNE1_FUN(v,[t1,...,tp,v=u,tq,...,tn]) or *) 446(* PRUNE1_FUN(v,[t1,...,tp,u=v,tq,...,tn]) *) 447(* returns [t1[u/v],...,tp[u/v],tq[u/v],...,tn[u/v]] *) 448(* has no effect if there is no equation ``v=u`` of ``u=v`` in the list *) 449(*****************************************************************************) 450 451val PRUNE1_FUN : term * term list -> term list 452 453val EXISTS_OUT_CONV : term -> thm 454 455(*****************************************************************************) 456(* BUS_CONCAT abstract syntax functions *) 457(*****************************************************************************) 458val is_BUS_CONCAT : term -> bool 459val dest_BUS_CONCAT : term -> term * term 460val mk_BUS_CONCAT : term * term -> term 461 462(*****************************************************************************) 463(* Match a varstruct with a bus. For example: *) 464(* *) 465(* BUS_MATCH ``(m,n,acc)`` ``v102 <> v101 <> v100`` *) 466(* --> *) 467(* [(``m``,``v102``), (``n``,``v101``), (``acc``, ``v100``)] *) 468(* *) 469(* *) 470(* BUS_MATCH ``(p1 - 1,p1',p1' + p2)`` ``v165 <> v164 <> v163`` *) 471(* --> *) 472(* [(``p1 - 1``,``v165``), (``p1'``,``v164``),(``p1' + p2``,``v163``) *) 473(*****************************************************************************) 474 475val BUS_MATCH : term -> term -> (term * term) list 476 477(*****************************************************************************) 478(* Convert a varstruct to a matching bus *) 479(* Example: varstruct_to_bus ty ``(v1,(v2,v3),v4)`` = ``v1<>(v2<>v3)<>v4`` *) 480(* (where types are lifted to functions from domain ty) *) 481(*****************************************************************************) 482 483val varstruct_to_bus : hol_type -> term -> term 484 485(*****************************************************************************) 486(* A pure abstraction has the form ``\<varstruct>. <body>`` where *) 487(* <body> is built out of variables in <varstruct> and combinational *) 488(* constants using pairing. *) 489(*****************************************************************************) 490 491val is_pure_abs : term -> bool 492 493(*****************************************************************************) 494(* Generate a bus made of fresh variables from the type of a term *) 495(*****************************************************************************) 496 497val genbus : hol_type -> term -> term * term list 498 499(*****************************************************************************) 500(* Synthesise combinational circuits. *) 501(* Examples (derived from FactScript.sml): *) 502(* *) 503(* COMB (\(m,n,acc). m) (v102 <> v101 <> v100, v134) *) 504(* --> *) 505(* (v134 = v102) *) 506(* *) 507(* COMB (\(m,n,p). op <term>) (v102 <> v101 <> v100, v134) *) 508(* --> *) 509(* ?v. COMB(\(m,n,p). <term>)(v102 <> v101 <> v100,v) /\ COMB op (v,v134) *) 510(* *) 511(* COMB (\(m,n,p). (op <term1>) <term2>) (v102 <> v101 <> v100, v134) *) 512(* --> *) 513(* ?v1 v2. COMB(\(m,n,p). <term1>)(v102 <> v101 <> v100,v1) /\ *) 514(* COMB(\(m,n,p). <term2>)(v102 <> v101 <> v100,v2) /\ *) 515(* COMB (UNCURRY op) (v1 <> v2,v134) *) 516(* *) 517(* COMB (\(m,n,p). (<term1>, <term2>) (v102 <> v101 <> v100, v134 <> v135) *) 518(* --> *) 519(* ?v1 v2. COMB(\(m,n,p). <term1>)(v102 <> v101 <> v100,v1) /\ *) 520(* COMB(\(m,n,p). <term2>)(v102 <> v101 <> v100,v2) /\ *) 521(* (v134 = v1) /\ (v135 = v2) *) 522(* *) 523(* COMB (\(p1,p1',p2). (p1 - 1,p1',p1' + p2)) *) 524(* (v109 <> v108 <> v107, v165 <> v164 <> v163) *) 525(* --> *) 526(* (?v. (CONSTANT 1 v /\ COMB (UNCURRY $-) (v109 <> v, v165)) /\ *) 527(* (v164 = v108) /\ *) 528(* COMB (UNCURRY $+) (v108 <> v107, v163) *) 529(*****************************************************************************) 530 531val comb_synth_goalref : term ref 532val if_print_flag : bool ref 533val if_print : string -> unit 534val if_print_term : term -> unit 535 536val COMB_SYNTH_CONV : term -> thm 537 538(*****************************************************************************) 539(* If *) 540(* *) 541(* f tm --> |- tm' ==> tm *) 542(* *) 543(* then DEPTH_IMP f tm descends recursively through existential *) 544(* quantifications and conjunctions applying f (or tm --> |- tm ==> tm) if *) 545(* f fails) and returning |- tm' ==> tm for some term tm' *) 546(* *) 547(*****************************************************************************) 548 549val DEPTH_IMP : (term -> thm) -> term -> thm 550 551(*****************************************************************************) 552(* AP_ANTE_IMP_TRANS f (|- t1 ==> t2) applies f to t1 to get |- t0 ==> t1 *) 553(* and then, using transitivity of ==>, returns |- t0 ==> t2 *) 554(*****************************************************************************) 555 556val AP_ANTE_IMP_TRANS : (term -> thm) -> thm -> thm 557 558(*****************************************************************************) 559(* DEV_IMP f (|- tm ==> d) applies f to tm to generate an implication *) 560(* |- tm' ==> tm and then returns |- tm' ==> d *) 561(*****************************************************************************) 562 563val DEV_IMP : (term -> thm) -> thm -> thm 564 565(*****************************************************************************) 566(* DFF_IMP_INTRO ``DFF p`` --> |- DFF_IMP p => DFF p *) 567(*****************************************************************************) 568 569val DFF_IMP_INTRO : term -> thm 570 571(*****************************************************************************) 572(* Test is a term is of the from ``s1 at p`` *) 573(*****************************************************************************) 574 575val is_at : term -> bool 576 577(*****************************************************************************) 578(* IMP_REFINE (|- tm1 ==> tm2) tm matches tm2 to tm and if a substitution *) 579(* sub is found such that sub tm2 = tm then |- sub tm1 ==> sub tm2 is *) 580(* returned; if the match fails IMP_REFINE_Fail is raised. *) 581(*****************************************************************************) 582 583exception IMP_REFINE_Fail 584val IMP_REFINE : thm -> term -> thm 585 586(*****************************************************************************) 587(* IMP_REFINEL [th1,...,thn] tm applies IMP_REFINE th1,...,IMP_REFINE thn *) 588(* to tm in turn until one succeeds. If none succeeds then |- tm => tm *) 589(* is returned. Never fails. *) 590(*****************************************************************************) 591 592val IMP_REFINEL : thm list -> term -> thm 593 594(*****************************************************************************) 595(* |- !s1 ... sn. P s1 ... sn *) 596(* ------------------------------------------------------- at_SPECL ``clk`` *) 597(* ([``s1``,...,``sn``], |- P (s1 at clk) ... (sn at clk)) *) 598(*****************************************************************************) 599 600val at_SPEC_ALL : term -> thm -> term list * thm 601 602(*****************************************************************************) 603(* |- P ==> Q *) 604(* ---------------- (x not free in Q) *) 605(* |- (?x. P) ==> Q *) 606(*****************************************************************************) 607 608val ANTE_EXISTS_INTRO : term -> thm -> thm 609val LIST_ANTE_EXISTS_INTRO : term list * thm -> thm 610 611(*****************************************************************************) 612(* ``: ty1 # ... # tyn`` --> [`:ty```, ..., :``tyn``] *) 613(*****************************************************************************) 614 615val strip_prodtype : hol_type -> hol_type list 616 617(*****************************************************************************) 618(* mapcount f [x1,...,xn] = [f 1 x1, ..., f n xn] *) 619(*****************************************************************************) 620 621val mapcount : (int -> 'a -> 'b) -> 'a list -> 'b list 622 623(*****************************************************************************) 624(* ``s : ty -> ty1#...#tyn`` --> ``(s1:ty->ty1) <> ... <> (sn:ty->tyn)`` *) 625(*****************************************************************************) 626 627val bus_split : term -> term 628 629(*****************************************************************************) 630(* |- Cir ===> DEV f *) 631(* ------------------------------------------------------ *) 632(* |- Cir (load,(inp1<>...<>inpm),done,(out1<>...<>outn)) *) 633(* ==> *) 634(* DEV f (load,(inp1<>...<>inpm),done,(out1<>...<>outn)) *) 635(*****************************************************************************) 636 637val IN_OUT_SPLIT : thm -> thm 638 639(*****************************************************************************) 640(* User modifiable library of combinational components. *) 641(*****************************************************************************) 642 643val combinational_components : thm list ref 644val add_combinational_components : thm list -> unit 645 646(*---------------------------------------------------------------------------*) 647(* Building netlists *) 648(*---------------------------------------------------------------------------*) 649 650val monitor_netlist_construction : bool ref 651val ptime : string -> ('a -> 'b) -> 'a -> 'b 652val comb_tm : term 653val CIRC_CONV : (term -> thm) -> term -> thm 654val CIRC_RULE : (term -> thm) -> thm -> thm 655val COMB_FN_CONV : (term -> thm) -> term -> thm 656val variants : term list -> term list -> term list 657val is_prod : hol_type -> bool 658val bus_concat_tm : term 659val mk_bus_concat : term * term -> term 660val dest_bus_concat : term -> term * term 661val bus_concat_of : hol_type -> term list -> term * term list 662 663(*---------------------------------------------------------------------------*) 664(* STEP 4 *) 665(*---------------------------------------------------------------------------*) 666 667val FUN_EXISTS_PROD_CONV : term -> thm 668val OLD_STEP4a : thm -> thm 669val STEP4a : thm -> thm 670val STEP4b : thm -> thm 671val STEP4c : thm -> thm 672val STEP4d : thm -> thm 673val STEP4e : thm -> thm 674val STEP4f : thm -> thm 675val STEP4 : thm -> thm 676 677(*---------------------------------------------------------------------------*) 678(* STEP 5 applies theorem *) 679(* *) 680(* BUS_CONCAT_ELIM = |- (\x1. P1 x1) <> (\x2. P2 x2) = (\x. (P1 x,P2 x)) *) 681(* *) 682(* Contorted code because of efficiency hacks. *) 683(*---------------------------------------------------------------------------*) 684 685val LAMBDA_CONCAT_CONV : term -> thm 686val STEP5_CONV : term -> thm 687 688(*---------------------------------------------------------------------------*) 689(* Translate a DEV into a netlist *) 690(*---------------------------------------------------------------------------*) 691 692val MAKE_NETLIST : thm -> thm 693 694 695(*****************************************************************************) 696(* User modifiable list of Melham-style temporal abstraction theorem *) 697(*****************************************************************************) 698 699val temporal_abstractions : thm list ref 700val add_temporal_abstractions : thm list -> unit 701 702(*****************************************************************************) 703(* Compile a device implementation into a clocked circuit represented in HOL *) 704(*****************************************************************************) 705 706val MAKE_CIRCUIT : thm -> thm 707val EXISTSL_CONV : term -> thm 708val NEW_MAKE_CIRCUIT : thm -> thm 709val NEW_MAKE_CIRCUIT' : thm -> thm 710val NEW_MAKE_CIRCUIT'' : thm -> thm 711 712(*****************************************************************************) 713(* Expand occurrences of component names into their definitions *) 714(*****************************************************************************) 715 716val EXPAND_COMPONENTS : thm -> thm 717 718(*****************************************************************************) 719(* Invoke hwDefine and then apply MAKE_CIRCUIT, EXPAND_COMPONENTS and *) 720(* REFINE_ALL to the device *) 721(*****************************************************************************) 722 723val cirDefine : term frag list -> thm * thm * thm 724val newcirDefine : term frag list -> thm * thm * thm 725 726(*---------------------------------------------------------------------------*) 727(* Don't go all the way to circuits. Instead stop at netlists built from *) 728(* COMB, CONSTANT, DEL and DELT. *) 729(*---------------------------------------------------------------------------*) 730 731val netDefine : term frag list -> thm * thm * thm 732 733end (* sig *) 734