start some eq tests; fix dep-ind (in dep-ind-fixed) so indices can depend on params
This commit is contained in:
Stephen Chang
parent
8eb637af0e
commit
84108c7300
717
turnstile/examples/dep-ind-fixed.rkt
Normal file
717
turnstile/examples/dep-ind-fixed.rkt
Normal file
|
|
@ -0,0 +1,717 @@
|
|||
#lang turnstile/lang
|
||||
|
||||
; a basic dependently-typed calculus
|
||||
; - with inductive datatypes
|
||||
|
||||
; created this new file to avoid breaking anything using dep-ind.rkt
|
||||
|
||||
; this file is mostly same as dep-ind.rkt but define-datatype has some fixes:
|
||||
; 1) params and indices must be applied separately
|
||||
; - for constructor (but not type constructor)
|
||||
; 2) allows indices to depend on param
|
||||
; 3) indices were not being inst with params
|
||||
; 4) arg refs were using x instead of Cx from new expansion
|
||||
; TODO: re-compute recur-x, ie recur-Cx
|
||||
|
||||
; Π λ ≻ ⊢ ≫ → ∧ (bidir ⇒ ⇐) τ⊑
|
||||
|
||||
(provide Type (rename-out [Type *])
|
||||
Π → ∀
|
||||
= eq-refl eq-elim
|
||||
λ (rename-out [app #%app]) ann
|
||||
define-datatype define define-type-alias
|
||||
)
|
||||
|
||||
;; TODO:
|
||||
;; - map #%datum to S and Z
|
||||
;; - rename define-type-alias to define
|
||||
;; - add "assistant" part
|
||||
;; - provide match and match/lambda so nat-ind can be fn
|
||||
;; - eg see https://gist.github.com/AndrasKovacs/6769513
|
||||
;; - add dependent existential
|
||||
;; - remove debugging code?
|
||||
|
||||
;; set (Type n) : (Type n+1)
|
||||
;; Type = (Type 0)
|
||||
(define-internal-type-constructor Type)
|
||||
(define-typed-syntax Type
|
||||
[:id ≫ --- [≻ (Type 0)]]
|
||||
[(_ n:exact-nonnegative-integer) ≫
|
||||
#:with n+1 (+ (syntax-e #'n) 1)
|
||||
-------------
|
||||
[≻ #,(syntax-property
|
||||
(syntax-property
|
||||
#'(Type- 'n) ':
|
||||
(syntax-property
|
||||
#'(Type- 'n+1)
|
||||
'orig
|
||||
(list #'(Type n+1))))
|
||||
'orig
|
||||
(list #'(Type n)))]])
|
||||
|
||||
(begin-for-syntax
|
||||
(define debug? #f)
|
||||
(define type-eq-debug? #f)
|
||||
(define debug-match? #f)
|
||||
|
||||
;; TODO: fix `type` stx class
|
||||
;; current-type and type stx class not working
|
||||
;; for case where var has type that is previous var
|
||||
;; that is not yet in tyenv
|
||||
;; eg in (Π ([A : *][a : A]) ...)
|
||||
;; expansion of 2nd type A will fail with unbound id err
|
||||
;;
|
||||
;; attempt 2
|
||||
;; (define old-type? (current-type?))
|
||||
;; (current-type?
|
||||
;; (lambda (t)
|
||||
;; (printf "t = ~a\n" (stx->datum t))
|
||||
;; (printf "ty = ~a\n" (stx->datum (typeof t)))
|
||||
;; (or (Type? (typeof t))
|
||||
;; (syntax-parse (typeof t)
|
||||
;; [((~literal Type-) n:exact-nonnegative-integer) #t]
|
||||
;; [_ #f]))))
|
||||
;; attempt 1
|
||||
;; (define old-type? (current-type?))
|
||||
;; (current-type?
|
||||
;; (lambda (t) (or (#%type? t) (old-type? t))))
|
||||
|
||||
|
||||
(define old-relation (current-typecheck-relation))
|
||||
(current-typecheck-relation
|
||||
(lambda (t1 t2)
|
||||
(define res
|
||||
;; expand (Type n) if unexpanded
|
||||
(or (syntax-parse t1
|
||||
[((~literal Type-) n)
|
||||
(typecheck? ((current-type-eval) t1) t2)]
|
||||
[_ #f])
|
||||
(old-relation t1 t2)))
|
||||
(when type-eq-debug?
|
||||
(pretty-print (stx->datum t1))
|
||||
(pretty-print (stx->datum t2))
|
||||
(printf "res: ~a\n" res))
|
||||
res))
|
||||
;; used to attach type after app/eval
|
||||
;; but not all apps will have types, eg
|
||||
;; - internal type representation
|
||||
;; - intermediate elim terms
|
||||
(define (maybe-assign-type e t)
|
||||
(if (syntax-e t) (assign-type e t) e)))
|
||||
|
||||
(define-internal-type-constructor →) ; equiv to Π with no uses on rhs
|
||||
(define-internal-binding-type ∀) ; equiv to Π with Type for all params
|
||||
|
||||
;; Π expands into combination of internal →- and ∀-
|
||||
;; uses "let*" syntax where X_i is in scope for τ_i+1 ...
|
||||
;; TODO: add tests to check this
|
||||
(define-typed-syntax (Π ([X:id : τ_in] ...) τ_out) ≫
|
||||
[[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ tyoutty]
|
||||
[τ_in ≫ τ_in- ⇒ tyinty] ...]
|
||||
;; check that types have type (Type _)
|
||||
;; must re-expand since (Type n) will have type unexpanded (Type n+1)
|
||||
#:with ((~Type _) ...) (stx-map (current-type-eval) #'(tyoutty tyinty ...))
|
||||
-------
|
||||
[⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ Type]
|
||||
#;[⊢ #,#`(∀- (X- ...)
|
||||
#,(assign-type
|
||||
#'(→- τ_in- ... τ_out-)
|
||||
#'#%type)) ⇒ #%type])
|
||||
|
||||
;; abbrevs for Π
|
||||
;; (→ τ_in τ_out) == (Π (unused : τ_in) τ_out)
|
||||
(define-simple-macro (→ τ_in ... τ_out)
|
||||
#:with (X ...) (generate-temporaries #'(τ_in ...))
|
||||
(Π ([X : τ_in] ...) τ_out))
|
||||
;; (∀ (X) τ) == (∀ ([X : Type]) τ)
|
||||
(define-simple-macro (∀ (X ...) τ)
|
||||
(Π ([X : Type] ...) τ))
|
||||
|
||||
;; pattern expanders
|
||||
(begin-for-syntax
|
||||
(define-syntax ~Π
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ ([x:id : τ_in] ... (~and (~literal ...) ooo)) τ_out)
|
||||
#'(~∀ (x ... ooo) (~→ τ_in ... ooo τ_out))]
|
||||
[(_ ([x:id : τ_in] ...) τ_out)
|
||||
#'(~∀ (x ...) (~→ τ_in ... τ_out))]))))
|
||||
|
||||
;; equality -------------------------------------------------------------------
|
||||
(define-internal-type-constructor =)
|
||||
(define-typed-syntax (= t1 t2) ≫
|
||||
[⊢ t1 ≫ t1- ⇒ ty]
|
||||
[⊢ t2 ≫ t2- ⇐ ty]
|
||||
;; #:do [(printf "t1: ~a\n" (stx->datum #'t1-))
|
||||
;; (printf "t2: ~a\n" (stx->datum #'t2-))]
|
||||
; [t1- τ= t2-]
|
||||
---------------------
|
||||
[⊢ (=- t1- t2-) ⇒ Type])
|
||||
|
||||
;; Q: what is the operational meaning of eq-refl?
|
||||
(define-typed-syntax (eq-refl e) ≫
|
||||
[⊢ e ≫ e- ⇒ _]
|
||||
----------
|
||||
[⊢ (#%app- void-) ⇒ (= e- e-)])
|
||||
|
||||
;; eq-elim: t : T
|
||||
;; P : (T -> Type)
|
||||
;; pt : (P t)
|
||||
;; w : T
|
||||
;; peq : (= t w)
|
||||
;; -> (P w)
|
||||
(define-typed-syntax (eq-elim t P pt w peq) ≫
|
||||
[⊢ t ≫ t- ⇒ ty]
|
||||
[⊢ P ≫ P- ⇐ (→ ty Type)]
|
||||
[⊢ pt ≫ pt- ⇐ (app P- t-)]
|
||||
[⊢ w ≫ w- ⇐ ty]
|
||||
[⊢ peq ≫ peq- ⇐ (= t- w-)]
|
||||
--------------
|
||||
[⊢ pt- ⇒ (app P- w-)])
|
||||
|
||||
;; lambda and #%app -----------------------------------------------------------
|
||||
|
||||
;; TODO: fix `type` stx class
|
||||
(define-typed-syntax λ
|
||||
;; expected ty only
|
||||
[(_ (y:id ...) e) ⇐ (~Π ([x:id : τ_in] ... ) τ_out) ≫
|
||||
[[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out]
|
||||
---------
|
||||
[⊢ (λ- (x- ...) e-)]]
|
||||
;; both expected ty and annotations
|
||||
[(_ ([y:id : τ_in*] ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫
|
||||
; [(_ ([y:id : τy_in:type] ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫
|
||||
#:fail-unless (stx-length=? #'(y ...) #'(x ...))
|
||||
"function's arity does not match expected type"
|
||||
[⊢ τ_in* ≫ τ_in** ⇐ Type] ...
|
||||
; #:when (typechecks? (stx-map (current-type-eval) #'(τ_in* ...))
|
||||
#:when (typechecks? #'(τ_in** ...) #'(τ_in ...))
|
||||
; #:when (typechecks? #'(τy_in.norm ...) #'(τ_in ...))
|
||||
; [τy_in τ= τ_in] ...
|
||||
[[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out]
|
||||
-------
|
||||
[⊢ (λ- (x- ...) e-)]]
|
||||
;; annotations only
|
||||
[(_ ([x:id : τ_in] ...) e) ≫
|
||||
[[x ≫ x- : τ_in] ... ⊢ [e ≫ e- ⇒ τ_out] [τ_in ≫ τ_in- ⇒ _] ...]
|
||||
-------
|
||||
[⊢ (λ- (x- ...) e-) ⇒ (Π ([x- : τ_in-] ...) τ_out)]])
|
||||
|
||||
;; helps debug which terms (app/evals) do not have types, eg
|
||||
;; - → in internal type representation
|
||||
;; - intermediate elim terms
|
||||
(define-for-syntax false-tys 0)
|
||||
|
||||
;; TODO: fix orig after subst, for err msgs
|
||||
;; app/eval should not try to ty check anymore
|
||||
(define-syntax app/eval
|
||||
(syntax-parser
|
||||
#;[(_ f . args) #:do[(printf "app/evaling ")
|
||||
(printf "f: ~a\n" (stx->datum #'f))
|
||||
(printf "args: ~a\n" (stx->datum #'args))]
|
||||
#:when #f #'void]
|
||||
[(_ f:id (_ matcher) (_ _ . args))
|
||||
#:do[(when debug-match?
|
||||
(printf "potential delayed match ~a ~a\n"
|
||||
(stx->datum #'matcher)
|
||||
(stx->datum #'args)))]
|
||||
#:with ty (typeof this-syntax)
|
||||
;; TODO: use pat expander instead
|
||||
#:with (_ m/d . _) (local-expand #'(#%app match/delayed 'dont 'care) 'expression null)
|
||||
#:when (free-identifier=? #'m/d #'f)
|
||||
#:do[(when debug-match? (printf "matching\n"))]
|
||||
;; TODO: need to attach type?
|
||||
#;[
|
||||
(unless (syntax-e #'ty)
|
||||
(displayln 3)
|
||||
(displayln #'ty)
|
||||
(set! false-tys (add1 false-tys))
|
||||
(displayln false-tys))]
|
||||
(maybe-assign-type #'(matcher . args) (typeof this-syntax))]
|
||||
;; TODO: apply to only lambda args or all args?
|
||||
[(_ (~and f ((~literal #%plain-lambda) (x ...) e)) e_arg ...)
|
||||
#:do[(when debug?
|
||||
(printf "apping: ~a\n" (stx->datum #'f))
|
||||
(printf "args\n")
|
||||
(pretty-print (stx->datum #'(e_arg ...))))]
|
||||
; #:with (~Π ([X : _] ...) τ_out) (typeof #'f) ; must re-subst in type
|
||||
;; TODO: need to replace all #%app- in this result with app/eval again
|
||||
;; and then re-expand
|
||||
; #:with ((~literal #%plain-app) newf . newargs) #'e
|
||||
; #:do[(displayln #'newf)(displayln #'newargs)(displayln (stx-car #'e+))]
|
||||
#:with r-app (datum->syntax (if (identifier? #'e) #'e (stx-car #'e)) '#%app)
|
||||
;; TODO: is this assign-type needed only for tests?
|
||||
;; eg, see id tests in dep2-peano.rkt
|
||||
#:with ty (typeof this-syntax)
|
||||
#:do[(when debug?
|
||||
(define ttt (typeof this-syntax))
|
||||
(define ttt2 (and ttt
|
||||
(substs #'(app/eval e_arg ...) #'(r-app x ...) ttt free-identifier=?)))
|
||||
(define ttt3 (and ttt2
|
||||
(local-expand ttt2 'expression null)))
|
||||
(printf "expected type\n")
|
||||
(pretty-print (stx->datum ttt))
|
||||
(pretty-print (stx->datum ttt2))
|
||||
(pretty-print (stx->datum ttt3)))]
|
||||
#:with e-inst (substs #'(app/eval e_arg ...) #'(r-app x ...) #'e free-identifier=?)
|
||||
;; some apps may not have type (eg in internal reps)
|
||||
#:with e+ (if (syntax-e #'ty)
|
||||
(assign-type
|
||||
#'e-inst
|
||||
(local-expand
|
||||
; (substs #'(app/eval e_arg ...) #'(r-app x ...) #'ty free-identifier=?)
|
||||
;; TODO: this is needed, which means there are some uneval'ed matches
|
||||
;; but is this the right place?
|
||||
;; eg, it wasnt waiting on any arg
|
||||
;; so that mean it could have been evaled but wasnt at some point
|
||||
(substs #'(app/eval) #'(r-app) #'ty free-identifier=?)
|
||||
'expression null))
|
||||
#'e-inst)
|
||||
#:do[(when debug?
|
||||
(displayln "res:--------------------")
|
||||
(pretty-print (stx->datum #'e+))
|
||||
;; (displayln "actual type:")
|
||||
;; (pretty-print (stx->datum (typeof #'e+)))
|
||||
(displayln "new type:")
|
||||
(pretty-print (stx->datum (typeof #'e+)))
|
||||
;; (displayln "res expanded:------------------------")
|
||||
;; (pretty-print
|
||||
;; (stx->datum (local-expand (substs #'(e_arg ...) #'(x ...) #'e) 'expression null)))
|
||||
(displayln "res app/eval re-expanding-----------------------"))]
|
||||
#:with ((~literal let-values) () ((~literal let-values) () e++))
|
||||
(local-expand
|
||||
#'(let-syntax (#;[app (make-rename-transformer #'app/eval)]
|
||||
#;[x (make-variable-like-transformer #'e_arg)]) e+)
|
||||
'expression null)
|
||||
#:do[(when debug?
|
||||
(pretty-print (stx->datum #'e++))
|
||||
; (pretty-print (stx->datum (typeof #'e++)))
|
||||
#;(local-expand
|
||||
#'(let-syntax ([app (make-rename-transformer #'app/eval)]
|
||||
#;[x (make-variable-like-transformer #'e_arg)]) e+)
|
||||
'expression null))]
|
||||
#;[(when (not (syntax-e #'ty))
|
||||
(displayln 1)
|
||||
(displayln (stx->datum this-syntax))
|
||||
(displayln #'ty)
|
||||
(set! false-tys (add1 false-tys))
|
||||
(displayln false-tys))]
|
||||
#'e++ #;(substs #'(e_arg ...) #'(x ...) #'e)]
|
||||
[(_ f . args)
|
||||
#:do[(when debug?
|
||||
(printf "not apping\n")
|
||||
(pretty-print (stx->datum #'f))
|
||||
(displayln "args")
|
||||
(pretty-print (stx->datum #'args)))]
|
||||
#:with f+ (expand/df #'f)
|
||||
#:with args+ (stx-map expand/df #'args)
|
||||
;; TODO: need to attach type?
|
||||
#:with ty (typeof this-syntax)
|
||||
#;[(unless (syntax-e #'ty)
|
||||
(displayln 2)
|
||||
(displayln (stx->datum this-syntax))
|
||||
(displayln #'ty)
|
||||
(displayln (syntax-property this-syntax '::))
|
||||
(set! false-tys (add1 false-tys))
|
||||
(displayln false-tys))]
|
||||
(syntax-parse #'f+
|
||||
[((~literal #%plain-lambda) . _)
|
||||
(maybe-assign-type #'(app/eval f+ . args+) #'ty)]
|
||||
[_
|
||||
;(maybe-assign-type
|
||||
#'(#%app- f+ . args+)
|
||||
;#'ty)
|
||||
])]))
|
||||
|
||||
;; TODO: fix orig after subst
|
||||
(define-typed-syntax app
|
||||
[(_ e_fn e_arg ...) ≫
|
||||
#:do[(when debug?
|
||||
(displayln "TYPECHECKING")
|
||||
(pretty-print (stx->datum this-syntax)))]
|
||||
; #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))]
|
||||
; [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)]
|
||||
[⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)]
|
||||
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
||||
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
|
||||
;; #:do[(displayln "expecting")
|
||||
;; (pretty-print (stx->datum #'(τ_in ...)))]
|
||||
;; [⊢ e_arg ≫ _ ⇒ ty2] ... ; typechecking args
|
||||
;; #:do[(displayln "got")
|
||||
;; (pretty-print (stx->datum (stx-map typeof #'(ty2 ...))))]
|
||||
[⊢ e_arg ≫ e_arg- ⇐ τ_in] ... ; typechecking args
|
||||
-----------------------------
|
||||
[⊢ (app/eval e_fn- e_arg- ...) ⇒ #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]])
|
||||
|
||||
(define-typed-syntax (ann e (~datum :) τ) ≫
|
||||
[⊢ e ≫ e- ⇐ τ]
|
||||
--------
|
||||
[⊢ e- ⇒ τ])
|
||||
|
||||
;; top-level ------------------------------------------------------------------
|
||||
;; TODO: shouldnt need define-type-alias, should be same as define
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(_ alias:id τ);τ:any-type)
|
||||
#'(define-syntax- alias
|
||||
(make-variable-like-transformer #'τ))]
|
||||
#;[(_ (f:id x:id ...) ty)
|
||||
#'(define-syntax- (f stx)
|
||||
(syntax-parse stx
|
||||
[(_ x ...)
|
||||
#:with τ:any-type #'ty
|
||||
#'τ.norm]))]))
|
||||
|
||||
;; TODO: delete this?
|
||||
(define-typed-syntax define
|
||||
[(_ x:id (~datum :) τ e:expr) ≫
|
||||
[⊢ e ≫ e- ⇐ τ]
|
||||
#:with y (generate-temporary #'x)
|
||||
#:with y+props (transfer-props #'e- #'y #:except '(origin))
|
||||
--------
|
||||
[≻ (begin-
|
||||
(define-syntax x (make-rename-transformer #'y+props))
|
||||
(define- y e-))]]
|
||||
[(_ x:id e) ≫
|
||||
;This won't work with mutually recursive definitions
|
||||
[⊢ e ≫ e- ⇒ _]
|
||||
#:with y (generate-temporary #'x)
|
||||
#:with y+props (transfer-props #'e- #'y #:except '(origin))
|
||||
--------
|
||||
[≻ (begin-
|
||||
(define-syntax x (make-rename-transformer #'y+props))
|
||||
(define- y e-))]]
|
||||
#;[(_ (f [x (~datum :) ty] ... (~or (~datum →) (~datum ->)) ty_out) e ...+) ≫
|
||||
#:with f- (add-orig (generate-temporary #'f) #'f)
|
||||
--------
|
||||
[≻ (begin-
|
||||
(define-syntax- f
|
||||
(make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
|
||||
(define- f-
|
||||
(stlc+lit:λ ([x : ty] ...)
|
||||
(stlc+lit:ann (begin e ...) : ty_out))))]])
|
||||
|
||||
|
||||
(define-typed-syntax (unsafe-assign-type e (~datum :) τ) ≫ --- [⊢ e ⇒ τ])
|
||||
|
||||
(struct TmpTy- ())
|
||||
(define-syntax TmpTy
|
||||
(syntax-parser
|
||||
[:id (assign-type #'TmpTy- #'Type)]
|
||||
[(_ . args) (assign-type #'(#%app TmpTy- . args) #'Type)]))
|
||||
|
||||
(struct match/delayed (name args) #:transparent)
|
||||
|
||||
(define-typed-syntax define-datatype
|
||||
;; datatype type `TY` is an id ----------------------------------------------
|
||||
;; - ie, no params or indices
|
||||
[(_ Name (~datum :) TY:id
|
||||
[C:id (~datum :) CTY] ...) ≫
|
||||
; need to expand `CTY` to find recur args,
|
||||
; but `Name` is still unbound so swap in a tmp id `TmpTy`
|
||||
#:with (CTY/tmp ...) (subst #'TmpTy #'Name #'(CTY ...))
|
||||
[⊢ CTY/tmp ≫ CTY/tmp- ⇐ Type] ...
|
||||
#:with TmpTy+ (local-expand #'TmpTy 'expression null)
|
||||
;; un-subst TmpTy for Name in expanded CTY
|
||||
;; TODO: replace TmpTy in origs of CTY_in ... CTY_out
|
||||
;; TODO: check CTY_out == `Name`?
|
||||
#:with ((~Π ([x : CTY_in] ...) CTY_out) ...)
|
||||
(subst #'Name #'TmpTy+ #'(CTY/tmp- ...) free-id=?)
|
||||
#:with (C/internal ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase- ...) (generate-temporaries #'(C ...))
|
||||
#:with ((recur-x ...) ...) (stx-map
|
||||
(lambda (xs ts)
|
||||
(filter
|
||||
(lambda (x) x) ; filter out #f
|
||||
(stx-map
|
||||
(lambda (x t) ; returns x or #f
|
||||
(and (free-id=? t #'Name) x))
|
||||
xs ts)))
|
||||
#'((x ...) ...) #'((CTY_in ...) ...))
|
||||
#:with elim-Name (format-id #'Name "elim-~a" #'Name)
|
||||
#:with match-Name (format-id #'Name "match-~a" #'Name)
|
||||
#:with Name/internal (generate-temporary #'Name)
|
||||
--------
|
||||
[≻ (begin-
|
||||
;; define `Name`, eg "Nat", as a valid type
|
||||
; (define-base-type Name) ; dont use bc uses '::, and runtime errs
|
||||
(struct Name/internal ())
|
||||
(define-typed-syntax Name [_:id ≫ --- [⊢ (Name/internal) ⇒ TY]])
|
||||
;; define structs for `C` constructors
|
||||
(struct C/internal (x ...) #:transparent) ...
|
||||
(define C (unsafe-assign-type C/internal : CTY)) ...
|
||||
;; elimination form
|
||||
(define-typed-syntax (elim-Name v P Ccase ...) ≫
|
||||
[⊢ v ≫ v- ⇐ Name]
|
||||
[⊢ P ≫ P- ⇐ (→ Name Type)] ; prop / motive
|
||||
;; each `Ccase` require 2 sets of args (even if set is empty):
|
||||
;; 1) args of the constructor `x` ...
|
||||
;; 2) IHs for each `x` that has type `Name`
|
||||
[⊢ Ccase ≫ Ccase- ⇐ (Π ([x : CTY_in] ...)
|
||||
(→ (app P- recur-x) ...
|
||||
(app P- (app C x ...))))] ...
|
||||
-----------
|
||||
[⊢ (match-Name v- P- Ccase- ...) ⇒ (app P- v-)])
|
||||
;; eval the elim redexes
|
||||
(define-syntax match-Name
|
||||
(syntax-parser
|
||||
#;[(_ . args)
|
||||
#:do[(printf "trying to match:\n~a\n" (stx->datum #'args))]
|
||||
#:when #f #'(void)]
|
||||
[(_ v P Ccase ...)
|
||||
#:with ty (typeof this-syntax)
|
||||
; local expand since v might be unexpanded due to reflection
|
||||
(syntax-parse (local-expand #'v 'expression null)
|
||||
; do eval if v is an actual `C` instance
|
||||
[((~literal #%plain-app) C-:id x ...)
|
||||
#:with (_ C+ . _) (local-expand #'(C 'x ...) 'expression null)
|
||||
#:when (free-identifier=? #'C- #'C+)
|
||||
(maybe-assign-type
|
||||
#`(app/eval (app Ccase x ...)
|
||||
; (match-Name x P Ccase ...) ...)
|
||||
#,@(stx-map (lambda (y)
|
||||
(maybe-assign-type
|
||||
#`(match-Name #,y P Ccase ...)
|
||||
#'ty))
|
||||
#'(x ...)))
|
||||
#'ty)]
|
||||
...
|
||||
; else generate a delayed term
|
||||
;; must be #%app-, not #%plain-app, ow match will not dispatch properly
|
||||
[_ ;(maybe-assign-type
|
||||
#'(#%app- match/delayed 'match-Name (void v P Ccase ...))
|
||||
;#'ty)
|
||||
])]))
|
||||
)]]
|
||||
;; --------------------------------------------------------------------------
|
||||
;; datatype type `TY` is a fn:
|
||||
;; - params A ... and indices i ... must be in separate fn types
|
||||
;; - but actual type formation constructor flattens to A ... i ...
|
||||
;; - and constructors also flatten to A ... i ...
|
||||
;; - all cases in elim-Name must consume i ... (but A ... is inferred)
|
||||
;; --------------------------------------------------------------------------
|
||||
[(_ Name (~datum :) TY
|
||||
[C:id (~datum :) CTY] ...) ≫
|
||||
|
||||
;; params and indices specified with separate fn types, to distinguish them,
|
||||
;; but are combined in other places,
|
||||
;; eg (Name A ... i ...) or (CTY A ... i ...)
|
||||
[⊢ TY ≫ (~Π ([A : TYA] ...) ; params
|
||||
(~Π ([i : TYi] ...) ; indices
|
||||
TY_out)) ⇐ Type]
|
||||
|
||||
; need to expand `CTY` but `Name` is still unbound so use tmp id
|
||||
; - extract arity of each `C` ...
|
||||
; - find recur args
|
||||
#:with (CTY/tmp ...) (subst #'TmpTy #'Name #'(CTY ...))
|
||||
[⊢ CTY/tmp ≫ CTY/tmp- ⇐ Type] ...
|
||||
#:with (_ TmpTy+) (local-expand #'(TmpTy) 'expression null)
|
||||
;; ;; TODO: replace TmpTy in origs of τ_in ... τ_out
|
||||
;; TODO: how to un-subst TmpTy (which is now a constructor)?
|
||||
;; - for now, dont use these τ_in/τ_out; just use for arity
|
||||
;; - instead, re-expand in generated `elim` macro below
|
||||
;;
|
||||
;; - 1st Π is tycon params, dont care for now
|
||||
;; - 2nd Π is tycon indices, dont care for now
|
||||
;; - 3rd Π is constructor args
|
||||
#:with ((~Π ([_ : _] ...)
|
||||
(~Π ([_ : _] ...)
|
||||
(~Π ([x : CTY_in/tmp] ...) CTY_out/tmp))) ...)
|
||||
#'(CTY/tmp- ...)
|
||||
;; each (recur-x ...) is subset of (x ...) that are recur args,
|
||||
;; ie, they are not fresh ids
|
||||
#:with ((recur-x ...) ...) (stx-map
|
||||
(lambda (xs ts)
|
||||
(filter
|
||||
(lambda (y) y) ; filter out #f
|
||||
(stx-map
|
||||
(lambda (x t)
|
||||
(and
|
||||
(syntax-parse t
|
||||
[((~literal #%plain-app) tmp . _)
|
||||
(free-id=? #'tmp #'TmpTy+)]
|
||||
[_ #f])
|
||||
x)) ; returns x or #f
|
||||
xs ts)))
|
||||
#'((x ...) ...)
|
||||
#'((CTY_in/tmp ...) ...))
|
||||
#:with ((recur-Cx ...) ...) (stx-map generate-temporaries #'((recur-x ...) ...))
|
||||
|
||||
;; pre-generate other patvars; makes nested macros below easier to read
|
||||
#:with (A- ...) (generate-temporaries #'(A ...))
|
||||
#:with (i- ...) (generate-temporaries #'(i ...))
|
||||
;; need to multiply A and i patvars, to match types of `C` ... constructors
|
||||
;; must be fresh vars to avoid dup patvar errors
|
||||
#:with ((CA ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
#:with ((CTYA ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
#:with ((Ci ...) ...) (stx-map (lambda _ (generate-temporaries #'(i ...))) #'(C ...))
|
||||
#:with ((CTYi/CA ...) ...) (stx-map (lambda _ (generate-temporaries #'(TYi ...))) #'(C ...))
|
||||
#:with ((CTYi ...) ...) (stx-map (lambda _ (generate-temporaries #'(TYi ...))) #'(C ...))
|
||||
#:with ((Cx ...) ...) (stx-map (lambda (xs) (generate-temporaries xs)) #'((x ...) ...))
|
||||
; Ci*recur dups Ci for each recur, to get the ellipses to work out below
|
||||
#:with (((Ci*recur ...) ...) ...) (stx-map
|
||||
(lambda (cis recurs)
|
||||
(stx-map (lambda (r) cis) recurs))
|
||||
#'((Ci ...) ...)
|
||||
#'((recur-x ...) ...))
|
||||
;; not inst'ed CTY_in
|
||||
#:with ((CTY_in/CA ...) ...) (stx-map generate-temporaries #'((CTY_in/tmp ...) ...))
|
||||
;; inst'ed CTY_in (with A ...)
|
||||
#:with ((CTY_in ...) ...) (stx-map generate-temporaries #'((CTY_in/tmp ...) ...))
|
||||
#:with (CTY_out/CA ...) (generate-temporaries #'(C ...))
|
||||
#:with (CTY_out ...) (generate-temporaries #'(C ...))
|
||||
; CTY_out_A matches the A and CTY_out_i matches the i in CTY_out,
|
||||
; - ie CTY_out = (Name CTY_out_A ... CTY_out_i ...)
|
||||
; - also, CTY_out_A refs (ie bound-id=) CA and CTY_out_i refs Ci
|
||||
#:with ((CTY_out_A ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
#:with ((CTY_out_i ...) ...) (stx-map (lambda _ (generate-temporaries #'(i ...))) #'(C ...))
|
||||
;; differently named `i`, to match type of P
|
||||
#:with (j ...) (generate-temporaries #'(i ...))
|
||||
; dup (A ...) C times, again for ellipses matching
|
||||
#:with ((A*C ...) ...) (stx-map (lambda _ #'(A ...)) #'(C ...))
|
||||
#:with (C/internal ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase- ...) (generate-temporaries #'(C ...))
|
||||
#:with Name- (mk-- #'Name)
|
||||
#:with Name-patexpand (mk-~ #'Name)
|
||||
#:with elim-Name (format-id #'Name "elim-~a" #'Name)
|
||||
#:with match-Name (format-id #'Name "match-~a" #'Name)
|
||||
#:with (ccasety ...) (generate-temporaries #'(Ccase ...))
|
||||
;; these are all the generated definitions that implement the define-datatype
|
||||
#:with OUTPUT-DEFS
|
||||
#'(begin-
|
||||
;; define the type
|
||||
(define-internal-type-constructor Name)
|
||||
;; TODO? This works when TYi depends on (e.g., is) A
|
||||
;; but is this always the case?
|
||||
(define-typed-syntax (Name A ... i ...) ≫
|
||||
[⊢ A ≫ A- ⇐ TYA] ...
|
||||
[⊢ i ≫ i- ⇐ TYi] ...
|
||||
----------
|
||||
[⊢ (Name- A- ... i- ...) ⇒ TY_out])
|
||||
|
||||
;; define structs for constructors
|
||||
(struct C/internal (x ...) #:transparent) ...
|
||||
;; TODO: this define should be a macro instead?
|
||||
(define C (unsafe-assign-type
|
||||
(lambda (A ...) (lambda (i ...) C/internal))
|
||||
: CTY)) ...
|
||||
|
||||
;; define eliminator-form
|
||||
(define-typed-syntax (elim-Name v P Ccase ...) ≫
|
||||
;; re-extract CTY_in and CTY_out, since we didnt un-subst above
|
||||
;; TODO: must re-compute recur-x, ie recur-Cx
|
||||
#:with ((~Π ([CA : CTYA] ...) ; ignore params, instead infer `A` ... from `v`
|
||||
(~Π ([Ci : CTYi/CA] ...)
|
||||
(~Π ([Cx : CTY_in/CA] ...)
|
||||
CTY_out/CA)))
|
||||
...)
|
||||
(stx-map (current-type-eval) #'(CTY ...))
|
||||
|
||||
;; compute recur-Cx by finding analogous x/recur-x pairs
|
||||
;; each (recur-Cx ...) is subset of (Cx ...) that are recur args,
|
||||
;; ie, they are not fresh ids
|
||||
#:with ((recur-Cx ...) ...)
|
||||
(stx-map
|
||||
(lambda (xs rxs cxs)
|
||||
(filter
|
||||
(lambda (z) z) ; filter out #f
|
||||
(stx-map
|
||||
(lambda (y cy)
|
||||
(if (stx-member y rxs) cy #f))
|
||||
xs cxs)))
|
||||
#'((x ...) ...)
|
||||
#'((recur-x ...) ...)
|
||||
#'((Cx ...) ...))
|
||||
#;(stx-map
|
||||
(lambda (xs ts)
|
||||
(filter
|
||||
(lambda (y) y) ; filter out #f
|
||||
(stx-map
|
||||
(lambda (x t)
|
||||
(and
|
||||
(syntax-parse t
|
||||
[(Name-patexpand . _) #t]
|
||||
[_ #f])
|
||||
x)) ; returns x or #f
|
||||
xs ts)))
|
||||
#'((Cx ...) ...)
|
||||
#'((CTY_in/CA ...) ...))
|
||||
|
||||
;; target, infers A ...
|
||||
[⊢ v ≫ v- ⇒ (Name-patexpand A ... i ...)]
|
||||
|
||||
;; inst CTY_in/CA and CTY_out/CA with inferred A ...
|
||||
#:with (((CTYi ...)
|
||||
(CTY_in ... CTY_out))
|
||||
...)
|
||||
(stx-map (lambda (ts tyis cas) (substs #'(A ...) cas #`(#,tyis #,ts)))
|
||||
#'((CTY_in/CA ... CTY_out/CA) ...)
|
||||
#'((CTYi/CA ...) ...)
|
||||
#'((CA ...) ...))
|
||||
;; get the params and indices in CTY_out
|
||||
;; - dont actually need CTY_out_A
|
||||
#:with ((Name-patexpand CTY_out_A ... CTY_out_i ...) ...) #'(CTY_out ...)
|
||||
|
||||
;; prop / motive
|
||||
[⊢ P ≫ P- ⇐ (Π ([j : TYi] ...) (→ (Name A ... j ...) Type))]
|
||||
|
||||
;; each Ccase consumes 3 nested sets of (possibly empty) args:
|
||||
;; 1) Ci - indices of the tycon
|
||||
;; 2) Cx - args of each constructor `C`
|
||||
;; 3) IHs - for each recur-Cx ... (which are a subset of Cx ...)
|
||||
;;
|
||||
;; somewhat of a hack:
|
||||
;; by reusing Ci and CTY_out_i both to match CTY/CTY_out above, and here,
|
||||
;; we automatically unify Ci with the indices in CTY_out
|
||||
[⊢ Ccase ≫ _ ⇒ ccasety] ...
|
||||
[⊢ Ccase ≫ Ccase- ⇐ (Π ([Ci : CTYi] ...) ; indices
|
||||
(Π ([Cx : CTY_in] ...) ; constructor args
|
||||
(→ (app (app P- Ci*recur ...) recur-Cx) ... ; IHs
|
||||
(app (app P- CTY_out_i ...)
|
||||
(app (app (app C A*C ...) Ci ...) Cx ...)))))] ...
|
||||
-----------
|
||||
[⊢ (match-Name v- P- Ccase- ...) ⇒ (app (app P- i ...) v-)])
|
||||
|
||||
;; implements reduction of elimator redexes
|
||||
(define-syntax match-Name
|
||||
(syntax-parser
|
||||
#;[(_ . args)
|
||||
#:do[(displayln "trying to match:")
|
||||
(pretty-print (stx->datum #'args))]
|
||||
#:when #f #'(void)]
|
||||
[(_ v P Ccase ...)
|
||||
#:with ty (typeof this-syntax)
|
||||
;; must local expand because `v` may be unexpanded due to reflection
|
||||
(syntax-parse (local-expand #'v 'expression null)
|
||||
[((~literal #%plain-app)
|
||||
((~literal #%plain-app)
|
||||
((~literal #%plain-app) C-:id CA ...)
|
||||
Ci ...)
|
||||
x ...)
|
||||
#:with (_ C+ . _) (local-expand #'(C 'CA ...) 'expression null)
|
||||
#:when (free-identifier=? #'C+ #'C-)
|
||||
;; can use app instead of app/eval to properly propagate types
|
||||
;; but doesnt quite for in all cases?
|
||||
(maybe-assign-type
|
||||
#`(app/eval ;#,(assign-type
|
||||
(app/eval (app Ccase Ci ...) x ...)
|
||||
;; TODO: is this right?
|
||||
; #'(app P Ci ...))
|
||||
; (match-Name recur-x P Ccase ...) ...)
|
||||
#,@(stx-map (lambda (r)
|
||||
(maybe-assign-type
|
||||
#`(match-Name #,r P Ccase ...)
|
||||
#'ty))
|
||||
#'(recur-x ...)))
|
||||
#'ty)] ...
|
||||
[_ ;(maybe-assign-type
|
||||
;; must be #%app-, not #%plain-app, ow match will not dispatch properly
|
||||
#'(#%app- match/delayed 'match-Name (void v P Ccase ...))
|
||||
;#'ty)
|
||||
])])))
|
||||
;; DEBUG: of generated defs
|
||||
; #:do[(pretty-print (stx->datum #'OUTPUT-DEFS))]
|
||||
--------
|
||||
[≻ OUTPUT-DEFS]])
|
||||
|
|
@ -393,7 +393,7 @@
|
|||
(struct match/delayed (name args) #:transparent)
|
||||
|
||||
(define-typed-syntax define-datatype
|
||||
;; datatype type `TY` is an id ---------------------------------------------------
|
||||
;; datatype type `TY` is an id ----------------------------------------------
|
||||
;; - ie, no params or indices
|
||||
[(_ Name (~datum :) TY:id
|
||||
[C:id (~datum :) CTY] ...) ≫
|
||||
|
|
|
|||
84
turnstile/examples/tests/dep-ind-eq-tests.rkt
Normal file
84
turnstile/examples/tests/dep-ind-eq-tests.rkt
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
#lang s-exp "../dep-ind-fixed.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
; Π → λ ∀ ≻ ⊢ ≫ ⇒
|
||||
|
||||
;; testing user-defined equality
|
||||
|
||||
(define-datatype my= : (Π ([A : (Type 0)]) (Π ([a : A] [b : A]) (Type 0)))
|
||||
(my-refl : (Π ([A : (Type 0)])
|
||||
(Π ([x : A][y : A])
|
||||
(Π ([a : A]) (my= A a a))))))
|
||||
|
||||
(define-datatype Nat : *
|
||||
[Z : (→ Nat)]
|
||||
[S : (→ Nat Nat)])
|
||||
|
||||
(define-type-alias plus
|
||||
(λ ([n : Nat][m : Nat])
|
||||
(elim-Nat n
|
||||
(λ ([k : Nat]) Nat)
|
||||
(λ () (λ () m))
|
||||
(λ ([k : Nat]) (λ ([IH : Nat]) (S IH))))))
|
||||
|
||||
;; index args (the Z's) to my-refl are unused
|
||||
;; TODO: drop them?
|
||||
(check-type (((my-refl Nat) (Z) (Z)) (Z)) : (my= Nat (Z) (Z))) ; 0=0
|
||||
(check-not-type (((my-refl Nat) (Z) (Z)) (S (Z))) : (my= Nat (Z) (Z))) ; 1 \neq 0
|
||||
(check-type (((my-refl Nat) (Z) (Z)) (S (Z)))
|
||||
: (my= Nat (S (Z)) (S (Z)))) ; 1=1
|
||||
(check-type (((my-refl Nat) (Z) (Z)) (S (Z)))
|
||||
: (my= Nat (S (Z)) (plus (S (Z)) (Z)))) ; 1=1+0
|
||||
(check-type (((my-refl Nat) (Z) (Z)) (S (Z)))
|
||||
: (my= Nat (plus (S (Z)) (Z)) (plus (S (Z)) (Z)))) ; 1+0=1+0
|
||||
(check-type (((my-refl Nat) (Z) (Z)) (S (Z)))
|
||||
: (my= Nat (plus (Z) (S (Z))) (plus (S (Z)) (Z)))) ; 1+0=0+1
|
||||
(check-type
|
||||
(((my-refl Nat) (Z) (Z)) (S (S (Z))))
|
||||
: (my= Nat (plus (S (Z)) (S (Z))) (plus (S (Z)) (plus (S (Z)) (Z))))) ; 1+1=1+1+0
|
||||
|
||||
;; = symmetric
|
||||
(check-type
|
||||
(λ ([B : (Type 0)])
|
||||
(λ ([x : B] [y : B])
|
||||
(λ ([e : (my= B x y)])
|
||||
(elim-my=
|
||||
e
|
||||
(λ ([a : B] [b : B])
|
||||
(λ ([e : (my= B a b)])
|
||||
(my= B b a)))
|
||||
(λ ([a : B] [b : B])
|
||||
(λ ([c : B])
|
||||
(λ ()
|
||||
(((my-refl B) c c) c))))))))
|
||||
: (Π ([A : (Type 0)])
|
||||
(Π ([x : A] [y : A])
|
||||
(→ (my= A x y) (my= A y x)))))
|
||||
|
||||
;; = transitive
|
||||
; TODO
|
||||
#;(check-type
|
||||
(λ ([A : (Type 0)])
|
||||
(λ ([x : A] [y : A] [z : A])
|
||||
(λ ([e1 : (my= A x y)] [e2 : (my= A y z)])
|
||||
(elim-my=
|
||||
e1
|
||||
(λ ([a : A] [b : A])
|
||||
(λ ([e : (my= A a b)])
|
||||
(my= A a z)))
|
||||
(λ ([a : A] [b : A])
|
||||
(λ ([c : A])
|
||||
(λ ()
|
||||
(elim-my=
|
||||
e2
|
||||
(λ ([a : A] [b : A])
|
||||
(λ ([e : (my= A a b)])
|
||||
(my= A c c)))
|
||||
(λ ([a : A] [b : A])
|
||||
(λ ([c : A])
|
||||
(λ ()
|
||||
(((my-refl A) c c) c))))))))))))
|
||||
: (Π ([A : (Type 0)])
|
||||
(Π ([x : A] [y : A] [z : A])
|
||||
(→ (my= A x y) (my= A y z) (my= A x z)))))
|
||||
|
||||
271
turnstile/examples/tests/dep-ind-fixed-list-tests.rkt
Normal file
271
turnstile/examples/tests/dep-ind-fixed-list-tests.rkt
Normal file
|
|
@ -0,0 +1,271 @@
|
|||
#lang s-exp "../dep-ind-fixed.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
; Π → λ ∀ ≻ ⊢ ≫ ⇒
|
||||
|
||||
;; same as dep-ind-list-tests except uses dep-ind-fixed
|
||||
;; - constructor params and indices must be applied separately
|
||||
|
||||
(define-datatype Nat : *
|
||||
[Z : (→ Nat)]
|
||||
[S : (→ Nat Nat)])
|
||||
|
||||
;; some basic tests
|
||||
(check-type Nat : *)
|
||||
;; this test wont work if define-datatype uses define-base-type
|
||||
(check-type (λ ([x : Nat]) Nat) : (→ Nat *))
|
||||
|
||||
;; constructors require 3 sets of args:
|
||||
;; 1) params
|
||||
;; 2) indices
|
||||
;; 3) constructor args, split into
|
||||
;; - non-recursive
|
||||
;; - recursive
|
||||
(define-datatype List : (→ * (→ *))
|
||||
[null : (∀ (A) (→ (→ (List A))))]
|
||||
[cons : (∀ (A) (→ (→ A (List A) (List A))))])
|
||||
|
||||
(check-type null : (∀ (A) (→ (→ (List A)))))
|
||||
(check-type cons : (∀ (A) (→ (→ A (List A) (List A)))))
|
||||
(check-type (null Nat) : (→ (→ (List Nat))))
|
||||
(check-type (cons Nat) : (→ (→ Nat (List Nat) (List Nat))))
|
||||
(check-type ((null Nat)) : (→ (List Nat)))
|
||||
(check-type (((null Nat))) : (List Nat))
|
||||
(check-type (((cons Nat)) (Z) (((null Nat)))) : (List Nat))
|
||||
|
||||
;; length 0
|
||||
(check-type
|
||||
(elim-List (((null Nat)))
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat
|
||||
-> (Z))
|
||||
|
||||
;; length 1
|
||||
(check-type
|
||||
(elim-List (((cons Nat)) (Z) (((null Nat))))
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat
|
||||
-> (S (Z)))
|
||||
|
||||
;; length 2
|
||||
(check-type
|
||||
(elim-List (((cons Nat)) (S (Z)) (((cons Nat)) (Z) (((null Nat)))))
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat
|
||||
-> (S (S (Z))))
|
||||
|
||||
(define-type-alias len/Nat
|
||||
(λ ([lst : (List Nat)])
|
||||
(elim-List lst
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))))
|
||||
|
||||
(check-type (len/Nat (((null Nat)))) : Nat -> (Z))
|
||||
(check-type (len/Nat (((cons Nat)) (Z) (((null Nat))))) : Nat -> (S (Z)))
|
||||
|
||||
(define-type-alias len
|
||||
(λ ([A : *])
|
||||
(λ ([lst : (List A)])
|
||||
(elim-List lst
|
||||
(λ () (λ ([l : (List A)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : A][xs : (List A)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH))))))))
|
||||
(check-type (len Nat) : (→ (List Nat) Nat))
|
||||
(check-type ((len Nat) (((null Nat)))) : Nat -> (Z))
|
||||
(check-type ((len Nat) (((cons Nat)) (Z) (((null Nat))))) : Nat -> (S (Z)))
|
||||
|
||||
;; test that elim matches on constructor name, and not arity
|
||||
(define-datatype Test : *
|
||||
[A : (→ Test)]
|
||||
[B : (→ Test)])
|
||||
|
||||
(check-type
|
||||
(elim-Test (A)
|
||||
(λ ([x : Test]) Nat)
|
||||
(λ () (λ () (Z)))
|
||||
(λ () (λ () (S (Z)))))
|
||||
: Nat -> (Z))
|
||||
|
||||
;; should match second branch, but just arity-checking would match 1st
|
||||
(check-type
|
||||
(elim-Test (B)
|
||||
(λ ([x : Test]) Nat)
|
||||
(λ () (λ () (Z)))
|
||||
(λ () (λ () (S (Z)))))
|
||||
: Nat -> (S (Z)))
|
||||
|
||||
;; Vect: indexed "lists" parameterized over length --------------------
|
||||
(define-datatype Vect : (→ * (→ Nat *))
|
||||
[nil : (Π ([A : *]) (Π ([k : Nat]) (→ (Vect A (Z)))))]
|
||||
[cns : (Π ([A : *]) (Π ([k : Nat]) (→ A (Vect A k) (Vect A (S k)))))])
|
||||
|
||||
(check-type nil : (Π ([A : *]) (Π ([k : Nat]) (→ (Vect A (Z))))))
|
||||
(check-type cns : (Π ([A : *]) (Π ([k : Nat]) (→ A (Vect A k) (Vect A (S k))))))
|
||||
|
||||
(check-type ((nil Nat) (Z)) : (→ (Vect Nat (Z))))
|
||||
(check-type ((cns Nat) (Z)) : (→ Nat (Vect Nat (Z)) (Vect Nat (S (Z)))))
|
||||
|
||||
(check-type (((nil Nat) (Z))) : (Vect Nat (Z)))
|
||||
(check-type (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))) : (Vect Nat (S (Z))))
|
||||
(check-type (((cns Nat) (S (Z))) (Z)
|
||||
(((cns Nat) (Z)) (Z)
|
||||
(((nil Nat) (Z)))))
|
||||
: (Vect Nat (S (S (Z)))))
|
||||
|
||||
(define-type-alias mtNatVec (((nil Nat) (Z))))
|
||||
(check-type mtNatVec : (Vect Nat (Z)))
|
||||
|
||||
;; nil must be applied again (bc it's a constructor of 0 args)
|
||||
(check-not-type ((nil Nat) (S (Z))) : (Vect Nat (S (Z))))
|
||||
|
||||
;; length
|
||||
(check-type
|
||||
(elim-Vect (((nil Nat) (Z)))
|
||||
(λ ([k : Nat]) (λ ([v : (Vect Nat k)]) Nat))
|
||||
(λ ([k : Nat]) (λ () (λ () (Z))))
|
||||
(λ ([k : Nat])
|
||||
(λ ([x : Nat][xs : (Vect Nat k)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat -> (Z))
|
||||
|
||||
(check-type
|
||||
(elim-Vect (((cns Nat) (Z)) (Z) (((nil Nat) (Z))))
|
||||
(λ ([k : Nat]) (λ ([v : (Vect Nat k)]) Nat))
|
||||
(λ ([k : Nat]) (λ () (λ () (Z))))
|
||||
(λ ([k : Nat])
|
||||
(λ ([x : Nat][xs : (Vect Nat k)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat -> (S (Z)))
|
||||
|
||||
(check-type
|
||||
(elim-Vect (((cns Nat) (S (Z))) (Z) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))
|
||||
(λ ([k : Nat]) (λ ([v : (Vect Nat k)]) Nat))
|
||||
(λ ([k : Nat]) (λ () (λ () (Z))))
|
||||
(λ ([k : Nat])
|
||||
(λ ([x : Nat][xs : (Vect Nat k)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat -> (S (S (Z))))
|
||||
|
||||
(define-type-alias plus
|
||||
(λ ([n : Nat][m : Nat])
|
||||
(elim-Nat n
|
||||
(λ ([k : Nat]) Nat)
|
||||
(λ () (λ () m))
|
||||
(λ ([k : Nat]) (λ ([IH : Nat]) (S IH))))))
|
||||
|
||||
(check-type plus : (→ Nat Nat Nat))
|
||||
|
||||
(check-type (plus (Z) (S (S (Z)))) : Nat -> (S (S (Z))))
|
||||
(check-type (plus (S (S (Z))) (Z)) : Nat -> (S (S (Z))))
|
||||
(check-type (plus (S (S (Z))) (S (S (S (Z)))))
|
||||
: Nat -> (S (S (S (S (S (Z)))))))
|
||||
|
||||
;; vappend
|
||||
(check-type
|
||||
(elim-Vect
|
||||
(((nil Nat) (Z)))
|
||||
(λ ([k : Nat])
|
||||
(λ ([v : (Vect Nat k)])
|
||||
(Vect Nat k)))
|
||||
(λ ([k : Nat]) (λ () (λ () (((nil Nat) (Z))))))
|
||||
(λ ([k : Nat])
|
||||
(λ ([x : Nat][v : (Vect Nat k)])
|
||||
(λ ([IH : (Vect Nat k)])
|
||||
(((cns Nat) k) x IH)))))
|
||||
: (Vect Nat (Z))
|
||||
-> (((nil Nat) (Z))))
|
||||
|
||||
(define-type-alias vappend
|
||||
(λ ([A : *])
|
||||
(λ ([n : Nat][m : Nat])
|
||||
(λ ([xs : (Vect A n)][ys : (Vect A m)])
|
||||
(elim-Vect
|
||||
xs
|
||||
(λ ([k : Nat])
|
||||
(λ ([v : (Vect A k)])
|
||||
(Vect A (plus k m))))
|
||||
(λ ([k : Nat]) (λ () (λ () ys)))
|
||||
(λ ([k : Nat])
|
||||
(λ ([x : A][v : (Vect A k)])
|
||||
(λ ([IH : (Vect A (plus k m))])
|
||||
(((cns A) (plus k m)) x IH)))))))))
|
||||
|
||||
(check-type
|
||||
vappend
|
||||
: (∀ (B)
|
||||
(Π ([n : Nat][m : Nat])
|
||||
(→ (Vect B n) (Vect B m) (Vect B (plus n m))))))
|
||||
|
||||
(check-type
|
||||
(vappend Nat)
|
||||
: (Π ([n : Nat][m : Nat])
|
||||
(→ (Vect Nat n) (Vect Nat m) (Vect Nat (plus n m)))))
|
||||
|
||||
(check-type
|
||||
((vappend Nat) (Z) (Z))
|
||||
: (→ (Vect Nat (Z)) (Vect Nat (Z)) (Vect Nat (Z))))
|
||||
|
||||
;; append nil + nil
|
||||
(check-type
|
||||
(((vappend Nat) (Z) (Z)) (((nil Nat) (Z))) (((nil Nat) (Z))))
|
||||
: (Vect Nat (Z))
|
||||
-> (((nil Nat) (Z))))
|
||||
|
||||
;; append 1 + 0
|
||||
(check-type
|
||||
(((vappend Nat) (S (Z)) (Z)) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))) (((nil Nat) (Z))))
|
||||
: (Vect Nat (S (Z)))
|
||||
-> (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))
|
||||
|
||||
;; m and n flipped
|
||||
(typecheck-fail
|
||||
(((vappend Nat) (S (Z)) (Z)) (((nil Nat) (Z))) (((cns Nat) (Z)) (Z) (((nil Nat) (Z))))))
|
||||
(typecheck-fail
|
||||
(((vappend Nat) (Z) (S (Z))) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))) (((nil Nat) (Z)))))
|
||||
|
||||
;; append 1 + 1
|
||||
(check-type
|
||||
(((vappend Nat) (S (Z)) (S (Z))) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))
|
||||
: (Vect Nat (S (S (Z))))
|
||||
-> (((cns Nat) (S (Z))) (Z) (((cns Nat) (Z)) (Z) (((nil Nat) (Z))))))
|
||||
|
||||
;; append 1 + 2
|
||||
(check-type
|
||||
(((vappend Nat) (S (Z)) (S (S (Z))))
|
||||
(((cns Nat) (Z)) (Z) (((nil Nat) (Z))))
|
||||
(((cns Nat) (S (Z))) (Z) (((cns Nat) (Z)) (Z) (((nil Nat) (Z))))))
|
||||
: (Vect Nat (S (S (S (Z)))))
|
||||
-> (((cns Nat) (S (S (Z)))) (Z) (((cns Nat) (S (Z))) (Z) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))))
|
||||
|
||||
;; append 2 + 1
|
||||
(check-type
|
||||
(((vappend Nat) (S (S (Z))) (S (Z)))
|
||||
(((cns Nat) (S (Z))) (Z) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))
|
||||
(((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))
|
||||
: (Vect Nat (S (S (S (Z)))))
|
||||
-> (((cns Nat) (S (S (Z)))) (Z) (((cns Nat) (S (Z))) (Z) (((cns Nat) (Z)) (Z) (((nil Nat) (Z)))))))
|
||||
153
turnstile/examples/tests/dep-ind-fixed-tests.rkt
Normal file
153
turnstile/examples/tests/dep-ind-fixed-tests.rkt
Normal file
|
|
@ -0,0 +1,153 @@
|
|||
#lang s-exp "../dep-ind-fixed.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
; Π → λ ∀ ≻ ⊢ ≫ ⇒
|
||||
|
||||
; should be identical to dep-ind-tests.rkt
|
||||
; since dep-ind-fixed does not change
|
||||
; first clause of define-datatype
|
||||
|
||||
;; examples from Prabhakar's Proust paper
|
||||
|
||||
;; this file is like dep-peano-tests.rkt except it uses
|
||||
;; define-datatype from #lang dep-ind.rkt to define Nat,
|
||||
;; instead of using the builtin Nat from #lang dep.rkt
|
||||
|
||||
;; the examples in this file are mostly identical to dep-peano-tests.rkt,
|
||||
;; except Z is replaced with (Z)
|
||||
|
||||
;; check (Type n) : (Type n+1)
|
||||
(check-type Type : (Type 1))
|
||||
(check-type (Type 0) : (Type 1))
|
||||
(check-not-type (Type 0) : (Type 0))
|
||||
(check-type (Type 1) : (Type 2))
|
||||
(check-type (Type 3) : (Type 4))
|
||||
|
||||
(typecheck-fail ((λ ([x : Type]) x) Type)
|
||||
#:with-msg "expected Type, given \\(Type 1\\)")
|
||||
(check-type ((λ ([x : (Type 1)]) x) Type) : (Type 1))
|
||||
(check-type ((λ ([x : (Type 2)]) x) (Type 1)) : (Type 2))
|
||||
|
||||
;; Peano nums -----------------------------------------------------------------
|
||||
|
||||
(define-datatype Nat : *
|
||||
[Z : (→ Nat)]
|
||||
[S : (→ Nat Nat)])
|
||||
|
||||
; TODO: special case 0-arity constructor using id macro
|
||||
(check-type Z : (→ Nat))
|
||||
(check-type S : (→ Nat Nat))
|
||||
;(check-type Z : Nat -> Z)
|
||||
(check-type (Z) : Nat -> (Z))
|
||||
(check-type (S (Z)) : Nat -> (S (Z)))
|
||||
(check-type (S (S (Z))) : Nat -> (S (S (Z))))
|
||||
|
||||
(define-type-alias nat-rec
|
||||
(λ ([C : *])
|
||||
(λ ([zc : (→ C)][sc : (→ C C)])
|
||||
(λ ([n : Nat])
|
||||
(elim-Nat n
|
||||
(λ ([x : Nat]) C)
|
||||
(λ () zc)
|
||||
(λ ([x : Nat]) sc))))))
|
||||
(check-type nat-rec : (∀ (C) (→ (→ C) (→ C C) (→ Nat C))))
|
||||
|
||||
;; nat-rec with no annotations
|
||||
(check-type
|
||||
(λ (C)
|
||||
(λ (zc sc)
|
||||
(λ (n)
|
||||
(elim-Nat n
|
||||
(λ (x) C)
|
||||
(λ () zc)
|
||||
(λ (x) sc)))))
|
||||
: (∀ (C) (→ (→ C) (→ C C) (→ Nat C))))
|
||||
|
||||
(check-type (nat-rec Nat) : (→ (→ Nat) (→ Nat Nat) (→ Nat Nat)))
|
||||
(check-type ((nat-rec Nat) Z (λ ([n : Nat]) (S n))) : (→ Nat Nat))
|
||||
|
||||
;; basic identity example, to test eval
|
||||
(define-type-alias id ((nat-rec Nat) Z (λ ([n : Nat]) (S n))))
|
||||
|
||||
(check-type (id (Z)) : Nat -> (Z))
|
||||
;; this example will err if eval tries to tycheck again
|
||||
(check-type (id (S (Z))) : Nat)
|
||||
(check-type (id (S (Z))) : Nat -> (S (Z)))
|
||||
|
||||
(define-type-alias plus
|
||||
(λ ([n : Nat])
|
||||
(((nat-rec (→ Nat Nat))
|
||||
(λ () (λ ([m : Nat]) m))
|
||||
(λ ([pm : (→ Nat Nat)])
|
||||
(λ ([x : Nat])
|
||||
(S (pm x)))))
|
||||
n)))
|
||||
|
||||
(check-type plus : (→ Nat (→ Nat Nat)))
|
||||
|
||||
;; infer, and dont curry
|
||||
(check-type
|
||||
(λ (n1 n2)
|
||||
((((nat-rec (→ Nat Nat))
|
||||
(λ () (λ (m) m))
|
||||
(λ (pm) (λ (x) (S (pm x)))))
|
||||
n1)
|
||||
n2))
|
||||
: (→ Nat Nat Nat))
|
||||
|
||||
;(check-type ((plus Z) Z) : Nat -> 0)
|
||||
;(check-type ((plus (S Z)) (S Z)) : Nat -> 2)
|
||||
;(check-type ((plus (S Z)) Z) : Nat -> 1)
|
||||
;(check-type ((plus (S Z)) Z) : Nat -> 1)
|
||||
(check-type (plus (Z)) : (→ Nat Nat))
|
||||
(check-type ((plus (Z)) (Z)) : Nat -> (Z))
|
||||
(check-type ((plus (Z)) (S (Z))) : Nat -> (S (Z)))
|
||||
(check-type ((plus (S (Z))) (Z)) : Nat -> (S (Z)))
|
||||
(check-type ((plus (S (Z))) (S (Z))) : Nat -> (S (S (Z))))
|
||||
(check-type ((plus (S (S (Z)))) (S (Z))) : Nat -> (S (S (S (Z)))))
|
||||
(check-type ((plus (S (Z))) (S (S (Z)))) : Nat -> (S (S (S (Z)))))
|
||||
|
||||
;; plus zero (left)
|
||||
(check-type (λ ([n : Nat]) (eq-refl n))
|
||||
: (Π ([n : Nat]) (= ((plus (Z)) n) n)))
|
||||
|
||||
;; plus zero (right)
|
||||
(check-type
|
||||
(λ ([n : Nat])
|
||||
(elim-Nat n
|
||||
(λ ([m : Nat]) (= ((plus m) (Z)) m))
|
||||
(λ () (λ () (eq-refl (Z))))
|
||||
(λ ([k : Nat])
|
||||
(λ ([p : (= ((plus k) (Z)) k)])
|
||||
(eq-elim ((plus k) (Z))
|
||||
(λ ([W : Nat]) (= (S ((plus k) (Z))) (S W)))
|
||||
(eq-refl (S ((plus k) (Z))))
|
||||
k
|
||||
p)))))
|
||||
: (Π ([n : Nat]) (= ((plus n) (Z)) n)))
|
||||
|
||||
;; plus zero identity, no annotations
|
||||
;; left:
|
||||
(check-type (λ (n) (eq-refl n))
|
||||
: (Π ([n : Nat]) (= ((plus (Z)) n) n)))
|
||||
;; right:
|
||||
(check-type
|
||||
(λ (n)
|
||||
(elim-Nat n
|
||||
(λ (m) (= ((plus m) (Z)) m))
|
||||
(λ () (λ () (eq-refl (Z))))
|
||||
(λ (k) (λ (p)
|
||||
(eq-elim ((plus k) (Z))
|
||||
(λ (W) (= (S ((plus k) (Z))) (S W)))
|
||||
(eq-refl (S ((plus k) (Z))))
|
||||
k
|
||||
p)))))
|
||||
: (Π ([n : Nat]) (= ((plus n) (Z)) n))
|
||||
)
|
||||
;; nat-ind as a function ; TODO: need matching form or matching lambda
|
||||
#;(define-typed-alias nat-ind2
|
||||
(λ ([P : (→ Nat *)]
|
||||
[Zcase : (P Z)]
|
||||
[Scase : (Π ([k : Nat]) (→ (P k) (P (S k))))]
|
||||
[n : Nat])
|
||||
(match/nat n ZCase (SCase n (nat-ind2 P ZCase SCase n-1)))))
|
||||
Loading…
Reference in New Issue
Block a user