From fcf472a68d948c7f7f556c869f0191e67f149832 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Tue, 5 Mar 2013 18:15:19 +0100 Subject: [PATCH] Add preliminary support for a Soc interpreter. Can be tried unsing the -exec option. currently only working with trivial programs manipulating equalities (wires) and predef operators (no pre, ->, arrays, and node calls). --- Makefile | 8 +- src/compile.ml | 44 ++--- src/global.ml | 5 +- src/lic.ml | 9 +- src/lic2soc.ml | 323 ++++++++++++++++++++++-------------- src/lic2soc.mli | 5 +- src/licTab.ml | 6 +- src/mainArgs.ml | 6 + src/soc.ml | 57 +++++-- src/socExecEvalPredef.ml | 254 ++++++++++++++++++++++++++++ src/socExecEvalPredef.mli | 11 ++ src/socExecValue.ml | 76 +++++++++ src/socExecValue.mli | 21 +++ src/socPredef.ml | 340 ++++++++++++++++++++++---------------- src/socPredef.mli | 8 +- src/socUtils.ml | 71 +++++--- src/socUtils.mli | 30 ++-- test/lus2lic.sum | 2 +- test/lus2lic.time | 2 +- 19 files changed, 918 insertions(+), 360 deletions(-) create mode 100644 src/socExecEvalPredef.ml create mode 100644 src/socExecEvalPredef.mli create mode 100644 src/socExecValue.ml create mode 100644 src/socExecValue.mli diff --git a/Makefile b/Makefile index 3ca5f4ca..4fb387b5 100644 --- a/Makefile +++ b/Makefile @@ -45,7 +45,13 @@ SOC_SOURCES = \ $(OBJDIR)/actionsDeps.mli \ $(OBJDIR)/actionsDeps.ml \ $(OBJDIR)/lic2soc.mli \ - $(OBJDIR)/lic2soc.ml + $(OBJDIR)/lic2soc.ml \ + $(OBJDIR)/socExecValue.mli \ + $(OBJDIR)/socExecValue.ml \ + $(OBJDIR)/socExecEvalPredef.mli \ + $(OBJDIR)/socExecEvalPredef.ml \ + $(OBJDIR)/socExec.mli \ + $(OBJDIR)/socExec.ml SOURCES = \ diff --git a/src/compile.ml b/src/compile.ml index 0c47a64d..1cbdd419 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 25/02/2013 (at 18:13) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/03/2013 (at 16:39) by Erwan Jahier> *) open Lxm open Errors @@ -15,16 +15,16 @@ let rec first_pack_in = let (doit : AstV6.pack_or_model list -> Ident.idref option -> LicPrg.t) = fun srclist main_node -> let syntax_tab = AstTab.create srclist in - (* Pour chaque package, on a un solveur de références - globales, pour les types, const et node : - - les références pointées (p::n) sont recherchées - directement dans la syntax_tab puisqu'il n'y a pas - d'ambiguité - - les références simples sont recherchées : - . dans le pack lui-même - . dans un des packs déclarés "uses", avec - priorité dans l'ordre - *) + (* Pour chaque package, on a un solveur de références + globales, pour les types, const et node : + - les références pointées (p::n) sont recherchées + directement dans la syntax_tab puisqu'il n'y a pas + d'ambiguité + - les références simples sont recherchées : + . dans le pack lui-même + . dans un des packs déclarés "uses", avec + priorité dans l'ordre + *) let lic_tab = LicTab.create syntax_tab in Verbose.exe ~level:2 (fun () -> AstTab.dump syntax_tab); Ident.set_dft_pack_name (first_pack_in srclist); @@ -38,10 +38,10 @@ let (doit : AstV6.pack_or_model list -> Ident.idref option -> LicPrg.t) = LicTab.compile_node lic_tab main_node in let zelic = LicTab.to_lic_prg lic_tab in - (* élimination polymorphisme surcharge *) + (* élimination polymorphisme surcharge *) let zelic = L2lRmPoly.doit zelic in - (* alias des types array *) - (* let zelic = L2lAliasType.doit zelic in *) + (* alias des types array *) + (* let zelic = L2lAliasType.doit zelic in *) let zelic = if not !Global.inline_iterator then zelic else (* to be done before array expansion otherwise they won't be expanded *) L2lExpandMetaOp.doit zelic @@ -52,12 +52,12 @@ let (doit : AstV6.pack_or_model list -> Ident.idref option -> LicPrg.t) = || !Global.expand_nodes (* expand performs no fixpoint, so it will work only if we have one op per equation...*) then - (* Split des equations (1 eq = 1 op) *) + (* Split des equations (1 eq = 1 op) *) L2lSplit.doit zelic else zelic in - (* Array and struct expansion: to do after polymorphism elimination *) + (* Array and struct expansion: to do after polymorphism elimination *) let zelic = if not !Global.expand_nodes then zelic else L2lExpandNodes.doit zelic in @@ -70,9 +70,15 @@ let (doit : AstV6.pack_or_model list -> Ident.idref option -> LicPrg.t) = L2lCheckOutputs.doit zelic; (* XXX just to see if it compiles *) -(* let zesoc = Lic2soc.f zelic in *) - -(* SocUtils.output true "xxx" zesoc; *) + (* SocUtils.output true "xxx" zesoc; *) + if !Global.exec then + (match main_node with + | None -> () + | Some main_node -> + let msk, zesoc = Lic2soc.f zelic (Lic.node_key_of_idref main_node) in + SocExec.f zesoc msk + ); + zelic diff --git a/src/global.ml b/src/global.ml index 43bb5ed2..edb90681 100644 --- a/src/global.ml +++ b/src/global.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 23/01/2013 (at 10:12) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/03/2013 (at 16:39) by Erwan Jahier> *) (** Global variables for handling command-line options. *) @@ -30,8 +30,9 @@ let expand_arrays = ref false let oc = ref Pervasives.stdout let tlex = ref false let nonreg_test = ref false -(** those functions are here as they modify some global vars *) +let exec = ref false +(** those functions are here as they modify some global vars *) let add_infile file_name = infiles := !infiles@[file_name] diff --git a/src/lic.ml b/src/lic.ml index b8f40451..df369cd4 100644 --- a/src/lic.ml +++ b/src/lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 20/02/2013 (at 11:19) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/02/2013 (at 18:58) by Erwan Jahier> *) (** Define the Data Structure representing Compiled programs. *) @@ -426,8 +426,11 @@ let ident_of_type = function (****************************************************************************) (* Utilitaires liés aux node_key *) -let (make_simple_node_key : Ident.long -> node_key) = - fun nkey -> (nkey, []) +let (node_key_of_idref : Ident.idref -> node_key) = + fun nkey -> (Ident.long_of_idref nkey, []) + +let (node_key_of_ident : string -> node_key) = + fun id -> (Ident.long_of_string id, []) (* OBSOLETE ET UN PEU FAUX ! R1: pas forcément obsolete ; cf commentaire plus haut. diff --git a/src/lic2soc.ml b/src/lic2soc.ml index 8abe38f3..d3a9bf7c 100644 --- a/src/lic2soc.ml +++ b/src/lic2soc.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 25/02/2013 (at 18:09) by Erwan Jahier> *) +(** Time-stamp: <modified the 04/03/2013 (at 18:03) by Erwan Jahier> *) open Lxm open Lic @@ -7,7 +7,7 @@ type action = ActionsDeps.action (* Raised when a soc that haven't been translated yet is used in another soc during the translation *) -exception Undef_soc of Lic.node_key +exception Undef_soc of Soc.key * Lxm.t * Lic.by_pos_op * Soc.var_type list (*********************************************************************************) (** Informations liées au contexte de traduction. *) @@ -49,6 +49,7 @@ let rec lic_to_soc_type: (Lic.type_ -> Soc.var_type) = | Lic.TypeVar Lic.AnyNum -> assert false + (*********************************************************************************) (** Renomme une variable définie par l'utilisateur. @@ -82,6 +83,7 @@ let (slice_info_to_index_list : Lic.slice_info -> int list) = in aux f +(* if val_exp is a leaf (i.e., a constant) *) let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) = fun licprg val_exp -> let v = val_exp.Lic.ve_core in @@ -91,7 +93,6 @@ let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) = | Lic.Merge(c_flg, cl) -> assert false | Lic.CallByPosLic (by_pos_op_flg, val_exp_list) -> ( match by_pos_op_flg.it with - | Lic.PREDEF_CALL _ -> assert false (* todo *) | Lic.VAR_REF name -> let type_ = (List.hd type_) in let translation = @@ -104,6 +105,11 @@ let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) = let type_ = lic_to_soc_type (List.hd type_) in Some [Soc.Const(Ident.string_of_long l, type_)] ) + | Lic.PREDEF_CALL AstPredef.TRUE_n -> Some [Soc.Const("true", Soc.Bool)] + | Lic.PREDEF_CALL AstPredef.FALSE_n -> Some [Soc.Const("false", Soc.Bool)] + | Lic.PREDEF_CALL AstPredef.RCONST_n id -> Some [Soc.Const(id, Soc.Real)] + | Lic.PREDEF_CALL AstPredef.ICONST_n id -> Some [Soc.Const(id, Soc.Int)] + | Lic.STRUCT_ACCESS(field) -> ( let expr = match val_exp_list with [e] -> e | _ -> assert false in let type_ = lic_to_soc_type (List.hd type_) in @@ -112,7 +118,7 @@ let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) = | None -> assert false | _ -> assert false in - Some [Soc.Field(filter_expr, field, type_)] + Some [Soc.Field(filter_expr, (field, type_))] ) | Lic.ARRAY_ACCES i -> ( let expr = match val_exp_list with [e] -> e | _ -> assert false in @@ -152,7 +158,8 @@ let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) = index_list in Some(exploded_array) - ) + ) + | Lic.PREDEF_CALL _ | Lic.CALL _ | Lic.PRE | Lic.ARROW @@ -174,7 +181,7 @@ let rec filter_of_left_part: (LicPrg.t -> Lic.left -> Soc.var_expr list) = ) | Lic.LeftFieldLic(lp,field,t) -> ( let lpl = filter_of_left_part licprg lp in - List.map (fun lp -> Soc.Field(lp, field, lic_to_soc_type t)) lpl + List.map (fun lp -> Soc.Field(lp, (field, lic_to_soc_type t))) lpl ) | Lic.LeftArrayLic(lp,index,t) -> ( let lpl = filter_of_left_part licprg lp in @@ -193,7 +200,8 @@ let rec (gao_of_action: action -> Soc.gao) = fun (ck, il, ol, op, lxm) -> let rec unpack_clock = function | Lic.BaseLic -> Soc.Call (ol, op, il) - | Lic.ClockVar i -> assert false + | Lic.ClockVar i -> (* should not occur ?*) + Soc.Call (ol, op, il) | Lic.On((c, value), inner_clock) -> (* let inner_clock = match inner_clock_opt with *) (* | Some x -> x *) @@ -217,6 +225,7 @@ let build_meth: Lxm.t -> string -> Lic.node_exp -> Soc.var list -> in { Soc.socm_name = name; + Soc.socm_lxm = lxm; Soc.socm_inputs = convert_node_interface node.Lic.inlist_eff; Soc.socm_outputs = convert_node_interface node.Lic.outlist_eff; Soc.socm_impl = @@ -227,12 +236,19 @@ let (lic_to_soc_var : Lic.var_info -> Soc.var) = fun vi -> vi.Lic.var_name_eff, lic_to_soc_type vi.Lic.var_type_eff -let component_profile_of_node: Lic.node_exp -> Soc.var list * Soc.var list = +let soc_profile_of_node: Lic.node_exp -> Soc.var list * Soc.var list = fun n -> let inputs = List.map lic_to_soc_var n.Lic.inlist_eff in let outputs = List.map lic_to_soc_var n.Lic.outlist_eff in inputs, outputs +let (soc_key_of_node_exp : Lic.node_exp -> Soc.key) = + fun n -> + let svi,svo = soc_profile_of_node n in + let (id, sargs) = n.node_key_eff in + assert (sargs=[]); + Ident.string_of_long2 id, List.map snd (svi@svo), None + let (val_exp_to_filter: LicPrg.t -> Lic.val_exp -> Soc.var_expr) = fun licprg val_exp -> @@ -255,6 +271,10 @@ let (val_exp_to_filter: LicPrg.t -> Lic.val_exp -> Soc.var_expr) = let type_ = lic_to_soc_type (List.hd type_) in Soc.Const(Ident.string_of_long l, type_) ) + | Lic.PREDEF_CALL AstPredef.TRUE_n -> Soc.Const("true", Soc.Bool) + | Lic.PREDEF_CALL AstPredef.FALSE_n -> Soc.Const("false", Soc.Bool) + | Lic.PREDEF_CALL AstPredef.RCONST_n id -> Soc.Const(id, Soc.Real) + | Lic.PREDEF_CALL AstPredef.ICONST_n id -> Soc.Const(id, Soc.Int) | STRUCT_ACCESS(field) -> ( let expr = match val_exp_list with [e] -> e | _ -> assert false in let type_ = match type_ with [t] -> lic_to_soc_type t | _ -> assert false in @@ -263,7 +283,7 @@ let (val_exp_to_filter: LicPrg.t -> Lic.val_exp -> Soc.var_expr) = | None -> assert false | _ -> assert false in - Soc.Field(filter_expr, field, type_) + Soc.Field(filter_expr, (field, type_)) ) | ARRAY_ACCES i -> ( let expr = match val_exp_list with [e] -> e | _ -> assert false in @@ -299,15 +319,13 @@ type memory = Soc.memory * action list (* m (** Créé une opération à partir d'un nom de méthode d'un composant. *) let component_meth_to_operation: - Soc.component -> string -> memory option -> Soc.atomic_operation = + Soc.t -> string -> memory option -> Soc.atomic_operation = fun comp func_name -> function - | None -> - let (node_name,_,_) = comp.Soc.socc_key in - Soc.Procedure (node_name ^ "_" ^ func_name) - | Some (m, _) -> Soc.Method(m, func_name) + | None -> Soc.Procedure comp.Soc.socc_key + | Some (m, _) -> Soc.Method(m, comp.Soc.socc_key) (* Créé une action concernant un appel de procédure ou de méthode. *) -let (action_of_method: Lxm.t -> Soc.component -> Lic.clock -> Soc.var_expr list -> +let (action_of_method: Lxm.t -> Soc.t -> Lic.clock -> Soc.var_expr list -> Soc.var_expr list -> memory option -> Soc.step_method -> action) = fun lxm c clk il ol mem m -> let nth i l = @@ -339,12 +357,12 @@ let create_new_memory: (ctx -> ctx * string) = fun ctx -> Il faut donc qu'on créé une mémoire représentant ce composant (issue de la traduction de cet opérateur), afin de garder son état dans le composant résultant de ce noeud. *) -let create_memory_from_component: (ctx -> Soc.component -> ctx * Soc.memory) = +let create_memory_from_component: (ctx -> Soc.t -> ctx * Soc.memory) = fun ctx c -> let ctx, mem_name = create_new_memory ctx in ctx, Soc.CompMem(mem_name, c.Soc.socc_key) -let (make_memory : Lxm.t -> Lic.clock -> ctx -> Soc.component -> +let (make_memory : Lxm.t -> Lic.clock -> ctx -> Soc.t -> Soc.var_expr list -> Soc.var_expr list -> ctx * memory option) = fun lxm clk ctx component inputs lpl -> match component.Soc.socc_memories with @@ -366,19 +384,27 @@ let (make_memory : Lxm.t -> Lic.clock -> ctx -> Soc.component -> *) type e2a_acc = ctx * action list * Soc.var_expr list * memory list * ActionsDeps.t -module NkMap = Map.Make( - struct - type t = Lic.node_key - let compare = compare - end -) - -type comp_tbl = Soc.component NkMap.t - -let rec (actions_of_expression_acc: Lxm.t -> comp_tbl -> +(* Béquille en attendant mieux *) +let by_pos_op_to_soc_ident = function + | PREDEF_CALL AstPredef.TRUE_n -> assert false + | PREDEF_CALL AstPredef.FALSE_n -> assert false + | PREDEF_CALL AstPredef.RCONST_n id -> assert false + | PREDEF_CALL AstPredef.ICONST_n id -> assert false + + | PREDEF_CALL c -> "Lustre::"^(AstPredef.op2string_long c) + | HAT _ -> assert false + | PRE -> "Lustre::pre" + | ARROW -> "Lustre::arrow" + | FBY-> "Lustre::fby" + | CURRENT -> "Lustre::current" + | CONCAT-> "Lustre::concat" + | ARRAY -> "Lustre::array" + | _ -> assert false + +let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl -> Lic.clock -> Soc.var_expr list -> e2a_acc -> Lic.val_exp -> e2a_acc) = - fun lxm comp_tbl clk lpl acc expr -> + fun lxm soc_tbl clk lpl acc expr -> let (ctx, al, iol, ml, deps) = acc in match get_leaf ctx.prg expr with | Some names -> @@ -396,7 +422,7 @@ let rec (actions_of_expression_acc: Lxm.t -> comp_tbl -> let filter_to_field filter field ftype = let ftype = match ftype with [x] -> x | _ -> assert false in let filter = match filter with [x] -> x | _ -> assert false in - Soc.Field(filter, field, lic_to_soc_type ftype) + Soc.Field(filter, (field, lic_to_soc_type ftype)) in let actions = List.map @@ -421,50 +447,71 @@ let rec (actions_of_expression_acc: Lxm.t -> comp_tbl -> | Lic.ARRAY_SLICE _ | Lic.VAR_REF _ | Lic.CONST_REF _ | Lic.ARRAY_ACCES _ | Lic.STRUCT_ACCESS _ | Lic.TUPLE -> assert false - | Lic.WHEN ck -> (assert false -(* (* L'opérateur when n'est pas un composant, il modifie *) -(* simplement les conditions de traitement des expressions. *) *) -(* let ctx, actions, inputs, mems, deps = *) -(* actions_of_expression_list comp_tbl clk lpl acc val_exp_list *) -(* in *) -(* let new_clock = *) -(* match ck with *) -(* | AstCore.Base -> CE_base *) -(* | AstCore.NamedClock {it=(cc,cv)} -> *) -(* CE_clock(name, value, clk) *) -(* Clocking.clock_eff_of_clock_exp ctx.prg ck *) -(* in *) -(* let ctx, outputs, actions_reclocked = *) -(* match actions with *) -(* | [] -> *) -(* (* L'expression du when est une feuille, on créé quand *) -(* même une nouvelle action pour clocker la feuille. *) *) -(* ctx, lpl, [new_clock, inputs, lpl, Soc.Assign, lxm] *) -(* | _ -> *) -(* ctx, inputs, *) -(* (* Remplacement de l'horloge des actions de l'expression *) -(* par la nouvelle horloge issue du `when`. *) *) -(* List.map *) -(* (fun (_, i,o,op,lxm) -> new_clock,i,o,op,lxm) *) -(* actions *) -(* in *) -(* ctx, actions_reclocked, outputs, mems, deps *) + | Lic.WHEN ck -> (assert false + (* XXX FINISH ME!!! *) + (* (* L'opérateur when n'est pas un composant, il modifie *) + (* simplement les conditions de traitement des expressions. *) *) + (* let ctx, actions, inputs, mems, deps = *) + (* actions_of_expression_list Soc.tbl clk lpl acc val_exp_list *) + (* in *) + (* let new_clock = *) + (* match ck with *) + (* | AstCore.Base -> CE_base *) + (* | AstCore.NamedClock {it=(cc,cv)} -> *) + (* CE_clock(name, value, clk) *) + (* Clocking.clock_eff_of_clock_exp ctx.prg ck *) + (* in *) + (* let ctx, outputs, actions_reclocked = *) + (* match actions with *) + (* | [] -> *) + (* (* L'expression du when est une feuille, on créé quand *) + (* même une nouvelle action pour clocker la feuille. *) *) + (* ctx, lpl, [new_clock, inputs, lpl, Soc.Assign, lxm] *) + (* | _ -> *) + (* ctx, inputs, *) + (* (* Remplacement de l'horloge des actions de l'expression *) + (* par la nouvelle horloge issue du `when`. *) *) + (* List.map *) + (* (fun (_, i,o,op,lxm) -> new_clock,i,o,op,lxm) *) + (* actions *) + (* in *) + (* ctx, actions_reclocked, outputs, mems, deps *) ) - | PREDEF_CALL _ | CALL _ | PRE | ARROW | FBY | CURRENT | CONCAT - | HAT _ | ARRAY -> ( + + | CALL _ -> assert false (* XXX todo *) + | HAT _ -> assert false (* XXX todo *) + | ARRAY -> assert false (* XXX todo *) + | PREDEF_CALL _ + | PRE | ARROW | FBY | CURRENT | CONCAT -> ( (* build the component of "expr" *) - let component : Soc.component = + let component : Soc.t = + let id = by_pos_op_to_soc_ident by_pos_op_flg.it in let args_types : Soc.var_type list = - List.map lic_to_soc_type + List.map lic_to_soc_type (List.flatten (List.map (fun ve -> ve.ve_typ) val_exp_list)) in - match - SocPredef.component_interface_of_pos_op lxm by_pos_op_flg.it args_types - with - | SocPredef.SC soc -> soc - | SocPredef.Undef nk -> - try NkMap.find nk comp_tbl - with Not_found -> raise (Undef_soc nk) + let exp_type = List.hd(List.rev args_types) in + let args_types_plus = + (* Add the type of the expression (indeed, ege, if ARROW has + 2 args of the same type t, its profile is "t -> t -> t" + hence we add the missing t in + *) + args_types @ [exp_type] + in + let id = SocPredef.instanciate_name id exp_type in + let sk = id, args_types_plus, None in + try Soc.SocMap.find sk soc_tbl + with Not_found -> + let l = Soc.SocMap.bindings soc_tbl in + let kl = fst (List.split l) in + let klstr = List.map SocUtils.string_of_soc_key kl in + + print_string ("\n********* Cannot find the soc.key " ^ + (SocUtils.string_of_soc_key sk) ^ " in \n\t" ^ + (String.concat "\n\t" klstr)^"\n"); + flush stdout; + raise (Undef_soc (sk, lxm, by_pos_op_flg.it, args_types)) + in (* Use that component to build the corresponding - actions @@ -490,22 +537,22 @@ let rec (actions_of_expression_acc: Lxm.t -> comp_tbl -> ) ) ) - - + + (** Traduction d'une liste d'expressions. *) -and (actions_of_expression_list: Lxm.t -> comp_tbl -> Lic.clock -> Soc.var_expr list -> +and (actions_of_expression_list: Lxm.t -> Soc.tbl -> Lic.clock -> Soc.var_expr list -> e2a_acc -> Lic.val_exp list -> e2a_acc) = - fun lxm comp_tbl clk lpl expr_list acc -> - List.fold_left (actions_of_expression_acc lxm comp_tbl clk lpl) expr_list acc + fun lxm soc_tbl clk lpl expr_list acc -> + List.fold_left (actions_of_expression_acc lxm soc_tbl clk lpl) expr_list acc -let (actions_of_expression : Lxm.t -> comp_tbl -> ctx -> Lic.clock -> Soc.var_expr list -> +let (actions_of_expression : Lxm.t -> Soc.tbl -> ctx -> Lic.clock -> Soc.var_expr list -> Lic.val_exp -> e2a_acc) = - fun lxm comp_tbl ctx clk lpl expr -> + fun lxm soc_tbl ctx clk lpl expr -> let acc0 = (ctx, [], [], [], ActionsDeps.empty) in - actions_of_expression_acc lxm comp_tbl clk lpl acc0 expr + actions_of_expression_acc lxm soc_tbl clk lpl acc0 expr (*********************************************************************************) (** Traduction d'une équation complète. @@ -513,15 +560,15 @@ let (actions_of_expression : Lxm.t -> comp_tbl -> ctx -> Lic.clock -> Soc.var_ex On traduit d'abord l'expression de l'équation, puis on fait une égalité entre les variables issues de la traduction de l'expression et la partie gauche de l'équation. *) -let (actions_of_equation: Lxm.t -> comp_tbl -> ctx -> Lic.eq_info -> +let (actions_of_equation: Lxm.t -> Soc.tbl -> ctx -> Lic.eq_info -> ctx * action list * memory list * ActionsDeps.t) = - fun lxm comp_tbl ctx (left_part, right_part) -> + fun lxm soc_tbl ctx (left_part, right_part) -> let clk = right_part.ve_clk in let clk = match clk with [clk] -> clk | _ -> assert false in let left_loc = List.map (filter_of_left_part ctx.prg) left_part in let left_loc = List.flatten left_loc in let ctx, actions, _, memories, deps = - actions_of_expression lxm comp_tbl ctx clk left_loc right_part + actions_of_expression lxm soc_tbl ctx clk left_loc right_part in (* let final_action = clk_l, inputs, left_loc, Soc.Identity in *) (* let deps = add deps final_action actions in *) @@ -531,27 +578,25 @@ let (actions_of_equation: Lxm.t -> comp_tbl -> ctx -> Lic.eq_info -> (*********************************************************************************) (** Traduit un noeud en composant Soc. *) -let rec (component_of_node: LicPrg.t -> Lic.node_exp -> comp_tbl -> ctx * Soc.component) = - fun licprg node comp_tbl -> +let rec (component_of_node: LicPrg.t -> Lic.node_exp -> Soc.tbl -> (ctx * Soc.t) option) = + fun licprg node soc_tbl -> match node.Lic.def_eff with - | ExternLic -> assert false - | MetaOpLic node_key -> assert false - | AbstractLic None -> assert false (* None if extern in the provide part *) - | AbstractLic (Some node_exp) -> component_of_node licprg node_exp comp_tbl - | BodyLic b -> - + | ExternLic -> None + | MetaOpLic node_key -> None + | AbstractLic None -> None (* None if extern in the provide part *) + | AbstractLic (Some node_exp) -> component_of_node licprg node_exp soc_tbl + | BodyLic b -> let lxm = node.lxm in let ctx = create_context licprg in let ctx, actions, mems, deps = (* on itere sur la liste des équations *) List.fold_left (fun (c, a, m, d) eq -> - let nc, na, nm, nd = actions_of_equation eq.src comp_tbl c eq.it in + let nc, na, nm, nd = actions_of_equation eq.src soc_tbl c eq.it in nc, a @ na, m @ nm, (ActionsDeps.concat nd d) ) (ctx, [], [], ActionsDeps.empty) - b.eqs_eff - + b.eqs_eff in (* Construction des dépendances entre les expressions *) let all_deps = ActionsDeps.build_data_deps_from_actions deps actions in @@ -570,7 +615,7 @@ let rec (component_of_node: LicPrg.t -> Lic.node_exp -> comp_tbl -> ctx * Soc.co | Some l -> List.map (lic_to_soc_var) l in let meth = build_meth lxm "step" node (locals @ ctx.locals) actions in - let profile = component_profile_of_node node in + let profile = soc_profile_of_node node in let memories, init_actions = List.split mems in let init_meth = match init_actions with | [] -> None @@ -579,7 +624,7 @@ let rec (component_of_node: LicPrg.t -> Lic.node_exp -> comp_tbl -> ctx * Soc.co let io_list = node.Lic.inlist_eff @ node.Lic.outlist_eff in let io_type = List.map (fun vi -> lic_to_soc_type vi.var_type_eff) io_list in let comp = { - Soc.socc_key = fst (fst node.Lic.node_key_eff), io_type, None; + Soc.socc_key = Ident.string_of_long2 (fst node.Lic.node_key_eff), io_type, None; Soc.socc_profile = profile; Soc.socc_memories = memories; Soc.socc_init = init_meth; @@ -588,41 +633,77 @@ let rec (component_of_node: LicPrg.t -> Lic.node_exp -> comp_tbl -> ctx * Soc.co seule méthode *) } in - ctx, comp + Some(ctx, comp) (*********************************************************************************) open Soc (* exported *) -let f: (LicPrg.t -> Soc.component list) = - fun prog -> - let rec (process_node:Lic.node_key -> Lic.node_exp -> comp_tbl -> comp_tbl) = +let f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) = + fun prog mnk -> + let rec (process_node : Lic.node_key -> Lic.node_exp -> Soc.tbl -> Soc.key * Soc.tbl) = fun nk node acc_comp -> - let name = (* Lic.string_of_node_key *) nk in - if NkMap.mem name acc_comp then acc_comp else - (match SocPredef.of_node_key name with - | SocPredef.SC soc -> NkMap.add name soc acc_comp - | SocPredef.Undef nk -> - try - (match LicPrg.find_node prog nk with - | None -> assert false - | Some node_def -> - let _, soc = component_of_node prog node_def acc_comp in - NkMap.add name soc acc_comp + let sk = soc_key_of_node_exp node in + let acc_comp = + if SocMap.mem sk acc_comp then acc_comp else + try + (match LicPrg.find_node prog nk with + | None -> assert false + | Some node_def -> + (match component_of_node prog node_def acc_comp with + | Some(_,soc) -> SocMap.add sk soc acc_comp + | None -> + print_string ("Undefined soc : " ^ (string_of_node_key nk) ^ "\n"); + flush stdout; + acc_comp ) - with - | Undef_soc n_ukn -> - (* Il manque une dépendance, on essaie de - la traduire puis de retraduire le noeud courant. *) - (match LicPrg.find_node prog n_ukn with - | None -> assert false - | Some node_ukn -> - let comps = process_node n_ukn node_ukn acc_comp in - process_node name node comps - ) - ) + ) + with + | Undef_soc (sk,lxm,pos_op, types) -> + (* Il manque une dépendance, on essaie de la + traduire puis de retraduire le noeud courant. *) + let soc = SocPredef.component_interface_of_pos_op lxm pos_op types in + let acc_comp = SocMap.add soc.socc_key soc acc_comp in + snd (process_node nk node acc_comp) + in + sk, acc_comp + + + + +(* try *) +(* *) +(* let soc = SocPredef.of_soc_key sk in *) +(* *) +(* (match SocPredef.of_soc_key sk with *) +(* | Some soc -> SocMap.add sk soc acc_comp *) +(* | None -> *) +(* try *) +(* (match LicPrg.find_node prog nk with *) +(* | None -> assert false *) +(* | Some node_def -> *) +(* (match component_of_node prog node_def acc_comp with *) +(* | Some(_,soc) -> SocMap.add sk soc acc_comp *) +(* | None -> *) +(* print_string ("Undefined soc : " ^ (string_of_node_key nk) ^ "\n"); *) +(* flush stdout; *) +(* acc_comp *) +(* ) *) +(* ) *) +(* with *) +(* | Undef_soc (sk,lxm,pos_op, types) -> *) +(* (* Il manque une dépendance, on essaie de la *) +(* traduire puis de retraduire le noeud courant. *) *) +(* let soc = SocPredef.component_interface_of_pos_op lxm pos_op types in *) +(* let acc_comp = SocMap.add sk soc acc_comp in *) +(* snd (process_node nk node acc_comp) *) +(* ) *) +(* in *) +(* sk, acc_comp *) in - let soc_string_map = LicPrg.fold_nodes process_node prog NkMap.empty in - let soc_list = NkMap.fold (fun n soc acc -> soc::acc) soc_string_map [] in - soc_list + match LicPrg.find_node prog mnk with + | None -> assert false + | Some node_exp -> + process_node mnk node_exp SocMap.empty + diff --git a/src/lic2soc.mli b/src/lic2soc.mli index 6f43c3fa..70ea308c 100644 --- a/src/lic2soc.mli +++ b/src/lic2soc.mli @@ -1,3 +1,4 @@ -(** Time-stamp: <modified the 20/02/2013 (at 10:50) by Erwan Jahier> *) +(** Time-stamp: <modified the 01/03/2013 (at 15:29) by Erwan Jahier> *) -val f: LicPrg.t -> Soc.component list + +val f: LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl diff --git a/src/licTab.ml b/src/licTab.ml index b9606c0f..50785367 100644 --- a/src/licTab.ml +++ b/src/licTab.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/02/2013 (at 15:08) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/02/2013 (at 10:55) by Erwan Jahier> *) open Lxm @@ -1373,9 +1373,7 @@ let compile_all (this:t) : t = let compile_node (this:t) (main_node:Ident.idref) : t = (* la clée "absolue" du main node (pas d'args statiques) *) - let main_node_key = - Lic.make_simple_node_key (Ident.long_of_idref main_node) - in + let main_node_key = node_key_of_idref main_node in Verbose.printf "-- MAIN NODE: \"%s\"\n" (LicDump.string_of_node_key_rec main_node_key); diff --git a/src/mainArgs.ml b/src/mainArgs.ml index 578404a1..f393f2e8 100644 --- a/src/mainArgs.ml +++ b/src/mainArgs.ml @@ -129,6 +129,12 @@ let mkoptab (opt:t) : unit = ( Global.outfile := x)) ["Set the output file name"] ; + mkopt opt + ["-exec"] + (Arg.Unit (fun _ -> Global.exec := true)) + ["interpret the program using RIF conventions for I/O (experimental)."] + ; + mkopt opt ["-knc"; "--keep-nested-calls"] (Arg.Unit (fun _ -> Global.one_op_per_equation := false)) diff --git a/src/soc.ml b/src/soc.ml index 491cbdb6..9ed4d07b 100644 --- a/src/soc.ml +++ b/src/soc.ml @@ -1,3 +1,5 @@ +(* Time-stamp: <modified the 05/03/2013 (at 15:28) by Erwan Jahier> *) + (** Synchronous Object Component *) (* Just a string because : @@ -16,49 +18,70 @@ type var_type = type var = ident * var_type -type component_key = +type key = ident * var_type list * (* I/O type list *) (int * int * int) option (* to deal with slices (useful?) *) + type memory = - | CompMem of ident * component_key (* Memory name * instanciated component key *) + | CompMem of ident * key (* Memory name * instanciated component key *) | VarMem of var (* Variable denotation *) type var_expr = - | Var of ident * var_type - | Const of ident * var_type (* useful? *) - | Field of var_expr * ident * var_type + | Var of var + | Const of var (* useful? *) + | Field of var_expr * var | Index of var_expr * int * var_type type atomic_operation = | Assign (* Wire *) - | Method of memory * ident (* step call *) - | Procedure of ident (* memoryless method made explicit *) + | Method of memory * key (* step call *) + | Procedure of key (* memoryless method made explicit (a good idea?) *) + (* Guarded Atomic Operation *) type gao = - | Case of ident * (ident * gao list) list + | Case of ident (* enum var *) * (ident (* enum value *) * gao list) list | Call of var_expr list * atomic_operation * var_expr list (* outputs * op * inputs *) + type step_method = { socm_name : ident; - socm_inputs : int list; - socm_outputs : int list; - socm_impl : (var list * gao list) option; (* local vars + body *) + socm_lxm : Lxm.t; + socm_inputs : int list; (* input index in the socc_profile *) + socm_outputs : int list; (* output index in the socc_profile *) + socm_impl : (var list * gao list) option; (* local vars + body ; None for predef op *) } type precedence = ident * ident list -(* maps a step method name with the list of step methods that should - be called _before_ in the current step *) +(* Partial order over socc_step members. Maps a step method name with + the list of step methods that should be called _before_. + + nb : steps in socc_step are already ordered ; this partial order + can be useful to find another (better) total order w.r.t. test + opening. +*) -type component = { - socc_key : component_key; +type t = { + socc_key : key; socc_profile : var list * var list; socc_memories : memory list; socc_init : step_method option; - socc_step : step_method list; - socc_precedences : precedence list; + socc_step : step_method list; (* the order in the list is a valid w.r.t. + the partial order defined in + socc_precedences *) + socc_precedences : precedence list; (* partial order over socc_step methods *) } + +module SocMap = Map.Make( + struct + type t = key + let compare = compare + end +) + +type tbl = t SocMap.t + diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml new file mode 100644 index 00000000..da23c485 --- /dev/null +++ b/src/socExecEvalPredef.ml @@ -0,0 +1,254 @@ +(* Time-stamp: <modified the 05/03/2013 (at 17:53) by Erwan Jahier> *) + +open SocExecValue +open Soc + +(* A boring but simple module... *) + +let (lustre_iplus:substs -> var_expr list -> var_expr list -> subst) = + fun s vei veo -> + let values = List.map (get_value s) vei in + match values,veo with + | [I i1; I i2], [Var(id,Int)] -> id,I(i1+i2) + | _ -> assert false + +let (lustre_rplus:substs -> var_expr list -> var_expr list -> subst) = + fun s vei veo -> + let values = List.map (get_value s) vei in + match values,veo with + | [F i1; F i2], [Var(id,Real)] -> id,F(i1+.i2) + | _ -> assert false + +let lustre_itimes s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,I(x1 * x2) + | _ -> assert false + +let lustre_rtimes s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,F(x1 *. x2) + | _ -> assert false + +let lustre_idiv s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,I(x1 / x2) + | _ -> assert false + +let lustre_rdiv s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,F(x1 /. x2) + | _ -> assert false + +let lustre_iminus s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,I(x1 - x2) + | _ -> assert false + +let lustre_rminus s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,F(x1 -. x2) + | _ -> assert false + +let lustre_mod s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,I(x1 mod x2) + | _ -> assert false + +let lustre_ieq s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,B(x1 = x2) + | _ -> assert false + +let lustre_req s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,B(x1 = x2) + | _ -> assert false + +let lustre_iuminus s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1], [Var(id,_)] -> id,I(- x1) + | _ -> assert false + +let lustre_ruminus s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1], [Var(id,_)] -> id,F(-. x1) + | _ -> assert false + +let lustre_real2int s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1], [Var(id,_)] -> id,I(int_of_float x1) + | _ -> assert false + +let lustre_int2real s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1], [Var(id,_)] -> id,F(float_of_int x1) + | _ -> assert false + +let lustre_not s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B x1], [Var(id,_)] -> id,B(not x1) + | _ -> assert false + +let lustre_ilt s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,B(x1 < x2) + | _ -> assert false + +let lustre_rlt s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,B(x1 < x2) + | _ -> assert false + +let lustre_igt s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,B(x1 > x2) + | _ -> assert false + +let lustre_rgt s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,B(x1 > x2) + | _ -> assert false + +let lustre_ilte s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,B(x1 <= x2) + | _ -> assert false + +let lustre_rlte s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,B(x1 <= x2) + | _ -> assert false + +let lustre_igte s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [I x1; I x2], [Var(id,_)] -> id,B(x1 >= x2) + | _ -> assert false + +let lustre_rgte s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [F x1; F x2], [Var(id,_)] -> id,B(x1 >= x2) + | _ -> assert false + +let lustre_and s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B x1; B x2], [Var(id,_)] -> id,B(x1 && x2) + | _ -> assert false +let lustre_beq s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B x1; B x2], [Var(id,_)] -> id,B(x1 = x2) + | _ -> assert false + +let lustre_neq s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B x1; B x2], [Var(id,_)] -> id,B(x1 <> x2) + | _ -> assert false + +let lustre_or s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B x1; B x2], [Var(id,_)] -> id,B(x1 || x2) + | _ -> assert false + +let lustre_impl s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B x1; B x2], [Var(id,_)] -> id,B(not x1 or x2) + | _ -> assert false + +let lustre_xor s vei veo = + let values = List.map (get_value s) vei in + let id = match veo with [Var(id,_)] -> id | _ -> assert false in + let l = List.filter (fun x -> x=B true) values in + id,B(List.length l = 1) + +let lustre_iif s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B c; I x1; I x2], [Var(id,_)] -> id,I(if c then x1 else x2) + | _ -> assert false + +let lustre_rif s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B c; F x1; F x2], [Var(id,_)] -> id,F(if c then x1 else x2) + | _ -> assert false + +let lustre_bif s vei veo = + let values = List.map (get_value s) vei in + match values,veo with + | [B c; B x1; B x2], [Var(id,_)] -> id,B(if c then x1 else x2) + | _ -> assert false + + + +(* exported *) +let (get: Soc.key -> (substs -> var_expr list -> var_expr list -> subst)) = + fun (n,_,_) -> + match n with + | "Lustre::iplus" -> lustre_iplus + | "Lustre::rplus" -> lustre_rplus + | "Lustre::itimes"-> lustre_itimes + | "Lustre::rtimes"-> lustre_rtimes + | "Lustre::idiv" -> lustre_idiv + | "Lustre::rdiv" -> lustre_rdiv + | "Lustre::iminus"-> lustre_iminus + | "Lustre::rminus"-> lustre_rminus + + | "Lustre::mod" -> lustre_mod + | "Lustre::iuminus" -> lustre_iuminus + | "Lustre::ruminus" -> lustre_ruminus + | "Lustre::not" -> lustre_not + | "Lustre::real2int" -> lustre_real2int + | "Lustre::int2real" -> lustre_int2real + + | "Lustre::ilt" -> lustre_ilt + | "Lustre::rlt" -> lustre_rlt + | "Lustre::igt" -> lustre_igt + | "Lustre::rgt" -> lustre_rgt + | "Lustre::ilte" -> lustre_ilte + | "Lustre::rlte" -> lustre_rlte + | "Lustre::igte" -> lustre_igte + | "Lustre::rgte" -> lustre_rgte + + | "Lustre::and" -> lustre_and + | "Lustre::beq" -> lustre_beq + | "Lustre::ieq" -> lustre_ieq + | "Lustre::req" -> lustre_req + | "Lustre::neq" -> lustre_neq + | "Lustre::or" -> lustre_or + + | "Lustre::xor" -> lustre_xor + | "Lustre::impl" -> lustre_impl + + | "Lustre::iif" -> lustre_iif + | "Lustre::rif" -> lustre_rif + | "Lustre::bif" -> lustre_bif + + | _ -> raise Not_found + + diff --git a/src/socExecEvalPredef.mli b/src/socExecEvalPredef.mli new file mode 100644 index 00000000..12b3925a --- /dev/null +++ b/src/socExecEvalPredef.mli @@ -0,0 +1,11 @@ +(* Time-stamp: <modified the 05/03/2013 (at 17:10) by Erwan Jahier> *) + + +(** Returns a predef operator interpreter. Raises Not_found if the + operator is not defined. + + The interpreper supposes that the substitution do replace all inputs + by values, and that types and arities are correct. +*) +val get: Soc.key -> + (SocExecValue.substs -> Soc.var_expr list -> Soc.var_expr list -> SocExecValue.subst) diff --git a/src/socExecValue.ml b/src/socExecValue.ml new file mode 100644 index 00000000..f2cfab87 --- /dev/null +++ b/src/socExecValue.ml @@ -0,0 +1,76 @@ +(* Time-stamp: <modified the 05/03/2013 (at 17:40) by Erwan Jahier> *) + +open Soc + +type t = I of int | F of float | B of bool | E of Soc.ident +type subst = (ident * t) +type substs = subst list + + +let (to_string : t -> string) = + function + | I i -> string_of_int i + | F f -> string_of_float f + | B true -> "t" + | B false -> "f" + | E e -> e + +(* XXX use a Rif reader *) +let rec (read_enum : ident list -> ident) = + fun idl -> + print_string ("Enter " ^ (String.concat "," idl)); flush stdout; + let str = read_line () in + if List.mem str idl then str else (print_string "Bad enum; "; read_enum idl) + +let (read_value : var -> t) = + fun (_,t) -> + match t with + | Bool -> print_string "Enter a bool (t/f):";flush stdout; B(read_line () = "t") + | Int -> print_string "Enter an int:"; flush stdout; I(read_int()) + | Real -> print_string "Enter a float:"; flush stdout; F(read_float()) + | Enum(_,idl) -> E(read_enum(idl)) + | _ -> assert false (* finish me! *) + +let (read_soc_input : Soc.t -> substs) = + fun soc -> + List.map (fun var -> "_"^(fst var), read_value var) (fst soc.socc_profile) + +let (string_of_substs :substs -> string) = + fun s -> + let str_l = List.map (fun (var,value) -> var ^ "->" ^ (to_string value)) s in + "{ "^ (String.concat "; " str_l) ^ " }" + + +let (get_val : ident -> substs -> t) = + fun id s -> + try List.assoc id s + with Not_found -> + failwith (id ^ " unbound in " ^ (string_of_substs s)) + +let (get_enum : ident -> substs -> ident) = +fun id s -> + match get_val id s with + | E e -> e + | _ -> assert false (* should not fail *) + +let (get_value : substs -> var_expr -> t) = + fun s v -> + match v with + | Var(id,_) -> get_val id s + | Const("true",Bool) -> B true + | Const("false",Bool) -> B false + | Const(id_in,Int) -> I (int_of_string id_in) + | Const(id_in,Real) -> F (float_of_string id_in) + | Const(id,_) -> assert false + | Field(_,_) -> assert false + | Index(_,_,_) -> assert false + +(* XXX use rif.dump *) +let (dump_substs : var list * var list -> substs -> unit) = + fun (ins,outs) s -> + let values = List.map (fun (var,value) -> var^"="^(to_string value)) s in + print_string ((String.concat " " values) ^ "\n"); + flush stdout + + + diff --git a/src/socExecValue.mli b/src/socExecValue.mli new file mode 100644 index 00000000..0c698448 --- /dev/null +++ b/src/socExecValue.mli @@ -0,0 +1,21 @@ +(* Time-stamp: <modified the 05/03/2013 (at 15:28) by Erwan Jahier> *) + +(** Manipulating data in the Soc interpreter *) + +type t = I of int | F of float | B of bool | E of Soc.ident +type subst = (Soc.ident * t) +type substs = subst list + +val get_val : Soc.ident -> substs -> t +val get_enum : Soc.ident -> substs -> Soc.ident +val get_value : substs -> Soc.var_expr -> t + +(* Pretty-printers *) +val to_string : t -> string +val string_of_substs :substs -> string + +(* RIF I/O *) +val dump_substs : Soc.var list * Soc.var list -> substs -> unit +val read_enum : Soc.ident list -> Soc.ident +val read_value : Soc.var -> t +val read_soc_input : Soc.t -> substs diff --git a/src/socPredef.ml b/src/socPredef.ml index 9ed70a02..783e4a39 100644 --- a/src/socPredef.ml +++ b/src/socPredef.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 21/02/2013 (at 11:10) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/03/2013 (at 18:05) by Erwan Jahier> *) (** Synchronous Object Code for Predefined operators. *) @@ -12,34 +12,60 @@ open Soc let b = Soc.Bool let i = Soc.Int let r = Soc.Real -let alpha = Soc.Alpha 0 let bb = ["x", b], ["z", b] let ii = ["x", i], ["z", i] let rr = ["x", r], ["z", r] let ri = ["r", r], ["i", i] let ir = ["i", i], ["r", r ] -let aa = ["x", alpha], ["z", alpha] let bbb = ["x", b; "y", b], ["z", b] let iii = ["x", i; "y", i], ["z", i] let rrr = ["x", r; "y", r], ["z", r] let rrb = ["x", r; "y", r], ["z", b] let iib = ["x", i; "y", i], ["z", b] -let aaa = ["i", alpha; "x", alpha], ["z", alpha] +(* if/then/else *) +let bbbb = ["c", b; "xt", b; "xe", b], ["z", b] +let biii = ["c", b; "xt", i; "xe", i], ["z", i] +let brrr = ["c", b; "xt", r; "xe", r], ["z", r] + +let (soc_profile_of_types : Soc.var_type list -> var list * var list) = + function + | [Soc.Bool;Soc.Bool] -> bb + | [Soc.Bool;Soc.Bool;Soc.Bool] -> bbb + | [Soc.Int ;Soc.Int] -> ii + | [Soc.Int ;Soc.Int ;Soc.Int] -> iii + | [Soc.Int ;Soc.Int ;Soc.Bool] -> iib + | [Soc.Real;Soc.Real] -> rr + | [Soc.Real;Soc.Int] -> ri + | [Soc.Int ;Soc.Real] -> ir + | [Soc.Real;Soc.Real;Soc.Real] -> rrr + | [Soc.Real;Soc.Real;Soc.Bool] -> rrb + | [Soc.Bool;Soc.Bool;Soc.Bool;Soc.Bool] -> bbbb + | [Soc.Bool;Soc.Int ;Soc.Int;Soc.Int] -> biii + | [Soc.Bool;Soc.Real;Soc.Real;Soc.Real] -> brrr + | tl -> + (* should not occurs *) + print_string ("Unsupported case: "^ ( + String.concat "," (List.map SocUtils.string_of_type_ref tl))); + flush stdout; + assert false + let step11 = { (* a useful alias again *) socm_name = "step"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0]; socm_outputs = [0]; socm_impl = None; } -let step21 = { (* a useful alias again *) +let step21 impl = { (* a useful alias again *) socm_name = "step"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0;1]; socm_outputs = [0]; - socm_impl = None; + socm_impl = impl; } (* used to build predef soc with no memory *) @@ -53,61 +79,64 @@ let make_soc key profile steps = { } -type soc_comp_opt = SC of Soc.component | Undef of Lic.node_key - (* exported *) -let of_node_key : Lic.node_key -> soc_comp_opt = - fun nk -> - match fst nk with - | "Lustre","mod" -> SC (make_soc ("mod", [], None) ii [step11]) - | "Lustre","iuminus" -> SC (make_soc ("iuminus", [], None) ii [step11]) - | "Lustre","ruminus" -> SC (make_soc ("ruminus", [], None) rr [step11]) - | "Lustre","not" -> SC (make_soc ("not", [], None) bb [step11]) - | "Lustre","real2int" -> SC (make_soc ("real2int", [], None) ri [step11]) - | "Lustre","int2real" -> SC (make_soc ("int2real", [], None) ir [step11]) - - | "Lustre","iplus" -> SC (make_soc ("iplus", [], None) iii [step21]) - | "Lustre","rplus" -> SC (make_soc ("rplus", [], None) rrr [step21]) - | "Lustre","itimes" -> SC (make_soc ("itimes", [], None) iii [step21]) - | "Lustre","rtimes" -> SC (make_soc ("rtimes", [], None) rrr [step21]) - | "Lustre","idiv" -> SC (make_soc ("idiv", [], None) iii [step21]) - | "Lustre","rdiv" -> SC (make_soc ("rdiv", [], None) rrr [step21]) - | "Lustre","iminus" -> SC (make_soc ("iminus", [], None) iii [step21]) - | "Lustre","rminus" -> SC (make_soc ("rminus", [], None) rrr [step21]) - - | "Lustre","ilt" -> SC (make_soc ("ilt", [], None) iib [step21]) - | "Lustre","rlt" -> SC (make_soc ("rlt", [], None) rrb [step21]) - | "Lustre","igt" -> SC (make_soc ("igt", [], None) iib [step21]) - | "Lustre","rgt" -> SC (make_soc ("rgt", [], None) rrb [step21]) - | "Lustre","ilte" -> SC (make_soc ("ilte", [], None) iib [step21]) - | "Lustre","rlte" -> SC (make_soc ("rlte", [], None) rrb [step21]) - | "Lustre","igte" -> SC (make_soc ("igte", [], None) iib [step21]) - | "Lustre","rgte" -> SC (make_soc ("rgte", [], None) rrb [step21]) - - | "Lustre","and" -> SC (make_soc ("and", [], None) bbb [step21]) - | "Lustre","beq" -> SC (make_soc ("beq", [], None) bbb [step21]) - | "Lustre","ieq" -> SC (make_soc ("ieq", [], None) iib [step21]) - | "Lustre","req" -> SC (make_soc ("req", [], None) rrb [step21]) - | "Lustre","neq" -> SC (make_soc ("neq", [], None) bbb [step21]) - | "Lustre","or" -> SC (make_soc ("or", [], None) bbb [step21]) - | "Lustre","xor" -> SC (make_soc ("xor", [], None) bbb [step21]) - | "Lustre","impl" -> SC (make_soc ("impl", [], None) bbb [step21]) +let of_soc_key : Soc.key -> Soc.t = + fun sk -> + let (id, tl, _) = sk in + let sp = soc_profile_of_types in + match id with + | "Lustre::mod" -> (make_soc sk (sp tl) [step11]) + | "Lustre::iuminus" -> (make_soc sk (sp tl) [step11]) + | "Lustre::ruminus" -> (make_soc sk (sp tl) [step11]) + | "Lustre::not" -> (make_soc sk (sp tl) [step11]) + | "Lustre::real2int" -> (make_soc sk (sp tl) [step11]) + | "Lustre::int2real" -> (make_soc sk (sp tl) [step11]) + + | "Lustre::iplus" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rplus" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::itimes" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rtimes" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::idiv" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rdiv" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::iminus" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rminus" -> (make_soc sk (sp tl) [step21 None]) + + | "Lustre::ilt" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rlt" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::igt" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rgt" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::ilte" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rlte" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::igte" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::rgte" -> (make_soc sk (sp tl) [step21 None]) + + | "Lustre::and" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::beq" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::ieq" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::req" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::neq" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::or" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::xor" -> (make_soc sk (sp tl) [step21 None]) + | "Lustre::impl" -> (make_soc sk (sp tl) [step21 None]) - | "Lustre","current" -> SC (make_soc ("current", [alpha], None) aa [step11]) + | "Lustre::current" -> (make_soc sk (sp tl) [step11]) - | "Lustre","fby" -> SC { - socc_key = "fby", [alpha], None; - socc_profile = aaa; - socc_memories = [VarMem("m", alpha)]; + (* Those have memories *) + | "Lustre::fby" -> { + socc_key = sk; + socc_profile = (sp tl); + socc_memories = [VarMem("m", snd (List.hd (snd (sp tl))))]; socc_step = [ { socm_name = "get"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = []; socm_outputs = [0]; socm_impl = None; }; { socm_name = "set"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [1]; socm_outputs = []; socm_impl = None @@ -116,25 +145,28 @@ let of_node_key : Lic.node_key -> soc_comp_opt = socc_precedences = ["set", ["get"]]; socc_init = Some { socm_name = "init"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0] ; socm_outputs = []; socm_impl = None; }; } - | "Lustre","pre" -> SC { - socc_key = "pre", [alpha], None; - socc_profile = aa; - socc_memories = [VarMem("m", alpha)]; + | "Lustre::pre" -> { + socc_key = sk; + socc_profile = (sp tl); + socc_memories = [VarMem("m", snd (List.hd (snd (sp tl))))]; socc_step = [ { socm_name = "get"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = []; socm_outputs = [0]; socm_impl = None; }; { - socm_name = "set"; + socm_name = "set"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0]; socm_outputs = []; socm_impl = None @@ -143,65 +175,88 @@ let of_node_key : Lic.node_key -> soc_comp_opt = socc_precedences = ["set", ["get"]]; socc_init = Some { socm_name = "init"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [] ; (* XXX ??? *) socm_outputs = []; socm_impl = None; }; } - | "Lustre","arrow" -> SC { - socc_key = "arrow", [alpha], None; - socc_profile = aaa; + | "Lustre::arrow" -> { + socc_key = sk; + socc_profile = (sp tl); socc_memories = []; socc_step = [ { socm_name = "step"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [1]; socm_outputs = [0]; - socm_impl = None; + socm_impl = None; (* XXX do something ? *) }; ]; socc_precedences = []; socc_init = Some { socm_name = "init"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0]; socm_outputs = []; - socm_impl = None; + socm_impl = None; (* XXX do something ? *) }; } - | "Lustre","if" -> SC { - socc_key = "if", [alpha], None; - socc_profile = ( - ["c", b ; "x", alpha; "y", alpha], - ["z", alpha] - ); + | "Lustre::if" -> { + socc_key = sk; + socc_profile = (sp tl); socc_memories = []; socc_init = None; socc_precedences = []; socc_step = [ { socm_name = "step"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0; 1; 2]; socm_outputs = [0]; socm_impl = None; } ]; } - | _ -> Undef nk + | _ -> + print_string (id ^ " is not defined.\n)"); flush stdout; + assert false + +let (instanciate_name : string -> Soc.var_type -> string) = + fun id concrete_type -> + match Str.split (Str.regexp "::") id, concrete_type with + | ["Lustre";op], Soc.Int -> "Lustre::i" ^ op + | ["Lustre";op], Soc.Real -> "Lustre::r" ^ op + | ["Lustre";op], Soc.Bool -> "Lustre::b" ^ op + | _,_ -> id + (** Instancie un composant polymorphe avec un type concret. *) -let instanciate_component: component -> Soc.var_type -> component = +let instanciate_component: Soc.t -> Soc.var_type -> Soc.t = fun c concrete_type -> + let rec instanciate_type vt = + match vt with + | Alpha _ -> concrete_type + | Struct(sn, fl) -> + Struct(sn, List.map (fun (id,vt) -> (id,instanciate_type vt)) fl) + | Array(vt,i) -> Array(instanciate_type vt,i) + | vt -> vt + in let new_profile = - List.map (fun (n, i) -> n, concrete_type) (fst c.socc_profile), - List.map (fun (n, i) -> n, concrete_type) (snd c.socc_profile) + List.map (fun (vn,vt) -> vn, instanciate_type vt) (fst c.socc_profile), + List.map (fun (vn,vt) -> vn, instanciate_type vt) (snd c.socc_profile) in let (key1, key2, key3) = c.socc_key in - let new_key = (key1, List.map (fun _ -> concrete_type) key2, key3) in + let new_key = (instanciate_name key1 concrete_type, + List.map instanciate_type key2, + key3) + in let new_memories = List.map - (function | VarMem(n, t) -> VarMem(n, concrete_type) | _ -> assert false) + (function | VarMem(n, t) -> VarMem(n, instanciate_type t) | _ -> assert false) c.socc_memories in { @@ -233,7 +288,7 @@ let instanciate_component: component -> Soc.var_type -> component = idem pour "x^n" (Hat_n). *) -let make_slice_component: Lic.slice_info -> Soc.var_type -> component = +let make_slice_component: Lic.slice_info -> Soc.var_type -> Soc.t = fun si t -> let (f,l,step) = (si.Lic.se_first, si.Lic.se_last,si.Lic.se_step) in let sub_array_type = @@ -250,6 +305,7 @@ let make_slice_component: Lic.slice_info -> Soc.var_type -> component = socc_step = [ { socm_name = "step"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0]; socm_outputs = [0]; socm_impl = None; @@ -260,7 +316,7 @@ let make_slice_component: Lic.slice_info -> Soc.var_type -> component = } -let make_array_component: int -> Soc.var_type -> component = +let make_array_component: int -> Soc.var_type -> Soc.t = fun i t -> let array_type = match t with @@ -274,6 +330,7 @@ let make_array_component: int -> Soc.var_type -> component = socc_step = [ { socm_name = "step"; + socm_lxm = Lxm.dummy "predef soc"; socm_inputs = [0]; socm_outputs = [0]; socm_impl = None; @@ -286,48 +343,48 @@ let make_array_component: int -> Soc.var_type -> component = let component_interface_of_predef: - Lxm.t -> AstPredef.op -> Soc.var_type list -> soc_comp_opt = + Lxm.t -> AstPredef.op -> Soc.var_type list -> Soc.t = fun lxm op types -> - match (op, types) with - | AstPredef.IPLUS_n, [Int; Int] -> of_node_key (("Lustre","iplus"), []) - | AstPredef.PLUS_n, [Int; Int] -> of_node_key (("Lustre","iplus"), []) - | AstPredef.PLUS_n, [Real; Real] -> of_node_key (("Lustre","rplus"), []) - | AstPredef.RPLUS_n, [Real; Real] -> of_node_key (("Lustre","rplus"), []) - | AstPredef.ITIMES_n,[Int; Int] -> of_node_key (("Lustre","itimes"), []) - | AstPredef.TIMES_n, [Int; Int] -> of_node_key (("Lustre","itimes"), []) - | AstPredef.TIMES_n, [Real; Real] -> of_node_key (("Lustre","rtimes"), []) - | AstPredef.RTIMES_n,[Real; Real] -> of_node_key (("Lustre","rtimes"), []) - | AstPredef.ISLASH_n,[Int; Int] -> of_node_key (("Lustre","idiv"), []) - | AstPredef.SLASH_n, [Int; Int] -> of_node_key (("Lustre","idiv"), []) - | AstPredef.DIV_n, [Int; Int] -> of_node_key (("Lustre","idiv"), []) - | AstPredef.MOD_n, [Int;Int] -> of_node_key (("Lustre","mod"), []) - | AstPredef.SLASH_n, [Real; Real] -> of_node_key (("Lustre","rdiv"), []) - | AstPredef.RSLASH_n,[Real; Real] -> of_node_key (("Lustre","rdiv"), []) - | AstPredef.MINUS_n, [Int; Int] -> of_node_key (("Lustre","iminus"), []) - | AstPredef.IMINUS_n,[Int; Int] -> of_node_key (("Lustre","iminus"), []) - | AstPredef.MINUS_n, [Real; Real] -> of_node_key (("Lustre","rminus"), []) - | AstPredef.RMINUS_n,[Real; Real] -> of_node_key (("Lustre","rminus"), []) - | AstPredef.UMINUS_n,[Int] -> of_node_key (("Lustre","iuminus"), []) - | AstPredef.IUMINUS_n, [Int] -> of_node_key (("Lustre","iuminus"), []) - | AstPredef.UMINUS_n, [Real] -> of_node_key (("Lustre","ruminus"), []) - | AstPredef.RUMINUS_n, [Real] -> of_node_key (("Lustre","ruminus"), []) - | AstPredef.LT_n, [Int; Int] -> of_node_key (("Lustre","ilt"), []) - | AstPredef.LT_n, [Real; Real] -> of_node_key (("Lustre","rlt"), []) - | AstPredef.GT_n, [Int; Int] -> of_node_key (("Lustre","igt"), []) - | AstPredef.GT_n, [Real; Real] -> of_node_key (("Lustre","rgt"), []) - | AstPredef.LTE_n, [Int; Int] -> of_node_key (("Lustre","ilte"), []) - | AstPredef.LTE_n, [Real; Real] -> of_node_key (("Lustre","rlte"), []) - | AstPredef.GTE_n, [Int; Int] -> of_node_key (("Lustre","igte"), []) - | AstPredef.GTE_n, [Real; Real] -> of_node_key (("Lustre","rgte"), []) - | AstPredef.AND_n, [Bool; Bool] -> of_node_key (("Lustre","and"), []) - | AstPredef.OR_n, [Bool; Bool] -> of_node_key (("Lustre","or"), []) - | AstPredef.XOR_n, [Bool; Bool] -> of_node_key (("Lustre","xor"), []) - | AstPredef.IMPL_n, [Bool; Bool] -> of_node_key (("Lustre","impl"), []) - | AstPredef.EQ_n, [Bool; Bool] -> of_node_key (("Lustre","beq"), []) - | AstPredef.EQ_n, [Int; Int] -> of_node_key (("Lustre","ieq"), []) - | AstPredef.EQ_n, [Real; Real] -> of_node_key (("Lustre","req"), []) - | AstPredef.NEQ_n, [Bool; Bool] -> of_node_key (("Lustre","neq"), []) - | AstPredef.NOT_n, [Bool] -> of_node_key (("Lustre","not"), []) + match (op, types) with (* utile de re-vérifier le type ? *) + | AstPredef.IPLUS_n, [Int; Int] -> of_soc_key (("Lustre::iplus"), types@[Int], None) + | AstPredef.PLUS_n, [Int; Int] -> of_soc_key (("Lustre::iplus"), types@[Int], None) + | AstPredef.PLUS_n, [Real; Real] -> of_soc_key (("Lustre::rplus"), types@[Real], None) + | AstPredef.RPLUS_n, [Real; Real] -> of_soc_key (("Lustre::rplus"), types@[Real], None) + | AstPredef.ITIMES_n,[Int; Int] -> of_soc_key (("Lustre::itimes"), types@[Int], None) + | AstPredef.TIMES_n, [Int; Int] -> of_soc_key (("Lustre::itimes"), types@[Int], None) + | AstPredef.TIMES_n, [Real; Real] -> of_soc_key (("Lustre::rtimes"), types@[Real], None) + | AstPredef.RTIMES_n,[Real; Real] -> of_soc_key (("Lustre::rtimes"), types@[Real], None) + | AstPredef.ISLASH_n,[Int; Int] -> of_soc_key (("Lustre::idiv"), types@[Int], None) + | AstPredef.SLASH_n, [Int; Int] -> of_soc_key (("Lustre::idiv"), types@[Int], None) + | AstPredef.DIV_n, [Int; Int] -> of_soc_key (("Lustre::idiv"), types@[Int], None) + | AstPredef.MOD_n, [Int;Int] -> of_soc_key (("Lustre::mod"), types@[Int], None) + | AstPredef.SLASH_n, [Real; Real] -> of_soc_key (("Lustre::rdiv"), types@[Real], None) + | AstPredef.RSLASH_n,[Real; Real] -> of_soc_key (("Lustre::rdiv"), types@[Real], None) + | AstPredef.MINUS_n, [Int; Int] -> of_soc_key (("Lustre::iminus"), types@[Int], None) + | AstPredef.IMINUS_n,[Int; Int] -> of_soc_key (("Lustre::iminus"), types@[Int], None) + | AstPredef.MINUS_n, [Real; Real] -> of_soc_key (("Lustre::rminus"), types@[Real], None) + | AstPredef.RMINUS_n,[Real; Real] -> of_soc_key (("Lustre::rminus"), types@[Real], None) + | AstPredef.UMINUS_n,[Int] -> of_soc_key (("Lustre::iuminus"), types@[Int], None) + | AstPredef.IUMINUS_n, [Int] -> of_soc_key (("Lustre::iuminus"), types@[Int], None) + | AstPredef.UMINUS_n, [Real] -> of_soc_key (("Lustre::ruminus"), types@[Real], None) + | AstPredef.RUMINUS_n, [Real] -> of_soc_key (("Lustre::ruminus"), types@[Real], None) + | AstPredef.LT_n, [Int; Int] -> of_soc_key (("Lustre::ilt"), types@[Int], None) + | AstPredef.LT_n, [Real; Real] -> of_soc_key (("Lustre::rlt"), types@[Real], None) + | AstPredef.GT_n, [Int; Int] -> of_soc_key (("Lustre::igt"), types@[Int], None) + | AstPredef.GT_n, [Real; Real] -> of_soc_key (("Lustre::rgt"), types@[Real], None) + | AstPredef.LTE_n, [Int; Int] -> of_soc_key (("Lustre::ilte"), types@[Int], None) + | AstPredef.LTE_n, [Real; Real] -> of_soc_key (("Lustre::rlte"), types@[Real], None) + | AstPredef.GTE_n, [Int; Int] -> of_soc_key (("Lustre::igte"), types@[Int], None) + | AstPredef.GTE_n, [Real; Real] -> of_soc_key (("Lustre::rgte"), types@[Real], None) + | AstPredef.AND_n, [Bool; Bool] -> of_soc_key (("Lustre::and"), types@[Bool], None) + | AstPredef.OR_n, [Bool; Bool] -> of_soc_key (("Lustre::or"), types@[Bool], None) + | AstPredef.XOR_n, [Bool; Bool] -> of_soc_key (("Lustre::xor"), types@[Bool], None) + | AstPredef.IMPL_n, [Bool; Bool] -> of_soc_key (("Lustre::impl"), types@[Bool], None) + | AstPredef.EQ_n, [Bool; Bool] -> of_soc_key (("Lustre::beq"), types@[Bool], None) + | AstPredef.EQ_n, [Int; Int] -> of_soc_key (("Lustre::ieq"), types@[Int], None) + | AstPredef.EQ_n, [Real; Real] -> of_soc_key (("Lustre::req"), types@[Real], None) + | AstPredef.NEQ_n, [Bool; Bool] -> of_soc_key (("Lustre::neq"), types@[Bool], None) + | AstPredef.NOT_n, [Bool] -> of_soc_key (("Lustre::not"), types@[Bool], None) | AstPredef.TRUE_n, [] -> finish_me lxm ; assert false (* todo *) | AstPredef.FALSE_n, [] -> finish_me lxm ; assert false (* todo *) @@ -337,14 +394,13 @@ let component_interface_of_predef: | AstPredef.INT2REAL_n, [Int] -> finish_me lxm ; assert false (* todo *) | AstPredef.NOR_n, _ -> finish_me lxm ; assert false (* todo *) | AstPredef.DIESE_n, _ -> finish_me lxm ; assert false (* todo *) - | AstPredef.IF_n, _ -> - let concrete_type = List.nth types 0 in - (match of_node_key (("Lustre","if"), []) with - | SC comp -> SC(instanciate_component comp concrete_type) - | Undef _ -> assert false - ) + | AstPredef.IF_n, [Bool; a ; b ] -> + let concrete_type = a in + let comp = of_soc_key (("Lustre::if"), types@[concrete_type], None) in + instanciate_component comp concrete_type (* « incorrect lic » *) + | AstPredef.IF_n, _ -> assert false | AstPredef.IUMINUS_n, _ -> assert false | AstPredef.IMINUS_n, _ -> assert false | AstPredef.RUMINUS_n, _ -> assert false @@ -379,10 +435,10 @@ let component_interface_of_predef: | AstPredef.EQ_n, _ -> assert false | AstPredef.NEQ_n, _ -> assert false | AstPredef.NOT_n, _ -> assert false - + let (component_interface_of_pos_op: - Lxm.t -> Lic.by_pos_op -> Soc.var_type list -> soc_comp_opt) = + Lxm.t -> Lic.by_pos_op -> Soc.var_type list -> Soc.t) = fun lxm op types -> match (op, types) with | Lic.PREDEF_CALL op, _ -> component_interface_of_predef lxm op types @@ -391,31 +447,25 @@ let (component_interface_of_pos_op: | Lic.FBY, _ -> let concrete_type = List.nth types 0 in - (match of_node_key (("Lustre","fby"), []) with - | SC comp -> SC(instanciate_component comp concrete_type) - | Undef _ -> assert false - ) + let comp = of_soc_key (("Lustre::fby"), types@[concrete_type], None) in + instanciate_component comp concrete_type | Lic.PRE, _ -> let concrete_type = List.nth types 0 in - (match of_node_key (("Lustre","pre"), []) with - | SC comp -> SC(instanciate_component comp concrete_type) - | Undef _ -> assert false - ) + let comp = of_soc_key (("Lustre::pre"), types@[concrete_type], None) in + instanciate_component comp concrete_type | Lic.CURRENT, _ -> let concrete_type = List.nth types 0 in - (match of_node_key (("Lustre","current"), []) with - | SC comp -> SC(instanciate_component comp concrete_type) - | Undef _ -> assert false - ) + let comp = of_soc_key (("Lustre::current"), types@[concrete_type], None) in + instanciate_component comp concrete_type | Lic.ARROW, _ -> let concrete_type = List.nth types 0 in - (match of_node_key (("Lustre","arrow"), []) with - | SC comp -> SC(instanciate_component comp concrete_type) - | Undef _ -> assert false - ) + let comp = of_soc_key (("Lustre::arrow"), types@[concrete_type], None) in + let soc = instanciate_component comp concrete_type in + SocUtils.string_of_component_ff soc Format.std_formatter; + soc | Lic.HAT i,_ -> let elt_type = List.nth types 0 in - SC(make_array_component i elt_type) + (make_array_component i elt_type) | Lic.ARRAY, _-> finish_me lxm ; assert false | Lic.CONCAT ,_-> finish_me lxm ; assert false @@ -437,7 +487,7 @@ dans des noeuds ? bon, je garde quelque temps en commentaire au cas ou... | Lic.Fill(node,size), _ | Lic.FillRed(node,size), _ | Lic.Red(node,size), _ -> - (match of_node_key node with + let comp = _key node with | Undef name -> Undef name (* Given - a node n of type @@ -447,7 +497,7 @@ dans des noeuds ? bon, je garde quelque temps en commentaire au cas ou... the red expression has the profile: tau * tau_1^c * ... * tau_n^c -> tau * teta_1^c * ... * teta_l^c *) - | SC c -> + | Some c -> let arrayse l = let exp (id,t) = match t with @@ -458,7 +508,7 @@ dans des noeuds ? bon, je garde quelque temps en commentaire au cas ou... | [] -> assert false | (id,t)::tail ->(id, t):: (List.map exp tail) in - SC { + Some { (* XXX la clef devrait contenir le node et la taille ? Les composants iterateurs ne meritent ils pas un traitement @@ -485,9 +535,9 @@ dans des noeuds ? bon, je garde quelque temps en commentaire au cas ou... } ) | Lic.Map(node,size), _ -> - (match of_node_key node with + let comp = _key node with | Undef name -> Undef name - | SC c -> + | Some c -> (* Given - a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l - an integer c @@ -503,7 +553,7 @@ dans des noeuds ? bon, je garde quelque temps en commentaire au cas ou... in (List.map exp l) in - SC { + Some { socc_key = ("map" ^ node ^ (string_of_int size), [], None); socc_profile = (arrayse (fst c.socc_profile), arrayse (snd c.socc_profile)); diff --git a/src/socPredef.mli b/src/socPredef.mli index 0e8b5f64..cffbcbe9 100644 --- a/src/socPredef.mli +++ b/src/socPredef.mli @@ -1,10 +1,9 @@ -(* Time-stamp: <modified the 21/02/2013 (at 10:19) by Erwan Jahier> *) +(* Time-stamp: <modified the 04/03/2013 (at 16:13) by Erwan Jahier> *) (** Synchronous Object Code for Predefined operators. *) -type soc_comp_opt = SC of Soc.component | Undef of Lic.node_key -val of_node_key : Lic.node_key -> soc_comp_opt +val of_soc_key : Soc.key -> Soc.t (** Associe un opérateur Lustre et le type de ses opérandes à un SOC et sa fonction de typage. @@ -13,7 +12,8 @@ val of_node_key : Lic.node_key -> soc_comp_opt *) val component_interface_of_pos_op: - Lxm.t -> Lic.by_pos_op -> Soc.var_type list -> soc_comp_opt + Lxm.t -> Lic.by_pos_op -> Soc.var_type list -> Soc.t +val instanciate_name : string -> Soc.var_type -> string diff --git a/src/socUtils.ml b/src/socUtils.ml index ccc34154..70d19de2 100644 --- a/src/socUtils.ml +++ b/src/socUtils.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 30/06/2009 (at 11:45) by Erwan Jahier> *) +(** Time-stamp: <modified the 01/03/2013 (at 16:14) by Erwan Jahier> *) open Soc @@ -8,7 +8,7 @@ open Soc C'est la liste des méthodes du composant, et la méthode d'initialisation le cas échéant. *) -let get_all_methods: component -> step_method list = fun c -> +let get_all_methods: Soc.t -> step_method list = fun c -> match c.socc_init with | None -> c.socc_step | Some m -> m :: c.socc_step @@ -60,18 +60,18 @@ and string_of_type_ref: (Soc.var_type -> string) = fun v -> (* Clé de composant *) -let string_of_component_key_ff: (Soc.component_key -> Format.formatter -> unit) = +let string_of_soc_key_ff: (Soc.key -> Format.formatter -> unit) = fun (id, types, si_opt) ff -> (match types with | [] -> fprintf ff "%s" id - | _ -> fprintf ff "(%s)%s" - (String.concat " * " (List.map string_of_type_ref types)) id); + | _ -> fprintf ff "%s:%s" id + (String.concat " -> " (List.map string_of_type_ref types))); (match si_opt with | None -> () | Some(f,l,step) -> fprintf ff "[%d .. %d step %d]" f l step) -let string_of_component_key: (Soc.component_key -> string) = fun v -> - call_fun_ff (string_of_component_key_ff v) +let string_of_soc_key: (Soc.key -> string) = fun v -> + call_fun_ff (string_of_soc_key_ff v) (* Variable *) @@ -95,7 +95,7 @@ let string_of_memory: (memory -> string) = fun v -> (* Déclaration d'une mémoire *) let string_of_memory_decl_ff: (memory -> Format.formatter -> unit) = fun v ff -> match v with - | CompMem(id, key) -> fprintf ff "%s : %s" id (string_of_component_key key) + | CompMem(id, key) -> fprintf ff "%s : %s" id (string_of_soc_key key) | VarMem v -> fprintf ff "%s" (string_of_var v) let string_of_memory_decl: (memory -> string) = fun v -> @@ -105,8 +105,8 @@ let string_of_memory_decl: (memory -> string) = fun v -> (* Opération *) let string_of_operation_ff: (atomic_operation -> Format.formatter -> unit) = fun v ff -> match v with | Assign -> () (* On suppose qu'il est déjà affiché dans string_of_gao *) - | Method(obj, meth) -> fprintf ff "%s.%s" (string_of_memory obj) meth - | Procedure proc -> fprintf ff "%s" proc + | Method(obj, meth) -> fprintf ff "%s.%s" (string_of_memory obj) (string_of_soc_key meth) + | Procedure proc -> fprintf ff "%s" (string_of_soc_key proc) let string_of_operation: (atomic_operation -> string) = fun v -> call_fun_ff (string_of_operation_ff v) @@ -117,7 +117,7 @@ let rec string_of_filter_ff: (Soc.var_expr -> Format.formatter -> unit) = fun v ff -> match v with | Const(id, _) | Var (id,_) -> fprintf ff "%s" id - | Field(f, id,_) -> string_of_filter_ff f ff; fprintf ff ".%s" id + | Field(f, (id,_)) -> string_of_filter_ff f ff; fprintf ff ".%s" id | Index(f, index,_) -> string_of_filter_ff f ff; fprintf ff "[%d]" index let string_of_filter: (Soc.var_expr -> string) = fun v -> @@ -163,7 +163,7 @@ let string_of_gaos_list: (gao list -> string) = fun v -> (* Profil de méthode *) -let string_interface_of_method_ff: (component -> step_method -> Format.formatter -> unit) = fun c m ff -> +let string_interface_of_method_ff: (Soc.t -> step_method -> Format.formatter -> unit) = fun c m ff -> let string_var_from_index: (Soc.var list -> int -> string) = fun vl i -> string_of_var (List.nth vl i) in @@ -173,12 +173,12 @@ let string_interface_of_method_ff: (component -> step_method -> Format.formatter (String.concat "; " (List.map (string_var_from_index (snd c.socc_profile)) m.socm_outputs)) -let string_interface_of_method: (component -> step_method -> string) = fun c m -> +let string_interface_of_method: (Soc.t -> step_method -> string) = fun c m -> call_fun_ff (string_interface_of_method_ff c m) (* Méthode complète *) -let string_of_method_ff: (component -> step_method -> Format.formatter -> unit) = fun c m ff -> +let string_of_method_ff: (Soc.t -> step_method -> Format.formatter -> unit) = fun c m ff -> fprintf ff "@[<v>@[<v 2>"; string_interface_of_method_ff c m ff; @@ -198,7 +198,7 @@ let string_of_method_ff: (component -> step_method -> Format.formatter -> unit) string_of_gaos_list_ff gaos ff; fprintf ff "@]@]@ }@]" -let string_of_method: (component -> step_method -> string) = fun c m -> +let string_of_method: (Soc.t -> step_method -> string) = fun c m -> call_fun_ff (string_of_method_ff c m) @@ -222,14 +222,14 @@ let string_of_profile: Soc.var list * Soc.var list -> string = fun profile -> (* Convertion des éléments d'un composant *) (* Convertion du profil ... *) -let string_of_component_profile_ff: (component -> Format.formatter -> unit) = fun comp ff -> +let string_of_component_profile_ff: (Soc.t -> Format.formatter -> unit) = fun comp ff -> string_of_profile_ff comp.socc_profile ff -let string_of_component_profile: (component -> string) = fun comp -> +let string_of_component_profile: (Soc.t -> string) = fun comp -> call_fun_ff (string_of_component_profile_ff comp) (* ... des contraintes *) -let string_of_comp_constraints_ff: (component -> Format.formatter -> unit) = fun comp ff -> +let string_of_comp_constraints_ff: (Soc.t -> Format.formatter -> unit) = fun comp ff -> fprintf ff "constraints: @["; match comp.socc_precedences with | [] -> fprintf ff "[]@]" @@ -238,8 +238,8 @@ let string_of_comp_constraints_ff: (component -> Format.formatter -> unit) = fun (String.concat "; " (List.map string_of_precedence comp.socc_precedences)) let string_of_component_factory_ff: ( - component -> Format.formatter -> - (component -> step_method -> Format.formatter -> unit) -> (* Formatage des méthodes *) + Soc.t -> Format.formatter -> + (Soc.t -> step_method -> Format.formatter -> unit) -> (* Formatage des méthodes *) (memory -> Format.formatter -> unit) option -> (* Formatage des mémoires *) unit ) = fun comp ff format_meth format_mem -> @@ -266,7 +266,7 @@ let string_of_component_factory_ff: ( in fprintf ff "@[<v>@[<v 2>component "; - string_of_component_key_ff comp.socc_key ff; + string_of_soc_key_ff comp.socc_key ff; fprintf ff ":@,@[<v>"; string_of_component_profile_ff comp ff; @@ -293,22 +293,22 @@ let string_of_component_factory_ff: ( (* Interface d'un composant *) -let string_interface_of_component_ff: (component -> Format.formatter -> unit) = fun comp ff -> +let string_interface_of_component_ff: (Soc.t -> Format.formatter -> unit) = fun comp ff -> string_of_component_factory_ff comp ff string_interface_of_method_ff None -let string_interface_of_component: (component -> string) = fun v -> +let string_interface_of_component: (Soc.t -> string) = fun v -> call_fun_ff (string_interface_of_component_ff v) (* Composant complet *) -let string_of_component_ff: (component -> Format.formatter -> unit) = fun comp ff -> +let string_of_component_ff: (Soc.t -> Format.formatter -> unit) = fun comp ff -> string_of_component_factory_ff comp ff string_of_method_ff (Some string_of_memory_decl_ff) -let string_of_component: (component -> string) = fun v -> +let string_of_component: (Soc.t -> string) = fun v -> call_fun_ff (string_of_component_ff v) @@ -348,7 +348,7 @@ let dump_entete oc = flush oc -let output: (bool -> string -> component list -> unit) = +let output: (bool -> string -> Soc.t list -> unit) = fun no_header pkg_name components -> let header = "Package '" ^ pkg_name ^ "' :" in let deco = (String.make (String.length header) '=') in @@ -359,3 +359,22 @@ let output: (bool -> string -> component list -> unit) = String.concat "\n\n" (List.map string_of_component components) ); flush stdout + + +let (find : Lxm.t -> Soc.key -> Soc.tbl -> Soc.t) = + fun lxm sk soc_tbl -> + try SocMap.find sk soc_tbl + with Not_found -> + let str_of_key = string_of_soc_key in + let nodes = SocMap.fold (fun sk _ acc -> (str_of_key sk)::acc) soc_tbl [] in + let nodes_str = String.concat "\n\t" nodes in + let msg = Printf.sprintf + ("Cannot find a soc for the node %s. \n Available nodes are: \n\t%s\n") + (str_of_key sk) + nodes_str + in + raise (Errors.Compile_error(lxm,msg)) + + + + diff --git a/src/socUtils.mli b/src/socUtils.mli index 3ce0371a..95b791d7 100644 --- a/src/socUtils.mli +++ b/src/socUtils.mli @@ -1,42 +1,44 @@ -(** Time-stamp: <modified the 25/02/2013 (at 18:03) by Erwan Jahier> *) +(** Time-stamp: <modified the 01/03/2013 (at 16:10) by Erwan Jahier> *) (** Donne toute les méthodes d'un composant. *) -val get_all_methods: Soc.component -> Soc.step_method list - +val get_all_methods: Soc.t -> Soc.step_method list + (** Fonctions de représentation des objets SOC. *) val string_of_type_ref : Soc.var_type -> string -val string_of_component_key : Soc.component_key -> string +val string_of_soc_key : Soc.key -> string val string_of_var : Soc.var -> string val string_of_memory : Soc.memory -> string val string_of_operation : Soc.atomic_operation -> string val string_of_gao : Soc.gao -> string val string_of_gaos_list : Soc.gao list -> string val string_of_filter : Soc.var_expr -> string -val string_of_method : Soc.component -> Soc.step_method -> string -val string_interface_of_method : Soc.component -> Soc.step_method -> string +val string_of_method : Soc.t -> Soc.step_method -> string +val string_interface_of_method : Soc.t -> Soc.step_method -> string val string_of_precedence : Soc.precedence -> string val string_of_profile : Soc.var list * Soc.var list -> string -val string_interface_of_component : Soc.component -> string -val string_of_component : Soc.component -> string +val string_interface_of_component : Soc.t -> string +val string_of_component : Soc.t -> string val string_of_type_ref_ff : Soc.var_type -> Format.formatter -> unit -val string_of_component_key_ff : Soc.component_key -> Format.formatter -> unit +val string_of_soc_key_ff : Soc.key -> Format.formatter -> unit val string_of_var_ff : Soc.var -> Format.formatter -> unit val string_of_memory_ff : Soc.memory -> Format.formatter -> unit val string_of_operation_ff : Soc.atomic_operation -> Format.formatter -> unit val string_of_filter_ff : Soc.var_expr -> Format.formatter -> unit val string_of_gao_ff : Soc.gao -> Format.formatter -> unit -val string_of_method_ff : Soc.component -> Soc.step_method -> Format.formatter -> unit -val string_interface_of_method_ff : Soc.component -> Soc.step_method -> Format.formatter -> unit +val string_of_method_ff : Soc.t -> Soc.step_method -> Format.formatter -> unit +val string_interface_of_method_ff : Soc.t -> Soc.step_method -> Format.formatter -> unit val string_of_precedence_ff : string * string list -> Format.formatter -> unit val string_of_profile_ff : Soc.var list * Soc.var list -> Format.formatter -> unit -val string_interface_of_component_ff : Soc.component -> Format.formatter -> unit -val string_of_component_ff : Soc.component -> Format.formatter -> unit +val string_interface_of_component_ff : Soc.t -> Format.formatter -> unit +val string_of_component_ff : Soc.t -> Format.formatter -> unit (** [output header_flag pack_name] dumps the soc list into a file. [header_flag] states whether or not headers (comment) should be printed *) -val output: bool -> string -> Soc.component list -> unit +val output: bool -> string -> Soc.t list -> unit + +val find : Lxm.t -> Soc.key -> Soc.tbl -> Soc.t diff --git a/test/lus2lic.sum b/test/lus2lic.sum index 3d235b10..d88bcb5d 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,4 +1,4 @@ -Test Run By jahier on Mon Feb 25 18:13:41 2013 +Test Run By jahier on Tue Mar 5 17:11:54 2013 Native configuration is i686-pc-linux-gnu === lus2lic tests === diff --git a/test/lus2lic.time b/test/lus2lic.time index 76997001..bc1f18b2 100644 --- a/test/lus2lic.time +++ b/test/lus2lic.time @@ -1,2 +1,2 @@ -testcase ./lus2lic.tests/non-reg.exp completed in 24 seconds +testcase ./lus2lic.tests/non-reg.exp completed in 53 seconds testcase ./lus2lic.tests/progression.exp completed in 0 seconds -- GitLab