src/Pure/Isar/code.ML
changeset 30076 f3043dafef5f
parent 30060 672012330c4e
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/Isar/code.ML	Mon Feb 23 10:07:57 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Feb 23 21:38:36 2009 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4      (*with explicit history*),
     1.5    dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
     1.6      (*with explicit history*),
     1.7 -  cases: (int * string list) Symtab.table * unit Symtab.table
     1.8 +  cases: (int * (int * string list)) Symtab.table * unit Symtab.table
     1.9  };
    1.10  
    1.11  fun mk_spec ((concluded_history, eqns), (dtyps, cases)) =
    1.12 @@ -574,12 +574,7 @@
    1.13  
    1.14  fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
    1.15  
    1.16 -fun get_case_scheme thy c = case Symtab.lookup ((fst o the_cases o the_exec) thy) c
    1.17 - of SOME (base_case_scheme as (_, case_pats)) =>
    1.18 -      if forall (is_some o get_datatype_of_constr thy) case_pats
    1.19 -      then SOME (1 + Int.max (1, length case_pats), base_case_scheme)
    1.20 -      else NONE
    1.21 -  | NONE => NONE;
    1.22 +fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
    1.23  
    1.24  val is_undefined = Symtab.defined o snd o the_cases o the_exec;
    1.25  
    1.26 @@ -589,11 +584,17 @@
    1.27    let
    1.28      val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
    1.29      val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
    1.30 +    val old_cs = (map fst o snd o get_datatype thy) tyco;
    1.31 +    fun drop_outdated_cases cases = fold Symtab.delete_safe
    1.32 +      (Symtab.fold (fn (c, (_, (_, cos))) =>
    1.33 +        if exists (member (op =) old_cs) cos
    1.34 +          then insert (op =) c else I) cases []) cases;
    1.35    in
    1.36      thy
    1.37      |> map_exec_purge NONE
    1.38          ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
    1.39 -        #> map_eqns (fold (Symtab.delete_safe o fst) cs))
    1.40 +        #> map_eqns (fold (Symtab.delete_safe o fst) cs)
    1.41 +        #> (map_cases o apfst) drop_outdated_cases)
    1.42      |> TypeInterpretation.data (tyco, serial ())
    1.43    end;
    1.44  
    1.45 @@ -607,10 +608,12 @@
    1.46  
    1.47  fun add_case thm thy =
    1.48    let
    1.49 -    val entry as (c, _) = Code_Unit.case_cert thm;
    1.50 -  in
    1.51 -    (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
    1.52 -  end;
    1.53 +    val (c, (k, case_pats)) = Code_Unit.case_cert thm;
    1.54 +    val _ = case filter (is_none o get_datatype_of_constr thy) case_pats
    1.55 +     of [] => ()
    1.56 +      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
    1.57 +    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
    1.58 +  in (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update (c, entry)) thy end;
    1.59  
    1.60  fun add_undefined c thy =
    1.61    (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;