helm/annotationHelper/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     ~callback:(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,_,_)
  96    | C.AVar (id,_)
  97    | C.AMeta (id,_,_)
  98    | C.ASort (id,_)
  99    | C.AImplicit id
 100    | C.ACast (id,_,_)
 101    | C.AProd (id,_,_,_)
 102    | C.ALambda (id,_,_,_)
 103    | C.ALetIn (id,_,_,_)
 104    | C.AAppl (id,_)
 105    | C.AConst (id,_,_)
 106    | C.AMutInd (id,_,_,_)
 107    | C.AMutConstruct (id,_,_,_,_)
 108    | C.AMutCase (id,_,_,_,_,_,_)
 109    | C.AFix (id,_,_)
 110    | C.ACoFix (id,_,_) -> id
 111 ;;
 112
 113 let create_hint_from_term annotation_window annterm =
 114  let module C = Cic in
 115   match annterm with
 116      C.ARel (id,_,_) ->
 117       link_hints annotation_window
 118        [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
 119    | C.AVar (id,_) ->
 120       link_hints annotation_window
 121        [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
 122    | C.AMeta (id,_,subst) ->
 123       let res =
 124        Array.append
 125         [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
 126         (Array.mapi
 127           (fun i s ->
 128             match s with
 129                None ->
 130                 "Argument " ^ string_of_int i, "_"
 131              | Some t ->
 132                 "Argument " ^ string_of_int i, "<node id ='" ^ get_id t ^ "'/>"
 133           ) (Array.of_list subst)
 134         )
 135       in
 136        link_hints annotation_window res
 137    | C.ASort (id,_) ->
 138       link_hints annotation_window
 139        [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
 140    | C.AImplicit id ->
 141       link_hints annotation_window [| |]
 142    | C.ACast (id,bo,ty) ->
 143       let boid = get_id bo
 144       and tyid = get_id ty in
 145        link_hints annotation_window
 146         [| "Body", "<node id = '" ^ boid ^ "'/>" ;
 147            "Type", "<node id = '" ^ tyid ^ "'/>"
 148         |]
 149    | C.AProd (id,_,ty,bo) ->
 150       let boid = get_id bo
 151       and tyid = get_id ty in
 152        link_hints annotation_window
 153         [| "Binder",
 154             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 155            "Body", "<node id = '" ^ boid ^ "'/>" ;
 156            "Type", "<node id = '" ^ tyid ^ "'/>"
 157         |]
 158    | C.ALambda (id,_,ty,bo) ->
 159       let boid = get_id bo
 160       and tyid = get_id ty in
 161        link_hints annotation_window
 162         [| "Binder",
 163             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 164            "Body", "<node id = '" ^ boid ^ "'/>" ;
 165            "Type", "<node id = '" ^ tyid ^ "'/>"
 166         |]
 167    | C.ALetIn (id,_,ty,bo) ->
 168       let boid = get_id bo
 169       and tyid = get_id ty in
 170        link_hints annotation_window
 171         [| "Binder",
 172             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 173            "Term", "<node id = '" ^ boid ^ "'/>" ;
 174            "Target", "<node id = '" ^ tyid ^ "'/>"
 175         |]
 176    | C.AAppl (id,args) ->
 177       let argsid =
 178        Array.mapi
 179         (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
 180           get_id te ^ "'/>")
 181         (Array.of_list args)
 182       in
 183        link_hints annotation_window argsid
 184    | C.AConst (id,_,_) ->
 185       link_hints annotation_window
 186        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 187    | C.AMutInd (id,_,_,_) ->
 188       link_hints annotation_window
 189        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 190    | C.AMutConstruct (id,_,_,_,_) ->
 191       link_hints annotation_window
 192        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 193    | C.AMutCase (id,_,_,_,outty,te,pl) ->
 194       let outtyid = get_id outty
 195       and teid = get_id te
 196       and plid =
 197        Array.mapi
 198         (fun i te -> "Pattern " ^ string_of_int i, "<node id ='" ^
 199           get_id te ^ "'/>")
 200         (Array.of_list pl)
 201       in
 202        link_hints annotation_window
 203         (Array.append
 204          [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
 205             "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
 206             "Term", "<node id = '" ^ teid ^ "'/>" ;
 207          |]
 208          plid)
 209    | C.AFix (id,_,funl) ->
 210       let funtylid =
 211        Array.mapi
 212         (fun i (_,_,ty,_) ->
 213           "Type " ^ string_of_int i, "<node id ='" ^
 214           get_id ty ^ "'/>")
 215         (Array.of_list funl)
 216       and funbolid =
 217        Array.mapi
 218         (fun i (_,_,_,bo) ->
 219           "Body " ^ string_of_int i, "<node id ='" ^
 220           get_id bo ^ "'/>")
 221         (Array.of_list funl)
 222       and funnamel =
 223        Array.mapi
 224         (fun i (_,_,_,_) ->
 225           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
 226            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
 227         (Array.of_list funl)
 228       and funrecindexl =
 229        Array.mapi
 230         (fun i (_,_,_,_) ->
 231           "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
 232            "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
 233         (Array.of_list funl)
 234       in
 235        link_hints annotation_window
 236         (Array.concat
 237          [ funtylid ;
 238            funbolid ;
 239            funnamel ;
 240            funrecindexl ;
 241            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
 242          ]
 243         )
 244    | C.ACoFix (id,_,funl) ->
 245       let funtylid =
 246        Array.mapi
 247         (fun i (_,ty,_) ->
 248           "Type " ^ string_of_int i, "<node id ='" ^
 249           get_id ty ^ "'/>")
 250         (Array.of_list funl)
 251       and funbolid =
 252        Array.mapi
 253         (fun i (_,_,bo) ->
 254           "Body " ^ string_of_int i, "<node id ='" ^
 255           get_id bo ^ "'/>")
 256         (Array.of_list funl)
 257       and funnamel =
 258        Array.mapi
 259         (fun i (_,_,_) ->
 260           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
 261            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
 262         (Array.of_list funl)
 263       in
 264        link_hints annotation_window
 265         (Array.concat
 266          [ funtylid ;
 267            funbolid ;
 268            funnamel ;
 269            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
 270          ]
 271         )
 272 ;;
 273
 274 (*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *)
 275 let create_hint_from_obj annotation_window annobj =
 276  let module C = Cic in
 277   match annobj with
 278      C.ADefinition (id,_,bo,ty,_) ->
 279       let boid = get_id bo
 280       and 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            "Body", "<node id = '" ^ boid ^ "'/>" ;
 285            "Type", "<node id = '" ^ tyid ^ "'/>"
 286         |]
 287    | C.AAxiom (id,_,ty,_) ->
 288       let tyid = get_id ty in
 289        link_hints annotation_window
 290         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 291            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 292            "Type", "<node id = '" ^ tyid ^ "'/>"
 293         |]
 294    | C.AVariable (id,_,bo,ty) ->
 295       let tyid = get_id ty in
 296        link_hints annotation_window
 297         (match bo with
 298             None ->
 299              [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 300                 "Type", "<node id = '" ^ tyid ^ "'/>"
 301              |]
 302           | Some bo ->
 303              let boid = get_id bo in
 304               [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 305                  "Body", "<node id = '" ^ boid ^ "'/>" ;
 306                  "Type", "<node id = '" ^ tyid ^ "'/>"
 307               |]
 308         )
 309    | C.ACurrentProof (id,_,conjs,bo,ty) ->
 310       let boid = get_id bo
 311       and tyid = get_id ty
 312       and conjsid = List.map (fun (id,_,_,_) -> id) conjs in
 313        link_hints annotation_window
 314 (*CSC: never tested since the introduction of the new Metas *)
 315         (Array.append
 316           [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 317              "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 318              "Body", "<node id = '" ^ boid ^ "'/>" ;
 319              "Type", "<node id = '" ^ tyid ^ "'/>"
 320           |]
 321           (Array.mapi
 322             (fun i id ->
 323               "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
 324             ) (Array.of_list conjsid)
 325           )
 326         )
 327    | C.AInductiveDefinition (id,itl,_,_) ->
 328       let itlids =
 329        List.map
 330         (fun (_,_,arity,cons) ->
 331           get_id arity,
 332           List.map (fun (_,ty,_) -> get_id ty) cons
 333         ) itl
 334       in
 335        link_hints annotation_window
 336         (Array.concat
 337           [
 338            [| "Ingredients","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
 339            (Array.mapi
 340              (fun i _ ->
 341                "Type Name " ^ string_of_int i,
 342                "<attribute name = 'name' child = '" ^ string_of_int i ^
 343                 "' id = '" ^ id ^ "'/>"
 344              ) (Array.of_list itlids)
 345            ) ;
 346            (Array.mapi
 347              (fun i (id,_) ->
 348                "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
 349              ) (Array.of_list itlids)
 350            ) ;
 351            (Array.concat
 352             (list_mapi
 353              (fun i (_,consid) ->
 354               (Array.mapi
 355                 (fun j _ ->
 356                   "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j,
 357                   "<attribute name = 'name' id = '" ^ id ^
 358                    "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
 359                    string_of_int j ^ "'/>"
 360                 ) (Array.of_list consid)
 361               ) ;
 362              ) itlids
 363             )
 364            ) ;
 365            (Array.concat
 366             (list_mapi
 367              (fun i (_,consid) ->
 368               (Array.mapi
 369                 (fun j id ->
 370                   "Constructor " ^ string_of_int i ^ " " ^ string_of_int j,
 371                   "<node id = '" ^ id ^ "'/>"
 372                 ) (Array.of_list consid)
 373               ) ;
 374              ) itlids
 375             )
 376            )
 377           ]
 378         )
 379 ;;
 380
 381 exception IdUnknown of string;;
 382
 383 let create_hints annotation_window ids_to_targets xpath =
 384  try
 385   match Hashtbl.find ids_to_targets xpath with
 386      Cic.Object annobj -> create_hint_from_obj annotation_window annobj
 387    | Cic.Term annterm -> create_hint_from_term annotation_window annterm
 388 (*CSC: never tested since the introduction of the new Metas *)
 389    | Cic.Hypothesis _
 390    | Cic.Conjecture _ -> assert false
 391  with
 392   Not_found -> raise (IdUnknown xpath)
 393 ;;