5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisignature ExportHelper =

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisig

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski type const_info = (string * (typ * term option)) list

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski type term_info = (string * term) list

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type datatype_info = (string * Datatype.info) list

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type class_info = (string * (string list) * term_info *

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ((string * typ) list)) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* name * parents * assumes * fixes *)

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich type locale_info = (string * ((string * typ) * mixfix) list

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (* name * fixes *)

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich * (string * term) list * (string * term) list

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (* in-locale axioms * ex-locale axioms *)

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich * string list) list

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (* parents *)

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich type theory_info =

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich string (* theory name *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * string list (* imports *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * const_info (* constants *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * term_info (* axioms *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * term_info (* theorems *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski * datatype_info (* data types *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski * class_info (* class info *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski * locale_info (* locale info *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski exception ExportError of string

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val theory_info : theory -> theory_info

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val tinfo2xml : theory -> string -> theory_info -> XML.tree

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiend;

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructure ExportHelper : ExportHelper =

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistruct

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(* Types *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type const_info = (string * (typ * term option)) list

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder type term_info = (string * term) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type datatype_info = (string * Datatype.info) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type class_info = (string * (string list) * term_info *

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ((string * typ) list)) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* name * parents * assumes * fixes *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type locale_info = (string * ((string * typ) * mixfix) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* name * fixes *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski * (string * term) list * (string * term) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* in-locale axioms * ex-locale axioms *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski * string list) list

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* parents *)

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type theory_info =

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski string (* theory name *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * string list (* imports *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * const_info (* constants *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * term_info (* axioms *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * term_info (* theorems *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * datatype_info (* data types *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * class_info (* class info *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * locale_info (* locale info *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski exception ExportError of string

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* General helper functions *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun internal_error s = raise (ExportError s)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun id x = x

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun mergesort _ [] = []

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | mergesort _ [x] = [x]

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | mergesort cmp_data xs =

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val (ys,zs) =

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski List.foldl (fn(i, (ys,zs)) => (zs, i::ys)) ([],[]) xs

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun merge (xs,[]) = xs

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | merge ([],xs) = xs

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | merge (x::xr,y::yr) = if (cmp_data x) <= (cmp_data y)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then x::merge(xr,y::yr)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else y::merge(x::xr,yr)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in merge(mergesort cmp_data ys, mergesort cmp_data zs) end

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* remove duplicate entries from a sorted list *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun unique [] = []

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | unique [x] = [x]

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | unique (x1::x2::xr) = if x1 = x2

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then unique (x2::xr)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else x1::(unique (x2::xr))

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* remove xs from ys - both lists need to be sorted asc *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun remove' _ _ ([],ys) = ys

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | remove' _ _ (_,[]) = []

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | remove' cd1 cd2 (x::xr,y::yr) =

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski if (cd1 x) < (cd2 y)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then remove' cd1 cd2 (xr,y::yr)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else if (cd2 y) < (cd1 x)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then y::(remove' cd1 cd2 (x::xr,yr))

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else remove' cd1 cd2 (xr,yr)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun remove cmp_data = remove' cmp_data cmp_data

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun remove_parent_data df cmp_data T =

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich let val d = df T

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich val pd = (List.foldl op@ [] (map df (Context.parents_of T)))

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in remove cmp_data (mergesort cmp_data pd,mergesort cmp_data d) end

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun filter rem (d : (string * 'a) list) =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski remove' id #1 ((mergesort id rem),(mergesort #1 d))

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(* Theory-specific helpers *)

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* remove unnecessary information from (recursive) datatypes *)

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun is_mutually_rec_type (_,i) = length (#descr i) > 1

65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke fun check_rec (n,v) = if is_mutually_rec_type (n,v)

65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke then (#index v) < 1

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else true

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun restructure_rec_types ts = List.foldl (fn (d,l) => case d of

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (n,SOME(v)) => if check_rec (n,v) then (n,v)::l

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else l

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | (_,NONE) => l) [] ts

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun unfold_conjunction tm =

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski case tm of

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Const ("Pure.conjunction",_)) $ t => unfold_conjunction t

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | t $ (Const ("Pure.conjunction",_)) => unfold_conjunction t

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | t1 $ t2 =>

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (unfold_conjunction t1)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski @(unfold_conjunction t2)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | _ => [tm]

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun unfold_hol_conjunction tm = case tm of

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Const ("HOL.conj",_) $ t $ t1 => (unfold_hol_conjunction t)@(unfold_hol_conjunction t1)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | Const ("HOL.conj",_) $ t => [t]

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | _ => [tm]

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun strip_hol_all l b tm = case (b,tm) of

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (true,Const ("HOL.All",_) $ Abs (s,t,tm)) =>

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski strip_hol_all ((s,t)::l) true tm

a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski | (_,Bound i) => if List.length l > i

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then let val (s,t) = List.nth(l,i)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in Var ((s,0),t) end

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else tm

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | (_,Abs (s,t,tm)) => Abs (s,t,strip_hol_all l false tm)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | (_,t1 $ t2) => (strip_hol_all l false t1) $

d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (strip_hol_all l false t2)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | _ => tm

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun remove_hol_true_prop t = case t of

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski op$ (Const ("HOL.Trueprop",_), tm) => tm

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)

f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski | tm => tm

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* get raw theory information *)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun get_consts T =

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val consts_of = (Name_Space.dest_table (Syntax.init_pretty_global T)) o

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder #constants o Consts.dest o Sign.consts_of

c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maeder in remove_parent_data consts_of #1 T end

e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski val get_axioms = remove_parent_data Theory.axioms_of #1

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski val get_theorems =

464c78620a182d2e8fbd125098045eae8788e2bdTill Mossakowski let fun theorems_of T = map (fn (a,b) => (a, prop_of b))

12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski (Global_Theory.all_thms_of T)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in remove_parent_data theorems_of #1 end

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun get_datatypes T =

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val tname = Context.theory_name T

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val tl = String.size tname

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val ts = (#log_types o Type.rep_tsig o Sign.tsig_of) T

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val ts' = map (fn s => (String.extract (s,tl+1,NONE),Datatype.get_info T s))

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (List.filter (String.isPrefix tname) ts)

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski in restructure_rec_types ts' end

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski fun get_classes T thms =

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski let val cls_suffix = "_class_def"

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski val cls_names = List.map (fn n => String.substring

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (n,0,String.size n-String.size cls_suffix))

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (List.filter (fn n =>

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski if String.isSuffix cls_suffix n

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski then true else false) (List.map #1 thms))

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski in List.map (fn name =>

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski let val name' = String.substring (name,String.size "Class.",

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski String.size name - String.size "Class.")

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski val i = AxClass.get_info T name

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski val parents = let fun split tms = case tms of

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (Const ("HOL.Trueprop",_))::_ => []

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | (Const ("TYPE",_))::tms' => (split tms')

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | (Const (s,_))::tms' => let val s' =

65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke if String.isPrefix "Class." s

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski then String.substring (s,String.size "Class.",

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski String.size s - String.size "Class."

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski - String.size "_class")

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski else s

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski in s'::(split tms') end

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | _::tms' => (split tms')

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | [] => []

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski in case (Thm.prop_of o #def) i of

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski _ $ t => (split o unfold_conjunction) t

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | _ => [] end

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski val axioms' = List.filter

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (fn (n,_) => String.isPrefix (name^".") n) thms

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski val axioms = List.map (fn (n,t) => case t of

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski _ $ (_ $ t') => (n,t')

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | _ => (n,t)) axioms'

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski val params = #params i

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski in (name',parents,axioms,params) end) cls_names end

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski fun fix_consts' params t = case t of

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski Var ((s,_),_) => (case List.find (fn ((s',_),_) => s'=s) params of

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski SOME ((s,tp),_) => Const (s,tp)

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | NONE => t)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | Abs (s,tp,tm) => Abs (s,tp,fix_consts' params tm)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | t1 $ t2 => (fix_consts' params t1) $ (fix_consts' params t2)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | _ => t

30256573a343132354b122097b0ee1215dda1364Till Mossakowski fun fix_consts params ts = List.map (fn (s,t) =>

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (s,fix_consts' params t)) ts

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder fun get_locales T thms =

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder let val cls_suffix = "_class_def"

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder val cls_names = List.map (fn n => String.substring

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (n,0,String.size n-String.size cls_suffix))

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (List.filter (fn n =>

30256573a343132354b122097b0ee1215dda1364Till Mossakowski if String.isSuffix cls_suffix n

30256573a343132354b122097b0ee1215dda1364Till Mossakowski then true else false) (List.map #1 thms))

30256573a343132354b122097b0ee1215dda1364Till Mossakowski val names' = List.filter (String.isPrefix (Context.theory_name T))

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (Locale.all_locales T)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski val names = List.filter

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (fn s => not (List.exists (fn s' => s = s') cls_names)) names'

30256573a343132354b122097b0ee1215dda1364Till Mossakowski val (_,tb) = Locale.locale_deps T

30256573a343132354b122097b0ee1215dda1364Till Mossakowski val tb_list = List.map (fn (k,t) =>

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (k,Symtab.dest t)) (Symtab.dest tb)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski val parents = List.foldl (fn ((s,l),t') =>

30256573a343132354b122097b0ee1215dda1364Till Mossakowski List.foldl (fn ((s1,l1),t) => Symtab.map_default (s1,([],[]))

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (fn (parents,pfixes) => (s::parents,(

30256573a343132354b122097b0ee1215dda1364Till Mossakowski ((List.map (fn Free (s,_) => s | _ =>

30256573a343132354b122097b0ee1215dda1364Till Mossakowski internal_error "ExportHelper.get_locales - Failed to parse fixes"))

30256573a343132354b122097b0ee1215dda1364Till Mossakowski o List.concat) l1)@pfixes)) t

30256573a343132354b122097b0ee1215dda1364Till Mossakowski ) t' l) Symtab.empty tb_list;

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val filter = ["_axioms.intro","_axioms_def",

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski "_def",".intro",".axioms_"]

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in List.map (fn name =>

376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski let val params' = Locale.params_of T name

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val parent_params =

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder case Symtab.lookup parents name of

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME (_,v) => v

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | _ => []

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val params = List.filter (fn ((s,_),_) =>

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski not (List.exists (fn p => p = s) parent_params)) params'

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val axs = List.filter (fn t => String.isPrefix name (#1 t))

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Global_Theory.all_thms_of T)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val axioms' = List.filter

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn t => (not (List.exists

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

3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski filter))) axs

3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski val axioms = List.map (fn (s,t) =>

3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (s,(remove_hol_true_prop o

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (fn Const ("==>",_) $ _ $ t => t

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski | _ => internal_error

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("ExportHelper.get_locales - Failed to parse axioms for locale "^name)) o Thm.prop_of) t))

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski axioms'

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val in_locale_axioms =

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case (List.find (fn x => (#1 x) = (name^"_axioms_def")) axs) of

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski SOME v => List.map (strip_hol_all [] true)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ((unfold_hol_conjunction o

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (fn _ $ _ $ tm => tm

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |_ => internal_error

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("ExportHelper.get_locales - Failed to parse axioms definition for locale "^name)) o Thm.prop_of o #2) v)

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | _ => case (List.find (fn x => (#1 x) = (name^"_def")) axs) of

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski SOME v => List.map (strip_hol_all [] true)

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ((unfold_hol_conjunction o

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn _ $ _ $ tm => tm

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |_ => internal_error

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("ExportHelper.get_locales - Failed to parse axioms definition for locale "^name)) o Thm.prop_of o #2) v)

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | _ => []

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

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

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

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

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val ps = case Symtab.lookup parents name of

f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski SOME(v,_) => v

881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder | _ => []

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder in (name,params,fix_consts params' in_loc,fix_consts params' ex_loc,ps) end

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder ) names end

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder(* Guess the names of generated axioms, consts and theorem *)

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder fun prefix p s = List.map (fn x => p^s^x)

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun postfix s p = List.map (fn x => x^s^p)

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder fun l_to_intl l = List.map Int.toString

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder (List.tl (List.rev (List.foldl

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder (fn (_,x::xs) => (x+1)::x::xs

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder |_ => internal_error

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder "ExportHelper.l_to_intl - Unexpected condition") [0] l)))

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun get_type_names ts =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val rec_types = List.filter check_rec ts

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder val grouped_rec_names = List.map (fn x =>

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder List.map (Long_Name.base_name o #1 o #2) ((#descr o #2) x)) rec_types

3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski val def_names = (List.map (Long_Name.base_name o #1 o #2)

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder (List.concat (List.map (#descr o #2) rec_types)))

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder val all_rec_names = (List.concat grouped_rec_names)@def_names

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder val constructors = List.map #1 (List.concat (List.map (#3 o #2)

0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder (List.concat (List.map (#descr o #2) ts))))

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in (grouped_rec_names,all_rec_names,constructors,def_names) end

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun get_gen_consts T name ts consts =

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let val (grouped_rec_names,all_rec_names,constructors,_) = get_type_names ts

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val rec_names = List.concat grouped_rec_names

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val mutually_rec_names =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.filter (fn x => List.length x > 1) grouped_rec_names

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder val simple_names = List.map List.hd

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (List.filter (fn x => List.length x = 1) grouped_rec_names)

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val locale_names = List.filter

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (String.isPrefix (Context.theory_name T))

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (Locale.all_locales T)

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski in constructors@(prefix name "." (List.concat

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski [prefix "Abs" "_" rec_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "Rep" "_" rec_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.map (fn x => "equal_"^x^"_inst.equal_"^x) all_rec_names,

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder List.concat (List.map (fn x => let val comb = space_implode "_" x

30256573a343132354b122097b0ee1215dda1364Till Mossakowski in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.concat (List.map (fn x => [x^"."^x^"_rec",

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski x^"."^x^"_rec_set",

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski x^"."^x^"_rep_set"]) simple_names),

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.concat (List.map

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (fn x => let val comb = space_implode "_" x

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski in (comb^"."^comb^"_rec_set")::

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (comb^"."^comb^"_rep_set")::(List.concat

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (List.map

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (fn y => [comb^"."^comb^"_rec_"^y,

7a8592051724fa46499bde120f44cdc8db270876Till Mossakowski comb^"."^comb^"_rec_set_"^y,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski comb^"."^comb^"_rep_set_"^y])

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (l_to_intl x))) end) mutually_rec_names)]))

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski @(List.filter (String.isPrefix "Class.") consts)

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski @(List.filter (fn s => List.exists

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (fn l => String.isPrefix l s) locale_names) consts) end

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun get_gen_axioms name ts =

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder let val (grouped_rec_names,_,constructors,def_names) =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski get_type_names ts

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val rec_names = List.concat grouped_rec_names

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val mutually_rec_names = List.filter (fn x => List.length x > 1)

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski grouped_rec_names

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder val simple_names = List.map List.hd

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (List.filter (fn x => List.length x = 1) grouped_rec_names)

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski in (postfix "_" "def" constructors)@(prefix name "." (List.concat

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski [prefix "arity_type" "_" def_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "equal" "_" (postfix "_" "def_raw" def_names),

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "type_definition" "_" rec_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.map (fn x => "equal_"^x^"_inst.equal_"^x^"_def") def_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (postfix "_" "def"

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (List.concat [(List.concat (List.map

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (fn x => let val comb = space_implode "_" x

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder in (comb^"."^comb^"_rec_set")::

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (comb^"."^comb^"_rep_set")::(List.concat

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (List.map

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (fn y => [comb^"."^comb^"_rec_"^y,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski comb^"."^comb^"_rec_set_"^y,

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski comb^"."^comb^"_rep_set_"^y]) (l_to_intl x))) end)

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski mutually_rec_names)),

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski List.concat (List.map (fn x => let val comb = space_implode "_" x

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich List.concat (List.map (fn x => [x^"."^x^"_rec",

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski x^"."^x^"_rec_set",

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder x^"."^x^"_rep_set"]) simple_names)]))])) end

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun get_gen_theorems T name ts ths =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val (grouped_rec_names,_,_,def_names) =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski get_type_names ts

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val rec_names = List.concat grouped_rec_names

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder val mutually_rec_names = List.filter (fn x => List.length x > 1)

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder grouped_rec_names

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val locale_names = List.filter

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (String.isPrefix (Context.theory_name T))

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (Locale.all_locales T)

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder val locale_filter = ["_axioms.intro","_axioms_def","_def","."]

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski in prefix name "." (List.concat

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski [prefix "arity_equal" "_" def_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "arity_type" "_" def_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "type_definition" "_" rec_names,

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "equal" "_" (postfix "_" "def" def_names),

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski prefix "equal" "_" (postfix "_" "def_raw" def_names),

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.map (fn x => "equal_"^x^"_inst.equal_"^x) def_names])

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski @(List.concat (List.map (fn x =>

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski List.filter (String.isPrefix (name^"."^x^".")) ths) (unique (rec_names@def_names))))

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski @(List.concat (List.map (fn x =>

30256573a343132354b122097b0ee1215dda1364Till Mossakowski List.filter (String.isPrefix (name^"."^(space_implode "_" x)^".")) ths)

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder mutually_rec_names))

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski @(List.filter (String.isPrefix "Class.") ths)

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski @(List.filter (fn s => (List.exists

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (fn l => List.exists

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (fn f => String.isPrefix (l^f) s) locale_filter) locale_names)) ths) end

2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich(* Represent collected data as XML *)

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

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fun mixfix_to_args m = case m of

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski SOME(Mixfix.Infixl (s,j)) =>

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder [("infixl",s),

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich ("mixfix_i",string_of_int j)]

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | SOME(Mixfix.Infixr (s,j)) =>

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski [("infixr",s),

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski ("mixfix_i",string_of_int j)]

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | SOME(Mixfix.Infix (s,j)) =>

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski [("infix",s),

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski ("mixifix_i",string_of_int j)]

c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski | _ => []

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun xml_of_term' T tbl t =

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski case t of

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

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

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

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski SOME(mx) => mixfix_to_args (SOME mx)

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

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

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

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | _ => t

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder fun xml_of_term T t = xml_of_term' T Symtab.empty

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (XML_Syntax.xml_of_term t)

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fun termListToXML T section l = XML.Elem ((section,[]),List.map (

38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fn (s,t) => XML.Elem (("Term",[("name",Long_Name.base_name s)]),

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski [xml_of_term T (remove_hol_true_prop t)])) l)

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun termTypListToXML T section l = XML.Elem ((section,[]),List.map (

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fn (s,(t,v)) => let val v' = case v of

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski SOME(tm) => (("Term",[("name",Long_Name.base_name s)]),[xml_of_term T tm])

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | NONE => (("NoTerm",[]),[])

30256573a343132354b122097b0ee1215dda1364Till Mossakowski in XML.Elem (("ConstDecl",[("name",Long_Name.base_name s)]),

30256573a343132354b122097b0ee1215dda1364Till Mossakowski [XML_Syntax.xml_of_type t,XML.Elem v']) end) l)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski fun dtypToXML (Datatype.DtTFree (s,_)) = XML.Elem (("DtTFree",[("s",s)]),[])

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | dtypToXML (Datatype.DtType (s,dtl)) =

30256573a343132354b122097b0ee1215dda1364Till Mossakowski XML.Elem (("DtType",[("s",s)]),List.map dtypToXML dtl)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski | dtypToXML (Datatype.DtRec i) =

30256573a343132354b122097b0ee1215dda1364Till Mossakowski XML.Elem (("DtRec",[("i",Int.toString i)]),[])

30256573a343132354b122097b0ee1215dda1364Till Mossakowski fun constructorToXML (name,dtl) = XML.Elem

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (("Constructor",[("val",Long_Name.base_name name)]),List.map dtypToXML dtl)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski fun typeToXML d = List.map

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (fn (i,(s,vs,dt)) => let val attrs =

30256573a343132354b122097b0ee1215dda1364Till Mossakowski [("i",Int.toString i),("name",Long_Name.base_name s)]

30256573a343132354b122097b0ee1215dda1364Till Mossakowski in XML.Elem (("RecType",attrs),[

30256573a343132354b122097b0ee1215dda1364Till Mossakowski XML.Elem (("Vars",[]),List.map dtypToXML vs),

30256573a343132354b122097b0ee1215dda1364Till Mossakowski XML.Elem (("Constructors",[]),List.map constructorToXML dt)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski ])

30256573a343132354b122097b0ee1215dda1364Till Mossakowski end)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski (#descr d)

30256573a343132354b122097b0ee1215dda1364Till Mossakowski fun typeListToXML section l = XML.Elem ((section,[]),List.map (

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder fn (s,d) => XML.Elem (("TypeDecl",[("name",s)]),typeToXML d)) l)

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(* Prepare data *)

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder (* make sure that type names local to the theory do not

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder have the theory name as prefix

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (because this is not their proper name) *)

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun fixTypeNames moduleName t = case t of

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

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder List.map (fn (n,s) =>

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

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

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder else (n,s)) a),

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski List.map (fixTypeNames moduleName) c)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder | XML.Elem (d,c) =>

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

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder | _ => t

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder(* Module interface *)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder (* collect information necessary to reconstruct the theory *)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder fun theory_info T =

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder let val name = Context.theory_name T

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val imports = List.map

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder Context.theory_name (Theory.parents_of T)

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder val types = get_datatypes T

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val consts = get_consts T

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val thms = get_theorems T

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val axioms = get_axioms T

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val classes = get_classes T thms

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val gen_consts = get_gen_consts T name types (List.map #1 consts)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val gen_thms = get_gen_theorems T name types (List.map #1 thms)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val gen_axioms = (get_gen_axioms name types)@(List.map #1 thms)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val locales = get_locales T thms

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder in (name, imports,

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder (filter gen_consts consts),

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder (filter gen_axioms axioms),

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder (filter gen_thms thms),

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder types,classes,locales) end

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder (* export theory info as xml *)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder fun tinfo2xml T fname (name,imports,consts,axioms,thms,

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski types,classes,locales) =

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder let val b = Long_Name.base_name

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val xml_imports = XML.Elem

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder (("Imports",[]), List.map (fn s => XML.Elem (("Import",[("name",s)]),[])) imports)

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val xml_consts = termTypListToXML T "Consts" consts

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val xml_axioms = termListToXML T "Axioms" axioms

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val xml_theorems = termListToXML T "Theorems" thms

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val xml_types = typeListToXML "Types" types

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder val xml_classes = XML.Elem (("Classes",[]),List.map

7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder (fn (name,parents,axioms,params) =>

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski XML.Elem (("ClassDecl",[("name",name)]),

9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (List.map (fn (s,t) => XML.Elem

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (("Axiom",[("name",Long_Name.base_name s)]),

8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder [xml_of_term T (remove_hol_true_prop t)])) axioms)

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski @((List.map (fn (s,t) => XML.Elem

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (("Param",[("name",Long_Name.base_name s)]),

a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski [XML_Syntax.xml_of_type t])) params))

e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich @(List.map (fn n => XML.Elem

a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski (("Parent",[("name",n)]),[])) parents))) classes)

a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski val xml_locales = XML.Elem (("Locales",[]),List.map

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (name,params,in_loc,ex_loc,parents) =>

5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val tbl = List.foldl (fn (((s,_),m),t) =>

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder Symtab.update (s,m) t)

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder Symtab.empty (Locale.params_of T name) in

91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski XML.Elem (("LocaleDecl",[("name",b name)]),

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

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski XML.Elem (("LocaleParam",[("name",s)]

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski @(mixfix_to_args (SOME m))),

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski [XML_Syntax.xml_of_type t])) params)

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski @(List.map (fn (s,t) => XML.Elem

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski (("IAxiom",[("name",b s)]),

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski [xml_of_term' T tbl (XML_Syntax.xml_of_term t)]))

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski in_loc)

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski @(List.map (fn (s,t) => XML.Elem

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski (("EAxiom",[("name",b s)]),

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski [xml_of_term' T tbl (XML_Syntax.xml_of_term t)]))

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ex_loc)

1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski @(List.map (fn n => XML.Elem

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (("Parent",[("name",b n)]),[])) parents)

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski )end) locales)

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski in fixTypeNames name (XML.Elem (("IsaExport",[("file",fname)]),

89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski [xml_imports,xml_consts,xml_axioms,xml_theorems,xml_types,xml_classes,xml_locales])) end

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederend;

e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder