driver utilise maintenant en interne des context list Transform.t

dans les drivers il n'y a qu'une seul liste de transformations

Makefile.in

@@ -128,7 +128,7 @@ PARSER_CMO := parser.cmo lexer.cmo typing.cmo
 PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 
 TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
-	split_conjunction.cmo 
+	split_conjunction.cmo split_goals.cmo 
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
 DRIVER_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo

bench/plugins/helloworld.drv

@@ -4,6 +4,6 @@ printer "helloworld"
 
 filename "%f-%t-%s.hw"
 
-apply_after_split_goals
+transformations
         "helloworld"
 end
\ No newline at end of file

bench/plugins/simplify_array.ml

@@ -2,8 +2,6 @@ open Term
 open Termlib
 open Theory
 
-open Transform
-
 let prelude = ["prelude"]
 let array = "Array"
 let store = ["store"]

lib/drivers/alt_ergo.drv

@@ -13,11 +13,9 @@ unknown "I don't know" "Unknown"
 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
 
 (* À discuter *)
-apply_before_split_goals
-  "split_conjunction"
-end
-apply_after_split_goals
+transformations
   "simplify_recursive_definition"      
+  "split_conjunction"
   "inline_trivial"
 end
 

lib/drivers/why3_inline_all.drv

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

lib/drivers/why3_split_conjunction.drv

@@ -2,7 +2,7 @@ printer "why3"
 filename "%f-%t-%s.why"
 
 (* À discuter *)
-apply_before_split_goals
+transformations
      "split_conjunction"
 end
 

src/main.ml

@@ -136,10 +136,9 @@ let transform env l =
 
 
 let extract_goals = 
-  let split_goals = Transform.split_goals () in
+  let split_goals = Split_goals.t () in
   fun env drv acc th ->
     let ctxt = Context.use_export (Context.init_context env) th in
-    let ctxt = Driver.apply_before_split drv ctxt in
     let l = Transform.apply split_goals ctxt in
     let l = List.rev_map (fun ctxt -> (th,ctxt)) l in
     List.rev_append l acc
@@ -193,9 +192,11 @@ let do_file env drv filename_printer file =
                                | Dprop (_,pr',_) -> pr == pr'
                                | _ -> assert false) goals in
       (* Apply transformations *)
-      let goals = List.map 
-        (fun (th,ctxt) -> (th,Driver.apply_after_split drv ctxt))
-        goals in
+      let goals = List.fold_left 
+        (fun acc (th,ctxt) -> 
+           List.rev_append 
+             (List.map (fun e -> (th,e)) (Driver.apply_transforms drv ctxt)
+             ) acc) [] goals in
       (* Pretty-print the goals or call the prover *)
       match !output with
         | None (* we are in the call mode *) -> 

src/output/driver.ml

@@ -126,8 +126,7 @@ and driver = {
   drv_prover      : Call_provers.prover;
   drv_prelude     : string option;
   drv_filename    : string option;
-  drv_beforesplit : Transform.ctxt_t list;
-  drv_aftersplit  : Transform.ctxt_t list;
+  drv_transforms  : Transform.ctxt_list_t;
   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 *)
@@ -145,10 +144,12 @@ let print_driver fmt driver =
 
 (** registering transformation *)
 
-let (transforms : (string, unit -> Transform.ctxt_t) Hashtbl.t) = Hashtbl.create 17
-
-let register_transform name transform = Hashtbl.replace transforms name transform
+let (transforms : (string, unit -> Transform.ctxt_list_t) Hashtbl.t) 
+    = Hashtbl.create 17
 
+let register_transform' name transform = Hashtbl.replace transforms name transform
+let register_transform name t = register_transform' name 
+  (fun () -> Transform.singleton (t ()))
 let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
 
 (** registering printers *)
@@ -283,8 +284,7 @@ let load_driver file env =
   let call_stdin  = ref None in
   let call_file   = ref None in
   let filename    = ref None in
-  let beforesplit = ref None in
-  let aftersplit  = ref None in
+  let ltransforms = ref None in
   let regexps     = ref [] in
   let set_or_raise loc r v error =
     if !r <> None then errorm ~loc "duplicate %s" error
@@ -304,8 +304,7 @@ 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"
-    | Beforesplit s -> set_or_raise loc beforesplit s "beforesplit"
-    | Aftersplit s -> set_or_raise loc aftersplit s "aftersplit"
+    | Transforms s -> set_or_raise loc ltransforms s "transform"
     | Plugin files -> load_plugin (Filename.dirname file) files
   in
   List.iter add f.f_global;
@@ -313,11 +312,15 @@ let load_driver file env =
   let trans r =
     let transformations = match !r with
       | None -> [] | Some l -> l in
-    List.map (fun (loc,s) -> try (Hashtbl.find transforms s) () 
-              with Not_found -> errorm ~loc "unknown transformation %s" s)
-      transformations in
-    let beforesplit = trans beforesplit in
-    let aftersplit = trans aftersplit in
+    List.fold_left 
+      (fun acc (loc,s) -> 
+         let t = 
+           try (Hashtbl.find transforms s) () 
+           with Not_found -> errorm ~loc "unknown transformation %s" s in
+         Transform.compose' acc t
+      )
+      Transform.identity' transformations in
+    let transforms = trans ltransforms in
   { drv_printer     = !printer;
     drv_context     = Context.init_context env;
     drv_prover      = {Call_provers.pr_call_stdin = !call_stdin;
@@ -325,8 +328,7 @@ let load_driver file env =
                        pr_regexps                 = regexps};
     drv_prelude     = !prelude;
     drv_filename    = !filename;
-    drv_beforesplit = beforesplit;
-    drv_aftersplit  = aftersplit;
+    drv_transforms  = transforms;
     drv_rules       = f.f_rules;
     drv_thprelude   = Hid.create 1;
     drv_theory      = Hid.create 1;
@@ -360,12 +362,7 @@ let syntax_arguments s print fmt l =
  
 (** using drivers *)
 
-let transform_context list ctxt =
-  List.fold_left (fun ctxt t -> Transform.apply t ctxt) 
-    ctxt list
-
-let apply_before_split drv = transform_context drv.drv_beforesplit
-let apply_after_split drv = transform_context drv.drv_aftersplit
+let apply_transforms drv = Transform.apply drv.drv_transforms
 
 let print_context drv fmt ctxt = match drv.drv_printer with
   | None -> errorm "no printer"

src/output/driver.mli

@@ -45,6 +45,7 @@ type printer = driver -> formatter -> context -> unit
 val register_printer : string -> printer -> unit
 
 val register_transform : string -> (unit -> Transform.ctxt_t) -> unit
+val register_transform' : string -> (unit -> Transform.ctxt_list_t) -> unit
 
 val list_printers : unit -> string list
 val list_transforms : unit -> string list
@@ -52,8 +53,7 @@ val list_transforms : unit -> string list
 (** using drivers *)
 
 (** transform context *)
-val apply_before_split : driver -> context -> context
-val apply_after_split : driver -> context -> context
+val apply_transforms : driver -> context -> context list
 
 (** print_context *)
 val print_context : printer

src/output/driver_ast.mli

@@ -47,8 +47,7 @@ type global =
   | RegexpUnknown of string * string
   | RegexpFailure of string * string
   | Filename of string
-  | Beforesplit of (loc * string) list
-  | Aftersplit of (loc * string) list
+  | Transforms of (loc * string) list
   | Plugin of (string * string)
 
 type file = {

src/output/driver_lexer.mll

@@ -45,8 +45,7 @@
         "type", TYPE;
         "prop", PROP;
         "filename", FILENAME;
-        "apply_before_split_goals", BEFORE_SPLIT;
-        "apply_after_split_goals", AFTER_SPLIT;
+        "transformations", TRANSFORMS;
         "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 BEFORE_SPLIT AFTER_SPLIT PLUGIN
+%token LOGIC TYPE PROP FILENAME TRANSFORMS PLUGIN
 
 %type <Driver_ast.file> file
 %start file
@@ -59,8 +59,7 @@ global:
 | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
 | FAIL STRING STRING { RegexpFailure ($2, $3) }
 | FILENAME STRING { Filename $2 }
-| BEFORE_SPLIT list0_string END { Beforesplit $2 }
-| AFTER_SPLIT list0_string END { Aftersplit $2 }
+| TRANSFORMS list0_string END { Transforms $2 }
 | PLUGIN STRING STRING { Plugin ($2,$3) }
 ;
 

src/test.why

@@ -26,7 +26,7 @@ end
 
 theory Test_conjunction
        use import prelude.Int
-       goal G : forall x:int. x*x=4 -> (x*x*x=8 or x*x*x=-8) and x*x*2 = 8
+       goal G : forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x=-8) and x*x*2 = 8)
 end
 
 

src/transform/split_conjunction.ml

+open Ident
 open Term
 open Theory
 
@@ -6,11 +7,18 @@ let list_fold_product f acc l1 l2 =
     (fun acc e1 ->
        List.fold_left 
          (fun acc e2 -> f acc e1 e2) 
-         l2 acc) 
+         acc l2) 
     acc l1
 
 let rec split_pos split_neg acc f =
-  let split_pos = split_pos split_neg in
+  let split_pos acc f = 
+    let p = split_pos split_neg acc f in
+(*    Format.printf "@[<hov 2>f : %a@\n acc : %a :@\n %a@]@." 
+      Pretty.print_fmla f
+      (Pp.print_list Pp.semi Pretty.print_fmla) acc
+      (Pp.print_list Pp.semi Pretty.print_fmla) p;*)
+    p in
+
   match f.f_node with
     | Ftrue -> acc
     | Ffalse -> f::acc
@@ -79,14 +87,11 @@ let split_pos = split_pos (fun acc x -> x::acc)
 let elt d =
   match d.d_node with
     | Dprop (Pgoal,pr,f) ->
-        begin
-          try
-            let l = split_pos [] f in
-            List.map (fun p -> create_prop_decl Pgoal pr p) l
-          with Exit -> [d]
-        end
-    | _ -> [d]
+        let l = split_pos [] f in
+        List.map (fun p -> [create_prop_decl Pgoal 
+                              (create_prop (id_clone (pr_name pr))) p]) l
+    | _ -> [[d]]
 
-let t () = Transform.elt elt
+let t () = Transform.elt' elt
 
-let () = Driver.register_transform "split_conjunction" t
+let () = Driver.register_transform' "split_conjunction" t

src/transform/split_goals.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+open Theory  
+open Context
+
+let t () =
+  let f ctxt0 (ctxt,l) =
+    let decl = ctxt0.ctxt_decl in
+    match decl.d_node with
+      | Dprop (Pgoal, _, _) -> (ctxt, add_decl ctxt decl :: l)
+      | Dprop (Plemma, pr, f) ->
+          let d1 = create_prop_decl Paxiom pr f in
+          let d2 = create_prop_decl Pgoal  pr f in
+          (add_decl ctxt d1,
+           add_decl ctxt d2 :: l)
+      | _ -> (add_decl ctxt decl, l) 
+  in
+  let g = Transform.fold f (fun env -> init_context env, []) in
+  Transform.conv_res g snd

src/transform/split_goals.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+val t : unit -> Transform.ctxt_list_t

src/transform/transform.ml

@@ -197,21 +197,6 @@ let elt_of_oelt ~ty ~logic ~ind ~prop ~use ~clone d =
 let fold_context_of_decl f ctxt env ctxt_done d =
   let env,decls = f ctxt env d in
   env,List.fold_left add_decl ctxt_done decls
-  
-let split_goals () =
-  let f ctxt0 (ctxt,l) =
-    let decl = ctxt0.ctxt_decl in
-    match decl.d_node with
-      | Dprop (Pgoal, _, _) -> (ctxt, add_decl ctxt decl :: l)
-      | Dprop (Plemma, pr, f) ->
-          let d1 = create_prop_decl Paxiom pr f in
-          let d2 = create_prop_decl Pgoal  pr f in
-          (add_decl ctxt d1,
-           add_decl ctxt d2 :: l)
-      | _ -> (add_decl ctxt decl, l) 
-  in
-  let g = fold f (fun env -> init_context env, []) in
-  conv_res g snd
 
 let remove_lemma =
   let f d =
@@ -235,6 +220,8 @@ let identity =
   { all = (fun x -> x);
     clear = (fun () -> ()); }
 
+let identity' = singleton identity
+
 let rewrite_elt rt rf d =
   match d.d_node with
     | Dtype _ -> [d]

src/transform/transform.mli

@@ -37,6 +37,9 @@ val compose' : context list t -> 'a list t -> 'a list t
 
 val singleton : 'a t -> 'a list t 
 
+val conv_res : 'a t -> ('a -> 'b) -> 'b t
+(* There is no memoisation is this only for constant 
+   modification of the result *)
 
 (* apply a transformation and memoise *)
 val apply : 'a t -> context -> 'a
@@ -87,14 +90,13 @@ val elt_env' : (env -> (decl -> decl list list)) -> context list t
 
 (* Utils *)
 
-val split_goals : unit -> context list t
-
 exception NotGoalContext
 val goal_of_ctxt : context -> prop
 (* goal_of_ctxt ctxts return the goal of a goal context
    the ctxt must end with a goal.*)
 
 val identity : context t
+val identity' : context list t
 
 
 val rewrite_elt :