From ad5c6641e31166a3e76fa61c8bd069f8d67c18ae Mon Sep 17 00:00:00 2001 From: Marc Pouzet Date: Fri, 25 Oct 2024 10:44:40 +0200 Subject: [PATCH] Cleaning; add markfunctions; and a few things. --- Makefile | 6 +- src/Makefile | 2 - src/compiler/main/compiler.ml | 20 +- src/compiler/main/zeluc.ml | 32 ++- src/compiler/main/zwrite.ml | 100 ------- src/compiler/rewrite/markfunctions.ml | 310 +++++----------------- src/compiler/{main => rewrite}/rewrite.ml | 116 ++------ src/compiler/typing/typing.ml | 2 +- src/ctests/good/1.zci | Bin 0 -> 547 bytes src/ctests/good/2.zci | Bin 0 -> 547 bytes src/ctests/good/3.zci | Bin 180 -> 304 bytes src/ctests/good/3.zls | 3 +- src/dune | 35 +-- src/global/misc.ml | 4 +- src/typdefs/typinfo.ml | 1 + 15 files changed, 165 insertions(+), 466 deletions(-) delete mode 100644 src/compiler/main/zwrite.ml rename src/compiler/{main => rewrite}/rewrite.ml (55%) create mode 100644 src/ctests/good/1.zci create mode 100644 src/ctests/good/2.zci diff --git a/Makefile b/Makefile index 0cfcfb33..857795ba 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,5 @@ ## Build the compiler and libraries -all: zwrite.exe zeluc.exe - -zwrite.exe: - (cd src; dune build -- zwrite.exe) +all: zeluc.exe zeluc.exe: (cd src; dune build -- zeluc.exe) @@ -11,7 +8,6 @@ tests: (cd tests; dune test) debug: - (cd src; dune build --debug-backtraces --debug-dependency-path -- zwrite.bc) (cd src; dune build --debug-backtraces --debug-dependency-path -- zeluc.bc) clean: diff --git a/src/Makefile b/src/Makefile index 9af1b8f1..5914f4fa 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,10 +1,8 @@ all: - dune build -- zwrite.exe dune build -- zeluc.exe dune build lib debug: - dune build --debug-backtraces --debug-dependency-path -- zwrite.bc dune build --debug-backtraces --debug-dependency-path -- zeluc.bc clean: diff --git a/src/compiler/main/compiler.ml b/src/compiler/main/compiler.ml index 92c2c03d..bd00e2dc 100644 --- a/src/compiler/main/compiler.ml +++ b/src/compiler/main/compiler.ml @@ -139,12 +139,28 @@ let compile modname filename = (Typing.program info_ff true) p in let p = do_optional_step !Misc.no_causality "Causality done. See below:" Debug.print_program (Causality.program info_ff) p in - let _ = do_optional_step + let p = do_optional_step !Misc.no_initialization "Initialization done. See below:" Debug.print_program (Initialization.program info_ff) p in (* Write the symbol table into the interface file *) let itc = open_out_bin obj_interf_name in + apply_with_close_out Modules.write itc; if !Misc.typeonly then raise Stop; - apply_with_close_out Modules.write itc + + (* Mark functions calls to be inlined. This step uses type informations *) + (* computed during the causality analysis *) + let _ = do_step "Mark functions calls to be inlined. See below:" + Debug.print_program Markfunctions.program p in + + (* source-to-source transformations *) + + (* defines the initial global environment for values *) + let genv0 = Genv.initialize modname [] in + (* Add Stdlib *) + let genv0 = Genv.add_module genv0 (Primitives.stdlib_env ()) in + + let _ = Rewrite.main print_message genv0 p !Misc.n_steps in + + () with | Stop -> () diff --git a/src/compiler/main/zeluc.ml b/src/compiler/main/zeluc.ml index 761051e9..3c44517a 100644 --- a/src/compiler/main/zeluc.ml +++ b/src/compiler/main/zeluc.ml @@ -56,23 +56,38 @@ and doc_simulation = \t\t where is equal to the argument of -o if the flag\n\ \t\t has been set, or otherwise" and doc_sampling = "

\t Sets the sampling period to p (float <= 1.0)" -and doc_check = " \t Check that the simulated node returns true for n steps" and doc_use_gtk = "\t Use lablgtk2 interface." and doc_inlining_level = " \t Level of inlining" and doc_inline_all = "\t Inline all function calls" and doc_dzero = "\t Turn on discrete zero-crossing detection" and doc_nocausality = "\t (undocumented)" -and doc_no_deadcode = "\t (undocumented)" and doc_no_initialization = "\t (undocumented)" and doc_nosimplify = "\t (undocumented)" -and doc_noreduce = "\t (undocumented)" -and doc_lmm = "\t Translate the node into Lustre--" -and doc_red_name = "\t Static reduction for" +and doc_no_deadcode = "\t (undocumented)" and doc_zsign = "\t Use the sign function for the zero-crossing argument" and doc_with_copy = "\t Add of a copy method for the state" -and doc_rif = "\t Use RIF format over stdin and stdout to communicate I/O to the node being simulated" and doc_no_opt = "\t (undocumented)" and doc_no_warning = "\t Turn off warnings" +and doc_check = " \t Check equivalence for that amount of steps" +and doc_set_steps = "\t Option to control source-to-source rewriting steps\n\ + \t\t + turn on step s\n\ + \t\t - turn off step s\n\ + \t\t s can be: +a: takes all; -a: takes none\n\ + \t\t static: static reduction \n\ + \t\t inline: inlining \n\ + \t\t der: normalize derivative \n\ + \t\t copylast: add copy equations [lx = last* x] for lasts \n\ + \t\t lastinpatterns: add copies for lasts that are inputs or outputs \n\ + \t\t auto: remove automata statements \n\ + \t\t present: remove present statements \n\ + \t\t pre: remove pre/fby \n\ + \t\t reset: normalise resets; remove initialization (->) \n\ + \t\t complete: complete branches \n\ + \t\t encore: add an extra step when a zero-crossing \n\ + \t\t\t change a discrete-time state variable \n\ + \t\t letin: fuse blocks \n\ + \t\t schedule: static scheduling \n\ + \t\t Example: -step -a+step+inline+static. Default is +a." let errmsg = "Options are:" let set_verbose () = @@ -116,7 +131,10 @@ let main () = "-inlineall", Arg.Set inline_all, doc_inline_all; "-zsign", Arg.Set zsign, doc_zsign; "-copy", Arg.Set with_copy, doc_with_copy; - "-rif", Arg.Set use_rif, doc_rif; + "-check", Arg.Int set_check_equivalence_for_n_steps, doc_check; + "-inline", Arg.Int Misc.set_inlining_level, doc_inlining_level; + "-inlineall", Arg.Set inline_all, doc_inline_all; + "-step", Arg.String Rewrite.set_steps, doc_set_steps; ]) compile errmsg; diff --git a/src/compiler/main/zwrite.ml b/src/compiler/main/zwrite.ml deleted file mode 100644 index 52e868b9..00000000 --- a/src/compiler/main/zwrite.ml +++ /dev/null @@ -1,100 +0,0 @@ -(***********************************************************************) -(* *) -(* *) -(* The ZRun Interpreter *) -(* *) -(* Marc Pouzet *) -(* *) -(* (c) 2020-2024 Inria Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed under *) -(* the terms of the INRIA Non-Commercial License Agreement (see the *) -(* LICENSE file). *) -(* *) -(* *********************************************************************) - - -(* the main *) -open Misc - -let main file = - if Filename.check_suffix file ".zls" - then - let filename = Filename.chop_extension file in - let modname = String.capitalize_ascii (Filename.basename filename) in - let n_steps = !equivalence_checking in - Rewrite.main modname filename n_steps - else raise (Arg.Bad "Expected *.zls file.") - -let doc_main = "\tThe main node to evaluate" -let doc_all = "\tEvaluate all nodes" -let doc_number_of_steps = "\tThe number of steps" -let doc_verbose = "\tVerbose mode" -let doc_vverbose = "\t Set even more verbose mode" -let doc_debug = "\t Set debug mode" -let doc_no_assert = "\tNo check of assertions" -let doc_nocausality = "\tTurn off the check that all variables are non bottom" -let doc_print_values = "\tPrint values" -let doc_number_of_fixpoint_iterations = - "\tPrint the number of steps for fixpoints" -let doc_esterel = - "\tSets the interpretation of if/then/else to be constructive" -let doc_lustre = - "\tSets the interpretation of if/then/else to be strict \n\ - \t\t(that of Lustre)" -let doc_static_reduction = - "\tReduce static (compile-time) expressions" -let doc_check = - " \t Check equivalence for that amount of steps" -and doc_inlining_level = " \t Level of inlining" -and doc_inline_all = "\t Inline all function calls" -and doc_set_steps = "\t Option to control source-to-source rewriting steps\n\ - \t\t + turn on step s\n\ - \t\t - turn off step s\n\ - \t\t s can be: +a: takes all; -a: takes none\n\ - \t\t static: static reduction \n\ - \t\t inline: inlining \n\ - \t\t der: normalize derivative \n\ - \t\t copylast: add copy equations [lx = last* x] for lasts \n\ - \t\t lastinpatterns: add copies for lasts that are inputs or outputs \n\ - \t\t auto: remove automata statements \n\ - \t\t present: remove present statements \n\ - \t\t pre: remove pre/fby \n\ - \t\t reset: normalise resets; remove initialization (->) \n\ - \t\t complete: complete branches \n\ - \t\t encore: add an extra step when a zero-crossing \n\ - \t\t\t change a discrete-time state variable \n\ - \t\t letin: fuse blocks \n\ - \t\t schedule: static scheduling \n\ - \t\t Example: -step -a+step+inline+static. Default is +a." -let errmsg = "Options are:" - - -let main () = - try - Arg.parse - (Arg.align - [ "-v", Arg.Unit Misc.set_verbose, doc_verbose; - "-vv", Arg.Unit Misc.set_vverbose, doc_vverbose; - "-debug", Arg.Unit Misc.set_debug, doc_debug; - "-print", Arg.Set Misc.print_values, doc_print_values; - "-noassert", Arg.Set Misc.no_assert, doc_no_assert; - "-nocausality", Arg.Set Misc.no_causality, doc_nocausality; - "-fix", Arg.Set Misc.print_number_of_fixpoint_iterations, - doc_number_of_fixpoint_iterations; - "-esterel", Arg.Set Misc.esterel, doc_esterel; - "-lustre", Arg.Set Misc.lustre, doc_lustre; - "-check", Arg.Int set_equivalence_checking, doc_check; - "-inline", Arg.Int Misc.set_inlining_level, doc_inlining_level; - "-inlineall", Arg.Set inline_all, doc_inline_all; - "-step", Arg.String Rewrite.set_steps, doc_set_steps; - ]) - main - errmsg - with - | Misc.Error -> exit 2 - -let _ = main () -let _ = exit 0 - diff --git a/src/compiler/rewrite/markfunctions.ml b/src/compiler/rewrite/markfunctions.ml index 48fd23f3..2cd982c2 100644 --- a/src/compiler/rewrite/markfunctions.ml +++ b/src/compiler/rewrite/markfunctions.ml @@ -3,7 +3,7 @@ (* *) (* Zelus, a synchronous language for hybrid systems *) (* *) -(* (c) 2020 Inria Paris (see the AUTHORS file) *) +(* (c) 2024 Inria Paris (see the AUTHORS file) *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed under *) @@ -18,7 +18,7 @@ open Zelus -type info = +type io_table = { inputs: Causal.S.t; (* the causality tags of inputs of the function *) outputs: Causal.S.t; (* the causality tags of outputs *) o_table: Causal.S.t Causal.M.t; (* outputs of a causality tag *) @@ -48,122 +48,44 @@ type info = *- on all of its inputs *) (* compute the set of causality tags that appear as input/outputs *) -(* of function applications *) -let funexp_info { f_args = p_list; f_body = ({ e_caus = tc } as e) } = - let rec exp c_set { e_desc = desc; e_caus = tc } = - match desc with - | Elocal _ | Eglobal _ | Econst _ - | Econstr0 _ | Elast _ -> c_set - | Eapp(_, op, arg_list) -> - let c_set = List.fold_left exp (exp c_set op) arg_list in - (* compute the set of causality tags *) - let tc_list = List.map (fun { e_caus = tc } -> tc) (op :: arg_list) in - List.fold_left Causal.vars (Causal.vars c_set tc) tc_list - | Eop(_, e_list) | Etuple(e_list) - | Econstr1(_, e_list) -> List.fold_left exp c_set e_list - | Erecord_access(e, _) | Etypeconstraint(e, _) -> exp c_set e - | Erecord(m_e_list) -> - List.fold_left (fun acc (_, e) -> exp acc e) c_set m_e_list - | Erecord_with(e_record, m_e_list) -> - List.fold_left (fun acc (_, e) -> exp acc e) - (exp c_set e_record) m_e_list - | Epresent(p_h_list, e_opt) -> - let c_set = - List.fold_left - (fun acc { p_body = e } -> exp acc e) c_set p_h_list in - Zmisc.optional exp c_set e_opt - | Ematch(_, e, m_h_list) -> - List.fold_left - (fun acc { m_body = e } -> exp acc e) (exp c_set e) m_h_list - | Elet(l, e) -> exp (local c_set l) e - | Eblock(b, e) -> exp (block_eq_list c_set b) e - | Eseq(e1, e2) -> exp (exp c_set e1) e2 - | Eperiod { p_phase = p1; p_period = p2 } -> - let c_set = Zmisc.optional exp c_set p1 in - exp c_set p2 - - and local c_set { l_eq = eq_list } = List.fold_left equation c_set eq_list - - and equation c_set { eq_desc = desc } = - match desc with - | EQeq(_, e) | EQpluseq(_, e) | EQinit(_, e) -> exp c_set e - | EQder(_, e, e_opt, p_h_list) -> - let c_set = Zmisc.optional exp (exp c_set e) e_opt in - List.fold_left (fun acc { p_body = e } -> exp acc e) c_set p_h_list - | EQnext(n, e, e_opt) -> - Zmisc.optional exp (exp c_set e) e_opt - | EQautomaton(_, s_h_list, se_opt) -> - let c_set = - List.fold_left - (fun acc { s_body = b_eq_list; s_trans = s_trans } -> - let acc = block_eq_list acc b_eq_list in - List.fold_left - (fun acc - { e_cond = scpat; e_block = b_opt; e_next_state = se } -> - let c_set = scondpat acc scpat in - let c_set = Zmisc.optional block_eq_list c_set b_opt in - state c_set se) - acc s_trans) - c_set s_h_list in - Zmisc.optional state c_set se_opt - | EQpresent(p_h_list, b_opt) -> - let c_set = - List.fold_left - (fun acc { p_cond = scpat; p_body = b_eq_list } -> - let acc = scondpat acc scpat in - block_eq_list acc b_eq_list) c_set p_h_list in - Zmisc.optional block_eq_list c_set b_opt - | EQmatch(_, e, m_h_list) -> - List.fold_left - (fun acc { m_body = b_eq_list } -> block_eq_list acc b_eq_list) - (exp c_set e) m_h_list - | EQreset(res_eq_list, e) -> - List.fold_left equation (exp c_set e) res_eq_list - | EQand(eq_list) | EQbefore(eq_list) -> - List.fold_left equation c_set eq_list - | EQemit(_, e_opt) -> Zmisc.optional exp c_set e_opt - | EQblock(b) -> block_eq_list c_set b - | EQforall({ for_index = i_list; for_init = init_list; - for_body = b_eq_list }) -> - let index c_set { desc = desc } = - match desc with - | Einput(_, e) -> exp c_set e - | Eindex(_, e1, e2) -> exp (exp c_set e1) e2 - | Eoutput _ -> c_set in - let init c_set { desc = desc } = - match desc with - | Einit_last(_, e) -> exp c_set e in - let c_set = List.fold_left index c_set i_list in - let c_set = List.fold_left init c_set init_list in - block_eq_list c_set b_eq_list - - and scondpat c_set { desc = desc } = - match desc with - | Econdand(sc1, sc2) | Econdor(sc1, sc2) -> - scondpat (scondpat c_set sc1) sc2 - | Econdexp(e) | Econdpat(e, _) -> exp c_set e - | Econdon(sc, e) -> scondpat (exp c_set e) sc - - and state c_set { desc = desc } = - match desc with - | Estate0 _ -> c_set - | Estate1(_, e_list) -> List.fold_left exp c_set e_list - - and block_eq_list c_set { b_locals = l_list; b_body = eq_list } = - let c_set = List.fold_left local c_set l_list in - List.fold_left equation c_set eq_list in - - (* First: compute the inputs/outputs of the main function *) - let tc_list = List.map (fun { p_caus = tc } -> tc) p_list in +(* of function applications inside the body of the function *) +let funexp_build_io_table { f_args; f_body = ({ r_info } as r) } = + (* traverses the body *) + let result c_set r = + let expression funs c_set ({ e_desc; e_info } as e) = + match e_desc with + | Eapp { f; arg_list } -> + let _, c_set = Util.mapfold (Mapfold.expression_it funs) c_set arg_list in + (* compute the set of causality tags *) + let tc_list = + List.map (fun { e_info } -> Typinfo.get_caus e_info) (arg_list) in + let tc = Typinfo.get_caus f.e_info in + let c_set = + List.fold_left Causal.vars (Causal.vars c_set tc) tc_list in + e, c_set + | _ -> Mapfold.expression_it funs c_set e in + let global_funs = Mapfold.default_global_funs in + let funs = { Mapfold.defaults with expression; global_funs } in + let _, c_set = Mapfold.result_it funs c_set r in + c_set in + (* Compute the inputs/outputs of the main function *) + let tc_list = + let arg acc a = + List.fold_left + (fun acc { var_info } -> Typinfo.get_caus var_info :: acc) acc a in + List.fold_left arg [] f_args in + + let tc = Typinfo.get_caus r_info in + (* mark inputs/outputs *) List.iter (Causal.mark_and_polarity false) tc_list; Causal.mark_and_polarity true tc; let c_set = Causal.vars (List.fold_left Causal.vars Causal.S.empty tc_list) tc in let inputs, outputs = Causal.ins_and_outs c_set in - (* computes the set of causality tags that appear in [e] *) - let c_set = exp c_set e in + (* computes the set of causality tags that appear in [f_body] *) + let c_set = result c_set r in (* compute the table of outputs for all the variables *) let o_table = Causal.build_o_table c_set Causal.M.empty in @@ -175,9 +97,9 @@ let funexp_info { f_args = p_list; f_body = ({ e_caus = tc } as e) } = io_table = io_table; o_table = o_table } -(* The function which decides whether or not a function call *) +(* [to_inline] The function which decides whether or not a function call *) (* [f(arg1,...,argn) must be inlined *) -let to_inline { io_table = io_table; o_table = o_table } tc_arg_list tc_res = +let to_inline { io_table; o_table } tc_arg_list tc_res = let _, out_of_inputs = List.fold_left (Causal.ins_and_outs_of_a_type true) (Causal.S.empty, Causal.S.empty) @@ -217,138 +139,42 @@ let to_inline { io_table = io_table; o_table = o_table } tc_arg_list tc_res = | Causal.Clash _ -> assert false (* Mark function calls to be inlined *) -let funexp_mark_to_inline info ({ f_body = e } as funexp) = - (* generic translation for match handlers *) - let match_handler body ({ m_body = b } as m_h) = - { m_h with m_body = body b } in - - (* generic translation function for present handlers *) - let present_handler scondpat body ({ p_cond = sc; p_body = b } as p_h) = - { p_h with p_cond = scondpat sc; p_body = body b } in - +let funexp_apply_io_table io_table ({ f_body } as f) = (* expressions *) - let rec exp ({ e_desc = desc; e_caus = tc } as e) = - let desc = match desc with - | Elocal _ | Eglobal _ | Econst _ - | Econstr0 _ | Elast _ | Eperiod _ -> desc - | Eop(op, e_list) -> Eop(op, List.map exp e_list) - | Eapp({ app_inline = i } as app, op, arg_list) -> - (* only fully applied functions can be inlined *) - let op = exp op in - let arg_list = List.map exp arg_list in - let i = - if i then true - else let tc_arg_list = - List.map (fun { e_caus = tc } -> tc) (op :: arg_list) in - to_inline info tc_arg_list tc in - Eapp({ app with app_inline = i }, op, arg_list) - | Etuple(e_list) -> Etuple(List.map exp e_list) - | Econstr1(c, e_list) -> Econstr1(c, List.map exp e_list) - | Erecord_access(e_record, m) -> Erecord_access(exp e_record, m) - | Erecord(m_e_list) -> - Erecord(List.map (fun (m, e) -> (m, exp e)) m_e_list) - | Erecord_with(e_record, m_e_list) -> - Erecord_with(exp e_record, - List.map (fun (m, e) -> (m, exp e)) m_e_list) - | Etypeconstraint(e, ty) -> Etypeconstraint(exp e, ty) - | Epresent(p_h_list, e_opt) -> - Epresent(List.map (present_handler scondpat exp) p_h_list, - Zmisc.optional_map exp e_opt) - | Ematch(total, e, m_h_list) -> - Ematch(total, exp e, List.map (match_handler exp) m_h_list) - | Elet(l, e) -> Elet(local l, exp e) - | Eblock(b, e) -> Eblock(block_eq_list b, exp e) - | Eseq(e1, e2) -> Eseq(exp e1, exp e2) in - { e with e_desc = desc } + let expression funs acc ({ e_desc; e_info } as e) = + match e_desc with + | Eapp { is_inline; f; arg_list } -> + (* only fully applied functions can be inlined *) + let op, _ = Mapfold.expression_it funs acc f in + let arg_list, _ = + Util.mapfold (Mapfold.expression_it funs) acc arg_list in + let is_inline = + if is_inline then true + else + let tc_res = Typinfo.get_caus e_info in + let tc_arg_list = + List.map + (fun { e_info } -> Typinfo.get_caus e_info) (op :: arg_list) in + to_inline io_table tc_arg_list tc_res in + { e with e_desc = Eapp({ is_inline; f; arg_list }) }, acc + | _ -> Mapfold.expression_it funs acc e in + let global_funs = Mapfold.default_global_funs in + let funs = { Mapfold.defaults with expression; global_funs } in + let f_body, _= Mapfold.result_it funs () f_body in + { f with f_body }, io_table - and local ({ l_eq = eq_list } as l) = - { l with l_eq = List.map equation eq_list } +let funexp funs _ f = + let io_table = funexp_build_io_table f in + let f, _ = funexp_apply_io_table io_table f in + f, () - and equation ({ eq_desc = desc } as eq) = - let desc = match desc with - | EQeq(p, e) -> EQeq(p, exp e) - | EQpluseq(n, e) -> EQpluseq(n, exp e) - | EQder(n, e, e_opt, p_h_list) -> - EQder(n, exp e, Zmisc.optional_map exp e_opt, - List.map (present_handler scondpat exp) p_h_list) - | EQinit(n, e) -> EQinit(n, exp e) - | EQnext(n, e, e_opt) -> - EQnext(n, exp e, Zmisc.optional_map exp e_opt) - | EQautomaton(is_weak, s_h_list, se_opt) -> - EQautomaton(is_weak, List.map state_handler s_h_list, - Zmisc.optional_map state se_opt) - | EQpresent(p_h_list, b_opt) -> - EQpresent(List.map (present_handler scondpat block_eq_list) p_h_list, - Zmisc.optional_map block_eq_list b_opt) - | EQmatch(total, e, m_h_list) -> - EQmatch(total, exp e, - List.map (match_handler block_eq_list) m_h_list) - | EQreset(res_eq_list, e) -> - EQreset(List.map equation res_eq_list, exp e) - | EQand(and_eq_list) -> - EQand(List.map equation and_eq_list) - | EQbefore(before_eq_list) -> - EQbefore(List.map equation before_eq_list) - | EQemit(n, e_opt) -> - EQemit(n, Zmisc.optional_map exp e_opt) - | EQblock(b) -> EQblock(block_eq_list b) - | EQforall({ for_index = i_list; for_init = init_list; - for_body = b_eq_list } as body) -> - let index ({ desc = desc } as ind) = - let desc = match desc with - | Einput(x, e) -> Einput(x, exp e) - | Eindex(x, e1, e2) -> - Eindex(x, exp e1, exp e2) - | Eoutput _ -> desc in - { ind with desc = desc } in - let init ({ desc = desc } as ini) = - let desc = match desc with - | Einit_last(x, e) -> Einit_last(x, exp e) in - { ini with desc = desc } in - let i_list = List.map index i_list in - let init_list = List.map init init_list in - let b_eq_list = block_eq_list b_eq_list in - EQforall { body with for_index = i_list; for_init = init_list; - for_body = b_eq_list } in - { eq with eq_desc = desc } +let program p = + let global_funs = Mapfold.default_global_funs in + let funs = + { Mapfold.defaults with funexp; global_funs } in + let { p_impl_list } as p, _ = + Mapfold.program_it funs () p in + { p with p_impl_list = p_impl_list } - and scondpat ({ desc = desc } as sc) = - let desc = match desc with - | Econdand(sc1, sc2) -> Econdand(scondpat sc1, scondpat sc2) - | Econdor(sc1, sc2) -> Econdor(scondpat sc1, scondpat sc2) - | Econdexp(e) -> Econdexp(exp e) - | Econdpat(e, p) -> Econdpat(exp e, p) - | Econdon(sc, e) -> Econdon(scondpat sc, exp e) in - { sc with desc = desc } - - and state_handler ({ s_body = b; s_trans = trans } as sh) = - { sh with s_body = block_eq_list b; s_trans = List.map escape trans } - - and state ({ desc = desc } as se) = - let desc = match desc with - | Estate0 _ -> desc - | Estate1(id, e_list) -> - Estate1(id, List.map exp e_list) in - { se with desc = desc } - - and block_eq_list ({ b_locals = l_list; b_body = eq_list } as b) = - { b with b_locals = List.map local l_list; - b_body = List.map equation eq_list } - - and escape ({ e_cond = sc; e_block = b_opt; e_next_state = se } as esc) = - { esc with e_cond = scondpat sc; - e_block = Zmisc.optional_map block_eq_list b_opt; - e_next_state = state se } in - { funexp with f_body = exp e } -let implementation impl = - match impl.desc with - | Eopen _ | Etypedecl _ | Econstdecl _ -> impl - | Efundecl(n, funexp) -> - let info = funexp_info funexp in - let funexp = funexp_mark_to_inline info funexp in - { impl with desc = Efundecl(n, funexp) } - -let implementation_list impl_list = - Zmisc.iter implementation impl_list diff --git a/src/compiler/main/rewrite.ml b/src/compiler/rewrite/rewrite.ml similarity index 55% rename from src/compiler/main/rewrite.ml rename to src/compiler/rewrite/rewrite.ml index 510537cd..15841b12 100644 --- a/src/compiler/main/rewrite.ml +++ b/src/compiler/rewrite/rewrite.ml @@ -12,66 +12,37 @@ (* *) (* *********************************************************************) -(* the main functions *) +(* the sequence of source-to-source transformations applied to the input program *) open Misc open Location -exception Stop - -let lexical_error err loc = - Format.eprintf "%aIllegal character.@." output_location loc; - raise Error - -let syntax_error loc = - Format.eprintf "%aSyntax error.@." output_location loc; - raise Error - -let parse parsing_fun lexing_fun source_name = - let ic = open_in source_name in - let lexbuf = Lexing.from_channel ic in - lexbuf.Lexing.lex_curr_p <- - { lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = source_name }; - try - parsing_fun lexing_fun lexbuf - with - | Lexer.Lexical_error(err, loc) -> - close_in ic; lexical_error err loc - | Parser.Error -> - close_in ic; - syntax_error - (Loc(Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) - -let parse_implementation_file source_name = - parse Parser.implementation_file Lexer.main source_name - -let apply_with_close_out f o = - try - f o; - close_out o - with x -> close_out o; raise x - -let print_message comment = - if !verbose then - Format.fprintf Format.err_formatter - "@[------------------------------------------------------------------\n\ - %s\n\ - --------------------------------------------------------------------@]@." - comment +let hybrid_list = + ["der", "Remove handlers in definitions of derivatives. See below:", + Der.program; + "period", "Translation of periods done. See below:", + Period.program; + "disc", "Translation of disc done. See below:", + Disc.program] -let do_step comment output step input = - print_message comment; - let o = step input in - output o; - o +(* +let optim_list = + ["horizon", + "Gather all horizons into a single one per function. See below:", + Horizon.program; + "aform", "A-normal form. See below:", + Aform.program; + "deadcode", "Dead-code removal. See below:", + Deadcode.program; + "copy", "Remove of copy variables. See below:", + Copy.program] +*) let default_list = ["static", "Static reduction done. See below:", Static.program; "inline", "Inlining done. See below:", - Inline.program; - "der", "Remove handlers in definitions of derivatives. See below:", - Der.program; - "auto", "Translation of automata. See below:", + Inline.program] @ hybrid_list @ [ + "automata", "Translation of automata. See below:", Automata.program; "present", "Translation of present. See below:", Present.program; @@ -119,7 +90,7 @@ let set_steps w = List.iter (fun l -> set true (List.hd l); List.iter (fun s -> set false s) (List.tl l)) l_l -let rewrite_list () = +let rewrite_list = List.filter (fun (w, _, _) -> S.mem w !s_set) default_list let compare name n_steps genv0 p p' = @@ -131,43 +102,14 @@ let compare name n_steps genv0 p p' = Coiteration.check n_steps genv genv'; p' (* Apply a sequence of source-to-source transformation *) -(* do equivalence checking for every step if the flag is turned on *) -let main modname filename n_steps = - let transform_and_compare genv p (name, comment, transform) = - let p' = transform genv p in +(* do equivalence checking for every step if [n_steps <> 0] *) +let main print_message genv0 p n_steps = + let rewrite_and_compare genv p (name, comment, rewrite) = + let p' = rewrite genv p in print_message comment; Debug.print_program p'; if n_steps = 0 then p' else compare name n_steps genv p p' in - let iter genv p l = List.fold_left (transform_and_compare genv) p l in - - let _ = Format.std_formatter in - - (* output file in which values are stored *) - let obj_name = filename ^ ".zlo" in - let otc = open_out_bin obj_name in - let source_name = filename ^ ".zls" in - (* set the current opened module *) - Location.initialize source_name; - - (* Parsing *) - let p = parse_implementation_file source_name in - Debug.print_message "Parsing done"; - - (* defines the initial global environment for values *) - let genv0 = Genv.initialize modname [] in - (* Add Stdlib *) - let genv0 = Genv.add_module genv0 (Primitives.stdlib_env ()) in + let iter genv p l = List.fold_left (rewrite_and_compare genv) p l in - (* Associate unique index to variables *) - let module Scoping = Scoping.Make(Typinfo) in - let p = do_step "Scoping done. See below:" Debug.print_program - Scoping.program p in - (* Write defined variables for equations *) - let module Write = Write.Make(Typinfo) in - let p = do_step "Write done. See below: " - Debug.print_program Write.program p in - (* Source-to-source transformations start here *) - let _ = iter genv0 p (rewrite_list ()) in - - apply_with_close_out (fun _ -> ()) otc + iter genv0 p rewrite_list diff --git a/src/compiler/typing/typing.ml b/src/compiler/typing/typing.ml index 53e75a09..9d2be6a7 100644 --- a/src/compiler/typing/typing.ml +++ b/src/compiler/typing/typing.ml @@ -1236,7 +1236,7 @@ let implementation ff is_first { desc; loc } = | Eopen(modname) -> if is_first then Modules.open_module modname | Eletdecl { d_leq } -> - let new_h, actual_k = leq (Tfun(Tconst)) Env.empty d_leq in + let new_h, actual_k = leq (Tfun(Tany)) Env.empty d_leq in (* check that there is no unbounded size variables *) check_no_unbounded_size_name loc new_h; (* update the global environment *) diff --git a/src/ctests/good/1.zci b/src/ctests/good/1.zci new file mode 100644 index 0000000000000000000000000000000000000000..aab538ccd0df52bc8faaa06d2302ece6002da8dd GIT binary patch literal 547 zcmYk3Jxc>Y5QYaCY!p<`G?L;HFqML0X)${jKXVFVWvPfUAR_TJe#DPLE1OH9mBnD8 zm2iT!P5!|Bqjh#~H(1Qx&b#kCGs8W;eEb3ojRC-qd}E159?a(y9Og_}KMg7S=9!)3 z;JCG4ZJi{P(iLdYaM-1npszs_5x+8)aFV3B`L7tKobgWT91zP+>lUnvOK(8mg1#T% z7I50&jx4T6gMo0-6+mpD=0zr2^5RB8RX$$_4GoD+KS4h&Dq`sA)M z>mMQ!Q#Rf9yhNa_(DZ_m`5_cSU1CjQYp_rU>qIJyWT}KncB>>cCO(y0HL2A&WoCQ| zqRbK>9P!+B=vj|x{_I{Zgq%`GPNTkInKNoz?F@8iVDCYg5sr|#e+H@me+A}8CSt^r XB5oHmY5QYaCY!p<`G?L;HFqIa;(qi^5ekKZHWvPfUAR_TJerutX&85)FVzAIk zIKkQ`f8hSnI{PISv$yl^JI~DSJv_hv01S-*z_)x`63rs27ZmLmO!**-DgWY`t#t3O zvs>*PrIgVHXwh)kr{|zAK@$P8$>EjI8=`IA366LLm9S&jONWzMNfxSg>PB=nl{}Cw%{*26zOvQ*L XMcj2W6$Rm_SQSp-IK?=Jvy{*;8W7We literal 0 HcmV?d00001 diff --git a/src/ctests/good/3.zci b/src/ctests/good/3.zci index 4125ee479784160729df8c939f5064c842a76f5f..8165b3c2c35e22c11ffa6590c5fb3d4c22d9424c 100644 GIT binary patch delta 195 zcmdnOxPeKeW$Lnh3=E7i3=9lmKw2M&btj70C^$^muz-VsL7l;Y;XgxwgM))3kbw{h zoLFFAf5Aa1&FI1chYeFU9G>U^rY1N6DHg3VMkAVj<- L7TB`_#T*;}hY}J4 diff --git a/src/ctests/good/3.zls b/src/ctests/good/3.zls index 3f97dfa8..bfd7b858 100644 --- a/src/ctests/good/3.zls +++ b/src/ctests/good/3.zls @@ -1,11 +1,10 @@ let node f1 () returns (o) if true then o = 1 else o = 2 -(* let node f2 () returns (o) automaton | A -> do o = 1 until true then B | B -> do o = 2 until false then A init if true then B else A - end *) + end \ No newline at end of file diff --git a/src/dune b/src/dune index 8535af5b..dc70f906 100644 --- a/src/dune +++ b/src/dune @@ -116,15 +116,26 @@ (libraries zelus.global_lib zelus.typdefs_lib) ) -; causality and initialisation analyses +; causality analysis (library - (name analyses_lib) - (public_name zelus.analyses_lib) + (name causality_lib) + (public_name zelus.causality_lib) (wrapped false) (modules causal ; type manipulation and unification between types for causality - init ; type manipulation and unification between types for initialisation causality ; causality inference + ) + (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib + zelus.typing_lib) +) + +; initialisation analysis + (library + (name initialization_lib) + (public_name zelus.initialization_lib) + (wrapped false) + (modules + init ; type manipulation and unification between types for initialisation initialization ; initialization inference ) (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib @@ -141,6 +152,7 @@ cost ; a cost function used to decide which function call to inline mapfold ; generic mapfold aux ; auxiliary functions for building terms + markfunctions ; mark function calls to be inlined static ; static reduction inline ; inlining of function calls der ; remove the initialization and handler part of a derivative equation @@ -164,7 +176,8 @@ schedule ; static scheduling rewrite ; compose rewriting steps ) - (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib zelus.zrun_lib) + (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib + zelus.causality_lib zelus.zrun_lib) ) ;sequential code generation @@ -181,16 +194,6 @@ (libraries zelus.global_lib zelus.typdefs_lib) ) -; Source-to-source transformations -(executable - (name zwrite) - (modes (byte exe)) - (modules - zwrite; the main function - ) - (libraries zelus.parser_lib zelus.global_lib zelus.zrun_lib zelus.rewrite_lib) - (promote (until-clean) (into ..))) - ; The compiler (executable (name zeluc) @@ -201,7 +204,7 @@ zeluc; the main function ) (libraries zelus.parser_lib zelus.global_lib zelus.zrun_lib - zelus.typing_lib zelus.analyses_lib zelus.rewrite_lib) + zelus.typing_lib zelus.causality_lib zelus.initialization_lib zelus.rewrite_lib) (promote (until-clean) (into ..))) (install diff --git a/src/global/misc.ml b/src/global/misc.ml index 21599945..7c6a289c 100644 --- a/src/global/misc.ml +++ b/src/global/misc.ml @@ -141,8 +141,8 @@ let lustre = ref false let static_reduction = ref false (* check equivalence *) -let equivalence_checking = ref 0 -let set_equivalence_checking n = equivalence_checking := n +let n_steps = ref 0 +let set_check_equivalence_for_n_steps n = n_steps := n (* sets the inline flags *) let inlining_level = ref 10 diff --git a/src/typdefs/typinfo.ml b/src/typdefs/typinfo.ml index 813fdd93..6c4cfba0 100644 --- a/src/typdefs/typinfo.ml +++ b/src/typdefs/typinfo.ml @@ -39,3 +39,4 @@ let set_caus typinfo tc = { typinfo with t_caus = tc } let set_init typinfo ti = { typinfo with t_init = ti } let get_type { t_typ } = t_typ +let get_caus { t_caus } = t_caus