# HG changeset patch # User wenzelm # Date 878588108 -3600 # Node ID 2270829d23645a7fb5e8b37e847aae574045c7f3 # Parent 01fa6e7e7196e26b19ff332c4bdc5e2f2954fe05 adapted to new datatypes thy info; diff -r 01fa6e7e7196 -r 2270829d2364 TFL/thry.sml --- a/TFL/thry.sml Mon Nov 03 21:13:24 1997 +0100 +++ b/TFL/thry.sml Mon Nov 03 21:15:08 1997 +0100 @@ -53,15 +53,17 @@ end; (*--------------------------------------------------------------------------- - * Hacks to make interactive mode work. Referring to "datatypes" directly - * is temporary, I hope! + * Hacks to make interactive mode work. *---------------------------------------------------------------------------*) + +fun get_info thy ty = Symtab.lookup (ThyData.get_datatypes thy, ty); + val match_info = fn thy => fn "*" => Some({case_const = #case_const (#2 prod_record), constructors = #constructors (#2 prod_record)}) | "nat" => Some({case_const = #case_const (#2 nat_record), constructors = #constructors (#2 nat_record)}) - | ty => case assoc(!datatypes,ty) + | ty => case get_info thy ty of None => None | Some{case_const,constructors, ...} => Some{case_const=case_const, constructors=constructors} @@ -71,14 +73,15 @@ constructors = #constructors (#2 prod_record)}) | "nat" => Some({nchotomy = #nchotomy (#2 nat_record), constructors = #constructors (#2 nat_record)}) - | ty => case assoc(!datatypes,ty) + | ty => case get_info thy ty of None => None | Some{nchotomy,constructors, ...} => Some{nchotomy=nchotomy, constructors=constructors} val extract_info = fn thy => - let val case_congs = map (#case_cong o #2) (!datatypes) - val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes)) + let val infos = map snd (Symtab.dest (ThyData.get_datatypes thy)); + val case_congs = map #case_cong infos; + val case_rewrites = flat (map #case_rewrites infos); in {case_congs = #case_cong (#2 prod_record):: #case_cong (#2 nat_record)::case_congs, case_rewrites = #case_rewrites(#2 prod_record)@ diff -r 01fa6e7e7196 -r 2270829d2364 src/HOL/datatype.ML --- a/src/HOL/datatype.ML Mon Nov 03 21:13:24 1997 +0100 +++ b/src/HOL/datatype.ML Mon Nov 03 21:15:08 1997 +0100 @@ -3,41 +3,36 @@ Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker, Konrad Slind Copyright 1995 TU Muenchen - *) -(** Information about datatypes **) + +(** theory information about datatypes **) -(* Retrieve information for a specific datatype *) -fun datatype_info thy tname = - case get_thydata (Sign.name_of (sign_of thy)) "datatypes" of - None => None - | Some (DT_DATA ds) => assoc (ds, tname); +fun datatype_info_sg sg name = + (case Symtab.lookup (ThyData.get_datatypes_sg sg, name) of + Some info => info + | None => error ("Unknown datatype " ^ quote name)); -fun match_info thy tname = - case datatype_info thy tname of - Some {case_const, constructors, ...} => - {case_const=case_const, constructors=constructors} - | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory."); +val datatype_info = datatype_info_sg o sign_of; -fun induct_info thy tname = - case datatype_info thy tname of - Some {constructors, nchotomy, ...} => - {constructors=constructors, nchotomy=nchotomy} - | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory."); - +fun match_info thy name = + let val {case_const, constructors, ...} = datatype_info thy name in + {case_const = case_const, constructors = constructors} + end; -(* Retrieve information for all datatypes defined in a theory and its - ancestors *) +fun induct_info thy name = + let val {constructors, nchotomy, ...} = datatype_info thy name in + {constructors = constructors, nchotomy = nchotomy} + end; + +(*retrieve information for all datatypes defined in a theory*) fun extract_info thy = - let val (congs, rewrites) = - case get_thydata (Sign.name_of (sign_of thy)) "datatypes" of - None => ([], []) - | Some (DT_DATA ds) => - let val info = map snd ds - in (map #case_cong info, flat (map #case_rewrites info)) end; + let + val infos = map snd (Symtab.dest (ThyData.get_datatypes thy)); + val (congs, rewrites) = (map #case_cong infos, flat (map #case_rewrites infos)); in {case_congs = congs, case_rewrites = rewrites} end; + local fun find_tname var Bi = @@ -49,14 +44,6 @@ | _ => error("Cannot induct on type of " ^ quote var) end; -fun get_dt_info sign tn = - case get_thydata (Sign.name_of sign) "datatypes" of - None => error ("No such datatype: " ^ quote tn) - | Some (DT_DATA ds) => - case assoc (ds, tn) of - Some info => info - | None => error ("Not a datatype: " ^ quote tn) - fun infer_tname state sign i aterm = let val (_, _, Bi, _) = dest_state (state, i) val params = Logic.strip_params Bi (*params of subgoal i*) @@ -78,14 +65,14 @@ let val (_, _, Bi, _) = dest_state (state, i) val sign = #sign(rep_thm state) val tn = find_tname var Bi - val ind_tac = #induct_tac(get_dt_info sign tn) + val ind_tac = #induct_tac(datatype_info_sg sign tn) in ind_tac var i end; (* generic exhaustion tactic for datatypes *) fun exhaust_tac aterm i state = state |> let val sign = #sign(rep_thm state) val tn = infer_tname state sign i aterm - val exh_tac = #exhaust_tac(get_dt_info sign tn) + val exh_tac = #exhaust_tac(datatype_info_sg sign tn) in exh_tac aterm i end; end; @@ -640,10 +627,10 @@ val case_thms : Sign.sg -> thm list -> (string -> int -> tactic) -> {nchotomy:thm, case_cong:thm} - val build_record : (theory * (string * string list) - * (string -> int -> tactic)) - -> (string * dtype_info) - + val build_record: theory * (string * string list) * (string -> int -> tactic) + -> string * datatype_info + val add_record: string * string list * (string -> int -> tactic) -> theory -> theory + val add_datatype_info: string * datatype_info -> theory -> theory end; @@ -1004,6 +991,15 @@ end; +fun add_datatype_info info thy = thy |> + ThyData.put_datatypes (Symtab.update (info, ThyData.get_datatypes thy)); + +fun add_record (ty, cl, itac) thy = thy |> + add_datatype_info (build_record (thy, (ty, cl), itac)); + + + + (*--------------------------------------------------------------------------- * Test *