Skip to content

GitLab

Commit 178030ec authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'master' into propagate 

Conflicts:
	tests/libtest/tallyingTest.ml
	types/types.ml
	types/types.mli
parents 6ffd23bb cee524ae
Hide whitespace changes
Inline Side-by-side
_tags
View file @ 178030ec
......@@ -14,7 +14,7 @@ true: -traverse
<parser/**>: package(ulex), package(netstring), syntax(camlp4o)
<schema/**>: package(pcre), package(netstring)
<runtime/**>: package(pcre), package(netstring)
<tests/libtest/*Test.*>: pp(camlp4orf.opt), package(netstring), package(pcre), package(oUnit), package(ulex), package(num), package(camlp4.lib)
<tests/libtest/*Test.*>: 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)
runtime/run_dispatch.ml
View file @ 178030ec
......@@ -201,7 +201,7 @@ let rec eval_sigma env =
List.fold_left (fun acc sigma_j ->
let exists_sub =
List.exists (fun (_,s_i) ->
inzero env env.(x) (Types.Tallying.(s_i @@ sigma_j))
inzero env env.(x) (Types.Tallying.(s_i $$ sigma_j))
) iface
in
if exists_sub then sigma_j::acc else acc
......@@ -219,7 +219,7 @@ and inzero env v t =
| Abstraction (Some iface,_,sigma) ->
let s = List.fold_left (fun acc t -> Types.cap acc (snd t)) Types.any iface in
List.for_all (fun si ->
Types.subtype (Types.Tallying.(s @@ si)) t
Types.subtype (Types.Tallying.(s $$ si)) t
) (eval_sigma env sigma)
| _ -> true
......
tests/libtest/tallyingTest.ml
View file @ 178030ec
......@@ -330,9 +330,9 @@ let test_tallying =
let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
let sigma = Tallying.tallying l in
List.iter (fun (s,t) ->
List.iter (fun si ->
let s_sigma = Tallying.(s @@ si) in
let t_sigma = Tallying.(t @@ si) in
List.iter (fun sigma ->
let s_sigma = Tallying.(s $$ sigma) in
let t_sigma = Tallying.(t $$ sigma) in
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "s @ sigma_i = %a\n" Types.Print.print s_sigma;
Format.fprintf fmt "t @ sigma_i = %a\n" Types.Print.print t_sigma
......
tests/libtest/typesTest.ml
View file @ 178030ec
open OUnit
(* open Types *)
let parse_typ s =
let st = Stream.of_string s in
let astpat = Parser.pat st in
......@@ -58,20 +56,6 @@ let tlv_tests = [ "is_var", [
"Any \\ `$A", Types.has_tlv, true;
];
"var_only", [
"Int", Types.TLV.var_only, false;
"Any", Types.has_tlv, false;
"Empty", Types.has_tlv, false;
"`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 | (`$B,Int)", Types.has_tlv, true;
"`$A | (Char,Int)", Types.has_tlv, true;
];
]
let test_tlv_operations =
......@@ -112,6 +96,24 @@ let test_set_operations =
) set_op_tests
;;
let squaresubtype_tests = [
"`$A -> `$B", "Int -> Bool", [], true;
"`$A -> `$B", "Int -> Bool", ["A"], false;
"`$A -> `$A", "(Int -> Int) & (Bool -> Bool)", [], true;
]
let test_squaresubtype =
"test squaresubtype" >:::
List.map (fun (s,t,delta,expected) ->
(Printf.sprintf " %s [= %s " s t) >:: (fun _ ->
let t1 = parse_typ s in
let t2 = parse_typ t in
let delta = List.fold_left (fun acc v -> Var.Set.add (Var.mk v) acc) Var.Set.empty delta in
assert_equal (snd(Types.squaresubtype delta t1 t2)) expected
)
) squaresubtype_tests
;;
let subst_tests = [
"`$A", "A", "Bool", "Bool";
"`$A", "A", "`$B", "`$B";
......@@ -213,6 +215,8 @@ let subtype_tests = [
"1--5" , "1--4", false ;
"Int" , "0--*", false ;
"Int -> Int", "Empty -> Any", true;
(* polymorphic cduce extension *)
"`$X" , "Any", true;
......@@ -225,7 +229,6 @@ let subtype_tests = [
(* ({ (int , true) } , { }) *)
"Int -> Int", "`$A -> `$A", false;
(* { (true^[ A ] , any) } *)
"Int -> Int", "Empty -> Any", true;
"(`$A -> `$C) & (`$B -> `$C)", "(`$A | `$B) -> `$C", true;
"((`$A -> `$C) & (`$B -> `$C))", "((`$A | `$B) -> `$C)", true;
"((`$A | `$B) -> `$C)", "((`$A -> `$C) & (`$B -> `$C))", true;
......@@ -296,6 +299,7 @@ let test_witness =
let all =
"all tests" >::: [
test_set_operations;
test_squaresubtype;
test_subtype;
test_substitution;
test_rec_subtitutions;
......
types/types.ml
View file @ 178030ec
......@@ -2481,9 +2481,6 @@ struct
end )
let substitute_aux v subst =
(* XXX do I really need memo here XXX *)
(* Kim: yes we do, see solve above. We use a list and memq since we rely on pointer identity
for cycles. *)
let memo = MemoHash.create 17 in
let rec aux v subst =
try
......@@ -2802,7 +2799,6 @@ module Tallying = struct
end
(* Set of equation sets *)
module ES = struct
include Set.Make(struct
......@@ -2914,6 +2910,15 @@ module Tallying = struct
type m = M.t
type es = ES.t
type sigma = Descr.s E.t
(*
module SUB = SortedList.FiniteCofinite(struct
let compare = E.compare
let equal = E.equal
let hash = 1
let dump = E.print
let check = fun _ -> ()
end)
*)
type sl = sigma list
let singleton = function
......@@ -3212,31 +3217,100 @@ module Tallying = struct
exception Step1Fail
exception Step2Fail
(* XXX add delta here !!! *)
let tallying l =
let n = List.fold_left (fun acc (s,t) ->
let d = diff s t in
if is_empty d then CS.sat
else if no_var d then CS.unsat
else CS.prod acc (norm d)) CS.sat l
let tallying ?(delta=Var.Set.empty) l =
let n =
List.fold_left (fun acc (s,t) ->
let d = diff s t in
if is_empty d then CS.sat
else if no_var d then CS.unsat
else CS.prod acc (norm d)
) CS.sat l
in
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 with UnSatConstr _ -> acc) n CS.ES.empty in
let m =
CS.S.fold (fun c acc ->
try CS.ES.union (solve (merge c)) acc
with UnSatConstr _ -> acc
) n CS.ES.empty
in
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
(* List.map (CS.E.bindings) *) (CS.ES.elements el)
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 ->
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) *)
if Var.Set.is_empty (Var.Set.inter (dom(si)) delta) then
CS.ES.add si acc
else acc
) m CS.ES.empty
in
(CS.ES.elements el)
type symsubst = I | S of CS.sigma | A of (symsubst * symsubst)
let rec dom = function
|I -> Var.Set.empty
|S si -> CS.E.fold (fun v _ acc -> Var.Set.add v acc) si Var.Set.empty
|A (si,sj) -> Var.Set.union (dom si) (dom sj)
(* composition of two symbolic substitution sets sigmaI, sigmaJ .
Cartesian product *)
let (++) sI sJ =
let bind m f = List.flatten(List.map f m) in
bind sI (fun si ->
bind sJ (fun sj ->
[A(si,sj)]
)
)
(* apply sigma to t *)
let ($$) t si = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) si t
(* apply a symbolic substitution si to a type t *)
let (@@) t si =
CS.E.fold (fun var subst acc ->
Positive.substitute acc (var,subst)
) si t
let vst = ref Var.Set.empty in
let vsi = ref Var.Set.empty in
let get e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
let filter t si =
vsi := get si;
vst := all_vars t;
not(Var.Set.is_empty (Var.Set.inter !vst !vsi))
in
let filterdiff t si sj =
let vsj = get sj in
not(Var.Set.is_empty (Var.Set.inter !vst (Var.Set.diff !vsi vsj)))
in
let rec aux t = function
|I -> t
|S si -> t $$ si
|A (S si,_) when filter t si -> t $$ si
|A (S si,S sj) when filterdiff t si sj -> (t $$ sj) $$ si
|A (si,sj) -> aux (aux t sj) si
in
aux t si
let domain ll =
List.fold_left (fun acc e ->
let domain sl =
List.fold_left (fun acc si ->
CS.E.fold (fun v _ acc ->
Var.Set.add v acc
) e acc
) Var.Set.empty ll
) si acc
) Var.Set.empty sl
(*
(* Returns Some l2 if l1 is a subsigma of l2, Some l1 if l2 is a subsigma of
l1, None otherwise. *)
let subsigma l1 l2 =
let rec aux l = function
| [] -> Some l
| x :: rest ->
(try ignore(List.find (fun y -> CS.E.compare Descr.compare x y = 0) l); aux l rest
with Not_found -> None)
in
if List.length l1 > List.length l2 then aux l1 l2 else aux l2 l1
*)
let is_identity = List.for_all (CS.E.is_empty)
let codomain ll =
List.fold_left (fun acc e ->
......@@ -3249,21 +3323,23 @@ module Tallying = struct
end
exception Found of t * int * int * Tallying.CS.sl
exception FoundApply of t * int * int * Tallying.CS.sl
let set a i v =
let len = Array.length !a in
if i < len then (!a).(i) <- v
else begin
let b = Array.make (2*len+1) empty in
Array.blit !a 0 b 0 len;
b.(i) <- v;
a := b
end
let get a i = if i < 0 then any else (!a).(i)
let apply_raw s t =
(** find two sets of type substitutions I,J such that
s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
let apply_raw s t =
DescrHash.clear Tallying.memo_norm;
let set a i v =
let len = Array.length !a in
if i < len then (!a).(i) <- v
else begin
let b = Array.make (2*len+1) empty in
Array.blit !a 0 b 0 len;
b.(i) <- v;
a := b
end
in
let get a i = if i < 0 then any else (!a).(i) in
let gamma = var (Var.mk "Gamma") in
let cgamma = cons gamma in
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
......@@ -3276,33 +3352,33 @@ let apply_raw s t =
let sl = Tallying.tallying [ (s,t) ] in
let new_res =
Positive.clean_type (
List.fold_left (fun tacc e ->
let res =
Tallying.CS.E.fold (fun var subst acc ->
Positive.substitute acc (var,subst)
) e gamma
in
cap tacc res
List.fold_left (fun tacc si ->
cap tacc (Tallying.(gamma $$ si))
) any sl
)
in
raise (Found(new_res,i,j,sl))
raise (FoundApply(new_res,i,j,sl))
with
Tallying.Step1Fail -> (assert (i == 0 && j == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
| Tallying.Step2Fail -> () (* continue *)
in
let rec loop i =
try
Format.printf "Starting expansion %i @\n@." i;
set ai i (cap (Positive.substitutefree s) (get ai (i-1)));
set aj i (cap (Positive.substitutefree t) (get aj (i-1)));
(* Format.printf "Starting expansion %i @\n@." i; *)
let (ss,tt) =
if i = 0 then (s,t) else
((cap (Positive.substitutefree s) (get ai (i-1))),
(cap (Positive.substitutefree t) (get aj (i-1))))
in
set ai i ss;
set aj i tt;
for j = 0 to i-1 do
tallying j i;
tallying i j;
done;
tallying i i;
loop (i+1)
with Found (res, i, j, sl) -> sl, get ai i, get aj j, res
with FoundApply (res, i, j, sl) -> sl, get ai i, get aj j, res
in
loop 0
......@@ -3313,19 +3389,41 @@ let apply_full s t =
let apply s t = let s,_,_,_ = apply_raw s t in s
let abstr s t =
let ss = Positive.substitutefree s in
let delta = all_vars t in
let sl = Tallying.tallying [(ss,t)] in
List.fold_left (fun acc e ->
let e1 = Tallying.CS.E.filter (fun v _ -> Var.Set.mem v delta) e in
e1 :: acc
) [] sl
(** square subtype *)
let subsqtype s t (sigma,delta) =
List.exists (fun si ->
let si =Tallying.CS.E.filter (fun v _ -> Var.Set.mem v delta) si in
subtype Tallying.(s @@ si) t
) sigma
exception FoundSquareSub of Tallying.CS.sl * bool
let squaresubtype delta s t =
DescrHash.clear Tallying.memo_norm;
assert (Var.Set.is_empty (all_vars t));
let ai = ref [| |] in
let tallying i =
try
let s = get ai i in
let sl = Tallying.tallying ~delta [ (s,t) ] in
let ss =
Positive.clean_type (
List.fold_left (fun acc si ->
cap acc (Tallying.(s $$ si))
) any sl
)
in
raise (FoundSquareSub(sl,subtype ss t))
with
Tallying.Step1Fail -> (assert (i == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
| Tallying.Step2Fail -> () (* continue *)
in
let rec loop i =
try
let ss =
if i = 0 then s
else (cap (Positive.substitutefree s) (get ai (i-1)))
in
set ai i ss;
(*
Format.printf "Starting expansion %i @\n@." i;
Format.printf "%a < %a\n@." Print.print ss Print.print t;
*)
tallying i;
loop (i+1)
with FoundSquareSub (sl,res) -> sl, res
in
loop 0
types/types.mli
View file @ 178030ec
......@@ -419,8 +419,25 @@ module Tallying : sig
val merge : CS.m -> CS.s
val solve : CS.s -> CS.es
val unify : CS.sigma -> CS.sigma
val tallying : (t * t) list -> CS.sl
val (@@) : t -> CS.sigma -> t
(* [s1 ... sn] . si is a solution for tallying problem
if si # delta and for all (s,t) in C si @ s < si @ t *)
val tallying : ?delta : Var.Set.t -> (t * t) list -> CS.sl
val ($$) : t -> CS.sigma -> t
(** Symbolic Substitution Set *)
type symsubst =
|I (** Identity *)
|S of CS.sigma (** Substitution *)
|A of (symsubst * symsubst) (** Composition si (sj t) *)
(** Cartesian Product of two symbolic substitution sets *)
val ( ++ ) : symsubst list -> symsubst list -> symsubst list
(** Evaluation of a substitution *)
val (@@) : t -> symsubst -> t
val domain : CS.sl -> Var.Set.t
val codomain : CS.sl -> Var.Set.t
val is_identity : CS.sl -> bool
......@@ -437,7 +454,7 @@ val apply_full : t -> t -> t
*)
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
(** tallying sigma s < t *)
val abstr : t -> t -> Tallying.CS.sl
val subsqtype : t -> t -> (Tallying.CS.sl * Var.Set.t) -> bool
(** Square Subtype relation. [squaresubtype s t delta sl] .
True if there exists a substitution in sl such that s < t only
considering variables that are not in delta *)
val squaresubtype : Var.Set.t -> t -> t -> (Tallying.CS.sl * bool)
typing/typer.ml
View file @ 178030ec
......@@ -895,7 +895,7 @@ and type_check' loc env ed constr precise = match ed with
if not (Types.subtype t1 acc) then
raise_loc loc (NonExhaustive (Types.diff t1 acc));
let t = type_check_branches loc env t1 a.fun_body t2 false in
(Types.abstr t t2)::tacc (* H_j *)
(fst(Types.squaresubtype env.delta t t2))::tacc (* H_j *)
) [] a.fun_iface
in
List.iter (fun 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