sort assignment before simultaneous term_check, not isolated parse_term;
authorwenzelm
Wed Nov 09 17:57:42 2011 +0100 (2011-11-09)
changeset 45427fca432074fb2
parent 45426 4548b8e1ba12
child 45428 aa35c9454a95
sort assignment before simultaneous term_check, not isolated parse_term;
prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment;
simplified Syntax_Phases.decode_sort/decode_typ;
discontinued unused Proof_Context.check_tvar;
NEWS
src/HOL/Tools/record.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/sign.ML
     1.1 --- a/NEWS	Wed Nov 09 17:12:26 2011 +0100
     1.2 +++ b/NEWS	Wed Nov 09 17:57:42 2011 +0100
     1.3 @@ -16,6 +16,16 @@
     1.4  * Redundant attribute 'code_inline' has been discontinued. Use
     1.5  'code_unfold' instead. INCOMPATIBILITY.
     1.6  
     1.7 +* Sort constraints are now propagated in simultaneous statements, just
     1.8 +like type constraints.  INCOMPATIBILITY in rare situations, where
     1.9 +distinct sorts used to be assigned accidentally.  For example:
    1.10 +
    1.11 +  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
    1.12 +
    1.13 +  lemma "P (x::'a)" and "Q (y::'a::bar)"
    1.14 +    -- "now uniform 'a::bar instead of default sort for first occurence (!)"
    1.15 +
    1.16 +
    1.17  
    1.18  *** HOL ***
    1.19  
     2.1 --- a/src/HOL/Tools/record.ML	Wed Nov 09 17:12:26 2011 +0100
     2.2 +++ b/src/HOL/Tools/record.ML	Wed Nov 09 17:57:42 2011 +0100
     2.3 @@ -652,12 +652,6 @@
     2.4  
     2.5  (** concrete syntax for records **)
     2.6  
     2.7 -(* decode type *)
     2.8 -
     2.9 -fun decode_type ctxt t =
    2.10 -  Syntax_Phases.typ_of_term (Proof_Context.get_sort ctxt (Syntax_Phases.term_sorts t)) t;
    2.11 -
    2.12 -
    2.13  (* parse translations *)
    2.14  
    2.15  local
    2.16 @@ -694,7 +688,7 @@
    2.17                      val types = map snd fields';
    2.18                      val (args, rest) = split_args (map fst fields') fargs
    2.19                        handle Fail msg => err msg;
    2.20 -                    val argtypes = map (Syntax.check_typ ctxt o decode_type ctxt) args;
    2.21 +                    val argtypes = map (Syntax.check_typ ctxt o Syntax_Phases.decode_typ) args;
    2.22                      val varifyT = varifyT (fold Term.maxidx_typ argtypes 0 + 1);
    2.23                      val vartypes = map varifyT types;
    2.24  
    2.25 @@ -799,7 +793,7 @@
    2.26    let
    2.27      val thy = Proof_Context.theory_of ctxt;
    2.28  
    2.29 -    val T = decode_type ctxt t;
    2.30 +    val T = Syntax_Phases.decode_typ t;
    2.31      val varifyT = varifyT (Term.maxidx_of_typ T + 1);
    2.32  
    2.33      fun strip_fields T =
    2.34 @@ -844,7 +838,7 @@
    2.35    the (nested) extension types*)
    2.36  fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
    2.37    let
    2.38 -    val T = decode_type ctxt tm;
    2.39 +    val T = Syntax_Phases.decode_typ tm;
    2.40      val varifyT = varifyT (maxidx_of_typ T + 1);
    2.41  
    2.42      fun mk_type_abbr subst name args =
     3.1 --- a/src/Pure/Isar/proof_context.ML	Wed Nov 09 17:12:26 2011 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Nov 09 17:57:42 2011 +0100
     3.3 @@ -72,7 +72,6 @@
     3.4    val read_const: Proof.context -> bool -> typ -> string -> term
     3.5    val allow_dummies: Proof.context -> Proof.context
     3.6    val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
     3.7 -  val check_tvar: Proof.context -> indexname * sort -> indexname * sort
     3.8    val check_tfree: Proof.context -> string * sort -> string * sort
     3.9    val intern_skolem: Proof.context -> string -> string option
    3.10    val read_term_pattern: Proof.context -> string -> term
    3.11 @@ -639,8 +638,7 @@
    3.12              " for type variable " ^ quote (Term.string_of_vname' xi)));
    3.13    in get end;
    3.14  
    3.15 -fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
    3.16 -fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
    3.17 +fun check_tfree ctxt (x, S) = (x, get_sort ctxt [((x, ~1), S)] (x, ~1));
    3.18  
    3.19  
    3.20  (* certify terms *)
    3.21 @@ -940,7 +938,7 @@
    3.22  
    3.23  in
    3.24  
    3.25 -val read_vars = prep_vars Syntax.parse_typ false;
    3.26 +val read_vars = prep_vars Syntax.read_typ false;
    3.27  val cert_vars = prep_vars (K I) true;
    3.28  
    3.29  end;
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 17:12:26 2011 +0100
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 17:57:42 2011 +0100
     4.3 @@ -7,8 +7,8 @@
     4.4  
     4.5  signature SYNTAX_PHASES =
     4.6  sig
     4.7 -  val term_sorts: term -> (indexname * sort) list
     4.8 -  val typ_of_term: (indexname -> sort) -> term -> typ
     4.9 +  val decode_sort: term -> sort
    4.10 +  val decode_typ: term -> typ
    4.11    val decode_term: Proof.context ->
    4.12      Position.report list * term Exn.result -> Position.report list * term Exn.result
    4.13    val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    4.14 @@ -58,11 +58,11 @@
    4.15  
    4.16  (** decode parse trees **)
    4.17  
    4.18 -(* sort_of_term *)
    4.19 +(* decode_sort *)
    4.20  
    4.21 -fun sort_of_term tm =
    4.22 +fun decode_sort tm =
    4.23    let
    4.24 -    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    4.25 +    fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
    4.26  
    4.27      fun class s = Lexicon.unmark_class s handle Fail _ => err ();
    4.28  
    4.29 @@ -77,52 +77,32 @@
    4.30    in sort tm end;
    4.31  
    4.32  
    4.33 -(* term_sorts *)
    4.34 -
    4.35 -fun term_sorts tm =
    4.36 -  let
    4.37 -    val sort_of = sort_of_term;
    4.38 +(* decode_typ *)
    4.39  
    4.40 -    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
    4.41 -          insert (op =) ((x, ~1), sort_of cs)
    4.42 -      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
    4.43 -          insert (op =) ((x, ~1), sort_of cs)
    4.44 -      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
    4.45 -          insert (op =) (xi, sort_of cs)
    4.46 -      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
    4.47 -          insert (op =) (xi, sort_of cs)
    4.48 -      | add_env (Abs (_, _, t)) = add_env t
    4.49 -      | add_env (t1 $ t2) = add_env t1 #> add_env t2
    4.50 -      | add_env _ = I;
    4.51 -  in add_env tm [] end;
    4.52 +fun decode_typ tm =
    4.53 +  let
    4.54 +    fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
    4.55  
    4.56 -
    4.57 -(* typ_of_term *)
    4.58 -
    4.59 -fun typ_of_term get_sort tm =
    4.60 -  let
    4.61 -    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
    4.62 -
    4.63 -    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
    4.64 -      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    4.65 -      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
    4.66 -      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
    4.67 -      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
    4.68 -      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
    4.69 -          TFree (x, get_sort (x, ~1))
    4.70 -      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
    4.71 -      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
    4.72 -          TVar (xi, get_sort xi)
    4.73 -      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
    4.74 -      | typ_of t =
    4.75 +    fun typ (Free (x, _)) = TFree (x, dummyS)
    4.76 +      | typ (Var (xi, _)) = TVar (xi, dummyS)
    4.77 +      | typ (Const ("_tfree",_) $ (t as Free _)) = typ t
    4.78 +      | typ (Const ("_tvar",_) $ (t as Var _)) = typ t
    4.79 +      | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s)
    4.80 +      | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) =
    4.81 +          TFree (x, decode_sort s)
    4.82 +      | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s)
    4.83 +      | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) =
    4.84 +          TVar (xi, decode_sort s)
    4.85 +      | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s)
    4.86 +      | typ t =
    4.87            let
    4.88              val (head, args) = Term.strip_comb t;
    4.89              val a =
    4.90                (case head of
    4.91                  Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
    4.92                | _ => err ());
    4.93 -          in Type (a, map typ_of args) end;
    4.94 -  in typ_of tm end;
    4.95 +          in Type (a, map typ args) end;
    4.96 +  in typ tm end;
    4.97  
    4.98  
    4.99  (* parsetree_to_ast *)
   4.100 @@ -207,19 +187,17 @@
   4.101              handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
   4.102          val get_free = Proof_Context.intern_skolem ctxt;
   4.103  
   4.104 -        val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
   4.105 -
   4.106          val reports = Unsynchronized.ref reports0;
   4.107          fun report ps = Position.store_reports reports ps;
   4.108  
   4.109          fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
   4.110                (case Term_Position.decode_position typ of
   4.111                  SOME p => decode (p :: ps) qs bs t
   4.112 -              | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
   4.113 +              | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
   4.114            | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
   4.115                (case Term_Position.decode_position typ of
   4.116                  SOME q => decode ps (q :: qs) bs t
   4.117 -              | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
   4.118 +              | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
   4.119            | decode _ qs bs (Abs (x, T, t)) =
   4.120                let
   4.121                  val id = serial ();
   4.122 @@ -328,7 +306,7 @@
   4.123      (fn (syms, pos) =>
   4.124        parse_raw ctxt "sort" (syms, pos)
   4.125        |> report_result ctxt pos
   4.126 -      |> sort_of_term
   4.127 +      |> decode_sort
   4.128        |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
   4.129        handle ERROR msg => parse_failed ctxt pos msg "sort");
   4.130  
   4.131 @@ -337,7 +315,7 @@
   4.132      (fn (syms, pos) =>
   4.133        parse_raw ctxt "type" (syms, pos)
   4.134        |> report_result ctxt pos
   4.135 -      |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
   4.136 +      |> decode_typ
   4.137        handle ERROR msg => parse_failed ctxt pos msg "type");
   4.138  
   4.139  fun parse_term is_prop ctxt =
   4.140 @@ -714,11 +692,31 @@
   4.141  
   4.142  (** check/uncheck **)
   4.143  
   4.144 +fun prepare_types ctxt tys =
   4.145 +  let
   4.146 +    fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
   4.147 +    val env =
   4.148 +      (fold o fold_atyps)
   4.149 +        (fn TFree (x, S) => constraint ((x, ~1), S)
   4.150 +          | TVar v => constraint v
   4.151 +          | _ => I) tys [];
   4.152 +    val get_sort = Proof_Context.get_sort ctxt env;
   4.153 +  in
   4.154 +    (map o map_atyps)
   4.155 +      (fn TFree (x, _) => TFree (x, get_sort (x, ~1))
   4.156 +        | TVar (xi, _) => TVar (xi, get_sort xi)
   4.157 +        | T => T) tys
   4.158 +  end;
   4.159 +
   4.160  fun check_typs ctxt =
   4.161 -  Syntax.apply_typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt);
   4.162 +  prepare_types ctxt #>
   4.163 +  Syntax.apply_typ_check ctxt #>
   4.164 +  Term_Sharing.typs (Proof_Context.theory_of ctxt);
   4.165  
   4.166  fun check_terms ctxt =
   4.167 -  Syntax.apply_term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt);
   4.168 +  Term.burrow_types (prepare_types ctxt) #>
   4.169 +  Syntax.apply_term_check ctxt #>
   4.170 +  Term_Sharing.terms (Proof_Context.theory_of ctxt);
   4.171  
   4.172  fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
   4.173  
     5.1 --- a/src/Pure/sign.ML	Wed Nov 09 17:12:26 2011 +0100
     5.2 +++ b/src/Pure/sign.ML	Wed Nov 09 17:57:42 2011 +0100
     5.3 @@ -361,18 +361,18 @@
     5.4  
     5.5  fun gen_syntax change_gram parse_typ mode args thy =
     5.6    let
     5.7 -    val ctxt = Proof_Context.init_global thy;
     5.8 +    val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
     5.9      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
    5.10        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
    5.11    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    5.12  
    5.13  fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
    5.14  
    5.15 -val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    5.16 +val add_modesyntax = gen_add_syntax Syntax.read_typ;
    5.17  val add_modesyntax_i = gen_add_syntax (K I);
    5.18  val add_syntax = add_modesyntax Syntax.mode_default;
    5.19  val add_syntax_i = add_modesyntax_i Syntax.mode_default;
    5.20 -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
    5.21 +val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
    5.22  val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
    5.23  
    5.24  fun type_notation add mode args =
    5.25 @@ -396,9 +396,9 @@
    5.26  
    5.27  local
    5.28  
    5.29 -fun gen_add_consts parse_typ ctxt raw_args thy =
    5.30 +fun gen_add_consts prep_typ ctxt raw_args thy =
    5.31    let
    5.32 -    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    5.33 +    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt;
    5.34      fun prep (b, raw_T, mx) =
    5.35        let
    5.36          val c = full_name thy b;
    5.37 @@ -417,7 +417,8 @@
    5.38  in
    5.39  
    5.40  fun add_consts args thy =
    5.41 -  #2 (gen_add_consts Syntax.parse_typ (Proof_Context.init_global thy) args thy);
    5.42 +  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
    5.43 +
    5.44  fun add_consts_i args thy =
    5.45    #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
    5.46