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

(*                                                                  *)

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

open Utils

(** Types definitions and a few utility functions on delay types. Delay analysis

    by type polymorphism instead of constraints *)

type delay_expr = { mutable ddesc : delay_desc; did : int }

and delay_desc =

  | Dvar (* Monomorphic type variable *)

  | Dundef

  | Darrow of delay_expr * delay_expr

  | Dtuple of delay_expr list

  | Dlink of delay_expr

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

  | Dunivar

(* Polymorphic type variable *)

type error = Delay_clash of delay_expr * delay_expr

exception Unify of delay_expr * delay_expr

exception Error of Location.t * error

let new_id = ref (-1)

let new_delay desc =

  incr new_id;

  { ddesc = desc; did = !new_id }

let new_var () = new_delay Dvar

let new_univar () = new_delay Dunivar

let rec repr = function { ddesc = Dlink i'; _ } -> repr i' | i -> i

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

    (ensured by language syntax) *)

let split_arrow de =

  match (repr de).ddesc with

  | Darrow (din, dout) ->

    din, dout

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

     considered here *)

  | _ ->

    failwith "Internal error: not an arrow type"

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

let delay_of_delay_list de =

  if List.length de > 1 then new_delay (Dtuple de) else List.hd de

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

let rec is_polymorphic de =

  match de.ddesc with

  | Dvar ->

    false

  | Dundef ->

    false

  | Darrow (de1, de2) ->

    is_polymorphic de1 || is_polymorphic de2

  | Dtuple dl ->

    List.exists is_polymorphic dl

  | Dlink d' ->

    is_polymorphic d'

  | Dunivar ->

    true

(* Pretty-print*)

open Format

let rec print_delay fmt de =

  match de.ddesc with

  | Dvar ->

    fprintf fmt "'_%s" (name_of_type de.did)

  | Dundef ->

    fprintf fmt "1"

  | Darrow (de1, de2) ->

    fprintf fmt "%a->%a" print_delay de1 print_delay de2

  | Dtuple delist ->

    fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"*" print_delay) delist

  | Dlink de ->

    print_delay fmt de

  | Dunivar ->

    fprintf fmt "'%s" (name_of_delay de.did)

let pp_error fmt = function

  | Delay_clash (de1, de2) ->

    Utils.reset_names ();

    fprintf fmt "Expected delay %a, got delay %a@." print_delay de1 print_delay

      de2