<?xml encoding="ISO-8859-1"?>
-<!-- Copyright (C) 2000, 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: -->
-<!-- First draft: September 1999, Claudio Sacerdoti Coen -->
-<!-- Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena -->
-<!-- Last Revision: April 4 2000, Claudio Sacerdoti Coen -->
-<!-- Last Revision: June 19 2000, Claudio Sacerdoti Coen -->
-<!-- Last Revision: June 20 2000, Claudio Sacerdoti Coen -->
-<!--*****************************************************************-->
+<!-- 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)'>
+ LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'>
<!-- CIC sorts -->
-<!ENTITY % sort '(Prop|Set|Type)'>
+<!ENTITY % sort '(Prop|Set|Type|CProp)'>
<!-- CIC sequents -->
<!-- CIC objects: -->
-<!ELEMENT Definition (body, type)>
-<!ATTLIST Definition
+<!-- CSC: so far params is equal to the one of the only body. -->
+<!ELEMENT ConstantType (attributes?,%term;)>
+<!ATTLIST ConstantType
name CDATA #REQUIRED
params CDATA #REQUIRED
- paramMode (POSSIBLE) #IMPLIED
id ID #REQUIRED>
-<!ELEMENT Axiom (type)>
-<!ATTLIST Axiom
- name CDATA #REQUIRED
- params CDATA #REQUIRED
- id ID #REQUIRED>
+<!ELEMENT ConstantBody (attributes?,%term;)>
+<!ATTLIST ConstantBody
+ for CDATA #REQUIRED
+ params CDATA #REQUIRED
+ id ID #REQUIRED>
-<!ELEMENT CurrentProof (Conjecture*,body,type)>
+<!ELEMENT CurrentProof (attributes?,Conjecture*,body)>
<!ATTLIST CurrentProof
- name CDATA #REQUIRED
- id ID #REQUIRED>
+ of CDATA #REQUIRED
+ id ID #REQUIRED>
-<!ELEMENT InductiveDefinition (InductiveType+)>
+<!ELEMENT InductiveDefinition (attributes?,InductiveType+)>
<!ATTLIST InductiveDefinition
noParams NMTOKEN #REQUIRED
params CDATA #REQUIRED
id ID #REQUIRED>
-<!ELEMENT Variable (body?,type)>
+<!ELEMENT Variable (attributes?,body?,type)>
<!ATTLIST Variable
- name CDATA #REQUIRED
- id ID #REQUIRED>
+ name CDATA #REQUIRED
+ params CDATA #REQUIRED
+ id ID #REQUIRED>
<!ELEMENT Sequent %sequent;>
<!ATTLIST Sequent
no NMTOKEN #REQUIRED
id ID #REQUIRED>
+<!ELEMENT attributes ((class,generated?)|(generated,class?))?>
+
+<!ELEMENT generated EMPTY>
+
+<!-- the fields are allowed only when @value = "record"
+ the SORT is allowed only when @value = "elim" -->
+<!ELEMENT class (field*|SORT)>
+<!ATTLIST class
+ value (coercion|elim|record|projection) #REQUIRED>
+
<!-- Elements used in CIC objects, which are not terms: -->
<!ELEMENT InductiveType (arity,Constructor*)>
<!ATTLIST InductiveType
name CDATA #REQUIRED
- inductive (true|false) #REQUIRED>
+ inductive (true|false) #REQUIRED
+ id ID #REQUIRED>
<!ELEMENT Conjecture %sequent;>
<!ATTLIST Conjecture
- no NMTOKEN #REQUIRED>
+ no NMTOKEN #REQUIRED
+ id ID #REQUIRED>
<!ELEMENT Constructor %term;>
<!ATTLIST Constructor
<!ELEMENT Decl %term;>
<!ATTLIST Decl
- name CDATA #IMPLIED>
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
<!ELEMENT Def %term;>
<!ATTLIST Def
- name CDATA #IMPLIED>
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
<!ELEMENT Hidden EMPTY>
+<!ATTLIST Hidden
+ id ID #REQUIRED>
<!ELEMENT Goal %term;>
<!-- CIC terms: -->
-<!ELEMENT LAMBDA (source,target)>
+<!ELEMENT LAMBDA (decl*,target)>
<!ATTLIST LAMBDA
- id ID #REQUIRED
sort %sort; #REQUIRED>
-<!ELEMENT LETIN (term,letintarget)>
+<!ELEMENT LETIN (def*,target)>
<!ATTLIST LETIN
- id ID #REQUIRED
sort %sort; #REQUIRED>
-<!ELEMENT PROD (source,target)>
+<!ELEMENT PROD (decl*,target)>
<!ATTLIST PROD
- id ID #REQUIRED
type %sort; #REQUIRED>
<!ELEMENT CAST (term,type)>
value NMTOKEN #REQUIRED
binder CDATA #REQUIRED
id ID #REQUIRED
+ idref IDREF #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT SORT EMPTY>
<!ELEMENT VAR EMPTY>
<!ATTLIST VAR
- relUri CDATA #REQUIRED
- id ID #REQUIRED
- sort %sort; #REQUIRED>
+ 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 -->
<!ELEMENT IMPLICIT EMPTY>
<!ATTLIST IMPLICIT
- id ID #REQUIRED>
+ id ID #REQUIRED
+ annotation (closed|type|hole) #IMPLIED>
<!ELEMENT CONST EMPTY>
<!ATTLIST CONST
<!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 source %term;>
+<!ELEMENT arg %term;>
+<!ATTLIST arg
+ relUri CDATA #REQUIRED>
-<!ELEMENT target %term;>
-<!ATTLIST target
- binder CDATA #IMPLIED>
+<!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 letintarget %term;>
-<!ATTLIST letintarget
- binder CDATA #REQUIRED>
+<!ELEMENT target %term;>
<!ELEMENT term %term;>
projects / helm.git / blobdiff