Commit 912c5b2c authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Start refactoring the Types module

parent 674264c7
...@@ -19,14 +19,14 @@ end ...@@ -19,14 +19,14 @@ end
module type S = sig module type S = sig
type s type s
type elem = s Var.pairvar type elem = s Var.var_or_atom
include Custom.T include Custom.T
(* returns the union of all leaves in the BDD *) (* returns the union of all leaves in the BDD *)
val leafconj: t -> s val leafconj: t -> s
val get: t -> (elem list * elem list) list val get: t -> (elem list * elem list) list
val build : (elem list * elem list) list -> t (* val build : (elem list * elem list) list -> t*)
val empty : t val empty : t
val full : t val full : t
(* same as full, but we keep it for the moment to avoid chaging (* same as full, but we keep it for the moment to avoid chaging
...@@ -87,7 +87,7 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -87,7 +87,7 @@ module Make (T : E) : S with type s = T.t = struct
*) *)
type s = T.t type s = T.t
type elem = s Var.pairvar type elem = s Var.var_or_atom
module X : Custom.T with type t = elem = Var.Make(T) module X : Custom.T with type t = elem = Var.Make(T)
type 'a bdd = type 'a bdd =
[ `True [ `True
...@@ -222,10 +222,11 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -222,10 +222,11 @@ module Make (T : E) : S with type s = T.t = struct
| `True -> full | `True -> full
| `False -> empty | `False -> empty
| `Split(_,x, p,i,n) -> | `Split(_,x, p,i,n) ->
let p = cap (atom x) (aux p) let x1 = atom x in
and i = aux i let p = cap x1 (aux p) in
and n = diff (aux n) (atom x) in let i = aux i in
cup (cup p i) n let n = diff (aux n) x1 in
cup (cup p i) n
in in
aux b aux b
......
...@@ -14,14 +14,14 @@ end ...@@ -14,14 +14,14 @@ end
module type S = sig module type S = sig
type s type s
type elem = s Var.pairvar type elem = s Var.var_or_atom
include Custom.T include Custom.T
(** returns the union of all leaves in the BDD *) (** returns the union of all leaves in the BDD *)
val leafconj: t -> s val leafconj: t -> s
val get: t -> (elem list * elem list) list val get: t -> (elem list * elem list) list
val build : (elem list * elem list) list -> t (* val build : (elem list * elem list) list -> t *)
val empty : t val empty : t
val full : t val full : t
(* same as full, but we keep it for the moment to avoid chaging the code everywhere *) (* same as full, but we keep it for the moment to avoid chaging the code everywhere *)
......
...@@ -2688,13 +2688,8 @@ module Positive = struct ...@@ -2688,13 +2688,8 @@ module Positive = struct
let ty d = cons (`Type d) let ty d = cons (`Type d)
let var d = cons (`Variable d) let var d = cons (`Variable d)
let neg v = cons (`Neg v) let neg v = cons (`Neg v)
let cup vl = let rec cup vl = cons (`Cup vl)
match vl with let cap vl = cons (`Cap vl)
[ v ] -> v
| _ -> cons (`Cup vl)
let cap vl = match vl with
[ v ] -> v
| _ -> cons (`Cap vl)
let times v1 v2 = cons (`Times (v1,v2)) let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2)) let arrow v1 v2 = cons (`Arrow (v1,v2))
let xml v1 v2 = cons (`Xml (v1,v2)) let xml v1 v2 = cons (`Xml (v1,v2))
...@@ -2752,13 +2747,13 @@ module Positive = struct ...@@ -2752,13 +2747,13 @@ module Positive = struct
and decompose_type t = and decompose_type t =
try DescrHash.find memo t try DescrHash.find memo t
with Not_found -> with Not_found ->
let node_t = forward () in
if no_var t then ty t if no_var t then ty t
else else
match check_var t with match check_var t with
`Pos v -> var v `Pos v -> var v
| `Neg v -> neg (var v) | `Neg v -> neg (var v)
| `NotVar -> | `NotVar ->
let node_t = forward () in
let () = DescrHash.add memo t node_t in let () = DescrHash.add memo t node_t in
let descr_t = let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms) decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
...@@ -2776,18 +2771,20 @@ module Positive = struct ...@@ -2776,18 +2771,20 @@ module Positive = struct
decompose_type t decompose_type t
let solve v = internalize (make_node v) let solve v = internalize (make_node v)
(* [map_var f v] applies returns the type
let substitute_aux delta v subst = [v{ 'a <- f 'a}] for all ['a] in [v]
*)
let map_var subst v =
let memo = MemoHash.create 17 in let memo = MemoHash.create 17 in
let rec aux v subst = let rec aux v subst =
try MemoHash.find memo v try MemoHash.find memo v
with Not_found -> begin with Not_found ->
let node_v = forward () in let node_v = forward () in
MemoHash.add memo v node_v; let () = MemoHash.add memo v node_v in
let new_v = let new_v =
match v.def with match v.def with
|`Type d -> `Type d |`Type d -> `Type d
|`Variable d when Var.Set.mem d delta -> v.def (* |`Variable d when Var.Set.mem d delta -> v.def *)
|`Variable d -> (subst d).def |`Variable d -> (subst d).def
|`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl) |`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl)
|`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl) |`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl)
...@@ -2800,62 +2797,54 @@ module Positive = struct ...@@ -2800,62 +2797,54 @@ module Positive = struct
in in
node_v.def <- new_v; node_v.def <- new_v;
node_v node_v
end
in in
aux v subst aux v subst
(* returns a recursive type where all occurrences of alpha n t let apply_subst ?(subst=(fun v -> var v)) ?(after=(fun x -> x)) t =
* are substituted with a recursive variable X *) if no_var t then t else
let substituterec t alpha = let res = map_var subst (decompose t) in
if no_var t then t let res = after res in
else begin descr (solve res)
let subst x d = if Var.equal d alpha then x else var d in
let x = forward () in (* Given a type t and a polymorphic variable 'a occuring in t,
define x (substitute_aux Var.Set.empty (decompose t) (subst x)); returns the type s which is the solution of 'a = t *)
descr(solve x) let solve_rectype t alpha =
end let x = forward () in
let subst d = if Var.equal d alpha then x else var d in
apply_subst ~subst:subst ~after:(fun y -> define x y;x) t
(* Pre-condition : alpha \not\in \delta *) (* Pre-condition : alpha \not\in \delta *)
let substitute t (alpha,s) = let substitute t (alpha,s) =
if no_var t then t let vs = ty s in
else begin let subst d = if Var.equal d alpha then vs else var d in
let subst s d = if Var.equal d alpha then s else var d in apply_subst ~subst:subst t
let new_t = (substitute_aux Var.Set.empty (decompose t) (subst (ty s))) in
descr (solve new_t)
end
let substitute_list t l = let substitute_list t l =
if no_var t then t let subst d =
else begin try
let subst l d = ty
try ty(snd(List.find (fun (alpha,_) -> Var.equal d alpha) l)) @@ snd
with Not_found -> var d @@ List.find (fun (alpha,_) -> Var.equal d alpha) l
in with Not_found -> var d
let new_t = (substitute_aux Var.Set.empty (decompose t) (subst l)) in in
descr (solve new_t) apply_subst ~subst:subst t
end
let substitutefree delta t = let substitute_free delta t =
if no_var t then t else
let h = Hashtbl.create 17 in let h = Hashtbl.create 17 in
let subst h d = let subst d =
try Hashtbl.find h d if Var.Set.mem d delta then var d else
with Not_found -> begin try
let x = var (Var.fresh d) in Hashtbl.find h d
Hashtbl.add h d x ; with Not_found ->
x let x = var (Var.fresh d) in
end Hashtbl.add h d x ;
x
in in
let dec = decompose t in apply_subst ~subst:subst t
let new_t = substitute_aux delta dec (subst h) in
descr (solve new_t)
let substitute_kind delta kind t = let substitute_kind delta kind t =
if no_var t then t else let subst d = var (Var.set_kind kind d) in
let subst kin d = var (Var.set_kind kind d) in apply_subst ~subst:subst t
let dec = decompose t in
let new_t = substitute_aux delta dec (subst kind) in
descr (solve new_t)
(* We cannot use the variance annotation of variables to simplify them, (* We cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types since variables are shared amongst types. If we have two types
...@@ -2916,24 +2905,21 @@ module Positive = struct ...@@ -2916,24 +2905,21 @@ module Positive = struct
aux true v; aux true v;
vars vars
let clean_variables delta t = let clean_type delta t =
if no_var t then t if no_var t then t
else begin else begin
let dec = decompose t in let dec = decompose t in
let h = collect_variables delta dec in let h = collect_variables delta dec in
let new_t = let new_t =
substitute_aux delta dec (fun d -> map_var (fun d ->
try Hashtbl.find h d try
with Not_found -> assert false Hashtbl.find h d
) with Not_found -> assert false
) dec
in in
descr (solve new_t) descr (solve new_t)
end end
let clean_type delta t =
if no_var t then t else
clean_variables delta t
let dump ppf t = pp ppf (decompose t) let dump ppf t = pp ppf (decompose t)
end end
...@@ -3473,8 +3459,8 @@ module Tallying = struct ...@@ -3473,8 +3459,8 @@ module Tallying = struct
(* Format.printf "e1 = %a\n" CS.print_e e1; *) (* Format.printf "e1 = %a\n" CS.print_e e1; *)
(* remove from E \ { (alpha,t) } every occurrences of alpha (* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *) * by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* substituterec remove also all previously introduced fresh variables *) (* solve_rectype remove also all previously introduced fresh variables *)
let x = Positive.substituterec t alpha in let x = Positive.solve_rectype t alpha in
(* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *) (* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
let es = let es =
CS.E.fold (fun beta s acc -> CS.E.fold (fun beta s acc ->
...@@ -3616,7 +3602,7 @@ let squaresubtype delta s t = ...@@ -3616,7 +3602,7 @@ let squaresubtype delta s t =
try try
let ss = let ss =
if i = 0 then s if i = 0 then s
else (cap (Positive.substitutefree delta s) (get ai (i-1))) else (cap (Positive.substitute_free delta s) (get ai (i-1)))
in in
set ai i ss; set ai i ss;
tallying i; tallying i;
...@@ -3665,8 +3651,8 @@ let apply_raw delta s t = ...@@ -3665,8 +3651,8 @@ let apply_raw delta s t =
(* Format.printf "Starting expansion %i @\n@." i; *) (* Format.printf "Starting expansion %i @\n@." i; *)
let (ss,tt) = let (ss,tt) =
if i = 0 then (s,t) else if i = 0 then (s,t) else
((cap (Positive.substitutefree delta s) (get ai (i-1))), ((cap (Positive.substitute_free delta s) (get ai (i-1))),
(cap (Positive.substitutefree delta t) (get aj (i-1)))) (cap (Positive.substitute_free delta t) (get aj (i-1))))
in in
set ai i ss; set ai i ss;
set aj i tt; set aj i tt;
......
...@@ -71,30 +71,20 @@ end ...@@ -71,30 +71,20 @@ end
module BoolAtoms : BoolVar.S with module BoolAtoms : BoolVar.S with
type s = Atoms.t and type s = Atoms.t and
type elem = Atoms.t Var.pairvar type elem = Atoms.t Var.var_or_atom
module BoolIntervals : BoolVar.S with module BoolIntervals : BoolVar.S with
type s = Intervals.t and type s = Intervals.t and
type elem = Intervals.t Var.pairvar type elem = Intervals.t Var.var_or_atom
module BoolChars : BoolVar.S with module BoolChars : BoolVar.S with
type s = Chars.t and type s = Chars.t and
type elem = Chars.t Var.pairvar type elem = Chars.t Var.var_or_atom
module BoolAbstracts: BoolVar.S with module BoolAbstracts: BoolVar.S with
type s = Abstracts.t and type s = Abstracts.t and
type elem = Abstracts.t Var.pairvar type elem = Abstracts.t Var.var_or_atom
include Custom.T include Custom.T
module Node : Custom.T module Node : Custom.T
module Pair : Bool.S with type elem = (Node.t * Node.t)
module BoolPair : BoolVar.S with
type s = Pair.t and
type elem = Pair.t Var.pairvar
module Rec : Bool.S with type elem = bool * Node.t Ident.label_map
module BoolRec : BoolVar.S with
type s = Rec.t and
type elem = Rec.t Var.pairvar
type descr = t type descr = t
val make: unit -> Node.t val make: unit -> Node.t
...@@ -163,12 +153,12 @@ module Positive : sig ...@@ -163,12 +153,12 @@ module Positive : sig
val cup: v list -> v val cup: v list -> v
val times: v -> v -> v val times: v -> v -> v
val xml: v -> v -> v val xml: v -> v -> v
val solve: v -> Node.t
val substitute : t -> (Var.var * t) -> t val substitute : t -> (Var.var * t) -> t
val substitute_list : t -> (Var.var * t) list -> t val substitute_list : t -> (Var.var * t) list -> t
val substituterec : t -> Var.var -> t val solve_rectype : t -> Var.var -> t
val solve: v -> Node.t val substitute_free : Var.Set.t -> t -> t
val substitutefree : Var.Set.t -> t -> t
val clean_type : Var.Set.t -> t -> t val clean_type : Var.Set.t -> t -> t
end end
......
...@@ -39,11 +39,11 @@ module Set = struct ...@@ -39,11 +39,11 @@ module Set = struct
let fold = fold let fold = fold
end end
type 'a pairvar = [ `Atm of 'a | `Var of t ] type 'a var_or_atom = [ `Atm of 'a | `Var of t ]
module Make (X : Custom.T) = struct module Make (X : Custom.T) = struct
type t = X.t pairvar type t = X.t var_or_atom
let hash = function `Atm t -> X.hash t | `Var x -> V.hash x let hash = function `Atm t -> 17 + 17 * X.hash t | `Var x -> 997 + 17 * V.hash x
let check = function `Atm t -> X.check t | `Var _ -> () let check = function `Atm t -> X.check t | `Var _ -> ()
...@@ -54,7 +54,7 @@ module Make (X : Custom.T) = struct ...@@ -54,7 +54,7 @@ module Make (X : Custom.T) = struct
|`Var _, `Atm _ -> -1 |`Var _, `Atm _ -> -1
|`Atm _, `Var _ -> 1 |`Atm _, `Var _ -> 1
let equal t1 t2 = (compare t1 t2) = 0 let equal t1 t2 = (compare t1 t2) == 0
let dump ppf = function let dump ppf = function
|`Atm x -> X.dump ppf x |`Atm x -> X.dump ppf x
......
...@@ -36,6 +36,6 @@ module Set : sig ...@@ -36,6 +36,6 @@ module Set : sig
val choose : t -> var val choose : t -> var
end end
type 'a pairvar = [ `Atm of 'a | `Var of t ] type 'a var_or_atom = [ `Atm of 'a | `Var of t ]
module Make (X : Custom.T) : Custom.T with type t = X.t pairvar module Make (X : Custom.T) : Custom.T with type t = X.t var_or_atom
...@@ -973,8 +973,8 @@ and type_check' loc env ed constr precise = match ed with ...@@ -973,8 +973,8 @@ and type_check' loc env ed constr precise = match ed with
(fun v -> (fun v ->
let open Types in let open Types in
match v with match v with
| Val t -> Val (Positive.substitutefree env.delta t) | Val t -> Val (Positive.substitute_free env.delta t)
| EVal (a,b,t) -> EVal (a,b,Positive.substitutefree env.delta t) | EVal (a,b,t) -> EVal (a,b,Positive.substitute_free env.delta t)
| x -> x) | x -> x)
env.ids } env.ids }
in in
...@@ -1050,7 +1050,7 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1050,7 +1050,7 @@ and type_check' loc env ed constr precise = match ed with
| Apply (e1,e2) -> | Apply (e1,e2) ->
let t1 = type_check env e1 Types.Arrow.any true in let t1 = type_check env e1 Types.Arrow.any true in
let t1arrow = Types.Arrow.get t1 in let t1arrow = Types.Arrow.get t1 in
let t1 = Types.Positive.substitutefree env.delta t1 in let t1 = Types.Positive.substitute_free env.delta t1 in
(* t [_delta 0 -> 1 *) (* t [_delta 0 -> 1 *)
begin try begin try
ignore(Types.Tallying.tallying env.delta [(t1,Types.Arrow.any)]) ignore(Types.Tallying.tallying env.delta [(t1,Types.Arrow.any)])
...@@ -1060,7 +1060,7 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1060,7 +1060,7 @@ and type_check' loc env ed constr precise = match ed with
let dom = Types.Arrow.domain(t1arrow) in let dom = Types.Arrow.domain(t1arrow) in
let t2 = type_check env e2 Types.any true in let t2 = type_check env e2 Types.any true in
let t2 = Types.Positive.substitutefree env.delta t2 in let t2 = Types.Positive.substitute_free env.delta t2 in
let (sl,res) = let (sl,res) =
if not (Types.no_var dom) || if not (Types.no_var dom) ||
not (Types.no_var t2) then not (Types.no_var t2) then
......
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