From 4f6616b07fb0de97199db9349b2dc01ee0dc33f3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Nov 2002 17:01:07 +0000
Subject: [PATCH] * iff notation added (new csymbol) * New notation for lists
 added (list.xml)

---
 helm/meta_style/.cvsignore     |  1 +
 helm/meta_style/Makefile       | 13 ++++++--
 helm/meta_style/basic.xml      | 11 +++++++
 helm/meta_style/list.xml       | 55 ++++++++++++++++++++++++++++++++++
 helm/meta_style/xslt_index.txt |  1 +
 5 files changed, 79 insertions(+), 2 deletions(-)
 create mode 100644 helm/meta_style/list.xml

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 847efdb31..f51cc8094 100644
--- 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 5eaefa3a8..66419e9a3 100644
--- 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
index 000000000..6e42d21a1
--- /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 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
-- 
2.39.2