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   | _           -> k ET.KO outs ins
  18
  19 let k_or k st outs ins =
  20   if st <> ET.OO then k st outs ins else
  21   !r_line (k_for k) st outs ins
  22
  23 let step k st outs ins =
  24   if st = ET.KO then k st outs ins else
  25   !d_line (k_or k) ET.OO outs ins
  26
  27 let register_d =
  28   ES.register d_line
  29
  30 let register_r =
  31   ES.register r_line
  32
  33 let main =
  34   EC.register_c step