src/Pure/sign.ML
changeset 3937 988ce6fbf85b
parent 3899 41a4abfa60fe
child 3956 d59fe4579004
     1.1 --- a/src/Pure/sign.ML	Mon Oct 20 10:51:01 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Oct 20 10:52:04 1997 +0200
     1.3 @@ -5,7 +5,10 @@
     1.4  The abstract type "sg" of signatures.
     1.5  *)
     1.6  
     1.7 -(*external forms*)
     1.8 +(*raw base names*)
     1.9 +type rstring = string;
    1.10 +type rclass = class;
    1.11 +(*external pruned forms*)
    1.12  type xstring = string;
    1.13  type xclass = class;
    1.14  type xsort = sort;
    1.15 @@ -37,20 +40,18 @@
    1.16    val classK: string
    1.17    val typeK: string
    1.18    val constK: string
    1.19 +  val full_name: sg -> rstring -> string
    1.20 +  val base_name: string -> rstring
    1.21    val intern: sg -> string -> xstring -> string
    1.22    val extern: sg -> string -> string -> xstring
    1.23 -  val full_name: sg -> xstring -> string
    1.24 +  val cond_extern: sg -> string -> string -> xstring
    1.25    val intern_class: sg -> xclass -> class
    1.26 -  val extern_class: sg -> class -> xclass
    1.27 -  val intern_sort: sg -> xsort -> sort
    1.28 -  val extern_sort: sg -> sort -> xsort
    1.29 -  val intern_typ: sg -> xtyp -> typ
    1.30 -  val extern_typ: sg -> typ -> xtyp
    1.31 -  val intern_term: sg -> xterm -> term
    1.32 -  val extern_term: sg -> term -> xterm
    1.33 -  val intern_tycons: sg -> xtyp -> typ
    1.34    val intern_tycon: sg -> xstring -> string
    1.35    val intern_const: sg -> xstring -> string
    1.36 +  val intern_sort: sg -> xsort -> sort
    1.37 +  val intern_typ: sg -> xtyp -> typ
    1.38 +  val intern_term: sg -> xterm -> term
    1.39 +  val intern_tycons: sg -> xtyp -> typ
    1.40    val print_sg: sg -> unit
    1.41    val pretty_sg: sg -> Pretty.T
    1.42    val pprint_sg: sg -> pprint_args -> unit
    1.43 @@ -71,23 +72,23 @@
    1.44    val infer_types: sg -> (indexname -> typ option) ->
    1.45      (indexname -> sort option) -> string list -> bool
    1.46      -> xterm list * typ -> int * term * (indexname * typ) list
    1.47 -  val add_classes: (xclass * xclass list) list -> sg -> sg
    1.48 -  val add_classes_i: (xclass * class list) list -> sg -> sg
    1.49 +  val add_classes: (rclass * xclass list) list -> sg -> sg
    1.50 +  val add_classes_i: (rclass * class list) list -> sg -> sg
    1.51    val add_classrel: (xclass * xclass) list -> sg -> sg
    1.52    val add_classrel_i: (class * class) list -> sg -> sg
    1.53    val add_defsort: xsort -> sg -> sg
    1.54    val add_defsort_i: sort -> sg -> sg
    1.55 -  val add_types: (xstring * int * mixfix) list -> sg -> sg
    1.56 -  val add_tyabbrs: (xstring * string list * string * mixfix) list -> sg -> sg
    1.57 -  val add_tyabbrs_i: (xstring * string list * typ * mixfix) list -> sg -> sg
    1.58 +  val add_types: (rstring * int * mixfix) list -> sg -> sg
    1.59 +  val add_tyabbrs: (rstring * string list * string * mixfix) list -> sg -> sg
    1.60 +  val add_tyabbrs_i: (rstring * string list * typ * mixfix) list -> sg -> sg
    1.61    val add_arities: (xstring * xsort list * xsort) list -> sg -> sg
    1.62    val add_arities_i: (string * sort list * sort) list -> sg -> sg
    1.63 -  val add_consts: (xstring * string * mixfix) list -> sg -> sg
    1.64 -  val add_consts_i: (xstring * typ * mixfix) list -> sg -> sg
    1.65 -  val add_syntax: (xstring * string * mixfix) list -> sg -> sg
    1.66 -  val add_syntax_i: (xstring * typ * mixfix) list -> sg -> sg
    1.67 -  val add_modesyntax: (string * bool) * (xstring * string * mixfix) list -> sg -> sg
    1.68 -  val add_modesyntax_i: (string * bool) * (xstring * typ * mixfix) list -> sg -> sg
    1.69 +  val add_consts: (rstring * string * mixfix) list -> sg -> sg
    1.70 +  val add_consts_i: (rstring * typ * mixfix) list -> sg -> sg
    1.71 +  val add_syntax: (rstring * string * mixfix) list -> sg -> sg
    1.72 +  val add_syntax_i: (rstring * typ * mixfix) list -> sg -> sg
    1.73 +  val add_modesyntax: (string * bool) * (rstring * string * mixfix) list -> sg -> sg
    1.74 +  val add_modesyntax_i: (string * bool) * (rstring * typ * mixfix) list -> sg -> sg
    1.75    val add_trfuns:
    1.76      (string * (ast list -> ast)) list *
    1.77      (string * (term list -> term)) list *
    1.78 @@ -222,7 +223,13 @@
    1.79    end;
    1.80  
    1.81  (*make full names*)
    1.82 -fun full path name = NameSpace.pack (path @ NameSpace.unpack name);
    1.83 +fun full path name =
    1.84 +  if NameSpace.qualified name then
    1.85 +    error ("Attempt to declare qualified name " ^ quote name)
    1.86 +  else NameSpace.pack (path @ [name]);
    1.87 +
    1.88 +(*base name*)
    1.89 +val base_name = NameSpace.base;
    1.90  
    1.91  
    1.92  (* intern / extern names *)
    1.93 @@ -286,11 +293,13 @@
    1.94  
    1.95    fun intrn_class spaces = intrn spaces classK;
    1.96    fun extrn_class spaces = extrn spaces classK;
    1.97 +
    1.98    val intrn_sort = map o intrn_class;
    1.99 -  val extrn_sort = map o extrn_class;
   1.100    val intrn_typ = trn_typ o intrn;
   1.101 +  val intrn_term = trn_term o intrn;
   1.102 +
   1.103 +  val extrn_sort = map o extrn_class;
   1.104    val extrn_typ = trn_typ o extrn;
   1.105 -  val intrn_term = trn_term o intrn;
   1.106    val extrn_term = trn_term o extrn;
   1.107  
   1.108    fun intrn_tycons spaces T =
   1.109 @@ -298,17 +307,16 @@
   1.110  
   1.111    val intern = intrn o spaces_of;
   1.112    val extern = extrn o spaces_of;
   1.113 +  fun cond_extern sg kind = if ! long_names then I else extern sg kind;
   1.114 +
   1.115    val intern_class = intrn_class o spaces_of;
   1.116 -  val extern_class = extrn_class o spaces_of;
   1.117    val intern_sort = intrn_sort o spaces_of;
   1.118 -  val extern_sort = extrn_sort o spaces_of;
   1.119    val intern_typ = intrn_typ o spaces_of;
   1.120 -  val extern_typ = extrn_typ o spaces_of;
   1.121    val intern_term = intrn_term o spaces_of;
   1.122 -  val extern_term = extrn_term o spaces_of;
   1.123  
   1.124    fun intern_tycon sg = intrn (spaces_of sg) typeK;
   1.125    fun intern_const sg = intrn (spaces_of sg) constK;
   1.126 +
   1.127    val intern_tycons = intrn_tycons o spaces_of;
   1.128  
   1.129    fun full_name (Sg {path, ...}) = full path;
   1.130 @@ -316,16 +324,61 @@
   1.131  
   1.132  
   1.133  
   1.134 +(** pretty printing of terms and types **)
   1.135 +
   1.136 +fun pretty_term (Sg {syn, spaces, stamps, ...}) t =
   1.137 +  Syntax.pretty_term syn
   1.138 +    ("CPure" mem_string (map ! stamps))
   1.139 +    (if ! long_names then t else extrn_term spaces t);
   1.140 +
   1.141 +fun pretty_typ (Sg {syn, spaces, ...}) T =
   1.142 +  Syntax.pretty_typ syn
   1.143 +    (if ! long_names then T else extrn_typ spaces T);
   1.144 +
   1.145 +fun pretty_sort (Sg {syn, spaces, ...}) S =
   1.146 +  Syntax.pretty_sort syn
   1.147 +    (if ! long_names then S else extrn_sort spaces S);
   1.148 +
   1.149 +fun pretty_classrel sg (c1, c2) = Pretty.block
   1.150 +  [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
   1.151 +
   1.152 +fun pretty_arity sg (t, Ss, S) =
   1.153 +  let
   1.154 +    val t' = cond_extern sg typeK t;
   1.155 +    val dom =
   1.156 +      if null Ss then []
   1.157 +      else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
   1.158 +  in
   1.159 +    Pretty.block
   1.160 +      ([Pretty.str (t' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S])
   1.161 +  end;
   1.162 +
   1.163 +fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
   1.164 +fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);
   1.165 +fun string_of_sort sg S = Pretty.string_of (pretty_sort sg S);
   1.166 +
   1.167 +fun str_of_sort sg S = Pretty.str_of (pretty_sort sg S);
   1.168 +fun str_of_classrel sg c1_c2 = Pretty.str_of (pretty_classrel sg c1_c2);
   1.169 +fun str_of_arity sg ar = Pretty.str_of (pretty_arity sg ar);
   1.170 +
   1.171 +fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   1.172 +fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   1.173 +
   1.174 +
   1.175 +
   1.176  (** print signature **)
   1.177  
   1.178  fun stamp_names stamps = rev (map ! stamps);
   1.179  
   1.180  fun print_sg sg =
   1.181    let
   1.182 -    val Sg {syn, ...} = sg;
   1.183 +    fun prt_cls c = pretty_sort sg [c];
   1.184 +    fun prt_sort S = pretty_sort sg S;
   1.185 +    fun prt_tycon t = Pretty.str (cond_extern sg typeK t);
   1.186 +    fun prt_arity t (c, Ss) = pretty_arity sg (t, Ss, [c]);
   1.187 +    fun prt_typ ty = Pretty.quote (pretty_typ sg ty);
   1.188 +    fun prt_const c = Pretty.quote (Pretty.str (cond_extern sg constK c));
   1.189  
   1.190 -    fun prt_typ ty = Pretty.quote (Syntax.pretty_typ syn ty);
   1.191 -    fun prt_cls c = Syntax.pretty_sort syn [c];
   1.192  
   1.193      fun pretty_space (kind, space) = Pretty.block (Pretty.breaks
   1.194        (map Pretty.str (kind ^ ":" :: map quote (NameSpace.dest space))));
   1.195 @@ -338,25 +391,19 @@
   1.196          Pretty.commas (map prt_cls cs));
   1.197  
   1.198      fun pretty_default S = Pretty.block
   1.199 -      [Pretty.str "default:", Pretty.brk 1, Syntax.pretty_sort syn S];
   1.200 +      [Pretty.str "default:", Pretty.brk 1, pretty_sort sg S];
   1.201  
   1.202 -    fun pretty_ty (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
   1.203 +    fun pretty_ty (t, n) = Pretty.block
   1.204 +      [prt_tycon t, Pretty.str (" " ^ string_of_int n)];
   1.205  
   1.206 -    fun pretty_abbr (ty, (vs, rhs)) = Pretty.block
   1.207 -      [prt_typ (Type (ty, map (fn v => TVar ((v, 0), [])) vs)),
   1.208 +    fun pretty_abbr (t, (vs, rhs)) = Pretty.block
   1.209 +      [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   1.210          Pretty.str " =", Pretty.brk 1, prt_typ rhs];
   1.211  
   1.212 -    fun pretty_arity ty (c, []) = Pretty.block
   1.213 -          [Pretty.str (ty ^ " ::"), Pretty.brk 1, prt_cls c]
   1.214 -      | pretty_arity ty (c, Ss) = Pretty.block
   1.215 -          [Pretty.str (ty ^ " ::"), Pretty.brk 1,
   1.216 -            Pretty.list "(" ")" (map (Syntax.pretty_sort syn) Ss),
   1.217 -            Pretty.brk 1, prt_cls c];
   1.218 -
   1.219 -    fun pretty_arities (ty, ars) = map (pretty_arity ty) ars;
   1.220 +    fun pretty_arities (t, ars) = map (prt_arity t) ars;
   1.221  
   1.222      fun pretty_const (c, ty) = Pretty.block
   1.223 -      [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty];
   1.224 +      [prt_const c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
   1.225  
   1.226      val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
   1.227      val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
   1.228 @@ -384,48 +431,6 @@
   1.229  
   1.230  
   1.231  
   1.232 -(** pretty printing of terms and types **)
   1.233 -
   1.234 -fun pretty_term (Sg {syn, spaces, stamps, ...}) t =
   1.235 -  Syntax.pretty_term syn
   1.236 -    ("CPure" mem_string (map ! stamps))
   1.237 -    (if ! long_names then t else extrn_term spaces t);
   1.238 -
   1.239 -fun pretty_typ (Sg {syn, spaces, ...}) T =
   1.240 -  Syntax.pretty_typ syn
   1.241 -    (if ! long_names then T else extrn_typ spaces T);
   1.242 -
   1.243 -fun pretty_sort (Sg {syn, spaces, ...}) S =
   1.244 -  Syntax.pretty_sort syn
   1.245 -    (if ! long_names then S else extrn_sort spaces S);
   1.246 -
   1.247 -fun pretty_classrel sg (c1, c2) = Pretty.block
   1.248 -  [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
   1.249 -
   1.250 -fun pretty_arity sg (t, Ss, S) =
   1.251 -  let
   1.252 -    val t' = if ! long_names then t else intern_tycon sg t;
   1.253 -    val dom =
   1.254 -      if null Ss then []
   1.255 -      else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
   1.256 -  in
   1.257 -    Pretty.block
   1.258 -      ([Pretty.str (t ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S])
   1.259 -  end;
   1.260 -
   1.261 -fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
   1.262 -fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);
   1.263 -fun string_of_sort sg S = Pretty.string_of (pretty_sort sg S);
   1.264 -
   1.265 -fun str_of_sort sg S = Pretty.str_of (pretty_sort sg S);
   1.266 -fun str_of_classrel sg c1_c2 = Pretty.str_of (pretty_classrel sg c1_c2);
   1.267 -fun str_of_arity sg ar = Pretty.str_of (pretty_arity sg ar);
   1.268 -
   1.269 -fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   1.270 -fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   1.271 -
   1.272 -
   1.273 -
   1.274  (** read types **)  (*exception ERROR*)
   1.275  
   1.276  fun err_in_type s =
   1.277 @@ -888,7 +893,7 @@
   1.278      ("prop", 0, NoSyn) ::
   1.279      ("itself", 1, NoSyn) ::
   1.280      Syntax.pure_types)
   1.281 -  |> add_classes_i [(NameSpace.base logicC, [])]
   1.282 +  |> add_classes_i [(logicC, [])]
   1.283    |> add_defsort_i logicS
   1.284    |> add_arities_i
   1.285     [("fun", [logicS, logicS], logicS),