From ff6eee275d22bd158f9ccd451aaae0cb61659a6e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 Nov 2001 17:17:43 +0000 Subject: [PATCH] cicAnnotationHinter.ml* were in the library without any reason. --- helm/annotationHelper/.depend | 4 + helm/annotationHelper/Makefile | 4 +- helm/annotationHelper/cicAnnotationHinter.ml | 381 ++++++++++++++++++ helm/annotationHelper/cicAnnotationHinter.mli | 46 +++ 4 files changed, 433 insertions(+), 2 deletions(-) create mode 100644 helm/annotationHelper/cicAnnotationHinter.ml create mode 100644 helm/annotationHelper/cicAnnotationHinter.mli diff --git a/helm/annotationHelper/.depend b/helm/annotationHelper/.depend index e69de29bb..699b8de3a 100644 --- a/helm/annotationHelper/.depend +++ b/helm/annotationHelper/.depend @@ -0,0 +1,4 @@ +cicAnnotationHinter.cmo: cicAnnotationHinter.cmi +cicAnnotationHinter.cmx: cicAnnotationHinter.cmi +cicAnnotationHelper.cmo: cicAnnotationHinter.cmi +cicAnnotationHelper.cmx: cicAnnotationHinter.cmx diff --git a/helm/annotationHelper/Makefile b/helm/annotationHelper/Makefile index 5c7de7bd5..2752dce01 100644 --- a/helm/annotationHelper/Makefile +++ b/helm/annotationHelper/Makefile @@ -9,9 +9,9 @@ OCAMLDEP = ocamldep all: cicAnnotationHelper opt: cicAnnotationHelper.opt -DEPOBJS = cicAnnotationHelper.ml +DEPOBJS = cicAnnotationHinter.mli cicAnnotationHinter.ml cicAnnotationHelper.ml -CICANNOTATIONHELPEROBJS = cicAnnotationHelper.cmo +CICANNOTATIONHELPEROBJS = cicAnnotationHinter.cmo cicAnnotationHelper.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml new file mode 100644 index 000000000..86bcb4588 --- /dev/null +++ b/helm/annotationHelper/cicAnnotationHinter.ml @@ -0,0 +1,381 @@ +(* 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 14/06/2000 *) +(* *) +(* *) +(******************************************************************************) + +let deactivate_hints_from annotation_window n = + let annotation_hints = annotation_window#annotation_hints in + for i = n to Array.length annotation_hints - 1 do + annotation_hints.(i)#misc#hide () + done +;; + +(* CSC: orripilante *) +(* the list of the signal ids *) +let sig_ids = ref ([] : GtkSignal.id list);; + +let disconnect_hint annotation_window buttonno = + match !sig_ids with + id::ids -> + annotation_window#annotation_hints.(buttonno)#misc#disconnect id ; + sig_ids := ids + | _ -> assert false +;; + +(* link_hint annotation_window n label hint *) +(* set the label of the nth hint button of annotation_window to label *) +(* and the correspondent hint to hint *) +let link_hint annotation_window buttonno label hint = + let button = annotation_window#annotation_hints.(buttonno) in + sig_ids := + (button#connect#clicked + (fun () -> (annotation_window#annotation : GEdit.text)#insert hint) + ) :: !sig_ids ; + button#misc#show () ; + match button#children with + [labelw] -> (GMisc.label_cast labelw)#set_text label + | _ -> assert false +;; + +exception TooManyHints;; + +let link_hints annotation_window a = + if Array.length a > Array.length annotation_window#annotation_hints then + raise TooManyHints ; + for i = List.length !sig_ids - 1 downto 0 do + disconnect_hint annotation_window i + done ; + Array.iteri + (fun i (label,hint) -> link_hint annotation_window i label hint) a ; + deactivate_hints_from annotation_window (Array.length a) +;; + +let list_mapi f = + let rec aux n = + function + [] -> [] + | he::tl -> (f n he)::(aux (n + 1) tl) + in + aux 0 +;; + +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 +;; + +let create_hint_from_term annotation_window annterm = + let module C = Cic in + match annterm with + C.ARel (id,_,_,_) -> + link_hints annotation_window + [| "Binder", "" |] + | C.AVar (id,_,_) -> + link_hints annotation_window + [| "relURI???", "" |] + | C.AMeta (id,_,_) -> + link_hints annotation_window + [| "Number", "" |] + | C.ASort (id,_,_) -> + link_hints annotation_window + [| "Value", "" |] + | C.AImplicit (id,_) -> + link_hints annotation_window [| |] + | 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) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Body", "" ; + "Type", "" + |] + | C.ALambda (id,_,_,ty,bo) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Body", "" ; + "Type", "" + |] + | C.ALetIn (id,_,_,ty,bo) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Term", "" ; + "Target", "" + |] + | C.AAppl (id,_,args) -> + let argsid = + Array.mapi + (fun i te -> "Argument " ^ string_of_int i, "") + (Array.of_list args) + in + link_hints annotation_window argsid + | C.AConst (id,_,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AAbst (id,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AMutInd (id,_,_,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AMutConstruct (id,_,_,_,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AMutCase (id,_,_,_,_,outty,te,pl) -> + let outtyid = get_id outty + and teid = get_id te + and plid = + Array.mapi + (fun i te -> "Pattern " ^ string_of_int i, "") + (Array.of_list pl) + in + link_hints annotation_window + (Array.append + [| "Uri???", "" ; + "Case Type", "" ; + "Term", "" ; + |] + plid) + | C.AFix (id,_,_,funl) -> + let funtylid = + Array.mapi + (fun i (_,_,ty,_) -> + "Type " ^ string_of_int i, "") + (Array.of_list funl) + and funbolid = + Array.mapi + (fun i (_,_,_,bo) -> + "Body " ^ string_of_int i, "") + (Array.of_list funl) + and funnamel = + Array.mapi + (fun i (_,_,_,_) -> + "Name " ^ string_of_int i, "") + (Array.of_list funl) + and funrecindexl = + Array.mapi + (fun i (_,_,_,_) -> + "Recursive Index??? " ^ string_of_int i, "") + (Array.of_list funl) + in + link_hints annotation_window + (Array.concat + [ funtylid ; + funbolid ; + funnamel ; + funrecindexl ; + [| "NoFun???", "" |] + ] + ) + | C.ACoFix (id,_,_,funl) -> + let funtylid = + Array.mapi + (fun i (_,ty,_) -> + "Type " ^ string_of_int i, "") + (Array.of_list funl) + and funbolid = + Array.mapi + (fun i (_,_,bo) -> + "Body " ^ string_of_int i, "") + (Array.of_list funl) + and funnamel = + Array.mapi + (fun i (_,_,_) -> + "Name " ^ string_of_int i, "") + (Array.of_list funl) + in + link_hints annotation_window + (Array.concat + [ funtylid ; + funbolid ; + funnamel ; + [| "NoFun???", "" |] + ] + ) +;; + +(*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *) +let create_hint_from_obj annotation_window annobj = + let module C = Cic in + match annobj with + C.ADefinition (id,_,_,bo,ty,_) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Name", "" ; + "Ingredients", "" ; + "Body", "" ; + "Type", "" + |] + | C.AAxiom (id,_,_,ty,_) -> + let tyid = get_id ty in + link_hints annotation_window + [| "Name", "" ; + "Ingredients", "" ; + "Type", "" + |] + | C.AVariable (id,_,_,bo,ty) -> + let tyid = get_id ty in + link_hints annotation_window + (match bo with + None -> + [| "Name", "" ; + "Type", "" + |] + | Some bo -> + let boid = get_id bo in + [| "Name", "" ; + "Body", "" ; + "Type", "" + |] + ) + | 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 + link_hints annotation_window + (Array.append + [| "Name", "" ; + "Ingredients", "" ; + "Body", "" ; + "Type", "" + |] + (Array.mapi + (fun i id -> + "Conjecture " ^ string_of_int i, "" + ) (Array.of_list conjsid) + ) + ) + | C.AInductiveDefinition (id,_,itl,_,_) -> + let itlids = + List.map + (fun (_,_,arity,cons) -> + get_id arity, + List.map (fun (_,ty,_) -> get_id ty) cons + ) itl + in + link_hints annotation_window + (Array.concat + [ + [| "Ingredients","" |]; + (Array.mapi + (fun i _ -> + "Type Name " ^ string_of_int i, + "" + ) (Array.of_list itlids) + ) ; + (Array.mapi + (fun i (id,_) -> + "Type " ^ string_of_int i, "" + ) (Array.of_list itlids) + ) ; + (Array.concat + (list_mapi + (fun i (_,consid) -> + (Array.mapi + (fun j _ -> + "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j, + "" + ) (Array.of_list consid) + ) ; + ) itlids + ) + ) ; + (Array.concat + (list_mapi + (fun i (_,consid) -> + (Array.mapi + (fun j id -> + "Constructor " ^ string_of_int i ^ " " ^ string_of_int j, + "" + ) (Array.of_list consid) + ) ; + ) itlids + ) + ) + ] + ) +;; + +exception IdUnknown of string;; + +let create_hints annotation_window (annobj,ids_to_targets) xpath = + try + match Hashtbl.find ids_to_targets xpath with + Cic.Object annobj -> create_hint_from_obj annotation_window annobj + | Cic.Term annterm -> create_hint_from_term annotation_window annterm + with + Not_found -> raise (IdUnknown xpath) +;; diff --git a/helm/annotationHelper/cicAnnotationHinter.mli b/helm/annotationHelper/cicAnnotationHinter.mli new file mode 100644 index 000000000..6846273b3 --- /dev/null +++ b/helm/annotationHelper/cicAnnotationHinter.mli @@ -0,0 +1,46 @@ +(* 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +val create_hints : + < annotation : GEdit.text; + annotation_hints : < children : < as_widget : 'a Gtk.obj; .. > list; + connect : < clicked : (unit -> unit) -> GtkSignal.id; + .. >; + misc : < disconnect : GtkSignal.id -> 'b; + hide : unit -> 'c; show : unit -> 'd; .. >; + .. > + array; + .. > -> + 'e * (string, Cic.anntarget) Hashtbl.t -> string -> unit -- 2.39.2