Ajout d'une proposition pour les transformations et les plugins dans les drivers

Makefile.in

@@ -55,9 +55,9 @@ PDFVIEWER = @PDFVIEWER@
 
 INCLUDES = -I src/core -I src/util -I src/parser -I src/output \
            -I src/transform -I src/programs -I src 
-BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma
+BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma dynlink.cma
 # no -warn-error because some do not compile all files (e.g. those linked to APRON)
-OFLAGS   = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa
+OFLAGS   = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa dynlink.cmxa
 
 COQC7  = @COQC7@
 COQC8  = @COQC8@
@@ -116,15 +116,18 @@ UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
 PARSER_CMO := parser.cmo lexer.cmo typing.cmo 
 PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 
-TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo	\
-	inlining.cmo 
+TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo 
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
+DRIVER_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo
+DRIVER_CMO := $(addprefix src/output/,$(DRIVER_CMO))
+
 OUTPUT_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo \
               print_real.cmo alt_ergo.cmo why3.cmo
 OUTPUT_CMO := $(addprefix src/output/,$(OUTPUT_CMO))
 
 CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) \
+      src/transform/transform.cmo $(DRIVER_CMO)\
       $(TRANSFORM_CMO) $(OUTPUT_CMO) src/main.cmo
 CMX = $(CMO:.cmo=.cmx)
 
@@ -160,6 +163,7 @@ PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_main.cmo
 PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))
 
 WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) \
+	   src/transform/transform.cmo $(DRIVER_CMO)\
            $(TRANSFORM_CMO) $(OUTPUT_CMO) $(PGM_CMO)
 WHYL_CMX = $(WHYL_CMO:.cmo=.cmx)
 
@@ -204,6 +208,17 @@ WHYVO=lib/coq/Why.vo
 bench:: $(BINARY) 
 	sh bench/bench "$(BINARY) -I lib/prelude/"
 
+BENCH_PLUGINS_CMO := helloworld.cmo
+BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
+BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
+
+
+bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte
+	bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I lib/prelude/ \
+        --output - --goal Test.G src/test.why
+	bin/why.byte --driver bench/plugins/helloworld.drv -I lib/prelude/ \
+        --output - --goal Test.G src/test.why
+
 # installation
 ##############
 
@@ -367,7 +382,7 @@ apidoc: $(OCAMLDOCSRC)
 # generic rules
 ###############
 
-.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4
+.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs
 
 .mli.cmi:
 	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<
@@ -384,6 +399,9 @@ apidoc: $(OCAMLDOCSRC)
 .ml.cmx:
 	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $<
 
+.ml.cmxs:
+	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -shared $(OFLAGS) -o $@ $<
+
 .mll.ml:
 	$(OCAMLLEX) $<
 
@@ -601,6 +619,7 @@ clean::
 	rm -f $(GENERATED)
 	rm -rf output_why3
 	rm -f ergo.why
+	rm -rf bench/plugins/*.cm[iox]* bench/plugins/*.annot
 #	make -C atp clean
 #	make -C doc clean
 #	if test -d examples-v7; then \
@@ -618,7 +637,7 @@ coq-clean::
 .PHONY: depend
 .depend depend: $(GENERATED)
 	rm -f .depend
-	$(OCAMLDEP) -slash $(INCLUDES) src/*/*.ml src/*/*.mli src/*.ml src/*.mli > .depend
+	$(OCAMLDEP) -slash $(INCLUDES) src/*/*.ml src/*/*.mli src/*.ml src/*.mli bench/plugins/*.ml > .depend
 ifeq ($(FRAMAC),yes)
 #	$(MAKE) -C $(JESSIE_PLUGIN_PATH) depend
 endif

bench/plugins/helloworld.drv

+plugin "helloworld.cmo" "helloworld.cmxs"
+
+printer "helloworld"
+
+filename "%f-%t-%s.hw"
+
+transformations
+        "helloworld"
+end
\ No newline at end of file

bench/plugins/helloworld.ml

+let print_context _ fmt _ = Format.fprintf fmt "helloworld"
+
+let transform_context () = Transform.identity
+
+let () = 
+  Driver.register_printer "helloworld" print_context;
+  Driver.register_transform "helloworld" transform_context

lib/drivers/alt_ergo.drv

@@ -10,13 +10,14 @@ call_on_file  "alt-ergo %s"
 valid "Valid"
 invalid "Invalid"
 unknown "I don't know" "Unknown"
+fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
 
-(*
-tranformations
+(* À discuter *)
+transformations
   "simplify_recursive_definition"      
-  "inlining" ("trivial")
+  "inline_trivial"
 end
-*)
+
 
 theory BuiltIn
   syntax type int "int"

lib/drivers/why3_inline_all.drv

+printer "why3"
+filename "%f-%t-%s.why"
+
+(* À discuter *)
+transformations
+  "simplify_recursive_definition"      
+  "inline_all"
+end

src/core/theory.ml

@@ -53,6 +53,12 @@ let create_prop n f = {
   pr_fmla = check_fvs f;
 }
 
+let shortcut_for_discussion_dont_be_mad_andrei_please n f =
+{
+  pr_name = n;
+  pr_fmla = check_fvs f;
+}
+
 (** Declarations *)
 
 (* type declaration *)

src/core/theory.mli

@@ -34,6 +34,8 @@ module Hpr : Hashtbl.S with type key = prop
 
 val create_prop : preid -> fmla -> prop
 
+val shortcut_for_discussion_dont_be_mad_andrei_please : ident -> fmla -> prop
+
 (** Declarations *)
 
 (* type declaration *)

src/main.ml

@@ -97,6 +97,8 @@ let rec report fmt = function
       fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
   | Driver.Error e ->
       Driver.report fmt e
+  | Dynlink.Error e ->
+      fprintf fmt "Dynlink : %s" (Dynlink.error_message e)
   | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
 
 (*
@@ -150,6 +152,7 @@ let do_file env drv filename_printer file =
         match drv with
           | None -> eprintf "a driver is needed@."; exit 1
           | Some drv -> drv in
+      (* Extract the goal(s) *)
       let goals = 
         match !which_goals with
           | Gall ->  Mnm.fold (fun _ th acc -> extract_goals env acc th) m []
@@ -182,6 +185,11 @@ let do_file env drv filename_printer file =
                                | Dprop (_,{pr_name = pr_name}) -> 
                                    Ident.derived_from pr_name pr.pr_name
                                | _ -> assert false) goals in
+      (* Apply transformations *)
+      let goals = List.map 
+        (fun (th,ctxt) -> (th,Driver.transform_context drv ctxt))
+        goals in
+      (* Pretty-print the goals or call the prover *)
       match !output with
         | None (* we are in the call mode *) -> 
             let call (th,ctxt) = 
@@ -191,7 +199,7 @@ let do_file env drv filename_printer file =
                 (goal_of_ctxt ctxt).pr_name.Ident.id_long
                 Call_provers.print_prover_result res in
             List.iter call goals
-        | Some dir -> 
+        | Some dir (* we are in the output mode *) -> 
             let file = 
               let file = Filename.basename file in
               let file = Filename.chop_extension file in

src/output/alt_ergo.ml

@@ -59,7 +59,7 @@ let rec print_term drv fmt t = match t.t_node with
       assert false
   | Tconst c ->
       Pretty.print_const fmt c
-  | Tvar { vs_name = id } | Tapp ({ ls_name = id }, []) ->
+  | Tvar { vs_name = id } ->
       print_ident fmt id
   | Tapp (ls, tl) ->
       begin      
@@ -67,7 +67,10 @@ let rec print_term drv fmt t = match t.t_node with
           | Driver.Remove -> assert false (* Mettre une erreur *)
           | Driver.Syntax s ->
               Driver.syntax_arguments s (print_term drv) fmt tl
-          | Driver.Tag _ -> 
+          | Driver.Tag _ ->
+              match tl with
+                | [] -> print_ident fmt ls.ls_name
+                | tl ->
               fprintf fmt "%a(%a)" 
 	        print_ident ls.ls_name (print_list comma (print_term drv)) tl
       end

src/output/call_provers.ml

@@ -42,7 +42,9 @@ type prover_result =
       pr_stdout : string}
 
 let print_prover_result fmt pr = 
-  fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time
+  fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time;
+  if pr.pr_answer == HighFailure 
+  then fprintf fmt "@\nstdout-stderr : \"%s\"" pr.pr_stdout;
 
 type prover =
     { pr_call_stdin : string option; (* %f pour le nom du fichier *)

src/output/driver.ml

@@ -126,6 +126,7 @@ and driver = {
   drv_prover     : Call_provers.prover;
   drv_prelude    : string option;
   drv_filename   : string option;
+  drv_transformations : Transform.ctxt_t list;
   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 *)
@@ -140,6 +141,11 @@ let print_driver fmt driver =
        (Pp.print_pair print_translation print_translation))
     driver.drv_theory
 
+(** registering transformation *)
+
+let (transforms : (string, unit -> Transform.ctxt_t) Hashtbl.t) = Hashtbl.create 17
+
+let register_transform name transform = Hashtbl.replace transforms name transform
 
 (** registering printers *)
 
@@ -147,6 +153,17 @@ let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17
 
 let register_printer name printer = Hashtbl.replace printers name printer
 
+
+let () = 
+  Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver";
+                     "Pervasives";"Format";"List";"Sys";"Unix"]
+
+
+let load_plugin dir (byte,nat) =
+  let file = if Dynlink.is_native then nat else byte in
+  let file = Filename.concat dir file in
+  Dynlink.loadfile_private file
+
 let load_file file =
   let c = open_in file in
   let lb = Lexing.from_channel c in
@@ -265,6 +282,7 @@ let load_driver file env =
   let call_stdin = ref None in
   let call_file = ref None in
   let filename = ref None in
+  let transformations = ref None in
   let regexps = ref [] in
   let set_or_raise loc r v error =
     if !r <> None then errorm ~loc "duplicate %s" error
@@ -284,9 +302,17 @@ let load_driver file env =
     | 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"
+    | Transformations s -> set_or_raise loc transformations  s "transformations"
+    | Plugin files -> load_plugin (Filename.dirname file) files
   in
   List.iter add f.f_global;
   let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
+  let transformations = match !transformations with
+    | None -> [] | Some l -> l in
+  let transformations = 
+    List.map (fun (loc,s) -> try (Hashtbl.find transforms s) () 
+              with Not_found -> errorm ~loc "unknown transformation %s" s)
+      transformations in
   { drv_printer    = !printer;
     drv_context    = Context.init_context env;
     drv_prover     = {Call_provers.pr_call_stdin = !call_stdin;
@@ -294,6 +320,7 @@ let load_driver file env =
                       pr_regexps                 = regexps};
     drv_prelude    = !prelude;
     drv_filename   = !filename;
+    drv_transformations = transformations;
     drv_rules      = f.f_rules;
     drv_thprelude  = Hid.create 1;
     drv_theory     = Hid.create 1;
@@ -327,6 +354,10 @@ let syntax_arguments s print fmt l =
  
 (** using drivers *)
 
+let transform_context drv ctxt =
+  List.fold_left (fun ctxt t -> Transform.apply t ctxt) 
+    ctxt drv.drv_transformations
+
 let print_context drv fmt ctxt = match drv.drv_printer with
   | None -> errorm "no printer"
   | Some f -> let drv = {drv with drv_context = ctxt;

src/output/driver.mli

@@ -44,8 +44,14 @@ type printer = driver -> formatter -> context -> unit
 
 val register_printer : string -> printer -> unit
 
+val register_transform : string -> (unit -> Transform.ctxt_t) -> unit
+
 (** using drivers *)
 
+(** transform context *)
+val transform_context : driver -> context -> context
+
+(** print_context *)
 val print_context : printer
 
 val filename_of_goal : driver -> Ident.ident_printer ->

src/output/driver_ast.mli

@@ -47,6 +47,8 @@ type global =
   | RegexpUnknown of string * string
   | RegexpFailure of string * string
   | Filename of string
+  | Transformations of (loc * string) list
+  | Plugin of (string * string)
 
 type file = {
   f_global : (loc * global) list;

src/output/driver_lexer.mll

@@ -45,6 +45,8 @@
         "type", TYPE;
         "prop", PROP;
         "filename", FILENAME;
+        "transformations", TRANSFORMATIONS;
+        "plugin", PLUGIN
       ]
 
 }

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 FILENAME
+%token LOGIC TYPE PROP FILENAME TRANSFORMATIONS PLUGIN
 
 %type <Driver_ast.file> file
 %start file
@@ -59,8 +59,16 @@ global:
 | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
 | FAIL STRING STRING { RegexpFailure ($2, $3) }
 | FILENAME STRING { Filename $2 }
+| TRANSFORMATIONS list0_string END { Transformations $2 }
+| PLUGIN STRING STRING { Plugin ($2,$3) }
 ;
 
+list0_string:
+| /* epsilon */       { [] }
+| STRING list0_string { (loc_i 1, $1) :: $2 }
+;
+
+
 list0_theory:
 | /* epsilon */       { [] }
 | theory list0_theory { $1 :: $2 }

src/test.why

@@ -4,8 +4,10 @@
 theory Test
   use import prelude.Int
   logic id(x: int) : int = x
+  logic id2(x: int) : int = id(x)
+  logic succ(x:int) : int = id(x+1)
   logic even(x: int) = 2*(x/2) = x
-  goal G : forall x:int. 0 = 0
+  goal G : forall x:int. 1 = succ(id2(zero))
   goal G2 : forall x:int. 0 = 1
 end
 

src/transform/inlining.ml

@@ -96,7 +96,7 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
     | Dind dl ->
         env, add_decl ctxt (create_ind_decl 
           (List.map (fun (ps,fmlal) -> ps, List.map (fun pr ->
-            create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla)) 
+            create_prop (id_clone pr.pr_name) (replacep env pr.pr_fmla)) 
           fmlal) dl))
     | Dlogic dl -> env,
         add_decl ctxt (create_logic_decl 
@@ -114,20 +114,33 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
                      Lpredicate (ps,Some (make_ps_defn ps vs t))
               ) dl))
     | Dtype dl -> env,add_decl ctxt d
-    | Dprop (k,pr) -> env,add_decl ctxt (create_prop_decl k
-        (create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla)))
+    | Dprop (k,pr) -> 
+        let prop = shortcut_for_discussion_dont_be_mad_andrei_please 
+          pr.pr_name (replacep env pr.pr_fmla) in
+        env,add_decl ctxt (create_prop_decl k prop)
     | Duse _ | Dclone _ -> env,add_decl ctxt d
         
 let t ~isnotinlinedt ~isnotinlinedf = 
   Transform.fold_map (fold isnotinlinedt isnotinlinedf) empty_env
 
-let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
+let all () = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
 
-let trivial = t 
+let trivial () = t 
   ~isnotinlinedt:(fun m -> match m.t_node with
                     | Tconst _ | Tvar _ -> false
                     | Tapp (ls,tl) when List.for_all 
-                        (fun m -> match m.t_node with Tvar _ -> true | _ -> false) tl -> true
+                        (fun m -> match m.t_node with 
+                           | Tvar _ -> true 
+                           | _ -> false) tl -> false
                     | _ -> true )
-  ~isnotinlinedf:(fun m -> match m.f_node with Ftrue | Ffalse | Fapp _ -> false
+  ~isnotinlinedf:(fun m -> match m.f_node with 
+                    | Ftrue | Ffalse -> false
+                    | Fapp (ls,tl) when List.for_all 
+                        (fun m -> match m.t_node with 
+                           | Tvar _ -> true 
+                           | _ -> false) tl -> false
                     | _ -> true)
+
+let () =
+  Driver.register_transform "inline_all" all;
+  Driver.register_transform "inline_trivial" trivial

src/transform/inlining.mli

@@ -28,12 +28,12 @@ val t :
 
 (* Inline them all *)
 
-val all : Transform.ctxt_t
+val all : unit -> Transform.ctxt_t
 
 (* Inline only the trivial definition :
    logic c : t = a
    logic f(x : t,...., ) : t = g(y : t2,...) *)
-val trivial : Transform.ctxt_t
+val trivial : unit -> Transform.ctxt_t
 
 
 (* Function to use in other transformations if inlining is needed *)

src/transform/simplify_recursive_definition.ml

@@ -140,5 +140,6 @@ let elt d =
     | Dind _ -> [d] (* TODO *)
     | Dprop _ | Dclone _ | Duse _ -> [d]
 
-let t = Transform.elt elt
+let t () = Transform.elt elt
 
+let () = Driver.register_transform "simplify_recursive_definition" t

src/transform/simplify_recursive_definition.mli

@@ -20,7 +20,7 @@
 
 (* Simplify the recursive type and logic definition *)
 
-val t : Transform.ctxt_t
+val t : unit -> Transform.ctxt_t
 
 
 (* ungroup recursive definition *)

src/transform/transform.ml

@@ -147,7 +147,7 @@ let split_goals =
   let g = fold_env f (fun env -> init_context env, []) in
   conv_res g snd
 
-let extract_goals =
+let extract_goals () =
   let f ctxt0 (ctxt,l) =
     let decl = ctxt0.ctxt_decl in    
     match decl.d_node with