-
Notifications
You must be signed in to change notification settings - Fork 13
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
A pass to simplify the language of expressions. It rewrites : - Ematch into EQmatch; - Ereset into EQreset.
- Loading branch information
1 parent
08ebec4
commit 1b9cf91
Showing
1 changed file
with
64 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
(***********************************************************************) | ||
(* *) | ||
(* *) | ||
(* Zelus, a synchronous language for hybrid systems *) | ||
(* *) | ||
(* (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 *) | ||
(* the terms of the INRIA Non-Commercial License Agreement (see the *) | ||
(* LICENSE file). *) | ||
(* *) | ||
(* *********************************************************************) | ||
|
||
(* translate some expressions into equations *) | ||
(* the constructs that are concerned are: | ||
*- [match e with P1 -> e1 | ... | Pn -> en] => | ||
[let match e with P1 -> r = e1 | ... | Pn -> r = en in r] | ||
*- [reset e every c] => let reset r = e every c in r] | ||
*) | ||
|
||
open Misc | ||
open Location | ||
open Ident | ||
open Zelus | ||
open Mapfold | ||
|
||
let empty = () | ||
|
||
let fresh () = Ident.fresh "r" | ||
|
||
let expression funs acc e = | ||
let ({ e_desc; e_loc } as e), acc = Mapfold.expression funs acc e in | ||
match e_desc with | ||
| Ematch { is_total; e; handlers } -> | ||
let result = fresh () in | ||
let handler { m_pat; m_body; m_env; m_loc; m_reset; m_zero } = | ||
{ m_pat; m_body = Aux.id_eq result m_body; m_env; m_loc; m_reset; m_zero } in | ||
let eq = | ||
{ eq_desc = EQmatch { is_total; e; handlers = List.map handler handlers }; | ||
eq_write = Defnames.singleton result; | ||
eq_safe = true; eq_index = -1; eq_loc = e_loc } in | ||
Aux.e_let (Aux.leq [eq]) (Aux.var result), acc | ||
| Ereset(e, e_r) -> | ||
let result = fresh () in | ||
let eq = | ||
{ eq_desc = EQreset(Aux.id_eq result e, e_r); | ||
eq_write = Defnames.singleton result; | ||
eq_safe = true; eq_index = -1; eq_loc = e_loc } in | ||
Aux.e_let (Aux.leq [eq]) (Aux.var result), acc | ||
| _ -> e, acc | ||
|
||
let set_index funs acc n = | ||
let _ = Ident.set n in n, acc | ||
let get_index funs acc n = Ident.get (), acc | ||
|
||
let program _ p = | ||
let global_funs = Mapfold.default_global_funs in | ||
let funs = | ||
{ Mapfold.defaults with expression; set_index; get_index; global_funs } in | ||
let { p_impl_list } as p, _ = | ||
Mapfold.program_it funs empty p in | ||
{ p with p_impl_list = p_impl_list } | ||
|