proper distinction of code datatypes and abstypes
authorhaftmann
Mon Feb 22 11:10:20 2010 +0100 (2010-02-22)
changeset 352994f4d5bf4ea08
parent 35279 4f6760122b2a
child 35300 ca05ceeeb9ab
proper distinction of code datatypes and abstypes
src/HOL/Code_Evaluation.thy
src/HOL/Typerep.thy
src/Pure/Isar/code.ML
src/Tools/Code/code_eval.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Feb 22 10:28:49 2010 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Feb 22 11:10:20 2010 +0100
     1.3 @@ -76,7 +76,8 @@
     1.4          andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
     1.5      in if need_inst then add_term_of tyco raw_vs thy else thy end;
     1.6  in
     1.7 -  Code.type_interpretation ensure_term_of
     1.8 +  Code.datatype_interpretation ensure_term_of
     1.9 +  #> Code.abstype_interpretation ensure_term_of
    1.10  end
    1.11  *}
    1.12  
    1.13 @@ -114,7 +115,7 @@
    1.14        val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    1.15      in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    1.16  in
    1.17 -  Code.type_interpretation ensure_term_of_code
    1.18 +  Code.datatype_interpretation ensure_term_of_code
    1.19  end
    1.20  *}
    1.21  
     2.1 --- a/src/HOL/Typerep.thy	Mon Feb 22 10:28:49 2010 +0100
     2.2 +++ b/src/HOL/Typerep.thy	Mon Feb 22 11:10:20 2010 +0100
     2.3 @@ -70,7 +70,8 @@
     2.4  
     2.5  add_typerep @{type_name fun}
     2.6  #> Typedef.interpretation ensure_typerep
     2.7 -#> Code.type_interpretation (ensure_typerep o fst)
     2.8 +#> Code.datatype_interpretation (ensure_typerep o fst)
     2.9 +#> Code.abstype_interpretation (ensure_typerep o fst)
    2.10  
    2.11  end
    2.12  *}
     3.1 --- a/src/Pure/Isar/code.ML	Mon Feb 22 10:28:49 2010 +0100
     3.2 +++ b/src/Pure/Isar/code.ML	Mon Feb 22 11:10:20 2010 +0100
     3.3 @@ -49,10 +49,13 @@
     3.4    val add_signature_cmd: string * string -> theory -> theory
     3.5    val add_datatype: (string * typ) list -> theory -> theory
     3.6    val add_datatype_cmd: string list -> theory -> theory
     3.7 +  val datatype_interpretation:
     3.8 +    (string * ((string * sort) list * (string * typ list) list)
     3.9 +      -> theory -> theory) -> theory -> theory
    3.10    val add_abstype: string * typ -> string * typ -> theory -> Proof.state
    3.11    val add_abstype_cmd: string -> string -> theory -> Proof.state
    3.12 -  val type_interpretation:
    3.13 -    (string * ((string * sort) list * (string * typ list) list)
    3.14 +  val abstype_interpretation:
    3.15 +    (string * ((string * sort) list * ((string * typ) * (string * thm)))
    3.16        -> theory -> theory) -> theory -> theory
    3.17    val add_eqn: thm -> theory -> theory
    3.18    val add_nbe_eqn: thm -> theory -> theory
    3.19 @@ -63,8 +66,8 @@
    3.20    val del_eqns: string -> theory -> theory
    3.21    val add_case: thm -> theory -> theory
    3.22    val add_undefined: string -> theory -> theory
    3.23 -  val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    3.24 -  val get_datatype_of_constr_or_abstr: theory -> string -> (string * bool) option
    3.25 +  val get_type: theory -> string -> ((string * sort) list * (string * typ list) list)
    3.26 +  val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
    3.27    val is_constr: theory -> string -> bool
    3.28    val is_abstr: theory -> string -> bool
    3.29    val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
    3.30 @@ -163,21 +166,21 @@
    3.31    signatures: int Symtab.table * typ Symtab.table,
    3.32    functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
    3.33      (*with explicit history*),
    3.34 -  datatypes: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
    3.35 +  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
    3.36      (*with explicit history*),
    3.37    cases: (int * (int * string list)) Symtab.table * unit Symtab.table
    3.38  };
    3.39  
    3.40 -fun make_spec (history_concluded, ((signatures, functions), (datatypes, cases))) =
    3.41 +fun make_spec (history_concluded, ((signatures, functions), (types, cases))) =
    3.42    Spec { history_concluded = history_concluded,
    3.43 -    signatures = signatures, functions = functions, datatypes = datatypes, cases = cases };
    3.44 +    signatures = signatures, functions = functions, types = types, cases = cases };
    3.45  fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
    3.46 -  functions = functions, datatypes = datatypes, cases = cases }) =
    3.47 -  make_spec (f (history_concluded, ((signatures, functions), (datatypes, cases))));
    3.48 +  functions = functions, types = types, cases = cases }) =
    3.49 +  make_spec (f (history_concluded, ((signatures, functions), (types, cases))));
    3.50  fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), functions = functions1,
    3.51 -    datatypes = datatypes1, cases = (cases1, undefs1) },
    3.52 +    types = types1, cases = (cases1, undefs1) },
    3.53    Spec { history_concluded = _, signatures = (tycos2, sigs2), functions = functions2,
    3.54 -    datatypes = datatypes2, cases = (cases2, undefs2) }) =
    3.55 +    types = types2, cases = (cases2, undefs2) }) =
    3.56    let
    3.57      val signatures = (Symtab.merge (op =) (tycos1, tycos2),
    3.58        Symtab.merge typ_equiv (sigs1, sigs2));
    3.59 @@ -190,15 +193,15 @@
    3.60            then raw_history else filtered_history;
    3.61        in ((false, (snd o hd) history), history) end;
    3.62      val functions = Symtab.join (K merge_functions) (functions1, functions2);
    3.63 -    val datatypes = Symtab.join (K (AList.merge (op =) (K true))) (datatypes1, datatypes2);
    3.64 +    val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2);
    3.65      val cases = (Symtab.merge (K true) (cases1, cases2),
    3.66        Symtab.merge (K true) (undefs1, undefs2));
    3.67 -  in make_spec (false, ((signatures, functions), (datatypes, cases))) end;
    3.68 +  in make_spec (false, ((signatures, functions), (types, cases))) end;
    3.69  
    3.70  fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
    3.71  fun the_signatures (Spec { signatures, ... }) = signatures;
    3.72  fun the_functions (Spec { functions, ... }) = functions;
    3.73 -fun the_datatypes (Spec { datatypes, ... }) = datatypes;
    3.74 +fun the_types (Spec { types, ... }) = types;
    3.75  fun the_cases (Spec { cases, ... }) = cases;
    3.76  val map_history_concluded = map_spec o apfst;
    3.77  val map_signatures = map_spec o apsnd o apfst o apfst;
    3.78 @@ -423,11 +426,11 @@
    3.79        $ Free ("x", ty_abs)), Free ("x", ty_abs));
    3.80    in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;    
    3.81  
    3.82 -fun get_datatype_entry thy tyco = case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
    3.83 +fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
    3.84   of (_, entry) :: _ => SOME entry
    3.85    | _ => NONE;
    3.86  
    3.87 -fun get_datatype_spec thy tyco = case get_datatype_entry thy tyco
    3.88 +fun get_type_spec thy tyco = case get_type_entry thy tyco
    3.89   of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
    3.90    | NONE => arity_number thy tyco
    3.91        |> Name.invents Name.context Name.aT
    3.92 @@ -435,23 +438,23 @@
    3.93        |> rpair []
    3.94        |> rpair false;
    3.95  
    3.96 -fun get_abstype_spec thy tyco = case get_datatype_entry thy tyco
    3.97 +fun get_abstype_spec thy tyco = case get_type_entry thy tyco
    3.98   of SOME (vs, Abstractor spec) => (vs, spec)
    3.99    | NONE => error ("Not an abstract type: " ^ tyco);
   3.100   
   3.101 -fun get_datatype thy = fst o get_datatype_spec thy;
   3.102 +fun get_type thy = fst o get_type_spec thy;
   3.103  
   3.104 -fun get_datatype_of_constr_or_abstr thy c =
   3.105 +fun get_type_of_constr_or_abstr thy c =
   3.106    case (snd o strip_type o const_typ thy) c
   3.107 -   of Type (tyco, _) => let val ((vs, cos), abstract) = get_datatype_spec thy tyco
   3.108 +   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco
   3.109          in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
   3.110      | _ => NONE;
   3.111  
   3.112 -fun is_constr thy c = case get_datatype_of_constr_or_abstr thy c
   3.113 +fun is_constr thy c = case get_type_of_constr_or_abstr thy c
   3.114   of SOME (_, false) => true
   3.115     | _ => false;
   3.116  
   3.117 -fun is_abstr thy c = case get_datatype_of_constr_or_abstr thy c
   3.118 +fun is_abstr thy c = case get_type_of_constr_or_abstr thy c
   3.119   of SOME (_, true) => true
   3.120     | _ => false;
   3.121  
   3.122 @@ -952,7 +955,7 @@
   3.123        |> Symtab.dest
   3.124        |> (map o apsnd) (snd o fst)
   3.125        |> sort (string_ord o pairself fst);
   3.126 -    val datatypes = the_datatypes exec
   3.127 +    val datatypes = the_types exec
   3.128        |> Symtab.dest
   3.129        |> map (fn (tyco, (_, (vs, spec)) :: _) =>
   3.130            ((tyco, vs), constructors_of spec))
   3.131 @@ -1088,15 +1091,12 @@
   3.132    (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
   3.133  
   3.134  
   3.135 -(* datatypes *)
   3.136 +(* types *)
   3.137  
   3.138 -structure Type_Interpretation =
   3.139 -  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   3.140 -
   3.141 -fun register_datatype (tyco, vs_spec) thy =
   3.142 +fun register_type (tyco, vs_spec) thy =
   3.143    let
   3.144      val (old_constrs, some_old_proj) =
   3.145 -      case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
   3.146 +      case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
   3.147         of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
   3.148          | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
   3.149          | [] => ([], NONE)
   3.150 @@ -1116,13 +1116,15 @@
   3.151      |> map_exec_purge
   3.152          ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
   3.153          #> (map_cases o apfst) drop_outdated_cases)
   3.154 -    |> Type_Interpretation.data (tyco, serial ())
   3.155    end;
   3.156  
   3.157 -fun type_interpretation f = Type_Interpretation.interpretation
   3.158 -  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   3.159 +fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
   3.160  
   3.161 -fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
   3.162 +structure Datatype_Interpretation =
   3.163 +  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   3.164 +
   3.165 +fun datatype_interpretation f = Datatype_Interpretation.interpretation
   3.166 +  (fn (tyco, _) => fn thy => f (tyco, get_type thy tyco) thy);
   3.167  
   3.168  fun add_datatype proto_constrs thy =
   3.169    let
   3.170 @@ -1131,20 +1133,28 @@
   3.171    in
   3.172      thy
   3.173      |> fold (del_eqns o fst) constrs
   3.174 -    |> register_datatype (tyco, (vs, Constructors cos))
   3.175 +    |> register_type (tyco, (vs, Constructors cos))
   3.176 +    |> Datatype_Interpretation.data (tyco, serial ())
   3.177    end;
   3.178  
   3.179  fun add_datatype_cmd raw_constrs thy =
   3.180    add_datatype (map (read_bare_const thy) raw_constrs) thy;
   3.181  
   3.182 +structure Abstype_Interpretation =
   3.183 +  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   3.184 +
   3.185 +fun abstype_interpretation f = Abstype_Interpretation.interpretation
   3.186 +  (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
   3.187 +
   3.188  fun add_abstype proto_abs proto_rep thy =
   3.189    let
   3.190      val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
   3.191      val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
   3.192      fun after_qed [[cert]] = ProofContext.theory
   3.193 -      (register_datatype (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
   3.194 +      (register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
   3.195        #> change_fun_spec false rep ((K o Proj)
   3.196 -        (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)));
   3.197 +        (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco))
   3.198 +      #> Abstype_Interpretation.data (tyco, serial ()));
   3.199    in
   3.200      thy
   3.201      |> ProofContext.init
   3.202 @@ -1188,7 +1198,7 @@
   3.203             (mk_attribute o code_target_attr))
   3.204        || Scan.succeed (mk_attribute add_warning_eqn);
   3.205    in
   3.206 -    Type_Interpretation.init
   3.207 +    Datatype_Interpretation.init
   3.208      #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
   3.209          "declare theorems for code generation"
   3.210    end));
     4.1 --- a/src/Tools/Code/code_eval.ML	Mon Feb 22 10:28:49 2010 +0100
     4.2 +++ b/src/Tools/Code/code_eval.ML	Mon Feb 22 11:10:20 2010 +0100
     4.3 @@ -130,7 +130,7 @@
     4.4      val thy = ProofContext.theory_of background;
     4.5      val tyco = Sign.intern_type thy raw_tyco;
     4.6      val constrs = map (Code.check_const thy) raw_constrs;
     4.7 -    val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
     4.8 +    val constrs' = (map fst o snd o Code.get_type thy) tyco;
     4.9      val _ = if eq_set (op =) (constrs, constrs') then ()
    4.10        else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
    4.11      val is_first = is_first_occ background;
     5.1 --- a/src/Tools/Code/code_thingol.ML	Mon Feb 22 10:28:49 2010 +0100
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Feb 22 11:10:20 2010 +0100
     5.3 @@ -256,7 +256,7 @@
     5.4      | thyname :: _ => thyname;
     5.5    fun thyname_of_const thy c = case AxClass.class_of_param thy c
     5.6     of SOME class => thyname_of_class thy class
     5.7 -    | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
     5.8 +    | NONE => (case Code.get_type_of_constr_or_abstr thy c
     5.9         of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
    5.10          | NONE => Codegen.thyname_of_const thy c);
    5.11    fun purify_base "==>" = "follows"
    5.12 @@ -543,7 +543,7 @@
    5.13    let
    5.14      val stmt_datatype =
    5.15        let
    5.16 -        val (vs, cos) = Code.get_datatype thy tyco;
    5.17 +        val (vs, cos) = Code.get_type thy tyco;
    5.18        in
    5.19          fold_map (translate_tyvar_sort thy algbr eqngr) vs
    5.20          ##>> fold_map (fn (c, tys) =>
    5.21 @@ -569,7 +569,7 @@
    5.22          ##>> fold_map (translate_eqn thy algbr eqngr) eqns
    5.23          #>> (fn info => Fun (c, info))
    5.24        end;
    5.25 -    val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
    5.26 +    val stmt_const = case Code.get_type_of_constr_or_abstr thy c
    5.27       of SOME (tyco, _) => stmt_datatypecons tyco
    5.28        | NONE => (case AxClass.class_of_param thy c
    5.29           of SOME class => stmt_classparam class