src/Pure/envir.ML
changeset 18937 0eb35519f0f3
parent 17412 e26cb20ef0cc
child 19422 bba26da0f227
equal deleted inserted replaced
18936:647528660980 18937:0eb35519f0f3
    29   val norm_type: Type.tyenv -> typ -> typ
    29   val norm_type: Type.tyenv -> typ -> typ
    30   val norm_type_same: Type.tyenv -> typ -> typ
    30   val norm_type_same: Type.tyenv -> typ -> typ
    31   val norm_types_same: Type.tyenv -> typ list -> typ list
    31   val norm_types_same: Type.tyenv -> typ list -> typ list
    32   val beta_norm: term -> term
    32   val beta_norm: term -> term
    33   val head_norm: env -> term -> term
    33   val head_norm: env -> term -> term
       
    34   val eta_contract: term -> term
       
    35   val beta_eta_contract: term -> term
    34   val fastype: env -> typ list -> term -> typ
    36   val fastype: env -> typ list -> term -> typ
    35   val typ_subst_TVars: Type.tyenv -> typ -> typ
    37   val typ_subst_TVars: Type.tyenv -> typ -> typ
    36   val subst_TVars: Type.tyenv -> term -> term
    38   val subst_TVars: Type.tyenv -> term -> term
    37   val subst_Vars: tenv -> term -> term
    39   val subst_Vars: tenv -> term -> term
    38   val subst_vars: Type.tyenv * tenv -> term -> term
    40   val subst_vars: Type.tyenv * tenv -> term -> term
       
    41   val expand_atom: Type.tsig -> typ -> typ * term -> term
    39 end;
    42 end;
    40 
    43 
    41 structure Envir : ENVIR =
    44 structure Envir : ENVIR =
    42 struct
    45 struct
    43 
    46 
   207       | hnorm (f $ t) = (case hnorm f of
   210       | hnorm (f $ t) = (case hnorm f of
   208           Abs (_, _, body) => head_norm env (subst_bound (t, body))
   211           Abs (_, _, body) => head_norm env (subst_bound (t, body))
   209         | nf => nf $ t)
   212         | nf => nf $ t)
   210 	  | hnorm _ =  raise SAME
   213 	  | hnorm _ =  raise SAME
   211   in hnorm t handle SAME => t end;
   214   in hnorm t handle SAME => t end;
       
   215 
       
   216 
       
   217 (*Eta-contract a term (fully)*)
       
   218 
       
   219 fun eta_contract t =
       
   220   let
       
   221     exception SAME;
       
   222     fun eta (Abs (a, T, body)) =
       
   223       ((case eta body of
       
   224           body' as (f $ Bound 0) =>
       
   225             if loose_bvar1 (f, 0) then Abs(a, T, body')
       
   226             else incr_boundvars ~1 f
       
   227         | body' => Abs (a, T, body')) handle SAME =>
       
   228        (case body of
       
   229           (f $ Bound 0) =>
       
   230             if loose_bvar1 (f, 0) then raise SAME
       
   231             else incr_boundvars ~1 f
       
   232         | _ => raise SAME))
       
   233       | eta (f $ t) =
       
   234           (let val f' = eta f
       
   235            in f' $ etah t end handle SAME => f $ eta t)
       
   236       | eta _ = raise SAME
       
   237     and etah t = (eta t handle SAME => t)
       
   238   in etah t end;
       
   239 
       
   240 val beta_eta_contract = eta_contract o beta_norm;
   212 
   241 
   213 
   242 
   214 (*finds type of term without checking that combinations are consistent
   243 (*finds type of term without checking that combinations are consistent
   215   Ts holds types of bound variables*)
   244   Ts holds types of bound variables*)
   216 fun fastype (Envir {iTs, ...}) =
   245 fun fastype (Envir {iTs, ...}) =
   244 (*Substitute for type Vars in a term*)
   273 (*Substitute for type Vars in a term*)
   245 val subst_TVars = map_term_types o typ_subst_TVars;
   274 val subst_TVars = map_term_types o typ_subst_TVars;
   246 
   275 
   247 (*Substitute for Vars in a term *)
   276 (*Substitute for Vars in a term *)
   248 fun subst_Vars itms t = if Vartab.is_empty itms then t else
   277 fun subst_Vars itms t = if Vartab.is_empty itms then t else
   249   let fun subst (v as Var ixnT) = getOpt (lookup' (itms, ixnT), v)
   278   let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
   250         | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   279         | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   251         | subst (f $ t) = subst f $ subst t
   280         | subst (f $ t) = subst f $ subst t
   252         | subst t = t
   281         | subst t = t
   253   in subst t end;
   282   in subst t end;
   254 
   283 
   263         | subst (b as Bound _) = b
   292         | subst (b as Bound _) = b
   264         | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
   293         | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
   265         | subst (f $ t) = subst f $ subst t
   294         | subst (f $ t) = subst f $ subst t
   266   in subst end;
   295   in subst end;
   267 
   296 
       
   297 
       
   298 (* expand_atom *)
       
   299 
       
   300 fun expand_atom tsig T (U, u) =
       
   301   subst_TVars (Type.typ_match tsig (U, T) Vartab.empty) u
       
   302   handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
       
   303 
   268 end;
   304 end;