first working version of instance target
authorhaftmann
Fri Nov 30 20:13:08 2007 +0100 (2007-11-30)
changeset 255144b508bb31a6c
parent 25513 b7de6e23e143
child 25515 32a5f675a85d
first working version of instance target
src/Pure/Isar/class.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Nov 30 20:13:07 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Nov 30 20:13:08 2007 +0100
     1.3 @@ -210,7 +210,7 @@
     1.4    let
     1.5      val _ = if mx <> NoSyn then
     1.6        error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
     1.7 -      else ()
     1.8 +      else ();
     1.9      val SOME class = AxClass.class_of_param thy c;
    1.10      val SOME tyco = inst_tyco thy (c, ty);
    1.11      val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
    1.12 @@ -841,32 +841,32 @@
    1.13  
    1.14  fun mk_instantiation (arities, params) =
    1.15    Instantiation { arities = arities, params = params };
    1.16 -fun get_instantiation ctxt = case Instantiation.get ctxt
    1.17 +fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
    1.18   of Instantiation data => data;
    1.19 -fun map_instantiation f (Instantiation { arities, params }) =
    1.20 -  mk_instantiation (f (arities, params));
    1.21 +fun map_instantiation f = (LocalTheory.target o Instantiation.map)
    1.22 +  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
    1.23  
    1.24 -fun the_instantiation ctxt = case get_instantiation ctxt
    1.25 +fun the_instantiation lthy = case get_instantiation lthy
    1.26   of { arities = [], ... } => error "No instantiation target"
    1.27    | data => data;
    1.28  
    1.29  val instantiation_params = #params o get_instantiation;
    1.30  
    1.31 -fun instantiation_param ctxt v = instantiation_params ctxt
    1.32 +fun instantiation_param lthy v = instantiation_params lthy
    1.33    |> find_first (fn (_, (v', _)) => v = v')
    1.34    |> Option.map (fst o fst);
    1.35  
    1.36 -fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
    1.37 +fun confirm_declaration c = (map_instantiation o apsnd)
    1.38    (filter_out (fn (_, (c', _)) => c' = c));
    1.39  
    1.40  
    1.41  (* syntax *)
    1.42  
    1.43 -fun inst_term_check ts ctxt =
    1.44 +fun inst_term_check ts lthy =
    1.45    let
    1.46 -    val params = instantiation_params ctxt;
    1.47 -    val tsig = ProofContext.tsig_of ctxt;
    1.48 -    val thy = ProofContext.theory_of ctxt;
    1.49 +    val params = instantiation_params lthy;
    1.50 +    val tsig = ProofContext.tsig_of lthy;
    1.51 +    val thy = ProofContext.theory_of lthy;
    1.52  
    1.53      fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
    1.54           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.55 @@ -882,17 +882,17 @@
    1.56                | NONE => t)
    1.57            | NONE => t)
    1.58        | t => t) ts';
    1.59 -  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
    1.60 +  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
    1.61  
    1.62 -fun inst_term_uncheck ts ctxt =
    1.63 +fun inst_term_uncheck ts lthy =
    1.64    let
    1.65 -    val params = instantiation_params ctxt;
    1.66 +    val params = instantiation_params lthy;
    1.67      val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
    1.68         (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
    1.69           of SOME c => Const (c, ty)
    1.70            | NONE => t)
    1.71        | t => t) ts;
    1.72 -  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
    1.73 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
    1.74  
    1.75  
    1.76  (* target *)
    1.77 @@ -946,8 +946,7 @@
    1.78  
    1.79  fun gen_instantiation_instance do_proof after_qed lthy =
    1.80    let
    1.81 -    val ctxt = LocalTheory.target_of lthy;
    1.82 -    val arities = (#arities o the_instantiation) ctxt;
    1.83 +    val arities = (#arities o the_instantiation) lthy;
    1.84      val arities_proof = maps Logic.mk_arities arities;
    1.85      fun after_qed' results =
    1.86        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
     2.1 --- a/src/Pure/Isar/instance.ML	Fri Nov 30 20:13:07 2007 +0100
     2.2 +++ b/src/Pure/Isar/instance.ML	Fri Nov 30 20:13:08 2007 +0100
     2.3 @@ -61,9 +61,9 @@
     2.4      |> `(fn ctxt => map (mk_def ctxt) defs)
     2.5      |-> (fn defs => fold_map Specification.definition defs)
     2.6      |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
     2.7 -    ||> LocalTheory.exit
     2.8 -    ||> ProofContext.theory_of
     2.9 -    ||> TheoryTarget.instantiation arities
    2.10 +    ||> LocalTheory.reinit
    2.11 +    (*||> ProofContext.theory_of
    2.12 +    ||> TheoryTarget.instantiation arities*)
    2.13      |-> (fn defs => do_proof defs)
    2.14    else
    2.15      thy
     3.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 30 20:13:07 2007 +0100
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 30 20:13:08 2007 +0100
     3.3 @@ -290,12 +290,7 @@
     3.4      val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
     3.5  
     3.6      (*axioms*)
     3.7 -    val resubst_instparams = map_aterms (fn t as Free (v, T) =>
     3.8 -      (case Class.instantiation_param lthy' v
     3.9 -       of NONE => t
    3.10 -        | SOME c => Const (c, T)) | t => t)
    3.11 -    val hyps = map Thm.term_of (Assumption.assms_of lthy')
    3.12 -      |> map resubst_instparams;
    3.13 +    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    3.14      fun axiom ((name, atts), props) thy = thy
    3.15        |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    3.16        |-> (fn ths => pair ((name, atts), [(ths, [])]));