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

   1 module EC = RecommCheck
   2 module ES = RecommStep
   3 module ET = RecommTypes
   4
   5 let d_line = ref ES.id
   6
   7 let r_line = ref ES.id
   8
   9 let k_exit k st out ins =
  10   if st <> ET.OK then k ET.KO out ins else
  11   k st out ins
  12
  13 let k_for k st outs ins =
  14   if st <> ET.OK then k ET.KO outs ins else
  15   match ins with
  16   | "FOR" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
  17   | "OF" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
  18   | _           -> k ET.KO outs ins
  19
  20 let k_or k st outs ins =
  21   if st <> ET.OO then k st outs ins else
  22   !r_line (k_for k) st outs ins
  23
  24 let step k st outs ins =
  25   if st = ET.KO then k st outs ins else
  26   !d_line (k_or k) ET.OO outs ins
  27
  28 let register_d =
  29   ES.register d_line
  30
  31 let register_r =
  32   ES.register r_line
  33
  34 let main =
  35   EC.register_c step