Simple groundness abstract domain

Usage:gr_call_to_entry(Sv,Sg,Hv,Head,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 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

The meaning of the variables is

• 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 that can be reused during the exit_to_prime 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)Fv is currently a term which is not a free variable.
  (nonvar/1)Proj is currently a term which is not a free variable.
  (var/1)Entry is a free variable.
  (var/1)ExtraInfo is a free variable.
  (list/1)Sv is a list.
  (callable/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Hv is a list.
  (callable/1)Head is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Fv is a list.
  (absu/1)Proj is an abstract substitution
  (absu/1)Entry is an abstract substitution
  (extrainfo/1)ExtraInfo is a par (absu,binds)

Usage:gr_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.
  (var/1)ExtraInfo is a free variable.
  (var/1)Prime is a free variable.
  (list/1)Sg is a list.
  (list/1)Hv is a list.
  (callable/1)Head is a term which represents a goal, i.e., an atom or a structure.
  (callable/1)Sv is a term which represents a goal, i.e., an atom or a structure.
  (absu/1)Exit is an abstract substitution
  (extrainfo/1)ExtraInfo is a par (absu,binds)
  (absu/1)Prime is an abstract substitution

Usage:gr_project(Asub,Vars,Proj)

Proj is the result of eliminating from Asub all X/Value such that X is not in Vars

• The following properties should hold at call time:
  (nonvar/1)Asub is currently a term which is not a free variable.
  (nonvar/1)Vars is currently a term which is not a free variable.
  (var/1)Proj is a free variable.
  (absu/1)Asub is an abstract substitution
  (list/1)Vars is a list.
  (absu/1)Proj is an abstract substitution

Usage:gr_extend(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)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.
  (var/1)Succ is a free variable.
  (absu/1)Prime is an abstract substitution
  (list/1)Sv is a list.
  (absu/1)Call is an abstract substitution
  (absu/1)Succ is an abstract substitution

Usage:gr_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.
  (var/1)Lub is a free variable.
  (list/2)ListASub is a list of absus.
  (absu/1)Lub is an abstract substitution

Usage:gr_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.
  (var/1)Glb is a free variable.
  (absu/1)ASub0 is an abstract substitution
  (absu/1)ASub1 is an abstract substitution
  (absu/1)Glb is an abstract substitution

Usage:gr_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.
  (absu/1)ASub0 is an abstract substitution
  (absu/1)ASub1 is an abstract substitution

Usage:gr_sort(Asub,Asub_s)

It sorts the set of X/Value in Asub ontaining Asub_s

• The following properties should hold at call time:
  (nonvar/1)Asub is currently a term which is not a free variable.
  (var/1)Asub_s is a free variable.
  (absu/1)Asub is an abstract substitution
  (absu/1)Asub_s is an abstract substitution

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

Specialized version of call_to_entry + exit_to_prime + extend 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)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.
  (var/1)Prime is a free variable.
  (var/1)Succ is a free variable.
  (callable/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Hv is a list.
  (callable/1)Head is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Sv is a list.
  (absu/1)Call is an abstract substitution
  (absu/1)Proj is an abstract substitution
  (absu/1)Prime is an abstract substitution
  (absu/1)Succ is an abstract substitution

Usage:gr_special_builtin(SgKey,Sg,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:

1. new_ground if the builtin makes all variables ground whithout imposing any condition on the previous freeness values of the variables
2. old_ground if the builtin requires the variables to be ground
3. old_new_ground if the builtin requires some variables to be ground and grounds the rest
4. 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.
5. some if it makes some variables ground without imposing conditions
6. 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.
  (var/1)Type is a free variable.
  (var/1)Condvars is a free variable.
  (predname/1)SgKey is a Name/Arity structure denoting a predicate name:

  predname(P/A) :-
          atm(P),
          nnegint(A).
  

  
  (callable/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (atm/1)Type is an atom.
  (term/1)Condvars is any term.

Usage:gr_success_builtin(Type,Sv_u,Condv,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 grouds 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 thatno 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)Condv is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
  (var/1)Succ is a free variable.
  (atm/1)Type is an atom.
  (list/1)Sv_u is a list.
  (term/1)Condv is any term.
  (absu/1)Call is an abstract substitution
  (absu/1)Succ is an abstract substitution

Usage:gr_call_to_success_builtin(SgKey,Sh,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)Sh 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.
  (var/1)Succ is a free variable.
  (predname/1)SgKey is a Name/Arity structure denoting a predicate name:

  predname(P/A) :-
          atm(P),
          nnegint(A).
  

  
  (callable/1)Sh is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Sv is a list.
  (absu/1)Call is an abstract substitution
  (absu/1)Proj is an abstract substitution
  (absu/1)Succ is an abstract substitution

Usage:gr_input_interface(Prop,Kind,Struc0,Struc1)

Adds native property Prop to the structure accumulating the properties relevant to this domain, namely: ground/1, free/1, and not_ground/1.

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

Usage:gr_input_user_interface(InputUser,Qv,ASub)

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)InputUser 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)ASub is currently a term which is not a free variable.
  (term/1)InputUser is any term.
  (list/1)Qv is a list.
  (absu/1)ASub is an abstract substitution

Usage:gr_asub_to_native(ASub,Qv,ASub_user)

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.
  (var/1)ASub_user is a free variable.
  (absu/1)ASub is an abstract substitution
  (list/1)Qv is a list.
  (term/1)ASub_user is any term.

Usage:gr_unknown_call(Call,Vars,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)Call is currently a term which is not a free variable.
  (nonvar/1)Vars is currently a term which is not a free variable.
  (var/1)Succ is a free variable.
  (absu/1)Call is an abstract substitution
  (list/1)Vars is a list.
  (absu/1)Succ is an abstract substitution

Usage:gr_unknown_entry(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:
  (nonvar/1)Qv is currently a term which is not a free variable.
  (var/1)Call is a free variable.
  (list/1)Qv is a list.
  (absu/1)Call is an abstract substitution

Usage:gr_empty_entry(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)Vars is currently a term which is not a free variable.
  (var/1)Entry is a free variable.
  (list/1)Vars is a list.
  (absu/1)Entry is an abstract substitution

Usage:extrainfo(E)

E is a par (absu,binds)

Usage:absu(A)

A is an abstract substitution

Usage:absu_elem(E)

E is a single substitution

Usage:gr_mode(M)

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

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