From 51ed84504f484746acb0e8522a964105e680960f Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 13 Dec 2022 14:25:48 +0100 Subject: [PATCH] [pre propagation] done. --- src/ast_to_c.ml | 1 + src/main.ml | 36 +++++++++++++++++++----------- src/parser.mly | 4 ++-- src/passes.ml | 57 ++++++++++++++++++++++++++++++++++++++++++++--- src/test.node | 8 +------ src/test_pre.node | 4 ++++ src/utils.ml | 2 ++ 7 files changed, 87 insertions(+), 25 deletions(-) create mode 100644 src/test_pre.node diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index bef25dc..1b10fcb 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -169,6 +169,7 @@ let pp_expression node_name = | ETuple _ -> Format.fprintf fmt "%a" pp_expression_list expression; + | EAuto _ -> failwith "todo" in pp_expression_aux diff --git a/src/main.ml b/src/main.ml index f5d6788..4e87279 100644 --- a/src/main.ml +++ b/src/main.ml @@ -9,16 +9,20 @@ 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 run ast verbose debug passes = +let exec_passes ast verbose debug passes f = let rec aux ast = function - | [] -> Format.printf "%a" Ast_to_c.ast_to_c ast + | [] -> f ast | (n, p) :: passes -> + verbose (Format.asprintf "Executing pass %s:\n" n); match p ast with | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0) - | Some ast -> aux ast passes + | Some ast -> ( + debug (Format.asprintf "Current AST (after %s):\n%a\n" n Pp.pp_ast ast); + aux ast passes) in aux ast passes + let _ = (** Usage and argument parsing. *) let default_passes = ["pre2vars"] in @@ -45,7 +49,7 @@ let _ = if !source_file = "" then exit_error "No source file specified" else if !passes = [] then passes := default_passes; let print_verbose = print_verbose !verbose in - let print_debug = print_debug !verbose in + let print_debug = print_debug !debug in (** Definition of the passes table *) let passes_table : (string, t_nodelist -> t_nodelist option) Hashtbl.t = Hashtbl.create 100 in @@ -84,13 +88,19 @@ let _ = end in - if !ppast then Format.printf "%a" Pp.pp_ast ast - else - let passes = List.map (fun (pass: string) -> (pass, - match Hashtbl.find_opt passes_table pass with - | None -> - (exit_error (Format.sprintf "The pass %s does not exist." pass); exit 0) - | Some f -> - (print_debug ("The pass "^pass^" has been selected."); f))) !passes in - run ast print_verbose print_debug passes + let passes = List.map (fun (pass: string) -> (pass, + match Hashtbl.find_opt passes_table pass with + | None -> + (exit_error (Format.sprintf "The pass %s does not exist." pass); exit 0) + | Some f -> + (print_debug ("The pass "^pass^" has been selected."); f))) !passes in + + print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" + Pp.pp_ast ast) ; + exec_passes ast print_verbose print_debug passes + begin + if !ppast + then (Format.printf "%a" Pp.pp_ast) + else (Format.printf "%a" Ast_to_c.ast_to_c) + end diff --git a/src/parser.mly b/src/parser.mly index cd3b358..ba06788 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -342,14 +342,14 @@ expr: { let e1 = $1 in let t1 = type_exp e1 in let e2 = $3 in let t2 = type_exp e2 in if t2 = [TBool] - then EWhen (type_exp $1, $1, $3) + then EWhen (t1, e1, e2) else raise (MyParsingError ("The when does not type-check!", current_location())) } | expr RESET expr { let e1 = $1 in let t1 = type_exp e1 in let e2 = $3 in let t2 = type_exp e2 in if t2 = [TBool] - then EReset (type_exp $1, $1, $3) + then EReset (t1, e1, e2) else raise (MyParsingError ("The reset does not type-check!", current_location())) } /* Constants */ diff --git a/src/passes.ml b/src/passes.ml index 155dd04..0d46f62 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -34,10 +34,60 @@ let expression_pass f: t_nodelist -> t_nodelist option = equation_pass aux let pre2vars = - let rec aux = function - | EVar (ty, v) -> EVar (ty, v) + 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 (Utils.type_exp expr, MOp_pre, expr) + | EConst _ -> expr (** pre(c) = c for any constant c *) | EMonOp (ty, mop, expr) -> - let expr = aux expr in 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) + | EAuto _ -> failwith "toto" + 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') @@ -62,6 +112,7 @@ let pre2vars = | EApp (ty, node, arg) -> let arg = aux arg in EApp (ty, node, arg) + | EAuto _ -> failwith "todo" in expression_pass (Utils.somify aux) diff --git a/src/test.node b/src/test.node index ed4b77a..af937b1 100644 --- a/src/test.node +++ b/src/test.node @@ -6,14 +6,8 @@ tel node undiag_test (i: int) returns (o : bool); var l1, l2: int; l3: int; let - l3 = 1 -> 0; + l3 = (pre (1)) -> 0; (l1, l2) = diagonal_int(i); o = (not (not (l1 = l2))) and (l1 = l2) and true; tel -node automaton () returns (o : bool); -let - automaton - | Incr -> do o = (pre o) + 1 done - | Decr -> do o = (pre o) - 1 done -tel diff --git a/src/test_pre.node b/src/test_pre.node new file mode 100644 index 0000000..7f30528 --- /dev/null +++ b/src/test_pre.node @@ -0,0 +1,4 @@ +node n2 (i: int) returns (o: bool); +let + o = pre (true and pre( i = pre(pre(i)))); +tel diff --git a/src/utils.ml b/src/utils.ml index 0029c14..9ad4f28 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -32,5 +32,7 @@ let type_exp : t_expression -> full_ty = function | EConst (full_ty , _) -> full_ty | ETuple (full_ty , _) -> full_ty | EApp (full_ty , _ , _) -> full_ty + | EAuto _ -> raise (MyParsingError ("bloup", Parsing.(symbol_start_pos(), + symbol_end_pos()))) let somify f = fun e -> Some (f e)