From f0dce3bf92993f474bcdc7fcfecf757c262c807a Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 12 Jan 2016 19:27:47 -0500 Subject: [PATCH] Fixed syntax-class of non-terminal definitions Previously, syntax class would accept definitions for which I could not generate inductive constructors. Changed the syntax class to rule these out. --- cur-lib/cur/curnel/redex-lang.rkt | 7 +-- cur-lib/cur/olly.rkt | 88 ++++++++++++++++++------------- 2 files changed, 51 insertions(+), 44 deletions(-) diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt index f4c9005..a66a954 100644 --- a/cur-lib/cur/curnel/redex-lang.rkt +++ b/cur-lib/cur/curnel/redex-lang.rkt @@ -61,7 +61,6 @@ cur->datum cur-expand type-infer/syn - type-infer/syn! type-check/syn? normalize/syn step/syn @@ -185,7 +184,7 @@ [(#%app e1 e2) (term (,(cur->datum #'e1) ,(cur->datum #'e2)))])))) (unless (or (inner-expand?) (type-infer/term reified-term)) - (printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma)) + #;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma)) (raise-syntax-error 'cur "term is ill-typed:" reified-term syn)) reified-term) @@ -247,10 +246,6 @@ (let ([t (type-infer/term (eval-cur syn))]) (and t (datum->cur syn t))))) - (define (type-infer/syn! . ls) - (let ([x (apply type-infer/syn ls)]) - (or x (begin (displayln (delta)) #f)))) - (define (type-check/syn? syn type) (type-check/term? (eval-cur syn) (eval-cur type))) diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt index 2155bc4..f272538 100644 --- a/cur-lib/cur/olly.rkt +++ b/cur-lib/cur/olly.rkt @@ -128,56 +128,68 @@ #:fail-unless (dict-has-key? (mv-map) (attribute sym)) #f #:attr type (dict-ref (mv-map) (attribute sym)))) - ;; A expression is parameterized by the name of the non-terminal to + ;; A terminal is a idnetifiers that is not a meta-variable. A terminal will always represent a constructor. + (define-syntax-class (terminal lang-name) + (pattern + x:id + #:attr sym (syntax->datum #'x) + #:fail-when (dict-has-key? (mv-map) (attribute sym)) #f + #:attr constructor-name + (format-id #'x "~a-~a" lang-name #'x))) + + ;; A nested-expression can appear as the argument to a terminal in + ;; an expression, or as a sub-expression in a nested-expression. + ;; Each nested-expression export args, a list of types the + ;; nested-expression represents and the list of types the non-terminal's + ;; constructor expects in this case. + (define-syntax-class (nested-expression non-terminal-type lang-name) + ;; A meta-variable is a nested-expression + (pattern + e:meta-variable + #:attr args + (list #'e.type)) + + ;; An identifier is a nested-expression, but is treated as syntax + (pattern + x:id + #:attr args + '()) + + ;; A nested-expression applied to other nested expressions is a nested-expression + (pattern + ((~var h (nested-expression non-terminal-type lang-name)) + (~var t (nested-expression non-terminal-type lang-name)) ...) + #:attr args + (for/fold ([ls (attribute h.args)]) + ([args (attribute t.args)]) + (append ls args)))) + + ;; 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 ;; their types. - ;; Each expression exports a decl-context and arg-context attribute. - ;; In decl-context, a expression generates a constructor - ;; declaration for an inductive type. - ;; In arg-context, a expression generates the list of types - ;; indicated by the expression; e.g., in the definition of - ;; stlc-term, the expression v, representing a meta-variable for - ;; stlc-val, generates - ;; (stlc-val->stlc-term : (-> stlc-val stlc-term)) - ;; in decl-context, and - ;; (stlc-val) - ;; in arg-context + ;; Each expression exports a constr-decl, which declares a + ;; constructor for the non-terminal type. (define-syntax-class (expression non-terminal-type lang-name) ;; A meta-variable is a valid expression. - ;; Generates a conversion constructor in decl-context, and the type of + ;; Generates a conversion constructor in constr-decl, and the type of (pattern e:meta-variable #:attr constructor-name (format-id #'e "~a->~a" #'e.type non-terminal-type) - #:attr arg-context - (list #'e.type) - #:attr decl-context - #`(constructor-name : (-> #,@(attribute arg-context) #,non-terminal-type))) + #:attr constr-decl + #`(constructor-name : (-> e.type #,non-terminal-type))) ;; An identifier is a valid expression, generating a base constructor. (pattern - x:id - #:attr constructor-name - (format-id #'x "~a-~a" lang-name #'x) - ;; Cannot appear in arg-context - #:attr arg-context - '() - #:attr decl-context - #`(constructor-name : #,non-terminal-type)) + (~var x (terminal lang-name)) + #:attr constr-decl + #`(x.constructor-name : #,non-terminal-type)) + ;; A terminal applied to a nested-expression is a valid expression. (pattern - ((~var x (expression non-terminal-type lang-name)) (~var c (expression non-terminal-type lang-name)) ...) - ;; TODO: Should be pattern below, but this simplifies defs as expression-args is mostly a expression. Related to arg-context vs decl-context - ;; (x:id (~var c (expression-args non-terminal-type lang-name)) ...) - #:attr constructor-name - (attribute x.constructor-name) - #:attr arg-context - ;; Flatten nested arg-contexts - (for/fold ([ls (attribute x.arg-context)]) - ([e (attribute c.arg-context)]) - (append ls e)) - #:attr decl-context - #`(constructor-name : (-> #,@(attribute arg-context) #,non-terminal-type)))) + ((~var x (terminal lang-name)) . (~var c (nested-expression non-terminal-type lang-name))) + #:attr constr-decl + #`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type)))) ;; Syntax class non-terminal-def is parameterized by a language name ;; to the inductive types representing their non-terminal. @@ -197,7 +209,7 @@ (~var c (expression (attribute nt-type) lang-name)) ...) ;; Generates the inductive data type for this non-terminal definition. #:attr def - #`(data nt-type : Type c.decl-context ...)))) + #`(data nt-type : Type c.constr-decl ...)))) ;; TODO: For better error messages, add context ;; TODO: Extend define-language with syntax such as ....