diff --git a/turnstile/examples/dep-ind-fixed.rkt b/turnstile/examples/dep-ind-fixed.rkt
new file mode 100644
index 0000000..e5cd68c
--- /dev/null
+++ b/turnstile/examples/dep-ind-fixed.rkt
@@ -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]])
diff --git a/turnstile/examples/dep-ind.rkt b/turnstile/examples/dep-ind.rkt
index 124cf9b..b08d8f5 100644
--- a/turnstile/examples/dep-ind.rkt
+++ b/turnstile/examples/dep-ind.rkt
@@ -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] ...) ≫
diff --git a/turnstile/examples/tests/dep-ind-eq-tests.rkt b/turnstile/examples/tests/dep-ind-eq-tests.rkt
new file mode 100644
index 0000000..ef8e680
--- /dev/null
+++ b/turnstile/examples/tests/dep-ind-eq-tests.rkt
@@ -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)))))
+
diff --git a/turnstile/examples/tests/dep-ind-fixed-list-tests.rkt b/turnstile/examples/tests/dep-ind-fixed-list-tests.rkt
new file mode 100644
index 0000000..698455f
--- /dev/null
+++ b/turnstile/examples/tests/dep-ind-fixed-list-tests.rkt
@@ -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)))))))
diff --git a/turnstile/examples/tests/dep-ind-fixed-tests.rkt b/turnstile/examples/tests/dep-ind-fixed-tests.rkt
new file mode 100644
index 0000000..c989c5b
--- /dev/null
+++ b/turnstile/examples/tests/dep-ind-fixed-tests.rkt
@@ -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)))))