]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/xml/ld.dtd
basic_rg: bugfix in AST to allow attributes in global entries
[helm.git] / helm / software / lambda-delta / xml / ld.dtd
diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd
new file mode 100644 (file)
index 0000000..00ea552
--- /dev/null
@@ -0,0 +1,84 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for persistent lambda-delta logical data -->
+
+<!-- TERMS -->
+
+<!ENTITY % leaf '(Sort|LRef|GRef)'>
+
+<!ENTITY % node '(Cast|Appl|Abst|Abbr|Void)'>
+
+<!ENTITY % term '(%node;*,%leaf;)'>
+
+<!ELEMENT Sort EMPTY>
+<!ATTLIST Sort
+          position NMTOKEN #REQUIRED
+          name     CDATA   #IMPLIED
+>
+
+<!ELEMENT LRef EMPTY>
+<!ATTLIST LRef
+          position NMTOKEN #REQUIRED
+          name     CDATA   #IMPLIED
+>
+
+<!ELEMENT GRef EMPTY>
+<!ATTLIST GRef
+          uri  CDATA #REQUIRED
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT Cast %term;>
+<!ATTLIST Cast
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT Appl %term;>
+<!ATTLIST Appl
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT Abst %term;>
+<!ATTLIST Abst
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT Abbr %term;>
+<!ATTLIST Abbr
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT Void EMPTY>
+<!ATTLIST Void
+          name CDATA #IMPLIED
+>
+
+<!-- ENVIRONMENT ENTRIES -->
+
+<!ENTITY % entry '(ABST|ABBR|VOID)'> 
+
+<!ELEMENT ABST %term;>
+<!ATTLIST ABST
+          uri  CDATA #REQUIRED
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT ABBR %term;>
+<!ATTLIST ABBR
+          uri  CDATA #REQUIRED
+          name CDATA #IMPLIED
+>
+
+<!ELEMENT VOID EMPTY>
+<!ATTLIST VOID
+          uri  CDATA #REQUIRED
+          name CDATA #IMPLIED
+>
+
+<!-- ROOT -->
+
+<!ELEMENT ENTRY %entry;>
+<!ATTLIST ENTRY
+          hierarchy NMTOKEN  #REQUIRED
+          options   NMTOKENS #IMPLIED
+>