Created
September 4, 2015 21:28
-
-
Save gbaz/96d29a782fb5cc34bd0b to your computer and use it in GitHub Desktop.
logical-mess.scm 9/4
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; Logical MESS (Logical Martin-Lof Extensible Simulater and Specification) | |
;; Gershom Bazerman, 2015 | |
(load "interp-uber.scm") | |
(load "mk/test-check.scm") | |
(load "mk/matche.scm") | |
(define ans (run 1 (q) (evalo | |
`(letrec ( | |
(reduce (lambda (cxt body) | |
(match body | |
[`(app (lam-pi ,var ,vt ,b) ,arg) | |
(if (hasType? cxt arg vt) (reduce cxt (b arg)) 'type-error)] ; todo add has-type cxt arg vt check | |
[`(app (close ,ty , b) ,arg) | |
(list 'close (app-type cxt (red-eval cxt ty arg)) (lambda (cxt) (list 'app (b cxt) arg)))] | |
[`(app ,fun ,arg) (if (or (not fun) (symbol? fun)) | |
(list 'stuck-app fun arg) | |
(reduce cxt (list 'app (reduce cxt fun) arg)))] | |
[anything body]))) | |
(app-type (lambda (cxt fun arg) | |
(match fun | |
[`(type-fun ,a ,b) | |
(if (hasType? cxt arg a) b 'type-error)] | |
[`(type-pi ,a ,at ,b) | |
(if (hasType? cxt arg a) (b arg) 'type-error)] | |
[any 'type-error]))) | |
(red-eval (lambda (cxt x) | |
(match (reduce cxt x) | |
[`(close ,typ ,b) (red-eval cxt (b cxt))] | |
[v v]))) | |
(find-cxt (lambda (nm cxt) | |
(if (null? cxt) | |
#f | |
(if (equal? (car (car cxt)) nm) | |
(cdr (car cxt)) | |
(find-cxt nm (cdr cxt)))))) | |
(fresh-var (lambda (nm cxt) | |
(if (find-cxt nm cxt) (fresh-var (quote nm)) nm))) | |
(extend-cxt (lambda (var vt cxt k) | |
(k (fresh-var var cxt) (cons (cons (fresh-var var cxt) vt) cxt)))) | |
; (letrec ((newvar (fresh-var var cxt))) ; Nested letrecs go boom | |
; (k newvar (cons (cons newvar vt) cxt))))) | |
(type? (lambda (cxt t) | |
(match (red-eval cxt t) | |
[`(type-fun ,a ,b) (and (type? cxt a) (type? cxt b))] | |
[`type-unit #t] | |
[`type #t] | |
[`(type-pi ,var ,a ,b) | |
(and (type? cxt a) (extend-cxt var a cxt (lambda (newvar newcxt) (type? newcxt (b newvar)))))] | |
[tt (and (symbol? tt) (eq? 'type (find-cxt tt cxt)))]))) ; TODO make extensible | |
(hasType? (lambda (cxt x1 t1) | |
(match (cons (reduce cxt x1) (red-eval cxt t1)) | |
[`((close ,typ ,b) . any) (eqType? cxt typ t)] | |
[`(unit . type-unit) #t] | |
[`(,(? symbol? x) . ,t) (eqType? cxt t (find-cxt x cxt))] | |
[`((lam-pi ,vn ,vt ,body) . (type-fun ,a ,b)) | |
(and (eqType? cxt vt a) | |
(extend-cxt vn vt cxt (lambda (newvar newcxt) (hasType? newcxt (body newvar) b))))] | |
[`((lam-pi ,vn ,vt ,body) . (type-pi any ,a ,b)) | |
(and (eqType? cxt vt a) | |
(extend-cxt vn vt cxt (lambda (newvar newcxt) (hasType? newcxt (body newvar) (reduce newcxt (b newvar))))))] | |
[`(,x . `type) (type? cxt x)] | |
[`(,x . ,t) #f] ; TODO make extensible | |
))) | |
(eqType? (lambda (cxt t1 t2) | |
(match (cons (red-eval cxt t1) (red-eval cxt t2)) | |
[`(,(? symbol? tname) . ,(? symbol? tname1)) (equal? tname tname1)] | |
[any #f]))) | |
) | |
; infer the type of identity at unit -- Slow | |
(hasType? '() (list 'lam-pi 'x 'type-unit (lambda (x) x)) ',q) | |
; check the type of identity at unit -- Not quite as slow | |
; (hasType? '() (list 'lam-pi 'x 'type-unit (lambda (x) x)) (list 'type-fun 'type-unit 'type-unit)) | |
; infer the term of identity at unit -- Hasn't yet finished | |
; (hasType? '() ',q (list 'type-fun 'type-unit 'type-unit)) | |
) | |
#t))) | |
(display ans) | |
; (reduce '() (list 'app (list 'lam-pi 'x 'bool (lambda (x) x)) (list 'app (list 'lam-pi 'y 'bool (lambda (x) (if x #f #t))) ',q)))) | |
; (reduce '() (list 'app (list 'lam-pi 'x 'bool (lambda (x) x)) ',q))) | |
; (reduce '() (list 'app (list 'lam-pi 'x 'bool (lambda (x) x)) #t))) | |
; (hasType? '() (list 'lam-pi 'x 'type-unit (lambda (x) x)) (list 'type-fun 'type-unit 'type-unit)) | |
; (hasType? '() ',q (list 'type-fun 'type-unit 'type-unit)) | |
;; (define (eqType? cxt t1 t2) | |
;; (match* ((red-eval cxt t1) (red-eval cxt t2)) | |
;; [((type-fun a b) (type-fun a1 b1)) | |
;; (and (eqType? cxt a a1) (eqType? cxt b b1))] | |
;; [((type-pi v a b) (type-pi v1 a1 b1)) | |
;; (and (eqType? cxt a a1) | |
;; (extend-cxt v a cxt (newvar newcxt) | |
;; (eqType? newcxt (b newvar) (b1 newvar))))] | |
;; [((? symbol? vname) (? symbol? vname1)) (eq? vname vname1)] | |
;; [((stuck-app fun arg) (stuck-app fun1 arg1)) | |
;; (and | |
;; (eqType? cxt (find-cxt fun cxt) (find-cxt fun1 cxt)) | |
;; (eqVal? cxt (find-cxt fun cxt) fun fun1) | |
;; (eqVal? cxt (head-type (find-cxt fun cxt)) arg arg1))] | |
;; [(a b) (and a b (or (eqType?-additional cxt a b) | |
;; (begin (printf "not equal\n ~a\n ~a\n cxt: ~a\n" a b cxt) #f)))])) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
martin-löf type theory in scheme in miniKanren in scheme