create_session.ml 3.19 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 16 17 18 19 20 21 22 23 24 25

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

This file builds a new session from a given file.

To each goal is added as many proof attempts as provers 
found in the configuration.


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

open Format

(* opening the Why3 library *)
open Why3
26 27
(* opening the Why3 session library *)
open Why3session
MARCHE Claude's avatar
MARCHE Claude committed
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 61 62 63


(* 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 *)
64
let env_session,_,_ =
MARCHE Claude's avatar
MARCHE Claude committed
65
  let dummy_session : unit Session.session = Session.create_session "." in
66 67
  Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true 
    dummy_session env config
MARCHE Claude's avatar
MARCHE Claude committed
68 69 70

(* adds a file in the new session *)
let file : unit Session.file = 
Andrei Paskevich's avatar
Andrei Paskevich committed
71
  let file_name = "examples/logic/hello_proof.why" in
MARCHE Claude's avatar
MARCHE Claude committed
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  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 *)
let theories = file.Session.file_theories 
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
      in ()) 
    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