CristalCaveGem » LustreC

  if !Options.lusi || !Options.print_nodes then

      else if !Options.print_nodes then (

        Format.printf "%a@.@?" Printers.pp_node_list prog;

        exit 0

      )

  let prog, dependencies =

    try

      Compiler_stages.stage1 params prog dirname basename extension 

   with Compiler_stages.StopPhase1 prog -> (

      if !Options.print_nodes then (

        Format.printf "%a@.@?" Printers.pp_node_list prog;

        exit 0

      )

      else

        assert false

    )

 in

      if !Options.print_nodes then (

        Format.printf "%a@.@?" Printers.pp_node_list prog;

        exit 0

      )

      else

let print_nodes = ref false

    "-print-nodes",  Arg.Set print_nodes, "prints node list";

let pp_node_list fmt prog =

  Format.fprintf fmt "@[<h 2>%a@]"

    (fprintf_list

       ~sep:"@ "

       (fun fmt decl ->

         match decl.top_decl_desc with

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

         | _ -> ()

    ))

    prog

           (pp_sys Printers.pp_expr) sw

let funsw_to_lustre m update_out =

  let orig_nd = m.mname in

  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in

  let output_eq =

    let e_update_out = process_sw copy_nd.node_outputs  (fun x -> x) update_out in

    [ 

      Eq

        { eq_loc = Location.dummy_loc;

          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 

          eq_rhs = e_update_out

        };

    ]

  in

  let new_nd =

    { copy_nd with

      node_id = copy_nd.node_id ^ "_seal";

      node_locals = [];

      node_stmts = output_eq;

    }

  in

  new_nd, orig_nd

let to_lustre basename prog new_node orig_node =

  let check_nd = Lustre_utils.check_eq new_node orig_node in

  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top])

let node_to_lustre basename prog m sw_init sw_step init_out update_out =

  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in

  to_lustre basename prog new_node orig_nd

let fun_to_lustre basename prog m update_out =

  let new_node, orig_nd = funsw_to_lustre m update_out in

  to_lustre basename prog new_node orig_nd

    (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *)

           let el = Corelang.expr_list_of_expr args in

           let eltyp = List.map (fun e -> e.expr_type) el in

           let elv = List.map e2ze el in

           let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in

       let new_e = { new_e with expr_type = expr.expr_type; expr_clock = expr.expr_clock } in

                              (pp_guard_list Printers.pp_expr) gl (pp_up Printers.pp_expr) up) res);

let build_environement  consts (mems:var_decl list) nd =

  Z3.Params.update_param_value !ctx "timeout" "10000";

  mem_defs, output_defs 

(* Iter through the elements and gather them by updates *)

let merge_updates sys =

  (* The map will associate to each update up the pair (set, set

       list) where set is the share guards and set list a list of

       disjunctive guards. Each set represents a conjunction of

       expressions. *)

  (* We perform multiple pass to avoid errors *)

  let map =

    List.fold_left (fun map (gl,up) ->

        (* creating a new set to describe gl *)

        let new_set =

          List.fold_left

            (fun set g -> Guards.add g set)

            Guards.empty

            gl

        in

        (* updating the map with up -> new_set *)

        if UpMap.mem up map then

          let guard_set = UpMap.find up map in

          UpMap.add up (new_set::guard_set) map

        else

          UpMap.add up [new_set] map

      ) UpMap.empty sys

  (* Processing the set of guards leading to the same update: return

       conj, disj with conf is a set of guards, and disj a DNF, ie a

       list of set of guards *)

  let map =

    UpMap.map (

        fun guards ->

        match guards with

        | [] -> Guards.empty, [] (* Nothing *)

        | [s]-> s, [] (* basic case *)

        | hd::tl ->

           let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in

           let remaining = List.map (fun s -> Guards.diff s shared) guards in

           (* If one of them is empty, we can remove the others, otherwise keep them *)

           if List.exists Guards.is_empty remaining then

             shared, []

           else

             shared, remaining

      ) map

  let rec mk_binop op l = match l with

      [] -> assert false

    | [e] -> e

    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]

  let gl_as_expr gl =

    let gl = Guards.elements gl in

    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 

    match gl with

      [] -> []

    | [e] -> [export e]

    | _ ->

       [mk_binop "&&"

          (List.map export gl)]

  let rec clean_disj disj =

    match disj with

    | [] -> []

    | [_] -> assert false (* A disjunction with a single case can be ignored *) 

    | _::_::_ -> (

      (* First basic version: producing a DNF One can later, (1)

           simplify it with z3, or (2) build the compact tree with

           maximum shared subexpression (and simplify it with z3) *)

      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in

      let or_expr = mk_binop "||" elems in

      [or_expr]

    (* TODO disj*)

    (* get the item that occurs in most case *)

    (* List.fold_left (fun accu s ->

     *     List.fold_left (fun accu (e,b) ->

     *         if List.mem_assoc (e.expr_tag, b)

     *       ) accu (Guards.elements s)

     *   ) [] disj *)

    )

  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);

  UpMap.fold (fun up (common, disj) accu ->

      if !seal_debug then

        report ~level:6 (fun fmt -> Format.fprintf fmt 

                                      "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."

                                      Guards.pp_short common

                                      (fprintf_list ~sep:";@ " Guards.pp_long) disj

                                      UpMap.pp up);

      let disj = clean_disj disj in

      let guard_expr = (gl_as_expr common)@disj in

      ((match guard_expr with

        | [] -> None 

        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu

    ) map []

(* Take a normalized node and extract a list of switches: (cond,

   update) meaning "if cond then update" where update shall define all

   node memories. Everything as to be expressed over inputs or

   memories, intermediate variables are removed through inlining *)

let node_as_switched_sys consts (mems:var_decl list) nd =

  let mem_defs, output_defs = build_environement consts mems nd in

  let init_defs, update_defs = split_init mem_defs in

  let init_out, update_out =   split_init output_defs in

  report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@."

                                (pp_assign_map pp_elem) init_defs

                                (pp_assign_map pp_elem) update_defs);

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "init/step as a switched system ...@.");

  let sw_init= build_switch_sys init_defs [] in

  let sw_sys = build_switch_sys update_defs [] in

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "init/step as a switched system ... done@.");

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "output function as a switched system ...@.");

  let init_out =   build_switch_sys init_out [] in

  let update_out = build_switch_sys update_out [] in

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "output function as a switched system ... done@.");

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "removing dead branches and merging remaining ...@.");

  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");

  let sw_init = merge_updates sw_init in

  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");

  let sw_sys = merge_updates sw_sys in

  report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");

  let init_out = merge_updates init_out in

  report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");

  let update_out = merge_updates update_out in

  report ~level:1 (fun fmt ->

      Format.fprintf fmt "removing dead branches and merging remaining ... done@.");

  sw_init , sw_sys, init_out, update_out

let fun_as_switched_sys consts  nd =

  let _, update_out = build_environement consts [] nd in

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "output function as a switched system ...@.");

  let update_out = build_switch_sys update_out [] in

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "output function as a switched system ... done@.");

  report ~level:1 (fun fmt -> Format.fprintf fmt

                                "removing dead branches and merging remaining ...@.");

  let update_out = clean_sys update_out in

  let update_out = merge_updates update_out in

  report ~level:1 (fun fmt ->

      Format.fprintf fmt "removing dead branches and merging remaining ... done@.");

  update_out

                                (* Some code that was used to check for duplicate entries in guards.

                                 *)

  Format.fprintf fmt "@[<v 2>@[%a@] ->@ @[<hov 2>%a@]@]"

let pp_assign_map pp_elem =

  fprintf_list ~sep:"@ "

    (fun fmt (m, mdefs) ->

      Format.fprintf fmt

        "%s -> @[<v 0>[%a@] ]@ "

        m

        (pp_mdefs pp_elem) mdefs

    )

let pp_up pp_elem fmt up =

  fprintf_list ~sep:"@ "

    (fun fmt (id,e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e)

    fmt

    up 

let pp_sys pp_elem fmt sw =

  fprintf_list ~sep:"@ "

    (fun fmt (gl,up) ->

      match gl with

      | None ->

         (pp_up pp_elem) fmt up

      | Some gl ->

         Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]"

           Printers.pp_expr gl (pp_up pp_elem) up)

    fmt

    sw

        let pp = pp_up Printers.pp_expr 

open Seal_slice

open Seal_extract

open Seal_utils

let active = ref false

let seal_export = ref None

let set_export s = match s with

  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s

  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)

  (* Slicing node *)

  report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd);

  let pp_sys = pp_sys Printers.pp_expr in

  if List.length mems = 0 then

    begin (* A stateless node = a function ! *)

      let update_out = fun_as_switched_sys consts sliced_nd in

      report ~level:1 (fun fmt ->

          Format.fprintf fmt

            "Output (%i step switch cases):@ @[<v 0>%a@]@."

            (List.length update_out)

            pp_sys update_out

        );

      let _ = match !seal_export with

        | Some "lustre" | Some "lus" ->

           Seal_export.fun_to_lustre basename prog m update_out  

        | Some "matlab" | Some "m" -> assert false (* TODO *)

        | Some _ -> assert false 

        | None -> ()

      in

      ()

    end

  else

    begin (* A stateful node *)

      let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in

      report ~level:1 (fun fmt ->

          Format.fprintf fmt

            "DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."

            (List.length mems)

            (List.length sw_init)

            (List.length sw_sys)

            pp_sys  sw_init

            pp_sys  sw_sys

        );

      report ~level:1 (fun fmt ->

          Format.fprintf fmt

            "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."

            (List.length init_out)

            (List.length update_out)

            pp_sys  init_out

            pp_sys  update_out

        );

      let _ = match !seal_export with

        | Some "lustre" | Some "lus" ->

           Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out update_out  

        | Some "matlab" | Some "m" -> assert false (* TODO *)

        | Some _ -> assert false 

        | None -> ()

      in

      ()

    end

let report = Log.report ~plugin:"z3 interface"

  with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt  "Unable to find func_decl %s@.@?" id); raise Not_found)

(* Declaring the function used in expr *) 

let decl_fun op args typ =

  let args = List.map type_to_sort args in

  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in

  register_fdecl op fdecl;

  fdecl

let horn_basic_app i vl (vltyp, typ) =

  | "ite", [v1; v2; v3] ->  Z3.Boolean.mk_ite !ctx v1 v2 v3

  | "uminus", [v] ->    Z3.Arithmetic.mk_unary_minus

       !ctx v

       !ctx v

       !ctx v1 v2

       [v1; v2]

       [v1;

         v2]

       !ctx v1 v2

       !ctx v1 v2

       v1 v2

       !ctx v1 v2

           !ctx v1 v2

       !ctx v1 v2

       [v1; v2]

       [v1 ;  v2]

       [ v1;  v2]

       !ctx v1 v2

       !ctx v1 v2

       !ctx v1 v2

       !ctx v1 v2

       !ctx v1

  | _ ->

     let fd =

       try

         get_fdecl i

       with Not_found -> begin

           report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); 

           decl_fun i vltyp typ

         end

     in

     Z3.FuncDecl.apply fd vl

(* | _ -> (

 *     let msg fmt = Format.fprintf fmt

 *                     "internal error: zustre unkown function %s (nb args = %i)@."

 *                     i (List.length vl)

 *     in

 *     raise (UnknownFunction(i, msg))

 *   ) *)

  (* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)

  | Fun (n, vl)   -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type)