renamed cert_typ_raw to cert_typ_abbrev;
authorwenzelm
Thu Jun 09 12:03:27 2005 +0200 (2005-06-09 ago)
changeset 16340fd027bb32896
parent 16339 b02b6da609c3
child 16341 e573e5167eda
renamed cert_typ_raw to cert_typ_abbrev;
renamed add_abbrs to add_abbrevs;
tuned;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Thu Jun 09 12:03:26 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Jun 09 12:03:27 2005 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
     1.5    val cert_typ: tsig -> typ -> typ
     1.6    val cert_typ_syntax: tsig -> typ -> typ
     1.7 -  val cert_typ_raw: tsig -> typ -> typ
     1.8 +  val cert_typ_abbrev: tsig -> typ -> typ
     1.9  
    1.10    (*special treatment of type vars*)
    1.11    val strip_sorts: typ -> typ
    1.12 @@ -62,7 +62,7 @@
    1.13    val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig
    1.14    val set_defsort: sort -> tsig -> tsig
    1.15    val add_types: (string * int) list -> tsig -> tsig
    1.16 -  val add_abbrs: (string * string list * typ) list -> tsig -> tsig
    1.17 +  val add_abbrevs: (string * string list * typ) list -> tsig -> tsig
    1.18    val add_nonterminals: string list -> tsig -> tsig
    1.19    val add_arities: Pretty.pp -> arity list -> tsig -> tsig
    1.20    val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
    1.21 @@ -186,9 +186,9 @@
    1.22  
    1.23  in
    1.24  
    1.25 -val cert_typ         = certify_typ true false;
    1.26 -val cert_typ_syntax  = certify_typ true true;
    1.27 -val cert_typ_raw     = certify_typ false true;
    1.28 +val cert_typ        = certify_typ true false;
    1.29 +val cert_typ_syntax = certify_typ true true;
    1.30 +val cert_typ_abbrev = certify_typ false true;
    1.31  
    1.32  end;
    1.33  
    1.34 @@ -295,21 +295,21 @@
    1.35  
    1.36  exception TYPE_MATCH;
    1.37  
    1.38 -fun typ_match tsig =
    1.39 +fun typ_match tsig (tyenv, TU) =
    1.40    let
    1.41 -    fun match (subs, (TVar (v, S), T)) =
    1.42 +    fun match (TVar (v, S), T) subs =
    1.43            (case lookup (subs, (v, S)) of
    1.44              NONE =>
    1.45                if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs)
    1.46                else raise TYPE_MATCH
    1.47            | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.48 -      | match (subs, (Type (a, Ts), Type (b, Us))) =
    1.49 +      | match (Type (a, Ts), Type (b, Us)) subs =
    1.50            if a <> b then raise TYPE_MATCH
    1.51 -          else Library.foldl match (subs, Ts ~~ Us)
    1.52 -      | match (subs, (TFree x, TFree y)) =
    1.53 +          else fold match (Ts ~~ Us) subs
    1.54 +      | match (TFree x, TFree y) subs =
    1.55            if x = y then subs else raise TYPE_MATCH
    1.56 -      | match _ = raise TYPE_MATCH;
    1.57 -  in match end;
    1.58 +      | match _ _ = raise TYPE_MATCH;
    1.59 +  in match TU tyenv end;
    1.60  
    1.61  fun typ_instance tsig (T, U) =
    1.62    (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
    1.63 @@ -423,7 +423,7 @@
    1.64      | NONE => (c, Ss) :: ars)
    1.65    end;
    1.66  
    1.67 -fun insert pp C t ((c, Ss), ars) =
    1.68 +fun insert pp C t (c, Ss) ars =
    1.69    (case assoc_string (ars, c) of
    1.70      NONE => coregular pp C t (c, Ss) ars
    1.71    | SOME Ss' =>
    1.72 @@ -434,14 +434,14 @@
    1.73  
    1.74  fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
    1.75  
    1.76 -fun insert_arities pp classes (arities, (t, ars)) =
    1.77 +fun insert_arities pp classes (t, ars) arities =
    1.78    let val ars' =
    1.79      Symtab.lookup_multi (arities, t)
    1.80 -    |> curry (Library.foldr (insert pp classes t)) (List.concat (map (complete classes) ars))
    1.81 +    |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
    1.82    in Symtab.update ((t, ars'), arities) end;
    1.83  
    1.84  fun insert_table pp classes = Symtab.foldl (fn (arities, (t, ars)) =>
    1.85 -  insert_arities pp classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
    1.86 +  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars) arities);
    1.87  
    1.88  in
    1.89  
    1.90 @@ -458,7 +458,7 @@
    1.91        | NONE => error (undecl_type t));
    1.92  
    1.93      val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
    1.94 -    val arities' = Library.foldl (insert_arities pp classes) (arities, ars);
    1.95 +    val arities' = fold (insert_arities pp classes) ars arities;
    1.96    in (classes, default, types, arities') end);
    1.97  
    1.98  fun rebuild_arities pp classes arities =
    1.99 @@ -546,11 +546,11 @@
   1.100          orelse exists (syntactic types) Ts
   1.101    | syntactic _ _ = false;
   1.102  
   1.103 -fun add_abbr (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   1.104 +fun add_abbrev (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   1.105    let
   1.106      fun err msg =
   1.107        error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   1.108 -    val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
   1.109 +    val rhs' = compress_type (strip_sorts (no_tvars (cert_typ_syntax tsig rhs)))
   1.110        handle TYPE (msg, _, _) => err msg;
   1.111    in
   1.112      (case duplicates vs of
   1.113 @@ -567,7 +567,7 @@
   1.114  fun add_types ps = change_types (fold new_decl (ps |> map (fn (c, n) =>
   1.115    if n < 0 then err_neg_args c else (c, LogicalType n))));
   1.116  
   1.117 -val add_abbrs = fold add_abbr;
   1.118 +val add_abbrevs = fold add_abbrev;
   1.119  val add_nonterminals = change_types o fold new_decl o map (rpair Nonterminal);
   1.120  
   1.121  fun merge_types (types1, types2) =