Commit 9ff4791e authored by David Hauzar's avatar David Hauzar

Applying projection functions transitively.

Transformation intro_projections_counterexmp applies projection
functions transitively.
parent 45e52f64
module M
use import ref.Ref
use import list.List
use import int.Int
function projf1 "model_trace:.projf1" (l : int) : int
type int_type = Integer int
function projfi "model_trace:.projfi" (l : int) : int
meta "inline : no" function projfi
meta "model_projection" function projfi
function projfl "model_trace:.projfl" (l : list int_type) : int
=
match l with
| Nil -> 0
| Cons (Integer n) _ -> n
| _ -> 0
end
function projf1 "model_trace:.projf1" (l : int) : bool
=
l+10
l > 0
function projf2 "model_trace:projf2" (l : int) : int
function projf2 "model_trace:.projf2" (l : int) : bool
=
l-10
l <= 0
meta "inline : no" function projfl
meta "model_projection" function projfl
meta "inline : no" function projf1
meta "model_projection" function projf1
......@@ -19,6 +36,15 @@ module M
val y "model_projected" "model" "model_trace:y" :ref int
let proj_test ( l "model_projected" : list int_type) : int
ensures { result > 0 }
=
match l with
| Nil -> 1
| Cons (Integer n) _ -> n
| _ -> 1
end
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
ensures { "model_vc" "model_func" !x23 = old !x23 + 2 + !y }
=
......
......@@ -13,7 +13,7 @@ open Ident
open Term
open Decl
(*
(* Debugging functions *)
let debug = Debug.register_info_flag "intro_projections_counterexmp"
~desc:"Print@ debugging@ messages@ about@ introducing@ projections@ for@ counterexamples."
......@@ -30,6 +30,7 @@ let debug_decl decl =
Pretty.print_decl Format.str_formatter decl;
let s = Format.flush_str_formatter () in
Debug.dprintf debug "Declaration %s @." s
*)
(* Label for terms that should be in counterexample *)
let model_label = Ident.create_label "model"
......@@ -68,15 +69,15 @@ let intro_proj_for_ls map_projs ls_projected =
(* Returns list of declarations for projection of ls_projected
if it has a label "model_projected", otherwise returns [].
There can be more projection functions for ls_projected. For
each projection function f the declarations include:
- declaration of new constant with labels of ls_projected
and label "model"
There can be more projections for ls_projected. For each projection
f the declarations include:
- declaration of new constant with labels of ls_projected, label "model",
and label "model_trace:proj_name" where proj_name is the name of the projection
- declaration of axiom saying that the new constant is equal to
ls_projected projected by its projection function
ls_projected projected by its projection
The projection functions for ls_declared are stored in map_projs
with key ls_projected.ls_value
The projection is composed from projection functions stored in
map_projs.
@param map_projs maps types to projection function for these types
@param ls_projected the label symbol that should be projected
......@@ -87,37 +88,61 @@ let intro_proj_for_ls map_projs ls_projected =
else
match ls_projected.ls_value with
| None -> []
| Some ty_projected ->
let introduce_constant t_proj proj_name =
(* introduce new constant c and axiom stating c = t_proj *)
| Some _ ->
let introduce_constant t_rhs proj_name =
(* introduce new constant c and axiom stating c = t_rhs *)
let const_label = Slab.add model_label ls_projected.ls_name.id_label in
let const_label = append_to_model_element_name ~labels:const_label ~to_append:proj_name in
let const_loc = Opt.get ls_projected.ls_name.id_loc in
let const_name = ls_projected.ls_name.id_string^"_proj_constant_"^proj_name in
let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom_"^proj_name in
intro_const_equal_to_term ~term:t_proj ~const_label ~const_loc ~const_name ~axiom_name in
intro_const_equal_to_term ~term:t_rhs ~const_label ~const_loc ~const_name ~axiom_name in
let rec projections_for_term term proj_name applied_projs map_projs =
(* Return declarations for projections of the term.
Parameter proj_name is the name of the projection
Parameter applied_proj_f is a set of projection functions already applied to term*)
try
(* Find all projection functions for the term *)
let pfs = Ty.Mty.find (Opt.get term.t_ty) map_projs in
(* Collect declarations for projections f of the form
f = pf_n .. pf_1 where pf_1 is an element of pfs *)
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant term proj_name
else
let t_applied = Term.t_app pf_1 [term] pf_1.ls_value in
let pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name in
let applied_projs = Term.Sls.add pf_1 applied_projs in
(* Return declarations for projections of t_applied = pf_1 term *)
let t_applied_projs = projections_for_term t_applied proj_name applied_projs map_projs in
List.append l t_applied_projs
)
[]
pfs
with Not_found ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant term proj_name
in
(* Create term from ls_projected *)
let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
try
let fs = Ty.Mty.find ty_projected map_projs in
(* Introduce constant c for each projectin function f stating that c = f t_projected *)
List.fold_left
(fun l f ->
let proj_name =
try
get_model_element_name ~labels:f.ls_name.id_label
with Not_found -> "" in
List.append l (introduce_constant (Term.t_app f [t_projected] f.ls_value) proj_name))
[]
fs
with Not_found ->
(* There are no projection functions, introduce constant c and and axiom stating c = t_projected *)
introduce_constant t_projected ""
projections_for_term t_projected "" Term.Sls.empty map_projs
let introduce_projs map_projs decl =
match decl.d_node with
| Dparam ls_projected ->
(* Create declarations for a projection of ls_projected *)
(* Create declarations for a projections of ls_projected *)
let projection_decls = intro_proj_for_ls map_projs ls_projected in
decl::projection_decls
......@@ -160,8 +185,8 @@ let intro_projections_counterexmp =
let () = Trans.register_transform "intro_projections_counterexmp" intro_projections_counterexmp
~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ with@ label@ model_projected@ \
and@ projectin@ funtion@ f@ for@ p@ creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom@ \
c = f p,@ if@ there@ is@ no@ projection@ function@ creates@ constant@ c@ and@ axiom@ c = p."
and@ projectin@ f@ for@ p@ creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom@ \
c = f p."
(*
Local Variables:
......
......@@ -13,16 +13,20 @@ val intro_projections_counterexmp : Task.task Trans.trans
(**
Transformation that for each declared abstract function or predicate
p labeled with label "model_projected" creates a declaration of new
constant c labeled with label "model" and declaration of new axiom.
If there exists a projection function f for p, the axiom states that
c = f p, otherwise it states that c = p.
constant c labeled with label "model" and declaration of new axiom
stating that c = f p where f is projection for p.
Projection functions are functions tagged with metas "model_projection"
and "inline : no" (the latter is needed just to prevent inlinng of this
function).
Function f is projection function for abstract function or predicate p
if f is tagged with meta "model_projection" and has a single argument
of the same type as is the type of p.
Projections are composed from projection functions. Projection function
is a function with a single argument tagged with metas "model_projection".
Projection f for abstract function or predicate p is defined as:
f = pf_n ... pf_1 id where id is identity function and pf_i for i = 1 .. n
are projection functions for that it holds that the argument of pf_1 is of
the same type as p, the return value of pf_i is of the same type as the argument
of pf_i+1, for all i, j = 1 .. n pf_i <> pf_j, and there is no projection
function pf that could further project f.
projected.
That is, projection for p is identify if there is no projection function with
an argument of the same type as p.
Projections can be given names by labeling projection function by label
of the form "model_trace:proj_name".
......
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