X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;fp=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=d945cc82f63d54b2e931424c625dacd9707ba383;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml deleted file mode 100644 index d945cc82f..000000000 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ /dev/null @@ -1,435 +0,0 @@ -(* 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 ~ask_dtd_to_the_getter dtd = - if ask_dtd_to_the_getter then - Configuration.getter_url ^ "getdtd?uri=" ^ dtd - else - "http://mowgli.cs.unibo.it/dtd/" ^ dtd -;; - -let param_attribute_of_params params = - String.concat " " (List.map UriManager.string_of_uri params) -;; - -(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -let print_term ~ids_to_inner_sorts = - let rec aux = - let module C = Cic in - let module X = Xml in - let module U = UriManager in - function - C.ARel (id,idref,n,b) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_empty "REL" - [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; - None,"idref",idref ; None,"sort",sort] - | C.AVar (id,uri,exp_named_subst) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - aux_subst uri - (X.xml_empty "VAR" - [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort]) - exp_named_subst - | C.AMeta (id,n,l) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" - [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort] - (List.fold_left - (fun i t -> - match t with - Some t' -> - [< i ; X.xml_nempty "substitution" [] (aux t') >] - | None -> - [< i ; X.xml_empty "substitution" [] >] - ) [< >] l) - | C.ASort (id,s) -> - let string_of_sort = - function - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type -> "Type" - in - X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id] - | C.AImplicit _ -> raise NotImplemented - | C.AProd (last_id,_,_,_) as prods -> - let rec eat_prods = - function - C.AProd (id,n,s,t) -> - let prods,t' = eat_prods t in - (id,n,s)::prods,t' - | t -> [],t - in - let prods,t = eat_prods prods in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "PROD" [None,"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 = - (None,"id",id)::(None,"type",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] - in - [< i ; X.xml_nempty "decl" attrs (aux s) >] - ) [< >] prods ; - X.xml_nempty "target" [] (aux t) - >] - | C.ACast (id,v,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] - [< X.xml_nempty "term" [] (aux v) ; - X.xml_nempty "type" [] (aux t) - >] - | C.ALambda (last_id,_,_,_) as lambdas -> - let rec eat_lambdas = - function - C.ALambda (id,n,s,t) -> - let lambdas,t' = eat_lambdas t in - (id,n,s)::lambdas,t' - | t -> [],t - in - let lambdas,t = eat_lambdas lambdas in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LAMBDA" [None,"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 = - (None,"id",id)::(None,"type",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] - in - [< i ; X.xml_nempty "decl" attrs (aux s) >] - ) [< >] lambdas ; - X.xml_nempty "target" [] (aux t) - >] - | C.ALetIn (xid,C.Anonymous,s,t) -> - assert false - | C.ALetIn (last_id,C.Name _,_,_) as letins -> - let rec eat_letins = - function - C.ALetIn (id,n,s,t) -> - let letins,t' = eat_letins t in - (id,n,s)::letins,t' - | t -> [],t - in - let letins,t = eat_letins letins in - let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LETIN" [None,"sort",sort] - [< List.fold_left - (fun i (id,binder,s) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - let attrs = - (None,"id",id)::(None,"sort",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] - in - [< i ; X.xml_nempty "def" attrs (aux s) >] - ) [< >] letins ; - X.xml_nempty "target" [] (aux t) - >] - | C.AAppl (id,li) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort] - [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) - >] - | C.AConst (id,uri,exp_named_subst) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - aux_subst uri - (X.xml_empty "CONST" - [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] - ) exp_named_subst - | C.AMutInd (id,uri,i,exp_named_subst) -> - aux_subst uri - (X.xml_empty "MUTIND" - [None, "uri", (U.string_of_uri uri) ; - None, "noType", (string_of_int i) ; - None, "id", id] - ) exp_named_subst - | C.AMutConstruct (id,uri,i,j,exp_named_subst) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - aux_subst uri - (X.xml_empty "MUTCONSTRUCT" - [None,"uri", (U.string_of_uri uri) ; - None,"noType",(string_of_int i) ; - None,"noConstr",(string_of_int j) ; - None,"id",id ; None,"sort",sort] - ) exp_named_subst - | C.AMutCase (id,uri,typeno,ty,te,patterns) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "MUTCASE" - [None,"uriType",(U.string_of_uri uri) ; - None,"noType", (string_of_int typeno) ; - None,"id", id ; None,"sort",sort] - [< 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) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "FIX" - [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] - [< List.fold_right - (fun (id,fi,ai,ti,bi) i -> - [< X.xml_nempty "FixFunction" - [None,"id",id ; None,"name", fi ; - None,"recIndex", (string_of_int ai)] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] ; - i - >] - ) funs [<>] - >] - | C.ACoFix (id,no,funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "COFIX" - [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] - [< List.fold_right - (fun (id,fi,ti,bi) i -> - [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] ; - i - >] - ) funs [<>] - >] - and aux_subst buri target subst = -(*CSC: I have now no way to assign an ID to the explicit named substitution *) - let id = None in - if subst = [] then - target - else - Xml.xml_nempty "instantiate" - (match id with None -> [] | Some id -> [None,"id",id]) - [< target ; - List.fold_left - (fun i (uri,arg) -> - let relUri = - let buri_frags = - Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in - let uri_frags = - Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in - let rec find_relUri buri_frags uri_frags = - match buri_frags,uri_frags with - [_], _ -> String.concat "/" uri_frags - | he1::tl1, he2::tl2 -> - assert (he1 = he2) ; - find_relUri tl1 tl2 - | _,_ -> assert false (* uri is not relative to buri *) - in - find_relUri buri_frags uri_frags - in - [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >] - ) [<>] subst - >] - in - aux -;; - -let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = - let module C = Cic in - let module X = Xml in - let module U = UriManager in - let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in - match obj with - C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> - let params' = param_attribute_of_params params in - 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" - [None,"of",UriManager.string_of_uri uri ; None,"id", id] - [< List.fold_left - (fun i (cid,n,canonical_context,t) -> - [< i ; - X.xml_nempty "Conjecture" - [None,"id",cid ; None,"no",(string_of_int n)] - [< List.fold_left - (fun i (hid,t) -> - [< (match t with - Some (n,C.ADecl t) -> - X.xml_nempty "Decl" - (match n with - C.Name n' -> - [None,"id",hid;None,"name",n'] - | C.Anonymous -> [None,"id",hid]) - (print_term ids_to_inner_sorts t) - | Some (n,C.ADef t) -> - X.xml_nempty "Def" - (match n with - C.Name n' -> - [None,"id",hid;None,"name",n'] - | C.Anonymous -> [None,"id",hid]) - (print_term ids_to_inner_sorts t) - | None -> X.xml_empty "Hidden" [None,"id",hid] - ) ; - i - >] - ) [< >] canonical_context ; - X.xml_nempty "Goal" [] - (print_term ids_to_inner_sorts t) - >] - >]) - [<>] conjectures ; - X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] - in - let xml_for_current_proof_type = - X.xml_nempty "ConstantType" - [None,"name",n ; None,"params",params' ; None,"id", id] - (print_term ids_to_inner_sorts ty) - in - let xmlbo = - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - xml_for_current_proof_body - >] in - let xmlty = - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - xml_for_current_proof_type - >] - in - xmlty, Some xmlbo - | C.AConstant (id,idbody,n,bo,ty,params) -> - let params' = param_attribute_of_params params in - let xmlbo = - match bo with - None -> None - | Some bo -> - Some - [< X.xml_cdata - "\n" ; - X.xml_cdata - ("\n") ; - X.xml_nempty "ConstantBody" - [None,"for",UriManager.string_of_uri uri ; - None,"params",params' ; None,"id", id] - [< print_term ids_to_inner_sorts bo >] - >] - in - let xmlty = - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - X.xml_nempty "ConstantType" - [None,"name",n ; None,"params",params' ; None,"id", id] - [< print_term ids_to_inner_sorts ty >] - >] - in - xmlty, xmlbo - | C.AVariable (id,n,bo,ty,params) -> - let params' = param_attribute_of_params params in - let xmlbo = - match bo with - None -> [< >] - | Some bo -> - X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >] - in - let aobj = - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - X.xml_nempty "Variable" - [None,"name",n ; None,"params",params' ; None,"id", id] - [< xmlbo ; - X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) - >] - >] - in - aobj, None - | C.AInductiveDefinition (id,tys,params,nparams) -> - let params' = param_attribute_of_params params in - [< X.xml_cdata "\n" ; - X.xml_cdata - ("\n") ; - X.xml_nempty "InductiveDefinition" - [None,"noParams",string_of_int nparams ; - None,"id",id ; - None,"params",params'] - [< (List.fold_left - (fun i (id,typename,finite,arity,cons) -> - [< i ; - X.xml_nempty "InductiveType" - [None,"id",id ; None,"name",typename ; - None,"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" - [None,"name",name] - (print_term ids_to_inner_sorts lc) - >]) [<>] cons - ) - >] - >] - ) [< >] tys - ) - >] - >], None -;; - -let - print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types - ~ask_dtd_to_the_getter -= - let module C2A = Cic2acic in - let module X = Xml in - let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in - [< X.xml_cdata "\n" ; - X.xml_cdata - ("\n") ; - X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi] - (Hashtbl.fold - (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> - [< x ; - X.xml_nempty "TYPE" [None,"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 [<>] - ) - >] -;;