Browse files

Actually make ollibot code doable in ASCII by adding $ as a shorthand…

… for gnab

git-svn-id: https://svn.concert.cs.cmu.edu/lollibot/trunk@296 88e30042-7354-0410-bf5e-e4d69759226d
  • Loading branch information...
1 parent b28fbcd commit 5588f269f11353e42b823b3126eeed32a2d147e0 @robsimmons robsimmons committed Apr 3, 2012
Showing with 53 additions and 18 deletions.
  1. +43 −0 examples/lics09/cbneed-error-ascii.olf
  2. +10 −18 src/parse.sml
View
43 examples/lics09/cbneed-error-ascii.olf
@@ -0,0 +1,43 @@
+-- Call-by-need suspensions with a fixed point
+-- Robert J. Simmons
+
+{-
+''This example is derived from Figures 3 and 10 in [[readme.txt| Substructural
+Operational Semantics as Ordered Logic Programming]].''
+
+This is a modification of [[cbneed-fix.olf]] that restores a linear
+`blackhole` when a suspension is forced. If the destination is encountered
+again, then a catchable error is raised. -}
+
+{== Call-by-value functions ==}
+
+elam : eval(lam \x. E x) ->> return(lam E).
+eapp1 : eval(app E1 E2) ->> comp(app1 E2) * eval(E1).
+eapp2 : comp(app1 E2) * return(V1) ->> comp(app2 V1) * eval(E2).
+eapp3 : comp(app2 (lam λx. E0 x)) * return(V2) ->> eval(E0 V2).
+
+
+{== Exceptions ==}
+
+etry : eval(try E1 E2) ->> catch(E2) * eval(E1).
+eraise : eval(raise) ->> fail.
+epop : comp(F) * fail ->> fail.
+ecatch : catch(E2) * fail ->> eval(E2).
+eret : catch(E2) * return(V) ->> return(V).
+
+
+{== Fixed point recursion (call-by-need) ==}
+
+efix : eval(fix \x. E x) ->> ∃D. eval(E D) * $susp (E D) D.
+esusp : eval(D) * $susp E D ->> comp(bind1 D) * eval E * $blackhole(D).
+ebind : comp(bind1 D) * return(V) * $blackhole(D) ->> return(V) * !bind V D.
+evar : eval(D) * !bind V D ->> return V.
+ehole : eval(D) * $blackhole(D) ->> fail * $blackhole(D).
+
+{== Example traces ==}
+{- Both examples appeared in [[cbneed-fix.olf]], where they got stuck. Here
+they raise an error. -}
+
+%trace * eval(fix \x. x).
+%trace * eval(fix \x. app (lam \y. y) x).
+
View
28 src/parse.sml
@@ -170,24 +170,15 @@ structure Parse :> PARSE = struct
(* Transform 2:
*** Consolidate identifiers and separate separators
*)
- val transform_tok2 =
- let
- val sep =
- fn "." => true | "(" => true | ")" => true
- | "!" => true | "¡" => true | "," => true
- | "" => true | "" => true
- | "·" => true | "" => true | "*" => true
- | "" => true | "" => true
- | "" => true | "" => true | "¬" => true
- | "λ" => true | "" => true | "" => true
- | "\\" => true | "%" => true | ":" => true
- | " " => true
- | _ => false
- val parser =
- alt [satisfy sep,
- repeat1 (satisfy (not o sep)) wth concat]
- in transform (!! parser)
- end
+ val transform_tok2 = let val sep = fn "." => true | "(" => true |
+ ")" => true | "!" => true | "$" => true |
+ "¡" => true | "," => true | "" =>
+ true | "" => true | "·" => true | "" => true | "*" => true |
+ "" => true | "" => true | "" => true | "" => true | "¬" =>
+ true | "λ" => true | "" => true | "" => true | "\\" => true |
+ "%" => true | ":" => true | " " => true | _ => false val parser
+ = alt [satisfy sep, repeat1 (satisfy (not o sep)) wth concat] in
+ transform (!! parser) end
(* Transform 3:
*** Tokenize separators
@@ -214,6 +205,7 @@ structure Parse :> PARSE = struct
literal "(" >> succeed LPAREN,
literal ")" >> succeed RPAREN,
literal "!" >> succeed BANG,
+ literal "$" >> succeed GNAB,
literal "¡" >> succeed GNAB,
literal "¬" >> succeed NEG,
literal "<1>" >> succeed ONE,

0 comments on commit 5588f26

Please sign in to comment.