helm/style/set.xsl

   1 <?xml version="1.0"?>
   2
   3 <!--******************************************************************-->
   4 <!-- Basic Set Theory                                                 -->
   5 <!-- First draft: April 3 2000                                        -->
   6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
   7 <!--******************************************************************-->
   8
   9 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  10                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  11                               xmlns:helm="http://www.cs.unibo.it/helm">
  12
  13 <!--******************************************************************-->
  14 <!-- Variable containing the absolute path of the CIC file            -->
  15 <!--******************************************************************-->
  16
  17 <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>
  18
  19 <!-- ************************* LOGIC *********************************-->
  20
  21
  22
  23 <xsl:template match="*" mode="set">
  24     <xsl:choose>
  25      <xsl:when test="name() = 'LAMBDA'">
  26       <m:set>
  27        <m:bvar>
  28         <m:ci>
  29          <xsl:value-of select="target/@binder"/>
  30         </m:ci>
  31         <m:type>
  32          <xsl:apply-templates select="source" mode="noannot"/>
  33         </m:type>
  34        </m:bvar>
  35        <m:condition>
  36         <xsl:apply-templates select="target" mode="noannot"/>
  37        </m:condition>
  38       </m:set>
  39      </xsl:when>
  40      <xsl:otherwise>
  41       <xsl:apply-templates select="." mode="noannot"/>
  42      </xsl:otherwise>
  43     </xsl:choose>
  44 </xsl:template>
  45
  46
  47 <!-- IN -->
  48
  49 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]" mode="pure">
  50     <xsl:variable name="no_params">
  51      <xsl:call-template name="get_no_params">
  52       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
  53       <xsl:with-param name="second_uri" select="CONST/@uri"/>
  54      </xsl:call-template>
  55     </xsl:variable>
  56     <xsl:choose>
  57      <xsl:when test="(count(child::*) - number($no_params)) = 3">
  58       <m:apply helm:xref="{@id}">
  59        <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
  60        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
  61        <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
  62        <xsl:apply-templates select="*[2+$no_params]" mode="set" />
  63       </m:apply>
  64      </xsl:when>
  65      <xsl:otherwise>
  66       <xsl:apply-imports/>
  67      </xsl:otherwise>
  68     </xsl:choose>
  69 </xsl:template>
  70
  71
  72 <!-- NOT-IN -->
  73 <!-- NOT ha no parameters -->
  74 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
  75 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]]" mode="pure">
  76     <xsl:variable name="no_params">
  77      <xsl:call-template name="get_no_params">
  78       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
  79       <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
  80      </xsl:call-template>
  81     </xsl:variable>
  82     <xsl:choose>
  83      <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
  84       <m:apply helm:xref="{@id}">
  85        <m:notin/>
  86        <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
  87   <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
  88        <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
  89       </m:apply>
  90      </xsl:when>
  91      <xsl:otherwise>
  92       <xsl:apply-imports/>
  93      </xsl:otherwise>
  94     </xsl:choose>
  95 </xsl:template>
  96
  97 <!-- EMPTY SET -->
  98
  99 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
 100     <xsl:variable name="no_params">
 101      <xsl:call-template name="get_no_params">
 102       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 103       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 104      </xsl:call-template>
 105     </xsl:variable>
 106     <xsl:choose>
 107      <xsl:when test="(count(child::*) - number($no_params)) = 1">
 108       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 109       </m:set>
 110      </xsl:when>
 111      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 112       <m:apply helm:xref="{@id}">
 113        <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
 114        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 115        <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 116        </m:set>
 117       </m:apply>
 118      </xsl:when>
 119      <xsl:otherwise>
 120       <xsl:apply-imports/>
 121      </xsl:otherwise>
 122     </xsl:choose>
 123 </xsl:template>
 124
 125 <!-- SINGLETON -->
 126
 127 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
 128     <xsl:variable name="no_params">
 129      <xsl:call-template name="get_no_params">
 130       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 131       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 132      </xsl:call-template>
 133     </xsl:variable>
 134     <xsl:choose>
 135      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 136       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 137        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 138       </m:set>
 139      </xsl:when>
 140      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 141       <m:apply helm:xref="{@id}">
 142        <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
 143        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 144        <m:set definitionURL="{MUTIND/@uri}">
 145         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 146        </m:set>
 147       </m:apply>
 148      </xsl:when>
 149      <xsl:otherwise>
 150       <xsl:apply-imports/>
 151      </xsl:otherwise>
 152     </xsl:choose>
 153 </xsl:template>
 154
 155 <!-- COUPLE -->
 156
 157 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Couple.ind']]" mode="pure">
 158     <xsl:variable name="no_params">
 159      <xsl:call-template name="get_no_params">
 160       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 161       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 162      </xsl:call-template>
 163     </xsl:variable>
 164     <xsl:choose>
 165      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 166       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 167        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 168        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 169       </m:set>
 170      </xsl:when>
 171      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 172       <m:apply helm:xref="{@id}">
 173        <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
 174        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 175        <m:set definitionURL="{MUTIND/@uri}">
 176         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 177         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 178        </m:set>
 179       </m:apply>
 180      </xsl:when>
 181      <xsl:otherwise>
 182       <xsl:apply-imports/>
 183      </xsl:otherwise>
 184     </xsl:choose>
 185 </xsl:template>
 186
 187 <!-- TRIPLE -->
 188
 189 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
 190     <xsl:variable name="no_params">
 191      <xsl:call-template name="get_no_params">
 192       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 193       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 194      </xsl:call-template>
 195     </xsl:variable>
 196     <xsl:choose>
 197      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 198       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 199        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 200        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 201        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 202       </m:set>
 203      </xsl:when>
 204      <xsl:when test="(count(child::*) - number($no_params)) = 5">
 205       <m:apply helm:xref="{@id}">
 206        <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
 207        <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
 208        <m:set definitionURL="{MUTIND/@uri}">
 209         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 210         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 211         <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 212        </m:set>
 213       </m:apply>
 214      </xsl:when>
 215      <xsl:otherwise>
 216       <xsl:apply-imports/>
 217      </xsl:otherwise>
 218     </xsl:choose>
 219 </xsl:template>
 220
 221 <!-- INTERSECTION -->
 222
 223 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
 224     <xsl:variable name="no_params">
 225      <xsl:call-template name="get_no_params">
 226       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 227       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 228      </xsl:call-template>
 229     </xsl:variable>
 230     <xsl:choose>
 231      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 232       <m:apply helm:xref="{@id}">
 233        <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 234        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 235        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 236       </m:apply>
 237      </xsl:when>
 238      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 239       <m:apply helm:xref="{@id}">
 240        <m:in/>
 241        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 242        <m:apply>
 243         <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 244         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 245         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 246        </m:apply>
 247       </m:apply>
 248      </xsl:when>
 249      <xsl:otherwise>
 250       <xsl:apply-imports/>
 251      </xsl:otherwise>
 252     </xsl:choose>
 253 </xsl:template>
 254
 255
 256 <!-- UNION -->
 257
 258 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Union.ind']]" mode="pure">
 259     <xsl:variable name="no_params">
 260      <xsl:call-template name="get_no_params">
 261       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 262       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 263      </xsl:call-template>
 264     </xsl:variable>
 265     <xsl:choose>
 266      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 267       <m:apply helm:xref="{@id}">
 268        <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 269        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 270        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 271       </m:apply>
 272      </xsl:when>
 273      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 274       <m:apply helm:xref="{@id}">
 275        <m:in/>
 276        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 277        <m:apply>
 278         <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 279         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 280         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 281        </m:apply>
 282       </m:apply>
 283      </xsl:when>
 284      <xsl:otherwise>
 285       <xsl:apply-imports/>
 286      </xsl:otherwise>
 287     </xsl:choose>
 288 </xsl:template>
 289
 290 <!-- INCLUDED -->
 291
 292 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Included.con']]" mode="pure">
 293     <xsl:variable name="no_params">
 294      <xsl:call-template name="get_no_params">
 295       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 296       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 297      </xsl:call-template>
 298     </xsl:variable>
 299     <xsl:choose>
 300      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 301       <m:apply helm:xref="{@id}">
 302        <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 303        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 304        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 305       </m:apply>
 306      </xsl:when>
 307      <xsl:otherwise>
 308       <xsl:apply-imports/>
 309      </xsl:otherwise>
 310     </xsl:choose>
 311 </xsl:template>
 312
 313 <!-- STRICTLY INCLUDED -->
 314
 315 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
 316     <xsl:variable name="no_params">
 317      <xsl:call-template name="get_no_params">
 318       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 319       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 320      </xsl:call-template>
 321     </xsl:variable>
 322     <xsl:choose>
 323      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 324       <m:apply helm:xref="{@id}">
 325        <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 326        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 327        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 328       </m:apply>
 329      </xsl:when>
 330      <xsl:otherwise>
 331       <xsl:apply-imports/>
 332      </xsl:otherwise>
 333     </xsl:choose>
 334 </xsl:template>
 335
 336 <!-- SET-DIFF -->
 337
 338 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Setminus.con']]" mode="pure">
 339     <xsl:variable name="no_params">
 340      <xsl:call-template name="get_no_params">
 341       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 342       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 343      </xsl:call-template>
 344     </xsl:variable>
 345     <xsl:choose>
 346      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 347       <m:apply helm:xref="{@id}">
 348        <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 349        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 350        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 351       </m:apply>
 352      </xsl:when>
 353      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 354       <m:apply helm:xref="{@id}">
 355        <m:in/>
 356        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 357        <m:apply>
 358         <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 359         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 360         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 361        </m:apply>
 362       </m:apply>
 363      </xsl:when>
 364      <xsl:otherwise>
 365       <xsl:apply-imports/>
 366      </xsl:otherwise>
 367     </xsl:choose>
 368 </xsl:template>
 369
 370 <!-- ADD-ELEM -->
 371
 372 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Add.con']]" mode="pure">
 373     <xsl:variable name="no_params">
 374      <xsl:call-template name="get_no_params">
 375       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 376       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 377      </xsl:call-template>
 378     </xsl:variable>
 379     <xsl:choose>
 380      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 381       <m:apply helm:xref="{@id}">
 382        <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 383        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 384        <m:set>
 385         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 386        </m:set>
 387       </m:apply>
 388      </xsl:when>
 389      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 390       <m:apply helm:xref="{@id}">
 391        <m:in/>
 392        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 393        <m:apply>
 394         <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 395         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 396         <m:set>
 397          <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 398         </m:set>
 399        </m:apply>
 400       </m:apply>
 401      </xsl:when>
 402      <xsl:otherwise>
 403       <xsl:apply-imports/>
 404      </xsl:otherwise>
 405     </xsl:choose>
 406 </xsl:template>
 407
 408 <!-- SUBTRACT-ELEM -->
 409
 410 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Subtract.con']]" mode="pure">
 411     <xsl:variable name="no_params">
 412      <xsl:call-template name="get_no_params">
 413       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 414       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 415      </xsl:call-template>
 416     </xsl:variable>
 417     <xsl:choose>
 418      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 419       <m:apply helm:xref="{@id}">
 420        <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 421        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 422        <m:set>
 423         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 424        </m:set>
 425       </m:apply>
 426      </xsl:when>
 427      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 428       <m:apply helm:xref="{@id}">
 429        <m:in/>
 430        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 431        <m:apply>
 432         <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 433         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 434         <m:set>
 435          <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 436         </m:set>
 437        </m:apply>
 438       </m:apply>
 439      </xsl:when>
 440      <xsl:otherwise>
 441       <xsl:apply-imports/>
 442      </xsl:otherwise>
 443     </xsl:choose>
 444 </xsl:template>
 445
 446 <!-- CARD -->
 447
 448 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
 449     <xsl:variable name="no_params">
 450      <xsl:call-template name="get_no_params">
 451       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
 452       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 453      </xsl:call-template>
 454     </xsl:variable>
 455     <xsl:choose>
 456      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 457       <m:apply helm:xref="{@id}">
 458        <m:eq/>
 459        <m:apply>
 460         <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 461         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 462        </m:apply>
 463        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 464       </m:apply>
 465      </xsl:when>
 466      <xsl:otherwise>
 467       <xsl:apply-imports/>
 468      </xsl:otherwise>
 469     </xsl:choose>
 470 </xsl:template>
 471
 472 </xsl:stylesheet>