certificates for code generator case expressions
authorhaftmann
Thu Oct 04 19:54:44 2007 +0200 (2007-10-04)
changeset 2484498c006a30218
parent 24843 0fc73c4003ac
child 24845 abcd15369ffa
certificates for code generator case expressions
src/HOL/Code_Setup.thy
src/HOL/HOL.thy
src/HOL/Product_Type.thy
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
src/Tools/code/code_package.ML
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Oct 04 19:46:09 2007 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:54:44 2007 +0200
     1.3 @@ -127,11 +127,6 @@
     1.4  
     1.5  lemmas [code func] = Let_def if_True if_False
     1.6  
     1.7 -setup {*
     1.8 -  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
     1.9 -  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
    1.10 -*}
    1.11 -
    1.12  
    1.13  subsection {* Evaluation oracle *}
    1.14  
    1.15 @@ -160,5 +155,4 @@
    1.16        THEN' resolve_tac [TrueI, refl]))
    1.17  *} "solve goal by normalization"
    1.18  
    1.19 -
    1.20  end
     2.1 --- a/src/HOL/HOL.thy	Thu Oct 04 19:46:09 2007 +0200
     2.2 +++ b/src/HOL/HOL.thy	Thu Oct 04 19:54:44 2007 +0200
     2.3 @@ -1687,6 +1687,23 @@
     2.4  
     2.5  code_datatype "TYPE('a)"
     2.6  
     2.7 +lemma Let_case_cert:
     2.8 +  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
     2.9 +  shows "CASE x \<equiv> f x"
    2.10 +  using assms by simp_all
    2.11 +
    2.12 +lemma If_case_cert:
    2.13 +  includes meta_conjunction_syntax
    2.14 +  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    2.15 +  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    2.16 +  using assms by simp_all
    2.17 +
    2.18 +setup {*
    2.19 +  Code.add_case @{thm Let_case_cert}
    2.20 +  #> Code.add_case @{thm If_case_cert}
    2.21 +  #> Code.add_undefined @{const_name undefined}
    2.22 +*}
    2.23 +
    2.24  
    2.25  subsection {* Legacy tactics and ML bindings *}
    2.26  
     3.1 --- a/src/HOL/Product_Type.thy	Thu Oct 04 19:46:09 2007 +0200
     3.2 +++ b/src/HOL/Product_Type.thy	Thu Oct 04 19:54:44 2007 +0200
     3.3 @@ -807,12 +807,10 @@
     3.4  declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
     3.5  declare prod_caseE' [elim!] prod_caseE [elim!]
     3.6  
     3.7 -lemma prod_case_split [code post]:
     3.8 +lemma prod_case_split:
     3.9    "prod_case = split"
    3.10    by (auto simp add: expand_fun_eq)
    3.11  
    3.12 -lemmas [code inline] = prod_case_split [symmetric]
    3.13 -
    3.14  
    3.15  subsection {* Further cases/induct rules for tuples *}
    3.16  
    3.17 @@ -902,6 +900,15 @@
    3.18  lemma [code func]:
    3.19    "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
    3.20  
    3.21 +lemma split_case_cert:
    3.22 +  assumes "CASE \<equiv> split f"
    3.23 +  shows "CASE (a, b) \<equiv> f a b"
    3.24 +  using assms by simp
    3.25 +
    3.26 +setup {*
    3.27 +  Code.add_case @{thm split_case_cert}
    3.28 +*}
    3.29 +
    3.30  code_type *
    3.31    (SML infix 2 "*")
    3.32    (OCaml infix 2 "*")
     4.1 --- a/src/Pure/Isar/code.ML	Thu Oct 04 19:46:09 2007 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 04 19:54:44 2007 +0200
     4.3 @@ -24,12 +24,16 @@
     4.4    val del_post: thm -> theory -> theory
     4.5    val add_datatype: (string * typ) list -> theory -> theory
     4.6    val add_datatype_cmd: string list -> theory -> theory
     4.7 +  val add_case: thm -> theory -> theory
     4.8 +  val add_undefined: string -> theory -> theory
     4.9  
    4.10    val coregular_algebra: theory -> Sorts.algebra
    4.11    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
    4.12    val these_funcs: theory -> string -> thm list
    4.13    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    4.14    val get_datatype_of_constr: theory -> string -> string option
    4.15 +  val get_case_data: theory -> string -> (int * string list) option
    4.16 +  val is_undefined: theory -> string -> bool
    4.17    val default_typ: theory -> string -> typ
    4.18  
    4.19    val preprocess_conv: cterm -> thm
    4.20 @@ -89,9 +93,9 @@
    4.21  fun certificate thy f r =
    4.22    case Susp.peek r
    4.23     of SOME thms => (Susp.value o f thy) thms
    4.24 -     | NONE => let
    4.25 -          val thy_ref = Theory.check_thy thy;
    4.26 -        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    4.27 +    | NONE => let
    4.28 +        val thy_ref = Theory.check_thy thy;
    4.29 +      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    4.30  
    4.31  fun merge' _ ([], []) = (false, [])
    4.32    | merge' _ ([], ys) = (true, ys)
    4.33 @@ -231,10 +235,6 @@
    4.34      fun merge c x = let val (touched, thms') = merge_sdthms x in
    4.35        (if touched then cs''' := cons c (!cs''') else (); thms') end;
    4.36    in (cs'' @ !cs''', Symtab.join merge tabs) end;
    4.37 -fun merge_funcs (thms1, thms2) =
    4.38 -  let
    4.39 -    val (consts, thms) = join_func_thms (thms1, thms2);
    4.40 -  in (SOME consts, thms) end;
    4.41  
    4.42  val eq_string = op = : string * string -> bool;
    4.43  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
    4.44 @@ -253,22 +253,37 @@
    4.45        then raise Symtab.SAME else cos2;
    4.46    in ((new_types, diff_types), Symtab.join join tabs) end;
    4.47  
    4.48 +fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
    4.49 +  let
    4.50 +    val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2)
    4.51 +      @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1);
    4.52 +    val touched2 = subtract (op =) (Symtab.keys undefs1) (Symtab.keys undefs2)
    4.53 +      @ subtract (op =) (Symtab.keys undefs2) (Symtab.keys undefs1);
    4.54 +    val touched = fold (insert (op =)) touched1 touched2;
    4.55 +  in
    4.56 +    (touched, (Symtab.merge (K true) (cases1, cases2),
    4.57 +      Symtab.merge (K true) (undefs1, undefs2)))
    4.58 +  end;
    4.59 +
    4.60  datatype spec = Spec of {
    4.61    funcs: sdthms Symtab.table,
    4.62 -  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
    4.63 +  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
    4.64 +  cases: (int * string list) Symtab.table * unit Symtab.table
    4.65  };
    4.66  
    4.67 -fun mk_spec (funcs, dtyps) =
    4.68 -  Spec { funcs = funcs, dtyps = dtyps };
    4.69 -fun map_spec f (Spec { funcs = funcs, dtyps = dtyps }) =
    4.70 -  mk_spec (f (funcs, dtyps));
    4.71 -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1 },
    4.72 -  Spec { funcs = funcs2, dtyps = dtyps2 }) =
    4.73 +fun mk_spec (funcs, (dtyps, cases)) =
    4.74 +  Spec { funcs = funcs, dtyps = dtyps, cases = cases };
    4.75 +fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
    4.76 +  mk_spec (f (funcs, (dtyps, cases)));
    4.77 +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    4.78 +  Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
    4.79    let
    4.80 -    val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
    4.81 +    val (touched_cs, funcs) = join_func_thms (funcs1, funcs2);
    4.82      val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
    4.83 -    val touched = if new_types orelse diff_types then NONE else touched_cs;
    4.84 -  in (touched, mk_spec (funcs, dtyps)) end;
    4.85 +    val (touched_cases, cases) = merge_cases (cases1, cases2);
    4.86 +    val touched = if new_types orelse diff_types then NONE else
    4.87 +      SOME (fold (insert (op =)) touched_cases touched_cs);
    4.88 +  in (touched, mk_spec (funcs, (dtyps, cases))) end;
    4.89  
    4.90  datatype exec = Exec of {
    4.91    thmproc: thmproc,
    4.92 @@ -287,15 +302,17 @@
    4.93      val touched = if touched' then NONE else touched_cs;
    4.94    in (touched, mk_exec (thmproc, spec)) end;
    4.95  val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
    4.96 -  mk_spec (Symtab.empty, Symtab.empty));
    4.97 +  mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
    4.98  
    4.99  fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
   4.100  fun the_spec (Exec { spec = Spec x, ...}) = x;
   4.101  val the_funcs = #funcs o the_spec;
   4.102  val the_dtyps = #dtyps o the_spec;
   4.103 +val the_cases = #cases o the_spec;
   4.104  val map_thmproc = map_exec o apfst o map_thmproc;
   4.105  val map_funcs = map_exec o apsnd o map_spec o apfst;
   4.106 -val map_dtyps = map_exec o apsnd o map_spec o apsnd;
   4.107 +val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst;
   4.108 +val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd;
   4.109  
   4.110  
   4.111  (* data slots dependent on executable content *)
   4.112 @@ -376,7 +393,7 @@
   4.113  
   4.114  (* access to executable content *)
   4.115  
   4.116 -val get_exec = fst o CodeData.get;
   4.117 +val the_exec = fst o CodeData.get;
   4.118  
   4.119  fun map_exec_purge touched f thy =
   4.120    CodeData.map (fn (exec, data) => 
   4.121 @@ -413,7 +430,7 @@
   4.122  fun print_codesetup thy =
   4.123    let
   4.124      val ctxt = ProofContext.init thy;
   4.125 -    val exec = get_exec thy;
   4.126 +    val exec = the_exec thy;
   4.127      fun pretty_func (s, lthms) =
   4.128        (Pretty.block o Pretty.fbreaks) (
   4.129          Pretty.str s :: pretty_sdthms ctxt lthms
   4.130 @@ -532,7 +549,7 @@
   4.131        o try (AxClass.params_of_class thy)) class;
   4.132      val funcs = classparams
   4.133        |> map (fn c => Class.inst_const thy (c, tyco))
   4.134 -      |> map (Symtab.lookup ((the_funcs o get_exec) thy))
   4.135 +      |> map (Symtab.lookup ((the_funcs o the_exec) thy))
   4.136        |> (map o Option.map) (Susp.force o fst)
   4.137        |> maps these
   4.138        |> map (Thm.transfer thy)
   4.139 @@ -653,7 +670,7 @@
   4.140    else error ("No such " ^ msg ^ ": " ^ quote key);
   4.141  
   4.142  fun get_datatype thy tyco =
   4.143 -  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   4.144 +  case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   4.145     of SOME spec => spec
   4.146      | NONE => Sign.arity_number thy tyco
   4.147          |> Name.invents Name.context "'a"
   4.148 @@ -663,7 +680,7 @@
   4.149  fun get_datatype_of_constr thy c =
   4.150    case (snd o strip_type o Sign.the_const_type thy) c
   4.151     of Type (tyco, _) => if member (op =)
   4.152 -       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c
   4.153 +       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o the_exec) thy)) tyco) c
   4.154         then SOME tyco else NONE
   4.155      | _ => NONE;
   4.156  
   4.157 @@ -676,6 +693,10 @@
   4.158          in SOME (Logic.varifyT ty) end
   4.159      | NONE => NONE;
   4.160  
   4.161 +val get_case_data = Symtab.lookup o fst o the_cases o the_exec;
   4.162 +
   4.163 +val is_undefined = Symtab.defined o snd o the_cases o the_exec;
   4.164 +
   4.165  fun add_func thm thy =
   4.166    let
   4.167      val func = mk_func thm;
   4.168 @@ -746,7 +767,7 @@
   4.169      val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
   4.170      val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
   4.171      val purge_cs = map fst (snd vs_cos);
   4.172 -    val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   4.173 +    val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   4.174       of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
   4.175        | NONE => NONE;
   4.176    in
   4.177 @@ -760,6 +781,16 @@
   4.178      val cs = map (CodeUnit.read_bare_const thy) raw_cs;
   4.179    in add_datatype cs thy end;
   4.180  
   4.181 +fun add_case thm thy =
   4.182 +  let
   4.183 +    val entry as (c, _) = CodeUnit.case_cert thm;
   4.184 +  in
   4.185 +    (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
   4.186 +  end;
   4.187 +
   4.188 +fun add_undefined c thy =
   4.189 +  (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
   4.190 +
   4.191  fun add_inline thm thy =
   4.192    (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   4.193      (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   4.194 @@ -850,9 +881,9 @@
   4.195  
   4.196  fun preprocess thy thms =
   4.197    thms
   4.198 -  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o get_exec) thy)
   4.199 -  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
   4.200 -  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
   4.201 +  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o the_exec) thy)
   4.202 +  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o the_exec) thy))
   4.203 +  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
   4.204  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   4.205    |> common_typ_funcs
   4.206    |> map (Conv.fconv_rule (Class.unoverload thy));
   4.207 @@ -862,9 +893,9 @@
   4.208      val thy = Thm.theory_of_cterm ct;
   4.209    in
   4.210      ct
   4.211 -    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
   4.212 +    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
   4.213      |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
   4.214 -        ((#inline_procs o the_thmproc o get_exec) thy)
   4.215 +        ((#inline_procs o the_thmproc o the_exec) thy)
   4.216      |> rhs_conv (Class.unoverload thy)
   4.217    end;
   4.218  
   4.219 @@ -876,7 +907,7 @@
   4.220    in
   4.221      ct
   4.222      |> Class.overload thy
   4.223 -    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
   4.224 +    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
   4.225    end;
   4.226  
   4.227  fun postprocess_term thy = term_of_conv thy postprocess_conv;
   4.228 @@ -894,7 +925,7 @@
   4.229  local
   4.230  
   4.231  fun get_funcs thy const =
   4.232 -  Symtab.lookup ((the_funcs o get_exec) thy) const
   4.233 +  Symtab.lookup ((the_funcs o the_exec) thy) const
   4.234    |> Option.map (Susp.force o fst)
   4.235    |> these
   4.236    |> map (Thm.transfer thy);
     5.1 --- a/src/Pure/Isar/code_unit.ML	Thu Oct 04 19:46:09 2007 +0200
     5.2 +++ b/src/Pure/Isar/code_unit.ML	Thu Oct 04 19:54:44 2007 +0200
     5.3 @@ -2,11 +2,23 @@
     5.4      ID:         $Id$
     5.5      Author:     Florian Haftmann, TU Muenchen
     5.6  
     5.7 -Basic units of code generation.  Auxiliary.
     5.8 +Basic notions of code generation.  Auxiliary.
     5.9  *)
    5.10  
    5.11  signature CODE_UNIT =
    5.12  sig
    5.13 +  (*generic non-sense*)
    5.14 +  val bad_thm: string -> 'a
    5.15 +  val error_thm: (thm -> thm) -> thm -> thm
    5.16 +  val warning_thm: (thm -> thm) -> thm -> thm option
    5.17 +  val try_thm: (thm -> thm) -> thm -> thm option
    5.18 +
    5.19 +  (*typ instantiations*)
    5.20 +  val typ_sort_inst: Sorts.algebra -> typ * sort
    5.21 +    -> sort Vartab.table -> sort Vartab.table
    5.22 +  val inst_thm: sort Vartab.table -> thm -> thm
    5.23 +
    5.24 +  (*constants*)
    5.25    val string_of_typ: theory -> typ -> string
    5.26    val string_of_const: theory -> string -> string
    5.27    val no_args: theory -> string -> int
    5.28 @@ -15,25 +27,22 @@
    5.29    val read_const_exprs: theory -> (string list -> string list)
    5.30      -> string list -> bool * string list
    5.31  
    5.32 +  (*constructor sets*)
    5.33    val constrset_of_consts: theory -> (string * typ) list
    5.34      -> string * ((string * sort) list * (string * typ list) list)
    5.35 -  val typ_sort_inst: Sorts.algebra -> typ * sort
    5.36 -    -> sort Vartab.table -> sort Vartab.table
    5.37  
    5.38 +  (*defining equations*)
    5.39    val assert_rew: thm -> thm
    5.40    val mk_rew: thm -> thm
    5.41    val mk_func: thm -> thm
    5.42    val head_func: thm -> string * typ
    5.43 -  val bad_thm: string -> 'a
    5.44 -  val error_thm: (thm -> thm) -> thm -> thm
    5.45 -  val warning_thm: (thm -> thm) -> thm -> thm option
    5.46 -  val try_thm: (thm -> thm) -> thm -> thm option
    5.47 -
    5.48 -  val inst_thm: sort Vartab.table -> thm -> thm
    5.49    val expand_eta: int -> thm -> thm
    5.50    val rewrite_func: thm list -> thm -> thm
    5.51    val norm_args: thm list -> thm list 
    5.52 -  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list 
    5.53 +  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list
    5.54 +
    5.55 +  (*case certificates*)
    5.56 +  val case_cert: thm -> string * (int * string list)
    5.57  end;
    5.58  
    5.59  structure CodeUnit: CODE_UNIT =
    5.60 @@ -360,4 +369,49 @@
    5.61      |> map Drule.zero_var_indexes
    5.62    end;
    5.63  
    5.64 +
    5.65 +(* case cerificates *)
    5.66 +
    5.67 +fun case_cert thm =
    5.68 +  let
    5.69 +    (*FIXME rework this code*)
    5.70 +    val thy = Thm.theory_of_thm thm;
    5.71 +    val (cas, t_pats) = (Logic.dest_implies o Thm.prop_of) thm;
    5.72 +    val pats = Logic.dest_conjunctions t_pats;
    5.73 +    val (head, proto_case_expr) = Logic.dest_equals cas;
    5.74 +    val _ = case head of Free _ => true
    5.75 +      | Var _ => true
    5.76 +      | _ => raise TERM ("case_cert", []);
    5.77 +    val ([(case_expr_v, _)], case_expr) = Term.strip_abs_eta 1 proto_case_expr;
    5.78 +    val (Const (c_case, _), raw_params) = strip_comb case_expr;
    5.79 +    val i = find_index
    5.80 +      (fn Free (v, _) => v = case_expr_v | _ => false) raw_params;
    5.81 +    val _ = if i = ~1 then raise TERM ("case_cert", []) else ();
    5.82 +    val t_params = nth_drop i raw_params;
    5.83 +    val params = map (fst o dest_Var) t_params;
    5.84 +    fun dest_pat t =
    5.85 +      let
    5.86 +        val (head' $ t_co, rhs) = Logic.dest_equals t;
    5.87 +        val _ = if head' = head then () else raise TERM ("case_cert", []);
    5.88 +        val (Const (co, _), args) = strip_comb t_co;
    5.89 +        val (Var (param, _), args') = strip_comb rhs;
    5.90 +        val _ = if args' = args then () else raise TERM ("case_cert", []);
    5.91 +      in (param, co) end;
    5.92 +    fun analyze_pats pats =
    5.93 +      let
    5.94 +        val co_list = fold (AList.update (op =) o dest_pat) pats [];
    5.95 +      in map (the o AList.lookup (op =) co_list) params end;
    5.96 +    fun analyze_let t =
    5.97 +      let
    5.98 +        val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
    5.99 +        val _ = if head' = head then () else raise TERM ("case_cert", []);
   5.100 +        val _ = if arg' = arg then () else raise TERM ("case_cert", []);
   5.101 +        val _ = if [param'] = params then () else raise TERM ("case_cert", []);
   5.102 +      in [] end;
   5.103 +  in (c_case, (i, case pats
   5.104 +   of [pat] => (analyze_pats pats handle Bind => analyze_let pat)
   5.105 +    | _ :: _ => analyze_pats pats))
   5.106 +  end handle Bind => error "bad case certificate"
   5.107 +    | TERM _ => error "bad case certificate";
   5.108 +
   5.109  end;
     6.1 --- a/src/Tools/code/code_package.ML	Thu Oct 04 19:46:09 2007 +0200
     6.2 +++ b/src/Tools/code/code_package.ML	Thu Oct 04 19:54:44 2007 +0200
     6.3 @@ -20,14 +20,6 @@
     6.4    val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
     6.5      -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
     6.6    val codegen_command: theory -> string -> unit;
     6.7 -
     6.8 -  type appgen;
     6.9 -  val add_appconst: string * appgen -> theory -> theory;
    6.10 -  val appgen_let: appgen;
    6.11 -  val appgen_if: appgen;
    6.12 -  val appgen_case: (theory -> term
    6.13 -    -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
    6.14 -    -> appgen;
    6.15  end;
    6.16  
    6.17  structure CodePackage : CODE_PACKAGE =
    6.18 @@ -35,23 +27,7 @@
    6.19  
    6.20  open BasicCodeThingol;
    6.21  
    6.22 -(** code translation **)
    6.23 -
    6.24 -(* theory data *)
    6.25 -
    6.26 -type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
    6.27 -  -> CodeFuncgr.T
    6.28 -  -> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact;
    6.29 -
    6.30 -structure Appgens = TheoryDataFun
    6.31 -(
    6.32 -  type T = (int * (appgen * stamp)) Symtab.table;
    6.33 -  val empty = Symtab.empty;
    6.34 -  val copy = I;
    6.35 -  val extend = I;
    6.36 -  fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
    6.37 -    bounds1 = bounds2 andalso stamp1 = stamp2);
    6.38 -);
    6.39 +(** code theorems **)
    6.40  
    6.41  fun code_depgr thy [] = CodeFuncgr.make thy []
    6.42    | code_depgr thy consts =
    6.43 @@ -80,6 +56,9 @@
    6.44      val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
    6.45    in Present.display_graph prgr end;
    6.46  
    6.47 +
    6.48 +(** code translation **)
    6.49 +
    6.50  structure Program = CodeDataFun
    6.51  (
    6.52    type T = CodeThingol.code;
    6.53 @@ -313,29 +292,55 @@
    6.54    exprgen_const thy algbr funcgr c_ty
    6.55    ##>> fold_map (exprgen_term thy algbr funcgr) ts
    6.56    #>> (fn (t, ts) => t `$$ ts)
    6.57 -and exprgen_app thy algbr funcgr ((c, ty), ts) =
    6.58 -  case Symtab.lookup (Appgens.get thy) c
    6.59 -   of SOME (i, (appgen, _)) =>
    6.60 -        if length ts < i then
    6.61 -          let
    6.62 -            val k = length ts;
    6.63 -            val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
    6.64 -            val ctxt = (fold o fold_aterms)
    6.65 -              (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
    6.66 -            val vs = Name.names ctxt "a" tys;
    6.67 -          in
    6.68 -            fold_map (exprgen_typ thy algbr funcgr) tys
    6.69 -            ##>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs)
    6.70 -            #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
    6.71 -          end
    6.72 -        else if length ts > i then
    6.73 -          appgen thy algbr funcgr ((c, ty), Library.take (i, ts))
    6.74 -          ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
    6.75 -          #>> (fn (t, ts) => t `$$ ts)
    6.76 -        else
    6.77 -          appgen thy algbr funcgr ((c, ty), ts)
    6.78 -    | NONE =>
    6.79 -        exprgen_app_default thy algbr funcgr ((c, ty), ts);
    6.80 +and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
    6.81 +  let
    6.82 +    (*FIXME rework this code*)
    6.83 +    val (all_tys, _) = strip_type ty;
    6.84 +    val (tys, _) = chop (1 + (if null cases then 1 else length cases)) all_tys;
    6.85 +    val st = nth ts n;
    6.86 +    val sty = nth tys n;
    6.87 +    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
    6.88 +      | is_undefined _ = false;
    6.89 +    fun mk_case (co, n) t =
    6.90 +      let
    6.91 +        val (vs, body) = Term.strip_abs_eta n t;
    6.92 +        val selector = list_comb (Const (co, map snd vs ---> sty), map Free vs);
    6.93 +      in if is_undefined body then NONE else SOME (selector, body) end;
    6.94 +    val ds = case cases
    6.95 +     of [] => let val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
    6.96 +          in [(Free v_ty, body)] end
    6.97 +      | cases => map_filter (uncurry mk_case) (AList.make (CodeUnit.no_args thy) cases
    6.98 +          ~~ nth_drop n ts);
    6.99 +  in
   6.100 +    exprgen_term thy algbr funcgr st
   6.101 +    ##>> exprgen_typ thy algbr funcgr sty
   6.102 +    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
   6.103 +          ##>> exprgen_term thy algbr funcgr body) ds
   6.104 +    ##>> exprgen_app_default thy algbr funcgr app
   6.105 +    #>> (fn (((st, sty), ds), t0) => ICase (((st, sty), ds), t0))
   6.106 +  end
   6.107 +and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
   6.108 + of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
   6.109 +      if length ts < i then
   6.110 +        let
   6.111 +          val k = length ts;
   6.112 +          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
   6.113 +          val ctxt = (fold o fold_aterms)
   6.114 +            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
   6.115 +          val vs = Name.names ctxt "a" tys;
   6.116 +        in
   6.117 +          fold_map (exprgen_typ thy algbr funcgr) tys
   6.118 +          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
   6.119 +          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   6.120 +        end
   6.121 +      else if length ts > i then
   6.122 +        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
   6.123 +        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
   6.124 +        #>> (fn (t, ts) => t `$$ ts)
   6.125 +      else
   6.126 +        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
   6.127 +      end
   6.128 +  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
   6.129  
   6.130  
   6.131  (* entrance points into translation kernel *)
   6.132 @@ -362,52 +367,6 @@
   6.133      ^ CodeUnit.string_of_typ thy ty_decl);
   6.134  
   6.135  
   6.136 -(* parametrized application generators, for instantiation in object logic *)
   6.137 -(* (axiomatic extensions of translation kernel) *)
   6.138 -
   6.139 -fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) =
   6.140 -  let
   6.141 -    val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
   6.142 -    fun clause_gen (dt, bt) =
   6.143 -      exprgen_term thy algbr funcgr
   6.144 -        (map_aterms (fn Const (c_ty as (c, ty)) => Const
   6.145 -          (Class.unoverload_const thy c_ty, ty) | t => t) dt)
   6.146 -      ##>> exprgen_term thy algbr funcgr bt;
   6.147 -  in
   6.148 -    exprgen_term thy algbr funcgr st
   6.149 -    ##>> exprgen_typ thy algbr funcgr sty
   6.150 -    ##>> fold_map clause_gen ds
   6.151 -    ##>> exprgen_app_default thy algbr funcgr app
   6.152 -    #>> (fn (((se, sty), ds), t0) => ICase (((se, sty), ds), t0))
   6.153 -  end;
   6.154 -
   6.155 -fun appgen_let thy algbr funcgr (app as (_, [st, ct])) =
   6.156 -  exprgen_term thy algbr funcgr ct
   6.157 -  ##>> exprgen_term thy algbr funcgr st
   6.158 -  ##>> exprgen_app_default thy algbr funcgr app
   6.159 -  #>> (fn (((v, ty) `|-> be, se), t0) =>
   6.160 -            ICase (CodeThingol.collapse_let (((v, ty), se), be), t0)
   6.161 -        | (_, t0) => t0);
   6.162 -
   6.163 -fun appgen_if thy algbr funcgr (app as (_, [tb, tt, tf])) =
   6.164 -  exprgen_term thy algbr funcgr tb
   6.165 -  ##>> exprgen_typ thy algbr funcgr (Type ("bool", []))
   6.166 -  ##>> exprgen_term thy algbr funcgr (Const ("True", Type ("bool", [])))
   6.167 -  ##>> exprgen_term thy algbr funcgr tt
   6.168 -  ##>> exprgen_term thy algbr funcgr (Const ("False", Type ("bool", [])))
   6.169 -  ##>> exprgen_term thy algbr funcgr tf
   6.170 -  ##>> exprgen_app_default thy algbr funcgr app
   6.171 -  #>> (fn ((((((tb, B), T), tt), F), tf), t0) => ICase (((tb, B), [(T, tt), (F, tf)]), t0));
   6.172 -
   6.173 -fun add_appconst (c, appgen) thy =
   6.174 -  let
   6.175 -    val i = (length o fst o strip_type o Sign.the_const_type thy) c;
   6.176 -    val _ = Program.change thy (K CodeThingol.empty_code);
   6.177 -  in
   6.178 -    Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy
   6.179 -  end;
   6.180 -
   6.181 -
   6.182  (** code generation interfaces **)
   6.183  
   6.184  (* generic generation combinators *)