{"size": 8211, "ext": "scrbl", "max_stars_repo_path": "cur-doc/cur/scribblings/olly.scrbl", "max_stars_repo_name": "jsmaniac/cur", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "cur-doc/cur/scribblings/olly.scrbl", "max_issues_repo_name": "jsmaniac/cur", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "cur-doc/cur/scribblings/olly.scrbl", "max_forks_repo_name": "jsmaniac/cur", "max_forks_repo_forks_event_min_datetime": "2021-10-02T16:05:54.000Z", "max_forks_repo_forks_event_max_datetime": "2021-10-02T16:05:54.000Z"}
{"max_stars_count": null, "max_issues_count": null, "max_forks_count": 1, "avg_line_length": 36.4933333333, "max_line_length": 102, "alphanum_fraction": 0.6201437097}
#lang scribble/manual
@(require "defs.rkt")

@title{Olly: Ott-like LibrarY}

@defmodule[cur/olly]
Olly provides syntax extensions for defining programming languages as inductive data. The library
is inspired by Ott@todo{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.

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

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

If @racket[#: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 @racket[Nat].
Binding positions in the syntax, represented by @racket[#:bind
nt-metavar], are erased in converting to De Bruijn indices, although
this may change if the representation of variables used by
@racket[define-language] changes.

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 (#:bind x : A) e) (cons e e)
                  (let (#:bind x #:bind 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
  (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))))]

@margin-note{This example is taken from @racketmodname[cur/tests/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 : 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:

@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)))
  ....)]
}

@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].
}

