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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
(** {1 Signature} *)
type t = (Type.t * bool) ID.Map.t
(** A signature maps symbols to their sort *)
let empty = ID.Map.empty
let is_empty = ID.Map.is_empty
let singleton = ID.Map.singleton
let mem signature s = ID.Map.mem s signature
let find_exn signature s =
let (t, _) = ID.Map.find s signature in t
let find signature s =
try Some (find_exn signature s)
with Not_found -> None
exception AlreadyDeclared of ID.t * Type.t * Type.t
let () = Printexc.register_printer
(function
| AlreadyDeclared (id, old, new_) ->
Some (
CCFormat.sprintf
"@[<2>symbol %a@ is already declared with type @[%a@],@ \
which is not compatible with @[%a@]@]"
ID.pp id Type.pp old Type.pp new_ )
| _ -> None)
let declare signature id ty =
try
let ty' = find_exn signature id in
if not (Type.equal ty ty') then raise (AlreadyDeclared (id, ty', ty))
else signature
with Not_found ->
if not (InnerTerm.DB.closed (ty : Type.t :> InnerTerm.t))
then raise (Invalid_argument "Signature.declare: non-closed type");
ID.Map.add id (ty,false) signature
let cardinal = ID.Map.cardinal
let arity signature s =
let ty = find_exn signature s in
match Type.arity ty with
| Type.NoArity ->
failwith (CCFormat.sprintf "symbol %a has ill-formed type %a" ID.pp s Type.TPTP.pp ty)
| Type.Arity (a,b) -> a, b
let is_ground signature =
ID.Map.for_all (fun _ (ty, _) -> Type.is_ground ty) signature
let merge s1 s2 =
ID.Map.merge
(fun s t1 t2 -> match t1, t2 with
| None, None -> assert false
| Some (ty1, c1), Some (ty2, c2) ->
if Type.equal ty1 ty2
then Some (ty1, c1 && c2)
else raise (AlreadyDeclared (s, ty1, ty2))
| Some (s1,c1), None -> Some (s1,c1)
| None, Some (s2,c2) -> Some (s2,c2))
s1 s2
let diff s1 s2 =
ID.Map.merge
(fun _ ty1 ty2 -> match ty1, ty2 with
| Some ty1, None -> Some ty1
| Some _, Some _
| None, Some _
| None, None -> None)
s1 s2
let well_founded s =
ID.Map.exists
(fun _ (ty,_) -> match Type.arity ty with
| Type.Arity (_, 0) -> true
| _ -> false)
s
let sym_in_conj s signature =
snd (ID.Map.get_or s signature ~default:(Type.int, false))
let set_sym_in_conj s signature =
let t = find_exn signature s in
ID.Map.add s (t, true) signature
module Seq = struct
let symbols s =
ID.Map.to_seq s |> Iter.map fst
let types s =
ID.Map.to_seq s |> Iter.map snd |> Iter.map fst
let to_seq = ID.Map.to_seq
let add_seq = ID.Map.add_seq
let of_seq = ID.Map.of_seq
end
let to_set s = Seq.symbols s |> ID.Set.of_seq
let to_list = ID.Map.to_list
let add_list = ID.Map.add_list
let of_list = ID.Map.of_list
let iter s f =
ID.Map.iter f s
let fold s acc f =
ID.Map.fold (fun s (ty,c) acc -> f acc s (ty,c)) s acc
let is_bool signature s =
let rec is_bool ty = match Type.view ty with
| Type.Builtin Type.Prop -> true
| Type.Fun (_, ret) -> is_bool ret
| Type.Forall ty' -> is_bool ty'
| _ -> false
in
is_bool (find_exn signature s)
let is_not_bool signature s =
not (is_bool signature s)
(** {2 IO} *)
let pp out s =
let pp_pair out (s,(ty, c)) =
Format.fprintf out "@[<hov2>%a:@ %a %B@]" ID.pp s Type.pp ty c
in
Format.fprintf out "{@[<hv>";
Util.pp_seq ~sep:", " pp_pair out (Seq.to_seq s);
Format.fprintf out "@]}";
()
let to_string = CCFormat.to_string pp