localized default sort;
authorwenzelm
Wed Apr 28 11:41:27 2010 +0200 (2010-04-28 ago)
changeset 36451ddc965e172c4
parent 36450 62eaaffe6e47
child 36452 d37c6eed8117
localized default sort;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:13:11 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:41:27 2010 +0200
     1.3 @@ -96,9 +96,9 @@
     1.4      >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     1.8 -    (P.sort >>
     1.9 -      (fn s => Toplevel.theory (fn thy => Sign.set_defsort (Syntax.read_sort_global thy s) thy)));
    1.10 +  OuterSyntax.local_theory "defaultsort" "declare default sort for explicit type variables"
    1.11 +    K.thy_decl
    1.12 +    (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
    1.13  
    1.14  
    1.15  (* types *)
     2.1 --- a/src/Pure/Isar/local_theory.ML	Wed Apr 28 11:13:11 2010 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Apr 28 11:41:27 2010 +0200
     2.3 @@ -40,6 +40,7 @@
     2.4      local_theory -> (string * thm list) list * local_theory
     2.5    val declaration: bool -> declaration -> local_theory -> local_theory
     2.6    val syntax_declaration: bool -> declaration -> local_theory -> local_theory
     2.7 +  val set_defsort: sort -> local_theory -> local_theory
     2.8    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     2.9    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.10    val class_alias: binding -> class -> local_theory -> local_theory
    2.11 @@ -183,7 +184,7 @@
    2.12  fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
    2.13  
    2.14  
    2.15 -(* basic operations *)
    2.16 +(* primitive operations *)
    2.17  
    2.18  fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    2.19  fun operation1 f x = operation (fn ops => f ops x);
    2.20 @@ -196,9 +197,16 @@
    2.21  val declaration = checkpoint ooo operation2 #declaration;
    2.22  val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
    2.23  
    2.24 +
    2.25 +
    2.26 +(** basic derived operations **)
    2.27 +
    2.28  val notes = notes_kind "";
    2.29  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    2.30  
    2.31 +fun set_defsort S =
    2.32 +  syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (ProofContext.set_defsort S)));
    2.33 +
    2.34  
    2.35  (* notation *)
    2.36  
    2.37 @@ -224,6 +232,9 @@
    2.38  val const_alias = alias Sign.const_alias ProofContext.const_alias;
    2.39  
    2.40  
    2.41 +
    2.42 +(** init and exit **)
    2.43 +
    2.44  (* init *)
    2.45  
    2.46  fun init group theory_prefix operations target =
     3.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:13:11 2010 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:41:27 2010 +0200
     3.3 @@ -28,6 +28,7 @@
     3.4    val full_name: Proof.context -> binding -> string
     3.5    val syn_of: Proof.context -> Syntax.syntax
     3.6    val tsig_of: Proof.context -> Type.tsig
     3.7 +  val set_defsort: sort -> Proof.context -> Proof.context
     3.8    val default_sort: Proof.context -> indexname -> sort
     3.9    val consts_of: Proof.context -> Consts.T
    3.10    val the_const_constraint: Proof.context -> string -> typ
    3.11 @@ -178,12 +179,12 @@
    3.12  
    3.13  datatype ctxt =
    3.14    Ctxt of
    3.15 -   {mode: mode,                       (*inner syntax mode*)
    3.16 -    naming: Name_Space.naming,        (*local naming conventions*)
    3.17 -    syntax: Local_Syntax.T,           (*local syntax*)
    3.18 -    tsig: Type.tsig * Type.tsig,      (*local/global type signature -- local name space only*)
    3.19 -    consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
    3.20 -    facts: Facts.T,                   (*local facts*)
    3.21 +   {mode: mode,                  (*inner syntax mode*)
    3.22 +    naming: Name_Space.naming,   (*local naming conventions*)
    3.23 +    syntax: Local_Syntax.T,      (*local syntax*)
    3.24 +    tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
    3.25 +    consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
    3.26 +    facts: Facts.T,              (*local facts*)
    3.27      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    3.28  
    3.29  fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) =
    3.30 @@ -255,6 +256,7 @@
    3.31  val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
    3.32  
    3.33  val tsig_of = #1 o #tsig o rep_context;
    3.34 +val set_defsort = map_tsig o apfst o Type.set_defsort;
    3.35  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    3.36  
    3.37  val consts_of = #1 o #consts o rep_context;