ty.ml 6.59 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19 20

open Util
21
open Ident
22 23 24

(** Types *)

25 26 27
type tvsymbol = {
  tv_name : ident;
}
28

Andrei Paskevich's avatar
Andrei Paskevich committed
29
module Tvar = WeakStructMake (struct
30
  type t = tvsymbol
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
31 32 33 34 35 36
  let tag tv = tv.tv_name.id_tag
end)

module Stv = Tvar.S
module Mtv = Tvar.M
module Htv = Tvar.H
37

38 39
let tv_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
40 41
let tv_hash tv = id_hash tv.tv_name

42
let create_tvsymbol n = { tv_name = id_register n }
43

44
(* type symbols and types *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
45

46
type tysymbol = {
47
  ts_name : ident;
48 49 50 51 52 53
  ts_args : tvsymbol list;
  ts_def  : ty option;
}

and ty = {
  ty_node : ty_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
54
  ty_tag  : Hashweak.tag;
55 56 57 58 59 60
}

and ty_node =
  | Tyvar of tvsymbol
  | Tyapp of tysymbol * ty list

Andrei Paskevich's avatar
Andrei Paskevich committed
61
module Tsym = WeakStructMake (struct
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
62 63 64 65 66 67 68
  type t = tysymbol
  let tag ts = ts.ts_name.id_tag
end)

module Sts = Tsym.S
module Mts = Tsym.M
module Hts = Tsym.H
Andrei Paskevich's avatar
Andrei Paskevich committed
69
module Wts = Tsym.W
70

71 72
let ts_equal : tysymbol -> tysymbol -> bool = (==)
let ty_equal : ty       -> ty       -> bool = (==)
73

Andrei Paskevich's avatar
Andrei Paskevich committed
74 75 76
let ts_hash ts = id_hash ts.ts_name
let ty_hash ty = Hashweak.tag_hash ty.ty_tag

77 78 79 80 81 82
let mk_ts name args def = {
  ts_name = name;
  ts_args = args;
  ts_def  = def;
}

83
let create_tysymbol name args def = mk_ts (id_register name) args def
84

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
85
module Hsty = Hashcons.Make (struct
86 87 88
  type t = ty

  let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
89 90 91
    | Tyvar n1, Tyvar n2 -> tv_equal n1 n2
    | Tyapp (s1,l1), Tyapp (s2,l2) ->
        ts_equal s1 s2 && List.for_all2 ty_equal l1 l2
92 93 94
    | _ -> false

  let hash ty = match ty.ty_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
95 96
    | Tyvar v -> tv_hash v
    | Tyapp (s,tl) -> Hashcons.combine_list ty_hash (ts_hash s) tl
97

Andrei Paskevich's avatar
Andrei Paskevich committed
98
  let tag n ty = { ty with ty_tag = Hashweak.create_tag n }
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
99 100
end)

Andrei Paskevich's avatar
Andrei Paskevich committed
101
module Ty = WeakStructMake (struct
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
102 103
  type t = ty
  let tag ty = ty.ty_tag
Andrei Paskevich's avatar
Andrei Paskevich committed
104
end)
105

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
106 107 108
module Sty = Ty.S
module Mty = Ty.M
module Hty = Ty.H
Andrei Paskevich's avatar
Andrei Paskevich committed
109
module Wty = Ty.W
110 111 112

let mk_ty n = {
  ty_node = n;
Andrei Paskevich's avatar
Andrei Paskevich committed
113
  ty_tag  = Hashweak.dummy_tag;
114 115
}

Francois Bobot's avatar
 
Francois Bobot committed
116 117
let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))
let ty_app s tl = Hsty.hashcons (mk_ty (Tyapp (s, tl)))
118 119 120 121 122 123 124 125 126

(* generic traversal functions *)

let ty_map fn ty = match ty.ty_node with
  | Tyvar _ -> ty
  | Tyapp (f, tl) -> ty_app f (List.map fn tl)

let ty_fold fn acc ty = match ty.ty_node with
  | Tyvar _ -> acc
MARCHE Claude's avatar
MARCHE Claude committed
127
  | Tyapp (_, tl) -> List.fold_left fn acc tl
128

129 130
let ty_all pr ty =
  try ty_fold (all_fn pr) true ty with FoldSkip -> false
131

132 133
let ty_any pr ty =
  try ty_fold (any_fn pr) false ty with FoldSkip -> true
134 135 136

(* smart constructors *)

137
exception BadTypeArity of tysymbol * int * int
138
exception DuplicateTypeVar of tvsymbol
139
exception UnboundTypeVar of tvsymbol
140 141

let create_tysymbol name args def =
142
  let add s v = Stv.add_new v (DuplicateTypeVar v) s in
143
  let s = List.fold_left add Stv.empty args in
144 145 146 147 148
  let rec vars () ty = match ty.ty_node with
    | Tyvar v when not (Stv.mem v s) -> raise (UnboundTypeVar v)
    | _ -> ty_fold vars () ty
  in
  option_iter (vars ()) def;
149 150 151
  create_tysymbol name args def

let rec tv_inst m ty = match ty.ty_node with
152
  | Tyvar n -> Mtv.find n m
153 154
  | _ -> ty_map (tv_inst m) ty

155 156 157 158
let rec ty_freevars s ty = match ty.ty_node with
  | Tyvar n -> Stv.add n s
  | _ -> ty_fold ty_freevars s ty

159
let ty_app s tl =
160 161
  let tll = List.length tl in
  let stl = List.length s.ts_args in
162
  if tll <> stl then raise (BadTypeArity (s,stl,tll));
163
  match s.ts_def with
164
    | Some ty ->
165 166
        let add m v t = Mtv.add v t m in
        tv_inst (List.fold_left2 add Mtv.empty s.ts_args tl) ty
167 168 169
    | _ ->
        ty_app s tl

170 171 172 173 174 175 176 177 178 179
(* symbol-wise map/fold *)

let rec ty_s_map fn ty = match ty.ty_node with
  | Tyvar _ -> ty
  | Tyapp (f, tl) -> ty_app (fn f) (List.map (ty_s_map fn) tl)

let rec ty_s_fold fn acc ty = match ty.ty_node with
  | Tyvar _ -> acc
  | Tyapp (f, tl) -> List.fold_left (ty_s_fold fn) (fn acc f) tl

180 181
let ty_s_all pr ty =
  try ty_s_fold (all_fn pr) true ty with FoldSkip -> false
182

183 184
let ty_s_any pr ty =
  try ty_s_fold (any_fn pr) false ty with FoldSkip -> true
185

186 187
(* type matching *)

188
let rec ty_inst s ty = match ty.ty_node with
189
  | Tyvar n -> Mtv.find_default n ty s
190
  | _ -> ty_map (ty_inst s) ty
191

192
let rec ty_match s ty1 ty2 =
193
  if ty_equal ty1 ty2 then s
194 195
  else match ty1.ty_node, ty2.ty_node with
    | Tyvar n1, _ ->
196 197 198 199
        Mtv.change n1 (function
          | None -> Some ty2
          | Some ty1 as r when ty_equal ty1 ty2 -> r
          | _ -> raise Exit) s
200
    | Tyapp (f1, l1), Tyapp (f2, l2) when ts_equal f1 f2 ->
201
        List.fold_left2 ty_match s l1 l2
202
    | _ ->
203
        raise Exit
204

205 206 207 208 209
exception TypeMismatch of ty * ty

let ty_match s ty1 ty2 =
  try ty_match s ty1 ty2
  with Exit -> raise (TypeMismatch (ty_inst s ty1, ty2))
210

211 212 213 214 215 216 217 218
(* built-in symbols *)

let ts_int  = create_tysymbol (id_fresh "int")  [] None
let ts_real = create_tysymbol (id_fresh "real") [] None

let ty_int  = ty_app ts_int  []
let ty_real = ty_app ts_real []

219 220 221 222 223 224 225 226 227 228 229 230
let ts_func =
  let tv_a = create_tvsymbol (id_fresh "a") in
  let tv_b = create_tvsymbol (id_fresh "b") in
  create_tysymbol (id_fresh "func") [tv_a;tv_b] None

let ts_pred =
  let tv_a = create_tvsymbol (id_fresh "a") in
  create_tysymbol (id_fresh "pred") [tv_a] None

let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]
let ty_pred ty_a = ty_app ts_pred [ty_a]

231
let ts_tuple = Util.memo_int 17 (fun n ->
232 233
  let vl = ref [] in
  for i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
234
  create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None)
235

236
let ty_tuple tyl = ty_app (ts_tuple (List.length tyl)) tyl
237

238
let is_ts_tuple ts = ts == ts_tuple (List.length ts.ts_args)
239