Merge branch 'master' into propagate

Conflicts:
	typing/typer.ml

tests/libtest/tallyingTest.ml

@@ -348,12 +348,145 @@ let test_tallying =
     ) tallying_tests
 ;;
 
+let apply_raw_tests = [
+  "iter  hd",
+   "(`$A -> []) -> [ `$A* ] -> []","[ `$A0* ] -> `$A0";
+
+  "iteri  assoc",
+   "(Int -> `$A -> []) -> [ `$A* ] -> []","`$A1 -> [ (`$A1 , `$B1)* ] -> `$B1";
+
+  "map  length",
+   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","[ `$A3* ] -> Int";
+
+  "map  length & hd",
+   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","([ `$A3* ] -> Int) & ([ `$A4* ] -> `$A4)";
+
+  "mapi  mem",
+   "(Int -> `$A -> `$B) -> [ `$A* ] -> [ `$B* ]","`$A45 -> [ `$A45* ] -> Bool";
+
+  "mapi  mem & memq",
+   "(Int -> `$A -> `$B) -> [ `$A* ] -> [ `$B* ]","(`$A45 -> [ `$A45* ] -> Bool) & (`$A46 -> [ `$A46* ] -> Bool)";
+
+  "rev_map  length",
+   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","[ `$A53* ] -> Int";
+
+  "rev_map  length & hd",
+   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","([ `$A53* ] -> Int) & ([ `$A54* ] -> `$A54)";
+
+  "fold_left  append",
+   "(`$A -> `$B -> `$A) -> `$A -> [ `$B* ] -> `$A","[ `$A95* ] -> [ `$A95* ] -> [ `$A95* ]";
+
+  "fold_right  hd",
+   "(`$A -> `$B -> `$B) -> [ `$A* ] -> `$B -> `$B","[ `$A103* ] -> `$A103";
+
+  "iter2  hd",
+   "(`$A -> `$B -> []) -> [ `$A* ] -> [ `$B* ] -> []","[ `$A117* ] -> `$A117";
+
+  "map2  hd",
+   "(`$A -> `$B -> `$C) -> [ `$A* ] -> [ `$B* ] -> [ `$C* ]","[ `$A124* ] -> `$A124";
+
+  "rev_map2  hd",
+   "(`$A -> `$B -> `$C) -> [ `$A* ] -> [ `$B* ] -> [ `$C* ]","[ `$A160* ] -> `$A160";
+
+  "fold_left2  assoc",
+   "(`$A -> `$B -> `$C -> `$A) -> `$A -> [ `$B* ] -> [ `$C* ] -> `$A","`$A196 -> [ (`$A196 , `$B196)* ] -> `$B196";
+
+  "for_all  hd",
+   "(`$A -> Bool) -> [ `$A* ] -> Bool","[ `$A198* ] -> `$A198";
+
+  "exists  hd",
+   "(`$A -> Bool) -> [ `$A* ] -> Bool","[ `$A199* ] -> `$A199";
+
+  "for_all2  hd",
+   "(`$A -> `$B -> Bool) -> [ `$A* ] -> [ `$B* ] -> Bool","[ `$A200* ] -> `$A200";
+
+  "exists2  hd",
+   "(`$A -> `$B -> Bool) -> [ `$A* ] -> [ `$B* ] -> Bool","[ `$A211* ] -> `$A211";
+
+  "mem  length",
+   "`$A -> [ `$A* ] -> Bool","[ `$A222* ] -> Int";
+
+  "memq  length",
+   "`$A -> [ `$A* ] -> Bool","[ `$A264* ] -> Int";
+
+  "find  hd",
+   "(`$A -> Bool) -> [ `$A* ] -> `$A","[ `$A306* ] -> `$A306";
+
+  "filter  hd",
+   "(`$A -> Bool) -> [ `$A* ] -> [ `$A* ]","[ `$A307* ] -> `$A307";
+
+  "find_all  hd",
+   "(`$A -> Bool) -> [ `$A* ] -> [ `$A* ]","[ `$A308* ] -> `$A308";
+
+  "partition  hd",
+   "(`$A -> Bool) -> [ `$A* ] ->( [ `$A* ] , [ `$A* ])","[ `$A309* ] -> `$A309";
+
+  "assoc  length",
+   "`$A -> [ (`$A , `$B)* ] -> `$B","[ `$A310* ] -> Int";
+
+  "assoc  length & hd",
+   "`$A -> [ (`$A , `$B)* ] -> `$B","([ `$A310* ] -> Int) & ([ `$A311* ] -> `$A311)";
+
+  "mem_assoc  length",
+   "`$A -> [ (`$A , `$B)* ] -> Bool","[ `$A394* ] -> Int";
+
+  "mem_assoc  length & hd",
+   "`$A -> [ (`$A , `$B)* ] -> Bool","([ `$A394* ] -> Int) & ([ `$A395* ] -> `$A395)";
+
+  "mem_assq  length",
+   "`$A -> [ (`$A , `$B)* ] -> Bool","[ `$A436* ] -> Int";
+
+  "mem_assq  length & hd",
+   "`$A -> [ (`$A , `$B)* ] -> Bool","([ `$A436* ] -> Int) & ([ `$A437* ] -> `$A437)";
+
+  "remove_assoc  length",
+   "`$A -> [ (`$A , `$B)* ] -> [ (`$A , `$B)* ]","[ `$A478* ] -> Int";
+
+  "remove_assoc  length & hd",
+   "`$A -> [ (`$A , `$B)* ] -> [ (`$A , `$B)* ]","([ `$A478* ] -> Int) & ([ `$A479* ] -> `$A479)";
+]
+
+let test_apply =
+  let print_test msg s t = Printf.sprintf "%s : (%s) o (%s)\n" msg s t in
+  "apply" >:::
+    let sigmacup sl t =
+      List.fold_left (fun acc sigma -> 
+        Types.cap acc Tallying.(t $$ sigma)
+      ) Types.any sl
+    in
+    List.map (fun (msg,s,t) ->
+      (print_test msg s t) >:: (fun _ ->
+        try
+          let (s,t) = (parse_typ s,parse_typ t) in
+          let (sl,s,t,g) = Types.apply_raw s t in
+
+          let s_sigma = sigmacup sl s in
+          let t_sigma = sigmacup sl t in
+          let t_sigma_domain = (Types.Arrow.domain(Types.Arrow.get t_sigma)) in
+
+          assert_equal ~pp_diff:(fun fmt _ ->
+            Format.fprintf fmt "t @@ sl < 0 - 1 = %a\n" Types.Print.print t_sigma
+          ) (Types.subtype t_sigma (parse_typ "Empty -> Any")) true;
+
+          assert_equal ~pp_diff:(fun fmt _ ->
+            Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
+            Format.fprintf fmt "(s @@ sl) = %a\n" Types.Print.print s_sigma;
+            Format.fprintf fmt "(t @@ sl) = %a\n" Types.Print.print t_sigma;
+            Format.fprintf fmt "g = %a\n" Types.Print.print g;
+            Format.fprintf fmt "domain(t @@ sl) = %a\n" Types.Print.print t_sigma_domain
+          ) (Types.subtype s_sigma t_sigma) true
+        with Tallying.Step1Fail -> assert_equal [] []
+      )
+    ) apply_raw_tests 
+;;
+
 let suite =
   "tests" >::: [
     test_constraints;
     test_norm;
     test_merge;
     test_tallying;
+    test_apply;
   ]
 
 let main () =

types/types.ml

@@ -3251,6 +3251,9 @@ module Tallying = struct
     in
     (CS.ES.elements el)
 
+  (* apply sigma to t *)
+  let ($$) t si = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) si t
+
   type symsubst = I | S of CS.sigma | A of (symsubst * symsubst)
 
   let rec dom = function
@@ -3268,9 +3271,6 @@ module Tallying = struct
       )
     )
 
-  (* apply sigma to t *)
-  let ($$) t si = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) si t
-
   (* apply a symbolic substitution si to a type t *)
   let (@@) t si =
     let vst = ref Var.Set.empty in
@@ -3388,7 +3388,7 @@ let apply_raw s t =
 
 let apply_full s t =
   let _,_,_,res = apply_raw s t in
-  Format.printf "result: %a@\n@." Print.print res;
+  (* Format.printf "result: %a@\n@." Print.print res; *)
   res
 
 let apply s t = let s,_,_,_ = apply_raw s t in s

typing/typer.ml

@@ -866,9 +866,8 @@ and type_check' loc env ed constr precise = match ed with
       let t = Types.descr t in
       ignore (type_check env e t false);
       (ed,verify loc t constr)
-(*
-  | Subst (e, sigma) -> (ed,type_check env e constr precise)
-*)
+
+  | Subst (e, sigma) -> (* (ed,type_check env e constr precise) *) assert false
 
   | Check (t0,e,t) ->
       let te = type_check env e Types.any true in
@@ -898,14 +897,14 @@ and type_check' loc env ed constr precise = match ed with
           (fst(Types.squaresubtype env.delta t t2))::tacc (* H_j *)
         ) [] a.fun_iface
       in
-        List.iter (fun sl ->
-          if not(Types.Tallying.is_identity sl) then
-            List.iter (fun br ->
-              let e = br.br_body in
-              let loc = br.br_body.exp_loc in
-              br.br_body <- exp' loc (Subst(e,sl)); 
-            ) a.fun_body.br_branches
-        ) (List.rev sll);
+      List.iter (fun sl ->
+        if not(Types.Tallying.is_identity sl) then
+          List.iter (fun br ->
+            let e = br.br_body in
+            let loc = br.br_body.exp_loc in
+            br.br_body <- exp' loc (Subst(e,sl)); 
+          ) a.fun_body.br_branches
+      ) (List.rev sll);
       (ed,t)
 
   | Match (e,b) ->