Fix all the examples broken by the change of binder syntax - a space …

…now must appear after a binder - Lambda x. x not Lambda x.x.

git-svn-id: https://svn.concert.cs.cmu.edu/lollibot/trunk@293 88e30042-7354-0410-bf5e-e4d69759226d

examples/kripke/modal.olf

@@ -3,13 +3,13 @@
 e/var  : @ W • eval X • !bind X W V
             ->> @ W • return V.
 e/lam  : eval (lam λx. M x)
-            ->> return (lam λx.M x).
+            ->> return (lam λx. M x).
 e/app1 : eval (app M N)
             ->> eval M • cont (app₁ N).
 e/app2 : return V • cont (app₁ N)
             ->> eval N • cont (app₂ V).
 e/app3 : @ W • return V • cont (app₂ (lam λx. M x)) 
-            ->> ∃x. !bind x W V' •
+            ->> ∃x. !bind x W V •
                 @ W • eval (M x).
 
 {- Box rules -}
@@ -36,8 +36,8 @@ e/dia2 : @ W' • return V • cont (dia₁ W ≤ W')
                 @ W • eval (dia W ≤ W' loc).
 
 -- And again, no need to store W. But we *DO* have to store W'' somewhere.
-e/let1 : @ W'' • eval (letdia W M λα.λx.N α x)
-            ->> @ W • eval M • cont (letdia₁ W'' W λα.λx.N α x).
+e/let1 : @ W'' • eval (letdia W M λα. λx. N α x)
+            ->> @ W • eval M • cont (letdia₁ W'' W λα. λx. N α x).
 
-e/let2 : @ W • return (dia W ≤ W' Loc) • cont (letdia₁ W'' W λα.λx.N α x)
+e/let2 : @ W • return (dia W ≤ W' Loc) • cont (letdia₁ W'' W λα. λx. N α x)
             ->> @ W'' • eval (N W' Loc).      

examples/kripke/modal2.olf

@@ -6,13 +6,13 @@
 e/var  : @ W • eval X • !bind X W V
             ->> @ W • return V.
 e/lam  : eval (lam λx. M x)
-            ->> return (lam λx.M x).
+            ->> return (lam λx. M x).
 e/app1 : eval (app M N)
             ->> eval M • cont (app₁ N).
 e/app2 : return V • cont (app₁ N)
             ->> eval N • cont (app₂ V).
 e/app3 : @ W • return V • cont (app₂ (lam λx. M x)) 
-            ->> ∃x. !bind x W V' •
+            ->> ∃x. !bind x W V •
                 @ W • eval (M x).
 
 {=== Box rules ===}
@@ -39,10 +39,10 @@ e/dia2 : @ W' • return V • cont (dia₁ W ≤ W')
                 @ W • eval (dia W ≤ W' loc).
 
 -- And again, no need to store W. But we *DO* have to store W'' somewhere.
-e/let1 : @ W'' • eval (letdia W M λα.λx.N α x)
-            ->> @ W • eval M • cont (letdia₁ W'' W λα.λx.N α x).
+e/let1 : @ W'' • eval (letdia W M λα. λx. N α x)
+            ->> @ W • eval M • cont (letdia₁ W'' W λα. λx. N α x).
 
-e/let2 : @ W • return (dia W ≤ W' Loc) • cont (letdia₁ W'' W λα.λx.N α x)
+e/let2 : @ W • return (dia W ≤ W' Loc) • cont (letdia₁ W'' W λα. λx. N α x)
             ->> @ W'' • eval (N W' Loc).      
 
 {- 

examples/lics09/asynch.lolf

@@ -10,7 +10,7 @@ Substructural Operational Semantics as Ordered Logic Programming]].''
 > r₁ : eval(lam λx. E x) ->> return(lam E).
 > r₂ : eval(app E₁ E₂) ->> comp(app₁ E₂) • eval(E₁).
 > r₃ : comp(app₁ E₂) • return(V₁) ->> comp(app₂ V₁) • eval(E₂).
-> r₄ : comp(app₂ (lam λx.E₀ x)) • return(V₂) ->> eval(E₀ V₂).
+> r₄ : comp(app₂ (lam λx. E₀ x)) • return(V₂) ->> eval(E₀ V₂).
 
 
 == Asynchronous communication ==

examples/lics09/cbn.olf

@@ -14,6 +14,6 @@ r₃ : comp(app₁ E₂) • return(lam (λx. E₁' x)) ->> eval(E₁' E₂).
 
 {== Example trace ==}
 
-%trace * eval(app (lam λx.x) (app (lam λy.y) (lam λz.c))).
+%trace * eval(app (lam λx. x) (app (lam λy. y) (lam λz. c))).
 
 

examples/lics09/cbneed-error.olf

@@ -14,7 +14,7 @@ again, then a catchable error is raised. -}
 elam : eval(lam λx. E x) ->> return(lam E).
 eapp₁ : eval(app E₁ E₂) ->> comp(app₁ E₂) • eval(E₁).
 eapp₂ : comp(app₁ E₂) • return(V₁) ->> comp(app₂ V₁) • eval(E₂).
-eapp₃ : comp(app₂ (lam λx.E₀ x)) • return(V₂) ->> eval(E₀ V₂).
+eapp₃ : comp(app₂ (lam λx. E₀ x)) • return(V₂) ->> eval(E₀ V₂).
 
 
 {== Exceptions ==}

examples/lics09/cbneed-fix.olf

@@ -16,7 +16,7 @@ nontermination]] and [[cbneed-error.olf | raising an error]].
 elam : eval(lam λx. E x) ->> return(lam E).
 eapp₁ : eval(app E₁ E₂) ->> comp(app₁ E₂) • eval(E₁).
 eapp₂ : comp(app₁ E₂) • return(V₁) ->> comp(app₂ V₁) • eval(E₂).
-eapp₃ : comp(app₂ (lam λx.E₀ x)) • return(V₂) ->> eval(E₀ V₂).
+eapp₃ : comp(app₂ (lam λx. E₀ x)) • return(V₂) ->> eval(E₀ V₂).
 
 {== Fixed point recursion (call-by-need) ==}
 
@@ -53,4 +53,4 @@ state; the trace would go forever if it was not ended by the `18` passed
 as an argument to `%trace`.
 -}
 
-%trace 18 eval(app (fix λf. lam λx. app f x) (lam λz.z)).
+%trace 18 eval(app (fix λf. lam λx. app f x) (lam λz. z)).

examples/lics09/cbneed-nonterm.olf

@@ -16,7 +16,7 @@ cetrain traces that would become stuck in the specification from
 elam : eval(lam λx. E x) ->> return(lam E).
 eapp₁ : eval(app E₁ E₂) ->> comp(app₁ E₂) • eval(E₁).
 eapp₂ : comp(app₁ E₂) • return(V₁) ->> comp(app₂ V₁) • eval(E₂).
-eapp₃ : comp(app₂ (lam λx.E₀ x)) • return(V₂) ->> eval(E₀ V₂).
+eapp₃ : comp(app₂ (lam λx. E₀ x)) • return(V₂) ->> eval(E₀ V₂).
 
 {== Fixed point recursion (call-by-need) ==}
 

examples/lics09/cbneed.lolf

@@ -36,7 +36,7 @@ Call-by-need has a particular interesting behavior: some non-termination
 that happens due to recursion can be detected at runtime! The particular
 type of non-termination 
 
-> %trace * eval (app (lam λx. app x x) (app (lam λy.y) (lam λz.z))).
+> %trace * eval (app (lam λx. app x x) (app (lam λy. y) (lam λz. z))).
 
 > %trace 10 eval(
 >   app (app 

examples/lics09/cbv.olf

@@ -11,8 +11,8 @@ Operational Semantics as Ordered Logic Programming]].''
 r₁ : eval(lam λx. E x) ->> return(lam E).
 r₂ : eval(app E₁ E₂) ->> comp(app₁ E₂) • eval(E₁).
 r₃ : comp(app₁ E₂) • return(V₁) ->> comp(app₂ V₁) • eval(E₂).
-r₄ : comp(app₂ (lam λx.E₀ x)) • return(V₂) ->> eval(E₀ V₂).
+r₄ : comp(app₂ (lam λx. E₀ x)) • return(V₂) ->> eval(E₀ V₂).
 
 {== Example trace ==}
 
-%trace * eval(app (lam λx.x) (app (lam λy.y) (lam λz.c))).
+%trace * eval(app (lam λx. x) (app (lam λy. y) (lam λz. c))).

examples/lics09/mutable.olf

@@ -12,7 +12,7 @@ vlam : eval(lam λx. E x) ->> return(lam λx. E x).
 
 eapp₁ : eval(app E₁ E₂) ->> comp(app₁ E₂) • eval(E₁).
 eapp₂ : comp(app₁ E₂) • return(V₁) ->> comp(app₂ V₁) • eval(E₂).
-eapp₃ : comp(app₂ (lam λx.E₀ x)) • return(V₂) ->> eval(E₀ V₂).
+eapp₃ : comp(app₂ (lam λx. E₀ x)) • return(V₂) ->> eval(E₀ V₂).
 
 {== Mutable storage ==}
 

examples/lics09/pairs.olf

@@ -13,8 +13,8 @@ eunit : eval(unit) ->> return unit.
 epair₁ : eval(pair E₁ E₂) ->> comp(pair₁) • eval(E₁) • eval(E₂).
 epair₂ : comp(pair₁) • return(V₁) • return(V₂) ->> return(pair V₁ V₂).
 
-elet₁ : eval(split E (λx₁.λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
-elet₂ : eval(split₁ (λx₁.λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).
+elet₁ : eval(split E (λx₁. λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
+elet₂ : eval(split₁ (λx₁. λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).
 
 {== Example traces ==}
 

examples/lics09/par-exn1.olf

@@ -21,8 +21,8 @@ eunit : eval(unit) ->> return(unit).
 epair₁ : eval(pair E₁ E₂) ->> comp(pair₁) • eval(E₁) • eval(E₂).
 epair₂ : comp(pair₁) • return(V₁) • return(V₂) ->> return(pair V₁ V₂).
 
-elet₁ : eval(split E (λx₁.λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
-elet₂ : eval(split₁ (λx₁.λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).
+elet₁ : eval(split E (λx₁. λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
+elet₂ : eval(split₁ (λx₁. λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).
 
 {== Exceptions (Figure 10) ==}
 

examples/lics09/par-exn2.olf

@@ -19,8 +19,8 @@ eunit : eval(unit) ->> return(unit).
 epair₁ : eval(pair E₁ E₂) ->> comp₂(pair₁) • eval(E₁) • eval(E₂).
 epair₂ : comp₂(pair₁) • return(V₁) • return(V₂) ->> return(pair V₁ V₂).
 
-elet₁ : eval(split E (λx₁.λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
-elet₂ : eval(split₁ (λx₁.λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).
+elet₁ : eval(split E (λx₁. λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
+elet₂ : eval(split₁ (λx₁. λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).
 
 {== Exceptions (Figure 10), including exceptions for comp₂ frames ==}
 {- Because we have generically defined a suspended computation, we can 

examples/ml5/lambda5.olf

@@ -29,9 +29,9 @@ effect, they do not distinguish between `eval` and `return`. Because we do, it
 is necessary to have a rule that switches from evaluating to returning when an 
 immediate value is reached. -}
 
-⊃i-v : @ W • eval(lam λx.M x) ->> @ W • return(lam λx.M x).
+⊃i-v : @ W • eval(lam λx. M x) ->> @ W • return(lam λx. M x).
 ♢i-v : @ W • eval(there W L) ->> @ W • return(there W L).
-□i-v : @ W • eval(box λω.M ω) ->> @ W • return(box λω.M ω).
+□i-v : @ W • eval(box λω. M ω) ->> @ W • return(box λω. M ω).
 
 {=== Basic types ===}
 
@@ -42,7 +42,7 @@ immediate value is reached. -}
   @ W • return(V) • comp(app □ N) ->>
   @ W • eval(N) • comp(app V □).
 ⊃e-r : -- app-reduce
-  @ W • return(V) • comp(app (lam λx.M x) □) ->>
+  @ W • return(V) • comp(app (lam λx. M x) □) ->>
   @ W • eval(M V).
 
 {=== Modal types ===}
@@ -57,10 +57,10 @@ persistent atomic proposition `!bind W L V`, where `L` is a fresh parameter. -}
   @ W • ∃L. return(there W L) • !bind W L V. -- Bindings are located at a world
 
 ♢e-p : -- letd-push
-  @ W • eval(letdia M λω.λx.N ω x) ->>
-  @ W • eval(M) • comp(letdia □ λω.λx.N ω x).
+  @ W • eval(letdia M λω. λx. N ω x) ->>
+  @ W • eval(M) • comp(letdia □ λω. λx. N ω x).
 ♢e-r : -- letd-reduce
-  @ W • return(there W' L) • comp(letdia □ λω.λx.N ω x) ->>
+  @ W • return(there W' L) • comp(letdia □ λω. λx. N ω x) ->>
   @ W • eval(N W' L).
 
 {- The lookup rule requires that the the current world and the location both
@@ -79,7 +79,7 @@ alternatively been used. -}
   @ W • eval(unbox M) ->>
   @ W • eval(M) • comp(unbox □).
 □e-r : -- unbox-reduce
-  @ W • return(box λw.M w) • comp(unbox □) ->>
+  @ W • return(box λw. M w) • comp(unbox □) ->>
   @ W • return(M W).
 
 {=== Communication ===}
@@ -120,7 +120,7 @@ get₂ : -- get-push (second part)
 {- First, we show a "round trip" - a valid value being passed from the client 
 to the server, and then back to the client. -}
 
-%trace * @ server • @ client • eval(get server (get client (box λω. lam λx.x))).
+%trace * @ server • @ client • eval(get server (get client (box λω. lam λx. x))).
 
 {- We can iterate this as much as we want... this trace stops after 17 steps 
 at the point where the client is finally prepared to return the value to the 
@@ -137,16 +137,16 @@ on to somewhere else. -}
                                  (get server
                                    (get client
                                      (get server
-                                       (get client (box λω. lam λx.x))))))))).
+                                       (get client (box λω. lam λx. x))))))))).
 
 {- Multiple worlds are not necessary, here is a one-world trace where the 
 client continually gets from itself. -}
 
 %trace *
-  @ client • eval(get client (get client (get client (box λω. lam λx.x)))).
+  @ client • eval(get client (get client (get client (box λω. lam λx. x)))).
 
 {- We can have more than two worlds, as this example with worlds `a`, `b`, and 
 `c` shows. -}
 
 %trace * 
-  @ a • eval(get b (get c (get b (get a (box λω. lam λx.x))))) • @ b • @ c.
+  @ a • eval(get b (get c (get b (get a (box λω. lam λx. x))))) • @ b • @ c.

examples/syntax.olf

@@ -28,7 +28,7 @@ r₃ : a₃ X Z · b₃ Y Z  ↠ ∃w. c₃ X Y w.
 r₄ : a₄ X Z * b₄ Y Z ->> Exists w. c₄ X Y w.
 
 -- Local existential quantification in the premise
-r₅ : ∀x. ∀y. (∃z. a₅ x z · b₅ y z)  ↠  ∃w. c₅ x y w.
+r₅ : ∀x. ∀y. (∃z. a₅ x z · b₅ y z)  ↠  ∃*w. c₅ x y w.
 r₆ : All x. All y. (Exists z. a₆ x z * b₆ y z) ->> Exists w. c₆ x y w.