Skip to content

GitLab

Commit 9b693d33 authored by Julien Lopez's avatar Julien Lopez
Browse files

Fixes in TLV; fix hook

parent 31f30efb
Hide whitespace changes
Inline Side-by-side
tests/libtest/tallyingTest.ml
View file @ 9b693d33
......@@ -465,7 +465,7 @@ let test_apply =
let t_sigma_domain = (Types.Arrow.domain(Types.Arrow.get t_sigma)) in
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "t @@ sl < 0 - 1 = %a\n" Types.Print.print t_sigma
Format.fprintf fmt "t @@ sl < 0 -> 1 = %a\n" Types.Print.print t_sigma
) (Types.subtype t_sigma (parse_typ "Empty -> Any")) true;
assert_equal ~pp_diff:(fun fmt _ ->
......
tests/libtest/typesTest.ml
View file @ 9b693d33
......@@ -13,18 +13,18 @@ let to_string pp t =
;;
let tlv_tests = [ "is_var", [
"`$A", Types.is_var, true;
(* "`$A", Types.is_var, true;
"Int", Types.is_var, false;
"Empty", Types.is_var, false;
"Any", Types.is_var, false;
"Any", Types.is_var, false;*)
"`$A & Int", Types.is_var, false;
"`$A & Any", Types.is_var, true;
(* "`$A & Any", Types.is_var, true;
"`$A | Int", Types.is_var, false;
"(`$A,Int)", Types.is_var, false;
"Any \\ `$A", Types.is_var, true;
"`$A \\ Any", Types.is_var, false;
"Any \\ `$A", Types.is_var, true; (* ~`$A *)
"`$A \\ Any", Types.is_var, false; (* Empty *)*)
];
(*
"no_var", [
"Int", Types.no_var, true;
"Any", Types.no_var, true;
......@@ -37,7 +37,7 @@ let tlv_tests = [ "is_var", [
"`$A | Char", Types.no_var, false;
"(`$A,Int)", Types.no_var, false;
"(Char,Int)", Types.no_var, true;
"`$A \\ Any", Types.no_var, true;
"`$A \\ Any", Types.no_var, true; (* Empty *)
];
"has_tlv", [
......@@ -47,15 +47,15 @@ let tlv_tests = [ "is_var", [
"`A", Types.has_tlv, false;
"`$A", Types.has_tlv, true;
"(`$A,Int)", Types.has_tlv, false;
"`$A & Int", Types.has_tlv, false;
"`$A | Int", Types.has_tlv, false;
"`$A | Char", Types.has_tlv, false;
"`$A | (Any,Any)", Types.has_tlv, false;
"`$A & Int", Types.has_tlv, true;
"`$A | Int", Types.has_tlv, true;
"`$A | Char", Types.has_tlv, true;
"`$A | (Any,Any)", Types.has_tlv, true;
"`$A | (`$B,Int)", Types.has_tlv, true;
"`$A | (Char,Int)", Types.has_tlv, true;
"Any \\ `$A", Types.has_tlv, true;
];
*)
]
let test_tlv_operations =
......
tools/git_hooks/debug/pre-commit 100644 → 100755
View file @ 9b693d33
......@@ -3,17 +3,22 @@ ROOTDIR="$(git rev-parse --git-dir)"
cd $ROOTDIR/..
echo "Testing the program before commit..."
echo "Testing tallying..."
ocamlbuild -tag debug tests/tallyingTest.byte && ./tallyingTest.byte
ocamlbuild tests/libtest/tallyingTest.native > /dev/null 2>&1 && ./tallyingTest.native > /dev/null 2>&1
if test $? -ne 0; then
echo "Tests failed. Aborting commit."
exit 2
fi
ocamlbuild tests/libtest/typesTest.native > /dev/null 2>&1 && ./typesTest.native > /dev/null 2>&1
if test $? -ne 0; then
echo "Tests failed. Aborting commit."
exit 2
fi
echo "Testing lambda..."
cd tests/lambda
make && ./lambdaTests.native && ./valueTests.native
make > /dev/null 2>&1 && ./lambdaTests.native > /dev/null 2>&1 && ./valueTests.native > /dev/null 2>&1
echo "Cleaning..."
make clean > /dev/null 2>&1
cd ../..
ocamlbuild -clean
ocamlbuild -clean > /dev/null 2>&1
echo "Success!"
exit 0
types/types.ml
View file @ 9b693d33
......@@ -166,35 +166,40 @@ module TLV = struct
end
(* tlv : top level variables
* fv : all free variables in the subtree
* varonly : true if the type contains only variables *)
type t = { tlv : Set.t ; fv : Var.Set.t ; varonly : bool }
* fv : all free variables in the subtree *)
type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool }
let empty = { tlv = Set.empty ; fv = Var.Set.empty ; varonly = false }
let any = { tlv = Set.empty ; fv = Var.Set.empty ; varonly = false }
let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; varonly = true }
let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true }
(* return the max of top level variables *)
let max x = Set.max_elt x.tlv
let pair x y = {
varonly = false ;
tlv = Set.empty ;
fv = Var.Set.union x.fv y.fv
fv = Var.Set.union x.fv y.fv ;
isvar = false
}
let record x = {
tlv = Set.empty ;
fv = x.fv ;
isvar = false
}
(* true if it contains only one variable *)
let is_single x = x.varonly && (Var.Set.cardinal x.fv = 1) && (Set.cardinal x.tlv = 1)
let is_single x = x.isvar && (Var.Set.cardinal x.fv = 1) && (Set.cardinal x.tlv = 1)
let no_variables x = (x.varonly == false) && (Var.Set.cardinal x.fv = 0) && (Set.cardinal x.tlv = 0)
let no_variables x = (Var.Set.cardinal x.fv = 0) && (Set.cardinal x.tlv = 0)
let has_toplevel x = Set.cardinal x.tlv > 0
let print ppf x = if x.varonly then Set.print ";" ppf x.tlv
let print ppf x = Set.print ";" ppf x.tlv
let dump ppf x =
Format.fprintf ppf "<varonly = %b ; fv = {%a} ; tlv = {%a}>"
x.varonly Var.Set.print x.fv (Set.print ";") x.tlv
Format.fprintf ppf "<fv = {%a} ; tlv = {%a}>"
Var.Set.print x.fv (Set.print ";") x.tlv
let mem v x = Set.mem v x.tlv
end
......@@ -237,6 +242,7 @@ sig
}
include Custom.T with type t = s
val empty: t
val is_empty : t -> bool
end =
struct
type s = {
......@@ -306,6 +312,16 @@ struct
(a.absent == b.absent)
)
let is_empty a =
(BoolAtoms.is_empty a.atoms) &&
(BoolChars.is_empty a.chars) &&
(BoolIntervals.is_empty a.ints) &&
(BoolPair.is_empty a.times) &&
(BoolPair.is_empty a.xml) &&
(BoolPair.is_empty a.arrow) &&
(BoolRec.is_empty a.record) &&
(Abstract.is_empty a.abstract)
let compare a b =
if a == b then 0
else let c = BoolAtoms.compare a.atoms b.atoms in if c <> 0 then c
......@@ -431,17 +447,11 @@ let arrow x y = { empty with
let record label t =
{ empty with
record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t)));
toplvars = (descr t).toplvars}
toplvars = TLV.record (descr t).toplvars }
let tlv_from_rec (_, l) =
let union x y =
let open TLV in {
varonly = x.varonly && y.varonly ;
tlv = Set.union x.tlv y.tlv ;
fv = Var.Set.union x.fv y.fv
} in
let rec aux acc = function
| (_, n) :: rest -> aux (union acc (descr n).toplvars) rest
| (_, n) :: rest -> aux (TLV.pair acc (descr n).toplvars) rest
| [] -> acc in
aux TLV.empty (Ident.LabelMap.get l)
......@@ -465,13 +475,6 @@ let var a = {
toplvars = TLV.singleton (a,true)
}
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars
let all_vars t = t.toplvars.TLV.fv
let all_tlv t = t.toplvars.TLV.tlv
(* 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 =
......@@ -499,7 +502,7 @@ let update_tlv x y t =
|[h] -> h
|h::l -> List.fold_left Set.inter h l
in
List.fold_left Set.inter
List.fold_left Set.union
(aux BoolChars.get t.chars)
[
(aux BoolIntervals.get t.ints);
......@@ -509,11 +512,16 @@ let update_tlv x y t =
(aux BoolRec.get t.record)
]
in
{ t with toplvars =
{
tlv = tlv t ;
fv = Var.Set.union x.toplvars.fv y.toplvars.fv ;
varonly = x.toplvars.varonly && x.toplvars.varonly
let fv t = if Descr.equal t Descr.empty then
Var.Set.empty, false else
Var.Set.union x.toplvars.fv y.toplvars.fv, t.toplvars.isvar
in
let fv, isvar = fv t in
{ t with toplvars =
{
tlv = tlv t ;
fv = fv ;
isvar = isvar
} }
;;
......@@ -593,6 +601,13 @@ and const_node c = cons (constant c)
let neg x = diff any x
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars
let all_vars t = t.toplvars.TLV.fv
let all_tlv t = t.toplvars.TLV.tlv
let any_node = cons any
let empty_node = cons empty
......@@ -1648,17 +1663,17 @@ struct
let add u = slot.def <- u :: slot.def in
let prepare_boolvar get is_full print tlv bdd =
let ll =
let ll =
List.fold_left (fun acc (p,n) ->
let (_,l1) =
List.fold_left (fun (has_tlv,acc) -> function
|(`Var v) as x when (TLV.mem (x,true) tlv) -> (true,acc)
|(`Var v) as x -> (has_tlv,(Atomic (fun ppf -> Var.print ppf x))::acc)
|`Atm bdd ->
|`Atm bdd ->
begin match has_tlv,acc with
|true,[] -> if is_full bdd then (has_tlv,[]) else (has_tlv,print bdd)
|false,[] -> (has_tlv,print bdd)
|_,_ -> (has_tlv,acc @ (print bdd))
|_,_ -> (has_tlv,acc @ (print bdd))
end
) (false,[]) p
in
......@@ -1682,7 +1697,7 @@ struct
if has_tlv not_seq then begin
let l =
TLV.Set.fold (fun ((`Var v) as x,p) acc ->
let s =
let s =
if p then (Atomic (fun ppf -> Var.print ppf x))
else (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))
in s::acc
......@@ -3025,14 +3040,14 @@ module Tallying = struct
(* if we already evaluated it, it is sat *)
if DescrSet.mem t mem || is_empty t then begin
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end
CS.sat end
else begin
if is_empty t then CS.sat
(* if there is only one variable then is it A <= 0 or 1 <= A *)
else if is_var t then
(* else if is_var t then
let (v,p) = TLV.max t.toplvars in
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
CS.singleton s*)
(* if there are no vars, and it is not empty then unsat *)
else if no_var t then CS.unsat
else begin
......@@ -3193,12 +3208,12 @@ module Tallying = struct
Hashtbl.add cache alpha ();
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
if is_var t then begin
(* if is_var t then begin
let (beta,_) = TLV.max t.toplvars in
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
aux alpha (s,t) acc1
end else
end else*)
(* alpha = ( s v fresh) ^ t *)
aux alpha (s,t) acc;
end
......@@ -3234,10 +3249,10 @@ module Tallying = struct
exception Step2Fail
let tallying ?(delta=Var.Set.empty) l =
let n =
let n =
List.fold_left (fun acc (s,t) ->
let d = diff s t in
if is_empty d then CS.sat
if is_empty d then CS.sat
else if no_var d then CS.unsat
else CS.prod acc (norm d)
) CS.sat l
......@@ -3245,14 +3260,14 @@ module Tallying = struct
if Pervasives.(n = CS.unsat) then raise Step1Fail else
let m =
CS.S.fold (fun c acc ->
try CS.ES.union (solve (merge c)) acc
try CS.ES.union (solve (merge c)) acc
with UnSatConstr _ -> acc
) n CS.ES.empty
) n CS.ES.empty
in
if CS.ES.is_empty m then raise Step2Fail else
let el =
let dom e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
CS.ES.fold (fun e acc ->
CS.ES.fold (fun e acc ->
let si = unify e in
(* XXX maybe we can eliminate solution earlier. Is it safe to do it here ? *)
(* si is a solution only if (dom(si) /\ delta = emptyset) *)
......@@ -3350,7 +3365,7 @@ let set a i v =
b.(i) <- v;
a := b
end
let get a i = if i < 0 then any else (!a).(i)
let get a i = if i < 0 then any else (!a).(i)
(** find two sets of type substitutions I,J such that
s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
......@@ -3430,10 +3445,10 @@ let squaresubtype delta s t =
let rec loop i =
try
let ss =
if i = 0 then s
if i = 0 then s
else (cap (Positive.substitutefree s) (get ai (i-1)))
in
set ai i ss;
in
set ai i ss;
(*
Format.printf "Starting expansion %i @\n@." i;
Format.printf "%a < %a\n@." Print.print ss Print.print t;
......
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