helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl

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