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