helm/style/objcontent.xsl.csc

   1 <?xml version="1.0"?>
   2
   3 <!--******************************************************************-->
   4 <!-- XSLT version 0.1 of CIC objects to objects and MathML content:   -->
   5 <!-- First draft: March 21 2000, Irene Schena                         -->
   6 <!--******************************************************************-->
   7
   8 <!--******************************************************************-->
   9 <!-- MANCA: gestione annotation e linking                             -->
  10 <!--******************************************************************-->
  11
  12 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  13                               xmlns:m="http://www.w3.org/1998/Math/MathML">
  14
  15 <xsl:import href="content.xsl"/>
  16
  17 <!-- ROOT -->
  18
  19 <xsl:template match="cicxml">
  20     <xsl:variable name="url"><xsl:value-of select="@baseurl"/></xsl:variable>
  21     <xsl:variable name="stylesheet"><xsl:value-of select="@stylesheet"/></xsl:variable>
  22     <xsl:processing-instruction name="cocoon-format">type="text/xml"</xsl:processing-instruction>
  23     <xsl:processing-instruction name="xml-stylesheet">href="<xsl:value-of select='concat($url,$stylesheet)'/>" type="text/xsl"</xsl:processing-instruction>
  24     <xsl:processing-instruction name="cocoon-process">type="xslt"</xsl:processing-instruction>
  25     <xsl:apply-templates/>
  26 </xsl:template>
  27
  28 <!-- CIC OBJECTS -->
  29
  30 <xsl:template match="Definition" mode="noannot">
  31     <Definition name="{@name}">
  32      <xsl:if test="string(@params) != &quot;&quot;">
  33       <Params>
  34        <xsl:value-of select="@params"/>
  35       </Params>
  36      </xsl:if>
  37      <body>
  38        <xsl:apply-templates select="body/*[1]">
  39         <xsl:with-param name="backpointer" select="&quot;*[1]&quot;"/>
  40        </xsl:apply-templates>
  41      </body>
  42      <type>
  43        <xsl:apply-templates select="type/*[1]">
  44         <xsl:with-param name="backpointer" select="&quot;*[2]&quot;"/>
  45        </xsl:apply-templates>
  46      </type>
  47     </Definition>
  48 </xsl:template>
  49
  50 <xsl:template match="Axiom" mode="noannot">
  51     <Axiom name="{@name}">
  52      <xsl:if test="string(@params) != &quot;&quot;">
  53       <Params>
  54        <xsl:value-of select="@params"/>
  55       </Params>
  56      </xsl:if>
  57      <type>
  58        <xsl:apply-templates select="type"/>
  59      </type>
  60     </Axiom>
  61 </xsl:template>
  62
  63 <xsl:template match="CurrentProof" mode="noannot">
  64     <CurrentProof name="{@name}">
  65      <xsl:for-each select="Conjecture">
  66       <Conjecture no="./{@no}">
  67         <xsl:apply-templates select="."/>
  68       </Conjecture>
  69      </xsl:for-each>
  70      <body>
  71        <xsl:apply-templates select="body"/>
  72      </body>
  73      <type>
  74        <xsl:apply-templates select="type"/>
  75      </type>
  76     </CurrentProof>
  77 </xsl:template>
  78
  79 <xsl:template match="InductiveDefinition" mode="noannot">
  80     <InductiveDefinition>
  81      <xsl:if test="string(@params) != &quot;&quot;">
  82       <Params>
  83        <xsl:value-of select="@params"/>
  84       </Params>
  85      </xsl:if>
  86      <xsl:if test="string(@noParams) != 0">
  87       <xsl:apply-templates select="InductiveType/arity/*[1]" mode="abstparams">
  88        <xsl:with-param name="noparams" select="@noParams"/>
  89       </xsl:apply-templates>
  90      </xsl:if>
  91      <xsl:for-each select="InductiveType">
  92       <InductiveType name="{./@name}" inductive="{./@inductive}">
  93        <arity>
  94          <xsl:apply-templates select="./arity/*[1]" mode="abstparams">
  95           <xsl:with-param name="noparams" select="../@noParams"/>
  96           <xsl:with-param name="target" select="1"/>
  97          </xsl:apply-templates>
  98        </arity>
  99        <xsl:for-each select="./Constructor">
 100         <Constructor name="{./@name}">
 101           <xsl:apply-templates select="./*[1]" mode="abstparams">
 102            <xsl:with-param name="noparams" select="../../@noParams"/>
 103            <xsl:with-param name="target" select="1"/>
 104           </xsl:apply-templates>
 105         </Constructor>
 106        </xsl:for-each>
 107       </InductiveType>
 108      </xsl:for-each>
 109     </InductiveDefinition>
 110 </xsl:template>
 111
 112 <xsl:template match="Variable" mode="noannot">
 113     <Variable name="{@name}">
 114      <type>
 115        <xsl:apply-templates select="type"/>
 116      </type>
 117     </Variable>
 118 </xsl:template>
 119
 120 <!--*******************************************-->
 121 <!--    ABSTRACTING PARAMETERS AND COUNTING    -->
 122 <!--*******************************************-->
 123 <!-- Si dimentica i CAST dei termini che astrae. Nel caso dell'astrazione -->
 124 <!-- dei lambda dei pattern del CASE, qualora i lambda non si trovino     -->
 125 <!-- nella forma weak-head, astrae solo i lambda che trova e restituisce  -->
 126 <!-- un corpo depurato da tutti i primi cast che precedono il termine     -->
 127 <!-- restituito.                                                          -->
 128
 129 <xsl:template match="*" mode="abstparams">
 130 <xsl:param name="noparams" select="0"/>
 131 <xsl:param name="target" select="0"/>
 132 <xsl:param name="binder">PROD</xsl:param>
 133     <xsl:choose>
 134     <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)=&quot;CAST&quot;))">
 135      <xsl:choose>
 136      <xsl:when test="name(.) = string($binder)">
 137       <xsl:if test="$target = 0">
 138        <xsl:choose>
 139        <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
 140         <m:ci>
 141          <xsl:value-of select="target/@binder"/>
 142         </m:ci>
 143        </xsl:when>
 144        <xsl:otherwise>
 145         <Param name="{target/@binder}">
 146          <xsl:apply-templates select="source" mode="noannot"/>
 147         </Param>
 148        </xsl:otherwise>
 149        </xsl:choose>
 150       </xsl:if>
 151       <xsl:apply-templates select="target/*[1]" mode="abstparams">
 152        <xsl:with-param name="noparams" select="$noparams - 1"/>
 153        <xsl:with-param name="target" select="$target"/>
 154        <xsl:with-param name="binder" select="$binder"/>
 155       </xsl:apply-templates>
 156      </xsl:when>
 157      <xsl:otherwise>
 158       <xsl:apply-templates select="term/*[1]" mode="abstparams">
 159        <xsl:with-param name="noparams" select="$noparams"/>
 160        <xsl:with-param name="target" select="$target"/>
 161        <xsl:with-param name="binder" select="$binder"/>
 162       </xsl:apply-templates>
 163      </xsl:otherwise>
 164      </xsl:choose>
 165     </xsl:when>
 166     <xsl:otherwise>
 167      <xsl:choose>
 168      <xsl:when test="($target = 1) and ($noparams != 0)">
 169       <m:apply>
 170       <m:csymbol>app</m:csymbol>
 171       <xsl:apply-templates select="." mode="noannot"/>
 172       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
 173       </m:apply>
 174      </xsl:when>
 175      <xsl:otherwise>
 176       <xsl:choose>
 177       <xsl:when test="$noparams != 0">
 178       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
 179       </xsl:when>
 180       <xsl:otherwise>
 181        <xsl:if test="$target = 1">
 182         <xsl:apply-templates select="." mode="noannot"/>
 183        </xsl:if>
 184       </xsl:otherwise>
 185       </xsl:choose>
 186      </xsl:otherwise>
 187      </xsl:choose>
 188     </xsl:otherwise>
 189     </xsl:choose>
 190 </xsl:template>
 191
 192 <xsl:template name="printparam">
 193 <xsl:param name="noleft" select="0"/>
 194 <xsl:param name="number" select="1"/>
 195     <xsl:if test="$noleft != 0">
 196      <m:ci>$<xsl:value-of select="$number"/></m:ci>
 197      <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noleft - 1"/><xsl:with-param name="number" select="$number + 1"/></xsl:call-template>
 198     </xsl:if>
 199 </xsl:template>
 200
 201 <xsl:template match="*" mode="counting">
 202 <xsl:param name="noparams" select="0"/>
 203 <xsl:param name="count" select="0"/>
 204  <xsl:choose>
 205  <xsl:when test="name(.) = &quot;PROD&quot;">
 206   <xsl:apply-templates select="target/*[1]" mode="counting">
 207    <xsl:with-param name="noparams" select="$noparams"/>
 208    <xsl:with-param name="count" select="$count + 1"/>
 209   </xsl:apply-templates>
 210  </xsl:when>
 211  <xsl:when test="name(.) = &quot;CAST&quot;">
 212   <xsl:apply-templates select="term/*[1]" mode="counting">
 213    <xsl:with-param name="noparams" select="$noparams"/>
 214    <xsl:with-param name="count" select="$count"/>
 215   </xsl:apply-templates>
 216  </xsl:when>
 217  <xsl:otherwise>
 218   <xsl:value-of select="$count - $noparams"/>
 219  </xsl:otherwise>
 220  </xsl:choose>
 221 </xsl:template>
 222
 223 </xsl:stylesheet>