src/Pure/type.ML
changeset 14830 faa4865ba1ce
parent 14790 0d984ee030a1
child 14906 2da524f3d785
     1.1 --- a/src/Pure/type.ML	Sat May 29 15:05:02 2004 +0200
     1.2 +++ b/src/Pure/type.ML	Sat May 29 15:05:25 2004 +0200
     1.3 @@ -32,7 +32,6 @@
     1.4    val cert_class: tsig -> class -> class
     1.5    val cert_sort: tsig -> sort -> sort
     1.6    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
     1.7 -  val norm_typ: tsig -> typ -> typ
     1.8    val cert_typ: tsig -> typ -> typ
     1.9    val cert_typ_syntax: tsig -> typ -> typ
    1.10    val cert_typ_raw: tsig -> typ -> typ
    1.11 @@ -47,8 +46,8 @@
    1.12    val freeze_thaw : term -> term * (term -> term)
    1.13  
    1.14    (*matching and unification*)
    1.15 -  val inst_term_tvars: tsig -> (indexname * typ) list -> term -> term
    1.16 -  val inst_typ_tvars: tsig -> (indexname * typ) list -> typ -> typ
    1.17 +  val inst_typ_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> typ -> typ
    1.18 +  val inst_term_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> term -> term
    1.19    exception TYPE_MATCH
    1.20    val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
    1.21    val typ_instance: tsig -> typ * typ -> bool
    1.22 @@ -57,14 +56,14 @@
    1.23    val raw_unify: typ * typ -> bool
    1.24  
    1.25    (*extend and merge type signatures*)
    1.26 -  val add_classes: (class * class list) list -> tsig -> tsig
    1.27 -  val add_classrel: (class * class) list -> tsig -> tsig
    1.28 +  val add_classes: Pretty.pp -> (class * class list) list -> tsig -> tsig
    1.29 +  val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig
    1.30    val set_defsort: sort -> tsig -> tsig
    1.31    val add_types: (string * int) list -> tsig -> tsig
    1.32    val add_abbrs: (string * string list * typ) list -> tsig -> tsig
    1.33    val add_nonterminals: string list -> tsig -> tsig
    1.34 -  val add_arities: (string * sort list * sort) list -> tsig -> tsig
    1.35 -  val merge_tsigs: tsig * tsig -> tsig
    1.36 +  val add_arities: Pretty.pp -> arity list -> tsig -> tsig
    1.37 +  val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
    1.38  end;
    1.39  
    1.40  structure Type: TYPE =
    1.41 @@ -147,6 +146,9 @@
    1.42  (* certified types *)
    1.43  
    1.44  fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
    1.45 +fun undecl_type c = "Undeclared type constructor: " ^ quote c;
    1.46 +
    1.47 +local
    1.48  
    1.49  fun inst_typ tye =
    1.50    let
    1.51 @@ -156,7 +158,6 @@
    1.52        | None => TVar var);
    1.53    in map_type_tvar inst end;
    1.54  
    1.55 -(*expand type abbreviations and normalize sorts*)
    1.56  fun norm_typ (tsig as TSig {types, ...}) ty =
    1.57    let
    1.58      val idx = Term.maxidx_of_typ ty + 1;
    1.59 @@ -172,7 +173,6 @@
    1.60      val ty' = norm ty;
    1.61    in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    1.62  
    1.63 -(*check validity of (not necessarily normal) type*)   (*exception TYPE*)
    1.64  fun certify_typ normalize syntax tsig ty =
    1.65    let
    1.66      val TSig {types, ...} = tsig;
    1.67 @@ -186,7 +186,7 @@
    1.68                Some (LogicalType n, _) => nargs n
    1.69              | Some (Abbreviation (vs, _), _) => nargs (length vs)
    1.70              | Some (Nonterminal, _) => nargs 0
    1.71 -            | None => err ("Undeclared type constructor: " ^ quote c));
    1.72 +            | None => err (undecl_type c));
    1.73              seq check_typ Ts
    1.74            end
    1.75      | check_typ (TFree (_, S)) = check_sort S
    1.76 @@ -206,10 +206,13 @@
    1.77      val _ = if not syntax then no_syntax ty' else ();
    1.78    in ty' end;
    1.79  
    1.80 +in
    1.81 +
    1.82  val cert_typ         = certify_typ true false;
    1.83  val cert_typ_syntax  = certify_typ true true;
    1.84  val cert_typ_raw     = certify_typ false true;
    1.85  
    1.86 +end;
    1.87  
    1.88  
    1.89  (** special treatment of type vars **)
    1.90 @@ -226,7 +229,7 @@
    1.91  fun no_tvars T =
    1.92    (case typ_tvars T of [] => T
    1.93    | vs => raise TYPE ("Illegal schematic type variable(s): " ^
    1.94 -      commas (map (Term.string_of_vname o #1) vs), [T], []));
    1.95 +      commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
    1.96  
    1.97  
    1.98  (* varify, unvarify *)
    1.99 @@ -263,7 +266,7 @@
   1.100        raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
   1.101  
   1.102  fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
   1.103 -      handle OPTION => TFree(a,sort);
   1.104 +  handle OPTION => TFree(a, sort);
   1.105  
   1.106  in
   1.107  
   1.108 @@ -295,20 +298,20 @@
   1.109  
   1.110  (* instantiation *)
   1.111  
   1.112 -fun type_of_sort tsig (T, S) =
   1.113 +fun type_of_sort pp tsig (T, S) =
   1.114    if of_sort tsig (T, S) then T
   1.115 -  else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
   1.116 +  else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [T], []);
   1.117  
   1.118 -fun inst_typ_tvars tsig tye =
   1.119 +fun inst_typ_tvars pp tsig tye =
   1.120    let
   1.121      fun inst (var as (v, S)) =
   1.122        (case assoc_string_int (tye, v) of
   1.123 -        Some U => type_of_sort tsig (U, S)
   1.124 +        Some U => type_of_sort pp tsig (U, S)
   1.125        | None => TVar var);
   1.126    in map_type_tvar inst end;
   1.127  
   1.128 -fun inst_term_tvars _ [] t = t
   1.129 -  | inst_term_tvars tsig tye t = map_term_types (inst_typ_tvars tsig tye) t;
   1.130 +fun inst_term_tvars _ _ [] t = t
   1.131 +  | inst_term_tvars pp tsig tye t = map_term_types (inst_typ_tvars pp tsig tye) t;
   1.132  
   1.133  
   1.134  (* matching *)
   1.135 @@ -319,7 +322,7 @@
   1.136    let
   1.137      fun match (subs, (TVar (v, S), T)) =
   1.138            (case Vartab.lookup (subs, v) of
   1.139 -            None => (Vartab.update_new ((v, type_of_sort tsig (T, S)), subs)
   1.140 +            None => (Vartab.update_new ((v, type_of_sort Pretty.pp_undef tsig (T, S)), subs)
   1.141                handle TYPE _ => raise TYPE_MATCH)
   1.142            | Some U => if U = T then subs else raise TYPE_MATCH)
   1.143        | match (subs, (Type (a, Ts), Type (b, Us))) =
   1.144 @@ -417,14 +420,17 @@
   1.145  local
   1.146  
   1.147  fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t);
   1.148 -fun err_undecl t = error ("Undeclared type constructor: " ^ quote t);
   1.149 +
   1.150 +fun for_classes _ None = ""
   1.151 +  | for_classes pp (Some (c1, c2)) =
   1.152 +      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
   1.153  
   1.154 -fun err_conflict t (c1, c2) (c, Ss) (c', Ss') =
   1.155 -  error ("Conflict of type arities for classes " ^ quote c1 ^ " < " ^ quote c2 ^ ":\n  " ^
   1.156 -    Sorts.str_of_arity (t, Ss, [c]) ^ " and\n  " ^
   1.157 -    Sorts.str_of_arity (t, Ss', [c']));
   1.158 +fun err_conflict pp t cc (c, Ss) (c', Ss') =
   1.159 +  error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
   1.160 +    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
   1.161 +    Pretty.string_of_arity pp (t, Ss', [c']));
   1.162  
   1.163 -fun coregular C t (c, Ss) ars =
   1.164 +fun coregular pp C t (c, Ss) ars =
   1.165    let
   1.166      fun conflict (c', Ss') =
   1.167        if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then
   1.168 @@ -434,33 +440,33 @@
   1.169        else None;
   1.170    in
   1.171      (case Library.get_first conflict ars of
   1.172 -      Some ((c1, c2), (c', Ss')) => err_conflict t (c1, c2) (c, Ss) (c', Ss')
   1.173 +      Some ((c1, c2), (c', Ss')) => err_conflict pp t (Some (c1, c2)) (c, Ss) (c', Ss')
   1.174      | None => (c, Ss) :: ars)
   1.175    end;
   1.176  
   1.177 -fun insert C t ((c, Ss), ars) =
   1.178 +fun insert pp C t ((c, Ss), ars) =
   1.179    (case assoc_string (ars, c) of
   1.180 -    None => coregular C t (c, Ss) ars
   1.181 +    None => coregular pp C t (c, Ss) ars
   1.182    | Some Ss' =>
   1.183        if Sorts.sorts_le C (Ss, Ss') then ars
   1.184        else if Sorts.sorts_le C (Ss', Ss)
   1.185 -      then coregular C t (c, Ss) (ars \ (c, Ss'))
   1.186 -      else coregular C t (c, Ss) ars);
   1.187 +      then coregular pp C t (c, Ss) (ars \ (c, Ss'))
   1.188 +      else err_conflict pp t None (c, Ss) (c, Ss'));
   1.189  
   1.190  fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
   1.191  
   1.192 -fun insert_arities classes (arities, (t, ars)) =
   1.193 +fun insert_arities pp classes (arities, (t, ars)) =
   1.194    let val ars' =
   1.195      Symtab.lookup_multi (arities, t)
   1.196 -    |> curry (foldr (insert classes t)) (flat (map (complete classes) ars))
   1.197 +    |> curry (foldr (insert pp classes t)) (flat (map (complete classes) ars))
   1.198    in Symtab.update ((t, ars'), arities) end;
   1.199  
   1.200 -fun insert_table classes = Symtab.foldl (fn (arities, (t, ars)) =>
   1.201 -  insert_arities classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
   1.202 +fun insert_table pp classes = Symtab.foldl (fn (arities, (t, ars)) =>
   1.203 +  insert_arities pp classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
   1.204  
   1.205  in
   1.206  
   1.207 -fun add_arities decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.208 +fun add_arities pp decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.209    let
   1.210      fun prep (t, Ss, S) =
   1.211        (case Symtab.lookup (types, t) of
   1.212 @@ -470,17 +476,17 @@
   1.213                handle TYPE (msg, _, _) => error msg
   1.214            else error (bad_nargs t)
   1.215        | Some (decl, _) => err_decl t decl
   1.216 -      | None => err_undecl t);
   1.217 +      | None => error (undecl_type t));
   1.218  
   1.219      val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
   1.220 -    val arities' = foldl (insert_arities classes) (arities, ars);
   1.221 +    val arities' = foldl (insert_arities pp classes) (arities, ars);
   1.222    in (classes, default, types, arities') end);
   1.223  
   1.224 -fun rebuild_arities classes arities =
   1.225 -  insert_table classes (Symtab.empty, arities);
   1.226 +fun rebuild_arities pp classes arities =
   1.227 +  insert_table pp classes (Symtab.empty, arities);
   1.228  
   1.229 -fun merge_arities classes (arities1, arities2) =
   1.230 -  insert_table classes (insert_table classes (Symtab.empty, arities1), arities2);
   1.231 +fun merge_arities pp classes (arities1, arities2) =
   1.232 +  insert_table pp classes (insert_table pp classes (Symtab.empty, arities1), arities2);
   1.233  
   1.234  end;
   1.235  
   1.236 @@ -492,37 +498,37 @@
   1.237  fun err_dup_classes cs =
   1.238    error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   1.239  
   1.240 -fun err_cyclic_classes css =
   1.241 +fun err_cyclic_classes pp css =
   1.242    error (cat_lines (map (fn cs =>
   1.243 -    "Cycle in class relation: " ^ space_implode " < " (map quote cs)) css));
   1.244 +    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   1.245  
   1.246 -fun add_class (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.247 +fun add_class pp (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.248    let
   1.249      val cs' = map (cert_class tsig) cs
   1.250        handle TYPE (msg, _, _) => error msg;
   1.251      val classes' = classes |> Graph.new_node (c, stamp ())
   1.252        handle Graph.DUP d => err_dup_classes [d];
   1.253      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs')
   1.254 -      handle Graph.CYCLES css => err_cyclic_classes css;
   1.255 +      handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.256    in (classes'', default, types, arities) end);
   1.257  
   1.258  in
   1.259  
   1.260 -val add_classes = fold add_class;
   1.261 +val add_classes = fold o add_class;
   1.262  
   1.263 -fun add_classrel ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.264 +fun add_classrel pp ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.265    let
   1.266      val ps' = map (pairself (cert_class tsig)) ps
   1.267        handle TYPE (msg, _, _) => error msg;
   1.268      val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
   1.269 -      handle Graph.CYCLES css => err_cyclic_classes css;
   1.270 +      handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.271      val default' = default |> Sorts.norm_sort classes';
   1.272 -    val arities' = arities |> rebuild_arities classes';
   1.273 +    val arities' = arities |> rebuild_arities pp classes';
   1.274    in (classes', default', types, arities') end);
   1.275  
   1.276 -fun merge_classes CC = Graph.merge_trans_acyclic (op =) CC
   1.277 +fun merge_classes pp CC = Graph.merge_trans_acyclic (op =) CC
   1.278    handle Graph.DUPS cs => err_dup_classes cs
   1.279 -    | Graph.CYCLES css => err_cyclic_classes css;
   1.280 +    | Graph.CYCLES css => err_cyclic_classes pp css;
   1.281  
   1.282  end;
   1.283  
   1.284 @@ -545,8 +551,9 @@
   1.285      val s = str_of_decl decl;
   1.286      val s' = str_of_decl decl';
   1.287    in
   1.288 -    if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
   1.289 -    else error ("Conflicting declarations of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   1.290 +    if s = s' then
   1.291 +      error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
   1.292 +    else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   1.293    end;
   1.294  
   1.295  fun new_decl (c, decl) types =
   1.296 @@ -592,17 +599,17 @@
   1.297  
   1.298  (* merge type signatures *)
   1.299  
   1.300 -fun merge_tsigs (tsig1, tsig2) =
   1.301 +fun merge_tsigs pp (tsig1, tsig2) =
   1.302    let
   1.303      val (TSig {classes = classes1, default = default1, types = types1, arities = arities1,
   1.304        log_types = _, witness = _}) = tsig1;
   1.305      val (TSig {classes = classes2, default = default2, types = types2, arities = arities2,
   1.306        log_types = _, witness = _}) = tsig2;
   1.307  
   1.308 -    val classes' = merge_classes (classes1, classes2);
   1.309 +    val classes' = merge_classes pp (classes1, classes2);
   1.310      val default' = Sorts.inter_sort classes' (default1, default2);
   1.311      val types' = merge_types (types1, types2);
   1.312 -    val arities' = merge_arities classes' (arities1, arities2);
   1.313 +    val arities' = merge_arities pp classes' (arities1, arities2);
   1.314    in build_tsig (classes', default', types', arities') end;
   1.315  
   1.316  end;