export_helper.ml revision 067b7cf571968fe8e91212059da1590c2dfa741a
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
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
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun get_generated_theorems T ts = let fun get_ths (n,i) = let val thms1 = (List.foldl (fn (get_thm,l) => (Thm.derivation_name (get_thm i))::l)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder [] [#induct,#exhaust,#nchotomy,#case_cong,#weak_case_cong,#split,#split_asm])
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder @(List.foldl (fn (get_thms,l) => (List.map Thm.derivation_name (get_thms i))@l)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder [] [#inject,#distinct,#inducts,#rec_rewrites,#case_rewrites])
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val new_type_names = the_default [n] (#alt_names i)
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 *)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val prfx = Binding.qualify true (space_implode "_" new_type_names)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val b = prfx (Binding.name "simps")
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val pre_name = Global_Theory.name_thms true true
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val post_name = Global_Theory.name_thms false true
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val name = Name_Space.full_name naming b
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val thms2 = List.map Thm.derivation_name (post_name name (pre_name name (
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (#inject i)@(#distinct i)@(#case_rewrites i)@(#rec_rewrites i))))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder cf. http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML#l319
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML#l340
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (*val b1 = prfx (Binding.name "split")
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val name1 = Name_Space.full_name naming b1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val thms3 = List.map Thm.derivation_name
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (post_name name1 (pre_name name1 (#split i)))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val b2 = prfx (Binding.name "split_asm")
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val name2 = Name_Space.full_name naming b2
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val thms4 = List.map Thm.derivation_name
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (post_name name2 (pre_name name2 (#split_asm i)))*)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in thms1@thms2 end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val ts' = List.foldl (fn (d,l) => case d of (n,SOME(v)) => (n,v)::l
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | (_,NONE) => l) [] ts
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in 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))