From 2fcba80950f9ae84ed8ee0d1c3904a6dba78fb47 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Mon, 18 Jan 2016 12:10:13 -0500 Subject: [PATCH] Fixed use of case*, added TODO about things --- cur-lib/cur/stdlib/sugar.rkt | 1 + cur-test/cur/tests/stlc.rkt | 5 ++--- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt index 153fb94..900c4f0 100644 --- a/cur-lib/cur/stdlib/sugar.rkt +++ b/cur-lib/cur/stdlib/sugar.rkt @@ -84,6 +84,7 @@ (attribute d.name) (attribute d.type))])) +;; TODO: This makes for really bad error messages when an identifier is undefined. (define-syntax (#%app syn) (syntax-case syn () [(_ e) diff --git a/cur-test/cur/tests/stlc.rkt b/cur-test/cur/tests/stlc.rkt index f032be2..915b5cf 100644 --- a/cur-test/cur/tests/stlc.rkt +++ b/cur-test/cur/tests/stlc.rkt @@ -24,13 +24,12 @@ (extend-gamma : (-> Gamma Var stlc-type Gamma))) (define (lookup-gamma (g : Gamma) (x : Var)) - (case* Gamma Type g () (lambda (g : Gamma) (Maybe stlc-type)) + (match g [emp-gamma (none stlc-type)] [(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type)) - IH: ((ih-g1 : (Maybe stlc-type))) (if (var-equal? v1 x) (some stlc-type t1) - ih-g1)])) + (recur g1))])) (define-relation (has-type Gamma stlc-term stlc-type) #:output-coq "stlc.v"