CristalCaveGem » LustreC

open Seal_utils

let process_sw vars f_e sw =

  let process_branch g_opt up =

    let el = List.map (fun (v,e) -> v, f_e e) up in

    (* Sorting list of elements, according to vars, safety check to

    let el, forgotten = List.fold_right (fun v (res, remaining) ->

                            let vid = v.var_id in

                            if List.mem_assoc vid remaining then

                              ((List.assoc vid remaining)::res),

                              (List.remove_assoc vid remaining)

                            else (

                              Format.eprintf

                                "Looking for variable %s in remaining expressions: [%a]@."

                                vid

                                (Utils.fprintf_list ~sep:";@ "

                                   (fun fmt (id,e) ->

                                     Format.fprintf fmt

                                       "(%s -> %a)"

                                       id

                                       Printers.pp_expr e))

                                remaining;

                              assert false (* Missing variable v in list *)

                            )

                          ) vars ([], el)

    assert (forgotten = []);

    let loc = (List.hd el).expr_loc in

    let new_e = Corelang.mkexpr loc (Expr_tuple el) in

    match g_opt with

      None -> None, new_e, loc

    | Some g ->

       let g = f_e g in

       let ee = Corelang.mkeexpr loc g in

       let new_e = if verbose then

                     {new_e with

                       expr_annot =

                         Some ({annots = [["seal";"guards"],ee];

                                annot_loc = loc})} else new_e 

       in

       Some g, new_e, loc

  in

  let rec process_sw f_e sw = 

    match sw with

       | None -> (

         Format.eprintf "SEAL issue: process_sw with %a"

           pp_sys sw

       ;

         assert false (* How could this happen anyway ? *)

       )

  process_sw f_e sw

let sw_to_lustre m sw_init sw_step init_out update_out =

  let orig_nd = m.mname in

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

  let vl = (* memories *)

    match sw_init with

    | [] -> assert false

    | (gl, up)::_ -> List.map (fun (v,_) -> v) up

  in    

      if !seal_debug then (

        report ~level:6 (fun fmt -> Format.fprintf fmt "Checking implication: %s => %s?@ "

      )); 

          | Z3.Solver.UNSATISFIABLE -> if !seal_debug then

                                         report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ "); 

          | _ -> if !seal_debug then report ~level:6 (fun fmt -> Format.fprintf fmt "not proved valid@ "); 

let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolexpr guard) =

    Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l; 

    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l; 

    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;

let rec rewrite defs expr : elem_guarded_expr list =

       let rec aux gell : (elem_boolexpr guard * expr list) list =

                      let new_gt : elem_boolexpr guard * expr list = (guard_comb, (deelem e)::minituple) in

let split_mdefs elem (mdefs: elem_guarded_expr list) =

          (pp_mdefs pp_elem) mdefs;

      (mem_defs: (ident * elem_guarded_expr list) list)

      ((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)

          (mem_defs : (Utils.ident * elem_guarded_expr list) list )

  if !seal_debug then

    report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."

         (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]"

                                 (pp_mdefs pp_elem) gel))

      mem_defs);

  let res =

      None -> assert false (* Otherwise the first case should have matched *)

      report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);

         let ok_neg, neg_prefix = clean neg_prefix in

         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);

         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in

         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);

         let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in

         ok_l @ nok_l

  in

    if !seal_debug then (

      report ~level:4 (fun fmt ->

          Format.fprintf fmt

            "@[<v 2>===> @[%t@ @]@]@ @]@ "

            (fun fmt -> List.iter (fun (gl,up) ->

                            Format.fprintf fmt "[@[%a@]] -> (%a)@ "

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

    ));

    res

  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in

               report ~level:3 (fun fmt ->

                   Format.fprintf fmt "Registering variable %s@." vid);

               add_def vid eq.eq_rhs;

               accu_mems, accu_outputs

             )

        "@[<v 0>%a@]@."

                  (pp_guard_expr pp_elem)) mdefs

        "@[<v 0>Init:@ %a@]@."

                  (pp_guard_expr pp_elem)) mdefs

        init_defs);

  report ~level:3

    (fun fmt ->

      Format.fprintf fmt

        "@[<v 0>Step:@ %a@]@."

                  (pp_guard_expr pp_elem)) mdefs

  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@.");

  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@.");

  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@.");

  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@.");

    report ~level:3 (fun fmt -> Format.fprintf fmt "%t@."

                                  (fun fmt -> List.iter (fun (gl,up) ->

                                                  Format.fprintf fmt "[@[%a@]] -> (%a)@ "

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

    (* We perform multiple pass to avoid errors *)

    let map =

            let guard_set = UpMap.find up map in

            UpMap.add up (new_set::guard_set) map

            UpMap.add up [new_set] map

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

  in

  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)]

  in

  let rec clean_disj disj =

    match disj with

    | [] -> []

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

    | _::_::_ -> (

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

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

    )

  in

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

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

      if !seal_debug then

        Format.eprintf

          "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 []

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

    let sw_init = process sw_init in

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

    let sw_sys = process sw_sys in

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

    let init_out = process init_out in

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

    let update_out = process update_out in

    sw_init , sw_sys, init_out, update_out

let seal_debug = ref false

type 'boolexpr guard = 'boolexpr list           

type ('guard, 'elem)  guarded_expr = 'guard * 'elem

type element = IsInit | Expr of expr

type elem_boolexpr = element * bool

type elem_guarded_expr = (elem_boolexpr guard, element) guarded_expr

type 'ge mdef_t = 'ge list 

               (*          

type mdef_t = guarded_expr list

                *)

let pp_elem fmt e =

  match e with

  | IsInit -> Format.fprintf fmt "init"

  | Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e 

let pp_guard_list pp_elem fmt gl =

  (fprintf_list ~sep:";@ "

     (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl

let pp_guard_expr pp_elem  fmt (gl,e) =

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

    (pp_guard_list pp_elem) gl

    pp_elem e

let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel

let deelem e =  match e with

    Expr e -> e

  | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *)

let is_eq_elem elem elem' =

  match elem, elem' with

  | IsInit, IsInit -> true

  | Expr e, Expr e' -> e = e' (*

     Corelang.is_eq_expr e e' *)

  | _ -> false

let select_elem elem (gelem, _) =

  is_eq_elem elem gelem

let pp_gl pp_expr =

  fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e)

let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) 

let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up 

let pp_sys fmt sw = List.iter (fun (gl,up) ->

                        match gl with

                        | None ->

                           pp_up fmt up

                        | Some gl ->

                           Format.fprintf fmt "[@[%a@]] -> (%a)@ "

                             Printers.pp_expr gl pp_up up) sw

module UpMap =

  struct

    include Map.Make (

                struct

                  type t = (ident * expr) list

                  let compare l1 l2 =

                    let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in

                    compare (proj l1) (proj l2) 

                end)

    let pp = pp_up 

  end

module Guards = struct

  include Set.Make (

              struct

                type t = (expr * bool) 

                let compare l1 l2 =

                  let proj (e,b) = e.expr_tag, b in

                  compare (proj l1) (proj l2) 

              end)

  let pp_short fmt s = pp_gl_short fmt (elements s)

  let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)

end

    let options =

      [

        "-export", Arg.String set_export, "seal export option (lustre, matlab)";

        "-debug", Arg.Set seal_debug, "seal debug"

      ]