summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng')
-rw-r--r--Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng634
1 files changed, 634 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng b/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng
new file mode 100644
index 00000000000..59e54d0f723
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng
@@ -0,0 +1,634 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ A RelaxNG schema for Open Mathematical documents (OMDoc 1.3) Module ST
+ $Id: omdocst.rnc 8972 2011-09-09 11:36:34Z kohlhase $
+ $HeadURL: https://svn.omdoc.org/repos/omdoc/branches/omdoc-1.3/schema/rnc/omdocst.rnc $
+ See the documentation and examples at http://www.omdoc.org
+ Copyright (c) 2004-2007 Michael Kohlhase, released under the GNU Public License (GPL)
+-->
+<grammar ns="http://omdoc.org/ns" xmlns:omdoc="http://omdoc.org/ns" xmlns:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0" datatypeLibrary="http://www.w3.org/2001/XMLSchema-datatypes">
+ <define name="omdoc.class" combine="interleave">
+ <interleave>
+ <zeroOrMore>
+ <ref name="symbol"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="axiom"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="definition"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="imports"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="assertion"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="type"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="alternative"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="example"/>
+ </zeroOrMore>
+ <zeroOrMore>
+ <ref name="theory"/>
+ </zeroOrMore>
+ </interleave>
+ </define>
+ <define name="constitutive.attribs">
+ <interleave>
+ <ref name="id.attribs"/>
+ <optional>
+ <attribute name="generated-from">
+ <ref name="omdocref"/>
+ </attribute>
+ </optional>
+ </interleave>
+ </define>
+ <define name="sym.role.attrib">
+ <attribute name="role">
+ <choice>
+ <value>type</value>
+ <value>sort</value>
+ <value>object</value>
+ <value>binder</value>
+ <value>attribution</value>
+ <value>application</value>
+ <value>constant</value>
+ <value>semantic-attribution</value>
+ <value>error</value>
+ </choice>
+ </attribute>
+ </define>
+ <define name="theory-unique">
+ <data type="NCName"/>
+ </define>
+ <define name="scope.attrib">
+ <optional>
+ <attribute name="scope">
+ <choice>
+ <value>global</value>
+ <value>local</value>
+ </choice>
+ </attribute>
+ </optional>
+ </define>
+ <define name="symbol.attribs">
+ <interleave>
+ <ref name="scope.attrib"/>
+ <optional>
+ <attribute name="name">
+ <ref name="theory-unique"/>
+ </attribute>
+ </optional>
+ <ref name="constitutive.attribs"/>
+ <optional>
+ <ref name="sym.role.attrib"/>
+ </optional>
+ </interleave>
+ </define>
+ <define name="symbol.model">
+ <interleave>
+ <ref name="metadata.class"/>
+ <zeroOrMore>
+ <ref name="type"/>
+ </zeroOrMore>
+ </interleave>
+ </define>
+ <define name="symbol">
+ <element name="symbol">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="symbol.attribs"/>
+ <ref name="symbol.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="forname.attrib">
+ <attribute name="for">
+ <list>
+ <oneOrMore>
+ <data type="NCName"/>
+ </oneOrMore>
+ </list>
+ </attribute>
+ </define>
+ <define name="axiom.attribs">
+ <interleave>
+ <ref name="constitutive.attribs"/>
+ <ref name="forname.attrib"/>
+ <optional>
+ <attribute name="type">
+ <data type="string"/>
+ </attribute>
+ </optional>
+ </interleave>
+ </define>
+ <define name="axiom.model">
+ <interleave>
+ <ref name="metadata.class"/>
+ <ref name="mcf.class"/>
+ </interleave>
+ </define>
+ <define name="axiom">
+ <element name="axiom">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="axiom.attribs"/>
+ <ref name="axiom.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <!-- informal definitions -->
+ <define name="def.informal">
+ <optional>
+ <attribute name="type">
+ <value>informal</value>
+ </attribute>
+ </optional>
+ </define>
+ <!-- simple definitions -->
+ <define name="def.simple.attribs">
+ <attribute name="type">
+ <value>simple</value>
+ </attribute>
+ </define>
+ <define name="def.simple">
+ <interleave>
+ <ref name="def.simple.attribs"/>
+ <ref name="mobj"/>
+ </interleave>
+ </define>
+ <!-- implicit definitions -->
+ <define name="exists.attrib">
+ <attribute name="existence">
+ <ref name="omdocref"/>
+ </attribute>
+ </define>
+ <define name="unique.attrib">
+ <attribute name="uniqueness">
+ <ref name="omdocref"/>
+ </attribute>
+ </define>
+ <define name="def.implicit.attribs">
+ <interleave>
+ <attribute name="type">
+ <value>implicit</value>
+ </attribute>
+ <optional>
+ <ref name="exists.attrib"/>
+ </optional>
+ <optional>
+ <ref name="unique.attrib"/>
+ </optional>
+ </interleave>
+ </define>
+ <define name="def.implicit">
+ <interleave>
+ <ref name="def.implicit.attribs"/>
+ <zeroOrMore>
+ <ref name="FMP"/>
+ </zeroOrMore>
+ </interleave>
+ </define>
+ <define name="exhaust.attrib">
+ <attribute name="exhaustivity">
+ <ref name="omdocref"/>
+ </attribute>
+ </define>
+ <define name="consist.attrib">
+ <attribute name="consistency">
+ <ref name="omdocref"/>
+ </attribute>
+ </define>
+ <define name="def.pattern.attribs">
+ <interleave>
+ <optional>
+ <attribute name="type">
+ <value>pattern</value>
+ </attribute>
+ </optional>
+ <optional>
+ <ref name="exhaust.attrib"/>
+ </optional>
+ <optional>
+ <ref name="consist.attrib"/>
+ </optional>
+ </interleave>
+ </define>
+ <define name="def.pattern.model">
+ <zeroOrMore>
+ <ref name="requation"/>
+ </zeroOrMore>
+ </define>
+ <define name="def.pattern">
+ <interleave>
+ <ref name="def.pattern.attribs"/>
+ <ref name="def.pattern.model"/>
+ </interleave>
+ </define>
+ <define name="def.inductive.attribs">
+ <interleave>
+ <optional>
+ <attribute name="type">
+ <value>inductive</value>
+ </attribute>
+ </optional>
+ <optional>
+ <ref name="exhaust.attrib"/>
+ </optional>
+ <optional>
+ <ref name="consist.attrib"/>
+ </optional>
+ </interleave>
+ </define>
+ <define name="def.inductive.model">
+ <interleave>
+ <zeroOrMore>
+ <ref name="requation"/>
+ </zeroOrMore>
+ <optional>
+ <ref name="measure"/>
+ </optional>
+ <optional>
+ <ref name="ordering"/>
+ </optional>
+ </interleave>
+ </define>
+ <define name="def.inductive">
+ <interleave>
+ <ref name="def.inductive.attribs"/>
+ <ref name="def.inductive.model"/>
+ </interleave>
+ </define>
+ <define name="def.eq">
+ <choice>
+ <ref name="def.pattern"/>
+ <ref name="def.inductive"/>
+ </choice>
+ </define>
+ <!-- all definition forms, add more by extending this. -->
+ <define name="defs.all">
+ <choice>
+ <ref name="def.informal"/>
+ <ref name="def.simple"/>
+ <ref name="def.implicit"/>
+ <ref name="def.eq"/>
+ </choice>
+ </define>
+ <!--
+ Definitions contain CMPs, FMPs and concept specifications.
+ The latter define the set of concepts defined in this element.
+ They can be reached under this name in the content dictionary
+ of the name specified in the theory attribute of the definition.
+ -->
+ <define name="definition.attribs">
+ <interleave>
+ <ref name="constitutive.attribs"/>
+ <ref name="forname.attrib"/>
+ </interleave>
+ </define>
+ <define name="definition">
+ <element name="definition">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="definition.attribs"/>
+ <ref name="mc.class"/>
+ <ref name="defs.all"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="requation.attribs">
+ <ref name="id.attribs"/>
+ </define>
+ <define name="requation.model">
+ <ref name="mobj"/>
+ <ref name="mobj"/>
+ </define>
+ <define name="requation">
+ <element name="requation">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="requation.attribs"/>
+ <ref name="requation.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="measure.attribs">
+ <ref name="id.attribs"/>
+ </define>
+ <define name="measure.model">
+ <ref name="mobj"/>
+ </define>
+ <define name="measure">
+ <element name="measure">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="measure.attribs"/>
+ <ref name="measure.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="ordering.attribs">
+ <interleave>
+ <ref name="id.attribs"/>
+ <optional>
+ <attribute name="terminating">
+ <ref name="omdocref"/>
+ </attribute>
+ </optional>
+ </interleave>
+ </define>
+ <define name="ordering.model">
+ <ref name="mobj"/>
+ </define>
+ <define name="ordering">
+ <element name="ordering">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="ordering.attribs"/>
+ <ref name="ordering.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <!-- the non-constitutive statements, they need a theory attribute -->
+ <define name="toplevel.attribs" combine="interleave">
+ <optional>
+ <attribute name="theory">
+ <ref name="omdocref"/>
+ </attribute>
+ </optional>
+ </define>
+ <define name="ded.status.class">
+ <choice>
+ <value>satisfiable</value>
+ <value>counter-satisfiable</value>
+ <value>no-consequence</value>
+ <value>theorem</value>
+ <value>conter-theorem</value>
+ <value>contradictory-axioms</value>
+ <value>tautologous-conclusion</value>
+ <value> tautology</value>
+ <value>equivalent</value>
+ <value>conunter-equivalent</value>
+ <value>unsatisfiable-conclusion</value>
+ <value>unsatisfiable</value>
+ </choice>
+ </define>
+ <define name="just-by.attrib">
+ <attribute name="just-by">
+ <ref name="omdocref"/>
+ </attribute>
+ </define>
+ <define name="assertion.attribs">
+ <interleave>
+ <ref name="toplevel.attribs"/>
+ <optional>
+ <attribute name="type">
+ <ref name="assertiontype"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="status">
+ <ref name="ded.status.class"/>
+ </attribute>
+ </optional>
+ <optional>
+ <ref name="just-by.attrib"/>
+ </optional>
+ </interleave>
+ </define>
+ <define name="assertion.model">
+ <ref name="mcf.class"/>
+ </define>
+ <define name="assertion">
+ <element name="assertion">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="assertion.attribs"/>
+ <ref name="assertion.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <!--
+ the assertiontype has no formal meaning yet, it is solely for human consumption.
+ 'just-by' is a list of URIRefs that point to proof objects, etc that justifies the status.
+ -->
+ <define name="type.attribs">
+ <interleave>
+ <ref name="toplevel.attribs"/>
+ <optional>
+ <ref name="just-by.attrib"/>
+ </optional>
+ <optional>
+ <attribute name="system">
+ <ref name="omdocref"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="for">
+ <ref name="omdocref"/>
+ </attribute>
+ </optional>
+ </interleave>
+ </define>
+ <define name="type.model">
+ <ref name="mc.class"/>
+ <ref name="mobj"/>
+ <optional>
+ <ref name="mobj"/>
+ </optional>
+ </define>
+ <define name="type">
+ <element name="type">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="type.attribs"/>
+ <ref name="type.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="alternative.attribs">
+ <a:documentation>just-by, points to the theorem justifying well-definedness
+entailed-by, entails, point to other (equivalent definitions
+entailed-by-thm, entails-thm point to the theorems justifying
+the entailment relation)</a:documentation>
+ <interleave>
+ <ref name="toplevel.attribs"/>
+ <ref name="for.attrib"/>
+ <choice>
+ <group>
+ <attribute name="equivalence">
+ <ref name="omdocref"/>
+ </attribute>
+ <attribute name="equivalence-thm">
+ <ref name="omdocref"/>
+ </attribute>
+ </group>
+ <interleave>
+ <attribute name="entailed-by">
+ <ref name="omdocref"/>
+ </attribute>
+ <attribute name="entails">
+ <ref name="omdocref"/>
+ </attribute>
+ <attribute name="entailed-by-thm">
+ <ref name="omdocref"/>
+ </attribute>
+ <attribute name="entails-thm">
+ <ref name="omdocref"/>
+ </attribute>
+ </interleave>
+ </choice>
+ </interleave>
+ </define>
+ <define name="alternative.model">
+ <interleave>
+ <ref name="mc.class"/>
+ <ref name="defs.all"/>
+ </interleave>
+ </define>
+ <define name="alternative">
+ <element name="alternative">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="alternative.attribs"/>
+ <ref name="alternative.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="example.attribs">
+ <interleave>
+ <ref name="toplevel.attribs"/>
+ <ref name="for.attrib"/>
+ <optional>
+ <attribute name="type">
+ <choice>
+ <value>for</value>
+ <value>against</value>
+ </choice>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="assertion">
+ <ref name="omdocref"/>
+ </attribute>
+ </optional>
+ </interleave>
+ </define>
+ <define name="example.model">
+ <ref name="mc.class"/>
+ <zeroOrMore>
+ <ref name="mobj"/>
+ </zeroOrMore>
+ </define>
+ <define name="example">
+ <element name="example">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="example.attribs"/>
+ <ref name="example.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="theory.attribs">
+ <interleave>
+ <ref name="id.attribs"/>
+ <optional>
+ <attribute name="cdurl">
+ <data type="anyURI"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="cdbase">
+ <data type="anyURI"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="cdreviewdate">
+ <data type="date"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="cdversion">
+ <data type="nonNegativeInteger"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="cdrevision">
+ <data type="nonNegativeInteger"/>
+ </attribute>
+ </optional>
+ <optional>
+ <attribute name="cdstatus">
+ <choice>
+ <value>official</value>
+ <value>experimental</value>
+ <value>private</value>
+ <value>obsolete</value>
+ </choice>
+ </attribute>
+ </optional>
+ </interleave>
+ </define>
+ <define name="theory.model">
+ <interleave>
+ <ref name="metadata.class"/>
+ <ref name="omdoc.class"/>
+ </interleave>
+ </define>
+ <define name="theory">
+ <element name="theory">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="theory.attribs"/>
+ <ref name="theory.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+ <define name="imports.attribs">
+ <interleave>
+ <ref name="id.attribs"/>
+ <ref name="from.attrib"/>
+ </interleave>
+ </define>
+ <define name="imports.model">
+ <ref name="metadata.class"/>
+ </define>
+ <define name="imports">
+ <element name="imports">
+ <choice>
+ <ref name="tref"/>
+ <interleave>
+ <ref name="imports.attribs"/>
+ <ref name="imports.model"/>
+ </interleave>
+ </choice>
+ </element>
+ </define>
+</grammar>