src/Pure/variable.ML
changeset 19911 300bc6ce970d
parent 19899 b7385ca02d79
child 19926 feb4d150cfd8
     1.1 --- a/src/Pure/variable.ML	Sat Jun 17 19:37:51 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Sat Jun 17 19:37:52 2006 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val fixed_names_of: Context.proof -> string list
     1.5    val binds_of: Context.proof -> (typ * term) Vartab.table
     1.6    val defaults_of: Context.proof ->
     1.7 -    typ Vartab.table * sort Vartab.table * string list * term list Symtab.table
     1.8 +    typ Vartab.table * sort Vartab.table * string list * string list Symtab.table
     1.9    val used_types: Context.proof -> string list
    1.10    val is_declared: Context.proof -> string -> bool
    1.11    val is_fixed: Context.proof -> string -> bool
    1.12 @@ -24,23 +24,29 @@
    1.13    val declare_type: typ -> Context.proof -> Context.proof
    1.14    val declare_syntax: term -> Context.proof -> Context.proof
    1.15    val declare_term: term -> Context.proof -> Context.proof
    1.16 +  val rename_wrt: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
    1.17 +  val add_fixes: string list -> Context.proof -> string list * Context.proof
    1.18 +  val invent_fixes: string list -> Context.proof -> string list * Context.proof
    1.19    val invent_types: sort list -> Context.proof -> (string * sort) list * Context.proof
    1.20 -  val rename_wrt: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
    1.21 +  val export_inst: Context.proof -> Context.proof -> string list * string list
    1.22 +  val exportT_inst: Context.proof -> Context.proof -> string list
    1.23 +  val export_terms: Context.proof -> Context.proof -> term list -> term list
    1.24 +  val exportT_terms: Context.proof -> Context.proof -> term list -> term list
    1.25 +  val exportT: Context.proof -> Context.proof -> thm list -> thm list
    1.26 +  val export: Context.proof -> Context.proof -> thm list -> thm list
    1.27 +  val importT_inst: term list -> Context.proof -> ((indexname * sort) * typ) list * Context.proof
    1.28 +  val import_inst: bool -> term list -> Context.proof ->
    1.29 +    (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Context.proof
    1.30 +  val importT_terms: term list -> Context.proof -> term list * Context.proof
    1.31 +  val import_terms: bool -> term list -> Context.proof -> term list * Context.proof
    1.32 +  val importT: thm list -> Context.proof -> thm list * Context.proof
    1.33 +  val import: bool -> thm list -> Context.proof -> thm list * Context.proof
    1.34    val warn_extra_tfrees: Context.proof -> Context.proof -> unit
    1.35 -  val generalize_tfrees: Context.proof -> Context.proof -> string list -> string list
    1.36 -  val generalize: Context.proof -> Context.proof -> term list -> term list
    1.37 +  val monomorphic: Context.proof -> term list -> term list
    1.38    val polymorphic: Context.proof -> term list -> term list
    1.39    val hidden_polymorphism: term -> typ -> (indexname * sort) list
    1.40 -  val monomorphic_inst: term list -> Context.proof ->
    1.41 -    ((indexname * sort) * typ) list * Context.proof
    1.42 -  val monomorphic: Context.proof -> term list -> term list
    1.43    val add_binds: (indexname * term option) list -> Context.proof -> Context.proof
    1.44    val expand_binds: Context.proof -> term -> term
    1.45 -  val add_fixes: string list -> Context.proof -> string list * Context.proof
    1.46 -  val invent_fixes: string list -> Context.proof -> string list * Context.proof
    1.47 -  val import_types: bool -> typ list -> Context.proof -> typ list * Context.proof
    1.48 -  val import_terms: bool -> term list -> Context.proof -> term list * Context.proof
    1.49 -  val import: bool -> thm list -> Context.proof -> thm list * Context.proof
    1.50  end;
    1.51  
    1.52  structure Variable: VARIABLE =
    1.53 @@ -49,14 +55,14 @@
    1.54  (** local context data **)
    1.55  
    1.56  datatype data = Data of
    1.57 - {is_body: bool,                          (*internal body mode*)
    1.58 -  fixes: (string * string) list,          (*term fixes*)
    1.59 + {is_body: bool,                          (*inner body mode*)
    1.60 +  fixes: (string * string) list,          (*term fixes -- extern/intern*)
    1.61    binds: (typ * term) Vartab.table,       (*term bindings*)
    1.62    defaults:
    1.63      typ Vartab.table *                    (*type constraints*)
    1.64      sort Vartab.table *                   (*default sorts*)
    1.65      string list *                         (*used type variables*)
    1.66 -    term list Symtab.table};              (*type variable occurrences*)
    1.67 +    string list Symtab.table};            (*occurrences of type variables in term variables*)
    1.68  
    1.69  fun make_data (is_body, fixes, binds, defaults) =
    1.70    Data {is_body = is_body, fixes = fixes, binds = binds, defaults = defaults};
    1.71 @@ -141,7 +147,8 @@
    1.72    (fn TFree (x, _) => insert (op =) x | _ => I);
    1.73  
    1.74  val ins_occs = fold_term_types (fn t =>
    1.75 -  fold_atyps (fn TFree (x, _) => Symtab.update_list (x, t) | _ => I));
    1.76 +  let val x = case t of Free (x, _) => x | _ => ""
    1.77 +  in fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I) end);
    1.78  
    1.79  fun ins_skolem def_ty = fold_rev (fn (x, x') =>
    1.80    (case def_ty x' of
    1.81 @@ -162,6 +169,9 @@
    1.82    fold_types ins_used t used,
    1.83    occ));
    1.84  
    1.85 +fun declare_occs t = map_defaults (fn (types, sorts, used, occ) =>
    1.86 +  (types, sorts, used, ins_occs t occ));
    1.87 +
    1.88  fun declare_term t ctxt =
    1.89    ctxt
    1.90    |> declare_syntax t
    1.91 @@ -174,15 +184,6 @@
    1.92  end;
    1.93  
    1.94  
    1.95 -(* invent types *)
    1.96 -
    1.97 -fun invent_types Ss ctxt =
    1.98 -  let
    1.99 -    val tfrees = Term.invent_names (used_types ctxt) "'a" (length Ss) ~~ Ss;
   1.100 -    val ctxt' = fold (declare_type o TFree) tfrees ctxt;
   1.101 -  in (tfrees, ctxt') end;
   1.102 -
   1.103 -
   1.104  (* renaming term/type frees *)
   1.105  
   1.106  fun rename_wrt ctxt ts frees =
   1.107 @@ -198,24 +199,142 @@
   1.108  
   1.109  
   1.110  
   1.111 -(** Hindley-Milner polymorphism **)
   1.112 +(** fixes **)
   1.113 +
   1.114 +fun no_dups [] = ()
   1.115 +  | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
   1.116 +
   1.117 +fun add_fixes xs ctxt =
   1.118 +  let
   1.119 +    val (ys, zs) = split_list (fixes_of ctxt);
   1.120 +    val _ = no_dups (duplicates (op =) xs);
   1.121 +    val _ =
   1.122 +      (case filter (can Term.dest_skolem) xs of [] => ()
   1.123 +      | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads));
   1.124 +    val xs' =
   1.125 +      if is_body ctxt then Term.variantlist (map Term.skolem xs, zs)
   1.126 +      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); xs);
   1.127 +  in
   1.128 +    ctxt
   1.129 +    |> map_fixes (fn fixes => rev (xs ~~ xs') @ fixes)
   1.130 +    |> fold (declare_syntax o Syntax.free) xs'
   1.131 +    |> pair xs'
   1.132 +  end;
   1.133 +
   1.134 +fun invent_fixes xs ctxt =
   1.135 +  ctxt
   1.136 +  |> set_body true
   1.137 +  |> add_fixes (Term.variantlist (xs, []))
   1.138 +  ||> restore_body ctxt;
   1.139 +
   1.140 +fun invent_types Ss ctxt =
   1.141 +  let
   1.142 +    val tfrees = Term.invent_names (used_types ctxt) "'a" (length Ss) ~~ Ss;
   1.143 +    val ctxt' = fold (declare_type o TFree) tfrees ctxt;
   1.144 +  in (tfrees, ctxt') end;
   1.145 +
   1.146 +
   1.147 +
   1.148 +(** export -- generalize type/term variables **)
   1.149 +
   1.150 +fun export_inst inner outer =
   1.151 +  let
   1.152 +    val types_outer = used_types outer;
   1.153 +    val fixes_inner = fixes_of inner;
   1.154 +    val fixes_outer = fixes_of outer;
   1.155 +
   1.156 +    val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
   1.157 +    val still_fixed = not o member (op =) ("" :: gen_fixes);
   1.158 +    val gen_fixesT =
   1.159 +      Symtab.fold (fn (a, xs) =>
   1.160 +        if member (op =) types_outer a orelse exists still_fixed xs
   1.161 +        then I else cons a) (type_occs_of inner) [];
   1.162 +  in (gen_fixesT, gen_fixes) end;
   1.163 +
   1.164 +fun exportT_inst inner outer = #1 (export_inst inner outer);
   1.165 +
   1.166 +fun exportT_terms inner outer ts =
   1.167 +  map (Term.generalize (exportT_inst (fold declare_occs ts inner) outer, [])
   1.168 +    (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
   1.169 +
   1.170 +fun export_terms inner outer ts =
   1.171 +  map (Term.generalize (export_inst (fold declare_occs ts inner) outer)
   1.172 +    (fold Term.maxidx_term ts ~1 + 1)) ts;
   1.173 +
   1.174 +fun gen_export inst inner outer ths =
   1.175 +  let
   1.176 +    val maxidx = fold Thm.maxidx_thm ths ~1;
   1.177 +    val inner' = fold (declare_occs o Thm.full_prop_of) ths inner;
   1.178 +  in map (Thm.generalize (inst inner' outer) (maxidx + 1)) ths end;
   1.179 +
   1.180 +val exportT = gen_export (rpair [] oo exportT_inst);
   1.181 +val export = gen_export export_inst;
   1.182 +
   1.183 +
   1.184 +
   1.185 +(** import -- fix schematic type/term variables **)
   1.186 +
   1.187 +fun importT_inst ts ctxt =
   1.188 +  let
   1.189 +    val tvars = rev (fold Term.add_tvars ts []);
   1.190 +    val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
   1.191 +  in (tvars ~~ map TFree tfrees, ctxt') end;
   1.192 +
   1.193 +fun import_inst is_open ts ctxt =
   1.194 +  let
   1.195 +    val (instT, ctxt') = importT_inst ts ctxt;
   1.196 +    val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
   1.197 +    val ren = if is_open then I else Term.internal;
   1.198 +    val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
   1.199 +    val inst = vars ~~ map Free (xs ~~ map #2 vars);
   1.200 +  in ((instT, inst), ctxt'') end;
   1.201 +
   1.202 +fun importT_terms ts ctxt =
   1.203 +  let val (instT, ctxt') = importT_inst ts ctxt
   1.204 +  in (map (Term.instantiate (instT, [])) ts, ctxt') end;
   1.205 +
   1.206 +fun import_terms is_open ts ctxt =
   1.207 +  let val (inst, ctxt') = import_inst is_open ts ctxt
   1.208 +  in (map (Term.instantiate inst) ts, ctxt') end;
   1.209 +
   1.210 +fun importT ths ctxt =
   1.211 +  let
   1.212 +    val thy = Context.theory_of_proof ctxt;
   1.213 +    val certT = Thm.ctyp_of thy;
   1.214 +    val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
   1.215 +    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
   1.216 +    val ths' = map (Thm.instantiate (instT', [])) ths;
   1.217 +  in (ths', ctxt') end;
   1.218 +
   1.219 +fun import is_open ths ctxt =
   1.220 +  let
   1.221 +    val thy = Context.theory_of_proof ctxt;
   1.222 +    val cert = Thm.cterm_of thy;
   1.223 +    val certT = Thm.ctyp_of thy;
   1.224 +    val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
   1.225 +    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
   1.226 +    val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
   1.227 +    val ths' = map (Thm.instantiate (instT', inst')) ths;
   1.228 +  in (ths', ctxt') end;
   1.229 +
   1.230 +
   1.231 +
   1.232 +(** implicit polymorphism **)
   1.233  
   1.234  (* warn_extra_tfrees *)
   1.235  
   1.236  fun warn_extra_tfrees ctxt1 ctxt2 =
   1.237    let
   1.238 -    fun occs_typ a (Type (_, Ts)) = exists (occs_typ a) Ts
   1.239 -      | occs_typ a (TFree (b, _)) = a = b
   1.240 -      | occs_typ _ (TVar _) = false;
   1.241 -    fun occs_free a (Free (x, _)) =
   1.242 +    fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b | _ => false);
   1.243 +    fun occs_free _ "" = I
   1.244 +      | occs_free a x =
   1.245            (case def_type ctxt1 false (x, ~1) of
   1.246              SOME T => if occs_typ a T then I else cons (a, x)
   1.247 -          | NONE => cons (a, x))
   1.248 -      | occs_free _ _ = I;
   1.249 +          | NONE => cons (a, x));
   1.250  
   1.251      val occs1 = type_occs_of ctxt1 and occs2 = type_occs_of ctxt2;
   1.252 -    val extras = Symtab.fold (fn (a, ts) =>
   1.253 -      if Symtab.defined occs1 a then I else fold (occs_free a) ts) occs2 [];
   1.254 +    val extras = Symtab.fold (fn (a, xs) =>
   1.255 +      if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 [];
   1.256      val tfrees = map #1 extras |> sort_distinct string_ord;
   1.257      val frees = map #2 extras |> sort_distinct string_ord;
   1.258    in
   1.259 @@ -225,29 +344,16 @@
   1.260    end;
   1.261  
   1.262  
   1.263 -(* generalize type variables *)
   1.264 +(* monomorphic vs. polymorphic terms *)
   1.265  
   1.266 -fun generalize_tfrees inner outer =
   1.267 -  let
   1.268 -    val extra_fixes = subtract (op =) (fixed_names_of outer) (fixed_names_of inner);
   1.269 -    fun still_fixed (Free (x, _)) = not (member (op =) extra_fixes x)
   1.270 -      | still_fixed _ = false;
   1.271 -    val occs_inner = type_occs_of inner;
   1.272 -    val occs_outer = type_occs_of outer;
   1.273 -    fun add a gen =
   1.274 -      if Symtab.defined occs_outer a orelse
   1.275 -        exists still_fixed (Symtab.lookup_list occs_inner a)
   1.276 -      then gen else a :: gen;
   1.277 -  in fn tfrees => fold add tfrees [] end;
   1.278 -
   1.279 -fun generalize inner outer ts =
   1.280 -  let
   1.281 -    val tfrees = generalize_tfrees inner outer (map #1 (fold Term.add_tfrees ts []));
   1.282 -    fun gen (x, S) = if member (op =) tfrees x then TVar ((x, 0), S) else TFree (x, S);
   1.283 -  in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
   1.284 +fun monomorphic ctxt ts =
   1.285 +  #1 (importT_terms ts (fold declare_term ts ctxt));
   1.286  
   1.287  fun polymorphic ctxt ts =
   1.288 -  generalize (fold declare_term ts ctxt) ctxt ts;
   1.289 +  exportT_terms (fold declare_term ts ctxt) ctxt ts;
   1.290 +
   1.291 +
   1.292 +(** term bindings **)
   1.293  
   1.294  fun hidden_polymorphism t T =
   1.295    let
   1.296 @@ -256,22 +362,6 @@
   1.297        (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   1.298    in extra_tvars end;
   1.299  
   1.300 -
   1.301 -(* monomorphic -- fixes type variables *)
   1.302 -
   1.303 -fun monomorphic_inst ts ctxt =
   1.304 -  let
   1.305 -    val tvars = rev (fold Term.add_tvars ts []);
   1.306 -    val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
   1.307 -  in (tvars ~~ map TFree tfrees, ctxt') end;
   1.308 -
   1.309 -fun monomorphic ctxt ts =
   1.310 -  map (Term.instantiate (#1 (monomorphic_inst ts (fold declare_term ts ctxt)), [])) ts;
   1.311 -
   1.312 -
   1.313 -
   1.314 -(** term abbreviations **)
   1.315 -
   1.316  fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
   1.317    | add_bind ((x, i), SOME t) =
   1.318        let
   1.319 @@ -293,65 +383,4 @@
   1.320        | expand t = t;
   1.321    in Envir.beta_norm o Term.map_aterms expand end;
   1.322  
   1.323 -
   1.324 -
   1.325 -(** fixes **)
   1.326 -
   1.327 -fun no_dups [] = ()
   1.328 -  | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
   1.329 -
   1.330 -fun add_fixes xs ctxt =
   1.331 -  let
   1.332 -    val (ys, zs) = split_list (fixes_of ctxt);
   1.333 -    val _ = no_dups (duplicates (op =) xs);
   1.334 -    val _ =
   1.335 -      (case filter (can Syntax.dest_skolem) xs of [] => ()
   1.336 -      | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads));
   1.337 -    val xs' =
   1.338 -      if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
   1.339 -      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); xs);
   1.340 -  in
   1.341 -    ctxt
   1.342 -    |> map_fixes (fn fixes => rev (xs ~~ xs') @ fixes)
   1.343 -    |> fold (declare_syntax o Syntax.free) xs'
   1.344 -    |> pair xs'
   1.345 -  end;
   1.346 -
   1.347 -fun invent_fixes xs ctxt =
   1.348 -  ctxt
   1.349 -  |> set_body true
   1.350 -  |> add_fixes (Term.variantlist (xs, []))
   1.351 -  ||> restore_body ctxt;
   1.352 -
   1.353 -
   1.354 -(* import -- fixes schematic variables *)
   1.355 -
   1.356 -fun import_inst is_open ts ctxt =
   1.357 -  let
   1.358 -    val (instT, ctxt') = monomorphic_inst ts ctxt;
   1.359 -    val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
   1.360 -    val ren = if is_open then I else Syntax.internal;
   1.361 -    val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
   1.362 -    val inst = vars ~~ map Free (xs ~~ map #2 vars);
   1.363 -  in ((instT, inst), ctxt'') end;
   1.364 -
   1.365 -fun import_terms is_open ts ctxt =
   1.366 -  let val (inst, ctxt') = import_inst is_open ts ctxt
   1.367 -  in (map (Term.instantiate inst) ts, ctxt') end;
   1.368 -
   1.369 -fun import_types is_open Ts ctxt =
   1.370 -  import_terms is_open (map Logic.mk_type Ts) ctxt
   1.371 -  |>> map Logic.dest_type;
   1.372 -
   1.373 -fun import is_open ths ctxt =
   1.374 -  let
   1.375 -    val thy = Context.theory_of_proof ctxt;
   1.376 -    val cert = Thm.cterm_of thy;
   1.377 -    val certT = Thm.ctyp_of thy;
   1.378 -    val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
   1.379 -    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
   1.380 -    val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
   1.381 -    val ths' = map (Thm.instantiate (instT', inst')) ths;
   1.382 -  in (ths', ctxt') end;
   1.383 -
   1.384  end;