Corrected Boolean pass

e_level_ck correctly translated
Hept_clocking on stateless functions
This commit is contained in:
Gwenal Delaval 2012-08-02 17:24:30 +02:00
parent a0af340825
commit 857dccd0b2
2 changed files with 8 additions and 2 deletions

View file

@ -38,6 +38,7 @@
*)
open Misc
open Names
open Idents
open Heptagon
open Hept_utils
@ -183,12 +184,15 @@ and expect h pat expected_ct e =
and typing_app h base pat op e_list = match op with
| Etuple (* to relax ? *)
| Earrow
| Efun _ (* stateless functions: inputs and outputs on the same clock *)
| Earray_fill | Eselect | Eselect_dyn | Eselect_trunc | Eupdate
| Eselect_slice | Econcat | Earray | Efield | Efield_update | Eifthenelse | Ereinit ->
List.iter (expect h pat (Ck base)) e_list;
Ck base
| Enode f ->
| Efun { qual = Module "Iostream"; name = "printf" }
| Efun { qual = Module "Iostream"; name = "fprintf" } ->
List.iter (expect h pat (Ck base)) e_list;
Cprod []
| (Efun f | Enode f) ->
let node = Modules.find_value f in
let pat_id_list = ident_list_of_pat pat in
let rec build_env a_l v_l env = match a_l, v_l with

View file

@ -638,6 +638,7 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
failwith("Boolean: not supported expression (abstract tree should be normalized)")
in
context,{ e with
e_level_ck = translate_ck env e.e_level_ck;
e_desc = desc;
e_ty = translate_ty ty;
e_ct_annot = ct}
@ -882,6 +883,7 @@ let node ({ n_input = inputs;
n_output = outputs;
n_contract = contract;
n_block = b } as n) =
Idents.enter_node n.n_name;
(* let inputs,in_loc,in_eq,env = buildenv_var_dec_list Env.empty inputs in *)
(* let outputs,out_loc,out_eq,env = buildenv_var_dec_list env outputs in *)
let contract, env = translate_contract Env.empty contract in