preliminary support for black lists in drivers

drivers/ocaml.drv

 
-filename "%f_%t.ml"
+printer "ocaml"
 
 theory BuiltIn
   syntax type       int   "Num.num"

plugins/tptp/tptp_printer.ml

@@ -225,7 +225,7 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task fof _env pr thpr ?old:_ fmt task =
+let print_task fof _env pr thpr _blacklist ?old:_ fmt task =
   forget_all ident_printer;
   forget_all pr_printer;
   print_prelude fmt pr;

src/core/printer.ml

@@ -31,10 +31,12 @@ open Task
 
 type prelude = string list
 type prelude_map = prelude Mid.t
+type blacklist = string list
 
 type 'a pp = formatter -> 'a -> unit
 
-type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp
+type printer =
+  Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
 
 type reg_printer =
   { reg_desc    : formatted;
@@ -62,7 +64,7 @@ let print_printer_desc fmt (s,f) =
     s Pp.formatted f
 
 let () = register_printer ~desc:"Print nothing" "(null)"
-  (fun _ _ _ ?old:_ _ _ -> ())
+  (fun _ _ _ _ ?old:_ _ _ -> ())
 
 (** Syntax substitutions *)
 

src/core/printer.mli

@@ -29,10 +29,12 @@ open Task
 
 type prelude = string list
 type prelude_map = prelude Mid.t
+type blacklist = string list
 
 type 'a pp = Format.formatter -> 'a -> unit
 
-type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp
+type printer =
+    Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
 
 val register_printer : desc:Pp.formatted -> string -> printer -> unit
 

src/driver/driver.ml

@@ -40,6 +40,7 @@ type driver = {
   drv_transform   : string list;
   drv_prelude     : prelude;
   drv_thprelude   : prelude_map;
+  drv_blacklist   : string list;
   drv_meta        : (theory * Stdecl.t) Mid.t;
   drv_meta_cl     : (theory * Stdecl.t) Mid.t;
   drv_regexps     : (Str.regexp * prover_answer) list;
@@ -87,6 +88,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
   let printer   = ref None in
   let transform = ref [] in
   let timeregexps = ref [] in
+  let blacklist = Queue.create () in
 
   let set_or_raise loc r v error = match !r with
     | Some _ -> raise (Loc.Located (loc, Duplicate error))
@@ -112,6 +114,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | Printer s -> set_or_raise loc printer s "printer"
     | Transform s -> add_to_list transform s
     | Plugin files -> load_plugin (Filename.dirname file) files
+    | Blacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
   in
   let f = load_file file in
   List.iter add_global f.f_global;
@@ -191,6 +194,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     drv_filename    = !filename;
     drv_transform   = List.rev !transform;
     drv_thprelude   = Mid.map List.rev !thprelude;
+    drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
     drv_meta        = !meta;
     drv_meta_cl     = !meta_cl;
     drv_regexps     = List.rev !regexps;
@@ -293,6 +297,7 @@ let print_task_prepared ?old drv fmt task =
   in
   let printer =
     lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
+      drv.drv_blacklist
   in
   fprintf fmt "@[%a@]@?" (printer ?old) task
 

src/driver/driver_ast.ml

@@ -45,6 +45,16 @@ type theory_rules = {
   thr_rules : (loc * th_rule) list;
 }
 
+type mo_rule =
+  | MRtheory    of th_rule
+  | MRexception of cloned * qualid * string
+  | MRval       of cloned * qualid * string
+
+type module_rules = {
+  mor_name  : qualid;
+  mor_rules : (loc * mo_rule) list;
+}
+
 type global =
   | Prelude of string
   | Printer of string
@@ -64,9 +74,15 @@ type global =
   | Filename of string
   | Transform of string
   | Plugin of (string * string)
+  | Blacklist of string list
 
 type file = {
   f_global : (loc * global) list;
   f_rules  : theory_rules list;
 }
 
+type file_extract = {
+  fe_global   : (loc * global) list;
+  fe_th_rules : theory_rules list;
+  fe_mo_rules : module_rules list;
+}

src/driver/driver_lexer.mll

@@ -55,7 +55,12 @@
         "prop", PROP;
         "filename", FILENAME;
         "transformation", TRANSFORM;
-        "plugin", PLUGIN
+        "plugin", PLUGIN;
+        "blacklist", BLACKLIST;
+        (* WhyML *)
+        "module", MODULE;
+        "exception", EXCEPTION;
+        "val", VAL;
       ]
 
 }

src/driver/driver_parser.mly

@@ -37,12 +37,16 @@
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
 %token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
 %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
+%token BLACKLIST
+%token MODULE EXCEPTION VAL
 %token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
 %token LEFTPAR_STAR_RIGHTPAR COMMA
 %token LEFTSQ RIGHTSQ LARROW
 
 %type <Driver_ast.file> file
 %start file
+%type <Driver_ast.file_extract> file_extract
+%start file_extract
 
 %%
 
@@ -77,6 +81,7 @@ global:
 | FILENAME STRING { Filename $2 }
 | TRANSFORM STRING { Transform $2 }
 | PLUGIN STRING STRING { Plugin ($2,$3) }
+| BLACKLIST list1_string_list { Blacklist $2 }
 ;
 
 theory:
@@ -161,3 +166,39 @@ operator:
 | LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
 ;
 
+list1_string_list:
+| STRING                   { [$1] }
+| list1_string_list STRING { $2 :: $1 }
+;
+
+/* WhyML */
+
+file_extract:
+| list0_global_theory_module EOF
+{ $1 }
+;
+
+list0_global_theory_module:
+| /* epsilon */      { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
+| global list0_global_theory_module
+    { {$2 with fe_global = (loc_i 1, $1) :: ($2.fe_global)} }
+| theory list0_global_theory_module
+    { {$2 with fe_th_rules = $1 :: ($2.fe_th_rules)} }
+| module_ list0_global_theory_module
+    { {$2 with fe_mo_rules = $1 :: ($2.fe_mo_rules)} }
+;
+
+module_:
+| MODULE tqualid list0_mrule END
+    { { mor_name = $2; mor_rules = $3 } }
+;
+
+list0_mrule:
+| /* epsilon */     { [] }
+| mrule list0_mrule { (loc_i 1, $1) :: $2 }
+;
+
+mrule:
+| trule { MRtheory $1 }
+;
+

src/printer/alt_ergo.ml

@@ -367,7 +367,7 @@ let print_decls =
       add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
     Printer.sprint_decls (print ac sl csm pjs axs))))
 
-let print_task _env pr thpr ?old:_ fmt task =
+let print_task _env pr thpr _blacklist ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is a no-no *)
   (* forget_all ident_printer; *)
   print_prelude fmt pr;

src/printer/coq.ml

@@ -791,7 +791,7 @@ let print_decl ~old info fmt d =
 let print_decls ~old info fmt dl =
   fprintf fmt "@\n@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
 
-let print_task env pr thpr realize ?old fmt task =
+let print_task env pr thpr _blacklist realize ?old fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
@@ -842,11 +842,11 @@ let print_task env pr thpr realize ?old fmt task =
   print_decls ~old info fmt local_decls;
   output_remaining fmt !old
 
-let print_task_full env pr thpr ?old fmt task =
-  print_task env pr thpr false ?old fmt task
+let print_task_full env pr thpr blacklist ?old fmt task =
+  print_task env pr thpr blacklist false ?old fmt task
 
-let print_task_real env pr thpr ?old fmt task =
-  print_task env pr thpr true  ?old fmt task
+let print_task_real env pr thpr blacklist ?old fmt task =
+  print_task env pr thpr blacklist true  ?old fmt task
 
 let () = register_printer "coq" print_task_full
   ~desc:"Printer@ for@ the@ Coq@ proof@ assistant@ \

src/printer/cvc3.ml

@@ -324,7 +324,7 @@ let distingued =
       let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
       Trans.return dis2))
 
-let print_task pr thpr fmt task =
+let print_task pr thpr _blacklist fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
@@ -337,7 +337,7 @@ let print_task pr thpr fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "cvc3"
-  (fun _env pr thpr ?old:_ fmt task ->
+  (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
-     print_task pr thpr fmt task)
+     print_task pr thpr blacklist fmt task)
   ~desc:"Printer@ for@ the@ CVC3@ theorem@ prover."

src/printer/gappa.ml

@@ -423,7 +423,7 @@ let print_goal info fmt g =
         fprintf fmt "# (no goal at all ??)@\n";
         fprintf fmt "1 in [0,0]@\n"
 
-let print_task env pr thpr ?old:_ fmt task =
+let print_task env pr thpr _blacklist ?old:_ fmt task =
   forget_all ident_printer;
   let info = get_info env task in
   print_prelude fmt pr;

src/printer/pvs.ml

@@ -824,7 +824,7 @@ let init_printer th =
   Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
   pr
 
-let print_task env pr thpr realize ?old fmt task =
+let print_task env pr thpr _blacklist realize ?old fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
@@ -906,11 +906,11 @@ let print_task env pr thpr realize ?old fmt task =
   output_remaining fmt !old;
   fprintf fmt "@]@\nEND %s@\n@]" thname
 
-let print_task_full env pr thpr ?old fmt task =
-  print_task env pr thpr false ?old fmt task
+let print_task_full env pr thpr blacklist ?old fmt task =
+  print_task env pr thpr blacklist false ?old fmt task
 
-let print_task_real env pr thpr ?old fmt task =
-  print_task env pr thpr true  ?old fmt task
+let print_task_real env pr thpr blacklist ?old fmt task =
+  print_task env pr thpr blacklist true  ?old fmt task
 
 let () = register_printer "pvs" print_task_full
   ~desc:"Printer@ for@ the@ PVS@ proof@ assistant@ \

src/printer/simplify.ml

@@ -161,7 +161,7 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr fmt task =
+let print_task pr thpr _blacklist fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
@@ -171,8 +171,8 @@ let print_task pr thpr fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "simplify"
-  (fun _env pr thpr ?old:_ fmt task ->
+  (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
-     print_task pr thpr fmt task)
+     print_task pr thpr blacklist fmt task)
   ~desc:"Printer@ for@ the@ Simplify@ theorem@ prover."
 

src/printer/smtv1.ml

@@ -216,7 +216,7 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr fmt task =
+let print_task pr thpr _blacklist fmt task =
   fprintf fmt "(benchmark why3@\n"
     (*print_ident (Task.task_goal task).pr_name*);
   fprintf fmt "  :status unknown@\n";
@@ -231,7 +231,7 @@ let print_task pr thpr fmt task =
   fprintf fmt "@\n)@."
 
 let () = register_printer "smtv1"
-  (fun _env pr thpr ?old:_ fmt task ->
+  (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
-     print_task pr thpr fmt task)
+     print_task pr thpr blacklist fmt task)
   ~desc:"Printer@ for@ the@ smtlib@ version@ 1@ format."

src/printer/smtv2.ml

@@ -311,7 +311,7 @@ let distingued =
       let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
       Trans.return dis2))
 
-let print_task_old pr thpr fmt task =
+let print_task_old pr thpr _blacklist fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
@@ -324,9 +324,9 @@ let print_task_old pr thpr fmt task =
   fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
 
 let () = register_printer "smtv2"
-  (fun _env pr thpr ?old:_ fmt task ->
+  (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
-     print_task_old pr thpr fmt task)
+     print_task_old pr thpr blacklist fmt task)
   ~desc:"Printer for the smtlib version 2 format."
 
 let print_decls =
@@ -344,7 +344,7 @@ let print_decls =
   Trans.on_meta Discriminate.meta_lsinst (fun dls ->
     Printer.sprint_decls (print dls))
 
-let print_task _env pr thpr ?old:_ fmt task =
+let print_task _env pr thpr _blacklist ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is taboo *)
   (* forget_all ident_printer; *)
   print_prelude fmt pr;

src/printer/why3printer.ml

@@ -387,7 +387,7 @@ let print_tdecl fmt td = match td.td_node with
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
         m.meta_name (print_list comma print_meta_arg) al
 
-let print_task_old _env pr thpr ?old:_ fmt task =
+let print_task_old _env pr thpr _blacklist ?old:_ fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
@@ -401,7 +401,7 @@ let print_tdecls =
     print_tdecl fmt td in
   Printer.sprint_tdecls print
 
-let print_task _env pr thpr ?old:_ fmt task =
+let print_task _env pr thpr _blacklist ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
   (* forget_all (); *)
   print_prelude fmt pr;

src/printer/yices.ml

@@ -325,7 +325,7 @@ let distingued =
       let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
       Trans.return dis2))
 
-let print_task pr thpr fmt task =
+let print_task pr thpr _blacklist fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
@@ -338,7 +338,7 @@ let print_task pr thpr fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "yices"
-  (fun _env pr thpr ?old:_ fmt task ->
+  (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
-     print_task pr thpr fmt task)
+     print_task pr thpr blacklist fmt task)
   ~desc:"Printer@ for@ the@ Yices@ theorem@ prover version 1."