share: sharing (abstract domain)

Usage:project(Sg,Vars,HvFv_u,ASub,Proj)

Eliminates from each element of the list of lists of variables given as second argument any variable which is not an element of the first argument. Both ordered. i.e. Proj = { Ys | Xs in ASub, Ys = Xs intersect Vars }

• The following properties should hold at call time:
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Vars is currently a term which is not a free variable.
  (nonvar/1)HvFv_u is currently a term which is not a free variable.
  (nonvar/1)ASub is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Proj is currently a term which is not a free variable.

Usage:call_to_entry(Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo)

It obtains the abstract substitution (Entry) which results from adding the abstraction of the Sg = Head to Proj, later projecting the resulting substitution onto Hv. This is done as follows:

• If Sg and Head are identical up to renaming it is just a question or renaming Proj and adding the Fv as singletons.
• If Hv = [], Entry is just the Fv as singletons.
• Otherwise, it will
  • obtain Gv1 (ground variables in Sv due to Proj).
  • obtain Binds (sorted list of primitive equations corresponding to the equation Sg = Head).
  • obtain Gv2 (variables in Sv or Hv involved in a primitive equation with a ground term).
  • propagate the groundnes of Gv1 and Gv2 to Proj through Binds obtaining NewBinds (grounding bindings eliminated) NewProj (ground variables eliinated) Gv (final set of ground variables) GvSv and GvHv (subset of vars in Gv belonging to Sg and Head respectively).
  • then it obtains Partition (the transitive closure of due to the sharing established by NewProj) and H_partition (Partition projected onto the Hv variables).
  • then it obtains in ShareArgsStar the star of the sharing among the arguments of Sg established by NewProj, and in Head_args the set of variables belonging to each argument of Head.
  • Then the idea is to obtain Entry by computing the powerset of each equivalence class in H_partition and eliminating those sets in the powerset which are not allowed (they would imply sharing among arguments in the head while there is no sharing among those arguments in ShareArgsStar).

• The following properties should hold at call time:
  (nonvar/1)Sv is currently a term which is not a free variable.
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Hv is currently a term which is not a free variable.
  (nonvar/1)Head is currently a term which is not a free variable.
  (nonvar/1)K is currently a term which is not a free variable.
  (nonvar/1)Fv is currently a term which is not a free variable.
  (nonvar/1)Proj is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Entry is currently a term which is not a free variable.
  (nonvar/1)ExtraInfo is currently a term which is not a free variable.

Usage:exit_to_prime(Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime)

It computes the prime abstract substitution Prime, i.e. the result of going from the abstract substitution over the head variables (Exit), to the abstract substitution over the variables in the subgoal. It will:

• If Exit is $bottom, Prime will be also $bottom.
• If Flag = yes (Head and Sg identical up to renaming) it is just a question or renaming Exit.
• If Hv = [], Prime = [].
• Otherwise, it will:
  • project Exit onto Hv obtaining BPrime.
  • subtract from Hv those vars which were ground due to the equation Head = Sg (Gv) obtaining Hv_rem.
  • obtain the vars Hv_rem which had becomed ground after the of the clause (NewGv_Hv).
  • Then if NewGv_Hv is == [], groundness must be propagated to obtain ASub.
  • Otherwise, ASub is just equal to NewProj.
  • Then Prime is obtained by obtaining New_partition (transitive closure of the sharing specified in BPrime) and performing the same kind of prunning that in the call_to_entry but in the opposite direction.

• The following properties should hold at call time:
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Hv is currently a term which is not a free variable.
  (nonvar/1)Head is currently a term which is not a free variable.
  (nonvar/1)Sv is currently a term which is not a free variable.
  (nonvar/1)Exit is currently a term which is not a free variable.
  (nonvar/1)ExtraInfo is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Prime is currently a term which is not a free variable.

Usage:abs_sort(Asub,Asub_s)

sorts the set of set of variables ASub to obtaint the Asub_s.

• The following properties should hold at call time:
  (nonvar/1)Asub is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Asub_s is currently a term which is not a free variable.

Usage:compute_lub(ListASub,Lub)

It computes the lub of a set of Asub. For each two abstract substitutions ASub1 and ASub2 in ListASub, obtaining the lub is just merging the ASub1 and ASub2.

• The following properties should hold at call time:
  (nonvar/1)ListASub is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Lub is currently a term which is not a free variable.

Usage:glb(ASub0,ASub1,Lub)

Glb is just intersection.

• The following properties should hold at call time:
  (nonvar/1)ASub0 is currently a term which is not a free variable.
  (nonvar/1)ASub1 is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Lub is currently a term which is not a free variable.

Usage:extend(Sg,Prime,Sv,Call,Succ)

If Prime = bottom, Succ = bottom. If Sv = [], Call = Succ. Otherwise, it splits Call into two sets of sets: Intersect (those sets containing at least a variabe in Sv) and Disjunct (the rest). Then is obtains in Star the closure under union of Intersect. Finally, it prunes Star with the information in Prime adding, at the end, Disjunct.

• The following properties should hold at call time:
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Prime is currently a term which is not a free variable.
  (nonvar/1)Sv is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.

Usage:

Specialized version of call_to_entry + exit_to_prime + extend for facts

Usage:pos(Xss,Arg,Xs,ArgShare)

Xss is a list containing in each Set_i the variables in the i-th arg of the Term. Arg is the number of the current arg. Xs is a sorted list of variables. It will obtain ArgShare, the set of arguments in at least one variable in Xs appears.

• The following properties should hold at call time:
  (nonvar/1)Xss is currently a term which is not a free variable.
  (nonvar/1)Arg is currently a term which is not a free variable.
  (nonvar/1)Xs is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)ArgShare is currently a term which is not a free variable.

Usage:script_p_star(Atom,ASub,ShareArgsStar)

It first obtains in ArgSare_info the set of sets of argument numbers of Atom each one corresponding to each set in ASub. Then it obtains the closure under union.

• The following properties should hold at call time:
  (nonvar/1)Atom is currently a term which is not a free variable.
  (nonvar/1)ASub is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)ShareArgsStar is currently a term which is not a free variable.

Usage:unknown_entry(Sg,Qv,Call)

The top value in Sharing for a set of variables is the powerset.

• The following properties should hold at call time:
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Qv is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Call is currently a term which is not a free variable.

Usage:empty_entry(Sg,Vars,Entry)

Gives the empty value in this domain for a given set of variables Vars, resulting in the abstract substitution Entry. I.e., obtains the abstraction of a substitution in which all variables Vars are unbound: free and unaliased. In this domain is the list of singleton lists of variables.

• The following properties should hold at call time:
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Vars is currently a term which is not a free variable.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Vars is a list.
  (absu/1)Entry is an abstract substitution
• The following properties should hold upon exit:
  (nonvar/1)Entry is currently a term which is not a free variable.

Usage:asub_to_native(ASub,Qv,OutFlag,ASub_user,Comps)

The user friendly format consists in extracting the ground variables.

• The following properties should hold at call time:
  (nonvar/1)ASub is currently a term which is not a free variable.
  (nonvar/1)Qv is currently a term which is not a free variable.
  (nonvar/1)OutFlag is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)ASub_user is currently a term which is not a free variable.
  (nonvar/1)Comps is currently a term which is not a free variable.

Usage:input_user_interface(InputUser,Qv,ASub,Sg,MaybeCallASub)

Obtaining the abstract substitution for Sharing from the user supplied information just consists in taking the mshare(Sharing) element of InputUser and sorting it. If there is no such element, get the top sharing for the variables involved.

• The following properties should hold at call time:
  (nonvar/1)Qv is currently a term which is not a free variable.
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)MaybeCallASub is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)ASub is currently a term which is not a free variable.

Usage:unknown_call(Sg,Vars,Call,Succ)

Obtained by selecting those sets in Call for which at least a variable in Vars appears, making the star of those sets, and adding the sets with empty intersection with Vars.

• The following properties should hold at call time:
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Vars is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.

Usage:less_or_equal(ASub0,ASub1)

Succeeds if ASub1 is more general or equal to ASub0.

• The following properties should hold at call time:
  (nonvar/1)ASub0 is currently a term which is not a free variable.
  (nonvar/1)ASub1 is currently a term which is not a free variable.

Usage:special_builtin(SgKey,Sg,Subgoal,Type,Condvars)

Satisfied if the builtin does not need a very complex action. It divides builtins into groups determined by the flag returned in the second argument + some special handling for some builtins:

• ground : if the builtin makes all variables ground whithout imposing any condition on the previous freeness values of the variables.
• bottom : if the abstract execution of the builtin returns bottom*.
• unchanged : if we cannot infer anything from the builtin, the substitution remains unchanged and there are no conditions imposed on the previous freeness values of the variables.
• some : if it makes some variables ground without imposing conditions.
• Sgkey : special handling of some particular builtins.

• The following properties should hold at call time:
  (nonvar/1)SgKey is currently a term which is not a free variable.
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Subgoal is currently a term which is not a free variable.
  (var/1)Condvars is a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Type is currently a term which is not a free variable.

Usage:success_builtin(Type,Sv_u,Condv,HvFv_u,Call,Succ)

Obtains the success for some particular builtins:

• If Type = ground, it updates Call making all vars in Sv_u ground.
• If Type = bottom, Succ = $bottom.
• If Type = unchanged, Succ = Call.
• If Type = some, it updates Call making all vars in Condv ground.
• Otherwise Type is the SgKey of a particular builtin for each the Succ is computed.

• The following properties should hold at call time:
  (nonvar/1)Type is currently a term which is not a free variable.
  (nonvar/1)Sv_u is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.

Usage:call_to_success_builtin(SgKey,Sg,Sv,Call,Proj,Succ)

Handles those builtins for which computing Prime is easier than Succ.

• The following properties should hold at call time:
  (nonvar/1)SgKey is currently a term which is not a free variable.
  (nonvar/1)Sg is currently a term which is not a free variable.
  (nonvar/1)Sv is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
  (nonvar/1)Proj is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.