+++ /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
- ~callback:(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,_,_)
- | 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.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,_,_) ->
- 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,_,subst) ->
- let res =
- Array.append
- [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
- (Array.mapi
- (fun i s ->
- match s with
- None ->
- "Argument " ^ string_of_int i, "_"
- | Some t ->
- "Argument " ^ string_of_int i, "<node id ='" ^ get_id t ^ "'/>"
- ) (Array.of_list subst)
- )
- in
- link_hints annotation_window res
- | 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.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 (id,_,_,_) -> id) conjs in
- link_hints annotation_window
-(*CSC: never tested since the introduction of the new Metas *)
- (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 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
-(*CSC: never tested since the introduction of the new Metas *)
- | Cic.Hypothesis _
- | Cic.Conjecture _ -> assert false
- with
- Not_found -> raise (IdUnknown xpath)
-;;