ty.ml 4.53 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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 21 22 23 24 25 26

open Util

(** Types *)

type tvsymbol = Name.t

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

28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
type tysymbol = {
  ts_name : Name.t;
  ts_args : tvsymbol list;
  ts_def  : ty option;
  ts_tag  : int;
}

and ty = {
  ty_node : ty_node;
  ty_tag : int;
}

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

module Tsym = struct
  type t = tysymbol
  let equal ts1 ts2 = Name.equal ts1.ts_name ts2.ts_name
  let hash ts = Name.hash ts.ts_name
  let tag n ts = { ts with ts_tag = n }
  let compare ts1 ts2 = Pervasives.compare ts1.ts_tag ts2.ts_tag
end
module Hts = Hashcons.Make(Tsym)
module Sts = Set.Make(Tsym)
module Mts = Map.Make(Tsym)

let mk_ts name args def = {
  ts_name = name;
  ts_args = args;
  ts_def  = def;
  ts_tag  = -1
}

let create_tysymbol name args def = Hts.hashcons (mk_ts name args def)

module Ty = struct

  type t = ty

  let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
    | Tyvar n1, Tyvar n2 -> Name.equal n1 n2
    | Tyapp (s1, l1), Tyapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
    | _ -> false

  let hash_ty ty = ty.ty_tag

  let hash ty = match ty.ty_node with
    | Tyvar v -> Name.hash v
    | Tyapp (s, tl) -> Hashcons.combine_list hash_ty (s.ts_tag) tl

  let tag n ty = { ty with ty_tag = n }

end
module Hty = Hashcons.Make(Ty)

let mk_ty n = { ty_node = n; ty_tag = -1 }
let ty_var n = Hty.hashcons (mk_ty (Tyvar n))
let ty_app s tl = Hty.hashcons (mk_ty (Tyapp (s, tl)))

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

let ty_forall pr ty =
  try ty_fold (forall_fn pr) true ty with FoldSkip -> false

let ty_exists pr ty =
  try ty_fold (exists_fn pr) false ty with FoldSkip -> true

(* smart constructors *)

exception NonLinear
exception UnboundTypeVariable

let rec tv_known vs ty = match ty.ty_node with
  | Tyvar n -> Name.S.mem n vs
  | _ -> ty_forall (tv_known vs) ty

let create_tysymbol name args def =
  let add s v = if Name.S.mem v s
  then raise NonLinear else Name.S.add v s in
  let s = List.fold_left add Name.S.empty args in
  let _ = match def with
    | Some ty -> tv_known s ty || raise UnboundTypeVariable
    | _ -> true
  in
  create_tysymbol name args def

exception BadTypeArity

let rec tv_inst m ty = match ty.ty_node with
  | Tyvar n -> Name.M.find n m
  | _ -> ty_map (tv_inst m) ty

let ty_app s tl =
  if List.length tl == List.length s.ts_args
  then match s.ts_def with
    | Some ty ->
        let add m v t = Name.M.add v t m in
        tv_inst (List.fold_left2 add Name.M.empty s.ts_args tl) ty
    | _ ->
        ty_app s tl
  else raise BadTypeArity

(* type matching *)

exception TypeMismatch

let rec matching s ty1 ty2 =
  if ty1 == ty2 then s
  else match ty1.ty_node, ty2.ty_node with
    | Tyvar n1, _ ->
        (try if Name.M.find n1 s == ty2 then s else raise TypeMismatch
         with Not_found -> Name.M.add n1 ty2 s)
    | Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
        List.fold_left2 matching s l1 l2
    | _ ->
        raise TypeMismatch

let ty_match ty1 ty2 s =
  try Some (matching s ty1 ty2) with TypeMismatch -> None