user interface for abstract datatypes is an attribute, not a command
authorhaftmann
Sun Apr 11 16:51:07 2010 +0200 (2010-04-11)
changeset 361127fa17a225852
parent 36111 5844017e31f8
child 36113 853c777f2907
user interface for abstract datatypes is an attribute, not a command
src/HOL/Library/Dlist.thy
src/HOL/Rat.thy
src/Pure/Isar/code.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:06 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:07 2010 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    show "[] \<in> ?dlist" by simp
     1.5  qed
     1.6  
     1.7 +
     1.8  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
     1.9  
    1.10  definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
    1.11 @@ -60,7 +61,7 @@
    1.12    "list_of_dlist (Dlist xs) = remdups xs"
    1.13    by (simp add: Dlist_def Abs_dlist_inverse)
    1.14  
    1.15 -lemma Dlist_list_of_dlist [simp]:
    1.16 +lemma Dlist_list_of_dlist [simp, code abstype]:
    1.17    "Dlist (list_of_dlist dxs) = dxs"
    1.18    by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
    1.19  
    1.20 @@ -100,9 +101,6 @@
    1.21  
    1.22  section {* Executable version obeying invariant *}
    1.23  
    1.24 -code_abstype Dlist list_of_dlist
    1.25 -  by simp
    1.26 -
    1.27  lemma list_of_dlist_empty [simp, code abstract]:
    1.28    "list_of_dlist empty = []"
    1.29    by (simp add: empty_def)
     2.1 --- a/src/HOL/Rat.thy	Sun Apr 11 16:51:06 2010 +0200
     2.2 +++ b/src/HOL/Rat.thy	Sun Apr 11 16:51:07 2010 +0200
     2.3 @@ -1019,11 +1019,9 @@
     2.4  definition Frct :: "int \<times> int \<Rightarrow> rat" where
     2.5    [simp]: "Frct p = Fract (fst p) (snd p)"
     2.6  
     2.7 -code_abstype Frct quotient_of
     2.8 -proof (rule eq_reflection)
     2.9 -  fix r :: rat
    2.10 -  show "Frct (quotient_of r) = r" by (cases r) (auto intro: quotient_of_eq)
    2.11 -qed
    2.12 +lemma [code abstype]:
    2.13 +  "Frct (quotient_of q) = q"
    2.14 +  by (cases q) (auto intro: quotient_of_eq)
    2.15  
    2.16  lemma Frct_code_post [code_post]:
    2.17    "Frct (0, k) = 0"
     3.1 --- a/src/Pure/Isar/code.ML	Sun Apr 11 16:51:06 2010 +0200
     3.2 +++ b/src/Pure/Isar/code.ML	Sun Apr 11 16:51:07 2010 +0200
     3.3 @@ -22,8 +22,6 @@
     3.4    (*constructor sets*)
     3.5    val constrset_of_consts: theory -> (string * typ) list
     3.6      -> string * ((string * sort) list * (string * typ list) list)
     3.7 -  val abstype_cert: theory -> string * typ -> string
     3.8 -    -> string * ((string * sort) list * ((string * typ) * (string * term)))
     3.9  
    3.10    (*code equations and certificates*)
    3.11    val mk_eqn: theory -> thm * bool -> thm * bool
    3.12 @@ -52,8 +50,7 @@
    3.13    val datatype_interpretation:
    3.14      (string * ((string * sort) list * (string * typ list) list)
    3.15        -> theory -> theory) -> theory -> theory
    3.16 -  val add_abstype: string * typ -> string * typ -> theory -> Proof.state
    3.17 -  val add_abstype_cmd: string -> string -> theory -> Proof.state
    3.18 +  val add_abstype: thm -> theory -> theory
    3.19    val abstype_interpretation:
    3.20      (string * ((string * sort) list * ((string * typ) * (string * thm)))
    3.21        -> theory -> theory) -> theory -> theory
    3.22 @@ -380,6 +377,7 @@
    3.23          val tfrees = Term.add_tfreesT ty [];
    3.24          val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
    3.25            handle TYPE _ => no_constr thy "bad type" c_ty
    3.26 +        val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
    3.27          val _ = if has_duplicates (eq_fst (op =)) vs
    3.28            then no_constr thy "duplicate type variables in datatype" c_ty else ();
    3.29          val _ = if length tfrees <> length vs
    3.30 @@ -411,22 +409,6 @@
    3.31      val cs''' = map (inst vs) cs'';
    3.32    in (tyco, (vs, rev cs''')) end;
    3.33  
    3.34 -fun abstype_cert thy abs_ty rep =
    3.35 -  let
    3.36 -    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
    3.37 -      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (fst abs_ty, rep);
    3.38 -    val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy abs_ty;
    3.39 -    val (ty, ty_abs) = case ty'
    3.40 -     of Type ("fun", [ty, ty_abs]) => (ty, ty_abs)
    3.41 -      | _ => error ("Not a datatype abstractor:\n" ^ string_of_const thy abs
    3.42 -          ^ " :: " ^ string_of_typ thy ty');
    3.43 -    val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle TYPE _ =>
    3.44 -      error ("Not a projection:\n" ^ string_of_const thy rep);
    3.45 -    val param = Free ("x", ty_abs);
    3.46 -    val cert = Logic.all param (Logic.mk_equals
    3.47 -      (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty) $ param), param));
    3.48 -  in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;    
    3.49 -
    3.50  fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
    3.51   of (_, entry) :: _ => SOME entry
    3.52    | _ => NONE;
    3.53 @@ -657,6 +639,29 @@
    3.54  fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
    3.55  
    3.56  
    3.57 +(* abstype certificates *)
    3.58 +
    3.59 +fun check_abstype_cert thy proto_thm =
    3.60 +  let
    3.61 +    val thm = meta_rewrite thy proto_thm;
    3.62 +    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
    3.63 +    val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
    3.64 +      handle TERM _ => bad "Not an equation"
    3.65 +           | THM _ => bad "Not a proper equation";
    3.66 +    val ((abs, raw_ty), ((rep, _), param)) = (apsnd (apfst dest_Const o dest_comb)
    3.67 +        o apfst dest_Const o dest_comb) lhs
    3.68 +      handle TERM _ => bad "Not an abstype certificate";
    3.69 +    val var = (fst o dest_Var) param
    3.70 +      handle TERM _ => bad "Not an abstype certificate";
    3.71 +    val _ = if param = rhs then () else bad "Not an abstype certificate";
    3.72 +    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
    3.73 +      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
    3.74 +    val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
    3.75 +    val ty = domain_type ty';
    3.76 +    val ty_abs = range_type ty';
    3.77 +  in (tyco, (vs ~~ sorts, ((abs, ty), (rep, thm)))) end;
    3.78 +
    3.79 +
    3.80  (* code equation certificates *)
    3.81  
    3.82  fun build_head thy (c, ty) =
    3.83 @@ -1152,25 +1157,19 @@
    3.84  fun abstype_interpretation f = Abstype_Interpretation.interpretation
    3.85    (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
    3.86  
    3.87 -fun add_abstype proto_abs proto_rep thy =
    3.88 +fun add_abstype proto_thm thy =
    3.89    let
    3.90 -    val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
    3.91 -    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
    3.92 -    fun after_qed [[cert]] = ProofContext.theory
    3.93 -      (del_eqns abs
    3.94 -      #> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
    3.95 -      #> change_fun_spec false rep ((K o Proj)
    3.96 -        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
    3.97 -      #> Abstype_Interpretation.data (tyco, serial ()));
    3.98 +    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
    3.99 +      check_abstype_cert thy proto_thm;
   3.100    in
   3.101      thy
   3.102 -    |> ProofContext.init
   3.103 -    |> Proof.theorem_i NONE after_qed [[(cert_prop, [])]]
   3.104 +    |> del_eqns abs
   3.105 +    |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
   3.106 +    |> change_fun_spec false rep ((K o Proj)
   3.107 +        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
   3.108 +    |> Abstype_Interpretation.data (tyco, serial ())
   3.109    end;
   3.110  
   3.111 -fun add_abstype_cmd raw_abs raw_rep thy =
   3.112 -  add_abstype (read_bare_const thy raw_abs) (read_bare_const thy raw_rep) thy;
   3.113 -
   3.114  
   3.115  (** infrastructure **)
   3.116  
   3.117 @@ -1200,6 +1199,7 @@
   3.118      val code_attribute_parser =
   3.119        Args.del |-- Scan.succeed (mk_attribute del_eqn)
   3.120        || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
   3.121 +      || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
   3.122        || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
   3.123        || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
   3.124             (mk_attribute o code_target_attr))
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:06 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:07 2010 +0200
     4.3 @@ -480,11 +480,6 @@
     4.4    OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
     4.5      (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
     4.6  
     4.7 -val _ =
     4.8 -  OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
     4.9 -    (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
    4.10 -      o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
    4.11 -
    4.12  
    4.13  
    4.14  (** proof commands **)