CristalCaveGem » LustreC

wrap-comments=true

cases-exp-indent=2

break-cases=nested

(*  version 2.1.                                                    *)

(*                                                                  *)

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

open Lustre_types

open Machine_code_types

open C_backend_common

let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string

    | [] ->

      pp_print_string fmt mem

  in

  aux fmt

module PrintSpec = struct

  type mode =

     fun ?output fmt e -> pp_expr ?output m mem_out fmt e

    in

    match p with

      let pp_mem_in, pp_mem_out =

        match inst with

        | None ->

          ( pp_print_string,

        | Some inst ->

          ( (fun fmt mem_in ->

              if r then pp_print_string fmt mem_in

      eprintf "Internal error: arrow not found";

      raise Not_found

    let rec pp_spec mode fmt f =

      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =

        let self = mk_self m in

          fmt

          ((f, mk_mem_reset m), (rc, tr))

    in

end

let pp_predicate pp_l pp_r fmt (l, r) =

    t.tindex

let pp_transition_footprint_lemma m fmt t =

  let name = t.tname.node_id in

  let mems =

  in

  let memories =

    List.map

      (fun v -> { v with var_type = { v.var_type with tid = -1 } })

  in

    pp_acsl

      (pp_lemma pp_transition_footprint

      fmt

      ( t,

let pp_transition_footprint_lemmas fmt m =

  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0

let rec translate_act env (y, expr) =

  let translate_act = translate_act env in

  let translate_guard = translate_guard env in

  let translate_expr = translate_expr env in

  let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in

  match expr.expr_desc with

    * var_decl list

    (* outputs *)

    * ISet.t (* memory footprint *)

    * mc_formula_t)

    (* formula *)

    list;

      locals_i,

      outputs_i,

      ctx.m,

      Exists

        ( Lustre_live.existential_vars id i eq (locals @ outputs),

          And

        (MStep ([ var_x ], inst, [ c1; c2 ]))

        (mk_memory_pack ~inst (node_name td))

        (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])

    in

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

    let var_x = env.get_var x in

    let e = translate_expr e in

        (MStep (var_p, inst, vl))

        (mk_memory_pack ~inst (node_name node_f))

        (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))

    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:

      si =

        (if Stateless.check_node node_f then ctx.si

        else mkinstr (MSetReset inst) :: ctx.si);

    }

  | [ x ], _ ->

    let var_x = env.get_var x in

    tlocals = [];

    toutputs = [];

    tformula = True;

  }

let transition_toplevel nd i =

    tformula =

      (if fst (get_stateless_status_node nd) then tr

      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));

  }

let translate_decl nd sch =

    transition_0 nd

    ::

    List.mapi

        {

          tname = nd;

          tindex = Some (i + 1);

          tlocals;

          toutputs;

          tformula = red f;

        })

      (List.rev ctx.t)

    @ [ transition_toplevel nd (List.length ctx.t) ]

     fun fmt e -> pp_expr m fmt e

    in

    match p with

      fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f

        (pp_print_option

           ~none:(fun fmt () -> pp_print_string fmt "SELF")

  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)

let mk_conditional ?lustre_eq c t e =

let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)

let arrow_machine =

  let state = "_first" in

  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in

  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in

  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in

open Spec_types

(* a small reduction engine *)

let is_true = function True -> true | _ -> false

    f

(* smart constructors *)

let vals vs = List.map (fun v -> Val v) vs

let mk_pred_call pred = Predicate pred

  let tr =

    mk_pred_call

      (Transition

           vals locals,

           vals outputs,

           (match r with Some _ -> true | None -> false),

  in

  match r, inst with

  | Some r, Some inst ->

let mk_conditional_tr v t f = Ternary (Val v, t, f)

let mk_assign_tr x v = Equal (Var x, Val v)

      (* outputs *)

      * bool (* reset *)

      * Utils.ISet.t (* memory footprint *)

      -> 'a predicate_t

  | Reset of ident * ident * 'a

  | MemoryPack of ident * ident option * int option

  tlocals : var_decl list;

  toutputs : var_decl list;

  tformula : 'a formula_t;

}

    x y

let pp_env pp_fun fmt env =

  let pp_fun fmt (id, value) = Format.fprintf fmt "%s |-> %a" id pp_fun value in

  Format.fprintf fmt "{ @[<v 2>%a@] }" (fprintf_list ~sep:"@," pp_fun) l'

module IMap = struct

  include Map.Make (IdentModule)

    merge

      (fun _ o1 o2 ->

        match o1, o2 with

      m1 m2

end

module ISet = Set.Make (IdentModule)

    | t :: q ->

      if p t then t :: filter_upto p (n - 1) q else filter_upto p n q

(** [gcd a b] returns the greatest common divisor of [a] and [b]. *)

let rec gcd a b = if b = 0 then a else gcd b (a mod b)