matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundRelocation.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   | "pr_sor" :: tl -> k T.OK ("pr_sor" :: outs) tl
   8   | "sor" :: tl -> k T.OK ("pr_sor" :: outs) tl
   9   | "pr_sand" :: tl -> k T.OK ("pr_sand" :: outs) tl
  10   | "sand" :: tl -> k T.OK ("pr_sand" :: outs) tl
  11   | "pr_sdj" :: tl -> k T.OK ("pr_sdj" :: outs) tl
  12   | "sdj" :: tl -> k T.OK ("pr_sdj" :: outs) tl
  13   | "pr_sle" :: tl -> k T.OK ("pr_sle" :: outs) tl
  14   | "sle" :: tl -> k T.OK ("pr_sle" :: outs) tl
  15   | "inclusion" :: tl -> k T.OK ("pr_sle" :: outs) tl
  16   | "pr_coafter" :: tl -> k T.OK ("pr_coafter" :: outs) tl
  17   | "coafter" :: tl -> k T.OK ("pr_coafter" :: outs) tl
  18   | "pr_after" :: tl -> k T.OK ("pr_after" :: outs) tl
  19   | "after" :: tl -> k T.OK ("pr_after" :: outs) tl
  20   | "pr_isd" :: tl -> k T.OK ("pr_isd" :: outs) tl
  21   | "isdiv" :: tl -> k T.OK ("pr_isd" :: outs) tl
  22   | "pr_ist" :: tl -> k T.OK ("pr_ist" :: outs) tl
  23   | "ist" :: tl -> k T.OK ("pr_ist" :: outs) tl
  24   | "istot" :: tl -> k T.OK ("pr_ist" :: outs) tl
  25   | "pr_isf" :: tl -> k T.OK ("pr_isf" :: outs) tl
  26   | "isf" :: tl -> k T.OK ("pr_isf" :: outs) tl
  27   | "isfin" :: tl -> k T.OK ("pr_isf" :: outs) tl
  28   | "test" :: "for" :: "finite" :: "colength" :: tl -> k T.OK ("pr_isf" :: outs) tl
  29   | "pr_fcla" :: tl -> k T.OK ("pr_fcla" :: outs) tl
  30   | "fcla" :: tl -> k T.OK ("pr_fcla" :: outs) tl
  31   | "finite" :: "colength" :: "assignment" :: tl -> k T.OK ("pr_fcla" :: outs) tl
  32   | "finite" :: "colength" :: tl -> k T.OK ("pr_fcla" :: outs) tl
  33   | "pr_isu" :: tl -> k T.OK ("pr_isu" :: outs) tl
  34   | "isuni" :: tl -> k T.OK ("pr_isu" :: outs) tl
  35   | "test" :: "for" :: "uniform" :: "relocations" :: tl -> k T.OK ("pr_isu" :: outs) tl
  36   | "pr_isi" :: tl -> k T.OK ("pr_isi" :: outs) tl
  37   | "isi" :: tl -> k T.OK ("pr_isi" :: outs) tl
  38   | "isid" :: tl -> k T.OK ("pr_isi" :: outs) tl
  39   | "test" :: "for" :: "identity" :: tl -> k T.OK ("pr_isi" :: outs) tl
  40   | "pr_nat" :: tl -> k T.OK ("pr_nat" :: outs) tl
  41   | "nat" :: tl -> k T.OK ("pr_nat" :: outs) tl
  42   | "pr_pat" :: tl -> k T.OK ("pr_pat" :: outs) tl
  43   | "pat" :: tl -> k T.OK ("pr_pat" :: outs) tl
  44   | "at" :: tl -> k T.OK ("pr_pat" :: outs) tl
  45   | "pr_basic" :: tl -> k T.OK ("pr_basic" :: outs) tl
  46   | "basic" :: "relocation" :: tl -> k T.OK ("pr_basic" :: outs) tl
  47   | "pr_uni" :: tl -> k T.OK ("pr_uni" :: outs) tl
  48   | "uni" :: tl -> k T.OK ("pr_uni" :: outs) tl
  49   | "uniform" :: "relocations" :: tl -> k T.OK ("pr_uni" :: outs) tl
  50   | "pr_id" :: tl -> k T.OK ("pr_id" :: outs) tl
  51   | "id" :: tl -> k T.OK ("pr_id" :: outs) tl
  52   | "pr_tls" :: tl -> k T.OK ("pr_tls" :: outs) tl
  53   | "tls" :: tl -> k T.OK ("pr_tls" :: outs) tl
  54   | "iterated" :: "tail" :: tl -> k T.OK ("pr_tls" :: outs) tl
  55   | "pr_nexts" :: tl -> k T.OK ("pr_nexts" :: outs) tl
  56   | "nexts" :: tl -> k T.OK ("pr_nexts" :: outs) tl
  57   | "iterated" :: "next" :: tl -> k T.OK ("pr_nexts" :: outs) tl
  58   | "pr_pushs" :: tl -> k T.OK ("pr_pushs" :: outs) tl
  59   | "pushs" :: tl -> k T.OK ("pr_pushs" :: outs) tl
  60   | "iterated" :: "push" :: tl -> k T.OK ("pr_pushs" :: outs) tl
  61   | "pr_tl" :: tl -> k T.OK ("pr_tl" :: outs) tl
  62   | "tl" :: tl -> k T.OK ("pr_tl" :: outs) tl
  63   | "tail" :: tl -> k T.OK ("pr_tl" :: outs) tl
  64   | "pr_eq" :: tl -> k T.OK ("pr_eq" :: outs) tl
  65   | _ -> k T.OO outs ins
  66
  67 let main =
  68   R.register_b step