    1:- module(pha_mi, [mi/3]).

PHA meta-interpreter

    6:- use_module(library(typedef)).    7
    8:- type goal  == term.
    9:- type rv(_) == term.
   10:- type prob == float.
   11
   12:- type pair(A,B)   ---> A-B.
   13:- type weighted(A) ---> prob:A.
   14:- type assumption  ---> rv(A) := A.
   15:- type cont        ---> ans(term) ; [goal|cont].
   16:- type susreq      ---> susreq(assumption, cont, prob).  % suspend on probabilistic choice
   17:- type request     ---> sus(list(susreq)) % result of meta-interpretation is suspension
   18                       ; ret(goal).        % result of meta-interpreteation is a proven goal.
   19
   20:- multifile pha_user:rule/3, pha_user:rv/2.

mi(+C:cont, +AS:list(assumption), -R:request) is det: Runs the given continuation until either an answer is generated or all threads of execution have become suspended on sampling decisions. Essentially, this interpreter runs one intial thread as far as it can without making any new assumptions, either reaching its goal or returning a weighted set of new threads, each predicated on a new assumption.

   28mi(Cont, AS, R) :- mi(Cont, [], AS, [], R).

mi(+C:cont, +T1:list(cont), +AS:list(assumption), +TS:list(susreq), -R:request) is det

   31mi(ans(G),_,_,_,ret(G)). 
   32mi([H|G1],T1,AS,TS,R) :- mi1(H,G1,T1,AS,TS,R) -> true; mi2(T1,AS,TS,R).

mi1(+G:goal, +G1:cont, +T1:list(cont), +AS:list(assumption), +TS:list(susreq), -R:request) is semidet: "defaulty" goal interpreter, built in preds in rule/3.

   36mi1(N:=V, G1,T1,AS,TS1,R) :- !,
   37   (  member(N:=V1,AS) % an assumption has alreadby been made about rv N
   38   -> V=V1,            % this can fail if values don't match
   39      mi(G1,T1,AS,TS1,R)    % carry on with remaining goals
   40   ;  rv(N,Dist),      % get suspension requests for each possible value of N...
   41      findall(susreq(N:=V,G1,P), member(P:V,Dist),TS2,TS1), % ... and stack them on TS1
   42      mi2(T1,AS,TS2,R) % continue with remaining active threads
   43   ).
   44mi1(G,G1,T1,AS,TS,R) :-
   45   % prepend list of continuations for this choice point and continue
   46   findall(G2,rule(G,G2,G1),T2,T1), % create new threads based on expansions of G
   47   mi2(T2,AS,TS,R).

mi2(+Alts:list(cont), +AS:list(assumption), +TS:list(susreq), -R:request) is det

   50mi2([],_,Threads,sus(Threads)). % no active continuations, so return suspended continuations 
   51mi2([T|T1],AS,TS,R) :- mi(T,T1,AS,TS,R). % interpret first continuation
   52
   53rule(X=X,GS,GS).
   54rule(X\=Y,GS,GS) :- X\=Y.
   55rule(X is Y,GS,GS) :- X is Y.
   56rule(or(GA,GB,G2),G1,G2) :- G1=GA; G1=GB.
   57rule(H,G1,G2) :- pha_user:rule(H,G1,G2).
   58rv(N,V) :- pha_user:rv(N,V)