1 (* ========================================================================= *)
2 (* Abstract type of HOL name-carrying terms and manipulation functions. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
10 module type Hol_term_primitives =
11 sig type term = private
12 Var of string * hol_type
13 | Const of string * hol_type
16 val constants : unit -> (string * hol_type) list
17 val get_const_type : string -> hol_type
18 val new_constant : string * hol_type -> unit
19 val type_of : term -> hol_type
20 val aconv : term -> term -> bool
21 val is_var : term -> bool
22 val is_const : term -> bool
23 val is_abs : term -> bool
24 val is_comb : term -> bool
25 val mk_var : string * hol_type -> term
26 val mk_const : string * (hol_type * hol_type) list -> term
27 val mk_abs : term * term -> term
28 val mk_comb : term * term -> term
29 val dest_var : term -> string * hol_type
30 val dest_const : term -> string * hol_type
31 val dest_comb : term -> term * term
32 val dest_abs : term -> term * term
33 val frees : term -> term list
34 val freesl : term list -> term list
35 val freesin : term list -> term -> bool
36 val vfree_in : term -> term -> bool
37 val type_vars_in_term : term -> hol_type list
38 val variant : term list -> term -> term
39 val vsubst : (term * term) list -> term -> term
40 val inst : (hol_type * hol_type) list -> term -> term
43 (* ------------------------------------------------------------------------- *)
44 (* This is the implementation of those primitives. *)
45 (* ------------------------------------------------------------------------- *)
47 module Term : Hol_term_primitives = struct
49 type term = Var of string * hol_type
50 | Const of string * hol_type
54 (* ------------------------------------------------------------------------- *)
55 (* List of term constants and their types. *)
57 (* We begin with just equality (over all types). Later, the Hilbert choice *)
58 (* operator is added. All other new constants are defined. *)
59 (* ------------------------------------------------------------------------- *)
61 let the_term_constants =
62 ref ["=", mk_fun_ty aty (mk_fun_ty aty bool_ty)]
64 (* ------------------------------------------------------------------------- *)
65 (* Return all the defined constants with generic types. *)
66 (* ------------------------------------------------------------------------- *)
68 let constants() = !the_term_constants
70 (* ------------------------------------------------------------------------- *)
71 (* Gets type of constant if it succeeds. *)
72 (* ------------------------------------------------------------------------- *)
74 let get_const_type s = assoc s (!the_term_constants)
76 (* ------------------------------------------------------------------------- *)
77 (* Declare a new constant. *)
78 (* ------------------------------------------------------------------------- *)
80 let new_constant(name,ty) =
81 if can get_const_type name then
82 failwith ("new_constant: constant "^name^" has already been declared")
83 else the_term_constants := (name,ty)::(!the_term_constants)
85 (* ------------------------------------------------------------------------- *)
86 (* Finds the type of a term (assumes it is well-typed). *)
87 (* ------------------------------------------------------------------------- *)
93 | Comb(s,_) -> hd(tl(snd(dest_type(type_of s))))
94 | Abs(Var(_,ty),t) -> mk_fun_ty ty (type_of t)
96 (* ------------------------------------------------------------------------- *)
97 (* Tests for alpha-convertibility (equality ignoring names in abstractions). *)
98 (* ------------------------------------------------------------------------- *)
101 let rec alphavars env tm1 tm2 =
105 (t1 = tm1 & t2 = tm2) or
106 (t1 <> tm1 & t2 <> tm2 & alphavars oenv tm1 tm2) in
107 let rec raconv env tm1 tm2 =
108 (tm1 == tm2 & env = []) or
110 Var(_,_),Var(_,_) -> alphavars env tm1 tm2
111 | Const(_,_),Const(_,_) -> tm1 = tm2
112 | Comb(s1,t1),Comb(s2,t2) -> raconv env s1 s2 & raconv env t1 t2
113 | Abs(Var(_,ty1) as x1,t1),Abs(Var(_,ty2) as x2,t2) ->
114 ty1 = ty2 & raconv ((x1,x2)::env) t1 t2
116 fun tm1 tm2 -> raconv [] tm1 tm2
118 (* ------------------------------------------------------------------------- *)
119 (* Primitive discriminators. *)
120 (* ------------------------------------------------------------------------- *)
122 let is_var = function (Var(_,_)) -> true | _ -> false
124 let is_const = function (Const(_,_)) -> true | _ -> false
126 let is_abs = function (Abs(_,_)) -> true | _ -> false
128 let is_comb = function (Comb(_,_)) -> true | _ -> false
130 (* ------------------------------------------------------------------------- *)
131 (* Primitive constructors. *)
132 (* ------------------------------------------------------------------------- *)
134 let mk_var(v,ty) = Var(v,ty)
136 let mk_const(name,theta) =
137 let uty = try get_const_type name with Failure _ ->
138 failwith "mk_const: not a constant name" in
139 Const(name,type_subst theta uty)
141 let mk_abs(bvar,bod) =
143 Var(_,_) -> Abs(bvar,bod)
144 | _ -> failwith "mk_abs: not a variable"
148 Tyapp("fun",[ty;_]) when ty = type_of a -> Comb(f,a)
149 | _ -> failwith "mk_comb: types do not agree"
151 (* ------------------------------------------------------------------------- *)
152 (* Primitive destructors. *)
153 (* ------------------------------------------------------------------------- *)
156 function (Var(s,ty)) -> s,ty | _ -> failwith "dest_var: not a variable"
159 function (Const(s,ty)) -> s,ty | _ -> failwith "dest_const: not a constant"
162 function (Comb(f,x)) -> f,x | _ -> failwith "dest_comb: not a combination"
165 function (Abs(v,b)) -> v,b | _ -> failwith "dest_abs: not an abstraction"
167 (* ------------------------------------------------------------------------- *)
168 (* Finds the variables free in a term (list of terms). *)
169 (* ------------------------------------------------------------------------- *)
175 | Abs(bv,bod) -> subtract (frees bod) [bv]
176 | Comb(s,t) -> union (frees s) (frees t)
178 let freesl tml = itlist (union o frees) tml []
180 (* ------------------------------------------------------------------------- *)
181 (* Whether all free variables in a term appear in a list. *)
182 (* ------------------------------------------------------------------------- *)
184 let rec freesin acc tm =
186 Var(_,_) -> mem tm acc
188 | Abs(bv,bod) -> freesin (bv::acc) bod
189 | Comb(s,t) -> freesin acc s & freesin acc t
191 (* ------------------------------------------------------------------------- *)
192 (* Whether a variable (or constant in fact) is free in a term. *)
193 (* ------------------------------------------------------------------------- *)
195 let rec vfree_in v tm =
197 Abs(bv,bod) -> v <> bv & vfree_in v bod
198 | Comb(s,t) -> vfree_in v s or vfree_in v t
201 (* ------------------------------------------------------------------------- *)
202 (* Finds the type variables (free) in a term. *)
203 (* ------------------------------------------------------------------------- *)
205 let rec type_vars_in_term tm =
207 Var(_,ty) -> tyvars ty
208 | Const(_,ty) -> tyvars ty
209 | Comb(s,t) -> union (type_vars_in_term s) (type_vars_in_term t)
210 | Abs(Var(_,ty),t) -> union (tyvars ty) (type_vars_in_term t)
212 (* ------------------------------------------------------------------------- *)
213 (* For name-carrying syntax, we need this early. *)
214 (* ------------------------------------------------------------------------- *)
216 let rec variant avoid v =
217 if not(exists (vfree_in v) avoid) then v else
219 Var(s,ty) -> variant avoid (Var(s^"'",ty))
220 | _ -> failwith "variant: not a variable"
222 (* ------------------------------------------------------------------------- *)
223 (* Substitution primitive (substitution for variables only!) *)
224 (* ------------------------------------------------------------------------- *)
227 let rec vsubst ilist tm =
229 Var(_,_) -> rev_assocd tm ilist tm
231 | Comb(s,t) -> let s' = vsubst ilist s and t' = vsubst ilist t in
232 if s' == s & t' == t then tm else Comb(s',t')
233 | Abs(v,s) -> let ilist' = filter (fun (t,x) -> x <> v) ilist in
234 if ilist' = [] then tm else
235 let s' = vsubst ilist' s in
236 if s' == s then tm else
237 if exists (fun (t,x) -> vfree_in v t & vfree_in x s) ilist'
238 then let v' = variant [s'] v in
239 Abs(v',vsubst ((v',v)::ilist') s)
242 if theta = [] then (fun tm -> tm) else
243 if forall (fun (t,x) -> type_of t = snd(dest_var x)) theta
244 then vsubst theta else failwith "vsubst: Bad substitution list"
246 (* ------------------------------------------------------------------------- *)
247 (* Type instantiation primitive. *)
248 (* ------------------------------------------------------------------------- *)
250 exception Clash of term
253 let rec inst env tyin tm =
255 Var(n,ty) -> let ty' = type_subst tyin ty in
256 let tm' = if ty' == ty then tm else Var(n,ty') in
257 if rev_assocd tm' env tm = tm then tm'
258 else raise (Clash tm')
259 | Const(c,ty) -> let ty' = type_subst tyin ty in
260 if ty' == ty then tm else Const(c,ty')
261 | Comb(f,x) -> let f' = inst env tyin f and x' = inst env tyin x in
262 if f' == f & x' == x then tm else Comb(f',x')
263 | Abs(y,t) -> let y' = inst [] tyin y in
264 let env' = (y,y')::env in
265 try let t' = inst env' tyin t in
266 if y' == y & t' == t then tm else Abs(y',t')
267 with (Clash(w') as ex) ->
268 if w' <> y' then raise ex else
269 let ifrees = map (inst [] tyin) (frees t) in
270 let y'' = variant ifrees y' in
271 let z = Var(fst(dest_var y''),snd(dest_var y)) in
272 inst env tyin (Abs(z,vsubst[z,y] t)) in
273 fun tyin -> if tyin = [] then fun tm -> tm else inst [] tyin