Source file `OCanren.ml`

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
(* SPDX-License-Identifier: LGPL-2.1-or-later *)
(*
 * OCanren.
 * Copyright (C) 2015-2022
 * Dmitri Boulytchev, Dmitry Kosarev, Alexey Syomin, Evgeny Moiseenko
 * St.Petersburg State University, JetBrains Research
 *
 * This software is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Library General Public
 * License version 2, as published by the Free Software Foundation.
 *
 * This software is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 *
 * See the GNU Library General Public License version 2 for more details
 * (enclosed in the file COPYING).
 *)

include Logic
include Core

module Stream  = Stream
module Runconf = Runconf
module Timer   = Timer
module Env = Env

module Std =
  struct
    module Pair    = Pair
    module Option  = Option
    module Bool    = Bool
    module Nat     = Nat
    module List    = List

    let eqo x y t =
      conde [
        (x === y) &&& (t === Bool.truo);
        (x =/= y) &&& (t === Bool.falso);
      ]

    let neqo x y t =
      conde [
        (x =/= y) &&& (t === Bool.truo);
        (x === y) &&& (t === Bool.falso);
      ]

    let nat n = Nat.nat (Nat.of_int n)

    let (%)  = List.cons
    let (%<) = List.(%<)
    let (!<) = List.(!<)
    let nil  = List.nil

    let rec list f = function
    | []    -> nil ()
    | x::xs -> List.cons (f x) (list f xs)

    let rec nat_list = function
    | []    -> nil ()
    | x::xs -> nat x % nat_list xs

    let some = Option.some
    let none = Option.none
    let pair = Pair.pair


    let structural = Core.structural
    let debug_var = Core.debug_var
    let only_head = Core.only_head


  end
IFDEF STATS THEN
module Peep = Peep

let _ = Peep.unification_counter
END