Skip to content
Snippets Groups Projects
  • Erwan Jahier's avatar
    65c62005
    Unnest array iterator calls by modifying the Lic printer. · 65c62005
    Erwan Jahier authored
    The  idea  is  the  following:  each  time  a  nested  iterator  call
    (map<<map<<n,3>>,4>>) is  encountered, we  create a fresh  alias name
    (create_alias_name) ad we  add it in the node_alias_tbl.   At the end
    of the  compilation, LicDump.dump_node_alias is  called, which prints
    the definition of those node aliases.
    
    For example, the expression  "map<<map<<n,3>>,4>>" is printed like this:
    
        map<<_node_alias1, 4>>
    
    and later, the node alias is defined:
    
        node _node_alias1(x:int) returns(y:int); let y = map<<n,3>>(x); tel;
    65c62005
    History
    Unnest array iterator calls by modifying the Lic printer.
    Erwan Jahier authored
    The  idea  is  the  following:  each  time  a  nested  iterator  call
    (map<<map<<n,3>>,4>>) is  encountered, we  create a fresh  alias name
    (create_alias_name) ad we  add it in the node_alias_tbl.   At the end
    of the  compilation, LicDump.dump_node_alias is  called, which prints
    the definition of those node aliases.
    
    For example, the expression  "map<<map<<n,3>>,4>>" is printed like this:
    
        map<<_node_alias1, 4>>
    
    and later, the node alias is defined:
    
        node _node_alias1(x:int) returns(y:int); let y = map<<n,3>>(x); tel;
predefEvalType.ml 10.41 KiB
(** 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