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

   1 module T = RecommTypes
   2 module R = RecommPcsAnd
   3
   4 let step k st outs ins =
   5   if st <> T.OO then k st outs ins else
   6   match ins with
   7   | "ylt" :: tl -> k T.OK ("ylt" :: outs) tl
   8   | "yle" :: tl -> k T.OK ("yle" :: outs) tl
   9   | "ylminus" :: tl -> k T.OK ("ylminus" :: outs) tl
  10   | "yminus" :: tl -> k T.OK ("ylminus" :: outs) tl
  11   | "yplus" :: tl -> k T.OK ("yplus" :: outs) tl
  12   | "ypred" :: tl -> k T.OK ("ypred" :: outs) tl
  13   | "ysucc" :: tl -> k T.OK ("ysucc" :: outs) tl
  14   | "nlt" :: tl -> k T.OK ("nlt" :: outs) tl
  15   | "nle" :: tl -> k T.OK ("nle" :: outs) tl
  16   | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
  17   | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
  18   | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
  19   | "nrplus" :: tl -> k T.OK ("nrplus" :: outs) tl
  20   | "rplus" :: tl -> k T.OK ("nrplus" :: outs) tl
  21   | "npred" :: tl -> k T.OK ("npred" :: outs) tl
  22   | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
  23   | "npsucc" :: tl -> k T.OK ("npsucc" :: outs) tl
  24   | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
  25   | "niter" :: tl -> k T.OK ("niter" :: outs) tl
  26   | "plt" :: tl -> k T.OK ("plt" :: outs) tl
  27   | "ple" :: tl -> k T.OK ("ple" :: outs) tl
  28   | "pplus" :: tl -> k T.OK ("pplus" :: outs) tl
  29   | "ppred" :: tl -> k T.OK ("ppred" :: outs) tl
  30   | "psucc" :: tl -> k T.OK ("psucc" :: outs) tl
  31   | _ -> k T.OO outs ins
  32
  33 let main =
  34   R.register_b step