src/HOL/Tools/typecopy_package.ML
changeset 25506 c9bea6426932
parent 25489 5b0625f6e324
child 25534 d0b74fdd6067
equal deleted inserted replaced
25505:4d531475129a 25506:c9bea6426932
    16     proj_def: thm
    16     proj_def: thm
    17   }
    17   }
    18   val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
    18   val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
    19     -> theory -> (string * info) * theory
    19     -> theory -> (string * info) * theory
    20   val get_typecopies: theory -> string list
    20   val get_typecopies: theory -> string list
    21   val get_typecopy_info: theory -> string -> info option
    21   val get_info: theory -> string -> info option
    22   val interpretation: (string -> theory -> theory) -> theory -> theory
    22   val interpretation: (string -> theory -> theory) -> theory -> theory
    23   val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
       
    24   val get_eq: theory -> string -> thm
    23   val get_eq: theory -> string -> thm
    25   val print_typecopies: theory -> unit
    24   val print_typecopies: theory -> unit
    26   val setup: theory -> theory
    25   val setup: theory -> theory
    27 end;
    26 end;
    28 
    27 
    63       (Pretty.writeln o Pretty.block o Pretty.fbreaks)
    62       (Pretty.writeln o Pretty.block o Pretty.fbreaks)
    64         (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
    63         (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
    65     end;
    64     end;
    66 
    65 
    67 val get_typecopies = Symtab.keys o TypecopyData.get;
    66 val get_typecopies = Symtab.keys o TypecopyData.get;
    68 val get_typecopy_info = Symtab.lookup o TypecopyData.get;
    67 val get_info = Symtab.lookup o TypecopyData.get;
    69 
    68 
    70 
    69 
    71 (* interpretation of type copies *)
    70 (* interpretation of type copies *)
    72 
    71 
    73 structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
    72 structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
   121 end;
   120 end;
   122 
   121 
   123 
   122 
   124 (* code generator setup *)
   123 (* code generator setup *)
   125 
   124 
   126 fun get_spec thy tyco =
   125 fun get_eq thy = #inject o the o get_info thy;
   127   let
       
   128     val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
       
   129   in (vs, [(constr, [typ])]) end;
       
   130 
       
   131 fun get_eq thy tyco =
       
   132   (#inject o the o get_typecopy_info thy) tyco;
       
   133 
   126 
   134 fun add_typecopy_spec tyco thy =
   127 fun add_typecopy_spec tyco thy =
   135   let
   128   let
   136     val c = (#constr o the o get_typecopy_info thy) tyco;
   129     val SOME { constr, proj_def, inject, ... } = get_info thy tyco;
   137     val ty = Logic.unvarifyT (Sign.the_const_type thy c);
   130     val ty = Logic.unvarifyT (Sign.the_const_type thy constr);
   138   in
   131   in
   139     thy |> Code.add_datatype [(c, ty)]
   132     thy
       
   133     |> Code.add_datatype [(constr, ty)]
       
   134     |> Code.add_func proj_def
   140   end;
   135   end;
   141 
       
   142 fun add_project tyco thy = thy |> Code.add_default_func
       
   143   ((#proj_def o the o get_typecopy_info thy) tyco);
       
   144 
   136 
   145 val setup =
   137 val setup =
   146   TypecopyInterpretation.init
   138   TypecopyInterpretation.init
   147   #> interpretation add_typecopy_spec
   139   #> interpretation add_typecopy_spec
   148   #> interpretation add_project
       
   149 
   140 
   150 end;
   141 end;