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:

  1. The mapping function has been applied to the singleton sets of name constant @3 and name variable z, respectively.

  2. Meanwhile, as the set variables X and Y 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.

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