refer to structure Type instead of Sorts;
authorwenzelm
Tue Apr 25 22:23:30 2006 +0200 (2006-04-25)
changeset 19465e6093a7fa53a
parent 19464 d13309e30aba
child 19466 29bc35832a77
refer to structure Type instead of Sorts;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Tue Apr 25 22:23:24 2006 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Apr 25 22:23:30 2006 +0200
     1.3 @@ -257,31 +257,29 @@
     1.4  exception NO_UNIFIER of string;
     1.5  
     1.6  
     1.7 -fun unify pp classes arities =
     1.8 +fun unify pp tsig =
     1.9    let
    1.10  
    1.11      (* adjust sorts of parameters *)
    1.12  
    1.13 -    fun not_in_sort x S' S =
    1.14 +    fun not_of_sort x S' S =
    1.15        "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
    1.16          Pretty.string_of_sort pp S;
    1.17  
    1.18 -    fun no_domain (a, c) = "No way to get " ^ Pretty.string_of_arity pp (a, [], [c]);
    1.19 -
    1.20      fun meet (_, []) = ()
    1.21        | meet (Link (r as (ref (Param S'))), S) =
    1.22 -          if Sorts.sort_le classes (S', S) then ()
    1.23 -          else r := mk_param (Sorts.inter_sort classes (S', S))
    1.24 +          if Type.subsort tsig (S', S) then ()
    1.25 +          else r := mk_param (Type.inter_sort tsig (S', S))
    1.26        | meet (Link (ref T), S) = meet (T, S)
    1.27        | meet (PType (a, Ts), S) =
    1.28 -          ListPair.app meet (Ts, Sorts.mg_domain (classes, arities) a S
    1.29 -            handle Sorts.DOMAIN ac => raise NO_UNIFIER (no_domain ac))
    1.30 +          ListPair.app meet (Ts, Type.arity_sorts pp tsig a S
    1.31 +            handle ERROR msg => raise NO_UNIFIER msg)
    1.32        | meet (PTFree (x, S'), S) =
    1.33 -          if Sorts.sort_le classes (S', S) then ()
    1.34 -          else raise NO_UNIFIER (not_in_sort x S' S)
    1.35 +          if Type.subsort tsig (S', S) then ()
    1.36 +          else raise NO_UNIFIER (not_of_sort x S' S)
    1.37        | meet (PTVar (xi, S'), S) =
    1.38 -          if Sorts.sort_le classes (S', S) then ()
    1.39 -          else raise NO_UNIFIER (not_in_sort (Syntax.string_of_vname xi) S' S)
    1.40 +          if Type.subsort tsig (S', S) then ()
    1.41 +          else raise NO_UNIFIER (not_of_sort (Syntax.string_of_vname xi) S' S)
    1.42        | meet (Param _, _) = sys_error "meet";
    1.43  
    1.44  
    1.45 @@ -332,7 +330,7 @@
    1.46  
    1.47  (* infer *)                                     (*DESTRUCTIVE*)
    1.48  
    1.49 -fun infer pp classes arities =
    1.50 +fun infer pp tsig =
    1.51    let
    1.52      (* errors *)
    1.53  
    1.54 @@ -376,7 +374,7 @@
    1.55  
    1.56      (* main *)
    1.57  
    1.58 -    val unif = unify pp classes arities;
    1.59 +    val unif = unify pp tsig;
    1.60  
    1.61      fun inf _ (PConst (_, T)) = T
    1.62        | inf _ (PFree (_, T)) = T
    1.63 @@ -402,7 +400,7 @@
    1.64  
    1.65  (* basic_infer_types *)
    1.66  
    1.67 -fun basic_infer_types pp const_type classes arities used freeze is_param ts Ts =
    1.68 +fun basic_infer_types pp tsig const_type used freeze is_param ts Ts =
    1.69    let
    1.70      (*convert to preterms/typs*)
    1.71      val (Tps, Ts') = pretyps_of (K true) ([], Ts);
    1.72 @@ -410,7 +408,7 @@
    1.73  
    1.74      (*run type inference*)
    1.75      val tTs' = ListPair.map Constraint (ts', Ts');
    1.76 -    val _ = List.app (fn t => (infer pp classes arities t; ())) tTs';
    1.77 +    val _ = List.app (fn t => (infer pp tsig t; ())) tTs';
    1.78  
    1.79      (*collect result unifier*)
    1.80      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
    1.81 @@ -529,13 +527,12 @@
    1.82  fun infer_types pp tsig const_type def_type def_sort
    1.83      map_const map_type map_sort used freeze pat_Ts raw_ts =
    1.84    let
    1.85 -    val {classes, arities, ...} = Type.rep_tsig tsig;
    1.86      val pat_Ts' = map (Type.cert_typ tsig) pat_Ts;
    1.87      val is_const = is_some o const_type;
    1.88      val raw_ts' =
    1.89        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
    1.90 -    val (ts, Ts, unifier) = basic_infer_types pp const_type
    1.91 -      (#2 classes) arities used freeze is_param raw_ts' pat_Ts';
    1.92 +    val (ts, Ts, unifier) =
    1.93 +      basic_infer_types pp tsig const_type used freeze is_param raw_ts' pat_Ts';
    1.94    in (ts, unifier) end;
    1.95  
    1.96  end;