type.ml

   1 (* ========================================================================= *)
   2 (* Abstract type of HOL types and functions for manipulating them.           *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 module type Hol_type_primitives =
  11   sig type hol_type = private
  12         Tyvar of string
  13       | Tyapp of string *  hol_type list
  14       val types: unit -> (string*int)list
  15       val get_type_arity : string -> int
  16       val new_type : (string * int) -> unit
  17       val mk_type: (string * hol_type list) -> hol_type
  18       val mk_vartype : string -> hol_type
  19       val dest_type : hol_type -> (string * hol_type list)
  20       val dest_vartype : hol_type -> string
  21       val is_type : hol_type -> bool
  22       val is_vartype : hol_type -> bool
  23       val tyvars : hol_type -> hol_type list
  24       val type_subst : (hol_type * hol_type)list -> hol_type -> hol_type
  25   end;;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* This is the implementation of those primitives.                           *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 module Type : Hol_type_primitives = struct
  32
  33   type hol_type = Tyvar of string
  34                 | Tyapp of string *  hol_type list
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* List of current type constants with their arities.                        *)
  38 (*                                                                           *)
  39 (* Initially we just have the boolean type and the function space            *)
  40 (* constructor. Later on we add as primitive the type of individuals.        *)
  41 (* All other new types result from definitional extension.                   *)
  42 (* ------------------------------------------------------------------------- *)
  43
  44   let the_type_constants = ref ["bool",0; "fun",2]
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* Return all the defined types.                                             *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50   let types() = !the_type_constants
  51
  52 (* ------------------------------------------------------------------------- *)
  53 (* Lookup function for type constants. Returns arity if it succeeds.         *)
  54 (* ------------------------------------------------------------------------- *)
  55
  56   let get_type_arity s = assoc s (!the_type_constants)
  57
  58 (* ------------------------------------------------------------------------- *)
  59 (* Declare a new type.                                                       *)
  60 (* ------------------------------------------------------------------------- *)
  61
  62   let new_type(name,arity) =
  63     if can get_type_arity name then
  64       failwith ("new_type: type "^name^" has already been declared")
  65     else the_type_constants := (name,arity)::(!the_type_constants)
  66
  67 (* ------------------------------------------------------------------------- *)
  68 (* Basic type constructors.                                                  *)
  69 (* ------------------------------------------------------------------------- *)
  70
  71   let mk_type(tyop,args) =
  72     let arity = try get_type_arity tyop with Failure _ ->
  73       failwith ("mk_type: type "^tyop^" has not been defined") in
  74     if arity = length args then
  75       Tyapp(tyop,args)
  76     else failwith ("mk_type: wrong number of arguments to "^tyop)
  77
  78   let mk_vartype v = Tyvar(v)
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* Basic type destructors.                                                   *)
  82 (* ------------------------------------------------------------------------- *)
  83
  84   let dest_type =
  85     function
  86         (Tyapp (s,ty)) -> s,ty
  87       | (Tyvar _) -> failwith "dest_type: type variable not a constructor"
  88
  89   let dest_vartype =
  90     function
  91         (Tyapp(_,_)) -> failwith "dest_vartype: type constructor not a variable"
  92       | (Tyvar s) -> s
  93
  94 (* ------------------------------------------------------------------------- *)
  95 (* Basic type discriminators.                                                *)
  96 (* ------------------------------------------------------------------------- *)
  97
  98   let is_type = can dest_type
  99
 100   let is_vartype = can dest_vartype
 101
 102 (* ------------------------------------------------------------------------- *)
 103 (* Return the type variables in a type and in a list of types.               *)
 104 (* ------------------------------------------------------------------------- *)
 105
 106   let rec tyvars =
 107       function
 108           (Tyapp(_,args)) -> itlist (union o tyvars) args []
 109         | (Tyvar v as tv) -> [tv]
 110
 111 (* ------------------------------------------------------------------------- *)
 112 (* Substitute types for type variables.                                      *)
 113 (*                                                                           *)
 114 (* NB: non-variables in subst list are just ignored (a check would be        *)
 115 (* repeated many times), as are repetitions (first possibility is taken).    *)
 116 (* ------------------------------------------------------------------------- *)
 117
 118   let rec type_subst i ty =
 119     match ty with
 120       Tyapp(tycon,args) ->
 121           let args' = qmap (type_subst i) args in
 122           if args' == args then ty else Tyapp(tycon,args')
 123       | _ -> rev_assocd ty i ty
 124
 125 end;;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* Display all the externally visible functions.                             *)
 129 (* ------------------------------------------------------------------------- *)
 130
 131 include Type;;
 132
 133 (* ------------------------------------------------------------------------- *)
 134 (* The following are common enough to deserve their own bindings.            *)
 135 (* ------------------------------------------------------------------------- *)
 136
 137 let bool_ty = mk_type("bool",[]);;
 138
 139 let mk_fun_ty ty1 ty2 = mk_type("fun",[ty1; ty2]);;
 140
 141 let aty = mk_vartype "A";;
 142
 143 let bty = mk_vartype "B";;