From 1898ffc8283cf32f9551c6cce80b43e6355a4579 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 5 Dec 2002 14:43:30 +0000
Subject: [PATCH] Notation for if then else. Other bug fixes.

---
 helm/style/content.xsl         |  1 +
 helm/style/content_to_html.xsl | 38 +++++++++++++++++++++++++++
 helm/style/html_init.xsl       |  2 --
 helm/style/inductive.xsl       |  7 ++---
 helm/style/ite.xsl             | 48 ++++++++++++++++++++++++++++++++++
 helm/style/logic.xsl           | 25 +++++++++++++++---
 helm/style/mmlextension.xsl    | 43 ++++++++++++++++++++++++++++++
 helm/style/proofs.xsl          |  2 +-
 helm/style/xslt_index.txt      |  1 +
 9 files changed, 157 insertions(+), 10 deletions(-)
 create mode 100644 helm/style/ite.xsl

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index f2f7b713a..1be668bb0 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -37,6 +37,7 @@
                               xmlns:helm="http://www.cs.unibo.it/helm">
 
 <xsl:include href="params.xsl"/>
+<xsl:include href="ite.xsl"/>
 <!-- adesso sono preprocessate -->
 <!-- <xsl:include href="coercions.xsl"/> -->
 
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 21b663942..1a66b86dd 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -227,6 +227,12 @@
 
 <xsl:template name="make_indent">
  <xsl:param name="current_indent" select="0"/>
+ <!-- non funziona bene con netscape !!! 
+ <span>
+  <xsl:attribute name="style">
+   <xsl:value-of select="concat('margin-left:',string($current_indent div 3), 'em')"/>
+  </xsl:attribute>
+ </span> -->
   <xsl:if test="$current_indent > 0">
    <xsl:text>&#x00a0;</xsl:text>
    <xsl:call-template name="make_indent">
@@ -460,6 +466,15 @@
       </xsl:choose>
      </xsl:for-each>
     </xsl:when>
+    <!-- if then else -->
+    <xsl:when test="$name='ite'">
+     <xsl:text>if </xsl:text> 
+     <xsl:apply-templates select="*[2]"/>
+     <xsl:text> then </xsl:text>
+     <xsl:apply-templates select="*[3]"/>
+     <xsl:text> else </xsl:text>
+     <xsl:apply-templates select="*[4]"/>
+    </xsl:when>
     <!-- proof and side_proof -->
     <xsl:when test="$name='proof' or $name='side_proof'">
        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
@@ -1187,6 +1202,29 @@
         <xsl:with-param name="current_indent" select="$current_indent+5"/>
        </xsl:apply-templates>
       </xsl:when>
+      <!-- it then else -->
+      <xsl:when test="$name='ite'">
+       <xsl:text>if </xsl:text> 
+       <xsl:apply-templates select="*[2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+       </xsl:apply-templates> 
+       <BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <xsl:text> then </xsl:text>
+       <xsl:apply-templates select="*[3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 12"/>
+       </xsl:apply-templates>
+       <BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <xsl:text> else </xsl:text>
+       <xsl:apply-templates select="*[4]">
+        <xsl:with-param name="current_indent" select="$current_indent + 12"/> 
+       </xsl:apply-templates>
+      </xsl:when>
 
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 46fc61b24..91d978f5c 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -481,8 +481,6 @@
  </xsl:template>
 
 
-
-
 <!-- COUNTING -->
 
 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 4066d4be3..21f16d7a4 100644
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -245,17 +245,18 @@
  <xsl:param name="arg_types" select="/.."/>
  <xsl:param name="actual_args" select="/.."/>
  <xsl:param name="bool_var" select="true()"/>
+ <!-- <xsl:value-of select="false()"/> -->
  <xsl:choose>
   <xsl:when test="count($arg_types) = 0">
     <xsl:value-of select="$bool_var"/>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="no_expected_arg_of_arg" 
-                 select="count($arg_types[1]/PROD/decl)"/>
+                 select="count($arg_types[1]/decl)"/>
    <xsl:variable name="no_actual_abst_of_arg" 
-                 select="count($actual_args[1]/LAMBDA/decl)"/> 
+                 select="count($actual_args[1]/decl)"/> 
    <xsl:variable name="test_arg" 
-    select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/> 
+    select="($no_actual_abst_of_arg >= $no_expected_arg_of_arg)"/> 
    <xsl:call-template name="check_args">
     <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
     <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>
diff --git a/helm/style/ite.xsl b/helm/style/ite.xsl
new file mode 100644
index 000000000..1b0e14a72
--- /dev/null
+++ b/helm/style/ite.xsl
@@ -0,0 +1,48 @@
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--******************************************************************--> 
+<!-- If the else                                                      -->
+<!-- (completely) Revisited: november 2002, Andrea Asperti            -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:template match="MUTCASE[@uriType='cic:/Coq/Init/Datatypes/bool.ind']" mode="pure">
+    <m:apply helm:xref="{@id}">
+     <m:csymbol>ite</m:csymbol>
+     <xsl:apply-templates select="inductiveTerm/*[1]" mode="pure"/>
+     <xsl:apply-templates select="pattern/*[1]" mode="noannot"/>
+     <xsl:apply-templates select="pattern/*[2]" mode="noannot"/>
+    </m:apply>
+</xsl:template>
+
+</xsl:stylesheet>
+
+
diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl
index 0685f47b0..0a261260a 100644
--- a/helm/style/logic.xsl
+++ b/helm/style/logic.xsl
@@ -47,7 +47,7 @@
 <xsl:template mode="proof_transform" match="APPLY[CONST[
  attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] and 
  count(child::*) = 6 and name(*[5])='LAMBDA' and 
- count(*[5]/decl) = 2]">
+ count(*[5]/decl) >= 2]">
   <xsl:variable name="id" select="@id"/>
   <m:apply helm:xref="{@id}">
    <m:csymbol>and_ind</m:csymbol>
@@ -56,7 +56,14 @@
    <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
    <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
    <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
-   <xsl:apply-templates mode="noannot" select="*[5]/target/*"/> 
+   <xsl:choose>
+    <xsl:when test="count(*[5]/decl) = 2">
+     <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates select="*[5]/*[3]" mode="lambda_prop"/>
+    </xsl:otherwise>
+   </xsl:choose> 
   </m:apply>
 </xsl:template>
 
@@ -117,11 +124,12 @@
 -->
 </xsl:template> 
 
+
 <xsl:template mode="proof_transform" match="APPLY[CONST[
  attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con' or
  attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'] and
  count(child::*) = 6 and
- name(*[5])='LAMBDA' and count(*[5]/decl) = 2 ]">
+ name(*[5])='LAMBDA' and count(*[5]/decl) >= 2 ]">
   <xsl:variable name="id" select="@id"/>
    <m:apply helm:xref="{@id}">
     <m:csymbol>ex_ind</m:csymbol>
@@ -130,9 +138,18 @@
     <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
     <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
-    <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+    <xsl:choose>
+     <xsl:when test="count(*[5]/decl) > 2">
+      <xsl:apply-templates mode="lambda_prop" select="*[5]/decl[3]"/>
+     </xsl:when>
+     <xsl:otherwise>     
+      <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+     </xsl:otherwise>
+    </xsl:choose>
    </m:apply>
 </xsl:template>
 
+
 </xsl:stylesheet>
 
+
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 31b8c766a..8757d0023 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1121,6 +1121,49 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mo stretchy="false">}</m:mo>
        </m:mrow>
       </xsl:when>
+      <!-- ITE -->
+      <xsl:when test="$name='ite'">
+       <xsl:choose>
+        <xsl:when test="$charlength >= $framewidth">
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>if</m:mo>
+             <xsl:apply-templates select="*[2]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>then</m:mo>
+             <xsl:apply-templates select="*[3]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>else</m:mo>
+             <xsl:apply-templates select="*[4]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:mrow>
+          <m:mo>if</m:mo>
+          <xsl:apply-templates select="*[2]"/>
+          <m:mo>then</m:mo>
+          <xsl:apply-templates select="*[3]"/>
+          <m:mo>else</m:mo>
+          <xsl:apply-templates select="*[4]"/>
+         </m:mrow>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 78efb9cb1..65de766d1 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -413,7 +413,7 @@
   </xsl:for-each>
  </xsl:variable>
  <xsl:choose>
-  <xsl:when test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
+  <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
    <m:apply>
     <m:csymbol>let</m:csymbol>
     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt
index 9b3260cbf..84cd46836 100644
--- a/helm/style/xslt_index.txt
+++ b/helm/style/xslt_index.txt
@@ -13,6 +13,7 @@ html_init.xsl
 html_reals.xsl
 html_set.xsl
 inductive.xsl
+ite.xsl
 lambda.xsl
 link.xsl
 links_library.xsl
-- 
2.39.2