renamed is_abbrev_mode to abbrev_mode;
authorwenzelm
Thu Jun 19 22:05:05 2008 +0200 (2008-06-19 ago)
changeset 272862ea20e5fdf16
parent 27285 def40a211768
child 27287 3b0d7a417a8b
renamed is_abbrev_mode to abbrev_mode;
added private get_sort (from sign.ML);
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jun 19 22:05:04 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jun 19 22:05:05 2008 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val set_mode: mode -> Proof.context -> Proof.context
     1.5    val get_mode: Proof.context -> mode
     1.6    val restore_mode: Proof.context -> Proof.context -> Proof.context
     1.7 -  val is_abbrev_mode: Proof.context -> bool
     1.8 +  val abbrev_mode: Proof.context -> bool
     1.9    val set_stmt: bool -> Proof.context -> Proof.context
    1.10    val naming_of: Proof.context -> NameSpace.naming
    1.11    val full_name: Proof.context -> bstring -> string
    1.12 @@ -166,8 +166,6 @@
    1.13  fun make_mode (stmt, pattern, schematic, abbrev) =
    1.14    Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev};
    1.15  
    1.16 -fun dest_mode (Mode mode) = mode;
    1.17 -
    1.18  val mode_default   = make_mode (false, false, false, false);
    1.19  val mode_stmt      = make_mode (true, false, false, false);
    1.20  val mode_pattern   = make_mode (false, true, false, false);
    1.21 @@ -236,6 +234,7 @@
    1.22  
    1.23  val get_mode = #mode o rep_context;
    1.24  fun restore_mode ctxt = set_mode (get_mode ctxt);
    1.25 +val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
    1.26  
    1.27  fun set_stmt stmt =
    1.28    map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
    1.29 @@ -442,12 +441,10 @@
    1.30  
    1.31  val tsig_of = Sign.tsig_of o ProofContext.theory_of;
    1.32  
    1.33 -val is_abbrev_mode = #abbrev o dest_mode o get_mode;
    1.34 -
    1.35  local
    1.36  
    1.37  fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
    1.38 -  (not (is_abbrev_mode ctxt)) (consts_of ctxt);
    1.39 +  (not (abbrev_mode ctxt)) (consts_of ctxt);
    1.40  
    1.41  fun reject_schematic (Var (xi, _)) =
    1.42        error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
    1.43 @@ -520,6 +517,30 @@
    1.44  
    1.45  (* decoding raw terms (syntax trees) *)
    1.46  
    1.47 +(* types *)
    1.48 +
    1.49 +fun get_sort thy def_sort raw_env =
    1.50 +  let
    1.51 +    val tsig = Sign.tsig_of thy;
    1.52 +
    1.53 +    fun eq ((xi, S), (xi', S')) =
    1.54 +      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
    1.55 +    val env = distinct eq raw_env;
    1.56 +    val _ = (case duplicates (eq_fst (op =)) env of [] => ()
    1.57 +      | dups => error ("Inconsistent sort constraints for type variable(s) "
    1.58 +          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
    1.59 +
    1.60 +    fun get xi =
    1.61 +      (case (AList.lookup (op =) env xi, def_sort xi) of
    1.62 +        (NONE, NONE) => Type.defaultS tsig
    1.63 +      | (NONE, SOME S) => S
    1.64 +      | (SOME S, NONE) => S
    1.65 +      | (SOME S, SOME S') =>
    1.66 +          if Type.eq_sort tsig (S, S') then S'
    1.67 +          else error ("Sort constraint inconsistent with default for type variable " ^
    1.68 +            quote (Term.string_of_vname' xi)));
    1.69 +  in get end;
    1.70 +
    1.71  local
    1.72  
    1.73  fun intern_skolem ctxt def_type x =
    1.74 @@ -539,7 +560,7 @@
    1.75  
    1.76  fun term_context ctxt =
    1.77    let val thy = theory_of ctxt in
    1.78 -   {get_sort = Sign.get_sort thy (Variable.def_sort ctxt),
    1.79 +   {get_sort = get_sort thy (Variable.def_sort ctxt),
    1.80      map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt a)))
    1.81        handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
    1.82      map_free = intern_skolem ctxt (Variable.def_type ctxt false),
    1.83 @@ -621,7 +642,7 @@
    1.84  fun parse_typ ctxt str =
    1.85    let
    1.86      val thy = ProofContext.theory_of ctxt;
    1.87 -    val get_sort = Sign.get_sort thy (Variable.def_sort ctxt);
    1.88 +    val get_sort = get_sort thy (Variable.def_sort ctxt);
    1.89      val T = Sign.intern_tycons thy
    1.90        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str);
    1.91    in T end