Indentation fixes!
This commit is contained in:
parent
ef55c8f9fd
commit
f35bf95458
9 changed files with 446 additions and 437 deletions
|
@ -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
|
||||
|
@ -40,7 +40,7 @@ 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 print_param ff p = Names.print_name ff p.p_name
|
||||
|
||||
|
|
|
@ -117,13 +117,13 @@ let rec cand nc1 nc2 =
|
|||
| nc1, Aor(nc2, nc22) -> Aor(cand nc1 nc2, cand nc1 nc22)
|
||||
| Aac(ac1), Aac(ac2) -> Aac(Aand(ac1, ac2))
|
||||
|
||||
let rec ctuple l =
|
||||
let rec ctuple l =
|
||||
let rec conv = function
|
||||
| Cwrite(n) -> Awrite(n)
|
||||
| Cread(n) -> Aread(n)
|
||||
| Clastread(n) -> Alastread(n)
|
||||
| Ctuple(l) -> Atuple (ctuple l)
|
||||
| Cand (c1, c2) -> Aand (conv c1, conv c2)
|
||||
| Cand (c1, c2) -> Aand (conv c1, conv c2)
|
||||
| Cseq _ -> Format.printf "Unexpected seq\n"; assert false
|
||||
| Cor _ -> Format.printf "Unexpected or\n"; assert false
|
||||
| _ -> assert false
|
||||
|
@ -214,26 +214,26 @@ let build ac =
|
|||
| Aseq(ac1, ac2) ->
|
||||
let top1, bot1 = make_graph ac1 in
|
||||
let top2, bot2 = make_graph ac2 in
|
||||
(* add extra dependences *)
|
||||
List.iter
|
||||
(fun top -> List.iter (fun bot -> add_depends top bot) bot1)
|
||||
top2;
|
||||
top1 @ top2, bot1 @ bot2
|
||||
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
|
||||
| Aread(n) -> let g = make ac in attach g n; [g], [g]
|
||||
| Atuple(l) ->
|
||||
let make_graph_tuple ac =
|
||||
(* add extra dependences *)
|
||||
List.iter
|
||||
(fun top -> List.iter (fun bot -> add_depends top bot) bot1)
|
||||
top2;
|
||||
top1 @ top2, bot1 @ bot2
|
||||
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
|
||||
| Aread(n) -> let g = make ac in attach g n; [g], [g]
|
||||
| Atuple(l) ->
|
||||
let make_graph_tuple ac =
|
||||
match ac with
|
||||
| Aand _ | Atuple _ -> make_graph ac
|
||||
| _ -> [], []
|
||||
in
|
||||
let g = node_for_ac ac in
|
||||
List.iter (add_dependence g) l;
|
||||
let top_l, bot_l = List.split (List.map make_graph_tuple l) in
|
||||
let top_l = List.flatten top_l in
|
||||
let bot_l = List.flatten bot_l in
|
||||
g::top_l, g::bot_l
|
||||
| _ -> [], []
|
||||
let g = node_for_ac ac in
|
||||
List.iter (add_dependence g) l;
|
||||
let top_l, bot_l = List.split (List.map make_graph_tuple l) in
|
||||
let top_l = List.flatten top_l in
|
||||
let bot_l = List.flatten bot_l in
|
||||
g::top_l, g::bot_l
|
||||
| _ -> [], []
|
||||
|
||||
in
|
||||
let top_list, bot_list = make_graph ac in
|
||||
|
|
|
@ -117,13 +117,13 @@ 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)
|
||||
Error.message e.e_loc (Error.Econst_var n)
|
||||
else
|
||||
SVar n
|
||||
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)
|
||||
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
|
||||
|
@ -157,8 +157,10 @@ 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
|
||||
|
@ -171,13 +173,14 @@ and translate_desc loc const_env env = function
|
|||
| Econst c -> Heptagon.Econst (translate_const c)
|
||||
| Evar x ->
|
||||
if Rename.mem x env then (* defined var *)
|
||||
Heptagon.Evar (Rename.name loc env x)
|
||||
Heptagon.Evar (Rename.name loc env x)
|
||||
else if NamesEnv.mem x const_env then (* defined as const var *)
|
||||
Heptagon.Econstvar x
|
||||
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)
|
||||
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)
|
||||
| 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
|
||||
|
@ -190,9 +193,11 @@ 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)
|
||||
|
@ -214,7 +219,7 @@ and translate_eq_desc loc const_env env = function
|
|||
| Epresent (present_handlers, b) ->
|
||||
Heptagon.Epresent
|
||||
(List.map (translate_present_handler const_env env) present_handlers
|
||||
, fst (translate_block const_env env b))
|
||||
, fst (translate_block const_env env b))
|
||||
| Eautomaton state_handlers ->
|
||||
Heptagon.Eautomaton (List.map (translate_state_handler const_env env)
|
||||
state_handlers)
|
||||
|
|
|
@ -22,17 +22,17 @@ 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\
|
||||
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
|
||||
print_exp exp
|
||||
print_clock actual_ct
|
||||
print_clock expected_ct;
|
||||
raise Error
|
||||
|
||||
exception Unify
|
||||
|
||||
|
||||
|
||||
|
||||
let index = ref 0
|
||||
|
||||
let gen_index () = (incr index; !index)
|
||||
|
@ -41,33 +41,33 @@ 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
|
||||
|
@ -76,29 +76,29 @@ and unify_ck 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
|
||||
|
@ -117,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
|
||||
|
@ -184,31 +184,31 @@ 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 -> err_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)
|
||||
|
||||
| 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
|
||||
(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 =
|
||||
|
@ -219,41 +219,41 @@ let sbuild h dec base =
|
|||
|
||||
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;
|
||||
n_input = i_list;
|
||||
n_output = o_list;
|
||||
n_contract = contract;
|
||||
n_local = l_list;
|
||||
n_equs = eq_list
|
||||
} as node) =
|
||||
n_input = i_list;
|
||||
n_output = o_list;
|
||||
n_contract = contract;
|
||||
n_local = l_list;
|
||||
n_equs = eq_list
|
||||
} 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
|
||||
(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_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 })
|
||||
|
||||
(*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 })
|
||||
|
||||
let program (({ p_nodes = p_node_list } as p)) =
|
||||
{ (p) with p_nodes = List.map typing_node p_node_list; }
|
||||
|
||||
|
|
|
@ -43,9 +43,11 @@ 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
|
||||
|
@ -65,11 +67,10 @@ 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
|
||||
|
@ -154,24 +155,24 @@ 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 mk_op ?(op_params = []) ?(op_kind = Enode) lname =
|
||||
{ op_name = lname; op_params = op_params; op_kind = op_kind }
|
||||
|
||||
{ op_name = lname; op_params = op_params; op_kind = op_kind }
|
||||
|
||||
let void = mk_exp (Etuple [])
|
||||
|
||||
|
|
|
@ -14,19 +14,19 @@ 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
|
||||
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
|
||||
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 =
|
||||
let rec bounds_list ty =
|
||||
match ty with
|
||||
| Tarray(ty, n) -> n::(bounds_list ty)
|
||||
| _ -> []
|
||||
|
@ -35,10 +35,10 @@ let rec bounds_list ty =
|
|||
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 ->
|
||||
| vd::l ->
|
||||
if vd.v_ident = n then vd else vd_find n l
|
||||
|
||||
(** @return whether an object of name [n] belongs to
|
||||
(** @return whether an object of name [n] belongs to
|
||||
a list of [var_dec]. *)
|
||||
let rec vd_mem n = function
|
||||
| [] -> false
|
||||
|
@ -47,15 +47,15 @@ let rec vd_mem n = function
|
|||
(** @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)
|
||||
(try
|
||||
ignore (Modules.find_struct n); true
|
||||
with
|
||||
Not_found -> false)
|
||||
| _ -> false
|
||||
|
||||
module Vars =
|
||||
struct
|
||||
let add x acc =
|
||||
let add x acc =
|
||||
if List.mem x acc then acc else x :: acc
|
||||
|
||||
let rec vars_pat acc = function
|
||||
|
@ -73,48 +73,48 @@ struct
|
|||
| 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
|
||||
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
|
||||
read is_left acc e
|
||||
| Etuple(e_list) -> List.fold_left (read is_left) acc e_list
|
||||
| Ecall(_, e_list, None) ->
|
||||
| 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
|
||||
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
|
||||
| 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
|
||||
vars_ck acc e.e_ck
|
||||
|
||||
and read_array_op is_left acc = function
|
||||
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) ->
|
||||
| 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
|
||||
List.fold_left (read is_left) acc e_list
|
||||
|
||||
let rec remove x = function
|
||||
| [] -> []
|
||||
|
@ -143,11 +143,11 @@ struct
|
|||
match ck with
|
||||
| Cbase | Cvar { contents = Cindex _ } -> l
|
||||
| Con(ck, c, n) -> headrec ck (n :: l)
|
||||
| Cvar { contents = Clink ck } -> headrec ck l
|
||||
| Cvar { contents = Clink ck } -> headrec ck l
|
||||
in
|
||||
headrec ck []
|
||||
headrec ck []
|
||||
|
||||
(** Returns a list of memory vars (x in x = v fby e)
|
||||
(** 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
|
||||
|
|
|
@ -11,11 +11,11 @@ let rec subst_stm map stm = match stm with
|
|||
| 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,
|
||||
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)
|
||||
, 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) ->
|
||||
|
@ -57,6 +57,6 @@ let assoc_map_for_fun sf =
|
|||
let fill_field map vd =
|
||||
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
|
||||
in
|
||||
List.fold_left fill_field NamesEnv.empty out
|
||||
|
||||
|
|
|
@ -19,12 +19,12 @@ 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 is_op = function
|
||||
| Modname { qual = "Pervasives"; id = _ } -> true | _ -> false
|
||||
|
||||
|
@ -46,13 +46,13 @@ 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
|
||||
|
||||
| ([ 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
|
||||
|
@ -61,69 +61,70 @@ let rec translate_type const_env = function
|
|||
| 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)
|
||||
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)) =
|
||||
(({ 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
|
||||
|
@ -134,164 +135,166 @@ 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) =
|
||||
(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
|
||||
|
@ -367,15 +370,15 @@ let subst_map inputs outputs locals mems =
|
|||
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
|
||||
} =
|
||||
{
|
||||
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
|
||||
|
|
|
@ -16,9 +16,9 @@ let df = function
|
|||
|
||||
(* LablGTK use for graphical simulator *)
|
||||
ocaml_lib ~extern:true ~dir:"+lablgtk2" "lablgtk";
|
||||
|
||||
|
||||
flag ["ocaml"; "parser" ; "menhir" ; "use_menhir"] (S[A"--explain"]);
|
||||
|
||||
|
||||
| _ -> ()
|
||||
|
||||
let _ = dispatch df
|
||||
|
|
Loading…
Reference in a new issue