eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maedersignature ExportHelper =

4e2331b387b90a234dc36b12c778914d3e202718Christian Maedersig

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski (* types *)

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder type named_term = (string * term)

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder (* general helper functions *)

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder val unlines : string list -> string

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val unqualify : string -> string

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (* isabelle specific functions *)

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val theory_of_string : string -> theory list -> theory

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski val theory_by_name : string -> theory

49588f3d624e56594d888bc622bc90618ae3c2c5Till Mossakowski val name_of_theory : theory -> string

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski val axioms_of : theory -> named_term list

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val non_image_theories : theory -> theory list

49588f3d624e56594d888bc622bc90618ae3c2c5Till Mossakowski val thms_of : theory -> named_term list

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val consts_of : theory -> (string * typ) list

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val datatypes_of : theory -> ((string * typ list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (string * typ list) list) list) list

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (* mutually_rec_types@(name * type_params *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder constructors@(constructor_name * type_args))) *)

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val functions_of : theory -> (string * typ *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (term list * term) list) list

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (* name * type *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder def_eqs@(pats * defterm) *)

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val classes_of : theory -> (class * string list *

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich (string * term) list *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (string * typ) list) list

1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder (* name * parents * assumes * fixes *)

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder val locales_of : theory -> (string *

2272b992302eb61b2a039033cb8cdaf7809fe682Christian Maeder ((string * typ) * mixfix) list *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder named_term list * named_term list *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder string list) list

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (* name * fixes * in-locale axioms *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder ex-locale axioms * parents *)

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder val pretty_as_str : Pretty.T -> string

2272b992302eb61b2a039033cb8cdaf7809fe682Christian Maeder val repr_term : theory -> term -> Pretty.T

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich val repr_typ : theory -> typ -> Pretty.T

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder val repr_name : string -> Pretty.T

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder val repr_function : theory -> (string * typ *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (term list * term) list) -> Pretty.T

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder val repr_class : theory -> (class * string list *

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder (string * term) list *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (string * typ) list) -> Pretty.T

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder val repr_locale : theory -> (string *

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder ((string * typ) * mixfix) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder named_term list * named_term list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder string list) -> Pretty.T

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val repr_datatype : theory -> (string * typ list * (string *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder typ list) list) list -> Pretty.T

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder val theory_of_exportable_data : theory -> theory

7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder val get_basic_theory_data : theory -> (named_term list *

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich named_term list *

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (string * typ) list)

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (* axioms * theorems * consts *)

e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9Christian Maeder type theory_data = (string * named_term list * named_term list *

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (string * typ) list * ((string * typ list *

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (string * typ list) list) list) list *

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe (string * typ * (term list * term) list) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (class * string list * (string * term) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (string * typ) list) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (string * ((string * typ) * mixfix) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder named_term list * named_term list *

ef7d1a1d5454458d46b9acefeda94b12bdc695b2Christian Maeder string list) list)

2de8dfc30c926ee27254bfa32230a01435530efeKlaus Luettich (* name * axioms * theorems * consts * datatypes *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder functions * classes * locales *)

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder val get_theories : theory -> theory_data list

54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder val xml_of_theories : theory_data list -> XML.tree

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder exception ExportError of string

4e2331b387b90a234dc36b12c778914d3e202718Christian Maederend;

2de8dfc30c926ee27254bfa32230a01435530efeKlaus Luettich

4e2331b387b90a234dc36b12c778914d3e202718Christian Maederstructure ExportHelper : ExportHelper =

4e2331b387b90a234dc36b12c778914d3e202718Christian Maederstruct

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder

54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederexception ExportError of string

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder

4e2331b387b90a234dc36b12c778914d3e202718Christian Maedertype named_term = string * term

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maedertype theory_data = (string * named_term list * named_term list *

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich (string * typ) list * ((string * typ list *

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich (string * typ list) list) list) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (string * typ * (term list * term) list) list *

da955132262baab309a50fdffe228c9efe68251dCui Jian (class * string list * (string * term) list *

f64f3dc78de82101483fe97bf109a42ca4d59d77Klaus Luettich (string * typ) list) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder (string * ((string * typ) * mixfix) list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder named_term list * named_term list *

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder string list) list)

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder (* name * axioms * theorems * consts * datatypes *

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich functions * classes * locales *)

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich(* ------------------------------ General helper functions *)

da955132262baab309a50fdffe228c9efe68251dCui Jian

f64f3dc78de82101483fe97bf109a42ca4d59d77Klaus Luettichval unlines = String.concatWith (String.str (Char.chr 10))

da955132262baab309a50fdffe228c9efe68251dCui Jian

4e2331b387b90a234dc36b12c778914d3e202718Christian Maederfun lift f sel = fn (t1,t2) => f (sel t1,sel t2)

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich

da955132262baab309a50fdffe228c9efe68251dCui Jianfun unqualify n = if Long_Name.is_qualified n

99634745e86bb1c79da4e2b376e580f65ee67082Klaus Luettich then (Long_Name.implode (List.tl (Long_Name.explode n)))

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maeder else n

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maeder

0ee3933098d65199ae39ea41cfc62634226dad15Klaus Luettich(* ------------------------------ Isabelle specific functions *)

04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder(* Keep track of the number of theories created from a string *)

4e2331b387b90a234dc36b12c778914d3e202718Christian Maederval thmNum = Unsynchronized.ref 0

ebdce567033765c1f16ccf25d721c02986a5da33Klaus Luettich

63324a97283728a30932828a612c7b0b0f687624Christian Maeder(* create a theory from a string of its body *)

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maederfun theory_of_string body parents =

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder let val name = "TempTheory"^Int.toString (Unsynchronized.inc thmNum)

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich val header = Thy_Header.make ("TempTheory",Position.none) [] [] []

edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian val text = unlines ["theory "^name,"begin",body,"end"]

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder in #1 (Thy_Load.load_thy 0 (Thy_Load.get_master_path ()) header

ef7d1a1d5454458d46b9acefeda94b12bdc695b2Christian Maeder Position.start text parents) end

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettichfun remove_hol_true_prop t = case t of

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder op$ (Const ("HOL.Trueprop",_), tm) => tm

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder | tm => tm

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder

7bf4436b6f9987b070033a323757b206c898c1beChristian Maederval prettify_term = Logic.strip_imp_concl o remove_hol_true_prop

63324a97283728a30932828a612c7b0b0f687624Christian Maeder

63324a97283728a30932828a612c7b0b0f687624Christian Maeder(* remove data that is already present in a parent theory *)

63324a97283728a30932828a612c7b0b0f687624Christian Maederfun remove_parent_data df cmp T =

7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder let val d = df T

7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder val pd = (List.foldl op@ [] (List.map df (Context.parents_of T)))

33c33fde308de14d34177617a28524312f5f0ad8Christian Maeder in Ord_List.subtract cmp (Ord_List.make cmp pd) (Ord_List.make cmp d) end

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder

04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder(* a couple of aliases *)

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maederval theory_by_name = Thy_Info.get_theory

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maederval name_of_theory = Context.theory_name

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maederval axioms_of = Theory.axioms_of

7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder

63324a97283728a30932828a612c7b0b0f687624Christian Maeder(* check if the theory is not part of the logic image *)

63324a97283728a30932828a612c7b0b0f687624Christian Maederfun is_non_image_theory T = length (Thy_Info.loaded_files (name_of_theory T)) > 0

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maeder

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maederfun non_image_theories T = List.concat (List.map

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maeder (fn T' => if is_non_image_theory T'

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maeder then T'::(non_image_theories T') else [])

63324a97283728a30932828a612c7b0b0f687624Christian Maeder (Context.parents_of T))

63324a97283728a30932828a612c7b0b0f687624Christian Maeder

63324a97283728a30932828a612c7b0b0f687624Christian Maederfun hol_forall_elim tm =

63324a97283728a30932828a612c7b0b0f687624Christian Maeder let val qnt = #1 (Term.dest_Const (HOLogic.all_const HOLogic.boolT))

209f37a7f7b3c61e5dc1a90bd83b65a24c8be3faChristian Maeder val body = Term.strip_qnt_body qnt tm

63324a97283728a30932828a612c7b0b0f687624Christian Maeder val vars = List.map (fn (s,tp) => Var ((s,0),tp))

cc77993cd3db08f4d731a3c218c2a03b547b8da8Christian Maeder (Term.strip_qnt_vars qnt tm)

4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder in Term.subst_bounds (List.rev vars, body) end

04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder

04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maederfun hol_conjunctions tm = case HOLogic.dest_conj tm of

63324a97283728a30932828a612c7b0b0f687624Christian Maeder [_] => [tm]

7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder | tms => List.concat (List.map hol_conjunctions tms)

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich

f64f3dc78de82101483fe97bf109a42ca4d59d77Klaus Luettichfun thms_of T = List.map (fn (s,d) => (s,prop_of d))

64325303fc09fc4d88ced49be11ff2d29966422aCui Jian (remove_parent_data Global_Theory.all_thms_of

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich (lift fast_string_ord #1) T)

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe(* currently there seems to be no way (anymore) to

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe attach any terms to a const directly. Thus the discarded

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe part is (hopefully) always NONE

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich todo: maybe throw an exception if this is not the case? *)

64325303fc09fc4d88ced49be11ff2d29966422aCui Jianfun consts_of T =

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe (((Name_Space.dest_table (Syntax.init_pretty_global T)) o

fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder #constants o Consts.dest o Sign.consts_of) T)

0ee3933098d65199ae39ea41cfc62634226dad15Klaus Luettich in remove_parent_data get_consts (lift fast_string_ord #1) T end

7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder

709653bffee501341e2fdc55b9223e4921047c65Till Mossakowskifun datatypes_of T =

709653bffee501341e2fdc55b9223e4921047c65Till Mossakowski let val get_datatypes = (#log_types o Type.rep_tsig o Sign.tsig_of)

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich val ts = remove_parent_data get_datatypes fast_string_ord T

5efed683fd173e9d53bd5f1929ba5b0c8a228710Christian Maeder val is_mutually_rec_type = fn (_,i) => length (#descr i) >1

17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder val check_rec = fn (n,v) => if is_mutually_rec_type (n,v)

64325303fc09fc4d88ced49be11ff2d29966422aCui Jian then (#index v) < 1 else true

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski val rec dtyp2typ = fn (descs,t) => case t of

64325303fc09fc4d88ced49be11ff2d29966422aCui Jian Datatype.DtTFree (s,srt) => TFree (s,srt)

c1f29a0f0c0b83858e7e57668dac254504f213b6Christian Maeder | Datatype.DtType (s,ts) =>

afe76697dd6888856a066934a1112a38809b27faChristian Maeder Type (s,List.map (curry dtyp2typ descs) ts)

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski | Datatype.DtRec i =>

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski case List.find (curry op= i o #1) descs of

d19b839f3726cc508e3c52a7af227167a9e38f45Klaus Luettich SOME (_,(s,ts,_)) => Type (s, List.map

da955132262baab309a50fdffe228c9efe68251dCui Jian (curry dtyp2typ descs) ts)

63324a97283728a30932828a612c7b0b0f687624Christian Maeder | NONE => raise ExportError("Internal Error!")

63324a97283728a30932828a612c7b0b0f687624Christian Maeder val dt_desc = fn info => List.map (fn (i,(s,vs,eqs)) =>

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich let val vs' = List.map (curry dtyp2typ info) vs

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich val eqs' = List.map (fn (s,ts) =>

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (s,List.map (curry dtyp2typ info) ts)) eqs

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich in (s,vs',eqs') end) info

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich in List.foldl (fn (n,l) => case Datatype.get_info T n of

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich SOME(v) => if check_rec (n,v)

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich then (dt_desc (#descr v))::l

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich else l

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich | NONE => l) [] ts end

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder(* Notes:

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe HOLogic is in HOL/Tools/hologic.ML

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich dest_Const is in Pure/term.ML

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe Logic is in Pure/logic.ML *)

da955132262baab309a50fdffe228c9efe68251dCui Jian

da955132262baab309a50fdffe228c9efe68251dCui Jianval functions_of =

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich let val get_funs = fn T =>

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich let val d = Item_Net.content (Function_Common.get_function

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (Proof_Context.init_global T))

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich val fun_def = (fn (pats,def) => (#2 (strip_comb pats),def))

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich o HOLogic.dest_eq o HOLogic.dest_Trueprop o #2

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich o Logic.dest_implies o prop_of

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich in List.map (fn (c,i) => case dest_Const c of

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (n,t) => (n,t,List.map fun_def (#psimps i))) d end

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich in remove_parent_data get_funs (lift fast_string_ord #1) end

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maederfun classes_of T =

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich let val cls_suffix = "_class_def"

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich val thms = thms_of T

da955132262baab309a50fdffe228c9efe68251dCui Jian val cls_names = List.map (fn n => String.substring (n,0,String.size n-

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich String.size cls_suffix)) (List.filter (String.isSuffix cls_suffix)

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich (List.map #1 thms))

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich in List.map (fn name =>

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder let val i = AxClass.get_info T name

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich val parents' = List.concat (List.map

833baa690207430f9cc3ca599039954a7840fa30Klaus Luettich (fn tm => Term.add_const_names tm [])

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder ((Logic.dest_conjunction_list o #2

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich o Logic.dest_equals o Thm.prop_of o #def) i))

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich val parents = List.map (fn n => String.substring

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (n,0,String.size n - String.size "_class"))

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (List.filter (fn n => (String.isSuffix "_class" n) andalso

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (not (String.isPrefix "HOL" n))) parents')

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich o Logic.dest_implies) t))

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (List.filter ((String.isPrefix (name^".")) o #1) thms)

5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361acKlaus Luettich (* note: instead of cls_names we should only use

eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder ancestors of the class *)

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe val all_params = List.map (fn (s,t) => (Long_Name.base_name s,t))

7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich (List.concat (List.map (#params o AxClass.get_info T) cls_names))

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params

7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))

fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder axioms'

fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder in (name,parents,axioms,#params i) end) cls_names end

fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbefun locales_of T =

fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder let val all_locales = fn T => List.map (fn l => (#name l, #parents l))

fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder (Locale.pretty_locale_deps T)

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe val locales = Ord_List.subtract

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe (fn (c,l) => fast_string_ord (#1 c,#1 l))

d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe (Ord_List.make (lift fast_string_ord #1)

33fc94b09b906329ca7505caa1ddcddf67e3f8daTill Mossakowski (classes_of T))

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (Ord_List.make (lift fast_string_ord #1)

(remove_parent_data all_locales

(lift fast_string_ord #1) T))

in List.map (fn (name,ps) =>

let val parent_params = List.map (#1 o #1) (List.concat

(List.map (Locale.params_of T o #1)

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

val params = Ord_List.subtract (fn (s,((s1,_),_)) =>

fast_string_ord (s,s1))

(Ord_List.make fast_string_ord parent_params)

(Ord_List.make (lift fast_string_ord (#1 o #1))

(Locale.params_of T name))

val filter = ["_axioms.intro","_axioms_def","_def",".intro",".axioms_"]

val axs = List.filter ((String.isPrefix name) o #1)

(Global_Theory.all_thms_of T)

val axioms' = List.filter

(fn t => (not (List.exists

(fn s => String.isPrefix (name ^ s) (#1 t))

filter))) axs

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

o Logic.dest_implies

o Thm.prop_of) t)) axioms'

val fix_consts = List.map (fn (s,t) => (s, Term.subst_Vars

(List.map (fn ((s,tp),_) =>

((s,0),Const (s,tp))) params) t))

val parse_axioms = fn v => List.map hol_forall_elim

((hol_conjunctions o #2 o Logic.dest_equals o Thm.prop_of o #2) v)

val in_locale_axioms =

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

SOME v => parse_axioms v

| _ =>

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

SOME v => parse_axioms v

| _ => []

val in_loc = List.filter (fn (_,t) =>

List.exists (fn t' => t = t') in_locale_axioms) axioms

val ex_loc = List.filter (fn (_,t) =>

not (List.exists (fn t' => t = t') in_locale_axioms)) axioms

in (name,params,fix_consts in_loc,fix_consts ex_loc,ps) end) locales end

(* ------------------------------ Represent as string *)

fun pretty_as_str p = Pretty.str_of p

fun repr_term T =

let val ctxt = Config.put Printer.show_question_marks false

(Proof_Context.init_global T)

in Syntax.pretty_term ctxt end

fun repr_typ T = Syntax.pretty_typ (Proof_Context.init_global T)

fun repr_name n' =

let val n = Long_Name.base_name n'

in if String.isSubstring " " n then Pretty.quote (Pretty.str n)

else Pretty.str n end

fun repr_function T (s,tp,def_eqs) =

let val head = [Pretty.str "fun ", repr_name s, Pretty.str " :: ",

Pretty.quote (repr_typ T tp), Pretty.str " where "]

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

((Pretty.breaks ([repr_name s]

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

pats)))@

[Pretty.str " = ",repr_term T tm]))) def_eqs

in Pretty.block (head@Pretty.separate " | " body) end

fun repr_class T (s,ps,assumes,fixes) =

let val head = [Pretty.str "class", repr_name s]

@(if length fixes + length assumes + length ps > 0

then [Pretty.str "="] else [])

val parents = List.map repr_name ps

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

[repr_name s,Pretty.str "::",

Pretty.quote (repr_typ T tp)])) fixes

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

[repr_name s, Pretty.str ":",

Pretty.quote (repr_term T tm)])) assumes

in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@

(if length (fixes'@assumes') > 0 andalso length parents > 0

then [Pretty.str "+"] else [])@

(if length fixes' > 0

then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@

(if length assumes' > 0

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

fun repr_locale T (s,fixes,in_loc,_,ps) =

let val head = [Pretty.str "locale", repr_name s]

@(if length fixes + length in_loc + length ps > 0

then [Pretty.str "="] else [])

val parents = List.map repr_name ps

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

[Pretty.str s,Pretty.str "::",

Pretty.quote (repr_typ T tp)])) fixes

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

[repr_name s, Pretty.str ":",

Pretty.quote (repr_term T tm)])) in_loc

in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@

(if length (fixes'@assumes') > 0 andalso length parents > 0

then [Pretty.str "+"] else [])@

(if length fixes' > 0

then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@

(if length assumes' > 0

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

fun repr_datatype T d =

let val dts = List.map (fn (s,vs,eqs) =>

let val vs' = Pretty.enclose "(" ")"

(Pretty.separate "," (List.map (repr_typ T) vs))

val eqs' = Pretty.separate "|" (List.map

(fn (s,vs) => Pretty.block (Pretty.breaks

([repr_name s]@

(List.map (Pretty.quote o repr_typ T) vs)))) eqs)

in Pretty.block (Pretty.breaks

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

in (Pretty.block o Pretty.breaks) ([Pretty.str "datatype"]@

Pretty.separate "and" dts) end

fun theory_of_exportable_data T =

let val datatypes = datatypes_of T

val functions = functions_of T

val classes_Graph = String_Graph.make

(List.map (fn l => ((#1 l,l),#2 l)) (classes_of T))

val classes_sorted =

List.rev (String_Graph.topological_order classes_Graph)

val classes = List.map

(#1 o #2 o (String_Graph.get_entry classes_Graph))

classes_sorted

val locales_Graph = String_Graph.make

(List.map (fn l => ((#1 l,l),#5 l)) (locales_of T))

val locales_sorted =

List.rev (String_Graph.topological_order locales_Graph)

val locales = List.map

(#1 o #2 o (String_Graph.get_entry locales_Graph))

locales_sorted

in theory_of_string (unlines (List.map pretty_as_str

((List.map (repr_datatype T) datatypes)

@(List.map (repr_function T) functions)

@(List.map (repr_class T) classes)

@(List.map (repr_locale T) locales)))) (Context.parents_of T) end

fun get_basic_theory_data T =

let val T' = theory_of_exportable_data T

val cmp = (fn (s,(s1,_)) =>

(lift fast_string_ord unqualify) (s,s1))

val axs = Ord_List.subtract cmp

(Ord_List.make fast_string_ord (List.map #1 (axioms_of T')))

(Ord_List.make (lift fast_string_ord #1) (axioms_of T))

val thms = Ord_List.subtract cmp

(Ord_List.make fast_string_ord (List.map #1 ((thms_of T')@axs)))

(Ord_List.make (lift fast_string_ord #1) (thms_of T))

val consts = Ord_List.subtract cmp

(Ord_List.make fast_string_ord (List.map #1 (consts_of T')))

(Ord_List.make (lift fast_string_ord #1) (consts_of T))

in (axs, thms, consts) end

fun get_theories T =

let val Ts = T::(non_image_theories T)

in List.map (fn T =>

let val name = name_of_theory T

val (axs,thms,consts) = get_basic_theory_data T

val datatypes = datatypes_of T

val functions = functions_of T

val classes = classes_of T

val locales = locales_of T

in (name,axs,thms,consts,datatypes,functions,

classes,locales) end) Ts end

(* Generate XML Output *)

structure XML_Syntax = Legacy_XML_Syntax

fun fixTypeNames moduleName t = case t of

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

List.map (fn (n,s) =>

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

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

else (n,s)) a),

List.map (fixTypeNames moduleName) c)

| XML.Elem (d,c) =>

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

| _ => t

(* Enrich the (isabelle-builtin) XML representation of terms with infix information *)

fun mixfix_to_args m = case m of

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

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

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

| _ => []

fun xml_of_term' T tbl t = case t of

XML.Elem (("Const",a),t) =>

let val b = case (Syntax.guess_infix (Sign.syn_of T)

(Lexicon.mark_const ((#2 o List.hd) a))) of

SOME(mx) => mixfix_to_args (SOME mx)

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

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

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

| _ => t

fun xml_of_term T t = xml_of_term' T Symtab.empty

(XML_Syntax.xml_of_term t)

fun xml_of_datatype T eqs = XML.Elem (("RecDatatypes",[]),List.map

(fn (name,type_params,constructors) =>

XML.Elem (("Datatype",[("name",Long_Name.base_name name)]),

(List.map XML_Syntax.xml_of_type type_params)

@(List.map (fn (s,tps) => XML.Elem

(("Constructor",[("name",Long_Name.base_name s)]),

List.map XML_Syntax.xml_of_type tps))

constructors))) eqs)

fun xml_of_function T (name,tp,def_eqs) =

XML.Elem (("Function",[("name",Long_Name.base_name name)]),

(XML_Syntax.xml_of_type tp)

::(List.map(fn (pats,tm) =>

XML.Elem (("Equations",[]),List.map (xml_of_term T)

(pats@[tm]))) def_eqs))

fun xml_of_class T (name,parents,assumps,fixes) =

XML.Elem (("ClassDef",[("name",Long_Name.base_name name)]),

(List.map (fn p =>

XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents)

@(List.map (fn (s,t) =>

XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),

[xml_of_term T t])) assumps)

@(List.map (fn (s,t) =>

XML.Elem (("ClassParam",[("name",Long_Name.base_name s)]),

[XML_Syntax.xml_of_type t])) fixes))

fun xml_of_locale T (name,fixes,assumps,thms,parents) =

XML.Elem (("Locale",[("name",Long_Name.base_name name)]),

(List.map (fn ((s,t),m) =>

XML.Elem (("LocaleParam",[("name",Long_Name.base_name s)]

@(mixfix_to_args (SOME m))),

[XML_Syntax.xml_of_type t])) fixes)

@(List.map (fn (s,t) =>

XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),

[xml_of_term T t])) assumps)

@(List.map (fn (s,t) =>

XML.Elem (("Theorem",[("name",Long_Name.base_name s)]),

[xml_of_term T t])) thms)

@(List.map (fn p =>

XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents))

fun xml_of_theory (name, axs, thms, cs, dts, fns, cls, locales) =

let val T = theory_by_name name

val imports = List.map

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

(Context.parents_of T)

val axioms = List.map (fn (n,t) => XML.Elem

(("Axiom",[("name",Long_Name.base_name n)]),

[(xml_of_term T o prettify_term) t])) axs

val theorems = List.map (fn (n,t) => XML.Elem

(("Theorem",[("name",Long_Name.base_name n)]),

[(xml_of_term T o prettify_term) t])) thms

val consts = List.map (fn (n,tp) => XML.Elem

(("Const",[("name",Long_Name.base_name n)]),

[XML_Syntax.xml_of_type tp])) cs

val datatypes = List.map (xml_of_datatype T) dts

val functions = List.map (xml_of_function T) fns

val classes = List.map (xml_of_class T) cls

val locales' = List.map (xml_of_locale T) locales

in fixTypeNames name (XML.Elem (("IsaTheory",[("name",name)]),

imports@axioms@theorems@consts@datatypes

@functions@classes@locales')) end

fun xml_of_theories theories =

XML.Elem (("IsaExport",[]),List.map xml_of_theory theories)

end;