paramify_vars: Term_Subst.map_atypsT_same
authorwenzelm
Thu Jul 23 16:53:00 2009 +0200 (2009-07-23)
changeset 321464937d9836824
parent 32145 220c9e439d39
child 32147 8228f67bfe18
paramify_vars: Term_Subst.map_atypsT_same
recovered coding conventions of this module;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Thu Jul 23 16:52:16 2009 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Jul 23 16:53:00 2009 +0200
     1.3 @@ -40,7 +40,9 @@
     1.4  fun param i (x, S) = TVar (("?" ^ x, i), S);
     1.5  
     1.6  val paramify_vars =
     1.7 -  perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE));
     1.8 +  Same.commit
     1.9 +    (Term_Subst.map_atypsT_same
    1.10 +      (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
    1.11  
    1.12  val paramify_dummies =
    1.13    let
    1.14 @@ -90,9 +92,10 @@
    1.15  
    1.16  (* utils *)
    1.17  
    1.18 -fun deref tye (T as Param (i, S)) = (case Inttab.lookup tye i of
    1.19 -      NONE => T
    1.20 -    | SOME U => deref tye U)
    1.21 +fun deref tye (T as Param (i, S)) =
    1.22 +      (case Inttab.lookup tye i of
    1.23 +        NONE => T
    1.24 +      | SOME U => deref tye U)
    1.25    | deref tye T = T;
    1.26  
    1.27  fun fold_pretyps f (PConst (_, T)) x = f T x
    1.28 @@ -194,32 +197,35 @@
    1.29  
    1.30  (* add_parms *)
    1.31  
    1.32 -fun add_parmsT tye T = case deref tye T of
    1.33 +fun add_parmsT tye T =
    1.34 +  (case deref tye T of
    1.35      PType (_, Ts) => fold (add_parmsT tye) Ts
    1.36    | Param (i, _) => insert (op =) i
    1.37 -  | _ => I;
    1.38 +  | _ => I);
    1.39  
    1.40  fun add_parms tye = fold_pretyps (add_parmsT tye);
    1.41  
    1.42  
    1.43  (* add_names *)
    1.44  
    1.45 -fun add_namesT tye T = case deref tye T of
    1.46 +fun add_namesT tye T =
    1.47 +  (case deref tye T of
    1.48      PType (_, Ts) => fold (add_namesT tye) Ts
    1.49    | PTFree (x, _) => Name.declare x
    1.50    | PTVar ((x, _), _) => Name.declare x
    1.51 -  | Param _ => I;
    1.52 +  | Param _ => I);
    1.53  
    1.54  fun add_names tye = fold_pretyps (add_namesT tye);
    1.55  
    1.56  
    1.57  (* simple_typ/term_of *)
    1.58  
    1.59 -fun simple_typ_of tye f T = case deref tye T of
    1.60 +fun simple_typ_of tye f T =
    1.61 +  (case deref tye T of
    1.62      PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts)
    1.63    | PTFree v => TFree v
    1.64    | PTVar v => TVar v
    1.65 -  | Param (i, S) => TVar (f i, S);
    1.66 +  | Param (i, S) => TVar (f i, S));
    1.67  
    1.68  (*convert types, drop constraints*)
    1.69  fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T)
    1.70 @@ -282,7 +288,8 @@
    1.71  
    1.72      fun occurs_check tye i (Param (i', S)) =
    1.73            if i = i' then raise NO_UNIFIER ("Occurs check!", tye)
    1.74 -          else (case Inttab.lookup tye i' of
    1.75 +          else
    1.76 +            (case Inttab.lookup tye i' of
    1.77                NONE => ()
    1.78              | SOME T => occurs_check tye i T)
    1.79        | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
    1.80 @@ -297,14 +304,15 @@
    1.81  
    1.82      (* unification *)
    1.83  
    1.84 -    fun unif (T1, T2) (tye_idx as (tye, idx)) = case (deref tye T1, deref tye T2) of
    1.85 +    fun unif (T1, T2) (tye_idx as (tye, idx)) =
    1.86 +      (case (deref tye T1, deref tye T2) of
    1.87          (Param (i, S), T) => assign i T S tye_idx
    1.88        | (T, Param (i, S)) => assign i T S tye_idx
    1.89        | (PType (a, Ts), PType (b, Us)) =>
    1.90            if a <> b then
    1.91              raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye)
    1.92            else fold unif (Ts ~~ Us) tye_idx
    1.93 -      | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye);
    1.94 +      | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));
    1.95  
    1.96    in unif end;
    1.97  
    1.98 @@ -396,7 +404,7 @@
    1.99            let val (T, tye_idx') = inf bs t tye_idx in
   1.100              (T,
   1.101               unif (T, U) tye_idx'
   1.102 -             handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
   1.103 +               handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
   1.104            end;
   1.105  
   1.106    in inf [] end;