diff options
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/COPYRIGHT | 25 | ||||
| -rw-r--r-- | plugins/xml/README | 269 | ||||
| -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 | 942 | ||||
| -rw-r--r-- | plugins/xml/doubleTypeInference.ml | 273 | ||||
| -rw-r--r-- | plugins/xml/doubleTypeInference.mli | 24 | ||||
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 136 | ||||
| -rw-r--r-- | plugins/xml/proof2aproof.ml | 78 | ||||
| -rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 205 | ||||
| -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 | 13 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 691 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.mli | 39 | ||||
| -rw-r--r-- | plugins/xml/xmlentries.ml4 | 38 |
21 files changed, 15 insertions, 3716 deletions
diff --git a/plugins/xml/COPYRIGHT b/plugins/xml/COPYRIGHT deleted file mode 100644 index c8d231fd..00000000 --- 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 a45dd31a..e3bcdaf0 100644 --- a/plugins/xml/README +++ b/plugins/xml/README @@ -1,254 +1,15 @@ -(******************************************************************************) -(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) -(* Project Helm (http://helm.cs.unibo.it) *) -(* Project MoWGLI (http://mowgli.cs.unibo.it) *) -(* *) -(* Coq Exportation to XML *) -(* *) -(******************************************************************************) - -This module provides commands to export a piece of Coq library in XML format. -Only the information relevant to proof-checking and proof-rendering is exported, -i.e. only the CIC proof objects (lambda-terms). - -This document is tructured in the following way: - 1. User documentation - 1.1. New vernacular commands available - 1.2. New coqc/coqtop flags and suggested usage - 1.3. How to exploit the XML files - 2. Technical informations - 2.1. Inner-types - 2.2. CIC with Explicit Named Substitutions - 2.3. The CIC with Explicit Named Substitutions XML DTD - -================================================================================ - USER DOCUMENTATION -================================================================================ - -======================================= -1.1. New vernacular commands available: -======================================= - -The new commands are: - - Print XML qualid. It prints in XML (to standard output) the - object whose qualified name is qualid and - its inner-types (see Sect. 2.1). - The inner-types are always printed - in their own XML file. If the object is a - constant, its type and body are also printed - as two distinct XML files. - The object printed is always the most - discharged form of the object (see - the Section command of the Coq manual). - - Print XML File "filename" qualid. Similar to "Print XML qualid". The generated - files are stored on the hard-disk using the - base file name "filename". - - Show XML Proof. It prints in XML the current proof in - progress. Its inner-types are also printed. - - Show XML File "filename" Proof. Similar to "Show XML Proof". The generated - files are stored on the hard-disk using - the base file name "filename". - - The verbosity of the previous commands is raised if the configuration - parameter verbose of xmlcommand.ml is set to true at compile time. - -============================================== -1.2. New coqc/coqtop flags and suggested usage -============================================== - - The following flag has been added to coqc and coqtop: - - -xml export XML files either to the hierarchy rooted in - the directory $COQ_XML_LIBRARY_ROOT (if the environment - variable is set) or to stdout (if unset) - - If the flag is set, every definition or declaration is immediately - exported to XML. The XML files describe the user-provided non-discharged - form of the definition or declaration. - - - The coq_makefile utility has also been modified to easily allow XML - exportation: - - make COQ_XML=-xml (or, equivalently, setting the environment - variable COQ_XML) - - - The suggested usage of the module is the following: - - 1. add to your own contribution a valid Make file and use coq_makefile - to generate the Makefile from the Make file. - *WARNING:* Since logical names are used to structure the XML hierarchy, - always add to the Make file at least one "-R" option to map physical - file names to logical module paths. See the Coq manual for further - informations on the -R flag. - 2. set $COQ_XML_LIBRARY_ROOT to the directory where the XML file hierarchy - must be physically rooted. - 3. compile your contribution with "make COQ_XML=-xml" - - -================================= -1.3. How to exploit the XML files -================================= - - Once the information is exported to XML, it becomes possible to implement - services that are completely Coq-independent. Projects HELM and MoWGLI - already provide rendering, searching and data mining functionalities. - - In particular, the standard library and contributions of Coq can be - browsed and searched on the HELM web site: - - http://helm.cs.unibo.it/library.html - - - If you want to publish your own contribution so that it is included in the - HELM library, use the MoWGLI prototype upload form: - - http://mowgli.cs.unibo.it - - -================================================================================ - TECHNICAL INFORMATIONS -================================================================================ - -========================== -2.1. Inner-types -========================== - -In order to do proof-rendering (for example in natural language), -some redundant typing information is required, i.e. the type of -at least some of the subterms of the bodies and types. So, each -new command described in section 1.1 print not only -the object, but also another XML file in which you can find -the type of all the subterms of the terms of the printed object -which respect the following conditions: - - 1. It's sort is Prop or CProp (the "sort"-like definition used in - CoRN to type computationally relevant predicative propositions). - 2. It is not a cast or an atomic term, i.e. it's root is not a CAST, REL, - VAR, MUTCONSTR or CONST. - 3. If it's root is a LAMBDA, then the root's parent node is not a LAMBDA, - i.e. only the type of the outer LAMBDA of a block of nested LAMBDAs is - printed. - -The rationale for the 3rd condition is that the type of the inner LAMBDAs -could be easily computed starting from the type of the outer LAMBDA; moreover, -the types of the inner LAMBDAs requires a lot of disk/memory space: removing -the 3rd condition leads to XML file that are two times as big as the ones -exported appling the 3rd condition. - -========================================== -2.2. CIC with Explicit Named Substitutions -========================================== - -The exported files are and XML encoding of the lambda-terms used by the -Coq system. The implementative details of the Coq system are hidden as much -as possible, so that the XML DTD is a straightforward encoding of the -Calculus of (Co)Inductive Constructions. - -Nevertheless, there is a feature of the Coq system that can not be -hidden in a completely satisfactory way: discharging. In Coq it is possible -to open a section, declare variables and use them in the rest of the section -as if they were axiom declarations. Once the section is closed, every definition -and theorem in the section is discharged by abstracting it over the section -variables. Variable declarations as well as section declarations are entirely -dropped. Since we are interested in an XML encoding of definitions and -theorems as close as possible to those directly provided the user, we -do not want to export discharged forms. Exporting non-discharged theorem -and definitions together with theorems that rely on the discharged forms -obliges the tools that work on the XML encoding to implement discharging to -achieve logical consistency. Moreover, the rendering of the files can be -misleading, since hyperlinks can be shown between occurrences of the discharge -form of a definition and the non-discharged definition, that are different -objects. - -To overcome the previous limitations, Claudio Sacerdoti Coen developed in his -PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions -with Explicit Named Substitutions, that is a slight extension of CIC where -discharging is not necessary. The DTD of the exported XML files describes -constants, inductive types and variables of the Calculus of (Co)Inductive -Constructions with Explicit Named Substitions. The conversion to the new -calculus is performed during the exportation phase. - -The following example shows a very small Coq development together with its -version in CIC with Explicit Named Substitutions. - -# CIC version: # -Section S. - Variable A : Prop. - - Definition impl := A -> A. - - Theorem t : impl. (* uses the undischarged form of impl *) - Proof. - exact (fun (a:A) => a). - Qed. - -End S. - -Theorem t' : (impl False). (* uses the discharged form of impl *) - Proof. - exact (t False). (* uses the discharged form of t *) - Qed. - -# Corresponding CIC with Explicit Named Substitutions version: # -Section S. - Variable A : Prop. - - Definition impl(A) := A -> A. (* theorems and definitions are - explicitly abstracted over the - variables. The name is sufficient - to completely describe the abstraction *) - - Theorem t(A) : impl. (* impl where A is not instantiated *) - Proof. - exact (fun (a:A) => a). - Qed. - -End S. - -Theorem t'() : impl{False/A}. (* impl where A is instantiated with False - Notice that t' does not depend on A *) - Proof. - exact t{False/A}. (* t where A is instantiated with False *) - Qed. - -Further details on the typing and reduction rules of the calculus can be -found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency -of the calculus is also proved. - -====================================================== -2.3. The CIC with Explicit Named Substitutions XML DTD -====================================================== - -A copy of the DTD can be found in the file "cic.dtd". - -<ConstantType> is the root element of the files that correspond to - constant types. -<ConstantBody> is the root element of the files that correspond to - constant bodies. It is used only for closed definitions and - theorems (i.e. when no metavariable occurs in the body - or type of the constant) -<CurrentProof> is the root element of the file that correspond to - the body of a constant that depends on metavariables - (e.g. unfinished proofs) -<Variable> is the root element of the files that correspond to variables -<InductiveTypes> is the root element of the files that correspond to blocks - of mutually defined inductive definitions - -The elements - <LAMBDA>,<CAST>,<PROD>,<REL>,<SORT>,<APPLY>,<VAR>,<META>, <IMPLICIT>,<CONST>, - <LETIN>,<MUTIND>,<MUTCONSTRUCT>,<MUTCASE>,<FIX> and <COFIX> -are used to encode the constructors of CIC. The sort or type attribute of the -element, if present, is respectively the sort or the type of the term, that -is a sort because of the typing rules of CIC. - -The element <instantiate> correspond to the application of an explicit named -substitution to its first argument, that is a reference to a definition -or declaration in the environment. - -All the other elements are just syntactic sugar. +The xml export plugin for Coq has been discontinued for lack of users: +it was most certainly broken while imposing a non-negligible cost on +Coq development. Its purpose was to give export Coq's kernel objects +in xml form for treatment by external tools. + +If you are looking for such a tool, you may want to look at commit +7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 responsible for the deletion +of this plugin (for instance, git checkout +7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9^ including the "^", will lead +you to the last commit before the xml plugin was deleted). + +Bear in mind, however, that the plugin was not working properly at the +time. You may want instead to write to the original author of the +plugin, Claudio Sacerdoti-Coen at sacerdot@cs.unibo.it. He has a +stable version of the plugin for an old version of Coq. diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml deleted file mode 100644 index 653c2b7b..00000000 --- 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 = identifier * 'constr context_entry -type context = constr hypothesis list - -type conjecture = existential_key * context * constr -type metasenv = conjecture list - -(* list of couples section path -- variables defined in that section *) -type params = (string * uri list) list - -type obj = - Constant of string * (* id, *) - constr option * constr * (* value, type, *) - params (* parameters *) - | Variable of - string * constr option * constr * (* name, body, type *) - params (* parameters *) - | CurrentProof of - string * metasenv * (* name, conjectures, *) - constr * constr (* value, type *) - | InductiveDefinition of - inductiveType list * (* inductive types , *) - params * int (* parameters,n ind. pars*) -and inductiveType = - identifier * bool * constr * (* typename, inductive, arity *) - constructor list (* constructors *) -and constructor = - identifier * constr (* id, type *) - -type aconstr = - | ARel of id * int * id * identifier - | AVar of id * uri - | AEvar of id * existential_key * aconstr list - | ASort of id * sorts - | ACast of id * aconstr * aconstr - | AProds of (id * name * aconstr) list * aconstr - | ALambdas of (id * name * aconstr) list * aconstr - | ALetIns of (id * name * aconstr) list * aconstr - | AApp of id * aconstr list - | AConst of id * explicit_named_substitution * uri - | AInd of id * explicit_named_substitution * uri * int - | AConstruct of id * explicit_named_substitution * uri * int * int - | ACase of id * uri * int * aconstr * aconstr * aconstr list - | AFix of id * int * ainductivefun list - | ACoFix of id * int * acoinductivefun list -and ainductivefun = - id * identifier * int * aconstr * aconstr -and acoinductivefun = - id * identifier * aconstr * aconstr -and explicit_named_substitution = id option * (uri * aconstr) list - -type acontext = (id * aconstr hypothesis) list -type aconjecture = id * existential_key * acontext * aconstr -type ametasenv = aconjecture list - -type aobj = - AConstant of id * string * (* id, *) - aconstr option * aconstr * (* value, type, *) - params (* parameters *) - | AVariable of id * - string * aconstr option * aconstr * (* name, body, type *) - params (* parameters *) - | ACurrentProof of id * - string * ametasenv * (* name, conjectures, *) - aconstr * aconstr (* value, type *) - | AInductiveDefinition of id * - anninductiveType list * (* inductive types , *) - params * int (* parameters,n ind. pars*) -and anninductiveType = - id * identifier * bool * aconstr * (* typename, inductive, arity *) - annconstructor list (* constructors *) -and annconstructor = - identifier * aconstr (* id, type *) diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 deleted file mode 100644 index 97f7e2bd..00000000 --- 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 - [] -> Util.anomaly "find_last_id: empty list" - | [id,_,_] -> id - | _::tl -> find_last_id tl -;; - -let export_existential = string_of_int - -let print_term ids_to_inner_sorts = - let rec aux = - let module A = Acic in - let module N = Names in - let module X = Xml in - function - A.ARel (id,n,idref,b) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_empty "REL" - ["value",(string_of_int n) ; "binder",(N.string_of_id b) ; - "id",id ; "idref",idref; "sort",sort] - | A.AVar (id,uri) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort] - | A.AEvar (id,n,l) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" - ["no",(export_existential n) ; "id",id ; "sort",sort] - (List.fold_left - (fun i t -> - [< i ; X.xml_nempty "substitution" [] (aux t) >] - ) [< >] (List.rev l)) - | A.ASort (id,s) -> - let string_of_sort = - match Term.family_of_sort s with - Term.InProp -> "Prop" - | Term.InSet -> "Set" - | Term.InType -> "Type" - in - X.xml_empty "SORT" ["value",string_of_sort ; "id",id] - | A.AProds (prods,t) -> - let last_id = find_last_id prods in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "PROD" ["type",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in - let attrs = - ("id",id)::("type",sort):: - match binder with - Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.string_of_id b] - in - [< X.xml_nempty "decl" attrs (aux s) ; i >] - ) [< >] prods ; - X.xml_nempty "target" [] (aux t) - >] - | A.ACast (id,v,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "CAST" ["id",id ; "sort",sort] - [< X.xml_nempty "term" [] (aux v) ; - X.xml_nempty "type" [] (aux t) - >] - | A.ALambdas (lambdas,t) -> - let last_id = find_last_id lambdas in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LAMBDA" ["sort",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in - let attrs = - ("id",id)::("type",sort):: - match binder with - Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.string_of_id b] - in - [< X.xml_nempty "decl" attrs (aux s) ; i >] - ) [< >] lambdas ; - X.xml_nempty "target" [] (aux t) - >] - | A.ALetIns (letins,t) -> - let last_id = find_last_id letins in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LETIN" ["sort",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in - let attrs = - ("id",id)::("sort",sort):: - match binder with - Names.Anonymous -> assert false - | Names.Name b -> ["binder",Names.string_of_id b] - in - [< X.xml_nempty "def" attrs (aux s) ; i >] - ) [< >] letins ; - X.xml_nempty "target" [] (aux t) - >] - | A.AApp (id,li) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "APPLY" ["id",id ; "sort",sort] - [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li) - >] - | A.AConst (id,subst,uri) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - let attrs = ["uri", uri ; "id",id ; "sort",sort] in - aux_subst (X.xml_empty "CONST" attrs) subst - | A.AInd (id,subst,uri,i) -> - let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in - aux_subst (X.xml_empty "MUTIND" attrs) subst - | A.AConstruct (id,subst,uri,i,j) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - let attrs = - ["uri", uri ; - "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; - "id",id ; "sort",sort] - in - aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst - | A.ACase (id,uri,typeno,ty,te,patterns) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "MUTCASE" - ["uriType", uri ; - "noType", (string_of_int typeno) ; - "id", id ; "sort",sort] - [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; - X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; - List.fold_left - (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >]) - [<>] patterns - >] - | A.AFix (id, no, funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "FIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] - [< List.fold_left - (fun i (id,fi,ai,ti,bi) -> - [< i ; - X.xml_nempty "FixFunction" - ["id",id ; "name", (Names.string_of_id fi) ; - "recIndex", (string_of_int ai)] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] - >] - ) [<>] funs - >] - | A.ACoFix (id,no,funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "COFIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] - [< List.fold_left - (fun i (id,fi,ti,bi) -> - [< i ; - X.xml_nempty "CofixFunction" - ["id",id ; "name", Names.string_of_id fi] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] - >] - ) [<>] funs - >] - and aux_subst target (id,subst) = - if subst = [] then - target - else - Xml.xml_nempty "instantiate" - (match id with None -> [] | Some id -> ["id",id]) - [< target ; - List.fold_left - (fun i (uri,arg) -> - [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >] - ) [<>] subst - >] - in - aux -;; - -let param_attribute_of_params params = - List.fold_right - (fun (path,l) i -> - List.fold_right - (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i' - ) l "" ^ match i with "" -> "" | i' -> " " ^ i' - ) params "" -;; - -let print_object uri ids_to_inner_sorts = - let rec aux = - let module A = Acic in - let module X = Xml in - function - A.ACurrentProof (id,n,conjectures,bo,ty) -> - let xml_for_current_proof_body = -(*CSC: Should the CurrentProof also have the list of variables it depends on? *) -(*CSC: I think so. Not implemented yet. *) - X.xml_nempty "CurrentProof" ["of",uri ; "id", id] - [< List.fold_left - (fun i (cid,n,canonical_context,t) -> - [< i ; - X.xml_nempty "Conjecture" - ["id", cid ; "no",export_existential n] - [< List.fold_left - (fun i (hid,t) -> - [< (match t with - n,A.Decl t -> - X.xml_nempty "Decl" - ["id",hid;"name",Names.string_of_id n] - (print_term ids_to_inner_sorts t) - | n,A.Def (t,_) -> - X.xml_nempty "Def" - ["id",hid;"name",Names.string_of_id n] - (print_term ids_to_inner_sorts t) - ) ; - i - >] - ) [< >] canonical_context ; - X.xml_nempty "Goal" [] - (print_term ids_to_inner_sorts t) - >] - >]) - [<>] (List.rev conjectures) ; - X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] - in - let xml_for_current_proof_type = - X.xml_nempty "ConstantType" ["name",n ; "id", id] - (print_term ids_to_inner_sorts ty) - in - let xmlbo = - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n"); - xml_for_current_proof_body - >] in - let xmlty = - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata - ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n"); - xml_for_current_proof_type - >] - in - xmlty, Some xmlbo - | A.AConstant (id,n,bo,ty,params) -> - let params' = param_attribute_of_params params in - let xmlbo = - match bo with - None -> None - | Some bo -> - Some - [< X.xml_cdata - "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata - ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ; - X.xml_nempty "ConstantBody" - ["for",uri ; "params",params' ; "id", id] - [< print_term ids_to_inner_sorts bo >] - >] - in - let xmlty = - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n"); - X.xml_nempty "ConstantType" - ["name",n ; "params",params' ; "id", id] - [< print_term ids_to_inner_sorts ty >] - >] - in - xmlty, xmlbo - | A.AVariable (id,n,bo,ty,params) -> - let params' = param_attribute_of_params params in - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n") ; - X.xml_nempty "Variable" ["name",n ; "params",params' ; "id", id] - [< (match bo with - None -> [<>] - | Some bo -> - X.xml_nempty "body" [] - (print_term ids_to_inner_sorts bo) - ) ; - X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) - >] - >], None - | A.AInductiveDefinition (id,tys,params,nparams) -> - let params' = param_attribute_of_params params in - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ - dtdname ^ "\">\n") ; - X.xml_nempty "InductiveDefinition" - ["noParams",string_of_int nparams ; - "id",id ; - "params",params'] - [< (List.fold_left - (fun i (id,typename,finite,arity,cons) -> - [< i ; - X.xml_nempty "InductiveType" - ["id",id ; "name",Names.string_of_id typename ; - "inductive",(string_of_bool finite) - ] - [< X.xml_nempty "arity" [] - (print_term ids_to_inner_sorts arity) ; - (List.fold_left - (fun i (name,lc) -> - [< i ; - X.xml_nempty "Constructor" - ["name",Names.string_of_id name] - (print_term ids_to_inner_sorts lc) - >]) [<>] cons - ) - >] - >] - ) [< >] tys - ) - >] - >], None - in - aux -;; - -let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = - let module C2A = Cic2acic in - let module X = Xml in - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^"\">\n"); - X.xml_nempty "InnerTypes" ["of",curi] - (Hashtbl.fold - (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> - [< x ; - X.xml_nempty "TYPE" ["of",id] - [< X.xml_nempty "synthesized" [] - (print_term ids_to_inner_sorts synty) ; - match expty with - None -> [<>] - | Some expty' -> - X.xml_nempty "expected" [] - (print_term ids_to_inner_sorts expty') - >] - >] - ) ids_to_inner_types [<>] - ) - >] -;; diff --git a/plugins/xml/cic.dtd b/plugins/xml/cic.dtd deleted file mode 100644 index c8035cab..00000000 --- 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 981503a6..00000000 --- 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 165bf83d..00000000 --- a/plugins/xml/cic2acic.ml +++ /dev/null @@ -1,942 +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 *) -(************************************************************************) - -(* 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_warn ("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 = - let module Ln = Libnames in - if Ln.is_dirpath_prefix_of basedir dir then - let ids = Names.repr_dirpath dir in - let rec remove_firsts n l = - match n,l with - (0,l) -> l - | (n,he::tl) -> remove_firsts (n-1) tl - | _ -> assert false - in - let ids' = - List.rev - (remove_firsts - (List.length (Names.repr_dirpath basedir)) - (List.rev ids)) - in - ids' - else Names.repr_dirpath dir -;; - - -let get_uri_of_var v pvars = - let module D = Decls in - let module N = Names in - let rec search_in_open_sections = - function - [] -> Util.error ("Variable "^v^" not found") - | he::tl as modules -> - let dirpath = N.make_dirpath modules in - if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then - modules - else - search_in_open_sections tl - in - let path = - if List.mem v pvars then - [] - else - search_in_open_sections (N.repr_dirpath (Lib.cwd ())) - in - "cic:" ^ - List.fold_left - (fun i x -> "/" ^ N.string_of_id 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 (Names.repr_dirpath l1) in - let l2' = List.rev (Names.repr_dirpath l2) in - let rec aux = - function - he::tl when tl = l2' -> [he] - | he::tl -> he::(aux tl) - | [] -> assert (l2' = []) ; [] - in - Names.make_dirpath (List.rev (aux l1')) -;; - -let token_list_of_path dir id tag = - let module N = Names in - let token_list_of_dirpath dirpath = - List.rev_map N.string_of_id (N.repr_dirpath dirpath) in - token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)] - -let token_list_of_kernel_name tag = - let module N = Names in - let module LN = Libnames in - let id,dir = match tag with - | Variable kn -> - N.id_of_label (N.label kn), Lib.cwd () - | Constant con -> - N.id_of_label (N.con_label con), - Lib.remove_section_part (LN.ConstRef con) - | Inductive kn -> - N.id_of_label (N.mind_label kn), - Lib.remove_section_part (LN.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 module LN = Libnames in - let dir = LN.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 *) - | _ -> Util.anomaly "family_of_term" -;; - -module CPropRetyping = - struct - module T = Term - - let outsort env sigma t = - family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t) - - let rec subst_type env sigma typ = function - | [] -> typ - | h::rest -> - match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with - | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Util.anomaly "Non-functional construction" - - - let sort_of_atomic_type env sigma ft args = - let rec concl_of_arity env ar = - match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma ar) with - | T.Prod (na, t, b) -> concl_of_arity (Environ.push_rel (na,None,t) env) b - | T.Sort s -> Coq_sort (T.family_of_sort s) - | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args)) - in concl_of_arity env ft - -let typeur sigma metamap = - let rec type_of env cstr= - match Term.kind_of_term cstr with - | T.Meta n -> - (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Util.anomaly "type_of: this is not a well-typed term") - | T.Rel n -> - let (_,_,ty) = Environ.lookup_rel n env in - T.lift n ty - | T.Var id -> - (try - let (_,_,ty) = Environ.lookup_named id env in - ty - with Not_found -> - Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) - | T.Const c -> - let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env (cb.Declarations.const_type) - | 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 -> Util.anomaly "type_of: 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) -> - T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) - | T.Fix ((_,i),(_,tys,_)) -> tys.(i) - | T.CoFix (i,(_,tys,_)) -> tys.(i) - | T.App(f,args)-> - T.strip_outer_cast - (subst_type env sigma (type_of env f) (Array.to_list args)) - | T.Cast (c,_, t) -> t - | T.Sort _ | T.Prod _ -> - match sort_of env cstr with - Coq_sort T.InProp -> T.mkProp - | Coq_sort T.InSet -> T.mkSet - | Coq_sort T.InType -> T.mkType Univ.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 _ -> - Util.anomaly "sort_of: Not a type (1)" - | _ -> outsort env sigma (type_of env t) - - and sort_family_of env t = - match T.kind_of_term t with - | T.Cast (c,_, s) when T.isSort s -> family_of_term s - | T.Sort (T.Prop c) -> Coq_sort T.InType - | T.Sort (T.Type u) -> Coq_sort T.InType - | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2 - | T.App(f,args) -> - sort_of_atomic_type env sigma (type_of env f) args - | T.Lambda _ | T.Fix _ | T.Construct _ -> - Util.anomaly "sort_of: Not a type (1)" - | _ -> outsort env sigma (type_of env t) - - in type_of, sort_of, sort_family_of - - let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c - let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c - - end -;; - -let get_sort_family_of env evar_map ty = - CPropRetyping.get_sort_family_of env evar_map ty -;; - -let type_as_sort env evar_map ty = -(* CCorn code *) - family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env evar_map ty) -;; - -let is_a_Prop = - function - "Prop" - | "CProp" -> true - | _ -> false -;; - -(* Main Functions *) - -type anntypes = - {annsynthesized : Acic.aconstr ; annexpected : Acic.aconstr option} -;; - -let gen_id seed = - let res = "i" ^ string_of_int !seed in - incr seed ; - res -;; - -let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids = - fun father t -> - let res = gen_id seed in - Hashtbl.add ids_to_father_ids res father ; - Hashtbl.add ids_to_terms res t ; - Acic.CicHash.add constr_to_ids t res ; - res -;; - -let source_id_of_id id = "#source#" ^ id;; - -let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types - ?(fake_dependent_products=false) env idrefs evar_map t expectedty -= - let module D = DoubleTypeInference in - let module E = Environ in - let module N = Names in - let module A = Acic in - let module T = Term in - let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in - (* CSC: do you have any reasonable substitute for 503? *) - let terms_to_types = Acic.CicHash.create 503 in - D.double_type_of env evar_map t expectedty terms_to_types ; - let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env - idrefs ?(subst=None,[]) tt - = - let fresh_id'' = fresh_id' father tt in - let aux' = aux computeinnertypes (Some fresh_id'') [] in - let string_of_sort_family = - function - Coq_sort T.InProp -> "Prop" - | Coq_sort T.InSet -> "Set" - | Coq_sort T.InType -> "Type" - | CProp -> "CProp" - in - let string_of_sort t = - string_of_sort_family - (type_as_sort env evar_map t) - in - let ainnertypes,innertype,innersort,expected_available = - let {D.synthesized = synthesized; D.expected = expected} = - if computeinnertypes then -try - Acic.CicHash.find terms_to_types tt -with e when e <> Sys.Break -> -(*CSC: Warning: it really happens, for example in Ring_theory!!! *) -Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.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. *) - {D.synthesized = - Reductionops.nf_beta evar_map - (CPropRetyping.get_type_of env evar_map - (Termops.refresh_universes tt)) ; - D.expected = None} - in -(* Debugging only: -print_endline "TERMINE:" ; flush stdout ; -Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ; -print_endline "TIPO:" ; flush stdout ; -Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ; -print_endline "ENVIRONMENT:" ; flush stdout ; -Pp.ppnl (Printer.pr_context_of env) ; flush stdout ; -print_endline "FINE_ENVIRONMENT" ; flush stdout ; -*) - let innersort = - 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 = Libnames.global_of_constr h in - let sp = - match g with - Libnames.ConstructRef ((induri,_),_) - | Libnames.IndRef (induri,_) -> - Nametab.path_of_global (Libnames.IndRef (induri,0)) - | Libnames.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.map Names.string_of_id (List.rev he1')) ^ "/" - ^ (Names.string_of_id he1_id) ^ ".var" - in - (he1'',he2)::subst, extra_args, uninst - in - get_explicit_subst variables t' - in - let uninst_vars_length = List.length uninst_vars in - if uninst_vars_length > 0 then - (* Not enough arguments provided. We must eta-expand! *) - let un_args,_ = - T.decompose_prod_n uninst_vars_length - (CPropRetyping.get_type_of env evar_map tt) - in - let eta_expanded = - let arguments = - List.map (T.lift uninst_vars_length) t @ - Termops.rel_list 0 uninst_vars_length - in - Unshare.unshare - (T.lamn uninst_vars_length un_args - (T.applistc h arguments)) - in - D.double_type_of env evar_map eta_expanded - None terms_to_types ; - Hashtbl.remove ids_to_inner_types fresh_id'' ; - aux' env idrefs eta_expanded - else - compute_result_if_eta_expansion_not_required subst residual_args - in - - (* Now that we have all the auxiliary functions we *) - (* can finally proceed with the main case analysis. *) - match T.kind_of_term tt with - T.Rel n -> - let id = - match List.nth (E.rel_context env) (n - 1) with - (N.Name id,_,_) -> id - | (N.Anonymous,_,_) -> Nameops.make_ident "_" None - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - A.ARel (fresh_id'', n, List.nth idrefs (n-1), id) - | T.Var id -> - let pvars = Termops.ids_of_named_context (E.named_context env) in - let pvars = List.map N.string_of_id pvars in - let path = get_uri_of_var (N.string_of_id id) pvars in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - A.AVar - (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var") - | T.Evar (n,l) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - A.AEvar - (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Util.anomaly "Meta met during exporting to XML" - | T.Sort s -> A.ASort (fresh_id'', s) - | T.Cast (v,_, t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - A.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t) - | T.Prod (n,s,t) -> - let n' = - match n with - N.Anonymous -> N.Anonymous - | _ -> - if not fake_dependent_products && T.noccurn 1 t then - N.Anonymous - else - N.Name - (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 - T.Prod _ -> true - | _ -> false - in - (fresh_id'', n', aux' env idrefs s):: - (if father_is_prod then - passed_lambdas_or_prods_or_letins - else []) - in - let new_env = E.push_rel (n', None, s) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term t with - T.Prod _ -> - aux computeinnertypes (Some fresh_id'') new_passed_prods - new_env new_idrefs t - | _ -> - A.AProds (new_passed_prods, aux' new_env new_idrefs t)) - | T.Lambda (n,s,t) -> - let n' = - match n with - N.Anonymous -> N.Anonymous - | _ -> - N.Name (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 - T.Lambda _ -> true - | _ -> false - in - if is_a_Prop innersort && - ((not father_is_lambda) || expected_available) - then add_inner_type fresh_id'' ; - let new_passed_lambdas = - (fresh_id'',n', aux' env idrefs s):: - (if father_is_lambda then - passed_lambdas_or_prods_or_letins - else []) in - let new_env = E.push_rel (n', None, s) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term t with - T.Lambda _ -> - aux computeinnertypes (Some fresh_id'') new_passed_lambdas - new_env new_idrefs t - | _ -> - let t' = aux' new_env new_idrefs t in - (* eta-expansion for explicit named substitutions *) - (* can create nested Lambdas. Here we perform the *) - (* flattening. *) - match t' with - A.ALambdas (lambdas, t'') -> - A.ALambdas (lambdas@new_passed_lambdas, t'') - | _ -> - A.ALambdas (new_passed_lambdas, t') - ) - | T.LetIn (n,s,t,d) -> - let id = - match n with - N.Anonymous -> N.id_of_string "_X" - | N.Name id -> id - in - let n' = - N.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 - T.LetIn _ -> true - | _ -> false - in - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let new_passed_letins = - (fresh_id'',n', aux' env idrefs s):: - (if father_is_letin then - passed_lambdas_or_prods_or_letins - else []) in - let new_env = E.push_rel (n', Some s, t) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term d with - T.LetIn _ -> - aux computeinnertypes (Some fresh_id'') new_passed_letins - new_env new_idrefs d - | _ -> A.ALetIns - (new_passed_letins, aux' new_env new_idrefs d)) - | T.App (h,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let - compute_result_if_eta_expansion_not_required subst residual_args - = - let residual_args_not_empty = 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 - A.AApp (fresh_id'', h'::residual_args) - else - h' - in - let t' = - Array.fold_right (fun x i -> (aux' env idrefs x)::i) t [] - in - explicit_substitute_and_eta_expand_if_required h - (Array.to_list t) t' - compute_result_if_eta_expansion_not_required - | T.Const kn -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - let compute_result_if_eta_expansion_not_required _ _ = - A.AConst (fresh_id'', subst, (uri_of_kernel_name (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 - | T.Ind (kn,i) -> - let compute_result_if_eta_expansion_not_required _ _ = - A.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 - | T.Construct ((kn,i),j) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - let compute_result_if_eta_expansion_not_required _ _ = - A.AConstruct - (fresh_id'', subst, (uri_of_kernel_name (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 - | T.Case ({T.ci_ind=(kn,i)},ty,term,a) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let a' = - Array.fold_right (fun x i -> (aux' env idrefs x)::i) a [] - in - A.ACase - (fresh_id'', (uri_of_kernel_name (Inductive kn)), i, - aux' env idrefs ty, aux' env idrefs term, a') - | T.Fix ((ai,i),(f,t,b)) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then add_inner_type fresh_id'' ; - let fresh_idrefs = - Array.init (Array.length t) (function _ -> gen_id seed) in - let new_idrefs = - (List.rev (Array.to_list fresh_idrefs)) @ idrefs - in - let f' = - let ids = ref (Termops.ids_of_context env) in - Array.map - (function - N.Anonymous -> Util.error "Anonymous fix function met" - | N.Name id as n -> - let res = N.Name (Namegen.next_name_away n !ids) in - ids := id::!ids ; - res - ) f - in - A.AFix (fresh_id'', i, - Array.fold_right - (fun (id,fi,ti,bi,ai) i -> - let fi' = - match fi with - N.Name fi -> fi - | N.Anonymous -> Util.error "Anonymous fix function met" - in - (id, fi', ai, - aux' env idrefs ti, - aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i) - (Array.mapi - (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f' - ) [] - ) - | T.CoFix (i,(f,t,b)) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then add_inner_type fresh_id'' ; - let fresh_idrefs = - Array.init (Array.length t) (function _ -> gen_id seed) in - let new_idrefs = - (List.rev (Array.to_list fresh_idrefs)) @ idrefs - in - let f' = - let ids = ref (Termops.ids_of_context env) in - Array.map - (function - N.Anonymous -> Util.error "Anonymous fix function met" - | N.Name id as n -> - let res = N.Name (Namegen.next_name_away n !ids) in - ids := id::!ids ; - res - ) f - in - A.ACoFix (fresh_id'', i, - Array.fold_right - (fun (id,fi,ti,bi) i -> - let fi' = - match fi with - N.Name fi -> fi - | N.Anonymous -> Util.error "Anonymous fix function met" - in - (id, fi', - aux' env idrefs ti, - aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i) - (Array.mapi - (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f' - ) [] - ) - in - aux computeinnertypes None [] env idrefs t -;; - -(* 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 module A = Acic in - let ids_to_terms = Hashtbl.create 503 in - let constr_to_ids = Acic.CicHash.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let ids_to_conjectures = Hashtbl.create 11 in - let ids_to_hypotheses = Hashtbl.create 127 in - let hypotheses_seed = ref 0 in - let conjectures_seed = ref 0 in - let seed = ref 0 in - let acic_term_of_cic_term_context' = - acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types in -(*CSC: is this the right env to use? Hhmmm. There is a problem: in *) -(*CSC: Global.env () the object we are exporting is already defined, *) -(*CSC: either in the environment or in the named context (in the case *) -(*CSC: of variables. Is this a problem? *) - let env = Global.env () in - let acic_term_of_cic_term' ?fake_dependent_products = - acic_term_of_cic_term_context' ?fake_dependent_products env [] sigma in -(*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *) -(*CSC: a modified version of the already existent fresh_id function *) - let fresh_id () = - let res = "i" ^ string_of_int !seed in - incr seed ; - res - in - let aobj = - match obj with - A.Constant (id,bo,ty,params) -> - let abo = - match bo with - None -> None - | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty)) - in - let aty = acic_term_of_cic_term' ty None in - A.AConstant (fresh_id (),id,abo,aty,params) - | A.Variable (id,bo,ty,params) -> - let abo = - match bo with - Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) - | None -> None - in - let aty = acic_term_of_cic_term' ty None in - A.AVariable (fresh_id (),id,abo,aty,params) - | A.CurrentProof (id,conjectures,bo,ty) -> - let aconjectures = - List.map - (function (i,canonical_context,term) as conjecture -> - let cid = "c" ^ string_of_int !conjectures_seed in - Hashtbl.add ids_to_conjectures cid conjecture ; - incr conjectures_seed ; - let canonical_env,idrefs',acanonical_context = - let rec aux env idrefs = - function - [] -> env,idrefs,[] - | ((n,decl_or_def) as hyp)::tl -> - let hid = "h" ^ string_of_int !hypotheses_seed in - let new_idrefs = hid::idrefs in - Hashtbl.add ids_to_hypotheses hid hyp ; - incr hypotheses_seed ; - match decl_or_def with - A.Decl t -> - let final_env,final_idrefs,atl = - aux (Environ.push_rel (Names.Name n,None,t) env) - new_idrefs tl - in - let at = - acic_term_of_cic_term_context' env idrefs sigma t None - in - final_env,final_idrefs,(hid,(n,A.Decl at))::atl - | A.Def (t,ty) -> - let final_env,final_idrefs,atl = - aux - (Environ.push_rel (Names.Name n,Some t,ty) env) - new_idrefs tl - in - let at = - acic_term_of_cic_term_context' env idrefs sigma t None - in - let dummy_never_used = - let s = "dummy_never_used" in - A.ARel (s,99,s,Names.id_of_string s) - in - final_env,final_idrefs, - (hid,(n,A.Def (at,dummy_never_used)))::atl - in - aux env [] canonical_context - in - let aterm = - acic_term_of_cic_term_context' canonical_env idrefs' sigma term - None - in - (cid,i,List.rev acanonical_context,aterm) - ) conjectures in - let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in - let aty = acic_term_of_cic_term_context' env [] sigma ty None in - A.ACurrentProof (fresh_id (),id,aconjectures,abo,aty) - | A.InductiveDefinition (tys,params,paramsno) -> - let env' = - List.fold_right - (fun (name,_,arity,_) env -> - Environ.push_rel (Names.Name name, None, arity) env - ) (List.rev tys) env in - let idrefs = List.map (function _ -> gen_id seed) tys in - let atys = - List.map2 - (fun id (name,inductive,ty,cons) -> - let acons = - List.map - (function (name,ty) -> - (name, - acic_term_of_cic_term_context' ~fake_dependent_products:true - env' idrefs Evd.empty ty None) - ) cons - in - let aty = - acic_term_of_cic_term' ~fake_dependent_products:true ty None - in - (id,name,inductive,aty,acons) - ) (List.rev idrefs) tys - in - A.AInductiveDefinition (fresh_id (),atys,params,paramsno) - in - aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses -;; diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml deleted file mode 100644 index c22c16f0..00000000 --- a/plugins/xml/doubleTypeInference.ml +++ /dev/null @@ -1,273 +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 prerr_endline _ = ();; - -let cprop = - let module N = Names in - N.make_con - (N.MPfile - (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.make_dirpath []) - (N.mk_label "CProp") -;; - -let whd_betadeltaiotacprop env _evar_map ty = - let module R = Glob_term in - let module C = Closure in - let module CR = C.RedFlags in - (*** CProp is made Opaque ***) - let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in - C.whd_val (C.create_clos_infos flags env) (C.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 E = Environ in - (* the type part is the synthesized type *) - let judgement = - match T.kind_of_term cstr with - T.Meta n -> - Util.error - "DoubleTypeInference.double_type_of: found a non-instanciated goal" - - | T.Evar ((n,l) as ev) -> - let ty = Unshare.unshare (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 (T.replace_vars [n,he1] ty)) - ) tl2 - in - iter tl1 tl2' - | _,_ -> assert false - in - (* for side effects only *) - iter (List.rev (Array.to_list l)) (List.rev evar_context) ; - E.make_judge cstr jty - - | T.Rel n -> - Typeops.judge_of_relative env n - - | T.Var id -> - Typeops.judge_of_variable env id - - | T.Const c -> - E.make_judge cstr (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 - let (j,_) = Typeops.judge_of_case env ci pj cj lfj in - j - - | T.Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let fix = (vni,recdef') in - E.make_judge (T.mkFix fix) tys.(i) - - | T.CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let cofix = (i,recdef') in - E.make_judge (T.mkCoFix cofix) tys.(i) - - | T.Sort (T.Prop c) -> - Typeops.judge_of_prop_contents c - - | T.Sort (T.Type u) -> -(*CSC: In case of need, I refresh the universe. But exportation of the *) -(*CSC: right universe level information is destroyed. It must be changed *) -(*CSC: again once Judicael will introduce his non-bugged algebraic *) -(*CSC: universes. *) -(try - Typeops.judge_of_type u - with e when e <> Sys.Break -> - (* Successor of a non universe-variable universe anomaly *) - (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ; - Typeops.judge_of_type (Termops.new_univ ()) -) - - | T.App (f,args) -> - let expected_head = - Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in - let j = execute env sigma f (Some expected_head) in - let expected_args = - let rec aux typ = - function - [] -> [] - | hj::restjl -> - match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with - T.Prod (_,c1,c2) -> - (Some (Reductionops.nf_beta sigma c1)) :: - (aux (T.subst1 hj c2) restjl) - | _ -> assert false - in - Array.of_list (aux j.Environ.uj_type (Array.to_list args)) - in - let jl = execute_array env sigma args expected_args in - let (j,_) = Typeops.judge_of_apply env j jl in - j - - | T.Lambda (name,c1,c2) -> - let j = execute env sigma c1 None in - let var = type_judgment env sigma j in - let env1 = E.push_rel (name,None,var.E.utj_val) env in - let expectedc2type = - match expectedty with - None -> None - | Some ety -> - match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with - T.Prod (_,_,expected_target_type) -> - Some (Reductionops.nf_beta 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.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ; - Acic.CicHash.add subterms_to_types cstr types ; - E.make_judge cstr res - - - and execute_recdef env sigma (names,lar,vdef) = - let length = Array.length lar in - let larj = - execute_array env sigma lar (Array.make length None) in - let lara = Array.map (assumption_of_judgment env sigma) larj in - let env1 = Environ.push_rec_types (names,lara,vdef) env in - let expectedtypes = - Array.map (function i -> Some (Term.lift length i)) lar - in - let vdefj = execute_array env1 sigma vdef expectedtypes in - let vdefv = Array.map Environ.j_val vdefj in - (names,lara,vdefv) - - and execute_array env sigma v expectedtypes = - let jl = - execute_list env sigma (Array.to_list v) (Array.to_list expectedtypes) - in - Array.of_list jl - - and execute_list env sigma = - List.map2 (execute env sigma) - -in - ignore (execute env sigma cstr expectedty) -;; diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli deleted file mode 100644 index 5c00bdc6..00000000 --- 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/dumptree.ml4 b/plugins/xml/dumptree.ml4 deleted file mode 100644 index 76364541..00000000 --- a/plugins/xml/dumptree.ml4 +++ /dev/null @@ -1,136 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This module provides the "Dump Tree" command that allows dumping the - current state of the proof stree in XML format *) - -(** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *) - -(*i camlp4deps: "parsing/grammar.cma" i*) -open Tacexpr;; -open Decl_mode;; -open Printer;; -open Pp;; -open Environ;; -open Format;; -open Proof_type;; -open Evd;; -open Termops;; -open Ppconstr;; -open Names;; - -exception Different - -let xmlstream s = - (* In XML we want to print the whole stream so we can force the evaluation *) - Stream.of_list (List.map xmlescape (Stream.npeek max_int s)) -;; - -let thin_sign osign sign = - Sign.fold_named_context - (fun (id,c,ty as d) sign -> - try - if Sign.lookup_named id osign = (id,c,ty) then sign - else raise Different - with Not_found | Different -> Environ.push_named_context_val d sign) - sign ~init:Environ.empty_named_context_val -;; - -let pr_tactic_xml = function - | TacArg (_,Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>" - | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>" -;; - -let pr_proof_instr_xml instr = - Ppdecl_proof.pr_proof_instr (Global.env()) instr -;; - -let pr_rule_xml pr = function - | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>" - | Nested(cmpd, subtree) -> - hov 2 (str "<cmpdrule>" ++ fnl () ++ - begin match cmpd with - Tactic (texp, _) -> pr_tactic_xml texp - end ++ fnl () - ++ pr subtree - ) ++ fnl () ++ str "</cmpdrule>" - | Daimon -> str "<daimon/>" - | Decl_proof _ -> str "<proof/>" -;; - -let pr_var_decl_xml env (id,c,typ) = - let ptyp = print_constr_env env typ in - match c with - | None -> - (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\"/>") - | Some c -> - (* Force evaluation *) - let pb = print_constr_env env c in - (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\" body=\"" ++ - xmlstream pb ++ str "\"/>") -;; - -let pr_rel_decl_xml env (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> - (* Force evaluation *) - let pb = print_constr_env env c in - (str" body=\"" ++ xmlstream pb ++ str "\"") in - let ptyp = print_constr_env env typ in - let pid = - match na with - | Anonymous -> mt () - | Name id -> str " id=\"" ++ pr_id id ++ str "\"" - in - (str "<hyp" ++ pid ++ str " type=\"" ++ xmlstream ptyp ++ str "\"" ++ pbody ++ str "/>") -;; - -let pr_context_xml env = - let sign_env = - fold_named_context - (fun env d pp -> pp ++ pr_var_decl_xml env d) - env ~init:(mt ()) - in - let db_env = - fold_rel_context - (fun env d pp -> pp ++ pr_rel_decl_xml env d) - env ~init:(mt ()) - in - (sign_env ++ db_env) -;; - -let pr_subgoal_metas_xml metas env= - let pr_one (meta, typ) = - fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++ - str "\"/>" - in - List.fold_left (++) (mt ()) (List.map pr_one metas) -;; - -let pr_goal_xml sigma g = - let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in - if Decl_mode.try_get_info sigma g = None then - (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++ - xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++ - str "\"/>" ++ - (pr_context_xml env)) ++ - fnl () ++ str "</goal>") - else - (hov 2 (str "<goal type=\"declarative\">" ++ - (pr_context_xml env)) ++ - fnl () ++ str "</goal>") -;; - -let print_proof_xml () = - Util.anomaly "Dump Tree command not supported in this version." - - -VERNAC COMMAND EXTEND DumpTree - [ "Dump" "Tree" ] -> [ print_proof_xml () ] -END diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml deleted file mode 100644 index 2d16190b..00000000 --- a/plugins/xml/proof2aproof.ml +++ /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 *) -(************************************************************************) - -(* Note: we can not use the Set module here because we _need_ physical *) -(* equality and there exists no comparison function compatible with *) -(* physical equality. *) - -module S = - struct - let empty = [] - let mem = List.memq - let add x l = x::l - end -;; - -(* evar reduction that preserves some terms *) -let nf_evar sigma ~preserve = - let module T = Term in - let rec aux t = - if preserve t then t else - match T.kind_of_term t with - | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _ - | T.Construct _ -> t - | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2) - | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2) - | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c) - | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c) - | T.App (c,l) -> - let c' = aux c in - let l' = Array.map aux l in - (match T.kind_of_term c' with - T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') - | T.Cast (he,_,_) -> - (match T.kind_of_term he with - T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') - | _ -> T.mkApp (c', l') - ) - | _ -> T.mkApp (c', l')) - | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e -> - aux (Evd.existential_value sigma (e,l)) - | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) - | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) - | T.Fix (ln,(lna,tl,bl)) -> - T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl)) - | T.CoFix(ln,(lna,tl,bl)) -> - T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl)) - in - aux -;; - -module ProofTreeHash = - Hashtbl.Make - (struct - type t = Proof_type.proof_tree - let equal = (==) - let hash = Hashtbl.hash - end) -;; - - -let extract_open_proof sigma pf = - (* Deactivated and candidate for removal. (Apr. 2010) *) - () - -let extract_open_pftreestate pts = - (* Deactivated and candidate for removal. (Apr. 2010) *) - () diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 deleted file mode 100644 index 2f5eb6ac..00000000 --- a/plugins/xml/proofTree2Xml.ml4 +++ /dev/null @@ -1,205 +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 *) -(************************************************************************) - -let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; - -let idref_of_id id = "v" ^ id;; - -(* Transform a constr to an Xml.token Stream.t *) -(* env is a named context *) -(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *) -let constr_to_xml obj sigma env = - let ids_to_terms = Hashtbl.create 503 in - let constr_to_ids = Acic.CicHash.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - - (* named_context holds section variables and local variables *) - let named_context = Environ.named_context env in - (* real_named_context holds only the section variables *) - let real_named_context = Environ.named_context (Global.env ()) in - (* named_context' holds only the local variables *) - let named_context' = - List.filter (function n -> not (List.mem n real_named_context)) named_context - in - let idrefs = - List.map - (function x,_,_ -> idref_of_id (Names.string_of_id x)) named_context' in - let rel_context = Sign.push_named_to_rel_context named_context' [] in - let rel_env = - Environ.push_rel_context rel_context - (Environ.reset_with_named_context - (Environ.val_of_named_context real_named_context) env) in - let obj' = - Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in - let seed = ref 0 in - try - let annobj = - Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env - idrefs sigma (Unshare.unshare obj') None - in - Acic2Xml.print_term ids_to_inner_sorts annobj - with e -> - Util.anomaly - ("Problem during the conversion of constr into XML: " ^ - Printexc.to_string e) -(* CSC: debugging stuff -Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ; -Pp.ppnl (Pp.str "ENVIRONMENT:") ; -Pp.ppnl (Printer.pr_context_of rel_env) ; -Pp.ppnl (Pp.str "TERM:") ; -Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ; -Pp.ppnl (Pp.str "RAW-TERM:") ; -Pp.ppnl (Printer.pr_lconstr obj') ; -Xml.xml_empty "MISSING TERM" [] (*; raise e*) -*) -;; - -let first_word s = - try let i = String.index s ' ' in - String.sub s 0 i - with _ -> s -;; - -let string_of_prim_rule x = match x with - | Proof_type.Intro _-> "Intro" - | Proof_type.Cut _ -> "Cut" - | Proof_type.FixRule _ -> "FixRule" - | Proof_type.Cofix _ -> "Cofix" - | Proof_type.Refine _ -> "Refine" - | Proof_type.Convert_concl _ -> "Convert_concl" - | Proof_type.Convert_hyp _->"Convert_hyp" - | Proof_type.Thin _ -> "Thin" - | Proof_type.ThinBody _-> "ThinBody" - | Proof_type.Move (_,_,_) -> "Move" - | Proof_type.Order _ -> "Order" - | Proof_type.Rename (_,_) -> "Rename" - | Proof_type.Change_evars -> "Change_evars" - -let - print_proof_tree curi sigma pf proof_tree_to_constr - proof_tree_to_flattened_proof_tree constr_to_ids -= - let module PT = Proof_type in - let module L = Logic in - let module X = Xml in - let module T = Tacexpr in - let ids_of_node node = - let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in -(* -let constr = - try - Proof2aproof.ProofTreeHash.find proof_tree_to_constr node - with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated -no lambda-term: ") (Refiner.print_script true (Evd.empty) -(Global.named_context ()) node)) ; assert false (* Closed bug, should not -happen any more *) -in -*) - try - Some (Acic.CicHash.find constr_to_ids constr) - with _ -> -Pp.ppnl (Pp.(++) (Pp.str -"The_generated_term_is_not_a_subterm_of_the_final_lambda_term") -(Printer.pr_lconstr constr)) ; - None - in - let rec aux node old_hyps = - let of_attribute = - match ids_of_node node with - None -> [] - | Some id -> ["of",id] - in - match node with - {PT.ref=Some(PT.Prim tactic_expr,nodes)} -> - let tac = string_of_prim_rule tactic_expr in - let of_attribute = ("name",tac)::of_attribute in - if nodes = [] then - X.xml_empty "Prim" of_attribute - else - X.xml_nempty "Prim" of_attribute - (List.fold_left - (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) - - | {PT.goal=goal; - PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} -> - (* [hidden_proof] is the proof of the tactic; *) - (* [nodes] are the proof of the subgoals generated by the tactic; *) - (* [flat_proof] if the proof-tree obtained substituting [nodes] *) - (* for the holes in [hidden_proof] *) - let flat_proof = - Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node - in begin - match tactic_expr with - | T.TacArg (_,T.Tacexp _) -> - (* We don't need to keep the level of abstraction introduced at *) - (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) - aux flat_proof old_hyps - | _ -> - (****** la tactique employee *) - let prtac = Pptactic.pr_tactic (Global.env()) in - let tac = Pp.string_of_ppcmds (prtac tactic_expr) in - let tacname= first_word tac in - let of_attribute = ("name",tacname)::("script",tac)::of_attribute in - - (****** le but *) - - let concl = Goal.V82.concl sigma goal in - let hyps = Goal.V82.hyps sigma goal in - - let env = Global.env_of_context hyps in - - - let xgoal = - X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in - - let rec build_hyps = - function - | [] -> xgoal - | (id,c,tid)::hyps1 -> - let id' = Names.string_of_id id in - [< build_hyps hyps1; - (X.xml_nempty "Hypothesis" - ["id",idref_of_id id' ; "name",id'] - (constr_to_xml tid sigma env)) - >] in - let old_names = List.map (fun (id,c,tid)->id) old_hyps in - let nhyps = Environ.named_context_of_val hyps in - let new_hyps = - List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in - - X.xml_nempty "Tactic" of_attribute - [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>] - end - - | {PT.ref=Some(PT.Daimon,_)} -> - X.xml_empty "Hidden_open_goal" of_attribute - - | {PT.ref=None;PT.goal=goal} -> - X.xml_empty "Open_goal" of_attribute - | {PT.ref=Some(PT.Decl_proof _, _)} -> failwith "TODO: xml and decl_proof" - in - [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; - X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n"); - X.xml_nempty "ProofTree" ["of",curi] (aux pf []) - >] -;; - - -(* Hook registration *) -(* CSC: debranched since it is bugged -Xmlcommand.set_print_proof_tree print_proof_tree;; -*) diff --git a/plugins/xml/theoryobject.dtd b/plugins/xml/theoryobject.dtd deleted file mode 100644 index 953fe009..00000000 --- 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 c854427d..00000000 --- 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 cace2de6..00000000 --- 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 8a4eb39a..00000000 --- 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 0b6d5198..00000000 --- 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 90797e8d..00000000 --- a/plugins/xml/xml_plugin.mllib +++ /dev/null @@ -1,13 +0,0 @@ -Unshare -Xml -Acic -DoubleTypeInference -Cic2acic -Acic2Xml -Proof2aproof -Xmlcommand -ProofTree2Xml -Xmlentries -Cic2Xml -Dumptree -Xml_plugin_mod diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml deleted file mode 100644 index 59ade01e..00000000 --- a/plugins/xml/xmlcommand.ml +++ /dev/null @@ -1,691 +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;; - -(* HOOKS *) -let print_proof_tree, set_print_proof_tree = - let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in - (fun () -> !print_proof_tree), - (fun f -> - print_proof_tree := - fun - curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree - constr_to_ids - -> - Some - (f curi sigma0 pf proof_tree_to_constr - proof_tree_to_flattened_proof_tree constr_to_ids)) -;; - -(* UTILITY FUNCTIONS *) - -let print_if_verbose s = if !verbose then print_string s;; - -(* Next exception is used only inside print_coq_object and tag_of_string_tag *) -exception Uninteresting;; - -(* NOT USED anymore, we back to the V6 point of view with global parameters - -(* Internally, for Coq V7, params of inductive types are associated *) -(* not to the whole block of mutual inductive (as it was in V6) but to *) -(* each member of the block; but externally, all params are required *) -(* to be the same; the following function checks that the parameters *) -(* of each inductive of a same block are all the same, then returns *) -(* this number; it fails otherwise *) -let extract_nparams pack = - let module D = Declarations in - let module U = Util in - let module S = Sign in - - let {D.mind_nparams=nparams0} = pack.(0) in - let arity0 = pack.(0).D.mind_user_arity in - let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in - for i = 1 to Array.length pack - 1 do - let {D.mind_nparams=nparamsi} = pack.(i) in - let arityi = pack.(i).D.mind_user_arity in - let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in - if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block" - done; - nparams0 - -*) - -(* could_have_namesakes sp = true iff o is an object that could be cooked and *) -(* than that could exists in cooked form with the same name in a super *) -(* section of the actual section *) -let could_have_namesakes o sp = (* namesake = omonimo in italian *) - let module DK = Decl_kinds in - let module D = Declare in - let tag = Libobject.object_tag o in - print_if_verbose ("Object tag: " ^ tag ^ "\n") ; - match tag with - "CONSTANT" -> true (* constants/parameters are non global *) - | "INDUCTIVE" -> true (* mutual inductive types are never local *) - | "VARIABLE" -> false (* variables are local, so no namesakes *) - | _ -> false (* uninteresting thing that won't be printed*) -;; - -(* filter_params pvars hyps *) -(* filters out from pvars (which is a list of lists) all the variables *) -(* that does not belong to hyps (which is a simple list) *) -(* It returns a list of couples relative section path -- list of *) -(* variable names. *) -let filter_params pvars hyps = - let rec aux ids = - function - [] -> [] - | (id,he)::tl -> - let ids' = id::ids in - let ids'' = - "cic:/" ^ - String.concat "/" (List.rev (List.map Names.string_of_id ids')) in - let he' = - ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in - let tl' = aux ids' tl in - match he' with - _,[] -> tl' - | _,_ -> he'::tl' - in - let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - aux (Names.repr_dirpath modulepath) (List.rev pvars) -;; - -type variables_type = - Definition of string * Term.constr * Term.types - | Assumption of string * Term.constr -;; - -(* The computation is very inefficient, but we can't do anything *) -(* better unless this function is reimplemented in the Declare *) -(* module. *) -let search_variables () = - let module N = Names in - let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - let rec aux = - function - [] -> [] - | he::tl as modules -> - let one_section_variables = - let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in - let t = List.map N.string_of_id (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 e <> Sys.Break -> () (* Let's ignore the errors on mkdir *) - ) ; - let newcwd = cwd ^ "/" ^ he in - join_dirs newcwd tail -;; - -let filename_of_path xml_library_root tag = - let module N = Names in - match xml_library_root with - None -> None (* stdout *) - | Some xml_library_root' -> - let tokens = Cic2acic.token_list_of_kernel_name tag in - Some (join_dirs xml_library_root' tokens) -;; - -let body_filename_of_filename = - function - Some f -> Some (f ^ ".body") - | None -> None -;; - -let types_filename_of_filename = - function - Some f -> Some (f ^ ".types") - | None -> None -;; - -let prooftree_filename_of_filename = - function - Some f -> Some (f ^ ".proof_tree") - | None -> None -;; - -let theory_filename xml_library_root = - let module N = Names in - match xml_library_root with - None -> None (* stdout *) - | Some xml_library_root' -> - let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in - (* theory from A/B/C/F.v goes into A/B/C/F.theory *) - let alltoks = List.rev toks in - Some (join_dirs xml_library_root' alltoks ^ ".theory") - -let print_object uri obj sigma proof_tree_infos filename = - (* function to pretty print and compress an XML file *) -(*CSC: Unix.system "gzip ..." is an horrible non-portable solution. *) - let pp xml filename = - Xml.pp xml filename ; - match filename with - None -> () - | Some fn -> - let fn' = - let rec escape s n = - try - let p = String.index_from s n '\'' in - String.sub s n (p - n) ^ "\\'" ^ escape s (p+1) - with Not_found -> String.sub s n (String.length s - n) - in - escape fn 0 - in - ignore (Unix.system ("gzip " ^ fn' ^ ".xml")) - in - let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) = - Cic2acic.acic_object_of_cic_object sigma obj in - let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in - let xmltypes = - Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in - pp xml filename ; - begin - match xml' with - None -> () - | Some xml' -> pp xml' (body_filename_of_filename filename) - end ; - pp xmltypes (types_filename_of_filename filename) ; - match proof_tree_infos with - None -> () - | Some (sigma0,proof_tree,proof_tree_to_constr, - proof_tree_to_flattened_proof_tree) -> - let xmlprooftree = - print_proof_tree () - uri sigma0 proof_tree proof_tree_to_constr - proof_tree_to_flattened_proof_tree constr_to_ids - in - match xmlprooftree with - None -> () - | Some xmlprooftree -> - pp xmlprooftree (prooftree_filename_of_filename filename) -;; - -let string_list_of_named_context_list = - List.map - (function (n,_,_) -> Names.string_of_id n) -;; - -(* Function to collect the variables that occur in a term. *) -(* Used only for variables (since for constants and mutual *) -(* inductive types this information is already available. *) -let find_hyps t = - let module T = Term in - let rec aux l t = - match T.kind_of_term t with - T.Var id when not (List.mem id l) -> - let (_,bo,ty) = Global.lookup_named id in - let boids = - match bo with - Some bo' -> aux l bo' - | None -> l - in - id::(aux boids ty) - | T.Var _ - | T.Rel _ - | T.Meta _ - | T.Evar _ - | T.Sort _ -> l - | T.Cast (te,_, ty) -> aux (aux l te) ty - | T.Prod (_,s,t) -> aux (aux l s) t - | T.Lambda (_,s,t) -> aux (aux l s) t - | T.LetIn (_,s,_,t) -> aux (aux l s) t - | T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl - | T.Const con -> - let hyps = (Global.lookup_constant con).Declarations.const_hyps in - map_and_filter l hyps @ l - | T.Ind ind - | T.Construct (ind,_) -> - let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in - map_and_filter l hyps @ l - | T.Case (_,t1,t2,b) -> - Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b - | T.Fix (_,(_,tys,bodies)) - | T.CoFix (_,(_,tys,bodies)) -> - let r = Array.fold_left (fun i x -> aux i x) l tys in - Array.fold_left (fun i x -> aux i x) r bodies - and map_and_filter l = - function - [] -> [] - | (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl) - | _::tl -> map_and_filter l tl - in - aux [] t -;; - -(* Functions to construct an object *) - -let mk_variable_obj id body typ = - let hyps,unsharedbody = - match body with - None -> [],None - | Some bo -> find_hyps bo, Some (Unshare.unshare bo) - in - let hyps' = find_hyps typ @ hyps in - let hyps'' = List.map Names.string_of_id hyps' in - let variables = search_variables () in - let params = filter_params variables hyps'' in - Acic.Variable - (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params) -;; - -(* Unsharing is not performed on the body, that must be already unshared. *) -(* The evar map and the type, instead, are unshared by this function. *) -let mk_current_proof_obj is_a_variable id bo ty evar_map env = - let unshared_ty = Unshare.unshare ty in - let metasenv = - List.map - (function - (n, {Evd.evar_concl = evar_concl ; - Evd.evar_hyps = evar_hyps} - ) -> - (* We map the named context to a rel context and every Var to a Rel *) - let final_var_ids,context = - let rec aux var_ids = - function - [] -> var_ids,[] - | (n,None,t)::tl -> - let final_var_ids,tl' = aux (n::var_ids) tl in - let t' = Term.subst_vars var_ids t in - final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl' - | (n,Some b,t)::tl -> - let final_var_ids,tl' = aux (n::var_ids) tl in - let b' = Term.subst_vars var_ids b in - (* t will not be exported to XML. Thus no unsharing performed *) - final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl' - in - aux [] (List.rev (Environ.named_context_of_val evar_hyps)) - in - (* We map the named context to a rel context and every Var to a Rel *) - (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl)) - ) (Evarutil.non_instantiated evar_map) - in - let id' = Names.string_of_id id in - if metasenv = [] then - let ids = - Names.Idset.union - (Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in - let hyps0 = Environ.keep_hyps env ids in - let hyps = string_list_of_named_context_list hyps0 in - (* Variables are the identifiers of the variables in scope *) - let variables = search_variables () in - let params = filter_params variables hyps in - if is_a_variable then - Acic.Variable (id',Some bo,unshared_ty,params) - else - Acic.Constant (id',Some bo,unshared_ty,params) - else - Acic.CurrentProof (id',metasenv,bo,unshared_ty) -;; - -let mk_constant_obj id bo ty variables hyps = - let hyps = string_list_of_named_context_list hyps in - let ty = Unshare.unshare ty in - let params = filter_params variables hyps in - match bo with - None -> - Acic.Constant (Names.string_of_id id,None,ty,params) - | Some c -> - Acic.Constant - (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)), - ty,params) -;; - -let mk_inductive_obj sp mib packs variables nparams hyps finite = - let module D = Declarations in - let hyps = string_list_of_named_context_list hyps in - let params = filter_params variables hyps in -(* let nparams = extract_nparams packs in *) - let tys = - let tyno = ref (Array.length packs) in - Array.fold_right - (fun p i -> - decr tyno ; - let {D.mind_consnames=consnames ; - D.mind_typename=typename } = p - in - let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in - let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in - let cons = - (Array.fold_right (fun (name,lc) i -> (name,lc)::i) - (Array.mapi - (fun j x ->(x,Unshare.unshare 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_global_goal = function - | Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition" - | Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k - | Decl_kinds.Local, _ -> assert false - -let kind_of_inductive isrecord kn = - "DEFINITION", - if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite - then begin - match isrecord with - | Declare.KernelSilent -> "Record" - | _ -> "Inductive" - end - else "CoInductive" -;; - -let kind_of_variable id = - let module DK = Decl_kinds in - match Decls.variable_kind id with - | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption" - | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis" - | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" - | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition" - | DK.IsProof _ -> "VARIABLE","LocalFact" - | _ -> Util.anomaly "Unsupported variable kind" -;; - -let kind_of_constant kn = - let module DK = Decl_kinds in - match Decls.constant_kind kn with - | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" - | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" - | DK.IsAssumption DK.Conjectural -> - Pp.msg_warn "Conjecture not supported in dtd (used Declaration instead)"; - "AXIOM","Declaration" - | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" - | DK.IsDefinition DK.Example -> - Pp.msg_warn "Example not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.Coercion -> - Pp.msg_warn "Coercion not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.SubClass -> - Pp.msg_warn "SubClass not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.CanonicalStructure -> - Pp.msg_warn "CanonicalStructure not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.Fixpoint -> - Pp.msg_warn "Fixpoint not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.CoFixpoint -> - Pp.msg_warn "CoFixpoint not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.Scheme -> - Pp.msg_warn "Scheme not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.StructureComponent -> - Pp.msg_warn "StructureComponent not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.IdentityCoercion -> - Pp.msg_warn "IdentityCoercion not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.Instance -> - Pp.msg_warn "Instance not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsDefinition DK.Method -> - Pp.msg_warn "Method not supported in dtd (used Definition instead)"; - "DEFINITION","Definition" - | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> - "THEOREM",DK.string_of_theorem_kind thm - | DK.IsProof _ -> - Pp.msg_warn "Unsupported theorem kind (used Theorem instead)"; - "THEOREM",DK.string_of_theorem_kind DK.Theorem -;; - -let kind_of_global r = - let module Ln = Libnames in - let module DK = Decl_kinds in - match r with - | Ln.IndRef kn | Ln.ConstructRef (kn,_) -> - let isrecord = - try let _ = Recordops.lookup_projections kn in Declare.KernelSilent - with Not_found -> Declare.KernelVerbose in - kind_of_inductive isrecord (fst kn) - | Ln.VarRef id -> kind_of_variable id - | Ln.ConstRef kn -> kind_of_constant kn -;; - -let print_object_kind uri (xmltag,variation) = - let s = - Printf.sprintf "<ht:%s uri=\"%s\" as=\"%s\"/>\n" xmltag uri variation - in - theory_output_string s -;; - -(* print id dest *) -(* where sp is the qualified identifier (section path) of a *) -(* definition/theorem, variable or inductive definition *) -(* and dest is either None (for stdout) or (Some filename) *) -(* pretty prints via Xml.pp the object whose identifier is id on dest *) -(* Note: it is printed only (and directly) the most cooked available *) -(* form of the definition (all the parameters are *) -(* lambda-abstracted, but the object can still refer to variables) *) -let print internal glob_ref kind xml_library_root = - let module D = Declarations in - let module De = Declare in - let module G = Global in - let module N = Names in - let module Nt = Nametab in - let module T = Term in - let module X = Xml in - let module Ln = Libnames in - (* Variables are the identifiers of the variables in scope *) - let variables = search_variables () in - let tag,obj = - match glob_ref with - Ln.VarRef id -> - (* this kn is fake since it is not provided by Coq *) - let kn = - let (mod_path,dir_path) = Lib.current_prefix () in - N.make_kn mod_path dir_path (N.label_of_id id) - in - let (_,body,typ) = G.lookup_named id in - Cic2acic.Variable kn,mk_variable_obj id body typ - | Ln.ConstRef kn -> - let id = N.id_of_label (N.con_label kn) in - let cb = G.lookup_constant kn in - let val0 = D.body_of_constant cb in - let typ = cb.D.const_type in - let hyps = cb.D.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 - | Ln.IndRef (kn,_) -> - let mib = G.lookup_mind kn in - let {D.mind_nparams=nparams; - D.mind_packets=packs ; - D.mind_hyps=hyps; - D.mind_finite=finite} = mib in - Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite - | Ln.ConstructRef _ -> - Util.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 None 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 - Util.anomaly "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 _ = - Pfedit.set_xml_cook_proof - (function pftreestate -> proof_to_export := Some pftreestate) -;; - -let _ = - Declare.set_xml_declare_variable - (function (sp,kn) -> - let id = Libnames.basename sp in - print Declare.UserVerbose (Libnames.VarRef id) (kind_of_variable id) xml_library_root ; - proof_to_export := None) -;; - -let _ = - Declare.set_xml_declare_constant - (function (internal,kn) -> - match !proof_to_export with - None -> - print internal (Libnames.ConstRef kn) (kind_of_constant kn) - xml_library_root - | Some pftreestate -> - (* It is a proof. Let's export it starting from the proof-tree *) - (* I saved in the Pfedit.set_xml_cook_proof callback. *) - let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in - show_pftreestate internal fn pftreestate - (Names.id_of_label (Names.con_label kn)) ; - proof_to_export := None) -;; - -let _ = - Declare.set_xml_declare_inductive - (function (isrecord,(sp,kn)) -> - print Declare.UserVerbose (Libnames.IndRef (Names.mind_of_kn kn,0)) - (kind_of_inductive isrecord (Names.mind_of_kn kn)) - xml_library_root) -;; - -let _ = - Vernac.set_xml_start_library - (function () -> - Buffer.reset theory_buffer; - theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n"; - theory_output_string ("<!DOCTYPE html [\n" ^ - "<!ENTITY % xhtml-lat1.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-lat1.ent\">\n" ^ - "<!ENTITY % xhtml-special.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-special.ent\">\n" ^ - "<!ENTITY % xhtml-symbol.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-symbol.ent\">\n\n" ^ - "%xhtml-lat1.ent;\n" ^ - "%xhtml-special.ent;\n" ^ - "%xhtml-symbol.ent;\n" ^ - "]>\n\n"); - theory_output_string "<html xmlns=\"http://www.w3.org/1999/xhtml\" xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\" xmlns:helm=\"http://www.cs.unibo.it/helm\">\n"; - theory_output_string "<head></head>\n<body>\n") -;; - -let _ = - Vernac.set_xml_end_library - (function () -> - theory_output_string "</body>\n</html>\n"; - let ofn = theory_filename xml_library_root in - begin - match ofn with - None -> - Buffer.output_buffer stdout theory_buffer ; - | Some fn -> - let ch = open_out (fn ^ ".v") in - Buffer.output_buffer ch theory_buffer ; - close_out ch; - (* 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 - Util.anomaly ("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 _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;; - -let uri_of_dirpath dir = - "/" ^ String.concat "/" - (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir))) -;; - -let _ = - Lib.set_xml_open_section - (fun _ -> - let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in - theory_output_string ("<ht:SECTION uri=\""^s^"\">")) -;; - -let _ = - Lib.set_xml_close_section - (fun _ -> theory_output_string "</ht:SECTION>") -;; - -let _ = - Library.set_xml_require - (fun d -> theory_output_string - (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>" - (uri_of_dirpath d) (Names.string_of_dirpath d))) -;; diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli deleted file mode 100644 index ec50d623..00000000 --- a/plugins/xml/xmlcommand.mli +++ /dev/null @@ -1,39 +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 - -(* set_print_proof_tree f *) -(* sets a callback function f to export the proof_tree to XML *) -val set_print_proof_tree : - (string -> - Evd.evar_map -> - Proof_type.proof_tree -> - Term.constr Proof2aproof.ProofTreeHash.t -> - Proof_type.proof_tree Proof2aproof.ProofTreeHash.t -> - string Acic.CicHash.t -> Xml.token Stream.t) -> - unit diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 deleted file mode 100644 index d65a1bd3..00000000 --- a/plugins/xml/xmlentries.ml4 +++ /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 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -open Util;; -open Vernacinterp;; - -open Extend;; -open Genarg;; -open Pp;; -open Pcoq;; - -(* File name *) - -VERNAC ARGUMENT EXTEND filename -| [ "File" string(fn) ] -> [ Some fn ] -| [ ] -> [ None ] -END - -(* Print XML and Show XML *) - -VERNAC COMMAND EXTEND Xml -| [ "Print" "XML" filename(fn) global(qid) ] -> [ Xmlcommand.print_ref qid fn ] - -| [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] -END |