predefEvalConst.ml

(** Time-stamp: <modified the 21/11/2008 (at 10:37) by Erwan Jahier> *)

open Predef
open Eff

(* open Lxm *)
(* open Errors *)

type const_evaluator = Eff.const evaluator
   
exception EvalConst_error of string

let eval_real_error () =
  raise (EvalConst_error "reals cannot be evaluated, sorry.")

(* exported *)
let (type_error_const : Eff.const list -> string -> 'a) =
  fun v expect -> 
    raise (EvalConst_error(
             "type mismatch "^(if expect = "" then "" else (expect^" expected"))))
      

let (arity_error_const : Eff.const list -> string -> 'a) =
  fun v expect -> 
    raise (EvalConst_error(
             Printf.sprintf "\n*** arity error: %d argument%s, whereas %s were expected"
               (List.length v) (if List.length v>1 then "s" else "") expect))
    

let (bbb_evaluator:(bool -> bool -> bool) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Bool_const_eff v0; Bool_const_eff v1] -> [Bool_const_eff (op v0 v1)]
    | _ -> assert false (* should not occur because eval_type is called before *)
          
let (ooo_evaluator:(int -> int -> int) -> (float -> float -> float) -> 
      const_evaluator) =
  fun opi opr -> fun ll -> match List.flatten ll with
      | [Int_const_eff v0; Int_const_eff v1] -> [Int_const_eff (opi v0 v1)]
       | [Real_const_eff v0; Real_const_eff v1] -> eval_real_error ()
           (* [Real_const_eff (opr v0 v1)] *)
      | _ -> assert false (* should not occur because eval_type is called before *)

let (iii_evaluator:(int -> int -> int) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Int_const_eff v0; Int_const_eff v1] -> [Int_const_eff (op v0 v1)]
    | _ -> assert false (* should not occur because eval_type is called before *)

let (aab_evaluator:('a -> 'a -> bool) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [v0; v1] -> [Bool_const_eff (op v0 v1)]
    | _ -> assert false (* should not occur because eval_type is called before *)

let (fff_evaluator:(float -> float -> float) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Real_const_eff v0; Real_const_eff v1] -> eval_real_error ()
(*         [Real_const_eff (op v0 v1)] *)
    | _ -> assert false (* should not occur because eval_type is called before *)
        
let (bb_evaluator:(bool -> bool) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Bool_const_eff v0] -> [Bool_const_eff (op v0)]
    | _ -> assert false (* should not occur because eval_type is called before *)
        
let (ii_evaluator:(int -> int) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Int_const_eff v0] -> [Int_const_eff (op v0)]
    | _ -> assert false (* should not occur because eval_type is called before *)
        
let (ff_evaluator:(float -> float) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Real_const_eff v0] -> eval_real_error () (* [Real_const_eff (op v0)] *)
    | _ -> assert false (* should not occur because eval_type is called before *)
        
let (oo_evaluator:(int -> int) -> (float -> float) -> const_evaluator) =
  fun opi opr  -> fun ll -> match List.flatten ll with
    | [Int_const_eff v0] -> [Int_const_eff (opi v0)]
    | [Real_const_eff v0] -> eval_real_error () (* [Real_const_eff (opr v0)] *)
    | _ -> assert false (* should not occur because eval_type is called before *)
        
let (sf_evaluator: Ident.t -> const_evaluator) =
  fun id ceff_ll ->  [Real_const_eff (Ident.to_string id)]

let (si_evaluator: Ident.t -> const_evaluator) =
  fun id ceff_ll -> 
    try let v = int_of_string (Ident.to_string id) in
      [Int_const_eff v]
    with Failure  "int_of_string" -> 
      raise (EvalConst_error(
               Printf.sprintf "\n*** fail to convert the string \"%s\" into an int"
                 (Ident.to_string id)))

let (sb_evaluator: bool -> const_evaluator) =
  fun v ceff_ll -> 
      [Bool_const_eff v]

let (fi_evaluator:(string -> int) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
     | [Real_const_eff v0] ->  [Int_const_eff (op v0)] 
    | _ -> assert false (* should not occur because [eval_type] is called before *)

let (if_evaluator: (int -> string) -> const_evaluator) =
  fun op -> fun ll -> match List.flatten ll with
    | [Int_const_eff v0] -> [Real_const_eff (op v0)]
    | _ -> assert false (* should not occur because [eval_type] is called before *)
        
let (ite_evaluator : const_evaluator) =
  function
    | [[Bool_const_eff c]; t; e] -> if c then t else e
    | _ -> assert false (* should not occur because [eval_type] is called before *)

let (boolred_evaluator : int -> int -> const_evaluator) =
  fun min max ceff_ll ->
    let nb = List.fold_left
      (fun acc -> function
         | (Bool_const_eff b) -> if b then acc+1 else acc | _ -> assert false)
      0
      (List.flatten ceff_ll)
    in
      [Bool_const_eff (min <= nb && nb <= max )]
      
         
(* exported *)
let (f: op -> Lxm.t -> Eff.static_arg list -> const_evaluator) = 
  fun op lxm sargs ll -> 
    (* we first check the type so that we do not need to check it during the const
       evaluation *)
    ignore (PredefEvalType.f op lxm sargs (List.map (List.map Eff.type_of_const) ll));
    match op with
      | TRUE_n  -> sb_evaluator true ll
      | FALSE_n -> sb_evaluator false ll
      | ICONST_n id -> si_evaluator id ll
      | RCONST_n id -> sf_evaluator id ll
      | NOT_n -> bb_evaluator (not) ll
      | REAL2INT_n -> fi_evaluator int_of_string ll
      | INT2REAL_n -> if_evaluator string_of_int ll
      | AND_n  -> bbb_evaluator (&&) ll
      | OR_n   -> bbb_evaluator (||) ll
      | XOR_n  -> bbb_evaluator (<>) ll
      | IMPL_n -> bbb_evaluator (fun a b -> (not a) || b) ll
      | EQ_n   -> aab_evaluator (=) ll
      | NEQ_n  -> aab_evaluator (<>) ll 
      | LT_n   -> aab_evaluator (<) ll
      | LTE_n  -> aab_evaluator (<=) ll
      | GT_n   -> aab_evaluator (>) ll
      | GTE_n  -> aab_evaluator (>=) ll
      | DIV_n  -> iii_evaluator (/) ll
      | MOD_n  -> iii_evaluator (mod) ll
      | IF_n -> ite_evaluator ll
      | UMINUS_n -> oo_evaluator (fun x -> -x) (fun x -> -.x) ll
      | MINUS_n -> ooo_evaluator (-) (-.) ll
      | PLUS_n  -> ooo_evaluator (+) (+.) ll
      | SLASH_n -> ooo_evaluator (/) (/.) ll
      | TIMES_n -> ooo_evaluator ( * ) ( *.) ll
      | IUMINUS_n  -> ii_evaluator (fun x -> -x) ll
      | IMINUS_n -> iii_evaluator (-) ll
      | IPLUS_n  -> iii_evaluator (+) ll
      | ISLASH_n -> iii_evaluator (/) ll
      | ITIMES_n -> iii_evaluator ( * ) ll
      | RUMINUS_n -> ff_evaluator (fun x -> -.x) ll
      | RMINUS_n -> fff_evaluator (-.) ll
      | RPLUS_n  -> fff_evaluator (+.) ll
      | RSLASH_n -> fff_evaluator (/.) ll
      | RTIMES_n -> fff_evaluator ( *.) ll
      | NOR_n   -> boolred_evaluator 0 0 ll
      | DIESE_n -> boolred_evaluator 1 1 ll
      | Map -> assert false
      | Fill -> assert false
      | Red -> assert false
      | FillRed -> assert false
      | BoolRed -> 
          match sargs with 
            | [ConstStaticArgEff(_,Int_const_eff i);
               ConstStaticArgEff(_,Int_const_eff j);
               ConstStaticArgEff(_,Int_const_eff n)
              ] -> 
                boolred_evaluator i j ll

            | _ -> assert false

(*********************************************************************************)
(*********************************************************************************)
(* 
pour evaluer l'galit, Pascal faisait comme ca (j'ai t plus (trop ?) brutal) :
      (*----------------------------
        Calcul de l'galit
        N.B. Sur les constantes abstraites
        on est trs mfiant
        N.B. Sur les types structure,
        on fait des appels rcursifs
        ----------------------------*)
    let rec compute_eq 
        (args : const_eff list)
        = (
          let rec fields_eq f0 f1 = (
            match (f0, f1) with
              | ([], []) -> 
                  [Bool_const_eff true]
                 
              | ((f0,h0)::t0, (f1,h1)::t1) -> (
                  assert (f0 = f1);
                  match (compute_eq [h0;h1]) with
                      [Bool_const_eff false] -> [Bool_const_eff false]
                    | [Bool_const_eff true] -> (fields_eq t0 t1) 
                    | _ -> assert false
                )
              | _ -> assert false
          ) 
          in
            match args with
                [Bool_const_eff v0; Bool_const_eff v1] -> [Bool_const_eff (v0 = v1)]
              | [Int_const_eff v0; Int_const_eff v1] -> [Bool_const_eff (v0 = v1)]
              | [Real_const_eff v0; Real_const_eff v1] -> (
                  let res = (v0 = v1) in
                    warning src 
                      (sprintf "float in static exp: %f=%f evaluated as %b" v0 v1 res);
                    [Bool_const_eff res]
                )
                  (*
                    2007-07 obsolete

                    |  [Extern_const_eff (v0, t0); Extern_const_eff (v1, t1)] -> (
                    if (t0 <> t1) then (
                    type_error args "t*t for some type t"
                    ) else if (v0 <> v1) then (
                    uneval_error args (
                    sprintf "%s=%s (external constants)"
                    (string_of_fullid v0)
                    (string_of_fullid v1)
                    )
                    ) else (
                    [Bool_const_eff true]
                    )
                    )
                  *)
              | [Enum_const_eff (v0, t0); Enum_const_eff (v1, t1)] -> (
                  if (t0 = t1) then [Bool_const_eff (v0 =  v1)]
                  else type_error args "t*t for some type t"
                )
              | [Struct_const_eff (f0, t0); Struct_const_eff (f1, t1)] -> (
                  if (t0 = t1) then (fields_eq f0 f1)
                  else type_error args "t*t for some type t"
                )
              | [x;y] -> type_error args "t*t for some type t"
              | x -> arity_error args "2"
        ) 
    in
 *)