# HG changeset patch # User haftmann # Date 1158672125 -7200 # Node ID 65fe827aa595e9e155a1fefa8b6d684817861b6d # Parent 3950e65f48f89c9ccfff6d49c582077ced460891 code generation 2 adjustments diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Library/EfficientNat.thy Tue Sep 19 15:22:05 2006 +0200 @@ -126,8 +126,8 @@ unfolding nat_less_def by simp lemma [code func, code inline]: "(m <= n) = nat_less_equal m n" unfolding nat_less_equal_def by simp -lemma [code func, code inline]: "(m = n) = nat_eq m n" - unfolding nat_eq_def by simp +lemma [code func, code inline]: "OperationalEquality.eq m n = nat_eq m n" + unfolding nat_eq_def eq_def by simp lemma [code func]: "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))" unfolding nat_eq_def nat_minus_def int_aux_def by simp @@ -273,8 +273,8 @@ setup {* Codegen.add_preprocessor eqn_suc_preproc #> Codegen.add_preprocessor clause_suc_preproc - #> CodegenTheorems.add_preproc (lift_obj_eq eqn_suc_preproc) - #> CodegenTheorems.add_preproc (lift_obj_eq clause_suc_preproc) + #> CodegenData.add_preproc (lift_obj_eq eqn_suc_preproc) + #> CodegenData.add_preproc (lift_obj_eq clause_suc_preproc) *} (*>*) diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Library/ExecutableRat.thy --- a/src/HOL/Library/ExecutableRat.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Library/ExecutableRat.thy Tue Sep 19 15:22:05 2006 +0200 @@ -48,8 +48,8 @@ to_rat :: "erat \ rat" to_rat_def: "to_rat r = (case r of (Rat a p q) \ if a then Fract p q else Fract (uminus p) q)" - eq_rat :: "erat \ erat \ bool" - "eq_rat r s = (norm r = norm s)" + eq_erat :: "erat \ erat \ bool" + "eq_erat r s = (norm r = norm s)" defs (overloaded) zero_rat_def: "0 == Rat True 0 1" @@ -117,7 +117,7 @@ "op * :: erat \ erat \ erat" "inverse :: erat \ erat" "op <= :: erat \ erat \ bool" - eq_rat + eq_erat (SML) (Haskell) code_const Fract @@ -156,8 +156,12 @@ (SML "{*op <= :: erat \ erat \ bool*}") (Haskell "{*op <= :: erat \ erat \ bool*}") -code_const "op = :: rat \ rat \ bool" - (SML "{*eq_rat*}") - (Haskell "{*eq_rat*}") +instance rat :: eq .. + +code_const "OperationalEquality.eq :: rat \ rat \ bool" + (SML "{*eq_erat*}") + (Haskell "{*eq_erat*}") + +code_gen (SML -) end diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Library/ExecutableSet.thy --- a/src/HOL/Library/ExecutableSet.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Library/ExecutableSet.thy Tue Sep 19 15:22:05 2006 +0200 @@ -9,14 +9,21 @@ imports Main begin -section {* Definitional rewrites *} +section {* Definitional equality rewrites *} + +instance set :: (eq) eq .. lemma [code target: Set]: "(A = B) = (A \ B \ B \ A)" by blast +lemma [code func]: + "OperationalEquality.eq A B = (A \ B \ B \ A)" + unfolding eq_def by blast + declare bex_triv_one_point1 [symmetric, standard, code] + section {* HOL definitions *} subsection {* Basic definitions *} @@ -24,9 +31,9 @@ definition flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" "flip f a b = f b a" - member :: "'a list \ 'a \ bool" + member :: "'a list \ 'a\eq \ bool" "member xs x = (x \ set xs)" - insertl :: "'a \ 'a list \ 'a list" + insertl :: "'a\eq\ 'a list \ 'a list" "insertl x xs = (if member xs x then xs else x#xs)" lemma @@ -44,6 +51,7 @@ declare drop_first.simps [code target: List] declare remove1.simps [code del] +ML {* reset CodegenData.strict_functyp *} lemma [code target: List]: "remove1 x xs = (if member xs x then drop_first (\y. y = x) xs else xs)" proof (cases "member xs x") @@ -53,6 +61,7 @@ have "remove1 x xs = drop_first (\y. y = x) xs" by (induct xs) simp_all with True show ?thesis by simp qed +ML {* set CodegenData.strict_functyp *} lemma member_nil [simp]: "member [] = (\x. False)" @@ -84,8 +93,7 @@ subsection {* Derived definitions *} - -function unionl :: "'a list \ 'a list \ 'a list" +function unionl :: "'a\eq list \ 'a list \ 'a list" where "unionl [] ys = ys" | "unionl xs ys = foldr insertl xs ys" @@ -94,7 +102,7 @@ lemmas unionl_def = unionl.simps(2) declare unionl.simps[code] -function intersect :: "'a list \ 'a list \ 'a list" +function intersect :: "'a\eq list \ 'a list \ 'a list" where "intersect [] ys = []" | "intersect xs [] = []" @@ -104,7 +112,7 @@ lemmas intersect_def = intersect.simps(3) declare intersect.simps[code] -function subtract :: "'a list \ 'a list \ 'a list" +function subtract :: "'a\eq list \ 'a list \ 'a list" where "subtract [] ys = ys" | "subtract xs [] = []" @@ -114,7 +122,7 @@ lemmas subtract_def = subtract.simps(3) declare subtract.simps[code] -function map_distinct :: "('a \ 'b) \ 'a list \ 'b list" +function map_distinct :: "('a \ 'b\eq) \ 'a list \ 'b list" where "map_distinct f [] = []" | "map_distinct f xs = foldr (insertl o f) xs []" @@ -123,7 +131,7 @@ lemmas map_distinct_def = map_distinct.simps(2) declare map_distinct.simps[code] -function unions :: "'a list list \ 'a list" +function unions :: "'a\eq list list \ 'a list" where "unions [] = []" "unions xs = foldr unionl xs []" @@ -132,14 +140,14 @@ lemmas unions_def = unions.simps(2) declare unions.simps[code] -consts intersects :: "'a list list \ 'a list" +consts intersects :: "'a\eq list list \ 'a list" primrec "intersects (x#xs) = foldr intersect xs x" definition - map_union :: "'a list \ ('a \ 'b list) \ 'b list" + map_union :: "'a list \ ('a \ 'b\eq list) \ 'b list" "map_union xs f = unions (map f xs)" - map_inter :: "'a list \ ('a \ 'b list) \ 'b list" + map_inter :: "'a list \ ('a \ 'b\eq list) \ 'b list" "map_inter xs f = intersects (map f xs)" @@ -266,11 +274,6 @@ "ExecutableSet.insertl" "List.insertl" "ExecutableSet.drop_first" "List.drop_first" -code_gen - insertl unionl intersect flip subtract map_distinct - unions intersects map_union map_inter Blall Blex - (SML) (Haskell) - code_const "{}" (SML target_atom "[]") (Haskell target_atom "[]") @@ -319,4 +322,6 @@ (SML "{*Blex*}") (Haskell "{*Blex*}") +code_gen (SML -) (SML _) + end diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 19 15:22:05 2006 +0200 @@ -8,9 +8,11 @@ signature DATATYPE_CODEGEN = sig val get_eq: theory -> string -> thm list - val get_datatype_spec_thms: theory -> string - -> (((string * sort) list * (string * typ list) list) * tactic) option - val datatype_tac: theory -> string -> tactic + val get_eq_datatype: theory -> string -> thm list + val get_eq_typecopy: theory -> string -> thm list + val get_cert: theory -> bool * string -> thm list + val get_cert_datatype: theory -> string -> thm list + val get_cert_typecopy: theory -> string -> thm list val dest_case_expr: theory -> term -> ((string * typ) list * ((term * typ) * (term * term) list)) option val add_datatype_case_const: string -> theory -> theory @@ -18,6 +20,8 @@ type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list -> theory -> theory + val codetype_hook: hook + val eq_hook: hook val codetypes_dependency: theory -> (string * bool) list list val add_codetypes_hook_bootstrap: hook -> theory -> theory val the_codetypes_mut_specs: theory -> (string * bool) list @@ -26,9 +30,10 @@ -> (string * (((string * sort list) * sort) * term list)) list option val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort -> (theory -> ((string * sort list) * sort) list -> (string * term list) list - -> ((bstring * attribute list) * term) list) -> theory -> theory + -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory val setup: theory -> theory + val setup2: theory -> theory end; structure DatatypeCodegen : DATATYPE_CODEGEN = @@ -370,26 +375,20 @@ in map mk_dist (sym_product cos) end; local - val not_sym = thm "HOL.not_sym"; + val bool_eq_implies = thm "iffD1"; + val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric; + val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric; val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI]; -in fun get_eq thy dtco = + val not_eq_quodlibet = thm "not_eq_quodlibet"; +in fun get_cert_datatype thy dtco = let val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco; - fun mk_triv_inject co = - let - val ct' = Thm.cterm_of thy - (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs))) - val cty' = Thm.ctyp_of_term ct'; - val refl = Thm.prop_of HOL.refl; - val SOME (ct, cty) = fold_aterms (fn Var (v, ty) => - (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I) - refl NONE; - in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end; - val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs - val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco; + val inject = (#inject o DatatypePackage.the_datatype thy) dtco + |> map (fn thm => bool_eq_implies OF [thm] ) + |> map (Tactic.rewrite_rule [rew_eq, rew_conj]); val ctxt = Context.init_proof thy; val simpset = Simplifier.context ctxt - (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]); + (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]); val cos = map (fn (co, tys) => (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs; val tac = ALLGOALS (simp_tac simpset) @@ -397,30 +396,19 @@ val distinct = mk_distinct cos |> map (fn t => Goal.prove_global thy [] [] t (K tac)) - |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms) - in inject1 @ inject2 @ distinct end; + |> map (fn thm => not_eq_quodlibet OF [thm]) + in inject @ distinct end +and get_cert_typecopy thy dtco = + let + val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco; + val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]); + in + [thm] + end; end (*local*); -fun datatype_tac thy dtco = - let - val ctxt = Context.init_proof thy; - val inject = (#inject o DatatypePackage.the_datatype thy) dtco; - val simpset = Simplifier.context ctxt - (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]); - in - (TRY o ALLGOALS o match_tac) [HOL.eq_reflection] - THEN ( - (ALLGOALS o match_tac) (eqTrueI :: inject) - ORELSE (ALLGOALS o simp_tac) simpset - ) - THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm] - end; - -fun get_datatype_spec_thms thy dtco = - case DatatypePackage.get_datatype_spec thy dtco - of SOME vs_cos => - SOME (vs_cos, datatype_tac thy dtco) - | NONE => NONE; +fun get_cert thy (true, dtco) = get_cert_datatype thy dtco + | get_cert thy (false, dtco) = get_cert_typecopy thy dtco; fun add_datatype_case_const dtco thy = let @@ -433,7 +421,7 @@ let val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco in - fold CodegenTheorems.add_fun case_rewrites thy + fold_rev CodegenData.add_func case_rewrites thy end; @@ -536,7 +524,7 @@ ) else NONE end; -fun prove_codetypes_arities tac tycos sort f thy = +fun prove_codetypes_arities tac tycos sort f after_qed thy = case get_codetypes_arities thy tycos sort of NONE => thy | SOME insts => let @@ -548,20 +536,128 @@ then NONE else SOME (arity, (tyco, cs)))) insts; in thy - |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac - arities ("", []) (f thy arities css) + |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac + arities ("", []) (f thy arities css) #> after_qed) end; +local + val class_eq = "OperationalEquality.eq"; +in fun add_eq_instance specs = + prove_codetypes_arities + (K (ClassPackage.intro_classes_tac [])) + (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) + [class_eq] ((K o K o K) []) +end; (*local*) + +local + val not_sym = thm "HOL.not_sym"; + val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI]; +in fun get_eq_datatype thy dtco = + let + val _ = writeln "01"; + val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco; + val _ = writeln "02"; + fun mk_triv_inject co = + let + val ct' = Thm.cterm_of (Context.check_thy thy) + (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs))) + val cty' = Thm.ctyp_of_term ct'; + val refl = Thm.prop_of HOL.refl; + val SOME (ct, cty) = fold_aterms (fn Var (v, ty) => + (K o SOME) (Thm.cterm_of (Context.check_thy thy) (Var (v, Thm.typ_of cty')), Thm.ctyp_of (Context.check_thy thy) ty) | _ => I) + refl NONE; + in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end; + val _ = writeln "03"; + val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs + val _ = writeln "04"; + val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco; + val _ = writeln "05"; + val ctxt = Context.init_proof (Context.check_thy thy); + val _ = writeln "06"; + val simpset = Simplifier.context ctxt + (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]); + val _ = writeln "07"; + val cos = map (fn (co, tys) => + (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs; + val tac = ALLGOALS (simp_tac simpset) + THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]); + val _ = writeln "08"; + val distinct = + mk_distinct cos + |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac)) + |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms) + val _ = writeln "09"; + in inject1 @ inject2 @ distinct end; + +fun get_eq_typecopy thy tyco = + case TypecopyPackage.get_typecopy_info thy tyco + of SOME { inject, ... } => [inject] + | NONE => []; + +local + val lift_not_thm = thm "HOL.Eq_FalseI"; + val lift_thm = thm "HOL.eq_reflection"; + val eq_def_sym = thm "eq_def" |> Thm.symmetric; + fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco + of SOME _ => get_eq_datatype (Context.check_thy thy) tyco + | NONE => case TypecopyPackage.get_typecopy_info thy tyco + of SOME _ => get_eq_typecopy thy tyco + | NONE => []; +in + fun get_eq thy tyco = + get_eq_thms (Context.check_thy thy) tyco + |> tap (fn _ => writeln "10") + |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy)) + |> tap (fn _ => writeln "11") + |> constrain_op_eq (Context.check_thy thy) + |> tap (fn _ => writeln "12") + |> map (Tactic.rewrite_rule [eq_def_sym]) + |> tap (fn _ => writeln "13") +end; + +end; + +fun add_eq_thms (dtco, (_, (vs, cs))) thy = + let + val thy_ref = Theory.self_ref thy; + val ty = Type (dtco, map TFree vs) |> Logic.varifyT; + val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]); + val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> tap (fn _ => writeln "14x") |> rev |> tap (fn _ => writeln "15x")); + in + CodegenData.add_funcl + (c, CodegenData.lazy get_thms) thy + end; + +fun codetype_hook dtcos theory = + let + fun add (dtco, (flag, spec)) thy = + let + fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco)); + in + CodegenData.add_datatype + (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy + end; + in + theory + |> fold add dtcos + end; + +fun eq_hook dtcos = + add_eq_instance dtcos (fold add_eq_thms dtcos); + (** theory setup **) val setup = - add_codegen "datatype" datatype_codegen #> - add_tycodegen "datatype" datatype_tycodegen #> - CodegenTheorems.add_datatype_extr - get_datatype_spec_thms #> - DatatypeHooks.add (fold add_datatype_case_const) #> - DatatypeHooks.add (fold add_datatype_case_defs) + add_codegen "datatype" datatype_codegen + #> add_tycodegen "datatype" datatype_tycodegen + #> DatatypeHooks.add (fold add_datatype_case_const) + #> DatatypeHooks.add (fold add_datatype_case_defs) + +val setup2 = + add_codetypes_hook_bootstrap codetype_hook + #> add_codetypes_hook_bootstrap eq_hook + end; diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue Sep 19 15:22:05 2006 +0200 @@ -308,7 +308,7 @@ (snd o PureThy.add_thmss [(("simps", simps), []), (("", List.concat case_thms @ size_thms @ List.concat distinct @ rec_thms), [Simplifier.simp_add]), - (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]), + (("", size_thms @ rec_thms), [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]), (("", List.concat inject), [iff_add]), (("", map name_notE (List.concat distinct)), [Classical.safe_elim NONE]), (("", weak_case_congs), [cong_att])]); @@ -479,9 +479,10 @@ strip_abs (length dts) t, is_dependent (length dts) t)) (constrs ~~ fs); fun count_cases (cs, (_, _, true)) = cs - | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of - NONE => (body, [cname]) :: cs - | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs); + | count_cases (cs, (cname, (_, body), false)) = + case AList.lookup (op = : term * term -> bool) cs body + of NONE => (body, [cname]) :: cs + | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs; val cases' = sort (int_ord o Library.swap o pairself (length o snd)) (Library.foldl count_cases ([], cases)); fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $ @@ -558,33 +559,42 @@ (********************* axiomatic introduction of datatypes ********************) -fun add_and_get_axioms_atts label tnames attss ts thy = - foldr (fn (((tname, atts), t), (thy', axs)) => - let - val ([ax], thy'') = - thy' - |> Theory.add_path tname - |> PureThy.add_axioms_i [((label, t), atts)]; - in (Theory.parent_path thy'', ax::axs) - end) (thy, []) (tnames ~~ attss ~~ ts) |> swap; +fun add_axiom label t atts thy = + thy + |> PureThy.add_axioms_i [((label, t), atts)]; + +fun add_axioms label ts atts thy = + thy + |> PureThy.add_axiomss_i [((label, ts), atts)]; -fun add_and_get_axioms label tnames = - add_and_get_axioms_atts label tnames (replicate (length tnames) []); +fun add_and_get_axioms_atts label tnames ts attss = + fold_map (fn (tname, (atts, t)) => fn thy => + thy + |> Theory.add_path tname + |> add_axiom label t atts + ||> Theory.parent_path + |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts)); -fun add_and_get_axiomss label tnames tss thy = - foldr (fn ((tname, ts), (thy', axss)) => - let - val ([axs], thy'') = - thy' - |> Theory.add_path tname - |> PureThy.add_axiomss_i [((label, ts), [])]; - in (Theory.parent_path thy'', axs::axss) - end) (thy, []) (tnames ~~ tss) |> swap; +fun add_and_get_axioms label tnames ts = + add_and_get_axioms_atts label tnames ts (replicate (length tnames) []); + +fun add_and_get_axiomss label tnames tss = + fold_map (fn (tname, ts) => fn thy => + thy + |> Theory.add_path tname + |> add_axioms label ts [] + ||> Theory.parent_path + |-> (fn [ax] => pair ax)) (tnames ~~ tss); fun specify_consts args thy = - let val specs = - args |> map (fn (c, T, mx) => Const (Sign.full_name thy (Syntax.const_name c mx), T)); - in thy |> Theory.add_consts_i args |> Theory.add_finals_i false specs end; + let + val specs = map (fn (c, T, mx) => + Const (Sign.full_name thy (Syntax.const_name c mx), T)) args; + in + thy + |> Sign.add_consts_i args + |> Theory.add_finals_i false specs + end; fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy = @@ -675,10 +685,9 @@ val ((([induct], [rec_thms]), inject), thy3) = thy2 |> Theory.add_path (space_implode "_" new_type_names) - |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), - [case_names_induct])] - ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])] - ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])]) + |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct] + ||>> add_axioms "recs" rec_axs [] + ||> (if no_size then I else add_axioms "size" size_axs [] #> snd) ||> Theory.parent_path ||>> add_and_get_axiomss "inject" new_type_names (DatatypeProp.make_injs descr sorts); @@ -688,7 +697,7 @@ val exhaust_ts = DatatypeProp.make_casedists descr sorts; val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names - (map Library.single case_names_exhausts) exhaust_ts thy4; + exhaust_ts (map single case_names_exhausts) thy4; val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5; val (split_ts, split_asm_ts) = ListPair.unzip @@ -924,11 +933,9 @@ Theory.add_types (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts); - val sign = Theory.sign_of tmp_thy; - val (tyvars, _, _, _)::_ = dts; val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => - let val full_tname = Sign.full_name sign (Syntax.type_name tname mx) + let val full_tname = Sign.full_name tmp_thy (Syntax.type_name tname mx) in (case duplicates (op =) tvs of [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx)) else error ("Mutually recursive datatypes must have same type parameters") @@ -943,12 +950,12 @@ let fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) = let - val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs); + val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs); val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of [] => () | vs => error ("Extra type variables on rhs: " ^ commas vs)) - in (constrs @ [((if flat_names then Sign.full_name sign else - Sign.full_name_path sign tname) (Syntax.const_name cname mx'), + in (constrs @ [((if flat_names then Sign.full_name tmp_thy else + Sign.full_name_path tmp_thy tname) (Syntax.const_name cname mx'), map (dtyp_of_typ new_dts) cargs')], constr_syntax' @ [(cname, mx')], sorts'') end handle ERROR msg => @@ -961,7 +968,7 @@ in case duplicates (op =) (map fst constrs') of [] => - (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx), + (dts' @ [(i, (Sign.full_name tmp_thy (Syntax.type_name tname mx), map DtTFree tvs, constrs'))], constr_syntax @ [constr_syntax'], sorts', i + 1) | dups => error ("Duplicate constructors " ^ commas dups ^ @@ -969,9 +976,9 @@ end; val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts); - val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts')); + val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts')); val dt_info = get_datatypes thy; - val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i; + val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i; val _ = check_nonempty descr handle (exn as Datatype_Empty s) => if err then error ("Nonemptiness check failed for datatype " ^ s) else raise exn; diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Sep 19 15:22:05 2006 +0200 @@ -17,7 +17,7 @@ open Codegen; -structure CodegenData = TheoryDataFun +structure RecCodegenData = TheoryDataFun (struct val name = "HOL/recfun_codegen"; type T = (thm * string option) list Symtab.table; @@ -40,27 +40,27 @@ let fun add thm = if Pattern.pattern (lhs_of thm) then - CodegenData.map + RecCodegenData.map (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, optmod))) else tap (fn _ => warn thm) handle TERM _ => tap (fn _ => warn thm); in add thm - #> CodegenTheorems.add_fun thm + #> CodegenData.add_func thm end); fun del_thm thm thy = let - val tab = CodegenData.get thy; + val tab = RecCodegenData.get thy; val (s, _) = const_of (prop_of thm); in case Symtab.lookup tab s of NONE => thy | SOME thms => - CodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy + RecCodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy end handle TERM _ => (warn thm; thy); val del = Thm.declaration_attribute - (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_fun thm)) + (fn thm => Context.map_theory (del_thm thm #> CodegenData.del_func thm)) fun del_redundant thy eqs [] = eqs | del_redundant thy eqs (eq :: eqs') = @@ -70,7 +70,7 @@ in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end; fun get_equations thy defs (s, T) = - (case Symtab.lookup (CodegenData.get thy) s of + (case Symtab.lookup (RecCodegenData.get thy) s of NONE => ([], "") | SOME thms => let val thms' = del_redundant thy [] @@ -172,10 +172,10 @@ val setup = - CodegenData.init #> + RecCodegenData.init #> add_codegen "recfun" recfun_codegen #> add_attribute "" (Args.del |-- Scan.succeed del - || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add); + || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> (fn name => setmp CodegenData.strict_functyp false (add name))); end; diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 19 15:22:05 2006 +0200 @@ -21,9 +21,6 @@ val get_typecopy_info: theory -> string -> info option type hook = string * info -> theory -> theory; val add_hook: hook -> theory -> theory; - val typecopy_fun_extr: theory -> string * typ -> thm list option - val typecopy_type_extr: theory -> string - -> (((string * sort) list * (string * typ list) list) * tactic) option val print: theory -> unit val setup: theory -> theory end; @@ -137,27 +134,13 @@ end; (*local*) -(* theory setup *) - -fun typecopy_type_extr thy tyco = - case get_typecopy_info thy tyco - of SOME { vs, constr, typ, inject, ... } => SOME ((vs, [(constr, [typ])]), - (ALLGOALS o match_tac) [eq_reflection] - THEN (ALLGOALS o match_tac) [inject]) - | NONE => NONE; +(* hooks for projection function code *) -fun typecopy_fun_extr thy (c, ty) = - case (fst o strip_type) ty - of Type (tyco, _) :: _ => - (case get_typecopy_info thy tyco - of SOME { proj_def, proj as (c', _), ... } => - if c = c' then SOME [proj_def] else NONE - | NONE => NONE) - | _ => NONE; +fun add_project (_ , { proj_def, ...} : info) = + CodegenData.add_func proj_def; val setup = TypecopyData.init - #> CodegenTheorems.add_fun_extr (these oo typecopy_fun_extr) - #> CodegenTheorems.add_datatype_extr typecopy_type_extr; + #> add_hook add_project; end; (*struct*) diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Tue Sep 19 15:22:05 2006 +0200 @@ -7,12 +7,6 @@ signature TYPEDEF_CODEGEN = sig - val get_triv_typedef: theory -> string - -> ((((string * sort) list * (string * typ list) list) * thm) * - ((string * typ) * thm)) option - val typedef_fun_extr: theory -> string * typ -> thm list option - val typedef_type_extr: theory -> string - -> (((string * sort) list * (string * typ list) list) * tactic) option val setup: theory -> theory end; @@ -106,42 +100,8 @@ end) | typedef_tycodegen thy defs gr dep module brack _ = NONE; -fun get_triv_typedef thy tyco = - case TypedefPackage.get_info thy tyco - of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, - set_def = SOME def, Abs_inject = inject, Abs_inverse = inverse, ... } => - let - val exists_thm = - UNIV_I - |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [] - |> rewrite_rule [symmetric def]; - in case try (op OF) (inject, [exists_thm, exists_thm]) - of SOME eq_thm => - SOME (((Term.add_tfreesT (Type.no_tvars ty_abs) [], [(c_abs, [ty_rep])]), eq_thm), - ((c_rep, ty_abs --> ty_rep), inverse OF [exists_thm])) - | NONE => NONE - end - | _ => NONE; - -fun typedef_type_extr thy tyco = - case get_triv_typedef thy tyco - of SOME ((vs_cs, thm), _) => SOME (vs_cs, - (ALLGOALS o match_tac) [eq_reflection] - THEN (ALLGOALS o match_tac) [thm]) - | NONE => NONE; - -fun typedef_fun_extr thy (c, ty) = - case (fst o strip_type) ty - of Type (tyco, _) :: _ => - (case get_triv_typedef thy tyco - of SOME (_, ((c', _), thm)) => if c = c' then SOME [thm] else NONE - | NONE => NONE) - | _ => NONE; - val setup = Codegen.add_codegen "typedef" typedef_codegen #> Codegen.add_tycodegen "typedef" typedef_tycodegen - #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr) - #> CodegenTheorems.add_datatype_extr typedef_type_extr end; diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/ex/Classpackage.thy Tue Sep 19 15:22:05 2006 +0200 @@ -26,7 +26,7 @@ from semigroup_int_def show "k \ l \ j = k \ (l \ j)" by simp qed -instance (type) list :: semigroup +instance list :: (type) semigroup "xs \ ys \ xs @ ys" proof fix xs ys zs :: "'a list" @@ -52,7 +52,7 @@ from monoidl_num_def show "\ \ k = k" by simp qed -instance (type) list :: monoidl +instance list :: (type) monoidl "\ \ []" proof fix xs :: "'a list" @@ -67,7 +67,7 @@ class monoid = monoidl + assumes neutr: "x \<^loc>\ \<^loc>\ = x" -instance monoid_list_def: (type) list :: monoid +instance monoid_list_def: list :: (type) monoid proof fix xs :: "'a list" show "xs \ \ = xs" @@ -288,26 +288,26 @@ "\<^loc>\ \<^loc>\ (k\int) = \<^loc>\" using pow_def nat_pow_one inv_one by simp -instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup +instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup mult_prod_def: "x \ y \ let (x1, x2) = x; (y1, y2) = y in (x1 \ y1, x2 \ y2)" by default (simp_all add: split_paired_all semigroup_prod_def assoc) -instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl +instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl one_prod_def: "\ \ (\, \)" by default (simp_all add: split_paired_all monoidl_prod_def neutl) -instance monoid_prod_def: (monoid, monoid) * :: monoid +instance monoid_prod_def: * :: (monoid, monoid) monoid by default (simp_all add: split_paired_all monoid_prod_def neutr) -instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm +instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm by default (simp_all add: split_paired_all monoidl_prod_def comm) -instance group_prod_def: (group, group) * :: group +instance group_prod_def: * :: (group, group) group inv_prod_def: "\
x \ let (x1, x2) = x in (\
x1, \
x2)" by default (simp_all add: split_paired_all group_prod_def invl) -instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm +instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm by default (simp_all add: split_paired_all group_prod_def comm) definition diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/ex/CodeCollections.thy --- a/src/HOL/ex/CodeCollections.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/ex/CodeCollections.thy Tue Sep 19 15:22:05 2006 +0200 @@ -5,7 +5,7 @@ header {* Collection classes as examples for code generation *} theory CodeCollections -imports CodeOperationalEquality +imports Main begin section {* Collection classes as examples for code generation *} @@ -119,7 +119,7 @@ termination by (auto_term "{}") -instance (ordered) option :: ordered +instance option :: (ordered) ordered "x <<= y == le_option' x y" proof (default, unfold ordered_option_def) fix x @@ -149,7 +149,7 @@ "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \ x1 = x2 \ y1 <<= y2)" termination by (auto_term "{}") -instance (ordered, ordered) * :: ordered +instance * :: (ordered, ordered) ordered "x <<= y == le_pair' x y" apply (default, unfold "ordered_*_def", unfold split_paired_all) apply simp_all @@ -238,11 +238,11 @@ "inf == ()" by default (simp add: infimum_unit_def) -instance (ordered) option :: infimum +instance option :: (ordered) infimum "inf == None" by default (simp add: infimum_option_def) -instance (infimum, infimum) * :: infimum +instance * :: (infimum, infimum) infimum "inf == (inf, inf)" by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf) @@ -333,7 +333,7 @@ apply (rule member_enum)+ sorry*) -instance (enum) option :: enum +instance option :: (enum) enum "_4": "enum == None # map Some enum" proof (default, unfold enum_option_def) fix x :: "'a::enum option" @@ -398,13 +398,11 @@ "test1 = sum [None, Some True, None, Some False]" "test2 = (inf :: nat \ unit)" -code_gen eq code_gen "op <<=" code_gen "op <<" code_gen inf code_gen between code_gen index -code_gen sum code_gen test1 code_gen test2 diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/ex/CodeEval.thy --- a/src/HOL/ex/CodeEval.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/ex/CodeEval.thy Tue Sep 19 15:22:05 2006 +0200 @@ -13,7 +13,7 @@ subsection {* The typ_of class *} class typ_of = - fixes typ_of :: "'a option \ typ" + fixes typ_of :: "'a itself \ typ" ML {* structure TypOf = @@ -22,17 +22,15 @@ local val thy = the_context (); val const_typ_of = Sign.intern_const thy "typ_of"; - val const_None = Sign.intern_const thy "None"; - fun typ_option ty = Type (Sign.intern_type (the_context ()) "option", [ty]); - fun term_typ_of ty = Const (const_typ_of, typ_option ty --> Embed.typ_typ); + fun term_typ_of ty = Const (const_typ_of, Term.itselfT ty --> Embed.typ_typ); in val class_typ_of = Sign.intern_class thy "typ_of"; - fun term_typ_of_None ty = - term_typ_of ty $ Const (const_None, typ_option ty); + fun term_typ_of_type ty = + term_typ_of ty $ Logic.mk_type ty; fun mk_typ_of_def ty = let - val lhs = term_typ_of ty $ Free ("x", typ_option ty) - val rhs = Embed.term_typ (fn v => term_typ_of_None (TFree v)) ty + val lhs = term_typ_of ty $ Free ("x", Term.itselfT ty) + val rhs = Embed.term_typ (fn v => term_typ_of_type (TFree v)) ty in Logic.mk_equals (lhs, rhs) end; end; @@ -41,14 +39,15 @@ setup {* let - fun mk _ arities _ = + fun mk thy arities _ = maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def - (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities; + (Type (tyco, map TFree (Name.names Name.context "'a" asorts))) + |> tap (writeln o Sign.string_of_term thy))]) arities; fun tac _ = ClassPackage.intro_classes_tac []; fun hook specs = DatatypeCodegen.prove_codetypes_arities tac (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) - [TypOf.class_typ_of] mk + [TypOf.class_typ_of] mk I in DatatypeCodegen.add_codetypes_hook_bootstrap hook end *} @@ -56,7 +55,7 @@ subsection {* term_of class *} class term_of = typ_of + - constrains typ_of :: "'a option \ typ" + constrains typ_of :: "'a itself \ typ" fixes term_of :: "'a \ term" ML {* @@ -77,7 +76,7 @@ val lhs : term = term_term_of dty $ c; val rhs : term = Embed.term_term (fn (v, ty) => term_term_of ty $ Free (v, ty)) - (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_None (TFree (v, sort)))) c + (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c in HOLogic.mk_eq (lhs, rhs) end; @@ -103,7 +102,7 @@ else DatatypeCodegen.prove_codetypes_arities tac (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) - [TermOf.class_term_of] mk + [TermOf.class_term_of] mk I in DatatypeCodegen.add_codetypes_hook_bootstrap hook end *} @@ -116,10 +115,9 @@ ML {* signature EVAL = sig - val eval_term: term -> theory -> term * theory - val eval_term' : theory -> term -> term + val eval_term: theory -> term -> term val term: string -> unit - val eval_ref: term ref + val eval_ref: term option ref val oracle: string * (theory * exn -> term) val method: Method.src -> Proof.context -> Method.method end; @@ -127,30 +125,24 @@ structure Eval : EVAL = struct -val eval_ref = ref Logic.protectC; - -fun eval_term t = - CodegenPackage.eval_term - (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t); +val eval_ref = ref NONE; -fun eval_term' thy t = - let - val thy' = Theory.copy thy; - val (t', _) = eval_term t thy'; - in t' end; +fun eval_term thy t = + CodegenPackage.eval_term + thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t); fun term t = let val thy = the_context (); - val t' = eval_term' thy (Sign.read_term thy t); - in () end; + val t = eval_term thy (Sign.read_term thy t); + in (writeln o Sign.string_of_term thy) t end; val lift_eq_Trueprop = thm "lift_eq_Trueprop"; exception Eval of term; val oracle = ("Eval", fn (thy, Eval t) => - Logic.mk_equals (t, eval_term' thy t)); + Logic.mk_equals (t, eval_term thy t)); val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle]; @@ -194,8 +186,6 @@ and ('a, 'b) cair = Cair 'a 'b -code_gen term_of - ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *} lemma @@ -207,4 +197,4 @@ lemma "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval -end +end \ No newline at end of file diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/ex/Codegenerator.thy Tue Sep 19 15:22:05 2006 +0200 @@ -27,8 +27,6 @@ definition swap :: "'a * 'b \ 'b * 'a" "swap p = (let (x, y) = p in (y, x))" - swapp :: "'a * 'b \ 'c * 'd \ ('a * 'c) * ('b * 'd)" - "swapp = (\(x, y) (z, w). ((x, z), (y, w)))" appl :: "('a \ 'b) * 'a \ 'b" "appl p = (let (f, x) = p in f x)" @@ -91,8 +89,14 @@ h "Mymod.A.B.f" code_gen xor -code_gen one "0::nat" "1::nat" -code_gen "0::int" "1::int" n fac +code_gen one +code_gen "0::int" "1::int" + (SML) (Haskell) +code_gen n + (SML) (Haskell) +code_gen fac + (SML) (Haskell) +code_gen n (SML) (Haskell) code_gen "op + :: nat \ nat \ nat" @@ -101,7 +105,9 @@ "op < :: nat \ nat \ bool" "op <= :: nat \ nat \ bool" code_gen - Pair fst snd Let split swap swapp appl + Pair fst snd Let split swap +code_gen + appl code_gen k "op + :: int \ int \ int" @@ -122,43 +128,31 @@ code_gen mut1 mut2 code_gen - "op @" filter concat foldl foldr hd tl - last butlast list_all2 - map - nth - list_update - take - drop - takeWhile - dropWhile - rev - zip - upt - remdups remove1 null - "distinct" replicate rotate1 rotate splice - (SML) (Haskell) +code_gen + remdups + "distinct" code_gen foo1 foo3 code_gen - "op = :: bool \ bool \ bool" - "op = :: nat \ nat \ bool" - "op = :: int \ int \ bool" - "op = :: 'a * 'b \ 'a * 'b \ bool" - "op = :: 'a + 'b \ 'a + 'b \ bool" - "op = :: 'a option \ 'a option \ bool" - "op = :: 'a list \ 'a list \ bool" - "op = :: point \ point \ bool" - "op = :: mut1 \ mut1 \ bool" - "op = :: mut2 \ mut2 \ bool" + "OperationalEquality.eq :: bool \ bool \ bool" + "OperationalEquality.eq :: nat \ nat \ bool" + "OperationalEquality.eq :: int \ int \ bool" + "OperationalEquality.eq :: ('a\eq) * ('b\eq) \ 'a * 'b \ bool" + "OperationalEquality.eq :: ('a\eq) + ('b\eq) \ 'a + 'b \ bool" + "OperationalEquality.eq :: ('a\eq) option \ 'a option \ bool" + "OperationalEquality.eq :: ('a\eq) list \ 'a list \ bool" + "OperationalEquality.eq :: mut1 \ mut1 \ bool" + "OperationalEquality.eq :: mut2 \ mut2 \ bool" + "OperationalEquality.eq :: ('a\eq) point_scheme \ 'a point_scheme \ bool" code_gen f g h -code_gen (SML -) +code_gen (SML -) (SML _) end \ No newline at end of file diff -r 3950e65f48f8 -r 65fe827aa595 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Sep 19 15:22:03 2006 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Sep 19 15:22:05 2006 +0200 @@ -6,7 +6,6 @@ no_document time_use_thy "Classpackage"; no_document time_use_thy "Codegenerator"; -no_document time_use_thy "CodeOperationalEquality"; no_document time_use_thy "CodeCollections"; no_document time_use_thy "CodeEval"; no_document time_use_thy "CodeRandom"; diff -r 3950e65f48f8 -r 65fe827aa595 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Sep 19 15:22:03 2006 +0200 +++ b/src/Pure/IsaMakefile Tue Sep 19 15:22:05 2006 +0200 @@ -59,9 +59,9 @@ Tools/am_interpreter.ML Tools/am_util.ML \ Tools/codegen_consts.ML \ Tools/codegen_names.ML \ - Tools/class_package.ML \ + Tools/class_package.ML Tools/codegen_data.ML \ Tools/codegen_package.ML Tools/codegen_serializer.ML \ - Tools/codegen_theorems.ML Tools/codegen_simtype.ML \ + Tools/codegen_funcgr.ML Tools/codegen_simtype.ML \ Tools/codegen_thingol.ML Tools/compute.ML \ Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \ assumption.ML axclass.ML codegen.ML compress.ML conjunction.ML consts.ML \