Compare commits

..

12 Commits

Author SHA1 Message Date
William J. Bowman
ed57d034dc
Updated documentation 2016-01-18 14:03:42 -05:00
William J. Bowman
c3f5719b30
Removed implementation of case & case* 2016-01-18 14:03:33 -05:00
William J. Bowman
2fcba80950
Fixed use of case*, added TODO about things 2016-01-18 12:10:13 -05:00
William J. Bowman
04619e1f0b
Removed case and case* exports 2016-01-18 11:52:01 -05:00
William J. Bowman
174e4560d1
All tests pass! Sugar simplified 2016-01-18 11:48:51 -05:00
William J. Bowman
d48a5a0647
Advanced match!
Advanced match now works in all stdlib. case and case* deprecated.
2016-01-18 00:22:28 -05:00
William J. Bowman
b52dca0114
[Buggy] Partially fixed match on type familes.
Fixed various application syntax bugs in match.

Match still fails to infer the correct motive on type familes.
This is due to indices being instantiated differently between motive and
match clause.
2016-01-17 17:31:33 -05:00
William J. Bowman
09f47481ab
Fixing redex-lang to aid in debugging 2016-01-17 17:28:57 -05:00
William J. Bowman
ceb2a1aefc
[Untested] Fixed advanced version of match.
Need to start testing/converting stdlib, replacing case and case*
2016-01-15 18:29:10 -05:00
William J. Bowman
6820c07cd1
[Broken?] Advanced match
Right now, there are two pattern-matching-esque constructs.
Match is the better one, but fails often.
Time to improve it via syntax parse, more inferrence, and optional
arguments.

However, currently some of these changes seem to conflict with how the
redex-core works.
2016-01-15 17:14:20 -05:00
William J. Bowman
8d46cbf206
Converted cur-lib to simpler sugar 2016-01-15 17:12:39 -05:00
William J. Bowman
df741faa83
Simplifying the syntax sugar
Right now, the syntax sugar provided by Cur is instructive, but annoying
to use.
Time to make it easier to use.
2016-01-15 16:32:08 -05:00
33 changed files with 1076 additions and 1202 deletions

View File

@ -45,10 +45,6 @@ Try it out: open up DrRacket and put the following in the definition area:
(if true (if true
false false
true) true)
(: + (-> Nat Nat Nat))
(define + plus)
(+ z (s z))
``` ```
Try entering the following in the interaction area: Try entering the following in the interaction area:
@ -56,23 +52,6 @@ Try entering the following in the interaction area:
(sub1 (s (s z))) (sub1 (s (s z)))
``` ```
Don't like parenthesis? Use Cur with sweet-expressions:
```racket
#lang sweet-exp cur
require
cur/stdlib/sugar
cur/stdlib/bool
cur/stdlib/nat
if true
false
true
define + plus
{z + s(z)}
```
See the docs: `raco docs cur`. See the docs: `raco docs cur`.
Going further Going further

View File

@ -33,44 +33,43 @@ restricted impredicative universe.
Type] Type]
} }
@defform[(λ (id : type-expr) body-expr)]{ @defform*[((lambda (id : type-expr) body-expr)
Produces a single-arity procedure, binding the identifier @racket[id] of type (λ (id : type-expr) body-expr))]{
@racket[type-expr] in @racket[body-expr] and in the type of @racket[body-expr]. Produces a single arity procedure, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr] and in the type of
Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, @racket[body-expr].
such as macros. Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, such as macros.
Currently, Cur will return the underlying representation of a procedure when a Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is
@racket[λ] is evaluated at the top-level. evaluated at the top-level. Do not rely on this representation.
Do not rely on this representation.
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(λ (x : Type) x)] (lambda (x : Type) x)]
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(λ (x : Type) (λ (y : x) y))] (λ (x : Type) (lambda (y : x) y))]
@defform[(#%app procedure argument)]{ @defform[(#%app procedure argument)]{
Applies the single-arity @racket[procedure] to @racket[argument]. Applies the single arity @racket[procedure] to @racket[argument].
} }
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
((λ (x : (Type 1)) x) Type)] ((lambda (x : (Type 1)) x) Type)]
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(#%app (λ (x : (Type 1)) x) Type)] (#%app (lambda (x : (Type 1)) x) Type)]
} }
@defform[(Π (id : type-expr) body-expr)]{ @defform*[((forall (id : type-expr) body-expr)
Produces a dependent function type, binding the identifier @racket[id] of type (∀ (id : type-expr) body-expr))]{
@racket[type-expr] in @racket[body-expr]. Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr].
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(Π (x : Type) Type)] (forall (x : Type) Type)]
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(λ (x : (Π (x : (Type 1)) Type)) (lambda (x : (forall (x : (Type 1)) Type))
(x Type))] (x Type))]
} }
@ -84,34 +83,31 @@ For instance, Cur does not currently perform strict positivity checking.
(data Bool : Type (data Bool : Type
(true : Bool) (true : Bool)
(false : Bool)) (false : Bool))
((λ (x : Bool) x) true) ((lambda (x : Bool) x) true)
(data False : Type) (data False : Type)
(data And : (Π (A : Type) (Π (B : Type) Type)) (data And : (forall (A : Type) (forall (B : Type) Type))
(conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B))))))) (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B)))))))
((((conj Bool) Bool) true) false)] ((((conj Bool) Bool) true) false)]
} }
@defform[(elim inductive-type motive (index ...) (method ...) disc)]{ @defform[(elim type motive-universe)]{
Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type]. Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
The @racket[motive] is a function that expects the indices of the inductive of the motive.
type and a term of the inductive type and produces the type that this The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
fold returns. each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
The type of @racket[disc] is @racket[(inductive-type index ...)]. to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
@racket[elim] takes one method for each constructor of @racket[inductive-type]. eliminate of type @racket[(type p_0 ... p_P)].
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))].
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(data Nat : Type (data Nat : Type
(z : Nat) (z : Nat)
(s : (Π (n : Nat) Nat))) (s : (forall (n : Nat) Nat)))
(elim Nat (λ (x : Nat) Nat) (((((elim Nat Type)
() (lambda (x : Nat) Nat))
(z z)
(λ (n : Nat) (λ (IH : Nat) n))) (lambda (n : Nat) (lambda (IH : Nat) n)))
(s z))] (s z))]
} }
@ -121,13 +117,11 @@ Binds @racket[id] to the result of @racket[expr].
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(data Nat : Type (data Nat : Type
(z : Nat) (z : Nat)
(s : (Π (n : Nat) Nat))) (s : (forall (n : Nat) Nat)))
(define sub1 (λ (n : Nat) (define sub1 (lambda (n : Nat)
(elim Nat (λ (x : Nat) Nat) (((((elim Nat Type) (lambda (x : Nat) Nat))
() z)
(z (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
(λ (n : Nat) (λ (IH : Nat) n)))
n)))
(sub1 (s (s z))) (sub1 (s (s z)))
(sub1 (s z)) (sub1 (s z))
(sub1 z)] (sub1 z)]

View File

@ -14,11 +14,11 @@ the language.
maybe-vars maybe-vars
maybe-output-coq maybe-output-coq
maybe-output-latex maybe-output-latex
(nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...) (nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
#:grammar #:grammar
[(maybe-vars [(maybe-vars
(code:line) (code:line)
(code:line #:vars (nt-metavar ...))) (code:line #:vars (nt-metavars ...)))
(maybe-output-coq (maybe-output-coq
(code:line) (code:line)
(code:line #:output-coq coq-filename)) (code:line #:output-coq coq-filename))
@ -27,51 +27,26 @@ the language.
(code:line #:output-latex latex-filename)) (code:line #:output-latex latex-filename))
(maybe-bnfdef (maybe-bnfdef
(code:line) (code:line)
(code:line ::=)) (code:line ::=))]]{
(non-terminal-def
nt-metavar
(code:line terminal)
(code:line (terminal terminal-args ...)))
(terminal-args
nt-metavar
(code:line literal)
(code:line ())
(code:line (#:bind nt-metavar . terminal-args))
(code:line (terminal-args terminal-args ...)))]]{
Defines a new language by generating inductive definitions for each Defines a new language by generating inductive definitions for each
non-terminal @racket[nt-name], whose syntax is generated by nonterminal @racket[nt-name], whose constructors are generated by
@racket[non-terminal-def]. @racket[constructors]. The constructors must either with a tag that can
Each @racket[non-terminal-def] must either be a reference to a be used to name the constructor, or be another meta-variable.
previously defined non-terminal using a @racket[nt-metavar], a The meta-variables @racket[nt-metavars] are replaced by the corresponding
@racket[terminal] (an identifier), or a @racket[terminal] applied to inductive types in @racket[constructors].
some @racket[terminal-args]. The name of each inductive datatype is generated by
The @racket[terminal-args] are a limited grammar of s-expressions, @racket[(format-id "~a-~a" name nt-name)].
which can reference previously defined @racket[nt-metavar]s to be
treated as arguments, literal symbols to be treated as syntax, binding
declarations, or a nested @racket[terminal-arg].
The inductive definitions are generated by generating a type for each Later nonterminals can refer to prior nonterminals, but they cannot be
@racket[nt-name] whose name @racket[nt-type] is generated by mutually inductive due to limitations in Cur. When nonterminals appear
@racket[(format-id name "~a-~a" name nt-name)] and whose constructors in @racket[constructors], a constructor is defined that coerces one
are generated by each @racket[non-terminal-def]. nonterminal to another.
For @racket[terminal]s, the constructor is a base constructor whose
name is generated by @racket[(format-id name "~a-~a" name terminal)].
For @racket[nt-metavar]s, the constructor is a conversion constructor
whose name is generated by @racket[(format-id name "~a->~a" nt-type
nt-metavar-type)] where @racket[nt-metavar-type] is the name of the
type generated for the nonterminal to which @racket[nt-metavars] refers.
For @racket[(terminal terminal-args ...)], the constructor is a
function that expects term of of the types generated by
@racket[terminal-args ...].
If @racket[#:vars] is given, it should be a list of meta-variables that If @racket[#:vars] is given, it should be a list of meta-variables that
representing variables in the language. representing variables in the language. These meta-variables should only
These variables are represented as De Bruijn indices, and uses of appear in binding positions in @racket[constructors]. These variables
variables in the syntax are treated as type @racket[Nat]. are represented as De Bruijn indexes, and Olly provides some functions
Binding positions in the syntax, represented by @racket[#:bind for working with De Bruijn indexes.
nt-metavar], are erased in converting to De Bruijn indices, although
this may change if the representation of variables used by
@racket[define-language] changes.
If @racket[#:output-coq] is given, it should be a string representing a If @racket[#:output-coq] is given, it should be a string representing a
filename. The form @racket[define-language] will output Coq versions of filename. The form @racket[define-language] will output Coq versions of
@ -91,8 +66,8 @@ Example:
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
(val (v) ::= true false unit) (val (v) ::= true false unit)
(type (A B) ::= boolty unitty (-> A B) (* A A)) (type (A B) ::= boolty unitty (-> A B) (* A A))
(term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e) (term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e)
(let (#:bind x #:bind x) = e in e))) (let (x x) = e in e)))
] ]
This example is equivalent to This example is equivalent to
@ -110,17 +85,20 @@ This example is equivalent to
(stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type)))) (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
(data stlc-term : Type (data stlc-term : Type
(Var->-stlc-term : (forall (x : Nat) stlc-term)) (stlc-var-->-stlc-term : (forall (x : Var) stlc-term))
(stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term)) (stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term))
(stlc-term-lambda : (forall (y : stlc-type) (stlc-term-lambda : (forall (x : Var)
(forall (y : stlc-type)
(forall (z : stlc-term) (forall (z : stlc-term)
stlc-term))) stlc-term))))
(stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term))) (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
(stlc-term-let : (forall (e1 : stlc-term) (stlc-term-let : (forall (x : Var)
(forall (y : Var)
(forall (e1 : stlc-term)
(forall (e2 : stlc-term) (forall (e2 : stlc-term)
stlc-term))))] stlc-term))))))]
@margin-note{This example is taken from @racketmodname[cur/tests/stlc]} @margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
} }
@defform[(define-relation (name args ...) @defform[(define-relation (name args ...)
@ -148,20 +126,20 @@ explain the syntax in detail, here is an example:
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
[(g : Gamma) [(g : Gamma)
------------------------ T-Unit ------------------------ T-Unit
(has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)] (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
[(g : Gamma) [(g : Gamma)
------------------------ T-True ------------------------ T-True
(has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)] (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
[(g : Gamma) [(g : Gamma)
------------------------ T-False ------------------------ T-False
(has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)] (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
[(g : Gamma) (x : Nat) (t : stlc-type) [(g : Gamma) (x : Var) (t : stlc-type)
(== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t)) (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
------------------------ T-Var ------------------------ T-Var
(has-type g (Var->stlc-term x) t)] (has-type g (Var-->-stlc-term x) t)]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
@ -173,15 +151,16 @@ explain the syntax in detail, here is an example:
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(t : stlc-type) (t : stlc-type)
(x : Var) (y : Var)
(has-type g e1 (stlc-* t1 t2)) (has-type g e1 (stlc-* t1 t2))
(has-type (extend-gamma (extend-gamma g t1) t2) e2 t) (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
---------------------- T-Let ---------------------- T-Let
(has-type g (stlc-let e1 e2) t)] (has-type g (stlc-let x y e1 e2) t)]
[(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
(has-type (extend-gamma g t1) e1 t2) (has-type (extend-gamma g x t1) e1 t2)
---------------------- T-Fun ---------------------- T-Fun
(has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))] (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
@ -200,11 +179,22 @@ This example is equivalent to:
(T-Unit : (forall (g : Gamma) (T-Unit : (forall (g : Gamma)
(has-type (has-type
g g
(stlc-val->stlc-term stlc-unit) (stlc-val-->-stlc-term stlc-unit)
stlc-unitty))) stlc-unitty)))
....)] ....)]
} }
@deftogether[(@defthing[Var Type]
@defthing[avar (forall (x : Nat) Var)])]{
The type of a De Bruijn variable.
}
@defproc[(var-equal? [v1 Var] [v2 Var])
Bool]{
A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
represent the same variable.
}
@todo{Need a Scribble library for defining Cur/Racket things in the same @todo{Need a Scribble library for defining Cur/Racket things in the same
library in a nice way.} library in a nice way.}

View File

@ -25,60 +25,60 @@ phase 1 in Cur.}
@examples[ @examples[
(eval:alts (define-syntax-rule (computed-type _) Type) (void)) (eval:alts (define-syntax-rule (computed-type _) Type) (void))
(eval:alts (cur-expand #'(λ (x : (computed-type bla)) x)) (eval:alts (cur-expand #'(lambda (x : (computed-type bla)) x))
(eval:result @racket[#'(λ (x : Type) x)] "" "")) (eval:result @racket[#'(lambda (x : Type) x)] "" ""))
] ]
} }
@defproc[(cur-type-infer [syn syntax?]) @defproc[(type-infer/syn [syn syntax?])
(or/c syntax? #f)]{ (or/c syntax? #f)]{
Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred. Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.
@examples[ @examples[
(eval:alts (cur-type-infer #'(λ (x : Type) x)) (eval:alts (type-infer/syn #'(lambda (x : Type) x))
(eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" "")) (eval:result @racket[#'(forall (x : (Type 0)) (Type 0))] "" ""))
(eval:alts (cur-type-infer #'Type) (eval:alts (type-infer/syn #'Type)
(eval:result @racket[#'(Type 1)] "" "")) (eval:result @racket[#'(Type 1)] "" ""))
] ]
} }
@defproc[(cur-type-check? [syn syntax?]) @defproc[(type-check/syn? [syn syntax?])
boolean?]{ boolean?]{
Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise. Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
@examples[ @examples[
(eval:alts (cur-type-check? #'(λ (x : Type) x)) (eval:alts (type-check/syn? #'(lambda (x : Type) x))
(eval:result @racket[#t] "" "")) (eval:result @racket[#t] "" ""))
(eval:alts (cur-type-check? #'Type) (eval:alts (type-check/syn? #'Type)
(eval:result @racket[#t] "" "")) (eval:result @racket[#t] "" ""))
(eval:alts (cur-type-check? #'x) (eval:alts (type-check/syn? #'x)
(eval:result @racket[#f] "" "")) (eval:result @racket[#f] "" ""))
] ]
} }
@defproc[(cur-normalize [syn syntax?]) @defproc[(normalize/syn [syn syntax?])
syntax?]{ syntax?]{
Runs the Cur term @racket[syn] to a value. Runs the Cur term @racket[syn] to a value.
@examples[ @examples[
(eval:alts (cur-normalize #'((λ (x : Type) x) Bool)) (eval:alts (normalize/syn #'((lambda (x : Type) x) Bool))
(eval:result @racket[#'Bool] "" "")) (eval:result @racket[#'Bool] "" ""))
(eval:alts (cur-normalize #'(sub1 (s (s z)))) (eval:alts (normalize/syn #'(sub1 (s (s z))))
(eval:result @racket[#'(s z)] "" "")) (eval:result @racket[#'(s z)] "" ""))
] ]
} }
@defproc[(cur-step [syn syntax?]) @defproc[(step/syn [syn syntax?])
syntax?]{ syntax?]{
Runs the Cur term @racket[syn] for one step. Runs the Cur term @racket[syn] for one step.
@examples[ @examples[
(eval:alts (cur-step #'((λ (x : Type) x) Bool)) (eval:alts (step/syn #'((lambda (x : Type) x) Bool))
(eval:result @racket[#'Bool] "" "")) (eval:result @racket[#'Bool] "" ""))
(eval:alts (cur-step #'(sub1 (s (s z)))) (eval:alts (step/syn #'(sub1 (s (s z))))
(eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat) (eval:result @racket[#'(((((elim Nat (Type 0))
() (lambda (x2 : Nat) Nat)) z)
(z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2))) (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2)))
(s (s z)))] "" "")) (s (s z)))] "" ""))
] ]
} }
@ -90,11 +90,11 @@ equal modulo α and β-equivalence.
@examples[ @examples[
(eval:alts (cur-equal? #'(λ (a : Type) a) #'(λ (b : Type) b)) (eval:alts (cur-equal? #'(lambda (a : Type) a) #'(lambda (b : Type) b))
(eval:result @racket[#t] "" "")) (eval:result @racket[#t] "" ""))
(eval:alts (cur-equal? #'((λ (a : Type) a) Bool) #'Bool) (eval:alts (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool)
(eval:result @racket[#t] "" "")) (eval:result @racket[#t] "" ""))
(eval:alts (cur-equal? #'(λ (a : Type) (sub1 (s z))) #'(λ (a : Type) z)) (eval:alts (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z))
(eval:result @racket[#f] "" "")) (eval:result @racket[#f] "" ""))
] ]
} }
@ -106,7 +106,7 @@ Converts @racket[s] to a datum representation of the @tech{curnel form}, after e
@examples[ @examples[
(eval:alts (cur->datum #'(λ (a : Type) a)) (eval:alts (cur-?datum #'(lambda (a : Type) a))
(eval:result @racket['(λ (a : (Unv 0) a))] "" "")) (eval:result @racket['(λ (a : (Unv 0) a))] "" ""))
] ]
} }

View File

@ -7,10 +7,10 @@ Cur has a small standard library, primary for demonstration purposes.
@local-table-of-contents[] @local-table-of-contents[]
@include-section{stdlib/tactics.scrbl}
@include-section{stdlib/sugar.scrbl} @include-section{stdlib/sugar.scrbl}
@include-section{stdlib/bool.scrbl} @include-section{stdlib/bool.scrbl}
@include-section{stdlib/nat.scrbl} @include-section{stdlib/nat.scrbl}
@include-section{stdlib/maybe.scrbl} @include-section{stdlib/maybe.scrbl}
@include-section{stdlib/list.scrbl} @include-section{stdlib/list.scrbl}
@include-section{stdlib/typeclass.scrbl} @include-section{stdlib/typeclass.scrbl}
@include-section{stdlib/tactics.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 (λ (x : Bool) Bool) () (false true) true)] (elim Bool Type (λ (x : Bool) Bool) false true true)]
} }
@defproc[(not [x Bool]) @defproc[(not [x Bool])

View File

@ -21,24 +21,22 @@ This library defines various syntactic extensions making Cur easier to write tha
@defform*[((-> decl decl ... type) @defform*[((-> decl decl ... type)
(→ decl decl ... type) (→ decl decl ... type)
(forall decl decl ... type) (forall decl decl ... type)
(∀ decl decl ... type) (∀ decl decl ... type))
(Π decl decl ... type)
(Pi decl decl ... type))
#:grammar #:grammar
[(decl [(decl
type type
(code:line (identifier : type)))]]{ (code:line (identifier : type)))]]{
A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying. A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying.
We provide lots of names for this form, because there are lots of synonyms in the literature.
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(data And : (-> Type Type Type) (data And : (-> Type Type)
(conj : (-> (A : Type) (B : Type) A B ((And A) B)))) (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
((((conj Bool) Bool) true) false)] ((((conj Bool) Bool) true) false)]
}
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
(data And : (forall Type Type Type) (data And : (forall Type Type Type)
(conj : (forall (A : Type) (B : Type) A B (And A B)))) (conj : (forall (A : Type) (B : Type) A B ((And A) B))))
((((conj Bool) Bool) true) false)] ((((conj Bool) Bool) true) false)]
} }
@ -62,24 +60,21 @@ Defines multi-arity procedure application via automatic currying.
(conj Bool Bool true false)] (conj Bool Bool true false)]
} }
@defform[(: name type)]{
Declare that the @emph{function} which will be defined as @racket[name] has type @racket[type].
Must precede the definition of @racket[name].
@racket[type] must expand to a function type of the form @racket[(Π (x : t1) t2)]
When used, this form allows omitting the annotations on arguments in the definition @racket[name]
}
@defform*[((define name body) @defform*[((define name body)
(define (name x ...) body)
(define (name (x : t) ...) body))]{ (define (name (x : t) ...) body))]{
Like the @racket[define] provided by @racketmodname[cur], but supports Like the @racket[define] provided by @racketmodname[cur], but supports
defining curried functions via @racket[lambda]. defining curried functions via @racket[lambda].
The second form, @racket[(define (name x ...) body)], can only be used when }
a @racket[(: name type)] form appears earlier in the module.
@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 @examples[#:eval curnel-eval
(: id (forall (A : Type) (a : A) A)) (elim Bool Type (lambda (x : Bool) Bool)
(define (id A a) a)] false
true
true)]
} }
@defform*[((define-type name type) @defform*[((define-type name type)
@ -125,6 +120,7 @@ If @racket[#:return] is not specified, attempts to infer the return type of the
@examples[#:eval curnel-eval @examples[#:eval curnel-eval
((match (nil Bool) ((match (nil Bool)
#:in (List Bool)
[(nil (A : Type)) [(nil (A : Type))
(lambda (n : Nat) (lambda (n : Nat)
(none A))] (none A))]
@ -172,7 +168,7 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if
} }
@defform[(run syn)]{ @defform[(run syn)]{
Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax. Like @racket[normalize/syn], but is a syntactic form to be used in surface syntax.
Allows a Cur term to be written by computing part of the term from Allows a Cur term to be written by computing part of the term from
another Cur term. another Cur term.
@ -182,7 +178,7 @@ another Cur term.
} }
@defform[(step syn)]{ @defform[(step syn)]{
Like @racket[run], but uses @racket[cur-step] to evaluate only one step and prints intermediate Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate
results before returning the result of evaluation. results before returning the result of evaluation.
@examples[#:eval curnel-eval @examples[#:eval curnel-eval

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.4") "sandbox-lib")) (define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
(define pkg-desc "Documentation for \"cur\".") (define pkg-desc "Documentation for \"cur\".")
(define pkg-authors '(wilbowma)) (define pkg-authors '(wilbowma))

View File

@ -26,11 +26,11 @@
(define-language ttL (define-language ttL
(i j k ::= natural) (i j k ::= natural)
(U ::= (Unv i)) (U ::= (Unv i))
(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) (D x c ::= variable-not-otherwise-mentioned)
;; (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))
@ -44,8 +44,6 @@
;;; ------------------------------------------------------------------------ ;;; ------------------------------------------------------------------------
;;; Universe typing ;;; Universe typing
;; Universe types
;; aka Axioms A of a PTS
(define-judgment-form ttL (define-judgment-form ttL
#:mode (unv-type I O) #:mode (unv-type I O)
#:contract (unv-type U U) #:contract (unv-type U U)
@ -55,7 +53,6 @@
(unv-type (Unv i_0) (Unv i_1))]) (unv-type (Unv i_0) (Unv i_1))])
;; Universe predicativity rules. Impredicative in (Unv 0) ;; Universe predicativity rules. Impredicative in (Unv 0)
;; aka Rules R of a PTS
(define-judgment-form ttL (define-judgment-form ttL
#:mode (unv-pred I I O) #:mode (unv-pred I I O)
#:contract (unv-pred U U U) #:contract (unv-pred U U U)
@ -108,6 +105,27 @@
[(Δ-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
@ -127,6 +145,14 @@
;; 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
@ -163,31 +189,47 @@
;; TODO: Test ;; TODO: Test
#| TODO: #| TODO:
| This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true | This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true
| that (convert t (Ξ-apply Ξ t))? | that (equivalent t (Ξ-apply Ξ t))?
| Maybe not. t is a lambda whose type is convert to (Ξ-apply Ξ t)? Yes. | Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
|# |#
(define-metafunction tt-ctxtL (define-metafunction tt-ctxtL
Ξ-apply : Ξ t -> t Ξ-apply : Ξ t -> t
[(Ξ-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
@ -209,6 +251,15 @@
[(Δ-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 -> Ξ
@ -226,6 +277,21 @@
(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
@ -254,6 +320,36 @@
(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.
;; ;;
@ -269,40 +365,29 @@
;; Ξ_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
Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ Δ-elim-type : Δ x U -> t
[(Δ-constructor-inductive-hypotheses Δ D c_i t_P) [(Δ-elim-type Δ x_D U)
(hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))]) (Π (x_P : (in-hole Ξ_P*D U))
;; The methods Ξ_m for each constructor of type x_D
;; Returns the type of the method corresponding to c_i (in-hole Ξ_m
(define-metafunction tt-ctxtL ;; And finally, the parameters and discriminant
Δ-constructor-method-type : Δ D c t -> t (in-hole Ξ_P*D
[(Δ-constructor-method-type Δ D c_i t_P) ;; The result is (P a ... (x_D a ...)), i.e., the motive
(in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i)))) ;; applied to the paramters and discriminant
(where Θ_p (Δ-constructor-parameters Δ D c_i)) (Ξ-apply Ξ_P*D x_P))))
(where Ξ_a (Δ-constructor-telescope Δ D c_i)) ;; Get the parameters of x_D
(where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))]) (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
(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 (Δ D Ξ)) 'x-D)) (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
;; The telescope (∀ a -> ... -> (D a ...) hole), i.e., ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
;; of the indices and the inductive type applied to the ;; of the parameters and the inductive type applied to the
;; indices ;; parameters
(where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ D)) hole)))]) (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))])
;;; ------------------------------------------------------------------------ ;;; ------------------------------------------------------------------------
;;; Dynamic semantics ;;; Dynamic semantics
@ -310,21 +395,16 @@
;;; 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
(v ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c)) ;; 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)) (Θv ::= hole (Θv v))
(C-elim ::= (elim D t_P (e_i ...) (e_m ...) hole)) ;; call-by-value, plus reduce under Π (helps with typing checking)
;; call-by-value (E ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
(E ::= hole (E e) (v 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 ...))
@ -340,6 +420,75 @@
| |
| 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
@ -353,34 +502,39 @@
;; 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-redL (define-metafunction tt-ctxtL
Δ-inductive-elim : Δ D C-elim Θ -> Θ Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
;; 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 any ... hole) [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
hole] ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
[(Δ-inductive-elim Δ D C-elim (Θ_c t_i)) (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
((Δ-inductive-elim Δ D C-elim Θ_c) (side-condition (term (is-inductive-argument Δ x_D t_i)))]
(in-hole C-elim t_i)) [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
(side-condition (term (is-inductive-argument Δ D t_i)))] (Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)]
[(Δ-inductive-elim any ... (Θ_c t_i)) [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m hole)
(Δ-inductive-elim any ... Θ_c)]) hole])
(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 (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c)))) (--> (Δ (in-hole E (in-hole Θv ((elim D U) v_P))))
(Δ (in-hole E (in-hole Θ_mi v_mi))) (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
;; Find the method for constructor c_i, relying on the order of the arguments. ;; Check that Θv is valid to avoid capturing other things
(where natural (Δ-constructor-index Δ D c)) (side-condition (term (Θ-valid Δ D Θv)))
(where v_mi ,(list-ref (term (v_m ...)) (term natural))) ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
;; 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 Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c)) (where Θ_r (Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i))
(where Θ_mi (in-hole Θ_ih Θv_c))
-->elim))) -->elim)))
(define-metafunction tt-redL (define-metafunction tt-redL
@ -396,6 +550,16 @@
(where (_ e_r) (where (_ e_r)
,(car (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)))]) ,(car (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)))])
(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 ;;; Type checking and synthesis
@ -405,24 +569,6 @@
(Γ ::= (Γ x : t))) (Γ ::= (Γ x : t)))
(define Γ? (redex-match? tt-typingL Γ)) (define Γ? (redex-match? tt-typingL Γ))
(define-judgment-form tt-typingL
#:mode (convert I I I I)
#:contract (convert Δ Γ t t)
[(side-condition ,(<= (term i_0) (term i_1)))
----------------- "≼-Unv"
(convert Δ Γ (Unv i_0) (Unv i_1))]
[(where t_2 (reduce Δ t_0))
(where t_3 (reduce Δ t_1))
(side-condition (α-equivalent? t_2 t_3))
----------------- "≼-αβ"
(convert Δ Γ t_0 t_1)]
[(convert Δ (Γ x : t_0) t_1 t_2)
----------------- "≼-Π"
(convert Δ Γ (Π (x : t_0) t_1) (Π (x : t_0) t_2))])
(define-metafunction tt-typingL (define-metafunction tt-typingL
Γ-union : Γ Γ -> Γ Γ-union : Γ Γ -> Γ
[(Γ-union Γ ) Γ] [(Γ-union Γ ) Γ]
@ -541,22 +687,16 @@
----------------- "DTR-Application" ----------------- "DTR-Application"
(type-infer Δ Γ (e_0 e_1) t_3)] (type-infer Δ Γ (e_0 e_1) t_3)]
[(type-check Δ Γ e_c (apply D e_i ...)) [(where t (Δ-elim-type Δ D U))
(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 e_motive (e_i ...) (e_m ...) e_c) (type-infer Δ Γ (elim D U) t)])
(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)
#:contract (type-check Δ Γ e t) #:contract (type-check Δ Γ e t)
[(type-infer Δ Γ e t_0) [(type-infer Δ Γ e t_0)
(convert Δ Γ t t_0) (equivalent Δ t t_0)
----------------- "DTR-Check" ----------------- "DTR-Check"
(type-check Δ Γ e t)]) (type-check Δ Γ e t)])

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
(except-in "redex-core.rkt" apply) "redex-core.rkt"
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
(except-in "redex-core.rkt" apply) "redex-core.rkt"
redex/reduction-semantics)) redex/reduction-semantics))
(provide (provide
;; Basic syntax ;; Basic syntax
@ -30,10 +30,10 @@
[dep-provide provide] [dep-provide provide]
[dep-require require] [dep-require require]
[dep-lambda λ] [dep-lambda lambda]
[dep-app #%app] [dep-app #%app]
[dep-forall Π] [dep-forall forall]
[dep-inductive data] [dep-inductive data]
@ -60,10 +60,10 @@
(all-from-out racket/syntax) (all-from-out racket/syntax)
cur->datum cur->datum
cur-expand cur-expand
cur-type-infer type-infer/syn
cur-type-check? type-check/syn?
cur-normalize normalize/syn
cur-step step/syn
cur-equal?)) cur-equal?))
(begin-for-syntax (begin-for-syntax
@ -177,11 +177,10 @@
[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 D motive (i ...) (m ...) d) [(elim t1 t2)
(term (elim ,(cur->datum #'D) ,(cur->datum #'motive) (let* ([t1 (cur->datum #'t1)]
,(map cur->datum (syntax->list #'(i ...))) [t2 (cur->datum #'t2)])
,(map cur->datum (syntax->list #'(m ...))) (term (elim ,t1 ,t2)))]
,(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))
@ -225,29 +224,29 @@
;; Reflection tools ;; Reflection tools
(define (cur-normalize syn) (define (normalize/syn syn)
(datum->cur (datum->cur
syn syn
(eval-cur syn))) (eval-cur syn)))
(define (cur-step syn) (define (step/syn syn)
(datum->cur (datum->cur
syn syn
(term (step ,(delta) ,(subst-bindings (cur->datum syn)))))) (term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
;; Are these two terms equivalent in type-systems internal equational reasoning? ;; Are these two terms equivalent in type-systems internal equational reasoning?
(define (cur-equal? e1 e2) (define (cur-equal? e1 e2)
(and (judgment-holds (convert ,(delta) ,(gamma) ,(eval-cur e1) ,(eval-cur e2))) #t)) (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
;; TODO: Document local-env ;; TODO: Document local-env
(define (cur-type-infer syn #:local-env [env '()]) (define (type-infer/syn syn #:local-env [env '()])
(parameterize ([gamma (for/fold ([gamma (gamma)]) (parameterize ([gamma (for/fold ([gamma (gamma)])
([(x t) (in-dict env)]) ([(x t) (in-dict env)])
(extend-Γ/syn (thunk gamma) x t))]) (extend-Γ/syn (thunk gamma) x t))])
(let ([t (type-infer/term (eval-cur syn))]) (let ([t (type-infer/term (eval-cur syn))])
(and t (datum->cur syn t))))) (and t (datum->cur syn t)))))
(define (cur-type-check? syn type) (define (type-check/syn? syn type)
(type-check/term? (eval-cur syn) (eval-cur type))) (type-check/term? (eval-cur syn) (eval-cur type)))
;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
@ -411,9 +410,8 @@
;; ;;
;; TODO: Can these be simplified further? ;; TODO: Can these be simplified further?
(define-syntax (dep-lambda syn) (define-syntax (dep-lambda syn)
(syntax-parse syn (syntax-case syn (:)
#:datum-literals (:) [(_ (x : t) e)
[(_ (x:id : t) e)
(syntax->curnel-syntax (syntax->curnel-syntax
(quasisyntax/loc syn (λ (x : t) e)))])) (quasisyntax/loc syn (λ (x : t) e)))]))
@ -424,32 +422,30 @@
(quasisyntax/loc syn (#%app e1 e2)))])) (quasisyntax/loc syn (#%app e1 e2)))]))
(define-syntax (dep-forall syn) (define-syntax (dep-forall syn)
(syntax-parse syn (syntax-case syn (:)
#:datum-literals (:) [(_ (x : t) e)
[(_ (x:id : t) e)
(syntax->curnel-syntax (syntax->curnel-syntax
(quasisyntax/loc syn (Π (x : t) e)))])) (quasisyntax/loc syn (Π (x : t) e)))]))
(define-syntax (Type syn) (define-syntax (Type syn)
(syntax-parse syn (syntax-case syn ()
[(_ i:nat) [(_ i)
(syntax->curnel-syntax (syntax->curnel-syntax
(quasisyntax/loc syn (Unv i)))] (quasisyntax/loc syn (Unv i)))]
[_ (quasisyntax/loc syn (Type 0))])) [_ (quasisyntax/loc syn (Type 0))]))
(define-syntax (dep-inductive syn) (define-syntax (dep-inductive syn)
(syntax-parse syn (syntax-case syn (:)
#:datum-literals (:) [(_ i : ti (x1 : t1) ...)
[(_ i:id : ti (x1:id : t1) ...)
(begin (begin
(extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...)) (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
#'(void))])) #'(void))]))
(define-syntax (dep-elim syn) (define-syntax (dep-elim syn)
(syntax-parse syn (syntax-case syn ()
[(_ D:id motive (i ...) (m ...) e) [(_ D T)
(syntax->curnel-syntax (syntax->curnel-syntax
(quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))])) (quasisyntax/loc syn (elim D T)))]))
(define-syntax-rule (dep-void) (void)) (define-syntax-rule (dep-void) (void))

View File

@ -1,2 +1,2 @@
#lang s-exp syntax/module-reader #lang s-exp syntax/module-reader
cur cur/cur

View File

@ -1,54 +1,245 @@
#lang s-exp "main.rkt" #lang s-exp "cur.rkt"
;; Olly: The OTT-Like LibrarY ;; Olly: The OTT-Like LibrarY
;; TODO: Automagically create a parser from bnf grammar ;; TODO: Automagically create a parser from bnf grammar
(require (require
"stdlib/sugar.rkt" "stdlib/sugar.rkt"
"stdlib/nat.rkt" "stdlib/nat.rkt"
;; TODO: "real-"? More like "curnel-" ;; TODO: "real-"? More like "curnel-"
(only-in (only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
"main.rkt"
[#%app real-app]
[elim real-elim]
[Π real-forall]
[λ real-lambda]))
(provide (provide
define-relation define-relation
define-language define-language
Var
avar
var-equal?
generate-coq generate-coq
;; private; exported for testing only ;; private; exported for testing only
(for-syntax (for-syntax
typeset-relation coq-defns
typeset-bnf output-latex-bnf
cur->coq)) output-coq
new-name
fresh-name))
(begin-for-syntax
(define-syntax-class dash
(pattern x:id
#:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
"Invalid dash"))
(define-syntax-class decl (pattern (x:id (~datum :) t:id)))
;; TODO: Automatically infer decl ... by binding all free identifiers?
;; TODO: Automatically infer decl ... for meta-variables that are the
;; same as bnf grammar.
(define-syntax-class inferrence-rule
(pattern (d:decl ...
x*:expr ...
line:dash lab:id
(name:id y* ...))
#:with rule #'(lab : (-> d ... x* ... (name y* ...)))
;; TODO: convert meta-vars such as e1 to e_1
#:attr latex (format "\\inferrule~n{~a}~n{~a}"
(string-trim
(for/fold ([str ""])
([hyp (syntax->datum #'(x* ...))])
(format "~a~a \\+" str hyp))
" \\+"
#:left? #f)
(format "~a" (syntax->datum #'(name y* ...)))))))
(define-syntax (define-relation syn)
(syntax-parse syn
[(_ (n:id types* ...)
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
rules:inferrence-rule ...)
#:fail-unless (andmap (curry equal? (length (syntax->datum #'(types* ...))))
(map length (syntax->datum #'((rules.y* ...)
...))))
"Mismatch between relation declared and relation definition"
#:fail-unless (andmap (curry equal? (syntax->datum #'n))
(syntax->datum #'(rules.name ...)))
"Mismatch between relation declared name and result of inference rule"
(let ([output #`(data n : (-> types* ... Type) rules.rule ...)])
;; TODO: Pull this out into a separate function and test. Except
;; that might make using attritbutes more difficult.
(when (attribute latex-file)
(with-output-to-file (syntax->datum #'latex-file)
(thunk
(printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
(syntax->datum #'(n types* ...))
(string-trim
(for/fold ([str ""])
([rule (attribute rules.latex)])
(format "~a~a\\and~n" str rule))
"\\and"
#:left? #f))))
#:exists 'append))
#`(begin
#,@(if (attribute coq-file)
#`((generate-coq #:file coq-file #:exists
'append #,output))
#'())
#,output))]))
(begin-for-syntax
(require racket/syntax)
(define (new-name name . id*)
(apply format-id name (for/fold ([str "~a"])
([_ id*])
(string-append str "-~a")) name (map syntax->datum id*)))
(define (fresh-name id)
(datum->syntax id (gensym (syntax->datum id)))))
;; TODO: Oh, this is a mess. Rewrite it.
(begin-for-syntax
(define lang-name (make-parameter #'name))
(define nts (make-parameter (make-immutable-hash)))
(define-syntax-class nt
(pattern e:id #:fail-unless (hash-has-key? (nts) (syntax->datum #'e)) #f
#:attr name (hash-ref (nts) (syntax->datum #'e))
#:attr type (hash-ref (nts) (syntax->datum #'e))))
(define (flatten-args arg arg*)
(for/fold ([ls (syntax->list arg)])
([e (syntax->list arg*)])
(append ls (syntax->list e))))
(define-syntax-class (right-clause type)
#;(pattern (~datum var)
#:attr clause-context #`(#,(new-name (lang-name) #'var) :
(-> #,(hash-ref (nts) 'var) #,(hash-ref (nts) type)))
#:attr name #'var
#:attr arg-context #'(var))
(pattern e:nt
#:attr clause-context #`(#,(new-name #'e.name #'->
(hash-ref (nts) type)) :
(-> e.type #,(hash-ref (nts) type)))
#:attr name (fresh-name #'e.name)
#:attr arg-context #'(e.type))
(pattern x:id
#:attr clause-context #`(#,(new-name (lang-name) #'x) :
#,(hash-ref (nts) type))
#:attr name (new-name (lang-name) #'x)
#:attr arg-context #'())
(pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
#:attr name (fresh-name #'e.name)
#:attr clause-context #`(e.name : (-> #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
#,(hash-ref (nts) type)))
#:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
(define-syntax-class (right type)
(pattern ((~var r (right-clause type)) ...)
#:attr clause #'(r.clause-context ...)))
#;(define-syntax-class left
(pattern (type:id (nt*:id ...+))
#:do ))
(define-syntax-class nt-clauses
(pattern ((type:id (nt*:id ...+)
(~do (nts (for/fold ([ht (nts)])
([nt (syntax->datum #'(type nt* ...))])
(hash-set ht nt (new-name (lang-name) #'type)))))
(~datum ::=)
. (~var rhs* (right (syntax->datum #'type)))) ...)
#:with defs (with-syntax ([(name* ...)
(map (λ (x) (hash-ref (nts) x))
(syntax->datum #'(type ...)))])
#`((data name* : Type . rhs*.clause)
...)))))
(begin-for-syntax
;; TODO: More clever use of syntax-parse would enable something akin to what
;; define-relation is doing---having attributes that contain the latex
;; code for each clause.
;; TODO: convert meta-vars such as e1 to e_1
(define (output-latex-bnf vars clauses)
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(for/fold ([str ""])
([clause (syntax->list clauses)])
(syntax-parse clause
#:datum-literals (::=)
[(type:id (nonterminal:id ...) ::= exprs ...)
(format "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
(symbol->string (syntax->datum #'type))
(string-trim
(for/fold ([str ""])
([nt (syntax->datum #'(nonterminal ...))])
(format "~a~a," str nt))
","
#:left? #f)
(string-trim
(for/fold ([str ""])
([expr (syntax->datum #'(exprs ...))])
(format "~a~a \\bnfalt " str expr))
" \\bnfalt "
#:left? #f))]))))
(define (generate-latex-bnf file-name vars clauses)
(with-output-to-file file-name
(thunk (printf (output-latex-bnf vars clauses)))
#:exists 'append)))
;; TODO: For better error messages, add context, rename some of these patterns. e.g.
;; (type (meta-vars) ::= ?? )
;; TODO: Extend define-language with syntax such as ....
;; (term (e) ::= (e1 e2) ((lambda (x) e)
; #:latex "(\\lambda ,x. ,e)"))
(define-syntax (define-language syn)
(syntax-parse syn
[(_ name:id (~do (lang-name #'name))
(~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
(~optional (~seq #:vars (x*:id ...)
(~do (nts (for/fold ([ht (nts)])
([v (syntax->datum #'(x* ...))])
(hash-set ht v (hash-ref ht 'var)))))))
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
. clause*:nt-clauses)
(let ([output #`(begin . clause*.defs)])
(when (attribute latex-file)
(generate-latex-bnf (syntax->datum #'latex-file) #'vars #'clause*))
#`(begin
#,@(if (attribute coq-file)
#`((generate-coq #:file coq-file #:exists 'append #,output))
#'())
#,output))]))
(data Var : Type (avar : (-> Nat Var)))
(define (var-equal? (v1 : Var) (v2 : Var))
(match v1
[(avar (n1 : Nat))
(match v2
[(avar (n2 : Nat))
(nat-equal? n1 n2)])]))
;; See stlc.rkt for examples
;; Generate Coq from Cur: ;; Generate Coq from Cur:
(begin-for-syntax (begin-for-syntax
(define coq-defns (make-parameter "")) (define coq-defns (make-parameter ""))
(define (coq-lift-top-level str) (define (coq-lift-top-level str)
(coq-defns (format "~a~a~n" (coq-defns) str))) (coq-defns (format "~a~a~n" (coq-defns) str)))
;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
(define (constructor-args syn) (define (constructor-args syn)
(syntax-parse (cur-type-infer syn) (syntax-parse (type-infer/syn syn)
#:datum-literals (Π :) #:datum-literals (Π :)
[(Π (x:id : t) body) [(Π (x:id : t) body)
(cons #'x (constructor-args #'body))] (cons #'x (constructor-args #'body))]
[_ null])) [_ null]))
(define (sanitize-id str) (define (sanitize-id str)
(let ([replace-by `((: _) (- _))]) (let ([replace-by `((: _) (- _))])
(for/fold ([str str]) (for/fold ([str str])
([p replace-by]) ([p replace-by])
(string-replace str (symbol->string (first p)) (string-replace str (symbol->string (first p))
(symbol->string (second p)))))) (symbol->string (second p))))))
(define (output-coq syn)
(define (cur->coq syn)
(parameterize ([coq-defns ""])
(define output
(let cur->coq ([syn syn])
(syntax-parse (cur-expand syn #'define #'begin) (syntax-parse (cur-expand syn #'define #'begin)
;; TODO: Need to add these to a literal set and export it ;; TODO: Need to add these to a literal set and export it
;; Or, maybe overwrite syntax-parse ;; Or, maybe overwrite syntax-parse
@ -56,394 +247,68 @@
[(begin e ...) [(begin e ...)
(for/fold ([str ""]) (for/fold ([str ""])
([e (syntax->list #'(e ...))]) ([e (syntax->list #'(e ...))])
(format "~a~n" (cur->coq e)))] (format "~a~n" (output-coq e)))]
[(define name:id body) [(define name:id body)
(begin (begin
(coq-lift-top-level (coq-lift-top-level
(format "Definition ~a := ~a.~n" (format "Definition ~a := ~a.~n"
(cur->coq #'name) (output-coq #'name)
(cur->coq #'body))) (output-coq #'body)))
"")] "")]
[(define (name:id (x:id : t) ...) body) [(define (name:id (x:id : t) ...) body)
(begin (begin
(coq-lift-top-level (coq-lift-top-level
(format "Function ~a ~a := ~a.~n" (format "Function ~a ~a := ~a.~n"
(cur->coq #'name) (output-coq #'name)
(for/fold ([str ""]) (for/fold ([str ""])
([n (syntax->list #'(x ...))] ([n (syntax->list #'(x ...))]
[t (syntax->list #'(t ...))]) [t (syntax->list #'(t ...))])
(format "~a(~a : ~a) " str (cur->coq n) (cur->coq t))) (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
(cur->coq #'body))) (output-coq #'body)))
"")] "")]
[(real-lambda ~! (x:id (~datum :) t) body:expr) [(real-lambda ~! (x:id (~datum :) t) body:expr)
(format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t) (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
(cur->coq #'body))] (output-coq #'body))]
[(real-forall ~! (x:id (~datum :) t) body:expr) [(real-forall ~! (x:id (~datum :) t) body:expr)
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t) (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
(cur->coq #'body))] (output-coq #'body))]
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...) [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
(begin (begin
(coq-lift-top-level (coq-lift-top-level
(format "Inductive ~a : ~a :=~a." (format "Inductive ~a : ~a :=~a."
(sanitize-id (format "~a" (syntax-e #'n))) (sanitize-id (format "~a" (syntax-e #'n)))
(cur->coq #'t) (output-coq #'t)
(for/fold ([strs ""]) (for/fold ([strs ""])
([clause (syntax->list #'((x* : t*) ...))]) ([clause (syntax->list #'((x* : t*) ...))])
(syntax-parse clause (syntax-parse clause
[(x (~datum :) t) [(x (~datum :) t)
(format "~a~n| ~a : ~a" strs (syntax-e #'x) (format "~a~n| ~a : ~a" strs (syntax-e #'x)
(cur->coq #'t))])))) (output-coq #'t))]))))
"")] "")]
[(Type i) "Type"] [(Type i) "Type"]
[(real-elim var:id motive (i ...) (m ...) d) [(real-elim var t)
(format (format "~a_rect" (output-coq #'var))]
"(~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)" (output-coq #'e1) (output-coq #'e2))]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))]))) [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
(format
"~a~a"
(coq-defns)
(if (regexp-match "^\\s*$" output)
""
(format "Eval compute in ~a." output))))))
(define-syntax (generate-coq syn) (define-syntax (generate-coq syn)
(syntax-parse syn (syntax-parse syn
[(_ (~optional (~seq #:file file)) [(_ (~optional (~seq #:file file))
(~optional (~seq #:exists flag)) (~optional (~seq #:exists flag)) body:expr)
body:expr) (parameterize ([current-output-port (if (attribute file)
(parameterize ([current-output-port (open-output-file (syntax->datum #'file)
(if (attribute file)
(open-output-file
(syntax->datum #'file)
#:exists #:exists
(if (attribute flag) (if (attribute flag)
;; TODO: AHH WHAT? ;; TODO: AHH WHAT?
(eval (syntax->datum #'flag)) (eval (syntax->datum #'flag))
'error)) 'error))
(current-output-port))]) (current-output-port))]
(displayln (cur->coq #'body)) [coq-defns ""])
(define output
(let ([body (output-coq #'body)])
(if (regexp-match "^\\s*$" body)
""
(format "Eval compute in ~a." body))))
(displayln (format "~a~a" (coq-defns) output))
#'(begin))])) #'(begin))]))
;; TODO: Should these display or return a string?
(begin-for-syntax
(define (display-mathpartir)
(displayln
"%% Requires mathpartir, http://pauillac.inria.fr/~remy/latex/mathpartir.html")
(displayln
"%% or mttex, https://github.com/wilbowma/mttex")
(displayln
"\\usepackage{mathpartir}"))
(define (display-bnf)
(displayln
"%% Some auxillary defs. These should deleted if using mttex, https://github.com/wilbowma/mttex")
(displayln
"\\newcommand{\\bnfdef}{{\\bf ::=}}")
(displayln
"\\newcommand{\\bnfalt}{{\\bf \\mid}}")))
;; ------------------------------------
;; define-relation
(begin-for-syntax
(define-syntax-class horizontal-line
(pattern
x:id
#:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
(define-syntax-class hypothesis
(pattern (x:id (~datum :) t))
(pattern (~not e:horizontal-line)))
;; Alias syntax-classes with names for better error messages
(define-syntax-class rule-name
(pattern x:id))
(define-syntax-class relation-name
(pattern x:id))
(define-syntax-class relation-index
(pattern e:expr))
(define-syntax-class (conclusion n args lab)
(pattern
(name:id arg:expr ...)
#:attr rule-label-symbol (syntax-e lab)
#:attr rule-name-symbol (syntax-e #'name)
#:attr relation-name-symbol (syntax-e n)
#:fail-unless (eq? (attribute rule-name-symbol) (attribute relation-name-symbol))
(format "In rule ~a, name of conclusion ~a did not match name of relation ~a"
(attribute rule-label-symbol)
(attribute rule-name-symbol)
(attribute relation-name-symbol))
#:attr rule-arg-count (length (attribute arg))
#:attr relation-arg-count (length args)
#:fail-unless (= (attribute rule-arg-count) (attribute relation-arg-count))
(format "In rule ~a, conclusion applied to ~a arguments, while relation declared to have ~a arguments"
(attribute rule-label-symbol)
(attribute rule-arg-count)
(attribute relation-arg-count))))
;; TODO: Automatically infer hypotheses that are merely declarations by binding all free identifiers?
;; TODO: Automatically infer hypotheses as above for meta-variables that are the
;; same as bnf grammar, as a simple first case
(define-syntax-class (inferrence-rule name indices)
(pattern (h:hypothesis ...
#;line:horizontal-line
(~optional line:horizontal-line)
~!
lab:rule-name
(~var t (conclusion name indices (attribute lab))))
#:with constr-decl
#'(lab : (-> h ... (t.name t.arg ...)))
;; TODO: convert meta-vars such as e1 to e_1
#:attr latex
(format
"\\inferrule~n{~a}~n{~a}"
(string-trim
(for/fold ([str ""])
;; TODO: Perhaps omit hypotheses that are merely delcarations of free variables
([hyp (syntax->datum #'(h ...))])
(format "~a~a \\+" str hyp))
" \\+"
#:left? #f)
(format "~a" (syntax->datum #'(t.name t.arg ...))))))
;; TODO: Should this display or return a string?
(define (typeset-relation form rules-latex)
(display-mathpartir)
(printf
"\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}"
form
(string-trim
(for/fold ([str ""])
([rule rules-latex])
(format "~a~a\\and~n" str rule))
"\\and"
#:left? #f))))
(define-syntax (define-relation syn)
(syntax-parse syn
[(_ (name:relation-name index:relation-index ...)
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
(~var rule (inferrence-rule (attribute name) (attribute index))) ...)
(let ([output #`(data name : (-> index ... Type) rule.constr-decl ...)])
(when (attribute latex-file)
(with-output-to-file (syntax->datum #'latex-file)
(thunk
(typeset-relation
(syntax->datum #'(name index ...))
(attribute rule.latex)))
#:exists 'append))
(when (attribute coq-file)
(with-output-to-file (syntax->datum #'coq-file)
(thunk (displayln (cur->coq output)))
#:exists 'append))
output)]))
;; ------------------------------------
;; define-language
(begin-for-syntax
;; A mutable dictionary from non-terminal meta-variables names to their types.
(define mv-map (make-parameter #f))
;; A set containing the meta-variables that represent variables.
(define vars (make-parameter #f))
;; The language name for the language currently being parsed
(define lang-name (make-parameter #f))
;; A meta-variable is any identifiers that belongs to the mv-map
(define-syntax-class meta-variable
(pattern
x:id
#:attr sym (syntax->datum #'x)
#:fail-unless (dict-has-key? (mv-map) (attribute sym)) #f
#:attr type (dict-ref (mv-map) (attribute sym))))
;; A var-meta-variable is a meta-variable that is declared to be
;; treated as a variable in the defined language.
(define-syntax-class var-meta-variable
(pattern
x:id
#:fail-unless (set-member? (vars) (syntax->datum #'x)) #f))
;; A terminal is a idnetifiers that is not a meta-variable. A terminal will always represent a constructor.
(define-syntax-class terminal
(pattern
x:id
#:attr sym (syntax->datum #'x)
#:fail-when (dict-has-key? (mv-map) (attribute sym)) #f
#:attr constructor-name
(format-id #'x "~a-~a" (lang-name) #'x)))
;; A terminal-args can appear as the argument to a terminal in
;; an expression, or as a sub-expression in a terminal-args.
;; Each terminal-args export args, a list of types the
;; terminal-args represents and the list of types the non-terminal's
;; constructor expects in this case.
(define-syntax-class (terminal-args non-terminal-type)
;; A meta-variable is a terminal-args
(pattern
e:meta-variable
#:attr args
(list #'e.type)
#:attr latex
(format "~a" (syntax-e #'e)))
;; An identifier is a terminal-args, but is treated as syntax
(pattern
x:id
#:attr args
'()
#:attr latex
(format "~a" (syntax-e #'x)))
;; So is an empty list
(pattern
()
#:attr args
'()
#:attr latex
"")
;; We use De-Bruijn indices, so binding positions are removed.
(pattern
(#:bind x:var-meta-variable . (~var t (terminal-args non-terminal-type)))
#:attr args
(attribute t.args)
#:attr latex
(format "~a ~a" (syntax-e #'x) (attribute t.latex)))
;; A terminal-args applied to other nested expressions is a terminal-args
(pattern
((~var h (terminal-args non-terminal-type))
(~var t (terminal-args non-terminal-type)) ...)
#:attr args
(for/fold ([ls (attribute h.args)])
([args (attribute t.args)])
(append ls args))
#:attr latex
(format "~a ~a" (attribute h.latex) (apply string-append (attribute t.latex)))))
;; a expression is parameterized by the name of the non-terminal to
;; which is belongs,
;; Each expression exports a constr-decl, which declares a
;; constructor for the non-terminal type.
(define-syntax-class (expression non-terminal-type)
;; A meta-variable is a valid expression.
;; Generates a conversion constructor in constr-decl, and the type of
(pattern
e:meta-variable
#:attr constructor-name
(format-id #'e "~a->~a" #'e.type non-terminal-type)
#:attr constr-decl
#`(constructor-name : (-> e.type #,non-terminal-type))
#:attr latex
(format "~a" (syntax-e #'e)))
;; An identifier is a valid expression, generating a base constructor.
(pattern
x:terminal
#:attr constr-decl
#`(x.constructor-name : #,non-terminal-type)
#:attr latex
(format "~a" (syntax-e #'x)))
;; A terminal applied to a terminal-args is a valid expression.
(pattern
(x:terminal . (~var c (terminal-args non-terminal-type)))
#:attr constr-decl
#`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))
#:attr latex
(format "(~a ~a)" (syntax-e #'x) (attribute c.latex))))
(define-syntax-class non-terminal-def
(pattern
(name:id
(meta-var:id ...+)
(~optional (~datum ::=))
;; Create a name for the type of this non-terminal, from the
;; language name and the non-terminal name.
(~bind [nt-type (format-id #'name "~a-~a" (lang-name) #'name)])
;; Imperatively update the map from meta-variables to the
;; nt-type, to be used when generating the types of the constructors
;; for this and later non-terminal.
(~do (for ([mv (syntax->datum #'(meta-var ...))])
(dict-set! (mv-map) mv (attribute nt-type))))
(~var c (expression (attribute nt-type))) ...)
;; Generates the inductive data type for this non-terminal definition.
#:attr def
#`(data nt-type : Type c.constr-decl ...)
#:attr latex
(format
"\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
(symbol->string (syntax->datum #'name))
(string-trim
(for/fold ([str ""])
([nt (syntax->datum #'(meta-var ...))])
(format "~a~a," str nt))
","
#:left? #f)
(string-trim
(for/fold ([str ""])
([expr (attribute c.latex)])
(format "~a~a \\bnfalt " str expr))
" \\bnfalt "
#:left? #f))))
;; TODO: Should this display or return a string?
(define (typeset-bnf nt-latex)
(display-mathpartir)
(display-bnf)
(printf
"\begin{displaymath}~n\\begin{array}{lrrl}~n~a~n\\end{array}~n\end{displaymath}"
(apply string-append nt-latex))))
;; TODO: For better error messages, add context
;; TODO: Extend define-language with syntax such as ....
;; (term (e) ::= (e1 e2) ((lambda (x) e)
(define-syntax (define-language syn)
(define/syntax-parse
(_ name:id
(~optional (~seq #:vars (x:id ...)))
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
.
non-terminal-defs)
syn)
(parameterize ([mv-map (make-hash)]
[lang-name #'name]
[vars (apply set (map syntax->datum (or (attribute x) '())))])
(cond
[(attribute x) =>
(lambda (xls)
(for ([x xls])
(dict-set! (mv-map) (syntax-e x) #'Nat)))])
(syntax-parse #'non-terminal-defs
[(def:non-terminal-def ...)
(let ([output #`(begin def.def ...)])
(when (attribute latex-file)
(with-output-to-file (syntax-e #'latex-file)
(thunk (typeset-bnf (attribute def.latex)))
#:exists 'append))
(when (attribute coq-file)
(with-output-to-file (syntax-e #'coq-file)
(thunk (displayln (cur->coq output)))
#:exists 'append))
output)])))
;; See stlc.rkt for examples

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(require "sugar.rkt") (require "sugar.rkt")
(provide Bool true false if not and or) (provide Bool true false if not and or)

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(require (require
"nat.rkt" "nat.rkt"
"maybe.rkt" "maybe.rkt"
@ -8,8 +8,7 @@
List List
nil nil
cons cons
list-ref list-ref)
length)
(data List : (-> (A : Type) Type) (data List : (-> (A : Type) Type)
(nil : (-> (A : Type) (List A))) (nil : (-> (A : Type) (List A)))
@ -23,11 +22,16 @@
(match n (match n
[z (some A a)] [z (some A a)]
[(s (n-1 : Nat)) [(s (n-1 : Nat))
((recur rest) n-1)]))])) ((recur rest) n-1)]))])
#;(elim
(define (length (A : Type) (ls : (List A))) List
(match ls Type
[(nil (A : Type)) (lambda (A : Type) (ls : (List A))
z] (-> Nat (Maybe A)))
[(cons (A : Type) (a : A) (rest : (List A))) (lambda (A : Type) (n : Nat) (none A))
(s (recur rest))])) (lambda (A : Type) (a : A) (ls : (List A)) (ih : (-> Nat (Maybe A)))
(lambda (n : Nat)
(match n
[z (some A a)]
[(s (n-1 : Nat))
(ih n-1)])))))

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(require "sugar.rkt") (require "sugar.rkt")
(provide Maybe none some some/i) (provide Maybe none some some/i)
@ -9,5 +9,5 @@
(define-syntax (some/i syn) (define-syntax (some/i syn)
(syntax-case syn () (syntax-case syn ()
[(_ a) [(_ a)
(let ([a-ty (cur-type-infer #'a)]) (let ([a-ty (type-infer/syn #'a)])
#`(some #,a-ty a))])) #`(some #,a-ty a))]))

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(require "sugar.rkt" "bool.rkt") (require "sugar.rkt" "bool.rkt")
;; TODO: override (all-defined-out) to enable exporting all these ;; TODO: override (all-defined-out) to enable exporting all these
;; properly. ;; properly.

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(require "sugar.rkt") (require "sugar.rkt")
;; TODO: Handle multiple provide forms properly ;; TODO: Handle multiple provide forms properly
;; TODO: Handle (all-defined-out) properly ;; TODO: Handle (all-defined-out) properly
@ -31,8 +31,8 @@
(define-syntax (conj/i syn) (define-syntax (conj/i syn)
(syntax-case syn () (syntax-case syn ()
[(_ a b) [(_ a b)
(let ([a-type (cur-type-infer #'a)] (let ([a-type (type-infer/syn #'a)]
[b-type (cur-type-infer #'b)]) [b-type (type-infer/syn #'b)])
#`(conj #,a-type #,b-type a b))])) #`(conj #,a-type #,b-type a b))]))
(define thm:and-is-symmetric (define thm:and-is-symmetric
@ -71,12 +71,11 @@
(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 (lambda (A : Type) (B : Type) (c : (Or A B)) A) (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
(A A) (lambda (A : Type) (B : Type) (a : A) a)
((lambda (A : Type) (B : Type) (a : A) a)
;; TODO: How do we know B is A? ;; TODO: How do we know B is A?
(lambda (A : Type) (B : Type) (b : B) b)) (lambda (A : Type) (B : Type) (b : B) b)
c))) A A c)))
(qed thm:A-or-A proof:A-or-A) (qed thm:A-or-A proof:A-or-A)
|# |#

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(provide (provide
-> ->
lambda lambda
@ -6,12 +6,10 @@
[-> ] [-> ]
[-> forall] [-> forall]
[-> ] [-> ]
[-> Π]
[-> Pi]
[lambda λ]) [lambda λ])
#%app #%app
define define
: elim
define-type define-type
match match
recur recur
@ -27,10 +25,12 @@
query-type) query-type)
(require (require
(only-in "../main.rkt" (only-in "../cur.rkt"
[elim real-elim]
[#%app real-app] [#%app real-app]
[λ real-lambda] ;; Somehow, using real-lambda instead of _lambda causes weird import error
[Π real-Π] [lambda real-lambda]
#;[forall real-forall]
[define real-define])) [define real-define]))
(begin-for-syntax (begin-for-syntax
@ -53,7 +53,7 @@
[(_ d:parameter-declaration ...+ result:result-type) [(_ d:parameter-declaration ...+ result:result-type)
(foldr (lambda (src name type r) (foldr (lambda (src name type r)
(quasisyntax/loc src (quasisyntax/loc src
(real-Π (#,name : #,type) #,r))) (forall (#,name : #,type) #,r)))
#'result #'result
(attribute d) (attribute d)
(attribute d.name) (attribute d.name)
@ -95,65 +95,21 @@
[(_ e1 e2 e3 ...) [(_ e1 e2 e3 ...)
(quasisyntax/loc syn (quasisyntax/loc syn
(#%app (#%app e1 e2) e3 ...))])) (#%app (#%app e1 e2) e3 ...))]))
(module+ test
((lambda (A : (Type 1)) (B : (Type 1)) A)
Type
Type))
(define-syntax define-type (define-syntax define-type
(syntax-rules () (syntax-rules ()
[(_ (name (a : t) ...) body) [(_ (name (a : t) ...) body)
(define name (-> (a : t) ... body))] (define name (forall (a : t) ... body))]
[(_ name type) [(_ name type)
(define name type)])) (define name type)]))
;; Cooperates with define to allow Haskell-esque type annotations
#| TODO NB:
| This method of cooperating macros is sort of a terrible
| hack. Instead, need principled way of adding/retrieving information
| to/from current module. E.g. perhaps provide extensions an interface to
| module's term environment and inductive signature. Then, :: could add
| new "id : type" to environment, and define could extract type and use.
|#
(begin-for-syntax
(define annotation-dict (make-hash))
(define (annotation->types type-syn)
(let loop ([ls '()]
[syn type-syn])
(syntax-parse (cur-expand syn)
#:datum-literals (:)
[(real-Π (x:id : type) body)
(loop (cons #'type ls) #'body)]
[_ (reverse ls)]))))
(define-syntax (: syn)
(syntax-parse syn
[(_ name:id type:expr)
;; NB: Unhygenic; need to reuse Racket's identifiers, and make this type annotation a syntax property
(syntax-parse (cur-expand #'type)
#:datum-literals (:)
[(real-Π (x:id : type) body) (void)]
[_
(raise-syntax-error
':
"Can only declare annotations for functions, but not a function type"
syn)])
(dict-set! annotation-dict (syntax->datum #'name) (annotation->types #'type))
#'(void)]))
;; TODO: Allow inferring types as in above TODOs for lambda, forall ;; TODO: Allow inferring types as in above TODOs for lambda, forall
(define-syntax (define syn) (define-syntax (define syn)
(syntax-parse syn (syntax-case syn ()
#:datum-literals (:)
[(define (name:id x:id ...) body)
(cond
[(dict-ref annotation-dict (syntax->datum #'name)) =>
(lambda (anns)
(quasisyntax/loc syn
(real-define name (lambda #,@(for/list ([x (syntax->list #'(x ...))]
[type anns])
#`(#,x : #,type)) body))))]
[else
(raise-syntax-error
'define
"Cannot omit type annotations unless you have declared them with (: name type) form first."
syn)])]
[(define (name (x : t) ...) body) [(define (name (x : t) ...) body)
(quasisyntax/loc syn (quasisyntax/loc syn
(real-define name (lambda (x : t) ... body)))] (real-define name (lambda (x : t) ... body)))]
@ -161,67 +117,8 @@
(quasisyntax/loc syn (quasisyntax/loc syn
(real-define id body))])) (real-define id body))]))
#| (define-syntax-rule (elim t1 t2 e ...)
(begin-for-syntax ((real-elim t1 t2) e ...))
(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
@ -268,7 +165,7 @@
#:attr types #:attr types
;; TODO: Detect failure, report error/suggestions ;; TODO: Detect failure, report error/suggestions
(for/list ([e (attribute indices)]) (for/list ([e (attribute indices)])
(or (cur-type-infer e) (or (type-infer/syn e)
(raise-syntax-error (raise-syntax-error
'match 'match
(format (format
@ -289,7 +186,7 @@
(lambda (return) (lambda (return)
;; NB: unhygenic ;; NB: unhygenic
;; Normalize at compile-time, for efficiency at run-time ;; Normalize at compile-time, for efficiency at run-time
(cur-normalize (normalize/syn
#`((lambda #`((lambda
;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed ;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed
;; works only for simple type familes and simply matches on them ;; works only for simple type familes and simply matches on them
@ -350,7 +247,7 @@
(define/syntax-parse type:inductive-type-declaration (cur-expand type-syn)) (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn))
(let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))] (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))]
;; Normalize at compile-time, for efficiency at run-time ;; Normalize at compile-time, for efficiency at run-time
[ih-type (cur-normalize #`(#,motive #,@(attribute type.indices) #,name-syn))]) [ih-type (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))])
(dict-set! ih-dict (syntax->datum name-syn) ih-name) (dict-set! ih-dict (syntax->datum name-syn) ih-name)
(append decls (list #`(#,ih-name : #,ih-type))))))) (append decls (list #`(#,ih-name : #,ih-type)))))))
@ -362,7 +259,7 @@
(or maybe-return-type (or maybe-return-type
;; Ignore errors when trying to infer this type; other attempt might succeed ;; Ignore errors when trying to infer this type; other attempt might succeed
(with-handlers ([values (lambda _ #f)]) (with-handlers ([values (lambda _ #f)])
(cur-type-infer #:local-env (attribute p.local-env) #'b))))) (type-infer/syn #:local-env (attribute p.local-env) #'b)))))
(define-syntax-class (match-clause D motive) (define-syntax-class (match-clause D motive)
(pattern (pattern
@ -398,7 +295,7 @@
(~optional (~optional
(~seq #:in ~! t) (~seq #:in ~! t)
#:defaults #:defaults
([t (or (cur-type-infer #'d) ([t (or (type-infer/syn #'d)
(raise-syntax-error (raise-syntax-error
'match 'match
"Could not infer discrimnant's type. Try using #:in to declare it." "Could not infer discrimnant's type. Try using #:in to declare it."
@ -423,9 +320,15 @@
(quasisyntax/loc syn (quasisyntax/loc syn
(elim (elim
D.inductive-name D.inductive-name
#,(or
(type-infer/syn (attribute return-type))
(raise-syntax-error
'match
"Could not infer type of motive. Sorry, you'll have to use elim."
syn))
motive motive
#,(attribute D.indices) c.method ...
(c.method ...) #,@(attribute D.indices)
d))])) d))]))
(begin-for-syntax (begin-for-syntax
@ -437,14 +340,14 @@
#:attr type (cond #:attr type (cond
[(attribute t) [(attribute t)
;; TODO: Code duplication in :: ;; TODO: Code duplication in ::
(unless (cur-type-check? #'e #'t) (unless (type-check/syn? #'e #'t)
(raise-syntax-error (raise-syntax-error
'let 'let
(format "Term ~a does not have expected type ~a. Inferred type was ~a" (format "Term ~a does not have expected type ~a. Inferred type was ~a"
(cur->datum #'e) (cur->datum #'t) (cur->datum (cur-type-infer #'e))) (cur->datum #'e) (cur->datum #'t) (cur->datum (type-infer/syn #'e)))
#'e (quasisyntax/loc #'x (x e)))) #'e (quasisyntax/loc #'x (x e))))
#'t] #'t]
[(cur-type-infer #'e)] [(type-infer/syn #'e)]
[else [else
(raise-syntax-error (raise-syntax-error
'let 'let
@ -455,29 +358,29 @@
[(let (c:let-clause ...) body) [(let (c:let-clause ...) body)
#'((lambda (c.id : c.type) ... body) c.e ...)])) #'((lambda (c.id : c.type) ... body) c.e ...)]))
;; Normally type checking will only happen if a term is actually used/appears at top-level. ;; Normally type checking will only happen if a term is actually used. This forces a term to be
;; This forces a term to be checked against a particular type. ;; checked against a particular type.
(define-syntax (:: syn) (define-syntax (:: syn)
(syntax-case syn () (syntax-case syn ()
[(_ pf t) [(_ pf t)
(begin (begin
;; TODO: Code duplication in let-clause pattern ;; TODO: Code duplication in let-clause pattern
(unless (cur-type-check? #'pf #'t) (unless (type-check/syn? #'pf #'t)
(raise-syntax-error (raise-syntax-error
':: '::
(format "Term ~a does not have expected type ~a. Inferred type was ~a" (format "Term ~a does not have expected type ~a. Inferred type was ~a"
(cur->datum #'pf) (cur->datum #'t) (cur->datum (cur-type-infer #'pf))) (cur->datum #'pf) (cur->datum #'t) (cur->datum (type-infer/syn #'pf)))
syn)) syn))
#'(void))])) #'(void))]))
(define-syntax (run syn) (define-syntax (run syn)
(syntax-case syn () (syntax-case syn ()
[(_ expr) (cur-normalize #'expr)])) [(_ expr) (normalize/syn #'expr)]))
(define-syntax (step syn) (define-syntax (step syn)
(syntax-case syn () (syntax-case syn ()
[(_ expr) [(_ expr)
(let ([t (cur-step #'expr)]) (let ([t (step/syn #'expr)])
(displayln (cur->datum t)) (displayln (cur->datum t))
t)])) t)]))
@ -493,6 +396,6 @@
(syntax-case syn () (syntax-case syn ()
[(_ term) [(_ term)
(begin (begin
(printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (cur-type-infer #'term))) (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
;; Void is undocumented and a hack, but sort of works ;; Void is undocumented and a hack, but sort of works
#'(void))])) #'(void))]))

View File

@ -1,4 +1,4 @@
#lang s-exp "../../main.rkt" #lang s-exp "../../cur.rkt"
(require (require
(for-syntax racket/syntax)) (for-syntax racket/syntax))
(provide (provide
@ -220,7 +220,7 @@
[pf (proof-state-proof ps)]) [pf (proof-state-proof ps)])
(unless (proof-state-proof-complete? ps) (unless (proof-state-proof-complete? ps)
(raise-syntax-error 'qed "Proof contains holes" (pf (current-hole-pretty-symbol)))) (raise-syntax-error 'qed "Proof contains holes" (pf (current-hole-pretty-symbol))))
(unless (cur-type-check? pf t) (unless (type-check/syn? pf t)
(raise-syntax-error 'qed "Invalid proof" pf t)) (raise-syntax-error 'qed "Invalid proof" pf t))
pf))) pf)))

View File

@ -1,4 +1,4 @@
#lang s-exp "../../main.rkt" #lang s-exp "../../cur.rkt"
(require (require
"base.rkt" "base.rkt"
(prefix-in basic: "standard.rkt") (prefix-in basic: "standard.rkt")

View File

@ -1,4 +1,4 @@
#lang s-exp "../../main.rkt" #lang s-exp "../../cur.rkt"
(require (require
"base.rkt" "base.rkt"
(for-syntax racket/syntax)) (for-syntax racket/syntax))
@ -22,7 +22,7 @@
[(forall (x:id : P:expr) body:expr) [(forall (x:id : P:expr) body:expr)
(let* ([ps (proof-state-extend-env ps name #'P)] (let* ([ps (proof-state-extend-env ps name #'P)]
[ps (proof-state-current-goal-set ps #'body)] [ps (proof-state-current-goal-set ps #'body)]
[ps (proof-state-fill-proof-hole ps (lambda (x) #`(λ (#,name : P) #,x)))]) [ps (proof-state-fill-proof-hole ps (lambda (x) #`(lambda (#,name : P) #,x)))])
ps)] ps)]
[_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")])) [_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")]))

View File

@ -1,4 +1,4 @@
#lang s-exp "../main.rkt" #lang s-exp "../cur.rkt"
(require (require
"nat.rkt" "nat.rkt"
"bool.rkt" "bool.rkt"
@ -38,7 +38,7 @@
#`(define-syntax (#,name syn) #`(define-syntax (#,name syn)
(syntax-case syn () (syntax-case syn ()
[(_ arg args (... ...)) [(_ arg args (... ...))
#`(#,(format-id syn "~a-~a" '#,name (cur-type-infer #'arg)) #`(#,(format-id syn "~a-~a" '#,name (type-infer/syn #'arg))
arg arg
args (... ...))]))))])) args (... ...))]))))]))
@ -57,7 +57,7 @@
#`(begin #`(begin
#,@(for/list ([def (syntax->list #'(defs ...))]) #,@(for/list ([def (syntax->list #'(defs ...))])
(let-values ([(name body) (process-def def)]) (let-values ([(name body) (process-def def)])
(unless (cur-type-check? (unless (type-check/syn?
body body
#`(#,(dict-ref #`(#,(dict-ref
(dict-ref typeclasses (syntax->datum #'class)) (dict-ref typeclasses (syntax->datum #'class))

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.4") (define version "0.2")
(define pkg-authors '(wilbowma)) (define pkg-authors '(wilbowma))

View File

@ -9,50 +9,77 @@
cur/olly) cur/olly)
(begin-for-syntax (begin-for-syntax
(require rackunit)) (require rackunit)
(define (check-id-equal? v1 v2)
;; Can't test this way anymore.
#;(begin-for-syntax
(check-equal? (check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$" (syntax->datum v1)
(format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n")) (syntax->datum v2)))
(typeset-bnf #'((term (e) ::= (e1 e2) (lambda (x) e))))) (define (check-id-match? v1 v2)
(check-equal? (check-regexp-match
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$" v1
(format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n")) (symbol->string (syntax->datum v2))))
(typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C)))))) (check-id-match?
#px"term\\d+"
(fresh-name #'term))
(check-id-equal?
#'stlc-lambda
(new-name #'stlc #'lambda))
(check-id-match?
#px"stlc-term\\d+"
(new-name #'stlc (fresh-name #'term))))
(begin-for-syntax (begin-for-syntax
(check-equal? (check-equal?
(format "Inductive nat : Type :=~n| z : nat.~n") (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(cur->coq #'(data nat : Type (z : nat)))) (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
(output-latex-bnf #'(x)
#'((term (e) ::= (e1 e2) (lambda (x) e)))))
(check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
(output-latex-bnf #'(x)
#'((type (A B C) ::= unit (* A B) (+ A C))))))
(check-equal?
(var-equal? (avar z) (avar z))
true)
(check-equal?
(var-equal? (avar z) (avar (s z)))
false)
(begin-for-syntax
(check-equal?
(parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
(format "Inductive nat : Type :=~n| z : nat.~n"))
(check-regexp-match (check-regexp-match
"(forall .+ : Type, Type)" "(forall .+ : Type, Type)"
(cur->coq #'(-> Type Type))) (output-coq #'(-> Type Type)))
(let ([t (cur->coq (let ([t (parameterize ([coq-defns ""])
#'(define-relation (meow gamma term type) (output-coq #'(define-relation (meow gamma term type)
[(g : gamma) (e : term) (t : type) [(g : gamma) (e : term) (t : type)
--------------- T-Bla --------------- T-Bla
(meow g e t)]))]) (meow g e t)]))
(coq-defns))])
(check-regexp-match (check-regexp-match
"Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :=" "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
(first (string-split t "\n"))) (first (string-split t "\n")))
(check-regexp-match (check-regexp-match
"\\| 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 (output-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"
(cur->coq (parameterize ([coq-defns ""])
#'(define thm:plus-commutes (forall (n : nat) (m : nat) (output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
(== nat (plus n m) (plus m n)))))) (== nat (plus n m) (plus m n)))))
(coq-defns)))
(check-regexp-match (check-regexp-match
"Function add1 \\(n : nat\\) := \\(s n\\).\n" "Function add1 \\(n : nat\\) := \\(s n\\).\n"
(cur->coq #'(define (add1 (n : nat)) (s n))))) (parameterize ([coq-defns ""])
(output-coq #'(define (add1 (n : nat)) (s n)))
(coq-defns))))

View File

@ -1,24 +0,0 @@
#lang cur
(require
cur/stdlib/sugar
rackunit)
(data Nat : Type
(z : Nat)
(s : (Π (x : Nat) Nat)))
(plus . : . (-> Nat Nat Nat))
(define (plus n m)
(match n
[z m]
[(s (x : Nat))
(s (recur x))]))
(check-equal?
(plus z z)
z)
(check-equal?
(plus (s z) z)
(s z))

View File

@ -81,6 +81,23 @@
(Π (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
@ -98,10 +115,41 @@
(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
;; ------------------------------------------------------------------------ ;; ------------------------------------------------------------------------
@ -109,32 +157,21 @@
(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 (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
(elim nat (λ (x : nat) nat) () ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
hole)
(hole zero))) (hole zero)))
(term (hole (elim nat (λ (x : nat) nat) (term (hole (((((elim nat Type) (λ (x : nat) nat))
() (s zero))
((s zero)
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero)))) zero))))
(check-telescope-equiv? (check-telescope-equiv?
(term (Δ-inductive-elim ,Δ nat (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
(elim nat (λ (x : nat) nat) () ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
hole)
(hole (s zero)))) (hole (s zero))))
(term (hole (elim nat (λ (x : nat) nat) () (term (hole (((((elim nat Type) (λ (x : nat) nat))
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (s zero))
(λ (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
;; ------------------------------------------------------------------------ ;; ------------------------------------------------------------------------
@ -142,8 +179,6 @@
(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)))
@ -153,71 +188,63 @@
(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))
(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0) (s zero))
(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat) (λ (x : nat) (λ (ih-x : nat)
() (s (s x)))))
((s zero)
(λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero))) zero)))
(term (s zero))) (term (s zero)))
(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat) (check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
() (s zero))
((s zero) (λ (x : nat) (λ (ih-x : nat)
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) (s (s x)))))
(s zero)))) (s zero))))
(term (s (s zero)))) (term (s (s zero))))
(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat) (check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
() (s zero))
((s zero)
(λ (x : nat) (λ (ih-x : nat) (s (s x))))) (λ (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 (λ (x : nat) nat) (((((elim nat Type) (λ (x : nat) nat))
() (s (s zero)))
((s (s zero))
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s (s zero))))) (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 (λ (x : nat) nat) (((((elim nat Type) (λ (x : nat) nat))
() (s (s zero)))
((s (s zero))
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s (s zero))))) (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 (λ (x : nat) nat) (((((elim nat Type) (λ (x : nat) nat))
() (s (s zero)))
((s (s zero))
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s zero))))) (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 (λ (x : nat) nat) (((((elim nat Type) (λ (x : nat) nat))
() (s (s zero)))
((s (s zero))
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
(s zero)))))) (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 (λ (x : nat) nat) (((((elim nat Type) (λ (x : nat) nat))
() (s (s zero)))
((s (s zero))
(λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
zero))))) zero)))))
(define-syntax-rule (check-equivalent e1 e2) (define-syntax-rule (check-equivalent e1 e2)
(check-holds (convert e1 e2))) (check-holds (equivalent e1 e2)))
(check-equivalent (check-equivalent
(λ (x : Type) x) (λ (y : Type) y)) (λ (x : Type) x) (λ (y : Type) y))
(check-equivalent (check-equivalent
@ -316,42 +343,28 @@
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-equiv? (check-telescope-equiv?
(term (Δ-motive-type ,Δtruth truth (Unv 2))) (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
(term (Π (x : truth) (Unv 2)))) (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))))
(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 (λ (x : truth) (Unv 1)) ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
() ((Unv 0)) T) 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 Type () (Type) T) ((((elim truth (Unv 1)) 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))
@ -369,54 +382,47 @@
(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 (λ (x : nat) nat) () (nat-test (((((elim nat Type) (λ (x : nat) nat)) zero)
(zero (λ (x : nat) (λ (ih-x : nat) x))) (λ (x : nat) (λ (ih-x : nat) x))) zero)
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 ,Δ (λ (x : nat) (type-infer ,Δ ((((elim nat (Unv 0)) (λ (x : nat) nat))
(elim nat (λ (x : nat) nat) zero)
()
(zero
(λ (x : nat) (λ (ih-x : nat) x))) (λ (x : nat) (λ (ih-x : nat) x)))
x))
t)) t))
(nat-test (elim nat (λ (x : nat) nat) (nat-test (((((elim nat (Unv 0)) (λ (x : nat) nat))
() zero)
(zero (λ (x : nat) (λ (ih-x : nat) x))) (λ (x : nat) (λ (ih-x : nat) x)))
zero) zero)
nat) nat)
(nat-test (elim nat (λ (x : nat) nat) (nat-test (((((elim nat (Unv 0)) (λ (x : nat) nat))
() (s zero))
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
zero) zero)
nat) nat)
(nat-test (elim nat (λ (x : nat) nat) (nat-test (((((elim nat Type) (λ (x : nat) nat))
() (s zero))
((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
zero)
nat) nat)
(nat-test ( n : nat) (nat-test ( n : nat)
(elim nat (λ (x : nat) nat) (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
()
(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 (λ (x : nat) bool) (((((elim nat (Unv 0)) (λ (x : nat) bool))
() btrue)
(btrue (λ (x : nat) (λ (ih-x : bool) bfalse))) (λ (x : nat) (λ (ih-x : bool) bfalse)))
n2) n2)
bool)) bool))
(check-not-holds (check-not-holds
(type-check ,Δ (type-check ,Δ
(elim nat nat () ((s zero)) zero) ((((elim nat (Unv 0)) nat) (s zero)) zero)
nat)) nat))
(define lam (term (λ (nat : (Unv 0)) nat))) (define lam (term (λ (nat : (Unv 0)) nat)))
(check-equivalent (check-equivalent
@ -475,14 +481,14 @@
(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 ((((((elim and (Unv 0))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
true))) true))))
(true true) (λ (A : (Unv 0))
((λ (A : (Unv 0))
(λ (B : (Unv 0)) (λ (B : (Unv 0))
(λ (a : A) (λ (a : A)
(λ (b : B) tt))))) (λ (b : B) tt)))))
true) true)
((((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)))))
@ -501,7 +507,7 @@
((and B) A)))) ((and B) A))))
(in-hole Ξ (Π (x : (in-hole Θ and)) U)))) (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
(check-holds (check-holds
(convert ,Δ4 (equivalent ,Δ4
(Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))) (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
(Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0)))))) (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
(check-holds (check-holds
@ -512,15 +518,14 @@
(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 ((((((elim and (Unv 0))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A)))) ((and B) A)))))
(P Q) (λ (A : (Unv 0))
((λ (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))))))
ab) P) Q) 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))))
@ -533,14 +538,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 ((((((elim and (Unv 0))
(λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
((and B) A)))) ((and B) A)))))
(true true) (λ (A : (Unv 0))
((λ (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)))
@ -563,18 +568,21 @@
(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 (λ (y : false) (Π (x : Type) x)) () () x) (((elim false (Unv 0)) (λ (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 (λ (n : nat) (term ((((elim nat Type) (λ (x : nat) bool))
(elim nat (λ (x : nat) bool) () true)
(true (λ (x : nat) (λ (x_ih : bool) false))) (λ (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?
@ -584,12 +592,9 @@
(term (reduce ,Δ (,zero? (s zero)))) (term (reduce ,Δ (,zero? (s zero))))
(term false)) (term false))
(define ih-equal? (define ih-equal?
(term (λ (ih : nat) (term ((((elim nat Type) (λ (x : nat) bool))
(elim nat (λ (x : nat) bool) false)
() (λ (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?
@ -601,13 +606,10 @@
(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 (λ (n : nat) (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
(elim nat (λ (x : nat) (Π (x : nat) bool)) ,zero?)
()
(,zero?
(λ (x : nat) (λ (x_ih : (Π (x : nat) bool)) (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
,ih-equal?))) ,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)
@ -629,12 +631,19 @@
(check-true (Δ? Δ=)) (check-true (Δ? Δ=))
(define refl-elim (define refl-elim
(term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat)))) (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
(bool true true) A1)
((λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) x1)
((refl bool) true)))) y1))
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

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 (lambda (A : Type) (ls : (List A)) Nat) (:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
(Bool) (lambda (A : Type) z)
((lambda (A : Type) z)
(lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat) (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
z)) z)
Bool
(nil Bool)) (nil Bool))
Nat)) Nat))

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 == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat) (elim == Type (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
(Bool (λ (A : Type) (x : A) z)
Bool
true
true true
true)
((λ (A : Type) (x : A) z))
(refl Bool true)) (refl Bool true))
z) z)

View File

@ -11,7 +11,9 @@
(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 b (not b)))) (if a
(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?

View File

@ -2,7 +2,6 @@
(require (require
rackunit rackunit
cur/stdlib/nat cur/stdlib/nat
cur/stdlib/list
cur/stdlib/sugar cur/stdlib/sugar
cur/olly cur/olly
cur/stdlib/maybe cur/stdlib/maybe
@ -16,55 +15,64 @@
(val (v) ::= true false unit) (val (v) ::= true false unit)
;; TODO: Allow datum, like 1, as terminals ;; TODO: Allow datum, like 1, as terminals
(type (A B) ::= boolty unitty (-> A B) (* A A)) (type (A B) ::= boolty unitty (-> A B) (* A A))
(term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e) (term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e)
(let (#:bind x #:bind x) = e in e))) (let (x x) = e in e)))
(define lookup-env (list-ref stlc-type)) ;; TODO: Abstract this over stlc-type, and provide from in OLL
(data Gamma : Type
(emp-gamma : Gamma)
(extend-gamma : (-> Gamma Var stlc-type Gamma)))
(define (extend-env (g : (List stlc-type)) (t : stlc-type)) (define (lookup-gamma (g : Gamma) (x : Var))
(cons stlc-type t g)) (match g
[emp-gamma (none stlc-type)]
[(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
(if (var-equal? v1 x)
(some stlc-type t1)
(recur g1))]))
(define-relation (has-type (List stlc-type) stlc-term stlc-type) (define-relation (has-type Gamma stlc-term stlc-type)
#:output-coq "stlc.v" #:output-coq "stlc.v"
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
[(g : (List stlc-type)) [(g : Gamma)
------------------------ T-Unit ------------------------ T-Unit
(has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)] (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
[(g : (List stlc-type)) [(g : Gamma)
------------------------ T-True ------------------------ T-True
(has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)] (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
[(g : (List stlc-type)) [(g : Gamma)
------------------------ T-False ------------------------ T-False
(has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)] (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
[(g : (List stlc-type)) (x : Nat) (t : stlc-type) [(g : Gamma) (x : Var) (t : stlc-type)
(== (Maybe stlc-type) (lookup-env g x) (some stlc-type t)) (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
------------------------ T-Var ------------------------ T-Var
(has-type g (Nat->stlc-term x) t)] (has-type g (Var-->-stlc-term x) t)]
[(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(has-type g e1 t1) (has-type g e1 t1)
(has-type g e2 t2) (has-type g e2 t2)
---------------------- T-Pair ---------------------- T-Pair
(has-type g (stlc-cons e1 e2) (stlc-* t1 t2))] (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))]
[(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(t : stlc-type) (t : stlc-type)
(x : Var) (y : Var)
(has-type g e1 (stlc-* t1 t2)) (has-type g e1 (stlc-* t1 t2))
(has-type (extend-env (extend-env g t1) t2) e2 t) (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
---------------------- T-Let ---------------------- T-Let
(has-type g (stlc-let e1 e2) t)] (has-type g (stlc-let x y e1 e2) t)]
[(g : (List stlc-type)) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
(has-type (extend-env g t1) e1 t2) (has-type (extend-gamma g x t1) e1 t2)
---------------------- T-Fun ---------------------- T-Fun
(has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))] (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
[(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(has-type g e1 (stlc--> t1 t2)) (has-type g e1 (stlc--> t1 t2))
(has-type g e2 t1) (has-type g e2 t1)
@ -76,57 +84,59 @@
;; TODO: When generating a parser, will need something like (#:name app (e e)) ;; TODO: When generating a parser, will need something like (#:name app (e e))
;; so I can name a constructor without screwing with syntax. ;; so I can name a constructor without screwing with syntax.
(begin-for-syntax (begin-for-syntax
(define (dict-shift d) (define index #'z))
(for/fold ([d (make-immutable-hash)])
([(k v) (in-dict d)])
(dict-set d k #`(s #,v)))))
(define-syntax (begin-stlc syn) (define-syntax (begin-stlc syn)
(let stlc ([syn (syntax-case syn () [(_ e) #'e])] (set! index #'z)
[d (make-immutable-hash)]) (let stlc ([syn (syntax-case syn () [(_ e) #'e])])
(syntax-parse syn (syntax-parse syn
#:datum-literals (lambda : prj * -> quote let in cons bool) #:datum-literals (lambda : prj * -> quote let in cons bool)
[(lambda (x : t) e) [(lambda (x : t) e)
#`(stlc-lambda #,(stlc #'t d) #,(stlc #'e (dict-set (dict-shift d) (syntax->datum #'x) #`z)))] (let ([oldindex index])
(set! index #`(s #,index))
;; Replace x with a de bruijn index, by running a CIC term at
;; compile time.
(normalize/syn
#`((lambda (x : stlc-term)
(stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
(Var-->-stlc-term (avar #,oldindex)))))]
[(quote (e1 e2)) [(quote (e1 e2))
#`(stlc-cons #,(stlc #'e1 d) #,(stlc #'e2 d))] #`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))]
[(let (x y) = e1 in e2) [(let (x y) = e1 in e2)
#`(stlc-let #,(stlc #'t d) #,(stlc #'e1 d) (let* ([y index]
#,(stlc #'e2 (dict-set* (dict-shift (dict-shift d)) [x #`(s #,y)])
(syntax->datum #'x) #`z (set! index #`(s (s #,index)))
(syntax->datum #'y) #`(s z))))] #`((lambda (x : stlc-term) (y : stlc-term)
(stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
#,(stlc #'e2)))
(Var-->-stlc-term (avar #,x))
(Var-->-stlc-term (avar #,y))))
#`(let x i #,(stlc #'e1))]
[(e1 e2) [(e1 e2)
#`(stlc-app #,(stlc #'e1 d) #,(stlc #'e2 d))] #`(stlc-app #,(stlc #'e1) #,(stlc #'e2))]
[() #'(stlc-val->stlc-term stlc-unit)] [() #'(stlc-val-->-stlc-term stlc-unit)]
[#t #'(stlc-val->stlc-term stlc-true)] [#t #'(stlc-val-->-stlc-term stlc-true)]
[#f #'(stlc-val->stlc-term stlc-false)] [#f #'(stlc-val-->-stlc-term stlc-false)]
[(t1 * t2) [(t1 * t2)
#`(stlc-* #,(stlc #'t1 d) #,(stlc #'t2 d))] #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))]
[(t1 -> t2) [(t1 -> t2)
#`(stlc--> #,(stlc #'t1 d) #,(stlc #'t2 d))] #`(stlc--> #,(stlc #'t1) #,(stlc #'t2))]
[bool #`stlc-boolty] [bool #`stlc-boolty]
[e [e
(cond (if (eq? 1 (syntax->datum #'e))
[(eq? 1 (syntax->datum #'e)) #'stlc-unitty
#'stlc-unitty] #'e)])))
[(dict-ref d (syntax->datum #'e) #f) =>
(lambda (x)
#`(Nat->stlc-term #,x))]
[else #'e])])))
(check-equal? (check-equal?
(begin-stlc (lambda (x : 1) x)) (begin-stlc (lambda (x : 1) x))
(stlc-lambda stlc-unitty (Nat->stlc-term z))) (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
(check-equal? (check-equal?
(begin-stlc ((lambda (x : 1) x) ())) (begin-stlc ((lambda (x : 1) x) ()))
(stlc-app (stlc-lambda stlc-unitty (Nat->stlc-term z)) (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
(stlc-val->stlc-term stlc-unit))) (stlc-val-->-stlc-term stlc-unit)))
(check-equal?
(begin-stlc (lambda (x : 1) (lambda (y : 1) x)))
(stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Nat->stlc-term (s z)))))
(check-equal? (check-equal?
(begin-stlc '(() ())) (begin-stlc '(() ()))
(stlc-cons (stlc-val->stlc-term stlc-unit) (stlc-cons (stlc-val-->-stlc-term stlc-unit)
(stlc-val->stlc-term stlc-unit))) (stlc-val-->-stlc-term stlc-unit)))
(check-equal? (check-equal?
(begin-stlc #t) (begin-stlc #t)
(stlc-val->stlc-term stlc-true)) (stlc-val-->-stlc-term stlc-true))

View File

@ -1,16 +0,0 @@
#lang sweet-exp cur
require
cur/stdlib/sugar
cur/stdlib/bool
cur/stdlib/nat
rackunit
check-equal?
if true false true
false
define + plus
check-equal?
{z + s(z)}
s(z)

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.4") "sweet-exp")) (define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
(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))