src/Pure/envir.ML
changeset 11513 2f6fe5b01521
parent 10485 f1576723371f
child 12231 4a25f04bea61
     1.1 --- a/src/Pure/envir.ML	Fri Aug 31 16:07:56 2001 +0200
     1.2 +++ b/src/Pure/envir.ML	Fri Aug 31 16:08:45 2001 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  signature ENVIR =
     1.5  sig
     1.6    datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
     1.7 +  exception SAME
     1.8    val genvars: string -> env * typ list -> env * term list
     1.9    val genvar: string -> env * typ -> env * term
    1.10    val lookup: env * indexname -> term option
    1.11 @@ -21,6 +22,10 @@
    1.12    val vupdate: (indexname * term) * env -> env
    1.13    val alist_of: env -> (indexname * term) list
    1.14    val norm_term: env -> term -> term
    1.15 +  val norm_term_same: env -> term -> term
    1.16 +  val norm_type: env -> typ -> typ
    1.17 +  val norm_type_same: env -> typ -> typ
    1.18 +  val norm_types_same: env -> typ list -> typ list
    1.19    val beta_norm: term -> term
    1.20  end;
    1.21  
    1.22 @@ -93,7 +98,7 @@
    1.23  (*raised when norm has no effect on a term, to do sharing instead of copying*)
    1.24  exception SAME;
    1.25  
    1.26 -fun norm_term1 (asol,t) : term =
    1.27 +fun norm_term1 same (asol,t) : term =
    1.28    let fun norm (Var (w,T)) =
    1.29              (case Vartab.lookup (asol, w) of
    1.30                  Some u => (norm u handle SAME => u)
    1.31 @@ -107,39 +112,53 @@
    1.32              handle SAME => f $ norm t)
    1.33          | norm _ =  raise SAME
    1.34        and normh t = norm t handle SAME => t
    1.35 -  in normh t end
    1.36 +  in (if same then norm else normh) t end
    1.37  
    1.38 -and norm_term2(asol,iTs,t) : term =
    1.39 -  let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
    1.40 -        | normT(TFree _) = raise SAME
    1.41 -        | normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
    1.42 -                Some(U) => normTh U
    1.43 -              | None => raise SAME)
    1.44 -      and normTh T = ((normT T) handle SAME => T)
    1.45 -      and normTs([]) = raise SAME
    1.46 -        | normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
    1.47 -                           handle SAME => T :: normTs Ts)
    1.48 -      and norm(Const(a,T)) = Const(a, normT T)
    1.49 -        | norm(Free(a,T)) = Free(a, normT T)
    1.50 -        | norm(Var (w,T)) =
    1.51 +fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
    1.52 +  | normT iTs (TFree _) = raise SAME
    1.53 +  | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
    1.54 +          Some U => normTh iTs U
    1.55 +        | None => raise SAME)
    1.56 +and normTh iTs T = ((normT iTs T) handle SAME => T)
    1.57 +and normTs iTs [] = raise SAME
    1.58 +  | normTs iTs (T :: Ts) =
    1.59 +      ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
    1.60 +       handle SAME => T :: normTs iTs Ts);
    1.61 +
    1.62 +fun norm_term2 same (asol, iTs, t) : term =
    1.63 +  let fun norm (Const (a, T)) = Const(a, normT iTs T)
    1.64 +        | norm (Free (a, T)) = Free(a, normT iTs T)
    1.65 +        | norm (Var (w, T)) =
    1.66              (case Vartab.lookup (asol, w) of
    1.67                  Some u => normh u
    1.68 -              | None   => Var(w,normT T))
    1.69 -        | norm(Abs(a,T,body)) =
    1.70 -              (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
    1.71 -        | norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
    1.72 -        | norm(f $ t) =
    1.73 +              | None   => Var(w, normT iTs T))
    1.74 +        | norm (Abs (a, T, body)) =
    1.75 +               (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
    1.76 +        | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
    1.77 +        | norm (f $ t) =
    1.78              ((case norm f of
    1.79 -               Abs(_,_,body) => normh(subst_bound (t, body))
    1.80 +               Abs(_, _, body) => normh (subst_bound (t, body))
    1.81               | nf => nf $ normh t)
    1.82              handle SAME => f $ norm t)
    1.83          | norm _ =  raise SAME
    1.84        and normh t = (norm t) handle SAME => t
    1.85 -  in normh t end;
    1.86 +  in (if same then norm else normh) t end;
    1.87  
    1.88 -fun norm_term (env as Envir{asol,iTs,...}) t : term =
    1.89 -  if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
    1.90 +fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
    1.91 +  if Vartab.is_empty iTs then norm_term1 same (asol, t)
    1.92 +  else norm_term2 same (asol, iTs, t);
    1.93 +
    1.94 +val norm_term = gen_norm_term false;
    1.95 +val norm_term_same = gen_norm_term true;
    1.96  
    1.97  val beta_norm = norm_term (empty 0);
    1.98  
    1.99 +fun norm_type (Envir {iTs, ...}) = normTh iTs;
   1.100 +fun norm_type_same (Envir {iTs, ...}) =
   1.101 +  if Vartab.is_empty iTs then raise SAME else normT iTs;
   1.102 +
   1.103 +fun norm_types_same (Envir {iTs, ...}) =
   1.104 +  if Vartab.is_empty iTs then raise SAME else normTs iTs;
   1.105 +
   1.106 +
   1.107  end;