Commit 692a2904 authored by Pietro Abate's avatar Pietro Abate

Account for polymorphic variables in patterns

parent 04a5751b
......@@ -197,7 +197,7 @@ and parse_branches env l toptype acc btype = function
br_used = br_used;
br_ghost = false;
br_vars_empty = [];
br_vars_poly = [];
br_vars_poly = Var.Set.empty;
br_pat = tpat;
br_body = br_body}
in
......
......@@ -97,9 +97,10 @@ and pp_branches ppf brs =
and pp_branch ppf brs =
let f ppf br =
Format.fprintf ppf
"\n{used:%b; ghost:%b; 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.Typed.br_used
br.Typed.br_ghost
Var.Set.print br.Typed.br_vars_poly
pp_fv br.Typed.br_vars_empty
pp_node br.Typed.br_pat
Types.Print.print br.Typed.br_body.Typed.exp_typ
......
......@@ -3007,7 +3007,8 @@ module Tallying = struct
(* if we already evaluated it, it is sat *)
if DescrSet.mem t mem || is_empty t then begin
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end else begin
CS.sat end
else begin
if is_empty t then CS.sat
(* if there is only one variable then is it A <= 0 or 1 <= A *)
else if is_var t then
......
......@@ -84,7 +84,7 @@ and branch = {
mutable br_used : bool;
br_ghost : bool;
mutable br_vars_empty : fv;
mutable br_vars_poly : fv;
mutable br_vars_poly : Var.Set.t;
br_pat : tpat;
(* this field is mutable because we need to add substitutions *)
mutable br_body : texpr
......
......@@ -50,7 +50,7 @@ type item =
type t = {
ids : item Env.t;
delta : fv;
delta : Var.Set.t;
gamma : Types.Node.t id_map;
ns: Ns.table;
keep_ns: bool
......@@ -107,7 +107,7 @@ let type_schema env loc name uri =
let empty_env = {
ids = Env.empty;
delta = IdSet.empty; (* set of bounded type variables *)
delta = Var.Set.empty; (* set of bounded type variables *)
gamma = IdMap.empty; (* map from expression variables to types *)
ns = Ns.def_table;
keep_ns = false
......@@ -595,14 +595,14 @@ and if_then_else loc cond yes no =
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_vars_poly = Fv.empty;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_pat = pat_true;
Typed.br_body = yes };
{ Typed.br_loc = no.Typed.exp_loc;
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_vars_poly = Fv.empty;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_pat = pat_false;
Typed.br_body = no } ];
Typed.br_accept = Builtin_defs.bool;
......@@ -728,7 +728,7 @@ and branches env b =
Typed.br_used = ghost;
Typed.br_ghost = ghost;
Typed.br_vars_empty = fvp;
Typed.br_vars_poly = Fv.empty;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_pat = p;
Typed.br_body = e } in
cur_branch := Branch (br, !cur_branch) :: cur_br;
......@@ -771,7 +771,7 @@ and select_from_where env loc e from where =
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = fvp;
Typed.br_vars_poly = Fv.empty;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_pat = p;
Typed.br_body = rest } in
cur_branch := [ Branch (br, !cur_branch) ];
......@@ -1129,7 +1129,15 @@ and branches_aux loc env targ tres constr precise = function
let env' = enter_values (IdMap.get res) env in
let xj = IdMap.domain (IdMap.restrict env'.gamma env'.delta) in (* Xi_j *)
(* Xi_j *)
let xj =
let pattpolyvars =
List.fold_left (fun acc (_,t) ->
Var.Set.union acc (Types.all_vars (Types.descr t))
) Var.Set.empty env'.gamma
in
Var.Set.diff pattpolyvars env'.delta
in
(* all poly variables associated with the pattern p_j that are not in \Delta *)
b.br_vars_poly <- xj;
......
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