Skip to content

GitLab

Commit f54881fa authored by Pietro Abate's avatar Pietro Abate
Browse files

Extend the structure of a polymorphic variable

parent 685c87eb
Hide whitespace changes
Inline Side-by-side
Showing with 167 additions and 85 deletions
parser/ast.ml
View file @ f54881fa
......@@ -103,7 +103,7 @@ and branches = (ppat * pexpr) list
and ppat = ppat' located
and ppat' =
| TVar of Var.t (** polymorphic type variables *)
| TVar of string (** polymorphic type variables *)
| PatVar of U.t list
| Cst of pexpr
| NsT of U.t
......
tests/libtest/boolvarTest.ml
View file @ f54881fa
......@@ -14,7 +14,7 @@ let to_string pp t =
module BoolAtoms : S with type s = Atoms.t = struct
include BoolVar.Make(Atoms)
let mk_var s = atom (`Var s)
let mk_var s = atom (Var.mk s)
let mk_atm s = atom (`Atm (Atoms.atom (Atoms.V.mk_ascii s)))
let to_string = to_string pp_print
end
......
tests/libtest/tallyingTest.ml
View file @ f54881fa
......@@ -21,7 +21,7 @@ module ESet = OUnitDiff.SetMake (struct
if (v1,t1) == (v2,t2) then 0
else let c = Var.compare v1 v2 in if c <> 0 then c
else Types.compare (diff t1 a) (diff t2 a)
let pp_printer ppf (`Var v,t) = Format.fprintf ppf "(%s = %s)" v (to_string Print.print t)
let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %s)" Var.print v (to_string Print.print t)
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
......@@ -43,15 +43,12 @@ module MSet = OUnitDiff.SetMake (struct
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
let mk_pos (alpha,t) = Tallying.CS.singleton (Tallying.Pos (`Var alpha,parse_typ t))
let mk_neg (t,alpha) = Tallying.CS.singleton (Tallying.Neg (parse_typ t,`Var alpha))
type pp = P of vv * string | N of string * vv
and vv = V of string
let mk_pp = function
|P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (`Var alpha,parse_typ t))
|N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,`Var alpha))
|P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
|N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))
let mk_prod l =
List.fold_left (fun acc2 c ->
......@@ -77,8 +74,8 @@ let mk_union_res l1 l2 =
in
let aux l =
List.fold_left (fun acc -> function
|P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,`Var v) (parse_typ s))
|N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,`Var v) (parse_typ s))
|P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,Var.mk v) (parse_typ s))
|N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,Var.mk v) (parse_typ s))
) Tallying.CS.M.empty l
in
match l1,l2 with
......@@ -262,29 +259,33 @@ let test_merge =
let mk_e ll =
List.map (fun l ->
List.map (fun (v,t) -> (`Var v),(parse_typ t)) l
List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
) ll
let tallying_tests = [
[("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
[("A","Int | Bool");("B","Int | Bool")];
[("A","Empty");("B","Empty")]
[(V "A","Int | Bool");(V "B","Int | Bool")];
[(V "A","Empty");(V "B","Empty")]
];
[("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
[("A","Empty")];
[("A","Int");("B","Bool")];
[(V "A","Empty")];
[(V "A","Int");(V "B","Bool")];
];
[("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
[("A","Empty")];
[(V "A","Empty")];
];
[("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
[("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [
[(V "A", "(Int,Int)"); (V "B","Int")]
];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[]];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
[("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [[("A","Int");("B","Int")]];
[("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
[(V "A","Int");(V "B","Int")]
];
]
let test_tallying =
......
tests/libtest/typesTest.ml
View file @ f54881fa
......@@ -14,6 +14,22 @@ let to_string pp t =
Format.flush_str_formatter ()
;;
let variance_test = [
"`$A -> `$B", [("A",`Covariant);("B",`ContraVariant)];
]
let test_variance =
"test variance annotations" >:::
List.map (fun (t1,expected) ->
(Printf.sprintf " %s" t1) >:: (fun _ ->
let t = parse_typ t1 in
assert_equal ~cmp:Types.equal ~printer:(to_string Types.Print.print) t1 t2
)
) set_op_tests
;;
let set_op_tests = [
"Int & `$B", "`$B & Int";
"Int | `$B", "`$B | Int";
......@@ -49,7 +65,7 @@ let test_substitution =
List.map (fun (t,v,s,expected) ->
(Printf.sprintf "[%s]{%s/%s}") t v s >:: (fun _ ->
let t = parse_typ t in
let v = `Var v in
let v = Var.mk v in
let s = parse_typ s in
let expected = parse_typ expected in
let result = Types.subst t (v,s) in
......@@ -76,7 +92,7 @@ let test_rec_subtitutions =
List.map (fun (t,v,expected) ->
(Printf.sprintf "mu X . [%s]{%s/X}") t v >:: (fun _ ->
let t = parse_typ t in
let v = `Var v in
let v = Var.mk v in
let expected = parse_typ expected in
let result = Types.Positive.substitute t v in
assert_equal ~cmp:Types.equiv ~printer:(fun t ->
......
types/types.ml
View file @ f54881fa
......@@ -524,10 +524,10 @@ let get_record r =
let rec substfree_aux subvar t =
let module C ( X : BoolVar.S ) =
struct
let atom_aux ?noderec subvar =
let atom_aux ?noderec subvar_aux =
let open X in function
(* this subvar is acutally specialized on subatoms, subints, etc ... *)
|`Var z -> subvar vars (`Var z)
|`Var z -> subvar_aux vars (`Var z)
|`Atm bdd when X.T.is_empty bdd || X.T.is_full bdd -> atom (`Atm bdd)
|`Atm bdd ->
begin match noderec with
......@@ -536,9 +536,9 @@ let rec substfree_aux subvar t =
end
|_ -> assert false
let subst ?noderec subvar bdd =
let subst ?noderec subvar_aux bdd =
let open X in
let atom z = atom_aux ?noderec subvar z in
let atom z = atom_aux ?noderec subvar_aux z in
compute ~empty ~full:`True ~cup ~cap ~diff ~atom bdd
end
in
......@@ -546,7 +546,6 @@ let rec substfree_aux subvar t =
List.fold_left (fun acc (left,rigth) ->
let deep_subst f l =
List.fold_left (fun acc (t1,t2) ->
(* this subvar is the general one ! *)
let d1 = cons (substfree_aux subvar (descr t1)) in
let d2 = cons (substfree_aux subvar (descr t2)) in
BoolPair.cap acc (f(BoolPair.atom(`Atm (Pair.atom (d1,d2)))))
......@@ -597,24 +596,27 @@ let subst t (v,s) =
(* using a Hashtbl here hides lots of in place modifications *)
(* the hashtbl can be used to remember all substitutions *)
let substfree t =
let subvar tbl v =
try Hashtbl.find tbl v
let subvar tbl z =
try Hashtbl.find tbl z
with Not_found -> begin
let z = Var.fresh () in
Hashtbl.add tbl v z;
z
let v = Var.fresh () in
Hashtbl.add tbl z v;
v
end
in
substfree_aux (subvar (Hashtbl.create 197)) t
(*
(* substitute all variables with s *)
let substvariance t =
let subvar ?(variance=`Variant) (`Var z) =
match variance with
|`Variant -> empty
|`CoVariant -> any
let subvar (`Var t) =
Format.printf "%a\n" Var.dump (`Var t);
match Var.variance (`Var t) with
|`Covariant -> `Constr any
|`ContraVariant -> `Constr empty
|_ -> `Var t
in
substfree subvar t
*)
substfree_aux subvar t
(* Subtyping algorithm *)
let diff_t d t = diff d (descr t)
......@@ -2167,9 +2169,12 @@ struct
decompose_aux atom (BoolAtoms.get t.atoms);
decompose_aux interval (BoolIntervals.get t.ints);
decompose_aux char (BoolChars.get t.chars);
decompose_aux ~noderec:(subpairs arrow) (fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) (BoolPair.get t.arrow);
decompose_aux ~noderec:(subpairs xml) (fun p -> { empty with xml = BoolPair.atom (`Atm p) }) (BoolPair.get t.xml);
decompose_aux ~noderec:(subpairs times) (fun p -> { empty with times = BoolPair.atom (`Atm p) }) (BoolPair.get t.times);
decompose_aux ~noderec:(subpairs arrow)
(fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) (BoolPair.get t.arrow);
decompose_aux ~noderec:(subpairs xml)
(fun p -> { empty with xml = BoolPair.atom (`Atm p) }) (BoolPair.get t.xml);
decompose_aux ~noderec:(subpairs times)
(fun p -> { empty with times = BoolPair.atom (`Atm p) }) (BoolPair.get t.times);
]
let solve v = internalize (make_node v)
......@@ -2407,11 +2412,11 @@ module Tallying = struct
end)
let print ppf m =
print_lst (fun ppf -> fun ((b,`Var v),s) ->
print_lst (fun ppf -> fun ((b,v),s) ->
if b then
Format.fprintf ppf "(`$%s <= %a)" v Print.print s
Format.fprintf ppf "(%a <= %a)" Var.print v Print.print s
else
Format.fprintf ppf "(%a <= `$%s)" Print.print s v
Format.fprintf ppf "(%a <= %a)" Print.print s Var.print v
) ppf (bindings m);
end
......@@ -2425,8 +2430,8 @@ module Tallying = struct
end)
let print ppf e =
print_lst (fun ppf -> fun (`Var v,t) ->
Format.fprintf ppf "`$%s = %a@," v Print.print t
print_lst (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.print v Print.print t
) ppf (bindings e)
end
......@@ -2737,12 +2742,12 @@ module Tallying = struct
let aux v (s,t) acc =
if CS.E.mem v acc then assert false else
if equal s empty && equal t any then
let b = var (Var.fresh ()) in
let b = var (Var.fresh ~variance:(Var.variance v) ()) in
CS.E.add v b acc
else if equal t empty then CS.E.add v empty acc
else if equal s any then CS.E.add v t acc
else
let b = var (Var.fresh ()) in
let b = var (Var.fresh ~variance:(Var.variance v) ()) in
CS.E.add v (cap (cup s b) t) acc
in
let aux m =
......@@ -2777,37 +2782,52 @@ module Tallying = struct
if CS.E.is_empty e then sol
else
let ((`Var v as alpha),t) = CS.E.max_binding e in
Format.printf "%s = %a\n" v Print.print t;
let e1 = CS.E.remove alpha e in
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh *)
(* Positive.transform : Descr.s -> Positive.t
* and then Positive.solve on the result ... *)
let es = CS.E.fold (fun beta s acc -> CS.E.add beta (subst s (alpha,t)) acc) e1 CS.E.empty in
aux ((CS.E.add alpha t sol),(CS.E.add alpha (subst t (alpha,t)) acc)) es
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* XXX : substvariance remove all previously introduced fresh variables *)
let x = substvariance (Positive.substitute t alpha) in
let es = CS.E.fold (fun beta s acc -> CS.E.add beta (subst s (alpha,x)) acc) e1 CS.E.empty in
aux ((CS.E.add alpha x sol),(CS.E.add alpha x acc)) es
in
aux (CS.E.empty,CS.E.empty) e
exception Step1Fail
exception Step2Fail
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.S.empty l in
if CS.S.is_empty n then raise UnSatConstr else
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
if CS.ES.is_empty m then raise UnSatConstr else
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)
end
exception KeepGoing
let appl t1 t2 =
let rec aux card s t =
let gamma = var (Var.fresh ()) in
(* create t1,t2 by increasing the cardinality ... ??? *)
let t1 = s and t2 = t in
let l = [(t1,arrow (cons t2) (cons gamma))] in
try Tallying.tallying l
with Tallying.UnSatConstr ->
if card >= 10 then assert false
else aux (card+1) t1 t2
let q = Queue.create () in
let gamma = var (Var.fresh ()) in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
Print.print Format.std_formatter acc1;
Print.print Format.std_formatter acc2;
try Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]
with
|Tallying.Step1Fail -> raise Tallying.UnSatConstr
|Tallying.Step2Fail -> begin
Queue.add (aux (i+1,(cap acc1 (substfree t1))) (j,acc2) t1 t2) q;
Queue.add (aux (i,acc1) (j+1,(cap acc2 (substfree t2))) t1 t2) q;
raise KeepGoing
end
in
aux 0 t1 t2
Queue.add (aux (0,t1) (1,(substfree t2)) t1 t2) q;
Queue.add (aux (1,(substfree t1)) (0,t2) t1 t2) q;
let result = ref [] in
while not(Queue.is_empty q) do
try result := (Queue.pop q) ();
with KeepGoing -> ()
done;
!result
types/var.ml
View file @ f54881fa
type t = String.t
type t = {
mutable variance : [ `Covariant | `ContraVariant | `Both | `None ] ;
fresh : bool;
id : String.t;
}
let make_id ?(fresh=false) ?(variance=`None) id =
{ id = id ; variance = variance; fresh = fresh }
let dump ppf t =
let to_string = function
|`ContraVariant -> "contravariant"
|`Covariant -> "covariant"
|`Both -> "invariant"
|`None -> "indetermined"
in
Format.fprintf ppf "{id=%s;variance=%s;fresh=%b}" t.id (to_string t.variance) t.fresh
let compare x y = Pervasives.compare x.id y.id
let equal x y = Pervasives.compare x.id y.id = 0
let hash x = Hashtbl.hash x.id
type var = [ `Var of t ]
type 'a pairvar = [ `Atm of 'a | var ]
let compare (x : var) (y : var) = Pervasives.compare x y
let equal x y = Pervasives.compare x y = 0
let hash (v : var) = Hashtbl.hash v
let dump ppf (`Var x) = Format.fprintf ppf "%a" dump x
let print ppf (`Var x) = Format.fprintf ppf "`$%s" x.id
let compare (`Var x) (`Var y) = compare x y
let equal v1 v2 = (compare v1 v2) = 0
let ch_variance variance (`Var t) =
match t.variance,variance with
|`None,_ -> `Var { t with variance = variance }
|`Both ,_ -> `Var t
|`ContraVariant,`ContraVariant
|`Covariant,`Covariant -> `Var t
|_,_ -> `Var { t with variance = `Both }
let variance (`Var t) = t.variance
module Set = Set.Make(
struct
type t = var
let compare = compare
end)
module Make (X : Custom.T) = struct
type t = X.t pairvar
let hash = function `Atm t -> X.hash t | `Var s -> hash (`Var s)
let hash = function `Atm t -> X.hash t | `Var x -> hash x
let check = function `Atm t -> X.check t | `Var _ -> ()
let compare t1 t2 =
match t1,t2 with
......@@ -22,18 +59,17 @@ module Make (X : Custom.T) = struct
let dump ppf = function
|`Atm x -> X.dump ppf x
|`Var x -> Format.fprintf ppf "`$%s" x
|`Var x -> print ppf (`Var x)
end
let fresh : unit -> var =
let mk ?fresh ?variance id =
`Var (make_id ?fresh ?variance id)
let fresh ?variance : unit -> [> var ] =
let counter = ref 0 in
fun _ ->
let v = `Var (Printf.sprintf "_fresh_%d" !counter) in
let id = (Printf.sprintf "_fresh_%d" !counter) in
let v = mk ~fresh:true ?variance id in
incr counter;
v
module Set = Set.Make(
struct
type t = var
let compare = Pervasives.compare
end)
typing/typer.ml
View file @ f54881fa
......@@ -288,9 +288,10 @@ module IType = struct
type penv = {
penv_tenv : t;
penv_derec : node Env.t;
penv_var : (string, Var.var) Hashtbl.t;
}
let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty }
let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty ; penv_var = Hashtbl.create 17 }
let all_delayed = ref []
......@@ -309,8 +310,17 @@ module IType = struct
all_delayed := [];
List.iter check_one_delayed l
let rec derecurs env p = match p.descr with
| TVar v -> mk_type (Types.var (`Var v))
let rec derecurs ?(variance=`Covariant) env p = match p.descr with
| TVar s -> begin
try
let v = Hashtbl.find env.penv_var s in
mk_type (Types.var (Var.ch_variance variance v))
with Not_found -> begin
let v = Var.mk ~variance s in
Hashtbl.add env.penv_var s v;
mk_type (Types.var v)
end
end
| PatVar ids -> derecurs_var env p.loc ids
| Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
| Internal t -> mk_type t
......@@ -321,7 +331,7 @@ module IType = struct
| Diff (p1,p2) -> mk_diff (derecurs env p1) (derecurs env p2)
| Prod (p1,p2) -> mk_prod (derecurs env p1) (derecurs env p2)
| XmlT (p1,p2) -> mk_xml (derecurs env p1) (derecurs env p2)
| Arrow (p1,p2) -> mk_arrow (derecurs env p1) (derecurs env p2)
| Arrow (p1,p2) -> mk_arrow (derecurs env p1) (derecurs ~variance:`ContraVariant env p2)
| Optional p -> mk_optional (derecurs env p)
| Record (o,r) ->
let aux = function
......@@ -370,8 +380,7 @@ module IType = struct
(v,p,delayed loc))
b in
let n =
List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
let n = List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
let env = { env with penv_derec = n } in
List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
(env, b)
......
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