Changeset 16322

Timestamp:

12/12/08 11:39:57 (4 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:

• alpha.ml (modified) (2 diffs)
• checker.ml (modified) (1 diff)
• functions.ml (modified) (1 diff)

src/typechecker/alpha.ml

@@ -79 +79 @@
         S_Term(_, sl, st) -> String_set.union (bound_spass st) (slist2set sl)
         | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (bound_spass b)) String_set.empty sl
-        | S_Symbol(S_Sym_Ident s) -> String_set.empty
+        | S_Symbol(S_Sym_Ident s) -> if (String.compare s "ftrue") = 0 then 
+                String_set.singleton s else String_set.empty
         | S_Symbol _ -> String_set.empty
 
@@ -85 +86 @@
         | S_Term(_, sl, st) -> String_set.diff (free_spass st) (slist2set sl)
         | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (free_spass b)) String_set.empty sl
-        | S_Symbol(S_Sym_Ident s) -> String_set.singleton s
+        | S_Symbol(S_Sym_Ident s) -> if (String.compare s "ftrue") = 0 then
+                String_set.empty else
+                String_set.singleton s
                 (* we need to treat all zeroary function symbols we add to spass  differenlty here*)
         | S_Symbol _ -> String_set.empty

src/typechecker/checker.ml

@@ -27 +27 @@
                 S_Term(a, List.map (fun a -> cfy a b) tl, cfy t b)
         | S_Symbol_Term(s, tl) -> S_Symbol_Term(s, List.map (fun a -> cfy a bound) tl)
-        | S_Symbol(S_Sym_Ident x) -> if (String_set.mem x bound) then spass_term else S_Symbol(S_Sym_Ident(("c" ^ x)))
+        | 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)))
         | _ -> spass_term
 

src/typechecker/functions.ml

@@ -105 +105 @@
 let rec create_form_from_sconstr c = match c with
         (* removed SPair because there is no constructor SPair any longer *)
-(*              | STrue -> S_Symbol(S_Sym_Ident("true"))*)
-                | STrue -> S_Symbol(S_True)
+                | STrue -> S_Symbol(S_Sym_Ident("ftrue"))
+                (*| STrue -> S_Symbol(S_True)*)
                 | SZk(n,m,_,stmlist) -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "zk_%d_%d" n m), List.map create_form_from_stmt stmlist) 
         (*>>blindSig>>*)