Documented the OLL
This commit is contained in:
William J. Bowman
parent
c68d0ae97a
commit
edea1909ec
|
|
@ -45,3 +45,4 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code--
|
||||||
@include-section{curnel.scrbl}
|
@include-section{curnel.scrbl}
|
||||||
@include-section{reflection.scrbl}
|
@include-section{reflection.scrbl}
|
||||||
@include-section{stdlib.scrbl}
|
@include-section{stdlib.scrbl}
|
||||||
|
@include-section{oll.scrbl}
|
||||||
|
|
|
||||||
215
scribblings/oll.scrbl
Normal file
215
scribblings/oll.scrbl
Normal file
|
|
@ -0,0 +1,215 @@
|
||||||
|
#lang scribble/manual
|
||||||
|
@(require "defs.rkt")
|
||||||
|
|
||||||
|
@title{OLL: Ott-like Library}
|
||||||
|
|
||||||
|
@defmodule[cur/oll]
|
||||||
|
The OLL provides syntax extensions for defining programming languages as
|
||||||
|
inductive data. The library is inspired by Ott, 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.
|
||||||
|
|
||||||
|
@defform[(define-lanugage name
|
||||||
|
maybe-vars
|
||||||
|
maybe-output-coq
|
||||||
|
maybe-output-latex
|
||||||
|
(nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
|
||||||
|
#:grammar
|
||||||
|
[(maybe-vars
|
||||||
|
(code:line)
|
||||||
|
(code:line #:vars (nt-metavars ...)))
|
||||||
|
(maybe-output-coq
|
||||||
|
(code:line)
|
||||||
|
(code:line #:output-coq coq-filename))
|
||||||
|
(maybe-output-latex
|
||||||
|
(code:line)
|
||||||
|
(code:line #:output-latex latex-filename))
|
||||||
|
(maybe-bnfdef
|
||||||
|
(code:line)
|
||||||
|
(code:line ::=))]]{
|
||||||
|
Defines a new language by generating inductive definitions for each
|
||||||
|
nonterminal @racket[nt-name], whose constructors are generated by
|
||||||
|
@racket[constructors]. The constructors must either with a tag that can
|
||||||
|
be used to name the constructor, or be another meta-variable.
|
||||||
|
The meta-variables @racket[nt-metavars] are replaced by the corresponding
|
||||||
|
inductive types in @racket[constructors].
|
||||||
|
The name of each inductive datatype is generated by
|
||||||
|
@racket[(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 @racket[constructors], a constructor is defined that coerces one
|
||||||
|
nonterminal to another.
|
||||||
|
|
||||||
|
If @racket[#: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 @racket[constructors]. These variables
|
||||||
|
are represented as De Bruijn indexes, and OLL provides some functions
|
||||||
|
for working with De Bruijn indexes.
|
||||||
|
|
||||||
|
If @racket[#:output-coq] is given, it should be a string representing a
|
||||||
|
filename. The form @racket[define-language] will output Coq versions of
|
||||||
|
the language definitions to the @racket[coq-filename], overwriting the file.
|
||||||
|
|
||||||
|
If @racket[#:output-latex] is given, it should be a string representing a
|
||||||
|
filename. The form @racket[define-language] will output Latex versions of
|
||||||
|
the language definitions to the @racket[latex-filename], overwriting the file.
|
||||||
|
|
||||||
|
|
||||||
|
Example:
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
|
(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
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
|
(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))))))]
|
||||||
|
|
||||||
|
@margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(define-relation (name args ...)
|
||||||
|
maybe-output-coq
|
||||||
|
maybe-output-latex
|
||||||
|
[premises ...
|
||||||
|
horizontal-line name
|
||||||
|
conclusion]
|
||||||
|
...)
|
||||||
|
#:grammar
|
||||||
|
[(maybe-output-coq
|
||||||
|
(code:line)
|
||||||
|
(code:line #:output-coq coq-filename))
|
||||||
|
(maybe-output-latex
|
||||||
|
(code:line)
|
||||||
|
(code:line #:output-latex latex-filename))]]{
|
||||||
|
|
||||||
|
Provides a notation for defining inductively defined relations similar
|
||||||
|
to the @racket[define-judgment-form] form Redex. Rather than attempt to
|
||||||
|
explain the syntax in detail, here is an example:
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
|
(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:
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
|
(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)))
|
||||||
|
....)]
|
||||||
|
}
|
||||||
|
|
||||||
|
@deftogether[(@defthing[Var Type]
|
||||||
|
@defthing[avar (forall (x : Nat) Var)])]{
|
||||||
|
The type of a De Bruijn variable.
|
||||||
|
}
|
||||||
|
|
||||||
|
@defproc[(var-equal? [v1 Var] [v2 Var])
|
||||||
|
Bool]{
|
||||||
|
A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
|
||||||
|
represent the same variable.
|
||||||
|
}
|
||||||
|
|
||||||
|
@todo{Need a Scribble library for defining Cur/Racket things in the same
|
||||||
|
library in a nice way.}
|
||||||
|
|
||||||
|
@defform[(generate-coq maybe-file maybe-exists expr)
|
||||||
|
#:grammar
|
||||||
|
[(maybe-file
|
||||||
|
(code:line)
|
||||||
|
(code:line #:file filename))
|
||||||
|
(maybe-exists
|
||||||
|
(code:line)
|
||||||
|
(code:line #:exists flag))]]{
|
||||||
|
A Racket form; translates the Cur expression @racket[expr] to Coq code
|
||||||
|
and outputs it to @racket[current-output-port], or to @racket[filename]
|
||||||
|
if @racket[filename] is provided. If the file already exists, uses
|
||||||
|
@racket[flag] to figure out what to do, defaulting to @racket['error].
|
||||||
|
}
|
||||||
|
|
||||||
Loading…
Reference in New Issue
Block a user