simplified consts: no auxiliary params, sane mixfix syntax;
authorwenzelm
Sun Nov 26 18:07:31 2006 +0100 (2006-11-26)
changeset 21533bada5ac1216a
parent 21532 8c162b766cef
child 21534 68f805e9db0b
simplified consts: no auxiliary params, sane mixfix syntax;
declarations: proper morphisms;
added target_morphism/name;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sun Nov 26 18:07:29 2006 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Nov 26 18:07:31 2006 +0100
     1.3 @@ -58,29 +58,22 @@
     1.4  
     1.5  fun consts loc depends decls lthy =
     1.6    let
     1.7 -    val xs = filter depends (#1 (ProofContext.inferred_fixes lthy));
     1.8 -    val ys = filter (Variable.newly_fixed lthy (LocalTheory.target_of lthy) o #1) xs;
     1.9 +    val is_loc = loc <> "";
    1.10 +    val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.11  
    1.12      fun const ((c, T), mx) thy =
    1.13        let
    1.14          val U = map #2 xs ---> T;
    1.15 -        val mx' = if null ys then mx else NoSyn;
    1.16 -        val mx'' = Syntax.unlocalize_mixfix (loc <> "") mx';
    1.17 +        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
    1.18 +        val thy' = Sign.add_consts_authentic [(c, U, Syntax.unlocalize_mixfix is_loc mx)] thy;
    1.19 +      in (((c, mx), t), thy') end;
    1.20  
    1.21 -        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
    1.22 -        val defn = ((c, if loc <> "" then mx else NoSyn (* FIXME !? *)), (("", []), t));
    1.23 -        val abbr = ((c, mx'), fold_rev (lambda o Free) ys t);
    1.24 -        val thy' = Sign.add_consts_authentic [(c, U, mx'')] thy;
    1.25 -      in ((defn, abbr), thy') end;
    1.26 -
    1.27 -    val ((defns, abbrs), lthy') = lthy
    1.28 -      |> LocalTheory.theory_result (fold_map const decls) |>> split_list;
    1.29 +    val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls);
    1.30 +    val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
    1.31    in
    1.32      lthy'
    1.33 -    |> K (loc <> "") ? (snd o LocalTheory.abbrevs Syntax.default_mode abbrs)
    1.34 -    |> ProofContext.set_stmt true
    1.35 -    |> LocalDefs.add_defs defns |>> map (apsnd snd)
    1.36 -    ||> ProofContext.restore_stmt lthy'
    1.37 +    |> K is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs
    1.38 +    |> LocalDefs.add_defs defs |>> map (apsnd snd)
    1.39    end;
    1.40  
    1.41  
    1.42 @@ -127,30 +120,37 @@
    1.43    Drule.term_rule (ProofContext.theory_of lthy)
    1.44      (Assumption.export false lthy (LocalTheory.target_of lthy));
    1.45  
    1.46 +infix also;
    1.47 +fun eq1 also eq2 = Thm.transitive eq1 eq2;
    1.48 +
    1.49  in
    1.50  
    1.51  fun defs kind args lthy =
    1.52    let
    1.53 -    fun def ((x, mx), ((name, atts), rhs)) lthy1 =
    1.54 +    fun def ((c, mx), ((name, atts), rhs)) lthy1 =
    1.55        let
    1.56 -        val name' = Thm.def_name_optional x name;
    1.57 +        val name' = Thm.def_name_optional c name;
    1.58          val T = Term.fastype_of rhs;
    1.59 +
    1.60          val rhs' = expand_defs lthy1 rhs;
    1.61          val depends = member (op =) (Term.add_frees rhs' []);
    1.62          val defined = filter_out depends (Term.add_frees rhs []);
    1.63  
    1.64 +        val ([(lhs, local_def)], lthy2) = lthy1
    1.65 +          |> LocalTheory.consts depends [((c, T), mx)];
    1.66 +        val lhs' = #2 (Logic.dest_equals (Thm.prop_of local_def));
    1.67 +
    1.68          val rhs_conv = rhs
    1.69            |> Thm.cterm_of (ProofContext.theory_of lthy1)
    1.70            |> Tactic.rewrite true (map_filter (LocalDefs.find_def lthy1 o #1) defined);
    1.71  
    1.72 -        val ([(lhs, local_def)], lthy2) = lthy1
    1.73 -          |> LocalTheory.consts depends [((x, T), mx)];
    1.74 -        val lhs' = #2 (Logic.dest_equals (Thm.prop_of local_def));
    1.75 -
    1.76          val (global_def, lthy3) = lthy2
    1.77            |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
    1.78  
    1.79 -        val eq = Thm.transitive (Thm.transitive local_def global_def) (Thm.symmetric rhs_conv);
    1.80 +        val eq =
    1.81 +          local_def                      (*c == loc.c xs*)
    1.82 +          also global_def                (*... == rhs'*)
    1.83 +          also Thm.symmetric rhs_conv;   (*... == rhs*)
    1.84        in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
    1.85  
    1.86      val ((lhss, facts), lthy') = lthy |> fold_map def args |>> split_list;
    1.87 @@ -196,22 +196,31 @@
    1.88        locale_notes loc kind facts #> context_notes kind facts;
    1.89  
    1.90  
    1.91 -(* declarations *)
    1.92 +(* target declarations *)
    1.93  
    1.94 -(* FIXME proper morphisms *)
    1.95 -fun decl _ "" f = LocalTheory.theory (Context.theory_map (f Morphism.identity))
    1.96 -  | decl add loc f = LocalTheory.target (add loc (Context.proof_map o f));
    1.97 +fun decl _ "" f =
    1.98 +      LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
    1.99 +      LocalTheory.target (Context.proof_map (f Morphism.identity))
   1.100 +  | decl add loc f =
   1.101 +      LocalTheory.target (add loc (Context.proof_map o f));
   1.102  
   1.103  val type_syntax = decl Locale.add_type_syntax;
   1.104  val term_syntax = decl Locale.add_term_syntax;
   1.105  val declaration = decl Locale.add_declaration;
   1.106  
   1.107 +fun target_morphism loc lthy =
   1.108 +  ProofContext.export_standard_morphism lthy (LocalTheory.target_of lthy) $>
   1.109 +  Morphism.name_morphism (NameSpace.qualified loc);
   1.110 +
   1.111 +fun target_name "" lthy = Sign.full_name (ProofContext.theory_of lthy)
   1.112 +  | target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy);
   1.113 +
   1.114  
   1.115  (* init and exit *)
   1.116  
   1.117  fun begin loc =
   1.118    Data.put (if loc = "" then NONE else SOME loc) #>
   1.119 -  LocalTheory.init (SOME (NameSpace.base loc))
   1.120 +  LocalTheory.init (NameSpace.base loc)
   1.121     {pretty = pretty loc,
   1.122      consts = consts loc,
   1.123      axioms = axioms,
   1.124 @@ -220,8 +229,10 @@
   1.125      type_syntax = type_syntax loc,
   1.126      term_syntax = term_syntax loc,
   1.127      declaration = declaration loc,
   1.128 +    target_morphism = target_morphism loc,
   1.129 +    target_name = target_name loc,
   1.130      reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc),
   1.131 -    exit = LocalTheory.target_of}
   1.132 +    exit = LocalTheory.target_of};
   1.133  
   1.134  fun init_i NONE thy = begin "" (ProofContext.init thy)
   1.135    | init_i (SOME loc) thy = begin loc (Locale.init loc thy);