create_session.ml 3.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11 12 13 14 15

(*******************

This file builds a new session from a given file.

16
To each goal is added as many proof attempts as provers
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
found in the configuration.


******************)

open Format

(* opening the Why3 library *)
open Why3

(* access to the Why configuration *)

(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)

(* loading the drivers *)
let provers =
  Whyconf.Mprover.fold
    (fun _ p acc ->
      try
45
        let d = Whyconf.load_driver main env p.Whyconf.driver [] in
MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49 50 51 52 53 54 55
        (p,d)::acc
      with e ->
        let p = p.Whyconf.prover in
        eprintf "Failed to load driver for %s %s: %a@."
          p.Whyconf.prover_name p.Whyconf.prover_version
          Exn_printer.exn_printer e;
        exit 1)
    provers
    []

56
let dummy_keygen ?parent () = ()
MARCHE Claude's avatar
MARCHE Claude committed
57 58 59

(* a dummy keygen function for sessions *)
(* create an empty session in the current directory *)
60
let env_session,_,_ =
MARCHE Claude's avatar
MARCHE Claude committed
61
  let dummy_session : unit Session.session = Session.create_session "." in
62 63 64
  let ctxt = Session.mk_update_context
    ~allow_obsolete_goals:true
    dummy_keygen
65 66
  in
  Session.update_session ~ctxt dummy_session env config
MARCHE Claude's avatar
MARCHE Claude committed
67 68

(* adds a file in the new session *)
69
let file : unit Session.file =
Andrei Paskevich's avatar
Andrei Paskevich committed
70
  let file_name = "examples/logic/hello_proof.why" in
MARCHE Claude's avatar
MARCHE Claude committed
71
  try
72
    Session.add_file ~keygen:dummy_keygen env_session file_name
MARCHE Claude's avatar
MARCHE Claude committed
73 74 75 76 77 78
  with e ->
    eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name
      Exn_printer.exn_printer e;
    exit 1

(* explore the theories in that file *)
79
let theories = file.Session.file_theories
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82 83 84 85 86 87 88
let () = eprintf "%d theories found@." (List.length theories)

(* add proof attempts for each goals in the theories *)

let add_proofs_attempts g =
  List.iter
    (fun (p,d) ->
      let _pa : unit Session.proof_attempt =
        Session.add_external_proof
89
          ~keygen:dummy_keygen
MARCHE Claude's avatar
MARCHE Claude committed
90 91
          ~obsolete:true
          ~archived:false
92 93 94
          ~limit:{Call_provers.empty_limit with
                  Call_provers.limit_time = 5;
                               limit_mem = 1000 }
MARCHE Claude's avatar
MARCHE Claude committed
95 96
          ~edit:None
          g p.Whyconf.prover Session.Scheduled
97
      in ())
MARCHE Claude's avatar
MARCHE Claude committed
98 99 100 101 102 103 104 105 106
    provers

let () =
  List.iter
    (fun th -> List.iter add_proofs_attempts th.Session.theory_goals)
    theories

(* save the session on disk *)
let () = Session.save_session config env_session.Session.session