Driver (en cours)

Makefile.in

@@ -143,7 +143,7 @@ bin/top: $(CMO)
 
 test: bin/why.byte
 	ocamlrun -bt bin/why.byte --print-stdout -I lib/prelude/ src/test.why
-	bin/why.byte --alt-ergo -I lib/prelude/ src/test.why > ergo.why
+	bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ src/test.why > ergo.why
 	timeout 3 alt-ergo ergo.why
 
 # graphical interface

bench/bench.in

@@ -67,6 +67,6 @@ goods lib/prelude --type-only
 echo ""
 
 echo "=== Checking lib/drivers ==="
-drivers lib/drivers
+drivers lib/drivers --driver
 echo ""
 

lib/drivers/alt_ergo.drv

 
 (* Why driver for Alt-Ergo *)
 
-"(* this is a prelude for Alt-Ergo*)"
+prelude "(* this is a prelude for Alt-Ergo*)"
+
+printer "alt-ergo"
+
+call_on_file  "alt-ergo %s"
 
 theory prelude.Int
 
-  "(* this is a prelude for Alt-Ergo arithmetic *)"
+  prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
 
   syntax zero "0"
 

src/core/theory.ml

@@ -374,7 +374,7 @@ let empty_inst = {
 
 module Context = struct
 
-  let create_context =
+  let init_context =
     let known = builtin_theory.th_ctxt.ctxt_known in
     let known = Mid.add builtin_theory.th_name use_builtin known in
     mk_context use_builtin None known Mid.empty
@@ -773,7 +773,7 @@ module Theory = struct
 
   let create_theory n = {
     uc_name   = n;
-    uc_ctxt   = Context.create_context;
+    uc_ctxt   = Context.init_context;
     uc_import = [builtin_theory.th_export];
     uc_export = [builtin_theory.th_export];
     uc_local  = Sid.empty;

src/core/theory.mli

@@ -147,7 +147,7 @@ val empty_inst : th_inst
 
 module Context : sig
 
-  val create_context : context
+  val init_context : context
 
   val add_decl : context -> decl -> context
 

src/core/transform.ml

@@ -81,7 +81,7 @@ let fold ?clear f_fold v_empty =
   t ?clear (f []) (fun () -> Hashtbl.clear memo_t)
 
 let fold_map ?clear f_fold v_empty =
-  let v_empty = v_empty,create_context in
+  let v_empty = v_empty,init_context in
   let f_fold ctxt (env,ctxt2) = f_fold ctxt ctxt2 env in
   conv_res (fold ?clear f_fold v_empty) snd
 
@@ -137,7 +137,7 @@ let split_goals =
           (add_decl ctxt d1,
            (add_decl ctxt d2)::l)
       | _ -> (add_decl ctxt decl,l) in
-  let g = fold f (create_context,[]) in
+  let g = fold f (init_context,[]) in
   conv_res g snd
 
 let extract_goals =
@@ -150,7 +150,7 @@ let extract_goals =
           (add_decl ctxt d,
            (f.pr_name,f.pr_fmla,ctxt)::l)
       | _ -> (add_decl ctxt decl,l) in
-  let g = fold f (create_context,[]) in
+  let g = fold f (init_context,[]) in
   conv_res g snd
 
 

src/main.ml

@@ -19,6 +19,7 @@
 
 open Format
 open Theory
+open Driver
 
 let files = ref []
 let parse_only = ref false
@@ -28,7 +29,7 @@ let loadpath = ref []
 let print_stdout = ref false
 let simplify_recursive = ref false
 let inlining = ref false
-let alt_ergo = ref false
+let driver = ref None
 
 let () = 
   Arg.parse 
@@ -38,9 +39,11 @@ let () =
      "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
        "<dir>  adds dir to the loadpath";
      "--print-stdout", Arg.Set print_stdout, "print the results to stdout";
-     "--simplify-recursive", Arg.Set simplify_recursive, "simplify recursive definition";
+     "--simplify-recursive", Arg.Set simplify_recursive, 
+       "simplify recursive definition";
      "--inline", Arg.Set inlining, "inline the definition not recursive";
-     "--alt-ergo", Arg.Set alt_ergo, "output for Alt-Ergo on stdout";
+     "--driver", Arg.String (fun s -> driver := Some s),
+       "<file>  set the driver file";
     ]
     (fun f -> files := f :: !files)
     "usage: why [options] files..."
@@ -67,6 +70,8 @@ let rec report fmt = function
       Typing.report fmt e
   | Context.UnknownIdent i ->
       fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
+  | Driver.Error e ->
+      Driver.report fmt e
   | e ->
       if in_emacs then
         let dir = Filename.dirname (Filename.dirname Sys.executable_name) in
@@ -84,46 +89,38 @@ let type_file env file =
     close_in c;
     env
   end else 
-    Typing.add_file env file
+    Typing.add_from_file env file
 
 let extract_goals ctxt =
-  Transform.apply Transform.extract_goals ctxt
-
-let driver_rules = ref Driver.empty_rules
+  Transform.apply Transform.split_goals ctxt
 
 let transform env l =
   let l = List.map 
-    (fun t -> t, Context.use_export Context.create_context t) 
+    (fun t -> t, Context.use_export Context.init_context t) 
       (Typing.local_theories l) in
   let l = transformation l in
   if !print_stdout then 
     List.iter 
       (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
-  else if !alt_ergo then match l with
-    | (_,ctxt) :: _ -> begin match extract_goals ctxt with
-	| g :: _ -> 
-	    let drv = Driver.create !driver_rules ctxt in
-	    Alt_ergo.print_goal drv std_formatter g
-	| [] -> 
-	    eprintf "no goal@."
-      end	
-    | [] -> ()
-
-let handle_file env file =
-  if Filename.check_suffix file ".why" then
-    type_file env file
-  else if Filename.check_suffix file ".drv" then begin
-    driver_rules := Driver.load file;
-    env
-  end else begin
-    eprintf "%s: don't know what to do with file %s@." Sys.argv.(0) file;
-    exit 1
-  end
+  else match !driver with
+    | None ->
+	()
+    | Some file ->
+	let drv = load_driver file env in
+	begin match l with
+	  | (_,ctxt) :: _ -> begin match extract_goals ctxt with
+	      | g :: _ -> 
+		  Driver.print_context drv std_formatter g
+	      | [] -> 
+		  eprintf "no goal@."
+	    end
+	  | [] -> ()
+	end
 
 let () =
   try
     let env = Typing.create !loadpath in
-    let l = List.fold_left handle_file env !files in
+    let l = List.fold_left type_file env !files in
     transform env l
   with e when not !debug ->
     eprintf "%a@." report e;

src/output/alt_ergo.ml

@@ -170,10 +170,11 @@ let print_decl drv ctxt fmt d = match d.d_node with
   | Duse _ | Dclone _ ->
       ()
 
-let print_context env fmt ctxt = 
+let print_context drv fmt ctxt = 
   let decls = Context.get_decls ctxt in
-  print_list newline2 (print_decl env ctxt) fmt decls
+  print_list newline2 (print_decl drv ctxt) fmt decls
 
+let () = Driver.register_printer "alt-ergo" print_context
 
 let print_goal env fmt (id, f, ctxt) =
   print_context env fmt ctxt;

src/output/alt_ergo.mli

@@ -16,16 +16,3 @@
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
 (*                                                                        *)
 (**************************************************************************)
-
-open Format
-open Ident
-open Term
-open Theory
-
-val print_term : formatter -> term -> unit
-
-val print_fmla : formatter -> fmla -> unit
-
-val print_context : Driver.t -> formatter -> context -> unit
-
-val print_goal : Driver.t -> formatter -> ident * fmla * context -> unit

src/output/driver.ml

@@ -17,32 +17,116 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t = unit
+open Format
+open Theory
+open Driver_ast
 
-type translation = 
-  | Remove
-  | Syntax of string
-  | Tag of string list
+type error = string
+
+exception Error of string
+
+let report = pp_print_string
+
+let error ?loc e = match loc with
+  | None -> raise (Error e)
+  | Some loc -> raise (Loc.Located (loc, Error e))
+
+let errorm ?loc f =
+  let buf = Buffer.create 512 in
+  let fmt = Format.formatter_of_buffer buf in
+  Format.kfprintf 
+    (fun _ -> 
+       Format.pp_print_flush fmt ();
+       let s = Buffer.contents buf in
+       Buffer.clear buf;
+       error ?loc s)
+    fmt f
+
+(** creating drivers *)
+
+type prover_answer =
+  | Valid
+  | Invalid
+  | Unknown of string
+  | Failure of string
+  | Timeout
+
+type theory_driver = {
+  thd_prelude : string option;
+  thd_tsymbol : unit ;
+}
+
+type printer = driver -> formatter -> context -> unit
 
-type rules = unit
+and driver = {
+  drv_printer    : printer option;
+  drv_context    : context;
+  drv_call_stdin : string option;
+  drv_call_file  : string option;
+  drv_regexps    : (string * prover_answer) list;
+  drv_prelude    : string option;
+  drv_rules      : (string list, theory_rules) Hashtbl.t;
+  drv_theory     : (string list, theory_driver) Hashtbl.t;
+}
 
-let empty_rules = ()
-    
-let load file =
+(** registering printers *)
+
+let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17
+
+let register_printer name printer = Hashtbl.replace printers name printer
+
+let load_file file =
   let c = open_in file in
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
-  let _f = Driver_lexer.parse_file lb in 
+  let f = Driver_lexer.parse_file lb in 
   close_in c;
-  ()
+  f
 
-let create rules ctxt =
-  (* TODO *)
-  ()
+let load_driver file env =
+  let f = load_file file in
+  let printer = ref (None : printer option) in
+  let add (loc, g) = match g with
+    | Printer _ when !printer <> None -> 
+	errorm ~loc "duplicate printer"
+    | Printer s when Hashtbl.mem printers s ->
+	printer := Some (Hashtbl.find printers s)
+    | Printer s -> 
+	errorm ~loc "unknown printer %s" s 
+    | _ -> 
+	() (* TODO *)
+  in
+  List.iter add f.f_global;
+  { drv_printer    = !printer;
+    drv_context    = Context.init_context;
+    drv_call_stdin = None;
+    drv_call_file  = None;
+    drv_regexps    = [];
+    drv_prelude    = None;
+    drv_rules      = Hashtbl.create 17;
+    drv_theory     = Hashtbl.create 17;
+  }
+
+(** querying drivers *)
+
+type translation = 
+  | Remove
+  | Syntax of string
+  | Tag of string list
 
-let ident dr id =
+let query_ident dr id =
   assert false (*TODO*)
 
+(** using drivers *)
+
+let print_context drv = match drv.drv_printer with
+  | None -> errorm "no printer"
+  | Some f -> f drv
+
+let call_prover drv ctx = assert false (*TODO*)
+let call_prover_on_file drv filename = assert false (*TODO*)
+let call_prover_on_channel drv filename ic = assert false (*TODO*)
+
 (*
 Local Variables: 
 compile-command: "unset LANG; make -C ../.. test"

src/output/driver.mli

@@ -17,23 +17,50 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Format
 open Ident
 open Theory
 
-type t
+(** creating drivers *)
+
+type driver 
+
+val load_driver : string -> Typing.env -> driver
+
+(** querying drivers *)
 
 type translation = 
   | Remove
   | Syntax of string
   | Tag of string list
 
-val ident : t -> ident -> translation
+val query_ident : driver -> ident -> translation
+
+(** registering printers *)
+
+type printer = driver -> formatter -> context -> unit
+
+val register_printer : string -> printer -> unit
+
+(** using drivers *)
+
+val print_context : printer
+
+type prover_answer =
+  | Valid
+  | Invalid
+  | Unknown of string
+  | Failure of string
+  | Timeout
 
-type rules
+val call_prover : driver -> context -> prover_answer
+val call_prover_on_file : driver -> string -> prover_answer
+val call_prover_on_channel : driver -> string -> in_channel -> prover_answer
 
-val empty_rules : rules
+(* error reporting *)
 
-val load : string -> rules
+type error
 
-val create : rules -> context -> t
+exception Error of error
 
+val report : formatter -> error -> unit

src/output/driver_ast.mli

@@ -19,9 +19,7 @@
 
 type loc = Loc.position
 
-type ident = Ptree.ident
-
-type qualid = Ptree.qualid
+type qualid = loc * string list
 
 type cloned = bool
 
@@ -29,14 +27,24 @@ type trule =
   | Rremove of cloned * qualid
   | Rsyntax of qualid * string
   | Rtag    of cloned * qualid * string
+  | Rprelude of string
 
 type theory_rules = {
   th_name    : qualid;
-  th_prelude : string option;
   th_rules   : trule list;
 }
 
+type global =
+  | Prelude of string
+  | Printer of string
+  | CallStdin of string
+  | CallFile of string
+  | RegexpValid of string
+  | RegexpInvalid of string
+  | RegexpUnknown of string * string
+  | RegexpFailure of string * string
+
 type file = {
-  f_prelude : string option;
-  f_rules   : theory_rules list;
+  f_global : (loc * global) list;
+  f_rules  : theory_rules list;
 }

src/output/driver_lexer.mll

@@ -33,6 +33,14 @@
 	"remove", REMOVE;
 	"tag", TAG;
 	"cloned", CLONED;
+	"prelude", PRELUDE;
+	"printer", PRINTER;
+	"call_on_file", CALL_ON_FILE;
+	"call_on_stdin", CALL_ON_STDIN;
+	"valid", VALID;
+	"invalid", INVALID;
+	"unknown", UNKNOWN;
+	"fail", FAIL;
       ]
 
 }

src/output/driver_parser.mly

@@ -18,10 +18,10 @@
 /**************************************************************************/
 
 %{
-  open Ptree
   open Driver_ast
   open Parsing
   let loc () = (symbol_start_pos (), symbol_end_pos ())
+  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
   let infix s = "infix " ^ s
   let prefix s = "prefix " ^ s
 %}
@@ -29,7 +29,8 @@
 %token <string> IDENT
 %token <string> STRING
 %token <string> OPERATOR
-%token THEORY END SYNTAX REMOVE TAG
+%token THEORY END SYNTAX REMOVE TAG PRELUDE PRINTER CALL_ON_FILE CALL_ON_STDIN
+%token VALID INVALID UNKNOWN FAIL
 %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
 
 %type <Driver_ast.file> file
@@ -38,13 +39,24 @@
 %%
 
 file:
-| string_option list0_theory EOF
-    { { f_prelude = $1; f_rules = $2 } }
+| list0_global list0_theory EOF
+    { { f_global = $1; f_rules = $2 } }
 ;
 
-string_option:
-| /* epsilon */ { None }
-| STRING        { Some $1 }
+list0_global:
+| /* epsilon */       { [] }
+| global list0_global { (loc_i 1, $1) :: $2 }
+;
+
+global:
+| PRELUDE STRING { Prelude $2 }
+| PRINTER STRING { Printer $2 }
+| CALL_ON_FILE STRING { CallFile $2 }
+| CALL_ON_STDIN STRING { CallStdin $2 }
+| VALID STRING { RegexpValid $2 }
+| INVALID STRING { RegexpInvalid $2 }
+| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
+| FAIL STRING STRING { RegexpFailure ($2, $3) }
 ;
 
 list0_theory:
@@ -53,8 +65,8 @@ list0_theory:
 ;
 
 theory:
-| THEORY qualid string_option list0_trule END
-    { { th_name = $2; th_prelude = $3; th_rules = $4 } }
+| THEORY qualid list0_trule END
+    { { th_name = $2; th_rules = $3 } }
 ;
 
 list0_trule:
@@ -63,6 +75,7 @@ list0_trule:
 ;
 
 trule:
+| PRELUDE STRING           { Rprelude $2 }
 | REMOVE cloned qualid     { Rremove ($2, $3) }
 | SYNTAX qualid STRING     { Rsyntax ($2, $3) }
 | TAG cloned qualid STRING { Rtag    ($2, $3, $4) }
@@ -74,18 +87,24 @@ cloned:
 ;
 
 qualid:
-| ident            { Qident $1 }
-| qualid DOT ident { Qdot ($1, $3) }
+| ident            { loc(), [$1] }
+| ident DOT qualid { loc(), ($1 :: snd $3) }
 ;
 
 ident:
 | IDENT  
-    { { id = $1; id_loc = loc () } }
+    { $1 }
 | STRING 
-    { { id = $1; id_loc = loc () } }
+    { $1 }
 | LEFTPAR UNDERSCORE OPERATOR UNDERSCORE RIGHTPAR 
-    { { id = infix $3; id_loc = loc () } }
+    { infix $3 }
 | LEFTPAR OPERATOR UNDERSCORE RIGHTPAR 
-    { { id = prefix $2; id_loc = loc () } }
+    { prefix $2 }
+/*
+| LEFTPAR UNDERSCORE lident_op RIGHTPAR 
+    { { id = postfix $3; id_loc = loc () } }
+*/
+| PRELUDE
+    { "prelude" }
 ;
 

src/parser/typing.ml

@@ -1042,11 +1042,15 @@ let locate_file env sl =
     | file1 :: file2 :: _ -> error (AmbiguousPath (file1, file2))
 
 (* parse file and store all theories into parsed_theories *)
-let load_file file =
-  let c = open_in file in
+
+let load_channel file c =
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
-  let tl = Lexer.parse_logic_file lb in 
+  Lexer.parse_logic_file lb
+
+let load_file file =
+  let c = open_in file in
+  let tl = load_channel file c in
   close_in c;
   tl
 
@@ -1178,11 +1182,20 @@ and type_and_add_theory q env pt =
   with 
     | Error (ClashTheory _ as e) -> error ~loc:id.id_loc e
    
+let clear_local_theories env =
+  { env with theories = M.empty }
 
-and add_file env file =
-  let tl = load_file file in
+let add_local_theories env tl =
   List.fold_left (type_and_add_theory "") env tl
 
+let add_from_file env file =
+  let tl = load_file file in
+  add_local_theories env tl
+
+let add_from_channel env file ic =
+  let tl = load_channel file ic in
+  add_local_theories env tl
+
 let local_theories env = 
   List.rev (M.fold (fun _ v acc -> v::acc) env.theories [])
 

src/parser/typing.mli

@@ -25,10 +25,18 @@ val create : string list -> env
   (** creates a new typing environment for a given loadpath *)
 
 val add_theory : env -> Theory.theory -> env
-  (** add a local theory *)