More quasisyntax/loc for better error messages

Fixed up some of the design and started testing.

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

@@ -58,13 +58,41 @@
    (all-from-out syntax/parse)
    (all-from-out racket)
    (all-from-out racket/syntax)
-    cur->datum
+   raise-curnel-type-error
-    cur-expand
+   raise-curnel-syntax-error
-    type-infer/syn
+   cur->datum
-    type-check/syn?
+   cur-expand
-    normalize/syn
+   type-infer/syn
-    step/syn
+   type-check/syn?
-    cur-equal?))
+   normalize/syn
+   step/syn
+   cur-equal?))
+
+;; Exceptions
+(begin-for-syntax
+  (provide
+   (struct-out exn:cur)
+   (struct-out exn:cur:curnel)
+   (struct-out exn:cur:curnel:type)
+   (struct-out exn:cur:curnel:syntax))
+  (define-struct (exn:cur exn) () #:transparent)
+  (define-struct (exn:cur:curnel exn:cur) () #:transparent)
+  (define-struct (exn:cur:curnel:type exn:cur) () #:transparent)
+  (define-struct (exn:cur:curnel:syntax exn:cur) () #:transparent)
+
+  (define (raise-curnel-type-error name v . other)
+    (raise
+     (make-exn:cur:curnel:type
+      (for/fold ([msg (format "~a: Cur type error;~n  Typing judgment did not hold in Curnel~n    term: ~a" name v)])
+                ([t other])
+        (format "~a~n   additional context: ~a" msg t))
+      (current-continuation-marks))))
+
+  (define (raise-curnel-syntax-error name v [more ""])
+    (raise
+     (make-exn:cur:curnel:syntax
+      (format "~a: Cur syntax error;~n  Term is invalid Curnel syntax;~a~n    term: ~a" name more v)
+      (current-continuation-marks)))))
 
 (begin-for-syntax
   ;; TODO: Gamma and Delta seem to get reset inside a module+
@@ -73,7 +101,7 @@
       (term ∅)
       (lambda (x)
         (unless (Γ? x)
-          (error 'core-error "We built a bad term environment ~s" x))
+          (raise-curnel-syntax-error 'term-environment "term is not a well-formed Γ"))
         x)))
 
   (define delta
@@ -81,7 +109,7 @@
       (term ∅)
       (lambda (x)
         (unless (Δ? x)
-          (error 'core-error "We built a bad inductive declaration ~s" x))
+          (raise-curnel-syntax-error 'inductive-delcaration x "term is not a well-formed Δ"))
         x)))
 
   ;; These should be provided by core, so details of envs can be hidden.
@@ -118,7 +146,7 @@
      (list null null)
      (lambda (x)
        (unless (subst? x)
-           (error 'core-error "We build a bad subst ~s" x))
+         (raise-curnel-syntax-error 'top-level-bindings x))
        x)))
 
   (define (add-binding/term! x t)
@@ -156,8 +184,6 @@
   (define (cur->datum syn)
     ;; Main loop; avoid type
     (define reified-term
-      ;; TODO: This results in less good error messages. Add an
-      ;; algorithm to find the smallest ill-typed term.
       (parameterize ([inner-expand? #t])
         (let cur->datum ([syn syn])
           (syntax-parse (core-expand syn)
@@ -185,7 +211,7 @@
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
     (unless (or (inner-expand?) (type-infer/term reified-term))
       #;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
-      (raise-syntax-error 'cur "term is ill-typed:" reified-term syn))
+      (raise-curnel-type-error 'cur->datum reified-term syn))
     reified-term)
 
   (define (datum->cur syn t)
@@ -223,11 +249,19 @@
       (term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
 
   ;; Reflection tools
+  ;; TODO: Reflection tools should catch internal errors, e.g., from eval-cur et al. to
+  ;; ensure users can provide better error messages. But should not catch errors caused by user macros.
 
-  (define (normalize/syn syn)
+  (define (local-env->gamma env)
-    (datum->cur
+    (for/fold ([gamma (gamma)])
-      syn
+              ([(x t) (in-dict env)])
-      (eval-cur syn)))
+      (extend-Γ/syn (thunk gamma) x t)))
+
+  (define (normalize/syn syn  #:local-env [env '()])
+    (parameterize ([gamma (local-env->gamma env)])
+      (datum->cur
+       syn
+       (eval-cur syn))))
 
   (define (step/syn syn)
     (datum->cur
@@ -239,26 +273,28 @@
     (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
 
   ;; TODO: Document local-env
-  (define (type-infer/syn syn #:local-env [env '()])
+  (define (type-infer/syn #:local-env [env '()] syn)
-    (parameterize ([gamma (for/fold ([gamma (gamma)])
+    (parameterize ([gamma (local-env->gamma env)])
-                                    ([(x t) (in-dict env)])
+      (with-handlers ([exn:cur:curnel:type? (lambda _ #f)])
-                            (extend-Γ/syn (thunk gamma) x t))])
+        (let ([t (type-infer/term (eval-cur syn))])
-      (let ([t (type-infer/term (eval-cur syn))])
+        (and t (datum->cur syn t))))))
-        (and t (datum->cur syn t)))))
 
   (define (type-check/syn? syn type)
-    (type-check/term? (eval-cur syn) (eval-cur type)))
+    (with-handlers ([exn:cur:curnel:type? (lambda _ #f)])
+      (type-check/term? (eval-cur syn) (eval-cur type))))
 
   ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
   ;; expanded until expansion reaches a Curnel form, or one of the
   ;; identifiers in ls.
-  (define (cur-expand syn . ls)
+  ;; TODO: Holy crap boilerplate
-    (disarm
+  (define (cur-expand syn #:local-env [env '()] . ls)
-      (local-expand
+    (parameterize ([gamma (local-env->gamma env)])
+      (disarm
+       (local-expand
         syn
         'expression
         (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top))
-                ls)))))
+                ls))))))
 
 ;; -----------------------------------------------------------------
 ;; Require/provide macros

cur-lib/cur/olly.rkt

@@ -43,57 +43,72 @@
   (define (cur->coq syn)
     (parameterize ([coq-defns ""])
       (define output
-        (let cur->coq ([syn syn])
+        (let cur->coq ([syn syn]
-          (syntax-parse (cur-expand syn #'define #'begin)
+                       [local-env (make-immutable-hash)])
+          (syntax-parse (cur-expand #:local-env local-env syn #'define #'begin)
             ;; TODO: Need to add these to a literal set and export it
             ;; Or, maybe overwrite syntax-parse
             #:literals (real-lambda real-forall data real-app real-elim define begin Type)
             [(begin e ...)
              (for/fold ([str ""])
                        ([e (syntax->list #'(e ...))])
-               (format "~a~n" (cur->coq e)))]
+               (format "~a~n" (cur->coq e local-env)))]
             [(define name:id body)
              (begin
                (coq-lift-top-level
                 (format "Definition ~a := ~a.~n"
-                        (cur->coq #'name)
+                        (cur->coq #'name local-env)
-                        (cur->coq #'body)))
+                        (cur->coq #'body local-env)))
                "")]
             [(define (name:id (x:id : t) ...) body)
              (begin
+               (define-values (args body-local-env)
+                 (for/fold ([str ""]
+                            [local-env local-env])
+                           ([n (syntax->list #'(x ...))]
+                            [t (syntax->list #'(t ...))])
+                   (values
+                    (format
+                     "~a(~a : ~a) "
+                     str
+                     (cur->coq n local-env)
+                     (cur->coq t local-env))
+                    (dict-set local-env n t))))
                (coq-lift-top-level
                 (format "Function ~a ~a := ~a.~n"
-                        (cur->coq #'name)
+                        (cur->coq #'name local-env)
-                        (for/fold ([str ""])
+                        args
-                                  ([n (syntax->list #'(x ...))]
+                        (cur->coq #'body body-local-env)))
-                                   [t (syntax->list #'(t ...))])
-                          (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
-                        (cur->coq #'body)))
                "")]
             [(real-lambda ~! (x:id (~datum :) t) body:expr)
-             (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
+             (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (cur->coq #'t local-env)
-                     (cur->coq #'body))]
+                     (cur->coq #'body (dict-set local-env #'x #'t)))]
             [(real-forall ~! (x:id (~datum :) t) body:expr)
-             (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
+             (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t local-env)
-                     (cur->coq #'body))]
+                     (cur->coq #'body (dict-set local-env #'x #'t)))]
             [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
              (begin
                (coq-lift-top-level
                 (format "Inductive ~a : ~a :=~a."
                         (sanitize-id (format "~a" (syntax-e #'n)))
-                        (cur->coq #'t)
+                        (cur->coq #'t local-env)
-                        (for/fold ([strs ""])
+                        (call-with-values
-                                  ([clause (syntax->list #'((x* : t*) ...))])
+                         (thunk
-                          (syntax-parse clause
+                          (for/fold ([strs ""]
-                            [(x (~datum :) t)
+                                     [local-env (dict-set local-env #'n #'t)])
-                             (format "~a~n| ~a : ~a" strs (syntax-e #'x)
+                                    ([x (attribute x*)]
-                                     (cur->coq #'t))]))))
+                                     [t (attribute t*)])
+                            (values
+                             (format "~a~n| ~a : ~a" strs (syntax-e x)
+                                     (cur->coq t local-env))
+                             (dict-set local-env x t))))
+                         (lambda (x y) x))))
                "")]
             [(Type i) "Type"]
             [(real-elim var t)
-             (format "~a_rect" (cur->coq #'var))]
+             (format "~a_rect" (cur->coq #'var local-env))]
             [(real-app e1 e2)
-             (format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
+             (format "(~a ~a)" (cur->coq #'e1 local-env) (cur->coq #'e2 local-env))]
             [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
       (format
        "~a~a"
@@ -191,6 +206,7 @@
               lab:rule-name
               (~var t (conclusion name indices (attribute lab))))
              #:with constr-decl
+             ;; TODO: quasisyntax/loc
              #'(lab : (-> h ... (t.name t.arg ...)))
              ;; TODO: convert meta-vars such as e1 to e_1
              #:attr latex
@@ -273,7 +289,8 @@
      #: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)))
+     (quasisyntax/loc #'x
+       #,(format-id #'x "~a-~a" (lang-name) #'x))))
 
   ;; A terminal-args can appear as the argument to a terminal in
   ;; an expression, or as a sub-expression in a terminal-args.
@@ -334,9 +351,9 @@
     (pattern
      e:meta-variable
      #:attr constructor-name
-     (format-id #'e "~a->~a" #'e.type non-terminal-type)
+     (quasisyntax/loc #'e #,(format-id #'e "~a->~a" #'e.type non-terminal-type))
      #:attr constr-decl
-     #`(constructor-name : (-> e.type #,non-terminal-type))
+     (quasisyntax/loc #'e (constructor-name : (-> e.type #,non-terminal-type)))
      #:attr latex
      (format "~a" (syntax-e #'e)))
 
@@ -344,7 +361,7 @@
     (pattern
      x:terminal
      #:attr constr-decl
-     #`(x.constructor-name : #,non-terminal-type)
+     (quasisyntax/loc #'x (x.constructor-name : #,non-terminal-type))
      #:attr latex
      (format "~a" (syntax-e #'x)))
 
@@ -352,7 +369,7 @@
     (pattern
      (x:terminal . (~var c (terminal-args non-terminal-type)))
      #:attr constr-decl
-     #`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))
+     (quasisyntax/loc #'x (x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type)))
      #:attr latex
      (format "(~a ~a)" (syntax-e #'x) (attribute c.latex))))
 
@@ -363,7 +380,7 @@
       (~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)])
+      (~bind [nt-type (quasisyntax/loc #'name #,(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.
@@ -372,7 +389,7 @@
       (~var c (expression (attribute nt-type))) ...)
      ;; Generates the inductive data type for this non-terminal definition.
      #:attr def
-     #`(data nt-type : Type c.constr-decl ...)
+     (quasisyntax/loc #'name (data nt-type : Type c.constr-decl ...))
      #:attr latex
      (format
       "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
@@ -420,7 +437,7 @@
            (dict-set! (mv-map) (syntax-e x) #'Nat)))])
     (syntax-parse #'non-terminal-defs
       [(def:non-terminal-def ...)
-       (let ([output #`(begin def.def ...)])
+       (let ([output (quasisyntax/loc #'name (begin def.def ...))])
          (when (attribute latex-file)
            (with-output-to-file (syntax-e #'latex-file)
              (thunk (typeset-bnf (attribute def.latex)))

cur-lib/cur/stdlib/sugar.rkt

@@ -31,31 +31,115 @@
     [lambda real-lambda]
     [define real-define]))
 
+;; Exceptions and such
 (begin-for-syntax
-  (define-syntax-class result-type
+  (define-struct (exn:cur:type exn:cur) () #:transparent)
-    (pattern type:expr))
 
+  (define (deduce-type-infer-error-hints term)
+    (syntax-parse term
+      [x:id
+       "; Seems to be an unbound variable"]
+      [_ "could not infer a type."]))
+
+  (define (cur-type-infer-error-msg name v . other)
+    (format
+     "~aCur type error;~n  Could not infer any type~a~n    term: ~a~a"
+     (if name (format "~a:" name) "")
+     (deduce-type-infer-error-hints v)
+     v
+     (for/fold ([str ""])
+               ([other other])
+       (format "~a~n    context: ~a" str other))))
+
+  (define (raise-cur-type-infer-error . all)
+    (raise
+     (make-exn:cur:type
+      (apply cur-type-infer-error-msg all)
+      (current-continuation-marks)))))
+
+(begin-for-syntax
+  #| TODO
+   | Design of "typed" macros for Cur.
+   |
+   | We can use syntax classes to emulate typed macros. The syntax
+   | class calls the type-checker to ensure the term parsed term is
+   | well-typed. This *must* not expand the the matched term as a side-effect.
+   | Unfortunately, to handle binding, patterns that have variables
+   | must thread binding information through while parsing in syntax
+   | parse.
+   | This can be handled by delaying the expansion and syntax-class
+   | check until the term is under the binder; see delay-check macros.
+   |
+   |#
+  (define-syntax-class cur-syntax
+    (pattern e:expr))
+
+  (define-syntax-class well-typed-cur-term
+    (pattern
+     e:cur-syntax
+     #:attr type (type-infer/syn #'e)
+     #:fail-unless (attribute type)
+     (cur-type-infer-error-msg #f #'e))))
+
+;; For delaying a type-check until the term is under a binder
+;; NB: This is an impressively awesome solution..... need to write something about it.
+(define-syntax (delayed-check syn)
+  (syntax-parse syn
+    [(_ e:well-typed-cur-term) #'e]))
+
+(begin-for-syntax
   (define-syntax-class parameter-declaration
-    (pattern (name:id (~datum :) type:expr))
+    #:commit
+    (pattern
+     (name:id (~datum :) ~! type:cur-syntax))
 
     (pattern
-     type:expr
+     type:cur-syntax
-     #:attr name (format-id #'type "~a" (gensym 'anon-parameter)))))
+     #:attr name (format-id #'type "~a" (gensym 'anon-parameter))))
+
+  (define-syntax-class well-typed-parameter-declaration
+    #:commit
+    (pattern
+     e:parameter-declaration
+     #:attr type #'(delayed-check e.type)
+     #:attr name #'e.name))
+
+  (define-syntax-class well-typed-argument-declaration
+    #:commit
+    (pattern
+     ;; TODO: Copy pasta from parameter-declaration
+     (name:id (~datum :) ~! _type:cur-syntax)
+     #:attr type #'(delayed-check _type)))
+
+  (define-syntax-class well-typed-parameter-list
+    (pattern
+     (d:well-typed-parameter-declaration ...+)
+     #:attr names (attribute d.name)
+     #:attr types (attribute d.type)))
+
+  (define-syntax-class well-typed-argument-list
+    (pattern
+     (d:well-typed-argument-declaration ...+)
+     #:attr names (attribute d.name)
+     #:attr types (attribute d.type))))
 
 ;; A multi-arity function type; takes parameter declaration of either
 ;; a binding (name : type), or type whose name is generated.
 ;; E.g.
 ;; (-> (A : Type) A A)
+
 (define-syntax (-> syn)
   (syntax-parse syn
-    [(_ d:parameter-declaration ...+ result:result-type)
+    [(_ d:parameter-declaration ...+ e:cur-syntax)
+     #:with ds #'(d ...)
+     #:declare ds well-typed-parameter-list
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
                 (forall (#,name : #,type) #,r)))
-            #'result
+            #'(delayed-check e)
-            (attribute d)
+            (syntax->list (attribute ds))
-            (attribute d.name)
+            (attribute ds.names)
-            (attribute d.type))]))
+            (attribute ds.types))]))
 
 ;; TODO: Add forall macro that allows specifying *names*, with types
 ;; inferred. unlike -> which require types but not names
@@ -64,35 +148,65 @@
 
 ;; TODO: Allows argument-declarations to have types inferred, similar
 ;; to above TODO forall
-(begin-for-syntax
-  ;; eta-expand syntax-class for error messages
-  (define-syntax-class argument-declaration
-    (pattern
-     e:parameter-declaration
-     #:attr name #'e.name
-     #:attr type #'e.type)))
 (define-syntax (lambda syn)
   (syntax-parse syn
-    [(_ d:argument-declaration ...+ body:expr)
+    [(_ d:parameter-declaration ...+ e:cur-syntax)
+     #:with ds #'(d ...)
+     #:declare ds well-typed-argument-list
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
                 (real-lambda (#,name : #,type) #,r)))
-            #'body
+            #'(delayed-check e)
-            (attribute d)
+            (syntax->list (attribute ds))
-            (attribute d.name)
+            (attribute ds.names)
-            (attribute d.type))]))
+            (attribute ds.types))]))
+
+(begin-for-syntax
+  (define-syntax-class forall-type
+    (pattern
+     ((~literal forall) ~! (parameter-name:id (~datum :) parameter-type) body)))
+
+  (define-syntax-class well-typed-cur-function
+    (pattern
+     e:well-typed-cur-term
+     #:attr type (attribute e.type)
+     #:fail-unless (syntax-parse (attribute e.type)
+                     [t:forall-type #t]
+                     [_ #f])
+     (format
+      "Expected ~a to be a function, but inferred type ~a"
+      (syntax->datum #'e)
+      (syntax->datum (attribute e.type))))))
 
-;; TODO: This makes for really bad error messages when an identifier is undefined.
 (define-syntax (#%app syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ e)
+    [(_ f:well-typed-cur-function ~! e:well-typed-cur-term ...+)
-     (quasisyntax/loc syn e)]
+     ;; Have to thread each argument through, to handle dependency.
-    [(_ e1 e2)
+     (for/fold ([type (attribute f.type)])
-     (quasisyntax/loc syn
+               ([arg (attribute e)]
-       (real-app e1 e2))]
+                [inferred-type (attribute e.type)])
-    [(_ e1 e2 e3 ...)
+       (define/syntax-parse expected:forall-type type)
-     (quasisyntax/loc syn
+       (define expected-type (attribute expected.parameter-type))
-       (#%app (#%app e1 e2) e3 ...))]))
+       (unless (type-check/syn? arg expected-type)
+         (raise-syntax-error
+          '#%app
+          (format
+           "Expected ~a to have type ~a, but inferred type ~a."
+           (syntax->datum arg)
+           (syntax->datum expected-type)
+           (syntax->datum inferred-type))
+          syn
+          arg))
+       (normalize/syn
+        #`(real-app
+           (real-lambda (expected.parameter-name : expected.parameter-type)
+                        expected.body)
+           #,arg)))
+     (for/fold ([app (quasisyntax/loc syn
+                       (real-app f #,(first (attribute e))))])
+               ([arg (rest (attribute e))])
+       (quasisyntax/loc arg
+         (real-app #,app #,arg)))]))
 
 (define-syntax define-type
   (syntax-rules ()
@@ -111,13 +225,22 @@
      (quasisyntax/loc syn
        (real-define id body))]))
 
-(define-syntax-rule (elim t1 t2 e ...)
+(define-syntax (elim syn)
-  ((real-elim t1 t2) e ...))
+  (syntax-parse syn
+    [(_ t1 t2 e ...)
+     (maybe-cur-apply
+      #`(real-elim t1 t2)
+      (attribute e))]))
 
 ;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
 (begin-for-syntax
   (define ih-dict (make-hash))
 
+  (define (maybe-cur-apply f ls)
+    (if (null? ls)
+        f
+        #`(#,f #,@ls)))
+
   (define-syntax-class curried-application
     (pattern
      ((~literal real-app) name:id e:expr)
@@ -140,6 +263,10 @@
      #'x
      #:attr indices
      '()
+     #:attr names
+     '()
+     #:attr types
+     '()
      #:attr decls
      (list #`(#,(gensym 'anon-discriminant) : x))
      #:attr abstract-indices
@@ -181,14 +308,20 @@
        ;; NB: unhygenic
        ;; Normalize at compile-time, for efficiency at run-time
        (normalize/syn
-        #`((lambda
+        #:local-env
-              ;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed
+        (for/fold ([d (make-immutable-hash)])
-              ;; works only for simple type familes and simply matches on them
+                  ([name (attribute names)]
-             #,@(for/list ([name (attribute indices)]
+                   [type (attribute types)])
-                           [type (attribute types)])
+          (dict-set d name type))
-                 #`(#,name : #,type))
+        (maybe-cur-apply
-            #,return)
+         #`(lambda
-          #,@(attribute names))))))
+               ;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed
+               ;; works only for simple type familes and simply matches on them
+               #,@(for/list ([name (attribute indices)]
+                             [type (attribute types)])
+                    #`(#,name : #,type))
+             #,return)
+         (attribute names))))))
 
   ;; todo: Support just names, inferring types
   (define-syntax-class match-declaration
@@ -231,19 +364,26 @@
      #:attr decls
      ;; Infer the inductive hypotheses, add them to the pattern decls
      ;; and update the dictionarty for the recur form
-     (for/fold ([decls (attribute d.decls)])
+     (call-with-values
-               ([type-syn (attribute d.types)]
+      (thunk
-                [name-syn (attribute d.names)]
+       (for/fold ([decls (attribute d.decls)]
-                [src (attribute d.decls)]
+                  [local-env (attribute d.local-env)])
-                ;; NB: Non-hygenic
+                 ([type-syn (attribute d.types)]
-                ;; BUG TODO: This fails when D is an inductive applied to arguments...
+                  [name-syn (attribute d.names)]
-                #:when (cur-equal? type-syn D))
+                  [src (attribute d.decls)]
-       (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn))
+                  ;; NB: Non-hygenic
-       (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))]
+                  ;; BUG TODO: This fails when D is an inductive applied to arguments...
-             ;; Normalize at compile-time, for efficiency at run-time
+                  #:when (cur-equal? type-syn D))
-             [ih-type (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))])
+         (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn))
-         (dict-set! ih-dict (syntax->datum name-syn) ih-name)
+         (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))]
-         (append decls (list #`(#,ih-name : #,ih-type)))))))
+               ;; Normalize at compile-time, for efficiency at run-time
+               [ih-type (normalize/syn #:local-env local-env
+                                       (maybe-cur-apply motive
+                                                        (append (attribute type.indices) (list name-syn))))])
+           (dict-set! ih-dict (syntax->datum name-syn) ih-name)
+           (values (append decls (list #`(#,ih-name : #,ih-type)))
+                   (dict-set local-env ih-name ih-type)))))
+      (lambda (x y) x))))
 
   (define-syntax-class (match-preclause maybe-return-type)
     (pattern
@@ -282,6 +422,8 @@
           (syntax->datum #'id))
          syn)))]))
 
+;; TODO: Better error messages; follow pattern of -> and lambda etc to first parse, then type-check.
+;; TODO: Deprecate #:local-env
 (define-syntax (match syn)
   (syntax-parse syn
     [(_ d

cur-test/cur/tests/olly.rkt

@@ -6,6 +6,9 @@
 (require
  rackunit
  cur/stdlib/sugar
+ cur/stdlib/nat
+ cur/stdlib/bool
+ cur/stdlib/prop
  cur/olly)
 
 (begin-for-syntax
@@ -30,28 +33,28 @@
    "(forall .+ : Type, Type)"
    (cur->coq #'(-> Type Type)))
   (let ([t (cur->coq
-            #'(define-relation (meow gamma term type)
+            #'(define-relation (meow Nat Bool Nat)
-                [(g : gamma) (e : term) (t : type)
+                [(n : Nat) (b : Bool) (m : Nat)
                  --------------- T-Bla
-                 (meow g e t)]))])
+                 (meow n b m)]))])
     (check-regexp-match
-     "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
+     "Inductive meow : \\(forall .+ : Nat, \\(forall .+ : Bool, \\(forall .+ : Nat, Type\\)\\)\\) :="
      (first (string-split t "\n")))
     (check-regexp-match
-     "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
+     "\\| T-Bla : \\(forall n : Nat, \\(forall b : Bool, \\(forall m : Nat, \\(\\(\\(meow n\\) b\\) m\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
   (let ([t (cur->coq
-            #'(elim nat Type (lambda (x : nat) nat) z
+            #'(elim Nat Type (lambda (x : Nat) Nat) z
-                    (lambda (x : nat) (ih-x : nat) ih-x)
+                    (lambda (x : Nat) (ih-x : Nat) ih-x)
-                    e))])
+                    z))])
     (check-regexp-match
-     "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+     "\\(\\(\\(\\(Nat_rect \\(fun x : Nat => Nat\\)\\) z\\) \\(fun x : Nat => \\(fun ih_x : Nat => ih_x\\)\\)\\) z\\)"
      t))
   (check-regexp-match
-   "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
+   "Definition thm_plus_commutes := \\(forall n : Nat, \\(forall m : Nat, \\(\\(\\(== Nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
    (cur->coq
-    #'(define thm:plus-commutes (forall (n : nat) (m : nat)
+    #'(define thm:plus-commutes (forall (n : Nat) (m : Nat)
-                                        (== nat (plus n m) (plus m n))))))
+                                        (== Nat (plus n m) (plus m n))))))
   (check-regexp-match
-   "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
+   "Function add1 \\(n : Nat\\)  := \\(s n\\).\n"
-   (cur->coq #'(define (add1 (n : nat)) (s n)))))
+   (cur->coq #'(define (add1 (n : Nat)) (s n)))))