# HG changeset patch # User wenzelm # Date 1320857862 -3600 # Node ID fca432074fb229cd31c9fb6f1ee610b7f811fbaa # Parent 4548b8e1ba12c74e36c67eecac449cafc3a75fc4 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; diff -r 4548b8e1ba12 -r fca432074fb2 NEWS --- a/NEWS Wed Nov 09 17:12:26 2011 +0100 +++ b/NEWS Wed Nov 09 17:57:42 2011 +0100 @@ -16,6 +16,16 @@ * Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold' instead. INCOMPATIBILITY. +* Sort constraints are now propagated in simultaneous statements, just +like type constraints. INCOMPATIBILITY in rare situations, where +distinct sorts used to be assigned accidentally. For example: + + lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" + + lemma "P (x::'a)" and "Q (y::'a::bar)" + -- "now uniform 'a::bar instead of default sort for first occurence (!)" + + *** HOL *** diff -r 4548b8e1ba12 -r fca432074fb2 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Nov 09 17:12:26 2011 +0100 +++ b/src/HOL/Tools/record.ML Wed Nov 09 17:57:42 2011 +0100 @@ -652,12 +652,6 @@ (** concrete syntax for records **) -(* decode type *) - -fun decode_type ctxt t = - Syntax_Phases.typ_of_term (Proof_Context.get_sort ctxt (Syntax_Phases.term_sorts t)) t; - - (* parse translations *) local @@ -694,7 +688,7 @@ val types = map snd fields'; val (args, rest) = split_args (map fst fields') fargs handle Fail msg => err msg; - val argtypes = map (Syntax.check_typ ctxt o decode_type ctxt) args; + val argtypes = map (Syntax.check_typ ctxt o Syntax_Phases.decode_typ) args; val varifyT = varifyT (fold Term.maxidx_typ argtypes 0 + 1); val vartypes = map varifyT types; @@ -799,7 +793,7 @@ let val thy = Proof_Context.theory_of ctxt; - val T = decode_type ctxt t; + val T = Syntax_Phases.decode_typ t; val varifyT = varifyT (Term.maxidx_of_typ T + 1); fun strip_fields T = @@ -844,7 +838,7 @@ the (nested) extension types*) fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm = let - val T = decode_type ctxt tm; + val T = Syntax_Phases.decode_typ tm; val varifyT = varifyT (maxidx_of_typ T + 1); fun mk_type_abbr subst name args = diff -r 4548b8e1ba12 -r fca432074fb2 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Nov 09 17:12:26 2011 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 09 17:57:42 2011 +0100 @@ -72,7 +72,6 @@ val read_const: Proof.context -> bool -> typ -> string -> term val allow_dummies: Proof.context -> Proof.context val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort - val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort val intern_skolem: Proof.context -> string -> string option val read_term_pattern: Proof.context -> string -> term @@ -639,8 +638,7 @@ " for type variable " ^ quote (Term.string_of_vname' xi))); in get end; -fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi); -fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S)); +fun check_tfree ctxt (x, S) = (x, get_sort ctxt [((x, ~1), S)] (x, ~1)); (* certify terms *) @@ -940,7 +938,7 @@ in -val read_vars = prep_vars Syntax.parse_typ false; +val read_vars = prep_vars Syntax.read_typ false; val cert_vars = prep_vars (K I) true; end; diff -r 4548b8e1ba12 -r fca432074fb2 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Nov 09 17:12:26 2011 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Nov 09 17:57:42 2011 +0100 @@ -7,8 +7,8 @@ signature SYNTAX_PHASES = sig - val term_sorts: term -> (indexname * sort) list - val typ_of_term: (indexname -> sort) -> term -> typ + val decode_sort: term -> sort + val decode_typ: term -> typ val decode_term: Proof.context -> Position.report list * term Exn.result -> Position.report list * term Exn.result val parse_ast_pattern: Proof.context -> string * string -> Ast.ast @@ -58,11 +58,11 @@ (** decode parse trees **) -(* sort_of_term *) +(* decode_sort *) -fun sort_of_term tm = +fun decode_sort tm = let - fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]); + fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]); fun class s = Lexicon.unmark_class s handle Fail _ => err (); @@ -77,52 +77,32 @@ in sort tm end; -(* term_sorts *) - -fun term_sorts tm = - let - val sort_of = sort_of_term; +(* decode_typ *) - fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) = - insert (op =) ((x, ~1), sort_of cs) - | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) = - insert (op =) ((x, ~1), sort_of cs) - | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) = - insert (op =) (xi, sort_of cs) - | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) = - insert (op =) (xi, sort_of cs) - | add_env (Abs (_, _, t)) = add_env t - | add_env (t1 $ t2) = add_env t1 #> add_env t2 - | add_env _ = I; - in add_env tm [] end; +fun decode_typ tm = + let + fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]); - -(* typ_of_term *) - -fun typ_of_term get_sort tm = - let - fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]); - - fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1)) - | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) - | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t - | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t - | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1)) - | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) = - TFree (x, get_sort (x, ~1)) - | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi) - | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) = - TVar (xi, get_sort xi) - | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t) - | typ_of t = + fun typ (Free (x, _)) = TFree (x, dummyS) + | typ (Var (xi, _)) = TVar (xi, dummyS) + | typ (Const ("_tfree",_) $ (t as Free _)) = typ t + | typ (Const ("_tvar",_) $ (t as Var _)) = typ t + | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s) + | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) = + TFree (x, decode_sort s) + | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s) + | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) = + TVar (xi, decode_sort s) + | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s) + | typ t = let val (head, args) = Term.strip_comb t; val a = (case head of Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ()) | _ => err ()); - in Type (a, map typ_of args) end; - in typ_of tm end; + in Type (a, map typ args) end; + in typ tm end; (* parsetree_to_ast *) @@ -207,19 +187,17 @@ handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a)); val get_free = Proof_Context.intern_skolem ctxt; - val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm)); - val reports = Unsynchronized.ref reports0; fun report ps = Position.store_reports reports ps; fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = (case Term_Position.decode_position typ of SOME p => decode (p :: ps) qs bs t - | NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) + | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t)) | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = (case Term_Position.decode_position typ of SOME q => decode ps (q :: qs) bs t - | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) + | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t)) | decode _ qs bs (Abs (x, T, t)) = let val id = serial (); @@ -328,7 +306,7 @@ (fn (syms, pos) => parse_raw ctxt "sort" (syms, pos) |> report_result ctxt pos - |> sort_of_term + |> decode_sort |> Type.minimize_sort (Proof_Context.tsig_of ctxt) handle ERROR msg => parse_failed ctxt pos msg "sort"); @@ -337,7 +315,7 @@ (fn (syms, pos) => parse_raw ctxt "type" (syms, pos) |> report_result ctxt pos - |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t) + |> decode_typ handle ERROR msg => parse_failed ctxt pos msg "type"); fun parse_term is_prop ctxt = @@ -714,11 +692,31 @@ (** check/uncheck **) +fun prepare_types ctxt tys = + let + fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S); + val env = + (fold o fold_atyps) + (fn TFree (x, S) => constraint ((x, ~1), S) + | TVar v => constraint v + | _ => I) tys []; + val get_sort = Proof_Context.get_sort ctxt env; + in + (map o map_atyps) + (fn TFree (x, _) => TFree (x, get_sort (x, ~1)) + | TVar (xi, _) => TVar (xi, get_sort xi) + | T => T) tys + end; + fun check_typs ctxt = - Syntax.apply_typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt); + prepare_types ctxt #> + Syntax.apply_typ_check ctxt #> + Term_Sharing.typs (Proof_Context.theory_of ctxt); fun check_terms ctxt = - Syntax.apply_term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt); + Term.burrow_types (prepare_types ctxt) #> + Syntax.apply_term_check ctxt #> + Term_Sharing.terms (Proof_Context.theory_of ctxt); fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; diff -r 4548b8e1ba12 -r fca432074fb2 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Nov 09 17:12:26 2011 +0100 +++ b/src/Pure/sign.ML Wed Nov 09 17:57:42 2011 +0100 @@ -361,18 +361,18 @@ fun gen_syntax change_gram parse_typ mode args thy = let - val ctxt = Proof_Context.init_global thy; + val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy); fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx) handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c); in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end; fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x; -val add_modesyntax = gen_add_syntax Syntax.parse_typ; +val add_modesyntax = gen_add_syntax Syntax.read_typ; val add_modesyntax_i = gen_add_syntax (K I); val add_syntax = add_modesyntax Syntax.mode_default; val add_syntax_i = add_modesyntax_i Syntax.mode_default; -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ; +val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ; val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I); fun type_notation add mode args = @@ -396,9 +396,9 @@ local -fun gen_add_consts parse_typ ctxt raw_args thy = +fun gen_add_consts prep_typ ctxt raw_args thy = let - val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt; + val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt; fun prep (b, raw_T, mx) = let val c = full_name thy b; @@ -417,7 +417,8 @@ in fun add_consts args thy = - #2 (gen_add_consts Syntax.parse_typ (Proof_Context.init_global thy) args thy); + #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy); + fun add_consts_i args thy = #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);