Commit d6f70069 authored by David Hauzar's avatar David Hauzar

Projections for counterexamples - appending character '.' in addition to

the name of the projection to projected element.
parent 1222ba5b
......@@ -56,10 +56,10 @@ module M
type r = {f "model_trace:field_f" :int; g:bool}
(* Projection functions *)
function projf_r_f "model_trace:.f" (x : r) : int
function projf_r_f "model_trace:f" (x : r) : int
=
x.f
function projf_r_g "model_trace:.g" (x : r) : bool
function projf_r_g "model_trace:g" (x : r) : bool
=
x.g
meta "inline : no" function projf_r_f
......@@ -106,10 +106,10 @@ module M
(*** Records and maps together ***)
type r_map = {f_map:map bool int; g_bool:bool}
function projf_r_map_f_map "model_trace:.f_map" (rec_map : r_map) : map bool int
function projf_r_map_f_map "model_trace:f_map" (rec_map : r_map) : map bool int
=
rec_map.f_map
function projf_r_map_g "model_trace:.g_map" (rec_map : r_map) : bool
function projf_r_map_g "model_trace:g_map" (rec_map : r_map) : bool
=
rec_map.g_bool
meta "inline : no" function projf_r_map_f_map
......@@ -140,15 +140,15 @@ module M
(*******************************************
** Definitions of projections used below **
*******************************************)
function projfi "model_trace:.projfi" (l : int) : int
function projfi "model_trace:projfi" (l : int) : int
= l
meta "inline : no" function projfi
meta "model_projection" function projfi
function projf1 "model_trace:.projf1" (l : int) : bool
function projf1 "model_trace:projf1" (l : int) : bool
=
l > 0
function projf2 "model_trace:.projf2" (l : int) : bool
function projf2 "model_trace:projf2" (l : int) : bool
=
l <= 0
meta "inline : no" function projf1
......@@ -180,7 +180,7 @@ module M
*********************************)
(* Warning: if definition of the following projections are present,
the proof of everything below will not terminate. *)
function projfl "model_trace:.projfl" (l : list int_type) : int
function projfl "model_trace:projfl" (l : list int_type) : int
=
match l with
| Nil -> 0
......
......@@ -105,6 +105,13 @@ let intro_proj_for_ls env map_projs ls_projected =
Parameter proj_name is the name of the projection
Parameter applied_proj_f is a set of projection functions already applied to the term *)
let get_record_field_suffix projection =
let proj_name =
try
get_model_element_name ~labels:projection.ls_name.id_label
with Not_found -> "" in
if proj_name = "" then proj_name else "."^proj_name in
match (Opt.get term.t_ty).ty_node with
| Tyapp (ts, [t_from; t_to]) when ts.ts_name.id_string = "map" -> begin
(* If the term is of map type, check whether t_to (and t_from - to be done later) can be projected.
......@@ -171,11 +178,7 @@ let intro_proj_for_ls env map_projs ls_projected =
let proj_axiom = Decl.create_prop_decl Decl.Paxiom proj_axiom_id fla_axiom in
(* Recursively call projecting of the term proj_map -> proj_map_projections *)
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 proj_name = proj_name^(get_record_field_suffix pf_1) in
let applied_projs = Term.Sls.add pf_1 applied_projs in
let proj_map_projections_defs = projections_for_term proj_map_t proj_name applied_projs map_projs in
......@@ -204,11 +207,7 @@ let intro_proj_for_ls env map_projs ls_projected =
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 proj_name = proj_name^(get_record_field_suffix pf_1) 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
......
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