test.ml 6.6 KB
Newer Older
MARCHE Claude's avatar
manager  
MARCHE Claude committed
1

MARCHE Claude's avatar
MARCHE Claude committed
2
open Format
MARCHE Claude's avatar
manager  
MARCHE Claude committed
3
open Why
4
open Whyconf
MARCHE Claude's avatar
manager  
MARCHE Claude committed
5

MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9
(******************************)
(* loading user configuration *)
(******************************)

10
(*
MARCHE Claude's avatar
manager  
MARCHE Claude committed
11
let autodetection () = 
12
  let alt_ergo = {
13 14 15
    name    = "Alt-Ergo";
    command = "alt-ergo %s";
    driver  = "drivers/alt_ergo.drv" }
16 17
  in
  let z3 = {
18 19 20
    name    = "Z3";
    command = "z3 -smt -in";
    driver  = "drivers/z3.drv" }
21 22
  in
  let cvc3 = {
23 24 25
    name    = "CVC3";
    command = "cvc3 -lang smt";
    driver  = "drivers/cvc3.drv" }
26 27
  in
  let coq = {
28 29 30
    name    = "Coq";
    command = "coqc %s";
    driver  = "drivers/coq.drv" }
31 32 33 34 35 36 37
  in
  let provers = Util.Mstr.empty in
  let provers = Util.Mstr.add "alt-ergo" alt_ergo provers in
  let provers = Util.Mstr.add "z3" z3 provers in
  let provers = Util.Mstr.add "cvc3" cvc3 provers in
  let provers = Util.Mstr.add "coq" coq provers in
  let config = {
38
    conf_file = "why.conf";
39
    loadpath  = ["theories"];
MARCHE Claude's avatar
MARCHE Claude committed
40
    timelimit = Some 2;
41 42 43 44
    memlimit  = None;
    provers   = provers }
  in
  save_config config
45
*)
46 47

let config = 
MARCHE Claude's avatar
test  
MARCHE Claude committed
48
  try 
49
    Whyconf.read_config None
50 51 52 53 54 55 56 57 58 59
  with 
      Not_found -> 
        eprintf "No config file found.@.";
(* "Running autodetection of provers.@.";
        autodetection ();
*)
        exit 1
    | Whyconf.Error e ->
        eprintf "Error while reading config file: %a@." Whyconf.report e;
        exit 1
MARCHE Claude's avatar
manager  
MARCHE Claude committed
60

61
let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) config.loadpath
MARCHE Claude's avatar
manager  
MARCHE Claude committed
62

63
let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
MARCHE Claude's avatar
manager  
MARCHE Claude committed
64

MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69 70 71 72 73
let timelimit = 
  match config.timelimit with
    | None -> 2
    | Some n -> n

(********************)
(* opening database *)
(********************)

MARCHE Claude's avatar
MARCHE Claude committed
74 75 76
let fname = "tests/test-claude"

let () = Db.init_base (fname ^ ".db")
MARCHE Claude's avatar
test2  
MARCHE Claude committed
77

78 79
let get_driver name = 
  let pi = Util.Mstr.find name config.provers in
80
  Why.Driver.load_driver env pi.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
81

MARCHE Claude's avatar
MARCHE Claude committed
82 83 84 85 86 87
type prover_data =
    { prover : Db.prover;
      command : string;
      driver : Why.Driver.driver;
    }

88
let provers_data =
MARCHE Claude's avatar
MARCHE Claude committed
89
  printf "===============================@\nProvers: ";
90 91 92 93 94
  let l = 
    Util.Mstr.fold
    (fun id conf acc ->
       let name = conf.Whyconf.name in
       printf " %s, " name;
MARCHE Claude's avatar
MARCHE Claude committed
95 96 97
       { prover = Db.get_prover name;
         command = conf.Whyconf.command;
         driver = get_driver id; } :: acc
98 99
    ) config.provers []
  in
MARCHE Claude's avatar
MARCHE Claude committed
100 101
  printf "@\n===============================@.";
  l 
102
   
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106
let () = 
  printf "previously known goals:@\n";
  List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
  printf "@."
MARCHE Claude's avatar
MARCHE Claude committed
107 108 109 110

(***********************)
(* Parsing input file  *)
(***********************)
MARCHE Claude's avatar
MARCHE Claude committed
111 112 113 114 115 116 117 118 119 120 121 122 123
   
let rec report fmt = function
  | Lexer.Error e ->
      fprintf fmt "lexical error: %a" Lexer.report e;
  | Loc.Located (loc, e) ->
      fprintf fmt "%a%a" Loc.report_position loc report e
  | Parsing.Parse_error ->
      fprintf fmt "syntax error"
  | Denv.Error e ->
      Denv.report fmt e
  | Typing.Error e ->
      Typing.report fmt e
  | Decl.UnknownIdent i ->
124
      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
MARCHE Claude's avatar
MARCHE Claude committed
125 126
  | Driver.Error e ->
      Driver.report fmt e
MARCHE Claude's avatar
MARCHE Claude committed
127 128
  | Config.Dynlink.Error e ->
      fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
MARCHE Claude's avatar
MARCHE Claude committed
129 130 131 132 133 134 135 136 137 138 139 140 141 142
  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)


let m : Why.Theory.theory Why.Theory.Mnm.t =
  try
    let cin = open_in (fname ^ ".why") in
    let m = Why.Typing.read_channel env fname cin in
    close_in cin;
    eprintf "Parsing/Typing Ok@.";
    m
  with e -> 
    eprintf "%a@." report e;
    exit 1

MARCHE Claude's avatar
MARCHE Claude committed
143 144 145 146
(***************************)
(* Process input theories  *)
(* add corresponding tasks *)
(***************************)
MARCHE Claude's avatar
MARCHE Claude committed
147

148
let add_task (tname : string) (task : Why.Task.task) acc =
149
  let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_string in
MARCHE Claude's avatar
MARCHE Claude committed
150 151
  eprintf "doing task: tname=%s, name=%s@." tname name;
  Db.add_or_replace_task ~tname ~name task :: acc
152 153 154 155 156 157

let do_theory tname th glist =
  let tasks = Why.Task.split_theory th None in
  List.fold_right (add_task tname) tasks glist


MARCHE Claude's avatar
MARCHE Claude committed
158 159 160 161
(***********************************)
(* back to the eighties:           *)
(* A good-old text-based interface *)
(***********************************)
MARCHE Claude's avatar
test2  
MARCHE Claude committed
162

163 164 165
let goal_menu g = 
  try
    while true do 
MARCHE Claude's avatar
MARCHE Claude committed
166
      printf "Choose a prover:@.";
167 168 169
      let _,menu = List.fold_left
        (fun (i,acc) p -> 
           let i = succ i in
MARCHE Claude's avatar
MARCHE Claude committed
170
           printf "%2d: try %s@." i (Db.prover_name p.prover);
171 172 173 174
           (i,(i,p)::acc)) (0,[]) provers_data
      in
      let s = read_line () in
      (try 
175
         let i = try int_of_string s with Failure _ -> raise Not_found in
176
         let p = List.assoc i menu in
MARCHE Claude's avatar
MARCHE Claude committed
177
         let call = 
178
	   try
MARCHE Claude's avatar
MARCHE Claude committed
179
             Db.try_prover ~debug:false ~timelimit ~memlimit:0 
180 181 182 183
               ~prover:p.prover ~command:p.command ~driver:p.driver g 
           with Db.AlreadyAttempted ->
             printf "Proof already attempted, no need to rerun@.";
             raise Exit
MARCHE Claude's avatar
MARCHE Claude committed
184
	 in
185 186 187
         call ();
         raise Exit
       with Not_found -> 
188 189 190 191 192 193 194
         printf "unknown choice@.");
    done
  with Exit -> ()
    
let main_loop goals =
  try
    while true do
MARCHE Claude's avatar
MARCHE Claude committed
195
      printf "======================@\nMenu:@.";
196 197 198 199
      printf " 0: exit@.";
      let _,menu = List.fold_left
        (fun (i,acc) g -> 
           let i = succ i in
MARCHE Claude's avatar
MARCHE Claude committed
200 201
           printf "%2d: name='%s', proved=%b@." i 
             (Db.goal_name g) (Db.goal_proved g);
MARCHE Claude's avatar
MARCHE Claude committed
202
           let e = Db.external_proofs g in
MARCHE Claude's avatar
MARCHE Claude committed
203 204 205 206 207 208 209 210 211
           List.iter 
             (fun e ->
                let p = Db.prover e in
                printf 
                  "    external proof: prover=%s, obsolete=%b\
                       , result=%a, time=%.2f@."
                  (Db.prover_name p) (Db.proof_obsolete e) 
                  Db.print_status (Db.status e)
                  (Db.result_time e))
MARCHE Claude's avatar
MARCHE Claude committed
212
             
MARCHE Claude's avatar
MARCHE Claude committed
213
             e;
214 215 216 217 218 219 220 221 222 223 224 225
           (i,(i,g)::acc)) (0,[]) goals
      in
      let s = read_line () in
      (try 
         let i = int_of_string s in
         if i=0 then raise Exit; 
         goal_menu (List.assoc i menu)
       with Not_found | Failure _ -> 
         printf "unknown choice@.");
    done
  with Exit -> ()
  
MARCHE Claude's avatar
MARCHE Claude committed
226 227 228 229 230

(****************)
(* Main program *)
(****************)

MARCHE Claude's avatar
test2  
MARCHE Claude committed
231
let () =
MARCHE Claude's avatar
MARCHE Claude committed
232 233
  eprintf "looking for goals@.";
  let add_th t th mi = 
234
    eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
MARCHE Claude's avatar
MARCHE Claude committed
235 236
    Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi 
  in
237
  let do_th _ (t,th) glist = 
238
    eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
239
    do_theory t th glist  
MARCHE Claude's avatar
MARCHE Claude committed
240
  in
241 242 243 244 245 246 247 248 249
  let goals = 
    Why.Ident.Mid.fold do_th (Why.Theory.Mnm.fold add_th m Why.Ident.Mid.empty) []
  in
  eprintf "Production of goals done@.";
  try
    main_loop goals
  with Exit -> eprintf "Exiting...@."


MARCHE Claude's avatar
MARCHE Claude committed
250 251 252 253 254 255 256


(*
Local Variables: 
compile-command: "make -C ../.. bin/manager.byte"
End: 
*)
MARCHE Claude's avatar
test2  
MARCHE Claude committed
257 258


MARCHE Claude's avatar
test  
MARCHE Claude committed
259

MARCHE Claude's avatar
manager  
MARCHE Claude committed
260