Commit 43dca83a authored by Pietro Abate's avatar Pietro Abate
Browse files

More bug fix and add norm function for record type

parent 4ff5f78b
......@@ -879,9 +879,11 @@ and check_record (labels,(oleft,left),rights) s =
| [] -> assert (i == Array.length ws); w
| l::labs ->
let w = match ws.(i) with
| Witness.WAbsent -> w
| wl -> LabelMap.add l wl w in
aux w (succ i) labs in
| Witness.WAbsent -> w
| wl -> LabelMap.add l wl w
in
aux w (succ i) labs
in
set s (Witness.wrecord (aux LabelMap.empty 0 labels) oleft)
| (false,_) :: rest when oleft -> aux ws accus seen rest
| (_,f) :: rest
......@@ -2301,6 +2303,10 @@ module Tallying = struct
let single_times = single_aux (fun p -> { empty with times = BoolPair.atom (`Atm p) })
let single_xml = single_aux (fun p -> { empty with xml = BoolPair.atom (`Atm p) })
let single_record = single_aux (fun p -> { empty with record = BoolRec.atom (`Atm p) })
let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })
(* check if there exists a toplevel varaible : fun (pos,neg) *)
......@@ -2342,10 +2348,8 @@ module Tallying = struct
let accu = aux_base single_chars normchars accu (BoolChars.get t.chars) in
let accu = aux_base single_ints normints accu (BoolIntervals.get t.ints) in
let accu = aux_base single_times normpair accu (BoolPair.get t.times) in
let accu = aux_base single_times normpair accu (BoolPair.get t.xml) in
(*
let accu = aux_base accu subrecord (BoolRec.get d.record) in
*)
let accu = aux_base single_xml normpair accu (BoolPair.get t.xml) in
let accu = aux_base single_record normrec accu (BoolRec.get t.record) in
let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
accu
with UnSatConstr -> CS.unsat
......@@ -2361,6 +2365,7 @@ module Tallying = struct
* [t2\s2] ^ prod'(t1,t2\s2,n)
* *)
and normpair ( (t,mem) : (BoolPair.s * DescrSet.t) ) =
(* this should be called with xml !!! *)
let mem = DescrSet.add { empty with times = BoolPair.atom (`Atm t) } mem in
let norm_prod pos neg =
let rec aux (t1 : s) (t2 : s ) = function
......@@ -2385,6 +2390,26 @@ module Tallying = struct
in
List.fold_left (fun acc (p,n) -> CS.cap acc (norm_prod p n)) CS.sat (Pair.get t)
and normrec ( (t,mem) : (BoolRec.s * DescrSet.t) ) =
let mem = DescrSet.add { empty with record = BoolRec.atom (`Atm t) } mem in
let norm_rec ((oleft,left),rights) =
let rec aux accus seen = function
|[] -> CS.S.empty
|(false,_) :: rest when oleft -> aux accus seen rest
|(b,field) :: rest ->
let right = seen @ rest in
snd (Array.fold_left (fun (i,acc) t ->
let di = diff accus.(i) t in
let accus' = Array.copy accus in accus'.(i) <- di ;
(i+1,CS.cap acc (CS.cap (norm (di,mem)) (aux accus' [] right)))
) (0,CS.S.empty) field
)
in
let c = Array.fold_left (fun acc t -> CS.cap (norm (t,mem)) acc) CS.S.empty left in
CS.cap (aux left [] rights) c
in
List.fold_left (fun acc (_,p,n) -> CS.cap acc (norm_rec (p,n))) CS.S.empty (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] ^ arrow'(t1,any \\ t2,p)
* arrow'(t1,acc,p) =
([t1\s1] ^ arrow'(t1\s1,acc,p)) v
......
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