Refactoring and todo.txt update.
This commit is contained in:
Léonard Gérard
parent
14f3c57d6a
commit
f3584601f0
7 changed files with 28 additions and 44 deletions
|
|
@ -381,7 +381,7 @@ let rec check_type const_env = function
|
|||
| Tarray(ty, e) ->
|
||||
let typed_e = expect_static_exp const_env (Tid Initial.pint) e in
|
||||
Tarray(check_type const_env ty, typed_e)
|
||||
| Tid ty_name -> Tid ty_name
|
||||
| Tid ty_name -> Tid ty_name (* TODO bug ? should check that ty_name exists ? *)
|
||||
| Tprod l ->
|
||||
Tprod (List.map (check_type const_env) l)
|
||||
| Tunit -> Tunit
|
||||
|
|
|
|||
|
|
@ -85,26 +85,21 @@ let rec translate map e =
|
|||
let e = translate map e in
|
||||
e.e_desc
|
||||
| Minils.Estruct f_e_list ->
|
||||
let type_name =
|
||||
(match e.Minils.e_ty with
|
||||
| Tid name -> name
|
||||
| _ -> assert false) in
|
||||
let f_e_list =
|
||||
List.map
|
||||
(fun (f, e) -> (f, (translate map e)))
|
||||
f_e_list
|
||||
in Estruct (type_name, f_e_list)
|
||||
| Minils.Eapp ({ Minils.a_op = Minils.Efield;
|
||||
Minils.a_params = [{ se_desc = Sfield f }] },
|
||||
[e], _) ->
|
||||
let e = translate map e in
|
||||
let type_name = (match e.Minils.e_ty with
|
||||
| Tid name -> name
|
||||
| _ -> assert false) in
|
||||
let f_e_list = List.map (fun (f, e) -> (f, (translate map e))) f_e_list in
|
||||
Estruct (type_name, f_e_list)
|
||||
| Minils.Eapp ({ Minils.a_op = Minils.Efield; Minils.a_params = params }, e_list, _) ->
|
||||
let f = match (assert_1 params).se_desc with Sfield f -> f | _ -> assert false in
|
||||
let e = translate map (assert_1 e_list) in
|
||||
Elhs (mk_lhs (Lfield (lhs_of_exp e, f)))
|
||||
(*Array operators*)
|
||||
(*Remaining array operators*)
|
||||
| Minils.Eapp ({ Minils.a_op = Minils.Earray }, e_list, _) ->
|
||||
Earray (List.map (translate map ) e_list)
|
||||
| Minils.Eapp ({ Minils.a_op = Minils.Eselect;
|
||||
Minils.a_params = idx }, [e], _) ->
|
||||
let e = translate map e in
|
||||
Minils.a_params = idx }, e_list, _) ->
|
||||
let e = translate map (assert_1 e_list) in
|
||||
let idx_list = List.map (fun idx -> mk_exp (Econst idx)) idx in
|
||||
Elhs (lhs_of_idx_list (lhs_of_exp e) idx_list)
|
||||
| _ ->
|
||||
|
|
@ -221,8 +216,9 @@ and translate_act map pat
|
|||
| Minils.Evarpat n, _ ->
|
||||
[Aassgn (var_from_name map n, translate map act)]
|
||||
| _ ->
|
||||
(*let ff = Format.formatter_of_out_channel stdout in
|
||||
Mls_printer.print_exp ff act; Format.fprintf ff "@?";*) assert false
|
||||
Format.eprintf "%a The pattern %a should be a simple var to be translated to obc.@."
|
||||
Location.print_location act.Minils.e_loc Mls_printer.print_pat pat;
|
||||
assert false
|
||||
|
||||
and translate_c_act_list map pat c_act_list =
|
||||
List.map
|
||||
|
|
@ -250,13 +246,9 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
|
|||
let x = var_from_name map n in
|
||||
let si = (match opt_c with
|
||||
| None -> si
|
||||
| Some c ->
|
||||
(Aassgn (x,
|
||||
mk_exp (Econst c))) :: si) in
|
||||
let action = Aassgn (var_from_name map n,
|
||||
translate map e)
|
||||
in
|
||||
v, si, j, (control map ck action) :: s
|
||||
| Some c -> (Aassgn (x, mk_exp (Econst c))) :: si) in
|
||||
let action = Aassgn (var_from_name map n, translate map e) in
|
||||
v, si, j, (control map ck action) :: s
|
||||
|
||||
| Minils.Etuplepat p_list,
|
||||
Minils.Eapp({ Minils.a_op = Minils.Etuple }, act_list, _) ->
|
||||
|
|
|
|||
|
|
@ -32,13 +32,8 @@ let add_check prefix pass nd nd_list =
|
|||
let ty_r = match nd.n_output with
|
||||
| [out] -> out.v_type
|
||||
| _ -> Tprod (List.map (fun vd -> vd.v_type) nd.n_output) in
|
||||
let mk_call nn =
|
||||
mk_exp ~ty:ty_r
|
||||
(Eapp ({ a_op = Enode nn; a_params = []; a_unsafe = false; },
|
||||
[], None)) in
|
||||
mk_exp ~ty:(Tid Initial.pbool)
|
||||
(Eapp ({ a_op = Eequal; a_params = []; a_unsafe = false; },
|
||||
[mk_call nd.n_name; mk_call nd'.n_name], None)) in
|
||||
let mk_call nn = mk_exp ~ty:ty_r (Eapp (mk_app (Enode nn), [], None)) in
|
||||
mk_exp ~ty:(Tid Initial.pbool) (Eapp (mk_app Eequal, [mk_call nd.n_name; mk_call nd'.n_name], None)) in
|
||||
|
||||
let nd_check =
|
||||
mk_node
|
||||
|
|
|
|||
|
|
@ -146,9 +146,7 @@ let node nd =
|
|||
let eq =
|
||||
mk_equation pat
|
||||
{ eq.eq_rhs with e_desc =
|
||||
Eapp ({ a_op = Etuple;
|
||||
a_params = [];
|
||||
a_unsafe = unsafe; }, e_list, rst); } in
|
||||
Eapp (mk_app ~unsafe:unsafe Etuple, e_list, rst); } in
|
||||
(eq :: eq_list, subst) in
|
||||
List.fold_right add_to_subst nd.n_equs ([], Env.empty) in
|
||||
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* $Id$ *)
|
||||
|
||||
|
||||
open Signature
|
||||
open Modules
|
||||
|
|
|
|||
|
|
@ -77,6 +77,9 @@ let print_method_name ff = function
|
|||
| Mmethod n -> fprintf ff "%s" n
|
||||
|
||||
let rec print_act ff a =
|
||||
let print_lhs_tuple ff var_list = match var_list with
|
||||
| [] -> ()
|
||||
| _ -> fprintf ff "@[(%a)@] =@ " (print_list print_lhs "" "," "") var_list in
|
||||
match a with
|
||||
| Aassgn (x, e) -> print_asgn ff "" x e
|
||||
| Acase(e, tag_act_list) ->
|
||||
|
|
@ -91,12 +94,6 @@ let rec print_act ff a =
|
|||
print_static_exp i2
|
||||
print_block act_list
|
||||
| Acall (var_list, o, meth, es) ->
|
||||
let print_lhs_tuple ff var_list = match var_list with
|
||||
| [] -> ()
|
||||
| _ ->
|
||||
fprintf ff "@[(%a)@] =@ "
|
||||
(print_list print_lhs "" "," "") var_list in
|
||||
|
||||
fprintf ff "@[<2>%a%a.%a(%a)@]"
|
||||
print_lhs_tuple var_list
|
||||
print_obj_call o
|
||||
|
|
|
|||
4
todo.txt
4
todo.txt
|
|
@ -1,7 +1,9 @@
|
|||
|
||||
Plus ou moins ordonné du plus urgent au moins urgent.
|
||||
|
||||
*- (LG) Faire la passe de transformation des switchs dans heptagon avant le reset et ainsi simplifier le reset.
|
||||
*- Optimisations du genre "if true then ... else ... " ou genre "x,y = if b then a,c else a2,c" qui devrait etre transformé en "x = if b then a else s2; y = c" ...
|
||||
|
||||
*- Optimisation de la traduction des automates : pas besoin de variables de reset pour les états "continue", etc.
|
||||
|
||||
*- (LG) Rajouter les annotations d'horloge dans le source (les mettres comme contrainte de sous typage en ck_base ?? voir avec lucy-n)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue