Commit d4db3bf7 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

minor code cleaning

parent ab80b96f
......@@ -27,12 +27,12 @@ module Ty = struct
ty_def : ty option;
}
and ty = {
ty_node : ty_node;
ty_tag : int;
}
and ty = {
ty_node : ty_node;
ty_tag : int;
}
and ty_node =
and ty_node =
| Tyvar of vsymbol
| Tyapp of tysymbol * ty list
......@@ -43,30 +43,30 @@ module Ty = struct
}
let equal_tysymbol s1 s2 = Name.equal s1.ty_name s2.ty_name
module H = struct
type t = ty
let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
| Tyvar n1, Tyvar n2 ->
Name.equal n1 n2
| Tyapp (s1, l1), Tyapp (s2, l2) ->
equal_tysymbol s1 s2 && List.for_all2 (==) l1 l2
| Tyvar n1, Tyvar n2 ->
Name.equal n1 n2
| Tyapp (s1, l1), Tyapp (s2, l2) ->
equal_tysymbol s1 s2 && List.for_all2 (==) l1 l2
| _ ->
false
false
let hash_ty ty =
let hash_ty ty =
ty.ty_tag
let hash ty = match ty.ty_node with
| Tyvar v ->
Name.hash v
| Tyapp (s, tl) ->
Hashcons.combine_list hash_ty (Name.hash s.ty_name) tl
| Tyvar v ->
Name.hash v
| Tyapp (s, tl) ->
Hashcons.combine_list hash_ty (Name.hash s.ty_name) tl
let tag n t = { t with ty_tag = n }
end
module Hty = Hashcons.Make(H)
......@@ -79,15 +79,13 @@ module Ty = struct
let rec matching s ty1 ty2 = match ty1.ty_node, ty2.ty_node with
| Tyvar n1, _ when Name.M.mem n1 s ->
if Name.M.find n1 s != ty2 then raise NoMatching;
s
| Tyvar n1, _ ->
Name.M.add n1 ty2 s
(try if Name.M.find n1 s == ty2 then s else raise NoMatching
with Not_found -> Name.M.add n1 ty2 s)
| Tyapp (f1, l1), Tyapp (f2, l2) when Name.equal f1.ty_name f2.ty_name ->
assert (List.length l1 = List.length l2);
List.fold_left2 matching s l1 l2
assert (List.length l1 = List.length l2);
List.fold_left2 matching s l1 l2
| _ ->
raise NoMatching
raise NoMatching
end
......@@ -118,11 +116,11 @@ let create_psymbol n s = {
let eq_psymbol s1 s2 = Name.equal s1.p_name s2.p_name
type quant =
type quant =
| Fforall
| Fexists
type binop =
type binop =
| Fand
| For
| Fimplies
......@@ -137,9 +135,9 @@ type pattern = {
pat_tag : int;
}
and pattern_node =
| Pwild
| Pvar of vsymbol
and pattern_node =
| Pwild
| Pvar of vsymbol
| Papp of fsymbol * pattern list
| Pas of pattern * vsymbol
......@@ -149,15 +147,15 @@ module Pattern = struct
let equal_node p1 p2 = match p1, p2 with
| Pwild, Pwild ->
true
true
| Pvar n1, Pvar n2 ->
Name.equal n1 n2
Name.equal n1 n2
| Papp (s1, l1), Papp (s2, l2) ->
eq_fsymbol s1 s2 && List.for_all2 (==) l1 l2
eq_fsymbol s1 s2 && List.for_all2 (==) l1 l2
| Pas (p1, n1), Pas (p2, n2) ->
p1 == p2 && Name.equal n1 n2
p1 == p2 && Name.equal n1 n2
| _ ->
false
false
let equal p1 p2 =
equal_node p1.pat_node p2.pat_node && p1.pat_ty == p2.pat_ty
......@@ -183,8 +181,8 @@ let pat_var n ty = Hpattern.hashcons (mk_pattern (Pvar n) ty)
let pat_app f pl ty = Hpattern.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p n = Hpattern.hashcons (mk_pattern (Pas (p, n)) p.pat_ty)
type term = {
t_node : term_node;
type term = {
t_node : term_node;
t_label : label list;
t_ty : ty;
t_tag : int;
......@@ -196,7 +194,7 @@ and fmla = {
f_tag : int;
}
and term_node =
and term_node =
| Tbvar of int
| Tvar of vsymbol
| Tapp of fsymbol * term list
......@@ -204,7 +202,7 @@ and term_node =
| Tlet of term * bind_term
| Teps of bind_fmla
and fmla_node =
and fmla_node =
| Fapp of psymbol * term list
| Fquant of quant * bind_fmla
| Fbinop of binop * fmla * fmla
......@@ -223,38 +221,38 @@ and bind_fmla = vsymbol * ty * fmla
and fbranch = pattern * int * fmla
module rec T : Hashcons.HashedType with type t = term =
module rec T : Hashcons.HashedType with type t = term =
struct
type t = term
let eq_tbranch (p1, _, t1) (p2, _, t2) =
let eq_tbranch (p1, _, t1) (p2, _, t2) =
p1 == p2 && t1 == t2
let eq_bind_term (v1, ty1, t1) (v2, ty2, t2) =
let eq_bind_term (v1, ty1, t1) (v2, ty2, t2) =
Name.equal v1 v2 && ty1 == ty2 && t1 == t2
let equal_term_node t1 t2 = match t1, t2 with
| Tbvar x1, Tbvar x2 ->
x1 == x2
| Tvar v1, Tvar v2 ->
Name.equal v1 v2
| Tapp (s1, l1), Tapp (s2, l2) ->
Name.equal s1.f_name s2.f_name && List.for_all2 (==) l1 l2
| Tbvar x1, Tbvar x2 ->
x1 == x2
| Tvar v1, Tvar v2 ->
Name.equal v1 v2
| Tapp (s1, l1), Tapp (s2, l2) ->
Name.equal s1.f_name s2.f_name && List.for_all2 (==) l1 l2
| Tcase (t1, l1), Tcase (t2, l2) ->
t1 == t2 && List.for_all2 eq_tbranch l1 l2
t1 == t2 && List.for_all2 eq_tbranch l1 l2
| Tlet (t1, b1), Tlet (t2, b2) ->
t1 == t2 && eq_bind_term b1 b2
t1 == t2 && eq_bind_term b1 b2
| Teps f1, Teps f2 ->
F.eq_bind_fmla f1 f2
| _ ->
false
F.eq_bind_fmla f1 f2
| _ ->
false
let equal t1 t2 =
equal_term_node t1.t_node t2.t_node &&
equal_term_node t1.t_node t2.t_node &&
(try List.for_all2 (=) t1.t_label t2.t_label with _ -> false) &&
t1.t_ty == t2.t_ty
let hash_bind_term (v, ty, t) =
let hash_bind_term (v, ty, t) =
Hashcons.combine2 (Name.hash v) ty.Ty.ty_tag t.t_tag
let hash_tbranch (p, _, t) =
......@@ -271,53 +269,53 @@ struct
| Teps f -> F.hash_bind_fmla f
let hash t =
Hashcons.combine (hash_term_node t.t_node)
Hashcons.combine (hash_term_node t.t_node)
(Hashcons.combine_list Hashtbl.hash t.t_ty.Ty.ty_tag t.t_label)
let tag n t = { t with t_tag = n }
end
and F : sig
include Hashcons.HashedType with type t = fmla
and F : sig
include Hashcons.HashedType with type t = fmla
val eq_bind_fmla : bind_fmla -> bind_fmla -> bool
val hash_bind_fmla : bind_fmla -> int
end = struct
type t = fmla
let eq_fbranch (p1, _, f1) (p2, _, f2) =
let eq_fbranch (p1, _, f1) (p2, _, f2) =
p1 == p2 && f1 == f2
let eq_bind_fmla (v1, ty1, f1) (v2, ty2, f2) =
Name.equal v1 v2 && ty1 == ty2 && f1 == f2
let equal_fmla_node f1 f2 = match f1, f2 with
| Fapp (s1, tl1), Fapp (s2, tl2) ->
Name.equal s1.p_name s2.p_name && List.for_all2 (==) tl1 tl2
Name.equal s1.p_name s2.p_name && List.for_all2 (==) tl1 tl2
| Fquant (q1, bf1), Fquant (q2, bf2) ->
q1 == q2 && eq_bind_fmla bf1 bf2
q1 == q2 && eq_bind_fmla bf1 bf2
| Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
op1 == op2 && f1 == f2 && g1 == g2
op1 == op2 && f1 == f2 && g1 == g2
| Funop (op1, f1), Funop (op2, f2) ->
op1 == op2 && f1 == f2
| Ftrue, Ftrue
op1 == op2 && f1 == f2
| Ftrue, Ftrue
| Ffalse, Ffalse ->
true
true
| Fif (f1, g1, h1), Fif (f2, g2, h2) ->
f1 == f2 && g1 == g2 && h1 == h2
f1 == f2 && g1 == g2 && h1 == h2
| Flet (t1, bf1), Flet (t2, bf2) ->
t1 == t2 && eq_bind_fmla bf1 bf2
t1 == t2 && eq_bind_fmla bf1 bf2
| Fcase (t1, bl1), Fcase (t2, bl2) ->
t1 == t2 && List.for_all2 eq_fbranch bl1 bl2
| _ ->
false
t1 == t2 && List.for_all2 eq_fbranch bl1 bl2
| _ ->
false
let equal f1 f2 =
equal_fmla_node f1.f_node f2.f_node &&
equal_fmla_node f1.f_node f2.f_node &&
(try List.for_all2 (=) f1.f_label f2.f_label with _ -> false)
let hash_fmla f = f.f_tag
let hash_bind_fmla (v, ty, f) =
let hash_bind_fmla (v, ty, f) =
Hashcons.combine2 (Name.hash v) ty.Ty.ty_tag (hash_fmla f)
let hash_fbranch (p, _, f) =
......@@ -328,13 +326,13 @@ end = struct
let hash_fmla_node = function
| Fapp (p, tl) -> Hashcons.combine_list hash_term (Name.hash p.p_name) tl
| Fquant (q, bf) -> Hashcons.combine (Hashtbl.hash q) (hash_bind_fmla bf)
| Fbinop (op, f1, f2) ->
Hashcons.combine2 (Hashtbl.hash op) (hash_fmla f1) (hash_fmla f2)
| Fbinop (op, f1, f2) ->
Hashcons.combine2 (Hashtbl.hash op) (hash_fmla f1) (hash_fmla f2)
| Funop (op, f) -> Hashcons.combine (Hashtbl.hash op) (hash_fmla f)
| Ftrue -> 0
| Ffalse -> 1
| Fif (f1, f2, f3) ->
Hashcons.combine2 (hash_fmla f1) (hash_fmla f2) (hash_fmla f3)
| Fif (f1, f2, f3) ->
Hashcons.combine2 (hash_fmla f1) (hash_fmla f2) (hash_fmla f3)
| Flet (t, bf) -> Hashcons.combine t.t_tag (hash_bind_fmla bf)
| Fcase (t, bl) -> Hashcons.combine_list hash_fbranch t.t_tag bl
......@@ -355,7 +353,7 @@ let t_app f tl ty = Hterm.hashcons (mk_term (Tapp (f, tl)) ty)
let t_label l t = Hterm.hashcons { t with t_label = l }
let t_label_add l t = Hterm.hashcons { t with t_label = l :: t.t_label }
let t_let v t1 t2 =
let t_let v t1 t2 =
Hterm.hashcons (mk_term (Tlet (t1, (v, t1.t_ty, t2))) t2.t_ty)
let t_case t bl ty = Hterm.hashcons (mk_term (Tcase (t, bl)) ty)
......@@ -375,7 +373,7 @@ let f_implies = f_binary Fimplies
let f_iff = f_binary Fiff
let f_unary op f = Hfmla.hashcons (mk_fmla (Funop (op, f)))
let f_not f = Hfmla.hashcons (mk_fmla (Funop (Fnot, f)))
let f_not = f_unary Fnot
let f_if f1 f2 f3 = Hfmla.hashcons (mk_fmla (Fif (f1, f2, f3)))
let f_quant q u ty f = Hfmla.hashcons (mk_fmla (Fquant (q, (u, ty, f))))
......@@ -409,7 +407,7 @@ let map_fmla_unsafe fnT fnF lvl f = match f.f_node with
(* replaces variables with de Bruijn indices in term [t] using a map [m] *)
let rec abst_term m lvl t = match t.t_node with
| Tvar u ->
| Tvar u ->
(try t_bvar (Name.M.find u m + lvl) t.t_ty
with Not_found -> t)
| _ -> map_term_unsafe (abst_term m) (abst_fmla m) lvl t
......@@ -422,7 +420,7 @@ module Im = Map.Make(struct type t = int let compare = Pervasives.compare end)
let rec inst_term m lvl t = match t.t_node with
| Tbvar n when n >= lvl ->
(try t_var (Im.find (n - lvl) m) t.t_ty
(try t_var (Im.find (n - lvl) m) t.t_ty
with Not_found -> assert false)
| _ -> map_term_unsafe (inst_term m) (inst_fmla m) lvl t
......@@ -430,67 +428,67 @@ and inst_fmla m lvl f = map_fmla_unsafe (inst_term m) (inst_fmla m) lvl f
(* smart constructors *)
let name_map_singleton v = Name.M.add v 0 Name.M.empty
let abst_term_single v t = abst_term (Name.M.add v 0 Name.M.empty) 0 t
let abst_fmla_single v f = abst_fmla (Name.M.add v 0 Name.M.empty) 0 f
(* TODO: checks *)
let t_let v t1 t2 = t_let v t1 (abst_term_single v t2)
(* TODO: checks *)
let t_let v t1 t2 = t_let v t1 (abst_term (name_map_singleton v) 0 t2)
let f_let v t1 f2 = f_let v t1 (abst_fmla_single v f2)
(* TODO: checks *)
let t_eps v ty f = t_eps v ty (abst_fmla (name_map_singleton v) 0 f)
let t_eps v ty f = t_eps v ty (abst_fmla_single v f)
let t_app f tl ty =
(* TODO: checks *)
let f_quant q v ty f = f_quant q v ty (abst_fmla_single v f)
let f_forall = f_quant Fforall
let f_exists = f_quant Fexists
let t_app f tl ty =
let args, res = f.f_scheme in
let _ =
List.fold_left2
Ty.matching (Ty.matching Name.M.empty res ty)
let _ =
List.fold_left2
Ty.matching (Ty.matching Name.M.empty res ty)
args (List.map (fun t -> t.t_ty) tl)
in
t_app f tl ty
let f_app f tl =
let args = f.p_scheme in
let _ =
List.fold_left2
Ty.matching Name.M.empty
args (List.map (fun t -> t.t_ty) tl)
in
f_app f tl
let varmap_for_pattern p =
let i = ref (-1) in
let rec make acc p = match p.pat_node with
| Pwild ->
acc
| Pvar n ->
assert (not (Name.M.mem n acc));
incr i; Name.M.add n !i acc
| Papp (_, pl) ->
List.fold_left make acc pl
| Pas (p, n) ->
assert (not (Name.M.mem n acc));
incr i; make (Name.M.add n !i acc) p
| Pwild ->
acc
| Pvar n ->
assert (not (Name.M.mem n acc));
incr i; Name.M.add n !i acc
| Papp (_, pl) ->
List.fold_left make acc pl
| Pas (p, n) ->
assert (not (Name.M.mem n acc));
incr i; make (Name.M.add n !i acc) p
in
let m = make Name.M.empty p in
m, !i + 1
(* TODO: checks *)
let t_case t bl =
let t_case t bl =
let make_tbranch (p, t) =
let m, nv = varmap_for_pattern p in (p, nv, abst_term m 0 t)
in
t_case t (List.map make_tbranch bl)
(* TODO: checks *)
let f_quant q v ty f = f_quant q v ty (abst_fmla (name_map_singleton v) 0 f)
let f_forall = f_quant Fforall
let f_exists = f_quant Fexists
(* TODO: checks *)
let f_let v t1 f2 = f_let v t1 (abst_fmla (name_map_singleton v) 0 f2)
let f_app f tl =
let args = f.p_scheme in
let _ =
List.fold_left2
Ty.matching Name.M.empty
args (List.map (fun t -> t.t_ty) tl)
in
f_app f tl
(* TODO: checks *)
let f_case t bl =
let f_case t bl =
let make_fbranch (p, f) =
let m, nv = varmap_for_pattern p in (p, nv, abst_fmla m 0 f)
in
......@@ -498,43 +496,42 @@ let f_case t bl =
(* opening binders *)
let int_map_singleton t = Im.add 0 t Im.empty
let inst_term_single v t = inst_term (Im.add 0 v Im.empty) 0 t
let inst_fmla_single v f = inst_fmla (Im.add 0 v Im.empty) 0 f
let open_bind_term (v, ty, t) =
let v = Name.fresh v in
v, ty, inst_term (int_map_singleton v) 0 t
let v = Name.fresh v in v, ty, inst_term_single v t
let open_bind_fmla (v, ty, f) =
let v = Name.fresh v in v, ty, inst_fmla_single v f
let rec subst_pat ns p = match p.pat_node with
| Pwild ->
let rec rename_pat ns p = match p.pat_node with
| Pwild ->
p
| Pvar n ->
(try pat_var (Name.M.find n ns) p.pat_ty with Not_found -> assert false)
| Papp (f, pl) ->
pat_app f (List.map (subst_pat ns) pl) p.pat_ty
pat_app f (List.map (rename_pat ns) pl) p.pat_ty
| Pas (p, n) ->
pat_as (subst_pat ns p)
(try Name.M.find n ns with Not_found -> assert false)
pat_as (rename_pat ns p)
(try Name.M.find n ns with Not_found -> assert false)
let substs_for_pat pat =
let substs_for_pattern pat =
let m, _ = varmap_for_pattern pat in
Name.M.fold
(fun x i (vars, s, ns) ->
Name.M.fold
(fun x i (vars, s, ns) ->
let x' = Name.fresh x in
Name.S.add x' vars, Im.add i x' s, Name.M.add x x' ns)
m
Name.S.add x' vars, Im.add i x' s, Name.M.add x x' ns)
m
(Name.S.empty, Im.empty, Name.M.empty)
let open_tbranch (pat, _, t) =
let vars, s, ns = substs_for_pat pat in
(subst_pat ns pat, vars, inst_term s 0 t)
let open_bind_fmla (v, ty, f) =
let v = Name.fresh v in
v, ty, inst_fmla (int_map_singleton v) 0 f
let vars, s, ns = substs_for_pattern pat in
(rename_pat ns pat, vars, inst_term s 0 t)
let open_fbranch (pat, _, f) =
let vars, s, ns = substs_for_pat pat in
(subst_pat ns pat, vars, inst_fmla s 0 f)
let vars, s, ns = substs_for_pattern pat in
(rename_pat ns pat, vars, inst_fmla s 0 f)
(* TODO: substitution functions (named variables -> terms)
......@@ -545,25 +542,25 @@ let open_fbranch (pat, _, f) =
let t_equal = (==)
let f_equal = (==)
let rec t_alpha_equal t1 t2 =
let rec t_alpha_equal t1 t2 =
t1 == t2 ||
t1.t_ty == t2.t_ty &&
match t1.t_node, t2.t_node with
| Tbvar x1, Tbvar x2 ->
x1 == x2
| Tvar v1, Tvar v2 ->
Name.equal v1 v2
| Tapp (s1, l1), Tapp (s2, l2) ->
Name.equal s1.f_name s2.f_name && List.for_all2 t_alpha_equal l1 l2
| Tbvar x1, Tbvar x2 ->
x1 == x2
| Tvar v1, Tvar v2 ->
Name.equal v1 v2
| Tapp (s1, l1), Tapp (s2, l2) ->
Name.equal s1.f_name s2.f_name && List.for_all2 t_alpha_equal l1 l2
| Tcase (t1, l1), Tcase (t2, l2) ->
t_alpha_equal t1 t2 && List.for_all2 tbranch_alpha_equal l1 l2
t_alpha_equal t1 t2 && List.for_all2 tbranch_alpha_equal l1 l2
| Tlet (t1, b1), Tlet (t2, b2) ->
t_alpha_equal t1 t2 && bind_term_alpha_equal b1 b2
t_alpha_equal t1 t2 && bind_term_alpha_equal b1 b2
| Teps f1, Teps f2 ->
bind_fmla_alpha_equal f1 f2
| _ ->
false
bind_fmla_alpha_equal f1 f2
| _ ->
false
and tbranch_alpha_equal (pat1, _, t1) (pat2, _, t2) =
pat_alpha_equal pat1 pat2 && t_alpha_equal t1 t2
......@@ -584,28 +581,28 @@ and bind_term_alpha_equal (_, _, t1) (_, _, t2) =
and bind_fmla_alpha_equal (_, _, f1) (_, _, f2) =
f_alpha_equal f1 f2
and f_alpha_equal f1 f2 =
and f_alpha_equal f1 f2 =
f1 == f2 ||
match f1.f_node, f2.f_node with
| Fapp (s1, tl1), Fapp (s2, tl2) ->
Name.equal s1.p_name s2.p_name && List.for_all2 t_alpha_equal tl1 tl2
Name.equal s1.p_name s2.p_name && List.for_all2 t_alpha_equal tl1 tl2
| Fquant (q1, bf1), Fquant (q2, bf2) ->
q1 == q2 && bind_fmla_alpha_equal bf1 bf2
q1 == q2 && bind_fmla_alpha_equal bf1 bf2
| Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
op1 == op2 && f_alpha_equal f1 f2 && f_alpha_equal g1 g2
op1 == op2 && f_alpha_equal f1 f2 && f_alpha_equal g1 g2
| Funop (op1, f1), Funop (op2, f2) ->
op1 == op2 && f_alpha_equal f1 f2
| Ftrue, Ftrue
op1 == op2 && f_alpha_equal f1 f2
| Ftrue, Ftrue
| Ffalse, Ffalse ->
true
true
| Fif (f1, g1, h1), Fif (f2, g2, h2) ->
f_alpha_equal f1 f2 && f_alpha_equal g1 g2 && f_alpha_equal h1 h2
f_alpha_equal f1 f2 && f_alpha_equal g1 g2 && f_alpha_equal h1 h2
| Flet (t1, bf1), Flet (t2, bf2) ->
t_alpha_equal t1 t2 && bind_fmla_alpha_equal bf1 bf2
t_alpha_equal t1 t2 && bind_fmla_alpha_equal bf1 bf2
| Fcase (t1, bl1), Fcase (t2, bl2) ->
t_alpha_equal t1 t2 && List.for_all2 fbranch_alpha_equal bl1 bl2
| _ ->
false
t_alpha_equal t1 t2 && List.for_all2 fbranch_alpha_equal bl1 bl2
| _ ->
false
and fbranch_alpha_equal (pat1, _, f1) (pat2, _, f2) =
pat_alpha_equal pat1 pat2 && f_alpha_equal f1 f2
......
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