Commit 367c6be1 authored by Pietro Abate's avatar Pietro Abate
Browse files

Minor changes

parent 42341383
......@@ -153,7 +153,6 @@ val cduce2ocaml_fun: ('a -> t) -> (t -> 'b) -> t -> ('a -> 'b)
val print_utf8: U.t -> unit
val add: t -> t -> t
val merge: t -> t -> t
val sub: t -> t -> t
......@@ -169,8 +168,6 @@ val transform: (t -> t) -> t -> t
val xtransform: (t -> t) -> t -> t
val remove_field: label -> t -> t
type pools
val extract_all: unit -> pools
val intract_all: pools -> unit
......@@ -98,11 +98,11 @@ module Print = struct
Format.pp_print_flush ppf ();
Buffer.contents b
let print_lst f ppf l =
let print_lst ?(sep=",") f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a" f h
|h::t -> Format.fprintf ppf "%a,%a" f h aux t
|h::t -> Format.fprintf ppf "%a%s%a" f h sep aux t
in
match l with
|[] -> Format.fprintf ppf ""
......@@ -160,7 +160,7 @@ module Print = struct
Format.fprintf ppf "Match(%a,%a)" pp_typed e pp_branches b
| Subst(e, s) ->
Format.fprintf ppf "Subst(%a,[%a])" pp_typed e pp_typedsigma s
| Op(s, i, l) -> Format.fprintf ppf "(%s, %d, " s i; (print_lst pp_typed ppf l); Format.fprintf ppf ")"
| Op(s, i, l) -> Format.fprintf ppf "(%s, %d, %a)" s i (print_lst pp_typed) l
| _ -> assert false
and pp_abst ppf abstr =
......@@ -195,7 +195,7 @@ module Print = struct
and pp_branch ppf brs =
let f ppf br =
Format.fprintf ppf
"\n{used:%b; ghost:%b; br_vars_poly:[%a];br_vars_empty:[%a];\npat:{%a};\nbody:{typ:%a, descr:%a}}"
"\n{used:%b; ghost:%b; br_vars_poly:{%a};br_vars_empty:[%a];\npat:{%a};\nbody:{typ:%a, descr:%a}}"
br.br_used
br.br_ghost
pp_vars_poly br.br_vars_poly
......@@ -212,9 +212,8 @@ module Print = struct
and pp_fv ppf fv = print_lst pp_v ppf fv
and pp_vars_poly ppf m =
let l = IdMap.fold (fun x s acc -> (x,s)::acc) m [] in
let pp_aux ppf (x,s) = Format.fprintf ppf "%a : %a" Ident.print x Var.Set.print s in
print_lst pp_aux ppf m
print_lst ~sep:";" pp_aux ppf m
let typed_to_string = print_to_string pp_typed
end
......@@ -1143,7 +1143,8 @@ and branches_aux loc env targ tres constr precise = function
(* Xi_j : a map from term variables in the pattern to type variables *)
let xj =
IdMap.fold (fun x t acc ->
IdMap.add x (Var.Set.diff (Types.all_vars t) env'.delta) acc
let s = Var.Set.diff (Types.all_vars t) env'.delta in
if not(Var.Set.is_empty s) then IdMap.add x s acc else acc
) res IdMap.empty
in
(* all poly variables associated with the pattern p_j that are not in \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