diff --git a/compiler/_tags b/compiler/_tags index 8a23c20..97f462d 100644 --- a/compiler/_tags +++ b/compiler/_tags @@ -2,3 +2,4 @@ <**/*.ml>: debug, dtypes : camlp4of, use_camlp4 <**/*.{byte,native}>: use_unix, use_str, debug +true: use_menhir diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index b64b85e..c0d510d 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -22,10 +22,10 @@ type param = { p_name : name } (** Node signature *) type node = - { node_inputs : arg list; - node_outputs : arg list; - node_params : param list; (** Static parameters *) - node_params_constraints : size_constr list } + { node_inputs : arg list; + node_outputs : arg list; + node_params : param list; (** Static parameters *) + node_params_constraints : size_constr list } type field = { f_name : name; f_type : ty } type structure = field list @@ -37,12 +37,10 @@ let names_of_arg_list l = List.map (fun ad -> ad.a_name) l let types_of_arg_list l = List.map (fun ad -> ad.a_type) l -let mk_arg name ty = - { a_type = ty; a_name = name } - -let mk_param name = - { p_name = name } +let mk_arg name ty = { a_type = ty; a_name = name } +let mk_param name = { p_name = name } + let print_param ff p = Names.print_name ff p.p_name diff --git a/compiler/heptagon/main/heptcheck.ml b/compiler/heptagon/main/heptcheck.ml index 088dd70..09d8e11 100644 --- a/compiler/heptagon/main/heptcheck.ml +++ b/compiler/heptagon/main/heptcheck.ml @@ -15,11 +15,23 @@ open Location let pp = Hept_printer.print stdout +let parse parsing_fun lexing_fun lexbuf = + try + parsing_fun lexing_fun lexbuf + with + | Hept_lexer.Lexical_error(err, pos1, pos2) -> + lexical_error err (Loc(pos1, pos2)) + | Parsing.Parse_error -> + let pos1 = Lexing.lexeme_start lexbuf + and pos2 = Lexing.lexeme_end lexbuf in + let l = Loc(pos1,pos2) in + syntax_error l + let parse_implementation lexbuf = - parse Parser.program Lexer.token lexbuf + parse Hept_parser.program Hept_lexer.token lexbuf let parse_interface lexbuf = - parse Parser.interface Lexer.token lexbuf + parse Hept_parser.interface Hept_lexer.token lexbuf let compile_impl modname filename = (* input and output files *) diff --git a/compiler/heptagon/parsing/scoping.ml b/compiler/heptagon/parsing/scoping.ml index b04e652..c1eb636 100644 --- a/compiler/heptagon/parsing/scoping.ml +++ b/compiler/heptagon/parsing/scoping.ml @@ -114,20 +114,17 @@ let op_from_app loc app = | _ -> Error.message loc Error.Estatic_exp_expected let check_const_vars = ref true -let rec translate_size_exp const_env e = - match e.e_desc with - | Evar n -> - if !check_const_vars & not (NamesEnv.mem n const_env) then - Error.message e.e_loc (Error.Econst_var n) - else - SVar n - | Econst (Cint i) -> SConst i - | Eapp(app, [e1;e2]) -> - let op = op_from_app e.e_loc app in - SOp(op, - translate_size_exp const_env e1, - translate_size_exp const_env e2) - | _ -> Error.message e.e_loc Error.Estatic_exp_expected +let rec translate_size_exp const_env e = match e.e_desc with + | Evar n -> + if !check_const_vars & not (NamesEnv.mem n const_env) then + Error.message e.e_loc (Error.Econst_var n) + else + SVar n + | Econst (Cint i) -> SConst i + | Eapp(app, [e1;e2]) -> + let op = op_from_app e.e_loc app in + SOp(op, translate_size_exp const_env e1, translate_size_exp const_env e2) + | _ -> Error.message e.e_loc Error.Estatic_exp_expected let rec translate_type const_env = function | Tprod ty_list -> Types.Tprod(List.map (translate_type const_env) ty_list) @@ -160,10 +157,8 @@ and translate_op_desc const_env desc = Heptagon.op_kind = translate_op_kind desc.op_kind } and translate_array_op const_env env = function - | Eselect e_list -> - Heptagon.Eselect (List.map (translate_size_exp const_env) e_list) - | Eupdate e_list -> - Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list) + | Eselect e_list -> Heptagon.Eselect (List.map (translate_size_exp const_env) e_list) + | Eupdate e_list -> Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list) | Erepeat -> Heptagon.Erepeat | Eselect_slice -> Heptagon.Eselect_slice | Econcat -> Heptagon.Econcat @@ -175,16 +170,14 @@ and translate_array_op const_env env = function and translate_desc loc const_env env = function | Econst c -> Heptagon.Econst (translate_const c) | Evar x -> - if Rename.mem x env then - Heptagon.Evar (Rename.name loc env x) - else - if NamesEnv.mem x const_env then (* var not defined, maybe a const var*) - Heptagon.Econstvar x - else - Error.message loc (Error.Evar x) + if Rename.mem x env then (* defined var *) + Heptagon.Evar (Rename.name loc env x) + else if NamesEnv.mem x const_env then (* defined as const var *) + Heptagon.Econstvar x + else (* undefined var *) + Error.message loc (Error.Evar x) | Elast x -> Heptagon.Elast (Rename.name loc env x) - | Etuple e_list -> - Heptagon.Etuple (List.map (translate_exp const_env env) e_list) + | Etuple e_list -> Heptagon.Etuple (List.map (translate_exp const_env env) e_list) | Eapp ({ a_op = (Earray_op Erepeat)} as app, e_list) -> let e_list = List.map (translate_exp const_env env) e_list in (match e_list with @@ -197,11 +190,9 @@ and translate_desc loc const_env env = function Heptagon.Eapp (translate_app const_env env app, e_list) | Efield (e, field) -> Heptagon.Efield (translate_exp const_env env e, field) | Estruct f_e_list -> - let f_e_list = - List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in - Heptagon.Estruct f_e_list - | Earray e_list -> - Heptagon.Earray (List.map (translate_exp const_env env) e_list) + let f_e_list = List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in + Heptagon.Estruct f_e_list + | Earray e_list -> Heptagon.Earray (List.map (translate_exp const_env env) e_list) and translate_pat loc env = function | Evarpat x -> Heptagon.Evarpat (Rename.name loc env x) @@ -221,9 +212,9 @@ and translate_eq_desc loc const_env env = function | Eeq(p, e) -> Heptagon.Eeq (translate_pat loc env p, translate_exp const_env env e) | Epresent (present_handlers, b) -> - Heptagon.Epresent (List.map (translate_present_handler const_env env) - present_handlers, - fst (translate_block const_env env b)) + Heptagon.Epresent + (List.map (translate_present_handler const_env env) present_handlers + , fst (translate_block const_env env b)) | Eautomaton state_handlers -> Heptagon.Eautomaton (List.map (translate_state_handler const_env env) state_handlers) @@ -302,8 +293,7 @@ let translate_typedec const_env ty = | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list) | Type_struct(field_ty_list) -> let translate_field_type (f,ty) = - Signature.mk_field f (translate_type const_env ty) - in + Signature.mk_field f (translate_type const_env ty) in Heptagon.Type_struct (List.map translate_field_type field_ty_list) in { Heptagon.t_name = ty.t_name; diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index bdc351c..9db44bb 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -19,6 +19,7 @@ open Format open Printf open Minils +open Mls_utils open Signature module Error = diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 1085fc4..8489ebe 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -11,25 +11,9 @@ open Misc open Location open Compiler_utils +open Heptcheck -let parse parsing_fun lexing_fun lexbuf = - try - parsing_fun lexing_fun lexbuf - with - | Hept_lexer.Lexical_error(err, pos1, pos2) -> - lexical_error err (Loc(pos1, pos2)) - | Parsing.Parse_error -> - let pos1 = Lexing.lexeme_start lexbuf - and pos2 = Lexing.lexeme_end lexbuf in - let l = Loc(pos1,pos2) in - syntax_error l - -let parse_implementation lexbuf = - parse Hept_parser.program Hept_lexer.token lexbuf - -let parse_interface lexbuf = - parse Hept_parser.interface Hept_lexer.token lexbuf let interface modname filename = (* input and output files *) diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 3a45752..ad9a535 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -17,23 +17,22 @@ open Types open Location open Printf -type error = | Etypeclash of ct * ct +(** Error Kind *) +type err_kind = | Etypeclash of ct * ct -exception TypingError of error +let err_message exp = function + | Etypeclash (actual_ct, expected_ct) -> + Printf.eprintf "%aClock Clash: this expression has clock %a, \n\ + but is expected to have clock %a.\n" + print_exp exp + print_clock actual_ct + print_clock expected_ct; + raise Error exception Unify -let error kind = raise (TypingError kind) - -let message e kind = - match kind with | Etypeclash (actual_ct, expected_ct) -> - Printf.eprintf "%aClock Clash: this expression has clock %a, \n\ - but is expected to have clock %a.\n" - Mls_printer.print_exp e - Mls_printer.print_clock actual_ct - Mls_printer.print_clock expected_ct; - raise Error + let index = ref 0 let gen_index () = (incr index; !index) @@ -42,65 +41,64 @@ let new_var () = Cvar { contents = Cindex (gen_index ()); } let rec repr ck = match ck with - | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck - | Cvar (({ contents = Clink ck } as link)) -> - let ck = repr ck in (link.contents <- Clink ck; ck) - + | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck + | Cvar (({ contents = Clink ck } as link)) -> + let ck = repr ck in (link.contents <- Clink ck; ck) + let rec occur_check index ck = let ck = repr ck in match ck with - | Cbase -> () - | Cvar { contents = Cindex n } when index <> n -> () - | Con (ck, _, _) -> occur_check index ck - | _ -> raise Unify + | Cbase -> () + | Cvar { contents = Cindex n } when index <> n -> () + | Con (ck, _, _) -> occur_check index ck + | _ -> raise Unify let rec ck_value ck = match ck with - | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck - | Cvar { contents = Clink ck } -> ck_value ck - + | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck + | Cvar { contents = Clink ck } -> ck_value ck + let rec unify t1 t2 = if t1 == t2 then () else (match (t1, t2) with - | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2 - | (Cprod ct_list1, Cprod ct_list2) -> - (try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify) - | _ -> raise Unify) + | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2 + | (Cprod ct_list1, Cprod ct_list2) -> + (try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify) + | _ -> raise Unify) and unify_ck ck1 ck2 = let ck1 = repr ck1 in - let ck2 = repr ck2 - in + let ck2 = repr ck2 in if ck1 == ck2 then () else (match (ck1, ck2) with - | (Cbase, Cbase) -> () - | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when - n1 = n2 -> () - | (Cvar (({ contents = Cindex n1 } as v)), _) -> - (occur_check n1 ck2; v.contents <- Clink ck2) - | (_, Cvar (({ contents = Cindex n2 } as v))) -> - (occur_check n2 ck1; v.contents <- Clink ck1) - | (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) -> - unify_ck ck1 ck2 - | _ -> raise Unify) + | (Cbase, Cbase) -> () + | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when + n1 = n2 -> () + | (Cvar (({ contents = Cindex n1 } as v)), _) -> + (occur_check n1 ck2; v.contents <- Clink ck2) + | (_, Cvar (({ contents = Cindex n2 } as v))) -> + (occur_check n2 ck1; v.contents <- Clink ck1) + | (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) -> + unify_ck ck1 ck2 + | _ -> raise Unify) let rec eq ck1 ck2 = match ((repr ck1), (repr ck2)) with - | (Cbase, Cbase) -> true - | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) -> true - | (Con (ck1, _, n1), Con (ck2, _, n2)) when n1 = n2 -> eq ck1 ck2 - | _ -> false - + | (Cbase, Cbase) -> true + | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) -> true + | (Con (ck1, _, n1), Con (ck2, _, n2)) when n1 = n2 -> eq ck1 ck2 + | _ -> false + let rec unify t1 t2 = match (t1, t2) with - | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2 - | (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list - | _ -> raise Unify + | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2 + | (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list + | _ -> raise Unify and unify_list t1_list t2_list = try List.iter2 unify t1_list t2_list with | _ -> raise Unify @@ -119,45 +117,45 @@ let typ_of_name h x = Env.find x h let rec typing h e = let ct = match e.e_desc with - | Econst _ | Econstvar _ -> Ck (new_var ()) - | Evar x -> Ck (typ_of_name h x) - | Efby (c, e) -> typing h e - | Etuple e_list -> Cprod (List.map (typing h) e_list) - | Ecall(_, e_list, r) -> - let ck_r = match r with - | None -> new_var() - | Some(reset) -> typ_of_name h reset - in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty) - | Ecall(_, e_list, Some(reset)) -> - let ck_r = typ_of_name h reset - in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty) - | Ewhen (e, c, n) -> - let ck_n = typ_of_name h n - in (expect h (skeleton ck_n e.e_ty) e; - skeleton (Con (ck_n, c, n)) e.e_ty) - | Eifthenelse (e1, e2, e3) -> - let ck = new_var () in - let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct) - | Emerge (n, c_e_list) -> - let ck_c = typ_of_name h n - in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty) - | Efield (e1, n) -> - let ck = new_var () in - let ct = skeleton ck e1.e_ty in (expect h (Ck ck) e1; ct) - | Efield_update (_, e1, e2) -> - let ck = new_var () in - let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; ct) - | Estruct l -> - let ck = new_var () in - (List.iter - (fun (n, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l; - Ck ck) - | Earray e_list -> - let ck = new_var () - in (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty) - | Earray_op(op) -> typing_array_op h e op + | Econst _ | Econstvar _ -> Ck (new_var ()) + | Evar x -> Ck (typ_of_name h x) + | Efby (c, e) -> typing h e + | Etuple e_list -> Cprod (List.map (typing h) e_list) + | Ecall(_, e_list, r) -> + let ck_r = match r with + | None -> new_var() + | Some(reset) -> typ_of_name h reset + in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty) + | Ecall(_, e_list, Some(reset)) -> + let ck_r = typ_of_name h reset + in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty) + | Ewhen (e, c, n) -> + let ck_n = typ_of_name h n + in (expect h (skeleton ck_n e.e_ty) e; + skeleton (Con (ck_n, c, n)) e.e_ty) + | Eifthenelse (e1, e2, e3) -> + let ck = new_var () in + let ct = skeleton ck e.e_ty + in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct) + | Emerge (n, c_e_list) -> + let ck_c = typ_of_name h n + in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty) + | Efield (e1, n) -> + let ck = new_var () in + let ct = skeleton ck e1.e_ty in (expect h (Ck ck) e1; ct) + | Efield_update (_, e1, e2) -> + let ck = new_var () in + let ct = skeleton ck e.e_ty + in (expect h (Ck ck) e1; expect h ct e2; ct) + | Estruct l -> + let ck = new_var () in + (List.iter + (fun (n, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l; + Ck ck) + | Earray e_list -> + let ck = new_var () + in (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty) + | Earray_op(op) -> typing_array_op h e op in (e.e_ck <- ckofct ct; ct) and typing_array_op h e = function @@ -186,97 +184,76 @@ and typing_array_op h e = function and expect h expected_ty e = let actual_ty = typing h e in - try unify actual_ty expected_ty - with | Unify -> message e (Etypeclash (actual_ty, expected_ty)) + try unify actual_ty expected_ty + with | Unify -> err_message e (Etypeclash (actual_ty, expected_ty)) and typing_c_e_list h ck_c n c_e_list = let rec typrec = function - | [] -> () - | (c, e) :: c_e_list -> - (expect h (skeleton (Con (ck_c, c, n)) e.e_ty) e; typrec c_e_list) + | [] -> () + | (c, e) :: c_e_list -> + (expect h (skeleton (Con (ck_c, c, n)) e.e_ty) e; typrec c_e_list) in typrec c_e_list let rec typing_pat h = function - | Evarpat x -> Ck (typ_of_name h x) - | Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list) - -let typing_eqs h eq_list = - List.iter - (fun { eq_lhs = pat; eq_rhs = e } -> - match e.e_desc with (*TODO FIXME*) - | _ -> - let ty_pat = typing_pat h pat - in - (try expect h ty_pat e - with - | Error -> - (* TODO remettre en route quand Printer fonctionne - - (* DEBUG *) - Printf.eprintf "Complete expression: %a\n" - Printer.print_exp e; - Printf.eprintf "Clock pattern: %a\n" - Printer.print_clock ty_pat; *) - raise Error)) - eq_list + | Evarpat x -> Ck (typ_of_name h x) + | Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list) + +let typing_eqs h eq_list = (*TODO FIXME*) + let typing_eq { eq_lhs = pat; eq_rhs = e } = match e.e_desc with + | _ -> let ty_pat = typing_pat h pat in + (try expect h ty_pat e with + | Error -> (* DEBUG *) + Printf.eprintf "Complete expression: %a\nClock pattern: %a\n" + Mls_printer.print_exp e + Mls_printer.print_clock ty_pat; + raise Error) in + List.iter typing_eq eq_list let build h dec = - List.fold_left (fun h { v_name = n } -> Env.add n (new_var ()) h) h dec + List.fold_left (fun h { v_ident = n } -> Env.add n (new_var ()) h) h dec let sbuild h dec base = - List.fold_left (fun h { v_name = n } -> Env.add n base h) h dec + List.fold_left (fun h { v_ident = n } -> Env.add n base h) h dec let typing_contract h contract base = match contract with - | None -> h - | Some - { - c_local = l_list; - c_eq = eq_list; - c_assume = e_a; - c_enforce = e_g; - c_controllables = c_list - } -> - let h = sbuild h c_list base in - let h' = build h l_list - in - (* assumption *) - (* property *) - (typing_eqs h' eq_list; - expect h' (Ck base) e_a; - expect h' (Ck base) e_g; - h) + | None -> h + | Some { c_local = l_list; + c_eq = eq_list; + c_assume = e_a; + c_enforce = e_g; + c_controllables = c_list } -> + let h = sbuild h c_list base in + let h' = build h l_list in + (* assumption *) + (* property *) + (typing_eqs h' eq_list; + expect h' (Ck base) e_a; + expect h' (Ck base) e_g; + h) -let typing_node (({ - n_name = f; +let typing_node ({ n_name = f; n_input = i_list; n_output = o_list; n_contract = contract; n_local = l_list; n_equs = eq_list - } as node)) - = + } as node) = let base = Cbase in let h = sbuild Env.empty i_list base in let h = sbuild h o_list base in let h = typing_contract h contract base in - let h = build h l_list - in + let h = build h l_list in (typing_eqs h eq_list; - (*update clock info in variables descriptions *) - let set_clock vd = - { (vd) with v_clock = ck_value (Env.find vd.v_name h); } - in - { - (node) - with + (*update clock info in variables descriptions *) + let set_clock vd = { vd with v_clock = ck_value (Env.find vd.v_ident h) } in + { (node) with n_input = List.map set_clock i_list; n_output = List.map set_clock o_list; - n_local = List.map set_clock l_list; - }) - + n_local = List.map set_clock l_list }) + let program (({ p_nodes = p_node_list } as p)) = { (p) with p_nodes = List.map typing_node p_node_list; } diff --git a/compiler/minils/analysis/init.ml b/compiler/minils/analysis/init.ml index 25f4d11..c0789df 100644 --- a/compiler/minils/analysis/init.ml +++ b/compiler/minils/analysis/init.ml @@ -282,7 +282,7 @@ let build h eq_list = let sbuild h dec = List.fold_left - (fun h { v_name = n } -> Env.add n { t_init = izero; t_value = None; } h) + (fun h { v_ident = n } -> Env.add n { t_init = izero; t_value = None; } h) h dec let typing_contract h contract = diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index bdd1944..cd0e889 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -10,8 +10,6 @@ (* The internal MiniLustre representation *) open Location -open Dep -open Misc open Names open Ident open Signature @@ -45,11 +43,9 @@ and edesc = | Econstvar of name | Efby of const option * exp | Etuple of exp list - | Ecall of op_desc * exp list * ident option (** [op_desc] is the function - called [exp list] is the - passed arguments [ident - option] is the optional reset - condition *) + | Ecall of op_desc * exp list * ident option (** [op_desc] is the function called + [exp list] is the passed arguments + [ident option] is the optional reset condition *) | Ewhen of exp * longname * ident | Emerge of ident * (longname * exp) list @@ -69,10 +65,11 @@ and array_op = | Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, array*) | Econcat of exp * exp - | Eiterator of iterator_type * op_desc * size_exp * exp list * ident option - (** [op_desc] is the function iterated, [size_exp] is the size of the - iteration, [exp list] is the passed arguments, [ident option] is the - optional reset condition *) + | Eiterator of iterator_type * op_desc * size_exp * exp list * ident option (** + [op_desc] is the function iterated, + [size_exp] is the size of the iteration, + [exp list] is the passed arguments, + [ident option] is the optional reset condition *) and op_desc = { op_name: longname; op_params: size_exp list; op_kind: op_kind } and op_kind = | Eop | Enode @@ -106,7 +103,7 @@ type eq = eq_loc : location } type var_dec = - { v_name : ident; + { v_ident : ident; v_type : ty; v_clock : ck } @@ -146,190 +143,35 @@ type program = (*Helper functions to build the AST*) - let mk_exp ?(exp_ty = Tprod []) ?(clock = Cbase) ?(loc = no_location) desc = { e_desc = desc; e_ty = exp_ty; e_ck = clock; e_loc = loc } -let mk_var_dec ?(clock = Cbase) name ty = - { v_name = name; v_type = ty; +let mk_var_dec ?(clock = Cbase) ident ty = + { v_ident = ident; v_type = ty; v_clock = clock } let mk_equation ?(loc = no_location) pat exp = { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) - ?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name = - { n_name = name; - n_input = input; - n_output = output; - n_contract = contract; - n_local = local; - n_equs = eq; - n_loc = loc; - n_params = param; - n_params_constraints = constraints; - n_params_instances = pinst; } + ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) + ?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name = + { n_name = name; + n_input = input; + n_output = output; + n_contract = contract; + n_local = local; + n_equs = eq; + n_loc = loc; + n_params = param; + n_params_constraints = constraints; + n_params_instances = pinst; } let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name = { t_name = name; t_desc = type_desc; t_loc = loc } - -let rec size_exp_of_exp e = - match e.e_desc with - | Econstvar n -> SVar n - | Econst (Cint i) -> SConst i - | Ecall(op, [e1;e2], _) -> - let sop = op_from_app_name op.op_name in - SOp(sop, size_exp_of_exp e1, size_exp_of_exp e2) - | _ -> raise Not_static - -(** @return the list of bounds of an array type*) -let rec bounds_list ty = - match ty with - | Tarray(ty, n) -> n::(bounds_list ty) - | _ -> [] - -(** @return the [var_dec] object corresponding to the name [n] - in a list of [var_dec]. *) -let rec vd_find n = function - | [] -> Format.printf "Not found var %s\n" (name n); raise Not_found - | vd::l -> - if vd.v_name = n then vd else vd_find n l - -(** @return whether an object of name [n] belongs to - a list of [var_dec]. *) -let rec vd_mem n = function - | [] -> false - | vd::l -> vd.v_name = n or (vd_mem n l) - -(** @return whether [ty] corresponds to a record type. *) -let is_record_type ty = match ty with - | Tid n -> - (try - ignore (Modules.find_struct n); true - with - Not_found -> false) - | _ -> false - -module Vars = -struct - let add x acc = - if List.mem x acc then acc else x :: acc - - let rec vars_pat acc = function - | Evarpat x -> x :: acc - | Etuplepat pat_list -> List.fold_left vars_pat acc pat_list - - let rec vars_ck acc = function - | Con(ck, c, n) -> add n acc - | Cbase | Cvar { contents = Cindex _ } -> acc - | Cvar { contents = Clink ck } -> vars_ck acc ck - - let rec read is_left acc e = - let acc = - match e.e_desc with - | Evar n -> add n acc - | Emerge(x, c_e_list) -> - let acc = add x acc in - List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list - | Eifthenelse(e1, e2, e3) -> - read is_left (read is_left (read is_left acc e1) e2) e3 - | Ewhen(e, c, x) -> - let acc = add x acc in - read is_left acc e - | Etuple(e_list) -> List.fold_left (read is_left) acc e_list - | Ecall(_, e_list, None) -> - List.fold_left (read is_left) acc e_list - | Ecall(_, e_list, Some x) -> - let acc = add x acc in - List.fold_left (read is_left) acc e_list - | Efby(_, e) -> - if is_left then vars_ck acc e.e_ck else read is_left acc e - | Efield(e, _) -> read is_left acc e - | Estruct(f_e_list) -> - List.fold_left (fun acc (_, e) -> read is_left acc e) acc f_e_list - | Econst _ | Econstvar _ -> acc - | Efield_update (_, e1, e2) -> - read is_left (read is_left acc e1) e2 - (*Array operators*) - | Earray e_list -> List.fold_left (read is_left) acc e_list - | Earray_op op -> read_array_op is_left acc op - in - vars_ck acc e.e_ck - - and read_array_op is_left acc = function - | Erepeat (_,e) -> read is_left acc e - | Eselect (_,e) -> read is_left acc e - | Eselect_dyn (e_list, _, e1, e2) -> - let acc = List.fold_left (read is_left) acc e_list in - read is_left (read is_left acc e1) e2 - | Eupdate (_, e1, e2) -> - read is_left (read is_left acc e1) e2 - | Eselect_slice (_ , _, e) -> read is_left acc e - | Econcat (e1, e2) -> - read is_left (read is_left acc e1) e2 - | Eiterator (_, _, _, e_list, None) -> - List.fold_left (read is_left) acc e_list - | Eiterator (_, _, _, e_list, Some x) -> - let acc = add x acc in - List.fold_left (read is_left) acc e_list - - let rec remove x = function - | [] -> [] - | y :: l -> if x = y then l else y :: remove x l - - let def acc { eq_lhs = pat } = vars_pat acc pat - - let read is_left { eq_lhs = pat; eq_rhs = e } = - match pat, e.e_desc with - | Evarpat(n), Efby(_, e1) -> - if is_left - then remove n (read is_left [] e1) - else read is_left [] e1 - | _ -> read is_left [] e - - let antidep { eq_rhs = e } = - match e.e_desc with Efby _ -> true | _ -> false - - let clock { eq_rhs = e } = - match e.e_desc with - | Emerge(_, (_, e) :: _) -> e.e_ck - | _ -> e.e_ck - - let head ck = - let rec headrec ck l = - match ck with - | Cbase | Cvar { contents = Cindex _ } -> l - | Con(ck, c, n) -> headrec ck (n :: l) - | Cvar { contents = Clink ck } -> headrec ck l - in - headrec ck [] - - (** Returns a list of memory vars (x in x = v fby e) - appearing in an equation. *) - let memory_vars ({ eq_lhs = _; eq_rhs = e } as eq) = - match e.e_desc with - | Efby(_, _) -> def [] eq - | _ -> [] -end - - -(* data-flow dependences. pre-dependences are discarded *) -module DataFlowDep = Make - (struct - type equation = eq - let read eq = Vars.read true eq - let def = Vars.def - let antidep = Vars.antidep - end) - -(* all dependences between variables *) -module AllDep = Make - (struct - type equation = eq - let read eq = Vars.read false eq - let def = Vars.def - let antidep eq = false - end) +let mk_op ?(op_params = []) ?(op_kind = Enode) lname = + { op_name = lname; op_params = op_params; op_kind = op_kind } + +let void = mk_exp (Etuple []) diff --git a/compiler/minils/mls_lexer.mll b/compiler/minils/mls_lexer.mll index 688de1b..3167f1b 100644 --- a/compiler/minils/mls_lexer.mll +++ b/compiler/minils/mls_lexer.mll @@ -20,14 +20,10 @@ let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);; List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "node", NODE; "fun", FUN; - "safe", SAFE; "returns", RETURNS; "var", VAR; - "val", VAL; - "unsafe", UNSAFE; "let", LET; "tel", TEL; - "end", END; "fby", FBY; "switch", SWITCH; "when", WHEN; @@ -140,16 +136,18 @@ rule token = parse | "&&" {AMPERAMPER} | "||" {BARBAR} | "," {COMMA} - | "->" {ARROW} +(* | "->" {ARROW} *) | "|" {BAR} | "-" {SUBTRACTIVE "-"} | "-." {SUBTRACTIVE "-."} + | "<<" {DOUBLE_LESS} + | ">>" {DOUBLE_GREATER} | (['A'-'Z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) - {Constructor id} + {CONSTRUCTOR id} | (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) { let s = Lexing.lexeme lexbuf in try Hashtbl.find keyword_table s - with Not_found -> IDENT id } + with Not_found -> NAME id } | '-'? ['0'-'9']+ | '-'? '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ | '-'? '0' ['o' 'O'] ['0'-'7']+ diff --git a/compiler/minils/mls_parser.mly b/compiler/minils/mls_parser.mly index 173847c..ffe6fe7 100644 --- a/compiler/minils/mls_parser.mly +++ b/compiler/minils/mls_parser.mly @@ -7,16 +7,15 @@ open Ident open Types open Location open Minils +open Mls_utils let mk_exp = mk_exp ~loc:(current_loc()) let mk_node = mk_node ~loc:(current_loc()) let mk_equation p e = mk_equation ~loc:(current_loc()) p e let mk_type name desc = mk_type_dec ~loc:(current_loc()) ~type_desc: desc name - - - let mk_var name ty = mk_var_dec name ty + %} %token DOT LPAREN RPAREN LBRACE RBRACE COLON SEMICOL @@ -55,6 +54,7 @@ let mk_var name ty = mk_var_dec name ty %token WITH %token INLINED %token AT +%token DOUBLE_LESS DOUBLE_GREATER %token PREFIX %token INFIX0 %token INFIX1 @@ -72,7 +72,7 @@ let mk_var name ty = mk_var_dec name ty %left OR %left AMPERSAND %left INFIX0 EQUAL -%right INFIX1 +%right INFIX1 EQUALEQUAL BARBAR AMPERAMPER %left INFIX2 SUBTRACTIVE %left STAR INFIX3 %left INFIX4 @@ -97,23 +97,22 @@ let mk_var name ty = mk_var_dec name ty /** Tools **/ /* Redefinitions */ -%inline option_list(x) : l=list(x) {l} -%inline list(x) : l=nonempty_list(x) {l} -%inline option_slist(S, x) : l=separated_list(S, x) {l} -%inline slist(S, x) : l=separated_nonempty_list(S, x) {l} - -%inline nuple(L, R, S, x) : L h=x S t=slist(S,x) R { h::t } -%inline stuple(S, x) : LPAREN h=x S t=slist(S,x) RPAREN { h::t } -%inline tuple(x) : t=stuple(COMMA,x) { t } -%inline option2(P,x) : /* empty */ { None } | P v=x { Some(v)} +%inline slist(S, x) : l=separated_list(S, x) {l} +%inline snlist(S, x) : l=separated_nonempty_list(S, x) {l} +%inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t } +%inline option(P,x): + |/* empty */ { None } + | P v=x { Some(v) } +%inline option2(L,x,R): + |/* empty */ { None } + | L v=x R { Some(v) } qualified(x) : - | n=x { Name(n) } %prec prec_ident + | n=x { Name(n) } | m=CONSTRUCTOR DOT n=x { Modname({ qual = m; id = n }) } - -structure(field): s=nuple(LBRACE, RBRACE, SEMICOL, field) {s} - - + +structure(field): LBRACE s=snlist(SEMICOL,field) RBRACE {s} + program: | pragma_headers open_modules type_decs node_decs EOF @@ -123,53 +122,52 @@ program: p_nodes = $4; p_consts = []}} /*TODO consts dans program*/ -pragma_headers: l=option_list(pragma) {l} -pragma: p=PRAGMA {p} +pragma_headers: l=list(PRAGMA) {l} -open_modules: l=option_list(opens) {l} +open_modules: l=list(opens) {l} opens: OPEN c=CONSTRUCTOR {c} -ident: n=NAME | LPAREN n=infix RPAREN | LPAREN n=prefix RPAREN { n } +name: n=NAME | LPAREN n=infix_ RPAREN | LPAREN n=prefix_ RPAREN { n } +ident: n=name { ident_of_name n } -field_type : n=NAME COLON t=type_ident { (n, t) } +field_type : n=NAME COLON t=type_ident { mk_field n t } type_ident: NAME { Tid(Name($1)) } -type_decs: t=option_list(type_dec) {t} +type_decs: t=list(type_dec) {t} type_dec: | TYPE n=NAME { mk_type n Type_abs } - | TYPE n=NAME EQUAL e=slist(BAR,NAME) { mk_type n (Type_enum e) } + | TYPE n=NAME EQUAL e=snlist(BAR,NAME) { mk_type n (Type_enum e) } | TYPE n=NAME EQUAL s=structure(field_type) { mk_type n (Type_struct s) } -node_decs: ns=option_list(node_dec) {ns} +node_decs: ns=list(node_dec) {ns} node_dec: - NODE id=ident LPAREN args=params RPAREN RETURNS LPAREN out=params RPAREN - vars=loc_vars LET eqs=equs TEL - { mk_node - ~input: args - ~output: out - ~local: vars - ~eq: eqs - id } + NODE n=name p=params(n_param) LPAREN args=args RPAREN + RETURNS LPAREN out=args RPAREN vars=loc_vars eqs=equs + { mk_node ~input:args ~output:out ~local:vars ~eq:eqs n } + -params: p=option_slist(SEMICOL, var) {p} +args_t: SEMICOL p=args {p} +args: + | /* empty */ {[]} + | h=var t=loption(args_t) {h@t} -loc_vars: - | /* empty */ { [] } - | VAR vs=slist(SEMICOL, var) { vs } +loc_vars_t: SEMICOL h=var t=loc_vars_t {h@t} +loc_vars_h: VAR h=var t=loc_vars_t {h@t} +loc_vars: l=loption(loc_vars_h) {l} var: - | ns=slist(COMMA, NAME) COLON t=type_ident - { List.map (fun id -> mk_var id t) ns } + | ns=snlist(COMMA, NAME) COLON t=type_ident + { List.map (fun id -> mk_var (ident_of_name id) t) ns } -equs: e=option_slist(SEMICOL, equ) ?SEMICOL {e} -equ: p=pat EQUAL e=exp { mk_eq p e } +equs: LET e=slist(SEMICOL, equ) TEL { e } +equ: p=pat EQUAL e=exp { mk_equation p e } pat: | n=NAME {Evarpat (ident_of_name n)} - | LPAREN p=slist(COMMA, pat) RPAREN {Etuplepat p} + | LPAREN p=snlist(COMMA, pat) RPAREN {Etuplepat p} -longname: l=qualified(ident) {l} +longname: l=qualified(name) {l} constructor: | ln=qualified(CONSTRUCTOR) {ln} @@ -180,40 +178,46 @@ const: | FLOAT { Cfloat($1) } | constructor { Cconstr($1) } -exps: LPAREN e=option_slist(COMMA, exp) RPAREN {e} - -tuple_exp: LPAREN e=option_slist(COMMA, exp) RPAREN {e} +exps: LPAREN e=slist(COMMA, exp) RPAREN {e} field_exp: longname EQUAL exp { ($1, $3) } simple_exp: | NAME { mk_exp (Evar (ident_of_name $1)) } - | c=const { mk_exp (Econst c) } | s=structure(field_exp) { mk_exp (Estruct s) } - | t=tuple_exp { mk_exp (Etuple t) } + | t=tuple(exp) { mk_exp (Etuple t) } | LPAREN e=exp RPAREN { e } exp: - | e=simple_exp { e } - | const FBY exp - { make_exp (Efby(Some($1),$3)) } - | PRE exp - { make_exp (Efby(None,$2)) } - | longname LPAREN exps RPAREN %prec prec_apply - { make_exp (Eapp(make_app $1 Ino, $3)) } - | INLINED longname LPAREN exps RPAREN %prec prec_apply - { make_exp (Eapp(make_app $2 Irec, $4)) } - | e1=exp op=infix e2=exp - { make_exp (Eop(Name(op), [e1; e2])) } - | op=prefix e=exp %prec prefixs - { make_exp (Eop(Name(op), [e])) } - | IF exp THEN exp ELSE exp - { make_exp (Eifthenelse($2, $4, $6)) } - | exp DOT longname - { make_exp (Efield($1, $3)) } + | e=simple_exp { e } + | c=const { mk_exp (Econst c) } + | const FBY exp { mk_exp (Efby(Some($1),$3)) } + | PRE exp { mk_exp (Efby(None,$2)) } + | op=node_app a=exps r=reset { mk_exp (Ecall(op, a, r)) } + | e1=exp i_op=infix e2=exp + { mk_exp (Ecall(mk_op ~op_kind:Eop i_op, [e1; e2], None)) } + | p_op=prefix e=exp %prec prefixs + { mk_exp (Ecall(mk_op ~op_kind:Eop p_op, [e], None)) } + | IF e1=exp THEN e2=exp ELSE e3=exp { mk_exp (Eifthenelse(e1, e2, e3)) } + | e=simple_exp DOT m=longname { mk_exp (Efield(e, m)) } -%inline infix: + +reset: r=option(RESET,ident) { r } + +node_app: ln=longname p=params(e_param) { mk_op ~op_kind:Enode ~op_params:p ln } + + +e_param: e=exp { size_exp_of_exp e } +n_param: n=NAME { mk_param n } +params(param): + | /*empty*/ { [] } + | DOUBLE_LESS p=slist(COMMA, param) DOUBLE_GREATER { p } + + +/*Inlining is compulsory in order to preserve priorities*/ +%inline infix: op=infix_ { Name(op) } +%inline infix_: | op=INFIX0 | op=INFIX1 | op=INFIX2 | op=INFIX3 | op=INFIX4 { op } | STAR { "*" } | EQUAL { "=" } @@ -221,7 +225,8 @@ exp: | AMPERSAND { "&" } | AMPERAMPER { "&&" } | OR { "or" } | BARBAR { "||" } -prefix: +prefix: op=prefix_ { Name(op) } +prefix_: | op = PREFIX { op } | NOT { "not" } | op = SUBTRACTIVE { "~" ^ op } /*TODO test 3 * -2 and co */ diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 4ff6044..13a6b72 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -38,7 +38,7 @@ let rec print_clock ff = function | Cprod ct_list -> fprintf ff "@[<2>%a@]" (print_list_r print_clock "("" *"")") ct_list -let print_vd ff { v_name = n; v_type = ty; v_clock = ck } = +let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } = if !Misc.full_type_info then fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck else fprintf ff "%a : %a" print_ident n print_type ty diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml new file mode 100644 index 0000000..30ac2cc --- /dev/null +++ b/compiler/minils/mls_utils.ml @@ -0,0 +1,175 @@ +open Minils +open Mls_printer +open Location +open Names +open Ident +open Signature +open Static +open Types +open Misc + +(** Error Kind *) +type err_kind = | Enot_size_exp + +let err_message ?(exp=void) ?(loc=exp.e_loc) = function + | Enot_size_exp -> + Printf.eprintf "The expression %a should be a size_exp.@." print_exp exp; + raise Error + +let rec size_exp_of_exp e = + match e.e_desc with + | Econstvar n -> SVar n + | Econst (Cint i) -> SConst i + | Ecall(op, [e1;e2], _) -> + let sop = op_from_app_name op.op_name in + SOp(sop, size_exp_of_exp e1, size_exp_of_exp e2) + | _ -> err_message ~exp:e Enot_size_exp + +(** @return the list of bounds of an array type*) +let rec bounds_list ty = + match ty with + | Tarray(ty, n) -> n::(bounds_list ty) + | _ -> [] + +(** @return the [var_dec] object corresponding to the name [n] + in a list of [var_dec]. *) +let rec vd_find n = function + | [] -> Format.printf "Not found var %s\n" (name n); raise Not_found + | vd::l -> + if vd.v_ident = n then vd else vd_find n l + +(** @return whether an object of name [n] belongs to + a list of [var_dec]. *) +let rec vd_mem n = function + | [] -> false + | vd::l -> vd.v_ident = n or (vd_mem n l) + +(** @return whether [ty] corresponds to a record type. *) +let is_record_type ty = match ty with + | Tid n -> + (try + ignore (Modules.find_struct n); true + with + Not_found -> false) + | _ -> false + +module Vars = +struct + let add x acc = + if List.mem x acc then acc else x :: acc + + let rec vars_pat acc = function + | Evarpat x -> x :: acc + | Etuplepat pat_list -> List.fold_left vars_pat acc pat_list + + let rec vars_ck acc = function + | Con(ck, c, n) -> add n acc + | Cbase | Cvar { contents = Cindex _ } -> acc + | Cvar { contents = Clink ck } -> vars_ck acc ck + + let rec read is_left acc e = + let acc = + match e.e_desc with + | Evar n -> add n acc + | Emerge(x, c_e_list) -> + let acc = add x acc in + List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list + | Eifthenelse(e1, e2, e3) -> + read is_left (read is_left (read is_left acc e1) e2) e3 + | Ewhen(e, c, x) -> + let acc = add x acc in + read is_left acc e + | Etuple(e_list) -> List.fold_left (read is_left) acc e_list + | Ecall(_, e_list, None) -> + List.fold_left (read is_left) acc e_list + | Ecall(_, e_list, Some x) -> + let acc = add x acc in + List.fold_left (read is_left) acc e_list + | Efby(_, e) -> + if is_left then vars_ck acc e.e_ck else read is_left acc e + | Efield(e, _) -> read is_left acc e + | Estruct(f_e_list) -> + List.fold_left (fun acc (_, e) -> read is_left acc e) acc f_e_list + | Econst _ | Econstvar _ -> acc + | Efield_update (_, e1, e2) -> + read is_left (read is_left acc e1) e2 + (*Array operators*) + | Earray e_list -> List.fold_left (read is_left) acc e_list + | Earray_op op -> read_array_op is_left acc op + in + vars_ck acc e.e_ck + + and read_array_op is_left acc = function + | Erepeat (_,e) -> read is_left acc e + | Eselect (_,e) -> read is_left acc e + | Eselect_dyn (e_list, _, e1, e2) -> + let acc = List.fold_left (read is_left) acc e_list in + read is_left (read is_left acc e1) e2 + | Eupdate (_, e1, e2) -> + read is_left (read is_left acc e1) e2 + | Eselect_slice (_ , _, e) -> read is_left acc e + | Econcat (e1, e2) -> + read is_left (read is_left acc e1) e2 + | Eiterator (_, _, _, e_list, None) -> + List.fold_left (read is_left) acc e_list + | Eiterator (_, _, _, e_list, Some x) -> + let acc = add x acc in + List.fold_left (read is_left) acc e_list + + let rec remove x = function + | [] -> [] + | y :: l -> if x = y then l else y :: remove x l + + let def acc { eq_lhs = pat } = vars_pat acc pat + + let read is_left { eq_lhs = pat; eq_rhs = e } = + match pat, e.e_desc with + | Evarpat(n), Efby(_, e1) -> + if is_left + then remove n (read is_left [] e1) + else read is_left [] e1 + | _ -> read is_left [] e + + let antidep { eq_rhs = e } = + match e.e_desc with Efby _ -> true | _ -> false + + let clock { eq_rhs = e } = + match e.e_desc with + | Emerge(_, (_, e) :: _) -> e.e_ck + | _ -> e.e_ck + + let head ck = + let rec headrec ck l = + match ck with + | Cbase | Cvar { contents = Cindex _ } -> l + | Con(ck, c, n) -> headrec ck (n :: l) + | Cvar { contents = Clink ck } -> headrec ck l + in + headrec ck [] + + (** Returns a list of memory vars (x in x = v fby e) + appearing in an equation. *) + let memory_vars ({ eq_lhs = _; eq_rhs = e } as eq) = + match e.e_desc with + | Efby(_, _) -> def [] eq + | _ -> [] +end + + +(* data-flow dependences. pre-dependences are discarded *) +module DataFlowDep = Dep.Make + (struct + type equation = eq + let read eq = Vars.read true eq + let def = Vars.def + let antidep = Vars.antidep + end) + +(* all dependences between variables *) +module AllDep = Dep.Make + (struct + type equation = eq + let read eq = Vars.read false eq + let def = Vars.def + let antidep eq = false + end) diff --git a/compiler/minils/sequential/cgen.ml b/compiler/minils/sequential/cgen.ml index 1fb3173..fd11b13 100644 --- a/compiler/minils/sequential/cgen.ml +++ b/compiler/minils/sequential/cgen.ml @@ -27,31 +27,26 @@ struct | Eno_unnamed_output | Ederef_not_pointer - let message loc kind = - begin match kind with - | Evar name -> - eprintf "%aCode generation : The variable name '%s' is unbound.\n" - output_location loc - name - | Enode name -> - eprintf "%aCode generation : The node name '%s' is unbound.\n" - output_location loc - name - | Eno_unnamed_output -> - eprintf "%aCode generation : Unnamed outputs are not supported.\n" - output_location loc - | Ederef_not_pointer -> - eprintf - "%aCode generation : Trying to deference a non pointer type.\n" - output_location loc - end; + let message loc kind = (match kind with + | Evar name -> + eprintf "%aCode generation : The variable name '%s' is unbound.\n" + output_location loc name + | Enode name -> + eprintf "%aCode generation : The node name '%s' is unbound.\n" + output_location loc name + | Eno_unnamed_output -> + eprintf "%aCode generation : Unnamed outputs are not supported.\n" + output_location loc + | Ederef_not_pointer -> + eprintf "%aCode generation : Trying to deference a non pointer type.\n" + output_location loc ); raise Misc.Error end let rec struct_name ty = match ty with - | Cty_id n -> n - | _ -> assert false + | Cty_id n -> n + | _ -> assert false let cname_of_name' name = match name with | Name n -> Name (cname_of_name n) @@ -151,7 +146,7 @@ let ctype_of_heptty ty = let cvarlist_of_ovarlist vl = let cvar_of_ovar vd = let ty = ctype_of_otype vd.v_type in - name vd.v_name, ty + name vd.v_ident, ty in List.map cvar_of_ovar vl @@ -165,7 +160,7 @@ let copname = function (** Translates an Obc var_dec to a tuple (name, cty). *) let cvar_of_vd vd = - name vd.v_name, ctype_of_otype vd.v_type + name vd.v_ident, ctype_of_otype vd.v_type (** If idx_list = [e1;..;ep], returns the lhs e[e1]...[ep] *) let rec csubscript_of_e_list e idx_list = @@ -212,9 +207,8 @@ let rec assoc_type_lhs lhs var_env = array_base_ctype ty [1] | Cderef lhs -> (match assoc_type_lhs lhs var_env with - | Cty_ptr ty -> ty - | _ -> Error.message no_location Error.Ederef_not_pointer - ) + | Cty_ptr ty -> ty + | _ -> Error.message no_location Error.Ederef_not_pointer) | Cfield(Cderef (Cvar "self"), x) -> assoc_type x var_env | Cfield(x, f) -> let ty = assoc_type_lhs x var_env in @@ -268,12 +262,12 @@ let rec cexpr_of_exp var_env exp = (** Constants, the easiest translation. *) | Const lit -> (match lit with - | Cint i -> Cconst (Ccint i) - | Cfloat f -> Cconst (Ccfloat f) - | Cconstr c -> Cconst (Ctag (shortname c)) - | Obc.Carray(n,c) -> - let cc = cexpr_of_exp var_env (Const c) in - Carraylit (repeat_list cc n) + | Cint i -> Cconst (Ccint i) + | Cfloat f -> Cconst (Ccfloat f) + | Cconstr c -> Cconst (Ctag (shortname c)) + | Obc.Carray(n,c) -> + let cc = cexpr_of_exp var_env (Const c) in + Carraylit (repeat_list cc n) ) (** Operators *) | Op(op, exps) -> @@ -551,7 +545,7 @@ let fun_def_of_step_fun name obj_env mem sf = let args_inputs_state = List.map (fun (arg_name,_) -> Clhs(Cvar(arg_name))) args in let addr_controllables = - let addrof { v_name = c_name } = + let addrof { v_ident = c_name } = Caddrof (Cvar (Ident.name c_name)) in List.map addrof c_list in let args_ctrlr = @@ -570,7 +564,7 @@ let fun_def_of_step_fun name obj_env mem sf = let epilogue = match sf.out with | [] -> [] | [vd] when Obc.is_scalar_type (List.hd sf.out) -> - [Creturn (Clhs (Cvar (Ident.name vd.v_name)))] + [Creturn (Clhs (Cvar (Ident.name vd.v_ident)))] | out -> [] in (** Substitute the return value variables with the corresponding diff --git a/compiler/minils/sequential/csubst.ml b/compiler/minils/sequential/csubst.ml index 2462bfe..dd42bbe 100644 --- a/compiler/minils/sequential/csubst.ml +++ b/compiler/minils/sequential/csubst.ml @@ -2,25 +2,24 @@ open C open Ident open Names -let rec subst_stm map stm = - match stm with - | Csexpr e -> Csexpr (subst_exp map e) - | Cskip -> Cskip - | Creturn e -> Creturn (subst_exp map e) - | Csblock cblock -> - Csblock (subst_block map cblock) - | Caffect (lhs, e) -> - Caffect(subst_lhs map lhs, subst_exp map e) - | Cif (e, truel, falsel) -> - Cif (subst_exp map e, subst_stm_list map truel, - subst_stm_list map falsel) - | Cswitch (e, l) -> - Cswitch (subst_exp map e, - List.map (fun (s, sl) -> s, subst_stm_list map sl) l) - | Cwhile (e, l) -> - Cwhile (subst_exp map e, subst_stm_list map l) - | Cfor (x, i1, i2, l) -> - Cfor (x, i1, i2, subst_stm_list map l) +let rec subst_stm map stm = match stm with + | Csexpr e -> Csexpr (subst_exp map e) + | Cskip -> Cskip + | Creturn e -> Creturn (subst_exp map e) + | Csblock cblock -> + Csblock (subst_block map cblock) + | Caffect (lhs, e) -> + Caffect(subst_lhs map lhs, subst_exp map e) + | Cif (e, truel, falsel) -> + Cif (subst_exp map e, subst_stm_list map truel, + subst_stm_list map falsel) + | Cswitch (e, l) -> + Cswitch (subst_exp map e + , List.map (fun (s, sl) -> s, subst_stm_list map sl) l) + | Cwhile (e, l) -> + Cwhile (subst_exp map e, subst_stm_list map l) + | Cfor (x, i1, i2, l) -> + Cfor (x, i1, i2, subst_stm_list map l) and subst_stm_list map = List.map (subst_stm map) @@ -28,10 +27,7 @@ and subst_stm_list map = and subst_lhs map lhs = match lhs with | Cvar n -> - if NamesEnv.mem n map then - NamesEnv.find n map - else - lhs + if NamesEnv.mem n map then NamesEnv.find n map else lhs | Cfield (lhs, s) -> Cfield (subst_lhs map lhs, s) | Carray (lhs, n) -> Carray (subst_lhs map lhs, n) | Cderef lhs -> Cderef (subst_lhs map lhs) @@ -59,8 +55,8 @@ let assoc_map_for_fun sf = NamesEnv.empty | out -> let fill_field map vd = - NamesEnv.add (name vd.Obc.v_name) - (Cfield (Cderef (Cvar "self"), name vd.Obc.v_name)) map - in - List.fold_left fill_field NamesEnv.empty out + NamesEnv.add (name vd.Obc.v_ident) + (Cfield (Cderef (Cvar "self"), name vd.Obc.v_ident)) map + in + List.fold_left fill_field NamesEnv.empty out diff --git a/compiler/minils/sequential/java.ml b/compiler/minils/sequential/java.ml index fa46b15..22afc79 100644 --- a/compiler/minils/sequential/java.ml +++ b/compiler/minils/sequential/java.ml @@ -428,7 +428,7 @@ let print_vd ff vd = fprintf ff "@["; print_name ff jty; fprintf ff " %s = %s;" - (jname_of_name (name vd.v_name)) + (jname_of_name (name vd.v_ident)) jdv; fprintf ff "@]" @@ -467,7 +467,7 @@ let print_ans_struct ff name fields = let print_vd' ff vd = fprintf ff "@["; print_type ff vd.v_type; - fprintf ff "@ %s" (jname_of_name (name vd.v_name)); + fprintf ff "@ %s" (jname_of_name (name vd.v_ident)); fprintf ff "@]" let rec print_in ff = function @@ -500,10 +500,10 @@ let print_step ff n s objs ts single = if single then fprintf ff "@ " else fprintf ff "%sAnswer step_ans = new %sAnswer();@ @ " n n; print_act ff s.bd objs - (List.map (fun vd -> vd.v_name) s.out) ts single; + (List.map (fun vd -> vd.v_ident) s.out) ts single; fprintf ff "@ @ return "; if single - then fprintf ff "%s" (jname_of_name (Ident.name (List.hd s.out).v_name)) + then fprintf ff "%s" (jname_of_name (Ident.name (List.hd s.out).v_ident)) else fprintf ff "step_ans"; fprintf ff ";@]@ }@ @]" diff --git a/compiler/minils/sequential/mls2obc.ml b/compiler/minils/sequential/mls2obc.ml index 7f0bb87..52ee98c 100644 --- a/compiler/minils/sequential/mls2obc.ml +++ b/compiler/minils/sequential/mls2obc.ml @@ -16,17 +16,15 @@ open Obc open Control open Static -let rec encode_name_params n = - function - | [] -> n - | p :: params -> encode_name_params (n ^ ("__" ^ (string_of_int p))) params - -let encode_longname_params n params = - match n with - | Name n -> Name (encode_name_params n params) - | Modname { qual = qual; id = id } -> - Modname { qual = qual; id = encode_name_params id params; } - +let rec encode_name_params n = function + | [] -> n + | p :: params -> encode_name_params (n ^ ("__" ^ (string_of_int p))) params + +let encode_longname_params n params = match n with + | Name n -> Name (encode_name_params n params) + | Modname { qual = qual; id = id } -> + Modname { qual = qual; id = encode_name_params id params; } + let is_op = function | Modname { qual = "Pervasives"; id = _ } -> true | _ -> false @@ -48,89 +46,84 @@ let array_elt_of_exp idx e = e1 <= n1 && .. && ep <= np *) let rec bound_check_expr idx_list bounds = match (idx_list, bounds) with - | ([ idx ], [ n ]) -> Op (op_from_string "<", [ idx; Const (Cint n) ]) - | (idx :: idx_list, n :: bounds) -> - Op (op_from_string "&", - [ Op (op_from_string "<", [ idx; Const (Cint n) ]); - bound_check_expr idx_list bounds ]) - | (_, _) -> assert false - -let rec translate_type const_env = - function - | Types.Tid id when id = Initial.pint -> Tint - | Types.Tid id when id = Initial.pfloat -> Tfloat - | Types.Tid id when id = Initial.pbool -> Tbool - | Types.Tid id -> Tid id - | Types.Tarray (ty, n) -> - Tarray (translate_type const_env ty, int_of_size_exp const_env n) - | Types.Tprod ty -> assert false - -let rec translate_const const_env = - function - | Minils.Cint v -> Cint v - | Minils.Cfloat v -> Cfloat v - | Minils.Cconstr c -> Cconstr c - | Minils.Carray (n, c) -> - Carray (int_of_size_exp const_env n, translate_const const_env c) - -let rec translate_pat map = - function - | Minils.Evarpat x -> [ var_from_name map x ] - | Minils.Etuplepat pat_list -> - List.fold_right (fun pat acc -> (translate_pat map pat) @ acc) - pat_list [] - + | ([ idx ], [ n ]) -> Op (op_from_string "<", [ idx; Const (Cint n) ]) + | (idx :: idx_list, n :: bounds) -> + Op (op_from_string "&", + [ Op (op_from_string "<", [ idx; Const (Cint n) ]); + bound_check_expr idx_list bounds ]) + | (_, _) -> assert false + +let rec translate_type const_env = function + | Types.Tid id when id = Initial.pint -> Tint + | Types.Tid id when id = Initial.pfloat -> Tfloat + | Types.Tid id when id = Initial.pbool -> Tbool + | Types.Tid id -> Tid id + | Types.Tarray (ty, n) -> + Tarray (translate_type const_env ty, int_of_size_exp const_env n) + | Types.Tprod ty -> assert false + +let rec translate_const const_env = function + | Minils.Cint v -> Cint v + | Minils.Cfloat v -> Cfloat v + | Minils.Cconstr c -> Cconstr c + | Minils.Carray (n, c) -> + Carray (int_of_size_exp const_env n, translate_const const_env c) + +let rec translate_pat map = function + | Minils.Evarpat x -> [ var_from_name map x ] + | Minils.Etuplepat pat_list -> + List.fold_right (fun pat acc -> (translate_pat map pat) @ acc) + pat_list [] + (* [translate e = c] *) -let rec - translate const_env map (m, si, j, s) (({ Minils.e_desc = desc } as e)) = +let rec translate const_env map (m, si, j, s) + (({ Minils.e_desc = desc } as e)) = match desc with - | Minils.Econst v -> Const (translate_const const_env v) - | Minils.Evar n -> Lhs (var_from_name map n) - | Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (SVar n))) - | Minils.Ecall ( { Minils.op_name = n; - Minils.op_kind = Minils.Eop }, e_list, _) -> - Op (n, List.map (translate const_env map (m, si, j, s)) e_list) - | Minils.Ewhen (e, _, _) -> translate const_env map (m, si, j, s) e - | Minils.Efield (e, field) -> - let e = translate const_env map (m, si, j, s) e - in Lhs (Field (lhs_of_exp e, field)) - | Minils.Estruct f_e_list -> - let type_name = - (match e.Minils.e_ty with - | Types.Tid name -> name - | _ -> assert false) in - let f_e_list = - List.map - (fun (f, e) -> (f, (translate const_env map (m, si, j, s) e))) - f_e_list - in Struct_lit (type_name, f_e_list) - (*Array operators*) - | Minils.Earray e_list -> - Array_lit (List.map (translate const_env map (m, si, j, s)) e_list) - | Minils.Earray_op (Minils.Eselect (idx, e)) -> - let e = translate const_env map (m, si, j, s) e in - let idx_list = - List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx - in - Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list) - | _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false + | Minils.Econst v -> Const (translate_const const_env v) + | Minils.Evar n -> Lhs (var_from_name map n) + | Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (SVar n))) + | Minils.Ecall ( { Minils.op_name = n; Minils.op_kind = Minils.Eop }, e_list, _) -> + Op (n, List.map (translate const_env map (m, si, j, s)) e_list) + | Minils.Ewhen (e, _, _) -> translate const_env map (m, si, j, s) e + | Minils.Efield (e, field) -> + let e = translate const_env map (m, si, j, s) e + in Lhs (Field (lhs_of_exp e, field)) + | Minils.Estruct f_e_list -> + let type_name = + (match e.Minils.e_ty with + | Types.Tid name -> name + | _ -> assert false) in + let f_e_list = + List.map + (fun (f, e) -> (f, (translate const_env map (m, si, j, s) e))) + f_e_list + in Struct_lit (type_name, f_e_list) + (*Array operators*) + | Minils.Earray e_list -> + Array_lit (List.map (translate const_env map (m, si, j, s)) e_list) + | Minils.Earray_op (Minils.Eselect (idx, e)) -> + let e = translate const_env map (m, si, j, s) e in + let idx_list = + List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx + in + Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list) + | _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false (* [translate pat act = si, j, d, s] *) and translate_act const_env map ((m, _, _, _) as context) pat - ({ Minils.e_desc = desc } as act) = + ({ Minils.e_desc = desc } as act) = match pat, desc with - | Minils.Etuplepat p_list, Minils.Etuple act_list -> - comp (List.map2 (translate_act const_env map context) p_list act_list) - | pat, Minils.Ewhen (e, _, _) -> - translate_act const_env map context pat e - | pat, Minils.Emerge (x, c_act_list) -> - let lhs = var_from_name map x - in - Case (Lhs lhs, - translate_c_act_list const_env map context pat c_act_list) - | Minils.Evarpat n, _ -> - Assgn (var_from_name map n, translate const_env map context act) - | _ -> (*Minils_printer.print_exp stdout act;*) assert false + | Minils.Etuplepat p_list, Minils.Etuple act_list -> + comp (List.map2 (translate_act const_env map context) p_list act_list) + | pat, Minils.Ewhen (e, _, _) -> + translate_act const_env map context pat e + | pat, Minils.Emerge (x, c_act_list) -> + let lhs = var_from_name map x in + Case (Lhs lhs + , translate_c_act_list const_env map context pat c_act_list) + | Minils.Evarpat n, _ -> + Assgn (var_from_name map n, translate const_env map context act) + | _ -> (*Minils_printer.print_exp stdout act;*) assert false and translate_c_act_list const_env map context pat c_act_list = List.map @@ -140,177 +133,165 @@ and translate_c_act_list const_env map context pat c_act_list = and comp s_list = List.fold_right (fun s rest -> Comp (s, rest)) s_list Nothing -let rec - translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } - (m, si, j, s) = - let { Minils.e_desc = desc; Minils.e_ty = ty; Minils.e_ck = ck } = e - in +let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } + (m, si, j, s) = + let { Minils.e_desc = desc; Minils.e_ty = ty; Minils.e_ck = ck } = e in match (pat, desc) with - | Minils.Evarpat n, Minils.Efby (opt_c, e) -> - let x = var_from_name map n in - let si = - (match opt_c with - | None -> si - | Some c -> - (Assgn (x, Const (translate_const const_env c))) :: si) in - let ty = translate_type const_env ty in - let m = (n, ty) :: m in - let action = - Assgn (var_from_name map n, - translate const_env map (m, si, j, s) e) - in - m, si, j, (control map ck action) :: s + | Minils.Evarpat n, Minils.Efby (opt_c, e) -> + let x = var_from_name map n in + let si = (match opt_c with + | None -> si + | Some c -> + (Assgn (x, Const (translate_const const_env c))) :: si) in + let ty = translate_type const_env ty in + let m = (n, ty) :: m in + let action = Assgn (var_from_name map n, + translate const_env map (m, si, j, s) e) + in + m, si, j, (control map ck action) :: s - | pat, Minils.Ecall ({ Minils.op_name = n; Minils.op_params = params; - Minils.op_kind = Minils.Enode }, + | pat, Minils.Ecall ({ Minils.op_name = n; Minils.op_params = params; + Minils.op_kind = Minils.Enode }, e_list, r) -> - let name_list = translate_pat map pat in - let c_list = - List.map (translate const_env map (m, si, j, s)) e_list in - let o = gen_symbol () in - let si = (Reinit o) :: si in - let params = List.map (int_of_size_exp const_env) params in - let j = (o, (encode_longname_params n params), 1) :: j in - let action = Step_ap (name_list, Context o, c_list) in - let s = - (match r with - | None -> (control map ck action) :: s - | Some r -> - let ra = - control map (Minils.Con (ck, Name "true", r)) (Reinit o) - in ra :: (control map ck action) :: s - ) - in - m, si, j, s + let name_list = translate_pat map pat in + let c_list = List.map (translate const_env map (m, si, j, s)) e_list in + let o = gen_symbol () in + let si = (Reinit o) :: si in + let params = List.map (int_of_size_exp const_env) params in + let j = (o, (encode_longname_params n params), 1) :: j in + let action = Step_ap (name_list, Context o, c_list) in + let s = (match r with + | None -> (control map ck action) :: s + | Some r -> + let ra = + control map (Minils.Con (ck, Name "true", r)) (Reinit o) in + ra :: (control map ck action) :: s ) in + m, si, j, s - | Minils.Etuplepat p_list, Minils.Etuple act_list -> - List.fold_right2 - (fun pat e -> - translate_eq const_env map - (Minils.mk_equation pat e)) - p_list act_list (m, si, j, s) + | Minils.Etuplepat p_list, Minils.Etuple act_list -> + List.fold_right2 + (fun pat e -> + translate_eq const_env map + (Minils.mk_equation pat e)) + p_list act_list (m, si, j, s) - | Minils.Evarpat x, Minils.Efield_update (f, e1, e2) -> - let x = var_from_name map x in - let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in - let action = - Assgn (Field (x, f), translate const_env map (m, si, j, s) e2) - in - m, si, j, (control map ck copy) :: (control map ck action) :: s + | Minils.Evarpat x, Minils.Efield_update (f, e1, e2) -> + let x = var_from_name map x in + let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in + let action = + Assgn (Field (x, f), translate const_env map (m, si, j, s) e2) + in + m, si, j, (control map ck copy) :: (control map ck action) :: s - | Minils.Evarpat x, - Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) -> - let idx1 = int_of_size_exp const_env idx1 in - let idx2 = int_of_size_exp const_env idx2 in - let cpt = Ident.fresh "i" in - let e = translate const_env map (m, si, j, s) e in - let idx = - Op (op_from_string "+", [ Lhs (Var cpt); Const (Cint idx1) ]) in - let action = - For (cpt, 0, (idx2 - idx1) + 1, - Assgn (Array (var_from_name map x, Lhs (Var cpt)), - Lhs (Array (lhs_of_exp e, idx)))) - in - m, si, j, (control map ck action) :: s + | Minils.Evarpat x, + Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) -> + let idx1 = int_of_size_exp const_env idx1 in + let idx2 = int_of_size_exp const_env idx2 in + let cpt = Ident.fresh "i" in + let e = translate const_env map (m, si, j, s) e in + let idx = + Op (op_from_string "+", [ Lhs (Var cpt); Const (Cint idx1) ]) in + let action = + For (cpt, 0, (idx2 - idx1) + 1, + Assgn (Array (var_from_name map x, Lhs (Var cpt)), + Lhs (Array (lhs_of_exp e, idx)))) + in + m, si, j, (control map ck action) :: s - | Minils.Evarpat x, - Minils.Earray_op (Minils.Eselect_dyn (idx, bounds, e1, e2)) -> - let x = var_from_name map x in - let e1 = translate const_env map (m, si, j, s) e1 in - let bounds = List.map (int_of_size_exp const_env) bounds in - let idx = List.map (translate const_env map (m, si, j, s)) idx in - let true_act = - Assgn (x, Lhs (lhs_of_idx_list (lhs_of_exp e1) idx)) in - let false_act = - Assgn (x, translate const_env map (m, si, j, s) e2) in - let cond = bound_check_expr idx bounds in - let action = - Case (cond, - [ ((Name "true"), true_act); ((Name "false"), false_act) ]) - in - m, si, j, (control map ck action) :: s + | Minils.Evarpat x, + Minils.Earray_op (Minils.Eselect_dyn (idx, bounds, e1, e2)) -> + let x = var_from_name map x in + let e1 = translate const_env map (m, si, j, s) e1 in + let bounds = List.map (int_of_size_exp const_env) bounds in + let idx = List.map (translate const_env map (m, si, j, s)) idx in + let true_act = + Assgn (x, Lhs (lhs_of_idx_list (lhs_of_exp e1) idx)) in + let false_act = + Assgn (x, translate const_env map (m, si, j, s) e2) in + let cond = bound_check_expr idx bounds in + let action = + Case (cond, + [ ((Name "true"), true_act); ((Name "false"), false_act) ]) + in + m, si, j, (control map ck action) :: s - | Minils.Evarpat x, - Minils.Earray_op (Minils.Eupdate (idx, e1, e2)) -> - let x = var_from_name map x in - let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in - let idx = - List.map (fun se -> Const (Cint (int_of_size_exp const_env se))) - idx in - let action = Assgn (lhs_of_idx_list x idx, - translate const_env map (m, si, j, s) e2) - in - m, si, j, (control map ck copy) :: (control map ck action) :: s + | Minils.Evarpat x, + Minils.Earray_op (Minils.Eupdate (idx, e1, e2)) -> + let x = var_from_name map x in + let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in + let idx = + List.map (fun se -> Const (Cint (int_of_size_exp const_env se))) + idx in + let action = Assgn (lhs_of_idx_list x idx, + translate const_env map (m, si, j, s) e2) + in + m, si, j, (control map ck copy) :: (control map ck action) :: s - | Minils.Evarpat x, - Minils.Earray_op (Minils.Erepeat (n, e)) -> - let cpt = Ident.fresh "i" in - let action = - For (cpt, 0, int_of_size_exp const_env n, - Assgn (Array (var_from_name map x, Lhs (Var cpt)), - translate const_env map (m, si, j, s) e)) - in - m, si, j, (control map ck action) :: s + | Minils.Evarpat x, + Minils.Earray_op (Minils.Erepeat (n, e)) -> + let cpt = Ident.fresh "i" in + let action = + For (cpt, 0, int_of_size_exp const_env n, + Assgn (Array (var_from_name map x, Lhs (Var cpt)), + translate const_env map (m, si, j, s) e)) + in + m, si, j, (control map ck action) :: s - | Minils.Evarpat x, - Minils.Earray_op (Minils.Econcat (e1, e2)) -> - let cpt1 = Ident.fresh "i" in - let cpt2 = Ident.fresh "i" in - let x = var_from_name map x - in - (match e1.Minils.e_ty, e2.Minils.e_ty with - | Types.Tarray (_, n1), Types.Tarray (_, n2) -> - let e1 = translate const_env map (m, si, j, s) e1 in - let e2 = translate const_env map (m, si, j, s) e2 in - let n1 = int_of_size_exp const_env n1 in - let n2 = int_of_size_exp const_env n2 in - let a1 = - For (cpt1, 0, n1, - Assgn (Array (x, Lhs (Var cpt1)), - Lhs (Array (lhs_of_exp e1, Lhs (Var cpt1))))) in - let idx = - Op (op_from_string "+", [ Const (Cint n1); Lhs (Var cpt2) ]) in - let a2 = - For (cpt2, 0, n2, - Assgn (Array (x, idx), - Lhs (Array (lhs_of_exp e2, Lhs (Var cpt2))))) - in - m, si, j, - (control map ck a1) :: (control map ck a2) :: s - | _ -> assert false - ) + | Minils.Evarpat x, + Minils.Earray_op (Minils.Econcat (e1, e2)) -> + let cpt1 = Ident.fresh "i" in + let cpt2 = Ident.fresh "i" in + let x = var_from_name map x in + (match e1.Minils.e_ty, e2.Minils.e_ty with + | Types.Tarray (_, n1), Types.Tarray (_, n2) -> + let e1 = translate const_env map (m, si, j, s) e1 in + let e2 = translate const_env map (m, si, j, s) e2 in + let n1 = int_of_size_exp const_env n1 in + let n2 = int_of_size_exp const_env n2 in + let a1 = + For (cpt1, 0, n1, + Assgn (Array (x, Lhs (Var cpt1)), + Lhs (Array (lhs_of_exp e1, Lhs (Var cpt1))))) in + let idx = + Op (op_from_string "+", [ Const (Cint n1); Lhs (Var cpt2) ]) in + let a2 = + For (cpt2, 0, n2, + Assgn (Array (x, idx), + Lhs (Array (lhs_of_exp e2, Lhs (Var cpt2))))) + in + m, si, j, (control map ck a1) :: (control map ck a2) :: s + | _ -> assert false ) - | pat, Minils.Earray_op ( - Minils.Eiterator (it, - { Minils.op_name = f; Minils.op_params = params; - Minils.op_kind = k }, - n, e_list, reset)) -> - let name_list = translate_pat map pat in - let c_list = - List.map (translate const_env map (m, si, j, s)) e_list in - let o = gen_symbol () in - let n = int_of_size_exp const_env n in - let si = - (match k with - | Minils.Eop -> si - | Minils.Enode -> (Reinit o) :: si) in - let params = List.map (int_of_size_exp const_env) params in - let j = (o, (encode_longname_params f params), n) :: j in - let x = Ident.fresh "i" in - let action = - translate_iterator const_env map it x name_list o n c_list in - let s = - (match reset with - | None -> (control map ck action) :: s - | Some r -> - (control map (Minils.Con (ck, Name "true", r)) (Reinit o)) :: - (control map ck action) :: s - ) - in (m, si, j, s) + | pat, Minils.Earray_op ( + Minils.Eiterator (it, + { Minils.op_name = f; Minils.op_params = params; + Minils.op_kind = k }, + n, e_list, reset)) -> + let name_list = translate_pat map pat in + let c_list = + List.map (translate const_env map (m, si, j, s)) e_list in + let o = gen_symbol () in + let n = int_of_size_exp const_env n in + let si = + (match k with + | Minils.Eop -> si + | Minils.Enode -> (Reinit o) :: si) in + let params = List.map (int_of_size_exp const_env) params in + let j = (o, (encode_longname_params f params), n) :: j in + let x = Ident.fresh "i" in + let action = + translate_iterator const_env map it x name_list o n c_list in + let s = + (match reset with + | None -> (control map ck action) :: s + | Some r -> + (control map (Minils.Con (ck, Name "true", r)) (Reinit o)) :: + (control map ck action) :: s ) + in (m, si, j, s) - | (pat, _) -> - let action = translate_act const_env map (m, si, j, s) pat e - in (m, si, j, ((control map ck action) :: s)) + | (pat, _) -> + let action = translate_act const_env map (m, si, j, s) pat e + in (m, si, j, ((control map ck action) :: s)) and translate_iterator const_env map it x name_list o n c_list = match it with @@ -345,7 +326,7 @@ let translate_eq_list const_env map act_list = List.fold_right (translate_eq const_env map) act_list ([], [], [], []) let remove m d_list = - List.filter (fun { Minils.v_name = n } -> not (List.mem_assoc n m)) d_list + List.filter (fun { Minils.v_ident = n } -> not (List.mem_assoc n m)) d_list let var_decl l = List.map (fun (x, t) -> mk_var_dec x t) l @@ -353,7 +334,7 @@ let var_decl l = let obj_decl l = List.map (fun (x, t, i) -> { obj = x; cls = t; size = i; }) l let translate_var_dec const_env map l = - let one_var { Minils.v_name = x; Minils.v_type = t } = + let one_var { Minils.v_ident = x; Minils.v_type = t } = mk_var_dec x (translate_type const_env t) in List.map one_var l @@ -380,22 +361,22 @@ let translate_contract const_env map = let subst_map inputs outputs locals mems = (* Create a map that simply maps each var to itself *) let m = - List.fold_left (fun m { Minils.v_name = x } -> Env.add x (Var x) m) + List.fold_left (fun m { Minils.v_ident = x } -> Env.add x (Var x) m) Env.empty (inputs @ outputs @ locals) in List.fold_left (fun m x -> Env.add x (Mem x) m) m mems let translate_node_aux const_env - { - Minils.n_name = f; - Minils.n_input = i_list; - Minils.n_output = o_list; - Minils.n_local = d_list; - Minils.n_equs = eq_list; - Minils.n_contract = contract; - Minils.n_params = params - } = - let mem_vars = List.flatten (List.map Minils.Vars.memory_vars eq_list) in + { + Minils.n_name = f; + Minils.n_input = i_list; + Minils.n_output = o_list; + Minils.n_local = d_list; + Minils.n_equs = eq_list; + Minils.n_contract = contract; + Minils.n_params = params + } = + let mem_vars = List.flatten (List.map Mls_utils.Vars.memory_vars eq_list) in let subst_map = subst_map i_list o_list d_list mem_vars in let (m, si, j, s_list) = translate_eq_list const_env subst_map eq_list in let (m', si', j', s_list', d_list', c_list) = diff --git a/compiler/minils/sequential/obc.ml b/compiler/minils/sequential/obc.ml index 2e8aa4a..7243ee7 100644 --- a/compiler/minils/sequential/obc.ml +++ b/compiler/minils/sequential/obc.ml @@ -70,7 +70,7 @@ type act = | Nothing type var_dec = - { v_name : var_name; + { v_ident : var_name; v_type : ty; } type obj_dec = @@ -103,15 +103,14 @@ type program = o_defs : class_def list } let mk_var_dec name ty = - { v_name = name; v_type = ty } + { v_ident = name; v_type = ty } (** [is_scalar_type vd] returns whether the type corresponding to this variable declaration is scalar (ie a type that can be returned by a C function). *) -let is_scalar_type vd = - match vd.v_type with - | Tint | Tfloat | Tbool -> true - | _ -> false +let is_scalar_type vd = match vd.v_type with + | Tint | Tfloat | Tbool -> true + | _ -> false let rec var_name x = match x with @@ -124,14 +123,14 @@ let rec var_name x = a list of var_dec. *) let rec vd_mem n = function | [] -> false - | vd::l -> vd.v_name = n or (vd_mem n l) + | vd::l -> vd.v_ident = n or (vd_mem n l) (** Returns the var_dec object corresponding to the name n in a list of var_dec. *) let rec vd_find n = function | [] -> Format.printf "Not found var %s\n" (name n); raise Not_found | vd::l -> - if vd.v_name = n then vd else vd_find n l + if vd.v_ident = n then vd else vd_find n l let lhs_of_exp = function | Lhs l -> l @@ -153,7 +152,7 @@ struct let print_vd ff vd = fprintf ff "@["; - print_ident ff vd.v_name; + print_ident ff vd.v_ident; fprintf ff ": "; print_type ff vd.v_type; fprintf ff "@]" diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index ebb9ec5..6280d0d 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -13,6 +13,7 @@ open Names open Ident open Signature open Minils +open Mls_utils let ctrue = Name "true" and cfalse = Name "false" diff --git a/compiler/minils/transformations/schedule.ml b/compiler/minils/transformations/schedule.ml index ef07556..5368ad1 100644 --- a/compiler/minils/transformations/schedule.ml +++ b/compiler/minils/transformations/schedule.ml @@ -8,10 +8,10 @@ (**************************************************************************) (* scheduling of equations *) -(* $Id$ *) open Misc open Minils +open Mls_utils open Graph open Dep diff --git a/compiler/myocamlbuild.ml b/compiler/myocamlbuild.ml index cc4da2a..bf2623e 100644 --- a/compiler/myocamlbuild.ml +++ b/compiler/myocamlbuild.ml @@ -15,7 +15,10 @@ let df = function dep ["ocaml"; "ocamldep"; "use_preproc"] ["preproc.cmo"]; (* LablGTK use for graphical simulator *) - ocaml_lib ~extern:true ~dir:"+lablgtk2" "lablgtk" + ocaml_lib ~extern:true ~dir:"+lablgtk2" "lablgtk"; + + flag ["ocaml"; "parser" ; "menhir" ; "use_menhir"] (S[A"--explain"]); + | _ -> () let _ = dispatch df