bugfix and added vm-unify2

parent 377241d8
......@@ -132,6 +132,7 @@ PSSOURCES = \
logic/guile-log/guile-prolog/vm/vm-args2.scm \
logic/guile-log/guile-prolog/vm/vm-disj2.scm \
logic/guile-log/guile-prolog/vm/vm-imprint2.scm \
logic/guile-log/guile-prolog/vm/vm-unify2.scm \
logic/guile-log/examples/kanren/type-inference.scm \
logic/guile-log/imatch.scm \
prolog-user.scm \
......
......@@ -119,7 +119,7 @@ get_post(S,C,Cplx,Tail,X,XX) :-
caller(cc,Args,label(G,N),V,[L,LL]) :- !,
touch_Q(V),
touch_Q(1,V),
narg(Args,0,MM),
M is MM + 3,
(M==N -> true ; throw(cc_does_not_match_caller)),
......@@ -134,7 +134,7 @@ caller(cc,Args,label(G,N),V,[L,LL]) :- !,
LL2 = [[Goto,G]|LL].
caller(cc,Args,Tail,V,[L,LL]) :- !,
touch_Q(V),
touch_Q(2,V),
(Tail=#f -> throw(cc_not_in_tail_context) ; true),
tr('clear-sp' , Clear),
L=[[Clear]|L2],
......@@ -147,10 +147,10 @@ caller(cc,Args,Tail,V,[L,LL]) :- !,
set_FS(V,F,S),
tr('tail-cc', Call),
LL2 = [[Call]|LW].
*/
*/
caller(F,Args,Tail,V,[L,LL]) :-
touch_Q(V),
touch_Q(3,V),
(get_recur(F,A,N) -> rec(F,A,N,Args,Tail,V,[L,LL]) ;
(
tr('clear-sp' , Clear),
......
......@@ -11,7 +11,7 @@
#:use-module (logic guile-log guile-prolog vm-compiler)
#:export (caller push_args_args2 push_args_args push_args))
#;
(eval-when (compile)
(pk (prolog-run-rewind 1 (x)
(dyntrace (@@ (logic guile-log guile-prolog vm vm-handle)
......
......@@ -57,25 +57,28 @@ compile_conj0([!|Gs],Tail,V,[L,LL]) :- !,
)).
compile_conj0([softie(A)|Gs],Tail,V,[L,LL]) :- !,
pop_Q(V,Q),
pop_Q(3,V,Q),
ifc(compile_conj0(Gs,Tail,V,[L1,LL]),E,
(
tfc(E),
(
E==#t ->
(Tail==#t -> L=[[softie,A],[cc]|LL] ; L=[[softie,A]|LL]);
(
push_Q(3,V,Q),
(
Tail==#t ->
L=[[softie,A],[cc]|LL] ;
L=[[softie,A]|LL]
)
);
E==c ->
throw(c);
throw(softie(A))
)
),
(
(
var(Q) ->
L=[['softie-light',A]|L1];
L=[[softie,A]|L1]
),
push_Q(V,Q)
L=[[softie,A]|L1],
push_Q(3.2,V,Q)
)).
compile_conj0([(fail;false)|Gs],Tail,V,[L,LL]) :- !,
......
......@@ -47,8 +47,8 @@ compile_disjunction0
([X],First,Aq,Ae,Out,Lab,A,Tail,S0,[U],V,[L,LL]) :- !,
(First=#t -> compile_goal(X,First,V,[L,LL]) ;
catch((
read_Q(V,Qit),
pop_Q(V,_),
read_Q(0,V,Qit),
pop_Q(0,V,_),
get_CES(V,[C|_],E,S),
set_AES(V,Aq,0,S0),
(
......@@ -87,7 +87,7 @@ compile_disjunction0
))).
goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :-
read_Q(V,Qit),
read_Q(1,V,Qit),
get_CES(V,[C|_],E,S),
set_AES(V,Aq,0,S0),
((nonvar(X),X=(G1->G2)) ->
......@@ -119,7 +119,7 @@ goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :-
Err==#t ->
throw(bug_true_not_be_send_in_non_first_disjunction);
(
pop_Q(V,_),
pop_Q(1,V,_),
head_at_true(Qit,First,#f,A,C,Lab,Lab2,L,LX),
UU=[[0,_]],
Err==c ->
......@@ -133,7 +133,7 @@ goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :-
compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !,
tr('goto-inst',Goto),
read_Q(V,Qit),
read_Q(2,V,Qit),
(Tail==#t -> LG=LLX ; LG = [[Goto,Out]|LLX]),
catch(goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,U,V,L,LL,LG,LLX), Er,
(
......
......@@ -31,6 +31,9 @@ reverse_op(=\\=,=\\=).
zero(V) :- get_A(V,A),A=[[0|_]].
print([]).
print([X|L]) :- write(X),nl,print(L).
wrap(Code,[L,LL]) :-
catch(Code,E,
(
......@@ -59,11 +62,11 @@ compile_goal(Code,Iout,StackSize,Narg,Constants,Pretty) :- !,
b_setval(pretty,#t),
make_state(0,[[0,_,_]],[0],0,0,0,0,[HC,HV],[],V),
wrap(compile_goal(Code,#t,V,[L,[]]),[L,[]]),!,
%write(L),nl,!,
%print(L),nl,!,
get_M(V,StackSize),
handle_all(L,LL),
(var(Constants)->Constants=scm[(get-consts)];true),
%write(LL),nl,!,
%print(LL),nl,!,
(Pretty==#t -> Iout=LL ; (b_setval(pretty,#f),mmtr(LL,Iout))).
compile_goal(X,Tail,V,L) :- var_p(X),!,
......@@ -180,7 +183,7 @@ compile_goal(Op(\"recur\",Args),Tail,V,[L,LL]) :-
add_recur(F,A,N),
push_args_args(#f,Xin,V,L,L1,_,_),
touch_A(V),
touch_Q(V),
touch_Q(10,V),
%set_F(V,scm[(gensym \"Rec\")]),
L1=[[label,A]|L2],
compile_goal((begin_att,Impr,end_att),Tail,V,[L2,LL]).
......@@ -203,7 +206,7 @@ compile_goal(';'(|X),Tail,V,[L,LL]) :- !,
get_AESM(V,Aq,E,S,M),
get_F(V,F),
label(Lab),label(Out),
push_Q(V,Q),
push_Q(0,V,Q),
compile_disjunction(XX,#t,Aq,Ae,Out,Lab,LabA,Tail,S,U,V,LM),!,
(zero(V) -> Tp is 0 ; Tp is 1),
(
......@@ -211,11 +214,11 @@ compile_goal(';'(|X),Tail,V,[L,LL]) :- !,
(
var_p(Var),
add_var_f(Var,V,F,LabA),
L = [['newframe-light',LabA,Lab] | LX]
L = [['newframe-light',LabA,Lab] | LX]
);
(
Lab=LabA,
L = [[newframe ,LabA,Tp] | LX]
Lab = LabA,
L = [[newframe ,LabA,Tp] | LX]
)
),
LM = [LX, [[label,Out] | LL]],
......@@ -275,7 +278,7 @@ compile_goal((X =.. Y),Tail,V, L, LL) :- !,
compile_goal(set(V,X),Tail,V,[L,LL]) :- !,
touch_Q(V),
touch_Q(11,V),
tr(set,Set),
(var_p(X) -> true ; throw(no_var_in_set)),
add_var(X,V,Tag),
......@@ -411,7 +414,7 @@ compile_goal(iss(X,Y),Tail,V,[L,LL]) :- !,
var_p(X) ->
(
add_var(X,V,Tag),
(isFirst(Tag) -> true ; touch_Q(V)),
(isFirst(Tag) -> true ; touch_Q(12,V)),
push_v(-1,V),
tr(unify,Unify),
LX=[[unify,Tag,#t]|LLL]
......@@ -429,7 +432,7 @@ compile_goal(iss(X,Y),Tail,V,[L,LL]) :- !,
compile_goal(unify_with_occurs_check(X,Y),Tail,V,L) :- !,
touch_Q(V),
touch_Q(13,V),
(
X==Y -> throw(#t) ;
zero(V) ->
......@@ -444,7 +447,7 @@ compile_goal(uni_0(X,Y),Tail,V,[L,LL]) :- !,
compile_goal(X = Y,Tail,V,L) :- !,
touch_Q(V),
touch_Q(14,V),
(
X==Y -> throw(#t) ;
zero(V) ->
......
......@@ -94,10 +94,17 @@ chech_push(F) :-
throw(first_variable_in_scheme_context);
true.
handle(['softie-light',[[S,V,Q],N,F|_]],I,II,L,LL) :-
new_var(V,Q,S),
V=[VC|_],
L=[['softie-light',VC]|LL],
handle([softie,A],I,II,L,LL) :- !,write(A),nl,
(
(var(A) ; number(A)) ->
L=[[softie,A]|LL] ;
(
A=[[S,V,Q],N,F|_],
new_var(V,Q,S),
V=[VC|_],
L=[['softie-light',VC]|LL]
)
),
II is I + 2.
handle(['newframe-light',[[S,V,Q],N,F|_],A],I,II,L,LL) :-
......@@ -118,16 +125,16 @@ handle(['unwind-light',[[S,V,Q],N,F|_],B],I,II,L,LL) :-
L=[['unwind-light',B]|LL],
II is I + 2.
handle((X,[('goto-inst';'store-state' ;'unwind-tail';softie;
handle((X,[('goto-inst';'store-state' ;'unwind-tail';
'post-q' ;'newframe-light'),N]),
I,II,L,LL) :- !,
II is I + 2,
L=[X|LL].
handle((X,[(newframe;'newframe-negation';'post-negation'
;'unwind' ;'unwind-negation'
;'post-s'),A,B]),
handle((X,[(newframe ; 'newframe-negation' ; 'post-negation'
; 'unwind' ; 'unwind-negation'
; 'post-s'),A,B]),
I,II,L,LL) :- !,
II is I + 3,
L=[X|LL].
......
(compile-prolog-string "
compile_unify(X,Y,V,[L,LL],M) :-
X==Y -> (!,throw(#t));
var_p(X) ->
(
!,
(
constant(Y) ->
(
tr('unify-constant-2',Unify),
regconst(Y,YY),
add_var(X,V,Tag1),
(isFirst(Tag1) -> true ; touch_A(V)),
L = [[Unify,Tag1,YY,M]|LL]
);
instruction(Y) ->
(
tr('unify-instruction-2',Unify),
add_var(X,V,Tag1),
(isFirst(Tag1) -> true ; touch_A(V)),
L = [[Unify,Tag1,Y,M]|LL]
);
var_p(Y) ->
(
get_H(V,H),
tr('unify-2',Unify),
add_var(X,V,Tag1),
add_var(Y,V,Tag2),
((isFirst(Tag1) ; isFirst(Tag2)) -> true ; touch_A(V)),
((isFirst(Tag1),isFirst(Tag2),M=#f) -> throw(#f) ; true),
L = [[Unify,Tag1,Tag2,M]|LL]
);
(
tr('push-variable',Push),
L=[[Push,Tag1]|L1],
add_var(X,V,Tag1),
(isFirst(Tag1) -> true ; touch_A(V)),
push_v(1,V),
compile_imprint(Y,V,L1,LL,M)
)
)
) ;
var_p(Y) -> (!,compile_unify(Y,X,V,[L,LL],M)).
compile_unify([X|LX],[Y|LY],V,L,M) :- !,
link_l(L,L1,L2),
catch(compile_unify(X,Y,V,L1,M),E,
(
tt(E),L1=[Q,Q]
)),
compile_unify(LX,LY,V,L2,M).
compile_unify(X(|LX),Y(|LY),V,L,M) :- !,
link_l(L,L1,L2),
catch(compile_unify(X,Y,V,L1,M),E,
(
tt(E),L1=[Q,Q]
)),
compile_unify(LX,LY,V,L2,M).
compile_unify({X},{Y},V,L,M) :- !,
compile_unify(X,Y,V,L,M).
compile_unify(X,Y,V,[[[False]|LL],LL],M) :-
throw(#f).
")
......@@ -11,71 +11,4 @@
#:use-module (logic guile-log guile-prolog vm vm-imprint)
#:export (compile_unify))
(compile-prolog-string "
compile_unify(X,Y,V,[L,LL],M) :-
X==Y -> (!,throw(#t));
var_p(X) ->
(
!,
(
constant(Y) ->
(
tr('unify-constant-2',Unify),
regconst(Y,YY),
add_var(X,V,Tag1),
(isFirst(Tag1) -> true ; touch_A(V)),
L = [[Unify,Tag1,YY,M]|LL]
);
instruction(Y) ->
(
tr('unify-instruction-2',Unify),
add_var(X,V,Tag1),
(isFirst(Tag1) -> true ; touch_A(V)),
L = [[Unify,Tag1,Y,M]|LL]
);
var_p(Y) ->
(
get_H(V,H),
tr('unify-2',Unify),
add_var(X,V,Tag1),
add_var(Y,V,Tag2),
((isFirst(Tag1) ; isFirst(Tag2)) -> true ; touch_A(V)),
((isFirst(Tag1),isFirst(Tag2),M=#f) -> throw(#f) ; true),
L = [[Unify,Tag1,Tag2,M]|LL]
);
(
tr('push-variable',Push),
L=[[Push,Tag1]|L1],
add_var(X,V,Tag1),
(isFirst(Tag1) -> true ; touch_A(V)),
push_v(1,V),
compile_imprint(Y,V,L1,LL,M)
)
)
) ;
var_p(Y) -> (!,compile_unify(Y,X,V,[L,LL],M)).
compile_unify([X|LX],[Y|LY],V,L,M) :- !,
link_l(L,L1,L2),
catch(compile_unify(X,Y,V,L1,M),E,
(
tt(E),L1=[Q,Q]
)),
compile_unify(LX,LY,V,L2,M).
compile_unify(X(|LX),Y(|LY),V,L,M) :- !,
link_l(L,L1,L2),
catch(compile_unify(X,Y,V,L1,M),E,
(
tt(E),L1=[Q,Q]
)),
compile_unify(LX,LY,V,L2,M).
compile_unify({X},{Y},V,L,M) :- !,
compile_unify(X,Y,V,L,M).
compile_unify(X,Y,V,[[[False]|LL],LL],M) :-
throw(#f).
")
(include-from-path "logic/guile-log/guile-prolog/vm/vm-unify-model.scm")
(define-module (logic guile-log guile-prolog vm vm-unify2)
#:use-module (logic guile-log)
#:use-module (logic guile-log iso-prolog)
#:use-module (logic guile-log guile-prolog hash)
#:use-module (logic guile-log guile-prolog ops)
#:use-module (logic guile-log prolog swi)
#:use-module (compat racket misc)
#:use-module (system vm assembler)
#:use-module (logic guile-log guile-prolog vm-compiler)
#:use-module (logic guile-log guile-prolog vm vm-pre)
#:use-module (logic guile-log guile-prolog vm vm-var)
#:use-module (logic guile-log guile-prolog vm vm-imprint2)
#:export (compile_unify))
#;
(eval-when (compile)
(pk (prolog-run-rewind 1 (x)
(dyntrace (@@ (logic guile-log guile-prolog vm vm-handle)
handle)))))
(compile-prolog-string
"
- eval_when(compile).
the_tr2(X,[X]).
:- add_term_expansion_temp(the_tr2).
")
(eval-when (compile)
(set! (@@ (logic guile-log prolog compile) include-meta) #f))
(include-from-path "logic/guile-log/guile-prolog/vm/vm-unify-model.scm")
(eval-when (compile)
(set! (@@ (logic guile-log prolog compile) include-meta) #t))
......@@ -27,23 +27,29 @@
(define nh 7)
(define nq 8)
(<define> (push_Q v u)
(<define> (push_Q e v u)
;(<pp> `(push ,e))
(let ((v (<lookup> v)))
(<set> (vector-ref v nq) (cons u (<lookup> (vector-ref v nq))))))
(<define> (pop_Q v x)
(<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> (touch_Q v)
(let ((l (<lookup> (vector-ref (<lookup> v) nq))))
(if (pair? l)
(<define> (touch_Q e v)
;(<pp> `(touch ,e))
(<recur> lp ((l (<lookup> (vector-ref (<lookup> v) nq))))
(if (pair? l)
(<and>
(<=> #t ,(car l))
<cc>)))
(lp (cdr l)))
<cc>)))
(<define> (read_Q v q)
(let ((v (<lookup> v)))
(<define> (read_Q e v q)
;(<pp> `(read ,e))
(let* ((v (<lookup> v)))
(<=> q ,(car (<lookup> (vector-ref v nq))))))
(<define> (copy_state v1 v2)
......
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