create_session.ml 3.13 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
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 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
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
        let d = Driver.load_driver env p.Whyconf.driver [] in
        (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
    []


(* a dummy keygen function for sessions *)
let keygen ?parent () = ()

(* create an empty session in the current directory *)
61
let env_session,_,_ =
MARCHE Claude's avatar
MARCHE Claude committed
62
  let dummy_session : unit Session.session = Session.create_session "." in
63
  Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true
64
    dummy_session env config
MARCHE Claude's avatar
MARCHE Claude committed
65 66

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

(* explore the theories in that file *)
77
let theories = file.Session.file_theories
MARCHE Claude's avatar
MARCHE Claude committed
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
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
          ~keygen
          ~obsolete:true
          ~archived:false
          ~timelimit:5
          ~memlimit:1000
          ~edit:None
          g p.Whyconf.prover Session.Scheduled
94
      in ())
MARCHE Claude's avatar
MARCHE Claude committed
95 96 97 98 99 100 101 102 103 104 105
    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