diff options
Diffstat (limited to 'dev/doc/cic.dtd')
| -rw-r--r-- | dev/doc/cic.dtd | 231 |
1 files changed, 231 insertions, 0 deletions
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd new file mode 100644 index 00000000..f2314e22 --- /dev/null +++ b/dev/doc/cic.dtd @@ -0,0 +1,231 @@ +<?xml encoding="ISO-8859-1"?> + +<!-- 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)'> + +<!-- CIC sequents --> + +<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> + +<!-- CIC objects: --> + +<!ELEMENT ConstantType %term;> +<!ATTLIST ConstantType + name 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 + 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> + +<!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 + id ID #REQUIRED + 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 + relUri 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 + recIndex NMTOKEN #REQUIRED> + +<!ELEMENT CofixFunction (type,body)> +<!ATTLIST CofixFunction + name CDATA #REQUIRED> + +<!ELEMENT substitution ((%term;)?)> + +<!-- Explicit named substitutions: --> + +<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),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;> |