<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:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
</m:apply>
</xsl:when>
</xsl:choose>
</xsl:template>
+<!-- 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:choose>
<xsl:variable name="uri" select="CONST[1]/@uri"/>
<xsl:choose>
<xsl:when test="contains($uri,'_ind.con')">
- <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="ind_uri"
select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
- <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="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:variable name="inductive_def"
+ select="document(concat(string($absPath),$ind_uri))/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:template mode="proof_transform" match="*">
+ <xsl:choose>
+ <xsl:when test="name()='APPLY'">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
<!-- NATIND 3 parametri -->
- <xsl:when test="name()='APPLY' and CONST[
- attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 4">
+ <xsl:when test="CONST[attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 4">
<m:apply>
<m:csymbol>nat_ind</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[3]"/>
</xsl:when>
<!-- NATIND 4 parametri (nuova versione) -->
<!--
- <xsl:when test="name()='APPLY' and CONST[
+ <xsl:when test="CONST[
attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con']
and count(child::*) = 5
and name(*[4])='LAMBDA'
</xsl:when>
-->
<!-- EQUALITY -->
- <xsl:when test="name()= 'APPLY' and CONST[
+ <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
<xsl:apply-templates mode="noannot" select="*[5]"/>
<xsl:apply-templates mode="pure" select="*[3]"/>
<xsl:apply-templates mode="pure" select="*[6]"/>
- <xsl:apply-templates mode="pure" select="*[7]"/>
+ <xsl:apply-templates mode="proof_transform" select="*[7]"/>
</m:apply>
</xsl:when>
<!-- EQUALITY with extra-parameters -->
- <xsl:when test="name()= 'APPLY' and CONST[
+ <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
</xsl:choose>
</xsl:when>
<!-- False_ind -->
- <xsl:when test="name()= 'APPLY' and CONST[
+ <xsl:when test="CONST[
attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
count(child::*) = 3">
<m:apply helm:xref="{@id}">
</xsl:when>
<!-- gestire meglio il caso di and_ind quando la prova
non e' della forma \x.\y.M -->
- <xsl:when test="name()= 'APPLY' and CONST[
+ <xsl:when test="CONST[
attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
and count(child::*) = 6
and name(*[5])='LAMBDA'
<xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
</m:apply>
</xsl:when>
- <xsl:when test="name()= 'APPLY' and CONST[
+ <xsl:when test="CONST[
attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
and count(child::*) = 7">
<xsl:choose>
</xsl:choose>
</xsl:when>
<!-- ex_ind, exT_ind -->
- <xsl:when test="name()= 'APPLY'
- and (CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
+ <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'
<xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
</m:apply>
</xsl:when>
- <xsl:when test="(name()='APPLY') and (name(*[1])='CONST')">
+ <xsl:when test="name(*[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'">
+ <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">
+ <xsl:value-of select="*[1]/target/@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:apply>
+ </xsl:when>
<xsl:otherwise>
- <xsl:choose>
- <xsl:when test="name()='APPLY'">
- <xsl:apply-templates select="." mode="letin"/>
- </xsl:when>
- <xsl:otherwise>
- <xsl:apply-templates select="." mode="pure"/>
- </xsl:otherwise>
- </xsl:choose>
+ <xsl:apply-templates select="." mode="letin"/>
</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: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>
+ </xsl:choose>
</xsl:template>
</m:apply>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates mode="pure" select="."/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop'">
+ <m:apply>
+ <m:csymbol>app</m:csymbol>
+ <xsl:apply-templates mode="erase" select="*[1]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
</xsl:for-each>
</xsl:template>
+<xsl:template match="*" mode="erase">
+ <xsl:choose>
+ <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:ci>.</m:ci>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
+</xsl:template>
+
<xsl:template match="*" mode="previous">
<xsl:choose>
<xsl:when test="$naturalLanguage='yes' and(@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX'))">
<m:ci>previous</m:ci>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates select="." mode="pure"/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop' or $naturalLanguage='no' ">
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:ci>.</m:ci>
+ </xsl:otherwise>
+ </xsl:choose>
+ <!-- <xsl:apply-templates select="." mode="pure"/> -->
</xsl:otherwise>
</xsl:choose>
<xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
</xsl:apply-templates>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates mode="pure" select="."/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:ci>.</m:ci>
+ </xsl:otherwise>
+ </xsl:choose>
+ <!-- <xsl:apply-templates mode="pure" select="."/> -->
<xsl:apply-templates mode="flat" select="following-sibling::*[1]">
<xsl:with-param name="n" select="$n"/>
</xsl:apply-templates>
projects / helm.git / blobdiff