On this page:
define-language
define-relation
generate-coq
6.12

4 Olly: Ott-like LibrarY

 (require cur/olly) package: cur-lib
Olly provides syntax extensions for defining programming languages as inductive data. The library is inspired by OttTODO: Citation needed, which provides an language that resembles math notation for generating Coq definitions. The purpose of Olly is not to replace Ott, but to demonstrate how powerful syntactic meta-programming can bring features previously only provided by external tools into the language.

syntax

(define-language name
  maybe-vars
  maybe-output-coq
  maybe-output-latex
  (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
 
maybe-vars = 
  | #:vars (nt-metavar ...)
     
maybe-output-coq = 
  | #:output-coq coq-filename
     
maybe-output-latex = 
  | #:output-latex latex-filename
     
maybe-bnfdef = 
  | ::=
     
non-terminal-def = nt-metavar
  | terminal
  | (terminal terminal-args ...)
     
terminal-args = nt-metavar
  | literal
  | ()
  | (#:bind nt-metavar . terminal-args)
  | (terminal-args terminal-args ...)
Defines a new language by generating inductive definitions for each non-terminal nt-name, whose syntax is generated by non-terminal-def. Each non-terminal-def must either be a reference to a previously defined non-terminal using a nt-metavar, a terminal (an identifier), or a terminal applied to some terminal-args. The terminal-args are a limited grammar of s-expressions, which can reference previously defined nt-metavars to be treated as arguments, literal symbols to be treated as syntax, binding declarations, or a nested terminal-arg.

The inductive definitions are generated by generating a type for each nt-name whose name nt-type is generated by (format-id name "~a-~a" name nt-name) and whose constructors are generated by each non-terminal-def. For terminals, the constructor is a base constructor whose name is generated by (format-id name "~a-~a" name terminal). For nt-metavars, the constructor is a conversion constructor whose name is generated by (format-id name "~a->~a" nt-type nt-metavar-type) where nt-metavar-type is the name of the type generated for the nonterminal to which nt-metavars refers. For (terminal terminal-args ...), the constructor is a function that expects term of of the types generated by terminal-args ....

If #:vars is given, it should be a list of meta-variables that representing variables in the language. These variables are represented as De Bruijn indices, and uses of variables in the syntax are treated as type Nat. Binding positions in the syntax, represented by #:bind nt-metavar, are erased in converting to De Bruijn indices, although this may change if the representation of variables used by define-language changes.

If #:output-coq is given, it should be a string representing a filename. The form define-language will output Coq versions of the language definitions to the coq-filename, overwriting the file. Note well: this feature is very fragile right now, as the extractor descends under binders while expanding. If the Cur code being extracted uses reflection, these bindings may not be properly tracked resulting in unexpected type errors during extraction. This feature is also not well tested, so it may or may not produce well-formed Coq code.

If #:output-latex is given, it should be a string representing a filename. The form define-language will output Latex versions of the language definitions to the latex-filename, overwriting the file.

Example:

(define-language stlc
  #:vars (x)
  #:output-coq "stlc.v"
  #: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 (#:bind x : A) e) (cons e e)
                  (let (#:bind x #:bind x) = e in e)))

This example is equivalent to

(data stlc-val : 0 Type
  (stlc-true : stlc-val)
  (stlc-false : stlc-val)
  (stlc-unit : stlc-val))
 
(data stlc-type : 0 Type
  (stlc-boolty : stlc-type)
  (stlc-unitty : stlc-type)
  (stlc--> : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type)))
  (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
 
(data stlc-term : 0 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-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
  (stlc-term-let : (forall (e1 : stlc-term)
                     (forall (e2 : stlc-term)
                       stlc-term))))

This example is taken from cur/tests/stlc

syntax

(define-relation (name args ...)
 maybe-output-coq
 maybe-output-latex
 [premises ...
  horizontal-line name
  conclusion]
 ...)
 
maybe-output-coq = 
  | #:output-coq coq-filename
     
maybe-output-latex = 
  | #:output-latex latex-filename
Provides a notation for defining inductively defined relations similar to the define-judgment-form form Redex. Rather than attempt to explain the syntax in detail, here is an example:

(define-relation (has-type Gamma stlc-term stlc-type)
  #:output-coq "stlc.v"
  #:output-latex "stlc.tex"
  [(g : Gamma)
   ------------------------ T-Unit
   (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)]
 
  [(g : Gamma)
   ------------------------ T-False
   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
 
  [(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)]
 
  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
               (t1 : stlc-type) (t2 : stlc-type)
   (has-type g e1 t1)
   (has-type g e2 t2)
   ---------------------- T-Pair
   (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))]
 
  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
               (t1 : stlc-type) (t2 : stlc-type)
               (t : stlc-type)
   (has-type g e1 (stlc-* t1 t2))
   (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
   ---------------------- T-Let
   (has-type g (stlc-let e1 e2) t)]
 
  [(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 t1 e1) (stlc--> t1 t2))]
 
  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
               (t1 : stlc-type) (t2 : stlc-type)
   (has-type g e1 (stlc--> t1 t2))
   (has-type g e2 t1)
   ---------------------- T-App
   (has-type g (stlc-app e1 e2) t2)])

This example is equivalent to:

(data has-type : 0 (forall (x : Gamma)
                   (forall (y : stlc-term)
                     (forall (z : stlc-type)
                       Type)))
  (T-Unit : (forall (g : Gamma)
              (has-type
                g
                (stlc-val->stlc-term stlc-unit)
                stlc-unitty)))
  ....)

TODO: Need a Scribble library for defining Cur/Racket things in the same library in a nice way.

syntax

(generate-coq maybe-file maybe-exists expr)

 
maybe-file = 
  | #:file filename
     
maybe-exists = 
  | #:exists flag
A Racket form; translates the Cur expression expr to Coq code and outputs it to current-output-port, or to filename if filename is provided. If the file already exists, uses flag to figure out what to do, defaulting to 'error.