src/Pure/sign.ML
changeset 3810 350150bd3744
parent 3805 a50d0b5219dd
child 3850 305e5adfd7c8
     1.1 --- a/src/Pure/sign.ML	Thu Oct 09 14:39:44 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Oct 09 14:50:39 1997 +0200
     1.3 @@ -33,6 +33,12 @@
     1.4    val norm_sort: sg -> sort -> sort
     1.5    val nonempty_sort: sg -> sort list -> sort -> bool
     1.6    val long_names: bool ref
     1.7 +  val classK: string
     1.8 +  val typeK: string
     1.9 +  val constK: string
    1.10 +  val intern: sg -> string -> xstring -> string
    1.11 +  val extern: sg -> string -> string -> xstring
    1.12 +  val full_name: sg -> xstring -> string
    1.13    val intern_class: sg -> xclass -> class
    1.14    val extern_class: sg -> class -> xclass
    1.15    val intern_sort: sg -> xsort -> sort
    1.16 @@ -90,7 +96,7 @@
    1.17    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    1.18    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    1.19    val add_path: string -> sg -> sg
    1.20 -  val add_space: string * xstring list -> sg -> sg
    1.21 +  val add_space: string * string list -> sg -> sg
    1.22    val add_name: string -> sg -> sg
    1.23    val make_draft: sg -> sg
    1.24    val merge: sg * sg -> sg
    1.25 @@ -205,7 +211,8 @@
    1.26      overwrite (spaces, (kind, space'))
    1.27    end;
    1.28  
    1.29 -fun full_name path name = NameSpace.pack (path @ (NameSpace.unpack name));
    1.30 +(*make full names*)
    1.31 +fun full path name = NameSpace.pack (path @ NameSpace.unpack name);
    1.32  
    1.33  
    1.34  (* intern / extern names *)
    1.35 @@ -279,6 +286,8 @@
    1.36    fun intrn_tycons spaces T =
    1.37      map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;
    1.38  
    1.39 +  val intern = intrn o spaces_of;
    1.40 +  val extern = intrn o spaces_of;
    1.41    val intern_class = intrn_class o spaces_of;
    1.42    val extern_class = extrn_class o spaces_of;
    1.43    val intern_sort = intrn_sort o spaces_of;
    1.44 @@ -292,6 +301,7 @@
    1.45    fun intern_const sg = intrn (spaces_of sg) constK;
    1.46    val intern_tycons = intrn_tycons o spaces_of;
    1.47  
    1.48 +  fun full_name (Sg {path, ...}) = full path;
    1.49  end;
    1.50  
    1.51  
    1.52 @@ -339,12 +349,13 @@
    1.53        [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty];
    1.54  
    1.55      val Sg {tsig, const_tab, syn = _, path, spaces, stamps} = sg;
    1.56 +    val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
    1.57      val {classes, classrel, default, tycons, abbrs, arities} =
    1.58        Type.rep_tsig tsig;
    1.59    in
    1.60      Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
    1.61      Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
    1.62 -    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces));
    1.63 +    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
    1.64      Pretty.writeln (pretty_classes classes);
    1.65      Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
    1.66      Pretty.writeln (pretty_default default);
    1.67 @@ -496,9 +507,10 @@
    1.68  fun infer_types sg def_type def_sort used freeze (ts, T) =
    1.69    let
    1.70      val Sg {tsig, ...} = sg;
    1.71 -    val prt = setmp Syntax.show_brackets true
    1.72 -      (fn _ => setmp long_names true pretty_term sg) ();
    1.73 -    val prT = pretty_typ sg;
    1.74 +    val prt =
    1.75 +      setmp Syntax.show_brackets true
    1.76 +        (setmp long_names true (pretty_term sg));
    1.77 +    val prT = setmp long_names true (pretty_typ sg);
    1.78      val infer = Type.infer_types prt prT tsig (const_type sg) def_type def_sort
    1.79        (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze;
    1.80  
    1.81 @@ -546,7 +558,7 @@
    1.82  (** signature extension functions **)  (*exception ERROR*)
    1.83  
    1.84  fun decls_of path name_of mfixs =
    1.85 -  map (fn (x, y, mx) => (full_name path (name_of x mx), y)) mfixs;
    1.86 +  map (fn (x, y, mx) => (full path (name_of x mx), y)) mfixs;
    1.87  
    1.88  fun no_read _ _ _ decl = decl;
    1.89  
    1.90 @@ -581,7 +593,7 @@
    1.91  
    1.92      val abbrs' =
    1.93        map (fn (t, vs, rhs, mx) =>
    1.94 -        (full_name path (Syntax.type_name t mx), vs, rhs)) abbrs;
    1.95 +        (full path (Syntax.type_name t mx), vs, rhs)) abbrs;
    1.96      val spaces' = add_names spaces typeK (map #1 abbrs');
    1.97      val decls = map (rd_abbr syn' tsig spaces') abbrs';
    1.98    in
    1.99 @@ -609,7 +621,7 @@
   1.100  (* add term constants and syntax *)
   1.101  
   1.102  fun const_name path c mx =
   1.103 -  full_name path (Syntax.const_name c mx);
   1.104 +  full path (Syntax.const_name c mx);
   1.105  
   1.106  fun err_in_const c =
   1.107    error ("in declaration of constant " ^ quote c);
   1.108 @@ -667,7 +679,7 @@
   1.109      val consts =
   1.110        map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   1.111  
   1.112 -    val full_names = map (full_name path) names;
   1.113 +    val full_names = map (full path) names;
   1.114      val spaces' = add_names spaces classK full_names;
   1.115      val intrn = if int then map (intrn_class spaces') else I;
   1.116      val classes' =
   1.117 @@ -833,14 +845,14 @@
   1.118    |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
   1.119    |> add_trfuns Syntax.pure_trfuns
   1.120    |> add_trfunsT Syntax.pure_trfunsT
   1.121 +  |> add_syntax
   1.122 +   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   1.123    |> add_consts
   1.124     [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   1.125      ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   1.126      ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   1.127      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   1.128      ("TYPE", "'a itself", NoSyn)]
   1.129 -  |> add_syntax
   1.130 -   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   1.131    |> add_name "ProtoPure";
   1.132  
   1.133  val pure = proto_pure