Release coccinelle-0.2.0

[bpt/coccinelle.git] / engine / postprocess_transinfo.ml

diff --git a/engine/postprocess_transinfo.ml b/engine/postprocess_transinfo.ml
index 1a66f31..fa41cd3 100644 (file)
--- a/engine/postprocess_transinfo.ml
+++ b/engine/postprocess_transinfo.ml
@@ -1,23 +1,23 @@
 (*
-* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
-* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
-* This file is part of Coccinelle.
-* 
-* Coccinelle is free software: you can redistribute it and/or modify
-* it under the terms of the GNU General Public License as published by
-* the Free Software Foundation, according to version 2 of the License.
-* 
-* Coccinelle is distributed in the hope that it will be useful,
-* but WITHOUT ANY WARRANTY; without even the implied warranty of
-* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-* GNU General Public License for more details.
-* 
-* You should have received a copy of the GNU General Public License
-* along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
-* 
-* The authors reserve the right to distribute this or future versions of
-* Coccinelle under other licenses.
-*)
+ * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
+ * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
+ * This file is part of Coccinelle.
+ *
+ * Coccinelle is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, according to version 2 of the License.
+ *
+ * Coccinelle is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
+ *
+ * The authors reserve the right to distribute this or future versions of
+ * Coccinelle under other licenses.
+ *)
 
 
 (* two goals: first drop from the environments things that are not used,
@@ -76,23 +76,40 @@ let process_tree inherited_env l =
   let fresh_env =
     List.map
       (function
-         ((r,n) as fresh,None) ->
+         ((r,n) as fresh,Ast.NoVal) ->
            Printf.printf "%s: name for %s: " r n; (* not debugging code!!! *)
            flush stdout;
-           (fresh,string2val(read_fresh_id()))
-       | ((r,n) as fresh,Some seed) ->
-           (fresh,string2val(get_seeded seed)))
+           (fresh,let v = string2val(read_fresh_id()) in function _ -> v)
+       | ((r,n) as fresh,Ast.StringSeed seed) ->
+           (fresh,let v = string2val(get_seeded seed) in function _ -> v)
+       | ((r,n) as fresh,Ast.ListSeed seed) ->
+           (fresh,
+            function env ->
+              let strings =
+                List.map
+                  (function
+                      Ast.SeedString s -> s
+                    | Ast.SeedId id ->
+                        try
+                          (match List.assoc id env with
+                            Lib_engine.NormalMetaVal(Ast_c.MetaIdVal(str)) ->
+                              str
+                          | _ -> failwith "bad id value")
+                        with
+                          Not_found -> failwith "fresh: no binding for meta")
+                  seed in
+           string2val(String.concat "" strings)))
       all_fresh in
   let (_,res) =
     List.split
       (List.fold_left
         (function freshs_node_env_preds ->
-          function (fresh,_) as elem ->
+          function (fresh,fn) ->
             List.map
               (function (freshs,((node,env,pred) as cur)) ->
                 try
                   let _ = List.assoc fresh freshs in
-                  (freshs,(node,elem::env,pred))
+                  (freshs,(node,(fresh,fn env)::env,pred))
                 with Not_found -> (freshs,cur))
               freshs_node_env_preds)
         (List.combine local_freshs new_triples)
@@ -101,9 +118,25 @@ let process_tree inherited_env l =
 
 (* ----------------------------------------------------------------------- *)
 (* Create the environment to be used afterwards *)
-
-let collect_used_after used_after envs =
-  List.map (List.filter (function (v,vl) -> List.mem v used_after)) envs
+(* anything that a used after fresh variable refers to has to have a unique
+value, by virtue of the placement of the quantifier.  thus we augment
+inherited env with the first element of l, if any *)
+
+let collect_used_after used_after envs l inherited_env =
+  List.map2
+    (function env -> function l ->
+      let inherited_env =
+       match l with
+         [] -> inherited_env
+       | (_,fse,_)::_ ->
+           (* l represents the result from a single tree. fse is a complete
+              environment in that tree.  for a fresh seed, the environments
+              for all leaves contain the same information *)
+           fse@inherited_env  in
+      List.map
+       (function (v,vl) -> (v,vl inherited_env))
+       (List.filter (function (v,vl) -> List.mem v used_after) env))
+    envs l
 
 (* ----------------------------------------------------------------------- *)
 (* distinguish between distinct witness trees, each gets an index n *)
@@ -130,4 +163,4 @@ let process used_after inherited_env l =
   let (trees, fresh_envs) =
     List.split (List.map (process_tree inherited_env) l) in
   let trees = numberify trees in
-  (trees, collect_used_after used_after fresh_envs)
+  (trees, collect_used_after used_after fresh_envs l inherited_env)