src/Pure/Isar/proof_context.ML
changeset 14174 f3cafd2929d5
parent 13629 a46362d2b19b
child 14257 a7ef3f7588c5
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Aug 29 13:18:45 2003 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Aug 29 15:19:02 2003 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    val get_skolem: context -> string -> string
     1.5    val extern_skolem: context -> term -> term
     1.6    val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
     1.7 +  val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
     1.8    val read_term: context -> string -> term
     1.9    val read_prop: context -> string -> term
    1.10    val read_prop_schematic: context -> string -> term
    1.11 @@ -440,12 +441,15 @@
    1.12      raise CONTEXT ("Illegal reference to internal variable: " ^ quote x, ctxt)
    1.13    else x;
    1.14  
    1.15 -fun intern_skolem ctxt =
    1.16 +fun intern_skolem ctxt env =
    1.17 +(* env contains names that are not to be internalised *)
    1.18    let
    1.19      fun intern (t as Free (x, T)) =
    1.20 -          (case lookup_skolem ctxt (no_skolem false ctxt x) of
    1.21 -            Some x' => Free (x', T)
    1.22 -          | None => t)
    1.23 +          (case env (x, ~1) of
    1.24 +              Some _ => t
    1.25 +            | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
    1.26 +		  Some x' => Free (x', T)
    1.27 +		| None => t))
    1.28        | intern (t $ u) = intern t $ intern u
    1.29        | intern (Abs (x, T, t)) = Abs (x, T, intern t)
    1.30        | intern a = a;
    1.31 @@ -513,7 +517,7 @@
    1.32    let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
    1.33    in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
    1.34  
    1.35 -fun norm_term (ctxt as Context {binds, ...}) schematic =
    1.36 +fun norm_term (ctxt as Context {binds, ...}) schematic allow_vars =
    1.37    let
    1.38      (*raised when norm has no effect on a term, to do sharing instead of copying*)
    1.39      exception SAME;
    1.40 @@ -523,11 +527,12 @@
    1.41              Some (Some (u, U)) =>
    1.42                let
    1.43                  val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
    1.44 -                  raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u]);
    1.45 +                  raise TYPE ("norm_term: ill-typed variable assignment", [T, U], [t, u]);
    1.46                  val u' = Term.subst_TVars_Vartab env u;
    1.47                in norm u' handle SAME => u' end
    1.48            | _ =>
    1.49              if schematic then raise SAME
    1.50 +            else if allow_vars then t
    1.51              else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
    1.52        | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
    1.53        | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
    1.54 @@ -552,29 +557,59 @@
    1.55  
    1.56  local
    1.57  
    1.58 -fun gen_read read app is_pat dummies schematic (ctxt as Context {defs = (_, _, used, _), ...}) s =
    1.59 -  (transform_error (read (syn_of ctxt)
    1.60 -      (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s
    1.61 -    handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
    1.62 -    | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
    1.63 -  |> app (intern_skolem ctxt)
    1.64 -  |> app (if is_pat then I else norm_term ctxt schematic)
    1.65 -  |> app (if is_pat then prepare_dummies else if dummies then I else reject_dummies ctxt);
    1.66 -
    1.67 +fun gen_read read app env_opt allow_vars is_pat dummies schematic
    1.68 +    (ctxt as Context {defs = (_, _, used, _), ...}) s =
    1.69 +  let
    1.70 +    (* Use environment of ctxt with the following modification:
    1.71 +       bindings in env_opt take precedence (needed for rule_tac) *)
    1.72 +    val types = def_type ctxt is_pat;
    1.73 +    val types' = case env_opt of
    1.74 +                     None => types
    1.75 +                   | Some (env, _, _) =>
    1.76 +                       (fn ixn => case env ixn of
    1.77 +                                      None => types ixn
    1.78 +                                    | some => some);
    1.79 +    val sorts = def_sort ctxt;
    1.80 +    val sorts' = case env_opt of
    1.81 +                     None => sorts
    1.82 +                   | Some (_, envT, _) =>
    1.83 +                       (fn ixn => case envT ixn of
    1.84 +                                      None => sorts ixn
    1.85 +                                    | some => some);
    1.86 +    val used' = case env_opt of
    1.87 +                    None => used
    1.88 +                  | Some (_, _, used'') => used @ used'';
    1.89 +  in
    1.90 +    (transform_error (read (syn_of ctxt)
    1.91 +	(sign_of ctxt) (types', sorts', used')) s
    1.92 +      handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
    1.93 +      | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
    1.94 +    |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
    1.95 +    |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
    1.96 +    |> app (if is_pat then prepare_dummies
    1.97 +	 else if dummies then I else reject_dummies ctxt)
    1.98 +  end
    1.99  in
   1.100  
   1.101 -val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false false;
   1.102 -val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false false;
   1.103 +val read_termTs =
   1.104 +  gen_read (read_def_termTs false) (apfst o map) None false false false false;
   1.105 +(* For rule_tac:
   1.106 +   takes extra environment (types, sorts and used type vars) *)
   1.107 +fun read_termTs_env env =
   1.108 +  gen_read (read_def_termTs false) (apfst o map) (Some env) true false false false;
   1.109 +val read_termT_pats =
   1.110 +  #1 oo gen_read (read_def_termTs false) (apfst o map) None false true false false;
   1.111  
   1.112  fun read_term_pats T ctxt pats = read_termT_pats ctxt (map (rpair T) pats);
   1.113  val read_prop_pats = read_term_pats propT;
   1.114  
   1.115 -val read_term = gen_read (read_term_sg true) I false false false;
   1.116 -val read_term_dummies = gen_read (read_term_sg true) I false true false;
   1.117 -val read_prop = gen_read (read_prop_sg true) I false false false;
   1.118 -val read_prop_schematic = gen_read (read_prop_sg true) I false false true;
   1.119 -val read_terms = gen_read (read_terms_sg true) map false false false;
   1.120 -val read_props = gen_read (read_props_sg true) map false false;
   1.121 +val read_term = gen_read (read_term_sg true) I None false false false false;
   1.122 +val read_term_dummies = gen_read (read_term_sg true) I None false false true false;
   1.123 +val read_prop = gen_read (read_prop_sg true) I None false false false false;
   1.124 +val read_prop_schematic =
   1.125 +  gen_read (read_prop_sg true) I None false false false true;
   1.126 +val read_terms = gen_read (read_terms_sg true) map None false false false false;
   1.127 +val read_props = gen_read (read_props_sg true) map None false false false;
   1.128  
   1.129  end;
   1.130  
   1.131 @@ -584,7 +619,7 @@
   1.132  local
   1.133  
   1.134  fun gen_cert cert is_pat schematic ctxt t = t
   1.135 -  |> (if is_pat then I else norm_term ctxt schematic)
   1.136 +  |> (if is_pat then I else norm_term ctxt schematic false)
   1.137    |> (fn t' => cert (sign_of ctxt) t' handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
   1.138  
   1.139  in