Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / EAFormula.mli @ e3cf4ca2

History | View | Annotate | Download (1.24 KB)

1
(* This module implements formulas with global box and global diamond (A, E) *)
2

    
3
module CA = CoAlgFormula
4

    
5
type nomTbl = string -> CoAlgFormula.sort option
6

    
7
type eaformula =
8
  | TRUE
9
  | FALSE
10
  | AP of string (*named atom*)
11
  | NOT of eaformula
12
  | OR of eaformula * eaformula
13
  | AND of eaformula * eaformula
14
  | EQU of eaformula * eaformula
15
  | IMP of eaformula * eaformula
16
  | EX of string * eaformula (* exists, diamond of K *)
17
  | AX of string * eaformula (* forall, box of K *)
18
  | ID of eaformula (* modality of the identity functor *)
19
  | E_AP of string (* global diamond *)
20
  | A of eaformula (* global box *)
21
  | MU of string * eaformula
22
  | NU of string * eaformula
23
  | AF of eaformula
24
  | EF of eaformula
25
  | AG of eaformula
26
  | EG of eaformula
27

    
28

    
29
val exportFormula : eaformula -> string
30
val rename : CoAlgFormula.formula -> string Map.Make(String).t ref -> string list ref -> CoAlgFormula.formula
31
val coalgtoea : CoAlgFormula.formula -> eaformula
32
val formula2 : CoAlgFormula.formula -> string list -> (string -> int option) -> CoAlgReasoner.sortTable -> CoAlgFormula.formula
33
val formula3 : string list -> eaformula
34
val nom2EA : CoAlgFormula.formula -> (string -> int option) -> CoAlgReasoner.sortTable -> eaformula
35

    
36
(* vim: set et sw=2 sts=2 ts=8 : *)