ajout de la trnasformation flatten

Makefile.in

@@ -112,7 +112,8 @@ 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 := transform.cmo simplify_recursive_definition.cmo inlining.cmo\
+	flatten.cmo
 
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 

src/main.ml

@@ -27,6 +27,7 @@ let loadpath = ref []
 let print_stdout = ref false
 let simplify_recursive = ref false
 let inlining = ref false
+let transform = ref false
 
 let () = 
   Arg.parse 
@@ -38,10 +39,13 @@ let () =
      "--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";
+     "--transform", Arg.Set transform, "transform the goal (--inline,and --simplify-recursive set it) ";
     ]
     (fun f -> files := f :: !files)
     "usage: why [options] files..."
 
+let transform = !transform || !simplify_recursive || !inlining
+
 let rec report fmt = function
   | Lexer.Error e ->
       fprintf fmt "lexical error: %a" Lexer.report e;
@@ -63,23 +67,27 @@ let type_file env file =
   if !parse_only then env else Typing.add_theories env f
 
 let transform l =
-  let transform = !simplify_recursive || !inlining in
+  let l = Typing.list_theory l in
   if !print_stdout && not transform then 
-    List.iter (Pretty.print_theory Format.std_formatter) 
-      (Typing.list_theory l)
+    List.iter (Pretty.print_theory Format.std_formatter) l
   else
-    let l = List.map (fun t -> t.Theory.th_decls) (Typing.list_theory l) in
+    let l = List.map (fun t -> t,Transform.apply Flatten.t t.Theory.th_decls)
+      l in
     let l = if !simplify_recursive 
     then 
-      List.map (fun t -> Transform.apply 
-                     Simplify_recursive_definition.t_use t) l
+      List.map (fun (t,dl) -> t,Transform.apply 
+                     Simplify_recursive_definition.t dl) l
     else l in
     let l = if !inlining
     then
-      List.map (fun t -> Transform.apply Inlining.t_use t) l
+      List.map (fun (t,dl) -> t,Transform.apply Inlining.t dl) l
     else l in
     if !print_stdout then 
-      List.iter (Pretty.print_decl_or_use_list Format.std_formatter) l
+      List.iter (fun (t,dl) ->
+                   Format.printf "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n@?" 
+                     Pretty.print_ident t.Theory.th_name 
+                     Pretty.print_decl_list dl
+                ) l
 
 
 let () =

src/parser/typing.ml

@@ -915,7 +915,7 @@ let add_theories =
     (fun env pt -> let _, env = add_theory env pt in env) 
 
 let list_theory env = 
-  M.fold (fun _ v acc -> v::acc) env.theories []
+  List.rev (M.fold (fun _ v acc -> v::acc) env.theories [])
 
 (*
 Local Variables: 

src/pretty.ml

@@ -54,7 +54,7 @@ let rec print_term fmt t = match t.t_node with
   | Tconst (ConstReal _) ->
       fprintf fmt "<real constant>"
   | Tapp (s, tl) ->
-      fprintf fmt "@[<hov>(%a(%a)@ : %a)@]" 
+      fprintf fmt "@[<hov>(%a(%a)@ : %a)@](" 
 	print_ident s.fs_name (print_list comma print_term) tl
 	print_ty t.t_ty
   | Tlet (t1,tbound) -> 
@@ -156,9 +156,9 @@ let print_logic_decl fmt = function
 
 let print_decl fmt d = match d.d_node with
   | Dtype tl -> 
-      fprintf fmt "@[<hov>%a@]@ (* *)" (print_list newline print_ty_decl) tl
+      fprintf fmt "@[<hov>%a@ (* *)@]" (print_list newline print_ty_decl) tl
   | Dlogic ldl -> 
-      fprintf fmt "@[<hov>%a@]@ (* *)" 
+      fprintf fmt "@[<hov>%a@ (* *)@]" 
 	(print_list newline print_logic_decl) ldl 
   | Dprop (k,id,fmla) -> 
       fprintf fmt "%s %a :@ %a@\n" 
@@ -166,6 +166,9 @@ let print_decl fmt d = match d.d_node with
         print_ident id
         print_fmla fmla
 
+let print_decl_list fmt de = 
+  fprintf fmt "@[<hov>%a@]" (print_list newline print_decl) de
+
 let print_decl_or_use fmt = function
   | Decl d -> fprintf fmt "%a" print_decl d
   | Use u -> fprintf fmt "use export %a@\n" print_ident u.th_name

src/pretty.mli

@@ -18,10 +18,13 @@
 (**************************************************************************)
 
 open Format
+open Ident
 open Ty
 open Term
 open Theory
 
+val print_ident : formatter -> ident -> unit
+
 val print_vsymbol : formatter -> vsymbol -> unit
 
 val print_fsymbol : formatter -> fsymbol -> unit
@@ -36,6 +39,8 @@ val print_fmla : formatter -> fmla -> unit
 
 val print_decl : formatter -> decl -> unit
 
+val print_decl_list : formatter -> decl list -> unit
+
 val print_decl_or_use : formatter -> decl_or_use -> unit
 
 val print_decl_or_use_list : formatter -> decl_or_use list -> unit

src/transform/flatten.ml

+open Theory
+
+let elt a =
+  let rec aux acc = function
+    | Decl a -> a::acc
+    | Use t -> List.fold_left aux acc t.th_decls in
+  List.rev (aux [] a)
+
+
+let t = Transform.TDecl_or_Use_Decl.elt elt

src/transform/flatten.mli

+(* a list of decl_or_use to a list of decl *)
+
+val t : (Theory.decl_or_use,Theory.decl) Transform.t

src/transform/inlining.mli

 (* Inline the definition not recursive *)
 
-
 val t : (Theory.decl,Theory.decl) Transform.t
 
 val t_use : (Theory.decl_or_use,Theory.decl_or_use) Transform.t

src/transform/transform.ml

@@ -22,10 +22,12 @@
 type 'a hashconsedlist = (int * 'a list) list
 
 
+type 'a tag = 'a -> int
+
 module type Sig =
 sig
   type t
-  val tag : t -> int
+  val tag : t tag
 end
 
 (* The datastructure for hashconsed list *)
@@ -106,19 +108,19 @@ let memo f tag h x =
 
 module type S =
 sig
-  type elt1
-  type elt2
+  type t1
+  type t2
 
-  val all : (elt1 list -> elt2 list) -> (elt1,elt2) t
-  val fold_map_right : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
-  val fold_map_left : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
-  val elt : (elt1 -> elt2 list) -> (elt1,elt2) t
+  val all : (t1 list -> t2 list) -> (t1,t2) t
+  val fold_map_right : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
+  val fold_map_left : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
+  val elt : (t1 -> t2 list) -> (t1,t2) t
 end
 
 module Make (X1 : Sig) (X2 : Sig) =
 struct
-  type elt1 = X1.t
-  type elt2 = X2.t
+  type t1 = X1.t
+  type t2 = X2.t
 
   module LH1 = LH(X1)
   module LH2 = LH(X2)
@@ -190,8 +192,6 @@ module SDecl =
     let tag x = x.d_tag
   end
 
-module TDecl = Make(SDecl)(SDecl)
-
 module SDecl_or_Use =
   struct
     type t = decl_or_use
@@ -200,14 +200,26 @@ module SDecl_or_Use =
       | Use t -> 1+t.th_name.Ident.id_tag 
   end
 
-module TDecl_or_Use = Make(SDecl_or_Use)(SDecl_or_Use)
-
 module STheory =
   struct
     type t = theory
     let tag t = t.th_name.Ident.id_tag 
   end
 
-module TTheory = Make(STheory)(STheory)
+module STerm =
+  struct
+    type t = Term.term
+    let tag t = t.Term.t_tag
+  end
+
+module SFmla =
+  struct
+    type t = Term.fmla
+    let tag t = t.Term.f_tag
+  end
 
+module TDecl = Make(SDecl)(SDecl)
+module TDecl_or_Use = Make(SDecl_or_Use)(SDecl_or_Use)
+module TDecl_or_Use_Decl = Make(SDecl_or_Use)(SDecl)
+module TTheory = Make(STheory)(STheory)
 module TTheory_Decl = Make(STheory)(SDecl)

src/transform/transform.mli

@@ -33,35 +33,56 @@ val apply : ('a,'b) t -> 'a list -> 'b list
 (* clear the datastructures used to store the memoisation *)
 val clear : ('a,'b) t -> unit
 
+(* The signature of a module of transformation from elt1 to elt2*)
 module type S =
 sig
   (* The type of the elements of the list*)
-  type elt1
-  type elt2
+  type t1
+  type t2
 
   (* The general tranformation only one memoisation is performed with
      the argument given *)
-  val all : (elt1 list -> elt2 list) -> (elt1,elt2) t
+  val all : (t1 list -> t2 list) -> (t1,t2) t
 
   (* map the element of the list from the first to the last.
      only one memoisation is performed *)
-  val fold_map_right : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
+  val fold_map_right : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
 
   (* map the element of the list from the last to the first.
      A memoisation is performed at each step *)
-  val fold_map_left : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
+  val fold_map_left : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
 
   (* map the element of the list without an environnment.
      A memoisation is performed at each step, and for each elements *)
-  val elt : (elt1 -> elt2 list) -> (elt1,elt2) t
+  val elt : (t1 -> t2 list) -> (t1,t2) t
     
 end
 
+(* a type with a tag function  *)
+type 'a tag
+
+module type Sig =
+  sig
+    type t
+    val tag : t tag
+  end
+
 open Theory
+open Term
 
-module TDecl : S with type elt1 = decl and type elt2 = decl
-module TDecl_or_Use : S with type elt1 = decl_or_use and type elt2 = decl_or_use
-module TTheory : S with type elt1 = theory and type elt2 = theory
-module TTheory_Decl : S with type elt1 = theory and type elt2 = decl
+(* They are the only modules of signature S, we can have *)
+module STerm : Sig with type t = term
+module SFmla : Sig with type t = fmla
+module SDecl : Sig with type t = decl
+module SDecl_or_Use : Sig with type t = decl_or_use
+module STheory : Sig with type t = theory
 
+(* The functor to construct transformation from one S.t to another *)
+module Make (X1 : Sig)(X2 : Sig) : S with type t1 = X1.t with type t2 = X2.t
 
+(* Predefined transformation *)
+module TDecl : S with type t1 = decl and type t2 = decl
+module TDecl_or_Use : S with type t1 = decl_or_use and type t2 = decl_or_use
+module TDecl_or_Use_Decl : S with type t1 = decl_or_use and type t2 = decl
+module TTheory : S with type t1 = theory and type t2 = theory
+module TTheory_Decl : S with type t1 = theory and type t2 = decl