Executable Specification

[View trans_tst.sig] [View trans_tst.mod]

/* Some test cases for transformations */

sig trans_tst.

accum_sig trans. [View trans.sig]

type term  tm -> o.
type term' tm' -> o.

type fvars_tst   (tm -> list tm) -> o.

/* Some test cases for transformations */

module trans_tst.

accumulate trans. [View trans.mod]

% Summation from 1 to n
term (app (fix (f\ n\ 
              ifz n n (plus n (app f (pred n)))))
            (nat (s (s (s z))))).

% A term : 
% open  =  in (f (1, e))
term' (open' (clos' 
               (abs' (p\ let' (fst' p) (z\ let' (snd' p) (e\
                        plus' (plus' z (fst' e)) (fst' (snd' e))))))
               (pair' (nat' (s (s z)))
                      (pair' (nat' (s (s (s z)))) unit')))
            (f\ e\ app' f (pair' (nat' (s z)) e))).
                     

% A simple source term for closure conversion test :
% (let x = 2 in let y =3 in (fix f z. z + x + y)) 1
term
  (app
     (let (nat (s (s z))) (x\ let (nat (s (s (s z)))) (y\
       fix (f\z\ plus (plus z x) y))))
     (nat (s z))).

% A simple source term for closure conversion test :
% (let x = 2 in let y =3 in (fix f z. z + ((fix f x. x + y) x)) 1
term (app
         (let (nat (s (s z))) (x\ let (nat (s (s (s z)))) (y\
            fix (f\z\ plus z (app (fix (f\x\ plus x y)) x)))))
         (nat (s z))).
term (let (nat (s (s z))) (x\ let (nat (s (s (s z)))) (y\
       fix (f\z\ plus (plus z x) y)))).

% Test case for fvars
fvars_tst FVs :-
  pi y\ pi z\ fvars (let (nat z) (x\ fix (f\ z\ plus (plus z x) y))) 
        (y :: nil)
        (FVs y).