src/Pure/Isar/rule_insts.ML
changeset 25333 0c509c33cfb7
parent 25329 63e8de11c8e9
child 25354 69560579abf1
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Nov 07 22:20:11 2007 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed Nov 07 22:20:12 2007 +0100
     1.3 @@ -57,13 +57,13 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun read_termTs ctxt ss Ts =
     1.8 +fun read_termTs ctxt schematic ss Ts =
     1.9    let
    1.10      fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
    1.11      val ts = map2 parse Ts ss;
    1.12      val ts' =
    1.13        map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
    1.14 -      |> Syntax.check_terms (ProofContext.set_mode ProofContext.mode_schematic ctxt)  (* FIXME !? *)
    1.15 +      |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
    1.16        |> Variable.polymorphic ctxt;
    1.17      val Ts' = map Term.fastype_of ts';
    1.18      val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
    1.19 @@ -91,7 +91,7 @@
    1.20          val S = the_sort tvars xi;
    1.21          val T =
    1.22            (case arg of
    1.23 -            Args.Text s => ProofContext.read_typ ctxt s
    1.24 +            Args.Text s => Syntax.read_typ ctxt s
    1.25            | Args.Typ T => T
    1.26            | _ => error_var "Type argument expected for " xi);
    1.27        in
    1.28 @@ -117,7 +117,7 @@
    1.29  
    1.30      val (xs, strs) = split_list external_insts;
    1.31      val Ts = map (the_type vars2) xs;
    1.32 -    val (ts, inferred) = read_termTs ctxt strs Ts;
    1.33 +    val (ts, inferred) = read_termTs ctxt true (* FIXME false *) strs Ts;
    1.34  
    1.35      val instT3 = Term.typ_subst_TVars inferred;
    1.36      val vars3 = map (apsnd instT3) vars2;
    1.37 @@ -236,47 +236,42 @@
    1.38            "'"::cs => true | cs => false);
    1.39      val Tinsts = List.filter has_type_var insts;
    1.40      val tinsts = filter_out has_type_var insts;
    1.41 +
    1.42      (* Tactic *)
    1.43      fun tac i st =
    1.44        let
    1.45 -        (* Preprocess state: extract environment information:
    1.46 -           - variables and their types
    1.47 -           - type variables and their sorts
    1.48 -           - parameters and their types *)
    1.49 -        val (types, sorts) = types_sorts st;
    1.50 -    (* Process type insts: Tinsts_env *)
    1.51 -    fun absent xi = error
    1.52 -          ("No such variable in theorem: " ^ Term.string_of_vname xi);
    1.53 -    val (rtypes, rsorts) = types_sorts thm;
    1.54 -    fun readT (xi, s) =
    1.55 -        let val S = case rsorts xi of SOME S => S | NONE => absent xi;
    1.56 -            val T = Sign.read_def_typ (thy, sorts) s;
    1.57 -            val U = TVar (xi, S);
    1.58 -        in if Sign.typ_instance thy (T, U) then (U, T)
    1.59 -           else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
    1.60 -        end;
    1.61 -    val Tinsts_env = map readT Tinsts;
    1.62 -    (* Preprocess rule: extract vars and their types, apply Tinsts *)
    1.63 -    fun get_typ xi =
    1.64 -      (case rtypes xi of
    1.65 -           SOME T => typ_subst_atomic Tinsts_env T
    1.66 -         | NONE => absent xi);
    1.67 -    val (xis, ss) = Library.split_list tinsts;
    1.68 -    val Ts = map get_typ xis;
    1.69 -        val (_, _, Bi, _) = dest_state(st,i)
    1.70 -        val params = Logic.strip_params Bi
    1.71 -                             (* params of subgoal i as string typ pairs *)
    1.72 -        val params = rev(Term.rename_wrt_term Bi params)
    1.73 -                           (* as they are printed: bound variables with *)
    1.74 -                           (* the same name are renamed during printing *)
    1.75 -        fun types' (a, ~1) = (case AList.lookup (op =) params a of
    1.76 -                NONE => types (a, ~1)
    1.77 -              | some => some)
    1.78 -          | types' xi = types xi;
    1.79 -        fun internal x = is_some (types' (x, ~1));
    1.80 -        val used = Drule.add_used thm (Drule.add_used st []);
    1.81 -        val (ts, envT) =
    1.82 -          ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
    1.83 +        val (_, _, Bi, _) = Thm.dest_state (st, i);
    1.84 +        val params = Logic.strip_params Bi;  (*params of subgoal i as string typ pairs*)
    1.85 +        val params = rev (Term.rename_wrt_term Bi params)
    1.86 +          (*as they are printed: bound variables with*)
    1.87 +          (*the same name are renamed during printing*)
    1.88 +
    1.89 +        val (param_names, ctxt') = ctxt
    1.90 +          |> Variable.declare_thm thm
    1.91 +          |> Thm.fold_terms Variable.declare_constraints st
    1.92 +          |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params);
    1.93 +
    1.94 +        (* Process type insts: Tinsts_env *)
    1.95 +        fun absent xi = error
    1.96 +              ("No such variable in theorem: " ^ Term.string_of_vname xi);
    1.97 +        val (rtypes, rsorts) = Drule.types_sorts thm;
    1.98 +        fun readT (xi, s) =
    1.99 +            let val S = case rsorts xi of SOME S => S | NONE => absent xi;
   1.100 +                val T = Syntax.read_typ ctxt' s;
   1.101 +                val U = TVar (xi, S);
   1.102 +            in if Sign.typ_instance thy (T, U) then (U, T)
   1.103 +               else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
   1.104 +            end;
   1.105 +        val Tinsts_env = map readT Tinsts;
   1.106 +        (* Preprocess rule: extract vars and their types, apply Tinsts *)
   1.107 +        fun get_typ xi =
   1.108 +          (case rtypes xi of
   1.109 +               SOME T => typ_subst_atomic Tinsts_env T
   1.110 +             | NONE => absent xi);
   1.111 +        val (xis, ss) = Library.split_list tinsts;
   1.112 +        val Ts = map get_typ xis;
   1.113 +
   1.114 +        val (ts, envT) = read_termTs ctxt' true ss Ts;
   1.115          val envT' = map (fn (ixn, T) =>
   1.116            (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
   1.117          val cenv =
   1.118 @@ -294,7 +289,7 @@
   1.119                Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
   1.120            | liftvar t = raise TERM("Variable expected", [t]);
   1.121          fun liftterm t = list_abs_free
   1.122 -              (params, Logic.incr_indexes(paramTs,inc) t)
   1.123 +              (param_names ~~ paramTs, Logic.incr_indexes(paramTs,inc) t)
   1.124          fun liftpair (cv,ct) =
   1.125                (cterm_fun liftvar cv, cterm_fun liftterm ct)
   1.126          val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);