moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
authorhaftmann
Wed Aug 11 12:24:24 2010 +0200 (2010-08-11)
changeset 3834172dba5bd5f63
parent 38340 7813e44db886
child 38342 09d4a04d5c2e
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
src/Pure/Isar/generic_target.ML
src/Pure/Isar/theory_target.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Wed Aug 11 12:04:49 2010 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Aug 11 12:24:24 2010 +0200
     1.3 @@ -21,11 +21,21 @@
     1.4      -> term list -> local_theory -> local_theory)
     1.5      -> string * bool -> (binding * mixfix) * term -> local_theory
     1.6      -> (term * term) * local_theory
     1.7 +
     1.8 +  val theory_declaration: declaration -> local_theory -> local_theory
     1.9 +  val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
    1.10 +    -> term list * term list -> local_theory -> (term * thm) * local_theory
    1.11 +  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
    1.12 +    -> local_theory -> local_theory
    1.13 +  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
    1.14 +    -> local_theory -> local_theory
    1.15  end;
    1.16  
    1.17  structure Generic_Target: GENERIC_TARGET =
    1.18  struct
    1.19  
    1.20 +(** lifting primitive to target operations **)
    1.21 +
    1.22  (* mixfix syntax *)
    1.23  
    1.24  fun check_mixfix ctxt (b, extra_tfrees) mx =
    1.25 @@ -176,4 +186,40 @@
    1.26      |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
    1.27    end;
    1.28  
    1.29 +
    1.30 +(** primitive theory operations **)
    1.31 +
    1.32 +fun theory_declaration decl lthy =
    1.33 +  let
    1.34 +    val global_decl = Morphism.form
    1.35 +      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
    1.36 +  in
    1.37 +    lthy
    1.38 +    |> Local_Theory.theory (Context.theory_map global_decl)
    1.39 +    |> Local_Theory.target (Context.proof_map global_decl)
    1.40 +  end;
    1.41 +
    1.42 +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    1.43 +  let
    1.44 +    val (const, lthy2) = lthy |> Local_Theory.theory_result
    1.45 +      (Sign.declare_const ((b, U), mx));
    1.46 +    val lhs = list_comb (const, type_params @ term_params);
    1.47 +    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
    1.48 +      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
    1.49 +  in ((lhs, def), lthy3) end;
    1.50 +
    1.51 +fun theory_notes kind global_facts lthy =
    1.52 +  let
    1.53 +    val thy = ProofContext.theory_of lthy;
    1.54 +    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
    1.55 +  in
    1.56 +    lthy
    1.57 +    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
    1.58 +    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
    1.59 +  end;
    1.60 +
    1.61 +fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
    1.62 +  (Sign.add_abbrev (#1 prmode) (b, t) #->
    1.63 +    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
    1.64 +
    1.65  end;
     2.1 --- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:04:49 2010 +0200
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:24:24 2010 +0200
     2.3 @@ -39,28 +39,18 @@
     2.4  
     2.5  (* generic declarations *)
     2.6  
     2.7 -fun theory_declaration decl lthy =
     2.8 -  let
     2.9 -    val global_decl = Morphism.form
    2.10 -      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
    2.11 -  in
    2.12 -    lthy
    2.13 -    |> Local_Theory.theory (Context.theory_map global_decl)
    2.14 -    |> Local_Theory.target (Context.proof_map global_decl)
    2.15 -  end;
    2.16 -
    2.17  fun locale_declaration locale { syntax, pervasive } decl lthy =
    2.18    let
    2.19      val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
    2.20      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
    2.21    in
    2.22      lthy
    2.23 -    |> pervasive ? theory_declaration decl
    2.24 +    |> pervasive ? Generic_Target.theory_declaration decl
    2.25      |> Local_Theory.target (add locale locale_decl)
    2.26    end;
    2.27  
    2.28  fun target_declaration (Target {target, ...}) { syntax, pervasive } =
    2.29 -  if target = "" then theory_declaration
    2.30 +  if target = "" then Generic_Target.theory_declaration
    2.31    else locale_declaration target { syntax = syntax, pervasive = pervasive };
    2.32  
    2.33  
    2.34 @@ -103,23 +93,14 @@
    2.35  
    2.36  fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    2.37  
    2.38 -fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    2.39 -  let
    2.40 -    val (const, lthy2) = lthy |> Local_Theory.theory_result
    2.41 -      (Sign.declare_const ((b, U), mx));
    2.42 -    val lhs = list_comb (const, type_params @ term_params);
    2.43 -    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
    2.44 -      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
    2.45 -  in ((lhs, def), lthy3) end;
    2.46 -
    2.47  fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.48 -  theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.49 +  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.50    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
    2.51      #> pair (lhs, def))
    2.52  
    2.53  fun class_foundation (ta as Target {target, ...})
    2.54      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.55 -  theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.56 +  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.57    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    2.58      #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
    2.59      #> pair (lhs, def))
    2.60 @@ -131,7 +112,7 @@
    2.61              ##>> AxClass.define_overloaded b_def (c, rhs))
    2.62            ||> Class_Target.confirm_declaration b
    2.63      | NONE => lthy |>
    2.64 -        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    2.65 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    2.66  
    2.67  fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    2.68    case Overloading.operation lthy b
    2.69 @@ -140,7 +121,7 @@
    2.70              ##>> Overloading.define checked b_def (c, rhs))
    2.71            ||> Overloading.confirm b
    2.72      | NONE => lthy |>
    2.73 -        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    2.74 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    2.75  
    2.76  fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
    2.77    if not is_locale then (NoSyn, NoSyn, mx)
    2.78 @@ -184,16 +165,6 @@
    2.79  
    2.80  (* notes *)
    2.81  
    2.82 -fun theory_notes kind global_facts lthy =
    2.83 -  let
    2.84 -    val thy = ProofContext.theory_of lthy;
    2.85 -    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
    2.86 -  in
    2.87 -    lthy
    2.88 -    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
    2.89 -    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
    2.90 -  end;
    2.91 -
    2.92  fun locale_notes locale kind global_facts local_facts lthy = 
    2.93    let
    2.94      val global_facts' = Attrib.map_facts (K I) global_facts;
    2.95 @@ -207,15 +178,11 @@
    2.96  
    2.97  fun target_notes (ta as Target {target, is_locale, ...}) =
    2.98    if is_locale then locale_notes target
    2.99 -    else fn kind => fn global_facts => fn _ => theory_notes kind global_facts;
   2.100 +    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
   2.101  
   2.102  
   2.103  (* abbrev *)
   2.104  
   2.105 -fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
   2.106 -  (Sign.add_abbrev (#1 prmode) (b, t) #->
   2.107 -    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
   2.108 -
   2.109  fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
   2.110    (Sign.add_abbrev Print_Mode.internal (b, t)) #->
   2.111      (fn (lhs, _) => locale_const_declaration ta prmode
   2.112 @@ -228,7 +195,7 @@
   2.113        |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
   2.114        |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
   2.115      else lthy
   2.116 -      |> theory_abbrev prmode ((b, mx), global_rhs);
   2.117 +      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
   2.118  
   2.119  
   2.120  (* pretty *)
   2.121 @@ -301,12 +268,12 @@
   2.122      |> Local_Theory.init NONE ""
   2.123         {define = Generic_Target.define overloading_foundation,
   2.124          notes = Generic_Target.notes
   2.125 -          (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
   2.126 +          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   2.127          abbrev = Generic_Target.abbrev
   2.128            (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
   2.129 -            theory_abbrev prmode ((b, mx), t)),
   2.130 -        declaration = fn pervasive => theory_declaration,
   2.131 -        syntax_declaration = fn pervasive => theory_declaration,
   2.132 +            Generic_Target.theory_abbrev prmode ((b, mx), t)),
   2.133 +        declaration = K Generic_Target.theory_declaration,
   2.134 +        syntax_declaration = K Generic_Target.theory_declaration,
   2.135          pretty = single o Overloading.pretty,
   2.136          reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
   2.137          exit = Local_Theory.target_of o Overloading.conclude}
   2.138 @@ -325,11 +292,11 @@
   2.139    |> Local_Theory.init NONE ""
   2.140       {define = Generic_Target.define instantiation_foundation,
   2.141        notes = Generic_Target.notes
   2.142 -        (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
   2.143 +        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   2.144        abbrev = Generic_Target.abbrev
   2.145 -        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)),
   2.146 -      declaration = fn pervasive => theory_declaration,
   2.147 -      syntax_declaration = fn pervasive => theory_declaration,
   2.148 +        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
   2.149 +      declaration = K Generic_Target.theory_declaration,
   2.150 +      syntax_declaration = K Generic_Target.theory_declaration,
   2.151        pretty = single o Class_Target.pretty_instantiation,
   2.152        reinit = instantiation arities o ProofContext.theory_of,
   2.153        exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
     3.1 --- a/src/Pure/ROOT.ML	Wed Aug 11 12:04:49 2010 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Wed Aug 11 12:24:24 2010 +0200
     3.3 @@ -204,9 +204,9 @@
     3.4  
     3.5  (*local theories and targets*)
     3.6  use "Isar/local_theory.ML";
     3.7 +use "Isar/locale.ML";
     3.8  use "Isar/generic_target.ML";
     3.9  use "Isar/overloading.ML";
    3.10 -use "Isar/locale.ML";
    3.11  use "axclass.ML";
    3.12  use "Isar/class_target.ML";
    3.13  use "Isar/theory_target.ML";