src/Pure/envir.ML

HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)

Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.

Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:

idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.

Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.

(*  Title:      Pure/envir.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1988  University of Cambridge
*)

(*Environments
  Should take account that typ is part of variable name,
    otherwise two variables with same name and different types
    will cause errors!
*)


signature ENVIR =
sig
  type 'a xolist
  exception ENVIR of string * indexname;
  datatype env = Envir of {asol: term xolist,
                           iTs: (indexname * typ) list,
                           maxidx: int}
  val alist_of		: env -> (indexname * term) list
  val alist_of_olist	: 'a xolist -> (indexname * 'a) list
  val empty		: int->env
  val is_empty		: env -> bool
  val minidx		: env -> int option
  val genvar		: string -> env * typ -> env * term
  val genvars		: string -> env * typ list -> env * term list
  val lookup		: env * indexname -> term option
  val norm_term		: env -> term -> term
  val null_olist	: 'a xolist
  val olist_of_alist	: (indexname * 'a) list -> 'a xolist
  val update		: (indexname * term) * env -> env
  val vupdate		: (indexname * term) * env -> env
end;

functor EnvirFun () : ENVIR =
struct


(*association lists with keys in ascending order, no repeated keys*)
datatype 'a xolist = Olist of (indexname * 'a) list;


exception ENVIR of string * indexname;

(*look up key in ordered list*)
fun xsearch (Olist[], key) = None
  | xsearch (Olist ((keyi,xi)::pairs), key) =
      if xless(keyi,key) then xsearch (Olist pairs, key)
      else if key=keyi then Some xi
      else None;

(*insert pair in ordered list, reject if key already present*)
fun xinsert_new (newpr as (key, x), Olist al) =
  let fun insert [] = [newpr]
        | insert ((pair as (keyi,xi)) :: pairs) =
            if xless(keyi,key) then pair :: insert pairs
            else if key=keyi then
                raise ENVIR("xinsert_new: already present",key)
            else newpr::pair::pairs
  in  Olist (insert al)  end;

(*insert pair in ordered list, overwrite if key already present*)
fun xinsert (newpr as (key, x), Olist al) =
  let fun insert [] = [newpr]
        | insert ((pair as (keyi,xi)) :: pairs) =
            if xless(keyi,key) then pair :: insert pairs
            else if key=keyi then newpr::pairs
            else newpr::pair::pairs
  in  Olist (insert al)  end;

(*apply function to the contents part of each pair*)
fun xmap f (Olist pairs) =
  let fun xmp [] = []
        | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
  in Olist (xmp pairs)  end;

(*allows redefinition of a key by "join"ing the contents parts*)
fun xmerge_olists join (Olist pairsa, Olist pairsb) =
  let fun xmrg ([],pairsb) = pairsb
        | xmrg (pairsa,[]) = pairsa
        | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
            if xless(keya,keyb) then
                (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
            else if xless(keyb,keya) then
                (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
            else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
  in  Olist (xmrg (pairsa,pairsb))  end;

val null_olist = Olist[];

fun alist_of_olist (Olist pairs) = pairs;

fun olist_of_alist pairs = foldr xinsert (pairs, Olist[]);



(*updating can destroy environment in 2 ways!!
   (1) variables out of range   (2) circular assignments
*)
datatype env = Envir of
    {maxidx: int,               (*maximum index of vars*)
     asol: term xolist,         (*table of assignments to Vars*)
     iTs: (indexname*typ)list}  (*table of assignments to TVars*)


(*Generate a list of distinct variables.
  Increments index to make them distinct from ALL present variables. *)
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
  let fun genvs (_, [] : typ list) : term list = []
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
        | genvs (n, T::Ts) =
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
            :: genvs(n+1,Ts)
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;

(*Generate a variable.*)
fun genvar name (env,T) : env * term =
  let val (env',[v]) = genvars name (env,[T])
  in  (env',v)  end;

fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);

fun update ((xname, t), Envir{maxidx, asol, iTs}) =
  Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};

(*The empty environment.  New variables will start with the given index.*)
fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};

(*is_empty*)
fun is_empty (Envir {asol = Olist [], iTs = [], ...}) = true
  | is_empty _ = false;

(*minidx*)
fun minidx (Envir {asol = Olist asns, iTs, ...}) =
  (case (asns, iTs) of
    ([], []) => None
  | (((_, i), _) :: _, _) => Some (min (i :: map (snd o fst) iTs))
  | _ => Some (min (map (snd o fst) iTs)));

(*Update, checking Var-Var assignments: try to suppress higher indexes*)
fun vupdate((a,t), env) = case t of
      Var(name',T) =>
        if a=name' then env     (*cycle!*)
        else if xless(a, name')  then
           (case lookup(env,name') of  (*if already assigned, chase*)
                None => update((name', Var(a,T)), env)
              | Some u => vupdate((a,u), env))
        else update((a,t), env)
    | _ => update((a,t), env);


(*Convert environment to alist*)
fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;


(*Beta normal form for terms (not eta normal form).
  Chases variables in env;  Does not exploit sharing of variable bindings
  Does not check types, so could loop. *)
local
      (*raised when norm has no effect on a term,
        to encourage sharing instead of copying*)
  exception SAME;

  fun norm_term1 (asol,t) : term =
    let fun norm (Var (w,T)) =
              (case xsearch(asol,w) of
                  Some u => normh u
                | None   => raise SAME)
          | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
          | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
          | norm (f $ t) =
              ((case norm f of
                 Abs(_,_,body) => normh(subst_bounds([t], body))
               | nf => nf $ normh t)
              handle SAME => f $ norm t)
          | norm _ =  raise SAME
        and normh t = (norm t) handle SAME => t
    in normh t end

  and norm_term2(asol,iTs,t) : term =
    let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
          | normT(TFree _) = raise SAME
          | normT(TVar(v,_)) = (case assoc(iTs,v) of
                  Some(U) => normTh U
                | None => raise SAME)
        and normTh T = ((normT T) handle SAME => T)
        and normTs([]) = raise SAME
          | normTs(T::Ts) = ((normT T :: normTsh Ts)
                             handle SAME => T :: normTs Ts)
        and normTsh Ts = ((normTs Ts) handle SAME => Ts)
        and norm(Const(a,T)) = Const(a, normT T)
          | norm(Free(a,T)) = Free(a, normT T)
          | norm(Var (w,T)) =
              (case xsearch(asol,w) of
                  Some u => normh u
                | None   => Var(w,normT T))
          | norm(Abs(a,T,body)) =
                (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
          | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
          | norm(f $ t) =
              ((case norm f of
                 Abs(_,_,body) => normh(subst_bounds([t], body))
               | nf => nf $ normh t)
              handle SAME => f $ norm t)
          | norm _ =  raise SAME
        and normh t = (norm t) handle SAME => t
    in normh t end;

in

(*curried version might be slower in recursive calls*)
fun norm_term (env as Envir{asol,iTs,...}) t : term =
        if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)

fun norm_ter (env as Envir{asol,iTs,...}) t : term =
        if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)

end;

end;