CristalCaveGem » LustreC

  | Mismatch (cr1,cr2) ->

    raise (Error (loc, Carrier_mismatch (cr1,cr2)))

  match (repr ck1).cdesc, (repr ck2).cdesc with

(* Clocks a list of arguments of Lustre builtin operators:

   - type each expression, remove carriers of clocks as

(* emulates a subtyping relation between clocks c and (cr : c),

   used during node application only *)

  let loc = real_arg.expr_loc in

  let real_clock = clock_expr env real_arg in

(* computes clocks for node application *)

and clock_appl env f args clock_reset loc =

  let ck_outs = clock_of_vlist nd.node_outputs in

  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in

  unify_imported_clock None ck_node;

  (* Local variables may contain first-order carrier variables that should be generalized.

     That's not the case for types. *)

  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;

(*  if (is_main && is_polymorphic ck_node) then

    raise (Error (loc,(Cannot_be_polymorphic ck_node)));

*)

  nd.node_clock <- ck_node;

  Env.add_value env nd.node_id ck_node

  nd.nodei_clock <- ck_node;

  Env.add_value env nd.nodei_id ck_node

let clock_top_consts env clist =

  List.fold_left (fun env cdecl ->

    let ck = new_var false in

    clock_node env decl.top_decl_loc nd

  | ImportedNode nd ->

    clock_imported_node env decl.top_decl_loc nd

  | Consts clist ->

    clock_top_consts env clist

  | Open _ ->

      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)

  | ImportedNode nd ->

      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

  | Consts clist -> ()

  | Open _  -> ()

 (*

      if cvar.cscoped

      then

	  (name_of_type cvar.cid)

	  print_ckset cset

      else

 *)

	  (name_of_type cvar.cid)

	  print_ckset cset

  | Cunivar cset ->

(*

      if ck.cscoped

      then

      else

*)

    | Cunivar cset ->

(*

      if ck.cscoped

     mutable node_checks: Dimension.dim_expr list;

     node_asserts: assert_t list; 

     node_eqs: eq list;

     node_spec: LustreSpec.node_annot option;

     node_annot: LustreSpec.expr_annot option;

    }

     nodei_spec: LustreSpec.node_annot option;

    }

type const_desc = 

    {const_id: ident; 

     const_loc: Location.t; 

  | Node of node_desc

  | Consts of const_desc list

  | ImportedNode of imported_node_desc

  | Open of string

type top_decl =

  | No_main_specified

  | Unbound_symbol of ident

  | Already_bound_symbol of ident

module VDeclModule =

struct (* Node module *)

  | ImportedNode nd -> true

  | _ -> assert false

(* alias and type definition table *)

let type_table =

  Utils.create_hashtable 20 [

    fun consts decl ->

      match decl.top_decl_desc with

	| Consts clist -> clist@consts

  ) [] prog

    fun nodes decl ->

      match decl.top_decl_desc with

	| Node nd -> nd::nodes

  ) [] prog

let prog_unfold_consts prog =

    node_checks = node_checks;

    node_asserts = node_asserts;

    node_eqs = eqs;

    node_spec = spec;

    node_annot = annot;

  }

      | Consts c -> 

	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }

      | ImportedNode _

      | Open _ -> top)

      ::accu

) [] prog

    fprintf fmt "%s: " ind.nodei_id;

    Utils.reset_names ();

    fprintf fmt "%a@ " Types.print_ty ind.nodei_type

  | Consts _ | Open _ -> ()

let pp_prog_type fmt tdecl_list =

    fprintf fmt "%s: " ind.nodei_id;

    Utils.reset_names ();

    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock

let pp_prog_clock fmt prog =

  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog

    fprintf fmt

      "%s is already defined.@."

      sym

(* filling node table with internal functions *)

let vdecls_of_typ_ck cpt ty =

     mutable node_checks: Dimension.dim_expr list;

     node_asserts: assert_t list; 

     node_eqs: eq list;

     node_spec: LustreSpec.node_annot option;

     node_annot: LustreSpec.expr_annot option;}

     nodei_outputs: var_decl list;

     nodei_stateless: bool;

     nodei_spec: LustreSpec.node_annot option;}

type imported_fun_desc =

    {fun_id: ident;

     mutable fun_type: Types.type_expr;

     fun_inputs: var_decl list;

     fun_outputs: var_decl list;

     fun_spec: LustreSpec.node_annot option;}

type const_desc = 

    {const_id: ident; 

     const_loc: Location.t; 

  | Node of node_desc

  | Consts of const_desc list

  | ImportedNode of imported_node_desc

  (* | SensorDecl of sensor_desc *)

  (* | ActuatorDecl of actuator_desc *)

  | Open of string

  | No_main_specified

  | Unbound_symbol of ident

  | Already_bound_symbol of ident

val mktyp: Location.t -> type_dec_desc -> type_dec

val mkclock: Location.t -> clock_dec_desc -> clock_dec

val node_inputs: top_decl -> var_decl list

val node_from_name: ident -> top_decl

val is_generic_node: top_decl -> bool

val is_imported_node: top_decl -> bool

val consts_table: (ident, const_desc) Hashtbl.t

val sort_handlers : (label * 'a) list -> (label * 'a) list

val is_eq_expr: expr -> expr -> bool

val pp_error :  Format.formatter -> error -> unit

	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 

	  mkexpr loc (Expr_appl ("=", args, None))

      }];

    node_spec = Some 

      {requires = []; 

       ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];

  "last", LAST;

  "resume", RESUME;

  "restart", RESTART;

  "if", IF;

  "then", THEN;

  "else", ELSE;

    node_checks = [];

    node_asserts = [];

    node_eqs= [];

    node_spec = None;

    node_annot = None;  }

    mannot = None;

  }

let new_instance =

  let cpt = ref (-1) in

  fun caller callee tag ->

    begin

      let o =

	  node_name callee

	else

	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in

let const_of_carrier cr =

 match (carrier_repr cr).carrier_desc with

 | Carry_const id -> id

(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)

(* the context contains  m : state aka memory variables  *)

      NodeDep.filter_static_inputs (node_inputs node_f) el in 

    let o = new_instance node node_f eq.eq_rhs.expr_tag in

    (m,

     (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j),

     d,

     reset_instance node args o r eq.eq_rhs.expr_clock @

    mname = nd;

    mmemory = ISet.elements m;

    mcalls = mmap;

    minit = init;

    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;

    mstep = {

let extensions = [".ec"; ".lus"; ".lusi"]

let type_decls env decls =  

  report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?");

  let new_env = 

  | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 

    Parse.report_error err;

    raise exc

     Format.eprintf "Parsing error at loc %a: %a@]@."

       Location.pp_loc loc

       Corelang.pp_error err;

    | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 

      Parse.report_error err;

      raise exc

      Format.eprintf "Parsing error at loc %a: %a@]@."

	Location.pp_loc loc

	Corelang.pp_error err;

  (* Sorting nodes *)

  let prog = SortProg.sort prog in

  (* Typing *)

  let computed_types_env = type_decls type_env prog in

      let _, declared_types_env, declared_clocks_env = check_lusi header in

      (* checking type compatibility with computed types*)

      Typing.check_env_compat header declared_types_env computed_types_env;

      (* checking clocks compatibility with computed clocks*)

      Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;

      Clock_calculus.uneval_prog_generics prog

    with Sys_error _ -> ( 

      (* Printing lusi file is necessary *)

  | Expr_uclock _

  | Expr_dclock _ 

  | Expr_phclock _ -> assert false (* Not handled yet *)

and normalize_branches node offsets defvars hl =

 List.fold_right

   (fun (t, h) (defvars, norm_q) ->

  match decl.top_decl_desc with

  | Node nd ->

    {decl with top_decl_desc = Node (normalize_node nd)}

let normalize_prog decls = 

  List.map normalize_decl decls

| IDENT {

  try 

    mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1))

}

| TFLOAT {mktyp Tydec_float}

| TREAL {mktyp Tydec_real}

    | ImportedNode _, _ ->

       Hashtbl.add hashtbl name value

    | Node _        , _ -> 

    | _                 -> assert false

  with

    Not_found ->

let add_symbol msg hashtbl name value =

 if Hashtbl.mem hashtbl name

 else Hashtbl.add hashtbl name value

let check_symbol msg hashtbl name =

 if not (Hashtbl.mem hashtbl name)

 else ()

%}

  top_decl_header {(fun own -> [$1 own]) }

| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) }

top_decl_header:

    {let nd = mktop_decl (ImportedNode

                            {nodei_id = $3;

                             nodei_type = Types.new_var ();

                             nodei_clock = Clocks.new_var true;

                             nodei_inputs = List.rev $5;

                             nodei_outputs = List.rev $10;

    in

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

top_decl:

| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }

    {let eqs, asserts, annots = $16 in

     let nd = mktop_decl (Node

                            {node_id = $3;

			     node_checks = [];

			     node_asserts = asserts; 

                             node_eqs = eqs;

			     node_annot = match annots with [] -> None | _ -> Some annots})

    in

    add_node true ("node " ^ $3) node_table $3 nd; nd}

nodespec_list:

typ_def_list:

    /* empty */ {}

  ()

let pp_node fmt nd = 

  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec

  nd.node_id

  pp_node_args nd.node_inputs

  pp_node_args nd.node_outputs

(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)

let pp_imported_node fmt ind = 

    ind.nodei_id

    pp_node_args ind.nodei_inputs

    pp_node_args ind.nodei_outputs

    (fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless") 

let pp_decl fmt decl =

  match decl.top_decl_desc with

  | Node nd -> fprintf fmt "%a@ " pp_node nd

  | ImportedNode ind ->

    fprintf fmt "imported %a;@ " pp_imported_node ind

  | Consts clist -> (

    fprintf fmt "const %a@ " 

      (fprintf_list ~sep:"@ " (fun fmt cdecl ->

  match decl.top_decl_desc with

  | Node nd -> fprintf fmt "node %s@ " nd.node_id

  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id

  | Consts clist -> (

    fprintf fmt "const %a@ " 

      (fprintf_list ~sep:"@ " (fun fmt cdecl ->

      nd.node_id

      pp_node_args nd.node_inputs

      pp_node_args nd.node_outputs

    if List.map fst tl1 <> List.map fst tl2

    then raise (Unify (ty1, ty2))

    else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2

  | Tstatic (d1, t1)   , Tstatic (d2, t2)   ->

    begin

      sub_unify sub t1 t2;

      Dimension.eval Basic_library.eval_env (fun c -> None) d2;

      Dimension.unify d1 d2

    end

let try_sub_unify sub ty1 ty2 loc =

  try

	 | Some d' -> try_unify real_type real_static_type loc);

	 real_static_type

    else real_type in

  try_sub_unify sub real_type formal_type loc

and type_ident env in_main loc const id =

  type_expr env in_main const (expr_of_ident id loc)

  nd.nodei_type <- ty_node;

  new_env

let type_top_consts env clist =

  List.fold_left (fun env cdecl ->

    let ty = type_const cdecl.const_loc cdecl.const_value in

  )

  | ImportedNode nd ->

      type_imported_node env nd decl.top_decl_loc

  | Consts clist ->

      type_top_consts env clist

  | Open _  -> env

      uneval_node_generics (nd.node_inputs @ nd.node_outputs)

  | ImportedNode nd ->

      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

  | Consts clist -> ()

  | Open _  -> ()