diff options
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/COPYRIGHT | 25 | ||||
| -rw-r--r-- | plugins/xml/README | 254 | ||||
| -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 | 272 | ||||
| -rw-r--r-- | plugins/xml/doubleTypeInference.mli | 24 | ||||
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 152 | ||||
| -rw-r--r-- | plugins/xml/proof2aproof.ml | 176 | ||||
| -rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 210 | ||||
| -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 | 40 | ||||
| -rw-r--r-- | plugins/xml/xml_plugin.mllib | 13 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 719 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.mli | 41 | ||||
| -rw-r--r-- | plugins/xml/xmlentries.ml4 | 40 |
21 files changed, 3868 insertions, 0 deletions
diff --git a/plugins/xml/COPYRIGHT b/plugins/xml/COPYRIGHT new file mode 100644 index 00000000..c8d231fd --- /dev/null +++ b/plugins/xml/COPYRIGHT @@ -0,0 +1,25 @@ +(******************************************************************************) +(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* Project Helm (http://helm.cs.unibo.it) *) +(* Project MoWGLI (http://mowgli.cs.unibo.it) *) +(* *) +(* Coq Exportation to XML *) +(* *) +(******************************************************************************) + +This Coq module has been developed by Claudio Sacerdoti Coen +<sacerdot@cs.unibo.it> as a developer of projects HELM and MoWGLI. + +Project HELM (for Hypertextual Electronic Library of Mathematics) is a +project developed at the Department of Computer Science, University of Bologna; +http://helm.cs.unibo.it + +Project MoWGLI (Mathematics on the Web: Get It by Logics and Interfaces) +is a UE IST project that generalizes and extends the HELM project; +http://mowgli.cs.unibo.it + +The author is interested in any possible usage of the module. +So, if you plan to use the module, please send him an e-mail. + +The licensing policy applied to the module is the same as for the whole Coq +distribution. diff --git a/plugins/xml/README b/plugins/xml/README new file mode 100644 index 00000000..a45dd31a --- /dev/null +++ b/plugins/xml/README @@ -0,0 +1,254 @@ +(******************************************************************************) +(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* Project Helm (http://helm.cs.unibo.it) *) +(* Project MoWGLI (http://mowgli.cs.unibo.it) *) +(* *) +(* Coq Exportation to XML *) +(* *) +(******************************************************************************) + +This module provides commands to export a piece of Coq library in XML format. +Only the information relevant to proof-checking and proof-rendering is exported, +i.e. only the CIC proof objects (lambda-terms). + +This document is tructured in the following way: + 1. User documentation + 1.1. New vernacular commands available + 1.2. New coqc/coqtop flags and suggested usage + 1.3. How to exploit the XML files + 2. Technical informations + 2.1. Inner-types + 2.2. CIC with Explicit Named Substitutions + 2.3. The CIC with Explicit Named Substitutions XML DTD + +================================================================================ + USER DOCUMENTATION +================================================================================ + +======================================= +1.1. New vernacular commands available: +======================================= + +The new commands are: + + Print XML qualid. It prints in XML (to standard output) the + object whose qualified name is qualid and + its inner-types (see Sect. 2.1). + The inner-types are always printed + in their own XML file. If the object is a + constant, its type and body are also printed + as two distinct XML files. + The object printed is always the most + discharged form of the object (see + the Section command of the Coq manual). + + Print XML File "filename" qualid. Similar to "Print XML qualid". The generated + files are stored on the hard-disk using the + base file name "filename". + + Show XML Proof. It prints in XML the current proof in + progress. Its inner-types are also printed. + + Show XML File "filename" Proof. Similar to "Show XML Proof". The generated + files are stored on the hard-disk using + the base file name "filename". + + The verbosity of the previous commands is raised if the configuration + parameter verbose of xmlcommand.ml is set to true at compile time. + +============================================== +1.2. New coqc/coqtop flags and suggested usage +============================================== + + The following flag has been added to coqc and coqtop: + + -xml export XML files either to the hierarchy rooted in + the directory $COQ_XML_LIBRARY_ROOT (if the environment + variable is set) or to stdout (if unset) + + If the flag is set, every definition or declaration is immediately + exported to XML. The XML files describe the user-provided non-discharged + form of the definition or declaration. + + + The coq_makefile utility has also been modified to easily allow XML + exportation: + + make COQ_XML=-xml (or, equivalently, setting the environment + variable COQ_XML) + + + The suggested usage of the module is the following: + + 1. add to your own contribution a valid Make file and use coq_makefile + to generate the Makefile from the Make file. + *WARNING:* Since logical names are used to structure the XML hierarchy, + always add to the Make file at least one "-R" option to map physical + file names to logical module paths. See the Coq manual for further + informations on the -R flag. + 2. set $COQ_XML_LIBRARY_ROOT to the directory where the XML file hierarchy + must be physically rooted. + 3. compile your contribution with "make COQ_XML=-xml" + + +================================= +1.3. How to exploit the XML files +================================= + + Once the information is exported to XML, it becomes possible to implement + services that are completely Coq-independent. Projects HELM and MoWGLI + already provide rendering, searching and data mining functionalities. + + In particular, the standard library and contributions of Coq can be + browsed and searched on the HELM web site: + + http://helm.cs.unibo.it/library.html + + + If you want to publish your own contribution so that it is included in the + HELM library, use the MoWGLI prototype upload form: + + http://mowgli.cs.unibo.it + + +================================================================================ + TECHNICAL INFORMATIONS +================================================================================ + +========================== +2.1. Inner-types +========================== + +In order to do proof-rendering (for example in natural language), +some redundant typing information is required, i.e. the type of +at least some of the subterms of the bodies and types. So, each +new command described in section 1.1 print not only +the object, but also another XML file in which you can find +the type of all the subterms of the terms of the printed object +which respect the following conditions: + + 1. It's sort is Prop or CProp (the "sort"-like definition used in + CoRN to type computationally relevant predicative propositions). + 2. It is not a cast or an atomic term, i.e. it's root is not a CAST, REL, + VAR, MUTCONSTR or CONST. + 3. If it's root is a LAMBDA, then the root's parent node is not a LAMBDA, + i.e. only the type of the outer LAMBDA of a block of nested LAMBDAs is + printed. + +The rationale for the 3rd condition is that the type of the inner LAMBDAs +could be easily computed starting from the type of the outer LAMBDA; moreover, +the types of the inner LAMBDAs requires a lot of disk/memory space: removing +the 3rd condition leads to XML file that are two times as big as the ones +exported appling the 3rd condition. + +========================================== +2.2. CIC with Explicit Named Substitutions +========================================== + +The exported files are and XML encoding of the lambda-terms used by the +Coq system. The implementative details of the Coq system are hidden as much +as possible, so that the XML DTD is a straightforward encoding of the +Calculus of (Co)Inductive Constructions. + +Nevertheless, there is a feature of the Coq system that can not be +hidden in a completely satisfactory way: discharging. In Coq it is possible +to open a section, declare variables and use them in the rest of the section +as if they were axiom declarations. Once the section is closed, every definition +and theorem in the section is discharged by abstracting it over the section +variables. Variable declarations as well as section declarations are entirely +dropped. Since we are interested in an XML encoding of definitions and +theorems as close as possible to those directly provided the user, we +do not want to export discharged forms. Exporting non-discharged theorem +and definitions together with theorems that rely on the discharged forms +obliges the tools that work on the XML encoding to implement discharging to +achieve logical consistency. Moreover, the rendering of the files can be +misleading, since hyperlinks can be shown between occurrences of the discharge +form of a definition and the non-discharged definition, that are different +objects. + +To overcome the previous limitations, Claudio Sacerdoti Coen developed in his +PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions +with Explicit Named Substitutions, that is a slight extension of CIC where +discharging is not necessary. The DTD of the exported XML files describes +constants, inductive types and variables of the Calculus of (Co)Inductive +Constructions with Explicit Named Substitions. The conversion to the new +calculus is performed during the exportation phase. + +The following example shows a very small Coq development together with its +version in CIC with Explicit Named Substitutions. + +# CIC version: # +Section S. + Variable A : Prop. + + Definition impl := A -> A. + + Theorem t : impl. (* uses the undischarged form of impl *) + Proof. + exact (fun (a:A) => a). + Qed. + +End S. + +Theorem t' : (impl False). (* uses the discharged form of impl *) + Proof. + exact (t False). (* uses the discharged form of t *) + Qed. + +# Corresponding CIC with Explicit Named Substitutions version: # +Section S. + Variable A : Prop. + + Definition impl(A) := A -> A. (* theorems and definitions are + explicitly abstracted over the + variables. The name is sufficient + to completely describe the abstraction *) + + Theorem t(A) : impl. (* impl where A is not instantiated *) + Proof. + exact (fun (a:A) => a). + Qed. + +End S. + +Theorem t'() : impl{False/A}. (* impl where A is instantiated with False + Notice that t' does not depend on A *) + Proof. + exact t{False/A}. (* t where A is instantiated with False *) + Qed. + +Further details on the typing and reduction rules of the calculus can be +found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency +of the calculus is also proved. + +====================================================== +2.3. The CIC with Explicit Named Substitutions XML DTD +====================================================== + +A copy of the DTD can be found in the file "cic.dtd". + +<ConstantType> is the root element of the files that correspond to + constant types. +<ConstantBody> is the root element of the files that correspond to + constant bodies. It is used only for closed definitions and + theorems (i.e. when no metavariable occurs in the body + or type of the constant) +<CurrentProof> is the root element of the file that correspond to + the body of a constant that depends on metavariables + (e.g. unfinished proofs) +<Variable> is the root element of the files that correspond to variables +<InductiveTypes> is the root element of the files that correspond to blocks + of mutually defined inductive definitions + +The elements + <LAMBDA>,<CAST>,<PROD>,<REL>,<SORT>,<APPLY>,<VAR>,<META>, <IMPLICIT>,<CONST>, + <LETIN>,<MUTIND>,<MUTCONSTRUCT>,<MUTCASE>,<FIX> and <COFIX> +are used to encode the constructors of CIC. The sort or type attribute of the +element, if present, is respectively the sort or the type of the term, that +is a sort because of the typing rules of CIC. + +The element <instantiate> correspond to the application of an explicit named +substitution to its first argument, that is a reference to a definition +or declaration in the environment. + +All the other elements are just syntactic sugar. diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml new file mode 100644 index 00000000..40bc61bb --- /dev/null +++ b/plugins/xml/acic.ml @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +open Names +open Term + +(* Maps fron \em{unshared} [constr] to ['a]. *) +module CicHash = + Hashtbl.Make + (struct + type t = Term.constr + let equal = (==) + let hash = Hashtbl.hash + end) +;; + +type id = string (* the type of the (annotated) node identifiers *) +type uri = string + +type 'constr context_entry = + Decl of 'constr (* Declaration *) + | Def of 'constr * 'constr (* Definition; the second argument (the type) *) + (* is not present in the DTD, but is needed *) + (* to use Coq functions during exportation. *) + +type 'constr hypothesis = identifier * 'constr context_entry +type context = constr hypothesis list + +type conjecture = existential_key * context * constr +type metasenv = conjecture list + +(* list of couples section path -- variables defined in that section *) +type params = (string * uri list) list + +type obj = + Constant of string * (* id, *) + constr option * constr * (* value, type, *) + params (* parameters *) + | Variable of + string * constr option * constr * (* name, body, type *) + params (* parameters *) + | CurrentProof of + string * metasenv * (* name, conjectures, *) + constr * constr (* value, type *) + | InductiveDefinition of + inductiveType list * (* inductive types , *) + params * int (* parameters,n ind. pars*) +and inductiveType = + identifier * bool * constr * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + identifier * constr (* id, type *) + +type aconstr = + | ARel of id * int * id * identifier + | AVar of id * uri + | AEvar of id * existential_key * aconstr list + | ASort of id * sorts + | ACast of id * aconstr * aconstr + | AProds of (id * name * aconstr) list * aconstr + | ALambdas of (id * name * aconstr) list * aconstr + | ALetIns of (id * name * aconstr) list * aconstr + | AApp of id * aconstr list + | AConst of id * explicit_named_substitution * uri + | AInd of id * explicit_named_substitution * uri * int + | AConstruct of id * explicit_named_substitution * uri * int * int + | ACase of id * uri * int * aconstr * aconstr * aconstr list + | AFix of id * int * ainductivefun list + | ACoFix of id * int * acoinductivefun list +and ainductivefun = + id * identifier * int * aconstr * aconstr +and acoinductivefun = + id * identifier * aconstr * aconstr +and explicit_named_substitution = id option * (uri * aconstr) list + +type acontext = (id * aconstr hypothesis) list +type aconjecture = id * existential_key * acontext * aconstr +type ametasenv = aconjecture list + +type aobj = + AConstant of id * string * (* id, *) + aconstr option * aconstr * (* value, type, *) + params (* parameters *) + | AVariable of id * + string * aconstr option * aconstr * (* name, body, type *) + params (* parameters *) + | ACurrentProof of id * + string * ametasenv * (* name, conjectures, *) + aconstr * aconstr (* value, type *) + | AInductiveDefinition of id * + anninductiveType list * (* inductive types , *) + params * int (* parameters,n ind. pars*) +and anninductiveType = + id * identifier * bool * aconstr * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + identifier * aconstr (* id, type *) diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 new file mode 100644 index 00000000..fb40ed86 --- /dev/null +++ b/plugins/xml/acic2Xml.ml4 @@ -0,0 +1,363 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(*CSC codice cut & paste da cicPp e xmlcommand *) + +exception ImpossiblePossible;; +exception NotImplemented;; +let dtdname = "http://mowgli.cs.unibo.it/dtd/cic.dtd";; +let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";; + +let rec find_last_id = + function + [] -> Util.anomaly "find_last_id: empty list" + | [id,_,_] -> id + | _::tl -> find_last_id tl +;; + +let export_existential = string_of_int + +let print_term ids_to_inner_sorts = + let rec aux = + let module A = Acic in + let module N = Names in + let module X = Xml in + function + A.ARel (id,n,idref,b) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "REL" + ["value",(string_of_int n) ; "binder",(N.string_of_id b) ; + "id",id ; "idref",idref; "sort",sort] + | A.AVar (id,uri) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort] + | A.AEvar (id,n,l) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "META" + ["no",(export_existential n) ; "id",id ; "sort",sort] + (List.fold_left + (fun i t -> + [< i ; X.xml_nempty "substitution" [] (aux t) >] + ) [< >] (List.rev l)) + | A.ASort (id,s) -> + let string_of_sort = + match Term.family_of_sort s with + Term.InProp -> "Prop" + | Term.InSet -> "Set" + | Term.InType -> "Type" + in + X.xml_empty "SORT" ["value",string_of_sort ; "id",id] + | A.AProds (prods,t) -> + let last_id = find_last_id prods in + let sort = Hashtbl.find ids_to_inner_sorts last_id in + X.xml_nempty "PROD" ["type",sort] + [< List.fold_left + (fun i (id,binder,s) -> + let sort = + Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) + in + let attrs = + ("id",id)::("type",sort):: + match binder with + Names.Anonymous -> [] + | Names.Name b -> ["binder",Names.string_of_id b] + in + [< X.xml_nempty "decl" attrs (aux s) ; i >] + ) [< >] prods ; + X.xml_nempty "target" [] (aux t) + >] + | A.ACast (id,v,t) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "CAST" ["id",id ; "sort",sort] + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] + | A.ALambdas (lambdas,t) -> + let last_id = find_last_id lambdas in + let sort = Hashtbl.find ids_to_inner_sorts last_id in + X.xml_nempty "LAMBDA" ["sort",sort] + [< List.fold_left + (fun i (id,binder,s) -> + let sort = + Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) + in + let attrs = + ("id",id)::("type",sort):: + match binder with + Names.Anonymous -> [] + | Names.Name b -> ["binder",Names.string_of_id b] + in + [< X.xml_nempty "decl" attrs (aux s) ; i >] + ) [< >] lambdas ; + X.xml_nempty "target" [] (aux t) + >] + | A.ALetIns (letins,t) -> + let last_id = find_last_id letins in + let sort = Hashtbl.find ids_to_inner_sorts last_id in + X.xml_nempty "LETIN" ["sort",sort] + [< List.fold_left + (fun i (id,binder,s) -> + let sort = + Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) + in + let attrs = + ("id",id)::("sort",sort):: + match binder with + Names.Anonymous -> assert false + | Names.Name b -> ["binder",Names.string_of_id b] + in + [< X.xml_nempty "def" attrs (aux s) ; i >] + ) [< >] letins ; + X.xml_nempty "target" [] (aux t) + >] + | A.AApp (id,li) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "APPLY" ["id",id ; "sort",sort] + [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li) + >] + | A.AConst (id,subst,uri) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + let attrs = ["uri", uri ; "id",id ; "sort",sort] in + aux_subst (X.xml_empty "CONST" attrs) subst + | A.AInd (id,subst,uri,i) -> + let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in + aux_subst (X.xml_empty "MUTIND" attrs) subst + | A.AConstruct (id,subst,uri,i,j) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + let attrs = + ["uri", uri ; + "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; + "id",id ; "sort",sort] + in + aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst + | A.ACase (id,uri,typeno,ty,te,patterns) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "MUTCASE" + ["uriType", uri ; + "noType", (string_of_int typeno) ; + "id", id ; "sort",sort] + [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; + X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; + List.fold_left + (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >]) + [<>] patterns + >] + | A.AFix (id, no, funs) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "FIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_left + (fun i (id,fi,ai,ti,bi) -> + [< i ; + X.xml_nempty "FixFunction" + ["id",id ; "name", (Names.string_of_id fi) ; + "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] + >] + ) [<>] funs + >] + | A.ACoFix (id,no,funs) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "COFIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_left + (fun i (id,fi,ti,bi) -> + [< i ; + X.xml_nempty "CofixFunction" + ["id",id ; "name", Names.string_of_id fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] + >] + ) [<>] funs + >] + and aux_subst target (id,subst) = + if subst = [] then + target + else + Xml.xml_nempty "instantiate" + (match id with None -> [] | Some id -> ["id",id]) + [< target ; + List.fold_left + (fun i (uri,arg) -> + [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >] + ) [<>] subst + >] + in + aux +;; + +let param_attribute_of_params params = + List.fold_right + (fun (path,l) i -> + List.fold_right + (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i' + ) l "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" +;; + +let print_object uri ids_to_inner_sorts = + let rec aux = + let module A = Acic in + let module X = Xml in + function + A.ACurrentProof (id,n,conjectures,bo,ty) -> + let xml_for_current_proof_body = +(*CSC: Should the CurrentProof also have the list of variables it depends on? *) +(*CSC: I think so. Not implemented yet. *) + X.xml_nempty "CurrentProof" ["of",uri ; "id", id] + [< List.fold_left + (fun i (cid,n,canonical_context,t) -> + [< i ; + X.xml_nempty "Conjecture" + ["id", cid ; "no",export_existential n] + [< List.fold_left + (fun i (hid,t) -> + [< (match t with + n,A.Decl t -> + X.xml_nempty "Decl" + ["id",hid;"name",Names.string_of_id n] + (print_term ids_to_inner_sorts t) + | n,A.Def (t,_) -> + X.xml_nempty "Def" + ["id",hid;"name",Names.string_of_id n] + (print_term ids_to_inner_sorts t) + ) ; + i + >] + ) [< >] canonical_context ; + X.xml_nempty "Goal" [] + (print_term ids_to_inner_sorts t) + >] + >]) + [<>] (List.rev conjectures) ; + X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] + in + let xml_for_current_proof_type = + X.xml_nempty "ConstantType" ["name",n ; "id", id] + (print_term ids_to_inner_sorts ty) + in + let xmlbo = + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n"); + xml_for_current_proof_body + >] in + let xmlty = + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata + ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n"); + xml_for_current_proof_type + >] + in + xmlty, Some xmlbo + | A.AConstant (id,n,bo,ty,params) -> + let params' = param_attribute_of_params params in + let xmlbo = + match bo with + None -> None + | Some bo -> + Some + [< X.xml_cdata + "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata + ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ; + X.xml_nempty "ConstantBody" + ["for",uri ; "params",params' ; "id", id] + [< print_term ids_to_inner_sorts bo >] + >] + in + let xmlty = + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n"); + X.xml_nempty "ConstantType" + ["name",n ; "params",params' ; "id", id] + [< print_term ids_to_inner_sorts ty >] + >] + in + xmlty, xmlbo + | A.AVariable (id,n,bo,ty,params) -> + let params' = param_attribute_of_params params in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n") ; + X.xml_nempty "Variable" ["name",n ; "params",params' ; "id", id] + [< (match bo with + None -> [<>] + | Some bo -> + X.xml_nempty "body" [] + (print_term ids_to_inner_sorts bo) + ) ; + X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) + >] + >], None + | A.AInductiveDefinition (id,tys,params,nparams) -> + let params' = param_attribute_of_params params in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ + dtdname ^ "\">\n") ; + X.xml_nempty "InductiveDefinition" + ["noParams",string_of_int nparams ; + "id",id ; + "params",params'] + [< (List.fold_left + (fun i (id,typename,finite,arity,cons) -> + [< i ; + X.xml_nempty "InductiveType" + ["id",id ; "name",Names.string_of_id typename ; + "inductive",(string_of_bool finite) + ] + [< X.xml_nempty "arity" [] + (print_term ids_to_inner_sorts arity) ; + (List.fold_left + (fun i (name,lc) -> + [< i ; + X.xml_nempty "Constructor" + ["name",Names.string_of_id name] + (print_term ids_to_inner_sorts lc) + >]) [<>] cons + ) + >] + >] + ) [< >] tys + ) + >] + >], None + in + aux +;; + +let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = + let module C2A = Cic2acic in + let module X = Xml in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^"\">\n"); + X.xml_nempty "InnerTypes" ["of",curi] + (Hashtbl.fold + (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> + [< x ; + X.xml_nempty "TYPE" ["of",id] + [< X.xml_nempty "synthesized" [] + (print_term ids_to_inner_sorts synty) ; + match expty with + None -> [<>] + | Some expty' -> + X.xml_nempty "expected" [] + (print_term ids_to_inner_sorts expty') + >] + >] + ) ids_to_inner_types [<>] + ) + >] +;; diff --git a/plugins/xml/cic.dtd b/plugins/xml/cic.dtd new file mode 100644 index 00000000..c8035cab --- /dev/null +++ b/plugins/xml/cic.dtd @@ -0,0 +1,259 @@ +<?xml encoding="ISO-8859-1"?> + +<!-- Copyright (C) 2000-2004, HELM Team --> +<!-- --> +<!-- This file is part of HELM, an Hypertextual, Electronic --> +<!-- Library of Mathematics, developed at the Computer Science --> +<!-- Department, University of Bologna, Italy. --> +<!-- --> +<!-- HELM is free software; you can redistribute it and/or --> +<!-- modify it under the terms of the GNU General Public License --> +<!-- as published by the Free Software Foundation; either version 2 --> +<!-- of the License, or (at your option) any later version. --> +<!-- --> +<!-- HELM is distributed in the hope that it will be useful, --> +<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of --> +<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the --> +<!-- GNU General Public License for more details. --> +<!-- --> +<!-- You should have received a copy of the GNU General Public License --> +<!-- along with HELM; if not, write to the Free Software --> +<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, --> +<!-- MA 02111-1307, USA. --> +<!-- --> +<!-- For details, see the HELM World-Wide-Web page, --> +<!-- http://cs.unibo.it/helm/. --> + +<!-- DTD FOR CIC OBJECTS: --> + +<!-- CIC term declaration --> + +<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST| + LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'> + +<!-- CIC sorts --> + +<!ENTITY % sort '(Prop|Set|Type|CProp)'> + +<!-- CIC sequents --> + +<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> + +<!-- CIC objects: --> + +<!ELEMENT ConstantType %term;> +<!ATTLIST ConstantType + name CDATA #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT ConstantBody %term;> +<!ATTLIST ConstantBody + for CDATA #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT CurrentProof (Conjecture*,body)> +<!ATTLIST CurrentProof + of CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT InductiveDefinition (InductiveType+)> +<!ATTLIST InductiveDefinition + noParams NMTOKEN #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Variable (body?,type)> +<!ATTLIST Variable + name CDATA #REQUIRED + params CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Sequent %sequent;> +<!ATTLIST Sequent + no NMTOKEN #REQUIRED + id ID #REQUIRED> + +<!-- Elements used in CIC objects, which are not terms: --> + +<!ELEMENT InductiveType (arity,Constructor*)> +<!ATTLIST InductiveType + name CDATA #REQUIRED + inductive (true|false) #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Conjecture %sequent;> +<!ATTLIST Conjecture + no NMTOKEN #REQUIRED + id ID #REQUIRED> + +<!ELEMENT Constructor %term;> +<!ATTLIST Constructor + name CDATA #REQUIRED> + +<!ELEMENT Decl %term;> +<!ATTLIST Decl + name CDATA #IMPLIED + id ID #REQUIRED> + +<!ELEMENT Def %term;> +<!ATTLIST Def + name CDATA #IMPLIED + id ID #REQUIRED> + +<!ELEMENT Hidden EMPTY> +<!ATTLIST Hidden + id ID #REQUIRED> + +<!ELEMENT Goal %term;> + +<!-- CIC terms: --> + +<!ELEMENT LAMBDA (decl*,target)> +<!ATTLIST LAMBDA + sort %sort; #REQUIRED> + +<!ELEMENT LETIN (def*,target)> +<!ATTLIST LETIN + sort %sort; #REQUIRED> + +<!ELEMENT PROD (decl*,target)> +<!ATTLIST PROD + type %sort; #REQUIRED> + +<!ELEMENT CAST (term,type)> +<!ATTLIST CAST + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT REL EMPTY> +<!ATTLIST REL + value NMTOKEN #REQUIRED + binder CDATA #REQUIRED + id ID #REQUIRED + idref IDREF #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT SORT EMPTY> +<!ATTLIST SORT + value CDATA #REQUIRED + id ID #REQUIRED> + +<!ELEMENT APPLY (%term;)+> +<!ATTLIST APPLY + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT VAR EMPTY> +<!ATTLIST VAR + uri CDATA #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!-- The substitutions are ordered by increasing DeBrujin --> +<!-- index. An empty substitution means that that index is --> +<!-- not accessible. --> +<!ELEMENT META (substitution*)> +<!ATTLIST META + no NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT IMPLICIT EMPTY> +<!ATTLIST IMPLICIT + id ID #REQUIRED> + +<!ELEMENT CONST EMPTY> +<!ATTLIST CONST + uri CDATA #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT MUTIND EMPTY> +<!ATTLIST MUTIND + uri CDATA #REQUIRED + noType NMTOKEN #REQUIRED + id ID #REQUIRED> + +<!ELEMENT MUTCONSTRUCT EMPTY> +<!ATTLIST MUTCONSTRUCT + uri CDATA #REQUIRED + noType NMTOKEN #REQUIRED + noConstr NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)> +<!ATTLIST MUTCASE + uriType CDATA #REQUIRED + noType NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT FIX (FixFunction+)> +<!ATTLIST FIX + noFun NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!ELEMENT COFIX (CofixFunction+)> +<!ATTLIST COFIX + noFun NMTOKEN #REQUIRED + id ID #REQUIRED + sort %sort; #REQUIRED> + +<!-- Elements used in CIC terms: --> + +<!ELEMENT FixFunction (type,body)> +<!ATTLIST FixFunction + name CDATA #REQUIRED + id ID #REQUIRED + recIndex NMTOKEN #REQUIRED> + +<!ELEMENT CofixFunction (type,body)> +<!ATTLIST CofixFunction + id ID #REQUIRED + name CDATA #REQUIRED> + +<!ELEMENT substitution ((%term;)?)> + +<!-- Explicit named substitutions: --> + +<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)> +<!ATTLIST instantiate + id ID #IMPLIED> + +<!-- Sintactic sugar for CIC terms and for CIC objects: --> + +<!ELEMENT arg %term;> +<!ATTLIST arg + relUri CDATA #REQUIRED> + +<!ELEMENT decl %term;> +<!ATTLIST decl + id ID #REQUIRED + type %sort; #REQUIRED + binder CDATA #IMPLIED> + +<!ELEMENT def %term;> +<!ATTLIST def + id ID #REQUIRED + sort %sort; #REQUIRED + binder CDATA #IMPLIED> + +<!ELEMENT target %term;> + +<!ELEMENT term %term;> + +<!ELEMENT type %term;> + +<!ELEMENT arity %term;> + +<!ELEMENT patternsType %term;> + +<!ELEMENT inductiveTerm %term;> + +<!ELEMENT pattern %term;> + +<!ELEMENT body %term;> diff --git a/plugins/xml/cic2Xml.ml b/plugins/xml/cic2Xml.ml new file mode 100644 index 00000000..981503a6 --- /dev/null +++ b/plugins/xml/cic2Xml.ml @@ -0,0 +1,17 @@ +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 new file mode 100644 index 00000000..a80ceb0f --- /dev/null +++ b/plugins/xml/cic2acic.ml @@ -0,0 +1,942 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(* Utility Functions *) + +exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; +let get_module_path_of_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.warning ("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 _ -> +(*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 new file mode 100644 index 00000000..f8921aec --- /dev/null +++ b/plugins/xml/doubleTypeInference.ml @@ -0,0 +1,272 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *) +type types = {synthesized : Term.types ; expected : Term.types option};; + +let prerr_endline _ = ();; + +let cprop = + let module N = Names in + N.make_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 = Rawterm 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 _ -> (* 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 new file mode 100644 index 00000000..b604ec4c --- /dev/null +++ b/plugins/xml/doubleTypeInference.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +type types = { synthesized : Term.types; expected : Term.types option; } + +val cprop : Names.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 new file mode 100644 index 00000000..9419ba59 --- /dev/null +++ b/plugins/xml/dumptree.ml4 @@ -0,0 +1,152 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \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 + | Proof_instr (_,instr) -> pr_proof_instr_xml instr + end ++ fnl () + ++ pr subtree + ) ++ fnl () ++ str "</cmpdrule>" + | Daimon -> str "<daimon/>" + | Decl_proof _ -> str "<proof/>" +(* | Change_evars -> str "<chgevars/>"*) +;; + +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_ltype_env_at_top env typ) ++ + str "\"/>" + in + List.fold_left (++) (mt ()) (List.map pr_one metas) +;; + +let pr_goal_xml g = + let env = try evar_unfiltered_env g with _ -> empty_env in + if g.evar_extra = None then + (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++ + xmlstream (pr_ltype_env_at_top env g.evar_concl) ++ + str "\"/>" ++ + (pr_context_xml env)) ++ + fnl () ++ str "</goal>") + else + (hov 2 (str "<goal type=\"declarative\">" ++ + (pr_context_xml env)) ++ + fnl () ++ str "</goal>") +;; + +let rec print_proof_xml sigma osign pf = + let hyps = Environ.named_context_of_val pf.goal.evar_hyps in + let hyps' = thin_sign osign hyps in + match pf.ref with + | None -> hov 2 (str "<tree>" ++ fnl () ++ (pr_goal_xml {pf.goal with evar_hyps=hyps'})) ++ fnl () ++ str "</tree>" + | Some(r,spfl) -> + hov 2 (str "<tree>" ++ fnl () ++ + (pr_goal_xml {pf.goal with evar_hyps=hyps'}) ++ fnl () ++ (pr_rule_xml (print_proof_xml sigma osign) r) ++ + (List.fold_left (fun x y -> x ++ fnl () ++ y) (mt ()) (List.map (print_proof_xml sigma hyps) spfl))) ++ fnl () ++ str "</tree>" +;; + +let print_proof_xml () = + let pp = print_proof_xml Evd.empty Sign.empty_named_context + (Tacmach.proof_of_pftreestate (Refiner.top_of_tree (Pfedit.get_pftreestate ()))) + in + msgnl pp +;; + +VERNAC COMMAND EXTEND DumpTree + [ "Dump" "Tree" ] -> [ print_proof_xml () ] +END diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml new file mode 100644 index 00000000..1beabf26 --- /dev/null +++ b/plugins/xml/proof2aproof.ml @@ -0,0 +1,176 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(* Note: we can not use the Set module here because we _need_ physical *) +(* equality and there exists no comparison function compatible with *) +(* physical equality. *) + +module S = + struct + let empty = [] + let mem = List.memq + let add x l = x::l + end +;; + +(* evar reduction that preserves some terms *) +let nf_evar sigma ~preserve = + let module T = Term in + let rec aux t = + if preserve t then t else + match T.kind_of_term t with + | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _ + | T.Construct _ -> t + | T.Cast (c1,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 +;; + +(* Unshares a proof-tree. *) +(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *) +let rec unshare_proof_tree = + let module PT = Proof_type in + function {PT.open_subgoals = status ; + PT.goal = goal ; + PT.ref = ref} -> + let unshared_ref = + match ref with + None -> None + | Some (rule,pfs) -> + let unshared_rule = + match rule with + PT.Nested (cmpd, pf) -> + PT.Nested (cmpd, unshare_proof_tree pf) + | other -> other + in + Some (unshared_rule, List.map unshare_proof_tree pfs) + in + {PT.open_subgoals = status ; + PT.goal = goal ; + PT.ref = unshared_ref} +;; + +module ProofTreeHash = + Hashtbl.Make + (struct + type t = Proof_type.proof_tree + let equal = (==) + let hash = Hashtbl.hash + end) +;; + + +let extract_open_proof sigma pf = + let module PT = Proof_type in + let module L = Logic in + let evd = ref (Evd.create_evar_defs sigma) in + let proof_tree_to_constr = ProofTreeHash.create 503 in + let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in + let unshared_constrs = ref S.empty in + let rec proof_extractor vl node = + let constr = + match node with + {PT.ref=Some(PT.Prim _,_)} as pf -> + L.prim_extractor proof_extractor vl pf + + | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} -> + let sgl,v = Refiner.frontier hidden_proof in + let flat_proof = v spfl in + ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ; + proof_extractor vl flat_proof + + | {PT.ref=None;PT.goal=goal} -> + let visible_rels = + Util.map_succeed + (fun id -> + (* Section variables are in the [id] list but are not *) + (* lambda abstracted in the term [vl] *) + try let n = Logic.proof_variable_index id vl in (n,id) + with Not_found -> failwith "caught") +(*CSC: the above function must be modified such that when it is found *) +(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *) +(*CSC: as the evar_instance. Ordering the instance becomes useless (it *) +(*CSC: will already be ordered. *) + (Termops.ids_of_named_context + (Environ.named_context_of_val goal.Evd.evar_hyps)) in + let sorted_rels = + Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in + let context = + let l = + List.map + (fun (_,id) -> Sign.lookup_named id + (Environ.named_context_of_val goal.Evd.evar_hyps)) + sorted_rels in + Environ.val_of_named_context l + in +(*CSC: the section variables in the right order must be added too *) + let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in + (* let env = Global.env_of_context context in *) + let evd',evar = + Evarutil.new_evar_instance context !evd goal.Evd.evar_concl + evar_instance in + evd := evd' ; + evar + + | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor" + in + let unsharedconstr = + let evar_nf_constr = + nf_evar ( !evd) + ~preserve:(function e -> S.mem e !unshared_constrs) constr + in + Unshare.unshare + ~already_unshared:(function e -> S.mem e !unshared_constrs) + evar_nf_constr + in +(*CSC: debugging stuff to be removed *) +if ProofTreeHash.mem proof_tree_to_constr node then + Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") + (Tactic_printer.print_proof ( !evd) [] node)) ; + ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; + unshared_constrs := S.add unsharedconstr !unshared_constrs ; + unsharedconstr + in + let unshared_pf = unshare_proof_tree pf in + let pfterm = proof_extractor [] unshared_pf in + (pfterm, !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, + unshared_pf) +;; + +let extract_open_pftreestate pts = + extract_open_proof (Refiner.evc_of_pftreestate pts) + (Tacmach.proof_of_pftreestate pts) +;; diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 new file mode 100644 index 00000000..3f1e0a63 --- /dev/null +++ b/plugins/xml/proofTree2Xml.ml4 @@ -0,0 +1,210 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; + +let std_ppcmds_to_string s = + Pp.msg_with Format.str_formatter s; + Format.flush_str_formatter () +;; + +let idref_of_id id = "v" ^ id;; + +(* Transform a constr to an Xml.token Stream.t *) +(* env is a named context *) +(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *) +let constr_to_xml obj sigma env = + let ids_to_terms = Hashtbl.create 503 in + let constr_to_ids = Acic.CicHash.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + + (* 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 = std_ppcmds_to_string (prtac tactic_expr) in + let tacname= first_word tac in + let of_attribute = ("name",tacname)::("script",tac)::of_attribute in + + (****** le but *) + let {Evd.evar_concl=concl; + Evd.evar_hyps=hyps}=goal in + + let 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.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} -> + Util.anomaly "Not Implemented" + + | {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 + 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 new file mode 100644 index 00000000..953fe009 --- /dev/null +++ b/plugins/xml/theoryobject.dtd @@ -0,0 +1,62 @@ +<?xml encoding="ISO-8859-1"?> + +<!-- Copyright (C) 2000-2004, HELM Team --> +<!-- --> +<!-- This file is part of HELM, an Hypertextual, Electronic --> +<!-- Library of Mathematics, developed at the Computer Science --> +<!-- Department, University of Bologna, Italy. --> +<!-- --> +<!-- HELM is free software; you can redistribute it and/or --> +<!-- modify it under the terms of the GNU General Public License --> +<!-- as published by the Free Software Foundation; either version 2 --> +<!-- of the License, or (at your option) any later version. --> +<!-- --> +<!-- HELM is distributed in the hope that it will be useful, --> +<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of --> +<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the --> +<!-- GNU General Public License for more details. --> +<!-- --> +<!-- You should have received a copy of the GNU General Public License --> +<!-- along with HELM; if not, write to the Free Software --> +<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, --> +<!-- MA 02111-1307, USA. --> +<!-- --> +<!-- For details, see the HELM World-Wide-Web page, --> +<!-- http://cs.unibo.it/helm/. --> + + + +<!-- Notice: the markup described in this DTD is meant to be embedded --> +<!-- in foreign markup (e.g. XHTML) --> + +<!ENTITY % theorystructure + '(ht:AXIOM|ht:DEFINITION|ht:THEOREM|ht:VARIABLE|ht:SECTION|ht:MUTUAL)*'> + +<!ELEMENT ht:SECTION (%theorystructure;)> +<!ATTLIST ht:SECTION + uri CDATA #REQUIRED> + +<!ELEMENT ht:MUTUAL (ht:DEFINITION,ht:DEFINITION+)> + +<!-- Theory Items --> + +<!ELEMENT ht:AXIOM (Axiom)> +<!ATTLIST ht:AXIOM + uri CDATA #REQUIRED + as (Axiom|Declaration) #REQUIRED> + +<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)> +<!ATTLIST ht:DEFINITION + uri CDATA #REQUIRED + as (Definition|InteractiveDefinition|Inductive|CoInductive + |Record) #REQUIRED> + +<!ELEMENT ht:THEOREM (type)> +<!ATTLIST ht:THEOREM + uri CDATA #REQUIRED + as (Theorem|Lemma|Corollary|Fact|Remark) #REQUIRED> + +<!ELEMENT ht:VARIABLE (Variable)> +<!ATTLIST ht:VARIABLE + uri CDATA #REQUIRED + as (Assumption|Hypothesis|LocalDefinition|LocalFact) #REQUIRED> diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml new file mode 100644 index 00000000..f30f8230 --- /dev/null +++ b/plugins/xml/unshare.ml @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +exception CanNotUnshare;; + +(* [unshare t] gives back a copy of t where all sharing has been removed *) +(* Physical equality becomes meaningful on unshared terms. Hashtables that *) +(* use physical equality can now be used to associate information to evey *) +(* node of the term. *) +let unshare ?(already_unshared = function _ -> false) t = + let obj = Obj.repr t in + let rec aux obj = + if already_unshared (Obj.obj obj) then + obj + else + (if Obj.is_int obj then + obj + else if Obj.is_block obj then + begin + let tag = Obj.tag obj in + if tag < Obj.no_scan_tag then + begin + let size = Obj.size obj in + let new_obj = Obj.new_block 0 size in + Obj.set_tag new_obj tag ; + for i = 0 to size - 1 do + Obj.set_field new_obj i (aux (Obj.field obj i)) + done ; + new_obj + end + else if tag = Obj.string_tag then + obj + else + raise CanNotUnshare + end + else + raise CanNotUnshare + ) + in + Obj.obj (aux obj) +;; diff --git a/plugins/xml/unshare.mli b/plugins/xml/unshare.mli new file mode 100644 index 00000000..31ba9037 --- /dev/null +++ b/plugins/xml/unshare.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +exception CanNotUnshare;; + +(* [unshare t] gives back a copy of t where all sharing has been removed *) +(* Physical equality becomes meaningful on unshared terms. Hashtables that *) +(* use physical equality can now be used to associate information to evey *) +(* node of the term. *) +val unshare: ?already_unshared:('a -> bool) -> 'a -> 'a diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4 new file mode 100644 index 00000000..5b217119 --- /dev/null +++ b/plugins/xml/xml.ml4 @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(* the type token for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t +;; + +(* currified versions of the constructors make the code more readable *) +let xml_empty name attrs = [< 'Empty(name,attrs) >] +let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] +let xml_cdata str = [< 'Str str >] + +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +let pp_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 new file mode 100644 index 00000000..3775287a --- /dev/null +++ b/plugins/xml/xml.mli @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(*i $Id$ i*) + +(* Tokens for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = + | Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t + +(* currified versions of the token constructors make the code more readable *) +val xml_empty : string -> (string * string) list -> token Stream.t +val xml_nempty : + string -> (string * string) list -> token Stream.t -> token Stream.t +val xml_cdata : string -> token Stream.t + +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 new file mode 100644 index 00000000..90797e8d --- /dev/null +++ b/plugins/xml/xml_plugin.mllib @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..2299e6c8 --- /dev/null +++ b/plugins/xml/xmlcommand.ml @@ -0,0 +1,719 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(* CONFIGURATION PARAMETERS *) + +let verbose = ref false;; + +(* HOOKS *) +let print_proof_tree, set_print_proof_tree = + let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in + (fun () -> !print_proof_tree), + (fun f -> + print_proof_tree := + fun + curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree + constr_to_ids + -> + Some + (f curi sigma0 pf proof_tree_to_constr + proof_tree_to_flattened_proof_tree constr_to_ids)) +;; + +(* UTILITY FUNCTIONS *) + +let print_if_verbose s = if !verbose then print_string s;; + +(* Next exception is used only inside print_coq_object and tag_of_string_tag *) +exception Uninteresting;; + +(* 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 _ -> () (* 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.warning "Conjecture not supported in dtd (used Declaration instead)"; + "AXIOM","Declaration" + | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" + | DK.IsDefinition DK.Example -> + Pp.warning "Example not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Coercion -> + Pp.warning "Coercion not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.SubClass -> + Pp.warning "SubClass not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.CanonicalStructure -> + Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Fixpoint -> + Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.CoFixpoint -> + Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Scheme -> + Pp.warning "Scheme not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.StructureComponent -> + Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.IdentityCoercion -> + Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Instance -> + Pp.warning "Instance not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Method -> + Pp.warning "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.warning "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 {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = + G.lookup_constant kn 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 = + let pf = Tacmach.proof_of_pftreestate pftst in + let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in + let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree, + unshared_pf + = + Proof2aproof.extract_open_pftreestate pftst in + let env = Global.env () in + let obj = + mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in + let uri = + match kind with + Decl_kinds.Local, _ -> + let uri = + "cic:/" ^ String.concat "/" + (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable) + in + let kind_of_var = "VARIABLE","LocalFact" in + (match internal with + | Declare.KernelSilent -> () + | _ -> print_object_kind uri kind_of_var + ); uri + | Decl_kinds.Global, _ -> + let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in + (match internal with + | Declare.KernelSilent -> () + | _ -> print_object_kind uri (kind_of_global_goal kind) + ); uri + in + print_object uri obj evar_map + (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr, + proof_tree_to_flattened_proof_tree)) fn +;; + +let show fn = + let pftst = Pfedit.get_pftreestate () in + let (id,kind,_,_) = Pfedit.current_proof_statement () in + show_pftreestate Declare.KernelVerbose 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 new file mode 100644 index 00000000..66ff9f0b --- /dev/null +++ b/plugins/xml/xmlcommand.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(*i $Id$ i*) + +(* print_global qid fn *) +(* where qid is a long name denoting a definition/theorem or *) +(* an inductive definition *) +(* and dest is either None (for stdout) or (Some filename) *) +(* pretty prints via Xml.pp the object whose name is ref on dest *) +(* Note: it is printed only (and directly) the most discharged available *) +(* form of the definition (all the parameters are *) +(* lambda-abstracted, but the object can still refer to variables) *) +val print_ref : Libnames.reference -> string option -> unit + +(* show dest *) +(* where dest is either None (for stdout) or (Some filename) *) +(* pretty prints via Xml.pp the proof in progress on dest *) +val show : string option -> unit + +(* set_print_proof_tree f *) +(* sets a callback function f to export the proof_tree to XML *) +val set_print_proof_tree : + (string -> + Evd.evar_map -> + Proof_type.proof_tree -> + Term.constr Proof2aproof.ProofTreeHash.t -> + Proof_type.proof_tree Proof2aproof.ProofTreeHash.t -> + string Acic.CicHash.t -> Xml.token Stream.t) -> + unit diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 new file mode 100644 index 00000000..41c107ad --- /dev/null +++ b/plugins/xml/xmlentries.ml4 @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +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 |