# HG changeset patch # User haftmann # Date 1191520484 -7200 # Node ID 98c006a30218c8a0304713788c179f13f40ac764 # Parent 0fc73c4003ac44f6d6be79857c29152680c57c72 certificates for code generator case expressions diff -r 0fc73c4003ac -r 98c006a30218 src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Thu Oct 04 19:46:09 2007 +0200 +++ b/src/HOL/Code_Setup.thy Thu Oct 04 19:54:44 2007 +0200 @@ -127,11 +127,6 @@ lemmas [code func] = Let_def if_True if_False -setup {* - CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let) - #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if) -*} - subsection {* Evaluation oracle *} @@ -160,5 +155,4 @@ THEN' resolve_tac [TrueI, refl])) *} "solve goal by normalization" - end diff -r 0fc73c4003ac -r 98c006a30218 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Oct 04 19:46:09 2007 +0200 +++ b/src/HOL/HOL.thy Thu Oct 04 19:54:44 2007 +0200 @@ -1687,6 +1687,23 @@ code_datatype "TYPE('a)" +lemma Let_case_cert: + assumes "CASE \ (\x. Let x f)" + shows "CASE x \ f x" + using assms by simp_all + +lemma If_case_cert: + includes meta_conjunction_syntax + assumes "CASE \ (\b. If b f g)" + shows "(CASE True \ f) && (CASE False \ g)" + using assms by simp_all + +setup {* + Code.add_case @{thm Let_case_cert} + #> Code.add_case @{thm If_case_cert} + #> Code.add_undefined @{const_name undefined} +*} + subsection {* Legacy tactics and ML bindings *} diff -r 0fc73c4003ac -r 98c006a30218 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Oct 04 19:46:09 2007 +0200 +++ b/src/HOL/Product_Type.thy Thu Oct 04 19:54:44 2007 +0200 @@ -807,12 +807,10 @@ declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] declare prod_caseE' [elim!] prod_caseE [elim!] -lemma prod_case_split [code post]: +lemma prod_case_split: "prod_case = split" by (auto simp add: expand_fun_eq) -lemmas [code inline] = prod_case_split [symmetric] - subsection {* Further cases/induct rules for tuples *} @@ -902,6 +900,15 @@ lemma [code func]: "(x1\'a\eq, y1\'b\eq) = (x2, y2) \ x1 = x2 \ y1 = y2" by auto +lemma split_case_cert: + assumes "CASE \ split f" + shows "CASE (a, b) \ f a b" + using assms by simp + +setup {* + Code.add_case @{thm split_case_cert} +*} + code_type * (SML infix 2 "*") (OCaml infix 2 "*") diff -r 0fc73c4003ac -r 98c006a30218 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Oct 04 19:46:09 2007 +0200 +++ b/src/Pure/Isar/code.ML Thu Oct 04 19:54:44 2007 +0200 @@ -24,12 +24,16 @@ val del_post: thm -> theory -> theory val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory + val add_case: thm -> theory -> theory + val add_undefined: string -> theory -> theory val coregular_algebra: theory -> Sorts.algebra val operational_algebra: theory -> (sort -> sort) * Sorts.algebra val these_funcs: theory -> string -> thm list val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option + val get_case_data: theory -> string -> (int * string list) option + val is_undefined: theory -> string -> bool val default_typ: theory -> string -> typ val preprocess_conv: cterm -> thm @@ -89,9 +93,9 @@ fun certificate thy f r = case Susp.peek r of SOME thms => (Susp.value o f thy) thms - | NONE => let - val thy_ref = Theory.check_thy thy; - in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end; + | NONE => let + val thy_ref = Theory.check_thy thy; + in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end; fun merge' _ ([], []) = (false, []) | merge' _ ([], ys) = (true, ys) @@ -231,10 +235,6 @@ fun merge c x = let val (touched, thms') = merge_sdthms x in (if touched then cs''' := cons c (!cs''') else (); thms') end; in (cs'' @ !cs''', Symtab.join merge tabs) end; -fun merge_funcs (thms1, thms2) = - let - val (consts, thms) = join_func_thms (thms1, thms2); - in (SOME consts, thms) end; val eq_string = op = : string * string -> bool; fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = @@ -253,22 +253,37 @@ then raise Symtab.SAME else cos2; in ((new_types, diff_types), Symtab.join join tabs) end; +fun merge_cases ((cases1, undefs1), (cases2, undefs2)) = + let + val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2) + @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1); + val touched2 = subtract (op =) (Symtab.keys undefs1) (Symtab.keys undefs2) + @ subtract (op =) (Symtab.keys undefs2) (Symtab.keys undefs1); + val touched = fold (insert (op =)) touched1 touched2; + in + (touched, (Symtab.merge (K true) (cases1, cases2), + Symtab.merge (K true) (undefs1, undefs2))) + end; + datatype spec = Spec of { funcs: sdthms Symtab.table, - dtyps: ((string * sort) list * (string * typ list) list) Symtab.table + dtyps: ((string * sort) list * (string * typ list) list) Symtab.table, + cases: (int * string list) Symtab.table * unit Symtab.table }; -fun mk_spec (funcs, dtyps) = - Spec { funcs = funcs, dtyps = dtyps }; -fun map_spec f (Spec { funcs = funcs, dtyps = dtyps }) = - mk_spec (f (funcs, dtyps)); -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1 }, - Spec { funcs = funcs2, dtyps = dtyps2 }) = +fun mk_spec (funcs, (dtyps, cases)) = + Spec { funcs = funcs, dtyps = dtyps, cases = cases }; +fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) = + mk_spec (f (funcs, (dtyps, cases))); +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 }, + Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) = let - val (touched_cs, funcs) = merge_funcs (funcs1, funcs2); + val (touched_cs, funcs) = join_func_thms (funcs1, funcs2); val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2); - val touched = if new_types orelse diff_types then NONE else touched_cs; - in (touched, mk_spec (funcs, dtyps)) end; + val (touched_cases, cases) = merge_cases (cases1, cases2); + val touched = if new_types orelse diff_types then NONE else + SOME (fold (insert (op =)) touched_cases touched_cs); + in (touched, mk_spec (funcs, (dtyps, cases))) end; datatype exec = Exec of { thmproc: thmproc, @@ -287,15 +302,17 @@ val touched = if touched' then NONE else touched_cs; in (touched, mk_exec (thmproc, spec)) end; val empty_exec = mk_exec (mk_thmproc ((([], []), []), []), - mk_spec (Symtab.empty, Symtab.empty)); + mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))); fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x; fun the_spec (Exec { spec = Spec x, ...}) = x; val the_funcs = #funcs o the_spec; val the_dtyps = #dtyps o the_spec; +val the_cases = #cases o the_spec; val map_thmproc = map_exec o apfst o map_thmproc; val map_funcs = map_exec o apsnd o map_spec o apfst; -val map_dtyps = map_exec o apsnd o map_spec o apsnd; +val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst; +val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd; (* data slots dependent on executable content *) @@ -376,7 +393,7 @@ (* access to executable content *) -val get_exec = fst o CodeData.get; +val the_exec = fst o CodeData.get; fun map_exec_purge touched f thy = CodeData.map (fn (exec, data) => @@ -413,7 +430,7 @@ fun print_codesetup thy = let val ctxt = ProofContext.init thy; - val exec = get_exec thy; + val exec = the_exec thy; fun pretty_func (s, lthms) = (Pretty.block o Pretty.fbreaks) ( Pretty.str s :: pretty_sdthms ctxt lthms @@ -532,7 +549,7 @@ o try (AxClass.params_of_class thy)) class; val funcs = classparams |> map (fn c => Class.inst_const thy (c, tyco)) - |> map (Symtab.lookup ((the_funcs o get_exec) thy)) + |> map (Symtab.lookup ((the_funcs o the_exec) thy)) |> (map o Option.map) (Susp.force o fst) |> maps these |> map (Thm.transfer thy) @@ -653,7 +670,7 @@ else error ("No such " ^ msg ^ ": " ^ quote key); fun get_datatype thy tyco = - case Symtab.lookup ((the_dtyps o get_exec) thy) tyco + case Symtab.lookup ((the_dtyps o the_exec) thy) tyco of SOME spec => spec | NONE => Sign.arity_number thy tyco |> Name.invents Name.context "'a" @@ -663,7 +680,7 @@ fun get_datatype_of_constr thy c = case (snd o strip_type o Sign.the_const_type thy) c of Type (tyco, _) => if member (op =) - ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c + ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o the_exec) thy)) tyco) c then SOME tyco else NONE | _ => NONE; @@ -676,6 +693,10 @@ in SOME (Logic.varifyT ty) end | NONE => NONE; +val get_case_data = Symtab.lookup o fst o the_cases o the_exec; + +val is_undefined = Symtab.defined o snd o the_cases o the_exec; + fun add_func thm thy = let val func = mk_func thm; @@ -746,7 +767,7 @@ val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs; val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs; val purge_cs = map fst (snd vs_cos); - val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco + val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos) | NONE => NONE; in @@ -760,6 +781,16 @@ val cs = map (CodeUnit.read_bare_const thy) raw_cs; in add_datatype cs thy end; +fun add_case thm thy = + let + val entry as (c, _) = CodeUnit.case_cert thm; + in + (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy + end; + +fun add_undefined c thy = + (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy; + fun add_inline thm thy = (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst) (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy; @@ -850,9 +881,9 @@ fun preprocess thy thms = thms - |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o get_exec) thy) - |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o get_exec) thy)) - |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy) + |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o the_exec) thy) + |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o the_exec) thy)) + |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy) (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *) |> common_typ_funcs |> map (Conv.fconv_rule (Class.unoverload thy)); @@ -862,9 +893,9 @@ val thy = Thm.theory_of_cterm ct; in ct - |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy) + |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy) |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f)) - ((#inline_procs o the_thmproc o get_exec) thy) + ((#inline_procs o the_thmproc o the_exec) thy) |> rhs_conv (Class.unoverload thy) end; @@ -876,7 +907,7 @@ in ct |> Class.overload thy - |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy)) + |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy)) end; fun postprocess_term thy = term_of_conv thy postprocess_conv; @@ -894,7 +925,7 @@ local fun get_funcs thy const = - Symtab.lookup ((the_funcs o get_exec) thy) const + Symtab.lookup ((the_funcs o the_exec) thy) const |> Option.map (Susp.force o fst) |> these |> map (Thm.transfer thy); diff -r 0fc73c4003ac -r 98c006a30218 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Thu Oct 04 19:46:09 2007 +0200 +++ b/src/Pure/Isar/code_unit.ML Thu Oct 04 19:54:44 2007 +0200 @@ -2,11 +2,23 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Basic units of code generation. Auxiliary. +Basic notions of code generation. Auxiliary. *) signature CODE_UNIT = sig + (*generic non-sense*) + val bad_thm: string -> 'a + val error_thm: (thm -> thm) -> thm -> thm + val warning_thm: (thm -> thm) -> thm -> thm option + val try_thm: (thm -> thm) -> thm -> thm option + + (*typ instantiations*) + val typ_sort_inst: Sorts.algebra -> typ * sort + -> sort Vartab.table -> sort Vartab.table + val inst_thm: sort Vartab.table -> thm -> thm + + (*constants*) val string_of_typ: theory -> typ -> string val string_of_const: theory -> string -> string val no_args: theory -> string -> int @@ -15,25 +27,22 @@ val read_const_exprs: theory -> (string list -> string list) -> string list -> bool * string list + (*constructor sets*) val constrset_of_consts: theory -> (string * typ) list -> string * ((string * sort) list * (string * typ list) list) - val typ_sort_inst: Sorts.algebra -> typ * sort - -> sort Vartab.table -> sort Vartab.table + (*defining equations*) val assert_rew: thm -> thm val mk_rew: thm -> thm val mk_func: thm -> thm val head_func: thm -> string * typ - val bad_thm: string -> 'a - val error_thm: (thm -> thm) -> thm -> thm - val warning_thm: (thm -> thm) -> thm -> thm option - val try_thm: (thm -> thm) -> thm -> thm option - - val inst_thm: sort Vartab.table -> thm -> thm val expand_eta: int -> thm -> thm val rewrite_func: thm list -> thm -> thm val norm_args: thm list -> thm list - val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list + val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list + + (*case certificates*) + val case_cert: thm -> string * (int * string list) end; structure CodeUnit: CODE_UNIT = @@ -360,4 +369,49 @@ |> map Drule.zero_var_indexes end; + +(* case cerificates *) + +fun case_cert thm = + let + (*FIXME rework this code*) + val thy = Thm.theory_of_thm thm; + val (cas, t_pats) = (Logic.dest_implies o Thm.prop_of) thm; + val pats = Logic.dest_conjunctions t_pats; + val (head, proto_case_expr) = Logic.dest_equals cas; + val _ = case head of Free _ => true + | Var _ => true + | _ => raise TERM ("case_cert", []); + val ([(case_expr_v, _)], case_expr) = Term.strip_abs_eta 1 proto_case_expr; + val (Const (c_case, _), raw_params) = strip_comb case_expr; + val i = find_index + (fn Free (v, _) => v = case_expr_v | _ => false) raw_params; + val _ = if i = ~1 then raise TERM ("case_cert", []) else (); + val t_params = nth_drop i raw_params; + val params = map (fst o dest_Var) t_params; + fun dest_pat t = + let + val (head' $ t_co, rhs) = Logic.dest_equals t; + val _ = if head' = head then () else raise TERM ("case_cert", []); + val (Const (co, _), args) = strip_comb t_co; + val (Var (param, _), args') = strip_comb rhs; + val _ = if args' = args then () else raise TERM ("case_cert", []); + in (param, co) end; + fun analyze_pats pats = + let + val co_list = fold (AList.update (op =) o dest_pat) pats []; + in map (the o AList.lookup (op =) co_list) params end; + fun analyze_let t = + let + val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; + val _ = if head' = head then () else raise TERM ("case_cert", []); + val _ = if arg' = arg then () else raise TERM ("case_cert", []); + val _ = if [param'] = params then () else raise TERM ("case_cert", []); + in [] end; + in (c_case, (i, case pats + of [pat] => (analyze_pats pats handle Bind => analyze_let pat) + | _ :: _ => analyze_pats pats)) + end handle Bind => error "bad case certificate" + | TERM _ => error "bad case certificate"; + end; diff -r 0fc73c4003ac -r 98c006a30218 src/Tools/code/code_package.ML --- a/src/Tools/code/code_package.ML Thu Oct 04 19:46:09 2007 +0200 +++ b/src/Tools/code/code_package.ML Thu Oct 04 19:54:44 2007 +0200 @@ -20,14 +20,6 @@ val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a; val codegen_command: theory -> string -> unit; - - type appgen; - val add_appconst: string * appgen -> theory -> theory; - val appgen_let: appgen; - val appgen_if: appgen; - val appgen_case: (theory -> term - -> ((string * typ) list * ((term * typ) * (term * term) list)) option) - -> appgen; end; structure CodePackage : CODE_PACKAGE = @@ -35,23 +27,7 @@ open BasicCodeThingol; -(** code translation **) - -(* theory data *) - -type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T - -> CodeFuncgr.T - -> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact; - -structure Appgens = TheoryDataFun -( - type T = (int * (appgen * stamp)) Symtab.table; - val empty = Symtab.empty; - val copy = I; - val extend = I; - fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => - bounds1 = bounds2 andalso stamp1 = stamp2); -); +(** code theorems **) fun code_depgr thy [] = CodeFuncgr.make thy [] | code_depgr thy consts = @@ -80,6 +56,9 @@ val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr []; in Present.display_graph prgr end; + +(** code translation **) + structure Program = CodeDataFun ( type T = CodeThingol.code; @@ -313,29 +292,55 @@ exprgen_const thy algbr funcgr c_ty ##>> fold_map (exprgen_term thy algbr funcgr) ts #>> (fn (t, ts) => t `$$ ts) -and exprgen_app thy algbr funcgr ((c, ty), ts) = - case Symtab.lookup (Appgens.get thy) c - of SOME (i, (appgen, _)) => - if length ts < i then - let - val k = length ts; - val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty; - val ctxt = (fold o fold_aterms) - (fn Free (v, _) => Name.declare v | _ => I) ts Name.context; - val vs = Name.names ctxt "a" tys; - in - fold_map (exprgen_typ thy algbr funcgr) tys - ##>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs) - #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t) - end - else if length ts > i then - appgen thy algbr funcgr ((c, ty), Library.take (i, ts)) - ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts)) - #>> (fn (t, ts) => t `$$ ts) - else - appgen thy algbr funcgr ((c, ty), ts) - | NONE => - exprgen_app_default thy algbr funcgr ((c, ty), ts); +and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) = + let + (*FIXME rework this code*) + val (all_tys, _) = strip_type ty; + val (tys, _) = chop (1 + (if null cases then 1 else length cases)) all_tys; + val st = nth ts n; + val sty = nth tys n; + fun is_undefined (Const (c, _)) = Code.is_undefined thy c + | is_undefined _ = false; + fun mk_case (co, n) t = + let + val (vs, body) = Term.strip_abs_eta n t; + val selector = list_comb (Const (co, map snd vs ---> sty), map Free vs); + in if is_undefined body then NONE else SOME (selector, body) end; + val ds = case cases + of [] => let val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts)) + in [(Free v_ty, body)] end + | cases => map_filter (uncurry mk_case) (AList.make (CodeUnit.no_args thy) cases + ~~ nth_drop n ts); + in + exprgen_term thy algbr funcgr st + ##>> exprgen_typ thy algbr funcgr sty + ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat + ##>> exprgen_term thy algbr funcgr body) ds + ##>> exprgen_app_default thy algbr funcgr app + #>> (fn (((st, sty), ds), t0) => ICase (((st, sty), ds), t0)) + end +and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c + of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in + if length ts < i then + let + val k = length ts; + val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty; + val ctxt = (fold o fold_aterms) + (fn Free (v, _) => Name.declare v | _ => I) ts Name.context; + val vs = Name.names ctxt "a" tys; + in + fold_map (exprgen_typ thy algbr funcgr) tys + ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs) + #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t) + end + else if length ts > i then + exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts)) + ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts)) + #>> (fn (t, ts) => t `$$ ts) + else + exprgen_case thy algbr funcgr n cases ((c, ty), ts) + end + | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts); (* entrance points into translation kernel *) @@ -362,52 +367,6 @@ ^ CodeUnit.string_of_typ thy ty_decl); -(* parametrized application generators, for instantiation in object logic *) -(* (axiomatic extensions of translation kernel) *) - -fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) = - let - val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts)); - fun clause_gen (dt, bt) = - exprgen_term thy algbr funcgr - (map_aterms (fn Const (c_ty as (c, ty)) => Const - (Class.unoverload_const thy c_ty, ty) | t => t) dt) - ##>> exprgen_term thy algbr funcgr bt; - in - exprgen_term thy algbr funcgr st - ##>> exprgen_typ thy algbr funcgr sty - ##>> fold_map clause_gen ds - ##>> exprgen_app_default thy algbr funcgr app - #>> (fn (((se, sty), ds), t0) => ICase (((se, sty), ds), t0)) - end; - -fun appgen_let thy algbr funcgr (app as (_, [st, ct])) = - exprgen_term thy algbr funcgr ct - ##>> exprgen_term thy algbr funcgr st - ##>> exprgen_app_default thy algbr funcgr app - #>> (fn (((v, ty) `|-> be, se), t0) => - ICase (CodeThingol.collapse_let (((v, ty), se), be), t0) - | (_, t0) => t0); - -fun appgen_if thy algbr funcgr (app as (_, [tb, tt, tf])) = - exprgen_term thy algbr funcgr tb - ##>> exprgen_typ thy algbr funcgr (Type ("bool", [])) - ##>> exprgen_term thy algbr funcgr (Const ("True", Type ("bool", []))) - ##>> exprgen_term thy algbr funcgr tt - ##>> exprgen_term thy algbr funcgr (Const ("False", Type ("bool", []))) - ##>> exprgen_term thy algbr funcgr tf - ##>> exprgen_app_default thy algbr funcgr app - #>> (fn ((((((tb, B), T), tt), F), tf), t0) => ICase (((tb, B), [(T, tt), (F, tf)]), t0)); - -fun add_appconst (c, appgen) thy = - let - val i = (length o fst o strip_type o Sign.the_const_type thy) c; - val _ = Program.change thy (K CodeThingol.empty_code); - in - Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy - end; - - (** code generation interfaces **) (* generic generation combinators *)