Commit af8cccfd authored by Pietro Abate's avatar Pietro Abate

Minor Changes

parent 52396db6
......@@ -12,10 +12,12 @@ type env = {
}
let pp_vars ppf vars =
Ident.pp_env Lambda.Print.pp_vloc ppf vars
let pp_item ppf (s,t) = Format.fprintf ppf "%s : %a" s Lambda.Print.pp_vloc t in
Ident.pp_env pp_item ppf vars
let pp_xi ppf xi =
Ident.pp_idmap Var.Set.pp ppf xi
let pp_item ppf (s,t) = Format.fprintf ppf "%s : %a" s Var.Set.pp t in
Ident.pp_idmap pp_item ppf xi
let pp_env ppf env =
Format.fprintf ppf "{vars=%a,sigma=%a,xi=%a}"
......
(* Typing environment with built-in types *)
val env: Typer.t
(* Typing environment with built-in types *)
val argv: Value.t ref
......@@ -22,9 +22,9 @@ type label = Ns.Label.t
type 'a label_map = 'a LabelMap.map
let pp_env f ppf env =
let f ppf (e,v) = Format.fprintf ppf "%a:%a" print e f v in
let f ppf (e,v) = f ppf ((Id.to_string e),v) in
Utils.pp_list ~delim:("<",">") ~sep:";" f ppf (Env.bindings env)
let pp_idmap f ppf map =
let f ppf (e,v) = Format.fprintf ppf "%a:%a" print e f v in
let f ppf (e,v) = f ppf ((Id.to_string e),v) in
Utils.pp_list ~delim:("<",">") ~sep:";" f ppf (IdMap.get map)
......@@ -2629,6 +2629,39 @@ module Positive = struct
]
and v = { mutable def : rhs; mutable node : node option }
module MemoHash = Hashtbl.Make( struct
type t = v
let hash = Hashtbl.hash
let equal u v = u == v
end )
let pp ppf v =
let id = ref 0 in
let memo = MemoHash.create 17 in
let rec aux ppf v =
try
let s = MemoHash.find memo v in
Format.fprintf ppf "%s" s
with Not_found -> begin
let node_name = Printf.sprintf "X_%i" !id in
incr id;
MemoHash.add memo v node_name;
match v.def with
|`Type d -> Format.fprintf ppf "`Type(%a)" Print.pp_type d
|`Variable d -> Format.fprintf ppf "`Var(%a)" Var.pp d
|`Cup vl -> Format.fprintf ppf "`Cup(%a)" (Utils.pp_list aux) vl
|`Cap vl -> Format.fprintf ppf "`Cap(%a)" (Utils.pp_list aux) vl
|`Times (v1,v2) -> Format.fprintf ppf "`Times(%a,%a)" aux v1 aux v2
|`Arrow (v1,v2) -> Format.fprintf ppf "`Arrow(%a,%a)" aux v1 aux v2
|`Xml (v1,v2) -> Format.fprintf ppf "`Xml(%a,%a)" aux v1 aux v2
|`Record _ -> Format.fprintf ppf "`Record"
|`Neg v -> Format.fprintf ppf "`Neg(%a)" aux v
end
in
aux ppf v
let printf = pp Format.std_formatter
let rec make_descr seen v =
if List.memq v seen then empty
else
......@@ -2675,17 +2708,17 @@ module Positive = struct
let decompose t =
let memo = DescrHash.create 17 in
let decompose_conj f_atom sign ilist acc =
let decompose_conj acc f_atom sign ilist acc =
List.fold_left (fun acc e ->
let ne = f_atom e in
(sign ne) :: acc) acc ilist
(sign ne) :: acc
) acc ilist
in
let decompose_dnf t_any f_atom dnf acc =
List.fold_left (fun acc (ipos, ineg) ->
match
decompose_conj f_atom neg ineg
@@ decompose_conj f_atom (fun x -> x) ipos [t_any]
with
let lacc = decompose_conj [] f_atom neg ineg in
let lacc = decompose_conj lacc f_atom (fun x -> x) ipos [t_any] in
match lacc with
| [v] -> v::acc
| l -> (cap l) :: acc) acc dnf
in
......@@ -2713,35 +2746,27 @@ module Positive = struct
cup (decompose_dnf (ty any) (fun (b, l) ->
make b (format_rec b [] (LabelMap.get l))) (Rec.get bdd) [])) dnf acc
and decompose_type t =
try
DescrHash.find memo t
with
Not_found ->
let node_t = forward () in
if no_var t then ty t
else
let () = DescrHash.add memo t node_t in
let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
@@ decompose_kind Int.any interval (BoolIntervals.get t.ints)
@@ decompose_kind Char.any char (BoolChars.get t.chars)
@@ decompose_bdd Product.any times (BoolPair.get t.times)
@@ decompose_bdd Product.any_xml xml (BoolPair.get t.xml)
@@ decompose_bdd Arrow.any arrow (BoolPair.get t.arrow)
@@ decompose_rec Record.any record (BoolRec.get t.record)
@@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
in
node_t.def <- (cup descr_t).def; node_t
try DescrHash.find memo t
with Not_found ->
let node_t = forward () in
if no_var t then ty t
else
let () = DescrHash.add memo t node_t in
let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
@@ decompose_kind Int.any interval (BoolIntervals.get t.ints)
@@ decompose_kind Char.any char (BoolChars.get t.chars)
@@ decompose_bdd Product.any times (BoolPair.get t.times)
@@ decompose_bdd Product.any_xml xml (BoolPair.get t.xml)
@@ decompose_bdd Arrow.any arrow (BoolPair.get t.arrow)
@@ decompose_rec Record.any record (BoolRec.get t.record)
@@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
in
node_t.def <- (cup descr_t).def; node_t
in
decompose_type t
let solve v = internalize (make_node v)
module MemoHash = Hashtbl.Make(
struct
type t = v
let hash = Hashtbl.hash
let equal u v = u == v
end )
let substitute_aux delta v subst =
let memo = MemoHash.create 17 in
......@@ -2770,34 +2795,6 @@ module Positive = struct
in
aux v subst
let pp ppf v =
let id = ref 0 in
let memo = MemoHash.create 17 in
let rec aux ppf v =
try
let s = MemoHash.find memo v in
Format.fprintf ppf "%s" s
with Not_found -> begin
let node_name = Printf.sprintf "X_%i" !id in
incr id;
MemoHash.add memo v node_name;
match v.def with
|`Type d -> Format.fprintf ppf "`Type(%a)" Print.pp_type d
|`Variable d -> Format.fprintf ppf "`Var(%a)" Var.pp d
|`Cup vl -> Format.fprintf ppf "`Cup(%a)" (Utils.pp_list aux) vl
|`Cap vl -> Format.fprintf ppf "`Cap(%a)" (Utils.pp_list aux) vl
|`Times (v1,v2) -> Format.fprintf ppf "`Times(%a,%a)" aux v1 aux v2
|`Arrow (v1,v2) -> Format.fprintf ppf "`Arrow(%a,%a)" aux v1 aux v2
|`Xml (v1,v2) -> Format.fprintf ppf "`Xml(%a,%a)" aux v1 aux v2
|`Record _ -> Format.fprintf ppf "`Record"
|`Neg v -> Format.fprintf ppf "`Neg(%a)" aux v
end
in
aux ppf v
let printf = pp Format.std_formatter
let dump ppf t = pp ppf (decompose t)
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
let substituterec t alpha =
......@@ -2836,7 +2833,7 @@ module Positive = struct
(* We cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
latter but the variance annotation tells us that A is invariant. *)
latter but the variance annotation tells us that A is invariant. *)
let collect_variables delta v =
(* we memoize based on the pair (pos, v), since v can occur both
positively and negatively. and we want to manage the variables
......@@ -2872,15 +2869,16 @@ module Positive = struct
let () = Memo.add memo (pos,v) () in
match v.def with
|`Type d -> ()
|`Variable d when Var.Set.mem d delta || (not (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
(* polarity conflict, replace the binding by a new, pretty-printed variable *)
if ((td == t_emp) && not pos) || ((td == t_any) && pos)
then Hashtbl.replace vars d (var(freshvar idx))
(* first time we see a variable, set to empty for covariant and
any for contravariant *)
(* first time we see a variable, set to empty for covariant and
any for contravariant *)
with Not_found -> Hashtbl.add vars d (if pos then t_emp else t_any) end
|`Cup vl | `Cap vl -> List.iter (fun v -> aux pos v) vl
|`Times (v1,v2) | `Xml (v1, v2) -> (aux pos v1); (aux pos v2)
......@@ -2909,6 +2907,7 @@ module Positive = struct
if no_var t then t else
clean_variables delta t
let dump ppf t = pp ppf (decompose t)
end
......
......@@ -12,8 +12,10 @@ module V = struct
let mk id = { id = id ; fr = 0 }
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
*)
Format.fprintf ppf "'%s" x.id
let fresh v = { v with fr = v.fr + 1 }
end
......
......@@ -56,17 +56,25 @@ type t = {
}
let pp_env ppf env =
let pp_item ppf = function
|Type t | Val t -> Types.Print.pp_type ppf t
(*
|ECDuce _ -> Format.fprintf ppf "ECDuce"
|ESchema _ -> Format.fprintf ppf "ESchema"
|ENamespace _ -> Format.fprintf ppf "ENamespace"
*)
let pp_item ppf (s,t) = match t with
|Val t -> Format.fprintf ppf "val %s : %a" s Types.Print.pp_type t
|Type t -> Format.fprintf ppf "type %s = %a" s Types.Print.pp_type t
|_ -> ()
in
let t = [
"Empty";"Any";"Int";"Char";"Byte";"Atom";
"Pair";"Arrow";"Record";
"String";"Latin1";
"Bool";"Float";"AnyXml";
"Namespaces";"Caml_int" ]
in
let ids =
Env.filter (fun n _ ->
not(List.mem (Id.to_string n) t)
) env.ids
in
Format.printf "{ids=%a;delta=%a}"
(Ident.pp_env pp_item) env.ids
(Ident.pp_env pp_item) ids
Var.Set.pp env.delta
;;
......
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