# HG changeset patch # User haftmann # Date 1402263049 -7200 # Node ID 5140ddfccea76424622e14380c5080e1c5e4b014 # Parent 329f7f76f0a416a688205023b7cceeab414e10b6 re-unified approach towards class and locale consts, with refined terminology: foo_const_declaration denotes declaration for a particular logical layer, foo_const the full stack for a particular target diff -r 329f7f76f0a4 -r 5140ddfccea7 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sun Jun 08 23:30:48 2014 +0200 +++ b/src/Pure/Isar/class.ML Sun Jun 08 23:30:49 2014 +0200 @@ -333,17 +333,14 @@ val rhs2 = Morphism.term phi2 rhs; in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end; -fun class_const class phi0 prmode ((b, mx), rhs) = - Generic_Target.locale_declaration class true (fn phi => - let - val b' = Morphism.binding phi b; - val rhs' = Morphism.term phi rhs; - val same_shape = Term.aconv_untyped (rhs, rhs'); - val is_plain = guess_morphism_identity (b, rhs) Morphism.identity phi; - val is_canonical = guess_morphism_identity (b, rhs) phi0 phi; - in - not (is_plain orelse is_canonical) ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs') - end); +fun const_declaration class phi0 prmode ((b, _), rhs) = + let + val guess_identity = guess_morphism_identity (b, rhs) Morphism.identity; + val guess_canonical = guess_morphism_identity (b, rhs) phi0; + in + Generic_Target.locale_const_declaration class + (not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs) + end; fun dangling_params_for lthy class (type_params, term_params) = let @@ -402,10 +399,10 @@ val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params)); in lthy - |> class_const class phi Syntax.mode_default ((b, mx), lhs) + |> const_declaration class phi Syntax.mode_default ((b, mx), lhs) |> Local_Theory.raw_theory (canonical_const class phi dangling_params ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs)) - |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) + |> Generic_Target.standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other) Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs) |> synchronize_class_syntax_target class end; @@ -416,10 +413,10 @@ val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params)); in lthy - |> class_const class phi prmode ((b, mx), lhs) + |> const_declaration class phi prmode ((b, mx), lhs) |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs')) - |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) + |> Generic_Target.standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, if null dangling_term_params then NoSyn else mx), lhs) |> synchronize_class_syntax_target class end; diff -r 329f7f76f0a4 -r 5140ddfccea7 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Sun Jun 08 23:30:48 2014 +0200 +++ b/src/Pure/Isar/generic_target.ML Sun Jun 08 23:30:49 2014 +0200 @@ -27,10 +27,10 @@ val background_declaration: declaration -> local_theory -> local_theory val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory val standard_declaration: (int * int -> bool) -> declaration -> local_theory -> local_theory - val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term -> - Context.generic -> Context.generic - val const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> + val standard_const_declaration: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory + val locale_const_declaration: string -> (morphism -> bool) -> Syntax.mode -> + (binding * mixfix) * term -> local_theory -> local_theory val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> @@ -246,49 +246,50 @@ (* const declaration *) -fun generic_const same_shape prmode ((b, mx), t) context = - let - val const_alias = - if same_shape then - (case t of - Const (c, T) => - let - val thy = Context.theory_of context; - val ctxt = Context.proof_of context; - in - (case Type_Infer_Context.const_type ctxt c of - SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE - | NONE => NONE) - end - | _ => NONE) - else NONE; - in - (case const_alias of - SOME c => - context - |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) - |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) - | NONE => - context - |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t) - |-> (fn (const as Const (c, _), _) => same_shape ? - (Proof_Context.generic_revert_abbrev (#1 prmode) c #> - Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) - end; +fun const_decl phi_pred prmode ((b, mx), rhs) phi context = + if phi_pred phi then + let + val b' = Morphism.binding phi b; + val rhs' = Morphism.term phi rhs; + val same_shape = Term.aconv_untyped (rhs, rhs'); + val const_alias = + if same_shape then + (case rhs' of + Const (c, T) => + let + val thy = Context.theory_of context; + val ctxt = Context.proof_of context; + in + (case Type_Infer_Context.const_type ctxt c of + SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE + | NONE => NONE) + end + | _ => NONE) + else NONE; + in + case const_alias of + SOME c => + context + |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c) + |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)]) + | NONE => + context + |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs') + |-> (fn (const as Const (c, _), _) => same_shape ? + (Proof_Context.generic_revert_abbrev (#1 prmode) c #> + Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))) + end + else context; -fun standard_const prmode ((b, mx), rhs) phi = - let - val b' = Morphism.binding phi b; - val rhs' = Morphism.term phi rhs; - val same_shape = Term.aconv_untyped (rhs, rhs'); - in generic_const same_shape prmode ((b', mx), rhs') end; +fun standard_const_declaration pred prmode ((b, mx), rhs) = + standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs)); -fun const pred prmode ((b, mx), rhs) = - standard_declaration pred (standard_const prmode ((b, mx), rhs)); +fun locale_const_declaration locale phi_pred prmode ((b, mx), rhs) = + locale_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs)) fun locale_const locale prmode ((b, mx), rhs) = - locale_declaration locale true (standard_const prmode ((b, mx), rhs)) - #> const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); + locale_const_declaration locale (K true) prmode ((b, mx), rhs) + #> standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); (* registrations and dependencies *) @@ -321,7 +322,7 @@ fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) - #-> (fn (lhs, def) => const (op <>) Syntax.mode_default ((b, mx), lhs) + #-> (fn (lhs, def) => standard_const_declaration (op <>) Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun theory_notes kind global_facts local_facts = @@ -337,7 +338,7 @@ (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) => (* FIXME type_params!? *) Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) - #-> (fn lhs => const (op <>) prmode + #-> (fn lhs => standard_const_declaration (op <>) prmode ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params))); fun theory_declaration decl =