Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

src/spec_common.ml
1 1
open Spec_types
2
open Utils
2 3

  
3 4
(* a small reduction engine *)
4 5
let is_true = function True -> true | _ -> false
......
73 74
    f
74 75

  
75 76
(* smart constructors *)
76
(* let mk_condition x l =
77
 *   if l = tag_true then Ternary (Val x, True, False)
78
 *   else if l = tag_false then Ternary (Val x, False, True)
79
 *   else Equal (Val x, Tag l) *)
80 77

  
81 78
let vals vs = List.map (fun v -> Val v) vs
82 79

  
83 80
let mk_pred_call pred = Predicate pred
84 81

  
85
(* let mk_clocked_on id =
86
 *   mk_pred_call (Clocked_on id) *)
87

  
88
let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
89
    outputs =
82
let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id
83
    inputs locals outputs =
90 84
  let tr =
91 85
    mk_pred_call
92 86
      (Transition
......
97 91
           vals locals,
98 92
           vals outputs,
99 93
           (match r with Some _ -> true | None -> false),
100
           mems ))
94
           mems,
95
           insts ))
101 96
  in
102 97
  match r, inst with
103 98
  | Some r, Some inst ->
......
113 108

  
114 109
let mk_conditional_tr v t f = Ternary (Val v, t, f)
115 110

  
116
let mk_branch_tr x hl =
117
  And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
111
let mk_branch_tr x =
112
  let open Lustre_types in
113
  function
114
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_true && h2 = tag_false ->
115
    Ternary (Var x, spec1, spec2)
116
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true ->
117
    Ternary (Var x, spec2, spec1)
118
  | hl ->
119
    And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
118 120

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

Also available in: Unified diff