src/Pure/term_subst.ML
changeset 21184 35baf14cfb6d
parent 20513 4294eb252283
child 21315 be2669fe8363
equal deleted inserted replaced
21183:a76f457b6d86 21184:35baf14cfb6d
    79 
    79 
    80 (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
    80 (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
    81 
    81 
    82 local
    82 local
    83 
    83 
    84 val maxidx = ref ~1;
       
    85 fun maxify i = if i > ! maxidx then maxidx := i else ();
       
    86 
       
    87 fun no_index (x, y) = (x, (y, ~1));
    84 fun no_index (x, y) = (x, (y, ~1));
    88 fun no_indexes1 inst = map no_index inst;
    85 fun no_indexes1 inst = map no_index inst;
    89 fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
    86 fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
    90 
    87 
    91 exception SAME;
    88 exception SAME;
    92 
    89 
    93 fun instantiateT_same instT ty =
    90 fun instantiateT_same maxidx instT ty =
    94   let
    91   let
       
    92     fun maxify i = if i > ! maxidx then maxidx := i else ();
       
    93 
    95     fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
    94     fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
    96       | subst_typ (TVar ((a, i), S)) =
    95       | subst_typ (TVar ((a, i), S)) =
    97           (case AList.lookup Term.eq_tvar instT ((a, i), S) of
    96           (case AList.lookup Term.eq_tvar instT ((a, i), S) of
    98             SOME (T, j) => (maxify j; T)
    97             SOME (T, j) => (maxify j; T)
    99           | NONE => (maxify i; raise SAME))
    98           | NONE => (maxify i; raise SAME))
   102         (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   101         (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   103           handle SAME => T :: subst_typs Ts)
   102           handle SAME => T :: subst_typs Ts)
   104       | subst_typs [] = raise SAME;
   103       | subst_typs [] = raise SAME;
   105   in subst_typ ty end;
   104   in subst_typ ty end;
   106 
   105 
   107 fun instantiate_same (instT, inst) tm =
   106 fun instantiate_same maxidx (instT, inst) tm =
   108   let
   107   let
   109     val substT = instantiateT_same instT;
   108     fun maxify i = if i > ! maxidx then maxidx := i else ();
       
   109 
       
   110     val substT = instantiateT_same maxidx instT;
   110     fun subst (Const (c, T)) = Const (c, substT T)
   111     fun subst (Const (c, T)) = Const (c, substT T)
   111       | subst (Free (x, T)) = Free (x, substT T)
   112       | subst (Free (x, T)) = Free (x, substT T)
   112       | subst (Var ((x, i), T)) =
   113       | subst (Var ((x, i), T)) =
   113           let val (T', same) = (substT T, false) handle SAME => (T, true) in
   114           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             (case AList.lookup Term.eq_var inst ((x, i), T') of
   123   in subst tm end;
   124   in subst tm end;
   124 
   125 
   125 in
   126 in
   126 
   127 
   127 fun instantiateT_maxidx instT ty i =
   128 fun instantiateT_maxidx instT ty i =
   128   (maxidx := i; (instantiateT_same instT ty handle SAME => ty, ! maxidx));
   129   let val maxidx = ref i
       
   130   in (instantiateT_same maxidx instT ty handle SAME => ty, ! maxidx) end;
   129 
   131 
   130 fun instantiate_maxidx insts tm i =
   132 fun instantiate_maxidx insts tm i =
   131   (maxidx := i; (instantiate_same insts tm handle SAME => tm, ! maxidx));
   133   let val maxidx = ref i
       
   134   in (instantiate_same maxidx insts tm handle SAME => tm, ! maxidx) end;
   132 
   135 
   133 fun instantiateT instT ty = instantiateT_same (no_indexes1 instT) ty handle SAME => ty;
   136 fun instantiateT instT ty =
   134 fun instantiate insts tm = instantiate_same (no_indexes2 insts) tm handle SAME => tm;
   137   instantiateT_same (ref ~1) (no_indexes1 instT) ty handle SAME => ty;
       
   138 
       
   139 fun instantiate insts tm =
       
   140   instantiate_same (ref ~1) (no_indexes2 insts) tm handle SAME => tm;
   135 
   141 
   136 fun instantiateT_option instT ty =
   142 fun instantiateT_option instT ty =
   137   SOME (instantiateT_same (no_indexes1 instT) ty) handle SAME => NONE;
   143   SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle SAME => NONE;
   138 
   144 
   139 fun instantiate_option insts tm =
   145 fun instantiate_option insts tm =
   140   SOME (instantiate_same (no_indexes2 insts) tm) handle SAME => NONE;
   146   SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle SAME => NONE;
   141 
   147 
   142 end;
   148 end;
   143 
   149 
   144 
   150 
   145 (* zero var indexes *)
   151 (* zero var indexes *)