Commit 85562d51 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2002-11-25 23:59:50 by cvscast] Empty log message

Original author: cvscast
Date: 2002-11-26 00:00:47+00:00
parent bd299ba7
...@@ -787,6 +787,7 @@ end ...@@ -787,6 +787,7 @@ end
module Sample = module Sample =
struct struct
let rec find f = function let rec find f = function
| [] -> raise Not_found | [] -> raise Not_found
| x::r -> try f x with Not_found -> find f r | x::r -> try f x with Not_found -> find f r
...@@ -800,6 +801,7 @@ type t = ...@@ -800,6 +801,7 @@ type t =
| Record of (label * t) list | Record of (label * t) list
| Fun of (node * node) list | Fun of (node * node) list
| Other | Other
exception FoundSampleRecord of (label * t) list
let rec sample_rec memo d = let rec sample_rec memo d =
if (Assumptions.mem d memo) || (is_empty d) then raise Not_found if (Assumptions.mem d memo) || (is_empty d) then raise Not_found
...@@ -824,6 +826,8 @@ and sample_rec_times memo c = ...@@ -824,6 +826,8 @@ and sample_rec_times memo c =
and sample_rec_times_aux memo (left,right) = and sample_rec_times_aux memo (left,right) =
let rec aux accu1 accu2 = function let rec aux accu1 accu2 = function
| (t1,t2)::right -> | (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 let accu1' = diff_t accu1 t1 in
if non_empty accu1' then aux accu1' accu2 right else if non_empty accu1' then aux accu1' accu2 right else
let accu2' = diff_t accu2 t2 in let accu2' = diff_t accu2 t2 in
...@@ -862,16 +866,42 @@ and sample_rec_arrow_aux (left,right) = ...@@ -862,16 +866,42 @@ and sample_rec_arrow_aux (left,right) =
and sample_rec_record memo c = and sample_rec_record memo c =
Record (find (sample_rec_record_aux memo) (get_record c)) Record (find (sample_rec_record_aux memo) (get_record c))
and sample_rec_record_aux memo fields = and sample_rec_record_aux memo (labels,(oleft,(left_opt,left)),rights) =
[] let rec aux = function
(*TODO*) | [] ->
(* let l = ref labels and fields = ref [] in
raise Not_found for i = 0 to Array.length left - 1 do
*) if not left_opt.(i) then
(* fields := (List.hd !l, sample_rec memo left.(i))::!fields;
let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in l := List.tl !l
List.fold_left aux [] fields done;
*) raise (FoundSampleRecord (List.rev !fields))
| (oright,(right_opt,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 oback = left_opt.(i) in
let odi = oback && (not right_opt.(i)) in
let di = diff back right.(i) in
if odi || not (is_empty di) then (
left.(i) <- diff back right.(i);
left_opt.(i) <- odi;
aux rights;
left.(i) <- back;
left_opt.(i) <- oback;
)
done
in
if exists (Array.length left)
(fun i -> not left_opt.(i) && (is_empty left.(i))) then raise Not_found;
try aux rights; raise Not_found
with FoundSampleRecord r -> r
let get x = try sample_rec Assumptions.empty x with Not_found -> Other let get x = try sample_rec Assumptions.empty x with Not_found -> Other
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment