--- /dev/null
+
+(* 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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+ dtdname ^ "\">\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 [< >]
+ >]
+ >]
+;;
--- /dev/null
+(* 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 ;
+ | _ -> ()
+;;
--- /dev/null
+(* 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();;
projects / helm.git / commitdiff