GuiConfig.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2019                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* ------------------------------------------------------------------------ *)
(* ---  Prover List in Configuration                                    --- *)
(* ------------------------------------------------------------------------ *)

class enabled key =
  object(self)
    inherit [Why3.Whyconf.Sprover.t] Wutil.selector Why3.Whyconf.Sprover.empty

    method private load () =
      let open Gtk_helper.Configuration in
      let prover_of_conf acc = function
        | ConfList [ConfString prover_name;
                    ConfString prover_version;
                    ConfString prover_altern] ->
            Why3.Whyconf.Sprover.add
              Why3.Whyconf.{ prover_name; prover_version; prover_altern }
              acc
        | _ -> acc in
      try
        let data = Gtk_helper.Configuration.find key in
        match data with
        | ConfList data ->
            (List.fold_left prover_of_conf Why3.Whyconf.Sprover.empty data)
        | _ -> Why3.Whyconf.Sprover.empty
      with Not_found -> Why3.Whyconf.Sprover.empty

    method private save () =
      let open Gtk_helper.Configuration in
      let conf_of_prover dp = ConfList Why3.Whyconf.[ConfString dp.prover_name;
                                                     ConfString dp.prover_version;
                                                     ConfString dp.prover_altern] in
      Gtk_helper.Configuration.set key
        (ConfList (List.map conf_of_prover
                     (Why3.Whyconf.Sprover.elements self#get)))

    initializer
      begin
        let settings = self#load () in
        (** select automatically the provers set on the command line *)
        let cmdline = Wp_parameters.Provers.get () in
        let selection = List.fold_left
            (fun acc e ->
               match VCS.Why3_prover.find_opt e with
               | None-> acc
               | Some p -> Why3.Whyconf.Sprover.add p acc)
            settings cmdline
        in
        self#set selection ;
        self#on_event self#save ;
      end

  end

(* ------------------------------------------------------------------------ *)
(* ---  WP Provers Configuration Panel                                  --- *)
(* ------------------------------------------------------------------------ *)

class dp_chooser
    ~(main:Design.main_window_extension_points)
    ~(enabled:enabled)
  =
  let dialog = new Wpane.dialog
    ~title:"Why3 Provers"
    ~window:main#main_window
    ~resize:false () in
  let array = new Wpane.warray () in
  object(self)

    val mutable selected = Why3.Whyconf.Mprover.empty

    method private enable dp e =
      selected <- Why3.Whyconf.Mprover.add dp e selected

    method private lookup dp =
      Why3.Whyconf.Mprover.find dp selected

    method private entry dp =
      let text = VCS.Why3_prover.title dp in
      let sw = new Widget.switch () in
      let lb = new Widget.label ~align:`Left ~text () in
      sw#set (self#lookup dp) ;
      sw#connect (self#enable dp) ;
      let hbox = GPack.hbox ~spacing:10 ~homogeneous:false () in
      hbox#pack ~expand:false sw#coerce ;
      hbox#pack ~expand:true lb#coerce ;
      (object
        method widget = hbox#coerce
        method update () = sw#set (self#lookup dp)
        method delete () = ()
      end)

    method private configure dps =
      begin
        array#set (Why3.Whyconf.Sprover.elements dps) ;
        array#update () ;
      end

    method private detect () =
      begin
        self#configure (VCS.Why3_prover.provers_set ());
      end

    method private apply () =
      enabled#set
        (Why3.Whyconf.Mprover.map_filter
           (function
             | true -> Some ()
             | false -> None)
           selected)

    method run () =
      let dps = VCS.Why3_prover.provers_set () in
      let sel = enabled#get in
      selected <- Why3.Whyconf.Mprover.merge
          (fun _ avail enab ->
             match avail, enab with
             | None, _ -> None
             | Some (), Some () -> Some true
             | Some (), None -> Some false)
          dps sel;
      self#configure dps ;
      dialog#run ()

    initializer
      begin
        dialog#button ~action:(`ACTION self#detect) ~label:"Detect Provers" () ;
        dialog#button ~action:(`CANCEL) ~label:"Cancel" () ;
        dialog#button ~action:(`APPLY) ~label:"Apply" () ;
        array#set_entry self#entry ;
        dialog#add_block array#coerce ;
        dialog#on_value `APPLY self#apply ;
      end

  end

(* ------------------------------------------------------------------------ *)
(* ---  WP Prover Switch Panel                                          --- *)
(* ------------------------------------------------------------------------ *)

type mprover =
  | NONE
  | ERGO
  | COQ
  | WHY of VCS.Why3_prover.t

class dp_button =
  let render = function
    | NONE -> "(none)"
    | ERGO -> "Alt-Ergo (native)"
    | COQ -> "Coq (native)"
    | WHY p when VCS.Why3_prover.has_shortcut p "alt-ergo" ->
        "Alt-Ergo (why3)"
    | WHY dp -> VCS.Why3_prover.title dp in
  let select = function
    | ERGO -> VCS.NativeAltErgo
    | COQ -> VCS.NativeCoq
    | NONE -> VCS.Qed
    | WHY p -> VCS.Why3 p in
  let rec import = function
    | [] -> ERGO
    | spec::others ->
        match VCS.prover_of_name spec with
        | None | Some VCS.Qed -> NONE
        | Some (VCS.NativeAltErgo|VCS.Tactical) -> ERGO
        | Some VCS.NativeCoq -> COQ
        | Some (VCS.Why3 p) ->
            if Why3.Whyconf.Sprover.mem p (VCS.Why3_prover.provers_set ())
            then WHY p
            else import others
  in
  let items = [ NONE ; ERGO ; COQ ] in
  let button = new Widget.menu ~default:ERGO ~render ~items () in
  object(self)
    method coerce = button#coerce
    method widget = (self :> Widget.t)
    method set_enabled = button#set_enabled
    method set_visible = button#set_visible
    val mutable dps = Why3.Whyconf.Sprover.empty

    method update () =
      (* called in polling mode *)
      begin
        let avl = VCS.Why3_prover.provers_set () in
        if Why3.Whyconf.Sprover.equal avl dps then
          begin
            dps <- avl ;
            let dps = Why3.Whyconf.Sprover.elements dps in
            let items = [NONE;ERGO] @ List.map (fun p -> WHY p) dps @ [COQ] in
            button#set_items items
          end ;
        let cur = Wp_parameters.Provers.get () |> import in
        if cur <> button#get then button#set cur ;
      end

    initializer button#connect
        (fun s ->
           let p = select s in
           let p = VCS.name_of_prover p in
           Wp_parameters.Provers.set [p]
        )
  end

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