added pretty_sg;
authorwenzelm
Fri Aug 19 15:40:44 1994 +0200 (1994-08-19)
changeset 562e9572d03b724
parent 561 95225e63ef02
child 563 e9bf62651beb
added pretty_sg;
added infer_types;
removed subclasses arg of add_classes;
removed old 'extend' and related stuff;
various minor internal changes;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Aug 19 15:40:10 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Aug 19 15:40:44 1994 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  The abstract type "sg" of signatures.
     1.5  
     1.6  TODO:
     1.7 +  clean
     1.8    pure sign: elim Syntax.constrainC
     1.9  *)
    1.10  
    1.11 @@ -14,7 +15,7 @@
    1.12    structure Syntax: SYNTAX
    1.13    structure Type: TYPE
    1.14    sharing Symtab = Type.Symtab
    1.15 -  local open Type Syntax Syntax.Mixfix in
    1.16 +  local open Type Syntax in
    1.17      type sg
    1.18      val rep_sg: sg ->
    1.19        {tsig: type_sig,
    1.20 @@ -29,6 +30,7 @@
    1.21      val subsort: sg -> sort * sort -> bool      (* FIXME move? *)
    1.22      val norm_sort: sg -> sort -> sort           (* FIXME move? *)
    1.23      val print_sg: sg -> unit
    1.24 +    val pretty_sg: sg -> Pretty.T
    1.25      val pprint_sg: sg -> pprint_args -> unit
    1.26      val pretty_term: sg -> term -> Pretty.T
    1.27      val pretty_typ: sg -> typ -> Pretty.T
    1.28 @@ -39,7 +41,9 @@
    1.29      val certify_typ: sg -> typ -> typ
    1.30      val certify_term: sg -> term -> term * typ * int
    1.31      val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.32 -    val add_classes: (class list * class * class list) list -> sg -> sg
    1.33 +    val infer_types: sg -> (indexname -> typ option) ->
    1.34 +      (indexname -> sort option) -> term * typ -> term * (indexname * typ) list
    1.35 +    val add_classes: (class * class list) list -> sg -> sg
    1.36      val add_classrel: (class * class) list -> sg -> sg
    1.37      val add_defsort: sort -> sg -> sg
    1.38      val add_types: (string * int * mixfix) list -> sg -> sg
    1.39 @@ -58,12 +62,6 @@
    1.40      val add_trrules: xrule list -> sg -> sg
    1.41      val add_name: string -> sg -> sg
    1.42      val make_draft: sg -> sg
    1.43 -    val extend: sg -> string ->
    1.44 -      (class * class list) list * class list *
    1.45 -      (string list * int) list *
    1.46 -      (string * string list * string) list *
    1.47 -      (string list * (sort list * class)) list *
    1.48 -      (string list * string) list * sext option -> sg
    1.49      val merge: sg * sg -> sg
    1.50      val pure: sg
    1.51      val const_of_class: class -> string
    1.52 @@ -79,8 +77,7 @@
    1.53  structure BasicSyntax: BASIC_SYNTAX = Syntax;
    1.54  structure Pretty = Syntax.Pretty;
    1.55  structure Type = Type;
    1.56 -open BasicSyntax (* FIXME *) Type;
    1.57 -open Syntax.Mixfix;   (* FIXME *)
    1.58 +open BasicSyntax Type;
    1.59  
    1.60  
    1.61  (** datatype sg **)
    1.62 @@ -175,8 +172,10 @@
    1.63    end;
    1.64  
    1.65  
    1.66 -fun pprint_sg (Sg {stamps, ...}) =
    1.67 -  Pretty.pprint (Pretty.str_list "{" "}" (stamp_names stamps));
    1.68 +fun pretty_sg (Sg {stamps, ...}) =
    1.69 +  Pretty.str_list "{" "}" (stamp_names stamps);
    1.70 +
    1.71 +val pprint_sg = Pretty.pprint o pretty_sg;
    1.72  
    1.73  
    1.74  
    1.75 @@ -193,6 +192,22 @@
    1.76  
    1.77  
    1.78  
    1.79 +(** read types **)  (*exception ERROR*)
    1.80 +
    1.81 +fun err_in_type s =
    1.82 +  error ("The error(s) above occurred in type " ^ quote s);
    1.83 +
    1.84 +fun read_raw_typ syn tsig sort_of str =
    1.85 +  Syntax.read_typ syn (fn x => if_none (sort_of x) (defaultS tsig)) str
    1.86 +    handle ERROR => err_in_type str;
    1.87 +
    1.88 +(*read and certify typ wrt a signature*)
    1.89 +fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
    1.90 +  cert_typ tsig (read_raw_typ syn tsig sort_of str)
    1.91 +    handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
    1.92 +
    1.93 +
    1.94 +
    1.95  (** certify types and terms **)   (*exception TYPE*)
    1.96  
    1.97  fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
    1.98 @@ -229,22 +244,24 @@
    1.99  
   1.100  
   1.101  
   1.102 -(** read types **)    (*exception ERROR*)
   1.103 +(** infer_types **)         (*exception ERROR*)   (* FIXME check *)
   1.104  
   1.105 -(* FIXME rd_typ vs. read_raw_typ (?) *)
   1.106 -
   1.107 -fun rd_typ tsig syn sort_of s =
   1.108 +fun infer_types sg types sorts (t, T) =
   1.109    let
   1.110 -    val def_sort = defaultS tsig;
   1.111 -    val raw_ty =        (*this may raise ERROR, too!*)
   1.112 -      Syntax.read_typ syn (fn x => if_none (sort_of x) def_sort) s;
   1.113 -  in
   1.114 -    cert_typ tsig raw_ty
   1.115 -      handle TYPE (msg, _, _) => error msg
   1.116 -  end
   1.117 -  handle ERROR => error ("The error(s) above occurred in type " ^ quote s);
   1.118 +    val Sg {tsig, ...} = sg;
   1.119 +    val show_typ = string_of_typ sg;
   1.120 +    val show_term = string_of_term sg;
   1.121  
   1.122 -fun read_typ (Sg {tsig, syn, ...}, sort_of) s = rd_typ tsig syn sort_of s;
   1.123 +    fun term_err [] = ""
   1.124 +      | term_err [t] = "\nInvolving this term:\n" ^ show_term t
   1.125 +      | term_err ts = "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   1.126 +
   1.127 +    val T' = certify_typ sg T
   1.128 +      handle TYPE (msg, _, _) => error msg;
   1.129 +    val (t', tye) = Type.infer_types (tsig, const_type sg, types, sorts, T', t)
   1.130 +      handle TYPE (msg, Ts, ts) => error ("Type checking error: " ^ msg ^ "\n"
   1.131 +        ^ cat_lines (map show_typ Ts) ^ term_err ts);
   1.132 +  in (t', tye) end;
   1.133  
   1.134  
   1.135  
   1.136 @@ -262,10 +279,7 @@
   1.137  (* fake newstyle interfaces *) (* FIXME -> type.ML *)
   1.138  
   1.139  fun ext_tsig_classes tsig classes =
   1.140 -  if exists (fn ([], _, _) => false | _ => true) classes then
   1.141 -    sys_error "FIXME ext_tsig_classes"
   1.142 -  else
   1.143 -    extend_tsig tsig (map (fn (_, c, cs) => (c, cs)) classes, [], [], []);
   1.144 +  extend_tsig tsig (classes, [], [], []);
   1.145  
   1.146  fun ext_tsig_types tsig types =
   1.147    extend_tsig tsig ([], [], map (fn (t, n) => ([t], n)) types, []);
   1.148 @@ -279,22 +293,6 @@
   1.149  
   1.150  
   1.151  
   1.152 -(** read types **)  (*exception ERROR*)
   1.153 -
   1.154 -fun err_in_type s =
   1.155 -  error ("The error(s) above occurred in type " ^ quote s);
   1.156 -
   1.157 -fun read_raw_typ syn tsig sort_of str =
   1.158 -  Syntax.read_typ syn (fn x => if_none (sort_of x) (defaultS tsig)) str
   1.159 -    handle ERROR => err_in_type str;
   1.160 -
   1.161 -(*read and certify typ wrt a signature*)
   1.162 -fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   1.163 -  cert_typ tsig (read_raw_typ syn tsig sort_of str)
   1.164 -    handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   1.165 -
   1.166 -
   1.167 -
   1.168  (** extension functions **)  (*exception ERROR*)
   1.169  
   1.170  fun decls_of name_of mfixs =
   1.171 @@ -311,7 +309,7 @@
   1.172  
   1.173  fun ext_types (syn, tsig, ctab) types =
   1.174    (Syntax.extend_type_gram syn types,
   1.175 -    ext_tsig_types tsig (decls_of type_name types),
   1.176 +    ext_tsig_types tsig (decls_of Syntax.type_name types),
   1.177      ctab);
   1.178  
   1.179  
   1.180 @@ -327,7 +325,7 @@
   1.181      val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs);
   1.182  
   1.183      fun decl_of (t, vs, rhs, mx) =
   1.184 -      rd_abbr syn1 tsig (type_name t mx, vs, rhs);
   1.185 +      rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs);
   1.186    in
   1.187      (syn1, ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   1.188    end;
   1.189 @@ -358,7 +356,7 @@
   1.190  
   1.191  fun read_const syn tsig (c, ty_src, mx) =
   1.192    (c, read_raw_typ syn tsig (K None) ty_src, mx)
   1.193 -    handle ERROR => err_in_const (const_name c mx);
   1.194 +    handle ERROR => err_in_const (Syntax.const_name c mx);
   1.195  
   1.196  (* FIXME move *)
   1.197  fun no_tvars ty =
   1.198 @@ -369,12 +367,12 @@
   1.199    let
   1.200      (* FIXME clean *)
   1.201      fun prep_const (c, ty, mx) = (c, varify_typ (cert_typ tsig (no_tvars ty)), mx)
   1.202 -      handle TYPE (msg, _, _) => (writeln msg; err_in_const (const_name c mx));
   1.203 +      handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
   1.204  
   1.205      val consts = map (prep_const o rd_const syn tsig) raw_consts;
   1.206      val decls =
   1.207        if syn_only then []
   1.208 -      else filter_out (equal "" o fst) (decls_of const_name consts);
   1.209 +      else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
   1.210    in
   1.211      (Syntax.extend_const_gram syn consts, tsig,
   1.212        Symtab.extend_new (ctab, decls)
   1.213 @@ -402,7 +400,7 @@
   1.214  
   1.215  fun ext_classes (syn, tsig, ctab) classes =
   1.216    let
   1.217 -    val names = map (fn (_, c, _) => c) classes;
   1.218 +    val names = map fst classes;
   1.219      val consts =
   1.220        map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   1.221    in
   1.222 @@ -467,57 +465,6 @@
   1.223  
   1.224  
   1.225  
   1.226 -(** extend signature (old) **)      (* FIXME remove *)
   1.227 -
   1.228 -fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
   1.229 -  let
   1.230 -    fun read_abbr syn (c, vs, rhs_src) =
   1.231 -      (c, (map (rpair 0) vs, varifyT (Syntax.read_typ syn (K []) rhs_src)))
   1.232 -        handle ERROR => error ("The error(s) above occurred in the rhs " ^
   1.233 -          quote rhs_src ^ "\nof type abbreviation " ^ quote c);
   1.234 -
   1.235 -    (*reset TVar indices to 0, renaming to preserve distinctness*)
   1.236 -    fun zero_tvar_idxs T =
   1.237 -      let
   1.238 -        val inxSs = typ_tvars T;
   1.239 -        val nms' = variantlist (map (#1 o #1) inxSs, []);
   1.240 -        val tye = map2 (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs, nms');
   1.241 -      in
   1.242 -        typ_subst_TVars tye T
   1.243 -      end;
   1.244 -
   1.245 -    (*read and check the type mentioned in a const declaration; zero type var
   1.246 -      indices because type inference requires it*)
   1.247 -    fun read_const tsig syn (c, s) =
   1.248 -      (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
   1.249 -        handle ERROR => error ("in declaration of constant " ^ quote c);
   1.250 -
   1.251 -
   1.252 -    val Sg {tsig, const_tab, syn, stamps} = sg;
   1.253 -    val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
   1.254 -      flat (map #1 consts);
   1.255 -    val sext = if_none opt_sext Syntax.empty_sext;
   1.256 -
   1.257 -    val tsig' = extend_tsig tsig (classes, default, types, arities);
   1.258 -    val tsig1 = Type.ext_tsig_abbrs tsig' (map (read_abbr syn) abbrs);
   1.259 -
   1.260 -    val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
   1.261 -      (logical_types tsig1, xconsts, sext);
   1.262 -
   1.263 -    val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
   1.264 -      (Syntax.constants sext @ consts));
   1.265 -
   1.266 -    val const_tab1 =
   1.267 -      Symtab.extend_new (const_tab, map (read_const tsig1 syn) all_consts)
   1.268 -        handle Symtab.DUPS cs => err_dup_consts cs;
   1.269 -
   1.270 -    val stamps1 = ext_stamps stamps name;
   1.271 -  in
   1.272 -    Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, stamps = stamps1}
   1.273 -  end;
   1.274 -
   1.275 -
   1.276 -
   1.277  (** merge signatures **)    (*exception TERM*)
   1.278  
   1.279  fun merge (sg1, sg2) =
   1.280 @@ -562,22 +509,22 @@
   1.281     (("fun", 2, NoSyn) ::
   1.282      ("prop", 0, NoSyn) ::
   1.283      ("itself", 1, NoSyn) ::
   1.284 -    Syntax.Mixfix.pure_types)
   1.285 -  |> add_classes [([], logicC, [])]
   1.286 +    Syntax.pure_types)
   1.287 +  |> add_classes [(logicC, [])]
   1.288    |> add_defsort logicS
   1.289    |> add_arities
   1.290     [("fun", [logicS, logicS], logicS),
   1.291      ("prop", [], logicS),
   1.292      ("itself", [logicS], logicS)]
   1.293 -  |> add_syntax Syntax.Mixfix.pure_syntax
   1.294 +  |> add_syntax Syntax.pure_syntax
   1.295    |> add_trfuns Syntax.pure_trfuns
   1.296    |> add_consts
   1.297     [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
   1.298      ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
   1.299      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
   1.300      ("all", "('a => prop) => prop", Binder ("!!", 0)),
   1.301 -    ("TYPE", "'a itself", NoSyn),
   1.302 -    (Syntax.constrainC, "'a::{} => 'a", NoSyn)]
   1.303 +    ("TYPE", "'a itself", NoSyn)(*,(* FIXME *)
   1.304 +    (Syntax.constrainC, "'a::{} => 'a", NoSyn)*)]
   1.305    |> add_name "Pure";
   1.306  
   1.307