Positive.substtute now build recursive types correctly

tests/libtest/typesTest.ml

@@ -44,8 +44,8 @@ let subst_tests = [
   "(`$A , (`$B -> (Bool -> `$C)))", "C", "Int", "(`$A , (`$B -> (Bool -> Int)))";
 ];;
 
-let test_set_operations =
-  "test set operations" >::: 
+let test_substitution =
+  "test type substitution operations" >::: 
     List.map (fun (t,v,s,expected) ->
       (Printf.sprintf "[%s]{%s/%s}") t v s >:: (fun _ ->
           let t = parse_typ t in
@@ -53,11 +53,40 @@ let test_set_operations =
           let s = parse_typ s in
           let expected = parse_typ expected in
           let result = Types.subst t (v,s) in
-          assert_equal ~cmp:Types.equiv ~printer:(fun t -> Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)) expected result
+          assert_equal ~cmp:Types.equiv ~printer:(fun t ->
+            Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)
+          ) expected result
       )
     ) subst_tests
 ;;
 
+let rec_subst_tests = [
+  "`$A", "A", "Empty";
+  "`$A", "B", "`$A";
+  "`$A | Int", "A", "X where X = (X | Int)";
+  "`$A | `$B | Int", "A", "X where X = X | `$B | Int";
+  "`$A -> `$B", "A", "X where X = X -> `$B";
+  "Bool -> `$B", "A", "Bool -> `$B";
+  "(`$A , `$B)", "A", "X where X = (X, `$B)";
+  "(`$A , (`$B -> (Bool -> `$C)))", "C", "X where X = (`$A , (`$B -> (Bool -> X)))";
+];;
+
+let test_rec_subtitutions =
+  "test recursive type substitution operations" >::: 
+    List.map (fun (t,v,expected) ->
+      (Printf.sprintf "mu X . [%s]{%s/X}") t v >:: (fun _ ->
+          let t = parse_typ t in
+          let v = `Var v in
+          let expected = parse_typ expected in
+          let result = Types.Positive.substitute t v in
+          assert_equal ~cmp:Types.equiv ~printer:(fun t ->
+            Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)
+          ) expected result
+      )
+    ) rec_subst_tests
+;;
+
+
 let subtype_tests = [
   "Int" , "Any", true;
   "`A | Int" , "`A", false;
@@ -189,6 +218,8 @@ let all =
   "all tests" >::: [
     test_set_operations;
     test_subtype;
+    test_substitution;
+    test_rec_subtitutions;
     (* test_witness; *)
   ]
  

types/types.ml

@@ -2126,7 +2126,7 @@ struct
   let xml v1 v2 = cons (`Xml (v1,v2))
   let define v1 v2 = def v1 (`Cup [v2]) 
 
-  let rec transform t =
+  let rec decompose t =
     let aux_bdd ?noderec constr (p,n) =
       let aux polarity constr l = 
         cap (
@@ -2150,8 +2150,8 @@ struct
           let deep polarity l =
             cap (
               List.map (fun (t1,t2) ->
-                let d1 = transform (descr t1) in
-                let d2 = transform (descr t2) in
+                let d1 = decompose (descr t1) in
+                let d2 = decompose (descr t2) in
                 polarity(constr d1 d2)
               ) l
             )
@@ -2160,16 +2160,16 @@ struct
         ) (Pair.get bdd)
       )
     in
-    let transform_aux ?noderec constr l =
+    let decompose_aux ?noderec constr l =
         cup (List.map (fun (p,n) -> (aux_bdd ?noderec constr (p,n))) l)
     in
     cup [
-      transform_aux atom (BoolAtoms.get t.atoms);
-      transform_aux interval (BoolIntervals.get t.ints);
-      transform_aux char (BoolChars.get t.chars);
-      transform_aux ~noderec:(subpairs arrow) (fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) (BoolPair.get t.arrow);
-      transform_aux ~noderec:(subpairs xml) (fun p -> { empty with xml = BoolPair.atom (`Atm p) }) (BoolPair.get t.xml);
-      transform_aux ~noderec:(subpairs times) (fun p -> { empty with times = BoolPair.atom (`Atm p) }) (BoolPair.get t.times);
+      decompose_aux atom (BoolAtoms.get t.atoms);
+      decompose_aux interval (BoolIntervals.get t.ints);
+      decompose_aux char (BoolChars.get t.chars);
+      decompose_aux ~noderec:(subpairs arrow) (fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) (BoolPair.get t.arrow);
+      decompose_aux ~noderec:(subpairs xml) (fun p -> { empty with xml = BoolPair.atom (`Atm p) }) (BoolPair.get t.xml);
+      decompose_aux ~noderec:(subpairs times) (fun p -> { empty with times = BoolPair.atom (`Atm p) }) (BoolPair.get t.times);
     ]
 
   let solve v = internalize (make_node v)
@@ -2190,9 +2190,8 @@ struct
       |`Neg v -> neg (aux_subst v (alpha,x))
     in
     let x = forward () in
-    let t1 = solve (aux_subst (transform t) (alpha,x)) in
-    t1.Node.descr <- (descr t1);
-    descr t1
+    define x (aux_subst (decompose t) (alpha,x));
+    descr(solve x)
 
 end
 

types/types.mli

@@ -156,7 +156,7 @@ sig
   val times: v -> v -> v
   val xml: v -> v -> v
 
-  val transform : t -> v
+  val decompose : t -> v
   val substitute : t -> Var.var -> t
   val solve: v -> Node.t
 end