home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / lifeos2.zip / LIFE-1.02 / TESTS / LF / INTABS.LF < prev    next >
Text File  |  1996-06-04  |  20KB  |  844 lines
  1.  
  2. %
  3. % This operator is syntactic sugar for project
  4. %
  5.  
  6. % Needed in map, used later on:
  7. my_project(A,B) -> B.A.
  8.  
  9.  
  10. %
  11. % setq for predicates
  12. %
  13. setPred(A,B) :-
  14.         C = eval(B),
  15.         retract(A),
  16.         !,
  17.         U=root_sort(A),
  18.         U=@(C),
  19.         assert(U).
  20. setPred(A,B) :-
  21.         dynamic(A),
  22.         C = eval(B),
  23.         U=A,
  24.         U=@(C),
  25.         assert(U).
  26.  
  27. non_strict(setPred)?
  28.  
  29. %
  30. % set new fact
  31. %
  32.  
  33. non_strict(set_new_fact) ?
  34. set_new_fact(F) :-
  35.     G = root_sort(F),
  36.     dynamic(G),
  37.     assert(F).
  38.  
  39. non_strict(set_fact) ?
  40. set_fact(F) :-
  41.     G = root_sort(F),
  42.     retract((G :- succeed)),
  43.     assert(F).
  44.  
  45. %
  46. %  make a new root from an old one and a suffix
  47. %
  48. suffixRoot(P,S:string) -> str2psi(strcon(psi2str(P),S)).
  49.  
  50. %
  51. %
  52. %
  53.  
  54. map_pred([],P) :- !.
  55. map_pred([A|B],P) :-
  56.     fake_copy(P) & @(A),
  57.     map_pred(B,P).
  58. %
  59. %
  60. %
  61.  
  62. fake_copy(T) -> root_sort(T)&strip(T).
  63.  
  64.  
  65. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  66. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  67. %
  68. % List manipulation
  69. %
  70. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  71. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  72.  
  73.  
  74. merge_ad([],L) -> L.
  75. merge_ad([A|B],C) -> 
  76.     cond( member_ad(C,A),
  77.           merge_ad(B,C),
  78.           [A|merge_ad(B,C)]).
  79.  
  80. no_redundant_ad([]) -> [].
  81. no_redundant_ad([A|B]) -> 
  82.     cond( member_ad(B,A),
  83.           no_redundant_ad(B),
  84.           [A|no_redundant_ad(B)]).
  85.  
  86. member_ad([],A) -> false.
  87. member_ad([B|C],A) ->
  88.     cond( A === B,
  89.           true,
  90.           member_ad(C,A)).
  91.  
  92. inter_ad([],L) -> [].
  93. inter_ad([A|B],C) ->
  94.     cond( member_ad(C,A),
  95.           [A| inter_ad(B,C)],
  96.           inter_ad(B,C)).
  97.  
  98. %
  99. % diff_list(L1,L2,L3): L3 is L2 \ (L1 inter L2)
  100. %
  101.  
  102. diff_list_ad([],L2,L2) :- !.
  103. diff_list_ad(L1:[A|NewL1],L2,RestL2) :-
  104.     cond( memberAndRest_ad(A,L2,InterRestL2),
  105.           diff_list_ad(NewL1,InterRestL2,RestL2),
  106.           diff_list_ad(NewL1,L2,RestL2)).
  107.  
  108. %
  109. % memberAndRest(A,List,Rest) returns true if A is a member of List, with Rest
  110. % containing the other members of List. 
  111. %
  112.  
  113. memberAndRest_ad(A,[],Rest) -> false.
  114. memberAndRest_ad(A,[B|C],Rest) ->
  115.     cond( A === B,
  116.           ( true | Rest = C),
  117.           memberAndRest_ad(A,C,OtherRest) | Rest = [B|OtherRest] ).
  118.  
  119. %
  120. % suppress_ad(List,Ad) returns a new list with no member at adress Ad
  121. %
  122.  
  123. supress_ad([],Ad) -> [].
  124. suppress_ad([A|B],Ad) ->
  125.     cond( A === Ad,
  126.           suppress_ad(B,Ad),
  127.           [A|suppress_ad(B,Ad)]).
  128.  
  129. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  130. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  131. %
  132. % compiler for abstract analyser
  133. %
  134. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  135. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  136.  
  137. op(1200,xfy,::--) ?
  138. non_strict(::--) ?
  139. op(1200,xf,'..') ?
  140. non_strict('..') ?
  141.  
  142. (Lhs '..') :-
  143.     PName = suffixRoot(Lhs,"_proc"),
  144.     setPred(PName,proced(global_vars => [],
  145.                          actions => [])).
  146. (Lhs ::-- Rhs) :-
  147.     abst_head(Lhs,GlobalVars),
  148.     abst_body(Rhs,GlobalVars,Vars,Actions),
  149.     PName = suffixRoot(Lhs,"_proc"),
  150.     PName = @(global_vars => GlobalVars,
  151.               actions => Actions),
  152.     set_new_fact(PName).
  153.  
  154.  
  155.  
  156. abst_head(Lhs,GlobalVars) :-
  157.     GlobalVars = map(my_project(2=>Lhs),features(Lhs)).
  158.  
  159.  
  160.  
  161. non_strict(abst_body) ?
  162.  
  163. abst_body((A,B),GVars,NGVars,Actions) :-
  164.     !,
  165.     abst_body(B,GVars,NGVarsB,ActionsB),
  166.     abst_body(A,NGVarsB,NGVars,[ActionA]),
  167.     Actions = [ActionA|ActionsB].
  168.  
  169. abst_body(A,GVars,NGVars,Actions) :-
  170.     abst_action(A,GVars,NGVars,ActionA),
  171.     Actions = [ActionA].
  172.  
  173.  
  174. non_strict(abst_action) ?
  175.  
  176. abst_action(A:(X=Y),GVars,NGVars,Action) :-
  177.     !,
  178.     Action = unif(X,Y),
  179.     NGVars = merge_ad( vars_in_term(A),GVars).
  180.  
  181. abst_action(D:(A;B),GVars,NGVars,ActionD) :-
  182.     !,
  183.     abst_body(A,GVars,NGVarsA,ActionsA),
  184.     abst_body(B,GVars,NGVarsB,ActionsB),
  185.     NGVars = merge_vars(NGVarsA,NGVarsB),
  186.     ActionD = disjunc( ActionsA,
  187.                         ActionsB,
  188.             global_vars  => inter_ad(vars_in_term(D),GVars)).
  189.  
  190. abst_action(A,GVars,NGVars,Action) :- 
  191.     Action = abscall(root_sort(A),map(my_project(2=>A),features(A))),
  192.     NGVars = merge_ad(vars_in_term(A),GVars).
  193.  
  194.  
  195. non_strict(vars_in_term) ?
  196. vars_in_term(X) ->
  197.     cond( F:features(X) :== [],
  198.           cond( root_sort(X) :== @,
  199.                 [X],
  200.             []),
  201.           ( vars_in_features(G,X) | G = F)).
  202.  
  203. non_strict(vars_in_features) ?
  204. vars_in_features([],X) -> [].
  205. vars_in_features([F1|Fs],X) -> 
  206.     Vars
  207.     |   T = X.F1,
  208.     Vars = merge_vars(vars_in_term(T), vars_in_features(Fs,X)).
  209.  
  210. merge_vars(L1,L2) -> merge_ad(L1,no_redundant_ad(L2)).
  211.  
  212.  
  213.  
  214. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  215. %
  216. %   GENERIC ABSTRACT INTERPRETATION ALGORITHM
  217. %
  218. %   main source: 
  219. %       Experimental Evaluation of a Generic Abstract Interpretation
  220. %                       algorithm for Prolog
  221. %       B. Le Charlier and Pascal Van Hentenryck
  222. %       Tech. Report No CS-91.55  Brown University, DCS
  223. %
  224. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  225.  
  226.  
  227. % LOCAL PREDICATES:
  228. %
  229. % solve, solve_call, solve_procedure, solve_goal, solve_goals, solve_alter,
  230. %        init_solve 
  231. % extend, extend_node, compare_nodes, adjust, adjust_node, adjust_fathers,
  232. %         find_node 
  233. % suspend, un_suspend, not_suspended
  234. % ext_dp, add_dp, remove_dp, dp_member, not_dp_member
  235. % set_sat, lub_out
  236. %
  237.  
  238. % EXTERNAL PREDICATES (defined w.r.t. an abstract domain and a data structure)
  239. %
  240. % 'U', more_gen_than, equ, less_general_than
  241. % ai_unif
  242. % extc, restrc, extg, restrg
  243. %
  244. op(450,xfy,'U') ?
  245. op(670,xfy,more_general_than)?
  246. op(670,xfy,equ)?
  247. op(670,xfy,less_general_than)?
  248.  
  249. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  250. %
  251. % GENERIC ABSTRACT INTERPRETATION 
  252. %
  253. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  254.  
  255. solve( BetaIn, PName) :-
  256.     init_solve(SAT),
  257.     solve_call( BetaIn, PName, SAT, AT).
  258.  
  259.  
  260. solve_call( BetaIn, PName, SAT, AbsTuple) :-
  261.     extend(BetaIn, PName, SAT) = @(SAT,AbsTuple,New),
  262.     (
  263.         not_suspended( AbsTuple) and not_dp_member( AbsTuple),
  264.         !,
  265.         set_sat(SAT),
  266.         repeat,
  267.         (
  268.         ext_dp(AbsTuple2:find_node(BetaIn,PName,SAT2:sat)),
  269.         suspend(AbsTuple2),
  270.         solve_procedure( AbsTuple2, SAT2, PName, BetaOut),
  271.         @(SAT2,Modified,AbsTuple3) = 
  272.                      adjust(BetaIn,PName,BetaOut,SAT2),
  273.         remove_dp(Modified,SAT2),
  274.         set_sat(SAT2)
  275.         ),
  276.         dp_member(AbsTuple3),
  277.         !,
  278.         AbsTuple <- AbsTuple3,
  279.         SAT <- SAT2,
  280.         un_suspend(AbsTuple);
  281.         succeed
  282.     ).
  283.  
  284. solve_procedure( AbsTuple:node(BetaIn), SAT, PName, BetaOut) :-
  285.     Proc:proc(PName),
  286.     BetaExt = extc(Proc,BetaIn),
  287.     nl,nl,write("enter solve_procedure ",PName," with ",BetaIn),
  288.     solve_goals( Proc.actions, BetaExt,SAT,PName,BetaIn,NewBetaExt),
  289.     BetaOut = restrc(Proc,NewBetaExt),
  290.     nl,nl,write("exit solve_procedure ",PName," with ",BetaOut).
  291.  
  292. solve_goals([],BetaExt,_,_,_,BetaExt) :- !.
  293. solve_goals([G1|Gs],BetaExt,SAT,PName,BetaIn,NewBetaExt) :-
  294.     BetaAux = restrg(G1,BetaExt),
  295.     solve_goal(G1,BetaAux,SAT,PName,BetaIn,BetaInt),
  296.     BetaExtInt = extg(G1,BetaExt,BetaInt),
  297.     solve_goals(Gs,BetaExtInt,SAT,PName,BetaIn,NewBetaExt).
  298.  
  299. solve_goal(unif(A,B),Beta1,SAT,PName,BetaIn,Beta2) :-
  300.     !, ai_unif(A,B,Beta1,Beta2).
  301.  
  302. solve_goal(G:abscall(QName),Beta1,SAT,PName,BetaIn,Beta2) :-
  303.     !,
  304.     nl,nl,write("enter solve_call ",QName," with ",Beta1),
  305.     solve_call( Beta1, QName, SAT, AbsTuple),
  306.     Beta2 = AbsTuple.2,
  307.     nl,nl,write("exit solve_call ",QName," with ",Beta2),
  308.     cond( dp_member(AbsTuple),
  309.           add_dp(BetaIn,PName,AbsTuple,SAT)).
  310.     
  311.     
  312. solve_goal(G:disjunc(Alt1,Alt2,global_vars => V),Beta1,SAT,PName,BetaIn,Beta2) :-
  313.     solve_alter(copy_term(alt(Alt1,global_vars => V)),
  314.                 Beta1,SAT,PName,BetaIn,Beta3),
  315.     solve_alter(copy_term(alt(Alt2,global_vars => V)),
  316.                 Beta1,SAT,PName,BetaIn,Beta4),
  317.     nl,nl, write("  first  alternative:",Beta3),
  318.     nl,nl, write("  second alternative:",Beta4),
  319.     Beta2 = Beta3 'U' Beta4,
  320.     nl,nl, write("  union             :",Beta2).
  321.     
  322. solve_alter(alt([]),Beta1,SAT,PName,BetaIn,bot) :- !.
  323. solve_alter(Alt:alt(Actions),Beta1,SAT,PName,BetaIn,Beta2) :-
  324.     nl,nl,write("enter solve_alter with ",Beta1),
  325.     BetaExt = extc(Alt,Beta1),
  326.     solve_goals(Actions,BetaExt,SAT,PName,BetaIn,NewBetaExt),
  327.     Beta2 = restrc(Alt,NewBetaExt),
  328.     nl,nl,write("exit solve_alter with ",Beta2).
  329.     
  330.     
  331.     
  332.     
  333. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  334. %
  335. % OPERATIONS ON SATs
  336. %
  337. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  338.  
  339. init_solve(SAT:hasse) :- 
  340.     setq(sat,SAT).                  % the first argument of state is a
  341.                     % hasse diagram whose features have the
  342.                     % names of the predicates encountered
  343.                     % so far.
  344.  
  345. %
  346. % EXTEND
  347. %
  348.  
  349. extend( Beta, PName, SAT) ->
  350.     @(SAT,NewNode,New)
  351.     |   cond( Top:(SAT.PName) :== @,
  352.           (
  353.           Top = [AT:node(Beta,bot,
  354.                      depend_on_me => [],
  355.                  fathers => [],
  356.                  sons => [],
  357.                  stable => false,
  358.                  suspended => false)],
  359.           NewNode = AT,
  360.           New = true
  361.           ),
  362.           extend_top(Top, Beta, NewNode, New)),
  363.     !.
  364.  
  365. extend_top( Top, Beta, NewNode, New) :- 
  366.         compare_nodes( Top, Beta, ENode,[],[],[],
  367.                    GTNodes,LTNodes,NCNodes),
  368.     (
  369.         ENode :== @,
  370.         !,
  371.         ( 
  372.         GTNodes :\== [],
  373.         !,
  374.         map_pred( GTNodes, extend_node( 2=>Beta,3=>NewNode,4=>New))
  375.         ;
  376.         (
  377.             Top <- [NewNode|NCNodes],
  378.             NewNode = node(Beta,lub_out(LTNodes),
  379.                            depend_on_me => [],
  380.                            fathers => [],
  381.                    sons => LTNodes,
  382.                    stable => false,
  383.                    suspended => false),
  384.             New = true,
  385.             map_pred(LTNodes,update_ex_top_sons(2=>NewNode))
  386.         )
  387.         )
  388.     ;
  389.         (
  390.         NewNode = ENode,
  391.         New = false
  392.         )
  393.     ).
  394.  
  395. extend_node(Node, Beta, NewNode, New) :- 
  396.         compare_nodes( NS:(Node.sons), Beta, ENode,[],[],[],
  397.                    GTNodes,LTNodes,NCNodes),
  398.     (
  399.         ENode :== @,
  400.         !,
  401.         ( 
  402.         GTNodes :\== [],
  403.         !,
  404.         map_pred( GTNodes, extend_node( 2=>Beta,3=>NewNode,4=>New))
  405.         ;
  406.         (
  407.             NS <- [NewNode|NCNodes],
  408.             NewNode = node(Beta,OldOut:{bot;@},
  409.                            depend_on_me => [],
  410.                            fathers => OldFathers:{[];@},
  411.                    sons => OldSons:{[];@},
  412.                    stable => false,
  413.                    suspended => false),
  414.             !,
  415.             New = true,
  416.             OldSons <- append(OldSons,LTNodes),
  417.             OldFathers <- [Node|fake_copy(OldFathers)],
  418.             OldOut <- OldOut 'U' lub_out(LTNodes),
  419.             map_pred(LTNodes,update_fathers(2=>NewNode,3=>Node))
  420.         )
  421.         )
  422.     ;
  423.         (
  424.         NewNode = ENode,
  425.         New = false
  426.         )
  427.     ).
  428.  
  429. update_fathers(Node,NewFatherNode,OldFatherNode) :-
  430.     NF:Node.Fathers <- [NewFatherNode|suppress_ad(NF,OldFatherNode)].
  431. update_ex_top_sons(Node,FatherNode) :-
  432.     Node.fathers <- [FatherNode].
  433.  
  434. % 
  435. % ADJUST
  436. %
  437.  
  438. adjust(BetaIn,PName,BetaOut,SAT) ->
  439.     @(SAT,Modified,AT)
  440.     |   adjust_node( AT:find_node(BetaIn,PName,SAT),BetaOut,[],Modified).
  441.  
  442.  
  443. adjust_node( Node:node(2=>BetaOut), NewBetaOut,L1,L2) :-
  444.     cond( NewBetaOut more_general_than BetaOut,
  445.           ( 
  446.           BetaOut <- NewBetaOut,
  447.           adjust_fathers(Node.fathers, NewBetaOut,[Node|L1],L2)
  448.           ),
  449.           L1 = L2 ).
  450.  
  451. adjust_fathers([],_,L,L) :- !.
  452. adjust_fathers([P1:node(2=>BetaOut)|Ps],NewBetaOut,L1,L3) :- 
  453.     adjust_node(P1,BetaOut 'U' NewBetaOut,L1,L2),
  454.     adjust_fathers(Ps,NewBetaOut,L2,L3).
  455.  
  456.  
  457. compare_nodes([],_,_,GT,LT,NC,GT,LT,NC) :- !.
  458. compare_nodes( [N1:node(BetaIn1)|Ns],Beta,E,GT1,LT1,NC1,GT3,LT3,NC3) :-
  459.     cond( Beta equ BetaIn1,
  460.           E = N1,
  461.           (
  462.           cond( BetaIn1 more_general_than Beta,
  463.                 (
  464.                 GT2 = [N1|GT1],
  465.                 LT2 = LT1,
  466.                 NC2 = NC1
  467.             ),
  468.             cond( BetaIn1 less_general_than Beta,
  469.                   (
  470.                   GT2 = GT1,
  471.                   LT2 = [N1|LT1],
  472.                   NC2 = NC1
  473.                   ),
  474.                   (
  475.                   GT2 = GT1,
  476.                   LT2 = LT1,
  477.                   NC2 = [N1|NC1]
  478.                   ))),
  479.                   compare_nodes(Ns,Beta,E,GT2,LT2,NC2,GT3,LT3,NC3)
  480.           )).
  481.  
  482. %
  483. % FIND_NODE
  484. %
  485.  
  486. find_node( Beta, PName, SAT) -> find_node_in_list(SAT.PName, Beta).
  487.  
  488. find_node_in_list([], Beta) -> false.
  489. find_node_in_list([N1:node(BetaIn1)|Ns],Beta) ->
  490.     Node
  491.     |   cond( Beta equ BetaIn1,
  492.           Node = N1,
  493.           cond( BetaIn1 more_general_than Beta,
  494.                 Node = find_node_in_list(N1.sons,Beta),
  495.             Node = find_node_in_list(Ns,Beta))).
  496.  
  497. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  498. %
  499. % OPERATIONS ON DEPENDENCIES
  500. %
  501. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  502.  
  503. ext_dp(AbsTuple) :-
  504.     AbsTuple.stable <- true.
  505.  
  506. add_dp(BetaIn,PName,AbsTuple,SAT) :-
  507.     AbsTuple2 = find_node( BetaIn, PName, SAT),
  508.     ATD:(AbsTuple.depend_on_me) <- [AbsTuple2|fake_copy(ATD)],
  509.     AbsTuple2.stable <- true.
  510.  
  511. remove_dp([],SAT) :- !.
  512. remove_dp([AT1|ATs],SAT) :-
  513.     map_pred(DP:(AT1.depend_on_me),stabilize),
  514.     DP <- [],
  515.     remove_dp(ATs,SAT).
  516.     
  517.  
  518. dp_member(node(stable => S)) -> S.
  519. not_dp_member(node(stable => S)) -> not(S).
  520.  
  521. stabilize(node(stable => S)) :- S <- false.
  522.  
  523. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  524. %
  525. % OPERATIONS ON SUSPENDED TUPLES
  526. %
  527. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  528.  
  529. suspend(AbsTuple) :- AbsTuple.suspended <- true.
  530. un_suspend(AbsTuple) :- AbsTuple.suspended <- false.
  531. not_suspended(node(suspended => B)) -> not(B).
  532.  
  533. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  534. %
  535. % MISC
  536. %
  537. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  538.  
  539. %
  540. % LEAST UPPER BOUND OF A LIST OF ELEMENTS
  541. %
  542.  
  543. lub_out ([]) -> bot.
  544. lub_out([node(2 => Beta)|Nodes]) -> lub_out(Nodes) 'U' Beta.
  545.  
  546. %
  547. % set_state
  548. %
  549.  
  550. set_sat(SAT) :- 
  551.     retract((sat -> @)),
  552.     asserta(( sat -> SAT)).
  553.  
  554.  
  555. %
  556. % proc
  557. %
  558.  
  559. proc(X) -> str2psi(strcon(psi2str(X),"_proc")).
  560.  
  561.  
  562. any <| free.
  563. any <| non_var.
  564. non_var <| ground.
  565.  
  566. bot -> @.
  567.  
  568.  
  569. A more_general_than B -> A :< B.
  570. A less_general_than B -> A :> B.
  571. A equ B -> A :== B.
  572.  
  573. % A 'U' B -> root_sort(A)&root_sort(B).
  574.  
  575.  
  576. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  577. %
  578. %   SIMPLE DOMAIN FOR THE GENERIC ABSTRACT INTERPRETATION ALGORITHM
  579. %
  580. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  581. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  582. %
  583. % LATTICE 
  584. %
  585. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  586. %
  587. %                    any                    
  588. %             free        non-var
  589. %                               ground            
  590. %                   bottom
  591. %
  592.  
  593. any <| free.
  594. any <| non_var.
  595. non_var <| ground.
  596.  
  597. bot -> @.
  598.  
  599. %
  600. % OPERATIONS ON THE LATTICE
  601. %
  602.  
  603. op( 670 ,xfy, less_general_or_equ ) ?
  604. op( 670, xfy, more_general_or_equ ) ?
  605. op( 670, xfy, more_general_list_than ) ?
  606. op( 670, xfy, less_general_list_than ) ?
  607. op( 670, xfy, equ_list ) ?
  608. op( 450, xfy, 'Ulist') ?
  609.  
  610. X more_general_than Y ->
  611.     cond( Y :== @,
  612.           true,
  613.           X more_general_list_than Y ).
  614.  
  615.  
  616. X less_general_than Y ->
  617.     cond( Y :== @,
  618.           false,
  619.           X less_general_list_than Y ).
  620.  
  621. X equ Y ->
  622.     cond( Y :== @,
  623.           X :== @,
  624.           X equ_list Y ).
  625.  
  626.  
  627.  
  628.  
  629.  
  630. [A|B] more_general_list_than [C|D] ->
  631.     cond( A :< C,
  632.           B more_general_or_equ D,
  633.           cond( A :== C,
  634.                 B more_general_list_than D,
  635.             false )).
  636.  
  637. [] more_general_list_than [] -> false.
  638.  
  639.  
  640. [A|B] more_general_or_equ [C|D] ->
  641.     cond( A :=< C,
  642.           B more_general_or_equ D,
  643.           false ).
  644.  
  645. [] more_general_or_equ [] -> true.
  646.  
  647. [A|B] less_general_list_than [C|D] ->
  648.     cond( A :> C,
  649.           B less_general_or_equ D,
  650.           cond( A :== C,
  651.                 B less_general_list_than D,
  652.             false )).
  653.  
  654.  
  655. [] less_general_list_than [] -> false.
  656.  
  657. [A|B] less_general_or_equ [C|D] ->
  658.     cond( A :>= C,
  659.           B less_general_or_equ D,
  660.           false ).
  661.  
  662. [] less_general_or_equ [] -> true.
  663.  
  664. [A|B] equ_list [C|D] ->
  665.     cond( A :== C,
  666.           B equ_list D,
  667.           false ).
  668.  
  669. [] equ_list [] -> true.
  670.           
  671. X 'U' Y ->
  672.     cond( X :== @ or Y :== @,
  673.           copy_term(X&Y),
  674.           X 'Ulist' Y).
  675. [] 'Ulist' [] -> [].
  676. [A|B] 'Ulist' [C|D] -> [root_sort(A)&root_sort(C)| B 'U' D].
  677.  
  678. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  679. %
  680. % UNIFICATION
  681. %
  682. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  683. %
  684. % hierarchy used for unification
  685. % 
  686.  
  687. ground2 <| non_var_false.
  688. non_var_false <| non_var_true.
  689. non_var_false <| any2.
  690. non_var_true <| free2.
  691. any2 <| free2.
  692.  
  693. bottom2 <| ground2.
  694.  
  695. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  696. %
  697. % CORRESPONDENCES BETWEEN THE TWO LATTICES
  698. %
  699. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  700.  
  701.  
  702. var2pat(@(type=>T)) ->
  703.     TT
  704.     |   cond( T :< free2,
  705.           cond( T :== any2,
  706.                 TT = any,
  707.                 cond( T:< non_var_false,
  708.               cond( T:< ground2,
  709.                     TT = @,
  710.                 TT = ground),
  711.               TT = non_var)),
  712.           TT = free).
  713.  
  714.  
  715. pat2var(T) ->
  716.     @(type=>TT) 
  717.     |   cond( T:== @,
  718.           TT = bottom2,
  719.           cond( T :== free,
  720.                     TT = free2,
  721.             cond( T:< ground,
  722.                       cond( T:< non_var,
  723.                         TT = any2,
  724.                 TT = non_var_false ),
  725.               TT = ground2))).
  726.  
  727.  
  728. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  729. %
  730. %  normalisation des variables... avec des coreferences, cela devient
  731. %  problematique (calcul de point fixe). Pour le moment la normalisation est
  732. %  correcte mais pas optimale.
  733. %
  734. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  735.  
  736.  
  737. % Une bonne normalisation consisterait a ajouter a chaque element un attribut
  738. % 1 (en decalant les autres arguments) qui represente le type de l'objet. Ce
  739. % serait fait dans une premiere phase de reecriture du programme.
  740.  
  741. normalize(X:@(type=>T),parents => P:{[];@}) :-
  742.     !,
  743.     cond( T :== bottom2,
  744.           bottomize(P),
  745.     cond( F:features(X)=[type],
  746.               cond( root_sort(X) :< @,
  747.                 T = ground2,
  748.                 T = free2),
  749.           (
  750.           T = non_var_true,
  751.           norm_features(F,T,[X|P],T1),
  752.           T = T1
  753.           ))).
  754.  
  755. norm_features([],_,_,ground2) :- !.
  756. norm_features([type|Feats],T,Parents,T1) :- 
  757.     !, norm_features(Feats,T,Parents,T1).
  758. norm_features([Feat|Feats],T,Parents:[X|P],T1) :- 
  759.     cond( member_ad(Parents,Y:(X.Feat)),              % occur-check
  760.           (
  761.           norm_features(Feats,T,Parents,T3),
  762.           T1 = up_feature(Y.type,T3)
  763.           ),
  764.           ( 
  765.           norm_feature(Y,T,T2,Parents),
  766.           norm_features(Feats,T,Parents,T3),
  767.           T1 = up_feature(T2,T3)
  768.           )).
  769.  
  770. norm_feature(X:@(type=>T2),T,T2,Parents) :-      % propagation descendante 
  771.     cond( T :== non_var_false,
  772.           T2 =  any2,
  773.           cond( T :== any2,
  774.                 ( T = non_var_false, T2 = any2 ),
  775.             cond( T :== ground2,
  776.                   T2 = ground2))),
  777.     normalize(X,parents=>Parents).
  778.  
  779. up_feature(X:ground2,Y:ground2) -> root_sort(X)&root_sort(Y).
  780.  
  781. bottomize([]) :- !.
  782. bottomize([A|B]) :-
  783.     A.type <- bottom2,
  784.     bottomize(B).
  785.  
  786.  
  787.  
  788. normalize_list([]) -> [].
  789. normalize_list([A|B]) ->
  790.     [A|normalize_list(B)]
  791.     |   normalize(A).
  792.     
  793.  
  794. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  795. %
  796. % DEFINITION OF THE PREDICATES NEEDED BY THE GENERIC ANALYSER
  797. %
  798. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  799. %
  800. % ai_unif
  801. %
  802.  
  803.  
  804. ai_unif(A,B,_,_) :-
  805.     normalize(A&B).
  806.  
  807. %
  808. % extc, restrc
  809. %
  810.     
  811.  
  812. extc(Proc,BetaIn) ->
  813.     BetaIn
  814.     |   Proc.global_vars = map(pat2var,BetaIn).
  815.  
  816. restrc(Proc,_) -> 
  817.     map(var2pat,normalize_list(Proc.global_vars)).
  818.  
  819. %
  820. % restrg
  821. %
  822.  
  823. restrg(abscall(PName,Vars),_) ->
  824.     map(var2pat,Vars).
  825. restrg(disjunc(global_vars => Vars),_) -> 
  826.     map(var2pat,Vars).
  827. restrg(unif,_) -> @.
  828.  
  829. extg(abscall(PName,Vars),_,BetaInt) ->
  830.     cond( BetaInt :< list,
  831.               (
  832.           BetaInt | Vars = map(pat2var, BetaInt)
  833.           ),
  834.           (
  835.           BetaInt | bottomize(Vars)
  836.           )).
  837.  
  838.  
  839. extg(disjunc(global_vars => Vars),_,BetaInt) ->
  840.     BetaInt
  841.     |   Vars = map(pat2var, BetaInt).
  842.  
  843. extg(unif,_,_) -> @.
  844.