1:- module(formulae,
    2	[ list_to_conj/3,
    3	  list_to_conj/2,
    4	  conj_to_list/2,
    5	  list_to_disj/2,
    6	  disj_to_list/2,
    7	  conj_to_llist/2,
    8	  llist_to_conj/2,
    9	  disj_to_llist/2,
   10	  llist_to_disj/2,
   11	  %
   12	  body2list/2,
   13	  asbody_to_conj/2
   14	]).   15
   16list_to_conj([X|More],(X,Next),End):-
   17        list_to_conj(More,Next,End).
   18list_to_conj([],End,End).
   19
   20list_to_conj([], true) :- !.
   21list_to_conj([A|B], (A,Br)) :- B \== [], !,
   22	list_to_conj_(B, Br).
   23list_to_conj([A], A) :- !.
   24list_to_conj(A, _) :-
   25	throw(error(domain_error(list, A), list_to_conj/2)).
   26
   27list_to_conj_(B, Br) :- var(B), var(Br), !,
   28	[Br] = B.
   29list_to_conj_(B, Br) :-
   30	list_to_conj(B, Br).
   31
   32conj_to_list(A, B) :- list_to_conj(B, A). % TODO: recover faster impl
   33
   34list_to_disj([], false) :- !.
   35list_to_disj([A|B], (A;Br)) :- B \== [], !,
   36	list_to_disj_(B, Br).
   37list_to_disj([A], A) :- !.
   38list_to_disj(A, _) :-
   39	throw(error(domain_error(list, A), list_to_disj/2)).
   40
   41list_to_disj_(B, Br) :- var(B), var(Br), !,
   42	[Br] = B.
   43list_to_disj_(B, Br) :-
   44	list_to_disj(B, Br).
   45
   46list_to_disj2([],false):- !.
   47list_to_disj2([X],X):- !.
   48list_to_disj2([X|Xs],(X;Ys)):-
   49	list_to_disj2(Xs,Ys).
   50
   51disj_to_list(D, L) :-
   52	list_to_disj(L, D). % TODO: recover efficient impl
   53
   54conj_to_llist(D,L):-
   55	conj_to_llist_diff(D,L,[]).
   56
   57conj_to_llist_diff((A,B),LL,LT):- !,
   58	conj_to_llist_diff(A,LL,LA),
   59	conj_to_llist_diff(B,LA,LT).
   60conj_to_llist_diff((A;B),[LL|LT],LT):- !,
   61	disj_to_llist_diff(A,LL,LA),
   62	disj_to_llist_diff(B,LA,[]).
   63conj_to_llist_diff(A,[A|LT],LT).
   64
   65llist_to_conj([LL],C):- !,
   66	llist_to_disj(LL,C).
   67llist_to_conj([LL|LLs],(C,Cs)):- !,
   68	llist_to_disj(LL,C),
   69	llist_to_conj(LLs,Cs).
   70llist_to_conj(C,C).
   71
   72disj_to_llist(D,L):-
   73	disj_to_llist_diff(D,L,[]).
   74
   75disj_to_llist_diff((A;B),LL,LT):- !,
   76	disj_to_llist_diff(A,LL,LA),
   77	disj_to_llist_diff(B,LA,LT).
   78disj_to_llist_diff((A,B),[LL|LT],LT):- !,
   79	conj_to_llist_diff(A,LL,LA),
   80	conj_to_llist_diff(B,LA,[]).
   81disj_to_llist_diff(A,[A|LT],LT).
   82
   83llist_to_disj([LL],D):- !,
   84	llist_to_conj(LL,D).
   85llist_to_disj([LL|LLs],(D;Ds)):- !,
   86	llist_to_conj(LL,D),
   87	llist_to_disj(LLs,Ds).
   88llist_to_disj(D,D).
   89
   90asbody_to_conj(A, B) :- var(A), !,
   91	( var(B) ->
   92	    A = B
   93	; conj_to_list_of_list(B, A, [])
   94	).
   95asbody_to_conj(A, B) :-
   96	list_of_list_to_conj(A, B).
   97
   98list_of_list_to_conj([(A;B)|C], Out) :- !,
   99	list_to_conj(A, AC),
  100	list_of_list_to_conj([B], BC),
  101	list_of_list_to_conj(C, CC),
  102	( CC == true ->
  103	    Out = (AC;BC)
  104	; Out = ((AC;BC),CC)
  105	).
  106list_of_list_to_conj([A|B], (AC,BC)) :- B \== [], !,
  107	list_of_list_to_conj(A, AC),
  108	list_of_list_to_conj(B, BC).
  109list_of_list_to_conj([AL], A) :-
  110	list_of_list_to_conj(AL, A),
  111	!.
  112list_of_list_to_conj(AL, A) :-
  113	is_list(AL), % TODO: calling a prop, instantiation?
  114	!,
  115	list_to_conj(AL, A).
  116list_of_list_to_conj(A, A).
  117
  118conj_to_list_of_list((A,B), Ac, TAc) :- !,
  119	conj_to_list_of_list(A, Ac, T),
  120	conj_to_list_of_list(B, T, TAc).
  121conj_to_list_of_list((A;B), [(AC;BC)|T], T) :- !,
  122	conj_to_list__(A, AC),
  123	conj_to_list__(B, BC).
  124conj_to_list_of_list(true, T, T) :- !.
  125conj_to_list_of_list(A, [A|T], T).
  126
  127conj_to_list__((A,B), [A|Bs]) :- !,
  128	conj_to_list(B, Bs).
  129conj_to_list__((A;B), (As;Bs)) :- !,
  130	conj_to_list(A, As),
  131	conj_to_list__(B, Bs).
  132conj_to_list__(A, [A]).
  133
  134body2list((First,Rest), [NewFirst|More]) :- !,
  135	p_exp2list(First, NewFirst),
  136        body2list(Rest, More).
  137body2list(Last, [NewLast]) :-
  138	p_exp2list(Last, NewLast).
  139
  140p_exp2list('&'(G,Goals), [G|More]) :- !,
  141	p_exp2list__(Goals, More).
  142p_exp2list(Goal, Goal).
  143
  144p_exp2list__('&'(G,Goals), [G|More]) :-
  145	p_exp2list__(Goals, More).
  146p_exp2list__(Goal, [Goal])