CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

(** Main typing module. Classic inference algorithm with destructive

    unification. *)

   shared. Simple environments, very limited identifier scoping, no identifier

   redefinition allowed. *)

open Utils

(* Yes, opening both modules is dirty as some type names will be overwritten,

   yet this makes notations far lighter.*)

open Init

open Format

    [ty]. False otherwise. *)

  let ty = repr ty in

  match ty.tdesc with

    ty = tvar

  | Ilink t ->

    occurs tvar t

  | Isucc t ->

    occurs tvar t

  | Iunivar ->

    false

(* Generalize by side-effects *)

(** Promote monomorphic type variables to polymorphic type variables. *)

  match ty.tdesc with

  | Ivar ->

    ty.idesc <- Iunivar

  | Iarrow (t1, t2) ->

    generalize t1;

    generalize t2

  | Tunivar ->

    ()

(** Downgrade polymorphic type variables to monomorphic type variables *)

let rec instanciate inst_vars ty =

  let ty = repr ty in

  match ty.idesc with

    ty

  | Iarrow (t1, t2) ->

    {

      ty with

      idesc = Iarrow (instanciate inst_vars t1, instanciate inst_vars t2);

    }

    { ty with idesc = Isucc (instanciate inst_vars t) }

    { ty with idesc = Ilink (instanciate inst_vars t) }

  | Iunivar -> (

    try List.assoc ty.iid !inst_vars

    with Not_found ->

      let var = new_var () in

      inst_vars := (ty.iid, var) :: !inst_vars;

      var)

    types are not unifiable.*)

(* Standard destructive unification *)

(* may loop for omega types *)

let rec unify t1 t2 =

  let t1 = repr t1 in

  let t2 = repr t2 in

    (* No type abbreviations resolution for now *)

    (* This case is not mandory but will keep "older" types *)

    | Ivar, _ when not (occurs t1 t2) ->

      t1.idesc <- Ilink t2

    | _, Ivar when not (occurs t2 t1) ->

      t2.idesc <- Ilink t1

    | Isucc t1, Isucc t1' ->

      unify t1 t1'

    | Iarrow (t1, t2), Iarrow (t1', t2') ->

      unify t1 t1';

      unify t2 t2'

      else List.iter2 unify tlist1 tlist2

    | Iunivar, _ | _, Iunivar ->

      ()

    | _, _ ->

      raise (Unify (t1, t2))

let rec init_expect env in_main expr ty =

  let texpr = init_expr env in_main expr in

  with Unify (t1, t2) -> raise (Error (expr.expr_loc, Init_clash (t1, t2)))

  match expr.expr_desc with

  | Expr_const c ->

    expr.expr_init <- ty;

    ty

      try Env.lookup_value env v

      with Not_found -> raise (Error (expr.expr_loc, Unbound_value v))

    in

    let ty = instanciate (ref []) tyv in

    expr.expr_init <- ty;

    ty

    expr.expr_init <- ty;

    ty

    (match r with

      ()

    | Some x ->

      let expr_x = expr_of_ident x expr.expr_loc in

      init_expect env in_main expr_x Init_predef.init_zero);

    let tfun = type_ident env in_main id expr.expr_loc in

    let tins, touts = split_arrow tfun in

    type_expect env in_main args tins;

    expr.expr_type <- touts;

    touts

  | Expr_arrow (e1, e2) ->

    let ty = type_expr env in_main e1 in

    type_expect env in_main e2 ty;

    expr.expr_type <- ty;

    ty

  | Expr_fby (init, e) ->

    let ty = type_of_const init in

    type_expect env in_main e ty;

    expr.expr_type <- ty;

    ty

  | Expr_concat (hd, e) ->

    let ty = type_of_const hd in

    type_expect env in_main e ty;

    expr.expr_type <- ty;

    ty

    expr.expr_type <- ty;

    ty

    expr.expr_type <- ty;

    ty

  | Expr_when (e1, c) | Expr_whennot (e1, c) ->

    let expr_c = expr_of_ident c expr.expr_loc in

    type_expect env in_main expr_c Type_predef.type_bool;

    let tlarg = type_expr env in_main e1 in

    expr.expr_type <- tlarg;

    tlarg

  | Expr_merge (c, e2, e3) ->

    let expr_c = expr_of_ident c expr.expr_loc in

    type_expect env in_main expr_c Type_predef.type_bool;

    let te2 = type_expr env in_main e2 in

    type_expect env in_main e3 te2;

    expr.expr_type <- te2;

    te2

  | Expr_uclock (e, k) | Expr_dclock (e, k) ->

    let ty = type_expr env in_main e in

    expr.expr_type <- ty;

    ty

  | Expr_phclock (e, q) ->

    let ty = type_expr env in_main e in

    expr.expr_type <- ty;

    ty

(** [type_eq env eq] types equation [eq] in environment [env] *)

let type_eq env in_main undefined_vars eq =

  (* Check multiple variable definitions *)

  let define_var id uvars =

    try

  let undefined_vars =

  in

  let get_value_type id =

    with Not_found -> raise (Error (eq.eq_loc, Unbound_value id))

  let tyl_lhs = List.map get_value_type eq.eq_lhs in

  let ty_lhs = type_of_type_list tyl_lhs in

  undefined_vars

(* [type_coretype cty] types the type declaration [cty] *)

let type_coretype cty =

  match cty with

    new_var ()

  | Tydec_int ->

    Type_predef.type_int

  | Tydec_real ->

    Type_predef.type_real

  | Tydec_float ->

    Type_predef.type_real

  | Tydec_bool ->

    Type_predef.type_bool

  | Tydec_clock ->

    Type_predef.type_clock

   environment [env] *)

  match ck.ck_dec_desc with

    ()

    let when_expr =

      List.fold_left

        (fun expr c ->

          match c with

          | Wtrue id ->

            {

              expr_tag = new_tag ();

              expr_desc = Expr_when (expr, id);

              expr_type = new_var ();

              expr_clock = Clocks.new_var true;

              expr_loc = loc;

            }

          | Wfalse id ->

            {

              expr_tag = new_tag ();

              expr_desc = Expr_whennot (expr, id);

              expr_type = new_var ();

              expr_clock = Clocks.new_var true;

              expr_loc = loc;

            })

        dummy_id_expr cl

    in

    ignore (type_expr env false when_expr)

let type_var_decl env vdecl =

    raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))

    let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in

    let new_env = Env.add_value env vdecl.var_id ty in

    type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;

    vdecl.var_type <- ty;

    new_env

let type_of_vlist vars =

  let tyl = List.map (fun v -> v.var_type) vars in

  type_of_type_list tyl

(** [type_node env nd loc] types node [nd] in environment env. The location is

    used for error reports. *)

  let is_main = nd.node_id = !Options.main_node in

  let delta_env = type_var_decl_list IMap.empty nd.node_inputs in

  let delta_env = type_var_decl_list delta_env nd.node_outputs in

  let delta_env = type_var_decl_list delta_env nd.node_locals in

  let new_env = Env.overwrite env delta_env in

  let undefined_vars_init =

    List.fold_left

      (fun uvs v -> IMap.add v.var_id () uvs)

      (nd.node_outputs @ nd.node_locals)

  in

    List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs

  in

  (* check that table is empty *)

    raise (Error (loc, Undefined_var undefined_vars));

  let ty_outs = type_of_vlist nd.node_outputs in

  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)

  nd.node_type <- ty_node;

  Env.add_value env nd.node_id ty_node

let type_imported_node env nd loc =

  let new_env = type_var_decl_list env nd.nodei_inputs in

  let ty_outs = type_of_vlist nd.nodei_outputs in

  let new_env = Env.add_value env nd.nodei_id ty_node in

  nd.nodei_type <- ty_node;

  new_env

let type_top_decl env decl =

  match decl.top_decl_desc with

    type_node env nd decl.top_decl_loc

  | SensorDecl _ | ActuatorDecl _ | Consts _ ->

    env

let type_top_consts env decl =

  match decl.top_decl_desc with

    List.fold_left

      (fun env (id, c) ->

        let ty = type_of_const c in

        Env.add_value env id ty)

      env clist

  | Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ ->

    env

let type_prog env decls =

  let new_env = List.fold_left type_top_consts env decls in

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)