a simple concept for datatype invariants
authorhaftmann
Fri Feb 19 11:06:21 2010 +0100 (2010-02-19)
changeset 35226b987b803616d
parent 35225 dfbcff38c9ed
child 35227 d67857e3a8c0
a simple concept for datatype invariants
src/Pure/Isar/code.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/code.ML	Fri Feb 19 11:06:21 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Feb 19 11:06:21 2010 +0100
     1.3 @@ -22,6 +22,8 @@
     1.4    (*constructor sets*)
     1.5    val constrset_of_consts: theory -> (string * typ) list
     1.6      -> string * ((string * sort) list * (string * typ list) list)
     1.7 +  val abstype_cert: theory -> string * typ -> string
     1.8 +    -> string * ((string * sort) list * ((string * typ) * (string * term)))
     1.9  
    1.10    (*code equations and certificates*)
    1.11    val mk_eqn: theory -> thm * bool -> thm * bool
    1.12 @@ -34,9 +36,10 @@
    1.13    val empty_cert: theory -> string -> cert
    1.14    val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
    1.15    val constrain_cert: theory -> sort list -> cert -> cert
    1.16 -  val typscheme_cert: theory -> cert -> (string * sort) list * typ
    1.17 -  val equations_cert: theory -> cert -> ((string * sort) list * typ) * (term list * term) list
    1.18 -  val equations_thms_cert: theory -> cert -> ((string * sort) list * typ) * ((term list * term) * (thm * bool)) list
    1.19 +  val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
    1.20 +  val equations_of_cert: theory -> cert ->
    1.21 +    ((string * sort) list * typ) * ((string option * (term list * term)) * (thm option * bool)) list
    1.22 +  val bare_thms_of_cert: theory -> cert -> thm list
    1.23    val pretty_cert: theory -> cert -> Pretty.T list
    1.24  
    1.25    (*executable code*)
    1.26 @@ -46,6 +49,8 @@
    1.27    val add_signature_cmd: string * string -> theory -> theory
    1.28    val add_datatype: (string * typ) list -> theory -> theory
    1.29    val add_datatype_cmd: string list -> theory -> theory
    1.30 +  val add_abstype: string * typ -> string * typ -> theory -> Proof.state
    1.31 +  val add_abstype_cmd: string -> string -> theory -> Proof.state
    1.32    val type_interpretation:
    1.33      (string * ((string * sort) list * (string * typ list) list)
    1.34        -> theory -> theory) -> theory -> theory
    1.35 @@ -59,7 +64,9 @@
    1.36    val add_case: thm -> theory -> theory
    1.37    val add_undefined: string -> theory -> theory
    1.38    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    1.39 -  val get_datatype_of_constr: theory -> string -> string option
    1.40 +  val get_datatype_of_constr_or_abstr: theory -> string -> (string * bool) option
    1.41 +  val is_constr: theory -> string -> bool
    1.42 +  val is_abstr: theory -> string -> bool
    1.43    val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
    1.44    val get_case_scheme: theory -> string -> (int * (int * string list)) option
    1.45    val undefineds: theory -> string list
    1.46 @@ -122,34 +129,31 @@
    1.47  fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
    1.48  
    1.49  
    1.50 -
    1.51  (** data store **)
    1.52  
    1.53 -(* code equations *)
    1.54 +(* datatypes *)
    1.55 +
    1.56 +datatype typ_spec = Constructors of (string * typ list) list
    1.57 +  | Abstractor of (string * typ) * (string * thm);
    1.58  
    1.59 -type eqns = bool * (thm * bool) list;
    1.60 -  (*default flag, theorems with proper flag *)
    1.61 +fun constructors_of (Constructors cos) = (cos, false)
    1.62 +  | constructors_of (Abstractor ((co, ty), _)) = ([(co, [ty])], true);
    1.63 +
    1.64 +
    1.65 +(* functions *)
    1.66  
    1.67 -fun add_drop_redundant thy (thm, proper) thms =
    1.68 -  let
    1.69 -    val args_of = snd o strip_comb o map_types Type.strip_sorts
    1.70 -      o fst o Logic.dest_equals o Thm.plain_prop_of;
    1.71 -    val args = args_of thm;
    1.72 -    val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
    1.73 -    fun matches_args args' = length args <= length args' andalso
    1.74 -      Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
    1.75 -    fun drop (thm', proper') = if (proper orelse not proper')
    1.76 -      andalso matches_args (args_of thm') then 
    1.77 -        (warning ("Code generator: dropping redundant code equation\n" ^
    1.78 -            Display.string_of_thm_global thy thm'); true)
    1.79 -      else false;
    1.80 -  in (thm, proper) :: filter_out drop thms end;
    1.81 +datatype fun_spec = Default of (thm * bool) list
    1.82 +  | Eqns of (thm * bool) list
    1.83 +  | Proj of term * string
    1.84 +  | Abstr of thm * string;
    1.85  
    1.86 -fun add_thm thy _ thm (false, thms) = (false, add_drop_redundant thy thm thms)
    1.87 -  | add_thm thy true thm (true, thms) = (true, thms @ [thm])
    1.88 -  | add_thm thy false thm (true, thms) = (false, [thm]);
    1.89 +val empty_fun_spec = Default [];
    1.90  
    1.91 -fun del_thm thm = apsnd (remove (eq_fst Thm.eq_thm_prop) (thm, true));
    1.92 +fun is_default (Default _) = true
    1.93 +  | is_default _ = false;
    1.94 +
    1.95 +fun associated_abstype (Abstr (_, tyco)) = SOME tyco
    1.96 +  | associated_abstype _ = NONE;
    1.97  
    1.98  
    1.99  (* executable code data *)
   1.100 @@ -157,49 +161,49 @@
   1.101  datatype spec = Spec of {
   1.102    history_concluded: bool,
   1.103    signatures: int Symtab.table * typ Symtab.table,
   1.104 -  eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
   1.105 +  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
   1.106      (*with explicit history*),
   1.107 -  dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
   1.108 +  datatypes: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
   1.109      (*with explicit history*),
   1.110    cases: (int * (int * string list)) Symtab.table * unit Symtab.table
   1.111  };
   1.112  
   1.113 -fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) =
   1.114 +fun make_spec (history_concluded, ((signatures, functions), (datatypes, cases))) =
   1.115    Spec { history_concluded = history_concluded,
   1.116 -    signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases };
   1.117 +    signatures = signatures, functions = functions, datatypes = datatypes, cases = cases };
   1.118  fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
   1.119 -  eqns = eqns, dtyps = dtyps, cases = cases }) =
   1.120 -  make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases))));
   1.121 -fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1,
   1.122 -    dtyps = dtyps1, cases = (cases1, undefs1) },
   1.123 -  Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2,
   1.124 -    dtyps = dtyps2, cases = (cases2, undefs2) }) =
   1.125 +  functions = functions, datatypes = datatypes, cases = cases }) =
   1.126 +  make_spec (f (history_concluded, ((signatures, functions), (datatypes, cases))));
   1.127 +fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), functions = functions1,
   1.128 +    datatypes = datatypes1, cases = (cases1, undefs1) },
   1.129 +  Spec { history_concluded = _, signatures = (tycos2, sigs2), functions = functions2,
   1.130 +    datatypes = datatypes2, cases = (cases2, undefs2) }) =
   1.131    let
   1.132      val signatures = (Symtab.merge (op =) (tycos1, tycos2),
   1.133        Symtab.merge typ_equiv (sigs1, sigs2));
   1.134 -    fun merge_eqns ((_, history1), (_, history2)) =
   1.135 +    fun merge_functions ((_, history1), (_, history2)) =
   1.136        let
   1.137          val raw_history = AList.merge (op = : serial * serial -> bool)
   1.138 -          (K true) (history1, history2)
   1.139 -        val filtered_history = filter_out (fst o snd) raw_history
   1.140 +          (K true) (history1, history2);
   1.141 +        val filtered_history = filter_out (is_default o snd) raw_history;
   1.142          val history = if null filtered_history
   1.143            then raw_history else filtered_history;
   1.144        in ((false, (snd o hd) history), history) end;
   1.145 -    val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2);
   1.146 -    val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
   1.147 +    val functions = Symtab.join (K merge_functions) (functions1, functions2);
   1.148 +    val datatypes = Symtab.join (K (AList.merge (op =) (K true))) (datatypes1, datatypes2);
   1.149      val cases = (Symtab.merge (K true) (cases1, cases2),
   1.150        Symtab.merge (K true) (undefs1, undefs2));
   1.151 -  in make_spec (false, ((signatures, eqns), (dtyps, cases))) end;
   1.152 +  in make_spec (false, ((signatures, functions), (datatypes, cases))) end;
   1.153  
   1.154  fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
   1.155  fun the_signatures (Spec { signatures, ... }) = signatures;
   1.156 -fun the_eqns (Spec { eqns, ... }) = eqns;
   1.157 -fun the_dtyps (Spec { dtyps, ... }) = dtyps;
   1.158 +fun the_functions (Spec { functions, ... }) = functions;
   1.159 +fun the_datatypes (Spec { datatypes, ... }) = datatypes;
   1.160  fun the_cases (Spec { cases, ... }) = cases;
   1.161  val map_history_concluded = map_spec o apfst;
   1.162  val map_signatures = map_spec o apsnd o apfst o apfst;
   1.163 -val map_eqns = map_spec o apsnd o apfst o apsnd;
   1.164 -val map_dtyps = map_spec o apsnd o apsnd o apfst;
   1.165 +val map_functions = map_spec o apsnd o apfst o apsnd;
   1.166 +val map_typs = map_spec o apsnd o apsnd o apfst;
   1.167  val map_cases = map_spec o apsnd o apsnd o apsnd;
   1.168  
   1.169  
   1.170 @@ -251,6 +255,7 @@
   1.171  
   1.172  in
   1.173  
   1.174 +
   1.175  (* access to executable code *)
   1.176  
   1.177  val the_exec = fst o Code_Data.get;
   1.178 @@ -259,9 +264,9 @@
   1.179  
   1.180  val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
   1.181  
   1.182 -fun change_eqns delete c f = (map_exec_purge o map_eqns
   1.183 -  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
   1.184 -    o apfst) (fn (_, eqns) => (true, f eqns));
   1.185 +fun change_fun_spec delete c f = (map_exec_purge o map_functions
   1.186 +  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), [])))
   1.187 +    o apfst) (fn (_, spec) => (true, f spec));
   1.188  
   1.189  
   1.190  (* tackling equation history *)
   1.191 @@ -276,7 +281,7 @@
   1.192    then NONE
   1.193    else thy
   1.194      |> (Code_Data.map o apfst)
   1.195 -        ((map_eqns o Symtab.map) (fn ((changed, current), history) =>
   1.196 +        ((map_functions o Symtab.map) (fn ((changed, current), history) =>
   1.197            ((false, current),
   1.198              if changed then (serial (), current) :: history else history))
   1.199          #> map_history_concluded (K true))
   1.200 @@ -359,29 +364,32 @@
   1.201  
   1.202  (* datatypes *)
   1.203  
   1.204 -fun constrset_of_consts thy cs =
   1.205 +fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
   1.206 +  ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
   1.207 +
   1.208 +fun ty_sorts thy (c, raw_ty) =
   1.209    let
   1.210 -    val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
   1.211 -      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
   1.212 -    fun no_constr s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
   1.213 -      ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
   1.214 +    val _ = Thm.cterm_of thy (Const (c, raw_ty));
   1.215 +    val ty = subst_signature thy c raw_ty;
   1.216 +    val ty_decl = (Logic.unvarifyT o const_typ thy) c;
   1.217      fun last_typ c_ty ty =
   1.218        let
   1.219          val tfrees = Term.add_tfreesT ty [];
   1.220          val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
   1.221 -          handle TYPE _ => no_constr "bad type" c_ty
   1.222 +          handle TYPE _ => no_constr thy "bad type" c_ty
   1.223          val _ = if has_duplicates (eq_fst (op =)) vs
   1.224 -          then no_constr "duplicate type variables in datatype" c_ty else ();
   1.225 +          then no_constr thy "duplicate type variables in datatype" c_ty else ();
   1.226          val _ = if length tfrees <> length vs
   1.227 -          then no_constr "type variables missing in datatype" c_ty else ();
   1.228 +          then no_constr thy "type variables missing in datatype" c_ty else ();
   1.229        in (tyco, vs) end;
   1.230 -    fun ty_sorts (c, raw_ty) =
   1.231 -      let
   1.232 -        val ty = subst_signature thy c raw_ty;
   1.233 -        val ty_decl = (Logic.unvarifyT o const_typ thy) c;
   1.234 -        val (tyco, _) = last_typ (c, ty) ty_decl;
   1.235 -        val (_, vs) = last_typ (c, ty) ty;
   1.236 -      in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
   1.237 +    val (tyco, _) = last_typ (c, ty) ty_decl;
   1.238 +    val (_, vs) = last_typ (c, ty) ty;
   1.239 +  in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
   1.240 +
   1.241 +fun constrset_of_consts thy cs =
   1.242 +  let
   1.243 +    val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
   1.244 +      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
   1.245      fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
   1.246        let
   1.247          val _ = if (tyco' : string) <> tyco
   1.248 @@ -394,31 +402,68 @@
   1.249          val the_v = the o AList.lookup (op =) (vs ~~ vs');
   1.250          val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
   1.251        in (c, (fst o strip_type) ty') end;
   1.252 -    val c' :: cs' = map ty_sorts cs;
   1.253 +    val c' :: cs' = map (ty_sorts thy) cs;
   1.254      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
   1.255      val vs = Name.names Name.context Name.aT sorts;
   1.256      val cs''' = map (inst vs) cs'';
   1.257    in (tyco, (vs, rev cs''')) end;
   1.258  
   1.259 -fun get_datatype thy tyco =
   1.260 -  case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
   1.261 -   of (_, spec) :: _ => spec
   1.262 -    | [] => arity_number thy tyco
   1.263 -        |> Name.invents Name.context Name.aT
   1.264 -        |> map (rpair [])
   1.265 -        |> rpair [];
   1.266 +fun abstype_cert thy abs_ty rep =
   1.267 +  let
   1.268 +    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
   1.269 +      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (fst abs_ty, rep);
   1.270 +    val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy abs_ty;
   1.271 +    val (ty, ty_abs) = case ty'
   1.272 +     of Type ("fun", [ty, ty_abs]) => (ty, ty_abs)
   1.273 +      | _ => error ("Not a datatype abstractor:\n" ^ string_of_const thy abs
   1.274 +          ^ " :: " ^ string_of_typ thy ty');
   1.275 +    val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle CTERM _ =>
   1.276 +      error ("Not a projection:\n" ^ string_of_const thy rep);
   1.277 +    val cert = Logic.mk_equals (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty)
   1.278 +      $ Free ("x", ty_abs)), Free ("x", ty_abs));
   1.279 +  in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;    
   1.280 +
   1.281 +fun get_datatype_entry thy tyco = case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
   1.282 + of (_, entry) :: _ => SOME entry
   1.283 +  | _ => NONE;
   1.284  
   1.285 -fun get_datatype_of_constr thy c =
   1.286 +fun get_datatype_spec thy tyco = case get_datatype_entry thy tyco
   1.287 + of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   1.288 +  | NONE => arity_number thy tyco
   1.289 +      |> Name.invents Name.context Name.aT
   1.290 +      |> map (rpair [])
   1.291 +      |> rpair []
   1.292 +      |> rpair false;
   1.293 +
   1.294 +fun get_abstype_spec thy tyco = case get_datatype_entry thy tyco
   1.295 + of SOME (vs, Abstractor spec) => (vs, spec)
   1.296 +  | NONE => error ("Not an abstract type: " ^ tyco);
   1.297 + 
   1.298 +fun get_datatype thy = fst o get_datatype_spec thy;
   1.299 +
   1.300 +fun get_datatype_of_constr_or_abstr thy c =
   1.301    case (snd o strip_type o const_typ thy) c
   1.302 -   of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
   1.303 -       then SOME tyco else NONE
   1.304 +   of Type (tyco, _) => let val ((vs, cos), abstract) = get_datatype_spec thy tyco
   1.305 +        in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
   1.306      | _ => NONE;
   1.307  
   1.308 -fun is_constr thy = is_some o get_datatype_of_constr thy;
   1.309 +fun is_constr thy c = case get_datatype_of_constr_or_abstr thy c
   1.310 + of SOME (_, false) => true
   1.311 +   | _ => false;
   1.312 +
   1.313 +fun is_abstr thy c = case get_datatype_of_constr_or_abstr thy c
   1.314 + of SOME (_, true) => true
   1.315 +   | _ => false;
   1.316  
   1.317  
   1.318  (* bare code equations *)
   1.319  
   1.320 +(* convention for variables:
   1.321 +    ?x ?'a   for free-floating theorems (e.g. in the data store)
   1.322 +    ?x  'a   for certificates
   1.323 +     x  'a   for final representation of equations
   1.324 +*)
   1.325 +
   1.326  exception BAD_THM of string;
   1.327  fun bad_thm msg = raise BAD_THM msg;
   1.328  fun error_thm f thm = f thm handle BAD_THM msg => error msg;
   1.329 @@ -430,12 +475,9 @@
   1.330    in not (has_duplicates (op =) ((fold o fold_aterms)
   1.331      (fn Var (v, _) => cons v | _ => I) args [])) end;
   1.332  
   1.333 -fun gen_assert_eqn thy check_patterns (thm, proper) =
   1.334 +fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
   1.335    let
   1.336      fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
   1.337 -    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   1.338 -      handle TERM _ => bad "Not an equation"
   1.339 -           | THM _ => bad "Not an equation";
   1.340      fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
   1.341        | Free _ => bad "Illegal free variable in equation"
   1.342        | _ => I) t [];
   1.343 @@ -461,21 +503,23 @@
   1.344        | check _ (Var _) = bad "Variable with application on left hand side of equation"
   1.345        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   1.346        | check n (Const (c_ty as (c, ty))) =
   1.347 -          let
   1.348 +          if allow_pats then let
   1.349              val c' = AxClass.unoverload_const thy c_ty
   1.350            in if n = (length o fst o strip_type o subst_signature thy c') ty
   1.351 -            then if not proper orelse not check_patterns orelse is_constr thy c'
   1.352 +            then if allow_consts orelse is_constr thy c'
   1.353                then ()
   1.354                else bad (quote c ^ " is not a constructor, on left hand side of equation")
   1.355              else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
   1.356 -          end;
   1.357 +          end else bad ("Pattern not allowed, but constant " ^ quote c ^ " encountered on left hand side")
   1.358      val _ = map (check 0) args;
   1.359 -    val _ = if not proper orelse is_linear thm then ()
   1.360 +    val _ = if allow_nonlinear orelse is_linear thm then ()
   1.361        else bad "Duplicate variables on left hand side of equation";
   1.362      val _ = if (is_none o AxClass.class_of_param thy) c then ()
   1.363        else bad "Overloaded constant as head in equation";
   1.364      val _ = if not (is_constr thy c) then ()
   1.365        else bad "Constructor as head in equation";
   1.366 +    val _ = if not (is_abstr thy c) then ()
   1.367 +      else bad "Abstractor as head in equation";
   1.368      val ty_decl = Sign.the_const_type thy c;
   1.369      val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   1.370        then () else bad_thm ("Type\n" ^ string_of_typ thy ty
   1.371 @@ -483,8 +527,39 @@
   1.372          ^ Display.string_of_thm_global thy thm
   1.373          ^ "\nis incompatible with declared function type\n"
   1.374          ^ string_of_typ thy ty_decl)
   1.375 +  in () end;
   1.376 +
   1.377 +fun gen_assert_eqn thy check_patterns (thm, proper) =
   1.378 +  let
   1.379 +    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
   1.380 +    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   1.381 +      handle TERM _ => bad "Not an equation"
   1.382 +           | THM _ => bad "Not a proper equation";
   1.383 +    val _ = check_eqn thy { allow_nonlinear = not proper,
   1.384 +      allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
   1.385    in (thm, proper) end;
   1.386  
   1.387 +fun assert_abs_eqn thy some_tyco thm =
   1.388 +  let
   1.389 +    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
   1.390 +    val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   1.391 +      handle TERM _ => bad "Not an equation"
   1.392 +           | THM _ => bad "Not a proper equation";
   1.393 +    val (rep, lhs) = dest_comb full_lhs
   1.394 +      handle TERM _ => bad "Not an abstract equation";
   1.395 +    val tyco = (fst o dest_Type o domain_type o snd o dest_Const) rep
   1.396 +      handle TERM _ => bad "Not an abstract equation";
   1.397 +    val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
   1.398 +          else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
   1.399 +      | NONE => ();
   1.400 +    val (_, (_, (rep', _))) = get_abstype_spec thy tyco;
   1.401 +    val rep_const = (fst o dest_Const) rep;
   1.402 +    val _ = if rep_const = rep' then ()
   1.403 +      else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
   1.404 +    val _ = check_eqn thy { allow_nonlinear = false,
   1.405 +      allow_consts = false, allow_pats = false } thm (lhs, rhs);
   1.406 +  in (thm, tyco) end;
   1.407 +
   1.408  fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
   1.409  
   1.410  fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   1.411 @@ -498,6 +573,8 @@
   1.412  fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   1.413    o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
   1.414  
   1.415 +fun mk_abs_eqn thy = error_thm (assert_abs_eqn thy NONE) o meta_rewrite thy;
   1.416 +
   1.417  val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.418  
   1.419  fun const_typ_eqn thy thm =
   1.420 @@ -509,11 +586,20 @@
   1.421  
   1.422  fun const_eqn thy = fst o const_typ_eqn thy;
   1.423  
   1.424 +fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
   1.425 +  o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.426 +
   1.427  fun logical_typscheme thy (c, ty) =
   1.428    (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
   1.429  
   1.430  fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
   1.431  
   1.432 +fun mk_proj tyco vs ty abs rep =
   1.433 +  let
   1.434 +    val ty_abs = Type (tyco, map TFree vs);
   1.435 +    val xarg = Var (("x", 0), ty);
   1.436 +  in Logic.mk_equals (Const (rep, ty_abs --> ty) $ (Const (abs, ty --> ty_abs) $ xarg), xarg) end;
   1.437 +
   1.438  
   1.439  (* technical transformations of code equations *)
   1.440  
   1.441 @@ -578,7 +664,50 @@
   1.442      val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head;
   1.443    in (typscheme thy (c, ty), head) end;
   1.444  
   1.445 -abstype cert = Cert of thm * bool list with
   1.446 +fun typscheme_projection thy =
   1.447 +  typscheme thy o dest_Const o fst o dest_comb o fst o Logic.dest_equals;
   1.448 +
   1.449 +fun typscheme_abs thy =
   1.450 +  typscheme thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.prop_of;
   1.451 +
   1.452 +fun constrain_thm thy vs sorts thm =
   1.453 +  let
   1.454 +    val mapping = map2 (fn (v, sort) => fn sort' =>
   1.455 +      (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
   1.456 +    val inst = map2 (fn (v, sort) => fn (_, sort') =>
   1.457 +      (((v, 0), sort), TFree (v, sort'))) vs mapping;
   1.458 +    val subst = (map_types o map_atyps)
   1.459 +      (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
   1.460 +  in
   1.461 +    thm
   1.462 +    |> Thm.varifyT
   1.463 +    |> Thm.certify_instantiate (inst, [])
   1.464 +    |> pair subst
   1.465 +  end;
   1.466 +
   1.467 +fun concretify_abs thy tyco abs_thm =
   1.468 +  let
   1.469 +    val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
   1.470 +    val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
   1.471 +    val ty = fastype_of lhs;
   1.472 +    val ty_abs = (fastype_of o snd o dest_comb) lhs;
   1.473 +    val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs));
   1.474 +    val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm];
   1.475 +  in (c, (Thm.varifyT o zero_var_indexes) raw_concrete_thm) end;
   1.476 +
   1.477 +fun add_rhss_of_eqn thy t =
   1.478 +  let
   1.479 +    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy) t;
   1.480 +    fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty))
   1.481 +      | add_const _ = I
   1.482 +  in fold_aterms add_const t end;
   1.483 +
   1.484 +fun dest_eqn thy = apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify;
   1.485 +
   1.486 +abstype cert = Equations of thm * bool list
   1.487 +  | Projection of term * string
   1.488 +  | Abstract of thm * string
   1.489 +with
   1.490  
   1.491  fun empty_cert thy c = 
   1.492    let
   1.493 @@ -590,7 +719,7 @@
   1.494            |> map (fn v => TFree (v, []));
   1.495      val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
   1.496      val chead = build_head thy (c, ty);
   1.497 -  in Cert (Thm.weaken chead Drule.dummy_thm, []) end;
   1.498 +  in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
   1.499  
   1.500  fun cert_of_eqns thy c [] = empty_cert thy c
   1.501    | cert_of_eqns thy c raw_eqns = 
   1.502 @@ -615,65 +744,127 @@
   1.503            else Conv.rewr_conv head_thm ct;
   1.504          val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
   1.505          val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
   1.506 -      in Cert (cert_thm, propers) end;
   1.507 +      in Equations (cert_thm, propers) end;
   1.508  
   1.509 -fun constrain_cert thy sorts (Cert (cert_thm, propers)) =
   1.510 +fun cert_of_proj thy c tyco =
   1.511 +  let
   1.512 +    val (vs, ((abs, ty), (rep, cert))) = get_abstype_spec thy tyco;
   1.513 +    val _ = if c = rep then () else
   1.514 +      error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   1.515 +  in Projection (mk_proj tyco vs ty abs rep, tyco) end;
   1.516 +
   1.517 +fun cert_of_abs thy tyco c raw_abs_thm =
   1.518    let
   1.519 -    val ((vs, _), head) = get_head thy cert_thm;
   1.520 -    val subst = map2 (fn (v, sort) => fn sort' =>
   1.521 -      (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
   1.522 -    val head' = Thm.term_of head
   1.523 -      |> (map_types o map_atyps)
   1.524 -          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v)))
   1.525 -      |> Thm.cterm_of thy;
   1.526 -    val inst = map2 (fn (v, sort) => fn (_, sort') =>
   1.527 -      (((v, 0), sort), TFree (v, sort'))) vs subst;
   1.528 -    val cert_thm' = cert_thm
   1.529 -      |> Thm.implies_intr head
   1.530 -      |> Thm.varifyT
   1.531 -      |> Thm.certify_instantiate (inst, [])
   1.532 -      |> Thm.elim_implies (Thm.assume head');
   1.533 -  in (Cert (cert_thm', propers)) end;
   1.534 +    val abs_thm = singleton (canonize_thms thy) raw_abs_thm;
   1.535 +    val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
   1.536 +    val _ = if c = const_abs_eqn thy abs_thm then ()
   1.537 +      else error ("Wrong head of abstract code equation,\nexpected constant "
   1.538 +        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
   1.539 +  in Abstract (Thm.freezeT abs_thm, tyco) end;
   1.540  
   1.541 -fun typscheme_cert thy (Cert (cert_thm, _)) =
   1.542 -  fst (get_head thy cert_thm);
   1.543 +fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
   1.544 +      let
   1.545 +        val ((vs, _), head) = get_head thy cert_thm;
   1.546 +        val (subst, cert_thm') = cert_thm
   1.547 +          |> Thm.implies_intr head
   1.548 +          |> constrain_thm thy vs sorts;
   1.549 +        val head' = Thm.term_of head
   1.550 +          |> subst
   1.551 +          |> Thm.cterm_of thy;
   1.552 +        val cert_thm'' = cert_thm'
   1.553 +          |> Thm.elim_implies (Thm.assume head');
   1.554 +      in Equations (cert_thm'', propers) end
   1.555 +  | constrain_cert thy _ (cert as Projection _) =
   1.556 +      cert
   1.557 +  | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
   1.558 +      Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
   1.559 +
   1.560 +fun typscheme_of_cert thy (Equations (cert_thm, _)) =
   1.561 +      fst (get_head thy cert_thm)
   1.562 +  | typscheme_of_cert thy (Projection (proj, _)) =
   1.563 +      typscheme_projection thy proj
   1.564 +  | typscheme_of_cert thy (Abstract (abs_thm, _)) =
   1.565 +      typscheme_abs thy abs_thm;
   1.566  
   1.567 -fun equations_cert thy (cert as Cert (cert_thm, propers)) =
   1.568 -  let
   1.569 -    val tyscm = typscheme_cert thy cert;
   1.570 -    val equations = if null propers then [] else
   1.571 -      Thm.prop_of cert_thm
   1.572 -      |> Logic.dest_conjunction_balanced (length propers)
   1.573 -      |> map Logic.dest_equals
   1.574 -      |> (map o apfst) (snd o strip_comb)
   1.575 -  in (tyscm, equations) end;
   1.576 +fun typargs_deps_of_cert thy (Equations (cert_thm, propers)) =
   1.577 +      let
   1.578 +        val vs = (fst o fst) (get_head thy cert_thm);
   1.579 +        val equations = if null propers then [] else
   1.580 +          Thm.prop_of cert_thm
   1.581 +          |> Logic.dest_conjunction_balanced (length propers);
   1.582 +      in (vs, fold (add_rhss_of_eqn thy) equations []) end
   1.583 +  | typargs_deps_of_cert thy (Projection (t, tyco)) =
   1.584 +      (fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
   1.585 +  | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
   1.586 +      let
   1.587 +        val vs = fst (typscheme_abs thy abs_thm);
   1.588 +        val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
   1.589 +      in (vs, add_rhss_of_eqn thy (Thm.prop_of abs_thm) []) end;
   1.590  
   1.591 -fun equations_thms_cert thy (cert as Cert (cert_thm, propers)) =
   1.592 -  let
   1.593 -    val (tyscm, equations) = equations_cert thy cert;
   1.594 -    val thms = if null propers then [] else
   1.595 -      cert_thm
   1.596 -      |> LocalDefs.expand [snd (get_head thy cert_thm)]
   1.597 -      |> Thm.varifyT
   1.598 -      |> Conjunction.elim_balanced (length propers)
   1.599 -  in (tyscm, equations ~~ (thms ~~ propers)) end;
   1.600 +fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
   1.601 +      let
   1.602 +        val tyscm = typscheme_of_cert thy cert;
   1.603 +        val thms = if null propers then [] else
   1.604 +          cert_thm
   1.605 +          |> LocalDefs.expand [snd (get_head thy cert_thm)]
   1.606 +          |> Thm.varifyT
   1.607 +          |> Conjunction.elim_balanced (length propers);
   1.608 +      in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
   1.609 +  | equations_of_cert thy (Projection (t, tyco)) =
   1.610 +      let
   1.611 +        val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
   1.612 +        val tyscm = typscheme_projection thy t;
   1.613 +        val t' = map_types Logic.varifyT t;
   1.614 +      in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
   1.615 +  | equations_of_cert thy (Abstract (abs_thm, tyco)) =
   1.616 +      let
   1.617 +        val tyscm = typscheme_abs thy abs_thm;
   1.618 +        val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
   1.619 +        val _ = fold_aterms (fn Const (c, _) => if c = abs
   1.620 +          then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
   1.621 +          else I | _ => I) (Thm.prop_of abs_thm);
   1.622 +      in (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT abs_thm), true))]) end;
   1.623  
   1.624 -fun pretty_cert thy = map (Display.pretty_thm_global thy o AxClass.overload thy o fst o snd)
   1.625 -  o snd o equations_thms_cert thy;
   1.626 +fun pretty_cert thy (cert as Equations _) =
   1.627 +      (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
   1.628 +         o snd o equations_of_cert thy) cert
   1.629 +  | pretty_cert thy (Projection (t, _)) =
   1.630 +      [Syntax.pretty_term_global thy (map_types Logic.varifyT t)]
   1.631 +  | pretty_cert thy (Abstract (abs_thm, tyco)) =
   1.632 +      [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT) abs_thm];
   1.633 +
   1.634 +fun bare_thms_of_cert thy (cert as Equations _) =
   1.635 +      (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
   1.636 +        o snd o equations_of_cert thy) cert
   1.637 +  | bare_thms_of_cert thy _ = [];
   1.638  
   1.639  end;
   1.640  
   1.641  
   1.642 -(* code equation access *)
   1.643 +(* code certificate access *)
   1.644 +
   1.645 +fun retrieve_raw thy c =
   1.646 +  Symtab.lookup ((the_functions o the_exec) thy) c
   1.647 +  |> Option.map (snd o fst)
   1.648 +  |> the_default (Default [])
   1.649  
   1.650 -fun get_cert thy f c =
   1.651 -  Symtab.lookup ((the_eqns o the_exec) thy) c
   1.652 -  |> Option.map (snd o snd o fst)
   1.653 -  |> these
   1.654 -  |> (map o apfst) (Thm.transfer thy)
   1.655 -  |> f
   1.656 -  |> (map o apfst) (AxClass.unoverload thy)
   1.657 -  |> cert_of_eqns thy c;
   1.658 +fun get_cert thy f c = case retrieve_raw thy c
   1.659 + of Default eqns => eqns
   1.660 +      |> (map o apfst) (Thm.transfer thy)
   1.661 +      |> f
   1.662 +      |> (map o apfst) (AxClass.unoverload thy)
   1.663 +      |> cert_of_eqns thy c
   1.664 +  | Eqns eqns => eqns
   1.665 +      |> (map o apfst) (Thm.transfer thy)
   1.666 +      |> f
   1.667 +      |> (map o apfst) (AxClass.unoverload thy)
   1.668 +      |> cert_of_eqns thy c
   1.669 +  | Proj (_, tyco) =>
   1.670 +      cert_of_proj thy c tyco
   1.671 +  | Abstr (abs_thm, tyco) => abs_thm
   1.672 +      |> Thm.transfer thy
   1.673 +      |> AxClass.unoverload thy
   1.674 +      |> cert_of_abs thy tyco c;
   1.675  
   1.676  
   1.677  (* cases *)
   1.678 @@ -729,48 +920,54 @@
   1.679    let
   1.680      val ctxt = ProofContext.init thy;
   1.681      val exec = the_exec thy;
   1.682 -    fun pretty_eqns (s, (_, eqns)) =
   1.683 +    fun pretty_equations const thms =
   1.684        (Pretty.block o Pretty.fbreaks) (
   1.685 -        Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns
   1.686 +        Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
   1.687        );
   1.688 -    fun pretty_dtyp (s, []) =
   1.689 -          Pretty.str s
   1.690 -      | pretty_dtyp (s, cos) =
   1.691 -          (Pretty.block o Pretty.breaks) (
   1.692 -            Pretty.str s
   1.693 -            :: Pretty.str "="
   1.694 -            :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
   1.695 -                 | (c, tys) =>
   1.696 -                     (Pretty.block o Pretty.breaks)
   1.697 -                        (Pretty.str (string_of_const thy c)
   1.698 -                          :: Pretty.str "of"
   1.699 -                          :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
   1.700 -          );
   1.701 +    fun pretty_function (const, Default eqns) = pretty_equations const (map fst eqns)
   1.702 +      | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
   1.703 +      | pretty_function (const, Proj (proj, _)) = Pretty.block
   1.704 +          [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
   1.705 +      | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
   1.706 +    fun pretty_typ (tyco, vs) = Pretty.str
   1.707 +      (string_of_typ thy (Type (tyco, map TFree vs)));
   1.708 +    fun pretty_typspec (typ, (cos, abstract)) = if null cos
   1.709 +      then pretty_typ typ
   1.710 +      else (Pretty.block o Pretty.breaks) (
   1.711 +        pretty_typ typ
   1.712 +        :: Pretty.str "="
   1.713 +        :: (if abstract then [Pretty.str "(abstract)"] else [])
   1.714 +        @ separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
   1.715 +             | (c, tys) =>
   1.716 +                 (Pretty.block o Pretty.breaks)
   1.717 +                    (Pretty.str (string_of_const thy c)
   1.718 +                      :: Pretty.str "of"
   1.719 +                      :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
   1.720 +      );
   1.721      fun pretty_case (const, (_, (_, []))) = Pretty.str (string_of_const thy const)
   1.722        | pretty_case (const, (_, (_, cos))) = (Pretty.block o Pretty.breaks) [
   1.723            Pretty.str (string_of_const thy const), Pretty.str "with",
   1.724            (Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
   1.725 -    val eqns = the_eqns exec
   1.726 +    val functions = the_functions exec
   1.727        |> Symtab.dest
   1.728 -      |> (map o apfst) (string_of_const thy)
   1.729        |> (map o apsnd) (snd o fst)
   1.730        |> sort (string_ord o pairself fst);
   1.731 -    val dtyps = the_dtyps exec
   1.732 +    val datatypes = the_datatypes exec
   1.733        |> Symtab.dest
   1.734 -      |> map (fn (dtco, (_, (vs, cos)) :: _) =>
   1.735 -          (string_of_typ thy (Type (dtco, map TFree vs)), cos))
   1.736 -      |> sort (string_ord o pairself fst);
   1.737 +      |> map (fn (tyco, (_, (vs, spec)) :: _) =>
   1.738 +          ((tyco, vs), constructors_of spec))
   1.739 +      |> sort (string_ord o pairself (fst o fst));
   1.740      val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
   1.741      val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
   1.742    in
   1.743      (Pretty.writeln o Pretty.chunks) [
   1.744        Pretty.block (
   1.745          Pretty.str "code equations:" :: Pretty.fbrk
   1.746 -        :: (Pretty.fbreaks o map pretty_eqns) eqns
   1.747 +        :: (Pretty.fbreaks o map pretty_function) functions
   1.748        ),
   1.749        Pretty.block (
   1.750          Pretty.str "datatypes:" :: Pretty.fbrk
   1.751 -        :: (Pretty.fbreaks o map pretty_dtyp) dtyps
   1.752 +        :: (Pretty.fbreaks o map pretty_typspec) datatypes
   1.753        ),
   1.754        Pretty.block (
   1.755          Pretty.str "cases:" :: Pretty.fbrk
   1.756 @@ -816,11 +1013,27 @@
   1.757  
   1.758  (* code equations *)
   1.759  
   1.760 -fun gen_add_eqn default (thm, proper) thy =
   1.761 +fun gen_add_eqn default (raw_thm, proper) thy =
   1.762    let
   1.763 -    val thm' = Thm.close_derivation thm;
   1.764 -    val c = const_eqn thy thm';
   1.765 -  in change_eqns false c (add_thm thy default (thm', proper)) thy end;
   1.766 +    val thm = Thm.close_derivation raw_thm;
   1.767 +    val c = const_eqn thy thm;
   1.768 +    fun add_eqn' true (Default eqns) = Default (eqns @ [(thm, proper)])
   1.769 +      | add_eqn' _ (Eqns eqns) =
   1.770 +          let
   1.771 +            val args_of = snd o strip_comb o map_types Type.strip_sorts
   1.772 +              o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.773 +            val args = args_of thm;
   1.774 +            val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
   1.775 +            fun matches_args args' = length args <= length args' andalso
   1.776 +              Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
   1.777 +            fun drop (thm', proper') = if (proper orelse not proper')
   1.778 +              andalso matches_args (args_of thm') then 
   1.779 +                (warning ("Code generator: dropping redundant code equation\n" ^
   1.780 +                    Display.string_of_thm_global thy thm'); true)
   1.781 +              else false;
   1.782 +          in Eqns ((thm, proper) :: filter_out drop eqns) end
   1.783 +      | add_eqn' false _ = Eqns [(thm, proper)];
   1.784 +  in change_fun_spec false c (add_eqn' default) thy end;
   1.785  
   1.786  fun add_eqn thm thy =
   1.787    gen_add_eqn false (mk_eqn thy (thm, true)) thy;
   1.788 @@ -842,11 +1055,22 @@
   1.789    (fn thm => Context.mapping (add_default_eqn thm) I);
   1.790  val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
   1.791  
   1.792 +fun add_abs_eqn raw_thm thy =
   1.793 +  let
   1.794 +    val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm;
   1.795 +    val c = const_abs_eqn thy abs_thm;
   1.796 +  in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end;
   1.797 +
   1.798  fun del_eqn thm thy = case mk_eqn_liberal thy thm
   1.799 - of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   1.800 + of SOME (thm, _) => let
   1.801 +        fun del_eqn' (Default eqns) = empty_fun_spec
   1.802 +          | del_eqn' (Eqns eqns) =
   1.803 +              Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
   1.804 +          | del_eqn' spec = spec
   1.805 +      in change_fun_spec true (const_eqn thy thm) del_eqn' thy end
   1.806    | NONE => thy;
   1.807  
   1.808 -fun del_eqns c = change_eqns true c (K (false, []));
   1.809 +fun del_eqns c = change_fun_spec true c (K empty_fun_spec);
   1.810  
   1.811  
   1.812  (* cases *)
   1.813 @@ -869,32 +1093,69 @@
   1.814  structure Type_Interpretation =
   1.815    Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   1.816  
   1.817 -fun add_datatype raw_cs thy =
   1.818 +fun register_datatype (tyco, vs_spec) thy =
   1.819    let
   1.820 -    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
   1.821 -    val (tyco, vs_cos) = constrset_of_consts thy cs;
   1.822 -    val old_cs = (map fst o snd o get_datatype thy) tyco;
   1.823 +    val (old_constrs, some_old_proj) =
   1.824 +      case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
   1.825 +       of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
   1.826 +        | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
   1.827 +        | [] => ([], NONE)
   1.828 +    val outdated_funs = case some_old_proj
   1.829 +     of NONE => []
   1.830 +      | SOME old_proj => Symtab.fold
   1.831 +          (fn (c, ((_, spec), _)) => if member (op =) (the_list (associated_abstype spec)) tyco
   1.832 +            then insert (op =) c else I)
   1.833 +            ((the_functions o the_exec) thy) [old_proj];
   1.834      fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.835        (Symtab.fold (fn (c, (_, (_, cos))) =>
   1.836 -        if exists (member (op =) old_cs) cos
   1.837 +        if exists (member (op =) old_constrs) cos
   1.838            then insert (op =) c else I) cases []) cases;
   1.839    in
   1.840      thy
   1.841 -    |> fold (del_eqns o fst) cs
   1.842 +    |> fold del_eqns outdated_funs
   1.843      |> map_exec_purge
   1.844 -        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   1.845 +        ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
   1.846          #> (map_cases o apfst) drop_outdated_cases)
   1.847      |> Type_Interpretation.data (tyco, serial ())
   1.848    end;
   1.849  
   1.850 -fun type_interpretation f =  Type_Interpretation.interpretation
   1.851 +fun type_interpretation f = Type_Interpretation.interpretation
   1.852    (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   1.853  
   1.854 -fun add_datatype_cmd raw_cs thy =
   1.855 +fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
   1.856 +
   1.857 +fun add_datatype proto_constrs thy =
   1.858 +  let
   1.859 +    val constrs = map (unoverload_const_typ thy) proto_constrs;
   1.860 +    val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
   1.861 +  in
   1.862 +    thy
   1.863 +    |> fold (del_eqns o fst) constrs
   1.864 +    |> register_datatype (tyco, (vs, Constructors cos))
   1.865 +  end;
   1.866 +
   1.867 +fun add_datatype_cmd raw_constrs thy =
   1.868 +  add_datatype (map (read_bare_const thy) raw_constrs) thy;
   1.869 +
   1.870 +fun add_abstype proto_abs proto_rep thy =
   1.871    let
   1.872 -    val cs = map (read_bare_const thy) raw_cs;
   1.873 -  in add_datatype cs thy end;
   1.874 +    val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
   1.875 +    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
   1.876 +    fun after_qed [[cert]] = ProofContext.theory
   1.877 +      (register_datatype (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
   1.878 +      #> change_fun_spec false rep ((K o Proj)
   1.879 +        (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)));
   1.880 +  in
   1.881 +    thy
   1.882 +    |> ProofContext.init
   1.883 +    |> Proof.theorem_i NONE after_qed [[(cert_prop, [])]]
   1.884 +  end;
   1.885  
   1.886 +fun add_abstype_cmd raw_abs raw_rep thy =
   1.887 +  add_abstype (read_bare_const thy raw_abs) (read_bare_const thy raw_rep) thy;
   1.888 +
   1.889 +
   1.890 +(** infrastructure **)
   1.891  
   1.892  (* c.f. src/HOL/Tools/recfun_codegen.ML *)
   1.893  
   1.894 @@ -912,6 +1173,8 @@
   1.895    let
   1.896      val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
   1.897    in thy |> add_warning_eqn thm |> attr prefix thm end;
   1.898 +
   1.899 +
   1.900  (* setup *)
   1.901  
   1.902  val _ = Context.>> (Context.map_theory
   1.903 @@ -920,6 +1183,7 @@
   1.904      val code_attribute_parser =
   1.905        Args.del |-- Scan.succeed (mk_attribute del_eqn)
   1.906        || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
   1.907 +      || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
   1.908        || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
   1.909             (mk_attribute o code_target_attr))
   1.910        || Scan.succeed (mk_attribute add_warning_eqn);
   1.911 @@ -932,7 +1196,7 @@
   1.912  end; (*struct*)
   1.913  
   1.914  
   1.915 -(** type-safe interfaces for data dependent on executable code **)
   1.916 +(* type-safe interfaces for data dependent on executable code *)
   1.917  
   1.918  functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA =
   1.919  struct
     2.1 --- a/src/Tools/Code/code_thingol.ML	Fri Feb 19 11:06:21 2010 +0100
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Feb 19 11:06:21 2010 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4  
     2.5    datatype stmt =
     2.6        NoStmt
     2.7 -    | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
     2.8 +    | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     2.9      | Datatype of string * ((vname * sort) list * (string * itype list) list)
    2.10      | Datatypecons of string * string
    2.11      | Class of class * (vname * ((class * string) list * (string * itype) list))
    2.12 @@ -256,8 +256,8 @@
    2.13      | thyname :: _ => thyname;
    2.14    fun thyname_of_const thy c = case AxClass.class_of_param thy c
    2.15     of SOME class => thyname_of_class thy class
    2.16 -    | NONE => (case Code.get_datatype_of_constr thy c
    2.17 -       of SOME dtco => Codegen.thyname_of_type thy dtco
    2.18 +    | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
    2.19 +       of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
    2.20          | NONE => Codegen.thyname_of_const thy c);
    2.21    fun purify_base "==>" = "follows"
    2.22      | purify_base "op &" = "and"
    2.23 @@ -400,7 +400,7 @@
    2.24  type typscheme = (vname * sort) list * itype;
    2.25  datatype stmt =
    2.26      NoStmt
    2.27 -  | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
    2.28 +  | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    2.29    | Datatype of string * ((vname * sort) list * (string * itype list) list)
    2.30    | Datatypecons of string * string
    2.31    | Class of class * (vname * ((class * string) list * (string * itype) list))
    2.32 @@ -523,14 +523,18 @@
    2.33          |> pair name
    2.34    end;
    2.35  
    2.36 -fun not_wellsorted thy thm ty sort e =
    2.37 +fun translation_error thy some_thm msg sub_msg =
    2.38 +  let
    2.39 +    val err_thm = case some_thm
    2.40 +     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
    2.41 +  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
    2.42 +
    2.43 +fun not_wellsorted thy some_thm ty sort e =
    2.44    let
    2.45      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
    2.46 -    val err_thm = case thm
    2.47 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
    2.48      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
    2.49        ^ Syntax.string_of_sort_global thy sort;
    2.50 -  in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
    2.51 +  in translation_error thy some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
    2.52  
    2.53  
    2.54  (* translation *)
    2.55 @@ -558,16 +562,15 @@
    2.56        #>> (fn class => Classparam (c, class));
    2.57      fun stmt_fun cert =
    2.58        let
    2.59 -        val ((vs, ty), raw_eqns) = Code.equations_thms_cert thy cert;
    2.60 -        val eqns = map snd raw_eqns;
    2.61 +        val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
    2.62        in
    2.63          fold_map (translate_tyvar_sort thy algbr eqngr) vs
    2.64          ##>> translate_typ thy algbr eqngr ty
    2.65          ##>> fold_map (translate_eqn thy algbr eqngr) eqns
    2.66          #>> (fn info => Fun (c, info))
    2.67        end;
    2.68 -    val stmt_const = case Code.get_datatype_of_constr thy c
    2.69 -     of SOME tyco => stmt_datatypecons tyco
    2.70 +    val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
    2.71 +     of SOME (tyco, _) => stmt_datatypecons tyco
    2.72        | NONE => (case AxClass.class_of_param thy c
    2.73           of SOME class => stmt_classparam class
    2.74            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
    2.75 @@ -614,7 +617,7 @@
    2.76            o Logic.dest_equals o Thm.prop_of) thm;
    2.77        in
    2.78          ensure_const thy algbr eqngr c
    2.79 -        ##>> translate_const thy algbr eqngr (SOME thm) c_ty
    2.80 +        ##>> translate_const thy algbr eqngr NONE (SOME thm) c_ty
    2.81          #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
    2.82        end;
    2.83      val stmt_inst =
    2.84 @@ -632,54 +635,54 @@
    2.85        ensure_tyco thy algbr eqngr tyco
    2.86        ##>> fold_map (translate_typ thy algbr eqngr) tys
    2.87        #>> (fn (tyco, tys) => tyco `%% tys)
    2.88 -and translate_term thy algbr eqngr thm (Const (c, ty)) =
    2.89 -      translate_app thy algbr eqngr thm ((c, ty), [])
    2.90 -  | translate_term thy algbr eqngr thm (Free (v, _)) =
    2.91 +and translate_term thy algbr eqngr some_abs some_thm (Const (c, ty)) =
    2.92 +      translate_app thy algbr eqngr some_abs some_thm ((c, ty), [])
    2.93 +  | translate_term thy algbr eqngr some_abs some_thm (Free (v, _)) =
    2.94        pair (IVar (SOME v))
    2.95 -  | translate_term thy algbr eqngr thm (Abs (v, ty, t)) =
    2.96 +  | translate_term thy algbr eqngr some_abs some_thm (Abs (v, ty, t)) =
    2.97        let
    2.98          val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
    2.99          val v'' = if member (op =) (Term.add_free_names t' []) v'
   2.100            then SOME v' else NONE
   2.101        in
   2.102          translate_typ thy algbr eqngr ty
   2.103 -        ##>> translate_term thy algbr eqngr thm t'
   2.104 +        ##>> translate_term thy algbr eqngr some_abs some_thm t'
   2.105          #>> (fn (ty, t) => (v'', ty) `|=> t)
   2.106        end
   2.107 -  | translate_term thy algbr eqngr thm (t as _ $ _) =
   2.108 +  | translate_term thy algbr eqngr some_abs some_thm (t as _ $ _) =
   2.109        case strip_comb t
   2.110         of (Const (c, ty), ts) =>
   2.111 -            translate_app thy algbr eqngr thm ((c, ty), ts)
   2.112 +            translate_app thy algbr eqngr some_abs some_thm ((c, ty), ts)
   2.113          | (t', ts) =>
   2.114 -            translate_term thy algbr eqngr thm t'
   2.115 -            ##>> fold_map (translate_term thy algbr eqngr thm) ts
   2.116 +            translate_term thy algbr eqngr some_abs some_thm t'
   2.117 +            ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
   2.118              #>> (fn (t, ts) => t `$$ ts)
   2.119 -and translate_eqn thy algbr eqngr (thm, proper) =
   2.120 +and translate_eqn thy algbr eqngr ((some_abs, (args, rhs)), (some_thm, proper)) =
   2.121 +  fold_map (translate_term thy algbr eqngr some_abs some_thm) args
   2.122 +  ##>> translate_term thy algbr eqngr some_abs some_thm rhs
   2.123 +  #>> rpair (some_thm, proper)
   2.124 +and translate_const thy algbr eqngr some_abs some_thm (c, ty) =
   2.125    let
   2.126 -    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   2.127 -      o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
   2.128 -  in
   2.129 -    fold_map (translate_term thy algbr eqngr (SOME thm)) args
   2.130 -    ##>> translate_term thy algbr eqngr (SOME thm) rhs
   2.131 -    #>> rpair (thm, proper)
   2.132 -  end
   2.133 -and translate_const thy algbr eqngr thm (c, ty) =
   2.134 -  let
   2.135 +    val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
   2.136 +        andalso Code.is_abstr thy c
   2.137 +        then translation_error thy some_thm
   2.138 +          "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
   2.139 +      else ()
   2.140      val tys = Sign.const_typargs thy (c, ty);
   2.141      val sorts = Code_Preproc.sortargs eqngr c;
   2.142      val tys_args = (fst o Term.strip_type) ty;
   2.143    in
   2.144      ensure_const thy algbr eqngr c
   2.145      ##>> fold_map (translate_typ thy algbr eqngr) tys
   2.146 -    ##>> fold_map (translate_dicts thy algbr eqngr thm) (tys ~~ sorts)
   2.147 +    ##>> fold_map (translate_dicts thy algbr eqngr some_thm) (tys ~~ sorts)
   2.148      ##>> fold_map (translate_typ thy algbr eqngr) tys_args
   2.149      #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
   2.150    end
   2.151 -and translate_app_const thy algbr eqngr thm (c_ty, ts) =
   2.152 -  translate_const thy algbr eqngr thm c_ty
   2.153 -  ##>> fold_map (translate_term thy algbr eqngr thm) ts
   2.154 +and translate_app_const thy algbr eqngr some_abs some_thm (c_ty, ts) =
   2.155 +  translate_const thy algbr eqngr some_abs some_thm c_ty
   2.156 +  ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
   2.157    #>> (fn (t, ts) => t `$$ ts)
   2.158 -and translate_case thy algbr eqngr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   2.159 +and translate_case thy algbr eqngr some_abs some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   2.160    let
   2.161      fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
   2.162      val tys = arg_types num_args (snd c_ty);
   2.163 @@ -723,14 +726,14 @@
   2.164                (constrs ~~ ts_clause);
   2.165        in ((t, ty), clauses) end;
   2.166    in
   2.167 -    translate_const thy algbr eqngr thm c_ty
   2.168 -    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs
   2.169 +    translate_const thy algbr eqngr some_abs some_thm c_ty
   2.170 +    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr some_abs some_thm constr #>> rpair n) constrs
   2.171      ##>> translate_typ thy algbr eqngr ty
   2.172 -    ##>> fold_map (translate_term thy algbr eqngr thm) ts
   2.173 +    ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
   2.174      #-> (fn (((t, constrs), ty), ts) =>
   2.175        `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
   2.176    end
   2.177 -and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   2.178 +and translate_app_case thy algbr eqngr some_abs some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   2.179    if length ts < num_args then
   2.180      let
   2.181        val k = length ts;
   2.182 @@ -739,23 +742,23 @@
   2.183        val vs = Name.names ctxt "a" tys;
   2.184      in
   2.185        fold_map (translate_typ thy algbr eqngr) tys
   2.186 -      ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs)
   2.187 +      ##>> translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts @ map Free vs)
   2.188        #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
   2.189      end
   2.190    else if length ts > num_args then
   2.191 -    translate_case thy algbr eqngr thm case_scheme ((c, ty), take num_args ts)
   2.192 -    ##>> fold_map (translate_term thy algbr eqngr thm) (drop num_args ts)
   2.193 +    translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), take num_args ts)
   2.194 +    ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) (drop num_args ts)
   2.195      #>> (fn (t, ts) => t `$$ ts)
   2.196    else
   2.197 -    translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
   2.198 -and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) =
   2.199 +    translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts)
   2.200 +and translate_app thy algbr eqngr some_abs some_thm (c_ty_ts as ((c, _), _)) =
   2.201    case Code.get_case_scheme thy c
   2.202 -   of SOME case_scheme => translate_app_case thy algbr eqngr thm case_scheme c_ty_ts
   2.203 -    | NONE => translate_app_const thy algbr eqngr thm c_ty_ts
   2.204 +   of SOME case_scheme => translate_app_case thy algbr eqngr some_abs some_thm case_scheme c_ty_ts
   2.205 +    | NONE => translate_app_const thy algbr eqngr some_abs some_thm c_ty_ts
   2.206  and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
   2.207    fold_map (ensure_class thy algbr eqngr) (proj_sort sort)
   2.208    #>> (fn sort => (unprefix "'" v, sort))
   2.209 -and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr thm (ty, sort) =
   2.210 +and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr some_thm (ty, sort) =
   2.211    let
   2.212      datatype typarg =
   2.213          Global of (class * string) * typarg list list
   2.214 @@ -773,7 +776,7 @@
   2.215      val typargs = Sorts.of_sort_derivation algebra
   2.216        {class_relation = class_relation, type_constructor = type_constructor,
   2.217         type_variable = type_variable} (ty, proj_sort sort)
   2.218 -      handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
   2.219 +      handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
   2.220      fun mk_dict (Global (inst, yss)) =
   2.221            ensure_inst thy algbr eqngr inst
   2.222            ##>> (fold_map o fold_map) mk_dict yss
   2.223 @@ -824,9 +827,9 @@
   2.224      val stmt_value =
   2.225        fold_map (translate_tyvar_sort thy algbr eqngr) vs
   2.226        ##>> translate_typ thy algbr eqngr ty
   2.227 -      ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
   2.228 +      ##>> translate_term thy algbr eqngr NONE NONE (Code.subst_signatures thy t)
   2.229        #>> (fn ((vs, ty), t) => Fun
   2.230 -        (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
   2.231 +        (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
   2.232      fun term_value (dep, (naming, program1)) =
   2.233        let
   2.234          val Fun (_, (vs_ty, [(([], t), _)])) =