[UNTESTED] Splitting and reorganizing packages
* Created split packages: cur-lib, cur-test, cur-doc, similar to other Racket packages. * Added info.rkt files to all packages * Moved tests out of core and into cur-test * Moved docs into cur-doc * Moved cur implementation into cur-lib
This commit is contained in:
William J. Bowman
parent
647229a577
commit
ea3dd97265
|
|
@ -1,6 +1,6 @@
|
|||
#lang scribble/manual
|
||||
@(require
|
||||
"defs.rkt"
|
||||
"scribbling/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{scribbling/curnel.scrbl}
|
||||
@include-section{scribbling/reflection.scrbl}
|
||||
@include-section{scribbling/stdlib.scrbl}
|
||||
@include-section{scribbling/oll.scrbl}
|
||||
2
cur-doc/cur/info.rkt
Normal file
2
cur-doc/cur/info.rkt
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
#lang info
|
||||
(define scribblings '(("cur.scrbl" (multi-page))))
|
||||
6
cur-doc/info.rkt
Normal file
6
cur-doc/info.rkt
Normal 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))
|
||||
590
cur-lib/cur/curnel/redex-core.rkt
Normal file
590
cur-lib/cur/curnel/redex-core.rkt
Normal 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)])
|
||||
7
cur-lib/info.rkt
Normal file
7
cur-lib/info.rkt
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
#lang info
|
||||
(define collection 'multi)
|
||||
(define deps '("base" ("redex-lib" #:version "1.11")))
|
||||
(define build-deps '())
|
||||
(define pkg-desc "Dependent types with parenthesis and meta-programming.")
|
||||
(define version "0.2")
|
||||
(define pkg-authors '(wilbowma))
|
||||
659
cur-test/cur/tests/core-tests.rkt
Normal file
659
cur-test/cur/tests/core-tests.rkt
Normal file
|
|
@ -0,0 +1,659 @@
|
|||
#lang racket/base
|
||||
|
||||
(require
|
||||
redex/reduction-semantics
|
||||
cur/curnel/redex-core
|
||||
rackunit
|
||||
(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))
|
||||
6
cur-test/info.rkt
Normal file
6
cur-test/info.rkt
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
#lang info
|
||||
(define collection 'multi)
|
||||
(define deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
|
||||
(define build-deps '())
|
||||
(define pkg-desc "Tests for \"cur\".")
|
||||
(define pkg-authors '(wilbowma))
|
||||
File diff suppressed because it is too large
Load Diff
8
info.rkt
8
info.rkt
|
|
@ -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))
|
||||
Loading…
Reference in New Issue
Block a user