pretty print et hashconslist maline (JC)

src/main.ml

@@ -24,7 +24,7 @@ let parse_only = ref false
 let type_only = ref false
 let debug = ref false
 let loadpath = ref []
-
+let print_stdout = ref false
 let () = 
   Arg.parse 
     ["--parse-only", Arg.Set parse_only, "stops after parsing";
@@ -32,6 +32,7 @@ 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";
     ]
     (fun f -> files := f :: !files)
     "usage: why [options] files..."
@@ -59,7 +60,10 @@ let type_file env file =
 let () =
   try
     let env = Typing.create !loadpath in
-    ignore (List.fold_left type_file env !files)
+    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)
   with e when not !debug ->
     eprintf "%a@." report e;
     exit 1

src/parser/typing.ml

@@ -783,6 +783,9 @@ let add_theories =
   List.fold_left
     (fun env pt -> let _, env = add_theory env pt in env) 
 
+let list_theory env = 
+  M.fold (fun _ v acc -> v::acc) env.theories []
+
 (*
 Local Variables: 
 compile-command: "make -C ../.. test"

src/parser/typing.mli

@@ -32,6 +32,8 @@ val add_theories : env -> Ptree.theory list -> env
 val find_theory : env -> Ptree.qualid -> Theory.theory
   (** searches for a theory using the environment's loadpath *)
 
+val list_theory : env -> Theory.theory list
+
 (** error reporting *)
 
 type error

src/pretty.ml

@@ -22,6 +22,7 @@ open Pp
 open Ident
 open Ty
 open Term
+open Theory
 
 let print_ident =
   let printer = create_printer () in
@@ -36,7 +37,7 @@ let rec print_ty fmt ty = match ty.ty_node with
   | Tyapp (s, [t]) -> 
       fprintf fmt "%a %a" print_ty t print_ident s.ts_name
   | Tyapp (s, l) -> 
-      fprintf fmt "(%a) %a" (print_list comma print_ty) l print_ident s.ts_name
+      fprintf fmt "(%a)@ %a" (print_list comma print_ty) l print_ident s.ts_name
   
 let rec print_term fmt t = match t.t_node with
   | Tbvar n -> 
@@ -44,40 +45,87 @@ let rec print_term fmt t = match t.t_node with
   | Tvar n -> 
       print_ident fmt n.vs_name
   | Tapp (s, tl) ->
-      fprintf fmt "(%a(%a) : %a)" 
+      fprintf fmt "(%a(%a@,)@ : %a@,@,)" 
 	print_ident s.fs_name (print_list comma print_term) tl
 	print_ty t.t_ty
   | Tlet (t1,tbound) -> 
       let vs,t2 = t_open_bound tbound in
-      fprintf fmt "(let %a = %a in %a)"
+      fprintf fmt "(let %a = %a in %a@,)"
       print_ident vs.vs_name print_term t1 print_term t2
   | Tcase _ -> assert false (*TODO*)
   | Teps _ -> assert false
 
 let rec print_fmla fmt f = match f.f_node with
   | Fapp (s,tl) -> 
-      fprintf fmt "(%a(%a))" 
+      fprintf fmt "(%a(%a@,)@,)" 
 	print_ident s.ps_name (print_list comma print_term) tl
   | Fquant (q,fbound) ->
       let vs,f = f_open_bound fbound in
-      fprintf fmt "(%s %a : %a. %a)"
+      fprintf fmt "(%s %a :@ %a.@ %a@,)"
         (match q with Fforall -> "forall" | Fexists -> "exists")
         print_ident vs.vs_name print_ty vs.vs_ty print_fmla f
-  | Ftrue -> fprintf fmt "(true)"
-  | Ffalse -> fprintf fmt "(false)"
+  | Ftrue -> fprintf fmt "(true@,)"
+  | Ffalse -> fprintf fmt "(false@,)"
   | Fbinop (b,f1,f2) -> 
-      fprintf fmt "(%a %s %a)"
+      fprintf fmt "(%a@ %s@ %a@,)"
         print_fmla f1
         (match b with 
            | Fand -> "and" | For -> "or" 
            | Fimplies -> "->" | Fiff -> "<->")
         print_fmla f2
-  | Fnot f -> fprintf fmt "(not %a)" print_fmla f
+  | Fnot f -> fprintf fmt "(not@ %a)" print_fmla f
   | _ -> assert false (*TODO*) 
 
-(*
+
+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_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 
+
+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
+      print_ty f
+  | Talgebraic d, None -> fprintf fmt "type %a =@ %a@." print_ident ts.ts_name
+      (print_list newline print_fsymbol) d
+  | Talgebraic _, Some _ -> assert false
+
+let print_vsymbol fmt {vs_name = vs_name; vs_ty = vs_ty} =
+  fprintf fmt "%a :@ %a" print_ident vs_name print_ty vs_ty
+
+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_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_fmla t
+  | Linductive _ -> assert false (*TODO*)
+
 let print_decl fmt d = match d.d_node with
-  | Dtype tl ->
-  | Dlogic ldl ->
-  | Dprop (k,id,fmla) ->
-*)
+  | Dtype tl -> fprintf fmt "(* *)@.%a" (print_list newline print_ty_decl) tl
+  | Dlogic ldl -> fprintf fmt "(* *)@.%a" 
+      (print_list newline print_logic_decl) ldl 
+  | Dprop (k,id,fmla) -> 
+      fprintf fmt "%s %a :@ %a@." 
+        (match k with Paxiom -> "axiom" | Pgoal -> "goal" | Plemma -> "lemma")
+        print_ident id
+        print_fmla fmla
+
+let print_decl_or_use fmt = function
+  | Decl d -> print_decl fmt 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 
+    (print_list newline print_decl_or_use) t.th_decls

src/pretty.mli

@@ -20,6 +20,7 @@
 open Format
 open Ty
 open Term
+open Theory
 
 val print_ty : formatter -> ty -> unit
 
@@ -27,3 +28,8 @@ val print_term : formatter -> term -> unit
 
 val print_fmla : formatter -> fmla -> unit
 
+val print_decl : formatter -> decl -> unit
+
+val print_decl_or_use : formatter -> decl_or_use -> unit
+
+val print_theory : formatter -> theory -> unit

src/transform/transform.ml

@@ -19,7 +19,7 @@
 
 (* This module has the invariant that each type has only one tag function *)
 
-type 'a hashconsedlist = (int * 'a) list
+type 'a hashconsedlist = (int * 'a list) list
 
 
 module type Sig =
@@ -39,33 +39,40 @@ struct
         | [], [] -> true
         | [], _ | _, [] -> false
             (* work evenif al and bl are nil *)
-        | (_,ae)::al,(_,be)::bl -> X.tag ae = X.tag be && al == bl
+        | (_,ae::_)::al,(_,be::_)::bl -> X.tag ae = X.tag be && al == bl
+        | (_,[])::_,_ | _,(_,[])::_ ->  assert false 
     let hash a = 
       match a with
         | [] -> 0
-        | (_,ae)::[] -> X.tag ae
-        | (_,ae)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
+        | (_,[ae])::[] -> X.tag ae
+        | _::[] -> assert false
+        | (_,ae::_)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
+        | (_,[])::_ ->  assert false 
     let tag t = function
       | [] -> []
-      | (_,ae)::al -> (t,ae)::al
+      | (_,lae)::al -> (t,lae)::al
   end
   module LH = Hashcons.Make(L)
     
   type t = L.t
 
   let empty : t = []
-  let cons e l : t = LH.hashcons ((0,e)::l)
+  let cons e l : t = match l with
+    | [] -> LH.hashcons ([0,[e]])
+    | (_,l2)::_ -> LH.hashcons ((0,e::l2)::l)
 
-  let to_list : t -> X.t list =
-    let rec aux acc t =
-      match t with
-        | [] -> acc
-        | (_,e)::t -> aux (e::acc) t
-    in
-    aux []
+  let to_list t : X.t list = match t with
+    | [] -> []
+    | (_,l)::_ -> l
       
   let from_list = List.fold_left (fun t e -> cons e t) empty        
 
+  let fold_left f acc l =
+    List.fold_left (fun acc l -> match l with
+                      | [] -> acc
+                      | (tag,ae::_)::_ -> f acc tag ae
+                      | (_,[])::_ -> assert false) acc l
+
   let tag = function
     | [] -> -1
     | (t,_)::_ -> t
@@ -77,19 +84,17 @@ end
 type ('a,'b) t = { all : 'a hashconsedlist -> 'b hashconsedlist;
                    clear : unit -> unit;
                    from_list : 'a list -> 'a hashconsedlist;
-                   to_list : 'b hashconsedlist -> 'b list;
-                   clear_to_list : unit -> unit}
+                   to_list : 'b hashconsedlist -> 'b list}
 
 
 let compose f g = {all = (fun x -> g.all (f.all x));
                    clear = (fun () -> f.clear (); g.clear ());
                    from_list = f.from_list;
-                   to_list = g.to_list;
-                   clear_to_list = g.clear_to_list}
+                   to_list = g.to_list}
 
 let apply f x = f.to_list (f.all (f.from_list x))
     
-let clear f = f.clear ();f.clear_to_list ()
+let clear f = f.clear ()
 
 let memo f tag h x =
   try Hashtbl.find h (tag x:int)
@@ -126,8 +131,7 @@ struct
     {all = all;
      clear = clear;
      from_list = LH1.from_list;
-     to_list = memo_to_list2 h_to_list;
-     clear_to_list = (fun () -> Hashtbl.clear h_to_list)
+     to_list = memo_to_list2 h_to_list
     } 
 
   let fold_map_left f_fold v_empty =
@@ -143,7 +147,8 @@ struct
     let rec f acc t1 = 
       match t1 with
         | [] -> rewind (LH2.empty,v_empty) acc
-        | (tag,e)::t2 -> 
+        | (_,[])::_ -> assert false
+        | (tag,e::_)::t2 -> 
             try 
               let edonev = Hashtbl.find memo_t tag in
               rewind edonev acc
@@ -161,7 +166,8 @@ struct
     let rec f (acc,v) t = 
       match t with
         | [] -> List.fold_left (List.fold_left (fun t e -> LH2.cons e t)) LH2.empty acc
-        | (_,e)::t -> 
+        | (_,[])::_ ->  assert false 
+        | (_,e::_)::t -> 
             let v,res = f_fold v e in
             f (res::acc,v) t in
     let memo_t = Hashtbl.create 16 in