Commit 045a8519 authored by Pietro Abate's avatar Pietro Abate
Browse files

Make distinction between (A ^ Int) and A in TLV

parent ff65c47f
......@@ -142,18 +142,19 @@ module TLV = struct
module Set = struct
include Set.Make(
struct
type t = (Var.var * bool)
let compare (v1,p1) (v2,p2) =
(* Var * polarity * if the variable is present in all kinds *)
type t = (Var.var * bool * bool)
let compare (v1,p1,b1) (v2,p2,b2) =
let c = Var.compare v1 v2 in
if c == 0 then
if p1 == p2 then 0
if p1 == p2 && b1 = b2 then 0
else if p1 then 1 else -1
else c
end)
let pp_aux ppf pp_elem s =
let f ppf = function
|(v,true) -> Format.fprintf ppf "%a" pp_elem v
|(v,false) -> Format.fprintf ppf "~ %a" pp_elem v
|(v,true,_) -> Format.fprintf ppf "%a" pp_elem v
|(v,false,_) -> Format.fprintf ppf "~ %a" pp_elem v
in
Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s)
let dump ppf s = pp_aux ppf Var.dump s
......@@ -164,37 +165,42 @@ module TLV = struct
(* tlv : top level variables
* fv : all free variables in the subtree *)
type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool }
type t = { tlv : Set.t ; fv : Var.Set.t }
let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let empty = { tlv = Set.empty ; fv = Var.Set.empty}
let any = { tlv = Set.empty ; fv = Var.Set.empty}
let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true }
let singleton (v,p) = { tlv = Set.singleton (v,p,true); fv = Var.Set.singleton v}
(* return the max of top level variables *)
let max x = Set.max_elt x.tlv
let max x = let (v,p,_) = Set.max_elt x.tlv in (v,p)
let pair x y = {
tlv = Set.empty ;
fv = Var.Set.union x.fv y.fv ;
isvar = false
fv = Var.Set.union x.fv y.fv
}
let record x = {
tlv = Set.empty ;
fv = x.fv ;
isvar = false
fv = x.fv
}
(* true if it contains only one variable *)
let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1)
let is_single t =
let (tlvsolo,tlvmix) = Set.partition (fun (_,_,b) -> b) x.tlv in
(Set.cardinal tlvsolo = 1) &&
(Var.Set.cardinal t.fv = 1) &&
(Set.cardinal tlvmix = 0)
let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0)
let has_toplevel t = Set.cardinal t.tlv > 0
let pp ppf x = Set.pp ppf x.tlv
let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv
let dump ppf x =
let (tlvsolo,tlvmix) = Set.partition (fun (_,_,b) -> b) x.tlv in
Format.fprintf ppf "<fv = %a ; tlv(mix) = %a ; tlv(solo) = %a>"
Var.Set.dump x.fv Set.dump tlvsolo Set.dump tlvmix
let printf = pp Format.std_formatter
let mem v x = Set.mem v x.tlv
......@@ -481,13 +487,13 @@ let update_tlv x y t =
List.fold_left (fun acc (p,n) ->
let acc1 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,true))
|(`Var v) as x -> Set.union acc (Set.singleton (x,true,true))
|_ -> acc
) Set.empty p
in
let acc2 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,false))
|(`Var v) as x -> Set.union acc (Set.singleton (x,false,true))
|_ -> assert false
) acc1 n
in acc2::acc
......@@ -498,22 +504,32 @@ let update_tlv x y t =
|[h] -> h
|h::l -> List.fold_left Set.union h l
in
List.fold_left Set.union
(aux BoolChars.get t.chars)
[
let vars = [
(aux BoolChars.get t.chars)
(aux BoolIntervals.get t.ints);
(aux BoolAtoms.get t.atoms);
(aux BoolPair.get t.arrow);
(aux BoolPair.get t.xml);
(aux BoolRec.get t.record)
]
(aux BoolRec.get t.record) ]
in
let (union,inter) =
let rec aux (union,inter) = function
|[] -> (union,inter)
|h :: t -> aux ((Set.union h union),(Set.inter h inter)) t
in
match vars with
|[] -> (Set.empty.Set.empty)
|h::t -> aux (h,h) t
in
let tlvmix = Set.fold (fun (v,p,_) -> (v,p,false)) (Set.diff union inter) in
let tlvsolo = inter in
Set.union tlvsolo tlvmix
in
let fv t =
if Descr.is_empty t || equal t Descr.any then Var.Set.empty
else Var.Set.union x.toplvars.fv y.toplvars.fv
in
let toplvars = { tlv = tlv t ; fv = fv t ; isvar = t.toplvars.isvar } in
{ t with toplvars = toplvars }
{ t with toplvars = { tlv = tlv t ; fv = fv t} }
;;
let char c = { empty with chars = BoolChars.atom (`Atm c) }
......@@ -543,8 +559,7 @@ let cup x y =
absent= x.absent || y.absent;
toplvars = TLV.empty
} in
let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
update_tlv x y t
let cap x y =
if x == y then x else
......@@ -560,8 +575,7 @@ let cap x y =
absent= x.absent && y.absent;
toplvars = TLV.empty
} in
let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
update_tlv x y t
let diff x y =
if x == y then empty else
......@@ -577,8 +591,7 @@ let diff x y =
absent= x.absent && not y.absent;
toplvars = TLV.empty
} in
let isvar = (equal x any && is_var y) || (is_var x && equal y empty) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
update_tlv x y t
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
......
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