Skip to content

GitLab

Commit 7cedb6e8 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Migrate to the new type substitution API (2/3).

parent 3a1e73e5
Hide whitespace changes
Inline Side-by-side
Showing with 359 additions and 114 deletions
types/boolVar.ml
View file @ 7cedb6e8
......@@ -219,8 +219,10 @@ module Make (T : E) : S with type s = T.t = struct
let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function
| `True -> full
| `True -> full
| `False -> empty
| `Split (_,`Atm x,`True,_,_) when T.equal x T.empty -> empty
| `Split (_,`Atm x,`True,_,_) when T.equal x T.full -> full
| `Split(_,x, p,i,n) ->
let x1 = atom x in
let p = cap x1 (aux p) in
......
types/types.ml
View file @ 7cedb6e8
......@@ -1748,16 +1748,17 @@ module Print = struct
trivial_pair d.arrow && trivial_rec d.record)
let worth_complement d =
let aux f x y = if f x y = 0 then 1 else 0 in
let dd = diff any d in
let aux x = if is_empty x then 1 else 0 in
let n =
aux BoolAtoms.compare d.atoms any.atoms +
aux BoolChars.compare d.chars any.chars +
aux BoolIntervals.compare d.ints any.ints +
aux BoolPair.compare d.times any.times +
aux BoolPair.compare d.xml any.xml +
aux BoolPair.compare d.arrow any.arrow +
aux BoolRec.compare d.record any.record +
aux BoolAbstracts.compare d.abstract any.abstract
aux { empty with atoms = dd.atoms } +
aux { empty with chars = dd.chars } +
aux { empty with ints = dd.ints } +
aux { empty with times = dd.times } +
aux { empty with xml = dd.xml } +
aux { empty with arrow = dd.arrow } +
aux { empty with record = dd.record } +
aux { empty with abstract = dd.abstract }
in
n >= 5
......@@ -2610,6 +2611,193 @@ let cond_partition univ qs =
in
List.fold_left add [ univ ] qs
module Iter =
struct
let any_node2 = any_node, any_node
let compute ~empty ~full ~cup ~cap ~diff ~var ~atom ~int ~char ~times ~xml ~arrow ~record ~abs ~opt t
=
let var_or f =
function `Atm a -> f a
| `Var v -> var v
in
let prod_bdd kind p =
let rects = Product.get ~kind
(if kind == `Normal then
{Descr.empty with times = BoolPair.atom (`Atm p) }
else {Descr.empty with xml = BoolPair.atom (`Atm p) })
in
List.fold_left
(fun acc (t1, t2) ->
let t1 = cons t1 and t2 = cons t2 in
cup acc (if kind == `Normal
then times (t1, t2) else xml (t1, t2))) empty rects
in
let record_bdd p =
Rec.compute ~empty ~full:(record (true,LabelMap.empty)) ~cup ~cap ~diff ~atom:record p
in
let any_atom = atom Atoms.full in
let any_int = int Intervals.full in
let any_char = char Chars.full in
let any_abs = abs Abstracts.full in
let any_times = prod_bdd `Normal Pair.full in
let any_xml = prod_bdd `XML Pair.full in
let any_record = record_bdd Rec.full in
let any_arrow = diff full
(List.fold_left cup any_atom
[ any_int; any_char; any_abs; any_times; any_xml; any_record ])
in
let arrow_bdd p =
Pair.compute ~empty ~full:any_arrow ~cup ~cap ~diff ~atom:arrow p
in
List.fold_left (fun acc e -> cup acc e)
(opt t.absent)
[ (BoolAtoms.compute
~empty ~full:any_atom ~cup ~cap ~diff ~atom:(var_or atom) t.atoms);
(BoolIntervals.compute
~empty ~full:any_int ~cup ~cap ~diff ~atom:(var_or int) t.ints);
(BoolChars.compute
~empty ~full:any_char ~cup ~cap ~diff ~atom:(var_or char) t.chars);
(BoolAbstracts.compute
~empty ~full:any_abs ~cup ~cap ~diff ~atom:(var_or abs) t.abstract);
(BoolPair.compute
~empty ~full:any_times ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Normal)) t.times);
(BoolPair.compute
~empty ~full:any_xml ~cup ~cap ~diff ~atom:(var_or (prod_bdd `XML)) t.xml);
(BoolPair.compute
~empty ~full:any_arrow ~cup ~cap ~diff ~atom:(var_or arrow_bdd) t.arrow);
(BoolRec.compute
~empty ~full:any_record ~cup ~cap ~diff ~atom:(var_or record_bdd) t.record);]
end
module Variable =
struct
type t = Var.t
let var_cache = DescrHash.create 17
let collect_vars t =
let memo = DescrHash.create 17 in
let union s1 s2 =
match s1, s2 with
Some s1, Some s2 -> Some (Var.Set.cup s1 s2)
| None, Some s | Some s, None -> Some s
| _ -> None
in
let inter s1 s2 =
match s1, s2 with
Some s1, Some s2 -> Some (Var.Set.cup s1 s2)
| _ -> None
in
let union3 (x1,y1,z1) (x2,y2,z2) =
union x1 x2, union y1 y2, union z1 z2
in
let inter3 (x1,y1,z1) (x2,y2,z2) =
inter x1 x2, inter y1 y2, inter z1 z2
in
let empty = Some Var.Set.empty in
let empty3 = empty,empty,empty in
let no3 = None, None, None in
let cst_empty3 _ = empty3 in
let rec loop t =
try
DescrHash.find memo t
with
Not_found ->
DescrHash.add memo t empty3;
let res =
Iter.compute
~empty:no3
~full:empty3
~cup:union3
~cap:inter3
~diff:(fun (x1,y1,z1) (x2, y2, z2) ->
inter x1 x2, inter y1 z2, inter z1 y2)
~var:(fun v -> let e = Some (Var.Set.singleton v) in
e,e,None)
~int:cst_empty3
~char:cst_empty3
~atom:cst_empty3
~abs:cst_empty3
~xml:prod
~times:prod
~arrow:arrow
~record:record
~opt:cst_empty3 t
in
DescrHash.replace memo t res;
res
and prod (t1, t2) =
let _,y1,z1 = loop (descr t1)
and _,y2,z2 = loop (descr t2) in
empty, union y1 y2, union z1 z2
and arrow (t1, t2) =
let _,y1,z1 = loop (descr t1)
and _,y2,z2 = loop (descr t2) in
empty, union z1 y2, union y1 z2
and record (b, lm) =
let _, y, z = List.fold_left (fun acc (_,t) ->
union3 acc (loop (descr t))) empty3 (LabelMap.get lm)
in
empty, y, z
in
loop t
let collect_vars t =
let extract = function Some e -> e | None -> Var.Set.empty in
try
DescrHash.find var_cache t
with Not_found ->
let tlv, pos, neg = collect_vars t in
let tlv, pos, neg = extract tlv, extract pos, extract neg in
let res = tlv, pos, neg, Var.Set.cup pos neg in
DescrHash.add var_cache t res;
res
let is_ground t =
let _, _, _, all = collect_vars t in
Var.Set.is_empty all
let no_var = is_ground
let all_tlv t =
let tlv, _, _, _ = collect_vars t in tlv
let has_tlv t = not (Var.Set.is_empty (all_tlv t))
let check_var =
let cache = DescrHash.create 17 in
let aux t =
let tlv, pos, neg, _ = collect_vars t in
match Var.Set.get tlv with
[] | _::_::_ -> `NotVar
| [ v ] ->
let is_pos = Var.Set.mem pos v
and is_neg = Var.Set.mem neg v in
assert (is_pos || is_neg);
if is_pos && is_neg then
(* this variable is positive and negative. It must
therefore be in a type of the form 'a&Int | Char\a *)
`NotVar
else if is_pos && equiv t (var v) then `Pos v
else if is_neg && equiv t (diff any (var v)) then `Neg v
else `NotVar
in
fun t ->
try DescrHash.find cache t with Not_found ->
let r = aux t in DescrHash.add cache t r; r
let is_var t = (check_var t) != `NotVar
let extract t =
match check_var t with
`Pos v -> v,true
| `Neg v -> v,false
| _ -> raise (Invalid_argument "Variable.extract")
let extract_variable = extract
end
module Positive = struct
module T = struct
type t = descr
......@@ -2673,30 +2861,41 @@ module Positive = struct
let printf = pp Format.std_formatter
let rec make_descr seen v =
if List.memq v seen then empty
else
let seen = v :: seen in
match v.def with
|`Type d -> d
|`Variable d -> var d
|`Cup vl -> List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
|`Cap vl -> List.fold_left (fun acc v -> cap acc (make_descr seen v)) any vl
|`Times (v1,v2) -> times (make_node v1) (make_node v2)
|`Arrow (v1,v2) -> arrow (make_node v1) (make_node v2)
|`Xml (v1,v2) -> xml (make_node v1) (make_node v2)
|`Record (b, flst) -> rec_of_list b (List.map (fun (b,l,v) -> (b,l,make_descr seen v)) flst)
|`Neg v -> neg (make_descr seen v)
and make_node v =
match v.node with
let solve_gen ?(stop_descr=(fun _ -> None)) ?(stop_node=(fun _ -> None)) v =
let rec make_descr seen v =
if List.memq v seen then empty else
let seen = v :: seen in
match stop_descr v with
Some t -> t
| None ->
match v.def with
| `Type d -> d
| `Variable d -> var d
| `Cup vl ->
List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
| `Cap vl ->
List.fold_left (fun acc v -> cap acc (make_descr seen v)) any vl
| `Times (v1,v2) -> times (make_node v1) (make_node v2)
| `Arrow (v1,v2) -> arrow (make_node v1) (make_node v2)
| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
| `Record (b, flst) -> rec_of_list b (List.map (fun (b,l,v) -> (b,l,make_descr seen v)) flst)
| `Neg v -> neg (make_descr seen v)
and make_node v =
match v.node with
| Some n -> n
| None ->
let n = make () in
v.node <- Some n;
let d = make_descr [] v in
define n d;
n
match stop_node v with
| Some t -> v.node <- Some t; t
| None -> let n = make () in
v.node <- Some n;
let d = make_descr [] v in
define n d;
n
in
internalize (make_node v)
let solve v = solve_gen v
(* We shadow the corresponding definitions in the outer module *)
let forward () = { def = `Cup []; node = None; descr = None}
......@@ -2705,8 +2904,31 @@ module Positive = struct
let ty d = cons (`Type d)
let var d = cons (`Variable d)
let neg v = cons (`Neg v)
let rec cup vl = cons (`Cup vl)
let cap vl = cons (`Cap vl)
let empty = ty empty
let any = ty any
let binop e f may_flat mk vl =
let has_f = ref false in
let vl = List.map (fun v ->
match may_flat v with
| Some vl -> vl
| None ->
if v == e then [] else if v == f then (has_f := true; [])
else [ v ]
) vl
in
if !has_f then f else
match List.concat vl with
[ v ] -> v
| vl -> mk vl
let cup = binop empty any
(function { def = `Cup (_::_ as vl) ; _ } -> Some vl | _ -> None)
(fun l -> cons (`Cup l))
let cap = binop any empty
(function { def = `Cap (_::_ as vl) ; _ } -> Some vl | _ -> None)
(fun l -> cons (`Cap l))
let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2))
let xml v1 v2 = cons (`Xml (v1,v2))
......@@ -2716,82 +2938,53 @@ module Positive = struct
let abstract a = ty (abstract a)
let record b vlst = cons (`Record (b, vlst))
let define v1 v2 = def v1 (`Cup [v2])
let diff v1 v2 = cap [v1 ; (neg v2)]
let decompose t =
let decompose ?(stop=(fun _ -> None)) t =
let memo = DescrHash.create 17 in
let decompose_conj f_atom sign ilist acc =
List.fold_left (fun acc e ->
let ne = f_atom e in
(sign ne) :: acc
) acc ilist
in
let decompose_dnf t_any f_atom dnf acc =
List.fold_left (fun acc (ipos, ineg) ->
let lacc = match ipos,ineg with
[],[] -> [t_any]
| _ -> []
in
let lacc = decompose_conj f_atom neg ineg lacc in
let lacc = decompose_conj f_atom (fun x -> x) ipos lacc in
match lacc with
| [] -> t_any::acc
| [v] -> v::acc
| l -> (cap l) :: acc) acc dnf
in
let or_var f = function
|`Var x -> var x
|`Atm a -> f a
let rec loop t =
let res =
try
DescrHash.find memo t
with
Not_found ->
let node_t = forward () in
let () = DescrHash.add memo t node_t in
let rhs =
match stop t with
| Some s -> s
| None -> loop_struct t
in
node_t.def <- (rhs).def; node_t
in
res.descr <- Some t; res
and loop_struct t =
Iter.compute ~empty:empty ~full:any
~cup:(fun v1 v2 -> cup [v1;v2])
~cap:(fun v1 v2 -> cap [v1;v2])
~diff:diff
~var ~int:interval ~char ~atom ~abs:abstract
~xml:(fun (t1, t2) -> xml (loop (descr t1)) (loop (descr t2)))
~times:(fun (t1, t2) -> times (loop (descr t1)) (loop (descr t2)))
~arrow:(fun (t1, t2) -> arrow (loop (descr t1)) (loop (descr t2)))
~record:(fun (b, lm) -> record b (List.map (fun (l,t) ->
let t = descr t in
t.absent, l, loop t) (LabelMap.get lm)))
~opt:(function true -> ty Record.absent | _ -> empty) t
in
let decompose_kind any make dnf acc =
decompose_dnf (ty any) (or_var make) dnf acc
loop t
let decompose t =
let res = decompose
~stop:(fun x -> if Variable.no_var x then Some (ty x) else
if Variable.is_var t then
let v, p = extract_variable t in
Some (if p then var v else neg (var v))
else None)
t
in
let rec decompose_bdd any make dnf acc =
decompose_kind any (fun bdd ->
cup (decompose_dnf (ty any) (fun (x,y) ->
let x = descr x
and y = descr y in
make
(decompose_type x)
(decompose_type y)
) (Pair.get bdd) [])) dnf acc
and format_rec b acc = function
| (l, t) :: rest -> format_rec b (acc @ [b, l, decompose_type (descr t)]) rest
| [] -> acc
and decompose_rec any make dnf acc =
decompose_kind any (fun bdd ->
cup (decompose_dnf (ty any) (fun (b, l) ->
make b (format_rec b [] (LabelMap.get l))) (Rec.get bdd) [])) dnf acc
and decompose_type t =
try DescrHash.find memo t
with Not_found ->
let res =
if no_var t then ty t
else
match check_var t with
`Pos v -> var v
| `Neg v -> neg (var v)
| `NotVar ->
let node_t = forward () in
let () = DescrHash.add memo t node_t in
let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
@@ decompose_kind Int.any interval (BoolIntervals.get t.ints)
@@ decompose_kind Char.any char (BoolChars.get t.chars)
@@ decompose_bdd Product.any times (BoolPair.get t.times)
@@ decompose_bdd Product.any_xml xml (BoolPair.get t.xml)
@@ decompose_bdd Arrow.any arrow (BoolPair.get t.arrow)
@@ decompose_rec Record.any record (BoolRec.get t.record)
@@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
in
node_t.def <- (cup descr_t).def; node_t
in res.descr <- Some t; res
in
decompose_type t
res
let solve v = internalize (make_node v)
(* [map_var f v] applies returns the type
[v{ 'a <- f 'a}] for all ['a] in [v]
*)
let map_var subst v =
let memo = MemoHash.create 17 in
let rec aux v subst =
......@@ -2802,7 +2995,6 @@ module Positive = struct
let new_v =
match v.def with
|`Type d -> `Type d
(* |`Variable d when Var.Set.mem d delta -> v.def *)
|`Variable d -> (subst d).def
|`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl)
|`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl)
......@@ -2985,7 +3177,6 @@ module Substitution =
struct
module Map = Var.Set.Map
type t = Descr.t Map.map
type order = int Map.map
let identity = Map.empty
......@@ -3009,6 +3200,12 @@ struct
end)
let global_memo = Memo.create 17
let app_subst2 v subst =
Positive.solve_gen ~stop_descr:(fun v ->
match v.Positive.def with
`Variable d -> (try Some (Map.assoc d subst) with Not_found -> None)
| _ -> None) v
let rec app_subst ?(after = (fun x -> x)) ?(do_var= fun x -> Positive.ty x) t subst =
let open Positive in
if subst == identity then descr (solve t) else
......@@ -3089,7 +3286,8 @@ struct
let full t l =
if no_var t then t else
app_subst (Positive.decompose t) (of_list l)
descr (app_subst2 (Positive.decompose t) (of_list l))
(*app_subst (Positive.decompose t) (of_list l) *)
let single t s = full t [s]
......@@ -3097,8 +3295,53 @@ struct
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.fresh v)) vars in
app_subst (Positive.decompose t) subst
(*descr (apply_subst2 t subst) *)
descr (app_subst2 (Positive.decompose t) subst)
let kind delta k t =
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.set_kind k v)) vars in
descr (app_subst2 (Positive.decompose t) subst)
let solve_rectype t alpha =
let x = make () in
let n = Positive.solve_gen ~stop_node:(fun v -> match v.Positive.def with
| `Variable d when Var.equal d alpha -> Some x
| _ -> None) (Positive.decompose t)
in
define x (descr n);
descr x
let clean_type delta t =
if no_var t then t else
let _,pos, neg, all = Variable.collect_vars t in
let vars = Var.Set.diff all delta in
if Var.Set.is_empty vars then t else
let idx = ref 0 in
let rec freshvar () =
let rec pretty i acc =
let ni,nm = i/26, i mod 26 in
let acc = acc ^
(String.make 1 (OldChar.chr (OldChar.code 'a' + nm)))
in
if ni == 0 then acc else pretty ni acc
in
let x = Var.mk (pretty !idx "") in
if Var.Set.mem delta x then
(* if the name is taken by a variable in delta, restart *)
(incr idx; freshvar ())
else x
in
let subst = Map.init
(fun v ->
let is_pos = Var.Set.mem pos v in
let is_neg = Var.Set.mem neg v in
if is_pos && is_neg then var (freshvar ())
else if is_pos then empty else any
) vars
in
descr (app_subst2 (Positive.decompose t) subst)
end
......@@ -3639,7 +3882,7 @@ module Tallying = struct
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* solve_rectype remove also all previously introduced fresh variables *)
let x = Positive.solve_rectype t alpha in
let x = Substitution.solve_rectype t alpha in
(* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
let es =
CS.E.fold (fun beta s acc ->
......@@ -3800,8 +4043,8 @@ exception FoundApply of t * int * int * Tallying.CS.sl
let apply_raw delta s t =
Tallying.NormMemoHash.clear Tallying.memo_norm;
let s = Positive.substitute_kind delta Var.function_kind s in
let t = Positive.substitute_kind delta Var.argument_kind t in
let s = Substitution.kind delta Var.function_kind s in
let t = Substitution.kind delta Var.argument_kind t in
let vgamma = Var.mk "Gamma" in
let gamma = var vgamma in
let cgamma = cons gamma in
......@@ -3814,7 +4057,7 @@ let apply_raw delta s t =
let t = arrow (cons (get aj j)) cgamma in
let sl = Tallying.tallying delta [ (s,t) ] in
let new_res =
Positive.clean_type delta (
Substitution.clean_type delta (
List.fold_left (fun tacc si ->
cap tacc (Tallying.(gamma >> si))
) any sl
......
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