067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersignature ExportHelper =

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersig

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* types *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder type named_term = (string * term)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* general helper functions *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val unlines : string list -> string

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val unqualify : string -> string

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* isabelle specific functions *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theory_of_string : string -> theory list -> theory

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theory_by_name : string -> theory

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val name_of_theory : theory -> string

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms_of : theory -> named_term list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val non_image_theories : theory -> theory list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val thms_of : theory -> named_term list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val consts_of : theory -> (string * typ) list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val datatypes_of : theory -> ((string * typ list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ list) list) list) list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* mutually_rec_types@(name * type_params *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder constructors@(constructor_name * type_args))) *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions_of : theory -> (string * typ *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (term list * term) list) list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * type *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder def_eqs@(pats * defterm) *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes_of : theory -> (class * string list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * term) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * parents * assumes * fixes *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales_of : theory -> (string *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((string * typ) * mixfix) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * fixes * in-locale axioms *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ex-locale axioms * parents *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val pretty_as_str : Pretty.T -> string

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_term : theory -> term -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_typ : theory -> typ -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_name : string -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_function : theory -> (string * typ *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (term list * term) list) -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_class : theory -> (class * string list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * term) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_locale : theory -> (string *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((string * typ) * mixfix) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_datatype : theory -> (string * typ list * (string *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder typ list) list) list -> Pretty.T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theory_of_exportable_data : theory -> theory

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val get_basic_theory_data : theory -> (named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* axioms * theorems * consts *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder type theory_data = (string * named_term list * named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list * ((string * typ list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ list) list) list) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ * (term list * term) list) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (class * string list * (string * term) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * ((string * typ) * mixfix) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) list)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * axioms * theorems * consts * datatypes *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder functions * classes * locales *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val get_theories : theory -> theory_data list

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val xml_of_theories : theory_data list -> XML.tree

97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder exception ExportError of string

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederend;

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstructure ExportHelper : ExportHelper =

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstruct

b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederexception ExportError of string

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertype named_term = string * term

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertype theory_data = (string * named_term list * named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list * ((string * typ list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ list) list) list) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ * (term list * term) list) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (class * string list * (string * term) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * ((string * typ) * mixfix) list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) list)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * axioms * theorems * consts * datatypes *

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder functions * classes * locales *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* ------------------------------ General helper functions *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval unlines = String.concatWith (String.str (Char.chr 10))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun lift f sel = fn (t1,t2) => f (sel t1,sel t2)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun unqualify n = if Long_Name.is_qualified n

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (Long_Name.implode (List.tl (Long_Name.explode n)))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder else n

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* ------------------------------ Isabelle specific functions *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* Keep track of the number of theories created from a string *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval thmNum = Unsynchronized.ref 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* create a theory from a string of its body *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun theory_of_string body parents =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val name = "TempTheory"^Int.toString (Unsynchronized.inc thmNum)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val header = Thy_Header.make ("TempTheory",Position.none) [] [] []

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val text = unlines ["theory "^name,"begin",body,"end"]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in #1 (Thy_Load.load_thy 0 (Thy_Load.get_master_path ()) header

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Position.start text parents) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun remove_hol_true_prop t = case t of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder op$ (Const ("HOL.Trueprop",_), tm) => tm

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | tm => tm

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval prettify_term = Logic.strip_imp_concl o remove_hol_true_prop

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* remove data that is already present in a parent theory *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun remove_parent_data df cmp T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val d = df T

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

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Ord_List.subtract cmp (Ord_List.make cmp pd) (Ord_List.make cmp d) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* a couple of aliases *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval theory_by_name = Thy_Info.get_theory

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval name_of_theory = Context.theory_name

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval axioms_of = Theory.axioms_of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* check if the theory is not part of the logic image *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun is_non_image_theory T = length (Thy_Info.loaded_files (name_of_theory T)) > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun non_image_theories T = List.concat (List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn T' => if is_non_image_theory T'

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then T'::(non_image_theories T') else [])

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Context.parents_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun hol_forall_elim tm =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val qnt = #1 (Term.dest_Const (HOLogic.all_const HOLogic.boolT))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val body = Term.strip_qnt_body qnt tm

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val vars = List.map (fn (s,tp) => Var ((s,0),tp))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Term.strip_qnt_vars qnt tm)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Term.subst_bounds (List.rev vars, body) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun hol_conjunctions tm = case HOLogic.dest_conj tm of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [_] => [tm]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | tms => List.concat (List.map hol_conjunctions tms)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun thms_of T = List.map (fn (s,d) => (s,prop_of d))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (remove_parent_data Global_Theory.all_thms_of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (lift fast_string_ord #1) T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* currently there seems to be no way (anymore) to

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder attach any terms to a const directly. Thus the discarded

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder part is (hopefully) always NONE

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder todo: maybe throw an exception if this is not the case? *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun consts_of T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (((Name_Space.dest_table (Syntax.init_pretty_global T)) o

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder #constants o Consts.dest o Sign.consts_of) T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in remove_parent_data get_consts (lift fast_string_ord #1) T end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun datatypes_of T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val get_datatypes = (#log_types o Type.rep_tsig o Sign.tsig_of)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val ts = remove_parent_data get_datatypes fast_string_ord T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val is_mutually_rec_type = fn (_,i) => length (#descr i) >1

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val check_rec = fn (n,v) => if is_mutually_rec_type (n,v)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (#index v) < 1 else true

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val rec dtyp2typ = fn (descs,t) => case t of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Datatype.DtTFree (s,srt) => TFree (s,srt)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | Datatype.DtType (s,ts) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Type (s,List.map (curry dtyp2typ descs) ts)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | Datatype.DtRec i =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder case List.find (curry op= i o #1) descs of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME (_,(s,ts,_)) => Type (s, List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (curry dtyp2typ descs) ts)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | NONE => raise ExportError("Internal Error!")

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val dt_desc = fn info => List.map (fn (i,(s,vs,eqs)) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val vs' = List.map (curry dtyp2typ info) vs

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val eqs' = List.map (fn (s,ts) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (s,List.map (curry dtyp2typ info) ts)) eqs

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (s,vs',eqs') end) info

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.foldl (fn (n,l) => case Datatype.get_info T n of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME(v) => if check_rec (n,v)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (dt_desc (#descr v))::l

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder else l

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | NONE => l) [] ts end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* Notes:

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder HOLogic is in HOL/Tools/hologic.ML

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder dest_Const is in Pure/term.ML

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Logic is in Pure/logic.ML *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval functions_of =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val get_funs = fn T =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val d = Item_Net.content (Function_Common.get_function

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Proof_Context.init_global T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fun_def = (fn (pats,def) => (#2 (strip_comb pats),def))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o HOLogic.dest_eq o HOLogic.dest_Trueprop o #2

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o Logic.dest_implies o prop_of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.map (fn (c,i) => case dest_Const c of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (n,t) => (n,t,List.map fun_def (#psimps i))) d end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in remove_parent_data get_funs (lift fast_string_ord #1) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun classes_of T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val cls_suffix = "_class_def"

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val thms = thms_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val cls_names = List.map (fn n => String.substring (n,0,String.size n-

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder String.size cls_suffix)) (List.filter (String.isSuffix cls_suffix)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map #1 thms))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.map (fn name =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val i = AxClass.get_info T name

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents' = List.concat (List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn tm => Term.add_const_names tm [])

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((Logic.dest_conjunction_list o #2

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o Logic.dest_equals o Thm.prop_of o #def) i))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents = List.map (fn n => String.substring

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (n,0,String.size n - String.size "_class"))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.filter (fn n => (String.isSuffix "_class" n) andalso

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (not (String.isPrefix "HOL" n))) parents')

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o Logic.dest_implies) t))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.filter ((String.isPrefix (name^".")) o #1) thms)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* note: instead of cls_names we should only use

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ancestors of the class *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val all_params = List.map (fn (s,t) => (Long_Name.base_name s,t))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.concat (List.map (#params o AxClass.get_info T) cls_names))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder axioms'

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (name,parents,axioms,#params i) end) cls_names end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun locales_of T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val all_locales = fn T => List.map (fn l => (#name l, #parents l))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Locale.pretty_locale_deps T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales = Ord_List.subtract

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn (c,l) => fast_string_ord (#1 c,#1 l))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (classes_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (remove_parent_data all_locales

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (lift fast_string_ord #1) T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.map (fn (name,ps) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val parent_params = List.map (#1 o #1) (List.concat

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (Locale.params_of T o #1)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.filter (fn (s,_) => List.exists (curry op= s) ps) locales)))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val params = Ord_List.subtract (fn (s,((s1,_),_)) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder fast_string_ord (s,s1))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord parent_params)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord (#1 o #1))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Locale.params_of T name))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val filter = ["_axioms.intro","_axioms_def","_def",".intro",".axioms_"]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axs = List.filter ((String.isPrefix name) o #1)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Global_Theory.all_thms_of T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms' = List.filter

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn t => (not (List.exists

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn s => String.isPrefix (name ^ s) (#1 t))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder filter))) axs

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms = List.map (fn (s,t) => (s,(HOLogic.dest_Trueprop o #2

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o Logic.dest_implies

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o Thm.prop_of) t)) axioms'

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fix_consts = List.map (fn (s,t) => (s, Term.subst_Vars

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn ((s,tp),_) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((s,0),Const (s,tp))) params) t))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parse_axioms = fn v => List.map hol_forall_elim

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((hol_conjunctions o #2 o Logic.dest_equals o Thm.prop_of o #2) v)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val in_locale_axioms =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder case List.find ((curry op= (name^"_axioms_def")) o #1) axs of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME v => parse_axioms v

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | _ =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder case List.find ((curry op= (name^"_def")) o #1) axs of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME v => parse_axioms v

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | _ => []

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val in_loc = List.filter (fn (_,t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.exists (fn t' => t = t') in_locale_axioms) axioms

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val ex_loc = List.filter (fn (_,t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder not (List.exists (fn t' => t = t') in_locale_axioms)) axioms

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (name,params,fix_consts in_loc,fix_consts ex_loc,ps) end) locales end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* ------------------------------ Represent as string *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun pretty_as_str p = Pretty.str_of p

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_term T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val ctxt = Config.put Printer.show_question_marks false

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Proof_Context.init_global T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Syntax.pretty_term ctxt end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_typ T = Syntax.pretty_typ (Proof_Context.init_global T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_name n' =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val n = Long_Name.base_name n'

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in if String.isSubstring " " n then Pretty.quote (Pretty.str n)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder else Pretty.str n end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_function T (s,tp,def_eqs) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val head = [Pretty.str "fun ", repr_name s, Pretty.str " :: ",

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_typ T tp), Pretty.str " where "]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val body = List.map (fn (pats,tm) => Pretty.quote (Pretty.block

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((Pretty.breaks ([repr_name s]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn p => Pretty.enclose "(" ")" [repr_term T p])

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder pats)))@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [Pretty.str " = ",repr_term T tm]))) def_eqs

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Pretty.block (head@Pretty.separate " | " body) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_class T (s,ps,assumes,fixes) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val head = [Pretty.str "class", repr_name s]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(if length fixes + length assumes + length ps > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "="] else [])

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents = List.map repr_name ps

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fixes' = List.map (fn (s,tp) => Pretty.block (Pretty.breaks

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [repr_name s,Pretty.str "::",

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_typ T tp)])) fixes

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [repr_name s, Pretty.str ":",

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_term T tm)])) assumes

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length (fixes'@assumes') > 0 andalso length parents > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "+"] else [])@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length fixes' > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length assumes' > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "assumes"]@(Pretty.separate "and" assumes') else [])) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_locale T (s,fixes,in_loc,_,ps) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val head = [Pretty.str "locale", repr_name s]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(if length fixes + length in_loc + length ps > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "="] else [])

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents = List.map repr_name ps

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fixes' = List.map (fn ((s,tp),_) => Pretty.block (Pretty.breaks

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [Pretty.str s,Pretty.str "::",

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_typ T tp)])) fixes

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [repr_name s, Pretty.str ":",

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_term T tm)])) in_loc

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length (fixes'@assumes') > 0 andalso length parents > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "+"] else [])@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length fixes' > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length assumes' > 0

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "assumes"]@(Pretty.separate "and" assumes') else [])) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_datatype T d =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val dts = List.map (fn (s,vs,eqs) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val vs' = Pretty.enclose "(" ")"

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Pretty.separate "," (List.map (repr_typ T) vs))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val eqs' = Pretty.separate "|" (List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn (s,vs) => Pretty.block (Pretty.breaks

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ([repr_name s]@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (Pretty.quote o repr_typ T) vs)))) eqs)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Pretty.block (Pretty.breaks

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ([vs']@[repr_name s,Pretty.str "="]@eqs')) end) d

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (Pretty.block o Pretty.breaks) ([Pretty.str "datatype"]@

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.separate "and" dts) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun theory_of_exportable_data T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val datatypes = datatypes_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions = functions_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes_Graph = String_Graph.make

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn l => ((#1 l,l),#2 l)) (classes_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes_sorted =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.rev (String_Graph.topological_order classes_Graph)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes = List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (#1 o #2 o (String_Graph.get_entry classes_Graph))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder classes_sorted

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales_Graph = String_Graph.make

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn l => ((#1 l,l),#5 l)) (locales_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales_sorted =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.rev (String_Graph.topological_order locales_Graph)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales = List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (#1 o #2 o (String_Graph.get_entry locales_Graph))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder locales_sorted

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in theory_of_string (unlines (List.map pretty_as_str

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((List.map (repr_datatype T) datatypes)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (repr_function T) functions)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (repr_class T) classes)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (repr_locale T) locales)))) (Context.parents_of T) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun get_basic_theory_data T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val T' = theory_of_exportable_data T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val cmp = (fn (s,(s1,_)) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (lift fast_string_ord unqualify) (s,s1))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axs = Ord_List.subtract cmp

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord (List.map #1 (axioms_of T')))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1) (axioms_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val thms = Ord_List.subtract cmp

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord (List.map #1 ((thms_of T')@axs)))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1) (thms_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val consts = Ord_List.subtract cmp

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord (List.map #1 (consts_of T')))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1) (consts_of T))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (axs, thms, consts) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun get_theories T =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val Ts = T::(non_image_theories T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.map (fn T =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val name = name_of_theory T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val (axs,thms,consts) = get_basic_theory_data T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val datatypes = datatypes_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions = functions_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes = classes_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales = locales_of T

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (name,axs,thms,consts,datatypes,functions,

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder classes,locales) end) Ts end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* Generate XML Output *)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederstructure XML_Syntax = Legacy_XML_Syntax

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun fixTypeNames moduleName t = case t of

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

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

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

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

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder else (n,s)) a),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.map (fixTypeNames moduleName) c)

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

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

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | _ => t

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

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

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun mixfix_to_args m = case m of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME(Mixfix.Infixl (s,j)) => [("infixl",s), ("mixfix_i",string_of_int j)]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | SOME(Mixfix.Infixr (s,j)) => [("infixr",s), ("mixfix_i",string_of_int j)]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | SOME(Mixfix.Infix (s,j)) => [("infix",s), ("mixifix_i",string_of_int j)]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | _ => []

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_term' T tbl t = case t of

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Const",a),t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan 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

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME(mx) => mixfix_to_args (SOME mx)

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

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

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

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | _ => t

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_term T t = xml_of_term' T Symtab.empty

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (XML_Syntax.xml_of_term t)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_datatype T eqs = XML.Elem (("RecDatatypes",[]),List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn (name,type_params,constructors) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Datatype",[("name",Long_Name.base_name name)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map XML_Syntax.xml_of_type type_params)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn (s,tps) => XML.Elem

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Constructor",[("name",Long_Name.base_name s)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.map XML_Syntax.xml_of_type tps))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder constructors))) eqs)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_function T (name,tp,def_eqs) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Function",[("name",Long_Name.base_name name)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (XML_Syntax.xml_of_type tp)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ::(List.map(fn (pats,tm) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Equations",[]),List.map (xml_of_term T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (pats@[tm]))) def_eqs))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_class T (name,parents,assumps,fixes) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("ClassDef",[("name",Long_Name.base_name name)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn p =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn (s,t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [xml_of_term T t])) assumps)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn (s,t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("ClassParam",[("name",Long_Name.base_name s)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [XML_Syntax.xml_of_type t])) fixes))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_locale T (name,fixes,assumps,thms,parents) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Locale",[("name",Long_Name.base_name name)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn ((s,t),m) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("LocaleParam",[("name",Long_Name.base_name s)]

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(mixfix_to_args (SOME m))),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [XML_Syntax.xml_of_type t])) fixes)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn (s,t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [xml_of_term T t])) assumps)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn (s,t) =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Theorem",[("name",Long_Name.base_name s)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [xml_of_term T t])) thms)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn p =>

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_theory (name, axs, thms, cs, dts, fns, cls, locales) =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val T = theory_by_name name

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val imports = List.map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn T => XML.Elem (("Import",[("name",name_of_theory T)]),[]))

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Context.parents_of T)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms = List.map (fn (n,t) => XML.Elem

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Axiom",[("name",Long_Name.base_name n)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [(xml_of_term T o prettify_term) t])) axs

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theorems = List.map (fn (n,t) => XML.Elem

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Theorem",[("name",Long_Name.base_name n)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [(xml_of_term T o prettify_term) t])) thms

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val consts = List.map (fn (n,tp) => XML.Elem

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Const",[("name",Long_Name.base_name n)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [XML_Syntax.xml_of_type tp])) cs

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val datatypes = List.map (xml_of_datatype T) dts

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions = List.map (xml_of_function T) fns

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes = List.map (xml_of_class T) cls

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales' = List.map (xml_of_locale T) locales

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in fixTypeNames name (XML.Elem (("IsaTheory",[("name",name)]),

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder imports@axioms@theorems@consts@datatypes

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @functions@classes@locales')) end

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_theories theories =

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("IsaExport",[]),List.map xml_of_theory theories)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederend;