alt-ergo.ml : decl_type avec arguments

main.ml : possibilité de mettre specifier plusieurs theories ou buts
split_goals : ajout d'un argument supplémentaire pour ne selectionner que certains buts.

src/main.ml

@@ -32,7 +32,7 @@ type which_goals =
   | Gall
   | Gtheory of string
   | Ggoal of string
-let which_goals = ref Gall
+let which_goals = ref []
 let timeout = ref 10
 let call = ref false
 let output = ref None
@@ -47,11 +47,11 @@ let () =
      "--debug", Arg.Set debug, "sets the debug flag";
      "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
      "<dir>  adds dir to the loadpath";
-     "--all_goals", Arg.Unit (fun () -> which_goals := Gall), 
+     "--all_goals", Arg.Unit (fun () -> which_goals := Gall::!which_goals), 
      "apply on all the goals of the file";
-     "--goals_of", Arg.String (fun s -> which_goals := Gtheory s), 
+     "--goals_of", Arg.String (fun s -> which_goals := Gtheory s::!which_goals), 
      "apply on all the goals of the theory given (ex. --goal T)";
-     "--goal", Arg.String (fun s -> which_goals := Ggoal s), 
+     "--goal", Arg.String (fun s -> which_goals := Ggoal s::!which_goals), 
      "apply only on the goal given (ex. --goal T.g)";
      "--output", Arg.String (fun s -> output := Some s), 
      "choose to output each goals in the directory given.\
@@ -137,8 +137,8 @@ let transform env l =
 *)
 
 
-let extract_goals = 
-  let split_goals = Split_goals.t () in
+let extract_goals ?filter = 
+  let split_goals = Split_goals.t ?filter () in
   fun env drv acc th ->
     let ctxt = Context.use_export (Context.init_context env) th in
     let l = Transform.apply split_goals ctxt in
@@ -166,38 +166,39 @@ let do_file env drv filename_printer file =
           | None -> eprintf "a driver is needed@."; exit 1
           | Some drv -> drv in
       (* Extract the goal(s) *)
-      let goals = 
-        match !which_goals with
-          | Gall ->  Mnm.fold (fun _ th acc -> extract_goals env drv acc th) m []
-          | Gtheory s ->  
-              begin
-                try 
-                  extract_goals env drv [] (Mnm.find s m)
-                with Not_found -> 
-                  eprintf "File %s : --goals_of : Unknown theory %s@." file s; exit 1
-              end
-          | Ggoal s ->
-              let l = Str.split (Str.regexp "\\.") s in
-              let tname, l = 
-                match l with
-                  | [] | [_] -> 
-                      eprintf "--goal : Must be a qualified name (%s)@." s;
-                      exit 1
-                  | a::l -> a,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 th =try Mnm.find tname m with Not_found -> 
-                eprintf "File %s : --goal : Unknown theory %s@." file tname; exit 1 in
-              let pr = try fst (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 drv [] th in
-              List.filter (fun (_,ctxt) ->
-                             match ctxt.ctxt_decl.d_node with
-                               | Dprop (_,pr',_) -> pr == pr'
-                               | _ -> assert false) goals in
-      (* Apply transformations *)
+      let goals = List.fold_left 
+        (fun acc wg -> match wg with
+           | Gall ->  Mnm.fold (fun _ th acc -> extract_goals env drv acc th) m acc
+           | Gtheory s ->  
+               begin
+                 try 
+                     extract_goals env drv acc (Mnm.find s m)
+                 with Not_found -> 
+                   eprintf "File %s : --goals_of : Unknown theory %s@." file s; exit 1
+               end
+           | Ggoal s ->
+               let l = Str.split (Str.regexp "\\.") s in
+               let tname, l = 
+                 match l with
+                   | [] | [_] -> 
+                       eprintf "--goal : Must be a qualified name (%s)@." s;
+                       exit 1
+                   | a::l -> a,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 th =try Mnm.find tname m with Not_found -> 
+                 eprintf "File %s : --goal : Unknown theory %s@." file tname; exit 1 in
+               let pr = try fst (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 drv acc th in
+               List.filter (fun (_,ctxt) ->
+                              match ctxt.ctxt_decl.d_node with
+                                | Dprop (_,pr',_) -> pr == pr'
+                                | _ -> assert false) goals)
+      [] !which_goals in
+        (* Apply transformations *)
       let goals = List.fold_left 
         (fun acc (th,ctxt) -> 
            List.rev_append 

src/output/alt_ergo.ml

@@ -32,11 +32,14 @@ let ident_printer =
 let print_ident fmt id =
   fprintf fmt "%s" (id_unique ident_printer id)
 
+let print_tvsymbols fmt id =
+  fprintf fmt "'%s" (id_unique ident_printer (tv_name id))
+
 let forget_var v = forget_id ident_printer v.vs_name
 
 let rec print_type drv fmt ty = match ty.ty_node with
   | Tyvar id -> 
-      fprintf fmt "'%a" print_ident (tv_name id)
+      print_tvsymbols fmt id
   | Tyapp (ts, tl) -> 
       match Driver.query_ident drv ts.ts_name with
         | Driver.Remove -> assert false (* Mettre une erreur *)
@@ -141,7 +144,12 @@ let print_type_decl drv fmt = function
       begin
         match Driver.query_ident drv ts.ts_name with
           | Driver.Remove | Driver.Syntax _ -> false
-          | Driver.Tag _ -> fprintf fmt "type %a" print_ident ts.ts_name; true
+          | Driver.Tag _ -> 
+              match ts.ts_args with
+                | [] -> fprintf fmt "type %a" print_ident ts.ts_name; true
+                | _  -> fprintf fmt "type (%a)%a" 
+                    (print_list comma print_tvsymbols) ts.ts_args  
+                      print_ident ts.ts_name; true
       end
   | _, Talgebraic _ ->
       assert false

src/transform/split_goals.ml

@@ -16,19 +16,27 @@
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
 (*                                                                        *)
 (**************************************************************************)
+open Ident
 open Theory  
 open Context
 
-let t () =
-  let f ctxt0 (ctxt,l) =
+let t ?filter () =
+  let filter = match filter with
+    | None -> (fun _ -> true)
+    | Some s -> (fun id -> Sid.mem id s) in
+  let f ctxt0 ((ctxt,l) as ctxtl) =
     let decl = ctxt0.ctxt_decl in
     match decl.d_node with
-      | Dprop (Pgoal, _, _) -> (ctxt, add_decl ctxt decl :: l)
-      | Dprop (Plemma, pr, f) ->
+      | Dprop (Pgoal, pr, _) when filter (pr_name pr) -> (ctxt, add_decl ctxt decl :: l)
+      | Dprop (Pgoal, pr, _)  -> ctxtl
+      | Dprop (Plemma, pr, f) when filter (pr_name pr) ->
           let d1 = create_prop_decl Paxiom pr f in
           let d2 = create_prop_decl Pgoal  pr f in
           (add_decl ctxt d1,
            add_decl ctxt d2 :: l)
+      | Dprop (Plemma, pr, f) ->
+          let d1 = create_prop_decl Paxiom pr f in
+          (add_decl ctxt d1,l)
       | _ -> (add_decl ctxt decl, l) 
   in
   let g = Transform.fold f (fun env -> init_context env, []) in

src/transform/split_goals.mli

@@ -17,4 +17,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val t : unit -> Transform.ctxt_list_t
+val t : ?filter:Ident.Sid.t -> unit -> Transform.ctxt_list_t