disjunctions

parent cc843fe9
......@@ -48,50 +48,7 @@ compile_goaler(X,Tail,V,LX,PP0) :-
get_P(V,P1),
combine_pp(P1,PP0,PP1),
set_P(V,PP1).
compile_disjunction0
([X],First,Aq,Ae,Out,Lab,A,Tail,S0,[U],B2,V,[L,LL],P0,PP0,Q,QQ) :- !,
set_P(V,P0),
(First=#t -> compile_goaler(X,Tail,V,[L,LL],PP0) ;
catch((
Q=Qit,
get_CES(V,[C|_],E,S),
set_AB2ES(V,Aq,B2,0,S0),
(
((nonvar(X),X=(G1->G2)) -> XX=(once(G1),G2) ; XX=X),
compile_goaler(XX,Tail,V,[LX,LL],PP0),
get_ACES(V,Aq1,[C1|_],E1,S1),
(C == C1 -> true ; throw(bug_c_state_error)),
(
eql_a(Ae,Aq1) -> true ;
throw(all_disjuction_goals_needs_the_same_begin_level)
),
SS is max(S,S1),
EE is E \\/ E1,
set_AES(V,Aq,EE,SS),
U = [E1,_],
head_at_true(Qit,First,#t,A,C,Lab,Lab2,L,LX)
)),Er,
(
tfc(Er),
(
Er == #t ->
(
First==#t ->
throw(#t) ;
(
head_at_true(Qit,#f,#t,A,C,Lab,Lab2,L,LL),
U=[0,_]
)
);
(
Er == c ->
throw(c) ;
throw(#f)
)
)
))).
combine_pp(P1,PP0,PP1) :-
var(PP0) ->
......@@ -120,18 +77,20 @@ combine_pp(P1,PP0,PP1) :-
);
PP1 = \"complex\".
goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,B2,LLX,P0,PP0,Q,QQ) :-
-trace.
goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,B2,LLX,P0,PP0,Q,QQ)
:-
Q=Qit,
get_CES(V,[C|_],E,S),
set_AB2ES(V,Aq,B2,0,S0),
((nonvar(X),X=(G1->G2)) ->
XX=(call(G1),softie(A),collect_F(FF),G2) ;
(QQ=#t,XX=(X,newtag_F(FF)))),
(W=#t,XX=(call(G1),softie(A),collect_F(FF),G2)) ;
(W=#f,,XX=(X,newtag_F(FF)))),
set_P(V,ground(Lab)),
push_Q(V,Q),
push_Q(3,V,Q),
compile_goal(XX,Tail,V,[LX,LG]),
pop_Q(V,Q),
(W=#t -> popl_Q(V,Q,_) ; popl_Q(V,Q,QQ)),
get_P(V,P1),
combine_pp(P1,PP0,PP1),
(var(FF) -> true ; set_F(V,FF)),
......@@ -171,6 +130,50 @@ goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,B2,LLX,P0,PP0,Q,QQ) :-
),
head_at_true(Qit,First,#f,A,C,Lab,Lab2,L,LX)
).
-trace.
compile_disjunction0
([X],First,Aq,Ae,Out,Lab,A,Tail,S0,[U],B2,V,[L,LL],P0,PP0,Q,QQ) :- !,
set_P(V,P0),
(First=#t -> compile_goaler(X,Tail,V,[L,LL],PP0) ;
catch((
Q=Qit,
get_CES(V,[C|_],E,S),
set_AB2ES(V,Aq,B2,0,S0),
(
((nonvar(X),X=(G1->G2)) -> XX=(once(G1),G2) ; XX=X),
compile_goaler(XX,Tail,V,[LX,LL],PP0),
get_ACES(V,Aq1,[C1|_],E1,S1),
(C == C1 -> true ; throw(bug_c_state_error)),
(
eql_a(Ae,Aq1) -> true ;
throw(all_disjuction_goals_needs_the_same_begin_level)
),
SS is max(S,S1),
EE is E \\/ E1,
set_AES(V,Aq,EE,SS),
U = [E1,_],
head_at_true(Qit,First,#t,A,C,Lab,Lab2,L,LX)
)),Er,
(
tfc(Er),
(
Er == #t ->
(
First==#t ->
throw(#t) ;
(
head_at_true(Qit,#f,#t,A,C,Lab,Lab2,L,LL),
U=[0,_]
)
);
(
Er == c ->
throw(c) ;
throw(#f)
)
)
))).
compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,B2,V,[L,LL],P0,PP0,Q,QQ) :- !,
tr('goto-inst',Goto),
......@@ -214,6 +217,7 @@ compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,B2,V,[L,LL],P0,PP0,Q
)
)).
-trace.
compile_disjunction(Y,First,Aq,Ae,Out,Lab,A,Tail,S0,U,B2,V,[L,LL],Q,QQ) :-
get_P(V,P0),
catch(compile_disjunction0(Y,First,Aq,Ae,Out,Lab,A,Tail,S0,U,B2,V,[L,LL],P0,PP0,Q,QQ),Er,
......
......@@ -228,8 +228,9 @@ compile_goal(';'(|X),Tail,V,[L,LL]) :- !,
(
get_AB2ESM(V,Aq,B2,E,S,M),
get_F(V,F),
compile_disjunction(XX,#t,Aq,Ae,Out,Lab,LabA,Tail,S,U,B2,V,LM,Q),!,
compile_disjunction(XX,#t,Aq,Ae,Out,Lab,LabA,Tail,S,U,B2,V,LM,Q,QQ),!,
(zero(V) -> Tp is 0 ; Tp is 1),
pushl_Q(V,QQ),
(
var(Q) ->
(
......
......@@ -23,12 +23,45 @@
(let ((v (<lookup> v)))
(<set> (vector-ref v nq) (cons u (<lookup> (vector-ref v nq))))))
(<define> (pushl_Q v qq)
(let* ((v (<lookup> v))
(u (<lookup> (vector-ref v nq))))
(let lp ((qq (<lookup> qq)) (r '()))
(if (pair? qq)
(lp (<lookup> (cdr qq)) (cons (car qq) r))
(<set> (vector-ref v nq)
((@ (guile) append) u r))))))
(<define> (pop_Q e v x)
;(<pp> `(pop ,e))
(let ((v (<lookup> v)))
(<=> x ,(car (<lookup> (vector-ref v nq))))
(<set> (vector-ref v nq) (cdr (<lookup> (vector-ref v nq))))))
(<define> (get_Q v x)
(let ((v (<lookup> v)))
(<=> x ,(<lookup> (vector-ref v nq)))))
(<define> (popl_Q v x xx)
(let ((v (<lookup> v)))
(let lp ((l (<lookup> (vector-ref v nq))) (r '()))
(if (pair? l)
(let ((y (car l)))
(if (eq? y x)
(<and>
(<set> (vector-ref v nq) (cdr l))
(let lp ((xx (<lookup> xx)))
(if (<var?> xx)
(let lp ((xx xx) (r (cons y r)))
(if (pair? r)
(<var> (xxx)
(<=> xx ,(cons (car r) xxx))
(lp xxx (cdr r)))
<cc>))
(lp (cdr xx)))))
(lp (cdr l) (cons y r))))
<cc>))))
(<define> (touch_Q e v)
;(<pp> `(touch ,e))
(<recur> lp ((l (<lookup> (vector-ref (<lookup> v) nq))))
......@@ -477,11 +510,11 @@ listp(X) :- var(X) -> (!, fail).
listp([X|Y]) :- listp(Y).
listp([]).
tail(Tail,V,LL,LLL) :-
tail(Tail,V,LL,LLL) :-
get_P(V,P),
(
Tail = #t ->
(tr(cc,CC),LL=[[CC,P]|LLL]) ;
(touch_Q(tail,V),tr(cc,CC),LL=[[CC,P]|LLL]) ;
LLL=LL
).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment