]> matita.cs.unibo.it Git - helm.git/commitdiff
Now it is possible to define a 'cookable' operator with arity = 0 and hide = 0
authorPietro Di Lena <pietro.dilena@unibo.it>
Mon, 25 Nov 2002 18:14:21 +0000 (18:14 +0000)
committerPietro Di Lena <pietro.dilena@unibo.it>
Mon, 25 Nov 2002 18:14:21 +0000 (18:14 +0000)
helm/meta_style/meta_cic2mathml.xsl

index 005821e6fbacddc8fa81007c67e1dd2004740f5a..f77890363dfbe41ad0d42acb8c562dda64987637 100644 (file)
                </xsl:choose>
        </xsl:variable>
 
+       <xsl:variable name="const">
+               <xsl:value-of select="@arity = 0 and @hide = 0 and @cook = 'false'"/>
+       </xsl:variable>
+
        <xsl:choose>
-               <xsl:when test="@arity = 0 and @hide = 0 and $not = 'true'">
+               <xsl:when test="$const = 'true' and $not = 'true'">
                        <xsl:call-template name="out_comment">
                                <xsl:with-param name="name" select="concat($uri,': &quot;not&quot; cannot  be applyed to a constant operator')"/>
                        </xsl:call-template>
                </xsl:when>
-               <xsl:when test="@arity = 0 and @hide = 0 and @cook = 'true'">
-                       <xsl:call-template name="out_comment">
-                               <xsl:with-param name="name" select="concat($uri,': a constant operator cannot be cooked')"/>
-                       </xsl:call-template>
-               </xsl:when>
                <xsl:otherwise>
                        <!-- All uris in uri1 list (if not empty) have CONST c-tag -->
                        <xsl:variable name="uri1">
@@ -99,6 +98,7 @@
                                        <xsl:with-param name="arity" select="@arity"/>
                                        <xsl:with-param name="m-tag" select="@m-tag"/>
                                        <xsl:with-param name="c-tag" select="'CONST'"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:if>
 
                                        <xsl:with-param name="arity" select="@arity"/>
                                        <xsl:with-param name="m-tag" select="@m-tag"/>
                                        <xsl:with-param name="c-tag" select="'MUTIND'"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:if>
                </xsl:otherwise>
                </xsl:choose>
        </xsl:variable>
 
+       <xsl:variable name="const">
+               <xsl:value-of select="*[name() = 'Case']/@arity = 0 and @hide = 0 and @cook = 'false'"/>
+       </xsl:variable>
+
        <xsl:choose>
-               <xsl:when test="*[name() = 'Case']/@arity = 0 and @hide = 0 and $not = 'true'">
+               <xsl:when test="$const = 'false' and $not = 'true'">
                        <xsl:call-template name="out_comment">
                                <xsl:with-param name="name" select="concat($uri,': &quot;not&quot; cannot  be applyed to a constant operator')"/>
                        </xsl:call-template>
                </xsl:when>
-               <xsl:when test="*[name() = 'Case']/@arity = 0 and @hide = 0 and @cook = 'true'">
+               <xsl:when test="$const = 'true'">
                        <xsl:call-template name="out_comment">
-                               <xsl:with-param name="name" select="concat($uri,': a constant operator cannot be cooked')"/>
+                               <xsl:with-param name="name" select="concat($uri,':  cannot be specified a constant operator when using OpSet element')"/>
                        </xsl:call-template>
                </xsl:when>
                <xsl:otherwise>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="m-tag"/>
        <xsl:param name="c-tag"/>
+       <xsl:param name="const" select="'false'"/>
 
        <xsl:variable name="apply_not">
                <xsl:if test="$not = 'true'">*[2]/</xsl:if>
        </xsl:variable>
 
        <xsl:variable name="match">
-               <xsl:call-template name="out_match">
-                       <xsl:with-param name="not"   select="$not"/>
-                       <xsl:with-param name="uri"   select="$uri"/>
-                       <xsl:with-param name="cook"  select="$cook"/>
-                       <xsl:with-param name="hide"  select="$hide"/>
-                       <xsl:with-param name="arity" select="$arity"/>
-                       <xsl:with-param name="c-tag" select="$c-tag"/>
-               </xsl:call-template>    
+               <xsl:variable name="match_op">
+                       <xsl:call-template name="out_match_op">
+                               <xsl:with-param name="not"   select="$not"/>
+                               <xsl:with-param name="uri"   select="$uri"/>
+                               <xsl:with-param name="c-tag" select="$c-tag"/>
+                       </xsl:call-template>
+               </xsl:variable>
+
+               <xsl:variable name="match_child">
+                       <xsl:if test="$cook = 'false' or $not = 'true'">
+                               <xsl:choose>
+                                       <!-- if the operator has been concatenated with not, the root apply node must have only two child -->
+                                       <xsl:when test="$not = 'true' and $cook = 'true'"> and count(*) = 2</xsl:when>
+                                       <xsl:when test="$not = 'true' and $cook = 'false'">
+                                               <xsl:value-of select="concat(' and count(*) = 2 and count(*[2]/*) = ',$arity + $hide + 1)"/>
+                                       </xsl:when>
+                                       <xsl:otherwise>
+                                               <xsl:value-of select="concat('count(*) = ',$arity + $hide + 1)"/>
+                                       </xsl:otherwise>
+                               </xsl:choose>
+                       </xsl:if>
+               </xsl:variable>
+
+               <xsl:choose>
+                       <xsl:when test="$const = 'false'">
+                               <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
+                       </xsl:when>
+                       <xsl:otherwise>
+                               <xsl:value-of select="$match_op"/>
+                       </xsl:otherwise>
+               </xsl:choose>
        </xsl:variable>
 
        <xsl:variable name="op_uri_attr">
                        <xsl:call-template name="op_uri_attr">
                                <xsl:with-param name="not"   select="$not"/>
                                <xsl:with-param name="c-tag" select="$c-tag"/>
-                               <xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
+                               <xsl:with-param name="const" select="$const"/>
                        </xsl:call-template>
                </xsl:variable>
                <xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
                <xsl:choose>
                        <xsl:when test="$cook = 'true'">
                                <oxsl:variable name="no_params">
-                                       <oxsl:variable name="no_params_tmp">
-                                               <oxsl:call-template name="get_no_params">
-                                                       <oxsl:with-param name="first_uri"  select="$CICURI"/>
-                                                       <oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
-                                               </oxsl:call-template>
-                                       </oxsl:variable>
-                                       <oxsl:value-of select="number($no_params_tmp)"/>
+                                       <oxsl:call-template name="get_no_params">
+                                               <oxsl:with-param name="first_uri"  select="$CICURI"/>
+                                               <oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
+                                       </oxsl:call-template>
                                </oxsl:variable>
                                <oxsl:choose>
                                        <oxsl:when test="{concat('count(',$apply_not,'*) = $no_params + ',$arity + $hide + 1)}">
                                                        <xsl:with-param name="hide"  select="$hide"/>
                                                        <xsl:with-param name="arity" select="$arity"/>
                                                        <xsl:with-param name="not"   select="$not"/>
+                                                       <xsl:with-param name="const" select="$const"/>
                                                </xsl:call-template>
                                         </oxsl:when>
                                         <oxsl:otherwise>
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:otherwise>
                </xsl:choose>
        </xsl:variable>
 
        <xsl:variable name="match">
-               <xsl:call-template name="out_match_op">
-                       <xsl:with-param name="not"   select="$not"/> 
-                       <xsl:with-param name="uri"   select="$uri"/> 
-                       <xsl:with-param name="c-tag" select="$c-tag"/>
-               </xsl:call-template>
+               <xsl:variable name="match_op">
+                       <xsl:call-template name="out_match_op">
+                               <xsl:with-param name="not"   select="$not"/> 
+                               <xsl:with-param name="uri"   select="$uri"/> 
+                               <xsl:with-param name="c-tag" select="$c-tag"/>
+                       </xsl:call-template>
+               </xsl:variable>
+               
+                <xsl:variable name="match_child">
+                       <xsl:if test="$not = 'true'"> and count(*) = 2</xsl:if>
+                </xsl:variable>
+
+                <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
        </xsl:variable>
 
        <xsl:variable name="apply_not">
                <xsl:with-param name="name" select="$name"/>
        </xsl:call-template>
        
-       <oxsl:template match="{concat('APPLY[',$match,']')}" mode="pure">
+       <oxsl:template match="{$match}" mode="pure">
                <xsl:if test="$cook = 'true'">
                        <oxsl:variable name="no_params">
-                               <oxsl:variable name="no_params_tmp">
-                                       <oxsl:call-template name="get_no_params">
-                                               <oxsl:with-param name="first_uri"  select="$CICURI"/>
-                                               <oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
-                                       </oxsl:call-template>
-                               </oxsl:variable>
-                               <oxsl:value-of select="number($no_params_tmp)"/>
+                               <oxsl:call-template name="get_no_params">
+                                       <oxsl:with-param name="first_uri"  select="$CICURI"/>
+                                       <oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
+                               </oxsl:call-template>
                        </oxsl:variable>
                </xsl:if>       
                <oxsl:choose>
        <xsl:value-of select="concat($app_not,$app_op)"/>
 </xsl:template>
 
-<!-- Returns a test on apply node children number-->
-<xsl:template name="out_match_child">
-       <xsl:param name="not"   select="'false'"/>
-       <xsl:param name="cook"  select="'false'"/>
-       <xsl:param name="hide"  select="0"/>
-       <xsl:param name="arity" select="0"/>
-
-       <!--
-               Test on children number only if the operator is concatenated with not of 
-               if it is not constant and it has not to be cooked.
-               It is not possible to concatenate a constant operator with not.
-       -->
-       <xsl:if test="$not = 'true' or (($arity != 0 or $hide != 0) and $cook = 'false')">
-               <xsl:choose>
-                       <!-- if the operator has been concatenated with not, the root apply node must have only two child -->
-                       <xsl:when test="$not = 'true'">
-                               <xsl:variable name="test_apply_children">
-                                       <xsl:if test="$cook = 'false'">
-                                               <xsl:value-of select="concat(' and count(*[2]/*) = ',$arity + $hide + 1)"/>
-                                       </xsl:if>
-                               </xsl:variable>
-                               
-                               <xsl:value-of select="concat('count(*) = 2',$test_apply_children)"/>
-                       </xsl:when>
-                       <xsl:otherwise>
-                               <xsl:value-of select="concat('count(*) = ',$arity + $hide + 1)"/>
-                       </xsl:otherwise>
-               </xsl:choose>
-       </xsl:if>
-</xsl:template>
-
-<xsl:template name="out_match">
-       <xsl:param name="not"   select="'false'"/>
-       <xsl:param name="uri"/>
-       <xsl:param name="cook"  select="'false'"/>
-       <xsl:param name="hide"  select="0"/>
-       <xsl:param name="arity" select="0"/>
-       <xsl:param name="c-tag"/>
-       
-       <!--           TEST ON OPERATOR(S) TYPE         -->
-       <xsl:variable name="match_op">
-               <xsl:call-template name="out_match_op">
-                       <xsl:with-param name="not"   select="$not"/>
-                       <xsl:with-param name="uri"   select="$uri"/>
-                       <xsl:with-param name="hide"  select="$hide"/>
-                       <xsl:with-param name="c-tag" select="$c-tag"/>
-               </xsl:call-template>
-       </xsl:variable>
-               
-       <!--           TEST ON CHILD(REN) NUMBER         -->
-       <xsl:variable name="match_child">
-               <xsl:call-template name="out_match_child">
-                       <xsl:with-param name="not"   select="$not"/>
-                       <xsl:with-param name="cook"  select="$cook"/>
-                       <xsl:with-param name="hide"  select="$hide"/>
-                       <xsl:with-param name="arity" select="$arity"/>
-               </xsl:call-template>
-       </xsl:variable>
-
-       <xsl:choose>
-               <!-- not a constant operator -->
-               <xsl:when test="$arity != 0 or $hide != 0">
-                       <xsl:choose>
-                               <xsl:when test="$match_child != ''">
-                                       <xsl:value-of select="concat('APPLY[',$match_op,' and ',$match_child,']')"/>
-                               </xsl:when>
-                               <xsl:otherwise>
-                                       <xsl:value-of select="concat('APPLY[',$match_op,']')"/>
-                               </xsl:otherwise>
-                       </xsl:choose>
-               </xsl:when>
-               <xsl:otherwise>
-                       <xsl:choose>
-                               <xsl:when test="$match_child != ''">
-                                       <xsl:value-of select="concat($match_op,' and ',$match_child)"/>
-                               </xsl:when>
-                               <xsl:otherwise>
-                                       <xsl:value-of select="$match_op"/>
-                               </xsl:otherwise>
-                       </xsl:choose>
-               </xsl:otherwise>
-       </xsl:choose>
-</xsl:template>
-
 <xsl:template name="out_params">
        <xsl:param name="params" select="1"/>
        <xsl:param name="cook"   select="'false'"/>
        <xsl:param name="hide"  select="0"/>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="not"   select="'false'"/>
+       <xsl:param name="const" select="'false'"/>
 
        <xsl:choose>
                <!--            SIMPLE TRANSFORMATIONS            -->
                <xsl:when test="count(*) = 0">
-                       <xsl:variable name="xref">{@id}</xsl:variable>
+                       <xsl:variable name="xref">
+                                <xsl:if test="$const = 'false'">{@id}</xsl:if>
+                       </xsl:variable>
 
                        <xsl:variable name="definitionURL">
                                <xsl:call-template name="op_uri_attr">
                                        <xsl:with-param name="not"   select="$not"/>
                                        <xsl:with-param name="c-tag" select="$c-tag"/>
-                                       <xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:variable>
 
                                <xsl:call-template name="op_id_attr">
                                        <xsl:with-param name="not"   select="$not"/>
                                        <xsl:with-param name="c-tag" select="$c-tag"/>
-                                       <xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                         </xsl:variable>
                
                                <xsl:with-param name="hide"  select="$hide"/>
                                <xsl:with-param name="arity" select="$arity"/>
                                <xsl:with-param name="not"   select="$not"/>
+                               <xsl:with-param name="const" select="$const"/>
                        </xsl:apply-templates>
                </xsl:otherwise>
        </xsl:choose>
        <xsl:param name="hide"  select="0"/>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="not"   select="'false'"/>
+       <xsl:param name="const" select="'false'"/>
        
        <xsl:variable name="helm:xref">
                <xsl:choose>
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:when>
-                       <xsl:otherwise>{@id}</xsl:otherwise>
+                       <xsl:otherwise>
+                               <xsl:if test="$const = 'false'">{@id}</xsl:if>
+                       </xsl:otherwise>
                </xsl:choose>
        </xsl:variable>
 
                        <xsl:with-param name="hide"   select="$hide"/>
                        <xsl:with-param name="arity"  select="$arity"/>
                        <xsl:with-param name="not"    select="$not"/>
+                       <xsl:with-param name="const" select="$const"/>
                        <xsl:with-param name="ignore" select="'xref'"/>
                </xsl:call-template>
        
                        <xsl:with-param name="hide"  select="$hide"/>
                        <xsl:with-param name="arity" select="$arity"/>
                        <xsl:with-param name="not"   select="$not"/>
+                       <xsl:with-param name="const" select="$const"/>
                </xsl:apply-templates>
        </m:apply>
 </xsl:template>
        <xsl:param name="hide"  select="0"/>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="not"   select="'false'"/>
+       <xsl:param name="const" select="'false'"/>
 
        <!-- set definitonURL attribute -->
        <xsl:variable name="definitionURL">
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:when>
                        <xsl:otherwise>
                                <xsl:call-template name="op_uri_attr">
                                        <xsl:with-param name="not"   select="$not"/>
                                        <xsl:with-param name="c-tag" select="$c-tag"/>
-                                       <xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:otherwise>
                </xsl:choose>
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:when>
                        <xsl:otherwise>
                                <xsl:call-template name="op_id_attr">
                                        <xsl:with-param name="not"   select="$not"/>
                                        <xsl:with-param name="c-tag" select="$c-tag"/>
-                                       <xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:otherwise>
                </xsl:choose>
                        <xsl:with-param name="hide"   select="$hide"/>
                        <xsl:with-param name="arity"  select="$arity"/>
                        <xsl:with-param name="not"    select="$not"/>
+                       <xsl:with-param name="const" select="$const"/>
                        <xsl:with-param name="ignore" select="'xref + definitionURL + tag'"/>
                </xsl:call-template>
                
                        <xsl:with-param name="hide"  select="$hide"/>
                        <xsl:with-param name="arity" select="$arity"/>
                        <xsl:with-param name="not"   select="$not"/>
+                       <xsl:with-param name="const" select="$const"/>
                </xsl:apply-templates>
        </xsl:element>
 </xsl:template>
        <xsl:param name="hide"  select="0"/>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="not"   select="'false'"/>
+       <xsl:param name="const" select="'false'"/>
        
        <xsl:copy>
                <xsl:call-template name="copy_attributes">
                        <xsl:with-param name="hide"  select="$hide"/>
                        <xsl:with-param name="arity" select="$arity"/>
                        <xsl:with-param name="not"   select="$not"/>
+                       <xsl:with-param name="const" select="$const"/>
                </xsl:call-template>
        
                <xsl:apply-templates>
                        <xsl:with-param name="hide"  select="$hide"/>
                        <xsl:with-param name="arity" select="$arity"/>
                        <xsl:with-param name="not"   select="$not"/>
+                       <xsl:with-param name="const" select="$const"/>
                </xsl:apply-templates>
        </xsl:copy>
 </xsl:template>
        <xsl:param name="hide"  select="0"/>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="not"   select="'false'"/>
+       <xsl:param name="const" select="'false'"/>
 
        <xsl:variable name="binded_params">
                <xsl:call-template name="get_binded_params">
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:apply-templates>
                        </m:bvar>
                </xsl:when>
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:apply-templates>
                        </m:bvar>
                </xsl:otherwise>
        <xsl:param name="hide"   select="0"/>
        <xsl:param name="arity"  select="0"/>
        <xsl:param name="not"    select="'false'"/>
+       <xsl:param name="const"  select="'false'"/>
        <xsl:param name="ignore" select="''"/>
        
        <xsl:variable name="test">
        
        <xsl:for-each select="@*">
                <xsl:if test="contains($test,concat('+',name(),'+')) = false()">
-                       <xsl:attribute name="{name()}">
+                       <xsl:variable name="name">
+                               <xsl:choose>
+                                       <xsl:when test="name() = 'xref'">helm:xref</xsl:when>
+                                       <xsl:otherwise>
+                                               <xsl:value-of select="name()"/>
+                                       </xsl:otherwise>
+                               </xsl:choose>
+                       </xsl:variable>
+                       
+                       <xsl:attribute name="{$name}">
                                <xsl:call-template name="set_attribute">
                                        <xsl:with-param name="attr"  select="."/>
                                        <xsl:with-param name="c-tag" select="$c-tag"/>
                                        <xsl:with-param name="hide"  select="$hide"/>
                                        <xsl:with-param name="arity" select="$arity"/>
                                        <xsl:with-param name="not"   select="$not"/>
+                                       <xsl:with-param name="const" select="$const"/>
                                </xsl:call-template>
                        </xsl:attribute>
                </xsl:if>
        <xsl:param name="hide"  select="0"/>
        <xsl:param name="arity" select="0"/>
        <xsl:param name="not"   select="'false'"/>
+       <xsl:param name="const" select="'false'"/>
        
        <xsl:choose>
-               <xsl:when test="$attr = '$APP-ID'">{@id}</xsl:when>
+               <xsl:when test="$attr = '$APP-ID'">
+                       <xsl:if test="$const = 'false'">{@id}</xsl:if>
+               </xsl:when>
                <xsl:when test="$attr = '$OP-ID' or $attr = '$OP-URI'">
                        <xsl:variable name="attr_type">
                                <xsl:choose>
                                <xsl:with-param name="attr_type" select="$attr_type"/>
                                <xsl:with-param name="not"       select="$not"/>
                                <xsl:with-param name="c-tag"     select="$c-tag"/>
-                               <xsl:with-param name="const"     select="$arity = 0 and $hide = 0"/>
+                               <xsl:with-param name="const"     select="$const"/>
                        </xsl:call-template>
                </xsl:when>
                <xsl:otherwise>