(*
 *	Copyright (c) 2002 by Laboratoire Spécification et Vérification (LSV),
 *	CNRS UMR 8643 & ENS Cachan.
 *	Written by Jean Goubault-Larrecq.  Not derived from licensed software.
 *
 *	Permission is granted to anyone to use this software for any
 *	purpose on any computer system, and to redistribute it freely,
 *	subject to the following restrictions:
 *
 *	1. Neither the author nor its employer is responsible for the consequences of use of
 *		this software, no matter how awful, even if they arise
 *		from defects in it.
 *
 *	2. The origin of this software must not be misrepresented, either
 *		by explicit claim or by omission.
 *
 *	3. Altered versions must be plainly marked as such, and must not
 *		be misrepresented as being the original software.
 *
 *	4. This software is restricted to non-commercial use only.  Commercial
 *		use is subject to a specific license, obtainable from LSV.
 *		This was developed as part of the EVA project; as such, access
 *		to this software by partners of the RNTL EVA Project (Trusted
 *		Logic S.A., Verimag) is defined by the intellectual property
 *		agreement signed as part of this project.
 *)

open Term

let lispwrite file =
    let outint i = output_string file (string_of_int i) in
    let outintsp i = (output_char file ' '; outint i) in
    let rec write t = match t with
            (VAR s) -> (output_char file '"';
			output_string file (String.escaped s);
			output_char file '"')
          | (INT i) -> outint i
          | (APP (f, l)) -> (output_char file '(';
				   output_string file f;
				   wl l;
				   output_char file ')')
          | (LINE (t, { first_line = i;
			first_column = j;
			last_line = k;
			last_column = l;
			in_file = s})) -> (output_string file "(line ";
					   write t;
					   outintsp i;
					   outintsp j;
					   outintsp k;
					   outintsp l;
					   output_char file ' ';
					   output_char file '"';
					   output_string file (String.escaped s);
					   output_char file '"';
					   output_char file ')')
        and wl l = match l with
			[] -> ()
		      | a::r -> (output_char file ' '; write a; wl r)
    in write;;