added add_tfreesT, add_tfrees;
authorwenzelm
Thu Jul 28 15:20:00 2005 +0200 (2005-07-28)
changeset 16943ba05effdec42
parent 16942 c01816b32c04
child 16944 83ea7e3c6ec9
added add_tfreesT, add_tfrees;
added bound;
added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst;
removed add_term_constsT;
tuned;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu Jul 28 15:19:59 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jul 28 15:20:00 2005 +0200
     1.3 @@ -68,6 +68,13 @@
     1.4    val map_type_tfree: (string * sort -> typ) -> typ -> typ
     1.5    val map_term_types: (typ -> typ) -> term -> term
     1.6    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
     1.7 +  val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
     1.8 +  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
     1.9 +  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.10 +  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.11 +  val add_term_names: term * string list -> string list
    1.12 +  val add_term_varnames: term -> indexname list -> indexname list
    1.13 +  val term_varnames: term -> indexname list
    1.14    val aconv: term * term -> bool
    1.15    val aconvs: term list * term list -> bool
    1.16    structure Vartab: TABLE
    1.17 @@ -127,12 +134,9 @@
    1.18    val add_term_classes: term * class list -> class list
    1.19    val add_term_tycons: term * string list -> string list
    1.20    val add_term_consts: term * string list -> string list
    1.21 -  val add_term_constsT: term * (string * typ) list -> (string * typ) list
    1.22    val term_consts: term -> string list
    1.23 -  val term_constsT: term -> (string * typ) list
    1.24 +  val exists_subterm: (term -> bool) -> term -> bool
    1.25    val exists_Const: (string * typ -> bool) -> term -> bool
    1.26 -  val exists_subterm: (term -> bool) -> term -> bool
    1.27 -  val add_new_id: string list * string -> string list
    1.28    val add_term_free_names: term * string list -> string list
    1.29    val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
    1.30    val add_typ_tfree_names: typ * string list -> string list
    1.31 @@ -156,13 +160,6 @@
    1.32    val term_frees: term -> term list
    1.33    val variant_abs: string * typ * term -> string * term
    1.34    val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
    1.35 -  val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    1.36 -  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    1.37 -  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.38 -  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.39 -  val add_term_names: term * string list -> string list
    1.40 -  val add_term_varnames: term -> indexname list -> indexname list
    1.41 -  val term_varnames: term -> indexname list
    1.42    val compress_type: typ -> typ
    1.43    val compress_term: term -> term
    1.44    val show_question_marks: bool ref
    1.45 @@ -172,6 +169,12 @@
    1.46  sig
    1.47    include BASIC_TERM
    1.48    val argument_type_of: term -> typ
    1.49 +  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.50 +  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.51 +  val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
    1.52 +  val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
    1.53 +  val add_tfrees: term -> (string * sort) list -> (string * sort) list
    1.54 +  val add_frees: term -> (string * typ) list -> (string * typ) list
    1.55    val fast_indexname_ord: indexname * indexname -> order
    1.56    val indexname_ord: indexname * indexname -> order
    1.57    val sort_ord: sort * sort -> order
    1.58 @@ -183,8 +186,10 @@
    1.59    val term_lpo: (string -> int) -> term * term -> order
    1.60    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    1.61    val rename_abs: term -> term -> term -> term option
    1.62 +  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
    1.63    val eq_var: (indexname * typ) * (indexname * typ) -> bool
    1.64 -  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
    1.65 +  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
    1.66 +  val var_ord: (indexname * typ) * (indexname * typ) -> order
    1.67    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.68      -> term -> term
    1.69    val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    1.70 @@ -195,10 +200,11 @@
    1.71    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
    1.72    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
    1.73    val dest_abs: string * typ * term -> string * term
    1.74 -  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.75 -  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.76 -  val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
    1.77 -  val add_frees: term -> (string * typ) list -> (string * typ) list
    1.78 +  val bound: int -> string -> string
    1.79 +  val zero_var_indexesT: typ -> typ
    1.80 +  val zero_var_indexes: term -> term
    1.81 +  val zero_var_indexes_inst: term ->
    1.82 +    ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.83    val dummy_patternN: string
    1.84    val no_dummy_patterns: term -> term
    1.85    val replace_dummy_patterns: int * term -> int * term
    1.86 @@ -466,6 +472,40 @@
    1.87  in iter end
    1.88  
    1.89  
    1.90 +(* fold types and terms *)
    1.91 +
    1.92 +(*fold atoms of type*)
    1.93 +fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
    1.94 +  | fold_atyps f T = f T;
    1.95 +
    1.96 +(*fold atoms of term*)
    1.97 +fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
    1.98 +  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
    1.99 +  | fold_aterms f a = f a;
   1.100 +
   1.101 +(*fold types of term*)
   1.102 +fun fold_term_types f (t as Const (_, T)) = f t T
   1.103 +  | fold_term_types f (t as Free (_, T)) = f t T
   1.104 +  | fold_term_types f (t as Var (_, T)) = f t T
   1.105 +  | fold_term_types f (Bound _) = I
   1.106 +  | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   1.107 +  | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   1.108 +
   1.109 +fun fold_types f = fold_term_types (K f);
   1.110 +
   1.111 +(*collect variables*)
   1.112 +val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   1.113 +val add_tvars = fold_types add_tvarsT;
   1.114 +val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   1.115 +val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   1.116 +val add_tfrees = fold_types add_tfreesT;
   1.117 +val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   1.118 +
   1.119 +(*collect variable names*)
   1.120 +val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   1.121 +fun term_varnames t = add_term_varnames t [];
   1.122 +
   1.123 +
   1.124  (** Comparing terms, types, sorts etc. **)
   1.125  
   1.126  (* fast syntactic comparison *)
   1.127 @@ -584,14 +624,8 @@
   1.128      | (t, u) =>
   1.129          (case int_ord (size_of_term t, size_of_term u) of
   1.130            EQUAL =>
   1.131 -            let
   1.132 -              val (f, m) = hd_depth (t, 0)
   1.133 -              and (g, n) = hd_depth (u, 0);
   1.134 -            in
   1.135 -              (case hd_ord (f, g) of EQUAL =>
   1.136 -                (case int_ord (m, n) of EQUAL => args_ord (t, u) | ord => ord)
   1.137 -              | ord => ord)
   1.138 -            end
   1.139 +            (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
   1.140 +              EQUAL => args_ord (t, u) | ord => ord)
   1.141          | ord => ord))
   1.142  and hd_ord (f, g) =
   1.143    prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   1.144 @@ -781,8 +815,11 @@
   1.145  
   1.146  (* variables *)
   1.147  
   1.148 -fun eq_var ((xi, T: typ), (yj, U)) = eq_ix (xi, yj) andalso T = U;
   1.149 -fun eq_tvar ((xi, S: sort), (yj, S')) = eq_ix (xi, yj) andalso S = S';
   1.150 +fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   1.151 +fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   1.152 +
   1.153 +val tvar_ord = prod_ord indexname_ord sort_ord;
   1.154 +val var_ord = prod_ord indexname_ord typ_ord;
   1.155  
   1.156  
   1.157  (* terms *)
   1.158 @@ -933,12 +970,12 @@
   1.159        in subst tm end;
   1.160  
   1.161  
   1.162 -(* efficient substitution of schematic variables *)
   1.163 +(* instantiation of schematic variables (types before terms) *)
   1.164  
   1.165  local exception SAME in
   1.166  
   1.167 -fun substT [] _ = raise SAME
   1.168 -  | substT instT ty =
   1.169 +fun instantiateT_same [] _ = raise SAME
   1.170 +  | instantiateT_same instT ty =
   1.171        let
   1.172          fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
   1.173            | subst_typ (TVar v) =
   1.174 @@ -955,23 +992,24 @@
   1.175  fun instantiate ([], []) tm = tm
   1.176    | instantiate (instT, inst) tm =
   1.177        let
   1.178 -        fun subst (Const (c, T)) = Const (c, substT instT T)
   1.179 -          | subst (Free (x, T)) = Free (x, substT instT T)
   1.180 +        val substT = instantiateT_same instT;
   1.181 +        fun subst (Const (c, T)) = Const (c, substT T)
   1.182 +          | subst (Free (x, T)) = Free (x, substT T)
   1.183            | subst (Var (xi, T)) =
   1.184 -              let val (T', same) = (substT instT T, false) handle SAME => (T, true) in
   1.185 +              let val (T', same) = (substT T, false) handle SAME => (T, true) in
   1.186                  (case gen_assoc eq_var (inst, (xi, T')) of
   1.187                     SOME t => t
   1.188                   | NONE => if same then raise SAME else Var (xi, T'))
   1.189                end
   1.190            | subst (Bound _) = raise SAME
   1.191            | subst (Abs (x, T, t)) =
   1.192 -              (Abs (x, substT instT T, subst t handle SAME => t)
   1.193 +              (Abs (x, substT T, subst t handle SAME => t)
   1.194                  handle SAME => Abs (x, T, subst t))
   1.195            | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
   1.196        in subst tm handle SAME => tm end;
   1.197  
   1.198  fun instantiateT instT ty =
   1.199 -  substT instT ty handle SAME => ty;
   1.200 +  instantiateT_same instT ty handle SAME => ty;
   1.201  
   1.202  end;
   1.203  
   1.204 @@ -1025,14 +1063,14 @@
   1.205  
   1.206  (*** Printing ***)
   1.207  
   1.208 -(*Makes a variant of a name distinct from the names in bs.
   1.209 +(*Makes a variant of a name distinct from the names in 'used'.
   1.210    First attaches the suffix and then increments this;
   1.211    preserves a suffix of underscores "_". *)
   1.212 -fun variant bs name =
   1.213 +fun variant used name =
   1.214    let
   1.215      val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
   1.216 -    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
   1.217 -    fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c;
   1.218 +    fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c;
   1.219 +    fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c;
   1.220    in vary1 (if c = "" then "u" else c) ^ u end;
   1.221  
   1.222  (*Create variants of the list of names, with priority to the first ones*)
   1.223 @@ -1067,29 +1105,18 @@
   1.224    | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   1.225    | add_term_consts (_, cs) = cs;
   1.226  
   1.227 -fun add_term_constsT (Const c, cs) = c::cs
   1.228 -  | add_term_constsT (t $ u, cs) = add_term_constsT (t, add_term_constsT (u, cs))
   1.229 -  | add_term_constsT (Abs (_, _, t), cs) = add_term_constsT (t, cs)
   1.230 -  | add_term_constsT (_, cs) = cs;
   1.231 -
   1.232  fun term_consts t = add_term_consts(t,[]);
   1.233  
   1.234 -fun term_constsT t = add_term_constsT(t,[]);
   1.235 +fun exists_subterm P =
   1.236 +  let
   1.237 +    fun ex tm = P tm orelse
   1.238 +      (case tm of
   1.239 +        t $ u => ex t orelse ex u
   1.240 +      | Abs (_, _, t) => ex t
   1.241 +      | _ => false);
   1.242 +  in ex end;
   1.243  
   1.244 -fun exists_Const P t = let
   1.245 -        fun ex (Const c      ) = P c
   1.246 -        |   ex (t $ u        ) = ex t orelse ex u
   1.247 -        |   ex (Abs (_, _, t)) = ex t
   1.248 -        |   ex _               = false
   1.249 -    in ex t end;
   1.250 -
   1.251 -fun exists_subterm P =
   1.252 -  let fun ex t = P t orelse
   1.253 -                 (case t of
   1.254 -                    u $ v        => ex u orelse ex v
   1.255 -                  | Abs(_, _, u) => ex u
   1.256 -                  | _            => false)
   1.257 -  in ex end;
   1.258 +fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   1.259  
   1.260  (*map classes, tycons*)
   1.261  fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   1.262 @@ -1107,9 +1134,6 @@
   1.263  
   1.264  (** TFrees and TVars **)
   1.265  
   1.266 -(*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   1.267 -fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   1.268 -
   1.269  (*Accumulates the names of Frees in the term, suppressing duplicates.*)
   1.270  fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   1.271    | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   1.272 @@ -1228,6 +1252,8 @@
   1.273      else (x, subst_bound (Free (x, T), body))
   1.274    end;
   1.275  
   1.276 +fun bound bounds x = "." ^ x ^ "." ^ string_of_int bounds;
   1.277 +
   1.278  (* renames and reverses the strings in vars away from names *)
   1.279  fun rename_aTs names vars : (string*typ)list =
   1.280    let fun rename_aT (vars,(a,T)) =
   1.281 @@ -1237,36 +1263,28 @@
   1.282  fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   1.283  
   1.284  
   1.285 -(* left-ro-right traversal *)
   1.286 +(* zero var indexes *)
   1.287  
   1.288 -(*fold atoms of type*)
   1.289 -fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   1.290 -  | fold_atyps f T = f T;
   1.291 -
   1.292 -(*fold atoms of term*)
   1.293 -fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   1.294 -  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   1.295 -  | fold_aterms f a = f a;
   1.296 +fun zero_var_inst vars =
   1.297 +  fold (fn v as ((x, i), X) => fn (used, inst) =>
   1.298 +    let
   1.299 +      val x' = variant used x;
   1.300 +      val used' = x' :: used;
   1.301 +    in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
   1.302 +  vars ([], []) |> #2;
   1.303  
   1.304 -(*fold types of term*)
   1.305 -fun fold_term_types f (t as Const (_, T)) = f t T
   1.306 -  | fold_term_types f (t as Free (_, T)) = f t T
   1.307 -  | fold_term_types f (t as Var (_, T)) = f t T
   1.308 -  | fold_term_types f (Bound _) = I
   1.309 -  | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   1.310 -  | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   1.311 -
   1.312 -fun fold_types f = fold_term_types (K f);
   1.313 +fun zero_var_indexesT ty =
   1.314 +  instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
   1.315  
   1.316 -(*collect variables*)
   1.317 -val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   1.318 -val add_tvars = fold_types add_tvarsT;
   1.319 -val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   1.320 -val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   1.321 +fun zero_var_indexes_inst tm =
   1.322 +  let
   1.323 +    val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm [])));
   1.324 +    val inst =
   1.325 +      add_vars tm [] |> map (apsnd (instantiateT instT))
   1.326 +      |> sort var_ord |> zero_var_inst |> map (apsnd Var);
   1.327 +  in (instT, inst) end;
   1.328  
   1.329 -(*collect variable names*)
   1.330 -val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   1.331 -fun term_varnames t = add_term_varnames t [];
   1.332 +fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;
   1.333  
   1.334  
   1.335