gr: simple groundness (abstract domain)

Usage:unknown_entry(Sg,Qv,Call)

Gives the top value for the variables involved in a literal whose definition is not present, and adds this top value to Call. In this domain the top value is X/any forall X in the set of variables.

• The following properties should hold at call time:
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Qv is a list.
  (term/1)Call is any term.
• The following properties should hold upon exit:
  (asub/1)Call is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form unknown_entry(Sg,Qv,Call) do not fail.
  (is_det/1)All calls of the form unknown_entry(Sg,Qv,Call) are deterministic.

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 the empty value is equivalent to the unknown value.

• 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.
  (term/1)Entry is any term.
• The following properties should hold upon exit:
  (nonvar/1)Entry is currently a term which is not a free variable.
  (asub/1)Entry is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form empty_entry(Sg,Vars,Entry) do not fail.
  (is_det/1)All calls of the form empty_entry(Sg,Vars,Entry) are deterministic.

Usage:abs_sort(Asub,Asub_s)

It sorts the set of X/Value in Asub obtaining Asub_s.

• The following properties should hold at call time:
  (nonvar/1)Asub is currently a term which is not a free variable.
  (asub/1)Asub is a well-formed abstract substitution of the gr domain.
• The following properties should hold upon exit:
  (nonvar/1)Asub_s is currently a term which is not a free variable.
  (asub/1)Asub_s is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form abs_sort(Asub,Asub_s) do not fail.
  (is_det/1)All calls of the form abs_sort(Asub,Asub_s) are deterministic.

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

Proj is the result of eliminating from Asub all X/Value such that X is not in Vars. HvFv_u may be a list or 'not_provided_HvFv_u'. This predicate may be used with Proj instantiated, see call_to_success_builtin/6.

• 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.
  (term/1)Sg is any term.
  (list/1)Vars is a list.
  (term/1)HvFv_u is any term.
  (asub/1)Asub is a well-formed abstract substitution of the gr domain.
  (term/1)Proj is any term.
• The following properties should hold upon exit:
  (asub/1)Proj is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form project(Sg,Vars,HvFv_u,Asub,Proj) do not fail.
  (is_det/1)All calls of the form project(Sg,Vars,HvFv_u,Asub,Proj) are deterministic.

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 + Fv. This is done as follows:

• If Sg and Head are identical up to renaming it is just renaming Proj and adding the Fv.
• If Hv = [], Entry is just adding the Fv.
• Otherwise, it will
  • obtain in Binds the primitive equations corresponding to Sg = Head.
  • add to Proj the variables in Hv as not ground in Temp1.
  • update Temp1, grounding some variables obtaining Temp2.
  • insert Fv in Temp2 as any obtaining Temp3.
  • projects Temp3 onto Hv + Fv obtaining Entry.

• Sv is a list of subgoal variables.
• Sg is the subgoal being analysed.
• Head is the Head of the clause being analysed.
• Fv is a list of free variables in the body of the clause being considered.
• Proj is the abstract substitution Call projected onto Sv.
• Entry is the Abstract entry substitution (i.e. the abstract subtitution obtained after the abstract unification of Sg and Head projected onto Hv + Fv).
• ExtraInfo Info computed during the call_to_entry/9 that can be reused during the exit_to_prime/7 step.

• 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.
  (list/1)Sv is a list.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Hv is a list.
  (cgoal/1)Head is a term which represents a goal, i.e., an atom or a structure.
  (term/1)K is any term.
  (list/1)Fv is a list.
  (asub/1)Proj is a well-formed abstract substitution of the gr domain.
• 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.
  (asub/1)Entry is a well-formed abstract substitution of the gr domain.
  (extrainfo/1)ExtraInfo is a par (asub/1,binds/1).
• The following properties should hold globally:
  (not_fails/1)All the calls of the form call_to_entry(Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo) do not fail.
  (is_det/1)All calls of the form call_to_entry(Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo) are deterministic.

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 renaming Exit.
• If Hv = [], Prime = { X/g| forall X in Sv }
• Otherwise: it will
  • obtain the primitive equations corresponding to Sg=Head from Extrainfo.
  • projects Exit onto Hv obtaining BPrime.
  • merge Proj from Extrainfo and BPrime obtaining TempPrime.
  • update TempPrime, grounding some variables obtaining NewTempPrime.
  • projects NewTempPrime onto Sv obtaining Prime.

• 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.
  (term/1)Sg is any term.
  (list/1)Hv is a list.
  (cgoal/1)Head is a term which represents a goal, i.e., an atom or a structure.
  (cgoal/1)Sv is a term which represents a goal, i.e., an atom or a structure.
  (asub/1)Exit is a well-formed abstract substitution of the gr domain.
  (term/1)ExtraInfo is any term.
  (term/1)Prime is any term.
• The following properties should hold upon exit:
  (nonvar/1)Prime is currently a term which is not a free variable.
  (extrainfo/1)ExtraInfo is a par (asub/1,binds/1).
  (asub/1)Prime is a well-formed abstract substitution of the gr domain.

Usage:compute_lub(ListASub,Lub)

It computes the least upper bound of a set of abstract substitutions. For each two abstract substitutions ASub1 and ASub2 in ListASub, obtaining the lub is just:

foreach X/Value1 in ASub1 and X/Value2 in ASub2:

• if Value1 == Value2, X/Value1 in Lub.
• otherwise, X/any in Lub.

• The following properties should hold at call time:
  (nonvar/1)ListASub is currently a term which is not a free variable.
  (list/2)ListASub is a list of asubs.
• The following properties should hold upon exit:
  (nonvar/1)Lub is currently a term which is not a free variable.
  (asub/1)Lub is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form compute_lub(ListASub,Lub) do not fail.
  (is_det/1)All calls of the form compute_lub(ListASub,Lub) are deterministic.

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

If Prime = $bottom, Succ = $bottom. If Sv = [], Call = Succ. Otherwise, Succ is computed updating the values of Call with those in Prime.

• 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.
  (term/1)Sg is any term.
  (asub/1)Prime is a well-formed abstract substitution of the gr domain.
  (list/1)Sv is a list.
  (asub/1)Call is a well-formed abstract substitution of the gr domain.
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.
  (asub/1)Succ is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form extend(Sg,Prime,Sv,Call,Succ) do not fail.
  (is_det/1)All calls of the form extend(Sg,Prime,Sv,Call,Succ) are deterministic.

Usage:call_to_success_fact(Sg,Hv,Head,K,Sv,Call,Proj,Prime,Succ)

Specialized version of call_to_entry/9 + exit_to_prime/7 + extend/5 for facts.

• 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)K 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.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Hv is a list.
  (cgoal/1)Head is a term which represents a goal, i.e., an atom or a structure.
  (term/1)K is any term.
  (list/1)Sv is a list.
  (asub/1)Call is a well-formed abstract substitution of the gr domain.
  (asub/1)Proj is a well-formed abstract substitution of the gr domain.
  (term/1)Prime is any term.
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (nonvar/1)Prime is currently a term which is not a free variable.
  (nonvar/1)Succ is currently a term which is not a free variable.
  (asub/1)Prime is a well-formed abstract substitution of the gr domain.
  (asub/1)Succ is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form call_to_success_fact(Sg,Hv,Head,K,Sv,Call,Proj,Prime,Succ) do not fail.
  (is_det/1)All calls of the form call_to_success_fact(Sg,Hv,Head,K,Sv,Call,Proj,Prime,Succ) are deterministic.

Usage:special_builtin(Pred,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:

• new_ground if the builtin makes all variables ground whithout imposing any condition on the previous freeness values of the variables.
• old_ground if the builtin requires the variables to be ground.
• old_new_ground if the builtin requires some variables to be ground and grounds the rest.
• 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)Pred 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.
  (term/1)Pred is any term.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (term/1)Subgoal is any term.
  (term/1)Type is any term.
  (term/1)Condvars is any term.

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

Obtains the success for some particular builtins:

• If Type = new_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.
• If Type = old_ground, if grounds all variables in Sv and checks that no free variables has becomed ground.
• If Type = old_ground, if grounds all variables in OldG and checks that no free variables has becomed ground. If so, it grounds all variables in NewG.
• 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)HvFv_u is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
  (atm/1)Type is an atom.
  (list/1)Sv_u is a list.
  (term/1)Condv is any term.
  (list/1)HvFv_u is a list.
  (asub/1)Call is a well-formed abstract substitution of the gr domain.
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.
  (asub/1)Succ is a well-formed abstract substitution of the gr domain.

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

Handles those builtins for which computing Proj 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.
  (atm/1)SgKey is an atom.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Sv is a list.
  (asub/1)Call is a well-formed abstract substitution of the gr domain.
  (asub/1)Proj is a well-formed abstract substitution of the gr domain.
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.

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

Obtains the abstract substitution for gr from the native properties found in the user supplied info.

• 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.
  (term/1)InputUser is any term.
  (list/1)Qv is a list.
  (term/1)ASub is any term.
  (term/1)Sg is any term.
  (term/1)MaybeCallASub is any term.
• The following properties should hold upon exit:
  (nonvar/1)ASub is currently a term which is not a free variable.
  (asub/1)ASub is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form input_user_interface(InputUser,Qv,ASub,Sg,MaybeCallASub) do not fail.
  (is_det/1)All calls of the form input_user_interface(InputUser,Qv,ASub,Sg,MaybeCallASub) are deterministic.

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

The user friendly format consists in extracting the ground variables and the nonground 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.
  (asub/1)ASub is a well-formed abstract substitution of the gr domain.
  (list/1)Qv is a list.
  (term/1)OutFlag is any term.
  (term/1)ASub_user is any term.
  (term/1)Comps is any term.
• 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:unknown_call(Sg,Vars,Call,Succ)

Gives the top value for the variables involved in a literal whose definition is not present, and adds this top value to Call.

• 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.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Vars is a list.
  (asub/1)Call is a well-formed abstract substitution of the gr domain.
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.
  (asub/1)Succ is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form unknown_call(Sg,Vars,Call,Succ) do not fail.
  (is_det/1)All calls of the form unknown_call(Sg,Vars,Call,Succ) are deterministic.

Usage:less_or_equal(ASub0,ASub1)

Succeeds if ASub1 is more general or equal to ASub0. It's assumed the two abstract substitutions are defined on the same variables.

• 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.
  (asub/1)ASub0 is a well-formed abstract substitution of the gr domain.
  (asub/1)ASub1 is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (is_det/1)All calls of the form less_or_equal(ASub0,ASub1) are deterministic.

Usage:glb(ASub0,ASub1,Glb)

Glb is the great lower bound of ASub0 and ASub1.

• 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.
  (asub/1)ASub0 is a well-formed abstract substitution of the gr domain.
  (asub/1)ASub1 is a well-formed abstract substitution of the gr domain.
  (term/1)Glb is any term.
• The following properties should hold upon exit:
  (nonvar/1)Glb is currently a term which is not a free variable.
  (asub/1)Glb is a well-formed abstract substitution of the gr domain.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form glb(ASub0,ASub1,Glb) do not fail.
  (is_det/1)All calls of the form glb(ASub0,ASub1,Glb) are deterministic.

Usage:asub(A)

A is a well-formed abstract substitution of the gr domain.

Usage:asub_elem(E)

E is a single substitution.

Usage:gr_mode(M)

M is g (ground), ng (nonground), or any.

Usage:extrainfo(E)

E is a par (asub/1,binds/1).

Usage:binds(B)

B is a list of bindings.

Usage:binding(B)

B is a triple (X,Term,Vars), where X is a variable, Term is a term and Vars is the set of variables in Term.