CristalCaveGem » LustreC

  | Open _

  | Type _ -> env

  | Consts _

  | Open _

  | Type _   -> ()

let rec coretype_equal ty1 ty2 =

  let res = 

  match ty1, ty2 with

  | Tydec_any       , _

  | _               , Tydec_any        -> assert false

  | Tydec_const _   , Tydec_const _    -> get_repr_type ty1 = get_repr_type ty2

  | Tydec_const _   , _                -> let ty1' = Hashtbl.find type_table ty1

					  in (not (is_user_type ty1')) && coretype_equal ty1' ty2

  | _               , Tydec_const _    -> coretype_equal ty2 ty1

  | Tydec_int       , Tydec_int

  | Tydec_real      , Tydec_real

  | Tydec_float     , Tydec_float

  | Tydec_bool      , Tydec_bool       -> true

  | Tydec_clock ty1 , Tydec_clock ty2  -> coretype_equal ty1 ty2

  | Tydec_enum tl1  , Tydec_enum tl2   -> List.sort compare tl1 = List.sort compare tl2

  | Tydec_struct fl1, Tydec_struct fl2 ->

       List.length fl1 = List.length fl2

    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)

      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)

      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)

  | _                                  -> false

  in ((*Format.eprint "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)

	| Consts _ | ImportedNode _ | Open _ | Type _ -> nodes  

	| Node _ | ImportedNode _ | Open _ | Type _ -> consts  

let get_types prog = 

  List.fold_left (

    fun types decl ->

      match decl.top_decl_desc with

	| Type typ -> typ::types

	| Node _ | ImportedNode _ | Open _ | Consts _ -> types  

  ) [] prog

      | Open _

      | Type _ -> top)

  | Consts _ | Open _ | Type _ -> ()

  | Consts _ | Open _ | Type _ -> ()

val coretype_equal: type_dec_desc -> type_dec_desc -> bool

  | Dint i1   , Dint i2    -> i1 = i2

  | Dbool b1  , Dbool b2   -> b1 = b2

  | Dident id1, Dident id2 -> id1 = id2

  | _                      -> false

type type_def =

  {

    ty_def_id: ident;

    ty_def_desc: type_dec_desc}

| Type of type_def

      eprintf "Parsing error: %a%a@."

   (* checking defined types are compatible with declared types*)

    Typing.check_typedef_compat header;

 in  

  let machine_code = 

    if !Options.optimization >= 3 && !Options.output <> "horn" then

      begin

	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization@,");

	Optimize_machine.machines_fusion machine_code

      end

    else

      machine_code

  | Open _ | ImportedNode _ | Consts _ | Type _ -> decl

open Causality

let rec instr_assign res instr =

  match instr with

  | MLocalAssign (i, _) -> Disjunction.CISet.add i res

  | MStateAssign (i, _) -> Disjunction.CISet.add i res

  | MBranch (g, hl)     -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl

  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res

  | _                   -> res

and instrs_assign res instrs =

  List.fold_left instr_assign res instrs

let rec instr_constant_assign var instr =

  match instr with

  | MLocalAssign (i, Cst (Const_tag _))

  | MStateAssign (i, Cst (Const_tag _)) -> i = var

  | MBranch (g, hl)                     -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl

  | _                                   -> false

and instrs_constant_assign var instrs =

  List.fold_left (fun res i -> if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then instr_constant_assign var i else res) false instrs

let rec instr_reduce branches instr1 cont =

  match instr1 with

  | MLocalAssign (_, Cst (Const_tag c)) -> instr1 :: (List.assoc c branches @ cont)

  | MStateAssign (_, Cst (Const_tag c)) -> instr1 :: (List.assoc c branches @ cont)

  | MBranch (g, hl)                     -> MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl) :: cont

  | _                                   -> instr1 :: cont

and instrs_reduce branches instrs cont =

 match instrs with

 | []        -> cont

 | [i]       -> instr_reduce branches i cont

 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont

let rec instrs_fusion instrs =

  match instrs with

  | []

  | [_]                                                               ->

    instrs

  | i1::(MBranch (LocalVar v, hl))::q when instr_constant_assign v i1 ->

    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)

  | i1::(MBranch (StateVar v, hl))::q when instr_constant_assign v i1 ->

    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q) 

  | i1::i2::q                                                         ->

    i1 :: instrs_fusion (i2::q)

let step_fusion step =

  { step with

    step_instrs = instrs_fusion step.step_instrs;

  }

let rec machine_fusion m =

  { m with

    mstep = step_fusion m.mstep

  }

let machines_fusion prog =

  List.map machine_fusion prog

open LustreSpec

open Corelang

let add_symbol loc msg hashtbl name value =

 if Hashtbl.mem hashtbl name

 then raise (Error (loc, Already_bound_symbol msg))

 else Hashtbl.add hashtbl name value

let check_symbol loc msg hashtbl name =

 if not (Hashtbl.mem hashtbl name)

 then raise (Error (loc, Unbound_symbol msg))

 else ()

let add_node own name value =

  try

    match (Hashtbl.find node_table name).top_decl_desc, value.top_decl_desc with

    | Node _        , ImportedNode _ when own   -> ()

    | ImportedNode _, _                         -> Hashtbl.add node_table name value

    | Node _        , _                         -> raise (Error (value.top_decl_loc, Already_bound_symbol ("node " ^ name)))

    | _                                         -> assert false

  with

    Not_found                                   -> Hashtbl.add node_table name value

let add_tag loc own name typ =

  if Hashtbl.mem tag_table name && (not own) then

    raise (Error (loc, Unbound_symbol ("enum tag " ^ name)))

  else Hashtbl.add tag_table name typ

let add_field loc own name typ =

  if Hashtbl.mem field_table name && (not own) then

    raise (Error (loc, Unbound_symbol ("struct field " ^ name)))

  else Hashtbl.add field_table name typ

let rec check_type_def loc own name ty =

  match ty with

  | Tydec_enum tl   ->

    begin

      List.iter (fun tag -> add_tag loc own tag (Tydec_const name)) tl;

      ty

    end

  | Tydec_struct fl -> 

    begin

      List.iter (fun (field, _) -> add_field loc own field (Tydec_const name)) fl;

      Tydec_struct (List.map (fun (f, ty) -> (f, check_type_def loc own name ty)) fl)

    end

  | Tydec_clock ty      -> Tydec_clock (check_type_def loc own name ty)

  | Tydec_const c       ->

    if not (Hashtbl.mem type_table (Tydec_const c))

    then raise (Error (loc, Unbound_symbol ("type " ^ c)))

    else get_repr_type ty

  | Tydec_array (c, ty) -> Tydec_array (c, check_type_def loc own name ty)

  | _                   -> ty

let add_type own name value =

(*Format.eprintf "add_type %B %s@." own name;*)

  match value.top_decl_desc with

  | Type ty ->

    let loc = value.top_decl_loc in

    if Hashtbl.mem type_table (Tydec_const name) && (not own)

    then raise (Error (loc, Already_bound_symbol ("type " ^ name)))

    else Hashtbl.add type_table (Tydec_const name) (check_type_def loc own name ty.ty_def_desc)

  | _       -> assert false

let check_type loc name =

 if not (Hashtbl.mem type_table (Tydec_const name))

 then raise (Error (loc, Unbound_symbol ("type " ^ name)))

 else ()

open Utils

open Parse

 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }

typ_def_prog:

 typ_def_list { $1 true }

 open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ let typs = $2 own in typs @ (List.rev ($3 own)))) }

   {[]}

   {(fun own -> []) }

| top_decl_header_list top_decl_header {(fun own -> let h1 = $1 own in ($2 own)::h1) }

     (fun own -> add_node own $3 nd; nd) }

     add_node true $3 nd; nd}

    /* empty */             { (fun own -> []) }

| typ_def SCOL typ_def_list { (fun own -> let ty1 = ($1 own) in ty1 :: ($3 own)) }

  TYPE IDENT EQ typ_def_rhs { let typ = mktop_decl (Type { ty_def_id = $2;

							   ty_def_desc = $4

							 })

			      in (fun own -> add_type own $2 typ; typ) }

typ_def_rhs:

  typeconst                   { $1 }

| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }

| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }

  TINT array_typ_decl   { $2 Tydec_int }

| TBOOL array_typ_decl  { $2 Tydec_bool  }

| TREAL array_typ_decl  { $2 Tydec_real  }

| IDENT array_typ_decl  { $2 (Tydec_const $1) }

| TBOOL TCLOCK          { Tydec_clock Tydec_bool }

| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }

  IDENT                { $1 :: [] }

| tag_list COMMA IDENT { $3 :: $1 }

field_list:                           { [] }

| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }

let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq

let rec pp_var_struct_type_field fmt (label, tdesc) =

  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc

and pp_var_type_dec_desc fmt tdesc =

  match tdesc with 

  | Tydec_any -> fprintf fmt "<any>"

  | Tydec_int -> fprintf fmt "int"

  | Tydec_real -> fprintf fmt "real"

  | Tydec_float -> fprintf fmt "float"

  | Tydec_bool -> fprintf fmt "bool"

  | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t

  | Tydec_const t -> fprintf fmt "%s" t

  | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list

  | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:" " pp_var_struct_type_field) f_list

  | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s

  pp_var_type_dec_desc fmt ty.ty_dec_desc

let pp_type_def fmt ty =

  fprintf fmt "type %s = %a;@ " ty.ty_def_id pp_var_type_dec_desc ty.ty_def_desc

  | Open (local, s) -> if local then fprintf fmt "open \"%s\"@ " s else fprintf fmt "open <%s>@ " s

  | Type tdef -> fprintf fmt "%a@ " pp_type_def tdef

  | Open (local, s) -> if local then fprintf fmt "open \"%s\"@ " s else fprintf fmt "open <%s>@ " s

  | Type tdef -> fprintf fmt "type %s;@ " tdef.ty_def_id

| Open (local, s) -> if local then fprintf fmt "open \"%s\"@ " s else fprintf fmt "open <%s>@ " s

| Type tdef -> fprintf fmt "%a@ " pp_type_def tdef

| ImportedNode _ -> ()

  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));

  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@.@.";

   Moreover, the dependency graph is browsed in a depth-first manner whenever possible,

   to improve the behavior of optimization algorithms applied in forthcoming compilation steps. 

  | Type_mismatch of ident

  | Type_mismatch id ->

    fprintf fmt "Definition and declaration of type %s don't agree@." id

  | Type _

  | Consts _

  | Type _

let check_typedef_top decl =

  match decl.top_decl_desc with

  | Type ty ->

Format.eprintf "check_typedef %a %a@." Printers.pp_var_type_dec_desc ty.ty_def_desc Printers.pp_var_type_dec_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id));

    if coretype_equal ty.ty_def_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id)) then ()

    else raise (Error (decl.top_decl_loc, Type_mismatch ty.ty_def_id))

  | _  -> ()

let check_typedef_compat header =

  List.iter check_typedef_top header