[math] better expt: when only exponent is known

This commit is contained in:
Ben Greenman 2016-05-22 19:15:12 -04:00
parent d43d918486
commit 911d376361
3 changed files with 12 additions and 3 deletions

View File

@ -15,6 +15,7 @@
(ann (let ([n 4]) (/: n n)) One)
(ann (let ([n 2]) (expt: 3 (-: n n))) One)
(ann (expt: 3 2) Zero)
(ann ((lambda ([x : Natural]) (expt x 3)) 2) Index)
;; -- lambda => back to racket/base
(ann ((lambda ([f : (-> Natural Natural Natural)]) (f 0 0)) +:) Zero)
(ann ((lambda ([f : (-> Natural Natural Integer)]) (f 0 0)) -:) Zero)

View File

@ -151,5 +151,8 @@
(define-num: n2 2)
(ann (-: (expt: n1 n2) 64) Zero))
0)
(check-true
(and (ann (lambda ([n : Natural]) (expt: n 0)) (-> Natural One)) #t))
(check-true
(and (ann (lambda ([n : Index]) (expt: n 1)) (-> Index Index)) #t))
)

View File

@ -119,6 +119,11 @@
[(_ n1 n2)
(let ([v1 (stx->num #'n1)]
[v2 (stx->num #'n2)])
(and v1 v2 ;; Should never fail
(quasisyntax/loc stx #,(expt v1 v2))))]
(cond
[(and v1 v2)
(quasisyntax/loc stx #,(expt v1 v2))]
[(and v2 (<= 0 v2 10))
(quasisyntax/loc stx (* #,@(for/list ([_i (in-range v2)]) (quasisyntax/loc stx n1))))]
[else
#f]))]
[_ #f]))))