summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocst.rnc
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocst.rnc')
-rw-r--r--Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocst.rnc135
1 files changed, 135 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocst.rnc b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocst.rnc
new file mode 100644
index 00000000000..46419186d52
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocst.rnc
@@ -0,0 +1,135 @@
+# 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)
+
+default namespace omdoc = "http://omdoc.org/ns"
+
+omdoc.class &= symbol* & axiom* & definition* & imports* & assertion* & type* & alternative* & example* & theory*
+
+constitutive.attribs = id.attribs & attribute generated-from {omdocref}?
+sym.role.attrib = attribute role {"type" | "sort" | "object" |
+ "binder" | "attribution" | "application" | "constant" |
+ "semantic-attribution" | "error"}
+theory-unique = xsd:NCName
+scope.attrib = attribute scope {"global" | "local"}?
+symbol.attribs = scope.attrib &
+ attribute name {theory-unique}? &
+ constitutive.attribs &
+ sym.role.attrib?
+symbol.model = metadata.class & type*
+symbol = element symbol {tref|(symbol.attribs & symbol.model)}
+
+forname.attrib = attribute for {list {xsd:NCName+}}
+axiom.attribs = constitutive.attribs & forname.attrib & attribute type {xsd:string}?
+axiom.model = metadata.class & mcf.class
+axiom = element axiom {tref|(axiom.attribs & axiom.model)}
+
+#informal definitions
+def.informal = attribute type {"informal"}?
+
+#simple definitions
+def.simple.attribs = attribute type {"simple"}
+def.simple = def.simple.attribs & mobj
+
+#implicit definitions
+exists.attrib = attribute existence {omdocref}
+unique.attrib = attribute uniqueness {omdocref}
+def.implicit.attribs = attribute type {"implicit"} & exists.attrib? & unique.attrib?
+def.implicit = def.implicit.attribs & FMP*
+
+exhaust.attrib = attribute exhaustivity {omdocref}
+consist.attrib = attribute consistency {omdocref}
+
+def.pattern.attribs = attribute type {"pattern"}? & exhaust.attrib? & consist.attrib?
+def.pattern.model = requation*
+def.pattern = def.pattern.attribs & def.pattern.model
+
+def.inductive.attribs = attribute type {"inductive"}? & exhaust.attrib? & consist.attrib?
+def.inductive.model = requation* & measure? & ordering?
+def.inductive = def.inductive.attribs & def.inductive.model
+
+def.eq = def.pattern | def.inductive
+
+#all definition forms, add more by extending this.
+defs.all = def.informal | def.simple | def.implicit | def.eq
+
+# 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.
+definition.attribs = constitutive.attribs & forname.attrib
+definition = element definition {tref|(definition.attribs & mc.class & defs.all)}
+
+requation.attribs = id.attribs
+requation.model = mobj,mobj
+requation = element requation {tref|(requation.attribs & requation.model)}
+
+measure.attribs = id.attribs
+measure.model = mobj
+measure = element measure {tref|(measure.attribs & measure.model)}
+
+ordering.attribs = id.attribs & attribute terminating {omdocref}?
+ordering.model = mobj
+ordering = element ordering {tref|(ordering.attribs & ordering.model)}
+
+# the non-constitutive statements, they need a theory attribute
+toplevel.attribs &= attribute theory {omdocref}?
+
+ded.status.class = "satisfiable" | "counter-satisfiable" | "no-consequence" |
+ "theorem" | "conter-theorem" | "contradictory-axioms" |
+ "tautologous-conclusion" | " tautology" | "equivalent" |
+ "conunter-equivalent" | "unsatisfiable-conclusion" | "unsatisfiable"
+
+just-by.attrib = attribute just-by {omdocref}
+assertion.attribs = toplevel.attribs &
+ attribute type {assertiontype}? &
+ attribute status {ded.status.class}? &
+ just-by.attrib?
+assertion.model = mcf.class
+assertion = element assertion {tref|(assertion.attribs & assertion.model)}
+# 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.
+
+type.attribs = toplevel.attribs & just-by.attrib? &
+ attribute system {omdocref}? &
+ attribute for {omdocref}?
+type.model = mc.class, mobj, mobj?
+type = element type {tref|(type.attribs & type.model)}
+
+##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)
+alternative.attribs = toplevel.attribs & for.attrib &
+ ((attribute equivalence {omdocref},
+ attribute equivalence-thm {omdocref}) |
+ (attribute entailed-by {omdocref} &
+ attribute entails {omdocref} &
+ attribute entailed-by-thm {omdocref} &
+ attribute entails-thm {omdocref}))
+alternative.model = mc.class & defs.all
+alternative = element alternative {tref|(alternative.attribs & alternative.model)}
+
+example.attribs = toplevel.attribs & for.attrib &
+ attribute type {"for" | "against" }? &
+ attribute assertion {omdocref}?
+example.model = mc.class,mobj*
+example = element example {tref|(example.attribs & example.model)}
+
+theory.attribs = id.attribs &
+ attribute cdurl {xsd:anyURI}? &
+ attribute cdbase {xsd:anyURI}? &
+ attribute cdreviewdate {xsd:date}? &
+ attribute cdversion {xsd:nonNegativeInteger}? &
+ attribute cdrevision {xsd:nonNegativeInteger}? &
+ attribute cdstatus {"official" | "experimental" |"private" | "obsolete"}?
+theory.model = metadata.class & omdoc.class
+theory = element theory {tref|(theory.attribs & theory.model)}
+
+imports.attribs = id.attribs & from.attrib
+imports.model = metadata.class
+imports = element imports {tref|(imports.attribs & imports.model)}
+
+