diff --git a/scribblings/cur.scrbl b/scribblings/cur.scrbl index b6f1a17..f3fcc76 100644 --- a/scribblings/cur.scrbl +++ b/scribblings/cur.scrbl @@ -45,3 +45,4 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code-- @include-section{curnel.scrbl} @include-section{reflection.scrbl} @include-section{stdlib.scrbl} +@include-section{oll.scrbl} diff --git a/scribblings/oll.scrbl b/scribblings/oll.scrbl new file mode 100644 index 0000000..ce3c855 --- /dev/null +++ b/scribblings/oll.scrbl @@ -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]. +} +