fix typed application problem

types/types.ml

@@ -190,11 +190,11 @@ module TLV = struct
   }
 
   (* true if it contains only one variable *)
-  let is_single x = x.isvar && (Var.Set.cardinal x.fv = 1) && (Set.cardinal x.tlv = 1)
+  let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1)
 
-  let no_variables x = (Var.Set.cardinal x.fv = 0) && (Set.cardinal x.tlv = 0)
+  let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0)
 
-  let has_toplevel x = Set.cardinal x.tlv > 0
+  let has_toplevel t = Set.cardinal t.tlv > 0
 
   let print ppf x = Set.print ";" ppf x.tlv
   let dump ppf x =
@@ -532,6 +532,8 @@ let has_tlv t = TLV.has_toplevel t.toplvars
 let all_vars t = t.toplvars.TLV.fv
 let all_tlv t = t.toplvars.TLV.tlv
 
+let is_closed delta t = (no_var t) || (Var.Set.is_empty (Var.Set.diff (all_vars t) delta))
+
 let cup x y =
   if x == y then x else
     let t = {
@@ -1953,7 +1955,7 @@ struct
     | Name _ | Char _ | Atomic _ -> ()
     | Regexp r -> assign_name_regexp r
     | Pair (t1,t2) -> assign_name t1; assign_name t2
-    | Intersection t -> assign_name t
+    | Intersection t -> () (* assign_name t *)
     | Xml (tag,t2,t3) ->
 	(match tag with `Type t -> assign_name t | _ -> ());
 	assign_name t2;

types/types.mli

@@ -113,6 +113,7 @@ val any    : t
 val no_var  : t -> bool
 val is_var  : t -> bool
 val has_tlv : t -> bool
+val is_closed : Var.Set.t -> t -> bool
 
 val any_node : Node.t
 val empty_node : Node.t

typing/typer.ml

@@ -946,45 +946,46 @@ and type_check' loc env ed constr precise = match ed with
       (ed,localize loc (flatten (type_map loc env true e b) constr) precise)
 
   | Apply (e1,e2) ->
-      let t1 = type_check env e1 Types.any true in 
-      let t2 = type_check env e2 Types.any true in
-      let (sl,res) = 
-        (* t [_delta 0 -> 1 *)
-        (* s [_delta dom(t) *)
-        try Types.squareapply env.delta t1 t2 
-        with Types.Tallying.UnSatConstr _ ->
-          raise_loc loc (Constraint (Types.Arrow.domain(Types.Arrow.get t1),t2))
+      Printf.printf "1\n";
+      let t1 = type_check env e1 Types.Arrow.any true in 
+
+      (* t [_delta 0 -> 1 *)
+      begin try ignore(Types.Tallying.tallying ~delta:env.delta [(t1,Types.Arrow.any)])
+      with Types.Tallying.UnSatConstr _ -> raise_loc loc (Constraint (t1, Types.Arrow.any)) end;
+
+      Printf.printf "2\n";
+      let t1arrow = Types.Arrow.get t1 in
+      let dom = Types.Arrow.domain(t1arrow) in
+      let res = 
+        if not(Types.is_closed env.delta dom) then begin
+          (* get t2 without constraint check *)
+      Printf.printf "3\n";
+          let t2 = type_check env e2 Types.any true in
+      Printf.printf "4\n";
+          let (sl,res) = 
+            (* s [_delta dom(t) *)
+            try Types.squareapply env.delta t1 t2 
+            with Types.Tallying.UnSatConstr _ ->
+              raise_loc loc (Constraint (dom,t2))
+          in 
+      Printf.printf "5\n";
+          res
+        end else begin
+          (* Monomorphic case as before *)
+      Printf.printf "44\n";
+          if Types.Arrow.need_arg t1arrow then begin
+            let t2 = type_check env e2 dom true in
+      Printf.printf "55\n";
+            Types.Arrow.apply t1arrow t2
+          end else begin
+            (ignore (type_check env e2 dom false); 
+      Printf.printf "66\n";
+            Types.Arrow.apply_noarg t1arrow)
+          end
+        end
       in
       (Apply(e1,e2),verify loc res constr)
-(*
-      let (sJ,is_subtype) = Types.squaresubtype env.delta t1_t Types.Arrow.any in
-      if not is_subtype then raise_loc loc (Constraint (t, s));
 
-  Format.printf "Apply e1 ->>%a\n\n" Typed.Print.pp_typed e1;
-
-      let t1 = Types.Arrow.get t1_t in
-      let dom = Types.Arrow.domain t1 in
-  
-      let sI,res =
-        if Types.Arrow.need_arg t1 then
-          let t2 = type_check env e2 dom true in
-          let (sl,is_subtype) = Types.squaresubtype env.delta t2 dom in
-          if not is_subtype then raise_loc loc (Constraint (t, s));
-  Format.printf "Apply e2 ->>%a\n\n" Typed.Print.pp_typed e2;
-          Types.apply_full env.delta t1_t t2
-        else begin
-          (* s [_delta dom(t) *)
-          let t2 = type_check env e2 dom false in
-          let (sl,is_subtype) = Types.squaresubtype env.delta t2 dom in
-          if not is_subtype then raise_loc loc (Constraint (t, s));
-
-          (* ignore (type_check env e2 dom false); *)
-  Format.printf "Apply e2 ->>%a\n\n" Typed.Print.pp_typed e2;
-          Types.Arrow.apply_noarg t1
-        end
-      in
-      (Apply(Subst(e1,sJ),Subst(e2,sI)),verify loc res constr)
-*)
   | Var s -> 
       (ed,verify loc (find_value s env) constr)