src/Pure/sign.ML
changeset 35429 afa8cf9e63d8
parent 35412 b8dead547d9e
child 35669 a91c7ed801b8
     1.1 --- a/src/Pure/sign.ML	Wed Mar 03 00:00:44 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Mar 03 00:28:22 2010 +0100
     1.3 @@ -56,10 +56,7 @@
     1.4    val intern_sort: theory -> sort -> sort
     1.5    val extern_sort: theory -> sort -> sort
     1.6    val intern_typ: theory -> typ -> typ
     1.7 -  val extern_typ: theory -> typ -> typ
     1.8    val intern_term: theory -> term -> term
     1.9 -  val extern_term: theory -> term -> term
    1.10 -  val intern_tycons: theory -> typ -> typ
    1.11    val the_type_decl: theory -> string -> Type.decl
    1.12    val arity_number: theory -> string -> int
    1.13    val arity_sorts: theory -> string -> sort -> sort list
    1.14 @@ -157,7 +154,7 @@
    1.15      make_sign (Name_Space.default_naming, syn, tsig, consts);
    1.16  
    1.17    val empty =
    1.18 -    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
    1.19 +    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
    1.20  
    1.21    fun merge pp (sign1, sign2) =
    1.22      let
    1.23 @@ -266,41 +263,10 @@
    1.24    | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.25    | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.26  
    1.27 -val add_classesT = Term.fold_atyps
    1.28 -  (fn TFree (_, S) => fold (insert (op =)) S
    1.29 -    | TVar (_, S) => fold (insert (op =)) S
    1.30 -    | _ => I);
    1.31 -
    1.32 -fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
    1.33 -  | add_tyconsT _ = I;
    1.34 -
    1.35 -val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
    1.36 -
    1.37 -fun mapping add_names f t =
    1.38 -  let
    1.39 -    fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
    1.40 -    val tab = map_filter f' (add_names t []);
    1.41 -    fun get x = the_default x (AList.lookup (op =) tab x);
    1.42 -  in get end;
    1.43 -
    1.44 -fun typ_mapping f g thy T =
    1.45 -  T |> map_typ
    1.46 -    (mapping add_classesT (f thy) T)
    1.47 -    (mapping add_tyconsT (g thy) T);
    1.48 -
    1.49 -fun term_mapping f g h thy t =
    1.50 -  t |> map_term
    1.51 -    (mapping (Term.fold_types add_classesT) (f thy) t)
    1.52 -    (mapping (Term.fold_types add_tyconsT) (g thy) t)
    1.53 -    (mapping add_consts (h thy) t);
    1.54 -
    1.55  in
    1.56  
    1.57 -val intern_typ = typ_mapping intern_class intern_type;
    1.58 -val extern_typ = typ_mapping extern_class extern_type;
    1.59 -val intern_term = term_mapping intern_class intern_type intern_const;
    1.60 -val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
    1.61 -val intern_tycons = typ_mapping (K I) intern_type;
    1.62 +fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
    1.63 +fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
    1.64  
    1.65  end;
    1.66  
    1.67 @@ -424,6 +390,27 @@
    1.68  val cert_arity = prep_arity (K I) certify_sort;
    1.69  
    1.70  
    1.71 +(* type syntax entities *)
    1.72 +
    1.73 +local
    1.74 +
    1.75 +fun read_type thy text =
    1.76 +  let
    1.77 +    val (syms, pos) = Syntax.read_token text;
    1.78 +    val c = intern_type thy (Symbol_Pos.content syms);
    1.79 +    val _ = the_type_decl thy c;
    1.80 +    val _ = Position.report (Markup.tycon c) pos;
    1.81 +  in c end;
    1.82 +
    1.83 +in
    1.84 +
    1.85 +val _ = Context.>>
    1.86 +  (Context.map_theory
    1.87 +    (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
    1.88 +
    1.89 +end;
    1.90 +
    1.91 +
    1.92  
    1.93  (** signature extension functions **)  (*exception ERROR/TYPE*)
    1.94  
    1.95 @@ -438,11 +425,13 @@
    1.96  
    1.97  (* add type constructors *)
    1.98  
    1.99 +val type_syntax = Syntax.mark_type oo full_name;
   1.100 +
   1.101  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.102    let
   1.103      val syn' =
   1.104        Syntax.update_type_gram true Syntax.mode_default
   1.105 -        (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
   1.106 +        (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
   1.107      val decls = map (fn (a, n, _) => (a, n)) types;
   1.108      val tsig' = fold (Type.add_type naming) decls tsig;
   1.109    in (naming, syn', tsig', consts) end);
   1.110 @@ -452,9 +441,8 @@
   1.111  
   1.112  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.113    let
   1.114 -    val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
   1.115      val tsig' = fold (Type.add_nonterminal naming) ns tsig;
   1.116 -  in (naming, syn', tsig', consts) end);
   1.117 +  in (naming, syn, tsig', consts) end);
   1.118  
   1.119  
   1.120  (* add type abbreviations *)
   1.121 @@ -465,7 +453,7 @@
   1.122        val ctxt = ProofContext.init thy;
   1.123        val syn' =
   1.124          Syntax.update_type_gram true Syntax.mode_default
   1.125 -          [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
   1.126 +          [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
   1.127        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
   1.128          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   1.129        val tsig' = Type.add_abbrev naming abbr tsig;
   1.130 @@ -495,8 +483,8 @@
   1.131  
   1.132  fun type_notation add mode args =
   1.133    let
   1.134 -    fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
   1.135 -          SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
   1.136 +    fun type_syntax (Type (c, args), mx) =
   1.137 +          SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
   1.138        | type_syntax _ = NONE;
   1.139    in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
   1.140  
   1.141 @@ -579,9 +567,8 @@
   1.142  fun primitive_class (bclass, classes) thy =
   1.143    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.144      let
   1.145 -      val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
   1.146        val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
   1.147 -    in (naming, syn', tsig', consts) end)
   1.148 +    in (naming, syn, tsig', consts) end)
   1.149    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   1.150  
   1.151  fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);