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