shfr: sharing+freeness (abstract domain)

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

Proj_sh is obtained as in the sharing domain. Proj_fr is the result of eliminating from Fr all X/Value such that X 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
  (term/1)ASub is any term.
  (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.
• 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:project_freeness(Vars,ListFreenessValues,Proj)

Eliminates from each list in the second argument any variable/Value such that the variable is not an element of the first argument.

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

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

• If Sg and Head are identical up to renaming it is just a question or 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_fr the variables in Hv as free variables (Temp1_fr).
  • update Temp1_fr, Proj_sh (grounding some variables) and Binds (eliminating those elements (X,Term,Tv) s.t. X or Term are ground), obtaining Temp2_fr, NewProj_sh, and NewBind.
  • insert Fv in Temp2_fr as free variables (Temp3_fr).
  • changes any nf(_,_) in Temp3_fr to nf(Beta_fr).
  • projects Beta_fr onto Hv obtaining Entry_fr.
  • Obtains in Share a first approximation of the sharing defined over the variables of Sg and Head based on Bindings, NewProj_sh and Temp3_fr.
  • Projects Share over Hv and obtains in Beta_sh the powerset of each set in the projected sharing.
  • then it obtains in ShareArgsStar the star of the sharing among the arguments of Sg established by NewProj_sh, and in Head_args the set of variables belonging to each argument of Head.
  • Then the idea is to obtain Entry_sh by eliminating from Beta_sh those sets which are not allowed (they would imply sharing among arguments in the head while there is no sharing among those arguments in ShareArgsStar).

• 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.
  (list/1)Hv is a list.
  (list/1)Fv is a list.
• 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.
• 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 a question or renaming Exit.
• If Hv = [], Prime_sh = [] and Prime_fr = {X/g| forall X in Sv}.

• 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/2)Hv is a list of vars.
  (list/2)Sv is a list of vars.
• 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.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form exit_to_prime(Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime) do not fail.

Usage:abs_sort(Asub,Asub_s)

First sorts the set of set of variables Sh to obtain the Sh_s. Then it sorts the set of X/Value in Fr obtaining Fr_s.

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

Usage:compute_lub(ListASub,Lub)

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

• merging the Sh1 and Sh2.
• foreach X/Value1 in Fr1 and X/Value2 in Fr2:
  • if Value1 == Value2, X/Value1 in Lub_fr.
  • otherwise, X/nf in Lub_fr.

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

Usage:glb(ASub0,ASub1,Glb)

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

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

If Prime = bottom, Succ = bottom. If Sv = [], Call = Succ. Otherwise, Succ_sh is computed as in share_extend/5, i.e. it splits Call_sh into two set of sets: Intersect (those sets containing at least a variabe in Sv) and Disjunct (the rest). Then it obtains in Star the closure under union of Intersect. Finally, it prunes Star with the information in Prime_sh adding, at the end, Disjunct. Call_fr is computed by:

• obtainig in NewGv the set of variables which have becomed ground (those which were not ground in Call but are ground in Succ_sh).
• adding this NewGv variables to Prime_fr, obtaining Temp1_fr.
• obtaining in BVars the set of nonground variables in Succ which do not belong to Sg (are not in Sv).
• Then it obtains in BVarsf the subset of BVars which are free w.r.t Call_fr, and in Temp2_fr, the result of adding X/nf to Temp1_fr for the rest of variables in BVars.
• If BVarsf = [],

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

Usage:

Specialized version of call_to_entry + exit_to_prime + extend for facts.

Usage:

Specialised version of call_to_success_fact/7 in order to allow the computation of the prime, the composition and then the extension Note that if the success is computed (instead of the prime) and then we compose the information and project it, we can loose information since the extension is the step in which more information is lost

Usage:unknown_entry(Sg,Qv,Call)

The top value in Sh for a set of variables is the powerset, in Fr is X/nf 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.
• The following properties should hold upon exit:
  (nonvar/1)Call is currently a term which is not a free variable.

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 Sh is the list of singleton lists of variables and in Fr is X/f 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)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.
  (absu/1)Entry is an abstract substitution
• The following properties should hold upon exit:
  (nonvar/1)Entry is currently a term which is not a free variable.

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

Obtaining the abstract substitution for Sh+Fr from the user supplied information just consists in taking the Sharing first and the var(Fv) element of InputUser, and construct from them the Freeness.

• 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.

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

The user friendly format consists in extracting the ground variables and the free 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.
  (term/1)ASub is any term.
  (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:obtain_info(Prop,Vars,ASub,Info)

Prop holds for Info in ASub over Vars.

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

Usage:obtain_info(Prop,ASub,Info)

Prop holds for Info in ASub.

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

Usage:less_or_equal(ASub0,ASub1)

Succeeds if ASub1 is more general or equal to ASub0.

• 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.

Usage:special_builtin(SgKey,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.
• all_nonfree if the builtin makes all variables possible non free.
• 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.
  (nonvar/1)Subgoal is currently a term which is not a free variable.
  (var/1)Condvars is a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Type is currently a term which is not a free variable.

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 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 that no free variables has becomed ground. If so, it grounds all variables in NewG.
• If Type = all_non_free it projects Call onto this variables, obatins the closure under union for the Sh, changes in Fr all f to nf and later extends the result.
• 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.
• The following properties should hold upon exit:
  (nonvar/1)Succ is currently a term which is not a free variable.

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

Usage:take_coupled(Sh,Vars,Coupled)

Sh is a list of lists of variables, Vars is a list of variables. Returns in Coupled the list of variables X s.t. exists at least one list in Sh containing X and at least one element in Vars.

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

Usage:split_coupled(Vars,Fr,Fv,Terms)

It receives as input a sorted list of variables Vars and a sorted lists of freeness values (Var/FreenessValue). It computes:

• Fv : list of vars X in Vars such that X/f appears in Fr.
• Terms: list of terms Term such that X/nf(_,Term) appears in Fr.

• The following properties should hold at call time:
  (nonvar/1)Vars is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Fv is currently a term which is not a free variable.
  (nonvar/1)Terms is currently a term which is not a free variable.

Usage:decide_update_lambda(Gv,Fr,Sh,Hv,NewFr,NewSh)

This predicates handles the case in which a set of variables (Gv) have been determined as ground, and it has to:

• Update the sharing component eliminating any set in which at least one of the now ground variables appears.
• Update the freeness component in order to:
  • all ground variables appear as ground.
  • those free variables which are coupled (but not are become ground) should become non free.

• The following properties should hold at call time:
  (nonvar/1)Gv is currently a term which is not a free variable.
  (nonvar/1)Fr 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)Hv is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewFr is currently a term which is not a free variable.
  (nonvar/1)NewSh is currently a term which is not a free variable.

Usage:update_lambda_sf(Gv,Fr,Sh,NewFr,NewSh)

Identical to decide_update_lambda/6 but since it is not call from the abstract unification, no test on the Hv is needed.

• The following properties should hold at call time:
  (nonvar/1)Gv is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
  (nonvar/1)Sh is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewFr is currently a term which is not a free variable.
  (nonvar/1)NewSh is currently a term which is not a free variable.

Usage:update_lambda_non_free(Gv,Fr,Sh,NewFr,NewSh)

Identical to update_lambda_sf/5 but:

• it tests that the variables that become ground are not free. The reason is that Ground should be ground already, and therefore they cannot make a definitely free variable to become ground.
• it does not change the freeness value of any variable from f to nf (The same reason).

• The following properties should hold at call time:
  (nonvar/1)Gv is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
  (nonvar/1)Sh is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewFr is currently a term which is not a free variable.
  (nonvar/1)NewSh is currently a term which is not a free variable.

Usage:partition_sf(Binds,Fr,Sh,NewSh)

If Binds is emtpy, then NewSh is { [X] | X/V in Freeness, V $\neq$ g, X not in vars(Sh) } union Sh. (this is computed by partition_end_sf(Fr,Sh,NewSh)). Otherwise:

• First computes TempSh = { [X] | $\forall$ X/V in Fr, V $\neq$ g and $\not \exists$ S in Sh, X in S }
• Then foreach (X,Term,Tv) in Binds, it computes the freeness value Value of X in Fr.
• If Value = nf(X,Term) then
  • eliminates from TempSh those elements SS such that either X in SS or Tv $\cap$ SS $\neq$ $\emptyset$.
  • adds P1 $\cup$ P2 s.t. X $\in$ P1, Tv $\cap$ P2 $\neq$ $\emptyset$.
• If Value = nf then
  • eliminates from TempSh those elements SS such that either X in SS or Tv $\cap$ SS $\neq$ $\emptyset$.
    • adds $\bigcup$ P s.t. X $\in$ P or Tv $\cap$ P $\neq$ $\emptyset$.
• If Value = f then (note that then Term is a variable)
  • eliminates from TempSh those elements SS such that either X in SS or Term $\in$ SS.
  • adds P1 $\cup$ P2 s.t. X $\in$ P1, Y $\notin$ P1, Y $\in$ P2 X $\notin$ P2.

• The following properties should hold at call time:
  (nonvar/1)Binds is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
  (nonvar/1)Sh is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewSh is currently a term which is not a free variable.

Usage:prune(Beta_sh,Head_args,ShareArgs,Temp1,Entry)

Eliminates any set in Beta_sh s.t. the induced sharing on the arguments of Head_args is allowed by ShareArgs.

• The following properties should hold at call time:
  (nonvar/1)Beta_sh is currently a term which is not a free variable.
  (nonvar/1)Head_args is currently a term which is not a free variable.
  (nonvar/1)ShareArgs is currently a term which is not a free variable.
  (nonvar/1)Temp1 is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Entry is currently a term which is not a free variable.

Usage:covering(Disjoint,Sh,AlsoPossible)

AlsoPossible = { X in Disjoint| $\exists$ S_1,..,S_n in Sh, union S_i = X }

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

Usage:eliminate_non_element(Sv,Sh1,Sh2,NewSh)

NewSh is the result of eliminating from Sh1 (list of lists of variables) those elements which projected over Sv do not appear in Sh2. All ordered.

• The following properties should hold at call time:
  (nonvar/1)Sv is currently a term which is not a free variable.
  (nonvar/1)Sh1 is currently a term which is not a free variable.
  (nonvar/1)Sh2 is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewSh is currently a term which is not a free variable.

Usage:obtain_prime_var_var(+[X/V,Y/V],Call,Success)

Handles the case X = Y where both X,Y are variables which freeness value == g.

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

Usage:sh_free_vars_compatible(Sh,Fs)

Satisfied if a list of free variables Fs and a potential sharing set Sh over those variables are compatible. This happens if and only if there is a subset of Sh that is a disjunt partition of Fs.

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

Usage:make_dependence(Sh,Vars,Fr,NewFr,NewSh)

It gives the new sharing and freeness component for the variables in Y (Vars) when recorded(X,Y,Z) was called, once the variables in Z have been made ground.

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

Usage:values_equal(Vars,Fr,Value)

Satisfied if the freeness values of all variables in Vars is equal to Value.

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

Usage:values_differ(Vars,Fr,Value)

Satisfied if the freeness values of all variables in Vars is different from Value.

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

Usage:change_values(Vars,Fr,NewFr,Value)

Forall X in Vars, there must exist an X/V in Fr. If so, it changes V to Value. Otherwise it fails.

• The following properties should hold at call time:
  (nonvar/1)Vars is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
  (nonvar/1)Value is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewFr is currently a term which is not a free variable.

Usage:change_values_if_not_g(Vars,Fr,NewFr,Value)

Forall X in Vars, there must exist an X/V in Fr. If so:

• if V is `g, X/V remains unchanged.
• else, X/V is replaced by X/Value is added.

• The following properties should hold at call time:
  (nonvar/1)Vars is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
  (nonvar/1)Value is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewFr is currently a term which is not a free variable.

Usage:change_values_if_f(Vars,Fr,NewFr,Value)

Forall X in Vars, there must exist an X/V in Fr. If so:

• if V is nf(_,_), X/V is replaced by X/Value.
• else, X/V remains unchanged.

• The following properties should hold at call time:
  (nonvar/1)Vars is currently a term which is not a free variable.
  (nonvar/1)Fr is currently a term which is not a free variable.
  (nonvar/1)Value is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewFr is currently a term which is not a free variable.

Usage:member_value_freeness_differ(Fr,Vars,Value)

It returns in Vars the list of variables with freeness value different from Value.

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

Usage:project_freeness_n(Fr1,Fr2,Eliminated)

Eliminates from Fr2 any X/Value s.t. X is not in Fr1. Also if the value in Fr1 is f and the value in Fr2 is nf, the value in Eliminated will be f. Otherwise, it will be the value in Fr2.

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

Usage:propagate_non_freeness(Vars,NonFv,Sh,Fr,NewFr)

NewFr is the result of inserting each variable in Vars with value nf, if it appears in Sh with a nonfree variable. Otherwise it inserts X/f.

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

Usage:add_environment_vars(Fr1,Fr2,NewFr)

Fr2 contains all variables in Fr1 and possibly new ones (Fr1 corresponds to a prime while Fr2 corresponds to a call). Then, NewFr = Fr1 + {`X`/`V` in `Fr2`| `X`/_ not in `Fr1`}.

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