Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

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

use the functor StructMake to make Maps, Sets and Hashtbls

for uniquely tagged objects.
parent e70e78d9
......@@ -86,16 +86,14 @@ type prsymbol = {
pr_name : ident;
}
module Prop = struct
module Prop = StructMake (struct
type t = prsymbol
let equal = (==)
let hash pr = pr.pr_name.id_tag
let compare pr1 pr2 =
Pervasives.compare pr1.pr_name.id_tag pr2.pr_name.id_tag
end
module Spr = Set.Make(Prop)
module Mpr = Map.Make(Prop)
module Hpr = Hashtbl.Make(Prop)
let tag pr = pr.pr_name.id_tag
end)
module Spr = Prop.S
module Mpr = Prop.M
module Hpr = Prop.H
let create_prsymbol n = { pr_name = id_register n }
......@@ -127,7 +125,7 @@ and decl_node =
(** Declarations *)
module Decl = struct
module Hsdecl = Hashcons.Make (struct
type t = decl
......@@ -182,21 +180,25 @@ module Decl = struct
let tag n d = { d with d_tag = n }
let compare d1 d2 = Pervasives.compare d1.d_tag d2.d_tag
end)
module Decl = StructMake (struct
type t = decl
let tag d = d.d_tag
end)
end
module Hdecl = Hashcons.Make(Decl)
module Mdecl = Map.Make(Decl)
module Sdecl = Set.Make(Decl)
module Sdecl = Decl.S
module Mdecl = Decl.M
module Hdecl = Decl.H
(** Declaration constructors *)
let mk_decl n = { d_node = n; d_tag = -1 }
let create_ty_decl tdl = Hdecl.hashcons (mk_decl (Dtype tdl))
let create_logic_decl ldl = Hdecl.hashcons (mk_decl (Dlogic ldl))
let create_ind_decl idl = Hdecl.hashcons (mk_decl (Dind idl))
let create_prop_decl k p f = Hdecl.hashcons (mk_decl (Dprop (k,p,f)))
let create_ty_decl tdl = Hsdecl.hashcons (mk_decl (Dtype tdl))
let create_logic_decl ldl = Hsdecl.hashcons (mk_decl (Dlogic ldl))
let create_ind_decl idl = Hsdecl.hashcons (mk_decl (Dind idl))
let create_prop_decl k p f = Hsdecl.hashcons (mk_decl (Dprop (k,p,f)))
exception ConstructorExpected of lsymbol
exception UnboundTypeVar of tvsymbol
......
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open Util
(** Identifiers *)
type ident = {
......@@ -31,15 +33,15 @@ and origin =
| Derived of ident
| Fresh
module Id = struct
module Id = StructMake (struct
type t = ident
let equal = (==)
let hash id1 = id1.id_tag
let compare id1 id2 = Pervasives.compare id1.id_tag id2.id_tag
end
module Mid = Map.Make(Id)
module Sid = Set.Make(Id)
module Hid = Hashtbl.Make(Id)
let tag id = id.id_tag
end)
module Sid = Id.S
module Mid = Id.M
module Hid = Id.H
type preid = ident
......
......@@ -28,17 +28,14 @@ type vsymbol = {
vs_ty : ty;
}
module Vsym = struct
module Vsym = StructMake (struct
type t = vsymbol
let equal = (==)
let hash vs = vs.vs_name.id_tag
let compare vs1 vs2 =
Pervasives.compare vs1.vs_name.id_tag vs2.vs_name.id_tag
end
let tag vs = vs.vs_name.id_tag
end)
module Mvs = Map.Make(Vsym)
module Svs = Set.Make(Vsym)
module Hvs = Hashtbl.Make(Vsym)
module Svs = Vsym.S
module Mvs = Vsym.M
module Hvs = Vsym.H
let create_vsymbol name ty = {
vs_name = id_register name;
......@@ -56,16 +53,14 @@ type lsymbol = {
ls_constr : bool;
}
module Lsym = struct
module Lsym = StructMake (struct
type t = lsymbol
let equal = (==)
let hash fs = fs.ls_name.id_tag
let compare fs1 fs2 =
Pervasives.compare fs1.ls_name.id_tag fs2.ls_name.id_tag
end
module Sls = Set.Make(Lsym)
module Mls = Map.Make(Lsym)
module Hls = Hashtbl.Make(Lsym)
let tag ls = ls.ls_name.id_tag
end)
module Sls = Lsym.S
module Mls = Lsym.M
module Hls = Lsym.H
let create_lsymbol name args value constr = {
ls_name = id_register name;
......@@ -92,8 +87,7 @@ and pattern_node =
| Papp of lsymbol * pattern list
| Pas of pattern * vsymbol
module Hpat = struct
module Hspat = Hashcons.Make (struct
type t = pattern
let equal_node p1 p2 = match p1, p2 with
......@@ -117,17 +111,24 @@ module Hpat = struct
let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
let tag n p = { p with pat_tag = n }
end)
module Pat = StructMake (struct
type t = pattern
let tag pat = pat.pat_tag
end)
end
module Hp = Hashcons.Make(Hpat)
module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H
(* h-consing constructors for patterns *)
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
let pat_wild ty = Hp.hashcons (mk_pattern Pwild ty)
let pat_var v = Hp.hashcons (mk_pattern (Pvar v) v.vs_ty)
let pat_app f pl ty = Hp.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p v = Hp.hashcons (mk_pattern (Pas (p, v)) p.pat_ty)
let pat_wild ty = Hspat.hashcons (mk_pattern Pwild ty)
let pat_var v = Hspat.hashcons (mk_pattern (Pvar v) v.vs_ty)
let pat_app f pl ty = Hspat.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p v = Hspat.hashcons (mk_pattern (Pas (p, v)) p.pat_ty)
(* generic traversal functions *)
......@@ -275,7 +276,7 @@ let e_apply fnT fnF = function Term t -> fnT t | Fmla f -> fnF f
let tr_map fnT fnF = List.map (List.map (e_map fnT fnF))
let tr_fold fnT fnF = List.fold_left (List.fold_left (e_fold fnT fnF))
module T = struct
module Hsterm = Hashcons.Make (struct
type t = term
......@@ -327,14 +328,18 @@ module T = struct
let tag n t = { t with t_tag = n }
let compare t1 t2 = Pervasives.compare t1.t_tag t2.t_tag
end)
end
module Hterm = Hashcons.Make(T)
module Mterm = Map.Make(T)
module Sterm = Set.Make(T)
module Term = StructMake (struct
type t = term
let tag term = term.t_tag
end)
module Sterm = Term.S
module Mterm = Term.M
module Hterm = Term.H
module F = struct
module Hsfmla = Hashcons.Make (struct
type t = fmla
......@@ -413,26 +418,30 @@ module F = struct
let tag n f = { f with f_tag = n }
let compare f1 f2 = Pervasives.compare f1.f_tag f2.f_tag
end)
module Fmla = StructMake (struct
type t = fmla
let tag fmla = fmla.f_tag
end)
end
module Hfmla = Hashcons.Make(F)
module Mfmla = Map.Make(F)
module Sfmla = Set.Make(F)
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
(* hash-consing constructors for terms *)
let mk_term n ty = { t_node = n; t_label = []; t_ty = ty; t_tag = -1 }
let t_bvar n ty = Hterm.hashcons (mk_term (Tbvar n) ty)
let t_var v = Hterm.hashcons (mk_term (Tvar v) v.vs_ty)
let t_const c ty = Hterm.hashcons (mk_term (Tconst c) ty)
let t_app f tl ty = Hterm.hashcons (mk_term (Tapp (f, tl)) ty)
let t_let v t1 t2 = Hterm.hashcons (mk_term (Tlet (t1, (v, t2))) t2.t_ty)
let t_case t bl ty = Hterm.hashcons (mk_term (Tcase (t, bl)) ty)
let t_eps u f = Hterm.hashcons (mk_term (Teps (u, f)) u.vs_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_bvar n ty = Hsterm.hashcons (mk_term (Tbvar n) ty)
let t_var v = Hsterm.hashcons (mk_term (Tvar v) v.vs_ty)
let t_const c ty = Hsterm.hashcons (mk_term (Tconst c) ty)
let t_app f tl ty = Hsterm.hashcons (mk_term (Tapp (f, tl)) ty)
let t_let v t1 t2 = Hsterm.hashcons (mk_term (Tlet (t1, (v, t2))) t2.t_ty)
let t_case t bl ty = Hsterm.hashcons (mk_term (Tcase (t, bl)) ty)
let t_eps u f = Hsterm.hashcons (mk_term (Teps (u, f)) u.vs_ty)
let t_label l t = Hsterm.hashcons { t with t_label = l }
let t_label_add l t = Hsterm.hashcons { t with t_label = l :: t.t_label }
let t_label_copy { t_label = l } t = if l == [] then t else t_label l t
let t_app_unsafe = t_app
......@@ -440,24 +449,24 @@ let t_app_unsafe = t_app
(* hash-consing constructors for formulas *)
let mk_fmla n = { f_node = n; f_label = []; f_tag = -1 }
let f_app f tl = Hfmla.hashcons (mk_fmla (Fapp (f, tl)))
let f_quant q ul n tl f = Hfmla.hashcons (mk_fmla (Fquant (q, (ul,n,tl,f))))
let f_app f tl = Hsfmla.hashcons (mk_fmla (Fapp (f, tl)))
let f_quant q ul n tl f = Hsfmla.hashcons (mk_fmla (Fquant (q, (ul,n,tl,f))))
let f_binary op f1 f2 = Hfmla.hashcons (mk_fmla (Fbinop (op, f1, f2)))
let f_binary op f1 f2 = Hsfmla.hashcons (mk_fmla (Fbinop (op, f1, f2)))
let f_and = f_binary Fand
let f_or = f_binary For
let f_implies = f_binary Fimplies
let f_iff = f_binary Fiff
let f_not f = Hfmla.hashcons (mk_fmla (Fnot f))
let f_true = Hfmla.hashcons (mk_fmla Ftrue)
let f_false = Hfmla.hashcons (mk_fmla Ffalse)
let f_if f1 f2 f3 = Hfmla.hashcons (mk_fmla (Fif (f1, f2, f3)))
let f_let v t f = Hfmla.hashcons (mk_fmla (Flet (t, (v, f))))
let f_case t bl = Hfmla.hashcons (mk_fmla (Fcase (t, bl)))
let f_not f = Hsfmla.hashcons (mk_fmla (Fnot f))
let f_true = Hsfmla.hashcons (mk_fmla Ftrue)
let f_false = Hsfmla.hashcons (mk_fmla Ffalse)
let f_if f1 f2 f3 = Hsfmla.hashcons (mk_fmla (Fif (f1, f2, f3)))
let f_let v t f = Hsfmla.hashcons (mk_fmla (Flet (t, (v, f))))
let f_case t bl = Hsfmla.hashcons (mk_fmla (Fcase (t, bl)))
let f_label l f = Hfmla.hashcons { f with f_label = l }
let f_label_add l f = Hfmla.hashcons { f with f_label = l :: f.f_label }
let f_label l f = Hsfmla.hashcons { f with f_label = l }
let f_label_add l f = Hsfmla.hashcons { f with f_label = l :: f.f_label }
let f_label_copy { f_label = l } f = if l == [] then f else f_label l f
(* built-in symbols *)
......
module Make (S:Util.Sstruct) =
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
module Make (S:Util.Sstruct) =
struct
type 'a t = { ht : (int,'a) Hashtbl.t;
final : S.t -> unit}
let wget w = Weak.get w 0
let wref v =
let wref v =
let w = Weak.create 1 in
Weak.set w 0 (Some v);
w
let create i =
let create i =
let ht = Hashtbl.create i in
let w = wref ht in
let final x =
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
module Make (X:Util.Sstruct) :
sig
type 'a t
val create : int -> 'a t
(* create a hashtbl with weak key*)
......
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