src/Pure/sign.ML
changeset 3995 88fc1015d241
parent 3975 ddeb5a0fd08d
child 4007 1d6aed7ff375
     1.1 --- a/src/Pure/sign.ML	Fri Oct 24 17:15:59 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Oct 24 17:17:10 1997 +0200
     1.3 @@ -109,17 +109,15 @@
     1.4    val add_path: string -> sg -> sg
     1.5    val add_space: string * string list -> sg -> sg
     1.6    val add_name: string -> sg -> sg
     1.7 -  val init_data: string * exn * (exn -> exn) * (exn * exn -> exn) *
     1.8 -    (string -> exn -> unit) -> sg -> sg
     1.9 +  val init_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
    1.10 +    -> sg -> sg
    1.11    val get_data: sg -> string -> exn
    1.12    val put_data: string * exn -> sg -> sg
    1.13    val print_data: sg -> string -> unit
    1.14    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.15    val prep_ext: sg -> sg
    1.16    val merge: sg * sg -> sg
    1.17 -  val proto_pure: sg
    1.18 -  val pure: sg
    1.19 -  val cpure: sg
    1.20 +  val pre_pure: sg
    1.21    val const_of_class: class -> string
    1.22    val class_of_const: string -> class
    1.23  end;
    1.24 @@ -160,9 +158,7 @@
    1.25  val str_of_sg = Pretty.str_of o pretty_sg;
    1.26  val pprint_sg = Pretty.pprint o pretty_sg;
    1.27  
    1.28 -
    1.29  val tsig_of = #tsig o rep_sg;
    1.30 -val self_ref = #self o rep_sg;
    1.31  val get_data = Data.get o #data o rep_sg;
    1.32  val print_data = Data.print o #data o rep_sg;
    1.33  
    1.34 @@ -174,10 +170,7 @@
    1.35  val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.36  
    1.37  
    1.38 -(* signature id *)
    1.39 -
    1.40 -fun deref (SgRef (Some (ref sg))) = sg
    1.41 -  | deref (SgRef None) = sys_error "Sign.deref";
    1.42 +(* id and self *)
    1.43  
    1.44  fun check_stale (sg as Sg ({id, ...},
    1.45          {self = SgRef (Some (ref (Sg ({id = id', ...}, _)))), ...})) =
    1.46 @@ -185,6 +178,11 @@
    1.47        else raise TERM ("Stale signature: " ^ str_of_sg sg, [])
    1.48    | check_stale _ = sys_error "Sign.check_stale";
    1.49  
    1.50 +fun self_ref (sg as Sg (_, {self, ...})) = (check_stale sg; self);
    1.51 +
    1.52 +fun deref (SgRef (Some (ref sg))) = sg
    1.53 +  | deref (SgRef None) = sys_error "Sign.deref";
    1.54 +
    1.55  fun name_of (sg as Sg ({id = ref name, ...}, _)) =
    1.56    if name = "" orelse name = "#" then
    1.57      raise TERM ("Nameless signature " ^ str_of_sg sg, [])
    1.58 @@ -285,8 +283,8 @@
    1.59    if_none (assoc (spaces, kind)) NameSpace.empty;
    1.60  
    1.61  (*input and output of qualified names*)
    1.62 -fun intrn spaces kind = NameSpace.lookup (space_of spaces kind);
    1.63 -fun extrn spaces kind = NameSpace.prune (space_of spaces kind);
    1.64 +fun intrn spaces kind = NameSpace.intern (space_of spaces kind);
    1.65 +fun extrn spaces kind = NameSpace.extern (space_of spaces kind);
    1.66  
    1.67  (*add names*)
    1.68  fun add_names spaces kind names =
    1.69 @@ -831,7 +829,7 @@
    1.70  
    1.71  (* signature data *)
    1.72  
    1.73 -fun ext_init_data (syn, tsig, ctab, names, data) (kind, e, ext, mrg, prt) =
    1.74 +fun ext_init_data (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
    1.75    (syn, tsig, ctab, names, Data.init data kind e ext mrg prt);
    1.76  
    1.77  fun ext_put_data (syn, tsig, ctab, names, data) (kind, e) =
    1.78 @@ -938,46 +936,14 @@
    1.79  
    1.80  
    1.81  
    1.82 -(** the Pure signature **)
    1.83 +(** partial Pure signature **)
    1.84  
    1.85  val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
    1.86    Symtab.null, Syntax.pure_syn, [], [], Data.empty, []);
    1.87  
    1.88 -val proto_pure =
    1.89 +val pre_pure =
    1.90    create_sign (SgRef (Some (ref dummy_sg))) [] "#"
    1.91 -    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty)
    1.92 -  |> add_types
    1.93 -   (("fun", 2, NoSyn) ::
    1.94 -    ("prop", 0, NoSyn) ::
    1.95 -    ("itself", 1, NoSyn) ::
    1.96 -    Syntax.pure_types)
    1.97 -  |> add_classes_i [(logicC, [])]
    1.98 -  |> add_defsort_i logicS
    1.99 -  |> add_arities_i
   1.100 -   [("fun", [logicS, logicS], logicS),
   1.101 -    ("prop", [], logicS),
   1.102 -    ("itself", [logicS], logicS)]
   1.103 -  |> add_syntax Syntax.pure_syntax
   1.104 -  |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
   1.105 -  |> add_trfuns Syntax.pure_trfuns
   1.106 -  |> add_trfunsT Syntax.pure_trfunsT
   1.107 -  |> add_syntax
   1.108 -   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   1.109 -  |> add_consts
   1.110 -   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   1.111 -    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   1.112 -    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   1.113 -    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   1.114 -    ("TYPE", "'a itself", NoSyn)]
   1.115 -  |> add_name "ProtoPure";
   1.116 -
   1.117 -val pure = proto_pure
   1.118 -  |> add_syntax Syntax.pure_appl_syntax
   1.119 -  |> add_name "Pure";
   1.120 -
   1.121 -val cpure = proto_pure
   1.122 -  |> add_syntax Syntax.pure_applC_syntax
   1.123 -  |> add_name "CPure";
   1.124 +    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty);
   1.125  
   1.126  
   1.127  end;