Permalink
Browse files

Changes left recursion example

  • Loading branch information...
1 parent f7b4532 commit c6d05f14aae88c0dedde44f67aebdfc8329637c5 @clklein committed Nov 3, 2011
Showing with 31 additions and 11 deletions.
  1. +10 −0 aplas2011/2-models/models.rkt
  2. +18 −0 aplas2011/2-models/test.rkt
  3. +3 −11 aplas2011/slides/slides.rkt
@@ -24,6 +24,8 @@
cont-eq-red :cont-eq-red
+ left-rec-eval-ctxt :left-rec-eval-ctxt
+
Σ
subst subst-1 subst-A)
@@ -271,6 +273,14 @@
(subst-vars (x_2 any_2) ... any_3))]
[(subst-vars any) any])
+;; a left recursive definition of evaluation contexts
+(define-double-language left-rec-eval-ctxt :left-rec-eval-ctxt
+ (E (in-hole E (hole e))
+ (in-hole E (v hole))
+ hole)
+ (e (e e) (λ (x) e) x)
+ (v (λ (x) e))
+ (x variable-not-otherwise-mentioned))
;; --- an example that Casey and Robby came up with
;; that illustrates why same said pair's idea for
@@ -331,6 +331,24 @@
(term (|+1| (|#| (|+1| (call/comp (λ (k) (k (k 0))))))))
(term 4))
+;; tests of left recursive contexts
+(test-double-match #f :left-rec-eval-ctxt
+ E
+ hole
+ (((E hole))))
+(test-double-match #f :left-rec-eval-ctxt
+ E
+ (hole ((λ (x) x) (λ (x) x)))
+ (((E (hole ((λ (x) x) (λ (x) x)))))))
+(test-double-match #f :left-rec-eval-ctxt
+ E
+ ((λ (x) x) hole)
+ (((E ((λ (x) x) hole)))))
+(test-double-match #f :left-rec-eval-ctxt
+ E
+ (((λ (x) x) (λ (x) x)) hole)
+ #f)
+
;; tests of exotic relations discussed in section 5
(test-double-reduction*
@@ -76,17 +76,9 @@
(lesson "Contexts may be involved in no decompositions during a match")
(example
- Λdk/red :Λdk/red ()
- (in-hole M (|#| (in-hole E (call/comp v))))
- (|+1| (|#| (|+1| (call/comp (λ (k) (k 2))))))
- #:out-of-memory? #t)
-
-(flush-examples)
-
-(example
- wacky :wacky ()
- C
- (f (f hole))
+ left-rec-eval-ctxt :left-rec-eval-ctxt (e v x)
+ E
+ ((λ (x) x) hole)
#:out-of-memory? #t)
(flush-examples)

0 comments on commit c6d05f1

Please sign in to comment.