Source file `Scope.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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
(*******************************************************************************
 * electrod - a model finder for relational first-order linear temporal logic
 * 
 * Copyright (C) 2016-2020 ONERA
 * Authors: Julien Brunel (ONERA), David Chemouil (ONERA)
 * 
 * This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/.
 * 
 * SPDX-License-Identifier: MPL-2.0
 * License-Filename: LICENSE.md
 ******************************************************************************)

open Containers
module TS = Tuple_set

type relation =
  | Plain_relation of TS.t * TS.t
  | Partial_function of int * TS.t
  | Total_function of int * TS.t

type t =
  | Exact of TS.t
  | Inexact of relation

let equal sc1 sc2 =
  match (sc1, sc2) with
  | Exact ts1, Exact ts2 ->
      TS.equal ts1 ts2
  | Exact _, Inexact _ | Inexact _, Exact _ ->
      false
  | Inexact r1, Inexact r2 ->
    ( match (r1, r2) with
    | Plain_relation (r11, r12), Plain_relation (r21, r22) ->
        TS.equal r11 r21 && TS.equal r12 r22
    | Partial_function (dom_ar1, sup1), Partial_function (dom_ar2, sup2)
    | Total_function (dom_ar1, sup1), Total_function (dom_ar2, sup2) ->
        dom_ar1 = dom_ar2 && TS.equal sup1 sup2
    | Plain_relation _, (Partial_function _ | Total_function _)
    | Partial_function _, (Plain_relation _ | Total_function _)
    | Total_function _, (Plain_relation _ | Partial_function _) ->
        false )


let exact bound = Exact bound

let plain_relation inf sup =
  assert (TS.(inferred_arity inf = inferred_arity sup || TS.is_empty inf));
  assert (TS.(size sup >= size inf));
  Plain_relation (inf, sup)


let partial_function dom_arity sup =
  assert (dom_arity >= 0);
  assert (dom_arity < TS.inferred_arity sup);
  Partial_function (dom_arity, sup)


let total_function dom_arity sup =
  assert (dom_arity >= 0);
  assert (dom_arity < TS.inferred_arity sup);
  Total_function (dom_arity, sup)


let inexact rel = Inexact rel

let is_partial = function
  | Inexact (Partial_function _) ->
      true
  | Inexact (Total_function _ | Plain_relation _) | Exact _ ->
      false


let inferred_arity = function
  | Exact b
  | Inexact
      (Plain_relation (_, b) | Partial_function (_, b) | Total_function (_, b))
    ->
      TS.inferred_arity b


let included_in tupleset = function
  | Exact exact ->
      TS.subset tupleset exact
  | Inexact (Plain_relation (inf, sup)) ->
      TS.subset inf tupleset && TS.subset tupleset sup
  | Inexact (Partial_function (_, sup) | Total_function (_, sup)) ->
      TS.subset tupleset sup


let inf = function
  | Exact ts | Inexact (Plain_relation (ts, _)) ->
      ts
  | Inexact (Partial_function _ | Total_function _) ->
      TS.empty


let sup = function
  | Exact ts | Inexact (Plain_relation (_, ts)) ->
      ts
  | Inexact (Partial_function (_, sup) | Total_function (_, sup)) ->
      sup


let must = inf

let may_aux sc =
  assert (TS.subset (inf sc) (sup sc));
  match sc with
  | Exact _ ->
      TS.empty
  | Inexact (Plain_relation (inf, sup)) ->
      TS.diff sup inf
  | Inexact (Partial_function (_, sup) | Total_function (_, sup)) ->
      sup


let may = CCCache.(with_cache (lru ~eq:equal 253) may_aux)

let pp out = function
  | Exact bound ->
      TS.pp out bound
  | Inexact (Plain_relation (inf, sup)) ->
      Fmtc.(box @@ pair ~sep:sp (box2 TS.pp) (box2 TS.pp)) out (inf, sup)
  | Inexact (Partial_function (dom_ar, sup)) ->
      Fmtc.(box @@ triple string int (box2 TS.pp)) out ("lone {}", dom_ar, sup)
  | Inexact (Total_function (dom_ar, sup)) ->
      Fmtc.(box @@ triple string int (box2 TS.pp)) out ("one {}", dom_ar, sup)


let rename atom_renaming = function
  | Exact bound ->
      Exact (TS.rename atom_renaming bound)
  | Inexact (Plain_relation (inf, sup)) ->
      Inexact
        (Plain_relation
           (TS.rename atom_renaming inf, TS.rename atom_renaming sup))
  | Inexact (Partial_function (dom_ar, sup)) ->
      Inexact (Partial_function (dom_ar, TS.rename atom_renaming sup))
  | Inexact (Total_function (dom_ar, sup)) ->
      Inexact (Total_function (dom_ar, TS.rename atom_renaming sup))


module P = Intf.Print.Mixin (struct
  type nonrec t = t

  let pp = pp
end)

include P