jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Made linearity field not optional

Browse source 
This helped solve a few bugs with linear types,
for instance when using automata.
The intermediate code is not well-typed (wrt to
linear types only), after the encoding of automata.
This commit is contained in:
Cédric Pasteur 2011-09-07 17:51:31 +02:00
parent 29a6721121
commit 81947eca40
21 changed files with 265 additions and 196 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
compiler/heptagon/analysis/hept_clocking.ml
View file

@ -111,6 +111,7 @@ let rec typing h pat e =
(Econst (Initial.mk_static_int 0))
~ct_annot:(Some(Ck(base_ck)))
Initial.tint
~linearity:Linearity.Ltop
) nl
in
typing_app h base_ck pat op (pargs@args@il)
@ -126,6 +127,7 @@ let rec typing h pat e =
(Econst (Initial.mk_static_int 0))
~ct_annot:(Some(Ck(base_ck)))
Initial.tint
~linearity:Linearity.Ltop
) nl
in
let rec insert_i args = match args with

28
compiler/heptagon/analysis/typing.ml
View file

@ -23,7 +23,7 @@ open Hept_mapfold
open Pp_tools
open Format
type value = { ty: ty; mutable last: bool }
type value = { vd: var_dec; mutable last: bool }
type error =
| Emissing of name
@ -235,7 +235,13 @@ let kind f ty_desc =
let typ_of_name h x =
try
let { ty = ty } = Env.find x h in ty
let { vd = vd } = Env.find x h in vd.v_type
with
Not_found -> error (Eundefined(name x))
let vd_of_name h x =
try
let { vd = vd } = Env.find x h in vd
with
Not_found -> error (Eundefined(name x))
@ -258,11 +264,11 @@ let rec subst_type_vars m = function
| Tprod l -> Tprod (List.map (subst_type_vars m) l)
| t -> t
let add_distinct_env id ty env =
let add_distinct_env id vd env =
if Env.mem id env then
error (Ealready_defined(name id))
else
Env.add id ty env
Env.add id vd env
let add_distinct_qualset n acc =
if QualSet.mem n acc then
@ -309,8 +315,8 @@ let rec merge local_names_list =
let two s1 s2 =
let total, partial = Env.partition (fun elt -> Env.mem elt s2) s1 in
let partial =
Env.fold (fun elt ty env ->
if not (Env.mem elt total) then Env.add elt ty env
Env.fold (fun elt vd env ->
if not (Env.mem elt total) then Env.add elt vd env
else env)
s2 partial in
total, partial in
@ -951,9 +957,9 @@ and typing_node_params cenv params_sig params =
let rec typing_pat h acc = function
| Evarpat(x) ->
let ty = typ_of_name h x in
let acc = add_distinct_env x ty acc in
acc, ty
let vd = vd_of_name h x in
let acc = add_distinct_env x vd acc in
acc, vd.v_type
| Etuplepat(pat_list) ->
let acc, ty_list =
List.fold_right
@ -1097,8 +1103,8 @@ and build cenv h dec =
if Env.mem vd.v_ident h then
error (Ealready_defined(name vd.v_ident));
let acc_defined = Env.add vd.v_ident ty acc_defined in
let h = Env.add vd.v_ident { ty = ty; last = last vd.v_last } h in
let acc_defined = Env.add vd.v_ident vd acc_defined in
let h = Env.add vd.v_ident { vd = vd; last = last vd.v_last } h in
{ vd with v_last = last_dec; v_type = ty }, (acc_defined, h)
with
TypingError(kind) -> message vd.v_loc kind

8
compiler/heptagon/hept_utils.ml
View file

@ -21,7 +21,7 @@ open Heptagon
(* Helper functions to create AST. *)
(* TODO : After switch, all mk_exp should take care of level_ck *)
let mk_exp desc ?(linearity = Ltop) ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty =
let mk_exp desc ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty ~linearity =
{ e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_linearity = linearity;
e_level_ck = level_ck; e_loc = loc; }
@ -41,7 +41,7 @@ let mk_equation ?(loc=no_location) desc =
eq_inits = Lno_init;
eq_loc = loc; }
let mk_var_dec ?(last = Var) ?(linearity = Ltop) ?(clock = fresh_clock()) name ty =
let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty ~linearity =
{ v_ident = name; v_type = ty; v_linearity = linearity; v_clock = clock;
v_last = last; v_loc = no_location }
@ -50,9 +50,9 @@ let mk_block ?(stateful = true) ?(defnames = Env.empty) ?(locals = []) eqs =
b_stateful = stateful; b_loc = no_location; }
let dfalse =
mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) ~linearity:Ltop
let dtrue =
mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool)
mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) ~linearity:Ltop
let mk_ifthenelse e1 e2 e3 =
{ e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }

2
compiler/heptagon/heptagon.ml
View file

@ -96,7 +96,7 @@ and eqdesc =
and block = {
b_local : var_dec list;
b_equs : eq list;
b_defnames : ty Env.t;
b_defnames : var_dec Env.t;
b_stateful : bool;
b_loc : location; }

31
compiler/heptagon/transformations/automata.ml
View file

@ -25,10 +25,11 @@ let fresh = Idents.gen_fresh "automata"
(function S -> "s" | NS -> "ns" | R -> "r" | NR -> "nr" | PNR -> "pnr")
let mk_var_exp n ty =
mk_exp (Evar n) ty
mk_exp (Evar n) ty ~linearity:Linearity.Ltop
let mk_pair e1 e2 =
mk_exp (mk_op_app Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
~linearity:(Linearity.Ltuple [Linearity.Ltop; Linearity.Ltop])
let mk_reset_equation eq_list e =
mk_equation (Ereset (mk_block eq_list, e))
@ -38,7 +39,7 @@ let mk_switch_equation e l =
let mk_exp_fby_false e =
mk_exp (Epre (Some (mk_static_bool false), e))
(Tid Initial.pbool)
(Tid Initial.pbool) ~linearity:Linearity.Ltop
let mk_constructor constr ty =
mk_static_exp ty (Sconstructor constr)
@ -95,7 +96,9 @@ let translate_automaton v eq_list handlers =
let pre_next_resetname = fresh PNR in
let name n = NamesEnv.find n state_env in
let state n = mk_exp (Econst (mk_constructor (name n) tstatetype)) tstatetype in
let state n =
mk_exp (Econst (mk_constructor (name n) tstatetype)) tstatetype ~linearity:Linearity.Ltop
in
let statevar n = mk_var_exp n tstatetype in
let boolvar n = mk_var_exp n (Tid Initial.pbool) in
@ -107,8 +110,10 @@ let translate_automaton v eq_list handlers =
in
let strong { s_state = n; s_unless = su } =
let defnames = Env.add resetname (Tid Initial.pbool) Env.empty in
let defnames = Env.add statename tstatetype defnames in
let rst_vd = mk_var_dec resetname (Tid Initial.pbool) Linearity.Ltop in
let defnames = Env.add resetname rst_vd Env.empty in
let state_vd = mk_var_dec statename tstatetype Linearity.Ltop in
let defnames = Env.add statename state_vd defnames in
let st_eq = mk_simple_equation
(Etuplepat[Evarpat(statename); Evarpat(resetname)])
(escapes n su (boolvar pre_next_resetname)) in
@ -117,8 +122,10 @@ let translate_automaton v eq_list handlers =
in
let weak { s_state = n; s_block = b; s_until = su } =
let defnames = Env.add next_resetname (Tid Initial.pbool) b.b_defnames in
let defnames = Env.add next_statename tstatetype defnames in
let nextrst_vd = mk_var_dec next_resetname (Tid Initial.pbool) Linearity.Ltop in
let defnames = Env.add next_resetname nextrst_vd b.b_defnames in
let nextstate_vd = mk_var_dec next_statename tstatetype Linearity.Ltop in
let defnames = Env.add next_statename nextstate_vd defnames in
let ns_eq = mk_simple_equation
(Etuplepat[Evarpat(next_statename); Evarpat(next_resetname)])
(escapes n su dfalse) in
@ -130,10 +137,10 @@ let translate_automaton v eq_list handlers =
in
let v =
(mk_var_dec next_statename tstatetype) ::
(mk_var_dec resetname (Tid Initial.pbool)) ::
(mk_var_dec next_resetname (Tid Initial.pbool)) ::
(mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in
(mk_var_dec next_statename tstatetype ~linearity:Linearity.Ltop) ::
(mk_var_dec resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop) ::
(mk_var_dec next_resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop) ::
(mk_var_dec pre_next_resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop) :: v in
if no_strong_transition handlers
then (* Only weak transitions : a Moore automaton. *)
let switch_e = mk_exp_fby_state initial (statevar next_statename) in
@ -150,7 +157,7 @@ let translate_automaton v eq_list handlers =
v, switch_eq :: nr_eq :: pnr_eq :: eq_list
else (* General case,
two switch to generate statename variable used and defined *)
let v = (mk_var_dec statename tstatetype) :: v in
let v = (mk_var_dec statename tstatetype ~linearity:Linearity.Ltop) :: v in
let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
let ns_switch_handlers =
List.map (fun ({ s_state = n } as case) ->

176
compiler/heptagon/transformations/boolean.ml
View file

@ -7,7 +7,7 @@
(* *)
(****************************************************)
(*
(*
Translate enumerated types (state variables) into boolean
type t = A | B | C | D
@ -28,7 +28,7 @@
(e when A(x))
-->
(e when False(x1)) when False(x2_0)
ck on A(x)
-->
ck on False(x1) on False(x2_0)
@ -68,7 +68,7 @@ let mk_tuple e_l =
Eapp((mk_app Etuple),e_l,None)
(* boolean decision tree ; left branch for true ; nodes are constructors *)
type btree = Node of constructor_name option | Tree of btree * btree
type btree = Node of constructor_name option | Tree of btree * btree
(* Debug
let print_indent n =
@ -78,7 +78,7 @@ let print_indent n =
let rec print_btree indent bt =
match bt with
| Node(None) ->
| Node(None) ->
print_indent indent;
Printf.printf "None\n"
| Node(Some c) ->
@ -111,8 +111,8 @@ let rec print_bl bl =
let print_enuminfo info =
Printf.printf "{ ty_nb_var = %d;\n ty_assoc = " info.ty_nb_var;
QualEnv.fold
(fun c l () ->
QualEnv.fold
(fun c l () ->
Printf.printf "(%s : " (fullname c);
print_bl l;
Printf.printf "), ")
@ -123,7 +123,7 @@ let print_enuminfo info =
(* ty_nb_var = n : var x of enum type will be represented by
boolean variables x_1,...,x_n
ty_assoc(A) = [b_1,...,b_n] : constant A will be represented by
x_1,...,x_n where x_i = b_i
@ -142,12 +142,12 @@ let print_enuminfo info =
x2_0 being on clock False(x1)
x2_1 being on clock True(x1)
*)
type var_tree = Vempty | VNode of var_ident * var_tree * var_tree
type var_tree = Vempty | VNode of var_ident * var_tree * var_tree
(*
let rec print_var_tree indent t =
match t with
| Vempty ->
| Vempty ->
print_indent indent;
Printf.printf "Empty\n"
| VNode(v,t1,t2) ->
@ -190,13 +190,13 @@ let print_enum_types () =
) !enum_types ()
*)
let get_enum name =
let get_enum name =
QualEnv.find name !enum_types
(* split2 k [x1;...;xn] = ([x1;...;xk],[xk+1;...;xn]) *)
let split2 n l =
let rec splitaux k acc l =
if k = 0 then (acc,l) else
if k = 0 then (acc,l) else
begin
match l with
| x::t -> splitaux (k-1) (x::acc) t
@ -212,10 +212,10 @@ let rec var_list clist =
match clist with
| [] -> (0,QualEnv.empty,Node(None))
| [c] -> (1, QualEnv.add c [false] QualEnv.empty, Tree(Node(Some c),Node(None)))
| [c1;c2] -> (1,
| [c1;c2] -> (1,
QualEnv.add c1 [false] (QualEnv.add c2 [true] QualEnv.empty),
Tree(Node(Some c1),Node(Some c2)))
| l ->
| l ->
let n = List.length l in
let n1 = n asr 1 in
let l1,l2 = split2 n1 l in
@ -239,11 +239,11 @@ let rec var_list clist =
(* | Some n -> n *)
(* end in *)
(* assert (nt2 = nv2); *)
let vl =
let vl =
QualEnv.fold (fun c l m -> QualEnv.add c (true::l) m) vl2
(QualEnv.fold
(if nv1 = nv2
then (fun c l m -> QualEnv.add c (false::l) m)
(QualEnv.fold
(if nv1 = nv2
then (fun c l m -> QualEnv.add c (false::l) m)
else (fun c l m -> QualEnv.add c (false::false::l) m))
vl1
QualEnv.empty) in
@ -263,7 +263,7 @@ let translate_pat env pat =
let rec trans = function
| Evarpat(name) ->
begin
try
try
let info = Env.find name env in
match info.var_enum.ty_nb_var with
| 1 ->
@ -287,7 +287,7 @@ let translate_ty ty =
begin match info with
| Type(_) -> ty
| Enum { ty_nb_var = 1 } -> ty_bool
| Enum { ty_nb_var = n } ->
| Enum { ty_nb_var = n } ->
let strlist = nvar_list "" n in
Tprod(List.map (fun _ -> ty_bool) strlist)
end
@ -312,7 +312,7 @@ let rec translate_ck env ck =
| Cbase -> Cbase
| Cvar {contents = Clink(ck)} -> translate_ck env ck
| Cvar {contents = Cindex(_)} -> ck
| Con(ck,c,n) ->
| Con(ck,c,n) ->
let ck = translate_ck env ck in
begin
try
@ -335,22 +335,22 @@ let translate_const c ty e =
| Sconstructor(cname),Tid(tname) ->
begin
try
begin
begin
match (get_enum tname) with
| Type _ -> Econst(c)
| Enum { ty_assoc = assoc } ->
let bl = QualEnv.find cname assoc in
let b_list = List.map (fun b -> Econst(sbool b)) bl in
begin
match b_list with
begin
match b_list with
| [] -> assert false
| [b] -> b
| _::_ ->
mk_tuple
(List.map
(fun b -> {e with
(fun b -> {e with
e_desc = b;
e_ty = ty_bool })
e_ty = ty_bool })
b_list)
end
end
@ -364,7 +364,7 @@ let new_var_list d_list ty ck n =
| n ->
let v = fresh "bool" in
let acc = v :: acc in
let d_list = (mk_var_dec ~clock:ck v ty) :: d_list in
let d_list = (mk_var_dec ~clock:ck v ty ~linearity:Linearity.Ltop) :: d_list in
varl acc d_list (n-1) in
varl [] d_list n
@ -373,13 +373,13 @@ let assert_ck = function
| _ -> assert false
let intro_tuple context e =
let n =
let n =
match e.e_ty with
| Tprod(l) -> List.length l
| Tprod(l) -> List.length l
| _ -> assert false in
match e.e_desc with
Eapp({a_op=Etuple},e_l,None) -> context,e_l
| _ ->
| _ ->
let (d_list,eq_list) = context in
(* e is not a tuple, therefore e.e_ct_annot = Ck(ck) *)
let ck = assert_ck e.e_ct_annot in
@ -404,7 +404,7 @@ let rec when_list e bl vtree =
let rec when_ck desc li ty ck =
match ck with
| Cbase | Cvar _ ->
| Cbase | Cvar _ ->
{ e_desc = desc;
e_level_ck = ck;
e_ct_annot = Some(Ck(ck));
@ -423,11 +423,11 @@ let rec when_ck desc li ty ck =
let rec base_value ck li ty =
match ty with
| Tid({qual = Pervasives; name = "int" }) ->
| Tid({qual = Pervasives; name = "int" }) ->
when_ck (Econst(mk_static_exp ty (Sint(0)))) li ty ck
| Tid({qual = Pervasives; name = "float"}) ->
when_ck (Econst(mk_static_exp ty (Sfloat(0.)))) li ty ck
| Tid({qual = Pervasives; name = "bool" }) ->
| Tid({qual = Pervasives; name = "bool" }) ->
when_ck (Econst(strue)) li ty ck
| Tid(sname) ->
begin
@ -439,17 +439,17 @@ let rec base_value ck li ty =
| Type(Type_abs) -> failwith("Abstract types not implemented")
| Type(Type_alias aty) -> base_value ck li aty
| Type(Type_enum(l)) ->
when_ck
(Econst(mk_static_exp ty (Sconstructor(List.hd l))))
when_ck
(Econst(mk_static_exp ty (Sconstructor(List.hd l))))
li ty ck
| Type(Type_struct(l)) ->
let fields =
List.map
(fun {f_name = name; f_type = ty} ->
name,(base_value ck li ty))
List.map
(fun {f_name = name; f_type = ty} ->
name,(base_value ck li ty))
l in
when_ck (Estruct(fields)) li ty ck
| Enum { ty_nb_var = 1 } ->
| Enum { ty_nb_var = 1 } ->
when_ck (Econst(strue)) li ty_bool ck
| Enum { ty_nb_var = n } ->
let e = when_ck (Econst(strue)) li ty_bool ck in
@ -486,7 +486,7 @@ let rec base_value ck li ty =
e_loc = no_location;
}
| Tinvalid -> failwith("Boolean: invalid type")
let rec merge_tree ck ty li e_map btree vtree =
match btree, vtree with
| Node(None), _ -> base_value ck li ty
@ -509,7 +509,7 @@ let rec merge_tree ck ty li e_map btree vtree =
let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e) =
let ct = Misc.optional (translate_ct env) ct in
let context,desc =
let context,desc =
match desc with
| Econst(c) ->
context, translate_const c ty e
@ -521,8 +521,8 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
Evar(List.nth info.var_list 0)
else
let ident_list = info.var_list in
mk_tuple (List.map
(fun v -> { e with
mk_tuple (List.map
(fun v -> { e with
e_ty = ty_bool;
e_ct_annot = ct;
e_desc = Evar(v); })
@ -550,17 +550,17 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
| _ -> assert false) e_c_l in
context,
mk_tuple
(List.map2
(fun c e -> { e with
(List.map2
(fun c e -> { e with
e_ty = ty_bool;
e_desc = Epre(Some c,e)})
c_l e_l)
| _ -> assert false
end
| Eapp(app, e_list, r) ->
| Eapp(app, e_list, r) ->
let context,e_list = translate_list env context e_list in
context, Eapp(app, e_list, r)
| Ewhen(e,c,ck) ->
| Ewhen(e,c,ck) ->
let context,e = translate env context e in
begin
try
@ -573,18 +573,18 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
context,Ewhen(e,c,ck)
end
| Emerge(ck,l) (* of name * (longname * exp) list *)
->
->
begin
try
let info = Env.find ck env in
let context,e_map = List.fold_left
(fun (context,e_map) (n,e) ->
let context,e_map = List.fold_left
(fun (context,e_map) (n,e) ->
let context,e = translate env context e in
context,QualEnv.add n e e_map)
context,QualEnv.add n e e_map)
(context,QualEnv.empty) l in
let e_merge =
merge_tree (assert_ck ct) ty e.e_linearity e_map
info.var_enum.ty_tree
let e_merge =
merge_tree (assert_ck ct) ty e.e_linearity e_map
info.var_enum.ty_tree
info.clocked_var in
context,e_merge.e_desc
with Not_found ->
@ -601,32 +601,32 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
let context,e1 = translate env context e1 in
let context,e2 = translate env context e2 in
context,Esplit(e1,e2)
| Estruct(l) ->
let context,acc =
List.fold_left
(fun (context,acc) (c,e) ->
| Estruct(l) ->
let context,acc =
List.fold_left
(fun (context,acc) (c,e) ->
let context,e = translate env context e in
(context,(c,e)::acc))
(context,(c,e)::acc))
(context,[]) l in
context,Estruct(List.rev acc)
| Eiterator(it,app,se,pe_list,e_list,r) ->
let context,pe_list = translate_list env context pe_list in
let context,e_list = translate_list env context e_list in
context,Eiterator(it,app,se,pe_list,e_list,r)
| Elast _ ->
| Elast _ ->
failwith("Boolean: not supported expression (abstract tree should be normalized)")
in
context,{ e with
e_desc = desc;
e_ty = translate_ty ty;
e_ct_annot = ct}
and translate_list env context e_list =
let context,acc_e =
List.fold_left
(fun (context,acc_e) e ->
and translate_list env context e_list =
let context,acc_e =
List.fold_left
(fun (context,acc_e) e ->
let context,e = translate env context e in
(context,e::acc_e))
(context,e::acc_e))
(context,[]) e_list in
context,List.rev acc_e
@ -636,14 +636,14 @@ and translate_list env context e_list =
- equations of these added variables
*)
let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
(* when_ck [v3_1_0;v2_1;v1] (ck on True(v1) on False(v2_1) on True(v3_1_0)) v4
= ((v4 when True(v1)) when False(v2_1)) when True(v3_1_0)
-> builds v4_1_0_1
*)
let rec when_ck ckvar_list ck var =
match ckvar_list,ck with
| [], _ ->
| [], _ ->
{ e_desc = Evar(var);
e_level_ck = ck;
e_ct_annot = Some(Ck(ck));
@ -667,14 +667,14 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
(* From v, build of v1...vn *)
let rec varl acc_vd k =
if k>n
if k>n
then acc_vd
else
begin
let var_prefix = prefix ^ "_" ^ (string_of_int k) in
let var = fresh var_prefix in
(* addition of var_k *)
let acc_vd = { var_from with
let acc_vd = { var_from with
v_ident = var;
v_type = ty_bool } :: acc_vd in
varl acc_vd (k+1)
@ -683,10 +683,10 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
let vd_list = varl [] 1 in
(* v_list = [vn;...;v1] *)
let acc_vd = List.rev_append vd_list acc_vd in
let v_list = List.rev_map (fun vd -> vd.v_ident) vd_list in
(* From v1...vn, build clocked tree
(* From v1...vn, build clocked tree
( vi_(0|1)* on ... on (True|False) (v1) ) *)
let rec clocked_tree (acc_loc,acc_eq) acc_var suffix v_list ck =
begin match v_list, acc_var with
@ -698,10 +698,10 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
(* Build left son (ck on False(vi_...)) *)
let ck_0 = Con(ck,cfalse,v1) in
let acc_loc,acc_eq,t0 =
clocked_tree
clocked_tree
(acc_loc,acc_eq)
([v1])
("_0")
("_0")
v_list ck_0 in
(* Build right son (ck on True(vi_...))*)
let ck_1 = Con(ck,ctrue,v1) in
@ -709,7 +709,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
clocked_tree
(acc_loc,acc_eq)
([v1])
("_1")
("_1")
v_list ck_1 in
acc_loc,acc_eq,VNode(v1,t0,t1)
| vi::v_list, _ ->
@ -730,10 +730,10 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
(* Build left son (ck on False(vi_...)) *)
let ck_0 = Con(ck,cfalse,id) in
let acc_loc,acc_eq,t0 =
clocked_tree
clocked_tree
(acc_loc,acc_eq)
(id::acc_var)
(suffix ^ "_0")
(suffix ^ "_0")
v_list ck_0 in
(* Build right son (ck on True(vi_...))*)
let ck_1 = Con(ck,ctrue,id) in
@ -741,12 +741,12 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
clocked_tree
(acc_loc,acc_eq)
(id::acc_var)
(suffix ^ "_1")
(suffix ^ "_1")
v_list ck_1 in
acc_loc,acc_eq,VNode(id,t0,t1)
end
end
in
let acc_loc,acc_eq,t =
clocked_tree (acc_loc,acc_eq) [] "" v_list var_from.v_clock in
@ -768,8 +768,8 @@ let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
match (get_enum tname) with
| Type _ -> v::acc_vd, acc_loc, acc_eq ,env
| Enum(info) ->
let (acc_vd,acc_loc,acc_eq,vl,t) =
var_dec_list
let (acc_vd,acc_loc,acc_eq,vl,t) =
var_dec_list
(acc_vd,acc_loc,acc_eq)
v info.ty_nb_var in
let vi = { var_enum = info;
@ -806,12 +806,12 @@ let rec translate_block env add_locals add_eqs ({ b_local = v;
let eq_list = eq_list@v_eq@add_eqs in
let context = translate_eqs env eq_list in
let d_list,eq_list = context in
{ b with
{ b with
b_local = v@d_list;
b_equs = eq_list }, env
and translate_eq env context ({eq_desc = desc} as eq) =
let desc,(d_list,eq_list) =
let desc,(d_list,eq_list) =
match desc with
| Eblock block ->
let block, _ = translate_block env [] [] block in
@ -829,7 +829,7 @@ and translate_eq env context ({eq_desc = desc} as eq) =
and translate_eqs env eq_list =
List.fold_left
(fun context eq ->
translate_eq env context eq) ([],[]) eq_list
translate_eq env context eq) ([],[]) eq_list
let translate_contract env contract =
match contract with
@ -846,7 +846,7 @@ let translate_contract env contract =
let context, e_a = translate env' (v,eqs) e_a in
let context, e_g = translate env' context e_g in
let (d_list,eq_list) = context in
Some { c_block = { b with
Some { c_block = { b with
b_local = d_list;
b_equs = eq_list };
c_assume = e_a;
@ -864,7 +864,7 @@ let node ({ n_input = inputs;
let add_locals = in_loc@out_loc in
let add_eqs = in_eq@out_eq in
let b,_ = translate_block env add_locals add_eqs b in
{ n with
{ n with
n_input = List.rev inputs;
n_output = List.rev outputs;
n_contract = contract;
@ -874,12 +874,12 @@ let program_desc p_desc =
match p_desc with
| Pnode(n) -> Pnode(node n)
| _ -> p_desc
let build p_desc =
match p_desc with
| Ptype(type_dec) ->
begin
let tenv =
let tenv =
match type_dec.t_desc with
| Type_enum clist ->
let (n,env,t) = var_list clist in

6
compiler/heptagon/transformations/completion.ml
View file

@ -47,9 +47,9 @@ let funs_collect =
(* adds an equation [x = last(x)] for every partially defined variable *)
(* in a control structure *)
let complete_with_last defined_names local_defined_names eq_list =
let last n ty = mk_exp (Elast n) ty in
let equation n ty eq_list =
(mk_equation (Eeq(Evarpat n, last n ty)))::eq_list in
let last n vd = mk_exp (Elast n) vd.v_type Linearity.Ltop in
let equation n vd eq_list =
(mk_equation (Eeq(Evarpat n, last n vd)))::eq_list in
let d = Env.diff defined_names local_defined_names in
Env.fold equation d eq_list

5
compiler/heptagon/transformations/inline.ml
View file

@ -82,7 +82,7 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
fst (Hept_mapfold.node_dec funs () ni) in
let mk_input_equ vd e = mk_equation (Eeq (Evarpat vd.v_ident, e)) in
let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type in
let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type ~linearity:vd.v_linearity in
let newvars = ni.n_input @ ni.n_block.b_local @ ni.n_output @ newvars
and newequs =
@ -95,7 +95,8 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
| [o] -> mk_output_exp o
| _ ->
mk_exp (Eapp ({ op with a_op = Etuple; },
List.map mk_output_exp ni.n_output, None)) exp.e_ty in
List.map mk_output_exp ni.n_output, None)) exp.e_ty
~linearity:exp.e_linearity in
(res_e, (env, newvars, newequs))
| _ -> Hept_mapfold.exp funs (env, newvars, newequs) exp

36
compiler/heptagon/transformations/itfusion.ml
View file

@ -51,13 +51,23 @@ match l with
| [vd] -> Evarpat (vd.v_ident)
| _ -> Etuplepat (List.map (fun vd -> Evarpat vd.v_ident) l)
let type_of_vd_list l =
Types.prod (List.map (fun vd -> vd.v_type) l)
let linearity_of_vd_list l =
Linearity.prod (List.map (fun vd -> vd.v_linearity) l)
let exp_of_vd vd =
mk_exp (Evar vd.v_ident) vd.v_type ~linearity:vd.v_linearity
let tuple_of_vd_list l =
let el = List.map (fun vd -> mk_exp (Evar vd.v_ident) vd.v_type) l in
let ty = Types.prod (List.map (fun vd -> vd.v_type) l) in
mk_exp (Eapp (mk_app Etuple, el, None)) ty
let el = List.map exp_of_vd l in
let ty = type_of_vd_list l in
let lin = linearity_of_vd_list l in
mk_exp (Eapp (mk_app Etuple, el, None)) ty ~linearity:lin
let vd_of_arg ad =
mk_var_dec (fresh_vd_of_arg ad) ad.a_type
mk_var_dec (fresh_vd_of_arg ad) ad.a_type ad.a_linearity
(** @return the lists of inputs and outputs (as var_dec) of
an app object. *)
@ -80,10 +90,10 @@ let get_node_inp_outp app = match app.a_op with
added equations. *)
let mk_call app acc_eq_list =
let new_inp, new_outp = get_node_inp_outp app in
let args = List.map (fun vd -> mk_exp
(Evar vd.v_ident) vd.v_type) new_inp in
let out_ty = Types.prod (List.map (fun vd -> vd.v_type) new_outp) in
let e = mk_exp (Eapp (app, args, None)) out_ty in
let args = List.map exp_of_vd new_inp in
let out_ty = type_of_vd_list new_outp in
let out_lin = linearity_of_vd_list new_outp in
let e = mk_exp (Eapp (app, args, None)) out_ty ~linearity:out_lin in
match List.length new_outp with
| 1 -> new_inp, e, acc_eq_list
| _ ->
@ -112,9 +122,8 @@ let edesc funs acc ed =
let new_inp, e, acc_eq_list = mk_call g acc_eq_list in
new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true
| _ ->
let vd = mk_var_dec (fresh_var ()) e.e_ty in
let x = mk_exp (Evar vd.v_ident) vd.v_type in
vd::inp, acc_eq_list, x::largs, e::args, b
let vd = mk_var_dec (fresh_var ()) e.e_ty e.e_linearity in
vd::inp, acc_eq_list, (exp_of_vd vd)::largs, e::args, b
in
let inp, acc_eq_list, largs, args, can_be_fused =
@ -123,8 +132,9 @@ let edesc funs acc ed =
then (
(* create the call to f in the lambda fun *)
let _, outp = get_node_inp_outp f in
let f_out_type = Types.prod (List.map (fun v -> v.v_type) outp) in
let call = mk_exp (Eapp(f, largs, None)) f_out_type in
let f_out_type = type_of_vd_list outp in
let f_out_lin = linearity_of_vd_list outp in
let call = mk_exp (Eapp(f, largs, None)) f_out_type f_out_lin in
let eq = mk_equation (Eeq(pat_of_vd_list outp, call)) in
(* create the lambda *)
let anon = mk_app

10
compiler/heptagon/transformations/last.ml
View file

@ -18,16 +18,18 @@ let fresh = Idents.gen_fresh "last" Idents.name
(* introduce a fresh equation [last_x = pre(x)] for every *)
(* variable declared with a last *)
let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } =
let last (eq_list, env, v) { v_ident = n; v_type = t; v_linearity = lin; v_last = last } =
match last with
| Var -> (eq_list, env, v)
| Last(default) ->
let lastn = fresh n in
let eq = mk_equation (Eeq (Evarpat lastn,
mk_exp (Epre (default, mk_exp (Evar n) t)) t)) in
let eq =
mk_equation (Eeq (Evarpat lastn,
mk_exp (Epre (default,
mk_exp (Evar n) t Linearity.Ltop)) t lin)) in
eq:: eq_list,
Env.add n lastn env,
(mk_var_dec lastn t) :: v
(mk_var_dec lastn t lin) :: v
let extend_env env v = List.fold_left last ([], env, []) v

36
compiler/heptagon/transformations/normalize.ml
View file

@ -15,6 +15,7 @@ open Hept_utils
open Hept_mapfold
open Types
open Clocks
open Linearity
open Format
(** Normalization pass
@ -36,7 +37,7 @@ end
let exp_list_of_static_exp_list se_list =
let mk_one_const se =
mk_exp (Econst se) se.se_ty
mk_exp (Econst se) se.se_ty ~linearity:Ltop
in
List.map mk_one_const se_list
@ -61,23 +62,29 @@ let flatten_e_list l =
(** Creates a new equation x = e, adds x to d_list
and the equation to eq_list. *)
let equation (d_list, eq_list) e =
let add_one_var ty d_list =
let add_one_var ty lin d_list =
let n = Idents.gen_var "normalize" "v" in
let d_list = (mk_var_dec n ty) :: d_list in
let d_list = (mk_var_dec n ty lin) :: d_list in
n, d_list
in
match e.e_ty with
| Tprod ty_list ->
let lin_list =
(match e.e_linearity with
| Ltuple l -> l
| Ltop -> Misc.repeat_list Ltop (List.length ty_list)
| _ -> assert false)
in
let var_list, d_list =
mapfold (fun d_list ty -> add_one_var ty d_list) d_list ty_list in
mapfold2 (fun d_list ty lin -> add_one_var ty lin d_list) d_list ty_list lin_list in
let pat_list = List.map (fun n -> Evarpat n) var_list in
let eq_list = (mk_equation (Eeq (Etuplepat pat_list, e))) :: eq_list in
let e_list = List.map2
(fun n ty -> mk_exp (Evar n) ty) var_list ty_list in
let e_list = Misc.map3
(fun n ty lin -> mk_exp (Evar n) ty lin) var_list ty_list lin_list in
let e = Eapp(mk_app Etuple, e_list, None) in
(d_list, eq_list), e
| _ ->
let n, d_list = add_one_var e.e_ty d_list in
let n, d_list = add_one_var e.e_ty e.e_linearity d_list in
let eq_list = (mk_equation (Eeq (Evarpat n, e))) :: eq_list in
(d_list, eq_list), Evar n
@ -172,9 +179,9 @@ and translate_list kind context e_list =
and fby kind context e v e1 =
let mk_fby c e =
mk_exp ~loc:e.e_loc (Epre(Some c, e)) e.e_ty in
mk_exp ~loc:e.e_loc (Epre(Some c, e)) e.e_ty ~linearity:Ltop in
let mk_pre e =
mk_exp ~loc:e.e_loc (Epre(None, e)) e.e_ty in
mk_exp ~loc:e.e_loc (Epre(None, e)) e.e_ty ~linearity:Ltop in
let context, e1 = translate ExtValue context e1 in
match e1.e_desc, v with
| Eapp({ a_op = Etuple } as app, e_list, r),
@ -207,7 +214,7 @@ and ifthenelse context e e1 e2 e3 =
let mk_ite_list e2_list e3_list =
let mk_ite e'2 e'3 =
mk_exp ~loc:e.e_loc
(Eapp (mk_app Eifthenelse, [e1; e'2; e'3], None)) e'2.e_ty
(Eapp (mk_app Eifthenelse, [e1; e'2; e'3], None)) e'2.e_ty ~linearity:e'2.e_linearity
in
let e_list = List.map2 mk_ite e2_list e3_list in
{ e with e_desc = Eapp(mk_app Etuple, e_list, None) }
@ -228,6 +235,7 @@ and merge context e x c_e_list =
in
let rec mk_merge x c_list e_lists =
let ty = (List.hd (List.hd e_lists)).e_ty in
let lin = (List.hd (List.hd e_lists)).e_linearity in
let rec build_c_e_list c_list e_lists =
match c_list, e_lists with
| [], [] -> [], []
@ -241,7 +249,7 @@ and merge context e x c_e_list =
| []::_ -> []
| _ ::_ ->
let c_e_list, e_lists = build_c_e_list c_list e_lists in
let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty in
let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty ~linearity:lin in
let e_merge_list = build_merge_list c_list e_lists in
e_merge::e_merge_list in
build_merge_list c_list e_lists
@ -254,8 +262,8 @@ and merge context e x c_e_list =
let c_list = List.map (fun (t,_) -> t) c_e_list in
let e_lists = List.map (fun (_,e) -> e_to_e_list e) c_e_list in
let e_lists, context =
mapfold
(fun context e_list -> add_list context ExtValue e_list)
mapfold
(fun context e_list -> add_list context ExtValue e_list)
context e_lists in
let e_list = mk_merge x c_list e_lists in
context, { e with
@ -314,7 +322,7 @@ let block funs _ b =
let contract funs context c =
let ({ c_block = b } as c), void_context =
Hept_mapfold.contract funs context c in
Hept_mapfold.contract funs context c in
(* Non-void context could mean lost equations *)
assert (void_context=([],[]));
let context, e_a = translate ExtValue ([],[]) c.c_assume in

9
compiler/heptagon/transformations/reset.ml
View file

@ -27,7 +27,9 @@ let fresh = Idents.gen_fresh "reset" ~reset:true (fun () -> "r")
(* get e and return r, var_dec_r, r = e *)
let reset_var_from_exp e =
let r = fresh() in
{ e with e_desc = Evar r }, mk_var_dec r (Tid Initial.pbool), mk_equation (Eeq(Evarpat r, e))
{ e with e_desc = Evar r },
mk_var_dec r (Tid Initial.pbool) ~linearity:Linearity.Ltop,
mk_equation (Eeq(Evarpat r, e))
(** Merge two reset conditions *)
let merge_resets res1 res2 =
@ -40,7 +42,10 @@ let merge_resets res1 res2 =
(** if res then e2 else e3 *)
let ifres res e2 e3 =
let init loc = mk_exp (Epre (Some (mk_static_bool true), dfalse)) ~loc:loc (Tid Initial.pbool) in
let init loc =
mk_exp (Epre (Some (mk_static_bool true), dfalse))
~loc:loc (Tid Initial.pbool) ~linearity:Linearity.Ltop
in
match res with
| None -> mk_op_app Eifthenelse [init e3.e_loc; e2; e3]
| Some re -> mk_op_app Eifthenelse [re; e2; e3]

14
compiler/heptagon/transformations/switch.ml
View file

@ -132,7 +132,7 @@ let level_up defnames constr h =
let add_to_locals vd_env locals h =
let add_one n nn (locals,vd_env) =
let orig_vd = Idents.Env.find n vd_env in
let vd_nn = mk_var_dec ~linearity:orig_vd.v_linearity nn orig_vd.v_type in
let vd_nn = mk_var_dec nn orig_vd.v_type orig_vd.v_linearity in
vd_nn::locals, Idents.Env.add vd_nn.v_ident vd_nn vd_env
in
fold add_one h (locals, vd_env)
@ -177,7 +177,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
(* create a clock var corresponding to the switch condition [e] *)
let ck = fresh_clock_id () in
let e, (vd_env,env,h) = exp_it funs (vd_env,env,h) e in
let locals = [mk_var_dec ck e.e_ty] in
let locals = [mk_var_dec ck e.e_ty e.e_linearity] in
let equs = [mk_equation (Eeq (Evarpat ck, e))] in
(* typing have proved that defined variables are the same among states *)
@ -203,14 +203,16 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
in
(* create a merge equation for each defnames *)
let new_merge n ty equs =
let c_h_to_c_e (constr,h) = constr, mk_exp (Evar(Rename.rename n h)) ty in
let new_merge n vd equs =
let c_h_to_c_e (constr,h) =
constr, mk_exp (Evar(Rename.rename n h)) vd.v_type ~linearity:vd.v_linearity
in
let c_e_l = List.map c_h_to_c_e c_h_l in
let merge = mk_exp (Emerge (ck, c_e_l)) ty in
let merge = mk_exp (Emerge (ck, c_e_l)) vd.v_type ~linearity:vd.v_linearity in
(mk_equation (Eeq (Evarpat (Rename.rename n h), merge))) :: equs
in
let equs =
Idents.Env.fold (fun n ty equs -> new_merge n ty equs) defnames equs
Idents.Env.fold (fun n vd equs -> new_merge n vd equs) defnames equs
in
(* return the transformation in a block *)

13
compiler/main/hept2mls.ml
View file

@ -45,19 +45,12 @@ struct
end
let fresh = Idents.gen_fresh "hept2mls"
(function Heptagon.Enode f -> (shortname f)
| _ -> "n")
(* add an equation *)
let equation locals eqs e =
let n = Idents.gen_var "hept2mls" "ck" in
n,
(mk_var_dec n e.e_ty) :: locals,
(mk_equation (Evarpat n) e):: eqs
(function Heptagon.Enode f -> (shortname f)
| _ -> "n")
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty; Heptagon.v_linearity = linearity;
Heptagon.v_loc = loc; Heptagon.v_clock = ck } =
mk_var_dec ~loc:loc ~linearity:linearity n ty ck
mk_var_dec ~loc:loc n ty linearity ck
let translate_reset = function
| Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n

4
compiler/minils/analysis/clocking.ml
View file

@ -154,7 +154,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
typing_app h base_ck pat op (pargs@args)
| Imapi -> (* clocking the node with the extra i input on [ck_r] *)
let il (* stubs i as 0 *) =
List.map (fun x -> mk_extvalue ~ty:Initial.tint
List.map (fun x -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl
in
typing_app h base_ck pat op (pargs@args@il)
@ -165,7 +165,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
ct
| Ifoldi -> (* clocking the node with the extra i and last in/out constraints *)
let il (* stubs i as 0 *) =
List.map (fun x -> mk_extvalue ~ty:Initial.tint
List.map (fun x -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl
in
let rec insert_i args = match args with

4
compiler/minils/analysis/interference.ml
View file

@ -471,10 +471,10 @@ let process_eq ({ eq_lhs = pat; eq_rhs = e } as eq) =
let add_init_return_eq f =
(** a_1,..,a_p = __init__ *)
let eq_init = mk_equation (Mls_utils.pat_from_dec_list f.n_input)
(mk_extvalue_exp Cbase Initial.tint (Wconst (Initial.mk_static_int 0))) in
(mk_extvalue_exp Cbase Initial.tint Ltop (Wconst (Initial.mk_static_int 0))) in
(** __return__ = o_1,..,o_q *)
let eq_return = mk_equation (Etuplepat [])
(mk_exp Cbase Tinvalid (Mls_utils.tuple_from_dec_list f.n_output)) in
(mk_exp Cbase Tinvalid Ltop (Mls_utils.tuple_from_dec_list f.n_output)) in
(eq_init::f.n_equs)@[eq_return]

12
compiler/minils/minils.ml
View file

@ -178,21 +178,21 @@ and interface_desc =
(*Helper functions to build the AST*)
let mk_extvalue ~ty ?(linearity = Ltop) ?(clock = fresh_clock()) ?(loc = no_location) desc =
let mk_extvalue ~ty ~linearity ?(clock = fresh_clock()) ?(loc = no_location) desc =
{ w_desc = desc; w_ty = ty; w_linearity = linearity;
w_ck = clock; w_loc = loc }
let mk_exp level_ck ty ?(linearity = Ltop) ?(ck = Cbase)
let mk_exp level_ck ty ~linearity ?(ck = Cbase)
?(ct = fresh_ct ty) ?(loc = no_location) desc =
{ e_desc = desc; e_ty = ty; e_linearity = linearity;
e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc }
let mk_var_dec ?(loc = no_location) ?(linearity = Ltop) ident ty ck =
let mk_var_dec ?(loc = no_location) ident ty linearity ck =
{ v_ident = ident; v_type = ty; v_linearity = linearity; v_clock = ck; v_loc = loc }
let mk_extvalue_exp ?(linearity = Ltop) ?(clock = fresh_clock())
?(loc = no_location) level_ck ty desc =
mk_exp ~ck:clock ~loc:loc level_ck ty
let mk_extvalue_exp ?(clock = fresh_clock())
?(loc = no_location) level_ck ty ~linearity desc =
mk_exp ~ck:clock ~loc:loc level_ck ty ~linearity:linearity
(Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc))
let mk_equation ?(loc = no_location) pat exp =

2
compiler/minils/mls_utils.ml
View file

@ -63,7 +63,7 @@ let pat_from_dec_list decs =
let tuple_from_dec_list decs =
let aux vd =
mk_extvalue ~clock:vd.v_clock ~ty:vd.v_type (Wvar vd.v_ident)
mk_extvalue ~clock:vd.v_clock ~ty:vd.v_type ~linearity:vd.v_linearity (Wvar vd.v_ident)
in
Eapp(mk_app Earray, List.map aux decs, None)

8
compiler/minils/transformations/normalize_mem.ml
View file

@ -22,9 +22,13 @@ let eq _ (outputs, eqs, env) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with
| Evarpat x, Efby _ ->
if Mls_utils.vd_mem x outputs then
let ty = eq.eq_rhs.e_ty in
let lin = eq.eq_rhs.e_linearity in
let ck = eq.eq_rhs.e_base_ck in
let x_copy = Idents.gen_var "normalize_mem" ("out_"^(Idents.name x)) in
let exp_x = mk_exp ck ~ck:ck ~ct:(Clocks.Ck ck) ty (Eextvalue (mk_extvalue ~clock:ck ~ty:ty (Wvar x))) in
let exp_x =
mk_exp ck ~ck:ck ~ct:(Clocks.Ck ck) ty ~linearity:lin
(Eextvalue (mk_extvalue ~clock:ck ~ty:ty ~linearity:lin (Wvar x)))
in
let eq_copy = { eq with eq_lhs = Evarpat x_copy; eq_rhs = exp_x } in
let env = Env.add x x_copy env in
eq, (outputs, eq::eq_copy::eqs, env)
@ -49,7 +53,7 @@ let node funs acc nd =
{ nd with n_local = v; n_equs = List.rev eqs; n_output = o }, acc
let program p =
let funs = { Mls_mapfold.defaults with
let funs = { Mls_mapfold.defaults with
eq = eq; node_dec = node; contract = contract } in
let p, _ = Mls_mapfold.program_it funs ([], [], Env.empty) p in
p

30
compiler/minils/transformations/tomato.ml
View file

@ -184,8 +184,10 @@ let rec add_equation is_input (tenv : tom_env) eq =
let class_id_list = match rst with
| None -> class_id_list
| Some rst ->
class_ref_of_var is_input (mk_extvalue ~ty:Initial.tbool (Wvar rst)) rst
:: class_id_list in
class_ref_of_var is_input
(mk_extvalue ~ty:Initial.tbool ~linearity:Linearity.Ltop (Wvar rst)) rst
:: class_id_list
in
Eapp (app, w_list, optional (fun _ -> dummy_var) rst), id, 0, class_id_list
| Efby (seo, w) ->
@ -195,13 +197,18 @@ let rec add_equation is_input (tenv : tom_env) eq =
| Ewhen (e', cn, x) ->
let ed, add_when, when_count, class_id_list = decompose e' in
ed, (fun e' -> { e with e_desc = Ewhen (add_when e', cn, x) }), when_count + 1,
class_ref_of_var is_input (mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool (Wvar x)) x
class_ref_of_var is_input
(mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool
~linearity:Linearity.Ltop (Wvar x)) x
:: class_id_list
| Emerge (x, clause_list) ->
let class_id_list, clause_list = mapfold_right add_clause clause_list [] in
let x_id =
class_ref_of_var is_input (mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool (Wvar x)) x in
class_ref_of_var is_input
(mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool
~linearity:Linearity.Ltop (Wvar x)) x
in
Emerge (dummy_var, clause_list), id, 0, x_id :: class_id_list
| Eiterator (it, app, sel, partial_w_list, w_list, rst) ->
@ -210,8 +217,10 @@ let rec add_equation is_input (tenv : tom_env) eq =
let class_id_list = match rst with
| None -> class_id_list
| Some rst ->
class_ref_of_var is_input (mk_extvalue ~ty:Initial.tbool (Wvar rst)) rst
:: class_id_list in
class_ref_of_var is_input
(mk_extvalue ~ty:Initial.tbool ~linearity:Linearity.Ltop (Wvar rst)) rst
:: class_id_list
in
Eiterator (it, app, sel, partial_w_list, w_list, optional (fun _ -> dummy_var) rst),
id, 0, class_id_list
@ -246,7 +255,7 @@ and extvalue is_input w class_id_list =
class_id_list, Wfield (w, f)
| Wwhen (w, cn, x) ->
(* Create the extvalue representing x *)
let w_x = mk_extvalue ~ty:Initial.tbool ~clock:w.w_ck (Wvar x) in
let w_x = mk_extvalue ~ty:Initial.tbool ~clock:w.w_ck ~linearity:w.w_linearity (Wvar x) in
let class_id_list, w = decompose w (class_ref_of_var is_input w_x x :: class_id_list) in
class_id_list, Wwhen (w, cn, dummy_var)
in
@ -419,7 +428,7 @@ and reconstruct_class_ref mapping cr = match cr with
| Cr_input w -> w
| Cr_plain x ->
let Info (x', ty, ck, _) = Env.find x mapping in
mk_extvalue ~clock:ck ~ty:ty (Wvar x')
mk_extvalue ~clock:ck ~ty:ty ~linearity:Linearity.Ltop (Wvar x')
and reconstruct_clock mapping ck = match ck_repr ck with
| Con (ck, c, x) -> Con (reconstruct_clock mapping ck, c, new_name mapping x)
@ -537,10 +546,11 @@ let rec fix_output_var_dec mapping vd (seen, equs, vd_list) =
let new_clock = reconstruct_clock mapping vd.v_clock in
let new_vd = { vd with v_ident = new_id; v_clock = new_clock } in
let new_eq =
let w = mk_extvalue ~ty:vd.v_type ~clock:new_clock (Wvar x) in
let w = mk_extvalue ~ty:vd.v_type ~clock:new_clock ~linearity:Linearity.Ltop (Wvar x) in
mk_equation
(Evarpat new_id)
(mk_exp new_clock vd.v_type ~ct:(Ck new_clock) ~ck:new_clock (Eextvalue w))
(mk_exp new_clock vd.v_type ~ct:(Ck new_clock)
~ck:new_clock ~linearity:Linearity.Ltop (Eextvalue w))
in
(seen, new_eq :: equs, new_vd :: vd_list)
else

25
test/good/linear_automata.ept
View file

@ -10,7 +10,7 @@ let
o = [ a with [n-1] = 0 ]
tel
node autom(a:int^n at r) returns (o:int^n at r)
node autom(a:int^n at r) returns (o:int^n at r; u:int)
let
automaton
state S1
@ -22,5 +22,24 @@ let
do
o = g(a)
until false then S1
end
tel
end;
u = a[0]
tel
node autom_last() returns (u:int)
var a:int^n at r; last o : int^n at r;
let
init<<r>> a = 1^n;
automaton
state S1
do
until true then S2
state S2
do
o = g(a)
until false then S1
end;
u = a[0]
tel