added syntax for _type_constraint_;
authorwenzelm
Fri May 05 21:59:45 2006 +0200 (2006-05-05)
changeset 19577fdb3642feb49
parent 19576 179ad0076f75
child 19578 f93b7637a5e6
added syntax for _type_constraint_;
src/Pure/Syntax/syn_trans.ML
src/Pure/pure_thy.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri May 05 21:59:44 2006 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri May 05 21:59:45 2006 +0200
     1.3 @@ -371,6 +371,13 @@
     1.4    | type_tr' _ _ _ = raise Match;
     1.5  
     1.6  
     1.7 +(* type constraints *)
     1.8 +
     1.9 +fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
    1.10 +      Term.list_comb (Lexicon.const SynExt.constrainC $ t $ TypeExt.term_of_typ show_sorts T, ts)
    1.11 +  | type_constraint_tr' _ _ _ = raise Match;
    1.12 +
    1.13 +
    1.14  (* dependent / nondependent quantifiers *)
    1.15  
    1.16  fun variant_abs' (x, T, B) =
    1.17 @@ -444,7 +451,8 @@
    1.18     ("_index", index_ast_tr')]);
    1.19  
    1.20  val pure_trfunsT =
    1.21 -  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
    1.22 +  [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr'),
    1.23 +   ("_type_constraint_", type_constraint_tr')];
    1.24  
    1.25  fun struct_trfuns structs =
    1.26    ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
     2.1 --- a/src/Pure/pure_thy.ML	Fri May 05 21:59:44 2006 +0200
     2.2 +++ b/src/Pure/pure_thy.ML	Fri May 05 21:59:45 2006 +0200
     2.3 @@ -569,6 +569,7 @@
     2.4      ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
     2.5      ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
     2.6      ("_idtypdummy", "type => idt",        Mixfix ("'_()\\<Colon>_", [], 0)),
     2.7 +    ("_type_constraint_", "'a",           NoSyn),
     2.8      ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     2.9      ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
    2.10      ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
     3.1 --- a/src/Pure/type_infer.ML	Fri May 05 21:59:44 2006 +0200
     3.2 +++ b/src/Pure/type_infer.ML	Fri May 05 21:59:45 2006 +0200
     3.3 @@ -173,7 +173,8 @@
     3.4            (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
     3.5        | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
     3.6        | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
     3.7 -      | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
     3.8 +      | pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) =
     3.9 +          constrain (pre_of (ps, t)) T
    3.10        | pre_of (ps, Bound i) = (ps, PBound i)
    3.11        | pre_of (ps, Abs (x, T, t)) =
    3.12            let
    3.13 @@ -431,7 +432,7 @@
    3.14  
    3.15  fun constrain t T =
    3.16    if T = dummyT then t
    3.17 -  else Const ("_type_constraint_", T) $ t;
    3.18 +  else Const ("_type_constraint_", T --> T) $ t;
    3.19  
    3.20  
    3.21  (* user parameters *)