diff options
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.rng | 634 |
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> |