blob: 5fc16c618af20d75ccd90bc6bfb9dae2211355a8 (
plain) (
blame)
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
|
(** Open terms and unification.
A pattern is a {!Term.t} that may contain logic variables. Goals,
rule heads, and rule bodies are made of patterns; solving a query
means finding substitutions that close them back into terms.
Unification here is the join mechanism of the whole language:
shared variables across conjoined propositions unify, and that is
what a join is. *)
type t =
| Var of string
| Integer of Z.t
| Rational of Q.t
| String of string
| Nil
| Record of t Label.Map.t
val of_term : Term.t -> t
(** Injects a closed term. Canonicity carries over unchanged. *)
val to_term : t -> Term.t option
(** Closes a pattern back into a term. [None] if any variable
remains, so [Some] is proof of groundness. *)
val is_ground : t -> bool
val vars : t -> string list
(** Free variables, each reported once. The solver reports solutions
for exactly these. *)
val cons : head:t -> tail:t -> t
(** One sequence cell over open terms, [{head: _ tail: _}]. The
loader elaborates [#( ... )] in rule heads and bodies with
this. *)
val equal : t -> t -> bool
(** Syntactic equality, variables by name. Used by the totality
checker to compare head and body arguments. *)
val strictly_contains : t -> sub:t -> bool
(** Whether [sub] occurs strictly inside the pattern, at depth one or
more. This is the structural decrease witness of the admission
checker: a recursive call is safe when its argument is strictly
contained in the head's. *)
val pp : Format.formatter -> t -> unit
(** Substitutions bind variables to patterns. They only grow;
unification never revokes a binding. *)
module Subst : sig
type pattern := t
type t
val empty : t
val walk : t -> pattern -> pattern
(** Follows variable bindings one level: the result is either a
non-variable or an unbound variable. The solver's view of "what
is this argument right now". *)
val resolve : t -> pattern -> pattern
(** Applies the substitution everywhere, recursively. Used to read
answers out and to test groundness of arguments. *)
val unify : t -> pattern -> pattern -> t option
(** Extends the substitution so both sides are equal, or reports
impossibility. Records unify only on identical label sets.
Runs an occurs check: Sol terms are finite, so a solution that
would need an infinite term is a failure, not a loop. *)
end
|
