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