src/Pure/sign.ML
changeset 14905 5f3fc2f62071
parent 14856 669a9a0e7279
child 14974 b1ecb7859c99
     1.1 --- a/src/Pure/sign.ML	Wed Jun 09 18:54:43 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Jun 09 18:55:07 2004 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val stamp_names_of: sg -> string list
     1.5    val exists_stamp: string -> sg -> bool
     1.6    val tsig_of: sg -> Type.tsig
     1.7 +  val is_logtype: sg -> string -> bool
     1.8    val deref: sg_ref -> sg
     1.9    val self_ref: sg -> sg_ref
    1.10    val subsig: sg * sg -> bool
    1.11 @@ -108,7 +109,7 @@
    1.12    val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
    1.13      (indexname -> sort option) -> string list -> bool
    1.14      -> (xterm list * typ) list -> term list * (indexname * typ) list
    1.15 -  val read_def_terms': Pretty.pp -> Syntax.syntax ->
    1.16 +  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
    1.17      sg * (indexname -> typ option) * (indexname -> sort option) ->
    1.18      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.19    val read_def_terms:
    1.20 @@ -230,6 +231,7 @@
    1.21  val pprint_sg = Pretty.pprint o pretty_sg;
    1.22  
    1.23  val tsig_of = #tsig o rep_sg;
    1.24 +fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
    1.25  fun const_type (Sg (_, {consts, ...})) c = apsome #1 (Symtab.lookup (consts, c));
    1.26  
    1.27  
    1.28 @@ -865,16 +867,16 @@
    1.29  (** read_def_terms **)
    1.30  
    1.31  (*read terms, infer types*)
    1.32 -fun read_def_terms' pp syn (sign, types, sorts) used freeze sTs =
    1.33 +fun read_def_terms' pp is_logtype syn (sign, types, sorts) used freeze sTs =
    1.34    let
    1.35      fun read (s, T) =
    1.36        let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg
    1.37 -      in (Syntax.read syn T' s, T') end;
    1.38 +      in (Syntax.read is_logtype syn T' s, T') end;
    1.39      val tsTs = map read sTs;
    1.40    in infer_types_simult pp sign types sorts used freeze tsTs end;
    1.41  
    1.42  fun read_def_terms (sign, types, sorts) =
    1.43 -  read_def_terms' (pp sign) (syn_of sign) (sign, types, sorts);
    1.44 +  read_def_terms' (pp sign) (is_logtype sign) (syn_of sign) (sign, types, sorts);
    1.45  
    1.46  fun simple_read_term sign T s =
    1.47    (read_def_terms (sign, K None, K None) [] true [(s, T)]
    1.48 @@ -904,15 +906,12 @@
    1.49  
    1.50  (* add type constructors *)
    1.51  
    1.52 -fun ext_types _ (syn, tsig, ctab, (path, spaces), data) types =
    1.53 +fun ext_types sg (syn, tsig, ctab, (path, spaces), data) types =
    1.54    let
    1.55      val decls = decls_of path Syntax.type_name types;
    1.56 +    val syn' = map_syntax (Syntax.extend_type_gram types) syn;
    1.57      val tsig' = Type.add_types decls tsig;
    1.58 -    val log_types = Type.logical_types tsig';
    1.59 -  in
    1.60 -    (map_syntax (Syntax.extend_log_types log_types o Syntax.extend_type_gram types) syn,
    1.61 -      tsig', ctab, (path, add_names spaces typeK (map fst decls)), data)
    1.62 -  end;
    1.63 +  in (syn', tsig', ctab, (path, add_names spaces typeK (map fst decls)), data) end;
    1.64  
    1.65  
    1.66  (* add type abbreviations *)
    1.67 @@ -924,16 +923,14 @@
    1.68  fun ext_abbrs rd_abbr sg (syn, tsig, ctab, (path, spaces), data) abbrs =
    1.69    let
    1.70      fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
    1.71 -    val syn' = map_syntax (Syntax.extend_type_gram (map mfix_of abbrs)) syn;
    1.72 +    val syn' = syn |> map_syntax (Syntax.extend_type_gram (map mfix_of abbrs));
    1.73  
    1.74      val abbrs' =
    1.75        map (fn (t, vs, rhs, mx) =>
    1.76          (full path (Syntax.type_name t mx), vs, rhs)) abbrs;
    1.77      val spaces' = add_names spaces typeK (map #1 abbrs');
    1.78      val decls = map (rd_abbr sg syn' tsig spaces') abbrs';
    1.79 -  in
    1.80 -    (syn', Type.add_abbrs decls tsig, ctab, (path, spaces'), data)
    1.81 -  end;
    1.82 +  in (syn', Type.add_abbrs decls tsig, ctab, (path, spaces'), data) end;
    1.83  
    1.84  fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
    1.85  fun ext_tyabbrs_i abbrs = ext_abbrs no_read abbrs;
    1.86 @@ -992,16 +989,16 @@
    1.87        if syn_only then []
    1.88        else decls_of path Syntax.const_name consts;
    1.89    in
    1.90 -    (map_syntax (Syntax.extend_const_gram prmode consts) syn, tsig,
    1.91 +    (map_syntax (Syntax.extend_const_gram (is_logtype sg) prmode consts) syn, tsig,
    1.92        Symtab.extend (ctab, map (fn (c, T) => (c, (T, stamp ()))) decls)
    1.93          handle Symtab.DUPS cs => err_dup_consts cs,
    1.94        (path, add_names spaces constK (map fst decls)), data)
    1.95    end;
    1.96  
    1.97 -fun ext_consts_i x = ext_cnsts no_read false ("", true) x;
    1.98 -fun ext_consts x = ext_cnsts read_const false ("", true) x;
    1.99 -fun ext_syntax_i x = ext_cnsts no_read true ("", true) x;
   1.100 -fun ext_syntax x = ext_cnsts read_const true ("", true) x;
   1.101 +fun ext_consts_i x = ext_cnsts no_read false Syntax.default_mode x;
   1.102 +fun ext_consts x = ext_cnsts read_const false Syntax.default_mode x;
   1.103 +fun ext_syntax_i x = ext_cnsts no_read true Syntax.default_mode x;
   1.104 +fun ext_syntax x = ext_cnsts read_const true Syntax.default_mode x;
   1.105  fun ext_modesyntax_i x y (prmode, consts) = ext_cnsts no_read true prmode x y consts;
   1.106  fun ext_modesyntax x y (prmode, consts) = ext_cnsts read_const true prmode x y consts;
   1.107  
   1.108 @@ -1071,7 +1068,7 @@
   1.109  (* add translation rules *)
   1.110  
   1.111  fun ext_trrules sg (syn, tsig, ctab, (path, spaces), data) args =
   1.112 -  (syn |> map_syntax (Syntax.extend_trrules (make_syntax sg syn)
   1.113 +  (syn |> map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn)
   1.114        (map (Syntax.map_trrule (fn (root, str) => (intrn spaces typeK root, str))) args)),
   1.115      tsig, ctab, (path, spaces), data);
   1.116  
   1.117 @@ -1212,14 +1209,9 @@
   1.118            {self = _, tsig = tsig2, consts = consts2,
   1.119              path = _, spaces = spaces2, data = data2}) = sg2;
   1.120  
   1.121 -      val id = ref "";
   1.122 -      val self_ref = ref dummy_sg;
   1.123 -      val self = SgRef (Some self_ref);
   1.124 -
   1.125        val stamps = merge_stamps stamps1 stamps2;
   1.126        val syntax = Syntax.merge_syntaxes syntax1 syntax2;
   1.127        val trfuns = merge_trfuns trfuns1 trfuns2;
   1.128 -      val tsig = Type.merge_tsigs (pp sg1) (tsig1, tsig2);   (* FIXME improve pp *)
   1.129        val consts = Symtab.merge eq_snd (consts1, consts2)
   1.130          handle Symtab.DUPS cs => err_dup_consts cs;
   1.131  
   1.132 @@ -1232,7 +1224,13 @@
   1.133  
   1.134        val data = merge_data (data1, data2);
   1.135  
   1.136 -      val sign = make_sign (id, self, tsig, consts, Syn (syntax, trfuns),
   1.137 +      val pre_sign = make_sign (ref "", SgRef (Some (ref dummy_sg)),
   1.138 +        tsig1, consts, Syn (syntax, trfuns), path, spaces, data, ref "#" :: stamps1);
   1.139 +      val tsig = Type.merge_tsigs (pp pre_sign) (tsig1, tsig2);
   1.140 +
   1.141 +      val self_ref = ref dummy_sg;
   1.142 +      val self = SgRef (Some self_ref);
   1.143 +      val sign = make_sign (ref "", self, tsig, consts, Syn (syntax, trfuns),
   1.144          path, spaces, data, stamps);
   1.145      in self_ref := sign; syn_of sign; sign end;
   1.146