diff options
Diffstat (limited to 'contrib/jprover/jlogic.ml')
-rw-r--r-- | contrib/jprover/jlogic.ml | 106 |
1 files changed, 0 insertions, 106 deletions
diff --git a/contrib/jprover/jlogic.ml b/contrib/jprover/jlogic.ml deleted file mode 100644 index c074e93e..00000000 --- a/contrib/jprover/jlogic.ml +++ /dev/null @@ -1,106 +0,0 @@ -open Opname -open Jterm - -type rule = - | Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl - | Allr | Alll| Exr | Exl | Fail | Falsel | Truer - -let ruletable = function - | Fail -> "Fail" - | Ax -> "Ax" - | Negl -> "Negl" - | Negr -> "Negr" - | Andl -> "Andl" - | Andr -> "Andr" - | Orl -> "Orl" - | Orr -> "Orr" - | Orr1 -> "Orr1" - | Orr2 -> "Orr2" - | Impl -> "Impl" - | Impr -> "Impr" - | Exl -> "Exl" - | Exr -> "Exr" - | Alll -> "Alll" - | Allr -> "Allr" - | Falsel -> "Falsel" - | Truer -> "Truer" - -module type JLogicSig = -sig - (* understanding the input *) - val is_all_term : term -> bool - val dest_all : term -> string * term * term - val is_exists_term : term -> bool - val dest_exists : term -> string * term * term - val is_and_term : term -> bool - val dest_and : term -> term * term - val is_or_term : term -> bool - val dest_or : term -> term * term - val is_implies_term : term -> bool - val dest_implies : term -> term * term - val is_not_term : term -> bool - val dest_not : term -> term - - (* processing the output *) - type inf_step = rule * (string * term) * (string * term) - type inference = inf_step list -(* type inference *) - val empty_inf : inference - val append_inf : inference -> (string * term) -> (string * term) -> rule -> inference - val print_inf : inference -> unit -end;; - -(* Copy from [term_op_std.ml]: *) - - let rec print_address int_list = - match int_list with - | [] -> - Format.print_string "" - | hd::rest -> - begin - Format.print_int hd; - print_address rest - end - -module JLogic: JLogicSig = -struct - let is_all_term = Jterm.is_all_term - let dest_all = Jterm.dest_all - let is_exists_term = Jterm.is_exists_term - let dest_exists = Jterm.dest_exists - let is_and_term = Jterm.is_and_term - let dest_and = Jterm.dest_and - let is_or_term = Jterm.is_or_term - let dest_or = Jterm.dest_or - let is_implies_term = Jterm.is_implies_term - let dest_implies = Jterm.dest_implies - let is_not_term = Jterm.is_not_term - let dest_not = Jterm.dest_not - - type inf_step = rule * (string * term) * (string * term) - type inference = inf_step list - - let empty_inf = [] - let append_inf inf t1 t2 rule = - (rule, t1, t2)::inf - - let rec print_inf inf = - match inf with - | [] -> print_string "."; Format.print_flush () - | (rule, (n1,t1), (n2,t2))::d -> - print_string (ruletable rule); - print_string (":("^n1^":"); - print_term stdout t1; - print_string (","^n2^":"); - print_term stdout t2; - print_string ")\n"; - print_inf d -end;; - -let show_loading s = print_string s -type my_Debug = { mutable debug_name: string; - mutable debug_description: string; - debug_value: bool - } - -let create_debug x = ref false |