;;HACK
(define-syntax-rule (define-module- name args ...)
  (cond-expand
   (guile-3
    (define-module name
      #:declarative? #f
      args ...))
   (guile
    (define-module name args ...))))


(use-modules (logic guile-log iso-prolog))
(use-modules (logic guile-log))
(use-modules (logic guile-log type))
(use-modules ((logic guile-log inheritance) #:select
              (compile-sup-sub print-theory *current-set-theory* reverse-lookup
			       order-the-set (lookup . get))))
(use-modules (logic guile-log guile-prolog attribute))
(use-modules (logic guile-log guile-prolog set))
(use-modules (logic guile-log guile-prolog wind))
(use-modules (logic guile-log vset))
(use-modules ((logic guile-log umatch) #:select (gp-pair?)))
(use-modules (logic guile-log guile-prolog coroutine))
(use-modules (logic guile-log guile-prolog set-theory))

(<define> (mktype x y) (mk-type (get (<lookup> x)) y))

(compile-prolog-string
"
%generates all subsets note X must be a attributed wraped var
f1(Z) :- mk({1,2,3},X),Z⊆X.    

%generate all disjoint decompositoins
f2(A,B) :- mk({1,2,3},X),(A⊔B)=X.  

%generate all unions decompositoins
f3(A,B) :- mk({1,2},X),(A∪B)=X.  

%generate all decompositions of subsets
f4(A,B) :- mk({1,2},X),(A⊔B)⊂X.
")

(define aT #f)
(define bT #f)
(define cT #f)
(define aS #f)
(define bS #f)
(define cS #f)

(<define> (revlookup a b)
 (<=> b ,(reverse-lookup (<lookup> a))))

(compile-prolog-string
"
   :- dynamic(class).

   tr(X,L) :-
      class(X,C),
      L = (X : C).

   e(X,L) :-
      texp(X,XX,true,LL),
      (
        LL=true ->
          L=XX ; 
        L = (LL,XX)
      ).

   texp(X,X,L,L) :- var(X),(\\+attvar(X)),!.
   texp(cls(X),U,L,LL) :- !,
     LL = (L,(class(X,C),U=(X : C))).
   texp(cls(X,C),U,L,LL) :- !,
     get_attr(C,'Type',[A|_]),
     revlookup(A,AA),
     AA ⊆ X,
     LL = (L,(U=(X : C))).
 
   texp([A|B],[AA|BB],L,LL) :- texp(A,AA,L,L1),texp(B,BB,L1,LL).
   texp(A(|B),AA(|BB),L,LL) :- texp(A,AA,L,L1),texp(B,BB,L1,LL).
   texp({A},{AA},L,LL) :- texp(A,AA,L,LL).
   texp(A,A,L,L).  

   

   mkclass(X,C) :-
     mktype(X,C),
     asserta(class(X,C)).

")


(compile-prolog-string
"
'init-theory' :-
    A is {\"a\"},
    B is {\"b\"},
    C is A∪B,
   
   sets_to_theory([A,B,C]),

   do[(set! aS (<lookup> A))],
   do[(set! bS (<lookup> B))],
   do[(set! cS (<lookup> C))].
")

(prolog-run 1 () (init-theory))

(compile-sup-sub)
(order-the-set)
(print-theory)

(compile-prolog-string
"
   tp :-
    mkclass(aS,AT),
    mkclass(bS,BT),
    mkclass(cS,CT),
    do[(set! aT (<lookup> AT))],
    do[(set! bT (<lookup> BT))],
    do[(set! cT (<lookup> CT))].
")

(prolog-run 1 () (tp))


(compile-prolog-string
"
   -generalized.
   ftheory(X : aT) :- write(a(X)),fail.
   ftheory(X : bT) :- write(b(X)),fail.
   ftheory(X : cT) :- write(c(X)),fail.

   t(X) :- e(X,XX),(XX -> write(true(X)) ; write(false(X))),nl.

   test :-
     nl,write(start),nl,nl,
     t(ftheory(cls(aS))),
     t(ftheory(cls(bS))),
     t(ftheory(cls(cS))),
     X is {a-2},t(ftheory(cls(X))),
     Y is {a-2,b-4},t(ftheory(cls(Y,aT))).

   test2 :-
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)),
     asserta(f(1)).
")

(prolog-run 1 () (test))