]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/params.xsl
added html templates and pages
[helm.git] / helm / style / params.xsl
index b5b7f9b88ee7357497be3ec9d189cc76bf11245e..1b5f4167064ad29292eba15569bda9ebbbfdd021 100644 (file)
 <!-- CSC: PROBLEMA: URI CHE NON CONTENGONO / ED INIZIANO CON cic: -->
 <xsl:template name="name_of_uri">
  <xsl:param name="uri" select="&quot;&quot;"/>
+ <xsl:param name="extension" select="'.con'"/>
  <xsl:variable name="suffix" select="substring-after($uri, &quot;/&quot;)"/>
  <xsl:choose>
   <xsl:when test="$suffix = &quot;&quot;">
    <!-- CSC: PROBLEMA: .con PUO' APPARIRE ALL'INTERNO DELLE URI ===>
      SCRIVERE UNA FUNZIONE RICORSIVA CHE RISOLVA -->
-   <xsl:value-of select="substring-before($uri,&quot;.con&quot;)"/>
+   <xsl:value-of select="substring-before($uri,$extension)"/>
   </xsl:when>
   <xsl:otherwise>
    <xsl:call-template name="name_of_uri">
     <xsl:with-param name="uri" select="$suffix"/>
+    <xsl:with-param name="extension" select="$extension"/> 
    </xsl:call-template>
   </xsl:otherwise>
  </xsl:choose>
  </xsl:choose>   
 </xsl:template>
 
+<!-- path gives the path of a uri, up to the final name -->
+<xsl:template name="path">
+ <xsl:param name="uri" select="&quot;&quot;"/>
+ <xsl:param name="current_path" select="&quot;&quot;"/>
+ <xsl:choose>
+  <xsl:when test="(substring-after($uri,&quot;/&quot;) != &quot;&quot;)">
+   <xsl:call-template name="path">
+    <xsl:with-param 
+        name="uri" select="substring-after($uri,&quot;/&quot;)"/>
+    <xsl:with-param
+        name="current_path" select="concat($current_path,substring-before($uri,&quot;/&quot;),'/')"/> 
+   </xsl:call-template>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="$current_path"/>
+  </xsl:otherwise>
+ </xsl:choose>   
+</xsl:template>
+
 <xsl:template name="blank_counting">
  <xsl:param name="string" select="&quot;&quot;"/>
  <xsl:param name="counter" select="0"/>
     <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)=&quot;CAST&quot;))">
      <xsl:choose>
      <xsl:when test="name(.) = string($binder)">
-      <xsl:if test="$target = 0">
-       <xsl:choose>
-       <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
-        <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
-        </m:ci>
+      <xsl:choose>
+       <xsl:when test="$noparams >= count(decl)">
+        <xsl:for-each select="decl">
+         <xsl:if test="$target = 0">
+          <xsl:choose>
+          <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
+           <m:ci>
+            <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+           </m:ci>
+          </xsl:when>
+          <xsl:otherwise> 
+           <Param name="{@binder}">
+            <xsl:apply-templates select="*[1]"/>
+           </Param>
+          </xsl:otherwise>
+          </xsl:choose>
+         </xsl:if> 
+       </xsl:for-each>
+        <xsl:apply-templates select="target/*[1]" mode="abstparams">
+         <xsl:with-param name="noparams" select="$noparams - count(decl)"/>
+         <xsl:with-param name="target" select="$target"/>
+         <xsl:with-param name="binder" select="$binder"/>
+        </xsl:apply-templates>
        </xsl:when>
-       <xsl:otherwise> 
-        <Param name="{target/@binder}">
-         <xsl:apply-templates select="source"/>
-        </Param>
+       <xsl:otherwise>
+        <xsl:for-each select="decl[$noparams >= position()]">
+         <xsl:if test="$target = 0">
+          <xsl:choose>
+          <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
+           <m:ci>
+            <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+           </m:ci>
+          </xsl:when>
+          <xsl:otherwise> 
+           <Param name="{@binder}">
+            <xsl:apply-templates select="*[1]"/>
+           </Param>
+          </xsl:otherwise>
+          </xsl:choose>
+         </xsl:if> 
+       </xsl:for-each>
+        <xsl:if test="$target = 1">
+         <xsl:choose>
+         <xsl:when test="name(.)=&quot;PROD&quot;">
+          <xsl:apply-templates select="decl[position()=$noparams+1]" mode="prod"/>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:apply-templates select="decl[position()=$noparams+1]" mode="lambda_prop"/>
+         </xsl:otherwise>
+        </xsl:choose>
+        </xsl:if>
        </xsl:otherwise>
-       </xsl:choose>
-      </xsl:if>
-      <xsl:apply-templates select="target/*[1]" mode="abstparams">
-       <xsl:with-param name="noparams" select="$noparams - 1"/>
-       <xsl:with-param name="target" select="$target"/>
-       <xsl:with-param name="binder" select="$binder"/>
-      </xsl:apply-templates>
+      </xsl:choose>
      </xsl:when>
      <xsl:otherwise>
       <xsl:apply-templates select="term/*[1]" mode="abstparams">
  <xsl:when test="name(.) = &quot;PROD&quot;">
   <xsl:apply-templates select="target/*[1]" mode="counting">
    <xsl:with-param name="noparams" select="$noparams"/>
-   <xsl:with-param name="count" select="$count + 1"/>
+   <xsl:with-param name="count" select="$count + count(decl)"/> 
   </xsl:apply-templates>
  </xsl:when>
  <xsl:when test="name(.) = &quot;CAST&quot;">