vm-goal.scm 11.6 KB
Newer Older
1
(define-module (logic guile-log guile-prolog vm vm-goal)
2
  #:use-module (logic guile-log)
3
  #:use-module (compat racket misc)
4 5 6 7
  #: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)
8 9
  #:use-module (logic guile-log guile-prolog vm vm-pre)
  #:use-module (logic guile-log guile-prolog vm vm-var)
10 11 12 13 14
  #:use-module (logic guile-log guile-prolog vm vm-args)
  #:use-module (logic guile-log guile-prolog vm vm-unify)
  #:use-module (logic guile-log guile-prolog vm vm-imprint)
  #:use-module (logic guile-log guile-prolog vm vm-scm)
  #:use-module (logic guile-log guile-prolog vm vm-disj)
15
  #:use-module (logic guile-log guile-prolog vm vm-conj)
16
  #:use-module (logic guile-log guile-prolog vm vm-handle)
17
  #:use-module (system vm assembler)
18
  #:export (begin_att end_att recur verbatim_call))
19 20 21 22 23 24 25 26 27 28 29 30 31

(compile-prolog-string "
reverse_op(<,>).
reverse_op(>,<).
reverse_op(=<,>=).
reverse_op(>=,=<).
reverse_op(@<,@>).
reverse_op(@>,@<).
reverse_op(@=<,@>=).
reverse_op(@>=,@=<).
reverse_op(=:=,=:=).
reverse_op(=\\=,=\\=).

32 33
zero(V)    :- get_A(V,A),A=[[0|_]].

34
wrap(Code,[L,LL]) :-
35 36 37 38 39 40 41 42 43 44
  catch(Code,E,
     (  
        tfc(E),
        (
           E==#t -> L=[[[cc]|LL],LL];
           E==c  -> L=[[[cut],[fail]|LL],LL];
           L=[[[fail]|LL],LL]
        )
     )).

45
-extended(',',m_and,;,m_or,\\+,m_not).
46 47 48
compile_goal(Code,Iout):-
  compile_goal(Code,Iout,StackSize,Narg,Consts,#t).

49 50 51 52 53 54 55 56 57 58 59
compile_goal(Code,Iout,StackSize,Narg,Constants,Pretty) :- !,
  (
    Code = (F(|A) :- Goal) -> length(A,Narg) ;
    Code = (F     :- Goal) -> Narg = 0       ;
    throw(compiles_only_clauses(Code))
  ),
  make_vhash(HV),
  make_vhash(HC),
  init_vars,init_e,
  (var(Constants) -> init_const ; true),
  b_setval(pretty,#t),
60
  make_state(0,[[0,_,_]],[0],0,0,0,0,[HC,HV],[],V),
61
  wrap(compile_goal(Code,#t,V,[L,[]]),[L,[]]),
62
  get_M(V,StackSize),
63 64
  handle_all(L,LL),
  (var(Constants)->Constants=scm[(get-consts)];true),
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
65
  write(LL),nl,!,
66 67
  (Pretty==#t -> Iout=LL ; (b_setval(pretty,#f),mmtr(LL,Iout))).

68
compile_goal(X,Tail,V,L) :- var_p(X),!,
69 70
  compile_goal(call(X),Tail,V,L).

71

Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
72
compile_goal(!,Tail,V,[L,LL]) :- !,
73 74
  check_tail(Tail),
  (Tail==#t -> L=[[cut],[cc]|LL] ; L=[[cut]|LL]).
75

76 77 78 79
compile_goal(softie(A),Tail,V,[LL,L]) :- !,
  check_tail(Tail),
  (Tail==#t -> L=[[softie,A],[cc]|LL] ; L=[[softie,A]|LL]).

80
compile_goal(begin_att,Tail,V,[L,LL]) :- !,
81
   check_tail(Tail),
82 83
   tail(Tail,LL,LLL),
   (
84
     Tail==#t -> L=LLL ;
85
     (
86
       get_A(V,A),
87
       A=[[Ai  | _] | _],
88
       set_A(V,[[AAi,AAx,AAt] | A]),
89
       AAi is Ai + 1,
90
       var_p(AAx),
91
       add_var(AAx,V,Tagx),
92
       tr('pre-unify',Pre),
93
       L = [[Pre,AAt,Tagx]|LL]
94 95 96 97
     )
   ).

compile_goal(end_att,Tail,V,[L,LL]) :- !,
98 99
   check_tail(Tail),
   get_AF(V, A, F),
100
   [[Ai,Ax,At]|AA]=A,
101
   set_A(V, AA),
102
   (Ai==0  -> throw(missmatching_begin_end_pair) ; true),
103
   var_p(Ax),
104
   add_var(Ax,V,Tag),
105
   (Tail==#t -> tr('post-unify-tail',Post) ; tr('post-unify',Post)),      
106
   (
107
     Tail==#t ->  LLL=LL ; 
108
     (
109
       At==#t ->
110 111 112 113 114
         (
           tr('post-unicall',PostCall),
           get_C(V,[C|_]),
           LLL=[[PostCall,C,F]|LL]
         ) ;
115 116
         LLL=LL
     )
117
   ),
118 119 120 121 122
   (
      At   == #t  ->  L = [[Post,Tag]|LLL] ; 
      Tail == #t  ->  L = [[cc]|LLL]       ; 
                      L = LLL
   ).  
123 124

compile_goal(pop(N),Tail,V,[L,LL]) :- !,
125
  check_tail(Tail),
126 127
  tr(pop,Pop),
  M is -N,
128
  push_v(M,V),
129 130 131
  tail(Tail,LL,LLL),
  L=[[Pop,N]|LLL].

132

133 134 135 136 137 138 139 140 141 142
compile_goal((Args <= Goal),Tail,V,L) :- !,
  (listp(Args) -> true ; throw(not_proper_head(Args <= goal))),
  reverse(Args,AArgs),
  mg(cc(|Args),AArgs,Impr,0,N),
  NN is N + 3,
  link_l(L,L1,L2,L3),
  compile_goal(Goal,label(G,NN),V,L1),
  L2=[[[label,G]|U],U],
  set_S(V,0),
  push_v(NN,V),
143
  compile_goal((begin_att,Impr,pop(3),end_att),Tail,V,L3).
144

145 146 147 148 149
compile_goal((F(|Args) :- Goal),Tail,V,L) :- !,
  (listp(Args) -> true ; throw(not_proper_head(F(|Args)))),
  reverse(Args,AArgs),
  mg(F(|Args),AArgs,Impr,0,N),
  NN is N + 4,
150
  push_v(NN,V),
151
  get_A(V,[[0|_]|_]) ->
152
     wrap(compile_goal((begin_att,Impr,pop(4),end_att,Goal),Tail,V,L),L);
153
     wrap(compile_goal((begin_att,Impr,pop(4),Goal),Tail,V,L),L).
154 155

compile_goal((F :- Goal),Tail,V,L) :- !,
156
  push_v(4,V),
157
  wrap(compile_goal((pop(4),Goal),Tail,V,L),L).
158

159

160
compile_goal(Op(\"recur\",Args),Tail,V,[L,LL]) :-    
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
161
   Args = F(|U),
162
   Op=\"op2*\",!,
163 164 165 166
   get_line(U,X,Xin,N),
   reverse(X,XX),
   mg(recur(|U),XX,Impr,0,N),
   add_recur(F,A,N),
167
   push_args_args(#f,Xin,V,L,L1,_,_),
168
   touch_A(V),
169
   touch_Q(V),
170
   set_F(V,scm[(gensym \"Rec\")]),
171 172 173
   L1=[[label,A]|L2],
   compile_goal((begin_att,Impr,end_att),Tail,V,[L2,LL]).

174

175
compile_goal((X,Y),Tail,V,L) :- !,
176
  collect_conj((X,Y),Gs,[]),
177
  compile_conj(Gs,Tail,V,L).
178

179

180 181 182
compile_goal(m_or(fail,false),#t,V,[[[fail],[cc] |L], L]).
compile_goal(m_or(fail,false),#f,V,[[[fail]      |L], L]).
compile_goal(true,_,_,_) :- throw(#t).
183 184 185
compile_goal(';'(|X),Tail,V,[L,LL]) :- !,
   collect_disj(X,XX,[]),
   (
186
     XX=[]  -> L=[[false]|LL]                ;
187 188
     XX=[Z] -> compile_goal(Z,Tail,V,[L,LL]) ; 
     (
189
       get_AESM(V,Aq,E,S,M), 
190 191
       label(Lab),label(Out),
       push_Q(V,Q),
192 193
       compile_disjunction(XX,#t,Aq,Ae,Out,Lab,Lab,Tail,S,U,V,LM),!,
       (zero(V) -> Tp is 0 ; Tp is 1),
194 195 196 197 198
       (
         var(Q) ->
            L  = [['newframe-light',Lab   ] | LX];
            L  = [[newframe        ,Lab,Tp] | LX]   
       ),
199
       LM = [LX,  [[label,Out] | LL]],
200
       get_EBH(V,Ed,B,H),  
201 202 203
       add_missing_variables(H,U,Ed,Ed,EEd),!,
       EE is E \\/ EEd,
       set_E(V,EE)
204 205 206
     )
  ).

207
compile_goal(verbatim_call(X),Tail,V,[L,LL]) :-
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
208
   ( \\+var_p(X),
209 210 211
     ( 
       F(|Args)=X -> 
        (
212
          (var_p(F) ; isApply(Args)) -> fail ; true
213 214 215 216 217 218 219 220
        ) ; 
       true
     )
   ),
   !, 
   compile_goal(X,Tail,V,[L,LL]).

compile_goal(call(X),Tail,V,[L,LL]) :-
221
   ( \\+var_p(X),
222 223 224
     ( 
       F(|Args)=X -> 
        (
225
          (var_p(F) ; isApply(Args)) -> fail ; true
226 227 228 229 230 231 232 233 234 235 236
        ) ; 
       true
     )
   ),
   !,
   L=[['newframe-negation',Al,0]|LX],
   get_C(V,C),
   C  = [C0|_],
   CC = [Al|C],
   compile_goal(X,#f,V,[LX,LLX]),
   set_C(V,C),
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
237 238
   (Tail=#t -> LG=[[cc]|LL] ; LG=LL),
   LLX = [['goto-inst'       ,Bl   ],
239 240 241
          [label             ,Al   ],
          ['unwind-negation' ,Al,C0],
          [label             ,Bl   ],
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
242
          ['post-q'          ,C0   ]|LG].
243 244

               
245
compile_goal((X =.. Y),Tail,V, L, LL) :- !,
246
  (var_p(X);constant(X)) ->
247 248 249 250 251 252 253 254
  (
     compile_arg(X,Branch,HC,HV,L,LLX),
     compile_imprint(Y,Branch,HC,HV,LLX,LLY),
     tr(=..,Op),
     LLY=[[Op]|LL]
  ).
  

Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
255
compile_goal(set(V,X),Tail,V,[L,LL]) :- !,
256
  touch_Q(V),
257
  tr(set,Set),
258
  (var_p(X) -> true ; throw(no_var_in_set)),
259 260 261 262 263 264 265 266 267 268
  add_var(X,V,Tag),
  (isFirst(Tag) -> true ; force_variable(Tag)),
  push_args(X,V,L,LX),
  push_v(-1,V),
  (
    Tail=#t ->
       LX=[[Set,Tag],[cc]|LL];
       LX=[[Set,Tag]     |LL]  
  ).

Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
269
compile_goal(once(G),Tail,V,[L,LL]) :- !,
270
  compile_goal(G,#f,V,[LX,LLX]),
271
  tr('store-state',Newframe),
272
  tr('softie'     ,UnwindTail),
273
  (zero(V) -> Tp is 0 ; Tp is 2),
274
  L=[[Newframe,A]|LX],
275 276
  (
    Tail=#t ->
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
277 278
       LLX=[[label,A],[UnwindTail,A],[cc]|LL];
       LLX=[[label,A],[UnwindTail,A]     |LL]
279 280 281 282
  ).
  
compile_goal((X->Y),Tail,V,L) :- !,
  compile_goal((once(X),Y),Tail,V,L).
283

284 285 286 287
compile_goal(\\+\\+\\+X,Tail,V,[L,LL]) :- !,
   compile_goal(\\+X,Tail,V,[L,LL]).

compile_goal(\\+\\+X,Tail,V,[L,LL]) :- !,
288
   L=[['newframe-negation',Al,0]|LX],
289
   get_QACESB(V,Q,A,C,E,S,B),
290
   C  = [C0|_],
291 292
   CC = [Al|C],   
   set_QACE(V,[],[[0|_]],CC,0),
293
   compile_goal(X,#f,V,[LX,LLX]),
294
   set_QACESB(V,Q,A,C,E,S,B),
295 296
   (Tail=#t -> LG=[[cc]|LL] ; LG=LL),
   LLX = [['goto-inst'       ,Bl   ],
297 298 299 300 301
          [label             ,Al   ],
          ['unwind-negation' ,Al,C0],
          [label             ,Bl   ],
          ['post-s'          ,Al,C0]|LG]. 

302
compile_goal(\\+X,Tail,V,[L,LL]) :- !,
303
  check_tail(Tail),
304 305 306 307 308 309
  label(Br),
  tr('newframe-negation', Newframe ),
  tr('unwind-negation'  , Unwind   ),
  tr('post-negation'    , Post     ),
  tr(notend,Notend),
  tail(Tail,LL,LLL),
310
  get_QACESB(V,Q,A,C,E,S,B),
311 312
  C  = [C0|_],
  CC = [Al|C],
313 314
  ifc(
  (
315
     set_QACE(V,[],[[0|_]],CC,0),
316 317
     compile_goal(X,#f,V,[LX,LLX])
  ),Er,
318 319 320 321 322 323 324
  (   
      tfc(Er),
      (Er==#t -> throw(#f) ; throw(#t))
  ),
  (
    get_A(V,A1),
    (A==A1 -> true ; throw(mismatching_begin_end_in_negation)),
325
    set_QACESB(V,Q,A,C,E,S,B),
326
    (A=[[0|_]|_] -> Tp is 0 ; Tp is 1),
327
    L   = [ [Newframe,Al,Tp] |LX ], 
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
328
    LLX = [ [Unwind,Al,C0],[label,Al],[Post,Al,C0] | LLL]
329
  )).
330 331 332 333 334



compile_goal((m_and(Op,m_or(<,>,=<,>=,=:=,=\\=,@<,@=<,@>,@>=)))(X,Y),
              Tail,V,[L,LL]) :- !,
335
  check_tail(Tail),
336
  tail(Tail,LL,LLL),
337
  ifc(compile_scm(X,V,L,LX),EX,
338
     (
339
       ifc(compile_scm(Y,V,L,LY),EY,
340
          (
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
             call(Op(EX,EY)) -> throw(#t) ; throw(#f)
          ),
          (
              push_v(-1,V),
              reverse_op(Op,Or),
              binop1L(Or,O),
              tr(O,OO),
              LY=[[OO,EX]|LLL]
         ))
     ),
     ifc(compile_scm(Y,V,LX,LY),EY,
       (
         push_v(-1,V),
         binop1L(Op,O),
         tr(O,OO),
         LX=[[OO,EY]|LLL]
       ),
       (
         push_v(-2,V),
         tr(Op,OOp),
Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
361 362
         binop(OOp,O),
         LY=[[Op]|LLL]
363
       ))).
364

365 366 367 368 369 370
compile_goal(X is Y,Tail,V,L) :- !,
    (zero(V) -> 
      compile_goal((begin_att,iss(X,Y),end_att),Tail,V,L);
      compile_goal(iss(X,Y),Tail,V,L)).

compile_goal(iss(X,Y),Tail,V,[L,LL]) :- !,
371
  check_tail(Tail),
372 373 374 375 376
  tail(Tail,LL,LLL),
  (
    instruction(Y) ->
    (
      instruction(X) ->
377 378 379
      (
        X==Y -> throw(#t) ; throw(#f)
      );
380 381
      (
        tr('unify-instruction-2',Unify),
382
        var_p(X),
383 384 385 386
        add_var(X,V,Tag),
        L=[[Unify,Tag,Y,#t]|LLL]
      )
    );
387 388
    ifc(compile_scm(Y,V,L,LX),EY,compile_goal(X is EY, Tail, V, [L,LL]),
    (
389
      var_p(X)   ->   
390
       ( 
391
         add_var(X,V,Tag),
392
         (isFirst(Tag) -> true ; touch_Q(V)),
393
         push_v(-1,V),
394 395
         tr(unify,Unify),
         LX=[[unify,Tag,#t]|LLL]
396 397 398 399 400 401 402 403 404 405
       );
       (
         (
          constant(X) ->
             tr('equal-constant',Equal) ; 
          tr('equal-instruction',Equal)
         ),
         push_v(-1,V),
         LX=[[Equal,X]|LLL]
       )
406
    ))).
407
   
408 409

compile_goal(unify_with_occurs_check(X,Y),Tail,V,L) :- !,
410
  touch_Q(V),
411 412 413 414 415 416
  (
    X==Y    -> throw(#t) ;
    zero(V) -> 
      compile_goal((begin_att,uni_0(X,Y),end_att),Tail,V,L);
      compile_goal(uni_0(X,Y),Tail,V,L)
  ).
417 418

compile_goal(uni_0(X,Y),Tail,V,[L,LL]) :- !,
419
  check_tail(Tail),
420 421 422
  tail(Tail,LL,LLL),
  compile_unify(X,Y,V,[L,LLL],0).

423

Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
424
compile_goal(X = Y,Tail,V,L) :- !,
425
  touch_Q(V),
426 427 428 429 430 431
  (
    X==Y    -> throw(#t) ;
    zero(V) -> 
      compile_goal((begin_att,uni_x(X,Y),end_att),Tail,V,L);
      compile_goal(uni_x(X,Y),Tail,V,L)
  ).
432 433

compile_goal(uni_x(X,Y),Tail,V,[L,LL]) :- !,
434
  check_tail(Tail),
435 436 437
  tail(Tail,LL,LLL),
  compile_unify(X,Y,V,[L,LLL],#t).

438 439 440 441 442 443 444
compile_goal(X == Y,Tail,V,L) :- !,
  (
    X==Y    -> throw(#t) ;
    zero(V) -> 
      compile_goal((begin_att,uni(X,Y),end_att),Tail,V,L);
      compile_goal(uni(X,Y),Tail,V,L)
  ).
445 446

compile_goal(uni(X,Y),Tail,V,[L,LL]) :- !,
447
  check_tail(Tail),
448 449 450
  tail(Tail,LL,LLL),
  compile_unify(X,Y,V,[L,LLL],#t).

Stefan Israelsson Tampe's avatar
Stefan Israelsson Tampe committed
451
compile_goal(imprint(X,M),Tail,V,[L,LL]) :- !,
452
  check_tail(Tail),
453 454 455 456 457
  tail(Tail,LL,LLL),
  compile_imprint(X,V,L,LLL,M).

compile_goal(m_and(X,F(|Args)),Tail,V,L) :- !,
   (
458
    (var_p(F) ; isApply(Args)) -> compile_goal(call(X),Tail,V,L) ;
459 460 461 462
    caller(F,Args,Tail,V,L)
   ).

compile_goal(F,Tail,V,L) :-
463
  constant(F) -> (!,caller(F,[],Tail,V,L)).
464 465 466 467

compile_goal(X,_,_,_) :-
  throw(failed_compile_goal(X)).
      
468
isApply(X) :- var_p(X),!.
469 470 471 472 473 474
isApply([X|L]) :- isApply(L).

ncons(X,N) :-
  ncons(X,0,N).
")

475 476 477

(set! (@@ (logic guile-log guile-prolog vm vm-var) compile_goal)
  compile_goal)