* iff notation added (new csymbol)

* New notation for lists added (list.xml)

diff --git a/helm/meta_style/.cvsignore b/helm/meta_style/.cvsignore
index b88948804d28848817afc3dd935d27ab05fbb20c..b20cfb2817d1ffc6de11bd83cf39dbbea3ad3fda 100644 (file)
--- 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 847efdb319e8b8ebfa80d496141238852bef4611..f51cc8094f58e1f1a4fe384203a5c1a28e0b0e71 100644 (file)
--- a/helm/meta_style/Makefile
+++ b/helm/meta_style/Makefile
@@ -5,10 +5,10 @@ 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/basic.xml b/helm/meta_style/basic.xml
index 5eaefa3a8661637f08feffc68d06ed72edf34555..66419e9a35214ea5860d36b0899d558ff2933365 100644 (file)
--- a/helm/meta_style/basic.xml
+++ b/helm/meta_style/basic.xml
@@ -17,6 +17,17 @@
  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"

diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml
new file mode 100644 (file)
index 0000000..6e42d21
--- /dev/null
+++ b/helm/meta_style/list.xml
@@ -0,0 +1,55 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+<!-- ************************** LISTS ****************************** -->
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<import href="positive.xsl"/>
+
+<!-- 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"
+ 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  = "LENGTH"
+ uri   = "cic:/Coq/Lists/PolyList/length.con"
+ cook  = "true"
+ arity = "1"
+ m-tag = "card"/>
+
+</OpList>

diff --git a/helm/meta_style/xslt_index.txt b/helm/meta_style/xslt_index.txt
index 889ce4c6c3d98bfbb9c4d953c4586f8844f82065..2f683f28dbe472985df7fe64910b415a2d8f4c9a 100644 (file)
--- 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