export_helper.ml revision 4d4ee5ef6601170c9d419da9fe8742c506507d11
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersignature ExportHelper =
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_consts : theory -> (string * (typ * term option)) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_axioms : theory -> (string * term) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_theorems : theory -> (string * term) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_datatypes : theory -> (string * (Datatype.info option)) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_generated_theorems : theory -> (string * (Datatype.info option)) list -> string list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val filter : string list -> (string * 'a) list -> (string * 'a) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstructure ExportHelper : ExportHelper =
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun mergesort _ [] = []
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | mergesort _ [x] = [x]
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | mergesort cmp_data xs = let val (ys,zs) = List.foldl (fn(i, (ys,zs)) => (zs, i::ys)) ([],[]) xs
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun merge (xs,[]) = xs
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | merge ([],xs) = xs
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | merge (x::xr,y::yr) = if (cmp_data x) <= (cmp_data y)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder then x::merge(xr,y::yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder else y::merge(x::xr,yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in merge(mergesort cmp_data ys, mergesort cmp_data zs) end
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (* make a sorted list unique*)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun unique [] = []
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | unique [x] = [x]
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | unique (x1::x2::xr) = if x1 = x2
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder then unique (x2::xr)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder else x1::(unique (x2::xr))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (* remove xs from ys - both lists need to be sorted asc *)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove' _ _ ([],ys) = ys
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | remove' _ _ (_,[]) = []
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | remove' cd1 cd2 (x::xr,y::yr) = if (cd1 x) < (cd2 y)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder then remove' cd1 cd2 (xr,y::yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder else if (cd2 y) < (cd1 x)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder then y::(remove' cd1 cd2 (x::xr,yr))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder else remove' cd1 cd2 (xr,yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove cmp_data = remove' cmp_data cmp_data
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove_parent_data df cmp_data T = let val d = df T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val pd = (List.foldl op@ [] (map df (Context.parents_of T)))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in remove cmp_data (mergesort cmp_data pd,mergesort cmp_data d) end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_consts = let val consts_of = Name_Space.dest_table o #constants o Consts.dest o Sign.consts_of
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in remove_parent_data consts_of #1 end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_axioms = remove_parent_data Theory.axioms_of #1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_theorems = let fun theorems_of T = map (fn (a,b) => (a, prop_of b)) (Global_Theory.all_thms_of T)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in remove_parent_data theorems_of #1 end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun get_datatypes T = let val tname = Context.theory_name T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val ts = (#log_types o Type.rep_tsig o Sign.tsig_of) T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in map (fn s => (String.extract (s,tl+1,NONE),Datatype.get_info T s)) (List.filter (String.isPrefix tname) ts) end
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun full_name T name = Name_Space.full_name (Sign.naming_of T) (Binding.name name)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun is_mutually_rec_type T (n,SOME(i)) = (case (#alt_names i) of SOME(names) => List.exists
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (Option.isSome o (Datatype.get_info T) o (full_name T))
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | NONE => false)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | is_mutually_rec_type _ (_,NONE) = false
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun get_generated_theorems T ts =
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder let fun get_ths (n,info) =
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder let val alt_names = case (#alt_names info) of
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder SOME(names) => n::(List.filter (Option.isSome o (Datatype.get_info T) o (full_name T)) names)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val is' = List.map ((Datatype.get_info T) o (full_name T)) alt_names
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun thms i g = List.foldl (fn (get_thm, l1) => (Thm.derivation_name (get_thm i))::l1) [] g
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun thmss i g = List.foldl (fn (get_thms,l1) => (List.map Thm.derivation_name (get_thms i)@l1)) [] g
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (fn (i,l) => (thms i [#induct,#exhaust,#nchotomy,#case_cong,#weak_case_cong,#split,#split_asm])
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder @(thmss i [#inject,#distinct,#inducts,#rec_rewrites,#case_rewrites])@l)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val new_type_names = the_default [n] (#alt_names info)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder cf. http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML#l329
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML#l338
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/Pure/global_theory.ML#l168
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/Pure/global_theory.ML#l162
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/Pure/global_theory.ML#l158
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/Pure/global_theory.ML#l139 *)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val prfx = Binding.qualify true (space_implode "_" new_type_names)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val b = prfx (Binding.name "simps")
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val pre_name = Global_Theory.name_thms true true
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val post_name = Global_Theory.name_thms false true
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val name = Name_Space.full_name naming b
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val thms2 = List.map Thm.derivation_name (post_name name (pre_name name (
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (List.foldl (fn (i,l) => ((#inject i)@(#distinct i)@(#case_rewrites i)@l)) [] is)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder @(#rec_rewrites info))))
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder cf. http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML#l324
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML#l340
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val b1 = prfx (Binding.name "splits")
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val name1 = Name_Space.full_name naming b1
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val splits = List.foldl (fn (i,l) => (#split i)::(#split_asm i)::l) [] is
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val thms3 = List.map Thm.derivation_name
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (post_name name1 (pre_name name1 splits))
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder cf. http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_codegen.ML#l65
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_codegen.ML#l109
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_codegen.ML#l113
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_codegen.ML#l114 *)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun eq_thms name =
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val (vs,cos) = Datatype.the_spec T (full_name T name);
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val {descr, index, ... } = Datatype.the_info T (full_name T name);
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val dummy = Skip_Proof.make_thm T (Var (("", 0), propT));
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val triv_injects = map_filter
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (fn (c,[]) => SOME (dummy)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | _ => NONE) cos;
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val injects = map (fn _ => dummy) (nth (Datatype_Prop.make_injs [descr] vs) index);
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val distincts = maps (fn _ => [dummy,dummy]) (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val prefix = Binding.qualify true name o Binding.qualify true "eq" o Binding.name;
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val name1 = Name_Space.full_name naming (prefix "refl");
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val name2 = Name_Space.full_name naming (prefix "simps");
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val thms = List.map Thm.derivation_name ((post_name name1 (pre_name name1 [dummy]))@(post_name name2 (pre_name name2 (triv_injects@injects@distincts))));
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val thms4 = flat (List.map eq_thms alt_names)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder in thms1@thms2@thms3@thms4 end
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun check_rec (n,v) = if is_mutually_rec_type T (n,SOME(v))
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder then if List.exists (fn altn => altn = n) (List.tl (Option.valOf (#alt_names v)))
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder val ts' = List.foldl (fn (d,l) => case d of (n,SOME(v)) => if check_rec (n,v) then (n,v)::l
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | (_,NONE) => l) [] ts
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder in unique (mergesort id (List.foldl (fn (t,l) => (get_ths t)@l) [] ts')) end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun filter rem d = remove' id #1 ((mergesort id rem),(mergesort #1 d))