(*
-* Copyright 2005-2008, 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,
extra_counter := !extra_counter + 1;
"__extra_counter__"^(string_of_int ctr)
-let read_fresh_id () =
+let get_seeded seed =
+ let ctr = !extra_counter in
+ extra_counter := !extra_counter + 1;
+ seed^(string_of_int ctr)
+
+let read_fresh_id _ =
try
let s = read_line () in
- match Parse_c.tokens_string s with
+ match Parse_c.tokens_of_string s with
[Parser_c.TIdent _; Parser_c.EOF _] -> s
+ | [Parser_c.EOF _] -> get_extra()
| _ -> failwith ("wrong fresh id: " ^ s)
with End_of_file -> get_extra()
let new_triples = List.rev new_triples in
let fresh_env =
List.map
- (function ((r,n) as fresh) ->
- Printf.printf "%s: name for %s: " r n; (* not debugging code!!! *)
- flush stdout;
- (fresh,string2val(read_fresh_id())))
+ (function
+ ((r,n) as fresh,Ast.NoVal) ->
+ Printf.printf "%s: name for %s: " r n; (* not debugging code!!! *)
+ flush stdout;
+ (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)) ->
- if List.mem fresh freshs
- then (freshs,(node,elem::env,pred))
- else (freshs,cur))
+ try
+ let _ = List.assoc fresh freshs in
+ (freshs,(node,(fresh,fn env)::env,pred))
+ with Not_found -> (freshs,cur))
freshs_node_env_preds)
(List.combine local_freshs new_triples)
fresh_env) in
(* ----------------------------------------------------------------------- *)
(* Create the environment to be used afterwards *)
+(* 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 *)
-let collect_used_after used_after envs =
- List.map (List.filter (function (v,vl) -> List.mem v used_after)) envs
+let numberify trees =
+ let trees =
+ Common.fold_left_with_index
+ (function acc -> function xs -> function n ->
+ (List.map (function x -> (n,x)) xs) @ acc)
+ [] trees in
+ List.fold_left
+ (function res ->
+ function (n,x) ->
+ let (same,diff) = List.partition (function (ns,xs) -> x = xs) res in
+ match same with
+ [(ns,xs)] -> (n::ns,xs)::diff
+ | _ -> ([n],x)::res)
+ [] trees
(* ----------------------------------------------------------------------- *)
(* entry point *)
let process used_after inherited_env l =
- extra_counter := 0;
let (trees, fresh_envs) =
List.split (List.map (process_tree inherited_env) l) in
- (Common.uniq(List.concat trees), collect_used_after used_after fresh_envs)
+ let trees = numberify trees in
+ (trees, collect_used_after used_after fresh_envs l inherited_env)
HCoop / bpt / coccinelle.git / blobdiff