helm/nuprl_stylesheets/nuprl_term.xsl

   1 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
   2                               xmlns:m="http://www.w3.org/1998/Math/MathML">
   3
   4 <xsl:include href="nuprl_proof.xsl"/>
   5 <xsl:include href="nuprl_abstract.xsl"/>
   6 <xsl:include href="nuprl_rules.xsl"/>
   7
   8 <!-- NuPrl Term -->
   9 <xsl:template match="var">
  10   <m:ci>
  11     <xsl:value-of select="@val"/>
  12   </m:ci>
  13 </xsl:template>
  14
  15
  16 <xsl:template match="function">
  17   <xsl:choose>
  18   <xsl:when test="type_of">
  19     <xsl:choose>
  20     <xsl:when test="type_of/@var=&quot;&quot;">
  21     <m:apply>
  22       <m:csymbol>arrow</m:csymbol>
  23       <xsl:apply-templates select="type_of/*"/>
  24       <xsl:apply-templates select="*[2]"/>
  25     </m:apply>
  26   </xsl:when>
  27   <xsl:otherwise>
  28     <m:apply>
  29       <m:csymbol>prod</m:csymbol>
  30       <m:bvar>
  31         <m:ci>
  32           <xsl:value-of select="type_of/@var"/>
  33         </m:ci>
  34         <m:type>
  35           <xsl:apply-templates select="type_of/*"/>
  36         </m:type>
  37       </m:bvar>
  38       <xsl:apply-templates select="*[2]"/>
  39     </m:apply>
  40   </xsl:otherwise>
  41   </xsl:choose>
  42   </xsl:when>
  43   <xsl:otherwise>
  44     <m:apply>
  45       <m:csymbol>arrow</m:csymbol>
  46       <xsl:apply-templates select="*[1]"/>
  47       <xsl:apply-templates select="*[2]"/>
  48     </m:apply>
  49   </xsl:otherwise>
  50   </xsl:choose>
  51 </xsl:template>
  52
  53
  54 <xsl:template match="lambda">
  55   <m:lambda>
  56     <m:bvar>
  57       <m:ci>
  58         <xsl:value-of select="@binder"/>
  59       </m:ci>
  60     </m:bvar>
  61     <xsl:apply-templates/>
  62   </m:lambda>
  63 </xsl:template>
  64
  65
  66 <xsl:template match="apply">
  67   <m:apply>
  68     <m:csymbol>app</m:csymbol>
  69     <xsl:apply-templates select="*[1]"/>
  70     <xsl:apply-templates select="*[2]"/>
  71   </m:apply>
  72 </xsl:template>
  73
  74
  75 <xsl:template match="product">
  76   <m:apply>
  77     <xsl:choose>
  78       <xsl:when test="type_of">
  79         <xsl:choose>
  80         <xsl:when test="type_of/@var=&quot;&quot;">
  81           <m:csymbol>product_ind</m:csymbol>
  82           <m:type>
  83             <xsl:apply-templates select="type_of/*"/>
  84           </m:type>
  85         </xsl:when>
  86         <xsl:otherwise>
  87           <m:csymbol>product</m:csymbol>
  88           <m:bvar>
  89             <m:ci>
  90               <xsl:value-of select="type_of/@var"/>
  91             </m:ci>
  92           <m:type>
  93             <xsl:apply-templates select="type_of/*"/>
  94           </m:type>
  95           </m:bvar>
  96         </xsl:otherwise>
  97         </xsl:choose>
  98       </xsl:when>
  99       <xsl:otherwise>
 100         <m:csymbol>product_ind</m:csymbol>
 101         <m:type>
 102           <xsl:apply-templates select="*[1]"/>
 103         </m:type>
 104       </xsl:otherwise>
 105     </xsl:choose>
 106     <xsl:apply-templates select="*[2]"/>
 107   </m:apply>
 108 </xsl:template>
 109
 110
 111 <xsl:template match="pair">
 112   <m:apply>
 113     <m:csymbol>pair</m:csymbol>
 114     <xsl:apply-templates select="*[1]"/>
 115     <xsl:apply-templates select="*[2]"/>
 116   </m:apply>
 117 </xsl:template>
 118
 119
 120 <xsl:template match="spread">
 121   <m:apply>
 122   <m:csymbol>mutcase</m:csymbol>
 123   <m:csymbol>NONE</m:csymbol>
 124   <xsl:apply-templates select="*[1]"/>
 125   <m:piecewise>
 126     <m:piece>
 127       <xsl:apply-templates select="*[4]"/>
 128       <m:apply>
 129         <m:csymbol>pair</m:csymbol>
 130         <xsl:apply-templates select="binder[1]"/>
 131         <xsl:apply-templates select="binder[2]"/>
 132       </m:apply>
 133     </m:piece>
 134   </m:piecewise>
 135   </m:apply>
 136 </xsl:template>
 137
 138
 139 <xsl:template match="union">
 140   <m:apply>
 141     <m:csymbol>union</m:csymbol>
 142     <xsl:apply-templates select="*[1]"/>
 143     <xsl:apply-templates select="*[2]"/>
 144   </m:apply>
 145 </xsl:template>
 146
 147
 148 <xsl:template match="inl">
 149   <m:apply>
 150     <m:csymbol>inl</m:csymbol>
 151     <xsl:apply-templates select="*[1]"/>
 152   </m:apply>
 153 </xsl:template>
 154
 155
 156 <xsl:template match="inr">
 157   <m:apply>
 158     <m:csymbol>inr</m:csymbol>
 159     <xsl:apply-templates select="*[1]"/>
 160   </m:apply>
 161 </xsl:template>
 162
 163
 164 <xsl:template match="decide">
 165   <m:apply>
 166     <m:csymbol>mutcase</m:csymbol>
 167     <m:csymbol>NONE</m:csymbol>
 168     <xsl:apply-templates select="*[1]"/>
 169     <m:piecewise>
 170     <m:piece>
 171       <xsl:apply-templates select="*[3]"/>
 172       <m:apply>
 173         <m:csymbol>inl</m:csymbol>
 174         <xsl:apply-templates select="binder[1]"/>
 175       </m:apply>
 176     </m:piece>
 177     <m:piece>
 178       <xsl:apply-templates select="*[5]"/>
 179       <m:apply>
 180         <m:csymbol>inr</m:csymbol>
 181         <xsl:apply-templates select="binder[2]"/>
 182       </m:apply>
 183     </m:piece>
 184     </m:piecewise>
 185   </m:apply>
 186 </xsl:template>
 187
 188
 189 <xsl:template match="universe">
 190   <m:apply>
 191     <m:csymbol>universe</m:csymbol>
 192     <m:cn>
 193       <xsl:value-of select="@level"/>
 194     </m:cn>
 195   </m:apply>
 196 </xsl:template>
 197
 198
 199 <xsl:template match="equal">
 200   <m:apply>
 201     <m:csymbol>equal</m:csymbol>
 202     <xsl:apply-templates select="*[1]"/>
 203     <xsl:apply-templates select="*[2]"/>
 204     <xsl:apply-templates select="*[3]"/>
 205   </m:apply>
 206 </xsl:template>
 207
 208
 209 <xsl:template match="axiom">
 210   <m:apply>
 211     <m:csymbol>Ax</m:csymbol>
 212   </m:apply>
 213 </xsl:template>
 214
 215
 216 <xsl:template match="void">
 217   <m:apply>
 218     <m:csymbol>void</m:csymbol>
 219   </m:apply>
 220 </xsl:template>
 221
 222
 223 <xsl:template match="any">
 224   <m:apply>
 225     <m:csymbol>mutcase</m:csymbol>
 226     <m:csymbol>NONE</m:csymbol>
 227     <xsl:apply-templates select="*[1]"/>
 228   </m:apply>
 229 </xsl:template>
 230
 231
 232 <xsl:template match="atom">
 233   <m:apply>
 234     <m:csymbol>atom</m:csymbol>
 235   </m:apply>
 236 </xsl:template>
 237
 238
 239 <xsl:template match="token">
 240   <m:apply>
 241     <m:csymbol>token</m:csymbol>
 242     <m:ci>
 243       <xsl:value-of select="@val"/>
 244     </m:ci>
 245   </m:apply>
 246 </xsl:template>
 247
 248
 249 <xsl:template match="atom_eq">
 250   <m:apply>
 251     <m:csymbol>if_then_else</m:csymbol>
 252     <m:where>atom_eq</m:where>
 253     <xsl:apply-templates select="*[1]"/>
 254     <xsl:apply-templates select="*[2]"/>
 255     <xsl:apply-templates select="*[3]"/>
 256     <xsl:apply-templates select="*[4]"/>
 257   </m:apply>
 258 </xsl:template>
 259
 260
 261 <xsl:template match="int">
 262   <m:integers/>
 263 </xsl:template>
 264
 265
 266 <xsl:template match="natural_number">
 267   <m:cn>
 268     <xsl:value-of select="@val"/>
 269   </m:cn>
 270 </xsl:template>
 271
 272
 273 <xsl:template match="minus">
 274   <m:apply>
 275     <m:minus/>
 276     <xsl:apply-templates select="*[1]"/>
 277   </m:apply>
 278 </xsl:template>
 279
 280
 281 <xsl:template match="add">
 282   <m:apply>
 283     <m:plus/>
 284     <xsl:apply-templates select="*[1]"/>
 285     <xsl:apply-templates select="*[2]"/>
 286   </m:apply>
 287 </xsl:template>
 288
 289
 290 <xsl:template match="subtract">
 291   <m:apply>
 292     <m:minus/>
 293     <xsl:apply-templates select="*[1]"/>
 294     <xsl:apply-templates select="*[2]"/>
 295   </m:apply>
 296 </xsl:template>
 297
 298
 299 <xsl:template match="multiply">
 300   <m:apply>
 301     <m:times/>
 302     <xsl:apply-templates select="*[1]"/>
 303     <xsl:apply-templates select="*[2]"/>
 304   </m:apply>
 305 </xsl:template>
 306
 307
 308 <xsl:template match="divide">
 309   <m:apply>
 310     <m:divide/>
 311     <xsl:apply-templates select="*[1]"/>
 312     <xsl:apply-templates select="*[2]"/>
 313   </m:apply>
 314 </xsl:template>
 315
 316
 317 <xsl:template match="remainder">
 318   <m:apply>
 319     <m:rem/>
 320     <xsl:apply-templates select="*[1]"/>
 321     <xsl:apply-templates select="*[2]"/>
 322   </m:apply>
 323 </xsl:template>
 324
 325
 326 <xsl:template match="int_eq">
 327   <m:apply>
 328     <m:csymbol>if_then_else</m:csymbol>
 329     <m:where>int_eq</m:where>
 330     <xsl:apply-templates select="*[1]"/>
 331     <xsl:apply-templates select="*[2]"/>
 332     <xsl:apply-templates select="*[3]"/>
 333     <xsl:apply-templates select="*[4]"/>
 334   </m:apply>
 335 </xsl:template>
 336
 337
 338 <xsl:template match="less">
 339   <m:apply>
 340     <m:csymbol>if_then_else</m:csymbol>
 341     <m:where>less</m:where>
 342     <xsl:apply-templates select="*[1]"/>
 343     <xsl:apply-templates select="*[2]"/>
 344     <xsl:apply-templates select="*[3]"/>
 345     <xsl:apply-templates select="*[4]"/>
 346   </m:apply>
 347 </xsl:template>
 348
 349
 350 <xsl:template match="ind">
 351   <m:apply>
 352     <m:csymbol>by_induction</m:csymbol>
 353     <m:ci>ind</m:ci>
 354     <m:csymbol>NONE</m:csymbol>
 355     <m:apply>   <!-- CASO BASE -->
 356       <m:csymbol>inductive_case</m:csymbol>
 357       <m:apply>
 358         <m:csymbol>case_lhs</m:csymbol>
 359         <m:ci>0</m:ci>
 360       </m:apply>
 361       <m:apply>
 362         <m:csymbol>induction_hypothesis</m:csymbol>
 363       </m:apply>
 364       <xsl:apply-templates select="*[5]"/>
 365     </m:apply>
 366
 367     <m:apply> <!--CASO INDUTTIVO PER I NUMERI POSITIVI-->
 368       <m:csymbol>inductive_case</m:csymbol>
 369       <m:apply>
 370         <m:csymbol>case_lhs</m:csymbol>
 371         <m:ci>succ</m:ci>
 372         <m:bvar>
 373           <xsl:apply-templates select="*[6]"/> <!-- u -->
 374           <m:type>int</m:type>
 375         </m:bvar>
 376       </m:apply>
 377       <m:apply>
 378         <m:csymbol>induction_hypothesis</m:csymbol>
 379         <xsl:apply-templates select="*[7]"/> <!-- v  -->
 380       </m:apply>
 381       <xsl:apply-templates select="*[8]"/> <!-- t -->
 382     </m:apply>
 383
 384     <m:apply> <!--CASO INDUTTIVO PER I NUMERI NEGATIVI-->
 385       <m:csymbol>inductive_case</m:csymbol>
 386       <m:apply>
 387         <m:csymbol>case_lhs</m:csymbol>
 388         <m:ci>pred</m:ci>
 389         <m:bvar>
 390           <xsl:apply-templates select="*[2]"/> <!-- x -->
 391           <m:type>int</m:type>
 392         </m:bvar>
 393       </m:apply>
 394       <m:apply>
 395         <m:csymbol>induction_hypothesis</m:csymbol>
 396         <xsl:apply-templates select="*[3]"/> <!-- y -->
 397       </m:apply>
 398       <xsl:apply-templates select="*[4]"/>
 399     </m:apply>
 400     <m:apply>
 401       <m:csymbol>extra_args</m:csymbol>
 402       <xsl:apply-templates select="*[1]"/>  <!-- a -->
 403     </m:apply>
 404   </m:apply>
 405 </xsl:template>
 406
 407
 408 <xsl:template match="less_than">
 409   <m:apply>
 410     <m:lt/>
 411     <xsl:apply-templates select="*[1]"/>
 412     <xsl:apply-templates select="*[2]"/>
 413   </m:apply>
 414 </xsl:template>
 415
 416
 417 <xsl:template match="list">
 418   <m:ci>list</m:ci>
 419 </xsl:template>
 420
 421
 422 <xsl:template match="nil">
 423   <m:apply>
 424     <m:csymbol>nil</m:csymbol>
 425   </m:apply>
 426 </xsl:template>
 427
 428
 429 <xsl:template match="cons">
 430   <m:apply>
 431     <m:csymbol>cons</m:csymbol>
 432     <xsl:apply-templates select="*[1]"/>
 433     <xsl:apply-templates select="*[2]"/>
 434   </m:apply>
 435 </xsl:template>
 436
 437
 438 <xsl:template match="list_ind">
 439   <m:apply>
 440     <m:csymbol>by_induction</m:csymbol>
 441     <m:ci>list_ind</m:ci>
 442     <m:csymbol>NONE</m:csymbol>
 443     <m:apply>
 444       <m:csymbol>inductive_case</m:csymbol>
 445       <m:apply>
 446         <m:csymbol>case_lhs</m:csymbol>
 447         <m:ci>nil</m:ci>
 448       </m:apply>
 449       <m:apply>
 450         <m:csymbol>induction_hypothesis</m:csymbol>
 451       </m:apply>
 452       <xsl:apply-templates select="*[2]"/> <!-- base -->
 453     </m:apply>
 454     <m:apply>
 455       <m:csymbol>inductive_case</m:csymbol>
 456       <m:apply>
 457         <m:csymbol>case_lhs</m:csymbol>
 458         <m:ci>cons</m:ci>
 459         <m:bvar>
 460           <xsl:apply-templates select="*[3]"/> <!-- x -->
 461           <m:type>?</m:type>
 462         </m:bvar>
 463         <m:bvar>
 464         <xsl:apply-templates select="*[4]"/> <!-- l -->
 465           <m:type>?</m:type>
 466         </m:bvar>
 467       </m:apply>
 468       <m:apply>
 469         <m:csymbol>induction_hypothesis</m:csymbol>
 470         <xsl:apply-templates select="*[5]"/> <!-- Fxl -->
 471       </m:apply>
 472       <xsl:apply-templates select="*[6]"/> <!-- t -->
 473     </m:apply>
 474     <m:apply>
 475       <m:csymbol>extra_args</m:csymbol>
 476       <xsl:apply-templates select="*[1]"/> <!-- s -->
 477     </m:apply>
 478   </m:apply>
 479 </xsl:template>
 480
 481
 482 <xsl:template match="rec">
 483   <m:apply>
 484     <m:csymbol>rec</m:csymbol>
 485     <xsl:apply-templates select="*[1]"/>
 486     <xsl:apply-templates select="*[2]"/>
 487   </m:apply>
 488 </xsl:template>
 489
 490
 491 <xsl:template match="rec_ind">
 492   <m:apply>
 493     <m:csymbol>app</m:csymbol>
 494     <m:apply>
 495       <m:csymbol>fix</m:csymbol>
 496       <m:ci>
 497         <xsl:apply-templates select="*[2]"/>
 498       </m:ci>
 499       <m:bvar>
 500         <m:ci>
 501           <xsl:apply-templates select="*[2]"/>
 502         </m:ci>
 503         <m:type>?</m:type>
 504       </m:bvar>
 505       <m:lambda>
 506         <m:bvar>
 507          <xsl:apply-templates select="*[3]"/>
 508         </m:bvar>
 509         <xsl:apply-templates select="*[4]"/>
 510       </m:lambda>
 511     </m:apply>
 512     <xsl:apply-templates select="*[1]"/>
 513   </m:apply>
 514 </xsl:template>
 515
 516
 517 <xsl:template match="set">
 518   <m:apply>
 519     <m:csymbol>t_set</m:csymbol>
 520     <m:bvar>
 521       <xsl:choose>
 522       <xsl:when test="type_of">
 523         <m:ci>
 524           <xsl:value-of select="type_of/@var"/>
 525         </m:ci>
 526         <m:type>
 527           <xsl:apply-templates select="type_of/*"/>
 528         </m:type>
 529       </xsl:when>
 530       <xsl:otherwise>
 531         <m:type>
 532           <xsl:apply-templates select="*[1]"/>
 533         </m:type>
 534       </xsl:otherwise>
 535       </xsl:choose>
 536     </m:bvar>
 537     <xsl:apply-templates select="*[2]"/>
 538   </m:apply>
 539 </xsl:template>
 540
 541
 542 <xsl:template match="isect">
 543   <m:apply>
 544     <m:csymbol>isect</m:csymbol>
 545     <m:bvar>
 546       <m:ci>
 547         <xsl:value-of select="type_of/@var"/>
 548       </m:ci>
 549       <m:type>
 550         <xsl:apply-templates select="type_of/*"/>
 551       </m:type>
 552     </m:bvar>
 553     <xsl:apply-templates select="*[1]"/>
 554   </m:apply>
 555 </xsl:template>
 556
 557
 558 <xsl:template match="quotient">
 559   <m:apply>
 560     <m:csymbol>quotient</m:csymbol>
 561     <xsl:apply-templates select="*[1]"/>
 562     <m:bvar>
 563       <xsl:value-of select="binder[1]/@var"/>
 564     </m:bvar>
 565     <m:bvar>
 566       <xsl:value-of select="binder[2]/@var"/>
 567     </m:bvar>
 568     <xsl:apply-templates select="*[4]"/>
 569   </m:apply>
 570 </xsl:template>
 571
 572
 573 <xsl:template match="type_of">
 574   <m:apply>
 575     <m:csymbol>type_of</m:csymbol>
 576     <m:ci>
 577       <xsl:value-of select="@var"/>
 578     </m:ci>
 579     <xsl:apply-templates select="*[1]"/>
 580   </m:apply>
 581 </xsl:template>
 582
 583 <xsl:template match="prop">
 584   <m:apply>
 585     <m:csymbol>prop</m:csymbol>
 586     <m:cn>
 587       <xsl:value-of select="@level"/>
 588     </m:cn>
 589   </m:apply>
 590 </xsl:template>
 591
 592 <xsl:template match="binder">
 593   <m:ci>
 594     <xsl:value-of select="@var"/>
 595   </m:ci>
 596 </xsl:template>
 597
 598 </xsl:stylesheet>