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

NB, API changes: Faster/more primitive elim

Browse Source 
This commit breaks previous API for eliminating inductive types.

The previous eliminator for inductive types was too complex. It performed
automagic currying, making it difficult to type check, and difficult and
expensive to reduce.

The new version must be fully applied, and magic should be implemented
in the surface language. A sketch of such magic is left in sugar.rkt,
but not yet implemented.

This new version gives a 40% speed up on the Cur test
suite. Unfortunately, Redex is still the major bottleneck, so no
algorithmic gains.
This commit is contained in:
William J. Bowman 2016-03-23 15:01:02 -04:00
parent 185cc71c62
commit 832b7be5db
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
17 changed files with 377 additions and 481 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
cur-doc/cur/scribblings/curnel.scrbl
View File

@ -17,7 +17,7 @@ Edwin C. Brady.
@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)")) @(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)"))
@defform*[((Type n) @defform*[((Type n)
Type)]{ Type)]{
Define the universe of types at level @racket[n], where @racket[n] is any natural number. Define the universe of types at level @racket[n], where @racket[n] is any natural number.
@racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative @racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative
in @racket[(Type 0)], although this is likely to change to a more in @racket[(Type 0)], although this is likely to change to a more
@ -91,13 +91,16 @@ For instance, Cur does not currently perform strict positivity checking.
((((conj Bool) Bool) true) false)] ((((conj Bool) Bool) true) false)]
} }
@defform[(elim type motive-universe)]{ @defform[(elim inductive-type motive (index ...) (method ...) disc)]{
Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
of the motive. The @racket[motive] is a function that expects the indices of the inductive
The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for type and a term of the inductive type and produces the type that this
each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments fold returns.
to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to The type of @racket[disc] is @racket[(inductive-type index ...)].
eliminate of type @racket[(type p_0 ... p_P)]. @racket[elim] takes one method for each constructor of @racket[inductive-type].
Each @racket[method] expects the arguments for its corresponding constructor,
and the inductive hypotheses generated by recursively eliminating all recursive
arguments of the constructor.
The following example runs @racket[(sub1 (s z))]. The following example runs @racket[(sub1 (s z))].
@ -105,11 +108,11 @@ The following example runs @racket[(sub1 (s z))].
(data Nat : Type (data Nat : Type
(z : Nat) (z : Nat)
(s : (Π (n : Nat) Nat))) (s : (Π (n : Nat) Nat)))
(((((elim Nat Type) (elim Nat (λ (x : Nat) Nat)
(λ (x : Nat) Nat)) ()
z) (z
(λ (n : Nat) (λ (IH : Nat) n))) (λ (n : Nat) (λ (IH : Nat) n)))
(s z))] (s z))]
} }
@defform[(define id expr)]{ @defform[(define id expr)]{
@ -120,9 +123,11 @@ Binds @racket[id] to the result of @racket[expr].
(z : Nat) (z : Nat)
(s : (Π (n : Nat) Nat))) (s : (Π (n : Nat) Nat)))
(define sub1 (λ (n : Nat) (define sub1 (λ (n : Nat)
(((((elim Nat Type) (λ (x : Nat) Nat)) (elim Nat (λ (x : Nat) Nat)
z) ()
(λ (n : Nat) (λ (IH : Nat) n))) n))) (z
(λ (n : Nat) (λ (IH : Nat) n)))
n)))
(sub1 (s (s z))) (sub1 (s (s z)))
(sub1 (s z)) (sub1 (s z))
(sub1 z)] (sub1 z)]

8
cur-doc/cur/scribblings/reflection.scrbl
View File

@ -76,10 +76,10 @@ Runs the Cur term @racket[syn] for one step.
(eval:alts (cur-step #'((λ (x : Type) x) Bool)) (eval:alts (cur-step #'((λ (x : Type) x) Bool))
(eval:result @racket[#'Bool] "" "")) (eval:result @racket[#'Bool] "" ""))
(eval:alts (cur-step #'(sub1 (s (s z)))) (eval:alts (cur-step #'(sub1 (s (s z))))
(eval:result @racket[#'(((((elim Nat (Type 0)) (eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat)
(λ (x2 : Nat) Nat)) z) ()
(λ (x2 : Nat) (λ (ih-n2 : Nat) x2))) (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
(s (s z)))] "" "")) (s (s z)))] "" ""))
] ]
} }

2
cur-doc/cur/scribblings/stdlib/bool.scrbl
View File

@ -22,7 +22,7 @@ A syntactic form that expands to the inductive eliminator for @racket[Bool]. Thi
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(if true false true) (if true false true)
(elim Bool Type (λ (x : Bool) Bool) false true true)] (elim Bool (λ (x : Bool) Bool) () (false true) true)]
} }
@defproc[(not [x Bool]) @defproc[(not [x Bool])

11
cur-doc/cur/scribblings/stdlib/sugar.scrbl
View File

@ -82,17 +82,6 @@ a @racket[(: name type)] form appears earlier in the module.
(define (id A a) a)] (define (id A a) a)]
} }
@defform[(elim type motive-result-type e ...)]{
Like the @racket[elim] provided by @racketmodname[cur], but supports
automatically curries the remaining arguments @racket[e ...].
@examples[#:eval curnel-eval
(elim Bool Type (lambda (x : Bool) Bool)
false
true
true)]
}
@defform*[((define-type name type) @defform*[((define-type name type)
(define-type (name (a : t) ...) body))]{ (define-type (name (a : t) ...) body))]{
Like @racket[define], but uses @racket[forall] instead of @racket[lambda]. Like @racket[define], but uses @racket[forall] instead of @racket[lambda].

2
cur-doc/info.rkt
View File

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

303
cur-lib/cur/curnel/redex-core.rkt
View File

@ -27,10 +27,10 @@
(i j k ::= natural) (i j k ::= natural)
(U ::= (Unv i)) (U ::= (Unv i))
(D x c ::= variable-not-otherwise-mentioned) (D x c ::= variable-not-otherwise-mentioned)
(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 : t ((c : t) ...))))
(t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
;; (elim inductive-type motive (indices ...) (methods ...) discriminant)
(elim D e (e ...) (e ...) e))
#:binding-forms #:binding-forms
(λ (x : t) e #:refers-to x) (λ (x : t) e #:refers-to x)
(Π (x : t_0) t_1 #:refers-to x)) (Π (x : t_0) t_1 #:refers-to x))
@ -108,27 +108,6 @@
[(Δ-union Δ_2 (Δ_1 (x : t any))) [(Δ-union Δ_2 (Δ_1 (x : t any)))
((Δ-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 or #f
[(Δ-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)]
[(Δ-key-by-constructor Δ x)
#f])
;; 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 ;; TODO: Should not use Δ-ref-type
(define-metafunction ttL (define-metafunction ttL
Δ-ref-constructor-type : Δ x x -> t Δ-ref-constructor-type : Δ x x -> t
@ -148,14 +127,6 @@
;; TODO: Mix of pure Redex/escaping to Racket sometimes is getting confusing. ;; TODO: Mix of pure Redex/escaping to Racket sometimes is getting confusing.
;; TODO: Justify, or stop. ;; TODO: Justify, or stop.
;; Return the number of constructors that D has
(define-metafunction ttL
Δ-constructor-count : Δ D -> natural or #f
[(Δ-constructor-count Δ D)
,(length (term (x ...)))
(where (x ...) (Δ-ref-constructors Δ D))]
[(Δ-constructor-count Δ D) #f])
;; NB: Depends on clause order ;; NB: Depends on clause order
(define-metafunction ttL (define-metafunction ttL
sequence-index-of : any (any ...) -> natural sequence-index-of : any (any ...) -> natural
@ -200,39 +171,23 @@
[(Ξ-apply hole t) t] [(Ξ-apply hole t) t]
[(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))]) [(Ξ-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 Ξ ;; Compute the number of arguments in a Ξ
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
Ξ-length : Ξ -> natural Ξ-length : Ξ -> natural
[(Ξ-length hole) 0] [(Ξ-length hole) 0]
[(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))]) [(Ξ-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 Θ)))])
;; Convert an apply context to a sequence of terms
(define-metafunction tt-ctxtL
Θ->list : Θ -> (e ...)
[(Θ->list hole) ()]
[(Θ->list (Θ e))
(e_r ... e)
(where (e_r ...) (Θ->list Θ))])
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
list->Θ : (e ...) -> Θ list->Θ : (e ...) -> Θ
[(list->Θ ()) hole] [(list->Θ ()) hole]
[(list->Θ (e e_r ...)) [(list->Θ (e e_r ...))
(in-hole (list->Θ (e_r ...)) (hole e))]) (in-hole (list->Θ (e_r ...)) (hole e))])
(define-metafunction tt-ctxtL
apply : e e ... -> e
[(apply e_f e ...)
(in-hole (list->Θ (e ...)) e_f)])
;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole. ;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
Θ-ref : Θ natural -> e or #f Θ-ref : Θ natural -> e or #f
@ -254,15 +209,6 @@
[(Δ-ref-parameter-Ξ Δ x) [(Δ-ref-parameter-Ξ Δ x)
#f]) #f])
;; Return the number of parameters of D
(define-metafunction tt-ctxtL
Δ-parameter-count : Δ D -> natural or #f
[(Δ-parameter-count Δ D)
(Ξ-length Ξ)
(where Ξ (Δ-ref-parameter-Ξ Δ D))]
[(Δ-parameter-count Δ D)
#f])
;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D ;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
Δ-constructor-telescope : Δ x x -> Ξ Δ-constructor-telescope : Δ x x -> Ξ
@ -280,21 +226,6 @@
(where (in-hole Ξ (in-hole Θ x_D)) (where (in-hole Ξ (in-hole Θ x_D))
(Δ-ref-constructor-type Δ x_D x_ci))]) (Δ-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 ;; Inner loop for Δ-constructor-inductive-telescope
;; NB: Depends on clause order ;; NB: Depends on clause order
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
@ -323,36 +254,6 @@
(hypotheses-loop x_D t_P Φ_1)) (hypotheses-loop x_D t_P Φ_1))
(where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))]) (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 ;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
;; is in universe U. ;; is in universe U.
;; ;;
@ -368,29 +269,40 @@
;; Ξ_P*D is the telescope of the parameters of x_D and ;; Ξ_P*D is the telescope of the parameters of x_D and
;; the witness of type x_D (applied to the parameters) ;; the witness of type x_D (applied to the parameters)
;; Ξ_m is the telescope of the methods for x_D ;; Ξ_m is the telescope of the methods for x_D
;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
;; inductive type D, when eliminating with motive t_P.
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
Δ-elim-type : Δ x U -> t Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
[(Δ-elim-type Δ x_D U) [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
(Π (x_P : (in-hole Ξ_P*D U)) (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
;; The methods Ξ_m for each constructor of type x_D
(in-hole Ξ_m ;; Returns the type of the method corresponding to c_i
;; And finally, the parameters and discriminant (define-metafunction tt-ctxtL
(in-hole Ξ_P*D Δ-constructor-method-type : Δ D c t -> t
;; The result is (P a ... (x_D a ...)), i.e., the motive [(Δ-constructor-method-type Δ D c_i t_P)
;; applied to the paramters and discriminant (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i))))
(Ξ-apply Ξ_P*D x_P)))) (where Θ_p (Δ-constructor-parameters Δ D c_i))
;; Get the parameters of x_D (where Ξ_a (Δ-constructor-telescope Δ D c_i))
(where Ξ (Δ-ref-parameter-Ξ Δ x_D)) (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
(define-metafunction tt-ctxtL
Δ-method-types : Δ D e -> (t ...)
[(Δ-method-types Δ D e)
,(map (lambda (c) (term (Δ-constructor-method-type Δ D ,c e))) (term (c ...)))
(where (c ...) (Δ-ref-constructors Δ D))])
(define-metafunction tt-ctxtL
Δ-motive-type : Δ D U -> t
[(Δ-motive-type Δ D U)
(in-hole Ξ_P*D U)
(where Ξ (Δ-ref-parameter-Ξ Δ D))
;; A fresh name to bind the discriminant ;; A fresh name to bind the discriminant
(where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D)) (where x ,(variable-not-in (term (Δ D Ξ)) 'x-D))
;; The telescope (∀ a -> ... -> (D a ...) hole), i.e., ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
;; of the parameters and the inductive type applied to the ;; of the indices and the inductive type applied to the
;; parameters ;; indices
(where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole))) (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ 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))])
;;; ------------------------------------------------------------------------ ;;; ------------------------------------------------------------------------
;;; Dynamic semantics ;;; Dynamic semantics
@ -398,16 +310,21 @@
;;; inductively defined type x with a motive whose result is in universe U ;;; inductively defined type x with a motive whose result is in universe U
(define-extended-language tt-redL tt-ctxtL (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, (v ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
;; determining whether or not it is partially applied cannot be done with the grammar alone. (Θv ::= hole (Θv v))
(v ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U))) (C-elim ::= (elim D t_P (e_i ...) (e_m ...) hole))
(Θv ::= hole (Θv v)) ;; call-by-value
;; call-by-value, plus reduce under Π (helps with typing checking) (E ::= hole (E e) (v E)
(E ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e))) (elim D e (e ...) (v ... E e ...) e)
(elim D e (e ...) (v ...) E)
;; reduce under Π (helps with typing checking)
;; TODO: Should be done in conversion judgment
(Π (x : v) E) (Π (x : E) e)))
(define Θv? (redex-match? tt-redL Θv)) (define Θv? (redex-match? tt-redL Θv))
(define E? (redex-match? tt-redL E)) (define E? (redex-match? tt-redL E))
(define v? (redex-match? tt-redL v)) (define v? (redex-match? tt-redL v))
#| #|
| The elim form must appear applied like so: | The elim form must appear applied like so:
| (elim D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...)) | (elim D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
@ -423,75 +340,6 @@
| |
| Using contexts, this appears as (in-hole Θ ((elim D U) v_P)) | Using contexts, this appears as (in-hole Θ ((elim D U) v_P))
|# |#
;;; NB: Next 3 meta-function Assume of Θ n constructors, j parameters, n+j+1-th element is discriminant
;; Given the apply context Θ in which an elimination of D with motive
;; v of type U appears, extract the parameters p ... from Θ.
(define-metafunction tt-redL
elim-parameters : Δ D Θ -> Θ
[(elim-parameters Δ D Θ)
;; Drop the methods, take the parameters
(list->Θ
,(take
(drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
(term (Δ-parameter-count Δ D))))])
;; Given the apply context Θ in which an elimination of D with motive
;; v of type U appears, extract the methods m_0 ... m_n from Θ.
(define-metafunction tt-redL
elim-methods : Δ D Θ -> Θ
[(elim-methods Δ D Θ)
;; Take the methods, one for each constructor
(list->Θ
,(take
(term (Θ->list Θ))
(term (Δ-constructor-count Δ D))))])
;; Given the apply context Θ in which an elimination of D with motive
;; v of type U appears, extract the discriminant (c_i a ...) from Θ.
(define-metafunction tt-redL
elim-discriminant : Δ D Θ -> e
[(elim-discriminant Δ D Θ)
;; Drop the methods, the parameters, and take the last element
,(car
(drop
(drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
(term (Δ-parameter-count Δ D))))])
;; Check that Θ is valid and ready to be evaluated as the arguments to an elim.
;; has length m = n + j + 1 and D has n constructors and j parameters,
;; and the 1 represents the discriminant.
;; discharges assumption for previous 3 meta-functions
(define-metafunction tt-redL
Θ-valid : Δ D Θ -> #t or #f
[(Θ-valid Δ D Θ)
#t
(where natural_m (Θ-length Θ))
(where natural_n (Δ-constructor-count Δ D))
(where natural_j (Δ-parameter-count Δ D))
(side-condition (= (+ (term natural_n) (term natural_j) 1) (term natural_m)))
;; As Cur allows reducing (through reflection) open terms,
;; check that the discriminant is a canonical form so that
;; reduction can proceed; otherwise not valid.
(where (in-hole Θ_i c_i) (elim-discriminant Δ D Θ))
(where D (Δ-key-by-constructor Δ c_i))]
[(Θ-valid Δ D Θ) #f])
(module+ test
(require rackunit)
(check-equal?
(term (Θ-length (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))
3)
(check-true
(term
(Θ-valid
((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat))))) (bool : (Unv 0) ((true : bool) (false : bool))))
nat
(((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))))
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
is-inductive-argument : Δ D t -> #t or #f is-inductive-argument : Δ D t -> #t or #f
;; Think this only works in call-by-value. A better solution would ;; Think this only works in call-by-value. A better solution would
@ -505,39 +353,34 @@
;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i, ;; 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) ;; generate: (elim x_D U t_P Θ_m ... Θ_p ... t_i)
;; TODO TTEESSSSSTTTTTTTT ;; TODO TTEESSSSSTTTTTTTT
(define-metafunction tt-ctxtL (define-metafunction tt-redL
Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ Δ-inductive-elim : Δ D C-elim Θ -> Θ
;; NB: If metafunction fails, recursive ;; NB: If metafunction fails, recursive
;; NB: elimination will be wrong. This will introduced extremely sublte bugs, ;; NB: elimination will be wrong. This will introduced extremely sublte bugs,
;; NB: inconsistency, failure of type safety, and other bad things. ;; NB: inconsistency, failure of type safety, and other bad things.
;; NB: It should be tested and audited thoroughly ;; NB: It should be tested and audited thoroughly
[(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i)) [(Δ-inductive-elim any ... hole)
((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i) hole]
(in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P))) [(Δ-inductive-elim Δ D C-elim (Θ_c t_i))
(side-condition (term (is-inductive-argument Δ x_D t_i)))] ((Δ-inductive-elim Δ D C-elim Θ_c)
[(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i)) (in-hole C-elim t_i))
(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)] (side-condition (term (is-inductive-argument Δ D t_i)))]
[(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m hole) [(Δ-inductive-elim any ... (Θ_c t_i))
hole]) (Δ-inductive-elim any ... Θ_c)])
(define tt--> (define tt-->
(reduction-relation tt-redL (reduction-relation tt-redL
(--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2))) (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
(Δ (in-hole E (subst t_1 x t_2))) (Δ (in-hole E (subst t_1 x t_2)))
-->β) -->β)
(--> (Δ (in-hole E (in-hole Θv ((elim D U) v_P)))) (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
(Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi)))) (Δ (in-hole E (in-hole Θ_mi v_mi)))
;; Check that Θv is valid to avoid capturing other things ;; Find the method for constructor c_i, relying on the order of the arguments.
(side-condition (term (Θ-valid Δ D Θv))) (where natural (Δ-constructor-index Δ D c))
;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
;; the discriminant: the constructor c_i applied to its argument Θv_i
(where Θv_p (elim-parameters Δ D Θv))
(where Θv_m (elim-methods Δ D Θv))
(where (in-hole Θv_i c_i) (elim-discriminant Δ D Θv))
;; Find the method for constructor x_ci, relying on the order of the arguments.
(where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ D c_i)))
;; Generate the inductive recursion ;; Generate the inductive recursion
(where Θ_r (Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i)) (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
(where Θ_mi (in-hole Θ_ih Θv_c))
-->elim))) -->elim)))
(define-metafunction tt-redL (define-metafunction tt-redL
@ -698,10 +541,16 @@
----------------- "DTR-Application" ----------------- "DTR-Application"
(type-infer Δ Γ (e_0 e_1) t_3)] (type-infer Δ Γ (e_0 e_1) t_3)]
[(where t (Δ-elim-type Δ D U)) [(type-check Δ Γ e_c (apply D e_i ...))
(type-infer Δ Γ t U_e)
(type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
(convert Δ Γ t_motive (Δ-motive-type Δ D U))
(where (t_m ...) (Δ-method-types Δ D e_motive))
(type-check Δ Γ e_m t_m) ...
----------------- "DTR-Elim_D" ----------------- "DTR-Elim_D"
(type-infer Δ Γ (elim D U) t)]) (type-infer Δ Γ (elim D e_motive (e_i ...) (e_m ...) e_c)
(apply e_motive e_i ... e_c))])
(define-judgment-form tt-typingL (define-judgment-form tt-typingL
#:mode (type-check I I I I) #:mode (type-check I I I I)

17
cur-lib/cur/curnel/redex-lang.rkt
View File

@ -2,7 +2,7 @@
;; This module just provide module language sugar over the redex model. ;; This module just provide module language sugar over the redex model.
(require (require
"redex-core.rkt" (except-in "redex-core.rkt" apply)
redex/reduction-semantics redex/reduction-semantics
racket/provide-syntax racket/provide-syntax
(for-syntax (for-syntax
@ -11,7 +11,7 @@
racket/syntax racket/syntax
(except-in racket/provide-transform export) (except-in racket/provide-transform export)
racket/require-transform racket/require-transform
"redex-core.rkt" (except-in "redex-core.rkt" apply)
redex/reduction-semantics)) redex/reduction-semantics))
(provide (provide
;; Basic syntax ;; Basic syntax
@ -177,10 +177,11 @@
[e (parameterize ([gamma (extend-Γ/term gamma x t)]) [e (parameterize ([gamma (extend-Γ/term gamma x t)])
(cur->datum #'e))]) (cur->datum #'e))])
(term (,(syntax->datum #'b) (,x : ,t) ,e)))] (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
[(elim t1 t2) [(elim D motive (i ...) (m ...) d)
(let* ([t1 (cur->datum #'t1)] (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
[t2 (cur->datum #'t2)]) ,(map cur->datum (syntax->list #'(i ...)))
(term (elim ,t1 ,t2)))] ,(map cur->datum (syntax->list #'(m ...)))
,(cur->datum #'d)))]
[(#%app e1 e2) [(#%app e1 e2)
(term (,(cur->datum #'e1) ,(cur->datum #'e2)))])))) (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
(unless (or (inner-expand?) (type-infer/term reified-term)) (unless (or (inner-expand?) (type-infer/term reified-term))
@ -446,9 +447,9 @@
(define-syntax (dep-elim syn) (define-syntax (dep-elim syn)
(syntax-parse syn (syntax-parse syn
[(_ D:id T) [(_ D:id motive (i ...) (m ...) e)
(syntax->curnel-syntax (syntax->curnel-syntax
(quasisyntax/loc syn (elim D T)))])) (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
(define-syntax-rule (dep-void) (void)) (define-syntax-rule (dep-void) (void))

14
cur-lib/cur/olly.rkt
View File

@ -95,8 +95,18 @@
(cur->coq #'t))])))) (cur->coq #'t))]))))
"")] "")]
[(Type i) "Type"] [(Type i) "Type"]
[(real-elim var t) [(real-elim var:id motive (i ...) (m ...) d)
(format "~a_rect" (cur->coq #'var))] (format
"(~a_rect ~a~a~a ~a)"
(cur->coq #'var)
(cur->coq #'motive)
(for/fold ([strs ""])
([m (syntax->list #'(m ...))])
(format "~a ~a" strs (cur->coq m)))
(for/fold ([strs ""])
([i (syntax->list #'(i ...))])
(format "~a ~a" strs (cur->coq i)))
(cur->coq #'d))]
[(real-app e1 e2) [(real-app e1 e2)
(format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))] (format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))]))) [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))

11
cur-lib/cur/stdlib/prop.rkt
View File

@ -71,11 +71,12 @@
(define proof:A-or-A (define proof:A-or-A
(lambda (A : Type) (c : (Or A A)) (lambda (A : Type) (c : (Or A A))
;; TODO: What should the motive be? ;; TODO: What should the motive be?
(elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A) (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
(lambda (A : Type) (B : Type) (a : A) a) (A A)
;; TODO: How do we know B is A? ((lambda (A : Type) (B : Type) (a : A) a)
(lambda (A : Type) (B : Type) (b : B) b) ;; TODO: How do we know B is A?
A A c))) (lambda (A : Type) (B : Type) (b : B) b))
c)))
(qed thm:A-or-A proof:A-or-A) (qed thm:A-or-A proof:A-or-A)
|# |#

75
cur-lib/cur/stdlib/sugar.rkt
View File

@ -12,7 +12,6 @@
#%app #%app
define define
: :
elim
define-type define-type
match match
recur recur
@ -29,7 +28,6 @@
(require (require
(only-in "../main.rkt" (only-in "../main.rkt"
[elim real-elim]
[#%app real-app] [#%app real-app]
[λ real-lambda] [λ real-lambda]
[Π real-Π] [Π real-Π]
@ -163,8 +161,67 @@
(quasisyntax/loc syn (quasisyntax/loc syn
(real-define id body))])) (real-define id body))]))
(define-syntax-rule (elim t1 t2 e ...) #|
((real-elim t1 t2) e ...)) (begin-for-syntax
(define (type->telescope syn)
(syntax-parse (cur-expand syn)
#:literals (real-Π)
#:datum-literals (:)
[(real-Π (x:id : t) body)
(cons #'(x : t) (type->telescope #'body))]
[_ '()]))
(define (type->body syn)
(syntax-parse syn
#:literals (real-Π)
#:datum-literals (:)
[(real-Π (x:id : t) body)
(type->body #'body)]
[e #'e]))
(define (constructor-indices D syn)
(let loop ([syn syn]
[args '()])
(syntax-parse (cur-expand syn)
#:literals (real-app)
[D:id args]
[(real-app e1 e2)
(loop #'e1 (cons #'e2 args))])))
(define (inductive-index-telescope D)
(type->telescope (cur-type-infer D)))
(define (inductive-method-telescope D motive)
(for/list ([syn (cur-constructor-map D)])
(with-syntax ([(c : t) syn]
[name (gensym (format-symbol "~a-~a" #'c 'method))]
[((arg : arg-type) ...) (type->telescope #'t)]
[((rarg : rarg-type) ...) (constructor-recursive-args D #'((arg : arg-type) ...))]
[((ih : ih-type) ...) (constructor-inductive-hypotheses #'((rarg : rarg-type) ...) motive)]
[(iarg ...) (constructor-indices D (type->body #'t))]
)
#`(name : (forall (arg : arg-type) ...
(ih : ih-type) ...
(motive iarg ...)))))))
(define-syntax (elim syn)
(syntax-parse syn
[(elim D:id U e ...)
(with-syntax ([((x : t) ...) (inductive-index-telescope #'D)]
[motive (gensym 'motive)]
[y (gensym 'y)]
[disc (gensym 'disc)]
[((method : method-type) ...) (inductive-method-telescope #'D #'motive)])
#`((lambda
(motive : (forall (x : t) ... (y : (D x ...)) U))
(method : ) ...
(x : t) ...
(disc : (D x ...)) ...
(real-elim D motive (x ...) (method ...) disc))
e ...)
)
]))
|#
;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive" ;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
(begin-for-syntax (begin-for-syntax
@ -366,15 +423,9 @@
(quasisyntax/loc syn (quasisyntax/loc syn
(elim (elim
D.inductive-name D.inductive-name
#,(or
(cur-type-infer (attribute return-type))
(raise-syntax-error
'match
"Could not infer type of motive. Sorry, you'll have to use elim."
syn))
motive motive
c.method ... #,(attribute D.indices)
#,@(attribute D.indices) (c.method ...)
d))])) d))]))
(begin-for-syntax (begin-for-syntax

2
cur-lib/info.rkt
View File

@ -3,5 +3,5 @@
(define deps '("base" ("redex-lib" #:version "1.11"))) (define deps '("base" ("redex-lib" #:version "1.11")))
(define build-deps '()) (define build-deps '())
(define pkg-desc "implementation (no documentation, tests) part of \"cur\".") (define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
(define version "0.3") (define version "0.4")
(define pkg-authors '(wilbowma)) (define pkg-authors '(wilbowma))

7
cur-test/cur/tests/olly.rkt
View File

@ -41,11 +41,12 @@
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\." "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
(second (string-split t "\n")))) (second (string-split t "\n"))))
(let ([t (cur->coq (let ([t (cur->coq
#'(elim nat Type (lambda (x : nat) nat) z #'(elim nat (lambda (x : nat) nat)
(lambda (x : nat) (ih-x : nat) ih-x) ()
(z (lambda (x : nat) (ih-x : nat) ih-x))
e))]) e))])
(check-regexp-match (check-regexp-match
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)" "\\(nat_rect \\(fun x : nat => nat\\) z \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\) e\\)"
t)) t))
(check-regexp-match (check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n" "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"

343
cur-test/cur/tests/redex-core.rkt
View File

@ -81,23 +81,6 @@
(Π (a : S) (Π (b : B) ((and S) B))) (Π (a : S) (Π (b : B) ((and S) B)))
(subst (Π (a : A) (Π (b : B) ((and A) B))) A S)))) (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 ;; Telescope tests
;; ------------------------------------------------------------------------ ;; ------------------------------------------------------------------------
;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed ;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
@ -115,41 +98,10 @@
(term (Δ-ref-parameter-Ξ ,Δ4 and)) (term (Δ-ref-parameter-Ξ ,Δ4 and))
(term (Π (A : Type) (Π (B : Type) hole)))) (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 (x? (term false)))
(check-true (Ξ? (term hole))) (check-true (Ξ? (term hole)))
(check-true (t? (term (λ (y : false) (Π (x : Type) x))))) (check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
(check-true (redex-match? ttL ((x : t) ...) (term ()))) (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 ;; Tests for inductive elimination
;; ------------------------------------------------------------------------ ;; ------------------------------------------------------------------------
@ -157,21 +109,32 @@
(check-true (check-true
(redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero)))) (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
(check-telescope-equiv? (check-telescope-equiv?
(term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole (term (Δ-inductive-elim ,Δ nat
((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (elim nat (λ (x : nat) nat) ()
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
hole)
(hole zero))) (hole zero)))
(term (hole (((((elim nat Type) (λ (x : nat) nat)) (term (hole (elim nat (λ (x : nat) nat)
(s zero)) ()
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) ((s zero)
zero)))) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero))))
(check-telescope-equiv? (check-telescope-equiv?
(term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole (term (Δ-inductive-elim ,Δ nat
((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (elim nat (λ (x : nat) nat) ()
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
hole)
(hole (s zero)))) (hole (s zero))))
(term (hole (((((elim nat Type) (λ (x : nat) nat)) (term (hole (elim nat (λ (x : nat) nat) ()
(s zero)) ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) (s zero)))))
(s zero))))) (check-telescope-equiv?
(term (Δ-inductive-elim ,Δ nat
(elim nat (λ (x : nat) nat) ()
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
hole)
hole))
(term hole))
;; Tests for dynamic semantics ;; Tests for dynamic semantics
;; ------------------------------------------------------------------------ ;; ------------------------------------------------------------------------
@ -179,6 +142,8 @@
(check-true (v? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (v? (term (refl Nat)))) (check-true (v? (term (refl Nat))))
(check-true (v? (term ((refl Nat) z)))) (check-true (v? (term ((refl Nat) z))))
(check-true (v? (term zero)))
(check-true (v? (term (s zero))))
;; TODO: Move equivalence up here, and use in these tests. ;; TODO: Move equivalence up here, and use in these tests.
(check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0))) (check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
@ -188,60 +153,68 @@
(term (Π (x : t) (Unv 0)))) (term (Π (x : t) (Unv 0))))
(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x)))) (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
(term (Π (x : t) (x x)))) (term (Π (x : t) (x x))))
(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
(s zero)) (check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
(λ (x : nat) (λ (ih-x : nat) (check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
(s (s x))))) ()
zero))) ((s zero)
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero)))
(term (s zero))) (term (s zero)))
(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat)) (check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
(s zero)) ()
(λ (x : nat) (λ (ih-x : nat) ((s zero)
(s (s x))))) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(s zero)))) (s zero))))
(term (s (s zero)))) (term (s (s zero))))
(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat)) (check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
(s zero)) ()
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) ((s zero)
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
(s (s (s zero)))))) (s (s (s zero))))))
(term (s (s (s (s zero)))))) (term (s (s (s (s zero))))))
(check-equiv? (check-equiv?
(term (reduce ,Δ (term (reduce ,Δ
(((((elim nat Type) (λ (x : nat) nat)) (elim nat (λ (x : nat) nat)
(s (s zero))) ()
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) ((s (s zero))
(s (s zero))))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s (s zero)))))
(term (s (s (s (s zero)))))) (term (s (s (s (s zero))))))
(check-equiv? (check-equiv?
(term (step ,Δ (term (step ,Δ
(((((elim nat Type) (λ (x : nat) nat)) (elim nat (λ (x : nat) nat)
(s (s zero))) ()
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) ((s (s zero))
(s (s zero))))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s (s zero)))))
(term (term
(((λ (x : nat) (λ (ih-x : nat) (s ih-x))) (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
(s zero)) (s zero))
(((((elim nat Type) (λ (x : nat) nat)) (elim nat (λ (x : nat) nat)
(s (s zero))) ()
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) ((s (s zero))
(s zero))))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s zero)))))
(check-equiv? (check-equiv?
(term (step ,Δ (step ,Δ (term (step ,Δ (step ,Δ
(((λ (x : nat) (λ (ih-x : nat) (s ih-x))) (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
(s zero)) (s zero))
(((((elim nat Type) (λ (x : nat) nat)) (elim nat (λ (x : nat) nat)
(s (s zero))) ()
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) ((s (s zero))
(s zero)))))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s zero))))))
(term (term
((λ (ih-x1 : nat) (s ih-x1)) ((λ (ih-x1 : nat) (s ih-x1))
(((λ (x : nat) (λ (ih-x : nat) (s ih-x))) (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
zero) zero)
(((((elim nat Type) (λ (x : nat) nat)) (elim nat (λ (x : nat) nat)
(s (s zero))) ()
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) ((s (s zero))
zero))))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
zero)))))
(define-syntax-rule (check-equivalent e1 e2) (define-syntax-rule (check-equivalent e1 e2)
(check-holds (convert ∅ ∅ e1 e2))) (check-holds (convert ∅ ∅ e1 e2)))
@ -343,28 +316,42 @@
U)) U))
;; ---- Elim ;; ---- Elim
;; TODO: Clean up/Reorganize these tests ;; 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)))))) (define Δtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
(check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U))) (check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
(check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth))) (check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
(check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1)) (check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
(in-hole Ξ (Π (x : (in-hole Θ truth)) U)))) (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
(check-telescope-equiv? (check-equiv?
(term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1)))) (term (Δ-motive-type ,Δtruth truth (Unv 2)))
(term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole))) (term (Π (x : truth) (Unv 2))))
(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
(check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
(check-holds (type-check ,Δtruth ∅ (Unv 0) ,(car (term (Δ-method-types ,Δtruth truth (λ (x : truth) (Unv 1)))))))
(check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
(check-equiv?
(term (apply (λ (x : truth) (Unv 1)) T))
(term ((λ (x : truth) (Unv 1)) T)))
(check-holds
(convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
(check-holds (type-infer ,Δtruth
∅ ∅
((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0)) (elim truth (λ (x : truth) (Unv 1))
T) () ((Unv 0)) T)
t))
(check-holds (type-check ,Δtruth
∅
(elim truth (λ (x : truth) (Unv 1))
() ((Unv 0)) T)
(Unv 1))) (Unv 1)))
(check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth)))) (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
∅ ∅
((((elim truth (Unv 1)) Type) Type) T) (elim truth Type () (Type) T)
(Unv 1))) (Unv 1)))
(check-holds (check-holds
(type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U)) (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
@ -382,47 +369,54 @@
(check-holds (type-check ,Δ syn ...))) (check-holds (type-check ,Δ syn ...)))
(nat-test ∅ (Π (x : nat) nat) (Unv 0)) (nat-test ∅ (Π (x : nat) nat) (Unv 0))
(nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat)) (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero) (nat-test ∅ (elim nat (λ (x : nat) nat) ()
(λ (x : nat) (λ (ih-x : nat) x))) zero) (zero (λ (x : nat) (λ (ih-x : nat) x)))
zero)
nat) nat)
(nat-test ∅ nat (Unv 0)) (nat-test ∅ nat (Unv 0))
(nat-test ∅ zero nat) (nat-test ∅ zero nat)
(nat-test ∅ s (Π (x : nat) nat)) (nat-test ∅ s (Π (x : nat) nat))
(nat-test ∅ (s zero) nat) (nat-test ∅ (s zero) nat)
;; TODO: Meta-function auto-currying and such
(check-holds (check-holds
(type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat)) (type-infer ,Δ ∅ (λ (x : nat)
zero) (elim nat (λ (x : nat) nat)
(λ (x : nat) (λ (ih-x : nat) x))) ()
(zero
(λ (x : nat) (λ (ih-x : nat) x)))
x))
t)) t))
(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat)) (nat-test ∅ (elim nat (λ (x : nat) nat)
zero) ()
(λ (x : nat) (λ (ih-x : nat) x))) (zero (λ (x : nat) (λ (ih-x : nat) x)))
zero) zero)
nat) nat)
(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat)) (nat-test ∅ (elim nat (λ (x : nat) nat)
(s zero)) ()
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero) zero)
nat) nat)
(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) (nat-test ∅ (elim nat (λ (x : nat) nat)
(s zero)) ()
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero) ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero)
nat) nat)
(nat-test (∅ n : nat) (nat-test (∅ n : nat)
(((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n) (elim nat (λ (x : nat) nat)
()
(zero (λ (x : nat) (λ (ih-x : nat) x)))
n)
nat) nat)
(check-holds (check-holds
(type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool)))) (type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
(∅ n2 : nat) (∅ n2 : nat)
(((((elim nat (Unv 0)) (λ (x : nat) bool)) (elim nat (λ (x : nat) bool)
btrue) ()
(λ (x : nat) (λ (ih-x : bool) bfalse))) (btrue (λ (x : nat) (λ (ih-x : bool) bfalse)))
n2) n2)
bool)) bool))
(check-not-holds (check-not-holds
(type-check ,Δ ∅ (type-check ,Δ ∅
((((elim nat (Unv 0)) nat) (s zero)) zero) (elim nat nat () ((s zero)) zero)
nat)) nat))
(define lam (term (λ (nat : (Unv 0)) nat))) (define lam (term (λ (nat : (Unv 0)) nat)))
(check-equivalent (check-equivalent
@ -481,15 +475,15 @@
(in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P)))) (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
(check-holds (check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
((((((elim and (Unv 0)) (elim and
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
true)))) true)))
(λ (A : (Unv 0)) (true true)
(λ (B : (Unv 0)) ((λ (A : (Unv 0))
(λ (a : A) (λ (B : (Unv 0))
(λ (b : B) tt))))) (λ (a : A)
true) true) (λ (b : B) tt)))))
((((conj true) true) tt) tt)) ((((conj true) true) tt) tt))
true)) true))
(check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))))) (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
(check-holds (check-holds
@ -518,14 +512,15 @@
(check-holds (check-holds
(type-check ,Δ4 (type-check ,Δ4
(((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)) (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
((((((elim and (Unv 0)) (elim and
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A))))) ((and B) A))))
(λ (A : (Unv 0)) (P Q)
(λ (B : (Unv 0)) ((λ (A : (Unv 0))
(λ (a : A) (λ (B : (Unv 0))
(λ (b : B) ((((conj B) A) b) a)))))) (λ (a : A)
P) Q) ab) (λ (b : B) ((((conj B) A) b) a))))))
ab)
((and Q) P))) ((and Q) P)))
(check-holds (check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
@ -538,14 +533,14 @@
t)) t))
(check-holds (check-holds
(type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
((((((elim and (Unv 0)) (elim and
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A))))) ((and B) A))))
(λ (A : (Unv 0)) (true true)
((λ (A : (Unv 0))
(λ (B : (Unv 0)) (λ (B : (Unv 0))
(λ (a : A) (λ (a : A)
(λ (b : B) ((((conj B) A) b) a)))))) (λ (b : B) ((((conj B) A) b) a))))))
true) true)
((((conj true) true) tt) tt)) ((((conj true) true) tt) tt))
((and true) true))) ((and true) true)))
(define gamma (term (∅ temp863 : pre))) (define gamma (term (∅ temp863 : pre)))
@ -568,21 +563,18 @@
(check-holds (check-holds
(type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x)) (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
(in-hole Ξ (Π (x : (in-hole Θ false)) U)))) (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 (check-holds
(type-check ,sigma (,gamma x : false) (type-check ,sigma (,gamma x : false)
(((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x) (elim false (λ (y : false) (Π (x : Type) x)) () () x)
(Π (x : (Unv 0)) x))) (Π (x : (Unv 0)) x)))
;; nat-equal? tests ;; nat-equal? tests
(define zero? (define zero?
(term ((((elim nat Type) (λ (x : nat) bool)) (term (λ (n : nat)
true) (elim nat (λ (x : nat) bool) ()
(λ (x : nat) (λ (x_ih : bool) false))))) (true (λ (x : nat) (λ (x_ih : bool) false)))
n))))
(check-holds (check-holds
(type-check ,Δ ∅ ,zero? (Π (x : nat) bool))) (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
(check-equal? (check-equal?
@ -592,9 +584,12 @@
(term (reduce ,Δ (,zero? (s zero)))) (term (reduce ,Δ (,zero? (s zero))))
(term false)) (term false))
(define ih-equal? (define ih-equal?
(term ((((elim nat Type) (λ (x : nat) bool)) (term (λ (ih : nat)
false) (elim nat (λ (x : nat) bool)
(λ (x : nat) (λ (y : bool) (x_ih x)))))) ()
(false
(λ (x : nat) (λ (y : bool) (x_ih x))))
ih))))
(check-holds (check-holds
(type-check ,Δ (∅ x_ih : (Π (x : nat) bool)) (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
,ih-equal? ,ih-equal?
@ -606,10 +601,13 @@
(check-holds (check-holds
(type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0)))) (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
(define nat-equal? (define nat-equal?
(term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool))) (term (λ (n : nat)
,zero?) (elim nat (λ (x : nat) (Π (x : nat) bool))
(λ (x : nat) (λ (x_ih : (Π (x : nat) bool)) ()
,ih-equal?))))) (,zero?
(λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
,ih-equal?)))
n))))
(check-holds (check-holds
(type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»))) (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
((nat-equal? zero) zero) ((nat-equal? zero) zero)
@ -631,19 +629,12 @@
(check-true (Δ? Δ=)) (check-true (Δ? Δ=))
(define refl-elim (define refl-elim
(term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
A1) (bool true true)
x1) ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
y1)) ((refl bool) true))))
nat)))))
(λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
(check-holds (check-holds
(type-check ,Δ= ∅ ,refl-elim nat)) (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 (check-true
(redex-match? (redex-match?
tt-redL tt-redL

10
cur-test/cur/tests/stdlib/list.rkt
View File

@ -32,11 +32,11 @@
(:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A))))) (:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
(check-equal? (check-equal?
(void) (void)
(:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat) (:: (elim List (lambda (A : Type) (ls : (List A)) Nat)
(lambda (A : Type) z) (Bool)
(lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat) ((lambda (A : Type) z)
z) (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
Bool z))
(nil Bool)) (nil Bool))
Nat)) Nat))

10
cur-test/cur/tests/stdlib/prop.rkt
View File

@ -11,11 +11,11 @@
(:: pf:proj1 thm:proj1) (:: pf:proj1 thm:proj1)
(:: pf:proj2 thm:proj2) (:: pf:proj2 thm:proj2)
(check-equal? (check-equal?
(elim == Type (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat) (elim == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
(λ (A : Type) (x : A) z) (Bool
Bool true
true true)
true ((λ (A : Type) (x : A) z))
(refl Bool true)) (refl Bool true))
z) z)

4
cur-test/cur/tests/stdlib/typeclass.rkt
View File

@ -11,9 +11,7 @@
(equal? : (forall (a : A) (b : A) Bool))) (equal? : (forall (a : A) (b : A) Bool)))
(impl (Eqv Bool) (impl (Eqv Bool)
(define (equal? (a : Bool) (b : Bool)) (define (equal? (a : Bool) (b : Bool))
(if a (if a b (not b))))
(if b true false)
(if b false true))))
(impl (Eqv Nat) (impl (Eqv Nat)
(define equal? nat-equal?)) (define equal? nat-equal?))
(check-equal? (check-equal?

2
cur-test/info.rkt
View File

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