Function fungi_lang::normal::normal_idxtm [−][src]
pub fn normal_idxtm(ctx: &Ctx, i: IdxTm) -> IdxTm
Normalize index terms, by expanding definitions and reducing function applications where possible.
Example 1:
// Unknowns:
idxtm X : NmSet
idxtm Y : NmSet
nmtm z : Nm
idxtm bin : Nm -> NmSet = (#x:Nm. {x * @1} % {x * @2})
idxtm set : NmSet = (({@3}%Y)%(X%{z}))
idxtm example : NmSet = (bin) set
The example
term normalizes to the following term
{@3*@1} % {@3*@2}
% (
NORM[ (#x:Nm. {x * @1} % {x * @2}) (X) ]
% (
{z*@1} % {z*@2}
% (
NORM[ (#x:Nm. {x * @1} % {x * @2}) (Y) ]
%
0 )))
: NmSet
Where the index-level flat-map terms (in each NORM[ ... ]
) normalize
further, converting into name-level maps, as follows:
NORM[ (#x:Nm. {x * @1} % {x * @2}) (X) ]
==
[ #x:Nm. x * @1 ](X) % [ #x:Nm. x * @2 ](X)
Example 2:
The following index term:
(#x:Nm. {x, @1} % {x, @2}) ({@3}%Y)%(X%{z})
Normalizes to the following:
{@3 * @1}
% (
{@3 * @2}
% (
((#x:Nm. {x,@1}) Y)
% (
((#x:Nm. {x,@2}) Y)
% (
((#x:Nm. {x,@1}) (X))
% (
((#x:Nm. {x,@2}) (X))
% (
{z,@1} % {z,@2}
%
0 ))))))
Notice that the nested binary tree of disjoint unions (%
) is
flattened into a list, where disjoint union (%
) plays the rule
of Cons
, and where empty set (0
) plays the role of Nil
.
Further, the flat-mapped function (bin
) has been applied to the
set structure:
-
The mapping function has been applied to the singleton sets of name constant
@3
and name variablez
, respectively. -
Meanwhile, as the set variables
X
andY
stand for unknown sets of names, the flat map is not reduced over these (unknown) sets, but only distributed across the disjoint union (%
) that connects them. -
Finally, the flat-map term
(#x:Nm. {x * @1} % {x * @2}) (X)
normalizes into two mapping terms, one for each singleton set of the flat-map function's body.