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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
(** Configuration for tactics based on first-order logic. *)
open Common open Error
open Core open Term
(** Builtin configuration for propositional logic. *)
type config =
{ symb_Prop: sym (** Type of propositions. *)
; symb_P : sym (** Encoding of propositions. *)
; symb_Set : sym (** Type of sets. *)
; symb_T : sym (** Encoding of types. *)
; symb_or : sym (** Disjunction(∨) symbol. *)
; symb_and : sym (** Conjunction(∧) symbol. *)
; symb_imp : sym (** Implication(⇒) symbol. *)
; symb_eqv : sym (** Equivalence(⇔) symbol. *)
; symb_bot : sym (** Bot(⊥) symbol. *)
; symb_top : sym (** Top(⊤) symbol. *)
; symb_not : sym (** Not(¬) symbol. *)
; symb_ex : sym (** Exists(∃) symbol. *)
; symb_all : sym (** Forall(∀) symbol. *) }
(** [get_config ss pos] build the configuration using [ss]. *)
let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos ->
let builtin = Builtin.get ss pos in
let symb_P = builtin "P" and symb_T = builtin "T" in
let symb_Prop =
match unfold Timed.(!(symb_P.sym_type)) with
| Prod(a,_) ->
begin
match unfold a with
| Symb s -> s
| _ ->
fatal pos "The type of %a is not of the form Prop → _ \
with Prop a symbol." Print.sym symb_P
end
| _ -> fatal pos "The type of %a is not a product" Print.sym symb_P
and symb_Set =
match unfold Timed.(!(symb_T.sym_type)) with
| Prod(a,_) ->
begin
match unfold a with
| Symb s -> s
| _ ->
fatal pos "The type of %a is not of the form Prop → _ \
with Prop a symbol." Print.sym symb_T
end
| _ -> fatal pos "The type of %a is not a product" Print.sym symb_T
in
{ symb_Prop
; symb_P
; symb_Set
; symb_T
; symb_or = builtin "or"
; symb_and = builtin "and"
; symb_imp = builtin "imp"
; symb_eqv = builtin "eqv"
; symb_bot = builtin "bot"
; symb_top = builtin "top"
; symb_not = builtin "not"
; symb_ex = builtin "ex"
; symb_all = builtin "all" }