ctl/ast_ctl.ml

   1
   2 (* ---------------------------------------------------------------------- *)
   3 (* Types                                                                  *)
   4 (* ---------------------------------------------------------------------- *)
   5
   6 type strict = STRICT | NONSTRICT
   7
   8 type keep_binding = bool (* true = put in witness tree *)
   9
  10 (* CTL parameterised on basic predicates and metavar's*)
  11 type ('pred,'mvar,'anno) generic_ctl =
  12   | False
  13   | True
  14   | Pred of 'pred
  15   | Not of (('pred,'mvar,'anno) generic_ctl)
  16   | Exists of keep_binding * 'mvar * (('pred,'mvar,'anno) generic_ctl)
  17   | And of strict * (('pred,'mvar,'anno) generic_ctl) *
  18       (('pred,'mvar,'anno) generic_ctl)
  19   | AndAny of direction * strict * (('pred,'mvar,'anno) generic_ctl) *
  20       (('pred,'mvar,'anno) generic_ctl)
  21   | HackForStmt of direction * strict * (('pred,'mvar,'anno) generic_ctl) *
  22       (('pred,'mvar,'anno) generic_ctl)
  23   | Or  of (('pred,'mvar,'anno) generic_ctl) *
  24       (('pred,'mvar,'anno) generic_ctl)
  25   | Implies of (('pred,'mvar,'anno) generic_ctl) *
  26       (('pred,'mvar,'anno) generic_ctl)
  27   | AF of direction * strict * (('pred,'mvar,'anno) generic_ctl)
  28   | AX of direction * strict * (('pred,'mvar,'anno) generic_ctl)
  29   | AG of direction * strict * (('pred,'mvar,'anno) generic_ctl)
  30   | AW of direction * strict *
  31         (* versions with exists v *)
  32         (('pred,'mvar,'anno) generic_ctl) * (('pred,'mvar,'anno) generic_ctl)
  33   | AU of direction * strict *
  34         (* versions with exists v *)
  35         (('pred,'mvar,'anno) generic_ctl) * (('pred,'mvar,'anno) generic_ctl)
  36   | EF of direction * (('pred,'mvar,'anno) generic_ctl)
  37   | EX of direction * (('pred,'mvar,'anno) generic_ctl)
  38   | EG of direction * (('pred,'mvar,'anno) generic_ctl)
  39   | EU of direction * (('pred,'mvar,'anno) generic_ctl) *
  40       (('pred,'mvar,'anno) generic_ctl)
  41   | Let of string *
  42       (('pred,'mvar,'anno) generic_ctl) *
  43       (('pred,'mvar,'anno) generic_ctl)
  44   | LetR of direction * string * (* evals phi1 wrt reachable states *)
  45       (('pred,'mvar,'anno) generic_ctl) *
  46       (('pred,'mvar,'anno) generic_ctl)
  47   | Ref of string
  48   | SeqOr of (('pred,'mvar,'anno) generic_ctl) *
  49       (('pred,'mvar,'anno) generic_ctl)
  50   | Uncheck of (('pred,'mvar,'anno) generic_ctl)
  51   | InnerAnd of (('pred,'mvar,'anno) generic_ctl)
  52   | XX of (('pred,'mvar,'anno) generic_ctl) (* fake, used in asttoctl *)
  53
  54 and direction = FORWARD (* the normal way *) | BACKWARD (* toward the start *)
  55
  56 let unwrap (ctl,_) = ctl
  57 let rewrap (_,model) ctl = (ctl,model)
  58 let get_line (_,l) = l
  59
  60
  61 (* NOTE: No explicit representation of the bottom subst., i.e., FALSE *)
  62 type ('mvar,'value) generic_subst =
  63   | Subst of 'mvar * 'value
  64   | NegSubst of 'mvar * 'value
  65 type ('mvar,'value) generic_substitution = ('mvar,'value) generic_subst list
  66
  67 type ('state,'subst,'anno) generic_witnesstree =
  68     Wit of
  69       'state * 'subst * 'anno * ('state,'subst,'anno) generic_witnesstree list
  70   | NegWit of ('state,'subst,'anno) generic_witnesstree
  71
  72 (* ---------------------------------------------------------------------- *)
  73
  74 type 'a modif = Modif of 'a | UnModif of 'a | Control
  75
  76 (* ---------------------------------------------------------------------- *)