Sign.extend: Syntax.extend now called with read_ty;
authorwenzelm
Thu Nov 25 11:37:51 1993 +0100 (1993-11-25)
changeset 143f8152ca36cd5
parent 142 6dfae8cddec7
child 144 0a0da273a6c5
Sign.extend: Syntax.extend now called with read_ty;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Nov 25 10:44:44 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 25 11:37:51 1993 +0100
     1.3 @@ -3,8 +3,8 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1992  University of Cambridge
     1.6  
     1.7 -  the abstract types "sg" (signatures)
     1.8 -  and "cterm" (certified terms under a signature)
     1.9 +The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
    1.10 +typs under a signature).
    1.11  *)
    1.12  
    1.13  signature SIGN =
    1.14 @@ -12,7 +12,7 @@
    1.15    structure Type: TYPE
    1.16    structure Symtab: SYMTAB
    1.17    structure Syntax: SYNTAX
    1.18 -  sharing Symtab=Type.Symtab
    1.19 +  sharing Symtab = Type.Symtab
    1.20    type sg
    1.21    type cterm
    1.22    type ctyp
    1.23 @@ -52,20 +52,23 @@
    1.24    val pretty_term: sg -> term -> Syntax.Pretty.T
    1.25  end;
    1.26  
    1.27 +functor SignFun(structure Type: TYPE and Syntax: SYNTAX): SIGN =
    1.28 +struct
    1.29  
    1.30 -functor SignFun (structure Type:TYPE and Syntax:SYNTAX) : SIGN =
    1.31 -struct
    1.32  structure Type = Type;
    1.33  structure Symtab = Type.Symtab;
    1.34  structure Syntax = Syntax;
    1.35  structure Pretty = Syntax.Pretty
    1.36  
    1.37 -(*Signatures of theories. *)
    1.38 +
    1.39 +(* Signatures of theories. *)
    1.40 +
    1.41  datatype sg =
    1.42 -  Sg of {tsig: Type.type_sig,           (* order-sorted signature of types *)
    1.43 -         const_tab: typ Symtab.table,   (*types of constants*)
    1.44 -         syn: Syntax.syntax,            (*Parsing and printing operations*)
    1.45 -         stamps: string ref list        (*unique theory indentifier*)  };
    1.46 +  Sg of {
    1.47 +    tsig: Type.type_sig,            (*order-sorted signature of types*)
    1.48 +    const_tab: typ Symtab.table,    (*types of constants*)
    1.49 +    syn: Syntax.syntax,             (*syntax for parsing and printing*)
    1.50 +    stamps: string ref list};       (*unique theory indentifier*)
    1.51  
    1.52  
    1.53  fun rep_sg (Sg args) = args;
    1.54 @@ -100,7 +103,6 @@
    1.55  
    1.56  (** The Extend operation **)
    1.57  
    1.58 -
    1.59  (*Reset TVar indices to zero, renaming to preserve distinctness*)
    1.60  fun zero_tvar_indices tsig T =
    1.61    let val inxSs = typ_tvars T;
    1.62 @@ -108,6 +110,7 @@
    1.63        val tye = map (fn ((v,S),a) => (v, TVar((a,0),S))) (inxSs ~~ nms')
    1.64    in typ_subst_TVars tye T end
    1.65  
    1.66 +
    1.67  (*Check that all types mentioned in the list of declarations are valid.
    1.68    If errors found then raise exception.
    1.69    Zero type var indices because type inference requires it.
    1.70 @@ -132,48 +135,60 @@
    1.71  (*Extend a signature: may add classes, types and constants.
    1.72    Replaces syntax with "syn".
    1.73    The "ref" in stamps ensures that no two signatures are identical --
    1.74 -  it is impossible to forge a signature.  *)
    1.75 -fun extend (Sg{tsig, const_tab, syn, stamps, ...}) signame
    1.76 -           (newclasses, newdefault, otypes, newtypes, const_decs, osext) : sg =
    1.77 -let val tsig' = Type.extend(tsig,newclasses,newdefault,otypes,newtypes);
    1.78 -    val S = Type.defaultS tsig';
    1.79 -    val roots = filter (Type.logical_type tsig')
    1.80 -                       (distinct(flat(map #1 newtypes)))
    1.81 +  it is impossible to forge a signature. *)
    1.82 +
    1.83 +fun extend (Sg {tsig, const_tab, syn, stamps}) signame
    1.84 +  (newclasses, newdefault, otypes, newtypes, const_decs, osext) =
    1.85 +  let
    1.86 +    (* FIXME abbr *)
    1.87 +    val tsig' = Type.extend (tsig, newclasses, newdefault, otypes, newtypes);
    1.88 +
    1.89 +    (* FIXME expand_typ, check typ *)
    1.90 +    val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig'));
    1.91 +
    1.92 +    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 newtypes)));
    1.93      val xconsts = map #1 newclasses @ flat (map #1 otypes) @ flat (map #1 const_decs);
    1.94      val syn' =
    1.95 -      case osext of
    1.96 -        Some sext => Syntax.extend (syn, K S) (roots, xconsts, sext)
    1.97 -      | None => if null roots andalso null xconsts then syn
    1.98 -                else Syntax.extend (syn, K S) (roots, xconsts, Syntax.empty_sext);
    1.99 -    val sconsts = case osext of
   1.100 -                    Some(sext) => Syntax.constants sext
   1.101 -                  | None => [];
   1.102 -    val const_decs' = read_consts(tsig',syn') (sconsts @ const_decs)
   1.103 -in Sg{tsig= tsig',
   1.104 -      const_tab= Symtab.st_of_declist (const_decs', const_tab)
   1.105 -                 handle Symtab.DUPLICATE(a) =>
   1.106 -                 error("Constant " ^ quote a ^ " declared twice"),
   1.107 -      syn=syn', stamps= ref signame :: stamps}
   1.108 -end;
   1.109 +      (case osext of
   1.110 +        Some sext => Syntax.extend syn read_ty (roots, xconsts, sext)
   1.111 +      | None =>
   1.112 +          if null roots andalso null xconsts then syn
   1.113 +          else Syntax.extend syn read_ty (roots, xconsts, Syntax.empty_sext));
   1.114 +    val sconsts =
   1.115 +      (case osext of
   1.116 +        Some sext => Syntax.constants sext
   1.117 +      | None => []);
   1.118 +    val const_decs' = read_consts (tsig', syn') (sconsts @ const_decs);
   1.119 +  in
   1.120 +    Sg {
   1.121 +      tsig = tsig',
   1.122 +      const_tab = Symtab.st_of_declist (const_decs', const_tab)
   1.123 +        handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   1.124 +      syn = syn',
   1.125 +      stamps = ref signame :: stamps}
   1.126 +  end;
   1.127  
   1.128  
   1.129  (* The empty signature *)
   1.130 -val sg0 = Sg{tsig= Type.tsig0, const_tab= Symtab.null,
   1.131 -             syn=Syntax.type_syn,  stamps= []};
   1.132 +
   1.133 +val sg0 = Sg {tsig = Type.tsig0,
   1.134 +  const_tab = Symtab.null, syn = Syntax.type_syn, stamps= []};
   1.135  
   1.136 -(*The pure signature*)
   1.137 -val pure : sg = extend sg0 "Pure"
   1.138 +
   1.139 +(* The pure signature *)
   1.140 +
   1.141 +val pure = extend sg0 "Pure"
   1.142  ([("logic", [])],
   1.143   ["logic"],
   1.144 - [(["fun"],2),
   1.145 -  (["prop"],0),
   1.146 -  (Syntax.syntax_types,0)],
   1.147 + [(["fun"], 2),
   1.148 +  (["prop"], 0),
   1.149 +  (Syntax.syntax_types, 0)],
   1.150   [(["fun"],  ([["logic"], ["logic"]], "logic")),
   1.151    (["prop"], ([], "logic"))],
   1.152   [(["*NORMALIZED*"], "'a::{} => 'a"),
   1.153 -  ([Syntax.constrainC], "'a::logic => 'a")],
   1.154 - Some(Syntax.pure_sext)
   1.155 -);
   1.156 +  ([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
   1.157 + Some Syntax.pure_sext);
   1.158 +
   1.159  
   1.160  
   1.161  (** The Merge operation **)
   1.162 @@ -330,3 +345,4 @@
   1.163  in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   1.164  
   1.165  end;
   1.166 +