export_helper.ml revision 255a89789d3d5b19f6a8c96bf6c260a96158ef6d
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersignature ExportHelper =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type const_info = (string * (typ * term option)) list
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type term_info = (string * term) list
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type datatype_info = (string * Datatype.info) list
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type theory_info =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder string (* theory name *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * string list (* imports *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * const_info (* constants *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* axioms *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* theorems *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * datatype_info (* data types *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val theory_info : theory -> theory_info
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val tinfo2xml : theory -> string -> theory_info -> XML.tree
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstructure ExportHelper : ExportHelper =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type const_info = (string * (typ * term option)) list
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type term_info = (string * term) list
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type datatype_info = (string * Datatype.info) list
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder type theory_info =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder string (* theory name *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * string list (* imports *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * const_info (* constants *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* axioms *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * term_info (* theorems *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder * datatype_info (* data types *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* General helper functions *)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun mergesort _ [] = []
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | mergesort _ [x] = [x]
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | mergesort cmp_data xs =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (ys,zs) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.foldl (fn(i, (ys,zs)) => (zs, i::ys)) ([],[]) xs
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun merge (xs,[]) = xs
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | merge ([],xs) = xs
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | merge (x::xr,y::yr) = if (cmp_data x) <= (cmp_data y)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder then x::merge(xr,y::yr)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder else y::merge(x::xr,yr)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in merge(mergesort cmp_data ys, mergesort cmp_data zs) end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* remove duplicate entries from a sorted list *)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun unique [] = []
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | unique [x] = [x]
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | unique (x1::x2::xr) = if x1 = x2
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder then unique (x2::xr)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder else x1::(unique (x2::xr))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (* remove xs from ys - both lists need to be sorted asc *)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove' _ _ ([],ys) = ys
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | remove' _ _ (_,[]) = []
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | remove' cd1 cd2 (x::xr,y::yr) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder if (cd1 x) < (cd2 y)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder then remove' cd1 cd2 (xr,y::yr)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder else if (cd2 y) < (cd1 x)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder then y::(remove' cd1 cd2 (x::xr,yr))
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder else remove' cd1 cd2 (xr,yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove cmp_data = remove' cmp_data cmp_data
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun remove_parent_data df cmp_data T =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val d = df T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val pd = (List.foldl op@ [] (map df (Context.parents_of T)))
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in remove cmp_data (mergesort cmp_data pd,mergesort cmp_data d) end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun filter rem (d : (string * 'a) list) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder remove' id #1 ((mergesort id rem),(mergesort #1 d))
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Theory-specific helpers *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* full name of a name used in theory T *)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun full_name T name = Name_Space.full_name (Sign.naming_of T) (Binding.name name)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* remove unnecessary information from (recursive) datatypes *)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun is_mutually_rec_type T (n,i) = (case (#alt_names i) of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (Option.isSome o (Datatype.get_info T) o (full_name T))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | NONE => false)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun check_rec T (n,v) = if is_mutually_rec_type T (n,v)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder then case String.compare (((#1 o #2 o List.hd o #descr) v),full_name T n) of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun restructure_rec_types T ts = List.foldl (fn (d,l) => case d of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (n,SOME(v)) => if check_rec T (n,v) then (n,v)::l
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | (_,NONE) => l) [] ts
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* get raw theory information *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_consts T =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val consts_of = (Name_Space.dest_table (Syntax.init_pretty_global T)) o
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder #constants o Consts.dest o Sign.consts_of
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in remove_parent_data consts_of #1 T end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val get_axioms = remove_parent_data Theory.axioms_of #1
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val get_theorems =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let fun theorems_of T = map (fn (a,b) => (a, prop_of b))
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in remove_parent_data theorems_of #1 end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_datatypes T =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val tname = Context.theory_name T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val ts = (#log_types o Type.rep_tsig o Sign.tsig_of) T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val ts' = map (fn s => (String.extract (s,tl+1,NONE),Datatype.get_info T s))
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (String.isPrefix tname) ts)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in restructure_rec_types T ts' end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Guess the names of generated axioms, consts and theorem *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun prefix p s = List.map (fn x => p^s^x)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun postfix s p = List.map (fn x => x^s^p)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun l_to_intl l = List.map Int.toString
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.tl (List.rev (List.foldl (fn (_,x::xs) => (x+1)::x::xs) [0] l)))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_type_names T ts =
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val rec_types = List.filter (is_mutually_rec_type T) ts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val grouped_rec_names = List.map (fn x => case (#alt_names o #2) x of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | NONE => []) rec_types
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val def_names = (List.map (Long_Name.base_name o #1 o #2)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.concat (List.map (#descr o #2) rec_types)))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val all_rec_names = (List.concat grouped_rec_names)@def_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val constructors = List.map #1 (List.concat (List.map (#3 o #2)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.concat (List.map (#descr o #2) ts))))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (grouped_rec_names,all_rec_names,constructors,def_names) end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_gen_consts T name ts =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (grouped_rec_names,all_rec_names,constructors,_) = get_type_names T ts
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val rec_names = List.concat grouped_rec_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val mutually_rec_names =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.filter (fn x => List.length x > 1) grouped_rec_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (fn x => List.length x = 1) grouped_rec_names)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in constructors@(prefix name "." (List.concat
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [prefix "Abs" "_" rec_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "Rep" "_" rec_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x) all_rec_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => let val comb = space_implode "_" x
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => [x^"."^x^"_rec",
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rec_set",
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rep_set"]) simple_names),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn x => let val comb = space_implode "_" x
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (comb^"."^comb^"_rec_set")::
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (comb^"."^comb^"_rep_set")::(List.concat
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn y => [comb^"."^comb^"_rec_"^y,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rec_set_"^y,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rep_set_"^y])
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (l_to_intl x))) end) mutually_rec_names)])) end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_gen_axioms T name ts =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (grouped_rec_names,all_rec_names,constructors,def_names) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder get_type_names T ts
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val rec_names = List.concat grouped_rec_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder grouped_rec_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (fn x => List.length x = 1) grouped_rec_names)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (postfix "_" "def" constructors)@(prefix name "." (List.concat
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [prefix "arity_type" "_" def_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "equal" "_" (postfix "_" "def_raw" def_names),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "type_definition" "_" rec_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x^"_def") def_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (postfix "_" "def"
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn x => let val comb = space_implode "_" x
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (comb^"."^comb^"_rec_set")::
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (comb^"."^comb^"_rep_set")::(List.concat
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (fn y => [comb^"."^comb^"_rec_"^y,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rec_set_"^y,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder comb^"."^comb^"_rep_set_"^y]) (l_to_intl x))) end)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder mutually_rec_names)),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => let val comb = space_implode "_" x
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.concat (List.map (fn x => [x^"."^x^"_rec",
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder x^"."^x^"_rec_set",
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder x^"."^x^"_rep_set"]) simple_names)]))])) end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun get_gen_theorems T name ts ths =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val (grouped_rec_names,all_rec_names,constructors,def_names) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder get_type_names T ts
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val rec_names = List.concat grouped_rec_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder grouped_rec_names
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (List.filter (fn x => List.length x = 1) grouped_rec_names)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in prefix name "." (List.concat
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [prefix "arity_equal" "_" def_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "arity_type" "_" def_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "type_definition" "_" rec_names,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "equal" "_" (postfix "_" "def" def_names),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder prefix "equal" "_" (postfix "_" "def_raw" def_names),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x) def_names])
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.filter (String.isPrefix (name^"."^x^".")) ths) (unique (rec_names@def_names))))
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder List.filter (String.isPrefix (name^"."^(space_implode "_" x)^".")) ths)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder mutually_rec_names)) end
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Represent collected data as XML *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* Enrich the (isabelle-builtin) XML representation of terms with infix information *)
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder fun xml_of_term' T t =
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder XML.Elem (("Const",a),t) =>
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (case (Syntax.guess_infix (Sign.syn_of T) (Lexicon.mark_const ((#2 o List.hd) a))) of
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder ("mixfix_i",string_of_int j)]
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder ("mixfix_i",string_of_int j)]
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder ("mixifix_i",string_of_int j)]
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder in XML.Elem (("Const",a@b),map (xml_of_term' T) t) end
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder | XML.Elem ((s,a),t) => XML.Elem ((s,a),map (xml_of_term' T) t)
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder fun xml_of_term T t = xml_of_term' T (XML_Syntax.xml_of_term t)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun remove_hol_true_prop t = case t of
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder $ (Const ("HOL.Trueprop",_), tm) => tm
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder fun termListToXML T section l = XML.Elem ((section,[]),List.map (
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fn (s,t) => XML.Elem (("Term",[("name",Long_Name.base_name s)]),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [xml_of_term T (remove_hol_true_prop t)])) l)
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder fun termTypListToXML T section l = XML.Elem ((section,[]),List.map (
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fn (s,(t,v)) => let val v' = case v of
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroeder SOME(tm) => (("Term",[("name",Long_Name.base_name s)]),[xml_of_term T tm])
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder | NONE => (("NoTerm",[]),[])
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in XML.Elem (("ConstDecl",[("name",Long_Name.base_name s)]),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [XML_Syntax.xml_of_type t,XML.Elem v']) end) l)
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fun dtypToXML (Datatype.DtTFree s) = XML.Elem (("DtTFree",[("s",s)]),[])
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | dtypToXML (Datatype.DtType (s,dtl)) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder XML.Elem (("DtType",[("s",s)]),List.map dtypToXML dtl)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder | dtypToXML (Datatype.DtRec i) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder XML.Elem (("DtRec",[("i",Int.toString i)]),[])
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fun constructorToXML (name,dtl) = XML.Elem
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder (("Constructor",[("val",Long_Name.base_name name)]),List.map dtypToXML dtl)
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder fun typeToXML d = List.map
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder (fn (i,(s,vs,dt)) => let val attrs = case (#alt_names d) of
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder SOME(ns) => if (List.nth (ns,i)) = (Long_Name.base_name s)
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder then [("i",Int.toString i),("name",Long_Name.base_name s)]
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder else [("i",Int.toString i),("name",Long_Name.base_name s),("altname",List.nth (ns,i))]
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder | NONE => [("i",Int.toString i),("name",Long_Name.base_name s)]
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder in XML.Elem (("RecType",attrs),[
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder XML.Elem (("Vars",[]),List.map dtypToXML vs),
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder XML.Elem (("Constructors",[]),List.map constructorToXML dt)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun typeListToXML section l = XML.Elem ((section,[]),List.map (
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fn (s,d) => XML.Elem (("TypeDecl",[("name",s)]),typeToXML d)) l)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Prepare data *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* make sure that type names local to the theory do not
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder have the theory name as prefix
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (because this is not their proper name) *)
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder fun fixTypeNames moduleName t = case t of
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder XML.Elem (("Type",a),c) => XML.Elem (("Type",
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder if n = "name" andalso String.isPrefix (moduleName^".") s
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder then (n,String.extract (s,(String.size moduleName)+1,NONE))
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder else (n,s)) a),
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder List.map (fixTypeNames moduleName) c)
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder XML.Elem (d,List.map (fixTypeNames moduleName) c)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(* Module interface *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* collect information necessary to reconstruct the theory *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun theory_info T =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder Context.theory_name (Theory.parents_of T)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val types = get_datatypes T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val consts = get_consts T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val thms = get_theorems T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val axioms = get_axioms T
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val gen_consts = get_gen_consts T name types
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val gen_thms = get_gen_theorems T name types (List.map #1 thms)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val gen_axioms = (get_gen_axioms T name types)@(List.map #1 thms)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in (name, imports,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (filter gen_consts consts),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (filter gen_axioms axioms),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (filter gen_thms thms),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (* export theory info as xml *)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder fun tinfo2xml T fname (name,imports,consts,axioms,thms,types) =
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder let val xml_imports = XML.Elem
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder (("Imports",[]), List.map (fn s => XML.Elem (("Import",[("name",s)]),[])) imports)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_consts = termTypListToXML T "Consts" consts
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_axioms = termListToXML T "Axioms" axioms
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_theorems = termListToXML T "Theorems" thms
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder val xml_types = typeListToXML "Types" types
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder in fixTypeNames name (XML.Elem (("IsaExport",[("file",fname)]),
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder [xml_imports,xml_consts,xml_axioms,xml_theorems,xml_types])) end