Suppression des separateurs inutiles; driver pour alt_ergo complet pour Int

lib/drivers/alt_ergo.drv

@@ -37,8 +37,15 @@ theory prelude.Int
   syntax logic (_>=_) "(%1 >= %2)"
   syntax logic (_> _) "(%1 >  %2)"
 
-  remove prop Mul_comm
   remove prop One_neutral
+  remove prop Add_assoc
+  remove prop Add_comm
+  remove prop Zero_neutral
+  remove prop Neg
+  remove prop Mul_comm
+  remove prop Mul_assoc
+  remove prop Mul_distr
+
 end
 
 theory algebra.AC

src/output/alt_ergo.ml

@@ -139,9 +139,8 @@ let print_type_decl drv fmt = function
   | ts, Tabstract ->
       begin
         match Driver.query_ident drv ts.ts_name with
-          | Driver.Remove -> ()
-          | Driver.Syntax _ -> ()
-          | Driver.Tag s -> fprintf fmt "type %a" print_ident ts.ts_name
+          | Driver.Remove | Driver.Syntax _ -> false
+          | Driver.Tag _ -> fprintf fmt "type %a" print_ident ts.ts_name; true
       end
   | _, Talgebraic _ ->
       assert false
@@ -152,8 +151,7 @@ let print_logic_decl drv ctxt fmt = function
   | Lfunction (ls, None) ->
       begin
         match Driver.query_ident drv ls.ls_name with
-          | Driver.Remove -> ()
-          | Driver.Syntax _ -> ()
+          | Driver.Remove | Driver.Syntax _ -> false
           | Driver.Tag s -> 
               let sac = if Snm.mem "AC" s then "ac " else "" in
               let tyl = ls.ls_args in
@@ -161,7 +159,8 @@ let print_logic_decl drv ctxt fmt = function
               fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
                 sac
                 print_ident ls.ls_name
-	        (print_list comma (print_type drv)) tyl (print_type drv) ty
+	        (print_list comma (print_type drv)) tyl (print_type drv) ty;
+              true
       end
   | Lfunction (ls, Some defn) ->
       let id = ls.ls_name in
@@ -169,45 +168,45 @@ let print_logic_decl drv ctxt fmt = function
       let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
       fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
         (print_list comma (print_logic_binder drv)) vl (print_type drv) ty (print_term drv) t;
-      List.iter forget_var vl
+      List.iter forget_var vl;true
   | Lpredicate (ls, None) ->
       begin
         match Driver.query_ident drv ls.ls_name with
-          | Driver.Remove -> ()
-          | Driver.Syntax _ -> ()
+          | Driver.Remove | Driver.Syntax _ -> false
           | Driver.Tag s -> 
               let sac = if Snm.mem "AC" s then "ac " else "" in
               fprintf fmt "@[<hov 2>logic %s%a : %a -> prop@]" sac
-	        print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args
+	        print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args;
+              true
       end
   | Lpredicate (ls, Some fd) ->
       let _,vl,f = open_ps_defn fd in
       fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
 	print_ident ls.ls_name 
-        (print_list comma (print_logic_binder drv)) vl (print_fmla drv) f
+        (print_list comma (print_logic_binder drv)) vl (print_fmla drv) f;
+      true
 
 let print_decl drv ctxt fmt d = match d.d_node with
   | Dtype dl ->
-      print_list newline (print_type_decl drv) fmt dl
+      print_list_opt newline (print_type_decl drv) fmt dl
   | Dlogic dl ->
-      print_list newline (print_logic_decl drv ctxt) fmt dl
+      print_list_opt newline (print_logic_decl drv ctxt) fmt dl
   | Dind _ -> assert false (* TODO *)
   | Dprop (Paxiom, pr) when
-      Driver.query_ident drv pr.pr_name = Driver.Remove -> ()
+      Driver.query_ident drv pr.pr_name = Driver.Remove -> false
   | Dprop (Paxiom, pr) ->
       fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" 
-        print_ident pr.pr_name (print_fmla drv) pr.pr_fmla
+        print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true
   | Dprop (Pgoal, pr) ->
       fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
-        print_ident pr.pr_name (print_fmla drv) pr.pr_fmla
+        print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true
   | Dprop (Plemma, _) ->
       assert false
-  | Duse _ | Dclone _ ->
-      ()
+  | Duse _ | Dclone _ -> false
 
 let print_context drv fmt ctxt = 
   let decls = Context.get_decls ctxt in
-  print_list newline2 (print_decl drv ctxt) fmt decls
+  ignore (print_list_opt newline2 (print_decl drv ctxt) fmt decls)
 
 let () = Driver.register_printer "alt-ergo" print_context
 

src/output/driver.ml

@@ -28,9 +28,6 @@ open Ident
 
 (* From global_substitute of str *)
 open Str
-let string_after s n fmt = pp_print_string fmt
-  (String.sub s n (String.length s - n))
-
 let opt_search_forward re s pos =
   try Some(search_forward re s pos) with Not_found -> None
 
@@ -38,11 +35,11 @@ let global_substitute expr repl_fun text fmt =
   let rec replace start last_was_empty =
     let startpos = if last_was_empty then start + 1 else start in
     if startpos > String.length text then
-      string_after text start fmt
+      pp_print_string fmt (string_after text start)
     else
       match opt_search_forward expr text startpos with
       | None ->
-          string_after text start fmt
+          pp_print_string fmt (string_after text start)
       | Some pos ->
           let end_pos = match_end() in
           pp_print_string fmt (String.sub text start (pos-start));

src/util/pp.ml

@@ -125,3 +125,13 @@ let print_in_file ?(margin=78) p f =
   close_out cout
 
 
+
+(* With optional separation *)
+let rec print_list_opt sep print fmt = function
+  | [] -> false
+  | [x] -> print fmt x
+  | x :: r -> 
+      let notempty1 = print fmt x in
+      if notempty1 then sep fmt ();
+      let notempty2 = print_list_opt sep print fmt r in
+      notempty1 || notempty2

src/util/pp.mli

@@ -93,3 +93,8 @@ val open_file_and_formatter : ?margin:int -> string -> out_channel * formatter
 val close_file_and_formatter : out_channel * formatter -> unit
 val print_in_file_no_close : ?margin:int -> (Format.formatter -> unit) -> string -> out_channel
 val print_in_file : ?margin:int -> (Format.formatter -> unit) -> string -> unit
+
+
+val print_list_opt : 
+  (formatter -> unit -> unit) -> 
+  (formatter -> 'a -> bool) -> formatter -> 'a list -> bool