1.1 --- a/doc-src/Codegen/Thy/ML.thy Thu May 14 15:09:47 2009 +0200
1.2 +++ b/doc-src/Codegen/Thy/ML.thy Thu May 14 15:09:48 2009 +0200
1.3 @@ -78,16 +78,16 @@
1.4
1.5 text %mlref {*
1.6 \begin{mldecls}
1.7 - @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
1.8 - @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\
1.9 + @{index_ML Code.read_const: "theory -> string -> string"} \\
1.10 + @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
1.11 \end{mldecls}
1.12
1.13 \begin{description}
1.14
1.15 - \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
1.16 + \item @{ML Code.read_const}~@{text thy}~@{text s}
1.17 reads a constant as a concrete term expression @{text s}.
1.18
1.19 - \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm}
1.20 + \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
1.21 rewrites a code equation @{text thm} with a simpset @{text ss};
1.22 only arguments and right hand side are rewritten,
1.23 not the head of the code equation.
2.1 --- a/doc-src/Codegen/Thy/document/Codegen.tex Thu May 14 15:09:47 2009 +0200
2.2 +++ b/doc-src/Codegen/Thy/document/Codegen.tex Thu May 14 15:09:48 2009 +0200
2.3 @@ -1550,20 +1550,20 @@
2.4 %
2.5 \begin{isamarkuptext}%
2.6 \begin{mldecls}
2.7 - \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
2.8 - \indexml{Code\_Unit.head\_func}\verb|Code_Unit.head_func: thm -> string * ((string * sort) list * typ)| \\
2.9 - \indexml{Code\_Unit.rewrite\_func}\verb|Code_Unit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\
2.10 + \indexml{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\
2.11 + \indexml{Code\_Unit.head\_func}\verb|Code.head_func: thm -> string * ((string * sort) list * typ)| \\
2.12 + \indexml{Code\_Unit.rewrite\_func}\verb|Code.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\
2.13 \end{mldecls}
2.14
2.15 \begin{description}
2.16
2.17 - \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
2.18 + \item \verb|Code.read_const|~\isa{thy}~\isa{s}
2.19 reads a constant as a concrete term expression \isa{s}.
2.20
2.21 - \item \verb|Code_Unit.head_func|~\isa{thm}
2.22 + \item \verb|Code.head_func|~\isa{thm}
2.23 extracts the constant and its type from a defining equation \isa{thm}.
2.24
2.25 - \item \verb|Code_Unit.rewrite_func|~\isa{ss}~\isa{thm}
2.26 + \item \verb|Code.rewrite_func|~\isa{ss}~\isa{thm}
2.27 rewrites a defining equation \isa{thm} with a simpset \isa{ss};
2.28 only arguments and right hand side are rewritten,
2.29 not the head of the defining equation.
3.1 --- a/doc-src/Codegen/Thy/document/ML.tex Thu May 14 15:09:47 2009 +0200
3.2 +++ b/doc-src/Codegen/Thy/document/ML.tex Thu May 14 15:09:48 2009 +0200
3.3 @@ -124,16 +124,16 @@
3.4 %
3.5 \begin{isamarkuptext}%
3.6 \begin{mldecls}
3.7 - \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
3.8 - \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
3.9 + \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\
3.10 + \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
3.11 \end{mldecls}
3.12
3.13 \begin{description}
3.14
3.15 - \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
3.16 + \item \verb|Code.read_const|~\isa{thy}~\isa{s}
3.17 reads a constant as a concrete term expression \isa{s}.
3.18
3.19 - \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
3.20 + \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
3.21 rewrites a code equation \isa{thm} with a simpset \isa{ss};
3.22 only arguments and right hand side are rewritten,
3.23 not the head of the code equation.
4.1 --- a/doc-src/more_antiquote.ML Thu May 14 15:09:47 2009 +0200
4.2 +++ b/doc-src/more_antiquote.ML Thu May 14 15:09:48 2009 +0200
4.3 @@ -87,7 +87,7 @@
4.4 fun pretty_code_thm src ctxt raw_const =
4.5 let
4.6 val thy = ProofContext.theory_of ctxt;
4.7 - val const = Code_Unit.check_const thy raw_const;
4.8 + val const = Code.check_const thy raw_const;
4.9 val (_, funcgr) = Code_Preproc.obtain thy [const] [];
4.10 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
4.11 val thms = Code_Preproc.eqns funcgr const
4.12 @@ -108,7 +108,7 @@
4.13 local
4.14
4.15 val parse_const_terms = Scan.repeat1 Args.term
4.16 - >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts);
4.17 + >> (fn ts => fn thy => map (Code.check_const thy) ts);
4.18 val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms
4.19 >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy));
4.20 val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name)
5.1 --- a/src/HOL/HOL.thy Thu May 14 15:09:47 2009 +0200
5.2 +++ b/src/HOL/HOL.thy Thu May 14 15:09:48 2009 +0200
5.3 @@ -1871,7 +1871,7 @@
5.4 declare simp_thms(6) [code nbe]
5.5
5.6 setup {*
5.7 - Code_Unit.add_const_alias @{thm equals_eq}
5.8 + Code.add_const_alias @{thm equals_eq}
5.9 *}
5.10
5.11 hide (open) const eq
6.1 --- a/src/HOL/Tools/datatype_codegen.ML Thu May 14 15:09:47 2009 +0200
6.2 +++ b/src/HOL/Tools/datatype_codegen.ML Thu May 14 15:09:48 2009 +0200
6.3 @@ -413,7 +413,7 @@
6.4 let
6.5 val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
6.6 val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
6.7 - in if is_some (try (Code_Unit.constrset_of_consts thy) cs')
6.8 + in if is_some (try (Code.constrset_of_consts thy) cs')
6.9 then SOME cs
6.10 else NONE
6.11 end;
7.1 --- a/src/HOL/Tools/recfun_codegen.ML Thu May 14 15:09:47 2009 +0200
7.2 +++ b/src/HOL/Tools/recfun_codegen.ML Thu May 14 15:09:48 2009 +0200
7.3 @@ -26,10 +26,10 @@
7.4 fun add_thm NONE thm thy = Code.add_eqn thm thy
7.5 | add_thm (SOME module_name) thm thy =
7.6 let
7.7 - val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true)
7.8 + val (thm', _) = Code.mk_eqn thy (K false) (thm, true)
7.9 in
7.10 thy
7.11 - |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name))
7.12 + |> ModuleData.map (Symtab.update (Code.const_eqn thy thm', module_name))
7.13 |> Code.add_eqn thm'
7.14 end;
7.15
7.16 @@ -44,10 +44,10 @@
7.17 fun expand_eta thy [] = []
7.18 | expand_eta thy (thms as thm :: _) =
7.19 let
7.20 - val (_, ty) = Code_Unit.const_typ_eqn thm;
7.21 + val (_, ty) = Code.const_typ_eqn thm;
7.22 in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
7.23 then thms
7.24 - else map (Code_Unit.expand_eta thy 1) thms
7.25 + else map (Code.expand_eta thy 1) thms
7.26 end;
7.27
7.28 fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
7.29 @@ -58,7 +58,7 @@
7.30 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
7.31 |> expand_eta thy
7.32 |> map_filter (meta_eq_to_obj_eq thy)
7.33 - |> Code_Unit.norm_varnames thy
7.34 + |> Code.norm_varnames thy
7.35 |> map (rpair opt_name)
7.36 in if null thms then NONE else SOME thms end;
7.37
8.1 --- a/src/HOL/ex/predicate_compile.ML Thu May 14 15:09:47 2009 +0200
8.2 +++ b/src/HOL/ex/predicate_compile.ML Thu May 14 15:09:48 2009 +0200
8.3 @@ -1405,7 +1405,7 @@
8.4 in
8.5
8.6 val code_pred = generic_code_pred (K I);
8.7 -val code_pred_cmd = generic_code_pred Code_Unit.read_const
8.8 +val code_pred_cmd = generic_code_pred Code.read_const
8.9
8.10 val setup =
8.11 Attrib.setup @{binding code_ind_intros} (Scan.succeed (attrib add_intro_thm))
9.1 --- a/src/Pure/IsaMakefile Thu May 14 15:09:47 2009 +0200
9.2 +++ b/src/Pure/IsaMakefile Thu May 14 15:09:48 2009 +0200
9.3 @@ -56,7 +56,7 @@
9.4 General/table.ML General/url.ML General/xml.ML General/yxml.ML \
9.5 Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
9.6 Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
9.7 - Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
9.8 + Isar/constdefs.ML Isar/context_rules.ML \
9.9 Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
9.10 Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
9.11 Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
10.1 --- a/src/Pure/Isar/ROOT.ML Thu May 14 15:09:47 2009 +0200
10.2 +++ b/src/Pure/Isar/ROOT.ML Thu May 14 15:09:48 2009 +0200
10.3 @@ -61,7 +61,6 @@
10.4 use "../simplifier.ML";
10.5
10.6 (*executable theory content*)
10.7 -use "code_unit.ML";
10.8 use "code.ML";
10.9
10.10 (*specifications*)
11.1 --- a/src/Pure/Isar/code.ML Thu May 14 15:09:47 2009 +0200
11.2 +++ b/src/Pure/Isar/code.ML Thu May 14 15:09:48 2009 +0200
11.3 @@ -7,6 +7,55 @@
11.4
11.5 signature CODE =
11.6 sig
11.7 + (*constructor sets*)
11.8 + val constrset_of_consts: theory -> (string * typ) list
11.9 + -> string * ((string * sort) list * (string * typ list) list)
11.10 +
11.11 + (*typ instantiations*)
11.12 + val typscheme: theory -> string * typ -> (string * sort) list * typ
11.13 + val inst_thm: theory -> sort Vartab.table -> thm -> thm
11.14 +
11.15 + (*constants*)
11.16 + val string_of_typ: theory -> typ -> string
11.17 + val string_of_const: theory -> string -> string
11.18 + val no_args: theory -> string -> int
11.19 + val check_const: theory -> term -> string
11.20 + val read_bare_const: theory -> string -> string * typ
11.21 + val read_const: theory -> string -> string
11.22 +
11.23 + (*constant aliasses*)
11.24 + val add_const_alias: thm -> theory -> theory
11.25 + val triv_classes: theory -> class list
11.26 + val resubst_alias: theory -> string -> string
11.27 +
11.28 + (*code equations*)
11.29 + val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
11.30 + val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
11.31 + val assert_eqn: theory -> thm * bool -> thm * bool
11.32 + val assert_eqns_const: theory -> string
11.33 + -> (thm * bool) list -> (thm * bool) list
11.34 + val const_typ_eqn: thm -> string * typ
11.35 + val const_eqn: theory -> thm -> string
11.36 + val typscheme_eqn: theory -> thm -> (string * sort) list * typ
11.37 + val expand_eta: theory -> int -> thm -> thm
11.38 + val rewrite_eqn: simpset -> thm -> thm
11.39 + val rewrite_head: thm list -> thm -> thm
11.40 + val norm_args: theory -> thm list -> thm list
11.41 + val norm_varnames: theory -> thm list -> thm list
11.42 +
11.43 + (*case certificates*)
11.44 + val case_cert: thm -> string * (int * string list)
11.45 +
11.46 + (*infrastructure*)
11.47 + val add_attribute: string * attribute parser -> theory -> theory
11.48 + val purge_data: theory -> theory
11.49 +
11.50 + (*executable content*)
11.51 + val add_datatype: (string * typ) list -> theory -> theory
11.52 + val add_datatype_cmd: string list -> theory -> theory
11.53 + val type_interpretation:
11.54 + (string * ((string * sort) list * (string * typ list) list)
11.55 + -> theory -> theory) -> theory -> theory
11.56 val add_eqn: thm -> theory -> theory
11.57 val add_nbe_eqn: thm -> theory -> theory
11.58 val add_default_eqn: thm -> theory -> theory
11.59 @@ -15,27 +64,16 @@
11.60 val del_eqn: thm -> theory -> theory
11.61 val del_eqns: string -> theory -> theory
11.62 val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
11.63 - val add_datatype: (string * typ) list -> theory -> theory
11.64 - val add_datatype_cmd: string list -> theory -> theory
11.65 - val type_interpretation:
11.66 - (string * ((string * sort) list * (string * typ list) list)
11.67 - -> theory -> theory) -> theory -> theory
11.68 val add_case: thm -> theory -> theory
11.69 val add_undefined: string -> theory -> theory
11.70 - val purge_data: theory -> theory
11.71
11.72 - val these_eqns: theory -> string -> (thm * bool) list
11.73 + (*data retrieval*)
11.74 val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
11.75 val get_datatype_of_constr: theory -> string -> string option
11.76 + val default_typscheme: theory -> string -> (string * sort) list * typ
11.77 + val these_eqns: theory -> string -> (thm * bool) list
11.78 val get_case_scheme: theory -> string -> (int * (int * string list)) option
11.79 val is_undefined: theory -> string -> bool
11.80 - val default_typscheme: theory -> string -> (string * sort) list * typ
11.81 - val assert_eqn: theory -> thm * bool -> thm * bool
11.82 - val assert_eqns_const: theory -> string
11.83 - -> (thm * bool) list -> (thm * bool) list
11.84 -
11.85 - val add_attribute: string * attribute parser -> theory -> theory
11.86 -
11.87 val print_codesetup: theory -> unit
11.88 end;
11.89
11.90 @@ -70,6 +108,400 @@
11.91 structure Code : PRIVATE_CODE =
11.92 struct
11.93
11.94 +(* auxiliary *)
11.95 +
11.96 +fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
11.97 +fun string_of_const thy c = case AxClass.inst_of_param thy c
11.98 + of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
11.99 + | NONE => Sign.extern_const thy c;
11.100 +
11.101 +fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;
11.102 +
11.103 +
11.104 +(* utilities *)
11.105 +
11.106 +fun typscheme thy (c, ty) =
11.107 + let
11.108 + val ty' = Logic.unvarifyT ty;
11.109 + fun dest (TFree (v, sort)) = (v, sort)
11.110 + | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty);
11.111 + val vs = map dest (Sign.const_typargs thy (c, ty'));
11.112 + in (vs, Type.strip_sorts ty') end;
11.113 +
11.114 +fun inst_thm thy tvars' thm =
11.115 + let
11.116 + val tvars = (Term.add_tvars o Thm.prop_of) thm [];
11.117 + val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
11.118 + fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
11.119 + of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
11.120 + (tvar, (v, inter_sort (sort, sort'))))
11.121 + | NONE => NONE;
11.122 + val insts = map_filter mk_inst tvars;
11.123 + in Thm.instantiate (insts, []) thm end;
11.124 +
11.125 +fun expand_eta thy k thm =
11.126 + let
11.127 + val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
11.128 + val (head, args) = strip_comb lhs;
11.129 + val l = if k = ~1
11.130 + then (length o fst o strip_abs) rhs
11.131 + else Int.max (0, k - length args);
11.132 + val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
11.133 + fun get_name _ 0 = pair []
11.134 + | get_name (Abs (v, ty, t)) k =
11.135 + Name.variants [v]
11.136 + ##>> get_name t (k - 1)
11.137 + #>> (fn ([v'], vs') => (v', ty) :: vs')
11.138 + | get_name t k =
11.139 + let
11.140 + val (tys, _) = (strip_type o fastype_of) t
11.141 + in case tys
11.142 + of [] => raise TERM ("expand_eta", [t])
11.143 + | ty :: _ =>
11.144 + Name.variants [""]
11.145 + #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
11.146 + #>> (fn vs' => (v, ty) :: vs'))
11.147 + end;
11.148 + val (vs, _) = get_name rhs l used;
11.149 + fun expand (v, ty) thm = Drule.fun_cong_rule thm
11.150 + (Thm.cterm_of thy (Var ((v, 0), ty)));
11.151 + in
11.152 + thm
11.153 + |> fold expand vs
11.154 + |> Conv.fconv_rule Drule.beta_eta_conversion
11.155 + end;
11.156 +
11.157 +fun eqn_conv conv =
11.158 + let
11.159 + fun lhs_conv ct = if can Thm.dest_comb ct
11.160 + then (Conv.combination_conv lhs_conv conv) ct
11.161 + else Conv.all_conv ct;
11.162 + in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
11.163 +
11.164 +fun head_conv conv =
11.165 + let
11.166 + fun lhs_conv ct = if can Thm.dest_comb ct
11.167 + then (Conv.fun_conv lhs_conv) ct
11.168 + else conv ct;
11.169 + in Conv.fun_conv (Conv.arg_conv lhs_conv) end;
11.170 +
11.171 +val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
11.172 +val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
11.173 +
11.174 +fun norm_args thy thms =
11.175 + let
11.176 + val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
11.177 + val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
11.178 + in
11.179 + thms
11.180 + |> map (expand_eta thy k)
11.181 + |> map (Conv.fconv_rule Drule.beta_eta_conversion)
11.182 + end;
11.183 +
11.184 +fun canonical_tvars thy thm =
11.185 + let
11.186 + val ctyp = Thm.ctyp_of thy;
11.187 + val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
11.188 + fun tvars_subst_for thm = (fold_types o fold_atyps)
11.189 + (fn TVar (v_i as (v, _), sort) => let
11.190 + val v' = purify_tvar v
11.191 + in if v = v' then I
11.192 + else insert (op =) (v_i, (v', sort)) end
11.193 + | _ => I) (prop_of thm) [];
11.194 + fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
11.195 + let
11.196 + val ty = TVar (v_i, sort)
11.197 + in
11.198 + (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
11.199 + end;
11.200 + val maxidx = Thm.maxidx_of thm + 1;
11.201 + val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
11.202 + in Thm.instantiate (inst, []) thm end;
11.203 +
11.204 +fun canonical_vars thy thm =
11.205 + let
11.206 + val cterm = Thm.cterm_of thy;
11.207 + val purify_var = Name.desymbolize false;
11.208 + fun vars_subst_for thm = fold_aterms
11.209 + (fn Var (v_i as (v, _), ty) => let
11.210 + val v' = purify_var v
11.211 + in if v = v' then I
11.212 + else insert (op =) (v_i, (v', ty)) end
11.213 + | _ => I) (prop_of thm) [];
11.214 + fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
11.215 + let
11.216 + val t = Var (v_i, ty)
11.217 + in
11.218 + (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
11.219 + end;
11.220 + val maxidx = Thm.maxidx_of thm + 1;
11.221 + val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
11.222 + in Thm.instantiate ([], inst) thm end;
11.223 +
11.224 +fun canonical_absvars thm =
11.225 + let
11.226 + val t = Thm.plain_prop_of thm;
11.227 + val purify_var = Name.desymbolize false;
11.228 + val t' = Term.map_abs_vars purify_var t;
11.229 + in Thm.rename_boundvars t t' thm end;
11.230 +
11.231 +fun norm_varnames thy thms =
11.232 + let
11.233 + fun burrow_thms f [] = []
11.234 + | burrow_thms f thms =
11.235 + thms
11.236 + |> Conjunction.intr_balanced
11.237 + |> f
11.238 + |> Conjunction.elim_balanced (length thms)
11.239 + in
11.240 + thms
11.241 + |> map (canonical_vars thy)
11.242 + |> map canonical_absvars
11.243 + |> map Drule.zero_var_indexes
11.244 + |> burrow_thms (canonical_tvars thy)
11.245 + |> Drule.zero_var_indexes_list
11.246 + end;
11.247 +
11.248 +
11.249 +(* const aliasses *)
11.250 +
11.251 +structure ConstAlias = TheoryDataFun
11.252 +(
11.253 + type T = ((string * string) * thm) list * class list;
11.254 + val empty = ([], []);
11.255 + val copy = I;
11.256 + val extend = I;
11.257 + fun merge _ ((alias1, classes1), (alias2, classes2)) : T =
11.258 + (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2),
11.259 + Library.merge (op =) (classes1, classes2));
11.260 +);
11.261 +
11.262 +fun add_const_alias thm thy =
11.263 + let
11.264 + val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm)
11.265 + of SOME lhs_rhs => lhs_rhs
11.266 + | _ => error ("Not an equation: " ^ Display.string_of_thm thm);
11.267 + val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
11.268 + of SOME c_c' => c_c'
11.269 + | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm);
11.270 + val some_class = the_list (AxClass.class_of_param thy (snd c_c'));
11.271 + in thy |>
11.272 + ConstAlias.map (fn (alias, classes) =>
11.273 + ((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
11.274 + end;
11.275 +
11.276 +fun resubst_alias thy =
11.277 + let
11.278 + val alias = fst (ConstAlias.get thy);
11.279 + val subst_inst_param = Option.map fst o AxClass.inst_of_param thy;
11.280 + fun subst_alias c =
11.281 + get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias;
11.282 + in
11.283 + perhaps subst_inst_param
11.284 + #> perhaps subst_alias
11.285 + end;
11.286 +
11.287 +val triv_classes = snd o ConstAlias.get;
11.288 +
11.289 +
11.290 +(* reading constants as terms *)
11.291 +
11.292 +fun check_bare_const thy t = case try dest_Const t
11.293 + of SOME c_ty => c_ty
11.294 + | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
11.295 +
11.296 +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
11.297 +
11.298 +fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
11.299 +
11.300 +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
11.301 +
11.302 +
11.303 +(* constructor sets *)
11.304 +
11.305 +fun constrset_of_consts thy cs =
11.306 + let
11.307 + val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
11.308 + then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
11.309 + fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c
11.310 + ^ " :: " ^ string_of_typ thy ty);
11.311 + fun last_typ c_ty ty =
11.312 + let
11.313 + val frees = OldTerm.typ_tfrees ty;
11.314 + val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
11.315 + handle TYPE _ => no_constr c_ty
11.316 + val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
11.317 + val _ = if length frees <> length vs then no_constr c_ty else ();
11.318 + in (tyco, vs) end;
11.319 + fun ty_sorts (c, ty) =
11.320 + let
11.321 + val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
11.322 + val (tyco, _) = last_typ (c, ty) ty_decl;
11.323 + val (_, vs) = last_typ (c, ty) ty;
11.324 + in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
11.325 + fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
11.326 + let
11.327 + val _ = if tyco' <> tyco
11.328 + then error "Different type constructors in constructor set"
11.329 + else ();
11.330 + val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
11.331 + in ((tyco, sorts), c :: cs) end;
11.332 + fun inst vs' (c, (vs, ty)) =
11.333 + let
11.334 + val the_v = the o AList.lookup (op =) (vs ~~ vs');
11.335 + val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
11.336 + in (c, (fst o strip_type) ty') end;
11.337 + val c' :: cs' = map ty_sorts cs;
11.338 + val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
11.339 + val vs = Name.names Name.context Name.aT sorts;
11.340 + val cs''' = map (inst vs) cs'';
11.341 + in (tyco, (vs, rev cs''')) end;
11.342 +
11.343 +
11.344 +(* code equations *)
11.345 +
11.346 +exception BAD_THM of string;
11.347 +fun bad_thm msg = raise BAD_THM msg;
11.348 +fun error_thm f thm = f thm handle BAD_THM msg => error msg;
11.349 +fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
11.350 +
11.351 +fun is_linear thm =
11.352 + let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
11.353 + in not (has_duplicates (op =) ((fold o fold_aterms)
11.354 + (fn Var (v, _) => cons v | _ => I) args [])) end;
11.355 +
11.356 +fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) =
11.357 + let
11.358 + val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
11.359 + handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
11.360 + | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
11.361 + fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
11.362 + | Free _ => bad_thm ("Illegal free variable in equation\n"
11.363 + ^ Display.string_of_thm thm)
11.364 + | _ => I) t [];
11.365 + fun tvars_of t = fold_term_types (fn _ =>
11.366 + fold_atyps (fn TVar (v, _) => insert (op =) v
11.367 + | TFree _ => bad_thm
11.368 + ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
11.369 + val lhs_vs = vars_of lhs;
11.370 + val rhs_vs = vars_of rhs;
11.371 + val lhs_tvs = tvars_of lhs;
11.372 + val rhs_tvs = tvars_of rhs;
11.373 + val _ = if null (subtract (op =) lhs_vs rhs_vs)
11.374 + then ()
11.375 + else bad_thm ("Free variables on right hand side of equation\n"
11.376 + ^ Display.string_of_thm thm);
11.377 + val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
11.378 + then ()
11.379 + else bad_thm ("Free type variables on right hand side of equation\n"
11.380 + ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
11.381 + val (c, ty) = case head
11.382 + of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
11.383 + | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
11.384 + fun check _ (Abs _) = bad_thm
11.385 + ("Abstraction on left hand side of equation\n"
11.386 + ^ Display.string_of_thm thm)
11.387 + | check 0 (Var _) = ()
11.388 + | check _ (Var _) = bad_thm
11.389 + ("Variable with application on left hand side of equation\n"
11.390 + ^ Display.string_of_thm thm)
11.391 + | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
11.392 + | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
11.393 + then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
11.394 + then ()
11.395 + else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
11.396 + ^ Display.string_of_thm thm)
11.397 + else bad_thm
11.398 + ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
11.399 + ^ Display.string_of_thm thm);
11.400 + val _ = map (check 0) args;
11.401 + val _ = if not proper orelse is_linear thm then ()
11.402 + else bad_thm ("Duplicate variables on left hand side of equation\n"
11.403 + ^ Display.string_of_thm thm);
11.404 + val _ = if (is_none o AxClass.class_of_param thy) c
11.405 + then ()
11.406 + else bad_thm ("Polymorphic constant as head in equation\n"
11.407 + ^ Display.string_of_thm thm)
11.408 + val _ = if not (is_constr_head c)
11.409 + then ()
11.410 + else bad_thm ("Constructor as head in equation\n"
11.411 + ^ Display.string_of_thm thm)
11.412 + val ty_decl = Sign.the_const_type thy c;
11.413 + val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
11.414 + then () else bad_thm ("Type\n" ^ string_of_typ thy ty
11.415 + ^ "\nof equation\n"
11.416 + ^ Display.string_of_thm thm
11.417 + ^ "\nis incompatible with declared function type\n"
11.418 + ^ string_of_typ thy ty_decl)
11.419 + in (thm, proper) end;
11.420 +
11.421 +fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr);
11.422 +
11.423 +val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
11.424 +
11.425 +
11.426 +(*those following are permissive wrt. to overloaded constants!*)
11.427 +
11.428 +fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
11.429 + apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
11.430 +
11.431 +fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
11.432 + o try_thm (gen_assert_eqn thy is_constr_head (K true))
11.433 + o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
11.434 +
11.435 +fun const_typ_eqn_unoverload thy thm =
11.436 + let
11.437 + val (c, ty) = const_typ_eqn thm;
11.438 + val c' = AxClass.unoverload_const thy (c, ty);
11.439 + in (c', ty) end;
11.440 +
11.441 +fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy;
11.442 +fun const_eqn thy = fst o const_typ_eqn_unoverload thy;
11.443 +
11.444 +
11.445 +(* case cerificates *)
11.446 +
11.447 +fun case_certificate thm =
11.448 + let
11.449 + val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
11.450 + o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
11.451 + val _ = case head of Free _ => true
11.452 + | Var _ => true
11.453 + | _ => raise TERM ("case_cert", []);
11.454 + val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
11.455 + val (Const (case_const, _), raw_params) = strip_comb case_expr;
11.456 + val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params;
11.457 + val _ = if n = ~1 then raise TERM ("case_cert", []) else ();
11.458 + val params = map (fst o dest_Var) (nth_drop n raw_params);
11.459 + fun dest_case t =
11.460 + let
11.461 + val (head' $ t_co, rhs) = Logic.dest_equals t;
11.462 + val _ = if head' = head then () else raise TERM ("case_cert", []);
11.463 + val (Const (co, _), args) = strip_comb t_co;
11.464 + val (Var (param, _), args') = strip_comb rhs;
11.465 + val _ = if args' = args then () else raise TERM ("case_cert", []);
11.466 + in (param, co) end;
11.467 + fun analyze_cases cases =
11.468 + let
11.469 + val co_list = fold (AList.update (op =) o dest_case) cases [];
11.470 + in map (the o AList.lookup (op =) co_list) params end;
11.471 + fun analyze_let t =
11.472 + let
11.473 + val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
11.474 + val _ = if head' = head then () else raise TERM ("case_cert", []);
11.475 + val _ = if arg' = arg then () else raise TERM ("case_cert", []);
11.476 + val _ = if [param'] = params then () else raise TERM ("case_cert", []);
11.477 + in [] end;
11.478 + fun analyze (cases as [let_case]) =
11.479 + (analyze_cases cases handle Bind => analyze_let let_case)
11.480 + | analyze cases = analyze_cases cases;
11.481 + in (case_const, (n, analyze cases)) end;
11.482 +
11.483 +fun case_cert thm = case_certificate thm
11.484 + handle Bind => error "bad case certificate"
11.485 + | TERM _ => error "bad case certificate";
11.486 +
11.487 +
11.488 (** code attributes **)
11.489
11.490 structure CodeAttr = TheoryDataFun (
11.491 @@ -333,16 +765,16 @@
11.492 (Pretty.block o Pretty.breaks) (
11.493 Pretty.str s
11.494 :: Pretty.str "="
11.495 - :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (Code_Unit.string_of_const thy c)
11.496 + :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
11.497 | (c, tys) =>
11.498 (Pretty.block o Pretty.breaks)
11.499 - (Pretty.str (Code_Unit.string_of_const thy c)
11.500 + (Pretty.str (string_of_const thy c)
11.501 :: Pretty.str "of"
11.502 :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
11.503 );
11.504 val eqns = the_eqns exec
11.505 |> Symtab.dest
11.506 - |> (map o apfst) (Code_Unit.string_of_const thy)
11.507 + |> (map o apfst) (string_of_const thy)
11.508 |> (map o apsnd) (snd o fst)
11.509 |> sort (string_ord o pairself fst);
11.510 val dtyps = the_dtyps exec
11.511 @@ -378,13 +810,13 @@
11.512 val max' = Thm.maxidx_of thm' + 1;
11.513 in (thm', max') end;
11.514 val (thms', maxidx) = fold_map incr_thm thms 0;
11.515 - val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms';
11.516 + val ty1 :: tys = map (snd o const_typ_eqn) thms';
11.517 fun unify ty env = Sign.typ_unify thy (ty1, ty) env
11.518 handle Type.TUNIFY =>
11.519 error ("Type unificaton failed, while unifying code equations\n"
11.520 ^ (cat_lines o map Display.string_of_thm) thms
11.521 ^ "\nwith types\n"
11.522 - ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys));
11.523 + ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
11.524 val (env, _) = fold unify tys (Vartab.empty, maxidx)
11.525 val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
11.526 cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
11.527 @@ -409,13 +841,13 @@
11.528
11.529 fun is_constr thy = is_some o get_datatype_of_constr thy;
11.530
11.531 -fun assert_eqn thy = Code_Unit.assert_eqn thy (is_constr thy);
11.532 +val assert_eqn = fn thy => assert_eqn thy (is_constr thy);
11.533
11.534 fun assert_eqns_const thy c eqns =
11.535 let
11.536 - fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm
11.537 + fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
11.538 then eqn else error ("Wrong head of code equation,\nexpected constant "
11.539 - ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
11.540 + ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
11.541 in map (cert o assert_eqn thy) eqns end;
11.542
11.543 fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
11.544 @@ -423,19 +855,19 @@
11.545 o apfst) (fn (_, eqns) => (true, f eqns));
11.546
11.547 fun gen_add_eqn default (eqn as (thm, _)) thy =
11.548 - let val c = Code_Unit.const_eqn thy thm
11.549 + let val c = const_eqn thy thm
11.550 in change_eqns false c (add_thm thy default eqn) thy end;
11.551
11.552 fun add_eqn thm thy =
11.553 - gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, true)) thy;
11.554 + gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy;
11.555
11.556 fun add_default_eqn thm thy =
11.557 - case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
11.558 + case mk_eqn_liberal thy (is_constr thy) thm
11.559 of SOME eqn => gen_add_eqn true eqn thy
11.560 | NONE => thy;
11.561
11.562 fun add_nbe_eqn thm thy =
11.563 - gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, false)) thy;
11.564 + gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, false)) thy;
11.565
11.566 fun add_eqnl (c, lthms) thy =
11.567 let
11.568 @@ -446,8 +878,8 @@
11.569 (fn thm => Context.mapping (add_default_eqn thm) I);
11.570 val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
11.571
11.572 -fun del_eqn thm thy = case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
11.573 - of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy
11.574 +fun del_eqn thm thy = case mk_eqn_liberal thy (is_constr thy) thm
11.575 + of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
11.576 | NONE => thy;
11.577
11.578 fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
11.579 @@ -461,7 +893,7 @@
11.580 fun add_datatype raw_cs thy =
11.581 let
11.582 val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
11.583 - val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
11.584 + val (tyco, vs_cos) = constrset_of_consts thy cs;
11.585 val old_cs = (map fst o snd o get_datatype thy) tyco;
11.586 fun drop_outdated_cases cases = fold Symtab.delete_safe
11.587 (Symtab.fold (fn (c, (_, (_, cos))) =>
11.588 @@ -481,12 +913,12 @@
11.589
11.590 fun add_datatype_cmd raw_cs thy =
11.591 let
11.592 - val cs = map (Code_Unit.read_bare_const thy) raw_cs;
11.593 + val cs = map (read_bare_const thy) raw_cs;
11.594 in add_datatype cs thy end;
11.595
11.596 fun add_case thm thy =
11.597 let
11.598 - val (c, (k, case_pats)) = Code_Unit.case_cert thm;
11.599 + val (c, (k, case_pats)) = case_cert thm;
11.600 val _ = case filter_out (is_constr thy) case_pats
11.601 of [] => ()
11.602 | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
11.603 @@ -517,7 +949,7 @@
11.604
11.605 fun default_typscheme thy c =
11.606 let
11.607 - fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const
11.608 + fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const
11.609 o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c;
11.610 fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
11.611 in case AxClass.class_of_param thy c
11.612 @@ -525,7 +957,7 @@
11.613 | NONE => if is_constr thy c
11.614 then strip_sorts (the_const_typscheme c)
11.615 else case get_eqns thy c
11.616 - of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm
11.617 + of (thm, _) :: _ => (typscheme_eqn thy o Drule.zero_var_indexes) thm
11.618 | [] => strip_sorts (the_const_typscheme c) end;
11.619
11.620 end; (*struct*)
12.1 --- a/src/Pure/Isar/code_unit.ML Thu May 14 15:09:47 2009 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,444 +0,0 @@
12.4 -(* Title: Pure/Isar/code_unit.ML
12.5 - Author: Florian Haftmann, TU Muenchen
12.6 -
12.7 -Basic notions of code generation. Auxiliary.
12.8 -*)
12.9 -
12.10 -signature CODE_UNIT =
12.11 -sig
12.12 - (*typ instantiations*)
12.13 - val typscheme: theory -> string * typ -> (string * sort) list * typ
12.14 - val inst_thm: theory -> sort Vartab.table -> thm -> thm
12.15 -
12.16 - (*constant aliasses*)
12.17 - val add_const_alias: thm -> theory -> theory
12.18 - val triv_classes: theory -> class list
12.19 - val resubst_alias: theory -> string -> string
12.20 -
12.21 - (*constants*)
12.22 - val string_of_typ: theory -> typ -> string
12.23 - val string_of_const: theory -> string -> string
12.24 - val no_args: theory -> string -> int
12.25 - val check_const: theory -> term -> string
12.26 - val read_bare_const: theory -> string -> string * typ
12.27 - val read_const: theory -> string -> string
12.28 -
12.29 - (*constructor sets*)
12.30 - val constrset_of_consts: theory -> (string * typ) list
12.31 - -> string * ((string * sort) list * (string * typ list) list)
12.32 -
12.33 - (*code equations*)
12.34 - val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
12.35 - val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
12.36 - val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
12.37 - val const_typ_eqn: thm -> string * typ
12.38 - val const_eqn: theory -> thm -> string
12.39 - val typscheme_eqn: theory -> thm -> (string * sort) list * typ
12.40 - val expand_eta: theory -> int -> thm -> thm
12.41 - val rewrite_eqn: simpset -> thm -> thm
12.42 - val rewrite_head: thm list -> thm -> thm
12.43 - val norm_args: theory -> thm list -> thm list
12.44 - val norm_varnames: theory -> thm list -> thm list
12.45 -
12.46 - (*case certificates*)
12.47 - val case_cert: thm -> string * (int * string list)
12.48 -end;
12.49 -
12.50 -structure Code_Unit: CODE_UNIT =
12.51 -struct
12.52 -
12.53 -
12.54 -(* auxiliary *)
12.55 -
12.56 -fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
12.57 -fun string_of_const thy c = case AxClass.inst_of_param thy c
12.58 - of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
12.59 - | NONE => Sign.extern_const thy c;
12.60 -
12.61 -fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;
12.62 -
12.63 -
12.64 -(* utilities *)
12.65 -
12.66 -fun typscheme thy (c, ty) =
12.67 - let
12.68 - val ty' = Logic.unvarifyT ty;
12.69 - fun dest (TFree (v, sort)) = (v, sort)
12.70 - | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty);
12.71 - val vs = map dest (Sign.const_typargs thy (c, ty'));
12.72 - in (vs, Type.strip_sorts ty') end;
12.73 -
12.74 -fun inst_thm thy tvars' thm =
12.75 - let
12.76 - val tvars = (Term.add_tvars o Thm.prop_of) thm [];
12.77 - val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
12.78 - fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
12.79 - of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
12.80 - (tvar, (v, inter_sort (sort, sort'))))
12.81 - | NONE => NONE;
12.82 - val insts = map_filter mk_inst tvars;
12.83 - in Thm.instantiate (insts, []) thm end;
12.84 -
12.85 -fun expand_eta thy k thm =
12.86 - let
12.87 - val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
12.88 - val (head, args) = strip_comb lhs;
12.89 - val l = if k = ~1
12.90 - then (length o fst o strip_abs) rhs
12.91 - else Int.max (0, k - length args);
12.92 - val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
12.93 - fun get_name _ 0 = pair []
12.94 - | get_name (Abs (v, ty, t)) k =
12.95 - Name.variants [v]
12.96 - ##>> get_name t (k - 1)
12.97 - #>> (fn ([v'], vs') => (v', ty) :: vs')
12.98 - | get_name t k =
12.99 - let
12.100 - val (tys, _) = (strip_type o fastype_of) t
12.101 - in case tys
12.102 - of [] => raise TERM ("expand_eta", [t])
12.103 - | ty :: _ =>
12.104 - Name.variants [""]
12.105 - #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
12.106 - #>> (fn vs' => (v, ty) :: vs'))
12.107 - end;
12.108 - val (vs, _) = get_name rhs l used;
12.109 - fun expand (v, ty) thm = Drule.fun_cong_rule thm
12.110 - (Thm.cterm_of thy (Var ((v, 0), ty)));
12.111 - in
12.112 - thm
12.113 - |> fold expand vs
12.114 - |> Conv.fconv_rule Drule.beta_eta_conversion
12.115 - end;
12.116 -
12.117 -fun eqn_conv conv =
12.118 - let
12.119 - fun lhs_conv ct = if can Thm.dest_comb ct
12.120 - then (Conv.combination_conv lhs_conv conv) ct
12.121 - else Conv.all_conv ct;
12.122 - in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
12.123 -
12.124 -fun head_conv conv =
12.125 - let
12.126 - fun lhs_conv ct = if can Thm.dest_comb ct
12.127 - then (Conv.fun_conv lhs_conv) ct
12.128 - else conv ct;
12.129 - in Conv.fun_conv (Conv.arg_conv lhs_conv) end;
12.130 -
12.131 -val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
12.132 -val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
12.133 -
12.134 -fun norm_args thy thms =
12.135 - let
12.136 - val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
12.137 - val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
12.138 - in
12.139 - thms
12.140 - |> map (expand_eta thy k)
12.141 - |> map (Conv.fconv_rule Drule.beta_eta_conversion)
12.142 - end;
12.143 -
12.144 -fun canonical_tvars thy thm =
12.145 - let
12.146 - val ctyp = Thm.ctyp_of thy;
12.147 - val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
12.148 - fun tvars_subst_for thm = (fold_types o fold_atyps)
12.149 - (fn TVar (v_i as (v, _), sort) => let
12.150 - val v' = purify_tvar v
12.151 - in if v = v' then I
12.152 - else insert (op =) (v_i, (v', sort)) end
12.153 - | _ => I) (prop_of thm) [];
12.154 - fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
12.155 - let
12.156 - val ty = TVar (v_i, sort)
12.157 - in
12.158 - (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
12.159 - end;
12.160 - val maxidx = Thm.maxidx_of thm + 1;
12.161 - val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
12.162 - in Thm.instantiate (inst, []) thm end;
12.163 -
12.164 -fun canonical_vars thy thm =
12.165 - let
12.166 - val cterm = Thm.cterm_of thy;
12.167 - val purify_var = Name.desymbolize false;
12.168 - fun vars_subst_for thm = fold_aterms
12.169 - (fn Var (v_i as (v, _), ty) => let
12.170 - val v' = purify_var v
12.171 - in if v = v' then I
12.172 - else insert (op =) (v_i, (v', ty)) end
12.173 - | _ => I) (prop_of thm) [];
12.174 - fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
12.175 - let
12.176 - val t = Var (v_i, ty)
12.177 - in
12.178 - (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
12.179 - end;
12.180 - val maxidx = Thm.maxidx_of thm + 1;
12.181 - val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
12.182 - in Thm.instantiate ([], inst) thm end;
12.183 -
12.184 -fun canonical_absvars thm =
12.185 - let
12.186 - val t = Thm.plain_prop_of thm;
12.187 - val purify_var = Name.desymbolize false;
12.188 - val t' = Term.map_abs_vars purify_var t;
12.189 - in Thm.rename_boundvars t t' thm end;
12.190 -
12.191 -fun norm_varnames thy thms =
12.192 - let
12.193 - fun burrow_thms f [] = []
12.194 - | burrow_thms f thms =
12.195 - thms
12.196 - |> Conjunction.intr_balanced
12.197 - |> f
12.198 - |> Conjunction.elim_balanced (length thms)
12.199 - in
12.200 - thms
12.201 - |> map (canonical_vars thy)
12.202 - |> map canonical_absvars
12.203 - |> map Drule.zero_var_indexes
12.204 - |> burrow_thms (canonical_tvars thy)
12.205 - |> Drule.zero_var_indexes_list
12.206 - end;
12.207 -
12.208 -
12.209 -(* const aliasses *)
12.210 -
12.211 -structure ConstAlias = TheoryDataFun
12.212 -(
12.213 - type T = ((string * string) * thm) list * class list;
12.214 - val empty = ([], []);
12.215 - val copy = I;
12.216 - val extend = I;
12.217 - fun merge _ ((alias1, classes1), (alias2, classes2)) : T =
12.218 - (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2),
12.219 - Library.merge (op =) (classes1, classes2));
12.220 -);
12.221 -
12.222 -fun add_const_alias thm thy =
12.223 - let
12.224 - val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm)
12.225 - of SOME lhs_rhs => lhs_rhs
12.226 - | _ => error ("Not an equation: " ^ Display.string_of_thm thm);
12.227 - val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
12.228 - of SOME c_c' => c_c'
12.229 - | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm);
12.230 - val some_class = the_list (AxClass.class_of_param thy (snd c_c'));
12.231 - in thy |>
12.232 - ConstAlias.map (fn (alias, classes) =>
12.233 - ((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
12.234 - end;
12.235 -
12.236 -fun resubst_alias thy =
12.237 - let
12.238 - val alias = fst (ConstAlias.get thy);
12.239 - val subst_inst_param = Option.map fst o AxClass.inst_of_param thy;
12.240 - fun subst_alias c =
12.241 - get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias;
12.242 - in
12.243 - perhaps subst_inst_param
12.244 - #> perhaps subst_alias
12.245 - end;
12.246 -
12.247 -val triv_classes = snd o ConstAlias.get;
12.248 -
12.249 -
12.250 -(* reading constants as terms *)
12.251 -
12.252 -fun check_bare_const thy t = case try dest_Const t
12.253 - of SOME c_ty => c_ty
12.254 - | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
12.255 -
12.256 -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
12.257 -
12.258 -fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
12.259 -
12.260 -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
12.261 -
12.262 -
12.263 -(* constructor sets *)
12.264 -
12.265 -fun constrset_of_consts thy cs =
12.266 - let
12.267 - val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
12.268 - then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
12.269 - fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c
12.270 - ^ " :: " ^ string_of_typ thy ty);
12.271 - fun last_typ c_ty ty =
12.272 - let
12.273 - val frees = OldTerm.typ_tfrees ty;
12.274 - val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
12.275 - handle TYPE _ => no_constr c_ty
12.276 - val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
12.277 - val _ = if length frees <> length vs then no_constr c_ty else ();
12.278 - in (tyco, vs) end;
12.279 - fun ty_sorts (c, ty) =
12.280 - let
12.281 - val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
12.282 - val (tyco, _) = last_typ (c, ty) ty_decl;
12.283 - val (_, vs) = last_typ (c, ty) ty;
12.284 - in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
12.285 - fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
12.286 - let
12.287 - val _ = if tyco' <> tyco
12.288 - then error "Different type constructors in constructor set"
12.289 - else ();
12.290 - val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
12.291 - in ((tyco, sorts), c :: cs) end;
12.292 - fun inst vs' (c, (vs, ty)) =
12.293 - let
12.294 - val the_v = the o AList.lookup (op =) (vs ~~ vs');
12.295 - val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
12.296 - in (c, (fst o strip_type) ty') end;
12.297 - val c' :: cs' = map ty_sorts cs;
12.298 - val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
12.299 - val vs = Name.names Name.context Name.aT sorts;
12.300 - val cs''' = map (inst vs) cs'';
12.301 - in (tyco, (vs, rev cs''')) end;
12.302 -
12.303 -
12.304 -(* code equations *)
12.305 -
12.306 -exception BAD_THM of string;
12.307 -fun bad_thm msg = raise BAD_THM msg;
12.308 -fun error_thm f thm = f thm handle BAD_THM msg => error msg;
12.309 -fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
12.310 -
12.311 -fun is_linear thm =
12.312 - let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
12.313 - in not (has_duplicates (op =) ((fold o fold_aterms)
12.314 - (fn Var (v, _) => cons v | _ => I) args [])) end;
12.315 -
12.316 -fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) =
12.317 - let
12.318 - val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
12.319 - handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
12.320 - | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
12.321 - fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
12.322 - | Free _ => bad_thm ("Illegal free variable in equation\n"
12.323 - ^ Display.string_of_thm thm)
12.324 - | _ => I) t [];
12.325 - fun tvars_of t = fold_term_types (fn _ =>
12.326 - fold_atyps (fn TVar (v, _) => insert (op =) v
12.327 - | TFree _ => bad_thm
12.328 - ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
12.329 - val lhs_vs = vars_of lhs;
12.330 - val rhs_vs = vars_of rhs;
12.331 - val lhs_tvs = tvars_of lhs;
12.332 - val rhs_tvs = tvars_of rhs;
12.333 - val _ = if null (subtract (op =) lhs_vs rhs_vs)
12.334 - then ()
12.335 - else bad_thm ("Free variables on right hand side of equation\n"
12.336 - ^ Display.string_of_thm thm);
12.337 - val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
12.338 - then ()
12.339 - else bad_thm ("Free type variables on right hand side of equation\n"
12.340 - ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
12.341 - val (c, ty) = case head
12.342 - of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
12.343 - | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
12.344 - fun check _ (Abs _) = bad_thm
12.345 - ("Abstraction on left hand side of equation\n"
12.346 - ^ Display.string_of_thm thm)
12.347 - | check 0 (Var _) = ()
12.348 - | check _ (Var _) = bad_thm
12.349 - ("Variable with application on left hand side of equation\n"
12.350 - ^ Display.string_of_thm thm)
12.351 - | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
12.352 - | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
12.353 - then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
12.354 - then ()
12.355 - else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
12.356 - ^ Display.string_of_thm thm)
12.357 - else bad_thm
12.358 - ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
12.359 - ^ Display.string_of_thm thm);
12.360 - val _ = map (check 0) args;
12.361 - val _ = if not proper orelse is_linear thm then ()
12.362 - else bad_thm ("Duplicate variables on left hand side of equation\n"
12.363 - ^ Display.string_of_thm thm);
12.364 - val _ = if (is_none o AxClass.class_of_param thy) c
12.365 - then ()
12.366 - else bad_thm ("Polymorphic constant as head in equation\n"
12.367 - ^ Display.string_of_thm thm)
12.368 - val _ = if not (is_constr_head c)
12.369 - then ()
12.370 - else bad_thm ("Constructor as head in equation\n"
12.371 - ^ Display.string_of_thm thm)
12.372 - val ty_decl = Sign.the_const_type thy c;
12.373 - val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
12.374 - then () else bad_thm ("Type\n" ^ string_of_typ thy ty
12.375 - ^ "\nof equation\n"
12.376 - ^ Display.string_of_thm thm
12.377 - ^ "\nis incompatible with declared function type\n"
12.378 - ^ string_of_typ thy ty_decl)
12.379 - in (thm, proper) end;
12.380 -
12.381 -fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr);
12.382 -
12.383 -val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
12.384 -
12.385 -
12.386 -(*those following are permissive wrt. to overloaded constants!*)
12.387 -
12.388 -fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
12.389 - apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
12.390 -
12.391 -fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
12.392 - o try_thm (gen_assert_eqn thy is_constr_head (K true))
12.393 - o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
12.394 -
12.395 -fun const_typ_eqn_unoverload thy thm =
12.396 - let
12.397 - val (c, ty) = const_typ_eqn thm;
12.398 - val c' = AxClass.unoverload_const thy (c, ty);
12.399 - in (c', ty) end;
12.400 -
12.401 -fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy;
12.402 -fun const_eqn thy = fst o const_typ_eqn_unoverload thy;
12.403 -
12.404 -
12.405 -(* case cerificates *)
12.406 -
12.407 -fun case_certificate thm =
12.408 - let
12.409 - val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
12.410 - o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
12.411 - val _ = case head of Free _ => true
12.412 - | Var _ => true
12.413 - | _ => raise TERM ("case_cert", []);
12.414 - val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
12.415 - val (Const (case_const, _), raw_params) = strip_comb case_expr;
12.416 - val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params;
12.417 - val _ = if n = ~1 then raise TERM ("case_cert", []) else ();
12.418 - val params = map (fst o dest_Var) (nth_drop n raw_params);
12.419 - fun dest_case t =
12.420 - let
12.421 - val (head' $ t_co, rhs) = Logic.dest_equals t;
12.422 - val _ = if head' = head then () else raise TERM ("case_cert", []);
12.423 - val (Const (co, _), args) = strip_comb t_co;
12.424 - val (Var (param, _), args') = strip_comb rhs;
12.425 - val _ = if args' = args then () else raise TERM ("case_cert", []);
12.426 - in (param, co) end;
12.427 - fun analyze_cases cases =
12.428 - let
12.429 - val co_list = fold (AList.update (op =) o dest_case) cases [];
12.430 - in map (the o AList.lookup (op =) co_list) params end;
12.431 - fun analyze_let t =
12.432 - let
12.433 - val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
12.434 - val _ = if head' = head then () else raise TERM ("case_cert", []);
12.435 - val _ = if arg' = arg then () else raise TERM ("case_cert", []);
12.436 - val _ = if [param'] = params then () else raise TERM ("case_cert", []);
12.437 - in [] end;
12.438 - fun analyze (cases as [let_case]) =
12.439 - (analyze_cases cases handle Bind => analyze_let let_case)
12.440 - | analyze cases = analyze_cases cases;
12.441 - in (case_const, (n, analyze cases)) end;
12.442 -
12.443 -fun case_cert thm = case_certificate thm
12.444 - handle Bind => error "bad case certificate"
12.445 - | TERM _ => error "bad case certificate";
12.446 -
12.447 -end;
13.1 --- a/src/Tools/code/code_haskell.ML Thu May 14 15:09:47 2009 +0200
13.2 +++ b/src/Tools/code/code_haskell.ML Thu May 14 15:09:48 2009 +0200
13.3 @@ -480,7 +480,7 @@
13.4
13.5 fun add_monad target' raw_c_bind thy =
13.6 let
13.7 - val c_bind = Code_Unit.read_const thy raw_c_bind;
13.8 + val c_bind = Code.read_const thy raw_c_bind;
13.9 in if target = target' then
13.10 thy
13.11 |> Code_Target.add_syntax_const target c_bind
14.1 --- a/src/Tools/code/code_ml.ML Thu May 14 15:09:47 2009 +0200
14.2 +++ b/src/Tools/code/code_ml.ML Thu May 14 15:09:48 2009 +0200
14.3 @@ -996,7 +996,7 @@
14.4 val (ml_code, target_names) = eval_code_of NONE thy naming program (consts' @ tycos');
14.5 val (consts'', tycos'') = chop (length consts') target_names;
14.6 val consts_map = map2 (fn const => fn NONE =>
14.7 - error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
14.8 + error ("Constant " ^ (quote o Code.string_of_const thy) const
14.9 ^ "\nhas a user-defined serialization")
14.10 | SOME const'' => (const, const'')) consts consts''
14.11 val tycos_map = map2 (fn tyco => fn NONE =>
14.12 @@ -1050,7 +1050,7 @@
14.13
14.14 fun ml_code_antiq raw_const {struct_name, background} =
14.15 let
14.16 - val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const;
14.17 + val const = Code.check_const (ProofContext.theory_of background) raw_const;
14.18 val is_first = is_first_occ background;
14.19 val background' = register_const const background;
14.20 in (print_code struct_name is_first (print_const const), background') end;
14.21 @@ -1059,7 +1059,7 @@
14.22 let
14.23 val thy = ProofContext.theory_of background;
14.24 val tyco = Sign.intern_type thy raw_tyco;
14.25 - val constrs = map (Code_Unit.check_const thy) raw_constrs;
14.26 + val constrs = map (Code.check_const thy) raw_constrs;
14.27 val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
14.28 val _ = if gen_eq_set (op =) (constrs, constrs') then ()
14.29 else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
15.1 --- a/src/Tools/code/code_preproc.ML Thu May 14 15:09:47 2009 +0200
15.2 +++ b/src/Tools/code/code_preproc.ML Thu May 14 15:09:48 2009 +0200
15.3 @@ -117,11 +117,11 @@
15.4 in
15.5 eqns
15.6 |> apply_functrans thy c functrans
15.7 - |> (map o apfst) (Code_Unit.rewrite_eqn pre)
15.8 + |> (map o apfst) (Code.rewrite_eqn pre)
15.9 |> (map o apfst) (AxClass.unoverload thy)
15.10 |> map (Code.assert_eqn thy)
15.11 - |> burrow_fst (Code_Unit.norm_args thy)
15.12 - |> burrow_fst (Code_Unit.norm_varnames thy)
15.13 + |> burrow_fst (Code.norm_args thy)
15.14 + |> burrow_fst (Code.norm_varnames thy)
15.15 end;
15.16
15.17 fun preprocess_conv thy ct =
15.18 @@ -186,7 +186,7 @@
15.19
15.20 fun pretty thy eqngr =
15.21 AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
15.22 - |> (map o apfst) (Code_Unit.string_of_const thy)
15.23 + |> (map o apfst) (Code.string_of_const thy)
15.24 |> sort (string_ord o pairself fst)
15.25 |> map (fn (s, thms) =>
15.26 (Pretty.block o Pretty.fbreaks) (
15.27 @@ -216,7 +216,7 @@
15.28 fun tyscm_rhss_of thy c eqns =
15.29 let
15.30 val tyscm = case eqns of [] => Code.default_typscheme thy c
15.31 - | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm;
15.32 + | ((thm, _) :: _) => Code.typscheme_eqn thy thm;
15.33 val rhss = consts_of thy eqns;
15.34 in (tyscm, rhss) end;
15.35
15.36 @@ -394,7 +394,7 @@
15.37 val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
15.38 Vartab.update ((v, 0), sort)) lhs;
15.39 val eqns = proto_eqns
15.40 - |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
15.41 + |> (map o apfst) (Code.inst_thm thy inst_tab);
15.42 val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
15.43 val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
15.44 in (map (pair c) rhss' @ rhss, eqngr') end;
16.1 --- a/src/Tools/code/code_target.ML Thu May 14 15:09:47 2009 +0200
16.2 +++ b/src/Tools/code/code_target.ML Thu May 14 15:09:48 2009 +0200
16.3 @@ -286,7 +286,7 @@
16.4 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
16.5 let
16.6 val c = prep_const thy raw_c;
16.7 - fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c
16.8 + fun check_args (syntax as (n, _)) = if n > Code.no_args thy c
16.9 then error ("Too many arguments in syntax for constant " ^ quote c)
16.10 else syntax;
16.11 in case raw_syn
16.12 @@ -319,8 +319,8 @@
16.13 | add (name, NONE) incls = Symtab.delete name incls;
16.14 in map_includes target (add args) thy end;
16.15
16.16 -val add_include = gen_add_include Code_Unit.check_const;
16.17 -val add_include_cmd = gen_add_include Code_Unit.read_const;
16.18 +val add_include = gen_add_include Code.check_const;
16.19 +val add_include_cmd = gen_add_include Code.read_const;
16.20
16.21 fun add_module_alias target (thyname, modlname) =
16.22 let
16.23 @@ -363,11 +363,11 @@
16.24 val allow_abort = gen_allow_abort (K I);
16.25 val add_reserved = add_reserved;
16.26
16.27 -val add_syntax_class_cmd = gen_add_syntax_class read_class Code_Unit.read_const;
16.28 +val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const;
16.29 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
16.30 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
16.31 -val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const;
16.32 -val allow_abort_cmd = gen_allow_abort Code_Unit.read_const;
16.33 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
16.34 +val allow_abort_cmd = gen_allow_abort Code.read_const;
16.35
16.36 fun the_literals thy =
16.37 let
16.38 @@ -387,15 +387,15 @@
16.39 local
16.40
16.41 fun labelled_name thy program name = case Graph.get_node program name
16.42 - of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c)
16.43 + of Code_Thingol.Fun (c, _) => quote (Code.string_of_const thy c)
16.44 | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
16.45 - | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c)
16.46 + | Code_Thingol.Datatypecons (c, _) => quote (Code.string_of_const thy c)
16.47 | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
16.48 | Code_Thingol.Classrel (sub, super) => let
16.49 val Code_Thingol.Class (sub, _) = Graph.get_node program sub
16.50 val Code_Thingol.Class (super, _) = Graph.get_node program super
16.51 in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
16.52 - | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c)
16.53 + | Code_Thingol.Classparam (c, _) => quote (Code.string_of_const thy c)
16.54 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let
16.55 val Code_Thingol.Class (class, _) = Graph.get_node program class
16.56 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
17.1 --- a/src/Tools/code/code_thingol.ML Thu May 14 15:09:47 2009 +0200
17.2 +++ b/src/Tools/code/code_thingol.ML Thu May 14 15:09:48 2009 +0200
17.3 @@ -498,7 +498,7 @@
17.4 let
17.5 val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
17.6 then raw_thms
17.7 - else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
17.8 + else (map o apfst) (Code.expand_eta thy 1) raw_thms;
17.9 in
17.10 fold_map (translate_tyvar_sort thy algbr funcgr) vs
17.11 ##>> translate_typ thy algbr funcgr ty
17.12 @@ -634,7 +634,7 @@
17.13 Term.strip_abs_eta 1 (the_single ts_clause)
17.14 in [(true, (Free v_ty, body))] end
17.15 else map (uncurry mk_clause)
17.16 - (AList.make (Code_Unit.no_args thy) case_pats ~~ ts_clause);
17.17 + (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
17.18 fun retermify ty (_, (IVar x, body)) =
17.19 (x, ty) `|-> body
17.20 | retermify _ (_, (pat, body)) =
17.21 @@ -812,7 +812,7 @@
17.22 fun read_const_expr "*" = ([], consts_of NONE)
17.23 | read_const_expr s = if String.isSuffix ".*" s
17.24 then ([], consts_of (SOME (unsuffix ".*" s)))
17.25 - else ([Code_Unit.read_const thy s], []);
17.26 + else ([Code.read_const thy s], []);
17.27 in pairself flat o split_list o map read_const_expr end;
17.28
17.29 fun code_depgr thy consts =
17.30 @@ -839,7 +839,7 @@
17.31 |> map (the o Symtab.lookup mapping)
17.32 |> distinct (op =);
17.33 val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
17.34 - fun namify consts = map (Code_Unit.string_of_const thy) consts
17.35 + fun namify consts = map (Code.string_of_const thy) consts
17.36 |> commas;
17.37 val prgr = map (fn (consts, constss) =>
17.38 { name = namify consts, ID = namify consts, dir = "", unfold = true,
18.1 --- a/src/Tools/nbe.ML Thu May 14 15:09:47 2009 +0200
18.2 +++ b/src/Tools/nbe.ML Thu May 14 15:09:48 2009 +0200
18.3 @@ -436,7 +436,7 @@
18.4 let
18.5 fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
18.6 | t => t);
18.7 - val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
18.8 + val resubst_triv_consts = subst_const (Code.resubst_alias thy);
18.9 val ty' = typ_of_itype program vs0 ty;
18.10 fun type_infer t =
18.11 singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
18.12 @@ -459,7 +459,7 @@
18.13 (* evaluation oracle *)
18.14
18.15 fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy))
18.16 - (Code_Unit.triv_classes thy);
18.17 + (Code.triv_classes thy);
18.18
18.19 fun mk_equals thy lhs raw_rhs =
18.20 let