# HG changeset patch # User wenzelm # Date 1191952135 -7200 # Node ID 6dd60d1191bf286c158df4b80cd73a2c3532e531 # Parent a220317465b495cf55e0630f7c5944ab92ec0f78 tuned; diff -r a220317465b4 -r 6dd60d1191bf src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Tue Oct 09 19:48:54 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Tue Oct 09 19:48:55 2007 +0200 @@ -34,20 +34,20 @@ fun pretty loc ctxt = let val thy = ProofContext.theory_of ctxt; + val loc_kind = if is_some (Class.class_of_locale thy loc) then "class" else "locale"; + val loc_name = Locale.extern thy loc; + val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt)); val elems = (if null fixes then [] else [Element.Fixes fixes]) @ (if null assumes then [] else [Element.Assumes assumes]); in - if loc = "" then - [Pretty.block - [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy), - Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] - else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)] - else - [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =") - (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] + Pretty.block [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy)] :: + (if loc = "" then [] + else if null elems then [Pretty.str (loc_kind ^ " " ^ loc_name)] + else [Pretty.big_list (loc_kind ^ " " ^ loc_name ^ " =") + (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]) end; @@ -77,211 +77,6 @@ |> NameSpace.qualified_names; -(* consts *) - -fun target_abbrev prmode ((c, mx), rhs) phi = - let - val c' = Morphism.name phi c; - val rhs' = Morphism.term phi rhs; - val arg' = (c', rhs'); - val eq_heads = - (case pairself Term.head_of (rhs, rhs') of - (Const (a, _), Const (a', _)) => a = a' - | _ => false); - in - eq_heads ? (Context.mapping_result - (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg') - #-> (fn (lhs, _) => - Term.equiv_types (rhs, rhs') ? - Morphism.form (ProofContext.target_notation prmode [(lhs, mx)]))) - end; - -fun internal_abbrev prmode ((c, mx), t) lthy = lthy - (* FIXME really permissive *) - |> LocalTheory.term_syntax (perhaps o try o target_abbrev prmode ((c, mx), t)) - |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t) - |> snd; - -fun consts is_loc some_class depends decls lthy = - let - val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); - - fun const ((c, T), mx) thy = - let - val U = map #2 xs ---> T; - val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); - val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; - val mx3 = if is_loc then NoSyn else mx1; - val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy; - in (((c, mx2), t), thy') end; - fun const_class (SOME class) ((c, _), mx) (_, t) = - LocalTheory.raw_theory_result - (Class.add_const_in_class class ((c, t), mx)) - #-> (fn c => Class.remove_constraint [class] c) - | const_class NONE _ _ = I; - fun hide_abbrev (SOME class) abbrs thy = - let - val raw_cs = map (fst o fst) abbrs; - val prfx = (Logic.const_of_class o NameSpace.base) class; - fun mk_name c = - let - val n1 = Sign.full_name thy c; - val n2 = NameSpace.qualifier n1; - val n3 = NameSpace.base n1; - in NameSpace.implode [n2, prfx, prfx, n3] end; - val cs = map mk_name raw_cs; - in - Sign.hide_consts_i true cs thy - end - | hide_abbrev NONE _ thy = thy; - - val (abbrs, lthy') = lthy - |> LocalTheory.theory_result (fold_map const decls) - val defs = map (apsnd (pair ("", []))) abbrs; - - in - lthy' - |> fold2 (const_class some_class) decls abbrs - |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs - |> LocalTheory.raw_theory (hide_abbrev some_class abbrs) - (*FIXME abbreviations should never occur*) - |> LocalDefs.add_defs defs - |>> map (apsnd snd) - end; - - -(* abbrev *) - -fun occ_params ctxt ts = - #1 (ProofContext.inferred_fixes ctxt) - |> filter (member (op =) (fold (Variable.add_fixed ctxt) ts [])); - -fun local_abbrev (x, rhs) = - Variable.add_fixes [x] #-> (fn [x'] => - let - val T = Term.fastype_of rhs; - val lhs = Free (x', T); - in - Variable.declare_term lhs #> - Variable.declare_term rhs #> - Assumption.add_assms (K (K (I, Envir.expand_term_frees [((x', T), rhs)]))) [] #> snd #> - pair (lhs, rhs) - end); - -fun abbrev is_loc some_class prmode ((raw_c, mx), raw_t) lthy = - let - val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy); - val target = LocalTheory.target_of lthy; - val target_morphism = LocalTheory.target_morphism lthy; - - val c = Morphism.name target_morphism raw_c; - val t = Morphism.term target_morphism raw_t; - val xs = map Free (occ_params target [t]); - val u = fold_rev Term.lambda xs t; - val U = Term.fastype_of u; - val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u; - val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; - val mx3 = if is_loc then NoSyn else mx1; - fun add_abbrev_in_class (SOME class) abbr = - LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr) - #-> (fn c => Class.remove_constraint [class] c) - | add_abbrev_in_class NONE _ = I; - in - lthy - |> LocalTheory.theory_result - (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u')) - |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)]) - #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) - #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) - #> local_abbrev (c, rhs)) - end; - - -(* defs *) - -local - -fun expand_term ctxt t = - let - val thy = ProofContext.theory_of ctxt; - val thy_ctxt = ProofContext.init thy; - val ct = Thm.cterm_of thy t; - val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term; - in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end; - -fun add_def (name, prop) thy = - let - val tfrees = rev (map TFree (Term.add_tfrees prop [])); - val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); - val strip_sorts = tfrees ~~ tfrees'; - val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees); - - val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; - val thy' = Theory.add_defs_i false false [(name, prop')] thy; - val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name); - val def = Thm.instantiate (recover_sorts, []) axm'; - in (Drule.unvarify def, thy') end; - -in - -fun local_def kind ((c, mx), ((name, atts), rhs)) lthy1 = - let - val (rhs', rhs_conv) = expand_term lthy1 rhs; - val xs = Variable.add_fixed (LocalTheory.target_of lthy1) rhs' []; - val T = Term.fastype_of rhs; - - (*consts*) - val ([(lhs, lhs_def)], lthy2) = lthy1 - |> LocalTheory.consts (member (op =) xs) [((c, T), mx)]; - val (_, lhs') = Logic.dest_equals (Thm.prop_of lhs_def); - - (*def*) - val name' = Thm.def_name_optional c name; - val (def, lthy3) = lthy2 - |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs'))); - val eq = LocalDefs.trans_terms lthy3 - [(*c == loc.c xs*) lhs_def, - (*lhs' == rhs'*) def, - (*rhs' == rhs*) Thm.symmetric rhs_conv]; - - (*notes*) - val ([(res_name, [res])], lthy4) = lthy3 - |> LocalTheory.notes kind [((name', atts), [([eq], [])])]; - in ((lhs, (res_name, res)), lthy4) end; - -end; - - -(* axioms *) - -local - -fun add_axiom hyps (name, prop) thy = - let - val name' = if name = "" then "axiom_" ^ serial_string () else name; - val prop' = Logic.list_implies (hyps, prop); - val thy' = thy |> Theory.add_axioms_i [(name', prop')]; - val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name')); - val prems = map (Thm.assume o Thm.cterm_of thy') hyps; - in (Drule.implies_elim_list axm prems, thy') end; - -in - -fun axioms kind specs lthy = - let - val hyps = map Thm.term_of (Assumption.assms_of lthy); - fun axiom ((name, atts), props) thy = thy - |> fold_map (add_axiom hyps) (PureThy.name_multi name props) - |-> (fn ths => pair ((name, atts), [(ths, [])])); - in - lthy - |> fold (fold Variable.declare_term o snd) specs - |> LocalTheory.theory_result (fold_map axiom specs) - |-> LocalTheory.notes kind - end; - -end; - (* notes *) @@ -335,7 +130,7 @@ in (result'', result) end; -fun notes loc kind facts lthy = +fun local_notes loc kind facts lthy = let val is_loc = loc <> ""; val thy = ProofContext.theory_of lthy; @@ -364,24 +159,236 @@ end; +(* consts *) + +fun target_abbrev prmode ((c, mx), rhs) phi = + let + val c' = Morphism.name phi c; + val rhs' = Morphism.term phi rhs; + val arg' = (c', rhs'); + val eq_heads = + (case pairself Term.head_of (rhs, rhs') of + (Const (a, _), Const (a', _)) => a = a' + | _ => false); + in + eq_heads ? (Context.mapping_result + (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg') + #-> (fn (lhs, _) => + Term.equiv_types (rhs, rhs') ? + Morphism.form (ProofContext.target_notation prmode [(lhs, mx)]))) + end; + +fun internal_abbrev loc prmode ((c, mx), t) lthy = lthy + (* FIXME really permissive *) + |> term_syntax loc (perhaps o try o target_abbrev prmode ((c, mx), t)) + |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t) + |> snd; + +fun declare_consts loc depends decls lthy = + let + val thy = ProofContext.theory_of lthy; + val is_loc = loc <> ""; + val some_class = Class.class_of_locale thy loc; + + val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); + + fun const ((c, T), mx) thy = + let + val U = map #2 xs ---> T; + val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); + val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; + val mx3 = if is_loc then NoSyn else mx1; + val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy; + in (((c, mx2), t), thy') end; + fun const_class (SOME class) ((c, _), mx) (_, t) = + LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx)) + #-> Class.remove_constraint [class] + | const_class NONE _ _ = I; + fun hide_abbrev (SOME class) abbrs thy = + let + val raw_cs = map (fst o fst) abbrs; + val prfx = (Logic.const_of_class o NameSpace.base) class; + fun mk_name c = + let + val n1 = Sign.full_name thy c; + val n2 = NameSpace.qualifier n1; + val n3 = NameSpace.base n1; + in NameSpace.implode [n2, prfx, prfx, n3] end; + val cs = map mk_name raw_cs; + in + Sign.hide_consts_i true cs thy + end + | hide_abbrev NONE _ thy = thy; + + val (abbrs, lthy') = lthy + |> LocalTheory.theory_result (fold_map const decls) + val defs = map (apsnd (pair ("", []))) abbrs; + + in + lthy' + |> fold2 (const_class some_class) decls abbrs + |> is_loc ? fold (internal_abbrev loc Syntax.default_mode) abbrs + |> LocalTheory.raw_theory (hide_abbrev some_class abbrs) + (*FIXME abbreviations should never occur*) + |> LocalDefs.add_defs defs + |>> map (apsnd snd) + end; + + +(* abbrev *) + +fun occ_params ctxt ts = + #1 (ProofContext.inferred_fixes ctxt) + |> filter (member (op =) (fold (Variable.add_fixed ctxt) ts [])); + +fun local_abbrev (x, rhs) = + Variable.add_fixes [x] #-> (fn [x'] => + let + val T = Term.fastype_of rhs; + val lhs = Free (x', T); + in + Variable.declare_term lhs #> + Variable.declare_term rhs #> + Assumption.add_assms (K (K (I, Envir.expand_term_frees [((x', T), rhs)]))) [] #> snd #> + pair (lhs, rhs) + end); + +fun abbrev loc prmode ((raw_c, mx), raw_t) lthy = + let + val thy = ProofContext.theory_of lthy; + val is_loc = loc <> ""; + val some_class = Class.class_of_locale thy loc; + + val thy_ctxt = ProofContext.init thy; + val target = LocalTheory.target_of lthy; + val target_morphism = LocalTheory.target_morphism lthy; + + val c = Morphism.name target_morphism raw_c; + val t = Morphism.term target_morphism raw_t; + val xs = map Free (occ_params target [t]); + val u = fold_rev Term.lambda xs t; + val U = Term.fastype_of u; + val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u; + val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; + val mx3 = if is_loc then NoSyn else mx1; + fun add_abbrev_in_class (SOME class) abbr = + LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr) + #-> (fn c => Class.remove_constraint [class] c) + | add_abbrev_in_class NONE _ = I; + in + lthy + |> LocalTheory.theory_result + (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u')) + |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)]) + #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) + #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) + #> local_abbrev (c, rhs)) + end; + + +(* defs *) + +local + +fun expand_term ctxt t = + let + val thy = ProofContext.theory_of ctxt; + val thy_ctxt = ProofContext.init thy; + val ct = Thm.cterm_of thy t; + val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term; + in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end; + +fun add_def (name, prop) thy = + let + val tfrees = rev (map TFree (Term.add_tfrees prop [])); + val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); + val strip_sorts = tfrees ~~ tfrees'; + val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees); + + val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; + val thy' = Theory.add_defs_i false false [(name, prop')] thy; + val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name); + val def = Thm.instantiate (recover_sorts, []) axm'; + in (Drule.unvarify def, thy') end; + +in + +fun local_def loc kind ((c, mx), ((name, atts), rhs)) lthy1 = + let + val (rhs', rhs_conv) = expand_term lthy1 rhs; + val xs = Variable.add_fixed (LocalTheory.target_of lthy1) rhs' []; + val T = Term.fastype_of rhs; + + (*consts*) + val ([(lhs, lhs_def)], lthy2) = lthy1 + |> declare_consts loc (member (op =) xs) [((c, T), mx)]; + val (_, lhs') = Logic.dest_equals (Thm.prop_of lhs_def); + + (*def*) + val name' = Thm.def_name_optional c name; + val (def, lthy3) = lthy2 + |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs'))); + val eq = LocalDefs.trans_terms lthy3 + [(*c == loc.c xs*) lhs_def, + (*lhs' == rhs'*) def, + (*rhs' == rhs*) Thm.symmetric rhs_conv]; + + (*notes*) + val ([(res_name, [res])], lthy4) = lthy3 + |> local_notes loc kind [((name', atts), [([eq], [])])]; + in ((lhs, (res_name, res)), lthy4) end; + +end; + + +(* axioms *) + +local + +fun add_axiom hyps (name, prop) thy = + let + val name' = if name = "" then "axiom_" ^ serial_string () else name; + val prop' = Logic.list_implies (hyps, prop); + val thy' = thy |> Theory.add_axioms_i [(name', prop')]; + val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name')); + val prems = map (Thm.assume o Thm.cterm_of thy') hyps; + in (Drule.implies_elim_list axm prems, thy') end; + +in + +fun axioms loc kind specs lthy = + let + val hyps = map Thm.term_of (Assumption.assms_of lthy); + fun axiom ((name, atts), props) thy = thy + |> fold_map (add_axiom hyps) (PureThy.name_multi name props) + |-> (fn ths => pair ((name, atts), [(ths, [])])); + in + lthy + |> fold (fold Variable.declare_term o snd) specs + |> LocalTheory.theory_result (fold_map axiom specs) + |-> local_notes loc kind + end; + +end; + + (* init and exit *) fun begin loc ctxt = let val thy = ProofContext.theory_of ctxt; val is_loc = loc <> ""; - val some_class = Class.class_of_locale thy loc; in ctxt |> Data.put (if is_loc then SOME loc else NONE) - |> fold Class.init (the_list some_class) + |> fold Class.init (the_list (Class.class_of_locale thy loc)) |> LocalTheory.init (NameSpace.base loc) {pretty = pretty loc, - consts = consts is_loc some_class, - axioms = axioms, - abbrev = abbrev is_loc some_class, - def = local_def, - notes = notes loc, + consts = declare_consts loc, + axioms = axioms loc, + abbrev = abbrev loc, + def = local_def loc, + notes = local_notes loc, type_syntax = type_syntax loc, term_syntax = term_syntax loc, declaration = declaration loc,