create_session.ml 3.23 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9
(*                                                                  *)
(*  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
10 11 12 13 14

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

This file builds a new session from a given file.

15
To each goal is added as many proof attempts as provers
MARCHE Claude's avatar
MARCHE Claude committed
16 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
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
    []

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

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

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

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