term.ml

   1 (* ========================================================================= *)
   2 (* Abstract type of HOL name-carrying terms and manipulation functions.      *)
   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_term_primitives =
  11   sig type term = private
  12     Var of string * hol_type
  13   | Const of string * hol_type
  14   | Comb of term * term
  15   | Abs of term * term
  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
  41 end;;
  42
  43 (* ------------------------------------------------------------------------- *)
  44 (* This is the implementation of those primitives.                           *)
  45 (* ------------------------------------------------------------------------- *)
  46
  47 module Term : Hol_term_primitives = struct
  48
  49   type term = Var of string * hol_type
  50             | Const of string * hol_type
  51             | Comb of term * term
  52             | Abs of term * term
  53
  54 (* ------------------------------------------------------------------------- *)
  55 (* List of term constants and their types.                                   *)
  56 (*                                                                           *)
  57 (* We begin with just equality (over all types). Later, the Hilbert choice   *)
  58 (* operator is added. All other new constants are defined.                   *)
  59 (* ------------------------------------------------------------------------- *)
  60
  61   let the_term_constants =
  62      ref ["=",  mk_fun_ty aty (mk_fun_ty aty bool_ty)]
  63
  64 (* ------------------------------------------------------------------------- *)
  65 (* Return all the defined constants with generic types.                      *)
  66 (* ------------------------------------------------------------------------- *)
  67
  68   let constants() = !the_term_constants
  69
  70 (* ------------------------------------------------------------------------- *)
  71 (* Gets type of constant if it succeeds.                                     *)
  72 (* ------------------------------------------------------------------------- *)
  73
  74   let get_const_type s = assoc s (!the_term_constants)
  75
  76 (* ------------------------------------------------------------------------- *)
  77 (* Declare a new constant.                                                   *)
  78 (* ------------------------------------------------------------------------- *)
  79
  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)
  84
  85 (* ------------------------------------------------------------------------- *)
  86 (* Finds the type of a term (assumes it is well-typed).                      *)
  87 (* ------------------------------------------------------------------------- *)
  88
  89   let rec type_of tm =
  90     match tm with
  91       Var(_,ty) -> ty
  92     | Const(_,ty) -> ty
  93     | Comb(s,_) -> hd(tl(snd(dest_type(type_of s))))
  94     | Abs(Var(_,ty),t) -> mk_fun_ty ty (type_of t)
  95
  96 (* ------------------------------------------------------------------------- *)
  97 (* Tests for alpha-convertibility (equality ignoring names in abstractions). *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100   let aconv =
 101     let rec alphavars env tm1 tm2 =
 102       match env with
 103         [] -> tm1 = tm2
 104       | (t1,t2)::oenv ->
 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
 109       match (tm1,tm2) with
 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
 115       | _ -> false in
 116     fun tm1 tm2 -> raconv [] tm1 tm2
 117
 118 (* ------------------------------------------------------------------------- *)
 119 (* Primitive discriminators.                                                 *)
 120 (* ------------------------------------------------------------------------- *)
 121
 122   let is_var = function (Var(_,_)) -> true | _ -> false
 123
 124   let is_const = function (Const(_,_)) -> true | _ -> false
 125
 126   let is_abs = function (Abs(_,_)) -> true | _ -> false
 127
 128   let is_comb = function (Comb(_,_)) -> true | _ -> false
 129
 130 (* ------------------------------------------------------------------------- *)
 131 (* Primitive constructors.                                                   *)
 132 (* ------------------------------------------------------------------------- *)
 133
 134   let mk_var(v,ty) = Var(v,ty)
 135
 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)
 140
 141   let mk_abs(bvar,bod) =
 142     match bvar with
 143       Var(_,_) -> Abs(bvar,bod)
 144     | _ -> failwith "mk_abs: not a variable"
 145
 146   let mk_comb(f,a) =
 147     match type_of f with
 148       Tyapp("fun",[ty;_]) when ty = type_of a -> Comb(f,a)
 149     | _ -> failwith "mk_comb: types do not agree"
 150
 151 (* ------------------------------------------------------------------------- *)
 152 (* Primitive destructors.                                                    *)
 153 (* ------------------------------------------------------------------------- *)
 154
 155   let dest_var =
 156     function (Var(s,ty)) -> s,ty | _ -> failwith "dest_var: not a variable"
 157
 158   let dest_const =
 159     function (Const(s,ty)) -> s,ty | _ -> failwith "dest_const: not a constant"
 160
 161   let dest_comb =
 162     function (Comb(f,x)) -> f,x | _ -> failwith "dest_comb: not a combination"
 163
 164   let dest_abs =
 165     function (Abs(v,b)) -> v,b | _ -> failwith "dest_abs: not an abstraction"
 166
 167 (* ------------------------------------------------------------------------- *)
 168 (* Finds the variables free in a term (list of terms).                       *)
 169 (* ------------------------------------------------------------------------- *)
 170
 171   let rec frees tm =
 172     match tm with
 173       Var(_,_) -> [tm]
 174     | Const(_,_) -> []
 175     | Abs(bv,bod) -> subtract (frees bod) [bv]
 176     | Comb(s,t) -> union (frees s) (frees t)
 177
 178   let freesl tml = itlist (union o frees) tml []
 179
 180 (* ------------------------------------------------------------------------- *)
 181 (* Whether all free variables in a term appear in a list.                    *)
 182 (* ------------------------------------------------------------------------- *)
 183
 184   let rec freesin acc tm =
 185     match tm with
 186       Var(_,_) -> mem tm acc
 187     | Const(_,_) -> true
 188     | Abs(bv,bod) -> freesin (bv::acc) bod
 189     | Comb(s,t) -> freesin acc s & freesin acc t
 190
 191 (* ------------------------------------------------------------------------- *)
 192 (* Whether a variable (or constant in fact) is free in a term.               *)
 193 (* ------------------------------------------------------------------------- *)
 194
 195   let rec vfree_in v tm =
 196     match tm with
 197       Abs(bv,bod) -> v <> bv & vfree_in v bod
 198     | Comb(s,t) -> vfree_in v s or vfree_in v t
 199     | _ -> tm = v
 200
 201 (* ------------------------------------------------------------------------- *)
 202 (* Finds the type variables (free) in a term.                                *)
 203 (* ------------------------------------------------------------------------- *)
 204
 205   let rec type_vars_in_term tm =
 206     match tm with
 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)
 211
 212 (* ------------------------------------------------------------------------- *)
 213 (* For name-carrying syntax, we need this early.                             *)
 214 (* ------------------------------------------------------------------------- *)
 215
 216   let rec variant avoid v =
 217     if not(exists (vfree_in v) avoid) then v else
 218     match v with
 219       Var(s,ty) -> variant avoid (Var(s^"'",ty))
 220     | _ -> failwith "variant: not a variable"
 221
 222 (* ------------------------------------------------------------------------- *)
 223 (* Substitution primitive (substitution for variables only!)                 *)
 224 (* ------------------------------------------------------------------------- *)
 225
 226   let vsubst =
 227     let rec vsubst ilist tm =
 228       match tm with
 229         Var(_,_) -> rev_assocd tm ilist tm
 230       | Const(_,_) -> 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)
 240                     else Abs(v,s') in
 241     fun theta ->
 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"
 245
 246 (* ------------------------------------------------------------------------- *)
 247 (* Type instantiation primitive.                                             *)
 248 (* ------------------------------------------------------------------------- *)
 249
 250   exception Clash of term
 251
 252   let inst =
 253     let rec inst env tyin tm =
 254       match tm with
 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
 274 end;;
 275
 276 include Term;;