--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
+ | C.AVar (id,_,_) ->
+ link_hints annotation_window
+ [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
+ | C.AMeta (id,_,_) ->
+ link_hints annotation_window
+ [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
+ | C.ASort (id,_,_) ->
+ link_hints annotation_window
+ [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
+ | 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", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | C.AProd (id,_,_,ty,bo) ->
+ let boid = get_id bo
+ and tyid = get_id ty in
+ link_hints annotation_window
+ [| "Binder",
+ "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
+ "Body", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | C.ALambda (id,_,_,ty,bo) ->
+ let boid = get_id bo
+ and tyid = get_id ty in
+ link_hints annotation_window
+ [| "Binder",
+ "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
+ "Body", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | C.ALetIn (id,_,_,ty,bo) ->
+ let boid = get_id bo
+ and tyid = get_id ty in
+ link_hints annotation_window
+ [| "Binder",
+ "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
+ "Term", "<node id = '" ^ boid ^ "'/>" ;
+ "Target", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | C.AAppl (id,_,args) ->
+ let argsid =
+ Array.mapi
+ (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
+ get_id te ^ "'/>")
+ (Array.of_list args)
+ in
+ link_hints annotation_window argsid
+ | C.AConst (id,_,_,_) ->
+ link_hints annotation_window
+ [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
+ | C.AAbst (id,_,_) ->
+ link_hints annotation_window
+ [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
+ | C.AMutInd (id,_,_,_,_) ->
+ link_hints annotation_window
+ [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
+ | C.AMutConstruct (id,_,_,_,_,_) ->
+ link_hints annotation_window
+ [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
+ | 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, "<node id ='" ^
+ get_id te ^ "'/>")
+ (Array.of_list pl)
+ in
+ link_hints annotation_window
+ (Array.append
+ [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
+ "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
+ "Term", "<node id = '" ^ teid ^ "'/>" ;
+ |]
+ plid)
+ | C.AFix (id,_,_,funl) ->
+ let funtylid =
+ Array.mapi
+ (fun i (_,_,ty,_) ->
+ "Type " ^ string_of_int i, "<node id ='" ^
+ get_id ty ^ "'/>")
+ (Array.of_list funl)
+ and funbolid =
+ Array.mapi
+ (fun i (_,_,_,bo) ->
+ "Body " ^ string_of_int i, "<node id ='" ^
+ get_id bo ^ "'/>")
+ (Array.of_list funl)
+ and funnamel =
+ Array.mapi
+ (fun i (_,_,_,_) ->
+ "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
+ "' name = 'name' child='" ^ string_of_int i ^ "'/>")
+ (Array.of_list funl)
+ and funrecindexl =
+ Array.mapi
+ (fun i (_,_,_,_) ->
+ "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
+ "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
+ (Array.of_list funl)
+ in
+ link_hints annotation_window
+ (Array.concat
+ [ funtylid ;
+ funbolid ;
+ funnamel ;
+ funrecindexl ;
+ [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
+ ]
+ )
+ | C.ACoFix (id,_,_,funl) ->
+ let funtylid =
+ Array.mapi
+ (fun i (_,ty,_) ->
+ "Type " ^ string_of_int i, "<node id ='" ^
+ get_id ty ^ "'/>")
+ (Array.of_list funl)
+ and funbolid =
+ Array.mapi
+ (fun i (_,_,bo) ->
+ "Body " ^ string_of_int i, "<node id ='" ^
+ get_id bo ^ "'/>")
+ (Array.of_list funl)
+ and funnamel =
+ Array.mapi
+ (fun i (_,_,_) ->
+ "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
+ "' name = 'name' child='" ^ string_of_int i ^ "'/>")
+ (Array.of_list funl)
+ in
+ link_hints annotation_window
+ (Array.concat
+ [ funtylid ;
+ funbolid ;
+ funnamel ;
+ [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
+ ]
+ )
+;;
+
+(*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", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
+ "Body", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | C.AAxiom (id,_,_,ty,_) ->
+ let tyid = get_id ty in
+ link_hints annotation_window
+ [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | C.AVariable (id,_,_,bo,ty) ->
+ let tyid = get_id ty in
+ link_hints annotation_window
+ (match bo with
+ None ->
+ [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | Some bo ->
+ let boid = get_id bo in
+ [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Body", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ )
+ | 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", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
+ "Body", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ (Array.mapi
+ (fun i id ->
+ "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
+ ) (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","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
+ (Array.mapi
+ (fun i _ ->
+ "Type Name " ^ string_of_int i,
+ "<attribute name = 'name' child = '" ^ string_of_int i ^
+ "' id = '" ^ id ^ "'/>"
+ ) (Array.of_list itlids)
+ ) ;
+ (Array.mapi
+ (fun i (id,_) ->
+ "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
+ ) (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,
+ "<attribute name = 'name' id = '" ^ id ^
+ "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
+ 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,
+ "<node id = '" ^ id ^ "'/>"
+ ) (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)
+;;
projects / helm.git / commitdiff