067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersignature ExportHelper =

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersig

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type const_info = (string * (typ * term option)) list

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type term_info = (string * term) list

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type datatype_info = (string * Datatype.info) list

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder type class_info = (string * (string list) * term_info *

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder ((string * typ) list)) list

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (* name * parents * assumes * fixes *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder type locale_info = (string * ((string * typ) * mixfix) list

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (* name * fixes *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder * (string * term) list * (string * term) list

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (* in-locale axioms * ex-locale axioms *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder * string list) list

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (* parents *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type theory_info =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder string (* theory name *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * string list (* imports *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * const_info (* constants *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* axioms *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* theorems *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * datatype_info (* data types *)

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder * class_info (* class info *)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder * locale_info (* locale info *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val theory_info : theory -> theory_info

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val tinfo2xml : theory -> string -> theory_info -> XML.tree

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederend;

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstructure ExportHelper : ExportHelper =

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstruct

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Types *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type const_info = (string * (typ * term option)) list

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type term_info = (string * term) list

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type datatype_info = (string * Datatype.info) list

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder type class_info = (string * (string list) * term_info *

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder ((string * typ) list)) list

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (* name * parents * assumes * fixes *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder type locale_info = (string * ((string * typ) * mixfix) list

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (* name * fixes *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder * (string * term) list * (string * term) list

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (* in-locale axioms * ex-locale axioms *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder * string list) list

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (* parents *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder type theory_info =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder string (* theory name *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * string list (* imports *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * const_info (* constants *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* axioms *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* theorems *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * datatype_info (* data types *)

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder * class_info (* class info *)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder * locale_info (* locale info *)

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* General helper functions *)

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun id x = x

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun mergesort _ [] = []

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | mergesort _ [x] = [x]

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | mergesort cmp_data xs =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (ys,zs) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.foldl (fn(i, (ys,zs)) => (zs, i::ys)) ([],[]) xs

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun merge (xs,[]) = xs

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | merge ([],xs) = xs

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | merge (x::xr,y::yr) = if (cmp_data x) <= (cmp_data y)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder then x::merge(xr,y::yr)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder else y::merge(x::xr,yr)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in merge(mergesort cmp_data ys, mergesort cmp_data zs) end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* remove duplicate entries from a sorted list *)

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' _ _ (_,[]) = []

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | remove' cd1 cd2 (x::xr,y::yr) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder if (cd1 x) < (cd2 y)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder then remove' cd1 cd2 (xr,y::yr)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder else if (cd2 y) < (cd1 x)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder then y::(remove' cd1 cd2 (x::xr,yr))

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder else remove' cd1 cd2 (xr,yr)

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove cmp_data = remove' cmp_data cmp_data

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun remove_parent_data df cmp_data T =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val d = df T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val pd = (List.foldl op@ [] (map df (Context.parents_of T)))

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in remove cmp_data (mergesort cmp_data pd,mergesort cmp_data d) end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun filter rem (d : (string * 'a) list) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder remove' id #1 ((mergesort id rem),(mergesort #1 d))

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Theory-specific helpers *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* full name of a name used in theory T *)

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun full_name T name = Name_Space.full_name (Sign.naming_of T) (Binding.name name)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* remove unnecessary information from (recursive) datatypes *)

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder fun is_mutually_rec_type T (n,i) = length (#descr i) > 1

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun check_rec T (n,v) = if is_mutually_rec_type T (n,v)

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder then (#index v) < 1

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder else true

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun restructure_rec_types T ts = List.foldl (fn (d,l) => case d of

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (n,SOME(v)) => if check_rec T (n,v) then (n,v)::l

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder else l

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | (_,NONE) => l) [] ts

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder fun unfold_conjunction tm =

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder case tm of

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (Const ("Pure.conjunction",_)) $ t => unfold_conjunction t

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | t $ (Const ("Pure.conjunction",_)) => unfold_conjunction t

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | t1 $ t2 =>

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (unfold_conjunction t1)

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder @(unfold_conjunction t2)

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | _ => [tm]

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder fun unfold_hol_conjunction tm = case tm of

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder Const ("HOL.conj",_) $ t $ t1 => (unfold_hol_conjunction t)@(unfold_hol_conjunction t1)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | Const ("HOL.conj",_) $ t => [t]

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | _ => [tm]

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder fun strip_hol_all l b tm = case (b,tm) of

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (true,Const ("HOL.All",_) $ Abs (s,t,tm)) =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder strip_hol_all ((s,t)::l) true tm

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | (_,Bound i) => if List.length l > i

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder then let val (s,t) = List.nth(l,i)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder in Var ((s,0),t) end

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder else tm

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | (_,Abs (s,t,tm)) => Abs (s,t,strip_hol_all l false tm)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | (_,t1 $ t2) => (strip_hol_all l false t1) $

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (strip_hol_all l false t2)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | _ => tm

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* get raw theory information *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_consts T =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val consts_of = (Name_Space.dest_table (Syntax.init_pretty_global T)) o

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder #constants o Consts.dest o Sign.consts_of

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in remove_parent_data consts_of #1 T end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val get_axioms = remove_parent_data Theory.axioms_of #1

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val get_theorems =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let fun theorems_of T = map (fn (a,b) => (a, prop_of b))

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (Global_Theory.all_thms_of T)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in remove_parent_data theorems_of #1 end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_datatypes T =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val tname = Context.theory_name T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val tl = String.size tname

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val ts = (#log_types o Type.rep_tsig o Sign.tsig_of) T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val ts' = map (fn s => (String.extract (s,tl+1,NONE),Datatype.get_info T s))

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (String.isPrefix tname) ts)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in restructure_rec_types T ts' end

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder fun get_classes T thms =

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder let val cls_suffix = "_class_def"

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val cls_names = List.map (fn n => String.substring

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (n,0,String.size n-String.size cls_suffix))

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (List.filter (fn n =>

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder if String.isSuffix cls_suffix n

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder then true else false) (List.map #1 thms))

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder in List.map (fn name =>

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder let val name' = String.substring (name,String.size "Class.",

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder String.size name - String.size "Class.")

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val i = AxClass.get_info T name

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val parents = let fun split tms = case tms of

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (Const ("HOL.Trueprop",_))::tms' => []

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | (Const ("TYPE",_))::tms' => (split tms')

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | (Const (s,_))::tms' => let val s' =

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder if String.isPrefix "Class." s

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder then String.substring (s,String.size "Class.",

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder String.size s - String.size "Class."

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder - String.size "_class")

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder else s

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder in s'::(split tms') end

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | _::tms' => (split tms')

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | [] => []

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder in case (Thm.prop_of o #def) i of

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder _ $ t => (split o unfold_conjunction) t

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | _ => [] end

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val axioms' = List.filter

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (fn (n,_) => String.isPrefix (name^".") n) thms

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val axioms = List.map (fn (n,t) => case t of

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder _ $ (_ $ t') => (n,t')

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder | _ => (n,t)) axioms'

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val params = #params i

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder in (name',parents,axioms,params) end) cls_names end

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder fun get_locales T =

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder let val names = List.filter (String.isPrefix (Context.theory_name T))

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (Locale.all_locales T)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val (_,tb) = Locale.locale_deps T

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val tb_list = List.map (fn (k,t) =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (k,Symtab.dest t)) (Symtab.dest tb)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val parents = List.foldl (fn ((s,l),t') =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder List.foldl (fn ((s1,l1),t) => Symtab.map_default (s1,([],[]))

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (fn (parents,pfixes) => (s::parents,(

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder ((List.map (fn Free (s,_) => s))

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder o List.concat) l1)@pfixes)) t

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder ) t' l) Symtab.empty tb_list;

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val filter = ["_axioms.intro","_axioms_def",

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder "_def",".intro",".axioms_"]

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder in List.map (fn name =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder let val params' = Locale.params_of T name

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val parent_params =

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder case Symtab.lookup parents name of

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder SOME (_,v) => v

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder | _ => []

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val params = List.filter (fn ((s,_),_) =>

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder not (List.exists (fn p => p = s) parent_params)) params'

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val axs = List.filter (fn t => String.isPrefix name (#1 t))

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (Global_Theory.all_thms_of T)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val axioms' = List.filter

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (fn t => (not (List.exists

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (fn s => #1 t = name ^ s) filter))) axs

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val axioms = List.map (fn (s,t) =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder (s,((fn Const ("==>",_) $ _ $ t => t) o Thm.prop_of) t))

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder axioms'

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val in_locale_axioms =

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder case (List.find (fn x => (#1 x) = (name^"_axioms_def")) axs) of

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder SOME v => List.map (strip_hol_all [] true)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder ((unfold_hol_conjunction o

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (fn _ $ _ $ tm => tm) o Thm.prop_of o #2) v)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder | _ => []

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val in_loc = List.filter (fn (s,t) =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder List.exists (fn t' => t = t') in_locale_axioms) axioms

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder val ex_loc = List.filter (fn (s,t) =>

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder not (List.exists (fn t' => t = t') in_locale_axioms)) axioms

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val ps = case Symtab.lookup parents name of

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder SOME(v,_) => v

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder | _ => []

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder in (name,params,in_loc,ex_loc,ps) end

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder ) names end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Guess the names of generated axioms, consts and theorem *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun prefix p s = List.map (fn x => p^s^x)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun postfix s p = List.map (fn x => x^s^p)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun l_to_intl l = List.map Int.toString

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.tl (List.rev (List.foldl (fn (_,x::xs) => (x+1)::x::xs) [0] l)))

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_type_names T ts =

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder let

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder val rec_types = List.filter (check_rec T) ts

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder val grouped_rec_names = List.map (fn x =>

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder List.map (Long_Name.base_name o #1 o #2) ((#descr o #2) x)) rec_types

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val def_names = (List.map (Long_Name.base_name o #1 o #2)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.concat (List.map (#descr o #2) rec_types)))

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val all_rec_names = (List.concat grouped_rec_names)@def_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val constructors = List.map #1 (List.concat (List.map (#3 o #2)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.concat (List.map (#descr o #2) ts))))

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (grouped_rec_names,all_rec_names,constructors,def_names) end

02ef6fcc031a33d9753dda5a46e6101328b3d7c5Jonathan von Schroeder fun get_gen_consts T name ts consts =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (grouped_rec_names,all_rec_names,constructors,_) = get_type_names T ts

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val rec_names = List.concat grouped_rec_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val mutually_rec_names =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.filter (fn x => List.length x > 1) grouped_rec_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val simple_names = List.map List.hd

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (fn x => List.length x = 1) grouped_rec_names)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val locale_names = List.filter

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (String.isPrefix (Context.theory_name T))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (Locale.all_locales T)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in constructors@(prefix name "." (List.concat

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [prefix "Abs" "_" rec_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "Rep" "_" rec_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x) all_rec_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => let val comb = space_implode "_" x

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => [x^"."^x^"_rec",

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rec_set",

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rep_set"]) simple_names),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn x => let val comb = space_implode "_" x

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (comb^"."^comb^"_rec_set")::

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (comb^"."^comb^"_rep_set")::(List.concat

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.map

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn y => [comb^"."^comb^"_rec_"^y,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rec_set_"^y,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rep_set_"^y])

02ef6fcc031a33d9753dda5a46e6101328b3d7c5Jonathan von Schroeder (l_to_intl x))) end) mutually_rec_names)]))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.filter (String.isPrefix "Class.") consts)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.filter (fn s => List.exists

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (fn l => String.isPrefix l s) locale_names) consts) end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_gen_axioms T name ts =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (grouped_rec_names,all_rec_names,constructors,def_names) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder get_type_names T ts

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val rec_names = List.concat grouped_rec_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder grouped_rec_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val simple_names = List.map List.hd

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (fn x => List.length x = 1) grouped_rec_names)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (postfix "_" "def" constructors)@(prefix name "." (List.concat

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [prefix "arity_type" "_" def_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "equal" "_" (postfix "_" "def_raw" def_names),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "type_definition" "_" rec_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x^"_def") def_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (postfix "_" "def"

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.concat [(List.concat (List.map

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn x => let val comb = space_implode "_" x

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (comb^"."^comb^"_rec_set")::

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (comb^"."^comb^"_rep_set")::(List.concat

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.map

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn y => [comb^"."^comb^"_rec_"^y,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rec_set_"^y,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rep_set_"^y]) (l_to_intl x))) end)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder mutually_rec_names)),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => let val comb = space_implode "_" x

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => [x^"."^x^"_rec",

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder x^"."^x^"_rec_set",

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder x^"."^x^"_rep_set"]) simple_names)]))])) end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_gen_theorems T name ts ths =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (grouped_rec_names,all_rec_names,constructors,def_names) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder get_type_names T ts

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val rec_names = List.concat grouped_rec_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder grouped_rec_names

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val simple_names = List.map List.hd

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (fn x => List.length x = 1) grouped_rec_names)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val locale_names = List.filter

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (String.isPrefix (Context.theory_name T))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (Locale.all_locales T)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val locale_filter = ["_axioms.intro","_axioms_def","_def","."]

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in prefix name "." (List.concat

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [prefix "arity_equal" "_" def_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "arity_type" "_" def_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "type_definition" "_" rec_names,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "equal" "_" (postfix "_" "def" def_names),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "equal" "_" (postfix "_" "def_raw" def_names),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x) def_names])

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder @(List.concat (List.map (fn x =>

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.filter (String.isPrefix (name^"."^x^".")) ths) (unique (rec_names@def_names))))

6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder @(List.concat (List.map (fn x =>

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.filter (String.isPrefix (name^"."^(space_implode "_" x)^".")) ths)

02ef6fcc031a33d9753dda5a46e6101328b3d7c5Jonathan von Schroeder mutually_rec_names))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.filter (String.isPrefix "Class.") ths)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.filter (fn s => (List.exists

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (fn l => List.exists

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (fn f => String.isPrefix (l^f) s) locale_filter) locale_names)) ths) end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Represent collected data as XML *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* Enrich the (isabelle-builtin) XML representation of terms with infix information *)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder fun mixfix_to_args m = case m of

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder SOME(Mixfix.Infixl (s,j)) =>

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [("infixl",s),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder ("mixfix_i",string_of_int j)]

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | SOME(Mixfix.Infixr (s,j)) =>

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [("infixr",s),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder ("mixfix_i",string_of_int j)]

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | SOME(Mixfix.Infix (s,j)) =>

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [("infix",s),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder ("mixifix_i",string_of_int j)]

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder | NONE => []

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder fun xml_of_term' T tbl t =

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder case t of

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder XML.Elem (("Const",a),t) =>

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder let val b = case (Syntax.guess_infix (Sign.syn_of T)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (Lexicon.mark_const ((#2 o List.hd) a))) of

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder SOME(mx) => mixfix_to_args (SOME mx)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder |NONE => mixfix_to_args (Symtab.lookup tbl ((#2 o List.hd) a))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder in XML.Elem (("Const",a@b),map (xml_of_term' T tbl) t) end

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder | XML.Elem ((s,a),t) => XML.Elem ((s,a),map (xml_of_term' T tbl) t)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder fun xml_of_term T t = xml_of_term' T Symtab.empty

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (XML_Syntax.xml_of_term t)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun remove_hol_true_prop t = case t of

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder $ (Const ("HOL.Trueprop",_), tm) => tm

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | tm => tm

b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder fun termListToXML T section l = XML.Elem ((section,[]),List.map (

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fn (s,t) => XML.Elem (("Term",[("name",Long_Name.base_name s)]),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [xml_of_term T (remove_hol_true_prop t)])) l)

b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder fun termTypListToXML T section l = XML.Elem ((section,[]),List.map (

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fn (s,(t,v)) => let val v' = case v of

b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder SOME(tm) => (("Term",[("name",Long_Name.base_name s)]),[xml_of_term T tm])

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder | NONE => (("NoTerm",[]),[])

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in XML.Elem (("ConstDecl",[("name",Long_Name.base_name s)]),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [XML_Syntax.xml_of_type t,XML.Elem v']) end) l)

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder fun dtypToXML (Datatype.DtTFree (s,_)) = XML.Elem (("DtTFree",[("s",s)]),[])

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | dtypToXML (Datatype.DtType (s,dtl)) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder XML.Elem (("DtType",[("s",s)]),List.map dtypToXML dtl)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | dtypToXML (Datatype.DtRec i) =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder XML.Elem (("DtRec",[("i",Int.toString i)]),[])

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fun constructorToXML (name,dtl) = XML.Elem

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder (("Constructor",[("val",Long_Name.base_name name)]),List.map dtypToXML dtl)

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fun typeToXML d = List.map

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder (fn (i,(s,vs,dt)) => let val attrs =

25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder [("i",Int.toString i),("name",Long_Name.base_name s)]

e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder in XML.Elem (("RecType",attrs),[

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder XML.Elem (("Vars",[]),List.map dtypToXML vs),

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder XML.Elem (("Constructors",[]),List.map constructorToXML dt)

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder ])

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder end)

75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder (#descr d)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun typeListToXML section l = XML.Elem ((section,[]),List.map (

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fn (s,d) => XML.Elem (("TypeDecl",[("name",s)]),typeToXML d)) l)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Prepare data *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* make sure that type names local to the theory do not

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder have the theory name as prefix

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (because this is not their proper name) *)

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder fun fixTypeNames moduleName t = case t of

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder XML.Elem (("Type",a),c) => XML.Elem (("Type",

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder List.map (fn (n,s) =>

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder if n = "name" andalso String.isPrefix (moduleName^".") s

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder then (n,String.extract (s,(String.size moduleName)+1,NONE))

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder else (n,s)) a),

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder List.map (fixTypeNames moduleName) c)

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder | XML.Elem (d,c) =>

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder XML.Elem (d,List.map (fixTypeNames moduleName) c)

d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder | _ => t

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Module interface *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* collect information necessary to reconstruct the theory *)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun theory_info T =

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val name = Context.theory_name T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val imports = List.map

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder Context.theory_name (Theory.parents_of T)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val types = get_datatypes T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val consts = get_consts T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val thms = get_theorems T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val axioms = get_axioms T

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val classes = get_classes T thms

02ef6fcc031a33d9753dda5a46e6101328b3d7c5Jonathan von Schroeder val gen_consts = get_gen_consts T name types (List.map #1 consts)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val gen_thms = get_gen_theorems T name types (List.map #1 thms)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val gen_axioms = (get_gen_axioms T name types)@(List.map #1 thms)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val locales = get_locales T

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (name, imports,

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (filter gen_consts consts),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (filter gen_axioms axioms),

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (filter gen_thms thms),

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder types,classes,locales) end

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* export theory info as xml *)

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder fun tinfo2xml T fname (name,imports,consts,axioms,thms,

8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder types,classes,locales) =

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder let val b = Long_Name.base_name

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val xml_imports = XML.Elem

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (("Imports",[]), List.map (fn s => XML.Elem (("Import",[("name",s)]),[])) imports)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_consts = termTypListToXML T "Consts" consts

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_axioms = termListToXML T "Axioms" axioms

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_theorems = termListToXML T "Theorems" thms

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_types = typeListToXML "Types" types

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder val xml_classes = XML.Elem (("Classes",[]),List.map

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (fn (name,parents,axioms,params) =>

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder XML.Elem (("ClassDecl",[("name",name)]),

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (List.map (fn (s,t) => XML.Elem

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (("Axiom",[("name",Long_Name.base_name s)]),

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder [xml_of_term T (remove_hol_true_prop t)])) axioms)

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder @((List.map (fn (s,t) => XML.Elem

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (("Param",[("name",Long_Name.base_name s)]),

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder [XML_Syntax.xml_of_type t])) params))

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder @(List.map (fn n => XML.Elem

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (("Parent",[("name",n)]),[])) parents))) classes)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder val xml_locales = XML.Elem (("Locales",[]),List.map

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (fn (name,params,in_loc,ex_loc,parents) =>

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder let val tbl = List.foldl (fn (((s,_),m),t) =>

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder Symtab.update (s,m) t)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder Symtab.empty params in

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder XML.Elem (("LocaleDecl",[("name",b name)]),

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (List.map (fn ((s,t),m) =>

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder XML.Elem (("LocaleParam",[("name",s)]

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(mixfix_to_args (SOME m))),

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder [XML_Syntax.xml_of_type t])) params)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.map (fn (s,t) => XML.Elem

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (("IAxiom",[("name",b s)]),

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder [xml_of_term' T tbl (XML_Syntax.xml_of_term t)]))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder in_loc)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.map (fn (s,t) => XML.Elem

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (("EAxiom",[("name",b s)]),

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder [xml_of_term' T tbl (XML_Syntax.xml_of_term t)]))

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder ex_loc)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder @(List.map (fn n => XML.Elem

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (("Parent",[("name",n)]),[])) parents)

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder )end) locales)

255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in fixTypeNames name (XML.Elem (("IsaExport",[("file",fname)]),

8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder [xml_imports,xml_consts,xml_axioms,xml_theorems,xml_types,xml_classes,xml_locales])) end

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederend;