CristalCaveGem » LustreC

    List.fold_left check_var_decl checks (get_node_vars nd) in

    | Const_string _ -> assert false (* string occurs in annotations not in C *)

open LustreSpec

  val other_targets: Format.formatter -> string -> string -> (string * bool * top_decl list) list -> unit

open Utils

(* OLD STUFF ???

  *)

      | Expr_when (e,_,_) -> get_expr_calls prednode e

    mk_new_name (get_node_vars n) id

    let var_decl = get_node_var var n in

let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}

let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}

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

(*   Eexpr functions *)

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

let merge_node_annot ann1 ann2 =

  { requires = ann1.requires @ ann2.requires;

    ensures = ann1.ensures @ ann2.ensures;

    behaviors = ann1.behaviors @ ann2.behaviors;

    spec_loc = ann1.spec_loc

  }

let mkeexpr loc expr =

  { eexpr_tag = Utils.new_tag ();

    eexpr_qfexpr = expr;

    eexpr_quantifiers = [];

    eexpr_type = Types.new_var ();

    eexpr_clock = Clocks.new_var true;

    eexpr_normalized = None;

    eexpr_loc = loc }

let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }

(*

let mkepredef_call loc funname args =

  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))

let mkepredef_unary_call loc funname arg =

  mkeexpr loc (EExpr_appl (funname, arg, None))

*)

let merge_expr_annot ann1 ann2 =

  match ann1, ann2 with

    | None, None -> assert false

    | Some _, None -> ann1

    | None, Some _ -> ann2

    | Some ann1, Some ann2 -> Some {

      annots = ann1.annots @ ann2.annots;

      annot_loc = ann1.annot_loc

    }

let update_expr_annot e annot =

  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }

let get_node_vars nd =

let get_var id var_list =

 List.find (fun v -> v.var_id = id) var_list

let get_node_var id node = get_var id (get_node_vars node)

let get_node_eq id node =

       )

    List.map 

let rec get_expr_calls nodes e =

  get_calls_expr_desc nodes e.expr_desc

and get_calls_expr_desc nodes expr_desc =

  let get_calls = get_expr_calls nodes in

  match expr_desc with

  | Expr_const _ 

   | Expr_ident _ -> Utils.ISet.empty

   | Expr_tuple el

   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el

   | Expr_pre e1 

   | Expr_when (e1, _, _) 

   | Expr_access (e1, _) 

   | Expr_power (e1, _) -> get_calls e1

   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 

   | Expr_arrow (e1, e2) 

   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)

   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl

   | Expr_appl (i, e', i') -> 

     if Basic_library.is_internal_fun i then 

       (get_calls e') 

     else

       let calls =  Utils.ISet.add i (get_calls e') in

       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in

       if List.exists test nodes then

	 match (List.find test nodes).top_decl_desc with

	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls

	 | _ -> assert false

       else 

	 calls

and get_eq_calls nodes eq =

  get_expr_calls nodes eq.eq_rhs

and get_node_calls nodes node =

  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs

let rec expr_has_arrows e =

  expr_desc_has_arrows e.expr_desc

and expr_desc_has_arrows expr_desc =

  match expr_desc with

  | Expr_const _ 

  | Expr_ident _ -> false

  | Expr_tuple el

  | Expr_array el -> List.exists expr_has_arrows el

  | Expr_pre e1 

  | Expr_when (e1, _, _) 

  | Expr_access (e1, _) 

  | Expr_power (e1, _) -> expr_has_arrows e1

  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]

  | Expr_arrow (e1, e2) 

  | Expr_fby (e1, e2) -> true

  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl

  | Expr_appl (i, e', i') -> expr_has_arrows e'

and eq_has_arrows eq =

  expr_has_arrows eq.eq_rhs

and node_has_arrows node =

  List.exists (fun eq -> eq_has_arrows eq) node.node_eqs

(*

*)

val dummy_type_dec: type_dec

val dummy_clock_dec: clock_dec

val get_node_vars: node_desc -> var_decl list

val get_node_var: ident -> node_desc -> var_decl

val get_node_eq: ident -> node_desc -> eq

(** Annotation expression related functions *)

val mkeexpr: Location.t ->  expr -> eexpr

val merge_node_annot: node_annot -> node_annot -> node_annot 

val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr

val update_expr_annot: expr -> expr_annot -> expr

(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)

(*

*)      

       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];

       behaviors = [];

       spec_loc = loc

    node_annot = [];

  (* open ParserLustreSpec *)

  open Parser_lustre

  (* "true", TRUE; *)

  (* "false", FALSE; *)

  (* "include", INCLUDE; *)

     Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lb

    Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lb

  let typ = (get_node_var var node).var_type in

  let eq_var = get_node_eq var node in

type label = Utils.ident

(** The core language and its ast. Every element of the ast contains its

    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). *)

type constant =

  | Const_int of int

  | Const_real of string

  | Const_float of float

  | Const_array of constant list

  | Const_tag of label

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

  | Const_struct of (label * constant) list

type quantifier_type = Exists | Forall

type expr =

    {expr_tag: tag;

     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 call_t = ident * expr * (ident * label) option 

     (* The third part denotes the reseting clock label and value *)

and 

  (* The tag of an expression is a unique identifier used to distinguish

     different instances of the same node *)

  eexpr =

     eexpr_qfexpr: expr;

     eexpr_quantifiers: (quantifier_type * var_decl list) list;

     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;

and expr_annot = {

  annots: (string list * eexpr) list;

  annot_loc: Location.t

}

and 

 eq =

    {eq_lhs: ident list;

     eq_rhs: expr;

     eq_loc: Location.t}

  ensures: eexpr list;

  behaviors: (string * eexpr list * eexpr list * Location.t) list;

  spec_loc: Location.t;

type assert_t = 

    {

      assert_expr: expr;

      assert_loc: Location.t

    } 

type node_desc =

    {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;

     node_asserts: assert_t list; 

     node_eqs: eq list;

     mutable node_dec_stateless: bool;

     mutable node_stateless: bool option;

     node_spec: node_annot option;

     node_annot: expr_annot list;

    }

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;

     nodei_spec: node_annot option;

     nodei_prototype: string option;

     nodei_in_lib: string option;

    }

type const_desc = 

    {const_id: ident; 

     const_loc: Location.t; 

     const_value: constant;      

     mutable const_type: Types.type_expr;

    }

type top_decl_desc =

| Node of node_desc

| Consts of const_desc list

| ImportedNode of imported_node_desc

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

			   lusi vs a lusi installed at system level *)

type top_decl =

    {top_decl_desc: top_decl_desc;

     top_decl_loc: Location.t}

type program = top_decl list

type error =

    Main_not_found

  | Main_wrong_kind

  | No_main_specified

  | Unbound_symbol of ident

  | Already_bound_symbol of ident

  mannot: expr_annot list;

    node_annot = [];  }

    mannot = [];

    let var_id = get_node_var id node in

    let var_x = get_node_var x node in

  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->

    let var_x = get_node_var x node in

  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->

    let var_x = get_node_var x node in

    let var_p = List.map (fun v -> get_node_var v node) p in

    let var_x = get_node_var x node in

    let var_x = get_node_var x node in

open LustreSpec

      (fun d accu -> match d.top_decl_desc with 

      | Open (local, s) -> (s, local)::accu 

  let vars = get_node_vars node in

open LustreSpec

  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')  

  let mkexpr x = mkexpr (Location.symbol_rloc ()) x

  let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x

  let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x

  (*

  *)

| REQUIRES qexpr SCOL requires { $2::$4 }

| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }

| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }

| ASSUMES qexpr SCOL assumes { $2::$4 } 

tuple_qexpr:

| qexpr COMMA qexpr {[$3;$1]}

| tuple_qexpr COMMA qexpr {$3::$1}

    expr COMMA expr {[$3;$1]}

// Same as tuple expr but accepting lists with single element

array_expr:

  expr {[$1]}

| expr COMMA array_expr {$1::$3}

dim_list:

  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }

| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }

/* constants */

  INT {mkexpr (Expr_const (Const_int $1))}

| REAL {mkexpr (Expr_const (Const_real $1))}

| FLOAT {mkexpr (Expr_const (Const_float $1))}

/* Idents or type enum tags */

| IDENT {

  if Hashtbl.mem tag_table $1

  then mkexpr (Expr_const (Const_tag $1))

  else mkexpr (Expr_ident $1)}

| LPAR ANNOT expr RPAR

    {update_expr_annot $3 $2}

    {mkexpr (Expr_tuple (List.rev $2))}

/* Array expressions */

| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

| expr POWER dim { mkexpr (Expr_power ($1, $3)) }

| expr LBRACKET dim_list { $3 $1 }

/* Temporal operators */

| PRE expr 

    {mkexpr (Expr_pre $2)}

    {mkexpr (Expr_arrow ($1,$3))}

    {(*mkexpr (Expr_fby ($1,$3))*)

      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}

    {mkexpr (Expr_when ($1,$3,tag_true))}

| expr WHENNOT IDENT

    {mkexpr (Expr_when ($1,$3,tag_false))}

| expr WHEN IDENT LPAR IDENT RPAR

    {mkexpr (Expr_when ($1, $5, $3))}

| MERGE IDENT handler_expr_list

    {mkexpr (Expr_merge ($2,$3))}

/* Applications */

    {mkexpr (Expr_appl ($1, $3, None))}

    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}

| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR

    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }

    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}

    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }

| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR

    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }

    {mkpredef_call "&&" [$1;$3]}

    {mkpredef_call "&&" [$1;$3]}

    {mkpredef_call "||" [$1;$3]}

    {mkpredef_call "||" [$1;$3]}

    {mkpredef_call "xor" [$1;$3]}

    {mkpredef_unary_call "not" $2}

    {mkpredef_call "impl" [$1;$3]}

    {mkpredef_call "=" [$1;$3]}

    {mkpredef_call "<" [$1;$3]}

    {mkpredef_call "<=" [$1;$3]}

    {mkpredef_call ">" [$1;$3]}

    {mkpredef_call ">=" [$1;$3]}

    {mkpredef_call "!=" [$1;$3]}

    {mkpredef_call "+" [$1;$3]}

    {mkpredef_call "-" [$1;$3]}

    {mkpredef_call "*" [$1;$3]}

    {mkpredef_call "/" [$1;$3]}

  {mkpredef_unary_call "uminus" $2}

    {mkpredef_call "mod" [$1;$3]}

    {mkexpr (Expr_ite ($2, $4, $6))}

handler_expr_list:

   { [] }

| handler_expr handler_expr_list { $1 :: $2 }

handler_expr:

 LPAR IDENT ARROW expr RPAR { ($2, $4) }

qexpr:

| expr { mkeexpr [] $1 }

  /* Quantifiers */

| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } 

| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 }

| INT {Const_int $1}

| REAL {Const_real $1}

| FLOAT {Const_float $1}

| TRUE {Const_bool true}

| FALSE {Const_bool false}

| STRING {Const_string $1}

let get_loc () = Location.symbol_rloc ()

let mktyp x = mktyp (get_loc ()) x

let mkclock x = mkclock (get_loc ()) x

let mkvar_decl x = mkvar_decl (get_loc ()) x

let mkexpr x = mkexpr (get_loc ()) x

let mkeexpr x = mkeexpr (get_loc ()) x 

let mkeq x = mkeq (get_loc ()) x

let mkassert x = mkassert (get_loc ()) x

let mktop_decl x = mktop_decl (get_loc ()) x

let mkpredef_call x = mkpredef_call (get_loc ()) x

(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)

let mkdim_int i = mkdim_int (get_loc ()) i

let mkdim_bool b = mkdim_bool (get_loc ()) b

let mkdim_ident id = mkdim_ident (get_loc ()) id

let mkdim_appl f args = mkdim_appl (get_loc ()) f args

let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e

let mkannots annots = { annots = annots; annot_loc = get_loc () }

    | Node _        , _                         -> raise (Error (loc, Already_bound_symbol msg))

 then raise (Error (loc, Already_bound_symbol msg))

 then raise (Error (loc, Unbound_symbol msg))

let check_node_symbol msg name value =

 if Hashtbl.mem node_table name

 then () (* TODO: should we check the types here ? *)

 else Hashtbl.add node_table name value

%token <string> STRING

%token REQUIRES ENSURES OBSERVER

%token INVARIANT BEHAVIOR ASSUMES

%token EXISTS FORALL

%nonassoc prec_exists prec_forall

%type <LustreSpec.top_decl list> prog

%type <bool -> LustreSpec.top_decl list> header

%start lustre_annot

%type <LustreSpec.expr_annot> lustre_annot

%start lustre_spec

%type <LustreSpec.node_annot> lustre_spec

     check_node_symbol ("node " ^ $3) $3 nd; 

     let loc = get_loc () in

     (fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }

			     node_annot = annots})

| NODESPEC nodespec_list { 

  (function 

  | None    -> (fun s1 -> Some s1) 

  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }

      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4)

| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}

lustre_spec:

| contract EOF { $1 }

contract:

requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }

requires:

{ [] }