Changeset 16147 for src/typechecker/alpha.ml

Timestamp:

12/04/08 18:41:26 (4 years ago)

Author:

broeni

Message:

think I fixed replace and added a bound_spass function to alpha that has the functionality of the old free_spass function, but just the bound part

File:

• src/typechecker/alpha.ml (modified) (2 diffs)

src/typechecker/alpha.ml

@@ -60 +60 @@
         get_fresh_name n (String_set.singleton n)
 
-
+let add_symbols_bound sl = List.fold_left (fun a b ->  match b with 
+        S_Symbol(S_Sym_Ident x) -> String_set.union a (String_set.singleton x)
+        | _ -> raise (Invalid_argument "add_symbols_bound: got a non-string in identifier list for quantifier")) String_set.empty sl
 
 
@@ -77 +79 @@
 
 let list_union list = List.fold_left String_set.union String_set.empty list
+
+let rec bound_spass c = match c with
+        S_Term(_, sl, st) -> String_set.union (bound_spass st) (add_symbols_bound sl)
+        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (bound_spass b)) String_set.empty sl
+        | S_Symbol(S_Sym_Ident s) -> if (String.compare s "ok") = 0 then
+                String_set.singleton s else String_set.empty
+        | S_Symbol _ -> String_set.empty
 
 let rec free_spass c = match c with