Skip to content

GitLab

C
cduce
Commit 083edd02 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files
Options

Seal the representation of SortedList.Make(X).t (by making the type private).... 

Seal the representation of SortedList.Make(X).t (by making the type private). Expose Var.Set as a SortedList.S
parent f217bc26
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 216 additions and 156 deletions
compile/compile.ml
View file @ 083edd02
......@@ -76,13 +76,13 @@ let enter_global_cu cu env x =
let rec domain = function
|Identity -> Var.Set.empty
|List l -> Types.Tallying.domain l
|Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|Comp (s1,s2) -> Var.Set.cup (domain s1) (domain s2)
|Sel(_,_,sigma) -> (domain sigma)
let rec codomain = function
| Identity -> Var.Set.empty
| List(l) -> Types.Tallying.codomain l
| Comp(s1,s2) -> Var.Set.union (codomain s1) (codomain s2)
| Comp(s1,s2) -> Var.Set.cup (codomain s1) (codomain s2)
| Sel(_,_,sigma) -> (codomain sigma)
let fresharg =
......@@ -111,7 +111,7 @@ let rec comp s1 s2 = match s1, s2 with
| res -> comp s3 (comp res s6))
(* If a variable in the image of s2 is in the domain of s1 we can't simplify *)
| _, _ when not (Var.Set.is_empty (Var.Set.inter (domain s1) (codomain s2)))
| _, _ when not (Var.Set.is_empty (Var.Set.cap (domain s1) (codomain s2)))
-> Comp(s1, s2)
| List(_), List(_) | Sel(_), List(_) ->
......@@ -135,8 +135,8 @@ and compile_aux env te = function
let is_mono x =
if Var.Set.is_empty ts then true else
let from_xi = try IdMap.assoc x env.xi with Not_found -> Var.Set.empty in
let d = Var.Set.inter from_xi (domain(env.sigma)) in
Var.Set.is_empty (Var.Set.inter ts d)
let d = Var.Set.cap from_xi (domain(env.sigma)) in
Var.Set.is_empty (Var.Set.cap ts d)
in
if is_mono x then Var (v) else TVar(v,env.sigma)
| Typed.Subst(e,sl) ->
......@@ -193,15 +193,15 @@ and compile_abstr env a =
List.fold_left(fun acc (t1,t2) ->
let ts1 = Types.all_vars t1 in
let ts2 = Types.all_vars t2 in
let tu = Var.Set.union ts1 ts2 in
Var.Set.union acc tu
let tu = Var.Set.cup ts1 ts2 in
Var.Set.cup acc tu
) Var.Set.empty a.Typed.fun_iface
in
if Var.Set.is_empty vars then true else
if env.sigma = Identity then false
else
let d = domain(env.sigma) in
Var.Set.is_empty (Var.Set.inter d vars)
Var.Set.is_empty (Var.Set.cap d vars)
in
let (slots,nb_slots,fun_env) =
(* we add a nameless empty slot for the argument *)
......@@ -258,7 +258,7 @@ and compile_branches env (brs : Typed.branches) =
(* p_i / t_i -> br.Typed.br_pat / br.Typed.br_type *)
and compile_branch env br =
let env = List.fold_left enter_local env (Patterns.fv br.Typed.br_pat) in
let env = List.fold_left enter_local env (IdSet.get (Patterns.fv br.Typed.br_pat)) in
let env =
{ env with
xi = IdMap.merge (fun _ v2 -> v2) env.xi br.Typed.br_vars_poly
......@@ -278,7 +278,7 @@ let compile_expr env e =
let compile_let_decl env decl =
let pat = decl.Typed.let_pat in
let e,lsize = compile_expr env decl.Typed.let_body in
let env = enter_globals env (Patterns.fv pat) in
let env = enter_globals env (IdSet.get (Patterns.fv pat)) in
let te = decl.Typed.let_body.Typed.exp_typ in
let comp = Patterns.Compile.make_branches te [ pat, () ] in
......
depend
View file @ 083edd02
......@@ -371,7 +371,7 @@ types/intervals.cmi : misc/custom.cmo
types/chars.cmi : misc/custom.cmo
types/atoms.cmi : misc/ns.cmi misc/encodings.cmi misc/custom.cmo
types/normal.cmi :
types/var.cmi : misc/custom.cmo
types/var.cmi : types/sortedList.cmi misc/custom.cmo
types/boolVar.cmi : types/var.cmi misc/custom.cmo
types/types.cmi : types/var.cmi misc/ns.cmi types/intervals.cmi \
types/ident.cmo misc/custom.cmo types/chars.cmi types/boolVar.cmi \
......
misc/custom.ml
View file @ 083edd02
......@@ -108,20 +108,20 @@ module Array(X : T) = struct
end
module List(X : T) = struct
module Elem = X
type t = X.t list
let dump = dump_list X.dump
let check l = List.iter X.check l
module Elem : T with type t = X.t = X
type t = Elem.t list
let dump = dump_list Elem.dump
let check l = List.iter Elem.check l
let rec equal l1 l2 =
(l1 == l2) ||
match (l1,l2) with
| x1::l1, x2::l2 -> (X.equal x1 x2) && (equal l1 l2)
| x1::l1, x2::l2 -> (Elem.equal x1 x2) && (equal l1 l2)
| _ -> false
let rec hash accu = function
| [] -> 1 + accu
| x::l -> hash (17 * accu + X.hash x) l
| x::l -> hash (17 * accu + Elem.hash x) l
let hash l = hash 1 l
......@@ -129,7 +129,7 @@ module List(X : T) = struct
if l1 == l2 then 0
else match (l1,l2) with
| x1::l1, x2::l2 ->
let c = X.compare x1 x2 in if c <> 0 then c
let c = Elem.compare x1 x2 in if c <> 0 then c
else compare l1 l2
| [],_ -> -1
| _ -> 1
......
runtime/value.ml
View file @ 083edd02
......@@ -27,13 +27,13 @@ and t =
let rec domain = function
| Identity | Mono -> Var.Set.empty
| List(l) -> Types.Tallying.domain l
| Comp(s1,s2) -> Var.Set.union (domain s1) (domain s2)
| Comp(s1,s2) -> Var.Set.cup (domain s1) (domain s2)
| Sel(_,_,sigma) -> (domain sigma)
let rec codomain = function
| Identity | Mono -> Var.Set.empty
| List(l) -> Types.Tallying.codomain l
| Comp(s1,s2) -> Var.Set.union (codomain s1) (codomain s2)
| Comp(s1,s2) -> Var.Set.cup (codomain s1) (codomain s2)
| Sel(_,_,sigma) -> (codomain sigma)
(* Comp for Value.sigma but simplify if possible. *)
......@@ -54,7 +54,7 @@ let rec comp s1 s2 = match s1, s2 with
| res -> comp s3 (comp res s6))
(* If a variable in the image of s2 is in the domain of s1 we can't simplify *)
| _, _ when not (Var.Set.is_empty (Var.Set.inter (domain s1) (codomain s2)))
| _, _ when not (Var.Set.is_empty (Var.Set.cap (domain s1) (codomain s2)))
-> Comp(s1, s2)
| List(_), List(_) | Sel(_), List(_) ->
......
types/patterns.ml
View file @ 083edd02
......@@ -91,7 +91,7 @@ let pp_node ppf node =
print node.descr
(Types.id node.accept)
Types.Print.pp_type (Types.descr node.accept)
pp_fv node.fv
pp_fv (node.fv :> Id.t list)
let counter = ref 0
......@@ -507,9 +507,9 @@ module Normal = struct
type t = NodeSet.t * Types.t * IdSet.t (* pl,t; t <= \accept{pl} *)
let check (pl,t,xs) =
let check ((pl,t,xs) : t) =
List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
(NodeSet.get pl)
(pl :> Node.t list)
let print ppf (pl,t,xs) =
Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]"
NodeSet.dump pl Types.Print.pp_type t
......@@ -523,11 +523,11 @@ module Normal = struct
let equal x y = compare x y == 0
let first_label (pl,t,xs) =
let first_label ((pl,t,xs) : t) =
List.fold_left
(fun l p -> Label.min l (first_label (descr p)))
(Types.Record.first_label t)
pl
(pl :> Node.t list)
end
......@@ -706,9 +706,9 @@ module Normal = struct
let factorize t0 (pl,t,xs) =
let t0 = if Types.subtype t t0 then t else Types.cap t t0 in
let vs_var = facto Factorize.var t0 xs pl in
let vs_var = facto Factorize.var t0 xs (NodeSet.get pl) in
let xs = IdSet.diff xs vs_var in
let vs_nil = facto Factorize.nil t0 xs pl in
let vs_nil = facto Factorize.nil t0 xs (NodeSet.get pl) in
let xs = IdSet.diff xs vs_nil in
(vs_var,vs_nil,(pl,t,xs))
......@@ -748,7 +748,7 @@ module Normal = struct
| (t,res,pl)::tl -> aux_check tl s accu (Types.diff t s) res pl
in
aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic)
IdMap.empty (List.map descr pl)
IdMap.empty (List.map descr (NodeSet.get pl))
(*
let prod_tests (pl,t,xs) =
......@@ -943,7 +943,7 @@ module Compile = struct
Format.fprintf ppf " pat %a@." Normal.Nnf.print p;
) disp.pl
let first_lab t reqs =
let first_lab t (reqs : Normal.Nnf.t array) =
let aux l req = Label.min l (Normal.Nnf.first_label req) in
let lab =
Array.fold_left aux (Types.Record.first_label t) reqs in
......@@ -953,7 +953,7 @@ module Compile = struct
let compute_actions = ref (fun _ -> assert false)
let dispatcher t pl : dispatcher =
let dispatcher t (pl : Normal.Nnf.t array) : dispatcher =
try DispMap.find (t,pl) !dispatchers
with Not_found ->
let lab = first_lab t pl in
......@@ -1105,7 +1105,7 @@ module Compile = struct
(* Collect all subrequests *)
let aux reqs (req,_) =
let (_,_,((_,tr,xs) as r')) as req' =
if facto then Normal.factorize t req else [],[],req in
if facto then Normal.factorize t req else IdSet.empty,IdSet.empty,req in
factorized := NfMap.add req req' !factorized;
if IdSet.is_empty xs && Types.subtype t tr then reqs
......@@ -1216,8 +1216,8 @@ module Compile = struct
if IdSet.mem var x || IdSet.mem nil x
then has_facto := true
else (assert (IdMap.assoc x res = !i); incr i)
) xs;
Match (List.length xs, (var,nil,xs,e))
) (IdSet.get xs);
Match (IdSet.length xs, (var,nil,xs,e))
| [] -> r
| _ -> assert false
in
......
types/sortedList.ml
View file @ 083edd02
This diff is collapsed.
types/sortedList.mli
View file @ 083edd02
module Make(X : Custom.T) :
module type S =
sig
include Custom.T with type t = X.t list
module Elem : Custom.T with type t = X.t
module Elem : Custom.T
include Custom.T with type t = private Elem.t list
external get: t -> Elem.t list = "%identity"
external get: t -> X.t list = "%identity"
val singleton: X.t -> t
val iter: (X.t -> unit) -> t -> unit
val filter: (X.t -> bool) -> t -> t
val exists: (X.t -> bool) -> t -> bool
val fold: ('a -> X.t -> 'a) -> 'a -> t -> 'a
val pick: t -> X.t option
val choose: t -> X.t
val singleton: Elem.t -> t
val iter: (Elem.t -> unit) -> t -> unit
val filter: (Elem.t -> bool) -> t -> t
val exists: (Elem.t -> bool) -> t -> bool
val fold: ('a -> Elem.t -> 'a) -> 'a -> t -> 'a
val pick: t -> Elem.t option
val choose: t -> Elem.t
val length: t -> int
val empty: t
val is_empty: t -> bool
val from_list : X.t list -> t
val add: X.t -> t -> t
val remove: X.t -> t -> t
val from_list : Elem.t list -> t
val add: Elem.t -> t -> t
val remove: Elem.t -> t -> t
val disjoint: t -> t -> bool
val cup: t -> t -> t
val split: t -> t -> t * t * t
......@@ -26,26 +25,26 @@ sig
val cap: t -> t -> t
val diff: t -> t -> t
val subset: t -> t -> bool
val map: (X.t -> X.t) -> t -> t
val mem: t -> X.t -> bool
val map: (Elem.t -> Elem.t) -> t -> t
val mem: t -> Elem.t -> bool
module Map: sig
type 'a map
external get: 'a map -> (X.t * 'a) list = "%identity"
val add: X.t -> 'a -> 'a map -> 'a map
val mem: X.t -> 'a map -> bool
external get: 'a map -> (Elem.t * 'a) list = "%identity"
val add: Elem.t -> 'a -> 'a map -> 'a map
val mem: Elem.t -> 'a map -> bool
val length: 'a map -> int
val domain: 'a map -> t
val restrict: 'a map -> t -> 'a map
val empty: 'a map
val fold: (X.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val fold: (Elem.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val iter: ('a -> unit) -> 'a map -> unit
val iteri: (X.t -> 'a -> unit) -> 'a map -> unit
val filter: (X.t -> 'a -> bool) -> 'a map -> 'a map
val iteri: (Elem.t -> 'a -> unit) -> 'a map -> unit
val filter: (Elem.t -> 'a -> bool) -> 'a map -> 'a map
val is_empty: 'a map -> bool
val singleton: X.t -> 'a -> 'a map
val assoc_remove: X.t -> 'a map -> 'a * 'a map
val remove: X.t -> 'a map -> 'a map
val singleton: Elem.t -> 'a -> 'a map
val assoc_remove: Elem.t -> 'a map -> 'a * 'a map
val remove: Elem.t -> 'a map -> 'a map
val merge: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map
val combine: ('a -> 'c) -> ('b -> 'c) -> ('a -> 'b -> 'c) ->
'a map -> 'b map -> 'c map
......@@ -55,20 +54,20 @@ sig
val merge_elem: 'a -> 'a map -> 'a map -> 'a map
val union_disj: 'a map -> 'a map -> 'a map
val diff: 'a map -> t -> 'a map
val from_list: ('a -> 'a -> 'a ) -> (X.t * 'a) list -> 'a map
val from_list_disj: (X.t * 'a) list -> 'a map
val from_list: ('a -> 'a -> 'a ) -> (Elem.t * 'a) list -> 'a map
val from_list_disj: (Elem.t * 'a) list -> 'a map
val map_from_slist: (X.t -> 'a) -> t -> 'a map
val map_from_slist: (Elem.t -> 'a) -> t -> 'a map
val collide: ('a -> 'b -> unit) -> 'a map -> 'b map -> unit
val may_collide: ('a -> 'b -> unit) -> exn -> 'a map -> 'b map -> unit
val map: ('a -> 'b) -> 'a map -> 'b map
val mapi: (X.t -> 'a -> 'b) -> 'a map -> 'b map
val mapi: (Elem.t -> 'a -> 'b) -> 'a map -> 'b map
val constant: 'a -> t -> 'a map
val num: int -> t -> int map
val map_to_list: ('a -> 'b) -> 'a map -> 'b list
val mapi_to_list: (X.t -> 'a -> 'b) -> 'a map -> 'b list
val assoc: X.t -> 'a map -> 'a
val assoc_present: X.t -> 'a map -> 'a
val mapi_to_list: (Elem.t -> 'a -> 'b) -> 'a map -> 'b list
val assoc: Elem.t -> 'a map -> 'a
val assoc_present: Elem.t -> 'a map -> 'a
val compare: ('a -> 'a -> int) -> 'a map -> 'a map -> int
val hash: ('a -> int) -> 'a map -> int
val equal: ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
......@@ -78,6 +77,8 @@ sig
end
end
module Make(X : Custom.T) : S with module Elem = X and type t = private X.t list
module type FiniteCofinite = sig
type elem
type s = private Finite of elem list | Cofinite of elem list
......
types/types.ml
View file @ 083edd02
......@@ -1005,9 +1005,9 @@ let get_variables main_memo temp_memo t =
acc
end
in
(Var.Set.union tvpos tpos,
Var.Set.union tvneg tneg,
Var.Set.union tvars vars)
(Var.Set.cup tvpos tpos,
Var.Set.cup tvneg tneg,
Var.Set.cup tvars vars)
in
get_variables true Var.Set.(empty,empty,empty) t
......@@ -1023,7 +1023,7 @@ let get_variables =
let check_var =
let aux t =
let tvpos, tvneg, tvars = get_variables t in
match Var.Set.(cardinal tvpos, cardinal tvneg, cardinal tvars) with
match Var.Set.(length tvpos, length tvneg, length tvars) with
1, 0, 1 -> let v = Var.Set.choose tvpos in
if equiv (var v) t then `Pos v else `NotVar
| 0, 1, 1 -> let v = Var.Set.choose tvneg in
......@@ -1049,7 +1049,7 @@ let all_vars t =
let _, _, s = get_variables t in s
let all_tlv t =
let p , n, _ = get_variables t in Var.Set.union p n
let p , n, _ = get_variables t in Var.Set.cup p n
let is_closed delta t =
Var.Set.(is_empty (diff (all_vars t) delta))
......@@ -1843,7 +1843,7 @@ module Print = struct
try
let res =
VarTable.fold (fun ((v1, v2) as k) tt acc ->
if Var.Set.(not (is_empty (inter v1 v2))) || is_empty tt then acc
if Var.Set.(not (is_empty (cap v1 v2))) || is_empty tt then acc
else if Key.is_empty k && subtype any tt then raise Not_found
else
(k, tt) :: acc
......@@ -1866,7 +1866,7 @@ module Print = struct
| i :: ll ->
let factp, factn =
List.fold_left (fun (accp, accn) (vp, vn) ->
Var.Set.(inter accp vp, inter accn vn))
Var.Set.(cap accp vp, cap accn vn))
i ll
in
let nl =
......@@ -2636,7 +2636,7 @@ module Positive = struct
|`Xml of v * v
|`Record of bool * (bool * Ns.Label.t * v) list
]
and v = { mutable def : rhs; mutable node : node option }
and v = { mutable def : rhs; mutable node : node option; }
module MemoHash = Hashtbl.Make( struct
type t = v
......@@ -2697,7 +2697,7 @@ module Positive = struct
n
(* We shadow the corresponding definitions in the outer module *)
let forward () = { def = `Cup []; node = None }
let forward () = { def = `Cup []; node = None; }
let def v d = v.def <- d
let cons d = let v = forward () in def v d; v
let ty d = cons (`Type d)
......@@ -2781,7 +2781,6 @@ module Positive = struct
@@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
in
node_t.def <- (cup descr_t).def; node_t
in
decompose_type t
......@@ -2883,7 +2882,7 @@ module Positive = struct
let substitute_free delta t =
let h = Hashtbl.create 17 in
let subst d =
if Var.Set.mem d delta then var d else
if Var.Set.mem delta d then var d else
try
Hashtbl.find h d
with Not_found ->
......@@ -2895,7 +2894,7 @@ module Positive = struct
let substitute_kind delta kind t =
let subst d =
if Var.Set.mem d delta then var d else
if Var.Set.mem delta d then var d else
var (Var.set_kind kind d)
in
apply_subst ~subst:subst t
......@@ -2923,7 +2922,7 @@ module Positive = struct
if ni == 0 then acc else pretty ni acc
in
let x = Var.mk (pretty !idx "") in
if Var.Set.mem x delta then (incr idx; freshvar idx) else x
if Var.Set.mem delta x then (incr idx; freshvar idx) else x
in
let vars = Hashtbl.create 17 in
let memo = Memo.create 17 in
......@@ -2939,7 +2938,7 @@ 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) ->
|`Variable d when Var.Set.mem delta d || (not (is_internal d) && not pos) ->
Hashtbl.replace vars d v
|`Variable d ->
begin try
......@@ -3042,7 +3041,7 @@ module Tallying = struct
with
Not_found -> inf, sup
in
if Var.Set.mem v delta then map
if Var.Set.mem delta v then map
else VarMap.add v (new_i, new_s) map
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
......@@ -3246,8 +3245,8 @@ module Tallying = struct
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n =
let _compare delta v1 v2 =
let monov1 = Var.Set.mem v1 delta in
let monov2 = Var.Set.mem v2 delta in
let monov1 = Var.Set.mem delta v1 in
let monov2 = Var.Set.mem delta v1 in
if monov1 == monov2 then
Var.compare v1 v2
else
......@@ -3310,7 +3309,7 @@ module Tallying = struct
begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
let (v,p) = extract_variable t in
if Var.Set.mem v delta then CS.unsat (* if it is monomorphic, unsat *)
if Var.Set.mem delta v then CS.unsat (* if it is monomorphic, unsat *)
else
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
......@@ -3332,7 +3331,7 @@ module Tallying = struct
let acc = aux single_record normrec acc (BoolRec.get t.record) in
let acc = (* Simplify the constraints on that type *)
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem v delta) ||
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem delta v) ||
let x = var v in subtype s x && subtype x t
) m)
acc
......@@ -3489,7 +3488,7 @@ module Tallying = struct
* means that the constraint is of the form (alpha,beta). *)
if is_var t then begin
let (beta,_) = extract_variable t in
if Var.Set.mem beta delta then aux alpha (s, t) acc
if Var.Set.mem delta beta then aux alpha (s, t) acc
else
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
......@@ -3565,7 +3564,7 @@ module Tallying = struct
let rec dom = function
|I -> Var.Set.empty
|S si -> CS.E.fold (fun v _ acc -> Var.Set.add v acc) si Var.Set.empty
|A (si,sj) -> Var.Set.union (dom si) (dom sj)
|A (si,sj) -> Var.Set.cup (dom si) (dom sj)
(* composition of two symbolic substitution sets sigmaI, sigmaJ .
Cartesian product *)
......@@ -3585,11 +3584,11 @@ module Tallying = struct
let filter t si =
vsi := get si;
vst := all_vars t;
not(Var.Set.is_empty (Var.Set.inter !vst !vsi))
not(Var.Set.is_empty (Var.Set.cap !vst !vsi))
in
let filterdiff t si sj =
let vsj = get sj in
not(Var.Set.is_empty (Var.Set.inter !vst (Var.Set.diff !vsi vsj)))
not(Var.Set.is_empty (Var.Set.cap !vst (Var.Set.diff !vsi vsj)))
in
let rec aux t = function
|I -> t
......@@ -3610,7 +3609,7 @@ module Tallying = struct
let codomain ll =
List.fold_left (fun acc e ->
CS.E.fold (fun _ v acc ->
Var.Set.union (all_vars v) acc
Var.Set.cup (all_vars v) acc
) e acc
) Var.Set.empty ll
......
types/var.ml
View file @ 083edd02
......@@ -31,11 +31,6 @@ module Set = struct
let dump ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") V.dump ppf (get s)
let pp ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") V.pp ppf (get s)
let printf = pp Format.std_formatter
let union = cup
let inter = cap
let cardinal = length
let mem t v = mem v t
let fold = fold
end
type 'a var_or_atom = [ `Atm of 'a | `Var of t ]
......
types/var.mli
View file @ 083edd02
......@@ -17,23 +17,9 @@ val is_internal : t -> bool
*)
module Set : sig
include Custom.T
val dump : Format.formatter -> t -> unit
include SortedList.S with type Elem.t = var
val pp : Format.formatter -> t -> unit
val printf : t -> unit
val is_empty : t -> bool
val empty : t
val singleton : var -> t
val union : t -> t -> t
val diff : t -> t -> t
val mem : var -> t -> bool
val add : var -> t -> t
val inter : t -> t -> t
val subset : t -> t -> bool
val cardinal : t -> int
val from_list : var list -> t
val fold : ('a -> var -> 'a) -> 'a -> t -> 'a
val choose : t -> var
val dump : Format.formatter -> t -> unit
end
type 'a var_or_atom = [ `Atm of 'a | `Var of t ]
......
typing/typed.ml
View file @ 083edd02
......@@ -184,7 +184,7 @@ module Print = struct
and pp_v ppf (id, name) =
Format.fprintf ppf "(%d,%s)" (Upool.int id) (Encodings.Utf8.to_string name)
and pp_fv ppf fv = Utils.pp_list pp_v ppf fv
and pp_fv ppf fv = Utils.pp_list pp_v ppf (IdSet.get fv)
and pp_vars_poly ppf m =
let pp_aux ppf (x,s) = Format.fprintf ppf "%a : %a" Ident.print x Var.Set.pp s in
......
typing/typer.ml
View file @ 083edd02
......@@ -614,7 +614,7 @@ module IType = struct
("This definition yields an empty type for " ^ (Ident.to_string v));
let vars_rhs = Types.all_vars t_rhs in
if List.exists (fun x -> not (Var.Set.mem (Var.mk (U.to_string x)) vars_rhs)) args then
if List.exists (fun x -> not (Var.Set.mem vars_rhs (Var.mk (U.to_string x)) )) args then
raise_loc_generic loc
(Printf.sprintf "Definition of type %s contains unbound type variables"
(Ident.to_string v));
......@@ -958,7 +958,7 @@ and branches env b =
let ploc = p.loc in
let p = pat env p in
let fvp = Patterns.fv p in
let (fv2,e) = expr (enter_values_dummy fvp env) noloc e in
let (fv2,e) = expr (enter_values_dummy (fvp :> Id.t list) env) noloc e in
let br_loc = merge_loc ploc e.Typed.exp_loc in
(match Fv.pick (Fv.diff fvp fv2) with
| None -> ()
......@@ -1004,7 +1004,7 @@ and select_from_where env loc e from where =
let p = pat !env p in
let fvp = Patterns.fv p in
let (fv2,e) = expr !env noloc e in
env := enter_values_dummy fvp !env;
env := enter_values_dummy (fvp :> Id.t list) !env;
all_fv := Fv.cup (Fv.diff fv2 !bound_fv) !all_fv;
bound_fv := Fv.cup fvp !bound_fv;
(ploc,p,fvp,e) in
......@@ -1160,7 +1160,7 @@ and type_check' loc env ed constr precise = match ed with
let delta_intf =