src/Pure/type.ML
changeset 16289 958207815931
parent 15797 a63605582573
child 16340 fd027bb32896
     1.1 --- a/src/Pure/type.ML	Sun Jun 05 23:07:26 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Sun Jun 05 23:07:27 2005 +0200
     1.3 @@ -42,8 +42,10 @@
     1.4    val varifyT: typ -> typ
     1.5    val unvarifyT: typ -> typ
     1.6    val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
     1.7 -  val freeze_thaw_type : typ -> typ * (typ -> typ)
     1.8 -  val freeze_thaw : term -> term * (term -> term)
     1.9 +  val freeze_thaw_type: typ -> typ * (typ -> typ)
    1.10 +  val freeze_type: typ -> typ
    1.11 +  val freeze_thaw: term -> term * (term -> term)
    1.12 +  val freeze: term -> term
    1.13  
    1.14    (*matching and unification*)
    1.15    exception TYPE_MATCH
    1.16 @@ -147,7 +149,7 @@
    1.17  local
    1.18  
    1.19  fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
    1.20 -  | inst_typ env (T as TFree (x, _)) = getOpt (Library.assoc_string (env, x),T)
    1.21 +  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
    1.22    | inst_typ _ T = T;
    1.23  
    1.24  fun certify_typ normalize syntax tsig ty =
    1.25 @@ -233,17 +235,17 @@
    1.26  
    1.27  local
    1.28  
    1.29 -fun new_name (ix, (pairs,used)) =
    1.30 -      let val v = variant used (string_of_indexname ix)
    1.31 -      in  ((ix,v)::pairs, v::used)  end;
    1.32 +fun new_name (ix, (pairs, used)) =
    1.33 +  let val v = variant used (string_of_indexname ix)
    1.34 +  in ((ix, v) :: pairs, v :: used) end;
    1.35  
    1.36 -fun freeze_one alist (ix,sort) =
    1.37 -  TFree (valOf (assoc (alist, ix)), sort)
    1.38 +fun freeze_one alist (ix, sort) =
    1.39 +  TFree (the (assoc_string_int (alist, ix)), sort)
    1.40      handle Option =>
    1.41        raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
    1.42  
    1.43 -fun thaw_one alist (a,sort) = TVar (valOf (assoc (alist,a)), sort)
    1.44 -  handle Option => TFree(a, sort);
    1.45 +fun thaw_one alist (a, sort) = TVar (the (assoc_string (alist, a)), sort)
    1.46 +  handle Option => TFree (a, sort);
    1.47  
    1.48  in
    1.49  
    1.50 @@ -255,6 +257,8 @@
    1.51      val (alist, _) = foldr new_name ([], used) tvars;
    1.52    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
    1.53  
    1.54 +val freeze_type = #1 o freeze_thaw_type;
    1.55 +
    1.56  fun freeze_thaw t =
    1.57    let
    1.58      val used = it_term_types add_typ_tfree_names (t, [])
    1.59 @@ -267,6 +271,8 @@
    1.60        map_term_types (map_type_tfree (thaw_one (map swap alist)))))
    1.61    end;
    1.62  
    1.63 +val freeze = #1 o freeze_thaw;
    1.64 +
    1.65  end;
    1.66  
    1.67  
    1.68 @@ -279,9 +285,11 @@
    1.69    quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
    1.70    [TVar (ixn, S), TVar (ixn, S')], []);
    1.71  
    1.72 -fun lookup (tye, (ixn, S)) = case Vartab.lookup (tye, ixn) of
    1.73 +fun lookup (tye, (ixn, S)) =
    1.74 +  (case Vartab.lookup (tye, ixn) of
    1.75      NONE => NONE
    1.76 -  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S';
    1.77 +  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
    1.78 +
    1.79  
    1.80  (* matching *)
    1.81  
    1.82 @@ -528,7 +536,7 @@
    1.83      SOME (decl', _) => err_in_decls c decl decl'
    1.84    | NONE => Symtab.update ((c, (decl, stamp ())), types));
    1.85  
    1.86 -fun the_decl types c = fst (valOf (Symtab.lookup (types, c)));
    1.87 +fun the_decl types c = fst (the (Symtab.lookup (types, c)));
    1.88  
    1.89  fun change_types f = change_tsig (fn (classes, default, types, arities) =>
    1.90    (classes, default, f types, arities));