X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmeta_style%2Fmeta_cic2mathml.xsl;h=072774b5d50bcb7c4c7dfefb93e47e76f59d8acd;hb=7e9ee837f75f38bf01240cdc03dd51c764c2665f;hp=005821e6fbacddc8fa81007c67e1dd2004740f5a;hpb=5379335718a93d3e933d9bfdc0dd85f00983bc21;p=helm.git

diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl
index 005821e6f..072774b5d 100644
--- a/helm/meta_style/meta_cic2mathml.xsl
+++ b/helm/meta_style/meta_cic2mathml.xsl
@@ -47,6 +47,7 @@
 	<oxsl:include href="{@href}"/>
 </xsl:template>
 
+
 <xsl:template match="Operator|NotOperator">
 	<xsl:variable name="uri">
 		<xsl:call-template name="remove_white_spaces">
@@ -61,17 +62,16 @@
 		</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">
@@ -80,7 +80,7 @@
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
 			</xsl:variable>
-			
+
 			<!-- All uris in uri2 list (if not empty) have MUTIND c-tag -->
 			<xsl:variable name="uri2">
 				<xsl:call-template name="select_uris">
@@ -94,12 +94,24 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri1"/>
-					<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="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 test="@cook = 'true'">
+					<xsl:call-template name="out_template">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri1"/>
+						<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="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'CONST'"/>
+					</xsl:call-template>
+				</xsl:if>
 			</xsl:if>
 
 			<xsl:if test="$uri2 != ''">
@@ -107,12 +119,24 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri2"/>
-					<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="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 test="@cook = 'true'">
+					<xsl:call-template name="out_template">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri2"/>
+						<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="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'MUTIND'"/>
+					</xsl:call-template>	
+				</xsl:if>
 			</xsl:if>
 		</xsl:otherwise>
 	</xsl:choose>
@@ -132,15 +156,19 @@
 		</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 = '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="*[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>
@@ -163,11 +191,21 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri1"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template_set">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri1"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'CONST'"/>
+					</xsl:call-template>
+				</xsl:if>
 			</xsl:if>
 
 			<xsl:if test="$uri2 != ''">
@@ -175,11 +213,21 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri2"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'MUTIND'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template_set">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri2"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'MUTIND'"/>
+					</xsl:call-template>	
+				</xsl:if>
 			</xsl:if>
 		</xsl:otherwise>
 	</xsl:choose>
@@ -199,31 +247,40 @@
 	<xsl:param name="arity" select="0"/>
 	<xsl:param name="m-tag"/>
 	<xsl:param name="c-tag"/>
-
-	<xsl:variable name="apply_not">
-		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
-	</xsl:variable>
-
+	<xsl:param name="const" select="'false'"/>
+	
 	<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>
-
-	<xsl:variable name="op_uri_attr">
-		<xsl:variable name="tmp_op_uri_attr">
-			<xsl:call-template name="op_uri_attr">
+		<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="cook"  select="$cook"/>
 				<xsl:with-param name="c-tag" select="$c-tag"/>
-				<xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
 			</xsl:call-template>
 		</xsl:variable>
-		<xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
+		
+		<xsl:variable name="match_child">
+			<xsl:if test="$const = '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:value-of select="concat(' and count(*) = 2 and count(*[2]/*) = ',$arity + $hide + 1)"/>
+					</xsl:when>
+					<xsl:otherwise>
+						<xsl:value-of select="concat(' and 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>
 
 	<!--                     TEMPLATE                     -->
@@ -232,44 +289,15 @@
 	</xsl:call-template>
 
 	<oxsl:template match="{$match}" mode="pure">
-		<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:variable>
-				<oxsl:choose>
-					<oxsl:when test="{concat('count(',$apply_not,'*) = $no_params + ',$arity + $hide + 1)}">
-						<xsl:call-template name="out_body">
-							<xsl:with-param name="c-tag" select="$c-tag"/>
-							<xsl:with-param name="m-tag" select="$m-tag"/>
-							<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="not"   select="$not"/>
-						</xsl:call-template>
-					 </oxsl:when>
-					 <oxsl:otherwise>
-					 	<oxsl:apply-imports/>
-					</oxsl:otherwise>
-				</oxsl:choose>
-			</xsl:when>
-			<xsl:otherwise>
-				<xsl:call-template name="out_body">
-					<xsl:with-param name="c-tag" select="$c-tag"/>
-					<xsl:with-param name="m-tag" select="$m-tag"/>
-					<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="not"   select="$not"/>
-				</xsl:call-template>
-			</xsl:otherwise>
-		</xsl:choose>
+		<xsl:call-template name="out_body">
+			<xsl:with-param name="c-tag" select="$c-tag"/>
+			<xsl:with-param name="m-tag" select="$m-tag"/>
+			<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="not"   select="$not"/>
+			<xsl:with-param name="const" select="$const"/>
+		</xsl:call-template>
 	</oxsl:template>
 </xsl:template>
 
@@ -282,30 +310,25 @@
 	<xsl:param name="m-tag"/>
 	<xsl:param name="c-tag"/>
 
-	<xsl:variable name="no_params_var">
-		<xsl:if test="$cook = 'true'">$no_params + </xsl:if>
-	</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>
-
-	<xsl:variable name="apply_not">
-		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
-	</xsl:variable>
-
-	<xsl:variable name="op_uri_attr">
-		<xsl:variable name="tmp_op_uri_attr">
-			<xsl:call-template name="op_uri_attr">
+		<xsl:variable name="match_op">
+			<xsl:call-template name="out_match_op">
 				<xsl:with-param name="not"   select="$not"/>
+				<xsl:with-param name="cook"  select="$cook"/>
+				<xsl:with-param name="uri"   select="$uri"/> 
 				<xsl:with-param name="c-tag" select="$c-tag"/>
 			</xsl:call-template>
 		</xsl:variable>
-		<xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
+		
+		<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:if test="$not = 'true'">*[2]/</xsl:if>
 	</xsl:variable>
 
 
@@ -314,21 +337,10 @@
 		<xsl:with-param name="name" select="$name"/>
 	</xsl:call-template>
 	
-	<oxsl:template match="{concat('APPLY[',$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:variable>
-		</xsl:if>	
+	<oxsl:template match="{$match}" mode="pure">
 		<oxsl:choose>
 			<xsl:for-each select="Case">
-				<oxsl:when test="{concat('count(',$apply_not,'*) = ',$no_params_var,@arity + $hide + 1)}">
+				<oxsl:when test="{concat('count(',$apply_not,'*) = ',@arity + $hide + 1)}">
 					<xsl:call-template name="out_body">
 						<xsl:with-param name="c-tag" select="$c-tag"/>
 						<xsl:with-param name="m-tag" select="$m-tag"/>
@@ -359,7 +371,12 @@
 <xsl:template name="out_match_op">
 	<xsl:param name="not"  select="'false'"/>
 	<xsl:param name="uri"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
+
+	<xsl:variable name="instantiate">
+		<xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+	</xsl:variable>
 	
 	<!-- application with not operator -->
 	<xsl:variable name="app_not">
@@ -374,100 +391,15 @@
 
 	<xsl:variable name="app_op">
 		<xsl:if test="$not = 'true'">APPLY[</xsl:if>
-		<xsl:value-of select="concat($c-tag,'[',$uris,']')"/>
+		<xsl:value-of select="concat($instantiate,$c-tag,'[',$uris,']')"/>
 		<xsl:if test="$not = 'true'">]</xsl:if>
 	</xsl:variable>
 
 	<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="not"    select="'false'"/>
 	<xsl:param name="mode"   select="'noannot'"/>
@@ -478,7 +410,6 @@
 			<xsl:call-template name="param">
 				<xsl:with-param name="id"    select="$params"/>
 				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="cook"  select="$cook"/>
 				<xsl:with-param name="hide"  select="$hide"/>
 			</xsl:call-template>
 		</xsl:variable>
@@ -487,7 +418,6 @@
 		
 		<xsl:call-template name="out_params">
 			<xsl:with-param name="params" select="$params + 1"/>
-			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="not"    select="$not"/>
 			<xsl:with-param name="mode"   select="$mode"/>
@@ -496,7 +426,6 @@
 	</xsl:if>
 </xsl:template>
 
-
 <xsl:template name="out_body">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -504,25 +433,30 @@
 	<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="cook"  select="$cook"/>
 					<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:variable name="helm:xref">
 			 	<xsl:call-template name="op_id_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<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>
 		
@@ -539,8 +473,7 @@
 				</xsl:element>
 				<!--            PARAMS            -->
 				<xsl:call-template name="out_params">
-					<xsl:with-param name="cook"   select="$cook"/>
-					<xsl:with-param name="hide"   select="$hide"/>	
+					<xsl:with-param name="hide"   select="$hide"/>					
 					<xsl:with-param name="not"    select="$not"/>
 					<xsl:with-param name="arity"  select="$arity"/>
 				</xsl:call-template>
@@ -554,11 +487,13 @@
 				<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:template>
 
+
 <xsl:template name="out_mvar">
 	<xsl:param name="vname"/>
 	
@@ -578,7 +513,6 @@
 <xsl:template name="out_choose_binder">
 	<xsl:param name="binded_params" select="''"/>
 	<xsl:param name="not"           select="'false'"/>
-	<xsl:param name="cook"          select="'false'"/>
 	<xsl:param name="hide"          select="0"/>
 	<xsl:param name="binder"/>
 	
@@ -588,7 +522,6 @@
 				<xsl:call-template name="out_choose_binder">
 					<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
 					<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="binder"        select="$binder"/>
 				</xsl:call-template>
@@ -596,7 +529,6 @@
 				<xsl:call-template name="out_choose_binder">
 					<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
 					<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="binder"        select="$binder"/>
 				</xsl:call-template>
@@ -606,7 +538,6 @@
 					<xsl:call-template name="param">
 						<xsl:with-param name="id"    select="$binded_params"/>
 						<xsl:with-param name="not"   select="$not"/>
-						<xsl:with-param name="cook"  select="$cook"/>
 						<xsl:with-param name="hide"  select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -619,6 +550,7 @@
 	</xsl:if>
 </xsl:template>
 
+
 <!-- *********************************************************************** -->
 <!--                     META LANGUAGE FOR MathML                            --> 
 <!-- *********************************************************************** -->
@@ -629,6 +561,7 @@
 	<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>
@@ -636,21 +569,27 @@
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@xref"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
+					<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="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>
 
 	<m:apply helm:xref="{$helm:xref}">
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"   select="$cook"/>
 			<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:with-param name="ignore" select="'xref'"/>
 		</xsl:call-template>
 	
@@ -660,17 +599,18 @@
 			<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:template match="mop">
 	<xsl:param name="c-tag"/>
 	<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'"/>
 
 	<!-- set definitonURL attribute -->
 	<xsl:variable name="definitionURL">
@@ -678,17 +618,20 @@
 			<xsl:when test="@definitionURL">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@definitionURL"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<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:when>
 			<xsl:otherwise>
 				<xsl:call-template name="op_uri_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<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>
@@ -700,17 +643,20 @@
 			<xsl:when test="@xref">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@xref"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<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:when>
 			<xsl:otherwise>
 				<xsl:call-template name="op_id_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<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>
@@ -725,10 +671,12 @@
 		</xsl:attribute>
 		
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"   select="$cook"/>
 			<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:with-param name="ignore" select="'xref + definitionURL + tag'"/>
 		</xsl:call-template>
 		
@@ -738,12 +686,13 @@
 			<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:template match="param">
-	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="hide" select="0"/>
 	<xsl:param name="not"  select="'false'"/>
 
@@ -751,7 +700,6 @@
 		<xsl:call-template name="param">
 			<xsl:with-param name="id"    select="@id"/>
 			<xsl:with-param name="not"   select="$not"/>
-			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 		</xsl:call-template>
 	</xsl:variable>
@@ -779,19 +727,23 @@
 	</xsl:choose>
 </xsl:template>
 
+
 <xsl:template match="m:*">
 	<xsl:param name="c-tag"/>
 	<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:copy>
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"  select="$cook"/>
 			<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:apply-templates>
@@ -800,16 +752,19 @@
 			<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:template match="mbvar">
 	<xsl:param name="c-tag"/>
 	<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:variable name="binded_params">
 		<xsl:call-template name="get_binded_params">
@@ -822,12 +777,11 @@
 		<xsl:call-template name="test_on_lambda">
 			<xsl:with-param name="binded_params" select="$binded_params"/>
 			<xsl:with-param name="not"           select="$not"/>
-			<xsl:with-param name="cook"          select="$cook"/>
 			<xsl:with-param name="hide"          select="$hide"/>
 		</xsl:call-template>
 	</xsl:variable>
 
-	<xsl:variable name="binder">/target/@binder</xsl:variable>
+	<xsl:variable name="binder">/decl/@binder</xsl:variable>
 
 	<xsl:choose>
 		<xsl:when test="$binded_params != ''">
@@ -844,11 +798,10 @@
 											<xsl:with-param name="binded_params" select="$binded_params"/>
 											<xsl:with-param name="not"           select="$not"/>
 											<xsl:with-param name="hide"          select="$hide"/>
-											<xsl:with-param name="cook"          select="$cook"/>
 											<xsl:with-param name="binder"        select="$binder"/>
 										</xsl:call-template>
 									</oxsl:choose>
-								</oxsl:variable>
+ 								</oxsl:variable>
 								<oxsl:call-template name="insert_subscript">
 									<oxsl:with-param name="node_value" select="$binder"/>
 								</oxsl:call-template>
@@ -859,11 +812,10 @@
 									<xsl:call-template name="param">
 										<xsl:with-param name="id"    select="$binded_params"/>
 										<xsl:with-param name="not"   select="$not"/>
-										<xsl:with-param name="cook"  select="$cook"/>
 										<xsl:with-param name="hide"  select="$hide"/>
 									</xsl:call-template>
-								</xsl:variable>
-							
+								</xsl:variable>								
+
 								<oxsl:call-template name="insert_subscript">
 									<oxsl:with-param name="node_value" select="{concat($param,$binder)}"/>
 								</oxsl:call-template>
@@ -887,6 +839,7 @@
 					<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>
@@ -901,12 +854,15 @@
 					<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:choose>
 </xsl:template>
 
+
+
 <xsl:template match="mvar">
 	<xsl:call-template name="out_mvar">
 		<xsl:with-param name="vname" select="@name"/>
@@ -914,7 +870,6 @@
 </xsl:template>
 
 
-
 <!-- *********************************************************************** -->
 <!--                          AUXILIARY FUNCTIONS                            -->
 <!-- *********************************************************************** -->
@@ -1034,7 +989,6 @@
 <xsl:template name="test_on_lambda">
 	<xsl:param name="binded_params" select="''"/>
 	<xsl:param name="not"           select="'false'"/>
-	<xsl:param name="cook"          select="'false'"/>
 	<xsl:param name="hide"          select="0"/>
 	
 	<xsl:if test="$binded_params != ''">
@@ -1044,7 +998,6 @@
 					<xsl:call-template name="test_on_lambda">
 						<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
 						<xsl:with-param name="not"           select="$not"/>
-						<xsl:with-param name="cook"          select="$cook"/>
 						<xsl:with-param name="hide"          select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1053,7 +1006,6 @@
 					<xsl:call-template name="test_on_lambda">
 						<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
 						<xsl:with-param name="not"           select="$not"/>
-						<xsl:with-param name="cook"          select="$cook"/>
 						<xsl:with-param name="hide"          select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1065,7 +1017,6 @@
 					<xsl:call-template name="param">
 						<xsl:with-param name="id"    select="$binded_params"/>
 						<xsl:with-param name="not"   select="$not"/>
-						<xsl:with-param name="cook"  select="$cook"/>
 						<xsl:with-param name="hide"  select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1170,29 +1121,26 @@
 <xsl:template name="param">
 	<xsl:param name="id"/>
 	<xsl:param name="not"   select="'false'"/>
-	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="hide"  select="0"/>
 
 	<xsl:variable name="apply_not">
 		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
 	</xsl:variable>
 
-	<xsl:variable name="no_params_var">
-		<xsl:if test="$cook = 'true'">$no_params+</xsl:if>
-	</xsl:variable>
-
-	<xsl:value-of select="concat($apply_not,'*[',$no_params_var,$id + $hide + 1,']')"/>
+	<xsl:value-of select="concat($apply_not,'*[',$id + $hide + 1,']')"/>
 </xsl:template>
 
 <!-- Returns a xpath string with the location of the operator uri attribute -->
 <xsl:template name="op_uri_attr">
 	<xsl:param name="not"   select="'false'"/>
+	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
 
 	<xsl:call-template name="op_attr">
 		<xsl:with-param name="attr_type" select="'@uri'"/>
 		<xsl:with-param name="not"       select="$not"/>
+		<xsl:with-param name="cook"      select="$cook"/>
 		<xsl:with-param name="c-tag"     select="$c-tag"/>
 		<xsl:with-param name="const"     select="$const"/>
 	</xsl:call-template>
@@ -1201,12 +1149,14 @@
 <!-- Returns a xpath string with the location of the operator id attribute -->
 <xsl:template name="op_id_attr">
 	<xsl:param name="not"  select="'false'"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
 	
 	<xsl:call-template name="op_attr">
 		<xsl:with-param name="attr_type" select="'@id'"/>
 		<xsl:with-param name="not"       select="$not"/>
+		<xsl:with-param name="cook"      select="$cook"/>
 		<xsl:with-param name="c-tag"     select="$c-tag"/>
 		<xsl:with-param name="const"     select="$const"/>
 	</xsl:call-template>
@@ -1217,8 +1167,13 @@
 <xsl:template name="op_attr">
 	<xsl:param name="attr_type"/>
 	<xsl:param name="not"  select="'false'"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
+	
+	<xsl:variable name="instantiate">
+		<xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+	</xsl:variable>
 
 	<xsl:variable name="apply">
 		<xsl:if test="$not = 'true'">APPLY/</xsl:if>
@@ -1229,16 +1184,18 @@
 			<xsl:value-of select="concat('{',$attr_type,'}')"/>	
 		</xsl:when>
 		<xsl:otherwise>
-			<xsl:value-of select="concat('{',$apply,$c-tag,'/',$attr_type,'}')"/> 			
+			<xsl:value-of select="concat('{',$apply,$instantiate,$c-tag,'/',$attr_type,'}')"/> 			
 		</xsl:otherwise>
 	</xsl:choose>
 </xsl:template>
 
 <xsl:template name="copy_attributes">
+	<xsl:param name="cook"   select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<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">
@@ -1249,13 +1206,24 @@
 	
 	<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="cook"  select="$cook"/>
 					<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>
@@ -1284,12 +1252,16 @@
 <xsl:template name="set_attribute">
 	<xsl:param name="attr"/>
 	<xsl:param name="c-tag"/>
+	<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>
-		<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>
@@ -1297,12 +1269,13 @@
 					<xsl:otherwise>@uri</xsl:otherwise>
 				</xsl:choose>
 			</xsl:variable>
-
+			
 			<xsl:call-template name="op_attr">
 				<xsl:with-param name="attr_type" select="$attr_type"/>
 				<xsl:with-param name="not"       select="$not"/>
+				<xsl:with-param name="cook"      select="$cook"/>
 				<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>