simplified interpretation setup;
authorwenzelm
Tue Sep 25 15:34:35 2007 +0200 (2007-09-25)
changeset 24711e8bba7723858
parent 24710 141df8b68f63
child 24712 64ed05609568
simplified interpretation setup;
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/interpretation.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 25 13:42:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 25 15:34:35 2007 +0200
     1.3 @@ -486,8 +486,8 @@
     1.4        hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
     1.5    in
     1.6      thy
     1.7 -    |> DatatypePackage.add_interpretator datatype_hook
     1.8 -    |> TypecopyPackage.add_interpretator typecopy_hook
     1.9 +    |> DatatypePackage.interpretation datatype_hook
    1.10 +    |> TypecopyPackage.interpretation typecopy_hook
    1.11    end;
    1.12  
    1.13  fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
    1.14 @@ -604,8 +604,8 @@
    1.15  val setup = 
    1.16    add_codegen "datatype" datatype_codegen
    1.17    #> add_tycodegen "datatype" datatype_tycodegen
    1.18 -  #> DatatypePackage.add_interpretator (fold add_datatype_case_const)
    1.19 -  #> DatatypePackage.add_interpretator (fold add_datatype_case_defs)
    1.20 +  #> DatatypePackage.interpretation (fold add_datatype_case_const)
    1.21 +  #> DatatypePackage.interpretation (fold add_datatype_case_defs)
    1.22  
    1.23  val setup_hooks =
    1.24    add_codetypes_hook codetype_hook
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 25 13:42:59 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 25 15:34:35 2007 +0200
     2.3 @@ -65,7 +65,7 @@
     2.4    val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
     2.5    val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option
     2.6    val get_datatype_constrs : theory -> string -> (string * typ) list option
     2.7 -  val add_interpretator: (string list -> theory -> theory) -> theory -> theory
     2.8 +  val interpretation: (string list -> theory -> theory) -> theory -> theory
     2.9    val print_datatypes : theory -> unit
    2.10    val make_case :  Proof.context -> bool -> string list -> term ->
    2.11      (term * term) list -> term * (term * (int * bool)) list
    2.12 @@ -134,7 +134,7 @@
    2.13  
    2.14  fun get_datatype_descr thy dtco =
    2.15    get_datatype thy dtco
    2.16 -  |> Option.map (fn info as { descr, index, ... } => 
    2.17 +  |> Option.map (fn info as { descr, index, ... } =>
    2.18         (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
    2.19  
    2.20  fun get_datatype_spec thy dtco =
    2.21 @@ -210,7 +210,7 @@
    2.22  
    2.23  in
    2.24  
    2.25 -fun gen_induct_tac inst_tac (varss, opt_rule) i state = 
    2.26 +fun gen_induct_tac inst_tac (varss, opt_rule) i state =
    2.27    SUBGOAL (fn (Bi,_) =>
    2.28    let
    2.29      val (rule, rule_name) =
    2.30 @@ -219,7 +219,7 @@
    2.31          | NONE =>
    2.32              let val tn = find_tname (hd (map_filter I (flat varss))) Bi
    2.33                  val thy = Thm.theory_of_thm state
    2.34 -            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn) 
    2.35 +            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn)
    2.36              end
    2.37      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    2.38      val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    2.39 @@ -423,7 +423,7 @@
    2.40  
    2.41  fun add_case_tr' case_names thy =
    2.42    Theory.add_advanced_trfuns ([], [],
    2.43 -    map (fn case_name => 
    2.44 +    map (fn case_name =>
    2.45        let val case_name' = Sign.const_syntax_name thy case_name
    2.46        in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
    2.47        end) case_names, []) thy;
    2.48 @@ -519,9 +519,8 @@
    2.49  val specify_consts = gen_specify_consts Sign.add_consts_i;
    2.50  val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
    2.51  
    2.52 -structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string list; val eq = op = end);
    2.53 -
    2.54 -fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator (fold interpretator);
    2.55 +structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    2.56 +val interpretation = DatatypeInterpretation.interpretation;
    2.57  
    2.58  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    2.59      case_names_induct case_names_exhausts thy =
    2.60 @@ -641,7 +640,7 @@
    2.61        |> Theory.parent_path
    2.62        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    2.63        |> snd
    2.64 -      |> DatatypeInterpretator.add_those [map fst dt_infos];
    2.65 +      |> DatatypeInterpretation.data (map fst dt_infos);
    2.66    in
    2.67      ({distinct = distinct,
    2.68        inject = inject,
    2.69 @@ -698,7 +697,7 @@
    2.70        |> add_cases_induct dt_infos induct
    2.71        |> Theory.parent_path
    2.72        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    2.73 -      |> DatatypeInterpretator.add_those [map fst dt_infos];
    2.74 +      |> DatatypeInterpretation.data (map fst dt_infos);
    2.75    in
    2.76      ({distinct = distinct,
    2.77        inject = inject,
    2.78 @@ -799,7 +798,7 @@
    2.79        |> Theory.parent_path
    2.80        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    2.81        |> snd
    2.82 -      |> DatatypeInterpretator.add_those [map fst dt_infos];
    2.83 +      |> DatatypeInterpretation.data (map fst dt_infos);
    2.84    in
    2.85      ({distinct = distinct,
    2.86        inject = inject,
    2.87 @@ -902,7 +901,7 @@
    2.88    Method.add_methods tactic_emulations #>
    2.89    simproc_setup #>
    2.90    trfun_setup #>
    2.91 -  DatatypeInterpretator.init;
    2.92 +  DatatypeInterpretation.init;
    2.93  
    2.94  
    2.95  (* outer syntax *)
     3.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 13:42:59 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 15:34:35 2007 +0200
     3.3 @@ -228,6 +228,6 @@
     3.4      |> fold_rev (make_casedists (#sorts info)) infos
     3.5    end;
     3.6  
     3.7 -val setup = DatatypePackage.add_interpretator add_dt_realizers;
     3.8 +val setup = DatatypePackage.interpretation add_dt_realizers;
     3.9  
    3.10  end;
     4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 25 13:42:59 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 25 15:34:35 2007 +0200
     4.3 @@ -177,7 +177,7 @@
     4.4  
     4.5  val case_cong = fold add_case_cong
     4.6  
     4.7 -val setup_case_cong = DatatypePackage.add_interpretator case_cong
     4.8 +val setup_case_cong = DatatypePackage.interpretation case_cong
     4.9  
    4.10  
    4.11  
     5.1 --- a/src/HOL/Tools/function_package/size.ML	Tue Sep 25 13:42:59 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/size.ML	Tue Sep 25 15:34:35 2007 +0200
     5.3 @@ -204,6 +204,6 @@
     5.4  
     5.5  fun size_thms thy = the o Symtab.lookup (SizeData.get thy);
     5.6  
     5.7 -val setup = DatatypePackage.add_interpretator add_size_thms;
     5.8 +val setup = DatatypePackage.interpretation add_size_thms;
     5.9  
    5.10  end;
    5.11 \ No newline at end of file
     6.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 25 13:42:59 2007 +0200
     6.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 25 15:34:35 2007 +0200
     6.3 @@ -19,8 +19,7 @@
     6.4      -> theory -> (string * info) * theory
     6.5    val get_typecopies: theory -> string list
     6.6    val get_typecopy_info: theory -> string -> info option
     6.7 -  type interpretator = string * info -> theory -> theory
     6.8 -  val add_interpretator: interpretator -> theory -> theory
     6.9 +  val interpretation: (string * info -> theory -> theory) -> theory -> theory
    6.10    val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    6.11    val get_eq: theory -> string -> thm
    6.12    val print_typecopies: theory -> unit
    6.13 @@ -41,8 +40,6 @@
    6.14    proj_def: thm
    6.15  };
    6.16  
    6.17 -structure TypecopyInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
    6.18 -
    6.19  structure TypecopyData = TheoryDataFun
    6.20  (
    6.21    type T = info Symtab.table;
    6.22 @@ -71,12 +68,12 @@
    6.23  val get_typecopy_info = Symtab.lookup o TypecopyData.get;
    6.24  
    6.25  
    6.26 -(* interpretator management *)
    6.27 +(* interpretation *)
    6.28  
    6.29 -type interpretator = string * info -> theory -> theory;
    6.30 +structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
    6.31  
    6.32 -fun add_interpretator interp = TypecopyInterpretator.add_interpretator
    6.33 -  (fold (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy));
    6.34 +fun interpretation interp = TypecopyInterpretation.interpretation
    6.35 +  (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy);
    6.36  
    6.37  
    6.38  (* add a type copy *)
    6.39 @@ -108,7 +105,7 @@
    6.40          in
    6.41            thy
    6.42            |> (TypecopyData.map o Symtab.update_new) (tyco, info)
    6.43 -          |> TypecopyInterpretator.add_those [tyco]
    6.44 +          |> TypecopyInterpretation.data tyco
    6.45            |> pair (tyco, info)
    6.46          end
    6.47    in
    6.48 @@ -137,10 +134,10 @@
    6.49    in (vs, [(constr, [typ])]) end;
    6.50  
    6.51  
    6.52 -(* interpretator for projection function code *)
    6.53 +(* interpretation for projection function code *)
    6.54  
    6.55 -fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def;
    6.56 +fun add_project (_, {proj_def, ...} : info) = Code.add_default_func proj_def;
    6.57  
    6.58 -val setup = TypecopyInterpretator.init #> add_interpretator add_project;
    6.59 +val setup = TypecopyInterpretation.init #> interpretation add_project;
    6.60  
    6.61  end;
     7.1 --- a/src/Pure/interpretation.ML	Tue Sep 25 13:42:59 2007 +0200
     7.2 +++ b/src/Pure/interpretation.ML	Tue Sep 25 15:34:35 2007 +0200
     7.3 @@ -5,78 +5,47 @@
     7.4  Generic interpretation of theory data.
     7.5  *)
     7.6  
     7.7 -signature THEORY_INTERPRETATOR =
     7.8 +signature INTERPRETATION =
     7.9  sig
    7.10    type T
    7.11 -  type interpretator = T list -> theory -> theory
    7.12 -  val add_those: T list -> theory -> theory
    7.13 -  val all_those: theory -> T list
    7.14 -  val add_interpretator: interpretator -> theory -> theory
    7.15 +  val result: theory -> T list
    7.16 +  val interpretation: (T -> theory -> theory) -> theory -> theory
    7.17 +  val data: T -> theory -> theory
    7.18    val init: theory -> theory
    7.19  end;
    7.20  
    7.21 -signature THEORY_INTERPRETATOR_KEY =
    7.22 -sig
    7.23 -  type T
    7.24 -  val eq: T * T -> bool
    7.25 -end;
    7.26 -
    7.27 -functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
    7.28 +functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
    7.29  struct
    7.30  
    7.31 -open Key;
    7.32 -
    7.33 -type interpretator = T list -> theory -> theory;
    7.34 +type T = T;
    7.35  
    7.36 -fun apply ips x = fold_rev (fn (_, f) => f x) ips;
    7.37 -
    7.38 -structure InterpretatorData = TheoryDataFun
    7.39 +structure Interp = TheoryDataFun
    7.40  (
    7.41 -  type T = ((serial * interpretator) list * T list) * (theory -> theory) list;
    7.42 -  val empty = (([], []), []);
    7.43 +  type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
    7.44 +  val empty = ([], []);
    7.45    val extend = I;
    7.46    val copy = I;
    7.47 -  fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
    7.48 -    let
    7.49 -      fun diff (interpretators1 : (serial * interpretator) list, done1)
    7.50 -        (interpretators2, done2) = let
    7.51 -          val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
    7.52 -          val undone = subtract eq done2 done1;
    7.53 -        in if null interpretators then [] else [apply interpretators undone] end;
    7.54 -      val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
    7.55 -      val done = Library.merge eq (done1, done2);
    7.56 -      val upd_new = diff (interpretators2, done2) (interpretators1, done1)
    7.57 -        @ diff (interpretators1, done1) (interpretators2, done2);
    7.58 -      val upd = upd1 @ upd2 @ upd_new;
    7.59 -    in ((interpretators, done), upd) end;
    7.60 +  fun merge _ ((data1, interps1), (data2, interps2)) : T =
    7.61 +    (Library.merge eq (data1, data2),
    7.62 +     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
    7.63  );
    7.64  
    7.65 +val result = #1 o Interp.get;
    7.66 +
    7.67  fun consolidate thy =
    7.68 -  (case #2 (InterpretatorData.get thy) of
    7.69 -    [] => NONE
    7.70 -  | upd => SOME (thy |> Library.apply upd |> (InterpretatorData.map o apsnd) (K [])));
    7.71 +  let
    7.72 +    val (data, interps) = Interp.get thy;
    7.73 +    val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
    7.74 +    val finished = map (fn (interp, _) => (interp, data)) interps;
    7.75 +  in
    7.76 +    if forall (null o #2) unfinished then NONE
    7.77 +    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
    7.78 +  end;
    7.79 +
    7.80 +fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
    7.81 +fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
    7.82  
    7.83  val init = Theory.at_begin consolidate;
    7.84  
    7.85 -fun add_those xs thy =
    7.86 -  let
    7.87 -    val ((interpretators, _), _) = InterpretatorData.get thy;
    7.88 -  in
    7.89 -    thy
    7.90 -    |> apply interpretators xs
    7.91 -    |> (InterpretatorData.map o apfst o apsnd) (append xs)
    7.92 -  end;
    7.93 -
    7.94 -val all_those = snd o fst o InterpretatorData.get;
    7.95 -
    7.96 -fun add_interpretator interpretator thy =
    7.97 -  let
    7.98 -    val ((interpretators, xs), _) = InterpretatorData.get thy;
    7.99 -  in
   7.100 -    thy
   7.101 -    |> interpretator (rev xs)
   7.102 -    |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
   7.103 -  end;
   7.104 -
   7.105  end;
   7.106