;prop -> quant varlist sep prop | prop1 | prop1 ==> prop

;prop1 -> prop2 | prop2 & prop1

;prop2 -> prop3 | ~ prop2

;prop3 -> atom | (prop)

;atom -> exp in exp | exp subset exp | exp = exp

; exp -> exp1 | exp1 intersection exp | exp1 union exp 

; exp1 -> exp2 | exp2 . exp1 | exp2 x exp1 

; exp2 -> exp3 | exp3 * | exp3 + 

; exp3 -> ID | [exp .. exp] | ( exp ) | { exp } 

(load-file "tokenize.ath")

(define (parse-error str toks)
  (begin 
    (match str
      ([] (begin (print "\nParsing error on tokens: ") (write toks)))
      (_ (begin (print str) (write 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 (parse-exp 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 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 toks)
          (match (parse-exp3 toks)
	    ([e (list-of STAR rest)] [(tc e) rest])
	    ([e (list-of PLUS-STAR rest)] [(rtc e) rest])
            ([e rest] [e rest]))
       (parse-exp3 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) rest) (match (look-up (id->string id))
				       ('none [(string->var (id->string id)) rest])
				       ([v] [v rest]))))
       (parse-exps 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 [])))


(define (p str) (parse-exp (tokenize str)))

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

(define (parse-term str) (head (p str)))

(define (make-atom bc e1 e2)
  (match bc 
    (IN (in e1 e2))
    (SUBSET (subset e1 e2))
    (EQ (= e1 e2))))
   
(define (parse-atom toks)
  (match (parse-exp toks)
    ([e (list-of bcon rest)] (match (parse-exp rest)
 			       ([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 (parse-prop 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 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 toks)
	  (match toks
	    ((list-of NOT rest) (match (parse-prop2 rest)
				  ([Q rest'] [(not Q) rest'])))
	    (_ (parse-prop3 toks)))
	(parse-prop3 toks)
	    (try (match (parse-exp toks)
		   ([e (list-of bc rest)] (match (parse-exp rest)
	        			    ([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 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''])))))))




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


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


(define pf prove-from)

(define (parse-prop str) (head (p str)))

(use-term-parser parse-term)

(use-prop-parser parse-prop)