Changeset 16309
 Timestamp:
 12/11/08 20:51:59 (7 years ago)
 Location:
 src/typechecker
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/typechecker/replace.ml
r16270 r16309 154 154 match c with 155 155 S_Term(qs, tl, t) > 156 let bound = String_set.elements (free_spass c)in157 if List.exists (create_pred x)bound then c156 let bound = bound_spass c in 157 if String_set.mem x bound then c 158 158 else 159 159 let i = intersection (List.flatten (List.map (get_names_spass) tl)) free in … … 182 182 let replace_stmt_in_formula x s c = let free = String_set.elements (free_stmt s) in replace_stmt_in_formula' x s free c 183 183 184 let replace_formula x m c = replace_stmt_in_formula x (term_to_stmt m) c 184 let replace_formula x m c = 185 Logmanager.log (Printf.sprintf "replace_formula %s $m $T\n" x) ~terms:[m] ~sterms:[c] ~loglevel:3; 186 replace_stmt_in_formula x (term_to_stmt m) c 185 187 186 188 let rec replace_stmt_in_type' x s free t = 
src/typechecker/typeprocess.ml
r16304 r16309 67 67 68 68 let ver_result_type l n_list yts c = 69 let c' = try List.fold_left2 (fun cc n (y,_) > replace_formula y n cc) c n_list (sub_list yts 0 l) with Invalid_argument x > ( 70 Printf.printf "error is %s\n" x; 71 Printf.printf "term list has length %d\n" (List.length n_list); 72 Printf.printf "yts list has length %d\n" (List.length yts); 73 Printf.printf "termlist: "; 74 List.iter (fun a > print_term a; Printf.printf ", ") n_list; 75 Printf.printf "\nyt list is: "; 76 List.iter (fun (a, _) > Printf.printf "%s, " a) yts; 77 Printf.printf "\n"; 78 raise (Invalid_argument "typeprocess: ver_result_type list.fold_left2")) 79 in 69 let c' = List.fold_left2 (fun cc n (y,_) > replace_formula y n cc) c n_list (sub_list yts 0 l) in 80 70 ver_result_type' l yts c' 81 71
Note: See TracChangeset
for help on using the changeset viewer.