CristalCaveGem » LustreC

#define _arrow_clear(self) {}

#define _arrow_reset(self) {(self)->_reg._first = 1;}

  match cr.carrier_desc with

  | Carry_const _

  | Carry_name ->

  | Carry_var -> ()

  | Carry_link cr' -> generalize_carrier cr'

(** Promote monomorphic clock variables to polymorphic clock variables. *)

(* Generalize by side-effects *)

let rec generalize ck =

let try_generalize ck_node loc =

  try 

    generalize ck_node

    raise (Error (loc, Carrier_extrusion (ck_node, cr)))

    raise (Error (loc, Clock_extrusion (ck_node, ck)))

(* Clocks instanciation *)

  let rec aux ck =

    match (repr ck).cdesc with

    | Cvar ->

    | Ctuple cl ->

    | Carrow (ck1,ck2) ->

    | Ccarrying (_, ck1) ->

    | Con (ck1, _, _) -> aux ck1

    | _ -> ()

  in

(** [clock_eq env eq] performs the clock-calculus for equation [eq] in

    environment [env] *)

let clock_eq env eq =

  let ck_rhs = clock_expr env eq.eq_rhs in

  clock_subtyping_arg env expr_lhs ck_rhs

    else

 *)

      if Types.get_clock_base_type vdecl.var_type <> None

      else ck in

  (if vdecl.var_dec_const

   then match vdecl.var_dec_value with

  List.iter (clock_eq new_env) eqs;

  let ck_ins = clock_of_vlist nd.node_inputs in

  let ck_outs = clock_of_vlist nd.node_outputs in

  unify_imported_clock None ck_node loc;

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

     That's not the case for types. *)

  try_generalize ck_node loc;

  (*  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

 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))

let clock_current ck =

let clock_of_impnode_clock ck =

  let ck = repr ck in

  | Factor_zero ->

    fprintf fmt "Cannot apply clock transformation with factor 0@."

  | Carrier_extrusion (ck,cr) ->

      print_ck ck

      print_carrier cr

  | Clock_extrusion (ck_node,ck) ->

      print_ck ck_node

      print_ck ck

  | Node nd ->

    fprintf fmt "%s: " nd.node_id;

    Utils.reset_names ();

  | ImportedNode ind ->

    fprintf fmt "%s: " ind.nodei_id;

    Utils.reset_names ();

  | Const _ | Include _ | Open _ | TypeDef _ -> ()

let pp_prog_type fmt tdecl_list =

let pp_decl_clock fmt cdecl =

  match cdecl.top_decl_desc with

(* Datastructure updated while visiting equations *)

type machine_ctx = {

  (* Memories *)

  m: VSet.t;

  (* Reset instructions *)

  t: mc_formula_t list;

}

  m = VSet.empty;

  si = [];

  j = IMap.empty;

  t = []

}

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

(* Main function to translate equations into this machine context we

   are building *) 

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

  mkinstr

    (MBranch (v, [l, [inst]]))

    match (Clocks.repr ck).cdesc with

    | Con (ck, cr, l) ->

      let id = Clocks.const_of_carrier cr in

      let ck_spec = mk_condition v l in

      aux (id :: ck_ids,

           v :: vs,

           },

    | _ -> acc

  in

let reset_instance env i r c =

  match r with

  | Some r ->

  | None -> []

  let translate_expr = translate_expr env in

  let translate_act = translate_act env in

  in

  let reset_instance = reset_instance env in

  let mkinstr' = mkinstr ~lustre_eq:eq True in

  (* Format.eprintf "translate_eq %a with clock %a@." 

     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)

  match eq.eq_lhs, eq.eq_rhs.expr_desc with

  | [x], Expr_arrow (e1, e2)                     ->

    let var_x = env.get_var x in

    let c1 = translate_expr e1 in

    let c2 = translate_expr e2 in

    { ctx with

      si = mkinstr True (MReset o) :: ctx.si;

    }

  | [x], Expr_pre e1 when env.is_local x    ->

    let var_x = env.get_var x in

    { ctx with

      m = VSet.add var_x ctx.m;

    }

  | [x], Expr_fby (e1, e2) when env.is_local x ->

    let var_x = env.get_var x in

    { ctx with

      m = VSet.add var_x ctx.m;

      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;

    }

  | p, Expr_appl (f, arg, r)

    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->

    let var_p = List.map (fun v -> env.get_var v) p in

        el [eq.eq_rhs.expr_clock] in

    let call_ck = Clock_calculus.compute_root_clock

        (Clock_predef.ck_tuple env_cks) in

    (*Clocks.new_var true in

      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;

      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)

           else reset_instance o r call_ck)

          @ ctx.s

    }

  | [x], _ ->

    let var_x = env.get_var x in

  | _ ->

    Format.eprintf "internal error: Machine_code.translate_eq %a@?"

      Printers.pp_node_eq eq;

    locals []

let translate_eqs env ctx eqs =

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

    in

    vars, eql, assertl

  let constant_eqs = constant_equations locals in

  let env = build_env locals other_vars  in

  (* Compute constants' instructions  *)

  assert (VSet.is_empty ctx0.m);

  assert (ctx0.si = []);

  assert (IMap.is_empty ctx0.j);

  (* Compute ctx for all eqs *)

  ctx, ctx0.s

   *   VSet.pp inout_vars

   * ; *)

  (* Format.eprintf "ok4@.@?"; *)

open Spec_types

open Spec_common

open Corelang

let print_statelocaltag = true

let is_memory m id =

  | Var v    ->

     if is_memory m v then

       if print_statelocaltag then

       else

     else     

       if print_statelocaltag then

       else

let rec  pp_instr m fmt i =

 let     pp_val = pp_val m and

      pp_branch = pp_branch m in

  let _ =

    match i.instr_desc with

    | MStep (il, i, vl)  ->

	 i

	 (Utils.fprintf_list ~sep:", " pp_val) vl

    | MBranch (g,hl)     ->

	 pp_val g

	 (Utils.fprintf_list ~sep:"@," pp_branch) hl

  in

  (* Annotation *)

  (* let _ = *)

  (* in *)

and pp_branch m fmt (t, h) =

(* merge log: get_node_def was in c0f8 *)

    let (decl, _) = List.assoc id m.mcalls in

    Corelang.node_of_top decl

  with Not_found -> ( 

    (*   id *)

    (* ; *)

    raise Not_found

  )

let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory

let pp_step m fmt s =

let pp_static_call fmt (node, args) =

   (node_name node)

   (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args

let pp_machine fmt m =

    "@[<v 2>machine %s@ \

     mem      : %a@ \

     instances: %a@ \

     annot    : @[%a@]@]@ "

    m.mname.node_id

    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory

    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit

    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst

    (pp_step m) m.mstep

    (fun fmt -> match m.mspec.mnode_spec with

       | None -> ()

       | Some (Contract spec) -> Printers.pp_spec fmt spec)

    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot

let pp_machines fmt ml =

let rec is_const_value v =

let mk_conditional ?lustre_eq c t e =

  mkinstr ?lustre_eq

    (MBranch(c, [

         (tag_true, t);

         (tag_false, e) ]))

let mk_branch ?lustre_eq c br =

  mkinstr ?lustre_eq

    (MBranch (c, br))

let mk_assign ?lustre_eq x v =

  mkinstr ?lustre_eq

    (MLocalAssign (x, v))

let mk_val v t =

 try

    Utils.desome (get_machine_opt machines node_name) 

 with Utils.DeSome ->

     node_name

      ; assert false

let get_const_assign m id =

type static_call = top_decl * (Dimension.dim_expr list)

type machine_spec = {

  mnode_spec: node_spec_t option;

}

type machine_t = {

type predicate_t =

  (* | Memory_pack *)

  | Clocked_on of ident

  | Initialization

type 'a formula_t =

  | Tarray (e, ty) ->

    fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e

  | Tlink ty ->

  | Tunivar ->

    fprintf fmt "'%s" (name_of_type ty.tid)

      let rec unif t1 t2 =

        let t1 = repr t1 in

        let t2 = repr t2 in

          ()

        else

          match t1.tdesc,t2.tdesc with

          (* strictly subtyping cases first *)

          | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->

          | _ , Tstatic (_, t2) when sub && (get_static_value t1 = None) ->

          (* This case is not mandatory but will keep "older" types *)

          | Tvar, Tvar ->

          | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->

          | _, Tvar when (not (occurs t2 t1)) ->

          | Tarrow (t1,t2), Tarrow (t1',t2') ->

          | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->

          | Ttuple [t1]        , _                  -> unif t1 t2

          | _                  , Ttuple [t2]        -> unif t1 t2

          | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->

          | Tclock _, Tstatic _

          | Tclock t1', Tclock t2' -> unif t1' t2'

          | Tunivar, _ | _, Tunivar -> ()

          | (Tconst t, _) ->

          | (_, Tconst t)  ->

          | Tenum tl, Tenum tl' when tl == tl' -> ()

          | Tstatic (e1, t1'), Tstatic (e2, t2')

          (* Special cases for machine_types. Rules to unify static types infered

          | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2

          | _,_ -> raise (Unify (t1, t2))

      in unif t1 t2

      try

        unify ~sub:sub ~semi:semi ty1 ty2

      with

         raise (Error (loc, Type_clash (ty1,ty2)))

      | Dimension.Unify _ ->

         raise (Error (loc, Type_clash (ty1,ty2)))