diff --git a/heptagon/analysis/causal.ml b/heptagon/analysis/causal.ml index 234d9fd..1e5d108 100644 --- a/heptagon/analysis/causal.ml +++ b/heptagon/analysis/causal.ml @@ -37,14 +37,12 @@ type sc = | Ctuple of sc list | Cwrite of ident | Cread of ident - | Clinread of ident | Clastread of ident | Cempty (* normalized constraints *) type ac = | Awrite of ident - | Alinread of ident | Aread of ident | Alastread of ident | Aseq of ac * ac @@ -85,7 +83,6 @@ let output_ac ff ac = fprintf ff ")" | Awrite(m) -> fprintf ff "%s" (sourcename m) | Aread(m) -> fprintf ff "^%s" (sourcename m) - | Alinread(m) -> fprintf ff "*%s" (sourcename m) | Alastread(m) -> fprintf ff "last %s" (sourcename m) end; fprintf ff "@]" in @@ -134,7 +131,6 @@ let rec ctuple l = let conv = function | Cwrite(n) -> Awrite(n) | Cread(n) -> Aread(n) - | Clinread(n) -> Alinread(n) | Clastread(n) -> Alastread(n) | Ctuple(l) -> Atuple (ctuple l) | Cand _ -> Format.printf "Unexpected and\n"; assert false @@ -154,7 +150,6 @@ let rec norm = function | Ctuple l -> Aac(Atuple (ctuple l)) | Cwrite(n) -> Aac(Awrite(n)) | Cread(n) -> Aac(Aread(n)) - | Clinread(n) -> Aac(Alinread(n)) | Clastread(n) -> Aac(Alastread(n)) | _ -> Aempty @@ -166,8 +161,6 @@ let build ac = let rec associate_node g (n_to_graph,lin_map) = function | Awrite(n) -> nametograph n g n_to_graph, lin_map - | Alinread(n) -> - n_to_graph, nametograph n g lin_map | Atuple l -> List.fold_left (associate_node g) (n_to_graph, lin_map) l | _ -> @@ -204,7 +197,6 @@ let build ac = let rec add_dependence g = function | Aread(n) -> attach g n; attach_lin g n - | Alinread(n) -> let g = Env.find n lin_map in attach g n | Atuple l -> List.iter (add_dependence g) l | _ -> () in @@ -220,7 +212,6 @@ let build ac = ) in match ac with - | Alinread n -> Env.find n lin_map | Awrite n -> Env.find n n_to_graph | Atuple l -> begin try @@ -247,7 +238,6 @@ let build ac = top1 @ top2, bot1 @ bot2 | Awrite(n) -> let g = Env.find n n_to_graph in [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) -> let g = node_for_ac ac in List.iter (add_dependence g) l; diff --git a/heptagon/analysis/causality.ml b/heptagon/analysis/causality.ml index bbe92bc..f425591 100644 --- a/heptagon/analysis/causality.ml +++ b/heptagon/analysis/causality.ml @@ -16,7 +16,6 @@ open Names open Ident open Heptagon open Location -open Linearity open Graph open Causal @@ -56,7 +55,6 @@ let rec cseqlist l = | c1 :: l -> cseq c1 (cseqlist l) let read x = Cread(x) -let linread x = Clinread(x) let lastread x = Clastread(x) let cwrite x = Cwrite(x) @@ -66,7 +64,7 @@ let rec pre = function | Cand(c1, c2) -> Cand(pre c1, pre c2) | Ctuple l -> Ctuple (List.map pre l) | Cseq(c1, c2) -> Cseq(pre c1, pre c2) - | Cread(x) | Clinread (x) -> Cempty + | Cread(x) -> Cempty | (Cwrite _ | Clastread _ | Cempty) as c -> c (* projection and restriction *) @@ -86,7 +84,7 @@ let clear env c = let c2 = clearec c2 in cseq c1 c2 | Ctuple l -> Ctuple (List.map clearec l) - | Cwrite(id) | Cread(id) | Clinread(id) | Clastread(id) -> + | Cwrite(id) | Cread(id) | Clastread(id) -> if IdentSet.mem id env then Cempty else c | Cempty -> c in clearec c @@ -99,11 +97,7 @@ let rec typing e = match e.e_desc with | Econst(c) -> cempty | Econstvar(x) -> cempty - | Evar(x) -> - (match e.e_linearity with - | At _ -> linread x - | _ -> read x - ) + | Evar(x) -> read x | Elast(x) -> lastread x | Etuple(e_list) -> candlist (List.map typing e_list) @@ -114,7 +108,6 @@ let rec typing e = candlist l | Earray(e_list) -> candlist (List.map typing e_list) - | Ereset_mem _ -> assert false (** Typing an application *) and apply op e_list = @@ -133,14 +126,24 @@ and apply op e_list = let i2 = typing e2 in let i3 = typing e3 in cseq t1 (cor i2 i3) - | (Enode _ | Eevery _ | Eop _ | Eiterator (_, _, _, _) - | Econcat | Eselect_slice | Emake _ | Eflatten _ - | Eselect_dyn | Eselect _ | Erepeat | Ecopy), e_list -> - ctuplelist (List.map typing e_list) - | Eupdate _, [e1;e2] | Efield_update _, [e1;e2] -> - let t1 = typing e1 in - let t2 = typing e2 in - cseq t2 t1 + | Ecall _, e_list -> + ctuplelist (List.map typing e_list) + | Efield_update _, [e1;e2] -> + let t1 = typing e1 in + let t2 = typing e2 in + cseq t2 t1 + | Earray_op op, e_list -> + apply_array_op op e_list + +and apply_array_op op e_list = + match op, e_list with + | (Eiterator (_, _, _) | Econcat | Eselect_slice + | Eselect_dyn | Eselect _ | Erepeat), e_list -> + ctuplelist (List.map typing e_list) + | Eupdate _, [e1;e2] -> + let t1 = typing e1 in + let t2 = typing e2 in + cseq t2 t1 let rec typing_pat = function | Evarpat(x) -> cwrite(x) diff --git a/heptagon/analysis/initialization.ml b/heptagon/analysis/initialization.ml index 1b551a3..fa57e8b 100644 --- a/heptagon/analysis/initialization.ml +++ b/heptagon/analysis/initialization.ml @@ -16,6 +16,7 @@ open Misc open Names open Ident open Heptagon +open Types open Location open Format @@ -90,8 +91,8 @@ let rec initialized i = (* build an initialization type from a type *) let rec skeleton i ty = match ty with - | Tbase _ -> leaf i | Tprod(ty_list) -> product (List.map (skeleton i) ty_list) + | _ -> leaf i (* sub-typing *) let rec less left_ty right_ty = @@ -188,10 +189,6 @@ let less_exp e actual_ty expected_ty = less actual_ty expected_ty with | Unify -> Error.message e.e_loc (Error.Eclash(actual_ty, expected_ty)) -(** Is-it a safe imported value? *) -let safe f = - let { Global.info = { Global.safe = s } } = Modules.find_value f in s - (** Main typing function *) let rec typing h e = match e.e_desc with @@ -234,19 +231,8 @@ and apply h op e_list = let i2 = itype (typing h e2) in let i3 = itype (typing h e3) in max i1 (max i2 i3) - | (Enode(f,_) | Eevery(f,_)), e_list -> - List.iter (fun e -> initialized_exp h e) e_list; izero - | Eop(f,_), e_list when safe f -> - (* unsafe primitives must have an initialized argument *) - List.fold_left (fun acc e -> itype (typing h e)) izero e_list - | Eop(f,_), e_list -> - List.iter (fun e -> initialized_exp h e) e_list; izero -(*Array operators*) - | (Erepeat | Econcat | Eupdate _ | Efield_update _ - | Eselect _ | Eselect_dyn | Eselect_slice - | Eiterator _ | Ecopy | Emake _ | Eflatten _), e_list -> - List.iter (fun e -> initialized_exp h e) e_list; izero - | _ -> assert false + | (Ecall _ | Earray_op _| Efield_update _) , e_list -> + List.iter (fun e -> initialized_exp h e) e_list; izero and expect h e expected_ty = let actual_ty = typing h e in