src/Pure/type.ML
changeset 15531 08c8dad8e399
parent 14998 9606c6224933
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/type.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/type.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4        |> Library.sort (Library.int_ord o pairself #2) |> map #1;
     1.5      val witness =
     1.6        (case Sorts.witness_sorts (classes, arities) log_types [] [Graph.keys classes] of
     1.7 -        [w] => Some w | _ => None);
     1.8 +        [w] => SOME w | _ => NONE);
     1.9    in make_tsig (classes, default, types, arities, log_types, witness) end;
    1.10  
    1.11  fun change_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
    1.12 @@ -165,13 +165,13 @@
    1.13              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    1.14            in
    1.15              (case Symtab.lookup (types, c) of
    1.16 -              Some (LogicalType n, _) => (nargs n; Type (c, Ts'))
    1.17 -            | Some (Abbreviation (vs, U, syn), _) => (nargs (length vs);
    1.18 +              SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
    1.19 +            | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
    1.20                  if syn then check_syntax c else ();
    1.21                  if normalize then inst_typ (vs ~~ Ts') U
    1.22                  else Type (c, Ts'))
    1.23 -            | Some (Nonterminal, _) => (nargs 0; check_syntax c; T)
    1.24 -            | None => err (undecl_type c))
    1.25 +            | SOME (Nonterminal, _) => (nargs 0; check_syntax c; T)
    1.26 +            | NONE => err (undecl_type c))
    1.27            end
    1.28        | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S)
    1.29        | cert (TVar (xi as (_, i), S)) =
    1.30 @@ -224,8 +224,8 @@
    1.31      val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
    1.32      fun thaw (f as (a, S)) =
    1.33        (case assoc (fmap, a) of
    1.34 -        None => TFree f
    1.35 -      | Some b => TVar (b, S));
    1.36 +        NONE => TFree f
    1.37 +      | SOME b => TVar (b, S));
    1.38    in (map_term_types (map_type_tfree thaw) t, fmap) end;
    1.39  
    1.40  
    1.41 @@ -239,11 +239,11 @@
    1.42  
    1.43  fun freeze_one alist (ix,sort) =
    1.44    TFree (the (assoc (alist, ix)), sort)
    1.45 -    handle OPTION =>
    1.46 +    handle Option =>
    1.47        raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
    1.48  
    1.49  fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
    1.50 -  handle OPTION => TFree(a, sort);
    1.51 +  handle Option => TFree(a, sort);
    1.52  
    1.53  in
    1.54  
    1.55 @@ -279,10 +279,10 @@
    1.56    let
    1.57      fun inst (var as (v, S)) =
    1.58        (case assoc_string_int (tye, v) of
    1.59 -        Some U =>
    1.60 +        SOME U =>
    1.61            if of_sort tsig (U, S) then U
    1.62            else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
    1.63 -      | None => TVar var);
    1.64 +      | NONE => TVar var);
    1.65    in map_type_tvar inst end;
    1.66  
    1.67  fun inst_term_tvars _ _ [] t = t
    1.68 @@ -297,10 +297,10 @@
    1.69    let
    1.70      fun match (subs, (TVar (v, S), T)) =
    1.71            (case Vartab.lookup (subs, v) of
    1.72 -            None =>
    1.73 +            NONE =>
    1.74                if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
    1.75                else raise TYPE_MATCH
    1.76 -          | Some U => if U = T then subs else raise TYPE_MATCH)
    1.77 +          | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.78        | match (subs, (Type (a, Ts), Type (b, Us))) =
    1.79            if a <> b then raise TYPE_MATCH
    1.80            else foldl match (subs, Ts ~~ Us)
    1.81 @@ -325,15 +325,15 @@
    1.82        | occ (TVar (w, _)) =
    1.83            eq_ix (v, w) orelse
    1.84              (case Vartab.lookup (tye, w) of
    1.85 -              None => false
    1.86 -            | Some U => occ U);
    1.87 +              NONE => false
    1.88 +            | SOME U => occ U);
    1.89    in occ end;
    1.90  
    1.91  (*chase variable assignments; if devar returns a type var then it must be unassigned*)
    1.92  fun devar (T as TVar (v, _), tye) =
    1.93        (case  Vartab.lookup (tye, v) of
    1.94 -        Some U => devar (U, tye)
    1.95 -      | None => T)
    1.96 +        SOME U => devar (U, tye)
    1.97 +      | NONE => T)
    1.98    | devar (T, tye) = T;
    1.99  
   1.100  fun unify (tsig as TSig {classes, arities, ...}) (tyenv, maxidx) TU =
   1.101 @@ -397,8 +397,8 @@
   1.102  
   1.103  fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t);
   1.104  
   1.105 -fun for_classes _ None = ""
   1.106 -  | for_classes pp (Some (c1, c2)) =
   1.107 +fun for_classes _ NONE = ""
   1.108 +  | for_classes pp (SOME (c1, c2)) =
   1.109        " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
   1.110  
   1.111  fun err_conflict pp t cc (c, Ss) (c', Ss') =
   1.112 @@ -410,24 +410,24 @@
   1.113    let
   1.114      fun conflict (c', Ss') =
   1.115        if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then
   1.116 -        Some ((c, c'), (c', Ss'))
   1.117 +        SOME ((c, c'), (c', Ss'))
   1.118        else if Sorts.class_le C (c', c) andalso not (Sorts.sorts_le C (Ss', Ss)) then
   1.119 -        Some ((c', c), (c', Ss'))
   1.120 -      else None;
   1.121 +        SOME ((c', c), (c', Ss'))
   1.122 +      else NONE;
   1.123    in
   1.124      (case Library.get_first conflict ars of
   1.125 -      Some ((c1, c2), (c', Ss')) => err_conflict pp t (Some (c1, c2)) (c, Ss) (c', Ss')
   1.126 -    | None => (c, Ss) :: ars)
   1.127 +      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
   1.128 +    | NONE => (c, Ss) :: ars)
   1.129    end;
   1.130  
   1.131  fun insert pp C t ((c, Ss), ars) =
   1.132    (case assoc_string (ars, c) of
   1.133 -    None => coregular pp C t (c, Ss) ars
   1.134 -  | Some Ss' =>
   1.135 +    NONE => coregular pp C t (c, Ss) ars
   1.136 +  | SOME Ss' =>
   1.137        if Sorts.sorts_le C (Ss, Ss') then ars
   1.138        else if Sorts.sorts_le C (Ss', Ss)
   1.139        then coregular pp C t (c, Ss) (ars \ (c, Ss'))
   1.140 -      else err_conflict pp t None (c, Ss) (c, Ss'));
   1.141 +      else err_conflict pp t NONE (c, Ss) (c, Ss'));
   1.142  
   1.143  fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
   1.144  
   1.145 @@ -446,13 +446,13 @@
   1.146    let
   1.147      fun prep (t, Ss, S) =
   1.148        (case Symtab.lookup (types, t) of
   1.149 -        Some (LogicalType n, _) =>
   1.150 +        SOME (LogicalType n, _) =>
   1.151            if length Ss = n then
   1.152              (t, map (cert_sort tsig) Ss, cert_sort tsig S)
   1.153                handle TYPE (msg, _, _) => error msg
   1.154            else error (bad_nargs t)
   1.155 -      | Some (decl, _) => err_decl t decl
   1.156 -      | None => error (undecl_type t));
   1.157 +      | SOME (decl, _) => err_decl t decl
   1.158 +      | NONE => error (undecl_type t));
   1.159  
   1.160      val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
   1.161      val arities' = foldl (insert_arities pp classes) (arities, ars);
   1.162 @@ -530,8 +530,8 @@
   1.163  
   1.164  fun new_decl (c, decl) types =
   1.165    (case Symtab.lookup (types, c) of
   1.166 -    Some (decl', _) => err_in_decls c decl decl'
   1.167 -  | None => Symtab.update ((c, (decl, stamp ())), types));
   1.168 +    SOME (decl', _) => err_in_decls c decl decl'
   1.169 +  | NONE => Symtab.update ((c, (decl, stamp ())), types));
   1.170  
   1.171  fun the_decl types c = fst (the (Symtab.lookup (types, c)));
   1.172  
   1.173 @@ -539,7 +539,7 @@
   1.174    (classes, default, f types, arities));
   1.175  
   1.176  fun syntactic types (Type (c, Ts)) =
   1.177 -      (case Symtab.lookup (types, c) of Some (Nonterminal, _) => true | _ => false)
   1.178 +      (case Symtab.lookup (types, c) of SOME (Nonterminal, _) => true | _ => false)
   1.179          orelse exists (syntactic types) Ts
   1.180    | syntactic _ _ = false;
   1.181