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
(** Symbols and signature for unification rules.
This module provides a signature to be used to handle unification rules.
The signature is not attached to any real lambdapi file and is henceforth
qualified to be a "ghost" signature. *)
open Common
open Term
(** Symbol "≡". *)
let equiv : sym =
let id = Pos.none "≡" in
let s =
Sign.add_symbol Ghost.sign Public Defin Eager false id None
mk_Kind [] in
Sign.add_notation Ghost.sign s (Infix(Pratter.Neither, 2.0)); s
(** Symbol ";". *)
let cons : sym =
let id = Pos.none ";" in
let s =
Sign.add_symbol Ghost.sign Public Const Eager true id None
mk_Kind [] in
Sign.add_notation Ghost.sign s (Infix(Pratter.Right, 1.0)); s
(** [unpack eqs] transforms a term of the form
[cons (equiv t u) (cons (equiv v w) ...)]
into a list [[(t,u); (v,w); ...]]. *)
let rec unpack : term -> (term * term) list = fun eqs ->
match get_args eqs with
| (Symb(s), [v; w]) ->
if s == cons then
match get_args v with
| (Symb(e), [t; u]) when e == equiv -> (t, u) :: unpack w
| _ -> assert false
else if s == equiv then [(v, w)]
else assert false
| _ -> assert false
(** [mem s] is true iff [s] belongs to [sign]. *)
let mem : sym -> bool = fun s -> s == equiv || s == cons