From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Jan 2004 15:13:45 +0000 (+0000)
Subject: Branch V7_3_new_exportation merged.
X-Git-Tag: V_0_5_1_3~19
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f2de2d1d6c8520e39c1c3793a4c2776dcf7c7c1;p=helm.git
Branch V7_3_new_exportation merged.
---
diff --git a/helm/meta_style/.cvsignore b/helm/meta_style/.cvsignore
index b88948804..b20cfb281 100644
--- a/helm/meta_style/.cvsignore
+++ b/helm/meta_style/.cvsignore
@@ -3,3 +3,4 @@ arith.xsl
basic.xsl
reals.xsl
set.xsl
+list.xsl
diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile
index c0e5fc645..f51cc8094 100644
--- a/helm/meta_style/Makefile
+++ b/helm/meta_style/Makefile
@@ -1,14 +1,14 @@
XSLTPROC = xsltproc --timing
FORMAT = xmllint --format
SUBST = ./subst.pl
-METASTYLESHEET = meta_cic2mathml.xsl
-TMP1 = /tmp/.tmpfile1
-TMP2 = /tmp/.tmpfile2
+METASTYLESHEET = ./meta_cic2mathml.xsl
+TMP1 = .tmpfile1
+TMP2 = .tmpfile2
-all: algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl
+all: algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl
clean:
- rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl
+ rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl
algebra.xsl: algebra.xml $(METASTYLESHEET)
@echo "**** PROCESSING algebra.xml ****"
@@ -54,3 +54,12 @@ set.xsl: set.xml $(METASTYLESHEET)
@rm $(TMP1)
@$(SUBST) oxsl: xsl: set.xsl
@$(SUBST) xmlns:oxsl xmlns:xsl set.xsl
+
+list.xsl: list.xml $(METASTYLESHEET)
+ @echo "**** PROCESSING list.xml ****"
+ @$(XSLTPROC) $(METASTYLESHEET) list.xml > $(TMP1)
+ @$(FORMAT) $(TMP1) > $(TMP2)
+ @mv $(TMP2) list.xsl
+ @rm $(TMP1)
+ @$(SUBST) oxsl: xsl: list.xsl
+ @$(SUBST) xmlns:oxsl xmlns:xsl list.xsl
diff --git a/helm/meta_style/algebra.xml b/helm/meta_style/algebra.xml
index 119effa3d..696a19a1b 100644
--- a/helm/meta_style/algebra.xml
+++ b/helm/meta_style/algebra.xml
@@ -1,33 +1,34 @@
<!DOCTYPE OpList SYSTEM "operator.dtd">
-<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML"
+ xmlns:helm="http://www.cs.unibo.it/helm">
<!-- Unary Operations -->
<Operator
name = "0"
- uri = "cic:/Algebra/CSemiGroups/csg_unit.con"
+ uri = "cic:/Algebra/algebra/CSemiGroups/csg_unit.con"
arity = "1">
<mop tag="ci" helm:xref="$APP-ID">0</mop>
</Operator>
<Operator
name = "1"
- uri = "cic:/Algebra/CRings/cr_one.con"
+ uri = "cic:/Algebra/algebra/CRings/cr_one.con"
arity = "1">
<mop tag="ci" helm:xref="$APP-ID">1</mop>
</Operator>
<Operator
name = "*****"
- uri = "cic:/Algebra/CGroups/cg_inv.con"
+ uri = "cic:/Algebra/algebra/CGroups/cg_inv.con"
hide = "1"
arity = "1"
m-tag = "minus"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con"
+ uri = "cic:/Algebra/reals/CMetricFields/cmf_abs.con"
hide = "1"
arity = "2"
m-tag = "abs"/>
@@ -36,63 +37,63 @@
<Operator
name = "SETOID EQUALITY"
- uri = "cic:/Algebra/CSetoids/cs_eq.con"
+ uri = "cic:/Algebra/algebra/CSetoids/cs_eq.con"
hide = "1"
arity = "2"
m-tag = "eq"/>
<Operator
name = "APART"
- uri = "cic:/Algebra/CSetoids/cs_ap.con"
+ uri = "cic:/Algebra/algebra/CSetoids/cs_ap.con"
hide = "1"
arity = "2"
m-tag = "neq"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/COrdFields/leEq.con"
+ uri = "cic:/Algebra/algebra/COrdFields/leEq.con"
hide = "1"
arity = "2"
m-tag = "leq"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/COrdFields/cof_less.con"
+ uri = "cic:/Algebra/algebra/COrdFields/cof_less.con"
hide = "1"
arity = "2"
m-tag = "lt"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CRings/cr_plus.con | cic:/Algebra/CSemiGroups/csg_op.con"
+ uri = "cic:/Algebra/algebra/CRings/cr_plus.con | cic:/Algebra/algebra/CSemiGroups/csg_op.con"
hide = "1"
arity = "2"
m-tag = "plus"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CRings/cr_minus.con | cic:/Algebra/CGroups/cg_minus.con"
+ uri = "cic:/Algebra/algebra/CRings/cr_minus.con | cic:/Algebra/algebra/CGroups/cg_minus.con"
hide = "1"
arity = "2"
m-tag = "minus"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CRings/cr_mult.con"
+ uri = "cic:/Algebra/algebra/CRings/cr_mult.con"
hide = "1"
arity = "2"
m-tag = "times"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CFields/cf_div.con"
+ uri = "cic:/Algebra/algebra/CFields/cf_div.con"
hide = "1"
arity = "2"
m-tag = "divide"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CRings/Ring_constructions/nzpro.con"
+ uri = "cic:/Algebra/algebra/CRings/nzpro.con"
cook = "true"
arity = "2">
<param id="1"/>
@@ -100,14 +101,14 @@
<Operator
name = "*****"
- uri = "cic:/Algebra/CRings/exponentiation/nexp.con"
+ uri = "cic:/Algebra/algebra/CRings/nexp.con"
cook = "true"
arity = "2"
m-tag = "power"/>
<Operator
name = "*****"
- uri = "cic:/Algebra/CRings/exponentiation/nexp_op.con | cic:/Algebra/Expon/Zexp_def/zexp.con"
+ uri = "cic:/Algebra/algebra/CRings/nexp_op.con | cic:/Algebra/algebra/Expon/zexp.con"
cook = "true"
arity = "2">
<mapp>
@@ -120,7 +121,7 @@
<Operator
name = "*****"
- uri = "cic:/Algebra/COrdFields/absSmall.con"
+ uri = "cic:/Algebra/algebra/COrdFields/absSmall.con"
hide = "1"
arity = "2">
<mapp>
@@ -135,7 +136,7 @@
<Operator
name = "*****"
- uri = "cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con"
+ uri = "cic:/Algebra/algebra/CPolynomials/cpoly_apply_fun.con"
cook = "true"
arity = "2">
<mapp>
@@ -147,7 +148,7 @@
<Operator
name = "********"
- uri = "cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con"
+ uri = "cic:/Algebra/algebra/COrdFields/seqLimit.con"
cook = "true"
arity = "2">
<mapp>
@@ -166,7 +167,7 @@
<Operator
name = "********"
- uri = "cic:/Algebra/CSums/Sums/sum0.con"
+ uri = "cic:/Algebra/algebra/CSums/sum0.con"
cook = "true"
arity = "2">
<m:apply helm:xref="$OP-ID">
@@ -185,7 +186,7 @@
<Operator
name = "SUM"
- uri = "cic:/Algebra/CSums/Sums/sum.con"
+ uri = "cic:/Algebra/algebra/CSums/sum_.con"
cook = "true"
arity = "3">
<m:apply helm:xref="$OP-ID">
diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml
index 17fc523cd..a21a51306 100644
--- a/helm/meta_style/arith.xml
+++ b/helm/meta_style/arith.xml
@@ -4,8 +4,6 @@
<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
-<import href="positive.xsl"/>
-
<Operator
name = "LESS EQUAL"
uri = "cic:/Coq/Init/Peano/le.ind | cic:/Coq/ZArith/zarith_aux/Zle.con"
@@ -32,7 +30,7 @@
<Operator
name = "*****"
- uri = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zplus.con"
+ uri = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/Zplus.con"
arity = "2"
m-tag = "plus"/>
@@ -44,7 +42,7 @@
<Operator
name = "*****"
- uri = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zmult.con"
+ uri = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/Zmult.con"
arity = "2"
m-tag = "times"/>
@@ -56,7 +54,7 @@
<Operator
name = "*****"
- uri = "cic:/Coq/ZArith/fast_integer/fast_integers/Zopp.con"
+ uri = "cic:/Coq/ZArith/fast_integer/Zopp.con"
arity = "1"
m-tag = "minus"/>
diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml
index b0681468c..e9da62a62 100644
--- a/helm/meta_style/basic.xml
+++ b/helm/meta_style/basic.xml
@@ -7,16 +7,27 @@
<Operator
name = "AND"
- uri = "cic:/Coq/Init/Logic/Conjunction/and.ind"
+ uri = "cic:/Coq/Init/Logic/and.ind"
arity = "2"
m-tag = "and"/>
<Operator
name = "OR"
- uri = "cic:/Coq/Init/Logic/Disjunction/or.ind"
+ uri = "cic:/Coq/Init/Logic/or.ind"
arity = "2"
m-tag = "or"/>
+<Operator
+ name = "IFF"
+ uri = "cic:/Coq/Init/Logic/iff.con"
+ arity = "2">
+ <mapp>
+ <m:csymbol>iff</m:csymbol>
+ <param id="1"/>
+ <param id="2"/>
+ </mapp>
+</Operator>
+
<Operator
name = "NOT"
uri = "cic:/Coq/Init/Logic/not.con"
@@ -28,14 +39,14 @@
<Operator
name = "EQUALITY and TYPE EQUALITY"
- uri = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
hide = "1"
arity = "2"
m-tag = "eq"/>
<NotOperator
name = "NOT-EQ and NOT-EQT"
- uri = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
hide = "1"
arity = "2">
<mapp>
@@ -47,7 +58,7 @@
<Operator
name = "EXIST"
- uri = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
+ uri = "cic:/Coq/Init/Logic/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
arity = "2">
<mapp>
<mop tag="exists"/>
@@ -61,7 +72,7 @@
<Operator
name = "EXIST"
- uri = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
+ uri = "cic:/Coq/Init/Logic/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
hide = "1"
arity = "2">
<mapp>
diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml
new file mode 100644
index 000000000..9ed07d69b
--- /dev/null
+++ b/helm/meta_style/list.xml
@@ -0,0 +1,60 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+<!-- ************************** LISTS ****************************** -->
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!-- CSC: manca
+<Operator
+ name = "CONS"
+ uri = "cic:/Coq/Lists/PolyList/list.ind"
+ arity = "2"
+ m-tag = "???"/>
+
+<Operator
+ name = "NIL"
+ uri = "cic:/Coq/Lists/PolyList/list.ind"
+ arity = "0"
+ m-tag = "???"/> -->
+
+<Operator
+ name = "APPEND"
+ uri = "cic:/Coq/Lists/PolyList/app.con"
+ cook = "true"
+ arity = "2">
+ <mapp>
+ <m:csymbol>append</m:csymbol>
+ <param id="1"/>
+ <param id="2"/>
+ </mapp>
+</Operator>
+
+<Operator
+ name = "IN"
+ uri = "cic:/Coq/Lists/PolyList/In.con | cic:/Coq/Lists/TheoryList/In_spec.ind | cic:/Coq/Lists/ListSet/set_In.con | cic:/Coq/Lists/ListSet/set_mem.con"
+ cook = "true"
+ arity = "2"
+ m-tag = "in"/>
+
+<Operator
+ name = "INCL"
+ uri = "cic:/Coq/Lists/PolyList/incl.con"
+ cook = "true"
+ arity = "2"
+ m-tag = "subset"/>
+
+<Operator
+ name = "INTER"
+ uri = "cic:/Coq/Lists/ListSet/set_inter.con"
+ cook = "true"
+ arity = "2"
+ m-tag = "intersect"/>
+
+<Operator
+ name = "LENGTH"
+ uri = "cic:/Coq/Lists/PolyList/length.con"
+ cook = "true"
+ arity = "1"
+ m-tag = "card"/>
+
+</OpList>
diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl
index f77890363..072774b5d 100644
--- a/helm/meta_style/meta_cic2mathml.xsl
+++ b/helm/meta_style/meta_cic2mathml.xsl
@@ -47,6 +47,7 @@
<oxsl:include href="{@href}"/>
</xsl:template>
+
<xsl:template match="Operator|NotOperator">
<xsl:variable name="uri">
<xsl:call-template name="remove_white_spaces">
@@ -79,7 +80,7 @@
<xsl:with-param name="c-tag" select="'CONST'"/>
</xsl:call-template>
</xsl:variable>
-
+
<!-- All uris in uri2 list (if not empty) have MUTIND c-tag -->
<xsl:variable name="uri2">
<xsl:call-template name="select_uris">
@@ -93,13 +94,24 @@
<xsl:with-param name="name" select="@name"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="uri" select="$uri1"/>
- <xsl:with-param name="cook" select="@cook"/>
<xsl:with-param name="hide" select="@hide"/>
<xsl:with-param name="arity" select="@arity"/>
<xsl:with-param name="m-tag" select="@m-tag"/>
<xsl:with-param name="c-tag" select="'CONST'"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
+ <xsl:if test="@cook = 'true'">
+ <xsl:call-template name="out_template">
+ <xsl:with-param name="name" select="@name"/>
+ <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="uri" select="$uri1"/>
+ <xsl:with-param name="cook" select="@cook"/>
+ <xsl:with-param name="hide" select="@hide"/>
+ <xsl:with-param name="arity" select="@arity"/>
+ <xsl:with-param name="m-tag" select="@m-tag"/>
+ <xsl:with-param name="c-tag" select="'CONST'"/>
+ </xsl:call-template>
+ </xsl:if>
</xsl:if>
<xsl:if test="$uri2 != ''">
@@ -107,13 +119,24 @@
<xsl:with-param name="name" select="@name"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="uri" select="$uri2"/>
- <xsl:with-param name="cook" select="@cook"/>
<xsl:with-param name="hide" select="@hide"/>
<xsl:with-param name="arity" select="@arity"/>
<xsl:with-param name="m-tag" select="@m-tag"/>
<xsl:with-param name="c-tag" select="'MUTIND'"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
+ <xsl:if test="@cook = 'true'">
+ <xsl:call-template name="out_template">
+ <xsl:with-param name="name" select="@name"/>
+ <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="uri" select="$uri2"/>
+ <xsl:with-param name="cook" select="@cook"/>
+ <xsl:with-param name="hide" select="@hide"/>
+ <xsl:with-param name="arity" select="@arity"/>
+ <xsl:with-param name="m-tag" select="@m-tag"/>
+ <xsl:with-param name="c-tag" select="'MUTIND'"/>
+ </xsl:call-template>
+ </xsl:if>
</xsl:if>
</xsl:otherwise>
</xsl:choose>
@@ -138,14 +161,14 @@
</xsl:variable>
<xsl:choose>
- <xsl:when test="$const = 'false' and $not = 'true'">
+ <xsl:when test="$const = 'true' and $not = 'true'">
<xsl:call-template name="out_comment">
<xsl:with-param name="name" select="concat($uri,': "not" cannot be applyed to a constant operator')"/>
</xsl:call-template>
</xsl:when>
<xsl:when test="$const = 'true'">
<xsl:call-template name="out_comment">
- <xsl:with-param name="name" select="concat($uri,': cannot be specified a constant operator when using OpSet element')"/>
+ <xsl:with-param name="name" select="concat($uri,': cannot be specified a constant operator when using OpSet element')"/>
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
@@ -168,11 +191,21 @@
<xsl:with-param name="name" select="@name"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="uri" select="$uri1"/>
- <xsl:with-param name="cook" select="@cook"/>
<xsl:with-param name="hide" select="@hide"/>
<xsl:with-param name="m-tag" select="@m-tag"/>
<xsl:with-param name="c-tag" select="'CONST'"/>
</xsl:call-template>
+ <xsl:if test="@cook = 'true'">
+ <xsl:call-template name="out_template_set">
+ <xsl:with-param name="name" select="@name"/>
+ <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="uri" select="$uri1"/>
+ <xsl:with-param name="cook" select="@cook"/>
+ <xsl:with-param name="hide" select="@hide"/>
+ <xsl:with-param name="m-tag" select="@m-tag"/>
+ <xsl:with-param name="c-tag" select="'CONST'"/>
+ </xsl:call-template>
+ </xsl:if>
</xsl:if>
<xsl:if test="$uri2 != ''">
@@ -180,11 +213,21 @@
<xsl:with-param name="name" select="@name"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="uri" select="$uri2"/>
- <xsl:with-param name="cook" select="@cook"/>
<xsl:with-param name="hide" select="@hide"/>
<xsl:with-param name="m-tag" select="@m-tag"/>
<xsl:with-param name="c-tag" select="'MUTIND'"/>
</xsl:call-template>
+ <xsl:if test="@cook = 'true'">
+ <xsl:call-template name="out_template_set">
+ <xsl:with-param name="name" select="@name"/>
+ <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="uri" select="$uri2"/>
+ <xsl:with-param name="cook" select="@cook"/>
+ <xsl:with-param name="hide" select="@hide"/>
+ <xsl:with-param name="m-tag" select="@m-tag"/>
+ <xsl:with-param name="c-tag" select="'MUTIND'"/>
+ </xsl:call-template>
+ </xsl:if>
</xsl:if>
</xsl:otherwise>
</xsl:choose>
@@ -205,30 +248,26 @@
<xsl:param name="m-tag"/>
<xsl:param name="c-tag"/>
<xsl:param name="const" select="'false'"/>
-
- <xsl:variable name="apply_not">
- <xsl:if test="$not = 'true'">*[2]/</xsl:if>
- </xsl:variable>
-
+
<xsl:variable name="match">
<xsl:variable name="match_op">
<xsl:call-template name="out_match_op">
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="uri" select="$uri"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
</xsl:call-template>
</xsl:variable>
-
+
<xsl:variable name="match_child">
- <xsl:if test="$cook = 'false' or $not = 'true'">
+ <xsl:if test="$const = 'false'">
<xsl:choose>
<!-- if the operator has been concatenated with not, the root apply node must have only two child -->
- <xsl:when test="$not = 'true' and $cook = 'true'"> and count(*) = 2</xsl:when>
- <xsl:when test="$not = 'true' and $cook = 'false'">
+ <xsl:when test="$not = 'true'">
<xsl:value-of select="concat(' and count(*) = 2 and count(*[2]/*) = ',$arity + $hide + 1)"/>
</xsl:when>
<xsl:otherwise>
- <xsl:value-of select="concat('count(*) = ',$arity + $hide + 1)"/>
+ <xsl:value-of select="concat(' and count(*) = ',$arity + $hide + 1)"/>
</xsl:otherwise>
</xsl:choose>
</xsl:if>
@@ -244,60 +283,21 @@
</xsl:choose>
</xsl:variable>
- <xsl:variable name="op_uri_attr">
- <xsl:variable name="tmp_op_uri_attr">
- <xsl:call-template name="op_uri_attr">
- <xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="c-tag" select="$c-tag"/>
- <xsl:with-param name="const" select="$const"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
- </xsl:variable>
-
<!-- TEMPLATE -->
<xsl:call-template name="out_comment">
<xsl:with-param name="name" select="$name"/>
</xsl:call-template>
<oxsl:template match="{$match}" mode="pure">
- <xsl:choose>
- <xsl:when test="$cook = 'true'">
- <oxsl:variable name="no_params">
- <oxsl:call-template name="get_no_params">
- <oxsl:with-param name="first_uri" select="$CICURI"/>
- <oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
- </oxsl:call-template>
- </oxsl:variable>
- <oxsl:choose>
- <oxsl:when test="{concat('count(',$apply_not,'*) = $no_params + ',$arity + $hide + 1)}">
- <xsl:call-template name="out_body">
- <xsl:with-param name="c-tag" select="$c-tag"/>
- <xsl:with-param name="m-tag" select="$m-tag"/>
- <xsl:with-param name="cook" select="$cook"/>
- <xsl:with-param name="hide" select="$hide"/>
- <xsl:with-param name="arity" select="$arity"/>
- <xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="const" select="$const"/>
- </xsl:call-template>
- </oxsl:when>
- <oxsl:otherwise>
- <oxsl:apply-imports/>
- </oxsl:otherwise>
- </oxsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="out_body">
- <xsl:with-param name="c-tag" select="$c-tag"/>
- <xsl:with-param name="m-tag" select="$m-tag"/>
- <xsl:with-param name="cook" select="$cook"/>
- <xsl:with-param name="hide" select="$hide"/>
- <xsl:with-param name="arity" select="$arity"/>
- <xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="const" select="$const"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
+ <xsl:call-template name="out_body">
+ <xsl:with-param name="c-tag" select="$c-tag"/>
+ <xsl:with-param name="m-tag" select="$m-tag"/>
+ <xsl:with-param name="cook" select="$cook"/>
+ <xsl:with-param name="hide" select="$hide"/>
+ <xsl:with-param name="arity" select="$arity"/>
+ <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="const" select="$const"/>
+ </xsl:call-template>
</oxsl:template>
</xsl:template>
@@ -310,40 +310,27 @@
<xsl:param name="m-tag"/>
<xsl:param name="c-tag"/>
- <xsl:variable name="no_params_var">
- <xsl:if test="$cook = 'true'">$no_params + </xsl:if>
- </xsl:variable>
-
<xsl:variable name="match">
<xsl:variable name="match_op">
<xsl:call-template name="out_match_op">
- <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="uri" select="$uri"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
</xsl:call-template>
</xsl:variable>
- <xsl:variable name="match_child">
- <xsl:if test="$not = 'true'"> and count(*) = 2</xsl:if>
- </xsl:variable>
+ <xsl:variable name="match_child">
+ <xsl:if test="$not = 'true'"> and count(*) = 2</xsl:if>
+ </xsl:variable>
- <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
+ <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
</xsl:variable>
<xsl:variable name="apply_not">
<xsl:if test="$not = 'true'">*[2]/</xsl:if>
</xsl:variable>
- <xsl:variable name="op_uri_attr">
- <xsl:variable name="tmp_op_uri_attr">
- <xsl:call-template name="op_uri_attr">
- <xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="c-tag" select="$c-tag"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
- </xsl:variable>
-
<!-- TEMPLATE -->
<xsl:call-template name="out_comment">
@@ -351,17 +338,9 @@
</xsl:call-template>
<oxsl:template match="{$match}" mode="pure">
- <xsl:if test="$cook = 'true'">
- <oxsl:variable name="no_params">
- <oxsl:call-template name="get_no_params">
- <oxsl:with-param name="first_uri" select="$CICURI"/>
- <oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
- </oxsl:call-template>
- </oxsl:variable>
- </xsl:if>
<oxsl:choose>
<xsl:for-each select="Case">
- <oxsl:when test="{concat('count(',$apply_not,'*) = ',$no_params_var,@arity + $hide + 1)}">
+ <oxsl:when test="{concat('count(',$apply_not,'*) = ',@arity + $hide + 1)}">
<xsl:call-template name="out_body">
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="m-tag" select="$m-tag"/>
@@ -392,7 +371,12 @@
<xsl:template name="out_match_op">
<xsl:param name="not" select="'false'"/>
<xsl:param name="uri"/>
+ <xsl:param name="cook" select="'false'"/>
<xsl:param name="c-tag"/>
+
+ <xsl:variable name="instantiate">
+ <xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+ </xsl:variable>
<!-- application with not operator -->
<xsl:variable name="app_not">
@@ -407,7 +391,7 @@
<xsl:variable name="app_op">
<xsl:if test="$not = 'true'">APPLY[</xsl:if>
- <xsl:value-of select="concat($c-tag,'[',$uris,']')"/>
+ <xsl:value-of select="concat($instantiate,$c-tag,'[',$uris,']')"/>
<xsl:if test="$not = 'true'">]</xsl:if>
</xsl:variable>
@@ -416,7 +400,6 @@
<xsl:template name="out_params">
<xsl:param name="params" select="1"/>
- <xsl:param name="cook" select="'false'"/>
<xsl:param name="hide" select="0"/>
<xsl:param name="not" select="'false'"/>
<xsl:param name="mode" select="'noannot'"/>
@@ -427,7 +410,6 @@
<xsl:call-template name="param">
<xsl:with-param name="id" select="$params"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
@@ -436,7 +418,6 @@
<xsl:call-template name="out_params">
<xsl:with-param name="params" select="$params + 1"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="mode" select="$mode"/>
@@ -445,7 +426,6 @@
</xsl:if>
</xsl:template>
-
<xsl:template name="out_body">
<xsl:param name="c-tag"/>
<xsl:param name="cook" select="'false'"/>
@@ -459,12 +439,13 @@
<!-- SIMPLE TRANSFORMATIONS -->
<xsl:when test="count(*) = 0">
<xsl:variable name="xref">
- <xsl:if test="$const = 'false'">{@id}</xsl:if>
+ <xsl:if test="$const = 'false'">{@id}</xsl:if>
</xsl:variable>
<xsl:variable name="definitionURL">
<xsl:call-template name="op_uri_attr">
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
@@ -473,6 +454,7 @@
<xsl:variable name="helm:xref">
<xsl:call-template name="op_id_attr">
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
@@ -491,8 +473,7 @@
</xsl:element>
<!-- PARAMS -->
<xsl:call-template name="out_params">
- <xsl:with-param name="cook" select="$cook"/>
- <xsl:with-param name="hide" select="$hide"/>
+ <xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="arity" select="$arity"/>
</xsl:call-template>
@@ -512,6 +493,7 @@
</xsl:choose>
</xsl:template>
+
<xsl:template name="out_mvar">
<xsl:param name="vname"/>
@@ -531,7 +513,6 @@
<xsl:template name="out_choose_binder">
<xsl:param name="binded_params" select="''"/>
<xsl:param name="not" select="'false'"/>
- <xsl:param name="cook" select="'false'"/>
<xsl:param name="hide" select="0"/>
<xsl:param name="binder"/>
@@ -541,7 +522,6 @@
<xsl:call-template name="out_choose_binder">
<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="binder" select="$binder"/>
</xsl:call-template>
@@ -549,7 +529,6 @@
<xsl:call-template name="out_choose_binder">
<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="binder" select="$binder"/>
</xsl:call-template>
@@ -559,7 +538,6 @@
<xsl:call-template name="param">
<xsl:with-param name="id" select="$binded_params"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
@@ -572,6 +550,7 @@
</xsl:if>
</xsl:template>
+
<!-- *********************************************************************** -->
<!-- META LANGUAGE FOR MathML -->
<!-- *********************************************************************** -->
@@ -590,6 +569,7 @@
<xsl:call-template name="set_attribute">
<xsl:with-param name="attr" select="@xref"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
<xsl:with-param name="not" select="$not"/>
@@ -604,6 +584,7 @@
<m:apply helm:xref="{$helm:xref}">
<xsl:call-template name="copy_attributes">
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
@@ -623,7 +604,6 @@
</m:apply>
</xsl:template>
-
<xsl:template match="mop">
<xsl:param name="c-tag"/>
<xsl:param name="cook" select="'false'"/>
@@ -638,6 +618,7 @@
<xsl:when test="@definitionURL">
<xsl:call-template name="set_attribute">
<xsl:with-param name="attr" select="@definitionURL"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
@@ -648,6 +629,7 @@
<xsl:otherwise>
<xsl:call-template name="op_uri_attr">
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
@@ -661,6 +643,7 @@
<xsl:when test="@xref">
<xsl:call-template name="set_attribute">
<xsl:with-param name="attr" select="@xref"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
@@ -671,6 +654,7 @@
<xsl:otherwise>
<xsl:call-template name="op_id_attr">
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
@@ -687,6 +671,7 @@
</xsl:attribute>
<xsl:call-template name="copy_attributes">
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
@@ -706,8 +691,8 @@
</xsl:element>
</xsl:template>
+
<xsl:template match="param">
- <xsl:param name="cook" select="'false'"/>
<xsl:param name="hide" select="0"/>
<xsl:param name="not" select="'false'"/>
@@ -715,7 +700,6 @@
<xsl:call-template name="param">
<xsl:with-param name="id" select="@id"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
@@ -743,6 +727,7 @@
</xsl:choose>
</xsl:template>
+
<xsl:template match="m:*">
<xsl:param name="c-tag"/>
<xsl:param name="cook" select="'false'"/>
@@ -753,6 +738,7 @@
<xsl:copy>
<xsl:call-template name="copy_attributes">
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
@@ -771,6 +757,7 @@
</xsl:copy>
</xsl:template>
+
<xsl:template match="mbvar">
<xsl:param name="c-tag"/>
<xsl:param name="cook" select="'false'"/>
@@ -790,12 +777,11 @@
<xsl:call-template name="test_on_lambda">
<xsl:with-param name="binded_params" select="$binded_params"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
- <xsl:variable name="binder">/target/@binder</xsl:variable>
+ <xsl:variable name="binder">/decl/@binder</xsl:variable>
<xsl:choose>
<xsl:when test="$binded_params != ''">
@@ -812,11 +798,10 @@
<xsl:with-param name="binded_params" select="$binded_params"/>
<xsl:with-param name="not" select="$not"/>
<xsl:with-param name="hide" select="$hide"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="binder" select="$binder"/>
</xsl:call-template>
</oxsl:choose>
- </oxsl:variable>
+ </oxsl:variable>
<oxsl:call-template name="insert_subscript">
<oxsl:with-param name="node_value" select="$binder"/>
</oxsl:call-template>
@@ -827,11 +812,10 @@
<xsl:call-template name="param">
<xsl:with-param name="id" select="$binded_params"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
- </xsl:variable>
-
+ </xsl:variable>
+
<oxsl:call-template name="insert_subscript">
<oxsl:with-param name="node_value" select="{concat($param,$binder)}"/>
</oxsl:call-template>
@@ -877,6 +861,8 @@
</xsl:choose>
</xsl:template>
+
+
<xsl:template match="mvar">
<xsl:call-template name="out_mvar">
<xsl:with-param name="vname" select="@name"/>
@@ -884,7 +870,6 @@
</xsl:template>
-
<!-- *********************************************************************** -->
<!-- AUXILIARY FUNCTIONS -->
<!-- *********************************************************************** -->
@@ -1004,7 +989,6 @@
<xsl:template name="test_on_lambda">
<xsl:param name="binded_params" select="''"/>
<xsl:param name="not" select="'false'"/>
- <xsl:param name="cook" select="'false'"/>
<xsl:param name="hide" select="0"/>
<xsl:if test="$binded_params != ''">
@@ -1014,7 +998,6 @@
<xsl:call-template name="test_on_lambda">
<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
@@ -1023,7 +1006,6 @@
<xsl:call-template name="test_on_lambda">
<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
@@ -1035,7 +1017,6 @@
<xsl:call-template name="param">
<xsl:with-param name="id" select="$binded_params"/>
<xsl:with-param name="not" select="$not"/>
- <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="hide" select="$hide"/>
</xsl:call-template>
</xsl:variable>
@@ -1140,29 +1121,26 @@
<xsl:template name="param">
<xsl:param name="id"/>
<xsl:param name="not" select="'false'"/>
- <xsl:param name="cook" select="'false'"/>
<xsl:param name="hide" select="0"/>
<xsl:variable name="apply_not">
<xsl:if test="$not = 'true'">*[2]/</xsl:if>
</xsl:variable>
- <xsl:variable name="no_params_var">
- <xsl:if test="$cook = 'true'">$no_params+</xsl:if>
- </xsl:variable>
-
- <xsl:value-of select="concat($apply_not,'*[',$no_params_var,$id + $hide + 1,']')"/>
+ <xsl:value-of select="concat($apply_not,'*[',$id + $hide + 1,']')"/>
</xsl:template>
<!-- Returns a xpath string with the location of the operator uri attribute -->
<xsl:template name="op_uri_attr">
<xsl:param name="not" select="'false'"/>
+ <xsl:param name="cook" select="'false'"/>
<xsl:param name="c-tag"/>
<xsl:param name="const" select="'false'"/>
<xsl:call-template name="op_attr">
<xsl:with-param name="attr_type" select="'@uri'"/>
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
@@ -1171,12 +1149,14 @@
<!-- Returns a xpath string with the location of the operator id attribute -->
<xsl:template name="op_id_attr">
<xsl:param name="not" select="'false'"/>
+ <xsl:param name="cook" select="'false'"/>
<xsl:param name="c-tag"/>
<xsl:param name="const" select="'false'"/>
<xsl:call-template name="op_attr">
<xsl:with-param name="attr_type" select="'@id'"/>
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
@@ -1187,8 +1167,13 @@
<xsl:template name="op_attr">
<xsl:param name="attr_type"/>
<xsl:param name="not" select="'false'"/>
+ <xsl:param name="cook" select="'false'"/>
<xsl:param name="c-tag"/>
<xsl:param name="const" select="'false'"/>
+
+ <xsl:variable name="instantiate">
+ <xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+ </xsl:variable>
<xsl:variable name="apply">
<xsl:if test="$not = 'true'">APPLY/</xsl:if>
@@ -1199,12 +1184,13 @@
<xsl:value-of select="concat('{',$attr_type,'}')"/>
</xsl:when>
<xsl:otherwise>
- <xsl:value-of select="concat('{',$apply,$c-tag,'/',$attr_type,'}')"/>
+ <xsl:value-of select="concat('{',$apply,$instantiate,$c-tag,'/',$attr_type,'}')"/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:template name="copy_attributes">
+ <xsl:param name="cook" select="'false'"/>
<xsl:param name="c-tag"/>
<xsl:param name="hide" select="0"/>
<xsl:param name="arity" select="0"/>
@@ -1232,6 +1218,7 @@
<xsl:attribute name="{$name}">
<xsl:call-template name="set_attribute">
<xsl:with-param name="attr" select="."/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="hide" select="$hide"/>
<xsl:with-param name="arity" select="$arity"/>
@@ -1265,6 +1252,7 @@
<xsl:template name="set_attribute">
<xsl:param name="attr"/>
<xsl:param name="c-tag"/>
+ <xsl:param name="cook" select="'false'"/>
<xsl:param name="hide" select="0"/>
<xsl:param name="arity" select="0"/>
<xsl:param name="not" select="'false'"/>
@@ -1281,10 +1269,11 @@
<xsl:otherwise>@uri</xsl:otherwise>
</xsl:choose>
</xsl:variable>
-
+
<xsl:call-template name="op_attr">
<xsl:with-param name="attr_type" select="$attr_type"/>
<xsl:with-param name="not" select="$not"/>
+ <xsl:with-param name="cook" select="$cook"/>
<xsl:with-param name="c-tag" select="$c-tag"/>
<xsl:with-param name="const" select="$const"/>
</xsl:call-template>
diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl
index f52b64702..e337b663e 100644
--- a/helm/meta_style/positive.xsl
+++ b/helm/meta_style/positive.xsl
@@ -73,7 +73,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
<xsl:apply-templates select="*[2]" mode="Zpositive">
<xsl:with-param name="base" select="0"/>
<xsl:with-param name="exp" select="1"/>
@@ -81,7 +81,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
</xsl:apply-templates>
</xsl:template>
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
<m:apply helm:xref="{@id}">
<m:minus definitionURL="{*[1]/@uri}" helm:xref="{*[1]/@id}"/>
<xsl:apply-templates select="*[2]" mode="Zpositive">
@@ -92,13 +92,13 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
</m:apply>
</xsl:template>
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='1']" mode="pure">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='1']" mode="pure">
<m:ci definitionURL="{@uri}" helm:xref="{@id}">0</m:ci>
</xsl:template>
<!-- prova di notazione per positive -->
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind']]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/positive.ind']]" mode="pure">
<xsl:apply-templates select="." mode="Zpositive">
<xsl:with-param name="base" select="0"/>
<xsl:with-param name="exp" select="1"/>
@@ -106,7 +106,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
</xsl:apply-templates>
</xsl:template>
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3']" mode="pure">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='3']" mode="pure">
<m:ci definitionURL="{@uri}" helm:xref="{@id}">1</m:ci>
</xsl:template>
@@ -116,7 +116,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
<xsl:param name="iden" select="''"/>
<xsl:choose>
<xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
-and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='1']">
+and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='1']">
<xsl:apply-templates select="*[2]" mode="Zpositive">
<xsl:with-param name="base" select="$base + $exp"/>
<xsl:with-param name="exp" select="2 * $exp"/>
@@ -124,14 +124,14 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr
</xsl:apply-templates>
</xsl:when>
<xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
-and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='2']">
+and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='2']">
<xsl:apply-templates select="*[2]" mode="Zpositive">
<xsl:with-param name="base" select="$base"/>
<xsl:with-param name="exp" select="2 * $exp"/>
<xsl:with-param name="iden" select="$iden"/>
</xsl:apply-templates>
</xsl:when>
- <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3'">
+ <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='3'">
<m:ci helm:xref="{$iden}"><xsl:value-of select="$base + $exp"/></m:ci>
</xsl:when>
<xsl:otherwise>
@@ -173,5 +173,46 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr
</xsl:choose>
</xsl:template>
+<!-- **************************** Reals ******************************** -->
+
+<xsl:template match="APPLY[CONST[position() = 1 and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and count(*) = 3]" mode="pure">
+ <xsl:variable name="result">
+ <xsl:apply-templates select="." mode="reals"/>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="string($result) = ''">
+ <m:apply helm:xref="{@id}">
+ <m:plus xmlns:m="http://www.w3.org/1998/Math/MathML" definitionURL="{CONST[1]/@uri}" helm:xref="{CONST[1]/@id}"/>
+ <xsl:apply-templates select="*[2]" mode="noannot"/>
+ <xsl:apply-templates select="*[3]" mode="noannot"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:cn helm:xref="{CONST[1]/@id}"><xsl:value-of select="$result"/></m:cn>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="APPLY[*[position() = 1 and name()='CONST' and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and *[position() = 2 and name()='CONST' and @uri='cic:/Coq/Reals/Rdefinitions/R1.con'] and count(*) = 3]" mode="reals">
+ <xsl:param name="real_counter" select="0"/>
+ <xsl:variable name="result">
+ <xsl:apply-templates select="*[3]" mode="reals">
+ <xsl:with-param name="real_counter" select="$real_counter + 1"/>
+ </xsl:apply-templates>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="string($result) = ''"/>
+ <xsl:otherwise>
+ <xsl:value-of select="$result"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="CONST[@uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="reals">
+ <xsl:param name="real_counter" select="0"/>
+ <xsl:value-of select="$real_counter + 1"/>
+</xsl:template>
+
+<xsl:template match="*" mode="reals"/>
</xsl:stylesheet>
diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml
index f1e888d98..0dbcd3761 100644
--- a/helm/meta_style/set.xml
+++ b/helm/meta_style/set.xml
@@ -1,12 +1,13 @@
<!DOCTYPE OpList SYSTEM "operator.dtd">
-<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML"
+ xmlns:helm="http://www.cs.unibo.it/helm">
<import href="modeset.xsl"/>
<Operator
name = "IN"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
+ uri = "cic:/Coq/Sets/Ensembles/In.con"
cook = "true"
arity = "2">
<mapp>
@@ -18,7 +19,7 @@
<NotOperator
name = "NOT IN"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
+ uri = "cic:/Coq/Sets/Ensembles/In.con"
cook = "true"
arity = "2">
<mapp>
@@ -28,86 +29,95 @@
</mapp>
</NotOperator>
-<OpSet
+<Operator
name = "EMPTY SET"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
- cook = "true">
-
- <Case arity="0">
- <mop tag="set" helm:xref="$APP-ID"/>
- </Case>
-
- <Case arity="1">
+ uri = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
+ cook = "true"
+ arity = "1">
<mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+ <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
<param id="1"/>
<mop tag="set" helm:xref="$APP-ID"/>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
- name = "SINGLETON"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind"
+<Operator
+ name = "EMPTY SET"
+ uri = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
cook = "true">
+ <mop tag="set" helm:xref="$APP-ID"/>
+</Operator>
- <Case arity="1">
+
+<Operator
+ name = "SINGLETON"
+ uri = "cic:/Coq/Sets/Ensembles/Singleton.ind"
+ cook = "true"
+ arity = "1">
<mop tag="set" helm:xref="$APP-ID">
<param id="1"/>
</mop>
- </Case>
+</Operator>
- <Case arity="2">
+<Operator
+ name = "SINGLETON"
+ uri = "cic:/Coq/Sets/Ensembles/Singleton.ind"
+ cook = "true"
+ arity = "2">
<mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+ <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
<param id="2"/>
<m:set definitionURL="$OP-URI">
<param id="1"/>
</m:set>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
+<Operator
name = "COUPLE"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind"
- cook = "true">
-
- <Case arity="2">
+ uri = "cic:/Coq/Sets/Ensembles/Couple.ind"
+ cook = "true"
+ arity = "2">
<mop tag="set" helm:xref="$APP-ID">
<param id="1"/>
<param id="2"/>
</mop>
- </Case>
+</Operator>
- <Case arity="3">
+<Operator
+ name = "COUPLE"
+ uri = "cic:/Coq/Sets/Ensembles/Couple.ind"
+ cook = "true"
+ arity = "3">
<mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+ <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
<param id="3"/>
<m:set definitionURL="$OP-URI">
<param id="1"/>
<param id="2"/>
</m:set>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
+<Operator
name = "TRIPLE"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind"
- cook = "true">
-
- <Case arity="3">
+ uri = "cic:/Coq/Sets/Ensembles/Triple.ind"
+ cook = "true"
+ arity = "3">
<mop tag="set">
<param id="1"/>
<param id="2"/>
<param id="3"/>
</mop>
- </Case>
+</Operator>
- <Case arity="4">
+<Operator
+ name = "TRIPLE"
+ uri = "cic:/Coq/Sets/Ensembles/Triple.ind"
+ cook = "true"
+ arity = "4">
<mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+ <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
<param id="4"/>
<m:set definitionURL="$OP-URI">
<param id="1"/>
@@ -115,23 +125,25 @@
<param id="3"/>
</m:set>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
+<Operator
name = "INTERSECTION"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind"
- cook = "true">
-
- <Case arity="2">
+ uri = "cic:/Coq/Sets/Ensembles/Intersection.ind"
+ cook = "true"
+ arity = "2">
<mapp>
<mop tag="intersect"/>
<param id="1" mode="set"/>
<param id="2" mode="set"/>
</mapp>
- </Case>
+</Operator>
- <Case arity="3">
+<Operator
+ name = "INTERSECTION"
+ uri = "cic:/Coq/Sets/Ensembles/Intersection.ind"
+ cook = "true"
+ arity = "3">
<mapp>
<m:in/>
<param id="3"/>
@@ -141,23 +153,25 @@
<param id="2" mode="set"/>
</m:apply>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
+<Operator
name = "UNION"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Union.ind"
- cook = "true">
-
- <Case arity="2">
+ uri = "cic:/Coq/Sets/Ensembles/Union.ind"
+ cook = "true"
+ arity = "2">
<mapp>
<mop tag="union"/>
<param id="1" mode="set"/>
<param id="2" mode="set"/>
</mapp>
- </Case>
+</Operator>
- <Case arity="3">
+<Operator
+ name = "UNION"
+ uri = "cic:/Coq/Sets/Ensembles/Union.ind"
+ cook = "true"
+ arity = "3">
<mapp>
<m:in/>
<param id="3"/>
@@ -167,12 +181,11 @@
<param id="2" mode="set"/>
</m:apply>
</mapp>
- </Case>
-</OpSet>
+</Operator>
<Operator
name = "INCLUDED"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Included.con"
+ uri = "cic:/Coq/Sets/Ensembles/Included.con"
cook = "true"
arity = "2">
<mapp>
@@ -184,7 +197,7 @@
<Operator
name = "STRICTLY INCLUDED"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con"
+ uri = "cic:/Coq/Sets/Ensembles/Strict_Included.con"
cook = "true"
arity = "2">
<mapp>
@@ -194,20 +207,23 @@
</mapp>
</Operator>
-<OpSet
+<Operator
name = "SET-DIFF"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con"
- cook = "true">
-
- <Case arity="2">
+ uri = "cic:/Coq/Sets/Ensembles/Setminus.con"
+ cook = "true"
+ arity = "2">
<mapp>
<mop tag="setdiff"/>
<param id="1" mode="set"/>
<param id="2" mode="set"/>
</mapp>
- </Case>
+</Operator>
- <Case arity="3">
+<Operator
+ name = "SET-DIFF"
+ uri = "cic:/Coq/Sets/Ensembles/Setminus.con"
+ cook = "true"
+ arity = "3">
<mapp>
<m:in/>
<param id="3"/>
@@ -217,15 +233,13 @@
<param id="2" mode="set"/>
</m:apply>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
+<Operator
name = "ADD-ELEM"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Add.con"
- cook = "true">
-
- <Case arity="2">
+ uri = "cic:/Coq/Sets/Ensembles/Add.con"
+ cook = "true"
+ arity = "2">
<mapp>
<mop tag="union"/>
<param id="1" mode="set"/>
@@ -233,9 +247,13 @@
<param id="2" mode="set"/>
</m:set>
</mapp>
- </Case>
+</Operator>
- <Case arity="3">
+<Operator
+ name = "ADD-ELEM"
+ uri = "cic:/Coq/Sets/Ensembles/Add.con"
+ cook = "true"
+ arity = "3">
<mapp>
<m:in/>
<param id="3"/>
@@ -247,15 +265,13 @@
</m:set>
</m:apply>
</mapp>
- </Case>
-</OpSet>
+</Operator>
-<OpSet
+<Operator
name = "SUBTRACT-ELEM"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con"
- cook = "true">
-
- <Case arity="2">
+ uri = "cic:/Coq/Sets/Ensembles/Subtract.con"
+ cook = "true"
+ arity = "2">
<mapp>
<mop tag="setdiff"/>
<param id="1" mode="set"/>
@@ -263,9 +279,13 @@
<param id="2"/>
</m:set>
</mapp>
- </Case>
+</Operator>
- <Case arity="3">
+<Operator
+ name = "SUBTRACT-ELEM"
+ uri = "cic:/Coq/Sets/Ensembles/Subtract.con"
+ cook = "true"
+ arity = "3">
<mapp>
<m:in/>
<param id="3"/>
@@ -277,12 +297,11 @@
</m:set>
</m:apply>
</mapp>
- </Case>
-</OpSet>
+</Operator>
<Operator
name = "CARD"
- uri = "cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind"
+ uri = "cic:/Coq/Sets/Finite_sets/cardinal.ind"
cook = "true"
arity = "2">
<mapp>
@@ -297,7 +316,7 @@
<Operator
name = "SIGMA"
- uri = "cic:/Coq/Init/Specif/Subsets/sig.ind"
+ uri = "cic:/Coq/Init/Specif/sig.ind"
arity = "2">
<m:set>
<mbvar name="x">
diff --git a/helm/meta_style/xslt_index.txt b/helm/meta_style/xslt_index.txt
index 889ce4c6c..2f683f28d 100644
--- a/helm/meta_style/xslt_index.txt
+++ b/helm/meta_style/xslt_index.txt
@@ -3,5 +3,6 @@ arith.xsl
basic.xsl
reals.xsl
set.xsl
+list.xsl
positive.xsl
modeset.xsl
diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl
index 97f259d67..9cc298f09 100644
--- a/helm/style/annotatedcont.xsl
+++ b/helm/style/annotatedcont.xsl
@@ -35,9 +35,9 @@
<xsl:import href="objcontent.xsl"/>
-<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
+<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate|ConstantType|ConstantBody|CurrentProof|InductiveDefinition|Variable"/>
-<xsl:template match="Definition|Axiom|CurrentProof|InductiveDefinition|Variable">
+<xsl:template match="ConstantType|ConstantBody|CurrentProof|InductiveDefinition|Variable">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
<xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
@@ -51,7 +51,7 @@
</xsl:choose>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
<xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index e60a85051..001ff876d 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"/> -->
@@ -62,63 +63,98 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
<!-- CIC TERMS -->
+
<xsl:template match="LAMBDA" mode="pure">
- <m:lambda helm:xref="{@id}">
- <m:bvar>
- <m:ci>
- <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
- </m:ci>
- <m:type>
- <xsl:apply-templates select="source/*[1]" mode="noannot"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates select="target/*[1]" mode="noannot"/>
- </m:lambda>
+ <xsl:apply-templates select="*[1]" mode="lambda"/>
+</xsl:template>
+
+<xsl:template match="decl" mode="lambda">
+ <m:lambda helm:xref="{@id}">
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="lambda"/>
+ </m:lambda>
+</xsl:template>
+
+
+<xsl:template match="target" mode="lambda">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
</xsl:template>
+
<xsl:template match="LETIN" mode="pure">
+ <xsl:apply-templates select="*[1]" mode="letin_pure"/>
+</xsl:template>
+
+<!-- Andrea: mode letin already exists in proofs.xsl, with a
+ different meaning -->
+
+<xsl:template match="def" mode="letin_pure">
<m:apply helm:xref="{@id}">
<m:csymbol>let_in</m:csymbol>
<m:bvar>
<m:ci>
- <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="letintarget/@binder"/></xsl:with-param></xsl:call-template>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
</m:ci>
</m:bvar>
<xsl:apply-templates select="*[1]" mode="noannot"/>
- <xsl:apply-templates select="letintarget/*[1]" mode="noannot"/>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="letin_pure"/>
</m:apply>
</xsl:template>
+
+<xsl:template match="target" mode="letin_pure">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+
<xsl:template match="PROD" mode="pure">
- <m:apply helm:xref="{@id}">
- <xsl:choose>
- <xsl:when test="string(target/@binder)= """>
- <m:csymbol>arrow</m:csymbol>
- <xsl:apply-templates select="source/*[1]" mode="noannot"/>
- </xsl:when>
- <xsl:otherwise>
+ <xsl:apply-templates select="*[1]" mode="prod"/>
+</xsl:template>
+
+
+<xsl:template match="decl" mode="prod">
+ <m:apply helm:xref="{@id}">
<xsl:choose>
- <xsl:when test="@type = 'Prop'">
- <m:csymbol>forall</m:csymbol>
+ <xsl:when test="string(@binder)= """>
+ <m:csymbol>arrow</m:csymbol>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
</xsl:when>
<xsl:otherwise>
- <m:csymbol>prod</m:csymbol>
+ <xsl:choose>
+ <xsl:when test="../@type = 'Prop'">
+ <m:csymbol>forall</m:csymbol>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:csymbol>prod</m:csymbol>
+ </xsl:otherwise>
+ </xsl:choose>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
</xsl:otherwise>
</xsl:choose>
- <m:bvar>
- <m:ci>
- <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
- </m:ci>
- <m:type>
- <xsl:apply-templates select="source/*[1]" mode="noannot"/>
- </m:type>
- </m:bvar>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:apply-templates select="target/*[1]" mode="noannot"/>
- </m:apply>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="prod"/>
+ </m:apply>
+</xsl:template>
+
+
+<xsl:template match="target" mode="prod">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
</xsl:template>
+
<xsl:template match="CAST" mode="pure">
<m:apply helm:xref="{@id}">
<m:csymbol>cast</m:csymbol>
@@ -126,12 +162,14 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+
<xsl:template match="REL" mode="pure">
<m:ci helm:xref="{@id}">
<xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
</m:ci>
</xsl:template>
+
<xsl:template match="SORT" mode="pure">
<m:apply helm:xref="{@id}">
<m:csymbol>
@@ -140,6 +178,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+
<xsl:template match="APPLY" mode="pure">
<m:apply helm:xref="{@id}">
<m:csymbol>app</m:csymbol>
@@ -147,6 +186,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+
<!-- Gestione senza pre-processing -->
<!--
<xsl:template match="APPLY" mode="pure">
@@ -163,10 +203,12 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
<xsl:template match="VAR" mode="pure">
<m:ci helm:xref="{@id}">
- <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="substring-after(@relUri,",")"/></xsl:with-param></xsl:call-template>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri_bis">
+ <xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:with-param></xsl:call-template>
</m:ci>
</xsl:template>
+
<xsl:template match="META" mode="pure">
<m:apply helm:xref="{@id}">
<m:csymbol>meta</m:csymbol>
@@ -191,6 +233,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+
<xsl:template match="CONST" mode="pure">
<m:ci definitionURL="{@uri}" helm:xref="{@id}">
<xsl:call-template name="insert_subscript">
@@ -203,6 +246,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:ci>
</xsl:template>
+
<xsl:template match="MUTIND" mode="pure">
<m:ci definitionURL="{@uri}" helm:xref="{@id}">
<xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
@@ -211,6 +255,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:ci>
</xsl:template>
+
<xsl:template match="MUTCONSTRUCT" mode="pure">
<m:ci definitionURL="{@uri}" helm:xref="{@id}">
<xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
@@ -220,6 +265,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:ci>
</xsl:template>
+
<xsl:template match="MUTCASE" mode="pure">
<xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
<xsl:variable name="Turi"><xsl:value-of select="@uriType"/></xsl:variable>
@@ -258,6 +304,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+
<xsl:template match="FIX" mode="pure">
<m:apply helm:xref="{@id}">
<xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
@@ -267,6 +314,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+
<xsl:template match="COFIX" mode="pure">
<m:apply helm:xref="{@id}">
<xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
@@ -276,6 +324,37 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
</m:apply>
</xsl:template>
+<xsl:template match="instantiate" mode="pure">
+ <m:apply>
+ <xsl:if test="@id">
+ <xsl:attribute name="helm:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>
+ <m:csymbol>inst</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[1]" />
+ <xsl:for-each select="arg">
+ <xsl:variable name="base_path">
+ <xsl:call-template name="path">
+ <xsl:with-param name="uri" select="../*[1]/@uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="varUri" select="concat($base_path,@relUri)"/>
+ <m:ci definitionURL="{$varUri}">
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value">
+ <xsl:call-template name="name_of_uri">
+ <xsl:with-param name="uri" select="$varUri"/>
+ <xsl:with-param name="extension" select="'.var'"/>
+ </xsl:call-template>
+ </xsl:with-param>
+ </xsl:call-template>
+ </m:ci>
+ <xsl:apply-templates mode ="noannot" select="*[1]" />
+ </xsl:for-each>
+ </m:apply>
+</xsl:template>
+
<!-- ELEMENTS OF CIC TERMS -->
<xsl:template match="FixFunction" mode="pure">
@@ -286,6 +365,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
<xsl:apply-templates select="body/*[1]" mode="noannot"/>
</xsl:template>
+
<xsl:template match="CofixFunction" mode="pure">
<m:bvar>
<m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@name"/></xsl:with-param></xsl:call-template></m:ci>
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 856fd6971..56231b2bc 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -39,6 +39,7 @@
<xsl:include href="html_init.xsl"/>
<xsl:include href="html_set.xsl"/>
<xsl:include href="html_reals.xsl"/>
+<xsl:include href="html_ccorns.xsl"/>
<xsl:variable name="showcast" select="0"/>
@@ -69,6 +70,12 @@
<xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
<xsl:variable name="fontsymbol">
<xsl:choose>
+ <xsl:when test="$symbol = 'append'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'iff'">
+ <xsl:value-of select="'«'"/>
+ </xsl:when>
<xsl:when test="$symbol = 'forall'">
<xsl:value-of select="'"'"/>
</xsl:when>
@@ -114,6 +121,12 @@
<xsl:otherwise>
<xsl:variable name="unicodesymbol">
<xsl:choose>
+ <xsl:when test="$symbol = 'append'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'iff'">
+ <xsl:value-of select="'↔'"/>
+ </xsl:when>
<xsl:when test="$symbol = 'forall'">
<xsl:value-of select="'∀'"/>
</xsl:when>
@@ -215,6 +228,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> </xsl:text>
<xsl:call-template name="make_indent">
@@ -311,6 +330,30 @@
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<xsl:text>)</xsl:text>
</xsl:when>
+ <!-- IFF -->
+ <xsl:when test="$name='iff'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
<!-- APP -->
<xsl:when test="$name='app'">
<xsl:text>(</xsl:text>
@@ -325,7 +368,7 @@
<xsl:when test="$name='cast'">
<xsl:text>(</xsl:text>
<xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:text>:></xsl:text>
+ <xsl:text>:</xsl:text>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<xsl:text>)</xsl:text>
</xsl:when>
@@ -363,6 +406,23 @@
select="./*[1]"/>
</xsl:for-each>
</xsl:when>
+
+ <xsl:when test="$name='inst'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <FONT color="blue">{</FONT>
+ <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+ <xsl:apply-templates select="following-sibling::*[position() = 1]" mode="inline"/>
+ <FONT color="blue">/</FONT>
+ <xsl:if test="name()='m:ci'">
+ <a href="{@definitionURL}">
+ <xsl:apply-templates/>
+ </a>
+ </xsl:if>
+ <!-- <xsl:apply-templates select="." mode="inline"/> -->
+ </xsl:for-each>
+ <FONT color="blue">}</FONT>
+ </xsl:when>
+
<!-- FIX -->
<xsl:when test="$name='fix'">
<FONT color="red">FIX</FONT>
@@ -407,6 +467,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]"/>
@@ -768,6 +837,10 @@
<!-- <xsl:value-of select="$charlength"/> -->
<xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
<xsl:choose>
+ <!-- inst -->
+ <xsl:when test="$name='inst'">
+ <xsl:apply-templates select="." mode="inline"/>
+ </xsl:when>
<!-- FORALL -->
<xsl:when test="$name='forall'">
<xsl:choose>
@@ -854,6 +927,62 @@
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- IFF -->
+ <xsl:when test="$name='iff'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
<!-- APP -->
<xsl:when test="$name='app'">
<xsl:choose>
@@ -1074,6 +1203,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 ************** -->
@@ -1089,6 +1241,24 @@
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
 
+ <xsl:if test="*[4]">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">we proved </FONT>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">and by delta equivalence</FONT>
+ <xsl:apply-templates select="*[position()=5]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:apply-templates>
+ </xsl:if>
</span>
<xsl:choose>
<xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
@@ -1112,7 +1282,7 @@
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:call-template>\
- <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
+ <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we obtain</a>\
</span>\
');
document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
@@ -1130,7 +1300,7 @@
</script>
</xsl:otherwise>
</xsl:choose>
- <xsl:apply-templates select="*[position()=3]">
+ <xsl:apply-templates select="*[position()=last()]">
<xsl:with-param name="current_indent" select="$current_indent + 16"/>
</xsl:apply-templates>
</xsl:when>
diff --git a/helm/style/diseq.xsl b/helm/style/diseq.xsl
new file mode 100644
index 000000000..dd3650db7
--- /dev/null
+++ b/helm/style/diseq.xsl
@@ -0,0 +1,336 @@
+<?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/. -->
+
+<!--******************************************************************-->
+<!-- Disequalities -->
+<!-- (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">
+
+<!-- ************************* LOGIC *********************************-->
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="diseq" match="*">
+ <xsl:param name="rel" select="'eq'"/>
+ <xsl:choose>
+ <xsl:when test="name()='APPLY'">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:choose>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- REALS -->
+ <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6">
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6">
+ <xsl:apply-templates mode="diseq" select="*[5]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:element name="{concat('m:',$rel)}"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:element name="{concat('m:',$rel)}"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
+</xsl:stylesheet>
diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl
index b31160eab..7b1316013 100644
--- a/helm/style/drop_coercions.xsl
+++ b/helm/style/drop_coercions.xsl
@@ -40,18 +40,18 @@
<!-- coercions -->
<xsl:template match="APPLY[CONST[position()='1' and
- (@uri='cic:/Algebra/CSemiGroups/csg_crr.con' or
- @uri='cic:/Algebra/CMonoids/cm_crr.con' or
- @uri='cic:/Algebra/CGroups/cg_crr.con' or
- @uri='cic:/Algebra/CRings/cr_crr.con' or
- @uri='cic:/Algebra/CFields/cf_crr.con' or
- @uri='cic:/Algebra/COrdFields/cof_crr.con' or
- @uri='cic:/Algebra/CReals/crl_crr.con')]]">
+ (@uri='cic:/Algebra/algebra/CSemiGroups/csg_crr.con' or
+ @uri='cic:/Algebra/algebra/CMonoids/cm_crr.con' or
+ @uri='cic:/Algebra/algebra/CGroups/cg_crr.con' or
+ @uri='cic:/Algebra/algebra/CRings/cr_crr.con' or
+ @uri='cic:/Algebra/algebra/CFields/cf_crr.con' or
+ @uri='cic:/Algebra/algebra/COrdFields/cof_crr.con' or
+ @uri='cic:/Algebra/reals/CReals/crl_crr.con')]]">
<xsl:apply-templates select="*[position()=last()]"/>
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
+ @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
@@ -84,7 +84,7 @@
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
+ @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
@@ -119,7 +119,7 @@
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
+ @uri='cic:/Algebra/algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
@@ -154,7 +154,7 @@
</xsl:template>
<xsl:template match="APPLY[CONST[position()='1' and
- @uri='cic:/Algebra/CRings/nat_injection/nring.con']]">
+ @uri='cic:/Algebra/algebra/CRings/nat_injection/nring.con']]">
<xsl:variable name="no_params">
<xsl:call-template name="get_no_params">
<xsl:with-param name="first_uri" select="$CICURI"/>
diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl
index f60883079..add3247b3 100644
--- a/helm/style/headercontent.xsl
+++ b/helm/style/headercontent.xsl
@@ -31,13 +31,17 @@
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
-<xsl:include href="contentlib.xsl"/> <!-- FG -->
+<!-- Warning: the first included stylesheet has the lowest precedence -->
+<xsl:include href="contentlib.xsl"/>
<xsl:include href="basic.xsl"/>
-<xsl:include href="arith.xsl"/> <!-- FG -->
+<xsl:include href="arith.xsl"/>
<xsl:include href="set.xsl"/>
+<xsl:include href="list.xsl"/>
<xsl:include href="reals.xsl"/>
-<xsl:include href="ring.xsl"/> <!-- FG -->
+<xsl:include href="ring.xsl"/>
<xsl:include href="algebra.xsl"/>
<xsl:include href="lambda.xsl"/>
+<xsl:include href="positive.xsl"/>
+<xsl:include href="ccorn.xsl"/>
</xsl:stylesheet>
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 83569d751..1d6dc4dd7 100644
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -26,6 +26,7 @@
<!--******************************************************************-->
<!-- XSLT version 0.1 of CIC inductive objects to MathML content: -->
+<!-- Completely revisited: November 2002, Andrea asperti -->
<!-- First draft: March 2001, Andrea asperti -->
<!--******************************************************************-->
@@ -34,20 +35,80 @@
xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
+<!-- try_inductive essentially checks if the head constant is an
+ invocation of an induction principle.
+ Si presuppone che il tipo induttivo non sia mutuamente
+ induttivo. Bisognerebbe andare a vedere l'utlimo parametro
+ del presunto "principio di induzione", tirare fuori il tipo induttivo
+ e vedere se il suo nome coincide con il prefisso di _ind.
+ Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
+ parametro di nat_double_ind e' di tipo nat, e nat e' diverso
+ da nat_double. Per ora, verifico solo l'esistenza di nat_double,
+ ma questo, benche' non porti ad errore, non copre tutti i
+ casi per quelli mutuamente induttivi -->
+
+
+<xsl:template mode="try_inductive" match="APPLY">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="uri">
+ <xsl:choose>
+ <xsl:when test="name(*[1])='CONST'">
+ <xsl:value-of select="*[1]/@uri"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- instantiate -->
+ <xsl:value-of select="*[1]/CONST[1]/@uri"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="contains($uri,'_ind.con')">
+ <xsl:variable name="ind_uri"
+ select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
+ <xsl:variable name="inductive_def"
+ select="document($InductiveTypeUrl)/InductiveDefinition"/>
+ <xsl:choose>
+ <xsl:when test="$inductive_def">
+ <xsl:variable name="ind_name">
+ <xsl:call-template name="get_name">
+ <xsl:with-param name="uri" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:apply-templates mode="inductive" select=".">
+ <xsl:with-param name="uri" select="$uri"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$ind_uri"/>
+ <xsl:with-param name="inductive_def" select="$inductive_def"/>
+ <xsl:with-param name="inductive_def_index" select="1"/>
+ <xsl:with-param name="inductive_def_name" select="$ind_name"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="." mode="letin"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="." mode="letin"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
<xsl:template mode="inductive" match="APPLY">
+ <xsl:param name="uri" select="''"/>
<xsl:param name="inductive_def_uri" select="''"/>
<xsl:param name="inductive_def" select="/.."/>
<xsl:param name="inductive_def_index" select="1"/>
<xsl:param name="inductive_def_name" select="''"/>
- <xsl:param name="section_params" select="0"/>
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$uri"/></xsl:call-template></xsl:variable>
<!-- expected_args_type contains the types of the arguments expected by
the induction principle -->
- <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
<xsl:variable name="expected_args_types"
- select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+ select="document($InductiveTypeUrl)/ConstantType/PROD/decl/*[1]"/>
<xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
- <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
+ <xsl:variable name="actual_arguments" select="*[position()>1]"/>
<!-- First check that the induction principle is applied to the
expected number of arguments -->
<xsl:choose>
@@ -65,7 +126,7 @@
<xsl:when test="string($argsOK) = 'true'">
<!-- arguments are in the expected form: we create a
"by_induction" content element -->
- <!-- no_params is the number of paramters in square brackets -->
+ <!-- no_params is the number of parameters in square brackets -->
<xsl:variable name="no_params"
select="$inductive_def/@noParams"/>
<!-- the inductive property is the first argument following
@@ -93,7 +154,7 @@
is the uri of the inductive definition -->
<m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
<!-- next, we have the inductive property, currently not
- used for rendering (it could be omitted??) -->
+ used for rendering (it could be omitted ??) -->
<xsl:apply-templates mode="pure" select="$inductive_property"/>
<!-- each case has its own "inductive_case" element -->
<!-- the inductive case element is composed by:
@@ -117,40 +178,44 @@
<m:csymbol>case_lhs</m:csymbol>
<m:ci definitionURL="{$inductive_def_uri}">
<xsl:value-of select="@name"/>
- </m:ci>
+ </m:ci>
<xsl:call-template name="get_constructor_args">
- <xsl:with-param name="no_params"
- select="$no_params"/>
- <xsl:with-param name="constructor_arity"
- select="*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$current_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
+ <xsl:with-param name="constructor_args"
+ select="PROD/decl[position()> $no_params]"/>
+ <xsl:with-param name="actual_args"
+ select="$current_arg/decl"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ </xsl:call-template>
</m:apply>
<m:apply>
<m:csymbol>induction_hypothesis</m:csymbol>
<xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="no_params"
- select="$no_params"/>
- <xsl:with-param name="constructor_arity"
- select="*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$current_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="PROD/decl[position()> $no_params]"/>
+ <xsl:with-param name="actual_args"
+ select="$current_arg/decl"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</m:apply>
- <xsl:call-template name="get_body">
- <xsl:with-param name="no_params"
- select="$no_params"/>
- <xsl:with-param name="constructor_arity"
- select="*[1]"/>
- <xsl:with-param name="actual_arg" select="$current_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="count(PROD/decl) > $no_params">
+ <!-- in this case the actual_arg must be a LAMBDA -->
+ <xsl:call-template name="get_body">
+ <xsl:with-param name="constructor_args"
+ select="PROD/decl[position()>$no_params]"/>
+ <xsl:with-param name="actual_args" select="$current_arg/decl"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ <xsl:with-param name="target"
+ select="$current_arg/target/*[1]"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="noannot" select="$current_arg"/>
+ </xsl:otherwise>
+ </xsl:choose>
</m:apply>
</xsl:for-each>
<!-- the inductive argument is the last argument of extra-args -->
@@ -179,28 +244,24 @@
If this is not the case, not good rendering looks possible.
Check_args returns a boolean.
-->
+
+
<xsl:template name="check_args">
<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">
- <xsl:apply-templates mode="count_arity" select="$arg_types[1]">
- <xsl:with-param name="what" select="'PROD'"/>
- </xsl:apply-templates>
- </xsl:variable>
- <xsl:variable name="no_actual_abst_of_arg">
- <xsl:apply-templates mode="count_arity" select="$actual_args[1]">
- <xsl:with-param name="what" select="'LAMBDA'"/>
- </xsl:apply-templates>
- </xsl:variable>
- <!-- REPLACE WITH EQUALITY ???? -->
+ <xsl:variable name="no_expected_arg_of_arg"
+ select="count($arg_types[1]/decl)"/>
+ <xsl:variable name="no_actual_abst_of_arg"
+ 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]"/>
@@ -208,25 +269,8 @@
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
-</xsl:template>
+</xsl:template>
-<!-- count_arity counts the number of head lambda (or prod) -->
-<xsl:template mode="count_arity" match="*">
- <xsl:param name="what" select="'LAMBDA'"/>
- <xsl:param name="num" select="0"/>
- <!-- MANCANO I CAST ??? -->
- <xsl:choose>
- <xsl:when test="name(.) = $what">
- <xsl:apply-templates mode="count_arity" select="target/*[1]">
- <xsl:with-param name="what" select="$what"/>
- <xsl:with-param name="num" select="$num+1"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="$num"/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
<!-- The following three functions are essentially identical
in their recursive structure.
@@ -246,162 +290,127 @@
single one without a conversion from document tree fragments
to node-sets.
-->
+
<xsl:template name="get_constructor_args">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
- <xsl:if test="name($constructor_arity)='PROD'">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:if test="$constructor_args">
<m:bvar>
- <m:ci><xsl:value-of select="$actual_arg/target/@binder"/></m:ci>
+ <m:ci><xsl:value-of select="$actual_args[1]/@binder"/></m:ci>
<m:type>
- <xsl:apply-templates mode="pure" select="$actual_arg/source/*[1]"/>
+ <xsl:apply-templates mode="pure" select="$actual_args[1]/*"/>
</m:type>
</m:bvar>
<xsl:choose>
- <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+ <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
<xsl:call-template name="get_constructor_args">
<xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/LAMBDA/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>2]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="get_constructor_args">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>1]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:if>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_constructor_args">
- <xsl:with-param name="no_params" select="$no_params - 1"/>
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
+</xsl:template>
<xsl:template name="get_induction_hypothesis">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
- <xsl:if test="name($constructor_arity)='PROD'">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:if test="$constructor_args">
<xsl:choose>
- <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+ <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
<m:bvar>
<m:ci>
- <xsl:value-of select="$actual_arg/target/LAMBDA/target/@binder"/>
+ <xsl:value-of select="$actual_args[2]/@binder"/>
</m:ci>
<m:type>
<xsl:apply-templates mode="pure"
- select="$actual_arg/target/LAMBDA/source"/>
+ select="$actual_args[2]/*"/>
</m:type>
</m:bvar>
<xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/LAMBDA/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>2]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()>1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()>1]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:if>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_induction_hypothesis">
- <xsl:with-param name="no_params" select="$no_params - 1"/>
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
</xsl:template>
<xsl:template name="get_body">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:param name="target" select="/.."/>
<xsl:choose>
- <xsl:when test="name($constructor_arity)='PROD'">
- <xsl:choose>
- <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
- <xsl:call-template name="get_body">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/LAMBDA/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_body">
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg/target/*[1]"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="noannot" select="$actual_arg"/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_body">
- <xsl:with-param name="no_params" select="$no_params - 1"/>
- <xsl:with-param name="constructor_arity"
- select="$constructor_arity/target/*[1]"/>
- <xsl:with-param name="actual_arg"
- select="$actual_arg"/>
- <xsl:with-param name="inductive_def_name"
- select="$inductive_def_name"/>
- </xsl:call-template>
- </xsl:otherwise>
+ <xsl:when test="$constructor_args">
+ <xsl:choose>
+ <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
+ <xsl:call-template name="get_body">
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()> 1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()> 2]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ <xsl:with-param name="target"
+ select="$target"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="get_body">
+ <xsl:with-param name="constructor_args"
+ select="$constructor_args[position()> 1]"/>
+ <xsl:with-param name="actual_args"
+ select="$actual_args[position()> 1]"/>
+ <xsl:with-param name="inductive_def_uri"
+ select="$inductive_def_uri"/>
+ <xsl:with-param name="target"
+ select="$target"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:choose>
+ <xsl:when test="$actual_args">
+ <xsl:apply-templates select="$actual_args[1]" mode="lambda_prop"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="noannot" select="$target"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:otherwise>
</xsl:choose>
-</xsl:template>
+</xsl:template>
</xsl:stylesheet>
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/link.xsl b/helm/style/link.xsl
index e3568a18f..e6d639a3b 100644
--- a/helm/style/link.xsl
+++ b/helm/style/link.xsl
@@ -39,6 +39,8 @@
<xsl:key name="id" use="@id" match="m:*"/>
+<xsl:param name="URLs_or_URIs" select="'URLs'"/>
+
<xsl:template match = "m:semantics">
<xsl:apply-templates select="*[1]" mode="semantics"/>
</xsl:template>
@@ -52,7 +54,14 @@ xlink:href) -->
<xsl:variable name="cnode" select="key('id',@xref)"/>
<xsl:if test="$cnode/@definitionURL">
<xsl:attribute name="xlink:href">
- <xsl:call-template name="makeURL"><xsl:with-param name="uri" select="$cnode/@definitionURL"/></xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="$URLs_or_URIs = 'URLs'">
+ <xsl:call-template name="makeURL"><xsl:with-param name="uri" select="$cnode/@definitionURL"/></xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$cnode/@definitionURL"/>
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:attribute>
<!-- xlink:show='other' requires the exact modality to be -->
<!-- specified in non-xlink markup. The point is that the -->
diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl
new file mode 100644
index 000000000..0a261260a
--- /dev/null
+++ b/helm/style/logic.xsl
@@ -0,0 +1,155 @@
+<?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/. -->
+
+<!--******************************************************************-->
+<!-- Basic Logic -->
+<!-- (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 mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and count(child::*) = 3]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>false_ind</m:csymbol>
+ <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ </m:apply>
+</xsl:template>
+
+
+<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]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>and_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[6]"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <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: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>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/or_ind.con']
+ and count(child::*) = 7 and
+ name(*[5])='LAMBDA' and count(*[5]/decl) = 1 and
+ name(*[6])='LAMBDA' and count(*[6]/decl) = 1 ]">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="definition_url"
+ select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>full_or_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[7]"/>
+ <xsl:for-each select="$InnerTypes">
+ <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+ </xsl:for-each>
+ <m:apply>
+ <m:csymbol>left_case</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:value-of select="*[5]/*[1]/@binder"/>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+ </m:apply>
+ <m:apply>
+ <m:csymbol>right_case</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates mode="pure" select="*[6]/*[1]/*"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates mode="noannot" select="*[6]/target"/>
+ </m:apply>
+ </m:apply>
+
+<!-- da tertminare
+ </xsl:when>
+ <xsl:otherwise>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>or_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[7]"/>
+ <xsl:for-each select="$InnerTypes">
+ <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+ </xsl:for-each>
+ <xsl:apply-templates mode="pure" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ </m:apply>
+ </xsl:otherwise>
+ </xsl:choose>
+-->
+</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 ]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>ex_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[6]"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <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: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/mk_meta_and_dep_graph.xsl b/helm/style/mk_meta_and_dep_graph.xsl
index a9a9a954b..c860e4b46 100644
--- a/helm/style/mk_meta_and_dep_graph.xsl
+++ b/helm/style/mk_meta_and_dep_graph.xsl
@@ -24,16 +24,10 @@
<!-- For details, see the HELM World-Wide-Web page, -->
<!-- http://cs.unibo.it/helm/. -->
-<!-- CSC: Sostituire l'andata a capo con la entity numerica opportuna -->
-<!DOCTYPE html [
- <!ENTITY CSCbr "
-">
-]>
-
<xsl:stylesheet version="1.0"
xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
- xmlns:h="http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#">
+ xmlns:h="http://www.cs.unibo.it/helm/schemas/mattone.rdf#">
<xsl:output method="text"/>
@@ -159,9 +153,9 @@
<xsl:template match="/">
<!--
- <xsl:text>strict digraph L0 { size = "83,83"; concentrate=true; node [style=filled, shape = box];&CSCbr;</xsl:text>
+ <xsl:text>strict digraph L0 { size = "83,83"; concentrate=true; node [style=filled, shape = box];
</xsl:text>
-->
- <xsl:text>strict digraph L0 { size = "83,83"; node [style=filled, shape = box];&CSCbr;</xsl:text>
+ <xsl:text>strict digraph L0 { size = "83,83"; node [style=filled, shape = box];
</xsl:text>
<xsl:variable name="quoted_CICURI">
<xsl:call-template name="quote_url">
<xsl:with-param name="s" select="$CICURI"/>
@@ -239,7 +233,7 @@
<xsl:if test="name(document(concat($uri_set_queueURL,'is_overflowed?uri=',$quotedCurrentCICURI,'&nonce=',generate-id(),'&PID=',$PID))/*)='true'">
<xsl:text>,color=red</xsl:text>
</xsl:if>
- <xsl:text>];&CSCbr;</xsl:text>
+ <xsl:text>];
</xsl:text>
</xsl:template>
<xsl:template match="*">
@@ -248,12 +242,12 @@
<xsl:for-each select="*/*/*">
<xsl:variable name="quotedURI">
<xsl:call-template name="quote">
- <xsl:with-param name="s" select="@rdf:value"/>
+ <xsl:with-param name="s" select="h:occurrence"/>
</xsl:call-template>
</xsl:variable>
<xsl:variable name="quoted_uri">
<xsl:call-template name="quote_url">
- <xsl:with-param name="s" select="@rdf:value"/>
+ <xsl:with-param name="s" select="h:occurrence"/>
</xsl:call-template>
</xsl:variable>
<!-- The nonce, quotedCurrentCICURI are used to force the document reload -->
@@ -263,7 +257,7 @@
<xsl:text> -> </xsl:text>
<xsl:value-of select="$quotedURI"/>
<xsl:value-of select="$link_direction"/>
- <xsl:text>;&CSCbr;</xsl:text>
+ <xsl:text>;
</xsl:text>
</xsl:if>
</xsl:for-each>
</xsl:template>
diff --git a/helm/style/mk_meta_theory.xsl b/helm/style/mk_meta_theory.xsl
index 3a07962a9..e433c4b26 100644
--- a/helm/style/mk_meta_theory.xsl
+++ b/helm/style/mk_meta_theory.xsl
@@ -28,25 +28,19 @@
xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
- xmlns:h="http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#">
-
-<xsl:variable name="MainConclusion" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#MainConclusion'"/>
-<xsl:variable name="InConclusion" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#InConclusion'"/>
-<xsl:variable name="MainHypothesis" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#MainHypothesis'"/>
-<xsl:variable name="InHypothesis" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#InHypothesis'"/>
-<xsl:variable name="InBody" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#InBody'"/>
+ xmlns:h="http://www.cs.unibo.it/helm/schemas/mattone.rdf#">
<xsl:template match="/">
<html>
<head>
- <title>Occurrences of <xsl:value-of select="*/*/@rdf:value"/></title>
+ <title>Occurrences of <xsl:value-of select="*/*/@rdf:about"/></title>
<style>
a { text-decoration: none }
a.underline {text-decoration: underline }
</style>
</head>
<!-- CSC: method onLoad to be removed once the window -->
- <!-- CSC: becomes a frame -->
+ <!-- CSC: becomes a frame -->
<body bgcolor="white" onLoad="window.focus()">
<xsl:apply-templates/>
</body>
@@ -55,15 +49,15 @@
<xsl:template match="h:Object">
<xsl:variable name="no_main"
- select="count(*/h:Occurrence[@rdf:about=$MainConclusion])"/>
+ select="count(*/h:Occurrence/h:position[text()='MainConclusion'])"/>
<xsl:variable name="no_concl"
- select="count(*/h:Occurrence[@rdf:about=$InConclusion])"/>
+ select="count(*/h:Occurrence/h:position[text()='InConclusion'])"/>
<xsl:variable name="no_main_hyp"
- select="count(*/h:Occurrence[@rdf:about=$MainHypothesis])"/>
+ select="count(*/h:Occurrence/h:position[text()='MainHypothesis'])"/>
<xsl:variable name="no_in_hyp"
- select="count(*/h:Occurrence[@rdf:about=$InHypothesis])"/>
+ select="count(*/h:Occurrence/h:position[text()='InHypothesis'])"/>
<xsl:variable name="no_body"
- select="count(*/h:Occurrence[@rdf:about=$InBody])"/>
+ select="count(*/h:Occurrence/h:position[text()='InBody'])"/>
<h1>Occurrences of <xsl:value-of select="@rdf:about"/></h1>
<ul>
@@ -92,17 +86,17 @@
<xsl:when test="$no_main = 0"/>
<xsl:when test="15 > $no_main">
<h2><a name="main">Head position inside conclusion:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainConclusion]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='MainConclusion']">
<div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
</div>
</xsl:for-each>
</xsl:when>
<xsl:when test="$no_main >= 15">
<h2><a name="main">Head position inside conclusion:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainConclusion]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='MainConclusion']">
<div style="margin: 0cm 0cm 0cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
</div>
</xsl:for-each>
</xsl:when>
@@ -111,17 +105,17 @@
<xsl:when test="$no_concl = 0"/>
<xsl:when test="15 > $no_concl">
<h2><a name="concl">Inside conclusion:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$InConclusion]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='InConclusion']">
<div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
</div>
</xsl:for-each>
</xsl:when>
<xsl:when test="$no_concl >= 15">
<h2><a name="concl">Inside conclusion:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$InConclusion]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='InConclusion']">
<div style="margin: 0cm 0cm 0cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
</div>
</xsl:for-each>
</xsl:when>
@@ -130,17 +124,17 @@
<xsl:when test="$no_main_hyp = 0"/>
<xsl:when test="15 > $no_main_hyp">
<h2><a name="main_hyp">Head position inside an hypothesis:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainHypothesis]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='MainHypothesis']">
<div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
</div>
</xsl:for-each>
</xsl:when>
<xsl:when test="$no_main_hyp >= 15">
<h2><a name="main_hyp">Head position inside an hypothesis:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainHypothesis]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='MainHypothesis']">
<div style="margin: 0cm 0cm 0cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
</div>
</xsl:for-each>
</xsl:when>
@@ -149,26 +143,26 @@
<xsl:when test="$no_in_hyp = 0"/>
<xsl:when test="15 > $no_in_hyp">
<h2><a name="hyp">Inside an hypothesis:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$InHypothesis]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='InHypothesis']">
<div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
</div>
</xsl:for-each>
</xsl:when>
<xsl:when test="$no_in_hyp >= 15">
<h2><a name="hyp">Inside an hypothesis:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$InHypothesis]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='InHypothesis']">
<div style="margin: 0cm 0cm 0cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
</div>
</xsl:for-each>
</xsl:when>
</xsl:choose>
<xsl:if test="$no_body > 0">
<h2><a name="body">Inside the body:</a></h2>
- <xsl:for-each select="*/h:Occurrence[@rdf:about=$InBody]">
+ <xsl:for-each select="*/h:Occurrence[h:position/text()='InBody']">
<div style="margin: 0cm 0cm 0cm 0.75cm">
- <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+ <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
</div>
</xsl:for-each>
</xsl:if>
diff --git a/helm/style/mmlctop.xsl b/helm/style/mmlctop.xsl
index 554c3a87b..b63ebee8a 100644
--- a/helm/style/mmlctop.xsl
+++ b/helm/style/mmlctop.xsl
@@ -1293,18 +1293,38 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
<xsl:choose>
<xsl:when test="$IN_PREC > $MINUS_PREC or $IN_PREC=$MINUS_PREC and
$PARAM=$PAR_SAME">
- <m:mfenced separators="">
- <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
- <xsl:attribute name="xref">
- <xsl:value-of select="@id"/>
- </xsl:attribute>
- </xsl:if>
- <xsl:apply-templates select="." mode="minus">
- <xsl:with-param name="PARAM" select="$PARAM"/>
- <xsl:with-param name="PAREN" select="$PAR_YES"/>
- <xsl:with-param name="PAR_NO_IGNORE" select="$PAR_NO_IGNORE"/>
- </xsl:apply-templates>
- </m:mfenced>
+ <!-- HELM: m:mrow is now used when the minus operator is unary.
+ Igor used m:mfenced instead. -->
+ <xsl:choose>
+ <xsl:when test="count(*)=2">
+ <m:mrow>
+ <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
+ <xsl:attribute name="xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>
+ <xsl:apply-templates select="." mode="minus">
+ <xsl:with-param name="PARAM" select="$PARAM"/>
+ <xsl:with-param name="PAREN" select="$PAR_YES"/>
+ <xsl:with-param name="PAR_NO_IGNORE" select="$PAR_NO_IGNORE"/>
+ </xsl:apply-templates>
+ </m:mrow>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mfenced separators="">
+ <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
+ <xsl:attribute name="xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>
+ <xsl:apply-templates select="." mode="minus">
+ <xsl:with-param name="PARAM" select="$PARAM"/>
+ <xsl:with-param name="PAREN" select="$PAR_YES"/>
+ <xsl:with-param name="PAR_NO_IGNORE" select="$PAR_NO_IGNORE"/>
+ </xsl:apply-templates>
+ </m:mfenced>
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:when>
<xsl:when test="$IN_PREC > $NO_PREC and $IN_PREC < $FUNCTION_PREC
and not($SEM_SW=$SEM_ALL) and not($SEM_SW=$SEM_XREF)
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 4a801a654..fad3dce6b 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1105,6 +1105,96 @@ which generates the toplevel element (see for instance xlink) -->
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- INST -->
+ <xsl:when test="$name='inst'">
+ <m:mrow>
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo stretchy="false">{</m:mo>
+ <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+ <xsl:apply-templates select="."/>
+ <m:mo stretchy="false">:=</m:mo>
+ <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+ </xsl:for-each>
+ <m:mo stretchy="false">}</m:mo>
+ </m:mrow>
+ </xsl:when>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <xsl:choose>
+ <xsl:when test="$charlength >= $framewidth">
+ <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo>@</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <xsl:apply-templates select="*[3]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mrow>
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo>@</m:mo>
+ <xsl:apply-templates select="*[3]"/>
+ </m:mrow>
+ </xsl:otherwise>
+ </xsl:choose>
+ </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 ************** -->
<!-- ***************************************** -->
@@ -1478,23 +1568,112 @@ which generates the toplevel element (see for instance xlink) -->
</m:mrow>
</m:mtd>
</m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mtext>Rewrite</m:mtext>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <xsl:apply-templates select="*[3]"/>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <m:mtext>with</m:mtext>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <xsl:apply-templates select="*[4]"/>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <m:mtext>by</m:mtext>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <xsl:apply-templates select="*[5]"/>
- </m:mrow>
- </m:mtd>
- </m:mtr>
+ <xsl:variable name="charlength1">
+ <xsl:apply-templates select="*[3]" mode="root_charcount"/>
+ </xsl:variable>
+ <xsl:variable name="charlength2">
+ <xsl:apply-templates select="*[4]" mode="root_charcount"/>
+ </xsl:variable>
+ <xsl:variable name="charlength3">
+ <xsl:apply-templates select="*[5]" mode="root_charcount"/>
+ </xsl:variable>
+ <xsl:variable name="split1"
+ select="($charlength1 + $charlength2) >= $framewidth"/>
+ <xsl:variable name="split2"
+ select="($charlength2 + $charlength3) >= $framewidth"/>
+ <xsl:choose>
+ <xsl:when test="$split1">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>Rewrite</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[3]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <xsl:choose>
+ <xsl:when test="$split2">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>with</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[4]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>by</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[5]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>with</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[4]"/>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtext>by</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[5]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="$split2">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>Rewrite</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[3]"/>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtext>with</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[4]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>by</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[5]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>Rewrite</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[3]"/>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtext>with</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[4]"/>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtext>by</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[5]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:otherwise>
+ </xsl:choose>
</m:mtable>
</xsl:when>
<!-- not existing any more
@@ -1966,7 +2145,7 @@ which generates the toplevel element (see for instance xlink) -->
<xsl:apply-templates select="*[3]"/>
</xsl:when>
<!-- interp -->
- <xsl:when test="$name='forgetful'">
+ <xsl:when test="$name='interp'">
<m:mfenced open="[" close="]">
<xsl:if test="$id != ''">
<xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
@@ -1977,7 +2156,7 @@ which generates the toplevel element (see for instance xlink) -->
<!-- ERROR -->
<xsl:otherwise>
- <m:mi>ERROR</m:mi>
+ <m:mi>ERROR("<xsl:value-of select="$name"/>")</m:mi>
</xsl:otherwise>
</xsl:choose>
</m:mrow>
@@ -2086,6 +2265,24 @@ which generates the toplevel element (see for instance xlink) -->
<!-- COUNTING -->
<!--**********************-->
+<!-- enter this counting mode selecting the root -->
+<xsl:template match="*" mode="root_charcount">
+<xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+ <xsl:when test="count(*)=0">
+ <xsl:value-of select="0"/>
+ </xsl:when>
+ <xsl:when test="name()='m:ci'">
+ <xsl:value-of select="string-length()"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="*[1]" mode="charcount">
+ <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
+ </xsl:apply-templates>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
<xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
|m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
|m:plus|m:minus|m:times" mode="charcount">
@@ -2113,14 +2310,24 @@ which generates the toplevel element (see for instance xlink) -->
</xsl:template>
<xsl:template match="m:ci|m:csymbol" mode="charcount">
-<xsl:param name="incurrent_length" select="0"/>
-<xsl:param name="nosibling" select="0"/>
+ <xsl:param name="incurrent_length" select="0"/>
+ <xsl:param name="nosibling" select="0"/>
+ <xsl:variable name="mylength">
+ <xsl:choose>
+ <!-- special notation -->
+ <xsl:when test="text()='append'">3</xsl:when>
+ <!-- no notation -->
+ <xsl:otherwise>
+ <xsl:value-of select="string-length()"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
<xsl:choose>
- <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
- <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
+ <xsl:when test="$framewidth > ($incurrent_length + $mylength) and ($nosibling = 0)">
+ <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + $mylength"/></xsl:apply-templates></xsl:variable>
<xsl:choose>
<xsl:when test="string($siblength) = """>
- <xsl:value-of select="$incurrent_length + string-length()"/>
+ <xsl:value-of select="$incurrent_length + $mylength"/>
</xsl:when>
<xsl:otherwise>
<xsl:value-of select="number($siblength)"/>
@@ -2128,7 +2335,7 @@ which generates the toplevel element (see for instance xlink) -->
</xsl:choose>
</xsl:when>
<xsl:otherwise>
- <xsl:value-of select="$incurrent_length + string-length()"/>
+ <xsl:value-of select="$incurrent_length + $mylength"/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl
index 5cf944e72..7081ad83f 100644
--- a/helm/style/mmlnotation.xsl
+++ b/helm/style/mmlnotation.xsl
@@ -139,26 +139,24 @@
<m:mtd>
<m:mrow>
<m:mo stretchy="false">(</m:mo>
- <xsl:apply-templates select="*[position()=2]"/>
+ <xsl:apply-templates select="*[2]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+ <m:mo>
+ <xsl:if test="*[1]/@id">
+ <xsl:attribute name="xref">
+ <xsl:value-of select="*[1]/@id"/>
+ </xsl:attribute>
+ </xsl:if><xsl:value-of select="$symbol"/></m:mo>
+ <xsl:apply-templates select="*[3]"/>
</m:mrow>
</m:mtd>
</m:mtr>
- <xsl:for-each select = "*[position()>2]">
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
- <m:mo>
- <xsl:if test="*[1]/@id">
- <xsl:attribute name="xref">
- <xsl:value-of select="*[1]/@id"/>
- </xsl:attribute>
- </xsl:if><xsl:value-of select="$symbol"/></m:mo>
- <xsl:apply-templates select="."/>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </xsl:for-each>
<m:mtr>
<m:mtd>
<m:mrow>
@@ -396,4 +394,4 @@
</xsl:template>
-</xsl:stylesheet>
\ No newline at end of file
+</xsl:stylesheet>
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index ceb7a22ba..5b243e783 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -52,6 +52,51 @@
<xsl:apply-templates select="*[1]"/>
</xsl:template>
+
+<!-- FUNZIONI AUSILIARIE -->
+
+<xsl:template name="name_of_uri_bis">
+ <xsl:param name="uri" select=""""/>
+ <xsl:variable name="suffix" select="substring-after($uri, "/")"/>
+ <xsl:choose>
+ <xsl:when test="$suffix = """>
+ <xsl:value-of select="substring-before($uri,".var")"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="name_of_uri_bis">
+ <xsl:with-param name="uri" select="$suffix"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="var_name">
+ <xsl:param name="uri"/>
+ <xsl:param name="string" select=""""/>
+ <xsl:variable name="prefix0" select="substring-before($uri, " ")"/>
+ <xsl:variable name="suffix" select="substring-after($uri, " ")"/>
+ <xsl:variable name="prefix">
+ <xsl:call-template name="name_of_uri_bis">
+ <xsl:with-param name="uri" select="$prefix0"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <!--xsl:if test="string($prefix) != " " "-->
+ <xsl:variable name="string1" select="concat($string,', ', $prefix)"/>
+ <!--/xsl:if-->
+ <xsl:choose>
+ <xsl:when test="$suffix = """>
+ <xsl:value-of select="substring-after(concat($string1, ' '),',')"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="$suffix"/>
+ <xsl:with-param name="string" select="$string1"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
<!-- CIC OBJECTS -->
<xsl:template match="Sequent"> <!-- For Sequents there are no annotations -->
@@ -73,11 +118,15 @@
</Sequent>
</xsl:template>
-<xsl:template match="Definition" mode="noannot">
+<xsl:template match="ConstantType" mode="noannot">
+ <xsl:variable name="ConstantBodyUrl"
+ select="concat($BaseCICURI,'.body')"/>
<Definition name="{@name}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
- <xsl:value-of select="@params"/>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
</Params>
</xsl:if>
<!-- <xsl:choose>
@@ -93,29 +142,35 @@
</xsl:otherwise>
</xsl:choose> -->
<body>
- <xsl:apply-templates select="body/*[1]"/>
+ <m:ci definitionURL="{$ConstantBodyUrl}">click here</m:ci>
</body>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]"/>
</type>
</Definition>
</xsl:template>
-<xsl:template match="Axiom" mode="noannot">
- <Axiom name="{@name}" helm:xref="{@id}">
+<xsl:template match="ConstantBody" mode= "noannot">
+ <Definition name="{@for}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
- <xsl:value-of select="@params"/>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
</Params>
</xsl:if>
+ <body>
+ <xsl:apply-templates select="./*[1]"/>
+ </body>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
</type>
- </Axiom>
+ </Definition>
</xsl:template>
+
<xsl:template match="CurrentProof" mode="noannot">
- <CurrentProof name="{@name}" helm:xref="{@id}">
+ <CurrentProof name="{@of}" helm:xref="{@id}">
<xsl:for-each select="Conjecture">
<Conjecture no="{@no}" helm:xref="{@id}">
<xsl:for-each select="*">
@@ -133,7 +188,7 @@
<xsl:apply-templates select="body/*[1]"/>
</body>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
</type>
</CurrentProof>
</xsl:template>
diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl
index 7d890d611..5bad7e108 100644
--- a/helm/style/objtheorycontent.xsl
+++ b/helm/style/objtheorycontent.xsl
@@ -43,42 +43,42 @@
<!-- CIC DEFINITION -->
-<xsl:template match="Definition">
- <xsl:choose>
+<xsl:template match="ConstantType">
+ <xsl:choose>
<xsl:when test="$type='typeonly'">
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]" mode="noannot"/>
</type>
</xsl:when>
<xsl:otherwise>
<Definition name="{@name}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
- <xsl:value-of select="@params"/>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
</Params>
</xsl:if>
- <body>
- <xsl:apply-templates select="body/*[1]"/>
- </body>
+ <body/>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]" mode="noannot"/>
</type>
</Definition>
</xsl:otherwise>
- </xsl:choose>
+ </xsl:choose>
</xsl:template>
<xsl:template match="Axiom|CurrentProof|InductiveDefinition|Variable">
<xsl:apply-templates select="." mode="noannot"/>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate">
<m:math>
<xsl:apply-templates select="." mode="noannot"/>
</m:math>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate" mode="noannot">
<xsl:apply-templates select="." mode="pure"/>
</xsl:template>
diff --git a/helm/style/params.xsl b/helm/style/params.xsl
index d703bfe06..1b5f41670 100644
--- a/helm/style/params.xsl
+++ b/helm/style/params.xsl
@@ -39,16 +39,18 @@
<!-- CSC: PROBLEMA: URI CHE NON CONTENGONO / ED INIZIANO CON cic: -->
<xsl:template name="name_of_uri">
<xsl:param name="uri" select=""""/>
+ <xsl:param name="extension" select="'.con'"/>
<xsl:variable name="suffix" select="substring-after($uri, "/")"/>
<xsl:choose>
<xsl:when test="$suffix = """>
<!-- CSC: PROBLEMA: .con PUO' APPARIRE ALL'INTERNO DELLE URI ===>
SCRIVERE UNA FUNZIONE RICORSIVA CHE RISOLVA -->
- <xsl:value-of select="substring-before($uri,".con")"/>
+ <xsl:value-of select="substring-before($uri,$extension)"/>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="name_of_uri">
<xsl:with-param name="uri" select="$suffix"/>
+ <xsl:with-param name="extension" select="$extension"/>
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
@@ -98,6 +100,25 @@
</xsl:choose>
</xsl:template>
+<!-- path gives the path of a uri, up to the final name -->
+<xsl:template name="path">
+ <xsl:param name="uri" select=""""/>
+ <xsl:param name="current_path" select=""""/>
+ <xsl:choose>
+ <xsl:when test="(substring-after($uri,"/") != "")">
+ <xsl:call-template name="path">
+ <xsl:with-param
+ name="uri" select="substring-after($uri,"/")"/>
+ <xsl:with-param
+ name="current_path" select="concat($current_path,substring-before($uri,"/"),'/')"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$current_path"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
<xsl:template name="blank_counting">
<xsl:param name="string" select=""""/>
<xsl:param name="counter" select="0"/>
@@ -163,14 +184,11 @@
</xsl:call-template>
</xsl:variable>
<xsl:choose>
- <xsl:when test="$offset > 0">
- <xsl:variable name="params">
- <xsl:variable name="second_url">
- <xsl:call-template name="URLofURI4getter">
- <xsl:with-param name="uri" select="$second_uri"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:value-of select="document($second_url)/*/@params"/>
+ <xsl:when test="$offset > 0">
+ <xsl:variable name="params">
+ <xsl:variable name="second_url"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$second_uri"/></xsl:call-template></xsl:variable>
+ <xsl:value-of
+ select="document($second_url)/*/@params"/>
</xsl:variable>
<xsl:variable name="minimum">
<xsl:call-template name="min">
@@ -179,7 +197,9 @@
</xsl:call-template>
</xsl:variable>
<xsl:choose>
- <xsl:when test="0 > $minimum">0</xsl:when>
+ <xsl:when test="0 > $minimum">
+ 0
+ </xsl:when>
<xsl:otherwise>
<xsl:variable name="relevant_params">
<!-- the blank after : in the next line is essential -->
@@ -198,11 +218,13 @@
<xsl:with-param name="counter" select="0"/>
</xsl:call-template>
</xsl:variable>
- <xsl:value-of select="number($tokens - $separators)"/>
+ <xsl:value-of select="$tokens - $separators"/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
- <xsl:otherwise>0</xsl:otherwise>
+ <xsl:otherwise>
+ 0
+ </xsl:otherwise>
</xsl:choose>
</xsl:template>
@@ -275,25 +297,59 @@
<xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)="CAST"))">
<xsl:choose>
<xsl:when test="name(.) = string($binder)">
- <xsl:if test="$target = 0">
- <xsl:choose>
- <xsl:when test="string($binder) = "LAMBDA"">
- <m:ci>
- <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
- </m:ci>
+ <xsl:choose>
+ <xsl:when test="$noparams >= count(decl)">
+ <xsl:for-each select="decl">
+ <xsl:if test="$target = 0">
+ <xsl:choose>
+ <xsl:when test="string($binder) = "LAMBDA"">
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ </xsl:when>
+ <xsl:otherwise>
+ <Param name="{@binder}">
+ <xsl:apply-templates select="*[1]"/>
+ </Param>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:if>
+ </xsl:for-each>
+ <xsl:apply-templates select="target/*[1]" mode="abstparams">
+ <xsl:with-param name="noparams" select="$noparams - count(decl)"/>
+ <xsl:with-param name="target" select="$target"/>
+ <xsl:with-param name="binder" select="$binder"/>
+ </xsl:apply-templates>
</xsl:when>
- <xsl:otherwise>
- <Param name="{target/@binder}">
- <xsl:apply-templates select="source"/>
- </Param>
+ <xsl:otherwise>
+ <xsl:for-each select="decl[$noparams >= position()]">
+ <xsl:if test="$target = 0">
+ <xsl:choose>
+ <xsl:when test="string($binder) = "LAMBDA"">
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ </xsl:when>
+ <xsl:otherwise>
+ <Param name="{@binder}">
+ <xsl:apply-templates select="*[1]"/>
+ </Param>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:if>
+ </xsl:for-each>
+ <xsl:if test="$target = 1">
+ <xsl:choose>
+ <xsl:when test="name(.)="PROD"">
+ <xsl:apply-templates select="decl[position()=$noparams+1]" mode="prod"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="decl[position()=$noparams+1]" mode="lambda_prop"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:if>
</xsl:otherwise>
- </xsl:choose>
- </xsl:if>
- <xsl:apply-templates select="target/*[1]" mode="abstparams">
- <xsl:with-param name="noparams" select="$noparams - 1"/>
- <xsl:with-param name="target" select="$target"/>
- <xsl:with-param name="binder" select="$binder"/>
- </xsl:apply-templates>
+ </xsl:choose>
</xsl:when>
<xsl:otherwise>
<xsl:apply-templates select="term/*[1]" mode="abstparams">
@@ -356,7 +412,7 @@
<xsl:when test="name(.) = "PROD"">
<xsl:apply-templates select="target/*[1]" mode="counting">
<xsl:with-param name="noparams" select="$noparams"/>
- <xsl:with-param name="count" select="$count + 1"/>
+ <xsl:with-param name="count" select="$count + count(decl)"/>
</xsl:apply-templates>
</xsl:when>
<xsl:when test="name(.) = "CAST"">
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index f61cbe6d9..dbcfabaa3 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -34,15 +34,19 @@
xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
+<xsl:include href="logic.xsl"/>
+<xsl:include href="inductive.xsl"/>
+<xsl:include href="rewrite.xsl"/>
+<xsl:include href="diseq.xsl"/>
+
<!-- ************************* LOGIC *********************************-->
<!-- Proof objects -->
-<!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
<xsl:key name="typeid" use="@of" match="TYPE"/>
-<!-- ALL this elements does not have inner type -->
-<xsl:template match="PROD|SORT|MUTIND" mode="noannot">
+<!-- These elements do not have inner type -->
+<xsl:template match="PROD|SORT|MUTIND|instantiate" mode="noannot">
<xsl:apply-templates select="." mode="pure"/>
</xsl:template>
@@ -59,10 +63,10 @@
</xsl:variable>
<xsl:choose>
<xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
+ <!--xsl:when test="@sort='Prop'"-->
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
<xsl:apply-templates mode="proof_transform" select="."/>
- <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
<xsl:for-each select="$InnerTypes">
<xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
</xsl:for-each>
@@ -76,8 +80,19 @@
<!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
-<!-- LAMBDA has inner type only if it is not nested inside another lambda -->
<xsl:template match="LAMBDA" mode="noannot">
+ <xsl:choose>
+ <xsl:when test="@sort='Prop'">
+ <xsl:apply-templates select="*[1]" mode="lambda_prop"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- mode lambda is defined in content.xsl -->
+ <xsl:apply-templates select="*[1]" mode="lambda"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="decl" mode="lambda_prop">
<xsl:variable name="id" select="@id"/>
<xsl:variable name="innertype_available">
<xsl:for-each select="$InnerTypes">
@@ -87,30 +102,114 @@
</xsl:for-each>
</xsl:variable>
<xsl:choose>
- <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
+ <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
- <xsl:apply-templates mode="proof_transform" select="."/>
+ <m:lambda helm:xref="{@id}">
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
+ </m:lambda>
<xsl:for-each select="$InnerTypes">
<xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
</xsl:for-each>
</m:apply>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates select="." mode="pure"/>
+ <m:lambda helm:xref="{@id}">
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
+ </m:lambda>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="target" mode="lambda_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+<!-- LETIN -->
+
+<xsl:template match="LETIN" mode="noannot">
+ <xsl:choose>
+ <xsl:when test="@sort='Prop'">
+ <xsl:apply-templates select="*[1]" mode="letin_prop"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <!-- mode letin is defined in content.xsl -->
+ <xsl:apply-templates select="*[1]" mode="letin_pure"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="def" mode="letin_prop">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+ <xsl:for-each select="$InnerTypes">
+ <xsl:if test="key('typeid',$id)/*">
+ <xsl:text>yes</xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>proof</m:csymbol>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>let_in</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ </m:bvar>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
+ </m:apply>
+ <xsl:for-each select="$InnerTypes">
+ <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
+ </xsl:for-each>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>let_in</m:csymbol>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ </m:bvar>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
+ </m:apply>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
+<xsl:template match="target" mode="letin_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
<!-- ALL these elements have inner type -->
-<xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
<xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
<xsl:apply-templates mode="proof_transform" select="."/>
- <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
<xsl:for-each select="$InnerTypes">
<xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
</xsl:for-each>
@@ -132,588 +231,32 @@
</xsl:choose>
</xsl:template>
-<!-- si presuppone che il tipo induttivo non sia mutuamente
- induttivo. Bisognerebbe andare a vedere l'ultimo parametro
- del presunto "principio di induzione", tirare fuori il tipo induttivo
- e vedere se il suo nome coincide con il prefisso di _ind.
- Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
- parametro di nat_double_ind e' di tipo nat, e nat e' diverso
- da nat_double. Per ora, verifico solo l'esistenza di nat_double,
- ma questo, benche' non porti ad errore, non copre tutti i
- casi per quelli mutuamente induttivi -->
-
-<xsl:template mode="try_inductive" match="APPLY">
- <xsl:variable name="id" select="@id"/>
- <xsl:choose>
- <xsl:when test="CONST[1]">
- <xsl:variable name="uri" select="CONST[1]/@uri"/>
- <xsl:choose>
- <xsl:when test="contains($uri,'_ind.con')">
- <xsl:variable name="ind_uri"
- select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
- <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
- <xsl:variable name="inductive_def"
- select="document($InductiveTypeUrl)/InductiveDefinition"/>
- <!-- check if the corresponding inductive definition actually
- exists -->
- <xsl:choose>
- <xsl:when test="$inductive_def">
- <xsl:variable name="ind_name">
- <xsl:call-template name="get_name">
- <xsl:with-param name="uri" select="$uri"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:variable name="no_params">
- <xsl:call-template name="get_no_params">
- <xsl:with-param name="first_uri" select="$CICURI"/>
- <xsl:with-param name="second_uri" select="$uri"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:apply-templates mode="inductive" select=".">
- <xsl:with-param name="inductive_def_uri"
- select="$ind_uri"/>
- <xsl:with-param name="inductive_def"
- select="$inductive_def"/>
- <xsl:with-param name="section_params" select="$no_params"/>
- <xsl:with-param name="inductive_def_index" select="1"/>
- <xsl:with-param name="inductive_def_name" select="$ind_name"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="letin" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="letin" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="letin" select="."/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template mode="eq_transitive" match="*">
- <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
- <xsl:choose>
- <xsl:when test="name()='APPLY'">
- <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
- <xsl:variable name="id" select="@id"/>
- <xsl:choose>
- <!-- ricordarsi di trattare il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
- <!-- <m:ci>eccomi-3</m:ci> -->
- <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template mode="diseq" match="*">
- <xsl:param name="rel" select="'eq'"/>
- <xsl:choose>
- <xsl:when test="name()='APPLY'">
- <xsl:variable name="id" select="@id"/>
- <xsl:choose>
- <!-- ricordarsi di trattare il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- </xsl:when>
- <!--
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
- <xsl:apply-templates mode="diseq" select="*[6]"/>
- <m:eq/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <m:eq/>
- <xsl:apply-templates mode="diseq" select="*[7]"/>
- </xsl:when>
- -->
- <xsl:otherwise>
- <xsl:element name="{concat('m:',$rel)}"/>
- <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:element name="{concat('m:',$rel)}"/>
- <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="."/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
<xsl:template mode="proof_transform" match="*">
<xsl:choose>
<xsl:when test="name()='APPLY'">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
- <!-- Algebra equality (eq_transitive_unfolded) -->
- <!-- It requires a special mode "eq_transitive"-->
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>eq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <!-- Algebra disequalities -->
- <!-- It requires a special mode "diseq"-->
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'leq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- <xsl:apply-templates mode="diseq" select="*[7]">
- <xsl:with-param name="rel" select="'eq'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <!-- togliere il parametro -->
- <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>diseq_chain</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <m:eq/>
- <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- <xsl:with-param name="show_statement" select="0"/>
- </xsl:call-template>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="diseq" select="*[6]">
- <xsl:with-param name="rel" select="'lt'"/>
- </xsl:apply-templates>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- </m:apply>
- </xsl:when>
- <!-- EQUALITY -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
- </m:apply>
- </xsl:when>
- <!-- EQUALITY with extra-parameters -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
- <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
- <xsl:choose>
- <xsl:when test="$no_extraproofs=0">
- <m:apply>
- <m:csymbol>rewrite_and_apply</m:csymbol>
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
- </m:apply>
- <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <xsl:choose>
- <xsl:when test="*[5]/@sort='Prop'">
- <m:apply helm:xref="{@id}">
- <m:csymbol>letin</m:csymbol>
- <m:apply>
- <m:csymbol>let</m:csymbol>
- <m:ci>
- <xsl:call-template name="insert_subscript">
- <xsl:with-param name="node_value" select="'h1'"/>
- </xsl:call-template>
- </m:ci>
- <xsl:apply-templates mode="noannot" select="*[5]"/>
- </m:apply>
- <xsl:call-template name="gen_let">
- <xsl:with-param name="init_pos" select="1"/>
- <xsl:with-param name="from" select="7"/>
- </xsl:call-template>
- <m:apply>
- <m:csymbol>rewrite_and_apply</m:csymbol>
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <m:ci>
- <xsl:call-template name="insert_subscript">
- <xsl:with-param name="node_value" select="'h1'"/>
- </xsl:call-template>
- </m:ci>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
- </m:apply>
- <xsl:apply-templates mode="flat" select="*[8]">
- <xsl:with-param name="n">
- <xsl:value-of select="2"/>
- </xsl:with-param>
- </xsl:apply-templates>
- </m:apply>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply helm:xref="{@id}">
- <m:csymbol>letin</m:csymbol>
- <xsl:call-template name="gen_let">
- <xsl:with-param name="init_pos" select="0"/>
- <xsl:with-param name="form" select="7"/>
- </xsl:call-template>
- <m:apply>
- <m:csymbol>rewrite_and_apply</m:csymbol>
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="pure" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[3]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
- </m:apply>
- <xsl:apply-templates mode="flat" select="*[8]">
- <xsl:with-param name="n">
- <xsl:value-of select="1"/>
- </xsl:with-param>
- </xsl:apply-templates>
- </m:apply>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- False_ind -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
- count(child::*) = 3">
- <m:apply helm:xref="{@id}">
- <m:csymbol>false_ind</m:csymbol>
- <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- </m:apply>
- </xsl:when>
- <!-- gestire meglio il caso di and_ind quando la prova
- non e' della forma \x.\y.M -->
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
- and count(child::*) = 6
- and name(*[5])='LAMBDA'
- and name(*[5]/target/*[1])='LAMBDA'">
- <m:apply helm:xref="{@id}">
- <m:csymbol>and_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[6]"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
- <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
- and count(child::*) = 7">
- <xsl:choose>
- <xsl:when test="name(*[5])='LAMBDA'
- and name(*[6])='LAMBDA'">
- <xsl:variable name="definition_url"
- select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
- <m:apply helm:xref="{@id}">
- <m:csymbol>full_or_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[7]"/>
- <xsl:for-each select="$InnerTypes">
- <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
- </xsl:for-each>
- <m:apply>
- <m:csymbol>left_case</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:value-of select="*[5]/target/@binder"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
- </m:apply>
- <m:apply>
- <m:csymbol>right_case</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
- </m:apply>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply helm:xref="{@id}">
- <m:csymbol>or_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[7]"/>
- <xsl:for-each select="$InnerTypes">
- <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
- </xsl:for-each>
- <xsl:apply-templates mode="pure" select="*[5]"/>
- <xsl:apply-templates mode="pure" select="*[6]"/>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <!-- ex_ind, exT_ind -->
- <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
- CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
- and count(child::*) = 6
- and name(*[5])='LAMBDA'
- and name(*[5]/target/*[1])='LAMBDA'">
- <m:apply helm:xref="{@id}">
- <m:csymbol>ex_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[6]"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
- <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
- <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
- <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
- </m:apply>
- </xsl:when>
- <xsl:when test="name(*[1])='CONST'">
+ <xsl:when test="name(*[1])='CONST' or
+ (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
<xsl:apply-templates mode="try_inductive" select="."/>
</xsl:when>
<!-- patch temporanea per la gestione di redex -->
- <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
- and *[2]/@sort='Prop'">
+ <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2">
+ <!-- old
+ and *[2]/@sort='Prop'"> -->
<m:apply helm:xref="{@id}">
- <m:csymbol>letin</m:csymbol>
- <m:apply>
- <m:csymbol>let</m:csymbol>
+ <m:csymbol>let_in</m:csymbol>
+ <m:bvar>
<m:ci>
<xsl:call-template name="insert_subscript">
<xsl:with-param name="node_value">
- <xsl:value-of select="*[1]/target/@binder"/>
+ <xsl:value-of select="*[1]/*[1]/@binder"/>
</xsl:with-param>
</xsl:call-template>
</m:ci>
- <xsl:apply-templates mode="noannot" select="*[2]"/>
- </m:apply>
- <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
+ </m:bvar>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
+ <xsl:apply-templates mode="lambda_prop" select="*[1]/*[2]"/>
</m:apply>
</xsl:when>
<xsl:otherwise>
@@ -721,32 +264,6 @@
</xsl:otherwise>
</xsl:choose>
</xsl:when>
- <xsl:when test="name()='LAMBDA'">
- <xsl:choose>
- <xsl:when test="(name(target/*[1])='APPLY' and
- name(target/*[1]/*[1])='CONST' and
- (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
- and count(target/*[1]/*) = 8
- and name(target/*[1]/*[8])='REL'
- and target/@binder = target/*[1]/*[8]/@binder )">
- <m:apply>
- <m:csymbol>rw_step</m:csymbol>
- <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
- <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
- <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
- <xsl:call-template name="generate_side_proof">
- <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
- </xsl:call-template>
- <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates mode="pure" select="."/>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
<xsl:otherwise>
<xsl:apply-templates select="." mode="pure"/>
</xsl:otherwise>
@@ -876,6 +393,49 @@
</xsl:choose>
</xsl:template>
+<xsl:template name="gen_let">
+ <xsl:param name="init_pos" select="1"/>
+ <xsl:param name="from" select="0"/>
+ <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
+ <xsl:with-param name="init_pos" select="$init_pos"/>
+ </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template mode="gen_let_aux" match="*">
+ <xsl:param name="init_pos" select="1"/>
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+ <xsl:for-each select="$InnerTypes">
+ <xsl:if test="key('typeid',$id)/*">
+ <xsl:text>yes</xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ </xsl:variable>
+ <xsl:choose>
+ <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>
+ <xsl:apply-templates mode="noannot" select="."/>
+ </m:apply>
+ <xsl:if test="following-sibling::*[1]">
+ <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
+ <xsl:with-param name="init_pos" select="$init_pos+1"/>
+ </xsl:apply-templates>
+ </xsl:if>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:if test="following-sibling::*[1]">
+ <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
+ <xsl:with-param name="init_pos" select="$init_pos"/>
+ </xsl:apply-templates>
+ </xsl:if>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
+
<xsl:template name="gen_let">
<xsl:param name="init_pos" select="0"/>
<xsl:param name="from" select="0"/>
@@ -896,11 +456,12 @@
</m:apply>
</xsl:if>
</xsl:for-each>
-</xsl:template>
+</xsl:template> -->
<xsl:template match="*" mode="erase">
<xsl:choose>
- <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:when test="@sort='Prop'
+ or name()='instantiate' or $naturalLanguage='no'">
<xsl:apply-templates mode="pure" select="."/>
</xsl:when>
<xsl:otherwise>
@@ -926,7 +487,8 @@
<xsl:otherwise>
<!-- forse bisognerebbe trattare solo l'elemento di testa -->
<xsl:choose>
- <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:when test="@sort='Prop'
+ or name()='instantiate' or $naturalLanguage='no'">
<xsl:apply-templates mode="pure" select="."/>
</xsl:when>
<xsl:otherwise>
@@ -960,7 +522,7 @@
</xsl:when>
<xsl:otherwise>
<xsl:choose>
- <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
+ <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
<xsl:apply-templates mode="pure" select="."/>
</xsl:when>
<xsl:otherwise>
@@ -993,27 +555,5 @@
</xsl:choose>
</xsl:template>
-<!-- <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
- <xsl:choose>
- <xsl:when test="count(child::*) > 4">
- <m:apply helm:xref="{@id}">
- <m:csymbol>app</m:csymbol>
- <xsl:apply-templates mode="pure" select="*[1]"/>
- <m:ci>*</m:ci>
- <m:ci>*</m:ci>
- <m:ci>*</m:ci>
- <xsl:apply-templates mode="flat" select="*[5]"/>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply helm:xref="{@id}">
- <m:csymbol>app</m:csymbol>
- <xsl:apply-templates mode="flat" select="*[1]"/>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template> -->
-
</xsl:stylesheet>
diff --git a/helm/style/rewrite.xsl b/helm/style/rewrite.xsl
new file mode 100644
index 000000000..e361944d3
--- /dev/null
+++ b/helm/style/rewrite.xsl
@@ -0,0 +1,135 @@
+<!-- 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/. -->
+
+<!--******************************************************************-->
+<!-- Basic Logic -->
+<!-- (completely) Revisited: february 2001, 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 mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7]">
+ <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
+ <xsl:choose>
+ <xsl:when test="$no_extraproofs=0">
+ <m:apply>
+ <m:csymbol>rewrite_and_apply</m:csymbol>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+ <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:choose>
+ <xsl:when test="*[5]/@sort='Prop'">
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>letin</m:csymbol>
+ <m:apply>
+ <m:csymbol>let</m:csymbol>
+ <m:ci>
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value" select="'h1'"/>
+ </xsl:call-template>
+ </m:ci>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ <xsl:call-template name="gen_let">
+ <xsl:with-param name="init_pos" select="1"/>
+ <xsl:with-param name="from" select="7"/>
+ </xsl:call-template>
+ <m:apply>
+ <m:csymbol>rewrite_and_apply</m:csymbol>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <m:ci>
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value" select="'h1'"/>
+ </xsl:call-template>
+ </m:ci>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+ <xsl:apply-templates mode="flat" select="*[8]">
+ <xsl:with-param name="n">
+ <xsl:value-of select="2"/>
+ </xsl:with-param>
+ </xsl:apply-templates>
+ </m:apply>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>letin</m:csymbol>
+ <xsl:call-template name="gen_let">
+ <xsl:with-param name="init_pos" select="0"/>
+ <xsl:with-param name="form" select="7"/>
+ </xsl:call-template>
+ <m:apply>
+ <m:csymbol>rewrite_and_apply</m:csymbol>
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="pure" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[3]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ </xsl:call-template>
+ </m:apply>
+ <xsl:apply-templates mode="flat" select="*[8]">
+ <xsl:with-param name="n">
+ <xsl:value-of select="1"/>
+ </xsl:with-param>
+ </xsl:apply-templates>
+ </m:apply>
+ </m:apply>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+</xsl:stylesheet>
\ No newline at end of file
diff --git a/helm/style/ring.xsl b/helm/style/ring.xsl
index d57723ea8..5136e77d5 100644
--- a/helm/style/ring.xsl
+++ b/helm/style/ring.xsl
@@ -4,12 +4,12 @@
xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con']" mode="pure">
+<xsl:template match="APPLY[CONST[@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con']] | APPLY[instantiate/CONST[@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con']]" mode="proof_transform">
<xsl:choose>
- <xsl:when test="count(child::*) > 1">
+ <xsl:when test="count(child::*) = 2">
<m:apply helm:xref="{@id}">
<m:csymbol>app</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[1]"/>
+ <xsl:apply-templates mode="noannot" select="*[1]/*[1]"/>
<m:ci>...</m:ci>
</m:apply>
</xsl:when>
@@ -19,12 +19,12 @@
</xsl:choose>
</xsl:template>
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con']" mode="pure">
+<xsl:template match="APPLY[instantiate/CONST[@uri='cic:/Coq/ring/Ring_abstract/interp_ap.con']] | APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_ap.con']" mode="pure">
<xsl:choose>
- <xsl:when test="count(child::*) = 9">
+ <xsl:when test="count(child::*) = 2">
<xsl:call-template name="start-interp">
- <xsl:with-param name="rtree" select="*[9]"/>
- <xsl:with-param name="atree" select="*[8]"/>
+ <xsl:with-param name="rtree" select="*[2]"/>
+ <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
@@ -33,16 +33,15 @@
</xsl:choose>
</xsl:template>
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con']" mode="pure">
+<xsl:template match="APPLY[instantiate/CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_sacs.con'] | APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_sacs.con']" mode="pure">
<xsl:choose>
- <xsl:when test="count(child::*) = 9 and *[APPLY and position()=9]
- [CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con']">
+ <xsl:when test="count(child::*) = 2 and *[APPLY and position()=2][CONST/@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con']">
<m:apply helm:xref="{@id}">
<m:csymbol>app</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[9]/*[1]"/>
+ <xsl:apply-templates mode="noannot" select="*[2]/*[1]"/>
<xsl:call-template name="start-interp">
- <xsl:with-param name="rtree" select="*[9]/*[2]"/>
- <xsl:with-param name="atree" select="*[8]"/>
+ <xsl:with-param name="rtree" select="*[2]/*[2]"/>
+ <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
</xsl:call-template>
</m:apply>
</xsl:when>
@@ -54,28 +53,34 @@
<!-- ************************** abstract polinomials rendering ************************ -->
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
- and @noConstr='1']]" mode="interp">
+<xsl:template match="*" mode="interp">
+ <m:apply>
+ <m:ci>ERROR INTERP:</m:ci>
+ <xsl:apply-templates select="." mode="noannot"/>
+ </m:apply>
+</xsl:template>
+
+<!-- APVar -->
+<!-- CSC: ??????????? -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='1']]" mode="interp">
<xsl:param name="atree"/>
<xsl:apply-templates select="*[2]" mode="interp">
<xsl:with-param name="atree" select="$atree"/>
</xsl:apply-templates>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
- and @noConstr='2']]" mode="interp">
- <xsl:param name="atree"/>
- <xsl:apply-templates mode="noannot" select="."/>
+<!-- AP0 -->
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='2']" mode="interp">
+ <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
- and @noConstr='3']]" mode="interp">
- <xsl:param name="atree"/>
- <xsl:apply-templates mode="noannot" select="."/>
+<!-- AP1 -->
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='3']" mode="interp">
+ <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
- and @noConstr='4']]" mode="interp">
+<!-- APplus -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='4']]" mode="interp">
<xsl:param name="atree"/>
<xsl:call-template name="mk-mml-op-interp">
<xsl:with-param name="arity" select="2"/>
@@ -85,8 +90,8 @@
</xsl:call-template>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
- and @noConstr='5']]" mode="interp">
+<!-- APmult -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='5']]" mode="interp">
<xsl:param name="atree"/>
<xsl:call-template name="mk-mml-op-interp">
<xsl:with-param name="arity" select="2"/>
@@ -96,8 +101,8 @@
</xsl:call-template>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind'
- and @noConstr='6']]" mode="interp">
+<!-- APopp -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='6']]" mode="interp">
<xsl:param name="atree"/>
<xsl:call-template name="mk-mml-op-interp">
<xsl:with-param name="arity" select="1"/>
@@ -107,24 +112,21 @@
</xsl:call-template>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind'
- and @noConstr='1']]" mode="interp">
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='1']]" mode="interp">
<xsl:param name="atree"/>
<xsl:apply-templates select="*[2]" mode="interp">
<xsl:with-param name="atree" select="$atree/*[4]"/>
</xsl:apply-templates>
</xsl:template>
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind'
- and @noConstr='2']]" mode="interp">
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='2']]" mode="interp">
<xsl:param name="atree"/>
<xsl:apply-templates select="*[2]" mode="interp">
<xsl:with-param name="atree" select="$atree/*[5]"/>
</xsl:apply-templates>
</xsl:template>
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind'
- and @noConstr='3']" mode="interp">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='3']" mode="interp">
<xsl:param name="atree"/>
<xsl:apply-templates select="$atree/*[3]" mode="noannot"/>
</xsl:template>
diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt
index 2f31b969a..84cd46836 100644
--- a/helm/style/xslt_index.txt
+++ b/helm/style/xslt_index.txt
@@ -3,6 +3,7 @@ annotatedpres.xsl
content.xsl
content_to_html.xsl
contentlib.xsl
+diseq.xsl
drop_coercions.xsl
expandobj.xsl
genmmlid.xsl
@@ -12,9 +13,11 @@ html_init.xsl
html_reals.xsl
html_set.xsl
inductive.xsl
+ite.xsl
lambda.xsl
link.xsl
links_library.xsl
+logic.xsl
mk_dep_graph.xsl
mk_meta_and_dep_graph.xsl
mk_meta_graph.xsl
@@ -27,6 +30,7 @@ objcontent.xsl
objtheorycontent.xsl
params.xsl
proofs.xsl
+rewrite.xsl
ricerca.xsl
ring.xsl
rootcontent.xsl