From: Claudio Sacerdoti Coen Date: Tue, 27 Nov 2001 17:28:57 +0000 (+0000) Subject: First version of fix_params into CVS. X-Git-Tag: mlminidom_0_2_2~50 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=02c3583e17631f04375a185af5d7b49698cd3d24;p=helm.git First version of fix_params into CVS. --- diff --git a/helm/fix_params/.cvsignore b/helm/fix_params/.cvsignore new file mode 100644 index 000000000..7335d1661 --- /dev/null +++ b/helm/fix_params/.cvsignore @@ -0,0 +1 @@ +*.cm[iox] *.o fix_params fix_params.opt diff --git a/helm/fix_params/.depend b/helm/fix_params/.depend new file mode 100644 index 000000000..152053f35 --- /dev/null +++ b/helm/fix_params/.depend @@ -0,0 +1,2 @@ +fix_params.cmo: cicFindParameters.cmo +fix_params.cmx: cicFindParameters.cmx diff --git a/helm/fix_params/Makefile b/helm/fix_params/Makefile new file mode 100644 index 000000000..24f3d4860 --- /dev/null +++ b/helm/fix_params/Makefile @@ -0,0 +1,38 @@ +REQUIRES = helm-getter helm-cic_cache helm-xml +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLDEP = ocamldep +OCAMLFIND = ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) + +all: fix_params +opt: fix_params.opt + +DEPOBJS = cic2Xml.ml cicFindParameters.ml fix_params.ml + +FIXPARAMSOBJS = cic2Xml.cmo cicFindParameters.cmo fix_params.cmo + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +fix_params: $(FIXPARAMSOBJS) + $(OCAMLC) -linkpkg -o fix_params $(FIXPARAMSOBJS) + +fix_params.opt: $(FIXPARAMSOBJS:.cmo=.cmx) + $(OCAMLOPT) -linkpkg -o fix_params.opt $(FIXPARAMSOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] *.o fix_params fix_params.opt + +.PHONY: clean + +include .depend diff --git a/helm/fix_params/cic2Xml.ml b/helm/fix_params/cic2Xml.ml new file mode 100644 index 000000000..58f35bb6f --- /dev/null +++ b/helm/fix_params/cic2Xml.ml @@ -0,0 +1,255 @@ + +(* 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;; +exception BinderNotSpecified;; + +let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";; + +(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +let print_term curi = + let rec aux = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + function + C.ARel (id,_,n,Some b) -> + X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id] + | C.ARel _ -> raise BinderNotSpecified + | C.AVar (id,_,uri) -> + let vdepth = U.depth_of_uri uri + and cdepth = U.depth_of_uri curi in + X.xml_empty "VAR" + ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^ + (U.name_of_uri uri) ; + "id",id] + | C.AMeta (id,_,n) -> + X.xml_empty "META" ["no",(string_of_int n) ; "id",id] + | C.ASort (id,_,s) -> + let string_of_sort = + function + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type -> "Type" + in + X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] + | C.AImplicit _ -> raise NotImplemented + | C.AProd (id,_,C.Anonimous,s,t) -> + X.xml_nempty "PROD" ["id",id] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] + | C.AProd (xid,_,C.Name id,s,t) -> + X.xml_nempty "PROD" ["id",xid] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] + | C.ACast (id,_,v,t) -> + X.xml_nempty "CAST" ["id",id] + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] + | C.ALambda (id,_,C.Anonimous,s,t) -> + X.xml_nempty "LAMBDA" ["id",id] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] + | C.ALambda (xid,_,C.Name id,s,t) -> + X.xml_nempty "LAMBDA" ["id",xid] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] + | C.ALetIn (xid,_,C.Anonimous,s,t) -> + assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*) + | C.ALetIn (xid,_,C.Name id,s,t) -> + X.xml_nempty "LETIN" ["id",xid] + [< X.xml_nempty "term" [] (aux s) ; + X.xml_nempty "letintarget" ["binder",id] (aux t) + >] + | C.AAppl (id,_,li) -> + X.xml_nempty "APPLY" ["id",id] + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) + >] + | C.AConst (id,_,uri,_) -> + X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id] + | C.AAbst (id,_,uri) -> raise NotImplemented + | C.AMutInd (id,_,uri,_,i) -> + X.xml_empty "MUTIND" + ["uri", (U.string_of_uri uri) ; + "noType",(string_of_int i) ; + "id",id] + | C.AMutConstruct (id,_,uri,_,i,j) -> + X.xml_empty "MUTCONSTRUCT" + ["uri", (U.string_of_uri uri) ; + "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; + "id",id] + | C.AMutCase (id,_,uri,_,typeno,ty,te,patterns) -> + X.xml_nempty "MUTCASE" + ["uriType",(U.string_of_uri uri) ; + "noType", (string_of_int typeno) ; + "id", id] + [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; + X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; + List.fold_right + (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) + patterns [<>] + >] + | C.AFix (id, _, no, funs) -> + X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id] + [< List.fold_right + (fun (fi,ai,ti,bi) i -> + [< X.xml_nempty "FixFunction" + ["name", fi; "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + | C.ACoFix (id,_,no,funs) -> + X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id] + [< List.fold_right + (fun (fi,ti,bi) i -> + [< X.xml_nempty "CofixFunction" ["name", fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + in + aux +;; + +let encode params = + List.fold_right + (fun (n,l) i -> + match l with + [] -> i + | _ -> + string_of_int n ^ ": " ^ + String.concat " " (List.map UriManager.name_of_uri l) ^ + i + ) params "" +;; + +let print_mutual_inductive_type curi (typename,inductive,arity,constructors) = + let module C = Cic in + let module X = Xml in + [< X.xml_nempty "InductiveType" + ["name",typename ; + "inductive",(string_of_bool inductive) + ] + [< X.xml_nempty "arity" [] (print_term curi arity) ; + (List.fold_right + (fun (name,ty,_) i -> + [< X.xml_nempty "Constructor" ["name",name] + (print_term curi ty) ; + i + >]) + constructors + [<>] + ) + >] + >] +;; + +let pp obj curi = + let module C = Cic in + let module X = Xml in + match obj with + C.ADefinition (xid, _, id, te, ty, params) -> + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Definition" + (["name", id ; "id",xid] @ + match params with + C.Possible _ -> raise ImpossiblePossible + (*CSC params are kept in inverted order in the internal *) + (* representation (the order of application) *) + | C.Actual fv' -> ["params",(encode (List.rev fv'))]) + [< X.xml_nempty "body" [] (print_term curi te) ; + X.xml_nempty "type" [] (print_term curi ty) >] + >] + | C.AAxiom (xid, _, id, ty, params) -> + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Axiom" + (*CSC params are kept in inverted order in the internal *) + (* representation (the order of application) *) + ["name",id ; "params",(encode (List.rev params)) ; "id",xid] + [< X.xml_nempty "type" [] (print_term curi ty) >] + >] + | C.AVariable (xid, _, name, bo, ty) -> + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Variable" ["name",name ; "id",xid] + [< (match bo with + None -> [<>] + | Some bo -> X.xml_nempty "body" [] (print_term curi bo) + ) ; + X.xml_nempty "type" [] (print_term curi ty) + >] + >] + | C.ACurrentProof (xid, _, name, conjs, bo, ty) -> + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n"); + X.xml_nempty "CurrentProof" ["name",name ; "id",xid] + [< List.fold_right + (fun (j,t) i -> + [< X.xml_nempty "Conjecture" ["no",(string_of_int j)] + [< print_term curi t >] ; i >]) + conjs [<>] ; + X.xml_nempty "body" [] [< print_term curi bo >] ; + X.xml_nempty "type" [] [< print_term curi ty >] + >] + >] + | C.AInductiveDefinition (xid, _, tys, params, paramsno) -> + let names = + List.map + (fun (typename,_,_,_) -> typename) + tys + in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "InductiveDefinition" + (*CSC params are kept in inverted order in the internal *) + (* representation (the order of application) *) + ["noParams",string_of_int paramsno ; + "params",(encode (List.rev params)) ; + "id",xid] + [< List.fold_right + (fun x i -> [< print_mutual_inductive_type curi x ; i >]) + tys [< >] + >] + >] +;; diff --git a/helm/fix_params/cicFindParameters.ml b/helm/fix_params/cicFindParameters.ml new file mode 100644 index 000000000..03c3e1c85 --- /dev/null +++ b/helm/fix_params/cicFindParameters.ml @@ -0,0 +1,158 @@ +(* 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/. + *) + +exception WrongUriToConstant;; +exception WrongUriToInductiveDefinition;; +exception CircularDependency of string;; + +module OrderedUris = + struct + type t = UriManager.uri + let compare (s1 : t) (s2 : t) = + (* library function for = *) + compare s1 s2 + (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*) + end +;; + +let filename_of_uri uri = + let uri' = UriManager.string_of_uri uri in + let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in + fn ^ ".xml" +;; + +(* quite inefficient coding of a set of strings: the only operations *) +(* performed are mem O(log n), and union O(n * log n?) *) +(* Perhaps a better implementation would be an array of bits or a map *) +(* from uri to booleans *) +module SetOfUris = Set.Make(OrderedUris);; + +let (@@) = SetOfUris.union;; + +let rec parameters_of te ty pparams= + let module S = SetOfUris in + let module C = Cic in + let rec aux = + function + C.Rel _ -> S.empty + | C.Var uri -> S.singleton uri + | C.Meta _ -> S.empty + | C.Sort _ -> S.empty + | C.Implicit -> S.empty + | C.Cast (te, ty) -> aux te @@ aux ty + | C.Prod (_, s, t) -> aux s @@ aux t + | C.Lambda (_, s, t) -> aux s @@ aux t + | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty + | C.Const (uri,_) -> + (* the parameters could be not exact but only possible *) + fix_params uri (Some (filename_of_uri uri)) ; + (* now the parameters are surely possible *) + (match CicCache.get_obj uri with + C.Definition (_, _, _, params) -> + List.fold_right + (fun (_,l) i -> + List.fold_right + (fun x i -> S.singleton x @@ i) l i + ) params S.empty + | C.Axiom (_, _, params) -> + List.fold_right + (fun (_,l) i -> + List.fold_right + (fun x i -> S.singleton x @@ i) l i + ) params S.empty + | C.CurrentProof _ -> S.empty (*CSC wrong *) + | _ -> raise WrongUriToConstant + ) + | C.Abst _ -> S.empty + | C.MutInd (uri,_,_) -> + (match CicCache.get_obj uri with + C.InductiveDefinition (_, params, _) -> + List.fold_right + (fun (_,l) i -> + List.fold_right + (fun x i -> S.singleton x @@ i) l i + ) params S.empty + | _ -> raise WrongUriToInductiveDefinition + ) + | C.MutConstruct (uri,_,_,_) -> + (match CicCache.get_obj uri with + C.InductiveDefinition (_, params, _) -> + List.fold_right + (fun (_,l) i -> + List.fold_right + (fun x i -> S.singleton x @@ i) l i + ) params S.empty + | _ -> raise WrongUriToInductiveDefinition + ) + | C.MutCase (uri,_,_,outtype,term,patterns) -> + (*CSC cosa basta? Ci vuole anche uri? *) + (match CicCache.get_obj uri with + C.InductiveDefinition (_, params, _) -> + List.fold_right + (fun (_,l) i -> + List.fold_right + (fun x i -> S.singleton x @@ i) l i + ) params S.empty + | _ -> raise WrongUriToInductiveDefinition + ) @@ aux outtype @@ aux term @@ + List.fold_right (fun x i -> aux x @@ i) patterns S.empty + | C.Fix (_,fl) -> + List.fold_right + (fun (_,_,ty,bo) i -> aux ty @@ aux bo @@ i) + fl S.empty + | C.CoFix (_,fl) -> + List.fold_right + (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i) + fl S.empty + in + let actual_params = aux te @@ aux ty in + (* sort_actual_params wants in input the ordered list of possible params *) + let rec sort_actual_params2 = + function + [] -> [] + | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl) + | _::tl -> sort_actual_params2 tl + in + let rec sort_actual_params = + function + [] -> [] + | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl) + in + sort_actual_params pparams + +and fix_params uri filename = + let module C = Cic in + let ann = CicCache.get_annobj uri in + match ann with + C.ADefinition (xid, ann, id, te, ty, C.Possible pparams) -> + let te' = Deannotate.deannotate_term te in + let ty' = Deannotate.deannotate_term ty in + let real_params = parameters_of te' ty' pparams in + let fixed = + C.ADefinition (xid,ann,id,te,ty,C.Actual real_params) + in + Xml.pp (Cic2Xml.pp fixed uri) filename ; + | _ -> () +;; diff --git a/helm/fix_params/fix_params.ml b/helm/fix_params/fix_params.ml new file mode 100644 index 000000000..f1edf091a --- /dev/null +++ b/helm/fix_params/fix_params.ml @@ -0,0 +1,74 @@ +(* 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/. + *) + +let read_from_stdin = ref false;; + +let uri_of_filename fn = + let uri = + Str.replace_first (Str.regexp (Str.quote Configuration.helm_dir)) "cic:" fn + in + let uri' = Str.replace_first (Str.regexp "\.xml$") "" uri in + UriManager.uri_of_string uri' +;; + +let main() = + Deannotate.expect_possible_parameters := true ; + let files = ref [] in + Arg.parse + ["-stdin", Arg.Set read_from_stdin, "Read from stdin"] + (fun x -> files := (x, uri_of_filename x) :: !files) + " +usage: experiment file ... + +List of options:"; + if !read_from_stdin then + begin + try + while true do + let l = Str.split (Str.regexp " ") (read_line ()) in + List.iter (fun x -> files := (x, uri_of_filename x) :: !files) l + done + with + End_of_file -> () + end ; + files := List.rev !files; + Getter.update () ; + print_endline "ATTENTION: have you changed servers.txt so that you'll try \ + to repair your own objs instead of others'?" ; + flush stdout ; + List.iter + (function (fn, uri) -> + print_string (UriManager.string_of_uri uri) ; + flush stdout ; + (try + CicFindParameters.fix_params uri (Some fn) + with + e -> print_newline () ; flush stdout ; raise e ) ; + print_endline " OK!" ; + flush stdout + ) !files +;; + +main();;