src/Pure/sign.ML
author nipkow
Thu, 25 Nov 1993 19:09:43 +0100
changeset 155 f58571828c68
parent 143 f8152ca36cd5
child 169 1b2765146aab
permissions -rw-r--r--
changed some names and deleted *NORMALIZED*
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
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
     6
The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
     7
typs under a signature).
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    10
signature SIGN =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  structure Type: TYPE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  structure Symtab: SYMTAB
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  structure Syntax: SYNTAX
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    15
  sharing Symtab = Type.Symtab
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  type sg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  type cterm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  type ctyp
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val cfun: (term -> term) -> (cterm -> cterm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val cterm_of: sg -> term -> cterm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val ctyp_of: sg -> typ -> ctyp
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val extend: sg -> string ->
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    23
        (class * class list) list * class list *
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    24
        (string list * int) list *
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    25
        (string list * (sort list * class)) list *
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    26
        (string list * string)list * Syntax.sext option -> sg
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val merge: sg * sg -> sg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val pure: sg
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val read_cterm: sg -> string * typ -> cterm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val read_ctyp: sg -> string -> ctyp
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    32
                  -> (indexname -> typ option) * (indexname -> sort option)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    33
                  -> (string*string)list
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    34
                  -> (indexname*ctyp)list * (cterm*cterm)list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val read_typ: sg * (indexname -> sort option) -> string -> typ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  val rep_ctyp: ctyp -> {T: typ, sign: sg}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val rep_sg: sg -> {tsig: Type.type_sig,
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    39
                     const_tab: typ Symtab.table,
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    40
                     syn: Syntax.syntax,
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    41
                     stamps: string ref list}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val string_of_cterm: cterm -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val string_of_ctyp: ctyp -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  val pprint_cterm: cterm -> pprint_args -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val pprint_ctyp: ctyp -> pprint_args -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  val string_of_term: sg -> term -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  val string_of_typ: sg -> typ -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  val pprint_term: sg -> term -> pprint_args -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  val pprint_typ: sg -> typ -> pprint_args -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  val term_of: cterm -> term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  val typ_of: ctyp -> typ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  val pretty_term: sg -> term -> Syntax.Pretty.T
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    55
functor SignFun(structure Type: TYPE and Syntax: SYNTAX): SIGN =
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    56
struct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
structure Type = Type;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
structure Symtab = Type.Symtab;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
structure Syntax = Syntax;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
structure Pretty = Syntax.Pretty
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    63
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    64
(* Signatures of theories. *)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    65
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    66
datatype sg =
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    67
  Sg of {
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    68
    tsig: Type.type_sig,            (*order-sorted signature of types*)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    69
    const_tab: typ Symtab.table,    (*types of constants*)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    70
    syn: Syntax.syntax,             (*syntax for parsing and printing*)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
    71
    stamps: string ref list};       (*unique theory indentifier*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
fun rep_sg (Sg args) = args;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
(*Is constant present in table with more generic type?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    82
        Some U => Type.typ_instance(tsig,T,U) | _ => false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
(*Check a term for errors.  Are all constants and types valid in signature?
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  Does not check that term is well-typed!*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    87
fun term_errors (sign as Sg{tsig,const_tab,...}) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
let val showtyp = string_of_typ sign;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    fun terrs (Const (a,T), errs) =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    90
        if valid_const tsig const_tab (a,T)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    91
        then Type.type_errors (tsig,showtyp) (T,errs)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    92
        else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
      | terrs (Free (_,T), errs) = Type.type_errors (tsig,showtyp) (T,errs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
      | terrs (Var  ((a,i),T), errs) =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    95
        if  i>=0  then  Type.type_errors (tsig,showtyp) (T,errs)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    96
        else  ("Negative index for Var: " ^ a) :: errs
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
      | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    98
      | terrs (Abs (_,T,t), errs) =
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    99
            Type.type_errors(tsig,showtyp)(T,terrs(t,errs))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
      | terrs (f$t, errs) = terrs(f, terrs (t,errs))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
in  terrs  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
(** The Extend operation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
(*Reset TVar indices to zero, renaming to preserve distinctness*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   107
fun zero_tvar_indices tsig T =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
  let val inxSs = typ_tvars T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
      val nms' = variantlist(map (#1 o #1) inxSs,[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
      val tye = map (fn ((v,S),a) => (v, TVar((a,0),S))) (inxSs ~~ nms')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
  in typ_subst_TVars tye T end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   113
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
(*Check that all types mentioned in the list of declarations are valid.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
  If errors found then raise exception.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  Zero type var indices because type inference requires it.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun read_consts(tsig,syn) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
let val showtyp = Syntax.string_of_typ syn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    fun read [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
      | read((cs,s)::pairs) =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   122
        let val t = Syntax.read syn Syntax.typeT s handle ERROR =>
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   123
                    error("The error above occurred in type " ^ quote s);
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   124
            val S = Type.defaultS tsig;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   125
            val T = Type.varifyT(Syntax.typ_of_term (K S) t)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   126
            val T0 = zero_tvar_indices tsig T;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   127
        in (case Type.type_errors (tsig,showtyp) (T0,[]) of
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   128
                [] => (cs,T0) :: read pairs
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   129
            | errs => error (cat_lines
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   130
           (("Error in type of constants " ^ space_implode " " cs) :: errs)))
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   131
        end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
in read end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
(*Extend a signature: may add classes, types and constants.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
  Replaces syntax with "syn".
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
  The "ref" in stamps ensures that no two signatures are identical --
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   138
  it is impossible to forge a signature. *)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   139
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   140
fun extend (Sg {tsig, const_tab, syn, stamps}) signame
155
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   141
  (classes, default, types, arities, const_decs, osext) =
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   142
  let
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   143
    (* FIXME abbr *)
155
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   144
    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
   145
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   146
    (* FIXME expand_typ, check typ *)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   147
    val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig'));
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   148
155
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   149
    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 arities)));
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   150
    val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    val syn' =
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   152
      (case osext of
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   153
        Some sext => Syntax.extend syn read_ty (roots, xconsts, sext)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   154
      | None =>
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   155
          if null roots andalso null xconsts then syn
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   156
          else Syntax.extend syn read_ty (roots, xconsts, Syntax.empty_sext));
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   157
    val sconsts =
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   158
      (case osext of
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   159
        Some sext => Syntax.constants sext
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   160
      | None => []);
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   161
    val const_decs' = read_consts (tsig', syn') (sconsts @ const_decs);
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   162
  in
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   163
    Sg {
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   164
      tsig = tsig',
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   165
      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
   166
        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
   167
      syn = syn',
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   168
      stamps = ref signame :: stamps}
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   169
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
(* The empty signature *)
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   173
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   174
val sg0 = Sg {tsig = Type.tsig0,
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   175
  const_tab = Symtab.null, syn = Syntax.type_syn, stamps= []};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   177
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   178
(* The pure signature *)
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   179
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   180
val pure = extend sg0 "Pure"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
([("logic", [])],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
 ["logic"],
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   183
 [(["fun"], 2),
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   184
  (["prop"], 0),
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   185
  (Syntax.syntax_types, 0)],
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
 [(["fun"],  ([["logic"], ["logic"]], "logic")),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
  (["prop"], ([], "logic"))],
155
f58571828c68 changed some names and deleted *NORMALIZED*
nipkow
parents: 143
diff changeset
   188
 [([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   189
 Some Syntax.pure_sext);
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   190
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(** The Merge operation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
(*Update table with (a,x) providing any existing asgt to "a" equals x. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
fun update_eq ((a,x),tab) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
    case Symtab.lookup(tab,a) of
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   198
        None => Symtab.update((a,x), tab)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   199
      | Some y => if x=y then tab
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   200
            else  raise TERM ("Incompatible types for constant: "^a, []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(*Combine tables, updating tab2 by tab1 and checking.*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   203
fun merge_tabs (tab1,tab2) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
(*Combine tables, overwriting tab2 with tab1.*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   207
fun smash_tabs (tab1,tab2) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
    Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
(*Combine stamps, checking that theory names are disjoint. *)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   211
fun merge_stamps (stamps1,stamps2) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
  let val stamps = stamps1 union stamps2 in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
  case findrep (map ! stamps) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
     a::_ => error ("Attempt to merge different versions of theory: " ^ a)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
   | [] => stamps
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
fun merge (sign1 as Sg{tsig=tsig1,const_tab=ctab1,stamps=stamps1,syn=syn1},
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   220
           sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
    if stamps2 subset stamps1 then sign1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
    else if stamps1 subset stamps2 then sign2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
    else  (*neither is union already;  must form union*)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   224
           Sg{tsig= Type.merge(tsig1,tsig2),
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   225
              const_tab= merge_tabs (ctab1, ctab2),
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   226
              stamps= merge_stamps (stamps1,stamps2),
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   227
              syn = Syntax.merge(syn1,syn2)};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
(**** CERTIFIED TYPES ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
(*Certified typs under a signature*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
datatype ctyp = Ctyp of {sign: sg,  T: typ};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
fun rep_ctyp(Ctyp ctyp) = ctyp;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
fun typ_of (Ctyp{sign,T}) = T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
fun ctyp_of (sign as Sg{tsig,...}) T =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   241
        case Type.type_errors (tsig,string_of_typ sign) (T,[]) of
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   242
          [] => Ctyp{sign= sign,T= T}
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   243
        | errs =>  error (cat_lines ("Error in type:" :: errs));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
(*The only use is a horrible hack in the simplifier!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
fun read_typ(Sg{tsig,syn,...}, defS) s =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
    let val term = Syntax.read syn Syntax.typeT s;
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   248
        val S0 = Type.defaultS tsig;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   249
        fun defS0 s = case defS s of Some S => S | None => S0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
    in Syntax.typ_of_term defS0 term end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
(**** CERTIFIED TERMS ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
(*Certified terms under a signature, with checked typ and maxidx of Vars*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
datatype cterm = Cterm of {sign: sg,  t: term,  T: typ,  maxidx: int};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
fun rep_cterm (Cterm args) = args;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
(*Return the underlying term*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
fun term_of (Cterm{sign,t,T,maxidx}) = t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
(** pretty printing of terms **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
(*Create a cterm by checking a "raw" term with respect to a signature*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
fun cterm_of sign t =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
  case  term_errors sign (t,[])  of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
(*Lexing, parsing, polymorphic typechecking of a term.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   291
                   (a,T) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
  let val showtyp = string_of_typ sign
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
      and showterm = string_of_term sign
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
      fun termerr [] = ""
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   295
        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   296
        | termerr ts = "\nInvolving these terms:\n" ^
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   297
                       cat_lines (map showterm ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
      val t = Syntax.read syn T a;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
      val (t',tye) = Type.infer_types (tsig, const_tab, types,
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   300
                                       sorts, showtyp, T, t)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   301
                  handle TYPE (msg, Ts, ts) =>
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   302
          error ("Type checking error: " ^ msg ^ "\n" ^
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   303
                  cat_lines (map showtyp Ts) ^ termerr ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
  in (cterm_of sign t', tye)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
  handle TERM (msg, _) => error ("Error: " ^  msg);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
(** reading of instantiations **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   314
        | _ => error("Lexical error in variable name " ^ quote (implode cs));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
fun absent ixn =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
fun inst_failure ixn =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
let fun split([],tvs,vs) = (tvs,vs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
      | split((sv,st)::l,tvs,vs) = (case explode sv of
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   325
                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   326
                | cs => split(l,tvs,(indexname cs,st)::vs));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
    val (tvs,vs) = split(insts,[],[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
    fun readT((a,i),st) =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   329
        let val ixn = ("'" ^ a,i);
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   330
            val S = case rsorts ixn of Some S => S | None => absent ixn;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   331
            val T = read_typ (sign,sorts) st;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   332
        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   333
           else inst_failure ixn
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   334
        end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
    val tye = map readT tvs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
    fun add_cterm ((cts,tye), (ixn,st)) =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   337
        let val T = case rtypes ixn of
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   338
                      Some T => typ_subst_TVars tye T
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   339
                    | None => absent ixn;
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   340
            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   341
            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
   342
        in ((cv,ct)::cts,tye2 @ tye) end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
    val (cterms,tye') = foldl add_cterm (([],tye), vs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
end;
143
f8152ca36cd5 Sign.extend: Syntax.extend now called with read_ty;
wenzelm
parents: 19
diff changeset
   347