heptagon/compiler/minils/minils.ml

172 lines
4.9 KiB
OCaml
Raw Normal View History

2010-06-15 10:49:03 +02:00
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* The internal MiniLustre representation *)
open Location
open Names
open Ident
2010-06-15 15:08:14 +02:00
open Signature
2010-06-15 10:49:03 +02:00
open Static
2010-06-16 19:30:37 +02:00
open Types
2010-06-15 10:49:03 +02:00
(** Warning: Whenever Minils ast is modified,
minils_format_version should be incremented. *)
let minils_format_version = "1"
type iterator_type =
| Imap
| Ifold
| Imapfold
2010-06-15 10:49:03 +02:00
type type_dec = {
t_name: name;
t_desc: tdesc;
t_loc: location }
2010-06-15 10:49:03 +02:00
and tdesc =
| Type_abs
| Type_enum of name list
2010-06-15 15:08:14 +02:00
| Type_struct of structure
2010-06-15 10:49:03 +02:00
and exp = {
e_desc: edesc;
mutable e_ck: ck;
mutable e_ty: ty;
e_loc: location }
2010-06-15 10:49:03 +02:00
2010-06-16 19:30:37 +02:00
and edesc =
2010-06-30 17:20:56 +02:00
| Econst of static_exp
| Evar of var_ident
2010-06-30 17:20:56 +02:00
| Efby of static_exp option * exp
2010-07-01 19:35:24 +02:00
(** static_exp fby exp *)
| Eapp of app * exp list * var_ident option
2010-07-01 19:35:24 +02:00
(** app ~args=(exp,exp...) reset ~r=ident *)
| Ewhen of exp * constructor_name * var_ident
2010-07-01 19:35:24 +02:00
(** exp when Constructor(ident) *)
| Emerge of var_ident * (constructor_name * exp) list
2010-07-01 19:35:24 +02:00
(** merge ident (Constructor -> exp)+ *)
| Estruct of (field_name * exp) list
2010-07-01 19:35:24 +02:00
(** { field=exp; ... } *)
| Eiterator of iterator_type * app * static_exp * exp list * var_ident option
2010-07-01 19:35:24 +02:00
(** map f <<n>> (exp,exp...) reset ident *)
2010-06-30 17:20:56 +02:00
2010-07-01 19:35:24 +02:00
and app = { a_op: op; a_params: static_exp list; a_unsafe: bool }
(** Unsafe applications could have side effects
and be delicate about optimizations, !be careful! *)
2010-06-30 17:20:56 +02:00
and op =
2010-07-01 19:35:24 +02:00
| Etuple (** (args) *)
| Efun of fun_name (** "Stateless" longname <<a_params>> (args) reset r *)
| Enode of fun_name (** "Stateful" longname <<a_params>> (args) reset r *)
2010-07-01 19:35:24 +02:00
| Eifthenelse (** if arg1 then arg2 else arg3 *)
| Efield (** arg1.a_param1 *)
| Efield_update (** { arg1 with a_param1 = arg2 } *)
2010-07-01 19:35:24 +02:00
| Earray (** [ args ] *)
| Earray_fill (** [arg1^a_param1] *)
2010-07-01 19:35:24 +02:00
| Eselect (** arg1[a_params] *)
| Eselect_slice (** arg1[a_param1..a_param2] *)
| Eselect_dyn (** arg1.[arg3...] default arg2 *)
| Eupdate (** [ arg1 with a_params = arg2 ] *)
| Econcat (** arg1@@arg2 *)
2010-06-30 17:20:56 +02:00
2010-06-15 10:49:03 +02:00
and ct =
| Ck of ck
| Cprod of ct list
and ck =
| Cbase
| Cvar of link ref
| Con of ck * constructor_name * var_ident
2010-06-15 10:49:03 +02:00
and link =
| Cindex of int
| Clink of ck
and pat =
| Etuplepat of pat list
| Evarpat of var_ident
type eq = {
eq_lhs : pat;
eq_rhs : exp;
eq_loc : location }
type var_dec = {
v_ident : var_ident;
v_type : ty;
2010-07-15 10:02:42 +02:00
v_clock : ck;
v_loc : location }
type contract = {
c_assume : exp;
c_enforce : exp;
c_local : var_dec list;
c_eq : eq list }
type node_dec = {
n_name : name;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
n_local : var_dec list;
n_equs : eq list;
n_loc : location;
n_params : param list; (** TODO CP mettre des petits commentaires *)
2010-07-08 14:56:49 +02:00
n_params_constraints : size_constraint list;
n_params_instances : (static_exp list) list }
type const_dec = {
c_name : name;
c_type : ty;
c_value : static_exp;
c_loc : location }
type program = {
p_modname : name;
p_format_version : string;
p_opened : name list;
p_types : type_dec list;
p_nodes : node_dec list;
p_consts : const_dec list }
2010-06-15 10:49:03 +02:00
(*Helper functions to build the AST*)
2010-07-20 09:34:11 +02:00
let mk_exp ?(exp_ty = invalid_type) ?(clock = Cbase) ?(loc = no_location) desc =
2010-06-16 19:30:37 +02:00
{ e_desc = desc; e_ty = exp_ty; e_ck = clock; e_loc = loc }
2010-07-15 10:02:42 +02:00
let mk_var_dec ?(loc = no_location) ?(clock = Cbase) ident ty =
{ v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc }
2010-06-18 11:46:57 +02:00
2010-06-18 14:59:10 +02:00
let mk_equation ?(loc = no_location) pat exp =
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
let mk_node
2010-06-29 11:18:50 +02:00
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name =
{ n_name = name;
n_input = input;
n_output = output;
n_contract = contract;
n_local = local;
n_equs = eq;
n_loc = loc;
n_params = param;
n_params_constraints = constraints;
n_params_instances = pinst; }
let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name =
2010-07-08 14:56:49 +02:00
{ t_name = name; t_desc = type_desc; t_loc = loc }
2010-07-08 14:56:49 +02:00
let mk_app ?(params=[]) ?(unsafe=false) op =
{ a_op = op; a_params = params; a_unsafe = unsafe }
2010-06-29 11:18:50 +02:00
2010-07-08 14:56:49 +02:00
let void = mk_exp (Eapp (mk_app Etuple, [], None))
2010-06-15 10:49:03 +02:00