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-1.0.0.tbz

sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58

sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2

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

Source file `Parser_main.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
(*******************************************************************************
 * 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 P = Parser

(* To allow paragraphs to appear in any order, or even, for some, not to appear,
   the grammar says that a list of paragraphs is allowed. Then this list has to be
   checked to see whether it corresponds to a legit permutation (defining legit
   permutations inside the grammar would be cumbersome and less efficient) *)
let check_paragraphs file pars =
  let open List in
  let goal =
    let candidates =
      filter
        (function
          | Raw.ParGoal _ ->
              true
          | Raw.ParInst _ | Raw.ParSym _ | Raw.ParInv _ ->
              false)
        pars
    in
    if length candidates = 1
    then
      (* there must be one goal *)
      match candidates with [ Raw.ParGoal g ] -> g | _ -> assert false
    else
      Msg.Fatal.syntax_error_paragraphs (fun args ->
          args file "one goal must be declared exactly")
  in
  let invar =
    let candidates =
      filter
        (function
          | Raw.ParInv _ ->
              true
          | Raw.ParGoal _ | Raw.ParInst _ | Raw.ParSym _ ->
              false)
        pars
    in
    if length candidates <= 1
    then
      (* there may be one list of instances *)
      match candidates with
      | [] ->
          []
      | [ Raw.ParInv g ] ->
          g
      | _ ->
          assert false
    else
      Msg.Fatal.syntax_error_paragraphs (fun args ->
          args file "at most one invariant section may be declared")
  in
  let inst =
    let candidates =
      filter
        (function
          | Raw.ParInst _ ->
              true
          | Raw.ParGoal _ | Raw.ParSym _ | Raw.ParInv _ ->
              false)
        pars
    in
    if length candidates <= 1
    then
      (* there may be one list of instances *)
      match candidates with
      | [] ->
          []
      | [ Raw.ParInst g ] ->
          g
      | _ ->
          assert false
    else
      Msg.Fatal.syntax_error_paragraphs (fun args ->
          args file "at most one (partial) instance may be declared")
  in
  let sym =
    let candidates =
      filter
        (function
          | Raw.ParSym _ ->
              true
          | Raw.ParGoal _ | Raw.ParInst _ | Raw.ParInv _ ->
              false)
        pars
    in
    if length candidates <= 1
    then
      (* there may be one list of symmetries *)
      match candidates with
      | [] ->
          []
      | [ Raw.ParSym g ] ->
          g
      | _ ->
          assert false
    else
      Msg.Fatal.syntax_error_paragraphs (fun args ->
          args file "at most one list of symmetries may be declared")
  in
  (goal, invar, inst, sym)


let parse_file file =
  IO.with_in file
  @@ fun ic ->
  let lexbuf = Lexing.from_channel ic in
  try
    let raw_univ, raw_decls, raw_paragraphs =
      P.parse_problem (Scanner.main (Some file)) lexbuf
    in
    let raw_goal, raw_fact, raw_inst, raw_syms =
      check_paragraphs (Some file) raw_paragraphs
    in
    Raw.problem
      (Some file)
      raw_univ
      raw_decls
      raw_goal
      raw_fact
      raw_inst
      raw_syms
  with
  | P.Error ->
      Msg.Fatal.syntax @@ fun args -> args file lexbuf


let parse_string s =
  let lexbuf = Lexing.from_string s in
  let raw_univ, raw_decls, raw_paragraphs =
    P.parse_problem (Scanner.main None) lexbuf
  in
  let raw_goal, raw_fact, raw_inst, raw_syms =
    check_paragraphs None raw_paragraphs
  in
  Raw.problem None raw_univ raw_decls raw_goal raw_fact raw_inst raw_syms