(* spi-calculus-like processes, headers.
   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.
*)

datatype spi_term = SPI_VAR of string
       | SPI_APPL of string * spi_term list
	 ;

type spi_pattern = spi_term;

datatype spi_fact = SPI_EQ of spi_term * spi_term
       | SPI_DIFF of spi_term * spi_term
	 ;

datatype spi_process = SPI_ZERO
       | SPI_CALL of string * spi_term list
	 (* f (e1, ..., en) *)
       | SPI_BANG of string * located_process (* name of var holding pid, process *)
	 (* ![X] P *)
       | SPI_NEW of string * located_process (* name of fresh var, process *)
	 (* new X; P *)
       | SPI_IF of spi_term * spi_term * located_process * located_process
	 (* if e=e' then P else Q *)
       | SPI_DECRYPT_SYM of spi_term * string * spi_term * located_process * located_process
	 (* case e1 of {X}_e2 => P else Q *)
       | SPI_DECRYPT_ASYM of spi_term * string * spi_term * located_process * located_process
	 (* case e1 of [X]_e2 => P else Q *)
       | SPI_DESTRUCT of spi_term * string * string list * located_process * located_process
	 (* case e1 of f (X1,...,Xn) => P else Q *)
       | SPI_IN of spi_term * string * located_process
	 (* in (c, x); P *)
       | SPI_OUT of spi_term * spi_term * located_process
       | SPI_LET of string * spi_term * located_process
       (*| SPI_EVT of spi_term * located_process*)
       | SPI_PAR of located_process list
withtype located_process = spi_process * int * int * int * int
	 ;

datatype spi_declaration = SPI_PROC of string * string list * located_process
	 ;

type spi_program = |[processes : string -m> string list * located_process,
		     constructors : string set,
		     funs : string -m> int
		     ]|;

extern val is_fun : string -> bool;
extern val print_spi_term : 'a outstream -> spi_term -> unit;
extern val mangle : 'a outstream -> |[ put : string -> unit ]|;