[/] [trunk/] [src/] [maketest/] [clock_expression.sig] - Blame information for rev 19

Line No. Rev Author Line
1 4 tbourke 
(* $Id: clock_expression.sig 19 2007-11-27 00:20:37Z tbourke $ *)
2 
 
3 
signature CLOCK_EXPRESSION = sig
4 
 
5 
  exception NonClockTerm
6 
 
7 
  type symbol    = Atom.atom
8 
   and symbolset = AtomSet.set
9 
 
10 
  datatype clockrel = Lt | Leq | Eq | Geq | Gt
11 
 
12 
  datatype clockval = Simple  of int
13 
                    | Complex of Expression.expr
14 
 
15 
  datatype clockterm = NonClock of Expression.expr
16 
                     | CRel     of Expression.var * clockrel * clockval
17 
                     | CDiff    of Expression.var * Expression.var
18 
                                   * clockrel * clockval
19 
 
20 
  datatype t = Term of clockterm
21 
             | And  of t * t
22 
             | Or   of t * t
23 
 
24 
  val negate         : t -> t
25 
  val getFree        : t -> symbolset
26 
 
27 
  val fromExpr       : symbolset * Environment.env * Expression.expr
28 
                       -> t * (symbol * Expression.ty) list * symbolset
29 
                       (* raises NonClockTerm *)
30 
  (* usednames * environment * expression to convert
31 
   *    -> result * forall bindings * usednames' -- now in prenex form *)
32 
 
33 
  val toExpr         : t * (symbol * Expression.ty) list -> Expression.expr
34 
 
35 
  val rename         : {old: symbol, new: symbol} * t -> t
36 19 tbourke 
  val conflictExists : symbolset * symbolset * clockterm list list -> bool
37 4 tbourke 
 
38 
  val toDNF          : t -> clockterm list list
39 
  val fromDNF        : clockterm list list -> t
40 
  val andexpr        : t * t -> t
41 
 
42 
  val toString       : t -> string
43 
 
44 
end
45