Fix problems in the function norm

tests/libtest/tallyingTest.ml

@@ -197,6 +197,8 @@ let norm_tests = [
     [P(V "A","Empty")]
   ];
   *)
+
+  "Bool -> Bool","Int -> `$A", mk_s [];
 ]
 
 let test_norm =
@@ -286,6 +288,8 @@ let tallying_tests = [
   [("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
     [(V "A","Int");(V "B","Int")]
   ];
+  [("[] -> []","Int -> `$A")], [[]];
+  [("Bool -> Bool","Int -> `$A")], [[]];
 ]
 
 let test_tallying =

types/types.ml

@@ -2531,8 +2531,8 @@ module Tallying = struct
     let prod x y =
       match S.is_empty x,S.is_empty y with
       |true,true -> S.empty
-      |false,true -> x
-      |true,false -> y
+      |false,true -> S.empty
+      |true,false -> S.empty
       |false,false ->
         S.fold (fun m1 acc ->
           S.fold (fun m2 acc1 -> union (S.singleton (merge m1 m2)) acc1) y acc
@@ -2612,7 +2612,7 @@ module Tallying = struct
           CS.prod acc (toplevel single norm_aux m (pos,neg)) 
         ) acc l
       in
-      let accu = CS.unsat in
+      let accu = CS.sat in
       let accu = aux_base single_atoms normatoms accu (BoolAtoms.get t.atoms) in
       let accu = aux_base single_chars normchars accu (BoolChars.get t.chars) in
       let accu = aux_base single_ints normints accu (BoolIntervals.get t.ints) in
@@ -2786,7 +2786,7 @@ module Tallying = struct
         (* remove from E \ { (alpha,t) } every occurrences of alpha 
          * by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
         (* XXX : substvariance remove all previously introduced fresh variables *)
-        let x = substvariance (Positive.substitute t alpha) in
+        let x = (* substvariance *) (Positive.substitute t alpha) in
         let es = CS.E.fold (fun beta s acc -> CS.E.add beta (subst s (alpha,x)) acc) e1 CS.E.empty in
         aux ((CS.E.add alpha x sol),(CS.E.add alpha x acc)) es
     in