Added v_loc in Minils too

This commit is contained in:
Cédric Pasteur 2010-07-15 10:02:42 +02:00
parent 46a09cf369
commit 4f9d6b2d82
3 changed files with 9 additions and 7 deletions

View file

@ -113,8 +113,9 @@ let add_locals ni l_eqs s_eqs s_handlers =
s_eqs s_handlers in
addrec l_eqs s_eqs s_handlers
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty; } =
mk_var_dec n ty
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty;
Heptagon.v_loc = loc } =
mk_var_dec ~loc:loc n ty
let translate_locals locals l =
List.fold_left (fun locals v -> translate_var v :: locals) locals l

View file

@ -343,8 +343,8 @@ let obj_decl l =
o_size = i; o_loc = Location.no_location (*TODO*) }) l
let translate_var_dec map l =
let one_var { Minils.v_ident = x; Minils.v_type = t } =
mk_var_dec x t
let one_var { Minils.v_ident = x; Minils.v_type = t; v_loc = loc } =
mk_var_dec ~loc:loc x t
in
List.map one_var l

View file

@ -101,7 +101,8 @@ type eq = {
type var_dec = {
v_ident : var_ident;
v_type : ty;
v_clock : ck }
v_clock : ck;
v_loc : location }
type contract = {
c_assume : exp;
@ -140,8 +141,8 @@ type program = {
let mk_exp ?(exp_ty = Tprod []) ?(clock = Cbase) ?(loc = no_location) desc =
{ e_desc = desc; e_ty = exp_ty; e_ck = clock; e_loc = loc }
let mk_var_dec ?(clock = Cbase) ident ty =
{ v_ident = ident; v_type = ty; v_clock = clock }
let mk_var_dec ?(loc = no_location) ?(clock = Cbase) ident ty =
{ v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc }
let mk_equation ?(loc = no_location) pat exp =
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }