This module implements the abstract operations of a types domain within the PLAI abstract interpretation framework. An abstract substitution is list of Var:Type elements, where Var is a variable and Type is a pure type term [DZ92].
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:
The meaning of the variables is
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:
Proj is the result of eliminating from Asub all X:Value such that X is not in Vars
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.
It sorts the set of X:Type in Asub ontaining Asub_s
If Prime = '$bottom', Succ = '$bottom' otherwise, Succ is computed updating the values of Call with those in Prime
Succeeds if ASub1 is more general or equal to ASub0. it's assumed the two abstract substitutions are defined on the same variables
Glb is the great lower bound of ASub0 and ASub1
Gives the “top” value for the variables involved in a literal whose definition is not present, and adds this top value to 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
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
Specialized version of call_to_entry + exit_to_prime + extend for facts
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.
Type3 is the union of Type1 and Type2 and is defined by a deterministic type rule. This is done as follows:
Def1 and Def2 are two sorted lists of type terms with compound type terms of different functor/arity. Def1 is the merge of both definitions, if two compound type terms have the same functor/arity, both are replaced by a new compound type terms whose arguments are the deterministic union of the formers.