src/Pure/sign.ML
author lcp
Tue, 18 Jan 1994 15:57:40 +0100
changeset 230 ec8a2b6aa8a7
parent 229 4002c4cd450c
child 251 c9b984c0a674
permissions -rw-r--r--
Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/sign.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
     4
    Copyright   1994  University of Cambridge
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
     6
The abstract types "sg" of signatures
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
     9
signature SIGN =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  structure Type: TYPE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  structure Symtab: SYMTAB
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  structure Syntax: SYNTAX
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    14
  sharing Symtab = Type.Symtab
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  type sg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val extend: sg -> string ->
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    17
        (class * class list) list * class list *
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    18
        (string list * int) list *
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
    19
        (string * indexname list * string) list *
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    20
        (string list * (sort list * class)) list *
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    21
        (string list * string)list * Syntax.sext option -> sg
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val merge: sg * sg -> sg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val pure: sg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val read_typ: sg * (indexname -> sort option) -> string -> typ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val rep_sg: sg -> {tsig: Type.type_sig,
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    26
                     const_tab: typ Symtab.table,
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    27
                     syn: Syntax.syntax,
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    28
                     stamps: string ref list}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val string_of_term: sg -> term -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val string_of_typ: sg -> typ -> string
206
0d624d1ba9cc added subsig: sg * sg -> bool to test if one signature is contained in another.
nipkow
parents: 200
diff changeset
    31
  val subsig: sg * sg -> bool
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val pprint_term: sg -> term -> pprint_args -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val pprint_typ: sg -> typ -> pprint_args -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val pretty_term: sg -> term -> Syntax.Pretty.T
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    35
  val term_errors: sg -> term -> string list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
    38
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    39
struct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
structure Type = Type;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
structure Symtab = Type.Symtab;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
structure Syntax = Syntax;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
structure Pretty = Syntax.Pretty
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    46
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    47
(* Signatures of theories. *)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    48
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    49
datatype sg =
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    50
  Sg of {
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    51
    tsig: Type.type_sig,            (*order-sorted signature of types*)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    52
    const_tab: typ Symtab.table,    (*types of constants*)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    53
    syn: Syntax.syntax,             (*syntax for parsing and printing*)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    54
    stamps: string ref list};       (*unique theory indentifier*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
fun rep_sg (Sg args) = args;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
206
0d624d1ba9cc added subsig: sg * sg -> bool to test if one signature is contained in another.
nipkow
parents: 200
diff changeset
    59
fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
0d624d1ba9cc added subsig: sg * sg -> bool to test if one signature is contained in another.
nipkow
parents: 200
diff changeset
    60
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(*Is constant present in table with more generic type?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    67
        Some U => Type.typ_instance(tsig,T,U) | _ => false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(*Check a term for errors.  Are all constants and types valid in signature?
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  Does not check that term is well-typed!*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    72
fun term_errors (sign as Sg{tsig,const_tab,...}) =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    73
  let val showtyp = string_of_typ sign
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    74
      fun terrs (Const (a,T), errs) =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    75
	  if valid_const tsig const_tab (a,T)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    76
	  then Type.type_errors tsig (T,errs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    77
	  else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    78
	| terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    79
	| terrs (Var  ((a,i),T), errs) =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    80
	  if  i>=0  then  Type.type_errors tsig (T,errs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    81
	  else  ("Negative index for Var: " ^ a) :: errs
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    82
	| terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    83
	| terrs (Abs (_,T,t), errs) =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    84
	      Type.type_errors tsig (T,terrs(t,errs))
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    85
	| terrs (f$t, errs) = terrs(f, terrs (t,errs))
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 224
diff changeset
    86
  in  fn t => terrs(t,[])  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    89
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(** The Extend operation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    92
(* Extend a signature: may add classes, types and constants. The "ref" in
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    93
   stamps ensures that no two signatures are identical -- it is impossible to
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    94
   forge a signature. *)
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    95
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    96
fun extend (Sg {tsig, const_tab, syn, stamps}) name
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
    97
  (classes, default, types, abbr, arities, const_decs, opt_sext) =
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    98
  let
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
    99
    fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   100
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   101
    fun read_typ tsg sy s =
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   102
      Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   103
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   104
    fun check_typ tsg sy ty =
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   105
      (case Type.type_errors tsg (ty, []) of
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   106
        [] => ty
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   107
      | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   108
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   109
    (*reset TVar indices to zero, renaming to preserve distinctness*)
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   110
    fun zero_tvar_indices T =
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   111
      let
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   112
        val inxSs = typ_tvars T;
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   113
        val nms' = variantlist (map (#1 o #1) inxSs, []);
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   114
        val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   115
      in typ_subst_TVars tye T end;
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   116
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   117
    (*read and check the type mentioned in a const declaration; zero type var
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   118
      indices because type inference requires it*)
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   119
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   120
    fun read_consts tsg sy (cs, s) =
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   121
      let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   122
      in
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   123
        (case Type.type_errors tsg (ty, []) of
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   124
          [] => (cs, ty)
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   125
        | errs => error (cat_lines (("Error in type of constants " ^
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   126
            space_implode " " (map quote cs)) :: errs)))
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   127
      end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
155
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   129
    val tsig' = Type.extend (tsig, classes, default, types, arities);
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   130
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   131
    fun read_typ_abbr(a,v,s)=
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   132
      let val T = Type.varifyT(read_typ tsig' syn s)
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   133
      in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   134
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   135
    val abbr' = map read_typ_abbr abbr;
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   136
    val tsig'' = Type.add_abbrs(tsig',abbr');
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   137
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   138
    val read_ty =
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   139
      (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   140
    val log_types = Type.logical_types tsig'';
155
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   141
    val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   142
    val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   143
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   144
    val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   145
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   146
    val const_decs' =
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   147
      map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   148
  in
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   149
    Sg {
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   150
      tsig = tsig'',
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   151
      const_tab = Symtab.st_of_declist (const_decs', const_tab)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   152
        handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   153
      syn = syn',
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   154
      stamps = ref name :: stamps}
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   155
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(* The empty signature *)
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   159
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   160
val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   161
  syn = Syntax.type_syn, stamps = []};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   163
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   164
(* The pure signature *)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   165
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   166
val pure = extend sg0 "Pure"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
([("logic", [])],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
 ["logic"],
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   169
 [(["fun"], 2),
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   170
  (["prop"], 0),
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   171
  (Syntax.syntax_types, 0)],
200
39a931cc6558 Necessary changes to accomodate type abbreviations.
nipkow
parents: 197
diff changeset
   172
 [],
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
 [(["fun"],  ([["logic"], ["logic"]], "logic")),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
  (["prop"], ([], "logic"))],
171
ab0f93a291b5 *** empty log message ***
wenzelm
parents: 169
diff changeset
   175
 [([Syntax.constrainC], "'a::logic => 'a")],
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   176
 Some Syntax.pure_sext);
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   177
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
(** The Merge operation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
(*Update table with (a,x) providing any existing asgt to "a" equals x. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
fun update_eq ((a,x),tab) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
    case Symtab.lookup(tab,a) of
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   185
        None => Symtab.update((a,x), tab)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   186
      | Some y => if x=y then tab
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   187
            else  raise TERM ("Incompatible types for constant: "^a, []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
(*Combine tables, updating tab2 by tab1 and checking.*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   190
fun merge_tabs (tab1,tab2) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
    Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(*Combine tables, overwriting tab2 with tab1.*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   194
fun smash_tabs (tab1,tab2) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
    Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
(*Combine stamps, checking that theory names are disjoint. *)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   198
fun merge_stamps (stamps1,stamps2) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
  let val stamps = stamps1 union stamps2 in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
  case findrep (map ! stamps) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
     a::_ => error ("Attempt to merge different versions of theory: " ^ a)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
   | [] => stamps
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
(*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   206
fun merge
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   207
  (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   208
   sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
    if stamps2 subset stamps1 then sign1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
    else if stamps1 subset stamps2 then sign2
169
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   211
    else (*neither is union already; must form union*)
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   212
      let val tsig = Type.merge (tsig1, tsig2);
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   213
      in
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   214
        Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   215
          stamps = merge_stamps (stamps1, stamps2),
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   216
          syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   217
      end;
1b2765146aab extend: cleaned up, adapted for new Syntax.extend;
wenzelm
parents: 155
diff changeset
   218
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
fun read_typ(Sg{tsig,syn,...}, defS) s =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
    let val term = Syntax.read syn Syntax.typeT s;
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   223
        val S0 = Type.defaultS tsig;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   224
        fun defS0 s = case defS s of Some S => S | None => S0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
    in Syntax.typ_of_term defS0 term end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
(** pretty printing of terms **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
end;
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   236