diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/xml/cic.dtd | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/xml/cic.dtd')
-rw-r--r-- | plugins/xml/cic.dtd | 259 |
1 files changed, 259 insertions, 0 deletions
diff --git a/plugins/xml/cic.dtd b/plugins/xml/cic.dtd new file mode 100644 index 00000000..c8035cab --- /dev/null +++ b/plugins/xml/cic.dtd @@ -0,0 +1,259 @@ +<?xml encoding="ISO-8859-1"?> + +<!-- Copyright (C) 2000-2004, HELM Team --> +<!-- --> +<!-- This file is part of HELM, an Hypertextual, Electronic --> +<!-- Library of Mathematics, developed at the Computer Science --> +<!-- Department, University of Bologna, Italy. --> +<!-- --> +<!-- HELM is free software; you can redistribute it and/or --> +<!-- modify it under the terms of the GNU General Public License --> +<!-- as published by the Free Software Foundation; either version 2 --> +<!-- of the License, or (at your option) any later version. --> +<!-- --> +<!-- HELM is distributed in the hope that it will be useful, --> +<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of --> +<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the --> +<!-- GNU General Public License for more details. --> +<!-- --> +<!-- You should have received a copy of the GNU General Public License --> +<!-- along with HELM; if not, write to the Free Software --> +<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, --> +<!-- MA 02111-1307, USA. --> +<!-- --> +<!-- For details, see the HELM World-Wide-Web page, --> +<!-- http://cs.unibo.it/helm/. --> + +<!-- DTD FOR CIC OBJECTS: --> + +<!-- CIC term declaration --> + +<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST| + LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'> + +<!-- CIC sorts --> + +<!ENTITY % sort '(Prop|Set|Type|CProp)'> + +<!-- CIC sequents --> + +<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> + +<!-- CIC objects: --> + +<!ELEMENT ConstantType %term;> +<!ATTLIST ConstantType + name CDATA #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT ConstantBody %term;> +<!ATTLIST ConstantBody + for CDATA #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT CurrentProof (Conjecture*,body)> +<!ATTLIST CurrentProof + of CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT InductiveDefinition (InductiveType+)> +<!ATTLIST InductiveDefinition + noParams NMTOKEN #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Variable (body?,type)> +<!ATTLIST Variable + name CDATA #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Sequent %sequent;> +<!ATTLIST Sequent + no NMTOKEN #REQUIRED + id ID #REQUIRED> + +<!-- Elements used in CIC objects, which are not terms: --> + +<!ELEMENT InductiveType (arity,Constructor*)> +<!ATTLIST InductiveType + name CDATA #REQUIRED + inductive (true|false) #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Conjecture %sequent;> +<!ATTLIST Conjecture + no NMTOKEN #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Constructor %term;> +<!ATTLIST Constructor + name CDATA #REQUIRED> + +<!ELEMENT Decl %term;> +<!ATTLIST Decl + name CDATA #IMPLIED + id ID #REQUIRED> + +<!ELEMENT Def %term;> +<!ATTLIST Def + name CDATA #IMPLIED + id ID #REQUIRED> + +<!ELEMENT Hidden EMPTY> +<!ATTLIST Hidden + id ID #REQUIRED> + +<!ELEMENT Goal %term;> + +<!-- CIC terms: --> + +<!ELEMENT LAMBDA (decl*,target)> +<!ATTLIST LAMBDA + sort %sort; #REQUIRED> + +<!ELEMENT LETIN (def*,target)> +<!ATTLIST LETIN + sort %sort; #REQUIRED> + +<!ELEMENT PROD (decl*,target)> +<!ATTLIST PROD + type %sort; #REQUIRED> + +<!ELEMENT CAST (term,type)> +<!ATTLIST CAST + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT REL EMPTY> +<!ATTLIST REL + value NMTOKEN #REQUIRED + binder CDATA #REQUIRED + id ID #REQUIRED + idref IDREF #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT SORT EMPTY> +<!ATTLIST SORT + value CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT APPLY (%term;)+> +<!ATTLIST APPLY + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT VAR EMPTY> +<!ATTLIST VAR + uri CDATA #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!-- The substitutions are ordered by increasing DeBrujin --> +<!-- index. An empty substitution means that that index is --> +<!-- not accessible. --> +<!ELEMENT META (substitution*)> +<!ATTLIST META + no NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT IMPLICIT EMPTY> +<!ATTLIST IMPLICIT + id ID #REQUIRED> + +<!ELEMENT CONST EMPTY> +<!ATTLIST CONST + uri CDATA #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT MUTIND EMPTY> +<!ATTLIST MUTIND + uri CDATA #REQUIRED + noType NMTOKEN #REQUIRED + id ID #REQUIRED> + +<!ELEMENT MUTCONSTRUCT EMPTY> +<!ATTLIST MUTCONSTRUCT + uri CDATA #REQUIRED + noType NMTOKEN #REQUIRED + noConstr NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)> +<!ATTLIST MUTCASE + uriType CDATA #REQUIRED + noType NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT FIX (FixFunction+)> +<!ATTLIST FIX + noFun NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT COFIX (CofixFunction+)> +<!ATTLIST COFIX + noFun NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!-- Elements used in CIC terms: --> + +<!ELEMENT FixFunction (type,body)> +<!ATTLIST FixFunction + name CDATA #REQUIRED + id ID #REQUIRED + recIndex NMTOKEN #REQUIRED> + +<!ELEMENT CofixFunction (type,body)> +<!ATTLIST CofixFunction + id ID #REQUIRED + name CDATA #REQUIRED> + +<!ELEMENT substitution ((%term;)?)> + +<!-- Explicit named substitutions: --> + +<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)> +<!ATTLIST instantiate + id ID #IMPLIED> + +<!-- Sintactic sugar for CIC terms and for CIC objects: --> + +<!ELEMENT arg %term;> +<!ATTLIST arg + relUri CDATA #REQUIRED> + +<!ELEMENT decl %term;> +<!ATTLIST decl + id ID #REQUIRED + type %sort; #REQUIRED + binder CDATA #IMPLIED> + +<!ELEMENT def %term;> +<!ATTLIST def + id ID #REQUIRED + sort %sort; #REQUIRED + binder CDATA #IMPLIED> + +<!ELEMENT target %term;> + +<!ELEMENT term %term;> + +<!ELEMENT type %term;> + +<!ELEMENT arity %term;> + +<!ELEMENT patternsType %term;> + +<!ELEMENT inductiveTerm %term;> + +<!ELEMENT pattern %term;> + +<!ELEMENT body %term;> |