(* spi-calculus-like processes. Copyright (C) 2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan and INRIA Futurs projet SECSI. This file is part of ispi. ispi is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version. ispi is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with ispi; see the file COPYING. If not, write to the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA. *) open "process_h"; fun print_spi_term (f as |[put, ...]|) = let fun pterm (SPI_VAR x) = put x | pterm (SPI_APPL ("crypt", [t, u])) = (put "{"; pterm t; put "}"; pterm u) | pterm (SPI_APPL ("acrypt", [t, u])) = (put "["; pterm t; put "]"; pterm u) | pterm (SPI_APPL (f, l)) = (put f; put "("; let val delimr = ref "" in iterate (put (!delimr); delimr := ","; pterm t) | t in list l end end; put ")") in pterm end; fun mangle (f as |[put, ...]|) = |[ put = (fn s => iterate put (case c of "(" => "_of_" | ")" => "_end" | "{" => "_oc_" | "}" => "_cc_" | "[" => "_ob_" | "]" => "_cb_" | "," => "_and_" | "=" => "_eq_" | "_" => "__" | _ => c) | c in list explode s end) ]|;