Commit 3f63d285 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Fix typing of application and optimize the code:

- fix a bug in Positive.decompose that was introducing components that were not
in the original type
- rewrite Positive.decompose to flatten long chains of `Cup [`Cup[`Cup ...]]
- rewrite apply_raw to perform the correct dove-tail exploration of the branches
- rewrite Positive.clean_type to perform substitution of {co,contra}-variant only
variables and internal variable beautification at the same time
- For the moment, only call Positive.clean_type at the very end, before returning the result type. Need to investigate if intermediate results would benefit from having less variables.
parent 28b75cf5
......@@ -2354,7 +2354,6 @@ struct
|`Record of bool * (bool * Ns.Label.t * v) list
]
and v = { mutable def : rhs; mutable node : node option }
let rec make_descr seen v =
if List.memq v seen then empty
else
......@@ -2379,112 +2378,100 @@ struct
let d = make_descr [] v in
define n d;
n
(* Kim: We shadow the corresponding definitions in the outer module *)
let forward () = { def = `Cup []; node = None }
let def v d = v.def <- d
let cons d = let v = forward () in def v d; v
let ty d = cons (`Type d)
let var d = cons (`Variable d)
let neg v = cons (`Neg v)
let cup vl = cons (`Cup vl)
let cup = function [ v ] -> v | vl -> cons (`Cup vl)
let cap vl = cons (`Cap vl)
let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2))
let xml v1 v2 = cons (`Xml (v1,v2))
let interval i = ty (interval i)
let char c = ty (char c)
let atom a = ty (atom a)
let record b vlst = cons (`Record (b, vlst))
let define v1 v2 = def v1 (`Cup [v2])
let decompose t =
let memo_decompose = DescrHash.create 17 in
let rec decompose t =
let _decompose_records t =
let rec_list = Record.get t in
cup (List.map (fun (map,op,_) ->
record op
(List.map (fun (lab,(pres,t)) ->
(pres,lab, decompose t))
(Ident.LabelMap.get map))
) rec_list)
in
let aux_bdd ?noderec constr (p,n) =
let aux polarity constr l =
cap (
List.map ( function
|`Var v -> (polarity(var (`Var v)))
|`Atm bdd ->
match noderec with
|None -> (polarity(ty (constr bdd)))
|Some g -> polarity(g bdd)
) l
)
in
cap [(aux (fun x -> x) constr p);(aux neg constr n)]
in
(* constr : times, arrow, xml *)
let subpairs (constr : v -> v -> v) bdd =
cup (
List.map (fun (left,rigth) ->
let deep polarity l =
cap (
List.map (fun (t1,t2) ->
let d1 = decompose (descr t1) in
let d2 = decompose (descr t2) in
polarity(constr d1 d2)
) l
)
let decompose 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) ->
match
decompose_conj f_atom neg ineg
@@ decompose_conj f_atom (fun x -> x) ipos [t_any]
with
| [v] -> v::acc
| l -> (cap l) :: acc) acc dnf
in
let or_var f e =
match e with
(`Var _) as v -> var v
| `Atm a -> f a
in
let decompose_kind any make dnf acc =
decompose_dnf (ty any) (or_var make) dnf acc
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 decompose_type t =
try
DescrHash.find memo t
with
Not_found ->
let node_t = forward () in
if no_var t then ty t
else
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)
@@ Record.(if has_absent t then [ty absent] else [])
in
cap [(deep (fun x -> x) left);(deep neg rigth)]
) (Pair.get bdd)
)
in
let decompose_aux ?noderec constr l =
cup (List.map (fun (p,n) -> (aux_bdd ?noderec constr (p,n))) l)
in
(*begin match DescrHash.find memo_decompose t with | None -> forward () | Some s -> s end *)
try DescrHash.find memo_decompose t with Not_found -> begin
let node_s = forward () in
DescrHash.add memo_decompose t node_s;
let s =
if no_var t then ty t else
cup [
decompose_aux atom (BoolAtoms.get t.atoms);
decompose_aux interval (BoolIntervals.get t.ints);
decompose_aux char (BoolChars.get t.chars);
(* XXX XXX record is not threated here yet !!! *)
decompose_aux ~noderec:(subpairs arrow)
(fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) (BoolPair.get t.arrow);
decompose_aux ~noderec:(subpairs xml)
(fun p -> { empty with xml = BoolPair.atom (`Atm p) }) (BoolPair.get t.xml);
decompose_aux ~noderec:(subpairs times)
(fun p -> { empty with times = BoolPair.atom (`Atm p) }) (BoolPair.get t.times);
(* Kim: Not sure how to reuse the above to decompose
records, so I'm adding my version here: *)
(* Kim: Not working at the moment, seems variables
are not propagated properly in records *)
(* _decompose_records { empty with record = t.record };*)
]
in
define node_s s; node_s
end
node_t.def <- (cup descr_t).def; node_t
in
DescrHash.clear memo_decompose;
decompose t
decompose_type t
let solve v = internalize (make_node v)
module MemoHash = Hashtbl.Make(
struct
type t = v
let hash = Hashtbl.hash
let equal u v = u == v
end )
let substitute_aux v subst =
(* XXX do I really need memo here XXX *)
(* Kim: yes we do, see solve above. We use a list and memq since we rely on pointer identity
for cycles. *)
let memo = ref [] in
let memo = MemoHash.create 17 in
let rec aux v subst =
try
List.assq v !memo
MemoHash.find memo v
with
Not_found -> begin
let node_v = forward () in
memo := (v, node_v) :: !memo;
MemoHash.add memo v node_v;
let new_v =
match v.def with
|`Type d -> `Type d
......@@ -2505,6 +2492,59 @@ struct
in
aux v subst
let print ppf v =
let id = ref 0 in
let memo = MemoHash.create 17 in
let rec aux v =
try
let s = MemoHash.find memo v in
Format.fprintf ppf "%s" s
with
Not_found -> begin
let node_name = Printf.sprintf "X_%i" !id in
incr id;
(*memo := (v, node_v) :: !memo; *)
MemoHash.add memo v node_name;
match v.def with
|`Type d -> Format.fprintf ppf "`Type(%a)" Print.print d
|`Variable d -> Format.fprintf ppf "`Var(%a)" Var.print d
|`Cup vl -> Format.fprintf ppf "`Cup(";
List.iter (fun v -> Format.fprintf ppf " "; aux v) vl;
Format.fprintf ppf ")"
|`Cap vl ->
Format.fprintf ppf "`Cap(";
List.iter (fun v -> Format.fprintf ppf " "; aux v) vl;
Format.fprintf ppf ")"
|`Times (v1,v2) ->
Format.fprintf ppf "`Times(";
aux v1;
Format.fprintf ppf ",";
aux v2;
Format.fprintf ppf ")";
|`Arrow (v1,v2) ->
Format.fprintf ppf "`Arrow(";
aux v1;
Format.fprintf ppf ",";
aux v2;
Format.fprintf ppf ")";
|`Xml (v1,v2) ->
Format.fprintf ppf "`Xml(";
aux v1;
Format.fprintf ppf ",";
aux v2;
Format.fprintf ppf ")";
| `Record _ -> ()
|`Neg v ->
Format.fprintf ppf "`Neg(";
aux v;
Format.fprintf ppf ")";
end
in
aux v
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X and all fresh variables
* in covariant position are substituted with empty and contravariant
......@@ -2542,91 +2582,93 @@ struct
x
end
in
let new_t = substitute_aux (decompose t) (subst h) in
descr(solve new_t)
let dec = decompose t in
let new_t = substitute_aux dec (subst h) in
descr (solve new_t)
(* Kim: we cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
latter but the variance annotation tells us that A is invariant.
*)
let rec pretty_name 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_name ni acc
let collect_variables v =
let cova = ref Var.Set.empty in
let contra = ref Var.Set.empty in
let rec memq_pair ((b, v) as key) = function [] -> false
| (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll)
in
let memo = ref [] in
let module Memo = Hashtbl.Make (struct
type t = bool * v
let hash = Hashtbl.hash
let equal (a,b) (c,d) = a == c && b == d
end)
in
let vars = Hashtbl.create 17 in
let memo = Memo.create 17 in
let t_emp = ty empty in
let t_any = ty any in
let idx = ref 0 in
(* we memoize based on the pair (pos, v), since v can occur both
* positively and negatively. and we want to manage the variables
* differently in both cases *)
let rec aux pos v =
if not (memq_pair (pos,v) !memo) then
let () = memo := (pos,v) :: !memo in
if not (Memo.mem memo (pos, v)) then
let () = Memo.add memo (pos,v) () in
match v.def with
|`Type d -> ()
|`Variable d -> if pos then cova := Var.Set.add d !cova else
contra := Var.Set.add d !contra
|`Cup vl -> List.iter (fun v -> aux pos v) vl
|`Cap vl -> List.iter (fun v -> aux pos v) vl
|`Times (v1,v2) -> (aux pos v1); (aux pos v2)
|`Variable d -> begin
try
let td = Hashtbl.find vars d in
if ((td == t_emp) && not pos)
|| ((td == t_any) && pos)
then (* polarity problem, replace the binding by a new,
pretty-printed variable *)
begin
let id = pretty_name !idx "" in
let x = var (Var.mk ~fresh:false id) in
incr idx;
Hashtbl.replace vars d x ;
end
with Not_found -> (* first time we see a variable,
set to empty for covariant and
any for contravariant *)
Hashtbl.add vars d (if pos then t_emp else t_any)
end
|`Cup vl | `Cap vl -> List.iter (fun v -> aux pos v) vl
|`Times (v1,v2) | `Xml (v1, v2) -> (aux pos v1); (aux pos v2)
|`Arrow (v1,v2) -> (aux (not pos) v1); (aux pos v2)
|`Xml (v1,v2) -> (aux pos v1); (aux pos v2)
|`Record (_, flst) -> List.iter (fun (_,_,v) -> aux pos v) flst
|`Neg v -> (aux (not pos) v)
in
aux true v;
let rcova = Var.Set.diff !cova !contra in
let rcontra = Var.Set.diff !contra !cova in
rcova, rcontra
let clean_variables t =
if no_var t then t
else begin
let dec = decompose t in
let cova, contra = collect_variables dec in
let new_t =
substitute_aux dec (fun d ->
if Var.Set.mem d cova then ty empty
else if Var.Set.mem d contra then ty any
else var d)
in
descr (solve new_t)
end
vars
(* Kim: Todo, share more code with substitutefree *)
let beautify_variables t =
let h = Hashtbl.create 17 in
let idx = ref 0 in
let rec pretty_name 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_name ni acc
in
let subst h d =
try Hashtbl.find h d
with Not_found -> begin
let id = pretty_name !idx "" in
let x = var (Var.mk ~fresh:false id) in
incr idx;
Hashtbl.add h d x ;
x
let clean_variables t =
if no_var t then t
else begin
let dec = decompose t in
let h = collect_variables dec in
let new_t =
substitute_aux dec (fun d ->
try Hashtbl.find h d with Not_found -> assert false
)
in
descr (solve new_t)
end
in
let new_t = (substitute_aux (decompose t) (subst h)) in
descr(solve new_t)
let clean_type t =
if no_var t then t else
if not (subtype t Arrow.any) then
beautify_variables (clean_variables t)
if not (subtype t Arrow.any) then clean_variables t
else
let _, u_arrow = Arrow.get t in
List.fold_left (fun acc i_arrow ->
T.cup acc (
(List.fold_left (fun acc (dom, cdom) ->
let indiv_arrow = T.arrow (T.cons dom) (T.cons cdom) in
let pretty_arrow = beautify_variables (clean_variables indiv_arrow) in
let pretty_arrow = clean_variables indiv_arrow in
T.cap acc pretty_arrow
) T.any i_arrow)
)
......@@ -3097,7 +3139,7 @@ module Tallying = struct
CS.E.add alpha (cap (cup s b) t) acc
in
let aux1 m =
let cache = Hashtbl.create (CS.M.cardinal m) in
let cache = Hashtbl.create 17 in
CS.M.fold (fun alpha (s,t) acc ->
if Hashtbl.mem cache alpha then acc else begin
Hashtbl.add cache alpha ();
......@@ -3150,8 +3192,8 @@ module Tallying = struct
if no_var d then CS.unsat else
CS.prod acc (norm d)) CS.sat l
in
(* Format.printf "Norm : %a\n" CS.pp_s n;*)
if Pervasives.(n = CS.unsat) then raise Step1Fail else
(* Format.printf "Norm : %a\n" CS.pp_s n; *)
if n == CS.unsat then raise Step1Fail else
let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in
(* Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
if CS.ES.is_empty m then raise Step2Fail else
......@@ -3172,66 +3214,69 @@ module Tallying = struct
end
exception KeepGoing
exception Found of t * int * int * Tallying.CS.sl
let apply_raw s t =
(*Kim: now that we have removed bugs in the normalisation,
it seems we can keep the memoisation table between calls
*)
(*DescrHash.clear Tallying.memo_norm; *)
let q = Queue.create () in
let apply_raw s t =
DescrHash.clear Tallying.memo_norm;
let set a i v =
let len = Array.length !a in
if i < len then (!a).(i) <- v
else begin
let b = Array.make (2*len+1) empty in
Array.blit !a 0 b 0 len;
b.(i) <- v;
a := b
end
in
let get a i = if i < 0 then any else (!a).(i) in
let gamma = var (Var.mk "Gamma") in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
let cgamma = cons gamma in
let ai = ref [| |]
and aj = ref [| |] in
let result = ref any in
let tallying i j =
try
(Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]),
(acc1, acc2)
let s = get ai i in
let t = arrow (cons (get aj j)) cgamma in
let sl = Tallying.tallying [ (s,t) ] in
let new_res =
List.fold_left (fun tacc constr_lst ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) gamma constr_lst)) any sl
in
if subtype new_res !result && not (subtype !result new_res)
then
(* strictly improved the result, continue *)
result := new_res
else raise (Found(new_res,i,j,sl))
with
|Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
|Tallying.Step2Fail -> begin
Queue.add (aux (i,lazy(acc1)) (j+1,lazy(cap acc2 (Positive.substitutefree t2))) t1 t2) q;
Queue.add (aux (i+1,lazy(cap acc1 (Positive.substitutefree t1))) (j,lazy(acc2)) t1 t2) q;
raise KeepGoing
end
Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
| Tallying.Step2Fail -> () (* continue *)
in
Queue.add (aux (1,lazy(Positive.substitutefree s)) (0,lazy(t)) s t) q;
Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q;
let result = ref ([],(any,any)) in
let counter = ref 0 in
(* I removed the condition to stop at the first solution since,
at least for map even it is only partial *)
while not(Queue.is_empty q) do
let rec loop i =
try
incr counter; (* don't know about termination... *)
if (!counter mod 10 == 0) then Format.printf "Warning: %i iterations during application typing\n%!" !counter;
result := (Queue.pop q) ()
with KeepGoing -> ()
done;
!result
let apply_full s t =
let subst_lst,(s,t) = apply_raw s t in
let ss =
List.fold_left (fun tacc constr_lst ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) s constr_lst)) any subst_lst
in
let tt =
List.fold_left (fun tacc constr_lst ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) t constr_lst)) any subst_lst
in
(*let arr = Arrow.get ss in
let res = Arrow.apply arr (tt) in *)
let ss = Positive.clean_type ss in
let tt = Positive.clean_type tt in
(*let res = Positive.clean_type res in *)
let res2 = List.fold_left
(fun acc l -> cap acc (snd (List.find (fun (`Var v, _) -> 0 == String.compare v.Var.id "Gamma") l))) any subst_lst
Format.printf "Starting expansion %i @\n@." i;
set ai (i) (cap (Positive.substitutefree s) (get ai (i-1)));
set aj (i) (cap (Positive.substitutefree t) (get aj (i-1)));
for j = 0 to i-1 do
tallying j i;
tallying i j;
done;
tallying i i;
loop (i+1)
with
Found (res, i, j, sl) ->
Format.printf "Found a solution at expansion: %i, %i@\n@."
i j;
sl, get ai i, get aj j, res
in
let res2 = Positive.clean_type res2 in
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n%!"
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res2; res2
loop 0
let apply s t = fst (apply_raw s t)
let apply_full s t =
let _,_,_,res = apply_raw s t in
let res = Positive.clean_type res in
Format.printf "result: %a@\n@." Print.print res;
res
let apply s t = let s,_,_,_ = apply_raw s t in s
......@@ -428,4 +428,10 @@ end
val apply : t -> t -> Tallying.CS.sl
val apply_full : t -> t -> t
val apply_raw : t -> t -> Tallying.CS.sl * (t*t)
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
(* apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
subst is the set of substitution that make the application succeed,
ss and tt are the expansions of s and t corresponding to that substitution
and res is the type of the result of the application
*)
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