diff --git a/heptagon/analysis/initialization.ml b/heptagon/analysis/initialization.ml index fa57e8b..c07c230 100644 --- a/heptagon/analysis/initialization.ml +++ b/heptagon/analysis/initialization.ml @@ -208,7 +208,10 @@ let rec typing h e = (fun acc (_, e) -> max acc (itype (typing h e))) izero l in skeleton i e.e_ty | Earray(e_list) -> - product (List.map (typing h) e_list) + let i = + List.fold_left + (fun acc e -> max acc (itype (typing h e))) izero e_list in + skeleton i e.e_ty (** Typing an application *) and apply h op e_list = diff --git a/heptagon/analysis/typing.ml b/heptagon/analysis/typing.ml index 39bdb39..f5b59b2 100644 --- a/heptagon/analysis/typing.ml +++ b/heptagon/analysis/typing.ml @@ -207,13 +207,13 @@ let size_exp ty = let rec unify t1 t2 = match t1, t2 with + | b1, b2 when b1 = b2 -> () | Tprod t1_list, Tprod t2_list -> (try List.iter2 unify t1_list t2_list with _ -> raise Unify ) - | b1, b2 when b1 = b2 -> () | Tarray (ty1, e1), Tarray (ty2, e2) -> add_size_constr (Equal(e1,e2)); unify ty1 ty2 diff --git a/heptagon/main/heptcheck.ml b/heptagon/main/heptcheck.ml index 4a4b1d6..b380316 100644 --- a/heptagon/main/heptcheck.ml +++ b/heptagon/main/heptcheck.ml @@ -55,7 +55,7 @@ let compile_impl modname filename = if !verbose then begin - comment "Check successfull" + comment "Checking" end; close_all_files () diff --git a/heptagon/printer.ml b/heptagon/printer.ml index dac38cf..ed6c1a8 100644 --- a/heptagon/printer.ml +++ b/heptagon/printer.ml @@ -185,19 +185,19 @@ let rec print_eq ff eq = | Eautomaton(state_handler_list) -> fprintf ff "@[automaton@,"; fprintf ff "@["; - print_list print_state_handler ff state_handler_list; + print_list print_state_handler "" "" "" ff state_handler_list; fprintf ff "@]@,"; fprintf ff "end@]" | Eswitch(e, switch_handler_list) -> fprintf ff "@[switch "; print_exp ff e; fprintf ff "@,@["; - print_list print_switch_handler ff switch_handler_list; + print_list print_switch_handler "" "" "" ff switch_handler_list; fprintf ff "@]@,"; fprintf ff "end@]" | Epresent(present_handler_list, b) -> fprintf ff "@[present@,"; - print_list print_present_handler ff present_handler_list; + print_list print_present_handler "" "" "" ff present_handler_list; if b.b_equs <> [] then begin fprintf ff " @[default@,"; print_block ff b; @@ -226,7 +226,7 @@ and print_state_handler ff if until <> [] then begin fprintf ff "@,@[until "; - print_list print_escape ff until; + print_list print_escape "" "" "" ff until; fprintf ff "@]" end; if unless <> [] then