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

Add a utility function to apply a substitution (as returned by the tallying) to a type

parent b49243b2
......@@ -152,14 +152,14 @@ module TLV = struct
end)
let print sep ppf s =
let aux1 ppf = function
|(v,true) -> Format.fprintf ppf "%a" Var.print v
|(v,false) -> Format.fprintf ppf "~ %a" Var.print v
|(v,true) -> Format.fprintf ppf "%a" Var.print v
|(v,false) -> Format.fprintf ppf "~ %a" Var.print v
in
let rec aux ppf = function
|[] -> ()
|[h] -> aux1 ppf h
|h::l -> Format.fprintf ppf "%a %s %a" aux1 h sep aux l
in
in
aux ppf (elements s)
end
......@@ -177,9 +177,9 @@ module TLV = struct
let max x = Set.max_elt x.s
let pair x y = {
b = false ;
s = Set.empty ;
f = Var.Set.union x.f y.f
b = false ;
s = Set.empty ;
f = Var.Set.union x.f y.f
}
(* true if it contains only one variable *)
......@@ -192,7 +192,7 @@ module TLV = struct
let print ppf x = if x.b then Set.print ";" ppf x.s
let dump ppf x =
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>"
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>"
x.b Var.Set.dump x.f (Set.print ";") x.s
let mem v x = Set.mem v x.s
......@@ -417,14 +417,14 @@ let non_constructed_or_absent =
{ non_constructed with absent = true }
(* Descr.t type constructors *)
let times x y = { empty with
times = BoolPair.atom (`Atm (Pair.atom (x,y)));
let times x y = { empty with
times = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with
let xml x y = { empty with
xml = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with
arrow = BoolPair.atom (`Atm (Pair.atom (x,y)));
let arrow x y = { empty with
arrow = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
(* XXX toplevel variables are not properly set for records *)
......@@ -454,21 +454,21 @@ let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let all_vars t = t.toplvars.TLV.f
(* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *)
(* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *)
let update_tlv x y t =
let open TLV in
let tlv t =
let aux get bdd : Set.t =
let l =
let l =
List.fold_left (fun acc (p,n) ->
let acc1 =
let acc1 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,true))
|_ -> acc
) Set.empty p
in
let acc2 =
let acc2 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,false))
|_ -> assert false
......@@ -482,7 +482,7 @@ let update_tlv x y t =
|h::l -> List.fold_left Set.inter h l
in
List.fold_left Set.inter
(aux BoolChars.get t.chars)
(aux BoolChars.get t.chars)
[(aux BoolIntervals.get t.ints);
(aux BoolAtoms.get t.atoms);
(aux BoolPair.get t.arrow);
......@@ -1510,7 +1510,7 @@ struct
| Xml of [ `Tag of (Format.formatter -> unit) | `Type of nd ] * nd * nd
| Record of (bool * nd) label_map * bool * bool
| Arrows of (nd * nd) list * (nd * nd) list
| Intersection of nd
| Intersection of nd
| Neg of nd
| Abs of nd
let compare x y = x.id - y.id
......@@ -1604,11 +1604,11 @@ struct
DescrHash.add memo d s;
s
end with Not_found ->
if d.absent then
if d.absent then
alloc [Abs (prepare ({d with absent=false}))]
else if worth_complement d then
else if worth_complement d then
alloc [Neg (prepare (neg d))]
else
else
let slot = alloc [] in
if not (worth_abbrev d) then slot.state <- `Expand;
......@@ -1618,7 +1618,7 @@ struct
if (subtype { empty with times = d.times } seqs_descr) then
(cap d seqs_descr, diff d seqs_descr)
else
(empty, d)
(empty, d)
in
let add u = slot.def <- u :: slot.def in
......@@ -1626,7 +1626,7 @@ struct
(* variables are printed if displayvars OR if x is not a toplevel variable *)
let prepare_boolvar displayvars displayatoms get is_full print tlv bdd =
List.iter (fun (p,n) ->
let l1 =
let l1 =
List.fold_left (fun acc -> function
|(`Var v) as x ->
if displayvars || not(TLV.mem (x,true) tlv) then
......@@ -1657,14 +1657,14 @@ struct
let bool = Atoms.cup (Atoms.atom (Atoms.V.mk_ascii "false")) (Atoms.atom (Atoms.V.mk_ascii "true")) in
(* base types *)
prepare_boolvar displayvars displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
prepare_boolvar displayvars displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
List.map (fun x -> (Atomic x)) (Intervals.print bdd)
) not_seq.toplvars not_seq.ints;
let displayvars = false in
prepare_boolvar displayvars displayatoms BoolChars.get (Chars.equal Chars.full) (fun bdd ->
match Chars.is_char bdd with
match Chars.is_char bdd with
| Some c -> [(Char c)]
| None -> List.map (fun x -> (Atomic x)) (Chars.print bdd)
) not_seq.toplvars not_seq.chars;
......@@ -2244,7 +2244,7 @@ struct
DescrHash.replace memo_decompose t (Some s);
s
end
in
in
DescrHash.clear memo_decompose;
decompose t
......@@ -2274,19 +2274,19 @@ struct
(* 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
* in covariant position are substituted with empty and contravariant
* position with any *)
let substituterec t alpha =
let subst x d =
let subst x d =
if Var.equal d alpha then x else
if Var.is_fresh d then begin
match Var.variance d with
| `Covariant -> ty empty
| `ContraVariant -> ty any
| _ -> var d
end else var d
end else var d
in
if no_var t then t
if no_var t then t
else begin
let x = forward () in
define x (substitute_aux (decompose t) (subst x));
......@@ -2418,11 +2418,11 @@ struct
let result =
let accu1 = diff accu1 t1 in
if non_empty accu1 then aux result accu1 accu2 left
else result
else result
in
let result =
let accu2 = cap accu2 s1 in
aux result accu1 accu2 left
aux result accu1 accu2 left
in
result
| [] ->
......@@ -2718,7 +2718,7 @@ module Tallying = struct
|([`Atm t], []) -> norm_rec (t,mem)
|_,_ -> assert false
let big_prod f acc l =
let big_prod f acc l =
List.fold_left (fun acc (pos,neg) ->
if CS.S.is_empty acc then acc else
CS.prod acc (f pos neg)
......@@ -2731,7 +2731,7 @@ module Tallying = struct
(* if there is only one variable then is it A <= 0 or 1 <= A *)
(*
if is_var t then
let (v,p) = TLV.max t.toplvars in
let (v,p) = TLV.max t.toplvars in
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
else
......@@ -2748,7 +2748,7 @@ module Tallying = struct
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
aux single_record normrec acc (BoolRec.get t.record)
aux single_record normrec acc (BoolRec.get t.record)
end
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
......@@ -2921,10 +2921,10 @@ module Tallying = struct
(* 1 <= alpha <= t --> alpha = t *)
else if equal s any then CS.E.add alpha t acc
(* s <= alpha <= 1 --> alpha = ( s v fresh ) *)
else if equal t any then
else if equal t any then
CS.E.add alpha (cup s b) acc
(* 0 <= alpha <= t --> alpha = ( t ^ fresh ) *)
else if equal s empty then
else if equal s empty then
CS.E.add alpha (cap b t) acc
else
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
......@@ -2995,6 +2995,10 @@ module Tallying = struct
Format.printf "Unify : %a\n" CS.ES.print el;
List.map (CS.E.bindings) (CS.ES.elements el)
let apply_subst t subl =
List.fold_left (fun acc s ->
Positive.substitute acc s) t subl
end
exception KeepGoing
......@@ -3004,7 +3008,7 @@ let apply s t =
let gamma = var (Var.mk ~variance:`Covariant "Gamma") in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
try Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]
try Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]
with
|Tallying.Step1Fail -> raise Tallying.UnSatConstr
|Tallying.Step2Fail -> begin
......
......@@ -10,7 +10,7 @@ module BoolChars : BoolVar.S with
type s = Chars.t and
type elem = Chars.t Var.pairvar
type const =
type const =
| Integer of Intervals.V.t
| Atom of Atoms.V.t
| Char of Chars.V.t
......@@ -21,7 +21,7 @@ type const =
type service_params =
| TProd of service_params * service_params
| TOption of service_params
| TOption of service_params
| TList of string * service_params
| TSet of service_params
| TSum of service_params * service_params
......@@ -29,17 +29,17 @@ type service_params =
| TInt of string
| TInt32 of string
| TInt64 of string
| TFloat of string
| TFloat of string
| TBool of string
| TFile of string
(* | TUserType of string * (string -> 'a) * ('a -> string) *)
| TCoord of string
| TCoord of string
| TCoordv of service_params * string
| TESuffix of string
| TESuffix of string
| TESuffixs of string
(* | TESuffixu of (string * (string -> 'a) * ('a -> string)) *)
| TSuffix of (bool * service_params)
| TUnit
| TUnit
| TAny
| TConst of string;;
......@@ -85,7 +85,7 @@ include 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 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
......@@ -184,7 +184,7 @@ module Product : sig
val pi1: t -> descr
val pi2: t -> descr
val pi2_restricted: descr -> t -> descr
(* Intersection with (pi1,Any) *)
val restrict_1: t -> descr -> t
......@@ -366,7 +366,7 @@ module Tallying : sig
exception Step2Fail
module CS : sig
module M : sig
module M : sig
include Map.S with type key = (bool * Var.var)
val print : Format.formatter -> descr t -> unit
end
......@@ -407,7 +407,7 @@ module Tallying : sig
val solve : CS.s -> CS.es
val unify : CS.e -> CS.e
val tallying : (t * t) list -> CS.sl
val apply_subst : t -> (Var.var * t) list -> t
end
val apply : t -> t -> Tallying.CS.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