of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
authorwenzelm
Sun Apr 11 13:08:14 2010 +0200 (2010-04-11)
changeset 36102a51d1d154c71
parent 36101 bae883012af3
child 36103 b2b9b687a4c4
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
src/Pure/sorts.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/sorts.ML	Fri Apr 09 13:35:54 2010 +0200
     1.2 +++ b/src/Pure/sorts.ML	Sun Apr 11 13:08:14 2010 +0200
     1.3 @@ -57,8 +57,8 @@
     1.4    val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
     1.5    val of_sort: algebra -> typ * sort -> bool
     1.6    val of_sort_derivation: algebra ->
     1.7 -    {class_relation: 'a * class -> class -> 'a,
     1.8 -     type_constructor: string -> ('a * class) list list -> class -> 'a,
     1.9 +    {class_relation: typ -> 'a * class -> class -> 'a,
    1.10 +     type_constructor: string * typ list -> ('a * class) list list -> class -> 'a,
    1.11       type_variable: typ -> ('a * class) list} ->
    1.12      typ * sort -> 'a list   (*exception CLASS_ERROR*)
    1.13    val classrel_derivation: algebra ->
    1.14 @@ -410,24 +410,24 @@
    1.15    let
    1.16      val arities = arities_of algebra;
    1.17  
    1.18 -    fun weaken S1 S2 = S2 |> map (fn c2 =>
    1.19 +    fun weaken T S1 S2 = S2 |> map (fn c2 =>
    1.20        (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
    1.21 -        SOME d1 => class_relation d1 c2
    1.22 +        SOME d1 => class_relation T d1 c2
    1.23        | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
    1.24  
    1.25      fun derive _ [] = []
    1.26 -      | derive (Type (a, Ts)) S =
    1.27 +      | derive (T as Type (a, Us)) S =
    1.28            let
    1.29              val Ss = mg_domain algebra a S;
    1.30 -            val dom = map2 (fn T => fn S => derive T S ~~ S) Ts Ss;
    1.31 +            val dom = map2 (fn U => fn S => derive U S ~~ S) Us Ss;
    1.32            in
    1.33              S |> map (fn c =>
    1.34                let
    1.35                  val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
    1.36 -                val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
    1.37 -              in class_relation (type_constructor a dom' c0, c0) c end)
    1.38 +                val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
    1.39 +              in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
    1.40            end
    1.41 -      | derive T S = weaken (type_variable T) S;
    1.42 +      | derive T S = weaken T (type_variable T) S;
    1.43    in uncurry derive end;
    1.44  
    1.45  fun classrel_derivation algebra class_relation =
     2.1 --- a/src/Tools/Code/code_preproc.ML	Fri Apr 09 13:35:54 2010 +0200
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Apr 11 13:08:14 2010 +0200
     2.3 @@ -365,13 +365,13 @@
     2.4  fun dicts_of thy (proj_sort, algebra) (T, sort) =
     2.5    let
     2.6      fun class_relation (x, _) _ = x;
     2.7 -    fun type_constructor tyco xs class =
     2.8 +    fun type_constructor (tyco, _) xs class =
     2.9        inst_params thy tyco (Sorts.complete_sort algebra [class])
    2.10          @ (maps o maps) fst xs;
    2.11      fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
    2.12    in
    2.13      flat (Sorts.of_sort_derivation algebra
    2.14 -      { class_relation = class_relation, type_constructor = type_constructor,
    2.15 +      { class_relation = K class_relation, type_constructor = type_constructor,
    2.16          type_variable = type_variable } (T, proj_sort sort)
    2.17         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
    2.18    end;
     3.1 --- a/src/Tools/Code/code_thingol.ML	Fri Apr 09 13:35:54 2010 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Sun Apr 11 13:08:14 2010 +0200
     3.3 @@ -767,14 +767,14 @@
     3.4            Global ((class, tyco), yss)
     3.5        | class_relation (Local (classrels, v), subclass) superclass =
     3.6            Local ((subclass, superclass) :: classrels, v);
     3.7 -    fun type_constructor tyco yss class =
     3.8 +    fun type_constructor (tyco, _) yss class =
     3.9        Global ((class, tyco), (map o map) fst yss);
    3.10      fun type_variable (TFree (v, sort)) =
    3.11        let
    3.12          val sort' = proj_sort sort;
    3.13        in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
    3.14      val typargs = Sorts.of_sort_derivation algebra
    3.15 -      {class_relation = Sorts.classrel_derivation algebra class_relation,
    3.16 +      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
    3.17         type_constructor = type_constructor,
    3.18         type_variable = type_variable} (ty, proj_sort sort)
    3.19        handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;