jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Fixed remainings non exhaustive patterns

Browse source 
Now the only shown warnings are the X type that 
we don't care about
This commit is contained in:
Cédric Pasteur 2010-09-13 16:02:33 +02:00
parent 5aa83246ca
commit d8dffe15d8
9 changed files with 125 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
compiler/global/static.ml
View file

@ -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

22
compiler/heptagon/analysis/causality.ml
View file

@ -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

68
compiler/heptagon/analysis/typing.ml
View file

@ -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 ->

48
compiler/heptagon/hept_printer.ml
View file

@ -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 " @@ ";

32
compiler/minils/analysis/clocking.ml
View file

@ -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)

34
compiler/minils/transformations/normalize.ml
View file

@ -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

2
compiler/obc/c/cgen.ml
View file

@ -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)

4
compiler/utilities/misc.ml
View file

@ -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

1
compiler/utilities/misc.mli
View file

@ -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