helm/interface/cicAnnotationHinter.ml

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
   6 (*                                 14/06/2000                                 *)
   7 (*                                                                            *)
   8 (*                                                                            *)
   9 (******************************************************************************)
  10
  11 let deactivate_hints_from annotation_window n =
  12  let annotation_hints = annotation_window#annotation_hints in
  13   for i = n to Array.length annotation_hints - 1 do
  14    annotation_hints.(i)#misc#hide ()
  15   done
  16 ;;
  17
  18 (* CSC: orripilante *)
  19 (* the list of the signal ids *)
  20 let sig_ids = ref ([] : GtkSignal.id list);;
  21
  22 let disconnect_hint annotation_window buttonno =
  23  match !sig_ids with
  24     id::ids ->
  25      annotation_window#annotation_hints.(buttonno)#misc#disconnect id ;
  26      sig_ids := ids
  27   | _ -> assert false
  28 ;;
  29
  30 (* link_hint annotation_window n label hint *)
  31 (* set the label of the nth hint button of annotation_window to label *)
  32 (* and the correspondent hint to hint                                 *)
  33 let link_hint annotation_window buttonno label hint =
  34  let button = annotation_window#annotation_hints.(buttonno) in
  35   sig_ids :=
  36    (button#connect#clicked
  37     (fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
  38    ) :: !sig_ids ;
  39   button#misc#show () ;
  40   match button#children with
  41      [labelw] -> (GMisc.label_cast labelw)#set_text label
  42    | _ -> assert false
  43 ;;
  44
  45 exception TooManyHints;;
  46
  47 let link_hints annotation_window a =
  48  if Array.length a > Array.length annotation_window#annotation_hints then
  49   raise TooManyHints ;
  50  for i = List.length !sig_ids - 1 downto 0 do
  51   disconnect_hint annotation_window i
  52  done ;
  53  Array.iteri
  54   (fun i (label,hint) -> link_hint annotation_window i label hint) a ;
  55  deactivate_hints_from annotation_window (Array.length a)
  56 ;;
  57
  58 let list_mapi f =
  59  let rec aux n =
  60   function
  61      [] -> []
  62    | he::tl -> (f n he)::(aux (n + 1) tl)
  63  in
  64   aux 0
  65 ;;
  66
  67 let get_id annterm =
  68  let module C = Cic in
  69   match annterm with
  70      C.ARel (id,_,_,_)             -> id
  71    | C.AVar (id,_,_)               -> id
  72    | C.AMeta (id,_,_)              -> id
  73    | C.ASort (id,_,_)              -> id
  74    | C.AImplicit (id,_)            -> id
  75    | C.ACast (id,_,_,_)            -> id
  76    | C.AProd (id,_,_,_,_)          -> id
  77    | C.ALambda (id,_,_,_,_)        -> id
  78    | C.AAppl (id,_,_)              -> id
  79    | C.AConst (id,_,_,_)           -> id
  80    | C.AAbst (id,_,_)              -> id
  81    | C.AMutInd (id,_,_,_,_)        -> id
  82    | C.AMutConstruct (id,_,_,_,_,_)-> id
  83    | C.AMutCase (id,_,_,_,_,_,_,_) -> id
  84    | C.AFix (id,_,_,_)             -> id
  85    | C.ACoFix (id,_,_,_)           -> id
  86 ;;
  87
  88 let create_hint_from_term annotation_window annterm =
  89  let module C = Cic in
  90   match annterm with
  91      C.ARel (id,_,_,_) ->
  92       link_hints annotation_window
  93        [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
  94    | C.AVar (id,_,_) ->
  95       link_hints annotation_window
  96        [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
  97    | C.AMeta (id,_,_) ->
  98       link_hints annotation_window
  99        [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
 100    | C.ASort (id,_,_) ->
 101       link_hints annotation_window
 102        [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
 103    | C.AImplicit (id,_) ->
 104       link_hints annotation_window [| |]
 105    | C.ACast (id,_,bo,ty) ->
 106       let boid = get_id bo
 107       and tyid = get_id ty in
 108        link_hints annotation_window
 109         [| "Body", "<node id = '" ^ boid ^ "'/>" ;
 110            "Type", "<node id = '" ^ tyid ^ "'/>"
 111         |]
 112    | C.AProd (id,_,_,ty,bo) ->
 113       let boid = get_id bo
 114       and tyid = get_id ty in
 115        link_hints annotation_window
 116         [| "Binder",
 117             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 118            "Body", "<node id = '" ^ boid ^ "'/>" ;
 119            "Type", "<node id = '" ^ tyid ^ "'/>"
 120         |]
 121    | C.ALambda (id,_,_,ty,bo) ->
 122       let boid = get_id bo
 123       and tyid = get_id ty in
 124        link_hints annotation_window
 125         [| "Binder",
 126             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
 127            "Body", "<node id = '" ^ boid ^ "'/>" ;
 128            "Type", "<node id = '" ^ tyid ^ "'/>"
 129         |]
 130    | C.AAppl (id,_,args) ->
 131       let argsid =
 132        Array.mapi
 133         (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
 134           get_id te ^ "'/>")
 135         (Array.of_list args)
 136       in
 137        link_hints annotation_window argsid
 138    | C.AConst (id,_,_,_) ->
 139       link_hints annotation_window
 140        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 141    | C.AAbst (id,_,_) ->
 142       link_hints annotation_window
 143        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 144    | C.AMutInd (id,_,_,_,_) ->
 145       link_hints annotation_window
 146        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 147    | C.AMutConstruct (id,_,_,_,_,_) ->
 148       link_hints annotation_window
 149        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
 150    | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
 151       let outtyid = get_id outty
 152       and teid = get_id te
 153       and plid =
 154        Array.mapi
 155         (fun i te -> "Pattern " ^ string_of_int i, "<node id ='" ^
 156           get_id te ^ "'/>")
 157         (Array.of_list pl)
 158       in
 159        link_hints annotation_window
 160         (Array.append
 161          [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
 162             "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
 163             "Term", "<node id = '" ^ teid ^ "'/>" ;
 164          |]
 165          plid)
 166    | C.AFix (id,_,_,funl) ->
 167       let funtylid =
 168        Array.mapi
 169         (fun i (_,_,ty,_) ->
 170           "Type " ^ string_of_int i, "<node id ='" ^
 171           get_id ty ^ "'/>")
 172         (Array.of_list funl)
 173       and funbolid =
 174        Array.mapi
 175         (fun i (_,_,_,bo) ->
 176           "Body " ^ string_of_int i, "<node id ='" ^
 177           get_id bo ^ "'/>")
 178         (Array.of_list funl)
 179       and funnamel =
 180        Array.mapi
 181         (fun i (_,_,_,_) ->
 182           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
 183            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
 184         (Array.of_list funl)
 185       and funrecindexl =
 186        Array.mapi
 187         (fun i (_,_,_,_) ->
 188           "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
 189            "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
 190         (Array.of_list funl)
 191       in
 192        link_hints annotation_window
 193         (Array.concat
 194          [ funtylid ;
 195            funbolid ;
 196            funnamel ;
 197            funrecindexl ;
 198            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
 199          ]
 200         )
 201    | C.ACoFix (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       in
 221        link_hints annotation_window
 222         (Array.concat
 223          [ funtylid ;
 224            funbolid ;
 225            funnamel ;
 226            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
 227          ]
 228         )
 229 ;;
 230
 231 (*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *)
 232 let create_hint_from_obj annotation_window annobj =
 233  let module C = Cic in
 234   match annobj with
 235      C.ADefinition (id,_,_,bo,ty,_) ->
 236       let boid = get_id bo
 237       and tyid = get_id ty in
 238        link_hints annotation_window
 239         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 240            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 241            "Body", "<node id = '" ^ boid ^ "'/>" ;
 242            "Type", "<node id = '" ^ tyid ^ "'/>"
 243         |]
 244    | C.AAxiom (id,_,_,ty,_) ->
 245       let tyid = get_id ty in
 246        link_hints annotation_window
 247         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 248            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 249            "Type", "<node id = '" ^ tyid ^ "'/>"
 250         |]
 251    | C.AVariable (id,_,_,ty) ->
 252       let tyid = get_id ty in
 253        link_hints annotation_window
 254         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 255            "Type", "<node id = '" ^ tyid ^ "'/>"
 256         |]
 257    | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
 258       let boid = get_id bo
 259       and tyid = get_id ty
 260       and conjsid = List.map (fun (_,te) -> get_id te) conjs in
 261        link_hints annotation_window
 262         (Array.append
 263           [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
 264              "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
 265              "Body", "<node id = '" ^ boid ^ "'/>" ;
 266              "Type", "<node id = '" ^ tyid ^ "'/>"
 267           |]
 268           (Array.mapi
 269             (fun i id ->
 270               "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
 271             ) (Array.of_list conjsid)
 272           )
 273         )
 274    | C.AInductiveDefinition (id,_,itl,_,_) ->
 275       let itlids =
 276        List.map
 277         (fun (_,_,arity,cons) ->
 278           get_id arity,
 279           List.map (fun (_,ty,_) -> get_id ty) cons
 280         ) itl
 281       in
 282        link_hints annotation_window
 283         (Array.concat
 284           [
 285            [| "Ingredients","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
 286            (Array.mapi
 287              (fun i _ ->
 288                "Type Name " ^ string_of_int i,
 289                "<attribute name = 'name' child = '" ^ string_of_int i ^
 290                 "' id = '" ^ id ^ "'/>"
 291              ) (Array.of_list itlids)
 292            ) ;
 293            (Array.mapi
 294              (fun i (id,_) ->
 295                "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
 296              ) (Array.of_list itlids)
 297            ) ;
 298            (Array.concat
 299             (list_mapi
 300              (fun i (_,consid) ->
 301               (Array.mapi
 302                 (fun j _ ->
 303                   "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j,
 304                   "<attribute name = 'name' id = '" ^ id ^
 305                    "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
 306                    string_of_int j ^ "'/>"
 307                 ) (Array.of_list consid)
 308               ) ;
 309              ) itlids
 310             )
 311            ) ;
 312            (Array.concat
 313             (list_mapi
 314              (fun i (_,consid) ->
 315               (Array.mapi
 316                 (fun j id ->
 317                   "Constructor " ^ string_of_int i ^ " " ^ string_of_int j,
 318                   "<node id = '" ^ id ^ "'/>"
 319                 ) (Array.of_list consid)
 320               ) ;
 321              ) itlids
 322             )
 323            )
 324           ]
 325         )
 326 ;;
 327
 328 exception IdUnknown of string;;
 329
 330 let create_hints annotation_window (annobj,ids_to_targets) xpath =
 331  try
 332   match Hashtbl.find ids_to_targets xpath with
 333      Cic.Object annobj -> create_hint_from_obj annotation_window annobj
 334    | Cic.Term annterm -> create_hint_from_term annotation_window annterm
 335  with
 336   Not_found -> raise (IdUnknown xpath)
 337 ;;