helm/interface/cicAnnotationHinter.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 14/06/2000                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36 let deactivate_hints_from annotation_window n =
  37  let annotation_hints = annotation_window#annotation_hints in
  38   for i = n to Array.length annotation_hints - 1 do
  39    annotation_hints.(i)#misc#hide ()
  40   done
  41 ;;
  42
  43 (* CSC: orripilante *)
  44 (* the list of the signal ids *)
  45 let sig_ids = ref ([] : GtkSignal.id list);;
  46
  47 let disconnect_hint annotation_window buttonno =
  48  match !sig_ids with
  49     id::ids ->
  50      annotation_window#annotation_hints.(buttonno)#misc#disconnect id ;
  51      sig_ids := ids
  52   | _ -> assert false
  53 ;;
  54
  55 (* link_hint annotation_window n label hint *)
  56 (* set the label of the nth hint button of annotation_window to label *)
  57 (* and the correspondent hint to hint                                 *)
  58 let link_hint annotation_window buttonno label hint =
  59  let button = annotation_window#annotation_hints.(buttonno) in
  60   sig_ids :=
  61    (button#connect#clicked
  62     (fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
  63    ) :: !sig_ids ;
  64   button#misc#show () ;
  65   match button#children with
  66      [labelw] -> (GMisc.label_cast labelw)#set_text label
  67    | _ -> assert false
  68 ;;
  69
  70 exception TooManyHints;;
  71
  72 let link_hints annotation_window a =
  73  if Array.length a > Array.length annotation_window#annotation_hints then
  74   raise TooManyHints ;
  75  for i = List.length !sig_ids - 1 downto 0 do
  76   disconnect_hint annotation_window i
  77  done ;
  78  Array.iteri
  79   (fun i (label,hint) -> link_hint annotation_window i label hint) a ;
  80  deactivate_hints_from annotation_window (Array.length a)
  81 ;;
  82
  83 let list_mapi f =
  84  let rec aux n =
  85   function
  86      [] -> []
  87    | he::tl -> (f n he)::(aux (n + 1) tl)
  88  in
  89   aux 0
  90 ;;
  91
  92 let get_id annterm =
  93  let module C = Cic in
  94   match annterm with
  95      C.ARel (id,_,_,_)             -> id
  96    | C.AVar (id,_,_)               -> id
  97    | C.AMeta (id,_,_)              -> id
  98    | C.ASort (id,_,_)              -> id
  99    | C.AImplicit (id,_)            -> id
 100    | C.ACast (id,_,_,_)            -> id
 101    | C.AProd (id,_,_,_,_)          -> id
 102    | C.ALambda (id,_,_,_,_)        -> id
 103    | C.ALetIn (id,_,_,_,_)         -> id
 104    | C.AAppl (id,_,_)              -> id
 105    | C.AConst (id,_,_,_)           -> id
 106    | C.AAbst (id,_,_)              -> id
 107    | C.AMutInd (id,_,_,_,_)        -> id
 108    | C.AMutConstruct (id,_,_,_,_,_)-> id
 109    | C.AMutCase (id,_,_,_,_,_,_,_) -> id
 110    | C.AFix (id,_,_,_)             -> id
 111    | C.ACoFix (id,_,_,_)           -> id
 112 ;;
 113
 114 let create_hint_from_term annotation_window annterm =
 115  let module C = Cic in
 116   match annterm with
 117      C.ARel (id,_,_,_) ->
 118       link_hints annotation_window
 119        [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
 120    | C.AVar (id,_,_) ->
 121       link_hints annotation_window
 122        [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
 123    | C.AMeta (id,_,_) ->
 124       link_hints annotation_window
 125        [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
 126    | C.ASort (id,_,_) ->
 127       link_hints annotation_window
 128        [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
 129    | C.AImplicit (id,_) ->
 130       link_hints annotation_window [| |]
 131    | C.ACast (id,_,bo,ty) ->
 132       let boid = get_id bo
 133       and tyid = get_id ty in
 134        link_hints annotation_window
 135         [| "Body", "<node id = '" ^ boid ^ "'/>" ;
 136            "Type", "<node id = '" ^ tyid ^ "'/>"
 137         |]
 138    | C.AProd (id,_,_,ty,bo) ->
 139       let boid = get_id bo
 140       and tyid = get_id ty in
 141        link_hints annotation_window
 142         [| "Binder",
 143             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 144            "Body", "<node id = '" ^ boid ^ "'/>" ;
 145            "Type", "<node id = '" ^ tyid ^ "'/>"
 146         |]
 147    | C.ALambda (id,_,_,ty,bo) ->
 148       let boid = get_id bo
 149       and tyid = get_id ty in
 150        link_hints annotation_window
 151         [| "Binder",
 152             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 153            "Body", "<node id = '" ^ boid ^ "'/>" ;
 154            "Type", "<node id = '" ^ tyid ^ "'/>"
 155         |]
 156    | C.ALetIn (id,_,_,ty,bo) ->
 157       let boid = get_id bo
 158       and tyid = get_id ty in
 159        link_hints annotation_window
 160         [| "Binder",
 161             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 162            "Term", "<node id = '" ^ boid ^ "'/>" ;
 163            "Target", "<node id = '" ^ tyid ^ "'/>"
 164         |]
 165    | C.AAppl (id,_,args) ->
 166       let argsid =
 167        Array.mapi
 168         (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
 169           get_id te ^ "'/>")
 170         (Array.of_list args)
 171       in
 172        link_hints annotation_window argsid
 173    | C.AConst (id,_,_,_) ->
 174       link_hints annotation_window
 175        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 176    | C.AAbst (id,_,_) ->
 177       link_hints annotation_window
 178        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 179    | C.AMutInd (id,_,_,_,_) ->
 180       link_hints annotation_window
 181        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 182    | C.AMutConstruct (id,_,_,_,_,_) ->
 183       link_hints annotation_window
 184        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 185    | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
 186       let outtyid = get_id outty
 187       and teid = get_id te
 188       and plid =
 189        Array.mapi
 190         (fun i te -> "Pattern " ^ string_of_int i, "<node id ='" ^
 191           get_id te ^ "'/>")
 192         (Array.of_list pl)
 193       in
 194        link_hints annotation_window
 195         (Array.append
 196          [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
 197             "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
 198             "Term", "<node id = '" ^ teid ^ "'/>" ;
 199          |]
 200          plid)
 201    | C.AFix (id,_,_,funl) ->
 202       let funtylid =
 203        Array.mapi
 204         (fun i (_,_,ty,_) ->
 205           "Type " ^ string_of_int i, "<node id ='" ^
 206           get_id ty ^ "'/>")
 207         (Array.of_list funl)
 208       and funbolid =
 209        Array.mapi
 210         (fun i (_,_,_,bo) ->
 211           "Body " ^ string_of_int i, "<node id ='" ^
 212           get_id bo ^ "'/>")
 213         (Array.of_list funl)
 214       and funnamel =
 215        Array.mapi
 216         (fun i (_,_,_,_) ->
 217           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
 218            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
 219         (Array.of_list funl)
 220       and funrecindexl =
 221        Array.mapi
 222         (fun i (_,_,_,_) ->
 223           "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
 224            "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
 225         (Array.of_list funl)
 226       in
 227        link_hints annotation_window
 228         (Array.concat
 229          [ funtylid ;
 230            funbolid ;
 231            funnamel ;
 232            funrecindexl ;
 233            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
 234          ]
 235         )
 236    | C.ACoFix (id,_,_,funl) ->
 237       let funtylid =
 238        Array.mapi
 239         (fun i (_,ty,_) ->
 240           "Type " ^ string_of_int i, "<node id ='" ^
 241           get_id ty ^ "'/>")
 242         (Array.of_list funl)
 243       and funbolid =
 244        Array.mapi
 245         (fun i (_,_,bo) ->
 246           "Body " ^ string_of_int i, "<node id ='" ^
 247           get_id bo ^ "'/>")
 248         (Array.of_list funl)
 249       and funnamel =
 250        Array.mapi
 251         (fun i (_,_,_) ->
 252           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
 253            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
 254         (Array.of_list funl)
 255       in
 256        link_hints annotation_window
 257         (Array.concat
 258          [ funtylid ;
 259            funbolid ;
 260            funnamel ;
 261            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
 262          ]
 263         )
 264 ;;
 265
 266 (*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *)
 267 let create_hint_from_obj annotation_window annobj =
 268  let module C = Cic in
 269   match annobj with
 270      C.ADefinition (id,_,_,bo,ty,_) ->
 271       let boid = get_id bo
 272       and tyid = get_id ty in
 273        link_hints annotation_window
 274         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 275            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 276            "Body", "<node id = '" ^ boid ^ "'/>" ;
 277            "Type", "<node id = '" ^ tyid ^ "'/>"
 278         |]
 279    | C.AAxiom (id,_,_,ty,_) ->
 280       let tyid = get_id ty in
 281        link_hints annotation_window
 282         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 283            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 284            "Type", "<node id = '" ^ tyid ^ "'/>"
 285         |]
 286    | C.AVariable (id,_,_,bo,ty) ->
 287       let tyid = get_id ty in
 288        link_hints annotation_window
 289         (match bo with
 290             None ->
 291              [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 292                 "Type", "<node id = '" ^ tyid ^ "'/>"
 293              |]
 294           | Some bo ->
 295              let boid = get_id bo in
 296               [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 297                  "Body", "<node id = '" ^ boid ^ "'/>" ;
 298                  "Type", "<node id = '" ^ tyid ^ "'/>"
 299               |]
 300         )
 301    | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
 302       let boid = get_id bo
 303       and tyid = get_id ty
 304       and conjsid = List.map (fun (_,te) -> get_id te) conjs in
 305        link_hints annotation_window
 306         (Array.append
 307           [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 308              "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 309              "Body", "<node id = '" ^ boid ^ "'/>" ;
 310              "Type", "<node id = '" ^ tyid ^ "'/>"
 311           |]
 312           (Array.mapi
 313             (fun i id ->
 314               "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
 315             ) (Array.of_list conjsid)
 316           )
 317         )
 318    | C.AInductiveDefinition (id,_,itl,_,_) ->
 319       let itlids =
 320        List.map
 321         (fun (_,_,arity,cons) ->
 322           get_id arity,
 323           List.map (fun (_,ty,_) -> get_id ty) cons
 324         ) itl
 325       in
 326        link_hints annotation_window
 327         (Array.concat
 328           [
 329            [| "Ingredients","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
 330            (Array.mapi
 331              (fun i _ ->
 332                "Type Name " ^ string_of_int i,
 333                "<attribute name = 'name' child = '" ^ string_of_int i ^
 334                 "' id = '" ^ id ^ "'/>"
 335              ) (Array.of_list itlids)
 336            ) ;
 337            (Array.mapi
 338              (fun i (id,_) ->
 339                "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
 340              ) (Array.of_list itlids)
 341            ) ;
 342            (Array.concat
 343             (list_mapi
 344              (fun i (_,consid) ->
 345               (Array.mapi
 346                 (fun j _ ->
 347                   "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j,
 348                   "<attribute name = 'name' id = '" ^ id ^
 349                    "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
 350                    string_of_int j ^ "'/>"
 351                 ) (Array.of_list consid)
 352               ) ;
 353              ) itlids
 354             )
 355            ) ;
 356            (Array.concat
 357             (list_mapi
 358              (fun i (_,consid) ->
 359               (Array.mapi
 360                 (fun j id ->
 361                   "Constructor " ^ string_of_int i ^ " " ^ string_of_int j,
 362                   "<node id = '" ^ id ^ "'/>"
 363                 ) (Array.of_list consid)
 364               ) ;
 365              ) itlids
 366             )
 367            )
 368           ]
 369         )
 370 ;;
 371
 372 exception IdUnknown of string;;
 373
 374 let create_hints annotation_window (annobj,ids_to_targets) xpath =
 375  try
 376   match Hashtbl.find ids_to_targets xpath with
 377      Cic.Object annobj -> create_hint_from_obj annotation_window annobj
 378    | Cic.Term annterm -> create_hint_from_term annotation_window annterm
 379  with
 380   Not_found -> raise (IdUnknown xpath)
 381 ;;