Itfusion moved to heptagon
This commit is contained in:
parent
cbf92beba2
commit
611c94bbbd
|
@ -232,6 +232,19 @@ let mk_signature name ins outs stateful params loc =
|
||||||
sig_params = params;
|
sig_params = params;
|
||||||
sig_loc = loc }
|
sig_loc = loc }
|
||||||
|
|
||||||
|
let mk_node
|
||||||
|
?(input = []) ?(output = []) ?(contract = None) ?(local = [])
|
||||||
|
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
|
||||||
|
name block =
|
||||||
|
{ n_name = name;
|
||||||
|
n_stateful = stateful;
|
||||||
|
n_input = input;
|
||||||
|
n_output = output;
|
||||||
|
n_contract = contract;
|
||||||
|
n_block = block;
|
||||||
|
n_loc = loc;
|
||||||
|
n_params = param;
|
||||||
|
n_params_constraints = constraints }
|
||||||
|
|
||||||
(** @return the set of variables defined in [pat]. *)
|
(** @return the set of variables defined in [pat]. *)
|
||||||
let vars_pat pat =
|
let vars_pat pat =
|
||||||
|
|
|
@ -2,10 +2,15 @@ open Signature
|
||||||
open Modules
|
open Modules
|
||||||
open Names
|
open Names
|
||||||
open Static
|
open Static
|
||||||
open Mls_mapfold
|
open Hept_mapfold
|
||||||
open Minils
|
open Heptagon
|
||||||
(* Iterator fusion *)
|
(* Iterator fusion *)
|
||||||
|
|
||||||
|
let is_stateful app =
|
||||||
|
match app.a_op with
|
||||||
|
| Enode _ -> true
|
||||||
|
| _ -> false
|
||||||
|
|
||||||
(* Functions to temporarily store anonymous nodes*)
|
(* Functions to temporarily store anonymous nodes*)
|
||||||
let mk_fresh_node_name () = Modules.fresh_value "itfusion" "temp"
|
let mk_fresh_node_name () = Modules.fresh_value "itfusion" "temp"
|
||||||
|
|
||||||
|
@ -21,8 +26,8 @@ let anon_nodes = ref QualEnv.empty
|
||||||
|
|
||||||
let add_anon_node inputs outputs locals eqs =
|
let add_anon_node inputs outputs locals eqs =
|
||||||
let n = mk_fresh_node_name () in
|
let n = mk_fresh_node_name () in
|
||||||
let nd = mk_node ~input:inputs ~output:outputs ~local:locals
|
let b = mk_block ~locals:locals eqs in
|
||||||
~eq:eqs n in
|
let nd = mk_node ~input:inputs ~output:outputs ~local:locals n b in
|
||||||
anon_nodes := QualEnv.add n nd !anon_nodes;
|
anon_nodes := QualEnv.add n nd !anon_nodes;
|
||||||
n
|
n
|
||||||
|
|
||||||
|
@ -46,9 +51,9 @@ match l with
|
||||||
| _ -> Etuplepat (List.map (fun vd -> Evarpat vd.v_ident) l)
|
| _ -> Etuplepat (List.map (fun vd -> Evarpat vd.v_ident) l)
|
||||||
|
|
||||||
let tuple_of_vd_list l =
|
let tuple_of_vd_list l =
|
||||||
let el = List.map (fun vd -> mk_exp ~ty:vd.v_type (Evar vd.v_ident)) l in
|
let el = List.map (fun vd -> mk_exp (Evar vd.v_ident) vd.v_type) l in
|
||||||
let ty = Types.prod (List.map (fun vd -> vd.v_type) l) in
|
let ty = Types.prod (List.map (fun vd -> vd.v_type) l) in
|
||||||
mk_exp ~ty:ty (Eapp (mk_app Etuple, el, None))
|
mk_exp (Eapp (mk_app Etuple, el, None)) ty
|
||||||
|
|
||||||
let vd_of_arg ad =
|
let vd_of_arg ad =
|
||||||
mk_var_dec (fresh_vd_of_arg ad) ad.a_type
|
mk_var_dec (fresh_vd_of_arg ad) ad.a_type
|
||||||
|
@ -70,24 +75,25 @@ let get_node_inp_outp app = match app.a_op with
|
||||||
|
|
||||||
(** Creates the equation to call the node [app].
|
(** Creates the equation to call the node [app].
|
||||||
@return the list of new inputs required by the call, the expression
|
@return the list of new inputs required by the call, the expression
|
||||||
used to retrieve the resul of the call and [acc_eq_list] with the
|
used to retrieve the result of the call and [acc_eq_list] with the
|
||||||
added equations. *)
|
added equations. *)
|
||||||
let mk_call app acc_eq_list =
|
let mk_call app acc_eq_list =
|
||||||
let new_inp, new_outp = get_node_inp_outp app in
|
let new_inp, new_outp = get_node_inp_outp app in
|
||||||
let args = List.map (fun vd -> mk_exp ~ty:vd.v_type
|
let args = List.map (fun vd -> mk_exp
|
||||||
(Evar vd.v_ident)) new_inp in
|
(Evar vd.v_ident) vd.v_type) new_inp in
|
||||||
let out_ty = Types.prod (List.map (fun vd -> vd.v_type) new_outp) in
|
let out_ty = Types.prod (List.map (fun vd -> vd.v_type) new_outp) in
|
||||||
let e = mk_exp ~ty:out_ty (Eapp (app, args, None)) in
|
let e = mk_exp (Eapp (app, args, None)) out_ty in
|
||||||
match List.length new_outp with
|
match List.length new_outp with
|
||||||
| 1 -> new_inp, e, acc_eq_list
|
| 1 -> new_inp, e, acc_eq_list
|
||||||
| _ ->
|
| _ ->
|
||||||
(*more than one output, we need to create a new equation *)
|
(*more than one output, we need to create a new equation *)
|
||||||
let eq = mk_equation (pat_of_vd_list new_outp) e in
|
let eq = mk_equation ~stateful:(is_stateful app)
|
||||||
|
(Eeq(pat_of_vd_list new_outp, e)) in
|
||||||
let e = tuple_of_vd_list new_outp in
|
let e = tuple_of_vd_list new_outp in
|
||||||
new_inp, e, eq::acc_eq_list
|
new_inp, e, eq::acc_eq_list
|
||||||
|
|
||||||
let edesc funs acc ed =
|
let edesc funs acc ed =
|
||||||
let ed, acc = Mls_mapfold.edesc funs acc ed in
|
let ed, acc = Hept_mapfold.edesc funs acc ed in
|
||||||
match ed with
|
match ed with
|
||||||
| Eiterator(Imap, f, n, [], e_list, r) ->
|
| Eiterator(Imap, f, n, [], e_list, r) ->
|
||||||
(** @return the list of inputs of the anonymous function,
|
(** @return the list of inputs of the anonymous function,
|
||||||
|
@ -107,7 +113,7 @@ let edesc funs acc ed =
|
||||||
new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true
|
new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true
|
||||||
| _ ->
|
| _ ->
|
||||||
let vd = mk_var_dec (fresh_var ()) e.e_ty in
|
let vd = mk_var_dec (fresh_var ()) e.e_ty in
|
||||||
let x = mk_exp ~ty:vd.v_type (Evar vd.v_ident) in
|
let x = mk_exp (Evar vd.v_ident) vd.v_type in
|
||||||
vd::inp, acc_eq_list, x::largs, e::args, b
|
vd::inp, acc_eq_list, x::largs, e::args, b
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -118,10 +124,12 @@ let edesc funs acc ed =
|
||||||
(* create the call to f in the lambda fun *)
|
(* create the call to f in the lambda fun *)
|
||||||
let _, outp = get_node_inp_outp f in
|
let _, outp = get_node_inp_outp f in
|
||||||
let f_out_type = Types.prod (List.map (fun v -> v.v_type) outp) in
|
let f_out_type = Types.prod (List.map (fun v -> v.v_type) outp) in
|
||||||
let call = mk_exp ~ty:f_out_type (Eapp(f, largs, None)) in
|
let call = mk_exp (Eapp(f, largs, None)) f_out_type in
|
||||||
let eq = mk_equation (pat_of_vd_list outp) call in
|
let eq = mk_equation ~stateful:(is_stateful f)
|
||||||
|
(Eeq(pat_of_vd_list outp, call)) in
|
||||||
(* create the lambda *)
|
(* create the lambda *)
|
||||||
let anon = mk_app (Enode (add_anon_node inp outp [] (eq::acc_eq_list))) in
|
let anon = mk_app
|
||||||
|
(Enode (add_anon_node inp outp [] (eq::acc_eq_list))) in
|
||||||
Eiterator(Imap, anon, n, [], args, r), acc)
|
Eiterator(Imap, anon, n, [], args, r), acc)
|
||||||
else
|
else
|
||||||
ed, acc
|
ed, acc
|
||||||
|
@ -131,6 +139,6 @@ let edesc funs acc ed =
|
||||||
|
|
||||||
|
|
||||||
let program p =
|
let program p =
|
||||||
let funs = { Mls_mapfold.defaults with edesc = edesc } in
|
let funs = { Hept_mapfold.defaults with edesc = edesc } in
|
||||||
let p, _ = Mls_mapfold.program_it funs false p in
|
let p, _ = Hept_mapfold.program_it funs false p in
|
||||||
p
|
p
|
|
@ -10,8 +10,8 @@ open Misc
|
||||||
open Initial
|
open Initial
|
||||||
open Names
|
open Names
|
||||||
open Idents
|
open Idents
|
||||||
open Signature
|
|
||||||
open Heptagon
|
open Heptagon
|
||||||
|
open Hept_mapfold
|
||||||
open Types
|
open Types
|
||||||
open Clocks
|
open Clocks
|
||||||
|
|
||||||
|
@ -50,6 +50,8 @@ let flatten_e_list l =
|
||||||
in
|
in
|
||||||
List.flatten (List.map flatten l)
|
List.flatten (List.map flatten l)
|
||||||
|
|
||||||
|
(** Creates a new equation x = e, adds x to d_list
|
||||||
|
and the equation to eq_list. *)
|
||||||
let equation (d_list, eq_list) e =
|
let equation (d_list, eq_list) e =
|
||||||
let add_one_var ty d_list =
|
let add_one_var ty d_list =
|
||||||
let n = Idents.gen_var "normalize" "v" in
|
let n = Idents.gen_var "normalize" "v" in
|
||||||
|
@ -93,6 +95,7 @@ let const e c =
|
||||||
|
|
||||||
type kind = ExtValue | Any
|
type kind = ExtValue | Any
|
||||||
|
|
||||||
|
(** Creates an equation and add it to the context if necessary. *)
|
||||||
let add context expected_kind ({ e_desc = de } as e) =
|
let add context expected_kind ({ e_desc = de } as e) =
|
||||||
let up = match de, expected_kind with
|
let up = match de, expected_kind with
|
||||||
| (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _
|
| (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _
|
||||||
|
|
|
@ -163,13 +163,12 @@ let mk_equation ?(loc = no_location) pat exp =
|
||||||
let mk_node
|
let mk_node
|
||||||
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
|
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
|
||||||
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
|
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
|
||||||
?(pinst = ([],[])) name =
|
name =
|
||||||
{ n_name = name;
|
{ n_name = name;
|
||||||
n_stateful = stateful;
|
n_stateful = stateful;
|
||||||
n_input = input;
|
n_input = input;
|
||||||
n_output = output;
|
n_output = output;
|
||||||
n_contract = contract;
|
n_contract = contract;
|
||||||
(* n_controller_call = pinst;*)
|
|
||||||
n_local = local;
|
n_local = local;
|
||||||
n_equs = eq;
|
n_equs = eq;
|
||||||
n_loc = loc;
|
n_loc = loc;
|
||||||
|
|
Loading…
Reference in a new issue