aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-08 18:34:04 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-08 18:46:25 +0200
commit7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 (patch)
treeeeb9435bb4e64566647c5626a2a0f4b83eb58b08 /plugins/xml
parent7a5eb53973ec3fd921b56339557c48681972849e (diff)
Removing the XML plugin.
Left a README, just in case someone will discover the remnants of it decades from now.
Diffstat (limited to 'plugins/xml')
-rw-r--r--plugins/xml/COPYRIGHT25
-rw-r--r--plugins/xml/README256
-rw-r--r--plugins/xml/acic.ml108
-rw-r--r--plugins/xml/acic2Xml.ml4363
-rw-r--r--plugins/xml/cic.dtd259
-rw-r--r--plugins/xml/cic2Xml.ml17
-rw-r--r--plugins/xml/cic2acic.ml927
-rw-r--r--plugins/xml/doubleTypeInference.ml266
-rw-r--r--plugins/xml/doubleTypeInference.mli24
-rw-r--r--plugins/xml/theoryobject.dtd62
-rw-r--r--plugins/xml/unshare.ml52
-rw-r--r--plugins/xml/unshare.mli21
-rw-r--r--plugins/xml/xml.ml478
-rw-r--r--plugins/xml/xml.mli38
-rw-r--r--plugins/xml/xml_plugin.mllib10
-rw-r--r--plugins/xml/xmlcommand.ml536
-rw-r--r--plugins/xml/xmlcommand.mli28
-rw-r--r--plugins/xml/xmlentries.ml432
18 files changed, 3 insertions, 3099 deletions
diff --git a/plugins/xml/COPYRIGHT b/plugins/xml/COPYRIGHT
deleted file mode 100644
index c8d231fd3..000000000
--- a/plugins/xml/COPYRIGHT
+++ /dev/null
@@ -1,25 +0,0 @@
-(******************************************************************************)
-(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* Project Helm (http://helm.cs.unibo.it) *)
-(* Project MoWGLI (http://mowgli.cs.unibo.it) *)
-(* *)
-(* Coq Exportation to XML *)
-(* *)
-(******************************************************************************)
-
-This Coq module has been developed by Claudio Sacerdoti Coen
-<sacerdot@cs.unibo.it> as a developer of projects HELM and MoWGLI.
-
-Project HELM (for Hypertextual Electronic Library of Mathematics) is a
-project developed at the Department of Computer Science, University of Bologna;
-http://helm.cs.unibo.it
-
-Project MoWGLI (Mathematics on the Web: Get It by Logics and Interfaces)
-is a UE IST project that generalizes and extends the HELM project;
-http://mowgli.cs.unibo.it
-
-The author is interested in any possible usage of the module.
-So, if you plan to use the module, please send him an e-mail.
-
-The licensing policy applied to the module is the same as for the whole Coq
-distribution.
diff --git a/plugins/xml/README b/plugins/xml/README
index a45dd31a5..cf5b3e0f4 100644
--- a/plugins/xml/README
+++ b/plugins/xml/README
@@ -1,254 +1,4 @@
-(******************************************************************************)
-(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* Project Helm (http://helm.cs.unibo.it) *)
-(* Project MoWGLI (http://mowgli.cs.unibo.it) *)
-(* *)
-(* Coq Exportation to XML *)
-(* *)
-(******************************************************************************)
+Here was the XML plugin. It is now defunct. May its soul rest in peace.
-This module provides commands to export a piece of Coq library in XML format.
-Only the information relevant to proof-checking and proof-rendering is exported,
-i.e. only the CIC proof objects (lambda-terms).
-
-This document is tructured in the following way:
- 1. User documentation
- 1.1. New vernacular commands available
- 1.2. New coqc/coqtop flags and suggested usage
- 1.3. How to exploit the XML files
- 2. Technical informations
- 2.1. Inner-types
- 2.2. CIC with Explicit Named Substitutions
- 2.3. The CIC with Explicit Named Substitutions XML DTD
-
-================================================================================
- USER DOCUMENTATION
-================================================================================
-
-=======================================
-1.1. New vernacular commands available:
-=======================================
-
-The new commands are:
-
- Print XML qualid. It prints in XML (to standard output) the
- object whose qualified name is qualid and
- its inner-types (see Sect. 2.1).
- The inner-types are always printed
- in their own XML file. If the object is a
- constant, its type and body are also printed
- as two distinct XML files.
- The object printed is always the most
- discharged form of the object (see
- the Section command of the Coq manual).
-
- Print XML File "filename" qualid. Similar to "Print XML qualid". The generated
- files are stored on the hard-disk using the
- base file name "filename".
-
- Show XML Proof. It prints in XML the current proof in
- progress. Its inner-types are also printed.
-
- Show XML File "filename" Proof. Similar to "Show XML Proof". The generated
- files are stored on the hard-disk using
- the base file name "filename".
-
- The verbosity of the previous commands is raised if the configuration
- parameter verbose of xmlcommand.ml is set to true at compile time.
-
-==============================================
-1.2. New coqc/coqtop flags and suggested usage
-==============================================
-
- The following flag has been added to coqc and coqtop:
-
- -xml export XML files either to the hierarchy rooted in
- the directory $COQ_XML_LIBRARY_ROOT (if the environment
- variable is set) or to stdout (if unset)
-
- If the flag is set, every definition or declaration is immediately
- exported to XML. The XML files describe the user-provided non-discharged
- form of the definition or declaration.
-
-
- The coq_makefile utility has also been modified to easily allow XML
- exportation:
-
- make COQ_XML=-xml (or, equivalently, setting the environment
- variable COQ_XML)
-
-
- The suggested usage of the module is the following:
-
- 1. add to your own contribution a valid Make file and use coq_makefile
- to generate the Makefile from the Make file.
- *WARNING:* Since logical names are used to structure the XML hierarchy,
- always add to the Make file at least one "-R" option to map physical
- file names to logical module paths. See the Coq manual for further
- informations on the -R flag.
- 2. set $COQ_XML_LIBRARY_ROOT to the directory where the XML file hierarchy
- must be physically rooted.
- 3. compile your contribution with "make COQ_XML=-xml"
-
-
-=================================
-1.3. How to exploit the XML files
-=================================
-
- Once the information is exported to XML, it becomes possible to implement
- services that are completely Coq-independent. Projects HELM and MoWGLI
- already provide rendering, searching and data mining functionalities.
-
- In particular, the standard library and contributions of Coq can be
- browsed and searched on the HELM web site:
-
- http://helm.cs.unibo.it/library.html
-
-
- If you want to publish your own contribution so that it is included in the
- HELM library, use the MoWGLI prototype upload form:
-
- http://mowgli.cs.unibo.it
-
-
-================================================================================
- TECHNICAL INFORMATIONS
-================================================================================
-
-==========================
-2.1. Inner-types
-==========================
-
-In order to do proof-rendering (for example in natural language),
-some redundant typing information is required, i.e. the type of
-at least some of the subterms of the bodies and types. So, each
-new command described in section 1.1 print not only
-the object, but also another XML file in which you can find
-the type of all the subterms of the terms of the printed object
-which respect the following conditions:
-
- 1. It's sort is Prop or CProp (the "sort"-like definition used in
- CoRN to type computationally relevant predicative propositions).
- 2. It is not a cast or an atomic term, i.e. it's root is not a CAST, REL,
- VAR, MUTCONSTR or CONST.
- 3. If it's root is a LAMBDA, then the root's parent node is not a LAMBDA,
- i.e. only the type of the outer LAMBDA of a block of nested LAMBDAs is
- printed.
-
-The rationale for the 3rd condition is that the type of the inner LAMBDAs
-could be easily computed starting from the type of the outer LAMBDA; moreover,
-the types of the inner LAMBDAs requires a lot of disk/memory space: removing
-the 3rd condition leads to XML file that are two times as big as the ones
-exported appling the 3rd condition.
-
-==========================================
-2.2. CIC with Explicit Named Substitutions
-==========================================
-
-The exported files are and XML encoding of the lambda-terms used by the
-Coq system. The implementative details of the Coq system are hidden as much
-as possible, so that the XML DTD is a straightforward encoding of the
-Calculus of (Co)Inductive Constructions.
-
-Nevertheless, there is a feature of the Coq system that can not be
-hidden in a completely satisfactory way: discharging. In Coq it is possible
-to open a section, declare variables and use them in the rest of the section
-as if they were axiom declarations. Once the section is closed, every definition
-and theorem in the section is discharged by abstracting it over the section
-variables. Variable declarations as well as section declarations are entirely
-dropped. Since we are interested in an XML encoding of definitions and
-theorems as close as possible to those directly provided the user, we
-do not want to export discharged forms. Exporting non-discharged theorem
-and definitions together with theorems that rely on the discharged forms
-obliges the tools that work on the XML encoding to implement discharging to
-achieve logical consistency. Moreover, the rendering of the files can be
-misleading, since hyperlinks can be shown between occurrences of the discharge
-form of a definition and the non-discharged definition, that are different
-objects.
-
-To overcome the previous limitations, Claudio Sacerdoti Coen developed in his
-PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions
-with Explicit Named Substitutions, that is a slight extension of CIC where
-discharging is not necessary. The DTD of the exported XML files describes
-constants, inductive types and variables of the Calculus of (Co)Inductive
-Constructions with Explicit Named Substitions. The conversion to the new
-calculus is performed during the exportation phase.
-
-The following example shows a very small Coq development together with its
-version in CIC with Explicit Named Substitutions.
-
-# CIC version: #
-Section S.
- Variable A : Prop.
-
- Definition impl := A -> A.
-
- Theorem t : impl. (* uses the undischarged form of impl *)
- Proof.
- exact (fun (a:A) => a).
- Qed.
-
-End S.
-
-Theorem t' : (impl False). (* uses the discharged form of impl *)
- Proof.
- exact (t False). (* uses the discharged form of t *)
- Qed.
-
-# Corresponding CIC with Explicit Named Substitutions version: #
-Section S.
- Variable A : Prop.
-
- Definition impl(A) := A -> A. (* theorems and definitions are
- explicitly abstracted over the
- variables. The name is sufficient
- to completely describe the abstraction *)
-
- Theorem t(A) : impl. (* impl where A is not instantiated *)
- Proof.
- exact (fun (a:A) => a).
- Qed.
-
-End S.
-
-Theorem t'() : impl{False/A}. (* impl where A is instantiated with False
- Notice that t' does not depend on A *)
- Proof.
- exact t{False/A}. (* t where A is instantiated with False *)
- Qed.
-
-Further details on the typing and reduction rules of the calculus can be
-found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency
-of the calculus is also proved.
-
-======================================================
-2.3. The CIC with Explicit Named Substitutions XML DTD
-======================================================
-
-A copy of the DTD can be found in the file "cic.dtd".
-
-<ConstantType> is the root element of the files that correspond to
- constant types.
-<ConstantBody> is the root element of the files that correspond to
- constant bodies. It is used only for closed definitions and
- theorems (i.e. when no metavariable occurs in the body
- or type of the constant)
-<CurrentProof> is the root element of the file that correspond to
- the body of a constant that depends on metavariables
- (e.g. unfinished proofs)
-<Variable> is the root element of the files that correspond to variables
-<InductiveTypes> is the root element of the files that correspond to blocks
- of mutually defined inductive definitions
-
-The elements
- <LAMBDA>,<CAST>,<PROD>,<REL>,<SORT>,<APPLY>,<VAR>,<META>, <IMPLICIT>,<CONST>,
- <LETIN>,<MUTIND>,<MUTCONSTRUCT>,<MUTCASE>,<FIX> and <COFIX>
-are used to encode the constructors of CIC. The sort or type attribute of the
-element, if present, is respectively the sort or the type of the term, that
-is a sort because of the typing rules of CIC.
-
-The element <instantiate> correspond to the application of an explicit named
-substitution to its first argument, that is a reference to a definition
-or declaration in the environment.
-
-All the other elements are just syntactic sugar.
+If you were looking for it, try contacting Claudio Sacerdoti-Coen, its original
+author, at sacerdot@cs.unibo.it. He had a working version in the past.
diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
deleted file mode 100644
index da7e57766..000000000
--- a/plugins/xml/acic.ml
+++ /dev/null
@@ -1,108 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-open Names
-open Term
-
-(* Maps fron \em{unshared} [constr] to ['a]. *)
-module CicHash =
- Hashtbl.Make
- (struct
- type t = Term.constr
- let equal = (==)
- let hash = Hashtbl.hash
- end)
-;;
-
-type id = string (* the type of the (annotated) node identifiers *)
-type uri = string
-
-type 'constr context_entry =
- Decl of 'constr (* Declaration *)
- | Def of 'constr * 'constr (* Definition; the second argument (the type) *)
- (* is not present in the DTD, but is needed *)
- (* to use Coq functions during exportation. *)
-
-type 'constr hypothesis = Id.t * 'constr context_entry
-type context = constr hypothesis list
-
-type conjecture = existential_key * context * constr
-type metasenv = conjecture list
-
-(* list of couples section path -- variables defined in that section *)
-type params = (string * uri list) list
-
-type obj =
- Constant of string * (* id, *)
- constr option * constr * (* value, type, *)
- params (* parameters *)
- | Variable of
- string * constr option * constr * (* name, body, type *)
- params (* parameters *)
- | CurrentProof of
- string * metasenv * (* name, conjectures, *)
- constr * constr (* value, type *)
- | InductiveDefinition of
- inductiveType list * (* inductive types , *)
- params * int (* parameters,n ind. pars*)
-and inductiveType =
- Id.t * bool * constr * (* typename, inductive, arity *)
- constructor list (* constructors *)
-and constructor =
- Id.t * constr (* id, type *)
-
-type aconstr =
- | ARel of id * int * id * Id.t
- | AVar of id * uri
- | AEvar of id * existential_key * aconstr list
- | ASort of id * sorts
- | ACast of id * aconstr * aconstr
- | AProds of (id * Name.t * aconstr) list * aconstr
- | ALambdas of (id * Name.t * aconstr) list * aconstr
- | ALetIns of (id * Name.t * aconstr) list * aconstr
- | AApp of id * aconstr list
- | AConst of id * explicit_named_substitution * uri
- | AInd of id * explicit_named_substitution * uri * int
- | AConstruct of id * explicit_named_substitution * uri * int * int
- | ACase of id * uri * int * aconstr * aconstr * aconstr list
- | AFix of id * int * ainductivefun list
- | ACoFix of id * int * acoinductivefun list
-and ainductivefun =
- id * Id.t * int * aconstr * aconstr
-and acoinductivefun =
- id * Id.t * aconstr * aconstr
-and explicit_named_substitution = id option * (uri * aconstr) list
-
-type acontext = (id * aconstr hypothesis) list
-type aconjecture = id * existential_key * acontext * aconstr
-type ametasenv = aconjecture list
-
-type aobj =
- AConstant of id * string * (* id, *)
- aconstr option * aconstr * (* value, type, *)
- params (* parameters *)
- | AVariable of id *
- string * aconstr option * aconstr * (* name, body, type *)
- params (* parameters *)
- | ACurrentProof of id *
- string * ametasenv * (* name, conjectures, *)
- aconstr * aconstr (* value, type *)
- | AInductiveDefinition of id *
- anninductiveType list * (* inductive types , *)
- params * int (* parameters,n ind. pars*)
-and anninductiveType =
- id * Id.t * bool * aconstr * (* typename, inductive, arity *)
- annconstructor list (* constructors *)
-and annconstructor =
- Id.t * aconstr (* id, type *)
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
deleted file mode 100644
index 73f113d6a..000000000
--- a/plugins/xml/acic2Xml.ml4
+++ /dev/null
@@ -1,363 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(*CSC codice cut & paste da cicPp e xmlcommand *)
-
-exception ImpossiblePossible;;
-exception NotImplemented;;
-let dtdname = "http://mowgli.cs.unibo.it/dtd/cic.dtd";;
-let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";;
-
-let rec find_last_id =
- function
- [] -> Errors.anomaly ~label:"find_last_id" (Pp.str "empty list")
- | [id,_,_] -> id
- | _::tl -> find_last_id tl
-;;
-
-let export_existential ev = string_of_int (Evar.repr ev)
-
-let print_term ids_to_inner_sorts =
- let rec aux =
- let module A = Acic in
- let module N = Names in
- let module X = Xml in
- function
- A.ARel (id,n,idref,b) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "REL"
- ["value",(string_of_int n) ; "binder",(N.Id.to_string b) ;
- "id",id ; "idref",idref; "sort",sort]
- | A.AVar (id,uri) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort]
- | A.AEvar (id,n,l) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "META"
- ["no",(export_existential n) ; "id",id ; "sort",sort]
- (List.fold_left
- (fun i t ->
- [< i ; X.xml_nempty "substitution" [] (aux t) >]
- ) [< >] (List.rev l))
- | A.ASort (id,s) ->
- let string_of_sort =
- match Term.family_of_sort s with
- Term.InProp -> "Prop"
- | Term.InSet -> "Set"
- | Term.InType -> "Type"
- in
- X.xml_empty "SORT" ["value",string_of_sort ; "id",id]
- | A.AProds (prods,t) ->
- let last_id = find_last_id prods in
- let sort = Hashtbl.find ids_to_inner_sorts last_id in
- X.xml_nempty "PROD" ["type",sort]
- [< List.fold_left
- (fun i (id,binder,s) ->
- let sort =
- Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
- in
- let attrs =
- ("id",id)::("type",sort)::
- match binder with
- Names.Anonymous -> []
- | Names.Name b -> ["binder",Names.Id.to_string b]
- in
- [< X.xml_nempty "decl" attrs (aux s) ; i >]
- ) [< >] prods ;
- X.xml_nempty "target" [] (aux t)
- >]
- | A.ACast (id,v,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "CAST" ["id",id ; "sort",sort]
- [< X.xml_nempty "term" [] (aux v) ;
- X.xml_nempty "type" [] (aux t)
- >]
- | A.ALambdas (lambdas,t) ->
- let last_id = find_last_id lambdas in
- let sort = Hashtbl.find ids_to_inner_sorts last_id in
- X.xml_nempty "LAMBDA" ["sort",sort]
- [< List.fold_left
- (fun i (id,binder,s) ->
- let sort =
- Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
- in
- let attrs =
- ("id",id)::("type",sort)::
- match binder with
- Names.Anonymous -> []
- | Names.Name b -> ["binder",Names.Id.to_string b]
- in
- [< X.xml_nempty "decl" attrs (aux s) ; i >]
- ) [< >] lambdas ;
- X.xml_nempty "target" [] (aux t)
- >]
- | A.ALetIns (letins,t) ->
- let last_id = find_last_id letins in
- let sort = Hashtbl.find ids_to_inner_sorts last_id in
- X.xml_nempty "LETIN" ["sort",sort]
- [< List.fold_left
- (fun i (id,binder,s) ->
- let sort =
- Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
- in
- let attrs =
- ("id",id)::("sort",sort)::
- match binder with
- Names.Anonymous -> assert false
- | Names.Name b -> ["binder",Names.Id.to_string b]
- in
- [< X.xml_nempty "def" attrs (aux s) ; i >]
- ) [< >] letins ;
- X.xml_nempty "target" [] (aux t)
- >]
- | A.AApp (id,li) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "APPLY" ["id",id ; "sort",sort]
- [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li)
- >]
- | A.AConst (id,subst,uri) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- let attrs = ["uri", uri ; "id",id ; "sort",sort] in
- aux_subst (X.xml_empty "CONST" attrs) subst
- | A.AInd (id,subst,uri,i) ->
- let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in
- aux_subst (X.xml_empty "MUTIND" attrs) subst
- | A.AConstruct (id,subst,uri,i,j) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- let attrs =
- ["uri", uri ;
- "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
- "id",id ; "sort",sort]
- in
- aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst
- | A.ACase (id,uri,typeno,ty,te,patterns) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "MUTCASE"
- ["uriType", uri ;
- "noType", (string_of_int typeno) ;
- "id", id ; "sort",sort]
- [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
- X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
- List.fold_left
- (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >])
- [<>] patterns
- >]
- | A.AFix (id, no, funs) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "FIX"
- ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
- [< List.fold_left
- (fun i (id,fi,ai,ti,bi) ->
- [< i ;
- X.xml_nempty "FixFunction"
- ["id",id ; "name", (Names.Id.to_string fi) ;
- "recIndex", (string_of_int ai)]
- [< X.xml_nempty "type" [] [< aux ti >] ;
- X.xml_nempty "body" [] [< aux bi >]
- >]
- >]
- ) [<>] funs
- >]
- | A.ACoFix (id,no,funs) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "COFIX"
- ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
- [< List.fold_left
- (fun i (id,fi,ti,bi) ->
- [< i ;
- X.xml_nempty "CofixFunction"
- ["id",id ; "name", Names.Id.to_string fi]
- [< X.xml_nempty "type" [] [< aux ti >] ;
- X.xml_nempty "body" [] [< aux bi >]
- >]
- >]
- ) [<>] funs
- >]
- and aux_subst target (id,subst) =
- if subst = [] then
- target
- else
- Xml.xml_nempty "instantiate"
- (match id with None -> [] | Some id -> ["id",id])
- [< target ;
- List.fold_left
- (fun i (uri,arg) ->
- [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >]
- ) [<>] subst
- >]
- in
- aux
-;;
-
-let param_attribute_of_params params =
- List.fold_right
- (fun (path,l) i ->
- List.fold_right
- (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i'
- ) l "" ^ match i with "" -> "" | i' -> " " ^ i'
- ) params ""
-;;
-
-let print_object uri ids_to_inner_sorts =
- let aux =
- let module A = Acic in
- let module X = Xml in
- function
- A.ACurrentProof (id,n,conjectures,bo,ty) ->
- let xml_for_current_proof_body =
-(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
-(*CSC: I think so. Not implemented yet. *)
- X.xml_nempty "CurrentProof" ["of",uri ; "id", id]
- [< List.fold_left
- (fun i (cid,n,canonical_context,t) ->
- [< i ;
- X.xml_nempty "Conjecture"
- ["id", cid ; "no",export_existential n]
- [< List.fold_left
- (fun i (hid,t) ->
- [< (match t with
- n,A.Decl t ->
- X.xml_nempty "Decl"
- ["id",hid;"name",Names.Id.to_string n]
- (print_term ids_to_inner_sorts t)
- | n,A.Def (t,_) ->
- X.xml_nempty "Def"
- ["id",hid;"name",Names.Id.to_string n]
- (print_term ids_to_inner_sorts t)
- ) ;
- i
- >]
- ) [< >] canonical_context ;
- X.xml_nempty "Goal" []
- (print_term ids_to_inner_sorts t)
- >]
- >])
- [<>] (List.rev conjectures) ;
- X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
- in
- let xml_for_current_proof_type =
- X.xml_nempty "ConstantType" ["name",n ; "id", id]
- (print_term ids_to_inner_sorts ty)
- in
- let xmlbo =
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
- xml_for_current_proof_body
- >] in
- let xmlty =
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata
- ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
- xml_for_current_proof_type
- >]
- in
- xmlty, Some xmlbo
- | A.AConstant (id,n,bo,ty,params) ->
- let params' = param_attribute_of_params params in
- let xmlbo =
- match bo with
- None -> None
- | Some bo ->
- Some
- [< X.xml_cdata
- "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata
- ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
- X.xml_nempty "ConstantBody"
- ["for",uri ; "params",params' ; "id", id]
- [< print_term ids_to_inner_sorts bo >]
- >]
- in
- let xmlty =
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
- X.xml_nempty "ConstantType"
- ["name",n ; "params",params' ; "id", id]
- [< print_term ids_to_inner_sorts ty >]
- >]
- in
- xmlty, xmlbo
- | A.AVariable (id,n,bo,ty,params) ->
- let params' = param_attribute_of_params params in
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n") ;
- X.xml_nempty "Variable" ["name",n ; "params",params' ; "id", id]
- [< (match bo with
- None -> [<>]
- | Some bo ->
- X.xml_nempty "body" []
- (print_term ids_to_inner_sorts bo)
- ) ;
- X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
- >]
- >], None
- | A.AInductiveDefinition (id,tys,params,nparams) ->
- let params' = param_attribute_of_params params in
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
- dtdname ^ "\">\n") ;
- X.xml_nempty "InductiveDefinition"
- ["noParams",string_of_int nparams ;
- "id",id ;
- "params",params']
- [< (List.fold_left
- (fun i (id,typename,finite,arity,cons) ->
- [< i ;
- X.xml_nempty "InductiveType"
- ["id",id ; "name",Names.Id.to_string typename ;
- "inductive",(string_of_bool finite)
- ]
- [< X.xml_nempty "arity" []
- (print_term ids_to_inner_sorts arity) ;
- (List.fold_left
- (fun i (name,lc) ->
- [< i ;
- X.xml_nempty "Constructor"
- ["name",Names.Id.to_string name]
- (print_term ids_to_inner_sorts lc)
- >]) [<>] cons
- )
- >]
- >]
- ) [< >] tys
- )
- >]
- >], None
- in
- aux
-;;
-
-let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
- let module C2A = Cic2acic in
- let module X = Xml in
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^"\">\n");
- X.xml_nempty "InnerTypes" ["of",curi]
- (Hashtbl.fold
- (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
- [< x ;
- X.xml_nempty "TYPE" ["of",id]
- [< X.xml_nempty "synthesized" []
- (print_term ids_to_inner_sorts synty) ;
- match expty with
- None -> [<>]
- | Some expty' ->
- X.xml_nempty "expected" []
- (print_term ids_to_inner_sorts expty')
- >]
- >]
- ) ids_to_inner_types [<>]
- )
- >]
-;;
diff --git a/plugins/xml/cic.dtd b/plugins/xml/cic.dtd
deleted file mode 100644
index c8035cab9..000000000
--- a/plugins/xml/cic.dtd
+++ /dev/null
@@ -1,259 +0,0 @@
-<?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;>
diff --git a/plugins/xml/cic2Xml.ml b/plugins/xml/cic2Xml.ml
deleted file mode 100644
index 981503a66..000000000
--- a/plugins/xml/cic2Xml.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-let print_xml_term ch env sigma cic =
- let ids_to_terms = Hashtbl.create 503 in
- let constr_to_ids = Acic.CicHash.create 503 in
- let ids_to_father_ids = Hashtbl.create 503 in
- let ids_to_inner_sorts = Hashtbl.create 503 in
- let ids_to_inner_types = Hashtbl.create 503 in
- let seed = ref 0 in
- let acic =
- Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids
- ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
- env [] sigma (Unshare.unshare cic) None in
- let xml = Acic2Xml.print_term ids_to_inner_sorts acic in
- Xml.pp_ch xml ch
-;;
-
-Tacinterp.declare_xml_printer print_xml_term
-;;
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
deleted file mode 100644
index bbaef1e70..000000000
--- a/plugins/xml/cic2acic.ml
+++ /dev/null
@@ -1,927 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-open Pp
-open Util
-open Names
-
-(* Utility Functions *)
-
-exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
-let get_module_path_of_full_path path =
- let dirpath = fst (Libnames.repr_path path) in
- let modules = Lib.library_dp () :: (Library.loaded_libraries ()) in
- match
- List.filter
- (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
- with
- [] ->
- Pp.msg_warning (Pp.str ("Modules not supported: reference to "^
- Libnames.string_of_path path^" will be wrong"));
- dirpath
- | [modul] -> modul
- | _ ->
- raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
-;;
-
-(*CSC: Problem: here we are using the wrong (???) hypothesis that there do *)
-(*CSC: not exist two modules whose dir_paths are one a prefix of the other *)
-let remove_module_dirpath_from_dirpath ~basedir dir =
- if Libnames.is_dirpath_prefix_of basedir dir then
- let ids = DirPath.repr dir in
- let rec remove_firsts n l =
- match n,l with
- (0,l) -> l
- | (n,he::tl) -> remove_firsts (n-1) tl
- | _ -> assert false
- in
- let ids' =
- List.rev
- (remove_firsts
- (List.length (DirPath.repr basedir))
- (List.rev ids))
- in
- ids'
- else DirPath.repr dir
-;;
-
-
-let get_uri_of_var v pvars =
- let rec search_in_open_sections =
- function
- [] -> Errors.error ("Variable "^v^" not found")
- | he::tl as modules ->
- let dirpath = DirPath.make modules in
- if Id.List.mem (Id.of_string v) (Decls.last_section_hyps dirpath)
- then
- modules
- else
- search_in_open_sections tl
- in
- let path =
- if String.List.mem v pvars then
- []
- else
- search_in_open_sections (DirPath.repr (Lib.cwd ()))
- in
- "cic:" ^
- List.fold_left
- (fun i x -> "/" ^ Id.to_string x ^ i) "" path
-;;
-
-type tag =
- Constant of Names.constant
- | Inductive of Names.mutual_inductive
- | Variable of Names.kernel_name
-;;
-
-type etag =
- TConstant
- | TInductive
- | TVariable
-;;
-
-let etag_of_tag =
- function
- Constant _ -> TConstant
- | Inductive _ -> TInductive
- | Variable _ -> TVariable
-
-let ext_of_tag =
- function
- TConstant -> "con"
- | TInductive -> "ind"
- | TVariable -> "var"
-;;
-
-exception FunctorsXMLExportationNotImplementedYet;;
-
-let subtract l1 l2 =
- let l1' = List.rev (DirPath.repr l1) in
- let l2' = List.rev (DirPath.repr l2) in
- let rec aux =
- function
- he::tl when tl = l2' -> [he]
- | he::tl -> he::(aux tl)
- | [] -> assert (l2' = []) ; []
- in
- DirPath.make (List.rev (aux l1'))
-;;
-
-let token_list_of_path dir id tag =
- let token_list_of_dirpath dirpath =
- List.rev_map Id.to_string (DirPath.repr dirpath) in
- token_list_of_dirpath dir @ [Id.to_string id ^ "." ^ (ext_of_tag tag)]
-
-let token_list_of_kernel_name tag =
- let id,dir = match tag with
- | Variable kn ->
- Label.to_id (Names.label kn), Lib.cwd ()
- | Constant con ->
- Label.to_id (Names.con_label con),
- Lib.remove_section_part (Globnames.ConstRef con)
- | Inductive kn ->
- Label.to_id (Names.mind_label kn),
- Lib.remove_section_part (Globnames.IndRef (kn,0))
- in
- token_list_of_path dir id (etag_of_tag tag)
-;;
-
-let uri_of_kernel_name tag =
- let tokens = token_list_of_kernel_name tag in
- "cic:/" ^ String.concat "/" tokens
-
-let uri_of_declaration id tag =
- let dir = Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in
- let tokens = token_list_of_path dir id tag in
- "cic:/" ^ String.concat "/" tokens
-
-(* Special functions for handling of CCorn's CProp "sort" *)
-
-type sort =
- Coq_sort of Term.sorts_family
- | CProp
-;;
-
-let prerr_endline _ = ();;
-
-let family_of_term ty =
- match Term.kind_of_term ty with
- Term.Sort s -> Coq_sort (Term.family_of_sort s)
- | Term.Const _ -> CProp (* I could check that the constant is CProp *)
- | _ -> Errors.anomaly (Pp.str "family_of_term")
-;;
-
-module CPropRetyping =
- struct
- module T = Term
- module V = Vars
-
- let outsort env sigma t =
- family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t)
-
- let rec subst_type env sigma typ = function
- | [] -> typ
- | h::rest ->
- match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
- | T.Prod (na,c1,c2) -> subst_type env sigma (V.subst1 h c2) rest
- | _ -> Errors.anomaly (Pp.str "Non-functional construction")
-
-
- let sort_of_atomic_type env sigma ft args =
- let rec concl_of_arity env ar =
- match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma ar) with
- | T.Prod (na, t, b) -> concl_of_arity (Environ.push_rel (na,None,t) env) b
- | T.Sort s -> Coq_sort (T.family_of_sort s)
- | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
- in concl_of_arity env ft
-
-let typeur sigma metamap =
- let rec type_of env cstr=
- match Term.kind_of_term cstr with
- | T.Proj _ -> assert false
- | T.Meta n ->
- (try T.strip_outer_cast (Int.List.assoc n metamap)
- with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
- | T.Rel n ->
- let (_,_,ty) = Environ.lookup_rel n env in
- V.lift n ty
- | T.Var id ->
- (try
- let (_,_,ty) = Environ.lookup_named id env in
- ty
- with Not_found ->
- Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound"))
- | T.Const c -> Typeops.type_of_constant_in env c
- | T.Evar ev -> Evd.existential_type sigma ev
- | T.Ind ind -> Inductiveops.type_of_inductive env ind
- | T.Construct cstr -> Inductiveops.type_of_constructor env cstr
- | T.Case (_,p,c,lf) ->
- let Inductiveops.IndType(_,realargs) =
- try Inductiveops.find_rectype env sigma (type_of env c)
- with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in
- let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
- (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
- | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
- | _ -> t)
- | T.Lambda (name,c1,c2) ->
- T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
- | T.LetIn (name,b,c1,c2) ->
- V.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2)
- | T.Fix ((_,i),(_,tys,_)) -> tys.(i)
- | T.CoFix (i,(_,tys,_)) -> tys.(i)
- | T.App(f,args)->
- T.strip_outer_cast
- (subst_type env sigma (type_of env f) (Array.to_list args))
- | T.Cast (c,_, t) -> t
- | T.Sort _ | T.Prod _ ->
- match sort_of env cstr with
- Coq_sort T.InProp -> T.mkProp
- | Coq_sort T.InSet -> T.mkSet
- | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *)
- | CProp -> T.mkConst DoubleTypeInference.cprop
-
- and sort_of env t =
- match Term.kind_of_term t with
- | T.Cast (c,_, s) when T.isSort s -> family_of_term s
- | T.Sort (T.Prop c) -> Coq_sort T.InType
- | T.Sort (T.Type u) -> Coq_sort T.InType
- | T.Prod (name,t,c2) ->
- (match sort_of env t,sort_of (Environ.push_rel (name,None,t) env) c2 with
- | _, (Coq_sort T.InProp as s) -> s
- | Coq_sort T.InProp, (Coq_sort T.InSet as s)
- | Coq_sort T.InSet, (Coq_sort T.InSet as s) -> s
- | Coq_sort T.InType, (Coq_sort T.InSet as s)
- | CProp, (Coq_sort T.InSet as s) when
- Environ.engagement env = Some Declarations.ImpredicativeSet -> s
- | Coq_sort T.InType, Coq_sort T.InSet
- | CProp, Coq_sort T.InSet -> Coq_sort T.InType
- | _, (Coq_sort T.InType as s) -> s (*Type Univ.dummy_univ*)
- | _, (CProp as s) -> s)
- | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
- | T.Lambda _ | T.Fix _ | T.Construct _ ->
- Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)")
- | _ -> outsort env sigma (type_of env t)
-
- and sort_family_of env t =
- match T.kind_of_term t with
- | T.Cast (c,_, s) when T.isSort s -> family_of_term s
- | T.Sort (T.Prop c) -> Coq_sort T.InType
- | T.Sort (T.Type u) -> Coq_sort T.InType
- | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2
- | T.App(f,args) ->
- sort_of_atomic_type env sigma (type_of env f) args
- | T.Lambda _ | T.Fix _ | T.Construct _ ->
- Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)")
- | _ -> outsort env sigma (type_of env t)
-
- in type_of, sort_of, sort_family_of
-
- let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c
- let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c
-
- end
-;;
-
-let get_sort_family_of env evar_map ty =
- CPropRetyping.get_sort_family_of env evar_map ty
-;;
-
-let type_as_sort env evar_map ty =
-(* CCorn code *)
- family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env evar_map ty)
-;;
-
-let is_a_Prop =
- function
- "Prop"
- | "CProp" -> true
- | _ -> false
-;;
-
-(* Main Functions *)
-
-type anntypes =
- {annsynthesized : Acic.aconstr ; annexpected : Acic.aconstr option}
-;;
-
-let gen_id seed =
- let res = "i" ^ string_of_int !seed in
- incr seed ;
- res
-;;
-
-let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids =
- fun father t ->
- let res = gen_id seed in
- Hashtbl.add ids_to_father_ids res father ;
- Hashtbl.add ids_to_terms res t ;
- Acic.CicHash.add constr_to_ids t res ;
- res
-;;
-
-let source_id_of_id id = "#source#" ^ id;;
-
-let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
- ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
- ?(fake_dependent_products=false) env idrefs evar_map t expectedty
-=
- let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in
- (* CSC: do you have any reasonable substitute for 503? *)
- let terms_to_types = Acic.CicHash.create 503 in
- DoubleTypeInference.double_type_of env evar_map t expectedty terms_to_types ;
- let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env
- idrefs ?(subst=None,[]) tt
- =
- let fresh_id'' = fresh_id' father tt in
- let aux' = aux computeinnertypes (Some fresh_id'') [] in
- let string_of_sort_family =
- function
- Coq_sort Term.InProp -> "Prop"
- | Coq_sort Term.InSet -> "Set"
- | Coq_sort Term.InType -> "Type"
- | CProp -> "CProp"
- in
- let string_of_sort t =
- string_of_sort_family
- (type_as_sort env evar_map t)
- in
- let ainnertypes,innertype,innersort,expected_available =
- let {DoubleTypeInference.synthesized = synthesized;
- DoubleTypeInference.expected = expected} =
- if computeinnertypes then
-try
- Acic.CicHash.find terms_to_types tt
-with e when Errors.noncritical e ->
-(*CSC: Warning: it really happens, for example in Ring_theory!!! *)
-Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
- else
- (* We are already in an inner-type and Coscoy's double *)
- (* type inference algorithm has not been applied. *)
- (* We need to refresh the universes because we are doing *)
- (* type inference on an already inferred type. *)
- {DoubleTypeInference.synthesized =
- Reductionops.nf_beta evar_map
- (CPropRetyping.get_type_of env evar_map
- ((* Termops.refresh_universes *) tt)) ;
- DoubleTypeInference.expected = None}
- in
- let innersort =
- let synthesized_innersort =
- get_sort_family_of env evar_map synthesized
- in
- match expected with
- None -> synthesized_innersort
- | Some ty ->
- let expected_innersort =
- get_sort_family_of env evar_map ty
- in
- match expected_innersort, synthesized_innersort with
- CProp, _
- | _, CProp -> CProp
- | _, _ -> expected_innersort
- in
-(* Debugging only:
-print_endline "PASSATO" ; flush stdout ;
-*)
- let ainnertypes,expected_available =
- if computeinnertypes then
- let annexpected,expected_available =
- match expected with
- None -> None,false
- | Some expectedty' ->
- Some (aux false (Some fresh_id'') [] env idrefs expectedty'),
- true
- in
- Some
- {annsynthesized =
- aux false (Some fresh_id'') [] env idrefs synthesized ;
- annexpected = annexpected
- }, expected_available
- else
- None,false
- in
- ainnertypes,synthesized, string_of_sort_family innersort,
- expected_available
- in
- let add_inner_type id =
- match ainnertypes with
- None -> ()
- | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes
- in
-
- (* explicit_substitute_and_eta_expand_if_required h t t' *)
- (* where [t] = [] and [tt] = [h]{[t']} ("{.}" denotes explicit *)
- (* named substitution) or [tt] = (App [h]::[t]) (and [t'] = []) *)
- (* check if [h] is a term that requires an explicit named *)
- (* substitution and, in that case, uses the first arguments of *)
- (* [t] as the actual arguments of the substitution. If there *)
- (* are not enough parameters in the list [t], then eta-expansion *)
- (* is performed. *)
- let
- explicit_substitute_and_eta_expand_if_required h t t'
- compute_result_if_eta_expansion_not_required
- =
- let subst,residual_args,uninst_vars =
- let variables,basedir =
- try
- let g = Globnames.global_of_constr h in
- let sp =
- match g with
- Globnames.ConstructRef ((induri,_),_)
- | Globnames.IndRef (induri,_) ->
- Nametab.path_of_global (Globnames.IndRef (induri,0))
- | Globnames.VarRef id ->
- (* Invariant: variables are never cooked in Coq *)
- raise Not_found
- | _ -> Nametab.path_of_global g
- in
- Dischargedhypsmap.get_discharged_hyps sp,
- get_module_path_of_full_path sp
- with Not_found ->
- (* no explicit substitution *)
- [], Libnames.dirpath_of_string "dummy"
- in
- (* returns a triple whose first element is *)
- (* an explicit named substitution of "type" *)
- (* (variable * argument) list, whose *)
- (* second element is the list of residual *)
- (* arguments and whose third argument is *)
- (* the list of uninstantiated variables *)
- let rec get_explicit_subst variables arguments =
- match variables,arguments with
- [],_ -> [],arguments,[]
- | _,[] -> [],[],variables
- | he1::tl1,he2::tl2 ->
- let subst,extra_args,uninst = get_explicit_subst tl1 tl2 in
- let (he1_sp, he1_id) = Libnames.repr_path he1 in
- let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in
- let he1'' =
- String.concat "/"
- (List.rev_map Id.to_string he1') ^ "/"
- ^ (Id.to_string he1_id) ^ ".var"
- in
- (he1'',he2)::subst, extra_args, uninst
- in
- get_explicit_subst variables t'
- in
- let uninst_vars_length = List.length uninst_vars in
- if uninst_vars_length > 0 then
- (* Not enough arguments provided. We must eta-expand! *)
- let un_args,_ =
- Term.decompose_prod_n uninst_vars_length
- (CPropRetyping.get_type_of env evar_map tt)
- in
- let eta_expanded =
- let arguments =
- List.map (Vars.lift uninst_vars_length) t @
- Termops.rel_list 0 uninst_vars_length
- in
- Unshare.unshare
- (Term.lamn uninst_vars_length un_args
- (Term.applistc h arguments))
- in
- DoubleTypeInference.double_type_of env evar_map eta_expanded
- None terms_to_types ;
- Hashtbl.remove ids_to_inner_types fresh_id'' ;
- aux' env idrefs eta_expanded
- else
- compute_result_if_eta_expansion_not_required subst residual_args
- in
-
- (* Now that we have all the auxiliary functions we *)
- (* can finally proceed with the main case analysis. *)
- match Term.kind_of_term tt with
- | Term.Proj _ -> assert false
- | Term.Rel n ->
- let id =
- match List.nth (Environ.rel_context env) (n - 1) with
- (Names.Name id,_,_) -> id
- | (Names.Anonymous,_,_) -> Nameops.make_ident "_" None
- in
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort && expected_available then
- add_inner_type fresh_id'' ;
- Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
- | Term.Var id ->
- let pvars = Termops.ids_of_named_context (Environ.named_context env) in
- let pvars = List.map Id.to_string pvars in
- let path = get_uri_of_var (Id.to_string id) pvars in
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort && expected_available then
- add_inner_type fresh_id'' ;
- Acic.AVar
- (fresh_id'', path ^ "/" ^ (Id.to_string id) ^ ".var")
- | Term.Evar (n,l) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort && expected_available then
- add_inner_type fresh_id'' ;
- Acic.AEvar
- (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
- | Term.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML")
- | Term.Sort s -> Acic.ASort (fresh_id'', s)
- | Term.Cast (v,_, t) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort then
- add_inner_type fresh_id'' ;
- Acic.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t)
- | Term.Prod (n,s,t) ->
- let n' =
- match n with
- Names.Anonymous -> Names.Anonymous
- | _ ->
- if not fake_dependent_products && Vars.noccurn 1 t then
- Names.Anonymous
- else
- Names.Name
- (Namegen.next_name_away n (Termops.ids_of_context env))
- in
- Hashtbl.add ids_to_inner_sorts fresh_id''
- (string_of_sort innertype) ;
- let sourcetype = CPropRetyping.get_type_of env evar_map s in
- Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
- (string_of_sort sourcetype) ;
- let new_passed_prods =
- let father_is_prod =
- match father with
- None -> false
- | Some father' ->
- match
- Term.kind_of_term (Hashtbl.find ids_to_terms father')
- with
- Term.Prod _ -> true
- | _ -> false
- in
- (fresh_id'', n', aux' env idrefs s)::
- (if father_is_prod then
- passed_lambdas_or_prods_or_letins
- else [])
- in
- let new_env = Environ.push_rel (n', None, s) env in
- let new_idrefs = fresh_id''::idrefs in
- (match Term.kind_of_term t with
- Term.Prod _ ->
- aux computeinnertypes (Some fresh_id'') new_passed_prods
- new_env new_idrefs t
- | _ ->
- Acic.AProds (new_passed_prods, aux' new_env new_idrefs t))
- | Term.Lambda (n,s,t) ->
- let n' =
- match n with
- Names.Anonymous -> Names.Anonymous
- | _ ->
- Names.Name (Namegen.next_name_away n (Termops.ids_of_context env))
- in
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- let sourcetype = CPropRetyping.get_type_of env evar_map s in
- Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
- (string_of_sort sourcetype) ;
- let father_is_lambda =
- match father with
- None -> false
- | Some father' ->
- match
- Term.kind_of_term (Hashtbl.find ids_to_terms father')
- with
- Term.Lambda _ -> true
- | _ -> false
- in
- if is_a_Prop innersort &&
- ((not father_is_lambda) || expected_available)
- then add_inner_type fresh_id'' ;
- let new_passed_lambdas =
- (fresh_id'',n', aux' env idrefs s)::
- (if father_is_lambda then
- passed_lambdas_or_prods_or_letins
- else []) in
- let new_env = Environ.push_rel (n', None, s) env in
- let new_idrefs = fresh_id''::idrefs in
- (match Term.kind_of_term t with
- Term.Lambda _ ->
- aux computeinnertypes (Some fresh_id'') new_passed_lambdas
- new_env new_idrefs t
- | _ ->
- let t' = aux' new_env new_idrefs t in
- (* eta-expansion for explicit named substitutions *)
- (* can create nested Lambdas. Here we perform the *)
- (* flattening. *)
- match t' with
- Acic.ALambdas (lambdas, t'') ->
- Acic.ALambdas (lambdas@new_passed_lambdas, t'')
- | _ ->
- Acic.ALambdas (new_passed_lambdas, t')
- )
- | Term.LetIn (n,s,t,d) ->
- let id =
- match n with
- Names.Anonymous -> Id.of_string "_X"
- | Names.Name id -> id
- in
- let n' =
- Names.Name (Namegen.next_ident_away id (Termops.ids_of_context env))
- in
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- let sourcesort =
- get_sort_family_of env evar_map
- (CPropRetyping.get_type_of env evar_map s)
- in
- Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
- (string_of_sort_family sourcesort) ;
- let father_is_letin =
- match father with
- None -> false
- | Some father' ->
- match
- Term.kind_of_term (Hashtbl.find ids_to_terms father')
- with
- Term.LetIn _ -> true
- | _ -> false
- in
- if is_a_Prop innersort then
- add_inner_type fresh_id'' ;
- let new_passed_letins =
- (fresh_id'',n', aux' env idrefs s)::
- (if father_is_letin then
- passed_lambdas_or_prods_or_letins
- else []) in
- let new_env = Environ.push_rel (n', Some s, t) env in
- let new_idrefs = fresh_id''::idrefs in
- (match Term.kind_of_term d with
- Term.LetIn _ ->
- aux computeinnertypes (Some fresh_id'') new_passed_letins
- new_env new_idrefs d
- | _ -> Acic.ALetIns
- (new_passed_letins, aux' new_env new_idrefs d))
- | Term.App (h,t) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort then
- add_inner_type fresh_id'' ;
- let
- compute_result_if_eta_expansion_not_required subst residual_args
- =
- let residual_args_not_empty = residual_args <> [] in
- let h' =
- if residual_args_not_empty then
- aux' env idrefs ~subst:(None,subst) h
- else
- aux' env idrefs ~subst:(Some fresh_id'',subst) h
- in
- (* maybe all the arguments were used for the explicit *)
- (* named substitution *)
- if residual_args_not_empty then
- Acic.AApp (fresh_id'', h'::residual_args)
- else
- h'
- in
- let t' =
- Array.fold_right (fun x i -> (aux' env idrefs x)::i) t []
- in
- explicit_substitute_and_eta_expand_if_required h
- (Array.to_list t) t'
- compute_result_if_eta_expansion_not_required
- | Term.Const (kn,u) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort && expected_available then
- add_inner_type fresh_id'' ;
- let compute_result_if_eta_expansion_not_required _ _ =
- Acic.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn)))
- in
- let (_,subst') = subst in
- explicit_substitute_and_eta_expand_if_required tt []
- (List.map snd subst')
- compute_result_if_eta_expansion_not_required
- | Term.Ind ((kn,i),u) ->
- let compute_result_if_eta_expansion_not_required _ _ =
- Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
- in
- let (_,subst') = subst in
- explicit_substitute_and_eta_expand_if_required tt []
- (List.map snd subst')
- compute_result_if_eta_expansion_not_required
- | Term.Construct (((kn,i),j),u) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort && expected_available then
- add_inner_type fresh_id'' ;
- let compute_result_if_eta_expansion_not_required _ _ =
- Acic.AConstruct
- (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j)
- in
- let (_,subst') = subst in
- explicit_substitute_and_eta_expand_if_required tt []
- (List.map snd subst')
- compute_result_if_eta_expansion_not_required
- | Term.Case ({Term.ci_ind=(kn,i)},ty,term,a) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort then
- add_inner_type fresh_id'' ;
- let a' =
- Array.fold_right (fun x i -> (aux' env idrefs x)::i) a []
- in
- Acic.ACase
- (fresh_id'', (uri_of_kernel_name (Inductive kn)), i,
- aux' env idrefs ty, aux' env idrefs term, a')
- | Term.Fix ((ai,i),(f,t,b)) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort then add_inner_type fresh_id'' ;
- let fresh_idrefs =
- Array.init (Array.length t) (function _ -> gen_id seed) in
- let new_idrefs =
- (List.rev (Array.to_list fresh_idrefs)) @ idrefs
- in
- let f' =
- let ids = ref (Termops.ids_of_context env) in
- Array.map
- (function
- Names.Anonymous -> Errors.error "Anonymous fix function met"
- | Names.Name id as n ->
- let res = Names.Name (Namegen.next_name_away n !ids) in
- ids := id::!ids ;
- res
- ) f
- in
- Acic.AFix (fresh_id'', i,
- Array.fold_right
- (fun (id,fi,ti,bi,ai) i ->
- let fi' =
- match fi with
- Names.Name fi -> fi
- | Names.Anonymous -> Errors.error "Anonymous fix function met"
- in
- (id, fi', ai,
- aux' env idrefs ti,
- aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i)
- (Array.mapi
- (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f'
- ) []
- )
- | Term.CoFix (i,(f,t,b)) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- if is_a_Prop innersort then add_inner_type fresh_id'' ;
- let fresh_idrefs =
- Array.init (Array.length t) (function _ -> gen_id seed) in
- let new_idrefs =
- (List.rev (Array.to_list fresh_idrefs)) @ idrefs
- in
- let f' =
- let ids = ref (Termops.ids_of_context env) in
- Array.map
- (function
- Names.Anonymous -> Errors.error "Anonymous fix function met"
- | Names.Name id as n ->
- let res = Names.Name (Namegen.next_name_away n !ids) in
- ids := id::!ids ;
- res
- ) f
- in
- Acic.ACoFix (fresh_id'', i,
- Array.fold_right
- (fun (id,fi,ti,bi) i ->
- let fi' =
- match fi with
- Names.Name fi -> fi
- | Names.Anonymous -> Errors.error "Anonymous fix function met"
- in
- (id, fi',
- aux' env idrefs ti,
- aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i)
- (Array.mapi
- (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f'
- ) []
- )
- in
- aux computeinnertypes None [] env idrefs t
-;;
-
-(* Obsolete [HH 1/2009]
-let acic_of_cic_context metasenv context t =
- let ids_to_terms = Hashtbl.create 503 in
- let constr_to_ids = Acic.CicHash.create 503 in
- let ids_to_father_ids = Hashtbl.create 503 in
- let ids_to_inner_sorts = Hashtbl.create 503 in
- let ids_to_inner_types = Hashtbl.create 503 in
- let seed = ref 0 in
- acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids
- ids_to_inner_sorts ids_to_inner_types metasenv context t,
- ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
-;;
-*)
-
-let acic_object_of_cic_object sigma obj =
- let ids_to_terms = Hashtbl.create 503 in
- let constr_to_ids = Acic.CicHash.create 503 in
- let ids_to_father_ids = Hashtbl.create 503 in
- let ids_to_inner_sorts = Hashtbl.create 503 in
- let ids_to_inner_types = Hashtbl.create 503 in
- let ids_to_conjectures = Hashtbl.create 11 in
- let ids_to_hypotheses = Hashtbl.create 127 in
- let hypotheses_seed = ref 0 in
- let conjectures_seed = ref 0 in
- let seed = ref 0 in
- let acic_term_of_cic_term_context' =
- acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids
- ids_to_inner_sorts ids_to_inner_types in
-(*CSC: is this the right env to use? Hhmmm. There is a problem: in *)
-(*CSC: Global.env () the object we are exporting is already defined, *)
-(*CSC: either in the environment or in the named context (in the case *)
-(*CSC: of variables. Is this a problem? *)
- let env = Global.env () in
- let acic_term_of_cic_term' ?fake_dependent_products =
- acic_term_of_cic_term_context' ?fake_dependent_products env [] sigma in
-(*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *)
-(*CSC: a modified version of the already existent fresh_id function *)
- let fresh_id () =
- let res = "i" ^ string_of_int !seed in
- incr seed ;
- res
- in
- let aobj =
- match obj with
- Acic.Constant (id,bo,ty,params) ->
- let abo =
- match bo with
- None -> None
- | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty))
- in
- let aty = acic_term_of_cic_term' ty None in
- Acic.AConstant (fresh_id (),id,abo,aty,params)
- | Acic.Variable (id,bo,ty,params) ->
- let abo =
- match bo with
- Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
- | None -> None
- in
- let aty = acic_term_of_cic_term' ty None in
- Acic.AVariable (fresh_id (),id,abo,aty,params)
- | Acic.CurrentProof (id,conjectures,bo,ty) ->
- let aconjectures =
- List.map
- (function (i,canonical_context,term) as conjecture ->
- let cid = "c" ^ string_of_int !conjectures_seed in
- Hashtbl.add ids_to_conjectures cid conjecture ;
- incr conjectures_seed ;
- let canonical_env,idrefs',acanonical_context =
- let rec aux env idrefs =
- function
- [] -> env,idrefs,[]
- | ((n,decl_or_def) as hyp)::tl ->
- let hid = "h" ^ string_of_int !hypotheses_seed in
- let new_idrefs = hid::idrefs in
- Hashtbl.add ids_to_hypotheses hid hyp ;
- incr hypotheses_seed ;
- match decl_or_def with
- Acic.Decl t ->
- let final_env,final_idrefs,atl =
- aux (Environ.push_rel (Names.Name n,None,t) env)
- new_idrefs tl
- in
- let at =
- acic_term_of_cic_term_context' env idrefs sigma t None
- in
- final_env,final_idrefs,(hid,(n,Acic.Decl at))::atl
- | Acic.Def (t,ty) ->
- let final_env,final_idrefs,atl =
- aux
- (Environ.push_rel (Names.Name n,Some t,ty) env)
- new_idrefs tl
- in
- let at =
- acic_term_of_cic_term_context' env idrefs sigma t None
- in
- let dummy_never_used =
- let s = "dummy_never_used" in
- Acic.ARel (s,99,s,Id.of_string s)
- in
- final_env,final_idrefs,
- (hid,(n,Acic.Def (at,dummy_never_used)))::atl
- in
- aux env [] canonical_context
- in
- let aterm =
- acic_term_of_cic_term_context' canonical_env idrefs' sigma term
- None
- in
- (cid,i,List.rev acanonical_context,aterm)
- ) conjectures in
- let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in
- let aty = acic_term_of_cic_term_context' env [] sigma ty None in
- Acic.ACurrentProof (fresh_id (),id,aconjectures,abo,aty)
- | Acic.InductiveDefinition (tys,params,paramsno) ->
- let env' =
- List.fold_right
- (fun (name,_,arity,_) env ->
- Environ.push_rel (Names.Name name, None, arity) env
- ) (List.rev tys) env in
- let idrefs = List.map (function _ -> gen_id seed) tys in
- let atys =
- List.map2
- (fun id (name,inductive,ty,cons) ->
- let acons =
- List.map
- (function (name,ty) ->
- (name,
- acic_term_of_cic_term_context' ~fake_dependent_products:true
- env' idrefs Evd.empty ty None)
- ) cons
- in
- let aty =
- acic_term_of_cic_term' ~fake_dependent_products:true ty None
- in
- (id,name,inductive,aty,acons)
- ) (List.rev idrefs) tys
- in
- Acic.AInductiveDefinition (fresh_id (),atys,params,paramsno)
- in
- aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses
-;;
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
deleted file mode 100644
index c8717e008..000000000
--- a/plugins/xml/doubleTypeInference.ml
+++ /dev/null
@@ -1,266 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *)
-type types = {synthesized : Term.types ; expected : Term.types option};;
-
-let cprop =
- Names.make_con
- (Names.MPfile
- (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
- (Names.DirPath.empty)
- (Names.Label.make "CProp")
-;;
-
-let whd_betadeltaiotacprop env _evar_map ty =
- (*** CProp is made Opaque ***)
- let flags = Closure.RedFlags.red_sub Closure.betadeltaiota (Closure.RedFlags.fCONST cprop) in
- Closure.whd_val (Closure.create_clos_infos flags env) (Closure.inject ty)
-;;
-
-
-(* Code similar to the code in the Typing module, but: *)
-(* - the term is already assumed to be well typed *)
-(* - some checks have been removed *)
-(* - both the synthesized and expected types of every *)
-(* node are computed (Coscoy's double type inference) *)
-
-let assumption_of_judgment env sigma j =
- Typeops.assumption_of_judgment env (Evarutil.j_nf_evar sigma j)
-;;
-
-let type_judgment env sigma j =
- Typeops.type_judgment env (Evarutil.j_nf_evar sigma j)
-;;
-
-let type_judgment_cprop env sigma j =
- match Term.kind_of_term(whd_betadeltaiotacprop env sigma j.Environ.uj_type) with
- | Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s }
- | _ -> None (* None means the CProp constant *)
-;;
-
-let double_type_of env sigma cstr expectedty subterms_to_types =
- (*CSC: the code is inefficient because judgments are created just to be *)
- (*CSC: destroyed using Environ.j_type. Moreover I am pretty sure that the *)
- (*CSC: functions used do checks that we do not need *)
- let rec execute env sigma cstr expectedty =
- let module T = Term in
- let module V = Vars in
- let module E = Environ in
- (* the type part is the synthesized type *)
- let judgement =
- match T.kind_of_term cstr with
- T.Meta n ->
- Errors.error
- "DoubleTypeInference.double_type_of: found a non-instanciated goal"
- | T.Proj _ -> assert false
- | T.Evar ((n,l) as ev) ->
- let ty = Unshare.unshare (Evd.existential_type sigma ev) in
- let jty = execute env sigma ty None in
- let jty = assumption_of_judgment env sigma jty in
- let evar_context =
- E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in
- let rec iter actual_args evar_context =
- match actual_args,evar_context with
- [],[] -> ()
- | he1::tl1,(n,_,ty)::tl2 ->
- (* for side-effects *)
- let _ = execute env sigma he1 (Some ty) in
- let tl2' =
- List.map
- (function (m,bo,ty) ->
- (* Warning: the substitution should be performed also on bo *)
- (* This is not done since bo is not used later yet *)
- (m,bo,Unshare.unshare (V.replace_vars [n,he1] ty))
- ) tl2
- in
- iter tl1 tl2'
- | _,_ -> assert false
- in
- (* for side effects only *)
- iter (List.rev (Array.to_list l)) (List.rev evar_context) ;
- E.make_judge cstr jty
-
- | T.Rel n ->
- Typeops.judge_of_relative env n
-
- | T.Var id ->
- Typeops.judge_of_variable env id
-
- | T.Const c ->
- E.make_judge cstr (fst (Typeops.type_of_constant env c))
-
- | T.Ind ind ->
- E.make_judge cstr (Inductiveops.type_of_inductive env ind)
-
- | T.Construct cstruct ->
- E.make_judge cstr (Inductiveops.type_of_constructor env cstruct)
-
- | T.Case (ci,p,c,lf) ->
- let expectedtype =
- Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in
- let cj = execute env sigma c (Some expectedtype) in
- let pj = execute env sigma p None in
- let (expectedtypes,_) =
- let indspec = Inductive.find_rectype env cj.Environ.uj_type in
- Inductive.type_case_branches env indspec pj cj.Environ.uj_val
- in
- let lfj =
- execute_array env sigma lf
- (Array.map (function x -> Some x) expectedtypes) in
- Typeops.judge_of_case env ci pj cj lfj
-
- | T.Fix ((vn,i as vni),recdef) ->
- let (_,tys,_ as recdef') = execute_recdef env sigma recdef in
- let fix = (vni,recdef') in
- E.make_judge (T.mkFix fix) tys.(i)
-
- | T.CoFix (i,recdef) ->
- let (_,tys,_ as recdef') = execute_recdef env sigma recdef in
- let cofix = (i,recdef') in
- E.make_judge (T.mkCoFix cofix) tys.(i)
-
- | T.Sort (T.Prop c) ->
- Typeops.judge_of_prop_contents c
-
- | T.Sort (T.Type u) ->
-(*CSC: In case of need, I refresh the universe. But exportation of the *)
-(*CSC: right universe level information is destroyed. It must be changed *)
-(*CSC: again once Judicael will introduce his non-bugged algebraic *)
-(*CSC: universes. *)
-(try
- (*FIXME*) (Typeops.judge_of_type u)
- with _ -> (* Successor of a non universe-variable universe anomaly *)
- Pp.msg_warning (Pp.str "Universe refresh performed!!!");
- (*FIXME*) (Typeops.judge_of_type (Universes.new_univ Names.empty_dirpath))
-)
-
- | T.App (f,args) ->
- let expected_head =
- Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in
- let j = execute env sigma f (Some expected_head) in
- let expected_args =
- let rec aux typ =
- function
- [] -> []
- | hj::restjl ->
- match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
- T.Prod (_,c1,c2) ->
- (Some (Reductionops.nf_beta sigma c1)) ::
- (aux (V.subst1 hj c2) restjl)
- | _ -> assert false
- in
- Array.of_list (aux j.Environ.uj_type (Array.to_list args))
- in
- let jl = execute_array env sigma args expected_args in
- let j = Typeops.judge_of_apply env j jl in
- j
-
- | T.Lambda (name,c1,c2) ->
- let j = execute env sigma c1 None in
- let var = type_judgment env sigma j in
- let env1 = E.push_rel (name,None,var.E.utj_val) env in
- let expectedc2type =
- match expectedty with
- None -> None
- | Some ety ->
- match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with
- T.Prod (_,_,expected_target_type) ->
- Some (Reductionops.nf_beta sigma expected_target_type)
- | _ -> assert false
- in
- let j' = execute env1 sigma c2 expectedc2type in
- Typeops.judge_of_abstraction env1 name var j'
-
- | T.Prod (name,c1,c2) ->
- let j = execute env sigma c1 None in
- let varj = type_judgment env sigma j in
- let env1 = E.push_rel (name,None,varj.E.utj_val) env in
- let j' = execute env1 sigma c2 None in
- (match type_judgment_cprop env1 sigma j' with
- Some varj' -> Typeops.judge_of_product env name varj varj'
- | None ->
- (* CProp found *)
- { Environ.uj_val = T.mkProd (name, j.Environ.uj_val, j'.Environ.uj_val);
- Environ.uj_type = T.mkConst cprop })
-
- | T.LetIn (name,c1,c2,c3) ->
-(*CSC: What are the right expected types for the source and *)
-(*CSC: target of a LetIn? None used. *)
- let j1 = execute env sigma c1 None in
- let j2 = execute env sigma c2 None in
- let j2 = type_judgment env sigma j2 in
- let env1 =
- E.push_rel (name,Some j1.E.uj_val,j2.E.utj_val) env
- in
- let j3 = execute env1 sigma c3 None in
- Typeops.judge_of_letin env name j1 j2 j3
-
- | T.Cast (c,k,t) ->
- let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
- let tj = execute env sigma t None in
- let tj = type_judgment env sigma tj in
- let j = Typeops.judge_of_cast env cj k tj in
- j
- in
- let synthesized = E.j_type judgement in
- let synthesized' = Reductionops.nf_beta sigma synthesized in
- let types,res =
- match expectedty with
- None ->
- (* No expected type *)
- {synthesized = synthesized' ; expected = None}, synthesized
- | Some ty when Term.eq_constr synthesized' ty ->
- (* The expected type is synthactically equal to the *)
- (* synthesized type. Let's forget it. *)
- (* Note: since eq_constr is up to casts, it is better *)
- (* to keep the expected type, since it can bears casts *)
- (* that change the innersort to CProp *)
- {synthesized = ty ; expected = None}, ty
- | Some expectedty' ->
- {synthesized = synthesized' ; expected = Some expectedty'},
- expectedty'
- in
-(*CSC: debugging stuff to be removed *)
-if Acic.CicHash.mem subterms_to_types cstr then
- Pp.msg_warning (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr));
- Acic.CicHash.add subterms_to_types cstr types ;
- E.make_judge cstr res
-
-
- and execute_recdef env sigma (names,lar,vdef) =
- let length = Array.length lar in
- let larj =
- execute_array env sigma lar (Array.make length None) in
- let lara = Array.map (assumption_of_judgment env sigma) larj in
- let env1 = Environ.push_rec_types (names,lara,vdef) env in
- let expectedtypes =
- Array.map (function i -> Some (Vars.lift length i)) lar
- in
- let vdefj = execute_array env1 sigma vdef expectedtypes in
- let vdefv = Array.map Environ.j_val vdefj in
- (names,lara,vdefv)
-
- and execute_array env sigma v expectedtypes =
- let jl =
- execute_list env sigma (Array.to_list v) (Array.to_list expectedtypes)
- in
- Array.of_list jl
-
- and execute_list env sigma =
- List.map2 (execute env sigma)
-
-in
- ignore (execute env sigma cstr expectedty)
-;;
diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
deleted file mode 100644
index 5c00bdc67..000000000
--- a/plugins/xml/doubleTypeInference.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-type types = { synthesized : Term.types; expected : Term.types option; }
-
-val cprop : Names.constant
-
-val whd_betadeltaiotacprop :
- Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
-
-val double_type_of :
- Environ.env -> Evd.evar_map -> Term.constr -> Term.constr option ->
- types Acic.CicHash.t -> unit
diff --git a/plugins/xml/theoryobject.dtd b/plugins/xml/theoryobject.dtd
deleted file mode 100644
index 953fe0092..000000000
--- a/plugins/xml/theoryobject.dtd
+++ /dev/null
@@ -1,62 +0,0 @@
-<?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/. -->
-
-
-
-<!-- Notice: the markup described in this DTD is meant to be embedded -->
-<!-- in foreign markup (e.g. XHTML) -->
-
-<!ENTITY % theorystructure
- '(ht:AXIOM|ht:DEFINITION|ht:THEOREM|ht:VARIABLE|ht:SECTION|ht:MUTUAL)*'>
-
-<!ELEMENT ht:SECTION (%theorystructure;)>
-<!ATTLIST ht:SECTION
- uri CDATA #REQUIRED>
-
-<!ELEMENT ht:MUTUAL (ht:DEFINITION,ht:DEFINITION+)>
-
-<!-- Theory Items -->
-
-<!ELEMENT ht:AXIOM (Axiom)>
-<!ATTLIST ht:AXIOM
- uri CDATA #REQUIRED
- as (Axiom|Declaration) #REQUIRED>
-
-<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
-<!ATTLIST ht:DEFINITION
- uri CDATA #REQUIRED
- as (Definition|InteractiveDefinition|Inductive|CoInductive
- |Record) #REQUIRED>
-
-<!ELEMENT ht:THEOREM (type)>
-<!ATTLIST ht:THEOREM
- uri CDATA #REQUIRED
- as (Theorem|Lemma|Corollary|Fact|Remark) #REQUIRED>
-
-<!ELEMENT ht:VARIABLE (Variable)>
-<!ATTLIST ht:VARIABLE
- uri CDATA #REQUIRED
- as (Assumption|Hypothesis|LocalDefinition|LocalFact) #REQUIRED>
diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml
deleted file mode 100644
index c854427d2..000000000
--- a/plugins/xml/unshare.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-exception CanNotUnshare;;
-
-(* [unshare t] gives back a copy of t where all sharing has been removed *)
-(* Physical equality becomes meaningful on unshared terms. Hashtables that *)
-(* use physical equality can now be used to associate information to evey *)
-(* node of the term. *)
-let unshare ?(already_unshared = function _ -> false) t =
- let obj = Obj.repr t in
- let rec aux obj =
- if already_unshared (Obj.obj obj) then
- obj
- else
- (if Obj.is_int obj then
- obj
- else if Obj.is_block obj then
- begin
- let tag = Obj.tag obj in
- if tag < Obj.no_scan_tag then
- begin
- let size = Obj.size obj in
- let new_obj = Obj.new_block 0 size in
- Obj.set_tag new_obj tag ;
- for i = 0 to size - 1 do
- Obj.set_field new_obj i (aux (Obj.field obj i))
- done ;
- new_obj
- end
- else if tag = Obj.string_tag then
- obj
- else
- raise CanNotUnshare
- end
- else
- raise CanNotUnshare
- )
- in
- Obj.obj (aux obj)
-;;
diff --git a/plugins/xml/unshare.mli b/plugins/xml/unshare.mli
deleted file mode 100644
index cace2de6f..000000000
--- a/plugins/xml/unshare.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-exception CanNotUnshare;;
-
-(* [unshare t] gives back a copy of t where all sharing has been removed *)
-(* Physical equality becomes meaningful on unshared terms. Hashtables that *)
-(* use physical equality can now be used to associate information to evey *)
-(* node of the term. *)
-val unshare: ?already_unshared:('a -> bool) -> 'a -> 'a
diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4
deleted file mode 100644
index c2523755b..000000000
--- a/plugins/xml/xml.ml4
+++ /dev/null
@@ -1,78 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(* the type token for XML cdata, empty elements and not-empty elements *)
-(* Usage: *)
-(* Str cdata *)
-(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *)
-(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
-(* content *)
-type token = Str of string
- | Empty of string * (string * string) list
- | NEmpty of string * (string * string) list * token Stream.t
-;;
-
-(* currified versions of the constructors make the code more readable *)
-let xml_empty name attrs = [< 'Empty(name,attrs) >]
-let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
-let xml_cdata str = [< 'Str str >]
-
-(* Usage: *)
-(* pp tokens None pretty prints the output on stdout *)
-(* pp tokens (Some filename) pretty prints the output on the file filename *)
-let pp_ch strm channel =
- let rec pp_r m =
- parser
- [< 'Str a ; s >] ->
- print_spaces m ;
- fprint_string (a ^ "\n") ;
- pp_r m s
- | [< 'Empty(n,l) ; s >] ->
- print_spaces m ;
- fprint_string ("<" ^ n) ;
- List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
- fprint_string "/>\n" ;
- pp_r m s
- | [< 'NEmpty(n,l,c) ; s >] ->
- print_spaces m ;
- fprint_string ("<" ^ n) ;
- List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
- fprint_string ">\n" ;
- pp_r (m+1) c ;
- print_spaces m ;
- fprint_string ("</" ^ n ^ ">\n") ;
- pp_r m s
- | [< >] -> ()
- and print_spaces m =
- for _i = 1 to m do fprint_string " " done
- and fprint_string str =
- output_string channel str
- in
- pp_r 0 strm
-;;
-
-
-let pp strm fn =
- match fn with
- Some filename ->
- let filename = filename ^ ".xml" in
- let ch = open_out filename in
- pp_ch strm ch;
- close_out ch ;
- print_string ("\nWriting on file \"" ^ filename ^ "\" was successful\n");
- flush stdout
- | None ->
- pp_ch strm stdout
-;;
-
diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli
deleted file mode 100644
index 0b6d51985..000000000
--- a/plugins/xml/xml.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(* Tokens for XML cdata, empty elements and not-empty elements *)
-(* Usage: *)
-(* Str cdata *)
-(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *)
-(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
-(* content *)
-type token =
- | Str of string
- | Empty of string * (string * string) list
- | NEmpty of string * (string * string) list * token Stream.t
-
-(* currified versions of the token constructors make the code more readable *)
-val xml_empty : string -> (string * string) list -> token Stream.t
-val xml_nempty :
- string -> (string * string) list -> token Stream.t -> token Stream.t
-val xml_cdata : string -> token Stream.t
-
-val pp_ch : token Stream.t -> out_channel -> unit
-
-(* The pretty printer for streams of token *)
-(* Usage: *)
-(* pp tokens None pretty prints the output on stdout *)
-(* pp tokens (Some filename) pretty prints the output on the file filename *)
-val pp : token Stream.t -> string option -> unit
diff --git a/plugins/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib
deleted file mode 100644
index 27b0ef36f..000000000
--- a/plugins/xml/xml_plugin.mllib
+++ /dev/null
@@ -1,10 +0,0 @@
-Unshare
-Xml
-Acic
-DoubleTypeInference
-Cic2acic
-Acic2Xml
-Xmlcommand
-Xmlentries
-Cic2Xml
-Xml_plugin_mod
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
deleted file mode 100644
index d65e6f317..000000000
--- a/plugins/xml/xmlcommand.ml
+++ /dev/null
@@ -1,536 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(* CONFIGURATION PARAMETERS *)
-
-let verbose = ref false;;
-
-(* UTILITY FUNCTIONS *)
-
-let print_if_verbose s = if !verbose then print_string s;;
-
-open Decl_kinds
-open Names
-open Util
-
-(* filter_params pvars hyps *)
-(* filters out from pvars (which is a list of lists) all the variables *)
-(* that does not belong to hyps (which is a simple list) *)
-(* It returns a list of couples relative section path -- list of *)
-(* variable names. *)
-let filter_params pvars hyps =
- let rec aux ids =
- function
- [] -> []
- | (id,he)::tl ->
- let ids' = id::ids in
- let ids'' =
- "cic:/" ^
- String.concat "/" (List.rev_map Id.to_string ids') in
- let he' =
- ids'', List.rev (List.filter (function x -> String.List.mem x hyps) he)
- in
- let tl' = aux ids' tl in
- match he' with
- _,[] -> tl'
- | _,_ -> he'::tl'
- in
- let cwd = Lib.cwd () in
- let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in
- let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
- aux (DirPath.repr modulepath) (List.rev pvars)
-;;
-
-(* The computation is very inefficient, but we can't do anything *)
-(* better unless this function is reimplemented in the Declare *)
-(* module. *)
-let search_variables () =
- let cwd = Lib.cwd () in
- let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in
- let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
- let rec aux =
- function
- [] -> []
- | he::tl as modules ->
- let one_section_variables =
- let dirpath = DirPath.make (modules @ DirPath.repr modulepath) in
- let t = List.map Id.to_string (Decls.last_section_hyps dirpath) in
- [he,t]
- in
- one_section_variables @ aux tl
- in
- aux
- (Cic2acic.remove_module_dirpath_from_dirpath
- ~basedir:modulepath cwd)
-;;
-
-(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
-
-let rec join_dirs cwd =
- function
- [] -> cwd
- | he::tail ->
- (try
- Unix.mkdir cwd 0o775
- with e when Errors.noncritical e -> () (* ignore the errors on mkdir *)
- ) ;
- let newcwd = cwd ^ "/" ^ he in
- join_dirs newcwd tail
-;;
-
-let filename_of_path xml_library_root tag =
- match xml_library_root with
- None -> None (* stdout *)
- | Some xml_library_root' ->
- let tokens = Cic2acic.token_list_of_kernel_name tag in
- Some (join_dirs xml_library_root' tokens)
-;;
-
-let body_filename_of_filename =
- function
- Some f -> Some (f ^ ".body")
- | None -> None
-;;
-
-let types_filename_of_filename =
- function
- Some f -> Some (f ^ ".types")
- | None -> None
-;;
-
-let theory_filename xml_library_root =
- match xml_library_root with
- None -> None (* stdout *)
- | Some xml_library_root' ->
- let toks = List.map Id.to_string (DirPath.repr (Lib.library_dp ())) in
- (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
- let alltoks = List.rev toks in
- Some (join_dirs xml_library_root' alltoks ^ ".theory")
-
-let print_object uri obj sigma filename =
- (* function to pretty print and compress an XML file *)
-(*CSC: Unix.system "gzip ..." is an horrible non-portable solution. *)
- let pp xml filename =
- Xml.pp xml filename ;
- match filename with
- None -> ()
- | Some fn ->
- let fn' =
- let rec escape s n =
- try
- let p = String.index_from s n '\'' in
- String.sub s n (p - n) ^ "\\'" ^ escape s (p+1)
- with Not_found -> String.sub s n (String.length s - n)
- in
- escape fn 0
- in
- ignore (Unix.system ("gzip " ^ fn' ^ ".xml"))
- in
- let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) =
- Cic2acic.acic_object_of_cic_object sigma obj in
- let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in
- let xmltypes =
- Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in
- pp xml filename ;
- begin
- match xml' with
- None -> ()
- | Some xml' -> pp xml' (body_filename_of_filename filename)
- end ;
- pp xmltypes (types_filename_of_filename filename)
-;;
-
-let string_list_of_named_context_list =
- List.map
- (function (n,_,_) -> Id.to_string n)
-;;
-
-(* Function to collect the variables that occur in a term. *)
-(* Used only for variables (since for constants and mutual *)
-(* inductive types this information is already available. *)
-let find_hyps t =
- let rec aux l t =
- match Term.kind_of_term t with
- Term.Var id when not (Id.List.mem id l) ->
- let (_,bo,ty) = Global.lookup_named id in
- let boids =
- match bo with
- Some bo' -> aux l bo'
- | None -> l
- in
- id::(aux boids ty)
- | Term.Var _
- | Term.Rel _
- | Term.Meta _
- | Term.Evar _
- | Term.Sort _ -> l
- | Term.Proj _ -> ignore(Errors.todo "Proj in find_hyps"); assert false
- | Term.Cast (te,_, ty) -> aux (aux l te) ty
- | Term.Prod (_,s,t) -> aux (aux l s) t
- | Term.Lambda (_,s,t) -> aux (aux l s) t
- | Term.LetIn (_,s,_,t) -> aux (aux l s) t
- | Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
- | Term.Const (con, _) ->
- let hyps = (Global.lookup_constant con).Declarations.const_hyps in
- map_and_filter l hyps @ l
- | Term.Ind (ind,_)
- | Term.Construct ((ind,_),_) ->
- let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
- map_and_filter l hyps @ l
- | Term.Case (_,t1,t2,b) ->
- Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b
- | Term.Fix (_,(_,tys,bodies))
- | Term.CoFix (_,(_,tys,bodies)) ->
- let r = Array.fold_left (fun i x -> aux i x) l tys in
- Array.fold_left (fun i x -> aux i x) r bodies
- and map_and_filter l =
- function
- [] -> []
- | (n,_,_)::tl when not (Id.List.mem n l) -> n::(map_and_filter l tl)
- | _::tl -> map_and_filter l tl
- in
- aux [] t
-;;
-
-(* Functions to construct an object *)
-
-let mk_variable_obj id body typ =
- let hyps,unsharedbody =
- match body with
- None -> [],None
- | Some bo -> find_hyps bo, Some (Unshare.unshare bo)
- in
- let hyps' = find_hyps typ @ hyps in
- let hyps'' = List.map Id.to_string hyps' in
- let variables = search_variables () in
- let params = filter_params variables hyps'' in
- Acic.Variable
- (Id.to_string id, unsharedbody, Unshare.unshare typ, params)
-;;
-
-
-let mk_constant_obj id bo ty variables hyps =
- let hyps = string_list_of_named_context_list hyps in
- let ty = Unshare.unshare ty in
- let params = filter_params variables hyps in
- match bo with
- None ->
- Acic.Constant (Id.to_string id,None,ty,params)
- | Some c ->
- Acic.Constant
- (Id.to_string id, Some (Unshare.unshare c), ty,params)
-;;
-
-let mk_inductive_obj sp mib packs variables nparams hyps finite =
- let hyps = string_list_of_named_context_list hyps in
- let params = filter_params variables hyps in
-(* let nparams = extract_nparams packs in *)
- let tys =
- let tyno = ref (Array.length packs) in
- Array.fold_right
- (fun p i ->
- decr tyno ;
- let {Declarations.mind_consnames=consnames ;
- Declarations.mind_typename=typename } = p
- in
- let inst = Univ.UContext.instance mib.Declarations.mind_universes in
- let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),inst) in
- let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),inst) in
- let cons =
- (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
- (Array.mapi
- (fun j x ->(x,Unshare.unshare lc.(j))) consnames)
- []
- )
- in
- (typename,finite,Unshare.unshare arity,cons)::i
- ) packs []
- in
- Acic.InductiveDefinition (tys,params,nparams)
-;;
-
-(* The current channel for .theory files *)
-let theory_buffer = Buffer.create 4000;;
-
-let theory_output_string ?(do_not_quote = false) s =
- (* prepare for coqdoc post-processing *)
- let s = if do_not_quote then s else "(** #"^s^"\n#*)\n" in
- print_if_verbose s;
- Buffer.add_string theory_buffer s
-;;
-
-let kind_of_inductive isrecord kn =
- "DEFINITION",
- if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite <> Decl_kinds.CoFinite
- then begin
- match isrecord with
- | Declare.KernelSilent -> "Record"
- | _ -> "Inductive"
- end
- else "CoInductive"
-;;
-
-let kind_of_variable id =
- match Decls.variable_kind id with
- | IsAssumption Definitional -> "VARIABLE","Assumption"
- | IsAssumption Logical -> "VARIABLE","Hypothesis"
- | IsAssumption Conjectural -> "VARIABLE","Conjecture"
- | IsDefinition Definition -> "VARIABLE","LocalDefinition"
- | IsProof _ -> "VARIABLE","LocalFact"
- | _ -> Errors.anomaly (Pp.str "Unsupported variable kind")
-;;
-
-let kind_of_constant kn =
- match Decls.constant_kind kn with
- | IsAssumption Definitional -> "AXIOM","Declaration"
- | IsAssumption Logical -> "AXIOM","Axiom"
- | IsAssumption Conjectural ->
- Pp.msg_warning (Pp.str "Conjecture not supported in dtd (used Declaration instead)");
- "AXIOM","Declaration"
- | IsDefinition Definition -> "DEFINITION","Definition"
- | IsDefinition Example ->
- Pp.msg_warning (Pp.str "Example not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition Coercion ->
- Pp.msg_warning (Pp.str "Coercion not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition SubClass ->
- Pp.msg_warning (Pp.str "SubClass not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition CanonicalStructure ->
- Pp.msg_warning (Pp.str "CanonicalStructure not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition Fixpoint ->
- Pp.msg_warning (Pp.str "Fixpoint not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition CoFixpoint ->
- Pp.msg_warning (Pp.str "CoFixpoint not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition Scheme ->
- Pp.msg_warning (Pp.str "Scheme not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition StructureComponent ->
- Pp.msg_warning (Pp.str "StructureComponent not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition IdentityCoercion ->
- Pp.msg_warning (Pp.str "IdentityCoercion not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition Instance ->
- Pp.msg_warning (Pp.str "Instance not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsDefinition Method ->
- Pp.msg_warning (Pp.str "Method not supported in dtd (used Definition instead)");
- "DEFINITION","Definition"
- | IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) ->
- "THEOREM",Kindops.string_of_theorem_kind thm
- | IsProof _ ->
- Pp.msg_warning (Pp.str "Unsupported theorem kind (used Theorem instead)");
- "THEOREM",Kindops.string_of_theorem_kind Theorem
-;;
-
-let kind_of_global r =
- match r with
- | Globnames.IndRef kn | Globnames.ConstructRef (kn,_) ->
- let isrecord =
- try let _ = Recordops.lookup_projections kn in Declare.KernelSilent
- with Not_found -> Declare.KernelVerbose in
- kind_of_inductive isrecord (fst kn)
- | Globnames.VarRef id -> kind_of_variable id
- | Globnames.ConstRef kn -> kind_of_constant kn
-;;
-
-let print_object_kind uri (xmltag,variation) =
- let s =
- Printf.sprintf "<ht:%s uri=\"%s\" as=\"%s\"/>\n" xmltag uri variation
- in
- theory_output_string s
-;;
-
-(* print id dest *)
-(* where sp is the qualified identifier (section path) of a *)
-(* definition/theorem, variable or inductive definition *)
-(* and dest is either None (for stdout) or (Some filename) *)
-(* pretty prints via Xml.pp the object whose identifier is id on dest *)
-(* Note: it is printed only (and directly) the most cooked available *)
-(* form of the definition (all the parameters are *)
-(* lambda-abstracted, but the object can still refer to variables) *)
-let print internal glob_ref kind xml_library_root =
- (* Variables are the identifiers of the variables in scope *)
- let variables = search_variables () in
- let tag,obj =
- match glob_ref with
- Globnames.VarRef id ->
- (* this kn is fake since it is not provided by Coq *)
- let kn = Lib.make_kn id in
- let (_,body,typ) = Global.lookup_named id in
- Cic2acic.Variable kn,mk_variable_obj id body typ
- | Globnames.ConstRef kn ->
- let id = Label.to_id (Names.con_label kn) in
- let cb = Global.lookup_constant kn in
- let val0 = Declareops.body_of_constant cb in
- let typ = cb.Declarations.const_type in
- let hyps = cb.Declarations.const_hyps in
- let typ = Typeops.type_of_constant_type (Global.env()) typ in
- Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
- | Globnames.IndRef (kn,_) ->
- let mib = Global.lookup_mind kn in
- let {Declarations.mind_nparams=nparams;
- Declarations.mind_packets=packs ;
- Declarations.mind_hyps=hyps;
- Declarations.mind_finite=finite} = mib in
- Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps (finite<>Decl_kinds.CoFinite)
- | Globnames.ConstructRef _ ->
- Errors.error ("a single constructor cannot be printed in XML")
- in
- let fn = filename_of_path xml_library_root tag in
- let uri = Cic2acic.uri_of_kernel_name tag in
- (match internal with
- | Declare.KernelSilent -> ()
- | _ -> print_object_kind uri kind);
- print_object uri obj Evd.empty fn
-;;
-
-let print_ref qid fn =
- let ref = Nametab.global qid in
- print Declare.UserVerbose ref (kind_of_global ref) fn
-
-(* show dest *)
-(* where dest is either None (for stdout) or (Some filename) *)
-(* pretty prints via Xml.pp the proof in progress on dest *)
-let show_pftreestate internal fn (kind,pftst) id =
- if true then
- Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.")
-
-let show fn =
- let pftst = Pfedit.get_pftreestate () in
- let (id,kind,_) = Pfedit.current_proof_statement () in
- show_pftreestate false fn (kind,pftst) id
-;;
-
-
-(* Let's register the callbacks *)
-let xml_library_root =
- try
- Some (Sys.getenv "COQ_XML_LIBRARY_ROOT")
- with Not_found -> None
-;;
-
-let proof_to_export = ref None (* holds the proof-tree to export *)
-;;
-
-let _ =
- Hook.set Declare.xml_declare_variable
- (function (sp,kn) ->
- let id = Libnames.basename sp in
- print Declare.UserVerbose (Globnames.VarRef id) (kind_of_variable id) xml_library_root ;
- proof_to_export := None)
-;;
-
-let _ =
- Hook.set Declare.xml_declare_constant
- (function (internal,kn) ->
- match !proof_to_export with
- None ->
- print internal (Globnames.ConstRef kn) (kind_of_constant kn)
- xml_library_root
- | Some pftreestate ->
- (* It is a proof. Let's export it starting from the proof-tree *)
- (* I saved in the Pfedit.set_xml_cook_proof callback. *)
- let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
- show_pftreestate internal fn pftreestate
- (Label.to_id (Names.con_label kn)) ;
- proof_to_export := None)
-;;
-
-let _ =
- Hook.set Declare.xml_declare_inductive
- (function (isrecord,(sp,kn)) ->
- print Declare.UserVerbose (Globnames.IndRef (Names.mind_of_kn kn,0))
- (kind_of_inductive isrecord (Names.mind_of_kn kn))
- xml_library_root)
-;;
-
-let _ =
- Hook.set Vernac.xml_start_library
- (function () ->
- Buffer.reset theory_buffer;
- theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n";
- theory_output_string ("<!DOCTYPE html [\n" ^
- "<!ENTITY % xhtml-lat1.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-lat1.ent\">\n" ^
- "<!ENTITY % xhtml-special.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-special.ent\">\n" ^
- "<!ENTITY % xhtml-symbol.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-symbol.ent\">\n\n" ^
- "%xhtml-lat1.ent;\n" ^
- "%xhtml-special.ent;\n" ^
- "%xhtml-symbol.ent;\n" ^
- "]>\n\n");
- theory_output_string "<html xmlns=\"http://www.w3.org/1999/xhtml\" xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\" xmlns:helm=\"http://www.cs.unibo.it/helm\">\n";
- theory_output_string "<head></head>\n<body>\n")
-;;
-
-let _ =
- Hook.set Vernac.xml_end_library
- (function () ->
- theory_output_string "</body>\n</html>\n";
- let ofn = theory_filename xml_library_root in
- begin
- match ofn with
- None ->
- Buffer.output_buffer stdout theory_buffer ;
- | Some fn ->
- let ch = open_out (fn ^ ".v") in
- Buffer.output_buffer ch theory_buffer ;
- close_out ch;
- (* dummy glob file *)
- let ch = open_out (fn ^ ".glob") in
- close_out ch
- end ;
- Option.iter
- (fun fn ->
- let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in
- let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
- let command cmd =
- if Sys.command cmd <> 0 then
- Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\""))
- in
- command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
- command ("rm "^fn^".v "^fn^".glob");
- print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n"))
- ofn)
-;;
-
-let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:true) ;;
-
-let uri_of_dirpath dir =
- "/" ^ String.concat "/"
- (List.rev_map Id.to_string (DirPath.repr dir))
-;;
-
-let _ =
- Hook.set Lib.xml_open_section
- (fun _ ->
- let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in
- theory_output_string ("<ht:SECTION uri=\""^s^"\">"))
-;;
-
-let _ =
- Hook.set Lib.xml_close_section
- (fun _ -> theory_output_string "</ht:SECTION>")
-;;
-
-let _ =
- Hook.set Library.xml_require
- (fun d -> theory_output_string
- (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
- (uri_of_dirpath d) (DirPath.to_string d)))
-;;
diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
deleted file mode 100644
index 8e6254efc..000000000
--- a/plugins/xml/xmlcommand.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(* print_global qid fn *)
-(* where qid is a long name denoting a definition/theorem or *)
-(* an inductive definition *)
-(* and dest is either None (for stdout) or (Some filename) *)
-(* pretty prints via Xml.pp the object whose name is ref on dest *)
-(* Note: it is printed only (and directly) the most discharged available *)
-(* form of the definition (all the parameters are *)
-(* lambda-abstracted, but the object can still refer to variables) *)
-val print_ref : Libnames.reference -> string option -> unit
-
-(* show dest *)
-(* where dest is either None (for stdout) or (Some filename) *)
-(* pretty prints via Xml.pp the proof in progress on dest *)
-val show : string option -> unit
diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4
deleted file mode 100644
index 8cf3a0bdc..000000000
--- a/plugins/xml/xmlentries.ml4
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(************************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Pp
-
-(* File name *)
-
-VERNAC ARGUMENT EXTEND filename
-| [ "File" string(fn) ] -> [ Some fn ]
-| [ ] -> [ None ]
-END
-
-(* Print XML and Show XML *)
-
-VERNAC COMMAND EXTEND Xml CLASSIFIED AS QUERY
-| [ "Print" "XML" filename(fn) global(qid) ] -> [ Xmlcommand.print_ref qid fn ]
-
-| [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ]
-END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 10:15:55 +0000