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

Gros blop pour que Mlsc compile.

Browse Source 
-* Séparation du fichier minils avec création de mls_utils
-* Lexer et Parser qui fonctionnent (pas complets encore)
-* Use of menhir with --explain pour debug du parser
-* Quelques refactoring (ident/name...)
master
Léonard Gérard 14 years ago committed by Léonard Gérard
parent 3a80061392
commit 0f2d046d59
21 changed files with 782 additions and 825 deletions
Show Stats Download Patch File Download Diff File

1
compiler/_tags
Unescape Escape View File

@ -2,3 +2,4 @@
<**/*.ml>: debug, dtypes
<preproc.ml>: camlp4of, use_camlp4
<**/*.{byte,native}>: use_unix, use_str, debug
true: use_menhir

16
compiler/global/signature.ml
Unescape Escape View File

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

16
compiler/heptagon/main/heptcheck.ml
Unescape Escape View File

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

64
compiler/heptagon/parsing/scoping.ml
Unescape Escape View File

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

1
compiler/main/hept2mls.ml
Unescape Escape View File

@ -19,6 +19,7 @@ open Format
open Printf
open Minils
open Mls_utils
open Signature
module Error =

18
compiler/main/heptc.ml
Unescape Escape View File

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

279
compiler/minils/analysis/clocking.ml
Unescape Escape View File

@ -17,23 +17,22 @@ open Types
open Location
open Printf
type error = | Etypeclash of ct * ct
exception TypingError of error
(** Error Kind *)
type err_kind = | Etypeclash of ct * ct
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)
let typing_node (({
n_name = f;
| 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;
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; }

2
compiler/minils/analysis/init.ml
Unescape Escape View File

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

212
compiler/minils/minils.ml
Unescape Escape View File

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

12
compiler/minils/mls_lexer.mll
Unescape Escape View File

@ -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']+

145
compiler/minils/mls_parser.mly
Unescape Escape View File

@ -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 <string> PREFIX
%token <string> INFIX0
%token <string> 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)) }
%inline infix:
| 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)) }
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 */

2
compiler/minils/mls_printer.ml
Unescape Escape View File

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

175
compiler/minils/mls_utils.ml
Unescape Escape View File

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

60
compiler/minils/sequential/cgen.ml
Unescape Escape View File

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

50
compiler/minils/sequential/csubst.ml
Unescape Escape View File

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

8
compiler/minils/sequential/java.ml
Unescape Escape View File

@ -428,7 +428,7 @@ let print_vd ff vd =
fprintf ff "@[<v>";
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 ";@]@ }@ @]"

521
compiler/minils/sequential/mls2obc.ml
Unescape Escape View File

@ -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
| pat, Minils.Ecall ({ Minils.op_name = n; Minils.op_params = params;
Minils.op_kind = Minils.Enode },
| 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 },
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
| 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.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.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.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, _) ->
let action = translate_act const_env map (m, si, j, s) pat e
in (m, si, j, ((control map ck action) :: 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.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_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.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 )
| 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))
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) =

17
compiler/minils/sequential/obc.ml
Unescape Escape View File

@ -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 "@[<v>";
print_ident ff vd.v_name;
print_ident ff vd.v_ident;
fprintf ff ": ";
print_type ff vd.v_type;
fprintf ff "@]"

1
compiler/minils/transformations/normalize.ml
Unescape Escape View File

@ -13,6 +13,7 @@ open Names
open Ident
open Signature
open Minils
open Mls_utils
let ctrue = Name "true"
and cfalse = Name "false"

2
compiler/minils/transformations/schedule.ml
Unescape Escape View File

@ -8,10 +8,10 @@
(**************************************************************************)
(* scheduling of equations *)
(* $Id$ *)
open Misc
open Minils
open Mls_utils
open Graph
open Dep

5
compiler/myocamlbuild.ml
Unescape Escape View File

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

Write Preview
Loading…
Cancel
Save