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

Split and reorganized package. Closes #14

Browse Source 
Created split packages: cur, cur-lib, cur-test, cur-doc, similar to
other Racket packages, e.g., redex.

* Moved tests out of core and into cur-test
* Moved docs into cur-doc
* Moved cur implementation and libraries into cur-lib
* Added cur meta-pacakge that installs all of the above
This commit is contained in:
William J. Bowman 2016-01-09 15:27:27 -05:00
parent 647229a577
commit 792d37252f
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
47 changed files with 1692 additions and 1648 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
README.md
View File

@ -15,20 +15,30 @@ cur (plural curs)
Disclaimer
==========
Cur is currently under active hackery and is not fit for use for any
particular purpose. It is fraught with unreadable code, errors, and
hacks that should never have been written by a reasonable human being.
particular purpose. It is fraught with unreadable code, errors,
performance bugs, and hacks that should never have been written by a
reasonable human being.
These may or may not be fixed shortly.
Getting started
===============
Easy mode:
Install cur via `raco pkg install cur`.
Advanced mode:
Cur is actually distributed as several packages.
`cur-lib` provides the implementation and all standard
libraries.
`cur-doc` provides the documentation.
`cur-test` provides a test suite and examples.
Try it out: open up DrRacket and put the following in the definition area:
```racket
#lang cur
(require
(require
cur/stdlib/bool
cur/stdlib/nat)
@ -44,27 +54,20 @@ Try entering the following in the interaction area:
See the docs: `raco docs cur`.
Most of the standard library is currently undocumented, so just see the source.
Going further
=============
Open up `examples/example.rkt` to see a tour of Cur's features.
Open up `examples/stlc.rkt` to see an example of what advanced meta-programming can let you do.
Open up `oll.rkt` to see the implementation of the meta-programs used to
enable `examples/stlc.rkt`, including the parsers for BNF syntax and inference rule
syntax, and Coq and LaTeX generators.
Open up `cur-tests/cur/tests/stlc.rkt` to see an example of the
simply-typed lambda-calculus modeled in Cur, with a parser and syntax
extension to enable deeply embedding.
Open up `examples/proofs-for-free.rkt` to see an implementation of the
translation defined in [Proofs for Free](http://staff.city.ac.uk/~ross/papers/proofs.html) as a meta-program.
Open up `stdlib/tactics` to see tactics, implemented entirely via
meta-programming.
Open up `cur-lib/cur/stdlib/tactics` to see one way to implement tactics in Cur.
Open up anything in `stdlib/` to see some standard dependent-type
Open up anything in `cur-lib/cur/stdlib/` to see some standard dependent-type
formalisms.
Open up `curnel/redex-core.rkt` to see the entire "trusted" (after a
large test suite) core.
Open up `cur-lib/cur/curnel/redex-core.rkt` to see the entire
implementation of the core language, <600 lines of code.

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

@ -1,6 +1,6 @@
#lang scribble/manual
@(require
"defs.rkt"
"scribblings/defs.rkt"
racket/function)
@title[#:style '(toc)]{Cur}
@ -42,7 +42,7 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code--
@local-table-of-contents[]
@include-section{curnel.scrbl}
@include-section{reflection.scrbl}
@include-section{stdlib.scrbl}
@include-section{oll.scrbl}
@include-section{scribblings/curnel.scrbl}
@include-section{scribblings/reflection.scrbl}
@include-section{scribblings/stdlib.scrbl}
@include-section{scribblings/oll.scrbl}

2
cur-doc/cur/info.rkt Normal file
View File

@ -0,0 +1,2 @@
#lang info
(define scribblings '(("cur.scrbl" (multi-page))))

0
scribblings/curnel.scrbl → cur-doc/cur/scribblings/curnel.scrbl
View File

0
scribblings/defs.rkt → cur-doc/cur/scribblings/defs.rkt
View File

0
scribblings/oll.scrbl → cur-doc/cur/scribblings/oll.scrbl
View File

0
scribblings/reflection.scrbl → cur-doc/cur/scribblings/reflection.scrbl
View File

0
scribblings/stdlib.scrbl → cur-doc/cur/scribblings/stdlib.scrbl
View File

0
scribblings/stdlib/bool.scrbl → cur-doc/cur/scribblings/stdlib/bool.scrbl
View File

0
scribblings/stdlib/maybe.scrbl → cur-doc/cur/scribblings/stdlib/maybe.scrbl
View File

0
scribblings/stdlib/nat.scrbl → cur-doc/cur/scribblings/stdlib/nat.scrbl
View File

0
scribblings/stdlib/sugar.scrbl → cur-doc/cur/scribblings/stdlib/sugar.scrbl
View File

0
scribblings/stdlib/tactics.scrbl → cur-doc/cur/scribblings/stdlib/tactics.scrbl
View File

0
scribblings/stdlib/typeclass.scrbl → cur-doc/cur/scribblings/stdlib/typeclass.scrbl
View File

6
cur-doc/info.rkt Normal file
View File

@ -0,0 +1,6 @@
#lang info
(define collection 'multi)
(define deps '("base" "racket-doc"))
(define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
(define pkg-desc "Documentation for \"cur\".")
(define pkg-authors '(wilbowma))

0
cur.rkt → cur-lib/cur/cur.rkt
View File

590
cur-lib/cur/curnel/redex-core.rkt Normal file
View File

@ -0,0 +1,590 @@
#lang racket/base
(require
racket/function
redex/reduction-semantics)
(provide
(all-defined-out))
(set-cache-size! 10000)
#| References:
| http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
| https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
| http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf
| http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf
| http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74
| http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
|#
#| ttL is the core language of Cur. Very similar to TT (Idirs core) and Luo's UTT. Surface
| langauge should provide short-hand, such as -> for non-dependent function types, and type
| inference.
|#
(define-language ttL
(i j k ::= natural)
(U ::= (Unv i))
(t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
;; Δ (signature). (inductive-name : type ((constructor : type) ...))
;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
(Δ ::= ∅ (Δ (D : t ((c : t) ...))))
(D x c ::= variable-not-otherwise-mentioned)
#:binding-forms
(λ (x : t) e #:refers-to x)
(Π (x : t_0) t_1 #:refers-to x))
(define x? (redex-match? ttL x))
(define t? (redex-match? ttL t))
(define e? (redex-match? ttL e))
(define U? (redex-match? ttL U))
(define Δ? (redex-match? ttL Δ))
;;; ------------------------------------------------------------------------
;;; Universe typing
(define-judgment-form ttL
#:mode (unv-type I O)
#:contract (unv-type U U)
[(where i_1 ,(add1 (term i_0)))
-----------------
(unv-type (Unv i_0) (Unv i_1))])
;; Universe predicativity rules. Impredicative in (Unv 0)
(define-judgment-form ttL
#:mode (unv-pred I I O)
#:contract (unv-pred U U U)
[----------------
(unv-pred (Unv i) (Unv 0) (Unv 0))]
[(where i_3 ,(max (term i_1) (term i_2)))
----------------
(unv-pred (Unv i_1) (Unv i_2) (Unv i_3))])
(define-metafunction ttL
α-equivalent? : t t -> #t or #f
[(α-equivalent? t_0 t_1)
,(alpha-equivalent? ttL (term t_0) (term t_1))])
;; Replace x by t_1 in t_0
(define-metafunction ttL
subst : t x t -> t
[(subst t_0 x t_1)
(substitute t_0 x t_1)])
(define-metafunction ttL
subst-all : t (x ...) (e ...) -> t
[(subst-all t () ()) t]
[(subst-all t (x_0 x ...) (e_0 e ...))
(subst-all (subst t x_0 e_0) (x ...) (e ...))])
;;; ------------------------------------------------------------------------
;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
;;; TODO: Might be worth maintaining the above bijection between Δ and maps for performance reasons
;; TODO: This is doing too many things
;; NB: Depends on clause order
(define-metafunction ttL
Δ-ref-type : Δ x -> t or #f
[(Δ-ref-type ∅ x) #f]
[(Δ-ref-type (Δ (x : t any)) x) t]
[(Δ-ref-type (Δ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
[(Δ-ref-type (Δ (x_0 : t_0 any)) x) (Δ-ref-type Δ x)])
(define-metafunction ttL
Δ-set : Δ x t ((x : t) ...) -> Δ
[(Δ-set Δ x t any) (Δ (x : t any))])
(define-metafunction ttL
Δ-union : Δ Δ -> Δ
[(Δ-union Δ ∅) Δ]
[(Δ-union Δ_2 (Δ_1 (x : t any)))
((Δ-union Δ_2 Δ_1) (x : t any))])
;; Returns the inductively defined type that x constructs
;; NB: Depends on clause order
(define-metafunction ttL
Δ-key-by-constructor : Δ x -> x
[(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
x]
[(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
(Δ-key-by-constructor Δ x)])
;; Returns the constructor map for the inductively defined type x_D in the signature Δ
(define-metafunction ttL
Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
;; NB: Depends on clause order
[(Δ-ref-constructor-map ∅ x_D) #f]
[(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
any]
[(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
(Δ-ref-constructor-map Δ x_D)])
;; TODO: Should not use Δ-ref-type
(define-metafunction ttL
Δ-ref-constructor-type : Δ x x -> t
[(Δ-ref-constructor-type Δ x_D x_ci)
(Δ-ref-type Δ x_ci)])
;; Get the list of constructors for the inducitvely defined type x_D
;; NB: Depends on clause order
(define-metafunction ttL
Δ-ref-constructors : Δ x -> (x ...) or #f
[(Δ-ref-constructors ∅ x_D) #f]
[(Δ-ref-constructors (Δ (x_D : t_D ((x : t) ...))) x_D)
(x ...)]
[(Δ-ref-constructors (Δ (x_1 : t_1 any)) x_D)
(Δ-ref-constructors Δ x_D)])
;; NB: Depends on clause order
(define-metafunction ttL
sequence-index-of : any (any ...) -> natural
[(sequence-index-of any_0 (any_0 any ...))
0]
[(sequence-index-of any_0 (any_1 any ...))
,(add1 (term (sequence-index-of any_0 (any ...))))])
;; Get the index of the constructor x_ci in the list of constructors for x_D
(define-metafunction ttL
Δ-constructor-index : Δ x x -> natural
[(Δ-constructor-index Δ x_D x_ci)
(sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
;;; ------------------------------------------------------------------------
;;; Operations that involve contexts.
(define-extended-language tt-ctxtL ttL
;; Telescope.
;; NB: There is a bijection between this an a vector of maps from x to t
(Ξ Φ ::= hole (Π (x : t) Ξ))
;; Apply context
;; NB: There is a bijection between this an a vector expressions
(Θ ::= hole (Θ e)))
(define Ξ? (redex-match? tt-ctxtL Ξ))
(define Φ? (redex-match? tt-ctxtL Φ))
(define Θ? (redex-match? tt-ctxtL Θ))
;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
;; Return the parameters of x_D as a telescope Ξ
;; TODO: Define generic traversals of Δ and Γ ?
(define-metafunction tt-ctxtL
Δ-ref-parameter-Ξ : Δ x -> Ξ
[(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
Ξ]
[(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
(Δ-ref-parameter-Ξ Δ x_D)])
;; Applies the term t to the telescope Ξ.
;; TODO: Test
#| TODO:
| This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true
| that (equivalent t (Ξ-apply Ξ t))?
| Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
|#
(define-metafunction tt-ctxtL
Ξ-apply : Ξ t -> t
[(Ξ-apply hole t) t]
[(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])
;; Compose multiple telescopes into a single telescope:
(define-metafunction tt-ctxtL
Ξ-compose : Ξ Ξ ... -> Ξ
[(Ξ-compose Ξ) Ξ]
[(Ξ-compose Ξ_0 Ξ_1 Ξ_rest ...)
(Ξ-compose (in-hole Ξ_0 Ξ_1) Ξ_rest ...)])
;; Compute the number of arguments in a Ξ
(define-metafunction tt-ctxtL
Ξ-length : Ξ -> natural
[(Ξ-length hole) 0]
[(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
;; Compute the number of applications in a Θ
(define-metafunction tt-ctxtL
Θ-length : Θ -> natural
[(Θ-length hole) 0]
[(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
(define-metafunction tt-ctxtL
Θ-ref : Θ natural -> e or #f
[(Θ-ref hole natural) #f]
[(Θ-ref (in-hole Θ (hole e)) 0) e]
[(Θ-ref (in-hole Θ (hole e)) natural) (Θ-ref Θ ,(sub1 (term natural)))])
;;; ------------------------------------------------------------------------
;;; Computing the types of eliminators
;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
(define-metafunction tt-ctxtL
Δ-constructor-telescope : Δ x x -> Ξ
[(Δ-constructor-telescope Δ x_D x_ci)
Ξ
(where (in-hole Ξ (in-hole Θ x_D))
(Δ-ref-constructor-type Δ x_D x_ci))])
;; Returns the parameter arguments as an apply context of the constructor x_ci of the inductively
;; defined type x_D
(define-metafunction tt-ctxtL
Δ-constructor-parameters : Δ x x -> Θ
[(Δ-constructor-parameters Δ x_D x_ci)
Θ
(where (in-hole Ξ (in-hole Θ x_D))
(Δ-ref-constructor-type Δ x_D x_ci))])
;; Inner loop for Δ-constructor-noninductive-telescope
(define-metafunction tt-ctxtL
noninductive-loop : x Φ -> Φ
[(noninductive-loop x_D hole) hole]
[(noninductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
(noninductive-loop x_D Φ_1)]
[(noninductive-loop x_D (Π (x : t) Φ_1))
(Π (x : t) (noninductive-loop x_D Φ_1))])
;; Returns the noninductive arguments to the constructor x_ci of the inductively defined type x_D
(define-metafunction tt-ctxtL
Δ-constructor-noninductive-telescope : Δ x x -> Ξ
[(Δ-constructor-noninductive-telescope Δ x_D x_ci)
(noninductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
;; Inner loop for Δ-constructor-inductive-telescope
;; NB: Depends on clause order
(define-metafunction tt-ctxtL
inductive-loop : x Φ -> Φ
[(inductive-loop x_D hole) hole]
[(inductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
(Π (x : (in-hole Φ (in-hole Θ x_D))) (inductive-loop x_D Φ_1))]
[(inductive-loop x_D (Π (x : t) Φ_1))
(inductive-loop x_D Φ_1)])
;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
(define-metafunction tt-ctxtL
Δ-constructor-inductive-telescope : Δ x x -> Ξ
[(Δ-constructor-inductive-telescope Δ x_D x_ci)
(inductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
;; Returns the inductive hypotheses required for eliminating the inductively defined type x_D with
;; motive t_P, where the telescope Φ are the inductive arguments to a constructor for x_D
(define-metafunction tt-ctxtL
hypotheses-loop : x t Φ -> Φ
[(hypotheses-loop x_D t_P hole) hole]
[(hypotheses-loop x_D t_P (name any_0 (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1)))
;; TODO: Instead of this nonsense, it might be simpler to pass in the type of t_P and use that
;; as/to compute the type of the hypothesis.
(Π (x_h : (in-hole Φ ((in-hole Θ t_P) (Ξ-apply Φ x))))
(hypotheses-loop x_D t_P Φ_1))
(where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
;; Returns the inductive hypotheses required for the elimination method of constructor x_ci for
;; inductive type x_D, when eliminating with motive t_P.
(define-metafunction tt-ctxtL
Δ-constructor-inductive-hypotheses : Δ x x t -> Ξ
[(Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P)
(hypotheses-loop x_D t_P (Δ-constructor-inductive-telescope Δ x_D x_ci))])
(define-metafunction tt-ctxtL
Δ-constructor-method-telescope : Δ x x t -> Ξ
[(Δ-constructor-method-telescope Δ x_D x_ci t_P)
(Π (x_mi : (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a x_ci)))))
hole)
(where Θ_p (Δ-constructor-parameters Δ x_D x_ci))
(where Ξ_a (Δ-constructor-telescope Δ x_D x_ci))
(where Ξ_h (Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P))
(where x_mi ,(variable-not-in (term (t_P Δ)) 'x-mi))])
;; fold Ξ-compose over map Δ-constructor-method-telescope over the list of constructors
(define-metafunction tt-ctxtL
method-loop : Δ x t (x ...) -> Ξ
[(method-loop Δ x_D t_P ()) hole]
[(method-loop Δ x_D t_P (x_0 x_rest ...))
(Ξ-compose (Δ-constructor-method-telescope Δ x_D x_0 t_P) (method-loop Δ x_D t_P (x_rest ...)))])
;; Returns the telescope of all methods required to eliminate the type x_D with motive t_P
(define-metafunction tt-ctxtL
Δ-methods-telescope : Δ x t -> Ξ
[(Δ-methods-telescope Δ x_D t_P)
(method-loop Δ x_D t_P (Δ-ref-constructors Δ x_D))])
;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
;; is in universe U.
;;
;; The type of (elim x_D U) is something like:
;; (∀ (P : (∀ a -> ... -> (D a ...) -> U))
;; (method_ci ...) -> ... ->
;; (a -> ... -> (D a ...) ->
;; (P a ... (D a ...))))
;;
;; x_D is an inductively defined type
;; U is the sort the motive
;; x_P is the name of the motive
;; Ξ_P*D is the telescope of the parameters of x_D and
;; the witness of type x_D (applied to the parameters)
;; Ξ_m is the telescope of the methods for x_D
(define-metafunction tt-ctxtL
Δ-elim-type : Δ x U -> t
[(Δ-elim-type Δ x_D U)
(Π (x_P : (in-hole Ξ_P*D U))
;; The methods Ξ_m for each constructor of type x_D
(in-hole Ξ_m
;; And finally, the parameters and discriminant
(in-hole Ξ_P*D
;; The result is (P a ... (x_D a ...)), i.e., the motive
;; applied to the paramters and discriminant
(Ξ-apply Ξ_P*D x_P))))
;; Get the parameters of x_D
(where Ξ (Δ-ref-parameter-Ξ Δ x_D))
;; A fresh name to bind the discriminant
(where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
;; of the parameters and the inductive type applied to the
;; parameters
(where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
;; A fresh name for the motive
(where x_P ,(variable-not-in (term (Δ Γ x_D Ξ Ξ_P*D x)) 'x-P))
;; The types of the methods for this inductive.
(where Ξ_m (Δ-methods-telescope Δ x_D x_P))])
;; TODO: This might belong in the next section, since it's related to evaluation
;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
;; In more detaill, given motive t_P, parameters Θ_p, methods Θ_m, and arguments Θ_i to constructor
;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i,
;; generate: (elim x_D U t_P Θ_m ... Θ_p ... t_i)
(define-metafunction tt-ctxtL
Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
[(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (in-hole Θ_i (hole (name t_i (in-hole Θ_r x_ci)))))
((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
(in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
(side-condition (memq (term x_ci) (term (Δ-ref-constructors Δ x_D))))]
[(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_nr) hole])
;;; ------------------------------------------------------------------------
;;; Dynamic semantics
;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
;;; inductively defined type x with a motive whose result is in universe U
(define-extended-language tt-redL tt-ctxtL
;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
;; determining whether or not it is partially applied cannot be done with the grammar alone.
(v ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
(Θv ::= hole (Θv v))
;; call-by-value, plus reduce under Π (helps with typing checking)
(E ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
(define Θv? (redex-match? tt-redL Θv))
(define E? (redex-match? tt-redL E))
(define v? (redex-match? tt-redL v))
(define tt-->
(reduction-relation tt-redL
(--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
(Δ (in-hole E (subst t_1 x t_2)))
-->β)
(--> (Δ (in-hole E (in-hole Θv ((elim x_D U) v_P))))
(Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
#|
| The elim form must appear applied like so:
| (elim x_D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
|
| Where:
| x_D is the inductive being eliminated
| U is the universe of the result of the motive
| v_P is the motive
| m_{0..n} are the methods
| p ... are the parameters of x_D
| c_i is a constructor of x_d
| a ... are the arguments to c_i
| Unfortunately, Θ contexts turn all this inside out:
| TODO: Write better abstractions for this notation
|#
;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
;; the discriminant: the constructor x_ci applied to its argument Θv_i
(where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
;; arguments.
(side-condition (equal? (term (Θ-length Θv_p)) (term (Ξ-length (Δ-ref-parameter-Ξ Δ x_D)))))
;; Ensure x_ci is actually a constructor for x_D
(where (x_c* ...) (Δ-ref-constructors Δ x_D))
(side-condition (memq (term x_ci) (term (x_c* ...))))
;; There should be a number of methods equal to the number of constructors; to ensure E
;; doesn't capture methods and Θv_m doesn't capture other arguments
(side-condition (equal? (length (term (x_c* ...))) (term (Θ-length Θv_m))))
;; Find the method for constructor x_ci, relying on the order of the arguments.
(where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ x_D x_ci)))
;; Generate the inductive recursion
(where Θ_r (Δ-inductive-elim Δ x_D U v_P Θv_p Θv_m Θv_i))
-->elim)))
(define-metafunction tt-redL
step : Δ e -> e
[(step Δ e)
e_r
(where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Δ e)))))])
(define-metafunction tt-redL
reduce : Δ e -> e
[(reduce Δ e)
e_r
(where (_ e_r)
,(let ([r (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)])
;; Efficient check for (= (length r) 1)
;; NB: Check is overly aggressive and produces wrong error,
;; because not reducing under lambda.
#;(unless (null? (cdr r))
(error "Church-Rosser broken" r))
(car r)))])
(define-judgment-form tt-redL
#:mode (equivalent I I I)
#:contract (equivalent Δ t t)
[(where t_2 (reduce Δ t_0))
(where t_3 (reduce Δ t_1))
(side-condition (α-equivalent? t_2 t_3))
----------------- "≡-αβ"
(equivalent Δ t_0 t_1)])
;;; ------------------------------------------------------------------------
;;; Type checking and synthesis
(define-extended-language tt-typingL tt-redL
;; NB: There may be a bijection between Γ and Ξ. That's interesting.
;; NB: Also a bijection between Γ and a list of maps from x to t.
(Γ ::= ∅ (Γ x : t)))
(define Γ? (redex-match? tt-typingL Γ))
(define-metafunction tt-typingL
Γ-union : Γ Γ -> Γ
[(Γ-union Γ ∅) Γ]
[(Γ-union Γ_2 (Γ_1 x : t))
((Γ-union Γ_2 Γ_1) x : t)])
(define-metafunction tt-typingL
Γ-set : Γ x t -> Γ
[(Γ-set Γ x t) (Γ x : t)])
;; NB: Depends on clause order
(define-metafunction tt-typingL
Γ-ref : Γ x -> t or #f
[(Γ-ref ∅ x) #f]
[(Γ-ref (Γ x : t) x) t]
[(Γ-ref (Γ x_0 : t_0) x_1) (Γ-ref Γ x_1)])
;; NB: Depends on clause order
(define-metafunction tt-typingL
Γ-remove : Γ x -> Γ
[(Γ-remove ∅ x) ∅]
[(Γ-remove (Γ x : t) x) Γ]
[(Γ-remove (Γ x_0 : t_0) x_1) (Γ-remove Γ x_1)])
(define-metafunction tt-typingL
nonpositive : x t -> #t or #f
[(nonpositive x (in-hole Θ x))
#t]
[(nonpositive x (Π (x_0 : (in-hole Θ x)) t))
#f]
[(nonpositive x (Π (x_0 : t_0) t))
,(and (term (positive x t_0)) (term (nonpositive x t)))]
[(nonpositive x t) #t])
(define-metafunction tt-typingL
positive : x t -> #t or #f
[(positive x (in-hole Θ x))
#f]
[(positive x (Π (x_0 : (in-hole Θ x)) t))
(positive x t)]
[(positive x (Π (x_0 : t_0) t))
,(and (term (nonpositive x t_0)) (term (positive x t)))]
[(positive x t) #t])
(define-metafunction tt-typingL
positive* : x (t ...) -> #t or #f
[(positive* x_D ()) #t]
[(positive* x_D (t_c t_rest ...))
;; Replace the result of the constructor with (Unv 0), to avoid the result being considered a
;; nonpositive position.
,(and (term (positive x_D (in-hole Ξ (Unv 0)))) (term (positive* x_D (t_rest ...))))
(where (in-hole Ξ (in-hole Θ x_D)) t_c)])
;; Holds when the signature Δ and typing context Γ are well-formed.
(define-judgment-form tt-typingL
#:mode (wf I I)
#:contract (wf Δ Γ)
[----------------- "WF-Empty"
(wf ∅ ∅)]
[(type-infer Δ Γ t t_0)
(wf Δ Γ)
----------------- "WF-Var"
(wf Δ (Γ x : t))]
[(wf Δ ∅)
(type-infer Δ ∅ t_D U_D)
(type-infer Δ (∅ x_D : t_D) t_c U_c) ...
;; NB: Ugh this should be possible with pattern matching alone ....
(side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
(side-condition (positive* x_D (t_c ...)))
----------------- "WF-Inductive"
(wf (Δ (x_D : t_D
;; Checks that a constructor for x actually produces an x, i.e., that
;; the constructor is well-formed.
((x_c : (name t_c (in-hole Ξ (in-hole Θ x_D*)))) ...))) ∅)])
;; TODO: Bi-directional and inference?
;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
;; Holds when e has type t under signature Δ and typing context Γ
(define-judgment-form tt-typingL
#:mode (type-infer I I I O)
#:contract (type-infer Δ Γ e t)
[(wf Δ Γ)
(unv-type U_0 U_1)
----------------- "DTR-Unv"
(type-infer Δ Γ U_0 U_1)]
[(where t (Δ-ref-type Δ x))
----------------- "DTR-Inductive"
(type-infer Δ Γ x t)]
[(where t (Γ-ref Γ x))
----------------- "DTR-Start"
(type-infer Δ Γ x t)]
[(type-infer Δ (Γ x : t_0) e t_1)
(type-infer Δ Γ (Π (x : t_0) t_1) U)
----------------- "DTR-Abstraction"
(type-infer Δ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
[(type-infer Δ Γ t_0 U_1)
(type-infer Δ (Γ x : t_0) t U_2)
(unv-pred U_1 U_2 U)
----------------- "DTR-Product"
(type-infer Δ Γ (Π (x : t_0) t) U)]
[(type-infer Δ Γ e_0 t)
;; Cannot rely on type-infer producing normal forms.
(where (Π (x_0 : t_0) t_1) (reduce Δ t))
(type-check Δ Γ e_1 t_0)
(where t_3 (subst t_1 x_0 e_1))
----------------- "DTR-Application"
(type-infer Δ Γ (e_0 e_1) t_3)]
[(where t (Δ-elim-type Δ D U))
(type-infer Δ Γ t U_e)
----------------- "DTR-Elim_D"
(type-infer Δ Γ (elim D U) t)])
(define-judgment-form tt-typingL
#:mode (type-check I I I I)
#:contract (type-check Δ Γ e t)
[(type-infer Δ Γ e t_0)
(equivalent Δ t t_0)
----------------- "DTR-Check"
(type-check Δ Γ e t)])

0
curnel/redex-lang.rkt → cur-lib/cur/curnel/redex-lang.rkt
View File

0
lang/reader.rkt → cur-lib/cur/lang/reader.rkt
View File

92
oll.rkt → cur-lib/cur/oll.rkt
View File

@ -12,7 +12,15 @@
Var
avar
var-equal?
generate-coq)
generate-coq
;; private; exported for testing only
(for-syntax
coq-defns
output-latex-bnf
output-coq
new-name
fresh-name))
(begin-for-syntax
(define-syntax-class dash
@ -86,27 +94,6 @@
(define (fresh-name id)
(datum->syntax id (gensym (syntax->datum id)))))
(module+ test
(begin-for-syntax
(require rackunit)
(define (check-id-equal? v1 v2)
(check-equal?
(syntax->datum v1)
(syntax->datum v2)))
(define (check-id-match? v1 v2)
(check-regexp-match
v1
(symbol->string (syntax->datum v2))))
(check-id-match?
#px"term\\d+"
(fresh-name #'term))
(check-id-equal?
#'stlc-lambda
(new-name #'stlc #'lambda))
(check-id-match?
#px"stlc-term\\d+"
(new-name #'stlc (fresh-name #'term)))))
;; TODO: Oh, this is a mess. Rewrite it.
(begin-for-syntax
(define lang-name (make-parameter #'name))
@ -196,20 +183,7 @@
(with-output-to-file file-name
(thunk (printf (output-latex-bnf vars clauses)))
#:exists 'append)))
(module+ test
(require "stdlib/sugar.rkt")
(begin-for-syntax
(require rackunit)
(check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
(output-latex-bnf #'(x)
#'((term (e) ::= (e1 e2) (lambda (x) e)))))
(check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
(output-latex-bnf #'(x)
#'((type (A B C) ::= unit (* A B) (+ A C)))))))
;; TODO: For better error messages, add context, rename some of these patterns. e.g.
;; (type (meta-vars) ::= ?? )
;; TODO: Extend define-language with syntax such as ....
@ -243,14 +217,6 @@
(match v2
[(avar (n2 : Nat))
(nat-equal? n1 n2)])]))
(module+ test
(require rackunit)
(check-equal?
(var-equal? (avar z) (avar z))
true)
(check-equal?
(var-equal? (avar z) (avar (s z)))
false))
;; See stlc.rkt for examples
@ -346,41 +312,3 @@
(format "Eval compute in ~a." body))))
(displayln (format "~a~a" (coq-defns) output))
#'(begin))]))
(module+ test
(begin-for-syntax
(check-equal?
(parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
(format "Inductive nat : Type :=~n| z : nat.~n"))
(check-regexp-match
"(forall .+ : Type, Type)"
(output-coq #'(-> Type Type)))
(let ([t (parameterize ([coq-defns ""])
(output-coq #'(define-relation (meow gamma term type)
[(g : gamma) (e : term) (t : type)
--------------- T-Bla
(meow g e t)]))
(coq-defns))])
(check-regexp-match
"Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
(first (string-split t "\n")))
(check-regexp-match
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
(second (string-split t "\n"))))
(let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
(lambda* (x : nat) (ih-x : nat) ih-x)
e))])
(check-regexp-match
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
t))
(check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
(parameterize ([coq-defns ""])
(output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
(== nat (plus n m) (plus m n)))))
(coq-defns)))
(check-regexp-match
"Function add1 \\(n : nat\\) := \\(s n\\).\n"
(parameterize ([coq-defns ""])
(output-coq #'(define (add1 (n : nat)) (s n)))
(coq-defns)))))

24
cur-lib/cur/stdlib/bool.rkt Normal file
View File

@ -0,0 +1,24 @@
#lang s-exp "../cur.rkt"
(require "sugar.rkt")
(provide Bool true false if not and or)
(data Bool : Type
(true : Bool)
(false : Bool))
(define-syntax-rule (if t s f)
(match t
[true s]
[false f]))
(define (not (x : Bool)) (if x false true))
(define (and (x : Bool) (y : Bool))
(if x
y
(not y)))
(define (or (x : Bool) (y : Bool))
(if x
true
y))

13
cur-lib/cur/stdlib/maybe.rkt Normal file
View File

@ -0,0 +1,13 @@
#lang s-exp "../cur.rkt"
(require "sugar.rkt")
(provide Maybe none some some/i)
(data Maybe : (forall (A : Type) Type)
(none : (forall (A : Type) (Maybe A)))
(some : (forall* (A : Type) (a : A) (Maybe A))))
(define-syntax (some/i syn)
(syntax-case syn ()
[(_ a)
(let ([a-ty (type-infer/syn #'a)])
#`(some #,a-ty a))]))

45
stdlib/nat.rkt → cur-lib/cur/stdlib/nat.rkt
View File

@ -3,55 +3,37 @@
;; TODO: override (all-defined-out) to enable exporting all these
;; properly.
(provide Nat z s add1 sub1 plus mult exp square nat-equal? even? odd?)
(module+ test
(require rackunit))
(data Nat : Type
(z : Nat)
(s : (-> Nat Nat)))
(define (add1 (n : Nat)) (s n))
(module+ test
(check-equal? (add1 (s z)) (s (s z))))
(define (sub1 (n : Nat))
(match n
[z z]
[(s (x : Nat)) x]))
(module+ test
(check-equal? (sub1 (s z)) z))
(define (plus (n1 : Nat) (n2 : Nat))
(match n1
[z n2]
[(s (x : Nat))
(s (recur x))]))
(module+ test
(check-equal? (plus z z) z)
(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
(define (mult (m : Nat) (n : Nat))
(match m
[z z]
[(s (x : Nat))
(plus n (recur x))]))
(module+ test
(check-equal? (mult (s (s z)) z) z)
(check-equal? (mult (s (s z)) (s z)) (s (s z))))
(define (exp (m : Nat) (e : Nat))
(match m
[z (s z)]
[(s (x : Nat))
(mult e (recur x))]))
(module+ test
#;(check-equal? (exp z z) (s z))
#;(check-equal? (exp (s z) z) z))
(define square (run (exp (s (s z)))))
;; TODO: This test takes too long t run
#;(module+ test
(check-equal? (square (s (s z))) (s (s (s (s z))))))
;; Credit to this function goes to Max
(define nat-equal?
@ -64,10 +46,6 @@
false
(lambda* (x : Nat) (ih-bla : Bool)
(ih x))))))
(module+ test
(check-equal? (nat-equal? z z) true)
(check-equal? (nat-equal? z (s z)) false)
(check-equal? (nat-equal? (s z) (s z)) true))
(define (even? (n : Nat))
(match n
@ -77,26 +55,3 @@
(define (odd? (n : Nat))
(not (even? n)))
(module+ test
(check-equal?
(even? z)
true)
(check-equal?
(even? (s z))
false)
(check-equal?
(even? (s (s z)))
true)
(check-equal?
(odd? z)
false)
(check-equal?
(odd? (s z))
true)
(check-equal?
(odd? (s (s z)))
false)
#;(check-equal?
(odd? (s (s (s z))))
true))

42
stdlib/prop.rkt → cur-lib/cur/stdlib/prop.rkt
View File

@ -15,17 +15,11 @@
thm:proj2 pf:proj2
== refl)
(module+ test
(require rackunit))
(data True : Type (T : True))
(define thm:anything-implies-true (forall (P : Type) True))
(define pf:anything-implies-true (lambda (P : Type) T))
(module+ test
(:: pf:anything-implies-true thm:anything-implies-true))
(data False : Type)
(define-type (Not (A : Type)) (-> A False))
@ -51,9 +45,6 @@
(And Q P))
((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
(module+ test
(:: pf:and-is-symmetric thm:and-is-symmetric))
(define thm:proj1
(forall* (A : Type) (B : Type) (c : (And A B)) A))
@ -63,9 +54,6 @@
(lambda* (A : Type) (B : Type) (c : (And A B)) A)
((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
(module+ test
(:: pf:proj1 thm:proj1))
(define thm:proj2
(forall* (A : Type) (B : Type) (c : (And A B)) B))
@ -75,9 +63,6 @@
(lambda* (A : Type) (B : Type) (c : (And A B)) B)
((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
(module+ test
(:: pf:proj2 thm:proj2))
#| TODO: Disabled until #22 fixed
(data Or : (forall* (A : Type) (B : Type) Type)
(left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
@ -100,30 +85,3 @@
(data == : (forall* (A : Type) (x : A) (-> A Type))
(refl : (forall* (A : Type) (x : A) (== A x x))))
(module+ test
(require "bool.rkt" "nat.rkt")
(check-equal?
(elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
(λ* (A : Type) (x : A) z)
Bool
true
true
(refl Bool true))
z)
(check-equal?
(conj/i (conj/i T T) T)
(conj (And True True) True (conj True True T T) T))
(define (id (A : Type) (x : A)) x)
(check-equal?
((id (== True T T))
(refl True (run (id True T))))
(refl True T))
(check-equal?
((id (== True T T))
(refl True (id True T)))
(refl True T)))

50
stdlib/sugar.rkt → cur-lib/cur/stdlib/sugar.rkt
View File

@ -249,53 +249,3 @@
(printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
;; Void is undocumented and a hack, but sort of works
#'(void))]))
(module+ test
(require rackunit (submod ".."))
(check-equal?
((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
(let ([x Type]
[y (λ (x : (Type 1)) x)])
(y x))
Type)
(check-equal?
(let ([(x : (Type 1)) Type]
[y (λ (x : (Type 1)) x)])
(y x))
Type)
;; check that raises decent syntax error
;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
#;(check-exn
exn:fail:syntax?
(let ([x : (Type 1) Type]
[y (λ (x : (Type 1)) x)])
(y x)))
;; check that raises type error
#;(check-exn
exn:fail:syntax?
(let ([x uninferrable-expr]
[y (λ (x : (Type 1)) x)])
(y x)))
)

0
stdlib/tactics/base.rkt → cur-lib/cur/stdlib/tactics/base.rkt
View File

8
stdlib/tactics/sartactics.rkt → cur-lib/cur/stdlib/tactics/sartactics.rkt
View File

@ -124,11 +124,3 @@
(loop (apply (lookup-tactic #'tactic)
(append (syntax->list #'(arg ...)) (list ps)))
(cons cmd cmds)))]))))
(module+ test
(require
rackunit
"../bool.rkt")
(define-theorem meow (forall (x : Bool) Bool))
#;(proof (interactive))
)

28
stdlib/tactics/standard.rkt → cur-lib/cur/stdlib/tactics/standard.rkt
View File

@ -98,31 +98,3 @@
;; Open interactive REPL for tactic DSL; exit with QED command, which
;; returns a QED script
;(define-syntax interactive-proof)
(module+ test
(require
rackunit
"../bool.rkt")
(define-theorem meow (forall (x : Bool) Bool))
(proof
(intro x)
(by-assumption))
(define-theorem meow1 (forall (x : Bool) Bool))
(proof
(obvious)
;; TODO: Add ability to check output
#;(print))
(define-theorem meow2 (forall (x : Bool) Bool))
(proof
(intro x)
(restart)
(intro x)
(by-assumption))
(define-theorem meow3 (forall (x : Bool) Bool))
(proof (obvious))
;; TODO: Fix this unit test so it doesn't require interaction
(define-theorem meow4 (forall (x : Bool) Bool))
#;(proof (interactive))
;; TODO: Add check-cur-equal? for unit testing?
#;(check-pred (curry cur-equal? '(lambda (x : bool) x)))
)

24
stdlib/typeclass.rkt → cur-lib/cur/stdlib/typeclass.rkt
View File

@ -71,27 +71,3 @@
#'body))
#`(define #,(format-id syn "~a-~a" name #'param)
#,body))))]))
(module+ test
(require rackunit)
(typeclass (Eqv (A : Type))
(equal? : (forall* (a : A) (b : A) Bool)))
(impl (Eqv Bool)
(define (equal? (a : Bool) (b : Bool))
(if a
(if b true false)
(if b false true))))
(impl (Eqv Nat)
(define equal? nat-equal?))
(check-equal?
(equal? z z)
true)
(check-equal?
(equal? z (s z))
false)
(check-equal?
(equal? true false)
false)
(check-equal?
(equal? true true)
true))

7
cur-lib/info.rkt Normal file
View File

@ -0,0 +1,7 @@
#lang info
(define collection 'multi)
(define deps '("base" ("redex-lib" #:version "1.11")))
(define build-deps '())
(define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
(define version "0.2")
(define pkg-authors '(wilbowma))

85
cur-test/cur/tests/oll.rkt Normal file
View File

@ -0,0 +1,85 @@
#lang cur
;; NB TODO: raco test reports incorrect number of total tests due to
;; beign-for-syntax; but all failing tests correctly raise errors
(require
rackunit
cur/stdlib/sugar
cur/oll)
(begin-for-syntax
(require rackunit)
(define (check-id-equal? v1 v2)
(check-equal?
(syntax->datum v1)
(syntax->datum v2)))
(define (check-id-match? v1 v2)
(check-regexp-match
v1
(symbol->string (syntax->datum v2))))
(check-id-match?
#px"term\\d+"
(fresh-name #'term))
(check-id-equal?
#'stlc-lambda
(new-name #'stlc #'lambda))
(check-id-match?
#px"stlc-term\\d+"
(new-name #'stlc (fresh-name #'term))))
(begin-for-syntax
(check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
(output-latex-bnf #'(x)
#'((term (e) ::= (e1 e2) (lambda (x) e)))))
(check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
(output-latex-bnf #'(x)
#'((type (A B C) ::= unit (* A B) (+ A C))))))
(check-equal?
(var-equal? (avar z) (avar z))
true)
(check-equal?
(var-equal? (avar z) (avar (s z)))
false)
(begin-for-syntax
(check-equal?
(parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
(format "Inductive nat : Type :=~n| z : nat.~n"))
(check-regexp-match
"(forall .+ : Type, Type)"
(output-coq #'(-> Type Type)))
(let ([t (parameterize ([coq-defns ""])
(output-coq #'(define-relation (meow gamma term type)
[(g : gamma) (e : term) (t : type)
--------------- T-Bla
(meow g e t)]))
(coq-defns))])
(check-regexp-match
"Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
(first (string-split t "\n")))
(check-regexp-match
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
(second (string-split t "\n"))))
(let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
(lambda* (x : nat) (ih-x : nat) ih-x)
e))])
(check-regexp-match
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
t))
(check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
(parameterize ([coq-defns ""])
(output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
(== nat (plus n m) (plus m n)))))
(coq-defns)))
(check-regexp-match
"Function add1 \\(n : nat\\) := \\(s n\\).\n"
(parameterize ([coq-defns ""])
(output-coq #'(define (add1 (n : nat)) (s n)))
(coq-defns))))

658
cur-test/cur/tests/redex-core.rkt Normal file
View File

@ -0,0 +1,658 @@
#lang racket/base
(require
redex/reduction-semantics
cur/curnel/redex-core
rackunit
racket/function
(only-in racket/set set=?))
(define-syntax-rule (check-holds (e ...))
(check-true
(judgment-holds (e ...))))
(define-syntax-rule (check-not-holds (e ...))
(check-false
(judgment-holds (e ...))))
(define-syntax-rule (check-equiv? e1 e2)
(check (default-equiv) e1 e2))
(define-syntax-rule (check-not-equiv? e1 e2)
(check (compose not (default-equiv)) e1 e2))
(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
;; Syntax tests
;; ------------------------------------------------------------------------
(define-term Type (Unv 0))
(check-true (x? (term T)))
(check-true (x? (term A)))
(check-true (x? (term truth)))
(check-true (x? (term zero)))
(check-true (x? (term s)))
(check-true (t? (term zero)))
(check-true (t? (term s)))
(check-true (x? (term nat)))
(check-true (t? (term nat)))
(check-true (t? (term A)))
(check-true (t? (term S)))
(check-true (U? (term (Unv 0))))
(check-true (U? (term Type)))
(check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
;; TODO: Rename these signatures, and use them in all future tests.
(define Δ (term ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat)))))
(bool : (Unv 0) ((true : bool) (false : bool))))))
(define Δ0 (term ∅))
(define Δ3 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ()))))
(define Δ4 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))))))
(check-true (Δ? Δ0))
(check-true (Δ? Δ))
(check-true (Δ? Δ4))
(check-true (Δ? Δ3))
(check-true (Δ? Δ4))
(define sigma (term ((((((∅ (true : (Unv 0) ((T : true))))
(false : (Unv 0) ()))
(equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
()))
(nat : (Unv 0) ()))
(heap : (Unv 0) ()))
(pre : (Π (temp808 : heap) (Unv 0)) ()))))
(check-true (Δ? (term (∅ (true : (Unv 0) ((T : true)))))))
(check-true (Δ? (term (∅ (false : (Unv 0) ())))))
(check-true (Δ? (term (∅ (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
())))))
(check-true (Δ? (term (∅ (nat : (Unv 0) ())))))
(check-true (Δ? (term (∅ (pre : (Π (temp808 : heap) (Unv 0)) ())))))
(check-true (Δ? (term ((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ())))))
(check-true (Δ? (term (((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ()))
(equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
())))))
(check-true (Δ? sigma))
(check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
;; α-equiv and subst tests
;; ------------------------------------------------------------------------
(check-true
(term
(α-equivalent?
(Π (a : S) (Π (b : B) ((and S) B)))
(subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
;; Various accessor tests
;; ------------------------------------------------------------------------
(check-equal?
(term (Δ-key-by-constructor ,Δ zero))
(term nat))
(check-equal?
(term (Δ-key-by-constructor ,Δ s))
(term nat))
(check-equal?
(term (Δ-ref-constructor-map ,Δ nat))
(term ((zero : nat) (s : (Π (x : nat) nat)))))
(check-equal?
(term (Δ-ref-constructor-map ,sigma false))
(term ()))
;; Telescope tests
;; ------------------------------------------------------------------------
;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
(define (telescope-equiv x y)
(alpha-equivalent? ttL (term (in-hole ,x (Unv 0))) (term (in-hole ,y (Unv 0)))))
(define-syntax-rule (check-telescope-equiv? e1 e2)
(check telescope-equiv e1 e2))
(define-syntax-rule (check-telescope-not-equiv? e1 e2)
(check (compose not telescope-equiv) e1 e2))
(check-telescope-equiv?
(term (Δ-ref-parameter-Ξ ,Δ nat))
(term hole))
(check-telescope-equiv?
(term (Δ-ref-parameter-Ξ ,Δ4 and))
(term (Π (A : Type) (Π (B : Type) hole))))
(check-telescope-equiv?
(term (Ξ-compose
(Π (x : t_0) (Π (y : t_1) hole))
(Π (z : t_2) (Π (a : t_3) hole))))
(term (Π (x : t_0) (Π (y : t_1) (Π (z : t_2) (Π (a : t_3) hole))))))
(check-telescope-equiv?
(term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
(term (Π (m-zero : ((λ (x : nat) nat) zero))
(Π (m-s : (Π (x : nat) (Π (x-ih : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole))))
(check-telescope-equiv?
(term (Δ-methods-telescope ,Δ nat P))
(term (Π (m-zero : (P zero))
(Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
hole))))
(check-telescope-equiv?
(term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
(term (Π (m-zero : ((λ (x : nat) nat) zero))
(Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x)))))
hole))))
(check-telescope-equiv?
(term (Δ-methods-telescope ,Δ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))
(term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
((((λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
A)
B)
((((conj A) B) a) b)))))))
hole)))
(check-true (x? (term false)))
(check-true (Ξ? (term hole)))
(check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
(check-true (redex-match? ttL ((x : t) ...) (term ())))
(check-telescope-equiv?
(term (Δ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
(term hole))
;; Tests for inductive elimination
;; ------------------------------------------------------------------------
;; TODO: Insufficient tests, no tests of inductives with parameters, or complex induction.
(check-true
(redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
(check-telescope-equiv?
(term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(hole zero)))
(term (hole (((((elim nat Type) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero))))
(check-telescope-equiv?
(term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(hole (s zero))))
(term (hole (((((elim nat Type) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(s zero)))))
;; Tests for dynamic semantics
;; ------------------------------------------------------------------------
(check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (v? (term (refl Nat))))
(check-true (v? (term ((refl Nat) z))))
;; TODO: Move equivalence up here, and use in these tests.
(check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
(check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
(check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
(term (Π (x : t) (Unv 0))))
(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
(term (Π (x : t) (x x))))
(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat)
(s (s x)))))
zero)))
(term (s zero)))
(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat)
(s (s x)))))
(s zero))))
(term (s (s zero))))
(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(s (s (s zero))))))
(term (s (s (s (s zero))))))
(check-equiv?
(term (reduce ,Δ
(((((elim nat Type) (λ (x : nat) nat))
(s (s zero)))
(λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s (s zero)))))
(term (s (s (s (s zero))))))
(check-equiv?
(term (step ,Δ
(((((elim nat Type) (λ (x : nat) nat))
(s (s zero)))
(λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s (s zero)))))
(term
(((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
(s zero))
(((((elim nat Type) (λ (x : nat) nat))
(s (s zero)))
(λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s zero)))))
(check-equiv?
(term (step ,Δ (step ,Δ
(((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
(s zero))
(((((elim nat Type) (λ (x : nat) nat))
(s (s zero)))
(λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s zero))))))
(term
((λ (ih-x1 : nat) (s ih-x1))
(((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
zero)
(((((elim nat Type) (λ (x : nat) nat))
(s (s zero)))
(λ (x : nat) (λ (ih-x : nat) (s ih-x))))
zero)))))
(define-syntax-rule (check-equivalent e1 e2)
(check-holds (equivalent ∅ e1 e2)))
(check-equivalent
(λ (x : Type) x) (λ (y : Type) y))
(check-equivalent
(Π (x : Type) x) (Π (y : Type) y))
;; Test static semantics
;; ------------------------------------------------------------------------
(check-true (term (positive* nat (nat))))
(check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
(check-true (term (positive* nat ((Π (x : nat) nat)))))
;; (nat -> nat) -> nat
;; Not sure if this is actually supposed to pass
(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
;; ((Unv 0) -> nat) -> nat
(check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
;; (((nat -> (Unv 0)) -> nat) -> nat)
(check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
;; Not sure if this is actually supposed to pass
;; ((nat -> nat) -> nat) -> nat
(check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))))
(check-true (judgment-holds (wf ,Δ0 ∅)))
(check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
(check-true (redex-match? tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
(term (Π (x : nat) nat))))
(define (bindings-equal? l1 l2)
(map set=? l1 l2))
(check-pred
(curry bindings-equal?
(list (list
(make-bind 'Ξ (term (Π (x : nat) hole)))
(make-bind 'Φ (term hole))
(make-bind 'Θ (term hole)))
(list
(make-bind 'Ξ (term hole))
(make-bind 'Φ (term (Π (x : nat) hole)))
(make-bind 'Θ (term hole)))))
(map match-bindings (redex-match tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
(term (Π (x : nat) nat)))))
(check-pred
(curry bindings-equal?
(list
(list
(make-bind 'Φ (term (Π (x : nat) hole)))
(make-bind 'Θ (term hole)))))
(map match-bindings (redex-match tt-redL (in-hole hole (in-hole Φ (in-hole Θ nat)))
(term (Π (x : nat) nat)))))
(check-true
(redex-match? tt-redL
(in-hole hole (in-hole hole (in-hole hole nat)))
(term nat)))
(check-true
(redex-match? tt-redL
(in-hole hole (in-hole (Π (x : nat) hole) (in-hole hole nat)))
(term (Π (x : nat) nat))))
(check-holds (wf (∅ (nat : (Unv 0) ())) ∅))
(check-holds (wf ,Δ0 ∅))
(check-holds (type-infer ∅ ∅ (Unv 0) U))
(check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
(check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
(check-holds
(wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
(check-holds
(wf (∅ (nat : (Unv 0) ((s : (Π (x : nat) nat))))) ∅))
(check-holds (wf ,Δ ∅))
(check-holds (wf ,Δ3 ∅))
(check-holds (wf ,Δ4 ∅))
(check-holds (wf (∅ (truth : (Unv 0) ())) ∅))
(check-holds (wf ∅ (∅ x : (Unv 0))))
(check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : nat)))
(check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : (Π (x : nat) nat))))
(check-holds (type-infer ∅ ∅ (Unv 0) (Unv 1)))
(check-holds (type-infer ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))
(check-holds (type-infer ∅ (∅ x : (Unv 0)) x (Unv 0)))
(check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
(Π (x_3 : x_0) x_1) (Unv 0)))
(check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) x_0 U_1))
(check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))
(check-holds (unv-pred (Unv 0) (Unv 0) (Unv 0)))
(check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
(check-holds (type-check ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
(check-holds (type-check ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
(Π (y : (Unv 0)) (Π (x : y) y))))
(check-equal? (list (term (Unv 1)))
(judgment-holds
(type-infer ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
U)
U))
;; ---- Elim
;; TODO: Clean up/Reorganize these tests
(check-true
(redex-match? tt-typingL
(in-hole Θ_m (((elim x_D U) e_D) e_P))
(term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
(define Δtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
(check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
(check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
(check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
(in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
(check-telescope-equiv?
(term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
(term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
(check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
∅
((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
T)
(Unv 1)))
(check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
∅
((((elim truth (Unv 1)) Type) Type) T)
(Unv 1)))
(check-holds
(type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
(check-holds
(type-infer ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
t))
(check-holds
(type-infer ,Δ ∅ nat (in-hole Ξ U)))
(check-holds
(type-infer ,Δ ∅ zero (in-hole Θ_ai nat)))
(check-holds
(type-infer ,Δ ∅ (λ (x : nat) nat)
(in-hole Ξ (Π (x : (in-hole Θ nat)) U))))
(define-syntax-rule (nat-test syn ...)
(check-holds (type-check ,Δ syn ...)))
(nat-test ∅ (Π (x : nat) nat) (Unv 0))
(nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
(λ (x : nat) (λ (ih-x : nat) x))) zero)
nat)
(nat-test ∅ nat (Unv 0))
(nat-test ∅ zero nat)
(nat-test ∅ s (Π (x : nat) nat))
(nat-test ∅ (s zero) nat)
;; TODO: Meta-function auto-currying and such
(check-holds
(type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
zero)
(λ (x : nat) (λ (ih-x : nat) x)))
t))
(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
zero)
(λ (x : nat) (λ (ih-x : nat) x)))
zero)
nat)
(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero)
nat)
(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
(s zero))
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
nat)
(nat-test (∅ n : nat)
(((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
nat)
(check-holds
(type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
(∅ n2 : nat)
(((((elim nat (Unv 0)) (λ (x : nat) bool))
btrue)
(λ (x : nat) (λ (ih-x : bool) bfalse)))
n2)
bool))
(check-not-holds
(type-check ,Δ ∅
((((elim nat (Unv 0)) nat) (s zero)) zero)
nat))
(define lam (term (λ (nat : (Unv 0)) nat)))
(check-equivalent
(Π (nat : (Unv 0)) (Unv 0))
,(car (judgment-holds (type-infer ,Δ0 ∅ ,lam t) t)))
(check-equivalent
(Π (nat : (Unv 0)) (Unv 0))
,(car (judgment-holds (type-infer ,Δ ∅ ,lam t) t)))
(check-equivalent
(Π (x : (Π (y : (Unv 0)) y)) nat)
,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
t) t)))
(check-equivalent
(Π (y : (Unv 0)) (Unv 0))
,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t)))
(check-equivalent
(Unv 0)
,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
(λ (y : (Unv 0)) y))
t) t)))
(check-equal?
(list (term (Unv 0)) (term (Unv 1)))
(judgment-holds
(type-infer ,Δ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
U) U))
(check-holds
(type-check ,Δ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
(check-holds
(type-check ,Δ4 (∅ S : (Unv 0))
conj (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : P) (Π (y : Q) ((and P) Q)))))))
(check-holds
(type-check ,Δ4 (∅ S : (Unv 0)) S (Unv 0)))
(check-holds
(type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
(Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
(check-holds
(type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
(Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
(check-holds
(type-check ,Δ4 ∅ (λ (S : (Unv 0)) (conj S))
(Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
(check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
((((conj true) true) tt) tt)
((and true) true)))
(check-holds
(type-infer ,Δ4 ∅ and (in-hole Ξ U_D)))
(check-holds
(type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
((((conj true) true) tt) tt)
(in-hole Θ and)))
(check-holds
(type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
(in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
(check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
((((((elim and (Unv 0))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
true))))
(λ (A : (Unv 0))
(λ (B : (Unv 0))
(λ (a : A)
(λ (b : B) tt)))))
true) true)
((((conj true) true) tt) tt))
true))
(check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
(check-holds
(type-infer ,Δ4 ∅ and (in-hole Ξ U)))
(check-holds
(type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
ab (in-hole Θ and)))
(check-true
(redex-match? tt-redL
(in-hole Ξ (Π (x : (in-hole Θ and)) U))
(term (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))))))
(check-holds
(type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A))))
(in-hole Ξ (Π (x : (in-hole Θ and)) U))))
(check-holds
(equivalent ,Δ4
(Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
(Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
(check-holds
(type-infer ,Δ4 ∅
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A))))
(in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
(check-holds
(type-check ,Δ4
(((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
((((((elim and (Unv 0))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A)))))
(λ (A : (Unv 0))
(λ (B : (Unv 0))
(λ (a : A)
(λ (b : B) ((((conj B) A) b) a))))))
P) Q) ab)
((and Q) P)))
(check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))
(Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))))
(check-holds
(type-infer (,Δ4 (true : (Unv 0) ((tt : true))))
((∅ A : Type) B : Type)
(conj B)
t))
(check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
((((((elim and (Unv 0))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A)))))
(λ (A : (Unv 0))
(λ (B : (Unv 0))
(λ (a : A)
(λ (b : B) ((((conj B) A) b) a))))))
true) true)
((((conj true) true) tt) tt))
((and true) true)))
(define gamma (term (∅ temp863 : pre)))
(check-holds (wf ,sigma ∅))
(check-holds (wf ,sigma ,gamma))
(check-holds
(type-infer ,sigma ,gamma (Unv 0) t))
(check-holds
(type-infer ,sigma ,gamma pre t))
(check-holds
(type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
(check-holds
(type-infer ,sigma ,gamma pre t))
(check-holds
(type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
(check-holds
(type-infer ,sigma (,gamma x : false) false (in-hole Ξ U_D)))
(check-holds
(type-infer ,sigma (,gamma x : false) x (in-hole Θ false)))
(check-holds
(type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
(in-hole Ξ (Π (x : (in-hole Θ false)) U))))
(check-true
(redex-match? tt-typingL
((in-hole Θ_m ((elim x_D U) e_P)) e_D)
(term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x)))
x))))
(check-holds
(type-check ,sigma (,gamma x : false)
(((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
(Π (x : (Unv 0)) x)))
;; nat-equal? tests
(define zero?
(term ((((elim nat Type) (λ (x : nat) bool))
true)
(λ (x : nat) (λ (x_ih : bool) false)))))
(check-holds
(type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
(check-equal?
(term (reduce ,Δ (,zero? zero)))
(term true))
(check-equal?
(term (reduce ,Δ (,zero? (s zero))))
(term false))
(define ih-equal?
(term ((((elim nat Type) (λ (x : nat) bool))
false)
(λ (x : nat) (λ (y : bool) (x_ih x))))))
(check-holds
(type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
,ih-equal?
(Π (x : nat) bool)))
(check-holds
(type-infer ,Δ ∅ nat (Unv 0)))
(check-holds
(type-infer ,Δ ∅ bool (Unv 0)))
(check-holds
(type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
(define nat-equal?
(term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
,zero?)
(λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
,ih-equal?)))))
(check-holds
(type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
((nat-equal? zero) zero)
bool))
(check-holds
(type-check ,Δ ∅
,nat-equal?
(Π (x : nat) (Π (y : nat) bool))))
(check-equal?
(term (reduce ,Δ ((,nat-equal? zero) (s zero))))
(term false))
(check-equal?
(term (reduce ,Δ ((,nat-equal? (s zero)) zero)))
(term false))
;; == tests
(define Δ= (term (,Δ (== : (Π (A : (Unv 0)) (Π (a : A) (Π (b : A) (Unv 0))))
((refl : (Π (A : (Unv 0)) (Π (a : A) (((== A) a) a)))))))))
(check-true (Δ? Δ=))
(define refl-elim
(term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
A1)
x1)
y1))
nat)))))
(λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
(check-holds
(type-check ,Δ= ∅ ,refl-elim nat))
(check-true
(redex-match?
tt-redL
(Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
(term (,Δ= ,refl-elim))))
(check-true
(redex-match?
tt-redL
(in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
(term (((((hole
(λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
(check-telescope-equiv?
(term (Δ-ref-parameter-Ξ ,Δ= ==))
(term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
(check-equal?
(term (reduce ,Δ= ,refl-elim))
(term zero))

18
cur-test/cur/tests/stdlib/bool.rkt Normal file
View File

@ -0,0 +1,18 @@
#lang cur
(require
rackunit
cur/stdlib/bool
cur/stdlib/sugar)
(check-equal? (not true) false)
(check-equal? (not false) true)
(check-equal? (and true false) false)
(check-equal? (and false false) true)
(check-equal? (and false true) false)
(check-equal? (and true true) true)
(check-equal? (or true false) true)
(check-equal? (or false false) false)
(check-equal? (or false true) true)
(check-equal? (or true true) true)

21
cur-test/cur/tests/stdlib/maybe.rkt Normal file
View File

@ -0,0 +1,21 @@
#lang cur
(require
rackunit
cur/stdlib/sugar
cur/stdlib/bool
cur/stdlib/maybe)
(check-equal?
(some/i true)
(some Bool true))
;; Disabled until #22 fixed
#;(check-equal?
(case* Maybe Type (some Bool true) (Bool)
(lambda* (A : Type) (x : (Maybe A)) A)
[(none (A : Type)) IH: ()
false]
[(some (A : Type) (x : A)) IH: ()
;; TODO: Don't know how to use dependency yet
(if x true false)])
true)

32
cur-test/cur/tests/stdlib/nat.rkt Normal file
View File

@ -0,0 +1,32 @@
#lang cur
(require
cur/stdlib/sugar
cur/stdlib/nat
cur/stdlib/bool
rackunit)
(check-equal? (add1 (s z)) (s (s z)))
(check-equal? (sub1 (s z)) z)
(check-equal? (plus z z) z)
(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z)))))
(check-equal? (mult (s (s z)) z) z)
(check-equal? (mult (s (s z)) (s z)) (s (s z)))
;; TODO Disabled due to performance bugs
#;(check-equal? (exp z z) (s z))
#;(check-equal? (exp (s z) z) z)
#;(check-equal? (square (s (s z))) (s (s (s (s z)))))
(check-equal? (nat-equal? z z) true)
(check-equal? (nat-equal? z (s z)) false)
(check-equal? (nat-equal? (s z) (s z)) true)
(check-equal? (even? z) true)
(check-equal? (even? (s z)) false)
(check-equal? (even? (s (s z))) true)
(check-equal? (odd? z) false)
(check-equal? (odd? (s z)) true)
(check-equal? (odd? (s (s z))) false)
(check-equal? (odd? (s (s (s z)))) true)

36
cur-test/cur/tests/stdlib/prop.rkt Normal file
View File

@ -0,0 +1,36 @@
#lang cur
(require
cur/stdlib/prop
cur/stdlib/sugar
cur/stdlib/bool
cur/stdlib/nat
rackunit)
(:: pf:anything-implies-true thm:anything-implies-true)
(:: pf:and-is-symmetric thm:and-is-symmetric)
(:: pf:proj1 thm:proj1)
(:: pf:proj2 thm:proj2)
(check-equal?
(elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
(λ* (A : Type) (x : A) z)
Bool
true
true
(refl Bool true))
z)
(check-equal?
(conj/i (conj/i T T) T)
(conj (And True True) True (conj True True T T) T))
(define (id (A : Type) (x : A)) x)
(check-equal?
((id (== True T T))
(refl True (run (id True T))))
(refl True T))
(check-equal?
((id (== True T T))
(refl True (id True T)))
(refl True T))

12
cur-test/cur/tests/stdlib/sartactics.rkt Normal file
View File

@ -0,0 +1,12 @@
#lang cur
(require
rackunit
cur/stdlib/bool
cur/stdlib/sugar
cur/stdlib/tactics/base
cur/stdlib/tactics/sartactics)
;; TODO: To much randomness for easy automated testing
(define-theorem meow (forall (x : Bool) Bool))
#;(proof (interactive))

51
cur-test/cur/tests/stdlib/sugar.rkt Normal file
View File

@ -0,0 +1,51 @@
#lang cur
(require
rackunit
cur/stdlib/sugar)
;; TODO: Missing tests for match, others
(check-equal?
((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
(let ([x Type]
[y (λ (x : (Type 1)) x)])
(y x))
Type)
(check-equal?
(let ([(x : (Type 1)) Type]
[y (λ (x : (Type 1)) x)])
(y x))
Type)
;; check that raises decent syntax error
;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
#;(check-exn
exn:fail:syntax?
(let ([x : (Type 1) Type]
[y (λ (x : (Type 1)) x)])
(y x)))
;; check that raises type error
#;(check-exn
exn:fail:syntax?
(let ([x uninferrable-expr]
[y (λ (x : (Type 1)) x)])
(y x)))

36
cur-test/cur/tests/stdlib/tactics.rkt Normal file
View File

@ -0,0 +1,36 @@
#lang cur
(require
rackunit
cur/stdlib/sugar
cur/stdlib/bool
cur/stdlib/tactics/base
cur/stdlib/tactics/standard)
(define-theorem meow (forall (x : Bool) Bool))
(check-equal?
((proof
(intro x)
(by-assumption)) true)
true)
(define-theorem meow1 (forall (x : Bool) Bool))
(check-equal?
((proof
(obvious)
;; TODO: Add ability to check output
#;(print)) true)
true)
(define-theorem meow2 (forall (x : Bool) Bool))
(check-equal?
((proof
(intro x)
(restart)
(intro x)
(by-assumption)) true)
true)
(define-theorem meow3 (forall (x : Bool) Bool))
(check-equal?
((proof (obvious)) true)
true)
;; TODO: Fix this unit test so it doesn't require interaction
(define-theorem meow4 (forall (x : Bool) Bool))
#;(proof (interactive))

30
cur-test/cur/tests/stdlib/typeclass.rkt Normal file
View File

@ -0,0 +1,30 @@
#lang cur
(require
rackunit
cur/stdlib/sugar
cur/stdlib/bool
cur/stdlib/nat
cur/stdlib/typeclass)
(typeclass (Eqv (A : Type))
(equal? : (forall* (a : A) (b : A) Bool)))
(impl (Eqv Bool)
(define (equal? (a : Bool) (b : Bool))
(if a
(if b true false)
(if b false true))))
(impl (Eqv Nat)
(define equal? nat-equal?))
(check-equal?
(equal? z z)
true)
(check-equal?
(equal? z (s z))
false)
(check-equal?
(equal? true false)
false)
(check-equal?
(equal? true true)
true)

47
examples/stlc.rkt → cur-test/cur/tests/stlc.rkt
View File

@ -1,18 +1,19 @@
#lang s-exp "../cur.rkt"
#lang cur
(require
"../stdlib/nat.rkt"
"../stdlib/sugar.rkt"
"../oll.rkt"
"../stdlib/maybe.rkt"
"../stdlib/bool.rkt"
"../stdlib/prop.rkt")
rackunit
cur/stdlib/nat
cur/stdlib/sugar
cur/oll
cur/stdlib/maybe
cur/stdlib/bool
cur/stdlib/prop)
(define-language stlc
#:vars (x)
#:output-coq "stlc.v"
#:output-latex "stlc.tex"
(val (v) ::= true false unit)
;; TODO: Allow datum as terminals
;; TODO: Allow datum, like 1, as terminals
(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)))
@ -126,19 +127,17 @@
#'stlc-unitty
#'e)])))
(module+ test
(require rackunit)
(check-equal?
(begin-stlc (lambda (x : 1) x))
(stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
(check-equal?
(begin-stlc ((lambda (x : 1) x) ()))
(stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
(stlc-val-->-stlc-term stlc-unit)))
(check-equal?
(begin-stlc '(() ()))
(stlc-cons (stlc-val-->-stlc-term stlc-unit)
(stlc-val-->-stlc-term stlc-unit)))
(check-equal?
(begin-stlc #t)
(stlc-val-->-stlc-term stlc-true)))
(check-equal?
(begin-stlc (lambda (x : 1) x))
(stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
(check-equal?
(begin-stlc ((lambda (x : 1) x) ()))
(stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
(stlc-val-->-stlc-term stlc-unit)))
(check-equal?
(begin-stlc '(() ()))
(stlc-cons (stlc-val-->-stlc-term stlc-unit)
(stlc-val-->-stlc-term stlc-unit)))
(check-equal?
(begin-stlc #t)
(stlc-val-->-stlc-term stlc-true))

7
cur-test/info.rkt Normal file
View File

@ -0,0 +1,7 @@
#lang info
(define collection 'multi)
(define deps '())
(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
(define update-implies '("cur-lib"))
(define pkg-desc "Tests for \"cur\".")
(define pkg-authors '(wilbowma))

6
cur/info.rkt Normal file
View File

@ -0,0 +1,6 @@
#lang info
(define collection 'multi)
(define deps '("cur-lib" "cur-doc" "cur-test"))
(define implies '("cur-lib" "cur-doc" "cur-test"))
(define pkg-desc "Dependent types with parenthesis and meta-programming.")
(define pkg-authors '(wilbowma))

1245
curnel/redex-core.rkt
View File

File diff suppressed because it is too large Load Diff

8
info.rkt
View File

@ -1,8 +0,0 @@
#lang info
(define collection "cur")
(define deps '("base" "rackunit-lib" ("redex-lib" #:version "1.11")))
(define build-deps '("scribble-lib" "racket-doc" "sandbox-lib"))
(define scribblings '(("scribblings/cur.scrbl" (multi-page))))
(define pkg-desc "Dependent types with parenthesis and meta-programming.")
(define version "0.1")
(define pkg-authors '(wilbowma))

41
stdlib/bool.rkt
View File

@ -1,41 +0,0 @@
#lang s-exp "../cur.rkt"
(require "sugar.rkt")
(provide Bool true false if not and or)
(data Bool : Type
(true : Bool)
(false : Bool))
(define-syntax-rule (if t s f)
(match t
[true s]
[false f]))
(define (not (x : Bool)) (if x false true))
(module+ test
(require rackunit)
(check-equal? (not true) false)
(check-equal? (not false) true))
(define (and (x : Bool) (y : Bool))
(if x
y
(not y)))
(module+ test
(check-equal? (and true false) false)
(check-equal? (and false false) true)
(check-equal? (and false true) false)
(check-equal? (and true true) true))
(define (or (x : Bool) (y : Bool))
(if x
true
y))
(module+ test
(check-equal? (or true false) true)
(check-equal? (or false false) false)
(check-equal? (or false true) true)
(check-equal? (or true true) true))

29
stdlib/maybe.rkt
View File

@ -1,29 +0,0 @@
#lang s-exp "../cur.rkt"
(require "sugar.rkt")
(provide Maybe none some some/i)
(data Maybe : (forall (A : Type) Type)
(none : (forall (A : Type) (Maybe A)))
(some : (forall* (A : Type) (a : A) (Maybe A))))
(define-syntax (some/i syn)
(syntax-case syn ()
[(_ a)
(let ([a-ty (type-infer/syn #'a)])
#`(some #,a-ty a))]))
(module+ test
(require rackunit "bool.rkt")
(check-equal?
(some/i true)
(some Bool true))
;; Disabled until #22 fixed
#;(check-equal?
(case* Maybe Type (some Bool true) (Bool)
(lambda* (A : Type) (x : (Maybe A)) A)
[(none (A : Type)) IH: ()
false]
[(some (A : Type) (x : A)) IH: ()
;; TODO: Don't know how to use dependency yet
(if x true false)])
true))