Project

General

Profile

Revision 1d36cd07 src/lib/CoAlgFormula.ml

View differences:

src/lib/CoAlgFormula.ml
135 135
 *)
136 136
let sizeSortedFormula f = sizeFormula (snd f)
137 137

  
138
let depthFormula form = 
139
  let rec depth f =
140
    match f with
141
      | TRUE
142
      | FALSE
143
      | AP _ -> 0
144
      | NOT f1
145
      | AT (_, f1) -> (depth f1)
146
      | OR (f1, f2)
147
      | AND (f1, f2)
148
      | EQU (f1, f2)
149
      | IMP (f1, f2) -> (max (depth f1)(depth f2))
150
      | EX (_, f1)
151
      | AX (_, f1)
152
      | ENFORCES (_, f1)
153
      | ALLOWS (_, f1) -> succ ((depth f1))
154
      | MIN (_, _, f1)
155
      | MAX (_, _, f1)
156
      | ATLEASTPROB (_, f1)
157
      | LESSPROBFAIL (_, f1)
158
      | MORETHAN (_, _, f1)
159
      | MAXEXCEPT (_, _, f1) -> succ ((depth f1))
160
      | ID (f1) -> succ ((depth f1))
161
      | NORM(f1, f2)
162
      | NORMN(f1, f2) -> succ ((max (depth f1) (depth f2))) 
163
      | CONST _
164
      | CONSTN _ -> 1
165
      | CHC (f1, f2) -> succ ((max (depth f1) (depth f2))) 
166
      | FUS (_, f1) -> succ (depth f1)
167
      | MU (_, f1)
168
      | NU (_, f1) -> depth f1
169
      | VAR _ -> 0
170
  in
171
  depth form
172

  
138 173

  
139 174
(* think of func: (formula -> unit) -> formula -> unit as identity.
140 175
  iterate over all subformulae and collect side effects. *)

Also available in: Unified diff