examples/bmark/Bmark.sml

241     def = --`(MULT_FUN_CURRY 0 i1 i2 m t =
242                   (if t then (m,0,t) else (if i1=0 then m else i2+m,0,T)))
244              (MULT_FUN_CURRY (SUC n) i1 i2 m t =
246                    else MULT_FUN_CURRY n i1 i2 (if i1=0 then m else i2+m)
247                                        (((n-1)=0) \/ (i2=0))))`--};
257  *    --`!i1 i2 m n t.
258  *      MULT_FUN_CURRY n i1 i2 m t =
260  *        else MULT_FUN_CURRY (n-1) i1 i2 (if i1=0 then m else i2+m)
261  *                            ((((n-1)-1)=0) \/ (i2=0)))`--,
269    --`!i1 i2 m n t.
270       MULT_FUN_CURRY n i1 i2 m t =
272         else MULT_FUN_CURRY(n-1) i1 i2 (if i1=0 then m else i2+m) (((n-1)-1=0)\/(i2=0)))`--,
281    --`MULT_FUN((i1,i2),m,n,t) = MULT_FUN_CURRY n i1 i2 m t`--);
284    --`!i1 i2 m n t.
285      MULT_FUN((i1,i2),m,n,t) =
287        else MULT_FUN ((i1,i2), (if i1=0 then m else i2+m), (n-1),
288                      ((((n-1)-1)=0) \/ (i2=0))))`--,
323    --`!i1 i2 m n.
324      MULT_FUN((i1,i2),m,n,T) = (m,n,T)`--,
332    --`!i1 i2 m n.
333      MULT_FUN((i1,i2),m,n,F) =
334      MULT_FUN((i1,i2),(if i1=0 then m else i2+m),(n-1),((((n-1)-1)=0) \/ (i2=0)))`--,
402    --`!n i1 i2 m t.
403      MULT_FUN((i1,i2),m,n,t) =
407        (if ((n-1)=0)\/(i2=0) then
408         ((if i1=0 then m else i2+m),(n-1),T)
410         ((if i1=0 then m else ((n-1)*i2)+m),1,T))`--,
416        THEN ASM_CASES_TAC (--`i2=0`--)
438        --`!i1 i2.
439          (MULT_FUN((i1,i2),(if i1=0 then 0 else i2),i1,(((i1-1)=0)\/(i2=0)))) =
440           ((i1*i2), (if ((i1-1)=0)\/(i2=0) then i1 else 1), T)`--,
443         THEN ASM_CASES_TAC (--`i2=0`--)
465  [("MUX"      , --`MUX(switch,(i1:num->num),(i2:num->num),out) =
466                       !(x:num). out x = (if switch x then i1 x else i2 x)`--),
474   ("ADDER"    , --`ADDER(i1,i2,out) = !x:num. out x = i1 x + i2 x`--),
478   ("OR_GATE"  , --`OR_GATE(i1,i2,out) = !x:num. out x = (i1 x \/ i2 x)`--),
496   --`MULT_IMP(i1,i2,o1,o2,done) =
508        MUX(b4,l9,i2,l8)   /\
511        ZERO_TEST(i2,b2)   /\
546    --`!i1 i2 m n t.
547      MULT_FUN((i1,i2),m,n,t) =
552         ((i1, i2),
553          (if t then (if i1 = 0 then 0 else i2) else (if i1 = 0 then 0 else i2) + m),
555          (((if t then i1 - 1 else (n - 1) - 1) = 0) \/ (i2 = 0))))`--,
562  --`!i1 i2 m n t.
563     G_FUN((i1,i2),(m,n,t)) =
564     ((if t then (if i1 = 0 then 0 else i2) else (if i1 = 0 then 0 else i2) + m),
566      (((if t then i1 - 1 else (n - 1) - 1) = 0) \/ (i2 = 0)))`--);
579                             --`\x. ((i1:num->num) x, (i2:num->num) x)`--,
586    --`MULT_IMP(i1,i2,o1,o2,done)
589              G_FUN((i1 x,i2 x),o2 x,o1 x,done x)`--,
620     (MULT_FUN((i1 x,i2 x),G_FUN((i1 x,i2 x),o2 x,o1 x,done x)) =
621              ((i1 x * i2 x),
622               (if ((i1 x - 1) = 0) \/ (i2 x = 0)
646    --`MULT_IMP(i1,i2,o1,o2,done)        /\
648       STABLE(x,x + d)(\x'. i1 x',i2 x') /\
650        (o2(x + d) = i1 x * i2 x)`--,