CristalCaveGem » LustreC

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

(*                                                                  *)

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

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

(*                                                                  *)

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

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

(*  version 2.1.                                                    *)

(*                                                                  *)

(*  This file was originally from the Prelude compiler              *)

(*                                                                  *)

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

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

    unification. *)

let debug _fmt _args = ()

(* Format.eprintf "%a" *)

(* Though it shares similarities with the clock calculus module, no code is

   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 Lustre_types

open Corelang

(* TODO general remark: except in the add_vdecl, it seems to me that all the

   pairs (env, vd_env) should be replace with just env, since vd_env is never

   used and the env element is always extract with a fst *)

module type EXPR_TYPE_HUB = sig

  type type_expr

  val import : Types.Main.type_expr -> type_expr

  val export : type_expr -> Types.Main.type_expr

end

module Make

    (T : Types.S)

    (Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.type_expr) =

struct

  module TP = Type_predef.Make (T)

  include TP

  let pp_typing_env fmt env = Env.pp_env print_ty fmt env

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

  (* Generic functions: occurs, instantiate and generalize         *)

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

  (** [occurs tvar ty] returns true if the type variable [tvar] occurs in type

      [ty]. False otherwise. *)

  let rec occurs tvar ty =

    let ty = repr ty in

    match type_desc ty with

    | Tvar ->

      ty = tvar

    | Tarrow (t1, t2) ->

      occurs tvar t1 || occurs tvar t2

    | Ttuple tl ->

      List.exists (occurs tvar) tl

    | Tstruct fl ->

      List.exists (fun (_, t) -> occurs tvar t) fl

    | Tarray (_, t) | Tstatic (_, t) | Tclock t | Tlink t ->

      occurs tvar t

    | Tenum _ | Tconst _ | Tunivar | Tbasic _ ->

      false

  (* Generalize by side-effects *)

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

  let rec generalize ty =

    match type_desc ty with

    | Tvar ->

      (* No scopes, always generalize *)

      ty.tdesc <- Tunivar

    | Tarrow (t1, t2) ->

      generalize t1;

      generalize t2

    | Ttuple tl ->

      List.iter generalize tl

    | Tstruct fl ->

      List.iter (fun (_, t) -> generalize t) fl

    | Tstatic (d, t) | Tarray (d, t) ->

      Dimension.generalize d;

      generalize t

    | Tclock t | Tlink t ->

      generalize t

    | Tenum _ | Tconst _ | Tunivar | Tbasic _ ->

      ()

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

  let rec instantiate inst_vars inst_dim_vars ty =

    let ty = repr ty in

    match ty.tdesc with

    | Tenum _ | Tconst _ | Tvar | Tbasic _ ->

      ty

    | Tarrow (t1, t2) ->

      {

        ty with

        tdesc =

          Tarrow

            ( instantiate inst_vars inst_dim_vars t1,

              instantiate inst_vars inst_dim_vars t2 );

      }

    | Ttuple tlist ->

      {

        ty with

        tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist);

      }

    | Tstruct flist ->

      {

        ty with

        tdesc =

          Tstruct

            (List.map

               (fun (f, t) -> f, instantiate inst_vars inst_dim_vars t)

               flist);

      }

    | Tclock t ->

      { ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t) }

    | Tstatic (d, t) ->

      {

        ty with

        tdesc =

          Tstatic

            ( Dimension.instantiate inst_dim_vars d,

              instantiate inst_vars inst_dim_vars t );

      }

    | Tarray (d, t) ->

      {

        ty with

        tdesc =

          Tarray

            ( Dimension.instantiate inst_dim_vars d,

              instantiate inst_vars inst_dim_vars t );

      }

    | Tlink t ->

      (* should not happen *)

      { ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t) }

    | Tunivar -> (

      try List.assoc ty.tid !inst_vars

      with Not_found ->

        let var = new_var () in

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

        var)

  let basic_coretype_type t =

    if is_real_type t then Tydec_real

    else if is_int_type t then Tydec_int

    else if is_bool_type t then Tydec_bool

    else assert false

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

  let rec type_coretype type_dim cty =

    match (*get_repr_type*)

          cty with

    | Tydec_any ->

      new_var ()

    | Tydec_int ->

      type_int

    | Tydec_real ->

      (* Type_predef. *)

      type_real

    (* | Tydec_float -> Type_predef.type_real *)

    | Tydec_bool ->

      (* Type_predef. *)

      type_bool

    | Tydec_clock ty ->

      (* Type_predef. *)

      type_clock (type_coretype type_dim ty)

    | Tydec_const c ->

      (* Type_predef. *)

      type_const c

    | Tydec_enum tl ->

      (* Type_predef. *)

      type_enum tl

    | Tydec_struct fl ->

      (* Type_predef. *)

      type_struct (List.map (fun (f, ty) -> f, type_coretype type_dim ty) fl)

    | Tydec_array (d, ty) ->

      let d = Dimension.copy (ref []) d in

      type_dim d;

      (* Type_predef. *)

      type_array d (type_coretype type_dim ty)

  (* [coretype_type] is the reciprocal of [type_typecore] *)

  let rec coretype_type ty =

    match (repr ty).tdesc with

    | Tvar ->

      Tydec_any

    | Tbasic _ ->

      basic_coretype_type ty

    | Tconst c ->

      Tydec_const c

    | Tclock t ->

      Tydec_clock (coretype_type t)

    | Tenum tl ->

      Tydec_enum tl

    | Tstruct fl ->

      Tydec_struct (List.map (fun (f, t) -> f, coretype_type t) fl)

    | Tarray (d, t) ->

      Tydec_array (d, coretype_type t)

    | Tstatic (_, t) ->

      coretype_type t

    | _ ->

      assert false

  let get_coretype_definition tname =

    try

      let top = Hashtbl.find type_table (Tydec_const tname) in

      match top.top_decl_desc with

      | TypeDef tdef ->

        tdef.tydef_desc

      | _ ->

        assert false

    with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))

  let get_type_definition tname =

    type_coretype (fun _ -> ()) (get_coretype_definition tname)

  (* Equality on ground types only *)

  (* Should be used between local variables which must have a ground type *)

  let rec eq_ground t1 t2 =

    let t1 = repr t1 in

    let t2 = repr t2 in

    t1 == t2

    ||

    match t1.tdesc, t2.tdesc with

    | Tbasic t1, Tbasic t2 when t1 == t2 ->

      true

    | Tenum tl, Tenum tl' when tl == tl' ->

      true

    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->

      List.for_all2 eq_ground tl tl'

    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->

      List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'

    | Tconst t, _ ->

      let def_t = get_type_definition t in

      eq_ground def_t t2

    | _, Tconst t ->

      let def_t = get_type_definition t in

      eq_ground t1 def_t

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

      eq_ground t1 t1' && eq_ground t2 t2'

    | Tclock t1', Tclock t2' ->

      eq_ground t1' t2'

    | Tstatic (e1, t1'), Tstatic (e2, t2') | Tarray (e1, t1'), Tarray (e2, t2')

      ->

      Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'

    | _ ->

      false

  (** [unify t1 t2] unifies types [t1] and [t2] using standard destructive

      unification. Raises [Unify (t1,t2)] if the types are not unifiable. [t1]

      is a expected/formal/spec type, [t2] is a computed/real/implem type, so in

      case of unification error: expected type [t1], got type [t2]. If

      [sub]-typing is allowed, [t2] may be a subtype of [t1]. If [semi]

      unification is required, [t1] should furthermore be an instance of [t2]

      and constants are handled differently.*)

  let unify ?(sub = false) ?(semi = false) t1 t2 =

    let rec unif t1 t2 =

      let t1 = repr t1 in

      let t2 = repr t2 in

      if t1 == t2 then ()

      else

        match t1.tdesc, t2.tdesc with

        (* strictly subtyping cases first *)

        | _, Tclock t2 when sub && get_clock_base_type t1 = None ->

          unif t1 t2

        | _, Tstatic (_, t2) when sub && get_static_value t1 = None ->

          unif t1 t2

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

        | Tvar, Tvar ->

          if t1.tid < t2.tid then t2.tdesc <- Tlink t1 else t1.tdesc <- Tlink t2

        | Tvar, _ when (not semi) && not (occurs t1 t2) ->

          t1.tdesc <- Tlink t2

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

          t2.tdesc <- Tlink t1

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

          unif t2 t2';

          unif t1' t1

        | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->

          List.iter2 unif tl tl'

        | Ttuple [ t1 ], _ ->

          unif t1 t2

        | _, Ttuple [ t2 ] ->

          unif t1 t2

        | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->

          List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'

        | Tclock _, Tstatic _ | Tstatic _, Tclock _ ->

          raise (Unify (t1, t2))

        | Tclock t1', Tclock t2' ->

          unif t1' t2'

        (* | Tbasic t1, Tbasic t2 when t1 == t2 -> () *)

        | Tunivar, _ | _, Tunivar ->

          ()

        | Tconst t, _ ->

          let def_t = get_type_definition t in

          unif def_t t2

        | _, Tconst t ->

          let def_t = get_type_definition t in

          unif t1 def_t

        | Tenum tl, Tenum tl' when tl == tl' ->

          ()

        | Tstatic (e1, t1'), Tstatic (e2, t2')

        | Tarray (e1, t1'), Tarray (e2, t2') ->

          let eval_const =

            if semi then fun c ->

              Some (Dimension.mkdim_ident Location.dummy_loc c)

            else fun _ -> None

          in

          unif t1' t2';

          Dimension.eval Basic_library.eval_dim_env eval_const e1;

          Dimension.eval Basic_library.eval_dim_env eval_const e2;

          Dimension.unify ~semi e1 e2

        (* Special cases for machine_types. Rules to unify static types infered

           for numerical constants with non static ones for variables with

           possible machine types *)

        | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 ->

          BasicT.unify bt1 bt2

        | _, _ ->

          raise (Unify (t1, t2))

    in

    unif t1 t2

  (* Expected type ty1, got type ty2 *)

  let try_unify ?(sub = false) ?(semi = false) ty1 ty2 loc =

    try unify ~sub ~semi ty1 ty2 with

    | Unify (t1', t2') ->

      raise (Error (loc, Type_clash (ty1, ty2)))

    | Dimension.Unify _ ->

      raise (Error (loc, Type_clash (ty1, ty2)))

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

  (* Typing function for each basic AST construct *)

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

  let rec type_struct_const_field ?(is_annot = false) loc (label, c) =

    if Hashtbl.mem field_table label then (

      let tydef = Hashtbl.find field_table label in

      let tydec = (typedef_of_top tydef).tydef_desc in

      let tydec_struct = get_struct_type_fields tydec in

      let ty_label =

        type_coretype (fun _ -> ()) (List.assoc label tydec_struct)

      in

      try_unify ty_label (type_const ~is_annot loc c) loc;

      type_coretype (fun _ -> ()) tydec)

    else raise (Error (loc, Unbound_value ("struct field " ^ label)))

  and type_const ?(is_annot = false) loc c =

    match c with

    | Const_int _ ->

      (* Type_predef. *)

      type_int

    | Const_real _ ->

      (* Type_predef. *)

      type_real

    | Const_array ca ->

      let d = Dimension.mkdim_int loc (List.length ca) in

      let ty = new_var () in

      List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;

      (* Type_predef. *)

      type_array d ty

    | Const_tag t ->

      if Hashtbl.mem tag_table t then

        let tydef = typedef_of_top (Hashtbl.find tag_table t) in

        let tydec =

          if is_user_type tydef.tydef_desc then Tydec_const tydef.tydef_id

          else tydef.tydef_desc

        in

        type_coretype (fun _ -> ()) tydec

      else raise (Error (loc, Unbound_value ("enum tag " ^ t)))

    | Const_struct fl -> (

      let ty_struct = new_var () in

      let used =

        List.fold_left

          (fun acc (l, c) ->

            if List.mem l acc then

              raise (Error (loc, Already_bound ("struct field " ^ l)))

            else

              try_unify ty_struct

                (type_struct_const_field ~is_annot loc (l, c))

                loc;

            l :: acc)

          [] fl

      in

      try

        let total =

          List.map fst (get_struct_type_fields (coretype_type ty_struct))

        in

        (* List.iter (fun l -> Format.eprintf "total: %s@." l) total; List.iter

           (fun l -> Format.eprintf "used: %s@." l) used; *)

        let undef = List.find (fun l -> not (List.mem l used)) total in

        raise (Error (loc, Unbound_value ("struct field " ^ undef)))

      with Not_found -> ty_struct)

    | Const_string s | Const_modeid s ->

      if is_annot then (* Type_predef. *)

        type_string

      else (

        Format.eprintf "Typing string %s outisde of annot scope@.@?" s;

        assert false (* string datatype should only appear in annotations *))

  (* The following typing functions take as parameter an environment [env] and

     whether the element being typed is expected to be constant [const]. [env]

     is a pair composed of: - a map from ident to type, associating to each

     ident, i.e. variables, constants and (imported) nodes, its type including

     whether it is constant or not. This latter information helps in checking

     constant propagation policy in Lustre. - a vdecl list, in order to modify

     types of declared variables that are later discovered to be clocks during

     the typing process. *)

  let check_constant loc const_expected const_real =

    if const_expected && not const_real then raise (Error (loc, Not_a_constant))

  let rec type_add_const env const arg targ =

    (*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg

      Types.print_ty targ;*)

    if const then (

      let d =

        if is_dimension_type targ then dimension_of_expr arg

        else Dimension.mkdim_var ()

      in

      let eval_const id =

        (* Types. *)

        get_static_value (Env.lookup_value (fst env) id)

      in

      Dimension.eval Basic_library.eval_dim_env eval_const d;

      let real_static_type =

        (* Type_predef. *)

        type_static d ((* Types. *)

                       dynamic_type targ)

      in

      (match (* Types. *)

             get_static_value targ with

      | None ->

        ()

      | Some _ ->

        try_unify targ real_static_type arg.expr_loc);

      real_static_type)

    else targ

  (* emulates a subtyping relation between types t and (d : t), used during node

     applications and assignments *)

  and type_subtyping_arg env in_main ?(sub = true) const real_arg formal_type =

    let loc = real_arg.expr_loc in

    let const =

      const

      || (* Types. *)

      get_static_value formal_type <> None

    in

    let real_type =

      type_add_const env const real_arg (type_expr env in_main const real_arg)

    in

    (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const

      Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty

      formal_type;*)

    try_unify ~sub formal_type real_type loc

  (* typing an application implies: - checking that const formal parameters

     match real const (maybe symbolic) arguments - checking type adequation

     between formal and real arguments An application may embed an

     homomorphic/internal function, in which case we need to split it in many

     calls *)

  and type_appl env in_main loc const f args =

    let targs = List.map (type_expr env in_main const) args in

    if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs

    then

      try

        let targs = Utils.transpose_list (List.map type_list_of_type targs) in

        (* Types. *)

        type_of_type_list

          (List.map (type_simple_call env in_main loc const f) targs)

      with Utils.TransposeError (l, l') ->

        raise (Error (loc, WrongMorphism (l, l')))

    else type_dependent_call env in_main loc const f (List.combine args targs)

  (* type a call with possible dependent types. [targs] is here a list of

     (argument, type) pairs. *)

  and type_dependent_call env in_main loc const f targs =

    (* Format.eprintf "Typing.type_dependent_call %s@." f; *)

    let tins, touts = new_var (), new_var () in

    (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)

    let tfun =

      (* Type_predef. *)

      type_arrow tins touts

    in

    (* Format.eprintf "fun=%a@." print_ty tfun; *)

    type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

    (* Format.eprintf "type subtyping@."; *)

    let tins = type_list_of_type tins in

    if List.length targs <> List.length tins then

      raise (Error (loc, WrongArity (List.length tins, List.length targs)))

    else (

      List.iter2

        (fun (a, t) ti ->

          let t' =

            type_add_const env

              (const

              || (* Types. *)

              get_static_value ti <> None)

              a t

          in

          (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti

             print_ty t' print_ty touts; *)

          try_unify ~sub:true ti t' a.expr_loc

          (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti

             print_ty t' print_ty touts; *))

        targs tins;

      touts)

  (* type a simple call without dependent types but possible homomorphic

     extension. [targs] is here a list of arguments' types. *)

  and type_simple_call env in_main loc const f targs =

    let tins, touts = new_var (), new_var () in

    let tfun =

      (* Type_predef. *)

      type_arrow tins touts

    in

    type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

    (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty

      (type_of_type_list targs);*)

    try_unify ~sub:true tins (type_of_type_list targs) loc;

    touts

  (** [type_expr env in_main expr] types expression [expr] in environment [env],

      expecting it to be [const] or not. *)

  and type_expr ?(is_annot = false) env in_main const expr =

    let resulting_ty =

      match expr.expr_desc with

      | Expr_const c ->

        let ty = type_const ~is_annot expr.expr_loc c in

        let ty =

          (* Type_predef. *)

          type_static (Dimension.mkdim_var ()) ty

        in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_ident v ->

        let tyv =

          try Env.lookup_value (fst env) v

          with Not_found ->

            Format.eprintf

              "Failure in typing expr %a. Not in typing environement@."

              Printers.pp_expr expr;

            raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))

        in

        let ty = instantiate (ref []) (ref []) tyv in

        let ty' =

          if const then

            (* Type_predef. *)

            type_static (Dimension.mkdim_var ()) (new_var ())

          else new_var ()

        in

        try_unify ty ty' expr.expr_loc;

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_array elist ->

        let ty_elt = new_var () in

        List.iter

          (fun e ->

            try_unify ty_elt

              (type_appl env in_main expr.expr_loc const "uminus" [ e ])

              e.expr_loc)

          elist;

        let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in

        let ty =

          (* Type_predef. *)

          type_array d ty_elt

        in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_access (e1, d) ->

        type_subtyping_arg env in_main false

          (* not necessary a constant *)

          (expr_of_dimension d)

          (* Type_predef. *)

          type_int;

        let ty_elt = new_var () in

        let d = Dimension.mkdim_var () in

        type_subtyping_arg env in_main const e1

          ((* Type_predef. *)

           type_array d ty_elt);

        expr.expr_type <- Expr_type_hub.export ty_elt;

        ty_elt

      | Expr_power (e1, d) ->

        let eval_const id =

          (* Types. *)

          get_static_value (Env.lookup_value (fst env) id)

        in

        type_subtyping_arg env in_main true (expr_of_dimension d)

          (* Type_predef. *)

          type_int;

        Dimension.eval Basic_library.eval_dim_env eval_const d;

        let ty_elt =

          type_appl env in_main expr.expr_loc const "uminus" [ e1 ]

        in

        let ty =

          (* Type_predef. *)

          type_array d ty_elt

        in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_tuple elist ->

        let ty =

          new_ty

            (Ttuple (List.map (type_expr ~is_annot env in_main const) elist))

        in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_ite (c, t, e) ->

        type_subtyping_arg env in_main const c (* Type_predef. *) type_bool;

        let ty = type_appl env in_main expr.expr_loc const "+" [ t; e ] in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_appl (id, args, r) ->

        (* application of non internal function is not legal in a constant

           expression *)

        (match r with

        | None ->

          ()

        | Some c ->

          check_constant expr.expr_loc const false;

          type_subtyping_arg env in_main const c (* Type_predef. *) type_bool);

        let args_list = expr_list_of_expr args in

        let touts = type_appl env in_main expr.expr_loc const id args_list in

        let targs =

          new_ty

            (Ttuple

               (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list))

        in

        args.expr_type <- Expr_type_hub.export targs;

        expr.expr_type <- Expr_type_hub.export touts;

        touts

      | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->

        (* fby/arrow is not legal in a constant expression *)

        check_constant expr.expr_loc const false;

        let ty = type_appl env in_main expr.expr_loc const "+" [ e1; e2 ] in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_pre e ->

        (* pre is not legal in a constant expression *)

        check_constant expr.expr_loc const false;

        let ty = type_appl env in_main expr.expr_loc const "uminus" [ e ] in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_when (e1, c, l) ->

        (* when is not legal in a constant expression *)

        check_constant expr.expr_loc const false;

        let typ_l =

          (* Type_predef. *)

          type_clock (type_const ~is_annot expr.expr_loc (Const_tag l))

        in

        let expr_c = expr_of_ident c expr.expr_loc in

        type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

        let ty = type_appl env in_main expr.expr_loc const "uminus" [ e1 ] in

        expr.expr_type <- Expr_type_hub.export ty;

        ty

      | Expr_merge (c, hl) ->

        (* merge is not legal in a constant expression *)

        check_constant expr.expr_loc const false;

        let typ_in, typ_out =

          type_branches env in_main expr.expr_loc const hl

        in

        let expr_c = expr_of_ident c expr.expr_loc in

        let typ_l =

          (* Type_predef. *)

          type_clock typ_in

        in

        type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

        expr.expr_type <- Expr_type_hub.export typ_out;

        typ_out

    in

    Log.report ~level:3 (fun fmt ->

        Format.fprintf fmt "Type of expr %a: %a@ " Printers.pp_expr expr

          (* Types. *)

          print_ty resulting_ty);

    resulting_ty

  and type_branches ?(is_annot = false) env in_main loc const hl =

    let typ_in = new_var () in

    let typ_out = new_var () in

    try

      let used_labels =

        List.fold_left

          (fun accu (t, h) ->

            unify typ_in (type_const ~is_annot loc (Const_tag t));

            type_subtyping_arg env in_main const h typ_out;

            if List.mem t accu then raise (Error (loc, Already_bound t))

            else t :: accu)

          [] hl

      in

      let type_labels = get_enum_type_tags (coretype_type typ_in) in

      if List.sort compare used_labels <> List.sort compare type_labels then

        let unbound_tag =

          List.find (fun t -> not (List.mem t used_labels)) type_labels

        in

        raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))

      else typ_in, typ_out

    with Unify (t1, t2) -> raise (Error (loc, Type_clash (t1, t2)))

  (* Eexpr are always in annotations. TODO: add the quantifiers variables to the

     env *)

  let type_eexpr env eexpr =

    type_expr ~is_annot:true env false (* not in main *) false (* not a const *)

      eexpr.eexpr_qfexpr

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

  let type_eq env in_main undefined_vars eq =

    (*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)

    (* Check undefined variables, type lhs *)

    let expr_lhs =

      expr_of_expr_list eq.eq_loc

        (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)

    in

    let ty_lhs = type_expr env in_main false expr_lhs in

    (* Check multiple variable definitions *)

    let define_var id uvars =

      if ISet.mem id uvars then ISet.remove id uvars

      else raise (Error (eq.eq_loc, Already_defined id))

    in

    (* check assignment of declared constant, assignment of clock *)

    let ty_lhs =

      type_of_type_list

        (List.map2

           (fun ty id ->

             if get_static_value ty <> None then

               raise (Error (eq.eq_loc, Assigned_constant id))

             else match get_clock_base_type ty with None -> ty | Some ty -> ty)

           (type_list_of_type ty_lhs) eq.eq_lhs)

    in

    let undefined_vars =

      List.fold_left

        (fun uvars v -> define_var v uvars)

        undefined_vars eq.eq_lhs

    in

    (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be

       assigned to a (always non-constant) lhs variable *)

    type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

    undefined_vars

  (* [type_coreclock env ck id loc] types the type clock declaration [ck] in

     environment [env] *)

  let type_coreclock env ck id loc =

    match ck.ck_dec_desc with

    | Ckdec_any ->

      ()

    | Ckdec_bool cl ->

      let dummy_id_expr = expr_of_ident id loc in

      let when_expr =

        List.fold_left

          (fun expr (x, l) ->

            {

              expr_tag = new_tag ();

              expr_desc = Expr_when (expr, x, l);

              expr_type = Types.Main.new_var ();

              expr_clock = Clocks.new_var true;

              expr_delay = Delay.new_var ();

              expr_loc = loc;

              expr_annot = None;

            })

          dummy_id_expr cl

      in

      ignore (type_expr env false false when_expr)

  let rec check_type_declaration loc cty =

    match cty with

    | Tydec_clock ty | Tydec_array (_, ty) ->

      check_type_declaration loc ty

    | Tydec_const tname ->

      (* Format.eprintf "TABLE: %a@." print_type_table (); *)

      if not (Hashtbl.mem type_table cty) then

        raise (Error (loc, Unbound_type tname))

    | _ ->

      ()

  let type_var_decl vd_env env vdecl =

    (*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl

      Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)

    check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

    let eval_const id =

      (* Types. *)

      get_static_value (Env.lookup_value env id)

    in

    let type_dim d =

      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d)

        (* Type_predef. *)

        type_int;

      Dimension.eval Basic_library.eval_dim_env eval_const d

    in

    let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in