Changeset 16309


Ignore:
Timestamp:
12/11/08 20:51:59 (5 years ago)
Author:
hritcu
Message:

Fixed bug in replace_stmt_in_formula

Location:
src/typechecker
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/typechecker/replace.ml

    r16270 r16309  
    154154        match c with 
    155155        S_Term(qs, tl, t) -> 
    156                 let bound = String_set.elements (free_spass c) in 
    157                 if List.exists (create_pred x) bound then c 
     156                let bound = bound_spass c in 
     157                if String_set.mem x bound then c 
    158158                else 
    159159                        let i = intersection (List.flatten (List.map (get_names_spass) tl)) free in 
     
    182182let replace_stmt_in_formula x s c = let free = String_set.elements (free_stmt s) in replace_stmt_in_formula' x s free c 
    183183 
    184 let replace_formula x m c = replace_stmt_in_formula x (term_to_stmt m) c 
     184let 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 
    185187 
    186188let rec replace_stmt_in_type' x s free t =  
  • src/typechecker/typeprocess.ml

    r16304 r16309  
    6767 
    6868let 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 
    8070        ver_result_type' l yts c' 
    8171 
Note: See TracChangeset for help on using the changeset viewer.