eterms: types with lnewiden_el/4 (abstract domain)

Usage:eterms_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 foreach X:Type1 in ASub1 and X:Type2 in ASub2, X:TypeUnion is in Lub, and TypeUnion is the deterministic union of Type1 an Type2.

• 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 eterms_asubs.
• The following properties should hold upon exit:
  (nonvar/1)Lub is currently a term which is not a free variable.
  (eterms_asub/1)Lub is an abstract substitution

Usage:eterms_widen(Prime0,Prime1,NewPrime)

Induction step on the abstract substitution of a fixpoint. Prime0 corresponds to non-recursive and Prime1 to recursive clauses. NewPrime is the result of apply one widening operation to the least upper bound of the formers.

• The following properties should hold at call time:
  (nonvar/1)Prime0 is currently a term which is not a free variable.
  (nonvar/1)Prime1 is currently a term which is not a free variable.
  (eterms_asub/1)Prime0 is an abstract substitution
  (eterms_asub/1)Prime1 is an abstract substitution
  (term/1)NewPrime is any term.
• The following properties should hold upon exit:
  (nonvar/1)NewPrime is currently a term which is not a free variable.
  (eterms_asub/1)NewPrime is an abstract substitution

Usage:eterms_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 renaming Proj and adding the Fv
• Otherwise, it will
  • obtain the abstract substitution from unifying Sg and Head calling ``unify_term_and_type_term''
  • add to this abstract substitution the variables in Fv as term type.

The meaning of the variables is

• 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).
• ExtraInfois a flag ``yes'' when no unification is required, i.e., Entry=Proj upto names of vars. and ignoring Fv. It is ``no'' if unification fails.

• 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.
  (term/1)Sv is any term.
  (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.
  (eterms_asub/1)Proj is an abstract substitution
  (term/1)Entry is any term.
  (term/1)ExtraInfo is any term.
• 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.
  (eterms_asub/1)Entry is an abstract substitution
  (eterms_extrainfo/1)eterms_extrainfo(ExtraInfo)

Usage:eterms_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 ExtraInfo = yes (Head and Sg identical up to renaming) it is just renaming Exit %
• Otherwise, it will:
  • projects Exit onto Hv obtaining BPrime.
  • obtain the abstract substitution from unifying Sg and Head calling ``unify_term_and_type_term''

• 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.
  (eterms_asub/1)Exit is an abstract substitution
  (term/1)ExtraInfo is any term.
  (term/1)Prime is any term.
• The following properties should hold upon exit:
  (nonvar/1)ExtraInfo is currently a term which is not a free variable.
  (nonvar/1)Prime is currently a term which is not a free variable.
  (eterms_extrainfo/1)eterms_extrainfo(ExtraInfo)
  (eterms_asub/1)Prime is an abstract substitution

Usage:eterms_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.

• 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.
  (hvfv_u/1)HvFv_u is head variables and free variables possibly unsorted
  (eterms_asub/1)ASub is an abstract substitution
  (term/1)Proj is any term.
• The following properties should hold upon exit:
  (nonvar/1)Proj is currently a term which is not a free variable.
  (eterms_asub/1)Proj is an abstract substitution

Usage:eterms_abs_sort(ASub,ASub_s)

It sorts the set of X:Type 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.
  (eterms_asub/1)ASub is an abstract substitution
• The following properties should hold upon exit:
  (nonvar/1)ASub_s is currently a term which is not a free variable.
  (eterms_asub/1)ASub_s is an abstract substitution

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

If Prime = '$bottom', \var{Succ} = '$bottom' 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.
  (eterms_asub/1)Prime is an abstract substitution
  (list/1)Sv is a list.
  (eterms_asub/1)Call is an abstract substitution
  (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.
  (eterms_asub/1)Succ is an abstract substitution

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

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

Usage:eterms_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:term forall X in the set 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)Qv 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)Qv is a list.
  (term/1)Call is any term.
• The following properties should hold upon exit:
  (nonvar/1)Call is currently a term which is not a free variable.
  (eterms_asub/1)Call is an abstract substitution

Usage:eterms_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 giving the variable type to each variable

• 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.
  (eterms_asub/1)Entry is an abstract substitution

Usage:eterms_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.
  (eterms_asub/1)Call is an abstract substitution
  (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.
  (eterms_asub/1)Succ is an abstract substitution

Usage:variables_are_top_type(Fv,ASub)

It assigns the value top_type to the variables in Fv and return the abstract substitution ASub

• The following properties should hold at call time:
  (nonvar/1)Fv is currently a term which is not a free variable.
  (list/1)Fv is a list.
• The following properties should hold upon exit:
  (nonvar/1)ASub is currently a term which is not a free variable.
  (eterms_asub/1)ASub is an abstract substitution

Usage:eterms_call_to_success_fact(Sg,Hv,Head,K,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)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.
  (eterms_asub/1)Call is an abstract substitution
  (eterms_asub/1)Proj is an abstract substitution
  (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.
  (eterms_asub/1)Prime is an abstract substitution
  (eterms_asub/1)Succ is an abstract substitution

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

Type is a flag indicating what is the abstraction of builtin SgKey and to which variables Condvars of the goal Sg it affects.

• 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.
  (atm/1)SgKey is an atom.
  (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
  (cgoal/1)Subgoal is a term which represents a goal, i.e., an atom or a structure.
• The following properties should hold upon exit:
  (nonvar/1)Type is currently a term which is not a free variable.
  (nonvar/1)Condvars is currently a term which is not a free variable.

Usage:eterms_success_builtin(Type,Sv_uns,Condvars,HvFv_u,Call,Succ)

Depending on Type it computes the abstraction of a builtin affecting variables Condvars and having variables Sv_uns with call subs. Call.

• The following properties should hold at call time:
  (nonvar/1)Type is currently a term which is not a free variable.
  (nonvar/1)Sv_uns is currently a term which is not a free variable.
  (nonvar/1)Condvars 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.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.

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

Same as above but for each particular builtin.

• 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.
  (eterms_asub/1)Call is an abstract substitution
  (eterms_asub/1)Proj is an abstract substitution
  (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.
  (eterms_asub/1)Succ is an abstract substitution

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

Obtains the abstract substitution ASub from user supplied information.

• 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:eterms_asub_to_native(ASub,Qv,OutFlag,OutputUser,Comps)

Transforms abstract substitution ASub to user friendly format.

• 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.
  (eterms_asub/1)ASub is an abstract substitution
  (list/1)Qv is a list.
• The following properties should hold upon exit:
  (nonvar/1)OutputUser is currently a term which is not a free variable.
  (nonvar/1)Comps is currently a term which is not a free variable.

Usage:eterms_output_interface(ASub,Output)

Transforms abstract substitution ASub to a more readable but still close to internal format.

• The following properties should hold at call time:
  (nonvar/1)ASub is currently a term which is not a free variable.
  (eterms_asub/1)ASub is an abstract substitution
• The following properties should hold upon exit:
  (nonvar/1)Output is currently a term which is not a free variable.