CristalCaveGem » LustreC

(*                                                                  *)

(*                                                                  *)

(** Types definitions and a few utility functions on types. *)

module type BASIC_TYPES = sig

  val pp : Format.formatter -> t -> unit

  val pp_c : Format.formatter -> t -> unit

  val is_scalar_type : t -> bool

  val is_numeric_type : t -> bool

  val is_int_type : t -> bool

  val is_real_type : t -> bool

  val is_bool_type : t -> bool

  val is_dimension_type : t -> bool

  val type_int_builder : t

  val type_real_builder : t

  val type_bool_builder : t

  val type_string_builder : t

  val unify : t -> t -> unit

  val is_unifiable : t -> t -> bool

module Basic = struct

  type t = Tstring | Tint | Treal | Tbool | Trat

  (* Actually unused for now. Only place where it can appear is in a clock

     declaration *)

      fprintf fmt "int"

      fprintf fmt "real"

      fprintf fmt "string"

      fprintf fmt "bool"

      fprintf fmt "rat"

  let is_scalar_type t =

    match t with Tbool | Tint | Treal -> true | _ -> false

  let is_numeric_type t = match t with Tint | Treal -> true | _ -> false

  let is_dimension_type t = match t with Tint | Tbool -> true | _ -> false

module Make (BasicT : BASIC_TYPES) = struct

  type type_expr = { mutable tdesc : type_desc; tid : int }

    | Tconst of ident

    (* type constant *)

    | Tclock of type_expr

    (* A type expression explicitely tagged as carrying a clock *)

    | Tstatic of dim_expr * type_expr

    (* a type carried by a dimension expression *)

    | Tlink of type_expr

    (* During unification, make links instead of substitutions *)

    | Tvar

    (* Monomorphic type variable *)

    | Tunivar

  (* Polymorphic type variable *)

  (* | Tclock of type_expr (\* A type expression explicitely tagged as carrying

     a clock *\) *)

  (* | Tstatic of dim_expr * type_expr (\* a type carried by a dimension

     expression *\) *)

  (* | Tlink of type_expr (\* During unification, make links instead of

     substitutions *\) *)

    | Unbound_value of ident

  exception Unify of type_expr * type_expr

  exception Error of Location.t * error

  let mk_basic t = Tbasic t

  (* Pretty-print*)

  open Format

  let rec print_struct_ty_field pp_basic fmt (label, ty) =

    fprintf fmt "%a : %a" pp_print_string label (print_ty_param pp_basic) ty

  and print_ty_param pp_basic fmt ty =

    let print_ty = print_ty_param pp_basic in

    match ty.tdesc with

    | Tvar ->

      fprintf fmt "_%s" (name_of_type ty.tid)

    | Tbasic t ->

      pp_basic fmt t

    | Tclock t ->

      fprintf fmt "%a%s" print_ty t

        (if !Options.kind2_print then "" else " clock")

    | Tstatic (_, t) ->

      print_ty fmt t

    (* fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t *)

    | Tconst t ->

      fprintf fmt "%s" t

    | Tarrow (ty1, ty2) ->

      fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2

    | Ttuple tylist ->

      fprintf fmt "(%a)" (Utils.fprintf_list ~sep:" * " print_ty) tylist

    | Tenum taglist ->

      fprintf fmt "enum {%a }"

        (Utils.fprintf_list ~sep:", " pp_print_string)

        taglist

    | Tstruct fieldlist ->

      fprintf fmt "struct {%a }"

        (Utils.fprintf_list ~sep:"; " (print_struct_ty_field pp_basic))

        fieldlist

    | Tarray (e, ty) ->

      fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e

    | Tlink ty ->

      print_ty fmt ty

    | Tunivar ->

      fprintf fmt "'%s" (name_of_type ty.tid)

  let print_ty = print_ty_param BasicT.pp

  let rec print_node_struct_ty_field fmt (label, ty) =

    fprintf fmt "%a : %a" pp_print_string label print_node_ty ty

  and print_node_ty fmt ty =

    match ty.tdesc with

    | Tvar ->

      (*Format.eprintf "DEBUG:Types.print_node@.";*)

      fprintf fmt "_%s" (name_of_type ty.tid)

    | Tbasic t ->

      BasicT.pp fmt t

    | Tclock t ->

      fprintf fmt "%a%s" print_node_ty t

        (if !Options.kind2_print then "" else " clock")

    | Tstatic (_, t) ->

      fprintf fmt "%a" print_node_ty t

    | Tconst t ->

      fprintf fmt "%s" t

    | Tarrow (ty1, ty2) ->

      fprintf fmt "%a -> %a" print_node_ty ty1 print_node_ty ty2

    | Ttuple tylist ->

      fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"*" print_node_ty) tylist

    | Tenum taglist ->

      fprintf fmt "enum {%a }"

        (Utils.fprintf_list ~sep:", " pp_print_string)

        taglist

    | Tstruct fieldlist ->

      fprintf fmt "struct {%a }"

        (Utils.fprintf_list ~sep:"; " print_node_struct_ty_field)

        fieldlist

    | Tarray (e, ty) ->

      fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e

    | Tlink ty ->

    | Tunivar ->

      fprintf fmt "'%s" (name_of_type ty.tid)

  let pp_error fmt = function

    | Unbound_value id ->

      fprintf fmt "Unknown value %s@." id

    | Unbound_type id ->

      fprintf fmt "Unknown type %s@." id

    | Already_bound id ->

      fprintf fmt "%s is already declared@." id

    | Already_defined id ->

      fprintf fmt "Multiple definitions of variable %s@." id

    | Not_a_constant ->

      fprintf fmt "This expression is not a constant@."

    | Assigned_constant id ->

      fprintf fmt "The constant %s cannot be assigned@." id

    | Not_a_dimension ->

      fprintf fmt "This expression is not a valid dimension@."

    | WrongArity (ar1, ar2) ->

      fprintf fmt "Expecting %d argument(s), found %d@." ar1 ar2

    | WrongMorphism (ar1, ar2) ->

      fprintf fmt

        "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2

    | Type_mismatch id ->

      fprintf fmt "Definition and declaration of type %s don't agree@." id

    | Undefined_var vset ->

      fprintf fmt "No definition provided for variable(s): %a@."

        (Utils.fprintf_list ~sep:"," pp_print_string)

        (ISet.elements vset)

    | Declared_but_undefined id ->

      fprintf fmt "%s is declared but not defined@." id

    | Type_clash (ty1, ty2) ->

      fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2

    | Poly_imported_node _ ->

      fprintf fmt "Imported nodes cannot have a polymorphic type@."

  let new_id = ref (-1)

  let rec bottom = { tdesc = Tlink bottom; tid = -666 }

  let new_ty desc =

    incr new_id;

    { tdesc = desc; tid = !new_id }

  let new_var () = new_ty Tvar

  let new_univar () = new_ty Tunivar

  let rec repr = function { tdesc = Tlink t'; _ } -> repr t' | t -> t

  let get_static_value ty =

    match (repr ty).tdesc with Tstatic (d, _) -> Some d | _ -> None

  let get_field_type ty label =

    match (repr ty).tdesc with

    | Tstruct fl -> (

      try Some (List.assoc label fl) with Not_found -> None)

    | _ ->

      None

  let is_static_type ty =

    match (repr ty).tdesc with Tstatic _ -> true | _ -> false

  let rec is_scalar_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      is_scalar_type ty

    | Tbasic t ->

      BasicT.is_scalar_type t

    | _ ->

      false

  let rec is_numeric_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      is_numeric_type ty

    | Tbasic t ->

      BasicT.is_numeric_type t

    | _ ->

      false

  let rec is_real_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      is_real_type ty

    | Tbasic t ->

      BasicT.is_real_type t

    | _ ->

      false

  let rec is_int_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      is_int_type ty

    | Tbasic t ->

      BasicT.is_int_type t

    | _ ->

      false

  let rec is_bool_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      is_bool_type ty

    | Tbasic t ->

      BasicT.is_bool_type t

    | _ ->

      false

  let rec is_const_type ty c =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      is_const_type ty c

    | Tconst c' ->

      c = c'

    | _ ->

      false

  let get_clock_base_type ty =

    match (repr ty).tdesc with Tclock ty -> Some ty | _ -> None

  let unclock_type ty =

    let ty = repr ty in

    match ty.tdesc with Tclock ty' -> ty' | _ -> ty

  let rec is_dimension_type ty =

    match (repr ty).tdesc with

    | Tbasic t ->

      BasicT.is_dimension_type t

    | Tclock ty' | Tstatic (_, ty') ->

      is_dimension_type ty'

    | _ ->

      false

  let dynamic_type ty =

    let ty = repr ty in

    match ty.tdesc with Tstatic (_, ty') -> ty' | _ -> ty

  let is_tuple_type ty =

    match (repr ty).tdesc with Ttuple _ -> true | _ -> false

  let map_tuple_type f ty =

    let ty = dynamic_type ty in

    match ty.tdesc with

    | Ttuple ty_list ->

      { ty with tdesc = Ttuple (List.map f ty_list) }

    | _ ->

      f ty

  let rec is_struct_type ty =

    match (repr ty).tdesc with

    | Tstruct _ ->

      true

    | Tstatic (_, ty') ->

      is_struct_type ty'

    | _ ->

      false

  let struct_field_type ty field =

    match (dynamic_type ty).tdesc with

    | Tstruct fields -> (

      try List.assoc field fields with Not_found -> assert false)

    | _ ->

      assert false

  let rec is_array_type ty =

    match (repr ty).tdesc with

    | Tarray _ ->

      true

    | Tstatic (_, ty') ->

      is_array_type ty' (* looks strange !? *)

    | _ ->

      false

  let array_type_dimension ty =

    match (dynamic_type ty).tdesc with

    | Tarray (d, _) ->

      d

    | _ ->

      Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty

        ty;

      assert false

  let rec array_type_multi_dimension ty =

    match (dynamic_type ty).tdesc with

    | Tarray (d, ty') ->

      d :: array_type_multi_dimension ty'

    | _ ->

      []

  let array_element_type ty =

    match (dynamic_type ty).tdesc with

    | Tarray (_, ty') ->

      ty'

    | _ ->

      Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty;

      assert false

  let rec array_base_type ty =

    let ty = repr ty in

    match ty.tdesc with

    | Tarray (_, ty') | Tstatic (_, ty') ->

      array_base_type ty'

    | _ ->

      ty

  let is_address_type ty =

    is_array_type ty || is_struct_type ty || (is_real_type ty && !Options.mpfr)

  let rec is_generic_type ty =

    match (dynamic_type ty).tdesc with

    | Tarray (d, ty') ->

      (not (Dimension.is_dimension_const d)) || is_generic_type ty'

    | _ ->

      false

  (** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type

      (ensured by language syntax) *)

  let rec split_arrow ty =

    match (repr ty).tdesc with

    | Tarrow (tin, tout) ->

      tin, tout

    | Tstatic (_, ty') ->

      split_arrow ty'

    (* Functions are not first order, I don't think the var case needs to be

       considered here *)

    | _ ->

      Format.eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty;

      assert false

  (** Returns the type corresponding to a type list. *)

  let type_of_type_list tyl =

    if List.length tyl > 1 then new_ty (Ttuple tyl) else List.hd tyl

  let rec type_list_of_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      type_list_of_type ty

    | Ttuple tl ->

      tl

    | _ ->

      [ ty ]

  (** [is_polymorphic ty] returns true if [ty] is polymorphic. *)

  let rec is_polymorphic ty =

    match ty.tdesc with

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

      false

    | Tclock ty ->

      is_polymorphic ty

    | Tarrow (ty1, ty2) ->

      is_polymorphic ty1 || is_polymorphic ty2

    | Ttuple tl ->

      List.exists (fun t -> is_polymorphic t) tl

    | Tstruct fl ->

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

    | Tlink t' ->

      is_polymorphic t'

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

      Dimension.is_polymorphic d || is_polymorphic ty

    | Tunivar ->

      true

  let mktyptuple nb typ =

    let array = Array.make nb typ in

    Ttuple (Array.to_list array)

  let type_desc t = t.tdesc

  let type_int = mk_basic BasicT.type_int_builder

  let type_real = mk_basic BasicT.type_real_builder

  let type_bool = mk_basic BasicT.type_bool_builder

  let type_string = mk_basic BasicT.type_string_builder

module type S = sig

  module BasicT : BASIC_TYPES

  type type_expr = { mutable tdesc : type_desc; tid : int }

    | Tconst of ident

    (* type constant *)

    | Tclock of type_expr

    (* A type expression explicitely tagged as carrying a clock *)

    | Tstatic of dim_expr * type_expr

    (* a type carried by a dimension expression *)

    | Tlink of type_expr

    (* During unification, make links instead of substitutions *)

    | Tvar

    (* Monomorphic type variable *)

    | Tunivar

  (* Polymorphic type variable *)

    | Unbound_value of ident

  exception Unify of type_expr * type_expr

  exception Error of Location.t * error

  val is_real_type : type_expr -> bool

  val is_int_type : type_expr -> bool

  val is_bool_type : type_expr -> bool

  val is_const_type : type_expr -> ident -> bool

  val is_static_type : type_expr -> bool

  val is_array_type : type_expr -> bool

  val is_dimension_type : type_expr -> bool

  val is_address_type : type_expr -> bool

  val is_generic_type : type_expr -> bool

  val print_ty : Format.formatter -> type_expr -> unit

  val repr : type_expr -> type_expr

  val dynamic_type : type_expr -> type_expr

  val type_desc : type_expr -> type_desc

  val new_var : unit -> type_expr

  val new_univar : unit -> type_expr

  val new_ty : type_desc -> type_expr

  val type_int : type_desc

  val type_real : type_desc

  val type_bool : type_desc

  val type_string : type_desc

  val array_element_type : type_expr -> type_expr

  val type_list_of_type : type_expr -> type_expr list

  val print_node_ty : Format.formatter -> type_expr -> unit

  val get_clock_base_type : type_expr -> type_expr option

  val get_static_value : type_expr -> Dimension.dim_expr option

  val is_tuple_type : type_expr -> bool

  val type_of_type_list : type_expr list -> type_expr

  val split_arrow : type_expr -> type_expr * type_expr

  val unclock_type : type_expr -> type_expr

  val bottom : type_expr

  val map_tuple_type : (type_expr -> type_expr) -> type_expr -> type_expr

  val array_base_type : type_expr -> type_expr

  val array_type_dimension : type_expr -> Dimension.dim_expr

  val pp_error : Format.formatter -> error -> unit

  val struct_field_type : type_expr -> ident -> type_expr

  val array_type_multi_dimension : type_expr -> Dimension.dim_expr list

end

(* with type type_expr = BasicT.t type_expr_gen *)

module type Sbasic = S with type BasicT.t = Basic.t

include Main