X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Ffix_params%2Fcic2Xml.ml;h=0d433d64add316b6cbf16bde494f8ec8e93a3be6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=58f35bb6f687c0581bd611589ac9ee94f3e25d97;hpb=02c3583e17631f04375a185af5d7b49698cd3d24;p=helm.git diff --git a/helm/fix_params/cic2Xml.ml b/helm/fix_params/cic2Xml.ml index 58f35bb6f..0d433d64a 100644 --- a/helm/fix_params/cic2Xml.ml +++ b/helm/fix_params/cic2Xml.ml @@ -28,8 +28,6 @@ exception ImpossiblePossible;; exception NotImplemented;; -exception BinderNotSpecified;; - let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) @@ -39,19 +37,18 @@ let print_term curi = let module X = Xml in let module U = UriManager in function - C.ARel (id,_,n,Some b) -> + C.ARel (id,n,b) -> X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id] - | C.ARel _ -> raise BinderNotSpecified - | C.AVar (id,_,uri) -> + | 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) -> + | C.AMeta (id,n) -> X.xml_empty "META" ["no",(string_of_int n) ; "id",id] - | C.ASort (id,_,s) -> + | C.ASort (id,s) -> let string_of_sort = function C.Prop -> "Prop" @@ -60,56 +57,55 @@ let print_term curi = in X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] | C.AImplicit _ -> raise NotImplemented - | C.AProd (id,_,C.Anonimous,s,t) -> + | 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) -> + | 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) -> + | 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) -> + | 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) -> + | 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) -> + | 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) -> + | 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) -> + | C.AAppl (id,li) -> X.xml_nempty "APPLY" ["id",id] [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) >] - | C.AConst (id,_,uri,_) -> + | 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) -> + | 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) -> + | 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) -> + | C.AMutCase (id,uri,_,typeno,ty,te,patterns) -> X.xml_nempty "MUTCASE" ["uriType",(U.string_of_uri uri) ; "noType", (string_of_int typeno) ; @@ -120,7 +116,7 @@ let print_term curi = (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) patterns [<>] >] - | C.AFix (id, _, no, funs) -> + | 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 -> @@ -133,7 +129,7 @@ let print_term curi = >] ) funs [<>] >] - | C.ACoFix (id,_,no,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 -> @@ -186,7 +182,7 @@ let pp obj curi = let module C = Cic in let module X = Xml in match obj with - C.ADefinition (xid, _, id, te, ty, params) -> + C.ADefinition (xid, id, te, ty, params) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Definition" @@ -199,7 +195,7 @@ let pp obj curi = [< X.xml_nempty "body" [] (print_term curi te) ; X.xml_nempty "type" [] (print_term curi ty) >] >] - | C.AAxiom (xid, _, id, ty, params) -> + | C.AAxiom (xid, id, ty, params) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Axiom" @@ -208,7 +204,7 @@ let pp obj curi = ["name",id ; "params",(encode (List.rev params)) ; "id",xid] [< X.xml_nempty "type" [] (print_term curi ty) >] >] - | C.AVariable (xid, _, name, bo, ty) -> + | C.AVariable (xid, name, bo, ty) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Variable" ["name",name ; "id",xid] @@ -219,7 +215,7 @@ let pp obj curi = X.xml_nempty "type" [] (print_term curi ty) >] >] - | C.ACurrentProof (xid, _, name, conjs, bo, 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] @@ -232,7 +228,7 @@ let pp obj curi = X.xml_nempty "type" [] [< print_term curi ty >] >] >] - | C.AInductiveDefinition (xid, _, tys, params, paramsno) -> + | C.AInductiveDefinition (xid, tys, params, paramsno) -> let names = List.map (fun (typename,_,_,_) -> typename)