Changeset 16309

Timestamp:

12/11/08 20:51:59 (5 years ago)

Author:

hritcu

Message:

Fixed bug in replace_stmt_in_formula

Location:

src/typechecker

Files:

• replace.ml (modified) (2 diffs)
• typeprocess.ml (modified) (1 diff)

src/typechecker/replace.ml

@@ -154 +154 @@
         match c with
         S_Term(qs, tl, t) ->
-                let bound = String_set.elements (free_spass c) in
-                if List.exists (create_pred x) bound then c
+                let bound = bound_spass c in
+                if String_set.mem x bound then c
                 else
                         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
 
-let replace_formula x m c = replace_stmt_in_formula x (term_to_stmt m) c
+let replace_formula x m c = 
+        Logmanager.log (Printf.sprintf "replace_formula %s $m $T\n" x) ~terms:[m] ~sterms:[c] ~loglevel:3;
+        replace_stmt_in_formula x (term_to_stmt m) c
 
 let rec replace_stmt_in_type' x s free t = 

src/typechecker/typeprocess.ml

@@ -67 +67 @@
 
 let ver_result_type l n_list yts c = 
-        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 -> (
-                Printf.printf "error is %s\n" x; 
-                Printf.printf "term list has length %d\n" (List.length n_list);
-                Printf.printf "yts list has length %d\n" (List.length yts); 
-                Printf.printf "termlist: ";
-                List.iter (fun a -> print_term a; Printf.printf ", ") n_list;
-                Printf.printf "\nyt list is: "; 
-                List.iter (fun (a, _) -> Printf.printf "%s, " a) yts; 
-                Printf.printf "\n";
-                raise (Invalid_argument "typeprocess: ver_result_type list.fold_left2"))
-        in
+        let c' = List.fold_left2 (fun cc n (y,_) -> replace_formula y n cc) c n_list (sub_list yts 0 l) in
         ver_result_type' l yts c'