Commit 604ee153 authored by Pietro Abate's avatar Pietro Abate
Browse files

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

Original author: cvscast
Date: 2003-05-24 19:31:53+00:00
parent cce87dd2
......@@ -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 \
\
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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)
]
];
......
......@@ -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
......
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
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
......@@ -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