[r2003-05-15 09:26:56 by cvscast] Empty log message

Original author: cvscast
Date: 2003-05-15 09:30:09+00:00

TODO

@@ -38,7 +38,7 @@ Regarder plus en general la section Error mining du Design paper
 
 Alain 2003-05-15
 
-  Détection des déclaration de type qui donnent un type vide
+  Fait: détection des déclaration de type qui donnent un type vide
 
 
 ======================================================================

driver/cduce.ml

@@ -49,6 +49,11 @@ let rec print_exn ppf = function
       Format.fprintf ppf "This expression should have type %a@\n%s@\n" 
         print_norm t
         msg
+  | Typer.ShouldHave2 (t1,msg,t2) ->
+      Format.fprintf ppf "This expression should have type %a@\n%s %a@\n" 
+        print_norm t1
+        msg
+        print_norm t2
   | Typer.Constraint (s,t,msg) ->
       Format.fprintf ppf "This expression should have type %a@\n" 
         print_norm t;

tests/bugs_prod.cd

 let x : `A | `B = `A;;
 let y : `A | `B = `B;;
-(* let z : (`A,`A)|(`B,`B) = (x,y);; *)
-let a : { x = `A; y = `A } |  { x = `B; y = `B } = { x = x; y = y };;
\ No newline at end of file
+let z : (`A,`A)|(`B,`B) = (x,y);;
+(* let a : { x = `A; y = `A } |  { x = `B; y = `B } = { x = x; y = y };; 
+*)

types/types.ml

@@ -656,7 +656,10 @@ struct
 
   let need_second = function _::_::_ -> true | _ -> false
 
-  let normal_aux d =
+  let normal_aux = function
+    | ([] | [ _ ]) as d -> d
+    | d ->
+
     let res = ref [] in
 
     let add (t1,t2) =
@@ -759,7 +762,8 @@ This version explodes when dealing with
 
   module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
 
-
+  (* TODO: try with an hashtable *)
+  (* Also, avoid lookup for simple products (t1,t2) *)
   let memo = ref Memo.empty
   let normal ?(kind=`Normal) d = 
     let d = match kind with `Normal -> d.times | `XML -> d.xml in
@@ -773,6 +777,13 @@ This version explodes when dealing with
 	  memo := Memo.add d n !memo;
 	  n
 
+  let constraint_on_2 n t1 =
+    List.fold_left 
+      (fun accu (d1,d2) ->
+	 if is_empty (cap d1 t1) then accu else cap accu d2)
+      any
+      n
+
   let any = { empty with times = any.times }
   and any_xml = { empty with xml = any.xml }
   let is_empty d = d == []

types/types.mli

@@ -94,6 +94,10 @@ module Product : sig
   type normal = t
   val normal: ?kind:pair_kind -> descr -> normal
 
+  val constraint_on_2: normal -> descr -> descr
+    (* constraint_on_2 n t1:  maximal t2 such that (t1,t2) <= n *)
+    (* Assumption: t1 <= pi1(n) *)
+
   val need_second: t -> bool
     (* Is there more than a single rectangle ? *)
 end

typing/typer.ml

@@ -27,6 +27,7 @@ module Env = Map.Make(Id)
 exception NonExhaustive of Types.descr
 exception Constraint of Types.descr * Types.descr * string
 exception ShouldHave of Types.descr * string
+exception ShouldHave2 of Types.descr * string * Types.descr
 exception WrongLabel of Types.descr * label
 exception UnboundId of string
 
@@ -264,7 +265,7 @@ module Arg = struct
     (s1 == s2) || 
     (incr gen; rank := 0; 
      let e = equal_slot s1 s2 in
-(*     if e then Printf.eprintf "Equal\n"; *)
+(*     if e then Printf.eprintf "Recursive hash-consig: Equal\n";  *)
      e)
 end
 module SlotTable = Hashtbl.Make(Arg)
@@ -813,22 +814,17 @@ and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
     (match kind with
       | `Normal -> raise_loc loc (ShouldHave (constr,"but it is a pair."))
       | `XML -> raise_loc loc (ShouldHave (constr,"but it is an XML element.")));
-  let pi1 = Types.Product.pi1 rects in
-
   let need_s = Types.Product.need_second rects in
-(*  Printf.eprintf "need_second: %b\n" need_s; *)
-  let precise = precise || need_s in
-  let t1 = type_check env e1 (Types.Product.pi1 rects) precise in
-  let rects = Types.Product.restrict_1 rects t1 in
-  let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
+  let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in
+  let c2 = Types.Product.constraint_on_2 rects t1 in
+  if Types.is_empty c2 then 
+    raise_loc loc (ShouldHave2 (constr,"but the first component has type",t1));
+  let t2 = type_check env e2 c2 precise in
 
   if precise then 
-    let t =
-      match kind with
-      	| `Normal -> Types.times (Types.cons t1) (Types.cons t2)
-      	| `XML -> Types.xml (Types.cons t1) (Types.cons t2) in
-    check loc t constr "";
-    t
+    match kind with
+      | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
+      | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
   else
     constr
 

typing/typer.mli

@@ -5,6 +5,7 @@ exception Constraint of Types.descr * Types.descr * string
 exception ShouldHave of Types.descr * string
 exception WrongLabel of Types.descr * label
 exception UnboundId of string
+exception ShouldHave2 of Types.descr * string * Types.descr
 
 module Env : Map.S with type key = id
 type env = Types.descr Env.t