suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixed binding in olly

Browse Source
This commit is contained in:
William J. Bowman 2016-01-12 21:33:08 -05:00
parent f0dce3bf92
commit 9fb4c55799
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
2 changed files with 103 additions and 68 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

89
cur-lib/cur/olly.rkt
View File

@ -117,32 +117,45 @@
#:exists 'append))) #:exists 'append)))
(begin-for-syntax (begin-for-syntax
;; A mutable map from non-terminal meta-variables names to their types ;; A mutable dictionary from non-terminal meta-variables names to their types.
(define mv-map (make-parameter #f)) (define mv-map (make-parameter #f))
;; A set containing the meta-variables that represent variables.
(define vars (make-parameter #f))
;; The language name for the language currently being parsed
(define lang-name (make-parameter #f))
;; A meta-variable is any identifiers that belongs to the mv-map ;; A meta-variable is any identifiers that belongs to the mv-map
(define-syntax-class meta-variable (define-syntax-class meta-variable
(pattern (pattern
e:id x:id
#:attr sym (syntax->datum #'e) #:attr sym (syntax->datum #'x)
#:fail-unless (dict-has-key? (mv-map) (attribute sym)) #f #:fail-unless (dict-has-key? (mv-map) (attribute sym)) #f
#:attr type (dict-ref (mv-map) (attribute sym)))) #:attr type (dict-ref (mv-map) (attribute sym))))
;; A var-meta-variable is a meta-variable that is declared to be
;; treated as a variable in the defined language.
(define-syntax-class var-meta-variable
(pattern
x:id
#:fail-unless (set-member? (vars) (syntax->datum #'x)) #f))
;; A terminal is a idnetifiers that is not a meta-variable. A terminal will always represent a constructor. ;; A terminal is a idnetifiers that is not a meta-variable. A terminal will always represent a constructor.
(define-syntax-class (terminal lang-name) (define-syntax-class terminal
(pattern (pattern
x:id x:id
#:attr sym (syntax->datum #'x) #:attr sym (syntax->datum #'x)
#:fail-when (dict-has-key? (mv-map) (attribute sym)) #f #:fail-when (dict-has-key? (mv-map) (attribute sym)) #f
#:attr constructor-name #:attr constructor-name
(format-id #'x "~a-~a" lang-name #'x))) (format-id #'x "~a-~a" (lang-name) #'x)))
;; A nested-expression can appear as the argument to a terminal in ;; A nested-expression can appear as the argument to a terminal in
;; an expression, or as a sub-expression in a nested-expression. ;; an expression, or as a sub-expression in a nested-expression.
;; Each nested-expression export args, a list of types the ;; Each nested-expression export args, a list of types the
;; nested-expression represents and the list of types the non-terminal's ;; nested-expression represents and the list of types the non-terminal's
;; constructor expects in this case. ;; constructor expects in this case.
(define-syntax-class (nested-expression non-terminal-type lang-name) (define-syntax-class (nested-expression non-terminal-type)
;; A meta-variable is a nested-expression ;; A meta-variable is a nested-expression
(pattern (pattern
e:meta-variable e:meta-variable
@ -155,21 +168,32 @@
#:attr args #:attr args
'()) '())
;; So is an empty list
(pattern
()
#:attr args
'())
;; We use De-Bruijn indices, so binding positions are removed.
(pattern
(#:bind x:var-meta-variable . (~var t (nested-expression non-terminal-type)))
#:attr args
(attribute t.args))
;; A nested-expression applied to other nested expressions is a nested-expression ;; A nested-expression applied to other nested expressions is a nested-expression
(pattern (pattern
((~var h (nested-expression non-terminal-type lang-name)) ((~var h (nested-expression non-terminal-type))
(~var t (nested-expression non-terminal-type lang-name)) ...) (~var t (nested-expression non-terminal-type)) ...)
#:attr args #:attr args
(for/fold ([ls (attribute h.args)]) (for/fold ([ls (attribute h.args)])
([args (attribute t.args)]) ([args (attribute t.args)])
(append ls args)))) (append ls args))))
;; a expression is parameterized by the name of the non-terminal to ;; a expression is parameterized by the name of the non-terminal to
;; which is belongs, the language name, and the map of meta-varibles to ;; which is belongs,
;; their types.
;; Each expression exports a constr-decl, which declares a ;; Each expression exports a constr-decl, which declares a
;; constructor for the non-terminal type. ;; constructor for the non-terminal type.
(define-syntax-class (expression non-terminal-type lang-name) (define-syntax-class (expression non-terminal-type)
;; A meta-variable is a valid expression. ;; A meta-variable is a valid expression.
;; Generates a conversion constructor in constr-decl, and the type of ;; Generates a conversion constructor in constr-decl, and the type of
(pattern (pattern
@ -181,32 +205,30 @@
;; An identifier is a valid expression, generating a base constructor. ;; An identifier is a valid expression, generating a base constructor.
(pattern (pattern
(~var x (terminal lang-name)) x:terminal
#:attr constr-decl #:attr constr-decl
#`(x.constructor-name : #,non-terminal-type)) #`(x.constructor-name : #,non-terminal-type))
;; A terminal applied to a nested-expression is a valid expression. ;; A terminal applied to a nested-expression is a valid expression.
(pattern (pattern
((~var x (terminal lang-name)) . (~var c (nested-expression non-terminal-type lang-name))) (x:terminal . (~var c (nested-expression non-terminal-type)))
#:attr constr-decl #:attr constr-decl
#`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type)))) #`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))))
;; Syntax class non-terminal-def is parameterized by a language name (define-syntax-class non-terminal-def
;; to the inductive types representing their non-terminal.
(define-syntax-class (non-terminal-def lang-name)
(pattern (pattern
(name:id (name:id
(meta-var:id ...+) (meta-var:id ...+)
(~optional (~datum ::=)) (~optional (~datum ::=))
;; Create a name for the type of this non-terminal, from the ;; Create a name for the type of this non-terminal, from the
;; language name and the non-terminal name. ;; language name and the non-terminal name.
(~bind [nt-type (format-id #'name "~a-~a" lang-name #'name)]) (~bind [nt-type (format-id #'name "~a-~a" (lang-name) #'name)])
;; Imperatively update the map from meta-variables to the ;; Imperatively update the map from meta-variables to the
;; nt-type, to be used when generating the types of the constructors ;; nt-type, to be used when generating the types of the constructors
;; for this and later non-terminal. ;; for this and later non-terminal.
(~do (for ([mv (syntax->datum #'(meta-var ...))]) (~do (for ([mv (syntax->datum #'(meta-var ...))])
(dict-set! (mv-map) mv (attribute nt-type)))) (dict-set! (mv-map) mv (attribute nt-type))))
(~var c (expression (attribute nt-type) lang-name)) ...) (~var c (expression (attribute nt-type))) ...)
;; Generates the inductive data type for this non-terminal definition. ;; Generates the inductive data type for this non-terminal definition.
#:attr def #:attr def
#`(data nt-type : Type c.constr-decl ...)))) #`(data nt-type : Type c.constr-decl ...))))
@ -215,19 +237,24 @@
;; TODO: Extend define-language with syntax such as .... ;; TODO: Extend define-language with syntax such as ....
;; (term (e) ::= (e1 e2) ((lambda (x) e) ;; (term (e) ::= (e1 e2) ((lambda (x) e)
(define-syntax (define-language syn) (define-syntax (define-language syn)
(parameterize ([mv-map (make-hash)]) (define/syntax-parse
(syntax-parse syn (_ name:id
[(_ lang-name:id (~optional (~seq #:vars (x:id ...)))
(~optional (~seq #:vars (x:id ...))) (~optional (~seq #:output-coq coq-file:str))
;; Update the mv-map to include x -> Var for each x (~optional (~seq #:output-latex latex-file:str))
(~do (cond .
[(attribute x) => non-terminal-defs)
(lambda (xls) syn)
(for ([x xls]) (parameterize ([mv-map (make-hash)]
(dict-set! (mv-map) (syntax-e x) #'Var)))])) [lang-name #'name]
(~optional (~seq #:output-coq coq-file:str)) [vars (apply set (map syntax->datum (or (attribute x) '())))])
(~optional (~seq #:output-latex latex-file:str)) (cond
(~var defs (non-terminal-def #'lang-name)) ...) [(attribute x) =>
(lambda (xls)
(for ([x xls])
(dict-set! (mv-map) (syntax-e x) #'Var)))])
(syntax-parse #'non-terminal-defs
[((~var defs non-terminal-def) ...)
(let ([output #`(begin defs.def ...)]) (let ([output #`(begin defs.def ...)])
;; TODO: Should do this via attributes ;; TODO: Should do this via attributes
(when (attribute latex-file) (when (attribute latex-file)

82
cur-test/cur/tests/stlc.rkt
View File

@ -15,8 +15,8 @@
(val (v) ::= true false unit) (val (v) ::= true false unit)
;; TODO: Allow datum, like 1, as terminals ;; TODO: Allow datum, like 1, as terminals
(type (A B) ::= boolty unitty (-> A B) (* A A)) (type (A B) ::= boolty unitty (-> A B) (* A A))
(term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e) (term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
(let (x x) = e in e))) (let (#:bind x #:bind x) = e in e)))
;; TODO: Abstract this over stlc-type, and provide from in OLL ;; TODO: Abstract this over stlc-type, and provide from in OLL
(data Gamma : Type (data Gamma : Type
@ -31,6 +31,17 @@
(some stlc-type t1) (some stlc-type t1)
(recur g1))])) (recur g1))]))
(define (shift-var (v : Var))
(match v
[(avar (n : Nat))
(avar (s n))]))
(define (shift (g : Gamma))
(match g
[emp-gamma emp-gamma]
[(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
(extend-gamma (recur g1) (shift-var v1) t1)]))
(define-relation (has-type Gamma stlc-term stlc-type) (define-relation (has-type Gamma stlc-term stlc-type)
#:output-coq "stlc.v" #:output-coq "stlc.v"
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
@ -61,16 +72,15 @@
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(t : stlc-type) (t : stlc-type)
(x : Var) (y : Var)
(has-type g e1 (stlc-* t1 t2)) (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 (shift (shift g)) (avar z) t1) (avar (s z)) t2) e2 t)
---------------------- T-Let ---------------------- 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) [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
(has-type (extend-gamma g x t1) e1 t2) (has-type (extend-gamma (shift g) (avar z) t1) e1 t2)
---------------------- T-Fun ---------------------- 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) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
@ -84,55 +94,53 @@
;; TODO: When generating a parser, will need something like (#:name app (e e)) ;; TODO: When generating a parser, will need something like (#:name app (e e))
;; so I can name a constructor without screwing with syntax. ;; so I can name a constructor without screwing with syntax.
(begin-for-syntax (begin-for-syntax
(define index #'z)) (define (dict-shift d)
(for/fold ([d (make-immutable-hash)])
([(k v) (in-dict d)])
(dict-set d k #`(s #,v)))))
(define-syntax (begin-stlc syn) (define-syntax (begin-stlc syn)
(set! index #'z) (let stlc ([syn (syntax-case syn () [(_ e) #'e])]
(let stlc ([syn (syntax-case syn () [(_ e) #'e])]) [d (make-immutable-hash)])
(syntax-parse syn (syntax-parse syn
#:datum-literals (lambda : prj * -> quote let in cons bool) #:datum-literals (lambda : prj * -> quote let in cons bool)
[(lambda (x : t) e) [(lambda (x : t) e)
(let ([oldindex index]) #`(stlc-lambda #,(stlc #'t d) #,(stlc #'e (dict-set (dict-shift d) (syntax->datum #'x) #`z)))]
(set! index #`(s #,index))
;; Replace x with a de bruijn index, by running a CIC term at
;; compile time.
(normalize/syn
#`((lambda (x : stlc-term)
(stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
(Var->stlc-term (avar #,oldindex)))))]
[(quote (e1 e2)) [(quote (e1 e2))
#`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))] #`(stlc-cons #,(stlc #'e1 d) #,(stlc #'e2 d))]
[(let (x y) = e1 in e2) [(let (x y) = e1 in e2)
(let* ([y index] #`(stlc-let #,(stlc #'t d) #,(stlc #'e1 d)
[x #`(s #,y)]) #,(stlc #'e2 (dict-set* (dict-shift (dict-shift d))
(set! index #`(s (s #,index))) (syntax->datum #'x) #`z
#`((lambda (x : stlc-term) (y : stlc-term) (syntax->datum #'y) #`(s z))))]
(stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
#,(stlc #'e2)))
(Var->stlc-term (avar #,x))
(Var->stlc-term (avar #,y))))
#`(let x i #,(stlc #'e1))]
[(e1 e2) [(e1 e2)
#`(stlc-app #,(stlc #'e1) #,(stlc #'e2))] #`(stlc-app #,(stlc #'e1 d) #,(stlc #'e2 d))]
[() #'(stlc-val->stlc-term stlc-unit)] [() #'(stlc-val->stlc-term stlc-unit)]
[#t #'(stlc-val->stlc-term stlc-true)] [#t #'(stlc-val->stlc-term stlc-true)]
[#f #'(stlc-val->stlc-term stlc-false)] [#f #'(stlc-val->stlc-term stlc-false)]
[(t1 * t2) [(t1 * t2)
#`(stlc-* #,(stlc #'t1) #,(stlc #'t2))] #`(stlc-* #,(stlc #'t1 d) #,(stlc #'t2 d))]
[(t1 -> t2) [(t1 -> t2)
#`(stlc--> #,(stlc #'t1) #,(stlc #'t2))] #`(stlc--> #,(stlc #'t1 d) #,(stlc #'t2 d))]
[bool #`stlc-boolty] [bool #`stlc-boolty]
[e [e
(if (eq? 1 (syntax->datum #'e)) (cond
#'stlc-unitty [(eq? 1 (syntax->datum #'e))
#'e)]))) #'stlc-unitty]
[(dict-ref d (syntax->datum #'e) #f) =>
(lambda (x)
#`(Var->stlc-term (avar #,x)))]
[else #'e])])))
(check-equal? (check-equal?
(begin-stlc (lambda (x : 1) x)) (begin-stlc (lambda (x : 1) x))
(stlc-lambda (avar z) stlc-unitty (Var->stlc-term (avar z)))) (stlc-lambda stlc-unitty (Var->stlc-term (avar z))))
(check-equal? (check-equal?
(begin-stlc ((lambda (x : 1) x) ())) (begin-stlc ((lambda (x : 1) x) ()))
(stlc-app (stlc-lambda (avar z) stlc-unitty (Var->stlc-term (avar z))) (stlc-app (stlc-lambda stlc-unitty (Var->stlc-term (avar z)))
(stlc-val->stlc-term stlc-unit))) (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))))))
(check-equal? (check-equal?
(begin-stlc '(() ())) (begin-stlc '(() ()))
(stlc-cons (stlc-val->stlc-term stlc-unit) (stlc-cons (stlc-val->stlc-term stlc-unit)