(* Lean semantics of ispi programs.
   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 "lean_h";

exception LeanSemantics;
exception LeanNotFound of string;
exception LeanCallArityMismatch of string;

(*
fun tuple nil = "nil" $ nil
  | tuple (t::l) = "cons" $ [t, tuple l];
*)

fun contC xi =
    let val t = SPI_APPL ("_c", [SPI_VAR x | x in list xi])
	val f as |[convert, ...]| = outstring ""
    in
	print_spi_term (mangle f) t;
	convert ()
    end;
(*
    let val f as |[convert, put, ...]| = outstring "__c"
	val |[put = mput, ...]| = mangle f
    in
	iterate
	  (put "_";
	   mput x)
	| x in list xi
	end;
	convert ()
    end;
*)

fun mkenv (xi, terms) =
    contC xi $ terms;

fun lean_semantics |[ funs, constructors, processes, ...]| =
    let open "gensym"
	val subprocs = ref ({} : located_process -m> string)
	memofun q lp = if lp inset !subprocs
			   then ?(!subprocs) lp
		       else let val s = gensym "q"
			    in
				subprocs := !subprocs ++ {lp => s};
				s
			    end
	val bullet = gensym "q"
	val start = (SPI_CALL ("main", nil), 0, 0, 0, 0)
	val startq = q start
	fun eq e = let val f as |[convert, ...]| = outstring "eq_"
		   in
		       print_spi_term (mangle f) e;
		       convert ()
		   end
	fun eq_inv e = let val f as |[convert, ...]| = outstring "eq_inv_"
		       in
			   print_spi_term (mangle f) e;
			   convert ()
		       end
	fun Xi i = let val f as |[convert, ...]| = outstring "X"
		   in
		       print f (pack (i:int));
		       V (convert ())
		   end
	fun vars_of l =
	    let val ir = ref 0
	    in
		[(inc ir; Xi (!ir)) | _ in list l]
	    end
	fun vars_upto k =
	    let val ir = ref 0
	    in
		[(inc ir; Xi (!ir)) |while !ir<k]
	    end
	val csr = ref (
		       ("start", GCLAUSE (nil, ["to" $ [bullet $ nil, startq $ nil]])) ::
		       ("zero", GCLAUSE (nil, ["nat" $ ["0" $ nil]])) ::
		       ("s", GCLAUSE (["nat" $ [V "X"]], ["nat" $ ["s" $ [V "X"]]])) ::
		       nil
		       : (string * string gclause) list)
	memofun do_expr (SPI_VAR _) = ()
	      | do_expr (e as SPI_APPL (f, l)) =
		let val vars = vars_of l
		in
		    csr := ("fun_" ^ f ^ "_eq",
			    GCLAUSE ([eq ei $ [xi]
				     || ei in list l and xi in list vars],
				       [eq e $ [f $ vars]])) :: !csr;
		    iterate
		      do_expr ei
		    | ei in list l
		    end
		end
	memofun do_inv_expr e =
		(do_expr e;
		 csr :=
		 ("pub_inv", GCLAUSE ([eq e $ ["pub" $ [V "X"]]],
					[eq_inv e $ ["prv" $ [V "X"]]])) ::
		 ("prv_inv", GCLAUSE ([eq e $ ["prv" $ [V "X"]]],
					[eq_inv e $ ["pub" $ [V "X"]]])) ::
		 !csr)

	val doner = ref ({} : located_process set)
	fun do_procs (xi : string list, lp as (p, ...) : located_process) =
	    if lp inset !doner
		then ()
	    else
		let val fromq = q lp
		    val reach = "to" $ [V "E", fromq $ nil]
		in
		    doner := !doner U {lp};
		    case p of
			SPI_ZERO => ()
		      | SPI_CALL (f, el) =>
			let val (xl, lp') = ?processes f handle MapGet => raise LeanNotFound f
			    val vars = vars_of el
			    val neg = reach ::
				[(do_expr e;
				  eq e $ [X])
				|| e in list el and X in list vars]
				handle ParSweep => raise LeanCallArityMismatch f
			    val toq = q lp'
			in
			    csr :=
			    ("call", GCLAUSE (neg, ["to" $ [fromq $ nil, toq $ nil]])) ::
			    ([("call_eq", GCLAUSE (neg, [eq (SPI_VAR x) $ [X]]))
			     || x in list xl and X in list vars] @ !csr);
			    do_procs (xl, lp')
			end
		      | SPI_BANG (pidvar, lp') =>
			let val toq = q lp'
			in
			    csr :=
			    ("bang", GCLAUSE ([reach], ["to" $ [fromq $ nil, toq $ nil]])) ::
			    ("bang_eq", GCLAUSE ([reach, "nat" $ [V "X"]],
						   [eq (SPI_VAR pidvar) $ [V "X"]])) ::
			    !csr;
			    do_procs (pidvar :: xi, lp')
			end
		      | SPI_NEW (x, lp') =>
			let val toq = q lp'
			    val k = len xi
			    val vars = vars_of xi
			in
			    csr :=
			    ("new", GCLAUSE ([reach], ["to" $ [fromq $ nil, toq $ nil]])) ::
			    ("new_eq", GCLAUSE (reach ::
						[eq (SPI_VAR y) $ [X]
						|| y in list xi and X in list vars],
						[eq (SPI_VAR x) $ ["__nu" $ [fromq $ nil,
									     mkenv (xi, vars)]]])) ::
			    !csr;
			    do_procs (xi, lp')
			end
		      | SPI_IF (e, e', thenb, elseb) =>
			let val neg_ok = [reach, eq e $ [V "X"], eq e' $ [V "X"]]
			    val neg_not_ok = [reach, eq e $ [V "X"], eq e' $ [V "Y"]]
			     val thenq = q thenb
			     val elseq = q elseb
			in
			    do_expr e; do_expr e';
			    csr :=
			    ("if_eq", GCLAUSE (neg_ok, ["to" $ [fromq $ nil, thenq $ nil]])) ::
			    !csr;
			    do_procs (xi, thenb);
			    csr :=
			    ("if_diff", GCLAUSE (neg_not_ok,
						 ["to" $ [fromq $ nil, elseq $ nil]])) ::
			    !csr;
			    do_procs (xi, elseb)
			end
		       | SPI_DECRYPT_SYM (e1, x, e2, thenb, elseb) =>
			 let val neg_ok = [reach, eq e1 $ ["crypt" $ [V "X", V "Y"]],
					   eq e2 $ [V "Y"]]
			     val neg_not_ok = [reach, eq e1 $ [V "X"]]
			     val thenq = q thenb
			     val elseq = q elseb
			 in
			     do_expr e1; do_expr e2;
			     csr :=
			     ("case_crypt", GCLAUSE (neg_ok,
						     ["to" $ [fromq $ nil, thenq $ nil]])) ::
			     ("case_crypt_eq", GCLAUSE (neg_ok, [eq (SPI_VAR x) $ [V "X"]])) ::
			     !csr;
			     do_procs (x :: xi, thenb);
			     csr :=
			     ("case_crypt_diff", GCLAUSE (neg_not_ok,
							  ["to" $ [fromq $ nil, elseq $ nil]])) ::
			     !csr;
			     do_procs (xi, elseb)
			 end
		       | SPI_DECRYPT_ASYM (e1, x, e2, thenb, elseb) =>
			 let val neg_ok = [reach, eq e1 $ ["crypt" $ [V "X", V "Y"]],
					   eq_inv e2 $ [V "Y"]]
			     val neg_not_ok = [reach, eq e1 $ [V "X"]]
			     val thenq = q thenb
			     val elseq = q elseb
			 in
			     do_expr e1; do_inv_expr e2;
			     csr :=
			     ("case_crypt", GCLAUSE (neg_ok,
						     ["to" $ [fromq $ nil, thenq $ nil]])) ::
			     ("case_crypt_eq", GCLAUSE (neg_ok, [eq (SPI_VAR x) $ [V "X"]])) ::
			     !csr;
			     do_procs (x :: xi, thenb);
			     csr :=
			     ("case_crypt_diff", GCLAUSE (neg_not_ok,
							  ["to" $ [fromq $ nil, elseq $ nil]])) ::
			     !csr;
			     do_procs (xi, elseb)
			 end
		      | SPI_DESTRUCT (e1, f, xl, thenb, elseb) =>
			let val vars = vars_of xl
			    val neg_ok = [reach, eq e1 $ [f $ vars]]
			    val thenq = q thenb
			    val elseq = q elseb
			in
			    do_expr e1;
			    csr :=
			    ("case_" ^ f, GCLAUSE (neg_ok, ["to" $ [fromq $ nil, thenq $ nil]])) ::
			    ([("case_" ^ f ^ "_eq", GCLAUSE (neg_ok, [eq (SPI_VAR x) $ [X]]))
			     || x in list xl and X in list vars] @ !csr);
			    do_procs (xl @ xi, thenb);
			    iterate
			      let val vars = vars_upto k
				  val neg = [reach, eq e1 $ [g $ vars]]
			      in
				  csr :=
				  ("case_" ^ f ^ "_diff_" ^ g,
				   GCLAUSE (neg, ["to" $ [fromq $ nil, elseq $ nil]])) ::
				  !csr
			      end
			    | g => k in map funs
				such that g<>f
			    end;
			    do_procs (xi, elseb)
			end
		      | SPI_IN (c, x, lp') =>
			let val neg = [reach, "send" $ [V "P", V "X", V "Y"], eq c $ [V "X"]]
			    val toq = q lp'
			in
			    do_expr c;
			    csr :=
			    ("in", GCLAUSE (neg, ["to" $ [fromq $ nil, toq $ nil]])) ::
			    ("in_eq", GCLAUSE (neg, [eq (SPI_VAR x) $ [V "Y"]])) ::
			    ("in_recv", GCLAUSE (neg, ["recv" $ [V "P", V "X",
								 V "Y", toq $ nil]])) ::
			    !csr;
			    do_procs (x :: xi, lp')
			end
		      | SPI_OUT (c, e, lp') =>
			let val neg = [reach, eq c $ [V "X"], eq e $ [V "Y"]]
			    val toq = q lp'
			in
			    do_expr c; do_expr e;
			    csr :=
			    ("out", GCLAUSE (neg, ["to" $ [fromq $ nil, toq $ nil]])) ::
			    ("out_send", GCLAUSE (neg, ["send" $ [fromq $ nil,
								  V "X", V "Y"]])) ::
			    !csr;
			    do_procs (xi, lp')
			end
		      | SPI_LET (x, e, lp') =>
			let val neg = [reach, eq e $ [V "X"]]
			    val toq = q lp'
			in
			    do_expr e;
			    csr :=
			    ("let", GCLAUSE (neg, ["to" $ [fromq $ nil, toq $ nil]])) ::
			    ("let_eq", GCLAUSE (neg, [eq (SPI_VAR x) $ [V "X"]])) ::
			    !csr;
			    do_procs (x :: xi, lp')
			end
		      | SPI_PAR lpl =>
			iterate
			  (csr := ("par", GCLAUSE ([reach], ["to" $ [fromq $ nil, toq $ nil]]))
			   :: !csr;
			   do_procs (xi, lp'))
			| lp' in list lpl
			val toq = q lp'
			end
		      | spi => raise LeanSemantics
		end
    in
	do_procs (nil, start);
	(!subprocs, !csr)
    end;