(define (numeric? c)
  (member? c "0123456789"))

(define o (function (f g) (function (x) (f (g x)))))

(define first head)

(define second (o first tail))

(define third (o second tail))

(define (forall* vars P)
  (match vars
    ([] P)
    ((list-of x rest) (forall* rest (forall x P)))))

(define (quant* Q var-list P)
 (match var-list 
   ([] P)
   ((list-of v more-vars) (Q v (quant* Q more-vars P)))))

(define (forall* vl P) (quant* forall vl P))

(define (exists* vl P) (quant* exists vl P))

(define (uspec* P terms)
  (dmatch terms
    ([] (dcheck ((holds? P) (!claim P)) (else (!claim true))))
    ((list-of t more-terms) (!uspec* (!uspec P t) more-terms))))

(define (zip L1 L2)
  (letrec ((f (function (L1 L2 res)
		(match [L1 L2]
		  ([(list-of x1 rest1) (list-of x2 rest2)] (f rest1 rest2 (add [x1 x2] res)))
                  (_ (rev res))))))
    (f L1 L2 [])))

(define (wl l) 
  (check ((null? l) (print "None")) (else (map-proc write l))))

(define (make-and props)
  (dmatch props
    ([P] (!claim P))
    ((list-of P rest) (!both P (!make-and rest)))))

(define (urep P terms)
  (match [P terms]
    ([(forall x Q) (list-of t more)] (urep (replace-var x t Q) more))
    (_ P)))

(define (body-of P)
  (match P
    (((some-quant Q) _ body) body)))

(define (qvar-of P)
  (match P
    (((some-quant Q) x _) x)))

(define (get-all-vars arg)
  (match arg
    ((some-term t) (vars t))
    ((some-prop P) (vars P))
    ((some-list args) (foldr join [] (map get-all-vars args)))))

(define (get-vars arg) (remove-duplicates (get-all-vars arg)))

(define (conjoin props)
  (match props
    ([P] P)
    ((list-of P rest) (and P (conjoin rest)))))

(primitive-method (equality s t)
  (check ((equal? s t) (= s t))))

(define (println s)
  (print (join "\n" s "\n")))


;(define (mread)
;  (let ((i (read))) (begin (read) i)))

(define (mread) ())


(define (show str v)
  (begin (println str) (write v)))


(define (show-read str v) (begin (print (join "\n" str "\n")) (write v) (read)))

(define (subterms t)
  (add t (fold join (map subterms (children t)) [])))

(define (constants&vars t)
  (match t 
    ((some-var v) [v])
    (((some-symbol f) (some-list args)) (check ((null? args) [f])
					       (else (fold join (map constants&vars args) []))))))


(define (from-terms P f)
  (match P
    ((some-atom A) (f A))
    ((not body) (from-terms body f))
    (((some-prop-con pc) P1 P2) (join (from-terms P1 f) (from-terms P2 f)))
    (((some-quant q) _ body) (from-terms body f))))

(define (from-terms* props f)
  (fold join (map (function (P) (from-terms P f)) props) []))

(define (prop-constants-and-vars props)
  (from-terms* props constants&vars))

(define (prop-subterms P)
  (from-terms P subterms))

(define (prop-subterms* props)
  (remove-duplicates (from-terms* props subterms)))

(define (non-var-term t)
  (match t
    (((some-symbol f) (some-list args)) true)
    (_ false)))
    
(define (prop-constants-and-free-vars props)
  (let ((fvars (fold join (map free-vars props) [])))
   (remove-duplicates (filter (from-terms* props constants&vars) 
			      (function (t) (|| (member? t fvars) (non-var-term t)))))))
				

(define (plus* L)
  (fold plus L 0))

(define (term-size t)
  (match t
    (((some-symbol f) (some-list args)) (plus* (add 1 (map term-size args))))
    (_ 1)))

(define (term-less? s t)
  (less? (term-size s) (term-size t)))

(define (no-free-vars? P)
  (null? (free-vars P)))

(define (interesting-prop-subterms P)
  (check ((no-free-vars? P) (prop-constants-and-free-vars [P]))
	 (else (prop-subterms P))))

(define (interesting-prop-subterms* props)
  (remove-duplicates (fold join (map interesting-prop-subterms props) [])))


(define (map-method M L K)
  (dletrec ((loop (method (L res)
		    (dmatch L
		      ([] (!K (rev res)))
		      ((list-of x rest) (dlet ((th (!M x)))
			  	          (!loop rest (add th res))))))))
     (!loop L [])))

(define (do-props props M K)
  (dletrec ((loop (method (props res)
                    (dmatch props
	  	      ([] (!K (rev res)))
		      ((list-of (some-prop P) rest) (dlet ((th (!M P)))
			  			      (!loop rest (add th res))))))))
     (!loop props [])))

(define (make-conjunction props)
  (dmatch props
    ([P] (!claim P))
    ((list-of P more-props) (!both P (!make-conjunction more-props)))))

(define (unify-props P1 P2)
    (letrec ((f (function (P1 P2)
		   (match [P1 P2]
    		     ([(some-atom A1) (some-atom A2)] (unify A1 A2))
		     ([(not Q1) (not Q2)] (f Q1 Q2))
		     ([((some-prop-con pc) Q1 Q2) (pc Q3 Q4)] 
			  (let ((sub1 (f Q1 Q3)))
                            (compose-subs (f (sub1 Q2) (sub1 Q4)) sub1)))
		     ([((some-quant Q) x B1) (Q y B2)] 
			  (let ((v (fresh-var)))
			    (f (replace-var x v B1) (replace-var y v B2))))
                     (_ false)))))
       (f (rename P1) P2)))

(define up unify-props)

(define (unify* v1 v2)
  (match [v1 v2]
    ([(some-term t1) (some-term t2)] (unify t1 t2))
    ([(some-prop P1) (some-prop P2)] (unify-props P1 P2))))

(define (get-conjuncts P)
  (match P
    ((and P1 P2) (join (get-conjuncts P1) (get-conjuncts P2)))
    (true [])
    (P [P])))

(primitive-method (cases P1 P2)
  (match [P1 P2]
    ([(if P Q) (if (not P) Q)] (check ((& (holds? P1) (holds? P2)) Q)))))

(define (hold? props)
  (match props
    ([] true)
    ((list-of P more) (& (holds? P) (hold? more)))))

(define (fire premise terms M)
  (dmatch premise
    ((forall (some-list vars) (if P Q)) (!mp (!uspec* premise terms) P))
    ((forall (some-list vars) (iff P Q)) 
       (dlet ((th (!M (!uspec* premise terms))))
         (dmatch th
           ((if P1 P2) (!mp th P1)))))))


(define (antecedent P)
  (match P
    ((if P1 P2) P1)))

(define (consequent P)
  (match P
    ((if P1 P2) P2)))

(define (prove-conjuncts-of P)
  (dmatch P
    ((and P1 P2) (!both P1 (!prove-conjuncts-of P2)))
    (_ (!claim P))))

(define (prove-antecedent P)
  (dmatch P
    ((if P1 P2) (!prove-conjuncts-of P1))))


(define (fire premise terms)
  (dmatch premise
    ((forall (some-list vars) (if P _)) (dlet ((th (!uspec* premise terms)))
                                          (!mp th (!prove-antecedent th))))
    ((forall (some-list vars) (iff _ _)) 
       (dlet ((th (!uspec* premise terms)))
         (dtry (dlet ((P (!left-iff th))) 
                 (!mp P (!prove-antecedent P)))
               (dlet ((P (!right-iff th)))
                 (!mp P (!prove-antecedent P))))))))


(define (~ t)
  (match t 
    (true false)
    (false true)))

(define (os p) (print (head (make-otter-prop-string [p]))))

(define pf prove-from)

(define (gp s) (match (and s s) ((and p p) p)))

;; Proves x = y from the assumption [x] in {[y]}

(define (eq-tup-parts premise)
  (dmatch premise 
    ((in (cons x unit) (singl (cons y unit)))
       (dlet ((P1 ((= (tup [x]) (tup [y])) BY (!fire singleton-axiom [(tup [x]) (tup [y])]))))
         (!left-and (!mp (!uspec* (!constructor-injectivity cons) [x unit y unit]) P1))))))

(define (eq-tup-parts1 premise)
  (dmatch premise 
    ((in (cons x unit) (singl (cons y unit)))
       (!pf (= x y) [premise (!constructor-injectivity cons) singleton-axiom]))))

(define (all-props) (fetch-all (function (P) true)))

(load-file "num.ath")

(define (map f lst)
  (match lst
    ([] [])
    ((list-of x rest) (add (f x) (map f rest)))))

(define (map-list f lst)
  (match lst
    ([] [])
    ((list-of x rest) (add (f x) (map-list f rest)))))

(define (map-proc f l)
  (match l
    ([] ())
    ((list-of x rest) (begin (f x) (map-proc f rest)))))

(define (fold f lst id)
  (match lst
    ([] [])
    ([x] (f x id))
    ((list-of x (list-of y more)) 
       (fold f (add (f x y) more) id))))

(define (foldr f e l)
  (match l
    ([] e)
    ((list-of x rest) (f x (foldr f e rest)))))

(define (length lst)
  (match lst
    ([] 0)
    ((list-of _ rest) (plus 1 (length rest)))))

(define (remove x L)
  (match L
    ((split L1 (list-of (val-of x) L2)) 
       (remove x (join L1 L2)))
    (_ L)))

(define (remove-duplicates lst)
  (match lst
    ((split L1 (list-of x (split L2 (list-of x more)))) 
       (remove-duplicates (join L1 [x] L2 more)))
    (_ lst)))

(define rd remove-duplicates)

(define (member? x l) 
  (match l
    ((split l1 (list-of (val-of x) l2)) true)
    (_ false)))

(define (for-each list pred)
  (match list
    ([] true)
    ((list-of x rest) (& (pred x) (for-each rest pred)))))

(define (subset? L1 L2)
  (for-each L1 (function (x) (member? x L2))))

(define (for-some list pred)
  (match list
    ([] false)
    ((list-of x rest) (|| (pred x) (for-some rest pred)))))

(define (filter L f)
  (match L
    ([] [])
    ((list-of x rest) (check ((f x) (add x (filter rest f)))
                             (else (filter rest f))))))

(define (list-diff L1 L2)
  (filter L1 (function (x) (~ (member? x L2)))))

(define (nth i l)
  (match [i l]
    ([1 (list-of x _)] x)
    (_ (nth (minus i 1) (tail l)))))

(define (nth-tail l n)
  (match n
    (0 l)
    (_ (nth-tail (tail l) (minus n 1)))))

(define (prefix? s1 s2)
  (match [s1 s2]
    ([[] _] true)
    ([(list-of x rest1) (list-of x rest2)] (prefix? rest1 rest2))
    (_ false)))

(define (find-min-rest l fun)
  (letrec ((f (function (rem rest min i)
		(match rem
		  ([] [min rest])
		  ((list-of x more) (check 
			              ((greater? i 0) (check ((less? (fun x) (fun min)) (f more (add min rest) x (plus i 1)))
  	 					             (else (f more (add x rest) min (plus i 1)))))
                                      (else (f more [] x (plus i 1)))))))))
    (check ((null? l) ()) (else (f l [] () 0)))))

(define (take l n)
  (letrec ((f (function (l n res)
		(match [l n]
		  ([_ 0] (rev res))
		  ([[] _] (rev res))
		  (_ (f (tail l) (minus n 1) (add (head l) res)))))))
    (f l n [])))

(define 
  (even-positions L)
    (match L
      ((list-of _ rest) (odd-positions rest))
      (_ []))
  (odd-positions L)
    (match L
      ((list-of x rest) (add x (even-positions rest)))
      (_ [])))


(define (merge L1 L2 less?)
  (match [L1 L2]
    ([(list-of x rest1) (list-of y rest2)] 
	(check ((less? x y) (add x (merge rest1 L2 less?)))
               (else (add y (merge rest2 L1 less?)))))
    ([[] _] L2)
    (_ L1)))

(define (merge-sort L less?)
  (match L
    ((list-of _ (list-of _ rest)) (merge (merge-sort (odd-positions L) less?)
				         (merge-sort (even-positions L) less?) less?))
    (_ L)))


(define (skip-until list pred)
  (match list
    ([] [])
    ((list-of x rest) (check ((pred x) list)
			     (else (skip-until rest pred))))))

(define (intersect l1 l2)
  (filter l1 (function (x) (member? x l2))))