predefEvalType.ml

(** Time-stamp: <modified the 26/05/2009 (at 15:36) by Erwan Jahier> *)

open Predef
open Lxm
open Errors
open UnifyType
open Eff

(* exported *)
type typer = Eff.type_ Predef.evaluator

(* exported *)
exception EvalType_error of string


(* exported *)
let (type_error : Eff.type_ list -> string -> 'a) =
  fun tel expect -> 
    let str_l = List.map LicDump.string_of_type_eff4msg tel in
    let str_provided = String.concat "*" str_l in 
      raise (EvalType_error(
               ("\n*** type '" ^ str_provided ^ "' was provided" ^
                  (if expect = "" then "" 
                   else (" whereas\n*** type '" ^expect^"' was expected")))))

let (type_error2 : string -> string -> string -> 'a) =
  fun provided expect msg -> 
    raise (EvalType_error(
             ("\n*** type '" ^ provided ^ "' was provided" ^
                (if expect = "" then "" 
                 else (" whereas\n*** type '" ^expect^"' was expected")) ^
                (if msg = "" then "" else ("\n*** " ^ msg)))))

let (arity_error : 'a list -> string -> 'b) =
  fun v expect -> 
    raise (EvalType_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))

(*********************************************************************************)
(* a few local alias to make the node profile below more readable. *)
let i = Int_type_eff
let r = Real_type_eff
let b = Bool_type_eff
let id str = Ident.of_string str

(** A few useful type profiles for simple operators *)
let bb_profile  = [(id "i", b)], [(id "o", b)]               (* bool -> bool *)
let bbb_profile = [(id "i1", b);(id "i2", b)], [(id "o", b)] (* bool*bool -> bool *)
let ii_profile  = [(id "i", i)], [(id "o", i)]               (* int -> int *)
let iii_profile = [(id "i1", i);(id "i2", i)], [(id "o", i)] (* int*int -> int *)
let rr_profile  = [(id "i", r)], [(id "o", r)]               (* real -> real *)
let rrr_profile = [(id "i1", r);(id "i2", r)], [(id "o", r)] (* real*real -> real *)
let ri_profile  = [id "i", r], [id "o", i] (* real -> int  *)
let ir_profile  = [id "i", i], [id "o", r] (* int  -> real *)

(** Constant profiles  *)
let b_profile = [],[id "o", b]
let i_profile = [],[id "o", i]
let r_profile = [],[id "o", r]

(** polymorphic operator profiles *)
let aab_profile = [(id "i1",Any);(id "i2",Any)], [(id "o", b)] (* 'a -> 'a -> bool*)
let baaa_profile = [(id "c", b);(id "b1",Any);(id "b2",Any)], [(id "o",Any)] 
  (* for if-then-else *)

(** overloaded operator profiles *)
let oo_profile  = [(id "i",Overload)], [(id "o",Overload)]
let ooo_profile = [(id "i1",Overload);(id "i2",Overload)], [(id "o",Overload)]

(** iterators profiles *)
(* [type_to_array_type [x1;...;xn] c] returns the array type [x1^c;...;xn^c] *)
let (type_to_array_type: Eff.var_info list -> int -> (Ident.t * Eff.type_) list) =
  fun l c ->
    List.map (fun vi -> vi.var_name_eff, Array_type_eff(vi.var_type_eff,c)) l

(* Extract the node and the constant from a list of static args *)
let (get_node_and_constant: Lxm.t -> 
       Eff.static_arg list -> Eff.item_key * var_info list * var_info list * int) =
  fun lxm sargs -> 
      match sargs with
        | [NodeStaticArgEff(_,(n, inlist, outlist));
           ConstStaticArgEff(_,Int_const_eff c)] -> n, inlist, outlist, c

	| [NodeStaticArgEff(_,(n, inlist, outlist)); 
	   ConstStaticArgEff(_, Abstract_const_eff(l,_,Int_const_eff c, true))] ->
	    n, inlist, outlist, c

        | [NodeStaticArgEff(_,_); ConstStaticArgEff(_, Extern_const_eff(l, _))] ->
            let msg = "an integer is expected, whereas an extern constant (" ^ 
              (Ident.string_of_long l) ^ ") was provided.\n"
            in
              raise (Compile_error(lxm, msg))
        | [NodeStaticArgEff(_,_); ConstStaticArgEff(_, Abstract_const_eff(l,_,_, false))] ->
            let msg = "an integer is expected, whereas an abstract constant (" ^ 
              (Ident.string_of_long l) ^ ") was provided.\n"
            in
              raise (Compile_error(lxm, msg))
        | [NodeStaticArgEff(_,(n, inlist, outlist)); ConstStaticArgEff(_, const)] ->
            let msg = "an integer is expected, whereas a " ^ 
              (LicDump.string_of_type_eff4msg (Eff.type_of_const const)) ^
              " was provided.\n"
            in
              raise (Compile_error(lxm, msg))
        | _ -> 
            let msg = "*** an integer and a node are expected.\n" in
              raise (Compile_error(lxm, msg))


let map_profile =
  (* Given 
     - a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l
     - a constant c (nb : sargs = [n,c])
       
     The profile of map is: tau_1^c * ... * tau_n^c -> teta_1^c * ... * teta_l^c
    *)
  fun lxm sargs -> 
    let (n, inlist, outlist, c) = get_node_and_constant lxm sargs in
    let lti = type_to_array_type inlist c in
    let lto = type_to_array_type outlist c in
    let res = (lti, lto) in
      res

let get_id_type vi = vi.var_name_eff, vi.var_type_eff

let (fillred_profile : Lxm.t -> Eff.static_arg list -> 
      (Ident.t * Eff.type_) list * (Ident.t * Eff.type_) list) =
  (* Given 
     - a node n of type tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l
     - a constant c (nb : sargs = [n,c])
       
     returns the profile: 
        tau * tau_1^c * ... * tau_n^c  -> tau * teta_1^c * ... * teta_l^c
    *)
  fun lxm sargs ->
    let (n, inlist, outlist, c) = get_node_and_constant lxm sargs in
    let _ = assert(inlist <> [] && outlist <> []) in
    let lti = (get_id_type (List.hd inlist))::
      type_to_array_type (List.tl inlist) c in
    let lto = (get_id_type (List.hd outlist))::
      type_to_array_type (List.tl outlist) c in
    let (id1, t1) = List.hd lti and (id2, t2) = List.hd lto in
    let res = 
      if t1 = t2 then (lti,lto) else
        (* if they are not equal, they migth be unifiable *)
        match UnifyType.f [t1] [t2] with
          | Equal  -> (lti,lto)
          | Unif t -> 
              (List.map (fun (id,tid) -> id, subst_type t tid) lti,
               List.map (fun (id,tid) -> id, subst_type t tid) lto)
          | Ko(msg) -> raise (Compile_error(lxm, msg))
    in
      res

(* let fill_profile = fillred_profile *)
  (* Given 
     - a node N of type tau -> tau * teta_1 * ... * teta_l
     - a constant c (nb : sargs = [N,c])       
     returns the profile: [tau -> tau * teta_1^c * ... * teta_l^c] 
    *)

(* let red_profile = fillpred_profile *)
  (* Given 
     - a node N of type tau * tau_1 * ... * tau_n -> tau 
     - a constant c (nb : sargs = [N,c])
       returns the profile tau * tau_1^c * ... * tau_n^c -> tau
    *)


(* Given 
   - 3 integer constant i, j, k 
   
   returns the profile bool^k -> bool
*)
let boolred_profile =     
  fun lxm sargs -> 
    let (get_three_constants: Lxm.t -> Eff.static_arg list -> int * int * int) =
      fun lxm sargs ->
        match sargs with
          | [ConstStaticArgEff(_,Int_const_eff i);
             ConstStaticArgEff(_,Int_const_eff j);
             ConstStaticArgEff(_,Int_const_eff k)] -> i,j,k
          | _ -> raise (Compile_error(lxm, "\n*** type error: 3 int were expected"))
    in
    let (_i,_j,k) = get_three_constants lxm sargs in
      [id "i",  (Array_type_eff(Bool_type_eff,k))], [id "o", b]
        

type node_profile = (Ident.t * Eff.type_) list * (Ident.t * Eff.type_) list



let (op2profile : Predef.op -> Lxm.t -> Eff.static_arg list -> node_profile) = 
  fun op lxm sargs -> 
    let res =
      match op with
        | TRUE_n | FALSE_n -> b_profile
        | ICONST_n id      -> i_profile
        | RCONST_n id      -> r_profile
        | NOT_n            -> bb_profile
        | REAL2INT_n       -> ri_profile
        | INT2REAL_n       -> ir_profile
        | IF_n             -> baaa_profile
        | UMINUS_n         -> oo_profile
        | IUMINUS_n        -> ii_profile
        | RUMINUS_n        -> rr_profile
        | IMPL_n | AND_n | OR_n | XOR_n              -> bbb_profile 
        | NEQ_n | EQ_n | LT_n | LTE_n | GT_n | GTE_n -> aab_profile 
        | MINUS_n  |  PLUS_n |  TIMES_n |  SLASH_n                 -> ooo_profile 
        | RMINUS_n | RPLUS_n | RTIMES_n | RSLASH_n                 -> rrr_profile
        | DIV_n | MOD_n | IMINUS_n | IPLUS_n | ISLASH_n | ITIMES_n -> iii_profile
        | Red | Fill | FillRed -> fillred_profile lxm sargs
        | Map                  -> map_profile lxm sargs
        | BoolRed              -> boolred_profile lxm sargs

        | NOR_n | DIESE_n  -> assert false
        (* XXX The current representation of node_profile prevent us
           from being able to represent "bool list" (i.e., operator
           of variable arity). I could extend the type node_profile,
           but is it worth the complication just to be able to define
           alias nodes on "nor" and "#"? Actually, even if I extend
           this data type, I don'ty know how I could generate an
           alias node for them anyway...
        *)
    in
      res
(* exported *)
let (make_node_exp_eff : 
       bool option -> op -> Lxm.t -> Eff.static_arg list -> Eff.node_exp) =
  fun has_mem op lxm sargs ->
    let id = Predef.op_to_long op in
    let (lti,lto) = op2profile op lxm sargs in
    let i = ref 0 in
    let is_polymorphic = ref false in
    let to_var_info_eff nature (vid, te) =
      let res =
        if Eff.is_polymorphic te then is_polymorphic := true ;
        {
          var_name_eff = vid;
          var_nature_eff = nature;
          var_number_eff = !i;
          var_type_eff   = te;
          var_clock_eff  = vid,BaseEff;
        }
      in
        incr i;
        res
    in
    let inlist_eff = List.map (to_var_info_eff SyntaxTreeCore.VarInput) lti in
    let outlist_eff = (i:=0;List.map (to_var_info_eff SyntaxTreeCore.VarOutput) lto) in
    let res = 
      {
        node_key_eff = id,sargs ;
        inlist_eff   = inlist_eff;
        outlist_eff  = outlist_eff;
        loclist_eff  = None;
        def_eff      = ExternEff;
        has_mem_eff  = (match has_mem with Some b -> b | None -> true);
        is_safe_eff  = true;
        is_polym_eff = 
(*           List.exists (fun vi -> Eff.is_polymorphic vi.var_type_eff) inlist_eff || *)
(*           List.exists (fun vi -> Eff.is_polymorphic vi.var_type_eff) outlist_eff *)
          !is_polymorphic
      }
    in 
      res

(* exported *)
let (f : op -> Lxm.t -> Eff.static_arg list -> typer) = 
  fun op lxm sargs ll ->
      match op with
        | IF_n  ->  (
            (* VERRUE 1 *)
            (* j'arrive pas a traiter le if de facon generique (pour l'instant...) 
               a cause du fait que le if peut renvoyer un tuple.
            *)
            match ll with
              | [[Bool_type_eff]; t; e] -> 
                  if t = e then t else 
                    (type_error (List.flatten [[Bool_type_eff]; t; e]) "bool*any*any")
              | x -> (arity_error x "3")
          )
        | (NOR_n | DIESE_n) -> 
            (* VERRUE 2 : cf XXX above: therefore i define an ad-hoc
               check for them.  *)
            let check_nary_iter acc ceff =
              match ceff with (Bool_type_eff) -> 
                acc | _ -> (type_error [ceff] "bool")
            in
              List.fold_left check_nary_iter () (List.flatten ll);
              [Bool_type_eff]
        | _ -> 
            (* general case *)
            let node_eff = make_node_exp_eff (Some false) op lxm sargs in
            let lti = List.map (fun v -> v.var_type_eff) node_eff.inlist_eff
            and lto = List.map (fun v -> v.var_type_eff) node_eff.outlist_eff in
            let l = List.flatten ll in
              if (List.length l <> List.length lti) then
                arity_error [l] (string_of_int (List.length lti))
              else
                match UnifyType.f lti l with
                  | Equal  -> lto
                  | Unif Any -> 
                      type_error2 
                        (LicDump.type_eff_list_to_string l) 
                        (LicDump.type_eff_list_to_string lti) 
                        "could not instanciate polymorphic type"
                  | Unif Overload -> 
                      type_error2 
                        (LicDump.type_eff_list_to_string l) 
                        (LicDump.type_eff_list_to_string lti) 
                        "could not instanciate overloaded type"

                  | Unif t -> 
                      List.map (subst_type t) lto

                  | Ko(str) -> 
                      type_error2 (LicDump.type_eff_list_to_string l) 
                        (LicDump.type_eff_list_to_string lti) str