Ignore:
Timestamp:
12/04/08 18:41:26 (6 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/typechecker/alpha.ml

    r16132 r16147  
    6060        get_fresh_name n (String_set.singleton n) 
    6161 
    62  
     62let add_symbols_bound sl = List.fold_left (fun a b ->  match b with  
     63        S_Symbol(S_Sym_Ident x) -> String_set.union a (String_set.singleton x) 
     64        | _ -> raise (Invalid_argument "add_symbols_bound: got a non-string in identifier list for quantifier")) String_set.empty sl 
    6365 
    6466 
     
    7779 
    7880let list_union list = List.fold_left String_set.union String_set.empty list 
     81 
     82let rec bound_spass c = match c with 
     83        S_Term(_, sl, st) -> String_set.union (bound_spass st) (add_symbols_bound sl) 
     84        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (bound_spass b)) String_set.empty sl 
     85        | S_Symbol(S_Sym_Ident s) -> if (String.compare s "ok") = 0 then 
     86                String_set.singleton s else String_set.empty 
     87        | S_Symbol _ -> String_set.empty 
    7988 
    8089let rec free_spass c = match c with 
Note: See TracChangeset for help on using the changeset viewer.