From d8dffe15d823d8cf020af04d4dd6110540e15e7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Mon, 13 Sep 2010 16:02:33 +0200 Subject: [PATCH] Fixed remainings non exhaustive patterns Now the only shown warnings are the X type that we don't care about --- compiler/global/static.ml | 2 +- compiler/heptagon/analysis/causality.ml | 22 ++++--- compiler/heptagon/analysis/typing.ml | 68 +++++++++----------- compiler/heptagon/hept_printer.ml | 48 +++++++++----- compiler/minils/analysis/clocking.ml | 32 +++++---- compiler/minils/transformations/normalize.ml | 34 ++++++---- compiler/obc/c/cgen.ml | 2 +- compiler/utilities/misc.ml | 4 ++ compiler/utilities/misc.mli | 1 + 9 files changed, 125 insertions(+), 88 deletions(-) diff --git a/compiler/global/static.ml b/compiler/global/static.ml index 024900d..6886e72 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -55,7 +55,7 @@ let apply_op op se_list = | _ -> se let eval_core eval apply_op env se = match se.se_desc with - | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> se + | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ | Sfield _ -> se | Svar ln -> ( try (* first try to find in global const env *) let cd = find_const ln in diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 708d610..f4f14dc 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -111,27 +111,33 @@ let rec typing e = (** Typing an application *) and apply op e_list = - match op, e_list with - | Earrow, [e1;e2] -> + match op with + | Earrow -> + let e1, e2 = assert_2 e_list in let t1 = typing e1 in let t2 = typing e2 in candlist [t1; t2] - | Efield, [e1] -> typing e1 - | Eifthenelse, [e1; e2; e3] -> + | Efield -> + let e1 = assert_1 e_list in + typing e1 + | Eifthenelse -> + let e1, e2, e3 = assert_3 e_list in let t1 = typing e1 in let i2 = typing e2 in let i3 = typing e3 in cseq t1 (cor i2 i3) | (Eequal | Efun _| Enode _ | Econcat | Eselect_slice - | Eselect_dyn| Eselect _ | Earray_fill), e_list -> + | Eselect_dyn| Eselect _ | Earray_fill) -> ctuplelist (List.map typing e_list) - | (Earray | Etuple), e_list -> + | (Earray | Etuple) -> candlist (List.map typing e_list) - | Efield_update, [e1;e2] -> + | Efield_update -> + let e1, e2 = assert_2 e_list in let t1 = typing e1 in let t2 = typing e2 in cseq t2 t1 - | Eupdate , e1::e_list -> + | Eupdate -> + let e1, e_list = assert_1min e_list in let t1 = typing e1 in let t2 = ctuplelist (List.map typing e_list) in cseq t2 t1 diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 4d97782..2d39fa6 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -596,25 +596,28 @@ and expect const_env h expected_ty e = with TypingError(kind) -> message e.e_loc kind and typing_app const_env h op e_list = - match op, e_list with - | { a_op = Eequal }, [e1;e2] -> + match op with + | { a_op = Eequal } -> + let e1, e2 = assert_2 e_list in let typed_e1, t1 = typing const_env h e1 in let typed_e2 = expect const_env h t1 e2 in Tid Initial.pbool, op, [typed_e1; typed_e2] - | { a_op = Earrow }, [e1;e2] -> + | { a_op = Earrow } -> + let e1, e2 = assert_2 e_list in let typed_e1, t1 = typing const_env h e1 in let typed_e2 = expect const_env h t1 e2 in t1, op, [typed_e1;typed_e2] - | { a_op = Eifthenelse }, [e1;e2;e3] -> + | { a_op = Eifthenelse }-> + let e1, e2, e3 = assert_3 e_list in let typed_e1 = expect const_env h (Tid Initial.pbool) e1 in let typed_e2, t1 = typing const_env h e2 in let typed_e3 = expect const_env h t1 e3 in t1, op, [typed_e1; typed_e2; typed_e3] - | { a_op = (Efun f | Enode f); a_params = params } as app, e_list -> + | { a_op = (Efun f | Enode f); a_params = params } as app -> let ty_desc = find_value f in let op, expected_ty_list, result_ty_list = kind f ty_desc in (*TODO verifier....*) @@ -635,18 +638,21 @@ and typing_app const_env h op e_list = { app with a_op = op; a_params = typed_params }, typed_e_list - | { a_op = Etuple }, e_list -> + | { a_op = Etuple } -> let typed_e_list,ty_list = List.split (List.map (typing const_env h) e_list) in prod ty_list, op, typed_e_list - | { a_op = Earray }, exp::e_list -> + | { a_op = Earray } -> + let exp, e_list = assert_1min e_list in let typed_exp, t1 = typing const_env h exp in let typed_e_list = List.map (expect const_env h t1) e_list in let n = mk_static_int (List.length e_list + 1) in Tarray(t1, n), op, typed_exp::typed_e_list - | { a_op = Efield; a_params = [f] }, [e] -> + | { a_op = Efield; a_params = params } -> + let e = assert_1 e_list in + let f = assert_1 params in let fn = (match f.se_desc with | Sfield fn -> fn @@ -656,7 +662,9 @@ and typing_app const_env h op e_list = let t2 = field_type const_env fn fields t1 e.e_loc in t2, op, [typed_e] - | { a_op = Efield_update; a_params = [f] }, [e1; e2] -> + | { a_op = Efield_update; a_params = params } -> + let e1, e2 = assert_2 e_list in + let f = assert_1 params in let typed_e1, t1 = typing const_env h e1 in let q, fields = struct_info t1 in let fn = @@ -667,33 +675,40 @@ and typing_app const_env h op e_list = let typed_e2 = expect const_env h t2 e2 in t1, op, [typed_e1; typed_e2] - | { a_op = Earray_fill; a_params = [n] }, [e1] -> + | { a_op = Earray_fill; a_params = params } -> + let n = assert_1 params in + let e1 = assert_1 e_list in let typed_n = expect_static_exp const_env (Tid Initial.pint) n in let typed_e1, t1 = typing const_env h e1 in add_size_constraint (Clequal (mk_static_int 1, typed_n)); Tarray (t1, typed_n), { op with a_params = [typed_n] }, [typed_e1] - | { a_op = Eselect; a_params = idx_list }, [e1] -> + | { a_op = Eselect; a_params = idx_list } -> + let e1 = assert_1 e_list in let typed_e1, t1 = typing const_env h e1 in let typed_idx_list, ty = typing_array_subscript const_env h idx_list t1 in ty, { op with a_params = typed_idx_list }, [typed_e1] - | { a_op = Eselect_dyn }, e1::defe::idx_list -> + | { a_op = Eselect_dyn } -> + let e1, defe, idx_list = assert_2min e_list in let typed_e1, t1 = typing const_env h e1 in let typed_defe = expect const_env h (element_type t1) defe in let ty, typed_idx_list = typing_array_subscript_dyn const_env h idx_list t1 in ty, op, typed_e1::typed_defe::typed_idx_list - | { a_op = Eupdate }, e1::e2::idx_list -> + | { a_op = Eupdate } -> + let e1, e2, idx_list = assert_2min e_list in let typed_e1, t1 = typing const_env h e1 in let ty, typed_idx_list = typing_array_subscript_dyn const_env h idx_list t1 in let typed_e2 = expect const_env h ty e2 in t1, op, typed_e1::typed_e2::typed_idx_list - | { a_op = Eselect_slice; a_params = [idx1; idx2] }, [e] -> + | { a_op = Eselect_slice; a_params = params } -> + let e = assert_1 e_list in + let idx1, idx2 = assert_2 params in let typed_idx1 = expect_static_exp const_env (Tid Initial.pint) idx1 in let typed_idx2 = expect_static_exp const_env (Tid Initial.pint) idx2 in let typed_e, t1 = typing const_env h e in @@ -706,7 +721,8 @@ and typing_app const_env h op e_list = Tarray (element_type t1, e2), { op with a_params = [typed_idx1; typed_idx2] }, [typed_e] - | { a_op = Econcat }, [e1; e2] -> + | { a_op = Econcat } -> + let e1, e2 = assert_2 e_list in let typed_e1, t1 = typing const_env h e1 in let typed_e2, t2 = typing const_env h e2 in begin try @@ -718,28 +734,6 @@ and typing_app const_env h op e_list = mk_static_int_op (mk_pervasives "+") [array_size t1; array_size t2] in Tarray (element_type t1, n), op, [typed_e1; typed_e2] - (*Arity problems*) - | { a_op = Earrow }, _ -> - error (Earity_clash(List.length e_list, 2)) - | { a_op = Eifthenelse }, _ -> - error (Earity_clash(List.length e_list, 2)) - | { a_op = Efield_update }, _ -> - error (Earity_clash(List.length e_list, 2)) - | { a_op = Earray }, [] -> - error (Earity_clash (0, 1)) - | { a_op = Econcat }, _ -> - error (Earity_clash(List.length e_list, 2)) - | { a_op = Eselect_slice }, _ -> - error (Earity_clash(List.length e_list, 3)) - | { a_op = Eupdate }, _ -> - error (Earity_clash(List.length e_list, 2)) - | { a_op = Eselect }, _ -> - error (Earity_clash(List.length e_list, 1)) - | { a_op = Eselect_dyn }, _ -> - error (Earity_clash(List.length e_list, 2)) - | { a_op = Earray_fill }, _ -> - error (Earity_clash(List.length e_list, 2)) - and typing_iterator const_env h it n args_ty_list result_ty_list e_list = match it with | Imap -> diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index e5e8096..0d145bb 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -103,26 +103,34 @@ and print_call_params ff = function | l -> print_list_r print_static_exp "<<" "," ">>" ff l and print_op ff op params e_list = - match op, params, e_list with - | Eequal, _, [e1; e2] -> + match op with + | Eequal -> + let e1, e2 = assert_2 e_list in fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2 - | Earrow, _, [e1;e2] -> print_exp ff e1; fprintf ff " -> "; print_exp ff e2 - | Eifthenelse, _, [e1;e2;e3] -> + | Earrow -> + let e1, e2 = assert_2 e_list in + print_exp ff e1; fprintf ff " -> "; print_exp ff e2 + | Eifthenelse -> + let e1, e2, e3 = assert_3 e_list in fprintf ff "@["; fprintf ff "if "; print_exp ff e1; fprintf ff "@ then@ "; print_exp ff e2; fprintf ff "@ else@ "; print_exp ff e3; fprintf ff "@]" - | Etuple, _, e_list -> print_exps ff e_list - | Earray, _, e_list -> + | Etuple -> print_exps ff e_list + | Earray -> print_list_r print_exp "[" "," "]" ff e_list - | (Efun f|Enode f), params, e_list -> + | (Efun f|Enode f) -> print_qualname ff f; print_call_params ff params; print_exps ff e_list - | Efield, [field], [e] -> + | Efield -> + let e = assert_1 e_list in + let field = assert_1 params in print_exp ff e; fprintf ff "."; print_static_exp ff field - | Efield_update, [se], [e1;e2] -> + | Efield_update -> + let e1, e2 = assert_2 e_list in + let se = assert_1 params in fprintf ff "(@["; print_exp ff e1; fprintf ff " with ."; @@ -130,20 +138,25 @@ and print_op ff op params e_list = fprintf ff " = "; print_exp ff e2; fprintf ff ")@]" - | Earray_fill, [se], [e] -> + | Earray_fill -> + let e = assert_1 e_list in + let se = assert_1 params in print_exp ff e; fprintf ff "^"; print_static_exp ff se - | Eselect, idx_list, [e] -> + | Eselect -> + let e = assert_1 e_list in print_exp ff e; - print_list_r print_static_exp "[" "][" "]" ff idx_list - | Eselect_dyn, _, e::defe::idx_list -> + print_list_r print_static_exp "[" "][" "]" ff params + | Eselect_dyn -> + let e, defe, idx_list = assert_2min e_list in fprintf ff "@[("; print_exp ff e; print_list_r print_exp "[" "][" "] default " ff idx_list; print_exp ff defe; fprintf ff ")@]" - | Eupdate, _, e1::e2::idx_list -> + | Eupdate -> + let e1, e2, idx_list = assert_2min e_list in fprintf ff "(@["; print_exp ff e1; fprintf ff " with "; @@ -151,14 +164,17 @@ and print_op ff op params e_list = fprintf ff " = "; print_exp ff e2; fprintf ff ")@]" - | Eselect_slice, [idx1;idx2], [e] -> + | Eselect_slice -> + let e = assert_1 e_list in + let idx1, idx2 = assert_2 params in print_exp ff e; fprintf ff "["; print_static_exp ff idx1; fprintf ff ".."; print_static_exp ff idx2; fprintf ff "]" - | Econcat, _, [e1;e2] -> + | Econcat -> + let e1, e2 = assert_2 e_list in fprintf ff "@["; print_exp ff e1; fprintf ff " @@ "; diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index e98c476..a6ecfc5 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -61,31 +61,37 @@ let rec typing h e = Ck ck) in (e.e_ck <- ckofct ct; ct) -and typing_op op args h e ck = match op, args with - | (Eequal | Efun _ | Enode _), e_list -> +and typing_op op e_list h e ck = match op with + | (Eequal | Efun _ | Enode _) -> (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty) - | Etuple, e_list -> + | Etuple -> Cprod (List.map (typing h) e_list) - | Eifthenelse, [e1; e2; e3] -> + | Eifthenelse -> + let e1, e2, e3 = assert_3 e_list in let ct = skeleton ck e.e_ty in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct) - | Efield, [e1] -> + | Efield -> + let e1 = assert_1 e_list in let ct = skeleton ck e1.e_ty in (expect h (Ck ck) e1; ct) - | Efield_update, [e1; e2] -> + | Efield_update -> + let e1, e2 = assert_2 e_list in let ct = skeleton ck e.e_ty in (expect h (Ck ck) e1; expect h ct e2; ct) - | Earray, e_list -> + | Earray -> (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty) - | Earray_fill, [e] -> typing h e - | Eselect, [e] -> typing h e - | Eselect_dyn, e1::defe::idx -> (* TODO defe not treated ? *) + | Earray_fill -> let e = assert_1 e_list in typing h e + | Eselect -> let e = assert_1 e_list in typing h e + | Eselect_dyn -> (* TODO defe not treated ? *) + let e1, defe, idx = assert_2min e_list in let ct = skeleton ck e1.e_ty in (List.iter (expect h ct) (e1::defe::idx); ct) - | Eupdate, e1::e2::idx -> + | Eupdate -> + let e1, e2, idx = assert_2min e_list in let ct = skeleton ck e.e_ty in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct) - | Eselect_slice, [e] -> typing h e - | Econcat, [e1; e2] -> + | Eselect_slice -> let e = assert_1 e_list in typing h e + | Econcat -> + let e1, e2 = assert_2 e_list in let ct = skeleton ck e.e_ty in (expect h (Ck ck) e1; expect h ct e2; ct) diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index a903d14..f2ad8d1 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -225,47 +225,57 @@ let rec translate kind context e = in add context kind e and translate_app kind context op e_list = - match op, e_list with - | Eequal, e_list -> + match op with + | Eequal -> let context, e_list = translate_list function_args_kind context e_list in context, e_list - | Etuple, e_list -> + | Etuple -> let context, e_list = translate_list kind context e_list in context, e_list - | Efield, [e'] -> + | Efield -> + let e' = assert_1 e_list in let context, e' = translate Exp context e' in context, [e'] - | Efield_update, [e1; e2] -> + | Efield_update -> + let e1, e2 = assert_2 e_list in let context, e1 = translate VRef context e1 in let context, e2 = translate Exp context e2 in context, [e1; e2] - | Earray, e_list -> + | Earray -> let context, e_list = translate_list kind context e_list in context, e_list - | Earray_fill, [e] -> + | Earray_fill -> + let e = assert_1 e_list in let context, e = translate Exp context e in context, [e] - | Eselect, [e'] -> + | Eselect -> + let e' = assert_1 e_list in let context, e' = translate VRef context e' in context, [e'] - | Eselect_dyn, e1::e2::idx -> + | Eselect_dyn -> + let e1, e2, idx = assert_2min e_list in let context, e1 = translate VRef context e1 in let context, idx = translate_list Exp context idx in let context, e2 = translate Exp context e2 in context, e1::e2::idx - | Eupdate, e1::e2::idx -> + | Eupdate -> + let e1, e2, idx = assert_2min e_list in let context, e1 = translate VRef context e1 in let context, idx = translate_list Exp context idx in let context, e2 = translate Exp context e2 in context, e1::e2::idx - | Eselect_slice, [e'] -> + | Eselect_slice -> + let e' = assert_1 e_list in let context, e' = translate VRef context e' in context, [e'] - | Econcat, [e1; e2] -> + | Econcat -> + let e1, e2 = assert_2 e_list in let context, e1 = translate VRef context e1 in let context, e2 = translate VRef context e2 in context, [e1; e2] + | Enode _ | Efun _ | Eifthenelse _ -> + assert false (*already done in translate*) and translate_list kind context e_list = match e_list with diff --git a/compiler/obc/c/cgen.ml b/compiler/obc/c/cgen.ml index 2f18c24..4dff40e 100644 --- a/compiler/obc/c/cgen.ml +++ b/compiler/obc/c/cgen.ml @@ -231,6 +231,7 @@ let rec cexpr_of_static_exp se = | Sint i -> Cconst (Ccint i) | Sfloat f -> Cconst (Ccfloat f) | Sbool b -> Cconst (Ctag (if b then "TRUE" else "FALSE")) + | Sfield f -> assert false | Sconstructor c -> Cconst (Ctag (cname_of_qn c)) | Sarray sl -> Carraylit (List.map cexpr_of_static_exp sl) | Sarray_power(n,c) -> @@ -563,7 +564,6 @@ let mem_decl_of_class_def cd = convention we described above. *) let struct_field_of_obj_dec l od = if is_statefull od.o_class then - let clsname = cname_of_qn od.o_class in let ty = Cty_id (qn_append od.o_class "_mem") in let ty = match od.o_size with | Some se -> Cty_arr (int_of_static_exp se, ty) diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index c2e00e1..6460bd4 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -278,6 +278,10 @@ let assert_1 = function | [v] -> v | l -> _arity_error 1 l +let assert_1min = function + | v::l -> v, l + | l -> _arity_min_error 1 l + let assert_2 = function | [v1; v2] -> v1, v2 | l -> _arity_error 1 l diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index ab2c71c..b53fff1 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -191,6 +191,7 @@ val mapi3: (int -> 'a -> 'b -> 'c -> 'd) -> (** Functions to decompose a list into a tuple *) val assert_empty : 'a list -> unit val assert_1 : 'a list -> 'a +val assert_1min : 'a list -> 'a * 'a list val assert_2 : 'a list -> 'a * 'a val assert_2min : 'a list -> 'a * 'a * 'a list val assert_3 : 'a list -> 'a * 'a * 'a