# HG changeset patch # User wenzelm # Date 1349269136 -7200 # Node ID 4341e4d86872a8b4e97cd04373831c1fea25feb9 # Parent 1cf810b8f6004317f518dd67d08ee0c7003bb0c4 allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables; diff -r 1cf810b8f600 -r 4341e4d86872 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Oct 02 09:20:28 2012 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Oct 03 14:58:56 2012 +0200 @@ -623,13 +623,17 @@ val tsig = tsig_of ctxt; val defaultS = Type.defaultS tsig; - fun constraint (xi, S) env = - if S = dummyS orelse Term_Position.is_positionS S then env - else - Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env - handle Vartab.DUP _ => - error ("Inconsistent sort constraints for type variable " ^ - quote (Term.string_of_vname' xi)); + fun constraint (xi, raw_S) env = + let val (ps, S) = Term_Position.decode_positionS raw_S in + if S = dummyS then env + else + Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env + handle Vartab.DUP _ => + error ("Inconsistent sort constraints for type variable " ^ + quote (Term.string_of_vname' xi) ^ + space_implode " " (map Position.here ps)) + end; + val env = (fold o fold_atyps) (fn TFree (x, S) => constraint ((x, ~1), S) @@ -648,14 +652,13 @@ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^ " for type variable " ^ quote (Term.string_of_vname' xi))); - fun add_report raw_S S reports = - (case Term_Position.decode_positionS raw_S of - SOME pos => - if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then - (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S)) - :: reports - else reports - | NONE => reports); + fun add_report S pos reports = + if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then + (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S)) + :: reports + else reports; + + val decode_pos = #1 o Term_Position.decode_positionS; val reports = (fold o fold_atyps) @@ -663,8 +666,8 @@ if Term_Position.is_positionT T then I else (case T of - TFree (x, raw_S) => add_report raw_S (get_sort (x, ~1)) - | TVar (xi, raw_S) => add_report raw_S (get_sort xi) + TFree (x, raw_S) => fold (add_report (get_sort (x, ~1))) (decode_pos raw_S) + | TVar (xi, raw_S) => fold (add_report (get_sort xi)) (decode_pos raw_S) | _ => I)) tys []; in (implode (map #2 reports), get_sort) end; diff -r 1cf810b8f600 -r 4341e4d86872 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 02 09:20:28 2012 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Oct 03 14:58:56 2012 +0200 @@ -86,7 +86,6 @@ fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]); fun class s = Lexicon.unmark_class s handle Fail _ => err (); - fun class_pos s = if is_some (Term_Position.decode s) then s else err (); fun classes (Const (s, _)) = [class s] | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs @@ -95,37 +94,44 @@ fun sort (Const ("_topsort", _)) = [] | sort (Const ("_sort", _) $ cs) = classes cs | sort (Const (s, _)) = [class s] - | sort (Free (s, _)) = [class_pos s] | sort _ = err (); in sort tm end; (* decode_typ *) +fun decode_pos (Free (s, _)) = + if is_some (Term_Position.decode s) then SOME s else NONE + | decode_pos _ = NONE; + fun decode_typ tm = let fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]); - 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 args) end; - in typ tm end; + fun typ ps sort tm = + (case tm of + Const ("_tfree", _) $ t => typ ps sort t + | Const ("_tvar", _) $ t => typ ps sort t + | Const ("_ofsort", _) $ t $ s => + (case decode_pos s of + SOME p => typ (p :: ps) sort t + | NONE => + if is_none sort then typ ps (SOME (decode_sort s)) t + else err ()) + | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s) + | Free (x, _) => TFree (x, ps @ the_default dummyS sort) + | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort) + | _ => + if null ps andalso is_none sort then + let + val (head, args) = Term.strip_comb tm; + val a = + (case head of + Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ()) + | _ => err ()); + in Type (a, map (typ [] NONE) args) end + else err ()); + in typ [] NONE tm end; (* parsetree_to_ast *) diff -r 1cf810b8f600 -r 4341e4d86872 src/Pure/Syntax/term_position.ML --- a/src/Pure/Syntax/term_position.ML Tue Oct 02 09:20:28 2012 +0200 +++ b/src/Pure/Syntax/term_position.ML Wed Oct 03 14:58:56 2012 +0200 @@ -11,10 +11,9 @@ val decode: string -> Position.T option val decode_position: term -> (Position.T * typ) option val decode_positionT: typ -> Position.T option - val decode_positionS: sort -> Position.T option + val decode_positionS: sort -> Position.T list * sort val is_position: term -> bool val is_positionT: typ -> bool - val is_positionS: sort -> bool val strip_positions: term -> term end; @@ -52,12 +51,12 @@ fun decode_positionT (TFree (x, _)) = decode x | decode_positionT _ = NONE; -fun decode_positionS [x] = decode x - | decode_positionS _ = NONE; +fun decode_positionS cs = + let val (ps, sort) = List.partition (is_some o decode) cs + in (map (the o decode) ps, sort) end; val is_position = is_some o decode_position; val is_positionT = is_some o decode_positionT; -val is_positionS = is_some o decode_positionS; fun strip_positions ((t as Const (c, _)) $ u $ v) = if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v diff -r 1cf810b8f600 -r 4341e4d86872 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Oct 02 09:20:28 2012 +0200 +++ b/src/Pure/pure_thy.ML Wed Oct 03 14:58:56 2012 +0200 @@ -75,8 +75,8 @@ ("", typ "type_name => type", Delimfix "_"), ("_type_name", typ "id => type_name", Delimfix "_"), ("_type_name", typ "longid => type_name", Delimfix "_"), - ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [1000, 0], 1000)), - ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [1000, 0], 1000)), + ("_ofsort", typ "tid_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)), + ("_ofsort", typ "tvar_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)), ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], 1000)), ("", typ "class_name => sort", Delimfix "_"), ("_class_name", typ "id => class_name", Delimfix "_"), @@ -160,7 +160,7 @@ #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), + ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\_", [4, 0], 3)), ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), diff -r 1cf810b8f600 -r 4341e4d86872 src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Oct 02 09:20:28 2012 +0200 +++ b/src/Pure/variable.ML Wed Oct 03 14:58:56 2012 +0200 @@ -213,9 +213,9 @@ (* constraints *) -fun constrain_tvar (xi, S) = - if S = dummyS orelse Term_Position.is_positionS S - then Vartab.delete_safe xi else Vartab.update (xi, S); +fun constrain_tvar (xi, raw_S) = + let val (_, S) = Term_Position.decode_positionS raw_S + in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; fun declare_constraints t = map_constraints (fn (types, sorts) => let