rationnalisation de transform.ml

src/core/transform.ml

@@ -31,7 +31,7 @@ let compose f g = {all = (fun x -> g.all (f.all x));
                    clear = (fun () -> f.clear (); g.clear ());
                   }
 
-let translation f c = {all = (fun x -> c (f.all x));
+let conv f c = {all = (fun x -> c (f.all x));
                        clear = f.clear}
 
 let apply f x = f.all x
@@ -75,66 +75,55 @@ let fold_up ?clear f_fold v_empty =
   t (f []) clear (fun () -> Hashtbl.clear memo_t)
 
 
-let fold_map_up ?clear f_fold v_empty =
-  let v_empty = v_empty,empty_context in
-  let f_fold ctxt (env,ctxt2) decl = f_fold ctxt env ctxt2 decl in
-  translation (fold_up ?clear f_fold v_empty) snd
-
-let elt ?clear f_elt =
-  let memo_elt = Hashtbl.create 64 in
-  let f_elt _ () ctx x = (),
-    List.fold_left add_decl ctx (memo f_elt d_tag memo_elt x) in
-  let f = fold_map_up ?clear f_elt () in
-  {f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
-
-let fold_bottom ?tag ?clear f_fold v_empty =
-  let tag_clear,tag_memo = match tag with
-    | None -> (fun () -> ()), (fun f v ctxt -> f v ctxt)
-    | Some tag_env ->
-        let memo_t = Hashtbl.create 64 in
-        (fun () -> Hashtbl.clear memo_t),(fun f v ctxt ->
-           try
-             Hashtbl.find memo_t (ctxt.ctxt_tag,(tag_env v : int))
-           with Not_found ->
-             let r = f v ctxt in
-             Hashtbl.add memo_t (ctxt.ctxt_tag,tag_env v) r;
-             r
-        ) in
-  let rec f v ctxt =
-    match ctxt.ctxt_decls with
-      | None -> v
-      | Some(d,ctxt2) ->
-          let v = f_fold ctxt v d in
-          tag_memo f v ctxt2 in
-  let memo_t = Hashtbl.create 16 in
-  t (memo (f v_empty) ctxt_tag memo_t) clear (fun () -> tag_clear ();Hashtbl.clear memo_t)
-
-
-let fold_map_bottom ?tag ?clear f_fold v_empty =
-  let rewind ldone ctxt =
-    List.fold_left (List.fold_left add_decl) ctxt ldone in
+let fold_bottom_up ?tag ?clear ~top ~down f_fold v_empty =
+  let rewind ldone env_down =
+    List.fold_left down env_down ldone in
   let tag_clear,tag_memo = match tag with
     | None -> (fun () -> ()), (fun f ldone v ctxt -> f ldone v ctxt)
     | Some tag_env ->
         let memo_t = Hashtbl.create 64 in
         (fun () -> Hashtbl.clear memo_t),(fun f ldone v ctxt ->
            try
-             let ctxt = Hashtbl.find memo_t (ctxt.ctxt_tag,tag_env v) in
-             rewind ldone ctxt
+             let env_down = Hashtbl.find memo_t (ctxt.ctxt_tag,tag_env v) in
+             rewind ldone env_down
            with Not_found ->
-             let r = f ldone v ctxt in
-             Hashtbl.add memo_t (ctxt.ctxt_tag,tag_env v) r;
-             r
+             let env_down = f ldone v ctxt in
+             Hashtbl.add memo_t (ctxt.ctxt_tag,tag_env v) env_down;
+             env_down
         ) in
   let rec f ldone v ctxt =
     match ctxt.ctxt_decls with
-      | None -> rewind ldone ctxt
+      | None -> rewind ldone (top v)
       | Some(d,ctxt2) ->
           let v,res = f_fold ctxt v d in
           tag_memo f (res::ldone) v ctxt2 in
   let memo_t = Hashtbl.create 16 in
   t (memo (f [] v_empty) ctxt_tag memo_t) clear (fun () -> tag_clear ();Hashtbl.clear memo_t)
 
+let fold_bottom ?tag ?clear f_fold v_empty =
+  let top x = x in
+  let down x () = x in
+  let f_fold ctxt env d = f_fold ctxt env d, () in
+  fold_bottom_up ?tag ?clear ~top ~down f_fold v_empty
+
+let fold_map_up ?clear f_fold v_empty =
+  let v_empty = v_empty,empty_context in
+  let f_fold ctxt (env,ctxt2) decl = f_fold ctxt env ctxt2 decl in
+  conv (fold_up ?clear f_fold v_empty) snd
+
+let elt ?clear f_elt = 
+  let memo_elt = Hashtbl.create 64 in
+  let f_elt _ () ctx x = (),
+    List.fold_left add_decl ctx (memo f_elt d_tag memo_elt x) in
+  let f = fold_map_up ?clear f_elt () in
+  {f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
+
+
+let fold_map_bottom ?tag ?clear f_fold v_empty =
+  let top _ = empty_context in
+  let down = (List.fold_left add_decl) in
+  fold_bottom_up ?tag ?clear ~top ~down f_fold v_empty
+    
 let all ?clear f =
   let memo_t = Hashtbl.create 16 in
   t (memo f ctxt_tag memo_t) clear (fun () -> Hashtbl.clear memo_t)
@@ -148,11 +137,11 @@ let all ?clear f =
   | Ouse   of theory
   | Oclone of (ident * ident) list*)
 
-let elt_of_oelt ~ty ~logic ~ind ~prop ~use ~clone d =
+let elt_of_oelt ~ty ~logic ~ind ~prop ~use ~clone d = 
   match d.d_node with
     | Dtype l -> [create_ty_decl (List.map ty l)]
     | Dlogic l -> [create_logic_decl (List.map logic l)]
-    | Dind l -> [create_ind_decl (List.map ind l)]
+    | Dind l -> ind l 
     | Dprop p -> prop p
     | Duse th -> use th
     | Dclone c -> clone c
@@ -160,4 +149,22 @@ let elt_of_oelt ~ty ~logic ~ind ~prop ~use ~clone d =
 let fold_context_of_decl f ctxt env ctxt_done d =
   let env,decls = f ctxt env d in
   env,List.fold_left add_decl ctxt_done decls
-
+  
+let split_goals =
+  let f _ (ctxt,l) decl = 
+    match decl.d_node with
+      | Dprop (Pgoal,_) -> (ctxt,(add_decl ctxt decl)::l)
+      | _ -> (add_decl ctxt decl,l) in
+  let g = fold_up f (empty_context,[]) in
+  conv g snd
+
+let extract_goals =
+  let f _ (ctxt,l) decl = 
+    match decl.d_node with
+      | Dprop (Pgoal,f) -> (ctxt,(f.pr_name,f.pr_fmla,ctxt)::l)
+      | _ -> (add_decl ctxt decl,l) in
+  let g = fold_up f (empty_context,[]) in
+  conv g snd
+
+
+let unit_tag () = 0

src/core/transform.mli

@@ -22,8 +22,10 @@ open Theory
 
 (* Tranformation on context with some memoisations *)
 
+(** General functions *)
+
 (* The type of transformation from list of 'a to list of 'b *)
-type 'a  t
+type 'a t
 
 (* compose two transformations, the underlying datastructures for
    the memoisation are shared *)
@@ -32,9 +34,34 @@ val compose : context t -> 'a t -> 'a t
 (* apply a transformation and memoise *)
 val apply : 'a t -> context -> 'a
 
+(* convert the result of a transformation witout memoisation *)
+val conv : 'a t -> ('a -> 'b) -> 'b t
+
 (* clear the datastructures used to store the memoisation *)
 val clear : 'a t -> unit
 
+(** General constructors *)
+val fold_up :
+  ?clear:(unit -> unit) ->
+  (context -> 'a -> decl -> 'a) -> 'a -> 'a t
+
+
+val fold_bottom :
+  ?tag:('a -> int) ->
+  ?clear:(unit -> unit) ->
+  (context -> 'a  -> decl -> 'a) -> 'a -> 'a t
+
+
+val fold_bottom_up :
+  ?tag:('a -> int) ->
+  ?clear:(unit -> unit) ->
+  top:('a -> 'c) ->
+  down:('c -> 'b -> 'c) ->
+  (context -> 'a  -> decl -> 'a * 'b) -> 'a -> 'c t
+
+
+
+
 (* the general tranformation only one memoisation is performed at the
    beginning *)
 val all :
@@ -62,17 +89,6 @@ val elt :
   (decl -> decl list) -> context t
 
 
-val fold_bottom :
-  ?tag:('a -> int) ->
-  ?clear:(unit -> unit) ->
-  (context -> 'a  -> decl -> 'a) -> 'a -> 'a t
-
-
-val fold_up :
-  ?clear:(unit -> unit) ->
-  (context -> 'a -> decl -> 'a) -> 'a -> 'a t
-
-
 
 (*type odecl =
   | Otype of ty_decl
@@ -84,7 +100,7 @@ val fold_up :
 val elt_of_oelt :
   ty:(ty_decl -> ty_decl) ->
   logic:(logic_decl -> logic_decl) ->
-  ind:(ind_decl -> ind_decl) ->
+  ind:(ind_decl list -> decl list) ->
   prop:(prop_decl -> decl list) ->
   use:(theory -> decl list) ->
   clone:((ident * ident) list -> decl list) ->
@@ -95,3 +111,9 @@ val fold_context_of_decl:
   (context -> 'a -> decl -> 'a * decl list) ->
   context -> 'a -> context -> decl -> ('a * context)
 
+(* Utils *)
+val unit_tag : unit -> int
+
+val split_goals : context list t
+
+val extract_goals : (Ident.ident * Term.fmla * context) list t

src/main.ml

@@ -74,38 +74,27 @@ let type_file env file =
   close_in c;
   if !parse_only then env else Typing.add_theories env f
 
-let extract_goals th =
-  let ctx = Context.use_export Context.empty_context th in
-  assert false
+let extract_goals ctxt =
+  Transform.apply Transform.extract_goals ctxt
 
 let transform l =
-  let l = Typing.list_theory l in
-  if !print_stdout && not transform then 
-    List.iter (Why3.print_theory Format.std_formatter) l
+  let l = List.map (fun t -> t,t.th_ctxt) (Typing.list_theory l) in
+  let l = if !simplify_recursive 
+  then 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,dl) -> t,Transform.apply Inlining.all dl) l
+  else l in
+  if !print_stdout then 
+    List.iter (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
   else if !alt_ergo then match l with
-    | th :: _ -> begin match extract_goals th with
+    | (_,ctxt) :: _ -> begin match extract_goals ctxt with
 	| g :: _ -> Alt_ergo.print_goal std_formatter g
 	| [] -> ()
       end	
     | [] -> ()
-  else if transform then
-    let l = List.map (fun t -> t,Transform.apply Flatten.t t.th_ctxt)
-      l in
-    let l = if !simplify_recursive 
-    then 
-      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,dl) -> t,Transform.apply Inlining.all dl) l
-    else l in
-    if !print_stdout then 
-      List.iter (fun (t,dl) ->
-                   Format.printf "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n@?" 
-                     Pretty.print_ident t.th_name 
-                     Pretty.print_context dl
-                ) l
+
 	
 
 let () =

src/output/why3.ml

@@ -320,7 +320,8 @@ let print_decl_list fmt dl =
 let print_context fmt ctxt =
   print_list newline2 print_decl fmt (Context.get_decls ctxt)
 
-let print_theory fmt t =
+let print_context_th fmt name ctxt =
   fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@\n@."
-    print_id t.th_name print_context t.th_ctxt
+    print_id name print_context ctxt
 
+let print_theory fmt t = print_context_th fmt t.th_name t.th_ctxt

src/output/why3.mli

@@ -30,5 +30,6 @@ val print_fmla : formatter -> fmla -> unit
 val print_decl : formatter -> decl -> unit
 val print_decl_list : formatter -> decl list -> unit
 val print_context : formatter -> context -> unit
+val print_context_th : formatter -> ident -> context -> unit
 val print_theory : formatter -> theory -> unit