1(* Title: Pure/envir.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 4Free-form environments. The type of a term variable / sort of a type variable is 5part of its name. The lookup function must apply type substitutions, 6since they may change the identity of a variable. 7*) 8 9signature ENVIR = 10sig 11 type tenv = (typ * term) Vartab.table 12 datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv} 13 val maxidx_of: env -> int 14 val term_env: env -> tenv 15 val type_env: env -> Type.tyenv 16 val is_empty: env -> bool 17 val empty: int -> env 18 val init: env 19 val merge: env * env -> env 20 val insert_sorts: env -> sort list -> sort list 21 val genvars: string -> env * typ list -> env * term list 22 val genvar: string -> env * typ -> env * term 23 val lookup1: tenv -> indexname * typ -> term option 24 val lookup: env -> indexname * typ -> term option 25 val update: (indexname * typ) * term -> env -> env 26 val above: env -> int -> bool 27 val vupdate: (indexname * typ) * term -> env -> env 28 val norm_type_same: Type.tyenv -> typ Same.operation 29 val norm_types_same: Type.tyenv -> typ list Same.operation 30 val norm_type: Type.tyenv -> typ -> typ 31 val norm_term_same: env -> term Same.operation 32 val norm_term: env -> term -> term 33 val beta_norm: term -> term 34 val head_norm: env -> term -> term 35 val eta_long: typ list -> term -> term 36 val eta_contract: term -> term 37 val beta_eta_contract: term -> term 38 val aeconv: term * term -> bool 39 val body_type: env -> typ -> typ 40 val binder_types: env -> typ -> typ list 41 val strip_type: env -> typ -> typ list * typ 42 val fastype: env -> typ list -> term -> typ 43 val subst_type_same: Type.tyenv -> typ Same.operation 44 val subst_term_types_same: Type.tyenv -> term Same.operation 45 val subst_term_same: Type.tyenv * tenv -> term Same.operation 46 val subst_type: Type.tyenv -> typ -> typ 47 val subst_term_types: Type.tyenv -> term -> term 48 val subst_term: Type.tyenv * tenv -> term -> term 49 val expand_atom: typ -> typ * term -> term 50 val expand_term: (term -> (typ * term) option) -> term -> term 51 val expand_term_frees: ((string * typ) * term) list -> term -> term 52end; 53 54structure Envir: ENVIR = 55struct 56 57(** datatype env **) 58 59(*Updating can destroy environment in 2 ways! 60 (1) variables out of range 61 (2) circular assignments 62*) 63 64type tenv = (typ * term) Vartab.table; 65 66datatype env = Envir of 67 {maxidx: int, (*upper bound of maximum index of vars*) 68 tenv: tenv, (*assignments to Vars*) 69 tyenv: Type.tyenv}; (*assignments to TVars*) 70 71fun make_env (maxidx, tenv, tyenv) = 72 Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv}; 73 74fun maxidx_of (Envir {maxidx, ...}) = maxidx; 75fun term_env (Envir {tenv, ...}) = tenv; 76fun type_env (Envir {tyenv, ...}) = tyenv; 77 78fun is_empty env = 79 Vartab.is_empty (term_env env) andalso 80 Vartab.is_empty (type_env env); 81 82 83(* build env *) 84 85fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty); 86val init = empty ~1; 87 88fun merge 89 (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1}, 90 Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) = 91 make_env (Int.max (maxidx1, maxidx2), 92 Vartab.merge (op =) (tenv1, tenv2), 93 Vartab.merge (op =) (tyenv1, tyenv2)); 94 95 96(*NB: type unification may invent new sorts*) (* FIXME tenv!? *) 97val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env; 98 99(*Generate a list of distinct variables. 100 Increments index to make them distinct from ALL present variables. *) 101fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list = 102 let 103 fun genvs (_, [] : typ list) : term list = [] 104 | genvs (_, [T]) = [Var ((name, maxidx + 1), T)] 105 | genvs (n, T :: Ts) = 106 Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T) 107 :: genvs (n + 1, Ts); 108 in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end; 109 110(*Generate a variable.*) 111fun genvar name (env, T) : env * term = 112 let val (env', [v]) = genvars name (env, [T]) 113 in (env', v) end; 114 115fun var_clash xi T T' = 116 raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]); 117 118fun lookup_check check tenv (xi, T) = 119 (case Vartab.lookup tenv xi of 120 NONE => NONE 121 | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U); 122 123(*When dealing with environments produced by matching instead 124 of unification, there is no need to chase assigned TVars. 125 In this case, we can simply ignore the type substitution 126 and use = instead of eq_type.*) 127fun lookup1 tenv = lookup_check (op =) tenv; 128 129fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified tyenv) tenv; 130 131fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) = 132 Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv}; 133 134(*Determine if the least index updated exceeds lim*) 135fun above (Envir {tenv, tyenv, ...}) lim = 136 (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso 137 (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true); 138 139(*Update, checking Var-Var assignments: try to suppress higher indexes*) 140fun vupdate ((a, U), t) env = 141 (case t of 142 Var (nT as (name', T)) => 143 if a = name' then env (*cycle!*) 144 else if Term_Ord.indexname_ord (a, name') = LESS then 145 (case lookup env nT of (*if already assigned, chase*) 146 NONE => update (nT, Var (a, T)) env 147 | SOME u => vupdate ((a, U), u) env) 148 else update ((a, U), t) env 149 | _ => update ((a, U), t) env); 150 151 152 153(** beta normalization wrt. environment **) 154 155(*Chases variables in env. Does not exploit sharing of variable bindings 156 Does not check types, so could loop.*) 157 158local 159 160fun norm_type0 tyenv : typ Same.operation = 161 let 162 fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts) 163 | norm (TFree _) = raise Same.SAME 164 | norm (TVar v) = 165 (case Type.lookup tyenv v of 166 SOME U => Same.commit norm U 167 | NONE => raise Same.SAME); 168 in norm end; 169 170fun norm_term1 tenv : term Same.operation = 171 let 172 fun norm (Var v) = 173 (case lookup1 tenv v of 174 SOME u => Same.commit norm u 175 | NONE => raise Same.SAME) 176 | norm (Abs (a, T, body)) = Abs (a, T, norm body) 177 | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) 178 | norm (f $ t) = 179 ((case norm f of 180 Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) 181 | nf => nf $ Same.commit norm t) 182 handle Same.SAME => f $ norm t) 183 | norm _ = raise Same.SAME; 184 in norm end; 185 186fun norm_term2 (envir as Envir {tyenv, ...}) : term Same.operation = 187 let 188 val normT = norm_type0 tyenv; 189 fun norm (Const (a, T)) = Const (a, normT T) 190 | norm (Free (a, T)) = Free (a, normT T) 191 | norm (Var (xi, T)) = 192 (case lookup envir (xi, T) of 193 SOME u => Same.commit norm u 194 | NONE => Var (xi, normT T)) 195 | norm (Abs (a, T, body)) = 196 (Abs (a, normT T, Same.commit norm body) 197 handle Same.SAME => Abs (a, T, norm body)) 198 | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) 199 | norm (f $ t) = 200 ((case norm f of 201 Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) 202 | nf => nf $ Same.commit norm t) 203 handle Same.SAME => f $ norm t) 204 | norm _ = raise Same.SAME; 205 in norm end; 206 207in 208 209fun norm_type_same tyenv T = 210 if Vartab.is_empty tyenv then raise Same.SAME 211 else norm_type0 tyenv T; 212 213fun norm_types_same tyenv Ts = 214 if Vartab.is_empty tyenv then raise Same.SAME 215 else Same.map (norm_type0 tyenv) Ts; 216 217fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T; 218 219fun norm_term_same (envir as Envir {tenv, tyenv, ...}) = 220 if Vartab.is_empty tyenv then norm_term1 tenv 221 else norm_term2 envir; 222 223fun norm_term envir t = norm_term_same envir t handle Same.SAME => t; 224 225fun beta_norm t = 226 if Term.could_beta_contract t then norm_term init t else t; 227 228end; 229 230 231(* head normal form for unification *) 232 233fun head_norm env = 234 let 235 fun norm (Var v) = 236 (case lookup env v of 237 SOME u => head_norm env u 238 | NONE => raise Same.SAME) 239 | norm (Abs (a, T, body)) = Abs (a, T, norm body) 240 | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) 241 | norm (f $ t) = 242 (case norm f of 243 Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) 244 | nf => nf $ t) 245 | norm _ = raise Same.SAME; 246 in Same.commit norm end; 247 248 249(* eta-long beta-normal form *) 250 251fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t) 252 | eta_long Ts t = 253 (case strip_comb t of 254 (Abs _, _) => eta_long Ts (beta_norm t) 255 | (u, ts) => 256 let 257 val Us = binder_types (fastype_of1 (Ts, t)); 258 val i = length Us; 259 val long = eta_long (rev Us @ Ts); 260 in 261 fold_rev (Term.abs o pair "x") Us 262 (list_comb (incr_boundvars i u, 263 map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0))) 264 end); 265 266 267(* full eta contraction *) 268 269local 270 271fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME 272 | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body) 273 | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u) 274 | decr _ _ = raise Same.SAME 275and decrh lev t = (decr lev t handle Same.SAME => t); 276 277fun eta (Abs (a, T, body)) = 278 ((case eta body of 279 body' as (f $ Bound 0) => 280 if Term.is_dependent f then Abs (a, T, body') 281 else decrh 0 f 282 | body' => Abs (a, T, body')) handle Same.SAME => 283 (case body of 284 f $ Bound 0 => 285 if Term.is_dependent f then raise Same.SAME 286 else decrh 0 f 287 | _ => raise Same.SAME)) 288 | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u) 289 | eta _ = raise Same.SAME; 290 291in 292 293fun eta_contract t = 294 if Term.could_eta_contract t then Same.commit eta t else t; 295 296end; 297 298val beta_eta_contract = eta_contract o beta_norm; 299 300fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u; 301 302 303fun body_type env (Type ("fun", [_, T])) = body_type env T 304 | body_type env (T as TVar v) = 305 (case Type.lookup (type_env env) v of 306 NONE => T 307 | SOME T' => body_type env T') 308 | body_type _ T = T; 309 310fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U 311 | binder_types env (TVar v) = 312 (case Type.lookup (type_env env) v of 313 NONE => [] 314 | SOME T' => binder_types env T') 315 | binder_types _ _ = []; 316 317fun strip_type env T = (binder_types env T, body_type env T); 318 319(*finds type of term without checking that combinations are consistent 320 Ts holds types of bound variables*) 321fun fastype (Envir {tyenv, ...}) = 322 let 323 val funerr = "fastype: expected function type"; 324 fun fast Ts (f $ u) = 325 (case Type.devar tyenv (fast Ts f) of 326 Type ("fun", [_, T]) => T 327 | TVar _ => raise TERM (funerr, [f $ u]) 328 | _ => raise TERM (funerr, [f $ u])) 329 | fast _ (Const (_, T)) = T 330 | fast _ (Free (_, T)) = T 331 | fast Ts (Bound i) = 332 (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i])) 333 | fast _ (Var (_, T)) = T 334 | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u; 335 in fast end; 336 337 338(** plain substitution -- without variable chasing **) 339 340local 341 342fun subst_type0 tyenv = Term_Subst.map_atypsT_same 343 (fn TVar v => 344 (case Type.lookup tyenv v of 345 SOME U => U 346 | NONE => raise Same.SAME) 347 | _ => raise Same.SAME); 348 349fun subst_term1 tenv = Term_Subst.map_aterms_same 350 (fn Var v => 351 (case lookup1 tenv v of 352 SOME u => u 353 | NONE => raise Same.SAME) 354 | _ => raise Same.SAME); 355 356fun subst_term2 tenv tyenv : term Same.operation = 357 let 358 val substT = subst_type0 tyenv; 359 fun subst (Const (a, T)) = Const (a, substT T) 360 | subst (Free (a, T)) = Free (a, substT T) 361 | subst (Var (xi, T)) = 362 (case lookup1 tenv (xi, T) of 363 SOME u => u 364 | NONE => Var (xi, substT T)) 365 | subst (Bound _) = raise Same.SAME 366 | subst (Abs (a, T, t)) = 367 (Abs (a, substT T, Same.commit subst t) 368 handle Same.SAME => Abs (a, T, subst t)) 369 | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); 370 in subst end; 371 372in 373 374fun subst_type_same tyenv T = 375 if Vartab.is_empty tyenv then raise Same.SAME 376 else subst_type0 tyenv T; 377 378fun subst_term_types_same tyenv t = 379 if Vartab.is_empty tyenv then raise Same.SAME 380 else Term_Subst.map_types_same (subst_type0 tyenv) t; 381 382fun subst_term_same (tyenv, tenv) = 383 if Vartab.is_empty tenv then subst_term_types_same tyenv 384 else if Vartab.is_empty tyenv then subst_term1 tenv 385 else subst_term2 tenv tyenv; 386 387fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T; 388fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t; 389fun subst_term envs t = subst_term_same envs t handle Same.SAME => t; 390 391end; 392 393 394 395(** expand defined atoms -- with local beta reduction **) 396 397fun expand_atom T (U, u) = 398 subst_term_types (Type.raw_match (U, T) Vartab.empty) u 399 handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]); 400 401fun expand_term get = 402 let 403 fun expand tm = 404 let 405 val (head, args) = Term.strip_comb tm; 406 val args' = map expand args; 407 fun comb head' = Term.list_comb (head', args'); 408 in 409 (case head of 410 Abs (x, T, t) => comb (Abs (x, T, expand t)) 411 | _ => 412 (case get head of 413 SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args') 414 | NONE => comb head)) 415 end; 416 in expand end; 417 418fun expand_term_frees defs = 419 let 420 val eqs = map (fn ((x, U), u) => (x, (U, u))) defs; 421 val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE; 422 in expand_term get end; 423 424end; 425