ty.ml 7.13 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Ident
14 15 16

(** Types *)

17 18 19
type tvsymbol = {
  tv_name : ident;
}
20

21
module Tvar = Stdlib.MakeMSHW (struct
22
  type t = tvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
23 24 25 26 27 28
  let tag tv = tv.tv_name.id_tag
end)

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

30
let tv_equal : tvsymbol -> tvsymbol -> bool = (==)
31

32 33
let tv_hash tv = id_hash tv.tv_name

34
let create_tvsymbol n = { tv_name = id_register n }
35

36
(* type symbols and types *)
Andrei Paskevich's avatar
Andrei Paskevich committed
37

38
type tysymbol = {
39
  ts_name : ident;
40 41 42 43 44 45
  ts_args : tvsymbol list;
  ts_def  : ty option;
}

and ty = {
  ty_node : ty_node;
46
  ty_tag  : Weakhtbl.tag;
47 48 49 50 51 52
}

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

53
module Tsym = Stdlib.MakeMSHW (struct
Andrei Paskevich's avatar
Andrei Paskevich committed
54 55 56 57 58 59 60
  type t = tysymbol
  let tag ts = ts.ts_name.id_tag
end)

module Sts = Tsym.S
module Mts = Tsym.M
module Hts = Tsym.H
61
module Wts = Tsym.W
62

63 64
let ts_equal : tysymbol -> tysymbol -> bool = (==)
let ty_equal : ty       -> ty       -> bool = (==)
65

66
let ts_hash ts = id_hash ts.ts_name
67
let ty_hash ty = Weakhtbl.tag_hash ty.ty_tag
68

69
let mk_ts name args def = {
70
  ts_name = id_register name;
71 72 73 74
  ts_args = args;
  ts_def  = def;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
75
module Hsty = Hashcons.Make (struct
76 77 78
  type t = ty

  let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
79 80 81
    | 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
82 83 84
    | _ -> false

  let hash ty = match ty.ty_node with
85 86
    | Tyvar v -> tv_hash v
    | Tyapp (s,tl) -> Hashcons.combine_list ty_hash (ts_hash s) tl
87

88
  let tag n ty = { ty with ty_tag = Weakhtbl.create_tag n }
Andrei Paskevich's avatar
Andrei Paskevich committed
89 90
end)

91
module Ty = MakeMSHW (struct
Andrei Paskevich's avatar
Andrei Paskevich committed
92 93
  type t = ty
  let tag ty = ty.ty_tag
94
end)
95

Andrei Paskevich's avatar
Andrei Paskevich committed
96 97 98
module Sty = Ty.S
module Mty = Ty.M
module Hty = Ty.H
99
module Wty = Ty.W
100 101 102

let mk_ty n = {
  ty_node = n;
103
  ty_tag  = Weakhtbl.dummy_tag;
104 105
}

106 107
let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))
let ty_app s tl = Hsty.hashcons (mk_ty (Tyapp (s, tl)))
108 109 110 111 112 113 114 115 116

(* 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
117
  | Tyapp (_, tl) -> List.fold_left fn acc tl
118

119
let ty_all pr ty =
120
  try ty_fold (Util.all_fn pr) true ty with Util.FoldSkip -> false
121

122
let ty_any pr ty =
123
  try ty_fold (Util.any_fn pr) false ty with Util.FoldSkip -> true
124

125 126 127 128 129 130 131 132 133 134 135
(* traversal functions on type variables *)

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

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

let ty_v_all pr ty =
136
  try ty_v_fold (Util.all_fn pr) true ty with Util.FoldSkip -> false
137 138

let ty_v_any pr ty =
139
  try ty_v_fold (Util.any_fn pr) false ty with Util.FoldSkip -> true
140 141 142 143 144

let ty_full_inst m ty = ty_v_map (fun v -> Mtv.find v m) ty
let ty_freevars s ty = ty_v_fold (fun s v -> Stv.add v s) s ty
let ty_closed ty = ty_v_all Util.ffalse ty

145 146
(* smart constructors *)

147
exception BadTypeArity of tysymbol * int
148
exception DuplicateTypeVar of tvsymbol
149
exception UnboundTypeVar of tvsymbol
150 151

let create_tysymbol name args def =
152
  let add s v = Stv.add_new (DuplicateTypeVar v) v s in
153
  let s = List.fold_left add Stv.empty args in
154
  let check v = Stv.mem v s || raise (UnboundTypeVar v) in
155
  ignore (Opt.map (ty_v_all check) def);
156
  mk_ts name args def
157

158 159 160 161 162 163 164 165 166
let ty_app s tl = match s.ts_def with
  | Some ty ->
      let mv = try List.fold_right2 Mtv.add s.ts_args tl Mtv.empty with
        | Invalid_argument _ -> raise (BadTypeArity (s, List.length tl)) in
      ty_full_inst mv ty
  | None ->
      if List.length s.ts_args <> List.length tl then
        raise (BadTypeArity (s, List.length tl));
      ty_app s tl
167

168 169 170 171 172 173 174 175 176 177
(* 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

178
let ty_s_all pr ty =
179
  try ty_s_fold (Util.all_fn pr) true ty with Util.FoldSkip -> false
180

181
let ty_s_any pr ty =
182
  try ty_s_fold (Util.any_fn pr) false ty with Util.FoldSkip -> true
183

184 185
(* type matching *)

186
let rec ty_inst s ty = match ty.ty_node with
187
  | Tyvar n -> Mtv.find_def ty n s
188
  | _ -> ty_map (ty_inst s) ty
189

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

202 203 204 205 206
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))
207

208 209 210 211
(* built-in symbols *)

let ts_int  = create_tysymbol (id_fresh "int")  [] None
let ts_real = create_tysymbol (id_fresh "real") [] None
212
let ts_bool = create_tysymbol (id_fresh "bool") [] None
213 214 215

let ty_int  = ty_app ts_int  []
let ty_real = ty_app ts_real []
216
let ty_bool = ty_app ts_bool []
217

218 219 220 221 222
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

223 224
let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]

225 226
let ts_pred =
  let tv_a = create_tvsymbol (id_fresh "a") in
227 228
  let def = Some (ty_func (ty_var tv_a) ty_bool) in
  create_tysymbol (id_fresh "pred") [tv_a] def
229 230 231

let ty_pred ty_a = ty_app ts_pred [ty_a]

232 233
let ts_tuple_ids = Hid.create 17

234
let ts_tuple = Hint.memo 17 (fun n ->
235
  let vl = ref [] in
236
  for _i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
237 238 239
  let ts = create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None in
  Hid.add ts_tuple_ids ts.ts_name n;
  ts)
240

241
let ty_tuple tyl = ty_app (ts_tuple (List.length tyl)) tyl
242

243
let is_ts_tuple ts = ts_equal ts (ts_tuple (List.length ts.ts_args))
244

245 246 247
let is_ts_tuple_id id =
  try Some (Hid.find ts_tuple_ids id) with Not_found -> None

248 249 250 251
(** {2 Operations on [ty option]} *)

exception UnexpectedProp

252
let oty_type = function Some ty -> ty | None -> raise UnexpectedProp
253

254 255
let oty_equal = Opt.equal ty_equal
let oty_hash = Opt.fold (fun _ -> ty_hash) 1
256 257 258 259 260 261

let oty_match m o1 o2 = match o1,o2 with
  | Some ty1, Some ty2 -> ty_match m ty1 ty2
  | None, None -> m
  | _ -> raise UnexpectedProp

262 263 264
let oty_inst m = Opt.map (ty_inst m)
let oty_freevars = Opt.fold ty_freevars
let oty_cons = Opt.fold (fun tl t -> t::tl)
265

266
let ty_equal_check ty1 ty2 =
267 268
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))