Rewrote define-language

Working on #9 and fixing issues in Olly

cur-lib/cur/curnel/redex-lang.rkt

@@ -61,6 +61,7 @@
     cur->datum
     cur-expand
     type-infer/syn
+    type-infer/syn!
     type-check/syn?
     normalize/syn
     step/syn
@@ -184,7 +185,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)
 
@@ -246,6 +247,10 @@
       (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)))
 

cur-lib/cur/olly.rkt

@@ -19,15 +19,13 @@
   (for-syntax
    coq-defns
    output-latex-bnf
-   output-coq
+   output-coq))
-   new-name
-   fresh-name))
 
 (begin-for-syntax
   (define-syntax-class dash
-    (pattern x:id
+    (pattern
-             #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
+     x:id
-             "Invalid dash"))
+     #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x))) "Invalid dash"))
 
   (define-syntax-class decl (pattern (x:id (~datum :) t:id)))
 
@@ -84,81 +82,15 @@
                    #'())
                #,output))]))
 
-(begin-for-syntax
+;; ------------------------------------
-  (require racket/syntax)
+;; define-language
-  (define (new-name name . id*)
-    (apply format-id name (for/fold ([str "~a"])
-                                    ([_ id*])
-                            (string-append str "-~a")) name (map syntax->datum id*)))
-
-  (define (fresh-name id)
-    (datum->syntax id (gensym (syntax->datum id)))))
-
-;; TODO: Oh, this is a mess. Rewrite it.
-(begin-for-syntax
-  (define lang-name (make-parameter #'name))
-  (define nts (make-parameter (make-immutable-hash)))
-
-  (define-syntax-class nt
-    (pattern e:id #:fail-unless (hash-has-key? (nts) (syntax->datum #'e)) #f
-             #:attr name (hash-ref (nts) (syntax->datum #'e))
-             #:attr type (hash-ref (nts) (syntax->datum #'e))))
-
-  (define (flatten-args arg arg*)
-    (for/fold ([ls (syntax->list arg)])
-              ([e (syntax->list arg*)])
-      (append ls (syntax->list e))))
-
-  (define-syntax-class (right-clause type)
-    #;(pattern (~datum var)
-             #:attr clause-context #`(#,(new-name (lang-name) #'var) :
-                                      (-> #,(hash-ref (nts) 'var) #,(hash-ref (nts) type)))
-             #:attr name #'var
-             #:attr arg-context #'(var))
-    (pattern e:nt
-             #:attr clause-context #`(#,(new-name #'e.name #'->
-                                                  (hash-ref (nts) type)) :
-                                      (-> e.type #,(hash-ref (nts) type)))
-             #:attr name (fresh-name #'e.name)
-             #:attr arg-context #'(e.type))
-    (pattern x:id
-             #:attr clause-context #`(#,(new-name (lang-name) #'x) :
-                                      #,(hash-ref (nts) type))
-             #:attr name (new-name (lang-name) #'x)
-             #:attr arg-context #'())
-    (pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
-             #:attr name (fresh-name #'e.name)
-             #:attr clause-context #`(e.name : (-> #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
-                                                    #,(hash-ref (nts) type)))
-             #:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
-
-  (define-syntax-class (right type)
-    (pattern ((~var r (right-clause type)) ...)
-             #:attr clause #'(r.clause-context ...)))
-
-  #;(define-syntax-class left
-    (pattern (type:id (nt*:id ...+))
-             #:do ))
-
-  (define-syntax-class nt-clauses
-    (pattern ((type:id (nt*:id ...+)
-              (~do (nts (for/fold ([ht (nts)])
-                                  ([nt (syntax->datum #'(type nt* ...))])
-                          (hash-set ht nt (new-name (lang-name) #'type)))))
-              (~datum ::=)
-              . (~var rhs* (right (syntax->datum #'type)))) ...)
-             #:with defs (with-syntax ([(name* ...)
-                                        (map (λ (x) (hash-ref (nts) x))
-                                             (syntax->datum #'(type ...)))])
-                           #`((data name* : Type . rhs*.clause)
-                              ...)))))
 
 (begin-for-syntax
   ;; TODO: More clever use of syntax-parse would enable something akin to what
   ;; define-relation is doing---having attributes that contain the latex
   ;; code for each clause.
   ;; TODO: convert meta-vars such as e1 to e_1
-  (define (output-latex-bnf vars clauses)
+  (define (output-latex-bnf clauses)
     (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
       (for/fold ([str ""])
                 ([clause (syntax->list clauses)])
@@ -179,35 +111,121 @@
                        (format "~a~a \\bnfalt " str expr))
                      " \\bnfalt "
                      #:left? #f))]))))
-  (define (generate-latex-bnf file-name vars clauses)
+  (define (generate-latex-bnf file-name clauses)
     (with-output-to-file file-name
-      (thunk (printf (output-latex-bnf vars clauses)))
+      (thunk (printf (output-latex-bnf clauses)))
       #:exists 'append)))
 
-;; TODO: For better error messages, add context, rename some of these patterns. e.g.
+(begin-for-syntax
-;;    (type (meta-vars) ::= ?? )
+  ;; A mutable map from non-terminal meta-variables names to their types
+  (define mv-map (make-parameter #f))
+
+  ;; A meta-variable is any identifiers that belongs to the mv-map
+  (define-syntax-class meta-variable
+    (pattern
+     e:id
+     #:attr sym (syntax->datum #'e)
+     #: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
+  ;; 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
+  (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
+    (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)))
+
+    ;; 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))
+
+    (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))))
+
+  ;; Syntax class non-terminal-def is parameterized by a language name
+  ;; to the inductive types representing their non-terminal.
+  (define-syntax-class (non-terminal-def lang-name)
+    (pattern
+     (name:id
+      (meta-var:id ...+)
+      (~optional (~datum ::=))
+      ;; Create a name for the type of this non-terminal, from the
+      ;; language name and the non-terminal name.
+      (~bind [nt-type (format-id #'name "~a-~a" lang-name #'name)])
+      ;; Imperatively update the map from meta-variables to the
+      ;; nt-type, to be used when generating the types of the constructors
+      ;; for this and later non-terminal.
+      (~do (for ([mv (syntax->datum #'(meta-var ...))])
+             (dict-set! (mv-map) mv (attribute nt-type))))
+      (~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 ...))))
+
+;; TODO: For better error messages, add context
 ;; TODO: Extend define-language with syntax such as ....
 ;;   (term (e) ::= (e1 e2) ((lambda (x) e)
-;                           #:latex "(\\lambda ,x. ,e)"))
 (define-syntax (define-language syn)
-  (syntax-parse syn
+  (parameterize ([mv-map (make-hash)])
-    [(_ name:id (~do (lang-name #'name))
+    (syntax-parse syn
-        (~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
+      [(_ lang-name:id
-        (~optional (~seq #:vars (x*:id ...)
+          (~optional (~seq #:vars (x:id ...)))
-           (~do (nts (for/fold ([ht (nts)])
+          ;; Update the mv-map to include x -> Var for each x
-                               ([v (syntax->datum #'(x* ...))])
+          (~do (cond
-                       (hash-set ht v (hash-ref ht 'var)))))))
+                 [(attribute x) =>
-        (~optional (~seq #:output-coq coq-file:str))
+                  (lambda (xls)
-        (~optional (~seq #:output-latex latex-file:str))
+                    (for ([x xls])
-        . clause*:nt-clauses)
+                      (dict-set! (mv-map) (syntax-e x) #'Var)))]))
-     (let ([output #`(begin . clause*.defs)])
+          (~optional (~seq #:output-coq coq-file:str))
-       (when (attribute latex-file)
+          (~optional (~seq #:output-latex latex-file:str))
-         (generate-latex-bnf (syntax->datum #'latex-file) #'vars #'clause*))
+          (~var defs (non-terminal-def #'lang-name)) ...)
-       #`(begin
+       (let ([output #`(begin defs.def ...)])
-           #,@(if (attribute coq-file)
+         ;; TODO: Should do this via attributes
-                 #`((generate-coq #:file coq-file #:exists 'append #,output))
+         (when (attribute latex-file)
-                 #'())
+           (generate-latex-bnf (syntax->datum #'latex-file) #'(defs ...)))
-           #,output))]))
+         #`(begin
+             ;; TODO: generate-coq should also export a compile-time function.
+             #,@(if (attribute coq-file)
+                    #`((generate-coq #:file coq-file #:exists 'append #,output))
+                    #'())
+             #,output))])))
 
 (data Var : Type (avar : (-> Nat Var)))
 
@@ -227,6 +245,7 @@
   (define (coq-lift-top-level str)
     (coq-defns (format "~a~a~n" (coq-defns) str)))
   ;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
+  ;; TODO: Think the above TODO was fixed; consult git log
   (define (constructor-args syn)
     (syntax-parse (type-infer/syn syn)
       #:datum-literals (Π :)

cur-test/cur/tests/olly.rkt

@@ -9,36 +9,17 @@
  cur/olly)
 
 (begin-for-syntax
-  (require rackunit)
+  (require rackunit))
-  (define (check-id-equal? v1 v2)
-    (check-equal?
-     (syntax->datum v1)
-     (syntax->datum v2)))
-  (define (check-id-match? v1 v2)
-    (check-regexp-match
-     v1
-     (symbol->string (syntax->datum v2))))
-  (check-id-match?
-   #px"term\\d+"
-   (fresh-name #'term))
-  (check-id-equal?
-   #'stlc-lambda
-   (new-name #'stlc #'lambda))
-  (check-id-match?
-   #px"stlc-term\\d+"
-   (new-name #'stlc (fresh-name #'term))))
 
 (begin-for-syntax
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
-   (output-latex-bnf #'(x)
+   (output-latex-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
-                     #'((term (e) ::= (e1 e2) (lambda (x) e)))))
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
-   (output-latex-bnf #'(x)
+   (output-latex-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
-                     #'((type (A B C) ::= unit (* A B) (+ A C))))))
 
 (check-equal?
  (var-equal? (avar z) (avar z))

cur-test/cur/tests/stlc.rkt

@@ -36,20 +36,20 @@
   #: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)
    (== (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)
@@ -98,7 +98,7 @@
          (normalize/syn
            #`((lambda (x : stlc-term)
                       (stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
-             (Var-->-stlc-term (avar #,oldindex)))))]
+             (Var->stlc-term (avar #,oldindex)))))]
       [(quote (e1 e2))
        #`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))]
       [(let (x y) = e1 in e2)
@@ -108,14 +108,14 @@
          #`((lambda (x : stlc-term) (y : stlc-term)
               (stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
                    #,(stlc #'e2)))
-            (Var-->-stlc-term (avar #,x))
+            (Var->stlc-term (avar #,x))
-            (Var-->-stlc-term (avar #,y))))
+            (Var->stlc-term (avar #,y))))
        #`(let x  i #,(stlc #'e1))]
       [(e1 e2)
        #`(stlc-app #,(stlc #'e1) #,(stlc #'e2))]
-      [() #'(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)
        #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))]
       [(t1 -> t2)
@@ -128,15 +128,15 @@
 
 (check-equal?
  (begin-stlc (lambda (x : 1) x))
- (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
+ (stlc-lambda (avar z) stlc-unitty (Var->stlc-term (avar z))))
 (check-equal?
  (begin-stlc ((lambda (x : 1) x) ()))
- (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
+ (stlc-app (stlc-lambda (avar z) stlc-unitty (Var->stlc-term (avar z)))
-           (stlc-val-->-stlc-term stlc-unit)))
+           (stlc-val->stlc-term stlc-unit)))
 (check-equal?
  (begin-stlc '(() ()))
- (stlc-cons (stlc-val-->-stlc-term stlc-unit)
+ (stlc-cons (stlc-val->stlc-term stlc-unit)
-            (stlc-val-->-stlc-term stlc-unit)))
+            (stlc-val->stlc-term stlc-unit)))
 (check-equal?
  (begin-stlc #t)
- (stlc-val-->-stlc-term stlc-true))
+ (stlc-val->stlc-term stlc-true))