aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/jprover/jlogic.mli
blob: a9079791100009ddb11c5d0e9316c2e97d51e21c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
(* The interface to manipulate [jterms], which is
   extracted and modified from Meta-Prl. *)

type rule =
   Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl
 | Allr | Alll| Exr | Exl | Fail | Falsel | Truer

module type JLogicSig =
  sig
    val is_all_term : Jterm.term -> bool
    val dest_all : Jterm.term -> string * Jterm.term * Jterm.term
    val is_exists_term : Jterm.term -> bool
    val dest_exists : Jterm.term -> string * Jterm.term * Jterm.term
    val is_and_term : Jterm.term -> bool
    val dest_and : Jterm.term -> Jterm.term * Jterm.term
    val is_or_term : Jterm.term -> bool
    val dest_or : Jterm.term -> Jterm.term * Jterm.term
    val is_implies_term : Jterm.term -> bool
    val dest_implies : Jterm.term -> Jterm.term * Jterm.term
    val is_not_term : Jterm.term -> bool
    val dest_not : Jterm.term -> Jterm.term
    type inf_step = rule * (string * Jterm.term) * (string * Jterm.term)
    type inference = inf_step list
    val empty_inf : inference
    val append_inf :
      inference -> (string * Jterm.term) -> (string * Jterm.term) -> rule -> inference
    val print_inf : inference -> unit
  end

module JLogic : JLogicSig

val show_loading : string -> unit

type my_Debug = {
  mutable debug_name : string;
  mutable debug_description : string;
  debug_value : bool;
} 
val create_debug : 'a -> bool ref
val ruletable : rule -> string