Vect and vappend working!
This commit is contained in:
Stephen Chang
parent
98327386ae
commit
47dc16e68a
|
|
@ -48,13 +48,17 @@
|
|||
(define old-relation (current-typecheck-relation))
|
||||
(current-typecheck-relation
|
||||
(lambda (t1 t2)
|
||||
(when type-eq-debug?
|
||||
(pretty-print (stx->datum t1))
|
||||
(pretty-print (stx->datum t2)))
|
||||
;; assumed #f can only come from (typeof #%type)
|
||||
;; (so this wont work when interacting with untyped code)
|
||||
(or (and (false? (syntax-e t1)) (#%type? t2)) ; assign Type : Type
|
||||
(old-relation t1 t2)))))
|
||||
(define res
|
||||
(or (and (false? (syntax-e t1)) (#%type? t2)) ; assign Type : Type
|
||||
; (and (#%type? t1) (false? (syntax-e t2)))
|
||||
(old-relation t1 t2)))
|
||||
(when type-eq-debug?
|
||||
(pretty-print (stx->datum t1))
|
||||
(pretty-print (stx->datum t2))
|
||||
(printf "res: ~a\n" res))
|
||||
res)))
|
||||
(define-for-syntax Type ((current-type-eval) #'#%type))
|
||||
|
||||
(define-internal-type-constructor →) ; equiv to Π with no uses on rhs
|
||||
|
|
@ -174,8 +178,13 @@
|
|||
(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 (_ 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?
|
||||
#'(matcher . args)]
|
||||
;; TODO: apply to only lambda args or all args?
|
||||
|
|
@ -183,9 +192,7 @@
|
|||
#:do[(when debug?
|
||||
(printf "apping: ~a\n" (stx->datum #'f))
|
||||
(printf "args\n")
|
||||
(pretty-print (stx->datum #'(e_arg ...)))
|
||||
(printf "expected type\n")
|
||||
(pretty-print (stx->datum (typeof this-syntax))))]
|
||||
(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
|
||||
|
|
@ -195,16 +202,37 @@
|
|||
;; 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 #'ty) #'e-inst)
|
||||
#: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 (substs #'(e_arg ...) #'(X ...) (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)))
|
||||
|
|
@ -457,112 +485,118 @@
|
|||
(struct TmpTy2 ())
|
||||
(define-syntax mTmpTy (syntax-parser [(_ . args) #'(#%app TmpTy . args)]))
|
||||
(define-typed-syntax define-datatype
|
||||
;; kind is an id --------------------
|
||||
[(_ Name (~datum :) kind:id [C:id (~datum :) TY #;(~and TY (ar tyin ... tyout))] ...) ≫
|
||||
; need to expand `TY` but `Name` is still unbound so use tmp id
|
||||
#:with (TY* ...) (subst #'TmpTy #'Name #'(TY ...))
|
||||
[⊢ TY* ≫ TY- ⇐ #%type] ...
|
||||
;; kind is an id ------------------------------------------------------------
|
||||
;; - ie, no params or indices
|
||||
[(_ Name (~datum :) kind: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)
|
||||
;; TODO: ignoring X ... for now
|
||||
;; un-subst TmpTy for Name in expanded CTY
|
||||
;; TODO: replace TmpTy in origs of τ_in ... τ_out
|
||||
#:with ((~Π ([X : τ_in] ...) τ_out) ...)
|
||||
(subst #'Name #'TmpTy+ #'(TY- ...) free-id=?)
|
||||
#:with (C* ...) (generate-temporaries #'(C ...))
|
||||
#:with ((~Π ([x : τ_in] ...) τ_out) ...)
|
||||
(subst #'Name #'TmpTy+ #'(CTY/tmp- ...) free-id=?)
|
||||
#:with (C/internal ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase ...) (generate-temporaries #'(C ...))
|
||||
#:with (C- ...) (generate-temporaries #'(C ...))
|
||||
;; Can I just use X instead of fld?
|
||||
#:with ((fld ...) ...) (stx-map generate-temporaries #'((τ_in ...) ...))
|
||||
#:with ((recur-fld ...) ...) (stx-map
|
||||
(lambda (fs ts)
|
||||
(filter
|
||||
(lambda (x) x) ; filter out #f
|
||||
(stx-map
|
||||
(lambda (f t) (and (free-id=? t #'Name) f)) ; returns f or #f
|
||||
fs ts)))
|
||||
#'((fld ...) ...)
|
||||
#'((τ_in ...) ...))
|
||||
#:with ((fld- ...) ...) (stx-map generate-temporaries #'((τ_in ...) ...))
|
||||
#: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) (and (free-id=? t #'Name) x)) ; returns x or #f
|
||||
xs ts)))
|
||||
#'((x ...) ...)
|
||||
#'((τ_in ...) ...))
|
||||
#:with elim-Name (format-id #'Name "elim-~a" #'Name)
|
||||
#:with match-Name (format-id #'Name "match-~a" #'Name)
|
||||
; #:with match-Name/delayed (format-id #'Name "match-~a/delayed" #'Name)
|
||||
#:with Name/internal (generate-temporary #'Name)
|
||||
--------
|
||||
[≻ (begin-
|
||||
(define-base-type Name)
|
||||
(struct C* (fld ...) #:transparent) ...
|
||||
(define C (unsafe-assign-type C* : TY)) ...
|
||||
#;(define-typed-syntax C
|
||||
[:id ≫ --- [⊢ C* ⇒ TY]]
|
||||
[(_ fld ...) ≫
|
||||
[⊢ fld ≫ fld- ⇐ τ_in] ...
|
||||
--------
|
||||
[⊢ (C* fld- ...) ⇒ τ_out]])
|
||||
(define-typed-syntax (elim-Name x P C* ...) ≫
|
||||
[⊢ x ≫ x- ⇐ Name]
|
||||
(struct Name/internal ())
|
||||
(define-typed-syntax Name
|
||||
[_:id ≫ --- [⊢ (Name/internal) ⇒ #%type]])
|
||||
;(define-base-type Name) ; cant use this bc it tries to attach type with '::
|
||||
(struct C/internal (x ...) #:transparent) ...
|
||||
(define C (unsafe-assign-type C/internal : CTY)) ...
|
||||
(define-typed-syntax (elim-Name v P Ccase ...) ≫
|
||||
[⊢ v ≫ v- ⇐ Name]
|
||||
[⊢ P ≫ P- ⇐ (→ Name #%type)] ; prop / motive
|
||||
; [⊢ z ≫ z- ⇐ (app P- Zero)] ; zero
|
||||
; [⊢ C ≫ C- ⇐ (Π ([k : Nat]) (→ (app P- k) (app P- (Succ k))))] ; succ
|
||||
;; TODO: the (app P- fld) ... is wrong, should only include recur args
|
||||
;; for now, each case consumes the number of args for each C,
|
||||
;; and then an IH for each arg
|
||||
;; each C consumes 3 sets of args
|
||||
;; 1) args of the tycon
|
||||
;; 2) args of the con
|
||||
;; 3) IH for each recursive arg
|
||||
;; TODO: get rid of this use of τ_in
|
||||
;; - then I wont have to un-subst above
|
||||
[⊢ C* ≫ C- ⇐ (Π ([fld : τ_in] ...) (→ (app P- recur-fld) ... (app P- (app C fld ...))))] ...
|
||||
[⊢ Ccase ≫ Ccase- ⇐ (Π ([x : τ_in] ...)
|
||||
(→ (app P- recur-x) ...
|
||||
(app P- (app C x ...))))] ...
|
||||
-----------
|
||||
[⊢ (match-Name x- P- C- ...) ⇒ (app P- x-)])
|
||||
; (struct match-Name/delayed (m))
|
||||
[⊢ (match-Name v- P- Ccase- ...) ⇒ (app P- v-)])
|
||||
(define-syntax match-Name
|
||||
(syntax-parser
|
||||
#;[(_ . args)
|
||||
#:do[(printf "trying to match:\n~a\n" (stx->datum #'args))]
|
||||
#:when #f #'(void)]
|
||||
[(_ n P Ccase ...)
|
||||
(syntax-parse #'n
|
||||
[((~literal #%plain-app) C-:id fld ...)
|
||||
;; TODO: check C- matches actual C
|
||||
;; for now, it's just an arity match
|
||||
#'(app/eval (app/eval Ccase fld ...) (match-Name fld P Ccase ...) ...)] ...
|
||||
[_ #'(#%app match/delayed 'match-Name (void n P Ccase ...))])]))
|
||||
[(_ v P Ccase ...)
|
||||
; must local expand since v might be reflected
|
||||
(syntax-parse (local-expand #'v 'expression null)
|
||||
; do eval
|
||||
[((~literal #%plain-app) C-:id x ...)
|
||||
#:with (_ C+ . _) (local-expand #'(C 'x ...) 'expression null)
|
||||
#:when (free-identifier=? #'C- #'C+)
|
||||
#'(app/eval (app/eval Ccase x ...) (match-Name x P Ccase ...) ...)]
|
||||
...
|
||||
; else generated a delayed term
|
||||
[_ #'(#%app match/delayed 'match-Name (void v P Ccase ...))])]))
|
||||
)]]
|
||||
;; --------------------------------------------------------------------------
|
||||
;; kind is a fn; all cases in elim-Name must consume tycon args -------------
|
||||
;; --------------------------------------------------------------------------
|
||||
[(_ Name (~datum :) k [C:id (~datum :) TY #;(~and TY (ar tyin ... tyout))] ...) ≫
|
||||
[⊢ k ≫ (~Π ([A : k_in] ...) k_out) ⇐ #%type]
|
||||
[(_ Name (~datum :) k [C:id (~datum :) CTY] ...) ≫
|
||||
;; params and indices are separate here, to distinguish them,
|
||||
;; but are combined in other places like CTY
|
||||
[⊢ k ≫ (~Π ([A : kA] ...) ; params
|
||||
(~Π ([i : ki] ...) ; indices
|
||||
k_out)) ⇐ #%type]
|
||||
#:with (A- ...) (generate-temporaries #'(A ...))
|
||||
#:with (i- ...) (generate-temporaries #'(i ...))
|
||||
#:with (j ...) (generate-temporaries #'(i ...))
|
||||
#:with (B ...) (generate-temporaries #'(A ...))
|
||||
;; need to multiply A patvars to use in def of C ...
|
||||
#:with ((CA ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
#:with ((CAtmp ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
; actually dup (A ...) C times
|
||||
#:with ((A* ...) ...) (stx-map (lambda _ #'(A ...)) #'(C ...))
|
||||
#:with ((Ci ...) ...) (stx-map (lambda _ (generate-temporaries #'(i ...))) #'(C ...))
|
||||
#:with ((Cj ...) ...) (stx-map (lambda _ (generate-temporaries #'(i ...))) #'(C ...))
|
||||
; CB is just reference to CA
|
||||
#:with ((CB ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
#:with ((Ck ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
; need to expand `TY` but `Name` is still unbound so use tmp id
|
||||
#:with (TY* ...) (subst #'mTmpTy #'Name #'(TY ...))
|
||||
[⊢ TY* ≫ TY- ⇐ #%type] ...
|
||||
#:with (_ TmpTy+) (local-expand #'(TmpTy) 'expression null)
|
||||
;; ;; TODO: ignoring X ... for now
|
||||
#:with ((CkA ...) ...) (stx-map (lambda _ (generate-temporaries #'(A ...))) #'(C ...))
|
||||
#:with ((Cki ...) ...) (stx-map (lambda _ (generate-temporaries #'(ki ...))) #'(C ...))
|
||||
; need to expand `CTY` but `Name` is still unbound so use tmp id
|
||||
#:with (CTY/tmp ...) (subst #'mTmpTy #'Name #'(CTY ...))
|
||||
[⊢ CTY/tmp ≫ CTY/tmp- ⇐ #%type] ...
|
||||
#:with (_ TmpTy+) (local-expand #'(mTmpTy) 'expression null)
|
||||
;; ;; TODO: replace TmpTy in origs of τ_in ... τ_out
|
||||
;; #:with ((~Π ([X : τ_in] ...) τ_out) ...)
|
||||
;; (subst #'Name #'TmpTy+ #'(TY- ...) free-id=?)
|
||||
;; 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 macro
|
||||
;; - first Π is tycon args
|
||||
;; - for now, dont use these τ_in/τ_out; just use for arity
|
||||
;; - instead, re-expand in generated macro
|
||||
|
||||
;; - 1st Π is tycon params and indices
|
||||
;; - 2nd Π is constructor args
|
||||
#:with ((~Π ([_ : _] ...) (~Π ([X : τ_in/tmp] ...) τ_out/tmp)) ...)
|
||||
#'(TY- ...)
|
||||
#:with (C* ...) (generate-temporaries #'(C ...))
|
||||
#'(CTY/tmp- ...)
|
||||
#:with (C/internal ...) (generate-temporaries #'(C ...))
|
||||
#:with (Cty ...) (generate-temporaries #'(C ...))
|
||||
#:with (C** ...) (generate-temporaries #'(C ...))
|
||||
#:with (Cty2 ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase ...) (generate-temporaries #'(C ...))
|
||||
#:with (Ccase- ...) (generate-temporaries #'(C ...))
|
||||
#:with (C- ...) (generate-temporaries #'(C ...))
|
||||
;; TODO: Can I just use X instead of fld?
|
||||
;; - but I need τ_in to find recurs
|
||||
#:with ((fld ...) ...) (stx-map generate-temporaries #'((X ...) ...))
|
||||
#:with ((τ_in ...) ...) (stx-map generate-temporaries #'((τ_in/tmp ...) ...))
|
||||
#:with ((τ_in/CA ...) ...) (stx-map generate-temporaries #'((τ_in/tmp ...) ...))
|
||||
#:with ((τ_in/X ...) ...) (stx-map generate-temporaries #'((τ_in/tmp ...) ...))
|
||||
#:with (τ_out ...) (generate-temporaries #'(τ_out/tmp ...))
|
||||
;; each (recur-fld ...) is subset of (fld ...) that are recur args
|
||||
;; - ie, they are not fresh ids
|
||||
#:with ((recur-fld ...) ...) (stx-map
|
||||
(lambda (fs ts)
|
||||
(filter
|
||||
|
|
@ -574,15 +608,21 @@
|
|||
[((~literal #%plain-app) tmp . _)
|
||||
(free-id=? #'tmp #'TmpTy+)]
|
||||
[_ #f])
|
||||
f)
|
||||
#;(and (free-id=? t #'Name) f)) ; returns f or #f
|
||||
f)) ; returns f or #f
|
||||
fs ts)))
|
||||
#'((fld ...) ...)
|
||||
#'((τ_in/tmp ...) ...))
|
||||
#:with ((CArecur ...) ...) (stx-map
|
||||
(lambda (cas recurs) cas)
|
||||
#'((CA ...) ...)
|
||||
#'((recur-fld ...) ...))
|
||||
#:with (((CAr ...) ...) ...) (stx-map
|
||||
(lambda (cas recurs)
|
||||
(stx-map (lambda (r) cas) recurs))
|
||||
#'((CA ...) ...)
|
||||
#'((recur-fld ...) ...))
|
||||
; dup Ci for each recur
|
||||
#:with (((Cir ...) ...) ...) (stx-map
|
||||
(lambda (cis recurs)
|
||||
(stx-map (lambda (r) cis) recurs))
|
||||
#'((Ci ...) ...)
|
||||
#'((recur-fld ...) ...))
|
||||
#:with ((fld- ...) ...) (stx-map generate-temporaries #'((X ...) ...))
|
||||
#:with Name- (mk-- #'Name)
|
||||
#:with Name-patexpand (mk-~ #'Name)
|
||||
|
|
@ -592,24 +632,25 @@
|
|||
--------
|
||||
[≻ (begin-
|
||||
(define-internal-type-constructor Name)
|
||||
(define-typed-syntax (Name A ...) ≫
|
||||
[⊢ A ≫ A- ⇐ k_in] ...
|
||||
(define-typed-syntax (Name A ... i ...) ≫
|
||||
[⊢ A ≫ A- ⇐ kA] ...
|
||||
[⊢ i ≫ i- ⇐ ki] ...
|
||||
----------
|
||||
[⊢ (Name- A- ...) ⇒ k_out])
|
||||
(struct C* (fld ...) #:transparent) ...
|
||||
(define C (unsafe-assign-type (lambda (A ...) C*) : TY)) ...
|
||||
(define-typed-syntax (elim-Name x P C** ...) ≫
|
||||
#:with ((~Π ([CA : Ck] ...) (~Π ([_ : τ_in] ...) (Name-patexpand CB ...))) ...)
|
||||
(stx-map (current-type-eval) #'(TY ...))
|
||||
;; #:with ((τ_in ...) ...)
|
||||
;; (stx-map (lambda (tins cas) (substs #'(A- ...) cas tins))
|
||||
;; #'((τ_in/X ...) ...)
|
||||
;; #'((CA ...) ...))
|
||||
[⊢ x ≫ x- ⇒ (Name-patexpand B ...)]
|
||||
; [⊢ x ≫ x- ⇐ (Name A ...)]
|
||||
[⊢ P ≫ P- ⇐ (Π ([A : k_in] ...) (→ (Name A ...) #%type))] ; prop / motive
|
||||
; [⊢ z ≫ z- ⇐ (app P- Zero)] ; zero
|
||||
; [⊢ C ≫ C- ⇐ (Π ([k : Nat]) (→ (app P- k) (app P- (Succ k))))] ; succ
|
||||
[⊢ (Name- A- ... i- ...) ⇒ k_out])
|
||||
(struct C/internal (fld ...) #:transparent) ...
|
||||
(define C (unsafe-assign-type (lambda (A ... i ...) C/internal) : CTY)) ...
|
||||
(define-typed-syntax (elim-Name v P Ccase ...) ≫
|
||||
#:with ((~Π ([CA : _] ... ; dont care about params, since we will immediately inst with A
|
||||
[Ci : Cki] ...)
|
||||
(~Π ([_ : τ_in/CA] ...)
|
||||
(Name-patexpand CB ... Cj ...)))
|
||||
...)
|
||||
(stx-map (current-type-eval) #'(CTY ...))
|
||||
[⊢ v ≫ v- ⇒ (Name-patexpand A ... i ...)]
|
||||
#:with ((τ_in ...) ...) (stx-map (lambda (tins cas) (substs #'(A ...) cas tins))
|
||||
#'((τ_in/CA ...) ...)
|
||||
#'((CA ...) ...))
|
||||
[⊢ P ≫ P- ⇐ (Π ([j : ki] ...) (→ (Name A ... j ...) #%type))] ; prop / motive
|
||||
;; TODO: the (app P- fld) ... is wrong, should only include recur args
|
||||
;; for now, each case consumes the number of args for each C,
|
||||
;; and then an IH for each arg
|
||||
|
|
@ -617,50 +658,44 @@
|
|||
;; 1) args of the tycon
|
||||
;; 2) args of the con
|
||||
;; 3) IH for each recursive arg
|
||||
|
||||
;; manually construct Cty, bc `syntax` isnt smart enough to figure out ellipses
|
||||
;; #:do[(printf "elim \n")
|
||||
;; (pretty-print (stx->datum this-syntax))]
|
||||
#:with (Cty ...)
|
||||
(stx-map
|
||||
(lambda (CA-Cks CAs CBs #;Cks fld-tins flds #;tins rflds c)
|
||||
#`(Π #,CA-Cks
|
||||
(Π #,fld-tins
|
||||
(→ #,@(stx-map
|
||||
(lambda (rf) #`(app (app P- #,@CAs) #,rf))
|
||||
rflds)
|
||||
(app (app P- #,@CBs) (app (app #,c #,@CAs) #,@flds))))))
|
||||
#'(([CA : Ck] ...) ...)
|
||||
#'((CA ...) ...)
|
||||
#'((CB ...) ...)
|
||||
; #'((Ck ...) ...)
|
||||
#'(([fld : τ_in] ...) ...)
|
||||
#'((fld ...) ...)
|
||||
; #'((τ_in ...) ...)
|
||||
#'((recur-fld ...) ...)
|
||||
#'(C ...))
|
||||
;; #:do[(stx-map (lambda (t) (pretty-print (stx->datum t))((current-type-eval) t)) #'(Cty ...))]
|
||||
;; #:do[(pretty-print (stx->datum #'(Cty ...)))]
|
||||
[⊢ C** ≫ C- ⇐ Cty] ...
|
||||
;; [⊢ C* ≫ C- ⇐ (Π ([CA : Ck] ...)
|
||||
;; (Π ([fld : τ_in] ...)
|
||||
;; (→ (app (app P- CA ...) recur-fld) ... ; IHs
|
||||
;; (app (app P- CA ...) (app (app C CA ...) fld ...)))))] ...
|
||||
;; #:with (Cty ...)
|
||||
;; (stx-map
|
||||
;; (lambda (CA-Cks CAs CBs #;Cks fld-tins flds #;tins rflds c)
|
||||
;; #`(Π #,CA-Cks
|
||||
;; (Π #,fld-tins
|
||||
;; (→ #,@(stx-map
|
||||
;; (lambda (rf) #`(app (app P- #,@CAs) #,rf))
|
||||
;; rflds)
|
||||
;; (app (app P- #,@CBs) (app (app #,c #,@CAs) #,@flds))))))
|
||||
;; #'(([CA : Ck] ...) ...)
|
||||
;; #'((CA ...) ...)
|
||||
;; #'((CB ...) ...)
|
||||
;; ; #'((Ck ...) ...)
|
||||
;; #'(([fld : τ_in] ...) ...)
|
||||
;; #'((fld ...) ...)
|
||||
;; ; #'((τ_in ...) ...)
|
||||
;; #'((recur-fld ...) ...)
|
||||
;; #'(C ...))
|
||||
[⊢ Ccase ≫ Ccase- ⇐ (Π ([Ci : Cki] ...)
|
||||
(Π ([fld : τ_in] ...)
|
||||
(→ (app (app P- Cir ...) recur-fld) ... ; IHs
|
||||
(app (app P- Cj ...)
|
||||
(app (app C A* ... Ci ...) fld ...)))))] ...
|
||||
-----------
|
||||
[⊢ (match-Name x- P- C- ...) ⇒ (app (app P- B ...) x-)])
|
||||
; (struct match-Name/delayed (m))
|
||||
[⊢ (match-Name v- P- Ccase- ...) ⇒ (app (app P- i ...) v-)])
|
||||
(define-syntax match-Name
|
||||
(syntax-parser
|
||||
#;[(_ . args)
|
||||
#:do[(printf "trying to match:\n~a\n" (stx->datum #'args))]
|
||||
#:when #f #'(void)]
|
||||
[(_ n P Ccase ...)
|
||||
(syntax-parse #'n
|
||||
[((~literal #%plain-app) ((~literal #%plain-app) C-:id CA ...) fld ...)
|
||||
(syntax-parse (local-expand #'n 'expression null)
|
||||
[((~literal #%plain-app) ((~literal #%plain-app) CC:id CA ... Ci ...) fld ...)
|
||||
#:with (_ CC- . _) (local-expand #'(C 'CA ...) 'expression null)
|
||||
#:when (free-identifier=? #'CC #'CC-)
|
||||
; #:do[(printf "matched ~a\n" #'C-)]
|
||||
;; TODO: check C- matches actual C
|
||||
;; for now, it's just an arity match
|
||||
#'(app/eval (app/eval (app/eval Ccase CA ...) fld ...) (match-Name recur-fld P Ccase ...) ...)] ...
|
||||
#'(app/eval (app/eval (app/eval Ccase Ci ...) fld ...) (match-Name recur-fld P Ccase ...) ...)] ...
|
||||
[_ #'(#%app match/delayed 'match-Name (void n P Ccase ...))])]))
|
||||
)]])
|
||||
;; ;; #:with res (if (typecheck? #'n- (expand/df #'Z))
|
||||
|
|
@ -764,7 +799,7 @@
|
|||
;; [s : (Π ([k : Nat]) (→ (P k) (P (S k))))]
|
||||
;; [n : Nat])
|
||||
;; #'(#%app- nat-ind- P z s n)))
|
||||
(struct match/delayed (name args))
|
||||
(struct match/delayed (name args) #:transparent)
|
||||
;; #;(define-syntax match/eval
|
||||
;; (syntax-parser
|
||||
;; [(_ n zc sc) #:do[(printf "matching: ~a\n" (stx->datum #'n))] #:when #f #'(void)]
|
||||
|
|
|
|||
|
|
@ -7,7 +7,12 @@
|
|||
[Z : (→ Nat)]
|
||||
[S : (→ Nat Nat)])
|
||||
|
||||
(define-datatype List : (→ * *)
|
||||
;; some basic tests
|
||||
(check-type Nat : *)
|
||||
;; this test wont work if define-datatype uses define-base-type
|
||||
(check-type (λ ([x : Nat]) Nat) : (→ Nat *))
|
||||
|
||||
(define-datatype List : (→ * (→ *))
|
||||
[null : (∀ (A) (→ (List A)))]
|
||||
[cons : (∀ (A) (→ A (List A) (List A)))])
|
||||
|
||||
|
|
@ -21,10 +26,10 @@
|
|||
;; length 0
|
||||
(check-type
|
||||
(elim-List ((null Nat))
|
||||
(λ ([A : *]) (λ ([l : (List A)]) Nat))
|
||||
(λ ([A : *]) (λ () (λ () (Z))))
|
||||
(λ ([A : *])
|
||||
(λ ([x : A][xs : (List A)])
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat
|
||||
|
|
@ -33,10 +38,10 @@
|
|||
;; length 1
|
||||
(check-type
|
||||
(elim-List ((cons Nat) (Z) ((null Nat)))
|
||||
(λ ([A : *]) (λ ([l : (List A)]) Nat))
|
||||
(λ ([A : *]) (λ () (λ () (Z))))
|
||||
(λ ([A : *])
|
||||
(λ ([x : A][xs : (List A)])
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat
|
||||
|
|
@ -45,30 +50,64 @@
|
|||
;; length 2
|
||||
(check-type
|
||||
(elim-List ((cons Nat) (S (Z)) ((cons Nat) (Z) ((null Nat))))
|
||||
(λ ([A : *]) (λ ([l : (List A)]) Nat))
|
||||
(λ ([A : *]) (λ () (λ () (Z))))
|
||||
(λ ([A : *])
|
||||
(λ ([x : A][xs : (List A)])
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))
|
||||
: Nat
|
||||
-> (S (S (Z))))
|
||||
|
||||
(define-type-alias len
|
||||
(define-type-alias len/Nat
|
||||
(λ ([lst : (List Nat)])
|
||||
(elim-List lst
|
||||
(λ ([A : *]) (λ ([l : (List A)]) Nat))
|
||||
(λ ([A : *]) (λ () (λ () (Z))))
|
||||
(λ ([A : *])
|
||||
(λ ([x : A][xs : (List A)])
|
||||
(λ () (λ ([l : (List Nat)]) Nat))
|
||||
(λ () (λ () (λ () (Z))))
|
||||
(λ ()
|
||||
(λ ([x : Nat][xs : (List Nat)])
|
||||
(λ ([IH : Nat])
|
||||
(S IH)))))))
|
||||
|
||||
(check-type (len ((null Nat))) : Nat -> (Z))
|
||||
(check-type (len ((cons Nat) (Z) ((null Nat)))) : Nat -> (S (Z)))
|
||||
(check-type (len/Nat ((null Nat))) : Nat -> (Z))
|
||||
(check-type (len/Nat ((cons Nat) (Z) ((null Nat)))) : Nat -> (S (Z)))
|
||||
|
||||
;; Vect: "lists" parameterized over length --------------------
|
||||
(define-datatype Vect : (→ * Nat *)
|
||||
(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))))])
|
||||
|
||||
|
|
@ -88,35 +127,135 @@
|
|||
(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)))
|
||||
(λ ([A : *][k : Nat]) (λ ([v : (Vect A k)]) Nat))
|
||||
(λ ([A : *][k : Nat]) (λ () (λ () (Z))))
|
||||
(λ ([A : *][k : Nat])
|
||||
(λ ([x : A][xs : (Vect A k)])
|
||||
(λ ([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))))
|
||||
(λ ([A : *][k : Nat]) (λ ([v : (Vect A k)]) Nat))
|
||||
(λ ([A : *][k : Nat]) (λ () (λ () (Z))))
|
||||
(λ ([A : *][k : Nat])
|
||||
(λ ([x : A][xs : (Vect A k)])
|
||||
(λ ([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)))))
|
||||
(λ ([A : *][k : Nat]) (λ ([v : (Vect A k)]) Nat))
|
||||
(λ ([A : *][k : Nat]) (λ () (λ () (Z))))
|
||||
(λ ([A : *][k : Nat])
|
||||
(λ ([x : A][xs : (Vect A k)])
|
||||
(λ ([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)))))))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user