logical-mess.scm 9/4

logical-mess.scm

;; 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)))]))

martin-löf type theory in scheme in miniKanren in scheme