package ocaml-logicalform

  1. Overview
  2. Docs

Source file Literal.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
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
open Base

module type I =
  sig
    open Properties

    module Id : Index.I

    type nonrec t = [ `True
                    | `False
                    | `Pos of Id.T.t
                    | `Neg of Id.T.t
                    | `L of Id.t ]
                    [@@deriving sexp]

    include Negatable with type t := t

    include Base.Stringable.S with type t := t

    include PrettyPrint.I with type t := t

    include NeedsValidation with type t := t

    include Executable with type t := t
  end

module Make (Id : Index.I) : I with module Id = Id =
  struct
    open PrettyPrint

    module Id = Id

    type nonrec t = [ `True
                    | `False
                    | `Pos of Id.T.t
                    | `Neg of Id.T.t
                    | `L of Id.t ]
                    [@@deriving sexp]

    let validate (lit : t) : t =
      match lit with
      | `Pos i -> `L (Id.id i)
      | `Neg i -> `L (Id.not_ (Id.id i))
      | _ -> lit

    let of_string (str : string) : t =
      let ( === ) = String.equal
      in if str === Style.Infix.default.true_string then `True
         else if str === Style.Infix.default.false_string then `False
         else `L (Id.of_string str)

    let to_string (lit : t) : string =
      match lit with
      | `True -> Style.Infix.default.true_string
      | `False -> Style.Infix.default.false_string
      | `Pos i -> Id.T.to_string i
      | `Neg i -> Id.T.to_string (Id.T.not_ i)
      | `L id -> Id.to_string id

    let to_pretty_string ?(style = Style.Infix.default) (lit : t) : string =
      let sfmt = Printf.sprintf
      in match lit with
         | `True -> style.true_string
         | `False -> style.false_string
         | `Pos i -> sfmt "%s%d" style.var_prefix (Id.T.to_int_exn i)
         | `Neg i
           -> sfmt "%s%s%d" style._not_ style.var_prefix (Id.T.to_int_exn i)
         | `L (Valid (sgn, id))
           -> let i = Id.T.to_int_exn id
              in match sgn with
                 | Pos -> sfmt "%s%d" style.var_prefix i
                 | Neg -> sfmt "%s%s%d" style._not_ style.var_prefix i

    let of_pretty_sexp ?(style = Style.Prefix.default) (sexp_lit : Sexp.t) : t =
      let open String
      in let open Exceptions
      in let plen = length style.var_prefix
      in match sexp_lit with
         | Atom a
           -> if equal a style.true_string then `True
              else if equal a style.false_string then `False
              else if equal (subo a ~len:plen) style.var_prefix
                   then `L (Id.id (Id.T.of_int_exn
                              (Int.of_string (subo a ~pos:plen))))
                   else raise (invalid_sexp_exception ~ctx:"literal" sexp_lit)
         | List [ Atom neg ; Atom a ]
           -> if equal neg style.not_
              then if equal (subo a ~len:plen) style.var_prefix
                   then `L (Id.not_ (Id.id (Id.T.of_int_exn
                              (Int.of_string (subo a ~pos:plen)))))
                   else raise (invalid_sexp_exception ~ctx:"literal" (Atom a))
              else raise (invalid_sexp_exception ~ctx:"literal" sexp_lit)
         | _ -> raise (invalid_sexp_exception ~ctx:"literal" sexp_lit)

    let to_pretty_sexp ?(style = Style.Prefix.default) (lit : t) : Sexp.t =
      let sfmt = Printf.sprintf
      in match lit with
         | `True -> Atom style.true_string
         | `False -> Atom style.false_string
         | `Pos i -> Atom (sfmt "%s%d" style.var_prefix (Id.T.to_int_exn i))
         | `Neg i
           -> List [ Atom style.not_
                   ; Atom (sfmt "%s%d" style.var_prefix (Id.T.to_int_exn i)) ]
         | `L (Valid (sgn, id))
           -> let i = Id.T.to_int_exn id
              in match sgn with
                 | Pos -> Atom (sfmt "%s%d" style.var_prefix i)
                 | Neg -> List [ Atom style.not_
                               ; Atom (sfmt "%s%d" style.var_prefix i) ]

    let not_ (lit : t) : t =
      match lit with
      | `True -> `False
      | `False -> `True
      | `Pos i
      | `Neg i -> `L (Id.id (Id.T.not_ i))
      | `L id -> `L (Id.not_ id)

    let eval (lit : t) (bools : bool array) : bool option =
      match lit with
      | `True -> Some true
      | `False -> Some false
      | `Pos i -> (try Some bools.((Id.T.to_int_exn i) - 1) with _ -> None)
      | `Neg i -> (try Some (not bools.((Id.T.to_int_exn i) - 1)) with _ -> None)
      | `L (Valid (sgn, id))
         -> let i = (Id.T.to_int_exn id) - 1
            in match sgn with Pos -> (try Some bools.(i) with _ -> None)
                            | Neg -> (try Some (not bools.(i)) with _ -> None)
  end
OCaml

Innovation. Community. Security.