-------------------------   semantics-runs.m  -----------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>

--- in p.m

--- Examples For Testing Purposes

--- evaluation of expresions without services

rew RedState(?, (Let ["x" = (Bool true)] 
                (Let ["y" = (Bool false)]
                (If "x"{0} Then "y"{0} Else (Bool true))))) .
***(
rewrites: 23 in -10ms cpu (0ms real) (~ rewrites/second)
result RedState: RedState(?, Bool false)
)

rew RedState(?, (Let ["x" = (Bool true)] 
                (Let ["y" = (Lam ["z" : TBool] "x"{0})]
                "y"{0}))) .

***(
rewrites: 12 in -10ms cpu (0ms real) (~ rewrites/second)
result RedState: RedState(?, Lam["z" : TBool]Bool true)
)

rew RedState(?, (Let ["x" = (Bool true)] 
                (Let ["y" = (Lam ["z" : TBool] "x"{0})]
                (Let ["x" = (Bool false)]
                "y"{0})))) .

***(
rewrites: 34 in -10ms cpu (0ms real) (~ rewrites/second)
result RedState: RedState(?, Lam["z" : TBool]Bool true)
)

rew RedState(?, (Let ["x" = (Bool true)] 
                (Let ["y" = (Bool false)]
                (Pair ((If "x"{0} Then "x"{0} Else "y"{0}),
                      (If "x"{0} Then "y"{0} Else "x"{0})))))) .

***(
rewrites: 75 in -10ms cpu (0ms real) (~ rewrites/second)
result RedState: RedState(?, Pair (Bool true,Bool false))
)

rew RedState(?, (Let ["consfirst" = Lam [("p","l") : ((TPair TBool TBool),(TList TBool))] 
                        (Cons ((Fst "p"{0}),"l"{0}))]
                ("consfirst"{0} ((Pair ((Bool true),(Bool false))),Nil)))) .

***(
rewrites: 57 in -10ms cpu (0ms real) (~ rewrites/second)
result RedState: RedState(?, Cons (Bool true,Nil))
)

rew RedState(?, (LetRec ["x" = (Bool true)] 
                (LetRec ["y" = (Bool false)]
                (Pair ((If "x"{0} Then "x"{0} Else "y"{0}),
                       (If "x"{0} Then "y"{0} Else "x"{0})))))) .

***(
rewrites: 175 in 0ms cpu (10ms real) (~ rewrites/second)
result RedState: RedState(?, Pair (Bool true,Bool false))
)

rew RedState(?, (LetRec [("x","y") = ((Bool true),(Bool false))] 
                (Pair ((If "x"{0} Then "x"{0} Else "y"{0}),
                       (If "x"{0} Then "y"{0} Else "x"{0}))))) .

***(
rewrites: 281 in -10ms cpu (0ms real) (~ rewrites/second)
result RedState: RedState(?, Pair (Bool true,Bool false))
)

rew RedState(?, (LetRec ["fact" = Lam ["x" : TInt] 
                        (If (Equal ("x"{0},(Int 0))) 
                         Then (Int 1) 
                         Else (Mul ("x"{0}, ("fact"{0} (Minus ("x"{0}, (Int 1)))))))]
                ("fact"{0} (Int 3)))) .

***(
rewrites: 1469 in 10ms cpu (20ms real) (146900 rewrites/second)
result RedState: RedState(?, Int 6)
)

rew Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, (LetRec ["fact" = Lam ["x" : TInt] 
                          (If (Equal ("x"{0},(Int 0))) 
                           Then (Int 1) 
                           Else (Mul ("x"{0}, (Eval (Chunk ("fact"{0},(Minus ("x"{0}, (Int 1)))))))))]
                  ("fact"{0} (Int 3))))) .

***(
rewrites: 1805 in 10ms cpu (20ms real) (180500 rewrites/second)
result Process: Process(loc("l1"), addr("i1"), addr("i1"), 1, 97, RedState(?, Int 6))
)


in topologies.m

rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, 
               (LetRec ["fact" = Lam ["x" : TInt] 
                  (If (Equal ("x"{0},(Int 0))) 
                   Then (Int 1) 
                   Else (Mul ("x"{0}, ("fact"{0} (Minus ("x"{0}, (Int 1)))))))]
                (OnNeighbor ((Chunk ("fact"{0},(Plus ((Int 2),(Int 1)))), 
                             (Addr addr("a2")), (Int 50), (Addr addr("a1"))))
                 )))) .

***(
rewrites: 1625 in 50ms cpu (60ms real) (32500 rewrites/second)
result Configuration: 
    ...
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 50, RedState(?, Dummy)) 
    Process(loc("l2"), addr("i1"), addr("a2"), 1, 49, RedState(?, Int 6))
)

rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, 
               (LetRec ["fact" = Lam ["x" : TInt] 
                  (If (Equal ("x"{0},(Int 0))) 
                   Then (Int 1) 
                   Else (Mul ("x"{0}, ("fact"{0} (Minus ("x"{0}, (Int 1)))))))]
                 (OnRemote ((Chunk ("fact"{0},(Plus ((Int 2),(Int 1)))), 
                             (Addr addr("b3")), (Int 50), DefaultRoute)))))) .

***(
rewrites: 2127 in 80ms cpu (150ms real) (26587 rewrites/second)
result Configuration: 
    ...
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 50, RedState(?, Dummy)) 
    Process(loc("l2"), addr("i1"), addr("a2"), 1, 0, RedState(?, Dummy)) 
    Process(loc("l3"), addr("i1"), addr("b3"), 1, 48, RedState(?, Int 6))
)

rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, (Let ["k" = (GenerateKey empty-exl)]
                   Put((String "a"),"k"{0},(Int 17),(Int 200));
                   SetLT((String "a"),"k"{0},(Int 16),(Int 200));
                   Let ["x" = Get((String "a"),"k"{0})]
                   Delete((String "a"),"k"{0}); "x"{0}))) .

***(
rewrites: 217 in 10ms cpu (20ms real) (21700 rewrites/second)
result Configuration: 
    FreshKey(11) 
    Data(loc("l1"), empty-dil) 
    Data(loc("l2"), empty-dil) 
    Data(loc("l3"), empty-dil) 
    Data(loc("l4"), empty-dil) 
    ...
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, RedState(?, Int 16))
)

rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, Try (Plus ((Int 2),(Int 1))) Handle ["x"] (Int 0))) .

***(
rewrites: 9 in 0ms cpu (10ms real) (~ rewrites/second)
result Configuration: 
    ...
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, RedState(?, Int 3))
)

rew example-topology-1
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, 
      RedState(?, (Plus ((Int 2),(Try (Div ((Int 1),(Int 0))) Handle ["x"] (Int 0)))))) .

***(
rewrites: 8 in -10ms cpu (0ms real) (~ rewrites/second)
result Configuration: 
    ...
    Process(loc("l1"), addr("i1"), addr("i1"), 1, 100, RedState(?, Int 0))
)