7.7
4 Olly: Ott-like LibrarY
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.
| (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-test/cur/tests/stlc
| (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.
(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.