examples/dev/compileScript.sml

99 (*  Seq f1 f2      f1 followed by f2 in series                               *)
100 (*  Par f1 f2      f1 in parallel with f2                                    *)
101 (*  Ite f1 f2 f3   if f1 then f2 else f3                                     *)
102 (*  Rec f1 f2 f3   tail recursion with test f1, base f2 and step f3          *)
106  Define `Seq f1 f2 = \x. f2(f1 x)`;
109  Define `Par f1 f2 = \x. (f1 x, f2 x)`;
112  Define `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
122    ``Seq f1 f2 = f2 o f1``,
154    ``!f1 f2 P.
155       (P ===> DEV f2)
159       DEV (Seq f1 f2)``,
199    ``!f2 f1 P.
202       FOLLOW P f2
204       DEV (Seq f1 f2)``,
227    ``!P1 P2 f1 f2.
228       (P1 ===> DEV f1) /\  (P2 ===> DEV f2)
230       SEQ P1 P2 ===> DEV (Seq f1 f2)``,
233     THEN `DEV f2 (c1,data,c2,p_2)` by PROVE_TAC[]
234     THEN `SEQ (DEV f1) (DEV f2) (p_1,p_1',p_1'',p_2)`
242    ``!P1 P2 f1 f2.
243       (P1 ===> DEV f1) /\  (P2  ===> DEV f2)
245       PAR P1 P2 ===> DEV (Par f1 f2)``,
248     THEN `DEV f2 (start,p_1',done'',data'')` by PROVE_TAC[]
251             PAR (DEV f1) (DEV f2) (p_1,p_1',p_1'',out)`
260    ``!P1 P2 P3 f1 f2 f3.
261       (P1 ===> DEV f1) /\  (P2 ===> DEV f2) /\  (P3 ===> DEV f3)
263        ITE P1 P2 P3 ===> DEV (Ite f1 f2 f3)``,
266     THEN `DEV f2 (start_f,q,done_f,data_f)` by PROVE_TAC[]
268     THEN `ITE (DEV f1) (DEV f2) (DEV f3) (p_1,p_1',p_1'',p_2)`
275    ``!f1 f2 f3 P1 P2 P3 .
276       TOTAL(f1,f2,f3)
278       (P1 ===> DEV f1) /\  (P2 ===> DEV f2) /\  (P3 ===> DEV f3)
280        REC P1 P2 P3 ===> DEV (Rec f1 f2 f3)``,
286     THEN `DEV f2 (start_f,q,done_f,p_2)` by PROVE_TAC[]
288     THEN `REC (DEV f1) (DEV f2) (DEV f3) (p_1,p_1',p_1'',p_2)`
337    ``!f1 f2 f3.
338       TOTAL (f1,f2,f3)
340       !x. Rec f1 f2 f3 x = if f1 x then f2 x else Rec f1 f2 f3 (f3 x)``,
349    ``!f f1 f2 f3.
350       TOTAL(f1,f2,f3)
352       (!x. f x = if f1 x then f2 x else f (f3 x))
354       (f = Rec f1 f2 f3)``,
450    ``COMB (\x. (let y = f1 x in f2(x,y))) (inp,out)
452     ?v. COMB f1 (inp,v) /\ COMB f2 (inp <> v,out)``,
567    ``(?f. P f) = ?f1 f2. P(f1 <> f2)``,
579    ``(!f. P f) = !f1 f2. P(f1 <> f2)``,
709    ``(f1 <> g1 = f2 <> g2) = (f1 = f2) /\ (g1 = g2)``,
1152 val Let_def = Define `Let f1 f2 = \x:'a. let v:'c = f1(x) in f2(x,v):'b`;
1157    ``Let f1 f2 = Seq (Par (\x.x) f1) f2``,