src/Pure/Isar/code.ML
changeset 25462 dad0291cb76a
parent 25312 eb9067371342
child 25485 33840a854e63
     1.1 --- a/src/Pure/Isar/code.ML	Fri Nov 23 21:09:34 2007 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Nov 23 21:09:35 2007 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4    val del_post: thm -> theory -> theory
     1.5    val add_datatype: (string * typ) list -> theory -> theory
     1.6    val add_datatype_cmd: string list -> theory -> theory
     1.7 +  val type_interpretation: (string * string list -> theory -> theory) -> theory -> theory
     1.8    val add_case: thm -> theory -> theory
     1.9    val add_undefined: string -> theory -> theory
    1.10  
    1.11 @@ -537,18 +538,15 @@
    1.12  fun aggregate f [] = NONE
    1.13    | aggregate f (x::xs) = SOME (aggr_neutr f x xs);
    1.14  
    1.15 -fun inter_sorts thy =
    1.16 -  let
    1.17 -    val algebra = Sign.classes_of thy;
    1.18 -    val inters = curry (Sorts.inter_sort algebra);
    1.19 -  in aggregate (map2 inters) end;
    1.20 +fun inter_sorts algebra =
    1.21 +  aggregate (map2 (curry (Sorts.inter_sort algebra)));
    1.22  
    1.23  fun specific_constraints thy (class, tyco) =
    1.24    let
    1.25      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
    1.26      val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
    1.27      val funcs = classparams
    1.28 -      |> map (fn c => Class.inst_const thy (c, tyco))
    1.29 +      |> map_filter (fn c => try (Class.inst_const thy) (c, tyco))
    1.30        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    1.31        |> (map o Option.map) (Susp.force o fst o snd)
    1.32        |> maps these
    1.33 @@ -558,37 +556,53 @@
    1.34      val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs;
    1.35    in sorts end;
    1.36  
    1.37 -fun weakest_constraints thy (class, tyco) =
    1.38 +fun weakest_constraints thy algebra (class, tyco) =
    1.39    let
    1.40 -    val all_superclasses = Sign.complete_sort thy [class];
    1.41 -  in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    1.42 +    val all_superclasses = Sorts.complete_sort algebra [class];
    1.43 +  in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    1.44     of SOME sorts => sorts
    1.45 -    | NONE => Sign.arity_sorts thy tyco [class]
    1.46 +    | NONE => Sorts.mg_domain algebra tyco [class]
    1.47    end;
    1.48  
    1.49 -fun strongest_constraints thy (class, tyco) =
    1.50 +fun strongest_constraints thy algebra (class, tyco) =
    1.51    let
    1.52 -    val algebra = Sign.classes_of thy;
    1.53      val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class];
    1.54      val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses;
    1.55 -  in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    1.56 +  in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    1.57     of SOME sorts => sorts
    1.58      | NONE => replicate
    1.59 -        (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
    1.60 +        (Sign.arity_number thy tyco) (Sorts.minimize_sort algebra (Sorts.all_classes algebra))
    1.61 +  end;
    1.62 +
    1.63 +fun get_algebra thy (class, tyco) =
    1.64 +  let
    1.65 +    val base_algebra = Sign.classes_of thy;
    1.66 +  in if can (Sorts.mg_domain base_algebra tyco) [class]
    1.67 +    then base_algebra
    1.68 +    else let
    1.69 +      val superclasses = Sorts.super_classes base_algebra class;
    1.70 +      val sorts = inter_sorts base_algebra
    1.71 +          (map_filter (fn class => try (Sorts.mg_domain base_algebra tyco) [class]) superclasses)
    1.72 +        |> the_default (replicate (Sign.arity_number thy tyco) [])
    1.73 +    in
    1.74 +      base_algebra
    1.75 +      |> Sorts.add_arities (Sign.pp thy) (tyco, [(class, sorts)])
    1.76 +    end
    1.77    end;
    1.78  
    1.79  fun gen_classparam_typ constr thy class (c, tyco) = 
    1.80    let
    1.81 +    val algebra = get_algebra thy (class, tyco);
    1.82      val cs = these (try (#params o AxClass.get_info thy) class);
    1.83 -    val ty = (the o AList.lookup (op =) cs) c;
    1.84 +    val SOME ty = AList.lookup (op =) cs c;
    1.85      val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
    1.86 -      (constr thy (class, tyco));
    1.87 +      (constr thy algebra (class, tyco));
    1.88      val ty_inst = Type (tyco, map TFree sort_args);
    1.89    in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
    1.90  
    1.91  fun retrieve_algebra thy operational =
    1.92    Sorts.subalgebra (Sign.pp thy) operational
    1.93 -    (weakest_constraints thy)
    1.94 +    (weakest_constraints thy (Sign.classes_of thy))
    1.95      (Sign.classes_of thy);
    1.96  
    1.97  in
    1.98 @@ -763,18 +777,22 @@
    1.99  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   1.100    (fn thm => Context.mapping (add_default_func thm) I));
   1.101  
   1.102 +structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =);
   1.103 +val type_interpretation = TypeInterpretation.interpretation;
   1.104 +
   1.105  fun add_datatype raw_cs thy =
   1.106    let
   1.107      val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
   1.108      val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
   1.109 -    val purge_cs = map fst (snd vs_cos);
   1.110 -    val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   1.111 -     of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
   1.112 +    val cs' = map fst (snd vs_cos);
   1.113 +    val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   1.114 +     of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos)
   1.115        | NONE => NONE;
   1.116    in
   1.117      thy
   1.118 -    |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos))
   1.119 +    |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos))
   1.120          #> map_funcs (fold (Symtab.delete_safe o fst) cs))
   1.121 +    |> TypeInterpretation.data (tyco, cs')
   1.122    end;
   1.123  
   1.124  fun add_datatype_cmd raw_cs thy =
   1.125 @@ -837,7 +855,8 @@
   1.126        add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
   1.127          || Scan.succeed (mk_attribute add))
   1.128    in
   1.129 -    add_del_attribute ("func", (add_func, del_func))
   1.130 +    TypeInterpretation.init
   1.131 +    #> add_del_attribute ("func", (add_func, del_func))
   1.132      #> add_del_attribute ("inline", (add_inline, del_inline))
   1.133      #> add_del_attribute ("post", (add_post, del_post))
   1.134    end);