6.2.901.900
4 OLL: Ott-like Library
The OLL 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 the OLL 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-metavars) maybe-bnfdef constructors ...) ...) |
|
| |
| maybe-vars | | = | | | | | | | | | #:vars (nt-metavars ...) | | | | | | | | maybe-output-coq | | = | | | | | | | | | #:output-coq coq-filename | | | | | | | | maybe-output-latex | | = | | | | | | | | | #:output-latex latex-filename | | | | | | | | maybe-bnfdef | | = | | | | | | | | | ::= |
|
Defines a new language by generating inductive definitions for each
nonterminal nt-name, whose constructors are generated by
constructors. The constructors must either with a tag that can
be used to name the constructor, or be another meta-variable.
The meta-variables nt-metavars are replaced by the corresponding
inductive types in constructors.
The name of each inductive datatype is generated by
(format-id "~a-~a" name nt-name).
Later nonterminals can refer to prior nonterminals, but they cannot be
mutually inductive due to limitations in Cur. When nonterminals appear
in constructors, a constructor is defined that coerces one
nonterminal to another.
If #:vars is given, it should be a list of meta-variables that
representing variables in the language. These meta-variables should only
appear in binding positions in constructors. These variables
are represented as De Bruijn indexes, and OLL provides some functions
for working with De Bruijn indexes.
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.
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 (x : A) e) (cons e e) |
| (let (x x) = e in e))) |
This example is equivalent to
| (data stlc-val : Type |
| (stlc-true : stlc-val) |
| (stlc-false : stlc-val) |
| (stlc-unit : stlc-val)) |
| |
| (data stlc-type : 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 : Type |
| (stlc-var-->-stlc-term : (forall (x : Var) stlc-term)) |
| (stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term)) |
| (stlc-term-lambda : (forall (x : Var) |
| (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 (x : Var) |
| (forall (y : Var) |
| (forall (e1 : stlc-term) |
| (forall (e2 : stlc-term) |
| stlc-term)))))) |
This example is taken from cur/examples/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 : 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)] |
| |
| [(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) |
| (x : Var) (y : Var) |
| (has-type g e1 (stlc-* t1 t2)) |
| (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t) |
| ---------------------- T-Let |
| (has-type g (stlc-let x y e1 e2) t)] |
| |
| [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var) |
| (has-type (extend-gamma g x t1) e1 t2) |
| ---------------------- T-Fun |
| (has-type g (stlc-lambda x 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 : (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))) |
| ....) |
|
avar : (forall (x : Nat) Var)
|
|
The type of a De Bruijn variable.
(var-equal? v1 v2) → Bool
|
| v1 : Var |
| v2 : Var |
A Cur procedure; returns true if v1 and v2
represent the same variable.
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.