CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

type rat = Utils.rat

type tag = Utils.tag

type type_dec =

    {ty_dec_desc: type_dec_desc;

     ty_dec_loc: Location.t}

and type_dec_desc =

  | Tydec_any

  | Tydec_int

  | Tydec_real

  | Tydec_clock of type_dec_desc

  | Tydec_const of ident

  | Tydec_enum of ident list

    {tydec_id: ident}

type typedef_desc =

    {tydef_id: ident;

     tydef_desc: type_dec_desc}

    {ck_dec_desc: clock_dec_desc;

     ck_dec_loc: Location.t}

and clock_dec_desc =

  | Ckdec_any

  | Const_int of int

  | Const_tag of label

  | Const_string of string (* used only for annotations *)

type quantifier_type = Exists | Forall

     var_dec_clock: clock_dec;

     var_dec_const: bool;

     mutable var_clock: Clocks.clock_expr;

     var_loc: Location.t}

    location in the program text. The type and clock of an ast element

    is mutable (and initialized to dummy values). This avoids to have to

    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)

   different instances of the same node *)

     expr_desc: expr_desc;

     mutable expr_type: Types.type_expr;

     mutable expr_clock: Clocks.clock_expr;

     mutable expr_delay: Delay.delay_expr;

     mutable expr_annot: expr_annot option;

     expr_loc: Location.t}

and expr_desc =

  | Expr_const of constant

  | Expr_ident of ident

  | Expr_tuple of expr list

  | Expr_ite   of expr * expr * expr

  | Expr_arrow of expr * expr

  | Expr_fby of expr * expr

  | Expr_array of expr list

  | Expr_access of expr * Dimension.dim_expr

  | Expr_power of expr * Dimension.dim_expr

  | Expr_pre of expr

  | Expr_when of expr * ident * label

  | Expr_merge of ident * (label * expr) list

  | Expr_appl of call_t

and eq =

    {eq_lhs: ident list;

     eq_rhs: expr;

     eq_loc: Location.t}

     different instances of the same node *)

     eexpr_quantifiers: (quantifier_type * var_decl list) list;

     mutable eexpr_clock: Clocks.clock_expr;

 {annots: (string list * eexpr) list;

  annot_loc: Location.t}

    mode_id: ident;

    require: eexpr list;

    ensure: eexpr list;

    mode_loc: Location.t

  }

type contract_import =

    inputs: expr;

    outputs: expr;

    import_loc: Location.t }

| Index of Dimension.dim_expr

| Field of label

      assert_expr: expr;

type statement =

| Eq of eq

| Aut of automata_desc

   aut_handlers: handler_desc list;

   aut_loc: Location.t}

and handler_desc =

  {hand_state: ident;

   hand_until: (Location.t * expr * bool * ident) list;

   hand_annots: expr_annot list;

  {

    consts: var_decl list;

    locals: var_decl list;

    stmts: statement list;

    assume: eexpr list;

    guarantees: eexpr list;

    modes: contract_mode list;

    imports: contract_import list; 

    spec_loc: Location.t;

  }

                 | NodeSpec of ident

    {node_id: ident;

     mutable node_type: Types.type_expr;

     mutable node_clock: Clocks.clock_expr;

     node_inputs: var_decl list;

     node_outputs: var_decl list;

     node_locals: var_decl list;

     mutable node_gencalls: expr list;

     mutable node_checks: Dimension.dim_expr list;

     mutable node_stateless: bool option;

type imported_node_desc =

    {nodei_id: ident;

     mutable nodei_type: Types.type_expr;

     mutable nodei_clock: Clocks.clock_expr;

     nodei_inputs: var_decl list;

     nodei_outputs: var_decl list;

     nodei_stateless: bool;

    {const_id: ident;

     const_loc: Location.t;

     const_value: constant;

    }

  | Const of const_desc

  | ImportedNode of imported_node_desc

  | Open of bool * string (* the boolean set to true denotes a local

     top_decl_owner: Location.filename; (* the module where it is defined *)

     top_decl_itf: bool;                (* header or source file ? *)

     top_decl_loc: Location.t}          (* the location where it is defined *)

    local: bool;

    name: ident;

    content: program_t;

    is_stateful: bool

  }

  | LocalContract of contract_desc

  | TopContract of top_decl list

let tag_false = "false"

(* compile-command:"make -C .." *)

(* End: *)