CristalCaveGem » LustreC

open Lustre_types

open Utils

let report = Log.report ~plugin:"seal"

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 "@[<v 2>@[%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 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 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' -> 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 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_all_defs =

  (Utils.fprintf_list ~sep:",@ "

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

                             id

                             (pp_mdefs pp_elem) gel))              

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 Printers.pp_expr 

      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