Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/delay.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
(** Types definitions and a few utility functions on delay types.
13
    Delay analysis by type polymorphism instead of constraints *)
14 12
open Utils
13
(** Types definitions and a few utility functions on delay types. Delay analysis
14
    by type polymorphism instead of constraints *)
15 15

  
16
type delay_expr =
17
    {mutable ddesc: delay_desc;
18
     did: int}
16
type delay_expr = { mutable ddesc : delay_desc; did : int }
19 17

  
20 18
and delay_desc =
21 19
  | Dvar (* Monomorphic type variable *)
22 20
  | Dundef
23 21
  | Darrow of delay_expr * delay_expr
24 22
  | Dtuple of delay_expr list
25
  | Dlink of delay_expr (* During unification, make links instead of substitutions *)
26
  | Dunivar (* Polymorphic type variable *)
27
type error =
28
  | Delay_clash of delay_expr * delay_expr
23
  | Dlink of delay_expr
24
  (* During unification, make links instead of substitutions *)
25
  | Dunivar
26
(* Polymorphic type variable *)
27

  
28
type error = Delay_clash of delay_expr * delay_expr
29 29

  
30 30
exception Unify of delay_expr * delay_expr
31

  
31 32
exception Error of Location.t * error
32 33

  
33 34
let new_id = ref (-1)
34 35

  
35 36
let new_delay desc =
36
  incr new_id; {ddesc = desc; did = !new_id }
37
  incr new_id;
38
  { ddesc = desc; did = !new_id }
37 39

  
38
let new_var () =
39
  new_delay Dvar
40
let new_var () = new_delay Dvar
40 41

  
41
let new_univar () =
42
  new_delay Dunivar
42
let new_univar () = new_delay Dunivar
43 43

  
44
let rec repr =
45
  function
46
    {ddesc = Dlink i'; _} ->
47
      repr i'
48
  | i -> i
44
let rec repr = function { ddesc = Dlink i'; _ } -> repr i' | i -> i
49 45

  
50 46
(** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type
51 47
    (ensured by language syntax) *)
52 48
let split_arrow de =
53 49
  match (repr de).ddesc with
54
  | Darrow (din,dout) -> din,dout
55
    (* Functions are not first order, I don't think the var case
56
       needs to be considered here *)
57
  | _ -> failwith "Internal error: not an arrow type"
50
  | Darrow (din, dout) ->
51
    din, dout
52
  (* Functions are not first order, I don't think the var case needs to be
53
     considered here *)
54
  | _ ->
55
    failwith "Internal error: not an arrow type"
58 56

  
59 57
(** Returns the type corresponding to a type list. *)
60 58
let delay_of_delay_list de =
61
  if (List.length de) > 1 then
62
    new_delay (Dtuple de)
63
  else
64
    List.hd de
59
  if List.length de > 1 then new_delay (Dtuple de) else List.hd de
65 60

  
66 61
(** [is_polymorphic de] returns true if [de] is polymorphic. *)
67 62
let rec is_polymorphic de =
68 63
  match de.ddesc with
69
  | Dvar  -> false
70
  | Dundef -> false
71
  | Darrow (de1,de2) -> (is_polymorphic de1) || (is_polymorphic de2)
72
  | Dtuple dl -> List.exists is_polymorphic dl
73
  | Dlink d' -> is_polymorphic d'
74
  | Dunivar -> true
64
  | Dvar ->
65
    false
66
  | Dundef ->
67
    false
68
  | Darrow (de1, de2) ->
69
    is_polymorphic de1 || is_polymorphic de2
70
  | Dtuple dl ->
71
    List.exists is_polymorphic dl
72
  | Dlink d' ->
73
    is_polymorphic d'
74
  | Dunivar ->
75
    true
75 76

  
76 77
(* Pretty-print*)
77 78
open Format
78
  
79

  
79 80
let rec print_delay fmt de =
80 81
  match de.ddesc with
81 82
  | Dvar ->
82 83
    fprintf fmt "'_%s" (name_of_type de.did)
83 84
  | Dundef ->
84 85
    fprintf fmt "1"
85
  | Darrow (de1,de2) ->
86
  | Darrow (de1, de2) ->
86 87
    fprintf fmt "%a->%a" print_delay de1 print_delay de2
87 88
  | Dtuple delist ->
88
    fprintf fmt "(%a)"
89
      (Utils.fprintf_list ~sep:"*" print_delay) delist
89
    fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"*" print_delay) delist
90 90
  | Dlink de ->
91
      print_delay fmt de
91
    print_delay fmt de
92 92
  | Dunivar ->
93 93
    fprintf fmt "'%s" (name_of_delay de.did)
94 94

  
95 95
let pp_error fmt = function
96
  | Delay_clash (de1,de2) ->
97
      Utils.reset_names ();
98
    fprintf fmt "Expected delay %a, got delay %a@." print_delay de1 print_delay de2
96
  | Delay_clash (de1, de2) ->
97
    Utils.reset_names ();
98
    fprintf fmt "Expected delay %a, got delay %a@." print_delay de1 print_delay
99
      de2

Also available in: Unified diff