From 7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Sep 2014 18:34:04 +0200 Subject: Removing the XML plugin. Left a README, just in case someone will discover the remnants of it decades from now. --- .gitignore | 5 - Makefile.build | 3 +- Makefile.common | 8 +- intf/tacexpr.mli | 2 - parsing/g_ltac.ml4 | 2 - parsing/parsing.mllib | 1 - plugins/pluginsbyte.itarget | 1 - plugins/pluginsdyn.itarget | 1 - plugins/pluginsopt.itarget | 1 - plugins/xml/COPYRIGHT | 25 - plugins/xml/README | 256 +--------- plugins/xml/acic.ml | 108 ----- plugins/xml/acic2Xml.ml4 | 363 -------------- plugins/xml/cic.dtd | 259 ---------- plugins/xml/cic2Xml.ml | 17 - plugins/xml/cic2acic.ml | 927 ------------------------------------ plugins/xml/doubleTypeInference.ml | 266 ----------- plugins/xml/doubleTypeInference.mli | 24 - plugins/xml/theoryobject.dtd | 62 --- plugins/xml/unshare.ml | 52 -- plugins/xml/unshare.mli | 21 - plugins/xml/xml.ml4 | 78 --- plugins/xml/xml.mli | 38 -- plugins/xml/xml_plugin.mllib | 10 - plugins/xml/xmlcommand.ml | 536 --------------------- plugins/xml/xmlcommand.mli | 28 -- plugins/xml/xmlentries.ml4 | 32 -- printing/pptactic.ml | 3 - tactics/tacintern.ml | 4 +- tactics/tacinterp.ml | 28 -- tactics/tacinterp.mli | 4 - tactics/tacsubst.ml | 2 - theories/Init/Prelude.v | 1 - 33 files changed, 8 insertions(+), 3160 deletions(-) delete mode 100644 plugins/xml/COPYRIGHT delete mode 100644 plugins/xml/acic.ml delete mode 100644 plugins/xml/acic2Xml.ml4 delete mode 100644 plugins/xml/cic.dtd delete mode 100644 plugins/xml/cic2Xml.ml delete mode 100644 plugins/xml/cic2acic.ml delete mode 100644 plugins/xml/doubleTypeInference.ml delete mode 100644 plugins/xml/doubleTypeInference.mli delete mode 100644 plugins/xml/theoryobject.dtd delete mode 100644 plugins/xml/unshare.ml delete mode 100644 plugins/xml/unshare.mli delete mode 100644 plugins/xml/xml.ml4 delete mode 100644 plugins/xml/xml.mli delete mode 100644 plugins/xml/xml_plugin.mllib delete mode 100644 plugins/xml/xmlcommand.ml delete mode 100644 plugins/xml/xmlcommand.mli delete mode 100644 plugins/xml/xmlentries.ml4 diff --git a/.gitignore b/.gitignore index b91f40129..1820bf7f9 100644 --- a/.gitignore +++ b/.gitignore @@ -122,11 +122,6 @@ grammar/vernacextend.ml grammar/argextend.ml parsing/pcoq.ml parsing/lexer.ml -plugins/xml/proofTree2Xml.ml -plugins/xml/acic2Xml.ml -plugins/xml/xml.ml -plugins/xml/dumptree.ml -plugins/xml/xmlentries.ml plugins/setoid_ring/newring.ml plugins/field/field.ml plugins/nsatz/nsatz.ml diff --git a/Makefile.build b/Makefile.build index 147f7e315..49ce0a663 100644 --- a/Makefile.build +++ b/Makefile.build @@ -552,7 +552,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ # 3) plugins ########################################################################### -.PHONY: plugins omega micromega setoid_ring nsatz xml extraction +.PHONY: plugins omega micromega setoid_ring nsatz extraction .PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte plugins: $(PLUGINSVO) @@ -560,7 +560,6 @@ omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMA) nsatz: $(NSATZVO) $(NSATZCMA) -xml: $(XMLVO) $(XMLCMA) extraction: $(EXTRACTIONCMA) fourier: $(FOURIERVO) $(FOURIERCMA) funind: $(FUNINDCMA) $(FUNINDVO) diff --git a/Makefile.common b/Makefile.common index 8e7cebdcb..812fbeeaf 100644 --- a/Makefile.common +++ b/Makefile.common @@ -175,7 +175,6 @@ MICROMEGACMA:=plugins/micromega/micromega_plugin.cma QUOTECMA:=plugins/quote/quote_plugin.cma RINGCMA:=plugins/setoid_ring/newring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -XMLCMA:=plugins/xml/xml_plugin.cma FOURIERCMA:=plugins/fourier/fourier_plugin.cma EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma FUNINDCMA:=plugins/funind/recdef_plugin.cma @@ -195,7 +194,7 @@ DERIVECMA:=plugins/Derive/derive_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) \ - $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ + $(FOURIERCMA) $(EXTRACTIONCMA) \ $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \ $(DERIVECMA) @@ -203,7 +202,7 @@ PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ - $(XMLCMA) $(FUNINDCMA) $(NATSYNTAXCMA) + $(FUNINDCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) @@ -314,12 +313,11 @@ FUNINDVO:=$(call cat_vo_itarget, plugins/funind) BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto) RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) -XMLVO:= CCVO:= DERIVEVO:=$(call cat_vo_itarget, plugins/Derive) PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \ - $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ + $(FOURIERVO) $(CCVO) $(FUNINDVO) \ $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e2995cfab..55d6e53a5 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -185,8 +185,6 @@ and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg = | Reference of 'ref | TacCall of Loc.t * 'ref * ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list - | TacExternal of Loc.t * string * string * - ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list | TacFreshId of string or_var list | Tacexp of ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr | TacPretype of 'trm diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index faea9badd..d8620a0f2 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -101,8 +101,6 @@ GEXTEND Gram | IDENT "idtac"; l = LIST0 message_token -> TacId l | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) - | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> - TacArg (!@loc,TacExternal (!@loc,com,req,la)) | st = simple_tactic -> st | IDENT "constr"; ":"; c = Constr.constr -> TacArg(!@loc,ConstrMayEval(ConstrTerm c)) diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 500d7dde9..a0cb83193 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -4,4 +4,3 @@ Lexer Pcoq Egramml Egramcoq -G_xml diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index 744b07539..e884554e4 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -8,7 +8,6 @@ fourier/fourier_plugin.cma romega/romega_plugin.cma omega/omega_plugin.cma micromega/micromega_plugin.cma -xml/xml_plugin.cma cc/cc_plugin.cma nsatz/nsatz_plugin.cma funind/recdef_plugin.cma diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget index 188eb408a..a2517d82b 100644 --- a/plugins/pluginsdyn.itarget +++ b/plugins/pluginsdyn.itarget @@ -9,7 +9,6 @@ fourier/fourier_plugin.cmxs romega/romega_plugin.cmxs omega/omega_plugin.cmxs micromega/micromega_plugin.cmxs -xml/xml_plugin.cmxs subtac/subtac_plugin.cmxs ring/ring_plugin.cmxs cc/cc_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget index 34b024663..e44d7c149 100644 --- a/plugins/pluginsopt.itarget +++ b/plugins/pluginsopt.itarget @@ -8,7 +8,6 @@ fourier/fourier_plugin.cmxa romega/romega_plugin.cmxa omega/omega_plugin.cmxa micromega/micromega_plugin.cmxa -xml/xml_plugin.cmxa cc/cc_plugin.cmxa nsatz/nsatz_plugin.cmxa funind/recdef_plugin.cmxa diff --git a/plugins/xml/COPYRIGHT b/plugins/xml/COPYRIGHT deleted file mode 100644 index c8d231fd3..000000000 --- a/plugins/xml/COPYRIGHT +++ /dev/null @@ -1,25 +0,0 @@ -(******************************************************************************) -(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen *) -(* 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 - as a developer of projects HELM and MoWGLI. - -Project HELM (for Hypertextual Electronic Library of Mathematics) is a -project developed at the Department of Computer Science, University of Bologna; -http://helm.cs.unibo.it - -Project MoWGLI (Mathematics on the Web: Get It by Logics and Interfaces) -is a UE IST project that generalizes and extends the HELM project; -http://mowgli.cs.unibo.it - -The author is interested in any possible usage of the module. -So, if you plan to use the module, please send him an e-mail. - -The licensing policy applied to the module is the same as for the whole Coq -distribution. diff --git a/plugins/xml/README b/plugins/xml/README index a45dd31a5..cf5b3e0f4 100644 --- a/plugins/xml/README +++ b/plugins/xml/README @@ -1,254 +1,4 @@ -(******************************************************************************) -(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen *) -(* Project Helm (http://helm.cs.unibo.it) *) -(* Project MoWGLI (http://mowgli.cs.unibo.it) *) -(* *) -(* Coq Exportation to XML *) -(* *) -(******************************************************************************) +Here was the XML plugin. It is now defunct. May its soul rest in peace. -This module provides commands to export a piece of Coq library in XML format. -Only the information relevant to proof-checking and proof-rendering is exported, -i.e. only the CIC proof objects (lambda-terms). - -This document is tructured in the following way: - 1. User documentation - 1.1. New vernacular commands available - 1.2. New coqc/coqtop flags and suggested usage - 1.3. How to exploit the XML files - 2. Technical informations - 2.1. Inner-types - 2.2. CIC with Explicit Named Substitutions - 2.3. The CIC with Explicit Named Substitutions XML DTD - -================================================================================ - USER DOCUMENTATION -================================================================================ - -======================================= -1.1. New vernacular commands available: -======================================= - -The new commands are: - - Print XML qualid. It prints in XML (to standard output) the - object whose qualified name is qualid and - its inner-types (see Sect. 2.1). - The inner-types are always printed - in their own XML file. If the object is a - constant, its type and body are also printed - as two distinct XML files. - The object printed is always the most - discharged form of the object (see - the Section command of the Coq manual). - - Print XML File "filename" qualid. Similar to "Print XML qualid". The generated - files are stored on the hard-disk using the - base file name "filename". - - Show XML Proof. It prints in XML the current proof in - progress. Its inner-types are also printed. - - Show XML File "filename" Proof. Similar to "Show XML Proof". The generated - files are stored on the hard-disk using - the base file name "filename". - - The verbosity of the previous commands is raised if the configuration - parameter verbose of xmlcommand.ml is set to true at compile time. - -============================================== -1.2. New coqc/coqtop flags and suggested usage -============================================== - - The following flag has been added to coqc and coqtop: - - -xml export XML files either to the hierarchy rooted in - the directory $COQ_XML_LIBRARY_ROOT (if the environment - variable is set) or to stdout (if unset) - - If the flag is set, every definition or declaration is immediately - exported to XML. The XML files describe the user-provided non-discharged - form of the definition or declaration. - - - The coq_makefile utility has also been modified to easily allow XML - exportation: - - make COQ_XML=-xml (or, equivalently, setting the environment - variable COQ_XML) - - - The suggested usage of the module is the following: - - 1. add to your own contribution a valid Make file and use coq_makefile - to generate the Makefile from the Make file. - *WARNING:* Since logical names are used to structure the XML hierarchy, - always add to the Make file at least one "-R" option to map physical - file names to logical module paths. See the Coq manual for further - informations on the -R flag. - 2. set $COQ_XML_LIBRARY_ROOT to the directory where the XML file hierarchy - must be physically rooted. - 3. compile your contribution with "make COQ_XML=-xml" - - -================================= -1.3. How to exploit the XML files -================================= - - Once the information is exported to XML, it becomes possible to implement - services that are completely Coq-independent. Projects HELM and MoWGLI - already provide rendering, searching and data mining functionalities. - - In particular, the standard library and contributions of Coq can be - browsed and searched on the HELM web site: - - http://helm.cs.unibo.it/library.html - - - If you want to publish your own contribution so that it is included in the - HELM library, use the MoWGLI prototype upload form: - - http://mowgli.cs.unibo.it - - -================================================================================ - TECHNICAL INFORMATIONS -================================================================================ - -========================== -2.1. Inner-types -========================== - -In order to do proof-rendering (for example in natural language), -some redundant typing information is required, i.e. the type of -at least some of the subterms of the bodies and types. So, each -new command described in section 1.1 print not only -the object, but also another XML file in which you can find -the type of all the subterms of the terms of the printed object -which respect the following conditions: - - 1. It's sort is Prop or CProp (the "sort"-like definition used in - CoRN to type computationally relevant predicative propositions). - 2. It is not a cast or an atomic term, i.e. it's root is not a CAST, REL, - VAR, MUTCONSTR or CONST. - 3. If it's root is a LAMBDA, then the root's parent node is not a LAMBDA, - i.e. only the type of the outer LAMBDA of a block of nested LAMBDAs is - printed. - -The rationale for the 3rd condition is that the type of the inner LAMBDAs -could be easily computed starting from the type of the outer LAMBDA; moreover, -the types of the inner LAMBDAs requires a lot of disk/memory space: removing -the 3rd condition leads to XML file that are two times as big as the ones -exported appling the 3rd condition. - -========================================== -2.2. CIC with Explicit Named Substitutions -========================================== - -The exported files are and XML encoding of the lambda-terms used by the -Coq system. The implementative details of the Coq system are hidden as much -as possible, so that the XML DTD is a straightforward encoding of the -Calculus of (Co)Inductive Constructions. - -Nevertheless, there is a feature of the Coq system that can not be -hidden in a completely satisfactory way: discharging. In Coq it is possible -to open a section, declare variables and use them in the rest of the section -as if they were axiom declarations. Once the section is closed, every definition -and theorem in the section is discharged by abstracting it over the section -variables. Variable declarations as well as section declarations are entirely -dropped. Since we are interested in an XML encoding of definitions and -theorems as close as possible to those directly provided the user, we -do not want to export discharged forms. Exporting non-discharged theorem -and definitions together with theorems that rely on the discharged forms -obliges the tools that work on the XML encoding to implement discharging to -achieve logical consistency. Moreover, the rendering of the files can be -misleading, since hyperlinks can be shown between occurrences of the discharge -form of a definition and the non-discharged definition, that are different -objects. - -To overcome the previous limitations, Claudio Sacerdoti Coen developed in his -PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions -with Explicit Named Substitutions, that is a slight extension of CIC where -discharging is not necessary. The DTD of the exported XML files describes -constants, inductive types and variables of the Calculus of (Co)Inductive -Constructions with Explicit Named Substitions. The conversion to the new -calculus is performed during the exportation phase. - -The following example shows a very small Coq development together with its -version in CIC with Explicit Named Substitutions. - -# CIC version: # -Section S. - Variable A : Prop. - - Definition impl := A -> A. - - Theorem t : impl. (* uses the undischarged form of impl *) - Proof. - exact (fun (a:A) => a). - Qed. - -End S. - -Theorem t' : (impl False). (* uses the discharged form of impl *) - Proof. - exact (t False). (* uses the discharged form of t *) - Qed. - -# Corresponding CIC with Explicit Named Substitutions version: # -Section S. - Variable A : Prop. - - Definition impl(A) := A -> A. (* theorems and definitions are - explicitly abstracted over the - variables. The name is sufficient - to completely describe the abstraction *) - - Theorem t(A) : impl. (* impl where A is not instantiated *) - Proof. - exact (fun (a:A) => a). - Qed. - -End S. - -Theorem t'() : impl{False/A}. (* impl where A is instantiated with False - Notice that t' does not depend on A *) - Proof. - exact t{False/A}. (* t where A is instantiated with False *) - Qed. - -Further details on the typing and reduction rules of the calculus can be -found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency -of the calculus is also proved. - -====================================================== -2.3. The CIC with Explicit Named Substitutions XML DTD -====================================================== - -A copy of the DTD can be found in the file "cic.dtd". - - is the root element of the files that correspond to - constant types. - 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) - is the root element of the file that correspond to - the body of a constant that depends on metavariables - (e.g. unfinished proofs) - is the root element of the files that correspond to variables - is the root element of the files that correspond to blocks - of mutually defined inductive definitions - -The elements - ,,,,,,,, ,, - ,,,, and -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 correspond to the application of an explicit named -substitution to its first argument, that is a reference to a definition -or declaration in the environment. - -All the other elements are just syntactic sugar. +If you were looking for it, try contacting Claudio Sacerdoti-Coen, its original +author, at sacerdot@cs.unibo.it. He had a working version in the past. diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml deleted file mode 100644 index da7e57766..000000000 --- a/plugins/xml/acic.ml +++ /dev/null @@ -1,108 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Errors.anomaly ~label:"find_last_id" (Pp.str "empty list") - | [id,_,_] -> id - | _::tl -> find_last_id tl -;; - -let export_existential ev = string_of_int (Evar.repr ev) - -let print_term ids_to_inner_sorts = - let rec aux = - let module A = Acic in - let module N = Names in - let module X = Xml in - function - A.ARel (id,n,idref,b) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_empty "REL" - ["value",(string_of_int n) ; "binder",(N.Id.to_string b) ; - "id",id ; "idref",idref; "sort",sort] - | A.AVar (id,uri) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort] - | A.AEvar (id,n,l) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" - ["no",(export_existential n) ; "id",id ; "sort",sort] - (List.fold_left - (fun i t -> - [< i ; X.xml_nempty "substitution" [] (aux t) >] - ) [< >] (List.rev l)) - | A.ASort (id,s) -> - let string_of_sort = - match Term.family_of_sort s with - Term.InProp -> "Prop" - | Term.InSet -> "Set" - | Term.InType -> "Type" - in - X.xml_empty "SORT" ["value",string_of_sort ; "id",id] - | A.AProds (prods,t) -> - let last_id = find_last_id prods in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "PROD" ["type",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in - let attrs = - ("id",id)::("type",sort):: - match binder with - Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.Id.to_string b] - in - [< X.xml_nempty "decl" attrs (aux s) ; i >] - ) [< >] prods ; - X.xml_nempty "target" [] (aux t) - >] - | A.ACast (id,v,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "CAST" ["id",id ; "sort",sort] - [< X.xml_nempty "term" [] (aux v) ; - X.xml_nempty "type" [] (aux t) - >] - | A.ALambdas (lambdas,t) -> - let last_id = find_last_id lambdas in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LAMBDA" ["sort",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in - let attrs = - ("id",id)::("type",sort):: - match binder with - Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.Id.to_string b] - in - [< X.xml_nempty "decl" attrs (aux s) ; i >] - ) [< >] lambdas ; - X.xml_nempty "target" [] (aux t) - >] - | A.ALetIns (letins,t) -> - let last_id = find_last_id letins in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LETIN" ["sort",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in - let attrs = - ("id",id)::("sort",sort):: - match binder with - Names.Anonymous -> assert false - | Names.Name b -> ["binder",Names.Id.to_string b] - in - [< X.xml_nempty "def" attrs (aux s) ; i >] - ) [< >] letins ; - X.xml_nempty "target" [] (aux t) - >] - | A.AApp (id,li) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "APPLY" ["id",id ; "sort",sort] - [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li) - >] - | A.AConst (id,subst,uri) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - let attrs = ["uri", uri ; "id",id ; "sort",sort] in - aux_subst (X.xml_empty "CONST" attrs) subst - | A.AInd (id,subst,uri,i) -> - let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in - aux_subst (X.xml_empty "MUTIND" attrs) subst - | A.AConstruct (id,subst,uri,i,j) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - let attrs = - ["uri", uri ; - "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; - "id",id ; "sort",sort] - in - aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst - | A.ACase (id,uri,typeno,ty,te,patterns) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "MUTCASE" - ["uriType", uri ; - "noType", (string_of_int typeno) ; - "id", id ; "sort",sort] - [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; - X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; - List.fold_left - (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >]) - [<>] patterns - >] - | A.AFix (id, no, funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "FIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] - [< List.fold_left - (fun i (id,fi,ai,ti,bi) -> - [< i ; - X.xml_nempty "FixFunction" - ["id",id ; "name", (Names.Id.to_string fi) ; - "recIndex", (string_of_int ai)] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] - >] - ) [<>] funs - >] - | A.ACoFix (id,no,funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "COFIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] - [< List.fold_left - (fun i (id,fi,ti,bi) -> - [< i ; - X.xml_nempty "CofixFunction" - ["id",id ; "name", Names.Id.to_string fi] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] - >] - ) [<>] funs - >] - and aux_subst target (id,subst) = - if subst = [] then - target - else - Xml.xml_nempty "instantiate" - (match id with None -> [] | Some id -> ["id",id]) - [< target ; - List.fold_left - (fun i (uri,arg) -> - [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >] - ) [<>] subst - >] - in - aux -;; - -let param_attribute_of_params params = - List.fold_right - (fun (path,l) i -> - List.fold_right - (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i' - ) l "" ^ match i with "" -> "" | i' -> " " ^ i' - ) params "" -;; - -let print_object uri ids_to_inner_sorts = - let aux = - let module A = Acic in - let module X = Xml in - function - A.ACurrentProof (id,n,conjectures,bo,ty) -> - let xml_for_current_proof_body = -(*CSC: Should the CurrentProof also have the list of variables it depends on? *) -(*CSC: I think so. Not implemented yet. *) - X.xml_nempty "CurrentProof" ["of",uri ; "id", id] - [< List.fold_left - (fun i (cid,n,canonical_context,t) -> - [< i ; - X.xml_nempty "Conjecture" - ["id", cid ; "no",export_existential n] - [< List.fold_left - (fun i (hid,t) -> - [< (match t with - n,A.Decl t -> - X.xml_nempty "Decl" - ["id",hid;"name",Names.Id.to_string n] - (print_term ids_to_inner_sorts t) - | n,A.Def (t,_) -> - X.xml_nempty "Def" - ["id",hid;"name",Names.Id.to_string n] - (print_term ids_to_inner_sorts t) - ) ; - i - >] - ) [< >] canonical_context ; - X.xml_nempty "Goal" [] - (print_term ids_to_inner_sorts t) - >] - >]) - [<>] (List.rev conjectures) ; - X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] - in - let xml_for_current_proof_type = - X.xml_nempty "ConstantType" ["name",n ; "id", id] - (print_term ids_to_inner_sorts ty) - in - let xmlbo = - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - xml_for_current_proof_body - >] in - let xmlty = - [< X.xml_cdata "\n" ; - X.xml_cdata - ("\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 - "\n" ; - X.xml_cdata - ("\n") ; - X.xml_nempty "ConstantBody" - ["for",uri ; "params",params' ; "id", id] - [< print_term ids_to_inner_sorts bo >] - >] - in - let xmlty = - [< X.xml_cdata "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\n") ; - X.xml_nempty "InductiveDefinition" - ["noParams",string_of_int nparams ; - "id",id ; - "params",params'] - [< (List.fold_left - (fun i (id,typename,finite,arity,cons) -> - [< i ; - X.xml_nempty "InductiveType" - ["id",id ; "name",Names.Id.to_string typename ; - "inductive",(string_of_bool finite) - ] - [< X.xml_nempty "arity" [] - (print_term ids_to_inner_sorts arity) ; - (List.fold_left - (fun i (name,lc) -> - [< i ; - X.xml_nempty "Constructor" - ["name",Names.Id.to_string name] - (print_term ids_to_inner_sorts lc) - >]) [<>] cons - ) - >] - >] - ) [< >] tys - ) - >] - >], None - in - aux -;; - -let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = - let module C2A = Cic2acic in - let module X = Xml in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - X.xml_nempty "InnerTypes" ["of",curi] - (Hashtbl.fold - (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> - [< x ; - X.xml_nempty "TYPE" ["of",id] - [< X.xml_nempty "synthesized" [] - (print_term ids_to_inner_sorts synty) ; - match expty with - None -> [<>] - | Some expty' -> - X.xml_nempty "expected" [] - (print_term ids_to_inner_sorts expty') - >] - >] - ) ids_to_inner_types [<>] - ) - >] -;; diff --git a/plugins/xml/cic.dtd b/plugins/xml/cic.dtd deleted file mode 100644 index c8035cab9..000000000 --- a/plugins/xml/cic.dtd +++ /dev/null @@ -1,259 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/plugins/xml/cic2Xml.ml b/plugins/xml/cic2Xml.ml deleted file mode 100644 index 981503a66..000000000 --- a/plugins/xml/cic2Xml.ml +++ /dev/null @@ -1,17 +0,0 @@ -let print_xml_term ch env sigma cic = - let ids_to_terms = Hashtbl.create 503 in - let constr_to_ids = Acic.CicHash.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let seed = ref 0 in - let acic = - Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types - env [] sigma (Unshare.unshare cic) None in - let xml = Acic2Xml.print_term ids_to_inner_sorts acic in - Xml.pp_ch xml ch -;; - -Tacinterp.declare_xml_printer print_xml_term -;; diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml deleted file mode 100644 index bbaef1e70..000000000 --- a/plugins/xml/cic2acic.ml +++ /dev/null @@ -1,927 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Libnames.is_dirpath_prefix_of modul dirpath) modules - with - [] -> - Pp.msg_warning (Pp.str ("Modules not supported: reference to "^ - Libnames.string_of_path path^" will be wrong")); - dirpath - | [modul] -> modul - | _ -> - raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther -;; - -(*CSC: Problem: here we are using the wrong (???) hypothesis that there do *) -(*CSC: not exist two modules whose dir_paths are one a prefix of the other *) -let remove_module_dirpath_from_dirpath ~basedir dir = - if Libnames.is_dirpath_prefix_of basedir dir then - let ids = DirPath.repr dir in - let rec remove_firsts n l = - match n,l with - (0,l) -> l - | (n,he::tl) -> remove_firsts (n-1) tl - | _ -> assert false - in - let ids' = - List.rev - (remove_firsts - (List.length (DirPath.repr basedir)) - (List.rev ids)) - in - ids' - else DirPath.repr dir -;; - - -let get_uri_of_var v pvars = - let rec search_in_open_sections = - function - [] -> Errors.error ("Variable "^v^" not found") - | he::tl as modules -> - let dirpath = DirPath.make modules in - if Id.List.mem (Id.of_string v) (Decls.last_section_hyps dirpath) - then - modules - else - search_in_open_sections tl - in - let path = - if String.List.mem v pvars then - [] - else - search_in_open_sections (DirPath.repr (Lib.cwd ())) - in - "cic:" ^ - List.fold_left - (fun i x -> "/" ^ Id.to_string x ^ i) "" path -;; - -type tag = - Constant of Names.constant - | Inductive of Names.mutual_inductive - | Variable of Names.kernel_name -;; - -type etag = - TConstant - | TInductive - | TVariable -;; - -let etag_of_tag = - function - Constant _ -> TConstant - | Inductive _ -> TInductive - | Variable _ -> TVariable - -let ext_of_tag = - function - TConstant -> "con" - | TInductive -> "ind" - | TVariable -> "var" -;; - -exception FunctorsXMLExportationNotImplementedYet;; - -let subtract l1 l2 = - let l1' = List.rev (DirPath.repr l1) in - let l2' = List.rev (DirPath.repr l2) in - let rec aux = - function - he::tl when tl = l2' -> [he] - | he::tl -> he::(aux tl) - | [] -> assert (l2' = []) ; [] - in - DirPath.make (List.rev (aux l1')) -;; - -let token_list_of_path dir id tag = - let token_list_of_dirpath dirpath = - List.rev_map Id.to_string (DirPath.repr dirpath) in - token_list_of_dirpath dir @ [Id.to_string id ^ "." ^ (ext_of_tag tag)] - -let token_list_of_kernel_name tag = - let id,dir = match tag with - | Variable kn -> - Label.to_id (Names.label kn), Lib.cwd () - | Constant con -> - Label.to_id (Names.con_label con), - Lib.remove_section_part (Globnames.ConstRef con) - | Inductive kn -> - Label.to_id (Names.mind_label kn), - Lib.remove_section_part (Globnames.IndRef (kn,0)) - in - token_list_of_path dir id (etag_of_tag tag) -;; - -let uri_of_kernel_name tag = - let tokens = token_list_of_kernel_name tag in - "cic:/" ^ String.concat "/" tokens - -let uri_of_declaration id tag = - let dir = Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in - let tokens = token_list_of_path dir id tag in - "cic:/" ^ String.concat "/" tokens - -(* Special functions for handling of CCorn's CProp "sort" *) - -type sort = - Coq_sort of Term.sorts_family - | CProp -;; - -let prerr_endline _ = ();; - -let family_of_term ty = - match Term.kind_of_term ty with - Term.Sort s -> Coq_sort (Term.family_of_sort s) - | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Errors.anomaly (Pp.str "family_of_term") -;; - -module CPropRetyping = - struct - module T = Term - module V = Vars - - let outsort env sigma t = - family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t) - - let rec subst_type env sigma typ = function - | [] -> typ - | h::rest -> - match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with - | T.Prod (na,c1,c2) -> subst_type env sigma (V.subst1 h c2) rest - | _ -> Errors.anomaly (Pp.str "Non-functional construction") - - - let sort_of_atomic_type env sigma ft args = - let rec concl_of_arity env ar = - match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma ar) with - | T.Prod (na, t, b) -> concl_of_arity (Environ.push_rel (na,None,t) env) b - | T.Sort s -> Coq_sort (T.family_of_sort s) - | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args)) - in concl_of_arity env ft - -let typeur sigma metamap = - let rec type_of env cstr= - match Term.kind_of_term cstr with - | T.Proj _ -> assert false - | T.Meta n -> - (try T.strip_outer_cast (Int.List.assoc n metamap) - with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) - | T.Rel n -> - let (_,_,ty) = Environ.lookup_rel n env in - V.lift n ty - | T.Var id -> - (try - let (_,_,ty) = Environ.lookup_named id env in - ty - with Not_found -> - Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound")) - | T.Const c -> Typeops.type_of_constant_in env c - | T.Evar ev -> Evd.existential_type sigma ev - | T.Ind ind -> Inductiveops.type_of_inductive env ind - | T.Construct cstr -> Inductiveops.type_of_constructor env cstr - | T.Case (_,p,c,lf) -> - let Inductiveops.IndType(_,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in - let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in - (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with - | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) - | _ -> t) - | T.Lambda (name,c1,c2) -> - T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2) - | T.LetIn (name,b,c1,c2) -> - V.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) - | T.Fix ((_,i),(_,tys,_)) -> tys.(i) - | T.CoFix (i,(_,tys,_)) -> tys.(i) - | T.App(f,args)-> - T.strip_outer_cast - (subst_type env sigma (type_of env f) (Array.to_list args)) - | T.Cast (c,_, t) -> t - | T.Sort _ | T.Prod _ -> - match sort_of env cstr with - Coq_sort T.InProp -> T.mkProp - | Coq_sort T.InSet -> T.mkSet - | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *) - | CProp -> T.mkConst DoubleTypeInference.cprop - - and sort_of env t = - match Term.kind_of_term t with - | T.Cast (c,_, s) when T.isSort s -> family_of_term s - | T.Sort (T.Prop c) -> Coq_sort T.InType - | T.Sort (T.Type u) -> Coq_sort T.InType - | T.Prod (name,t,c2) -> - (match sort_of env t,sort_of (Environ.push_rel (name,None,t) env) c2 with - | _, (Coq_sort T.InProp as s) -> s - | Coq_sort T.InProp, (Coq_sort T.InSet as s) - | Coq_sort T.InSet, (Coq_sort T.InSet as s) -> s - | Coq_sort T.InType, (Coq_sort T.InSet as s) - | CProp, (Coq_sort T.InSet as s) when - Environ.engagement env = Some Declarations.ImpredicativeSet -> s - | Coq_sort T.InType, Coq_sort T.InSet - | CProp, Coq_sort T.InSet -> Coq_sort T.InType - | _, (Coq_sort T.InType as s) -> s (*Type Univ.dummy_univ*) - | _, (CProp as s) -> s) - | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args - | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") - | _ -> outsort env sigma (type_of env t) - - and sort_family_of env t = - match T.kind_of_term t with - | T.Cast (c,_, s) when T.isSort s -> family_of_term s - | T.Sort (T.Prop c) -> Coq_sort T.InType - | T.Sort (T.Type u) -> Coq_sort T.InType - | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2 - | T.App(f,args) -> - sort_of_atomic_type env sigma (type_of env f) args - | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") - | _ -> outsort env sigma (type_of env t) - - in type_of, sort_of, sort_family_of - - let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c - let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c - - end -;; - -let get_sort_family_of env evar_map ty = - CPropRetyping.get_sort_family_of env evar_map ty -;; - -let type_as_sort env evar_map ty = -(* CCorn code *) - family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env evar_map ty) -;; - -let is_a_Prop = - function - "Prop" - | "CProp" -> true - | _ -> false -;; - -(* Main Functions *) - -type anntypes = - {annsynthesized : Acic.aconstr ; annexpected : Acic.aconstr option} -;; - -let gen_id seed = - let res = "i" ^ string_of_int !seed in - incr seed ; - res -;; - -let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids = - fun father t -> - let res = gen_id seed in - Hashtbl.add ids_to_father_ids res father ; - Hashtbl.add ids_to_terms res t ; - Acic.CicHash.add constr_to_ids t res ; - res -;; - -let source_id_of_id id = "#source#" ^ id;; - -let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types - ?(fake_dependent_products=false) env idrefs evar_map t expectedty -= - let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in - (* CSC: do you have any reasonable substitute for 503? *) - let terms_to_types = Acic.CicHash.create 503 in - DoubleTypeInference.double_type_of env evar_map t expectedty terms_to_types ; - let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env - idrefs ?(subst=None,[]) tt - = - let fresh_id'' = fresh_id' father tt in - let aux' = aux computeinnertypes (Some fresh_id'') [] in - let string_of_sort_family = - function - Coq_sort Term.InProp -> "Prop" - | Coq_sort Term.InSet -> "Set" - | Coq_sort Term.InType -> "Type" - | CProp -> "CProp" - in - let string_of_sort t = - string_of_sort_family - (type_as_sort env evar_map t) - in - let ainnertypes,innertype,innersort,expected_available = - let {DoubleTypeInference.synthesized = synthesized; - DoubleTypeInference.expected = expected} = - if computeinnertypes then -try - Acic.CicHash.find terms_to_types tt -with e when Errors.noncritical e -> -(*CSC: Warning: it really happens, for example in Ring_theory!!! *) -Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false - else - (* We are already in an inner-type and Coscoy's double *) - (* type inference algorithm has not been applied. *) - (* We need to refresh the universes because we are doing *) - (* type inference on an already inferred type. *) - {DoubleTypeInference.synthesized = - Reductionops.nf_beta evar_map - (CPropRetyping.get_type_of env evar_map - ((* Termops.refresh_universes *) tt)) ; - DoubleTypeInference.expected = None} - in - let innersort = - let synthesized_innersort = - get_sort_family_of env evar_map synthesized - in - match expected with - None -> synthesized_innersort - | Some ty -> - let expected_innersort = - get_sort_family_of env evar_map ty - in - match expected_innersort, synthesized_innersort with - CProp, _ - | _, CProp -> CProp - | _, _ -> expected_innersort - in -(* Debugging only: -print_endline "PASSATO" ; flush stdout ; -*) - let ainnertypes,expected_available = - if computeinnertypes then - let annexpected,expected_available = - match expected with - None -> None,false - | Some expectedty' -> - Some (aux false (Some fresh_id'') [] env idrefs expectedty'), - true - in - Some - {annsynthesized = - aux false (Some fresh_id'') [] env idrefs synthesized ; - annexpected = annexpected - }, expected_available - else - None,false - in - ainnertypes,synthesized, string_of_sort_family innersort, - expected_available - in - let add_inner_type id = - match ainnertypes with - None -> () - | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes - in - - (* explicit_substitute_and_eta_expand_if_required h t t' *) - (* where [t] = [] and [tt] = [h]{[t']} ("{.}" denotes explicit *) - (* named substitution) or [tt] = (App [h]::[t]) (and [t'] = []) *) - (* check if [h] is a term that requires an explicit named *) - (* substitution and, in that case, uses the first arguments of *) - (* [t] as the actual arguments of the substitution. If there *) - (* are not enough parameters in the list [t], then eta-expansion *) - (* is performed. *) - let - explicit_substitute_and_eta_expand_if_required h t t' - compute_result_if_eta_expansion_not_required - = - let subst,residual_args,uninst_vars = - let variables,basedir = - try - let g = Globnames.global_of_constr h in - let sp = - match g with - Globnames.ConstructRef ((induri,_),_) - | Globnames.IndRef (induri,_) -> - Nametab.path_of_global (Globnames.IndRef (induri,0)) - | Globnames.VarRef id -> - (* Invariant: variables are never cooked in Coq *) - raise Not_found - | _ -> Nametab.path_of_global g - in - Dischargedhypsmap.get_discharged_hyps sp, - get_module_path_of_full_path sp - with Not_found -> - (* no explicit substitution *) - [], Libnames.dirpath_of_string "dummy" - in - (* returns a triple whose first element is *) - (* an explicit named substitution of "type" *) - (* (variable * argument) list, whose *) - (* second element is the list of residual *) - (* arguments and whose third argument is *) - (* the list of uninstantiated variables *) - let rec get_explicit_subst variables arguments = - match variables,arguments with - [],_ -> [],arguments,[] - | _,[] -> [],[],variables - | he1::tl1,he2::tl2 -> - let subst,extra_args,uninst = get_explicit_subst tl1 tl2 in - let (he1_sp, he1_id) = Libnames.repr_path he1 in - let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in - let he1'' = - String.concat "/" - (List.rev_map Id.to_string he1') ^ "/" - ^ (Id.to_string he1_id) ^ ".var" - in - (he1'',he2)::subst, extra_args, uninst - in - get_explicit_subst variables t' - in - let uninst_vars_length = List.length uninst_vars in - if uninst_vars_length > 0 then - (* Not enough arguments provided. We must eta-expand! *) - let un_args,_ = - Term.decompose_prod_n uninst_vars_length - (CPropRetyping.get_type_of env evar_map tt) - in - let eta_expanded = - let arguments = - List.map (Vars.lift uninst_vars_length) t @ - Termops.rel_list 0 uninst_vars_length - in - Unshare.unshare - (Term.lamn uninst_vars_length un_args - (Term.applistc h arguments)) - in - DoubleTypeInference.double_type_of env evar_map eta_expanded - None terms_to_types ; - Hashtbl.remove ids_to_inner_types fresh_id'' ; - aux' env idrefs eta_expanded - else - compute_result_if_eta_expansion_not_required subst residual_args - in - - (* Now that we have all the auxiliary functions we *) - (* can finally proceed with the main case analysis. *) - match Term.kind_of_term tt with - | Term.Proj _ -> assert false - | Term.Rel n -> - let id = - match List.nth (Environ.rel_context env) (n - 1) with - (Names.Name id,_,_) -> id - | (Names.Anonymous,_,_) -> Nameops.make_ident "_" None - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id) - | Term.Var id -> - let pvars = Termops.ids_of_named_context (Environ.named_context env) in - let pvars = List.map Id.to_string pvars in - let path = get_uri_of_var (Id.to_string id) pvars in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - Acic.AVar - (fresh_id'', path ^ "/" ^ (Id.to_string id) ^ ".var") - | Term.Evar (n,l) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - Acic.AEvar - (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | Term.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") - | Term.Sort s -> Acic.ASort (fresh_id'', s) - | Term.Cast (v,_, t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - Acic.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t) - | Term.Prod (n,s,t) -> - let n' = - match n with - Names.Anonymous -> Names.Anonymous - | _ -> - if not fake_dependent_products && Vars.noccurn 1 t then - Names.Anonymous - else - Names.Name - (Namegen.next_name_away n (Termops.ids_of_context env)) - in - Hashtbl.add ids_to_inner_sorts fresh_id'' - (string_of_sort innertype) ; - let sourcetype = CPropRetyping.get_type_of env evar_map s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - let new_passed_prods = - let father_is_prod = - match father with - None -> false - | Some father' -> - match - Term.kind_of_term (Hashtbl.find ids_to_terms father') - with - Term.Prod _ -> true - | _ -> false - in - (fresh_id'', n', aux' env idrefs s):: - (if father_is_prod then - passed_lambdas_or_prods_or_letins - else []) - in - let new_env = Environ.push_rel (n', None, s) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term t with - Term.Prod _ -> - aux computeinnertypes (Some fresh_id'') new_passed_prods - new_env new_idrefs t - | _ -> - Acic.AProds (new_passed_prods, aux' new_env new_idrefs t)) - | Term.Lambda (n,s,t) -> - let n' = - match n with - Names.Anonymous -> Names.Anonymous - | _ -> - Names.Name (Namegen.next_name_away n (Termops.ids_of_context env)) - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - let sourcetype = CPropRetyping.get_type_of env evar_map s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - let father_is_lambda = - match father with - None -> false - | Some father' -> - match - Term.kind_of_term (Hashtbl.find ids_to_terms father') - with - Term.Lambda _ -> true - | _ -> false - in - if is_a_Prop innersort && - ((not father_is_lambda) || expected_available) - then add_inner_type fresh_id'' ; - let new_passed_lambdas = - (fresh_id'',n', aux' env idrefs s):: - (if father_is_lambda then - passed_lambdas_or_prods_or_letins - else []) in - let new_env = Environ.push_rel (n', None, s) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term t with - Term.Lambda _ -> - aux computeinnertypes (Some fresh_id'') new_passed_lambdas - new_env new_idrefs t - | _ -> - let t' = aux' new_env new_idrefs t in - (* eta-expansion for explicit named substitutions *) - (* can create nested Lambdas. Here we perform the *) - (* flattening. *) - match t' with - Acic.ALambdas (lambdas, t'') -> - Acic.ALambdas (lambdas@new_passed_lambdas, t'') - | _ -> - Acic.ALambdas (new_passed_lambdas, t') - ) - | Term.LetIn (n,s,t,d) -> - let id = - match n with - Names.Anonymous -> Id.of_string "_X" - | Names.Name id -> id - in - let n' = - Names.Name (Namegen.next_ident_away id (Termops.ids_of_context env)) - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - let sourcesort = - get_sort_family_of env evar_map - (CPropRetyping.get_type_of env evar_map s) - in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort_family sourcesort) ; - let father_is_letin = - match father with - None -> false - | Some father' -> - match - Term.kind_of_term (Hashtbl.find ids_to_terms father') - with - Term.LetIn _ -> true - | _ -> false - in - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let new_passed_letins = - (fresh_id'',n', aux' env idrefs s):: - (if father_is_letin then - passed_lambdas_or_prods_or_letins - else []) in - let new_env = Environ.push_rel (n', Some s, t) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term d with - Term.LetIn _ -> - aux computeinnertypes (Some fresh_id'') new_passed_letins - new_env new_idrefs d - | _ -> Acic.ALetIns - (new_passed_letins, aux' new_env new_idrefs d)) - | Term.App (h,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let - compute_result_if_eta_expansion_not_required subst residual_args - = - let residual_args_not_empty = residual_args <> [] in - let h' = - if residual_args_not_empty then - aux' env idrefs ~subst:(None,subst) h - else - aux' env idrefs ~subst:(Some fresh_id'',subst) h - in - (* maybe all the arguments were used for the explicit *) - (* named substitution *) - if residual_args_not_empty then - Acic.AApp (fresh_id'', h'::residual_args) - else - h' - in - let t' = - Array.fold_right (fun x i -> (aux' env idrefs x)::i) t [] - in - explicit_substitute_and_eta_expand_if_required h - (Array.to_list t) t' - compute_result_if_eta_expansion_not_required - | Term.Const (kn,u) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - let compute_result_if_eta_expansion_not_required _ _ = - Acic.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn))) - in - let (_,subst') = subst in - explicit_substitute_and_eta_expand_if_required tt [] - (List.map snd subst') - compute_result_if_eta_expansion_not_required - | Term.Ind ((kn,i),u) -> - let compute_result_if_eta_expansion_not_required _ _ = - Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i) - in - let (_,subst') = subst in - explicit_substitute_and_eta_expand_if_required tt [] - (List.map snd subst') - compute_result_if_eta_expansion_not_required - | Term.Construct (((kn,i),j),u) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort && expected_available then - add_inner_type fresh_id'' ; - let compute_result_if_eta_expansion_not_required _ _ = - Acic.AConstruct - (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j) - in - let (_,subst') = subst in - explicit_substitute_and_eta_expand_if_required tt [] - (List.map snd subst') - compute_result_if_eta_expansion_not_required - | Term.Case ({Term.ci_ind=(kn,i)},ty,term,a) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let a' = - Array.fold_right (fun x i -> (aux' env idrefs x)::i) a [] - in - Acic.ACase - (fresh_id'', (uri_of_kernel_name (Inductive kn)), i, - aux' env idrefs ty, aux' env idrefs term, a') - | Term.Fix ((ai,i),(f,t,b)) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then add_inner_type fresh_id'' ; - let fresh_idrefs = - Array.init (Array.length t) (function _ -> gen_id seed) in - let new_idrefs = - (List.rev (Array.to_list fresh_idrefs)) @ idrefs - in - let f' = - let ids = ref (Termops.ids_of_context env) in - Array.map - (function - Names.Anonymous -> Errors.error "Anonymous fix function met" - | Names.Name id as n -> - let res = Names.Name (Namegen.next_name_away n !ids) in - ids := id::!ids ; - res - ) f - in - Acic.AFix (fresh_id'', i, - Array.fold_right - (fun (id,fi,ti,bi,ai) i -> - let fi' = - match fi with - Names.Name fi -> fi - | Names.Anonymous -> Errors.error "Anonymous fix function met" - in - (id, fi', ai, - aux' env idrefs ti, - aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i) - (Array.mapi - (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f' - ) [] - ) - | Term.CoFix (i,(f,t,b)) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then add_inner_type fresh_id'' ; - let fresh_idrefs = - Array.init (Array.length t) (function _ -> gen_id seed) in - let new_idrefs = - (List.rev (Array.to_list fresh_idrefs)) @ idrefs - in - let f' = - let ids = ref (Termops.ids_of_context env) in - Array.map - (function - Names.Anonymous -> Errors.error "Anonymous fix function met" - | Names.Name id as n -> - let res = Names.Name (Namegen.next_name_away n !ids) in - ids := id::!ids ; - res - ) f - in - Acic.ACoFix (fresh_id'', i, - Array.fold_right - (fun (id,fi,ti,bi) i -> - let fi' = - match fi with - Names.Name fi -> fi - | Names.Anonymous -> Errors.error "Anonymous fix function met" - in - (id, fi', - aux' env idrefs ti, - aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i) - (Array.mapi - (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f' - ) [] - ) - in - aux computeinnertypes None [] env idrefs t -;; - -(* Obsolete [HH 1/2009] -let acic_of_cic_context metasenv context t = - let ids_to_terms = Hashtbl.create 503 in - let constr_to_ids = Acic.CicHash.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let seed = ref 0 in - acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types metasenv context t, - ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types -;; -*) - -let acic_object_of_cic_object sigma obj = - let ids_to_terms = Hashtbl.create 503 in - let constr_to_ids = Acic.CicHash.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let ids_to_conjectures = Hashtbl.create 11 in - let ids_to_hypotheses = Hashtbl.create 127 in - let hypotheses_seed = ref 0 in - let conjectures_seed = ref 0 in - let seed = ref 0 in - let acic_term_of_cic_term_context' = - acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types in -(*CSC: is this the right env to use? Hhmmm. There is a problem: in *) -(*CSC: Global.env () the object we are exporting is already defined, *) -(*CSC: either in the environment or in the named context (in the case *) -(*CSC: of variables. Is this a problem? *) - let env = Global.env () in - let acic_term_of_cic_term' ?fake_dependent_products = - acic_term_of_cic_term_context' ?fake_dependent_products env [] sigma in -(*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *) -(*CSC: a modified version of the already existent fresh_id function *) - let fresh_id () = - let res = "i" ^ string_of_int !seed in - incr seed ; - res - in - let aobj = - match obj with - Acic.Constant (id,bo,ty,params) -> - let abo = - match bo with - None -> None - | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty)) - in - let aty = acic_term_of_cic_term' ty None in - Acic.AConstant (fresh_id (),id,abo,aty,params) - | Acic.Variable (id,bo,ty,params) -> - let abo = - match bo with - Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) - | None -> None - in - let aty = acic_term_of_cic_term' ty None in - Acic.AVariable (fresh_id (),id,abo,aty,params) - | Acic.CurrentProof (id,conjectures,bo,ty) -> - let aconjectures = - List.map - (function (i,canonical_context,term) as conjecture -> - let cid = "c" ^ string_of_int !conjectures_seed in - Hashtbl.add ids_to_conjectures cid conjecture ; - incr conjectures_seed ; - let canonical_env,idrefs',acanonical_context = - let rec aux env idrefs = - function - [] -> env,idrefs,[] - | ((n,decl_or_def) as hyp)::tl -> - let hid = "h" ^ string_of_int !hypotheses_seed in - let new_idrefs = hid::idrefs in - Hashtbl.add ids_to_hypotheses hid hyp ; - incr hypotheses_seed ; - match decl_or_def with - Acic.Decl t -> - let final_env,final_idrefs,atl = - aux (Environ.push_rel (Names.Name n,None,t) env) - new_idrefs tl - in - let at = - acic_term_of_cic_term_context' env idrefs sigma t None - in - final_env,final_idrefs,(hid,(n,Acic.Decl at))::atl - | Acic.Def (t,ty) -> - let final_env,final_idrefs,atl = - aux - (Environ.push_rel (Names.Name n,Some t,ty) env) - new_idrefs tl - in - let at = - acic_term_of_cic_term_context' env idrefs sigma t None - in - let dummy_never_used = - let s = "dummy_never_used" in - Acic.ARel (s,99,s,Id.of_string s) - in - final_env,final_idrefs, - (hid,(n,Acic.Def (at,dummy_never_used)))::atl - in - aux env [] canonical_context - in - let aterm = - acic_term_of_cic_term_context' canonical_env idrefs' sigma term - None - in - (cid,i,List.rev acanonical_context,aterm) - ) conjectures in - let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in - let aty = acic_term_of_cic_term_context' env [] sigma ty None in - Acic.ACurrentProof (fresh_id (),id,aconjectures,abo,aty) - | Acic.InductiveDefinition (tys,params,paramsno) -> - let env' = - List.fold_right - (fun (name,_,arity,_) env -> - Environ.push_rel (Names.Name name, None, arity) env - ) (List.rev tys) env in - let idrefs = List.map (function _ -> gen_id seed) tys in - let atys = - List.map2 - (fun id (name,inductive,ty,cons) -> - let acons = - List.map - (function (name,ty) -> - (name, - acic_term_of_cic_term_context' ~fake_dependent_products:true - env' idrefs Evd.empty ty None) - ) cons - in - let aty = - acic_term_of_cic_term' ~fake_dependent_products:true ty None - in - (id,name,inductive,aty,acons) - ) (List.rev idrefs) tys - in - Acic.AInductiveDefinition (fresh_id (),atys,params,paramsno) - in - aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses -;; diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml deleted file mode 100644 index c8717e008..000000000 --- a/plugins/xml/doubleTypeInference.ml +++ /dev/null @@ -1,266 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s } - | _ -> None (* None means the CProp constant *) -;; - -let double_type_of env sigma cstr expectedty subterms_to_types = - (*CSC: the code is inefficient because judgments are created just to be *) - (*CSC: destroyed using Environ.j_type. Moreover I am pretty sure that the *) - (*CSC: functions used do checks that we do not need *) - let rec execute env sigma cstr expectedty = - let module T = Term in - let module V = Vars in - let module E = Environ in - (* the type part is the synthesized type *) - let judgement = - match T.kind_of_term cstr with - T.Meta n -> - Errors.error - "DoubleTypeInference.double_type_of: found a non-instanciated goal" - | T.Proj _ -> assert false - | T.Evar ((n,l) as ev) -> - let ty = Unshare.unshare (Evd.existential_type sigma ev) in - let jty = execute env sigma ty None in - let jty = assumption_of_judgment env sigma jty in - let evar_context = - E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in - let rec iter actual_args evar_context = - match actual_args,evar_context with - [],[] -> () - | he1::tl1,(n,_,ty)::tl2 -> - (* for side-effects *) - let _ = execute env sigma he1 (Some ty) in - let tl2' = - List.map - (function (m,bo,ty) -> - (* Warning: the substitution should be performed also on bo *) - (* This is not done since bo is not used later yet *) - (m,bo,Unshare.unshare (V.replace_vars [n,he1] ty)) - ) tl2 - in - iter tl1 tl2' - | _,_ -> assert false - in - (* for side effects only *) - iter (List.rev (Array.to_list l)) (List.rev evar_context) ; - E.make_judge cstr jty - - | T.Rel n -> - Typeops.judge_of_relative env n - - | T.Var id -> - Typeops.judge_of_variable env id - - | T.Const c -> - E.make_judge cstr (fst (Typeops.type_of_constant env c)) - - | T.Ind ind -> - E.make_judge cstr (Inductiveops.type_of_inductive env ind) - - | T.Construct cstruct -> - E.make_judge cstr (Inductiveops.type_of_constructor env cstruct) - - | T.Case (ci,p,c,lf) -> - let expectedtype = - Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in - let cj = execute env sigma c (Some expectedtype) in - let pj = execute env sigma p None in - let (expectedtypes,_) = - let indspec = Inductive.find_rectype env cj.Environ.uj_type in - Inductive.type_case_branches env indspec pj cj.Environ.uj_val - in - let lfj = - execute_array env sigma lf - (Array.map (function x -> Some x) expectedtypes) in - Typeops.judge_of_case env ci pj cj lfj - - | T.Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let fix = (vni,recdef') in - E.make_judge (T.mkFix fix) tys.(i) - - | T.CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let cofix = (i,recdef') in - E.make_judge (T.mkCoFix cofix) tys.(i) - - | T.Sort (T.Prop c) -> - Typeops.judge_of_prop_contents c - - | T.Sort (T.Type u) -> -(*CSC: In case of need, I refresh the universe. But exportation of the *) -(*CSC: right universe level information is destroyed. It must be changed *) -(*CSC: again once Judicael will introduce his non-bugged algebraic *) -(*CSC: universes. *) -(try - (*FIXME*) (Typeops.judge_of_type u) - with _ -> (* Successor of a non universe-variable universe anomaly *) - Pp.msg_warning (Pp.str "Universe refresh performed!!!"); - (*FIXME*) (Typeops.judge_of_type (Universes.new_univ Names.empty_dirpath)) -) - - | T.App (f,args) -> - let expected_head = - Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in - let j = execute env sigma f (Some expected_head) in - let expected_args = - let rec aux typ = - function - [] -> [] - | hj::restjl -> - match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with - T.Prod (_,c1,c2) -> - (Some (Reductionops.nf_beta sigma c1)) :: - (aux (V.subst1 hj c2) restjl) - | _ -> assert false - in - Array.of_list (aux j.Environ.uj_type (Array.to_list args)) - in - let jl = execute_array env sigma args expected_args in - let j = Typeops.judge_of_apply env j jl in - j - - | T.Lambda (name,c1,c2) -> - let j = execute env sigma c1 None in - let var = type_judgment env sigma j in - let env1 = E.push_rel (name,None,var.E.utj_val) env in - let expectedc2type = - match expectedty with - None -> None - | Some ety -> - match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with - T.Prod (_,_,expected_target_type) -> - Some (Reductionops.nf_beta sigma expected_target_type) - | _ -> assert false - in - let j' = execute env1 sigma c2 expectedc2type in - Typeops.judge_of_abstraction env1 name var j' - - | T.Prod (name,c1,c2) -> - let j = execute env sigma c1 None in - let varj = type_judgment env sigma j in - let env1 = E.push_rel (name,None,varj.E.utj_val) env in - let j' = execute env1 sigma c2 None in - (match type_judgment_cprop env1 sigma j' with - Some varj' -> Typeops.judge_of_product env name varj varj' - | None -> - (* CProp found *) - { Environ.uj_val = T.mkProd (name, j.Environ.uj_val, j'.Environ.uj_val); - Environ.uj_type = T.mkConst cprop }) - - | T.LetIn (name,c1,c2,c3) -> -(*CSC: What are the right expected types for the source and *) -(*CSC: target of a LetIn? None used. *) - let j1 = execute env sigma c1 None in - let j2 = execute env sigma c2 None in - let j2 = type_judgment env sigma j2 in - let env1 = - E.push_rel (name,Some j1.E.uj_val,j2.E.utj_val) env - in - let j3 = execute env1 sigma c3 None in - Typeops.judge_of_letin env name j1 j2 j3 - - | T.Cast (c,k,t) -> - let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in - let tj = execute env sigma t None in - let tj = type_judgment env sigma tj in - let j = Typeops.judge_of_cast env cj k tj in - j - in - let synthesized = E.j_type judgement in - let synthesized' = Reductionops.nf_beta sigma synthesized in - let types,res = - match expectedty with - None -> - (* No expected type *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when Term.eq_constr synthesized' ty -> - (* The expected type is synthactically equal to the *) - (* synthesized type. Let's forget it. *) - (* Note: since eq_constr is up to casts, it is better *) - (* to keep the expected type, since it can bears casts *) - (* that change the innersort to CProp *) - {synthesized = ty ; expected = None}, ty - | Some expectedty' -> - {synthesized = synthesized' ; expected = Some expectedty'}, - expectedty' - in -(*CSC: debugging stuff to be removed *) -if Acic.CicHash.mem subterms_to_types cstr then - Pp.msg_warning (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)); - Acic.CicHash.add subterms_to_types cstr types ; - E.make_judge cstr res - - - and execute_recdef env sigma (names,lar,vdef) = - let length = Array.length lar in - let larj = - execute_array env sigma lar (Array.make length None) in - let lara = Array.map (assumption_of_judgment env sigma) larj in - let env1 = Environ.push_rec_types (names,lara,vdef) env in - let expectedtypes = - Array.map (function i -> Some (Vars.lift length i)) lar - in - let vdefj = execute_array env1 sigma vdef expectedtypes in - let vdefv = Array.map Environ.j_val vdefj in - (names,lara,vdefv) - - and execute_array env sigma v expectedtypes = - let jl = - execute_list env sigma (Array.to_list v) (Array.to_list expectedtypes) - in - Array.of_list jl - - and execute_list env sigma = - List.map2 (execute env sigma) - -in - ignore (execute env sigma cstr expectedty) -;; diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli deleted file mode 100644 index 5c00bdc67..000000000 --- a/plugins/xml/doubleTypeInference.mli +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Evd.evar_map -> Term.constr -> Term.constr - -val double_type_of : - Environ.env -> Evd.evar_map -> Term.constr -> Term.constr option -> - types Acic.CicHash.t -> unit diff --git a/plugins/xml/theoryobject.dtd b/plugins/xml/theoryobject.dtd deleted file mode 100644 index 953fe0092..000000000 --- a/plugins/xml/theoryobject.dtd +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml deleted file mode 100644 index c854427d2..000000000 --- a/plugins/xml/unshare.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* false) t = - let obj = Obj.repr t in - let rec aux obj = - if already_unshared (Obj.obj obj) then - obj - else - (if Obj.is_int obj then - obj - else if Obj.is_block obj then - begin - let tag = Obj.tag obj in - if tag < Obj.no_scan_tag then - begin - let size = Obj.size obj in - let new_obj = Obj.new_block 0 size in - Obj.set_tag new_obj tag ; - for i = 0 to size - 1 do - Obj.set_field new_obj i (aux (Obj.field obj i)) - done ; - new_obj - end - else if tag = Obj.string_tag then - obj - else - raise CanNotUnshare - end - else - raise CanNotUnshare - ) - in - Obj.obj (aux obj) -;; diff --git a/plugins/xml/unshare.mli b/plugins/xml/unshare.mli deleted file mode 100644 index cace2de6f..000000000 --- a/plugins/xml/unshare.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool) -> 'a -> 'a diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4 deleted file mode 100644 index c2523755b..000000000 --- a/plugins/xml/xml.ml4 +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] -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") ; - pp_r m s - | [< >] -> () - and print_spaces m = - for _i = 1 to m do fprint_string " " done - and fprint_string str = - output_string channel str - in - pp_r 0 strm -;; - - -let pp strm fn = - match fn with - Some filename -> - let filename = filename ^ ".xml" in - let ch = open_out filename in - pp_ch strm ch; - close_out ch ; - print_string ("\nWriting on file \"" ^ filename ^ "\" was successful\n"); - flush stdout - | None -> - pp_ch strm stdout -;; - diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli deleted file mode 100644 index 0b6d51985..000000000 --- a/plugins/xml/xml.mli +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (string * string) list -> token Stream.t -val xml_nempty : - string -> (string * string) list -> token Stream.t -> token Stream.t -val xml_cdata : string -> token Stream.t - -val pp_ch : token Stream.t -> out_channel -> unit - -(* The pretty printer for streams of token *) -(* Usage: *) -(* pp tokens None pretty prints the output on stdout *) -(* pp tokens (Some filename) pretty prints the output on the file filename *) -val pp : token Stream.t -> string option -> unit diff --git a/plugins/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib deleted file mode 100644 index 27b0ef36f..000000000 --- a/plugins/xml/xml_plugin.mllib +++ /dev/null @@ -1,10 +0,0 @@ -Unshare -Xml -Acic -DoubleTypeInference -Cic2acic -Acic2Xml -Xmlcommand -Xmlentries -Cic2Xml -Xml_plugin_mod diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml deleted file mode 100644 index d65e6f317..000000000 --- a/plugins/xml/xmlcommand.ml +++ /dev/null @@ -1,536 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] - | (id,he)::tl -> - let ids' = id::ids in - let ids'' = - "cic:/" ^ - String.concat "/" (List.rev_map Id.to_string ids') in - let he' = - ids'', List.rev (List.filter (function x -> String.List.mem x hyps) he) - in - let tl' = aux ids' tl in - match he' with - _,[] -> tl' - | _,_ -> he'::tl' - in - let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - aux (DirPath.repr modulepath) (List.rev pvars) -;; - -(* The computation is very inefficient, but we can't do anything *) -(* better unless this function is reimplemented in the Declare *) -(* module. *) -let search_variables () = - let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - let rec aux = - function - [] -> [] - | he::tl as modules -> - let one_section_variables = - let dirpath = DirPath.make (modules @ DirPath.repr modulepath) in - let t = List.map Id.to_string (Decls.last_section_hyps dirpath) in - [he,t] - in - one_section_variables @ aux tl - in - aux - (Cic2acic.remove_module_dirpath_from_dirpath - ~basedir:modulepath cwd) -;; - -(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *) - -let rec join_dirs cwd = - function - [] -> cwd - | he::tail -> - (try - Unix.mkdir cwd 0o775 - with e when Errors.noncritical e -> () (* ignore the errors on mkdir *) - ) ; - let newcwd = cwd ^ "/" ^ he in - join_dirs newcwd tail -;; - -let filename_of_path xml_library_root tag = - match xml_library_root with - None -> None (* stdout *) - | Some xml_library_root' -> - let tokens = Cic2acic.token_list_of_kernel_name tag in - Some (join_dirs xml_library_root' tokens) -;; - -let body_filename_of_filename = - function - Some f -> Some (f ^ ".body") - | None -> None -;; - -let types_filename_of_filename = - function - Some f -> Some (f ^ ".types") - | None -> None -;; - -let theory_filename xml_library_root = - match xml_library_root with - None -> None (* stdout *) - | Some xml_library_root' -> - let toks = List.map Id.to_string (DirPath.repr (Lib.library_dp ())) in - (* theory from A/B/C/F.v goes into A/B/C/F.theory *) - let alltoks = List.rev toks in - Some (join_dirs xml_library_root' alltoks ^ ".theory") - -let print_object uri obj sigma filename = - (* function to pretty print and compress an XML file *) -(*CSC: Unix.system "gzip ..." is an horrible non-portable solution. *) - let pp xml filename = - Xml.pp xml filename ; - match filename with - None -> () - | Some fn -> - let fn' = - let rec escape s n = - try - let p = String.index_from s n '\'' in - String.sub s n (p - n) ^ "\\'" ^ escape s (p+1) - with Not_found -> String.sub s n (String.length s - n) - in - escape fn 0 - in - ignore (Unix.system ("gzip " ^ fn' ^ ".xml")) - in - let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) = - Cic2acic.acic_object_of_cic_object sigma obj in - let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in - let xmltypes = - Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in - pp xml filename ; - begin - match xml' with - None -> () - | Some xml' -> pp xml' (body_filename_of_filename filename) - end ; - pp xmltypes (types_filename_of_filename filename) -;; - -let string_list_of_named_context_list = - List.map - (function (n,_,_) -> Id.to_string n) -;; - -(* Function to collect the variables that occur in a term. *) -(* Used only for variables (since for constants and mutual *) -(* inductive types this information is already available. *) -let find_hyps t = - let rec aux l t = - match Term.kind_of_term t with - Term.Var id when not (Id.List.mem id l) -> - let (_,bo,ty) = Global.lookup_named id in - let boids = - match bo with - Some bo' -> aux l bo' - | None -> l - in - id::(aux boids ty) - | Term.Var _ - | Term.Rel _ - | Term.Meta _ - | Term.Evar _ - | Term.Sort _ -> l - | Term.Proj _ -> ignore(Errors.todo "Proj in find_hyps"); assert false - | Term.Cast (te,_, ty) -> aux (aux l te) ty - | Term.Prod (_,s,t) -> aux (aux l s) t - | Term.Lambda (_,s,t) -> aux (aux l s) t - | Term.LetIn (_,s,_,t) -> aux (aux l s) t - | Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl - | Term.Const (con, _) -> - let hyps = (Global.lookup_constant con).Declarations.const_hyps in - map_and_filter l hyps @ l - | Term.Ind (ind,_) - | Term.Construct ((ind,_),_) -> - let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in - map_and_filter l hyps @ l - | Term.Case (_,t1,t2,b) -> - Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b - | Term.Fix (_,(_,tys,bodies)) - | Term.CoFix (_,(_,tys,bodies)) -> - let r = Array.fold_left (fun i x -> aux i x) l tys in - Array.fold_left (fun i x -> aux i x) r bodies - and map_and_filter l = - function - [] -> [] - | (n,_,_)::tl when not (Id.List.mem n l) -> n::(map_and_filter l tl) - | _::tl -> map_and_filter l tl - in - aux [] t -;; - -(* Functions to construct an object *) - -let mk_variable_obj id body typ = - let hyps,unsharedbody = - match body with - None -> [],None - | Some bo -> find_hyps bo, Some (Unshare.unshare bo) - in - let hyps' = find_hyps typ @ hyps in - let hyps'' = List.map Id.to_string hyps' in - let variables = search_variables () in - let params = filter_params variables hyps'' in - Acic.Variable - (Id.to_string id, unsharedbody, Unshare.unshare typ, params) -;; - - -let mk_constant_obj id bo ty variables hyps = - let hyps = string_list_of_named_context_list hyps in - let ty = Unshare.unshare ty in - let params = filter_params variables hyps in - match bo with - None -> - Acic.Constant (Id.to_string id,None,ty,params) - | Some c -> - Acic.Constant - (Id.to_string id, Some (Unshare.unshare c), ty,params) -;; - -let mk_inductive_obj sp mib packs variables nparams hyps finite = - let hyps = string_list_of_named_context_list hyps in - let params = filter_params variables hyps in -(* let nparams = extract_nparams packs in *) - let tys = - let tyno = ref (Array.length packs) in - Array.fold_right - (fun p i -> - decr tyno ; - let {Declarations.mind_consnames=consnames ; - Declarations.mind_typename=typename } = p - in - let inst = Univ.UContext.instance mib.Declarations.mind_universes in - let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),inst) in - let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),inst) in - let cons = - (Array.fold_right (fun (name,lc) i -> (name,lc)::i) - (Array.mapi - (fun j x ->(x,Unshare.unshare lc.(j))) consnames) - [] - ) - in - (typename,finite,Unshare.unshare arity,cons)::i - ) packs [] - in - Acic.InductiveDefinition (tys,params,nparams) -;; - -(* The current channel for .theory files *) -let theory_buffer = Buffer.create 4000;; - -let theory_output_string ?(do_not_quote = false) s = - (* prepare for coqdoc post-processing *) - let s = if do_not_quote then s else "(** #"^s^"\n#*)\n" in - print_if_verbose s; - Buffer.add_string theory_buffer s -;; - -let kind_of_inductive isrecord kn = - "DEFINITION", - if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite <> Decl_kinds.CoFinite - then begin - match isrecord with - | Declare.KernelSilent -> "Record" - | _ -> "Inductive" - end - else "CoInductive" -;; - -let kind_of_variable id = - match Decls.variable_kind id with - | IsAssumption Definitional -> "VARIABLE","Assumption" - | IsAssumption Logical -> "VARIABLE","Hypothesis" - | IsAssumption Conjectural -> "VARIABLE","Conjecture" - | IsDefinition Definition -> "VARIABLE","LocalDefinition" - | IsProof _ -> "VARIABLE","LocalFact" - | _ -> Errors.anomaly (Pp.str "Unsupported variable kind") -;; - -let kind_of_constant kn = - match Decls.constant_kind kn with - | IsAssumption Definitional -> "AXIOM","Declaration" - | IsAssumption Logical -> "AXIOM","Axiom" - | IsAssumption Conjectural -> - Pp.msg_warning (Pp.str "Conjecture not supported in dtd (used Declaration instead)"); - "AXIOM","Declaration" - | IsDefinition Definition -> "DEFINITION","Definition" - | IsDefinition Example -> - Pp.msg_warning (Pp.str "Example not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition Coercion -> - Pp.msg_warning (Pp.str "Coercion not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition SubClass -> - Pp.msg_warning (Pp.str "SubClass not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition CanonicalStructure -> - Pp.msg_warning (Pp.str "CanonicalStructure not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition Fixpoint -> - Pp.msg_warning (Pp.str "Fixpoint not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition CoFixpoint -> - Pp.msg_warning (Pp.str "CoFixpoint not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition Scheme -> - Pp.msg_warning (Pp.str "Scheme not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition StructureComponent -> - Pp.msg_warning (Pp.str "StructureComponent not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition IdentityCoercion -> - Pp.msg_warning (Pp.str "IdentityCoercion not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition Instance -> - Pp.msg_warning (Pp.str "Instance not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsDefinition Method -> - Pp.msg_warning (Pp.str "Method not supported in dtd (used Definition instead)"); - "DEFINITION","Definition" - | IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) -> - "THEOREM",Kindops.string_of_theorem_kind thm - | IsProof _ -> - Pp.msg_warning (Pp.str "Unsupported theorem kind (used Theorem instead)"); - "THEOREM",Kindops.string_of_theorem_kind Theorem -;; - -let kind_of_global r = - match r with - | Globnames.IndRef kn | Globnames.ConstructRef (kn,_) -> - let isrecord = - try let _ = Recordops.lookup_projections kn in Declare.KernelSilent - with Not_found -> Declare.KernelVerbose in - kind_of_inductive isrecord (fst kn) - | Globnames.VarRef id -> kind_of_variable id - | Globnames.ConstRef kn -> kind_of_constant kn -;; - -let print_object_kind uri (xmltag,variation) = - let s = - Printf.sprintf "\n" xmltag uri variation - in - theory_output_string s -;; - -(* print id dest *) -(* where sp is the qualified identifier (section path) of a *) -(* definition/theorem, variable or inductive definition *) -(* and dest is either None (for stdout) or (Some filename) *) -(* pretty prints via Xml.pp the object whose identifier is id on dest *) -(* Note: it is printed only (and directly) the most cooked available *) -(* form of the definition (all the parameters are *) -(* lambda-abstracted, but the object can still refer to variables) *) -let print internal glob_ref kind xml_library_root = - (* Variables are the identifiers of the variables in scope *) - let variables = search_variables () in - let tag,obj = - match glob_ref with - Globnames.VarRef id -> - (* this kn is fake since it is not provided by Coq *) - let kn = Lib.make_kn id in - let (_,body,typ) = Global.lookup_named id in - Cic2acic.Variable kn,mk_variable_obj id body typ - | Globnames.ConstRef kn -> - let id = Label.to_id (Names.con_label kn) in - let cb = Global.lookup_constant kn in - let val0 = Declareops.body_of_constant cb in - let typ = cb.Declarations.const_type in - let hyps = cb.Declarations.const_hyps in - let typ = Typeops.type_of_constant_type (Global.env()) typ in - Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps - | Globnames.IndRef (kn,_) -> - let mib = Global.lookup_mind kn in - let {Declarations.mind_nparams=nparams; - Declarations.mind_packets=packs ; - Declarations.mind_hyps=hyps; - Declarations.mind_finite=finite} = mib in - Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps (finite<>Decl_kinds.CoFinite) - | Globnames.ConstructRef _ -> - Errors.error ("a single constructor cannot be printed in XML") - in - let fn = filename_of_path xml_library_root tag in - let uri = Cic2acic.uri_of_kernel_name tag in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri kind); - print_object uri obj Evd.empty fn -;; - -let print_ref qid fn = - let ref = Nametab.global qid in - print Declare.UserVerbose ref (kind_of_global ref) fn - -(* show dest *) -(* where dest is either None (for stdout) or (Some filename) *) -(* pretty prints via Xml.pp the proof in progress on dest *) -let show_pftreestate internal fn (kind,pftst) id = - if true then - Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.") - -let show fn = - let pftst = Pfedit.get_pftreestate () in - let (id,kind,_) = Pfedit.current_proof_statement () in - show_pftreestate false fn (kind,pftst) id -;; - - -(* Let's register the callbacks *) -let xml_library_root = - try - Some (Sys.getenv "COQ_XML_LIBRARY_ROOT") - with Not_found -> None -;; - -let proof_to_export = ref None (* holds the proof-tree to export *) -;; - -let _ = - Hook.set Declare.xml_declare_variable - (function (sp,kn) -> - let id = Libnames.basename sp in - print Declare.UserVerbose (Globnames.VarRef id) (kind_of_variable id) xml_library_root ; - proof_to_export := None) -;; - -let _ = - Hook.set Declare.xml_declare_constant - (function (internal,kn) -> - match !proof_to_export with - None -> - print internal (Globnames.ConstRef kn) (kind_of_constant kn) - xml_library_root - | Some pftreestate -> - (* It is a proof. Let's export it starting from the proof-tree *) - (* I saved in the Pfedit.set_xml_cook_proof callback. *) - let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in - show_pftreestate internal fn pftreestate - (Label.to_id (Names.con_label kn)) ; - proof_to_export := None) -;; - -let _ = - Hook.set Declare.xml_declare_inductive - (function (isrecord,(sp,kn)) -> - print Declare.UserVerbose (Globnames.IndRef (Names.mind_of_kn kn,0)) - (kind_of_inductive isrecord (Names.mind_of_kn kn)) - xml_library_root) -;; - -let _ = - Hook.set Vernac.xml_start_library - (function () -> - Buffer.reset theory_buffer; - theory_output_string "\n"; - theory_output_string ("\n" ^ - "\n" ^ - "\n\n" ^ - "%xhtml-lat1.ent;\n" ^ - "%xhtml-special.ent;\n" ^ - "%xhtml-symbol.ent;\n" ^ - "]>\n\n"); - theory_output_string "\n"; - theory_output_string "\n\n") -;; - -let _ = - Hook.set Vernac.xml_end_library - (function () -> - theory_output_string "\n\n"; - let ofn = theory_filename xml_library_root in - begin - match ofn with - None -> - Buffer.output_buffer stdout theory_buffer ; - | Some fn -> - let ch = open_out (fn ^ ".v") in - Buffer.output_buffer ch theory_buffer ; - close_out ch; - (* dummy glob file *) - let ch = open_out (fn ^ ".glob") in - close_out ch - end ; - Option.iter - (fun fn -> - let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in - let options = " --html -s --body-only --no-index --latin1 --raw-comments" in - let command cmd = - if Sys.command cmd <> 0 then - Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\"")) - in - command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); - command ("rm "^fn^".v "^fn^".glob"); - print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n")) - ofn) -;; - -let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:true) ;; - -let uri_of_dirpath dir = - "/" ^ String.concat "/" - (List.rev_map Id.to_string (DirPath.repr dir)) -;; - -let _ = - Hook.set Lib.xml_open_section - (fun _ -> - let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in - theory_output_string ("")) -;; - -let _ = - Hook.set Lib.xml_close_section - (fun _ -> theory_output_string "") -;; - -let _ = - Hook.set Library.xml_require - (fun d -> theory_output_string - (Printf.sprintf "Require %s.
" - (uri_of_dirpath d) (DirPath.to_string d))) -;; diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli deleted file mode 100644 index 8e6254efc..000000000 --- a/plugins/xml/xmlcommand.mli +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string option -> unit - -(* show dest *) -(* where dest is either None (for stdout) or (Some filename) *) -(* pretty prints via Xml.pp the proof in progress on dest *) -val show : string option -> unit diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 deleted file mode 100644 index 8cf3a0bdc..000000000 --- a/plugins/xml/xmlentries.ml4 +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ Some fn ] -| [ ] -> [ None ] -END - -(* Print XML and Show XML *) - -VERNAC COMMAND EXTEND Xml CLASSIFIED AS QUERY -| [ "Print" "XML" filename(fn) global(qid) ] -> [ Xmlcommand.print_ref qid fn ] - -| [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] -END diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 890e0d585..b6b8c9c2e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -985,9 +985,6 @@ and pr_tacarg = function | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacPretype c -> str "type_term" ++ pr.pr_constr c | TacNumgoals -> str "numgoals" - | TacExternal (_,com,req,la) -> - str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ - spc() ++ prlist_with_sep spc pr_tacarg la | (TacCall _|Tacexp _ | TacGeneric _) as a -> str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9d1a9eeaf..69798a6d2 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -633,7 +633,7 @@ and intern_tactic_seq onlytac ist = function and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with - | TacCall _ | TacExternal _ | Reference _ + | TacCall _ | Reference _ | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> @@ -664,8 +664,6 @@ and intern_tacarg strict onlytac ist = function TacCall (loc, intern_applied_tactic_reference ist f, List.map (intern_tacarg !strict_check false ist) l) - | TacExternal (loc,com,req,la) -> - TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) | TacPretype c -> TacPretype (intern_constr ist c) | TacNumgoals -> TacNumgoals diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c3869ec29..85d0ac4cd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -221,23 +221,6 @@ let coerce_to_tactic loc id v = | _ -> fail () else fail () -(* External tactics *) -let print_xml_term = ref (fun _ -> failwith "print_xml_term unset") -let declare_xml_printer f = print_xml_term := f - -let internalise_tacarg ch = G_xml.parse_tactic_arg ch - -let extern_tacarg ch env sigma v = match Value.to_constr v with -| None -> - error "Only externing of closed terms is implemented." -| Some c -> !print_xml_term ch env sigma c - -let extern_request ch req gl la = - output_string ch "\n"; - List.iter (pf_apply (extern_tacarg ch) gl) la; - output_string ch "\n" - let value_of_ident id = in_gen (topwit wit_intro_pattern) (Loc.ghost, IntroNaming (IntroIdentifier id)) @@ -1317,10 +1300,6 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = interp_ltac_reference loc true ist f >>= fun fv -> Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs - | TacExternal (loc,com,req,la) -> - let (>>=) = Ftactic.bind in - Ftactic.List.map (fun a -> interp_tacarg ist a) la >>= fun la_interp -> - interp_external loc ist com req la_interp | TacFreshId l -> Ftactic.enter begin fun gl -> let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in @@ -1522,13 +1501,6 @@ and interp_match_goal ist lz lr lmr = interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr) end -and interp_external loc ist com req la = - Ftactic.nf_enter begin fun gl -> - let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in - let g ch = internalise_tacarg ch in - interp_tacarg ist (System.connect f g com) - end - (* Interprets extended tactic generic arguments *) (* spiwack: interp_genarg has an argument [concl] for the case of "casted open constr". And [gl] for [Geninterp]. I haven't changed diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 8c639cb18..54e604fe4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -103,10 +103,6 @@ val interp : raw_tactic_expr -> unit Proofview.tactic val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic -(** Declare the xml printer *) -val declare_xml_printer : - (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit - (** Internals that can be useful for syntax extensions. *) val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t Loc.located -> 'a diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index ab96fe674..b1d03f86e 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -258,8 +258,6 @@ and subst_tacarg subst = function | MetaIdArg (_loc,_,_) -> assert false | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) - | TacExternal (_loc,com,req,la) -> - TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) | TacNumgoals -> TacNumgoals diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 01383365e..5d88fa5b7 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -22,6 +22,5 @@ Declare ML Module "decl_mode_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". -Declare ML Module "xml_plugin". (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_admitted" "_subproof" "Private_". -- cgit v1.2.3