7.13.18 Definition of the root show operator

Page 260 of 800

Search internet

To define the texrootshow operator we need a function which shows the principal operator of a term and renders the rest normally. The lgc page defines a render-use1 and render-show1 function for use and show rendering, respectively, so we define a render-rootshow1 function for our task:

eager define render-rootshow1 ( f , x ) as newline let << t ,, s ,, c >> = x in newline let f prime :: C :: V = s in newline let s = f :: C :: V in newline let x = << t ,, s ,, c >> in newline lgc-render-show1 ( x ) end define

The function takes two arguments: a function f which defines what it means to render a term 'normally' and an argument x which is similar to the argument of render-use1 and render-show1 of the lgc page.

The render-rootshow1 function destructures x into a term t to be rendered, a rendering state s, and the cache c of the page being rendered. Then it destructures the rendering state into a rendering function f prime , an accumulating state C, and a pass down state V.

The render-rootshow1 function eventually ends up as the f prime of a rendering state and is eventually invoked by the stateexpand function from the base page. When render-rootshow1 is eventually invoked, f prime will be the render-rootshow1 function itself.

The render-rootshow1 function then constructs a new rendering state which does 'normal' rendering as defined by the parameter f, constructs a new x in which this new rendering state is installed, and then does what show rendering would have done. The effect is that lgc-render-show1 renders x, so x is show rendered. However, when lgc-render-show1 renders subterms of x, it uses the f it can get from the rendering state s. Thus, it ends up using 'normal' rendering for the subterms.

To include render-rootshow1 in a rendering state, we need its closure:

$eager define render-rootshow as newline map ( \ f . \ x . render-rootshow1 ( f , x ) ) end define$

Now that we have render-rootshow we can define the texrootshow operator:

$eager define texrootshow x end show as map ( \ x . texrootshow1 ( x ) ) end define$

eager define texrootshow1 ( x ) as newline let a :: s :: c :: T = x in newline let f :: C :: V = s in newline let << t >> = T in newline let f = render-rootshow apply f maptag in newline let s = f :: C :: V in newline lgc-render-eval ( t , a , s , c ) end define

The texrootshow construct can appear in the right hand side of a rendering definition, c.f. the previous page. When it is invoked by the renderer, it is applied to a structure x which is passed on to texrootshow1.

The texrootshow1 function destructures x into a list a of arguments, a rendering state s, a cache c, and a list T of subterms of texrootshow1. The list T has exactly one element because texrootshow1 has arity 1.

Note that a and T are two different lists of arguments. To see what they contain, consider the rendering definition from the previous section:

$tex show define root value define x as y end define as " [ "[ texrootshow x end show ]" \mathrel{\dot{\equiv}} "[ y ]" ]" end define$

The list a is the list of arguments of the left hand side of the rendering definition. The list T contains the argument of the texrootshow operator on the right hand side. Thus, the list a has two elements and the list T has one. The element of the list T represents x. The two elements of the list a indicate how x and y are instantiated.

Once texrootshow has decomposed x, it decomposes the state s into renderer f, accumulating state C, and pass down state V.

Then texrootshow extracts the sole element of the list T.

The renderer f defines what 'normal' rendering is. So texrootshow instantiates render-rootshow to a renderer which show renders a principal operator and then reverts to rendering using f.

Finally, texrootshow proceeds to rendering of t using root show rendering for all parameters it meets.

Page 260 of 800

Search logiweb.eu