From: Claudio Sacerdoti Coen Date: Mon, 3 Dec 2001 14:52:07 +0000 (+0000) Subject: Main code clean-up. X-Git-Tag: mlminidom_0_2_2~37 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6e4a271838bc59f3b22e68a282dc995776360cb;p=helm.git Main code clean-up. --- diff --git a/helm/annotationHelper/cicAnnotationHelper.ml b/helm/annotationHelper/cicAnnotationHelper.ml index 0b858b268..7b150ffed 100644 --- a/helm/annotationHelper/cicAnnotationHelper.ml +++ b/helm/annotationHelper/cicAnnotationHelper.ml @@ -45,11 +45,13 @@ (* GLOBAL REFERENCES (USED BY CALLBACKS) *) -let annotated_obj = ref None;; (* reference to a couple option where *) +let annotated_obj = ref None;; (* reference to a triple option where *) (* the first component is the current *) - (* annotated object and the second is *) - (* the map from ids to annotated targets *) -let ann = ref (ref None);; (* current annotation *) + (* annotated object, the second is the *) + (* map from ids to annotated targets and *) + (* the third is the map from ids to *) + (* annotations. *) +let current_id = ref None;; (* id of the element to annotate *) let radio_some_status = ref false;; (* is the radio_some button selected? *) let current_url = ref "";; @@ -179,7 +181,13 @@ let get_annotated_obj () = match !annotated_obj with None -> let annobj = - (CicCache.get_annobj (get_current_uri ())) + let (annobj,ids_to_annotations) = + match CicCache.get_annobj (get_current_uri ()) with + (annobj,None) -> annobj, Hashtbl.create 503 + | (annobj, Some ids_to_annotations) -> (annobj,ids_to_annotations) + in + let ids_to_targets = CicXPath.get_ids_to_targets annobj in + (annobj,ids_to_targets,ids_to_annotations) in annotated_obj := Some annobj ; annobj @@ -210,52 +218,77 @@ let annotateb_pressed rendering_window annotation_window () = begin match (node#get_attribute_ns (O.o_mDOMString_of_string "xref") helmns) with Some xpath -> - let annobj = get_annotated_obj () - and annotation = (annotation_window#annotation : GEdit.text) in - ann := CicXPath.get_annotation annobj (xpath#get_string) ; - CicAnnotationHinter.create_hints annotation_window annobj - (xpath#get_string) ; - annotation#delete_text 0 annotation#length ; - begin - match !(!ann) with - None -> - annotation#misc#set_sensitive false ; - annotation_window#radio_none#set_active true ; - radio_some_status := false - | Some ann' -> - annotation#insert ann' ; - annotation#misc#set_sensitive true ; - annotation_window#radio_some#set_active true ; - radio_some_status := true - end ; - GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; - annotation_window#show () ; + let annobj = get_annotated_obj () in + let (anno, ids_to_targets, ids_to_annotations) = annobj in + let annotation = (annotation_window#annotation : GEdit.text) in + let id = xpath#get_string in + current_id := Some id ; + let ann = CicXPath.get_annotation ids_to_annotations id in + CicAnnotationHinter.create_hints annotation_window ids_to_targets + (xpath#get_string) ; + annotation#delete_text 0 annotation#length ; + begin + match ann with + None -> + annotation#misc#set_sensitive false ; + annotation_window#radio_none#set_active true ; + radio_some_status := false + | Some ann' -> + annotation#insert ann' ; + annotation#misc#set_sensitive true ; + annotation_window#radio_some#set_active true ; + radio_some_status := true + end ; + GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; + annotation_window#show () ; | None -> rendering_window#label#set_text ("ERROR: No xref found!!!\n") end | None -> rendering_window#label#set_text ("ERROR: No selection!!!\n") ;; +let change_annotation ids_to_annotations id ann = + begin + try + Hashtbl.remove ids_to_annotations id + with + Not_found -> () + end ; + match ann with + None -> () + | Some ann' -> Hashtbl.add ids_to_annotations id ann' +;; + (* called when the annotation is confirmed *) let save_annotation annotation = let module S = Str in let module U = UriManager in - if !radio_some_status then - !ann := Some (annotation#get_chars 0 annotation#length) - else - !ann := None ; - match !annotated_obj with - None -> assert false - | Some (annobj,_) -> - let uri = get_current_uri () in - let annxml = CicAnnotation2Xml.pp_annotation annobj uri in - make_dirs - (pathname_of_annuri (U.buri_of_uri uri)) ; - Xml.pp ~quiet:true annxml - (Some - (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ - ".xml" - ) - ) + let (annobj,ids_to_annotations) = + match !annotated_obj with + None -> assert false + | Some (annobj,_,ids_to_annotations) -> annobj,ids_to_annotations + in + change_annotation ids_to_annotations + (match !current_id with + Some id -> id + | None -> assert false + ) + (if !radio_some_status then + Some (annotation#get_chars 0 annotation#length) + else + None + ) ; + let uri = get_current_uri () in + let annxml = + CicAnnotation2Xml.pp_annotation annobj ids_to_annotations uri + in + make_dirs + (pathname_of_annuri (U.buri_of_uri uri)) ; + Xml.pp ~quiet:true annxml + (Some + (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ + ".xml" + ) + ) ;; (* STUFF TO BUILD THE GTK INTERFACE *) diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml index 86bcb4588..a84b1a44d 100644 --- a/helm/annotationHelper/cicAnnotationHinter.ml +++ b/helm/annotationHelper/cicAnnotationHinter.ml @@ -92,50 +92,50 @@ let list_mapi f = let get_id annterm = let module C = Cic in match annterm with - C.ARel (id,_,_,_) -> id - | C.AVar (id,_,_) -> id - | C.AMeta (id,_,_) -> id - | C.ASort (id,_,_) -> id - | C.AImplicit (id,_) -> id - | C.ACast (id,_,_,_) -> id - | C.AProd (id,_,_,_,_) -> id - | C.ALambda (id,_,_,_,_) -> id - | C.ALetIn (id,_,_,_,_) -> id - | C.AAppl (id,_,_) -> id - | C.AConst (id,_,_,_) -> id - | C.AAbst (id,_,_) -> id - | C.AMutInd (id,_,_,_,_) -> id - | C.AMutConstruct (id,_,_,_,_,_)-> id - | C.AMutCase (id,_,_,_,_,_,_,_) -> id - | C.AFix (id,_,_,_) -> id - | C.ACoFix (id,_,_,_) -> id + C.ARel (id,_,_) + | C.AVar (id,_) + | C.AMeta (id,_) + | C.ASort (id,_) + | C.AImplicit id + | C.ACast (id,_,_) + | C.AProd (id,_,_,_) + | C.ALambda (id,_,_,_) + | C.ALetIn (id,_,_,_) + | C.AAppl (id,_) + | C.AConst (id,_,_) + | C.AAbst (id,_) + | C.AMutInd (id,_,_,_) + | C.AMutConstruct (id,_,_,_,_) + | C.AMutCase (id,_,_,_,_,_,_) + | C.AFix (id,_,_) + | C.ACoFix (id,_,_) -> id ;; let create_hint_from_term annotation_window annterm = let module C = Cic in match annterm with - C.ARel (id,_,_,_) -> + C.ARel (id,_,_) -> link_hints annotation_window [| "Binder", "" |] - | C.AVar (id,_,_) -> + | C.AVar (id,_) -> link_hints annotation_window [| "relURI???", "" |] - | C.AMeta (id,_,_) -> + | C.AMeta (id,_) -> link_hints annotation_window [| "Number", "" |] - | C.ASort (id,_,_) -> + | C.ASort (id,_) -> link_hints annotation_window [| "Value", "" |] - | C.AImplicit (id,_) -> + | C.AImplicit id -> link_hints annotation_window [| |] - | C.ACast (id,_,bo,ty) -> + | C.ACast (id,bo,ty) -> let boid = get_id bo and tyid = get_id ty in link_hints annotation_window [| "Body", "" ; "Type", "" |] - | C.AProd (id,_,_,ty,bo) -> + | C.AProd (id,_,ty,bo) -> let boid = get_id bo and tyid = get_id ty in link_hints annotation_window @@ -144,7 +144,7 @@ let create_hint_from_term annotation_window annterm = "Body", "" ; "Type", "" |] - | C.ALambda (id,_,_,ty,bo) -> + | C.ALambda (id,_,ty,bo) -> let boid = get_id bo and tyid = get_id ty in link_hints annotation_window @@ -153,7 +153,7 @@ let create_hint_from_term annotation_window annterm = "Body", "" ; "Type", "" |] - | C.ALetIn (id,_,_,ty,bo) -> + | C.ALetIn (id,_,ty,bo) -> let boid = get_id bo and tyid = get_id ty in link_hints annotation_window @@ -162,7 +162,7 @@ let create_hint_from_term annotation_window annterm = "Term", "" ; "Target", "" |] - | C.AAppl (id,_,args) -> + | C.AAppl (id,args) -> let argsid = Array.mapi (fun i te -> "Argument " ^ string_of_int i, "" |] - | C.AAbst (id,_,_) -> + | C.AAbst (id,_) -> link_hints annotation_window [| "Uri???", "" |] - | C.AMutInd (id,_,_,_,_) -> + | C.AMutInd (id,_,_,_) -> link_hints annotation_window [| "Uri???", "" |] - | C.AMutConstruct (id,_,_,_,_,_) -> + | C.AMutConstruct (id,_,_,_,_) -> link_hints annotation_window [| "Uri???", "" |] - | C.AMutCase (id,_,_,_,_,outty,te,pl) -> + | C.AMutCase (id,_,_,_,outty,te,pl) -> let outtyid = get_id outty and teid = get_id te and plid = @@ -198,7 +198,7 @@ let create_hint_from_term annotation_window annterm = "Term", "" ; |] plid) - | C.AFix (id,_,_,funl) -> + | C.AFix (id,_,funl) -> let funtylid = Array.mapi (fun i (_,_,ty,_) -> @@ -233,7 +233,7 @@ let create_hint_from_term annotation_window annterm = [| "NoFun???", "" |] ] ) - | C.ACoFix (id,_,_,funl) -> + | C.ACoFix (id,_,funl) -> let funtylid = Array.mapi (fun i (_,ty,_) -> @@ -267,7 +267,7 @@ let create_hint_from_term annotation_window annterm = let create_hint_from_obj annotation_window annobj = let module C = Cic in match annobj with - C.ADefinition (id,_,_,bo,ty,_) -> + C.ADefinition (id,_,bo,ty,_) -> let boid = get_id bo and tyid = get_id ty in link_hints annotation_window @@ -276,14 +276,14 @@ let create_hint_from_obj annotation_window annobj = "Body", "" ; "Type", "" |] - | C.AAxiom (id,_,_,ty,_) -> + | C.AAxiom (id,_,ty,_) -> let tyid = get_id ty in link_hints annotation_window [| "Name", "" ; "Ingredients", "" ; "Type", "" |] - | C.AVariable (id,_,_,bo,ty) -> + | C.AVariable (id,_,bo,ty) -> let tyid = get_id ty in link_hints annotation_window (match bo with @@ -298,7 +298,7 @@ let create_hint_from_obj annotation_window annobj = "Type", "" |] ) - | C.ACurrentProof (id,_,_,conjs,bo,ty) -> + | C.ACurrentProof (id,_,conjs,bo,ty) -> let boid = get_id bo and tyid = get_id ty and conjsid = List.map (fun (_,te) -> get_id te) conjs in @@ -315,7 +315,7 @@ let create_hint_from_obj annotation_window annobj = ) (Array.of_list conjsid) ) ) - | C.AInductiveDefinition (id,_,itl,_,_) -> + | C.AInductiveDefinition (id,itl,_,_) -> let itlids = List.map (fun (_,_,arity,cons) -> @@ -371,7 +371,7 @@ let create_hint_from_obj annotation_window annobj = exception IdUnknown of string;; -let create_hints annotation_window (annobj,ids_to_targets) xpath = +let create_hints annotation_window ids_to_targets xpath = try match Hashtbl.find ids_to_targets xpath with Cic.Object annobj -> create_hint_from_obj annotation_window annobj diff --git a/helm/annotationHelper/cicAnnotationHinter.mli b/helm/annotationHelper/cicAnnotationHinter.mli index 6846273b3..c21eefc88 100644 --- a/helm/annotationHelper/cicAnnotationHinter.mli +++ b/helm/annotationHelper/cicAnnotationHinter.mli @@ -43,4 +43,4 @@ val create_hints : .. > array; .. > -> - 'e * (string, Cic.anntarget) Hashtbl.t -> string -> unit + (Cic.id, Cic.anntarget) Hashtbl.t -> string -> unit diff --git a/helm/fix_params/cic2Xml.ml b/helm/fix_params/cic2Xml.ml index 58f35bb6f..ea58eb382 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,56 @@ 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.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) -> + | 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 +117,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 +130,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 +183,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 +196,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 +205,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 +216,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 +229,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) diff --git a/helm/fix_params/cicFindParameters.ml b/helm/fix_params/cicFindParameters.ml index 555f44e2e..f74675155 100644 --- a/helm/fix_params/cicFindParameters.ml +++ b/helm/fix_params/cicFindParameters.ml @@ -147,12 +147,12 @@ 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) -> + C.ADefinition (xid, 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) + C.ADefinition (xid,id,te,ty,C.Actual real_params) in Xml.pp (Cic2Xml.pp fixed uri) filename ; | _ -> () diff --git a/helm/metadata/create2/mk_forward/mk_forward.ml b/helm/metadata/create2/mk_forward/mk_forward.ml index 294746124..80ed9caf5 100644 --- a/helm/metadata/create2/mk_forward/mk_forward.ml +++ b/helm/metadata/create2/mk_forward/mk_forward.ml @@ -149,12 +149,7 @@ let output_file cic_string_uri rdf_string_uri = let get_obj uri = let cicfilename = Getter.getxml uri in - let res = - match CicParser.term_of_xml cicfilename uri false with - (annobj, None) -> - Deannotate.deannotate_obj annobj - | _ -> assert false - in + let res = CicParser.obj_of_xml cicfilename uri in Unix.unlink cicfilename ; res ;; diff --git a/helm/metadata/create2/touch/touch.ml b/helm/metadata/create2/touch/touch.ml index 8538a8faa..8fea03e0e 100644 --- a/helm/metadata/create2/touch/touch.ml +++ b/helm/metadata/create2/touch/touch.ml @@ -60,12 +60,7 @@ let touch_file rdf_string_uri = let get_obj uri = let cicfilename = Getter.getxml uri in - let res = - match CicParser.term_of_xml cicfilename uri false with - (annobj, None) -> - Deannotate.deannotate_obj annobj - | _ -> assert false - in + let res = CicParser.obj_of_xml cicfilename uri in Unix.unlink cicfilename ; res ;;