Optimization for non unifying choices added

parent 24a49db9
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
#:use-module (logic guile-log guile-prolog vm vm-goal) #:use-module (logic guile-log guile-prolog vm vm-goal)
#:use-module (system vm assembler) #:use-module (system vm assembler)
#:re-export (compile_goal begin_att end_att cc) #:re-export (compile_goal begin_att end_att cc)
#:export (compilable_scm collect_data #:export (compilable_scm collect_data define-prolog-fkn
make-vm-function make-vm-function
compile_to_fkn compile_to_fkn
instr define-prolog)) instr define-prolog))
...@@ -175,7 +175,13 @@ variables is the most difficult part to maintain ...@@ -175,7 +175,13 @@ variables is the most difficult part to maintain
(mk-instructions instructions) (mk-instructions instructions)
(list->vector constants) (list->vector constants)
tvar)))))))))) tvar))))))))))
#;
(define (get-mod c)
(let ((a (procedure-property c 'module)))
(if a
a
(module-name (current-module)))))
(<define> (compile_to_meta stx code meta) (<define> (compile_to_meta stx code meta)
(<var> (stackSize constants l nvar nsvar tvar narg) (<var> (stackSize constants l nvar nsvar tvar narg)
(compile_goal code l stackSize narg constants #f) (compile_goal code l stackSize narg constants #f)
...@@ -196,17 +202,22 @@ variables is the most difficult part to maintain ...@@ -196,17 +202,22 @@ variables is the most difficult part to maintain
(constants-r (map (lambda (c) (constants-r (map (lambda (c)
(let ((c (<lookup> c))) (let ((c (<lookup> c)))
#`(@@ #`(@@
#,(precedure-property c 'mod) #,(map
#,(precedure-property c 'name)))) (lambda (x)
(datum->syntax stx x))
(get-mod c))
#,(datum->syntax
stx
(procedure-name c)))))
constants))) constants)))
<cut> <cut>
(<=> meta (<=> meta
#`(make-vm-function ,#`(make-vm-function
'(#,(+ narg 4) . #,(+ stackSize nsvar)) '(#,(+ narg 4) . #,(+ stackSize nsvar))
`#,(pack-start nvar `#,(pack-start nvar
stackSize stackSize
(mk-instructions instructions) (mk-instructions instructions)
,(vector #,@constants-r) #`,(vector #,@constants-r)
tvar))))))))) tvar)))))))))
(define readline_term_str (@@ (logic guile-log guile-prolog interpreter) (define readline_term_str (@@ (logic guile-log guile-prolog interpreter)
...@@ -218,7 +229,20 @@ generate_lambda(X,F) :- ...@@ -218,7 +229,20 @@ generate_lambda(X,F) :-
compile_to_fkn(T,F). compile_to_fkn(T,F).
") ")
(define-syntax-rule (define-prolog n code-string)
(compile-prolog-string "
generate_stx(STX,X,F) :-
catch(
(
readline_term_str(X,T,[variables(V),variable_names(N)]),
compile_to_meta(STX,T,F)
),E,
(
write(error(E)),nl,F=1
)).
")
(define-syntax-rule (define-prolog-fkn n code-string)
(define n (letrec ((n (define n (letrec ((n
(let ((g (prolog-run 1 (f) (let ((g (prolog-run 1 (f)
(generate_lambda code-string f)))) (generate_lambda code-string f))))
...@@ -226,3 +250,30 @@ generate_lambda(X,F) :- ...@@ -226,3 +250,30 @@ generate_lambda(X,F) :-
(error "failed compile") (error "failed compile")
(car g))))) (car g)))))
n))) n)))
(define (cur x)
(map (lambda (s) (datum->syntax x s))
(module-name (current-module))))
(define-syntax define-prolog
(lambda (x)
(syntax-case x ()
((_ n code-string)
#`(define n (let ((g (lambda ()
#,(let ((g (prolog-run 1 (meta)
(generate_stx x
(syntax->datum
#'code-string)
meta))))
(if (null? g)
(lambda x (error "not implemented"))
(if (not (eq? (car g) 1))
(car g)
(lambda x
(error "not implemented"))))))))
(letrec ((n (lambda x
(let ((gg (g)))
(module-set! (resolve-module '#,(cur x))
'n gg)
(apply gg x)))))
n)))))))
...@@ -50,6 +50,7 @@ constant = #(nlocals nstack constants code) ...@@ -50,6 +50,7 @@ constant = #(nlocals nstack constants code)
(<global> SCM *gp-is-delayed?* (<scm> #f)) (<global> SCM *gp-is-delayed?* (<scm> #f))
(<declare-s> SCM gp_get_state_token ()) (<declare-s> SCM gp_get_state_token ())
(<declare-s> SCM gp_cons_bang ((SCM x) (SCM y) (SCM s)))
(<declare-s> SCM scm_gr_p ((SCM x) (SCM y))) (<declare-s> SCM scm_gr_p ((SCM x) (SCM y)))
(<declare-s> SCM scm_less_p ((SCM x) (SCM y))) (<declare-s> SCM scm_less_p ((SCM x) (SCM y)))
(<declare-s> SCM scm_geq_p ((SCM x) (SCM y))) (<declare-s> SCM scm_geq_p ((SCM x) (SCM y)))
...@@ -91,8 +92,10 @@ constant = #(nlocals nstack constants code) ...@@ -91,8 +92,10 @@ constant = #(nlocals nstack constants code)
(<declare-s> SCM gp_gp_cdr ((SCM x) (SCM s))) (<declare-s> SCM gp_gp_cdr ((SCM x) (SCM s)))
(<declare-s> SCM gp_with_fluid ((SCM x) (SCM y))) (<declare-s> SCM gp_with_fluid ((SCM x) (SCM y)))
(<declare-s> SCM gp_gp_newframe ((SCM s))) (<declare-s> SCM gp_gp_newframe ((SCM s)))
(<declare-s> SCM gp_gp_unwind ((SCM s))) (<declare-s> SCM gp_gp_unwind_ncons ((SCM s) (int ncons)))
(<declare-s> SCM gp_gp_unwind_soft ((int ncons)))
(<declare-s> SCM gp_gp_unwind_tail ((SCM s))) (<declare-s> SCM gp_gp_unwind_tail ((SCM s)))
(<declare-s> SCM gp_gp_unwind ((SCM s)))
(<declare-s> SCM gp_set ((SCM a) (SCM b) (SCM s))) (<declare-s> SCM gp_set ((SCM a) (SCM b) (SCM s)))
(<declare-s> int scm_is_true ((SCM x))) (<declare-s> int scm_is_true ((SCM x)))
(<declare-s> int scm_is_false ((SCM x))) (<declare-s> int scm_is_false ((SCM x)))
...@@ -115,6 +118,8 @@ constant = #(nlocals nstack constants code) ...@@ -115,6 +118,8 @@ constant = #(nlocals nstack constants code)
(<declare-s> SCM scm_make_variable ((SCM s))) (<declare-s> SCM scm_make_variable ((SCM s)))
(<declare-s> int SCM_VARIABLEP ((SCM s))) (<declare-s> int SCM_VARIABLEP ((SCM s)))
(<declare-s> int gp_varp ((SCM x) (SCM s))) (<declare-s> int gp_varp ((SCM x) (SCM s)))
(<declare-s> int gp_pair ((SCM x) (SCM s)))
(<declare-s> SCM gp_custom_fkn ((SCM model) (SCM a) (SCM b) (SCM c) (<declare-s> SCM gp_custom_fkn ((SCM model) (SCM a) (SCM b) (SCM c)
(SCM d))) (SCM d)))
(<declare-s> remove_me_t gp_make_vm_model ()) (<declare-s> remove_me_t gp_make_vm_model ())
...@@ -130,6 +135,10 @@ constant = #(nlocals nstack constants code) ...@@ -130,6 +135,10 @@ constant = #(nlocals nstack constants code)
(<=> middle (CONS (<scm> '()) session)) (<=> middle (CONS (<scm> '()) session))
(<=> pinned? (<scm> #f))))) (<=> pinned? (<scm> #f)))))
(define-syntax-rule (GPPAIR? x s) (TRUE (<call> gp_pair x s)))
(define-syntax-rule (GPCAR x s) (LOOKUP (<call> gp_car x s) s))
(define-syntax-rule (GPCDR x s) (LOOKUP (<call> gp_gp_cdr x s) s))
(define-syntax-rule (GPCONS x y s) (<call> gp_cons_bang x y s))
(define-syntax-rule (1- x) (int->scm (<-> (scm->int x) (<c> 1)))) (define-syntax-rule (1- x) (int->scm (<-> (scm->int x) (<c> 1))))
(define-syntax-rule (GET-TOKEN) (<call> gp_get_state_token)) (define-syntax-rule (GET-TOKEN) (<call> gp_get_state_token))
(define-syntax-rule (SET x y s) (<call> gp_set x y s)) (define-syntax-rule (SET x y s) (<call> gp_set x y s))
...@@ -732,19 +741,18 @@ constant = #(nlocals nstack constants code) ...@@ -732,19 +741,18 @@ constant = #(nlocals nstack constants code)
(define-syntax-rule (STORE-STATE tp tag s p stack) (define-syntax-rule (STORE-STATE tp tag s p stack)
(CONS (CONS tag (GPCONS (GPCONS tag
(CONS s (GPCONS p
(<if> tp (<if> tp
(CONS p (GPCONS s (<call> scm_fluid_ref *delayers*) s)
(<call> scm_fluid_ref *delayers*)) s)
p))) s)
stack)) s)
stack s))
(define-syntax-rule (STORE-STATE-SOFT tag p stack)
(CONS (CONS tag (define-syntax-rule (STORE-STATE-SOFT s tag p stack)
(CONS (<scm> #f) (GPCONS (GPCONS tag p s)
p)) stack s))
stack))
(define-syntax-rule (CLEAR-SP-XP sp xp) (define-syntax-rule (CLEAR-SP-XP sp xp)
(<recur> lp () (<recur> lp ()
...@@ -762,53 +770,60 @@ constant = #(nlocals nstack constants code) ...@@ -762,53 +770,60 @@ constant = #(nlocals nstack constants code)
(define-syntax-rule (RESTORE-STATE s tag stack) (define-syntax-rule (RESTORE-STATE s tag stack)
(<recur> lp () (<recur> lp ()
(<let> ((x (CAR stack))) (<let> ((x (GPCAR stack s)))
(<if> (EQ (CAR x) tag) (<if> (EQ (GPCAR x s) tag)
(<let*> ((x1 (CDR x)) (<let*> ((x1 (GPCDR x s))
(ss (CAR x1)) (x2 (GPCDR x1 s)))
(x2 (CDR x1))) (<if> (GPPAIR? x2 s)
(<=> s ss) (<begin>
(<if> (PAIR? x2)
(<call> scm_fluid_set_x *delayers* (<call> scm_fluid_set_x *delayers*
(CDR x2)))) (GPCDR x2 s))
(<=> s (GPCAR x2 s))
(<c> 4))
(<begin>
(<=> s x2)
(<c> 3))))
(<begin> (<begin>
(<=> stack (CDR stack)) (<=> stack (GPCDR stack s))
(<next> lp)))))) (<next> lp))))))
(define-syntax-rule (RESTORE-STATE-TAIL s p tag stack) (define-syntax-rule (RESTORE-STATE-TAIL s p tag stack)
(<recur> lp () (<recur> lp ()
(<let> ((x (CAR stack))) (<let> ((x (GPCAR stack s)))
(<if> (EQ (CAR x) tag) (<if> (EQ (GPCAR x s) tag)
(<let*> ((x1 (CDR x)) (<let*> ((x1 (GPCDR x s))
(ss (CAR x1)) (x2 (GPCDR x1 s)))
(x2 (CDR x1))) (<=> p (GPCAR x1 s))
(<=> stack (CDR stack)) (<=> stack (GPCDR stack s))
(<=> s ss)
(<if> (PAIR? x2) (<if> (PAIR? x2)
(<begin> (<let> ((ss (GPCAR x2 s)))
(<=> p (CAR x2))
(<call> scm_fluid_set_x *delayers* (<call> scm_fluid_set_x *delayers*
(CDR x2))) (GPCDR x2 s))
(<=> p x2))) (<=> s ss))
(<=> s x2)))
(<begin> (<begin>
(<=> stack (CDR stack)) (<=> stack (GPCDR stack s))
(<next> lp)))))) (<next> lp))))))
(define-syntax-rule (RESTORE-STATE-SOFT p tag stack) (define-syntax-rule (RESTORE-STATE-SOFT s p tag stack)
(<recur> lp () (<recur> lp ()
(<let> ((x (CAR stack))) (<let> ((x (GPCAR stack s)))
(<if> (EQ (CAR x) tag) (<if> (EQ (GPCAR x s) tag)
(<let*> ((x1 (CDR x)) (<let*> ((x1 (GPCDR x s)))
(x2 (CDR x1))) (<=> stack (GPCDR stack s))
(<=> stack (CDR stack)) (<if> (GPPAIR? x1 s)
(<if> (PAIR? x2) (<begin>
(<=> p (CAR x2)) (<=> p (GPCAR x1 s))
(<=> p x2))) (<if> (GPPAIR? (GPCDR x1 s) s)
(<c> 4)
(<c> 3)))
(<begin>
(<=> p x1)
(<c> 2))))
(<begin> (<begin>
(<=> stack (CDR stack)) (<=> stack (GPCDR stack s))
(<next> lp)))))) (<next> lp))))))
(define-syntax-rule (NEXT inst-pt) (define-syntax-rule (NEXT inst-pt)
(<let> (((void *) jmp (<ref> *operations* (<let> (((void *) jmp (<ref> *operations*
(scm->int (<*> inst-pt))))) (scm->int (<*> inst-pt)))))
...@@ -835,9 +850,13 @@ constant = #(nlocals nstack constants code) ...@@ -835,9 +850,13 @@ constant = #(nlocals nstack constants code)
(<begin> (<begin>
(REGISTER store-state) (REGISTER store-state)
(REGISTER softie) (REGISTER softie)
(REGISTER softie-light)
(REGISTER newframe) (REGISTER newframe)
(REGISTER newframe-light)
(REGISTER unwind) (REGISTER unwind)
(REGISTER unwind-tail) (REGISTER unwind-tail)
(REGISTER unwind-light)
(REGISTER unwind-light-tail)
(REGISTER newframe-negation) (REGISTER newframe-negation)
(REGISTER unwind-negation) (REGISTER unwind-negation)
...@@ -1302,11 +1321,13 @@ constant = #(nlocals nstack constants code) ...@@ -1302,11 +1321,13 @@ constant = #(nlocals nstack constants code)
(<next> lp (CDR l))))) (<next> lp (CDR l)))))
(<call> gp_gp_newframe s))) (<call> gp_gp_newframe s)))
(define-syntax-rule (mk-unw UNWIND gp_gp_unwind) (define-syntax-rule (UNWIND-SOFT ncons)
(define-syntax-rule (UNWIND s) (<call> gp_gp_unwind_soft ncons))
(define-syntax-rule (UNWIND s ncons)
(<begin> (<begin>
(<call> scm_fluid_set_x *unwind-hooks* (<scm> '())) (<call> scm_fluid_set_x *unwind-hooks* (<scm> '()))
(<call> gp_gp_unwind s) (<call> gp_gp_unwind_ncons s ncons)
(<recur> lp ((SCM l (CDR (<call> scm_fluid_ref *unwind-parameters*)))) (<recur> lp ((SCM l (CDR (<call> scm_fluid_ref *unwind-parameters*))))
(<if> (PAIR? l) (<if> (PAIR? l)
(<let> ((SCM f (CAR l))) (<let> ((SCM f (CAR l)))
...@@ -1317,11 +1338,30 @@ constant = #(nlocals nstack constants code) ...@@ -1317,11 +1338,30 @@ constant = #(nlocals nstack constants code)
(<if> (PAIR? l) (<if> (PAIR? l)
(<begin> (<begin>
(CALL (CAR l) s *false* *true*) (CALL (CAR l) s *false* *true*)
(<call> gp_gp_unwind s) (<call> gp_gp_unwind_ncons s ncons)
(<next> lp (CDR l)))))))) (<next> lp (CDR l)))))))
(mk-unw UNWIND gp_gp_unwind) (define-syntax-rule (UNWIND-TAIL s)
(mk-unw UNWIND-TAIL gp_gp_unwind_tail) (<begin>
(<call> scm_fluid_set_x *unwind-hooks* (<scm> '()))
(<recur> lp ((SCM l (CDR (<call> scm_fluid_ref *unwind-parameters*))))
(<if> (PAIR? l)
(<let> ((SCM f (CAR l)))
(CALL (CAR f) (CDR f))
(<next> lp (CDR l)))))
(<let> ((SCM l (<call> scm_reverse
(<call> scm_fluid_ref *unwind-hooks*))))
(<if> (PAIR? l)
(<begin>
(<call> gp_gp_unwind s)
(<recur> lp ((SCM l l))
(<if> (PAIR? l)
(<begin>
(CALL (CAR l) s *false* *true*)
(<call> gp_gp_unwind s)
(<next> lp (CDR l)))))
(<call> gp_gp_unwind_tail s))
(<call> gp_gp_unwind_tail s)))))
(<define> SCM gp_c_vector_x ((SCM x) (int n) (SCM s)) (<define> SCM gp_c_vector_x ((SCM x) (int n) (SCM s))
(<let> ((x (<call> gp_gp_lookup x s))) (<let> ((x (<call> gp_gp_lookup x s)))
...@@ -1599,7 +1639,15 @@ constant = #(nlocals nstack constants code) ...@@ -1599,7 +1639,15 @@ constant = #(nlocals nstack constants code)
(PRSTACK sp fp) (PRSTACK sp fp)
(<let> ((SCM np (<ref> inst-pt (<c> 0)))) (<let> ((SCM np (<ref> inst-pt (<c> 0))))
(<=> inst-pt (<+> inst-pt (<c> 1))) (<=> inst-pt (<+> inst-pt (<c> 1)))
(<=> ctrl-stack (STORE-STATE-SOFT np p ctrl-stack)) (<=> ctrl-stack (STORE-STATE-SOFT s np p ctrl-stack))
(NEXT inst-pt))
(LABEL newframe-light)
(PRSTACK sp fp)
(<let> ((SCM np (<ref> inst-pt (<c> 0))))
(<=> inst-pt (<+> inst-pt (<c> 1)))
(<=> ctrl-stack (STORE-STATE-SOFT s np p ctrl-stack))
(<=> p np)
(NEXT inst-pt)) (NEXT inst-pt))
(LABEL newframe) (LABEL newframe)
...@@ -1688,22 +1736,43 @@ constant = #(nlocals nstack constants code) ...@@ -1688,22 +1736,43 @@ constant = #(nlocals nstack constants code)
(UNWIND-TAIL s) (UNWIND-TAIL s)
(NEXT inst-pt)) (NEXT inst-pt))
(LABEL unwind-light-tail)
(PRSTACK sp fp)
(<let> ((SCM tag (<*> inst-pt)))
(<=> inst-pt (<+> inst-pt (<c> 1)))
(<let> ((int ncons (RESTORE-STATE-SOFT s p tag ctrl-stack)))
(UNWIND-SOFT ncons)
(NEXT inst-pt)))
(LABEL softie) (LABEL softie)
(PRSTACK sp fp) (PRSTACK sp fp)
(<let> ((SCM tag (<*> inst-pt))) (<let> ((SCM tag (<*> inst-pt)))
(<=> inst-pt (<+> inst-pt (<c> 1))) (<=> inst-pt (<+> inst-pt (<c> 1)))
(RESTORE-STATE-SOFT p tag ctrl-stack) (<let> ((int ncons (RESTORE-STATE-SOFT s p tag ctrl-stack)))
(NEXT inst-pt)) (NEXT inst-pt)))
(LABEL softie-light)
(PRSTACK sp fp)
(<let> ((SCM tag (<*> inst-pt)))
(<=> inst-pt (<+> inst-pt (<c> 1)))
(<let> ((int ncons (RESTORE-STATE-SOFT s p tag ctrl-stack)))
(UNWIND-SOFT ncons)
(NEXT inst-pt)))
(LABEL unwind) (LABEL unwind)
(PRSTACK sp fp) (PRSTACK sp fp)
(<let> ((SCM tag (<ref> inst-pt (<c> 0)))) (<let> ((SCM tag (<ref> inst-pt (<c> 0))))
(<=> p (<ref> inst-pt (<c> 1))) (<=> p (<ref> inst-pt (<c> 1)))
(<=> inst-pt (<+> inst-pt (<c> 2))) (<=> inst-pt (<+> inst-pt (<c> 2)))
(RESTORE-STATE s tag ctrl-stack) (<let> ((int ncons (RESTORE-STATE s tag ctrl-stack)))
(UNWIND s) (UNWIND s ncons)
(NEXT inst-pt)) (NEXT inst-pt)))
(LABEL unwind-light)
(PRSTACK sp fp)
(<=> p (<ref> inst-pt (<c> 1)))
(<=> inst-pt (<+> inst-pt (<c> 2)))
(NEXT inst-pt)
(LABEL unwind-negation) (LABEL unwind-negation)
...@@ -1715,6 +1784,7 @@ constant = #(nlocals nstack constants code) ...@@ -1715,6 +1784,7 @@ constant = #(nlocals nstack constants code)
(<call> gp_fluid_force_bang *gp-is-delayed?* (<scm> #f) s) (<call> gp_fluid_force_bang *gp-is-delayed?* (<scm> #f) s)
(BACKTRACK p instructions inst-pt fp sp)) (BACKTRACK p instructions inst-pt fp sp))
(LABEL false) (LABEL false)
(PRSTACK sp fp) (PRSTACK sp fp)
(BACKTRACK p instructions inst-pt fp sp) (BACKTRACK p instructions inst-pt fp sp)
......
...@@ -93,6 +93,7 @@ get_post(S,C,Cplx,Tail,X,XX) :- ...@@ -93,6 +93,7 @@ get_post(S,C,Cplx,Tail,X,XX) :-
). ).
caller(cc,Args,label(G,N),V,[L,LL]) :- !, caller(cc,Args,label(G,N),V,[L,LL]) :- !,
touch_Q(V),
narg(Args,0,MM), narg(Args,0,MM),
M is MM + 3, M is MM + 3,
(M==N -> true ; throw(cc_does_not_match_caller)), (M==N -> true ; throw(cc_does_not_match_caller)),
...@@ -108,6 +109,7 @@ caller(cc,Args,label(G,N),V,[L,LL]) :- !, ...@@ -108,6 +109,7 @@ caller(cc,Args,label(G,N),V,[L,LL]) :- !,
LL2 = [[Goto,G]|LL]. LL2 = [[Goto,G]|LL].
caller(cc,Args,Tail,V,[L,LL]) :- !, caller(cc,Args,Tail,V,[L,LL]) :- !,
touch_Q(V),
(Tail=#f -> throw(cc_not_in_tail_context) ; true), (Tail=#f -> throw(cc_not_in_tail_context) ; true),
tr('clear-sp' , Clear), tr('clear-sp' , Clear),
L=[[Clear]|L2], L=[[Clear]|L2],
...@@ -123,6 +125,7 @@ caller(cc,Args,Tail,V,[L,LL]) :- !, ...@@ -123,6 +125,7 @@ caller(cc,Args,Tail,V,[L,LL]) :- !,
LL2 = [[Call]|LL]. LL2 = [[Call]|LL].
caller(F,Args,Tail,V,[L,LL]) :- caller(F,Args,Tail,V,[L,LL]) :-
touch_Q(V),
get_recur(F,A,N) -> rec(F,A,N,Args,Tail,V,[L,LL]) ; get_recur(F,A,N) -> rec(F,A,N,Args,Tail,V,[L,LL]) ;
( (
tr('clear-sp' , Clear), tr('clear-sp' , Clear),
......
...@@ -39,6 +39,9 @@ compile_conj0([],Tail,V,L) :- throw(#t). ...@@ -39,6 +39,9 @@ compile_conj0([],Tail,V,L) :- throw(#t).
compile_conj0([X],Tail,V,L) :- !, compile_conj0([X],Tail,V,L) :- !,
compile_goal(X,Tail,V,L). compile_goal(X,Tail,V,L).
compile_conj0([X|Gs],Tail,V,L) :- var(X),!,
compile_conj0([call(X)|Gs],Tail,V,L).
compile_conj0([!|Gs],Tail,V,[L,LL]) :- !, compile_conj0([!|Gs],Tail,V,[L,LL]) :- !,
ifc(compile_conj0(Gs,Tail,V,[L1,LL]),E, ifc(compile_conj0(Gs,Tail,V,[L1,LL]),E,
( (
...@@ -54,6 +57,7 @@ compile_conj0([!|Gs],Tail,V,[L,LL]) :- !, ...@@ -54,6 +57,7 @@ compile_conj0([!|Gs],Tail,V,[L,LL]) :- !,
)). )).
compile_conj0([softie(A)|Gs],Tail,V,[L,LL]) :- !, compile_conj0([softie(A)|Gs],Tail,V,[L,LL]) :- !,
pop_Q(V,Q),
ifc(compile_conj0(Gs,Tail,V,[L1,LL]),E, ifc(compile_conj0(Gs,Tail,V,[L1,LL]),E,
( (
tfc(E), tfc(E),
...@@ -66,7 +70,12 @@ compile_conj0([softie(A)|Gs],Tail,V,[L,LL]) :- !, ...@@ -66,7 +70,12 @@ compile_conj0([softie(A)|Gs],Tail,V,[L,LL]) :- !,
) )
), ),
( (
(
var(Q) ->
L=[['softie-light',A]|L1];
L=[[softie,A]|L1] L=[[softie,A]|L1]
),
push_Q(V,Q)
)). )).
compile_conj0([(fail;false)|Gs],Tail,V,[L,LL]) :- !, compile_conj0([(fail;false)|Gs],Tail,V,[L,LL]) :- !,
......
...@@ -34,23 +34,23 @@ collect_disjunction(';'(|L),U,UU) :- !, ...@@ -34,23 +34,23 @@ collect_disjunction(';'(|L),U,UU) :- !,
collect_disjunction(X,[X|UU],UU). collect_disjunction(X,[X|UU],UU).
%head_at_true(First,Last,A,C,Lab,Lab2,L1,LLX) %head_at_true(First,Last,A,C,Lab,Lab2,L1,LLX)
head_at_true(#t,_,A,C,Lab,Lab2,L1,LLX) :- L1=LLX, Lab2=Lab. head_at_true(Q,#t,_,A,C,Lab,Lab2,L1,LLX) :- L1=LLX, Lab2=Lab.
head_at_true(#t,_,A,C,Lab,Lab2,L1,LLX) :- L1=LLX, Lab2=Lab. head_at_true(Q,#t,_,A,C,Lab,Lab2,L1,LLX) :- L1=LLX, Lab2=Lab.
head_at_true(#f,#f,A,C,Lab,Lab2,L1,LLX) :- head_at_true(Q,#f,#f,A,C,Lab,Lab2,L1,LLX) :-
tr(unwind,Unwind), (var(Q) -> tr('unwind-light',Unwind) ; tr(unwind,Unwind)),
label(Lab2),
L1=[[label,Lab,U],[Unwind,A,Lab2]|LLX]. L1=[[label,Lab,U],[Unwind,A,Lab2]|LLX].
head_at_true(#f,#t,A,C,Lab,Lab2,L1,LLX) :- head_at_true(Q,#f,#t,A,C,Lab,Lab2,L1,LLX) :-
label(Lab2), (var(Q) -> tr('unwind-light-tail',Unwind) ; tr('unwind-tail',Unwind)),
tr('unwind-tail',UnwindTail), L1=[[label,Lab,U],[Unwind,A]|LLX].
L1=[[label,Lab,U],[UnwindTail,A]|LLX].
compile_disjunction0 compile_disjunction0
([X],First,Aq,Ae,Out,Lab,A,Tail,S0,[U],V,[L,LL]) :- !, ([X],First,Aq,Ae,Out,Lab,A,Tail,S0,[U],V,[L,LL]) :- !,
(First=#t -> compile_goal(X,First,V,[L,LL]) ; (First=#t -> compile_goal(X,First,V,[L,LL]) ;
catch(( catch((
read_Q(V,Qit),
pop_Q(V,_),
set_F(V,scm[(gensym \"tag\")]), set_F(V,scm[(gensym \"tag\")]),
get_CES(V,[C|_],E,S), get_CES(V,[C|_],E,S),
set_AES(V,Aq,0,S0), set_AES(V,Aq,0,S0),
...@@ -67,7 +67,7 @@ compile_disjunction0 ...@@ -67,7 +67,7 @@ compile_disjunction0
EE is E \\/ E1, EE is E \\/ E1,
set_AES(V,Aq,EE,SS), set_AES(V,Aq,EE,SS),
U = [E1,_], U = [E1,_],
head_at_true(First,#t,A,C,Lab,Lab2,L,LX) head_at_true(Qit,First,#t,A,C,Lab,Lab2,L,LX)
)),Er, )),Er,
( (
tfc(Er), tfc(Er),
...@@ -76,7 +76,7 @@ compile_disjunction0 ...@@ -76,7 +76,7 @@ compile_disjunction0
( (
First==#t -> First==#t ->
throw(#t) ; throw(#t) ;
head_at_true(#f,#t,A,C,Lab,Lab2,L,LL) head_at_true(Qit,#f,#t,A,C,Lab,Lab2,L,LL)
); );
Er == c -> Er == c ->
throw(c) ; throw(c) ;
...@@ -85,6 +85,7 @@ compile_disjunction0 ...@@ -85,6 +85,7 @@ compile_disjunction0
))). ))).
goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :- goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :-
read_Q(V,Qit),
get_CES(V,[C|_],E,S), get_CES(V,[C|_],E,S),
set_AES(V,Aq,0,S0), set_AES(V,Aq,0,S0),
(First==#t -> true ; set_F(V,scm[(gensym \"tag\")])), (First==#t -> true ; set_F(V,scm[(gensym \"tag\")])),
...@@ -113,18 +114,20 @@ goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :- ...@@ -113,18 +114,20 @@ goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,[U|UU],V,L,LL,LG,LLX) :-
Err==#t -> Err==#t ->
throw(bug_true_not_be_send_in_non_first_disjunction); throw(bug_true_not_be_send_in_non_first_disjunction);
( (
head_at_true(First,#f,A,C,Lab,Lab2,L,LX), pop_Q(V,_),
head_at_true(Qit,First,#f,A,C,Lab,Lab2,L,LX),
Err==c -> Err==c ->
LLX=[[cut],[fail]|LL]; LLX=[[cut],[fail]|LL];
LLX=LL LLX=LL
) )
) )
), ),
head_at_true(First,#f,A,C,Lab,Lab2,L,LX) head_at_true(Qit,First,#f,A,C,Lab,Lab2,L,LX)
). ).
compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !, compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !,
tr('goto-inst',Goto), tr('goto-inst',Goto),
read_Q(V,Qit),
(Tail==#t -> LG=LLX ; LG = [[Goto,Out]|LLX]), (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, catch(goal(X,Y,First,Lab,Tail,Out,A,Ae,Aq,S0,U,V,L,LL,LG,LLX), Er,
( (
...@@ -146,7 +149,7 @@ compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !, ...@@ -146,7 +149,7 @@ compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !,
First = #t -> First = #t ->
throw(#t); throw(#t);
( (
head_at_true(#f,#t,A,C,Lab,Lab2,L,LLG), head_at_true(Qit,#f,#t,A,C,Lab,Lab2,L,LLG),
LLX=LL LLX=LL
) )
); );
...@@ -157,7 +160,7 @@ compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !, ...@@ -157,7 +160,7 @@ compile_disjunction0([X|Y],First,Aq,Ae,Out, Lab,A,Tail,S0,U,V,[L,LL]) :- !,
(First==#t -> true ; (First==#t -> true ;