allow position constraints to coexist with 0 or 1 sort constraints;
more position information in sorting error;
report sorting of all type variables;
--- 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;
--- 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 *)
--- 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
--- 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 ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
+ ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
--- 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