12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849(*******************************************************************************
* 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
******************************************************************************)typet={sym:Symbol.t;loc:Location.toption}letcomparea1a2=Symbol.comparea1.syma2.symletequala1a2=Symbol.equala1.syma2.sym(* |> Fun.tap *)(* (fun res -> *)(* (Fmt.epr "Atom.equal %a %a = %B" *)(* Symbol.pp a1.sym *)(* Symbol.pp a2.sym *)(* res)) *)letatom?locs={sym=Symbol.makes;loc}letof_raw_identid=atom~loc:(Raw_ident.locationid)(Raw_ident.basenameid)lethashatom=Symbol.hashatom.sym(** Generic interface implementations *)letppout{sym;_}=Symbol.ppoutsymmoduleP=Intf.Print.Mixin(structtypenonrect=tletpp=ppend)includePletpp_listatoms=Fmtc.(braces_@@list~sep:sppp)atoms