;; (load-file "elms-lemmas-new-1.ath")

(load-file "tokenize.ath")

(define (parse-error str toks) (halt))

(define (parse-vars toks)
   (letrec ((loop (function (toks res)
		    (match toks
		      ((list-of (ID id) rest) (loop rest (add (string->var (id->string id)) res)))
		      ((list-of SEP rest) [(rev res) rest]))))) 
     (loop toks [])))

(define (number? id)
  (match (id->string id)
    ("0" 'zero)
    ("1" 'one)
    (_ 'none)))

(define (parse-exp toks look-up)
(letrec ((parse-exp (function (toks)
  	    (match (parse-exp1 toks)
	      ([e (list-of INTER rest)] (match (parse-exp rest) ([e' rest'] [(intersection e e') rest'])))
	      ([e (list-of UNION rest)] (match (parse-exp rest) ([e' rest'] [(union e e') rest'])))
	      ([e rest] [e rest]))))
         (parse-exp1 (function (toks)
 	  (match (parse-exp2 toks)
	    ([e (list-of DOT rest)] (match (parse-exp1 rest) ([e' rest'] [(sbdot e e') rest'])))
	    ([e rest] [e rest]))))
       (parse-exp2 (function (toks)
          (match (parse-exp3 toks)
	    ([e (list-of STAR rest)] [(rtc e) rest])
	    ([e (list-of PLUS-STAR rest)] [(tc e) rest])
	    ([e (list-of EXP-OP rest)] (match (parse-exponent rest)
                                         ([(+ x (succ zero)) rest'] [(pow e (succ x)) rest'])
                                         ([num-exp rest'] [(pow e num-exp) rest'])))
            ([e rest] [e rest]))))
       (parse-exp3 (function (toks)
           (match toks
	    ((list-of LPAREN rest) (match (parse-exp rest) 
				     ([e (list-of RPAREN rest')] [e rest'])
				     (_ (parse-error "Right parenthesis expected here." rest))))
	    ((list-of LSQB rest) (match (parse-exps rest) 
				     ([exps (list-of RSQB rest')] [(tup exps) rest'])
				     (_ (parse-error "Right square bracket expected here." rest))))
	    ((list-of LBRACK rest) (match (parse-exp rest)
				     ([e (list-of RBRACK rest')] [(singl e) rest'])
			 	     ([e rest'] (parse-error "Right bracket expected here." rest'))))
	    ((list-of (ID id) (list-of LPAREN rest)) (match (parse-args rest [])
						       ([exps (list-of RPAREN rest')] 
							  [(make-term (parse-id id) exps) rest'])))
	    ((list-of (ID id) rest) [(parse-id id) rest]))))
       (parse-args (function (toks res)
	             (match toks
		       ((list-of RPAREN _) [(rev res) toks])
                       (_ (match (parse-exp toks)
			    ([e (list-of COMMA rest)] (parse-args rest (add e res)))
			    ([e rest] (parse-args rest (add e res))))))))
       (parse-id (function (id)
		   (match (look-up (id->string id))
		     ('none (string->var (id->string id)))
		     ([v] v))))
       (parse-exps (function (toks)
	  (letrec ((loop (function (toks res)
			    (match toks
			      ((list-of RSQB rest) [(rev res) toks])
                              (_ (match (parse-exp toks)
					  ([e rest] (loop rest (add e res)))))))))
            (loop toks []))))
       (parse-exponent (function (toks)
 			 (match toks
                           ((list-of (ID id) (list-of PLUS-STAR rest)) 
                              (match (parse-exponent rest)
                                ([e rest'] [(+ (parse-id id) e) rest'])))
                           ((list-of (ID id) rest) (match (number? id)
						     ('zero [zero rest])
						     ('one [(succ zero) rest])
          					     (_ [(parse-id id) rest])))))))
  (parse-exp toks)))



(define (parse-exp' toks vars lu)
(let ((var-strings (map var->string vars))
       (parse-id (function (id)
                   (let ((id-str (id->string id)))
                     (check ((member? id-str var-strings)  (string->var id-str))
 		            (else (match (lu id-str)
 		                    ('none (string->var id-str))
 		                    ([v] v))))))))
 (letrec ((parse-exp (function (toks)
  	    (match (parse-exp1 toks)
	      ([e (list-of INTER rest)] (match (parse-exp rest) ([e' rest'] [(intersection e e') rest'])))
	      ([e (list-of UNION rest)] (match (parse-exp rest) ([e' rest'] [(union e e') rest'])))
	      ([e rest] [e rest]))))
         (parse-exp1 (function (toks)
 	  (match (parse-exp2 toks)
	    ([e (list-of DOT rest)] (match (parse-exp1 rest) ([e' rest'] [(sbdot e e') rest'])))
	    ([e rest] [e rest]))))
       (parse-exp2 (function (toks)
          (match (parse-exp3 toks)
	    ([e (list-of STAR rest)] [(rtc e) rest])
	    ([e (list-of PLUS-STAR rest)] [(tc e) rest])
	    ([e (list-of EXP-OP rest)] (match (parse-exponent rest)
                                         ([(+ x (succ zero)) rest'] [(pow e (succ x)) rest'])
                                         ([num-exp rest'] [(pow e num-exp) rest'])))
            ([e rest] [e rest]))))
       (parse-exp3 (function (toks)
           (match toks
	    ((list-of LPAREN rest) (match (parse-exp rest) 
				     ([e (list-of RPAREN rest')] [e rest'])
				     (_ (parse-error "Right parenthesis expected here." rest))))
	    ((list-of LSQB rest) (match (parse-exps rest) 
				     ([exps (list-of RSQB rest')] [(tup exps) rest'])
				     (_ (parse-error "Right square bracket expected here." rest))))
	    ((list-of LBRACK rest) (match (parse-exp rest)
				     ([e (list-of RBRACK rest')] [(singl e) rest'])
			 	     ([e rest'] (parse-error "Right bracket expected here." rest'))))
	    ((list-of (ID id) (list-of LPAREN rest)) (match (parse-args rest [])
						       ([exps (list-of RPAREN rest')] 
							   [(make-term (parse-id id) exps) rest'])))
	    ((list-of (ID id) rest) [(parse-id id) rest]))))
       (parse-exponent (function (toks)
 			 (match toks
                           ((list-of (ID id) (list-of PLUS-STAR rest)) 
                              (match (parse-exponent rest)
                                ([e rest'] [(+ (parse-id id) e) rest'])))
                           ((list-of (ID id) rest) (match (number? id)
						     ('zero [zero rest])
						     ('one [(succ zero) rest])
          					     (_ [(parse-id id) rest]))))))
       (parse-args (function (toks res)
	             (match toks
		       ((list-of RPAREN _) [(rev res) toks])
                       (_ (match (parse-exp toks)
			    ([e (list-of COMMA rest)] (parse-args rest (add e res)))
			    ([e rest] (parse-args rest (add e res))))))))
       (parse-exps (function (toks)
	  (letrec ((loop (function (toks res)
			    (match toks
			      ((list-of RSQB rest) [(rev res) toks])
                              (_ (match (parse-exp toks)
					  ([e rest] (loop rest (add e res)))))))))
            (loop toks [])))))
  (parse-exp toks))))


; (p "S.R* union U")

; (p "S.R* union U")

(define (parse-term str look-up) (head (parse-exp (tokenize str) look-up)))

(define (pt str) (head (parse-exp' (tokenize str) [] look-up)))

(define (p s) (parse-term s look-up))

(define (make-atom bc e1 e2)
  (match bc 
    (IN (in e1 e2))
    (SUBSET (subset e1 e2))
    (EQ (= e1 e2))))
   
;(define (parse-atom toks look-up)
;  (match (parse-exp toks look-up)
;    ([e (list-of bcon rest)] (match (parse-exp rest look-up)
; 			       ([e' rest'] [(make-atom bcon e e') rest'])))))

(define (get-rem f toks P sym)
  (match (f toks)
    ([Q rest] [(sym P Q) rest])
    (_ (parse-error "" toks))))

(define (get-rem' f toks vars P sym)
  (match (f toks vars)
    ([Q rest] [(sym P Q) rest])
    (_ (parse-error "" toks))))

(define (parse-prop toks look-up)
  (letrec ((parse-prop (function (toks)
   	    (try (parse-quantified-prop toks)
               (match (parse-prop1 toks)
		 ([P (list-of IF rest)]  (get-rem parse-prop rest P if))
 	         ([P (list-of IFF rest)] (get-rem parse-prop rest P iff))
 	         (res res)))))
     	(parse-prop1 (function (toks)
	  (match (parse-prop2 toks)
	    ([P (list-of AND rest)] (get-rem parse-prop1 rest P and))
	    ([P (list-of OR rest)]  (get-rem parse-prop1 rest P or))
	    (res res))))
	(parse-prop2 (function (toks)
	  (match toks
	    ((list-of NOT rest) (match (parse-prop2 rest)
				  ([Q rest'] [(not Q) rest'])))
	    (_ (parse-prop3 toks)))))
	(parse-prop3 (function (toks)
	    (try (match (parse-exp toks look-up)
		   ([e (list-of bc rest)] (match (parse-exp rest look-up)
	        			    ([e' rest'] [(make-atom bc e e') rest']))))
		 (match toks
	           ((list-of LPAREN rest) (match (parse-prop rest)
					    ([P (list-of RPAREN rest')] [P rest'])
					    ([_ rest'] (parse-error "Right parenthesis expected here." rest'))))))))
	(parse-quantified-prop (function (toks)
	  (match toks
	    ((list-of ALL rest) (match (parse-vars rest)
				  ([vars rest'] (match (parse-prop rest')
						  ([P rest''] [(quant* forall vars P) rest''])))))
	    ((list-of SOME rest) (match (parse-vars rest)
				   ([vars rest'] (match (parse-prop rest')
					 	   ([P rest''] [(quant* exists vars P) rest''])))))))))
  (parse-prop toks)))

(define (parse-prop' toks look-up)
  (letrec ((parse-prop (function (toks vars)
   	    (try (parse-quantified-prop toks vars)
               (match (parse-prop1 toks vars)
		 ([P (list-of IF rest)]  (get-rem' parse-prop rest vars P if))
 	         ([P (list-of IFF rest)] (get-rem' parse-prop rest vars P iff))
 	         (res res)))))
     	(parse-prop1 (function (toks vars)
	  (match (parse-prop2 toks vars)
	    ([P (list-of AND rest)] (get-rem' parse-prop1 rest vars P and))
	    ([P (list-of OR rest)]  (get-rem' parse-prop1 rest vars P or))
	    (res res))))
	(parse-prop2 (function (toks vars)
	  (match toks
	    ((list-of NOT rest) (match (parse-prop2 rest vars)
				  ([Q rest'] [(not Q) rest'])))
	    (_ (parse-prop3 toks vars)))))
	(parse-prop3 (function (toks vars)
	    (try (match (parse-exp' toks vars look-up)
		   ([e (list-of bc rest)] (match (parse-exp' rest vars look-up)
	        			    ([e' rest'] [(make-atom bc e e') rest']))))
		 (match toks
	           ((list-of LPAREN rest) (match (parse-prop rest vars)
					    ([P (list-of RPAREN rest')] [P rest'])
					    ([_ rest'] (parse-error "Right parenthesis expected here." rest'))))))))
	(parse-quantified-prop (function (toks vars)
	  (match toks
	    ((list-of ALL rest) (match (parse-vars rest)
				  ([vars' rest'] (match (parse-prop rest' (join vars' vars))
						   ([P rest''] [(quant* forall vars' P) rest''])))))
	    ((list-of SOME rest) (match (parse-vars rest)
				   ([vars' rest'] (match (parse-prop rest' (join vars' vars))
					 	   ([P rest''] [(quant* exists vars' P) rest''])))))))))
  (parse-prop toks [])))



(define (pp' str) (head (parse-prop' (tokenize str) look-up)))

(define (pp s look-up) (parse-prop (tokenize s) look-up))


; (pp "ALL x y z | EXISTS foo | x subset data & y = z")


(define pf prove-from)

(define (parse-prop str look-up) (head (pp str look-up)))

(define (parse-proposition str look-up) (head (parse-prop' (tokenize str) look-up)))

(use-term-parser parse-term)

(use-prop-parser parse-proposition)

(define (gp s) (parse-prop s look-up))

(define (string->prop s) (let ((c (assume s $s))) (match c ((if p _) p))))



;(set-debug-mode "detailed")

;(print-call-stack)