X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Ffix_params%2Fcic2Xml.ml;fp=helm%2Ffix_params%2Fcic2Xml.ml;h=0000000000000000000000000000000000000000;hp=0d433d64add316b6cbf16bde494f8ec8e93a3be6;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/fix_params/cic2Xml.ml b/helm/fix_params/cic2Xml.ml deleted file mode 100644 index 0d433d64a..000000000 --- a/helm/fix_params/cic2Xml.ml +++ /dev/null @@ -1,251 +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 = "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,b) -> - X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id] - | 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.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 [< >] - >] - >] -;;