diff options
| author | herbelin | 2002-11-05 16:59:25 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-05 16:59:25 +0000 |
| commit | 9f2ec7fc9f1ed08be8bc5a09d352951073a69633 (patch) | |
| tree | c5f06d5b112ed9731f71c98910d6f69852b3de5b | |
| parent | 1f95f087d79d6c2c79012921ce68553caf20b090 (diff) | |
Intégration de la branche mowgli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3213 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/xml/acic.ml | 94 | ||||
| -rw-r--r-- | contrib/xml/acic2Xml.ml4 | 371 | ||||
| -rw-r--r-- | contrib/xml/cic2acic.ml | 723 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 243 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.mli | 5 | ||||
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 154 | ||||
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 190 | ||||
| -rw-r--r-- | contrib/xml/unshare.ml | 56 | ||||
| -rw-r--r-- | contrib/xml/unshare.mli | 25 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 823 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.mli | 2 | ||||
| -rw-r--r-- | contrib/xml/xmlentries.ml4 | 2 |
12 files changed, 2688 insertions, 0 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml new file mode 100644 index 0000000000..693b7cb3c8 --- /dev/null +++ b/contrib/xml/acic.ml @@ -0,0 +1,94 @@ +open Names +open Term + +(* Maps fron \em{unshared} [constr] to ['a]. *) +module CicHash = + Hashtbl.Make + (struct + type t = Term.constr + let equal = (==) + let hash = Hashtbl.hash + end) +;; + +type id = string (* the type of the (annotated) node identifiers *) +type uri = string + +type 'constr context_entry = + Decl of 'constr (* Declaration *) + | Def of 'constr * 'constr (* Definition; the second argument (the type) *) + (* is not present in the DTD, but is needed *) + (* to use Coq functions during exportation. *) + +type 'constr hypothesis = identifier * 'constr context_entry +type context = constr hypothesis list + +type conjecture = int * context * constr +type metasenv = conjecture list + +(* list of couples section path -- variables defined in that section *) +type params = (string * uri list) list + +type obj = + Constant of string * (* id, *) + constr option * constr * (* value, type, *) + params (* parameters *) + | Variable of + string * constr option * constr * (* name, body, type *) + params (* parameters *) + | CurrentProof of + string * metasenv * (* name, conjectures, *) + constr * constr (* value, type *) + | InductiveDefinition of + inductiveType list * (* inductive types , *) + params * int (* parameters,n ind. pars*) +and inductiveType = + identifier * bool * constr * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + identifier * constr (* id, type *) + +type aconstr = + | ARel of id * int * id * identifier + | AVar of id * uri + | AEvar of id * int * aconstr list + | ASort of id * sorts + | ACast of id * aconstr * aconstr + | AProds of (id * name * aconstr) list * aconstr + | ALambdas of (id * name * aconstr) list * aconstr + | ALetIns of (id * name * aconstr) list * aconstr + | AApp of id * aconstr list + | AConst of id * explicit_named_substitution * uri + | AInd of id * explicit_named_substitution * uri * int + | AConstruct of id * explicit_named_substitution * uri * int * int + | ACase of id * uri * int * aconstr * aconstr * aconstr list + | AFix of id * int * ainductivefun list + | ACoFix of id * int * acoinductivefun list +and ainductivefun = + id * identifier * int * aconstr * aconstr +and acoinductivefun = + id * identifier * aconstr * aconstr +and explicit_named_substitution = id option * (uri * aconstr) list + +type acontext = (id * aconstr hypothesis) list +type aconjecture = id * int * acontext * aconstr +type ametasenv = aconjecture list + +type aobj = + AConstant of id * string * (* id, *) + aconstr option * aconstr * (* value, type, *) + params (* parameters *) + | AVariable of id * + string * aconstr option * aconstr * (* name, body, type *) + params (* parameters *) + | ACurrentProof of id * + string * ametasenv * (* name, conjectures, *) + aconstr * aconstr (* value, type *) + | AInductiveDefinition of id * + anninductiveType list * (* inductive types , *) + params * int (* parameters,n ind. pars*) +and anninductiveType = + id * identifier * bool * aconstr * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + identifier * aconstr (* id, type *) diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4 new file mode 100644 index 0000000000..b70ede2d8e --- /dev/null +++ b/contrib/xml/acic2Xml.ml4 @@ -0,0 +1,371 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*CSC codice cut & paste da cicPp e xmlcommand *) + +exception ImpossiblePossible;; +exception NotImplemented;; +let dtdname = "http://mowgli.cs.unibo.it/dtd/cic.dtd";; +let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";; + +let rec find_last_id = + function + [] -> Util.anomaly "find_last_id: empty list" + | [id,_,_] -> id + | _::tl -> find_last_id tl +;; + +let print_term ids_to_inner_sorts = + let rec aux = + let module A = Acic in + let module N = Names in + let module X = Xml in + function + A.ARel (id,n,idref,b) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "REL" + ["value",(string_of_int n) ; "binder",(N.string_of_id b) ; + "id",id ; "idref",idref; "sort",sort] + | A.AVar (id,uri) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort] + | A.AEvar (id,n,l) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort] + (List.fold_left + (fun i t -> + [< i ; X.xml_nempty "substitution" [] (aux t) >] + ) [< >] (List.rev l)) + | A.ASort (id,s) -> + let string_of_sort = + match Term.family_of_sort s with + Term.InProp -> "Prop" + | Term.InSet -> "Set" + | Term.InType -> "Type" + in + X.xml_empty "SORT" ["value",string_of_sort ; "id",id] + | A.AProds (prods,t) -> + let last_id = find_last_id prods in + let sort = Hashtbl.find ids_to_inner_sorts last_id in + X.xml_nempty "PROD" ["type",sort] + [< List.fold_left + (fun i (id,binder,s) -> + let sort = + Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) + in + let attrs = + ("id",id)::("type",sort):: + match binder with + Names.Anonymous -> [] + | Names.Name b -> ["binder",Names.string_of_id b] + in + [< X.xml_nempty "decl" attrs (aux s) ; i >] + ) [< >] prods ; + X.xml_nempty "target" [] (aux t) + >] + | A.ACast (id,v,t) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "CAST" ["id",id ; "sort",sort] + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] + | A.ALambdas (lambdas,t) -> + let last_id = find_last_id lambdas in + let sort = Hashtbl.find ids_to_inner_sorts last_id in + X.xml_nempty "LAMBDA" ["sort",sort] + [< List.fold_left + (fun i (id,binder,s) -> + let sort = + Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) + in + let attrs = + ("id",id)::("type",sort):: + match binder with + Names.Anonymous -> [] + | Names.Name b -> ["binder",Names.string_of_id b] + in + [< X.xml_nempty "decl" attrs (aux s) ; i >] + ) [< >] lambdas ; + X.xml_nempty "target" [] (aux t) + >] + | A.ALetIns (letins,t) -> + let last_id = find_last_id letins in + let sort = Hashtbl.find ids_to_inner_sorts last_id in + X.xml_nempty "LETIN" ["sort",sort] + [< List.fold_left + (fun i (id,binder,s) -> + let sort = + Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) + in + let attrs = + ("id",id)::("sort",sort):: + match binder with + Names.Anonymous -> assert false + | Names.Name b -> ["binder",Names.string_of_id b] + in + [< X.xml_nempty "def" attrs (aux s) ; i >] + ) [< >] letins ; + X.xml_nempty "target" [] (aux t) + >] + | A.AApp (id,li) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "APPLY" ["id",id ; "sort",sort] + [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li) + >] + | A.AConst (id,subst,uri) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + let attrs = ["uri", uri ; "id",id ; "sort",sort] in + aux_subst (X.xml_empty "CONST" attrs) subst + | A.AInd (id,subst,uri,i) -> + let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in + aux_subst (X.xml_empty "MUTIND" attrs) subst + | A.AConstruct (id,subst,uri,i,j) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + let attrs = + ["uri", uri ; + "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; + "id",id ; "sort",sort] + in + aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst + | A.ACase (id,uri,typeno,ty,te,patterns) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "MUTCASE" + ["uriType", uri ; + "noType", (string_of_int typeno) ; + "id", id ; "sort",sort] + [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; + X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; + List.fold_left + (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >]) + [<>] patterns + >] + | A.AFix (id, no, funs) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "FIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_left + (fun i (id,fi,ai,ti,bi) -> + [< i ; + X.xml_nempty "FixFunction" + ["id",id ; "name", (Names.string_of_id fi) ; + "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] + >] + ) [<>] funs + >] + | A.ACoFix (id,no,funs) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "COFIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_left + (fun i (id,fi,ti,bi) -> + [< i ; + X.xml_nempty "CofixFunction" + ["id",id ; "name", Names.string_of_id fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] + >] + ) [<>] funs + >] + and aux_subst target (id,subst) = + if subst = [] then + target + else + Xml.xml_nempty "instantiate" + (match id with None -> [] | Some id -> ["id",id]) + [< target ; + List.fold_left + (fun i (uri,arg) -> + [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >] + ) [<>] subst + >] + in + aux +;; + +let param_attribute_of_params params = + List.fold_right + (fun (path,l) i -> + List.fold_right + (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i' + ) l "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" +;; + +let print_object uri ids_to_inner_sorts = + let rec aux = + let module A = Acic in + let module X = Xml in + function + A.ACurrentProof (id,n,conjectures,bo,ty) -> + let xml_for_current_proof_body = +(*CSC: Should the CurrentProof also have the list of variables it depends on? *) +(*CSC: I think so. Not implemented yet. *) + X.xml_nempty "CurrentProof" ["of",uri ; "id", id] + [< List.fold_left + (fun i (cid,n,canonical_context,t) -> + [< i ; + X.xml_nempty "Conjecture" + ["id", cid ; "no",(string_of_int n)] + [< List.fold_left + (fun i (hid,t) -> + [< (match t with + n,A.Decl t -> + X.xml_nempty "Decl" + ["id",hid;"name",Names.string_of_id n] + (print_term ids_to_inner_sorts t) + | n,A.Def (t,_) -> + X.xml_nempty "Def" + ["id",hid;"name",Names.string_of_id n] + (print_term ids_to_inner_sorts t) + ) ; + i + >] + ) [< >] canonical_context ; + X.xml_nempty "Goal" [] + (print_term ids_to_inner_sorts t) + >] + >]) + [<>] (List.rev conjectures) ; + X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] + in + let xml_for_current_proof_type = + X.xml_nempty "ConstantType" ["name",n ; "id", id] + (print_term ids_to_inner_sorts ty) + in + let xmlbo = + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n"); + xml_for_current_proof_body + >] in + let xmlty = + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata + ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n"); + xml_for_current_proof_type + >] + in + xmlty, Some xmlbo + | A.AConstant (id,n,bo,ty,params) -> + let params' = param_attribute_of_params params in + let xmlbo = + match bo with + None -> None + | Some bo -> + Some + [< X.xml_cdata + "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata + ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ; + X.xml_nempty "ConstantBody" + ["for",uri ; "params",params' ; "id", id] + [< print_term ids_to_inner_sorts bo >] + >] + in + let xmlty = + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n"); + X.xml_nempty "ConstantType" + ["name",n ; "params",params' ; "id", id] + [< print_term ids_to_inner_sorts ty >] + >] + in + xmlty, xmlbo + | A.AVariable (id,n,bo,ty,params) -> + let params' = param_attribute_of_params params in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n") ; + X.xml_nempty "Variable" ["name",n ; "params",params' ; "id", id] + [< (match bo with + None -> [<>] + | Some bo -> + X.xml_nempty "body" [] + (print_term ids_to_inner_sorts bo) + ) ; + X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) + >] + >], None + | A.AInductiveDefinition (id,tys,params,nparams) -> + let params' = param_attribute_of_params params in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ + dtdname ^ "\">\n") ; + X.xml_nempty "InductiveDefinition" + ["noParams",string_of_int nparams ; + "id",id ; + "params",params'] + [< (List.fold_left + (fun i (id,typename,finite,arity,cons) -> + [< i ; + X.xml_nempty "InductiveType" + ["id",id ; "name",Names.string_of_id typename ; + "inductive",(string_of_bool finite) + ] + [< X.xml_nempty "arity" [] + (print_term ids_to_inner_sorts arity) ; + (List.fold_left + (fun i (name,lc) -> + [< i ; + X.xml_nempty "Constructor" + ["name",Names.string_of_id name] + (print_term ids_to_inner_sorts lc) + >]) [<>] cons + ) + >] + >] + ) [< >] tys + ) + >] + >], None + in + aux +;; + +let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = + let module C2A = Cic2acic in + let module X = Xml in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^"\">\n"); + X.xml_nempty "InnerTypes" ["of",curi] + (Hashtbl.fold + (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> + [< x ; + X.xml_nempty "TYPE" ["of",id] + [< X.xml_nempty "synthesized" [] + (print_term ids_to_inner_sorts synty) ; + match expty with + None -> [<>] + | Some expty' -> + X.xml_nempty "expected" [] + (print_term ids_to_inner_sorts expty') + >] + >] + ) ids_to_inner_types [<>] + ) + >] +;; diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml new file mode 100644 index 0000000000..19dfc940ae --- /dev/null +++ b/contrib/xml/cic2acic.ml @@ -0,0 +1,723 @@ +(* Utility Functions *) + +exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; +let get_module_path_of_section_path path = + let dirpath = fst (Libnames.repr_path path) in + let modules = Lib.module_dp () :: (Library.loaded_libraries ()) in + match + List.filter + (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules + with + [modul] -> modul + | _ -> raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther +;; + +(*CSC: Problem: here we are using the wrong (???) hypothesis that there do *) +(*CSC: not exist two modules whose dir_paths are one a prefix of the other *) +let remove_module_dirpath_from_dirpath ~basedir dir = + let module Ln = Libnames in + if Ln.is_dirpath_prefix_of basedir dir then + let ids = Names.repr_dirpath dir in + let rec remove_firsts n l = + match n,l with + (0,l) -> l + | (n,he::tl) -> remove_firsts (n-1) tl + | _ -> assert false + in + let ids' = + List.rev + (remove_firsts + (List.length (Names.repr_dirpath basedir)) + (List.rev ids)) + in + ids' + else Names.repr_dirpath dir +;; + + +let get_uri_of_var v pvars = + let module D = Declare in + let module N = Names in + let rec search_in_pvars names = + function + [] -> None + | ((name,l)::tl) -> + let names' = name::names in + if List.mem v l then + Some names' + else + search_in_pvars names' tl + in + let rec search_in_open_sections = + function + [] -> Util.error "Variable not found" + | he::tl as modules -> + let dirpath = N.make_dirpath modules in + if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then + modules + else + search_in_open_sections tl + in + let path = + match search_in_pvars [] pvars with + None -> search_in_open_sections (N.repr_dirpath (Lib.cwd ())) + | Some path -> path + in + "cic:" ^ + List.fold_left + (fun i x -> "/" ^ N.string_of_id x ^ i) "" path +;; + +type tag = + Constant + | Inductive + | Variable +;; + +let ext_of_tag = + function + Constant -> "con" + | Inductive -> "ind" + | Variable -> "var" +;; + +exception FunctorsXMLExportationNotImplementedYet;; + +let subtract l1 l2 = + let l1' = List.rev (Names.repr_dirpath l1) in + let l2' = List.rev (Names.repr_dirpath l2) in + let rec aux = + function + he::tl when tl = l2' -> [he] + | he::tl -> he::(aux tl) + | [] -> assert (l2' = []) ; [] + in + Names.make_dirpath (List.rev (aux l1')) +;; + +let token_list_of_kernel_name ~keep_sections kn tag = + let module N = Names in + let (modpath,dirpath,label) = Names.repr_kn kn in + let token_list_of_dirpath dirpath = + List.rev_map N.string_of_id (N.repr_dirpath dirpath) in + let rec token_list_of_modpath = + function + N.MPdot (path,label) -> + token_list_of_modpath path @ [N.string_of_label label] + | N.MPfile dirpath -> token_list_of_dirpath dirpath + | N.MPself _ -> +(*CSC: ask Hugo if this always make sense *) + let module_path = + subtract (Lib.cwd ()) (snd (Lib.current_prefix ())) + in + token_list_of_dirpath module_path + | N.MPbound _ -> raise FunctorsXMLExportationNotImplementedYet + in + token_list_of_modpath modpath @ + (if keep_sections then token_list_of_dirpath dirpath else []) @ + [N.string_of_label label ^ "." ^ (ext_of_tag tag)] +;; + +let uri_of_kernel_name ?(keep_sections=false) kn tag = + let module N = Names in + let tokens = token_list_of_kernel_name ~keep_sections kn tag in + "cic:/" ^ String.concat "/" tokens +;; + +(* Main Functions *) + +type anntypes = + {annsynthesized : Acic.aconstr ; annexpected : Acic.aconstr option} +;; + +let gen_id seed = + let res = "i" ^ string_of_int !seed in + incr seed ; + res +;; + +let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids = + fun father t -> + let res = gen_id seed in + Hashtbl.add ids_to_father_ids res father ; + Hashtbl.add ids_to_terms res t ; + Acic.CicHash.add constr_to_ids t res ; + res +;; + +let source_id_of_id id = "#source#" ^ id;; + +let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids + ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars env idrefs + evar_map t expectedty += + let module D = DoubleTypeInference in + let module E = Environ in + let module N = Names in + let module A = Acic in + let module T = Term in + let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in + (* CSC: do you have any reasonable substitute for 503? *) + let terms_to_types = Acic.CicHash.create 503 in + D.double_type_of env evar_map t expectedty terms_to_types ; + let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env + idrefs ?(subst=None,[]) tt + = + let fresh_id'' = fresh_id' father tt in + let aux' = aux computeinnertypes (Some fresh_id'') [] in + let string_of_sort_family = + function + T.InProp -> "Prop" + | T.InSet -> "Set" + | T.InType -> "Type" + in + let string_of_sort t = + string_of_sort_family + (T.family_of_sort + (T.destSort (Reductionops.whd_betadeltaiota env evar_map t))) + in + let ainnertypes,innertype,innersort,expected_available = + let {D.synthesized = synthesized; D.expected = expected} = + if computeinnertypes then +try + Acic.CicHash.find terms_to_types tt +with _ -> +(*CSC: Warning: it really happens, for example in Ring_theory!!! *) +Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm tt)) ; assert false (* buco nella double-type-inference *) ; {D.synthesized = Reductionops.nf_beta (Retyping.get_type_of env evar_map (Evarutil.refresh_universes tt)) ; D.expected = None} + else + (* We are already in an inner-type and Coscoy's double *) + (* type inference algorithm has not been applied. *) + (* We need to refresh the universes because we are doing *) + (* type inference on an already inferred type. *) + {D.synthesized = + Reductionops.nf_beta + (Retyping.get_type_of env evar_map + (Evarutil.refresh_universes tt)) ; + D.expected = None} + in +(* Debugging only: +print_endline "TERMINE:" ; flush stdout ; +Pp.ppnl (Printer.prterm tt) ; flush stdout ; +print_endline "TIPO:" ; flush stdout ; +Pp.ppnl (Printer.prterm synthesized) ; flush stdout ; +print_endline "ENVIRONMENT:" ; flush stdout ; +Pp.ppnl (Printer.pr_context_of env) ; flush stdout ; +print_endline "FINE_ENVIRONMENT" ; flush stdout ; +*) + let innersort = Retyping.get_sort_family_of env evar_map synthesized in +(* Debugging only: +print_endline "PASSATO" ; flush stdout ; +*) + let ainnertypes,expected_available = + if computeinnertypes then + let annexpected,expected_available = + match expected with + None -> None,false + | Some expectedty' -> + Some (aux false (Some fresh_id'') [] env idrefs expectedty'), + true + in + Some + {annsynthesized = + aux false (Some fresh_id'') [] env idrefs synthesized ; + annexpected = annexpected + }, expected_available + else + None,false + in + ainnertypes,synthesized, string_of_sort_family innersort, + expected_available + in + let add_inner_type id = + match ainnertypes with + None -> () + | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes + in + + (* explicit_substitute_and_eta_expand_if_required h t t' *) + (* where [t] = [] and [tt] = [h]{[t']} ("{.}" denotes explicit *) + (* named substitution) or [tt] = (App [h]::[t]) (and [t'] = []) *) + (* check if [h] is a term that requires an explicit named *) + (* substitution and, in that case, uses the first arguments of *) + (* [t] as the actual arguments of the substitution. If there *) + (* are not enough parameters in the list [t], then eta-expansion *) + (* is performed. *) + let + explicit_substitute_and_eta_expand_if_required h t t' + compute_result_if_eta_expansion_not_required + = + let subst,residual_args,uninst_vars = + let variables,basedir = + try + let g = Declare.reference_of_constr h in + let sp = + match g with + Libnames.ConstructRef ((induri,_),_) + | Libnames.IndRef (induri,_) -> + Nametab.sp_of_global None (Libnames.IndRef (induri,0)) + | Libnames.VarRef id -> + (* Invariant: variables are never cooked in Coq *) + raise Not_found + | _ -> Nametab.sp_of_global None g + in + Dischargedhypsmap.get_discharged_hyps sp, + get_module_path_of_section_path sp + with Not_found -> + (* no explicit substitution *) + [], Libnames.dirpath_of_string "dummy" + in + (* returns a triple whose first element is *) + (* an explicit named substitution of "type" *) + (* (variable * argument) list, whose *) + (* second element is the list of residual *) + (* arguments and whose third argument is *) + (* the list of uninstantiated variables *) + let rec get_explicit_subst variables arguments = + match variables,arguments with + [],_ -> [],arguments,[] + | _,[] -> [],[],variables + | he1::tl1,he2::tl2 -> + let subst,extra_args,uninst = get_explicit_subst tl1 tl2 in + let (he1_sp, he1_id) = Libnames.repr_path he1 in + let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in + let he1'' = + String.concat "/" + (List.map Names.string_of_id (List.rev he1')) ^ "/" + ^ (Names.string_of_id he1_id) ^ ".var" + in + (he1'',he2)::subst, extra_args, uninst + in + get_explicit_subst variables t' + in + let uninst_vars_length = List.length uninst_vars in + if uninst_vars_length > 0 then + (* Not enough arguments provided. We must eta-expand! *) + let un_args,_ = + T.decompose_prod_n uninst_vars_length + (Retyping.get_type_of env evar_map tt) + in + let eta_expanded = + let arguments = + List.map (T.lift uninst_vars_length) t @ + Termops.rel_list 0 uninst_vars_length + in + Unshare.unshare + (T.lamn uninst_vars_length un_args + (T.applistc h arguments)) + in + D.double_type_of env evar_map eta_expanded + None terms_to_types ; + Hashtbl.remove ids_to_inner_types fresh_id'' ; + aux' env idrefs eta_expanded + else + compute_result_if_eta_expansion_not_required subst residual_args + in + + (* Now that we have all the auxiliary functions we *) + (* can finally proceed with the main case analysis. *) + match T.kind_of_term tt with + T.Rel n -> + let id = + match List.nth (E.rel_context env) (n - 1) with + (N.Name id,_,_) -> id + | (N.Anonymous,_,_) -> Nameops.make_ident "_" None + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + A.ARel (fresh_id'', n, List.nth idrefs (n-1), id) + | T.Var id -> + let path = get_uri_of_var (N.string_of_id id) pvars in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + A.AVar + (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var") + | T.Evar (n,l) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + A.AEvar + (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) + | T.Meta _ -> Util.anomaly "Meta met during exporting to XML" + | T.Sort s -> A.ASort (fresh_id'', s) + | T.Cast (v,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + A.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t) + | T.Prod (n,s,t) -> + let n' = + match n with + N.Anonymous -> N.Anonymous + | _ -> + N.Name (Nameops.next_name_away n (Termops.ids_of_context env)) + in + Hashtbl.add ids_to_inner_sorts fresh_id'' + (string_of_sort innertype) ; + let sourcetype = Retyping.get_type_of env evar_map s in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort sourcetype) ; + let new_passed_prods = + let father_is_prod = + match father with + None -> false + | Some father' -> + match + Term.kind_of_term (Hashtbl.find ids_to_terms father') + with + T.Prod _ -> true + | _ -> false + in + (fresh_id'', n', aux' env idrefs s):: + (if father_is_prod then + passed_lambdas_or_prods_or_letins + else []) + in + let new_env = E.push_rel (n', None, s) env in + let new_idrefs = fresh_id''::idrefs in + (match Term.kind_of_term t with + T.Prod _ -> + aux computeinnertypes (Some fresh_id'') new_passed_prods + new_env new_idrefs t + | _ -> + A.AProds (new_passed_prods, aux' new_env new_idrefs t)) + | T.Lambda (n,s,t) -> + let n' = + match n with + N.Anonymous -> N.Anonymous + | _ -> + N.Name (Nameops.next_name_away n (Termops.ids_of_context env)) + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + let sourcetype = Retyping.get_type_of env evar_map s in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort sourcetype) ; + let father_is_lambda = + match father with + None -> false + | Some father' -> + match + Term.kind_of_term (Hashtbl.find ids_to_terms father') + with + T.Lambda _ -> true + | _ -> false + in + if innersort = "Prop" && + ((not father_is_lambda) || expected_available) + then add_inner_type fresh_id'' ; + let new_passed_lambdas = + (fresh_id'',n', aux' env idrefs s):: + (if father_is_lambda then + passed_lambdas_or_prods_or_letins + else []) in + let new_env = E.push_rel (n', None, s) env in + let new_idrefs = fresh_id''::idrefs in + (match Term.kind_of_term t with + T.Lambda _ -> + aux computeinnertypes (Some fresh_id'') new_passed_lambdas + new_env new_idrefs t + | _ -> + let t' = aux' new_env new_idrefs t in + (* eta-expansion for explicit named substitutions *) + (* can create nested Lambdas. Here we perform the *) + (* flattening. *) + match t' with + A.ALambdas (lambdas, t'') -> + A.ALambdas (lambdas@new_passed_lambdas, t'') + | _ -> + A.ALambdas (new_passed_lambdas, t') + ) + | T.LetIn (n,s,t,d) -> + let n' = + match n with + N.Anonymous -> N.Anonymous + | _ -> + N.Name (Nameops.next_name_away n (Termops.ids_of_context env)) + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + let sourcesort = + Retyping.get_sort_family_of env evar_map + (Retyping.get_type_of env evar_map s) + in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort_family sourcesort) ; + let father_is_letin = + match father with + None -> false + | Some father' -> + match + Term.kind_of_term (Hashtbl.find ids_to_terms father') + with + T.LetIn _ -> true + | _ -> false + in + if innersort = "Prop" then + add_inner_type fresh_id'' ; + let new_passed_letins = + (fresh_id'',n', aux' env idrefs s):: + (if father_is_letin then + passed_lambdas_or_prods_or_letins + else []) in + let new_env = E.push_rel (n', Some s, t) env in + let new_idrefs = fresh_id''::idrefs in + (match Term.kind_of_term d with + T.LetIn _ -> + aux computeinnertypes (Some fresh_id'') new_passed_letins + new_env new_idrefs d + | _ -> A.ALetIns + (new_passed_letins, aux' new_env new_idrefs d)) + | T.App (h,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + let + compute_result_if_eta_expansion_not_required subst residual_args + = + let residual_args_not_empty = List.length residual_args > 0 in + let h' = + if residual_args_not_empty then + aux' env idrefs ~subst:(None,subst) h + else + aux' env idrefs ~subst:(Some fresh_id'',subst) h + in + (* maybe all the arguments were used for the explicit *) + (* named substitution *) + if residual_args_not_empty then + A.AApp (fresh_id'', h'::residual_args) + else + h' + in + let t' = + Array.fold_right (fun x i -> (aux' env idrefs x)::i) t [] + in + explicit_substitute_and_eta_expand_if_required h + (Array.to_list t) t' + compute_result_if_eta_expansion_not_required + | T.Const kn -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let compute_result_if_eta_expansion_not_required _ _ = + A.AConst (fresh_id'', subst, (uri_of_kernel_name kn Constant)) + in + let (_,subst') = subst in + explicit_substitute_and_eta_expand_if_required tt [] + (List.map snd subst') + compute_result_if_eta_expansion_not_required + | T.Ind (kn,i) -> + let compute_result_if_eta_expansion_not_required _ _ = + A.AInd (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i) + in + let (_,subst') = subst in + explicit_substitute_and_eta_expand_if_required tt [] + (List.map snd subst') + compute_result_if_eta_expansion_not_required + | T.Construct ((kn,i),j) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let compute_result_if_eta_expansion_not_required _ _ = + A.AConstruct + (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i, j) + in + let (_,subst') = subst in + explicit_substitute_and_eta_expand_if_required tt [] + (List.map snd subst') + compute_result_if_eta_expansion_not_required + | T.Case ({T.ci_ind=(kn,i)},ty,term,a) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + let a' = + Array.fold_right (fun x i -> (aux' env idrefs x)::i) a [] + in + A.ACase + (fresh_id'', (uri_of_kernel_name kn Inductive), i, + aux' env idrefs ty, aux' env idrefs term, a') + | T.Fix ((ai,i),((f,t,b) as rec_decl)) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" 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 + A.AFix (fresh_id'', i, + Array.fold_right + (fun (id,fi,ti,bi,ai) i -> + let fi' = + match fi with + N.Name fi -> fi + | N.Anonymous -> Util.error "Anonymous fix function met" + in + (id, fi', ai, + aux' env idrefs ti, + aux' (E.push_rec_types rec_decl env) new_idrefs bi)::i) + (Array.mapi + (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f + ) [] + ) + | T.CoFix (i,((f,t,b) as rec_decl)) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" 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 + A.ACoFix (fresh_id'', i, + Array.fold_right + (fun (id,fi,ti,bi) i -> + let fi' = + match fi with + N.Name fi -> fi + | N.Anonymous -> Util.error "Anonymous fix function met" + in + (id, fi', + aux' env idrefs ti, + aux' (E.push_rec_types rec_decl env) new_idrefs bi)::i) + (Array.mapi + (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f + ) [] + ) + in + aux computeinnertypes None [] env idrefs t +;; + +let acic_of_cic_context metasenv context t = + let ids_to_terms = Hashtbl.create 503 in + let constr_to_ids = Acic.CicHash.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + let seed = ref 0 in + acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids + ids_to_inner_sorts ids_to_inner_types metasenv context t, + ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types +;; + +let acic_object_of_cic_object pvars sigma obj = + let module A = Acic in + let ids_to_terms = Hashtbl.create 503 in + let constr_to_ids = Acic.CicHash.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + let ids_to_conjectures = Hashtbl.create 11 in + let ids_to_hypotheses = Hashtbl.create 127 in + let hypotheses_seed = ref 0 in + let conjectures_seed = ref 0 in + let seed = ref 0 in + let acic_term_of_cic_term_context' = + acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids + ids_to_inner_sorts ids_to_inner_types pvars in +(*CSC: is this the right env to use? Hhmmm. There is a problem: in *) +(*CSC: Global.env () the object we are exporting is already defined, *) +(*CSC: either in the environment or in the named context (in the case *) +(*CSC: of variables. Is this a problem? *) + let env = Global.env () in + let acic_term_of_cic_term' = acic_term_of_cic_term_context' env [] sigma in +(*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *) +(*CSC: a modified version of the already existent fresh_id function *) + let fresh_id () = + let res = "i" ^ string_of_int !seed in + incr seed ; + res + in + let aobj = + match obj with + A.Constant (id,bo,ty,params) -> + let abo = + match bo with + None -> None + | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty)) + in + let aty = acic_term_of_cic_term' ty None in + A.AConstant (fresh_id (),id,abo,aty,params) + | A.Variable (id,bo,ty,params) -> + let abo = + match bo with + Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) + | None -> None + in + let aty = acic_term_of_cic_term' ty None in + A.AVariable (fresh_id (),id,abo,aty,params) + | A.CurrentProof (id,conjectures,bo,ty) -> + let aconjectures = + List.map + (function (i,canonical_context,term) as conjecture -> + let cid = "c" ^ string_of_int !conjectures_seed in + Hashtbl.add ids_to_conjectures cid conjecture ; + incr conjectures_seed ; + let canonical_env,idrefs',acanonical_context = + let rec aux env idrefs = + function + [] -> env,idrefs,[] + | ((n,decl_or_def) as hyp)::tl -> + let hid = "h" ^ string_of_int !hypotheses_seed in + let new_idrefs = hid::idrefs in + Hashtbl.add ids_to_hypotheses hid hyp ; + incr hypotheses_seed ; + match decl_or_def with + A.Decl t -> + let final_env,final_idrefs,atl = + aux (Environ.push_rel (Names.Name n,None,t) env) + new_idrefs tl + in + let at = + acic_term_of_cic_term_context' env idrefs sigma t None + in + final_env,final_idrefs,(hid,(n,A.Decl at))::atl + | A.Def (t,ty) -> + let final_env,final_idrefs,atl = + aux + (Environ.push_rel (Names.Name n,Some t,ty) env) + new_idrefs tl + in + let at = + acic_term_of_cic_term_context' env idrefs sigma t None + in + let dummy_never_used = + let s = "dummy_never_used" in + A.ARel (s,99,s,Names.id_of_string s) + in + final_env,final_idrefs, + (hid,(n,A.Def (at,dummy_never_used)))::atl + in + aux env [] canonical_context + in + let aterm = + acic_term_of_cic_term_context' canonical_env idrefs' sigma term + None + in + (cid,i,List.rev acanonical_context,aterm) + ) conjectures in + let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in + let aty = acic_term_of_cic_term_context' env [] sigma ty None in + A.ACurrentProof (fresh_id (),id,aconjectures,abo,aty) + | A.InductiveDefinition (tys,params,paramsno) -> + let env' = + List.fold_right + (fun (name,_,arity,_) env -> + Environ.push_rel (Names.Name name, None, arity) env + ) (List.rev tys) env in + let idrefs = List.map (function _ -> gen_id seed) tys in + let atys = + List.map2 + (fun id (name,inductive,ty,cons) -> + let acons = + List.map + (function (name,ty) -> + (name, + acic_term_of_cic_term_context' env' idrefs Evd.empty ty None) + ) cons + in + (id,name,inductive,acic_term_of_cic_term' ty None,acons) + ) (List.rev idrefs) tys + in + A.AInductiveDefinition (fresh_id (),atys,params,paramsno) + in + aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses +;; diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml new file mode 100644 index 0000000000..d0ea156e7e --- /dev/null +++ b/contrib/xml/doubleTypeInference.ml @@ -0,0 +1,243 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT MoWGLI *) +(* *) +(* A module to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* 22/06/2002 *) +(* *) +(*****************************************************************************) + +(*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *) +type types = {synthesized : Term.types ; expected : Term.types option};; + +(* Code similar to the code in the Typing module, but: *) +(* - the term is already assumed to be well typed *) +(* - some checks have been removed *) +(* - both the synthesized and expected types of every *) +(* node are computed (Coscoy's double type inference) *) + +let assumption_of_judgment env sigma j = + Typeops.assumption_of_judgment env (Evarutil.j_nf_evar sigma j) +;; + +let type_judgment env sigma j = + Typeops.type_judgment env (Evarutil.j_nf_evar sigma j) +;; + +let double_type_of env sigma cstr expectedty subterms_to_types = + (*CSC: the code is inefficient because judgments are created just to be *) + (*CSC: destroyed using Environ.j_type. Moreover I am pretty sure that the *) + (*CSC: functions used do checks that we do not need *) + let rec execute env sigma cstr expectedty = + let module T = Term in + let module E = Environ in + (* the type part is the synthesized type *) + let judgement = + match T.kind_of_term cstr with + T.Meta n -> + Util.error + "DoubleTypeInference.double_type_of: found a non-instanciated goal" + + | T.Evar ((n,l) as ev) -> + let ty = Unshare.unshare (Instantiate.existential_type sigma ev) in + let jty = execute env sigma ty None in + let jty = assumption_of_judgment env sigma jty in + let evar_context = (Evd.map sigma n).Evd.evar_hyps in + let rec iter actual_args evar_context = + match actual_args,evar_context with + [],[] -> () + | he1::tl1,(n,_,ty)::tl2 -> + (* for side-effects *) + let _ = execute env sigma he1 (Some ty) in + let tl2' = + List.map + (function (m,bo,ty) -> + (* Warning: the substitution should be performed also on bo *) + (* This is not done since bo is not used later yet *) + (m,bo,Unshare.unshare (T.replace_vars [n,he1] ty)) + ) tl2 + in + iter tl1 tl2' + | _,_ -> assert false + in + (* for side effects only *) + iter (List.rev (Array.to_list l)) (List.rev evar_context) ; + E.make_judge cstr jty + + | T.Rel n -> + Typeops.judge_of_relative env n + + | T.Var id -> + Typeops.judge_of_variable env id + + | T.Const c -> + E.make_judge cstr (E.constant_type env c) + + | T.Ind ind -> + E.make_judge cstr (Inductive.type_of_inductive env ind) + + | T.Construct cstruct -> + E.make_judge cstr (Inductive.type_of_constructor env cstruct) + + | T.Case (ci,p,c,lf) -> + let expectedtype = + Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in + let cj = execute env sigma c (Some expectedtype) in + let pj = execute env sigma p None in + let (expectedtypes,_,_) = + let indspec = Inductive.find_rectype env cj.Environ.uj_type in + Inductive.type_case_branches env indspec pj cj.Environ.uj_val + in + let lfj = + execute_array env sigma lf + (Array.map (function x -> Some x) expectedtypes) in + let (j,_) = Typeops.judge_of_case env ci pj cj lfj in + j + + | T.Fix ((vn,i as vni),recdef) -> + let (_,tys,_ as recdef') = execute_recdef env sigma recdef in + let fix = (vni,recdef') in + E.make_judge (T.mkFix fix) tys.(i) + + | T.CoFix (i,recdef) -> + let (_,tys,_ as recdef') = execute_recdef env sigma recdef in + let cofix = (i,recdef') in + E.make_judge (T.mkCoFix cofix) tys.(i) + + | T.Sort (T.Prop c) -> + Typeops.judge_of_prop_contents c + + | T.Sort (T.Type u) -> +(*CSC: In case of need, I refresh the universe. But exportation of the *) +(*CSC: right universe level information is destroyed. It must be changed *) +(*CSC: again once Judicael will introduce his non-bugged algebraic *) +(*CSC: universes. *) +(try + Typeops.judge_of_type u + with _ -> (* Successor of a non universe-variable universe anomaly *) + (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ; + Typeops.judge_of_type (Termops.new_univ ()) +) + + | T.App (f,args) -> + let expected_head = + Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in + let j = execute env sigma f (Some expected_head) in + let expected_args = + let rec aux typ = + function + [] -> [] + | hj::restjl -> + match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with + T.Prod (_,c1,c2) -> + (Some (Reductionops.nf_beta c1)) :: + (aux (T.subst1 hj c2) restjl) + | _ -> assert false + in + Array.of_list (aux j.Environ.uj_type (Array.to_list args)) + in + let jl = execute_array env sigma args expected_args in + let (j,_) = Typeops.judge_of_apply env j jl in + j + + | T.Lambda (name,c1,c2) -> + let j = execute env sigma c1 None in + let var = type_judgment env sigma j in + let env1 = E.push_rel (name,None,var.E.utj_val) env in + let expectedc2type = + match expectedty with + None -> None + | Some ety -> + match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with + T.Prod (_,_,expected_target_type) -> + Some (Reductionops.nf_beta expected_target_type) + | _ -> assert false + in + let j' = execute env1 sigma c2 expectedc2type in + Typeops.judge_of_abstraction env1 name var j' + + | T.Prod (name,c1,c2) -> + let j = execute env sigma c1 None in + let varj = type_judgment env sigma j in + let env1 = E.push_rel (name,None,varj.E.utj_val) env in + let j' = execute env1 sigma c2 None in + let varj' = type_judgment env1 sigma j' in + Typeops.judge_of_product env name varj varj' + + | T.LetIn (name,c1,c2,c3) -> +(*CSC: What are the right expected types for the source and *) +(*CSC: target of a LetIn? None used. *) + let j1 = execute env sigma c1 None in + let j2 = execute env sigma c2 None in + let j2 = type_judgment env sigma j2 in + let env1 = + E.push_rel (name,Some j1.E.uj_val,j2.E.utj_val) env + in + let j3 = execute env1 sigma c3 None in + Typeops.judge_of_letin env name j1 j2 j3 + + | T.Cast (c,t) -> + let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in + let tj = execute env sigma t None in + let tj = type_judgment env sigma tj in + let j, _ = Typeops.judge_of_cast env cj tj in + j + in + let synthesized = E.j_type judgement in + let synthesized' = Reductionops.nf_beta synthesized in + let types,res = + match expectedty with + None -> + (* No expected type *) + {synthesized = synthesized' ; expected = None}, synthesized + (*CSC: in HELM we did not considered Casts to be irrelevant. *) + (*CSC: does it really matter? (eq_constr is up to casts) *) + | Some ty when Term.eq_constr synthesized' ty -> + (* The expected type is synthactically equal to *) + (* the synthesized type. Let's forget it. *) + {synthesized = synthesized' ; expected = None}, synthesized + | Some expectedty' -> + {synthesized = synthesized' ; expected = Some expectedty'}, + expectedty' + in +(*CSC: debugging stuff to be removed *) +if Acic.CicHash.mem subterms_to_types cstr then + (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ; + Acic.CicHash.add subterms_to_types cstr types ; + E.make_judge cstr res + + + and execute_recdef env sigma (names,lar,vdef) = + let length = Array.length lar in + let larj = + execute_array env sigma lar (Array.make length None) in + let lara = Array.map (assumption_of_judgment env sigma) larj in + let env1 = Environ.push_rec_types (names,lara,vdef) env in + let expectedtypes = + Array.map (function i -> Some (Term.lift length i)) lar + in + let vdefj = execute_array env1 sigma vdef expectedtypes in + let vdefv = Array.map Environ.j_val vdefj in + (names,lara,vdefv) + + and execute_array env sigma v expectedtypes = + let jl = + execute_list env sigma (Array.to_list v) (Array.to_list expectedtypes) + in + Array.of_list jl + + and execute_list env sigma = + List.map2 (execute env sigma) + +in + ignore (execute env sigma cstr expectedty) +;; diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli new file mode 100644 index 0000000000..2e0badbfbd --- /dev/null +++ b/contrib/xml/doubleTypeInference.mli @@ -0,0 +1,5 @@ +type types = { synthesized : Term.types; expected : Term.types option; } + +val double_type_of : + Environ.env -> Evd.evar_map -> Term.constr -> Term.constr option -> + types Acic.CicHash.t -> unit diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml new file mode 100644 index 0000000000..80b45cc6d7 --- /dev/null +++ b/contrib/xml/proof2aproof.ml @@ -0,0 +1,154 @@ +(* Note: we can not use the Set module here because we _need_ physical *) +(* equality and there exists no comparison function compatible with *) +(* physical equality. *) +module S = + struct + let empty = [] + let mem = List.memq + let add x l = x::l + end +;; + +(* evar reduction that preserves some terms *) +let nf_evar sigma ~preserve = + let module T = Term in + let rec aux t = + if preserve t then t else + match T.kind_of_term t with + | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _ + | T.Construct _ -> t + | T.Cast (c1,c2) -> T.mkCast (aux c1, aux c2) + | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2) + | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c) + | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c) + | T.App (c,l) -> + let c' = aux c in + let l' = Array.map aux l in + (match T.kind_of_term c' with + T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') + | T.Cast (he,_) -> + (match T.kind_of_term he with + T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') + | _ -> T.mkApp (c', l') + ) + | _ -> T.mkApp (c', l')) + | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e -> + aux (Instantiate.existential_value sigma (e,l)) + | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) + | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) + | T.Fix (ln,(lna,tl,bl)) -> + T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl)) + | T.CoFix(ln,(lna,tl,bl)) -> + T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl)) + in + aux +;; + +(* Unshares a proof-tree. *) +(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *) +let rec unshare_proof_tree = + let module PT = Proof_type in + function {PT.status = status ; PT.goal = goal ; PT.ref = ref} -> + let unshared_ref = + match ref with + None -> None + | Some (rule,pfs) -> + let unshared_rule = + match rule with + PT.Prim prim -> PT.Prim prim + | PT.Change_evars -> PT.Change_evars + | PT.Tactic (tactic_expr, pf) -> + PT.Tactic (tactic_expr, unshare_proof_tree pf) + in + Some (unshared_rule, List.map unshare_proof_tree pfs) + in + {PT.status = status ; PT.goal = goal ; PT.ref = unshared_ref} +;; + +module ProofTreeHash = + Hashtbl.Make + (struct + type t = Proof_type.proof_tree + let equal = (==) + let hash = Hashtbl.hash + end) +;; + + +let extract_open_proof sigma pf = + let module PT = Proof_type in + let module L = Logic in + let sigma = ref sigma in + let proof_tree_to_constr = ProofTreeHash.create 503 in + let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in + let unshared_constrs = ref S.empty in + let rec proof_extractor vl node = + let constr = + match node with + {PT.ref=Some(PT.Prim _,_)} as pf -> + L.prim_extractor proof_extractor vl pf + + | {PT.ref=Some(PT.Tactic (_,hidden_proof),spfl)} -> + let sgl,v = Refiner.frontier hidden_proof in + let flat_proof = v spfl in + ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ; + proof_extractor vl flat_proof + + | {PT.ref=Some(PT.Change_evars,[pf])} -> (proof_extractor vl) pf + + | {PT.ref=None;PT.goal=goal} -> + let visible_rels = + Util.map_succeed + (fun id -> + (* Section variables are in the [id] list but are not *) + (* lambda abstracted in the term [vl] *) + try let n = Util.list_index id vl in (n,id) + with Not_found -> failwith "caught") +(*CSC: the above function must be modified such that when it is found *) +(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *) +(*CSC: as the evar_instance. Ordering the instance becomes useless (it *) +(*CSC: will already be ordered. *) + (Termops.ids_of_named_context goal.Evd.evar_hyps) in + let sorted_rels = + Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in + let context = + List.map + (fun (_,id) -> Sign.lookup_named id goal.Evd.evar_hyps) + sorted_rels + in +(*CSC: the section variables in the right order must be added too *) + let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in + let env = Global.env_of_context context in + let sigma',evar = + Evarutil.new_isevar_sign env !sigma goal.Evd.evar_concl evar_instance + in + sigma := sigma' ; + evar + + | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor" + in + let unsharedconstr = + let evar_nf_constr = + nf_evar !sigma ~preserve:(function e -> S.mem e !unshared_constrs) constr + in + Unshare.unshare + ~already_unshared:(function e -> S.mem e !unshared_constrs) + evar_nf_constr + in +(*CSC: debugging stuff to be removed *) +if ProofTreeHash.mem proof_tree_to_constr node then + Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") (Refiner.print_proof !sigma [] node)) ; + ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; + unshared_constrs := S.add unsharedconstr !unshared_constrs ; + unsharedconstr + in + let unshared_pf = unshare_proof_tree pf in + let pfterm = proof_extractor [] unshared_pf in + (pfterm, !sigma, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, + unshared_pf) +;; + +let extract_open_pftreestate pts = + extract_open_proof (Refiner.evc_of_pftreestate pts) + (Tacmach.proof_of_pftreestate pts) +;; diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 new file mode 100644 index 0000000000..4a568da36f --- /dev/null +++ b/contrib/xml/proofTree2Xml.ml4 @@ -0,0 +1,190 @@ +let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; + +let std_ppcmds_to_string s = + Pp.msg_with Format.str_formatter s; + Format.flush_str_formatter () +;; + +let idref_of_id id = "v" ^ id;; + +(* Transform a constr to an Xml.token Stream.t *) +(* env is a named context *) +(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *) +let constr_to_xml obj sigma env = + let ids_to_terms = Hashtbl.create 503 in + let constr_to_ids = Acic.CicHash.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + + let pvars = [] in + (* named_context holds section variables and local variables *) + let named_context = Environ.named_context env in + (* real_named_context holds only the section variables *) + let real_named_context = Environ.named_context (Global.env ()) in + (* named_context' holds only the local variables *) + let named_context' = + List.filter (function n -> not (List.mem n real_named_context)) named_context + in + let idrefs = + List.map + (function x,_,_ -> idref_of_id (Names.string_of_id x)) named_context' in + let rel_context = Sign.push_named_to_rel_context named_context' [] in + let rel_env = + Environ.push_rel_context rel_context + (Environ.reset_with_named_context real_named_context env) in + let obj' = + Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in + let seed = ref 0 in + try + let annobj = + Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids + ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars rel_env + idrefs sigma (Unshare.unshare obj') None + in + Acic2Xml.print_term ids_to_inner_sorts annobj + with e -> + Util.anomaly + ("Problem during the conversion of constr into XML: " ^ + Printexc.to_string e) +(* CSC: debugging stuff +Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ; +Pp.ppnl (Pp.str "ENVIRONMENT:") ; +Pp.ppnl (Printer.pr_context_of rel_env) ; +Pp.ppnl (Pp.str "TERM:") ; +Pp.ppnl (Printer.prterm_env rel_env obj') ; +Pp.ppnl (Pp.str "RAW-TERM:") ; +Pp.ppnl (Printer.prterm obj') ; +Xml.xml_empty "MISSING TERM" [] (*; raise e*) +*) +;; + +let first_word s = + try let i = String.index s ' ' in + String.sub s 0 i + with _ -> s +;; + +let string_of_prim_rule x = match x with + | Proof_type.Intro _-> "Intro" + | Proof_type.Intro_replacing _-> "Intro_replacing" + | Proof_type.Cut (_,_,_) -> "Cut" + | Proof_type.FixRule (_,_,_) -> "FixRule" + | Proof_type.Cofix (_,_)-> "Cofix" + | Proof_type.Refine _ -> "Refine" + | Proof_type.Convert_concl _ -> "Convert_concl" + | Proof_type.Convert_hyp _->"Convert_hyp" + | Proof_type.Thin _ -> "Thin" + | Proof_type.ThinBody _-> "ThinBody" + | Proof_type.Move (_,_,_) -> "Move" + | Proof_type.Rename (_,_) -> "Rename" + + +let + print_proof_tree curi sigma0 pf proof_tree_to_constr + proof_tree_to_flattened_proof_tree constr_to_ids += + let module PT = Proof_type in + let module L = Logic in + let module X = Xml in + let module T = Tacexpr in + let ids_of_node node = + let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in +(* +let constr = + try + Proof2aproof.ProofTreeHash.find proof_tree_to_constr node + with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated +no lambda-term: ") (Refiner.print_script true (Evd.empty) +(Global.named_context ()) node)) ; assert false (* Closed bug, should not +happen any more *) +in +*) + try + Some (Acic.CicHash.find constr_to_ids constr) + with _ -> +Pp.ppnl (Pp.(++) (Pp.str +"The_generated_term_is_not_a_subterm_of_the_final_lambda_term") +(Printer.prterm constr)) ; + None + in + let rec aux node old_hyps = + let of_attribute = + match ids_of_node node with + None -> [] + | Some id -> ["of",id] + in + match node with + {PT.ref=Some(PT.Prim tactic_expr,nodes)} -> + let tac = string_of_prim_rule tactic_expr in + let of_attribute = ("name",tac)::of_attribute in + if nodes = [] then + X.xml_empty "Prim" of_attribute + else + X.xml_nempty "Prim" of_attribute + (List.fold_left + (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) + + | {PT.goal=goal; + PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} -> + (* [hidden_proof] is the proof of the tactic; *) + (* [nodes] are the proof of the subgoals generated by the tactic; *) + (* [flat_proof] if the proof-tree obtained substituting [nodes] *) + (* for the holes in [hidden_proof] *) + let flat_proof = + Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node + in begin + match tactic_expr with + | T.TacArg (T.Tacexp _) -> + (* We don't need to keep the level of abstraction introduced at *) + (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) + aux flat_proof old_hyps + | _ -> + (****** la tactique employee *) + let tac = std_ppcmds_to_string (Pptactic.pr_tactic tactic_expr) in + let tacname= first_word tac in + let of_attribute = ("name",tacname)::("script",tac)::of_attribute in + + (****** le but *) + let {Evd.evar_concl=concl; + Evd.evar_hyps=hyps}=goal in + + let rc = (Proof_trees.rc_of_gc sigma0 goal) in + let sigma = Proof_trees.get_gc rc in + let hyps = Proof_trees.get_hyps rc in + let env= Proof_trees.get_env rc in + + let xgoal = + X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in + + let rec build_hyps = + function + | [] -> xgoal + | (id,c,tid)::hyps1 -> + let id' = Names.string_of_id id in + [< build_hyps hyps1; + (X.xml_nempty "Hypothesis" + ["id",idref_of_id id' ; "name",id'] + (constr_to_xml tid sigma env)) + >] in + let old_names = List.map (fun (id,c,tid)->id) old_hyps in + let new_hyps = + List.filter (fun (id,c,tid)-> not (List.mem id old_names)) hyps in + + X.xml_nempty "Tactic" of_attribute + [<(build_hyps new_hyps) ; (aux flat_proof hyps)>] + end + + | {PT.ref=Some(PT.Change_evars,nodes)} -> + X.xml_nempty "Change_evars" of_attribute + (List.fold_left + (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) + + | {PT.ref=None;PT.goal=goal} -> + X.xml_empty "Open_goal" of_attribute + in + [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; + X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n"); + X.xml_nempty "ProofTree" ["of",curi] (aux pf []) + >] +;; diff --git a/contrib/xml/unshare.ml b/contrib/xml/unshare.ml new file mode 100644 index 0000000000..b9fcdb09f8 --- /dev/null +++ b/contrib/xml/unshare.ml @@ -0,0 +1,56 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(******************************************************************************) +(* *) +(* PROJECT MoWGLI *) +(* *) +(* Unsharing of 100% pure ocaml terms. *) +(* *) +(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* 11/04/2002 *) +(* *) +(******************************************************************************) + +exception CanNotUnshare;; + +(* [unshare t] gives back a copy of t where all sharing has been removed *) +(* Physical equality becomes meaningful on unshared terms. Hashtables that *) +(* use physical equality can now be used to associate information to evey *) +(* node of the term. *) +let unshare ?(already_unshared = function _ -> false) t = + let obj = Obj.repr t in + let rec aux obj = + if already_unshared (Obj.obj obj) then + obj + else + (if Obj.is_int obj then + obj + else if Obj.is_block obj then + begin + let tag = Obj.tag obj in + if tag < Obj.no_scan_tag then + begin + let size = Obj.size obj in + let new_obj = Obj.new_block 0 size in + Obj.set_tag new_obj tag ; + for i = 0 to size - 1 do + Obj.set_field new_obj i (aux (Obj.field obj i)) + done ; + new_obj + end + else if tag = Obj.string_tag then + obj + else + raise CanNotUnshare + end + else + raise CanNotUnshare + ) + in + Obj.obj (aux obj) +;; diff --git a/contrib/xml/unshare.mli b/contrib/xml/unshare.mli new file mode 100644 index 0000000000..211258d276 --- /dev/null +++ b/contrib/xml/unshare.mli @@ -0,0 +1,25 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(******************************************************************************) +(* *) +(* PROJECT MoWGLI *) +(* *) +(* Unsharing of 100% pure ocaml terms. *) +(* *) +(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* 11/04/2002 *) +(* *) +(******************************************************************************) + +exception CanNotUnshare;; + +(* [unshare t] gives back a copy of t where all sharing has been removed *) +(* Physical equality becomes meaningful on unshared terms. Hashtables that *) +(* use physical equality can now be used to associate information to evey *) +(* node of the term. *) +val unshare: ?already_unshared:('a -> bool) -> 'a -> 'a diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml new file mode 100644 index 0000000000..151d4582b9 --- /dev/null +++ b/contrib/xml/xmlcommand.ml @@ -0,0 +1,823 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT MoWGLI *) +(* *) +(* A module to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* 22/06/2002 *) +(* *) +(*****************************************************************************) + + +(* CONFIGURATION PARAMETERS *) + +(*CSC: was false*) +let verbose = ref true;; (* always set to true during a "Print XML All" *) + +(* UTILITY FUNCTIONS *) + +let print_if_verbose s = if !verbose then print_string s;; + +(* Next exception is used only inside print_coq_object and tag_of_string_tag *) +exception Uninteresting;; + +(*CSC: CODE USEFUL ONLY FOR THE CODE COMMENTED OUT +let tag_of_string_tag = + function + "CONSTANT" + | "PARAMETER" -> Constant + | "INDUCTIVE" -> Inductive + | "VARIABLE" -> Variable + | _ -> raise Uninteresting +;; +*) + +(* Internally, for Coq V7, params of inductive types are associated *) +(* not to the whole block of mutual inductive (as it was in V6) but to *) +(* each member of the block; but externally, all params are required *) +(* to be the same; the following function checks that the parameters *) +(* of each inductive of a same block are all the same, then returns *) +(* this number; it fails otherwise *) +let extract_nparams pack = + let module D = Declarations in + let module U = Util in + let module S = Sign in + + let {D.mind_nparams=nparams0} = pack.(0) in + let arity0 = pack.(0).D.mind_user_arity in + let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in + for i = 1 to Array.length pack - 1 do + let {D.mind_nparams=nparamsi} = pack.(i) in + let arityi = pack.(i).D.mind_user_arity in + let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in + if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block" + done; + nparams0 + +(* could_have_namesakes sp = true iff o is an object that could be cooked and *) +(* than that could exists in cooked form with the same name in a super *) +(* section of the actual section *) +let could_have_namesakes o sp = (* namesake = omonimo in italian *) + let module DK = Decl_kinds in + let module D = Declare in + let tag = Libobject.object_tag o in + print_if_verbose ("Object tag: " ^ tag ^ "\n") ; + match tag with + "CONSTANT" -> + (match D.constant_strength sp with + | DK.Local -> false (* a local definition *) + | DK.Global -> true (* a non-local one *) + ) + | "PARAMETER" (* axioms and *) + | "INDUCTIVE" -> true (* mutual inductive types are never local *) + | "VARIABLE" -> false (* variables are local, so no namesakes *) + | _ -> false (* uninteresting thing that won't be printed*) +;; + + +(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *) +(* ENVIRONMENT (= [(name1,l1); ...;(namen,ln)] WHERE li IS THE LIST *) +(* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT *) +(* SECTION, WHOSE PATH IS namei *) + +let pvars = + ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);; +let cumenv = ref Environ.empty_env;; + +(* filter_params pvars hyps *) +(* filters out from pvars (which is a list of lists) all the variables *) +(* that does not belong to hyps (which is a simple list) *) +(* It returns a list of couples relative section path -- list of *) +(* variable names. *) +let filter_params pvars hyps = + let rec aux ids = + function + [] -> [] + | (id,he)::tl -> + let ids' = id::ids in + let ids'' = + "cic:/" ^ + String.concat "/" (List.rev (List.map Names.string_of_id ids')) in + let he' = + ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in + let tl' = aux ids' tl in + match he' with + _,[] -> tl' + | _,_ -> he'::tl' + in + let cwd = Lib.cwd () in + let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in + let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in + aux (Names.repr_dirpath modulepath) (List.rev pvars) +;; + +type variables_type = + Definition of string * Term.constr * Term.types + | Assumption of string * Term.constr +;; + +let add_to_pvars x = + let module E = Environ in + let v = + match x with + Definition (v, bod, typ) -> + cumenv := + E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ; + v + | Assumption (v, typ) -> + cumenv := + E.push_named (Names.id_of_string v, None, typ) !cumenv ; + v + in + match !pvars with + [] -> assert false + | ((name,l)::tl) -> pvars := (name,v::l)::tl +;; + +(* The computation is very inefficient, but we can't do anything *) +(* better unless this function is reimplemented in the Declare *) +(* module. *) +let search_variables () = + let module N = Names in + let cwd = Lib.cwd () in + let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in + let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in + let rec aux = + function + [] -> [] + | he::tl as modules -> + let one_section_variables = + let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in + let t = List.map N.string_of_id (Declare.last_section_hyps dirpath) in + [he,t] + in + one_section_variables @ aux tl + in + aux + (Cic2acic.remove_module_dirpath_from_dirpath + ~basedir:modulepath cwd) +;; + +(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *) + +let body_filename_of_filename = + function + Some f -> Some (f ^ ".body") + | None -> None +;; + +let types_filename_of_filename = + function + Some f -> Some (f ^ ".types") + | None -> None +;; + +let prooftree_filename_of_filename = + function + Some f -> Some (f ^ ".proof_tree") + | None -> None +;; + +let print_object uri obj sigma proof_tree_infos filename = + (* function to pretty print and compress an XML file *) +(*CSC: Unix.system "gzip ..." is an orrible non-portable solution. *) + let pp xml filename = + Xml.pp xml filename ; + match filename with + None -> () + | Some fn -> + let fn' = + let rec escape s n = + try + let p = String.index_from s n '\'' in + String.sub s n (p - n) ^ "\\'" ^ escape s (p+1) + with Not_found -> String.sub s n (String.length s - n) + in + escape fn 0 + in + ignore (Unix.system ("gzip " ^ fn' ^ ".xml")) + in + let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) = + Cic2acic.acic_object_of_cic_object !pvars sigma obj in + let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in + let xmltypes = + Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in + pp xml filename ; + begin + match xml' with + None -> () + | Some xml' -> pp xml' (body_filename_of_filename filename) + end ; + pp xmltypes (types_filename_of_filename filename) ; + match proof_tree_infos with + None -> () + | Some (sigma0,proof_tree,proof_tree_to_constr, + proof_tree_to_flattened_proof_tree) -> + let xmlprooftree = + ProofTree2Xml.print_proof_tree + uri sigma0 proof_tree proof_tree_to_constr + proof_tree_to_flattened_proof_tree constr_to_ids + in + pp xmlprooftree (prooftree_filename_of_filename filename) +;; + +let string_list_of_named_context_list = + List.map + (function (n,_,_) -> Names.string_of_id n) +;; + +(* Function to collect the variables that occur in a term. *) +(* Used only for variables (since for constants and mutual *) +(* inductive types this information is already available. *) +let find_hyps t = + let module T = Term in + let rec aux l t = + match T.kind_of_term t with + T.Var id when not (List.mem id l) -> + let (_,bo,ty) = Global.lookup_named id in + let boids = + match bo with + Some bo' -> aux l bo' + | None -> l + in + id::(aux boids ty) + | T.Var _ + | T.Rel _ + | T.Meta _ + | T.Evar _ + | T.Sort _ -> l + | T.Cast (te,ty) -> aux (aux l te) ty + | T.Prod (_,s,t) -> aux (aux l s) t + | T.Lambda (_,s,t) -> aux (aux l s) t + | T.LetIn (_,s,_,t) -> aux (aux l s) t + | T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl + | T.Const con -> + let hyps = (Global.lookup_constant con).Declarations.const_hyps in + map_and_filter l hyps @ l + | T.Ind ind + | T.Construct (ind,_) -> + let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in + map_and_filter l hyps @ l + | T.Case (_,t1,t2,b) -> + Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b + | T.Fix (_,(_,tys,bodies)) + | T.CoFix (_,(_,tys,bodies)) -> + let r = Array.fold_left (fun i x -> aux i x) l tys in + Array.fold_left (fun i x -> aux i x) r bodies + and map_and_filter l = + function + [] -> [] + | (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl) + | _::tl -> map_and_filter l tl + in + aux [] t +;; + +(* Functions to construct an object *) + +let mk_variable_obj id body typ = + let hyps,unsharedbody = + match body with + None -> [],None + | Some bo -> find_hyps bo, Some (Unshare.unshare bo) + in + let hyps' = find_hyps typ @ hyps in + let hyps'' = List.map Names.string_of_id hyps' in + let variables = search_variables () in + let params = filter_params variables hyps'' in + Acic.Variable + (Names.string_of_id id, unsharedbody, + (Unshare.unshare (Term.body_of_type typ)), params) +;; + +(* Unsharing is not performed on the body, that must be already unshared. *) +(* The evar map and the type, instead, are unshared by this function. *) +let mk_current_proof_obj id bo ty evar_map env = + let unshared_ty = Unshare.unshare (Term.body_of_type ty) in + let metasenv = + List.map + (function + (n, {Evd.evar_concl = evar_concl ; + Evd.evar_hyps = evar_hyps} + ) -> + (* We map the named context to a rel context and every Var to a Rel *) + let final_var_ids,context = + let rec aux var_ids = + function + [] -> var_ids,[] + | (n,None,t)::tl -> + let final_var_ids,tl' = aux (n::var_ids) tl in + let t' = Term.subst_vars var_ids t in + final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl' + | (n,Some b,t)::tl -> + let final_var_ids,tl' = aux (n::var_ids) tl in + let b' = Term.subst_vars var_ids b in + (* t will not be exported to XML. Thus no unsharing performed *) + final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl' + in + aux [] (List.rev evar_hyps) + in + (* We map the named context to a rel context and every Var to a Rel *) + (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl)) + ) (Evd.non_instantiated evar_map) + in + let id' = Names.string_of_id id in + if metasenv = [] then + let ids = + Names.Idset.union + (Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in + let hyps0 = Environ.keep_hyps env ids in + let hyps = string_list_of_named_context_list hyps0 in + (* Variables are the identifiers of the variables in scope *) + let variables = search_variables () in + let params = filter_params variables hyps in + Acic.Constant (id',Some bo,unshared_ty,params) + else + Acic.CurrentProof (id',metasenv,bo,unshared_ty) +;; + +let mk_constant_obj id bo ty variables hyps = + let hyps = string_list_of_named_context_list hyps in + let ty = Unshare.unshare (Term.body_of_type ty) in + let params = filter_params variables hyps in + match bo with + None -> + Acic.Constant (Names.string_of_id id,None,ty,params) + | Some c -> + Acic.Constant + (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)), + ty,params) +;; + +let mk_inductive_obj sp packs variables hyps finite = + let module D = Declarations in + let hyps = string_list_of_named_context_list hyps in + let params = filter_params variables hyps in + let nparams = extract_nparams packs in + let tys = + let tyno = ref (Array.length packs) in + Array.fold_right + (fun p i -> + decr tyno ; + let {D.mind_consnames=consnames ; + D.mind_typename=typename ; + D.mind_nf_arity=arity} = p + in + let lc = Inductive.arities_of_constructors (Global.env ()) (sp,!tyno) in + let cons = + (Array.fold_right (fun (name,lc) i -> (name,lc)::i) + (Array.mapi + (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames) + [] + ) + in + (typename,finite,Unshare.unshare arity,cons)::i + ) packs [] + in + Acic.InductiveDefinition (tys,params,nparams) +;; + +(* 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 (_,qid as locqid) fn = + let module D = Declarations in + let module De = Declare in + let module G = Global in + let module N = Names in + let module Nt = Nametab in + let module T = Term in + let module X = Xml in + let module Ln = Libnames in + let (_,id) = Libnames.repr_qualid qid in + let glob_ref = +(*CSC: ask Hugo why Nametab.global does not work with variables and *) +(*CSC: we have to do this hugly try ... with *) + try + Nt.global locqid + with + _ -> let (_,id) = Ln.repr_qualid qid in Ln.VarRef id + in + (* Variables are the identifiers of the variables in scope *) + let variables = search_variables () in + let keep_sections,kn,tag,obj = + match glob_ref with + Ln.VarRef id -> + let sp = Declare.find_section_variable id in + (* this kn is fake since it is not provided by Coq *) + let kn = + let (mod_path,dir_path) = Lib.current_prefix () in + N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp)) + in + let (_,body,typ) = G.lookup_named id in + true,kn,Cic2acic.Variable,mk_variable_obj id body typ + | Ln.ConstRef kn -> + let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = + G.lookup_constant kn in + false,kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps + | Ln.IndRef (kn,_) -> + let {D.mind_packets=packs ; + D.mind_hyps=hyps; + D.mind_finite=finite} = G.lookup_mind kn in + false,kn,Cic2acic.Inductive, + mk_inductive_obj kn packs variables hyps finite + | Ln.ConstructRef _ -> + Util.anomaly ("print: this should not happen") + in + print_object (Cic2acic.uri_of_kernel_name ~keep_sections kn tag) obj + Evd.empty None 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 fn pftst id = + let str = Names.string_of_id id in + let pf = Tacmach.proof_of_pftreestate pftst in + let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in + let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree, + unshared_pf + = + Proof2aproof.extract_open_pftreestate pftst in + let kn = Lib.make_kn id in + let env = Global.env () in + let obj = mk_current_proof_obj id val0 typ evar_map env in + print_object (Cic2acic.uri_of_kernel_name kn Cic2acic.Constant) obj evar_map + (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr, + proof_tree_to_flattened_proof_tree)) fn +;; + +let show fn = + let pftst = Pfedit.get_pftreestate () in + let id = Pfedit.get_current_proof_name () in + show_pftreestate fn pftst id +;; + +(* +(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *) + +(* list of (name, uncooked sp, most cooked sp, uncooked leaf object, *) +(* list of possible variables, directory name) *) +(* used to collect informations on the uncooked and most cooked forms *) +(* of objects that could be cooked (have namesakes) *) +let printed = ref [];; + +(* makes a filename from a directory name, a section path and an extension *) +let mkfilename dn sp ext = +(*CSC: + let dir_list_of_dirpath s = + let rec aux n = + try + let pos = String.index_from s n '/' in + let head = String.sub s n (pos - n) in + head::(aux (pos + 1)) + with + Not_found -> [String.sub s n (String.length s - n)] + in + aux 0 + in + let rec join_dirs cwd = + function + [] -> assert false + | [he] -> "/" ^ he + | he::tail -> + let newcwd = cwd ^ "/" ^ he in + (try + Unix.mkdir newcwd 0o775 + with _ -> () (* Let's ignore the errors on mkdir *) + ) ; + "/" ^ he ^ join_dirs newcwd tail + in + let module L = Library in + let module S = System in + let module N = Names in + let module No = Nameops in + match dn with + None -> None + | Some basedir -> + let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in + let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in + Some (basedir ^ join_dirs basedir dir ^ "." ^ ext) +*) match dn with None -> None | Some _ -> Some "/tmp/nonloso" +;; + +(* print_coq_object leaf_object id section_path directory_name formal_vars *) +(* where leaf_object is a leaf object *) +(* and id is the identifier (name) of the definition/theorem *) +(* or of the inductive definition o *) +(* and section_path is the section path of o *) +(* and directory_name is the base directory in which putting the print *) +(* and formal_vars is the list of parameters (variables) of o *) +(* pretty prints via Xml.pp the object o in the right directory deduced *) +(* from directory_name and section_path *) +(* Note: it is printed only the uncooked available form of the object plus *) +(* the list of parameters of the object deduced from it's most cooked *) +(* form *) +let print_coq_object lobj id sp dn fv env = + let module D = Declarations in + let module E = Environ in + let module G = Global in + let module N = Names in + let module T = Term in + let module X = Xml in +(*CSC: GROSSO BUG: env e' l'environment cumulativo in cui aggiungiamo passo passo tutte le variabili. Qui, invece, non lo stiamo piu' usando per nulla. Quindi la prima variabile che incontreremo non verra' trovata ;-(((( Direi che l'environment vada passato fino alla print_object che a sua volta lo passera' a chi di dovere (ovvero sia a Cic2Acic che a DoubleTypeInference *) + let strtag = Libobject.object_tag lobj in + try + let tag = tag_of_string_tag strtag in + let obj = + match strtag with + "CONSTANT" (* = Definition, Theorem *) + | "PARAMETER" (* = Axiom *) -> + let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = + G.lookup_constant sp + in + mk_constant_obj id val0 typ fv hyps + | "INDUCTIVE" -> + let + {D.mind_packets=packs ; + D.mind_hyps = hyps; + D.mind_finite = finite + } = G.lookup_mind sp + in + mk_inductive_obj sp packs fv hyps finite + | "VARIABLE" -> + let (_,(_,varentry,_)) = Declare.out_variable lobj in + begin + match varentry with + Declare.SectionLocalDef (body,optt,opaq) -> + let typ = match optt with + | None -> Retyping.get_type_of env Evd.empty body + | Some t -> t in + add_to_pvars (Definition (N.string_of_id id, body, typ)) ; + mk_variable_obj id (Some body) typ + | Declare.SectionLocalAssum typ -> + add_to_pvars (Assumption (N.string_of_id id, typ)) ; + mk_variable_obj id None (T.body_of_type typ) + end + | "CLASS" + | "COERCION" + | _ -> raise Uninteresting + in + let fileext () = ext_of_tag tag in + let fn = mkfilename dn sp (fileext ()) in + print_object (uri_of_path sp tag) obj Evd.empty None fn + with + Uninteresting -> () +;; + +(* print_library_segment state bprintleaf directory_name *) +(* where state is a list of (section-path, node) *) +(* and bprintleaf is true iff the leaf objects should be printed *) +(* and directory_name is the name of the base directory in which to print *) +(* the files *) +(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state *) +let rec print_library_segment state bprintleaf dn = + List.iter + (function (sp, node) -> + print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ; + print_node node (Nameops.basename sp) sp bprintleaf dn ; + print_if_verbose "\n" + ) (List.rev state) +(* print_node node id section_path bprintleaf directory_name *) +(* prints a single node (and all it's subnodes via print_library_segment *) +and print_node n id sp bprintleaf dn = + let module L = Lib in + match n with + L.Leaf o -> + print_if_verbose "LEAF\n" ; + if bprintleaf then + begin + if not (List.mem id !printed) then + (* this is an uncooked term or a local (with no namesakes) term *) + begin +(*CSC: pezza quando i .vo sono magri +try +*) + if could_have_namesakes o sp then + begin + (* this is an uncooked term *) + print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ; + print_coq_object o id sp dn !pvars !cumenv ; + printed := id::!printed + end + else + begin + (* this is a local term *) + print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ; + print_coq_object o id sp dn !pvars !cumenv + end +(*CSC: pezza quando i .vo sono magri +with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n"); +*) + end + else + begin + (* update the least cooked sp *) + print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n") + end + end + | L.OpenedSection (dir,_) -> + let id = snd (Nameops.split_dirpath dir) in + print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n") + | L.ClosedSection (_,dir,state) -> + let id = snd (Nameops.split_dirpath dir) in + print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ; + if bprintleaf then + begin + (* open a new scope *) + let (_,section_name) = Nameops.split_dirpath dir in + pvars := (section_name,[])::!pvars ; + print_library_segment state bprintleaf dn ; + (* close the scope *) + match !pvars with + [] -> assert false + | he::tl -> pvars := tl + end ; + print_if_verbose "/ClosedDir\n" + | L.Module s -> + print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n") + | L.FrozenState _ -> + print_if_verbose ("FrozenState\n") +;; + +(* print_closed_section module_name node directory_name *) +(* where module_name is the name of a module *) +(* and node is the library segment of the module *) +(* and directory_name is the base directory in which to put the xml files *) +(* prints all the leaf objects of the tree rooted in node using *) +(* print_library_segment on all its sons *) +let print_closed_section s ls dn = + let module L = Lib in + printed := [] ; + pvars := [Names.id_of_string "",[]] ; + cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ; + print_if_verbose ("Module " ^ s ^ ":\n") ; + print_library_segment ls true dn ; + print_if_verbose "\n/Module\n" ; +;; + +(* printModule identifier directory_name *) +(* where identifier is the name of a module (section) d *) +(* and directory_name is the directory in which to root all the xml files *) +(* prints all the xml files and directories corresponding to the subsections *) +(* and terms of the module d *) +(* Note: the terms are printed in their uncooked form plus the informations *) +(* on the parameters of their most cooked form *) +let printModule (loc,qid) dn = + let module L = Library in + let module N = Nametab in + let module X = Xml in + + let (_,dir_path,_) = L.locate_qualified_library qid in + + let str = N.string_of_qualid qid in + let ls = L.module_segment (Some dir_path) in + print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ + (L.module_full_filename dir_path) ^ "\n") ; + print_closed_section str (List.rev ls) dn ; + print_if_verbose ("MODULE_END " ^ str ^ " " ^ + (L.module_full_filename dir_path) ^ "\n") +;; + +(* printSection identifier directory_name *) +(* where identifier is the name of a closed section d *) +(* and directory_name is the directory in which to root all the xml files *) +(* prints all the xml files and directories corresponding to the subsections *) +(* and terms of the closed section d *) +(* Note: the terms are printed in their uncooked form plus the informations *) +(* on the parameters of their most cooked form *) +let printSection id dn = + let module L = Library in + let module N = Names in + let module No = Nameops in + let module X = Xml in + let sp = Lib.make_path id in + let ls = + let rec find_closed_section = + function + [] -> raise Not_found + | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id + -> ls + | _::t -> find_closed_section t + in + print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ; + find_closed_section (Lib.contents_after None) + in + let str = N.string_of_id id in + print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n"); + print_closed_section str ls dn ; + print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n") +;; + +(* print All () prints what is the structure of the current environment of *) +(* Coq. No terms are printed. Useful only for debugging *) +let printAll () = + let state = Library.module_segment None in + let oldverbose = !verbose in + verbose := true ; + print_library_segment state false None ; +(* + let ml = Library.loaded_modules () in + List.iter (function i -> printModule (Names.id_of_string i) None) ml ; +*) + verbose := oldverbose +;; +*) + + +let rec join_dirs cwd = + function + [] -> assert false + | [he] -> cwd ^ "/" ^ he + | he::tail -> + let newcwd = cwd ^ "/" ^ he in + (try + Unix.mkdir newcwd 0o775 + with _ -> () (* Let's ignore the errors on mkdir *) + ) ; + join_dirs newcwd tail +;; + +let filename_of_path ?(keep_sections=false) xml_library_root kn tag = + let module N = Names in + match xml_library_root with + None -> None (* stdout *) + | Some xml_library_root' -> + let tokens = Cic2acic.token_list_of_kernel_name ~keep_sections kn tag in + Some (join_dirs xml_library_root' tokens) +;; + +(*CSC: Ask Hugo for a better solution *) +let qualid_of_kernel_name kn = + let module N = Names in + let (modpath,_,label) = N.repr_kn kn in + match modpath with + N.MPself _ -> Libnames.make_qualid (Lib.cwd ()) (N.id_of_label label) + | _ -> + Util.anomaly ("qualid_of_kernel_name: the module path is not MPself") +;; + +(* Let's register the callbacks *) +let xml_library_root = + try + Some (Sys.getenv "COQ_XML_LIBRARY_ROOT") + with Not_found -> None +;; + +let proof_to_export = ref None (* holds the proof-tree to export *) +;; + +let _ = + Pfedit.set_xml_cook_proof + (function pftreestate -> proof_to_export := Some pftreestate) +;; + +let _ = + Declare.set_xml_declare_variable + (function kn -> + let filename = + filename_of_path ~keep_sections:true xml_library_root kn + Cic2acic.Variable in + let qualid = qualid_of_kernel_name kn in + let dummy_location = -1,-1 in + print (dummy_location,qualid) filename) +;; + +let _ = + Declare.set_xml_declare_constant + (function kn -> + let filename = filename_of_path xml_library_root kn Cic2acic.Constant in + let qualid = qualid_of_kernel_name kn in + match !proof_to_export with + None -> + let dummy_location = -1,-1 in + print (dummy_location,qualid) filename + | 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. *) + show_pftreestate filename pftreestate + (Names.id_of_label (Names.label kn)) ; + proof_to_export := None) +;; + +let _ = + Declare.set_xml_declare_inductive + (function kn -> + let filename = filename_of_path xml_library_root kn Cic2acic.Inductive in + let qualid = qualid_of_kernel_name kn in + let dummy_location = -1,-1 in + print (dummy_location,qualid) filename) +;; diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 485bb93c27..4690e21c19 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -35,6 +35,7 @@ val print : Libnames.qualid Util.located -> string option -> unit (* pretty prints via Xml.pp the proof in progress on dest *) val show : string option -> unit +(*CSC: untested, no more working or semantics unclear (* print All () prints what is the structure of the current environment of *) (* Coq. No terms are printed. Useful only for debugging *) val printAll : unit -> unit @@ -56,3 +57,4 @@ val printLibrary : Libnames.qualid Util.located -> string option -> unit (* Note: the terms are printed in their uncooked form plus the informations *) (* on the parameters of their most cooked form *) val printSection : Names.identifier -> string option -> unit +*) diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index 876da02e2e..fbb9944d37 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -85,6 +85,7 @@ VERNAC COMMAND EXTEND Xml | [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] +(* | [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ] | [ "Print" "XML" "Module" diskname(dn) qualid(id) ] -> @@ -92,6 +93,7 @@ VERNAC COMMAND EXTEND Xml | [ "Print" "XML" "Section" diskname(dn) ident(id) ] -> [ Xmlcommand.printSection id dn ] +*) END (* vinterp_add "Print" |