wenzelm@247: (*  Title:      Pure/envir.ML
wenzelm@247:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@10485: 
berghofe@15797: Environments.  The type of a term variable / sort of a type variable is
berghofe@15797: part of its name. The lookup function must apply type substitutions,
berghofe@15797: since they may change the identity of a variable.
clasohm@0: *)
clasohm@0: 
wenzelm@247: signature ENVIR =
clasohm@0: sig
berghofe@15797:   type tenv
berghofe@15797:   datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
berghofe@15797:   val type_env: env -> Type.tyenv
wenzelm@26638:   val insert_sorts: env -> sort list -> sort list
berghofe@11513:   exception SAME
wenzelm@10485:   val genvars: string -> env * typ list -> env * term list
wenzelm@10485:   val genvar: string -> env * typ -> env * term
berghofe@15797:   val lookup: env * (indexname * typ) -> term option
berghofe@16652:   val lookup': tenv * (indexname * typ) -> term option
berghofe@15797:   val update: ((indexname * typ) * term) * env -> env
wenzelm@10485:   val empty: int -> env
wenzelm@10485:   val is_empty: env -> bool
wenzelm@19861:   val above: env -> int -> bool
berghofe@15797:   val vupdate: ((indexname * typ) * term) * env -> env
berghofe@15797:   val alist_of: env -> (indexname * (typ * term)) list
wenzelm@10485:   val norm_term: env -> term -> term
berghofe@11513:   val norm_term_same: env -> term -> term
berghofe@15797:   val norm_type: Type.tyenv -> typ -> typ
berghofe@15797:   val norm_type_same: Type.tyenv -> typ -> typ
berghofe@15797:   val norm_types_same: Type.tyenv -> typ list -> typ list
wenzelm@10485:   val beta_norm: term -> term
berghofe@12231:   val head_norm: env -> term -> term
wenzelm@18937:   val eta_contract: term -> term
wenzelm@18937:   val beta_eta_contract: term -> term
berghofe@12231:   val fastype: env -> typ list -> term -> typ
berghofe@15797:   val typ_subst_TVars: Type.tyenv -> typ -> typ
berghofe@15797:   val subst_TVars: Type.tyenv -> term -> term
berghofe@15797:   val subst_Vars: tenv -> term -> term
berghofe@15797:   val subst_vars: Type.tyenv * tenv -> term -> term
wenzelm@19422:   val expand_atom: typ -> typ * term -> term
wenzelm@21695:   val expand_term: (term -> (typ * term) option) -> term -> term
wenzelm@21795:   val expand_term_frees: ((string * typ) * term) list -> term -> term
clasohm@0: end;
clasohm@0: 
paulson@1500: structure Envir : ENVIR =
clasohm@0: struct
clasohm@0: 
clasohm@0: (*updating can destroy environment in 2 ways!!
clasohm@0:    (1) variables out of range   (2) circular assignments
clasohm@0: *)
berghofe@15797: type tenv = (typ * term) Vartab.table
berghofe@15797: 
clasohm@0: datatype env = Envir of
berghofe@15797:     {maxidx: int,      (*maximum index of vars*)
berghofe@15797:      asol: tenv,       (*table of assignments to Vars*)
berghofe@15797:      iTs: Type.tyenv}  (*table of assignments to TVars*)
clasohm@0: 
wenzelm@12496: fun type_env (Envir {iTs, ...}) = iTs;
clasohm@0: 
wenzelm@26638: (*NB: type unification may invent new sorts*)
wenzelm@26638: val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
wenzelm@26638: 
clasohm@0: (*Generate a list of distinct variables.
clasohm@0:   Increments index to make them distinct from ALL present variables. *)
clasohm@0: fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
clasohm@0:   let fun genvs (_, [] : typ list) : term list = []
clasohm@0:         | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
clasohm@0:         | genvs (n, T::Ts) =
wenzelm@247:             Var((name ^ radixstring(26,"a",n), maxidx+1), T)
wenzelm@247:             :: genvs(n+1,Ts)
clasohm@0:   in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
clasohm@0: 
clasohm@0: (*Generate a variable.*)
clasohm@0: fun genvar name (env,T) : env * term =
wenzelm@247:   let val (env',[v]) = genvars name (env,[T])
clasohm@0:   in  (env',v)  end;
clasohm@0: 
berghofe@15797: fun var_clash ixn T T' = raise TYPE ("Variable " ^
wenzelm@22678:   quote (Term.string_of_vname ixn) ^ " has two distinct types",
berghofe@15797:   [T', T], []);
clasohm@0: 
berghofe@15797: fun gen_lookup f asol (xname, T) =
wenzelm@17412:   (case Vartab.lookup asol xname of
berghofe@15797:      NONE => NONE
berghofe@15797:    | SOME (U, t) => if f (T, U) then SOME t
berghofe@15797:        else var_clash xname T U);
berghofe@15797: 
berghofe@16652: (* When dealing with environments produced by matching instead *)
berghofe@16652: (* of unification, there is no need to chase assigned TVars.   *)
berghofe@16652: (* In this case, we can simply ignore the type substitution    *)
berghofe@16652: (* and use = instead of eq_type.                               *)
berghofe@15797: 
berghofe@16652: fun lookup' (asol, p) = gen_lookup op = asol p;
berghofe@15797: 
berghofe@16652: fun lookup2 (iTs, asol) p =
berghofe@16652:   if Vartab.is_empty iTs then lookup' (asol, p)
berghofe@16652:   else gen_lookup (Type.eq_type iTs) asol p;
berghofe@15797: 
berghofe@15797: fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
berghofe@15797: 
berghofe@15797: fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
wenzelm@17412:   Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs};
clasohm@0: 
wenzelm@5289: (*The empty environment.  New variables will start with the given index+1.*)
berghofe@8407: fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
clasohm@0: 
paulson@2142: (*Test for empty environment*)
berghofe@8407: fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
wenzelm@247: 
paulson@2142: (*Determine if the least index updated exceeds lim*)
wenzelm@19861: fun above (Envir {asol, iTs, ...}) lim =
wenzelm@19861:   (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
wenzelm@19861:   (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
wenzelm@247: 
clasohm@0: (*Update, checking Var-Var assignments: try to suppress higher indexes*)
berghofe@15797: fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
berghofe@15797:       Var (nT as (name', T)) =>
berghofe@15797:         if a = name' then env     (*cycle!*)
wenzelm@29269:         else if TermOrd.indexname_ord (a, name') = LESS then
berghofe@15797:            (case lookup (env, nT) of  (*if already assigned, chase*)
berghofe@15797:                 NONE => update ((nT, Var (a, T)), env)
berghofe@15797:               | SOME u => vupdate ((aU, u), env))
berghofe@15797:         else update ((aU, t), env)
berghofe@15797:     | _ => update ((aU, t), env);
clasohm@0: 
clasohm@0: 
clasohm@0: (*Convert environment to alist*)
berghofe@8407: fun alist_of (Envir{asol,...}) = Vartab.dest asol;
clasohm@0: 
clasohm@0: 
paulson@1500: (*** Beta normal form for terms (not eta normal form).
paulson@1500:      Chases variables in env;  Does not exploit sharing of variable bindings
paulson@1500:      Does not check types, so could loop. ***)
paulson@1500: 
paulson@1500: (*raised when norm has no effect on a term, to do sharing instead of copying*)
paulson@1500: exception SAME;
clasohm@0: 
berghofe@11513: fun norm_term1 same (asol,t) : term =
berghofe@15797:   let fun norm (Var wT) =
berghofe@16652:             (case lookup' (asol, wT) of
skalberg@15531:                 SOME u => (norm u handle SAME => u)
skalberg@15531:               | NONE   => raise SAME)
wenzelm@10485:         | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
wenzelm@10485:         | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
wenzelm@10485:         | norm (f $ t) =
wenzelm@10485:             ((case norm f of
wenzelm@10485:                Abs(_,_,body) => normh(subst_bound (t, body))
wenzelm@10485:              | nf => nf $ (norm t handle SAME => t))
wenzelm@10485:             handle SAME => f $ norm t)
wenzelm@10485:         | norm _ =  raise SAME
paulson@2191:       and normh t = norm t handle SAME => t
berghofe@11513:   in (if same then norm else normh) t end
clasohm@0: 
berghofe@11513: fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
berghofe@11513:   | normT iTs (TFree _) = raise SAME
haftmann@26328:   | normT iTs (TVar vS) = (case Type.lookup iTs vS of
skalberg@15531:           SOME U => normTh iTs U
skalberg@15531:         | NONE => raise SAME)
berghofe@11513: and normTh iTs T = ((normT iTs T) handle SAME => T)
berghofe@11513: and normTs iTs [] = raise SAME
berghofe@11513:   | normTs iTs (T :: Ts) =
berghofe@11513:       ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
berghofe@11513:        handle SAME => T :: normTs iTs Ts);
berghofe@11513: 
berghofe@11513: fun norm_term2 same (asol, iTs, t) : term =
berghofe@11513:   let fun norm (Const (a, T)) = Const(a, normT iTs T)
berghofe@11513:         | norm (Free (a, T)) = Free(a, normT iTs T)
berghofe@11513:         | norm (Var (w, T)) =
berghofe@15797:             (case lookup2 (iTs, asol) (w, T) of
skalberg@15531:                 SOME u => normh u
skalberg@15531:               | NONE   => Var(w, normT iTs T))
berghofe@11513:         | norm (Abs (a, T, body)) =
berghofe@11513:                (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
berghofe@11513:         | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
berghofe@11513:         | norm (f $ t) =
wenzelm@10485:             ((case norm f of
berghofe@11513:                Abs(_, _, body) => normh (subst_bound (t, body))
wenzelm@10485:              | nf => nf $ normh t)
wenzelm@10485:             handle SAME => f $ norm t)
wenzelm@10485:         | norm _ =  raise SAME
paulson@1500:       and normh t = (norm t) handle SAME => t
berghofe@11513:   in (if same then norm else normh) t end;
clasohm@0: 
berghofe@11513: fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
berghofe@11513:   if Vartab.is_empty iTs then norm_term1 same (asol, t)
berghofe@11513:   else norm_term2 same (asol, iTs, t);
berghofe@11513: 
berghofe@11513: val norm_term = gen_norm_term false;
berghofe@11513: val norm_term_same = gen_norm_term true;
wenzelm@10485: 
berghofe@25471: fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
lcp@719: 
wenzelm@12496: fun norm_type iTs = normTh iTs;
wenzelm@12496: fun norm_type_same iTs =
berghofe@11513:   if Vartab.is_empty iTs then raise SAME else normT iTs;
berghofe@11513: 
wenzelm@12496: fun norm_types_same iTs =
berghofe@11513:   if Vartab.is_empty iTs then raise SAME else normTs iTs;
berghofe@11513: 
berghofe@11513: 
berghofe@12231: (*Put a term into head normal form for unification.*)
berghofe@12231: 
berghofe@12231: fun head_norm env t =
berghofe@12231:   let
berghofe@15797:     fun hnorm (Var vT) = (case lookup (env, vT) of
skalberg@15531:           SOME u => head_norm env u
skalberg@15531:         | NONE => raise SAME)
berghofe@12231:       | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
berghofe@12231:       | hnorm (Abs (_, _, body) $ t) =
berghofe@12231:           head_norm env (subst_bound (t, body))
berghofe@12231:       | hnorm (f $ t) = (case hnorm f of
berghofe@12231:           Abs (_, _, body) => head_norm env (subst_bound (t, body))
berghofe@12231:         | nf => nf $ t)
wenzelm@20670:           | hnorm _ =  raise SAME
berghofe@12231:   in hnorm t handle SAME => t end;
berghofe@12231: 
berghofe@12231: 
wenzelm@18937: (*Eta-contract a term (fully)*)
wenzelm@18937: 
wenzelm@22174: local
wenzelm@22174: 
wenzelm@22174: fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise SAME
wenzelm@22174:   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
wenzelm@22174:   | decr lev (t $ u) = (decr lev t $ decrh lev u handle SAME => t $ decr lev u)
wenzelm@22174:   | decr _ _ = raise SAME
wenzelm@22174: and decrh lev t = (decr lev t handle SAME => t);
wenzelm@20670: 
wenzelm@22174: fun eta (Abs (a, T, body)) =
wenzelm@22174:     ((case eta body of
wenzelm@22174:         body' as (f $ Bound 0) =>
wenzelm@22174:           if loose_bvar1 (f, 0) then Abs (a, T, body')
wenzelm@22174:           else decrh 0 f
wenzelm@22174:      | body' => Abs (a, T, body')) handle SAME =>
wenzelm@22174:         (case body of
wenzelm@22174:           f $ Bound 0 =>
wenzelm@22174:             if loose_bvar1 (f, 0) then raise SAME
wenzelm@22174:             else decrh 0 f
wenzelm@22174:         | _ => raise SAME))
wenzelm@22174:   | eta (t $ u) = (eta t $ etah u handle SAME => t $ eta u)
wenzelm@22174:   | eta _ = raise SAME
wenzelm@22174: and etah t = (eta t handle SAME => t);
wenzelm@22174: 
wenzelm@22174: in
wenzelm@22174: 
wenzelm@22174: fun eta_contract t =
wenzelm@24670:   if Term.has_abs t then etah t else t;
wenzelm@18937: 
wenzelm@18937: val beta_eta_contract = eta_contract o beta_norm;
wenzelm@18937: 
wenzelm@22174: end;
wenzelm@22174: 
wenzelm@18937: 
berghofe@12231: (*finds type of term without checking that combinations are consistent
berghofe@12231:   Ts holds types of bound variables*)
berghofe@12231: fun fastype (Envir {iTs, ...}) =
berghofe@12231: let val funerr = "fastype: expected function type";
berghofe@12231:     fun fast Ts (f $ u) =
wenzelm@20670:         (case fast Ts f of
wenzelm@20670:            Type ("fun", [_, T]) => T
wenzelm@20670:          | TVar ixnS =>
haftmann@26328:                 (case Type.lookup iTs ixnS of
wenzelm@20670:                    SOME (Type ("fun", [_, T])) => T
wenzelm@20670:                  | _ => raise TERM (funerr, [f $ u]))
wenzelm@20670:          | _ => raise TERM (funerr, [f $ u]))
berghofe@12231:       | fast Ts (Const (_, T)) = T
berghofe@12231:       | fast Ts (Free (_, T)) = T
berghofe@12231:       | fast Ts (Bound i) =
wenzelm@30146:         (nth Ts i
wenzelm@20670:          handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
wenzelm@20670:       | fast Ts (Var (_, T)) = T
berghofe@12231:       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
berghofe@12231: in fast end;
berghofe@12231: 
berghofe@15797: 
berghofe@15797: (*Substitute for type Vars in a type*)
berghofe@15797: fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
berghofe@15797:   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
berghofe@15797:         | subst(T as TFree _) = T
berghofe@15797:         | subst(T as TVar ixnS) =
haftmann@26328:             (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
berghofe@15797:   in subst T end;
berghofe@15797: 
berghofe@15797: (*Substitute for type Vars in a term*)
wenzelm@20548: val subst_TVars = map_types o typ_subst_TVars;
berghofe@15797: 
berghofe@15797: (*Substitute for Vars in a term *)
berghofe@15797: fun subst_Vars itms t = if Vartab.is_empty itms then t else
wenzelm@18937:   let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
berghofe@15797:         | subst (Abs (a, T, t)) = Abs (a, T, subst t)
berghofe@15797:         | subst (f $ t) = subst f $ subst t
berghofe@15797:         | subst t = t
berghofe@15797:   in subst t end;
berghofe@15797: 
berghofe@15797: (*Substitute for type/term Vars in a term *)
berghofe@16652: fun subst_vars (iTs, itms) =
berghofe@15797:   if Vartab.is_empty iTs then subst_Vars itms else
berghofe@15797:   let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
berghofe@15797:         | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
berghofe@16652:         | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
berghofe@15797:             NONE   => Var (ixn, typ_subst_TVars iTs T)
berghofe@15797:           | SOME t => t)
berghofe@15797:         | subst (b as Bound _) = b
berghofe@15797:         | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
berghofe@15797:         | subst (f $ t) = subst f $ subst t
berghofe@15797:   in subst end;
berghofe@15797: 
wenzelm@18937: 
wenzelm@21795: (* expand defined atoms -- with local beta reduction *)
wenzelm@18937: 
wenzelm@19422: fun expand_atom T (U, u) =
wenzelm@19422:   subst_TVars (Type.raw_match (U, T) Vartab.empty) u
wenzelm@18937:   handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
wenzelm@18937: 
wenzelm@21795: fun expand_term get =
wenzelm@21695:   let
wenzelm@21695:     fun expand tm =
wenzelm@21695:       let
wenzelm@21695:         val (head, args) = Term.strip_comb tm;
wenzelm@21695:         val args' = map expand args;
wenzelm@21695:         fun comb head' = Term.list_comb (head', args');
wenzelm@21695:       in
wenzelm@21695:         (case head of
wenzelm@21695:           Abs (x, T, t) => comb (Abs (x, T, expand t))
wenzelm@21695:         | _ =>
wenzelm@21795:             (case get head of
wenzelm@21695:               SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
wenzelm@21695:             | NONE => comb head)
wenzelm@21695:         | _ => comb head)
wenzelm@21695:       end;
wenzelm@21695:   in expand end;
wenzelm@21695: 
wenzelm@21795: fun expand_term_frees defs =
wenzelm@21795:   let
wenzelm@21795:     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
wenzelm@21795:     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
wenzelm@21795:   in expand_term get end;
wenzelm@21795: 
clasohm@0: end;