(** Time-stamp: <modified the 22/08/2008 (at 15:57) by Erwan Jahier> *)
open Predef
open SyntaxTreeCore
open CompiledData
open Lxm
open Errors
open UnifyType
(* exported *)
type typer = type_eff Predef.evaluator
(* exported *)
exception EvalType_error of string
(* exported *)
let (type_error : type_eff list -> string -> 'a) =
fun tel expect ->
let str_l = List.map LicDump.string_of_type_eff 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: var_info_eff list -> int -> (Ident.t * type_eff) 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:static_arg_eff list -> node_exp_eff * int)=
fun sargs ->
match sargs with
| [NodeStaticArgEff(_,n);ConstStaticArgEff(_,Int_const_eff c)] -> n,c
| _ -> assert false
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,c) = get_node_and_constant sargs in
let lti = type_to_array_type n.inlist_eff c in
let lto = type_to_array_type n.outlist_eff c in
(lti, lto)
let get_id_type vi = vi.var_name_eff, vi.var_type_eff
let (fillred_profile : Lxm.t -> CompiledData.static_arg_eff list ->
(Ident.t * type_eff) list * (Ident.t * type_eff) 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,c) = get_node_and_constant sargs in
let _ = assert(n.inlist_eff <> [] && n.outlist_eff <> []) in
let lti = (get_id_type (List.hd n.inlist_eff))::
type_to_array_type (List.tl n.inlist_eff) c in
let lto = (get_id_type (List.hd n.outlist_eff))::
type_to_array_type (List.tl n.outlist_eff) c in
let (id1, t1) = List.hd lti and (id2, t2) = List.hd lto in
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))
(* 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 -> static_arg_eff 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 * type_eff) list * (Ident.t * type_eff) list
let (op2profile : Predef.op -> Lxm.t -> static_arg_eff list -> node_profile) =
fun op lxm sargs -> 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...
*)
(* exported *)
let (make_node_exp_eff :
bool option -> op -> Lxm.t -> static_arg_eff list -> node_exp_eff) =
fun has_mem op lxm sargs ->
let id = Ident.make_long
(Ident.pack_name_of_string "Lustre") (Ident.of_string (Predef.op2string_long op))
in
let (lti,lto) = op2profile op lxm sargs in
let i = ref 0 in
let to_var_info_eff nature (id, te) =
let res =
{
var_name_eff = id;
var_nature_eff = nature;
var_number_eff = !i;
var_type_eff = te;
var_clock_eff = BaseEff;
}
in
incr i;
res
in
{
node_key_eff = id,sargs ;
inlist_eff = List.map (to_var_info_eff VarInput) lti;
outlist_eff = (i:=0; List.map (to_var_info_eff VarOutput) lto);
loclist_eff = None;
def_eff = ExternEff;
has_mem_eff = (match has_mem with Some b -> b | None -> true);
is_safe_eff = true;
}
(* exported *)
let (f : op -> Lxm.t -> CompiledData.static_arg_eff 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 rec (subst_type : type_eff -> type_eff -> type_eff) =
fun t teff -> match teff with
(* substitutes [t] in [teff] *)
| Bool_type_eff -> Bool_type_eff
| Int_type_eff -> Int_type_eff
| Real_type_eff -> Real_type_eff
| External_type_eff l -> External_type_eff l
| Enum_type_eff(l,el) -> Enum_type_eff(l,el)
| Array_type_eff(teff,i) -> Array_type_eff(subst_type t teff, i)
| Struct_type_eff(l, fl) ->
Struct_type_eff(
l,
List.map
(fun (id,(teff,copt)) -> (id,(subst_type t teff,copt)))
fl)
| Any
| Overload -> t
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