affichage apres la transformation

bench/typing/good/alias1.why

+theory Test
+
+type t1 = t2
+
+type t5
+
+type t2 = t5
+
+logic f(x : t1, y : t2) : t5
+
+logic g(x : t1) : t5 = f(x,x) 
+
+end
\ No newline at end of file

src/main.ml

@@ -25,6 +25,7 @@ let type_only = ref false
 let debug = ref false
 let loadpath = ref []
 let print_stdout = ref false
+let print_simplify_recursive = ref false
 let () = 
   Arg.parse 
     ["--parse-only", Arg.Set parse_only, "stops after parsing";
@@ -32,7 +33,8 @@ let () =
      "--debug", Arg.Set debug, "sets the debug flag";
      "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
        "<dir>  adds dir to the loadpath";
-     "-print_stdout", Arg.Set print_stdout, "print the results to stdout";
+     "--print_stdout", Arg.Set print_stdout, "print the results to stdout";
+     "--print_simplify_recursive", Arg.Set print_simplify_recursive, "print the results of simplify recursive definition";
     ]
     (fun f -> files := f :: !files)
     "usage: why [options] files..."
@@ -63,6 +65,13 @@ let () =
     let l = List.fold_left type_file env !files in
     if !print_stdout then 
       List.iter (Pretty.print_theory Format.std_formatter) 
+        (Typing.list_theory l);
+    if !print_simplify_recursive then 
+      List.iter (fun t ->
+                   let de = Transform.apply 
+                     Simplify_recursive_definition.t_use t.Theory.th_decls in
+                   (Pp.print_list Pp.newline Pretty.print_decl_or_use) 
+                     Format.std_formatter de) 
         (Typing.list_theory l)
   with e when not !debug ->
     eprintf "%a@." report e;

src/pretty.ml

@@ -24,6 +24,8 @@ open Ty
 open Term
 open Theory
 
+let print_list_paren x = print_list_delim lparen rparen x
+
 let print_ident =
   let printer = create_printer () in
   let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
@@ -80,19 +82,25 @@ let rec print_fmla fmt f = match f.f_node with
 let print_fsymbol fmt {fs_name = fs_name; fs_scheme = tyl,ty} = 
   fprintf fmt "%a%a :@ %a" 
     print_ident fs_name
-    (print_list_par comma print_ty) tyl 
+    (print_list_paren comma print_ty) tyl 
     print_ty ty
 
 let print_psymbol fmt {ps_name = ps_name; ps_scheme = tyl} = 
   fprintf fmt "%a%a" 
     print_ident ps_name
-    (print_list_par comma print_ty) tyl 
+    (print_list_paren comma print_ty) tyl 
 
 let print_ty_decl fmt (ts,tydef) = match tydef,ts.ts_def with
-  | Tabstract,None -> fprintf fmt "type %a@." print_ident ts.ts_name
-  | Tabstract,Some f -> fprintf fmt "type %a =@ %a@." print_ident ts.ts_name
+  | Tabstract,None -> fprintf fmt "type %a%a@." 
+      (print_list_paren comma print_ident) ts.ts_args
+      print_ident ts.ts_name
+  | Tabstract,Some f -> fprintf fmt "type %a%a =@ %a@." 
+      (print_list_paren comma print_ident) ts.ts_args
+      print_ident ts.ts_name
       print_ty f
-  | Talgebraic d, None -> fprintf fmt "type %a =@ %a@." print_ident ts.ts_name
+  | Talgebraic d, None -> fprintf fmt "type %a%a =@ %a@." 
+      (print_list_paren comma print_ident) ts.ts_args
+      print_ident ts.ts_name
       (print_list newline print_fsymbol) d
   | Talgebraic _, Some _ -> assert false
 
@@ -103,12 +111,12 @@ let print_logic_decl fmt = function
   | Lfunction (fs,None) -> fprintf fmt "logic %a@." print_fsymbol fs
   | Lfunction (fs,Some (vsl,t)) -> 
       fprintf fmt "logic %a%a =@ %a@." print_ident fs.fs_name
-      (print_list_par comma print_vsymbol) vsl
+      (print_list_paren comma print_vsymbol) vsl
         print_term t
   | Lpredicate (fs,None) -> fprintf fmt "logic %a@." print_psymbol fs
   | Lpredicate (ps,Some (vsl,t)) -> 
       fprintf fmt "logic %a%a =@ %a@." print_ident ps.ps_name
-      (print_list_par comma print_vsymbol) vsl
+      (print_list_paren comma print_vsymbol) vsl
         print_fmla t
   | Linductive _ -> assert false (*TODO*)
 
@@ -123,9 +131,9 @@ let print_decl fmt d = match d.d_node with
         print_fmla fmla
 
 let print_decl_or_use fmt = function
-  | Decl d -> print_decl fmt d
+  | Decl d -> fprintf fmt "%a" print_decl d
   | Use u -> fprintf fmt "use export %a@." print_ident u.th_name
 
 let print_theory fmt t =
-  fprintf fmt "theory %a@.%a@.end" print_ident t.th_name 
+  fprintf fmt "theory %a@.%aend@." print_ident t.th_name 
     (print_list newline print_decl_or_use) t.th_decls

src/transform/simplify_recursive_definition.ml

@@ -149,3 +149,8 @@ let elt d =
         List.map (fun e -> create_type (List.map (Hid.find mem) e)) l
 
 let t = Transform.TDecl.elt elt
+
+let t_use = Transform.TDecl_or_Use.elt 
+  (function 
+     | Decl d -> List.map (fun d -> Decl d) (elt d) 
+     | Use _ as u -> [u])

src/transform/simplify_recursive_definition.mli

@@ -21,3 +21,5 @@
 (* Simplify the recursive type and logic definition *)
 
 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

@@ -92,7 +92,7 @@ let compose f g = {all = (fun x -> g.all (f.all x));
                    from_list = f.from_list;
                    to_list = g.to_list}
 
-let apply f x = f.to_list (f.all (f.from_list x))
+let apply f x = f.to_list (f.all (f.from_list (List.rev x)))
     
 let clear f = f.clear ()
 

src/transform/transform.mli

@@ -61,7 +61,7 @@ end
 open Theory
 
 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 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