Commit 8dfc863f authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Multiple application test.

parent 9c70e7b8
......@@ -17,3 +17,4 @@ true: -traverse
<tests/libtest/*Test.*>: pp(camlp4orf.opt), package(netstring), package(pcre), package(oUnit), package(ulex), package(num), package(camlp4.lib)
<tests/eval/src/main.*>: pp(camlp4orf.opt), package(netstring), package(pcre), package(oUnit), package(ulex), package(num), package(camlp4.lib)
<kim*.native>: pp(camlp4orf.opt), package(netstring), package(pcre), package(oUnit), package(ulex), package(num), package(camlp4.lib)
This diff is collapsed.
#!/bin/sh
PREF=0
# echo "let funs_h0 = ["
for i in `seq 1 20`
do
echo -n '"'
for j in `seq 1 $i`
do
echo -n '`$A'${PREF}${j}' -> '
done
echo 'Int", ['
for j in `seq 1 $i`
do
echo '"`$B'${PREF}${j}'";'
#echo '"Int";'
done
echo "];"
PREF=$(($PREF + 1 ))
done
echo "];;"
exit 0
echo "let funs_hh = ["
for i in `seq 1 15`
do
echo -n '"( `$A'${PREF}1' -> `$B'${PREF}1' ) '
for j in `seq 2 $i`
do
echo -n '-> ( `$A'${PREF}${j}' -> `$B'${PREF}${j}' ) '
done
echo -n '-> `$A'${PREF}1' '
for j in `seq 2 $i`
do
echo -n '-> `$A'${PREF}${j}' '
done
echo -n ' -> ('
echo -n '`$B'${PREF}1
for j in `seq 2 $i`
do
echo -n ', `$B'${PREF}${j}
done
echo ')", ['
for j in `seq 1 $i`
do
echo '" (`$C'${PREF}${j}' -> `$D'${PREF}${j}' ) ";' # & (`$E'${PREF}${j}' -> `$F'${PREF}${j}') ";'
done
for j in `seq 1 $i`
do
echo '" (`$C'${PREF}${j}' )";' # |`$E'${PREF}${j}') ";'
done
echo "];"
PREF=$(($PREF + 1 ))
done
echo "]"
......@@ -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 *)
......@@ -2986,25 +2986,34 @@ module Tallying = struct
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.sat l in
Format.printf "Norm : %a\n" CS.pp_s n;
(* Format.printf "Norm : %a\n" CS.pp_s n; *)
if CS.S.is_empty n 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;
(* Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
if CS.ES.is_empty m then raise Step2Fail else
let el = CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc) m CS.ES.empty in
Format.printf "Unify : %a\n" CS.ES.print el;
(* Format.printf "Unify : %a\n" CS.ES.print el;*)
List.map (CS.E.bindings) (CS.ES.elements el)
let domain ll =
List.fold_left (fun acc l ->
List.fold_left (fun acc (v,_) ->
Var.Set.add v acc
) acc l
) Var.Set.empty ll
end
exception KeepGoing
let apply s t =
let apply_raw s t =
DescrHash.clear Tallying.memo_norm;
let q = Queue.create () in
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))]) , (acc1, acc2)
with
|Tallying.Step1Fail -> raise Tallying.UnSatConstr
|Tallying.Step2Fail -> begin
......@@ -3015,9 +3024,27 @@ let apply s t =
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 [] in
while (List.length !result) = 0 && not(Queue.is_empty q) do
let result = ref ([],(any,any)) in
while (List.length (fst !result)) = 0 && not(Queue.is_empty q) do
try 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
Arrow.apply arr (tt)
let apply s t = fst (apply_raw s t)
......@@ -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
......@@ -411,3 +411,5 @@ module Tallying : sig
end
val apply : t -> t -> Tallying.CS.sl
val apply_full : t -> t -> t
val apply_raw : t -> t -> Tallying.CS.sl * (t*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