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

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

Authors

Maintainers

D

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

Sources

electrod-0.5.tbz

sha256=4f84384e51d9145d8c3af99b10512d2a872cc80d08e374deff50f1253bd75dd4

sha512=d7116b82e5879d91bc9e80aef1cecf46a7f5fa967b5881dfc29d30a5da0c71b802f8901dbc99f861534e020f3af254ef19b507088410f5dabcb753c430d2bb82

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

Source file `Relation.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
(*******************************************************************************
 * 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

type t =
  | Const of {name : Name.t; arity : int; scope : Scope.t}
  | Var of {name : Name.t; arity : int; scope : Scope.t; fby : Scope.t option}

let const name arity scope = Const {name; arity; scope}

let var name arity scope fby = Var {name; arity; scope; fby}

let equal rel1 rel2 =
  match (rel1, rel2) with
  | Const c1, Const c2 ->
      Name.equal c1.name c2.name
      && c1.arity = c2.arity
      && Scope.equal c1.scope c2.scope
  | Var c1, Var c2 ->
      Name.equal c1.name c2.name
      && c1.arity = c2.arity
      && Scope.equal c1.scope c2.scope
      && Option.equal Scope.equal c1.fby c2.fby
  | Const _, Var _ | Var _, Const _ ->
      false


let arity = function Const {arity; _} | Var {arity; _} -> arity

let name = function Const {name; _} | Var {name; _} -> name

let is_set rel = arity rel = 1

let is_nary rel = arity rel > 1

let is_const = function Const _ -> true | Var _ -> false

let is_var = function Const _ -> false | Var _ -> true

let scope = function Const {scope; _} | Var {scope; _} -> scope

let pp ?(print_name = true) out rel =
  let open! Fmtc in
  (* shadows const *)
  let pp_name =
    if print_name then sp **> colon **> nbsp **> Name.pp else nop
  in
  let pp_def const_or_var name scope fby arity =
    pp_name out name;
    (styled `Bold @@ string) out const_or_var;
    Format.pp_open_hbox out ();
    string out "«";
    int out arity;
    (sp **> string) out "»";
    Format.pp_open_box out 2;
    (box2 @@ Scope.pp) out scope;
    option
      ( (styled `Bold @@ (sp **< const string "then"))
      **< sp
      **< (box2 @@ Scope.pp) )
      out
      fby;
    Format.pp_close_box out ();
    Format.pp_close_box out ()
  in
  match rel with
  | Const {name; scope; arity} ->
      pp_def "const" name scope None arity
  | Var {name; scope; fby; arity} ->
      pp_def "var" name scope fby arity


let must = function Const {scope; _} | Var {scope; _} -> Scope.must scope

let may = function Const {scope; _} | Var {scope; _} -> Scope.may scope

let sup = function Const {scope; _} | Var {scope; _} -> Scope.sup scope

let rename atom_renaming name_renaming rel =
  match rel with
  | Const const ->
      Const
        { const with
          name = List.assoc ~eq:Name.equal const.name name_renaming
        ; scope = Scope.rename atom_renaming const.scope }
  | Var var ->
      Var
        { var with
          name = List.assoc ~eq:Name.equal var.name name_renaming
        ; scope = Scope.rename atom_renaming var.scope
        ; fby = Option.map (Scope.rename atom_renaming) var.fby }


let to_string ?(print_name = true) rel = Fmtc.to_to_string (pp ~print_name) rel