socPredef2c.ml

(* Time-stamp: <modified the 12/06/2014 (at 11:11) by Erwan Jahier> *)

open Data
open Soc
open Soc2cIdent

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

let (lustre_binop : Soc.key -> string -> string) =
  fun sk op  -> 
    let ctx = get_ctx_name sk in
    Printf.sprintf "  %s.z = (%s.x %s %s.y);\n" ctx ctx op ctx

let (lustre_unop : Soc.key -> string -> string) =
  fun sk op  -> 
    let ctx = get_ctx_name sk in
    Printf.sprintf"  %s.z = %s %s.x;\n" ctx op ctx

let (lustre_ite : Soc.key -> string) =
  fun sk -> 
    let ctx = get_ctx_name sk in
    Printf.sprintf"  %s.z = (%s.c)? %s.xt : %s.xe;\n" ctx ctx ctx ctx

let (lustre_impl : Soc.key -> string) =
  fun sk -> 
    let ctx = get_ctx_name sk in
    Printf.sprintf"  %s.z = (!%s.x || %s.y);\n" ctx ctx ctx

let (lustre_arrow : Soc.key -> string) =
  fun sk -> 
    let ctx = get_ctx_name sk in
    let x,y,z = ctx^".x", ctx^".y", ctx^".z" in
    Printf.sprintf"  %s = (first_step)? %s : %s;\n" z x y

let (lustre_merge : Soc.key -> string) =
  fun sk -> 
    let ctx = get_ctx_name sk in
    let (_,tc::tl,_) = sk in
    match tc with
      | Bool ->
        Printf.sprintf"  %s.z = (%s.clk) ? %s.x1 : %s.x2  ;\n" ctx ctx ctx ctx
      | Enum(en,el) ->
        let case_list = List.mapi
          (fun i e -> Printf.sprintf "    case %s: %s.x%i; break;\n" (id2s e) ctx i) el  
        in
        let cases = String.concat "" case_list in
        Printf.sprintf"  %s.z =\n    switch (%s.clk){\n%s}\n" ctx ctx cases
      | Int ->
        let case_list = List.mapi
          (fun i e -> Printf.sprintf "    case %i: %s.z = %s.x%i; break;\n" i ctx ctx i) tl  
        in
        let cases = String.concat "" case_list in
        Printf.sprintf"  switch (%s.clk){\n%s}\n" ctx cases
      | _ -> assert false


let (lustre_hat : Soc.key -> string) =
  fun (n,tl,si_opt) -> 
    let ctx = get_ctx_name (n,tl,si_opt) in
    let i,t = match tl with
      | [_;Data.Array(t,i)] -> i,t
      | _ -> assert false
    in
    let buff = ref "" in
    for j=0 to i-1 do
      buff := !buff^(Soc2cUtil.gen_assign t (Printf.sprintf "%s.z[%d]" ctx j)
                       (Printf.sprintf "%s.x" ctx)); 
    done;
    !buff

let (lustre_array: Soc.key -> string) =
  fun (n,tl,si_opt) -> 
    let ctx = get_ctx_name (n,tl,si_opt) in
    let t,i = match List.hd (List.rev tl) with
      | Data.Array(t,i) -> t,i
      | _ -> assert false
    in
    let buff = ref "" in
    for j=0 to i-1 do
      buff := !buff^(Soc2cUtil.gen_assign t (Printf.sprintf "%s.z[%d]" ctx j)
                       (Printf.sprintf "%s.x%d" ctx (j+1))); 
    done;
    !buff


 
let (lustre_concat: Soc.key -> string) =
  fun sk -> 
    let ctx = get_ctx_name sk in
    assert false

let (lustre_slice: Soc.key -> string) =
  fun sk -> 
    let ctx = get_ctx_name sk in 
    assert false



(* exported *)
let (get: Soc.key -> string) =
  fun sk -> 
    let (n,tl,si_opt) = sk in
    match n with
      | "Lustre::rplus" 
      | "Lustre::plus"
      | "Lustre::iplus"  -> lustre_binop sk "+" 
      | "Lustre::itimes" 
      | "Lustre::times"
      | "Lustre::rtimes" -> lustre_binop sk "*" 
      | "Lustre::idiv"
      | "Lustre::div"  
      | "Lustre::rdiv"   -> lustre_binop sk "/" 
      | "Lustre::islash" 
      | "Lustre::slash" 
      | "Lustre::rslash" -> lustre_binop sk "/"
      | "Lustre::iminus"
      | "Lustre::minus"
      | "Lustre::rminus" -> lustre_binop sk "-" 

      | "Lustre::mod" -> lustre_binop sk "%"
      | "Lustre::iuminus"
      | "Lustre::uminus" 
      | "Lustre::ruminus"-> lustre_unop sk "-" 

      | "Lustre::eq" -> lustre_binop sk "==" 

      | "Lustre::and" -> lustre_binop sk "&&" 
      | "Lustre::neq" -> lustre_binop sk "<>"  
      | "Lustre::or"  -> lustre_binop sk "||"  

      | "Lustre::xor" -> lustre_binop sk "^" 
      | "Lustre::not" -> lustre_unop  sk "!"
      | "Lustre::real2int" -> lustre_unop sk "(_integer)"
      | "Lustre::int2real" -> lustre_unop sk "(_real)"

      | "Lustre::lt"
      | "Lustre::rlt"
      | "Lustre::ilt" -> lustre_binop sk "<"
      | "Lustre::gt"
      | "Lustre::rgt"
      | "Lustre::igt" -> lustre_binop sk ">"
      | "Lustre::lte" 
      | "Lustre::rlte"
      | "Lustre::ilte" -> lustre_binop sk "<="
      | "Lustre::gte"
      | "Lustre::rgte"
      | "Lustre::igte" -> lustre_binop sk ">="
      | "Lustre::impl" -> lustre_impl sk

      | "Lustre::if"
      | "Lustre::rif"
      | "Lustre::iif" -> lustre_ite sk

      | "Lustre::arrow" -> lustre_arrow sk
      | "Lustre::merge" -> lustre_merge sk

      | "Lustre::hat" -> lustre_hat sk
      | "Lustre::array" -> lustre_array sk
      | "Lustre::concat" -> lustre_concat sk
      | "Lustre::array_slice" -> lustre_slice sk

      | "Lustre::current" -> assert false (* o*)
      | "Lustre::nor" -> assert false (* ougth to be translated into boolred *)
      | "Lustre::diese" -> assert false (* ditto *)

      | _ -> assert false