(* 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)
;;