1.1 --- a/src/HOL/Nominal/nominal.ML Sun Jun 21 23:04:37 2009 +0200
1.2 +++ b/src/HOL/Nominal/nominal.ML Mon Jun 22 08:00:46 2009 +0200
1.3 @@ -6,7 +6,7 @@
1.4
1.5 signature NOMINAL =
1.6 sig
1.7 - val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
1.8 + val add_nominal_datatype : Datatype.config -> string list ->
1.9 (string list * bstring * mixfix *
1.10 (bstring * string list * mixfix) list) list -> theory -> theory
1.11 type descr
1.12 @@ -2084,7 +2084,7 @@
1.13 val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
1.14 val specs = map (fn ((((_, vs), t), mx), cons) =>
1.15 (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
1.16 - in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
1.17 + in add_nominal_datatype Datatype.default_config names specs end;
1.18
1.19 val _ =
1.20 OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
2.1 --- a/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 23:04:37 2009 +0200
2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Mon Jun 22 08:00:46 2009 +0200
2.3 @@ -102,7 +102,7 @@
2.4 fold_map (fn ak => fn thy =>
2.5 let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
2.6 val ({inject,case_thms,...},thy1) = Datatype.add_datatype
2.7 - DatatypeAux.default_datatype_config [ak] [dt] thy
2.8 + Datatype.default_config [ak] [dt] thy
2.9 val inject_flat = flat inject
2.10 val ak_type = Type (Sign.intern_type thy1 ak,[])
2.11 val ak_sign = Sign.intern_const thy1 ak
3.1 --- a/src/HOL/Tools/datatype_package/datatype.ML Sun Jun 21 23:04:37 2009 +0200
3.2 +++ b/src/HOL/Tools/datatype_package/datatype.ML Mon Jun 22 08:00:46 2009 +0200
3.3 @@ -6,26 +6,7 @@
3.4
3.5 signature DATATYPE =
3.6 sig
3.7 - type datatype_config = DatatypeAux.datatype_config
3.8 - type datatype_info = DatatypeAux.datatype_info
3.9 - type descr = DatatypeAux.descr
3.10 - val get_datatypes : theory -> datatype_info Symtab.table
3.11 - val get_datatype : theory -> string -> datatype_info option
3.12 - val the_datatype : theory -> string -> datatype_info
3.13 - val datatype_of_constr : theory -> string -> datatype_info option
3.14 - val datatype_of_case : theory -> string -> datatype_info option
3.15 - val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
3.16 - val the_datatype_descr : theory -> string list
3.17 - -> descr * (string * sort) list * string list
3.18 - * (string list * string list) * (typ list * typ list)
3.19 - val get_datatype_constrs : theory -> string -> (string * typ) list option
3.20 - val distinct_simproc : simproc
3.21 - val make_case : Proof.context -> bool -> string list -> term ->
3.22 - (term * term) list -> term * (term * (int * bool)) list
3.23 - val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
3.24 - val read_typ: theory ->
3.25 - (typ list * (string * sort) list) * string -> typ list * (string * sort) list
3.26 - val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
3.27 + include DATATYPE_COMMON
3.28 type rules = {distinct : thm list list,
3.29 inject : thm list list,
3.30 exhaustion : thm list,
3.31 @@ -34,15 +15,31 @@
3.32 split_thms : (thm * thm) list,
3.33 induction : thm,
3.34 simps : thm list}
3.35 - val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
3.36 - -> string list option -> term list -> theory -> Proof.state;
3.37 + val add_datatype : config -> string list -> (string list * binding * mixfix *
3.38 + (binding * typ list * mixfix) list) list -> theory -> rules * theory
3.39 + val datatype_cmd : string list -> (string list * binding * mixfix *
3.40 + (binding * string list * mixfix) list) list -> theory -> theory
3.41 + val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
3.42 + -> string list option -> term list -> theory -> Proof.state
3.43 val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
3.44 - val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
3.45 - (binding * typ list * mixfix) list) list -> theory -> rules * theory
3.46 - val add_datatype_cmd : string list -> (string list * binding * mixfix *
3.47 - (binding * string list * mixfix) list) list -> theory -> rules * theory
3.48 + val get_datatypes : theory -> info Symtab.table
3.49 + val get_datatype : theory -> string -> info option
3.50 + val the_datatype : theory -> string -> info
3.51 + val datatype_of_constr : theory -> string -> info option
3.52 + val datatype_of_case : theory -> string -> info option
3.53 + val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
3.54 + val the_datatype_descr : theory -> string list
3.55 + -> descr * (string * sort) list * string list
3.56 + * (string list * string list) * (typ list * typ list)
3.57 + val get_datatype_constrs : theory -> string -> (string * typ) list option
3.58 + val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
3.59 + val distinct_simproc : simproc
3.60 + val make_case : Proof.context -> bool -> string list -> term ->
3.61 + (term * term) list -> term * (term * (int * bool)) list
3.62 + val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
3.63 + val read_typ: theory ->
3.64 + (typ list * (string * sort) list) * string -> typ list * (string * sort) list
3.65 val setup: theory -> theory
3.66 - val print_datatypes : theory -> unit
3.67 end;
3.68
3.69 structure Datatype : DATATYPE =
3.70 @@ -56,9 +53,9 @@
3.71 structure DatatypesData = TheoryDataFun
3.72 (
3.73 type T =
3.74 - {types: datatype_info Symtab.table,
3.75 - constrs: datatype_info Symtab.table,
3.76 - cases: datatype_info Symtab.table};
3.77 + {types: info Symtab.table,
3.78 + constrs: info Symtab.table,
3.79 + cases: info Symtab.table};
3.80
3.81 val empty =
3.82 {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
3.83 @@ -75,14 +72,10 @@
3.84 val get_datatypes = #types o DatatypesData.get;
3.85 val map_datatypes = DatatypesData.map;
3.86
3.87 -fun print_datatypes thy =
3.88 - Pretty.writeln (Pretty.strs ("datatypes:" ::
3.89 - map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
3.90 -
3.91
3.92 (** theory information about datatypes **)
3.93
3.94 -fun put_dt_infos (dt_infos : (string * datatype_info) list) =
3.95 +fun put_dt_infos (dt_infos : (string * info) list) =
3.96 map_datatypes (fn {types, constrs, cases} =>
3.97 {types = fold Symtab.update dt_infos types,
3.98 constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
3.99 @@ -207,7 +200,7 @@
3.100 let
3.101 val inducts = ProjectRule.projections (ProofContext.init thy) induction;
3.102
3.103 - fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
3.104 + fun named_rules (name, {index, exhaustion, ...}: info) =
3.105 [((Binding.empty, nth inducts index), [Induct.induct_type name]),
3.106 ((Binding.empty, exhaustion), [Induct.cases_type name])];
3.107 fun unnamed_rule i =
3.108 @@ -351,13 +344,13 @@
3.109 simps : thm list}
3.110
3.111 structure DatatypeInterpretation = InterpretationFun
3.112 - (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
3.113 + (type T = config * string list val eq: T * T -> bool = eq_snd op =);
3.114 fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
3.115
3.116
3.117 (******************* definitional introduction of datatypes *******************)
3.118
3.119 -fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.120 +fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.121 case_names_induct case_names_exhausts thy =
3.122 let
3.123 val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
3.124 @@ -414,7 +407,7 @@
3.125
3.126 (*********************** declare existing type as datatype *********************)
3.127
3.128 -fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
3.129 +fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
3.130 let
3.131 val ((_, [induct']), _) =
3.132 Variable.importT_thms [induct] (Variable.thm_context induct);
3.133 @@ -487,7 +480,7 @@
3.134 simps = simps}, thy11)
3.135 end;
3.136
3.137 -fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
3.138 +fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
3.139 let
3.140 fun constr_of_term (Const (c, T)) = (c, T)
3.141 | constr_of_term t =
3.142 @@ -553,13 +546,13 @@
3.143 end;
3.144
3.145 val rep_datatype = gen_rep_datatype Sign.cert_term;
3.146 -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
3.147 +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
3.148
3.149
3.150
3.151 (******************************** add datatype ********************************)
3.152
3.153 -fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
3.154 +fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
3.155 let
3.156 val _ = Theory.requires thy "Datatype" "datatype definitions";
3.157
3.158 @@ -627,12 +620,12 @@
3.159 val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
3.160 in
3.161 add_datatype_def
3.162 - (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.163 + (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.164 case_names_induct case_names_exhausts thy
3.165 end;
3.166
3.167 val add_datatype = gen_add_datatype cert_typ;
3.168 -val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
3.169 +val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
3.170
3.171
3.172
3.173 @@ -649,23 +642,29 @@
3.174
3.175 (* outer syntax *)
3.176
3.177 -local structure P = OuterParse and K = OuterKeyword in
3.178 +local
3.179
3.180 -val datatype_decl =
3.181 - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
3.182 - (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
3.183 +structure P = OuterParse and K = OuterKeyword
3.184
3.185 -fun mk_datatype args =
3.186 +fun prep_datatype_decls args =
3.187 let
3.188 val names = map
3.189 (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
3.190 val specs = map (fn ((((_, vs), t), mx), cons) =>
3.191 (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
3.192 - in snd o add_datatype_cmd names specs end;
3.193 + in (names, specs) end;
3.194 +
3.195 +val parse_datatype_decl =
3.196 + (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
3.197 + (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
3.198 +
3.199 +val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
3.200 +
3.201 +in
3.202
3.203 val _ =
3.204 OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
3.205 - (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
3.206 + (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
3.207
3.208 val _ =
3.209 OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
4.1 --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 23:04:37 2009 +0200
4.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Mon Jun 22 08:00:46 2009 +0200
4.3 @@ -14,24 +14,22 @@
4.4
4.5 signature DATATYPE_ABS_PROOFS =
4.6 sig
4.7 - type datatype_config = DatatypeAux.datatype_config
4.8 - type descr = DatatypeAux.descr
4.9 - type datatype_info = DatatypeAux.datatype_info
4.10 - val prove_casedist_thms : datatype_config -> string list ->
4.11 + include DATATYPE_COMMON
4.12 + val prove_casedist_thms : config -> string list ->
4.13 descr list -> (string * sort) list -> thm ->
4.14 attribute list -> theory -> thm list * theory
4.15 - val prove_primrec_thms : datatype_config -> string list ->
4.16 + val prove_primrec_thms : config -> string list ->
4.17 descr list -> (string * sort) list ->
4.18 - datatype_info Symtab.table -> thm list list -> thm list list ->
4.19 + info Symtab.table -> thm list list -> thm list list ->
4.20 simpset -> thm -> theory -> (string list * thm list) * theory
4.21 - val prove_case_thms : datatype_config -> string list ->
4.22 + val prove_case_thms : config -> string list ->
4.23 descr list -> (string * sort) list ->
4.24 string list -> thm list -> theory -> (thm list list * string list) * theory
4.25 - val prove_split_thms : datatype_config -> string list ->
4.26 + val prove_split_thms : config -> string list ->
4.27 descr list -> (string * sort) list ->
4.28 thm list list -> thm list list -> thm list -> thm list list -> theory ->
4.29 (thm * thm) list * theory
4.30 - val prove_nchotomys : datatype_config -> string list -> descr list ->
4.31 + val prove_nchotomys : config -> string list -> descr list ->
4.32 (string * sort) list -> thm list -> theory -> thm list * theory
4.33 val prove_weak_case_congs : string list -> descr list ->
4.34 (string * sort) list -> theory -> thm list * theory
4.35 @@ -47,7 +45,7 @@
4.36
4.37 (************************ case distinction theorems ***************************)
4.38
4.39 -fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
4.40 +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
4.41 let
4.42 val _ = message config "Proving case distinction theorems ...";
4.43
4.44 @@ -89,8 +87,8 @@
4.45
4.46 (*************************** primrec combinators ******************************)
4.47
4.48 -fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
4.49 - (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
4.50 +fun prove_primrec_thms (config : config) new_type_names descr sorts
4.51 + (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
4.52 let
4.53 val _ = message config "Constructing primrec combinators ...";
4.54
4.55 @@ -275,7 +273,7 @@
4.56
4.57 (***************************** case combinators *******************************)
4.58
4.59 -fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
4.60 +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
4.61 let
4.62 val _ = message config "Proving characteristic theorems for case combinators ...";
4.63
4.64 @@ -349,7 +347,7 @@
4.65
4.66 (******************************* case splitting *******************************)
4.67
4.68 -fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
4.69 +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
4.70 casedist_thms case_thms thy =
4.71 let
4.72 val _ = message config "Proving equations for case splitting ...";
4.73 @@ -398,7 +396,7 @@
4.74
4.75 (************************* additional theorems for TFL ************************)
4.76
4.77 -fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
4.78 +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
4.79 let
4.80 val _ = message config "Proving additional theorems for TFL ...";
4.81
5.1 --- a/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 23:04:37 2009 +0200
5.2 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Mon Jun 22 08:00:46 2009 +0200
5.3 @@ -4,11 +4,23 @@
5.4 Auxiliary functions for defining datatypes.
5.5 *)
5.6
5.7 +signature DATATYPE_COMMON =
5.8 +sig
5.9 + type config
5.10 + val default_config : config
5.11 + datatype dtyp =
5.12 + DtTFree of string
5.13 + | DtType of string * (dtyp list)
5.14 + | DtRec of int;
5.15 + type descr
5.16 + type info
5.17 +end
5.18 +
5.19 signature DATATYPE_AUX =
5.20 sig
5.21 - type datatype_config
5.22 - val default_datatype_config : datatype_config
5.23 - val message : datatype_config -> string -> unit
5.24 + include DATATYPE_COMMON
5.25 +
5.26 + val message : config -> string -> unit
5.27
5.28 val add_path : bool -> string -> theory -> theory
5.29 val parent_path : bool -> theory -> theory
5.30 @@ -33,12 +45,6 @@
5.31 datatype simproc_dist = FewConstrs of thm list
5.32 | ManyConstrs of thm * simpset;
5.33
5.34 - datatype dtyp =
5.35 - DtTFree of string
5.36 - | DtType of string * (dtyp list)
5.37 - | DtRec of int;
5.38 - type descr
5.39 - type datatype_info
5.40
5.41 exception Datatype
5.42 exception Datatype_Empty of string
5.43 @@ -61,7 +67,7 @@
5.44 -> ((string * Term.typ list) * (string * 'a list) list) list
5.45 val check_nonempty : descr list -> unit
5.46 val unfold_datatypes :
5.47 - theory -> descr -> (string * sort) list -> datatype_info Symtab.table ->
5.48 + theory -> descr -> (string * sort) list -> info Symtab.table ->
5.49 descr -> int -> descr list * int
5.50 end;
5.51
5.52 @@ -70,10 +76,10 @@
5.53
5.54 (* datatype option flags *)
5.55
5.56 -type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
5.57 -val default_datatype_config : datatype_config =
5.58 +type config = { strict: bool, flat_names: bool, quiet: bool };
5.59 +val default_config : config =
5.60 { strict = true, flat_names = false, quiet = false };
5.61 -fun message ({ quiet, ...} : datatype_config) s =
5.62 +fun message ({ quiet, ...} : config) s =
5.63 if quiet then () else writeln s;
5.64
5.65 fun add_path flat_names s = if flat_names then I else Sign.add_path s;
5.66 @@ -186,7 +192,7 @@
5.67 (* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
5.68 type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
5.69
5.70 -type datatype_info =
5.71 +type info =
5.72 {index : int,
5.73 alt_names : string list option,
5.74 descr : descr,
5.75 @@ -317,7 +323,7 @@
5.76 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
5.77 (* need to be unfolded *)
5.78
5.79 -fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
5.80 +fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i =
5.81 let
5.82 fun typ_error T msg = error ("Non-admissible type expression\n" ^
5.83 Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
6.1 --- a/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 23:04:37 2009 +0200
6.2 +++ b/src/HOL/Tools/datatype_package/datatype_case.ML Mon Jun 22 08:00:46 2009 +0200
6.3 @@ -7,16 +7,16 @@
6.4
6.5 signature DATATYPE_CASE =
6.6 sig
6.7 - val make_case: (string -> DatatypeAux.datatype_info option) ->
6.8 + val make_case: (string -> DatatypeAux.info option) ->
6.9 Proof.context -> bool -> string list -> term -> (term * term) list ->
6.10 term * (term * (int * bool)) list
6.11 - val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
6.12 + val dest_case: (string -> DatatypeAux.info option) -> bool ->
6.13 string list -> term -> (term * (term * term) list) option
6.14 - val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
6.15 + val strip_case: (string -> DatatypeAux.info option) -> bool ->
6.16 term -> (term * (term * term) list) option
6.17 - val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
6.18 + val case_tr: bool -> (theory -> string -> DatatypeAux.info option)
6.19 -> Proof.context -> term list -> term
6.20 - val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
6.21 + val case_tr': (theory -> string -> DatatypeAux.info option) ->
6.22 string -> Proof.context -> term list -> term
6.23 end;
6.24
6.25 @@ -31,7 +31,7 @@
6.26 * Get information about datatypes
6.27 *---------------------------------------------------------------------------*)
6.28
6.29 -fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
6.30 +fun ty_info (tab : string -> DatatypeAux.info option) s =
6.31 case tab s of
6.32 SOME {descr, case_name, index, sorts, ...} =>
6.33 let
7.1 --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 23:04:37 2009 +0200
7.2 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Mon Jun 22 08:00:46 2009 +0200
7.3 @@ -6,7 +6,7 @@
7.4
7.5 signature DATATYPE_CODEGEN =
7.6 sig
7.7 - val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
7.8 + val find_shortest_path: Datatype.descr -> int -> (string * int) option
7.9 val mk_eq_eqns: theory -> string -> (thm * bool) list
7.10 val mk_case_cert: theory -> string -> thm
7.11 val setup: theory -> theory
7.12 @@ -17,7 +17,7 @@
7.13
7.14 (** find shortest path to constructor with no recursive arguments **)
7.15
7.16 -fun find_nonempty (descr: DatatypeAux.descr) is i =
7.17 +fun find_nonempty (descr: Datatype.descr) is i =
7.18 let
7.19 val (_, _, constrs) = the (AList.lookup (op =) descr i);
7.20 fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
7.21 @@ -42,7 +42,7 @@
7.22
7.23 (* datatype definition *)
7.24
7.25 -fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
7.26 +fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
7.27 let
7.28 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
7.29 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
8.1 --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 23:04:37 2009 +0200
8.2 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Mon Jun 22 08:00:46 2009 +0200
8.3 @@ -7,7 +7,7 @@
8.4
8.5 signature DATATYPE_REALIZER =
8.6 sig
8.7 - val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
8.8 + val add_dt_realizers: Datatype.config -> string list -> theory -> theory
8.9 val setup: theory -> theory
8.10 end;
8.11
8.12 @@ -38,7 +38,7 @@
8.13
8.14 fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
8.15
8.16 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
8.17 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
8.18 let
8.19 val recTs = get_rec_types descr sorts;
8.20 val pnames = if length descr = 1 then ["P"]
8.21 @@ -157,7 +157,7 @@
8.22 in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
8.23
8.24
8.25 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
8.26 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
8.27 let
8.28 val cert = cterm_of thy;
8.29 val rT = TFree ("'P", HOLogic.typeS);
9.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 23:04:37 2009 +0200
9.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Mon Jun 22 08:00:46 2009 +0200
9.3 @@ -11,12 +11,10 @@
9.4
9.5 signature DATATYPE_REP_PROOFS =
9.6 sig
9.7 - type datatype_config = DatatypeAux.datatype_config
9.8 - type descr = DatatypeAux.descr
9.9 - type datatype_info = DatatypeAux.datatype_info
9.10 + include DATATYPE_COMMON
9.11 val distinctness_limit : int Config.T
9.12 val distinctness_limit_setup : theory -> theory
9.13 - val representation_proofs : datatype_config -> datatype_info Symtab.table ->
9.14 + val representation_proofs : config -> info Symtab.table ->
9.15 string list -> descr list -> (string * sort) list ->
9.16 (binding * mixfix) list -> (binding * mixfix) list list -> attribute
9.17 -> theory -> (thm list list * thm list list * thm list list *
9.18 @@ -43,12 +41,12 @@
9.19 val myinv_f_f = thm "myinv_f_f";
9.20
9.21
9.22 -fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
9.23 +fun exh_thm_of (dt_info : info Symtab.table) tname =
9.24 #exhaustion (the (Symtab.lookup dt_info tname));
9.25
9.26 (******************************************************************************)
9.27
9.28 -fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
9.29 +fun representation_proofs (config : config) (dt_info : info Symtab.table)
9.30 new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
9.31 let
9.32 val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
10.1 --- a/src/HOL/Tools/function_package/size.ML Sun Jun 21 23:04:37 2009 +0200
10.2 +++ b/src/HOL/Tools/function_package/size.ML Mon Jun 22 08:00:46 2009 +0200
10.3 @@ -57,7 +57,7 @@
10.4
10.5 val app = curry (list_comb o swap);
10.6
10.7 -fun prove_size_thms (info : datatype_info) new_type_names thy =
10.8 +fun prove_size_thms (info : info) new_type_names thy =
10.9 let
10.10 val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
10.11 val l = length new_type_names;
11.1 --- a/src/HOL/Tools/hologic.ML Sun Jun 21 23:04:37 2009 +0200
11.2 +++ b/src/HOL/Tools/hologic.ML Mon Jun 22 08:00:46 2009 +0200
11.3 @@ -603,8 +603,11 @@
11.4
11.5 val typerepT = Type ("Typerep.typerep", []);
11.6
11.7 -fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
11.8 - Term.itselfT T --> typerepT) $ Logic.mk_type T;
11.9 +fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
11.10 + literalT --> listT typerepT --> typerepT) $ mk_literal tyco
11.11 + $ mk_list typerepT (map mk_typerep Ts)
11.12 + | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
11.13 + Term.itselfT T --> typerepT) $ Logic.mk_type T;
11.14
11.15 val termT = Type ("Code_Eval.term", []);
11.16
12.1 --- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 23:04:37 2009 +0200
12.2 +++ b/src/HOL/Tools/old_primrec.ML Mon Jun 22 08:00:46 2009 +0200
12.3 @@ -221,7 +221,7 @@
12.4
12.5 (* find datatypes which contain all datatypes in tnames' *)
12.6
12.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
12.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
12.9 | find_dts dt_info tnames' (tname::tnames) =
12.10 (case Symtab.lookup dt_info tname of
12.11 NONE => primrec_err (quote tname ^ " is not a datatype")
12.12 @@ -230,7 +230,7 @@
12.13 (tname, dt)::(find_dts dt_info tnames' tnames)
12.14 else find_dts dt_info tnames' tnames);
12.15
12.16 -fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
12.17 +fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
12.18 let
12.19 fun constrs_of (_, (_, _, cs)) =
12.20 map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
13.1 --- a/src/HOL/Tools/primrec.ML Sun Jun 21 23:04:37 2009 +0200
13.2 +++ b/src/HOL/Tools/primrec.ML Mon Jun 22 08:00:46 2009 +0200
13.3 @@ -203,7 +203,7 @@
13.4
13.5 (* find datatypes which contain all datatypes in tnames' *)
13.6
13.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
13.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
13.9 | find_dts dt_info tnames' (tname::tnames) =
13.10 (case Symtab.lookup dt_info tname of
13.11 NONE => primrec_error (quote tname ^ " is not a datatype")
14.1 --- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 23:04:37 2009 +0200
14.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Mon Jun 22 08:00:46 2009 +0200
14.3 @@ -12,10 +12,10 @@
14.4 -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
14.5 val ensure_random_typecopy: string -> theory -> theory
14.6 val random_aux_specification: string -> term list -> local_theory -> local_theory
14.7 - val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
14.8 + val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
14.9 -> string list -> string list * string list -> typ list * typ list
14.10 -> string * (term list * (term * term) list)
14.11 - val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
14.12 + val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
14.13 val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
14.14 val setup: theory -> theory
14.15 end;
14.16 @@ -362,16 +362,20 @@
14.17 val algebra = Sign.classes_of thy;
14.18 val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
14.19 Datatype.the_datatype_descr thy raw_tycos;
14.20 + val typrep_vs = (map o apsnd)
14.21 + (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
14.22 val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
14.23 - (DatatypeAux.interpret_construction descr raw_vs { atyp = single, dtyp = (K o K o K) [] });
14.24 + (DatatypeAux.interpret_construction descr typrep_vs
14.25 + { atyp = single, dtyp = (K o K o K) [] });
14.26 val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
14.27 - (DatatypeAux.interpret_construction descr raw_vs { atyp = K [], dtyp = K o K });
14.28 + (DatatypeAux.interpret_construction descr typrep_vs
14.29 + { atyp = K [], dtyp = K o K });
14.30 val has_inst = exists (fn tyco =>
14.31 can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
14.32 in if has_inst then thy
14.33 - else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
14.34 + else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
14.35 of SOME constrain => mk_random_datatype config descr
14.36 - (map constrain raw_vs) tycos (names, auxnames)
14.37 + (map constrain typrep_vs) tycos (names, auxnames)
14.38 ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
14.39 | NONE => thy
14.40 end;
15.1 --- a/src/HOL/Tools/refute.ML Sun Jun 21 23:04:37 2009 +0200
15.2 +++ b/src/HOL/Tools/refute.ML Mon Jun 22 08:00:46 2009 +0200
15.3 @@ -73,7 +73,7 @@
15.4 val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
15.5 val string_of_typ : Term.typ -> string
15.6 val typ_of_dtyp :
15.7 - DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp
15.8 + Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
15.9 -> Term.typ
15.10 end; (* signature REFUTE *)
15.11
15.12 @@ -411,15 +411,6 @@
15.13 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
15.14 (* ------------------------------------------------------------------------- *)
15.15
15.16 -(* ------------------------------------------------------------------------- *)
15.17 -(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *)
15.18 -(* ('Term.typ'), given type parameters for the data type's type *)
15.19 -(* arguments *)
15.20 -(* ------------------------------------------------------------------------- *)
15.21 -
15.22 - (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list ->
15.23 - DatatypeAux.dtyp -> Term.typ *)
15.24 -
15.25 fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
15.26 (* replace a 'DtTFree' variable by the associated type *)
15.27 the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
15.28 @@ -1660,10 +1651,6 @@
15.29 (* their arguments) of the size of the argument types *)
15.30 (* ------------------------------------------------------------------------- *)
15.31
15.32 - (* theory -> (Term.typ * int) list -> DatatypeAux.descr ->
15.33 - (DatatypeAux.dtyp * Term.typ) list ->
15.34 - (string * DatatypeAux.dtyp list) list -> int *)
15.35 -
15.36 fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
15.37 sum (map (fn (_, dtyps) =>
15.38 product (map (size_of_type thy (typ_sizes, []) o
15.39 @@ -2144,7 +2131,6 @@
15.40 (* decrement depth for the IDT 'T' *)
15.41 val typs' = (case AList.lookup (op =) typs T of NONE => typs
15.42 | SOME n => AList.update (op =) (T, n-1) typs)
15.43 - (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *)
15.44 fun constructor_terms terms [] = terms
15.45 | constructor_terms terms (d::ds) =
15.46 let
15.47 @@ -2241,7 +2227,6 @@
15.48 else ()
15.49 (* returns an interpretation where everything is mapped to *)
15.50 (* an "undefined" element of the datatype *)
15.51 - (* DatatypeAux.dtyp list -> interpretation *)
15.52 fun make_undef [] =
15.53 Leaf (replicate total False)
15.54 | make_undef (d::ds) =
15.55 @@ -2253,7 +2238,6 @@
15.56 Node (replicate size (make_undef ds))
15.57 end
15.58 (* returns the interpretation for a constructor *)
15.59 - (* int * DatatypeAux.dtyp list -> int * interpretation *)
15.60 fun make_constr (offset, []) =
15.61 if offset<total then
15.62 (offset+1, Leaf ((replicate offset False) @ True ::
15.63 @@ -2421,9 +2405,6 @@
15.64 (* mutually recursive types must have the same type *)
15.65 (* parameters, unless the mutual recursion comes from *)
15.66 (* indirect recursion *)
15.67 - (* (DatatypeAux.dtyp * Term.typ) list ->
15.68 - (DatatypeAux.dtyp * Term.typ) list ->
15.69 - (DatatypeAux.dtyp * Term.typ) list *)
15.70 fun rec_typ_assoc acc [] =
15.71 acc
15.72 | rec_typ_assoc acc ((d, T)::xs) =
15.73 @@ -2458,7 +2439,6 @@
15.74 else
15.75 raise REFUTE ("IDT_recursion_interpreter",
15.76 "different type associations for the same dtyp"))
15.77 - (* (DatatypeAux.dtyp * Term.typ) list *)
15.78 val typ_assoc = filter
15.79 (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
15.80 (rec_typ_assoc []
15.81 @@ -2613,7 +2593,6 @@
15.82 val rec_dtyps_args = List.filter
15.83 (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
15.84 (* map those indices to interpretations *)
15.85 - (* (DatatypeAux.dtyp * interpretation) list *)
15.86 val rec_dtyps_intrs = map (fn (dtyp, arg) =>
15.87 let
15.88 val dT = typ_of_dtyp descr typ_assoc dtyp
15.89 @@ -2625,8 +2604,6 @@
15.90 (* takes the dtyp and interpretation of an element, *)
15.91 (* and computes the interpretation for the *)
15.92 (* corresponding recursive argument *)
15.93 - (* DatatypeAux.dtyp -> interpretation ->
15.94 - interpretation *)
15.95 fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
15.96 (* recursive argument is "rec_i params elem" *)
15.97 compute_array_entry i (find_index_eq True xs)
15.98 @@ -3252,8 +3229,6 @@
15.99 (* constructor generates the datatype's element that is given by *)
15.100 (* 'element', returns the constructor (as a term) as well as the *)
15.101 (* indices of the arguments *)
15.102 - (* string * DatatypeAux.dtyp list ->
15.103 - (Term.term * int list) option *)
15.104 fun get_constr_args (cname, cargs) =
15.105 let
15.106 val cTerm = Const (cname,
15.107 @@ -3281,7 +3256,6 @@
15.108 in
15.109 Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
15.110 end
15.111 - (* Term.term * DatatypeAux.dtyp list * int list *)
15.112 val (cTerm, cargs, args) =
15.113 (* we could speed things up by computing the correct *)
15.114 (* constructor directly (rather than testing all *)
16.1 --- a/src/HOL/Tools/typecopy.ML Sun Jun 21 23:04:37 2009 +0200
16.2 +++ b/src/HOL/Tools/typecopy.ML Mon Jun 22 08:00:46 2009 +0200
16.3 @@ -6,21 +6,13 @@
16.4
16.5 signature TYPECOPY =
16.6 sig
16.7 - type info = {
16.8 - vs: (string * sort) list,
16.9 - constr: string,
16.10 - typ: typ,
16.11 - inject: thm,
16.12 - proj: string * typ,
16.13 - proj_def: thm
16.14 - }
16.15 + type info = { vs: (string * sort) list, constr: string, typ: typ,
16.16 + inject: thm, proj: string * typ, proj_def: thm }
16.17 val typecopy: binding * string list -> typ -> (binding * binding) option
16.18 -> theory -> (string * info) * theory
16.19 - val get_typecopies: theory -> string list
16.20 val get_info: theory -> string -> info option
16.21 val interpretation: (string -> theory -> theory) -> theory -> theory
16.22 val add_default_code: string -> theory -> theory
16.23 - val print_typecopies: theory -> unit
16.24 val setup: theory -> theory
16.25 end;
16.26
16.27 @@ -47,22 +39,6 @@
16.28 fun merge _ = Symtab.merge (K true);
16.29 );
16.30
16.31 -fun print_typecopies thy =
16.32 - let
16.33 - val tab = TypecopyData.get thy;
16.34 - fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
16.35 - (Pretty.block o Pretty.breaks) [
16.36 - Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
16.37 - Pretty.str "=",
16.38 - (Pretty.str o Sign.extern_const thy) constr,
16.39 - Syntax.pretty_typ_global thy typ,
16.40 - Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]];
16.41 - in
16.42 - (Pretty.writeln o Pretty.block o Pretty.fbreaks)
16.43 - (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
16.44 - end;
16.45 -
16.46 -val get_typecopies = Symtab.keys o TypecopyData.get;
16.47 val get_info = Symtab.lookup o TypecopyData.get;
16.48
16.49
16.50 @@ -72,7 +48,7 @@
16.51 val interpretation = TypecopyInterpretation.interpretation;
16.52
16.53
16.54 -(* declaring typecopies *)
16.55 +(* introducing typecopies *)
16.56
16.57 fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
16.58 let
17.1 --- a/src/HOL/Tools/typedef.ML Sun Jun 21 23:04:37 2009 +0200
17.2 +++ b/src/HOL/Tools/typedef.ML Mon Jun 22 08:00:46 2009 +0200
17.3 @@ -12,13 +12,13 @@
17.4 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
17.5 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
17.6 Rep_induct: thm, Abs_induct: thm}
17.7 - val get_info: theory -> string -> info option
17.8 val add_typedef: bool -> binding option -> binding * string list * mixfix ->
17.9 term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
17.10 val typedef: (bool * binding) * (binding * string list * mixfix) * term
17.11 * (binding * binding) option -> theory -> Proof.state
17.12 val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
17.13 * (binding * binding) option -> theory -> Proof.state
17.14 + val get_info: theory -> string -> info option
17.15 val interpretation: (string -> theory -> theory) -> theory -> theory
17.16 val setup: theory -> theory
17.17 end;
18.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Sun Jun 21 23:04:37 2009 +0200
18.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 22 08:00:46 2009 +0200
18.3 @@ -25,20 +25,6 @@
18.4 "~~/src/HOL/ex/Records"
18.5 begin
18.6
18.7 -(*temporary Haskell workaround*)
18.8 -declare typerep_fun_def [code inline]
18.9 -declare typerep_prod_def [code inline]
18.10 -declare typerep_sum_def [code inline]
18.11 -declare typerep_cpoint_ext_type_def [code inline]
18.12 -declare typerep_itself_def [code inline]
18.13 -declare typerep_list_def [code inline]
18.14 -declare typerep_option_def [code inline]
18.15 -declare typerep_point_ext_type_def [code inline]
18.16 -declare typerep_point'_ext_type_def [code inline]
18.17 -declare typerep_point''_ext_type_def [code inline]
18.18 -declare typerep_pol_def [code inline]
18.19 -declare typerep_polex_def [code inline]
18.20 -
18.21 (*avoid popular infixes*)
18.22 code_reserved SML union inter upto
18.23
19.1 --- a/src/HOLCF/Fixrec.thy Sun Jun 21 23:04:37 2009 +0200
19.2 +++ b/src/HOLCF/Fixrec.thy Mon Jun 22 08:00:46 2009 +0200
19.3 @@ -6,7 +6,7 @@
19.4
19.5 theory Fixrec
19.6 imports Sprod Ssum Up One Tr Fix
19.7 -uses ("Tools/fixrec_package.ML")
19.8 +uses ("Tools/fixrec.ML")
19.9 begin
19.10
19.11 subsection {* Maybe monad type *}
19.12 @@ -599,12 +599,12 @@
19.13
19.14 subsection {* Initializing the fixrec package *}
19.15
19.16 -use "Tools/fixrec_package.ML"
19.17 +use "Tools/fixrec.ML"
19.18
19.19 -setup {* FixrecPackage.setup *}
19.20 +setup {* Fixrec.setup *}
19.21
19.22 setup {*
19.23 - FixrecPackage.add_matchers
19.24 + Fixrec.add_matchers
19.25 [ (@{const_name up}, @{const_name match_up}),
19.26 (@{const_name sinl}, @{const_name match_sinl}),
19.27 (@{const_name sinr}, @{const_name match_sinr}),
20.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 23:04:37 2009 +0200
20.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Mon Jun 22 08:00:46 2009 +0200
20.3 @@ -6,7 +6,7 @@
20.4
20.5 theory Abstraction
20.6 imports LiveIOA
20.7 -uses ("ioa_package.ML")
20.8 +uses ("ioa.ML")
20.9 begin
20.10
20.11 defaultsort type
20.12 @@ -613,6 +613,6 @@
20.13
20.14 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
20.15
20.16 -use "ioa_package.ML"
20.17 +use "ioa.ML"
20.18
20.19 end
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOLCF/IOA/meta_theory/ioa.ML Mon Jun 22 08:00:46 2009 +0200
21.3 @@ -0,0 +1,536 @@
21.4 +(* Title: HOLCF/IOA/meta_theory/ioa.ML
21.5 + Author: Tobias Hamberger, TU Muenchen
21.6 +*)
21.7 +
21.8 +signature IOA =
21.9 +sig
21.10 + val add_ioa: string -> string
21.11 + -> (string) list -> (string) list -> (string) list
21.12 + -> (string * string) list -> string
21.13 + -> (string * string * (string * string)list) list
21.14 + -> theory -> theory
21.15 + val add_composition : string -> (string)list -> theory -> theory
21.16 + val add_hiding : string -> string -> (string)list -> theory -> theory
21.17 + val add_restriction : string -> string -> (string)list -> theory -> theory
21.18 + val add_rename : string -> string -> string -> theory -> theory
21.19 +end;
21.20 +
21.21 +structure Ioa: IOA =
21.22 +struct
21.23 +
21.24 +val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
21.25 +val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
21.26 +
21.27 +exception malformed;
21.28 +
21.29 +(* stripping quotes *)
21.30 +fun strip [] = [] |
21.31 +strip ("\""::r) = strip r |
21.32 +strip (a::r) = a :: (strip r);
21.33 +fun strip_quote s = implode(strip(explode(s)));
21.34 +
21.35 +(* used by *_of_varlist *)
21.36 +fun extract_first (a,b) = strip_quote a;
21.37 +fun extract_second (a,b) = strip_quote b;
21.38 +(* following functions producing sth from a varlist *)
21.39 +fun comma_list_of_varlist [] = "" |
21.40 +comma_list_of_varlist [a] = extract_first a |
21.41 +comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
21.42 +fun primed_comma_list_of_varlist [] = "" |
21.43 +primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
21.44 +primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
21.45 + (primed_comma_list_of_varlist r);
21.46 +fun type_product_of_varlist [] = "" |
21.47 +type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
21.48 +type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
21.49 +
21.50 +(* listing a list *)
21.51 +fun list_elements_of [] = "" |
21.52 +list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
21.53 +
21.54 +(* extracting type parameters from a type list *)
21.55 +(* fun param_tupel thy [] res = res |
21.56 +param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
21.57 +param_tupel thy ((TFree(a,_))::r) res =
21.58 +if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
21.59 +param_tupel thy (a::r) res =
21.60 +error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
21.61 +*)
21.62 +
21.63 +(* used by constr_list *)
21.64 +fun extract_constrs thy [] = [] |
21.65 +extract_constrs thy (a::r) =
21.66 +let
21.67 +fun delete_bold [] = []
21.68 +| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
21.69 + then (let val (_::_::_::s) = xs in delete_bold s end)
21.70 + else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
21.71 + then (let val (_::_::_::s) = xs in delete_bold s end)
21.72 + else (x::delete_bold xs));
21.73 +fun delete_bold_string s = implode(delete_bold(explode s));
21.74 +(* from a constructor term in *.induct (with quantifiers,
21.75 +"Trueprop" and ?P stripped away) delivers the head *)
21.76 +fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
21.77 +extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
21.78 +extract_hd (Var(_,_) $ r) = extract_hd r |
21.79 +extract_hd (a $ b) = extract_hd a |
21.80 +extract_hd (Const(s,_)) = s |
21.81 +extract_hd _ = raise malformed;
21.82 +(* delivers constructor term string from a prem of *.induct *)
21.83 +fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
21.84 +extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
21.85 +extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) |
21.86 +extract_constr _ _ = raise malformed;
21.87 +in
21.88 +(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
21.89 +end;
21.90 +
21.91 +(* delivering list of constructor terms of a datatype *)
21.92 +fun constr_list thy atyp =
21.93 +let
21.94 +fun act_name thy (Type(s,_)) = s |
21.95 +act_name _ s =
21.96 +error("malformed action type: " ^ (string_of_typ thy s));
21.97 +fun afpl ("." :: a) = [] |
21.98 +afpl [] = [] |
21.99 +afpl (a::r) = a :: (afpl r);
21.100 +fun unqualify s = implode(rev(afpl(rev(explode s))));
21.101 +val q_atypstr = act_name thy atyp;
21.102 +val uq_atypstr = unqualify q_atypstr;
21.103 +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
21.104 +in
21.105 +extract_constrs thy prem
21.106 +handle malformed =>
21.107 +error("malformed theorem : " ^ uq_atypstr ^ ".induct")
21.108 +end;
21.109 +
21.110 +fun check_for_constr thy atyp (a $ b) =
21.111 +let
21.112 +fun all_free (Free(_,_)) = true |
21.113 +all_free (a $ b) = if (all_free a) then (all_free b) else false |
21.114 +all_free _ = false;
21.115 +in
21.116 +if (all_free b) then (check_for_constr thy atyp a) else false
21.117 +end |
21.118 +check_for_constr thy atyp (Const(a,_)) =
21.119 +let
21.120 +val cl = constr_list thy atyp;
21.121 +fun fstmem a [] = false |
21.122 +fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
21.123 +in
21.124 +if (fstmem a cl) then true else false
21.125 +end |
21.126 +check_for_constr _ _ _ = false;
21.127 +
21.128 +(* delivering the free variables of a constructor term *)
21.129 +fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
21.130 +free_vars_of (Const(_,_)) = [] |
21.131 +free_vars_of (Free(a,_)) = [a] |
21.132 +free_vars_of _ = raise malformed;
21.133 +
21.134 +(* making a constructor set from a constructor term (of signature) *)
21.135 +fun constr_set_string thy atyp ctstr =
21.136 +let
21.137 +val trm = OldGoals.simple_read_term thy atyp ctstr;
21.138 +val l = free_vars_of trm
21.139 +in
21.140 +if (check_for_constr thy atyp trm) then
21.141 +(if (l=[]) then ("{" ^ ctstr ^ "}")
21.142 +else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
21.143 +else (raise malformed)
21.144 +handle malformed =>
21.145 +error("malformed action term: " ^ (string_of_term thy trm))
21.146 +end;
21.147 +
21.148 +(* extracting constructor heads *)
21.149 +fun constructor_head thy atypstr s =
21.150 +let
21.151 +fun hd_of (Const(a,_)) = a |
21.152 +hd_of (t $ _) = hd_of t |
21.153 +hd_of _ = raise malformed;
21.154 +val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
21.155 +in
21.156 +hd_of trm handle malformed =>
21.157 +error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
21.158 +end;
21.159 +fun constructor_head_list _ _ [] = [] |
21.160 +constructor_head_list thy atypstr (a::r) =
21.161 + (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
21.162 +
21.163 +(* producing an action set *)
21.164 +(*FIXME*)
21.165 +fun action_set_string thy atyp [] = "Set.empty" |
21.166 +action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
21.167 +action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
21.168 + " Un " ^ (action_set_string thy atyp r);
21.169 +
21.170 +(* used by extend *)
21.171 +fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
21.172 +pstr s ((a,b)::r) =
21.173 +if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
21.174 +fun poststring [] l = "" |
21.175 +poststring [(a,b)] l = pstr a l |
21.176 +poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
21.177 +
21.178 +(* extends a (action string,condition,assignlist) tupel by a
21.179 +(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list
21.180 +(where bool indicates whether there is a precondition *)
21.181 +fun extend thy atyp statetupel (actstr,r,[]) =
21.182 +let
21.183 +val trm = OldGoals.simple_read_term thy atyp actstr;
21.184 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
21.185 +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
21.186 +in
21.187 +if (check_for_constr thy atyp trm)
21.188 +then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
21.189 +else
21.190 +error("transition " ^ actstr ^ " is not a pure constructor term")
21.191 +end |
21.192 +extend thy atyp statetupel (actstr,r,(a,b)::c) =
21.193 +let
21.194 +fun pseudo_poststring [] = "" |
21.195 +pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
21.196 +pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
21.197 +val trm = OldGoals.simple_read_term thy atyp actstr;
21.198 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
21.199 +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
21.200 +in
21.201 +if (check_for_constr thy atyp trm) then
21.202 +(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
21.203 +(* the case with transrel *)
21.204 + else
21.205 + (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
21.206 + "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
21.207 +else
21.208 +error("transition " ^ actstr ^ " is not a pure constructor term")
21.209 +end;
21.210 +(* used by make_alt_string *)
21.211 +fun extended_list _ _ _ [] = [] |
21.212 +extended_list thy atyp statetupel (a::r) =
21.213 + (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
21.214 +
21.215 +(* used by write_alts *)
21.216 +fun write_alt thy (chead,tr) inp out int [] =
21.217 +if (chead mem inp) then
21.218 +(
21.219 +error("Input action " ^ tr ^ " was not specified")
21.220 +) else (
21.221 +if (chead mem (out@int)) then
21.222 +(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
21.223 +(tr ^ " => False",tr ^ " => False")) |
21.224 +write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
21.225 +let
21.226 +fun hd_of (Const(a,_)) = a |
21.227 +hd_of (t $ _) = hd_of t |
21.228 +hd_of _ = raise malformed;
21.229 +fun occurs_again c [] = false |
21.230 +occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
21.231 +in
21.232 +if (chead=(hd_of a)) then
21.233 +(if ((chead mem inp) andalso e) then (
21.234 +error("Input action " ^ b ^ " has a precondition")
21.235 +) else (if (chead mem (inp@out@int)) then
21.236 + (if (occurs_again chead r) then (
21.237 +error("Two specifications for action: " ^ b)
21.238 + ) else (b ^ " => " ^ c,b ^ " => " ^ d))
21.239 + else (
21.240 +error("Action " ^ b ^ " is not in automaton signature")
21.241 +))) else (write_alt thy (chead,ctrm) inp out int r)
21.242 +handle malformed =>
21.243 +error ("malformed action term: " ^ (string_of_term thy a))
21.244 +end;
21.245 +
21.246 +(* used by make_alt_string *)
21.247 +fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
21.248 +write_alts thy (a,b) inp out int [c] ttr =
21.249 +let
21.250 +val wa = write_alt thy c inp out int ttr
21.251 +in
21.252 + (a ^ (fst wa),b ^ (snd wa))
21.253 +end |
21.254 +write_alts thy (a,b) inp out int (c::r) ttr =
21.255 +let
21.256 +val wa = write_alt thy c inp out int ttr
21.257 +in
21.258 + write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
21.259 +end;
21.260 +
21.261 +fun make_alt_string thy inp out int atyp statetupel trans =
21.262 +let
21.263 +val cl = constr_list thy atyp;
21.264 +val ttr = extended_list thy atyp statetupel trans;
21.265 +in
21.266 +write_alts thy ("","") inp out int cl ttr
21.267 +end;
21.268 +
21.269 +(* used in add_ioa *)
21.270 +fun check_free_primed (Free(a,_)) =
21.271 +let
21.272 +val (f::r) = rev(explode a)
21.273 +in
21.274 +if (f="'") then [a] else []
21.275 +end |
21.276 +check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
21.277 +check_free_primed (Abs(_,_,t)) = check_free_primed t |
21.278 +check_free_primed _ = [];
21.279 +
21.280 +fun overlap [] _ = true |
21.281 +overlap (a::r) l = if (a mem l) then (
21.282 +error("Two occurences of action " ^ a ^ " in automaton signature")
21.283 +) else (overlap r l);
21.284 +
21.285 +(* delivering some types of an automaton *)
21.286 +fun aut_type_of thy aut_name =
21.287 +let
21.288 +fun left_of (( _ $ left) $ _) = left |
21.289 +left_of _ = raise malformed;
21.290 +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
21.291 +in
21.292 +(#T(rep_cterm(cterm_of thy (left_of aut_def))))
21.293 +handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
21.294 +end;
21.295 +
21.296 +fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
21.297 +act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
21.298 +(string_of_typ thy t));
21.299 +fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
21.300 +st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
21.301 +(string_of_typ thy t));
21.302 +
21.303 +fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
21.304 +comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
21.305 +comp_st_type_of _ _ = error "empty automaton list";
21.306 +
21.307 +(* checking consistency of action types (for composition) *)
21.308 +fun check_ac thy (a::r) =
21.309 +let
21.310 +fun ch_f_a thy acttyp [] = acttyp |
21.311 +ch_f_a thy acttyp (a::r) =
21.312 +let
21.313 +val auttyp = aut_type_of thy a;
21.314 +val ac = (act_type_of thy auttyp);
21.315 +in
21.316 +if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
21.317 +end;
21.318 +val auttyp = aut_type_of thy a;
21.319 +val acttyp = (act_type_of thy auttyp);
21.320 +in
21.321 +ch_f_a thy acttyp r
21.322 +end |
21.323 +check_ac _ [] = error "empty automaton list";
21.324 +
21.325 +fun clist [] = "" |
21.326 +clist [a] = a |
21.327 +clist (a::r) = a ^ " || " ^ (clist r);
21.328 +
21.329 +val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
21.330 +
21.331 +
21.332 +(* add_ioa *)
21.333 +
21.334 +fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
21.335 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
21.336 +let
21.337 +val state_type_string = type_product_of_varlist(statetupel);
21.338 +val styp = Syntax.read_typ_global thy state_type_string;
21.339 +val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
21.340 +val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
21.341 +val atyp = Syntax.read_typ_global thy action_type;
21.342 +val inp_set_string = action_set_string thy atyp inp;
21.343 +val out_set_string = action_set_string thy atyp out;
21.344 +val int_set_string = action_set_string thy atyp int;
21.345 +val inp_head_list = constructor_head_list thy action_type inp;
21.346 +val out_head_list = constructor_head_list thy action_type out;
21.347 +val int_head_list = constructor_head_list thy action_type int;
21.348 +val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int));
21.349 +val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list
21.350 + atyp statetupel trans;
21.351 +val thy2 = (thy
21.352 +|> Sign.add_consts
21.353 +[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
21.354 +(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
21.355 +(Binding.name (automaton_name ^ "_trans"),
21.356 + "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
21.357 +(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
21.358 +|> add_defs
21.359 +[(automaton_name ^ "_initial_def",
21.360 +automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
21.361 +(automaton_name ^ "_asig_def",
21.362 +automaton_name ^ "_asig == (" ^
21.363 + inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
21.364 +(automaton_name ^ "_trans_def",
21.365 +automaton_name ^ "_trans == {(" ^
21.366 + state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
21.367 +"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
21.368 +(automaton_name ^ "_def",
21.369 +automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
21.370 +"_initial, " ^ automaton_name ^ "_trans,{},{})")
21.371 +])
21.372 +val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
21.373 +( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
21.374 +in
21.375 +(
21.376 +if (chk_prime_list = []) then thy2
21.377 +else (
21.378 +error("Precondition or assignment terms in postconditions contain following primed variables:\n"
21.379 + ^ (list_elements_of chk_prime_list)))
21.380 +)
21.381 +end)
21.382 +
21.383 +fun add_composition automaton_name aut_list thy =
21.384 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
21.385 +let
21.386 +val acttyp = check_ac thy aut_list;
21.387 +val st_typ = comp_st_type_of thy aut_list;
21.388 +val comp_list = clist aut_list;
21.389 +in
21.390 +thy
21.391 +|> Sign.add_consts_i
21.392 +[(Binding.name automaton_name,
21.393 +Type("*",
21.394 +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
21.395 + Type("*",[Type("set",[st_typ]),
21.396 + Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
21.397 + Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
21.398 +,NoSyn)]
21.399 +|> add_defs
21.400 +[(automaton_name ^ "_def",
21.401 +automaton_name ^ " == " ^ comp_list)]
21.402 +end)
21.403 +
21.404 +fun add_restriction automaton_name aut_source actlist thy =
21.405 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
21.406 +let
21.407 +val auttyp = aut_type_of thy aut_source;
21.408 +val acttyp = act_type_of thy auttyp;
21.409 +val rest_set = action_set_string thy acttyp actlist
21.410 +in
21.411 +thy
21.412 +|> Sign.add_consts_i
21.413 +[(Binding.name automaton_name, auttyp,NoSyn)]
21.414 +|> add_defs
21.415 +[(automaton_name ^ "_def",
21.416 +automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
21.417 +end)
21.418 +fun add_hiding automaton_name aut_source actlist thy =
21.419 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
21.420 +let
21.421 +val auttyp = aut_type_of thy aut_source;
21.422 +val acttyp = act_type_of thy auttyp;
21.423 +val hid_set = action_set_string thy acttyp actlist
21.424 +in
21.425 +thy
21.426 +|> Sign.add_consts_i
21.427 +[(Binding.name automaton_name, auttyp,NoSyn)]
21.428 +|> add_defs
21.429 +[(automaton_name ^ "_def",
21.430 +automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
21.431 +end)
21.432 +
21.433 +fun ren_act_type_of thy funct =
21.434 + (case Term.fastype_of (Syntax.read_term_global thy funct) of
21.435 + Type ("fun", [a, b]) => a
21.436 + | _ => error "could not extract argument type of renaming function term");
21.437 +
21.438 +fun add_rename automaton_name aut_source fun_name thy =
21.439 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
21.440 +let
21.441 +val auttyp = aut_type_of thy aut_source;
21.442 +val st_typ = st_type_of thy auttyp;
21.443 +val acttyp = ren_act_type_of thy fun_name
21.444 +in
21.445 +thy
21.446 +|> Sign.add_consts_i
21.447 +[(Binding.name automaton_name,
21.448 +Type("*",
21.449 +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
21.450 + Type("*",[Type("set",[st_typ]),
21.451 + Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
21.452 + Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
21.453 +,NoSyn)]
21.454 +|> add_defs
21.455 +[(automaton_name ^ "_def",
21.456 +automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
21.457 +end)
21.458 +
21.459 +
21.460 +(** outer syntax **)
21.461 +
21.462 +(* prepare results *)
21.463 +
21.464 +(*encoding transition specifications with a element of ParseTrans*)
21.465 +datatype ParseTrans = Rel of string | PP of string*(string*string)list;
21.466 +fun mk_trans_of_rel s = Rel(s);
21.467 +fun mk_trans_of_prepost (s,l) = PP(s,l);
21.468 +
21.469 +fun trans_of (a, Rel b) = (a, b, [("", "")])
21.470 + | trans_of (a, PP (b, l)) = (a, b, l);
21.471 +
21.472 +
21.473 +fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
21.474 + add_ioa aut action_type inp out int states initial (map trans_of trans);
21.475 +
21.476 +fun mk_composition_decl (aut, autlist) =
21.477 + add_composition aut autlist;
21.478 +
21.479 +fun mk_hiding_decl (aut, (actlist, source_aut)) =
21.480 + add_hiding aut source_aut actlist;
21.481 +
21.482 +fun mk_restriction_decl (aut, (source_aut, actlist)) =
21.483 + add_restriction aut source_aut actlist;
21.484 +
21.485 +fun mk_rename_decl (aut, (source_aut, rename_f)) =
21.486 + add_rename aut source_aut rename_f;
21.487 +
21.488 +
21.489 +(* outer syntax *)
21.490 +
21.491 +local structure P = OuterParse and K = OuterKeyword in
21.492 +
21.493 +val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
21.494 + "outputs", "internals", "states", "initially", "transitions", "pre",
21.495 + "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
21.496 + "rename"];
21.497 +
21.498 +val actionlist = P.list1 P.term;
21.499 +val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
21.500 +val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
21.501 +val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
21.502 +val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
21.503 +val initial = P.$$$ "initially" |-- P.!!! P.term;
21.504 +val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
21.505 +val pre = P.$$$ "pre" |-- P.!!! P.term;
21.506 +val post = P.$$$ "post" |-- P.!!! assign_list;
21.507 +val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
21.508 +val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
21.509 +val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
21.510 +val transition = P.term -- (transrel || pre1 || post1);
21.511 +val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
21.512 +
21.513 +val ioa_decl =
21.514 + (P.name -- (P.$$$ "=" |--
21.515 + (P.$$$ "signature" |--
21.516 + P.!!! (P.$$$ "actions" |--
21.517 + (P.typ --
21.518 + (Scan.optional inputslist []) --
21.519 + (Scan.optional outputslist []) --
21.520 + (Scan.optional internalslist []) --
21.521 + stateslist --
21.522 + (Scan.optional initial "True") --
21.523 + translist))))) >> mk_ioa_decl ||
21.524 + (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
21.525 + >> mk_composition_decl ||
21.526 + (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
21.527 + P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
21.528 + (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
21.529 + P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
21.530 + (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
21.531 + >> mk_rename_decl;
21.532 +
21.533 +val _ =
21.534 + OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
21.535 + (ioa_decl >> Toplevel.theory);
21.536 +
21.537 +end;
21.538 +
21.539 +end;
22.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 23:04:37 2009 +0200
22.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
22.3 @@ -1,537 +0,0 @@
22.4 -(* Title: HOLCF/IOA/meta_theory/ioa_package.ML
22.5 - ID: $Id$
22.6 - Author: Tobias Hamberger, TU Muenchen
22.7 -*)
22.8 -
22.9 -signature IOA_PACKAGE =
22.10 -sig
22.11 - val add_ioa: string -> string
22.12 - -> (string) list -> (string) list -> (string) list
22.13 - -> (string * string) list -> string
22.14 - -> (string * string * (string * string)list) list
22.15 - -> theory -> theory
22.16 - val add_composition : string -> (string)list -> theory -> theory
22.17 - val add_hiding : string -> string -> (string)list -> theory -> theory
22.18 - val add_restriction : string -> string -> (string)list -> theory -> theory
22.19 - val add_rename : string -> string -> string -> theory -> theory
22.20 -end;
22.21 -
22.22 -structure IoaPackage: IOA_PACKAGE =
22.23 -struct
22.24 -
22.25 -val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
22.26 -val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
22.27 -
22.28 -exception malformed;
22.29 -
22.30 -(* stripping quotes *)
22.31 -fun strip [] = [] |
22.32 -strip ("\""::r) = strip r |
22.33 -strip (a::r) = a :: (strip r);
22.34 -fun strip_quote s = implode(strip(explode(s)));
22.35 -
22.36 -(* used by *_of_varlist *)
22.37 -fun extract_first (a,b) = strip_quote a;
22.38 -fun extract_second (a,b) = strip_quote b;
22.39 -(* following functions producing sth from a varlist *)
22.40 -fun comma_list_of_varlist [] = "" |
22.41 -comma_list_of_varlist [a] = extract_first a |
22.42 -comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
22.43 -fun primed_comma_list_of_varlist [] = "" |
22.44 -primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
22.45 -primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
22.46 - (primed_comma_list_of_varlist r);
22.47 -fun type_product_of_varlist [] = "" |
22.48 -type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
22.49 -type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
22.50 -
22.51 -(* listing a list *)
22.52 -fun list_elements_of [] = "" |
22.53 -list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
22.54 -
22.55 -(* extracting type parameters from a type list *)
22.56 -(* fun param_tupel thy [] res = res |
22.57 -param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
22.58 -param_tupel thy ((TFree(a,_))::r) res =
22.59 -if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
22.60 -param_tupel thy (a::r) res =
22.61 -error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
22.62 -*)
22.63 -
22.64 -(* used by constr_list *)
22.65 -fun extract_constrs thy [] = [] |
22.66 -extract_constrs thy (a::r) =
22.67 -let
22.68 -fun delete_bold [] = []
22.69 -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
22.70 - then (let val (_::_::_::s) = xs in delete_bold s end)
22.71 - else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
22.72 - then (let val (_::_::_::s) = xs in delete_bold s end)
22.73 - else (x::delete_bold xs));
22.74 -fun delete_bold_string s = implode(delete_bold(explode s));
22.75 -(* from a constructor term in *.induct (with quantifiers,
22.76 -"Trueprop" and ?P stripped away) delivers the head *)
22.77 -fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
22.78 -extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
22.79 -extract_hd (Var(_,_) $ r) = extract_hd r |
22.80 -extract_hd (a $ b) = extract_hd a |
22.81 -extract_hd (Const(s,_)) = s |
22.82 -extract_hd _ = raise malformed;
22.83 -(* delivers constructor term string from a prem of *.induct *)
22.84 -fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
22.85 -extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
22.86 -extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) |
22.87 -extract_constr _ _ = raise malformed;
22.88 -in
22.89 -(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
22.90 -end;
22.91 -
22.92 -(* delivering list of constructor terms of a datatype *)
22.93 -fun constr_list thy atyp =
22.94 -let
22.95 -fun act_name thy (Type(s,_)) = s |
22.96 -act_name _ s =
22.97 -error("malformed action type: " ^ (string_of_typ thy s));
22.98 -fun afpl ("." :: a) = [] |
22.99 -afpl [] = [] |
22.100 -afpl (a::r) = a :: (afpl r);
22.101 -fun unqualify s = implode(rev(afpl(rev(explode s))));
22.102 -val q_atypstr = act_name thy atyp;
22.103 -val uq_atypstr = unqualify q_atypstr;
22.104 -val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
22.105 -in
22.106 -extract_constrs thy prem
22.107 -handle malformed =>
22.108 -error("malformed theorem : " ^ uq_atypstr ^ ".induct")
22.109 -end;
22.110 -
22.111 -fun check_for_constr thy atyp (a $ b) =
22.112 -let
22.113 -fun all_free (Free(_,_)) = true |
22.114 -all_free (a $ b) = if (all_free a) then (all_free b) else false |
22.115 -all_free _ = false;
22.116 -in
22.117 -if (all_free b) then (check_for_constr thy atyp a) else false
22.118 -end |
22.119 -check_for_constr thy atyp (Const(a,_)) =
22.120 -let
22.121 -val cl = constr_list thy atyp;
22.122 -fun fstmem a [] = false |
22.123 -fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
22.124 -in
22.125 -if (fstmem a cl) then true else false
22.126 -end |
22.127 -check_for_constr _ _ _ = false;
22.128 -
22.129 -(* delivering the free variables of a constructor term *)
22.130 -fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
22.131 -free_vars_of (Const(_,_)) = [] |
22.132 -free_vars_of (Free(a,_)) = [a] |
22.133 -free_vars_of _ = raise malformed;
22.134 -
22.135 -(* making a constructor set from a constructor term (of signature) *)
22.136 -fun constr_set_string thy atyp ctstr =
22.137 -let
22.138 -val trm = OldGoals.simple_read_term thy atyp ctstr;
22.139 -val l = free_vars_of trm
22.140 -in
22.141 -if (check_for_constr thy atyp trm) then
22.142 -(if (l=[]) then ("{" ^ ctstr ^ "}")
22.143 -else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
22.144 -else (raise malformed)
22.145 -handle malformed =>
22.146 -error("malformed action term: " ^ (string_of_term thy trm))
22.147 -end;
22.148 -
22.149 -(* extracting constructor heads *)
22.150 -fun constructor_head thy atypstr s =
22.151 -let
22.152 -fun hd_of (Const(a,_)) = a |
22.153 -hd_of (t $ _) = hd_of t |
22.154 -hd_of _ = raise malformed;
22.155 -val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
22.156 -in
22.157 -hd_of trm handle malformed =>
22.158 -error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
22.159 -end;
22.160 -fun constructor_head_list _ _ [] = [] |
22.161 -constructor_head_list thy atypstr (a::r) =
22.162 - (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
22.163 -
22.164 -(* producing an action set *)
22.165 -(*FIXME*)
22.166 -fun action_set_string thy atyp [] = "Set.empty" |
22.167 -action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
22.168 -action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
22.169 - " Un " ^ (action_set_string thy atyp r);
22.170 -
22.171 -(* used by extend *)
22.172 -fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
22.173 -pstr s ((a,b)::r) =
22.174 -if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
22.175 -fun poststring [] l = "" |
22.176 -poststring [(a,b)] l = pstr a l |
22.177 -poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
22.178 -
22.179 -(* extends a (action string,condition,assignlist) tupel by a
22.180 -(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list
22.181 -(where bool indicates whether there is a precondition *)
22.182 -fun extend thy atyp statetupel (actstr,r,[]) =
22.183 -let
22.184 -val trm = OldGoals.simple_read_term thy atyp actstr;
22.185 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
22.186 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
22.187 -in
22.188 -if (check_for_constr thy atyp trm)
22.189 -then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
22.190 -else
22.191 -error("transition " ^ actstr ^ " is not a pure constructor term")
22.192 -end |
22.193 -extend thy atyp statetupel (actstr,r,(a,b)::c) =
22.194 -let
22.195 -fun pseudo_poststring [] = "" |
22.196 -pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
22.197 -pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
22.198 -val trm = OldGoals.simple_read_term thy atyp actstr;
22.199 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
22.200 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
22.201 -in
22.202 -if (check_for_constr thy atyp trm) then
22.203 -(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
22.204 -(* the case with transrel *)
22.205 - else
22.206 - (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
22.207 - "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
22.208 -else
22.209 -error("transition " ^ actstr ^ " is not a pure constructor term")
22.210 -end;
22.211 -(* used by make_alt_string *)
22.212 -fun extended_list _ _ _ [] = [] |
22.213 -extended_list thy atyp statetupel (a::r) =
22.214 - (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
22.215 -
22.216 -(* used by write_alts *)
22.217 -fun write_alt thy (chead,tr) inp out int [] =
22.218 -if (chead mem inp) then
22.219 -(
22.220 -error("Input action " ^ tr ^ " was not specified")
22.221 -) else (
22.222 -if (chead mem (out@int)) then
22.223 -(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
22.224 -(tr ^ " => False",tr ^ " => False")) |
22.225 -write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
22.226 -let
22.227 -fun hd_of (Const(a,_)) = a |
22.228 -hd_of (t $ _) = hd_of t |
22.229 -hd_of _ = raise malformed;
22.230 -fun occurs_again c [] = false |
22.231 -occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
22.232 -in
22.233 -if (chead=(hd_of a)) then
22.234 -(if ((chead mem inp) andalso e) then (
22.235 -error("Input action " ^ b ^ " has a precondition")
22.236 -) else (if (chead mem (inp@out@int)) then
22.237 - (if (occurs_again chead r) then (
22.238 -error("Two specifications for action: " ^ b)
22.239 - ) else (b ^ " => " ^ c,b ^ " => " ^ d))
22.240 - else (
22.241 -error("Action " ^ b ^ " is not in automaton signature")
22.242 -))) else (write_alt thy (chead,ctrm) inp out int r)
22.243 -handle malformed =>
22.244 -error ("malformed action term: " ^ (string_of_term thy a))
22.245 -end;
22.246 -
22.247 -(* used by make_alt_string *)
22.248 -fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
22.249 -write_alts thy (a,b) inp out int [c] ttr =
22.250 -let
22.251 -val wa = write_alt thy c inp out int ttr
22.252 -in
22.253 - (a ^ (fst wa),b ^ (snd wa))
22.254 -end |
22.255 -write_alts thy (a,b) inp out int (c::r) ttr =
22.256 -let
22.257 -val wa = write_alt thy c inp out int ttr
22.258 -in
22.259 - write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
22.260 -end;
22.261 -
22.262 -fun make_alt_string thy inp out int atyp statetupel trans =
22.263 -let
22.264 -val cl = constr_list thy atyp;
22.265 -val ttr = extended_list thy atyp statetupel trans;
22.266 -in
22.267 -write_alts thy ("","") inp out int cl ttr
22.268 -end;
22.269 -
22.270 -(* used in add_ioa *)
22.271 -fun check_free_primed (Free(a,_)) =
22.272 -let
22.273 -val (f::r) = rev(explode a)
22.274 -in
22.275 -if (f="'") then [a] else []
22.276 -end |
22.277 -check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
22.278 -check_free_primed (Abs(_,_,t)) = check_free_primed t |
22.279 -check_free_primed _ = [];
22.280 -
22.281 -fun overlap [] _ = true |
22.282 -overlap (a::r) l = if (a mem l) then (
22.283 -error("Two occurences of action " ^ a ^ " in automaton signature")
22.284 -) else (overlap r l);
22.285 -
22.286 -(* delivering some types of an automaton *)
22.287 -fun aut_type_of thy aut_name =
22.288 -let
22.289 -fun left_of (( _ $ left) $ _) = left |
22.290 -left_of _ = raise malformed;
22.291 -val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
22.292 -in
22.293 -(#T(rep_cterm(cterm_of thy (left_of aut_def))))
22.294 -handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
22.295 -end;
22.296 -
22.297 -fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
22.298 -act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
22.299 -(string_of_typ thy t));
22.300 -fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
22.301 -st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
22.302 -(string_of_typ thy t));
22.303 -
22.304 -fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
22.305 -comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
22.306 -comp_st_type_of _ _ = error "empty automaton list";
22.307 -
22.308 -(* checking consistency of action types (for composition) *)
22.309 -fun check_ac thy (a::r) =
22.310 -let
22.311 -fun ch_f_a thy acttyp [] = acttyp |
22.312 -ch_f_a thy acttyp (a::r) =
22.313 -let
22.314 -val auttyp = aut_type_of thy a;
22.315 -val ac = (act_type_of thy auttyp);
22.316 -in
22.317 -if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
22.318 -end;
22.319 -val auttyp = aut_type_of thy a;
22.320 -val acttyp = (act_type_of thy auttyp);
22.321 -in
22.322 -ch_f_a thy acttyp r
22.323 -end |
22.324 -check_ac _ [] = error "empty automaton list";
22.325 -
22.326 -fun clist [] = "" |
22.327 -clist [a] = a |
22.328 -clist (a::r) = a ^ " || " ^ (clist r);
22.329 -
22.330 -val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
22.331 -
22.332 -
22.333 -(* add_ioa *)
22.334 -
22.335 -fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
22.336 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
22.337 -let
22.338 -val state_type_string = type_product_of_varlist(statetupel);
22.339 -val styp = Syntax.read_typ_global thy state_type_string;
22.340 -val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
22.341 -val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
22.342 -val atyp = Syntax.read_typ_global thy action_type;
22.343 -val inp_set_string = action_set_string thy atyp inp;
22.344 -val out_set_string = action_set_string thy atyp out;
22.345 -val int_set_string = action_set_string thy atyp int;
22.346 -val inp_head_list = constructor_head_list thy action_type inp;
22.347 -val out_head_list = constructor_head_list thy action_type out;
22.348 -val int_head_list = constructor_head_list thy action_type int;
22.349 -val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int));
22.350 -val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list
22.351 - atyp statetupel trans;
22.352 -val thy2 = (thy
22.353 -|> Sign.add_consts
22.354 -[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
22.355 -(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
22.356 -(Binding.name (automaton_name ^ "_trans"),
22.357 - "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
22.358 -(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
22.359 -|> add_defs
22.360 -[(automaton_name ^ "_initial_def",
22.361 -automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
22.362 -(automaton_name ^ "_asig_def",
22.363 -automaton_name ^ "_asig == (" ^
22.364 - inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
22.365 -(automaton_name ^ "_trans_def",
22.366 -automaton_name ^ "_trans == {(" ^
22.367 - state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
22.368 -"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
22.369 -(automaton_name ^ "_def",
22.370 -automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
22.371 -"_initial, " ^ automaton_name ^ "_trans,{},{})")
22.372 -])
22.373 -val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
22.374 -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
22.375 -in
22.376 -(
22.377 -if (chk_prime_list = []) then thy2
22.378 -else (
22.379 -error("Precondition or assignment terms in postconditions contain following primed variables:\n"
22.380 - ^ (list_elements_of chk_prime_list)))
22.381 -)
22.382 -end)
22.383 -
22.384 -fun add_composition automaton_name aut_list thy =
22.385 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
22.386 -let
22.387 -val acttyp = check_ac thy aut_list;
22.388 -val st_typ = comp_st_type_of thy aut_list;
22.389 -val comp_list = clist aut_list;
22.390 -in
22.391 -thy
22.392 -|> Sign.add_consts_i
22.393 -[(Binding.name automaton_name,
22.394 -Type("*",
22.395 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
22.396 - Type("*",[Type("set",[st_typ]),
22.397 - Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
22.398 - Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
22.399 -,NoSyn)]
22.400 -|> add_defs
22.401 -[(automaton_name ^ "_def",
22.402 -automaton_name ^ " == " ^ comp_list)]
22.403 -end)
22.404 -
22.405 -fun add_restriction automaton_name aut_source actlist thy =
22.406 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
22.407 -let
22.408 -val auttyp = aut_type_of thy aut_source;
22.409 -val acttyp = act_type_of thy auttyp;
22.410 -val rest_set = action_set_string thy acttyp actlist
22.411 -in
22.412 -thy
22.413 -|> Sign.add_consts_i
22.414 -[(Binding.name automaton_name, auttyp,NoSyn)]
22.415 -|> add_defs
22.416 -[(automaton_name ^ "_def",
22.417 -automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
22.418 -end)
22.419 -fun add_hiding automaton_name aut_source actlist thy =
22.420 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
22.421 -let
22.422 -val auttyp = aut_type_of thy aut_source;
22.423 -val acttyp = act_type_of thy auttyp;
22.424 -val hid_set = action_set_string thy acttyp actlist
22.425 -in
22.426 -thy
22.427 -|> Sign.add_consts_i
22.428 -[(Binding.name automaton_name, auttyp,NoSyn)]
22.429 -|> add_defs
22.430 -[(automaton_name ^ "_def",
22.431 -automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
22.432 -end)
22.433 -
22.434 -fun ren_act_type_of thy funct =
22.435 - (case Term.fastype_of (Syntax.read_term_global thy funct) of
22.436 - Type ("fun", [a, b]) => a
22.437 - | _ => error "could not extract argument type of renaming function term");
22.438 -
22.439 -fun add_rename automaton_name aut_source fun_name thy =
22.440 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
22.441 -let
22.442 -val auttyp = aut_type_of thy aut_source;
22.443 -val st_typ = st_type_of thy auttyp;
22.444 -val acttyp = ren_act_type_of thy fun_name
22.445 -in
22.446 -thy
22.447 -|> Sign.add_consts_i
22.448 -[(Binding.name automaton_name,
22.449 -Type("*",
22.450 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
22.451 - Type("*",[Type("set",[st_typ]),
22.452 - Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
22.453 - Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
22.454 -,NoSyn)]
22.455 -|> add_defs
22.456 -[(automaton_name ^ "_def",
22.457 -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
22.458 -end)
22.459 -
22.460 -
22.461 -(** outer syntax **)
22.462 -
22.463 -(* prepare results *)
22.464 -
22.465 -(*encoding transition specifications with a element of ParseTrans*)
22.466 -datatype ParseTrans = Rel of string | PP of string*(string*string)list;
22.467 -fun mk_trans_of_rel s = Rel(s);
22.468 -fun mk_trans_of_prepost (s,l) = PP(s,l);
22.469 -
22.470 -fun trans_of (a, Rel b) = (a, b, [("", "")])
22.471 - | trans_of (a, PP (b, l)) = (a, b, l);
22.472 -
22.473 -
22.474 -fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
22.475 - add_ioa aut action_type inp out int states initial (map trans_of trans);
22.476 -
22.477 -fun mk_composition_decl (aut, autlist) =
22.478 - add_composition aut autlist;
22.479 -
22.480 -fun mk_hiding_decl (aut, (actlist, source_aut)) =
22.481 - add_hiding aut source_aut actlist;
22.482 -
22.483 -fun mk_restriction_decl (aut, (source_aut, actlist)) =
22.484 - add_restriction aut source_aut actlist;
22.485 -
22.486 -fun mk_rename_decl (aut, (source_aut, rename_f)) =
22.487 - add_rename aut source_aut rename_f;
22.488 -
22.489 -
22.490 -(* outer syntax *)
22.491 -
22.492 -local structure P = OuterParse and K = OuterKeyword in
22.493 -
22.494 -val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
22.495 - "outputs", "internals", "states", "initially", "transitions", "pre",
22.496 - "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
22.497 - "rename"];
22.498 -
22.499 -val actionlist = P.list1 P.term;
22.500 -val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
22.501 -val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
22.502 -val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
22.503 -val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
22.504 -val initial = P.$$$ "initially" |-- P.!!! P.term;
22.505 -val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
22.506 -val pre = P.$$$ "pre" |-- P.!!! P.term;
22.507 -val post = P.$$$ "post" |-- P.!!! assign_list;
22.508 -val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
22.509 -val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
22.510 -val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
22.511 -val transition = P.term -- (transrel || pre1 || post1);
22.512 -val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
22.513 -
22.514 -val ioa_decl =
22.515 - (P.name -- (P.$$$ "=" |--
22.516 - (P.$$$ "signature" |--
22.517 - P.!!! (P.$$$ "actions" |--
22.518 - (P.typ --
22.519 - (Scan.optional inputslist []) --
22.520 - (Scan.optional outputslist []) --
22.521 - (Scan.optional internalslist []) --
22.522 - stateslist --
22.523 - (Scan.optional initial "True") --
22.524 - translist))))) >> mk_ioa_decl ||
22.525 - (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
22.526 - >> mk_composition_decl ||
22.527 - (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
22.528 - P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
22.529 - (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
22.530 - P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
22.531 - (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
22.532 - >> mk_rename_decl;
22.533 -
22.534 -val _ =
22.535 - OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
22.536 - (ioa_decl >> Toplevel.theory);
22.537 -
22.538 -end;
22.539 -
22.540 -end;
23.1 --- a/src/HOLCF/IsaMakefile Sun Jun 21 23:04:37 2009 +0200
23.2 +++ b/src/HOLCF/IsaMakefile Mon Jun 22 08:00:46 2009 +0200
23.3 @@ -67,8 +67,8 @@
23.4 Tools/domain/domain_library.ML \
23.5 Tools/domain/domain_syntax.ML \
23.6 Tools/domain/domain_theorems.ML \
23.7 - Tools/fixrec_package.ML \
23.8 - Tools/pcpodef_package.ML \
23.9 + Tools/fixrec.ML \
23.10 + Tools/pcpodef.ML \
23.11 holcf_logic.ML \
23.12 document/root.tex
23.13 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
23.14 @@ -127,7 +127,7 @@
23.15 IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \
23.16 IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \
23.17 IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \
23.18 - IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
23.19 + IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
23.20 @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
23.21
23.22
24.1 --- a/src/HOLCF/Pcpodef.thy Sun Jun 21 23:04:37 2009 +0200
24.2 +++ b/src/HOLCF/Pcpodef.thy Mon Jun 22 08:00:46 2009 +0200
24.3 @@ -6,7 +6,7 @@
24.4
24.5 theory Pcpodef
24.6 imports Adm
24.7 -uses ("Tools/pcpodef_package.ML")
24.8 +uses ("Tools/pcpodef.ML")
24.9 begin
24.10
24.11 subsection {* Proving a subtype is a partial order *}
24.12 @@ -303,6 +303,6 @@
24.13
24.14 subsection {* HOLCF type definition package *}
24.15
24.16 -use "Tools/pcpodef_package.ML"
24.17 +use "Tools/pcpodef.ML"
24.18
24.19 end
25.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 23:04:37 2009 +0200
25.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Mon Jun 22 08:00:46 2009 +0200
25.3 @@ -6,7 +6,7 @@
25.4
25.5 signature DOMAIN_AXIOMS =
25.6 sig
25.7 - val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term
25.8 + val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
25.9
25.10 val calc_axioms :
25.11 string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
25.12 @@ -171,7 +171,7 @@
25.13 val mat_names = map mat_name con_names;
25.14 fun qualify n = Sign.full_name thy (Binding.name n);
25.15 val ms = map qualify con_names ~~ map qualify mat_names;
25.16 - in FixrecPackage.add_matchers ms thy end;
25.17 + in Fixrec.add_matchers ms thy end;
25.18
25.19 fun add_axioms comp_dnam (eqs : eq list) thy' =
25.20 let
26.1 --- a/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 23:04:37 2009 +0200
26.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 22 08:00:46 2009 +0200
26.3 @@ -135,10 +135,10 @@
26.4 eqtype arg;
26.5 type cons = string * arg list;
26.6 type eq = (string * typ list) * cons list;
26.7 - val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
26.8 + val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
26.9 val is_lazy : arg -> bool;
26.10 val rec_of : arg -> int;
26.11 - val dtyp_of : arg -> DatatypeAux.dtyp;
26.12 + val dtyp_of : arg -> Datatype.dtyp;
26.13 val sel_of : arg -> string option;
26.14 val vname : arg -> string;
26.15 val upd_vname : (string -> string) -> arg -> arg;
26.16 @@ -154,7 +154,7 @@
26.17 val idx_name : 'a list -> string -> int -> string;
26.18 val app_rec_arg : (int -> term) -> arg -> term;
26.19 val con_app : string -> arg list -> term;
26.20 - val dtyp_of_eq : eq -> DatatypeAux.dtyp;
26.21 + val dtyp_of_eq : eq -> Datatype.dtyp;
26.22
26.23
26.24 (* Name mangling *)
26.25 @@ -215,7 +215,7 @@
26.26 (* ----- constructor list handling ----- *)
26.27
26.28 type arg =
26.29 - (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *)
26.30 + (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
26.31 string option * (* selector name *)
26.32 string; (* argument name *)
26.33
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/src/HOLCF/Tools/fixrec.ML Mon Jun 22 08:00:46 2009 +0200
27.3 @@ -0,0 +1,435 @@
27.4 +(* Title: HOLCF/Tools/fixrec.ML
27.5 + Author: Amber Telfer and Brian Huffman
27.6 +
27.7 +Recursive function definition package for HOLCF.
27.8 +*)
27.9 +
27.10 +signature FIXREC =
27.11 +sig
27.12 + val add_fixrec: bool -> (binding * typ option * mixfix) list
27.13 + -> (Attrib.binding * term) list -> local_theory -> local_theory
27.14 + val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
27.15 + -> (Attrib.binding * string) list -> local_theory -> local_theory
27.16 + val add_fixpat: Thm.binding * term list -> theory -> theory
27.17 + val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
27.18 + val add_matchers: (string * string) list -> theory -> theory
27.19 + val setup: theory -> theory
27.20 +end;
27.21 +
27.22 +structure Fixrec :> FIXREC =
27.23 +struct
27.24 +
27.25 +val def_cont_fix_eq = @{thm def_cont_fix_eq};
27.26 +val def_cont_fix_ind = @{thm def_cont_fix_ind};
27.27 +
27.28 +
27.29 +fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
27.30 +fun fixrec_eq_err thy s eq =
27.31 + fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
27.32 +
27.33 +(*************************************************************************)
27.34 +(***************************** building types ****************************)
27.35 +(*************************************************************************)
27.36 +
27.37 +(* ->> is taken from holcf_logic.ML *)
27.38 +fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
27.39 +
27.40 +infixr 6 ->>; val (op ->>) = cfunT;
27.41 +
27.42 +fun cfunsT (Ts, U) = foldr cfunT U Ts;
27.43 +
27.44 +fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
27.45 + | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
27.46 +
27.47 +fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
27.48 + | binder_cfun _ = [];
27.49 +
27.50 +fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
27.51 + | body_cfun T = T;
27.52 +
27.53 +fun strip_cfun T : typ list * typ =
27.54 + (binder_cfun T, body_cfun T);
27.55 +
27.56 +fun maybeT T = Type(@{type_name "maybe"}, [T]);
27.57 +
27.58 +fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
27.59 + | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
27.60 +
27.61 +fun tupleT [] = HOLogic.unitT
27.62 + | tupleT [T] = T
27.63 + | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
27.64 +
27.65 +fun matchT (T, U) =
27.66 + body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
27.67 +
27.68 +
27.69 +(*************************************************************************)
27.70 +(***************************** building terms ****************************)
27.71 +(*************************************************************************)
27.72 +
27.73 +val mk_trp = HOLogic.mk_Trueprop;
27.74 +
27.75 +(* splits a cterm into the right and lefthand sides of equality *)
27.76 +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
27.77 +
27.78 +(* similar to Thm.head_of, but for continuous application *)
27.79 +fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
27.80 + | chead_of u = u;
27.81 +
27.82 +fun capply_const (S, T) =
27.83 + Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
27.84 +
27.85 +fun cabs_const (S, T) =
27.86 + Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
27.87 +
27.88 +fun mk_cabs t =
27.89 + let val T = Term.fastype_of t
27.90 + in cabs_const (Term.domain_type T, Term.range_type T) $ t end
27.91 +
27.92 +fun mk_capply (t, u) =
27.93 + let val (S, T) =
27.94 + case Term.fastype_of t of
27.95 + Type(@{type_name "->"}, [S, T]) => (S, T)
27.96 + | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
27.97 + in capply_const (S, T) $ t $ u end;
27.98 +
27.99 +infix 0 ==; val (op ==) = Logic.mk_equals;
27.100 +infix 1 ===; val (op ===) = HOLogic.mk_eq;
27.101 +infix 9 ` ; val (op `) = mk_capply;
27.102 +
27.103 +(* builds the expression (LAM v. rhs) *)
27.104 +fun big_lambda v rhs =
27.105 + cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
27.106 +
27.107 +(* builds the expression (LAM v1 v2 .. vn. rhs) *)
27.108 +fun big_lambdas [] rhs = rhs
27.109 + | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
27.110 +
27.111 +fun mk_return t =
27.112 + let val T = Term.fastype_of t
27.113 + in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
27.114 +
27.115 +fun mk_bind (t, u) =
27.116 + let val (T, mU) = dest_cfunT (Term.fastype_of u);
27.117 + val bindT = maybeT T ->> (T ->> mU) ->> mU;
27.118 + in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
27.119 +
27.120 +fun mk_mplus (t, u) =
27.121 + let val mT = Term.fastype_of t
27.122 + in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
27.123 +
27.124 +fun mk_run t =
27.125 + let val mT = Term.fastype_of t
27.126 + val T = dest_maybeT mT
27.127 + in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
27.128 +
27.129 +fun mk_fix t =
27.130 + let val (T, _) = dest_cfunT (Term.fastype_of t)
27.131 + in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
27.132 +
27.133 +fun mk_cont t =
27.134 + let val T = Term.fastype_of t
27.135 + in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
27.136 +
27.137 +val mk_fst = HOLogic.mk_fst
27.138 +val mk_snd = HOLogic.mk_snd
27.139 +
27.140 +(* builds the expression (v1,v2,..,vn) *)
27.141 +fun mk_tuple [] = HOLogic.unit
27.142 +| mk_tuple (t::[]) = t
27.143 +| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
27.144 +
27.145 +(* builds the expression (%(v1,v2,..,vn). rhs) *)
27.146 +fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
27.147 + | lambda_tuple (v::[]) rhs = Term.lambda v rhs
27.148 + | lambda_tuple (v::vs) rhs =
27.149 + HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
27.150 +
27.151 +
27.152 +(*************************************************************************)
27.153 +(************* fixed-point definitions and unfolding theorems ************)
27.154 +(*************************************************************************)
27.155 +
27.156 +fun add_fixdefs
27.157 + (fixes : ((binding * typ) * mixfix) list)
27.158 + (spec : (Attrib.binding * term) list)
27.159 + (lthy : local_theory) =
27.160 + let
27.161 + val thy = ProofContext.theory_of lthy;
27.162 + val names = map (Binding.name_of o fst o fst) fixes;
27.163 + val all_names = space_implode "_" names;
27.164 + val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
27.165 + val functional = lambda_tuple lhss (mk_tuple rhss);
27.166 + val fixpoint = mk_fix (mk_cabs functional);
27.167 +
27.168 + val cont_thm =
27.169 + Goal.prove lthy [] [] (mk_trp (mk_cont functional))
27.170 + (K (simp_tac (local_simpset_of lthy) 1));
27.171 +
27.172 + fun one_def (l as Free(n,_)) r =
27.173 + let val b = Long_Name.base_name n
27.174 + in ((Binding.name (b^"_def"), []), r) end
27.175 + | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
27.176 + fun defs [] _ = []
27.177 + | defs (l::[]) r = [one_def l r]
27.178 + | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
27.179 + val fixdefs = defs lhss fixpoint;
27.180 + val define_all = fold_map (LocalTheory.define Thm.definitionK);
27.181 + val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
27.182 + |> define_all (map (apfst fst) fixes ~~ fixdefs);
27.183 + fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
27.184 + val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
27.185 + val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
27.186 + val predicate = lambda_tuple lhss (list_comb (P, lhss));
27.187 + val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
27.188 + |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
27.189 + |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
27.190 + val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
27.191 + |> LocalDefs.unfold lthy' @{thms split_conv};
27.192 + fun unfolds [] thm = []
27.193 + | unfolds (n::[]) thm = [(n^"_unfold", thm)]
27.194 + | unfolds (n::ns) thm = let
27.195 + val thmL = thm RS @{thm Pair_eqD1};
27.196 + val thmR = thm RS @{thm Pair_eqD2};
27.197 + in (n^"_unfold", thmL) :: unfolds ns thmR end;
27.198 + val unfold_thms = unfolds names tuple_unfold_thm;
27.199 + fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
27.200 + val (thmss, lthy'') = lthy'
27.201 + |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
27.202 + ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
27.203 + in
27.204 + (lthy'', names, fixdef_thms, map snd unfold_thms)
27.205 + end;
27.206 +
27.207 +(*************************************************************************)
27.208 +(*********** monadic notation and pattern matching compilation ***********)
27.209 +(*************************************************************************)
27.210 +
27.211 +structure FixrecMatchData = TheoryDataFun (
27.212 + type T = string Symtab.table;
27.213 + val empty = Symtab.empty;
27.214 + val copy = I;
27.215 + val extend = I;
27.216 + fun merge _ tabs : T = Symtab.merge (K true) tabs;
27.217 +);
27.218 +
27.219 +(* associate match functions with pattern constants *)
27.220 +fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
27.221 +
27.222 +fun taken_names (t : term) : bstring list =
27.223 + let
27.224 + fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
27.225 + | taken (Free(a,_) , bs) = insert (op =) a bs
27.226 + | taken (f $ u , bs) = taken (f, taken (u, bs))
27.227 + | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
27.228 + | taken (_ , bs) = bs;
27.229 + in
27.230 + taken (t, [])
27.231 + end;
27.232 +
27.233 +(* builds a monadic term for matching a constructor pattern *)
27.234 +fun pre_build match_name pat rhs vs taken =
27.235 + case pat of
27.236 + Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
27.237 + pre_build match_name f rhs (v::vs) taken
27.238 + | Const(@{const_name Rep_CFun},_)$f$x =>
27.239 + let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
27.240 + in pre_build match_name f rhs' (v::vs) taken' end
27.241 + | Const(c,T) =>
27.242 + let
27.243 + val n = Name.variant taken "v";
27.244 + fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
27.245 + | result_type T _ = T;
27.246 + val v = Free(n, result_type T vs);
27.247 + val m = Const(match_name c, matchT (T, fastype_of rhs));
27.248 + val k = big_lambdas vs rhs;
27.249 + in
27.250 + (m`v`k, v, n::taken)
27.251 + end
27.252 + | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
27.253 + | _ => fixrec_err "pre_build: invalid pattern";
27.254 +
27.255 +(* builds a monadic term for matching a function definition pattern *)
27.256 +(* returns (name, arity, matcher) *)
27.257 +fun building match_name pat rhs vs taken =
27.258 + case pat of
27.259 + Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
27.260 + building match_name f rhs (v::vs) taken
27.261 + | Const(@{const_name Rep_CFun}, _)$f$x =>
27.262 + let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
27.263 + in building match_name f rhs' (v::vs) taken' end
27.264 + | Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
27.265 + | Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
27.266 + | _ => fixrec_err ("function is not declared as constant in theory: "
27.267 + ^ ML_Syntax.print_term pat);
27.268 +
27.269 +fun strip_alls t =
27.270 + if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
27.271 +
27.272 +fun match_eq match_name eq =
27.273 + let
27.274 + val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
27.275 + in
27.276 + building match_name lhs (mk_return rhs) [] (taken_names eq)
27.277 + end;
27.278 +
27.279 +(* returns the sum (using +++) of the terms in ms *)
27.280 +(* also applies "run" to the result! *)
27.281 +fun fatbar arity ms =
27.282 + let
27.283 + fun LAM_Ts 0 t = ([], Term.fastype_of t)
27.284 + | LAM_Ts n (_ $ Abs(_,T,t)) =
27.285 + let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
27.286 + | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
27.287 + fun unLAM 0 t = t
27.288 + | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
27.289 + | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
27.290 + fun reLAM ([], U) t = t
27.291 + | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
27.292 + val msum = foldr1 mk_mplus (map (unLAM arity) ms);
27.293 + val (Ts, U) = LAM_Ts arity (hd ms)
27.294 + in
27.295 + reLAM (rev Ts, dest_maybeT U) (mk_run msum)
27.296 + end;
27.297 +
27.298 +(* this is the pattern-matching compiler function *)
27.299 +fun compile_pats match_name eqs =
27.300 + let
27.301 + val (((n::names),(a::arities)),mats) =
27.302 + apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
27.303 + val cname = if forall (fn x => n=x) names then n
27.304 + else fixrec_err "all equations in block must define the same function";
27.305 + val arity = if forall (fn x => a=x) arities then a
27.306 + else fixrec_err "all equations in block must have the same arity";
27.307 + val rhs = fatbar arity mats;
27.308 + in
27.309 + mk_trp (cname === rhs)
27.310 + end;
27.311 +
27.312 +(*************************************************************************)
27.313 +(********************** Proving associated theorems **********************)
27.314 +(*************************************************************************)
27.315 +
27.316 +(* proves a block of pattern matching equations as theorems, using unfold *)
27.317 +fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
27.318 + let
27.319 + val tacs =
27.320 + [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
27.321 + asm_simp_tac (local_simpset_of lthy) 1];
27.322 + fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
27.323 + fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
27.324 + in
27.325 + map prove_eqn eqns
27.326 + end;
27.327 +
27.328 +(*************************************************************************)
27.329 +(************************* Main fixrec function **************************)
27.330 +(*************************************************************************)
27.331 +
27.332 +local
27.333 +(* code adapted from HOL/Tools/primrec.ML *)
27.334 +
27.335 +fun gen_fixrec
27.336 + (set_group : bool)
27.337 + prep_spec
27.338 + (strict : bool)
27.339 + raw_fixes
27.340 + raw_spec
27.341 + (lthy : local_theory) =
27.342 + let
27.343 + val (fixes : ((binding * typ) * mixfix) list,
27.344 + spec : (Attrib.binding * term) list) =
27.345 + fst (prep_spec raw_fixes raw_spec lthy);
27.346 + val chead_of_spec =
27.347 + chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
27.348 + fun name_of (Free (n, _)) = n
27.349 + | name_of t = fixrec_err ("unknown term");
27.350 + val all_names = map (name_of o chead_of_spec) spec;
27.351 + val names = distinct (op =) all_names;
27.352 + fun block_of_name n =
27.353 + map_filter
27.354 + (fn (m,eq) => if m = n then SOME eq else NONE)
27.355 + (all_names ~~ spec);
27.356 + val blocks = map block_of_name names;
27.357 +
27.358 + val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
27.359 + fun match_name c =
27.360 + case Symtab.lookup matcher_tab c of SOME m => m
27.361 + | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
27.362 +
27.363 + val matches = map (compile_pats match_name) (map (map snd) blocks);
27.364 + val spec' = map (pair Attrib.empty_binding) matches;
27.365 + val (lthy', cnames, fixdef_thms, unfold_thms) =
27.366 + add_fixdefs fixes spec' lthy;
27.367 + in
27.368 + if strict then let (* only prove simp rules if strict = true *)
27.369 + val simps : (Attrib.binding * thm) list list =
27.370 + map (make_simps lthy') (unfold_thms ~~ blocks);
27.371 + fun mk_bind n : Attrib.binding =
27.372 + (Binding.name (n ^ "_simps"),
27.373 + [Attrib.internal (K Simplifier.simp_add)]);
27.374 + val simps1 : (Attrib.binding * thm list) list =
27.375 + map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
27.376 + val simps2 : (Attrib.binding * thm list) list =
27.377 + map (apsnd (fn thm => [thm])) (List.concat simps);
27.378 + val (_, lthy'') = lthy'
27.379 + |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
27.380 + in
27.381 + lthy''
27.382 + end
27.383 + else lthy'
27.384 + end;
27.385 +
27.386 +in
27.387 +
27.388 +val add_fixrec = gen_fixrec false Specification.check_spec;
27.389 +val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
27.390 +
27.391 +end; (* local *)
27.392 +
27.393 +(*************************************************************************)
27.394 +(******************************** Fixpat *********************************)
27.395 +(*************************************************************************)
27.396 +
27.397 +fun fix_pat thy t =
27.398 + let
27.399 + val T = fastype_of t;
27.400 + val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
27.401 + val cname = case chead_of t of Const(c,_) => c | _ =>
27.402 + fixrec_err "function is not declared as constant in theory";
27.403 + val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
27.404 + val simp = Goal.prove_global thy [] [] eq
27.405 + (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
27.406 + in simp end;
27.407 +
27.408 +fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
27.409 + let
27.410 + val atts = map (prep_attrib thy) srcs;
27.411 + val ts = map (prep_term thy) strings;
27.412 + val simps = map (fix_pat thy) ts;
27.413 + in
27.414 + (snd o PureThy.add_thmss [((name, simps), atts)]) thy
27.415 + end;
27.416 +
27.417 +val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
27.418 +val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
27.419 +
27.420 +
27.421 +(*************************************************************************)
27.422 +(******************************** Parsers ********************************)
27.423 +(*************************************************************************)
27.424 +
27.425 +local structure P = OuterParse and K = OuterKeyword in
27.426 +
27.427 +val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
27.428 + ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
27.429 + >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
27.430 +
27.431 +val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
27.432 + (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
27.433 +
27.434 +end;
27.435 +
27.436 +val setup = FixrecMatchData.init;
27.437 +
27.438 +end;
28.1 --- a/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 23:04:37 2009 +0200
28.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
28.3 @@ -1,435 +0,0 @@
28.4 -(* Title: HOLCF/Tools/fixrec_package.ML
28.5 - Author: Amber Telfer and Brian Huffman
28.6 -
28.7 -Recursive function definition package for HOLCF.
28.8 -*)
28.9 -
28.10 -signature FIXREC_PACKAGE =
28.11 -sig
28.12 - val add_fixrec: bool -> (binding * typ option * mixfix) list
28.13 - -> (Attrib.binding * term) list -> local_theory -> local_theory
28.14 - val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
28.15 - -> (Attrib.binding * string) list -> local_theory -> local_theory
28.16 - val add_fixpat: Thm.binding * term list -> theory -> theory
28.17 - val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
28.18 - val add_matchers: (string * string) list -> theory -> theory
28.19 - val setup: theory -> theory
28.20 -end;
28.21 -
28.22 -structure FixrecPackage :> FIXREC_PACKAGE =
28.23 -struct
28.24 -
28.25 -val def_cont_fix_eq = @{thm def_cont_fix_eq};
28.26 -val def_cont_fix_ind = @{thm def_cont_fix_ind};
28.27 -
28.28 -
28.29 -fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
28.30 -fun fixrec_eq_err thy s eq =
28.31 - fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
28.32 -
28.33 -(*************************************************************************)
28.34 -(***************************** building types ****************************)
28.35 -(*************************************************************************)
28.36 -
28.37 -(* ->> is taken from holcf_logic.ML *)
28.38 -fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
28.39 -
28.40 -infixr 6 ->>; val (op ->>) = cfunT;
28.41 -
28.42 -fun cfunsT (Ts, U) = foldr cfunT U Ts;
28.43 -
28.44 -fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
28.45 - | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
28.46 -
28.47 -fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
28.48 - | binder_cfun _ = [];
28.49 -
28.50 -fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
28.51 - | body_cfun T = T;
28.52 -
28.53 -fun strip_cfun T : typ list * typ =
28.54 - (binder_cfun T, body_cfun T);
28.55 -
28.56 -fun maybeT T = Type(@{type_name "maybe"}, [T]);
28.57 -
28.58 -fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
28.59 - | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
28.60 -
28.61 -fun tupleT [] = HOLogic.unitT
28.62 - | tupleT [T] = T
28.63 - | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
28.64 -
28.65 -fun matchT (T, U) =
28.66 - body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
28.67 -
28.68 -
28.69 -(*************************************************************************)
28.70 -(***************************** building terms ****************************)
28.71 -(*************************************************************************)
28.72 -
28.73 -val mk_trp = HOLogic.mk_Trueprop;
28.74 -
28.75 -(* splits a cterm into the right and lefthand sides of equality *)
28.76 -fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
28.77 -
28.78 -(* similar to Thm.head_of, but for continuous application *)
28.79 -fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
28.80 - | chead_of u = u;
28.81 -
28.82 -fun capply_const (S, T) =
28.83 - Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
28.84 -
28.85 -fun cabs_const (S, T) =
28.86 - Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
28.87 -
28.88 -fun mk_cabs t =
28.89 - let val T = Term.fastype_of t
28.90 - in cabs_const (Term.domain_type T, Term.range_type T) $ t end
28.91 -
28.92 -fun mk_capply (t, u) =
28.93 - let val (S, T) =
28.94 - case Term.fastype_of t of
28.95 - Type(@{type_name "->"}, [S, T]) => (S, T)
28.96 - | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
28.97 - in capply_const (S, T) $ t $ u end;
28.98 -
28.99 -infix 0 ==; val (op ==) = Logic.mk_equals;
28.100 -infix 1 ===; val (op ===) = HOLogic.mk_eq;
28.101 -infix 9 ` ; val (op `) = mk_capply;
28.102 -
28.103 -(* builds the expression (LAM v. rhs) *)
28.104 -fun big_lambda v rhs =
28.105 - cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
28.106 -
28.107 -(* builds the expression (LAM v1 v2 .. vn. rhs) *)
28.108 -fun big_lambdas [] rhs = rhs
28.109 - | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
28.110 -
28.111 -fun mk_return t =
28.112 - let val T = Term.fastype_of t
28.113 - in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
28.114 -
28.115 -fun mk_bind (t, u) =
28.116 - let val (T, mU) = dest_cfunT (Term.fastype_of u);
28.117 - val bindT = maybeT T ->> (T ->> mU) ->> mU;
28.118 - in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
28.119 -
28.120 -fun mk_mplus (t, u) =
28.121 - let val mT = Term.fastype_of t
28.122 - in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
28.123 -
28.124 -fun mk_run t =
28.125 - let val mT = Term.fastype_of t
28.126 - val T = dest_maybeT mT
28.127 - in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
28.128 -
28.129 -fun mk_fix t =
28.130 - let val (T, _) = dest_cfunT (Term.fastype_of t)
28.131 - in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
28.132 -
28.133 -fun mk_cont t =
28.134 - let val T = Term.fastype_of t
28.135 - in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
28.136 -
28.137 -val mk_fst = HOLogic.mk_fst
28.138 -val mk_snd = HOLogic.mk_snd
28.139 -
28.140 -(* builds the expression (v1,v2,..,vn) *)
28.141 -fun mk_tuple [] = HOLogic.unit
28.142 -| mk_tuple (t::[]) = t
28.143 -| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
28.144 -
28.145 -(* builds the expression (%(v1,v2,..,vn). rhs) *)
28.146 -fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
28.147 - | lambda_tuple (v::[]) rhs = Term.lambda v rhs
28.148 - | lambda_tuple (v::vs) rhs =
28.149 - HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
28.150 -
28.151 -
28.152 -(*************************************************************************)
28.153 -(************* fixed-point definitions and unfolding theorems ************)
28.154 -(*************************************************************************)
28.155 -
28.156 -fun add_fixdefs
28.157 - (fixes : ((binding * typ) * mixfix) list)
28.158 - (spec : (Attrib.binding * term) list)
28.159 - (lthy : local_theory) =
28.160 - let
28.161 - val thy = ProofContext.theory_of lthy;
28.162 - val names = map (Binding.name_of o fst o fst) fixes;
28.163 - val all_names = space_implode "_" names;
28.164 - val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
28.165 - val functional = lambda_tuple lhss (mk_tuple rhss);
28.166 - val fixpoint = mk_fix (mk_cabs functional);
28.167 -
28.168 - val cont_thm =
28.169 - Goal.prove lthy [] [] (mk_trp (mk_cont functional))
28.170 - (K (simp_tac (local_simpset_of lthy) 1));
28.171 -
28.172 - fun one_def (l as Free(n,_)) r =
28.173 - let val b = Long_Name.base_name n
28.174 - in ((Binding.name (b^"_def"), []), r) end
28.175 - | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
28.176 - fun defs [] _ = []
28.177 - | defs (l::[]) r = [one_def l r]
28.178 - | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
28.179 - val fixdefs = defs lhss fixpoint;
28.180 - val define_all = fold_map (LocalTheory.define Thm.definitionK);
28.181 - val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
28.182 - |> define_all (map (apfst fst) fixes ~~ fixdefs);
28.183 - fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
28.184 - val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
28.185 - val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
28.186 - val predicate = lambda_tuple lhss (list_comb (P, lhss));
28.187 - val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
28.188 - |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
28.189 - |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
28.190 - val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
28.191 - |> LocalDefs.unfold lthy' @{thms split_conv};
28.192 - fun unfolds [] thm = []
28.193 - | unfolds (n::[]) thm = [(n^"_unfold", thm)]
28.194 - | unfolds (n::ns) thm = let
28.195 - val thmL = thm RS @{thm Pair_eqD1};
28.196 - val thmR = thm RS @{thm Pair_eqD2};
28.197 - in (n^"_unfold", thmL) :: unfolds ns thmR end;
28.198 - val unfold_thms = unfolds names tuple_unfold_thm;
28.199 - fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
28.200 - val (thmss, lthy'') = lthy'
28.201 - |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
28.202 - ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
28.203 - in
28.204 - (lthy'', names, fixdef_thms, map snd unfold_thms)
28.205 - end;
28.206 -
28.207 -(*************************************************************************)
28.208 -(*********** monadic notation and pattern matching compilation ***********)
28.209 -(*************************************************************************)
28.210 -
28.211 -structure FixrecMatchData = TheoryDataFun (
28.212 - type T = string Symtab.table;
28.213 - val empty = Symtab.empty;
28.214 - val copy = I;
28.215 - val extend = I;
28.216 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
28.217 -);
28.218 -
28.219 -(* associate match functions with pattern constants *)
28.220 -fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
28.221 -
28.222 -fun taken_names (t : term) : bstring list =
28.223 - let
28.224 - fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
28.225 - | taken (Free(a,_) , bs) = insert (op =) a bs
28.226 - | taken (f $ u , bs) = taken (f, taken (u, bs))
28.227 - | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
28.228 - | taken (_ , bs) = bs;
28.229 - in
28.230 - taken (t, [])
28.231 - end;
28.232 -
28.233 -(* builds a monadic term for matching a constructor pattern *)
28.234 -fun pre_build match_name pat rhs vs taken =
28.235 - case pat of
28.236 - Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
28.237 - pre_build match_name f rhs (v::vs) taken
28.238 - | Const(@{const_name Rep_CFun},_)$f$x =>
28.239 - let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
28.240 - in pre_build match_name f rhs' (v::vs) taken' end
28.241 - | Const(c,T) =>
28.242 - let
28.243 - val n = Name.variant taken "v";
28.244 - fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
28.245 - | result_type T _ = T;
28.246 - val v = Free(n, result_type T vs);
28.247 - val m = Const(match_name c, matchT (T, fastype_of rhs));
28.248 - val k = big_lambdas vs rhs;
28.249 - in
28.250 - (m`v`k, v, n::taken)
28.251 - end
28.252 - | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
28.253 - | _ => fixrec_err "pre_build: invalid pattern";
28.254 -
28.255 -(* builds a monadic term for matching a function definition pattern *)
28.256 -(* returns (name, arity, matcher) *)
28.257 -fun building match_name pat rhs vs taken =
28.258 - case pat of
28.259 - Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
28.260 - building match_name f rhs (v::vs) taken
28.261 - | Const(@{const_name Rep_CFun}, _)$f$x =>
28.262 - let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
28.263 - in building match_name f rhs' (v::vs) taken' end
28.264 - | Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
28.265 - | Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
28.266 - | _ => fixrec_err ("function is not declared as constant in theory: "
28.267 - ^ ML_Syntax.print_term pat);
28.268 -
28.269 -fun strip_alls t =
28.270 - if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
28.271 -
28.272 -fun match_eq match_name eq =
28.273 - let
28.274 - val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
28.275 - in
28.276 - building match_name lhs (mk_return rhs) [] (taken_names eq)
28.277 - end;
28.278 -
28.279 -(* returns the sum (using +++) of the terms in ms *)
28.280 -(* also applies "run" to the result! *)
28.281 -fun fatbar arity ms =
28.282 - let
28.283 - fun LAM_Ts 0 t = ([], Term.fastype_of t)
28.284 - | LAM_Ts n (_ $ Abs(_,T,t)) =
28.285 - let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
28.286 - | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
28.287 - fun unLAM 0 t = t
28.288 - | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
28.289 - | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
28.290 - fun reLAM ([], U) t = t
28.291 - | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
28.292 - val msum = foldr1 mk_mplus (map (unLAM arity) ms);
28.293 - val (Ts, U) = LAM_Ts arity (hd ms)
28.294 - in
28.295 - reLAM (rev Ts, dest_maybeT U) (mk_run msum)
28.296 - end;
28.297 -
28.298 -(* this is the pattern-matching compiler function *)
28.299 -fun compile_pats match_name eqs =
28.300 - let
28.301 - val (((n::names),(a::arities)),mats) =
28.302 - apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
28.303 - val cname = if forall (fn x => n=x) names then n
28.304 - else fixrec_err "all equations in block must define the same function";
28.305 - val arity = if forall (fn x => a=x) arities then a
28.306 - else fixrec_err "all equations in block must have the same arity";
28.307 - val rhs = fatbar arity mats;
28.308 - in
28.309 - mk_trp (cname === rhs)
28.310 - end;
28.311 -
28.312 -(*************************************************************************)
28.313 -(********************** Proving associated theorems **********************)
28.314 -(*************************************************************************)
28.315 -
28.316 -(* proves a block of pattern matching equations as theorems, using unfold *)
28.317 -fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
28.318 - let
28.319 - val tacs =
28.320 - [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
28.321 - asm_simp_tac (local_simpset_of lthy) 1];
28.322 - fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
28.323 - fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
28.324 - in
28.325 - map prove_eqn eqns
28.326 - end;
28.327 -
28.328 -(*************************************************************************)
28.329 -(************************* Main fixrec function **************************)
28.330 -(*************************************************************************)
28.331 -
28.332 -local
28.333 -(* code adapted from HOL/Tools/primrec_package.ML *)
28.334 -
28.335 -fun gen_fixrec
28.336 - (set_group : bool)
28.337 - prep_spec
28.338 - (strict : bool)
28.339 - raw_fixes
28.340 - raw_spec
28.341 - (lthy : local_theory) =
28.342 - let
28.343 - val (fixes : ((binding * typ) * mixfix) list,
28.344 - spec : (Attrib.binding * term) list) =
28.345 - fst (prep_spec raw_fixes raw_spec lthy);
28.346 - val chead_of_spec =
28.347 - chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
28.348 - fun name_of (Free (n, _)) = n
28.349 - | name_of t = fixrec_err ("unknown term");
28.350 - val all_names = map (name_of o chead_of_spec) spec;
28.351 - val names = distinct (op =) all_names;
28.352 - fun block_of_name n =
28.353 - map_filter
28.354 - (fn (m,eq) => if m = n then SOME eq else NONE)
28.355 - (all_names ~~ spec);
28.356 - val blocks = map block_of_name names;
28.357 -
28.358 - val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
28.359 - fun match_name c =
28.360 - case Symtab.lookup matcher_tab c of SOME m => m
28.361 - | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
28.362 -
28.363 - val matches = map (compile_pats match_name) (map (map snd) blocks);
28.364 - val spec' = map (pair Attrib.empty_binding) matches;
28.365 - val (lthy', cnames, fixdef_thms, unfold_thms) =
28.366 - add_fixdefs fixes spec' lthy;
28.367 - in
28.368 - if strict then let (* only prove simp rules if strict = true *)
28.369 - val simps : (Attrib.binding * thm) list list =
28.370 - map (make_simps lthy') (unfold_thms ~~ blocks);
28.371 - fun mk_bind n : Attrib.binding =
28.372 - (Binding.name (n ^ "_simps"),
28.373 - [Attrib.internal (K Simplifier.simp_add)]);
28.374 - val simps1 : (Attrib.binding * thm list) list =
28.375 - map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
28.376 - val simps2 : (Attrib.binding * thm list) list =
28.377 - map (apsnd (fn thm => [thm])) (List.concat simps);
28.378 - val (_, lthy'') = lthy'
28.379 - |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
28.380 - in
28.381 - lthy''
28.382 - end
28.383 - else lthy'
28.384 - end;
28.385 -
28.386 -in
28.387 -
28.388 -val add_fixrec = gen_fixrec false Specification.check_spec;
28.389 -val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
28.390 -
28.391 -end; (* local *)
28.392 -
28.393 -(*************************************************************************)
28.394 -(******************************** Fixpat *********************************)
28.395 -(*************************************************************************)
28.396 -
28.397 -fun fix_pat thy t =
28.398 - let
28.399 - val T = fastype_of t;
28.400 - val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
28.401 - val cname = case chead_of t of Const(c,_) => c | _ =>
28.402 - fixrec_err "function is not declared as constant in theory";
28.403 - val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
28.404 - val simp = Goal.prove_global thy [] [] eq
28.405 - (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
28.406 - in simp end;
28.407 -
28.408 -fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
28.409 - let
28.410 - val atts = map (prep_attrib thy) srcs;
28.411 - val ts = map (prep_term thy) strings;
28.412 - val simps = map (fix_pat thy) ts;
28.413 - in
28.414 - (snd o PureThy.add_thmss [((name, simps), atts)]) thy
28.415 - end;
28.416 -
28.417 -val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
28.418 -val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
28.419 -
28.420 -
28.421 -(*************************************************************************)
28.422 -(******************************** Parsers ********************************)
28.423 -(*************************************************************************)
28.424 -
28.425 -local structure P = OuterParse and K = OuterKeyword in
28.426 -
28.427 -val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
28.428 - ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
28.429 - >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
28.430 -
28.431 -val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
28.432 - (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
28.433 -
28.434 -end;
28.435 -
28.436 -val setup = FixrecMatchData.init;
28.437 -
28.438 -end;
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/src/HOLCF/Tools/pcpodef.ML Mon Jun 22 08:00:46 2009 +0200
29.3 @@ -0,0 +1,201 @@
29.4 +(* Title: HOLCF/Tools/pcpodef.ML
29.5 + Author: Brian Huffman
29.6 +
29.7 +Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
29.8 +typedef (see also ~~/src/HOL/Tools/typedef.ML).
29.9 +*)
29.10 +
29.11 +signature PCPODEF =
29.12 +sig
29.13 + val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
29.14 + * (binding * binding) option -> theory -> Proof.state
29.15 + val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
29.16 + * (binding * binding) option -> theory -> Proof.state
29.17 + val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
29.18 + * (binding * binding) option -> theory -> Proof.state
29.19 + val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
29.20 + * (binding * binding) option -> theory -> Proof.state
29.21 +end;
29.22 +
29.23 +structure Pcpodef :> PCPODEF =
29.24 +struct
29.25 +
29.26 +(** type definitions **)
29.27 +
29.28 +(* prepare_cpodef *)
29.29 +
29.30 +fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
29.31 +
29.32 +fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
29.33 +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
29.34 +
29.35 +fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
29.36 + let
29.37 + val _ = Theory.requires thy "Pcpodef" "pcpodefs";
29.38 + val ctxt = ProofContext.init thy;
29.39 +
29.40 + val full = Sign.full_name thy;
29.41 + val full_name = full name;
29.42 + val bname = Binding.name_of name;
29.43 +
29.44 + (*rhs*)
29.45 + val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
29.46 + val setT = Term.fastype_of set;
29.47 + val rhs_tfrees = Term.add_tfrees set [];
29.48 + val oldT = HOLogic.dest_setT setT handle TYPE _ =>
29.49 + error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
29.50 +
29.51 + (*goal*)
29.52 + val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
29.53 + val goal_nonempty =
29.54 + HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
29.55 + val goal_admissible =
29.56 + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
29.57 +
29.58 + (*lhs*)
29.59 + val defS = Sign.defaultS thy;
29.60 + val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
29.61 + val lhs_sorts = map snd lhs_tfrees;
29.62 +
29.63 + val tname = Binding.map_name (Syntax.type_name mx) t;
29.64 + val full_tname = full tname;
29.65 + val newT = Type (full_tname, map TFree lhs_tfrees);
29.66 +
29.67 + val (Rep_name, Abs_name) =
29.68 + (case opt_morphs of
29.69 + NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
29.70 + | SOME morphs => morphs);
29.71 + val RepC = Const (full Rep_name, newT --> oldT);
29.72 + fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
29.73 + val below_def = Logic.mk_equals (belowC newT,
29.74 + Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
29.75 +
29.76 + fun make_po tac thy1 =
29.77 + let
29.78 + val ((_, {type_definition, set_def, ...}), thy2) = thy1
29.79 + |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
29.80 + val lthy3 = thy2
29.81 + |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
29.82 + val below_def' = Syntax.check_term lthy3 below_def;
29.83 + val ((_, (_, below_definition')), lthy4) = lthy3
29.84 + |> Specification.definition (NONE,
29.85 + ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
29.86 + val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
29.87 + val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
29.88 + val thy5 = lthy4
29.89 + |> Class.prove_instantiation_instance
29.90 + (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
29.91 + |> LocalTheory.exit_global;
29.92 + in ((type_definition, below_definition, set_def), thy5) end;
29.93 +
29.94 + fun make_cpo admissible (type_def, below_def, set_def) theory =
29.95 + let
29.96 + val admissible' = fold_rule (the_list set_def) admissible;
29.97 + val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
29.98 + val theory' = theory
29.99 + |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
29.100 + (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
29.101 + val cpo_thms' = map (Thm.transfer theory') cpo_thms;
29.102 + in
29.103 + theory'
29.104 + |> Sign.add_path (Binding.name_of name)
29.105 + |> PureThy.add_thms
29.106 + ([((Binding.prefix_name "adm_" name, admissible'), []),
29.107 + ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
29.108 + ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
29.109 + ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
29.110 + ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
29.111 + ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
29.112 + |> snd
29.113 + |> Sign.parent_path
29.114 + end;
29.115 +
29.116 + fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
29.117 + let
29.118 + val UU_mem' = fold_rule (the_list set_def) UU_mem;
29.119 + val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
29.120 + val theory' = theory
29.121 + |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
29.122 + (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
29.123 + val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
29.124 + in
29.125 + theory'
29.126 + |> Sign.add_path (Binding.name_of name)
29.127 + |> PureThy.add_thms
29.128 + ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
29.129 + ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
29.130 + ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
29.131 + ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
29.132 + ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
29.133 + ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
29.134 + |> snd
29.135 + |> Sign.parent_path
29.136 + end;
29.137 +
29.138 + fun pcpodef_result UU_mem admissible =
29.139 + make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
29.140 + #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
29.141 +
29.142 + fun cpodef_result nonempty admissible =
29.143 + make_po (Tactic.rtac nonempty 1)
29.144 + #-> make_cpo admissible;
29.145 + in
29.146 + if pcpo
29.147 + then (goal_UU_mem, goal_admissible, pcpodef_result)
29.148 + else (goal_nonempty, goal_admissible, cpodef_result)
29.149 + end
29.150 + handle ERROR msg =>
29.151 + cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
29.152 +
29.153 +
29.154 +(* proof interface *)
29.155 +
29.156 +local
29.157 +
29.158 +fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
29.159 + let
29.160 + val (goal1, goal2, make_result) =
29.161 + prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
29.162 + fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
29.163 + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
29.164 +
29.165 +in
29.166 +
29.167 +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
29.168 +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
29.169 +
29.170 +fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
29.171 +fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
29.172 +
29.173 +end;
29.174 +
29.175 +
29.176 +
29.177 +(** outer syntax **)
29.178 +
29.179 +local structure P = OuterParse and K = OuterKeyword in
29.180 +
29.181 +val typedef_proof_decl =
29.182 + Scan.optional (P.$$$ "(" |--
29.183 + ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
29.184 + --| P.$$$ ")") (true, NONE) --
29.185 + (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
29.186 + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
29.187 +
29.188 +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
29.189 + (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
29.190 + ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
29.191 +
29.192 +val _ =
29.193 + OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
29.194 + (typedef_proof_decl >>
29.195 + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
29.196 +
29.197 +val _ =
29.198 + OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
29.199 + (typedef_proof_decl >>
29.200 + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
29.201 +
29.202 +end;
29.203 +
29.204 +end;
30.1 --- a/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 23:04:37 2009 +0200
30.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
30.3 @@ -1,201 +0,0 @@
30.4 -(* Title: HOLCF/Tools/pcpodef_package.ML
30.5 - Author: Brian Huffman
30.6 -
30.7 -Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
30.8 -typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
30.9 -*)
30.10 -
30.11 -signature PCPODEF_PACKAGE =
30.12 -sig
30.13 - val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
30.14 - * (binding * binding) option -> theory -> Proof.state
30.15 - val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
30.16 - * (binding * binding) option -> theory -> Proof.state
30.17 - val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
30.18 - * (binding * binding) option -> theory -> Proof.state
30.19 - val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
30.20 - * (binding * binding) option -> theory -> Proof.state
30.21 -end;
30.22 -
30.23 -structure PcpodefPackage :> PCPODEF_PACKAGE =
30.24 -struct
30.25 -
30.26 -(** type definitions **)
30.27 -
30.28 -(* prepare_cpodef *)
30.29 -
30.30 -fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
30.31 -
30.32 -fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
30.33 -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
30.34 -
30.35 -fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
30.36 - let
30.37 - val _ = Theory.requires thy "Pcpodef" "pcpodefs";
30.38 - val ctxt = ProofContext.init thy;
30.39 -
30.40 - val full = Sign.full_name thy;
30.41 - val full_name = full name;
30.42 - val bname = Binding.name_of name;
30.43 -
30.44 - (*rhs*)
30.45 - val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
30.46 - val setT = Term.fastype_of set;
30.47 - val rhs_tfrees = Term.add_tfrees set [];
30.48 - val oldT = HOLogic.dest_setT setT handle TYPE _ =>
30.49 - error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
30.50 -
30.51 - (*goal*)
30.52 - val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
30.53 - val goal_nonempty =
30.54 - HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
30.55 - val goal_admissible =
30.56 - HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
30.57 -
30.58 - (*lhs*)
30.59 - val defS = Sign.defaultS thy;
30.60 - val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
30.61 - val lhs_sorts = map snd lhs_tfrees;
30.62 -
30.63 - val tname = Binding.map_name (Syntax.type_name mx) t;
30.64 - val full_tname = full tname;
30.65 - val newT = Type (full_tname, map TFree lhs_tfrees);
30.66 -
30.67 - val (Rep_name, Abs_name) =
30.68 - (case opt_morphs of
30.69 - NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
30.70 - | SOME morphs => morphs);
30.71 - val RepC = Const (full Rep_name, newT --> oldT);
30.72 - fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
30.73 - val below_def = Logic.mk_equals (belowC newT,
30.74 - Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
30.75 -
30.76 - fun make_po tac thy1 =
30.77 - let
30.78 - val ((_, {type_definition, set_def, ...}), thy2) = thy1
30.79 - |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
30.80 - val lthy3 = thy2
30.81 - |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
30.82 - val below_def' = Syntax.check_term lthy3 below_def;
30.83 - val ((_, (_, below_definition')), lthy4) = lthy3
30.84 - |> Specification.definition (NONE,
30.85 - ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
30.86 - val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
30.87 - val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
30.88 - val thy5 = lthy4
30.89 - |> Class.prove_instantiation_instance
30.90 - (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
30.91 - |> LocalTheory.exit_global;
30.92 - in ((type_definition, below_definition, set_def), thy5) end;
30.93 -
30.94 - fun make_cpo admissible (type_def, below_def, set_def) theory =
30.95 - let
30.96 - val admissible' = fold_rule (the_list set_def) admissible;
30.97 - val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
30.98 - val theory' = theory
30.99 - |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
30.100 - (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
30.101 - val cpo_thms' = map (Thm.transfer theory') cpo_thms;
30.102 - in
30.103 - theory'
30.104 - |> Sign.add_path (Binding.name_of name)
30.105 - |> PureThy.add_thms
30.106 - ([((Binding.prefix_name "adm_" name, admissible'), []),
30.107 - ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
30.108 - ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
30.109 - ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
30.110 - ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
30.111 - ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
30.112 - |> snd
30.113 - |> Sign.parent_path
30.114 - end;
30.115 -
30.116 - fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
30.117 - let
30.118 - val UU_mem' = fold_rule (the_list set_def) UU_mem;
30.119 - val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
30.120 - val theory' = theory
30.121 - |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
30.122 - (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
30.123 - val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
30.124 - in
30.125 - theory'
30.126 - |> Sign.add_path (Binding.name_of name)
30.127 - |> PureThy.add_thms
30.128 - ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
30.129 - ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
30.130 - ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
30.131 - ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
30.132 - ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
30.133 - ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
30.134 - |> snd
30.135 - |> Sign.parent_path
30.136 - end;
30.137 -
30.138 - fun pcpodef_result UU_mem admissible =
30.139 - make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
30.140 - #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
30.141 -
30.142 - fun cpodef_result nonempty admissible =
30.143 - make_po (Tactic.rtac nonempty 1)
30.144 - #-> make_cpo admissible;
30.145 - in
30.146 - if pcpo
30.147 - then (goal_UU_mem, goal_admissible, pcpodef_result)
30.148 - else (goal_nonempty, goal_admissible, cpodef_result)
30.149 - end
30.150 - handle ERROR msg =>
30.151 - cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
30.152 -
30.153 -
30.154 -(* proof interface *)
30.155 -
30.156 -local
30.157 -
30.158 -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
30.159 - let
30.160 - val (goal1, goal2, make_result) =
30.161 - prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
30.162 - fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
30.163 - in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
30.164 -
30.165 -in
30.166 -
30.167 -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
30.168 -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
30.169 -
30.170 -fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
30.171 -fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
30.172 -
30.173 -end;
30.174 -
30.175 -
30.176 -
30.177 -(** outer syntax **)
30.178 -
30.179 -local structure P = OuterParse and K = OuterKeyword in
30.180 -
30.181 -val typedef_proof_decl =
30.182 - Scan.optional (P.$$$ "(" |--
30.183 - ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
30.184 - --| P.$$$ ")") (true, NONE) --
30.185 - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
30.186 - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
30.187 -
30.188 -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
30.189 - (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
30.190 - ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
30.191 -
30.192 -val _ =
30.193 - OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
30.194 - (typedef_proof_decl >>
30.195 - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
30.196 -
30.197 -val _ =
30.198 - OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
30.199 - (typedef_proof_decl >>
30.200 - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
30.201 -
30.202 -end;
30.203 -
30.204 -end;