suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Changed oll to olly

Browse Source
This commit is contained in:
William J. Bowman 2016-01-11 15:46:55 -05:00
parent 792d37252f
commit ebdb419dd7
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
5 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cur-doc/cur/cur.scrbl
View File

@ -45,4 +45,4 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code--
@include-section{scribblings/curnel.scrbl} @include-section{scribblings/curnel.scrbl}
@include-section{scribblings/reflection.scrbl} @include-section{scribblings/reflection.scrbl}
@include-section{scribblings/stdlib.scrbl} @include-section{scribblings/stdlib.scrbl}
@include-section{scribblings/oll.scrbl} @include-section{scribblings/olly.scrbl}

10
cur-doc/cur/scribblings/oll.scrbl → cur-doc/cur/scribblings/olly.scrbl
View File

@ -1,12 +1,12 @@
#lang scribble/manual #lang scribble/manual
@(require "defs.rkt") @(require "defs.rkt")
@title{OLL: Ott-like Library} @title{Olly: Ott-like LibrarY}
@defmodule[cur/oll] @defmodule[cur/olly]
The OLL provides syntax extensions for defining programming languages as inductive data. The library 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 is inspired by Ott@todo{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 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 powerful syntactic meta-programming can bring features previously only provided by external tools into
the language. the language.
@ -45,7 +45,7 @@ nonterminal to another.
If @racket[#:vars] is given, it should be a list of meta-variables that If @racket[#:vars] is given, it should be a list of meta-variables that
representing variables in the language. These meta-variables should only representing variables in the language. These meta-variables should only
appear in binding positions in @racket[constructors]. These variables appear in binding positions in @racket[constructors]. These variables
are represented as De Bruijn indexes, and OLL provides some functions are represented as De Bruijn indexes, and Olly provides some functions
for working with De Bruijn indexes. for working with De Bruijn indexes.
If @racket[#:output-coq] is given, it should be a string representing a If @racket[#:output-coq] is given, it should be a string representing a

2
cur-lib/cur/oll.rkt → cur-lib/cur/olly.rkt
View File

@ -1,5 +1,5 @@
#lang s-exp "cur.rkt" #lang s-exp "cur.rkt"
;; OLL: The OTT-Like Library ;; Olly: The OTT-Like LibrarY
;; TODO: Automagically create a parser from bnf grammar ;; TODO: Automagically create a parser from bnf grammar
(require (require
"stdlib/sugar.rkt" "stdlib/sugar.rkt"

2
cur-test/cur/tests/oll.rkt → cur-test/cur/tests/olly.rkt
View File

@ -6,7 +6,7 @@
(require (require
rackunit rackunit
cur/stdlib/sugar cur/stdlib/sugar
cur/oll) cur/olly)
(begin-for-syntax (begin-for-syntax
(require rackunit) (require rackunit)

2
cur-test/cur/tests/stlc.rkt
View File

@ -3,7 +3,7 @@
rackunit rackunit
cur/stdlib/nat cur/stdlib/nat
cur/stdlib/sugar cur/stdlib/sugar
cur/oll cur/olly
cur/stdlib/maybe cur/stdlib/maybe
cur/stdlib/bool cur/stdlib/bool
cur/stdlib/prop) cur/stdlib/prop)