Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit ffd3526f authored by Andrei Paskevich's avatar Andrei Paskevich

type cloning: a couple of fixes

parent c34a77cd
......@@ -304,13 +304,14 @@ let mk_decl_meta = let r = ref 0 in fun meta node pure ->
let mk_decl = mk_decl_meta []
let close_record_invariant ts fl itd =
let axiom_of_invariant itd =
let ts = itd.itd_its.its_ts in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let u = create_vsymbol (id_fresh "self") ty in
let tl = [t_var u] in
let add_fd sbs s = let pj = ls_of_rs s in
Mvs.add (fd_of_rs s).pv_vs (t_app pj tl pj.ls_value) sbs in
let sbs = List.fold_left add_fd Mvs.empty fl in
let sbs = List.fold_left add_fd Mvs.empty itd.itd_fields in
let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
t_forall_close [u] [] inv
......@@ -362,7 +363,7 @@ let create_type_decl dl =
let meta = Theory.(meta_float, [MAts ts; MAls pj_ls; MAls iF_ls]) in
mk_decl_meta [meta] (PDtype [itd]) pure
| fl, _, NoDef when itd.itd_invariant <> [] ->
let inv = close_record_invariant ts fl itd in
let inv = axiom_of_invariant itd in
let pr = create_prsymbol (id_derive (nm ^ "'invariant") id) in
let ax = create_prop_decl Paxiom pr inv in
let add_fd s dl = create_param_decl (ls_of_rs s) :: dl in
......
......@@ -91,9 +91,9 @@ and pdecl_node = private
and meta_decl = Theory.meta * Theory.meta_arg list
val close_record_invariant : tysymbol -> rsymbol list -> its_defn -> term
(** [close_record_invariant ts fl itd] universally closes a record invariant
with a variable 'self', of the record type, with respect to the list [fl]. *)
val axiom_of_invariant : its_defn -> term
(** [axiom_of_invariant itd] returns a closed formula that postulates
the type invariant of [itd] for all values of the type *)
val create_type_decl : its_defn list -> pdecl list
......
......@@ -669,33 +669,28 @@ let clone_type_decl inst cl tdl kn =
end else
(* abstract *)
if s.its_private && cloned then begin
(* FIXME: currently, we cannot refine a block of mutual types *)
if List.length tdl <> 1 then raise (CannotInstantiate id);
(* FIXME: better error messsage *)
begin match Mts.find_opt ts inst.mi_ts with
| Some s' ->
if not (List.length ts.ts_args = List.length s'.its_ts.ts_args) then
raise (BadInstance id);
let pd' = Mid.find s'.its_ts.ts_name kn in
let d' = begin match pd'.pd_node with
let d' = match pd'.pd_node with
| PDtype [d'] -> d'
| PDtype _ -> (* FIXME: we could refine with mutual types *)
raise (BadInstance id)
| PDlet _ | PDexn _ | PDpure -> raise (BadInstance id)
end in
(* FIXME: we could refine with mutual types *)
| PDtype _ -> raise (BadInstance id)
| PDlet _ | PDexn _ | PDpure -> raise (BadInstance id) in
clone_type_record cl s d s' d'; (* clone record fields *)
(* generate and add VC for type invariant implication *)
begin match d.itd_invariant, d'.itd_invariant with
| [], _ -> ()
| _, [] -> raise (BadInstance id) (* TODO? also reject the *)
(* trivial invariant ? *)
| _ ->
let inv = close_record_invariant s.its_ts d.itd_fields d in
let inv = clone_invl cl (sm_of_cl cl) [inv] in
if d.itd_invariant <> [] then begin
let inv = axiom_of_invariant d in
let invl = clone_invl cl (sm_of_cl cl) [inv] in
let add_vc inv = vcs := (d.itd_its, inv) :: !vcs in
List.iter add_vc inv end
List.iter add_vc invl end
| None -> begin match Mts.find_opt ts inst.mi_ty with
| Some ity -> (* creative indentation *)
(* TODO: clone_type_record, axiom_of_invariant *)
(* TODO: should we only allow cloning into ity for
private types with no fields and no invariant? *)
let stv = Stv.of_list ts.ts_args in
if not (Stv.subset (ity_freevars Stv.empty ity) stv &&
its_pure s && ity_immutable ity) then raise (BadInstance id);
......@@ -740,6 +735,7 @@ let clone_type_decl inst cl tdl kn =
cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
save_itd itd
end
and conv_ity alg ity =
let rec down ity = match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl}
......
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