(load-file "list.ath")
(load-file "set.ath")
(load-file "tuple.ath")

(domain Att)

(domain Val)

(structure Name
  (name (List-Of (Triple-Of Att Val Name))))

(domain Rec)

(structure WVal
  (val Val)
  wildcard)

(structures
  (DB (db (List-Of (Pair-Of Att (List-Of VR)))))
  (VR (vr-entry Val (List-Of Rec) DB)))

(structure Query
  (query (List-Of (Triple-Of Att WVal Query))))


(declare lookup (-> (Query DB) (List-Of Rec)))
(declare locate-att-wval (-> (Att WVal Query DB) (List-Of Rec)))
(declare locate-wval (-> (WVal Query (List-Of VR)) (List-Of Rec)))
(declare recs-of-db (-> (DB) (List-Of Rec)))
(declare recs-of-vrl (-> ((List-Of VR)) (List-Of Rec)))


(define recs-of-db-axiom1
  (= (recs-of-db (db nil)) nil))

(define recs-of-db-axiom2
  (forall ?a ?vrl ?rest
    (= (recs-of-db (db (cons (pair ?a ?vrl) ?rest)))
       (append (recs-of-vrl ?vrl) (recs-of-db (db ?rest))))))

(assert recs-of-db-axiom1 recs-of-db-axiom2)


(define recs-of-vrl-axiom1
  (= (recs-of-vrl nil) nil))

(define recs-of-vrl-axiom2
  (forall ?v ?rl ?d ?rest
    (= (recs-of-vrl (cons (vr-entry ?v ?rl ?d) ?rest))
       (append ?rl (append (recs-of-db ?d) (recs-of-vrl ?rest))))))

(assert recs-of-vrl-axiom1 recs-of-vrl-axiom2)


(define locate-wval-axiom1
  (forall ?q ?vrl
    (= (locate-wval wildcard ?q ?vrl)
       (recs-of-vrl ?vrl))))

(define locate-wval-axiom2
  (forall ?v ?q
    (= (locate-wval (val ?v) ?q nil) nil)))

(define locate-wval-axiom3
  (forall ?v ?rl ?q ?d ?rest
    (= (locate-wval (val ?v) ?q (cons (vr-entry ?v ?rl ?d) ?rest))
       (append (lookup ?q ?d) ?rl))))

(define locate-wval-axiom4
  (forall ?v ?v' ?rl ?q ?d ?rest
    (if (not (= ?v ?v'))
        (= (locate-wval (val ?v) ?q (cons (vr-entry ?v' ?rl ?d) ?rest))
           (locate-wval (val ?v) ?q ?rest)))))

(assert locate-wval-axiom1 locate-wval-axiom2 locate-wval-axiom3 locate-wval-axiom4)


(define locate-att-wval-axiom1
  (forall ?a ?wv ?q
    (= (locate-att-wval ?a ?wv ?q (db nil)) nil)))

(define locate-att-wval-axiom2
  (forall ?a ?wv ?q ?rest ?vrl
    (= (locate-att-wval ?a ?wv ?q (db (cons (pair ?a ?vrl) ?rest)))
       (locate-wval ?wv ?q ?vrl))))

(define locate-att-wval-axiom3
  (forall ?a ?a' ?wv ?q ?rest ?vrl
    (if (not (= ?a ?a'))
        (= (locate-att-wval ?a ?wv ?q (db (cons (pair ?a' ?vrl) ?rest)))
           (locate-att-wval ?a ?wv ?q (db ?rest))))))

(assert locate-att-wval-axiom1 locate-att-wval-axiom2 locate-att-wval-axiom3)


(define lookup-axiom1
  (forall ?db
    (= (lookup (query nil) ?db) (recs-of-db ?db))))

(define lookup-axiom2
  (forall ?a ?wv ?q ?rest ?db
    (= (lookup (query (cons (triple ?a ?wv ?q) ?rest)) ?db)
       (list-inter (locate-att-wval ?a ?wv ?q ?db) (lookup (query ?rest) ?db)))))

(assert lookup-axiom1 lookup-axiom2)


;;=============================================================================================
;; A full-correctness spec using paths and branches: 

(define QueryPath (List-Of (Pair-Of Att WVal)))
(define DBPath (List-Of (Triple-Of Att Val (List-Of Rec))))

(declare query-path (-> (QueryPath Query) Boolean))
(declare query-branch (-> (QueryPath Query) Boolean))
(declare db-path (-> (DBPath DB) Boolean))
(declare qd-prefix (-> (QueryPath DBPath) Boolean))

(define query-path-axiom-1
  (forall ?q 
    (query-path nil ?q)))

(define query-path-axiom-2
  (forall ?a ?v ?q ?children ?rest
    (if (and (list-elem (triple ?a ?v ?q) ?children)
	     (query-path ?rest ?q))
	(query-path (cons (pair ?a ?v) ?rest) (query ?children)))))

(define db-path-axiom-1
  (forall ?d (db-path nil ?d)))

(define db-path-axiom-2
  (forall ?a ?v ?rest ?av-list
    (if (exists ?vrl ?recs ?d
          (and (list-elem (pair ?a ?vrl) ?av-list)
	       (and (list-elem (vr-entry ?v ?recs ?d) ?vrl)
		    (db-path ?rest ?d))))
	(db-path (cons (triple ?a ?v ?recs) ?rest) (db ?av-list)))))

(define qd-prefix-axiom-1
  (forall ?p (qd-prefix nil ?p)))

(define qd-prefix-axiom-2
  (forall ?a ?v ?rl ?rest ?rest'
    (if (qd-prefix ?rest ?rest') 
    	(qd-prefix (cons (pair ?a (val ?v)) ?rest)
	           (cons (triple ?a ?v ?rl) ?rest')))))

;;=============================================================================================

;;;;;;;;;;;;;;;; subtree is here defined as a translation of its impementation,
;;;;;;;;;;;;;;;; but we can instead have a shorter specification

(declare subtree (-> (Query Name) Boolean))
(declare subtree-att-val (-> (Att Val Query Name) Boolean))

(define subtree-axiom1
  (forall ?n
    (subtree (query nil) ?n)))

(define subtree-axiom2
  (forall ?a ?q ?rest ?n
   (if (subtree (query ?rest) ?n)
       (subtree (query (cons (triple ?a wildcard ?q) ?rest)) ?n))))

(define subtree-axiom3
  (forall ?a ?v ?q ?rest ?n
   (if (and (subtree-att-val ?a ?v ?q ?n) (subtree (query ?rest) ?n))
       (subtree (query (cons (triple ?a (val ?v) ?q) ?rest)) ?n))))

(assert subtree-axiom1 subtree-axiom2 subtree-axiom3)


(define subtree-att-val-axiom1
  (forall ?a ?v ?q
    (subtree-att-val ?a ?v ?q (name nil))))

(define subtree-att-val-axiom2
  (forall ?a ?v ?q ?n ?rest
    (if (subtree ?q ?n)
        (subtree-att-val ?a ?v ?q (name (cons (triple ?a ?v ?n) ?rest))))))

(define subtree-att-val-axiom3
  (forall ?a ?a' ?v ?v' ?q ?n ?rest
    (if (or (not (= ?a ?a')) (not (= ?v ?v')))
        (if (subtree-att-val ?a ?v ?q (name ?rest))
            (subtree-att-val ?a ?v ?q (name (cons (triple ?a' ?v' ?n) ?rest)))))))

(assert subtree-att-val-axiom1 subtree-att-val-axiom2 subtree-att-val-axiom3)


;;;;;;;;;;;;;;;; "ins-add" as translated from an implementation
;;;;;;;;;;;;;;;; the name "add" clashed with the stadard library

(declare ins-add (-> (Name Rec DB) DB))
(declare ins-add-att-val (-> (Att Val Name Rec DB) (List-Of (Pair-Of Att (List-Of VR)))))
(declare ins-add-val (-> (Val Name Rec (List-Of VR)) (List-Of VR)))
(declare graft (-> (Val Name Rec (List-Of Rec) DB) VR))

(define ins-add-axiom1
  (forall ?r ?d
    (= (ins-add (name nil) ?r ?d) ?d)))

(define ins-add-axiom2
  (forall ?a ?v ?n ?rest ?r ?d
    (= (ins-add (name (cons (triple ?a ?v ?n) ?rest)) ?r ?d)
       (ins-add (name ?rest) ?r (db (ins-add-att-val ?a ?v ?n ?r ?d))))))

(assert ins-add-axiom1 ins-add-axiom2)


(define ins-add-att-val-axiom1
  (forall ?a ?v ?n ?r
    (= (ins-add-att-val ?a ?v ?n ?r (db nil))
       (cons (pair ?a (cons (graft ?v ?n ?r nil (db nil)) nil)) nil))))

(define ins-add-att-val-axiom2
  (forall ?a ?v ?n ?r ?vrl ?rest
    (= (ins-add-att-val ?a ?v ?n ?r (db (cons (pair ?a ?vrl) ?rest)))
       (cons (pair ?a (ins-add-val ?v ?n ?r ?vrl)) ?rest))))

(define ins-add-att-val-axiom3
  (forall ?a ?v ?n ?r ?a' ?vrl ?rest
    (if (not (= ?a ?a'))
        (= (ins-add-att-val ?a ?v ?n ?r (db (cons (pair ?a' ?vrl) ?rest)))
           (cons ?p (ins-add-att-val ?a ?v ?n ?r (db ?rest)))))))

(assert ins-add-att-val-axiom1 ins-add-att-val-axiom2 ins-add-att-val-axiom3)


(define ins-add-val-axiom1
  (forall ?v ?n ?r
    (= (ins-add-val ?v ?n ?r nil)
       (cons (graft ?v ?n ?r nil (db nil)) nil))))

(define ins-add-val-axiom2
  (forall ?v ?n ?r ?rl ?d ?rest
    (= (ins-add-val ?v ?n ?r (cons (vr-entry ?v ?rl ?d) ?rest))
       (cons (graft ?v ?n ?r ?rl ?d) ?rest))))

(define ins-add-val-axiom3
  (forall ?v ?n ?r ?v' ?rl ?d ?rest
    (if (not (= ?v ?v'))
        (= (ins-add-val ?v ?n ?r (cons (vr-entry ?v' ?rl ?d) ?rest))
           (cons ?t (ins-add-val ?v ?n ?r ?rest))))))

(assert ins-add-val-axiom1 ins-add-val-axiom2 ins-add-val-axiom3)


(define graft-axiom1
  (forall ?v ?n ?r ?rl ?d
    (= (graft ?v (name nil) ?r ?rl ?d)
       (vr-entry ?v (cons ?r ?rl) ?d))))

(define graft-axiom2
  (forall ?v ?n ?r ?h ?rest ?rl ?d
    (= (graft ?v (name (cons ?h ?rest)) ?r ?rl ?d)
       (vr-entry ?v ?rl (ins-add (name (cons ?h ?rest)) ?r ?d)))))

(assert graft-axiom1 graft-axiom2)


(define goal-lookup-ins-add1
  (forall ?r ?q
    (not (list-elem ?r (lookup ?q (db nil))))))

(define goal-lookup-ins-add2
  (forall ?q ?d ?n ?r
    (forall ?r'
      (iff (list-elem ?r' (lookup ?q (ins-add ?n ?r ?d)))
           (or (subtree ?q ?n)
               (list-elem ?r' (lookup ?q ?d)))))))

;;;;;;;;;;;;;;;; "get" as translated from an implementation

(declare get (-> (Rec DB) Name))
(declare get-att-val (-> (Att (List-Of VR) Rec) Name))
(declare combine (-> (Name Name) Name))

(define get-axiom1
  (forall ?r
    (= (get ?r (db nil)) (name nil))))

(define get-axiom2
  (forall ?r ?a ?lvr ?rest
    (= (get ?r (db (cons (pair ?a ?lvr) ?rest)))
       (combine (get-att-val ?a ?lvr ?r) (get ?r (db ?rest))))))

(assert get-axiom1 get-axiom2)


(define get-att-val-axiom1
  (forall ?a ?r
    (= (get-att-val ?a nil ?r)
       (name nil))))

(define get-att-val-axiom2
  (forall ?a ?v ?lr ?d ?rest ?r
    (= (get-att-val ?a (cons (vr-entry ?v ?lr ?d) ?rest) ?r)
       (combine    (name nil) (name nil)))));(dummy ...) (get-att-val ?a ?rest ?r)))))
;;           (check ((member? r (unmklist lr)) (name (singleton (triple a v (name nil)))))
;;                  (else (let ((n (get r d)))
;;                          (match n
;;                            ((name nil) n)
;;                            (_ (name (singleton (triple a v n))))))))

(assert get-att-val-axiom1 get-att-val-axiom2)


(define combine-axiom
  (forall ?l1 ?l2 ?l3
    (iff (= (combine (name ?l1) (name ?l2)) (name ?l3))
         (= (append ?l1 ?l2) ?l3))))

(assert combine-axiom)


(define goal-get-ins-add1
  (forall ?r
    (= (get ?r (db nil)) (name nil))))

(define goal-get-ins-add2
  (forall ?r ?n ?d
    (= (get ?r (ins-add ?n ?r ?d)) ?n)))

(define goal-get-ins-add3
  (forall ?r ?r' ?n ?d
    (if (not (= ?r ?r'))
        (= (get ?r (ins-add ?n ?r' ?d)) (get ?r ?d)))))