summaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/xml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/COPYRIGHT25
-rw-r--r--contrib/xml/README254
-rw-r--r--contrib/xml/acic.ml108
-rw-r--r--contrib/xml/acic2Xml.ml4363
-rw-r--r--contrib/xml/cic.dtd259
-rw-r--r--contrib/xml/cic2acic.ml946
-rw-r--r--contrib/xml/doubleTypeInference.ml288
-rw-r--r--contrib/xml/doubleTypeInference.mli24
-rw-r--r--contrib/xml/proof2aproof.ml169
-rw-r--r--contrib/xml/proofTree2Xml.ml4211
-rw-r--r--contrib/xml/theoryobject.dtd62
-rw-r--r--contrib/xml/unshare.ml52
-rw-r--r--contrib/xml/unshare.mli21
-rw-r--r--contrib/xml/xml.ml473
-rw-r--r--contrib/xml/xml.mli38
-rw-r--r--contrib/xml/xmlcommand.ml706
-rw-r--r--contrib/xml/xmlcommand.mli41
-rw-r--r--contrib/xml/xmlentries.ml440
18 files changed, 3680 insertions, 0 deletions
diff --git a/contrib/xml/COPYRIGHT b/contrib/xml/COPYRIGHT
new file mode 100644
index 00000000..c8d231fd
--- /dev/null
+++ b/contrib/xml/COPYRIGHT
@@ -0,0 +1,25 @@
+(******************************************************************************)
+(* 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/contrib/xml/README b/contrib/xml/README
new file mode 100644
index 00000000..a45dd31a
--- /dev/null
+++ b/contrib/xml/README
@@ -0,0 +1,254 @@
+(******************************************************************************)
+(* 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 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.
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml
new file mode 100644
index 00000000..032ddbeb
--- /dev/null
+++ b/contrib/xml/acic.ml
@@ -0,0 +1,108 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 = identifier * '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 =
+ identifier * bool * constr * (* typename, inductive, arity *)
+ constructor list (* constructors *)
+and constructor =
+ identifier * constr (* id, type *)
+
+type aconstr =
+ | ARel of id * int * id * identifier
+ | AVar of id * uri
+ | AEvar of id * existential_key * aconstr list
+ | ASort of id * sorts
+ | ACast of id * aconstr * aconstr
+ | AProds of (id * name * aconstr) list * aconstr
+ | ALambdas of (id * name * aconstr) list * aconstr
+ | ALetIns of (id * name * 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 * identifier * int * aconstr * aconstr
+and acoinductivefun =
+ id * identifier * 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 * identifier * bool * aconstr * (* typename, inductive, arity *)
+ annconstructor list (* constructors *)
+and annconstructor =
+ identifier * aconstr (* id, type *)
diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4
new file mode 100644
index 00000000..64dc8a05
--- /dev/null
+++ b/contrib/xml/acic2Xml.ml4
@@ -0,0 +1,363 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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
+ [] -> Util.anomaly "find_last_id: empty list"
+ | [id,_,_] -> id
+ | _::tl -> find_last_id tl
+;;
+
+let export_existential = string_of_int
+
+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.string_of_id 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.string_of_id 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.string_of_id 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.string_of_id 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.string_of_id 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.string_of_id 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 rec 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.string_of_id n]
+ (print_term ids_to_inner_sorts t)
+ | n,A.Def (t,_) ->
+ X.xml_nempty "Def"
+ ["id",hid;"name",Names.string_of_id 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.string_of_id 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.string_of_id 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/contrib/xml/cic.dtd b/contrib/xml/cic.dtd
new file mode 100644
index 00000000..c8035cab
--- /dev/null
+++ b/contrib/xml/cic.dtd
@@ -0,0 +1,259 @@
+<?xml encoding="ISO-8859-1"?>
+
+<!-- Copyright (C) 2000-2004, HELM Team -->
+<!-- -->
+<!-- This file is part of HELM, an Hypertextual, Electronic -->
+<!-- Library of Mathematics, developed at the Computer Science -->
+<!-- Department, University of Bologna, Italy. -->
+<!-- -->
+<!-- HELM is free software; you can redistribute it and/or -->
+<!-- modify it under the terms of the GNU General Public License -->
+<!-- as published by the Free Software Foundation; either version 2 -->
+<!-- of the License, or (at your option) any later version. -->
+<!-- -->
+<!-- HELM is distributed in the hope that it will be useful, -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
+<!-- GNU General Public License for more details. -->
+<!-- -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
+<!-- MA 02111-1307, USA. -->
+<!-- -->
+<!-- For details, see the HELM World-Wide-Web page, -->
+<!-- http://cs.unibo.it/helm/. -->
+
+<!-- DTD FOR CIC OBJECTS: -->
+
+<!-- CIC term declaration -->
+
+<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
+ LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'>
+
+<!-- CIC sorts -->
+
+<!ENTITY % sort '(Prop|Set|Type|CProp)'>
+
+<!-- CIC sequents -->
+
+<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
+
+<!-- CIC objects: -->
+
+<!ELEMENT ConstantType %term;>
+<!ATTLIST ConstantType
+ name CDATA #REQUIRED
+ params CDATA #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT ConstantBody %term;>
+<!ATTLIST ConstantBody
+ for CDATA #REQUIRED
+ params CDATA #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT CurrentProof (Conjecture*,body)>
+<!ATTLIST CurrentProof
+ of CDATA #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT InductiveDefinition (InductiveType+)>
+<!ATTLIST InductiveDefinition
+ noParams NMTOKEN #REQUIRED
+ params CDATA #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT Variable (body?,type)>
+<!ATTLIST Variable
+ name CDATA #REQUIRED
+ params CDATA #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT Sequent %sequent;>
+<!ATTLIST Sequent
+ no NMTOKEN #REQUIRED
+ id ID #REQUIRED>
+
+<!-- Elements used in CIC objects, which are not terms: -->
+
+<!ELEMENT InductiveType (arity,Constructor*)>
+<!ATTLIST InductiveType
+ name CDATA #REQUIRED
+ inductive (true|false) #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT Conjecture %sequent;>
+<!ATTLIST Conjecture
+ no NMTOKEN #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT Constructor %term;>
+<!ATTLIST Constructor
+ name CDATA #REQUIRED>
+
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
+
+<!ELEMENT Hidden EMPTY>
+<!ATTLIST Hidden
+ id ID #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
+<!-- CIC terms: -->
+
+<!ELEMENT LAMBDA (decl*,target)>
+<!ATTLIST LAMBDA
+ sort %sort; #REQUIRED>
+
+<!ELEMENT LETIN (def*,target)>
+<!ATTLIST LETIN
+ sort %sort; #REQUIRED>
+
+<!ELEMENT PROD (decl*,target)>
+<!ATTLIST PROD
+ type %sort; #REQUIRED>
+
+<!ELEMENT CAST (term,type)>
+<!ATTLIST CAST
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT REL EMPTY>
+<!ATTLIST REL
+ value NMTOKEN #REQUIRED
+ binder CDATA #REQUIRED
+ id ID #REQUIRED
+ idref IDREF #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT SORT EMPTY>
+<!ATTLIST SORT
+ value CDATA #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT APPLY (%term;)+>
+<!ATTLIST APPLY
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT VAR EMPTY>
+<!ATTLIST VAR
+ uri CDATA #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!-- The substitutions are ordered by increasing DeBrujin -->
+<!-- index. An empty substitution means that that index is -->
+<!-- not accessible. -->
+<!ELEMENT META (substitution*)>
+<!ATTLIST META
+ no NMTOKEN #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT IMPLICIT EMPTY>
+<!ATTLIST IMPLICIT
+ id ID #REQUIRED>
+
+<!ELEMENT CONST EMPTY>
+<!ATTLIST CONST
+ uri CDATA #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT MUTIND EMPTY>
+<!ATTLIST MUTIND
+ uri CDATA #REQUIRED
+ noType NMTOKEN #REQUIRED
+ id ID #REQUIRED>
+
+<!ELEMENT MUTCONSTRUCT EMPTY>
+<!ATTLIST MUTCONSTRUCT
+ uri CDATA #REQUIRED
+ noType NMTOKEN #REQUIRED
+ noConstr NMTOKEN #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
+<!ATTLIST MUTCASE
+ uriType CDATA #REQUIRED
+ noType NMTOKEN #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT FIX (FixFunction+)>
+<!ATTLIST FIX
+ noFun NMTOKEN #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!ELEMENT COFIX (CofixFunction+)>
+<!ATTLIST COFIX
+ noFun NMTOKEN #REQUIRED
+ id ID #REQUIRED
+ sort %sort; #REQUIRED>
+
+<!-- Elements used in CIC terms: -->
+
+<!ELEMENT FixFunction (type,body)>
+<!ATTLIST FixFunction
+ name CDATA #REQUIRED
+ id ID #REQUIRED
+ recIndex NMTOKEN #REQUIRED>
+
+<!ELEMENT CofixFunction (type,body)>
+<!ATTLIST CofixFunction
+ id ID #REQUIRED
+ name CDATA #REQUIRED>
+
+<!ELEMENT substitution ((%term;)?)>
+
+<!-- Explicit named substitutions: -->
+
+<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)>
+<!ATTLIST instantiate
+ id ID #IMPLIED>
+
+<!-- Sintactic sugar for CIC terms and for CIC objects: -->
+
+<!ELEMENT arg %term;>
+<!ATTLIST arg
+ relUri CDATA #REQUIRED>
+
+<!ELEMENT decl %term;>
+<!ATTLIST decl
+ id ID #REQUIRED
+ type %sort; #REQUIRED
+ binder CDATA #IMPLIED>
+
+<!ELEMENT def %term;>
+<!ATTLIST def
+ id ID #REQUIRED
+ sort %sort; #REQUIRED
+ binder CDATA #IMPLIED>
+
+<!ELEMENT target %term;>
+
+<!ELEMENT term %term;>
+
+<!ELEMENT type %term;>
+
+<!ELEMENT arity %term;>
+
+<!ELEMENT patternsType %term;>
+
+<!ELEMENT inductiveTerm %term;>
+
+<!ELEMENT pattern %term;>
+
+<!ELEMENT body %term;>
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
new file mode 100644
index 00000000..d820f9e5
--- /dev/null
+++ b/contrib/xml/cic2acic.ml
@@ -0,0 +1,946 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 *)
+(************************************************************************)
+
+(* Utility Functions *)
+
+exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
+let get_module_path_of_section_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
+ [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 =
+ let module Ln = Libnames in
+ if Ln.is_dirpath_prefix_of basedir dir then
+ let ids = Names.repr_dirpath 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 (Names.repr_dirpath basedir))
+ (List.rev ids))
+ in
+ ids'
+ else Names.repr_dirpath dir
+;;
+
+
+let get_uri_of_var v pvars =
+ let module D = Declare in
+ let module N = Names in
+ let rec search_in_pvars names =
+ function
+ [] -> None
+ | ((name,l)::tl) ->
+ let names' = name::names in
+ if List.mem v l then
+ Some names'
+ else
+ search_in_pvars names' tl
+ in
+ let rec search_in_open_sections =
+ function
+ [] -> Util.error "Variable not found"
+ | he::tl as modules ->
+ let dirpath = N.make_dirpath modules in
+ if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then
+ modules
+ else
+ search_in_open_sections tl
+ in
+ let path =
+ match search_in_pvars [] pvars with
+ None -> search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
+ | Some path -> path
+ in
+ "cic:" ^
+ List.fold_left
+ (fun i x -> "/" ^ N.string_of_id x ^ i) "" path
+;;
+
+type tag =
+ Constant
+ | Inductive
+ | Variable
+;;
+
+let ext_of_tag =
+ function
+ Constant -> "con"
+ | Inductive -> "ind"
+ | Variable -> "var"
+;;
+
+exception FunctorsXMLExportationNotImplementedYet;;
+
+let subtract l1 l2 =
+ let l1' = List.rev (Names.repr_dirpath l1) in
+ let l2' = List.rev (Names.repr_dirpath l2) in
+ let rec aux =
+ function
+ he::tl when tl = l2' -> [he]
+ | he::tl -> he::(aux tl)
+ | [] -> assert (l2' = []) ; []
+ in
+ Names.make_dirpath (List.rev (aux l1'))
+;;
+
+(*CSC: Dead code to be removed
+let token_list_of_kernel_name ~keep_sections kn tag =
+ let module N = Names in
+ let (modpath,dirpath,label) = Names.repr_kn kn in
+ let token_list_of_dirpath dirpath =
+ List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
+ let rec token_list_of_modpath =
+ function
+ N.MPdot (path,label) ->
+ token_list_of_modpath path @ [N.string_of_label label]
+ | N.MPfile dirpath -> token_list_of_dirpath dirpath
+ | N.MPself self ->
+ if self = Names.initial_msid then
+ [ "Top" ]
+ else
+ let module_path =
+ let f = N.string_of_id (N.id_of_msid self) in
+ let _,longf =
+ System.find_file_in_path (Library.get_load_path ()) (f^".v") in
+ let ldir0 = Library.find_logical_path (Filename.dirname longf) in
+ let id = Names.id_of_string (Filename.basename f) in
+ Libnames.extend_dirpath ldir0 id
+ in
+ token_list_of_dirpath module_path
+ | N.MPbound _ -> raise FunctorsXMLExportationNotImplementedYet
+ in
+ token_list_of_modpath modpath @
+ (if keep_sections then token_list_of_dirpath dirpath else []) @
+ [N.string_of_label label ^ "." ^ (ext_of_tag tag)]
+;;
+*)
+
+let token_list_of_path dir id tag =
+ let module N = Names in
+ let token_list_of_dirpath dirpath =
+ List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
+ token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
+
+let token_list_of_kernel_name kn tag =
+ let module N = Names in
+ let module LN = Libnames in
+ let dir = match tag with
+ | Variable ->
+ Lib.cwd ()
+ | Constant ->
+ Lib.library_part (LN.ConstRef kn)
+ | Inductive ->
+ Lib.library_part (LN.IndRef (kn,0))
+ in
+ let id = N.id_of_label (N.label kn) in
+ token_list_of_path dir id tag
+;;
+
+let uri_of_kernel_name kn tag =
+ let tokens = token_list_of_kernel_name kn tag in
+ "cic:/" ^ String.concat "/" tokens
+
+let uri_of_declaration id tag =
+ let module LN = Libnames in
+ let dir = LN.extract_dirpath_prefix (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 *)
+ | _ -> Util.anomaly "family_of_term"
+;;
+
+module CPropRetyping =
+ struct
+ module T = Term
+
+ 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 (T.subst1 h c2) rest
+ | _ -> Util.anomaly "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.Meta n ->
+ (try T.strip_outer_cast (List.assoc n metamap)
+ with Not_found -> Util.anomaly "type_of: this is not a well-typed term")
+ | T.Rel n ->
+ let (_,_,ty) = Environ.lookup_rel n env in
+ T.lift n ty
+ | T.Var id ->
+ (try
+ let (_,_,ty) = Environ.lookup_named id env in
+ T.body_of_type ty
+ with Not_found ->
+ Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
+ | T.Const c ->
+ let cb = Environ.lookup_constant c env in
+ T.body_of_type cb.Declarations.const_type
+ | T.Evar ev -> Instantiate.existential_type sigma ev
+ | T.Ind ind -> T.body_of_type (Inductive.type_of_inductive env ind)
+ | T.Construct cstr ->
+ T.body_of_type (Inductive.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 -> Util.anomaly "type_of: Bad recursive type" in
+ let t = Reductionops.whd_beta (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 (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) ->
+ T.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.prop_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 Environ.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 _ ->
+ Util.anomaly "sort_of: 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 _ ->
+ Util.anomaly "sort_of: 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
+ pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty
+=
+ let module D = DoubleTypeInference in
+ let module E = Environ in
+ let module N = Names in
+ let module A = Acic in
+ let module T = Term in
+ 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
+ D.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 T.InProp -> "Prop"
+ | Coq_sort T.InSet -> "Set"
+ | Coq_sort T.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 {D.synthesized = synthesized; D.expected = expected} =
+ if computeinnertypes then
+try
+ Acic.CicHash.find terms_to_types tt
+with _ ->
+(*CSC: Warning: it really happens, for example in Ring_theory!!! *)
+Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm 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. *)
+ {D.synthesized =
+ Reductionops.nf_beta
+ (CPropRetyping.get_type_of env evar_map
+ (Evarutil.refresh_universes tt)) ;
+ D.expected = None}
+ in
+(* Debugging only:
+print_endline "TERMINE:" ; flush stdout ;
+Pp.ppnl (Printer.prterm tt) ; flush stdout ;
+print_endline "TIPO:" ; flush stdout ;
+Pp.ppnl (Printer.prterm synthesized) ; flush stdout ;
+print_endline "ENVIRONMENT:" ; flush stdout ;
+Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
+print_endline "FINE_ENVIRONMENT" ; flush stdout ;
+*)
+ let innersort = get_sort_family_of env evar_map synthesized 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 = Libnames.reference_of_constr h in
+ let sp =
+ match g with
+ Libnames.ConstructRef ((induri,_),_)
+ | Libnames.IndRef (induri,_) ->
+ Nametab.sp_of_global (Libnames.IndRef (induri,0))
+ | Libnames.VarRef id ->
+ (* Invariant: variables are never cooked in Coq *)
+ raise Not_found
+ | _ -> Nametab.sp_of_global g
+ in
+ Dischargedhypsmap.get_discharged_hyps sp,
+ get_module_path_of_section_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.map Names.string_of_id (List.rev he1')) ^ "/"
+ ^ (Names.string_of_id 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,_ =
+ T.decompose_prod_n uninst_vars_length
+ (CPropRetyping.get_type_of env evar_map tt)
+ in
+ let eta_expanded =
+ let arguments =
+ List.map (T.lift uninst_vars_length) t @
+ Termops.rel_list 0 uninst_vars_length
+ in
+ Unshare.unshare
+ (T.lamn uninst_vars_length un_args
+ (T.applistc h arguments))
+ in
+ D.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 T.kind_of_term tt with
+ T.Rel n ->
+ let id =
+ match List.nth (E.rel_context env) (n - 1) with
+ (N.Name id,_,_) -> id
+ | (N.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'' ;
+ A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
+ | T.Var id ->
+ let path = get_uri_of_var (N.string_of_id 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'' ;
+ A.AVar
+ (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var")
+ | T.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'' ;
+ A.AEvar
+ (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
+ | T.Meta _ -> Util.anomaly "Meta met during exporting to XML"
+ | T.Sort s -> A.ASort (fresh_id'', s)
+ | T.Cast (v,t) ->
+ Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if is_a_Prop innersort then
+ add_inner_type fresh_id'' ;
+ A.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t)
+ | T.Prod (n,s,t) ->
+ let n' =
+ match n with
+ N.Anonymous -> N.Anonymous
+ | _ ->
+ if not fake_dependent_products && T.noccurn 1 t then
+ N.Anonymous
+ else
+ N.Name
+ (Nameops.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
+ T.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 = E.push_rel (n', None, s) env in
+ let new_idrefs = fresh_id''::idrefs in
+ (match Term.kind_of_term t with
+ T.Prod _ ->
+ aux computeinnertypes (Some fresh_id'') new_passed_prods
+ new_env new_idrefs t
+ | _ ->
+ A.AProds (new_passed_prods, aux' new_env new_idrefs t))
+ | T.Lambda (n,s,t) ->
+ let n' =
+ match n with
+ N.Anonymous -> N.Anonymous
+ | _ ->
+ N.Name (Nameops.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
+ T.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 = E.push_rel (n', None, s) env in
+ let new_idrefs = fresh_id''::idrefs in
+ (match Term.kind_of_term t with
+ T.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
+ A.ALambdas (lambdas, t'') ->
+ A.ALambdas (lambdas@new_passed_lambdas, t'')
+ | _ ->
+ A.ALambdas (new_passed_lambdas, t')
+ )
+ | T.LetIn (n,s,t,d) ->
+ let n' =
+ match n with
+ N.Anonymous -> N.Anonymous
+ | _ ->
+ N.Name (Nameops.next_name_away n (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
+ T.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 = E.push_rel (n', Some s, t) env in
+ let new_idrefs = fresh_id''::idrefs in
+ (match Term.kind_of_term d with
+ T.LetIn _ ->
+ aux computeinnertypes (Some fresh_id'') new_passed_letins
+ new_env new_idrefs d
+ | _ -> A.ALetIns
+ (new_passed_letins, aux' new_env new_idrefs d))
+ | T.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 = List.length residual_args > 0 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
+ A.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
+ | T.Const kn ->
+ 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 _ _ =
+ A.AConst (fresh_id'', subst, (uri_of_kernel_name kn Constant))
+ in
+ let (_,subst') = subst in
+ explicit_substitute_and_eta_expand_if_required tt []
+ (List.map snd subst')
+ compute_result_if_eta_expansion_not_required
+ | T.Ind (kn,i) ->
+ let compute_result_if_eta_expansion_not_required _ _ =
+ A.AInd (fresh_id'', subst, (uri_of_kernel_name kn Inductive), 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
+ | T.Construct ((kn,i),j) ->
+ 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 _ _ =
+ A.AConstruct
+ (fresh_id'', subst, (uri_of_kernel_name kn Inductive), 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
+ | T.Case ({T.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
+ A.ACase
+ (fresh_id'', (uri_of_kernel_name kn Inductive), i,
+ aux' env idrefs ty, aux' env idrefs term, a')
+ | T.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
+ N.Anonymous -> Util.error "Anonymous fix function met"
+ | N.Name id as n ->
+ let res = N.Name (Nameops.next_name_away n !ids) in
+ ids := id::!ids ;
+ res
+ ) f
+ in
+ A.AFix (fresh_id'', i,
+ Array.fold_right
+ (fun (id,fi,ti,bi,ai) i ->
+ let fi' =
+ match fi with
+ N.Name fi -> fi
+ | N.Anonymous -> Util.error "Anonymous fix function met"
+ in
+ (id, fi', ai,
+ aux' env idrefs ti,
+ aux' (E.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'
+ ) []
+ )
+ | T.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
+ N.Anonymous -> Util.error "Anonymous fix function met"
+ | N.Name id as n ->
+ let res = N.Name (Nameops.next_name_away n !ids) in
+ ids := id::!ids ;
+ res
+ ) f
+ in
+ A.ACoFix (fresh_id'', i,
+ Array.fold_right
+ (fun (id,fi,ti,bi) i ->
+ let fi' =
+ match fi with
+ N.Name fi -> fi
+ | N.Anonymous -> Util.error "Anonymous fix function met"
+ in
+ (id, fi',
+ aux' env idrefs ti,
+ aux' (E.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
+;;
+
+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 pvars sigma obj =
+ let module A = Acic in
+ 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 pvars 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
+ A.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
+ A.AConstant (fresh_id (),id,abo,aty,params)
+ | A.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
+ A.AVariable (fresh_id (),id,abo,aty,params)
+ | A.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
+ A.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,A.Decl at))::atl
+ | A.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
+ A.ARel (s,99,s,Names.id_of_string s)
+ in
+ final_env,final_idrefs,
+ (hid,(n,A.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
+ A.ACurrentProof (fresh_id (),id,aconjectures,abo,aty)
+ | A.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
+ A.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/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
new file mode 100644
index 00000000..f0e3f5e3
--- /dev/null
+++ b/contrib/xml/doubleTypeInference.ml
@@ -0,0 +1,288 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 prerr_endline _ = ();;
+
+let cprop =
+ let module N = Names in
+ N.make_kn
+ (N.MPfile
+ (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
+ (N.make_dirpath [])
+ (N.mk_label "CProp")
+;;
+
+let whd_betadeltaiotacprop env evar_map ty =
+ let module R = Rawterm in
+ let red_exp =
+ R.Hnf (*** Instead CProp is made Opaque ***)
+(*
+ R.Cbv
+ {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ;
+ R.rConst = [Names.EvalConstRef cprop]
+ }
+*)
+ in
+Conv_oracle.set_opaque_const cprop;
+prerr_endline "###whd_betadeltaiotacprop:" ;
+let xxx =
+(*Pp.msgerr (Printer.prterm_env env ty);*)
+prerr_endline "";
+ Tacred.reduction_of_redexp red_exp env evar_map ty
+in
+prerr_endline "###FINE" ;
+(*
+Pp.msgerr (Printer.prterm_env env xxx);
+*)
+prerr_endline "";
+Conv_oracle.set_transparent_const cprop;
+xxx
+;;
+
+
+(* 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 (Term.body_of_type 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 E = Environ in
+ (* the type part is the synthesized type *)
+ let judgement =
+ match T.kind_of_term cstr with
+ T.Meta n ->
+ Util.error
+ "DoubleTypeInference.double_type_of: found a non-instanciated goal"
+
+ | T.Evar ((n,l) as ev) ->
+ let ty = Unshare.unshare (Instantiate.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 = (Evd.map 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 (T.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 (E.constant_type env c)
+
+ | T.Ind ind ->
+ E.make_judge cstr (Inductive.type_of_inductive env ind)
+
+ | T.Construct cstruct ->
+ E.make_judge cstr (Inductive.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
+ let (j,_) = Typeops.judge_of_case env ci pj cj lfj in
+ j
+
+ | 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
+ Typeops.judge_of_type u
+ with _ -> (* Successor of a non universe-variable universe anomaly *)
+ (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
+ Typeops.judge_of_type (Termops.new_univ ())
+)
+
+ | 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 c1)) ::
+ (aux (T.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 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,t) ->
+ let cj = execute env sigma c (Some (Reductionops.nf_beta 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 tj in
+ j
+ in
+ let synthesized = E.j_type judgement in
+ let synthesized' = Reductionops.nf_beta synthesized in
+ let types,res =
+ match expectedty with
+ None ->
+ (* No expected type *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ (*CSC: in HELM we did not considered Casts to be irrelevant. *)
+ (*CSC: does it really matter? (eq_constr is up to casts) *)
+ | Some ty when Term.eq_constr synthesized' ty ->
+ (* The expected type is synthactically equal to *)
+ (* the synthesized type. Let's forget it. *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | 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.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ;
+ 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 (Term.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/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli
new file mode 100644
index 00000000..33d3e5cd
--- /dev/null
+++ b/contrib/xml/doubleTypeInference.mli
@@ -0,0 +1,24 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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.kernel_name
+
+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/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
new file mode 100644
index 00000000..165a456d
--- /dev/null
+++ b/contrib/xml/proof2aproof.ml
@@ -0,0 +1,169 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 *)
+(************************************************************************)
+
+(* Note: we can not use the Set module here because we _need_ physical *)
+(* equality and there exists no comparison function compatible with *)
+(* physical equality. *)
+
+module S =
+ struct
+ let empty = []
+ let mem = List.memq
+ let add x l = x::l
+ end
+;;
+
+(* evar reduction that preserves some terms *)
+let nf_evar sigma ~preserve =
+ let module T = Term in
+ let rec aux t =
+ if preserve t then t else
+ match T.kind_of_term t with
+ | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _
+ | T.Construct _ -> t
+ | T.Cast (c1,c2) -> T.mkCast (aux c1, aux c2)
+ | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2)
+ | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c)
+ | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c)
+ | T.App (c,l) ->
+ let c' = aux c in
+ let l' = Array.map aux l in
+ (match T.kind_of_term c' with
+ T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
+ | T.Cast (he,_) ->
+ (match T.kind_of_term he with
+ T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
+ | _ -> T.mkApp (c', l')
+ )
+ | _ -> T.mkApp (c', l'))
+ | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e ->
+ aux (Instantiate.existential_value sigma (e,l))
+ | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l)
+ | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl)
+ | T.Fix (ln,(lna,tl,bl)) ->
+ T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl))
+ | T.CoFix(ln,(lna,tl,bl)) ->
+ T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl))
+ in
+ aux
+;;
+
+(* Unshares a proof-tree. *)
+(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
+let rec unshare_proof_tree =
+ let module PT = Proof_type in
+ function {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = ref} ->
+ let unshared_ref =
+ match ref with
+ None -> None
+ | Some (rule,pfs) ->
+ let unshared_rule =
+ match rule with
+ PT.Prim prim -> PT.Prim prim
+ | PT.Change_evars -> PT.Change_evars
+ | PT.Tactic (tactic_expr, pf) ->
+ PT.Tactic (tactic_expr, unshare_proof_tree pf)
+ in
+ Some (unshared_rule, List.map unshare_proof_tree pfs)
+ in
+ {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = unshared_ref}
+;;
+
+module ProofTreeHash =
+ Hashtbl.Make
+ (struct
+ type t = Proof_type.proof_tree
+ let equal = (==)
+ let hash = Hashtbl.hash
+ end)
+;;
+
+
+let extract_open_proof sigma pf =
+ let module PT = Proof_type in
+ let module L = Logic in
+ let sigma = ref sigma in
+ let proof_tree_to_constr = ProofTreeHash.create 503 in
+ let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in
+ let unshared_constrs = ref S.empty in
+ let rec proof_extractor vl node =
+ let constr =
+ match node with
+ {PT.ref=Some(PT.Prim _,_)} as pf ->
+ L.prim_extractor proof_extractor vl pf
+
+ | {PT.ref=Some(PT.Tactic (_,hidden_proof),spfl)} ->
+ let sgl,v = Refiner.frontier hidden_proof in
+ let flat_proof = v spfl in
+ ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ;
+ proof_extractor vl flat_proof
+
+ | {PT.ref=Some(PT.Change_evars,[pf])} -> (proof_extractor vl) pf
+
+ | {PT.ref=None;PT.goal=goal} ->
+ let visible_rels =
+ Util.map_succeed
+ (fun id ->
+ (* Section variables are in the [id] list but are not *)
+ (* lambda abstracted in the term [vl] *)
+ try let n = Util.list_index id vl in (n,id)
+ with Not_found -> failwith "caught")
+(*CSC: the above function must be modified such that when it is found *)
+(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *)
+(*CSC: as the evar_instance. Ordering the instance becomes useless (it *)
+(*CSC: will already be ordered. *)
+ (Termops.ids_of_named_context goal.Evd.evar_hyps) in
+ let sorted_rels =
+ Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in
+ let context =
+ List.map
+ (fun (_,id) -> Sign.lookup_named id goal.Evd.evar_hyps)
+ sorted_rels
+ in
+(*CSC: the section variables in the right order must be added too *)
+ let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in
+ let env = Global.env_of_context context in
+ let sigma',evar =
+ Evarutil.new_isevar_sign env !sigma goal.Evd.evar_concl evar_instance
+ in
+ sigma := sigma' ;
+ evar
+
+ | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor"
+ in
+ let unsharedconstr =
+ let evar_nf_constr =
+ nf_evar !sigma ~preserve:(function e -> S.mem e !unshared_constrs) constr
+ in
+ Unshare.unshare
+ ~already_unshared:(function e -> S.mem e !unshared_constrs)
+ evar_nf_constr
+ in
+(*CSC: debugging stuff to be removed *)
+if ProofTreeHash.mem proof_tree_to_constr node then
+ Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") (Refiner.print_proof !sigma [] node)) ;
+ ProofTreeHash.add proof_tree_to_constr node unsharedconstr ;
+ unshared_constrs := S.add unsharedconstr !unshared_constrs ;
+ unsharedconstr
+ in
+ let unshared_pf = unshare_proof_tree pf in
+ let pfterm = proof_extractor [] unshared_pf in
+ (pfterm, !sigma, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
+ unshared_pf)
+;;
+
+let extract_open_pftreestate pts =
+ extract_open_proof (Refiner.evc_of_pftreestate pts)
+ (Tacmach.proof_of_pftreestate pts)
+;;
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
new file mode 100644
index 00000000..b9b66774
--- /dev/null
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -0,0 +1,211 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 *)
+(************************************************************************)
+
+let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";;
+
+let std_ppcmds_to_string s =
+ Pp.msg_with Format.str_formatter s;
+ Format.flush_str_formatter ()
+;;
+
+let idref_of_id id = "v" ^ id;;
+
+(* Transform a constr to an Xml.token Stream.t *)
+(* env is a named context *)
+(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *)
+let constr_to_xml obj sigma env =
+ 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 pvars = [] in
+ (* named_context holds section variables and local variables *)
+ let named_context = Environ.named_context env in
+ (* real_named_context holds only the section variables *)
+ let real_named_context = Environ.named_context (Global.env ()) in
+ (* named_context' holds only the local variables *)
+ let named_context' =
+ List.filter (function n -> not (List.mem n real_named_context)) named_context
+ in
+ let idrefs =
+ List.map
+ (function x,_,_ -> idref_of_id (Names.string_of_id x)) named_context' in
+ let rel_context = Sign.push_named_to_rel_context named_context' [] in
+ let rel_env =
+ Environ.push_rel_context rel_context
+ (Environ.reset_with_named_context real_named_context env) in
+ let obj' =
+ Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
+ let seed = ref 0 in
+ try
+ let annobj =
+ Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids
+ ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars rel_env
+ idrefs sigma (Unshare.unshare obj') None
+ in
+ Acic2Xml.print_term ids_to_inner_sorts annobj
+ with e ->
+ Util.anomaly
+ ("Problem during the conversion of constr into XML: " ^
+ Printexc.to_string e)
+(* CSC: debugging stuff
+Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
+Pp.ppnl (Pp.str "ENVIRONMENT:") ;
+Pp.ppnl (Printer.pr_context_of rel_env) ;
+Pp.ppnl (Pp.str "TERM:") ;
+Pp.ppnl (Printer.prterm_env rel_env obj') ;
+Pp.ppnl (Pp.str "RAW-TERM:") ;
+Pp.ppnl (Printer.prterm obj') ;
+Xml.xml_empty "MISSING TERM" [] (*; raise e*)
+*)
+;;
+
+let first_word s =
+ try let i = String.index s ' ' in
+ String.sub s 0 i
+ with _ -> s
+;;
+
+let string_of_prim_rule x = match x with
+ | Proof_type.Intro _-> "Intro"
+ | Proof_type.Intro_replacing _-> "Intro_replacing"
+ | Proof_type.Cut (_,_,_) -> "Cut"
+ | Proof_type.FixRule (_,_,_) -> "FixRule"
+ | Proof_type.Cofix (_,_)-> "Cofix"
+ | Proof_type.Refine _ -> "Refine"
+ | Proof_type.Convert_concl _ -> "Convert_concl"
+ | Proof_type.Convert_hyp _->"Convert_hyp"
+ | Proof_type.Thin _ -> "Thin"
+ | Proof_type.ThinBody _-> "ThinBody"
+ | Proof_type.Move (_,_,_) -> "Move"
+ | Proof_type.Rename (_,_) -> "Rename"
+
+
+let
+ print_proof_tree curi sigma0 pf proof_tree_to_constr
+ proof_tree_to_flattened_proof_tree constr_to_ids
+=
+ let module PT = Proof_type in
+ let module L = Logic in
+ let module X = Xml in
+ let module T = Tacexpr in
+ let ids_of_node node =
+ let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
+(*
+let constr =
+ try
+ Proof2aproof.ProofTreeHash.find proof_tree_to_constr node
+ with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated
+no lambda-term: ") (Refiner.print_script true (Evd.empty)
+(Global.named_context ()) node)) ; assert false (* Closed bug, should not
+happen any more *)
+in
+*)
+ try
+ Some (Acic.CicHash.find constr_to_ids constr)
+ with _ ->
+Pp.ppnl (Pp.(++) (Pp.str
+"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
+(Printer.prterm constr)) ;
+ None
+ in
+ let rec aux node old_hyps =
+ let of_attribute =
+ match ids_of_node node with
+ None -> []
+ | Some id -> ["of",id]
+ in
+ match node with
+ {PT.ref=Some(PT.Prim tactic_expr,nodes)} ->
+ let tac = string_of_prim_rule tactic_expr in
+ let of_attribute = ("name",tac)::of_attribute in
+ if nodes = [] then
+ X.xml_empty "Prim" of_attribute
+ else
+ X.xml_nempty "Prim" of_attribute
+ (List.fold_left
+ (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
+
+ | {PT.goal=goal;
+ PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} ->
+ (* [hidden_proof] is the proof of the tactic; *)
+ (* [nodes] are the proof of the subgoals generated by the tactic; *)
+ (* [flat_proof] if the proof-tree obtained substituting [nodes] *)
+ (* for the holes in [hidden_proof] *)
+ let flat_proof =
+ Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
+ in begin
+ match tactic_expr with
+ | T.TacArg (T.Tacexp _) ->
+ (* We don't need to keep the level of abstraction introduced at *)
+ (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
+ aux flat_proof old_hyps
+ | _ ->
+ (****** la tactique employee *)
+ let prtac = if !Options.v7 then Pptactic.pr_tactic else Pptacticnew.pr_tactic (Global.env()) in
+ let tac = std_ppcmds_to_string (prtac tactic_expr) in
+ let tacname= first_word tac in
+ let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
+
+ (****** le but *)
+ let {Evd.evar_concl=concl;
+ Evd.evar_hyps=hyps}=goal in
+
+ let rc = (Proof_trees.rc_of_gc sigma0 goal) in
+ let sigma = Proof_trees.get_gc rc in
+ let hyps = Proof_trees.get_hyps rc in
+ let env= Proof_trees.get_env rc in
+
+ let xgoal =
+ X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
+
+ let rec build_hyps =
+ function
+ | [] -> xgoal
+ | (id,c,tid)::hyps1 ->
+ let id' = Names.string_of_id id in
+ [< build_hyps hyps1;
+ (X.xml_nempty "Hypothesis"
+ ["id",idref_of_id id' ; "name",id']
+ (constr_to_xml tid sigma env))
+ >] in
+ let old_names = List.map (fun (id,c,tid)->id) old_hyps in
+ let new_hyps =
+ List.filter (fun (id,c,tid)-> not (List.mem id old_names)) hyps in
+
+ X.xml_nempty "Tactic" of_attribute
+ [<(build_hyps new_hyps) ; (aux flat_proof hyps)>]
+ end
+
+ | {PT.ref=Some(PT.Change_evars,nodes)} ->
+ X.xml_nempty "Change_evars" of_attribute
+ (List.fold_left
+ (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
+
+ | {PT.ref=None;PT.goal=goal} ->
+ X.xml_empty "Open_goal" of_attribute
+ in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n");
+ X.xml_nempty "ProofTree" ["of",curi] (aux pf [])
+ >]
+;;
+
+
+(* Hook registration *)
+(* CSC: debranched since it is bugged
+Xmlcommand.set_print_proof_tree print_proof_tree;;
+*)
diff --git a/contrib/xml/theoryobject.dtd b/contrib/xml/theoryobject.dtd
new file mode 100644
index 00000000..953fe009
--- /dev/null
+++ b/contrib/xml/theoryobject.dtd
@@ -0,0 +1,62 @@
+<?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/contrib/xml/unshare.ml b/contrib/xml/unshare.ml
new file mode 100644
index 00000000..f30f8230
--- /dev/null
+++ b/contrib/xml/unshare.ml
@@ -0,0 +1,52 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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/contrib/xml/unshare.mli b/contrib/xml/unshare.mli
new file mode 100644
index 00000000..31ba9037
--- /dev/null
+++ b/contrib/xml/unshare.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
new file mode 100644
index 00000000..d0c64f30
--- /dev/null
+++ b/contrib/xml/xml.ml4
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 strm fn =
+ let channel = ref stdout in
+ 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
+ match fn with
+ Some filename ->
+ let filename = filename ^ ".xml" in
+ channel := open_out filename ;
+ pp_r 0 strm ;
+ close_out !channel ;
+ print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n");
+ flush stdout
+ | None ->
+ pp_r 0 strm
+;;
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli
new file mode 100644
index 00000000..e65e6c81
--- /dev/null
+++ b/contrib/xml/xml.mli
@@ -0,0 +1,38 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 $Id: xml.mli,v 1.5.2.2 2004/07/16 19:30:15 herbelin Exp $ i*)
+
+(* 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
+
+(* 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/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
new file mode 100644
index 00000000..9fba5474
--- /dev/null
+++ b/contrib/xml/xmlcommand.ml
@@ -0,0 +1,706 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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;;
+
+(* HOOKS *)
+let print_proof_tree, set_print_proof_tree =
+ let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in
+ (fun () -> !print_proof_tree),
+ (fun f ->
+ print_proof_tree :=
+ fun
+ curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree
+ constr_to_ids
+ ->
+ Some
+ (f curi sigma0 pf proof_tree_to_constr
+ proof_tree_to_flattened_proof_tree constr_to_ids))
+;;
+
+(* UTILITY FUNCTIONS *)
+
+let print_if_verbose s = if !verbose then print_string s;;
+
+(* Next exception is used only inside print_coq_object and tag_of_string_tag *)
+exception Uninteresting;;
+
+(* Internally, for Coq V7, params of inductive types are associated *)
+(* not to the whole block of mutual inductive (as it was in V6) but to *)
+(* each member of the block; but externally, all params are required *)
+(* to be the same; the following function checks that the parameters *)
+(* of each inductive of a same block are all the same, then returns *)
+(* this number; it fails otherwise *)
+let extract_nparams pack =
+ let module D = Declarations in
+ let module U = Util in
+ let module S = Sign in
+
+ let {D.mind_nparams=nparams0} = pack.(0) in
+ let arity0 = pack.(0).D.mind_user_arity in
+ let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in
+ for i = 1 to Array.length pack - 1 do
+ let {D.mind_nparams=nparamsi} = pack.(i) in
+ let arityi = pack.(i).D.mind_user_arity in
+ let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in
+ if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
+ done;
+ nparams0
+
+(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
+(* than that could exists in cooked form with the same name in a super *)
+(* section of the actual section *)
+let could_have_namesakes o sp = (* namesake = omonimo in italian *)
+ let module DK = Decl_kinds in
+ let module D = Declare in
+ let tag = Libobject.object_tag o in
+ print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
+ match tag with
+ "CONSTANT" ->
+ (match D.constant_strength sp with
+ | DK.Local -> false (* a local definition *)
+ | DK.Global -> true (* a non-local one *)
+ )
+ | "INDUCTIVE" -> true (* mutual inductive types are never local *)
+ | "VARIABLE" -> false (* variables are local, so no namesakes *)
+ | _ -> false (* uninteresting thing that won't be printed*)
+;;
+
+
+(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
+(* ENVIRONMENT (= [(name1,l1); ...;(namen,ln)] WHERE li IS THE LIST *)
+(* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT *)
+(* SECTION, WHOSE PATH IS namei *)
+
+let pvars =
+ ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);;
+let cumenv = ref Environ.empty_env;;
+
+(* 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 (List.map Names.string_of_id ids')) in
+ let he' =
+ ids'', List.rev (List.filter (function x -> 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 (Names.id_of_string "dummy") in
+ let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+ aux (Names.repr_dirpath modulepath) (List.rev pvars)
+;;
+
+type variables_type =
+ Definition of string * Term.constr * Term.types
+ | Assumption of string * Term.constr
+;;
+
+let add_to_pvars x =
+ let module E = Environ in
+ let v =
+ match x with
+ Definition (v, bod, typ) ->
+ cumenv :=
+ E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ;
+ v
+ | Assumption (v, typ) ->
+ cumenv :=
+ E.push_named (Names.id_of_string v, None, typ) !cumenv ;
+ v
+ in
+ match !pvars with
+ [] -> assert false
+ | ((name,l)::tl) -> pvars := (name,v::l)::tl
+;;
+
+(* 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 module N = Names in
+ let cwd = Lib.cwd () in
+ let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+ let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+ let rec aux =
+ function
+ [] -> []
+ | he::tl as modules ->
+ let one_section_variables =
+ let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
+ let t = List.map N.string_of_id (Declare.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 _ -> () (* Let's ignore the errors on mkdir *)
+ ) ;
+ let newcwd = cwd ^ "/" ^ he in
+ join_dirs newcwd tail
+;;
+
+let filename_of_path xml_library_root kn tag =
+ let module N = Names in
+ match xml_library_root with
+ None -> None (* stdout *)
+ | Some xml_library_root' ->
+ let tokens = Cic2acic.token_list_of_kernel_name kn 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 prooftree_filename_of_filename =
+ function
+ Some f -> Some (f ^ ".proof_tree")
+ | None -> None
+;;
+
+let theory_filename xml_library_root =
+ let module N = Names in
+ match xml_library_root with
+ None -> None (* stdout *)
+ | Some xml_library_root' ->
+ let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
+ let hd = List.hd toks 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 proof_tree_infos 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 !pvars 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) ;
+ match proof_tree_infos with
+ None -> ()
+ | Some (sigma0,proof_tree,proof_tree_to_constr,
+ proof_tree_to_flattened_proof_tree) ->
+ let xmlprooftree =
+ print_proof_tree ()
+ uri sigma0 proof_tree proof_tree_to_constr
+ proof_tree_to_flattened_proof_tree constr_to_ids
+ in
+ match xmlprooftree with
+ None -> ()
+ | Some xmlprooftree ->
+ pp xmlprooftree (prooftree_filename_of_filename filename)
+;;
+
+let string_list_of_named_context_list =
+ List.map
+ (function (n,_,_) -> Names.string_of_id 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 module T = Term in
+ let rec aux l t =
+ match T.kind_of_term t with
+ T.Var id when not (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)
+ | T.Var _
+ | T.Rel _
+ | T.Meta _
+ | T.Evar _
+ | T.Sort _ -> l
+ | T.Cast (te,ty) -> aux (aux l te) ty
+ | T.Prod (_,s,t) -> aux (aux l s) t
+ | T.Lambda (_,s,t) -> aux (aux l s) t
+ | T.LetIn (_,s,_,t) -> aux (aux l s) t
+ | T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
+ | T.Const con ->
+ let hyps = (Global.lookup_constant con).Declarations.const_hyps in
+ map_and_filter l hyps @ l
+ | T.Ind ind
+ | T.Construct (ind,_) ->
+ let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
+ map_and_filter l hyps @ l
+ | T.Case (_,t1,t2,b) ->
+ Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b
+ | T.Fix (_,(_,tys,bodies))
+ | T.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 (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 Names.string_of_id hyps' in
+ let variables = search_variables () in
+ let params = filter_params variables hyps'' in
+ Acic.Variable
+ (Names.string_of_id id, unsharedbody,
+ (Unshare.unshare (Term.body_of_type typ)), params)
+;;
+
+(* Unsharing is not performed on the body, that must be already unshared. *)
+(* The evar map and the type, instead, are unshared by this function. *)
+let mk_current_proof_obj is_a_variable id bo ty evar_map env =
+ let unshared_ty = Unshare.unshare (Term.body_of_type ty) in
+ let metasenv =
+ List.map
+ (function
+ (n, {Evd.evar_concl = evar_concl ;
+ Evd.evar_hyps = evar_hyps}
+ ) ->
+ (* We map the named context to a rel context and every Var to a Rel *)
+ let final_var_ids,context =
+ let rec aux var_ids =
+ function
+ [] -> var_ids,[]
+ | (n,None,t)::tl ->
+ let final_var_ids,tl' = aux (n::var_ids) tl in
+ let t' = Term.subst_vars var_ids t in
+ final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl'
+ | (n,Some b,t)::tl ->
+ let final_var_ids,tl' = aux (n::var_ids) tl in
+ let b' = Term.subst_vars var_ids b in
+ (* t will not be exported to XML. Thus no unsharing performed *)
+ final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl'
+ in
+ aux [] (List.rev evar_hyps)
+ in
+ (* We map the named context to a rel context and every Var to a Rel *)
+ (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
+ ) (Evd.non_instantiated evar_map)
+ in
+ let id' = Names.string_of_id id in
+ if metasenv = [] then
+ let ids =
+ Names.Idset.union
+ (Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in
+ let hyps0 = Environ.keep_hyps env ids in
+ let hyps = string_list_of_named_context_list hyps0 in
+ (* Variables are the identifiers of the variables in scope *)
+ let variables = search_variables () in
+ let params = filter_params variables hyps in
+ if is_a_variable then
+ Acic.Variable (id',Some bo,unshared_ty,params)
+ else
+ Acic.Constant (id',Some bo,unshared_ty,params)
+ else
+ Acic.CurrentProof (id',metasenv,bo,unshared_ty)
+;;
+
+let mk_constant_obj id bo ty variables hyps =
+ let hyps = string_list_of_named_context_list hyps in
+ let ty = Unshare.unshare (Term.body_of_type ty) in
+ let params = filter_params variables hyps in
+ match bo with
+ None ->
+ Acic.Constant (Names.string_of_id id,None,ty,params)
+ | Some c ->
+ Acic.Constant
+ (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)),
+ ty,params)
+;;
+
+let mk_inductive_obj sp packs variables hyps finite =
+ let module D = Declarations in
+ 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 {D.mind_consnames=consnames ;
+ D.mind_typename=typename ;
+ D.mind_nf_arity=arity} = p
+ in
+ let lc = Inductive.arities_of_constructors (Global.env ()) (sp,!tyno) in
+ let cons =
+ (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
+ (Array.mapi
+ (fun j x ->(x,Unshare.unshare (Term.body_of_type 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_theorem = function
+ | Decl_kinds.Theorem -> "Theorem"
+ | Decl_kinds.Lemma -> "Lemma"
+ | Decl_kinds.Fact -> "Fact"
+ | Decl_kinds.Remark -> "Remark"
+
+let kind_of_global_goal = function
+ | Decl_kinds.IsGlobal Decl_kinds.DefinitionBody -> "DEFINITION","InteractiveDefinition"
+ | Decl_kinds.IsGlobal (Decl_kinds.Proof k) -> "THEOREM",kind_of_theorem k
+ | Decl_kinds.IsLocal -> assert false
+
+let kind_of_inductive isrecord kn =
+ "DEFINITION",
+ if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite
+ then if isrecord then "Record" else "Inductive"
+ else "CoInductive"
+;;
+
+let kind_of_variable id =
+ let module DK = Decl_kinds in
+ match Declare.variable_kind id with
+ | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
+ | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
+ | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
+ | DK.IsDefinition -> "VARIABLE","LocalDefinition"
+ | DK.IsConjecture -> "VARIABLE","Conjecture"
+ | DK.IsProof DK.LocalStatement -> "VARIABLE","LocalFact"
+;;
+
+let kind_of_constant kn =
+ let module DK = Decl_kinds in
+ match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with
+ | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
+ | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
+ | DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
+ | DK.IsDefinition -> "DEFINITION","Definition"
+ | DK.IsConjecture -> "THEOREM","Conjecture"
+ | DK.IsProof thm -> "THEOREM",kind_of_theorem thm
+;;
+
+let kind_of_global r =
+ let module Ln = Libnames in
+ let module DK = Decl_kinds in
+ match r with
+ | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
+ let isrecord =
+ try let _ = Recordops.find_structure kn in true
+ with Not_found -> false in
+ kind_of_inductive isrecord (fst kn)
+ | Ln.VarRef id -> kind_of_variable id
+ | Ln.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 =
+ let module D = Declarations in
+ let module De = Declare in
+ let module G = Global in
+ let module N = Names in
+ let module Nt = Nametab in
+ let module T = Term in
+ let module X = Xml in
+ let module Ln = Libnames in
+ (* Variables are the identifiers of the variables in scope *)
+ let variables = search_variables () in
+ let kn,tag,obj =
+ match glob_ref with
+ Ln.VarRef id ->
+ let sp = Declare.find_section_variable id in
+ (* this kn is fake since it is not provided by Coq *)
+ let kn =
+ let (mod_path,dir_path) = Lib.current_prefix () in
+ N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp))
+ in
+ let (_,body,typ) = G.lookup_named id in
+ kn,Cic2acic.Variable,mk_variable_obj id body typ
+ | Ln.ConstRef kn ->
+ let id = N.id_of_label (N.label kn) in
+ let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+ G.lookup_constant kn in
+ kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps
+ | Ln.IndRef (kn,_) ->
+ let {D.mind_packets=packs ;
+ D.mind_hyps=hyps;
+ D.mind_finite=finite} = G.lookup_mind kn in
+ kn,Cic2acic.Inductive,
+ mk_inductive_obj kn packs variables hyps finite
+ | Ln.ConstructRef _ ->
+ Util.anomaly ("print: this should not happen")
+ in
+ let fn = filename_of_path xml_library_root kn tag in
+ let uri = Cic2acic.uri_of_kernel_name kn tag in
+ if not internal then print_object_kind uri kind;
+ print_object uri obj Evd.empty None fn
+;;
+
+let print_ref qid fn =
+ let ref = Nametab.global qid in
+ print false 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 =
+ let str = Names.string_of_id id in
+ let pf = Tacmach.proof_of_pftreestate pftst in
+ let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in
+ let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree,
+ unshared_pf
+ =
+ Proof2aproof.extract_open_pftreestate pftst in
+ let kn = Lib.make_kn id in
+ let env = Global.env () in
+ let obj =
+ mk_current_proof_obj (kind = Decl_kinds.IsLocal) id val0 typ evar_map env in
+ let uri =
+ match kind with
+ Decl_kinds.IsLocal ->
+ let uri =
+ "cic:/" ^ String.concat "/"
+ (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.Variable) in
+ let kind_of_var = "VARIABLE","LocalFact" in
+ if not internal then print_object_kind uri kind_of_var;
+ uri
+ | Decl_kinds.IsGlobal _ ->
+ let uri = Cic2acic.uri_of_declaration id Cic2acic.Constant in
+ if not internal then print_object_kind uri (kind_of_global_goal kind);
+ uri
+ in
+ print_object uri obj evar_map
+ (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr,
+ proof_tree_to_flattened_proof_tree)) fn
+;;
+
+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 _ =
+ Pfedit.set_xml_cook_proof
+ (function pftreestate -> proof_to_export := Some pftreestate)
+;;
+
+let _ =
+ Declare.set_xml_declare_variable
+ (function (sp,kn) ->
+ let id = Libnames.basename sp in
+ print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
+ proof_to_export := None)
+;;
+
+let _ =
+ Declare.set_xml_declare_constant
+ (function (internal,(sp,kn)) ->
+ match !proof_to_export with
+ None ->
+ print internal (Libnames.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 kn Cic2acic.Constant in
+ show_pftreestate internal fn pftreestate
+ (Names.id_of_label (Names.label kn)) ;
+ proof_to_export := None)
+;;
+
+let _ =
+ Declare.set_xml_declare_inductive
+ (function (isrecord,(sp,kn)) ->
+ print false (Libnames.IndRef (kn,0)) (kind_of_inductive isrecord kn)
+ xml_library_root)
+;;
+
+let _ =
+ Vernac.set_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 _ =
+ Vernac.set_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
+ end ;
+ Util.option_iter
+ (fun fn ->
+ let coqdoc = Coq_config.bindir^"/coqdoc" in
+ let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
+ let dir = Util.out_some xml_library_root in
+ let command cmd =
+ if Sys.command cmd <> 0 then
+ Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
+ in
+ command (coqdoc^options^" -d "^dir^" "^fn^".v");
+ let dot = if fn.[0]='/' then "." else "" in
+ command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
+ command ("rm "^fn^".v");
+ print_string("\nWriting on file \"" ^ fn ^ ".xml\" was succesful\n"))
+ ofn)
+;;
+
+let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;;
+
+let uri_of_dirpath dir =
+ "/" ^ String.concat "/"
+ (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
+;;
+
+let _ =
+ Lib.set_xml_open_section
+ (fun _ ->
+ let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in
+ theory_output_string ("<ht:SECTION uri=\""^s^"\">"))
+;;
+
+let _ =
+ Lib.set_xml_close_section
+ (fun _ -> theory_output_string "</ht:SECTION>")
+;;
+
+let _ =
+ Library.set_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) (Names.string_of_dirpath d)))
+;;
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
new file mode 100644
index 00000000..9a7464bd
--- /dev/null
+++ b/contrib/xml/xmlcommand.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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 $Id: xmlcommand.mli,v 1.18.2.2 2004/07/16 19:30:15 herbelin Exp $ i*)
+
+(* 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
+
+(* set_print_proof_tree f *)
+(* sets a callback function f to export the proof_tree to XML *)
+val set_print_proof_tree :
+ (string ->
+ Evd.evar_map ->
+ Proof_type.proof_tree ->
+ Term.constr Proof2aproof.ProofTreeHash.t ->
+ Proof_type.proof_tree Proof2aproof.ProofTreeHash.t ->
+ string Acic.CicHash.t -> Xml.token Stream.t) ->
+ unit
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
new file mode 100644
index 00000000..2bc686f7
--- /dev/null
+++ b/contrib/xml/xmlentries.ml4
@@ -0,0 +1,40 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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: "parsing/grammar.cma" i*)
+
+(* $Id: xmlentries.ml4,v 1.12.2.2 2004/07/16 19:30:15 herbelin Exp $ *)
+
+open Util;;
+open Vernacinterp;;
+
+open Extend;;
+open Genarg;;
+open Pp;;
+open Pcoq;;
+
+(* File name *)
+
+VERNAC ARGUMENT EXTEND filename
+| [ "File" string(fn) ] -> [ Some fn ]
+| [ ] -> [ None ]
+END
+
+(* Print XML and Show XML *)
+
+VERNAC COMMAND EXTEND Xml
+| [ "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 2025-01-28 19:24:40 +0000