package electrod

You can search for identifiers within the package.

in-package search v0.2.0

Formal analysis for the Electrod formal pivot language

Install

Dune Dependency

grayswandyr.github.io Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

Maintainers

D

David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-0.2.3.tbz

sha256=7371c45e28b84a1955d117ef2c798d545febb87c74f596b6efe24965e4b28f31

sha512=e579db68ac05e30b0985f7d90080a82697de18c12e818d48bd7029cea8844571423f08d5881accbf8a0cbeb7df7de9b5b95ff5fe813330a6c92448a0901cdfe7

doc/src/electrod.libelectrod/Scope.ml.html

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-2019 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