- Ajout de split_conjunction
 - Ajout du choix d'appliquer les transformations avant ou après la séparation
   en un but par contexte (certainement à modifier)
 - Ajout de quelques transformations et plugins
 - ajout des options list-printers et list-transforms

Makefile.in

@@ -116,7 +116,8 @@ UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
 PARSER_CMO := parser.cmo lexer.cmo typing.cmo 
 PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 
-TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo 
+TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
+	split_conjunction.cmo 
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
 DRIVER_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo
@@ -208,17 +209,17 @@ WHYVO=lib/coq/Why.vo
 bench:: $(BINARY) 
 	sh bench/bench "$(BINARY) -I lib/prelude/"
 
-BENCH_PLUGINS_CMO := helloworld.cmo
+BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.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
+	bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I lib/prelude/ \
+        --output - --goal Test.G src/test.why
 
 # installation
 ##############
@@ -400,7 +401,7 @@ apidoc: $(OCAMLDOCSRC)
 .ml.cmx:
 	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $<
 
-.ml.cmxs: $*.cmo
+%.cmxs: %.ml %.cmx
 	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(INCLUDES) -o $@ $<
 
 .mll.ml:

bench/plugins/helloworld.drv

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

bench/plugins/simplify_array.drv

+plugin "simplify_array.cmo" "simplify_array.cmxs"
+
+printer "why3"
+
+filename "%f-%t-%s.why"
+
+apply_after_split_goals
+        "simplify_array"
+end
\ No newline at end of file

bench/plugins/simplify_array.ml

+open Term
+open Termlib
+open Theory
+
+open Transform
+
+let prelude = ["prelude"]
+let array = "Array"
+let store = ["store"]
+let select = ["select"]
+
+let make_rt_rf =
+  let rec rt ctxt t =
+    let t = t_map (rt ctxt) (rf ctxt) t in
+    let array  = find_theory ctxt.ctxt_env prelude array in
+    let store  = (find_l array.th_export store).ls_name in
+    let select = (find_l array.th_export select).ls_name in
+    match t.t_node with
+      | Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
+          when cloned_from ctxt lselect.ls_name select &&
+            cloned_from ctxt lstore.ls_name store &&
+            t_equal_alpha a1 a2 -> b
+      | _ -> t
+  and rf ctxt f = f_map (rt ctxt) (rf ctxt) f  in
+  rt,rf
+  
+let t () =
+  let rt,rf = make_rt_rf in
+  Transform.rewrite_map rt rf
+
+let () = Driver.register_transform "simplify_array" t

lib/drivers/alt_ergo.drv

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

lib/drivers/why3_inline_all.drv

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

lib/drivers/why3_split_conjunction.drv

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

src/main.ml

@@ -36,6 +36,8 @@ let which_goals = ref Gall
 let timeout = ref 10
 let call = ref false
 let output = ref None
+let list_printers = ref false
+let list_transforms = ref false
 
 let () = 
   Arg.parse 
@@ -59,6 +61,8 @@ let () =
      "--driver", Arg.String (fun s -> driver := Some s),
      "<file>  set the driver file";
      "--timeout", Arg.Set_int timeout, "set the timeout used when calling provers (0 unlimited, default 10)";
+     "--list-printers", Arg.Set list_printers, "list the printers registered";
+     "--list-transforms", Arg.Set list_transforms, "list the transformation registered";
     ]
     (fun f -> Queue.push f files)
     "usage: why [options] files..."
@@ -131,8 +135,9 @@ let transform env l =
 *)
 
 
-let extract_goals env acc th =
+let extract_goals 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 Transform.split_goals ctxt in
   let l = List.rev_map (fun ctxt -> (th,ctxt)) l in
   List.rev_append l acc
@@ -156,11 +161,11 @@ let do_file env drv filename_printer file =
       (* Extract the goal(s) *)
       let goals = 
         match !which_goals with
-          | Gall ->  Mnm.fold (fun _ th acc -> extract_goals env acc th) m []
+          | Gall ->  Mnm.fold (fun _ th acc -> extract_goals env drv acc th) m []
           | Gtheory s ->  
               begin
                 try 
-                  extract_goals env [] (Mnm.find s m)
+                  extract_goals env drv [] (Mnm.find s m)
                 with Not_found -> 
                   eprintf "File %s : --goals_of : Unknown theory %s@." file s; exit 1
               end
@@ -180,7 +185,7 @@ let do_file env drv filename_printer file =
                 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
+              let goals = extract_goals env drv [] th in
               List.filter (fun (_,ctxt) ->
                              match ctxt.ctxt_decl.d_node with
                                | Dprop (_,{pr_name = pr_name}) -> 
@@ -188,7 +193,7 @@ let do_file env drv filename_printer file =
                                | _ -> assert false) goals in
       (* Apply transformations *)
       let goals = List.map 
-        (fun (th,ctxt) -> (th,Driver.transform_context drv ctxt))
+        (fun (th,ctxt) -> (th,Driver.apply_after_split drv ctxt))
         goals in
       (* Pretty-print the goals or call the prover *)
       match !output with
@@ -230,6 +235,18 @@ let () =
     let drv = match !driver with
       | None -> None
       | Some file -> Some (load_driver file env) in
+    if !list_printers then 
+      begin
+        printf "@[<hov 2>printers :@\n%a@]@."
+          (Pp.print_list Pp.newline Pp.string) (Driver.list_printers ());
+        exit 0
+      end;
+    if !list_transforms then 
+      begin
+        printf "@[<hov 2>transforms :@\n%a@]@."
+          (Pp.print_list Pp.newline Pp.string) (Driver.list_transforms ());
+        exit 0          
+      end;
     let filename_printer = Ident.create_ident_printer 
       ~sanitizer:file_sanitizer [] in
     Queue.iter (do_file env drv filename_printer) files

src/output/driver.ml

@@ -121,17 +121,18 @@ let print_translation fmt = function
 type printer = driver -> formatter -> context -> unit
 
 and driver = {
-  drv_printer    : printer option;
-  drv_context    : context;
-  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;
+  drv_printer     : printer option;
+  drv_context     : context;
+  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_rules       : theory_rules list;
+  drv_thprelude   : string Hid.t;
   (* the first is the translation only for this ident, the second is also for representant *)
-  drv_theory     : (translation * translation) Hid.t;
-  drv_with_ctxt  : translation Hid.t;
+  drv_theory      : (translation * translation) Hid.t;
+  drv_with_ctxt   : translation Hid.t;
 }
 
 (*
@@ -148,12 +149,16 @@ let (transforms : (string, unit -> Transform.ctxt_t) Hashtbl.t) = Hashtbl.create
 
 let register_transform name transform = Hashtbl.replace transforms name transform
 
+let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
+
 (** registering printers *)
 
 let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17
 
 let register_printer name printer = Hashtbl.replace printers name printer
 
+let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
+
 (*
 let () = 
   Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver";
@@ -209,30 +214,18 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
     with Not_found ->
       let t23 = if cloned then (Tag Snm.empty),t else t,(Tag Snm.empty) in
       Hid.add driver.drv_theory id t23 in
-  let rec find_l ns = function
-    | [] -> assert false
-    | [a] -> Mnm.find a ns.ns_ls
-    | a::l -> find_l (Mnm.find a ns.ns_ns) l in
-  let rec find_ty ns = function
-    | [] -> assert false
-    | [a] -> Mnm.find a ns.ns_ts
-    | a::l -> find_ty (Mnm.find a ns.ns_ns) 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 add = function
     | Rremove (c,(loc,q)) -> 
         begin
           try
-            add_htheory c (find_pr th.th_export q).pr_name Remove
+            add_htheory c (Transform.find_pr th.th_export q).pr_name Remove
           with Not_found -> errorm ~loc "Unknown axioms %s" 
             (string_of_qualid qualid q)
         end 
     | Rsyntaxls ((loc,q),s) -> 
         begin
           try
-            let ls = (find_l th.th_export q) in
+            let ls = (Transform.find_l th.th_export q) in
             check_syntax loc s (List.length ls.ls_args);
             add_htheory false ls.ls_name (Syntax s)
           with Not_found -> errorm ~loc "Unknown logic %s" 
@@ -241,7 +234,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
     | Rsyntaxty ((loc,q),s) -> 
         begin
           try
-            let ts = find_ty th.th_export q in
+            let ts = Transform.find_ty th.th_export q in
             check_syntax loc s (List.length ts.ts_args);
             add_htheory false ts.ts_name (Syntax s)
           with Not_found -> errorm ~loc "Unknown type %s" 
@@ -250,7 +243,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
     | Rtagls (c,(loc,q),s) ->
         begin
           try
-            add_htheory c (find_l th.th_export q).ls_name 
+            add_htheory c (Transform.find_l th.th_export q).ls_name 
               (Tag (Snm.singleton s))
           with Not_found -> errorm ~loc "Unknown logic %s" 
             (string_of_qualid qualid q)
@@ -258,7 +251,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
     | Rtagty (c,(loc,q),s) ->
         begin
           try
-            add_htheory c (find_ty th.th_export q).ts_name 
+            add_htheory c (Transform.find_ty th.th_export q).ts_name 
               (Tag (Snm.singleton s))
           with Not_found -> errorm ~loc "Unknown type %s" 
             (string_of_qualid qualid q)
@@ -266,7 +259,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
     | Rtagpr (c,(loc,q),s) ->
         begin
           try
-            add_htheory c (find_pr th.th_export q).pr_name 
+            add_htheory c (Transform.find_pr th.th_export q).pr_name 
               (Tag (Snm.singleton s))
           with Not_found -> errorm ~loc "Unknown proposition %s" 
             (string_of_qualid qualid q)
@@ -278,13 +271,14 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
 
 let load_driver file env =
   let f = load_file file in
-  let prelude = ref None in
-  let printer = ref None in
-  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 prelude     = ref None in
+  let printer     = ref None in
+  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 regexps     = ref [] in
   let set_or_raise loc r v error =
     if !r <> None then errorm ~loc "duplicate %s" error
     else r := Some v in 
@@ -303,29 +297,33 @@ 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"
+    | Beforesplit s -> set_or_raise loc beforesplit s "beforesplit"
+    | Aftersplit s -> set_or_raise loc aftersplit s "aftersplit"
     | 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 = 
+  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
-  { drv_printer    = !printer;
-    drv_context    = Context.init_context env;
-    drv_prover     = {Call_provers.pr_call_stdin = !call_stdin;
-                      pr_call_file               = !call_file;
-                      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;
-    drv_with_ctxt  = Hid.create 1;
+    let beforesplit = trans beforesplit in
+    let aftersplit = trans aftersplit in
+  { drv_printer     = !printer;
+    drv_context     = Context.init_context env;
+    drv_prover      = {Call_provers.pr_call_stdin = !call_stdin;
+                       pr_call_file               = !call_file;
+                       pr_regexps                 = regexps};
+    drv_prelude     = !prelude;
+    drv_filename    = !filename;
+    drv_beforesplit = beforesplit;
+    drv_aftersplit  = aftersplit;
+    drv_rules       = f.f_rules;
+    drv_thprelude   = Hid.create 1;
+    drv_theory      = Hid.create 1;
+    drv_with_ctxt   = Hid.create 1;
   }
 
 (** querying drivers *)
@@ -355,9 +353,12 @@ let syntax_arguments s print fmt l =
  
 (** using drivers *)
 
-let transform_context drv ctxt =
+let transform_context list ctxt =
   List.fold_left (fun ctxt t -> Transform.apply t ctxt) 
-    ctxt drv.drv_transformations
+    ctxt list
+
+let apply_before_split drv = transform_context drv.drv_beforesplit
+let apply_after_split drv = transform_context drv.drv_aftersplit
 
 let print_context drv fmt ctxt = match drv.drv_printer with
   | None -> errorm "no printer"

src/output/driver.mli

@@ -46,10 +46,14 @@ val register_printer : string -> printer -> unit
 
 val register_transform : string -> (unit -> Transform.ctxt_t) -> unit
 
+val list_printers : unit -> string list
+val list_transforms : unit -> string list
+
 (** using drivers *)
 
 (** transform context *)
-val transform_context : driver -> context -> context
+val apply_before_split : driver -> context -> context
+val apply_after_split : driver -> context -> context
 
 (** print_context *)
 val print_context : printer

src/output/driver_ast.mli

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

src/output/driver_lexer.mll

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

src/test.why

@@ -18,6 +18,18 @@ theory Test
   goal G2 : forall x:int. 0 = 1
 end
 
+theory Test_simplify_array
+       use import prelude.Array
+       goal G : forall x,y:int. forall m: (int,int) t. 
+       select(store(m,y,x),y) = x
+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
+end
+
+
 (*
 Local Variables: 
 compile-command: "make -C .. test"

src/transform/split_conjunction.ml

+open Term
+open Theory
+
+let split_pos = 
+  let rec rf acc f =
+    match f.f_node with
+      | Ftrue -> acc
+      | Ffalse -> f::acc
+      | Fapp _ -> f::acc
+      | Fbinop (Fand,f1,f2) -> rf (rf acc f2) f1
+      | Fbinop (Fimplies,f1,f2) -> 
+          List.fold_left (fun acc f -> (f_implies f1 f)::acc) 
+          acc (rf [] f2)
+      | Fbinop (Fiff,f1,f2) -> rf (rf acc (f_implies f1 f2)) (f_implies f2 f1)
+      | Fbinop (For,_,_) -> f::acc
+      | Fnot _ -> f::acc
+      | Fif (fif,fthen,felse) -> 
+          rf 
+            (rf acc (f_implies fif fthen)) 
+            (f_implies (f_not fif) felse)
+      | Flet (t,fb) ->
+          let vs,f = f_open_bound fb in
+          List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (rf [] f)
+      | Fcase _ -> (* TODO better *) f::acc
+      | Fquant (Fforall,fmlaq) ->
+          let vsl,trl,fmla = f_open_quant fmlaq in
+          List.fold_left (fun acc f -> 
+                            (* Remove unused variable*)
+                         (f_forall vsl trl f)::acc) acc (rf [] fmla)
+      | Fquant (Fexists,_) -> f::acc in
+  rf []
+
+
+let elt d =
+  match d.d_node with
+    | Dprop (Pgoal,pr) ->
+        begin
+          try
+            let l = split_pos pr.pr_fmla in
+            List.map (fun p ->
+                        create_prop_decl Pgoal
+                          (create_prop (Ident.id_clone pr.pr_name) p)) l
+          with Exit -> [d]
+        end
+    | _ -> [d]
+
+let t () = Transform.elt elt
+
+let () = Driver.register_transform "split_conjunction" t

src/transform/transform.ml

@@ -17,6 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Term
 open Ident
 open Theory
 open Context
@@ -145,6 +146,19 @@ let split_goals =
   let g = fold_env f (fun env -> init_context env, []) in
   conv_res g snd
 
+let remove_lemma =
+  let f d =
+    match d.d_node with
+      | Dprop (Plemma, f) ->
+          let da = create_prop_decl Paxiom 
+            (create_prop (id_clone f.pr_name) f.pr_fmla) in
+          let dg = create_prop_decl Pgoal
+            (create_prop (id_clone f.pr_name) f.pr_fmla) in
+          [dg;da]
+      | _ ->  [d]
+  in
+  elt f
+
 exception NotGoalContext
 
 let goal_of_ctxt ctxt =
@@ -152,50 +166,104 @@ let goal_of_ctxt ctxt =
     | Dprop (Pgoal,pr) -> pr
     | _ -> raise NotGoalContext
 
-(*
-let extract_goals () =
-  let f ctxt0 (ctxt,l) =
-    let decl = ctxt0.ctxt_decl in    
-    match decl.d_node with
-      | Dprop (Pgoal, f) -> 
-	  ctxt, (f.pr_name,f.pr_fmla,ctxt) :: l
-      | Dprop (Plemma, f) ->
-          let d = create_prop_decl Paxiom f in
-          add_decl ctxt d, (f.pr_name, f.pr_fmla,ctxt) :: l
-      | _ -> 
-	  add_decl ctxt decl, l
-  in
-  let g = fold_env f (fun env -> init_context env, []) in
-  conv_res g snd
-*)
-
 let identity = 
   { all = (fun x -> x);
     clear = (fun () -> ()); }
 
-(*
-let cloned_from_ts env ctxt l s ls1 =
-  assert false (*TODO*)
+let rewrite_elt rt rf d =
+  match d.d_node with
+    | Dtype _ -> [d]
+    | Dlogic l -> [create_logic_decl (List.map 
+        (function 
+           | Lfunction(ls,Some def) -> 
+               let (ls,vsl,term) = open_fs_defn def in
+               let term = rt term in
+               Lfunction (ls,Some (make_fs_defn ls vsl term))
+           | Lpredicate(ls,Some def) ->
+               let (ls,vsl,fmla) = open_ps_defn def in
+               let fmla = rf fmla in
+               Lpredicate (ls,Some (make_ps_defn ls vsl fmla))
+           | l -> l) l)]
+    | Dind indl -> [create_ind_decl 
+        (List.map (fun (ls,pl) -> ls, 
+        (List.map
+           (fun pr -> shortcut_for_discussion_dont_be_mad_andrei_please
+              pr.pr_name (rf pr.pr_fmla)) pl)) indl)]
+    |Dprop (k,pr) -> [create_prop_decl k
+       (shortcut_for_discussion_dont_be_mad_andrei_please
+          pr.pr_name (rf pr.pr_fmla))]
+    |Duse _ |Dclone _ -> [d]
+
+let rewrite_elt rt rf = elt (rewrite_elt rt rf)
+
+let rewrite_map rt rf ctxt1 ctxt2 =
+  let d = ctxt1.ctxt_decl in
+  match d.d_node with
+    | Dtype _ -> add_decl ctxt2 d
+    | Dlogic l -> add_decl ctxt2 (create_logic_decl (List.map 
+        (function 
+           | Lfunction(ls,Some def) -> 
+               let (ls,vsl,term) = open_fs_defn def in
+               let term = rt ctxt1 term in
+               Lfunction (ls,Some (make_fs_defn ls vsl term))
+           | Lpredicate(ls,Some def) ->
+               let (ls,vsl,fmla) = open_ps_defn def in
+               let fmla = rf ctxt1 fmla in
+               Lpredicate (ls,Some (make_ps_defn ls vsl fmla))
+           | l -> l) l))
+    | Dind indl -> add_decl ctxt2 (create_ind_decl 
+        (List.map (fun (ls,pl) -> ls, 
+        (List.map
+           (fun pr -> shortcut_for_discussion_dont_be_mad_andrei_please
+              pr.pr_name (rf ctxt1 pr.pr_fmla)) pl)) indl))
+    |Dprop (k,pr) -> add_decl ctxt2 (create_prop_decl k
+       (shortcut_for_discussion_dont_be_mad_andrei_please
+          pr.pr_name (rf ctxt1 pr.pr_fmla)))
+    |Duse _ |Dclone _ -> add_decl ctxt2 d
+
+let rewrite_map rt rf = map (rewrite_map rt rf)
+  
+let rec find_l ns = function
+  | [] -> assert false
+  | [a] -> Mnm.find a ns.ns_ls
+  | a::l -> find_l (Mnm.find a ns.ns_ns) l
+      
+let rec find_ty ns = function
+  | [] -> assert false
+  | [a] -> Mnm.find a ns.ns_ts
+  | a::l -> find_ty (Mnm.find a ns.ns_ns) l
+  
+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
+
+
+let cloned_from ctxt i1 i2 = 
+  try
+    i1 = i2 || Sid.mem i2 (Mid.find i1 ctxt.ctxt_cloned)
+  with Not_found -> false
+
+(* let find_theory *)
+
+(* let cloned_from_ts ctxt slth sth sil ls1 = *)
 (*   try *)
-(*     let th = Typing.find_theory env l in *)
-(*     let ls2 = Mnm.find s th.th_export.ns_ts in *)
+(*     let th = find_theory ctxt.ctxt_env slth sth in *)
+(*     let ls2 = find_ty th.th_export sil in *)
 (*     Context_utils.cloned_from ctxt ls1.ts_name ls2.ts_name *)
-(*   with Loc.Located _ -> assert false *)
-    
+(*   with Loc.Located _ -> raise Not_found *)
     
-let cloned_from_ls env ctxt l s ls1 =
-  assert false (*TODO*)
+(* let cloned_from_ls ctxt slth sth sil ls1 = *)
 (*   try *)
-(*     let th = Typing.find_theory env l in *)
-(*     let ls2 = Mnm.find s th.th_export.ns_ls in *)
-(*     Context_utils.cloned_from ctxt ls1.ls_name ls2.ls_name *)
+(*     let th = find_theory ctxt.ctxt_env l in *)