25:- use_module(library(lists)).   26
   27% settings
   28% set(refinethreadvar, vid).
   29%
   30
   31progol_engine(aleph).
   32
   33
   34:- multifile legitimate_literal/1.   35
   36set_def(refinethreadvar, refineop,
   37        'Description',
   38        templatevar, 'thread', 
   39        show). 
   40
   41set_def(refinelitgen, refineop,
   42        'Description',
   43        [modes, user], modes,
   44        show).
   45
   46lith(Head) :-
   47    progol_engine(Engine),
   48    lith(Engine, Head).
   49
   50litb(Lit) :-
   51    progol_engine(Engine),
   52    litb(Engine, Lit).
   53
   54
   55thread_type(Type) :-
   56    setting(refinethreadvar, Type).
   57
   58lith(aleph, Head) :-
   59    '$aleph_global'(modeh, modeh(_, Head)).
   60
   61litb(aleph, Lit) :- 
   62    '$aleph_global'(modeb, modeb(_, Lit)).
   63
   64refine(A, B) :-
   65    setting(construct_bottom, saturation) 
   66    ->  refine_bot(A, B) 
   67      ; refine_lazy(A, B).
   68
   69refine_lazy(nil, Clause) :-
   70   lith(HeadTemplate),
   71   functor(HeadTemplate, Name, Arity),
   72   functor(Head, Name, Arity),  
   73   Clause = (Head).
   74
   75refine_lazy((Head:-Body), (Head:-Body2)):- !,
   76   generate_lit(Lit),
   77   copy_term(Body, Body1),
   78   append_thread(Lit, Body1, Body2),
   79   connect_thread((Head:-Body2)).
   80
   81refine_lazy(Head, Clause) :- !,
   82   refine_lazy((Head:-true), Clause).
   83
   84
   85generate_lit(Lit) :-
   86   setting(refinelitgen, user)
   87   -> legitimate_literal(Lit)
   88   ; generate_lit_modes(Lit). 
   89
   90generate_lit_modes(Lit) :-
   91   find_mode(modeb, Name/Arity, Mode),
   92   functor(Lit, Name, Arity),
   93   split_args(Lit, Mode, _Inputs, _Outputs, Constants),
   94   generate_constants(Lit, Constants).
   95
   96generate_constants(Lit, []).
   97generate_constants(Lit, [Type/Place|Z]) :-
   98   arg(Lit, Place, ConArg),
   99   call(Type,ConArg),
  100   generate_constants(Lit, Z).
  101
  102
  103subset([], []).
  104subset([X|L], [X|S]) :- subset(L, S).
  105subset(L, [_|S]) :- subset(L, S).
  106
  107unordered_subset(Set, SubSet):-
  108  length(Set, LSet),
  109  between(0,LSet, LSubSet),
  110  length(NSubSet, LSubSet),
  111%  permutation(SubSet, NSubSet),
  112%  SubSet = NSubSet,
  113  subset(NSubSet,Set),
  114  permutation(NSubSet, SubSet).
  115
  116refine_bot(nil, Clause) :-
  117    bottom(BottomClause),
  118    BottomClause = (Head:-Body),
  119    has_pieces(Body, BottomClauseList),
  120    unordered_subset(BottomClauseList, SelectedLits),
  121    has_pieces(Body2, SelectedLits),
  122    Clause = (Head :- Body2),
  123    connect_thread(Clause).
  124
  125
  126% arg places
  127argp(Term, InputPlaces, OutputPlaces) :- 
  128    split_args(Term, _Mode, Inputs, Outputs, _Constants),
  129    thread_type(Type),
  130    member(InputPlaces/Type, Inputs),
  131    member(OutputPlaces/Type, Outputs).
  132
  133inout_lit(Term, Input, Output) :-
  134    functor(Term, _, Arity),
  135    once(argp(Term, [InArg], [OutArg])),
  136    arg(InArg,  Term, Input),
  137    arg(OutArg, Term, Output).
  138
  139inout_thread(','(A, B), Input, Output) :-
  140    inout_lit(A, Input, FirstOut),
  141    inout_thread(B, FirstOut, Output), !.
  142
  143inout_thread(Atom, Input, Output) :- inout_lit(Atom, Input, Output), !.
  144
  145% has_pieces(+Body, -AtomList).
  146% returns the body as a list of atoms
  147has_pieces(','(A, R), [A|Z]) :- Z \== [], has_pieces(R, Z), !.
  148has_pieces(A, [A]) :- A \== true, !.
  149has_pieces(true, []) :- !.
  150
  151% concat_thread(+List, -Body)
  152% concat_thread: concat a list of literals as a thread.
  153concat_thread([A], A) :- !.
  154concat_thread([A|Z], ','(A, Z1)) :- 
  155    concat_thread(Z, Z1),
  156    inout_lit(A, _, Out),
  157    inout_thread(Z1, Out, _).
  158
  159% count_literals(+Literals, -Count)
  160count_literals(Lits, Count) :-
  161    has_pieces(Lits, LitList), 
  162    length(LitList, Count).
  163
  164% connect_thread(+Clause)
  165% connect_thread: Connect the head variables with the body variables.
  166connect_thread((Head:-Body)) :-
  167    inout_lit(Head, Input, Output),
  168    inout_thread(Body, Input, Output), !.
  169
  170% append_thread(+Literal, +Body, -BodyWithLit)
  171% append and connect the Literal to the Body resulting to BodyWithLit.
  172append_thread(Lit, Body, BodyWith) :-
  173    has_pieces(Body, Atoms),
  174    append(Atoms, [Lit], Atoms2),
  175    concat_thread(Atoms2, BodyWith), !