[r2003-05-24 19:31:52 by cvscast] New sample system

Original author: cvscast
Date: 2003-05-24 19:31:53+00:00

Makefile

@@ -48,6 +48,7 @@ OBJECTS = \
  types/sortedList.cmo types/boolean.cmo types/ident.cmo \
  types/intervals.cmo types/chars.cmo types/atoms.cmo types/normal.cmo \
  types/types.cmo types/patterns.cmo types/sequence.cmo types/builtin.cmo \
+ types/sample.cmo \
  \
  parser/location.cmo parser/wlexer.cmo parser/ast.cmo parser/parser.cmo \
  \

depend

@@ -56,6 +56,8 @@ types/patterns.cmo: types/atoms.cmi types/chars.cmi types/ident.cmo \
     types/sortedList.cmi misc/state.cmi types/types.cmi types/patterns.cmi 
 types/patterns.cmx: types/atoms.cmx types/chars.cmx types/ident.cmx \
     types/sortedList.cmx misc/state.cmx types/types.cmx types/patterns.cmi 
+types/sample.cmo: types/ident.cmo types/types.cmi types/sample.cmi 
+types/sample.cmx: types/ident.cmx types/types.cmx types/sample.cmi 
 types/sequence.cmo: types/atoms.cmi types/types.cmi types/sequence.cmi 
 types/sequence.cmx: types/atoms.cmx types/types.cmx types/sequence.cmi 
 types/sortedList.cmo: types/sortedList.cmi 
@@ -117,6 +119,7 @@ types/atoms.cmi: misc/encodings.cmi
 types/boolean.cmi: types/sortedList.cmi 
 types/patterns.cmi: types/atoms.cmi types/chars.cmi types/ident.cmo \
     types/types.cmi 
+types/sample.cmi: types/types.cmi 
 types/sequence.cmi: types/atoms.cmi types/types.cmi 
 types/types.cmi: types/atoms.cmi types/chars.cmi types/ident.cmo \
     types/intervals.cmi types/sortedList.cmi 

driver/cduce.ml

@@ -68,17 +68,17 @@ let rec print_exn ppf = function
         print_norm t;
       Format.fprintf ppf "but its infered type is:@\n%a@\n" 
         print_norm s;
-      Format.fprintf ppf "which is not a subtype, as shown by the value " ;
+      Format.fprintf ppf "which is not a subtype, as shown by the sample " ;
       Location.protect ppf
 	(fun ppf ->
-	   Types.Sample.print ppf (Types.Sample.get (Types.diff s t)));
+	   Sample.print ppf (Sample.get (Types.diff s t)));
       Format.fprintf ppf "@\n%s@\n" msg
   | Typer.NonExhaustive t ->
       Format.fprintf ppf "This pattern matching is not exhaustive@\n";
       Format.fprintf ppf "Residual type:@\n%a@\n"
 	print_norm t;
-      Format.fprintf ppf "Sample value:@\n%a@\n" 
-	Types.Sample.print (Types.Sample.get t)
+      Format.fprintf ppf "Sample:@\n%a@\n" 
+	Sample.print (Sample.get t)
   | Typer.UnboundId x ->
       Format.fprintf ppf "Unbound identifier %a@\n" U.print (Id.value x)
   | Wlexer.Illegal_character c ->
@@ -104,6 +104,12 @@ let debug ppf = function
       and t2 = Types.descr (Typer.typ t2) in
       Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2
 	(Types.subtype t1 t2)
+  | `Sample t ->
+      Format.fprintf ppf "[DEBUG:sample]@\n";
+      let t = Types.descr (Typer.typ t) in
+      Location.protect ppf
+	(fun ppf -> Sample.print ppf (Sample.get t));
+      Format.fprintf ppf "@\n"
   | `Filter (t,p) -> 
       Format.fprintf ppf "[DEBUG:filter]@\n";
       let t = Typer.typ t

parser/ast.ml

@@ -15,6 +15,7 @@ and pmodule_item' =
   | Debug of debug_directive
 and debug_directive =
   [ `Filter of ppat * ppat
+  | `Sample of ppat
   | `Accept of ppat
   | `Compile of ppat * ppat list 
   | `Subtype of ppat * ppat

parser/parser.ml

@@ -127,6 +127,7 @@ EXTEND
     [ LIDENT "filter"; t = pat; p = pat -> `Filter(t,p)
     | LIDENT "accept"; p = pat -> `Accept p
     | LIDENT "compile"; t = pat; p = LIST1 pat -> `Compile (t,p)
+    | LIDENT "sample"; t = pat -> `Sample t
     | LIDENT "subtype"; t1 = pat; t2 = pat -> `Subtype (t1,t2)
     ]
   ];

types/patterns.ml

@@ -190,6 +190,9 @@ let filter t p =
 
 let min (a:int) (b:int) = if a < b then a else b
 
+let any_basic = Types.Record.or_absent Types.non_constructed
+
+
 module Normal : sig 
   type source = 
     | SCatch | SConst of Types.const 
@@ -218,18 +221,10 @@ module Normal : sig
   val dummy: t
   val compare_nf: t -> t -> int
 
-  val any_basic: Types.descr
   val first_label: descr -> label
   val normal: label option -> Types.descr -> node list -> t
 end = 
 struct
-  let any_basic = 
-    Types.Record.or_absent
-      (Types.neg (List.fold_left Types.cup Types.empty
-		    [Types.Product.any_xml;
-		     Types.Product.any;
-		     Types.Record.any]))
-
 
   type source = 
     | SCatch | SConst of Types.const 
@@ -869,7 +864,7 @@ struct
       Array.iteri (fun i -> Normal.NLineBasic.iter (aux i)) pl;
       Types.DescrSList.Map.get (Types.DescrSList.Map.from_list (@) !accu) in
 
-    let t = Types.cap Normal.any_basic disp.t in
+    let t = Types.cap any_basic disp.t in
     let accu = ref [] in
     let rec aux (success : (int * Normal.result) list) t l = 
       if Types.non_empty t 

types/sample.ml

+open Ident
+
+type t = Types.descr
+
+let rec try_seq f = function
+  | [] -> raise Not_found
+  | hd::tl -> try f hd with Not_found -> try_seq f tl
+
+module D = Types.DescrSet
+  
+let absent = Types.cons (Types.Record.or_absent Types.empty)
+
+let rec get memo t =
+  if D.mem t memo then raise Not_found;
+  let memo = D.add t memo in
+  let cons t = Types.cons (get memo t) in
+  let pair (t1,t2) = Types.times (cons t1) (cons t2) in
+  let xml (t1,t2) = Types.xml (cons t1) (cons t2) in
+  let rec fields = function
+    | (true,_) -> absent
+    | (false,t) -> cons t in
+  let record (r,some,none) = Types.record' (not none, LabelMap.map fields r) in
+  let typ u = 
+    let u = Types.cap t u in 
+    if Types.is_empty u then raise Not_found else u in
+  try try_seq typ [ Types.Int.any; Types.Atom.any; Types.Char.any ] with Not_found ->
+  try try_seq pair (Types.Product.get t) with Not_found ->
+  try try_seq xml (Types.Product.get ~kind:`XML t) with Not_found ->
+  try try_seq record (Types.Record.get t) with Not_found ->
+  try Types.Arrow.sample t with Not_found ->
+  raise Not_found
+     
+let get = get D.empty
+
+let print = Types.Print.print

types/sample.mli

+type t = Types.descr
+
+val get : Types.descr -> t
+  (** 
+    Extract when possible a subtype which is ``trivially'' non-empty.
+    This subtype is built from scalar and intersection of simple arrow types
+    using products, XML elements and records, without recursion.
+
+    Interpretation of this subtype, to extract sample values:
+    - open record type:  add some extra field not listed
+    - intersection of arrow types: ...
+    
+    Raises Not_found for an empty type
+  **)
+
+val print : Format.formatter -> t -> unit

types/types.ml

@@ -134,7 +134,10 @@ let any =  {
   chars = Chars.any;
   absent= false;
 }
-	     
+
+let non_constructed =
+  { any with times = empty.times; xml = empty.xml; record = empty.record }
+     
 	     
 let interval i = { empty with ints = i }
 let times x y = { empty with times = BoolPair.atom (x,y) }
@@ -262,9 +265,9 @@ let define n d =
 (*  DescrHash.add hash_cons d n; *)
   n.descr <- d
 let cons d = 
-  (* try DescrHash.find hash_cons d with Not_found ->
+(*   try DescrHash.find hash_cons d with Not_found ->
   incr count; let n = { id = !count; descr = d } in
-  DescrHash.add hash_cons d n; n *)
+  DescrHash.add hash_cons d n; n  *)
   incr count; { id = !count; descr = d }
 let descr n = n.descr
 let internalize n = n
@@ -332,16 +335,13 @@ let get_record r =
 let diff_t d t = diff d (descr t)
 let cap_t d t = cap d (descr t)
 let cup_t d t = cup d (descr t)
-let cap_product l =
+let cap_product any_left any_right l =
   List.fold_left 
     (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
-    (any,any)
-    l
-let cup_product l =
-  List.fold_left 
-    (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
-    (empty,empty)
+    (any_left,any_right)
     l
+let any_pair = { empty with times = any.times }
+
 
 let rec exists max f =
   (max > 0) && (f (max - 1) || exists (max - 1) f)
@@ -412,7 +412,7 @@ and slot d =
     DescrHash.add memo d s;
     (try
        iter_s s check_times (BoolPair.get d.times);  
-       iter_s s check_times (BoolPair.get d.xml); 
+       iter_s s check_xml (BoolPair.get d.xml); 
        iter_s s check_arrow (BoolPair.get d.arrow);
        iter_s s check_record (get_record d.record);
        if s.active then marks := s :: !marks else s.status <- Empty;
@@ -436,7 +436,26 @@ and check_times (left,right) s =
 	)
     | [] -> set s
   in
-  let (accu1,accu2) = cap_product left in
+  let (accu1,accu2) = cap_product any any left in
+  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
+
+and check_xml (left,right) s =
+  let rec aux accu1 accu2 right s = match right with
+    | (t1,t2)::right ->
+	let t1 = descr t1 and t2 = descr t2 in
+	if trivially_disjoint accu1 t1 || 
+	   trivially_disjoint accu2 t2 then (
+	     aux accu1 accu2 right s )
+	else (
+          let accu1' = diff accu1 t1 in 
+	  guard accu1' (aux accu1' accu2 right) s;
+
+          let accu2' = diff accu2 t2 in 
+	  guard accu2' (aux accu1 accu2' right) s  
+	)
+    | [] -> set s
+  in
+  let (accu1,accu2) = cap_product any any_pair left in
   guard accu1 (guard accu2 (aux accu1 accu2 right)) s
 
 and check_arrow (left,right) s =
@@ -652,7 +671,7 @@ This version explodes when dealing with
    Any - [ t1? t2? t3? ... tn? ]
 ==> need partitioning 
 *)
-  let get_aux d =
+  let get_aux any_right d =
     let line accu (left,right) =
       let rec aux accu d1 d2 = function
 	| (t1,t2)::right ->
@@ -665,7 +684,7 @@ This version explodes when dealing with
 	    accu
 	| [] -> (d1,d2) :: accu
       in
-      let (d1,d2) = cap_product left in
+      let (d1,d2) = cap_product any any_right left in
       if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
     in
     List.fold_left line [] d
@@ -677,10 +696,10 @@ This version explodes when dealing with
 (t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)
 
 *)
-  let get_aux d =
+  let get_aux any_right d =
     let accu = ref [] in
     let line (left,right) =
-      let (d1,d2) = cap_product left in
+      let (d1,d2) = cap_product any any_right left in
       if (non_empty d1) && (non_empty d2) then
 	let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
 	let right = normal_aux right in
@@ -705,8 +724,8 @@ This version explodes when dealing with
 
   let get ?(kind=`Normal) d = 
     match kind with
-      | `Normal -> get_aux d.times
-      | `XML -> get_aux d.xml
+      | `Normal -> get_aux any d.times
+      | `XML -> get_aux any_pair d.xml
 
   let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
   let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
@@ -727,18 +746,33 @@ This version explodes when dealing with
   (* 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
+  let normal_times d = 
     try Memo.find d !memo 
     with
 	Not_found ->
-	  let gd = get_aux d in
+	  let gd = get_aux any d in
 	  let n = normal_aux gd in
 (* Could optimize this call to normal_aux because one already
    know that each line is normalized ... *)
 	  memo := Memo.add d n !memo;
 	  n
 
+  let memo_xml = ref Memo.empty
+  let normal_xml d = 
+    try Memo.find d !memo_xml
+    with
+	Not_found ->
+	  let gd = get_aux any_pair d in
+	  let n = normal_aux gd in
+	  memo_xml := Memo.add d n !memo_xml;
+	  n
+
+  let normal ?(kind=`Normal) d =
+    match kind with 
+      | `Normal -> normal_times d.times 
+      | `XML -> normal_xml d.xml
+
+
   let merge_same_2 r =
     let r = 
       List.fold_left 
@@ -928,7 +962,9 @@ struct
 	if o1 || o2 then (LabelMap.from_list_disj r,o1,o2)::accu else accu
       else
 	List.fold_left 
-	  (fun accu (t1,t2) -> aux ((l,t1)::r) accu t2)
+	  (fun accu (t1,t2) -> 
+	     let x = (t1.absent, { t1 with absent = false }) in
+	     aux ((l,x)::r) accu t2)
 	  accu
 	  (split d l)
     in
@@ -1063,6 +1099,7 @@ struct
 	       match Atoms.is_atom t1.atoms with
 		 | Some a when is_empty { t1 with atoms = Atoms.empty } -> `Tag a
 		 | _ -> `Type (prepare t1) in
+	     assert (equal_descr { t2 with times = empty.times } empty);
 	     List.iter
 	       (fun (ta,tb) -> add (Xml (tag, prepare ta, prepare tb)))
 	       (Product.get t2)
@@ -1070,9 +1107,7 @@ struct
 	  ((*Product.merge_same_2*) (Product.get ~kind:`XML not_seq));
 	List.iter
 	  (fun (r,some,none) -> 
-	     let r = LabelMap.map 
-		       (fun t ->
-			  (t.absent, prepare { t with absent = false })) r in
+	     let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
 	     add (Record (r,some,none)))
 	  (Record.get not_seq);
 	(match Chars.is_char not_seq.chars with
@@ -1310,183 +1345,6 @@ struct
 end
 
 
-
-
-(* Sample value *)
-module Sample =
-struct
-
-
-let rec find f = function
-  | [] -> raise Not_found
-  | x::r -> try f x with Not_found -> find f r
-
-type t =
-  | Int of Intervals.v
-  | Atom of Atoms.v
-  | Char of Chars.v
-  | Pair of (t * t)
-  | Xml of (t * t)
-  | Record of (bool * (label * t) list)
-  | Fun of (node * node) list
-  | Other
- exception FoundSampleRecord of bool * (label * t) list
-
-let rec sample_rec memo d =
-  if (DescrSet.mem d memo) || (is_empty d) then raise Not_found 
-  else 
-    try Int (Intervals.sample d.ints) with Not_found ->
-    try Atom (Atoms.sample d.atoms) with 
-	Not_found ->
-(* Here: could create a fresh atom ... *)
-    try Char (Chars.sample d.chars) with Not_found ->
-    try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
-
-    let memo = DescrSet.add d memo in
-    try Pair (sample_rec_times memo (BoolPair.get d.times)) with Not_found ->
-    try Xml (sample_rec_times memo (BoolPair.get d.xml)) with Not_found ->
-    try sample_rec_record memo d.record with Not_found ->  
-    raise Not_found
-
-
-and sample_rec_times memo c = 
-  find (sample_rec_times_aux memo) c
-
-and sample_rec_times_aux memo (left,right) =
-  let rec aux accu1 accu2 = function
-    | (t1,t2)::right ->
-(*TODO: check: is this correct ?  non_empty could return true
-  but because of coinduction, the call to aux may raise Not_found, no ? *)
-        let accu1' = diff_t accu1 t1 in
-        if non_empty accu1' then aux accu1' accu2 right else
-          let accu2' = diff_t accu2 t2 in
-          if non_empty accu2' then aux accu1 accu2' right else
-	    raise Not_found
-    | [] -> (sample_rec memo accu1, sample_rec memo accu2)
-  in
-  let (accu1,accu2) = cap_product left in
-  if (is_empty accu1) || (is_empty accu2) then raise Not_found;
-  aux accu1 accu2 right
-
-and sample_rec_arrow c =
-  find sample_rec_arrow_aux c
-
-and check_empty_simple_arrow_line left (s1,s2) = 
-  let rec aux accu1 accu2 = function
-    | (t1,t2)::left ->
-        let accu1' = diff_t accu1 t1 in
-        if non_empty accu1' then aux accu1 accu2 left;
-        let accu2' = cap_t accu2 t2 in
-        if non_empty accu2' then aux accu1 accu2 left
-    | [] -> raise NotEmpty
-  in
-  let accu1 = descr s1 in
-  (is_empty accu1) ||
-  (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
-
-and check_empty_arrow_line left right = 
-  List.exists (check_empty_simple_arrow_line left) right
-
-and sample_rec_arrow_aux (left,right) =
-  if (check_empty_arrow_line left right) then raise Not_found
-  else Fun left
-
-
-and sample_rec_record memo c =
-  Record (find (sample_rec_record_aux memo) (get_record c))
-
-and sample_rec_record_aux memo (labels,(oleft,left),rights) =
-  let rec aux = function
-    | [] -> 
-	let l = ref labels and fields = ref [] in
-	for i = 0 to Array.length left - 1 do
-	  fields := (List.hd !l, sample_rec memo left.(i))::!fields;
-	  l := List.tl !l
-	done;
-	raise (FoundSampleRecord (oleft, List.rev !fields))
-    | (oright,right)::rights ->
-	let next = (oleft && (not oright)) in
-	if next then aux rights 
-	else
-	  for i = 0 to Array.length left - 1 do
-	    let back = left.(i) in
-	    let di = diff back right.(i) in
-	    if not (is_empty di) then (
-	      left.(i) <- diff back right.(i);
-	      aux rights;
-	      left.(i) <- back;
-	    )
-	  done
-  in
-  if exists (Array.length left) 
-    (fun i -> is_empty left.(i)) then raise Not_found;
-  try aux rights; raise Not_found
-  with FoundSampleRecord (o,r) -> (o,r)
-
-	    
-
-
-    
-  let get x = try sample_rec DescrSet.empty x with Not_found -> Other
-
-  let rec print_sep f sep ppf = function
-    | [] -> ()
-    | [x] -> f ppf x
-    | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
-
-  let rec is_seq = function
-    | Atom a -> a == Print.nil_atom
-    | Pair (_,y) -> is_seq y
-    | _ -> false
-
-  let rec print ppf s = 
-    if is_seq s then
-      Format.fprintf ppf "@[[@ %a]@]" print_seq s
-    else match s with
-    | Int i -> Intervals.print_v ppf i
-    | Atom a -> Atoms.print_v ppf a
-    | Char c -> Chars.print_v ppf c
-    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
-    | Xml (Atom tag, Pair (Record (o,r), child)) -> 
-	Format.fprintf ppf "<%a%a>%a" Utf8.print (Atoms.value tag) print_rec r 
-	print child
-    | Xml (Atom tag, Pair (attr, child)) -> 
-	Format.fprintf ppf "<%a %a>%a"  Utf8.print (Atoms.value tag) print attr print child
-    | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
-    | Record (o,r) ->
-	Format.fprintf ppf "{%a%s }"
-	  print_rec r
-	  (if o then "; ..." else "")
-    | Fun iface ->
-	Format.fprintf ppf "(fun ( %a ) x -> ...)"
-	  (print_sep
-	     (fun ppf (t1,t2) ->
-		Format.fprintf ppf "%a -> %a; "
-		Print.print (descr t1) Print.print (descr t2)
-	     )
-	     " ; "
-	  ) iface
-    | Other ->
-	Format.fprintf ppf "[cannot determine value]"
-  and print_rec ppf r = 
-    print_sep 
-      (fun ppf (l,x) -> 
-	 Format.fprintf ppf " %a = %a"
-	 Utf8.print
-	 (LabelPool.value l)
-	 print x
-      )
-      " ;" ppf r
-  and print_seq ppf = function
-    | Pair(x,y) -> print ppf x; Format.fprintf ppf "@ "; print_seq ppf y
-    | _ -> ()
-end
-
-
-
-
-
-
 let memo_normalize = ref DescrMap.empty
 
 
@@ -1515,7 +1373,7 @@ let normalize n =
 
 module Arrow =
 struct
-  let check_simple left s1 s2 =
+  let check_simple left (s1,s2) =
     let rec aux accu1 accu2 = function
       | (t1,t2)::left ->
           let accu1' = diff_t accu1 t1 in
@@ -1527,6 +1385,15 @@ struct
     let accu1 = descr s1 in
     (is_empty accu1) ||
     (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
+
+  let check_line_non_empty (left,right) =
+    not (List.exists (check_simple left) right)
+
+  let sample t =
+    let (left,right) = List.find check_line_non_empty (BoolPair.get t.arrow) in
+    List.fold_left (fun accu (t,s) -> cap accu (arrow t s)) 
+      { empty with arrow = any.arrow } left
+	
       
   let check_strenghten t s =
 (*
@@ -1571,15 +1438,12 @@ struct
   let get t =
     List.fold_left
       (fun ((dom,arr) as accu) (left,right) ->
-	 if Sample.check_empty_arrow_line left right 
-	 then accu
-	 else (
-	   let left =
-	     List.map 
-	       (fun (t,s) -> (descr t, descr s)) left in
+	 if check_line_non_empty (left,right)
+	 then
+	   let left = List.map (fun (t,s) -> (descr t, descr s)) left in
 	   let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
 	   (cap dom d, left :: arr)
-	 )
+	 else accu
       )
       (any, [])
       (BoolPair.get t.arrow)
@@ -1627,17 +1491,18 @@ end
 module Int = struct
   let has_int d i = Intervals.contains i d.ints
   let get d = d.ints
-  let any = { empty with ints = Intervals.any }
+  let any = { empty with ints = any.ints }
 end
 
 module Atom = struct
   let has_atom d a = Atoms.contains a d.atoms
   let get d = d.atoms
+  let any = { empty with atoms = any.atoms }
 end
 
 module Char = struct
   let has_char d c = Chars.contains c d.chars
   let is_empty d = Chars.is_empty d.chars
   let get d = d.chars
-  let any = { empty with chars = Chars.any }
+  let any = { empty with chars = any.chars }
 end

types/types.mli

@@ -29,6 +29,7 @@ val compare_descr: descr -> descr -> int
 module DescrHash: Hashtbl.S with type key = descr
 module DescrSList: SortedList.S with type 'a elem = descr
 module DescrMap: Map.S with type key = descr
+module DescrSet: Set.S with type elt = descr