(* Time-stamp: <modified the 20/03/2013 (at 17:57) by Erwan Jahier> *)

open SocExecValue
open Soc

(* A boring but simple module... *)

let (lustre_plus : ctx -> ctx) =
  fun ctx -> 
    let (vn,vv) =
      match [get_val "x" ctx; get_val "y" ctx] with
        | [I x1; I x2] -> "z"::ctx.cpath,I(x1+x2)
        | [F i1; F i2] -> "z"::ctx.cpath,F(i1+.i2)
        | [U; _] | [_;U] -> "z"::ctx.cpath,U
        |  _  -> assert false
    in
    { ctx with s = sadd ctx.s vn vv }

let lustre_times ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 * x2)
      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 *. x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_div ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_minus ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 - x2)
      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 -. x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_mod ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 mod x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_eq ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,B(x1 = x2)
      | [F x1; F x2] -> "z"::ctx.cpath,B(x1 = x2)
      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 = x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_uminus ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx]) with
      | [I x1] -> "z"::ctx.cpath,I(- x1)
      | [F x1] -> "z"::ctx.cpath,F(-. x1)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_real2int ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx]) with
      | [F x1] -> "z"::ctx.cpath,I(int_of_float x1)
      | [U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_int2real ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx]) with
      | [I x1] -> "z"::ctx.cpath,F(float_of_int x1)
      | [U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_not ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx]) with
      | [B x1] -> "z"::ctx.cpath,B(not x1)
      | [U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_lt ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,B(x1 < x2)
      | [F x1; F x2] -> "z"::ctx.cpath,B(x1 < x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }
 
let lustre_gt ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,B(x1 > x2)
      | [F x1; F x2] -> "z"::ctx.cpath,B(x1 > x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_lte ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,B(x1 <= x2)
      | [F x1; F x2] -> "z"::ctx.cpath,B(x1 <= x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_gte ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [I x1; I x2] -> "z"::ctx.cpath,B(x1 >= x2)
      | [F x1; F x2] -> "z"::ctx.cpath,B(x1 >= x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_and ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 && x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_neq  ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_or  ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 || x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }


let lustre_impl ctx =
  let (vn,vv) = 
    match ([get_val "x" ctx; get_val "y" ctx]) with
      | [B x1; B x2] -> "z"::ctx.cpath,B(not x1 or x2)
      | [U; _] | [_;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }

let lustre_if ctx =
  let (vn,vv) = 
    match ([get_val "c" ctx; get_val "xt" ctx; get_val "xe" ctx]) with
      | [B c; I x1; I x2]  -> "z"::ctx.cpath,I(if c then x1 else x2)
      | [B c; F x1; F x2]  -> "z"::ctx.cpath,F(if c then x1 else x2)
      | [B c; B x1; B x2]  -> "z"::ctx.cpath,B(if c then x1 else x2)
      | [B c; I x1; U]     -> "z"::ctx.cpath,if c then I x1 else U 
      | [B c; U; I x2]     -> "z"::ctx.cpath,if c then U else I x2
      | [B c; B x1; U]     -> "z"::ctx.cpath,if c then B x1 else U 
      | [B c; U; B x2]     -> "z"::ctx.cpath,if c then U else B x2
      | [B c; F x1; U]     -> "z"::ctx.cpath,if c then F x1 else U 
      | [B c; U; F x2]     -> "z"::ctx.cpath,if c then U else F x2
      | [U;_; _] | [_;U;U] -> "z"::ctx.cpath,U
      | _  -> assert false
  in
  { ctx with s = sadd ctx.s vn vv }
 
let lustre_array tl ctx =
  let t,size = match List.hd (List.rev tl) with
    | Soc.Array(t,i) -> t,i
    | _ -> assert false
  in
  let inames = 
    let res = ref [] in
    for k=size downto 1 do
      res:= ("x"^(string_of_int k)) :: !res;
    done;
    !res
  in
  let l = List.map (fun name -> get_val name ctx) inames in
  let a = Array.of_list l in
  { ctx with s = sadd ctx.s ("z"::ctx.cpath) (A a) }

  let lustre_hat tl ctx =
    let i = match tl with
      | [_;Soc.Array(_,i)] -> i
      | _ -> assert false
    in
    let (vn,vv) = 
      match ([get_val "x" ctx]) with
        | [B x]  -> "z"::ctx.cpath,A(Array.make i (B x))
        | [I x]  -> "z"::ctx.cpath,A(Array.make i (I x))
        | [F x]  -> "z"::ctx.cpath,A(Array.make i (F x))
        | [A x]  -> "z"::ctx.cpath,A(Array.make i (A x))
        | [U]  -> "z"::ctx.cpath,U
        | _  -> assert false
    in
    { ctx with s = sadd ctx.s vn vv }
 
(* That one is different *)
let lustre_xor ctx = assert false
let lustre_diese ctx = assert false
(*   let (vn,vv) =  *)
(*     let values = [get_val "x" ctx; get_val "y" ctx] in *)
(*     let l = List.filter (fun x -> x=B true) values in *)
(*     "z"::ctx.cpath,B(List.length l = 1) *)


(* exported *)
let (get: Soc.key -> (ctx -> ctx)) =
  fun (n,tl,_) -> 
    match n with
    | "Lustre::plus" -> lustre_plus
    | "Lustre::times"-> lustre_times 
    | "Lustre::div"  -> lustre_div 
    | "Lustre::minus"-> lustre_minus

    | "Lustre::mod" -> lustre_mod
    | "Lustre::uminus" -> lustre_uminus
    | "Lustre::not" -> lustre_not 
    | "Lustre::real2int" -> lustre_real2int
    | "Lustre::int2real" -> lustre_int2real

    | "Lustre::lt"  -> lustre_lt
    | "Lustre::gt"  -> lustre_gt
    | "Lustre::lte" -> lustre_lte
    | "Lustre::gte" -> lustre_gte

    | "Lustre::and" -> lustre_and 
    | "Lustre::eq" -> lustre_eq 
    | "Lustre::neq" -> lustre_neq 
    | "Lustre::or"  -> lustre_or 

    | "Lustre::impl" -> lustre_impl

    | "Lustre::if" -> lustre_if

    | "Lustre::hat" -> lustre_hat tl
    | "Lustre::array" -> lustre_array tl

    | "Lustre::xor" -> lustre_xor 
    | "Lustre::diese" -> lustre_diese
    | _ -> raise Not_found