renamed of_sort_derivation record fields (avoid clash with Alice keywords);
authorwenzelm
Tue Apr 03 19:24:16 2007 +0200 (2007-04-03 ago)
changeset 22570f166a5416b3f
parent 22569 e5d7d9de7d85
child 22571 3f00e937d1c9
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/codegen_package.ML
src/Pure/axclass.ML
src/Pure/sorts.ML
     1.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Tue Apr 03 19:24:15 2007 +0200
     1.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Tue Apr 03 19:24:16 2007 +0200
     1.3 @@ -89,17 +89,18 @@
     1.4    let
     1.5      val tys_decl = Sign.const_typargs thy (c, ty_decl);
     1.6      val tys = Sign.const_typargs thy (c, ty);
     1.7 -    fun classrel (x, _) _ = x;
     1.8 -    fun constructor tyco xs class =
     1.9 +    fun class_relation (x, _) _ = x;
    1.10 +    fun type_constructor tyco xs class =
    1.11        (tyco, class) :: maps (maps fst) xs;
    1.12 -    fun variable (TVar (_, sort)) = map (pair []) sort
    1.13 -      | variable (TFree (_, sort)) = map (pair []) sort;
    1.14 +    fun type_variable (TVar (_, sort)) = map (pair []) sort
    1.15 +      | type_variable (TFree (_, sort)) = map (pair []) sort;
    1.16      fun mk_inst ty (TVar (_, sort)) = cons (ty, sort)
    1.17        | mk_inst ty (TFree (_, sort)) = cons (ty, sort)
    1.18        | mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2;
    1.19      fun of_sort_deriv (ty, sort) =
    1.20        Sorts.of_sort_derivation (Sign.pp thy) algebra
    1.21 -        { classrel = classrel, constructor = constructor, variable = variable }
    1.22 +        { class_relation = class_relation, type_constructor = type_constructor,
    1.23 +          type_variable = type_variable }
    1.24          (ty, sort)
    1.25    in
    1.26      flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
     2.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Apr 03 19:24:15 2007 +0200
     2.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Apr 03 19:24:16 2007 +0200
     2.3 @@ -210,18 +210,19 @@
     2.4      datatype typarg =
     2.5          Global of (class * string) * typarg list list
     2.6        | Local of (class * class) list * (string * (int * sort));
     2.7 -    fun classrel (Global ((_, tyco), yss), _) class =
     2.8 +    fun class_relation (Global ((_, tyco), yss), _) class =
     2.9            Global ((class, tyco), yss)
    2.10 -      | classrel (Local (classrels, v), subclass) superclass =
    2.11 +      | class_relation (Local (classrels, v), subclass) superclass =
    2.12            Local ((subclass, superclass) :: classrels, v);
    2.13 -    fun constructor tyco yss class =
    2.14 +    fun type_constructor tyco yss class =
    2.15        Global ((class, tyco), (map o map) fst yss);
    2.16 -    fun variable (TFree (v, sort)) =
    2.17 +    fun type_variable (TFree (v, sort)) =
    2.18        let
    2.19          val sort' = proj_sort sort;
    2.20        in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
    2.21      val typargs = Sorts.of_sort_derivation pp algebra
    2.22 -      {classrel = classrel, constructor = constructor, variable = variable}
    2.23 +      {class_relation = class_relation, type_constructor = type_constructor,
    2.24 +       type_variable = type_variable}
    2.25        (ty_ctxt, proj_sort sort_decl);
    2.26      fun mk_dict (Global (inst, yss)) =
    2.27            ensure_def_inst thy algbr funcgr strct inst
     3.1 --- a/src/Pure/axclass.ML	Tue Apr 03 19:24:15 2007 +0200
     3.2 +++ b/src/Pure/axclass.ML	Tue Apr 03 19:24:16 2007 +0200
     3.3 @@ -436,13 +436,13 @@
     3.4          val hyps = vars
     3.5            |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
     3.6          val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
     3.7 -           {classrel =
     3.8 +           {class_relation =
     3.9                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
    3.10 -            constructor =
    3.11 +            type_constructor =
    3.12                fn a => fn dom => fn c =>
    3.13                  let val Ss = map (map snd) dom and ths = maps (map fst) dom
    3.14                  in ths MRS the_arity thy a (c, Ss) end,
    3.15 -            variable =
    3.16 +            type_variable =
    3.17                the_default [] o AList.lookup (op =) hyps};
    3.18        in ths end;
    3.19  
     4.1 --- a/src/Pure/sorts.ML	Tue Apr 03 19:24:15 2007 +0200
     4.2 +++ b/src/Pure/sorts.ML	Tue Apr 03 19:24:16 2007 +0200
     4.3 @@ -52,9 +52,9 @@
     4.4    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
     4.5    val of_sort: algebra -> typ * sort -> bool
     4.6    val of_sort_derivation: Pretty.pp -> algebra ->
     4.7 -    {classrel: 'a * class -> class -> 'a,
     4.8 -     constructor: string -> ('a * class) list list -> class -> 'a,
     4.9 -     variable: typ -> ('a * class) list} ->
    4.10 +    {class_relation: 'a * class -> class -> 'a,
    4.11 +     type_constructor: string -> ('a * class) list list -> class -> 'a,
    4.12 +     type_variable: typ -> ('a * class) list} ->
    4.13      typ * sort -> 'a list   (*exception CLASS_ERROR*)
    4.14    val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
    4.15  end;
    4.16 @@ -348,11 +348,11 @@
    4.17  
    4.18  (* of_sort_derivation *)
    4.19  
    4.20 -fun of_sort_derivation pp algebra {classrel, constructor, variable} =
    4.21 +fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
    4.22    let
    4.23      val {classes, arities} = rep_algebra algebra;
    4.24      fun weaken_path (x, c1 :: c2 :: cs) =
    4.25 -          weaken_path (classrel (x, c1) c2, c2 :: cs)
    4.26 +          weaken_path (class_relation (x, c1) c2, c2 :: cs)
    4.27        | weaken_path (x, _) = x;
    4.28      fun weaken (x, c1) c2 =
    4.29        (case Graph.irreducible_paths classes (c1, c2) of
    4.30 @@ -375,9 +375,9 @@
    4.31                let
    4.32                  val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
    4.33                  val dom' = map2 (fn d => fn S' => weakens d S' ~~ S') dom Ss';
    4.34 -              in weaken (constructor a dom' c0, c0) c end)
    4.35 +              in weaken (type_constructor a dom' c0, c0) c end)
    4.36            end
    4.37 -      | derive T S = weakens (variable T) S;
    4.38 +      | derive T S = weakens (type_variable T) S;
    4.39    in uncurry derive end;
    4.40  
    4.41