;;;;;;;;;;;;;;;;;;
;; From repro-constraineq

;; repro-constraineq
(push)
(rule ((= x 1) (= y x) (= z y)) ())
(run 1)
(pop)

;; repro-constraineq2
(push)
(rule ((= x 1) (= y x)) ())
(run 1)
(pop)

;; repro-constraineq3
(push)
(relation f (i64))

(rule ((= x 1)
       (= x 2))
      ((f x)))
      
(run 1)
(print-function f 10)
(pop)

;;;;;;;;;;;;;;;;;;
;; Atoms need to be order-insensitive

;; Issue #196
(push)
(relation R (i64))

(rule 
  ((= x y)
   (= y 1)) 
  ((R x)))
(run 1)
(check (R 1))
(pop)

(push)
(relation R (i64))

(rule 
  ((= x (+ y 1))
   (= y 1)) 
  ((R x)))
(run 1)
(check (R 2))
(pop)

;; Issue #80
(push)
(datatype TYPE)
(datatype TERM)
(function type (TERM) TYPE)
(function Ob () TYPE)
(function Hom (TERM TERM) TYPE)

(function id (TERM) TERM)
(rule ((type (id A)))
      ((type A)))
(rewrite (type (id A)) 
         (Hom A A) 
    :when ((= (type A) (Ob))))

(function compose (TERM TERM) TERM)
(rule ((type (compose f g)))  
      ((type f) 
       (type g)))
(rewrite (type (compose f g)) 
         (Hom A C) 
    :when ((= (type f) (Hom A B)) 
           (= (type g) (Hom B C))))

(birewrite (compose (compose f g) h) 
           (compose f (compose g h)) 
    :when ((= (type A) (Ob)) 
           (= (type B) (Ob))
           (= (type C) (Ob))
           (= (type D) (Ob))
           (= (type f) (Hom A B))
           (= (type g) (Hom B C))
           (= (type h) (Hom C D))))
(birewrite (compose f (id B)) f 
    :when ((= (type A) (Ob)) 
           (= (type B) (Ob))
           (= (type f) (Hom A B))))
(birewrite (compose (id A) f) f 
    :when ((= (type A) (Ob)) 
           (= (type B) (Ob))
           (= (type f) (Hom A B))))

(function AConst () TERM)
(let A (AConst))
(function BConst () TERM)
(let B (BConst))
(function fConst () TERM)
(let f (fConst))
(function gConst () TERM)
(let g (gConst))
(let fog (compose g f))
(union (type f) (Hom A B))
(union (type g) (Hom B A))
(union (type A) (Ob))
(union (type B) (Ob))
(type fog)
(run 10)
(print-function type 10)
(check (= (type f) 
          (type (compose (id A) 
                         (compose f (id B))))))
(check (= (type fog)
          (Hom B B)))
(pop)


;;;;;;;;;;;;;;;;;;
;; Finding the right type in case of container types and primitives

;; Issue #113

(push)
(sort MyMap (Map i64 String))
(sort MyMap1 (Map i64 i64))

(let my_map1 (map-insert (map-empty) 1 "one"))
(pop)

(push)
(sort MyMap1 (Map i64 i64))
(sort MyMap (Map i64 String))

(let my_map1 (map-insert (map-empty) 1 "one"))
(pop)