src/Pure/Isar/code.ML
changeset 24844 98c006a30218
parent 24837 cacc5744be75
child 24848 5dbbd33c3236
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 04 19:46:09 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 04 19:54:44 2007 +0200
     1.3 @@ -24,12 +24,16 @@
     1.4    val del_post: thm -> theory -> theory
     1.5    val add_datatype: (string * typ) list -> theory -> theory
     1.6    val add_datatype_cmd: string list -> theory -> theory
     1.7 +  val add_case: thm -> theory -> theory
     1.8 +  val add_undefined: string -> theory -> theory
     1.9  
    1.10    val coregular_algebra: theory -> Sorts.algebra
    1.11    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
    1.12    val these_funcs: theory -> string -> thm list
    1.13    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    1.14    val get_datatype_of_constr: theory -> string -> string option
    1.15 +  val get_case_data: theory -> string -> (int * string list) option
    1.16 +  val is_undefined: theory -> string -> bool
    1.17    val default_typ: theory -> string -> typ
    1.18  
    1.19    val preprocess_conv: cterm -> thm
    1.20 @@ -89,9 +93,9 @@
    1.21  fun certificate thy f r =
    1.22    case Susp.peek r
    1.23     of SOME thms => (Susp.value o f thy) thms
    1.24 -     | NONE => let
    1.25 -          val thy_ref = Theory.check_thy thy;
    1.26 -        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    1.27 +    | NONE => let
    1.28 +        val thy_ref = Theory.check_thy thy;
    1.29 +      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    1.30  
    1.31  fun merge' _ ([], []) = (false, [])
    1.32    | merge' _ ([], ys) = (true, ys)
    1.33 @@ -231,10 +235,6 @@
    1.34      fun merge c x = let val (touched, thms') = merge_sdthms x in
    1.35        (if touched then cs''' := cons c (!cs''') else (); thms') end;
    1.36    in (cs'' @ !cs''', Symtab.join merge tabs) end;
    1.37 -fun merge_funcs (thms1, thms2) =
    1.38 -  let
    1.39 -    val (consts, thms) = join_func_thms (thms1, thms2);
    1.40 -  in (SOME consts, thms) end;
    1.41  
    1.42  val eq_string = op = : string * string -> bool;
    1.43  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
    1.44 @@ -253,22 +253,37 @@
    1.45        then raise Symtab.SAME else cos2;
    1.46    in ((new_types, diff_types), Symtab.join join tabs) end;
    1.47  
    1.48 +fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
    1.49 +  let
    1.50 +    val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2)
    1.51 +      @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1);
    1.52 +    val touched2 = subtract (op =) (Symtab.keys undefs1) (Symtab.keys undefs2)
    1.53 +      @ subtract (op =) (Symtab.keys undefs2) (Symtab.keys undefs1);
    1.54 +    val touched = fold (insert (op =)) touched1 touched2;
    1.55 +  in
    1.56 +    (touched, (Symtab.merge (K true) (cases1, cases2),
    1.57 +      Symtab.merge (K true) (undefs1, undefs2)))
    1.58 +  end;
    1.59 +
    1.60  datatype spec = Spec of {
    1.61    funcs: sdthms Symtab.table,
    1.62 -  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
    1.63 +  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
    1.64 +  cases: (int * string list) Symtab.table * unit Symtab.table
    1.65  };
    1.66  
    1.67 -fun mk_spec (funcs, dtyps) =
    1.68 -  Spec { funcs = funcs, dtyps = dtyps };
    1.69 -fun map_spec f (Spec { funcs = funcs, dtyps = dtyps }) =
    1.70 -  mk_spec (f (funcs, dtyps));
    1.71 -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1 },
    1.72 -  Spec { funcs = funcs2, dtyps = dtyps2 }) =
    1.73 +fun mk_spec (funcs, (dtyps, cases)) =
    1.74 +  Spec { funcs = funcs, dtyps = dtyps, cases = cases };
    1.75 +fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
    1.76 +  mk_spec (f (funcs, (dtyps, cases)));
    1.77 +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    1.78 +  Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
    1.79    let
    1.80 -    val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
    1.81 +    val (touched_cs, funcs) = join_func_thms (funcs1, funcs2);
    1.82      val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
    1.83 -    val touched = if new_types orelse diff_types then NONE else touched_cs;
    1.84 -  in (touched, mk_spec (funcs, dtyps)) end;
    1.85 +    val (touched_cases, cases) = merge_cases (cases1, cases2);
    1.86 +    val touched = if new_types orelse diff_types then NONE else
    1.87 +      SOME (fold (insert (op =)) touched_cases touched_cs);
    1.88 +  in (touched, mk_spec (funcs, (dtyps, cases))) end;
    1.89  
    1.90  datatype exec = Exec of {
    1.91    thmproc: thmproc,
    1.92 @@ -287,15 +302,17 @@
    1.93      val touched = if touched' then NONE else touched_cs;
    1.94    in (touched, mk_exec (thmproc, spec)) end;
    1.95  val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
    1.96 -  mk_spec (Symtab.empty, Symtab.empty));
    1.97 +  mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
    1.98  
    1.99  fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
   1.100  fun the_spec (Exec { spec = Spec x, ...}) = x;
   1.101  val the_funcs = #funcs o the_spec;
   1.102  val the_dtyps = #dtyps o the_spec;
   1.103 +val the_cases = #cases o the_spec;
   1.104  val map_thmproc = map_exec o apfst o map_thmproc;
   1.105  val map_funcs = map_exec o apsnd o map_spec o apfst;
   1.106 -val map_dtyps = map_exec o apsnd o map_spec o apsnd;
   1.107 +val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst;
   1.108 +val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd;
   1.109  
   1.110  
   1.111  (* data slots dependent on executable content *)
   1.112 @@ -376,7 +393,7 @@
   1.113  
   1.114  (* access to executable content *)
   1.115  
   1.116 -val get_exec = fst o CodeData.get;
   1.117 +val the_exec = fst o CodeData.get;
   1.118  
   1.119  fun map_exec_purge touched f thy =
   1.120    CodeData.map (fn (exec, data) => 
   1.121 @@ -413,7 +430,7 @@
   1.122  fun print_codesetup thy =
   1.123    let
   1.124      val ctxt = ProofContext.init thy;
   1.125 -    val exec = get_exec thy;
   1.126 +    val exec = the_exec thy;
   1.127      fun pretty_func (s, lthms) =
   1.128        (Pretty.block o Pretty.fbreaks) (
   1.129          Pretty.str s :: pretty_sdthms ctxt lthms
   1.130 @@ -532,7 +549,7 @@
   1.131        o try (AxClass.params_of_class thy)) class;
   1.132      val funcs = classparams
   1.133        |> map (fn c => Class.inst_const thy (c, tyco))
   1.134 -      |> map (Symtab.lookup ((the_funcs o get_exec) thy))
   1.135 +      |> map (Symtab.lookup ((the_funcs o the_exec) thy))
   1.136        |> (map o Option.map) (Susp.force o fst)
   1.137        |> maps these
   1.138        |> map (Thm.transfer thy)
   1.139 @@ -653,7 +670,7 @@
   1.140    else error ("No such " ^ msg ^ ": " ^ quote key);
   1.141  
   1.142  fun get_datatype thy tyco =
   1.143 -  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   1.144 +  case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   1.145     of SOME spec => spec
   1.146      | NONE => Sign.arity_number thy tyco
   1.147          |> Name.invents Name.context "'a"
   1.148 @@ -663,7 +680,7 @@
   1.149  fun get_datatype_of_constr thy c =
   1.150    case (snd o strip_type o Sign.the_const_type thy) c
   1.151     of Type (tyco, _) => if member (op =)
   1.152 -       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c
   1.153 +       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o the_exec) thy)) tyco) c
   1.154         then SOME tyco else NONE
   1.155      | _ => NONE;
   1.156  
   1.157 @@ -676,6 +693,10 @@
   1.158          in SOME (Logic.varifyT ty) end
   1.159      | NONE => NONE;
   1.160  
   1.161 +val get_case_data = Symtab.lookup o fst o the_cases o the_exec;
   1.162 +
   1.163 +val is_undefined = Symtab.defined o snd o the_cases o the_exec;
   1.164 +
   1.165  fun add_func thm thy =
   1.166    let
   1.167      val func = mk_func thm;
   1.168 @@ -746,7 +767,7 @@
   1.169      val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
   1.170      val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
   1.171      val purge_cs = map fst (snd vs_cos);
   1.172 -    val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   1.173 +    val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   1.174       of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
   1.175        | NONE => NONE;
   1.176    in
   1.177 @@ -760,6 +781,16 @@
   1.178      val cs = map (CodeUnit.read_bare_const thy) raw_cs;
   1.179    in add_datatype cs thy end;
   1.180  
   1.181 +fun add_case thm thy =
   1.182 +  let
   1.183 +    val entry as (c, _) = CodeUnit.case_cert thm;
   1.184 +  in
   1.185 +    (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
   1.186 +  end;
   1.187 +
   1.188 +fun add_undefined c thy =
   1.189 +  (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.190 +
   1.191  fun add_inline thm thy =
   1.192    (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   1.193      (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   1.194 @@ -850,9 +881,9 @@
   1.195  
   1.196  fun preprocess thy thms =
   1.197    thms
   1.198 -  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o get_exec) thy)
   1.199 -  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
   1.200 -  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
   1.201 +  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o the_exec) thy)
   1.202 +  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o the_exec) thy))
   1.203 +  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
   1.204  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   1.205    |> common_typ_funcs
   1.206    |> map (Conv.fconv_rule (Class.unoverload thy));
   1.207 @@ -862,9 +893,9 @@
   1.208      val thy = Thm.theory_of_cterm ct;
   1.209    in
   1.210      ct
   1.211 -    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
   1.212 +    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
   1.213      |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
   1.214 -        ((#inline_procs o the_thmproc o get_exec) thy)
   1.215 +        ((#inline_procs o the_thmproc o the_exec) thy)
   1.216      |> rhs_conv (Class.unoverload thy)
   1.217    end;
   1.218  
   1.219 @@ -876,7 +907,7 @@
   1.220    in
   1.221      ct
   1.222      |> Class.overload thy
   1.223 -    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
   1.224 +    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
   1.225    end;
   1.226  
   1.227  fun postprocess_term thy = term_of_conv thy postprocess_conv;
   1.228 @@ -894,7 +925,7 @@
   1.229  local
   1.230  
   1.231  fun get_funcs thy const =
   1.232 -  Symtab.lookup ((the_funcs o get_exec) thy) const
   1.233 +  Symtab.lookup ((the_funcs o the_exec) thy) const
   1.234    |> Option.map (Susp.force o fst)
   1.235    |> these
   1.236    |> map (Thm.transfer thy);