matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml

   1 let step k ok outs ins =
   2   if ok then k ok outs ins else
   3   match ins with
   4   | "rtc_ist" :: tl -> k true ("rtc_ist" :: outs) tl
   5   | "test" :: "for" :: "t-transition" :: "counter" :: tl -> k true ("rtc_ist" :: outs) tl
   6   | "rtc_ism" :: tl -> k true ("rtc_ism" :: outs) tl
   7   | "test" :: "for" :: "constrained" :: "rt-transition" :: "counter" :: tl -> k true ("rtc_ism" :: outs) tl
   8   | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl
   9   | "shift" :: tl -> k true ("rtc_shift" :: outs) tl
  10   | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl
  11   | "max" :: tl -> k true ("rtc_max" :: outs) tl
  12   | _ -> k ok outs ins
  13
  14 let main =
  15   RecommPcsAnd.register_b step