| 2 |
open Printf |
open Printf |
| 3 |
|
|
| 4 |
|
|
| 5 |
|
let map_sort f l = |
| 6 |
|
SortedList.from_list (List.map f l) |
| 7 |
|
|
| 8 |
type label = int |
type label = int |
| 9 |
type atom = int |
type atom = int |
| 662 |
let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in |
let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in |
| 663 |
List.filter line (get_record d.record) |
List.filter line (get_record d.record) |
| 664 |
|
|
|
|
|
| 665 |
let restrict_label_present t l = |
let restrict_label_present t l = |
| 666 |
let restr = function |
let restr = function |
| 667 |
| (true, d) -> if non_empty d then (false,d) else raise Exit |
| (true, d) -> if non_empty d then (false,d) else raise Exit |
| 707 |
match (n, r) with |
match (n, r) with |
| 708 |
| (`Success, _) | (_, []) -> `Success |
| (`Success, _) | (_, []) -> `Success |
| 709 |
| (`Fail, r) -> |
| (`Fail, r) -> |
| 710 |
let aux (l,(o,t)) n = `Label (l, [t,n], if o then n else `Fail) in |
let aux (l,(o,t)) n = |
| 711 |
|
`Label (l, [t,n], if o then n else `Fail) in |
| 712 |
List.fold_right aux r `Success |
List.fold_right aux r `Success |
| 713 |
| (`Label (l1,present,absent), (l2,(o,t2))::r') -> |
| (`Label (l1,present,absent), (l2,(o,t2))::r') -> |
| 714 |
if (l1 < l2) then |
if (l1 < l2) then |
| 715 |
let pr = List.map (fun (t,x) -> (t, merge_record x r)) present in |
let pr = List.map (fun (t,x) -> (t, merge_record x r)) present in |
| 716 |
|
let t = List.fold_left (fun a (t,_) -> diff a t) any present in |
| 717 |
|
let pr = |
| 718 |
|
if non_empty t then (t, merge_record `Fail r) :: pr |
| 719 |
|
else pr in |
| 720 |
`Label (l1,pr,merge_record absent r) |
`Label (l1,pr,merge_record absent r) |
| 721 |
else if (l2 < l1) then |
else if (l2 < l1) then |
| 722 |
let n' = merge_record n r' in |
let n' = merge_record n r' in |
| 737 |
let abs = if o then merge_record absent r' else absent in |
let abs = if o then merge_record absent r' else absent in |
| 738 |
`Label (l1, !res, abs) |
`Label (l1, !res, abs) |
| 739 |
|
|
| 740 |
|
module Unify = Map.Make(struct type t = normal let compare = compare end) |
| 741 |
|
|
| 742 |
|
let repository = ref Unify.empty |
| 743 |
|
|
| 744 |
|
let rec canonize = function |
| 745 |
|
| `Label (l,pr,ab) as x -> |
| 746 |
|
(try Unify.find x !repository |
| 747 |
|
with Not_found -> |
| 748 |
|
let pr = List.map (fun (t,n) -> canonize n,t) pr in |
| 749 |
|
let pr = SortedMap.from_list cup pr in |
| 750 |
|
let pr = List.map (fun (n,t) -> (t,n)) pr in |
| 751 |
|
let x = `Label (l, pr, canonize ab) in |
| 752 |
|
try Unify.find x !repository |
| 753 |
|
with Not_found -> repository := Unify.add x x !repository; x |
| 754 |
|
) |
| 755 |
|
| x -> x |
| 756 |
|
|
| 757 |
let normal d = |
let normal d = |
| 758 |
List.fold_left merge_record `Fail (get d) |
let r = canonize (List.fold_left merge_record `Fail (get d)) in |
| 759 |
|
repository := Unify.empty; |
| 760 |
|
r |
| 761 |
|
|
| 762 |
|
type normal' = |
| 763 |
|
[ `Success |
| 764 |
|
| `Label of label * (descr * descr) list * descr option ] option |
| 765 |
|
|
| 766 |
|
(* NOTE: this function relies on the fact that generic order |
| 767 |
|
makes smallest labels appear first *) |
| 768 |
|
|
| 769 |
|
let first_label d = |
| 770 |
|
let d = d.record in |
| 771 |
|
let min = ref None in |
| 772 |
|
let lab (l,o,t) = match !min with |
| 773 |
|
| Some l' when l >= l' -> () |
| 774 |
|
| _ -> if o && (descr t = any) then () else min := Some l in |
| 775 |
|
let line (p,n) = |
| 776 |
|
(match p with f::_ -> lab f | _ -> ()); |
| 777 |
|
(match n with f::_ -> lab f | _ -> ()) in |
| 778 |
|
List.iter line d; |
| 779 |
|
match !min with |
| 780 |
|
| None -> if d = [] then `Empty else `Any |
| 781 |
|
| Some l -> `Label l |
| 782 |
|
|
| 783 |
|
let normal' (d : descr) l = |
| 784 |
|
let ab = ref empty in |
| 785 |
|
let rec extract f = function |
| 786 |
|
| (l',o,t) :: rem when l = l' -> |
| 787 |
|
f o (descr t); extract f rem |
| 788 |
|
| x :: rem -> x :: (extract f rem) |
| 789 |
|
| [] -> [] in |
| 790 |
|
let line (p,n) = |
| 791 |
|
let ao = ref true and ad = ref any in |
| 792 |
|
let p = |
| 793 |
|
extract (fun o d -> ao := !ao && o; ad := cap !ad d) p |
| 794 |
|
and n = |
| 795 |
|
extract (fun o d -> ao := !ao && not o; ad := diff !ad d) n |
| 796 |
|
in |
| 797 |
|
(* Note: p and n are still sorted *) |
| 798 |
|
let d = { empty with record = [(p,n)] } in |
| 799 |
|
if !ao then ab := cup d !ab; |
| 800 |
|
(!ad, d) in |
| 801 |
|
let pr = List.map line d.record in |
| 802 |
|
let pr = Product.normal_aux pr in |
| 803 |
|
let ab = if is_empty !ab then None else Some !ab in |
| 804 |
|
(pr, ab) |
| 805 |
|
|
| 806 |
|
|
| 807 |
let any = { empty with record = any.record } |
let any = { empty with record = any.record } |
| 808 |
let is_empty d = d = [] |
let is_empty d = d = [] |
| 809 |
|
let descr l = |
| 810 |
|
let line l = map_sort (fun (l,(o,d)) -> (l,o,cons d)) l, [] in |
| 811 |
|
{ empty with record = map_sort line l } |
| 812 |
end |
end |
| 813 |
|
|
| 814 |
|
|
| 815 |
|
|
| 816 |
let memo_normalize = ref DescrMap.empty |
let memo_normalize = ref DescrMap.empty |
| 817 |
|
|
|
let map_sort f l = |
|
|
SortedList.from_list (List.map f l) |
|
| 818 |
|
|
| 819 |
let rec rec_normalize d = |
let rec rec_normalize d = |
| 820 |
try DescrMap.find d !memo_normalize |
try DescrMap.find d !memo_normalize |