From 8c4217ab83182820ac5a160b356609a6ee64041e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Wed, 20 Apr 2011 11:42:03 +0200 Subject: [PATCH] Rebase bzr branch on old decade --- compiler/heptagon/parsing/hept_scoping.ml | 2 +- compiler/main/hept2mls.ml | 2 ++ compiler/main/mls2obc.ml | 4 +-- compiler/minils/minils.ml | 4 ++- compiler/minils/sigali/sigalimain.ml | 10 ++++---- compiler/minils/transformations/boolean.ml | 30 +++++++++++++--------- 6 files changed, 31 insertions(+), 21 deletions(-) diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 1f5b56c..d039d84 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -247,7 +247,7 @@ and translate_desc loc env = function | Eapp ({ a_op = op; a_params = params; a_inlined = inl }, e_list) -> let e_list = List.map (translate_exp env) e_list in let params = List.map (expect_static_exp) params in - let app = Heptagon.mk_op ~params:params ~inlined:inl (translate_op op) in + let app = Heptagon.mk_app ~params:params ~inlined:inl (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) -> diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 5b2ac21..5efddc0 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -191,12 +191,14 @@ let node n = n_input = List.map translate_var n.Heptagon.n_input; n_output = List.map translate_var n.Heptagon.n_output; n_contract = translate_contract n.Heptagon.n_contract; + n_controller_call = ([],[]); n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local; n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs; n_loc = n.Heptagon.n_loc ; n_params = n.Heptagon.n_params; n_params_constraints = n.Heptagon.n_params_constraints } + let typedec {Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} = let onetype = function diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 4afff64..85bad7d 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -463,8 +463,8 @@ and mk_node_call map call_context app loc name_list args ty = | Minils.Enode f | Minils.Efun f -> let id = begin match app.Minils.a_id with - None -> gen_obj_name f - | Some id -> name id + None -> gen_obj_ident f + | Some id -> id end in let o = mk_obj_call_from_context call_context id in let obj = diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index ac7bce2..e808f12 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -166,7 +166,8 @@ let mk_equation ?(loc = no_location) pat exp = { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) + ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[])) + ?(local = []) ?(eq = []) ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = []) name = { n_name = name; @@ -174,6 +175,7 @@ let mk_node n_input = input; n_output = output; n_contract = contract; + n_controller_call = pinst; n_local = local; n_equs = eq; n_loc = loc; diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 033dd55..9a5dcbd 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -22,8 +22,8 @@ open Sigali type mtype = Tint | Tbool | Tother let actual_ty = function - | Tid({ qual = "Pervasives"; name = "bool"}) -> Tbool - | Tid({ qual = "Pervasives"; name = "int"}) -> Tint + | Tid({ qual = Pervasives; name = "bool"}) -> Tbool + | Tid({ qual = Pervasives; name = "int"}) -> Tint | _ -> Tother let var_list prefix n = @@ -73,7 +73,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = end | Minils.Evar(n) -> Svar(prefix ^ (name n)) | Minils.Eapp (* pervasives binary or unary stateless operations *) - ({ Minils.a_op = Minils.Efun({qual="Pervasives";name=n})}, + ({ Minils.a_op = Minils.Efun({qual=Pervasives;name=n})}, e_list, _) -> begin match n, e_list with @@ -134,7 +134,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = end | Minils.Estruct(_) -> failwith("Sigali: structures not implemented") - | Minils.Eiterator(_,_,_,_,_) -> + | Minils.Eiterator(_,_,_,_,_,_) -> failwith("Sigali: iterators not implemented") | Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) -> failwith("Sigali: node in expressions; programs should be normalized") @@ -657,7 +657,7 @@ let program p = (NamesEnv.empty,[]) p.Minils.p_nodes in let procs = List.rev acc_proc in - let filename = filename_of_name p.Minils.p_modname in + let filename = filename_of_name (modul_to_string p.Minils.p_modname) in let dirname = build_path (filename ^ "_z3z") in let dir = clean_dir dirname in Sigali.Printer.print dir procs diff --git a/compiler/minils/transformations/boolean.ml b/compiler/minils/transformations/boolean.ml index 33506fc..aeaa830 100644 --- a/compiler/minils/transformations/boolean.ml +++ b/compiler/minils/transformations/boolean.ml @@ -51,7 +51,7 @@ open Minils let fresh = Idents.gen_fresh "bool" (fun s -> s) -let ty_bool = Tid({ qual = "Pervasives"; name = "bool"}) +let ty_bool = Tid({ qual = Pervasives; name = "bool"}) let strue = mk_static_exp ~ty:ty_bool (Sbool(true)) let sfalse = mk_static_exp ~ty:ty_bool (Sbool(false)) @@ -60,8 +60,8 @@ let sbool = function | true -> strue | false -> sfalse -let ctrue = { qual = "Pervasives"; name = "true" } -let cfalse = { qual = "Pervasives"; name = "false" } +let ctrue = { qual = Pervasives; name = "true" } +let cfalse = { qual = Pervasives; name = "false" } let mk_tuple e_l = Eapp((mk_app Etuple),e_l,None) @@ -224,7 +224,7 @@ let translate_pat env pat = let translate_ty ty = let rec trans ty = match ty with - | Tid({ qual = "Pervasives"; name = "bool" }) -> ty + | Tid({ qual = Pervasives; name = "bool" }) -> ty | Tid(name) -> begin try @@ -240,6 +240,7 @@ let translate_ty ty = end | Tprod(ty_list) -> Tprod(List.map trans ty_list) | Tarray(ty,se) -> Tarray(trans ty,se) + | Tmutable ty -> Tmutable(trans ty) | Tunit -> Tunit in trans ty @@ -271,7 +272,7 @@ let rec translate_ck env ck = let translate_const c ty e = match c.se_desc,ty with - | _, Tid({ qual = "Pervasives"; name = "bool" }) -> Econst(c) + | _, Tid({ qual = Pervasives; name = "bool" }) -> Econst(c) | Sconstructor(cname),Tid(tname) -> begin try @@ -352,11 +353,11 @@ let rec when_ck desc ty ck = let rec base_value ck ty = match ty with - | Tid({qual = "Pervasives"; name = "int" }) -> + | Tid({qual = Pervasives; name = "int" }) -> when_ck (Econst(mk_static_exp ~ty:ty (Sint(0)))) ty ck - | Tid({qual = "Pervasives"; name = "float"}) -> + | Tid({qual = Pervasives; name = "float"}) -> when_ck (Econst(mk_static_exp ~ty:ty (Sfloat(0.)))) ty ck - | Tid({qual = "Pervasives"; name = "bool" }) -> + | Tid({qual = Pervasives; name = "bool" }) -> when_ck (Econst(strue)) ty ck | Tid(sname) -> begin @@ -411,6 +412,9 @@ let rec base_value ck ty = e_ck = ck; e_loc = no_location; } + | Tmutable ty -> + let e = base_value ck ty in + e | Tunit -> { e_desc = Eapp (mk_app Etuple, [], None); e_ty = Tunit; @@ -530,9 +534,10 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ck = ck} as e) = (context,(c,e)::acc)) (context,[]) l in context,Estruct(List.rev acc) - | Eiterator(it,app,se,e_list,r) -> + | 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,e_list,r) + context,Eiterator(it,app,se,pe_list,e_list,r) in context,{ e with e_desc = desc; @@ -678,11 +683,12 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) = match ty with - | Tprod _ | Tarray _ | Tunit -> v::acc_vd, acc_loc, acc_eq, env + | Tprod _ | Tarray _ | Tmutable _ | Tunit -> + v::acc_vd, acc_loc, acc_eq, env | Tid(tname) -> begin match tname with - | { qual = "Pervasives"; name = ("bool" | "int" | "float") } -> + | { qual = Pervasives; name = ("bool" | "int" | "float") } -> v::acc_vd, acc_loc, acc_eq, env | _ -> begin