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              *)

(*                                                                  *)

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

open Utils

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

module type BASIC_TYPES = sig

  type t

  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

end

module type S = sig

  module BasicT : BASIC_TYPES

  type basic_type = BasicT.t

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

  and type_desc =

    | Tconst of ident

    (* type constant *)

    | Tbasic of basic_type

    | Tclock of t

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

    | Tarrow of t * t

    | Ttuple of t list

    | Tenum of ident list

    | Tstruct of (ident * t) list

    | Tarray of Dimension.t * t

    | Tstatic of Dimension.t * t

    (* a type carried by a dimension expression *)

    | Tlink of t

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

    | Tvar

    (* Monomorphic type variable *)

    | Tunivar

  (* Polymorphic type variable *)

  type error =

    | Unbound_value of ident

    | Already_bound of ident

    | Already_defined of ident

    | Undefined_var of ISet.t

    | Declared_but_undefined of ident

    | Unbound_type of ident

    | Not_a_dimension

    | Not_a_constant

    | Assigned_constant of ident

    | WrongArity of int * int

    | WrongMorphism of int * int

    | Type_mismatch of ident

    | Type_clash of t * t

    | Poly_imported_node of ident

  exception Unify of t * t

  exception Error of Location.t * error

  val is_real_type : t -> bool

  val is_int_type : t -> bool

  val is_bool_type : t -> bool

  val is_const_type : t -> ident -> bool

  val is_static_type : t -> bool

  val is_array_type : t -> bool

  val is_dimension_type : t -> bool

  val is_address_type : t -> bool

  val is_generic_type : t -> bool

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

  val repr : t -> t

  val dynamic_type : t -> t

  val type_desc : t -> type_desc

  val new_var : unit -> t

  val new_univar : unit -> t

  val new_ty : type_desc -> t

  val type_int : type_desc

  val type_real : type_desc

  val type_bool : type_desc

  val type_string : type_desc

  val array_element_type : t -> t

  val type_list_of_type : t -> t list

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

  val get_clock_base_type : t -> t option

  val get_static_value : t -> Dimension.t option

  val types_of_tuple_type : t -> t list

  val is_tuple_type : t -> bool

  val type_of_type_list : t list -> t

  val split_arrow : t -> t * t

  val unclock_type : t -> t

  val bottom : t

  val map_tuple_type : (t -> t) -> t -> t

  val array_base_type : t -> t

  val array_type_dimension : t -> Dimension.t

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

  val struct_field_type : t -> ident -> t

  val array_type_multi_dimension : t -> Dimension.t list

end

module Basic : BASIC_TYPES = struct

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

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

     declaration *)

  let type_string_builder = Tstring

  let type_int_builder = Tint

  let type_real_builder = Treal

  let type_bool_builder = Tbool

  open Format

  let pp fmt t =

    match t with

    | Tint ->

      fprintf fmt "int"

    | Treal ->

      fprintf fmt "real"

    | Tstring ->

      fprintf fmt "string"

    | Tbool ->

      fprintf fmt "bool"

    | Trat ->

      fprintf fmt "rat"

  let pp_c = pp

  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_int_type t = t = Tint

  let is_real_type t = t = Treal

  let is_bool_type t = t = Tbool

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

  let is_unifiable b1 b2 = b1 == b2

  let unify _ _ = ()

end

module Make (BasicT : BASIC_TYPES) = struct

  module BasicT = BasicT

  type basic_type = BasicT.t

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

  and type_desc =

    | Tconst of ident

    (* type constant *)

    | Tbasic of basic_type

    | Tclock of t

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

    | Tarrow of t * t

    | Ttuple of t list

    | Tenum of ident list

    | Tstruct of (ident * t) list

    | Tarray of Dimension.t * t

    | Tstatic of Dimension.t * t

    (* a type carried by a dimension expression *)

    | Tlink of t

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

    | Tvar

    (* Monomorphic type variable *)

    | Tunivar

  (* Polymorphic type variable *)

  type error =

    | Unbound_value of ident

    | Already_bound of ident

    | Already_defined of ident

    | Undefined_var of ISet.t

    | Declared_but_undefined of ident

    | Unbound_type of ident

    | Not_a_dimension

    | Not_a_constant

    | Assigned_constant of ident

    | WrongArity of int * int

    | WrongMorphism of int * int

    | Type_mismatch of ident

    | Type_clash of t * t

    | Poly_imported_node of ident

  exception Unify of t * t

  exception Error of Location.t * error

  let mk_basic t = Tbasic t

  (* Pretty-print*)

  open Format

  let rec pp_struct_ty_field pp_basic fmt (label, ty) =

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

  and pp_ty_param pp_basic fmt ty =

    let pp_ty = pp_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" pp_ty t (if !Options.kind2_print then "" else " clock")

    | Tstatic (_, t) ->

      pp_ty fmt t

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

    | Tconst t ->

      fprintf fmt "%s" t

    | Tarrow (ty1, ty2) ->

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

    | Ttuple tylist ->

      fprintf

        fmt

        "(%a)"

        (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " * ") pp_ty)

        tylist

    | Tenum taglist ->

      fprintf fmt "enum {%a }" (pp_comma_list pp_print_string) taglist

    | Tstruct fieldlist ->

      fprintf

        fmt

        "struct {%a }"

        (pp_print_list ~pp_sep:pp_print_semicolon (pp_struct_ty_field pp_basic))

        fieldlist

    | Tarray (e, ty) ->

      fprintf fmt "%a^%a" pp_ty ty Dimension.pp e

    | Tlink ty ->

      pp_ty fmt ty

    | Tunivar ->

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

  let pp = pp_ty_param BasicT.pp

  let rec pp_node_struct_ty_field fmt (label, ty) =

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

  and pp_node_ty fmt ty =

    match ty.tdesc with

    | Tvar ->

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

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

    | Tbasic t ->

      BasicT.pp fmt t

    | Tclock t ->

      fprintf

        fmt

        "%a%s"

        pp_node_ty

        t

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

    | Tstatic (_, t) ->

      fprintf fmt "%a" pp_node_ty t

    | Tconst t ->

      fprintf fmt "%s" t

    | Tarrow (ty1, ty2) ->

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

    | Ttuple tylist ->

      fprintf

        fmt

        "(%a)"

        (pp_print_list

           ~pp_sep:(fun fmt () -> pp_print_string fmt "")

           pp_node_ty)

        tylist

    | Tenum taglist ->

      fprintf fmt "enum {%a }" (pp_comma_list pp_print_string) taglist

    | Tstruct fieldlist ->

      fprintf

        fmt

        "struct {%a }"

        (pp_print_list ~pp_sep:pp_print_semicolon pp_node_struct_ty_field)

        fieldlist

    | Tarray (e, ty) ->

      fprintf fmt "%a^%a" pp_node_ty ty Dimension.pp e

    | Tlink ty ->

      pp_node_ty fmt 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@."

        (pp_comma_list pp_print_string)

        (ISet.elements vset)

    | Declared_but_undefined id ->

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

    | Type_clash (ty1, ty2) ->

      Utils.reset_names ();

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

    | Poly_imported_node _ ->

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

  let new_id = ref (-1)

  let rec bottom : t = { 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

  (* XXX: UNUSED *)

  (* 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

  (* XXX: UNUSED *)

  (* 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 *)

  (* XXX: UNUSED *)

  (* 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 types_of_tuple_type ty =

    match (repr ty).tdesc with Ttuple ts -> ts | _ -> []

  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

    | _ ->

      eprintf "internal error: Types.array_type_dimension %a@." pp 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'

    | _ ->

      eprintf "internal error: Types.array_element_type %a@." pp 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_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 *)

    | _ ->

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

      assert false

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

  let type_of_type_list = function [ t ] -> t | tyl -> new_ty (Ttuple tyl)

  let rec type_list_of_type ty =

    match (repr ty).tdesc with

    | Tstatic (_, ty) ->

      type_list_of_type ty

    | Ttuple tl ->

      tl

    | _ ->

      [ ty ]

  (* XXX: UNUSED *)

  (** [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 *)

  (* XXX: UNUSED *)

  (* 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

end

include Make (Basic)

(* Local Variables: *)

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

(* End: *)