src/Pure/term_subst.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 21607 3698319f6503
child 29269 5c25a2012975
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      Pure/term_subst.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Efficient term substitution -- avoids copying.
     6 *)
     7 
     8 signature TERM_SUBST =
     9 sig
    10   val generalize: string list * string list -> int -> term -> term
    11   val generalizeT: string list -> int -> typ -> typ
    12   val generalize_option: string list * string list -> int -> term -> term option
    13   val generalizeT_option: string list -> int -> typ -> typ option
    14   val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int
    15   val instantiate_maxidx:
    16     ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
    17     term -> int -> term * int
    18   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    19     term -> term
    20   val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    21   val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    22     term -> term option
    23   val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
    24   val zero_var_indexes: term -> term
    25   val zero_var_indexes_inst: term list ->
    26     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    27 end;
    28 
    29 structure TermSubst: TERM_SUBST =
    30 struct
    31 
    32 (* generalization of fixed variables *)
    33 
    34 local
    35 
    36 exception SAME;
    37 
    38 fun generalizeT_same [] _ _ = raise SAME
    39   | generalizeT_same tfrees idx ty =
    40       let
    41         fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
    42           | gen_typ (TFree (a, S)) =
    43               if member (op =) tfrees a then TVar ((a, idx), S)
    44               else raise SAME
    45           | gen_typ _ = raise SAME
    46         and gen_typs (T :: Ts) =
    47             (gen_typ T :: (gen_typs Ts handle SAME => Ts)
    48               handle SAME => T :: gen_typs Ts)
    49           | gen_typs [] = raise SAME;
    50       in gen_typ ty end;
    51 
    52 fun generalize_same ([], []) _ _ = raise SAME
    53   | generalize_same (tfrees, frees) idx tm =
    54       let
    55         val genT = generalizeT_same tfrees idx;
    56         fun gen (Free (x, T)) =
    57               if member (op =) frees x then
    58                 Var (Name.clean_index (x, idx), genT T handle SAME => T)
    59               else Free (x, genT T)
    60           | gen (Var (xi, T)) = Var (xi, genT T)
    61           | gen (Const (c, T)) = Const (c, genT T)
    62           | gen (Bound _) = raise SAME
    63           | gen (Abs (x, T, t)) =
    64               (Abs (x, genT T, gen t handle SAME => t)
    65                 handle SAME => Abs (x, T, gen t))
    66           | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u);
    67       in gen tm end;
    68 
    69 in
    70 
    71 fun generalize names i tm = generalize_same names i tm handle SAME => tm;
    72 fun generalizeT names i ty = generalizeT_same names i ty handle SAME => ty;
    73 
    74 fun generalize_option names i tm = SOME (generalize_same names i tm) handle SAME => NONE;
    75 fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle SAME => NONE;
    76 
    77 end;
    78 
    79 
    80 (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
    81 
    82 local
    83 
    84 fun no_index (x, y) = (x, (y, ~1));
    85 fun no_indexes1 inst = map no_index inst;
    86 fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
    87 
    88 exception SAME;
    89 
    90 fun instantiateT_same maxidx instT ty =
    91   let
    92     fun maxify i = if i > ! maxidx then maxidx := i else ();
    93 
    94     fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
    95       | subst_typ (TVar ((a, i), S)) =
    96           (case AList.lookup Term.eq_tvar instT ((a, i), S) of
    97             SOME (T, j) => (maxify j; T)
    98           | NONE => (maxify i; raise SAME))
    99       | subst_typ _ = raise SAME
   100     and subst_typs (T :: Ts) =
   101         (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   102           handle SAME => T :: subst_typs Ts)
   103       | subst_typs [] = raise SAME;
   104   in subst_typ ty end;
   105 
   106 fun instantiate_same maxidx (instT, inst) tm =
   107   let
   108     fun maxify i = if i > ! maxidx then maxidx := i else ();
   109 
   110     val substT = instantiateT_same maxidx instT;
   111     fun subst (Const (c, T)) = Const (c, substT T)
   112       | subst (Free (x, T)) = Free (x, substT T)
   113       | subst (Var ((x, i), T)) =
   114           let val (T', same) = (substT T, false) handle SAME => (T, true) in
   115             (case AList.lookup Term.eq_var inst ((x, i), T') of
   116                SOME (t, j) => (maxify j; t)
   117              | NONE => (maxify i; if same then raise SAME else Var ((x, i), T')))
   118           end
   119       | subst (Bound _) = raise SAME
   120       | subst (Abs (x, T, t)) =
   121           (Abs (x, substT T, subst t handle SAME => t)
   122             handle SAME => Abs (x, T, subst t))
   123       | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
   124   in subst tm end;
   125 
   126 in
   127 
   128 fun instantiateT_maxidx instT ty i =
   129   let val maxidx = ref i
   130   in (instantiateT_same maxidx instT ty handle SAME => ty, ! maxidx) end;
   131 
   132 fun instantiate_maxidx insts tm i =
   133   let val maxidx = ref i
   134   in (instantiate_same maxidx insts tm handle SAME => tm, ! maxidx) end;
   135 
   136 fun instantiateT [] ty = ty
   137   | instantiateT instT ty =
   138       (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle SAME => ty);
   139 
   140 fun instantiate ([], []) tm = tm
   141   | instantiate insts tm =
   142       (instantiate_same (ref ~1) (no_indexes2 insts) tm handle SAME => tm);
   143 
   144 fun instantiateT_option [] _ = NONE
   145   | instantiateT_option instT ty =
   146       (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle SAME => NONE);
   147 
   148 fun instantiate_option ([], []) _ = NONE
   149   | instantiate_option insts tm =
   150       (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle SAME => NONE);
   151 
   152 end;
   153 
   154 
   155 (* zero var indexes *)
   156 
   157 fun zero_var_inst vars =
   158   fold (fn v as ((x, i), X) => fn (inst, used) =>
   159     let
   160       val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
   161     in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
   162   vars ([], Name.context) |> #1;
   163 
   164 fun zero_var_indexes_inst ts =
   165   let
   166     val tvars = sort Term.tvar_ord (fold Term.add_tvars ts []);
   167     val instT = map (apsnd TVar) (zero_var_inst tvars);
   168     val vars = sort Term.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
   169     val inst = map (apsnd Var) (zero_var_inst vars);
   170   in (instT, inst) end;
   171 
   172 fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;
   173 
   174 end;