Causality check for linear types
This commit is contained in:
parent
0728f3dae7
commit
d5218ff91c
|
@ -36,6 +36,7 @@ type sc =
|
||||||
| Ctuple of sc list
|
| Ctuple of sc list
|
||||||
| Cwrite of ident
|
| Cwrite of ident
|
||||||
| Cread of ident
|
| Cread of ident
|
||||||
|
| Clinread of ident
|
||||||
| Clastread of ident
|
| Clastread of ident
|
||||||
| Cempty
|
| Cempty
|
||||||
|
|
||||||
|
@ -43,6 +44,7 @@ type sc =
|
||||||
type ac =
|
type ac =
|
||||||
| Awrite of ident
|
| Awrite of ident
|
||||||
| Aread of ident
|
| Aread of ident
|
||||||
|
| Alinread of ident
|
||||||
| Alastread of ident
|
| Alastread of ident
|
||||||
| Aseq of ac * ac
|
| Aseq of ac * ac
|
||||||
| Aand of ac * ac
|
| Aand of ac * ac
|
||||||
|
@ -71,6 +73,7 @@ let output_ac ff ac =
|
||||||
fprintf ff "@[%a@]" (print_list_r (print 1) "(" "," ")") acs
|
fprintf ff "@[%a@]" (print_list_r (print 1) "(" "," ")") acs
|
||||||
| Awrite(m) -> fprintf ff "%s" (name m)
|
| Awrite(m) -> fprintf ff "%s" (name m)
|
||||||
| Aread(m) -> fprintf ff "^%s" (name m)
|
| Aread(m) -> fprintf ff "^%s" (name m)
|
||||||
|
| Alinread(m) -> fprintf ff "*%s" (name m)
|
||||||
| Alastread(m) -> fprintf ff "last %s" (name m)
|
| Alastread(m) -> fprintf ff "last %s" (name m)
|
||||||
in
|
in
|
||||||
fprintf ff "@[<v 1>%a@]@?" (print 0) ac
|
fprintf ff "@[<v 1>%a@]@?" (print 0) ac
|
||||||
|
@ -131,6 +134,7 @@ and norm = function
|
||||||
| Ctuple l -> ctuple (List.map norm l)
|
| Ctuple l -> ctuple (List.map norm l)
|
||||||
| Cwrite(n) -> Aac(Awrite(n))
|
| Cwrite(n) -> Aac(Awrite(n))
|
||||||
| Cread(n) -> Aac(Aread(n))
|
| Cread(n) -> Aac(Aread(n))
|
||||||
|
| Clinread(n) -> Aac(Alinread(n))
|
||||||
| Clastread(n) -> Aac(Alastread(n))
|
| Clastread(n) -> Aac(Alastread(n))
|
||||||
| _ -> Aempty
|
| _ -> Aempty
|
||||||
|
|
||||||
|
@ -139,39 +143,48 @@ let build ac =
|
||||||
(* associate a graph node for each name declaration *)
|
(* associate a graph node for each name declaration *)
|
||||||
let nametograph n g n_to_graph = Env.add n g n_to_graph in
|
let nametograph n g n_to_graph = Env.add n g n_to_graph in
|
||||||
|
|
||||||
let rec associate_node g n_to_graph = function
|
let rec associate_node g (n_to_graph, lin_map) = function
|
||||||
| Awrite(n) ->
|
| Awrite(n) ->
|
||||||
nametograph n g n_to_graph
|
nametograph n g n_to_graph, lin_map
|
||||||
|
| Alinread(n) ->
|
||||||
|
n_to_graph, nametograph n g lin_map
|
||||||
| Atuple l ->
|
| Atuple l ->
|
||||||
List.fold_left (associate_node g) n_to_graph l
|
List.fold_left (associate_node g) (n_to_graph, lin_map) l
|
||||||
| _ ->
|
| _ ->
|
||||||
n_to_graph
|
n_to_graph, lin_map
|
||||||
in
|
in
|
||||||
|
|
||||||
(* first build the association [n -> node] *)
|
(* first build the association [n -> node] *)
|
||||||
(* for every defined variable *)
|
(* for every defined variable *)
|
||||||
let rec initialize ac n_to_graph =
|
let rec initialize ac n_to_graph lin_map =
|
||||||
match ac with
|
match ac with
|
||||||
| Aand(ac1, ac2) ->
|
| Aand(ac1, ac2) ->
|
||||||
let n_to_graph = initialize ac1 n_to_graph in
|
let n_to_graph, lin_map = initialize ac1 n_to_graph lin_map in
|
||||||
initialize ac2 n_to_graph
|
initialize ac2 n_to_graph lin_map
|
||||||
| Aseq(ac1, ac2) ->
|
| Aseq(ac1, ac2) ->
|
||||||
let n_to_graph = initialize ac1 n_to_graph in
|
let n_to_graph, lin_map = initialize ac1 n_to_graph lin_map in
|
||||||
initialize ac2 n_to_graph
|
initialize ac2 n_to_graph lin_map
|
||||||
| _ ->
|
| _ ->
|
||||||
let g = make ac in
|
let g = make ac in
|
||||||
associate_node g n_to_graph ac
|
associate_node g (n_to_graph, lin_map) ac
|
||||||
in
|
in
|
||||||
|
|
||||||
let make_graph ac n_to_graph =
|
let make_graph ac n_to_graph lin_map =
|
||||||
let attach node n =
|
let attach node n =
|
||||||
try
|
try
|
||||||
let g = Env.find n n_to_graph in add_depends node g
|
let g = Env.find n n_to_graph in add_depends node g
|
||||||
with
|
with
|
||||||
| Not_found -> () in
|
| Not_found -> () in
|
||||||
|
|
||||||
|
let attach_lin node n =
|
||||||
|
try
|
||||||
|
let g = Env.find n lin_map in add_depends g node
|
||||||
|
with
|
||||||
|
| Not_found -> () in
|
||||||
|
|
||||||
let rec add_dependence g = function
|
let rec add_dependence g = function
|
||||||
| Aread(n) -> attach g n
|
| Aread(n) -> attach g n; attach_lin g n
|
||||||
|
| Alinread(n) -> let g = Env.find n lin_map in attach g n
|
||||||
| _ -> ()
|
| _ -> ()
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -187,12 +200,12 @@ let build ac =
|
||||||
in
|
in
|
||||||
match ac with
|
match ac with
|
||||||
| Awrite n -> Env.find n n_to_graph
|
| Awrite n -> Env.find n n_to_graph
|
||||||
|
| Alinread n -> Env.find n lin_map
|
||||||
| Atuple l ->
|
| Atuple l ->
|
||||||
begin try
|
(try
|
||||||
node_for_tuple l
|
node_for_tuple l
|
||||||
with Not_found
|
with Not_found
|
||||||
_ -> make ac
|
_ -> make ac)
|
||||||
end
|
|
||||||
| _ -> make ac
|
| _ -> make ac
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -211,7 +224,8 @@ let build ac =
|
||||||
top2;
|
top2;
|
||||||
top1 @ top2, bot1 @ bot2
|
top1 @ top2, bot1 @ bot2
|
||||||
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
|
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
|
||||||
| Aread(n) -> let g = make ac in attach g n; [g], [g]
|
| Aread(n) ->let g = make ac in attach g n; attach_lin g n; [g], [g]
|
||||||
|
| Alinread(n) -> let g = Env.find n lin_map in attach g n; [g], [g]
|
||||||
| Atuple(l) ->
|
| Atuple(l) ->
|
||||||
let make_graph_tuple ac =
|
let make_graph_tuple ac =
|
||||||
match ac with
|
match ac with
|
||||||
|
@ -230,8 +244,8 @@ let build ac =
|
||||||
let top_list, bot_list = make_graph ac in
|
let top_list, bot_list = make_graph ac in
|
||||||
graph top_list bot_list in
|
graph top_list bot_list in
|
||||||
|
|
||||||
let n_to_graph = initialize ac Env.empty in
|
let n_to_graph, lin_map = initialize ac Env.empty Env.empty in
|
||||||
let g = make_graph ac n_to_graph in
|
let g = make_graph ac n_to_graph lin_map in
|
||||||
g
|
g
|
||||||
|
|
||||||
(* the main entry. *)
|
(* the main entry. *)
|
||||||
|
|
|
@ -15,6 +15,7 @@ open Idents
|
||||||
open Heptagon
|
open Heptagon
|
||||||
open Location
|
open Location
|
||||||
open Sgraph
|
open Sgraph
|
||||||
|
open Linearity
|
||||||
open Causal
|
open Causal
|
||||||
|
|
||||||
let cempty = Cempty
|
let cempty = Cempty
|
||||||
|
@ -53,6 +54,7 @@ let rec cseqlist l =
|
||||||
| c1 :: l -> cseq c1 (cseqlist l)
|
| c1 :: l -> cseq c1 (cseqlist l)
|
||||||
|
|
||||||
let read x = Cread(x)
|
let read x = Cread(x)
|
||||||
|
let linread x = Clinread(x)
|
||||||
let lastread x = Clastread(x)
|
let lastread x = Clastread(x)
|
||||||
let cwrite x = Cwrite(x)
|
let cwrite x = Cwrite(x)
|
||||||
|
|
||||||
|
@ -62,7 +64,7 @@ let rec pre = function
|
||||||
| Cand(c1, c2) -> Cand(pre c1, pre c2)
|
| Cand(c1, c2) -> Cand(pre c1, pre c2)
|
||||||
| Ctuple l -> Ctuple (List.map pre l)
|
| Ctuple l -> Ctuple (List.map pre l)
|
||||||
| Cseq(c1, c2) -> Cseq(pre c1, pre c2)
|
| Cseq(c1, c2) -> Cseq(pre c1, pre c2)
|
||||||
| Cread _ -> Cempty
|
| Cread _ | Clinread _ -> Cempty
|
||||||
| (Cwrite _ | Clastread _ | Cempty) as c -> c
|
| (Cwrite _ | Clastread _ | Cempty) as c -> c
|
||||||
|
|
||||||
(* projection and restriction *)
|
(* projection and restriction *)
|
||||||
|
@ -82,7 +84,7 @@ let clear env c =
|
||||||
let c2 = clearec c2 in
|
let c2 = clearec c2 in
|
||||||
cseq c1 c2
|
cseq c1 c2
|
||||||
| Ctuple l -> Ctuple (List.map clearec l)
|
| Ctuple l -> Ctuple (List.map clearec l)
|
||||||
| Cwrite(id) | Cread(id) | Clastread(id) ->
|
| Cwrite(id) | Cread(id) | Clinread(id) | Clastread(id) ->
|
||||||
if IdentSet.mem id env then Cempty else c
|
if IdentSet.mem id env then Cempty else c
|
||||||
| Cempty -> c in
|
| Cempty -> c in
|
||||||
clearec c
|
clearec c
|
||||||
|
@ -95,7 +97,10 @@ let build dec =
|
||||||
let rec typing e =
|
let rec typing e =
|
||||||
match e.e_desc with
|
match e.e_desc with
|
||||||
| Econst _ -> cempty
|
| Econst _ -> cempty
|
||||||
| Evar(x) -> read x
|
| Evar(x) ->
|
||||||
|
(match e.e_linearity with
|
||||||
|
| Lat _ -> linread x
|
||||||
|
| _ -> read x)
|
||||||
| Elast(x) -> lastread x
|
| Elast(x) -> lastread x
|
||||||
| Epre (_, e) -> pre (typing e)
|
| Epre (_, e) -> pre (typing e)
|
||||||
| Efby (e1, e2) ->
|
| Efby (e1, e2) ->
|
||||||
|
|
Loading…
Reference in a new issue