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