Source file GuiTactic.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It 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 Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Tactical

(* -------------------------------------------------------------------------- *)
(* --- Composer                                                           --- *)
(* -------------------------------------------------------------------------- *)

class type composer =
  object
    method title : string
    method descr : string
    method target : selection
    method ranged : bool
    method is_valid : selection -> bool
    method get_value : selection
    method set_value : selection -> unit
  end

class type browser =
  object
    method title : string
    method descr : string
    method target : selection
    method search : (unit named -> unit) -> int -> bool
    method choose : string option -> unit
  end

(* -------------------------------------------------------------------------- *)
(* --- Field Widget                                                       --- *)
(* -------------------------------------------------------------------------- *)

class virtual wfield =
  object(self)
    method wfield = (self :> wfield)
    val mutable target = Empty
    method target = target
    method select tgt = target <- tgt
    method compose_with (_ : composer -> unit) = ()
    method browse_with (_ : browser -> unit) = ()
    method clear = self#reset ; target <- Empty
    method virtual reset : unit
    method virtual connect : (unit -> unit) -> unit
    method virtual update :
      ?enabled:bool -> ?title:string -> ?tooltip:string ->
      ?range:bool -> ?vmin:int -> ?vmax:int ->
      ?filter:(Lang.F.term -> bool) -> string -> unit
  end

(* -------------------------------------------------------------------------- *)
(* --- Checkbox Widget                                                    --- *)
(* -------------------------------------------------------------------------- *)

class checkbox
    (tac : Tactical.t) (form : Wpane.form) (field : bool field) =
  let s = Tactical.signature field in
  let button = new Widget.checkbox ~label:s.title ~tooltip:s.descr () in
  object
    inherit wfield
    initializer
      begin
        form#add_field ~field:`Compact button#coerce ;
        button#connect (tac#set_field field) ;
      end
    method reset = button#set s.value
    method connect = button#on_event
    method update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id =
      if id = Tactical.ident field then
        begin
          Wutil.on enabled button#set_visible ;
          Wutil.on tooltip button#set_tooltip ;
          Wutil.on title button#set_label ;
          ignore filter ;
          ignore vmin ;
          ignore vmax ;
          ignore range ;
        end
  end

(* -------------------------------------------------------------------------- *)
(* --- Spinner Widget                                                     --- *)
(* -------------------------------------------------------------------------- *)

class spinner
    (tac : Tactical.t) (form : Wpane.form) (field : int field)
    (range : int range) =
  let s = Tactical.signature field in
  let spin = new Widget.spinner
    ?min:range.vmin ?max:range.vmax
    ~step:range.vstep
    ~value:s.value
    ~tooltip:s.descr () in
  object
    inherit wfield
    initializer
      begin
        form#add_field ~label:s.title ~field:`Compact spin#coerce ;
        spin#connect (tac#set_field field) ;
      end
    method reset = spin#set s.value
    method connect = spin#on_event
    method update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id =
      if id = Tactical.ident field then
        begin
          Wutil.on enabled spin#set_visible ;
          Wutil.on tooltip spin#set_tooltip ;
          Wutil.on vmin spin#set_min ;
          Wutil.on vmax spin#set_max ;
          ignore title ;
          ignore range ;
          ignore filter ;
        end
  end

(* -------------------------------------------------------------------------- *)
(* --- Composer Widget                                                    --- *)
(* -------------------------------------------------------------------------- *)

class mkcomposer
    (tac : Tactical.t) (form : Wpane.form) (field : selection field)
    (accept : Lang.F.term -> bool)
    (pp : Format.formatter -> Tactical.selection -> unit) =
  let s = Tactical.signature field in
  let head = new Widget.label ~style:`Label ~align:`Left () in
  let edit = new Widget.button ~icon:`EDIT ~tooltip:s.descr () in
  let hbox = Wbox.(hbox [ h head ; w ~padding:8 edit ]) in
  object(self)
    inherit wfield
    initializer form#add_row hbox#coerce
    val mutable wtitle = s.title
    val mutable wdescr = s.descr
    val mutable wvalid = accept
    val mutable ranged = false
    val mutable demon = []
    method private updated =
      match tac#get_field field with
      | Empty ->
        Pretty_utils.ksfprintf head#set_text "%s: -" wtitle
      | value ->
        let text =
          Format.asprintf "@[<hov 2>%s: %a@]" wtitle pp value in
        let msg =
          if String.length text <= 20 then text else
            String.sub text 0 17 ^ "..." in
        head#set_text msg

    (* --- Composer API ---- *)
    method composer = (self :> composer)
    method title = wtitle
    method descr = wdescr
    method ranged = ranged
    method is_valid = function
      | Empty -> false
      | Compose(Range(a,b)) -> ranged && (a <= b)
      | _ as s ->
        try wvalid (Tactical.selected s)
        with _ -> false
    method get_value = tac#get_field field
    method set_value v =
      tac#set_field field v ;
      self#updated ;
      List.iter (fun f -> f ()) demon
    method! compose_with f = edit#connect (fun () -> f self#composer)
    (* --- Wfield API ---- *)
    method reset =
      wtitle <- s.title ;
      wdescr <- s.descr ;
      wvalid <- accept ;
      tac#set_field field Tactical.Empty ;
      self#updated
    method connect f = demon <- demon @ [f]
    method update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id =
      if id = Tactical.ident field then
        begin
          Wutil.on enabled hbox#set_visible ;
          Wutil.on title (fun s -> wtitle <- s) ;
          Wutil.on tooltip (fun d -> wdescr <- d) ;
          Wutil.on filter (fun f -> wvalid <- f) ;
          Wutil.on range (fun r -> ranged <- r) ;
          ignore vmin ; ignore vmax ;
          self#updated
        end
  end

(* -------------------------------------------------------------------------- *)
(* --- Search Widget                                                      --- *)
(* -------------------------------------------------------------------------- *)

exception StopLookup

class ['a] mksearch
    (tac : Tactical.t) (form : Wpane.form) (field : 'a named option field)
    (browser : 'a Tactical.browser)
  =
  let s = Tactical.signature field in
  let head = new Widget.label ~style:`Label ~align:`Left () in
  let edit = new Widget.button ~icon:`FIND ~tooltip:s.descr () in
  let hbox = Wbox.(hbox [ h head ; w ~padding:8 edit ]) in
  object(self)
    inherit wfield
    initializer form#add_row hbox#coerce ;
    val mutable wtitle = s.title
    val mutable wdescr = s.descr
    val items : (string,'a named) Hashtbl.t = Hashtbl.create 7
    val mutable demon = []
    method private updated =
      match tac#get_field field with
      | None ->
        Pretty_utils.ksfprintf head#set_text "%s: -" wtitle
      | Some item ->
        begin
          let text = item.title in
          let msg =
            if String.length text <= 20 then text else
              String.sub text 0 17 ^ "..." in
          head#set_text msg ;
          head#set_tooltip item.descr ;
        end

    (* --- Browser API --- *)
    method browser = (self :> browser)

    method choose item =
      let value = match item with
        | Some id ->
          (try Some(Hashtbl.find items id)
           with Not_found -> None)
        | None -> None in
      tac#set_field field value ;
      self#updated ;
      List.iter (fun f -> f ()) demon

    method search f n =
      let count = ref n in
      Hashtbl.clear items ;
      try
        browser
          (fun item ->
             if !count <= 0 then raise StopLookup ;
             Hashtbl.add items item.vid item ;
             f { item with value = () } ;
             decr count ;
          ) target ; true
      with StopLookup ->
        false

    method! browse_with f = edit#connect (fun () -> f self#browser)

    (* --- Wfield API --- *)
    method title = wtitle
    method descr = wdescr
    method reset =
      wtitle <- s.title ;
      wdescr <- s.descr ;
      tac#set_field field None ;
      Hashtbl.clear items ;
      self#updated ;
    method connect f = demon <- demon @ [f]
    method update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id =
      if id = Tactical.ident field then
        begin
          Wutil.on enabled hbox#set_visible ;
          Wutil.on title (fun s -> wtitle <- s) ;
          Wutil.on tooltip (fun d -> wdescr <- d) ;
          ignore filter ; ignore range ;
          ignore vmin ; ignore vmax ;
        end
  end

(* -------------------------------------------------------------------------- *)
(* --- Selector Widget                                                    --- *)
(* -------------------------------------------------------------------------- *)

class ['a] selector
    (tac : Tactical.t) (form : Wpane.form) (field : 'a field)
    (options : 'a Tactical.named list) (equal : 'a -> 'a -> bool) =
  let s = Tactical.signature field in
  let lookup a =
    try List.find (fun v -> equal v.value a) options
    with Not_found ->
      { title = "" ; descr = "(unknown item)" ; vid = "unknown" ; value=a }
  in
  let default = lookup s.value in
  let render item = item.title in
  let combo = new Widget.menu ~default ~render ~items:options () in
  object
    inherit wfield
    initializer
      begin
        form#add_field ~label:s.title ~field:`Compact combo#coerce ;
        combo#connect (fun opt -> tac#set_field field opt.value) ;
      end
    method reset = combo#set default
    method connect = combo#on_event
    method update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id =
      if id = Tactical.ident field then
        begin
          Wutil.on enabled combo#widget#set_visible ;
          Wutil.on tooltip combo#set_tooltip ;
          ignore filter ;
          ignore title ;
          ignore vmin ;
          ignore vmax ;
          ignore range ;
        end
  end

(* -------------------------------------------------------------------------- *)
(* --- Dispatcher                                                         --- *)
(* -------------------------------------------------------------------------- *)

let wfield tac form pp = function
  | Checkbox fd -> (new checkbox tac form fd)#wfield
  | Spinner(fd,r) -> (new spinner tac form fd r)#wfield
  | Selector(fd,opt,eq) -> (new selector tac form fd opt eq)#wfield
  | Composer(fd,f) -> (new mkcomposer tac form fd f pp)#wfield
  | Search(fd,browser,_) -> (new mksearch tac form fd browser)#wfield

(* -------------------------------------------------------------------------- *)
(* --- Tactic Widget                                                      --- *)
(* -------------------------------------------------------------------------- *)

type edited = {
  tree : ProofEngine.tree ;
  target : selection ;
  browser : (browser -> unit) ;
  composer : (composer -> unit) ;
  process : (tactical -> selection -> process -> unit) ;
}

class tactic
    (tac : tactical)
    (pp : Format.formatter -> Tactical.selection -> unit) =
  let form = new Wpane.form () in
  let descr = new Widget.label ~style:`Descr ~width:24 ~align:`Left () in
  object(self)

    val mutable title = tac#title
    val mutable wfields : wfield list = []
    val mutable edited : edited option = None
    val mutable hints = Fmap.create ()
    val mutable error = false

    inherit Wpalette.tool ~content:form#widget () as dongle

    initializer
      begin
        form#add_row ~xpadding:4 ~ypadding:2 ~field:`Compact descr#coerce ;
        self#set_action () ;
        wfields <- List.map (wfield tac form pp) tac#params ;
        List.iter (fun fd -> fd#connect self#updated) wfields ;
        List.iter (fun fd -> fd#compose_with self#compose) wfields ;
        List.iter (fun fd -> fd#browse_with self#browse) wfields ;
        self#set_tooltip
          (if wfields = [] then "Tactic Details" else "Configure Tactic") ;
      end

    (* -------------------------------------------------------------------------- *)
    (* --- Panel API                                                          --- *)
    (* -------------------------------------------------------------------------- *)

    method! set_label =
      fun msg -> title <- msg ; dongle#set_label msg
    method set_title : 'a. 'a formatter =
      fun msg -> Pretty_utils.ksfprintf self#set_label msg
    method set_descr : 'a. 'a formatter =
      fun msg -> Pretty_utils.ksfprintf descr#set_text msg

    (* -------------------------------------------------------------------------- *)
    (* --- Feedback API                                                       --- *)
    (* -------------------------------------------------------------------------- *)

    method pool = match edited with
      | None -> assert false
      | Some { tree } -> ProofEngine.pool tree

    method interactive = self#is_active
    method get_title = title
    method has_error = error
    method set_error : 'a. 'a formatter =
      begin fun msg ->
        error <- true ;
        descr#set_fg (`NAME "red") ;
        Pretty_utils.ksfprintf descr#set_text msg ;
      end

    method update_field :
      'a. ?enabled:bool -> ?title:string -> ?tooltip:string ->
      ?range:bool -> ?vmin:int -> ?vmax:int ->
      ?filter:(Lang.F.term -> bool) -> 'a field -> unit =
      fun ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter field ->
      let id = Tactical.ident field in
      List.iter (fun (fd : wfield) ->
          fd#update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id
        ) wfields

    (* -------------------------------------------------------------------------- *)
    (* --- Widget Behavior                                                    --- *)
    (* -------------------------------------------------------------------------- *)

    method private reset_dongle =
      begin
        self#set_label tac#title ;
        descr#set_text tac#descr ;
        if error then descr#set_fg `NORMAL ;
        error <- false ;
        edited <- None ;
      end

    method private reset_fields =
      List.iter (fun fd -> fd#clear) wfields

    method private compose widget =
      match edited with
      | None -> ()
      | Some edited -> self#set_action () ; edited.composer widget

    method private browse widget =
      match edited with
      | None -> ()
      | Some edited -> self#set_action () ; edited.browser widget

    method private updated () =
      match edited with
      | None -> ()
      | Some { process ; composer ; browser ; target ; tree } ->
        self#select ~process ~composer ~browser ~tree target

    method clear =
      begin
        self#reset_dongle ;
        self#reset_fields ;
        self#set_status `FIND ;
        self#set_action () ;
      end

    method targeted = match edited with None -> false | Some _ -> true

    method private status target =
      List.iter (fun fd -> fd#select target) wfields ;
      try Lang.local ~pool:self#pool (tac#select (self :> feedback)) target
      with Not_found | Exit -> Not_applicable

    method select ~process ~browser ~composer ~tree
        (target : selection) =
      begin
        self#reset_dongle ;
        edited <- Some { process ; composer ; browser ; target ; tree } ;
        let status = self#status target in
        match status , error with
        | Not_applicable , _ ->
          self#set_visible false ;
          self#set_status `FIND ;
          self#set_action () ;
        | Not_configured , _ | Applicable _ , true ->
          self#set_visible true ;
          self#set_status `DIALOG_WARNING ;
          self#set_action () ;
        | Applicable proc , false ->
          self#set_visible true ;
          self#set_status `APPLY ;
          let callback () = process tac target proc in
          self#set_action ~callback () ;
      end

  end

(* -------------------------------------------------------------------------- *)
(* --- Strategies                                                         --- *)
(* -------------------------------------------------------------------------- *)

module User = Gtk_helper.Configuration

type hform = {
  search : Strategy.heuristic ;
  widget : Widget.checkbox ;
}

let hcompare f g = String.compare f.search#title g.search#title

let spinner ~(form:Wpane.form) ~default ~label ~tooltip =
  let config = "wp.strategies." ^ label in
  let value = User.find_int ~default config in
  let spinner = new Widget.spinner ~min:1 ~value ~tooltip () in
  spinner#connect (User.set_int config) ;
  form#add_field ~label spinner#coerce ;
  spinner

let checkbox ~(form:Wpane.form) ~default ~label ~tooltip =
  let config = "wp.strategies." ^ label in
  let value = User.find_bool ~default config in
  let checkbox = new Widget.checkbox ~label ~tooltip () in
  checkbox#set value ;
  checkbox#connect (User.set_bool config) ;
  form#add_field ~label checkbox#coerce ;
  checkbox

type auto_callback = depth:int -> width:int -> Strategy.heuristic list -> unit

class autosearch () =
  let form = new Wpane.form () in
  let depth = spinner ~form ~default:1 ~label:"Depth"
      ~tooltip:"Limit the number of nested strategies" in
  let width = spinner ~form ~default:16 ~label:"Width"
      ~tooltip:"Limit the number of pending goals" in
  object(self)
    inherit Wpalette.tool
        ~content:form#widget
        ~label:"Auto"
        ~tooltip:"Automated proof search (-wp-auto)" ()
    val mutable hforms : hform list = []
    val mutable demon : auto_callback option = None

    method register (search : Strategy.heuristic) =
      begin
        let widget = new Widget.checkbox
          ~label:search#title ~tooltip:search#descr () in
        let config = "wp.strategies." ^ search#id in
        let default = User.find_bool ~default:true config in
        widget#set default ;
        widget#connect (User.set_bool config) ;
        widget#on_event self#update ;
        form#add_row widget#coerce ;
        let hform = { search ; widget } in
        hforms <- List.merge hcompare [hform] hforms
      end

    method private update () =
      match demon with
      | None ->
        self#set_visible false
      | Some _ ->
        self#set_visible true ;
        if List.exists (fun h -> h.widget#get) hforms then
          begin
            self#set_status `APPLY ;
            self#set_action ~callback:self#callback () ;
          end
        else
          begin
            self#set_status `INDEX ;
            self#set_action ()
          end

    method private callback () =
      match demon with
      | Some f ->
        let hs =
          List.fold_right
            (fun h hs -> if h.widget#get then h.search :: hs else hs)
            hforms [] in
        f ~depth:depth#get ~width:width#get hs
      | None -> ()

    method connect f = demon <- f ; self#update ()
  end

(* -------------------------------------------------------------------------- *)
(* --- Proof Strategies                                                   --- *)
(* -------------------------------------------------------------------------- *)

type callback = (depth:int -> ProofStrategy.strategy option -> unit)

type strategy = {
  strategy : ProofStrategy.strategy ;
  button : Widget.button ;
}

class strategies () =
  let form = new Wpane.form () in
  let depth = spinner ~form ~default:1 ~label:"Auto depth"
      ~tooltip:"Depth of exploration" in
  let hints = checkbox ~form ~default:true ~label:"Hints only"
      ~tooltip:"Display hints for the current goal" in
  object(self)
    inherit Wpalette.tool
        ~content:form#widget
        ~label:"Strategies"
        ~tooltip:"Run the full Proof Strategy Engine (-wp-strategy)" ()

    val mutable registered = false
    val mutable proofhints : ProofStrategy.strategy list = []
    val mutable strategies : strategy list = []
    val mutable callback : callback option = None

    initializer hints#connect (fun _ -> self#update)

    method register (s : ProofStrategy.strategy) =
      begin
        registered <- true ;
        let label = ProofStrategy.name s in
        let tooltip = Format.asprintf "%a: strategy %s (single step)"
            Filepath.pp_pos (fst @@ ProofStrategy.loc s) label in
        let button = new Widget.button ~icon:`MEDIA_PLAY ~label ~tooltip () in
        button#set_visible false ;
        button#connect (self#strategy s) ;
      end

    method connect ?(hints=[]) (cb : callback option) =
      callback <- cb ;
      proofhints <- hints ;
      self#update

    method private strategy (s : ProofStrategy.strategy) () =
      Option.iter (fun fn -> fn ~depth:depth#get (Some s)) callback

    method private explore () =
      Option.iter (fun fn -> fn ~depth:depth#get None) callback

    method private setvisible ?(filter=false) ?(rank=0) (s: strategy) =
      let show = not filter || rank > 0 in
      s.button#set_visible show ;
      if show then
        let name = ProofStrategy.name s.strategy in
        if rank = 0 then
          s.button#set_label name
        else
          Pretty_utils.ksfprintf s.button#set_label "%s (#%d)" name rank

    method private setrank (s: strategy) =
      let filter = hints#get in
      let rec apply (s:strategy) rank = function
        | [] -> self#setvisible s ~filter
        | h::hs ->
          if s.strategy == h then
            self#setvisible s ~rank
          else
            self#setvisible s ~filter ;
          apply s (succ rank) hs
      in apply s 1 proofhints

    method private update =
      if callback = None || not registered then
        self#set_visible false
      else
        begin
          self#set_visible true ;
          self#set_status `APPLY ;
          self#set_action ~callback:self#explore () ;
          List.iter self#setrank strategies
        end

  end

(* -------------------------------------------------------------------------- *)