termsd: types with shortening (abstract domain)

Usage:terms_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.
  (var/1)Lub is a free variable.
  (list/2)ListASub is a list of termsd_asubs.
• The following properties should hold upon exit:
  (termsd_asub/1)Lub is an abstract substitution

Usage:terms_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. Widening operations implemented are ``shortening'' and ``restricted shortening'' [GdW94,SG94].

• 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.
  (var/1)NewPrime is a free variable.
  (termsd_asub/1)Prime0 is an abstract substitution
  (termsd_asub/1)Prime1 is an abstract substitution
  (term/1)NewPrime is any term.
• The following properties should hold upon exit:
  (termsd_asub/1)NewPrime is an abstract substitution

Usage:terms_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 substituion 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).
• ExtraInfo is 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.
  (var/1)Entry is a free variable.
  (var/1)ExtraInfo is 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.
  (termsd_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:
  (termsd_asub/1)Entry is an abstract substitution
  (termsd_extrainfo/1)termsd_extrainfo(ExtraInfo)

Usage:variables_are_variable_type(Fv,ASub)

(at the moment) assigns the value top_type to the variables in Fv but in the future it must assign the value var

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

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

Usage:unify_term_and_type_term(Term1,Tv,Term2,ASub,NewASub)

It unifies the term Term1 to the type term Term2 obtaining the the abstract substitution TypeAss which is sorted and projeted on Tv

• The following properties should hold at call time:
  (nonvar/1)Term1 is currently a term which is not a free variable.
  (nonvar/1)Tv is currently a term which is not a free variable.
  (nonvar/1)Term2 is currently a term which is not a free variable.
  (nonvar/1)ASub is currently a term which is not a free variable.
  (var/1)NewASub is a free variable.
  (cgoal/1)Term1 is a term which represents a goal, i.e., an atom or a structure.
  (list/1)Tv is a list.
  (cgoal/1)Term2 is a term which represents a goal, i.e., an atom or a structure.
  (termsd_asub/1)ASub is an abstract substitution
  (term/1)NewASub is any term.
• The following properties should hold upon exit:
  (termsd_asub/1)NewASub is an abstract substitution

Usage:compute_type(Term,Type,Types)

Given the term Term and a type Type, computes the type corresponding to each variable in Term, and store it in the data structure Types. Types have the structure [vt(Var1, TypeList1), ..., vt(VarN, TypeListN)|_], where TypeListN is the list of types corresponding to variable VarN.

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

Usage:terms_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 and is not used by this predicate.

• 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.
  (var/1)Proj is a free variable.
  (term/1)Sg is any term.
  (list/1)Vars is a list.
  (term/1)HvFv_u is any term.
  (termsd_asub/1)Asub is an abstract substitution
  (term/1)Proj is any term.
• The following properties should hold upon exit:
  (termsd_asub/1)Proj is an abstract substitution

Usage:terms_abs_sort(Asub,Asub_s)

It sorts the set of X:Type in Asub containing 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.
  (termsd_asub/1)Asub is an abstract substitution
• The following properties should hold upon exit:
  (termsd_asub/1)Asub_s is an abstract substitution

Usage:terms_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.
  (var/1)Succ is a free variable.
  (term/1)Sg is any term.
  (termsd_asub/1)Prime is an abstract substitution
  (list/1)Sv is a list.
  (termsd_asub/1)Call is an abstract substitution
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (termsd_asub/1)Succ is an abstract substitution

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

Usage:terms_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.
  (termsd_asub/1)ASub0 is an abstract substitution
  (termsd_asub/1)ASub1 is an abstract substitution
  (term/1)Glb is any term.
• The following properties should hold upon exit:
  (termsd_asub/1)Glb is an abstract substitution

Usage:terms_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.
  (var/1)Call is 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:
  (termsd_asub/1)Call is an abstract substitution

Usage:terms_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.
  (var/1)Entry is 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:
  (termsd_asub/1)Entry is an abstract substitution

Usage:terms_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.
  (var/1)Succ is 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.
  (termsd_asub/1)Call is an abstract substitution
  (term/1)Succ is any term.
• The following properties should hold upon exit:
  (termsd_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.
  (var/1)ASub is a free variable.
  (list/1)Fv is a list.
• The following properties should hold upon exit:
  (termsd_asub/1)ASub is an abstract substitution

Usage:terms_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.
  (var/1)Prime is a free variable.
  (var/1)Succ is 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.
  (termsd_asub/1)Call is an abstract substitution
  (termsd_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:
  (termsd_asub/1)Prime is an abstract substitution
  (termsd_asub/1)Succ is an abstract substitution

Usage:terms_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.
  (var/1)Type is a free variable.
  (var/1)Condvars is a free variable.

Usage:terms_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.
  (var/1)ASub is 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.

Usage:terms_asub_to_native(ASub,Qv,OutFlag,OutputUser,Comps)

Transforms abstract substitution ASub to user friendly format. Record relevant symbols for output if OutFlag is yes.

• 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.
  (var/1)OutputUser is a free variable.
  (var/1)Comps is a free variable.