From c7aefdb03299b21024c736b45226df0274c7b032 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 14 Jan 2016 15:16:58 -0500 Subject: [PATCH] Removed Var "abstractions" Olly uses De Bruijn, but was attempting to use abstractions to allow changing that. Unfortunately, these were not really abstractions. So they're now gone. --- cur-doc/cur/scribblings/olly.scrbl | 118 ++++++++++++++++------------- cur-lib/cur/olly.rkt | 14 +--- cur-test/cur/tests/olly.rkt | 7 -- cur-test/cur/tests/stlc.rkt | 17 ++--- 4 files changed, 72 insertions(+), 84 deletions(-) diff --git a/cur-doc/cur/scribblings/olly.scrbl b/cur-doc/cur/scribblings/olly.scrbl index 59b04ce..0556ebd 100644 --- a/cur-doc/cur/scribblings/olly.scrbl +++ b/cur-doc/cur/scribblings/olly.scrbl @@ -14,11 +14,11 @@ the language. maybe-vars maybe-output-coq maybe-output-latex - (nt-name (nt-metavars) maybe-bnfdef constructors ...) ...) + (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...) #:grammar [(maybe-vars (code:line) - (code:line #:vars (nt-metavars ...))) + (code:line #:vars (nt-metavar ...))) (maybe-output-coq (code:line) (code:line #:output-coq coq-filename)) @@ -27,26 +27,51 @@ the language. (code:line #:output-latex latex-filename)) (maybe-bnfdef (code:line) - (code:line ::=))]]{ + (code:line ::=)) + (non-terminal-def + nt-metavar + (code:line terminal) + (code:line (terminal terminal-args ...))) + (terminal-args + nt-metavar + (code:line literal) + (code:line ()) + (code:line (#:bind nt-metavar . terminal-args)) + (code:line (terminal-args terminal-args ...)))]]{ Defines a new language by generating inductive definitions for each -nonterminal @racket[nt-name], whose constructors are generated by -@racket[constructors]. The constructors must either with a tag that can -be used to name the constructor, or be another meta-variable. -The meta-variables @racket[nt-metavars] are replaced by the corresponding -inductive types in @racket[constructors]. -The name of each inductive datatype is generated by -@racket[(format-id "~a-~a" name nt-name)]. +non-terminal @racket[nt-name], whose syntax is generated by +@racket[non-terminal-def]. +Each @racket[non-terminal-def] must either be a reference to a +previously defined non-terminal using a @racket[nt-metavar], a +@racket[terminal] (an identifier), or a @racket[terminal] applied to +some @racket[terminal-args]. +The @racket[terminal-args] are a limited grammar of s-expressions, +which can reference previously defined @racket[nt-metavar]s to be +treated as arguments, literal symbols to be treated as syntax, binding +declarations, or a nested @racket[terminal-arg]. -Later nonterminals can refer to prior nonterminals, but they cannot be -mutually inductive due to limitations in Cur. When nonterminals appear -in @racket[constructors], a constructor is defined that coerces one -nonterminal to another. +The inductive definitions are generated by generating a type for each +@racket[nt-name] whose name @racket[nt-type] is generated by +@racket[(format-id name "~a-~a" name nt-name)] and whose constructors +are generated by each @racket[non-terminal-def]. +For @racket[terminal]s, the constructor is a base constructor whose +name is generated by @racket[(format-id name "~a-~a" name terminal)]. +For @racket[nt-metavar]s, the constructor is a conversion constructor +whose name is generated by @racket[(format-id name "~a->~a" nt-type +nt-metavar-type)] where @racket[nt-metavar-type] is the name of the +type generated for the nonterminal to which @racket[nt-metavars] refers. +For @racket[(terminal terminal-args ...)], the constructor is a +function that expects term of of the types generated by +@racket[terminal-args ...]. If @racket[#:vars] is given, it should be a list of meta-variables that -representing variables in the language. These meta-variables should only -appear in binding positions in @racket[constructors]. These variables -are represented as De Bruijn indexes, and Olly provides some functions -for working with De Bruijn indexes. +representing variables in the language. +These variables are represented as De Bruijn indices, and uses of +variables in the syntax are treated as type @racket[Nat]. +Binding positions in the syntax, represented by @racket[#:bind +nt-metavar], are erased in converting to De Bruijn indices, although +this may change if the representation of variables used by +@racket[define-language] changes. If @racket[#:output-coq] is given, it should be a string representing a filename. The form @racket[define-language] will output Coq versions of @@ -66,8 +91,8 @@ Example: #:output-latex "stlc.tex" (val (v) ::= true false unit) (type (A B) ::= boolty unitty (-> A B) (* A A)) - (term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e) - (let (x x) = e in e))) + (term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e) + (let (#:bind x #:bind x) = e in e))) ] This example is equivalent to @@ -85,20 +110,17 @@ This example is equivalent to (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type)))) (data stlc-term : Type - (stlc-var-->-stlc-term : (forall (x : Var) stlc-term)) - (stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term)) - (stlc-term-lambda : (forall (x : Var) - (forall (y : stlc-type) + (Var->-stlc-term : (forall (x : Nat) stlc-term)) + (stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term)) + (stlc-term-lambda : (forall (y : stlc-type) (forall (z : stlc-term) - stlc-term)))) + stlc-term))) (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term))) - (stlc-term-let : (forall (x : Var) - (forall (y : Var) - (forall (e1 : stlc-term) - (forall (e2 : stlc-term) - stlc-term))))))] + (stlc-term-let : (forall (e1 : stlc-term) + (forall (e2 : stlc-term) + stlc-term))))] -@margin-note{This example is taken from @racketmodname[cur/examples/stlc]} +@margin-note{This example is taken from @racketmodname[cur/tests/stlc]} } @defform[(define-relation (name args ...) @@ -126,20 +148,20 @@ explain the syntax in detail, here is an example: #:output-latex "stlc.tex" [(g : Gamma) ------------------------ T-Unit - (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)] + (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)] [(g : Gamma) ------------------------ T-True - (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)] + (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)] [(g : Gamma) ------------------------ T-False - (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)] + (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)] - [(g : Gamma) (x : Var) (t : stlc-type) + [(g : Gamma) (x : Nat) (t : stlc-type) (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t)) ------------------------ T-Var - (has-type g (Var-->-stlc-term x) t)] + (has-type g (Var->stlc-term x) t)] [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) @@ -151,16 +173,15 @@ explain the syntax in detail, here is an example: [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (t : stlc-type) - (x : Var) (y : Var) (has-type g e1 (stlc-* t1 t2)) - (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t) + (has-type (extend-gamma (extend-gamma g t1) t2) e2 t) ---------------------- T-Let - (has-type g (stlc-let x y e1 e2) t)] + (has-type g (stlc-let e1 e2) t)] - [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var) - (has-type (extend-gamma g x t1) e1 t2) + [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) + (has-type (extend-gamma g t1) e1 t2) ---------------------- T-Fun - (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))] + (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))] [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) @@ -179,22 +200,11 @@ This example is equivalent to: (T-Unit : (forall (g : Gamma) (has-type g - (stlc-val-->-stlc-term stlc-unit) + (stlc-val->stlc-term stlc-unit) stlc-unitty))) ....)] } -@deftogether[(@defthing[Var Type] - @defthing[avar (forall (x : Nat) Var)])]{ -The type of a De Bruijn variable. -} - -@defproc[(var-equal? [v1 Var] [v2 Var]) - Bool]{ -A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2] -represent the same variable. -} - @todo{Need a Scribble library for defining Cur/Racket things in the same library in a nice way.} diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt index 7afbe1a..ca54269 100644 --- a/cur-lib/cur/olly.rkt +++ b/cur-lib/cur/olly.rkt @@ -10,9 +10,6 @@ (provide define-relation define-language - Var - avar - var-equal? generate-coq ;; private; exported for testing only @@ -252,7 +249,7 @@ [(attribute x) => (lambda (xls) (for ([x xls]) - (dict-set! (mv-map) (syntax-e x) #'Var)))]) + (dict-set! (mv-map) (syntax-e x) #'Nat)))]) (syntax-parse #'non-terminal-defs [((~var defs non-terminal-def) ...) (let ([output #`(begin defs.def ...)]) @@ -266,15 +263,6 @@ #'()) #,output))]))) -(data Var : Type (avar : (-> Nat Var))) - -(define (var-equal? (v1 : Var) (v2 : Var)) - (match v1 - [(avar (n1 : Nat)) - (match v2 - [(avar (n2 : Nat)) - (nat-equal? n1 n2)])])) - ;; See stlc.rkt for examples ;; Generate Coq from Cur: diff --git a/cur-test/cur/tests/olly.rkt b/cur-test/cur/tests/olly.rkt index 07e0d5b..3eb4c9a 100644 --- a/cur-test/cur/tests/olly.rkt +++ b/cur-test/cur/tests/olly.rkt @@ -21,13 +21,6 @@ (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n")) (output-latex-bnf #'((type (A B C) ::= unit (* A B) (+ A C)))))) -(check-equal? - (var-equal? (avar z) (avar z)) - true) -(check-equal? - (var-equal? (avar z) (avar (s z))) - false) - (begin-for-syntax (check-equal? (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns)) diff --git a/cur-test/cur/tests/stlc.rkt b/cur-test/cur/tests/stlc.rkt index ac52541..d38d930 100644 --- a/cur-test/cur/tests/stlc.rkt +++ b/cur-test/cur/tests/stlc.rkt @@ -19,10 +19,7 @@ (term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e) (let (#:bind x #:bind x) = e in e))) -(define (lookup-env (g : (List stlc-type))) - ;; TODO: Can't use match due to limitation in type inference - (elim Var Type (lambda (x : Var) (Maybe stlc-type)) - (list-ref stlc-type g))) +(define lookup-env (list-ref stlc-type)) (define (extend-env (g : (List stlc-type)) (t : stlc-type)) (cons stlc-type t g)) @@ -42,10 +39,10 @@ ------------------------ T-False (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)] - [(g : (List stlc-type)) (x : Var) (t : stlc-type) + [(g : (List stlc-type)) (x : Nat) (t : stlc-type) (== (Maybe stlc-type) (lookup-env g x) (some stlc-type t)) ------------------------ T-Var - (has-type g (Var->stlc-term x) t)] + (has-type g (Nat->stlc-term x) t)] [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) @@ -113,19 +110,19 @@ #'stlc-unitty] [(dict-ref d (syntax->datum #'e) #f) => (lambda (x) - #`(Var->stlc-term (avar #,x)))] + #`(Nat->stlc-term #,x))] [else #'e])]))) (check-equal? (begin-stlc (lambda (x : 1) x)) - (stlc-lambda stlc-unitty (Var->stlc-term (avar z)))) + (stlc-lambda stlc-unitty (Nat->stlc-term z))) (check-equal? (begin-stlc ((lambda (x : 1) x) ())) - (stlc-app (stlc-lambda stlc-unitty (Var->stlc-term (avar z))) + (stlc-app (stlc-lambda stlc-unitty (Nat->stlc-term z)) (stlc-val->stlc-term stlc-unit))) (check-equal? (begin-stlc (lambda (x : 1) (lambda (y : 1) x))) - (stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Var->stlc-term (avar (s z)))))) + (stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Nat->stlc-term (s z))))) (check-equal? (begin-stlc '(() ())) (stlc-cons (stlc-val->stlc-term stlc-unit)