[pre propagation] done.
This commit is contained in:
parent
e9d586dfe7
commit
51ed84504f
@ -169,6 +169,7 @@ let pp_expression node_name =
|
|||||||
| ETuple _ ->
|
| ETuple _ ->
|
||||||
Format.fprintf fmt "%a"
|
Format.fprintf fmt "%a"
|
||||||
pp_expression_list expression;
|
pp_expression_list expression;
|
||||||
|
| EAuto _ -> failwith "todo"
|
||||||
in
|
in
|
||||||
pp_expression_aux
|
pp_expression_aux
|
||||||
|
|
||||||
|
24
src/main.ml
24
src/main.ml
@ -9,16 +9,20 @@ let print_debug d s =
|
|||||||
let print_verbose v s =
|
let print_verbose v s =
|
||||||
if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else ()
|
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
|
let rec aux ast = function
|
||||||
| [] -> Format.printf "%a" Ast_to_c.ast_to_c ast
|
| [] -> f ast
|
||||||
| (n, p) :: passes ->
|
| (n, p) :: passes ->
|
||||||
|
verbose (Format.asprintf "Executing pass %s:\n" n);
|
||||||
match p ast with
|
match p ast with
|
||||||
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
|
| 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
|
in
|
||||||
aux ast passes
|
aux ast passes
|
||||||
|
|
||||||
|
|
||||||
let _ =
|
let _ =
|
||||||
(** Usage and argument parsing. *)
|
(** Usage and argument parsing. *)
|
||||||
let default_passes = ["pre2vars"] in
|
let default_passes = ["pre2vars"] in
|
||||||
@ -45,7 +49,7 @@ let _ =
|
|||||||
if !source_file = "" then exit_error "No source file specified" else
|
if !source_file = "" then exit_error "No source file specified" else
|
||||||
if !passes = [] then passes := default_passes;
|
if !passes = [] then passes := default_passes;
|
||||||
let print_verbose = print_verbose !verbose in
|
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 *)
|
(** Definition of the passes table *)
|
||||||
let passes_table : (string, t_nodelist -> t_nodelist option) Hashtbl.t = Hashtbl.create 100 in
|
let passes_table : (string, t_nodelist -> t_nodelist option) Hashtbl.t = Hashtbl.create 100 in
|
||||||
@ -84,13 +88,19 @@ let _ =
|
|||||||
end
|
end
|
||||||
in
|
in
|
||||||
|
|
||||||
if !ppast then Format.printf "%a" Pp.pp_ast ast
|
|
||||||
else
|
|
||||||
let passes = List.map (fun (pass: string) -> (pass,
|
let passes = List.map (fun (pass: string) -> (pass,
|
||||||
match Hashtbl.find_opt passes_table pass with
|
match Hashtbl.find_opt passes_table pass with
|
||||||
| None ->
|
| None ->
|
||||||
(exit_error (Format.sprintf "The pass %s does not exist." pass); exit 0)
|
(exit_error (Format.sprintf "The pass %s does not exist." pass); exit 0)
|
||||||
| Some f ->
|
| Some f ->
|
||||||
(print_debug ("The pass "^pass^" has been selected."); f))) !passes in
|
(print_debug ("The pass "^pass^" has been selected."); f))) !passes in
|
||||||
run ast print_verbose print_debug passes
|
|
||||||
|
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
|
||||||
|
|
||||||
|
@ -342,14 +342,14 @@ expr:
|
|||||||
{ let e1 = $1 in let t1 = type_exp e1 in
|
{ let e1 = $1 in let t1 = type_exp e1 in
|
||||||
let e2 = $3 in let t2 = type_exp e2 in
|
let e2 = $3 in let t2 = type_exp e2 in
|
||||||
if t2 = [TBool]
|
if t2 = [TBool]
|
||||||
then EWhen (type_exp $1, $1, $3)
|
then EWhen (t1, e1, e2)
|
||||||
else raise (MyParsingError ("The when does not type-check!",
|
else raise (MyParsingError ("The when does not type-check!",
|
||||||
current_location())) }
|
current_location())) }
|
||||||
| expr RESET expr
|
| expr RESET expr
|
||||||
{ let e1 = $1 in let t1 = type_exp e1 in
|
{ let e1 = $1 in let t1 = type_exp e1 in
|
||||||
let e2 = $3 in let t2 = type_exp e2 in
|
let e2 = $3 in let t2 = type_exp e2 in
|
||||||
if t2 = [TBool]
|
if t2 = [TBool]
|
||||||
then EReset (type_exp $1, $1, $3)
|
then EReset (t1, e1, e2)
|
||||||
else raise (MyParsingError ("The reset does not type-check!",
|
else raise (MyParsingError ("The reset does not type-check!",
|
||||||
current_location())) }
|
current_location())) }
|
||||||
/* Constants */
|
/* Constants */
|
||||||
|
@ -34,10 +34,60 @@ let expression_pass f: t_nodelist -> t_nodelist option =
|
|||||||
equation_pass aux
|
equation_pass aux
|
||||||
|
|
||||||
let pre2vars =
|
let pre2vars =
|
||||||
let rec aux = function
|
let rec all_pre expr =
|
||||||
| EVar (ty, v) -> EVar (ty, v)
|
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) ->
|
| 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') ->
|
| EBinOp (ty, bop, expr, expr') ->
|
||||||
let expr = aux expr in let expr' = aux expr' in
|
let expr = aux expr in let expr' = aux expr' in
|
||||||
EBinOp (ty, bop, expr, expr')
|
EBinOp (ty, bop, expr, expr')
|
||||||
@ -62,6 +112,7 @@ let pre2vars =
|
|||||||
| EApp (ty, node, arg) ->
|
| EApp (ty, node, arg) ->
|
||||||
let arg = aux arg in
|
let arg = aux arg in
|
||||||
EApp (ty, node, arg)
|
EApp (ty, node, arg)
|
||||||
|
| EAuto _ -> failwith "todo"
|
||||||
in
|
in
|
||||||
expression_pass (Utils.somify aux)
|
expression_pass (Utils.somify aux)
|
||||||
|
|
||||||
|
@ -6,14 +6,8 @@ tel
|
|||||||
node undiag_test (i: int) returns (o : bool);
|
node undiag_test (i: int) returns (o : bool);
|
||||||
var l1, l2: int; l3: int;
|
var l1, l2: int; l3: int;
|
||||||
let
|
let
|
||||||
l3 = 1 -> 0;
|
l3 = (pre (1)) -> 0;
|
||||||
(l1, l2) = diagonal_int(i);
|
(l1, l2) = diagonal_int(i);
|
||||||
o = (not (not (l1 = l2))) and (l1 = l2) and true;
|
o = (not (not (l1 = l2))) and (l1 = l2) and true;
|
||||||
tel
|
tel
|
||||||
|
|
||||||
node automaton () returns (o : bool);
|
|
||||||
let
|
|
||||||
automaton
|
|
||||||
| Incr -> do o = (pre o) + 1 done
|
|
||||||
| Decr -> do o = (pre o) - 1 done
|
|
||||||
tel
|
|
||||||
|
4
src/test_pre.node
Normal file
4
src/test_pre.node
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
node n2 (i: int) returns (o: bool);
|
||||||
|
let
|
||||||
|
o = pre (true and pre( i = pre(pre(i))));
|
||||||
|
tel
|
@ -32,5 +32,7 @@ let type_exp : t_expression -> full_ty = function
|
|||||||
| EConst (full_ty , _) -> full_ty
|
| EConst (full_ty , _) -> full_ty
|
||||||
| ETuple (full_ty , _) -> full_ty
|
| ETuple (full_ty , _) -> full_ty
|
||||||
| EApp (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)
|
let somify f = fun e -> Some (f e)
|
||||||
|
Loading…
Reference in New Issue
Block a user