Commit 52396db6 authored by Pietro Abate's avatar Pietro Abate

More cleanup in the variable module

- New fresh variables now share the same str, but different freshness index
- Remove the function is_internal from var module
parent 810d01bb
......@@ -2746,29 +2746,27 @@ module Positive = struct
let substitute_aux delta v subst =
let memo = MemoHash.create 17 in
let rec aux v subst =
try
MemoHash.find memo v
with
Not_found -> begin
let node_v = forward () in
MemoHash.add memo v node_v;
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)
|`Times (v1,v2) -> `Times (aux v1 subst, aux v2 subst)
|`Arrow (v1,v2) -> `Arrow (aux v1 subst, aux v2 subst)
|`Xml (v1,v2) -> `Xml (aux v1 subst, aux v2 subst)
|`Record (b, flst) ->
`Record (b, List.map (fun (b,l,v) -> (b,l,aux v subst)) flst)
|`Neg v -> `Neg (aux v subst)
in
node_v.def <- new_v;
node_v
end
try MemoHash.find memo v
with Not_found -> begin
let node_v = forward () in
MemoHash.add memo v node_v;
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)
|`Times (v1,v2) -> `Times (aux v1 subst, aux v2 subst)
|`Arrow (v1,v2) -> `Arrow (aux v1 subst, aux v2 subst)
|`Xml (v1,v2) -> `Xml (aux v1 subst, aux v2 subst)
|`Record (b, flst) ->
`Record (b, List.map (fun (b,l,v) -> (b,l,aux v subst)) flst)
|`Neg v -> `Neg (aux v subst)
in
node_v.def <- new_v;
node_v
end
in
aux v subst
......@@ -2803,12 +2801,9 @@ module Positive = struct
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
let substituterec t alpha =
let subst x d =
if Var.equal d alpha then x
else var d
in
if no_var t then t
else begin
let subst x d = if Var.equal d alpha then x else var d in
let x = forward () in
define x (substitute_aux Var.Set.empty (decompose t) (subst x));
descr(solve x)
......@@ -2823,16 +2818,13 @@ module Positive = struct
descr (solve new_t)
end
let substitutefree delta =
let idx = ref 0 in
fun t -> if no_var t then t else
let substitutefree delta t =
if no_var t then t else
let h = Hashtbl.create 17 in
let subst h d =
try Hashtbl.find h d
with Not_found -> begin
let id = Printf.sprintf "_%s_%d" (Var.id d) !idx in
let x = var (Var.mk ~repr:(Var.id d) id) in
incr idx;
let x = var (Var.fresh d) in
Hashtbl.add h d x ;
x
end
......@@ -2871,12 +2863,16 @@ module Positive = struct
let t_emp = cup [] in
let t_any = cap [] in
let idx = ref 0 in
let is_internal x =
let s = Var.id x in
String.length s >= 1 && s.[0] == '#'
in
let rec aux pos v =
if not (Memo.mem memo (pos, v)) then
let () = Memo.add memo (pos,v) () in
match v.def with
|`Type d -> ()
|`Variable d when Var.Set.mem d delta || (not (Var.is_internal d) && not pos) -> Hashtbl.replace vars d v
|`Variable d when Var.Set.mem d delta || (not (is_internal d) && not pos) -> Hashtbl.replace vars d v
|`Variable d ->
begin try
let td = Hashtbl.find vars d in
......@@ -3397,9 +3393,9 @@ module Tallying = struct
let aux alpha (s,t) acc =
(* we cannot solve twice the same variable *)
assert(not(CS.E.mem alpha acc));
let pre = Printf.sprintf "#fr_%s_" (Var.id alpha) in
let b = var (Var.fresh ~pre ()) in
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
let v = Var.mk (Printf.sprintf "#fr_%s" (Var.id alpha)) in
let b = var v in
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
CS.E.add alpha (cap (cup s b) t) acc
in
let aux1 m =
......
module V = struct
type t = { id : string; repr : string }
let dump ppf t =
let r = if t.repr = t.id then "" else Format.sprintf ";repr=%s" t.repr in
Format.fprintf ppf "{id=%s;%s}" t.id r
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 t = { id : string ; fr : int }
let dump ppf t = Format.fprintf ppf "{%s(%d)}" t.id t.fr
let compare x y = Pervasives.compare (x.id,x.fr) (y.id,y.fr)
let equal x y = (compare x y) = 0
let hash x = Hashtbl.hash (x.id,x.fr)
let check _ = ()
let id x = x.id
let is_internal x =
let s = x.repr in
String.length s >= 1 && s.[0] == '#'
let id x = x.id
let is_fresh x = x.fr > 0
let make_id ?repr id =
match repr with
|None -> { id = id ; repr = id }
|Some r -> { id = id ; repr = r }
let mk id = { id = id ; fr = 0 }
let mk ?repr id = make_id ?repr id
let pp ppf x =
let pre = if x.fr == 0 then "" else (Printf.sprintf "_fresh_%d" x.fr) in
Format.fprintf ppf "'%s%s" x.id pre
let pp ppf x = Format.fprintf ppf "'%s" x.repr
let fresh : ?pre: string -> unit -> t =
let counter = ref 0 in
fun ?(pre="_fresh_") -> fun _ ->
let id = (Printf.sprintf "%s%d" pre !counter) in
let v = mk id in
incr counter;
v
let fresh v = { v with fr = v.fr + 1 }
end
include V
......
......@@ -3,10 +3,13 @@ include Custom.T
type var = t
val pp : Format.formatter -> t -> unit
val mk : ?repr:string -> string -> t
val fresh : ?pre:string -> unit -> t
val mk : string -> t
val id : t -> string
val fresh : t -> t
val is_fresh : t -> bool
(*
val is_internal : t -> bool
*)
module Set : sig
include Custom.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