(load-file "general-alloy.ath")


(domain NODE)
(domain ELM)

(declare Node (Set-Of (Pair-Of NODE Unit)))
(declare Elm (Set-Of (Pair-Of ELM Unit)))
(declare next (Set-Of (Pair-Of NODE (Pair-Of NODE Unit))))
(declare data (Set-Of (Pair-Of NODE (Pair-Of ELM Unit))))

(define next-left-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) next)
        (in (tup [?x]) Node))))

(define next-right-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) next)
        (in (tup [?y]) Node))))

(define data-left-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) data)
        (in (tup [?x]) Node))))

(define data-right-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) data)
        (in (tup [?y]) Elm))))

(define membership-constraints 
  [next-left-constraint next-right-constraint data-left-constraint data-right-constraint])


(assert membership-constraints)

(define data-is-total
  (forall ?x
    (if (in (tup [?x]) Node)
        (exists ?y
          (and (holds data [?x ?y])
	       (forall ?y' 
		 (if (holds data [?x ?y'])
		     (= ?y ?y'))))))))

(assert data-is-total)

(define next-is-partial-fun
  (forall* [?x ?y ?y']
    (if (and (holds next [?x ?y])
             (holds next [?x ?y']))
        (= ?y ?y'))))

(assert next-is-partial-fun)

(declare elms (-> (NODE) (Set-Of (Pair-Of ELM Unit))))

(define elms-semantics
  (forall ?n
     (and (if (not (exists ?m (holds next [?n ?m])))
              (= (elms ?n) (sbdot (scalar ?n) data)))
          (forall ?m
            (if (holds next [?n ?m])
	        (= (elms ?n) (union (sbdot (scalar ?n) data) (elms ?m))))))))

(define elms-hc-1
  (forall ?n
    (if (not (exists ?m (holds next [?n ?m])))
        (= (elms ?n) (sbdot (scalar ?n) data)))))

(define elms-hc-2
  (forall* [?n ?m]
    (if (holds next [?n ?m])
	(= (elms ?n) (union (sbdot (scalar ?n) data) (elms ?m))))))

(assert elms-hc-1 elms-hc-2)

(assert elms-semantics)

(define horn-clauses-old
   [elms-hc-1 elms-hc-2 singleton-hc-1  union-hc-1 union-hc-2 sbdot-hc])

(define horn-clauses 
   [elms-hc-1 elms-hc-2 singleton-hc-1 union-hc-1 union-hc-2 sbdot-hc
    pow-axiom-hc1 pow-axiom-hc2 pow-axiom-hc3 tc-axiom-hc rtc-axiom-hc])

(define (special? P)
  (match P
    ((= s1 s2) (method (g) (!equality s1 s2)))
    (_ ())))

(define (cond props M)
  (dmatch props
    ([] (!M))
    ((list-of (some-prop P) rest) (assume P (!cond rest M)))))

(define (bc1 goal hyps)
  (!do-props hyps (method (P) (assume true (!claim P))) 
     (method (results) 
        (!cond results (method () 
                         (!solve [goal] (join results horn-clauses) special?))))))

(define (bc goal hyps)
  (!cond hyps
     (method ()
        (!do-props hyps (method (P) (assume true (!claim P)))
                        (method (results)
			  (!solve [goal] (join results horn-clauses) special?))))))

(define (bc-old goal hyps)
  (!cond hyps
     (method ()
        (!do-props hyps (method (P) (assume true (!claim P)))
                        (method (results)
			  (!solve [goal] (join results horn-clauses-old) special?))))))

(define (bc-new goal hyps)
  (!cond hyps
     (method ()
        (!do-props hyps (method (P) (assume true (!claim P)))
                        (method (results)
			  (!solve [goal] (join results horn-clauses) special?))))))

(define (pbc goal hyps)
  (!do-props hyps (method (P) (assume true (!claim P)))
                        (method (results)
			  (!solve [goal] (join results horn-clauses) special?))))





(define (pbc1 goal hyps hc)
  (!do-props hyps (method (P) (assume true (!claim P)))
                        (method (results)
			  (!solve [goal] (join results hc horn-clauses) special?))))

(forall* [?n ?x]
  (if (in (tup [?n ?x]) data) 
      (in (tup [?x]) (elms ?n))))


(define acyclicity
  (forall ?n 
    (not (in (tup [?n]) (sbdot (scalar ?n) (tc next))))))
  
(primitive-method (list-induction goal-prop)
  (let ((base (forall ?n (if (not (exists ?m (holds next [?n ?m])))
			     (goal-prop ?n))))
	(step (forall ?n
		(forall ?m
		  (if (holds next [?n ?m])
		      (if (goal-prop ?m)
			  (goal-prop ?n)))))))
   (check ((& (holds? base)
	      (holds? step)
	      (holds? acyclicity)) (forall ?n (goal-prop ?n))))))