From c344f125e55384d9f9f78c572d14f2c107046437 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Sun, 18 Dec 2022 19:00:24 +0100 Subject: [PATCH] [passes] linearization of tuple-equations + deletion of unused pass --- src/main.ml | 11 ++-- src/passes.ml | 138 +++++++++++--------------------------------------- src/test.node | 12 +++-- 3 files changed, 42 insertions(+), 119 deletions(-) diff --git a/src/main.ml b/src/main.ml index 78e1dc1..8c0fc97 100644 --- a/src/main.ml +++ b/src/main.ml @@ -9,12 +9,12 @@ let print_debug d s = let print_verbose v s = if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else () -let exec_passes ast main_fn verbose debug passes f = +let exec_passes ast verbose debug passes f = let rec aux ast = function | [] -> f ast | (n, p) :: passes -> verbose (Format.asprintf "Executing pass %s:\n" n); - match p verbose debug main_fn ast with + match p verbose debug ast with | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0) | Some ast -> ( debug (Format.asprintf "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast); @@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = [] in + let default_passes = ["linearization_tuples"; "linearization"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -57,13 +57,12 @@ let _ = if !passes = [] then passes := default_passes; let print_verbose = print_verbose !verbose in let print_debug = print_debug !debug in - let main_fn = "main" in (** Definition of the passes table *) let passes_table = Hashtbl.create 100 in List.iter (fun (s, k) -> Hashtbl.add passes_table s k) [ - ("pre2vars", Passes.pre2vars); + ("linearization_tuples", Passes.pass_linearization_tuples); ("chkvar_init_unicity", Passes.chkvar_init_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); @@ -120,7 +119,7 @@ let _ = print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" Lustre_pp.pp_ast ast) ; - exec_passes ast main_fn print_verbose print_debug passes + exec_passes ast print_verbose print_debug passes begin if !ppast then (Format.printf "%a" Lustre_pp.pp_ast) diff --git a/src/passes.ml b/src/passes.ml index 179242f..4cc32fe 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -4,88 +4,29 @@ open Ast open Passes_utils open Utils -let pre2vars verbose debug main_fn = - let rec all_pre expr = - match expr with - | EMonOp (ty, MOp_pre, expr) -> all_pre expr - | EMonOp _ -> false - | EVar _ -> true - | _ -> false - in - let rec pre_push expr : t_expression = - match expr with - | EVar _ -> EMonOp (type_exp expr, MOp_pre, expr) - | EConst _ -> expr (** pre(c) = c for any constant c *) - | EMonOp (ty, mop, expr) -> - begin - match mop with - | MOp_pre -> - if all_pre expr - then EMonOp (ty, mop, EMonOp (ty, mop, expr)) - else pre_push (pre_push expr) - | _ -> EMonOp (ty, mop, pre_push expr) - end - | EBinOp (ty, bop, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EBinOp (ty, bop, expr, expr') - | ETriOp (ty, top, expr, expr', expr'') -> - let expr = pre_push expr in let expr' = pre_push expr' in - let expr'' = pre_push expr'' in - ETriOp (ty, top, expr, expr', expr'') - | EComp (ty, cop, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EComp (ty, cop, expr, expr') - | EWhen (ty, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EWhen (ty, expr, expr') - | EReset (ty, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EReset (ty, expr, expr') - | ETuple (ty, elist) -> - let elist = - List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in - ETuple (ty, elist) - | EApp (ty, node, arg) -> - let arg = pre_push arg in - EApp (ty, node, arg) - in - let rec aux (expr: t_expression) = - match expr with - | EVar _ -> expr - | EMonOp (ty, mop, expr) -> - begin - match mop with - | MOp_pre -> pre_push expr - | _ -> let expr = aux expr in EMonOp (ty, mop, expr) - end - | EBinOp (ty, bop, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EBinOp (ty, bop, expr, expr') - | ETriOp (ty, top, expr, expr', expr'') -> - let expr = aux expr in let expr' = aux expr' in - let expr'' = aux expr'' in - ETriOp (ty, top, expr, expr', expr'') - | EComp (ty, cop, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EComp (ty, cop, expr, expr') - | EWhen (ty, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EWhen (ty, expr, expr') - | EReset (ty, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EReset (ty, expr, expr') - | EConst (ty, c) -> EConst (ty, c) - | ETuple (ty, elist) -> - let elist = - List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in - ETuple (ty, elist) - | EApp (ty, node, arg) -> - let arg = aux arg in - EApp (ty, node, arg) - in - expression_pass (somify aux) +let rec split_tuple (eq: t_equation): t_eqlist = + let patt, expr = eq in + match expr with + | ETuple (_, expr_h :: expr_t) -> + begin + let t_l = type_exp expr_h in + let patt_l, patt_r = list_select (List.length t_l) (snd patt) in + let t_r = List.flatten (List.map type_var patt_r) in + ((t_l, patt_l), expr_h) :: + split_tuple ((t_r, patt_r), ETuple (t_r, expr_t)) + end + | ETuple (_, []) -> [] + | _ -> [eq] -let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option = + +let pass_linearization_tuples verbose debug = + let aux_linearization_tuples node = + let new_equations = List.flatten (List.map split_tuple node.n_equations) in + Some { node with n_equations = new_equations } + in + node_pass aux_linearization_tuples + +let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = let aux (node: t_node) : t_node option = let incr_aux h n = match Hashtbl.find_opt h n with @@ -171,7 +112,7 @@ let rec tpl debug ((pat, exp): t_equation) = | ETuple (_, []) -> [] | _ -> [(pat, exp)] -let pass_linearization verbose debug main_fn = +let pass_linearization verbose debug = let node_lin (node: t_node): t_node option = let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression = match expr with @@ -237,34 +178,13 @@ let pass_linearization verbose debug main_fn = let eqs, vars, expr = pre_aux_expression vars expr in (patt, expr)::eqs, vars in - let rec tpl ((pat, exp): t_equation) = - match exp with - | ETuple (_, hexps :: texps) -> - debug "An ETuple has been recognized, inlining..."; - let p1, p2 = - list_select - (List.length (type_exp hexps)) - (snd pat) in - let t1 = List.flatten (List.map type_var p1) in - let t2 = List.flatten (List.map type_var p2) in - ((t1, p1), hexps) - :: (tpl ((t2, p2), - ETuple (List.flatten (List.map type_exp texps), texps))) - | ETuple (_, []) -> [] - | _ -> [(pat, exp)] - in - let new_equations = List.flatten - (List.map - tpl - node.n_equations) - in let new_equations, new_locvars = List.fold_left (fun (eqs, vars) eq -> let es, vs = pre_aux_equation vars eq in es @ eqs, vs) ([], node.n_local_vars) - new_equations + node.n_equations in Some { @@ -278,7 +198,7 @@ let pass_linearization verbose debug main_fn = in node_pass node_lin -let pass_eq_reordering verbose debug main_fn ast = +let pass_eq_reordering verbose debug ast = let rec pick_equations init_vars eqs remaining_equations = match remaining_equations with | [] -> Some eqs @@ -312,7 +232,7 @@ let pass_eq_reordering verbose debug main_fn ast = in node_pass node_eq_reorganising ast -let pass_typing verbose debug main_fn ast = +let pass_typing verbose debug ast = let htbl = Hashtbl.create (List.length ast) in let () = debug "[typing verification]" in let () = List.iter @@ -382,7 +302,7 @@ let pass_typing verbose debug main_fn ast = else None in aux ast -let check_automata_validity verbos debug main_fn = +let check_automata_validity verbos debug = let check_automaton_branch_vars automaton = let (init, states) = automaton in let left_side = Hashtbl.create 10 in @@ -539,10 +459,10 @@ let automata_trans_pass debug (node:t_node) : t_node option= n_automata = []; (* not needed anymore *) } -let automata_translation_pass verbose debug main_fn = +let automata_translation_pass verbose debug = node_pass (automata_trans_pass debug) -let clock_unification_pass verbose debug main_fn ast = +let clock_unification_pass verbose debug ast = let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in diff --git a/src/test.node b/src/test.node index 5fb4a8f..faa8355 100644 --- a/src/test.node +++ b/src/test.node @@ -1,6 +1,10 @@ -node n (i: int) returns (o: int); -var v: int; +node my_and (a, b: bool) returns (o: bool); let - o = 1; - v = pre o; + o = a and b; +tel + +node n (i: int) returns (o: int); +var v: bool; +let + (o, v) = (1, my_and (pre o = 8, pre v)); tel