--- a/NEWS Tue Jun 15 16:42:09 2010 +0200
+++ b/NEWS Thu Jun 17 10:02:29 2010 +0200
@@ -35,6 +35,12 @@
* List.thy: use various operations from the Haskell prelude when
generating Haskell code.
+* code_simp.ML: simplification with rules determined by
+code generator.
+
+* code generator: do not print function definitions for case
+combinators any longer.
+
New in Isabelle2009-2 (June 2010)
--- a/src/HOL/HOL.thy Tue Jun 15 16:42:09 2010 +0200
+++ b/src/HOL/HOL.thy Thu Jun 17 10:02:29 2010 +0200
@@ -1773,6 +1773,7 @@
setup {*
Code_Preproc.map_pre (K HOL_basic_ss)
#> Code_Preproc.map_post (K HOL_basic_ss)
+ #> Code_Simp.map_ss (K HOL_basic_ss)
*}
subsubsection {* Equality *}
--- a/src/HOL/IsaMakefile Tue Jun 15 16:42:09 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Jun 17 10:02:29 2010 +0200
@@ -112,6 +112,7 @@
$(SRC)/Tools/Code/code_preproc.ML \
$(SRC)/Tools/Code/code_printer.ML \
$(SRC)/Tools/Code/code_scala.ML \
+ $(SRC)/Tools/Code/code_simp.ML \
$(SRC)/Tools/Code/code_target.ML \
$(SRC)/Tools/Code/code_thingol.ML \
$(SRC)/Tools/Code_Generator.thy \
--- a/src/Pure/Isar/code.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Pure/Isar/code.ML Thu Jun 17 10:02:29 2010 +0200
@@ -72,6 +72,7 @@
val is_abstr: theory -> string -> bool
val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
val get_case_scheme: theory -> string -> (int * (int * string list)) option
+ val get_case_cong: theory -> string -> thm option
val undefineds: theory -> string list
val print_codesetup: theory -> unit
@@ -168,7 +169,7 @@
(*with explicit history*),
types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
(*with explicit history*),
- cases: (int * (int * string list)) Symtab.table * unit Symtab.table
+ cases: ((int * (int * string list)) * thm) Symtab.table * unit Symtab.table
};
fun make_spec (history_concluded, ((signatures, functions), (types, cases))) =
@@ -935,7 +936,8 @@
handle Bind => error "bad case certificate"
| TERM _ => error "bad case certificate";
-fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
+fun get_case_scheme thy = Option.map fst o Symtab.lookup ((fst o the_cases o the_exec) thy);
+fun get_case_cong thy = Option.map snd o Symtab.lookup ((fst o the_cases o the_exec) thy);
val undefineds = Symtab.keys o snd o the_cases o the_exec;
@@ -970,8 +972,8 @@
:: Pretty.str "of"
:: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
);
- fun pretty_case (const, (_, (_, []))) = Pretty.str (string_of_const thy const)
- | pretty_case (const, (_, (_, cos))) = (Pretty.block o Pretty.breaks) [
+ fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const)
+ | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
Pretty.str (string_of_const thy const), Pretty.str "with",
(Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
val functions = the_functions exec
@@ -1108,14 +1110,34 @@
(* cases *)
+fun case_cong thy case_const (num_args, (pos, constrs)) =
+ let
+ val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
+ val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
+ val (ws, vs) = chop pos zs;
+ val T = Logic.unvarifyT_global (const_typ thy case_const);
+ val Ts = (fst o strip_type) T;
+ val T_cong = nth Ts pos;
+ fun mk_prem z = Free (z, T_cong);
+ fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
+ val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
+ fun tac { prems, ... } = Simplifier.rewrite_goals_tac prems
+ THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
+ in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
+
fun add_case thm thy =
let
- val (c, (k, case_pats)) = case_cert thm;
+ val (case_const, (k, case_pats)) = case_cert thm;
val _ = case filter_out (is_constr thy) case_pats
of [] => ()
| cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
- val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
- in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
+ val entry = (1 + Int.max (1, length case_pats), (k, case_pats));
+ in
+ thy
+ |> Theory.checkpoint
+ |> `(fn thy => case_cong thy case_const entry)
+ |-> (fn cong => (map_exec_purge o map_cases o apfst) (Symtab.update (case_const, (entry, cong))))
+ end;
fun add_undefined c thy =
(map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
@@ -1138,7 +1160,7 @@
then insert (op =) c else I)
((the_functions o the_exec) thy) (old_proj :: old_constrs);
fun drop_outdated_cases cases = fold Symtab.delete_safe
- (Symtab.fold (fn (c, (_, (_, cos))) =>
+ (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
if exists (member (op =) old_constrs) cos
then insert (op =) c else I) cases []) cases;
in
--- a/src/Pure/simplifier.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Pure/simplifier.ML Thu Jun 17 10:02:29 2010 +0200
@@ -36,7 +36,7 @@
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
- val global_context: theory -> simpset -> simpset
+ val global_context: theory -> simpset -> simpset
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
val simproc_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
--- a/src/Tools/Code/code_eval.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Thu Jun 17 10:02:29 2010 +0200
@@ -55,7 +55,7 @@
val value_name = "Value.VALUE.value"
val program' = program
|> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
+ Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
|> fold (curry Graph.add_edge value_name) deps;
val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
(the_default target some_target) "" naming program' [value_name];
--- a/src/Tools/Code/code_haskell.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Jun 17 10:02:29 2010 +0200
@@ -115,7 +115,7 @@
end
| print_case tyvars some_thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
- fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
+ fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
@@ -275,7 +275,8 @@
val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
in (base', (nsp_fun, nsp_typ')) end;
val add_name = case stmt
- of Code_Thingol.Fun _ => add_fun false
+ of Code_Thingol.Fun (_, (_, SOME _)) => pair base
+ | Code_Thingol.Fun _ => add_fun false
| Code_Thingol.Datatype _ => add_typ
| Code_Thingol.Datatypecons _ => add_fun true
| Code_Thingol.Class _ => add_typ
@@ -283,7 +284,9 @@
| Code_Thingol.Classparam _ => add_fun false
| Code_Thingol.Classinst _ => pair base;
fun add_stmt' base' = case stmt
- of Code_Thingol.Datatypecons _ =>
+ of Code_Thingol.Fun (_, (_, SOME _)) =>
+ I
+ | Code_Thingol.Datatypecons _ =>
cons (name, (Long_Name.append module_name' base', NONE))
| Code_Thingol.Classrel _ => I
| Code_Thingol.Classparam _ =>
--- a/src/Tools/Code/code_ml.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jun 17 10:02:29 2010 +0200
@@ -758,7 +758,12 @@
val base' = if upper then first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
- fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
+ fun deps_of names =
+ []
+ |> fold (fold (insert (op =)) o Graph.imm_succs program) names
+ |> subtract (op =) names
+ |> filter_out (Code_Thingol.is_case o Graph.get_node program);
+ fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
let
val eqs = filter (snd o snd) raw_eqs;
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
@@ -845,10 +850,7 @@
fun add_stmts' stmts nsp_nodes =
let
val names as (name :: names') = map fst stmts;
- val deps =
- []
- |> fold (fold (insert (op =)) o Graph.imm_succs program) names
- |> subtract (op =) names;
+ val deps = deps_of names;
val (module_names, _) = (split_list o map dest_name) names;
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
@@ -882,9 +884,9 @@
|> apsnd (fold (fn name => fold (add_dep name) deps) names)
|> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
end;
- val (_, nodes) = empty_module
- |> fold add_stmts' (map (AList.make (Graph.get_node program))
- (rev (Graph.strong_conn program)));
+ val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program))
+ |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false);
+ val (_, nodes) = fold add_stmts' stmts empty_module;
fun deresolver prefix name =
let
val module_name = (fst o dest_name) name;
--- a/src/Tools/Code/code_preproc.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Thu Jun 17 10:02:29 2010 +0200
@@ -28,6 +28,7 @@
-> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
val eval: theory -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
+ val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
val setup: theory -> theory
end
@@ -457,6 +458,8 @@
fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
(K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
+fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
+
(** setup **)
--- a/src/Tools/Code/code_scala.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Jun 17 10:02:29 2010 +0200
@@ -129,7 +129,7 @@
(map2 (fn param => fn ty => print_typed tyvars
((str o lookup_var vars) param) ty)
params tys)) implicits) ty, str " ="]
- fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
+ fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
of [] =>
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
@@ -334,8 +334,9 @@
|> add_name
|-> (fn base' => rpair (add_stmt base' stmts))
end;
- val (_, sca_program) = fold prepare_stmt (AList.make (fn name => Graph.get_node program name)
- (Graph.strong_conn program |> flat)) (((reserved, reserved), reserved), []);
+ val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
+ |> filter_out (Code_Thingol.is_case o snd);
+ val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, (the_module_name, sca_program)) end;
@@ -351,8 +352,8 @@
module_name reserved raw_module_alias program;
val reserved = make_vars reserved;
fun args_num c = case Graph.get_node program c
- of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
- | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
+ of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
+ | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
| Code_Thingol.Datatypecons (_, tyco) =>
let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
in (length o the o AList.lookup (op =) constrs) c end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_simp.ML Thu Jun 17 10:02:29 2010 +0200
@@ -0,0 +1,83 @@
+(* Title: Tools/code/code_simp.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Connecting the simplifier and the code generator.
+*)
+
+signature CODE_SIMP =
+sig
+ val no_frees_conv: conv -> conv
+ val map_ss: (simpset -> simpset) -> theory -> theory
+ val current_conv: theory -> conv
+ val current_tac: theory -> int -> tactic
+ val make_conv: theory -> simpset option -> string list -> conv
+ val make_tac: theory -> simpset option -> string list -> int -> tactic
+ val setup: theory -> theory
+end;
+
+structure Code_Simp : CODE_SIMP =
+struct
+
+(* avoid free variables during conversion *)
+
+fun no_frees_conv conv ct =
+ let
+ val frees = Thm.add_cterm_frees ct [];
+ fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
+ |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
+ in
+ ct
+ |> fold_rev Thm.cabs frees
+ |> conv
+ |> fold apply_beta frees
+ end;
+
+
+(* dedicated simpset *)
+
+structure Simpset = Theory_Data (
+ type T = simpset;
+ val empty = empty_ss;
+ fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
+ val merge = merge_ss;
+);
+
+val map_ss = Simpset.map;
+
+
+(* build simpset and conversion from program *)
+
+fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
+ ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
+ | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
+ ss addsimps (map (fst o snd) classparam_insts)
+ | add_stmt _ ss = ss;
+
+val add_program = Graph.fold (add_stmt o fst o snd)
+
+fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
+ (add_program program (Simplifier.global_context thy
+ (the_default (Simpset.get thy) some_ss)));
+
+
+(* evaluation with current code context *)
+
+fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
+ (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
+
+fun current_tac thy = CONVERSION (current_conv thy);
+
+val setup = Method.setup (Binding.name "code_simp")
+ (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
+ "simplification with code equations"
+
+
+(* evaluation with freezed code context *)
+
+fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
+ ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
+
+fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts);
+
+end;
--- a/src/Tools/Code/code_thingol.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jun 17 10:02:29 2010 +0200
@@ -66,7 +66,7 @@
datatype stmt =
NoStmt
- | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
+ | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
| Datatype of string * ((vname * sort) list * (string * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -81,6 +81,7 @@
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
val is_cons: program -> string -> bool
+ val is_case: stmt -> bool
val contr_classparam_typs: program -> string -> itype option list
val labelled_name: theory -> program -> string -> string
val group_stmts: theory -> program
@@ -402,7 +403,7 @@
type typscheme = (vname * sort) list * itype;
datatype stmt =
NoStmt
- | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
+ | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
| Datatype of string * ((vname * sort) list * (string * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -416,7 +417,7 @@
type program = stmt Graph.T;
fun empty_funs program =
- Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c
+ Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
| _ => I) program [];
fun map_terms_bottom_up f (t as IConst _) = f t
@@ -430,8 +431,8 @@
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
fun map_terms_stmt f NoStmt = NoStmt
- | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst)
- (fn (ts, t) => (map f ts, f t)) eqs))
+ | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
+ (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
| map_terms_stmt f (stmt as Datatype _) = stmt
| map_terms_stmt f (stmt as Datatypecons _) = stmt
| map_terms_stmt f (stmt as Class _) = stmt
@@ -445,6 +446,9 @@
of Datatypecons _ => true
| _ => false;
+fun is_case (Fun (_, (_, SOME _))) = true
+ | is_case _ = false;
+
fun contr_classparam_typs program name = case Graph.get_node program name
of Classparam (_, class) => let
val Class (_, (_, (_, params))) = Graph.get_node program class;
@@ -473,6 +477,10 @@
val Datatype (tyco, _) = Graph.get_node program tyco
in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
+fun linear_stmts program =
+ rev (Graph.strong_conn program)
+ |> map (AList.make (Graph.get_node program));
+
fun group_stmts thy program =
let
fun is_fun (_, Fun _) = true | is_fun _ = false;
@@ -492,8 +500,7 @@
else error ("Illegal mutual dependencies: " ^
(commas o map (labelled_name thy program o fst)) stmts)
in
- rev (Graph.strong_conn program)
- |> map (AList.make (Graph.get_node program))
+ linear_stmts program
|> map group
end;
@@ -568,12 +575,12 @@
fun stmt_fun cert =
let
val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
+ val some_case_cong = Code.get_case_cong thy c;
in
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
##>> translate_typ thy algbr eqngr permissive ty
- ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns
- #>> map_filter I)
- #>> (fn info => Fun (c, info))
+ ##>> translate_eqns thy algbr eqngr permissive eqns
+ #>> (fn info => Fun (c, (info, some_case_cong)))
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => stmt_datatypecons tyco
@@ -667,9 +674,9 @@
fold_map (translate_term thy algbr eqngr permissive some_thm) args
##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
#>> rpair (some_thm, proper)
-and translate_equation thy algbr eqngr permissive eqn prgrm =
- prgrm |> translate_eqn thy algbr eqngr permissive eqn |>> SOME
- handle PERMISSIVE () => (NONE, prgrm)
+and translate_eqns thy algbr eqngr permissive eqns prgrm =
+ prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns
+ handle PERMISSIVE () => ([], prgrm)
and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
let
val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
@@ -847,10 +854,10 @@
##>> translate_typ thy algbr eqngr false ty
##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
#>> (fn ((vs, ty), t) => Fun
- (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
+ (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
fun term_value (dep, (naming, program1)) =
let
- val Fun (_, (vs_ty, [(([], t), _)])) =
+ val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
Graph.get_node program1 Term.dummy_patternN;
val deps = Graph.imm_succs program1 Term.dummy_patternN;
val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
--- a/src/Tools/Code_Generator.thy Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/Code_Generator.thy Thu Jun 17 10:02:29 2010 +0200
@@ -13,6 +13,7 @@
"~~/src/Tools/value.ML"
"~~/src/Tools/Code/code_preproc.ML"
"~~/src/Tools/Code/code_thingol.ML"
+ "~~/src/Tools/Code/code_simp.ML"
"~~/src/Tools/Code/code_printer.ML"
"~~/src/Tools/Code/code_target.ML"
"~~/src/Tools/Code/code_ml.ML"
@@ -24,6 +25,7 @@
setup {*
Code_Preproc.setup
+ #> Code_Simp.setup
#> Code_ML.setup
#> Code_Eval.setup
#> Code_Haskell.setup
--- a/src/Tools/nbe.ML Tue Jun 15 16:42:09 2010 +0200
+++ b/src/Tools/nbe.ML Thu Jun 17 10:02:29 2010 +0200
@@ -396,9 +396,9 @@
(* preparing function equations *)
-fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =
+fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
[]
- | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) =
+ | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
[(const, (vs, map fst eqns))]
| eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
[]
@@ -581,19 +581,6 @@
fun norm_oracle thy program vsp_ty_t deps ct =
raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
-fun no_frees_conv conv ct =
- let
- val frees = Thm.add_cterm_frees ct [];
- fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
- |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
- |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
- in
- ct
- |> fold_rev Thm.cabs frees
- |> conv
- |> fold apply_beta frees
- end;
-
fun no_frees_rew rew t =
let
val frees = map Free (Term.add_frees t []);
@@ -604,7 +591,7 @@
|> (fn t' => Term.betapplys (t', frees))
end;
-val norm_conv = no_frees_conv (fn ct =>
+val norm_conv = Code_Simp.no_frees_conv (fn ct =>
let
val thy = Thm.theory_of_cterm ct;
in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);