Better surface syntax. Closes #34
* Unified the surface syntax. There are no longer distinctions between single-arity and multi-arity function/function types. * Removed case and case*, in favor of match, a single advanced pattern matching construct. * Updated all libraries, tests and documentation to use these new syntax. * Some work to provide improved error messages in surface syntax.
This commit is contained in:
William J. Bowman
parent
e162ef3acc
commit
bf987cdb06
|
|
@ -12,7 +12,7 @@ This library defines the datatype @racket[List] and several functions on them.
|
|||
|
||||
@deftogether[(@defthing[List (-> Type Type)]
|
||||
@defthing[nil (forall (A : Type) (List A))]
|
||||
@defthing[cons (forall* (A : Type) (a : A) (-> (List A) (List A)))])]{
|
||||
@defthing[cons (forall (A : Type) (a : A) (-> (List A) (List A)))])]{
|
||||
The polymorphic list datatype.
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
"../defs.rkt"
|
||||
scribble/eval)
|
||||
|
||||
@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar)"))
|
||||
@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar cur/stdlib/list)"))
|
||||
|
||||
|
||||
@title{Sugar}
|
||||
|
|
@ -18,46 +18,36 @@ that expands into the eliminator.
|
|||
@defmodule[cur/stdlib/sugar]
|
||||
This library defines various syntactic extensions making Cur easier to write than writing raw TT.
|
||||
|
||||
@defform*[((-> t1 t2)
|
||||
(→ t1 t2))]{
|
||||
A non-dependent function type Equivalent to @racket[(forall (_ : t1) t2)], where @racket[_] indicates an variable that is not used.
|
||||
@defform*[((-> decl decl ... type)
|
||||
(→ decl decl ... type)
|
||||
(forall decl decl ... type)
|
||||
(∀ decl decl ... type))
|
||||
#:grammar
|
||||
[(decl
|
||||
type
|
||||
(code:line (identifier : type)))]]{
|
||||
A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(data And : (-> Type (-> Type Type))
|
||||
(conj : (forall (A : Type) (forall (B : Type) (-> A (-> B ((And A) B)))))))
|
||||
(data And : (-> Type Type)
|
||||
(conj : (-> (A : Type) (B : Type) A B ((And A) B))))
|
||||
((((conj Bool) Bool) true) false)]
|
||||
}
|
||||
|
||||
@defform*[((->* t ...)
|
||||
(→* t ...))]{
|
||||
A non-dependent multi-arity function type that supports automatic currying.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(data And : (->* Type Type Type)
|
||||
(conj : (forall (A : Type) (forall (B : Type) (->* A B ((And A) B))))))
|
||||
((((conj Bool) Bool) true) false)]
|
||||
}
|
||||
|
||||
|
||||
@defform*[((forall* (a : t) ... type)
|
||||
(∀* (a : t) ... type))]{
|
||||
A multi-arity function type that supports automatic currying.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(data And : (->* Type Type Type)
|
||||
(conj : (forall* (A : Type) (B : Type)
|
||||
(->* A B ((And A) B)))))
|
||||
(data And : (forall Type Type Type)
|
||||
(conj : (forall (A : Type) (B : Type) A B ((And A) B))))
|
||||
((((conj Bool) Bool) true) false)]
|
||||
|
||||
}
|
||||
|
||||
@defform*[((lambda* (a : t) ... body)
|
||||
(λ* (a : t) ... body))]{
|
||||
@defform*[((lambda (a : t) ... body)
|
||||
(λ (a : t) ... body))]{
|
||||
Defines a multi-arity procedure that supports automatic currying.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
((lambda (x : Bool) (lambda (y : Bool) y)) true)
|
||||
((lambda* (x : Bool) (y : Bool) y) true)
|
||||
((lambda (x : Bool) (y : Bool) y) true)
|
||||
]
|
||||
}
|
||||
|
||||
|
|
@ -65,20 +55,19 @@ Defines a multi-arity procedure that supports automatic currying.
|
|||
Defines multi-arity procedure application via automatic currying.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(data And : (->* Type Type Type)
|
||||
(conj : (forall* (A : Type) (B : Type)
|
||||
(->* A B ((And A) B)))))
|
||||
(data And : (-> Type Type Type)
|
||||
(conj : (-> (A : Type) (B : Type) A B ((And A) B))))
|
||||
(conj Bool Bool true false)]
|
||||
}
|
||||
|
||||
@defform*[((define name body)
|
||||
(define (name (x : t) ...) body))]{
|
||||
Like the @racket[define] provided by @racketmodname[cur/curnel/redex-lang], but supports
|
||||
defining curried functions via @racket[lambda*].
|
||||
Like the @racket[define] provided by @racketmodname[cur], but supports
|
||||
defining curried functions via @racket[lambda].
|
||||
}
|
||||
|
||||
@defform[(elim type motive-result-type e ...)]{
|
||||
Like the @racket[elim] provided by @racketmodname[cur/curnel/redex-lang], but supports
|
||||
Like the @racket[elim] provided by @racketmodname[cur], but supports
|
||||
automatically curries the remaining arguments @racket[e ...].
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
|
|
@ -90,12 +79,16 @@ automatically curries the remaining arguments @racket[e ...].
|
|||
|
||||
@defform*[((define-type name type)
|
||||
(define-type (name (a : t) ...) body))]{
|
||||
Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*].
|
||||
Like @racket[define], but uses @racket[forall] instead of @racket[lambda].
|
||||
}
|
||||
|
||||
@defform[(match e [pattern body] ...)
|
||||
@defform[(match e [maybe-in] [maybe-return] [pattern body] ...)
|
||||
#:grammar
|
||||
[(pattern
|
||||
[(maybe-in
|
||||
(code:line #:in type))
|
||||
(maybe-return
|
||||
(code:line #:return type))
|
||||
(pattern
|
||||
constructor
|
||||
(code:line (constructor (x : t) ...)))]]{
|
||||
A pattern-matcher-like syntax for inductive elimination.
|
||||
|
|
@ -108,6 +101,9 @@ Generates a call to the inductive eliminator for @racket[e].
|
|||
Currently does not work on inductive type-families as types indices
|
||||
are not inferred.
|
||||
|
||||
If @racket[#:in] is not specified, attempts to infer the type of @racket[e].
|
||||
If @racket[#:return] is not specified, attempts to infer the return type of the @racket[match].
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(match z
|
||||
[z true]
|
||||
|
|
@ -116,42 +112,32 @@ are not inferred.
|
|||
|
||||
@examples[#:eval curnel-eval
|
||||
(match (s z)
|
||||
#:in Nat
|
||||
#:return Bool
|
||||
[z true]
|
||||
[(s (n : Nat))
|
||||
(not (recur n))])]
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
((match (nil Bool)
|
||||
#:in (List Bool)
|
||||
[(nil (A : Type))
|
||||
(lambda (n : Nat)
|
||||
(none A))]
|
||||
[(cons (A : Type) (a : A) (rest : (List A)))
|
||||
(lambda (n : Nat)
|
||||
(match n
|
||||
[z (some A a)]
|
||||
[(s (n-1 : Nat))
|
||||
((recur rest) n-1)]))])
|
||||
z)]
|
||||
|
||||
}
|
||||
|
||||
@defform[(recur id)]{
|
||||
A form valid only in the body of a @racket[match] clause. Generates a
|
||||
reference to the induction hypothesis for @racket[x].
|
||||
}
|
||||
|
||||
|
||||
@defform[(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...)
|
||||
#:grammar
|
||||
[(pattern
|
||||
constructor
|
||||
(code:line)
|
||||
(code:line (constructor (x : t) ...)))
|
||||
(maybe-IH
|
||||
(code:line)
|
||||
(code:line IH: ((x : t) ...)))]]{
|
||||
A pattern-matcher-like syntax for inductive elimination that does not try to infer the type or motive.
|
||||
Necessary for more advanced types, like @racket[And], because @racket[case] is not very smart.
|
||||
|
||||
@margin-note{Don't worry about all that output from requiring prop}
|
||||
@examples[#:eval curnel-eval
|
||||
(case* Nat Type z () (lambda (x : Nat) Bool)
|
||||
[z true]
|
||||
[(s (n : Nat))
|
||||
IH: ((_ : Bool))
|
||||
false])
|
||||
(require cur/stdlib/prop)
|
||||
(case* And Type (conj Bool Nat true z) (Bool Nat)
|
||||
(lambda* (A : Type) (B : Type) (ab : (And A B)) A)
|
||||
[(conj (A : Type) (B : Type) (a : A) (b : B))
|
||||
IH: ()
|
||||
a])]
|
||||
A form valid only in the body of a @racket[match] clause.
|
||||
Generates a reference to the induction hypothesis for @racket[x]
|
||||
inferred by a @racket[match] clause.
|
||||
}
|
||||
|
||||
@defform[(let (clause ...) body)
|
||||
|
|
@ -182,8 +168,9 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if
|
|||
}
|
||||
|
||||
@defform[(run syn)]{
|
||||
Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
|
||||
computing part of the term from another Cur term.
|
||||
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
|
||||
another Cur term.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(lambda (x : (run (if true Bool Nat))) x)]
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ are @racket[t ...].
|
|||
|
||||
@examples[#:eval curnel-eval
|
||||
(typeclass (Eqv (A : Type))
|
||||
(equal? : (forall* (a : A) (b : A) Bool)))]
|
||||
(equal? : (forall (a : A) (b : A) Bool)))]
|
||||
}
|
||||
|
||||
@defform[(impl (class param) defs ...)]{
|
||||
|
|
|
|||
|
|
@ -31,11 +31,9 @@
|
|||
[dep-require require]
|
||||
|
||||
[dep-lambda lambda]
|
||||
[dep-lambda λ]
|
||||
[dep-app #%app]
|
||||
|
||||
[dep-forall forall]
|
||||
[dep-forall ∀]
|
||||
|
||||
[dep-inductive data]
|
||||
|
||||
|
|
@ -191,35 +189,29 @@
|
|||
reified-term)
|
||||
|
||||
(define (datum->cur syn t)
|
||||
(match t
|
||||
[(list (quote term) e)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(datum->cur syn e))]
|
||||
[(list (quote Unv) i)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(Type #,i))]
|
||||
[(list (quote Π) (list x (quote :) t) body)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
|
||||
[(list (quote λ) (list x (quote :) t) body)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
|
||||
[(list (list (quote elim) t1) t2)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))]
|
||||
[(list e1 e2)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
|
||||
[_
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
#,(datum->syntax syn t))]))
|
||||
(let datum->cur ([t t])
|
||||
(match t
|
||||
[(list (quote term) e)
|
||||
(quasisyntax/loc syn
|
||||
(datum->cur e))]
|
||||
[(list (quote Unv) i)
|
||||
(quasisyntax/loc syn
|
||||
(Type #,i))]
|
||||
[(list (quote Π) (list x (quote :) t) body)
|
||||
(quasisyntax/loc syn
|
||||
(dep-forall (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
|
||||
[(list (quote λ) (list x (quote :) t) body)
|
||||
(quasisyntax/loc syn
|
||||
(dep-lambda (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
|
||||
[(list (list (quote elim) t1) t2)
|
||||
(quasisyntax/loc syn
|
||||
(dep-elim #,(datum->cur t1) #,(datum->cur t2)))]
|
||||
[(list e1 e2)
|
||||
(quasisyntax/loc syn
|
||||
(dep-app #,(datum->cur e1) #,(datum->cur e2)))]
|
||||
[_
|
||||
(quasisyntax/loc syn
|
||||
#,(datum->syntax syn t))])))
|
||||
|
||||
(define (eval-cur syn)
|
||||
(term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
|
||||
|
|
@ -424,8 +416,8 @@
|
|||
(quasisyntax/loc syn (λ (x : t) e)))]))
|
||||
|
||||
(define-syntax (dep-app syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e1 e2)
|
||||
(syntax-parse syn
|
||||
[(_ e1:expr e2:expr)
|
||||
(syntax->curnel-syntax
|
||||
(quasisyntax/loc syn (#%app e1 e2)))]))
|
||||
|
||||
|
|
|
|||
|
|
@ -4,7 +4,8 @@
|
|||
(require
|
||||
"stdlib/sugar.rkt"
|
||||
"stdlib/nat.rkt"
|
||||
(only-in "cur.rkt" [#%app real-app] [elim real-elim]))
|
||||
;; TODO: "real-"? More like "curnel-"
|
||||
(only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
|
||||
|
||||
(provide
|
||||
define-relation
|
||||
|
|
@ -38,8 +39,7 @@
|
|||
x*:expr ...
|
||||
line:dash lab:id
|
||||
(name:id y* ...))
|
||||
#:with rule #'(lab : (forall* d ...
|
||||
(->* x* ... (name 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
|
||||
|
|
@ -62,7 +62,7 @@
|
|||
#: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 ...)])
|
||||
(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)
|
||||
|
|
@ -128,7 +128,7 @@
|
|||
#: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 ...))
|
||||
#: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 ...)))))
|
||||
|
||||
|
|
@ -243,7 +243,7 @@
|
|||
(syntax-parse (cur-expand syn #'define #'begin)
|
||||
;; TODO: Need to add these to a literal set and export it
|
||||
;; Or, maybe overwrite syntax-parse
|
||||
#:literals (lambda forall data real-app real-elim define begin Type)
|
||||
#:literals (real-lambda real-forall data real-app real-elim define begin Type)
|
||||
[(begin e ...)
|
||||
(for/fold ([str ""])
|
||||
([e (syntax->list #'(e ...))])
|
||||
|
|
@ -266,10 +266,10 @@
|
|||
(format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
|
||||
(output-coq #'body)))
|
||||
"")]
|
||||
[(lambda ~! (x:id (~datum :) t) body:expr)
|
||||
[(real-lambda ~! (x:id (~datum :) t) body:expr)
|
||||
(format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
|
||||
(output-coq #'body))]
|
||||
[(forall ~! (x:id (~datum :) t) body:expr)
|
||||
[(real-forall ~! (x:id (~datum :) t) body:expr)
|
||||
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
|
||||
(output-coq #'body))]
|
||||
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
|
||||
|
|
|
|||
|
|
@ -10,20 +10,28 @@
|
|||
cons
|
||||
list-ref)
|
||||
|
||||
(data List : (forall (A : Type) Type)
|
||||
(nil : (forall (A : Type) (List A)))
|
||||
(cons : (forall* (A : Type) (->* A (List A) (List A)))))
|
||||
(data List : (-> (A : Type) Type)
|
||||
(nil : (-> (A : Type) (List A)))
|
||||
(cons : (-> (A : Type) A (List A) (List A))))
|
||||
|
||||
(define list-ref
|
||||
(elim
|
||||
(define (list-ref (A : Type) (ls : (List A)))
|
||||
(match ls
|
||||
[(nil (A : Type)) (lambda (n : Nat) (none A))]
|
||||
[(cons (A : Type) (a : A) (rest : (List A)))
|
||||
(lambda (n : Nat)
|
||||
(match n
|
||||
[z (some A a)]
|
||||
[(s (n-1 : Nat))
|
||||
((recur rest) n-1)]))])
|
||||
#;(elim
|
||||
List
|
||||
Type
|
||||
(lambda* (A : Type) (ls : (List A))
|
||||
(lambda (A : Type) (ls : (List A))
|
||||
(-> Nat (Maybe A)))
|
||||
(lambda* (A : Type) (n : Nat) (none A))
|
||||
(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)])))))
|
||||
(lambda (A : Type) (n : Nat) (none A))
|
||||
(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)])))))
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
|
||||
(data Maybe : (forall (A : Type) Type)
|
||||
(none : (forall (A : Type) (Maybe A)))
|
||||
(some : (forall* (A : Type) (a : A) (Maybe A))))
|
||||
(some : (forall (A : Type) (a : A) (Maybe A))))
|
||||
|
||||
(define-syntax (some/i syn)
|
||||
(syntax-case syn ()
|
||||
|
|
|
|||
|
|
@ -35,17 +35,21 @@
|
|||
|
||||
(define square (run (exp (s (s z)))))
|
||||
|
||||
;; Credit to this function goes to Max
|
||||
(define nat-equal?
|
||||
(elim Nat Type (lambda (x : Nat) (-> Nat Bool))
|
||||
(elim Nat Type (lambda (x : Nat) Bool)
|
||||
true
|
||||
(lambda* (x : Nat) (ih-n2 : Bool) false))
|
||||
(lambda* (x : Nat) (ih : (-> Nat Bool))
|
||||
(elim Nat Type (lambda (x : Nat) Bool)
|
||||
false
|
||||
(lambda* (x : Nat) (ih-bla : Bool)
|
||||
(ih x))))))
|
||||
(define (zero? (n : Nat))
|
||||
(match n
|
||||
[z true]
|
||||
[(s (n : Nat))
|
||||
false]))
|
||||
|
||||
(define (nat-equal? (n : Nat))
|
||||
(match n
|
||||
[z zero?]
|
||||
[(s (n-1 : Nat))
|
||||
(lambda (m : Nat)
|
||||
(match m
|
||||
[z false]
|
||||
[(s (m-1 : Nat))
|
||||
((recur n-1) m-1)]))]))
|
||||
|
||||
(define (even? (n : Nat))
|
||||
(match n
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@
|
|||
|
||||
(define-type (Not (A : Type)) (-> A False))
|
||||
|
||||
(data And : (forall* (A : Type) (B : Type) Type)
|
||||
(conj : (forall* (A : Type) (B : Type)
|
||||
(data And : (forall (A : Type) (B : Type) Type)
|
||||
(conj : (forall (A : Type) (B : Type)
|
||||
(x : A) (y : B) (And A B))))
|
||||
|
||||
(define-syntax (conj/i syn)
|
||||
|
|
@ -36,52 +36,49 @@
|
|||
#`(conj #,a-type #,b-type a b))]))
|
||||
|
||||
(define thm:and-is-symmetric
|
||||
(forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
|
||||
(forall (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
|
||||
|
||||
(define pf:and-is-symmetric
|
||||
(lambda* (P : Type) (Q : Type) (ab : (And P Q))
|
||||
(case* And Type ab (P Q)
|
||||
(lambda* (P : Type) (Q : Type) (ab : (And P Q))
|
||||
(And Q P))
|
||||
((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
|
||||
(lambda (P : Type) (Q : Type) (ab : (And P Q))
|
||||
(match ab
|
||||
[(conj (P : Type) (Q : Type) (x : P) (y : Q))
|
||||
(conj/i y x)])))
|
||||
|
||||
(define thm:proj1
|
||||
(forall* (A : Type) (B : Type) (c : (And A B)) A))
|
||||
(forall (A : Type) (B : Type) (c : (And A B)) A))
|
||||
|
||||
(define pf:proj1
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B))
|
||||
(case* And Type c (A B)
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B)) A)
|
||||
((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
|
||||
(lambda (A : Type) (B : Type) (c : (And A B))
|
||||
(match c
|
||||
[(conj (A : Type) (B : Type) (a : A) (b : B)) a])))
|
||||
|
||||
(define thm:proj2
|
||||
(forall* (A : Type) (B : Type) (c : (And A B)) B))
|
||||
(forall (A : Type) (B : Type) (c : (And A B)) B))
|
||||
|
||||
(define pf:proj2
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B))
|
||||
(case* And Type c (A B)
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B)) B)
|
||||
((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
|
||||
(lambda (A : Type) (B : Type) (c : (And A B))
|
||||
(match c
|
||||
[(conj (A : Type) (B : Type) (a : A) (b : B)) b])))
|
||||
|
||||
#| TODO: Disabled until #22 fixed
|
||||
(data Or : (forall* (A : Type) (B : Type) Type)
|
||||
(left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
|
||||
(right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
|
||||
(data Or : (forall (A : Type) (B : Type) Type)
|
||||
(left : (forall (A : Type) (B : Type) (a : A) (Or A B)))
|
||||
(right : (forall (A : Type) (B : Type) (b : B) (Or A B))))
|
||||
|
||||
(define-theorem thm:A-or-A
|
||||
(forall* (A : Type) (o : (Or A A)) A))
|
||||
(forall (A : Type) (o : (Or A A)) 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?
|
||||
(elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
|
||||
(lambda* (A : Type) (B : Type) (a : A) a)
|
||||
(elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
|
||||
(lambda (A : Type) (B : Type) (a : A) 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)
|
||||
A A c)))
|
||||
|
||||
(qed thm:A-or-A proof:A-or-A)
|
||||
|#
|
||||
|
||||
(data == : (forall* (A : Type) (x : A) (-> A Type))
|
||||
(refl : (forall* (A : Type) (x : A) (== A x x))))
|
||||
(data == : (forall (A : Type) (x : A) (-> A Type))
|
||||
(refl : (forall (A : Type) (x : A) (== A x x))))
|
||||
|
|
|
|||
|
|
@ -1,20 +1,16 @@
|
|||
#lang s-exp "../cur.rkt"
|
||||
(provide
|
||||
->
|
||||
->*
|
||||
forall*
|
||||
lambda*
|
||||
lambda
|
||||
(rename-out
|
||||
[-> →]
|
||||
[->* →*]
|
||||
[lambda* λ*]
|
||||
[forall* ∀*])
|
||||
[-> forall]
|
||||
[-> ∀]
|
||||
[lambda λ])
|
||||
#%app
|
||||
define
|
||||
elim
|
||||
define-type
|
||||
case
|
||||
case*
|
||||
match
|
||||
recur
|
||||
let
|
||||
|
|
@ -32,127 +28,245 @@
|
|||
(only-in "../cur.rkt"
|
||||
[elim real-elim]
|
||||
[#%app real-app]
|
||||
;; Somehow, using real-lambda instead of _lambda causes weird import error
|
||||
[lambda real-lambda]
|
||||
#;[forall real-forall]
|
||||
[define real-define]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class result-type
|
||||
(pattern type:expr))
|
||||
|
||||
(define-syntax-class parameter-declaration
|
||||
(pattern (name:id (~datum :) type:expr))
|
||||
|
||||
(pattern
|
||||
type:expr
|
||||
#:attr name (format-id #'type "~a" (gensym 'anon-parameter)))))
|
||||
|
||||
;; A multi-arity function type; takes parameter declaration of either
|
||||
;; a binding (name : type), or type whose name is generated.
|
||||
;; E.g.
|
||||
;; (-> (A : Type) A A)
|
||||
(define-syntax (-> syn)
|
||||
(syntax-case syn ()
|
||||
[(_ t1 t2) #`(forall (#,(gensym) : t1) t2)]))
|
||||
(syntax-parse syn
|
||||
[(_ d:parameter-declaration ...+ result:result-type)
|
||||
(foldr (lambda (src name type r)
|
||||
(quasisyntax/loc src
|
||||
(forall (#,name : #,type) #,r)))
|
||||
#'result
|
||||
(attribute d)
|
||||
(attribute d.name)
|
||||
(attribute d.type))]))
|
||||
|
||||
(define-syntax ->*
|
||||
(syntax-rules ()
|
||||
[(->* a) a]
|
||||
[(->* a a* ...)
|
||||
(-> a (->* a* ...))]))
|
||||
;; TODO: Add forall macro that allows specifying *names*, with types
|
||||
;; inferred. unlike -> which require types but not names
|
||||
;; E.g.
|
||||
;; (forall x (y : Nat) (== Nat x y))
|
||||
|
||||
(define-syntax forall*
|
||||
(syntax-rules (:)
|
||||
[(_ (a : t) (ar : tr) ... b)
|
||||
(forall (a : t)
|
||||
(forall* (ar : tr) ... b))]
|
||||
[(_ b) b]))
|
||||
|
||||
(define-syntax lambda*
|
||||
(syntax-rules (:)
|
||||
[(_ (a : t) (ar : tr) ... b)
|
||||
(lambda (a : t)
|
||||
(lambda* (ar : tr) ... b))]
|
||||
[(_ b) b]))
|
||||
;; TODO: Allows argument-declarations to have types inferred, similar
|
||||
;; to above TODO forall
|
||||
(begin-for-syntax
|
||||
;; eta-expand syntax-class for error messages
|
||||
(define-syntax-class argument-declaration
|
||||
(pattern
|
||||
e:parameter-declaration
|
||||
#:attr name #'e.name
|
||||
#:attr type #'e.type)))
|
||||
(define-syntax (lambda syn)
|
||||
(syntax-parse syn
|
||||
[(_ d:argument-declaration ...+ body:expr)
|
||||
(foldr (lambda (src name type r)
|
||||
(quasisyntax/loc src
|
||||
(real-lambda (#,name : #,type) #,r)))
|
||||
#'body
|
||||
(attribute d)
|
||||
(attribute d.name)
|
||||
(attribute d.type))]))
|
||||
|
||||
;; TODO: This makes for really bad error messages when an identifier is undefined.
|
||||
(define-syntax (#%app syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e) #'e]
|
||||
[(_ e)
|
||||
(quasisyntax/loc syn e)]
|
||||
[(_ e1 e2)
|
||||
#'(real-app e1 e2)]
|
||||
(quasisyntax/loc syn
|
||||
(real-app e1 e2))]
|
||||
[(_ e1 e2 e3 ...)
|
||||
#'(#%app (#%app e1 e2) e3 ...)]))
|
||||
(quasisyntax/loc syn
|
||||
(#%app (#%app e1 e2) e3 ...))]))
|
||||
|
||||
(define-syntax define-type
|
||||
(syntax-rules ()
|
||||
[(_ (name (a : t) ...) body)
|
||||
(define name (forall* (a : t) ... body))]
|
||||
(define name (forall (a : t) ... body))]
|
||||
[(_ name type)
|
||||
(define name type)]))
|
||||
|
||||
;; TODO: Allow inferring types as in above TODOs for lambda, forall
|
||||
(define-syntax (define syn)
|
||||
(syntax-case syn ()
|
||||
[(define (name (x : t) ...) body)
|
||||
#'(real-define name (lambda* (x : t) ... body))]
|
||||
(quasisyntax/loc syn
|
||||
(real-define name (lambda (x : t) ... body)))]
|
||||
[(define id body)
|
||||
#'(real-define id body)]))
|
||||
(quasisyntax/loc syn
|
||||
(real-define id body))]))
|
||||
|
||||
(define-syntax-rule (elim t1 t2 e ...)
|
||||
((real-elim t1 t2) e ...))
|
||||
|
||||
;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
|
||||
(begin-for-syntax
|
||||
(define (rewrite-clause clause)
|
||||
(syntax-case clause (: IH:)
|
||||
[((con (a : A) ...) IH: ((x : t) ...) body)
|
||||
#'(lambda* (a : A) ... (x : t) ... body)]
|
||||
[(e body) #'body])))
|
||||
|
||||
;; TODO: Expects clauses in same order as constructors as specified when
|
||||
;; TODO: inductive D is defined.
|
||||
;; TODO: Assumes D has no parameters
|
||||
(define-syntax (case syn)
|
||||
;; duplicated code
|
||||
(define (clause-body syn)
|
||||
(syntax-case (car (syntax->list syn)) (: IH:)
|
||||
[((con (a : A) ...) IH: ((x : t) ...) body) #'body]
|
||||
[(e body) #'body]))
|
||||
(syntax-case syn (=>)
|
||||
[(_ e clause* ...)
|
||||
(let* ([D (type-infer/syn #'e)]
|
||||
[M (type-infer/syn (clause-body #'(clause* ...)))]
|
||||
[U (type-infer/syn M)])
|
||||
#`(elim #,D #,U (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
|
||||
e))]))
|
||||
|
||||
(define-syntax (case* syn)
|
||||
(syntax-case syn ()
|
||||
[(_ D U e (p ...) P clause* ...)
|
||||
#`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-struct clause (args types decl body))
|
||||
(define ih-dict (make-hash))
|
||||
(define (clause-parse syn)
|
||||
(syntax-case syn (:)
|
||||
[((con (a : A) ...) body)
|
||||
(make-clause (syntax->list #'(a ...)) (syntax->list #'(A ...)) #'((a : A) ...) #'body)]
|
||||
[(e body)
|
||||
(make-clause '() '() #'() #'body)]))
|
||||
|
||||
(define (infer-result clauses)
|
||||
(or
|
||||
(for/or ([clause clauses])
|
||||
(type-infer/syn
|
||||
(clause-body clause)
|
||||
#:local-env (for/fold ([d '()])
|
||||
([arg (clause-args clause)]
|
||||
[type (clause-types clause)])
|
||||
(dict-set d arg type))))
|
||||
(raise-syntax-error
|
||||
'match
|
||||
"Could not infer type of result."
|
||||
(clause-body (car clauses)))))
|
||||
(define-syntax-class curried-application
|
||||
(pattern
|
||||
((~literal real-app) name:id e:expr)
|
||||
#:attr args
|
||||
(list #'e))
|
||||
|
||||
(define (infer-ihs D motive args types)
|
||||
(for/fold ([ih-dict (make-immutable-hash)])
|
||||
([type-syn types]
|
||||
[arg-syn args]
|
||||
;; NB: Non-hygenic
|
||||
#:when (cur-equal? type-syn D))
|
||||
(dict-set ih-dict (syntax->datum arg-syn) `(,(format-id arg-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn)))))
|
||||
(pattern
|
||||
((~literal real-app) a:curried-application e:expr)
|
||||
#:attr name #'a.name
|
||||
#:attr args
|
||||
;; TODO BUG: repeated appends are not performant; cons then reverse in inductive-type-declaration
|
||||
(append
|
||||
(attribute a.args)
|
||||
(list #'e))))
|
||||
|
||||
(define (clause->method D motive clause)
|
||||
(dict-clear! ih-dict)
|
||||
(let* ([ihs (infer-ihs D motive (clause-args clause) (clause-types clause))]
|
||||
[ih-args (dict-map
|
||||
ihs
|
||||
(lambda (k v)
|
||||
(dict-set! ih-dict k (car v))
|
||||
#`(#,(car v) : #,(cdr v))))])
|
||||
#`(lambda* #,@(clause-decl clause) #,@ih-args #,(clause-body clause)))))
|
||||
(define-syntax-class inductive-type-declaration
|
||||
(pattern
|
||||
x:id
|
||||
#:attr inductive-name
|
||||
#'x
|
||||
#:attr indices
|
||||
'()
|
||||
#:attr decls
|
||||
(list #`(#,(gensym 'anon-discriminant) : x))
|
||||
#:attr abstract-indices
|
||||
values)
|
||||
|
||||
(pattern
|
||||
;; BUG TODO NB: Because the inductive type may have been inferred, it may appear in Curnel syntax, i.e., nested applications starting with dep-app
|
||||
;; Best to ensure it *always* is in Curnel form, and pattern match on that.
|
||||
a:curried-application
|
||||
#:attr inductive-name
|
||||
(attribute a.name)
|
||||
#:attr indices
|
||||
(attribute a.args)
|
||||
#:attr names
|
||||
(for/list ([e (attribute indices)])
|
||||
(format-id e "~a" (gensym 'anon-index)))
|
||||
#:attr types
|
||||
;; TODO: Detect failure, report error/suggestions
|
||||
(for/list ([e (attribute indices)])
|
||||
(or (type-infer/syn e)
|
||||
(raise-syntax-error
|
||||
'match
|
||||
(format
|
||||
"Could not infer type of index ~a"
|
||||
e)
|
||||
e)))
|
||||
#:attr decls
|
||||
(append
|
||||
(for/list ([name (attribute names)]
|
||||
[type (attribute types)]
|
||||
[src (attribute indices)])
|
||||
(quasisyntax/loc src
|
||||
(#,name : #,type)))
|
||||
(list
|
||||
(quasisyntax/loc #'a
|
||||
(#,(gensym 'anon-discriminant) : (inductive-name #,@(attribute names))))))
|
||||
#:attr abstract-indices
|
||||
(lambda (return)
|
||||
;; NB: unhygenic
|
||||
;; Normalize at compile-time, for efficiency at run-time
|
||||
(normalize/syn
|
||||
#`((lambda
|
||||
;; 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
|
||||
#,@(for/list ([name (attribute indices)]
|
||||
[type (attribute types)])
|
||||
#`(#,name : #,type))
|
||||
#,return)
|
||||
#,@(attribute names))))))
|
||||
|
||||
;; todo: Support just names, inferring types
|
||||
(define-syntax-class match-declaration
|
||||
(pattern
|
||||
;; TODO: Use parameter-declaration defined earlier
|
||||
(name:id (~datum :) type:expr)
|
||||
#:attr decl
|
||||
#'(name : type)))
|
||||
|
||||
(define-syntax-class match-prepattern
|
||||
;; TODO: Check that x is a valid constructor for the inductive type
|
||||
(pattern
|
||||
x:id
|
||||
#:attr local-env
|
||||
'()
|
||||
#:attr decls
|
||||
'()
|
||||
#:attr types
|
||||
'()
|
||||
#:attr names
|
||||
'())
|
||||
|
||||
(pattern
|
||||
(x:id d:match-declaration ...+)
|
||||
#:attr local-env
|
||||
(for/fold ([d (make-immutable-hash)])
|
||||
([name (attribute d.name)]
|
||||
[type (attribute d.type)])
|
||||
(dict-set d name type))
|
||||
#:attr decls
|
||||
(attribute d.decl)
|
||||
#:attr names
|
||||
(attribute d.name)
|
||||
#:attr types
|
||||
(attribute d.type)))
|
||||
|
||||
(define-syntax-class (match-pattern D motive)
|
||||
(pattern
|
||||
d:match-prepattern
|
||||
#:attr decls
|
||||
;; Infer the inductive hypotheses, add them to the pattern decls
|
||||
;; and update the dictionarty for the recur form
|
||||
(for/fold ([decls (attribute d.decls)])
|
||||
([type-syn (attribute d.types)]
|
||||
[name-syn (attribute d.names)]
|
||||
[src (attribute d.decls)]
|
||||
;; NB: Non-hygenic
|
||||
;; BUG TODO: This fails when D is an inductive applied to arguments...
|
||||
#:when (cur-equal? type-syn D))
|
||||
(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))]
|
||||
;; Normalize at compile-time, for efficiency at run-time
|
||||
[ih-type (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))])
|
||||
(dict-set! ih-dict (syntax->datum name-syn) ih-name)
|
||||
(append decls (list #`(#,ih-name : #,ih-type)))))))
|
||||
|
||||
(define-syntax-class (match-preclause maybe-return-type)
|
||||
(pattern
|
||||
(p:match-prepattern b:expr)
|
||||
#:attr return-type
|
||||
;; TODO: Check that the infered type matches maybe-return-type, if it is provied
|
||||
(or maybe-return-type
|
||||
;; Ignore errors when trying to infer this type; other attempt might succeed
|
||||
(with-handlers ([values (lambda _ #f)])
|
||||
(type-infer/syn #:local-env (attribute p.local-env) #'b)))))
|
||||
|
||||
(define-syntax-class (match-clause D motive)
|
||||
(pattern
|
||||
((~var p (match-pattern D motive))
|
||||
;; TODO: nothing more advanced?
|
||||
b:expr)
|
||||
#:attr method
|
||||
(quasisyntax/loc #'p
|
||||
#,(if (null? (attribute p.decls))
|
||||
#'b
|
||||
#`(lambda #,@(attribute p.decls) b))))))
|
||||
|
||||
(define-syntax (recur syn)
|
||||
(syntax-case syn ()
|
||||
|
|
@ -163,23 +277,55 @@
|
|||
(lambda ()
|
||||
(raise-syntax-error
|
||||
'match
|
||||
(format "Cannot recur on ~a" (syntax->datum #'id))
|
||||
;; TODO: Detect when inside a match to provide better error
|
||||
(format
|
||||
"Cannot recur on ~a. Ether not inside a match or ~a is not an inductive argument."
|
||||
(syntax->datum #'id)
|
||||
(syntax->datum #'id))
|
||||
syn)))]))
|
||||
|
||||
;; TODO: Test
|
||||
(define-syntax (match syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e clause* ...)
|
||||
(let* ([clauses (map clause-parse (syntax->list #'(clause* ...)))]
|
||||
[R (infer-result clauses)]
|
||||
[D (or (type-infer/syn #'e)
|
||||
(raise-syntax-error 'match "Could not infer discrimnant's type." syn))]
|
||||
[motive #`(lambda (x : #,D) #,R)]
|
||||
[U (type-infer/syn R)])
|
||||
#`((elim #,D #,U)
|
||||
#,motive
|
||||
#,@(map (curry clause->method D motive) clauses)
|
||||
e))]))
|
||||
(syntax-parse syn
|
||||
[(_ d
|
||||
~!
|
||||
(~optional
|
||||
(~seq #:in ~! t)
|
||||
#:defaults
|
||||
([t (or (type-infer/syn #'d)
|
||||
(raise-syntax-error
|
||||
'match
|
||||
"Could not infer discrimnant's type. Try using #:in to declare it."
|
||||
syn))]))
|
||||
(~optional (~seq #:return ~! maybe-return-type))
|
||||
(~peek (~seq (~var prec (match-preclause (attribute maybe-return-type))) ...))
|
||||
~!
|
||||
(~parse D:inductive-type-declaration (cur-expand (attribute t)))
|
||||
(~bind (return-type (ormap values (attribute prec.return-type))))
|
||||
(~do (unless (attribute return-type)
|
||||
(raise-syntax-error
|
||||
'match
|
||||
"Could not infer return type. Try using #:return to declare it."
|
||||
syn)))
|
||||
;; BUG TODO: return-type is inferred with the indexes of the branches, but those must be abstracted in the motive...
|
||||
;; Replace each of the D.indicies with the equivalent name from D.decls
|
||||
(~bind (motive (quasisyntax/loc syn
|
||||
(lambda #,@(attribute D.decls)
|
||||
#,((attribute D.abstract-indices) (attribute return-type))))))
|
||||
(~var c (match-clause (attribute D) (attribute motive))) ...)
|
||||
;; TODO: Make all syntax extensions type check, report good error, rather than fail at Curnel
|
||||
(quasisyntax/loc syn
|
||||
(elim
|
||||
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
|
||||
c.method ...
|
||||
#,@(attribute D.indices)
|
||||
d))]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class let-clause
|
||||
|
|
@ -206,7 +352,7 @@
|
|||
(define-syntax (let syn)
|
||||
(syntax-parse syn
|
||||
[(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. This forces a term to be
|
||||
;; checked against a particular type.
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@
|
|||
(define (process-def def)
|
||||
(syntax-case def (define)
|
||||
[(define (name (a : t) ...) body ...)
|
||||
(values (syntax->datum #'name) #'(lambda* (a : t) ... body ...))]
|
||||
(values (syntax->datum #'name) #'(lambda (a : t) ... body ...))]
|
||||
[(define name body)
|
||||
(values (syntax->datum #'name) #'body)]))
|
||||
(syntax-case syn ()
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@
|
|||
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
|
||||
(second (string-split t "\n"))))
|
||||
(let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
|
||||
(lambda* (x : nat) (ih-x : nat) ih-x)
|
||||
(lambda (x : nat) (ih-x : nat) ih-x)
|
||||
e))])
|
||||
(check-regexp-match
|
||||
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
|
||||
|
|
@ -75,7 +75,7 @@
|
|||
(check-regexp-match
|
||||
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
|
||||
(parameterize ([coq-defns ""])
|
||||
(output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
|
||||
(output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
|
||||
(== nat (plus n m) (plus m n)))))
|
||||
(coq-defns)))
|
||||
(check-regexp-match
|
||||
|
|
|
|||
|
|
@ -17,24 +17,24 @@
|
|||
(:: (cons Bool true (nil Bool)) (List Bool)))
|
||||
(check-equal?
|
||||
(void)
|
||||
(:: (lambda* (A : Type) (a : A)
|
||||
(:: (lambda (A : Type) (a : A)
|
||||
(ih-a : (-> Nat (Maybe A)))
|
||||
(n : Nat)
|
||||
(match n
|
||||
[z (some A a)]
|
||||
[(s (n-1 : Nat))
|
||||
(ih-a n-1)]))
|
||||
(forall* (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
|
||||
(forall (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
|
||||
(n : Nat)
|
||||
(Maybe A))))
|
||||
(check-equal?
|
||||
(void)
|
||||
(:: (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?
|
||||
(void)
|
||||
(:: (elim List Type (lambda* (A : Type) (ls : (List A)) Nat)
|
||||
(:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
|
||||
(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)
|
||||
Bool
|
||||
(nil Bool))
|
||||
|
|
@ -43,7 +43,7 @@
|
|||
|
||||
(check-equal?
|
||||
(void)
|
||||
(:: list-ref (forall (A : Type) (->* (List A) Nat (Maybe A)))))
|
||||
(:: list-ref (forall (A : Type) (-> (List A) Nat (Maybe A)))))
|
||||
(check-equal?
|
||||
((list-ref Bool (cons Bool true (nil Bool))) z)
|
||||
(some Bool true))
|
||||
|
|
|
|||
|
|
@ -11,11 +11,10 @@
|
|||
(some Bool true))
|
||||
;; Disabled until #22 fixed
|
||||
#;(check-equal?
|
||||
(case* Maybe Type (some Bool true) (Bool)
|
||||
(lambda* (A : Type) (x : (Maybe A)) A)
|
||||
[(none (A : Type)) IH: ()
|
||||
false]
|
||||
[(some (A : Type) (x : A)) IH: ()
|
||||
;; TODO: Don't know how to use dependency yet
|
||||
(if x true false)])
|
||||
(match (some Bool true)
|
||||
[(none (A : Type))
|
||||
false]
|
||||
[(some (A : Type) (x : A))
|
||||
;; TODO: Don't know how to use dependency yet
|
||||
(if x true false)])
|
||||
true)
|
||||
|
|
|
|||
|
|
@ -11,8 +11,8 @@
|
|||
(:: pf:proj1 thm:proj1)
|
||||
(:: pf:proj2 thm:proj2)
|
||||
(check-equal?
|
||||
(elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
|
||||
(λ* (A : Type) (x : A) z)
|
||||
(elim == Type (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
|
||||
(λ (A : Type) (x : A) z)
|
||||
Bool
|
||||
true
|
||||
true
|
||||
|
|
|
|||
|
|
@ -5,19 +5,19 @@
|
|||
|
||||
;; TODO: Missing tests for match, others
|
||||
(check-equal?
|
||||
((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
|
||||
((λ (x : (Type 1)) (y : (∀ (x : (Type 1)) (Type 1))) (y x))
|
||||
Type
|
||||
(λ (x : (Type 1)) x))
|
||||
Type)
|
||||
|
||||
(check-equal?
|
||||
((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
|
||||
((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
|
||||
Type
|
||||
(λ (x : (Type 1)) x))
|
||||
Type)
|
||||
|
||||
(check-equal?
|
||||
((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
|
||||
((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
|
||||
Type
|
||||
(λ (x : (Type 1)) x))
|
||||
Type)
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
cur/stdlib/typeclass)
|
||||
|
||||
(typeclass (Eqv (A : Type))
|
||||
(equal? : (forall* (a : A) (b : A) Bool)))
|
||||
(equal? : (forall (a : A) (b : A) Bool)))
|
||||
(impl (Eqv Bool)
|
||||
(define (equal? (a : Bool) (b : Bool))
|
||||
(if a
|
||||
|
|
|
|||
|
|
@ -21,16 +21,15 @@
|
|||
;; TODO: Abstract this over stlc-type, and provide from in OLL
|
||||
(data Gamma : Type
|
||||
(emp-gamma : Gamma)
|
||||
(extend-gamma : (->* Gamma Var stlc-type Gamma)))
|
||||
(extend-gamma : (-> Gamma Var stlc-type Gamma)))
|
||||
|
||||
(define (lookup-gamma (g : Gamma) (x : Var))
|
||||
(case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
|
||||
(match g
|
||||
[emp-gamma (none stlc-type)]
|
||||
[(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
|
||||
IH: ((ih-g1 : (Maybe stlc-type)))
|
||||
(if (var-equal? v1 x)
|
||||
(some stlc-type t1)
|
||||
ih-g1)]))
|
||||
(recur g1))]))
|
||||
|
||||
(define-relation (has-type Gamma stlc-term stlc-type)
|
||||
#:output-coq "stlc.v"
|
||||
|
|
@ -97,7 +96,7 @@
|
|||
;; Replace x with a de bruijn index, by running a CIC term at
|
||||
;; compile time.
|
||||
(normalize/syn
|
||||
#`((lambda* (x : stlc-term)
|
||||
#`((lambda (x : stlc-term)
|
||||
(stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
|
||||
(Var-->-stlc-term (avar #,oldindex)))))]
|
||||
[(quote (e1 e2))
|
||||
|
|
@ -106,7 +105,7 @@
|
|||
(let* ([y index]
|
||||
[x #`(s #,y)])
|
||||
(set! index #`(s (s #,index)))
|
||||
#`((lambda* (x : stlc-term) (y : stlc-term)
|
||||
#`((lambda (x : stlc-term) (y : stlc-term)
|
||||
(stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
|
||||
#,(stlc #'e2)))
|
||||
(Var-->-stlc-term (avar #,x))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user