Changeset 16322


Ignore:
Timestamp:
12/12/08 11:39:57 (6 years ago)
Author:
broeni
Message:

changed form creation to create ftrue instead of S_True, adde special checks for zeroary ftrue in free, bound and when cfy'ing

Location:
src/typechecker
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/typechecker/alpha.ml

    r16308 r16322  
    7979        S_Term(_, sl, st) -> String_set.union (bound_spass st) (slist2set sl) 
    8080        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (bound_spass b)) String_set.empty sl 
    81         | S_Symbol(S_Sym_Ident s) -> String_set.empty 
     81        | S_Symbol(S_Sym_Ident s) -> if (String.compare s "ftrue") = 0 then  
     82                String_set.singleton s else String_set.empty 
    8283        | S_Symbol _ -> String_set.empty 
    8384 
     
    8586        | S_Term(_, sl, st) -> String_set.diff (free_spass st) (slist2set sl) 
    8687        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (free_spass b)) String_set.empty sl 
    87         | S_Symbol(S_Sym_Ident s) -> String_set.singleton s 
     88        | S_Symbol(S_Sym_Ident s) -> if (String.compare s "ftrue") = 0 then 
     89                String_set.empty else 
     90                String_set.singleton s 
    8891                (* we need to treat all zeroary function symbols we add to spass  differenlty here*) 
    8992        | S_Symbol _ -> String_set.empty 
  • src/typechecker/checker.ml

    r16308 r16322  
    2727                S_Term(a, List.map (fun a -> cfy a b) tl, cfy t b) 
    2828        | S_Symbol_Term(s, tl) -> S_Symbol_Term(s, List.map (fun a -> cfy a bound) tl) 
    29         | S_Symbol(S_Sym_Ident x) -> if (String_set.mem x bound) then spass_term else S_Symbol(S_Sym_Ident(("c" ^ x))) 
     29        | S_Symbol(S_Sym_Ident x) -> if (String_set.mem x bound) || (String.compare x "ftrue") = 0 then spass_term else S_Symbol(S_Sym_Ident(("c" ^ x))) 
    3030        | _ -> spass_term 
    3131 
  • src/typechecker/functions.ml

    r16282 r16322  
    105105let rec create_form_from_sconstr c = match c with 
    106106        (* removed SPair because there is no constructor SPair any longer *) 
    107 (*              | STrue -> S_Symbol(S_Sym_Ident("true"))*) 
    108                 | STrue -> S_Symbol(S_True) 
     107                | STrue -> S_Symbol(S_Sym_Ident("ftrue")) 
     108                (*| STrue -> S_Symbol(S_True)*) 
    109109                | SZk(n,m,_,stmlist) -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "zk_%d_%d" n m), List.map create_form_from_stmt stmlist)  
    110110        (*>>blindSig>>*) 
Note: See TracChangeset for help on using the changeset viewer.