CristalCaveGem » LustreC

open Spec_types

(* a small reduction engine *)

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

let is_false = function False -> true | _ -> false

let expr_eq : type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool

    =

 fun a b ->

  match a, b with

  | Var x, Var y ->

    x = y

  | Memory r1, Memory r2 ->

    r1 = r2

  | _ ->

    false

let rec red : type a. a formula_t -> a formula_t = function

  | Equal (a, b) when expr_eq a b ->

    True

  | And l -> (

    let l' =

      List.filter_map

        (fun a ->

          let a' = red a in

          if is_true a' then None else Some a')

        l

    in

    match l' with

    | [] ->

      True

    | [ a ] ->

      a

    | l' when List.exists is_false l' ->

      False

    | _ ->

      And l')

  | Or l -> (

    let l' =

      List.filter_map

        (fun a ->

          let a' = red a in

          if is_false a' then None else Some a')

        l

    in

    match l' with

    | [] ->

      assert false

    | [ a ] ->

      a

    | l' when List.exists is_true l' ->

      True

    | _ ->

      Or l')

  | Imply (a, b) ->

    let a' = red a in

    let b' = red b in

    if a' = b' || is_false a' || is_true b' then True

    else if is_true a' && is_false b' then False

    else Imply (a', b')

  | Exists (x, p) -> (

    let p' = red p in

    if is_true p' then True else match x with [] -> p' | x -> Exists (x, p'))

  | Forall (x, p) -> (

    let p' = red p in

    if is_true p' then True else match x with [] -> p' | x -> Forall (x, p'))

  | Ternary (x, a, b) ->

    let a' = red a in

    let b' = red b in

    Ternary (x, a', b')

  | f ->

    f

(* smart constructors *)

(* let mk_condition x l =

 *   if l = tag_true then Ternary (Val x, True, False)

 *   else if l = tag_false then Ternary (Val x, False, True)

 *   else Equal (Val x, Tag l) *)

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

let mk_pred_call pred = Predicate pred

(* let mk_clocked_on id =

 *   mk_pred_call (Clocked_on id) *)

let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals

    outputs =

  let tr =

    mk_pred_call

      (Transition

         ( id,

           inst,

           i,

           vals inputs,

           vals locals,

           vals outputs,

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

           mems ))

  in

  match r, inst with

  | Some r, Some inst ->

    ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)

  | _ ->

    tr

let mk_memory_pack ?i ?inst id = mk_pred_call (MemoryPack (id, inst, i))

let mk_state_variable_pack x = StateVarPack (StateVar x)

let mk_state_assign_tr x v = Equal (Memory (StateVar x), Val v)

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

let mk_branch_tr x hl =

  And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)

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