cic.dtd

<?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 de Bruijn  -->
<!-- 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;>