Commit 727e0b21 authored by Pietro Abate's avatar Pietro Abate

propagate delta in Types.Positive.substfree

parent 9a8eface
......@@ -1800,6 +1800,11 @@ struct
let add u = slot.def <- u :: slot.def in
(*
alpha ^ ( union )
alpha / ( union ) only if alpha is not present in at most 2
*)
let prepare_boolvar get is_full print tlv bdd =
let ll =
List.fold_left (fun acc (p,n) ->
......@@ -2528,7 +2533,7 @@ struct
let equal u v = u == v
end )
let substitute_aux v subst =
let substitute_aux delta v subst =
let memo = MemoHash.create 17 in
let rec aux v subst =
try
......@@ -2540,6 +2545,7 @@ struct
let new_v =
match v.def with
|`Type d -> `Type d
|`Variable d when Var.Set.mem d delta -> v.def
|`Variable d -> (subst d).def
|`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl)
|`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl)
......@@ -2594,7 +2600,7 @@ struct
if no_var t then t
else begin
let x = forward () in
define x (substitute_aux (decompose t) (subst x));
define x (substitute_aux Var.Set.empty (decompose t) (subst x));
descr(solve x)
end
......@@ -2602,11 +2608,11 @@ struct
if no_var t then t
else begin
let subst s d = if Var.equal d alpha then s else var d in
let new_t = (substitute_aux (decompose t) (subst (ty s))) in
let new_t = (substitute_aux Var.Set.empty (decompose t) (subst (ty s))) in
descr (solve new_t)
end
let substitutefree =
let substitutefree delta =
let idx = ref 0 in
fun t -> if no_var t then t else
let h = Hashtbl.create 17 in
......@@ -2621,7 +2627,7 @@ struct
end
in
let dec = decompose t in
let new_t = substitute_aux dec (subst h) in
let new_t = substitute_aux delta dec (subst h) in
descr (solve new_t)
(* We cannot use the variance annotation of variables to simplify them,
......@@ -2685,7 +2691,7 @@ struct
let dec = decompose t in
let h = collect_variables delta dec in
let new_t =
substitute_aux dec (fun d ->
substitute_aux delta dec (fun d ->
try Hashtbl.find h d
with Not_found -> assert false
)
......@@ -3345,7 +3351,7 @@ let squaresubtype delta s t =
try
let ss =
if i = 0 then s
else (cap (Positive.substitutefree s) (get ai (i-1)))
else (cap (Positive.substitutefree delta s) (get ai (i-1)))
in
set ai i ss;
(*
......@@ -3393,8 +3399,8 @@ let apply_raw delta s t =
(* 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))))
((cap (Positive.substitutefree delta s) (get ai (i-1))),
(cap (Positive.substitutefree delta t) (get aj (i-1))))
in
set ai i ss;
set aj i tt;
......
......@@ -168,7 +168,7 @@ sig
val substitute : t -> (Var.var * t) -> t
val substituterec : t -> Var.var -> t
val solve: v -> Node.t
val substitutefree : t -> t
val substitutefree : Var.Set.t -> t -> t
end
(** Normalization **)
......
......@@ -952,7 +952,7 @@ and type_check' loc env ed constr precise = match ed with
| Apply (e1,e2) ->
let t1 = type_check env e1 Types.Arrow.any true in
let t1arrow = Types.Arrow.get t1 in
let t1 = Types.Positive.substitutefree t1 in
let t1 = Types.Positive.substitutefree env.delta t1 in
(* t [_delta 0 -> 1 *)
begin try
......
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