Common theory targets.
authorwenzelm
Sat Oct 07 01:31:23 2006 +0200 (2006-10-07)
changeset 20894784eefc906aa
parent 20893 c99f79910ae8
child 20895 ac772d489fde
Common theory targets.
src/Pure/Isar/theory_target.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Oct 07 01:31:23 2006 +0200
     1.3 @@ -0,0 +1,213 @@
     1.4 +(*  Title:      Pure/Isar/theory_target.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Common theory targets.
     1.9 +*)
    1.10 +
    1.11 +signature THEORY_TARGET =
    1.12 +sig
    1.13 +  val init: xstring option -> theory -> local_theory
    1.14 +  val init_i: string option -> theory -> local_theory
    1.15 +  val exit: local_theory -> local_theory * theory
    1.16 +  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
    1.17 +end;
    1.18 +
    1.19 +structure TheoryTarget: THEORY_TARGET =
    1.20 +struct
    1.21 +
    1.22 +(** locale targets **)
    1.23 +
    1.24 +(* pretty *)
    1.25 +
    1.26 +fun pretty loc ctxt =
    1.27 +  let
    1.28 +    val thy = ProofContext.theory_of ctxt;
    1.29 +    val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
    1.30 +    val assumes = map (fn A => (("", []), [(A, [])])) (Assumption.assms_of ctxt);
    1.31 +    val elems =
    1.32 +      (if null fixes then [] else [Element.Fixes fixes]) @
    1.33 +      (if null assumes then [] else [Element.Assumes assumes]);
    1.34 +  in
    1.35 +    ([Pretty.block
    1.36 +      [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
    1.37 +        Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] @
    1.38 +      (if loc = "" then []
    1.39 +       else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
    1.40 +       else
    1.41 +         [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
    1.42 +           (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]))
    1.43 +    |> Pretty.chunks
    1.44 +  end;
    1.45 +
    1.46 +
    1.47 +(* consts *)
    1.48 +
    1.49 +fun consts loc depends decls lthy =
    1.50 +  let
    1.51 +    val xs = filter depends (#1 (ProofContext.inferred_fixes lthy));
    1.52 +    val ys = filter (Variable.newly_fixed lthy (LocalTheory.target_of lthy) o #1) xs;
    1.53 +
    1.54 +    fun const ((c, T), mx) thy =
    1.55 +      let
    1.56 +        val U = map #2 xs ---> T;
    1.57 +        val mx' = if null ys then mx else NoSyn;
    1.58 +        val mx'' = Syntax.unlocalize_mixfix (loc <> "") mx';
    1.59 +
    1.60 +        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
    1.61 +        val defn = ((c, if loc <> "" then mx else NoSyn (* FIXME !? *)), (("", []), t));
    1.62 +        val abbr = ((c, mx'), fold_rev (lambda o Free) ys t);
    1.63 +        val thy' = Sign.add_consts_authentic [(c, U, mx'')] thy;
    1.64 +      in ((defn, abbr), thy') end;
    1.65 +
    1.66 +    val ((defns, abbrs), lthy') = lthy
    1.67 +      |> LocalTheory.theory_result (fold_map const decls) |>> split_list;
    1.68 +  in
    1.69 +    lthy'
    1.70 +    |> K (loc <> "") ? LocalTheory.abbrevs Syntax.default_mode abbrs
    1.71 +    |> LocalDefs.add_defs defns |>> map (apsnd snd)
    1.72 +  end;
    1.73 +
    1.74 +
    1.75 +(* axioms *)
    1.76 +
    1.77 +local
    1.78 +
    1.79 +fun add_axiom hyps (name, prop) thy =
    1.80 +  let
    1.81 +    val name' = if name = "" then "axiom_" ^ serial_string () else name;
    1.82 +    val prop' = Logic.list_implies (hyps, prop);
    1.83 +    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
    1.84 +    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
    1.85 +    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
    1.86 +  in (Drule.implies_elim_list axm prems, thy') end;
    1.87 +
    1.88 +in
    1.89 +
    1.90 +fun axioms specs =
    1.91 +  fold (fold Variable.fix_frees o snd) specs #>   (* FIXME !? *)
    1.92 +  (fn lthy =>
    1.93 +    let
    1.94 +      val hyps = Assumption.assms_of lthy;
    1.95 +      fun axiom ((name, atts), props) thy = thy
    1.96 +        |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
    1.97 +        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.98 +    in
    1.99 +      lthy
   1.100 +      |> LocalTheory.theory_result (fold_map axiom specs)
   1.101 +      |-> LocalTheory.notes
   1.102 +    end);
   1.103 +
   1.104 +end;
   1.105 +
   1.106 +
   1.107 +(* defs *)
   1.108 +
   1.109 +local
   1.110 +
   1.111 +fun add_def (name, prop) =
   1.112 +  Theory.add_defs_i false false [(name, prop)] #>
   1.113 +  (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
   1.114 +
   1.115 +fun expand_defs lthy =
   1.116 +  Drule.term_rule (ProofContext.theory_of lthy)
   1.117 +    (Assumption.export false lthy (LocalTheory.target_of lthy));
   1.118 +
   1.119 +in
   1.120 +
   1.121 +fun defs args lthy =
   1.122 +  let
   1.123 +    fun def ((x, mx), ((name, atts), rhs)) lthy1 =
   1.124 +      let
   1.125 +        val name' = Thm.def_name_optional x name;
   1.126 +        val T = Term.fastype_of rhs;
   1.127 +        val rhs' = expand_defs lthy1 rhs;
   1.128 +        val depends = member (op =) (Term.add_frees rhs' []);
   1.129 +        val defined = filter_out depends (Term.add_frees rhs []);
   1.130 +
   1.131 +        val rhs_conv = rhs
   1.132 +          |> Thm.cterm_of (ProofContext.theory_of lthy1)
   1.133 +          |> Tactic.rewrite true (map_filter (LocalDefs.find_def lthy1 o #1) defined);
   1.134 +
   1.135 +        val ([(lhs, local_def)], lthy2) = lthy1
   1.136 +          |> LocalTheory.consts depends [((x, T), mx)];
   1.137 +        val lhs' = #2 (Logic.dest_equals (Thm.prop_of local_def));
   1.138 +
   1.139 +        val (global_def, lthy3) = lthy2
   1.140 +          |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
   1.141 +
   1.142 +        val eq = Thm.transitive (Thm.transitive local_def global_def) (Thm.symmetric rhs_conv);
   1.143 +      in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
   1.144 +
   1.145 +    val ((lhss, facts), lthy') = lthy |> fold_map def args |>> split_list;
   1.146 +    val (res, lthy'') = lthy' |> LocalTheory.notes facts;
   1.147 +  in (lhss ~~ map (apsnd the_single) res, lthy'') end;
   1.148 +
   1.149 +end;
   1.150 +
   1.151 +
   1.152 +(* notes *)
   1.153 +
   1.154 +fun context_notes facts lthy =
   1.155 +  let
   1.156 +    val facts' = facts
   1.157 +      |> Element.export_standard_facts lthy lthy
   1.158 +      |> Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of lthy));
   1.159 +  in
   1.160 +    lthy
   1.161 +    |> ProofContext.qualified_names
   1.162 +    |> ProofContext.note_thmss_i facts'
   1.163 +    ||> ProofContext.restore_naming lthy
   1.164 +  end;
   1.165 +
   1.166 +fun theory_notes facts lthy = lthy |> LocalTheory.theory (fn thy =>
   1.167 +  let
   1.168 +    val facts' = facts
   1.169 +      |> Element.export_standard_facts lthy (ProofContext.init thy)
   1.170 +      |> Attrib.map_facts (Attrib.attribute_i thy);
   1.171 +  in
   1.172 +    thy
   1.173 +    |> Sign.qualified_names
   1.174 +    |> PureThy.note_thmss_i "" facts' |> #2
   1.175 +    |> Sign.restore_naming thy
   1.176 +  end);
   1.177 +
   1.178 +fun locale_notes loc facts lthy = lthy |> LocalTheory.target (fn ctxt =>
   1.179 +  #2 (Locale.add_thmss "" loc (Element.export_standard_facts lthy ctxt facts) ctxt));
   1.180 +
   1.181 +fun notes "" facts = theory_notes facts #> context_notes facts
   1.182 +  | notes loc facts = locale_notes loc facts #> context_notes facts
   1.183 +
   1.184 +
   1.185 +(* declarations *)
   1.186 +
   1.187 +fun term_syntax "" f = LocalTheory.theory (Context.theory_map f)
   1.188 +  | term_syntax loc f = LocalTheory.target (Locale.add_term_syntax loc (Context.proof_map f));
   1.189 +
   1.190 +fun declaration "" f = LocalTheory.theory (Context.theory_map f)
   1.191 +  | declaration loc f = I;    (* FIXME *)
   1.192 +
   1.193 +
   1.194 +
   1.195 +(* init and exit *)
   1.196 +
   1.197 +fun target_operations loc : LocalTheory.operations =
   1.198 + {pretty = pretty loc,
   1.199 +  consts = consts loc,
   1.200 +  axioms = axioms,
   1.201 +  defs = defs,
   1.202 +  notes = notes loc,
   1.203 +  term_syntax = term_syntax loc,
   1.204 +  declaration = declaration loc};
   1.205 +
   1.206 +fun init_i NONE thy = LocalTheory.init (SOME "") (target_operations "") (ProofContext.init thy)
   1.207 +  | init_i (SOME loc) thy =
   1.208 +      LocalTheory.init (SOME (NameSpace.base loc)) (target_operations loc) (Locale.init loc thy);
   1.209 +
   1.210 +fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
   1.211 +
   1.212 +fun exit lthy = (lthy, ProofContext.theory_of lthy);
   1.213 +
   1.214 +fun mapping loc f = init loc #> f #> exit;
   1.215 +
   1.216 +end;