Commit 9dfb61db authored by Kim Nguyễn's avatar Kim Nguyễn

Add a field in the VarType modules to allow dynamic dispatch.

parent f58d2708
......@@ -16,7 +16,6 @@ let pp_sl ppf l =
type constr = Types.t * Types.t (* lower and
upper bounds *)
(* A comparison function between types that
is compatible with subtyping. If types are
not in a subtyping relation, use implementation
......@@ -34,6 +33,7 @@ let compare_type t1 t2 =
(* A line is a conjunction of constraints *)
module Line = struct
type t = constr Var.Map.map
......@@ -181,19 +181,20 @@ struct
s2 acc1) s1 []
let filter = List.filter
let singleton c =
let cstr = match c with
`pos (v, s) -> Line.singleton v (Types.empty, s)
| `neg (s, v) -> Line.singleton v (s, Types.any)
in
[ cstr ]
let singleton v cs = [ (Line.singleton v cs) ]
end
let normatoms _ _ t = if Atoms.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normchars _ _ t = if Chars.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normints _ _ t = if Intervals.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normabstract _ _ t = if Abstracts.is_empty t then ConstrSet.sat else ConstrSet.unsat
let norm_simple (type a) (module V : VarType with type Atom.t = a) t =
if V.(Atom.is_empty (leafconj (proj t))) then ConstrSet.sat
else ConstrSet.unsat
let norm_atoms _ _ t = norm_simple (module VarAtoms) t
let norm_chars _ _ t = norm_simple (module VarChars) t
let norm_ints _ _ t = norm_simple (module VarIntervals) t
let norm_abstract _ _ t = norm_simple (module VarAbstracts) t
let single (type a) (module V : VarType with type Atom.t = a) b v lpos lneg =
let aux dir l =
......@@ -208,51 +209,43 @@ let single (type a) (module V : VarType with type Atom.t = a) b v lpos lneg =
let t = cap (aux id lpos) (aux neg lneg) in
if b then neg t else t
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel (type a) (module V : VarType with type Atom.t = a)
let toplevel
(type a) (module V : VarType with type Atom.t = a)
delta norm_rec mem lpos lneg
=
let _compare delta v1 v2 =
let monov1 = Var.Set.mem delta v1 in
let monov2 = Var.Set.mem delta v2 in
if monov1 == monov2 then
Var.compare v1 v2
else
if monov1 then 1 else -1
in
let singleton c =
match c with
`neg (t, x) when Var.Set.mem delta x
&& not(subtype t (var x)) -> ConstrSet.unsat
| `pos (x, t) when Var.Set.mem delta x
&& not(subtype (var x) t) -> ConstrSet.unsat
| _ -> ConstrSet.singleton c
let singleton x ((t, s) as cst) =
(* constraints over monomorphic variables must be trivial,
that is true for all substitutions
*)
let vx = var x in
if Var.Set.mem delta x && (not (subtype t vx) || not (subtype vx s))
then ConstrSet.unsat
else ConstrSet.singleton x cst
in
match lpos, lneg with
[], (`Var x)::neg ->
let t = single (module V) false x [] neg in
singleton (`neg (t, x))
singleton x (t, any)
| (`Var x)::pos,[] ->
| (`Var x)::pos, [] ->
let t = single (module V) true x pos [] in
singleton (`pos (x,t))
singleton x (empty, t)
| (`Var x)::pos, (`Var y)::neg ->
if _compare delta x y < 0 then
if Var.compare x y < 0 then
let t = single (module V) true x pos lneg in
singleton (`pos (x,t))
singleton x (empty, t)
else
let t = single (module V) false y lpos neg in
singleton (`neg (t, y))
singleton y (t, any)
| [`Atm _ ], (`Var x)::neg ->
let t = single (module V) false x lpos neg in
singleton (`neg (t, x))
singleton x (t, any)
| [ `Atm t ], [ ] -> norm_rec delta mem t
| __ -> assert false
| [ (`Atm _) as a ], [ ] -> norm_rec delta mem V.(inj (atom a))
| _ -> assert false
let big_prod f acc l =
......@@ -302,39 +295,25 @@ let rec norm delta mem t =
end else begin
DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (`pos (v,empty)) else (`neg (any,v)) in
ConstrSet.singleton s
ConstrSet.singleton v (if p then (empty, empty) else (any, any))
end
end else begin (* type is not empty and is not a variable *)
DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n");
let mem = NormMemoHash.add mem (t,delta) (false, ConstrSet.sat); mem in
let t = Iter.simplify t in
let aux (type a) (module V : VarType with type Atom.t = a)
norm_constr acc t
=
big_prod (toplevel
(module V)
delta norm_constr mem)
acc
V.(get (proj t))
let aux (module V : VarType) t acc =
let res =
big_prod
(toplevel (module V) delta (norm_dispatch V.kind) mem)
acc
V.(get (proj t))
in
DEBUG normrec
(Format.eprintf "@[ - After %s constraints: %a @]@\n"
pp_type_kind V.kind ConstrSet.print res);
res
in
let acc = ConstrSet.sat in
let acc = aux (module VarAtoms) normatoms acc t in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarIntervals) normints acc t in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarChars) normchars acc t in
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarTimes) normpair acc t in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarXml) normpair acc t in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarArrow) normarrow acc t in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarRec) normrec acc t in
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" ConstrSet.print acc);
let acc = aux (module VarAbstracts) normabstract acc t in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" ConstrSet.print acc);
let acc = Iter.fold aux t ConstrSet.sat in
DEBUG normrec (Format.eprintf "@]@\n");
acc
......@@ -350,6 +329,16 @@ let rec norm delta mem t =
);
res
and norm_dispatch k =
match k with
`intervals -> norm_ints
| `chars -> norm_chars
| `atoms -> norm_atoms
| `abstracts -> norm_abstract
| `times -> norm_pair (module VarTimes : VarType with type Atom.t = Pair.t)
| `xml -> norm_pair (module VarXml : VarType with type Atom.t = Pair.t)
| `arrow -> norm_arrow
| `record -> norm_rec
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
* [t1] v [t2] v ( [t1 \ s1] ^ [t2 \ s2] ^
......@@ -361,7 +350,7 @@ let rec norm delta mem t =
* ([t2\s2] v prod'(t1,t2\s2,n))
* *)
and normpair delta mem t =
and norm_pair (module V : VarType with type Atom.t = Pair.t) delta mem t =
let norm_prod pos neg =
let rec aux t1 t2 = function
|[] -> ConstrSet.unsat
......@@ -384,10 +373,11 @@ and normpair delta mem t =
let con0 = aux t1 t2 neg in
ConstrSet.(union (union con1 con2) con0)
in
let t = V.leafconj (V.proj t) in
big_prod norm_prod ConstrSet.sat (Pair.get t)
and normrec delta mem t =
let norm_rec ((oleft,left),rights) =
and norm_rec delta mem t =
let norm_rec_array ((oleft,left),rights) =
let rec aux accus seen = function
| [ ] -> ConstrSet.sat
|(false,_) :: rest when oleft -> aux accus seen rest
......@@ -403,10 +393,11 @@ and normrec delta mem t =
let c = Array.fold_left (fun acc t -> ConstrSet.union (norm delta mem t) acc) ConstrSet.sat left in
ConstrSet.inter (aux left [] rights) c
in
let t = VarRec.leafconj (VarRec.proj t) in
List.fold_left (fun acc (_,p,n) ->
if ConstrSet.is_unsat acc then acc else ConstrSet.inter acc (norm_rec (p,n))
if ConstrSet.is_unsat acc then acc else ConstrSet.inter acc (norm_rec_array (p,n))
) ConstrSet.sat (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
* ([t1\s1] v arrow'(t1\s1,acc,p)) ^
......@@ -420,7 +411,7 @@ and normrec delta mem t =
* P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
and normarrow delta mem t =
and norm_arrow delta mem t =
let rec norm_arrow pos neg =
match neg with
|[] -> ConstrSet.unsat
......@@ -443,6 +434,7 @@ and normarrow delta mem t =
let con22 = ConstrSet.union con2 con20 in
ConstrSet.inter con11 con22
in
let t = VarArrow.leafconj (VarArrow.proj t) in
big_prod norm_arrow ConstrSet.sat (Pair.get t)
......
......@@ -131,6 +131,19 @@ struct
end
type pair_kind = [ `Normal | `XML ]
type type_kind = [ `atoms | `intervals | `chars | `times | `xml | `arrow | `record | `abstracts ]
let pp_type_kind ppf k =
Format.fprintf ppf "%s" (match k with
`atoms -> "atoms"
| `intervals -> "intervals"
| `chars -> "chars"
| `times -> "times"
| `xml -> "xml"
| `arrow -> "arrow"
| `record -> "record"
| `abstracts -> "abstracts"
)
type ('atoms, 'ints, 'chars, 'times, 'xml, 'arrow, 'record, 'abstract) descr_ =
{
......@@ -149,6 +162,7 @@ module type VarTypeSig =
sig
include Bool.V
type descr
val kind : type_kind
val inj : t -> descr
val proj : descr -> t
val update : descr -> t -> descr
......@@ -307,6 +321,7 @@ and VarAtoms : VarTypeSig with type Atom.t = Atoms.t
struct
include Bool.MakeVar(Atoms)
type descr = Descr.t
let kind = `atoms
let inj t = { empty_descr_ with atoms = t }
let proj t = t.atoms
let update t d = { t with atoms = d }
......@@ -318,6 +333,7 @@ and VarIntervals : VarTypeSig with type Atom.t = Intervals.t
struct
include Bool.MakeVar(Intervals)
type descr = Descr.t
let kind = `intervals
let inj t = { empty_descr_ with ints = t }
let proj t = t.ints
let update t d = { t with ints = d }
......@@ -329,6 +345,7 @@ and VarChars : VarTypeSig with type Atom.t = Chars.t
struct
include Bool.MakeVar(Chars)
type descr = Descr.t
let kind = `chars
let inj t = { empty_descr_ with chars = t }
let proj t = t.chars
let update t d = { t with chars = d }
......@@ -340,6 +357,7 @@ and VarAbstracts : VarTypeSig with type Atom.t = Abstracts.t
struct
include Bool.MakeVar(Abstracts)
type descr = Descr.t
let kind = `abstracts
let inj t = { empty_descr_ with abstract = t }
let proj t = t.abstract
let update t d = { t with abstract = d }
......@@ -353,6 +371,7 @@ and VarTimes : VarTypeSig with module Atom = Pair
=
struct include Bool.MakeVar(Pair)
type descr = Descr.t
let kind = `times
let inj (t : t) : descr = { empty_descr_ with times = t }
let proj (t : descr) : t = t.times
let update (t : descr) (d : t) : descr = { t with times = d }
......@@ -363,6 +382,7 @@ and VarXml : VarTypeSig with module Atom = Pair
=
struct include Bool.MakeVar(Pair)
type descr = Descr.t
let kind = `xml
let inj (t : t) : descr = { empty_descr_ with xml = t }
let proj (t : descr) : t = t.xml
let update (t : descr) (d : t) : descr = { t with xml = d }
......@@ -373,6 +393,7 @@ and VarArrow : VarTypeSig with module Atom = Pair
=
struct include Bool.MakeVar(Pair)
type descr = Descr.t
let kind = `arrow
let inj (t : t) : descr = { empty_descr_ with arrow = t }
let proj (t : descr) : t = t.arrow
let update (t : descr) (d : t) : descr = { t with arrow = d }
......@@ -390,7 +411,7 @@ and VarRec : VarTypeSig with module Atom = Rec
=
struct include Bool.MakeVar(Rec)
type descr = Descr.t
let full_atom = Rec.atom (true, LabelMap.empty)
let kind = `record
let inj (t : t) : descr = { empty_descr_ with record = t }
let proj (t : descr) : t = t.record
let update (t : descr) (d : t) : descr = { t with record = d }
......
......@@ -77,10 +77,13 @@ include Custom.T with type t = Descr.t
module Node : Custom.T
type descr = t
type type_kind = [ `atoms | `intervals | `chars | `times | `xml | `arrow | `record | `abstracts ]
val pp_type_kind : Format.formatter -> type_kind -> unit
module type VarType = sig
include Bool.V
type descr = Descr.t
val kind : type_kind
val inj : t -> descr
val proj : descr -> t
val update : descr -> t -> descr
......
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