1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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
|
(* ========================================================================= *)
(* Abstract type of HOL types and functions for manipulating them. *)
(* *)
(* John Harrison, University of Cambridge Computer Laboratory *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
module type Hol_type_primitives =
sig type hol_type = private
Tyvar of string
| Tyapp of string * hol_type list
val types: unit -> (string*int)list
val get_type_arity : string -> int
val new_type : (string * int) -> unit
val mk_type: (string * hol_type list) -> hol_type
val mk_vartype : string -> hol_type
val dest_type : hol_type -> (string * hol_type list)
val dest_vartype : hol_type -> string
val is_type : hol_type -> bool
val is_vartype : hol_type -> bool
val tyvars : hol_type -> hol_type list
val type_subst : (hol_type * hol_type)list -> hol_type -> hol_type
end;;
(* ------------------------------------------------------------------------- *)
(* This is the implementation of those primitives. *)
(* ------------------------------------------------------------------------- *)
module Type : Hol_type_primitives = struct
type hol_type = Tyvar of string
| Tyapp of string * hol_type list
(* ------------------------------------------------------------------------- *)
(* List of current type constants with their arities. *)
(* *)
(* Initially we just have the boolean type and the function space *)
(* constructor. Later on we add as primitive the type of individuals. *)
(* All other new types result from definitional extension. *)
(* ------------------------------------------------------------------------- *)
let the_type_constants = ref ["bool",0; "fun",2]
(* ------------------------------------------------------------------------- *)
(* Return all the defined types. *)
(* ------------------------------------------------------------------------- *)
let types() = !the_type_constants
(* ------------------------------------------------------------------------- *)
(* Lookup function for type constants. Returns arity if it succeeds. *)
(* ------------------------------------------------------------------------- *)
let get_type_arity s = assoc s (!the_type_constants)
(* ------------------------------------------------------------------------- *)
(* Declare a new type. *)
(* ------------------------------------------------------------------------- *)
let new_type(name,arity) =
if can get_type_arity name then
failwith ("new_type: type "^name^" has already been declared")
else the_type_constants := (name,arity)::(!the_type_constants)
(* ------------------------------------------------------------------------- *)
(* Basic type constructors. *)
(* ------------------------------------------------------------------------- *)
let mk_type(tyop,args) =
let arity = try get_type_arity tyop with Failure _ ->
failwith ("mk_type: type "^tyop^" has not been defined") in
if arity = length args then
Tyapp(tyop,args)
else failwith ("mk_type: wrong number of arguments to "^tyop)
let mk_vartype v = Tyvar(v)
(* ------------------------------------------------------------------------- *)
(* Basic type destructors. *)
(* ------------------------------------------------------------------------- *)
let dest_type =
function
(Tyapp (s,ty)) -> s,ty
| (Tyvar _) -> failwith "dest_type: type variable not a constructor"
let dest_vartype =
function
(Tyapp(_,_)) -> failwith "dest_vartype: type constructor not a variable"
| (Tyvar s) -> s
(* ------------------------------------------------------------------------- *)
(* Basic type discriminators. *)
(* ------------------------------------------------------------------------- *)
let is_type = can dest_type
let is_vartype = can dest_vartype
(* ------------------------------------------------------------------------- *)
(* Return the type variables in a type and in a list of types. *)
(* ------------------------------------------------------------------------- *)
let rec tyvars =
function
(Tyapp(_,args)) -> itlist (union o tyvars) args []
| (Tyvar v as tv) -> [tv]
(* ------------------------------------------------------------------------- *)
(* Substitute types for type variables. *)
(* *)
(* NB: non-variables in subst list are just ignored (a check would be *)
(* repeated many times), as are repetitions (first possibility is taken). *)
(* ------------------------------------------------------------------------- *)
let rec type_subst i ty =
match ty with
Tyapp(tycon,args) ->
let args' = qmap (type_subst i) args in
if args' == args then ty else Tyapp(tycon,args')
| _ -> rev_assocd ty i ty
end;;
(* ------------------------------------------------------------------------- *)
(* Display all the externally visible functions. *)
(* ------------------------------------------------------------------------- *)
include Type;;
(* ------------------------------------------------------------------------- *)
(* The following are common enough to deserve their own bindings. *)
(* ------------------------------------------------------------------------- *)
let bool_ty = mk_type("bool",[]);;
let mk_fun_ty ty1 ty2 = mk_type("fun",[ty1; ty2]);;
let aty = mk_vartype "A";;
let bty = mk_vartype "B";;
|
