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

   1 module T = RecommTypes
   2 module R = RecommPccFor
   3
   4 let step k st outs ins =
   5   if st <> T.OO then k st outs ins else
   6   match ins with
   7   | "UNIFORMITY" :: "CONDITION" :: tl -> k T.OK ("CONDITION" :: "UNIFORMITY" :: outs) tl
   8   | "UNIFORM" :: "ELEMENTS" :: tl -> k T.OK ("ELEMENTS" :: "UNIFORM" :: outs) tl
   9   | "TOTALITY" :: "CONDITION" :: tl -> k T.OK ("CONDITION" :: "TOTALITY" :: outs) tl
  10   | "RELATIONAL" :: "UNION" :: tl -> k T.OK ("UNION" :: "RELATIONAL" :: outs) tl
  11   | "RELATIONAL" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "RELATIONAL" :: outs) tl
  12   | "RELATIONAL" :: "INTERSECTION" :: tl -> k T.OK ("INTERSECTION" :: "RELATIONAL" :: outs) tl
  13   | "RELATIONAL" :: "COMPOSITION" :: tl -> k T.OK ("COMPOSITION" :: "RELATIONAL" :: outs) tl
  14   | "RELATIONAL" :: "CO-COMPOSITION" :: tl -> k T.OK ("CO-COMPOSITION" :: "RELATIONAL" :: outs) tl
  15   | "POSITIVE" :: "APPLICATION" :: tl -> k T.OK ("APPLICATION" :: "POSITIVE" :: outs) tl
  16   | "NON-NEGATIVE" :: "APPLICATION" :: tl -> k T.OK ("APPLICATION" :: "NON-NEGATIVE" :: outs) tl
  17   | "ITERATED" :: "NEXT" :: tl -> k T.OK ("NEXT" :: "ITERATED" :: outs) tl
  18   | "ITERATED" :: "PUSH" :: tl -> k T.OK ("PUSH" :: "ITERATED" :: outs) tl
  19   | "INCLUSION" :: tl -> k T.OK ("INCLUSION" :: outs) tl
  20   | "IDENTITY" :: "ELEMENT" :: tl -> k T.OK ("ELEMENT" :: "IDENTITY" :: outs) tl
  21   | "IDENTITY" :: "CONDITION" :: tl -> k T.OK ("CONDITION" :: "IDENTITY" :: outs) tl
  22   | "FINITE" :: "COLENGTH" :: "CONDITION" :: tl -> k T.OK ("CONDITION" :: "COLENGTH" :: "FINITE" :: outs) tl
  23   | "FINITE" :: "COLENGTH" :: "ASSIGNMENT" :: tl -> k T.OK ("ASSIGNMENT" :: "COLENGTH" :: "FINITE" :: outs) tl
  24   | "DIVERGENCE" :: "CONDITION" :: tl -> k T.OK ("CONDITION" :: "DIVERGENCE" :: outs) tl
  25   | "DISJOINTNESS" :: tl -> k T.OK ("DISJOINTNESS" :: outs) tl
  26   | "BASIC" :: "ELEMENTS" :: tl -> k T.OK ("ELEMENTS" :: "BASIC" :: outs) tl
  27   | _ -> k T.OO outs ins
  28
  29 let main =
  30   R.register_r step