allow position constraints to coexist with 0 or 1 sort constraints;
authorwenzelm
Wed Oct 03 14:58:56 2012 +0200 (2012-10-03)
changeset 496854341e4d86872
parent 49684 1cf810b8f600
child 49686 678aa92e921c
allow position constraints to coexist with 0 or 1 sort constraints;
more position information in sorting error;
report sorting of all type variables;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/term_position.ML
src/Pure/pure_thy.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 02 09:20:28 2012 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Oct 03 14:58:56 2012 +0200
     1.3 @@ -623,13 +623,17 @@
     1.4      val tsig = tsig_of ctxt;
     1.5      val defaultS = Type.defaultS tsig;
     1.6  
     1.7 -    fun constraint (xi, S) env =
     1.8 -      if S = dummyS orelse Term_Position.is_positionS S then env
     1.9 -      else
    1.10 -        Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
    1.11 -          handle Vartab.DUP _ =>
    1.12 -            error ("Inconsistent sort constraints for type variable " ^
    1.13 -              quote (Term.string_of_vname' xi));
    1.14 +    fun constraint (xi, raw_S) env =
    1.15 +      let val (ps, S) = Term_Position.decode_positionS raw_S in
    1.16 +        if S = dummyS then env
    1.17 +        else
    1.18 +          Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
    1.19 +            handle Vartab.DUP _ =>
    1.20 +              error ("Inconsistent sort constraints for type variable " ^
    1.21 +                quote (Term.string_of_vname' xi) ^
    1.22 +                space_implode " " (map Position.here ps))
    1.23 +      end;
    1.24 +
    1.25      val env =
    1.26        (fold o fold_atyps)
    1.27          (fn TFree (x, S) => constraint ((x, ~1), S)
    1.28 @@ -648,14 +652,13 @@
    1.29                " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
    1.30                " for type variable " ^ quote (Term.string_of_vname' xi)));
    1.31  
    1.32 -    fun add_report raw_S S reports =
    1.33 -      (case Term_Position.decode_positionS raw_S of
    1.34 -        SOME pos =>
    1.35 -          if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
    1.36 -            (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
    1.37 -              :: reports
    1.38 -          else reports
    1.39 -      | NONE => reports);
    1.40 +    fun add_report S pos reports =
    1.41 +      if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
    1.42 +        (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
    1.43 +          :: reports
    1.44 +      else reports;
    1.45 +
    1.46 +    val decode_pos = #1 o Term_Position.decode_positionS;
    1.47  
    1.48      val reports =
    1.49        (fold o fold_atyps)
    1.50 @@ -663,8 +666,8 @@
    1.51            if Term_Position.is_positionT T then I
    1.52            else
    1.53              (case T of
    1.54 -              TFree (x, raw_S) => add_report raw_S (get_sort (x, ~1))
    1.55 -            | TVar (xi, raw_S) => add_report raw_S (get_sort xi)
    1.56 +              TFree (x, raw_S) => fold (add_report (get_sort (x, ~1))) (decode_pos raw_S)
    1.57 +            | TVar (xi, raw_S) => fold (add_report (get_sort xi)) (decode_pos raw_S)
    1.58              | _ => I)) tys [];
    1.59  
    1.60    in (implode (map #2 reports), get_sort) end;
     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Oct 02 09:20:28 2012 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Oct 03 14:58:56 2012 +0200
     2.3 @@ -86,7 +86,6 @@
     2.4      fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
     2.5  
     2.6      fun class s = Lexicon.unmark_class s handle Fail _ => err ();
     2.7 -    fun class_pos s = if is_some (Term_Position.decode s) then s else err ();
     2.8  
     2.9      fun classes (Const (s, _)) = [class s]
    2.10        | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
    2.11 @@ -95,37 +94,44 @@
    2.12      fun sort (Const ("_topsort", _)) = []
    2.13        | sort (Const ("_sort", _) $ cs) = classes cs
    2.14        | sort (Const (s, _)) = [class s]
    2.15 -      | sort (Free (s, _)) = [class_pos s]
    2.16        | sort _ = err ();
    2.17    in sort tm end;
    2.18  
    2.19  
    2.20  (* decode_typ *)
    2.21  
    2.22 +fun decode_pos (Free (s, _)) =
    2.23 +      if is_some (Term_Position.decode s) then SOME s else NONE
    2.24 +  | decode_pos _ = NONE;
    2.25 +
    2.26  fun decode_typ tm =
    2.27    let
    2.28      fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
    2.29  
    2.30 -    fun typ (Free (x, _)) = TFree (x, dummyS)
    2.31 -      | typ (Var (xi, _)) = TVar (xi, dummyS)
    2.32 -      | typ (Const ("_tfree",_) $ (t as Free _)) = typ t
    2.33 -      | typ (Const ("_tvar",_) $ (t as Var _)) = typ t
    2.34 -      | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s)
    2.35 -      | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) =
    2.36 -          TFree (x, decode_sort s)
    2.37 -      | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s)
    2.38 -      | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) =
    2.39 -          TVar (xi, decode_sort s)
    2.40 -      | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s)
    2.41 -      | typ t =
    2.42 -          let
    2.43 -            val (head, args) = Term.strip_comb t;
    2.44 -            val a =
    2.45 -              (case head of
    2.46 -                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
    2.47 -              | _ => err ());
    2.48 -          in Type (a, map typ args) end;
    2.49 -  in typ tm end;
    2.50 +    fun typ ps sort tm =
    2.51 +      (case tm of
    2.52 +        Const ("_tfree", _) $ t => typ ps sort t
    2.53 +      | Const ("_tvar", _) $ t => typ ps sort t
    2.54 +      | Const ("_ofsort", _) $ t $ s =>
    2.55 +          (case decode_pos s of
    2.56 +            SOME p => typ (p :: ps) sort t
    2.57 +          | NONE =>
    2.58 +              if is_none sort then typ ps (SOME (decode_sort s)) t
    2.59 +              else err ())
    2.60 +      | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s)
    2.61 +      | Free (x, _) => TFree (x, ps @ the_default dummyS sort)
    2.62 +      | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort)
    2.63 +      | _ =>
    2.64 +          if null ps andalso is_none sort then
    2.65 +            let
    2.66 +              val (head, args) = Term.strip_comb tm;
    2.67 +              val a =
    2.68 +                (case head of
    2.69 +                  Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
    2.70 +                | _ => err ());
    2.71 +            in Type (a, map (typ [] NONE) args) end
    2.72 +          else err ());
    2.73 +  in typ [] NONE tm end;
    2.74  
    2.75  
    2.76  (* parsetree_to_ast *)
     3.1 --- a/src/Pure/Syntax/term_position.ML	Tue Oct 02 09:20:28 2012 +0200
     3.2 +++ b/src/Pure/Syntax/term_position.ML	Wed Oct 03 14:58:56 2012 +0200
     3.3 @@ -11,10 +11,9 @@
     3.4    val decode: string -> Position.T option
     3.5    val decode_position: term -> (Position.T * typ) option
     3.6    val decode_positionT: typ -> Position.T option
     3.7 -  val decode_positionS: sort -> Position.T option
     3.8 +  val decode_positionS: sort -> Position.T list * sort
     3.9    val is_position: term -> bool
    3.10    val is_positionT: typ -> bool
    3.11 -  val is_positionS: sort -> bool
    3.12    val strip_positions: term -> term
    3.13  end;
    3.14  
    3.15 @@ -52,12 +51,12 @@
    3.16  fun decode_positionT (TFree (x, _)) = decode x
    3.17    | decode_positionT _ = NONE;
    3.18  
    3.19 -fun decode_positionS [x] = decode x
    3.20 -  | decode_positionS _ = NONE;
    3.21 +fun decode_positionS cs =
    3.22 +  let val (ps, sort) = List.partition (is_some o decode) cs
    3.23 +  in (map (the o decode) ps, sort) end;
    3.24  
    3.25  val is_position = is_some o decode_position;
    3.26  val is_positionT = is_some o decode_positionT;
    3.27 -val is_positionS = is_some o decode_positionS;
    3.28  
    3.29  fun strip_positions ((t as Const (c, _)) $ u $ v) =
    3.30        if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
     4.1 --- a/src/Pure/pure_thy.ML	Tue Oct 02 09:20:28 2012 +0200
     4.2 +++ b/src/Pure/pure_thy.ML	Wed Oct 03 14:58:56 2012 +0200
     4.3 @@ -75,8 +75,8 @@
     4.4      ("",            typ "type_name => type",           Delimfix "_"),
     4.5      ("_type_name",  typ "id => type_name",             Delimfix "_"),
     4.6      ("_type_name",  typ "longid => type_name",         Delimfix "_"),
     4.7 -    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [1000, 0], 1000)),
     4.8 -    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [1000, 0], 1000)),
     4.9 +    ("_ofsort",     typ "tid_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
    4.10 +    ("_ofsort",     typ "tvar_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
    4.11      ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], 1000)),
    4.12      ("",            typ "class_name => sort",          Delimfix "_"),
    4.13      ("_class_name", typ "id => class_name",            Delimfix "_"),
    4.14 @@ -160,7 +160,7 @@
    4.15    #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    4.16     [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    4.17      ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    4.18 -    ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    4.19 +    ("_ofsort",           typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    4.20      ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    4.21      ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    4.22      ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
     5.1 --- a/src/Pure/variable.ML	Tue Oct 02 09:20:28 2012 +0200
     5.2 +++ b/src/Pure/variable.ML	Wed Oct 03 14:58:56 2012 +0200
     5.3 @@ -213,9 +213,9 @@
     5.4  
     5.5  (* constraints *)
     5.6  
     5.7 -fun constrain_tvar (xi, S) =
     5.8 -  if S = dummyS orelse Term_Position.is_positionS S
     5.9 -  then Vartab.delete_safe xi else Vartab.update (xi, S);
    5.10 +fun constrain_tvar (xi, raw_S) =
    5.11 +  let val (_, S) = Term_Position.decode_positionS raw_S
    5.12 +  in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
    5.13  
    5.14  fun declare_constraints t = map_constraints (fn (types, sorts) =>
    5.15    let