From 0007b802d0904f48660e1e00f0cecdcb7a176564 Mon Sep 17 00:00:00 2001 From: Francois Bobot Date: Thu, 11 Mar 2010 17:09:40 +0000 Subject: [PATCH] ajout des options --all-goals --goals-of Test --goal Test.G --output dir (-d),... --- Makefile.in | 9 ++- lib/drivers/alt_ergo.drv | 3 +- lib/drivers/why3.drv | 2 + src/core/ident.ml | 4 ++ src/core/ident.mli | 5 ++ src/main.ml | 133 +++++++++++++++++++++++++++++------ src/output/driver.ml | 29 +++++++- src/output/driver.mli | 4 ++ src/output/driver_ast.mli | 1 + src/output/driver_lexer.mll | 1 + src/output/driver_parser.mly | 3 +- 11 files changed, 166 insertions(+), 28 deletions(-) create mode 100644 lib/drivers/why3.drv diff --git a/Makefile.in b/Makefile.in index bc230b7d4..a8b7d741f 100644 --- a/Makefile.in +++ b/Makefile.in @@ -144,8 +144,11 @@ bin/top: $(CMO) ocamlmktop $(BFLAGS) -o $@ nums.cma $^ test: bin/why.byte - ocamlrun -bt bin/why.byte --print-stdout -I lib/prelude/ src/test.why - bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ src/test.why > ergo.why + mkdir -p output_why3 + ocamlrun -bt bin/why.byte --debug -I lib/prelude/ --driver lib/drivers/why3.drv \ + --output output_why3 src/test.why + bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ \ + --output - --goal Test.G src/test.why > ergo.why timeout 3 alt-ergo ergo.why testl: bin/whyl.byte @@ -597,6 +600,8 @@ clean:: rm -f bin/why-cpulimit rm -f lib/coq*/*.vo lib/coq*/*~ rm -f $(GENERATED) + rm -rf output_why3 + rm -f ergo.why # make -C atp clean # make -C doc clean # if test -d examples-v7; then \ diff --git a/lib/drivers/alt_ergo.drv b/lib/drivers/alt_ergo.drv index 55a964c11..b35b12840 100644 --- a/lib/drivers/alt_ergo.drv +++ b/lib/drivers/alt_ergo.drv @@ -4,8 +4,9 @@ prelude "(* this is a prelude for Alt-Ergo*)" printer "alt-ergo" - +filename "%f-%t-%s.why" call_on_file "alt-ergo %s" + (* tranformations "simplify_recursive_definition" diff --git a/lib/drivers/why3.drv b/lib/drivers/why3.drv new file mode 100644 index 000000000..25d25b2cd --- /dev/null +++ b/lib/drivers/why3.drv @@ -0,0 +1,2 @@ +printer "why3" +filename "%f-%t-%s.why" \ No newline at end of file diff --git a/src/core/ident.ml b/src/core/ident.ml index f0a8d392f..4ca6a1fc5 100644 --- a/src/core/ident.ml +++ b/src/core/ident.ml @@ -68,6 +68,10 @@ let id_derive_long sh ln id = create_ident sh ln (Derived id) let id_clone id = create_ident id.id_short id.id_long (Derived id) let id_dup id = { id with id_tag = -1 } +(* Utils *) +let rec derived_from i1 i2 = + i1 == i2 || (match i1.id_origin with Derived i3 -> derived_from i1 i2 | _ -> false) + (** Unique names for pretty printing *) type ident_printer = diff --git a/src/core/ident.mli b/src/core/ident.mli index 20722d963..f21e16ee9 100644 --- a/src/core/ident.mli +++ b/src/core/ident.mli @@ -59,6 +59,11 @@ val id_clone : ident -> preid (* create a duplicate pre-ident *) val id_dup : ident -> preid +(* Utils *) +val derived_from : ident -> ident -> bool + +(* derived_from i1 i2 is true if i1 is derived from i2 *) + (** Unique persistent names for pretty printing *) type ident_printer diff --git a/src/main.ml b/src/main.ml index 21611975b..22a751d6d 100644 --- a/src/main.ml +++ b/src/main.ml @@ -21,15 +21,20 @@ open Format open Theory open Driver -let files = ref [] +let files = Queue.create () let parse_only = ref false let type_only = ref false let debug = ref false let loadpath = ref [] -let print_stdout = ref false -let simplify_recursive = ref false -let inlining = ref false let driver = ref None +type which_goals = + | Gall + | Gtheory of string + | Ggoal of string +let which_goals = ref Gall +let timeout = ref 10 +let call = ref false +let output = ref None let () = Arg.parse @@ -37,19 +42,31 @@ let () = "--type-only", Arg.Set type_only, "stops after type-checking"; "--debug", Arg.Set debug, "sets the debug flag"; "-I", Arg.String (fun s -> loadpath := s :: !loadpath), - " 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"; - "--inline", Arg.Set inlining, "inline the definition not recursive"; + " adds dir to the loadpath"; + "--all_goals", Arg.Unit (fun () -> which_goals := Gall), + "apply on all the goals of the file"; + "--goals_of", Arg.String (fun s -> which_goals := Gtheory s), + "apply on all the goals of the theory given (ex. --goal T)"; + "--goal", Arg.String (fun s -> which_goals := Ggoal s), + "apply only on the goal given (ex. --goal T.g)"; + "--output", Arg.String (fun s -> output := Some s), + "choose to output each goals in the directory given.\ + Can't be used with --call"; + "--call", Arg.Set call, + "choose to call the prover on each goals.\ + Can't be used with --output"; (* Why not? *) "--driver", Arg.String (fun s -> driver := Some s), - " set the driver file"; + " set the driver file"; ] - (fun f -> files := f :: !files) + (fun f -> Queue.push f files) "usage: why [options] files..." -let in_emacs = Sys.getenv "TERM" = "dumb" +let () = + match !output with + | None when not !call -> type_only := true + | _ -> () +(* let transformation l = let t1 = Simplify_recursive_definition.t in let t2 = Inlining.all in @@ -60,7 +77,7 @@ let transformation l = let c = if !inlining then Transform.apply t2 c else c in (t,c)) l - +*) let rec report fmt = function | Lexer.Error e -> fprintf fmt "lexical error: %a" Lexer.report e; @@ -76,16 +93,14 @@ let rec report fmt = function Driver.report fmt e | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e) -let extract_goals ctxt = - Transform.apply Transform.split_goals ctxt - +(* let transform env l = let l = List.map (fun t -> t, Context.use_export (Context.init_context env) t) l in - let l = transformation l in + (*let l = transformation l in*) if !print_stdout then List.iter (fun (t,ctxt) -> Pretty.print_named_context @@ -94,7 +109,7 @@ let transform env l = | None -> () | Some file -> - let drv = load_driver file env in + begin match l with | (_,ctxt) :: _ -> begin match extract_goals ctxt with | g :: _ -> @@ -104,8 +119,18 @@ let transform env l = end | [] -> () end +*) + + +let extract_goals env acc th = + let ctxt = Context.use_export (Context.init_context env) th in + let l = Transform.apply Transform.split_goals ctxt in + let l = List.rev_map (fun ctxt -> (th,ctxt)) l in + List.rev_append l acc + +let file_sanitizer = Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus -let type_file env file = +let do_file env drv filename_printer file = if !parse_only then begin let c = open_in file in let lb = Lexing.from_channel c in @@ -114,14 +139,78 @@ let type_file env file = close_in c end else begin let m = Typing.read_file env file in - let l = Mnm.fold (fun _ th acc -> th :: acc) m [] in - transform env l + if not !type_only then + let drv = + match drv with + | None -> eprintf "a driver is needed@."; exit 1 + | Some drv -> drv in + let goals = + match !which_goals with + | Gall -> Mnm.fold (fun _ th acc -> extract_goals env acc th) m [] + | Gtheory s -> + begin + try + extract_goals env [] (Mnm.find s m) + with Not_found -> + eprintf "File %s : --goals_of : Unknown theory %s@." file s; exit 1 + end + | Ggoal s -> + let l = Str.split (Str.regexp "\\.") s in + let tname, l = + match l with + | [] | [_] -> + eprintf "--goal : Must be a qualified name (%s)@." s; + exit 1 + | a::l -> a,l in + let rec find_pr ns = function + | [] -> assert false + | [a] -> Mnm.find a ns.ns_pr + | a::l -> find_pr (Mnm.find a ns.ns_ns) l in + let th =try Mnm.find tname m with Not_found -> + eprintf "File %s : --goal : Unknown theory %s@." file tname; exit 1 in + let pr = try find_pr th.th_export l with Not_found -> + eprintf "File %s : --goal : Unknown goal %s@." file s ; exit 1 in + let goals = extract_goals env [] th in + List.filter (fun (_,ctxt) -> + match ctxt.ctxt_decl.d_node with + | Dprop (_,{pr_name = pr_name}) -> + Ident.derived_from pr_name pr.pr_name + | _ -> assert false) goals in + let file = + let file = Filename.basename file in + let file = Filename.chop_extension file in + Ident.id_unique filename_printer + (Ident.id_register (Ident.id_fresh file)) in + match !output with + | None -> () + | Some dir -> + let ident_printer = Ident.create_ident_printer + ~sanitizer:file_sanitizer [] in + List.iter + (fun (th,ctxt) -> + let cout = + if dir = "-" + then stdout + else + let filename = + Driver.filename_of_goal drv ident_printer + file th.th_name.Ident.id_short ctxt in + let filename = Filename.concat dir filename in + open_out filename in + let fmt = formatter_of_out_channel cout in + fprintf fmt "%a@?" (Driver.print_context drv) ctxt; + close_out cout) goals end let () = try let env = create_env (Typing.retrieve !loadpath) in - List.iter (type_file env) !files + let drv = match !driver with + | None -> None + | Some file -> Some (load_driver file env) in + let filename_printer = Ident.create_ident_printer + ~sanitizer:file_sanitizer [] in + Queue.iter (do_file env drv filename_printer) files with e when not !debug -> eprintf "%a@." report e; exit 1 diff --git a/src/output/driver.ml b/src/output/driver.ml index baf741263..b98ed4c27 100644 --- a/src/output/driver.ml +++ b/src/output/driver.ml @@ -31,7 +31,7 @@ open Str let opt_search_forward re s pos = try Some(search_forward re s pos) with Not_found -> None -let global_substitute expr repl_fun text fmt = +let global_substitute_fmt expr repl_fun text fmt = let rec replace start last_was_empty = let startpos = if last_was_empty then start + 1 else start in if startpos > String.length text then @@ -125,6 +125,7 @@ and driver = { drv_call_file : string option; drv_regexps : (string * prover_answer) list; drv_prelude : string option; + drv_filename : string option; drv_rules : theory_rules list; drv_thprelude : string Hid.t; (* the first is the translation only for this ident, the second is also for representant *) @@ -263,6 +264,7 @@ let load_driver file env = let printer = ref None in let call_stdin = ref None in let call_file = ref None in + let filename = ref None in let regexps = ref [] in let set_or_raise loc r v error = if !r <> None then errorm ~loc "duplicate %s" error @@ -281,6 +283,7 @@ let load_driver file env = | RegexpInvalid s -> regexps:=(s,Invalid)::!regexps | RegexpUnknown (s1,s2) -> regexps:=(s1,Unknown s2)::!regexps | RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps + | Filename s -> set_or_raise loc filename s "filename" in List.iter add f.f_global; { drv_printer = !printer; @@ -289,6 +292,7 @@ let load_driver file env = drv_call_file = !call_file; drv_regexps = !regexps; drv_prelude = !prelude; + drv_filename = !filename; drv_rules = f.f_rules; drv_thprelude = Hid.create 1; drv_theory = Hid.create 1; @@ -318,7 +322,7 @@ let syntax_arguments s print fmt l = let repl_fun s fmt = let i = int_of_string (matched_group 1 s) in print fmt args.(i-1) in - global_substitute regexp_arg_pos repl_fun s fmt + global_substitute_fmt regexp_arg_pos repl_fun s fmt (** using drivers *) @@ -331,10 +335,31 @@ let print_context drv fmt ctxt = match drv.drv_printer with List.iter (load_rules drv) drv.drv_rules; f drv fmt ctxt +let regexp_filename = Str.regexp "%\\([a-z]\\)" + +let filename_of_goal drv ident_printer filename theory_name ctxt = + match drv.drv_filename with + | None -> errorm "no filename syntax given" + | Some f -> + let pr_name = match ctxt.ctxt_decl.d_node with + | Dprop (Pgoal,{pr_name=pr_name}) -> pr_name + | _ -> errorm "the bottom of this context is not a goal" in + let repl_fun s = + let i = matched_group 1 s in + match i with + | "f" -> filename + | "t" -> theory_name + | "s" -> id_unique ident_printer pr_name + | _ -> errorm "substitution variable are only %%f %%t and %%s" in + global_substitute regexp_filename repl_fun f + + 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" diff --git a/src/output/driver.mli b/src/output/driver.mli index 8ebe3e49d..4181db719 100644 --- a/src/output/driver.mli +++ b/src/output/driver.mli @@ -48,6 +48,10 @@ val register_printer : string -> printer -> unit val print_context : printer +val filename_of_goal : driver -> Ident.ident_printer -> + string -> string -> context -> string +(* filename_of_goal printer file_ident theory_ident ctxt *) + type prover_answer = | Valid | Invalid diff --git a/src/output/driver_ast.mli b/src/output/driver_ast.mli index 39c740197..5c358cf19 100644 --- a/src/output/driver_ast.mli +++ b/src/output/driver_ast.mli @@ -46,6 +46,7 @@ type global = | RegexpInvalid of string | RegexpUnknown of string * string | RegexpFailure of string * string + | Filename of string type file = { f_global : (loc * global) list; diff --git a/src/output/driver_lexer.mll b/src/output/driver_lexer.mll index 2d0ba6ec8..2e090c8ab 100644 --- a/src/output/driver_lexer.mll +++ b/src/output/driver_lexer.mll @@ -44,6 +44,7 @@ "logic", LOGIC; "type", TYPE; "prop", PROP; + "filename", FILENAME; ] } diff --git a/src/output/driver_parser.mly b/src/output/driver_parser.mly index 1a709c81e..5b1161207 100644 --- a/src/output/driver_parser.mly +++ b/src/output/driver_parser.mly @@ -32,7 +32,7 @@ %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 -%token LOGIC TYPE PROP +%token LOGIC TYPE PROP FILENAME %type file %start file @@ -58,6 +58,7 @@ global: | INVALID STRING { RegexpInvalid $2 } | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) } | FAIL STRING STRING { RegexpFailure ($2, $3) } +| FILENAME STRING { Filename $2 } ; list0_theory: -- GitLab