← Back to branch summary

~npalix/coccinelle/upstream

« back to all changes in this revision

Viewing changes to ctl/ast_ctl.ml

  • Committer: Nicolas Palix
  • Date: 2010-01-28 14:23:49 UTC
  • Revision ID: git-v1:70d17887795852eca805bfe27745b9810c0a39be
Remove trailing whitespace/tab

svn path=/coccinelle/; revision=8684

Show diffs side-by-side

added added

removed removed

Lines of Context:
ctl/ast_ctl.ml
8
8
type keep_binding = bool (* true = put in witness tree *)
9
9
 
10
10
(* CTL parameterised on basic predicates and metavar's*)
11
 
type ('pred,'mvar,'anno) generic_ctl = 
 
11
type ('pred,'mvar,'anno) generic_ctl =
12
12
  | False
13
13
  | True
14
14
  | Pred of 'pred
15
15
  | Not of (('pred,'mvar,'anno) generic_ctl)
16
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) * 
 
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
26
      (('pred,'mvar,'anno) generic_ctl)
27
27
  | AF of direction * strict * (('pred,'mvar,'anno) generic_ctl)
28
28
  | AX of direction * strict * (('pred,'mvar,'anno) generic_ctl)
36
36
  | EF of direction * (('pred,'mvar,'anno) generic_ctl)
37
37
  | EX of direction * (('pred,'mvar,'anno) generic_ctl)
38
38
  | EG of direction * (('pred,'mvar,'anno) generic_ctl)
39
 
  | EU of direction * (('pred,'mvar,'anno) generic_ctl) * 
 
39
  | EU of direction * (('pred,'mvar,'anno) generic_ctl) *
40
40
      (('pred,'mvar,'anno) generic_ctl)
41
 
  | Let of string * 
42
 
      (('pred,'mvar,'anno) generic_ctl) * 
 
41
  | Let of string *
 
42
      (('pred,'mvar,'anno) generic_ctl) *
43
43
      (('pred,'mvar,'anno) generic_ctl)
44
44
  | LetR of direction * string * (* evals phi1 wrt reachable states *)
45
 
      (('pred,'mvar,'anno) generic_ctl) * 
 
45
      (('pred,'mvar,'anno) generic_ctl) *
46
46
      (('pred,'mvar,'anno) generic_ctl)
47
47
  | Ref of string
48
 
  | SeqOr of (('pred,'mvar,'anno) generic_ctl) * 
 
48
  | SeqOr of (('pred,'mvar,'anno) generic_ctl) *
49
49
      (('pred,'mvar,'anno) generic_ctl)
50
50
  | Uncheck of (('pred,'mvar,'anno) generic_ctl)
51
51
  | InnerAnd of (('pred,'mvar,'anno) generic_ctl)
59
59
 
60
60
 
61
61
(* NOTE: No explicit representation of the bottom subst., i.e., FALSE *)
62
 
type ('mvar,'value) generic_subst = 
 
62
type ('mvar,'value) generic_subst =
63
63
  | Subst of 'mvar * 'value
64
64
  | NegSubst of 'mvar * 'value
65
65
type ('mvar,'value) generic_substitution = ('mvar,'value) generic_subst list